tuned slightly the previous commit
authorurbanc
Sat Apr 07 11:36:35 2007 +0200 (2007-04-07)
changeset 22610c8b5133045f3
parent 22609 40ade470e319
child 22611 0e008e3ddb1e
tuned slightly the previous commit
src/HOL/Nominal/Nominal.thy
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_permeq.ML
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Sat Apr 07 11:05:25 2007 +0200
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Sat Apr 07 11:36:35 2007 +0200
     1.3 @@ -443,6 +443,14 @@
     1.4  (* rules to calculate simple premutations *)
     1.5  lemmas at_calc = at2 at1 at3
     1.6  
     1.7 +lemma at_swap_simps:
     1.8 +  fixes a ::"'x"
     1.9 +  and   b ::"'x"
    1.10 +  assumes a: "at TYPE('x)"
    1.11 +  shows "[(a,b)]\<bullet>a = b"
    1.12 +  and   "[(a,b)]\<bullet>b = a"
    1.13 +  using a by (simp_all add: at_calc)
    1.14 +
    1.15  lemma at4: 
    1.16    assumes a: "at TYPE('x)"
    1.17    shows "infinite (UNIV::'x set)"
    1.18 @@ -1090,20 +1098,6 @@
    1.19  section {* further lemmas for permutation types *}
    1.20  (*==============================================*)
    1.21  
    1.22 -lemma swap_simp_a:
    1.23 -  fixes a ::"'x"
    1.24 -  and   b ::"'x"
    1.25 -  assumes a: "at TYPE('x)"
    1.26 -  shows "[(a,b)]\<bullet> a = b" 
    1.27 -  using a by (auto simp add:at_calc)
    1.28 -
    1.29 -lemma swap_simp_b:
    1.30 -  fixes a ::"'x"
    1.31 -  and   b ::"'x"
    1.32 -  assumes a: "at TYPE('x)"
    1.33 -  shows "[(a,b)]\<bullet> b = a" 
    1.34 -  using a by (auto simp add:at_calc)
    1.35 -
    1.36  lemma pt_rev_pi:
    1.37    fixes pi :: "'x prm"
    1.38    and   x  :: "'a"
     2.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat Apr 07 11:05:25 2007 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Apr 07 11:36:35 2007 +0200
     2.3 @@ -694,6 +694,7 @@
     2.4         val at_fresh            = thm "Nominal.at_fresh";
     2.5         val at_fresh_ineq       = thm "Nominal.at_fresh_ineq";
     2.6         val at_calc             = thms "Nominal.at_calc";
     2.7 +       val at_swap_simps       = thms "Nominal.at_swap_simps";
     2.8         val swap_simp_a         = thm "swap_simp_a";
     2.9         val swap_simp_b         = thm "swap_simp_b";
    2.10         val at_supp             = thm "Nominal.at_supp";
    2.11 @@ -787,6 +788,7 @@
    2.12  	    |>   PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])]
    2.13              ||>> PureThy.add_thmss [(("alpha'", inst_pt_at [abs_fun_eq']),[])]
    2.14              ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij] @ inst_pt_at [pt_swap_bij']),[])]
    2.15 +            ||>> PureThy.add_thmss [(("swap_simps", inst_at at_swap_simps),[])]	 
    2.16              ||>> PureThy.add_thmss 
    2.17  	      let val thms1 = inst_pt_at [pt_pi_rev];
    2.18  		  val thms2 = inst_pt_at [pt_rev_pi];
    2.19 @@ -802,8 +804,6 @@
    2.20              ||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
    2.21              ||>> PureThy.add_thmss [(("exists_fresh", inst_at [at_exists_fresh]),[])]
    2.22              ||>> PureThy.add_thmss [(("exists_fresh'", inst_at [at_exists_fresh']),[])]
    2.23 -            ||>> PureThy.add_thmss [(("swap_simp_a", inst_at [swap_simp_a]),[])]	 
    2.24 -            ||>> PureThy.add_thmss [(("swap_simp_b", inst_at [swap_simp_b]),[])]
    2.25              ||>> PureThy.add_thmss [(("all_eqvt", inst_pt_at [all_eqvt]),[NominalThmDecls.eqvt_add])] 
    2.26              ||>> PureThy.add_thmss [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_add])]
    2.27              ||>> PureThy.add_thmss 
     3.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Sat Apr 07 11:05:25 2007 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Sat Apr 07 11:36:35 2007 +0200
     3.3 @@ -71,7 +71,6 @@
     3.4  fun dynamic_thms st name = PureThy.get_thms (theory_of_thm st) (Name name);
     3.5  fun dynamic_thm  st name = PureThy.get_thm  (theory_of_thm st) (Name name);
     3.6  
     3.7 -fun eqvts_thms st = NominalThmDecls.get_eqvt_thms (theory_of_thm st);
     3.8  
     3.9  (* needed in the process of fully simplifying permutations *)
    3.10  val strong_congs = [thm "if_cong"]
    3.11 @@ -153,8 +152,18 @@
    3.12      end);
    3.13  
    3.14  (* general simplification of permutations and permutation that arose from eqvt-problems *)
    3.15 -val perm_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp","swap_simp_a","swap_simp_b"] (fn st => []);
    3.16 -val eqvt_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_pi_simp"] eqvts_thms;
    3.17 +val perm_simp = 
    3.18 +    let val simps = ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp","swap_simps"]
    3.19 +    in 
    3.20 +	perm_simp_gen simps (fn st => [])
    3.21 +    end;
    3.22 +
    3.23 +val eqvt_simp = 
    3.24 +    let val simps = ["perm_swap","perm_fresh_fresh","perm_pi_simp"]
    3.25 +	fun eqvts_thms st = NominalThmDecls.get_eqvt_thms (theory_of_thm st);
    3.26 +    in 
    3.27 +	perm_simp_gen simps eqvts_thms
    3.28 +    end;
    3.29  
    3.30  (* FIXME removes the name lookup for these theorems use an ml value instead *)
    3.31