1 (* Title: HOL/Quotient.thy |
1 (* Title: HOL/Quotient.thy |
2 Author: Cezary Kaliszyk and Christian Urban |
2 Author: Cezary Kaliszyk and Christian Urban |
3 *) |
3 *) |
4 |
4 |
5 section {* Definition of Quotient Types *} |
5 section \<open>Definition of Quotient Types\<close> |
6 |
6 |
7 theory Quotient |
7 theory Quotient |
8 imports Lifting |
8 imports 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 begin |
13 begin |
14 |
14 |
15 text {* |
15 text \<open> |
16 Basic definition for equivalence relations |
16 Basic definition for equivalence relations |
17 that are represented by predicates. |
17 that are represented by predicates. |
18 *} |
18 \<close> |
19 |
19 |
20 text {* Composition of Relations *} |
20 text \<open>Composition of Relations\<close> |
21 |
21 |
22 abbreviation |
22 abbreviation |
23 rel_conj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" (infixr "OOO" 75) |
23 rel_conj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" (infixr "OOO" 75) |
24 where |
24 where |
25 "r1 OOO r2 \<equiv> r1 OO r2 OO r1" |
25 "r1 OOO r2 \<equiv> r1 OO r2 OO r1" |
190 shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)" |
190 shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)" |
191 unfolding fun_eq_iff |
191 unfolding fun_eq_iff |
192 using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] |
192 using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] |
193 by simp |
193 by simp |
194 |
194 |
195 text{* |
195 text\<open> |
196 In the following theorem R1 can be instantiated with anything, |
196 In the following theorem R1 can be instantiated with anything, |
197 but we know some of the types of the Rep and Abs functions; |
197 but we know some of the types of the Rep and Abs functions; |
198 so by solving Quotient assumptions we can get a unique R1 that |
198 so by solving Quotient assumptions we can get a unique R1 that |
199 will be provable; which is why we need to use @{text apply_rsp} and |
199 will be provable; which is why we need to use @{text apply_rsp} and |
200 not the primed version *} |
200 not the primed version\<close> |
201 |
201 |
202 lemma apply_rspQ3: |
202 lemma apply_rspQ3: |
203 fixes f g::"'a \<Rightarrow> 'c" |
203 fixes f g::"'a \<Rightarrow> 'c" |
204 assumes q: "Quotient3 R1 Abs1 Rep1" |
204 assumes q: "Quotient3 R1 Abs1 Rep1" |
205 and a: "(R1 ===> R2) f g" "R1 x y" |
205 and a: "(R1 ===> R2) f g" "R1 x y" |
603 show x: "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)" proof - |
603 show x: "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)" proof - |
604 obtain x where r: "R x x" and rep: "Rep a = Collect (R x)" using rep_prop[of a] by auto |
604 obtain x where r: "R x x" and rep: "Rep a = Collect (R x)" using rep_prop[of a] by auto |
605 have "R (SOME x. x \<in> Rep a) x" using r rep some_collect by metis |
605 have "R (SOME x. x \<in> Rep a) x" using r rep some_collect by metis |
606 then have "R x (SOME x. x \<in> Rep a)" using part_equivp_symp[OF equivp] by fast |
606 then have "R x (SOME x. x \<in> Rep a)" using part_equivp_symp[OF equivp] by fast |
607 then show "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)" |
607 then show "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)" |
608 using part_equivp_transp[OF equivp] by (metis `R (SOME x. x \<in> Rep a) x`) |
608 using part_equivp_transp[OF equivp] by (metis \<open>R (SOME x. x \<in> Rep a) x\<close>) |
609 qed |
609 qed |
610 have "Collect (R (SOME x. x \<in> Rep a)) = (Rep a)" by (metis some_collect rep_prop) |
610 have "Collect (R (SOME x. x \<in> Rep a)) = (Rep a)" by (metis some_collect rep_prop) |
611 then show "Abs (Collect (R (SOME x. x \<in> Rep a))) = a" using rep_inverse by auto |
611 then show "Abs (Collect (R (SOME x. x \<in> Rep a))) = a" using rep_inverse by auto |
612 have "R r r \<Longrightarrow> R s s \<Longrightarrow> Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s" |
612 have "R r r \<Longrightarrow> R s s \<Longrightarrow> Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s" |
613 proof - |
613 proof - |
742 show "R r s = (R r r \<and> R s s \<and> Abs r = Abs s)" using q by(rule Quotient3_rel[symmetric]) |
742 show "R r s = (R r r \<and> R s s \<and> Abs r = Abs s)" using q by(rule Quotient3_rel[symmetric]) |
743 next |
743 next |
744 show "T = (\<lambda>x y. R x x \<and> Abs x = y)" using T_def equivp_reflp[OF eR] by simp |
744 show "T = (\<lambda>x y. R x x \<and> Abs x = y)" using T_def equivp_reflp[OF eR] by simp |
745 qed |
745 qed |
746 |
746 |
747 subsection {* ML setup *} |
747 subsection \<open>ML setup\<close> |
748 |
748 |
749 text {* Auxiliary data for the quotient package *} |
749 text \<open>Auxiliary data for the quotient package\<close> |
750 |
750 |
751 named_theorems quot_equiv "equivalence relation theorems" |
751 named_theorems quot_equiv "equivalence relation theorems" |
752 and quot_respect "respectfulness theorems" |
752 and quot_respect "respectfulness theorems" |
753 and quot_preserve "preservation theorems" |
753 and quot_preserve "preservation theorems" |
754 and id_simps "identity simp rules for maps" |
754 and id_simps "identity simp rules for maps" |
761 lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp |
761 lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp |
762 lemmas [quot_preserve] = if_prs o_prs let_prs id_prs |
762 lemmas [quot_preserve] = if_prs o_prs let_prs id_prs |
763 lemmas [quot_equiv] = identity_equivp |
763 lemmas [quot_equiv] = identity_equivp |
764 |
764 |
765 |
765 |
766 text {* Lemmas about simplifying id's. *} |
766 text \<open>Lemmas about simplifying id's.\<close> |
767 lemmas [id_simps] = |
767 lemmas [id_simps] = |
768 id_def[symmetric] |
768 id_def[symmetric] |
769 map_fun_id |
769 map_fun_id |
770 id_apply |
770 id_apply |
771 id_o |
771 id_o |
772 o_id |
772 o_id |
773 eq_comp_r |
773 eq_comp_r |
774 vimage_id |
774 vimage_id |
775 |
775 |
776 text {* Translation functions for the lifting process. *} |
776 text \<open>Translation functions for the lifting process.\<close> |
777 ML_file "Tools/Quotient/quotient_term.ML" |
777 ML_file "Tools/Quotient/quotient_term.ML" |
778 |
778 |
779 |
779 |
780 text {* Definitions of the quotient types. *} |
780 text \<open>Definitions of the quotient types.\<close> |
781 ML_file "Tools/Quotient/quotient_type.ML" |
781 ML_file "Tools/Quotient/quotient_type.ML" |
782 |
782 |
783 |
783 |
784 text {* Definitions for quotient constants. *} |
784 text \<open>Definitions for quotient constants.\<close> |
785 ML_file "Tools/Quotient/quotient_def.ML" |
785 ML_file "Tools/Quotient/quotient_def.ML" |
786 |
786 |
787 |
787 |
788 text {* |
788 text \<open> |
789 An auxiliary constant for recording some information |
789 An auxiliary constant for recording some information |
790 about the lifted theorem in a tactic. |
790 about the lifted theorem in a tactic. |
791 *} |
791 \<close> |
792 definition |
792 definition |
793 Quot_True :: "'a \<Rightarrow> bool" |
793 Quot_True :: "'a \<Rightarrow> bool" |
794 where |
794 where |
795 "Quot_True x \<longleftrightarrow> True" |
795 "Quot_True x \<longleftrightarrow> True" |
796 |
796 |
807 |
807 |
808 context |
808 context |
809 begin |
809 begin |
810 interpretation lifting_syntax . |
810 interpretation lifting_syntax . |
811 |
811 |
812 text {* Tactics for proving the lifted theorems *} |
812 text \<open>Tactics for proving the lifted theorems\<close> |
813 ML_file "Tools/Quotient/quotient_tacs.ML" |
813 ML_file "Tools/Quotient/quotient_tacs.ML" |
814 |
814 |
815 end |
815 end |
816 |
816 |
817 subsection {* Methods / Interface *} |
817 subsection \<open>Methods / Interface\<close> |
818 |
818 |
819 method_setup lifting = |
819 method_setup lifting = |
820 {* Attrib.thms >> (fn thms => fn ctxt => |
820 \<open>Attrib.thms >> (fn thms => fn ctxt => |
821 SIMPLE_METHOD' (Quotient_Tacs.lift_tac ctxt [] thms)) *} |
821 SIMPLE_METHOD' (Quotient_Tacs.lift_tac ctxt [] thms))\<close> |
822 {* lift theorems to quotient types *} |
822 \<open>lift theorems to quotient types\<close> |
823 |
823 |
824 method_setup lifting_setup = |
824 method_setup lifting_setup = |
825 {* Attrib.thm >> (fn thm => fn ctxt => |
825 \<open>Attrib.thm >> (fn thm => fn ctxt => |
826 SIMPLE_METHOD' (Quotient_Tacs.lift_procedure_tac ctxt [] thm)) *} |
826 SIMPLE_METHOD' (Quotient_Tacs.lift_procedure_tac ctxt [] thm))\<close> |
827 {* set up the three goals for the quotient lifting procedure *} |
827 \<open>set up the three goals for the quotient lifting procedure\<close> |
828 |
828 |
829 method_setup descending = |
829 method_setup descending = |
830 {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_tac ctxt [])) *} |
830 \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_tac ctxt []))\<close> |
831 {* decend theorems to the raw level *} |
831 \<open>decend theorems to the raw level\<close> |
832 |
832 |
833 method_setup descending_setup = |
833 method_setup descending_setup = |
834 {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_procedure_tac ctxt [])) *} |
834 \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_procedure_tac ctxt []))\<close> |
835 {* set up the three goals for the decending theorems *} |
835 \<open>set up the three goals for the decending theorems\<close> |
836 |
836 |
837 method_setup partiality_descending = |
837 method_setup partiality_descending = |
838 {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_tac ctxt [])) *} |
838 \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_tac ctxt []))\<close> |
839 {* decend theorems to the raw level *} |
839 \<open>decend theorems to the raw level\<close> |
840 |
840 |
841 method_setup partiality_descending_setup = |
841 method_setup partiality_descending_setup = |
842 {* Scan.succeed (fn ctxt => |
842 \<open>Scan.succeed (fn ctxt => |
843 SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_procedure_tac ctxt [])) *} |
843 SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_procedure_tac ctxt []))\<close> |
844 {* set up the three goals for the decending theorems *} |
844 \<open>set up the three goals for the decending theorems\<close> |
845 |
845 |
846 method_setup regularize = |
846 method_setup regularize = |
847 {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.regularize_tac ctxt)) *} |
847 \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.regularize_tac ctxt))\<close> |
848 {* prove the regularization goals from the quotient lifting procedure *} |
848 \<open>prove the regularization goals from the quotient lifting procedure\<close> |
849 |
849 |
850 method_setup injection = |
850 method_setup injection = |
851 {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.all_injection_tac ctxt)) *} |
851 \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.all_injection_tac ctxt))\<close> |
852 {* prove the rep/abs injection goals from the quotient lifting procedure *} |
852 \<open>prove the rep/abs injection goals from the quotient lifting procedure\<close> |
853 |
853 |
854 method_setup cleaning = |
854 method_setup cleaning = |
855 {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.clean_tac ctxt)) *} |
855 \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.clean_tac ctxt))\<close> |
856 {* prove the cleaning goals from the quotient lifting procedure *} |
856 \<open>prove the cleaning goals from the quotient lifting procedure\<close> |
857 |
857 |
858 attribute_setup quot_lifted = |
858 attribute_setup quot_lifted = |
859 {* Scan.succeed Quotient_Tacs.lifted_attrib *} |
859 \<open>Scan.succeed Quotient_Tacs.lifted_attrib\<close> |
860 {* lift theorems to quotient types *} |
860 \<open>lift theorems to quotient types\<close> |
861 |
861 |
862 no_notation |
862 no_notation |
863 rel_conj (infixr "OOO" 75) |
863 rel_conj (infixr "OOO" 75) |
864 |
864 |
865 end |
865 end |