# HG changeset patch # User wenzelm # Date 1697839992 -7200 # Node ID aca84704d46f7a96873c7014915fa4fa9e134576 # Parent 62616d8422c5cd955a1277cf75f948ca6ae9f3f1 more standard simproc_setup using ML antiquotation; diff -r 62616d8422c5 -r aca84704d46f src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Fri Oct 20 22:19:05 2023 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Sat Oct 21 00:13:12 2023 +0200 @@ -93,7 +93,7 @@ fun permTs_of (Const (\<^const_name>\Nominal.perm\, T) $ t $ u) = fst (dest_permT T) :: permTs_of u | permTs_of _ = []; -fun perm_simproc' ctxt ct = +fun perm_proc ctxt ct = (case Thm.term_of ct of Const (\<^const_name>\Nominal.perm\, T) $ t $ (u as Const (\<^const_name>\Nominal.perm\, U) $ r $ s) => let @@ -115,9 +115,7 @@ end | _ => NONE); -val perm_simproc = - Simplifier.make_simproc \<^context> "perm_simp" - {lhss = [\<^term>\pi1 \ (pi2 \ x)\], proc = K perm_simproc'}; +val perm_simproc = \<^simproc_setup>\passive perm_simp ("pi1 \ (pi2 \ x)") = \K perm_proc\\; fun projections ctxt rule = Project_Rule.projections ctxt rule @@ -1562,7 +1560,7 @@ resolve_tac ctxt [rec_induct] 1 THEN REPEAT (simp_tac (put_simpset HOL_basic_ss ctxt addsimps flat perm_simps' - addsimprocs [NominalPermeq.perm_simproc_app]) 1 THEN + addsimprocs [NominalPermeq.perm_app_simproc]) 1 THEN (resolve_tac ctxt rec_intrs THEN_ALL_NEW asm_simp_tac (put_simpset HOL_ss ctxt addsimps (fresh_bij @ perm_bij))) 1)))) val ths' = map (fn ((P, Q), th) => @@ -1975,7 +1973,7 @@ [cut_facts_tac [th'] 1, full_simp_tac (put_simpset HOL_ss ctxt addsimps rec_eqns @ pi1_pi2_eqs @ perm_swap - addsimprocs [NominalPermeq.perm_simproc_app]) 1, + addsimprocs [NominalPermeq.perm_app_simproc]) 1, full_simp_tac (put_simpset HOL_ss context'' addsimps (calc_atm @ fresh_prems' @ freshs2' @ perm_fresh_fresh)) 1]) end; @@ -2008,7 +2006,7 @@ (fold_rev (mk_perm []) pi1 rhs', fold_rev (mk_perm []) pi2 lhs'))) (fn _ => simp_tac (put_simpset HOL_ss context'' addsimps pi1_pi2_eqs @ rec_eqns - addsimprocs [NominalPermeq.perm_simproc_app]) 1 THEN + addsimprocs [NominalPermeq.perm_app_simproc]) 1 THEN TRY (simp_tac (put_simpset HOL_ss context'' addsimps (fresh_prems' @ freshs2' @ calc_atm @ perm_fresh_fresh)) 1)); diff -r 62616d8422c5 -r aca84704d46f src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Fri Oct 20 22:19:05 2023 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Sat Oct 21 00:13:12 2023 +0200 @@ -279,7 +279,7 @@ put_simpset HOL_basic_ss ctxt addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) addsimprocs [mk_perm_bool_simproc [\<^const_name>\Fun.id\], - NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; + NominalPermeq.perm_app_simproc, NominalPermeq.perm_fun_simproc]; val fresh_bij = Global_Theory.get_thms thy "fresh_bij"; val perm_bij = Global_Theory.get_thms thy "perm_bij"; val fs_atoms = map (fn aT => Global_Theory.get_thm thy @@ -467,7 +467,7 @@ fun cases_eqvt_simpset ctxt = put_simpset HOL_ss ctxt addsimps eqvt_thms @ swap_simps @ perm_pi_simp - addsimprocs [NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; + addsimprocs [NominalPermeq.perm_app_simproc, NominalPermeq.perm_fun_simproc]; fun simp_fresh_atm ctxt = Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps fresh_atm); @@ -626,7 +626,7 @@ fun eqvt_simpset ctxt = put_simpset HOL_basic_ss ctxt addsimps (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs [mk_perm_bool_simproc names, - NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; + NominalPermeq.perm_app_simproc, NominalPermeq.perm_fun_simproc]; val ps = map (fst o HOLogic.dest_imp) (HOLogic.dest_conj (HOLogic.dest_Trueprop t)); fun eqvt_tac ctxt pi (intr, vs) st = diff -r 62616d8422c5 -r aca84704d46f src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Fri Oct 20 22:19:05 2023 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Sat Oct 21 00:13:12 2023 +0200 @@ -298,7 +298,7 @@ put_simpset HOL_basic_ss ctxt addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) addsimprocs [mk_perm_bool_simproc [\<^const_name>\Fun.id\], - NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; + NominalPermeq.perm_app_simproc, NominalPermeq.perm_fun_simproc]; val fresh_star_bij = Global_Theory.get_thms thy "fresh_star_bij"; val pt_insts = map (NominalAtoms.pt_inst_of thy) atoms; val at_insts = map (NominalAtoms.at_inst_of thy) atoms; diff -r 62616d8422c5 -r aca84704d46f src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Fri Oct 20 22:19:05 2023 +0200 +++ b/src/HOL/Nominal/nominal_permeq.ML Sat Oct 21 00:13:12 2023 +0200 @@ -27,8 +27,8 @@ signature NOMINAL_PERMEQ = sig - val perm_simproc_fun : simproc - val perm_simproc_app : simproc + val perm_fun_simproc : simproc + val perm_app_simproc : simproc val perm_simp_tac : Proof.context -> int -> tactic val perm_extend_simp_tac : Proof.context -> int -> tactic @@ -85,7 +85,7 @@ (* of applications; just adding this rule to the simplifier *) (* would loop; it also needs careful tuning with the simproc *) (* for functions to avoid further possibilities for looping *) -fun perm_simproc_app' ctxt ct = +fun perm_app_proc ctxt ct = let val thy = Proof_Context.theory_of ctxt val redex = Thm.term_of ct @@ -112,12 +112,10 @@ | _ => NONE end -val perm_simproc_app = - Simplifier.make_simproc \<^context> "perm_simproc_app" - {lhss = [\<^term>\Nominal.perm pi x\], proc = K perm_simproc_app'} +val perm_app_simproc = \<^simproc_setup>\passive perm_app ("Nominal.perm pi x") = \K perm_app_proc\\ (* a simproc that deals with permutation instances in front of functions *) -fun perm_simproc_fun' ctxt ct = +fun perm_fun_proc ctxt ct = let val redex = Thm.term_of ct fun applicable_fun t = @@ -134,9 +132,7 @@ | _ => NONE end -val perm_simproc_fun = - Simplifier.make_simproc \<^context> "perm_simproc_fun" - {lhss = [\<^term>\Nominal.perm pi x\], proc = K perm_simproc_fun'} +val perm_fun_simproc = \<^simproc_setup>\passive perm_fun ("Nominal.perm pi x") = \K perm_fun_proc\\ (* function for simplyfying permutations *) (* stac contains the simplifiation tactic that is *) @@ -146,7 +142,7 @@ let val ctxt' = ctxt addsimps (maps (Proof_Context.get_thms ctxt) dyn_thms @ eqvt_thms) - addsimprocs [perm_simproc_fun, perm_simproc_app] + addsimprocs [perm_fun_simproc, perm_app_simproc] |> fold Simplifier.del_cong weak_congs |> fold Simplifier.add_cong strong_congs in @@ -188,7 +184,7 @@ (* generating perm_aux'es for the outermost permutation and then un- *) (* folding the definition *) -fun perm_compose_simproc' ctxt ct = +fun perm_compose_proc ctxt ct = (case Thm.term_of ct of (Const (\<^const_name>\Nominal.perm\, Type (\<^type_name>\fun\, [Type (\<^type_name>\list\, [Type (\<^type_name>\Product_Type.prod\, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const (\<^const_name>\Nominal.perm\, @@ -217,9 +213,7 @@ | _ => NONE); val perm_compose_simproc = - Simplifier.make_simproc \<^context> "perm_compose" - {lhss = [\<^term>\Nominal.perm pi1 (Nominal.perm pi2 t)\], - proc = K perm_compose_simproc'} + \<^simproc_setup>\passive perm_compose ("perm pi1 (perm pi2 t)") = \K perm_compose_proc\\; fun perm_compose_tac ctxt i = ("analysing permutation compositions on the lhs",