1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{natsum}% |
3 \def\isabellecontext{natsum}% |
4 \isamarkupfalse% |
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 \isamarkuptrue% |
5 % |
18 % |
6 \begin{isamarkuptext}% |
19 \begin{isamarkuptext}% |
7 \noindent |
20 \noindent |
8 In particular, there are \isa{case}-expressions, for example |
21 In particular, there are \isa{case}-expressions, for example |
9 \begin{isabelle}% |
22 \begin{isabelle}% |
10 \ \ \ \ \ case\ n\ of\ {\isadigit{0}}\ {\isasymRightarrow}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m% |
23 \ \ \ \ \ case\ n\ of\ {\isadigit{0}}\ {\isasymRightarrow}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m% |
11 \end{isabelle} |
24 \end{isabelle} |
12 primitive recursion, for example% |
25 primitive recursion, for example% |
13 \end{isamarkuptext}% |
26 \end{isamarkuptext}% |
14 \isamarkuptrue% |
27 \isamarkupfalse% |
15 \isacommand{consts}\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
28 \isacommand{consts}\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
16 \isamarkupfalse% |
29 \isamarkupfalse% |
17 \isacommand{primrec}\ {\isachardoublequote}sum\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline |
30 \isacommand{primrec}\ {\isachardoublequote}sum\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline |
18 \ \ \ \ \ \ \ \ {\isachardoublequote}sum\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharplus}\ sum\ n{\isachardoublequote}\isamarkupfalse% |
31 \ \ \ \ \ \ \ \ {\isachardoublequote}sum\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharplus}\ sum\ n{\isachardoublequote}\isamarkuptrue% |
19 % |
32 % |
20 \begin{isamarkuptext}% |
33 \begin{isamarkuptext}% |
21 \noindent |
34 \noindent |
22 and induction, for example% |
35 and induction, for example% |
23 \end{isamarkuptext}% |
36 \end{isamarkuptext}% |
24 \isamarkuptrue% |
37 \isamarkupfalse% |
25 \isacommand{lemma}\ {\isachardoublequote}sum\ n\ {\isacharplus}\ sum\ n\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\isanewline |
38 \isacommand{lemma}\ {\isachardoublequote}sum\ n\ {\isacharplus}\ sum\ n\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\isanewline |
|
39 % |
|
40 \isadelimproof |
|
41 % |
|
42 \endisadelimproof |
|
43 % |
|
44 \isatagproof |
26 \isamarkupfalse% |
45 \isamarkupfalse% |
27 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}\isanewline |
46 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}\isanewline |
28 \isamarkupfalse% |
47 \isamarkupfalse% |
29 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline |
48 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline |
30 \isamarkupfalse% |
49 \isamarkupfalse% |
31 \isacommand{done}\isamarkupfalse% |
50 \isacommand{done}% |
|
51 \endisatagproof |
|
52 {\isafoldproof}% |
|
53 % |
|
54 \isadelimproof |
|
55 % |
|
56 \endisadelimproof |
|
57 \isamarkuptrue% |
32 % |
58 % |
33 \begin{isamarkuptext}% |
59 \begin{isamarkuptext}% |
34 \newcommand{\mystar}{*% |
60 \newcommand{\mystar}{*% |
35 } |
61 } |
36 \index{arithmetic operations!for \protect\isa{nat}}% |
62 \index{arithmetic operations!for \protect\isa{nat}}% |
82 |
108 |
83 Both \isa{auto} and \isa{simp} |
109 Both \isa{auto} and \isa{simp} |
84 (a method introduced below, \S\ref{sec:Simplification}) prove |
110 (a method introduced below, \S\ref{sec:Simplification}) prove |
85 simple arithmetic goals automatically:% |
111 simple arithmetic goals automatically:% |
86 \end{isamarkuptext}% |
112 \end{isamarkuptext}% |
87 \isamarkuptrue% |
113 \isamarkupfalse% |
88 \isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isacharplus}\ {\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isamarkupfalse% |
114 \isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isacharplus}\ {\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}% |
89 \isamarkupfalse% |
115 \isadelimproof |
|
116 % |
|
117 \endisadelimproof |
|
118 % |
|
119 \isatagproof |
|
120 % |
|
121 \endisatagproof |
|
122 {\isafoldproof}% |
|
123 % |
|
124 \isadelimproof |
|
125 % |
|
126 \endisadelimproof |
|
127 \isamarkuptrue% |
90 % |
128 % |
91 \begin{isamarkuptext}% |
129 \begin{isamarkuptext}% |
92 \noindent |
130 \noindent |
93 For efficiency's sake, this built-in prover ignores quantified formulae, |
131 For efficiency's sake, this built-in prover ignores quantified formulae, |
94 many logical connectives, and all arithmetic operations apart from addition. |
132 many logical connectives, and all arithmetic operations apart from addition. |
95 In consequence, \isa{auto} and \isa{simp} cannot prove this slightly more complex goal:% |
133 In consequence, \isa{auto} and \isa{simp} cannot prove this slightly more complex goal:% |
96 \end{isamarkuptext}% |
134 \end{isamarkuptext}% |
97 \isamarkuptrue% |
135 \isamarkupfalse% |
98 \isacommand{lemma}\ {\isachardoublequote}m\ {\isasymnoteq}\ {\isacharparenleft}n{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymLongrightarrow}\ m\ {\isacharless}\ n\ {\isasymor}\ n\ {\isacharless}\ m{\isachardoublequote}\isamarkupfalse% |
136 \isacommand{lemma}\ {\isachardoublequote}m\ {\isasymnoteq}\ {\isacharparenleft}n{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymLongrightarrow}\ m\ {\isacharless}\ n\ {\isasymor}\ n\ {\isacharless}\ m{\isachardoublequote}% |
99 \isamarkupfalse% |
137 \isadelimproof |
|
138 % |
|
139 \endisadelimproof |
|
140 % |
|
141 \isatagproof |
|
142 % |
|
143 \endisatagproof |
|
144 {\isafoldproof}% |
|
145 % |
|
146 \isadelimproof |
|
147 % |
|
148 \endisadelimproof |
|
149 \isamarkuptrue% |
100 % |
150 % |
101 \begin{isamarkuptext}% |
151 \begin{isamarkuptext}% |
102 \noindent The method \methdx{arith} is more general. It attempts to |
152 \noindent The method \methdx{arith} is more general. It attempts to |
103 prove the first subgoal provided it is a \textbf{linear arithmetic} formula. |
153 prove the first subgoal provided it is a \textbf{linear arithmetic} formula. |
104 Such formulas may involve the usual logical connectives (\isa{{\isasymnot}}, |
154 Such formulas may involve the usual logical connectives (\isa{{\isasymnot}}, |
105 \isa{{\isasymand}}, \isa{{\isasymor}}, \isa{{\isasymlongrightarrow}}, \isa{{\isacharequal}}, |
155 \isa{{\isasymand}}, \isa{{\isasymor}}, \isa{{\isasymlongrightarrow}}, \isa{{\isacharequal}}, |
106 \isa{{\isasymforall}}, \isa{{\isasymexists}}), the relations \isa{{\isacharequal}}, |
156 \isa{{\isasymforall}}, \isa{{\isasymexists}}), the relations \isa{{\isacharequal}}, |
107 \isa{{\isasymle}} and \isa{{\isacharless}}, and the operations \isa{{\isacharplus}}, \isa{{\isacharminus}}, |
157 \isa{{\isasymle}} and \isa{{\isacharless}}, and the operations \isa{{\isacharplus}}, \isa{{\isacharminus}}, |
108 \isa{min} and \isa{max}. For example,% |
158 \isa{min} and \isa{max}. For example,% |
109 \end{isamarkuptext}% |
159 \end{isamarkuptext}% |
110 \isamarkuptrue% |
160 \isamarkupfalse% |
111 \isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline |
161 \isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline |
112 \isamarkupfalse% |
162 % |
113 \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isamarkupfalse% |
163 \isadelimproof |
114 \isamarkupfalse% |
164 % |
|
165 \endisadelimproof |
|
166 % |
|
167 \isatagproof |
|
168 \isamarkupfalse% |
|
169 \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}% |
|
170 \endisatagproof |
|
171 {\isafoldproof}% |
|
172 % |
|
173 \isadelimproof |
|
174 % |
|
175 \endisadelimproof |
|
176 \isamarkuptrue% |
115 % |
177 % |
116 \begin{isamarkuptext}% |
178 \begin{isamarkuptext}% |
117 \noindent |
179 \noindent |
118 succeeds because \isa{k\ {\isacharasterisk}\ k} can be treated as atomic. In contrast,% |
180 succeeds because \isa{k\ {\isacharasterisk}\ k} can be treated as atomic. In contrast,% |
119 \end{isamarkuptext}% |
181 \end{isamarkuptext}% |
120 \isamarkuptrue% |
182 \isamarkupfalse% |
121 \isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}\ {\isasymor}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}\isamarkupfalse% |
183 \isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}\ {\isasymor}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}% |
122 \isamarkupfalse% |
184 \isadelimproof |
|
185 % |
|
186 \endisadelimproof |
|
187 % |
|
188 \isatagproof |
|
189 % |
|
190 \endisatagproof |
|
191 {\isafoldproof}% |
|
192 % |
|
193 \isadelimproof |
|
194 % |
|
195 \endisadelimproof |
|
196 \isamarkuptrue% |
123 % |
197 % |
124 \begin{isamarkuptext}% |
198 \begin{isamarkuptext}% |
125 \noindent |
199 \noindent |
126 is not proved even by \isa{arith} because the proof relies |
200 is not proved even by \isa{arith} because the proof relies |
127 on properties of multiplication. Only multiplication by numerals (which is |
201 on properties of multiplication. Only multiplication by numerals (which is |