diff -r 478c5648e73f -r d1bdc281be2b Nominal/Ex/Foo2.thy
--- a/Nominal/Ex/Foo2.thy	Thu Dec 23 00:22:41 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Thu Dec 23 00:46:06 2010 +0000
@@ -24,10 +24,6 @@
   "bn (As x y t a) = [atom x] @ bn a"
 | "bn (As_Nil) = []"
 
-
-
-
-
 thm foo.bn_defs
 thm foo.permute_bn
 thm foo.perm_bn_alpha
@@ -39,6 +35,7 @@
 thm foo.induct
 thm foo.inducts
 thm foo.exhaust
+thm foo.strong_exhaust
 thm foo.fv_defs
 thm foo.bn_defs
 thm foo.perm_simps
@@ -50,308 +47,6 @@
 thm foo.supp
 thm foo.fresh
 
-lemma at_set_avoiding5:
-  assumes "finite xs"
-  and     "finite (supp c)"
-  shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp p = xs \<union> p \<bullet> xs"
-using assms
-apply(erule_tac c="c" in at_set_avoiding)
-apply(auto)
-done
-
-
-lemma Abs_rename_lst3:
-  fixes x::"'a::fs"
-  assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" 
-  shows "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> p \<bullet> bs = q \<bullet> bs"
-proof -
-  from a have "p \<bullet> (set bs) \<inter> (set bs) = {}" using at_fresh_star_inter 
-    by (simp add: fresh_star_Pair fresh_star_set)
-  with list_renaming_perm 
-  obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by metis 
-  have "[bs]lst. x =  q \<bullet> ([bs]lst. x)"
-    apply(rule perm_supp_eq[symmetric])
-    using a **
-    unfolding fresh_star_Pair
-    unfolding Abs_fresh_star_iff
-    unfolding fresh_star_def
-    by auto
-  also have "\<dots> = [q \<bullet> bs]lst. (q \<bullet> x)" by simp
-  also have "\<dots> = [p \<bullet> bs]lst. (q \<bullet> x)" using * by simp
-  finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" .
-  then show "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> p \<bullet> bs = q \<bullet> bs" 
-    using * ** by metis
-qed
-
-
-lemma
-  fixes c::"'a::fs"
-  assumes a:  "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P"
-  shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P"
-apply -
-apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and>
-  supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2))))")
-defer
-apply(rule at_set_avoiding5)
-apply(simp add: foo.bn_finite)
-apply(simp add: supp_Pair finite_supp)
-apply(erule exE)
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair)
-apply(erule conjE)+
-thm Abs_rename_lst
-apply(insert Abs_rename_lst)[1]
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="bn assg1" in meta_spec)
-apply(drule_tac x="trm1" in meta_spec)
-apply(insert Abs_rename_lst)[1]
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="bn assg2" in meta_spec)
-apply(drule_tac x="trm2" in meta_spec)
-apply(drule meta_mp)
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair fresh_star_Un)
-apply(drule meta_mp)
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair fresh_star_Un)
-apply(erule exE)+
-apply(rule a)
-apply(assumption)
-apply(simp only: foo.eq_iff)
-apply(perm_simp add: foo.permute_bn)
-apply(rule conjI)
-apply(rule refl)
-apply(rule conjI)
-apply(rule foo.perm_bn_alpha)
-apply(rule conjI)
-apply(perm_simp add: foo.permute_bn)
-apply(rule refl)
-apply(rule foo.perm_bn_alpha)
-done
-
-lemma
-  fixes c::"'a::fs"
-  assumes a:  "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P"
-  shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P"
-apply -
-apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and>
-  supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2))))")
-defer
-apply(rule at_set_avoiding5)
-apply(simp add: foo.bn_finite)
-apply(simp add: supp_Pair finite_supp)
-apply(erule exE)
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair)
-apply(erule conjE)+
-apply(insert Abs_rename_lst3)[1]
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="bn assg1" in meta_spec)
-apply(drule_tac x="trm1" in meta_spec)
-apply(insert Abs_rename_lst3)[1]
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="bn assg2" in meta_spec)
-apply(drule_tac x="trm2" in meta_spec)
-apply(drule meta_mp)
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair fresh_star_Un)
-apply(drule meta_mp)
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair fresh_star_Un)
-apply(erule exE)+
-apply(erule conjE)+
-apply(simp add: foo.permute_bn)
-apply(rule a)
-apply(assumption)
-apply(clarify)
-apply(simp (no_asm) only: foo.eq_iff)
-apply(rule conjI)
-apply(assumption)
-apply(rule conjI)
-apply(rule foo.perm_bn_alpha)
-apply(rule conjI)
-apply(assumption)
-apply(rule foo.perm_bn_alpha)
-done
-
-
-lemma
-  fixes c::"'a::fs"
-  assumes a:  "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P"
-  shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P"
-apply -
-apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and>
-  supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2))))")
-defer
-apply(rule at_set_avoiding5)
-apply(simp add: foo.bn_finite)
-apply(simp add: supp_Pair finite_supp)
-apply(erule exE)
-apply(simp add: fresh_star_Pair)
-apply(erule conjE)+
-apply(simp (no_asm_use) only: foo.permute_bn set_eqvt union_eqvt)
-apply(rule a)
-apply(assumption)
-apply(clarify)
-apply(simp (no_asm) only: foo.eq_iff)
-apply(rule conjI)
-apply(rule trans)
-apply(rule_tac p="p" in supp_perm_eq[symmetric])
-apply(rule fresh_star_supp_conv)
-apply(simp (no_asm_use) add: fresh_star_def)
-apply(simp (no_asm_use) add: Abs_fresh_iff)[1]
-apply(rule ballI)
-apply(auto simp add: fresh_Pair)[1]
-apply(simp (no_asm_use) only: permute_Abs)
-apply(simp (no_asm_use) only: multi_recs.fv_bn_eqvt)
-apply(simp)
-apply(rule at_set_avoiding5)
-apply(simp add: multi_recs.bn_finite)
-apply(simp add: supp_Pair finite_supp)
-apply(rule finite_sets_supp)
-apply(simp add: multi_recs.bn_finite)
-done
-
-
-
-lemma test6:
-  fixes c::"'a::fs"
-  assumes "\<And>name. y = Var name \<Longrightarrow> P" 
-  and     "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
-  and     "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" 
-  and     "\<And>a1 trm1 a2 trm2.  \<lbrakk>((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c; y = Let1 a1 trm1 a2 trm2\<rbrakk> \<Longrightarrow> P"
-  and     "\<exists>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<Longrightarrow> P"
-  shows "P"
-apply(rule_tac y="y" in foo.exhaust(1))
-apply(rule assms(1))
-apply(assumption)
-apply(rule assms(2))
-apply(assumption)
-(* lam case *)
-apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, name, trm)")
-apply(erule exE)
-apply(insert Abs_rename_lst)[1]
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="[atom name]" in meta_spec)
-apply(drule_tac x="trm" in meta_spec)
-apply(simp only: fresh_star_Pair set.simps)
-apply(drule meta_mp)
-apply(simp add: fresh_star_def fresh_Nil fresh_Cons fresh_atom_at_base)
-apply(erule exE)
-apply(rule assms(3))
-apply(perm_simp)
-apply(erule conjE)+
-apply(assumption)
-apply(clarify)
-apply(simp (no_asm) add: foo.eq_iff)
-apply(perm_simp)
-apply(assumption)
-apply(rule at_set_avoiding1)
-apply(simp)
-apply(simp add: finite_supp)
-(* let1 case *)
-apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)")
-apply(erule exE)
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair)
-apply(erule conjE)+
-apply(insert Abs_rename_lst)[1]
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="bn assg1" in meta_spec)
-apply(drule_tac x="trm1" in meta_spec)
-apply(insert Abs_rename_lst)[1]
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="bn assg2" in meta_spec)
-apply(drule_tac x="trm2" in meta_spec)
-apply(drule meta_mp)
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair fresh_star_Un)
-apply(drule meta_mp)
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair fresh_star_Un)
-apply(erule exE)+
-apply(rule assms(4))
-apply(assumption)
-apply(simp add: foo.eq_iff refl)
-apply(rule conjI)
-apply(perm_simp add: foo.permute_bn)
-apply(rule refl)
-apply(rule conjI)
-apply(rule foo.perm_bn_alpha)
-apply(rule conjI)
-apply(perm_simp add: foo.permute_bn)
-apply(rule refl)
-apply(rule foo.perm_bn_alpha)
-apply(rule at_set_avoiding1)
-apply(simp)
-apply(simp add: finite_supp)
-(* let2 case *)
-apply(subgoal_tac "\<exists>p. (p \<bullet> ({atom name1} \<union> {atom name2})) \<sharp>* (c, atom name1, atom name2, trm1, trm2)")
-apply(erule exE)
-apply(rule assms(5))
-apply(simp only:)
-apply(simp only: foo.eq_iff)
-apply(insert Abs_rename_list)[1]
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="[atom name1] @ [atom name2]" in meta_spec)
-apply(drule_tac x="trm1" in meta_spec)
-apply(insert Abs_rename_list)[1]
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="[atom name2]" in meta_spec)
-apply(drule_tac x="trm2" in meta_spec)
-apply(drule meta_mp)
-apply(simp only: union_eqvt fresh_star_Pair fresh_star_list fresh_star_Un, simp)
-apply(auto)[1]
-apply(perm_simp)
-apply(auto simp add: fresh_star_def)[1]
-apply(perm_simp)
-apply(auto simp add: fresh_star_def)[1]
-apply(perm_simp)
-apply(auto simp add: fresh_star_def)[1]
-apply(drule meta_mp)
-apply(perm_simp)
-apply(auto simp add: fresh_star_def fresh_Pair fresh_Nil fresh_Cons)[1]
-apply(erule exE)+
-apply(rule exI)+
-apply(perm_simp add: foo.permute_bn)
-apply(rule conjI)
-prefer 2
-apply(rule conjI)
-apply(assumption)
-apply(assumption)
-apply(simp add: fresh_star_Pair)
-apply(simp add: fresh_star_def)
-apply(rule at_set_avoiding1)
-apply(simp)
-apply(simp add: finite_supp)
-done
-
-lemma test5:
-  fixes c::"'a::fs"
-  assumes "\<And>name. y = Var name \<Longrightarrow> P" 
-  and     "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
-  and     "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" 
-  and     "\<And>a1 trm1 a2 trm2. \<lbrakk>((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c; y = Let1 a1 trm1 a2 trm2\<rbrakk> \<Longrightarrow> P"
-  and     "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1, atom x2} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P"
-  shows "P"
-apply(rule_tac y="y" in test6)
-apply(erule exE)+
-apply(rule assms(1))
-apply(assumption)
-apply(erule exE)+
-apply(rule assms(2))
-apply(assumption)
-apply(rule assms(3))
-apply(auto)[2]
-apply(erule exE)+
-apply(rule assms(4))
-apply(auto)[2]
-apply(erule exE)+
-apply(rule assms(5))
-apply(auto)[2]
-done
-
-
 lemma strong_induct:
   fixes c :: "'a :: fs"
   and assg :: assg and trm :: trm
@@ -362,15 +57,15 @@
     \<lbrakk>((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c; \<And>d. P2 c a1; \<And>d. P1 d t1; \<And>d. P2 d a2; \<And>d. P1 d t2\<rbrakk> 
     \<Longrightarrow> P1 c (Let1 a1 t1 a2 t2)"
   and a4: "\<And>n1 n2 t1 t2 c. 
-    \<lbrakk>{atom n1, atom n2} \<sharp>* c; \<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (Let2 n1 n2 t1 t2)"
+    \<lbrakk>({atom n1} \<union> {atom n2}) \<sharp>* c; \<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (Let2 n1 n2 t1 t2)"
   and a5: "\<And>c. P2 c As_Nil"
   and a6: "\<And>name1 name2 trm assg c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d assg\<rbrakk> \<Longrightarrow> P2 c (As name1 name2 trm assg)"
   shows "P1 c trm" "P2 c assg"
   using assms
   apply(induction_schema)
-  apply(rule_tac y="trm" and c="c" in test5)
+  apply(rule_tac y="trm" and c="c" in foo.strong_exhaust(1))
   apply(simp_all)[5]
-  apply(rule_tac y="assg" in foo.exhaust(2))
+  apply(rule_tac ya="assg" in foo.strong_exhaust(2))
   apply(simp_all)[2]
   apply(relation "measure (sum_case (size o snd) (size o snd))")
   apply(simp_all add: foo.size)