26 The arithmetic operations \isadxboldpos{+}{$HOL2arithfun}, |
26 The arithmetic operations \isadxboldpos{+}{$HOL2arithfun}, |
27 \isadxboldpos{-}{$HOL2arithfun}, \isadxboldpos{\mystar}{$HOL2arithfun}, |
27 \isadxboldpos{-}{$HOL2arithfun}, \isadxboldpos{\mystar}{$HOL2arithfun}, |
28 \sdx{div}, \sdx{mod}, \cdx{min} and |
28 \sdx{div}, \sdx{mod}, \cdx{min} and |
29 \cdx{max} are predefined, as are the relations |
29 \cdx{max} are predefined, as are the relations |
30 \isadxboldpos{\isasymle}{$HOL2arithrel} and |
30 \isadxboldpos{\isasymle}{$HOL2arithrel} and |
31 \isadxboldpos{<}{$HOL2arithrel}. As usual, @{prop"m-n = (0::nat)"} if |
31 \isadxboldpos{<}{$HOL2arithrel}. As usual, \<^prop>\<open>m-n = (0::nat)\<close> if |
32 @{prop"m<n"}. There is even a least number operation |
32 \<^prop>\<open>m<n\<close>. There is even a least number operation |
33 \sdx{LEAST}\@. For example, @{prop"(LEAST n. 0 < n) = Suc 0"}. |
33 \sdx{LEAST}\@. For example, \<^prop>\<open>(LEAST n. 0 < n) = Suc 0\<close>. |
34 \begin{warn}\index{overloading} |
34 \begin{warn}\index{overloading} |
35 The constants \cdx{0} and \cdx{1} and the operations |
35 The constants \cdx{0} and \cdx{1} and the operations |
36 \isadxboldpos{+}{$HOL2arithfun}, \isadxboldpos{-}{$HOL2arithfun}, |
36 \isadxboldpos{+}{$HOL2arithfun}, \isadxboldpos{-}{$HOL2arithfun}, |
37 \isadxboldpos{\mystar}{$HOL2arithfun}, \cdx{min}, |
37 \isadxboldpos{\mystar}{$HOL2arithfun}, \cdx{min}, |
38 \cdx{max}, \isadxboldpos{\isasymle}{$HOL2arithrel} and |
38 \cdx{max}, \isadxboldpos{\isasymle}{$HOL2arithrel} and |
39 \isadxboldpos{<}{$HOL2arithrel} are overloaded: they are available |
39 \isadxboldpos{<}{$HOL2arithrel} are overloaded: they are available |
40 not just for natural numbers but for other types as well. |
40 not just for natural numbers but for other types as well. |
41 For example, given the goal \<open>x + 0 = x\<close>, there is nothing to indicate |
41 For example, given the goal \<open>x + 0 = x\<close>, there is nothing to indicate |
42 that you are talking about natural numbers. Hence Isabelle can only infer |
42 that you are talking about natural numbers. Hence Isabelle can only infer |
43 that @{term x} is of some arbitrary type where \<open>0\<close> and \<open>+\<close> are |
43 that \<^term>\<open>x\<close> is of some arbitrary type where \<open>0\<close> and \<open>+\<close> are |
44 declared. As a consequence, you will be unable to prove the |
44 declared. As a consequence, you will be unable to prove the |
45 goal. To alert you to such pitfalls, Isabelle flags numerals without a |
45 goal. To alert you to such pitfalls, Isabelle flags numerals without a |
46 fixed type in its output: @{prop"x+0 = x"}. (In the absence of a numeral, |
46 fixed type in its output: \<^prop>\<open>x+0 = x\<close>. (In the absence of a numeral, |
47 it may take you some time to realize what has happened if \pgmenu{Show |
47 it may take you some time to realize what has happened if \pgmenu{Show |
48 Types} is not set). In this particular example, you need to include |
48 Types} is not set). In this particular example, you need to include |
49 an explicit type constraint, for example \<open>x+0 = (x::nat)\<close>. If there |
49 an explicit type constraint, for example \<open>x+0 = (x::nat)\<close>. If there |
50 is enough contextual information this may not be necessary: @{prop"Suc x = |
50 is enough contextual information this may not be necessary: \<^prop>\<open>Suc x = |
51 x"} automatically implies \<open>x::nat\<close> because @{term Suc} is not |
51 x\<close> automatically implies \<open>x::nat\<close> because \<^term>\<open>Suc\<close> is not |
52 overloaded. |
52 overloaded. |
53 |
53 |
54 For details on overloading see \S\ref{sec:overloading}. |
54 For details on overloading see \S\ref{sec:overloading}. |
55 Table~\ref{tab:overloading} in the appendix shows the most important |
55 Table~\ref{tab:overloading} in the appendix shows the most important |
56 overloaded operations. |
56 overloaded operations. |
57 \end{warn} |
57 \end{warn} |
58 \begin{warn} |
58 \begin{warn} |
59 The symbols \isadxboldpos{>}{$HOL2arithrel} and |
59 The symbols \isadxboldpos{>}{$HOL2arithrel} and |
60 \isadxboldpos{\isasymge}{$HOL2arithrel} are merely syntax: \<open>x > y\<close> |
60 \isadxboldpos{\isasymge}{$HOL2arithrel} are merely syntax: \<open>x > y\<close> |
61 stands for @{prop"y < x"} and similary for \<open>\<ge>\<close> and |
61 stands for \<^prop>\<open>y < x\<close> and similary for \<open>\<ge>\<close> and |
62 \<open>\<le>\<close>. |
62 \<open>\<le>\<close>. |
63 \end{warn} |
63 \end{warn} |
64 \begin{warn} |
64 \begin{warn} |
65 Constant \<open>1::nat\<close> is defined to equal @{term"Suc 0"}. This definition |
65 Constant \<open>1::nat\<close> is defined to equal \<^term>\<open>Suc 0\<close>. This definition |
66 (see \S\ref{sec:ConstDefinitions}) is unfolded automatically by some |
66 (see \S\ref{sec:ConstDefinitions}) is unfolded automatically by some |
67 tactics (like \<open>auto\<close>, \<open>simp\<close> and \<open>arith\<close>) but not by |
67 tactics (like \<open>auto\<close>, \<open>simp\<close> and \<open>arith\<close>) but not by |
68 others (especially the single step tactics in Chapter~\ref{chap:rules}). |
68 others (especially the single step tactics in Chapter~\ref{chap:rules}). |
69 If you need the full set of numerals, see~\S\ref{sec:numerals}. |
69 If you need the full set of numerals, see~\S\ref{sec:numerals}. |
70 \emph{Novices are advised to stick to @{term"0::nat"} and @{term Suc}.} |
70 \emph{Novices are advised to stick to \<^term>\<open>0::nat\<close> and \<^term>\<open>Suc\<close>.} |
71 \end{warn} |
71 \end{warn} |
72 |
72 |
73 Both \<open>auto\<close> and \<open>simp\<close> |
73 Both \<open>auto\<close> and \<open>simp\<close> |
74 (a method introduced below, \S\ref{sec:Simplification}) prove |
74 (a method introduced below, \S\ref{sec:Simplification}) prove |
75 simple arithmetic goals automatically: |
75 simple arithmetic goals automatically: |
91 prove the first subgoal provided it is a \textbf{linear arithmetic} formula. |
91 prove the first subgoal provided it is a \textbf{linear arithmetic} formula. |
92 Such formulas may involve the usual logical connectives (\<open>\<not>\<close>, |
92 Such formulas may involve the usual logical connectives (\<open>\<not>\<close>, |
93 \<open>\<and>\<close>, \<open>\<or>\<close>, \<open>\<longrightarrow>\<close>, \<open>=\<close>, |
93 \<open>\<and>\<close>, \<open>\<or>\<close>, \<open>\<longrightarrow>\<close>, \<open>=\<close>, |
94 \<open>\<forall>\<close>, \<open>\<exists>\<close>), the relations \<open>=\<close>, |
94 \<open>\<forall>\<close>, \<open>\<exists>\<close>), the relations \<open>=\<close>, |
95 \<open>\<le>\<close> and \<open><\<close>, and the operations \<open>+\<close>, \<open>-\<close>, |
95 \<open>\<le>\<close> and \<open><\<close>, and the operations \<open>+\<close>, \<open>-\<close>, |
96 @{term min} and @{term max}. For example,\<close> |
96 \<^term>\<open>min\<close> and \<^term>\<open>max\<close>. For example,\<close> |
97 |
97 |
98 lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))" |
98 lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))" |
99 apply(arith) |
99 apply(arith) |
100 (*<*)done(*>*) |
100 (*<*)done(*>*) |
101 |
101 |
102 text\<open>\noindent |
102 text\<open>\noindent |
103 succeeds because @{term"k*k"} can be treated as atomic. In contrast, |
103 succeeds because \<^term>\<open>k*k\<close> can be treated as atomic. In contrast, |
104 \<close> |
104 \<close> |
105 |
105 |
106 lemma "n*n = n+1 \<Longrightarrow> n=0" |
106 lemma "n*n = n+1 \<Longrightarrow> n=0" |
107 (*<*)oops(*>*) |
107 (*<*)oops(*>*) |
108 |
108 |