--- a/src/HOL/Nominal/Nominal.thy Sat Apr 07 11:05:25 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy Sat Apr 07 11:36:35 2007 +0200
@@ -443,6 +443,14 @@
(* rules to calculate simple premutations *)
lemmas at_calc = at2 at1 at3
+lemma at_swap_simps:
+ fixes a ::"'x"
+ and b ::"'x"
+ assumes a: "at TYPE('x)"
+ shows "[(a,b)]\<bullet>a = b"
+ and "[(a,b)]\<bullet>b = a"
+ using a by (simp_all add: at_calc)
+
lemma at4:
assumes a: "at TYPE('x)"
shows "infinite (UNIV::'x set)"
@@ -1090,20 +1098,6 @@
section {* further lemmas for permutation types *}
(*==============================================*)
-lemma swap_simp_a:
- fixes a ::"'x"
- and b ::"'x"
- assumes a: "at TYPE('x)"
- shows "[(a,b)]\<bullet> a = b"
- using a by (auto simp add:at_calc)
-
-lemma swap_simp_b:
- fixes a ::"'x"
- and b ::"'x"
- assumes a: "at TYPE('x)"
- shows "[(a,b)]\<bullet> b = a"
- using a by (auto simp add:at_calc)
-
lemma pt_rev_pi:
fixes pi :: "'x prm"
and x :: "'a"
--- a/src/HOL/Nominal/nominal_atoms.ML Sat Apr 07 11:05:25 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Sat Apr 07 11:36:35 2007 +0200
@@ -694,6 +694,7 @@
val at_fresh = thm "Nominal.at_fresh";
val at_fresh_ineq = thm "Nominal.at_fresh_ineq";
val at_calc = thms "Nominal.at_calc";
+ val at_swap_simps = thms "Nominal.at_swap_simps";
val swap_simp_a = thm "swap_simp_a";
val swap_simp_b = thm "swap_simp_b";
val at_supp = thm "Nominal.at_supp";
@@ -787,6 +788,7 @@
|> PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])]
||>> PureThy.add_thmss [(("alpha'", inst_pt_at [abs_fun_eq']),[])]
||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij] @ inst_pt_at [pt_swap_bij']),[])]
+ ||>> PureThy.add_thmss [(("swap_simps", inst_at at_swap_simps),[])]
||>> PureThy.add_thmss
let val thms1 = inst_pt_at [pt_pi_rev];
val thms2 = inst_pt_at [pt_rev_pi];
@@ -802,8 +804,6 @@
||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
||>> PureThy.add_thmss [(("exists_fresh", inst_at [at_exists_fresh]),[])]
||>> PureThy.add_thmss [(("exists_fresh'", inst_at [at_exists_fresh']),[])]
- ||>> PureThy.add_thmss [(("swap_simp_a", inst_at [swap_simp_a]),[])]
- ||>> PureThy.add_thmss [(("swap_simp_b", inst_at [swap_simp_b]),[])]
||>> PureThy.add_thmss [(("all_eqvt", inst_pt_at [all_eqvt]),[NominalThmDecls.eqvt_add])]
||>> PureThy.add_thmss [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_add])]
||>> PureThy.add_thmss
--- a/src/HOL/Nominal/nominal_permeq.ML Sat Apr 07 11:05:25 2007 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Sat Apr 07 11:36:35 2007 +0200
@@ -71,7 +71,6 @@
fun dynamic_thms st name = PureThy.get_thms (theory_of_thm st) (Name name);
fun dynamic_thm st name = PureThy.get_thm (theory_of_thm st) (Name name);
-fun eqvts_thms st = NominalThmDecls.get_eqvt_thms (theory_of_thm st);
(* needed in the process of fully simplifying permutations *)
val strong_congs = [thm "if_cong"]
@@ -153,8 +152,18 @@
end);
(* general simplification of permutations and permutation that arose from eqvt-problems *)
-val perm_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp","swap_simp_a","swap_simp_b"] (fn st => []);
-val eqvt_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_pi_simp"] eqvts_thms;
+val perm_simp =
+ let val simps = ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp","swap_simps"]
+ in
+ perm_simp_gen simps (fn st => [])
+ end;
+
+val eqvt_simp =
+ let val simps = ["perm_swap","perm_fresh_fresh","perm_pi_simp"]
+ fun eqvts_thms st = NominalThmDecls.get_eqvt_thms (theory_of_thm st);
+ in
+ perm_simp_gen simps eqvts_thms
+ end;
(* FIXME removes the name lookup for these theorems use an ml value instead *)