--- a/Nominal/ExCoreHaskell.thy	Mon Mar 29 12:06:22 2010 +0200
+++ b/Nominal/ExCoreHaskell.thy	Mon Mar 29 16:29:50 2010 +0200
@@ -11,7 +11,7 @@
 
 (* there are types, coercion types and regular types list-data-structure *)
 
-ML {* val _ = alpha_type := AlphaGen *}
+ML {* val _ = alpha_type := AlphaLst *}
 nominal_datatype tkind =
   KStar
 | KFun "tkind" "tkind"
@@ -71,18 +71,18 @@
   TVCKNil
 | TVCKCons "tvar" "ckind" "tvck_lst"
 binder
-    bv :: "pat \<Rightarrow> atom set"
-and bv_vt :: "vt_lst \<Rightarrow> atom set"
-and bv_tvtk :: "tvtk_lst \<Rightarrow> atom set"
-and bv_tvck :: "tvck_lst \<Rightarrow> atom set"
+    bv :: "pat \<Rightarrow> atom list"
+and bv_vt :: "vt_lst \<Rightarrow> atom list"
+and bv_tvtk :: "tvtk_lst \<Rightarrow> atom list"
+and bv_tvck :: "tvck_lst \<Rightarrow> atom list"
 where
-  "bv (K s tvts tvcs vs) = (bv_tvtk tvts) \<union> (bv_tvck tvcs) \<union> (bv_vt vs)"
-| "bv_vt VTNil = {}"
-| "bv_vt (VTCons v k t) = {atom v} \<union> bv_vt t"
-| "bv_tvtk TVTKNil = {}"
-| "bv_tvtk (TVTKCons v k t) = {atom v} \<union> bv_tvtk t"
-| "bv_tvck TVCKNil = {}"
-| "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t"
+  "bv (K s tvts tvcs vs) = append (bv_tvtk tvts) (append (bv_tvck tvcs) (bv_vt vs))"
+| "bv_vt VTNil = []"
+| "bv_vt (VTCons v k t) = (atom v) # bv_vt t"
+| "bv_tvtk TVTKNil = []"
+| "bv_tvtk (TVTKCons v k t) = (atom v) # bv_tvtk t"
+| "bv_tvck TVCKNil = []"
+| "bv_tvck (TVCKCons v k t) = (atom v) # bv_tvck t"
 
 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.supp(1-9,11,13,15)
 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified fv_supp]
@@ -201,7 +201,7 @@
   done
 
 lemma ACons_subst:
-  "supp (Abs (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (q \<bullet> trm) al"
+  "supp (Abs_lst (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (q \<bullet> trm) al"
   apply (simp only: eq_iff)
   apply (rule_tac x="q" in exI)
   apply (simp add: alphas)
@@ -295,36 +295,30 @@
 apply (simp add: fin1 fin2 fin3)
 done
 
-lemma finb1: "finite (bv_tvtk x)"
+lemma finb1: "finite (set (bv_tvtk x))"
 apply (induct x rule: inducts(11))
 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 apply (simp_all add: fv_supp finite_supp)
 done
 
-lemma finb2: "finite (bv_tvck x)"
+lemma finb2: "finite (set (bv_tvck x))"
 apply (induct x rule: inducts(12))
 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 apply (simp_all add: fv_supp finite_supp)
 done
 
-lemma finb3: "finite (bv_vt x)"
+lemma finb3: "finite (set (bv_vt x))"
 apply (induct x rule: inducts(10))
 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 apply (simp_all add: fv_supp finite_supp)
 done
 
-lemma fin_bv: "finite (bv x)"
+lemma fin_bv: "finite (set (bv x))"
 apply (induct x rule: inducts(9))
 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 apply (simp add: finb1 finb2 finb3)
 done
 
-lemma "bv x \<sharp>* fv_bv x"
-apply (induct x rule: inducts(9))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
-apply (simp)
-oops
-
 lemma strong_inudction_principle:
   assumes a01: "\<And>b. P1 b KStar"
   and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)"
@@ -368,7 +362,7 @@
   and a35: "\<And>trm assoc_lst b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P8 c assoc_lst\<rbrakk> \<Longrightarrow> P7 b (Case trm assoc_lst)"
   and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)"
   and a37: "\<And>b. P8 b ANil"
-  and a38: "\<And>pat trm assoc_lst b. \<lbrakk>\<And>c. P9 c pat; \<And>c. P7 c trm; \<And>c. P8 c assoc_lst; bv(pat) \<sharp>* b\<rbrakk>
+  and a38: "\<And>pat trm assoc_lst b. \<lbrakk>\<And>c. P9 c pat; \<And>c. P7 c trm; \<And>c. P8 c assoc_lst; set (bv (pat)) \<sharp>* b\<rbrakk>
     \<Longrightarrow> P8 b (ACons pat trm assoc_lst)"
   and a39: "\<And>string tvtk_lst tvck_lst vt_lst b. \<lbrakk>\<And>c. P11 c tvtk_lst; \<And>c. P12 c tvck_lst; \<And>c. P10 c vt_lst\<rbrakk>
     \<Longrightarrow> P9 b (K string tvtk_lst tvck_lst vt_lst)"
@@ -643,8 +637,8 @@
     apply blast
 
 (* MAIN ACons Goal *)
-    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (bv (p \<bullet> pat))) \<sharp>* h \<and>
-                       supp (Abs (p \<bullet> (bv pat)) (p \<bullet> trm)) \<sharp>* pa)")
+    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (set (bv (p \<bullet> pat)))) \<sharp>* h \<and>
+                       supp (Abs_lst (p \<bullet> (bv pat)) (p \<bullet> trm)) \<sharp>* pa)")
     apply clarify
     apply (simp only: perm eqvts)
     apply (subst ACons_subst)
@@ -661,7 +655,6 @@
     apply (simp add: fin_bv)
     apply (simp add: finite_supp)
     apply (simp add: supp_abs)
-    apply (rule finite_Diff)
     apply (simp add: finite_supp)
     apply (simp add: fresh_star_def fresh_def supp_abs eqvts)
     done