--- a/Nominal/Ex/Foo1.thy	Sat Nov 27 23:00:16 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Sun Nov 28 16:37:34 2010 +0000
@@ -154,11 +154,11 @@
   fixes c::"'a::fs"
   assumes "\<exists>name. y = Var name \<Longrightarrow> P" 
   and     "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
-  and     "\<exists>name trm. {atom name} \<sharp>* c \<and> y = Lam name trm \<Longrightarrow> P" 
-  and     "\<exists>assn trm. set (bn1 assn) \<sharp>* c \<and> y = Let1 assn trm \<Longrightarrow> P"
-  and     "\<exists>assn trm. set (bn2 assn) \<sharp>* c \<and> y = Let2 assn trm \<Longrightarrow> P"
-  and     "\<exists>assn trm. set (bn3 assn) \<sharp>* c \<and> y = Let3 assn trm \<Longrightarrow> P"
-  and     "\<exists>assn' trm. (bn4 assn') \<sharp>* c \<and> y = Let4 assn' trm \<Longrightarrow> P"
+  and     "\<exists>name trm.  {atom name} \<sharp>* c \<and> y = Lam name trm \<Longrightarrow> P" 
+  and     "\<exists>(c::'a::fs) assn trm. set (bn1 assn) \<sharp>* c \<and> y = Let1 assn trm \<Longrightarrow> P"
+  and     "\<exists>(c::'a::fs) assn trm. set (bn2 assn) \<sharp>* c \<and> y = Let2 assn trm \<Longrightarrow> P"
+  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))
@@ -168,6 +168,115 @@
 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)
+
+
+lemma strong_exhaust2:
+  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>assn trm. \<lbrakk>set (bn1 assn) \<sharp>* c; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P"
+  and     "\<And>assn trm. \<lbrakk>set (bn2 assn) \<sharp>* c; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P"
+  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)

--- a/Nominal/Ex/Foo2.thy	Sat Nov 27 23:00:16 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Sun Nov 28 16:37:34 2010 +0000
@@ -61,284 +61,23 @@
 apply(simp add: atom_eqvt)
 done
 
-
-lemma Let1_rename:
-  assumes "supp ([bn assn1]lst. trm1) \<sharp>* p" "supp ([bn assn2]lst. trm2) \<sharp>* p"
-  shows "Let1 assn1 trm1 assn2 trm2 = Let1 (permute_bn p assn1) (p \<bullet> trm1) (permute_bn p assn2) (p \<bullet> trm2)"
-using assms
-apply -
-apply(drule supp_perm_eq[symmetric])
-apply(drule supp_perm_eq[symmetric])
-apply(simp only: permute_Abs)
-apply(simp only: tt1)
-apply(simp only: foo.eq_iff)
-apply(simp add: uu1)
-done
-
-lemma Let2_rename:
-  assumes "(supp ([[atom x, atom y]]lst. t1)) \<sharp>* p" and "(supp ([[atom y]]lst. t2)) \<sharp>* p"
-  shows "Let2 x y t1 t2 = Let2 (p \<bullet> x) (p \<bullet> y) (p \<bullet> t1) (p \<bullet> t2)"
-  using assms
-  apply -
-  apply(drule supp_perm_eq[symmetric])
-  apply(drule supp_perm_eq[symmetric])
-  apply(simp only: foo.eq_iff)
-  apply(simp only: eqvts)
-  apply simp
-  done
-
-lemma Let2_rename2:
-  assumes "(supp ([[atom x, atom y]]lst. t1)) \<sharp>* p" and "(atom y) \<sharp> p"
-  shows "Let2 x y t1 t2 = Let2 (p \<bullet> x) y (p \<bullet> t1) t2"
-  using assms
-  apply -
-  apply(drule supp_perm_eq[symmetric])
-  apply(simp only: foo.eq_iff)
-  apply(simp only: eqvts)
-  apply simp
-  by (metis assms(2) atom_eqvt fresh_perm)
-
-lemma Let2_rename3:
-  assumes "(supp ([[atom x, atom y]]lst. t1)) \<sharp>* p"
-  and "(supp ([[atom y]]lst. t2)) \<sharp>* p"
-  and "(atom x) \<sharp> p"
-  shows "Let2 x y t1 t2 = Let2 x (p \<bullet> y) (p \<bullet> t1) (p \<bullet> t2)"
-  using assms
-  apply -
-  apply(drule supp_perm_eq[symmetric])
-  apply(drule supp_perm_eq[symmetric])
-  apply(simp only: foo.eq_iff)
-  apply(simp only: eqvts)
-  apply simp
-  by (metis assms(2) atom_eqvt fresh_perm)
-
-lemma strong_exhaust1_pre:
-  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>assn1 trm1 assn2 trm2. 
-    \<lbrakk>((set (bn assn1)) \<union> (set (bn assn2))) \<sharp>* c; y = Let1 assn1 trm1 assn2 trm2\<rbrakk> \<Longrightarrow> P"
-  and     "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<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(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assg1))) \<sharp>* c \<and> supp ([bn assg1]lst. trm1) \<sharp>* q")
-apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assg2))) \<sharp>* c \<and> supp ([bn assg2]lst. trm2) \<sharp>* q")
-apply(erule exE)+
-apply(erule conjE)+
-apply(rule assms(4))
-apply(simp add: set_eqvt union_eqvt)
-apply(simp add: tt1)
-apply(simp add: fresh_star_union)
-apply(rule conjI)
-apply(assumption)
-apply(rotate_tac 3)
-apply(assumption)
-apply(simp add: foo.eq_iff)
-apply(drule supp_perm_eq[symmetric])+
-apply(simp add: tt1 uu1)
-apply(auto)[1]
-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(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(case_tac "name1 = name2")
-apply(subgoal_tac 
-  "\<exists>q. (q \<bullet> {atom name1, atom name2}) \<sharp>* c \<and> (supp (([[atom name1, atom name2]]lst. trm1), ([[atom name2]]lst. trm2))) \<sharp>* q")
-apply(erule exE)+
-apply(erule conjE)+
-apply(perm_simp)
-apply(rule assms(5))
-
-apply (simp add: fresh_star_def eqvts)
-apply (simp only: supp_Pair)
-apply (simp only: fresh_star_Un_elim)
-apply (subst Let2_rename)
-apply assumption
-apply assumption
-apply (rule refl)
-apply(rule at_set_avoiding2)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply clarify
-apply (simp add: fresh_star_def)
-apply (simp add: fresh_def supp_Pair supp_Abs)
-apply(subgoal_tac
-  "\<exists>q. (q \<bullet> {atom name1}) \<sharp>* c \<and> (supp ((([[atom name1, atom name2]]lst. trm1)), (atom name2))) \<sharp>* q")
-prefer 2
-apply(rule at_set_avoiding2)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply (simp add: fresh_star_def)
-apply (simp add: fresh_def supp_Pair supp_Abs supp_atom)
-apply(erule exE)+
-apply(erule conjE)+
-apply(perm_simp)
-apply(rule assms(5))
-apply assumption
-apply clarify
-apply (rule_tac x="name1" and y="name2" and ?t1.0="trm1" and ?t2.0="trm2" in Let2_rename2)
-apply (simp_all add: fresh_star_Un_elim supp_Pair supp_Abs)
-apply (simp add: fresh_star_def supp_atom)
-done
-
-lemma strong_exhaust1:
-  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>assn1 trm1 assn2 trm2. 
-    \<lbrakk>((set (bn assn1)) \<union> (set (bn assn2))) \<sharp>* c; y = Let1 assn1 trm1 assn2 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 strong_exhaust1_pre)
-  apply (erule assms)
-  apply (erule assms)
-  apply (erule assms) apply assumption
-  apply (erule assms) apply assumption
-apply(case_tac "x1 = x2")
-apply(subgoal_tac 
-  "\<exists>q. (q \<bullet> {atom x1, atom x2}) \<sharp>* c \<and> (supp (([[atom x1, atom x2]]lst. trm1), ([[atom x2]]lst. trm2))) \<sharp>* q")
-apply(erule exE)+
-apply(erule conjE)+
-apply(perm_simp)
-apply(rule assms(5))
-apply assumption
-apply simp
-apply (rule Let2_rename)
-apply (simp only: supp_Pair)
-apply (simp only: fresh_star_Un_elim)
-apply (simp only: supp_Pair)
-apply (simp only: fresh_star_Un_elim)
-apply(rule at_set_avoiding2)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply clarify
-apply (simp add: fresh_star_def)
-apply (simp add: fresh_def supp_Pair supp_Abs)
-
-  apply(subgoal_tac 
-    "\<exists>q. (q \<bullet> {atom x2}) \<sharp>* c \<and> supp (([[atom x2]]lst. trm2), ([[atom x1, atom x2]]lst. trm1), (atom x1)) \<sharp>* q")
-  apply(erule exE)+
-  apply(erule conjE)+
-  apply(rule assms(5))
-apply(perm_simp)
-apply(simp (no_asm) add: fresh_star_insert)
-apply(rule conjI)
-apply (simp add: fresh_star_def)
-apply(rotate_tac 2)
-apply(simp add: fresh_star_def)
-apply(simp)
-apply (rule Let2_rename3)
-apply (simp add: supp_Pair fresh_star_union)
-apply (simp add: supp_Pair fresh_star_union)
-apply (simp add: supp_Pair fresh_star_union)
-apply clarify
-apply (simp add: fresh_star_def supp_atom)
-apply(rule at_set_avoiding2)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: fresh_star_def)
-apply (simp add: fresh_def supp_Pair supp_Abs supp_atom)
-done
-
-lemma strong_induct:
-  fixes c :: "'a :: fs"
-  and assg :: assg and trm :: trm
-  assumes a0: "\<And>name c. P1 c (Var name)"
-  and a1: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (App trm1 trm2)"
-  and a2: "\<And>name trm c. (\<And>d. P1 d trm) \<Longrightarrow> P1 c (Lam name trm)"
-  and a3: "\<And>assg1 trm1 assg2 trm2 c. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; \<And>d. P2 c assg1; \<And>d. P1 d trm1; \<And>d. P2 d assg2; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Let1 assg1 trm1 assg2 trm2)"
-  and a4: "\<And>name1 name2 trm1 trm2 c. \<lbrakk>{atom name1, atom name2} \<sharp>* c; \<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Let2 name1 name2 trm1 trm2)"
-  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 strong_exhaust1)
-apply(simp_all)[5]
-apply(rule_tac y="assg" in foo.exhaust(2))
-apply(simp_all)[2]
-apply(relation "measure (sum_case (size o snd) (\<lambda>y. size (snd y)))")
-apply(simp_all add: foo.size)
-done
-
-
 text {*
   tests by cu
 *}
 
 
-thm at_set_avoiding2 supp_perm_eq at_set_avoiding
-
-lemma abs_rename_set:
-  fixes x::"'a::fs"
-  assumes "b' \<sharp> x" "sort_of b = sort_of b'"
-  shows "\<exists>y. [{b}]set. x = [{b'}]set. y"
-apply(rule_tac x="(b \<rightleftharpoons> b') \<bullet> x" in exI)
-apply(subst Abs_swap1[where a="b" and b="b'"])
-apply(simp)
-using assms
-apply(simp add: fresh_def)
-apply(perm_simp)
-using assms
-apply(simp)
-done
-
-lemma abs_rename_set1:
-  fixes x::"'a::fs"
-  assumes "(p \<bullet> b) \<sharp> x" 
-  shows "\<exists>y. [{b}]set. x = [{p \<bullet> b}]set. y"
-apply(rule_tac x="(b \<rightleftharpoons> (p \<bullet> b)) \<bullet> x" in exI)
-apply(subst Abs_swap1[where a="b" and b="p \<bullet> b"])
-apply(simp)
-using assms
-apply(simp add: fresh_def)
-apply(perm_simp)
-apply(simp)
-done
-
 lemma yy:
-  assumes "finite bs"
-  and "bs \<inter> p \<bullet> bs = {}"
+  assumes a: "p \<bullet> bs \<inter> bs = {}" 
+  and     b: "finite bs"
   shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"
-using assms
+using b a
 apply(induct)
 apply(simp add: permute_set_eq)
 apply(rule_tac x="0" in exI)
 apply(simp add: supp_perm)
 apply(perm_simp)
 apply(drule meta_mp)
-apply(auto)[1]
+apply(auto simp add: fresh_star_def fresh_finite_insert)[1]
 apply(erule exE)
 apply(simp)
 apply(case_tac "q \<bullet> x = p \<bullet> x")
@@ -353,36 +92,35 @@
 apply(simp)
 apply(rule conjI)
 apply(simp add: supp_swap)
-defer
+apply(simp add: supp_perm)
+apply(auto)[1]
 apply(auto)[1]
 apply(erule conjE)+
 apply(drule sym)
-apply(auto)[1]
 apply(simp add: mem_permute_iff)
 apply(simp add: mem_permute_iff)
-apply(auto)[1]
-apply(simp add: supp_perm)
-apply(auto)[1]
 done
 
-lemma zz:
-  fixes bs::"atom list"
-  assumes "set bs \<inter> (set (p \<bullet> bs)) = {}"
-  shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (set (p \<bullet> bs))"
-sorry
+lemma yy1:
+  assumes "(p \<bullet> bs) \<sharp>* bs" "finite bs"
+  shows "p \<bullet> bs \<inter> bs = {}"
+using assms
+apply(auto simp add: fresh_star_def)
+apply(simp add: fresh_def supp_finite_atom_set)
+done
 
-lemma abs_rename_set2:
+lemma abs_rename_set:
   fixes x::"'a::fs"
-  assumes "(p \<bullet> bs) \<sharp>* x" "bs \<inter> p \<bullet> bs ={}" "finite bs"
+  assumes "(p \<bullet> bs) \<sharp>* x" "(p \<bullet> bs) \<sharp>* bs" "finite bs"
   shows "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y"
 using yy assms
 apply -
+apply(drule_tac x="p" in meta_spec)
 apply(drule_tac x="bs" in meta_spec)
-apply(drule_tac x="p" in meta_spec)
-apply(auto)
+apply(auto simp add: yy1)
 apply(rule_tac x="q \<bullet> x" in exI)
 apply(subgoal_tac "(q \<bullet> ([bs]set. x)) = [bs]set. x")
-apply(simp add: permute_Abs)
+apply(simp)
 apply(rule supp_perm_eq)
 apply(rule fresh_star_supp_conv)
 apply(simp add: fresh_star_def)
@@ -390,29 +128,73 @@
 apply(auto)
 done
 
+lemma zz0:
+  assumes "p \<bullet> bs = q \<bullet> bs"
+  and a: "a \<in> set bs"
+  shows "p \<bullet> a = q \<bullet> a"
+using assms
+by (induct bs) (auto)
+
+lemma zz:
+  fixes bs::"atom list"
+  assumes "set bs \<inter> (p \<bullet> (set bs)) = {}"
+  shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (p \<bullet> (set bs))"
+using assms
+apply(induct bs)
+apply(simp add: permute_set_eq)
+apply(rule_tac x="0" in exI)
+apply(simp add: supp_perm)
+apply(drule meta_mp)
+apply(perm_simp)
+apply(auto)[1]
+apply(erule exE)
+apply(simp)
+apply(case_tac "a \<in> set bs")
+apply(rule_tac x="q" in exI)
+apply(perm_simp)
+apply(auto dest: zz0)[1]
+apply(subgoal_tac "q \<bullet> a \<sharp> p \<bullet> bs")
+apply(subgoal_tac "p \<bullet> a \<sharp> p \<bullet> bs")
+apply(rule_tac x="((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q" in exI)
+apply(simp add: swap_fresh_fresh)
+apply(rule subset_trans)
+apply(rule supp_plus_perm)
+apply(simp)
+apply(rule conjI)
+apply(simp add: supp_swap)
+apply(simp add: supp_perm)
+apply(perm_simp)
+apply(auto simp add: fresh_def supp_of_atom_list)[1]
+apply(perm_simp)
+apply(auto)[1]
+apply(simp add: fresh_permute_iff)
+apply(simp add: fresh_def supp_of_atom_list)
+apply(erule conjE)+
+apply(drule sym)
+apply(drule sym)
+apply(simp)
+apply(simp add: fresh_permute_iff)
+apply(auto simp add: fresh_def supp_of_atom_list)[1]
+done
+
+lemma zz1:
+  assumes "(p \<bullet> (set bs)) \<sharp>* bs" 
+  shows "(set bs) \<inter> (p \<bullet> (set bs)) = {}"
+using assms
+apply(auto simp add: fresh_star_def)
+apply(simp add: fresh_def supp_of_atom_list)
+done
+
 lemma abs_rename_list:
   fixes x::"'a::fs"
-  assumes "b' \<sharp> x" "sort_of b = sort_of b'"
-  shows "\<exists>y. [[b]]lst. x = [[b']]lst. y"
-apply(rule_tac x="(b \<rightleftharpoons> b') \<bullet> x" in exI)
-apply(subst Abs_swap2[where a="b" and b="b'"])
-apply(simp)
-using assms
-apply(simp add: fresh_def)
-apply(perm_simp)
-using assms
-apply(simp)
-done
-
-lemma abs_rename_list2:
-  fixes x::"'a::fs"
-  assumes "(set (p \<bullet> bs)) \<sharp>* x" "(set bs) \<inter> (set (p \<bullet> bs)) ={}" 
+  assumes "(p \<bullet> (set bs)) \<sharp>* x" "(p \<bullet> (set bs)) \<sharp>* bs" 
   shows "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y"
 using zz assms
 apply -
 apply(drule_tac x="bs" in meta_spec)
 apply(drule_tac x="p" in meta_spec)
-apply(auto simp add: set_eqvt)
+apply(drule_tac zz1)
+apply(auto)
 apply(rule_tac x="q \<bullet> x" in exI)
 apply(subgoal_tac "(q \<bullet> ([bs]lst. x)) = [bs]lst. x")
 apply(simp)
@@ -423,72 +205,172 @@
 apply(auto)
 done
 
+lemma fresh_star_list:
+  shows "as \<sharp>* (xs @ ys) \<longleftrightarrow> as \<sharp>* xs \<and> as \<sharp>* ys"
+  and   "as \<sharp>* (x # xs) \<longleftrightarrow> as \<sharp>* x \<and> as \<sharp>* xs"
+  and   "as \<sharp>* []"
+by (auto simp add: fresh_star_def fresh_Nil fresh_Cons fresh_append)
 
-lemma test3:
+
+lemma test6:
   fixes c::"'a::fs"
-  assumes a: "y = Let2 x1 x2 trm1 trm2"
-  and b: "\<forall>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<longrightarrow> P"
+  assumes "\<exists>name. y = Var name \<Longrightarrow> P" 
+  and     "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
+  and     "\<exists>name trm. {atom name} \<sharp>* c \<and> y = Lam name trm \<Longrightarrow> P" 
+  and     "\<exists>a1 trm1 a2 trm2.  ((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c \<and> y = Let1 a1 trm1 a2 trm2 \<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"
-using b[simplified a]
-apply -
-apply(subgoal_tac "\<exists>q::perm. (q \<bullet> {atom x1, atom x2}) \<sharp>* (c, x1, x2, trm1, trm2)")
+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(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, [atom name], trm)")
 apply(erule exE)
+apply(rule assms(3))
+apply(insert abs_rename_list)[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_prod set.simps)
+apply(drule meta_mp)
+apply(rule TrueI)
+apply(drule meta_mp)
+apply(rule TrueI)
+apply(erule exE)
+apply(rule exI)+
 apply(perm_simp)
-apply(simp only: foo.eq_iff)
-apply(drule_tac x="q \<bullet> x1" in spec)
-apply(drule_tac x="q \<bullet> x2" in spec)
-apply(simp)
-apply(erule mp)
+apply(erule conjE)+
 apply(rule conjI)
-apply(simp add: fresh_star_prod)
+apply(assumption)
+apply(simp add: foo.eq_iff)
+defer
+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(rule assms(4))
+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="bn assg1" 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="bn assg2" in meta_spec)
+apply(drule_tac x="trm2" in meta_spec)
+apply(drule meta_mp)
+apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union)
+apply(drule meta_mp)
+apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union)
+apply(drule meta_mp)
+apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union)
+apply(drule meta_mp)
+apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union)
+apply(erule exE)+
+apply(rule exI)+
+apply(perm_simp add: tt1)
+apply(rule conjI)
+apply(simp add: fresh_star_prod fresh_star_union)
+apply(erule conjE)+
+apply(rule conjI)
+apply(assumption)
+apply(rotate_tac 4)
+apply(assumption)
+apply(rule conjI)
+apply(assumption)
 apply(rule conjI)
-apply(simp add: atom_eqvt[symmetric])
-apply(subst (2) permute_list.simps(1)[where p="q", symmetric])
-apply(subst permute_list.simps(2)[symmetric])
-apply(subst permute_list.simps(2)[symmetric])
-apply(rule abs_rename_list2)
-apply(simp add: atom_eqvt fresh_star_prod)
-apply(simp add: atom_eqvt fresh_star_prod fresh_star_def fresh_Pair fresh_def supp_Pair supp_at_base)
-apply(simp add: atom_eqvt[symmetric])
-apply(subst (2) permute_list.simps(1)[where p="q", symmetric])
-apply(subst permute_list.simps(2)[symmetric])
-apply(rule abs_rename_list2)
-apply(simp add: atom_eqvt fresh_star_prod)
-apply(simp add: atom_eqvt fresh_star_prod fresh_star_def fresh_Pair fresh_def supp_Pair supp_at_base)
-apply(simp add: atom_eqvt[symmetric])
-apply(simp add: atom_eqvt fresh_star_prod fresh_star_def fresh_Pair fresh_def supp_Pair supp_at_base)
+apply(rule uu1)
+apply(rule conjI)
+apply(assumption)
+apply(rule uu1)
+defer
+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_prod set.simps set_append fresh_star_union, simp)
+apply(drule meta_mp)
+apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union)
+apply(drule meta_mp)
+apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union set_append fresh_star_list, simp)
+apply(drule meta_mp)
+apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union set_append fresh_star_list, simp)
+apply(erule exE)+
+apply(rule exI)+
+apply(perm_simp add: tt1)
+apply(rule conjI)
+prefer 2
+apply(rule conjI)
+apply(assumption)
+apply(assumption)
+apply(simp add: fresh_star_prod)
+apply(simp add: fresh_star_def)
 sorry
 
-lemma test4:
-  fixes c::"'a::fs"
-  assumes a: "y = Let2 x1 x2 trm1 trm2"
-  and b: "\<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 test3)
-apply(rule a)
-using b
-apply(auto)
-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>assn1 trm1 assn2 trm2. 
-    \<lbrakk>((set (bn assn1)) \<union> (set (bn assn2))) \<sharp>* c; y = Let1 assn1 trm1 assn2 trm2\<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 foo.exhaust(1))
-apply (erule assms)
-apply (erule assms)
-prefer 3
-apply(erule test4[where c="c"])
-apply (rule assms(5)) 
-apply assumption
-apply(simp)
-oops
+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(erule exE)+
+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
+  assumes a0: "\<And>name c. P1 c (Var name)"
+  and a1: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (App trm1 trm2)"
+  and a2: "\<And>name trm c. (\<And>d. P1 d trm) \<Longrightarrow> P1 c (Lam name trm)"
+  and a3: "\<And>a1 t1 a2 t2 c. 
+    \<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)"
+  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(simp_all)[5]
+  apply(rule_tac y="assg" in foo.exhaust(2))
+  apply(simp_all)[2]
+  apply(relation "measure (sum_case (size o snd) (size o snd))")
+  apply(simp_all add: foo.size)
+  done
 
 end
 

--- a/Nominal/Nominal2_Base.thy	Sat Nov 27 23:00:16 2010 +0000
+++ b/Nominal/Nominal2_Base.thy	Sun Nov 28 16:37:34 2010 +0000
@@ -414,7 +414,6 @@
   shows "p \<bullet> (f x) = (p \<bullet> f) (p \<bullet> x)"
   unfolding permute_fun_def by simp
 
-
 subsection {* Permutations for booleans *}
 
 instantiation bool :: pt
@@ -483,6 +482,18 @@
   unfolding permute_fun_def permute_bool_def
   unfolding vimage_def Collect_def mem_def ..
 
+lemma permute_finite [simp]:
+  shows "finite (p \<bullet> X) = finite X"
+apply(simp add: permute_set_eq_image)
+apply(rule iffI)
+apply(drule finite_imageD)
+using inj_permute[where p="p"]
+apply(simp add: inj_on_def)
+apply(assumption)
+apply(rule finite_imageI)
+apply(assumption)
+done
+
 lemma swap_set_not_in:
   assumes a: "a \<notin> S" "b \<notin> S"
   shows "(a \<rightleftharpoons> b) \<bullet> S = S"
@@ -1162,6 +1173,12 @@
 apply (simp_all add: supp_Nil supp_Cons finite_supp)
 done
 
+lemma supp_of_atom_list:
+  fixes as::"atom list"
+  shows "supp as = set as"
+by (induct as)
+   (simp_all add: supp_Nil supp_Cons supp_atom)
+
 
 section {* Support and Freshness for Applications *}
 
@@ -1288,6 +1305,13 @@
   using fin
   by (simp add: supp_of_finite_sets)
 
+lemma fresh_finite_insert:
+  fixes S::"('a::fs) set"
+  assumes fin:  "finite S"
+  shows "a \<sharp> (insert x S) \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> S"
+  using fin unfolding fresh_def
+  by (simp add: supp_of_finite_insert)
+
 
 subsection {* Type @{typ "'a fset"} is finitely supported *}