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 1688 0b2535a72fd0
parent 1687 51bc795b81fd
parent 1684 b9e4c812d2c6
child 1695 e42ee5947b5c
equal deleted inserted replaced
1687:51bc795b81fd 1688:0b2535a72fd0 
     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 (* At ??? *)
 
    38 (* At ??? *)
 
    44 and co_lst =
 
    45 and co_lst =
 
    45   CsNil
 
    46   CsNil
 
    46 | CsCons "co" "co_lst"
 
    47 | CsCons "co" "co_lst"
 
    47 and trm =
 
    48 and trm =
 
    48   Var "var"
 
    49   Var "var"
 
    49 | C "char"
 
    50 | C "string"
 
    50 | LAMT tv::"tvar" "tkind" t::"trm" bind tv in t
 
    51 | LAMT tv::"tvar" "tkind" t::"trm" bind tv in t
 
    51 | LAMC tv::"tvar" "ckind" t::"trm" bind tv in t
 
    52 | LAMC tv::"tvar" "ckind" t::"trm" bind tv in t
 
    52 | APP "trm" "ty"
 
    53 | APP "trm" "ty"
 
    53 | Lam v::"var" "ty" t::"trm"       bind v in t
 
    54 | Lam v::"var" "ty" t::"trm"       bind v in t
 
    54 | App "trm" "trm"
 
    55 | App "trm" "trm"
 
    57 | Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"
 
    58 | Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"
 
    58 and assoc_lst =
 
    59 and assoc_lst =
 
    59   ANil
 
    60   ANil
 
    60 | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t
 
    61 | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t
 
    61 and pat =
 
    62 and pat =
 
    62   K "char" "tvtk_lst" "tvck_lst" "vt_lst"
 
    63   K "string" "tvtk_lst" "tvck_lst" "vt_lst"
 
    63 and vt_lst =
 
    64 and vt_lst =
 
    64   VTNil
 
    65   VTNil
 
    65 | VTCons "var" "ty" "vt_lst"
 
    66 | VTCons "var" "ty" "vt_lst"
 
    66 and tvtk_lst =
 
    67 and tvtk_lst =
 
    67   TVTKNil
 
    68   TVTKNil
 
   139  apply (simp_all)
 
   140  apply (simp_all)
 
   140  apply (rule alpha_intros)
 
   141  apply (rule alpha_intros)
 
   141  apply (simp_all add: rsp_pre)
 
   142  apply (simp_all add: rsp_pre)
 
   142  done
 
   143  done
 
   143 
   144 
   144 lemmas permute_bv[simp] = permute_bv_raw.simps[quot_lifted]
 
   145 thm permute_bv_raw.simps[no_vars]
 
       
   146  permute_bv_vt_raw.simps[quot_lifted]
 
       
   147  permute_bv_tvck_raw.simps[quot_lifted]
 
       
   148  permute_bv_tvtk_raw.simps[quot_lifted]
 
       
   149 
       
   150 lemma permute_bv_pre:
 
       
   151   "permute_bv p (K c l1 l2 l3) =
 
       
   152    K c (permute_bv_tvtk p l1) (permute_bv_tvck p l2) (permute_bv_vt p l3)"
 
       
   153   by (lifting permute_bv_raw.simps)
 
       
   154 
       
   155 lemmas permute_bv[simp] =
 
       
   156  permute_bv_pre
 
   145  permute_bv_vt_raw.simps[quot_lifted]
 
   157  permute_bv_vt_raw.simps[quot_lifted]
 
   146  permute_bv_tvck_raw.simps[quot_lifted]
 
   158  permute_bv_tvck_raw.simps[quot_lifted]
 
   147  permute_bv_tvtk_raw.simps[quot_lifted]
 
   159  permute_bv_tvtk_raw.simps[quot_lifted]
 
   148 
   160 
   149 lemma perm_bv1:
 
   161 lemma perm_bv1:
 
   316 lemma strong_inudction_principle:
 
   328 lemma strong_inudction_principle:
 
   317   assumes a01: "\<And>b. P1 b KStar"
 
   329   assumes a01: "\<And>b. P1 b KStar"
 
   318   and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)"
 
   330   and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)"
 
   319   and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)"
 
   331   and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)"
 
   320   and a04: "\<And>tvar b. P3 b (TVar tvar)"
 
   332   and a04: "\<And>tvar b. P3 b (TVar tvar)"
 
   321   and a05: "\<And>char b. P3 b (TC char)"
 
   333   and a05: "\<And>string b. P3 b (TC string)"
 
   322   and a06: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P3 b (TApp ty1 ty2)"
 
   334   and a06: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P3 b (TApp ty1 ty2)"
 
   323   and a07: "\<And>char ty_lst b. \<lbrakk>\<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P3 b (TFun char ty_lst)"
 
   335   and a07: "\<And>string ty_lst b. \<lbrakk>\<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P3 b (TFun string ty_lst)"
 
   324   and a08: "\<And>tvar tkind ty b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P3 c ty; atom tvar \<sharp> b\<rbrakk>
 
   336   and a08: "\<And>tvar tkind ty b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P3 c ty; atom tvar \<sharp> b\<rbrakk>
 
   325     \<Longrightarrow> P3 b (TAll tvar tkind ty)"
 
   337     \<Longrightarrow> P3 b (TAll tvar tkind ty)"
 
   326   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)"
 
   338   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)"
 
   327   and a10: "\<And>b. P4 b TsNil"
 
   339   and a10: "\<And>b. P4 b TsNil"
 
   328   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)"
 
   340   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)"
 
   329   and a12: "\<And>char b. P5 b (CC char)"
 
   341   and a12: "\<And>string b. P5 b (CC string)"
 
   330   and a13: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CApp co1 co2)"
 
   342   and a13: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CApp co1 co2)"
 
   331   and a14: "\<And>char co_lst b. \<lbrakk>\<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P5 b (CFun char co_lst)"
 
   343   and a14: "\<And>string co_lst b. \<lbrakk>\<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P5 b (CFun string co_lst)"
 
   332   and a15: "\<And>tvar ckind co b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P5 c co; atom tvar \<sharp> b\<rbrakk>
 
   344   and a15: "\<And>tvar ckind co b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P5 c co; atom tvar \<sharp> b\<rbrakk>
 
   333     \<Longrightarrow> P5 b (CAll tvar ckind co)"
 
   345     \<Longrightarrow> P5 b (CAll tvar ckind co)"
 
   334   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)"
 
   346   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)"
 
   335   and a17: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CSym co)"
 
   347   and a17: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CSym co)"
 
   336   and a18: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCir co1 co2)"
 
   348   and a18: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCir co1 co2)"
 
   341   and a23: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeftc co)"
 
   353   and a23: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeftc co)"
 
   342   and a24: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCoe co1 co2)"
 
   354   and a24: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCoe co1 co2)"
 
   343   and a25: "\<And>b. P6 b CsNil"
 
   355   and a25: "\<And>b. P6 b CsNil"
 
   344   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)"
 
   356   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)"
 
   345   and a27: "\<And>var b. P7 b (Var var)"
 
   357   and a27: "\<And>var b. P7 b (Var var)"
 
   346   and a28: "\<And>char b. P7 b (C char)"
 
   358   and a28: "\<And>string b. P7 b (C string)"
 
   347   and a29: "\<And>tvar tkind trm b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>
 
   359   and a29: "\<And>tvar tkind trm b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>
 
   348     \<Longrightarrow> P7 b (LAMT tvar tkind trm)"
 
   360     \<Longrightarrow> P7 b (LAMT tvar tkind trm)"
 
   349   and a30: "\<And>tvar ckind trm b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>
 
   361   and a30: "\<And>tvar ckind trm b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>
 
   350     \<Longrightarrow> P7 b (LAMC tvar ckind trm)"
 
   362     \<Longrightarrow> P7 b (LAMC tvar ckind trm)"
 
   351   and a31: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (APP trm ty)"
 
   363   and a31: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (APP trm ty)"
 
   356   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)"
 
   368   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)"
 
   357   and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)"
 
   369   and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)"
 
   358   and a37: "\<And>b. P8 b ANil"
 
   370   and a37: "\<And>b. P8 b ANil"
 
   359   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>
 
   371   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>
 
   360     \<Longrightarrow> P8 b (ACons pat trm assoc_lst)"
 
   372     \<Longrightarrow> P8 b (ACons pat trm assoc_lst)"
 
   361   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>
 
   373   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>
 
   362     \<Longrightarrow> P9 b (K char tvtk_lst tvck_lst vt_lst)"
 
   374     \<Longrightarrow> P9 b (K string tvtk_lst tvck_lst vt_lst)"
 
   363   and a40: "\<And>b. P10 b VTNil"
 
   375   and a40: "\<And>b. P10 b VTNil"
 
   364   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)"
 
   376   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)"
 
   365   and a42: "\<And>b. P11 b TVTKNil"
 
   377   and a42: "\<And>b. P11 b TVTKNil"
 
   366   and a43: "\<And>tvar tkind tvtk_lst b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P11 c tvtk_lst\<rbrakk>
 
   378   and a43: "\<And>tvar tkind tvtk_lst b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P11 c tvtk_lst\<rbrakk>
 
   367     \<Longrightarrow> P11 b (TVTKCons tvar tkind tvtk_lst)"
 
   379     \<Longrightarrow> P11 b (TVTKCons tvar tkind tvtk_lst)"
nominal2