added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
authorurbanc
Mon May 15 19:40:17 2006 +0200 (2006-05-15)
changeset 196384358b88a9d12
parent 19637 d33a71ffb9e3
child 19639 d9079a9ccbfb
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
(they are used in the proof of the strong
induction principle)

added code to nominal_atoms to collect these
lemmas in "fresh_aux" instantiated for each
atom type

deleted the fresh_fun_eqvt from nominal_atoms,
since fresh_fun is not used anymore in the recursion
combinator
src/HOL/Nominal/Nominal.thy
src/HOL/Nominal/nominal_atoms.ML
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Sat May 13 21:13:25 2006 +0200
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Mon May 15 19:40:17 2006 +0200
     1.3 @@ -847,6 +847,38 @@
     1.4  apply(rule at_ds8[OF at])
     1.5  done
     1.6  
     1.7 +section {* disjointness properties *}
     1.8 +(*=================================*)
     1.9 +lemma dj_perm_forget:
    1.10 +  fixes pi::"'y prm"
    1.11 +  and   x ::"'x"
    1.12 +  assumes dj: "disjoint TYPE('x) TYPE('y)"
    1.13 +  shows "pi\<bullet>x=x" 
    1.14 +  using dj by (simp_all add: disjoint_def)
    1.15 +
    1.16 +lemma dj_perm_perm_forget:
    1.17 +  fixes pi1::"'x prm"
    1.18 +  and   pi2::"'y prm"
    1.19 +  assumes dj: "disjoint TYPE('x) TYPE('y)"
    1.20 +  shows "pi2\<bullet>pi1=pi1"
    1.21 +  using dj by (induct pi1, auto simp add: disjoint_def)
    1.22 +
    1.23 +lemma dj_cp:
    1.24 +  fixes pi1::"'x prm"
    1.25 +  and   pi2::"'y prm"
    1.26 +  and   x  ::"'a"
    1.27 +  assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
    1.28 +  and     dj: "disjoint TYPE('y) TYPE('x)"
    1.29 +  shows "pi1\<bullet>(pi2\<bullet>x) = (pi2)\<bullet>(pi1\<bullet>x)"
    1.30 +  by (simp add: cp1[OF cp] dj_perm_perm_forget[OF dj])
    1.31 +
    1.32 +lemma dj_supp:
    1.33 +  fixes a::"'x"
    1.34 +  assumes dj: "disjoint TYPE('x) TYPE('y)"
    1.35 +  shows "(supp a) = ({}::'y set)"
    1.36 +apply(simp add: supp_def dj_perm_forget[OF dj])
    1.37 +done
    1.38 +
    1.39  section {* permutation type instances *}
    1.40  (* ===================================*)
    1.41  
    1.42 @@ -1399,6 +1431,32 @@
    1.43    with a2' neg show False by simp
    1.44  qed
    1.45  
    1.46 +(* the next two lemmas are needed in the proof *)
    1.47 +(* of the structural induction principle       *)
    1.48 +lemma pt_fresh_aux:
    1.49 +  fixes a::"'x"
    1.50 +  and   b::"'x"
    1.51 +  and   c::"'x"
    1.52 +  and   x::"'a"
    1.53 +  assumes pt: "pt TYPE('a) TYPE('x)"
    1.54 +  and     at: "at TYPE ('x)"
    1.55 +  assumes a1: "c\<noteq>a" and  a2: "a\<sharp>x" and a3: "c\<sharp>x"
    1.56 +  shows "c\<sharp>([(a,b)]\<bullet>x)"
    1.57 +using a1 a2 a3 by (simp_all add: pt_fresh_left[OF pt, OF at] at_calc[OF at])
    1.58 +
    1.59 +lemma pt_fresh_aux_ineq:
    1.60 +  fixes pi::"'x prm"
    1.61 +  and   c::"'y"
    1.62 +  and   x::"'a"
    1.63 +  assumes pta: "pt TYPE('a) TYPE('x)"
    1.64 +  and     ptb: "pt TYPE('y) TYPE('x)"
    1.65 +  and     at:  "at TYPE('x)"
    1.66 +  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
    1.67 +  and     dj:  "disjoint TYPE('y) TYPE('x)"
    1.68 +  assumes a: "c\<sharp>x"
    1.69 +  shows "c\<sharp>(pi\<bullet>x)"
    1.70 +using a by (simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj])
    1.71 +
    1.72  -- "three helper lemmas for the perm_fresh_fresh-lemma"
    1.73  lemma comprehension_neg_UNIV: "{b. \<not> P b} = UNIV - {b. P b}"
    1.74    by (auto)
    1.75 @@ -2082,38 +2140,6 @@
    1.76    shows "a\<sharp>(set xs) = a\<sharp>xs"
    1.77  by (simp add: fresh_def pt_list_set_supp[OF pt, OF at, OF fs])
    1.78   
    1.79 -section {* disjointness properties *}
    1.80 -(*=================================*)
    1.81 -lemma dj_perm_forget:
    1.82 -  fixes pi::"'y prm"
    1.83 -  and   x ::"'x"
    1.84 -  assumes dj: "disjoint TYPE('x) TYPE('y)"
    1.85 -  shows "pi\<bullet>x=x"
    1.86 -  using dj by (simp add: disjoint_def)
    1.87 -
    1.88 -lemma dj_perm_perm_forget:
    1.89 -  fixes pi1::"'x prm"
    1.90 -  and   pi2::"'y prm"
    1.91 -  assumes dj: "disjoint TYPE('x) TYPE('y)"
    1.92 -  shows "pi2\<bullet>pi1=pi1"
    1.93 -  using dj by (induct pi1, auto simp add: disjoint_def)
    1.94 -
    1.95 -lemma dj_cp:
    1.96 -  fixes pi1::"'x prm"
    1.97 -  and   pi2::"'y prm"
    1.98 -  and   x  ::"'a"
    1.99 -  assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
   1.100 -  and     dj: "disjoint TYPE('y) TYPE('x)"
   1.101 -  shows "pi1\<bullet>(pi2\<bullet>x) = (pi2)\<bullet>(pi1\<bullet>x)"
   1.102 -  by (simp add: cp1[OF cp] dj_perm_perm_forget[OF dj])
   1.103 -
   1.104 -lemma dj_supp:
   1.105 -  fixes a::"'x"
   1.106 -  assumes dj: "disjoint TYPE('x) TYPE('y)"
   1.107 -  shows "(supp a) = ({}::'y set)"
   1.108 -apply(simp add: supp_def dj_perm_forget[OF dj])
   1.109 -done
   1.110 -
   1.111  section {* composition instances *}
   1.112  (* ============================= *)
   1.113  
   1.114 @@ -2911,4 +2937,14 @@
   1.115    {* finite_gs_meth_debug *}
   1.116    {* tactic for deciding whether something has finite support including debuging facilities *}
   1.117  
   1.118 +(* FIXME: this code has not yet been checked in
   1.119 +method_setup fresh_guess =
   1.120 +  {* fresh_gs_meth *}
   1.121 +  {* tactic for deciding whether an atom is fresh for something*}
   1.122 +
   1.123 +method_setup fresh_guess_debug =
   1.124 +  {* fresh_gs_meth_debug *}
   1.125 +  {* tactic for deciding whether an atom is fresh for something including debuging facilities *}
   1.126 +*)
   1.127 +
   1.128  end
     2.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat May 13 21:13:25 2006 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Mon May 15 19:40:17 2006 +0200
     2.3 @@ -677,9 +677,11 @@
     2.4         val fresh_right         = thm "Nominal.pt_fresh_right";
     2.5         val fresh_bij_ineq      = thm "Nominal.pt_fresh_bij_ineq";
     2.6         val fresh_bij           = thm "Nominal.pt_fresh_bij";
     2.7 +       val fresh_aux_ineq      = thm "Nominal.pt_fresh_aux_ineq";
     2.8 +       val fresh_aux           = thm "Nominal.pt_fresh_aux";
     2.9         val pt_pi_rev           = thm "Nominal.pt_pi_rev";
    2.10         val pt_rev_pi           = thm "Nominal.pt_rev_pi";
    2.11 -       val fresh_fun_eqvt      = thm "Nominal.fresh_fun_equiv";
    2.12 +  
    2.13  
    2.14         (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
    2.15         (* types; this allows for example to use abs_perm (which is a      *)
    2.16 @@ -791,7 +793,10 @@
    2.17  	      let val thms1 = inst_pt_at [fresh_bij]
    2.18  		  and thms2 = inst_pt_pt_at_cp [fresh_bij_ineq]
    2.19  	      in [(("fresh_eqvt", thms1 @ thms2),[])] end
    2.20 -            ||>> PureThy.add_thmss [(("fresh_fun_eqvt",inst_pt_at [fresh_fun_eqvt]),[])]
    2.21 +            ||>> PureThy.add_thmss
    2.22 +	      let val thms1 = inst_pt_at [fresh_aux]
    2.23 +		  and thms2 = inst_pt_pt_at_cp_dj [fresh_aux_ineq]
    2.24 +	      in [(("fresh_aux", thms1 @ thms2),[])] end
    2.25  	   end;
    2.26  
    2.27      in NominalData.put (fold Symtab.update (map (rpair ()) full_ak_names)