# HG changeset patch # User Cezary Kaliszyk # Date 1269430618 -3600 # Node ID e94bfef17bb8a0fdcdd7204e138468a6d76494dc # Parent b295a928c56b95a79c437fde1a1560e0a2a027c5 stating the strong induction; further. diff -r b295a928c56b -r e94bfef17bb8 Nominal/ExCoreHaskell.thy --- a/Nominal/ExCoreHaskell.thy Wed Mar 24 12:05:38 2010 +0100 +++ b/Nominal/ExCoreHaskell.thy Wed Mar 24 12:36:58 2010 +0100 @@ -89,56 +89,81 @@ lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified fv_supp] lemma - assumes a01: "P1 KStar" - and a02: "\tkind1 tkind2. \P1 tkind1; P1 tkind2\ \ P1 (KFun tkind1 tkind2)" - and a03: "\ty1 ty2. \P3 ty1; P3 ty2\ \ P2 (CKEq ty1 ty2)" - and a04: "\tvar. P3 (TVar tvar)" - and a05: "\char. P3 (TC char)" - and a06: "\ty1 ty2. \P3 ty1; P3 ty2\ \ P3 (TApp ty1 ty2)" - and a07: "\char ty_lst. P4 ty_lst \ P3 (TFun char ty_lst)" - and a08: "\tvar tkind ty. \P1 tkind; P3 ty\ \ P3 (TAll tvar tkind ty)" - and a09: "\ty1 ty2 ty3. \P3 ty1; P3 ty2; P3 ty3\ \ P3 (TEq ty1 ty2 ty3)" - and a10: "P4 TsNil" - and a11: "\ty ty_lst. \P3 ty; P4 ty_lst\ \ P4 (TsCons ty ty_lst)" - and a12: "\char. P5 (CC char)" - and a13: "\co1 co2. \P5 co1; P5 co2\ \ P5 (CApp co1 co2)" - and a14: "\char co_lst. P6 co_lst \ P5 (CFun char co_lst)" - and a15: "\tvar ckind co. \P2 ckind; P5 co\ \ P5 (CAll tvar ckind co)" - and a16: "\co1 co2 co3. \P5 co1; P5 co2; P5 co3\ \ P5 (CEq co1 co2 co3)" - and a17: "\co. P5 co \ P5 (CSym co)" - and a18: "\co1 co2. \P5 co1; P5 co2\ \ P5 (CCir co1 co2)" - and a19: "\co. P5 co \ P5 (CLeft co)" - and a20: "\co. P5 co \ P5 (CRight co)" - and a21: "\co. P5 co \ P5 (CSim co)" - and a22: "\co. P5 co \ P5 (CRightc co)" - and a23: "\co. P5 co \ P5 (CLeftc co)" - and a24: "\co1 co2. \P5 co1; P5 co2\ \ P5 (CCoe co1 co2)" - and a25: "P6 CsNil" - and a26: "\co co_lst. \P5 co; P6 co_lst\ \ P6 (CsCons co co_lst)" - and a27: "\var. P7 (Var var)" - and a28: "\char. P7 (C char)" - and a29: "\tvar tkind trm. \P1 tkind; P7 trm\ \ P7 (LAMT tvar tkind trm)" - and a30: "\tvar ckind trm. \P2 ckind; P7 trm\ \ P7 (LAMC tvar ckind trm)" - and a31: "\trm ty. \P7 trm; P3 ty\ \ P7 (APP trm ty)" - and a32: "\var ty trm. \P3 ty; P7 trm\ \ P7 (Lam var ty trm)" - and a33: "\trm1 trm2. \P7 trm1; P7 trm2\ \ P7 (App trm1 trm2)" - and a34: "\var ty trm1 trm2. \P3 ty; P7 trm1; P7 trm2\ \ P7 (ExCoreHaskell.Let var ty trm1 trm2)" - and a35: "\trm assoc_lst. \P7 trm; P8 assoc_lst\ \ P7 (Case trm assoc_lst)" - and a36: "\trm ty. \P7 trm; P3 ty\ \ P7 (Cast trm ty)" - and a37: "P8 ANil" - and a38: "\pat trm assoc_lst. \P9 pat; P7 trm; P8 assoc_lst\ \ P8 (ACons pat trm assoc_lst)" - and a39: "\char tvtk_lst tvck_lst vt_lst. \P11 tvtk_lst; P12 tvck_lst; P10 vt_lst\ - \ P9 (K char tvtk_lst tvck_lst vt_lst)" - and a40: "P10 VTNil" - and a41: "\var ty vt_lst. \P3 ty; P10 vt_lst\ \ P10 (VTCons var ty vt_lst)" - and a42: "P11 TVTKNil" - and a43: "\tvar tkind tvtk_lst. \P1 tkind; P11 tvtk_lst\ \ P11 (TVTKCons tvar tkind tvtk_lst)" - and a44: "P12 TVCKNil" - and a45: "\tvar ckind tvck_lst. \P2 ckind; P12 tvck_lst\ \ P12 (TVCKCons tvar ckind tvck_lst)" - shows "P1 tkind \ P2 ckind \ P3 ty \ P4 ty_lst \ P5 co \ P6 co_lst \ - P7 trm \ P8 assoc_lst \ P9 pat \ P10 vt_lst \ P11 tvtk_lst \ P12 tvck_lst" + assumes a01: "\b. P1 b KStar" + and a02: "\tkind1 tkind2 b. \\c. P1 c tkind1; \c. P1 c tkind2\ \ P1 b (KFun tkind1 tkind2)" + and a03: "\ty1 ty2 b. \\c. P3 c ty1; \c. P3 c ty2\ \ P2 b (CKEq ty1 ty2)" + and a04: "\tvar b. P3 b (TVar tvar)" + and a05: "\char b. P3 b (TC char)" + and a06: "\ty1 ty2 b. \\c. P3 c ty1; \c. P3 c ty2\ \ P3 b (TApp ty1 ty2)" + and a07: "\char ty_lst b. \\c. P4 c ty_lst\ \ P3 b (TFun char ty_lst)" + and a08: "\tvar tkind ty b. \\c. P1 c tkind; \c. P3 c ty\ \ P3 b (TAll tvar tkind ty)" + and a09: "\ty1 ty2 ty3 b. \\c. P3 c ty1; \c. P3 c ty2; \c. P3 c ty3\ \ P3 b (TEq ty1 ty2 ty3)" + and a10: "\b. P4 b TsNil" + and a11: "\ty ty_lst b. \\c. P3 c ty; \c. P4 c ty_lst\ \ P4 b (TsCons ty ty_lst)" + and a12: "\char b. P5 b (CC char)" + and a13: "\co1 co2 b. \\c. P5 c co1; \c. P5 c co2\ \ P5 b (CApp co1 co2)" + and a14: "\char co_lst b. \\c. P6 c co_lst\ \ P5 b (CFun char co_lst)" + and a15: "\tvar ckind co b. \\c. P2 c ckind; \c. P5 c co\ \ P5 b (CAll tvar ckind co)" + and a16: "\co1 co2 co3 b. \\c. P5 c co1; \c. P5 c co2; \c. P5 c co3\ \ P5 b (CEq co1 co2 co3)" + and a17: "\co b. \\c. P5 c co\ \ P5 b (CSym co)" + and a18: "\co1 co2 b. \\c. P5 c co1; \c. P5 c co2\ \ P5 b (CCir co1 co2)" + and a19: "\co b. \\c. P5 c co\ \ P5 b (CLeft co)" + and a20: "\co b. \\c. P5 c co\ \ P5 b (CRight co)" + and a21: "\co b. \\c. P5 c co\ \ P5 b (CSim co)" + and a22: "\co b. \\c. P5 c co\ \ P5 b (CRightc co)" + and a23: "\co b. \\c. P5 c co\ \ P5 b (CLeftc co)" + and a24: "\co1 co2 b. \\c. P5 c co1; \c. P5 c co2\ \ P5 b (CCoe co1 co2)" + and a25: "\b. P6 b CsNil" + and a26: "\co co_lst b. \\c. P5 c co; \c. P6 c co_lst\ \ P6 b (CsCons co co_lst)" + and a27: "\var b. P7 b (Var var)" + and a28: "\char b. P7 b (C char)" + and a29: "\tvar tkind trm b. \\c. P1 c tkind; \c. P7 c trm\ \ P7 b (LAMT tvar tkind trm)" + and a30: "\tvar ckind trm b. \\c. P2 c ckind; \c. P7 c trm\ \ P7 b (LAMC tvar ckind trm)" + and a31: "\trm ty b. \\c. P7 c trm; \c. P3 c ty\ \ P7 b (APP trm ty)" + and a32: "\var ty trm b. \\c. P3 c ty; \c. P7 c trm\ \ P7 b (Lam var ty trm)" + and a33: "\trm1 trm2 b. \\c. P7 c trm1; \c. P7 c trm2\ \ P7 b (App trm1 trm2)" + and a34: "\var ty trm1 trm2 b. \\c. P3 c ty; \c. P7 c trm1; \c. P7 c trm2\ + \ P7 b (Let var ty trm1 trm2)" + and a35: "\trm assoc_lst b. \\c. P7 c trm; \c. P8 c assoc_lst\ \ P7 b (Case trm assoc_lst)" + and a36: "\trm ty b. \\c. P7 c trm; \c. P3 c ty\ \ P7 b (Cast trm ty)" + and a37: "\b. P8 b ANil" + and a38: "\pat trm assoc_lst b. \\c. P9 c pat; \c. P7 c trm; \c. P8 c assoc_lst\ + \ P8 b (ACons pat trm assoc_lst)" + and a39: "\char tvtk_lst tvck_lst vt_lst b. \\c. P11 c tvtk_lst; \c. P12 c tvck_lst; \c. P10 c vt_lst\ + \ P9 b (K char tvtk_lst tvck_lst vt_lst)" + and a40: "\b. P10 b VTNil" + and a41: "\var ty vt_lst b. \\c. P3 c ty; \c. P10 c vt_lst\ \ P10 b (VTCons var ty vt_lst)" + and a42: "\b. P11 b TVTKNil" + and a43: "\tvar tkind tvtk_lst b. \\c. P1 c tkind; \c. P11 c tvtk_lst\ + \ P11 b (TVTKCons tvar tkind tvtk_lst)" + and a44: "\b. P12 b TVCKNil" + and a45: "\tvar ckind tvck_lst b. \\c. P2 c ckind; \c. P12 c tvck_lst\ + \ P12 b (TVCKCons tvar ckind tvck_lst)" + shows "P1 (a :: 'a :: pt) tkind \ + P2 (b :: 'b :: pt) ckind \ + P3 (c :: 'c :: pt) ty \ + P4 (d :: 'd :: pt) ty_lst \ + P5 (e :: 'e :: pt) co \ + P6 (f :: 'f :: pt) co_lst \ + P7 (g :: 'g :: pt) trm \ + P8 (h :: 'h :: pt) assoc_lst \ + P9 (i :: 'i :: pt) pat \ + P10 (j :: 'j :: pt) vt_lst \ + P11 (k :: 'k :: pt) tvtk_lst \ + P12 (l :: 'l :: pt) tvck_lst" +proof - + have a: "(\p a. P1 a (p \ tkind)) \ (\p b. P2 b (p \ ckind)) \ (\p c. P3 c (p \ ty)) \ (\p d. P4 d (p \ ty_lst)) \ (\p e. P5 e (p \ co)) \ (\p f. P6 f (p \ co_lst)) \ (\p g. P7 g (p \ trm)) \ (\p h. P8 h (p \ assoc_lst)) \ (\p i. P9 i (p \ pat)) \ (\p j. P10 j (p \ vt_lst)) \ (\p k. P11 k (p \ tvtk_lst)) \ (\p l. P12 l (p \ 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) + sorry + have g1: "P1 a (0 \ tkind)" using a[THEN conjunct1] by blast + have g2: "P2 b (0 \ ckind)" using a[THEN conjunct2,THEN conjunct1] by blast + have g3: "P3 c (0 \ ty) \ + P4 d (0 \ ty_lst) \ P5 e (0 \ co) \ P6 f (0 \ co_lst) \ + P7 g (0 \ trm) \ P8 h (0 \ assoc_lst) \ P9 i (0 \