# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1268901091 -3600
# Node ID 21dda372fb1115c54359a5bb609592a77b569153
# Parent  2ff84b1f551f047e64000ac9569acd0a260802ee
simplified strong induction proof by using flip

diff -r 2ff84b1f551f -r 21dda372fb11 Nominal/Nominal2_Atoms.thy
--- a/Nominal/Nominal2_Atoms.thy	Thu Mar 18 08:32:55 2010 +0100
+++ b/Nominal/Nominal2_Atoms.thy	Thu Mar 18 09:31:31 2010 +0100
@@ -137,6 +137,12 @@
   and   "(a \<leftrightarrow> b) \<bullet> b = a"
   unfolding permute_flip_at by simp_all
 
+lemma flip_fresh_fresh:
+  fixes a b::"'a::at_base"
+  assumes "atom a \<sharp> x" "atom b \<sharp> x"
+  shows "(a \<leftrightarrow> b) \<bullet> x = x"
+using assms
+by (simp add: flip_def swap_fresh_fresh)
 
 subsection {* Syntax for coercing at-elements to the atom-type *}
 
diff -r 2ff84b1f551f -r 21dda372fb11 Nominal/Test.thy
--- a/Nominal/Test.thy	Thu Mar 18 08:32:55 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 18 09:31:31 2010 +0100
@@ -58,46 +58,42 @@
 
 lemmas supp_fn' = lm_fv[simplified supp_fn[symmetric]]
 
-lemma obtain_atom_ex:
-  assumes fin: "finite (supp x)"
-  shows "\<exists>a. a \<sharp> x \<and> sort_of a = s"
-using obtain_atom[OF fin]
-unfolding fresh_def
-by blast
-
 lemma
-  assumes a0: "finite (supp c)"
-  and     a1: "\<And>name c. P c (Vr name)"
-  and     a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
-  and     a3: "\<And>name lm c. \<lbrakk>\<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
+  fixes c::"'a::fs"
+  assumes a1: "\<And>name c. P c (Vr name)"
+  and     a2: "\<And>lm_raw1 lm_raw2 c. \<lbrakk>\<And>d. P d lm_raw1; \<And>d. P d lm_raw2\<rbrakk> \<Longrightarrow> P c (Ap lm_raw1 lm_raw2)"
+  and     a3: "\<And>name lm_raw c. \<lbrakk>\<And>d. P d lm_raw\<rbrakk> \<Longrightarrow> P c (Lm name lm_raw)"
   shows "P c lm"
 proof -
-  have "\<And>p c. P c (p \<bullet> lm)"
-    apply(induct lm rule: lm_induct)
+  have "\<And>p. P c (p \<bullet> lm)"
+    apply(induct lm arbitrary: c rule: lm_induct)
     apply(simp only: lm_perm)
     apply(rule a1)
     apply(simp only: lm_perm)
     apply(rule a2)
-    apply(assumption)
+    apply(blast)[1]
     apply(assumption)
-    apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm)) 
-                          \<and> sort_of (atom new) = sort_of (atom name)")
+    apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm_raw))")
     apply(erule exE)
-    apply(rule_tac t="(p \<bullet> Lm name lm)" and 
-                   s="((((atom (p \<bullet> name)) \<rightleftharpoons> (atom new)) + p) \<bullet> Lm name lm)" in subst)
+    apply(rule_tac t="p \<bullet> Lm name lm_raw" and 
+                   s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm_raw" in subst)
     apply(simp)
     apply(subst lm_perm)
     apply(subst (2) lm_perm)
-    apply(rule swap_fresh_fresh)
+    apply(rule flip_fresh_fresh)
     apply(simp add: fresh_def)
     apply(simp only: supp_fn')
     apply(simp)
     apply(simp add: fresh_Pair)
     apply(simp add: lm_perm)
     apply(rule a3)
-    apply(drule_tac x="(atom (p \<bullet> name) \<rightleftharpoons> atom new) + p" in meta_spec)
+    apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec)
     apply(simp)
-    sorry (* use at_set_avoiding *)    
+    apply(simp add: fresh_def)
+    apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm_raw))" in obtain_at_base)
+    apply(simp add: supp_Pair finite_supp)
+    apply(blast)
+    done
   then have "P c (0 \<bullet> lm)" by blast
   then show "P c lm" by simp
 qed