86 | "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t" |
86 | "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t" |
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 |
|
92 assumes a01: "P1 KStar" |
|
93 and a02: "\<And>tkind1 tkind2. \<lbrakk>P1 tkind1; P1 tkind2\<rbrakk> \<Longrightarrow> P1 (KFun tkind1 tkind2)" |
|
94 and a03: "\<And>ty1 ty2. \<lbrakk>P3 ty1; P3 ty2\<rbrakk> \<Longrightarrow> P2 (CKEq ty1 ty2)" |
|
95 and a04: "\<And>tvar. P3 (TVar tvar)" |
|
96 and a05: "\<And>char. P3 (TC char)" |
|
97 and a06: "\<And>ty1 ty2. \<lbrakk>P3 ty1; P3 ty2\<rbrakk> \<Longrightarrow> P3 (TApp ty1 ty2)" |
|
98 and a07: "\<And>char ty_lst. P4 ty_lst \<Longrightarrow> P3 (TFun char ty_lst)" |
|
99 and a08: "\<And>tvar tkind ty. \<lbrakk>P1 tkind; P3 ty\<rbrakk> \<Longrightarrow> P3 (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)" |
|
101 and a10: "P4 TsNil" |
|
102 and a11: "\<And>ty ty_lst. \<lbrakk>P3 ty; P4 ty_lst\<rbrakk> \<Longrightarrow> P4 (TsCons ty ty_lst)" |
|
103 and a12: "\<And>char. P5 (CC char)" |
|
104 and a13: "\<And>co1 co2. \<lbrakk>P5 co1; P5 co2\<rbrakk> \<Longrightarrow> P5 (CApp co1 co2)" |
|
105 and a14: "\<And>char co_lst. P6 co_lst \<Longrightarrow> P5 (CFun char co_lst)" |
|
106 and a15: "\<And>tvar ckind co. \<lbrakk>P2 ckind; P5 co\<rbrakk> \<Longrightarrow> P5 (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)" |
|
108 and a17: "\<And>co. P5 co \<Longrightarrow> P5 (CSym co)" |
|
109 and a18: "\<And>co1 co2. \<lbrakk>P5 co1; P5 co2\<rbrakk> \<Longrightarrow> P5 (CCir co1 co2)" |
|
110 and a19: "\<And>co. P5 co \<Longrightarrow> P5 (CLeft co)" |
|
111 and a20: "\<And>co. P5 co \<Longrightarrow> P5 (CRight co)" |
|
112 and a21: "\<And>co. P5 co \<Longrightarrow> P5 (CSim co)" |
|
113 and a22: "\<And>co. P5 co \<Longrightarrow> P5 (CRightc co)" |
|
114 and a23: "\<And>co. P5 co \<Longrightarrow> P5 (CLeftc co)" |
|
115 and a24: "\<And>co1 co2. \<lbrakk>P5 co1; P5 co2\<rbrakk> \<Longrightarrow> P5 (CCoe co1 co2)" |
|
116 and a25: "P6 CsNil" |
|
117 and a26: "\<And>co co_lst. \<lbrakk>P5 co; P6 co_lst\<rbrakk> \<Longrightarrow> P6 (CsCons co co_lst)" |
|
118 and a27: "\<And>var. P7 (Var var)" |
|
119 and a28: "\<And>char. P7 (C char)" |
|
120 and a29: "\<And>tvar tkind trm. \<lbrakk>P1 tkind; P7 trm\<rbrakk> \<Longrightarrow> P7 (LAMT tvar tkind trm)" |
|
121 and a30: "\<And>tvar ckind trm. \<lbrakk>P2 ckind; P7 trm\<rbrakk> \<Longrightarrow> P7 (LAMC tvar ckind trm)" |
|
122 and a31: "\<And>trm ty. \<lbrakk>P7 trm; P3 ty\<rbrakk> \<Longrightarrow> P7 (APP trm ty)" |
|
123 and a32: "\<And>var ty trm. \<lbrakk>P3 ty; P7 trm\<rbrakk> \<Longrightarrow> P7 (Lam var ty trm)" |
|
124 and a33: "\<And>trm1 trm2. \<lbrakk>P7 trm1; P7 trm2\<rbrakk> \<Longrightarrow> P7 (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)" |
|
126 and a35: "\<And>trm assoc_lst. \<lbrakk>P7 trm; P8 assoc_lst\<rbrakk> \<Longrightarrow> P7 (Case trm assoc_lst)" |
|
127 and a36: "\<And>trm ty. \<lbrakk>P7 trm; P3 ty\<rbrakk> \<Longrightarrow> P7 (Cast trm ty)" |
|
128 and a37: "P8 ANil" |
|
129 and a38: "\<And>pat trm assoc_lst. \<lbrakk>P9 pat; P7 trm; P8 assoc_lst\<rbrakk> \<Longrightarrow> P8 (ACons pat trm assoc_lst)" |
|
130 and a39: "\<And>char tvtk_lst tvck_lst vt_lst. \<lbrakk>P11 tvtk_lst; P12 tvck_lst; P10 vt_lst\<rbrakk> |
|
131 \<Longrightarrow> P9 (K char tvtk_lst tvck_lst vt_lst)" |
|
132 and a40: "P10 VTNil" |
|
133 and a41: "\<And>var ty vt_lst. \<lbrakk>P3 ty; P10 vt_lst\<rbrakk> \<Longrightarrow> P10 (VTCons var ty vt_lst)" |
|
134 and a42: "P11 TVTKNil" |
|
135 and a43: "\<And>tvar tkind tvtk_lst. \<lbrakk>P1 tkind; P11 tvtk_lst\<rbrakk> \<Longrightarrow> P11 (TVTKCons tvar tkind tvtk_lst)" |
|
136 and a44: "P12 TVCKNil" |
|
137 and a45: "\<And>tvar ckind tvck_lst. \<lbrakk>P2 ckind; P12 tvck_lst\<rbrakk> \<Longrightarrow> P12 (TVCKCons tvar ckind tvck_lst)" |
|
138 shows "P1 tkind \<and> P2 ckind \<and> P3 ty \<and> P4 ty_lst \<and> P5 co \<and> P6 co_lst \<and> |
|
139 P7 trm \<and> P8 assoc_lst \<and> P9 pat \<and> P10 vt_lst \<and> P11 tvtk_lst \<and> P12 tvck_lst" |
91 |
140 |
92 end |
141 end |
93 |
142 |
94 |
143 |
95 |
144 |