equal
deleted
inserted
replaced
237 |
237 |
238 val alpha_tys = map (domain_type o fastype_of) alpha_trms |
238 val alpha_tys = map (domain_type o fastype_of) alpha_trms |
239 |
239 |
240 val _ = trace_msg (K "Proving distinct theorems...") |
240 val _ = trace_msg (K "Proving distinct theorems...") |
241 val alpha_distincts = |
241 val alpha_distincts = |
242 mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_tys |
242 mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_dt_names |
243 |
243 |
244 val _ = trace_msg (K "Proving eq-iff theorems...") |
244 val _ = trace_msg (K "Proving eq-iff theorems...") |
245 val alpha_eq_iff = |
245 val alpha_eq_iff = |
246 mk_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases |
246 mk_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases |
247 |
247 |
285 alpha_trans_thms lthy5 |
285 alpha_trans_thms lthy5 |
286 |
286 |
287 val _ = trace_msg (K "Proving alpha implies bn...") |
287 val _ = trace_msg (K "Proving alpha implies bn...") |
288 val alpha_bn_imp_thms = |
288 val alpha_bn_imp_thms = |
289 raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy5 |
289 raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy5 |
290 |
290 |
291 val _ = trace_msg (K "Proving respectfulness...") |
291 val _ = trace_msg (K "Proving respectfulness...") |
292 val raw_funs_rsp_aux = |
292 val raw_funs_rsp_aux = |
293 raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs |
293 raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs |
294 raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy5 |
294 raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy5 |
295 |
295 |