# HG changeset patch
# User urbanc
# Date 1147714817 -7200
# Node ID 4358b88a9d1286327899099ee78456f0982f861f
# Parent  d33a71ffb9e3947edb6af71992103499e992fd4c
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

diff -r d33a71ffb9e3 -r 4358b88a9d12 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Sat May 13 21:13:25 2006 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Mon May 15 19:40:17 2006 +0200
@@ -847,6 +847,38 @@
 apply(rule at_ds8[OF at])
 done
 
+section {* disjointness properties *}
+(*=================================*)
+lemma dj_perm_forget:
+  fixes pi::"'y prm"
+  and   x ::"'x"
+  assumes dj: "disjoint TYPE('x) TYPE('y)"
+  shows "pi\<bullet>x=x" 
+  using dj by (simp_all add: disjoint_def)
+
+lemma dj_perm_perm_forget:
+  fixes pi1::"'x prm"
+  and   pi2::"'y prm"
+  assumes dj: "disjoint TYPE('x) TYPE('y)"
+  shows "pi2\<bullet>pi1=pi1"
+  using dj by (induct pi1, auto simp add: disjoint_def)
+
+lemma dj_cp:
+  fixes pi1::"'x prm"
+  and   pi2::"'y prm"
+  and   x  ::"'a"
+  assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
+  and     dj: "disjoint TYPE('y) TYPE('x)"
+  shows "pi1\<bullet>(pi2\<bullet>x) = (pi2)\<bullet>(pi1\<bullet>x)"
+  by (simp add: cp1[OF cp] dj_perm_perm_forget[OF dj])
+
+lemma dj_supp:
+  fixes a::"'x"
+  assumes dj: "disjoint TYPE('x) TYPE('y)"
+  shows "(supp a) = ({}::'y set)"
+apply(simp add: supp_def dj_perm_forget[OF dj])
+done
+
 section {* permutation type instances *}
 (* ===================================*)
 
@@ -1399,6 +1431,32 @@
   with a2' neg show False by simp
 qed
 
+(* the next two lemmas are needed in the proof *)
+(* of the structural induction principle       *)
+lemma pt_fresh_aux:
+  fixes a::"'x"
+  and   b::"'x"
+  and   c::"'x"
+  and   x::"'a"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE ('x)"
+  assumes a1: "c\<noteq>a" and  a2: "a\<sharp>x" and a3: "c\<sharp>x"
+  shows "c\<sharp>([(a,b)]\<bullet>x)"
+using a1 a2 a3 by (simp_all add: pt_fresh_left[OF pt, OF at] at_calc[OF at])
+
+lemma pt_fresh_aux_ineq:
+  fixes pi::"'x prm"
+  and   c::"'y"
+  and   x::"'a"
+  assumes pta: "pt TYPE('a) TYPE('x)"
+  and     ptb: "pt TYPE('y) TYPE('x)"
+  and     at:  "at TYPE('x)"
+  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
+  and     dj:  "disjoint TYPE('y) TYPE('x)"
+  assumes a: "c\<sharp>x"
+  shows "c\<sharp>(pi\<bullet>x)"
+using a by (simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj])
+
 -- "three helper lemmas for the perm_fresh_fresh-lemma"
 lemma comprehension_neg_UNIV: "{b. \<not> P b} = UNIV - {b. P b}"
   by (auto)
@@ -2082,38 +2140,6 @@
   shows "a\<sharp>(set xs) = a\<sharp>xs"
 by (simp add: fresh_def pt_list_set_supp[OF pt, OF at, OF fs])
  
-section {* disjointness properties *}
-(*=================================*)
-lemma dj_perm_forget:
-  fixes pi::"'y prm"
-  and   x ::"'x"
-  assumes dj: "disjoint TYPE('x) TYPE('y)"
-  shows "pi\<bullet>x=x"
-  using dj by (simp add: disjoint_def)
-
-lemma dj_perm_perm_forget:
-  fixes pi1::"'x prm"
-  and   pi2::"'y prm"
-  assumes dj: "disjoint TYPE('x) TYPE('y)"
-  shows "pi2\<bullet>pi1=pi1"
-  using dj by (induct pi1, auto simp add: disjoint_def)
-
-lemma dj_cp:
-  fixes pi1::"'x prm"
-  and   pi2::"'y prm"
-  and   x  ::"'a"
-  assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
-  and     dj: "disjoint TYPE('y) TYPE('x)"
-  shows "pi1\<bullet>(pi2\<bullet>x) = (pi2)\<bullet>(pi1\<bullet>x)"
-  by (simp add: cp1[OF cp] dj_perm_perm_forget[OF dj])
-
-lemma dj_supp:
-  fixes a::"'x"
-  assumes dj: "disjoint TYPE('x) TYPE('y)"
-  shows "(supp a) = ({}::'y set)"
-apply(simp add: supp_def dj_perm_forget[OF dj])
-done
-
 section {* composition instances *}
 (* ============================= *)
 
@@ -2911,4 +2937,14 @@
   {* finite_gs_meth_debug *}
   {* tactic for deciding whether something has finite support including debuging facilities *}
 
+(* FIXME: this code has not yet been checked in
+method_setup fresh_guess =
+  {* fresh_gs_meth *}
+  {* tactic for deciding whether an atom is fresh for something*}
+
+method_setup fresh_guess_debug =
+  {* fresh_gs_meth_debug *}
+  {* tactic for deciding whether an atom is fresh for something including debuging facilities *}
+*)
+
 end
diff -r d33a71ffb9e3 -r 4358b88a9d12 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Sat May 13 21:13:25 2006 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Mon May 15 19:40:17 2006 +0200
@@ -677,9 +677,11 @@
        val fresh_right         = thm "Nominal.pt_fresh_right";
        val fresh_bij_ineq      = thm "Nominal.pt_fresh_bij_ineq";
        val fresh_bij           = thm "Nominal.pt_fresh_bij";
+       val fresh_aux_ineq      = thm "Nominal.pt_fresh_aux_ineq";
+       val fresh_aux           = thm "Nominal.pt_fresh_aux";
        val pt_pi_rev           = thm "Nominal.pt_pi_rev";
        val pt_rev_pi           = thm "Nominal.pt_rev_pi";
-       val fresh_fun_eqvt      = thm "Nominal.fresh_fun_equiv";
+  
 
        (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
        (* types; this allows for example to use abs_perm (which is a      *)
@@ -791,7 +793,10 @@
 	      let val thms1 = inst_pt_at [fresh_bij]
 		  and thms2 = inst_pt_pt_at_cp [fresh_bij_ineq]
 	      in [(("fresh_eqvt", thms1 @ thms2),[])] end
-            ||>> PureThy.add_thmss [(("fresh_fun_eqvt",inst_pt_at [fresh_fun_eqvt]),[])]
+            ||>> PureThy.add_thmss
+	      let val thms1 = inst_pt_at [fresh_aux]
+		  and thms2 = inst_pt_pt_at_cp_dj [fresh_aux_ineq]
+	      in [(("fresh_aux", thms1 @ thms2),[])] end
 	   end;
 
     in NominalData.put (fold Symtab.update (map (rpair ()) full_ak_names)