diff -r 25dcb2b1329e -r 515e5496171c Nominal/Ex/Foo1.thy
--- a/Nominal/Ex/Foo1.thy	Mon Dec 06 14:24:17 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Mon Dec 06 16:35:42 2010 +0000
@@ -55,43 +55,6 @@
 thm foo.fresh
 thm foo.bn_finite
 
-lemma uu1:
-  shows "alpha_bn1 as (permute_bn1 p as)"
-apply(induct as rule: foo.inducts(2))
-apply(auto)[7]
-apply(simp add: foo.perm_bn_simps)
-apply(simp add: foo.eq_iff)
-apply(auto)
-done
-
-lemma uu2:
-  shows "alpha_bn2 as (permute_bn2 p as)"
-apply(induct as rule: foo.inducts(2))
-apply(auto)[7]
-apply(simp add: foo.perm_bn_simps)
-apply(simp add: foo.eq_iff)
-apply(auto)
-done
-
-lemma uu3:
-  shows "alpha_bn3 as (permute_bn3 p as)"
-apply(induct as rule: foo.inducts(2))
-apply(auto)[7]
-apply(simp add: foo.perm_bn_simps)
-apply(simp add: foo.eq_iff)
-apply(auto)
-done
-
-lemma uu4:
-  shows "alpha_bn4 as (permute_bn4 p as)"
-apply(induct as rule: foo.inducts(3))
-apply(auto)[8]
-apply(simp add: foo.perm_bn_simps)
-apply(simp add: foo.eq_iff)
-apply(simp add: foo.perm_bn_simps)
-apply(simp add: foo.eq_iff)
-done
-
 
 lemma tt1:
   shows "(p \<bullet> bn1 as) = bn1 (permute_bn1 p as)"
@@ -129,30 +92,6 @@
 apply(simp add: atom_eqvt insert_eqvt)
 done
 
-
-lemma Let1_rename:
-  assumes "supp ([bn1 assn]lst. trm) \<sharp>* p"
-  shows "Let1 assn trm = Let1 (permute_bn1 p assn) (p \<bullet> trm)"
-using assms
-apply -
-apply(drule supp_perm_eq[symmetric])
-apply(simp only: permute_Abs)
-apply(simp only: tt1)
-apply(simp only: foo.eq_iff)
-apply(rule conjI)
-apply(rule refl)
-apply(rule uu1)
-done
-
-lemma Let1_rename_a:
-  fixes c::"'a::fs"
-  assumes "y =  Let1 assn trm"
-  shows "\<exists>p. (p \<bullet> (set (bn1 assn))) \<sharp>* c \<and> y = Let1 (permute_bn1 p assn) (p \<bullet> trm)"
-using assms
-apply(simp only: foo.eq_iff uu1 tt1[symmetric] permute_Abs[symmetric])
-apply(simp del: permute_Abs)
-sorry
-
 lemma strong_exhaust1:
   fixes c::"'a::fs"
   assumes "\<exists>name. y = Var name \<Longrightarrow> P" 
@@ -163,60 +102,7 @@
   and     "\<exists>(c::'a::fs) assn trm. set (bn3 assn) \<sharp>* c \<and> y = Let3 assn trm \<Longrightarrow> P"
   and     "\<exists>(c::'a::fs) assn' trm. (bn4 assn') \<sharp>* c \<and> y = Let4 assn' trm \<Longrightarrow> P"
   shows "P"
-apply(rule_tac y="y" in foo.exhaust(1))
-apply(rule assms(1))
-apply(rule exI)
-apply(assumption)
-apply(rule assms(2))
-apply(rule exI)+
-apply(assumption)
-apply(rule assms(3))
-apply(subgoal_tac "\<exists>p::perm. (p \<bullet> {atom name}) \<sharp>* (c, name, trm)")
-apply(erule exE)
-apply(perm_simp)
-apply(rule_tac exI)+
-apply(rule conjI)
-apply(simp add: fresh_star_prod)
-apply(erule conjE)+
-apply(assumption)
-apply(simp)
-apply(simp add: foo.eq_iff)
-(* HERE *)
-defer
-defer
-apply(rule assms(4))
-apply(subgoal_tac "\<exists>p::perm. (p \<bullet> (set (bn1 assg))) \<sharp>* (c, assg, trm)")
-apply(erule exE)
-apply(perm_simp add: tt1)
-apply(simp only: fresh_star_prod)
-apply(erule conjE)+
-apply(rule_tac exI)+
-apply(rule conjI)
-apply(assumption)
-apply(simp add: foo.eq_iff)
-apply(rule conjI)
-apply(simp only: tt1[symmetric])
-defer
-apply(rule uu1)
-defer
-apply(rule assms(5))
-apply(subgoal_tac "\<exists>p::perm. (p \<bullet> (set (bn2 assg))) \<sharp>* (c, assg, trm)")
-apply(erule exE)
-apply(perm_simp add: tt2)
-apply(simp only: fresh_star_prod)
-apply(erule conjE)+
-apply(rule_tac exI)+
-apply(rule conjI)
-apply(assumption)
-apply(simp add: foo.eq_iff)
-apply(rule conjI)
-apply(simp only: tt2[symmetric])
-defer
-apply(rule uu2)
-defer
-apply(rule refl)
-apply(subst (asm) fresh_star_supp_conv)
-apply(simp)
+oops
 
 
 lemma strong_exhaust2:
@@ -229,89 +115,7 @@
   and     "\<And>assn trm. \<lbrakk>set (bn3 assn) \<sharp>* c; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P"
   and     "\<And>assn' trm. \<lbrakk>(bn4 assn') \<sharp>* c; y = Let4 assn' trm\<rbrakk> \<Longrightarrow> P"
   shows "P"
-apply(rule strong_exhaust1[where y="y"])
-apply(erule exE)+
-apply(rule assms(1))
-apply(assumption)
-apply(erule exE)+
-apply(rule assms(2))
-apply(assumption)
-apply(erule exE | erule conjE)?
-apply(rule assms(3))
-apply(drule_tac x="c" in spec)
-apply(erule exE | erule conjE)+
-apply(assumption)+
-apply(drule_tac x="c" in spec)
-apply(erule exE | erule conjE)+
-apply(assumption)+
-apply(erule exE | erule conjE)+
-apply(rule assms(4))
-apply(assumption)+
-apply(erule exE | erule conjE)+
-apply(rule assms(5))
-apply(assumption)+
-apply(erule exE | erule conjE)+
-apply(rule assms(6))
-apply(assumption)+
-apply(erule exE | erule conjE)+
-apply(rule assms(7))
-apply(assumption)+
-done
-
-
-
-
-
-
-
-
-
-
-
-
-apply(rule_tac y="y" in foo.exhaust(1))
-apply(rule assms(1))
-apply(rule exI)
-apply(assumption)
-apply(rule assms(2))
-apply(rule exI)+
-apply(assumption)
-apply(rule assms(3))
-apply(rule_tac p="p" in permute_boolE)
-apply(perm_simp)
-apply(simp)
-apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q")
-apply(erule exE)
-apply(erule conjE)
-apply(rule assms(3))
-apply(perm_simp)
-apply(assumption)
-apply(simp)
-apply(drule supp_perm_eq[symmetric])
-apply(perm_simp)
-apply(simp)
-apply(rule at_set_avoiding2)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: foo.fresh fresh_star_def)
-apply(drule Let1_rename_a)
-apply(erule exE)
-apply(erule conjE)
-apply(rule assms(4))
-apply(simp only: set_eqvt tt1)
-apply(assumption)
-(*
-apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn2 assg))) \<sharp>* c \<and> supp ([bn2 assg]lst.trm) \<sharp>* q")
-apply(erule exE)
-apply(erule conjE)
-*)
-thm assms(5)
-apply(rule assms(5))
-prefer 2
-apply(clarify)
-unfolding foo.eq_iff
-apply
+oops
 
 lemma strong_exhaust1:
   fixes c::"'a::fs"
@@ -323,95 +127,7 @@
   and     "\<And>assn trm. \<lbrakk>set (bn3 assn) \<sharp>* c; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P"
   and     "\<And>assn' trm. \<lbrakk>(bn4 assn') \<sharp>* c; y = Let4 assn' trm\<rbrakk> \<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)
-apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q")
-apply(erule exE)
-apply(erule conjE)
-apply(rule assms(3))
-apply(perm_simp)
-apply(assumption)
-apply(simp)
-apply(drule supp_perm_eq[symmetric])
-apply(perm_simp)
-apply(simp)
-apply(rule at_set_avoiding2)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: foo.fresh fresh_star_def)
-apply(drule Let1_rename_a)
-apply(erule exE)
-apply(erule conjE)
-apply(rule assms(4))
-apply(simp only: set_eqvt tt1)
-apply(assumption)
-(*
-apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn2 assg))) \<sharp>* c \<and> supp ([bn2 assg]lst.trm) \<sharp>* q")
-apply(erule exE)
-apply(erule conjE)
-*)
-thm assms(5)
-apply(rule assms(5))
-prefer 2
-apply(clarify)
-unfolding foo.eq_iff
-apply(rule conjI)
-prefer 2
-apply(rule uu2)
-apply(simp only: tt2[symmetric])
-prefer 2
-apply(simp only: tt2[symmetric])
-
-apply(simp_all only:)[2]
-apply(simp add: set_eqvt)
-apply(simp add: tt2)
-apply(simp add: foo.eq_iff)
-apply(drule supp_perm_eq[symmetric])
-apply(simp)
-apply(simp add: tt2 uu2)
-apply(rule at_set_avoiding2)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: Abs_fresh_star)
-apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn3 assg))) \<sharp>* c \<and> supp ([bn3 assg]lst.trm) \<sharp>* q")
-apply(erule exE)
-apply(erule conjE)
-apply(rule assms(6))
-apply(simp add: set_eqvt)
-apply(simp add: tt3)
-apply(simp add: foo.eq_iff)
-apply(drule supp_perm_eq[symmetric])
-apply(simp)
-apply(simp add: tt3 uu3)
-apply(rule at_set_avoiding2)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: Abs_fresh_star)
-apply(subgoal_tac "\<exists>q. (q \<bullet> (bn4 assg')) \<sharp>* c \<and> supp ([bn4 assg']set.trm) \<sharp>* q")
-apply(erule exE)
-apply(erule conjE)
-apply(rule assms(7))
-apply(simp add: tt4)
-apply(simp add: foo.eq_iff)
-apply(drule supp_perm_eq[symmetric])
-apply(simp)
-apply(simp add: tt4 uu4)
-apply(rule at_set_avoiding2)
-apply(simp add: foo.bn_finite)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: Abs_fresh_star)
-done
-
-thm strong_exhaust1 foo.exhaust(1)
-
-
+oops 
 
 lemma strong_exhaust2:
   assumes "\<And>x y t. as = As x y t \<Longrightarrow> P" 
@@ -448,6 +164,8 @@
   and     a9: "\<And>c. P3 c (BNil)"
   and     a10: "\<And>c a as. \<And>d. P3 d as \<Longrightarrow> P3 c (BAs a as)"
   shows "P1 c t" "P2 c as" "P3 c as'"
+oops
+(*
 using assms
 apply(induction_schema)
 apply(rule_tac y="t" and c="c" in strong_exhaust1)
@@ -459,6 +177,7 @@
 apply(relation "measure (sum_case (size o snd) (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z))))")
 apply(simp_all add: foo.size)
 done
+*)
 
 end