# HG changeset patch # User urbanc # Date 1175938595 -7200 # Node ID c8b5133045f396a57ff8b729933bf03aabf36f92 # Parent 40ade470e3193dcaf2b1240c3aca001fac0d7c59 tuned slightly the previous commit diff -r 40ade470e319 -r c8b5133045f3 src/HOL/Nominal/Nominal.thy --- 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)]\a = b" + and "[(a,b)]\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)]\ 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)]\ b = a" - using a by (auto simp add:at_calc) - lemma pt_rev_pi: fixes pi :: "'x prm" and x :: "'a" diff -r 40ade470e319 -r c8b5133045f3 src/HOL/Nominal/nominal_atoms.ML --- 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 diff -r 40ade470e319 -r c8b5133045f3 src/HOL/Nominal/nominal_permeq.ML --- 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 *)