--- a/Nominal/ExCoreHaskell.thy	Sat Mar 27 14:55:07 2010 +0100
+++ b/Nominal/ExCoreHaskell.thy	Sat Mar 27 16:17:45 2010 +0100
@@ -11,6 +11,7 @@
 
 (* there are types, coercion types and regular types list-data-structure *)
 
+ML {* val _ = alpha_type := AlphaGen *}
 nominal_datatype tkind =
   KStar
 | KFun "tkind" "tkind"
@@ -18,18 +19,18 @@
   CKEq "ty" "ty"
 and ty =
   TVar "tvar"
-| TC "char"
+| TC "string"
 | TApp "ty" "ty"
-| TFun "char" "ty_lst"
+| TFun "string" "ty_lst"
 | TAll tv::"tvar" "tkind" T::"ty"  bind tv in T
 | TEq "ty" "ty" "ty"
 and ty_lst =
   TsNil
 | TsCons "ty" "ty_lst"
 and co =
-  CC "char"
+  CC "string"
 | CApp "co" "co"
-| CFun "char" "co_lst"
+| CFun "string" "co_lst"
 | CAll tv::"tvar" "ckind" C::"co"  bind tv in C
 | CEq "co" "co" "co"
 | CSym "co"
@@ -45,7 +46,7 @@
 | CsCons "co" "co_lst"
 and trm =
   Var "var"
-| C "char"
+| C "string"
 | LAMT tv::"tvar" "tkind" t::"trm" bind tv in t
 | LAMC tv::"tvar" "ckind" t::"trm" bind tv in t
 | APP "trm" "ty"
@@ -58,7 +59,7 @@
   ANil
 | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t
 and pat =
-  K "char" "tvtk_lst" "tvck_lst" "vt_lst"
+  K "string" "tvtk_lst" "tvck_lst" "vt_lst"
 and vt_lst =
   VTNil
 | VTCons "var" "ty" "vt_lst"
@@ -140,7 +141,18 @@
  apply (simp_all add: rsp_pre)
  done
 
-lemmas permute_bv[simp] = permute_bv_raw.simps[quot_lifted]
+thm permute_bv_raw.simps[no_vars]
+ permute_bv_vt_raw.simps[quot_lifted]
+ permute_bv_tvck_raw.simps[quot_lifted]
+ permute_bv_tvtk_raw.simps[quot_lifted]
+
+lemma permute_bv_pre:
+  "permute_bv p (K c l1 l2 l3) =
+   K c (permute_bv_tvtk p l1) (permute_bv_tvck p l2) (permute_bv_vt p l3)"
+  by (lifting permute_bv_raw.simps)
+
+lemmas permute_bv[simp] =
+ permute_bv_pre
  permute_bv_vt_raw.simps[quot_lifted]
  permute_bv_tvck_raw.simps[quot_lifted]
  permute_bv_tvtk_raw.simps[quot_lifted]
@@ -317,17 +329,17 @@
   and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)"
   and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)"
   and a04: "\<And>tvar b. P3 b (TVar tvar)"
-  and a05: "\<And>char b. P3 b (TC char)"
+  and a05: "\<And>string b. P3 b (TC string)"
   and a06: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P3 b (TApp ty1 ty2)"
-  and a07: "\<And>char ty_lst b. \<lbrakk>\<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P3 b (TFun char ty_lst)"
+  and a07: "\<And>string ty_lst b. \<lbrakk>\<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P3 b (TFun string ty_lst)"
   and a08: "\<And>tvar tkind ty b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P3 c ty; atom tvar \<sharp> b\<rbrakk>
     \<Longrightarrow> P3 b (TAll tvar tkind ty)"
   and a09: "\<And>ty1 ty2 ty3 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2; \<And>c. P3 c ty3\<rbrakk> \<Longrightarrow> P3 b (TEq ty1 ty2 ty3)"
   and a10: "\<And>b. P4 b TsNil"
   and a11: "\<And>ty ty_lst b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P4 b (TsCons ty ty_lst)"
-  and a12: "\<And>char b. P5 b (CC char)"
+  and a12: "\<And>string b. P5 b (CC string)"
   and a13: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CApp co1 co2)"
-  and a14: "\<And>char co_lst b. \<lbrakk>\<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P5 b (CFun char co_lst)"
+  and a14: "\<And>string co_lst b. \<lbrakk>\<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P5 b (CFun string co_lst)"
   and a15: "\<And>tvar ckind co b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P5 c co; atom tvar \<sharp> b\<rbrakk>
     \<Longrightarrow> P5 b (CAll tvar ckind co)"
   and a16: "\<And>co1 co2 co3 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2; \<And>c. P5 c co3\<rbrakk> \<Longrightarrow> P5 b (CEq co1 co2 co3)"
@@ -342,7 +354,7 @@
   and a25: "\<And>b. P6 b CsNil"
   and a26: "\<And>co co_lst b. \<lbrakk>\<And>c. P5 c co; \<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P6 b (CsCons co co_lst)"
   and a27: "\<And>var b. P7 b (Var var)"
-  and a28: "\<And>char b. P7 b (C char)"
+  and a28: "\<And>string b. P7 b (C string)"
   and a29: "\<And>tvar tkind trm b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>
     \<Longrightarrow> P7 b (LAMT tvar tkind trm)"
   and a30: "\<And>tvar ckind trm b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>
@@ -357,8 +369,8 @@
   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>
     \<Longrightarrow> P8 b (ACons pat trm assoc_lst)"
-  and a39: "\<And>char 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 char tvtk_lst tvck_lst vt_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)"
   and a40: "\<And>b. P10 b VTNil"
   and a41: "\<And>var ty vt_lst b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P10 c vt_lst\<rbrakk> \<Longrightarrow> P10 b (VTCons var ty vt_lst)"
   and a42: "\<And>b. P11 b TVTKNil"