perm_simp can now simplify using the rules (a,b) o a = b and (a,b) o b = a
authornarboux
Sat Apr 07 11:05:25 2007 +0200 (2007-04-07)
changeset 2260940ade470e319
parent 22608 092a3353241e
child 22610 c8b5133045f3
perm_simp can now simplify using the rules (a,b) o a = b and (a,b) o b = a
src/HOL/Nominal/Examples/Crary.thy
src/HOL/Nominal/Nominal.thy
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_permeq.ML
     1.1 --- a/src/HOL/Nominal/Examples/Crary.thy	Fri Apr 06 01:26:30 2007 +0200
     1.2 +++ b/src/HOL/Nominal/Examples/Crary.thy	Sat Apr 07 11:05:25 2007 +0200
     1.3 @@ -318,8 +318,9 @@
     1.4  inductive_cases2 t_Lam_elim_auto[elim]: "\<Gamma> \<turnstile> Lam [x].t : T"
     1.5  inductive_cases2 t_Var_elim_auto[elim]: "\<Gamma> \<turnstile> Var x : T"
     1.6  inductive_cases2 t_App_elim_auto[elim]: "\<Gamma> \<turnstile> App x y : T"
     1.7 -inductive_cases2  t_Const_elim_auto[elim]: "\<Gamma> \<turnstile> Const n : T"
     1.8 -inductive_cases2  t_Unit_elim_auto[elim]: "\<Gamma> \<turnstile> Unit : TUnit"
     1.9 +inductive_cases2 t_Const_elim_auto[elim]: "\<Gamma> \<turnstile> Const n : T"
    1.10 +inductive_cases2 t_Unit_elim_auto[elim]: "\<Gamma> \<turnstile> Unit : TUnit"
    1.11 +inductive_cases2 t_Unit_elim_auto'[elim]: "\<Gamma> \<turnstile> s : TUnit"
    1.12  
    1.13  declare trm.inject [simp del]
    1.14  declare ty.inject [simp del]
    1.15 @@ -479,12 +480,6 @@
    1.16  declare trm.inject [simp del]
    1.17  declare ty.inject [simp del]
    1.18  
    1.19 -(* FIXME this lemma should not be here *)
    1.20 -lemma perm_basic[simp]:
    1.21 - fixes x y::"name"
    1.22 -shows "[(x,y)]\<bullet>y = x"
    1.23 -using assms using calc_atm by perm_simp
    1.24 -
    1.25  lemma Q_Arrow_strong_inversion:
    1.26    assumes fs: "x\<sharp>\<Gamma>" "x\<sharp>t" "x\<sharp>u" 
    1.27    and h: "\<Gamma> \<turnstile> t \<Leftrightarrow> u : T\<^isub>1\<rightarrow>T\<^isub>2"
     2.1 --- a/src/HOL/Nominal/Nominal.thy	Fri Apr 06 01:26:30 2007 +0200
     2.2 +++ b/src/HOL/Nominal/Nominal.thy	Sat Apr 07 11:05:25 2007 +0200
     2.3 @@ -1090,6 +1090,20 @@
     2.4  section {* further lemmas for permutation types *}
     2.5  (*==============================================*)
     2.6  
     2.7 +lemma swap_simp_a:
     2.8 +  fixes a ::"'x"
     2.9 +  and   b ::"'x"
    2.10 +  assumes a: "at TYPE('x)"
    2.11 +  shows "[(a,b)]\<bullet> a = b" 
    2.12 +  using a by (auto simp add:at_calc)
    2.13 +
    2.14 +lemma swap_simp_b:
    2.15 +  fixes a ::"'x"
    2.16 +  and   b ::"'x"
    2.17 +  assumes a: "at TYPE('x)"
    2.18 +  shows "[(a,b)]\<bullet> b = a" 
    2.19 +  using a by (auto simp add:at_calc)
    2.20 +
    2.21  lemma pt_rev_pi:
    2.22    fixes pi :: "'x prm"
    2.23    and   x  :: "'a"
     3.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Fri Apr 06 01:26:30 2007 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Apr 07 11:05:25 2007 +0200
     3.3 @@ -694,6 +694,8 @@
     3.4         val at_fresh            = thm "Nominal.at_fresh";
     3.5         val at_fresh_ineq       = thm "Nominal.at_fresh_ineq";
     3.6         val at_calc             = thms "Nominal.at_calc";
     3.7 +       val swap_simp_a         = thm "swap_simp_a";
     3.8 +       val swap_simp_b         = thm "swap_simp_b";
     3.9         val at_supp             = thm "Nominal.at_supp";
    3.10         val dj_supp             = thm "Nominal.dj_supp";
    3.11         val fresh_left_ineq     = thm "Nominal.pt_fresh_left_ineq";
    3.12 @@ -800,6 +802,8 @@
    3.13              ||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
    3.14              ||>> PureThy.add_thmss [(("exists_fresh", inst_at [at_exists_fresh]),[])]
    3.15              ||>> PureThy.add_thmss [(("exists_fresh'", inst_at [at_exists_fresh']),[])]
    3.16 +            ||>> PureThy.add_thmss [(("swap_simp_a", inst_at [swap_simp_a]),[])]	 
    3.17 +            ||>> PureThy.add_thmss [(("swap_simp_b", inst_at [swap_simp_b]),[])]
    3.18              ||>> PureThy.add_thmss [(("all_eqvt", inst_pt_at [all_eqvt]),[NominalThmDecls.eqvt_add])] 
    3.19              ||>> PureThy.add_thmss [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_add])]
    3.20              ||>> PureThy.add_thmss 
     4.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Fri Apr 06 01:26:30 2007 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Sat Apr 07 11:05:25 2007 +0200
     4.3 @@ -153,7 +153,7 @@
     4.4      end);
     4.5  
     4.6  (* general simplification of permutations and permutation that arose from eqvt-problems *)
     4.7 -val perm_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp"] (fn st => []);
     4.8 +val perm_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp","swap_simp_a","swap_simp_b"] (fn st => []);
     4.9  val eqvt_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_pi_simp"] eqvts_thms;
    4.10  
    4.11  (* FIXME removes the name lookup for these theorems use an ml value instead *)