equal
deleted
inserted
replaced
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 (* can lift *) |
88 (* can lift *) |
89 thm distinct |
89 thm distinct |
90 thm fv_defs |
90 thm fv_defs |
|
91 thm alpha_bn_imps alpha_equivp |
91 |
92 |
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 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_simps |
94 thm perm_laws |
95 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 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) |
126 |
127 |
127 ML {* |
128 ML {* |
128 val thms_f = map (lift_thm qtys @{context}) @{thms perm_laws} |
129 val thms_f = map (lift_thm qtys @{context}) @{thms perm_laws} |
129 *} |
130 *} |
130 |
131 |
131 |
132 ML {* |
|
133 val thms_e = map (lift_thm qtys @{context}) |
|
134 @{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps |
|
135 prod.cases]} |
|
136 *} |
132 |
137 |
133 |
138 |
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) |
139 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) |
135 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] |
140 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] |
136 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm |
141 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm |