421 if get_STEPS lthy > 12 |
421 if get_STEPS lthy > 12 |
422 then raw_prove_trans (alpha_trms @ alpha_bn_trms) (raw_distinct_thms @ raw_inject_thms) |
422 then raw_prove_trans (alpha_trms @ alpha_bn_trms) (raw_distinct_thms @ raw_inject_thms) |
423 alpha_intros alpha_induct alpha_cases lthy6 |
423 alpha_intros alpha_induct alpha_cases lthy6 |
424 else raise TEST lthy6 |
424 else raise TEST lthy6 |
425 |
425 |
426 val alpha_equivp_thms = |
426 val (alpha_equivp_thms, alpha_bn_equivp_thms) = |
427 if get_STEPS lthy > 13 |
427 if get_STEPS lthy > 13 |
428 then raw_prove_equivp alpha_trms alpha_refl_thms alpha_sym_thms alpha_trans_thms lthy6 |
428 then raw_prove_equivp alpha_trms alpha_bn_trms alpha_refl_thms alpha_sym_thms |
|
429 alpha_trans_thms lthy6 |
429 else raise TEST lthy6 |
430 else raise TEST lthy6 |
430 |
431 |
431 (* proving alpha implies alpha_bn *) |
432 (* proving alpha implies alpha_bn *) |
432 val _ = warning "Proving alpha implies bn" |
433 val _ = warning "Proving alpha implies bn" |
433 |
434 |
448 val raw_constrs_rsp = raw_constrs_rsp raw_constrs alpha_trms alpha_intros |
449 val raw_constrs_rsp = raw_constrs_rsp raw_constrs alpha_trms alpha_intros |
449 (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 |
450 (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 |
450 |
451 |
451 val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt |
452 val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt |
452 |
453 |
|
454 val alpha_bn_rsp = raw_alpha_bn_rsp alpha_bn_equivp_thms alpha_bn_imp_thms |
|
455 |
453 (* noting the quot_respects lemmas *) |
456 (* noting the quot_respects lemmas *) |
454 val (_, lthy6a) = |
457 val (_, lthy6a) = |
455 if get_STEPS lthy > 15 |
458 if get_STEPS lthy > 15 |
456 then Local_Theory.note ((Binding.empty, [rsp_attrib]), |
459 then Local_Theory.note ((Binding.empty, [rsp_attrib]), |
457 raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp) lthy6 |
460 raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ alpha_bn_rsp) lthy6 |
458 else raise TEST lthy6 |
461 else raise TEST lthy6 |
459 |
462 |
460 (* defining the quotient type *) |
463 (* defining the quotient type *) |
461 val _ = warning "Declaring the quotient types" |
464 val _ = warning "Declaring the quotient types" |
462 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
465 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
532 ||>> Local_Theory.note ((@{binding "eq_iff_simps"}, []), alpha_eq_iff_simps) |
535 ||>> Local_Theory.note ((@{binding "eq_iff_simps"}, []), alpha_eq_iff_simps) |
533 ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) |
536 ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) |
534 ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) |
537 ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) |
535 ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) |
538 ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) |
536 ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) |
539 ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) |
|
540 ||>> Local_Theory.note ((@{binding "alpha_equivp"}, []), alpha_equivp_thms) |
537 |
541 |
538 val _ = |
542 val _ = |
539 if get_STEPS lthy > 20 |
543 if get_STEPS lthy > 20 |
540 then true else raise TEST lthy9' |
544 then true else raise TEST lthy9' |
541 |
545 |