# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269435260 -3600
# Node ID 68c8666453f721c58f54a75b94b8516a1272b6a7
# Parent  e94bfef17bb8a0fdcdd7204e138468a6d76494dc
Started proving strong induction.

diff -r e94bfef17bb8 -r 68c8666453f7 Nominal/ExCoreHaskell.thy
--- a/Nominal/ExCoreHaskell.thy	Wed Mar 24 12:36:58 2010 +0100
+++ b/Nominal/ExCoreHaskell.thy	Wed Mar 24 13:54:20 2010 +0100
@@ -96,14 +96,16 @@
   and a05: "\<And>char b. P3 b (TC char)"
   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 a08: "\<And>tvar tkind ty b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P3 b (TAll tvar tkind ty)"
+  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 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 a15: "\<And>tvar ckind co b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CAll tvar ckind co)"
+  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 a18: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCir co1 co2)"
@@ -117,17 +119,19 @@
   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 a29: "\<And>tvar tkind trm b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P7 c trm\<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\<rbrakk> \<Longrightarrow> P7 b (LAMC tvar ckind trm)"
+  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 a32: "\<And>var ty trm b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm\<rbrakk> \<Longrightarrow> P7 b (Lam var ty trm)"
+  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\<rbrakk>
+  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>
     \<Longrightarrow> P7 b (Let var ty trm1 trm2)"
   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\<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; 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)"
@@ -139,7 +143,7 @@
   and a44: "\<And>b. P12 b TVCKNil"
   and a45: "\<And>tvar ckind tvck_lst b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P12 c tvck_lst\<rbrakk>
     \<Longrightarrow> P12 b (TVCKCons tvar ckind tvck_lst)"
-  shows "P1 (a :: 'a :: pt) tkind \<and> 
+  shows "P1 (a :: 'a :: pt) tkind \<and>
          P2 (b :: 'b :: pt) ckind \<and>
          P3 (c :: 'c :: pt) ty \<and>
          P4 (d :: 'd :: pt) ty_lst \<and>
@@ -154,7 +158,8 @@
 proof -
   have a: "(\<forall>p a. P1 a (p \<bullet> tkind)) \<and> (\<forall>p b. P2 b (p \<bullet> ckind)) \<and> (\<forall>p c. P3 c (p \<bullet> ty)) \<and> (\<forall>p d. P4 d (p \<bullet> ty_lst)) \<and> (\<forall>p e. P5 e (p \<bullet> co)) \<and> (\<forall>p f. P6 f (p \<bullet> co_lst)) \<and> (\<forall>p g. P7 g (p \<bullet> trm)) \<and> (\<forall>p h. P8 h (p \<bullet> assoc_lst)) \<and> (\<forall>p i. P9 i (p \<bullet> pat)) \<and> (\<forall>p j. P10 j (p \<bullet> vt_lst)) \<and> (\<forall>p k. P11 k (p \<bullet> tvtk_lst)) \<and> (\<forall>p l. P12 l (p \<bullet> tvck_lst))"
     apply (rule tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.induct)
-    apply (simp add: a01)
+    apply (tactic {* ALLGOALS (REPEAT o rtac allI) *})
+    apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *})
     sorry
   have g1: "P1 a (0 \<bullet> tkind)" using a[THEN conjunct1] by blast
   have g2: "P2 b (0 \<bullet> ckind)" using a[THEN conjunct2,THEN conjunct1] by blast