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 |
444 |
445 val raw_size_rsp = raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct |
445 val raw_size_rsp = raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct |
446 (raw_size_thms @ raw_size_eqvt) lthy6 |
446 (raw_size_thms @ raw_size_eqvt) lthy6 |
447 |
447 |
|
448 val raw_constrs_rsp = raw_constrs_rsp all_raw_constrs alpha_trms alpha_intros |
|
449 (alpha_bn_imp_thms @ raw_funs_rsp) lthy6 |
448 |
450 |
449 (* defining the quotient type *) |
451 (* defining the quotient type *) |
450 val _ = warning "Declaring the quotient types" |
452 val _ = warning "Declaring the quotient types" |
451 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
453 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
452 val qty_binds = map (fn (_, bind, _, _) => bind) dts |
454 val qty_binds = map (fn (_, bind, _, _) => bind) dts |
507 ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) |
509 ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) |
508 ||>> Local_Theory.note ((@{binding "funs_rsp"}, []), raw_funs_rsp) |
510 ||>> Local_Theory.note ((@{binding "funs_rsp"}, []), raw_funs_rsp) |
509 ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), raw_size_eqvt) |
511 ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), raw_size_eqvt) |
510 ||>> Local_Theory.note ((@{binding "size_simps"}, []), raw_size_thms) |
512 ||>> Local_Theory.note ((@{binding "size_simps"}, []), raw_size_thms) |
511 ||>> Local_Theory.note ((@{binding "size_rsp"}, []), raw_size_rsp) |
513 ||>> Local_Theory.note ((@{binding "size_rsp"}, []), raw_size_rsp) |
|
514 ||>> Local_Theory.note ((@{binding "constrs_rsp"}, []), raw_constrs_rsp) |
512 ||>> Local_Theory.note ((@{binding "alpha_sym_thms"}, []), alpha_sym_thms) |
515 ||>> Local_Theory.note ((@{binding "alpha_sym_thms"}, []), alpha_sym_thms) |
513 ||>> Local_Theory.note ((@{binding "alpha_trans_thms"}, []), alpha_trans_thms) |
516 ||>> Local_Theory.note ((@{binding "alpha_trans_thms"}, []), alpha_trans_thms) |
514 |
517 |
515 val _ = |
518 val _ = |
516 if get_STEPS lthy > 17 |
519 if get_STEPS lthy > 17 |