--- 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>\<open>Nominal.perm\<close>, 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>\<open>Nominal.perm\<close>, T) $ t $ (u as Const (\<^const_name>\<open>Nominal.perm\<close>, U) $ r $ s) =>
let
@@ -115,9 +115,7 @@
end
| _ => NONE);
-val perm_simproc =
- Simplifier.make_simproc \<^context> "perm_simp"
- {lhss = [\<^term>\<open>pi1 \<bullet> (pi2 \<bullet> x)\<close>], proc = K perm_simproc'};
+val perm_simproc = \<^simproc_setup>\<open>passive perm_simp ("pi1 \<bullet> (pi2 \<bullet> x)") = \<open>K perm_proc\<close>\<close>;
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));
--- 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>\<open>Fun.id\<close>],
- 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 =
--- 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>\<open>Fun.id\<close>],
- 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;
--- 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>\<open>Nominal.perm pi x\<close>], proc = K perm_simproc_app'}
+val perm_app_simproc = \<^simproc_setup>\<open>passive perm_app ("Nominal.perm pi x") = \<open>K perm_app_proc\<close>\<close>
(* 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>\<open>Nominal.perm pi x\<close>], proc = K perm_simproc_fun'}
+val perm_fun_simproc = \<^simproc_setup>\<open>passive perm_fun ("Nominal.perm pi x") = \<open>K perm_fun_proc\<close>\<close>
(* 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>\<open>Nominal.perm\<close>, Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>list\<close>,
[Type (\<^type_name>\<open>Product_Type.prod\<close>, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const (\<^const_name>\<open>Nominal.perm\<close>,
@@ -217,9 +213,7 @@
| _ => NONE);
val perm_compose_simproc =
- Simplifier.make_simproc \<^context> "perm_compose"
- {lhss = [\<^term>\<open>Nominal.perm pi1 (Nominal.perm pi2 t)\<close>],
- proc = K perm_compose_simproc'}
+ \<^simproc_setup>\<open>passive perm_compose ("perm pi1 (perm pi2 t)") = \<open>K perm_compose_proc\<close>\<close>;
fun perm_compose_tac ctxt i =
("analysing permutation compositions on the lhs",