873 (* Mention why equivalence *) |
873 (* Mention why equivalence *) |
874 |
874 |
875 text {* |
875 text {* |
876 |
876 |
877 In this section we will show, a complete interaction with the quotient package |
877 In this section we will show, a complete interaction with the quotient package |
878 for lifting a theorem about integers. A user of our quotient package first |
878 for defining the type of integers by quotienting pairs of natural numbers and |
879 needs to define a relation on the raw type, by which the quotienting will be |
879 lifting theorems to integers. Our quotient package is fully compatible with |
880 performed. We give the same integer relation as the one presented in the |
880 Isabelle type classes, but for clarity we will not use them in this example. |
881 introduction: |
881 In a larger formalization of integers using the type class mechanism would |
882 |
882 provide many algebraic properties ``for free''. |
883 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
883 |
884 \isacommand{fun}~~@{text "\<approx>"}~~\isacommand{where}~~@{text "(x \<Colon> nat, y) \<approx> (u, v) = (x + v = u + y)"} |
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 |
|
886 the same integer relation as the one presented in the introduction: |
|
887 |
|
888 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % |
|
889 \isacommand{fun}~~@{text "\<approx>"}~~\isacommand{where}~~@{text "(m \<Colon> nat, n) \<approx> (p, q) = (m + q = n + p)"} |
885 \end{isabelle} |
890 \end{isabelle} |
886 |
891 |
887 \noindent |
892 \noindent |
888 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 |
889 relation is an equivalence relation which is solved automatically using the |
894 relation is an equivalence relation which is solved automatically using the |
890 definitions: |
895 definitions: |
891 |
896 |
892 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
897 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % |
893 \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 "\<approx>"} |
894 \end{isabelle} |
899 \end{isabelle} |
895 |
900 |
896 \noindent |
901 \noindent |
897 The user can then specify the constants on the quotient type: |
902 The user can then specify the constants on the quotient type: |
898 |
903 |
899 @{text "quotient_definition 0 \<Colon> int is (0\<Colon>nat, 0\<Colon>nat)"} |
904 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % |
900 @{text "fun plus_raw where plus_raw (x, y) (u, v) = (x + u, y + v)"} |
905 \begin{tabular}{@ {}l} |
901 @{text "quotient_definition (op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int) is plus_raw"} |
906 \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0::nat, 0::nat)"}\\ |
902 |
907 \isacommand{fun}~~@{text "plus_raw"}~~\isacommand{where}~~@{text "plus_raw (m :: nat, n) (p, q) = (m + p, n + q)"}\\ |
|
908 \isacommand{quotient\_definition}~~@{text "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)"}~~\isacommand{is}~~@{text "plus_raw"}\\ |
|
909 \end{tabular} |
|
910 \end{isabelle} |
|
911 |
|
912 \noindent |
903 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: |
904 |
914 |
905 @{text "lemma plus_zero_raw: plus_raw (0, 0) i \<approx> i"} |
915 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % |
906 |
916 \isacommand{lemma}~~@{text "plus_zero_raw: plus_raw (0, 0) x \<approx> x"} |
|
917 \end{isabelle} |
|
918 |
|
919 \noindent |
907 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 |
908 proof obligation is left, so let us prove it first: |
921 proof obligation is left, so let us prove it first: |
909 |
922 |
910 @{text "lemma (op \<approx> \<Longrightarrow> op \<approx> \<Longrightarrow> op \<approx>) plus_raw plus_raw"} |
923 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % |
911 |
924 \isacommand{lemma}~~@{text "[quot_respect]: (op \<approx> \<Longrightarrow> op \<approx> \<Longrightarrow> op \<approx>) plus_raw plus_raw"} |
|
925 \end{isabelle} |
|
926 |
|
927 \noindent |
912 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 |
913 of @{term "op \<Longrightarrow>"}. |
929 of @{text "op \<Longrightarrow>"}. |
914 |
|
915 Now the user can either prove a lifted lemma explicitly: |
930 Now the user can either prove a lifted lemma explicitly: |
916 |
931 |
917 @{text "lemma 0 + i = i by lifting plus_zero_raw"} |
932 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % |
918 |
933 \isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting plus_zero_raw"} |
|
934 \end{isabelle} |
|
935 |
|
936 \noindent |
919 Or in this simple case use the automated translation mechanism: |
937 Or in this simple case use the automated translation mechanism: |
920 |
938 |
921 @{text "thm plus_zero_raw[quot_lifted]"} |
939 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % |
922 |
940 \isacommand{thm}~~@{text "plus_zero_raw[quot_lifted]"} |
|
941 \end{isabelle} |
|
942 |
|
943 \noindent |
923 obtaining the same result. |
944 obtaining the same result. |
924 *} |
945 *} |
925 |
946 |
926 section {* Related Work *} |
947 section {* Related Work *} |
927 |
948 |