--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Foo2.thy	Sun Nov 21 02:17:19 2010 +0000
@@ -0,0 +1,158 @@
+theory Foo2
+imports "../Nominal2" 
+begin
+
+(* 
+  Contrived example that has more than one
+  binding clause
+*)
+
+atom_decl name
+
+nominal_datatype foo: trm =
+  Var "name"
+| App "trm" "trm"
+| Lam x::"name" t::"trm"  bind x in t
+| Let1 a1::"assg" t1::"trm" a2::"assg" t2::"trm" bind "bn a1" in t1, bind "bn a2" in t2
+| Let2 x::"name" y::"name" t1::"trm" t2::"trm" bind x y in t1, bind y in t2
+and assg =
+  As_Nil
+| As "name" x::"name" t::"trm" "assg" 
+binder
+  bn::"assg \<Rightarrow> atom list"
+where
+ "bn (As x y t a) = [atom x] @ bn a"
+| "bn (As_Nil) = []"
+
+thm foo.perm_bn_simps
+
+
+thm foo.distinct
+thm foo.induct
+thm foo.inducts
+thm foo.exhaust
+thm foo.fv_defs
+thm foo.bn_defs
+thm foo.perm_simps
+thm foo.eq_iff
+thm foo.fv_bn_eqvt
+thm foo.size_eqvt
+thm foo.supports
+thm foo.fsupp
+thm foo.supp
+thm foo.fresh
+
+lemma uu1:
+  shows "alpha_bn as (permute_bn p as)"
+apply(induct as rule: foo.inducts(2))
+apply(auto)[5]
+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> bn as) = bn (permute_bn p as)"
+apply(induct as rule: foo.inducts(2))
+apply(auto)[5]
+apply(simp add: foo.perm_bn_simps foo.bn_defs)
+apply(simp add: foo.perm_bn_simps foo.bn_defs)
+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 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_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)
+thm foo.eq_iff
+apply(subgoal_tac 
+  "\<exists>q. (q \<bullet> {atom name1}) \<sharp>* c \<and> supp ([[atom name1]]lst. trm1) \<sharp>* q")
+apply(subgoal_tac 
+  "\<exists>q. (q \<bullet> {atom name2}) \<sharp>* c \<and> supp ([[atom name2]]lst. trm2) \<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 3)
+apply(simp add: fresh_star_def)
+apply(simp)
+apply(simp add: foo.eq_iff)
+apply(drule supp_perm_eq[symmetric])+
+apply(simp add: atom_eqvt)
+apply(rule conjI)
+oops
+
+
+end
+
+
+