83 | "bv_tvs TvsNil = []" |
83 | "bv_tvs TvsNil = []" |
84 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" |
84 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" |
85 | "bv_cvs CvsNil = []" |
85 | "bv_cvs CvsNil = []" |
86 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" |
86 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" |
87 |
87 |
88 |
88 (* can lift *) |
89 thm distinct |
89 thm distinct |
90 |
90 thm fv_defs |
91 term TvsNil |
91 |
|
92 thm tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.inducts |
|
93 thm perm_simps |
|
94 thm perm_laws |
|
95 thm tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.size(50 - 98) |
|
96 |
|
97 (* cannot lift yet *) |
|
98 thm eq_iff |
|
99 thm eq_iff_simps |
|
100 |
|
101 ML {* |
|
102 val qtys = [@{typ tkind}, @{typ ckind}, @{typ ty}, @{typ ty_lst}, @{typ co}, |
|
103 @{typ co_lst}, @{typ trm}, @{typ assoc_lst}, @{typ pat}, @{typ vars}, |
|
104 @{typ tvars}, @{typ cvars}] |
|
105 *} |
|
106 |
|
107 ML {* |
|
108 val thms_d = map (lift_thm qtys @{context}) @{thms distinct} |
|
109 *} |
|
110 |
|
111 ML {* |
|
112 val thms_i = map (lift_thm qtys @{context}) @{thms tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.inducts} |
|
113 *} |
|
114 |
|
115 ML {* |
|
116 val thms_f = map (lift_thm qtys @{context}) @{thms fv_defs} |
|
117 *} |
|
118 |
|
119 ML {* |
|
120 val thms_i = map (lift_thm qtys @{context}) @{thms tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.size(50 - 98)} |
|
121 *} |
|
122 |
|
123 ML {* |
|
124 val thms_p = map (lift_thm qtys @{context}) @{thms perm_simps} |
|
125 *} |
|
126 |
|
127 ML {* |
|
128 val thms_f = map (lift_thm qtys @{context}) @{thms perm_laws} |
|
129 *} |
|
130 |
|
131 |
92 |
132 |
93 |
133 |
94 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) |
134 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) |
95 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] |
135 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] |
96 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm |
136 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm |