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 1684 b9e4c812d2c6
parent 1667 2922b04d9545
child 1688 0b2535a72fd0
equal deleted inserted replaced
1683:f78c820f67c3 1684:b9e4c812d2c6 
     9 atom_decl var
 
     9 atom_decl var
 
    10 atom_decl tvar
 
    10 atom_decl tvar
 
    11 
    11 
    12 (* there are types, coercion types and regular types list-data-structure *)
 
    12 (* there are types, coercion types and regular types list-data-structure *)
 
    13 
    13 
       
    14 ML {* val _ = alpha_type := AlphaGen *}
 
    14 nominal_datatype tkind =
 
    15 nominal_datatype tkind =
 
    15   KStar
 
    16   KStar
 
    16 | KFun "tkind" "tkind"
 
    17 | KFun "tkind" "tkind"
 
    17 and ckind =
 
    18 and ckind =
 
    18   CKEq "ty" "ty"
 
    19   CKEq "ty" "ty"
 
    19 and ty =
 
    20 and ty =
 
    20   TVar "tvar"
 
    21   TVar "tvar"
 
    21 | TC "char"
 
    22 | TC "string"
 
    22 | TApp "ty" "ty"
 
    23 | TApp "ty" "ty"
 
    23 | TFun "char" "ty_lst"
 
    24 | TFun "string" "ty_lst"
 
    24 | TAll tv::"tvar" "tkind" T::"ty"  bind tv in T
 
    25 | TAll tv::"tvar" "tkind" T::"ty"  bind tv in T
 
    25 | TEq "ty" "ty" "ty"
 
    26 | TEq "ty" "ty" "ty"
 
    26 and ty_lst =
 
    27 and ty_lst =
 
    27   TsNil
 
    28   TsNil
 
    28 | TsCons "ty" "ty_lst"
 
    29 | TsCons "ty" "ty_lst"
 
    29 and co =
 
    30 and co =
 
    30   CC "char"
 
    31   CC "string"
 
    31 | CApp "co" "co"
 
    32 | CApp "co" "co"
 
    32 | CFun "char" "co_lst"
 
    33 | CFun "string" "co_lst"
 
    33 | CAll tv::"tvar" "ckind" C::"co"  bind tv in C
 
    34 | CAll tv::"tvar" "ckind" C::"co"  bind tv in C
 
    34 | CEq "co" "co" "co"
 
    35 | CEq "co" "co" "co"
 
    35 | CSym "co"
 
    36 | CSym "co"
 
    36 | CCir "co" "co"
 
    37 | CCir "co" "co"
 
    37 | CLeft "co"
 
    38 | CLeft "co"
 
    43 and co_lst =
 
    44 and co_lst =
 
    44   CsNil
 
    45   CsNil
 
    45 | CsCons "co" "co_lst"
 
    46 | CsCons "co" "co_lst"
 
    46 and trm =
 
    47 and trm =
 
    47   Var "var"
 
    48   Var "var"
 
    48 | C "char"
 
    49 | C "string"
 
    49 | LAMT tv::"tvar" "tkind" t::"trm" bind tv in t
 
    50 | LAMT tv::"tvar" "tkind" t::"trm" bind tv in t
 
    50 | LAMC tv::"tvar" "ckind" t::"trm" bind tv in t
 
    51 | LAMC tv::"tvar" "ckind" t::"trm" bind tv in t
 
    51 | APP "trm" "ty"
 
    52 | APP "trm" "ty"
 
    52 | Lam v::"var" "ty" t::"trm"       bind v in t
 
    53 | Lam v::"var" "ty" t::"trm"       bind v in t
 
    53 | App "trm" "trm"
 
    54 | App "trm" "trm"
 
    56 | Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"
 
    57 | Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"
 
    57 and assoc_lst =
 
    58 and assoc_lst =
 
    58   ANil
 
    59   ANil
 
    59 | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t
 
    60 | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t
 
    60 and pat =
 
    61 and pat =
 
    61   K "char" "tvtk_lst" "tvck_lst" "vt_lst"
 
    62   K "string" "tvtk_lst" "tvck_lst" "vt_lst"
 
    62 and vt_lst =
 
    63 and vt_lst =
 
    63   VTNil
 
    64   VTNil
 
    64 | VTCons "var" "ty" "vt_lst"
 
    65 | VTCons "var" "ty" "vt_lst"
 
    65 and tvtk_lst =
 
    66 and tvtk_lst =
 
    66   TVTKNil
 
    67   TVTKNil
 
   138  apply (simp_all)
 
   139  apply (simp_all)
 
   139  apply (rule alpha_intros)
 
   140  apply (rule alpha_intros)
 
   140  apply (simp_all add: rsp_pre)
 
   141  apply (simp_all add: rsp_pre)
 
   141  done
 
   142  done
 
   142 
   143 
   143 lemmas permute_bv[simp] = permute_bv_raw.simps[quot_lifted]
 
   144 thm permute_bv_raw.simps[no_vars]
 
       
   145  permute_bv_vt_raw.simps[quot_lifted]
 
       
   146  permute_bv_tvck_raw.simps[quot_lifted]
 
       
   147  permute_bv_tvtk_raw.simps[quot_lifted]
 
       
   148 
       
   149 lemma permute_bv_pre:
 
       
   150   "permute_bv p (K c l1 l2 l3) =
 
       
   151    K c (permute_bv_tvtk p l1) (permute_bv_tvck p l2) (permute_bv_vt p l3)"
 
       
   152   by (lifting permute_bv_raw.simps)
 
       
   153 
       
   154 lemmas permute_bv[simp] =
 
       
   155  permute_bv_pre
 
   144  permute_bv_vt_raw.simps[quot_lifted]
 
   156  permute_bv_vt_raw.simps[quot_lifted]
 
   145  permute_bv_tvck_raw.simps[quot_lifted]
 
   157  permute_bv_tvck_raw.simps[quot_lifted]
 
   146  permute_bv_tvtk_raw.simps[quot_lifted]
 
   158  permute_bv_tvtk_raw.simps[quot_lifted]
 
   147 
   159 
   148 lemma perm_bv1:
 
   160 lemma perm_bv1:
 
   315 lemma strong_inudction_principle:
 
   327 lemma strong_inudction_principle:
 
   316   assumes a01: "\<And>b. P1 b KStar"
 
   328   assumes a01: "\<And>b. P1 b KStar"
 
   317   and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)"
 
   329   and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)"
 
   318   and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)"
 
   330   and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)"
 
   319   and a04: "\<And>tvar b. P3 b (TVar tvar)"
 
   331   and a04: "\<And>tvar b. P3 b (TVar tvar)"
 
   320   and a05: "\<And>char b. P3 b (TC char)"
 
   332   and a05: "\<And>string b. P3 b (TC string)"
 
   321   and a06: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P3 b (TApp ty1 ty2)"
 
   333   and a06: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P3 b (TApp ty1 ty2)"
 
   322   and a07: "\<And>char ty_lst b. \<lbrakk>\<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P3 b (TFun char ty_lst)"
 
   334   and a07: "\<And>string ty_lst b. \<lbrakk>\<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P3 b (TFun string ty_lst)"
 
   323   and a08: "\<And>tvar tkind ty b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P3 c ty; atom tvar \<sharp> b\<rbrakk>
 
   335   and a08: "\<And>tvar tkind ty b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P3 c ty; atom tvar \<sharp> b\<rbrakk>
 
   324     \<Longrightarrow> P3 b (TAll tvar tkind ty)"
 
   336     \<Longrightarrow> P3 b (TAll tvar tkind ty)"
 
   325   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)"
 
   337   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)"
 
   326   and a10: "\<And>b. P4 b TsNil"
 
   338   and a10: "\<And>b. P4 b TsNil"
 
   327   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)"
 
   339   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)"
 
   328   and a12: "\<And>char b. P5 b (CC char)"
 
   340   and a12: "\<And>string b. P5 b (CC string)"
 
   329   and a13: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CApp co1 co2)"
 
   341   and a13: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CApp co1 co2)"
 
   330   and a14: "\<And>char co_lst b. \<lbrakk>\<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P5 b (CFun char co_lst)"
 
   342   and a14: "\<And>string co_lst b. \<lbrakk>\<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P5 b (CFun string co_lst)"
 
   331   and a15: "\<And>tvar ckind co b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P5 c co; atom tvar \<sharp> b\<rbrakk>
 
   343   and a15: "\<And>tvar ckind co b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P5 c co; atom tvar \<sharp> b\<rbrakk>
 
   332     \<Longrightarrow> P5 b (CAll tvar ckind co)"
 
   344     \<Longrightarrow> P5 b (CAll tvar ckind co)"
 
   333   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)"
 
   345   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)"
 
   334   and a17: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CSym co)"
 
   346   and a17: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CSym co)"
 
   335   and a18: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCir co1 co2)"
 
   347   and a18: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCir co1 co2)"
 
   340   and a23: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeftc co)"
 
   352   and a23: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeftc co)"
 
   341   and a24: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCoe co1 co2)"
 
   353   and a24: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCoe co1 co2)"
 
   342   and a25: "\<And>b. P6 b CsNil"
 
   354   and a25: "\<And>b. P6 b CsNil"
 
   343   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)"
 
   355   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)"
 
   344   and a27: "\<And>var b. P7 b (Var var)"
 
   356   and a27: "\<And>var b. P7 b (Var var)"
 
   345   and a28: "\<And>char b. P7 b (C char)"
 
   357   and a28: "\<And>string b. P7 b (C string)"
 
   346   and a29: "\<And>tvar tkind trm b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>
 
   358   and a29: "\<And>tvar tkind trm b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>
 
   347     \<Longrightarrow> P7 b (LAMT tvar tkind trm)"
 
   359     \<Longrightarrow> P7 b (LAMT tvar tkind trm)"
 
   348   and a30: "\<And>tvar ckind trm b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>
 
   360   and a30: "\<And>tvar ckind trm b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>
 
   349     \<Longrightarrow> P7 b (LAMC tvar ckind trm)"
 
   361     \<Longrightarrow> P7 b (LAMC tvar ckind trm)"
 
   350   and a31: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (APP trm ty)"
 
   362   and a31: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (APP trm ty)"
 
   355   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)"
 
   367   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)"
 
   356   and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)"
 
   368   and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)"
 
   357   and a37: "\<And>b. P8 b ANil"
 
   369   and a37: "\<And>b. P8 b ANil"
 
   358   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>
 
   370   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>
 
   359     \<Longrightarrow> P8 b (ACons pat trm assoc_lst)"
 
   371     \<Longrightarrow> P8 b (ACons pat trm assoc_lst)"
 
   360   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>
 
   372   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>
 
   361     \<Longrightarrow> P9 b (K char tvtk_lst tvck_lst vt_lst)"
 
   373     \<Longrightarrow> P9 b (K string tvtk_lst tvck_lst vt_lst)"
 
   362   and a40: "\<And>b. P10 b VTNil"
 
   374   and a40: "\<And>b. P10 b VTNil"
 
   363   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)"
 
   375   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)"
 
   364   and a42: "\<And>b. P11 b TVTKNil"
 
   376   and a42: "\<And>b. P11 b TVTKNil"
 
   365   and a43: "\<And>tvar tkind tvtk_lst b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P11 c tvtk_lst\<rbrakk>
 
   377   and a43: "\<And>tvar tkind tvtk_lst b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P11 c tvtk_lst\<rbrakk>
 
   366     \<Longrightarrow> P11 b (TVTKCons tvar tkind tvtk_lst)"
 
   378     \<Longrightarrow> P11 b (TVTKCons tvar tkind tvtk_lst)"
nominal2