equal
deleted
inserted
replaced
8 imports Plain Hilbert_Choice Equiv_Relations Lifting |
8 imports Plain Hilbert_Choice Equiv_Relations Lifting |
9 keywords |
9 keywords |
10 "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and |
10 "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and |
11 "quotient_type" :: thy_goal and "/" and |
11 "quotient_type" :: thy_goal and "/" and |
12 "quotient_definition" :: thy_goal |
12 "quotient_definition" :: thy_goal |
13 uses |
|
14 ("Tools/Quotient/quotient_info.ML") |
|
15 ("Tools/Quotient/quotient_type.ML") |
|
16 ("Tools/Quotient/quotient_def.ML") |
|
17 ("Tools/Quotient/quotient_term.ML") |
|
18 ("Tools/Quotient/quotient_tacs.ML") |
|
19 begin |
13 begin |
20 |
14 |
21 text {* |
15 text {* |
22 Basic definition for equivalence relations |
16 Basic definition for equivalence relations |
23 that are represented by predicates. |
17 that are represented by predicates. |
763 |
757 |
764 subsection {* ML setup *} |
758 subsection {* ML setup *} |
765 |
759 |
766 text {* Auxiliary data for the quotient package *} |
760 text {* Auxiliary data for the quotient package *} |
767 |
761 |
768 use "Tools/Quotient/quotient_info.ML" |
762 ML_file "Tools/Quotient/quotient_info.ML" |
769 setup Quotient_Info.setup |
763 setup Quotient_Info.setup |
770 |
764 |
771 declare [[mapQ3 "fun" = (fun_rel, fun_quotient3)]] |
765 declare [[mapQ3 "fun" = (fun_rel, fun_quotient3)]] |
772 |
766 |
773 lemmas [quot_thm] = fun_quotient3 |
767 lemmas [quot_thm] = fun_quotient3 |
785 o_id |
779 o_id |
786 eq_comp_r |
780 eq_comp_r |
787 vimage_id |
781 vimage_id |
788 |
782 |
789 text {* Translation functions for the lifting process. *} |
783 text {* Translation functions for the lifting process. *} |
790 use "Tools/Quotient/quotient_term.ML" |
784 ML_file "Tools/Quotient/quotient_term.ML" |
791 |
785 |
792 |
786 |
793 text {* Definitions of the quotient types. *} |
787 text {* Definitions of the quotient types. *} |
794 use "Tools/Quotient/quotient_type.ML" |
788 ML_file "Tools/Quotient/quotient_type.ML" |
795 |
789 |
796 |
790 |
797 text {* Definitions for quotient constants. *} |
791 text {* Definitions for quotient constants. *} |
798 use "Tools/Quotient/quotient_def.ML" |
792 ML_file "Tools/Quotient/quotient_def.ML" |
799 |
793 |
800 |
794 |
801 text {* |
795 text {* |
802 An auxiliary constant for recording some information |
796 An auxiliary constant for recording some information |
803 about the lifted theorem in a tactic. |
797 about the lifted theorem in a tactic. |
818 lemma QT_imp: "Quot_True a \<equiv> Quot_True b" |
812 lemma QT_imp: "Quot_True a \<equiv> Quot_True b" |
819 by (simp add: Quot_True_def) |
813 by (simp add: Quot_True_def) |
820 |
814 |
821 |
815 |
822 text {* Tactics for proving the lifted theorems *} |
816 text {* Tactics for proving the lifted theorems *} |
823 use "Tools/Quotient/quotient_tacs.ML" |
817 ML_file "Tools/Quotient/quotient_tacs.ML" |
824 |
818 |
825 subsection {* Methods / Interface *} |
819 subsection {* Methods / Interface *} |
826 |
820 |
827 method_setup lifting = |
821 method_setup lifting = |
828 {* Attrib.thms >> (fn thms => fn ctxt => |
822 {* Attrib.thms >> (fn thms => fn ctxt => |