equal
deleted
inserted
replaced
884 A user of our quotient package first needs to define a relation on |
884 A user of our quotient package first needs to define a relation on |
885 the raw type, by which the quotienting will be performed. We give |
885 the raw type, by which the quotienting will be performed. We give |
886 the same integer relation as the one presented in the introduction: |
886 the same integer relation as the one presented in the introduction: |
887 |
887 |
888 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % |
888 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % |
889 \isacommand{fun}~~@{text "\<approx>"}~~\isacommand{where}~~@{text "(m \<Colon> nat, n) \<approx> (p, q) = (m + q = n + p)"} |
889 \isacommand{fun}~~@{text "int_rel"}~~\isacommand{where}~~@{text "(m \<Colon> nat, n) int_rel (p, q) = (m + q = n + p)"} |
890 \end{isabelle} |
890 \end{isabelle} |
891 |
891 |
892 \noindent |
892 \noindent |
893 Next the quotient type is defined. This leaves a proof obligation that the |
893 Next the quotient type is defined. This leaves a proof obligation that the |
894 relation is an equivalence relation which is solved automatically using the |
894 relation is an equivalence relation which is solved automatically using the |
895 definitions: |
895 definitions: |
896 |
896 |
897 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % |
897 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % |
898 \isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \<times> nat)"}~~\isacommand{/}~~@{text "\<approx>"} |
898 \isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \<times> nat)"}~~\isacommand{/}~~@{text "int_rel"} |
899 \end{isabelle} |
899 \end{isabelle} |
900 |
900 |
901 \noindent |
901 \noindent |
902 The user can then specify the constants on the quotient type: |
902 The user can then specify the constants on the quotient type: |
903 |
903 |
911 |
911 |
912 \noindent |
912 \noindent |
913 Lets first take a simple theorem about addition on the raw level: |
913 Lets first take a simple theorem about addition on the raw level: |
914 |
914 |
915 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % |
915 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % |
916 \isacommand{lemma}~~@{text "plus_zero_raw: plus_raw (0, 0) x \<approx> x"} |
916 \isacommand{lemma}~~@{text "plus_zero_raw: int_rel (plus_raw (0, 0) x) x"} |
917 \end{isabelle} |
917 \end{isabelle} |
918 |
918 |
919 \noindent |
919 \noindent |
920 When the user tries to lift a theorem about integer addition, the respectfulness |
920 When the user tries to lift a theorem about integer addition, the respectfulness |
921 proof obligation is left, so let us prove it first: |
921 proof obligation is left, so let us prove it first: |
922 |
922 |
923 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % |
923 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % |
924 \isacommand{lemma}~~@{text "[quot_respect]: (op \<approx> \<Longrightarrow> op \<approx> \<Longrightarrow> op \<approx>) plus_raw plus_raw"} |
924 \isacommand{lemma}~~@{text "[quot_respect]: (int_rel \<Longrightarrow> int_rel \<Longrightarrow> int_rel) plus_raw plus_raw"} |
925 \end{isabelle} |
925 \end{isabelle} |
926 |
926 |
927 \noindent |
927 \noindent |
928 Can be proved automatically by the system just by unfolding the definition |
928 Can be proved automatically by the system just by unfolding the definition |
929 of @{text "op \<Longrightarrow>"}. |
929 of @{text "op \<Longrightarrow>"}. |