434 if get_STEPS lthy > 11 |
434 if get_STEPS lthy > 11 |
435 then raw_prove_trans (alpha_trms @ alpha_bn_trms) (distinct_thms @ inject_thms) |
435 then raw_prove_trans (alpha_trms @ alpha_bn_trms) (distinct_thms @ inject_thms) |
436 alpha_intros alpha_induct alpha_cases lthy_tmp'' |
436 alpha_intros alpha_induct alpha_cases lthy_tmp'' |
437 else raise TEST lthy4 |
437 else raise TEST lthy4 |
438 |
438 |
|
439 (* proving alpha implies alpha_bn *) |
|
440 val _ = warning "Proving alpha implies bn" |
|
441 |
|
442 val alpha_bn_imp_thms = |
|
443 if get_STEPS lthy > 12 |
|
444 then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy_tmp'' |
|
445 else raise TEST lthy4 |
|
446 |
439 |
447 |
440 val _ = tracing ("alphas " ^ commas (map (Syntax.string_of_term lthy4) alpha_trms)) |
448 val _ = tracing ("alphas " ^ commas (map (Syntax.string_of_term lthy4) alpha_trms)) |
441 val _ = tracing ("alpha_bns " ^ commas (map (Syntax.string_of_term lthy4) alpha_bn_trms)) |
449 val _ = tracing ("alpha_bns " ^ commas (map (Syntax.string_of_term lthy4) alpha_bn_trms)) |
442 val _ = tracing ("alpha_refl\n" ^ |
450 val _ = tracing ("alpha_refl\n" ^ |
443 cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_refl_thms)) |
451 cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_refl_thms)) |
|
452 val _ = tracing ("alpha_bn_imp\n" ^ |
|
453 cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_bn_imp_thms)) |
444 |
454 |
445 val _ = |
455 val _ = |
446 if get_STEPS lthy > 12 |
456 if get_STEPS lthy > 13 |
447 then true else raise TEST lthy4 |
457 then true else raise TEST lthy4 |
448 |
458 |
449 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
459 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
450 val bns = raw_bn_funs ~~ bn_nos; |
460 val bns = raw_bn_funs ~~ bn_nos; |
451 |
461 |