326 val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt |
326 val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt |
327 |
327 |
328 val alpha_bn_rsp = |
328 val alpha_bn_rsp = |
329 raw_alpha_bn_rsp alpha_result alpha_bn_equivp_thms alpha_bn_imp_thms |
329 raw_alpha_bn_rsp alpha_result alpha_bn_equivp_thms alpha_bn_imp_thms |
330 |
330 |
331 val raw_perm_bn_rsp =raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps |
331 val raw_perm_bn_rsp = raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps |
332 |
332 |
333 (* noting the quot_respects lemmas *) |
333 (* noting the quot_respects lemmas *) |
334 val (_, lthy6) = |
334 val (_, lthy6) = |
335 Local_Theory.note ((Binding.empty, [rsp_attr]), |
335 Local_Theory.note ((Binding.empty, [rsp_attr]), |
336 raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ |
336 raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ |
406 val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def |
406 val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def |
407 prod.cases} |
407 prod.cases} |
408 |
408 |
409 val ([ qdistincts, qeq_iffs, qfv_defs, qbn_defs, qperm_simps, qfv_qbn_eqvts, |
409 val ([ qdistincts, qeq_iffs, qfv_defs, qbn_defs, qperm_simps, qfv_qbn_eqvts, |
410 qbn_inducts, qsize_eqvt, [qinduct], qexhausts, qsize_simps, qperm_bn_simps, |
410 qbn_inducts, qsize_eqvt, [qinduct], qexhausts, qsize_simps, qperm_bn_simps, |
411 qalpha_refl_thms ], lthyB) = |
411 qalpha_refl_thms, qalpha_sym_thms, qalpha_trans_thms ], lthyB) = |
412 lthy9a |
412 lthy9a |
413 |>>> lift_thms qtys [] alpha_distincts |
413 |>>> lift_thms qtys [] alpha_distincts |
414 ||>>> lift_thms qtys eq_iff_simps alpha_eq_iff |
414 ||>>> lift_thms qtys eq_iff_simps alpha_eq_iff |
415 ||>>> lift_thms qtys [] raw_fv_defs |
415 ||>>> lift_thms qtys [] raw_fv_defs |
416 ||>>> lift_thms qtys [] raw_bn_defs |
416 ||>>> lift_thms qtys [] raw_bn_defs |
421 ||>>> lift_thms qtys [] [raw_induct_thm] |
421 ||>>> lift_thms qtys [] [raw_induct_thm] |
422 ||>>> lift_thms qtys [] raw_exhaust_thms |
422 ||>>> lift_thms qtys [] raw_exhaust_thms |
423 ||>>> lift_thms qtys [] raw_size_thms |
423 ||>>> lift_thms qtys [] raw_size_thms |
424 ||>>> lift_thms qtys [] raw_perm_bn_simps |
424 ||>>> lift_thms qtys [] raw_perm_bn_simps |
425 ||>>> lift_thms qtys [] alpha_refl_thms |
425 ||>>> lift_thms qtys [] alpha_refl_thms |
|
426 ||>>> lift_thms qtys [] alpha_sym_thms |
|
427 ||>>> lift_thms qtys [] alpha_trans_thms |
426 |
428 |
427 val qinducts = Project_Rule.projections lthyB qinduct |
429 val qinducts = Project_Rule.projections lthyB qinduct |
428 |
430 |
429 val _ = trace_msg (K "Proving supp lemmas and fs-instances...") |
431 val _ = trace_msg (K "Proving supp lemmas and fs-instances...") |
430 val qsupports_thms = prove_supports lthyB qperm_simps (flat qtrms) |
432 val qsupports_thms = prove_supports lthyB qperm_simps (flat qtrms) |
510 ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs) |
512 ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs) |
511 ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps) |
513 ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps) |
512 ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms) |
514 ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms) |
513 ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms) |
515 ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms) |
514 ||>> Local_Theory.note ((thms_suffix "permute_bn", []), qpermute_bn_thms) |
516 ||>> Local_Theory.note ((thms_suffix "permute_bn", []), qpermute_bn_thms) |
|
517 ||>> Local_Theory.note ((thms_suffix "alpha_refl", []), qalpha_refl_thms) |
|
518 ||>> Local_Theory.note ((thms_suffix "alpha_sym", []), qalpha_sym_thms) |
|
519 ||>> Local_Theory.note ((thms_suffix "alpha_trans", []), qalpha_trans_thms) |
|
520 |
515 in |
521 in |
516 lthy9' |
522 lthy9' |
517 end |
523 end |
518 *} |
524 *} |
519 |
525 |