From dd7e4ef993a4e7335d0022d6ee62ab9e26d34ae9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= Date: Fri, 20 Dec 2024 10:51:30 +0000 Subject: [PATCH] Fix not being able to use rho as variable name in binder_induction ISSUES FIXED: #59 --- Tools/binder_induction.ML | 25 ++++++++++++++++--------- 1 file changed, 16 insertions(+), 9 deletions(-) diff --git a/Tools/binder_induction.ML b/Tools/binder_induction.ML index abbce0e..f135020 100644 --- a/Tools/binder_induction.ML +++ b/Tools/binder_induction.ML @@ -330,22 +330,29 @@ fun gen_binder_context_tactic mod_cases simp def_insts arbitrary avoiding taking fun mk_all (a, b) c = HOLogic.mk_all (a, b, c) val rho = Free ("\", fastype_of avoiding_dynamic); val inst_rule = infer_instantiate ctxt (map fst P_vars ~~ - @{map 4} (fn goal => fn inst => fn arb => fn defs => Thm.cterm_of ctxt ( - fold_rev Term.absfree (map dest_Free inst) (Term.absfree (dest_Free rho) ( - fold_rev mk_all arb (Induct.atomize_term ctxt ( - Logic.mk_implies (HOLogic.mk_Trueprop (mk_induct_equal ( - avoiding_dynamic, rho - )), fold_rev (curry Logic.mk_implies) (map Thm.prop_of defs) goal) + @{map 4} (fn goal => fn inst => fn arb => fn defs => + let + val goal' = fold_rev (curry Logic.mk_implies) (map Thm.prop_of defs) goal; + val rho = Free (hd (Term.rename_wrt_term goal' [dest_Free rho])) + in Thm.cterm_of ctxt ( + fold_rev Term.absfree (map dest_Free inst) (Term.absfree (dest_Free rho) ( + fold_rev mk_all arb (Induct.atomize_term ctxt ( + Logic.mk_implies (HOLogic.mk_Trueprop (mk_induct_equal ( + avoiding_dynamic, rho + )), goal') + )) )) - )) - )) goals'' finsts' arbitrary defs + ) end + ) goals'' finsts' arbitrary defs ) rule; val inst_concl = Thm.concl_of inst_rule; val inst_concls = Logic.dest_conjunction_list inst_concl; fun dest_induct_imp (Const (@{const_name HOL.induct_implies}, _) $ t1 $ t2) = (t2, t1) - fun to_pure_all (Const ("HOL.All", _) $ Abs (a, b, t)) = to_pure_all (subst_bound (Free (a, b), t)) + fun to_pure_all (Const ("HOL.All", _) $ Abs (a, b, t)) = + let val x = Free (hd (Term.rename_wrt_term t [(a, b)])) + in to_pure_all (subst_bound (x, t)) end | to_pure_all t = dest_induct_imp t val (inst_concls', rho_imps) = split_list (map (to_pure_all o HOLogic.dest_Trueprop) inst_concls); val (def_conclss, inst_concls') = split_list (map2 (fn defs =>