Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/ExCoreHaskell.thy
changeset 1631 e94bfef17bb8
parent 1630 b295a928c56b
child 1632 68c8666453f7
equal deleted inserted replaced
1630:b295a928c56b 1631:e94bfef17bb8 
    87 
    87 
    88 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)
 
    88 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)
 
    89 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified fv_supp]
 
    89 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified fv_supp]
 
    90 
    90 
    91 lemma 
    91 lemma 
    92   assumes a01: "P1 KStar"
 
    92   assumes a01: "\<And>b. P1 b KStar"
 
    93   and a02: "\<And>tkind1 tkind2. \<lbrakk>P1 tkind1; P1 tkind2\<rbrakk> \<Longrightarrow> P1 (KFun tkind1 tkind2)"
 
    93   and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)"
 
    94   and a03: "\<And>ty1 ty2. \<lbrakk>P3 ty1; P3 ty2\<rbrakk> \<Longrightarrow> P2 (CKEq ty1 ty2)"
 
    94   and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)"
 
    95   and a04: "\<And>tvar. P3 (TVar tvar)"
 
    95   and a04: "\<And>tvar b. P3 b (TVar tvar)"
 
    96   and a05: "\<And>char. P3 (TC char)"
 
    96   and a05: "\<And>char b. P3 b (TC char)"
 
    97   and a06: "\<And>ty1 ty2. \<lbrakk>P3 ty1; P3 ty2\<rbrakk> \<Longrightarrow> P3 (TApp ty1 ty2)"
 
    97   and a06: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P3 b (TApp ty1 ty2)"
 
    98   and a07: "\<And>char ty_lst. P4 ty_lst \<Longrightarrow> P3 (TFun char ty_lst)"
 
    98   and a07: "\<And>char ty_lst b. \<lbrakk>\<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P3 b (TFun char ty_lst)"
 
    99   and a08: "\<And>tvar tkind ty. \<lbrakk>P1 tkind; P3 ty\<rbrakk> \<Longrightarrow> P3 (TAll tvar tkind ty)"
 
    99   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)"
 
   100   and a09: "\<And>ty1 ty2 ty3. \<lbrakk>P3 ty1; P3 ty2; P3 ty3\<rbrakk> \<Longrightarrow> P3 (TEq ty1 ty2 ty3)"
 
   100   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)"
 
   101   and a10: "P4 TsNil"
 
   101   and a10: "\<And>b. P4 b TsNil"
 
   102   and a11: "\<And>ty ty_lst. \<lbrakk>P3 ty; P4 ty_lst\<rbrakk> \<Longrightarrow> P4 (TsCons ty ty_lst)"
 
   102   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)"
 
   103   and a12: "\<And>char. P5 (CC char)"
 
   103   and a12: "\<And>char b. P5 b (CC char)"
 
   104   and a13: "\<And>co1 co2. \<lbrakk>P5 co1; P5 co2\<rbrakk> \<Longrightarrow> P5 (CApp co1 co2)"
 
   104   and a13: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CApp co1 co2)"
 
   105   and a14: "\<And>char co_lst. P6 co_lst \<Longrightarrow> P5 (CFun char co_lst)"
 
   105   and a14: "\<And>char co_lst b. \<lbrakk>\<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P5 b (CFun char co_lst)"
 
   106   and a15: "\<And>tvar ckind co. \<lbrakk>P2 ckind; P5 co\<rbrakk> \<Longrightarrow> P5 (CAll tvar ckind co)"
 
   106   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)"
 
   107   and a16: "\<And>co1 co2 co3. \<lbrakk>P5 co1; P5 co2; P5 co3\<rbrakk> \<Longrightarrow> P5 (CEq co1 co2 co3)"
 
   107   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)"
 
   108   and a17: "\<And>co. P5 co \<Longrightarrow> P5 (CSym co)"
 
   108   and a17: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CSym co)"
 
   109   and a18: "\<And>co1 co2. \<lbrakk>P5 co1; P5 co2\<rbrakk> \<Longrightarrow> P5 (CCir co1 co2)"
 
   109   and a18: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCir co1 co2)"
 
   110   and a19: "\<And>co. P5 co \<Longrightarrow> P5 (CLeft co)"
 
   110   and a19: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeft co)"
 
   111   and a20: "\<And>co. P5 co \<Longrightarrow> P5 (CRight co)"
 
   111   and a20: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRight co)"
 
   112   and a21: "\<And>co. P5 co \<Longrightarrow> P5 (CSim co)"
 
   112   and a21: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CSim co)"
 
   113   and a22: "\<And>co. P5 co \<Longrightarrow> P5 (CRightc co)"
 
   113   and a22: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRightc co)"
 
   114   and a23: "\<And>co. P5 co \<Longrightarrow> P5 (CLeftc co)"
 
   114   and a23: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeftc co)"
 
   115   and a24: "\<And>co1 co2. \<lbrakk>P5 co1; P5 co2\<rbrakk> \<Longrightarrow> P5 (CCoe co1 co2)"
 
   115   and a24: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCoe co1 co2)"
 
   116   and a25: "P6 CsNil"
 
   116   and a25: "\<And>b. P6 b CsNil"
 
   117   and a26: "\<And>co co_lst. \<lbrakk>P5 co; P6 co_lst\<rbrakk> \<Longrightarrow> P6 (CsCons co co_lst)"
 
   117   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)"
 
   118   and a27: "\<And>var. P7 (Var var)"
 
   118   and a27: "\<And>var b. P7 b (Var var)"
 
   119   and a28: "\<And>char. P7 (C char)"
 
   119   and a28: "\<And>char b. P7 b (C char)"
 
   120   and a29: "\<And>tvar tkind trm. \<lbrakk>P1 tkind; P7 trm\<rbrakk> \<Longrightarrow> P7 (LAMT tvar tkind trm)"
 
   120   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)"
 
   121   and a30: "\<And>tvar ckind trm. \<lbrakk>P2 ckind; P7 trm\<rbrakk> \<Longrightarrow> P7 (LAMC tvar ckind trm)"
 
   121   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)"
 
   122   and a31: "\<And>trm ty. \<lbrakk>P7 trm; P3 ty\<rbrakk> \<Longrightarrow> P7 (APP trm ty)"
 
   122   and a31: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (APP trm ty)"
 
   123   and a32: "\<And>var ty trm. \<lbrakk>P3 ty; P7 trm\<rbrakk> \<Longrightarrow> P7 (Lam var ty trm)"
 
   123   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)"
 
   124   and a33: "\<And>trm1 trm2. \<lbrakk>P7 trm1; P7 trm2\<rbrakk> \<Longrightarrow> P7 (App trm1 trm2)"
 
   124   and a33: "\<And>trm1 trm2 b. \<lbrakk>\<And>c. P7 c trm1; \<And>c. P7 c trm2\<rbrakk> \<Longrightarrow> P7 b (App trm1 trm2)"
 
   125   and a34: "\<And>var ty trm1 trm2. \<lbrakk>P3 ty; P7 trm1; P7 trm2\<rbrakk> \<Longrightarrow> P7 (ExCoreHaskell.Let var ty trm1 trm2)"
 
   125   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>
 
   126   and a35: "\<And>trm assoc_lst. \<lbrakk>P7 trm; P8 assoc_lst\<rbrakk> \<Longrightarrow> P7 (Case trm assoc_lst)"
 
   126     \<Longrightarrow> P7 b (Let var ty trm1 trm2)"
 
   127   and a36: "\<And>trm ty. \<lbrakk>P7 trm; P3 ty\<rbrakk> \<Longrightarrow> P7 (Cast trm ty)"
 
   127   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)"
 
   128   and a37: "P8 ANil"
 
   128   and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)"
 
   129   and a38: "\<And>pat trm assoc_lst. \<lbrakk>P9 pat; P7 trm; P8 assoc_lst\<rbrakk> \<Longrightarrow> P8 (ACons pat trm assoc_lst)"
 
   129   and a37: "\<And>b. P8 b ANil"
 
   130   and a39: "\<And>char tvtk_lst tvck_lst vt_lst. \<lbrakk>P11 tvtk_lst; P12 tvck_lst; P10 vt_lst\<rbrakk>
 
   130   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>
 
   131     \<Longrightarrow> P9 (K char tvtk_lst tvck_lst vt_lst)"
 
   131     \<Longrightarrow> P8 b (ACons pat trm assoc_lst)"
 
   132   and a40: "P10 VTNil"
 
   132   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>
 
   133   and a41: "\<And>var ty vt_lst. \<lbrakk>P3 ty; P10 vt_lst\<rbrakk> \<Longrightarrow> P10 (VTCons var ty vt_lst)"
 
   133     \<Longrightarrow> P9 b (K char tvtk_lst tvck_lst vt_lst)"
 
   134   and a42: "P11 TVTKNil"
 
   134   and a40: "\<And>b. P10 b VTNil"
 
   135   and a43: "\<And>tvar tkind tvtk_lst. \<lbrakk>P1 tkind; P11 tvtk_lst\<rbrakk> \<Longrightarrow> P11 (TVTKCons tvar tkind tvtk_lst)"
 
   135   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)"
 
   136   and a44: "P12 TVCKNil"
 
   136   and a42: "\<And>b. P11 b TVTKNil"
 
   137   and a45: "\<And>tvar ckind tvck_lst. \<lbrakk>P2 ckind; P12 tvck_lst\<rbrakk> \<Longrightarrow> P12 (TVCKCons tvar ckind tvck_lst)"
 
   137   and a43: "\<And>tvar tkind tvtk_lst b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P11 c tvtk_lst\<rbrakk>
 
   138   shows "P1 tkind \<and> P2 ckind \<and> P3 ty \<and> P4 ty_lst \<and> P5 co \<and> P6 co_lst \<and>
 
   138     \<Longrightarrow> P11 b (TVTKCons tvar tkind tvtk_lst)"
 
   139          P7 trm \<and> P8 assoc_lst \<and> P9 pat \<and> P10 vt_lst \<and> P11 tvtk_lst \<and> P12 tvck_lst"
 
   139   and a44: "\<And>b. P12 b TVCKNil"
 
       
   140   and a45: "\<And>tvar ckind tvck_lst b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P12 c tvck_lst\<rbrakk>
 
       
   141     \<Longrightarrow> P12 b (TVCKCons tvar ckind tvck_lst)"
 
       
   142   shows "P1 (a :: 'a :: pt) tkind \<and> 
       
   143          P2 (b :: 'b :: pt) ckind \<and>
 
       
   144          P3 (c :: 'c :: pt) ty \<and>
 
       
   145          P4 (d :: 'd :: pt) ty_lst \<and>
 
       
   146          P5 (e :: 'e :: pt) co \<and>
 
       
   147          P6 (f :: 'f :: pt) co_lst \<and>
 
       
   148          P7 (g :: 'g :: pt) trm \<and>
 
       
   149          P8 (h :: 'h :: pt) assoc_lst \<and>
 
       
   150          P9 (i :: 'i :: pt) pat \<and>
 
       
   151          P10 (j :: 'j :: pt) vt_lst \<and>
 
       
   152          P11 (k :: 'k :: pt) tvtk_lst \<and>
 
       
   153          P12 (l :: 'l :: pt) tvck_lst"
 
       
   154 proof -
 
       
   155   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))"
 
       
   156     apply (rule tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.induct)
 
       
   157     apply (simp add: a01)
 
       
   158     sorry
 
       
   159   have g1: "P1 a (0 \<bullet> tkind)" using a[THEN conjunct1] by blast
 
       
   160   have g2: "P2 b (0 \<bullet> ckind)" using a[THEN conjunct2,THEN conjunct1] by blast
 
       
   161   have g3: "P3 c (0 \<bullet> ty) \<and>
 
       
   162         P4 d (0 \<bullet> ty_lst) \<and> P5 e (0 \<bullet> co) \<and> P6 f (0 \<bullet> co_lst) \<and>
 
       
   163         P7 g (0 \<bullet> trm) \<and> P8 h (0 \<bullet> assoc_lst) \<and> P9 i (0 \<bullet> pat) \<and>
 
       
   164         P10 j (0 \<bullet> vt_lst) \<and> P11 k (0 \<bullet> tvtk_lst) \<and> P12 l (0 \<bullet> tvck_lst)" using a by blast
 
       
   165   show ?thesis using g1 g2 g3 by simp
 
       
   166 qed
 
   140 
   167 
   141 end
 
   168 end
 
   142 
   169 
   143 
       
   144
nominal2