76 Both \isa{auto} and \isa{simp} |
76 Both \isa{auto} and \isa{simp} |
77 (a method introduced below, \S\ref{sec:Simplification}) prove |
77 (a method introduced below, \S\ref{sec:Simplification}) prove |
78 simple arithmetic goals automatically:% |
78 simple arithmetic goals automatically:% |
79 \end{isamarkuptext}% |
79 \end{isamarkuptext}% |
80 \isamarkuptrue% |
80 \isamarkuptrue% |
81 \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% |
81 \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}\isanewline |
|
82 \isamarkupfalse% |
82 \isamarkupfalse% |
83 \isamarkupfalse% |
83 % |
84 % |
84 \begin{isamarkuptext}% |
85 \begin{isamarkuptext}% |
85 \noindent |
86 \noindent |
86 For efficiency's sake, this built-in prover ignores quantified formulae, |
87 For efficiency's sake, this built-in prover ignores quantified formulae, |
87 logical connectives, and all arithmetic operations apart from addition. |
88 logical connectives, and all arithmetic operations apart from addition. |
88 In consequence, \isa{auto} and \isa{simp} cannot prove this slightly more complex goal:% |
89 In consequence, \isa{auto} and \isa{simp} cannot prove this slightly more complex goal:% |
89 \end{isamarkuptext}% |
90 \end{isamarkuptext}% |
90 \isamarkuptrue% |
91 \isamarkuptrue% |
91 \isacommand{lemma}\ {\isachardoublequote}m\ {\isasymnoteq}\ {\isacharparenleft}n{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymLongrightarrow}\ m\ {\isacharless}\ n\ {\isasymor}\ n\ {\isacharless}\ m{\isachardoublequote}\isamarkupfalse% |
92 \isacommand{lemma}\ {\isachardoublequote}m\ {\isasymnoteq}\ {\isacharparenleft}n{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymLongrightarrow}\ m\ {\isacharless}\ n\ {\isasymor}\ n\ {\isacharless}\ m{\isachardoublequote}\isanewline |
|
93 \isamarkupfalse% |
92 \isamarkupfalse% |
94 \isamarkupfalse% |
93 % |
95 % |
94 \begin{isamarkuptext}% |
96 \begin{isamarkuptext}% |
95 \noindent |
97 \noindent |
96 The method \methdx{arith} is more general. It attempts to prove |
98 The method \methdx{arith} is more general. It attempts to prove |
103 For example,% |
105 For example,% |
104 \end{isamarkuptext}% |
106 \end{isamarkuptext}% |
105 \isamarkuptrue% |
107 \isamarkuptrue% |
106 \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 |
108 \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 |
107 \isamarkupfalse% |
109 \isamarkupfalse% |
108 \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isamarkupfalse% |
110 \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline |
|
111 \isamarkupfalse% |
109 \isamarkupfalse% |
112 \isamarkupfalse% |
110 % |
113 % |
111 \begin{isamarkuptext}% |
114 \begin{isamarkuptext}% |
112 \noindent |
115 \noindent |
113 succeeds because \isa{k\ {\isacharasterisk}\ k} can be treated as atomic. In contrast,% |
116 succeeds because \isa{k\ {\isacharasterisk}\ k} can be treated as atomic. In contrast,% |
114 \end{isamarkuptext}% |
117 \end{isamarkuptext}% |
115 \isamarkuptrue% |
118 \isamarkuptrue% |
116 \isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}\ {\isasymor}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}\isamarkupfalse% |
119 \isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}\ {\isasymor}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}\isanewline |
|
120 \isamarkupfalse% |
117 \isamarkupfalse% |
121 \isamarkupfalse% |
118 % |
122 % |
119 \begin{isamarkuptext}% |
123 \begin{isamarkuptext}% |
120 \noindent |
124 \noindent |
121 is not proved even by \isa{arith} because the proof relies |
125 is not proved even by \isa{arith} because the proof relies |
130 role, it may fail to prove a valid formula, for example |
134 role, it may fail to prove a valid formula, for example |
131 \isa{m{\isacharplus}m\ {\isasymnoteq}\ n{\isacharplus}n{\isacharplus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}}. Fortunately, such examples are rare. |
135 \isa{m{\isacharplus}m\ {\isasymnoteq}\ n{\isacharplus}n{\isacharplus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}}. Fortunately, such examples are rare. |
132 \end{warn}% |
136 \end{warn}% |
133 \end{isamarkuptext}% |
137 \end{isamarkuptext}% |
134 \isamarkuptrue% |
138 \isamarkuptrue% |
135 \isanewline |
|
136 \isamarkupfalse% |
139 \isamarkupfalse% |
137 \end{isabellebody}% |
140 \end{isabellebody}% |
138 %%% Local Variables: |
141 %%% Local Variables: |
139 %%% mode: latex |
142 %%% mode: latex |
140 %%% TeX-master: "root" |
143 %%% TeX-master: "root" |