--- a/Nominal/Ex/Foo1.thy	Sun Nov 14 01:00:56 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Sun Nov 14 10:02:30 2010 +0000
@@ -2,10 +2,10 @@
 imports "../Nominal2" 
 begin
 
-(* 
+text {* 
   Contrived example that has more than one
-  binding function for a datatype
-*)
+  binding function
+*}
 
 atom_decl name
 
@@ -16,16 +16,24 @@
 | Let1 a::"assg" t::"trm"  bind "bn1 a" in t
 | Let2 a::"assg" t::"trm"  bind "bn2 a" in t
 | Let3 a::"assg" t::"trm"  bind "bn3 a" in t
+| Let4 a::"assg'" t::"trm"  bind (set) "bn4 a" in t
 and assg =
   As "name" "name" "trm"
+and assg' =
+  BNil
+| BAs "name" "assg'"
 binder
   bn1::"assg \<Rightarrow> atom list" and
   bn2::"assg \<Rightarrow> atom list" and
-  bn3::"assg \<Rightarrow> atom list"
+  bn3::"assg \<Rightarrow> atom list" and
+  bn4::"assg' \<Rightarrow> atom set"
 where
   "bn1 (As x y t) = [atom x]"
 | "bn2 (As x y t) = [atom y]"
 | "bn3 (As x y t) = [atom x, atom y]"
+| "bn4 (BNil) = {}"
+| "bn4 (BAs a as) = {atom a} \<union> bn4 as"
+
 
 thm foo.distinct
 thm foo.induct
@@ -42,57 +50,86 @@
 thm foo.supp
 thm foo.fresh
 
-
-lemmas permute_bn1 = permute_bn1_raw.simps[quot_lifted]
-lemmas permute_bn2 = permute_bn2_raw.simps[quot_lifted]
-lemmas permute_bn3 = permute_bn3_raw.simps[quot_lifted]
-
 lemma uu1:
   shows "alpha_bn1 as (permute_bn1 p as)"
 apply(induct as rule: foo.inducts(2))
-apply(auto)[6]
-apply(simp add: permute_bn1)
+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)[6]
-apply(simp add: permute_bn2)
+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)[6]
-apply(simp add: permute_bn3)
+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)"
 apply(induct as rule: foo.inducts(2))
-apply(auto)[6]
-apply(simp add: permute_bn1 foo.bn_defs)
+apply(auto)[7]
+apply(simp add: foo.perm_bn_simps foo.bn_defs)
 apply(simp add: atom_eqvt)
+apply(auto)
 done
 
 lemma tt2:
   shows "(p \<bullet> bn2 as) = bn2 (permute_bn2 p as)"
 apply(induct as rule: foo.inducts(2))
-apply(auto)[6]
-apply(simp add: permute_bn2 foo.bn_defs)
+apply(auto)[7]
+apply(simp add: foo.perm_bn_simps foo.bn_defs)
 apply(simp add: atom_eqvt)
+apply(auto)
 done
 
 lemma tt3:
   shows "(p \<bullet> bn3 as) = bn3 (permute_bn3 p as)"
 apply(induct as rule: foo.inducts(2))
-apply(auto)[6]
-apply(simp add: permute_bn3 foo.bn_defs)
+apply(auto)[7]
+apply(simp add: foo.perm_bn_simps foo.bn_defs)
 apply(simp add: atom_eqvt)
+apply(auto)
+done
+
+lemma tt4:
+  shows "(p \<bullet> bn4 as) = bn4 (permute_bn4 p as)"
+apply(induct as rule: foo.inducts(3))
+apply(auto)[8]
+apply(simp add: foo.perm_bn_simps foo.bn_defs permute_set_eq)
+apply(simp add: foo.perm_bn_simps foo.bn_defs)
+apply(simp add: atom_eqvt insert_eqvt)
+done
+
+lemma bn_finite:
+  shows "(\<lambda>x. True) t"
+  and  "finite (set (bn1 as)) \<and> finite (set (bn2 as)) \<and> finite (set (bn3 as))"
+  and  "finite (bn4 as')"
+apply(induct "t::trm" and as and as' rule: foo.inducts)
+apply(simp_all add: foo.bn_defs)
 done
 
 
@@ -104,6 +141,7 @@
   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_tac y="y" in foo.exhaust(1))
 apply(rule assms(1))
@@ -168,6 +206,20 @@
 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: bn_finite)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: Abs_fresh_star)
 done
 
 lemma strong_exhaust2:
@@ -178,10 +230,21 @@
 apply(assumption)
 done
 
+lemma strong_exhaust3:
+  assumes "as' = BNil \<Longrightarrow> P"
+  and "\<And>a as. as' = BAs a as \<Longrightarrow> P" 
+  shows "P"
+apply(rule_tac y="as'" in foo.exhaust(3))
+apply(rule assms(1))
+apply(assumption)
+apply(rule assms(2))
+apply(assumption)
+done
 
 lemma 
   fixes t::trm
   and   as::assg
+  and   as'::assg'
   and   c::"'a::fs"
   assumes a1: "\<And>x c. P1 c (Var x)"
   and     a2: "\<And>t1 t2 c. \<lbrakk>\<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (App t1 t2)"
@@ -189,15 +252,20 @@
   and     a4: "\<And>as t c. \<lbrakk>set (bn1 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let1 as t)"
   and     a5: "\<And>as t c. \<lbrakk>set (bn2 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let2 as t)"
   and     a6: "\<And>as t c. \<lbrakk>set (bn3 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let3 as t)"
-  and     a7: "\<And>x y t c. \<And>d. P1 d t \<Longrightarrow> P2 c (As x y t)"
-  shows "P1 c t" "P2 c as"
+  and     a7: "\<And>as' t c. \<lbrakk>(bn4 as') \<sharp>* c; \<And>d. P3 d as'; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let4 as' t)" 
+  and     a8: "\<And>x y t c. \<And>d. P1 d t \<Longrightarrow> P2 c (As x y t)"
+  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'"
 using assms
 apply(induction_schema)
 apply(rule_tac y="t" and c="c" in strong_exhaust1)
-apply(simp_all)[6]
+apply(simp_all)[7]
 apply(rule_tac as="as" in strong_exhaust2)
 apply(simp)
-apply(relation "measure (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z)))")
+apply(rule_tac as'="as'" in strong_exhaust3)
+apply(simp_all)[2]
+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