538 |> lift_thms qtys [] raw_size_eqvt |
538 |> lift_thms qtys [] raw_size_eqvt |
539 ||>> lift_thms qtys [] [raw_induct_thm] |
539 ||>> lift_thms qtys [] [raw_induct_thm] |
540 ||>> lift_thms qtys [] raw_exhaust_thms |
540 ||>> lift_thms qtys [] raw_exhaust_thms |
541 else raise TEST lthyA |
541 else raise TEST lthyA |
542 |
542 |
543 (* Supports lemmas *) |
543 (* supports lemmas *) |
544 |
|
545 val qsupports_thms = |
544 val qsupports_thms = |
546 if get_STEPS lthy > 28 |
545 if get_STEPS lthy > 28 |
547 then prove_supports lthyB qperm_simps qtrms |
546 then prove_supports lthyB qperm_simps qtrms |
548 else raise TEST lthyB |
547 else raise TEST lthyB |
549 |
548 |
|
549 (* finite supp lemmas *) |
550 val qfsupp_thms = |
550 val qfsupp_thms = |
551 if get_STEPS lthy > 29 |
551 if get_STEPS lthy > 29 |
552 then prove_fsupp lthyB qtys qinduct qsupports_thms |
552 then prove_fsupp lthyB qtys qinduct qsupports_thms |
553 else raise TEST lthyB |
553 else raise TEST lthyB |
554 |
554 |
|
555 (* fs instances *) |
|
556 val lthyC = |
|
557 if get_STEPS lthy > 30 |
|
558 then fs_instance qtys qty_full_names tvs qfsupp_thms lthyB |
|
559 else raise TEST lthyB |
555 |
560 |
556 (* noting the theorems *) |
561 (* noting the theorems *) |
557 |
562 |
558 (* generating the prefix for the theorem names *) |
563 (* generating the prefix for the theorem names *) |
559 val thms_name = |
564 val thms_name = |
560 the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name |
565 the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name |
561 fun thms_suffix s = Binding.qualified true s thms_name |
566 fun thms_suffix s = Binding.qualified true s thms_name |
562 |
567 |
563 val (_, lthy9') = lthyB |
568 val (_, lthy9') = lthyC |
564 |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) |
569 |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) |
565 ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs) |
570 ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs) |
566 ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) |
571 ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) |
567 ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) |
572 ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) |
568 ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) |
573 ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) |