436 val alpha_bn_imp_thms = |
436 val alpha_bn_imp_thms = |
437 if get_STEPS lthy > 14 |
437 if get_STEPS lthy > 14 |
438 then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6 |
438 then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6 |
439 else raise TEST lthy6 |
439 else raise TEST lthy6 |
440 |
440 |
441 (* auxiliary lemmas for respectfulness proofs *) |
441 (* respectfulness proofs *) |
442 val raw_funs_rsp = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs |
442 val raw_funs_rsp_aux = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs |
443 raw_bns raw_fv_bns alpha_induct (raw_bn_eqs @ raw_fv_defs) lthy6 |
443 raw_bns raw_fv_bns alpha_induct (raw_bn_eqs @ raw_fv_defs) lthy6 |
|
444 val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux |
444 |
445 |
445 val raw_size_rsp = raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct |
446 val raw_size_rsp = raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct |
446 (raw_size_thms @ raw_size_eqvt) lthy6 |
447 (raw_size_thms @ raw_size_eqvt) lthy6 |
|
448 |> map mk_funs_rsp |
447 |
449 |
448 val raw_constrs_rsp = raw_constrs_rsp all_raw_constrs alpha_trms alpha_intros |
450 val raw_constrs_rsp = raw_constrs_rsp all_raw_constrs alpha_trms alpha_intros |
449 (alpha_bn_imp_thms @ raw_funs_rsp) lthy6 |
451 (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 |
|
452 |
|
453 val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt |
450 |
454 |
451 (* defining the quotient type *) |
455 (* defining the quotient type *) |
452 val _ = warning "Declaring the quotient types" |
456 val _ = warning "Declaring the quotient types" |
453 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
457 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
454 val qty_binds = map (fn (_, bind, _, _) => bind) dts |
458 val qty_binds = map (fn (_, bind, _, _) => bind) dts |
506 ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) |
510 ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) |
507 ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) |
511 ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) |
508 ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) |
512 ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) |
509 ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) |
513 ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) |
510 ||>> Local_Theory.note ((@{binding "funs_rsp"}, []), raw_funs_rsp) |
514 ||>> Local_Theory.note ((@{binding "funs_rsp"}, []), raw_funs_rsp) |
511 ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), raw_size_eqvt) |
|
512 ||>> Local_Theory.note ((@{binding "size_simps"}, []), raw_size_thms) |
|
513 ||>> Local_Theory.note ((@{binding "size_rsp"}, []), raw_size_rsp) |
515 ||>> Local_Theory.note ((@{binding "size_rsp"}, []), raw_size_rsp) |
514 ||>> Local_Theory.note ((@{binding "constrs_rsp"}, []), raw_constrs_rsp) |
516 ||>> Local_Theory.note ((@{binding "constrs_rsp"}, []), raw_constrs_rsp) |
515 ||>> Local_Theory.note ((@{binding "alpha_sym_thms"}, []), alpha_sym_thms) |
517 ||>> Local_Theory.note ((@{binding "permute_rsp"}, []), alpha_permute_rsp) |
516 ||>> Local_Theory.note ((@{binding "alpha_trans_thms"}, []), alpha_trans_thms) |
518 |
517 |
|
518 val _ = |
519 val _ = |
519 if get_STEPS lthy > 17 |
520 if get_STEPS lthy > 17 |
520 then true else raise TEST lthy8' |
521 then true else raise TEST lthy8' |
521 |
522 |
522 (* old stuff *) |
523 (* old stuff *) |