--- a/Nominal/ExCoreHaskell.thy	Mon Mar 29 17:32:17 2010 +0200
+++ b/Nominal/ExCoreHaskell.thy	Mon Mar 29 18:12:54 2010 +0200
@@ -323,7 +323,9 @@
 apply (simp add: finb1 finb2 finb3)
 done
 
-lemma strong_inudction_principle:
+thm tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.induct
+
+lemma strong_induction_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)"
   and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)"
@@ -333,32 +335,36 @@
   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 TvsNil"
-  and a11: "\<And>ty ty_lst b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P4 b (TvsCons ty ty_lst)"
-  and a12: "\<And>string b. P5 b (CC string)"
+  and a09: "\<And>ck ty b. \<lbrakk>\<And>c. P2 c ck; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P3 b (TEq ck ty)"
+  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>string b. P5 b (CVar string)"
+  and a12a:"\<And>str b. P5 b (CConst str)"
   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>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)"
-  and a17: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CSym co)"
+  and a16: "\<And>ck co b. \<lbrakk>\<And>c. P2 c ck; \<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CEq ck co)"
+  and a17: "\<And>ty b. \<lbrakk>\<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P5 b (CRefl ty)"
+  and a17a: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CSym co)"
   and a18: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCir co1 co2)"
+  and a18a:"\<And>co ty b. \<lbrakk>\<And>c. P5 c co; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P5 b (CAt co ty)"
   and a19: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeft co)"
   and a20: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRight co)"
-  and a21: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CSim co)"
+  and a21: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CSim co1 co2)"
   and a22: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRightc co)"
   and a23: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeftc co)"
   and a24: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCoe co1 co2)"
   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>string b. P7 b (C string)"
+  and a28: "\<And>string b. P7 b (K 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>
     \<Longrightarrow> P7 b (LAMC tvar ckind trm)"
-  and a31: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (APP trm ty)"
+  and a31: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (AppT trm ty)"
+  and a31a:"\<And>trm co b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P5 c co\<rbrakk> \<Longrightarrow> P7 b (AppC trm co)"
   and a32: "\<And>var ty trm b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm; atom var \<sharp> b\<rbrakk> \<Longrightarrow> P7 b (Lam var ty trm)"
   and a33: "\<And>trm1 trm2 b. \<lbrakk>\<And>c. P7 c trm1; \<And>c. P7 c trm2\<rbrakk> \<Longrightarrow> P7 b (App trm1 trm2)"
   and a34: "\<And>var ty trm1 trm2 b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm1; \<And>c. P7 c trm2; atom var \<sharp> b\<rbrakk>
@@ -369,7 +375,7 @@
   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 tvars cvars vars b. \<lbrakk>\<And>c. P11 c tvars; \<And>c. P12 c cvars; \<And>c. P10 c vars\<rbrakk>
-    \<Longrightarrow> P9 b (K string tvars cvars vars)"
+    \<Longrightarrow> P9 b (Kpat string tvars cvars vars)"
   and a40: "\<And>b. P10 b VsNil"
   and a41: "\<And>var ty vars b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P10 c vars\<rbrakk> \<Longrightarrow> P10 b (VsCons var ty vars)"
   and a42: "\<And>b. P11 b TvsNil"
@@ -437,17 +443,17 @@
     apply blast
 
 (* GOAL2 *)
-    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> e \<and>
-                       supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> co)) \<sharp>* pa)")
+    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> e \<and>
+                       supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> co)) \<sharp>* pa)")
     apply clarify
     apply (simp only: perm)
-    apply(rule_tac t="CAll (p \<bullet> tvar) (p \<bullet> ckind) (p \<bullet> co)"
-               and s="CAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> co)" in subst)
+    apply(rule_tac t="CAll (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> co)"
+               and s="CAll (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> co)" in subst)
     apply (simp only: eq_iff)
     apply (rule_tac x="-pa" in exI)
     apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
-    apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> tvar)}"
-                and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom tvar})" in subst)
+    apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> cvar)}"
+                and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom cvar})" in subst)
     apply (simp add: eqvts)
     apply (simp add: eqvts[symmetric])
     apply (rule conjI)
@@ -518,17 +524,17 @@
     apply blast
 
 (* GOAL4 a copy-and-paste *)
-    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and>
-                       supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)")
+    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> g \<and>
+                       supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> trm)) \<sharp>* pa)")
     apply clarify
     apply (simp only: perm)
-    apply(rule_tac t="LAMC (p \<bullet> tvar) (p \<bullet> ckind) (p \<bullet> trm)"
-               and s="LAMC (pa \<bullet> p \<bullet> tvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> trm)" in subst)
+    apply(rule_tac t="LAMC (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> trm)"
+               and s="LAMC (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> trm)" in subst)
     apply (simp only: eq_iff)
     apply (rule_tac x="-pa" in exI)
     apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
-    apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}"
-                and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst)
+    apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> cvar)}"
+                and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom cvar})" in subst)
     apply (simp add: eqvts)
     apply (simp add: eqvts[symmetric])
     apply (rule conjI)