313 then define_raw_bns raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs |
313 then define_raw_bns raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs |
314 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3 |
314 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3 |
315 else raise TEST lthy3 |
315 else raise TEST lthy3 |
316 |
316 |
317 (* defining the permute_bn functions *) |
317 (* defining the permute_bn functions *) |
318 val (_, _, lthy3b) = |
318 val (raw_perm_bns, raw_perm_bn_simps, lthy3b) = |
319 if get_STEPS lthy3a > 2 |
319 if get_STEPS lthy3a > 2 |
320 then define_raw_bn_perms raw_tys raw_bn_info raw_cns_info |
320 then define_raw_bn_perms raw_tys raw_bn_info raw_cns_info |
321 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3a |
321 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3a |
322 else raise TEST lthy3a |
322 else raise TEST lthy3a |
323 |
323 |
445 val alpha_bn_rsp = |
445 val alpha_bn_rsp = |
446 if get_STEPS lthy > 20 |
446 if get_STEPS lthy > 20 |
447 then raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp_thms alpha_bn_imp_thms |
447 then raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp_thms alpha_bn_imp_thms |
448 else raise TEST lthy6 |
448 else raise TEST lthy6 |
449 |
449 |
|
450 val raw_perm_bn_rsp = |
|
451 if get_STEPS lthy > 21 |
|
452 then raw_perm_bn_rsp (alpha_trms @ alpha_bn_trms) raw_perm_bns alpha_induct |
|
453 alpha_intros raw_perm_bn_simps lthy6 |
|
454 else raise TEST lthy6 |
|
455 |
450 (* noting the quot_respects lemmas *) |
456 (* noting the quot_respects lemmas *) |
451 val (_, lthy6a) = |
457 val (_, lthy6a) = |
452 if get_STEPS lthy > 21 |
458 if get_STEPS lthy > 22 |
453 then Local_Theory.note ((Binding.empty, [rsp_attr]), |
459 then Local_Theory.note ((Binding.empty, [rsp_attr]), |
454 raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ alpha_bn_rsp) lthy6 |
460 raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ |
|
461 alpha_bn_rsp @ raw_perm_bn_rsp) lthy6 |
455 else raise TEST lthy6 |
462 else raise TEST lthy6 |
456 |
463 |
457 (* defining the quotient type *) |
464 (* defining the quotient type *) |
458 val _ = warning "Declaring the quotient types" |
465 val _ = warning "Declaring the quotient types" |
459 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
466 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
460 |
467 |
461 val (qty_infos, lthy7) = |
468 val (qty_infos, lthy7) = |
462 if get_STEPS lthy > 22 |
469 if get_STEPS lthy > 23 |
463 then define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a |
470 then define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a |
464 else raise TEST lthy6a |
471 else raise TEST lthy6a |
465 |
472 |
466 val qtys = map #qtyp qty_infos |
473 val qtys = map #qtyp qty_infos |
467 val qty_full_names = map (fst o dest_Type) qtys |
474 val qty_full_names = map (fst o dest_Type) qtys |
490 |
497 |
491 val qsize_descr = |
498 val qsize_descr = |
492 map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms |
499 map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms |
493 |
500 |
494 val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) = |
501 val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) = |
495 if get_STEPS lthy > 23 |
502 if get_STEPS lthy > 24 |
496 then |
503 then |
497 lthy7 |
504 lthy7 |
498 |> define_qconsts qtys qconstrs_descr |
505 |> define_qconsts qtys qconstrs_descr |
499 ||>> define_qconsts qtys qbns_descr |
506 ||>> define_qconsts qtys qbns_descr |
500 ||>> define_qconsts qtys qfvs_descr |
507 ||>> define_qconsts qtys qfvs_descr |
502 ||>> define_qconsts qtys qalpha_bns_descr |
509 ||>> define_qconsts qtys qalpha_bns_descr |
503 else raise TEST lthy7 |
510 else raise TEST lthy7 |
504 |
511 |
505 (* definition of the quotient permfunctions and pt-class *) |
512 (* definition of the quotient permfunctions and pt-class *) |
506 val lthy9 = |
513 val lthy9 = |
507 if get_STEPS lthy > 24 |
514 if get_STEPS lthy > 25 |
508 then define_qperms qtys qty_full_names tvs qperm_descr raw_perm_laws lthy8 |
515 then define_qperms qtys qty_full_names tvs qperm_descr raw_perm_laws lthy8 |
509 else raise TEST lthy8 |
516 else raise TEST lthy8 |
510 |
517 |
511 val lthy9a = |
518 val lthy9a = |
512 if get_STEPS lthy > 25 |
519 if get_STEPS lthy > 26 |
513 then define_qsizes qtys qty_full_names tvs qsize_descr lthy9 |
520 then define_qsizes qtys qty_full_names tvs qsize_descr lthy9 |
514 else raise TEST lthy9 |
521 else raise TEST lthy9 |
515 |
522 |
516 val qtrms = map #qconst qconstrs_info |
523 val qtrms = map #qconst qconstrs_info |
517 val qbns = map #qconst qbns_info |
524 val qbns = map #qconst qbns_info |
524 |
531 |
525 val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def |
532 val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def |
526 prod.cases} |
533 prod.cases} |
527 |
534 |
528 val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) = |
535 val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) = |
529 if get_STEPS lthy > 26 |
536 if get_STEPS lthy > 27 |
530 then |
537 then |
531 lthy9a |
538 lthy9a |
532 |> lift_thms qtys [] alpha_distincts |
539 |> lift_thms qtys [] alpha_distincts |
533 ||>> lift_thms qtys eq_iff_simps alpha_eq_iff |
540 ||>> lift_thms qtys eq_iff_simps alpha_eq_iff |
534 ||>> lift_thms qtys [] raw_fv_defs |
541 ||>> lift_thms qtys [] raw_fv_defs |
536 ||>> lift_thms qtys [] raw_perm_simps |
543 ||>> lift_thms qtys [] raw_perm_simps |
537 ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt) |
544 ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt) |
538 else raise TEST lthy9a |
545 else raise TEST lthy9a |
539 |
546 |
540 val ((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), lthyB) = |
547 val ((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), lthyB) = |
541 if get_STEPS lthy > 27 |
548 if get_STEPS lthy > 28 |
542 then |
549 then |
543 lthyA |
550 lthyA |
544 |> lift_thms qtys [] raw_size_eqvt |
551 |> lift_thms qtys [] raw_size_eqvt |
545 ||>> lift_thms qtys [] [raw_induct_thm] |
552 ||>> lift_thms qtys [] [raw_induct_thm] |
546 ||>> lift_thms qtys [] raw_exhaust_thms |
553 ||>> lift_thms qtys [] raw_exhaust_thms |
550 val qinducts = Project_Rule.projections lthyA qinduct |
557 val qinducts = Project_Rule.projections lthyA qinduct |
551 |
558 |
552 (* supports lemmas *) |
559 (* supports lemmas *) |
553 val _ = warning "Proving Supports Lemmas and fs-Instances" |
560 val _ = warning "Proving Supports Lemmas and fs-Instances" |
554 val qsupports_thms = |
561 val qsupports_thms = |
555 if get_STEPS lthy > 28 |
562 if get_STEPS lthy > 29 |
556 then prove_supports lthyB qperm_simps qtrms |
563 then prove_supports lthyB qperm_simps qtrms |
557 else raise TEST lthyB |
564 else raise TEST lthyB |
558 |
565 |
559 (* finite supp lemmas *) |
566 (* finite supp lemmas *) |
560 val qfsupp_thms = |
567 val qfsupp_thms = |
561 if get_STEPS lthy > 29 |
568 if get_STEPS lthy > 30 |
562 then prove_fsupp lthyB qtys qinduct qsupports_thms |
569 then prove_fsupp lthyB qtys qinduct qsupports_thms |
563 else raise TEST lthyB |
570 else raise TEST lthyB |
564 |
571 |
565 (* fs instances *) |
572 (* fs instances *) |
566 val lthyC = |
573 val lthyC = |
567 if get_STEPS lthy > 30 |
574 if get_STEPS lthy > 31 |
568 then fs_instance qtys qty_full_names tvs qfsupp_thms lthyB |
575 then fs_instance qtys qty_full_names tvs qfsupp_thms lthyB |
569 else raise TEST lthyB |
576 else raise TEST lthyB |
570 |
577 |
571 (* fv - supp equality *) |
578 (* fv - supp equality *) |
572 val _ = warning "Proving Equality between fv and supp" |
579 val _ = warning "Proving Equality between fv and supp" |
573 val qfv_supp_thms = |
580 val qfv_supp_thms = |
574 if get_STEPS lthy > 31 |
581 if get_STEPS lthy > 32 |
575 then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs |
582 then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs |
576 qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC |
583 qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC |
577 else [] |
584 else [] |
578 |
585 |
579 (* postprocessing of eq and fv theorems *) |
586 (* postprocessing of eq and fv theorems *) |