762 text {* Tactics for proving the lifted theorems *} |
762 text {* Tactics for proving the lifted theorems *} |
763 use "quotient_tacs.ML" |
763 use "quotient_tacs.ML" |
764 |
764 |
765 section {* Methods / Interface *} |
765 section {* Methods / Interface *} |
766 |
766 |
767 (* TODO inline *) |
|
768 ML {* |
|
769 fun mk_method1 tac thms ctxt = |
|
770 SIMPLE_METHOD (HEADGOAL (tac ctxt thms)) |
|
771 |
|
772 fun mk_method2 tac ctxt = |
|
773 SIMPLE_METHOD (HEADGOAL (tac ctxt)) |
|
774 *} |
|
775 |
|
776 method_setup lifting = |
767 method_setup lifting = |
777 {* Attrib.thms >> (mk_method1 Quotient_Tacs.lift_tac) *} |
768 {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *} |
778 {* lifts theorems to quotient types *} |
769 {* lifts theorems to quotient types *} |
779 |
770 |
780 method_setup lifting_setup = |
771 method_setup lifting_setup = |
781 {* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *} |
772 {* Attrib.thm >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.procedure_tac ctxt thms))) *} |
782 {* sets up the three goals for the quotient lifting procedure *} |
773 {* sets up the three goals for the quotient lifting procedure *} |
783 |
774 |
784 method_setup regularize = |
775 method_setup regularize = |
785 {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *} |
776 {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.regularize_tac ctxt))) *} |
786 {* proves the regularization goals from the quotient lifting procedure *} |
777 {* proves the regularization goals from the quotient lifting procedure *} |
787 |
778 |
788 method_setup injection = |
779 method_setup injection = |
789 {* Scan.succeed (mk_method2 Quotient_Tacs.all_injection_tac) *} |
780 {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.all_injection_tac ctxt))) *} |
790 {* proves the rep/abs injection goals from the quotient lifting procedure *} |
781 {* proves the rep/abs injection goals from the quotient lifting procedure *} |
791 |
782 |
792 method_setup cleaning = |
783 method_setup cleaning = |
793 {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *} |
784 {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.clean_tac ctxt))) *} |
794 {* proves the cleaning goals from the quotient lifting procedure *} |
785 {* proves the cleaning goals from the quotient lifting procedure *} |
795 |
786 |
796 attribute_setup quot_lifted = |
787 attribute_setup quot_lifted = |
797 {* Scan.succeed Quotient_Tacs.lifted_attrib *} |
788 {* Scan.succeed Quotient_Tacs.lifted_attrib *} |
798 {* lifts theorems to quotient types *} |
789 {* lifts theorems to quotient types *} |