author  wenzelm 
Sun, 04 Nov 2012 19:51:53 +0100  
changeset 50065  7c01dc2dcb8c 
parent 50064  e08cc8b20564 
child 50068  310e9b810bbf 
permissions  rwrr 
26782  1 
theory Generic 
42651  2 
imports Base Main 
26782  3 
begin 
4 

5 
chapter {* Generic tools and packages \label{ch:gentools} *} 

6 

42655  7 
section {* Configuration options \label{sec:config} *} 
26782  8 

40291  9 
text {* Isabelle/Pure maintains a record of named configuration 
10 
options within the theory or proof context, with values of type 

11 
@{ML_type bool}, @{ML_type int}, @{ML_type real}, or @{ML_type 

12 
string}. Tools may declare options in ML, and then refer to these 

13 
values (relative to the context). Thus global reference variables 

14 
are easily avoided. The user may change the value of a 

15 
configuration option by means of an associated attribute of the same 

16 
name. This form of context declaration works particularly well with 

42655  17 
commands such as @{command "declare"} or @{command "using"} like 
18 
this: 

19 
*} 

20 

21 
declare [[show_main_goal = false]] 

26782  22 

42655  23 
notepad 
24 
begin 

25 
note [[show_main_goal = true]] 

26 
end 

27 

28 
text {* For historical reasons, some tools cannot take the full proof 

26782  29 
context into account and merely refer to the background theory. 
30 
This is accommodated by configuration options being declared as 

31 
``global'', which may not be changed within a local context. 

32 

33 
\begin{matharray}{rcll} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

34 
@{command_def "print_configs"} & : & @{text "context \<rightarrow>"} \\ 
26782  35 
\end{matharray} 
36 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

37 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

38 
@{syntax name} ('=' ('true'  'false'  @{syntax int}  @{syntax float}  @{syntax name}))? 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

39 
"} 
26782  40 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

41 
\begin{description} 
26782  42 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

43 
\item @{command "print_configs"} prints the available configuration 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

44 
options, with names, types, and current values. 
26782  45 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

46 
\item @{text "name = value"} as an attribute expression modifies the 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

47 
named option, with the syntax of the value depending on the option's 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

48 
type. For @{ML_type bool} the default value is @{text true}. Any 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

49 
attempt to change a global option in a local context is ignored. 
26782  50 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

51 
\end{description} 
26782  52 
*} 
53 

54 

27040  55 
section {* Basic proof tools *} 
26782  56 

57 
subsection {* Miscellaneous methods and attributes \label{sec:miscmethatt} *} 

58 

59 
text {* 

60 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

61 
@{method_def unfold} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

62 
@{method_def fold} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

63 
@{method_def insert} & : & @{text method} \\[0.5ex] 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

64 
@{method_def erule}@{text "\<^sup>*"} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

65 
@{method_def drule}@{text "\<^sup>*"} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

66 
@{method_def frule}@{text "\<^sup>*"} & : & @{text method} \\ 
43365  67 
@{method_def intro} & : & @{text method} \\ 
68 
@{method_def elim} & : & @{text method} \\ 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

69 
@{method_def succeed} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

70 
@{method_def fail} & : & @{text method} \\ 
26782  71 
\end{matharray} 
72 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

73 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

74 
(@@{method fold}  @@{method unfold}  @@{method insert}) @{syntax thmrefs} 
26782  75 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

76 
(@@{method erule}  @@{method drule}  @@{method frule}) 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

77 
('(' @{syntax nat} ')')? @{syntax thmrefs} 
43365  78 
; 
79 
(@@{method intro}  @@{method elim}) @{syntax thmrefs}? 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

80 
"} 
26782  81 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

82 
\begin{description} 
26782  83 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

84 
\item @{method unfold}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{method fold}~@{text 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

85 
"a\<^sub>1 \<dots> a\<^sub>n"} expand (or fold back) the given definitions throughout 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

86 
all goals; any chained facts provided are inserted into the goal and 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

87 
subject to rewriting as well. 
26782  88 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

89 
\item @{method insert}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} inserts theorems as facts 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

90 
into all goals of the proof state. Note that current facts 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

91 
indicated for forward chaining are ignored. 
26782  92 

30397  93 
\item @{method erule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, @{method 
94 
drule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, and @{method frule}~@{text 

95 
"a\<^sub>1 \<dots> a\<^sub>n"} are similar to the basic @{method rule} 

96 
method (see \secref{sec:puremethatt}), but apply rules by 

97 
elimresolution, destructresolution, and forwardresolution, 

98 
respectively \cite{isabelleimplementation}. The optional natural 

99 
number argument (default 0) specifies additional assumption steps to 

100 
be performed here. 

26782  101 

102 
Note that these methods are improper ones, mainly serving for 

103 
experimentation and tactic script emulation. Different modes of 

104 
basic rule application are usually expressed in Isar at the proof 

105 
language level, rather than via implicit proof state manipulations. 

106 
For example, a proper singlestep elimination would be done using 

107 
the plain @{method rule} method, with forward chaining of current 

108 
facts. 

109 

43365  110 
\item @{method intro} and @{method elim} repeatedly refine some goal 
111 
by intro or elimresolution, after having inserted any chained 

112 
facts. Exactly the rules given as arguments are taken into account; 

113 
this allows finetuned decomposition of a proof problem, in contrast 

114 
to common automated tools. 

115 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

116 
\item @{method succeed} yields a single (unchanged) result; it is 
26782  117 
the identity of the ``@{text ","}'' method combinator (cf.\ 
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27248
diff
changeset

118 
\secref{sec:proofmeth}). 
26782  119 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

120 
\item @{method fail} yields an empty result sequence; it is the 
26782  121 
identity of the ``@{text ""}'' method combinator (cf.\ 
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27248
diff
changeset

122 
\secref{sec:proofmeth}). 
26782  123 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

124 
\end{description} 
26782  125 

126 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

127 
@{attribute_def tagged} & : & @{text attribute} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

128 
@{attribute_def untagged} & : & @{text attribute} \\[0.5ex] 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

129 
@{attribute_def THEN} & : & @{text attribute} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

130 
@{attribute_def unfolded} & : & @{text attribute} \\ 
47497  131 
@{attribute_def folded} & : & @{text attribute} \\ 
132 
@{attribute_def abs_def} & : & @{text attribute} \\[0.5ex] 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

133 
@{attribute_def rotated} & : & @{text attribute} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

134 
@{attribute_def (Pure) elim_format} & : & @{text attribute} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

135 
@{attribute_def standard}@{text "\<^sup>*"} & : & @{text attribute} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

136 
@{attribute_def no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\ 
26782  137 
\end{matharray} 
138 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

139 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

140 
@@{attribute tagged} @{syntax name} @{syntax name} 
26782  141 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

142 
@@{attribute untagged} @{syntax name} 
26782  143 
; 
48205  144 
@@{attribute THEN} ('[' @{syntax nat} ']')? @{syntax thmref} 
26782  145 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

146 
(@@{attribute unfolded}  @@{attribute folded}) @{syntax thmrefs} 
26782  147 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

148 
@@{attribute rotated} @{syntax int}? 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

149 
"} 
26782  150 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

151 
\begin{description} 
26782  152 

28764  153 
\item @{attribute tagged}~@{text "name value"} and @{attribute 
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

154 
untagged}~@{text name} add and remove \emph{tags} of some theorem. 
26782  155 
Tags may be any list of string pairs that serve as formal comment. 
28764  156 
The first string is considered the tag name, the second its value. 
157 
Note that @{attribute untagged} removes any tags of the same name. 

26782  158 

48205  159 
\item @{attribute THEN}~@{text a} composes rules by resolution; it 
160 
resolves with the first premise of @{text a} (an alternative 

161 
position may be also specified). See also @{ML_op "RS"} in 

162 
\cite{isabelleimplementation}. 

26782  163 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

164 
\item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

165 
folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

166 
definitions throughout a rule. 
26782  167 

47497  168 
\item @{attribute abs_def} turns an equation of the form @{prop "f x 
169 
y \<equiv> t"} into @{prop "f \<equiv> \<lambda>x y. t"}, which ensures that @{method 

170 
simp} or @{method unfold} steps always expand it. This also works 

171 
for objectlogic equality. 

172 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

173 
\item @{attribute rotated}~@{text n} rotate the premises of a 
26782  174 
theorem by @{text n} (default 1). 
175 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

176 
\item @{attribute (Pure) elim_format} turns a destruction rule into 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

177 
elimination rule format, by resolving with the rule @{prop "PROP A \<Longrightarrow> 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

178 
(PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}. 
26782  179 

180 
Note that the Classical Reasoner (\secref{sec:classical}) provides 

181 
its own version of this operation. 

182 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

183 
\item @{attribute standard} puts a theorem into the standard form of 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

184 
objectrules at the outermost theory level. Note that this 
26782  185 
operation violates the local proof context (including active 
186 
locales). 

187 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

188 
\item @{attribute no_vars} replaces schematic variables by free 
26782  189 
ones; this is mainly for tuning output of pretty printed theorems. 
190 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

191 
\end{description} 
26782  192 
*} 
193 

194 

27044  195 
subsection {* Lowlevel equational reasoning *} 
196 

197 
text {* 

198 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

199 
@{method_def subst} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

200 
@{method_def hypsubst} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

201 
@{method_def split} & : & @{text method} \\ 
27044  202 
\end{matharray} 
203 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

204 
@{rail " 
42704  205 
@@{method subst} ('(' 'asm' ')')? \\ ('(' (@{syntax nat}+) ')')? @{syntax thmref} 
27044  206 
; 
44094
f7bbfdf4b4a7
updated documentation of method "split" according to e6a4bb832b46;
wenzelm
parents:
43367
diff
changeset

207 
@@{method split} @{syntax thmrefs} 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

208 
"} 
27044  209 

210 
These methods provide lowlevel facilities for equational reasoning 

211 
that are intended for specialized applications only. Normally, 

212 
single step calculations would be performed in a structured text 

213 
(see also \secref{sec:calculation}), while the Simplifier methods 

214 
provide the canonical way for automated normalization (see 

215 
\secref{sec:simplifier}). 

216 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

217 
\begin{description} 
27044  218 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

219 
\item @{method subst}~@{text eq} performs a single substitution step 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

220 
using rule @{text eq}, which may be either a meta or object 
27044  221 
equality. 
222 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

223 
\item @{method subst}~@{text "(asm) eq"} substitutes in an 
27044  224 
assumption. 
225 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

226 
\item @{method subst}~@{text "(i \<dots> j) eq"} performs several 
27044  227 
substitutions in the conclusion. The numbers @{text i} to @{text j} 
228 
indicate the positions to substitute at. Positions are ordered from 

229 
the top of the term tree moving down from left to right. For 

230 
example, in @{text "(a + b) + (c + d)"} there are three positions 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

231 
where commutativity of @{text "+"} is applicable: 1 refers to @{text 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

232 
"a + b"}, 2 to the whole term, and 3 to @{text "c + d"}. 
27044  233 

234 
If the positions in the list @{text "(i \<dots> j)"} are nonoverlapping 

235 
(e.g.\ @{text "(2 3)"} in @{text "(a + b) + (c + d)"}) you may 

236 
assume all substitutions are performed simultaneously. Otherwise 

237 
the behaviour of @{text subst} is not specified. 

238 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

239 
\item @{method subst}~@{text "(asm) (i \<dots> j) eq"} performs the 
27071  240 
substitutions in the assumptions. The positions refer to the 
241 
assumptions in order from left to right. For example, given in a 

242 
goal of the form @{text "P (a + b) \<Longrightarrow> P (c + d) \<Longrightarrow> \<dots>"}, position 1 of 

243 
commutativity of @{text "+"} is the subterm @{text "a + b"} and 

244 
position 2 is the subterm @{text "c + d"}. 

27044  245 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

246 
\item @{method hypsubst} performs substitution using some 
27044  247 
assumption; this only works for equations of the form @{text "x = 
248 
t"} where @{text x} is a free or bound variable. 

249 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

250 
\item @{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} performs singlestep case 
44094
f7bbfdf4b4a7
updated documentation of method "split" according to e6a4bb832b46;
wenzelm
parents:
43367
diff
changeset

251 
splitting using the given rules. Splitting is performed in the 
f7bbfdf4b4a7
updated documentation of method "split" according to e6a4bb832b46;
wenzelm
parents:
43367
diff
changeset

252 
conclusion or some assumption of the subgoal, depending of the 
f7bbfdf4b4a7
updated documentation of method "split" according to e6a4bb832b46;
wenzelm
parents:
43367
diff
changeset

253 
structure of the rule. 
27044  254 

255 
Note that the @{method simp} method already involves repeated 

44094
f7bbfdf4b4a7
updated documentation of method "split" according to e6a4bb832b46;
wenzelm
parents:
43367
diff
changeset

256 
application of split rules as declared in the current context, using 
f7bbfdf4b4a7
updated documentation of method "split" according to e6a4bb832b46;
wenzelm
parents:
43367
diff
changeset

257 
@{attribute split}, for example. 
27044  258 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

259 
\end{description} 
27044  260 
*} 
261 

262 

26782  263 
subsection {* Further tactic emulations \label{sec:tactics} *} 
264 

265 
text {* 

266 
The following improper proof methods emulate traditional tactics. 

267 
These admit direct access to the goal state, which is normally 

268 
considered harmful! In particular, this may involve both numbered 

269 
goal addressing (default 1), and dynamic instantiation within the 

270 
scope of some subgoal. 

271 

272 
\begin{warn} 

273 
Dynamic instantiations refer to universally quantified parameters 

274 
of a subgoal (the dynamic context) rather than fixed variables and 

275 
term abbreviations of a (static) Isar context. 

276 
\end{warn} 

277 

278 
Tactic emulation methods, unlike their ML counterparts, admit 

279 
simultaneous instantiation from both dynamic and static contexts. 

280 
If names occur in both contexts goal parameters hide locally fixed 

281 
variables. Likewise, schematic variables refer to term 

282 
abbreviations, if present in the static context. Otherwise the 

283 
schematic variable is interpreted as a schematic variable and left 

284 
to be solved by unification with certain parts of the subgoal. 

285 

286 
Note that the tactic emulation proof methods in Isabelle/Isar are 

287 
consistently named @{text foo_tac}. Note also that variable names 

288 
occurring on left hand sides of instantiations must be preceded by a 

289 
question mark if they coincide with a keyword or contain dots. This 

290 
is consistent with the attribute @{attribute "where"} (see 

291 
\secref{sec:puremethatt}). 

292 

293 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

294 
@{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

295 
@{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

296 
@{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

297 
@{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

298 
@{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

299 
@{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

300 
@{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

301 
@{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

302 
@{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

303 
@{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

304 
@{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\ 
26782  305 
\end{matharray} 
306 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

307 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

308 
(@@{method rule_tac}  @@{method erule_tac}  @@{method drule_tac}  
42705  309 
@@{method frule_tac}  @@{method cut_tac}  @@{method thin_tac}) @{syntax goal_spec}? \\ 
42617  310 
( dynamic_insts @'in' @{syntax thmref}  @{syntax thmrefs} ) 
26782  311 
; 
42705  312 
@@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

313 
; 
42705  314 
@@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +) 
26782  315 
; 
42705  316 
@@{method rotate_tac} @{syntax goal_spec}? @{syntax int}? 
26782  317 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

318 
(@@{method tactic}  @@{method raw_tactic}) @{syntax text} 
26782  319 
; 
320 

42617  321 
dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and') 
322 
"} 

26782  323 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

324 
\begin{description} 
26782  325 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

326 
\item @{method rule_tac} etc. do resolution of rules with explicit 
26782  327 
instantiation. This works the same way as the ML tactics @{ML 
30397  328 
res_inst_tac} etc. (see \cite{isabelleimplementation}) 
26782  329 

330 
Multiple rules may be only given if there is no instantiation; then 

331 
@{method rule_tac} is the same as @{ML resolve_tac} in ML (see 

30397  332 
\cite{isabelleimplementation}). 
26782  333 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

334 
\item @{method cut_tac} inserts facts into the proof state as 
46706
877d57975427
updated cut_tac, without loose references to implementation manual;
wenzelm
parents:
46494
diff
changeset

335 
assumption of a subgoal; instantiations may be given as well. Note 
877d57975427
updated cut_tac, without loose references to implementation manual;
wenzelm
parents:
46494
diff
changeset

336 
that the scope of schematic variables is spread over the main goal 
877d57975427
updated cut_tac, without loose references to implementation manual;
wenzelm
parents:
46494
diff
changeset

337 
statement and rule premises are turned into new subgoals. This is 
877d57975427
updated cut_tac, without loose references to implementation manual;
wenzelm
parents:
46494
diff
changeset

338 
in contrast to the regular method @{method insert} which inserts 
877d57975427
updated cut_tac, without loose references to implementation manual;
wenzelm
parents:
46494
diff
changeset

339 
closed rule statements. 
26782  340 

46277  341 
\item @{method thin_tac}~@{text \<phi>} deletes the specified premise 
342 
from a subgoal. Note that @{text \<phi>} may contain schematic 

343 
variables, to abbreviate the intended proposition; the first 

344 
matching subgoal premise will be deleted. Removing useless premises 

345 
from a subgoal increases its readability and can make search tactics 

346 
run faster. 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

347 

46271  348 
\item @{method subgoal_tac}~@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} adds the propositions 
349 
@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} as local premises to a subgoal, and poses the same 

350 
as new subgoals (in the original context). 

26782  351 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

352 
\item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

353 
goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

354 
\emph{suffix} of variables. 
26782  355 

46274  356 
\item @{method rotate_tac}~@{text n} rotates the premises of a 
357 
subgoal by @{text n} positions: from right to left if @{text n} is 

26782  358 
positive, and from left to right if @{text n} is negative; the 
46274  359 
default value is 1. 
26782  360 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

361 
\item @{method tactic}~@{text "text"} produces a proof method from 
26782  362 
any ML text of type @{ML_type tactic}. Apart from the usual ML 
27223  363 
environment and the current proof context, the ML code may refer to 
364 
the locally bound values @{ML_text facts}, which indicates any 

365 
current facts used for forwardchaining. 

26782  366 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

367 
\item @{method raw_tactic} is similar to @{method tactic}, but 
27223  368 
presents the goal state in its raw internal form, where simultaneous 
369 
subgoals appear as conjunction of the logical framework instead of 

370 
the usual split into several subgoals. While feature this is useful 

371 
for debugging of complex method definitions, it should not never 

372 
appear in production theories. 

26782  373 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

374 
\end{description} 
26782  375 
*} 
376 

377 

27040  378 
section {* The Simplifier \label{sec:simplifier} *} 
26782  379 

50063  380 
text {* The Simplifier performs conditional and unconditional 
381 
rewriting and uses contextual information: rule declarations in the 

382 
background theory or local proof context are taken into account, as 

383 
well as chained facts and subgoal premises (``local assumptions''). 

384 
There are several general hooks that allow to modify the 

385 
simplification strategy, or incorporate other proof tools that solve 

386 
subproblems, produce rewrite rules on demand etc. 

387 

388 
The default Simplifier setup of major object logics (HOL, HOLCF, 

389 
FOL, ZF) makes the Simplifier ready for immediate use, without 

390 
engaging into the internal structures. Thus it serves as 

391 
generalpurpose proof tool with the main focus on equational 

392 
reasoning, and a bit more than that. *} 

393 

394 

395 
subsection {* Simplification methods \label{sec:simpmeth} *} 

26782  396 

397 
text {* 

398 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

399 
@{method_def simp} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

400 
@{method_def simp_all} & : & @{text method} \\ 
26782  401 
\end{matharray} 
402 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

403 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

404 
(@@{method simp}  @@{method simp_all}) opt? (@{syntax simpmod} * ) 
26782  405 
; 
406 

40255
9ffbc25e1606
eliminated obsolete \_ escapes in rail environments;
wenzelm
parents:
35613
diff
changeset

407 
opt: '(' ('no_asm'  'no_asm_simp'  'no_asm_use'  'asm_lr' ) ')' 
26782  408 
; 
50063  409 
@{syntax_def simpmod}: ('add'  'del'  'only'  'split' (()  'add'  'del')  
410 
'cong' (()  'add'  'del')) ':' @{syntax thmrefs} 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

411 
"} 
26782  412 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

413 
\begin{description} 
26782  414 

50063  415 
\item @{method simp} invokes the Simplifier on the first subgoal, 
416 
after inserting chained facts as additional goal premises; further 

417 
rule declarations may be included via @{text "(simp add: facts)"}. 

418 
The proof method fails if the subgoal remains unchanged after 

419 
simplification. 

26782  420 

50063  421 
Note that the original goal premises and chained facts are subject 
422 
to simplification themselves, while declarations via @{text 

423 
"add"}/@{text "del"} merely follow the policies of the objectlogic 

424 
to extract rewrite rules from theorems, without further 

425 
simplification. This may lead to slightly different behavior in 

426 
either case, which might be required precisely like that in some 

427 
boundary situations to perform the intended simplification step! 

428 

429 
\medskip The @{text only} modifier first removes all other rewrite 

430 
rules, looper tactics (including split rules), congruence rules, and 

431 
then behaves like @{text add}. Implicit solvers remain, which means 

432 
that trivial rules like reflexivity or introduction of @{text 

433 
"True"} are available to solve the simplified subgoals, but also 

434 
nontrivial tools like linear arithmetic in HOL. The latter may 

435 
lead to some surprise of the meaning of ``only'' in Isabelle/HOL 

436 
compared to English! 

26782  437 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

438 
\medskip The @{text split} modifiers add or delete rules for the 
26782  439 
Splitter (see also \cite{isabelleref}), the default is to add. 
440 
This works only if the Simplifier method has been properly setup to 

441 
include the Splitter (all major object logics such HOL, HOLCF, FOL, 

442 
ZF do this already). 

443 

50065  444 
There is also a separate @{method_ref split} method available for 
445 
singlestep case splitting. The effect of repeatedly applying 

446 
@{text "(split thms)"} can be imitated by ``@{text "(simp only: 

447 
split: thms)"}''. 

448 

50063  449 
\medskip The @{text cong} modifiers add or delete Simplifier 
450 
congruence rules (see also \secref{sec:simprules}); the default is 

451 
to add. 

452 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

453 
\item @{method simp_all} is similar to @{method simp}, but acts on 
50063  454 
all goals, working backwards from the last to the first one as usual 
455 
in Isabelle.\footnote{The order is irrelevant for goals without 

456 
schematic variables, so simplification might actually be performed 

457 
in parallel here.} 

458 

459 
Chained facts are inserted into all subgoals, before the 

460 
simplification process starts. Further rule declarations are the 

461 
same as for @{method simp}. 

462 

463 
The proof method fails if all subgoals remain unchanged after 

464 
simplification. 

26782  465 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

466 
\end{description} 
26782  467 

50063  468 
By default the Simplifier methods above take local assumptions fully 
469 
into account, using equational assumptions in the subsequent 

470 
normalization process, or simplifying assumptions themselves. 

471 
Further options allow to finetune the behavior of the Simplifier 

472 
in this respect, corresponding to a variety of ML tactics as 

473 
follows.\footnote{Unlike the corresponding Isar proof methods, the 

474 
ML tactics do not insist in changing the goal state.} 

475 

476 
\begin{center} 

477 
\small 

50065  478 
\begin{supertabular}{llp{0.3\textwidth}} 
50063  479 
\hline 
480 
Isar method & ML tactic & behavior \\\hline 

481 

482 
@{text "(simp (no_asm))"} & @{ML simp_tac} & assumptions are ignored 

483 
completely \\\hline 

26782  484 

50063  485 
@{text "(simp (no_asm_simp))"} & @{ML asm_simp_tac} & assumptions 
486 
are used in the simplification of the conclusion but are not 

487 
themselves simplified \\\hline 

488 

489 
@{text "(simp (no_asm_use))"} & @{ML full_simp_tac} & assumptions 

490 
are simplified but are not used in the simplification of each other 

491 
or the conclusion \\\hline 

26782  492 

50063  493 
@{text "(simp)"} & @{ML asm_full_simp_tac} & assumptions are used in 
494 
the simplification of the conclusion and to simplify other 

495 
assumptions \\\hline 

496 

497 
@{text "(simp (asm_lr))"} & @{ML asm_lr_simp_tac} & compatibility 

498 
mode: an assumption is only used for simplifying assumptions which 

499 
are to the right of it \\\hline 

500 

50065  501 
\end{supertabular} 
50063  502 
\end{center} 
26782  503 
*} 
504 

505 

50064  506 
subsubsection {* Examples *} 
507 

508 
text {* We consider basic algebraic simplifications in Isabelle/HOL. 

509 
The rather trivial goal @{prop "0 + (x + 0) = x + 0 + 0"} looks like 

510 
a good candidate to be solved by a single call of @{method simp}: 

511 
*} 

512 

513 
lemma "0 + (x + 0) = x + 0 + 0" apply simp? oops 

514 

515 
text {* The above attempt \emph{fails}, because @{term "0"} and @{term 

516 
"op +"} in the HOL library are declared as generic type class 

517 
operations, without stating any algebraic laws yet. More specific 

518 
types are required to get access to certain standard simplifications 

519 
of the theory context, e.g.\ like this: *} 

520 

521 
lemma fixes x :: nat shows "0 + (x + 0) = x + 0 + 0" by simp 

522 
lemma fixes x :: int shows "0 + (x + 0) = x + 0 + 0" by simp 

523 
lemma fixes x :: "'a :: monoid_add" shows "0 + (x + 0) = x + 0 + 0" by simp 

524 

525 
text {* 

526 
\medskip In many cases, assumptions of a subgoal are also needed in 

527 
the simplification process. For example: 

528 
*} 

529 

530 
lemma fixes x :: nat shows "x = 0 \<Longrightarrow> x + x = 0" by simp 

531 
lemma fixes x :: nat assumes "x = 0" shows "x + x = 0" apply simp oops 

532 
lemma fixes x :: nat assumes "x = 0" shows "x + x = 0" using assms by simp 

533 

534 
text {* As seen above, local assumptions that shall contribute to 

535 
simplification need to be part of the subgoal already, or indicated 

536 
explicitly for use by the subsequent method invocation. Both too 

537 
little or too much information can make simplification fail, for 

538 
different reasons. 

539 

540 
In the next example the malicious assumption @{prop "\<And>x::nat. f x = 

541 
g (f (g x))"} does not contribute to solve the problem, but makes 

542 
the default @{method simp} method loop: the rewrite rule @{text "f 

543 
?x \<equiv> g (f (g ?x))"} extracted from the assumption does not 

544 
terminate. The Simplifier notices certain simple forms of 

545 
nontermination, but not this one. The problem can be solved 

546 
nonetheless, by ignoring assumptions via special options as 

547 
explained before: 

548 
*} 

549 

550 
lemma "(\<And>x::nat. f x = g (f (g x))) \<Longrightarrow> f 0 = f 0 + 0" 

551 
by (simp (no_asm)) 

552 

553 
text {* The latter form is typical for long unstructured proof 

554 
scripts, where the control over the goal content is limited. In 

555 
structured proofs it is usually better to avoid pushing too many 

556 
facts into the goal state in the first place. Assumptions in the 

557 
Isar proof context do not intrude the reasoning if not used 

558 
explicitly. This is illustrated for a toplevel statement and a 

559 
local proof body as follows: 

560 
*} 

561 

562 
lemma 

563 
assumes "\<And>x::nat. f x = g (f (g x))" 

564 
shows "f 0 = f 0 + 0" by simp 

565 

566 
notepad 

567 
begin 

568 
assume "\<And>x::nat. f x = g (f (g x))" 

569 
have "f 0 = f 0 + 0" by simp 

570 
end 

571 

572 
text {* \medskip Because assumptions may simplify each other, there 

573 
can be very subtle cases of nontermination. For example, the regular 

574 
@{method simp} method applied to @{prop "P (f x) \<Longrightarrow> y = x \<Longrightarrow> f x = f y 

575 
\<Longrightarrow> Q"} gives rise to the infinite reduction sequence 

576 
\[ 

577 
@{text "P (f x)"} \stackrel{@{text "f x \<equiv> f y"}}{\longmapsto} 

578 
@{text "P (f y)"} \stackrel{@{text "y \<equiv> x"}}{\longmapsto} 

579 
@{text "P (f x)"} \stackrel{@{text "f x \<equiv> f y"}}{\longmapsto} \cdots 

580 
\] 

581 
whereas applying the same to @{prop "y = x \<Longrightarrow> f x = f y \<Longrightarrow> P (f x) \<Longrightarrow> 

582 
Q"} terminates (without solving the goal): 

583 
*} 

584 

585 
lemma "y = x \<Longrightarrow> f x = f y \<Longrightarrow> P (f x) \<Longrightarrow> Q" 

586 
apply simp 

587 
oops 

588 

589 
text {* See also \secref{sec:simpconfig} for options to enable 

590 
Simplifier trace mode, which often helps to diagnose problems with 

591 
rewrite systems. 

592 
*} 

593 

594 

50063  595 
subsection {* Declaring rules \label{sec:simprules} *} 
26782  596 

597 
text {* 

598 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

599 
@{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

600 
@{attribute_def simp} & : & @{text attribute} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

601 
@{attribute_def split} & : & @{text attribute} \\ 
50063  602 
@{attribute_def cong} & : & @{text attribute} \\ 
26782  603 
\end{matharray} 
604 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

605 
@{rail " 
50063  606 
(@@{attribute simp}  @@{attribute split}  @@{attribute cong}) 
607 
(()  'add'  'del') 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

608 
"} 
26782  609 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

610 
\begin{description} 
26782  611 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

612 
\item @{command "print_simpset"} prints the collection of rules 
26782  613 
declared to the Simplifier, which is also known as ``simpset'' 
50063  614 
internally. 
615 

616 
For historical reasons, simpsets may occur independently from the 

617 
current context, but are conceptually dependent on it. When the 

618 
Simplifier is invoked via one of its main entry points in the Isar 

619 
source language (as proof method \secref{sec:simpmeth} or rule 

620 
attribute \secref{sec:simpmeth}), its simpset is derived from the 

621 
current proof context, and carries a backreference to that for 

622 
other tools that might get invoked internally (e.g.\ simplification 

623 
procedures \secref{sec:simproc}). A mismatch of the context of the 

624 
simpset and the context of the problem being simplified may lead to 

625 
unexpected results. 

26782  626 

50065  627 
\item @{attribute simp} declares simplification rules, by adding or 
628 
deleting them from the simpset within the theory or proof context. 

629 

630 
Internally, all rewrite rules have to be expressed as Pure 

631 
equalities, potentially with some conditions of arbitrary form. 

632 
Such rewrite rules in Pure are derived automatically from 

633 
objectlevel equations that are supplied by the user. 

26782  634 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

635 
\item @{attribute split} declares case split rules. 
26782  636 

45645  637 
\item @{attribute cong} declares congruence rules to the Simplifier 
638 
context. 

639 

640 
Congruence rules are equalities of the form @{text [display] 

641 
"\<dots> \<Longrightarrow> f ?x\<^sub>1 \<dots> ?x\<^sub>n = f ?y\<^sub>1 \<dots> ?y\<^sub>n"} 

642 

643 
This controls the simplification of the arguments of @{text f}. For 

644 
example, some arguments can be simplified under additional 

645 
assumptions: @{text [display] "?P\<^sub>1 \<longleftrightarrow> ?Q\<^sub>1 \<Longrightarrow> (?Q\<^sub>1 \<Longrightarrow> ?P\<^sub>2 \<longleftrightarrow> ?Q\<^sub>2) \<Longrightarrow> 

646 
(?P\<^sub>1 \<longrightarrow> ?P\<^sub>2) \<longleftrightarrow> (?Q\<^sub>1 \<longrightarrow> ?Q\<^sub>2)"} 

647 

648 
Given this rule, the simplifier assumes @{text "?Q\<^sub>1"} and extracts 

649 
rewrite rules from it when simplifying @{text "?P\<^sub>2"}. Such local 

650 
assumptions are effective for rewriting formulae such as @{text "x = 

651 
0 \<longrightarrow> y + x = y"}. 

652 

653 
%FIXME 

654 
%The local assumptions are also provided as theorems to the solver; 

655 
%see \secref{sec:simpsolver} below. 

656 

657 
\medskip The following congruence rule for bounded quantifiers also 

658 
supplies contextual information  about the bound variable: 

659 
@{text [display] "(?A = ?B) \<Longrightarrow> (\<And>x. x \<in> ?B \<Longrightarrow> ?P x \<longleftrightarrow> ?Q x) \<Longrightarrow> 

660 
(\<forall>x \<in> ?A. ?P x) \<longleftrightarrow> (\<forall>x \<in> ?B. ?Q x)"} 

661 

662 
\medskip This congruence rule for conditional expressions can 

663 
supply contextual information for simplifying the arms: 

664 
@{text [display] "?p = ?q \<Longrightarrow> (?q \<Longrightarrow> ?a = ?c) \<Longrightarrow> (\<not> ?q \<Longrightarrow> ?b = ?d) \<Longrightarrow> 

665 
(if ?p then ?a else ?b) = (if ?q then ?c else ?d)"} 

666 

667 
A congruence rule can also \emph{prevent} simplification of some 

668 
arguments. Here is an alternative congruence rule for conditional 

669 
expressions that conforms to nonstrict functional evaluation: 

670 
@{text [display] "?p = ?q \<Longrightarrow> (if ?p then ?a else ?b) = (if ?q then ?a else ?b)"} 

671 

672 
Only the first argument is simplified; the others remain unchanged. 

673 
This can make simplification much faster, but may require an extra 

674 
case split over the condition @{text "?q"} to prove the goal. 

50063  675 

676 
\end{description} 

50065  677 

678 
The implicit simpset of the theory context is propagated 

679 
monotonically through the theory hierarchy: forming a new theory, 

680 
the union of the simpsets of its imports are taken as starting 

681 
point. Also note that definitional packages like @{command 

682 
"datatype"}, @{command "primrec"}, @{command "fun"} routinely 

683 
declare Simplifier rules to the target context, while plain 

684 
@{command "definition"} is an exception in \emph{not} declaring 

685 
anything. 

686 

687 
\medskip It is up the user to manipulate the current simpset further 

688 
by explicitly adding or deleting theorems as simplification rules, 

689 
or installing other tools via simplification procedures 

690 
(\secref{sec:simproc}). Good simpsets are hard to design. Rules 

691 
that obviously simplify, like @{text "?n + 0 \<equiv> ?n"} are good 

692 
candidates for the implicit simpset, unless a special 

693 
nonnormalizing behavior of certain operations is intended. More 

694 
specific rules (such as distributive laws, which duplicate subterms) 

695 
should be added only for specific proof steps. Conversely, 

696 
sometimes a rule needs to be deleted just for some part of a proof. 

697 
The need of frequent additions or deletions may indicate a poorly 

698 
designed simpset. 

699 

700 
\begin{warn} 

701 
The union of simpsets from theory imports (as described above) is 

702 
not always a good starting point for the new theory. If some 

703 
ancestors have deleted simplification rules because they are no 

704 
longer wanted, while others have left those rules in, then the union 

705 
will contain the unwanted rules, and thus have to be deleted again 

706 
in the theory body. 

707 
\end{warn} 

45645  708 
*} 
709 

710 

50063  711 
subsection {* Configuration options \label{sec:simpconfig} *} 
712 

713 
text {* 

714 
\begin{tabular}{rcll} 

715 
@{attribute_def simp_depth_limit} & : & @{text attribute} & default @{text 100} \\ 

716 
@{attribute_def simp_trace} & : & @{text attribute} & default @{text false} \\ 

717 
@{attribute_def simp_trace_depth_limit} & : & @{text attribute} & default @{text 1} \\ 

718 
@{attribute_def simp_debug} & : & @{text attribute} & default @{text false} \\ 

719 
\end{tabular} 

720 
\medskip 

721 

722 
These configurations options control further aspects of the Simplifier. 

723 
See also \secref{sec:config}. 

724 

725 
\begin{description} 

726 

727 
\item @{attribute simp_depth_limit} limits the number of recursive 

728 
invocations of the Simplifier during conditional rewriting. 

729 

730 
\item @{attribute simp_trace} makes the Simplifier output internal 

731 
operations. This includes rewrite steps, but also bookkeeping like 

732 
modifications of the simpset. 

733 

734 
\item @{attribute simp_trace_depth_limit} limits the effect of 

735 
@{attribute simp_trace} to the given depth of recursive Simplifier 

736 
invocations (when solving conditions of rewrite rules). 

737 

738 
\item @{attribute simp_debug} makes the Simplifier output some extra 

739 
information about internal operations. This includes any attempted 

740 
invocation of simplification procedures. 

741 

742 
\end{description} 

743 
*} 

744 

745 

746 
subsection {* Simplification procedures \label{sec:simproc} *} 

26782  747 

42925  748 
text {* Simplification procedures are ML functions that produce proven 
749 
rewrite rules on demand. They are associated with higherorder 

750 
patterns that approximate the lefthand sides of equations. The 

751 
Simplifier first matches the current redex against one of the LHS 

752 
patterns; if this succeeds, the corresponding ML function is 

753 
invoked, passing the Simplifier context and redex term. Thus rules 

754 
may be specifically fashioned for particular situations, resulting 

755 
in a more powerful mechanism than term rewriting by a fixed set of 

756 
rules. 

757 

758 
Any successful result needs to be a (possibly conditional) rewrite 

759 
rule @{text "t \<equiv> u"} that is applicable to the current redex. The 

760 
rule will be applied just as any ordinary rewrite rule. It is 

761 
expected to be already in \emph{internal form}, bypassing the 

762 
automatic preprocessing of objectlevel equivalences. 

763 

26782  764 
\begin{matharray}{rcl} 
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

765 
@{command_def "simproc_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

766 
simproc & : & @{text attribute} \\ 
26782  767 
\end{matharray} 
768 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

769 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

770 
@@{command simproc_setup} @{syntax name} '(' (@{syntax term} + '') ')' '=' 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

771 
@{syntax text} \\ (@'identifier' (@{syntax nameref}+))? 
26782  772 
; 
773 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

774 
@@{attribute simproc} (('add' ':')?  'del' ':') (@{syntax name}+) 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

775 
"} 
26782  776 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

777 
\begin{description} 
26782  778 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

779 
\item @{command "simproc_setup"} defines a named simplification 
26782  780 
procedure that is invoked by the Simplifier whenever any of the 
781 
given term patterns match the current redex. The implementation, 

782 
which is provided as ML source text, needs to be of type @{ML_type 

783 
"morphism > simpset > cterm > thm option"}, where the @{ML_type 

784 
cterm} represents the current redex @{text r} and the result is 

785 
supposed to be some proven rewrite rule @{text "r \<equiv> r'"} (or a 

786 
generalized version), or @{ML NONE} to indicate failure. The 

787 
@{ML_type simpset} argument holds the full context of the current 

788 
Simplifier invocation, including the actual Isar proof context. The 

789 
@{ML_type morphism} informs about the difference of the original 

790 
compilation context wrt.\ the one of the actual application later 

791 
on. The optional @{keyword "identifier"} specifies theorems that 

792 
represent the logical content of the abstract theory of this 

793 
simproc. 

794 

795 
Morphisms and identifiers are only relevant for simprocs that are 

796 
defined within a local target context, e.g.\ in a locale. 

797 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

798 
\item @{text "simproc add: name"} and @{text "simproc del: name"} 
26782  799 
add or delete named simprocs to the current Simplifier context. The 
800 
default is to add a simproc. Note that @{command "simproc_setup"} 

801 
already adds the new simproc to the subsequent context. 

802 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

803 
\end{description} 
26782  804 
*} 
805 

806 

42925  807 
subsubsection {* Example *} 
808 

809 
text {* The following simplification procedure for @{thm 

810 
[source=false, show_types] unit_eq} in HOL performs finegrained 

811 
control over rule application, beyond higherorder pattern matching. 

812 
Declaring @{thm unit_eq} as @{attribute simp} directly would make 

813 
the simplifier loop! Note that a version of this simplification 

814 
procedure is already active in Isabelle/HOL. *} 

815 

816 
simproc_setup unit ("x::unit") = {* 

817 
fn _ => fn _ => fn ct => 

818 
if HOLogic.is_unit (term_of ct) then NONE 

819 
else SOME (mk_meta_eq @{thm unit_eq}) 

820 
*} 

821 

822 
text {* Since the Simplifier applies simplification procedures 

823 
frequently, it is important to make the failure check in ML 

824 
reasonably fast. *} 

825 

826 

50063  827 
subsection {* Forward simplification \label{sec:simpforward} *} 
26782  828 

829 
text {* 

830 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

831 
@{attribute_def simplified} & : & @{text attribute} \\ 
26782  832 
\end{matharray} 
833 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

834 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

835 
@@{attribute simplified} opt? @{syntax thmrefs}? 
26782  836 
; 
837 

40255
9ffbc25e1606
eliminated obsolete \_ escapes in rail environments;
wenzelm
parents:
35613
diff
changeset

838 
opt: '(' ('no_asm'  'no_asm_simp'  'no_asm_use') ')' 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

839 
"} 
26782  840 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

841 
\begin{description} 
26782  842 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

843 
\item @{attribute simplified}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} causes a theorem to 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

844 
be simplified, either by exactly the specified rules @{text "a\<^sub>1, \<dots>, 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

845 
a\<^sub>n"}, or the implicit Simplifier context if no arguments are given. 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

846 
The result is fully simplified by default, including assumptions and 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

847 
conclusion; the options @{text no_asm} etc.\ tune the Simplifier in 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

848 
the same way as the for the @{text simp} method. 
26782  849 

850 
Note that forward simplification restricts the simplifier to its 

851 
most basic operation of term rewriting; solver and looper tactics 

852 
\cite{isabelleref} are \emph{not} involved here. The @{text 

853 
simplified} attribute should be only rarely required under normal 

854 
circumstances. 

855 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

856 
\end{description} 
26782  857 
*} 
858 

859 

27040  860 
section {* The Classical Reasoner \label{sec:classical} *} 
26782  861 

42930  862 
subsection {* Basic concepts *} 
42927
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

863 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

864 
text {* Although Isabelle is generic, many users will be working in 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

865 
some extension of classical firstorder logic. Isabelle/ZF is built 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

866 
upon theory FOL, while Isabelle/HOL conceptually contains 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

867 
firstorder logic as a fragment. Theoremproving in predicate logic 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

868 
is undecidable, but many automated strategies have been developed to 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

869 
assist in this task. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

870 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

871 
Isabelle's classical reasoner is a generic package that accepts 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

872 
certain information about a logic and delivers a suite of automatic 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

873 
proof tools, based on rules that are classified and declared in the 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

874 
context. These proof procedures are slow and simplistic compared 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

875 
with highend automated theorem provers, but they can save 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

876 
considerable time and effort in practice. They can prove theorems 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

877 
such as Pelletier's \cite{pelletier86} problems 40 and 41 in a few 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

878 
milliseconds (including full proof reconstruction): *} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

879 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

880 
lemma "(\<exists>y. \<forall>x. F x y \<longleftrightarrow> F x x) \<longrightarrow> \<not> (\<forall>x. \<exists>y. \<forall>z. F z y \<longleftrightarrow> \<not> F z x)" 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

881 
by blast 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

882 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

883 
lemma "(\<forall>z. \<exists>y. \<forall>x. f x y \<longleftrightarrow> f x z \<and> \<not> f x x) \<longrightarrow> \<not> (\<exists>z. \<forall>x. f x z)" 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

884 
by blast 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

885 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

886 
text {* The proof tools are generic. They are not restricted to 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

887 
firstorder logic, and have been heavily used in the development of 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

888 
the Isabelle/HOL library and applications. The tactics can be 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

889 
traced, and their components can be called directly; in this manner, 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

890 
any proof can be viewed interactively. *} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

891 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

892 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

893 
subsubsection {* The sequent calculus *} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

894 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

895 
text {* Isabelle supports natural deduction, which is easy to use for 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

896 
interactive proof. But natural deduction does not easily lend 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

897 
itself to automation, and has a bias towards intuitionism. For 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

898 
certain proofs in classical logic, it can not be called natural. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

899 
The \emph{sequent calculus}, a generalization of natural deduction, 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

900 
is easier to automate. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

901 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

902 
A \textbf{sequent} has the form @{text "\<Gamma> \<turnstile> \<Delta>"}, where @{text "\<Gamma>"} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

903 
and @{text "\<Delta>"} are sets of formulae.\footnote{For firstorder 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

904 
logic, sequents can equivalently be made from lists or multisets of 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

905 
formulae.} The sequent @{text "P\<^sub>1, \<dots>, P\<^sub>m \<turnstile> Q\<^sub>1, \<dots>, Q\<^sub>n"} is 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

906 
\textbf{valid} if @{text "P\<^sub>1 \<and> \<dots> \<and> P\<^sub>m"} implies @{text "Q\<^sub>1 \<or> \<dots> \<or> 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

907 
Q\<^sub>n"}. Thus @{text "P\<^sub>1, \<dots>, P\<^sub>m"} represent assumptions, each of which 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

908 
is true, while @{text "Q\<^sub>1, \<dots>, Q\<^sub>n"} represent alternative goals. A 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

909 
sequent is \textbf{basic} if its left and right sides have a common 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

910 
formula, as in @{text "P, Q \<turnstile> Q, R"}; basic sequents are trivially 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

911 
valid. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

912 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

913 
Sequent rules are classified as \textbf{right} or \textbf{left}, 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

914 
indicating which side of the @{text "\<turnstile>"} symbol they operate on. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

915 
Rules that operate on the right side are analogous to natural 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

916 
deduction's introduction rules, and left rules are analogous to 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

917 
elimination rules. The sequent calculus analogue of @{text "(\<longrightarrow>I)"} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

918 
is the rule 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

919 
\[ 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

920 
\infer[@{text "(\<longrightarrow>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, P \<longrightarrow> Q"}}{@{text "P, \<Gamma> \<turnstile> \<Delta>, Q"}} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

921 
\] 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

922 
Applying the rule backwards, this breaks down some implication on 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

923 
the right side of a sequent; @{text "\<Gamma>"} and @{text "\<Delta>"} stand for 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

924 
the sets of formulae that are unaffected by the inference. The 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

925 
analogue of the pair @{text "(\<or>I1)"} and @{text "(\<or>I2)"} is the 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

926 
single rule 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

927 
\[ 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

928 
\infer[@{text "(\<or>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, P \<or> Q"}}{@{text "\<Gamma> \<turnstile> \<Delta>, P, Q"}} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

929 
\] 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

930 
This breaks down some disjunction on the right side, replacing it by 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

931 
both disjuncts. Thus, the sequent calculus is a kind of 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

932 
multipleconclusion logic. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

933 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

934 
To illustrate the use of multiple formulae on the right, let us 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

935 
prove the classical theorem @{text "(P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"}. Working 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

936 
backwards, we reduce this formula to a basic sequent: 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

937 
\[ 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

938 
\infer[@{text "(\<or>R)"}]{@{text "\<turnstile> (P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"}} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

939 
{\infer[@{text "(\<longrightarrow>R)"}]{@{text "\<turnstile> (P \<longrightarrow> Q), (Q \<longrightarrow> P)"}} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

940 
{\infer[@{text "(\<longrightarrow>R)"}]{@{text "P \<turnstile> Q, (Q \<longrightarrow> P)"}} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

941 
{@{text "P, Q \<turnstile> Q, P"}}}} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

942 
\] 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

943 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

944 
This example is typical of the sequent calculus: start with the 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

945 
desired theorem and apply rules backwards in a fairly arbitrary 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

946 
manner. This yields a surprisingly effective proof procedure. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

947 
Quantifiers add only few complications, since Isabelle handles 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

948 
parameters and schematic variables. See \cite[Chapter 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

949 
10]{paulsonml2} for further discussion. *} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

950 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

951 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

952 
subsubsection {* Simulating sequents by natural deduction *} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

953 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

954 
text {* Isabelle can represent sequents directly, as in the 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

955 
objectlogic LK. But natural deduction is easier to work with, and 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

956 
most objectlogics employ it. Fortunately, we can simulate the 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

957 
sequent @{text "P\<^sub>1, \<dots>, P\<^sub>m \<turnstile> Q\<^sub>1, \<dots>, Q\<^sub>n"} by the Isabelle formula 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

958 
@{text "P\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> P\<^sub>m \<Longrightarrow> \<not> Q\<^sub>2 \<Longrightarrow> ... \<Longrightarrow> \<not> Q\<^sub>n \<Longrightarrow> Q\<^sub>1"} where the order of 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

959 
the assumptions and the choice of @{text "Q\<^sub>1"} are arbitrary. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

960 
Elimresolution plays a key role in simulating sequent proofs. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

961 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

962 
We can easily handle reasoning on the left. Elimresolution with 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

963 
the rules @{text "(\<or>E)"}, @{text "(\<bottom>E)"} and @{text "(\<exists>E)"} achieves 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

964 
a similar effect as the corresponding sequent rules. For the other 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

965 
connectives, we use sequentstyle elimination rules instead of 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

966 
destruction rules such as @{text "(\<and>E1, 2)"} and @{text "(\<forall>E)"}. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

967 
But note that the rule @{text "(\<not>L)"} has no effect under our 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

968 
representation of sequents! 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

969 
\[ 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

970 
\infer[@{text "(\<not>L)"}]{@{text "\<not> P, \<Gamma> \<turnstile> \<Delta>"}}{@{text "\<Gamma> \<turnstile> \<Delta>, P"}} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

971 
\] 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

972 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

973 
What about reasoning on the right? Introduction rules can only 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

974 
affect the formula in the conclusion, namely @{text "Q\<^sub>1"}. The 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

975 
other rightside formulae are represented as negated assumptions, 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

976 
@{text "\<not> Q\<^sub>2, \<dots>, \<not> Q\<^sub>n"}. In order to operate on one of these, it 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

977 
must first be exchanged with @{text "Q\<^sub>1"}. Elimresolution with the 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

978 
@{text swap} rule has this effect: @{text "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

979 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

980 
To ensure that swaps occur only when necessary, each introduction 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

981 
rule is converted into a swapped form: it is resolved with the 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

982 
second premise of @{text "(swap)"}. The swapped form of @{text 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

983 
"(\<and>I)"}, which might be called @{text "(\<not>\<and>E)"}, is 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

984 
@{text [display] "\<not> (P \<and> Q) \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (\<not> R \<Longrightarrow> Q) \<Longrightarrow> R"} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

985 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

986 
Similarly, the swapped form of @{text "(\<longrightarrow>I)"} is 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

987 
@{text [display] "\<not> (P \<longrightarrow> Q) \<Longrightarrow> (\<not> R \<Longrightarrow> P \<Longrightarrow> Q) \<Longrightarrow> R"} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

988 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

989 
Swapped introduction rules are applied using elimresolution, which 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

990 
deletes the negated formula. Our representation of sequents also 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

991 
requires the use of ordinary introduction rules. If we had no 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

992 
regard for readability of intermediate goal states, we could treat 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

993 
the right side more uniformly by representing sequents as @{text 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

994 
[display] "P\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> P\<^sub>m \<Longrightarrow> \<not> Q\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> \<not> Q\<^sub>n \<Longrightarrow> \<bottom>"} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

995 
*} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

996 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

997 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

998 
subsubsection {* Extra rules for the sequent calculus *} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

999 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1000 
text {* As mentioned, destruction rules such as @{text "(\<and>E1, 2)"} and 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1001 
@{text "(\<forall>E)"} must be replaced by sequentstyle elimination rules. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1002 
In addition, we need rules to embody the classical equivalence 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1003 
between @{text "P \<longrightarrow> Q"} and @{text "\<not> P \<or> Q"}. The introduction 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1004 
rules @{text "(\<or>I1, 2)"} are replaced by a rule that simulates 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1005 
@{text "(\<or>R)"}: @{text [display] "(\<not> Q \<Longrightarrow> P) \<Longrightarrow> P \<or> Q"} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1006 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1007 
The destruction rule @{text "(\<longrightarrow>E)"} is replaced by @{text [display] 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1008 
"(P \<longrightarrow> Q) \<Longrightarrow> (\<not> P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1009 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1010 
Quantifier replication also requires special rules. In classical 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1011 
logic, @{text "\<exists>x. P x"} is equivalent to @{text "\<not> (\<forall>x. \<not> P x)"}; 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1012 
the rules @{text "(\<exists>R)"} and @{text "(\<forall>L)"} are dual: 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1013 
\[ 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1014 
\infer[@{text "(\<exists>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, \<exists>x. P x"}}{@{text "\<Gamma> \<turnstile> \<Delta>, \<exists>x. P x, P t"}} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1015 
\qquad 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1016 
\infer[@{text "(\<forall>L)"}]{@{text "\<forall>x. P x, \<Gamma> \<turnstile> \<Delta>"}}{@{text "P t, \<forall>x. P x, \<Gamma> \<turnstile> \<Delta>"}} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1017 
\] 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1018 
Thus both kinds of quantifier may be replicated. Theorems requiring 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1019 
multiple uses of a universal formula are easy to invent; consider 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1020 
@{text [display] "(\<forall>x. P x \<longrightarrow> P (f x)) \<and> P a \<longrightarrow> P (f\<^sup>n a)"} for any 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1021 
@{text "n > 1"}. Natural examples of the multiple use of an 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1022 
existential formula are rare; a standard one is @{text "\<exists>x. \<forall>y. P x 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1023 
\<longrightarrow> P y"}. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1024 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1025 
Forgoing quantifier replication loses completeness, but gains 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1026 
decidability, since the search space becomes finite. Many useful 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1027 
theorems can be proved without replication, and the search generally 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1028 
delivers its verdict in a reasonable time. To adopt this approach, 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1029 
represent the sequent rules @{text "(\<exists>R)"}, @{text "(\<exists>L)"} and 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1030 
@{text "(\<forall>R)"} by @{text "(\<exists>I)"}, @{text "(\<exists>E)"} and @{text "(\<forall>I)"}, 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1031 
respectively, and put @{text "(\<forall>E)"} into elimination form: @{text 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1032 
[display] "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q"} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1033 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1034 
Elimresolution with this rule will delete the universal formula 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1035 
after a single use. To replicate universal quantifiers, replace the 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1036 
rule by @{text [display] "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q) \<Longrightarrow> Q"} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1037 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1038 
To replicate existential quantifiers, replace @{text "(\<exists>I)"} by 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1039 
@{text [display] "(\<not> (\<exists>x. P x) \<Longrightarrow> P t) \<Longrightarrow> \<exists>x. P x"} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1040 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1041 
All introduction rules mentioned above are also useful in swapped 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1042 
form. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1043 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1044 
Replication makes the search space infinite; we must apply the rules 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1045 
with care. The classical reasoner distinguishes between safe and 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1046 
unsafe rules, applying the latter only when there is no alternative. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1047 
Depthfirst search may well go down a blind alley; bestfirst search 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1048 
is better behaved in an infinite search space. However, quantifier 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1049 
replication is too expensive to prove any but the simplest theorems. 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1050 
*} 
c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1051 

c40adab7568e
moved/updated introduction to Classical Reasoner;
wenzelm
parents:
42925
diff
changeset

1052 

42928
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1053 
subsection {* Rule declarations *} 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1054 

9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1055 
text {* The proof tools of the Classical Reasoner depend on 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1056 
collections of rules declared in the context, which are classified 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1057 
as introduction, elimination or destruction and as \emph{safe} or 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1058 
\emph{unsafe}. In general, safe rules can be attempted blindly, 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1059 
while unsafe rules must be used with care. A safe rule must never 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1060 
reduce a provable goal to an unprovable set of subgoals. 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1061 

9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1062 
The rule @{text "P \<Longrightarrow> P \<or> Q"} is unsafe because it reduces @{text "P 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1063 
\<or> Q"} to @{text "P"}, which might turn out as premature choice of an 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1064 
unprovable subgoal. Any rule is unsafe whose premises contain new 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1065 
unknowns. The elimination rule @{text "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q"} is 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1066 
unsafe, since it is applied via elimresolution, which discards the 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1067 
assumption @{text "\<forall>x. P x"} and replaces it by the weaker 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1068 
assumption @{text "P t"}. The rule @{text "P t \<Longrightarrow> \<exists>x. P x"} is 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1069 
unsafe for similar reasons. The quantifier duplication rule @{text 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1070 
"\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q) \<Longrightarrow> Q"} is unsafe in a different sense: 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1071 
since it keeps the assumption @{text "\<forall>x. P x"}, it is prone to 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1072 
looping. In classical firstorder logic, all rules are safe except 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1073 
those mentioned above. 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1074 

9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1075 
The safe~/ unsafe distinction is vague, and may be regarded merely 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1076 
as a way of giving some rules priority over others. One could argue 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1077 
that @{text "(\<or>E)"} is unsafe, because repeated application of it 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1078 
could generate exponentially many subgoals. Induction rules are 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1079 
unsafe because inductive proofs are difficult to set up 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1080 
automatically. Any inference is unsafe that instantiates an unknown 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1081 
in the proof state  thus matching must be used, rather than 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1082 
unification. Even proof by assumption is unsafe if it instantiates 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1083 
unknowns shared with other subgoals. 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1084 

9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1085 
\begin{matharray}{rcl} 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1086 
@{command_def "print_claset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1087 
@{attribute_def intro} & : & @{text attribute} \\ 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1088 
@{attribute_def elim} & : & @{text attribute} \\ 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1089 
@{attribute_def dest} & : & @{text attribute} \\ 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1090 
@{attribute_def rule} & : & @{text attribute} \\ 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1091 
@{attribute_def iff} & : & @{text attribute} \\ 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1092 
@{attribute_def swapped} & : & @{text attribute} \\ 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1093 
\end{matharray} 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1094 

9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1095 
@{rail " 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1096 
(@@{attribute intro}  @@{attribute elim}  @@{attribute dest}) ('!'  ()  '?') @{syntax nat}? 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1097 
; 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1098 
@@{attribute rule} 'del' 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1099 
; 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1100 
@@{attribute iff} (((()  'add') '?'?)  'del') 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1101 
"} 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1102 

9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1103 
\begin{description} 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1104 

9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1105 
\item @{command "print_claset"} prints the collection of rules 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1106 
declared to the Classical Reasoner, i.e.\ the @{ML_type claset} 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1107 
within the context. 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1108 

9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1109 
\item @{attribute intro}, @{attribute elim}, and @{attribute dest} 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1110 
declare introduction, elimination, and destruction rules, 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1111 
respectively. By default, rules are considered as \emph{unsafe} 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1112 
(i.e.\ not applied blindly without backtracking), while ``@{text 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1113 
"!"}'' classifies as \emph{safe}. Rule declarations marked by 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1114 
``@{text "?"}'' coincide with those of Isabelle/Pure, cf.\ 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1115 
\secref{sec:puremethatt} (i.e.\ are only applied in single steps 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1116 
of the @{method rule} method). The optional natural number 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1117 
specifies an explicit weight argument, which is ignored by the 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1118 
automated reasoning tools, but determines the search order of single 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1119 
rule steps. 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1120 

9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1121 
Introduction rules are those that can be applied using ordinary 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1122 
resolution. Their swapped forms are generated internally, which 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1123 
will be applied using elimresolution. Elimination rules are 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1124 
applied using elimresolution. Rules are sorted by the number of 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1125 
new subgoals they will yield; rules that generate the fewest 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1126 
subgoals will be tried first. Otherwise, later declarations take 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1127 
precedence over earlier ones. 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1128 

9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1129 
Rules already present in the context with the same classification 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1130 
are ignored. A warning is printed if the rule has already been 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1131 
added with some other classification, but the rule is added anyway 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1132 
as requested. 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1133 

9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1134 
\item @{attribute rule}~@{text del} deletes all occurrences of a 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1135 
rule from the classical context, regardless of its classification as 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1136 
introduction~/ elimination~/ destruction and safe~/ unsafe. 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1137 

9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1138 
\item @{attribute iff} declares logical equivalences to the 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1139 
Simplifier and the Classical reasoner at the same time. 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1140 
Nonconditional rules result in a safe introduction and elimination 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1141 
pair; conditional ones are considered unsafe. Rules with negative 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1142 
conclusion are automatically inverted (using @{text "\<not>"}elimination 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1143 
internally). 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1144 

9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1145 
The ``@{text "?"}'' version of @{attribute iff} declares rules to 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1146 
the Isabelle/Pure context only, and omits the Simplifier 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1147 
declaration. 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1148 

9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1149 
\item @{attribute swapped} turns an introduction rule into an 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1150 
elimination, by resolving with the classical swap principle @{text 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1151 
"\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"} in the second position. This is mainly for 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1152 
illustrative purposes: the Classical Reasoner already swaps rules 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1153 
internally as explained above. 
9d946de41120
updated and reunified classical rule declarations;
wenzelm
parents:
42927
diff
changeset

1154 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

1155 
\end{description} 
26782  1156 
*} 
1157 

1158 

43365  1159 
subsection {* Structured methods *} 
1160 

1161 
text {* 

1162 
\begin{matharray}{rcl} 

1163 
@{method_def rule} & : & @{text method} \\ 

1164 
@{method_def contradiction} & : & @{text method} \\ 

1165 
\end{matharray} 

1166 

1167 
@{rail " 

1168 
@@{method rule} @{syntax thmrefs}? 

1169 
"} 

1170 

1171 
\begin{description} 

1172 

1173 
\item @{method rule} as offered by the Classical Reasoner is a 

1174 
refinement over the Pure one (see \secref{sec:puremethatt}). Both 

1175 
versions work the same, but the classical version observes the 

1176 
classical rule context in addition to that of Isabelle/Pure. 

1177 

1178 
Common object logics (HOL, ZF, etc.) declare a rich collection of 

1179 
classical rules (even if these would qualify as intuitionistic 

1180 
ones), but only few declarations to the rule context of 

1181 
Isabelle/Pure (\secref{sec:puremethatt}). 

1182 

1183 
\item @{method contradiction} solves some goal by contradiction, 

1184 
deriving any result from both @{text "\<not> A"} and @{text A}. Chained 

1185 
facts, which are guaranteed to participate, may appear in either 

1186 
order. 

1187 

1188 
\end{description} 

1189 
*} 

1190 

1191 

27040  1192 
subsection {* Automated methods *} 
26782  1193 

1194 
text {* 

1195 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1196 
@{method_def blast} & : & @{text method} \\ 
42930  1197 
@{method_def auto} & : & @{text method} \\ 
1198 
@{method_def force} & : & @{text method} \\ 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1199 
@{method_def fast} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1200 
@{method_def slow} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1201 
@{method_def best} & : & @{text method} \\ 
44911  1202 
@{method_def fastforce} & : & @{text method} \\ 
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1203 
@{method_def slowsimp} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1204 
@{method_def bestsimp} & : & @{text method} \\ 
43367  1205 
@{method_def deepen} & : & @{text method} \\ 
26782  1206 
\end{matharray} 
1207 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

1208 
@{rail " 
42930  1209 
@@{method blast} @{syntax nat}? (@{syntax clamod} * ) 
1210 
; 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

1211 
@@{method auto} (@{syntax nat} @{syntax nat})? (@{syntax clasimpmod} * ) 
26782  1212 
; 
42930  1213 
@@{method force} (@{syntax clasimpmod} * ) 
1214 
; 

1215 
(@@{method fast}  @@{method slow}  @@{method best}) (@{syntax clamod} * ) 

26782  1216 
; 
44911  1217 
(@@{method fastforce}  @@{method slowsimp}  @@{method bestsimp}) 
42930  1218 
(@{syntax clasimpmod} * ) 
1219 
; 

43367  1220 
@@{method deepen} (@{syntax nat} ?) (@{syntax clamod} * ) 
1221 
; 

42930  1222 
@{syntax_def clamod}: 
1223 
(('intro'  'elim'  'dest') ('!'  ()  '?')  'del') ':' @{syntax thmrefs} 

1224 
; 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

1225 
@{syntax_def clasimpmod}: ('simp' (()  'add'  'del'  'only')  
26782  1226 
('cong'  'split') (()  'add'  'del')  
1227 
'iff' (((()  'add') '?'?)  'del')  

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

1228 
(('intro'  'elim'  'dest') ('!'  ()  '?')  'del')) ':' @{syntax thmrefs} 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40291
diff
changeset

1229 
"} 
26782  1230 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28754
diff
changeset

1231 
\begin{description} 
26782  1232 

42930  1233 
\item @{method blast} is a separate classical tableau prover that 
1234 
uses the same classical rule declarations as explained before. 

1235 

1236 
Proof search is coded directly in ML using special data structures. 

1237 
A successful proof is then reconstructed using regular Isabelle 

1238 
inferences. It is faster and more powerful than the other classical 

1239 
reasoning tools, but has major limitations too. 

1240 

1241 
\begin{itemize} 

1242 

1243 
\item It does not use the classical wrapper tacticals, such as the 

44911  1244 
integration with the Simplifier of @{method fastforce}. 
42930  1245 

1246 
\item It does not perform higherorder unification, as needed by the 

1247 
rule @{thm [source=false] rangeI} in HOL. There are often 

1248 
alternatives to such rules, for example @{thm [source=false] 

1249 
range_eqI}. 

1250 

1251 
\item Function variables may only be applied to parameters of the 

1252 
subgoal. (This restriction arises because the prover does not use 

1253 
higherorder unification.) If other function variables are present 

1254 
then the prover will fail with the message \texttt{Function Var's 

1255 
argument not a bound variable}. 

1256 

1257 
\item Its proof strategy is more general than @{method fast} but can 

1258 
be slower. If @{method blast} fails or seems to be running forever, 

1259 
try @{method fast} and the other proof tools described below. 

1260 

1261 
\end{itemize} 

1262 

1263 
The optional integer argument specifies a bound for the number of 

1264 
unsafe steps used in a proof. By default, @{method blast} starts 

1265 
with a bound of 0 and increases it successively to 20. In contrast, 

1266 
@{text "(blast lim)"} tries to prove the goal using a search bound 

1267 
of @{text "lim"}. Sometimes a slow proof using @{method blast} can 

1268 
be made much faster by supplying the successful search bound to this 

1269 
proof method instead. 

1270 

1271 
\item @{method auto} combines classical reasoning with 

1272 
simplification. It is intended for situations where there are a lot 

1273 
of mostly trivial subgoals; it proves all the easy ones, leaving the 

1274 
ones it cannot prove. Occasionally, attempting to prove the hard 
