summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Doc/Isar_Ref/Generic.thy

author | wenzelm |

Wed Mar 25 11:39:52 2015 +0100 (2015-03-25) | |

changeset 59809 | 87641097d0f3 |

parent 59785 | 4e6ab5831cc0 |

child 59853 | 4039d8aecda4 |

permissions | -rw-r--r-- |

tuned signature;

1 theory Generic

2 imports Base Main

3 begin

5 chapter \<open>Generic tools and packages \label{ch:gen-tools}\<close>

7 section \<open>Configuration options \label{sec:config}\<close>

9 text \<open>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

17 commands such as @{command "declare"} or @{command "using"} like

18 this:

19 \<close>

21 declare [[show_main_goal = false]]

23 notepad

24 begin

25 note [[show_main_goal = true]]

26 end

28 text \<open>For historical reasons, some tools cannot take the full proof

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.

33 \begin{matharray}{rcll}

34 @{command_def "print_options"} & : & @{text "context \<rightarrow>"} \\

35 \end{matharray}

37 @{rail \<open>

38 @{syntax name} ('=' ('true' | 'false' | @{syntax int} | @{syntax float} | @{syntax name}))?

39 \<close>}

41 \begin{description}

43 \item @{command "print_options"} prints the available configuration

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

46 \item @{text "name = value"} as an attribute expression modifies the

47 named option, with the syntax of the value depending on the option's

48 type. For @{ML_type bool} the default value is @{text true}. Any

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

51 \end{description}

52 \<close>

55 section \<open>Basic proof tools\<close>

57 subsection \<open>Miscellaneous methods and attributes \label{sec:misc-meth-att}\<close>

59 text \<open>

60 \begin{matharray}{rcl}

61 @{method_def unfold} & : & @{text method} \\

62 @{method_def fold} & : & @{text method} \\

63 @{method_def insert} & : & @{text method} \\[0.5ex]

64 @{method_def erule}@{text "\<^sup>*"} & : & @{text method} \\

65 @{method_def drule}@{text "\<^sup>*"} & : & @{text method} \\

66 @{method_def frule}@{text "\<^sup>*"} & : & @{text method} \\

67 @{method_def intro} & : & @{text method} \\

68 @{method_def elim} & : & @{text method} \\

69 @{method_def succeed} & : & @{text method} \\

70 @{method_def fail} & : & @{text method} \\

71 \end{matharray}

73 @{rail \<open>

74 (@@{method fold} | @@{method unfold} | @@{method insert}) @{syntax thmrefs}

75 ;

76 (@@{method erule} | @@{method drule} | @@{method frule})

77 ('(' @{syntax nat} ')')? @{syntax thmrefs}

78 ;

79 (@@{method intro} | @@{method elim}) @{syntax thmrefs}?

80 \<close>}

82 \begin{description}

84 \item @{method unfold}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{method fold}~@{text

85 "a\<^sub>1 \<dots> a\<^sub>n"} expand (or fold back) the given definitions throughout

86 all goals; any chained facts provided are inserted into the goal and

87 subject to rewriting as well.

89 \item @{method insert}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} inserts theorems as facts

90 into all goals of the proof state. Note that current facts

91 indicated for forward chaining are ignored.

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:pure-meth-att}), but apply rules by

97 elim-resolution, destruct-resolution, and forward-resolution,

98 respectively @{cite "isabelle-implementation"}. The optional natural

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

100 be performed here.

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 single-step elimination would be done using

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

108 facts.

110 \item @{method intro} and @{method elim} repeatedly refine some goal

111 by intro- or elim-resolution, after having inserted any chained

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

113 this allows fine-tuned decomposition of a proof problem, in contrast

114 to common automated tools.

116 \item @{method succeed} yields a single (unchanged) result; it is

117 the identity of the ``@{text ","}'' method combinator (cf.\

118 \secref{sec:proof-meth}).

120 \item @{method fail} yields an empty result sequence; it is the

121 identity of the ``@{text "|"}'' method combinator (cf.\

122 \secref{sec:proof-meth}).

124 \end{description}

126 \begin{matharray}{rcl}

127 @{attribute_def tagged} & : & @{text attribute} \\

128 @{attribute_def untagged} & : & @{text attribute} \\[0.5ex]

129 @{attribute_def THEN} & : & @{text attribute} \\

130 @{attribute_def unfolded} & : & @{text attribute} \\

131 @{attribute_def folded} & : & @{text attribute} \\

132 @{attribute_def abs_def} & : & @{text attribute} \\[0.5ex]

133 @{attribute_def rotated} & : & @{text attribute} \\

134 @{attribute_def (Pure) elim_format} & : & @{text attribute} \\

135 @{attribute_def no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\

136 \end{matharray}

138 @{rail \<open>

139 @@{attribute tagged} @{syntax name} @{syntax name}

140 ;

141 @@{attribute untagged} @{syntax name}

142 ;

143 @@{attribute THEN} ('[' @{syntax nat} ']')? @{syntax thmref}

144 ;

145 (@@{attribute unfolded} | @@{attribute folded}) @{syntax thmrefs}

146 ;

147 @@{attribute rotated} @{syntax int}?

148 \<close>}

150 \begin{description}

152 \item @{attribute tagged}~@{text "name value"} and @{attribute

153 untagged}~@{text name} add and remove \emph{tags} of some theorem.

154 Tags may be any list of string pairs that serve as formal comment.

155 The first string is considered the tag name, the second its value.

156 Note that @{attribute untagged} removes any tags of the same name.

158 \item @{attribute THEN}~@{text a} composes rules by resolution; it

159 resolves with the first premise of @{text a} (an alternative

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

161 @{cite "isabelle-implementation"}.

163 \item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute

164 folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given

165 definitions throughout a rule.

167 \item @{attribute abs_def} turns an equation of the form @{prop "f x

168 y \<equiv> t"} into @{prop "f \<equiv> \<lambda>x y. t"}, which ensures that @{method

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

170 for object-logic equality.

172 \item @{attribute rotated}~@{text n} rotate the premises of a

173 theorem by @{text n} (default 1).

175 \item @{attribute (Pure) elim_format} turns a destruction rule into

176 elimination rule format, by resolving with the rule @{prop "PROP A \<Longrightarrow>

177 (PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}.

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

180 its own version of this operation.

182 \item @{attribute no_vars} replaces schematic variables by free

183 ones; this is mainly for tuning output of pretty printed theorems.

185 \end{description}

186 \<close>

189 subsection \<open>Low-level equational reasoning\<close>

191 text \<open>

192 \begin{matharray}{rcl}

193 @{method_def subst} & : & @{text method} \\

194 @{method_def hypsubst} & : & @{text method} \\

195 @{method_def split} & : & @{text method} \\

196 \end{matharray}

198 @{rail \<open>

199 @@{method subst} ('(' 'asm' ')')? \<newline> ('(' (@{syntax nat}+) ')')? @{syntax thmref}

200 ;

201 @@{method split} @{syntax thmrefs}

202 \<close>}

204 These methods provide low-level facilities for equational reasoning

205 that are intended for specialized applications only. Normally,

206 single step calculations would be performed in a structured text

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

208 provide the canonical way for automated normalization (see

209 \secref{sec:simplifier}).

211 \begin{description}

213 \item @{method subst}~@{text eq} performs a single substitution step

214 using rule @{text eq}, which may be either a meta or object

215 equality.

217 \item @{method subst}~@{text "(asm) eq"} substitutes in an

218 assumption.

220 \item @{method subst}~@{text "(i \<dots> j) eq"} performs several

221 substitutions in the conclusion. The numbers @{text i} to @{text j}

222 indicate the positions to substitute at. Positions are ordered from

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

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

225 where commutativity of @{text "+"} is applicable: 1 refers to @{text

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

228 If the positions in the list @{text "(i \<dots> j)"} are non-overlapping

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

230 assume all substitutions are performed simultaneously. Otherwise

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

233 \item @{method subst}~@{text "(asm) (i \<dots> j) eq"} performs the

234 substitutions in the assumptions. The positions refer to the

235 assumptions in order from left to right. For example, given in a

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

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

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

240 \item @{method hypsubst} performs substitution using some

241 assumption; this only works for equations of the form @{text "x =

242 t"} where @{text x} is a free or bound variable.

244 \item @{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} performs single-step case

245 splitting using the given rules. Splitting is performed in the

246 conclusion or some assumption of the subgoal, depending of the

247 structure of the rule.

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

250 application of split rules as declared in the current context, using

251 @{attribute split}, for example.

253 \end{description}

254 \<close>

257 subsection \<open>Further tactic emulations \label{sec:tactics}\<close>

259 text \<open>

260 The following improper proof methods emulate traditional tactics.

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

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

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

264 scope of some subgoal.

266 \begin{warn}

267 Dynamic instantiations refer to universally quantified parameters

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

269 term abbreviations of a (static) Isar context.

270 \end{warn}

272 Tactic emulation methods, unlike their ML counterparts, admit

273 simultaneous instantiation from both dynamic and static contexts.

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

275 variables. Likewise, schematic variables refer to term

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

277 schematic variable is interpreted as a schematic variable and left

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

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

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

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

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

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

285 \secref{sec:pure-meth-att}).

287 \begin{matharray}{rcl}

288 @{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\

289 @{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\

290 @{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\

291 @{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\

292 @{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\

293 @{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\

294 @{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\

295 @{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\

296 @{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\

297 @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\

298 @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\

299 \end{matharray}

301 @{rail \<open>

302 (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |

303 @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>

304 ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )

305 ;

306 dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and') @{syntax for_fixes}

307 ;

308 @@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}

309 ;

310 @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) @{syntax for_fixes}

311 ;

312 @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)

313 ;

314 @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?

315 ;

316 (@@{method tactic} | @@{method raw_tactic}) @{syntax text}

317 \<close>}

319 \begin{description}

321 \item @{method rule_tac} etc. do resolution of rules with explicit

322 instantiation. This works the same way as the ML tactics @{ML

323 Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}).

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

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

327 @{cite "isabelle-implementation"}).

329 \item @{method cut_tac} inserts facts into the proof state as

330 assumption of a subgoal; instantiations may be given as well. Note

331 that the scope of schematic variables is spread over the main goal

332 statement and rule premises are turned into new subgoals. This is

333 in contrast to the regular method @{method insert} which inserts

334 closed rule statements.

336 \item @{method thin_tac}~@{text \<phi>} deletes the specified premise

337 from a subgoal. Note that @{text \<phi>} may contain schematic

338 variables, to abbreviate the intended proposition; the first

339 matching subgoal premise will be deleted. Removing useless premises

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

341 run faster.

343 \item @{method subgoal_tac}~@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} adds the propositions

344 @{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} as local premises to a subgoal, and poses the same

345 as new subgoals (in the original context).

347 \item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a

348 goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the

349 \emph{suffix} of variables.

351 \item @{method rotate_tac}~@{text n} rotates the premises of a

352 subgoal by @{text n} positions: from right to left if @{text n} is

353 positive, and from left to right if @{text n} is negative; the

354 default value is 1.

356 \item @{method tactic}~@{text "text"} produces a proof method from

357 any ML text of type @{ML_type tactic}. Apart from the usual ML

358 environment and the current proof context, the ML code may refer to

359 the locally bound values @{ML_text facts}, which indicates any

360 current facts used for forward-chaining.

362 \item @{method raw_tactic} is similar to @{method tactic}, but

363 presents the goal state in its raw internal form, where simultaneous

364 subgoals appear as conjunction of the logical framework instead of

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

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

367 appear in production theories.

369 \end{description}

370 \<close>

373 section \<open>The Simplifier \label{sec:simplifier}\<close>

375 text \<open>The Simplifier performs conditional and unconditional

376 rewriting and uses contextual information: rule declarations in the

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

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

379 There are several general hooks that allow to modify the

380 simplification strategy, or incorporate other proof tools that solve

381 sub-problems, produce rewrite rules on demand etc.

383 The rewriting strategy is always strictly bottom up, except for

384 congruence rules, which are applied while descending into a term.

385 Conditions in conditional rewrite rules are solved recursively

386 before the rewrite rule is applied.

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 general-purpose proof tool with the main focus on equational

392 reasoning, and a bit more than that.

393 \<close>

396 subsection \<open>Simplification methods \label{sec:simp-meth}\<close>

398 text \<open>

399 \begin{tabular}{rcll}

400 @{method_def simp} & : & @{text method} \\

401 @{method_def simp_all} & : & @{text method} \\

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

403 \end{tabular}

404 \medskip

406 @{rail \<open>

407 (@@{method simp} | @@{method simp_all}) opt? (@{syntax simpmod} * )

408 ;

410 opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'

411 ;

412 @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') |

413 'cong' (() | 'add' | 'del')) ':' @{syntax thmrefs}

414 \<close>}

416 \begin{description}

418 \item @{method simp} invokes the Simplifier on the first subgoal,

419 after inserting chained facts as additional goal premises; further

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

421 The proof method fails if the subgoal remains unchanged after

422 simplification.

424 Note that the original goal premises and chained facts are subject

425 to simplification themselves, while declarations via @{text

426 "add"}/@{text "del"} merely follow the policies of the object-logic

427 to extract rewrite rules from theorems, without further

428 simplification. This may lead to slightly different behavior in

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

430 boundary situations to perform the intended simplification step!

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

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

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

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

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

437 non-trivial tools like linear arithmetic in HOL. The latter may

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

439 compared to English!

441 \medskip The @{text split} modifiers add or delete rules for the

442 Splitter (see also \secref{sec:simp-strategies} on the looper).

443 This works only if the Simplifier method has been properly setup to

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

445 ZF do this already).

447 There is also a separate @{method_ref split} method available for

448 single-step case splitting. The effect of repeatedly applying

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

450 split: thms)"}''.

452 \medskip The @{text cong} modifiers add or delete Simplifier

453 congruence rules (see also \secref{sec:simp-rules}); the default is

454 to add.

456 \item @{method simp_all} is similar to @{method simp}, but acts on

457 all goals, working backwards from the last to the first one as usual

458 in Isabelle.\footnote{The order is irrelevant for goals without

459 schematic variables, so simplification might actually be performed

460 in parallel here.}

462 Chained facts are inserted into all subgoals, before the

463 simplification process starts. Further rule declarations are the

464 same as for @{method simp}.

466 The proof method fails if all subgoals remain unchanged after

467 simplification.

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

470 invocations of the Simplifier during conditional rewriting.

472 \end{description}

474 By default the Simplifier methods above take local assumptions fully

475 into account, using equational assumptions in the subsequent

476 normalization process, or simplifying assumptions themselves.

477 Further options allow to fine-tune the behavior of the Simplifier

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

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

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

482 \begin{center}

483 \small

484 \begin{tabular}{|l|l|p{0.3\textwidth}|}

485 \hline

486 Isar method & ML tactic & behavior \\\hline

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

489 completely \\\hline

491 @{text "(simp (no_asm_simp))"} & @{ML asm_simp_tac} & assumptions

492 are used in the simplification of the conclusion but are not

493 themselves simplified \\\hline

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

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

497 or the conclusion \\\hline

499 @{text "(simp)"} & @{ML asm_full_simp_tac} & assumptions are used in

500 the simplification of the conclusion and to simplify other

501 assumptions \\\hline

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

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

505 are to the right of it \\\hline

507 \end{tabular}

508 \end{center}

509 \<close>

512 subsubsection \<open>Examples\<close>

514 text \<open>We consider basic algebraic simplifications in Isabelle/HOL.

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

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

517 \<close>

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

521 text \<open>The above attempt \emph{fails}, because @{term "0"} and @{term

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

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

524 types are required to get access to certain standard simplifications

525 of the theory context, e.g.\ like this:\<close>

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

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

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

531 text \<open>

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

533 the simplification process. For example:

534 \<close>

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

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

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

540 text \<open>As seen above, local assumptions that shall contribute to

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

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

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

544 different reasons.

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

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

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

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

550 terminate. The Simplifier notices certain simple forms of

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

552 nonetheless, by ignoring assumptions via special options as

553 explained before:

554 \<close>

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

557 by (simp (no_asm))

559 text \<open>The latter form is typical for long unstructured proof

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

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

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

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

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

565 local proof body as follows:

566 \<close>

568 lemma

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

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

572 notepad

573 begin

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

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

576 end

578 text \<open>\medskip Because assumptions may simplify each other, there

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

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

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

582 \[

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

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

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

586 \]

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

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

589 \<close>

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

592 apply simp

593 oops

595 text \<open>See also \secref{sec:simp-trace} for options to enable

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

597 rewrite systems.

598 \<close>

601 subsection \<open>Declaring rules \label{sec:simp-rules}\<close>

603 text \<open>

604 \begin{matharray}{rcl}

605 @{attribute_def simp} & : & @{text attribute} \\

606 @{attribute_def split} & : & @{text attribute} \\

607 @{attribute_def cong} & : & @{text attribute} \\

608 @{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

609 \end{matharray}

611 @{rail \<open>

612 (@@{attribute simp} | @@{attribute split} | @@{attribute cong})

613 (() | 'add' | 'del')

614 \<close>}

616 \begin{description}

618 \item @{attribute simp} declares rewrite rules, by adding or

619 deleting them from the simpset within the theory or proof context.

620 Rewrite rules are theorems expressing some form of equality, for

621 example:

623 @{text "Suc ?m + ?n = ?m + Suc ?n"} \\

624 @{text "?P \<and> ?P \<longleftrightarrow> ?P"} \\

625 @{text "?A \<union> ?B \<equiv> {x. x \<in> ?A \<or> x \<in> ?B}"}

627 \smallskip

628 Conditional rewrites such as @{text "?m < ?n \<Longrightarrow> ?m div ?n = 0"} are

629 also permitted; the conditions can be arbitrary formulas.

631 \medskip Internally, all rewrite rules are translated into Pure

632 equalities, theorems with conclusion @{text "lhs \<equiv> rhs"}. The

633 simpset contains a function for extracting equalities from arbitrary

634 theorems, which is usually installed when the object-logic is

635 configured initially. For example, @{text "\<not> ?x \<in> {}"} could be

636 turned into @{text "?x \<in> {} \<equiv> False"}. Theorems that are declared as

637 @{attribute simp} and local assumptions within a goal are treated

638 uniformly in this respect.

640 The Simplifier accepts the following formats for the @{text "lhs"}

641 term:

643 \begin{enumerate}

645 \item First-order patterns, considering the sublanguage of

646 application of constant operators to variable operands, without

647 @{text "\<lambda>"}-abstractions or functional variables.

648 For example:

650 @{text "(?x + ?y) + ?z \<equiv> ?x + (?y + ?z)"} \\

651 @{text "f (f ?x ?y) ?z \<equiv> f ?x (f ?y ?z)"}

653 \item Higher-order patterns in the sense of @{cite "nipkow-patterns"}.

654 These are terms in @{text "\<beta>"}-normal form (this will always be the

655 case unless you have done something strange) where each occurrence

656 of an unknown is of the form @{text "?F x\<^sub>1 \<dots> x\<^sub>n"}, where the

657 @{text "x\<^sub>i"} are distinct bound variables.

659 For example, @{text "(\<forall>x. ?P x \<and> ?Q x) \<equiv> (\<forall>x. ?P x) \<and> (\<forall>x. ?Q x)"}

660 or its symmetric form, since the @{text "rhs"} is also a

661 higher-order pattern.

663 \item Physical first-order patterns over raw @{text "\<lambda>"}-term

664 structure without @{text "\<alpha>\<beta>\<eta>"}-equality; abstractions and bound

665 variables are treated like quasi-constant term material.

667 For example, the rule @{text "?f ?x \<in> range ?f = True"} rewrites the

668 term @{text "g a \<in> range g"} to @{text "True"}, but will fail to

669 match @{text "g (h b) \<in> range (\<lambda>x. g (h x))"}. However, offending

670 subterms (in our case @{text "?f ?x"}, which is not a pattern) can

671 be replaced by adding new variables and conditions like this: @{text

672 "?y = ?f ?x \<Longrightarrow> ?y \<in> range ?f = True"} is acceptable as a conditional

673 rewrite rule of the second category since conditions can be

674 arbitrary terms.

676 \end{enumerate}

678 \item @{attribute split} declares case split rules.

680 \item @{attribute cong} declares congruence rules to the Simplifier

681 context.

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

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

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

687 example, some arguments can be simplified under additional

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

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

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

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

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

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

696 %FIXME

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

698 %see \secref{sec:simp-solver} below.

700 \medskip The following congruence rule for bounded quantifiers also

701 supplies contextual information --- about the bound variable:

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

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

705 \medskip This congruence rule for conditional expressions can

706 supply contextual information for simplifying the arms:

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

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

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

711 arguments. Here is an alternative congruence rule for conditional

712 expressions that conforms to non-strict functional evaluation:

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

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

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

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

719 \item @{command "print_simpset"} prints the collection of rules

720 declared to the Simplifier, which is also known as ``simpset''

721 internally.

723 For historical reasons, simpsets may occur independently from the

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

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

726 source language (as proof method \secref{sec:simp-meth} or rule

727 attribute \secref{sec:simp-meth}), its simpset is derived from the

728 current proof context, and carries a back-reference to that for

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

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

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

732 unexpected results.

734 \end{description}

736 The implicit simpset of the theory context is propagated

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

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

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

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

741 declare Simplifier rules to the target context, while plain

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

743 anything.

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

746 by explicitly adding or deleting theorems as simplification rules,

747 or installing other tools via simplification procedures

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

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

750 candidates for the implicit simpset, unless a special

751 non-normalizing behavior of certain operations is intended. More

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

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

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

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

756 designed simpset.

758 \begin{warn}

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

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

761 ancestors have deleted simplification rules because they are no

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

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

764 in the theory body.

765 \end{warn}

766 \<close>

769 subsection \<open>Ordered rewriting with permutative rules\<close>

771 text \<open>A rewrite rule is \emph{permutative} if the left-hand side and

772 right-hand side are the equal up to renaming of variables. The most

773 common permutative rule is commutativity: @{text "?x + ?y = ?y +

774 ?x"}. Other examples include @{text "(?x - ?y) - ?z = (?x - ?z) -

775 ?y"} in arithmetic and @{text "insert ?x (insert ?y ?A) = insert ?y

776 (insert ?x ?A)"} for sets. Such rules are common enough to merit

777 special attention.

779 Because ordinary rewriting loops given such rules, the Simplifier

780 employs a special strategy, called \emph{ordered rewriting}.

781 Permutative rules are detected and only applied if the rewriting

782 step decreases the redex wrt.\ a given term ordering. For example,

783 commutativity rewrites @{text "b + a"} to @{text "a + b"}, but then

784 stops, because the redex cannot be decreased further in the sense of

785 the term ordering.

787 The default is lexicographic ordering of term structure, but this

788 could be also changed locally for special applications via

789 @{index_ML Simplifier.set_termless} in Isabelle/ML.

791 \medskip Permutative rewrite rules are declared to the Simplifier

792 just like other rewrite rules. Their special status is recognized

793 automatically, and their application is guarded by the term ordering

794 accordingly.\<close>

797 subsubsection \<open>Rewriting with AC operators\<close>

799 text \<open>Ordered rewriting is particularly effective in the case of

800 associative-commutative operators. (Associativity by itself is not

801 permutative.) When dealing with an AC-operator @{text "f"}, keep

802 the following points in mind:

804 \begin{itemize}

806 \item The associative law must always be oriented from left to

807 right, namely @{text "f (f x y) z = f x (f y z)"}. The opposite

808 orientation, if used with commutativity, leads to looping in

809 conjunction with the standard term order.

811 \item To complete your set of rewrite rules, you must add not just

812 associativity (A) and commutativity (C) but also a derived rule

813 \emph{left-commutativity} (LC): @{text "f x (f y z) = f y (f x z)"}.

815 \end{itemize}

817 Ordered rewriting with the combination of A, C, and LC sorts a term

818 lexicographically --- the rewriting engine imitates bubble-sort.

819 \<close>

821 locale AC_example =

822 fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<bullet>" 60)

823 assumes assoc: "(x \<bullet> y) \<bullet> z = x \<bullet> (y \<bullet> z)"

824 assumes commute: "x \<bullet> y = y \<bullet> x"

825 begin

827 lemma left_commute: "x \<bullet> (y \<bullet> z) = y \<bullet> (x \<bullet> z)"

828 proof -

829 have "(x \<bullet> y) \<bullet> z = (y \<bullet> x) \<bullet> z" by (simp only: commute)

830 then show ?thesis by (simp only: assoc)

831 qed

833 lemmas AC_rules = assoc commute left_commute

835 text \<open>Thus the Simplifier is able to establish equalities with

836 arbitrary permutations of subterms, by normalizing to a common

837 standard form. For example:\<close>

839 lemma "(b \<bullet> c) \<bullet> a = xxx"

840 apply (simp only: AC_rules)

841 txt \<open>@{subgoals}\<close>

842 oops

844 lemma "(b \<bullet> c) \<bullet> a = a \<bullet> (b \<bullet> c)" by (simp only: AC_rules)

845 lemma "(b \<bullet> c) \<bullet> a = c \<bullet> (b \<bullet> a)" by (simp only: AC_rules)

846 lemma "(b \<bullet> c) \<bullet> a = (c \<bullet> b) \<bullet> a" by (simp only: AC_rules)

848 end

850 text \<open>Martin and Nipkow @{cite "martin-nipkow"} discuss the theory and

851 give many examples; other algebraic structures are amenable to

852 ordered rewriting, such as Boolean rings. The Boyer-Moore theorem

853 prover @{cite bm88book} also employs ordered rewriting.

854 \<close>

857 subsubsection \<open>Re-orienting equalities\<close>

859 text \<open>Another application of ordered rewriting uses the derived rule

860 @{thm [source] eq_commute}: @{thm [source = false] eq_commute} to

861 reverse equations.

863 This is occasionally useful to re-orient local assumptions according

864 to the term ordering, when other built-in mechanisms of

865 reorientation and mutual simplification fail to apply.\<close>

868 subsection \<open>Simplifier tracing and debugging \label{sec:simp-trace}\<close>

870 text \<open>

871 \begin{tabular}{rcll}

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

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

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

875 @{attribute_def simp_trace_new} & : & @{text attribute} \\

876 @{attribute_def simp_break} & : & @{text attribute} \\

877 \end{tabular}

878 \medskip

880 @{rail \<open>

881 @@{attribute simp_trace_new} ('interactive')? \<newline>

882 ('mode' '=' ('full' | 'normal'))? \<newline>

883 ('depth' '=' @{syntax nat})?

884 ;

886 @@{attribute simp_break} (@{syntax term}*)

887 \<close>}

889 These attributes and configurations options control various aspects of

890 Simplifier tracing and debugging.

892 \begin{description}

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

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

896 modifications of the simpset.

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

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

900 invocations (when solving conditions of rewrite rules).

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

903 information about internal operations. This includes any attempted

904 invocation of simplification procedures.

906 \item @{attribute simp_trace_new} controls Simplifier tracing within

907 Isabelle/PIDE applications, notably Isabelle/jEdit @{cite "isabelle-jedit"}.

908 This provides a hierarchical representation of the rewriting steps

909 performed by the Simplifier.

911 Users can configure the behaviour by specifying breakpoints, verbosity and

912 enabling or disabling the interactive mode. In normal verbosity (the

913 default), only rule applications matching a breakpoint will be shown to

914 the user. In full verbosity, all rule applications will be logged.

915 Interactive mode interrupts the normal flow of the Simplifier and defers

916 the decision how to continue to the user via some GUI dialog.

918 \item @{attribute simp_break} declares term or theorem breakpoints for

919 @{attribute simp_trace_new} as described above. Term breakpoints are

920 patterns which are checked for matches on the redex of a rule application.

921 Theorem breakpoints trigger when the corresponding theorem is applied in a

922 rewrite step. For example:

924 \end{description}

925 \<close>

927 declare conjI [simp_break]

928 declare [[simp_break "?x \<and> ?y"]]

931 subsection \<open>Simplification procedures \label{sec:simproc}\<close>

933 text \<open>Simplification procedures are ML functions that produce proven

934 rewrite rules on demand. They are associated with higher-order

935 patterns that approximate the left-hand sides of equations. The

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

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

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

939 may be specifically fashioned for particular situations, resulting

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

941 rules.

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

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

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

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

947 automatic preprocessing of object-level equivalences.

949 \begin{matharray}{rcl}

950 @{command_def "simproc_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

951 simproc & : & @{text attribute} \\

952 \end{matharray}

954 @{rail \<open>

955 @@{command simproc_setup} @{syntax name} '(' (@{syntax term} + '|') ')' '='

956 @{syntax text} \<newline> (@'identifier' (@{syntax nameref}+))?

957 ;

959 @@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+)

960 \<close>}

962 \begin{description}

964 \item @{command "simproc_setup"} defines a named simplification

965 procedure that is invoked by the Simplifier whenever any of the

966 given term patterns match the current redex. The implementation,

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

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

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

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

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

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

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

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

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

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

977 represent the logical content of the abstract theory of this

978 simproc.

980 Morphisms and identifiers are only relevant for simprocs that are

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

983 \item @{text "simproc add: name"} and @{text "simproc del: name"}

984 add or delete named simprocs to the current Simplifier context. The

985 default is to add a simproc. Note that @{command "simproc_setup"}

986 already adds the new simproc to the subsequent context.

988 \end{description}

989 \<close>

992 subsubsection \<open>Example\<close>

994 text \<open>The following simplification procedure for @{thm

995 [source=false, show_types] unit_eq} in HOL performs fine-grained

996 control over rule application, beyond higher-order pattern matching.

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

998 the Simplifier loop! Note that a version of this simplification

999 procedure is already active in Isabelle/HOL.\<close>

1001 simproc_setup unit ("x::unit") =

1002 \<open>fn _ => fn _ => fn ct =>

1003 if HOLogic.is_unit (Thm.term_of ct) then NONE

1004 else SOME (mk_meta_eq @{thm unit_eq})\<close>

1006 text \<open>Since the Simplifier applies simplification procedures

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

1008 reasonably fast.\<close>

1011 subsection \<open>Configurable Simplifier strategies \label{sec:simp-strategies}\<close>

1013 text \<open>The core term-rewriting engine of the Simplifier is normally

1014 used in combination with some add-on components that modify the

1015 strategy and allow to integrate other non-Simplifier proof tools.

1016 These may be reconfigured in ML as explained below. Even if the

1017 default strategies of object-logics like Isabelle/HOL are used

1018 unchanged, it helps to understand how the standard Simplifier

1019 strategies work.\<close>

1022 subsubsection \<open>The subgoaler\<close>

1024 text \<open>

1025 \begin{mldecls}

1026 @{index_ML Simplifier.set_subgoaler: "(Proof.context -> int -> tactic) ->

1027 Proof.context -> Proof.context"} \\

1028 @{index_ML Simplifier.prems_of: "Proof.context -> thm list"} \\

1029 \end{mldecls}

1031 The subgoaler is the tactic used to solve subgoals arising out of

1032 conditional rewrite rules or congruence rules. The default should

1033 be simplification itself. In rare situations, this strategy may

1034 need to be changed. For example, if the premise of a conditional

1035 rule is an instance of its conclusion, as in @{text "Suc ?m < ?n \<Longrightarrow>

1036 ?m < ?n"}, the default strategy could loop. % FIXME !??

1038 \begin{description}

1040 \item @{ML Simplifier.set_subgoaler}~@{text "tac ctxt"} sets the

1041 subgoaler of the context to @{text "tac"}. The tactic will

1042 be applied to the context of the running Simplifier instance.

1044 \item @{ML Simplifier.prems_of}~@{text "ctxt"} retrieves the current

1045 set of premises from the context. This may be non-empty only if

1046 the Simplifier has been told to utilize local assumptions in the

1047 first place (cf.\ the options in \secref{sec:simp-meth}).

1049 \end{description}

1051 As an example, consider the following alternative subgoaler:

1052 \<close>

1054 ML \<open>

1055 fun subgoaler_tac ctxt =

1056 assume_tac ctxt ORELSE'

1057 resolve_tac ctxt (Simplifier.prems_of ctxt) ORELSE'

1058 asm_simp_tac ctxt

1059 \<close>

1061 text \<open>This tactic first tries to solve the subgoal by assumption or

1062 by resolving with with one of the premises, calling simplification

1063 only if that fails.\<close>

1066 subsubsection \<open>The solver\<close>

1068 text \<open>

1069 \begin{mldecls}

1070 @{index_ML_type solver} \\

1071 @{index_ML Simplifier.mk_solver: "string ->

1072 (Proof.context -> int -> tactic) -> solver"} \\

1073 @{index_ML_op setSolver: "Proof.context * solver -> Proof.context"} \\

1074 @{index_ML_op addSolver: "Proof.context * solver -> Proof.context"} \\

1075 @{index_ML_op setSSolver: "Proof.context * solver -> Proof.context"} \\

1076 @{index_ML_op addSSolver: "Proof.context * solver -> Proof.context"} \\

1077 \end{mldecls}

1079 A solver is a tactic that attempts to solve a subgoal after

1080 simplification. Its core functionality is to prove trivial subgoals

1081 such as @{prop "True"} and @{text "t = t"}, but object-logics might

1082 be more ambitious. For example, Isabelle/HOL performs a restricted

1083 version of linear arithmetic here.

1085 Solvers are packaged up in abstract type @{ML_type solver}, with

1086 @{ML Simplifier.mk_solver} as the only operation to create a solver.

1088 \medskip Rewriting does not instantiate unknowns. For example,

1089 rewriting alone cannot prove @{text "a \<in> ?A"} since this requires

1090 instantiating @{text "?A"}. The solver, however, is an arbitrary

1091 tactic and may instantiate unknowns as it pleases. This is the only

1092 way the Simplifier can handle a conditional rewrite rule whose

1093 condition contains extra variables. When a simplification tactic is

1094 to be combined with other provers, especially with the Classical

1095 Reasoner, it is important whether it can be considered safe or not.

1096 For this reason a simpset contains two solvers: safe and unsafe.

1098 The standard simplification strategy solely uses the unsafe solver,

1099 which is appropriate in most cases. For special applications where

1100 the simplification process is not allowed to instantiate unknowns

1101 within the goal, simplification starts with the safe solver, but may

1102 still apply the ordinary unsafe one in nested simplifications for

1103 conditional rules or congruences. Note that in this way the overall

1104 tactic is not totally safe: it may instantiate unknowns that appear

1105 also in other subgoals.

1107 \begin{description}

1109 \item @{ML Simplifier.mk_solver}~@{text "name tac"} turns @{text

1110 "tac"} into a solver; the @{text "name"} is only attached as a

1111 comment and has no further significance.

1113 \item @{text "ctxt setSSolver solver"} installs @{text "solver"} as

1114 the safe solver of @{text "ctxt"}.

1116 \item @{text "ctxt addSSolver solver"} adds @{text "solver"} as an

1117 additional safe solver; it will be tried after the solvers which had

1118 already been present in @{text "ctxt"}.

1120 \item @{text "ctxt setSolver solver"} installs @{text "solver"} as the

1121 unsafe solver of @{text "ctxt"}.

1123 \item @{text "ctxt addSolver solver"} adds @{text "solver"} as an

1124 additional unsafe solver; it will be tried after the solvers which

1125 had already been present in @{text "ctxt"}.

1127 \end{description}

1129 \medskip The solver tactic is invoked with the context of the

1130 running Simplifier. Further operations

1131 may be used to retrieve relevant information, such as the list of

1132 local Simplifier premises via @{ML Simplifier.prems_of} --- this

1133 list may be non-empty only if the Simplifier runs in a mode that

1134 utilizes local assumptions (see also \secref{sec:simp-meth}). The

1135 solver is also presented the full goal including its assumptions in

1136 any case. Thus it can use these (e.g.\ by calling @{ML

1137 assume_tac}), even if the Simplifier proper happens to ignore local

1138 premises at the moment.

1140 \medskip As explained before, the subgoaler is also used to solve

1141 the premises of congruence rules. These are usually of the form

1142 @{text "s = ?x"}, where @{text "s"} needs to be simplified and

1143 @{text "?x"} needs to be instantiated with the result. Typically,

1144 the subgoaler will invoke the Simplifier at some point, which will

1145 eventually call the solver. For this reason, solver tactics must be

1146 prepared to solve goals of the form @{text "t = ?x"}, usually by

1147 reflexivity. In particular, reflexivity should be tried before any

1148 of the fancy automated proof tools.

1150 It may even happen that due to simplification the subgoal is no

1151 longer an equality. For example, @{text "False \<longleftrightarrow> ?Q"} could be

1152 rewritten to @{text "\<not> ?Q"}. To cover this case, the solver could

1153 try resolving with the theorem @{text "\<not> False"} of the

1154 object-logic.

1156 \medskip

1158 \begin{warn}

1159 If a premise of a congruence rule cannot be proved, then the

1160 congruence is ignored. This should only happen if the rule is

1161 \emph{conditional} --- that is, contains premises not of the form

1162 @{text "t = ?x"}. Otherwise it indicates that some congruence rule,

1163 or possibly the subgoaler or solver, is faulty.

1164 \end{warn}

1165 \<close>

1168 subsubsection \<open>The looper\<close>

1170 text \<open>

1171 \begin{mldecls}

1172 @{index_ML_op setloop: "Proof.context *

1173 (Proof.context -> int -> tactic) -> Proof.context"} \\

1174 @{index_ML_op addloop: "Proof.context *

1175 (string * (Proof.context -> int -> tactic))

1176 -> Proof.context"} \\

1177 @{index_ML_op delloop: "Proof.context * string -> Proof.context"} \\

1178 @{index_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\

1179 @{index_ML Splitter.del_split: "thm -> Proof.context -> Proof.context"} \\

1180 \end{mldecls}

1182 The looper is a list of tactics that are applied after

1183 simplification, in case the solver failed to solve the simplified

1184 goal. If the looper succeeds, the simplification process is started

1185 all over again. Each of the subgoals generated by the looper is

1186 attacked in turn, in reverse order.

1188 A typical looper is \emph{case splitting}: the expansion of a

1189 conditional. Another possibility is to apply an elimination rule on

1190 the assumptions. More adventurous loopers could start an induction.

1192 \begin{description}

1194 \item @{text "ctxt setloop tac"} installs @{text "tac"} as the only

1195 looper tactic of @{text "ctxt"}.

1197 \item @{text "ctxt addloop (name, tac)"} adds @{text "tac"} as an

1198 additional looper tactic with name @{text "name"}, which is

1199 significant for managing the collection of loopers. The tactic will

1200 be tried after the looper tactics that had already been present in

1201 @{text "ctxt"}.

1203 \item @{text "ctxt delloop name"} deletes the looper tactic that was

1204 associated with @{text "name"} from @{text "ctxt"}.

1206 \item @{ML Splitter.add_split}~@{text "thm ctxt"} adds split tactics

1207 for @{text "thm"} as additional looper tactics of @{text "ctxt"}.

1209 \item @{ML Splitter.del_split}~@{text "thm ctxt"} deletes the split

1210 tactic corresponding to @{text thm} from the looper tactics of

1211 @{text "ctxt"}.

1213 \end{description}

1215 The splitter replaces applications of a given function; the

1216 right-hand side of the replacement can be anything. For example,

1217 here is a splitting rule for conditional expressions:

1219 @{text [display] "?P (if ?Q ?x ?y) \<longleftrightarrow> (?Q \<longrightarrow> ?P ?x) \<and> (\<not> ?Q \<longrightarrow> ?P ?y)"}

1221 Another example is the elimination operator for Cartesian products

1222 (which happens to be called @{text split} in Isabelle/HOL:

1224 @{text [display] "?P (split ?f ?p) \<longleftrightarrow> (\<forall>a b. ?p = (a, b) \<longrightarrow> ?P (f a b))"}

1226 For technical reasons, there is a distinction between case splitting

1227 in the conclusion and in the premises of a subgoal. The former is

1228 done by @{ML Splitter.split_tac} with rules like @{thm [source]

1229 split_if} or @{thm [source] option.split}, which do not split the

1230 subgoal, while the latter is done by @{ML Splitter.split_asm_tac}

1231 with rules like @{thm [source] split_if_asm} or @{thm [source]

1232 option.split_asm}, which split the subgoal. The function @{ML

1233 Splitter.add_split} automatically takes care of which tactic to

1234 call, analyzing the form of the rules given as argument; it is the

1235 same operation behind @{text "split"} attribute or method modifier

1236 syntax in the Isar source language.

1238 Case splits should be allowed only when necessary; they are

1239 expensive and hard to control. Case-splitting on if-expressions in

1240 the conclusion is usually beneficial, so it is enabled by default in

1241 Isabelle/HOL and Isabelle/FOL/ZF.

1243 \begin{warn}

1244 With @{ML Splitter.split_asm_tac} as looper component, the

1245 Simplifier may split subgoals! This might cause unexpected problems

1246 in tactic expressions that silently assume 0 or 1 subgoals after

1247 simplification.

1248 \end{warn}

1249 \<close>

1252 subsection \<open>Forward simplification \label{sec:simp-forward}\<close>

1254 text \<open>

1255 \begin{matharray}{rcl}

1256 @{attribute_def simplified} & : & @{text attribute} \\

1257 \end{matharray}

1259 @{rail \<open>

1260 @@{attribute simplified} opt? @{syntax thmrefs}?

1261 ;

1263 opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'

1264 \<close>}

1266 \begin{description}

1268 \item @{attribute simplified}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} causes a theorem to

1269 be simplified, either by exactly the specified rules @{text "a\<^sub>1, \<dots>,

1270 a\<^sub>n"}, or the implicit Simplifier context if no arguments are given.

1271 The result is fully simplified by default, including assumptions and

1272 conclusion; the options @{text no_asm} etc.\ tune the Simplifier in

1273 the same way as the for the @{text simp} method.

1275 Note that forward simplification restricts the Simplifier to its

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

1277 (\secref{sec:simp-strategies}) are \emph{not} involved here. The

1278 @{attribute simplified} attribute should be only rarely required

1279 under normal circumstances.

1281 \end{description}

1282 \<close>

1285 section \<open>The Classical Reasoner \label{sec:classical}\<close>

1287 subsection \<open>Basic concepts\<close>

1289 text \<open>Although Isabelle is generic, many users will be working in

1290 some extension of classical first-order logic. Isabelle/ZF is built

1291 upon theory FOL, while Isabelle/HOL conceptually contains

1292 first-order logic as a fragment. Theorem-proving in predicate logic

1293 is undecidable, but many automated strategies have been developed to

1294 assist in this task.

1296 Isabelle's classical reasoner is a generic package that accepts

1297 certain information about a logic and delivers a suite of automatic

1298 proof tools, based on rules that are classified and declared in the

1299 context. These proof procedures are slow and simplistic compared

1300 with high-end automated theorem provers, but they can save

1301 considerable time and effort in practice. They can prove theorems

1302 such as Pelletier's @{cite pelletier86} problems 40 and 41 in a few

1303 milliseconds (including full proof reconstruction):\<close>

1305 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)"

1306 by blast

1308 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)"

1309 by blast

1311 text \<open>The proof tools are generic. They are not restricted to

1312 first-order logic, and have been heavily used in the development of

1313 the Isabelle/HOL library and applications. The tactics can be

1314 traced, and their components can be called directly; in this manner,

1315 any proof can be viewed interactively.\<close>

1318 subsubsection \<open>The sequent calculus\<close>

1320 text \<open>Isabelle supports natural deduction, which is easy to use for

1321 interactive proof. But natural deduction does not easily lend

1322 itself to automation, and has a bias towards intuitionism. For

1323 certain proofs in classical logic, it can not be called natural.

1324 The \emph{sequent calculus}, a generalization of natural deduction,

1325 is easier to automate.

1327 A \textbf{sequent} has the form @{text "\<Gamma> \<turnstile> \<Delta>"}, where @{text "\<Gamma>"}

1328 and @{text "\<Delta>"} are sets of formulae.\footnote{For first-order

1329 logic, sequents can equivalently be made from lists or multisets of

1330 formulae.} The sequent @{text "P\<^sub>1, \<dots>, P\<^sub>m \<turnstile> Q\<^sub>1, \<dots>, Q\<^sub>n"} is

1331 \textbf{valid} if @{text "P\<^sub>1 \<and> \<dots> \<and> P\<^sub>m"} implies @{text "Q\<^sub>1 \<or> \<dots> \<or>

1332 Q\<^sub>n"}. Thus @{text "P\<^sub>1, \<dots>, P\<^sub>m"} represent assumptions, each of which

1333 is true, while @{text "Q\<^sub>1, \<dots>, Q\<^sub>n"} represent alternative goals. A

1334 sequent is \textbf{basic} if its left and right sides have a common

1335 formula, as in @{text "P, Q \<turnstile> Q, R"}; basic sequents are trivially

1336 valid.

1338 Sequent rules are classified as \textbf{right} or \textbf{left},

1339 indicating which side of the @{text "\<turnstile>"} symbol they operate on.

1340 Rules that operate on the right side are analogous to natural

1341 deduction's introduction rules, and left rules are analogous to

1342 elimination rules. The sequent calculus analogue of @{text "(\<longrightarrow>I)"}

1343 is the rule

1344 \[

1345 \infer[@{text "(\<longrightarrow>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, P \<longrightarrow> Q"}}{@{text "P, \<Gamma> \<turnstile> \<Delta>, Q"}}

1346 \]

1347 Applying the rule backwards, this breaks down some implication on

1348 the right side of a sequent; @{text "\<Gamma>"} and @{text "\<Delta>"} stand for

1349 the sets of formulae that are unaffected by the inference. The

1350 analogue of the pair @{text "(\<or>I1)"} and @{text "(\<or>I2)"} is the

1351 single rule

1352 \[

1353 \infer[@{text "(\<or>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, P \<or> Q"}}{@{text "\<Gamma> \<turnstile> \<Delta>, P, Q"}}

1354 \]

1355 This breaks down some disjunction on the right side, replacing it by

1356 both disjuncts. Thus, the sequent calculus is a kind of

1357 multiple-conclusion logic.

1359 To illustrate the use of multiple formulae on the right, let us

1360 prove the classical theorem @{text "(P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"}. Working

1361 backwards, we reduce this formula to a basic sequent:

1362 \[

1363 \infer[@{text "(\<or>R)"}]{@{text "\<turnstile> (P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"}}

1364 {\infer[@{text "(\<longrightarrow>R)"}]{@{text "\<turnstile> (P \<longrightarrow> Q), (Q \<longrightarrow> P)"}}

1365 {\infer[@{text "(\<longrightarrow>R)"}]{@{text "P \<turnstile> Q, (Q \<longrightarrow> P)"}}

1366 {@{text "P, Q \<turnstile> Q, P"}}}}

1367 \]

1369 This example is typical of the sequent calculus: start with the

1370 desired theorem and apply rules backwards in a fairly arbitrary

1371 manner. This yields a surprisingly effective proof procedure.

1372 Quantifiers add only few complications, since Isabelle handles

1373 parameters and schematic variables. See @{cite \<open>Chapter 10\<close>

1374 "paulson-ml2"} for further discussion.\<close>

1377 subsubsection \<open>Simulating sequents by natural deduction\<close>

1379 text \<open>Isabelle can represent sequents directly, as in the

1380 object-logic LK. But natural deduction is easier to work with, and

1381 most object-logics employ it. Fortunately, we can simulate the

1382 sequent @{text "P\<^sub>1, \<dots>, P\<^sub>m \<turnstile> Q\<^sub>1, \<dots>, Q\<^sub>n"} by the Isabelle formula

1383 @{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

1384 the assumptions and the choice of @{text "Q\<^sub>1"} are arbitrary.

1385 Elim-resolution plays a key role in simulating sequent proofs.

1387 We can easily handle reasoning on the left. Elim-resolution with

1388 the rules @{text "(\<or>E)"}, @{text "(\<bottom>E)"} and @{text "(\<exists>E)"} achieves

1389 a similar effect as the corresponding sequent rules. For the other

1390 connectives, we use sequent-style elimination rules instead of

1391 destruction rules such as @{text "(\<and>E1, 2)"} and @{text "(\<forall>E)"}.

1392 But note that the rule @{text "(\<not>L)"} has no effect under our

1393 representation of sequents!

1394 \[

1395 \infer[@{text "(\<not>L)"}]{@{text "\<not> P, \<Gamma> \<turnstile> \<Delta>"}}{@{text "\<Gamma> \<turnstile> \<Delta>, P"}}

1396 \]

1398 What about reasoning on the right? Introduction rules can only

1399 affect the formula in the conclusion, namely @{text "Q\<^sub>1"}. The

1400 other right-side formulae are represented as negated assumptions,

1401 @{text "\<not> Q\<^sub>2, \<dots>, \<not> Q\<^sub>n"}. In order to operate on one of these, it

1402 must first be exchanged with @{text "Q\<^sub>1"}. Elim-resolution with the

1403 @{text swap} rule has this effect: @{text "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"}

1405 To ensure that swaps occur only when necessary, each introduction

1406 rule is converted into a swapped form: it is resolved with the

1407 second premise of @{text "(swap)"}. The swapped form of @{text

1408 "(\<and>I)"}, which might be called @{text "(\<not>\<and>E)"}, is

1409 @{text [display] "\<not> (P \<and> Q) \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (\<not> R \<Longrightarrow> Q) \<Longrightarrow> R"}

1411 Similarly, the swapped form of @{text "(\<longrightarrow>I)"} is

1412 @{text [display] "\<not> (P \<longrightarrow> Q) \<Longrightarrow> (\<not> R \<Longrightarrow> P \<Longrightarrow> Q) \<Longrightarrow> R"}

1414 Swapped introduction rules are applied using elim-resolution, which

1415 deletes the negated formula. Our representation of sequents also

1416 requires the use of ordinary introduction rules. If we had no

1417 regard for readability of intermediate goal states, we could treat

1418 the right side more uniformly by representing sequents as @{text

1419 [display] "P\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> P\<^sub>m \<Longrightarrow> \<not> Q\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> \<not> Q\<^sub>n \<Longrightarrow> \<bottom>"}

1420 \<close>

1423 subsubsection \<open>Extra rules for the sequent calculus\<close>

1425 text \<open>As mentioned, destruction rules such as @{text "(\<and>E1, 2)"} and

1426 @{text "(\<forall>E)"} must be replaced by sequent-style elimination rules.

1427 In addition, we need rules to embody the classical equivalence

1428 between @{text "P \<longrightarrow> Q"} and @{text "\<not> P \<or> Q"}. The introduction

1429 rules @{text "(\<or>I1, 2)"} are replaced by a rule that simulates

1430 @{text "(\<or>R)"}: @{text [display] "(\<not> Q \<Longrightarrow> P) \<Longrightarrow> P \<or> Q"}

1432 The destruction rule @{text "(\<longrightarrow>E)"} is replaced by @{text [display]

1433 "(P \<longrightarrow> Q) \<Longrightarrow> (\<not> P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"}

1435 Quantifier replication also requires special rules. In classical

1436 logic, @{text "\<exists>x. P x"} is equivalent to @{text "\<not> (\<forall>x. \<not> P x)"};

1437 the rules @{text "(\<exists>R)"} and @{text "(\<forall>L)"} are dual:

1438 \[

1439 \infer[@{text "(\<exists>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, \<exists>x. P x"}}{@{text "\<Gamma> \<turnstile> \<Delta>, \<exists>x. P x, P t"}}

1440 \qquad

1441 \infer[@{text "(\<forall>L)"}]{@{text "\<forall>x. P x, \<Gamma> \<turnstile> \<Delta>"}}{@{text "P t, \<forall>x. P x, \<Gamma> \<turnstile> \<Delta>"}}

1442 \]

1443 Thus both kinds of quantifier may be replicated. Theorems requiring

1444 multiple uses of a universal formula are easy to invent; consider

1445 @{text [display] "(\<forall>x. P x \<longrightarrow> P (f x)) \<and> P a \<longrightarrow> P (f\<^sup>n a)"} for any

1446 @{text "n > 1"}. Natural examples of the multiple use of an

1447 existential formula are rare; a standard one is @{text "\<exists>x. \<forall>y. P x

1448 \<longrightarrow> P y"}.

1450 Forgoing quantifier replication loses completeness, but gains

1451 decidability, since the search space becomes finite. Many useful

1452 theorems can be proved without replication, and the search generally

1453 delivers its verdict in a reasonable time. To adopt this approach,

1454 represent the sequent rules @{text "(\<exists>R)"}, @{text "(\<exists>L)"} and

1455 @{text "(\<forall>R)"} by @{text "(\<exists>I)"}, @{text "(\<exists>E)"} and @{text "(\<forall>I)"},

1456 respectively, and put @{text "(\<forall>E)"} into elimination form: @{text

1457 [display] "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q"}

1459 Elim-resolution with this rule will delete the universal formula

1460 after a single use. To replicate universal quantifiers, replace the

1461 rule by @{text [display] "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q) \<Longrightarrow> Q"}

1463 To replicate existential quantifiers, replace @{text "(\<exists>I)"} by

1464 @{text [display] "(\<not> (\<exists>x. P x) \<Longrightarrow> P t) \<Longrightarrow> \<exists>x. P x"}

1466 All introduction rules mentioned above are also useful in swapped

1467 form.

1469 Replication makes the search space infinite; we must apply the rules

1470 with care. The classical reasoner distinguishes between safe and

1471 unsafe rules, applying the latter only when there is no alternative.

1472 Depth-first search may well go down a blind alley; best-first search

1473 is better behaved in an infinite search space. However, quantifier

1474 replication is too expensive to prove any but the simplest theorems.

1475 \<close>

1478 subsection \<open>Rule declarations\<close>

1480 text \<open>The proof tools of the Classical Reasoner depend on

1481 collections of rules declared in the context, which are classified

1482 as introduction, elimination or destruction and as \emph{safe} or

1483 \emph{unsafe}. In general, safe rules can be attempted blindly,

1484 while unsafe rules must be used with care. A safe rule must never

1485 reduce a provable goal to an unprovable set of subgoals.

1487 The rule @{text "P \<Longrightarrow> P \<or> Q"} is unsafe because it reduces @{text "P

1488 \<or> Q"} to @{text "P"}, which might turn out as premature choice of an

1489 unprovable subgoal. Any rule is unsafe whose premises contain new

1490 unknowns. The elimination rule @{text "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q"} is

1491 unsafe, since it is applied via elim-resolution, which discards the

1492 assumption @{text "\<forall>x. P x"} and replaces it by the weaker

1493 assumption @{text "P t"}. The rule @{text "P t \<Longrightarrow> \<exists>x. P x"} is

1494 unsafe for similar reasons. The quantifier duplication rule @{text

1495 "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q) \<Longrightarrow> Q"} is unsafe in a different sense:

1496 since it keeps the assumption @{text "\<forall>x. P x"}, it is prone to

1497 looping. In classical first-order logic, all rules are safe except

1498 those mentioned above.

1500 The safe~/ unsafe distinction is vague, and may be regarded merely

1501 as a way of giving some rules priority over others. One could argue

1502 that @{text "(\<or>E)"} is unsafe, because repeated application of it

1503 could generate exponentially many subgoals. Induction rules are

1504 unsafe because inductive proofs are difficult to set up

1505 automatically. Any inference is unsafe that instantiates an unknown

1506 in the proof state --- thus matching must be used, rather than

1507 unification. Even proof by assumption is unsafe if it instantiates

1508 unknowns shared with other subgoals.

1510 \begin{matharray}{rcl}

1511 @{command_def "print_claset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

1512 @{attribute_def intro} & : & @{text attribute} \\

1513 @{attribute_def elim} & : & @{text attribute} \\

1514 @{attribute_def dest} & : & @{text attribute} \\

1515 @{attribute_def rule} & : & @{text attribute} \\

1516 @{attribute_def iff} & : & @{text attribute} \\

1517 @{attribute_def swapped} & : & @{text attribute} \\

1518 \end{matharray}

1520 @{rail \<open>

1521 (@@{attribute intro} | @@{attribute elim} | @@{attribute dest}) ('!' | () | '?') @{syntax nat}?

1522 ;

1523 @@{attribute rule} 'del'

1524 ;

1525 @@{attribute iff} (((() | 'add') '?'?) | 'del')

1526 \<close>}

1528 \begin{description}

1530 \item @{command "print_claset"} prints the collection of rules

1531 declared to the Classical Reasoner, i.e.\ the @{ML_type claset}

1532 within the context.

1534 \item @{attribute intro}, @{attribute elim}, and @{attribute dest}

1535 declare introduction, elimination, and destruction rules,

1536 respectively. By default, rules are considered as \emph{unsafe}

1537 (i.e.\ not applied blindly without backtracking), while ``@{text

1538 "!"}'' classifies as \emph{safe}. Rule declarations marked by

1539 ``@{text "?"}'' coincide with those of Isabelle/Pure, cf.\

1540 \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps

1541 of the @{method rule} method). The optional natural number

1542 specifies an explicit weight argument, which is ignored by the

1543 automated reasoning tools, but determines the search order of single

1544 rule steps.

1546 Introduction rules are those that can be applied using ordinary

1547 resolution. Their swapped forms are generated internally, which

1548 will be applied using elim-resolution. Elimination rules are

1549 applied using elim-resolution. Rules are sorted by the number of

1550 new subgoals they will yield; rules that generate the fewest

1551 subgoals will be tried first. Otherwise, later declarations take

1552 precedence over earlier ones.

1554 Rules already present in the context with the same classification

1555 are ignored. A warning is printed if the rule has already been

1556 added with some other classification, but the rule is added anyway

1557 as requested.

1559 \item @{attribute rule}~@{text del} deletes all occurrences of a

1560 rule from the classical context, regardless of its classification as

1561 introduction~/ elimination~/ destruction and safe~/ unsafe.

1563 \item @{attribute iff} declares logical equivalences to the

1564 Simplifier and the Classical reasoner at the same time.

1565 Non-conditional rules result in a safe introduction and elimination

1566 pair; conditional ones are considered unsafe. Rules with negative

1567 conclusion are automatically inverted (using @{text "\<not>"}-elimination

1568 internally).

1570 The ``@{text "?"}'' version of @{attribute iff} declares rules to

1571 the Isabelle/Pure context only, and omits the Simplifier

1572 declaration.

1574 \item @{attribute swapped} turns an introduction rule into an

1575 elimination, by resolving with the classical swap principle @{text

1576 "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"} in the second position. This is mainly for

1577 illustrative purposes: the Classical Reasoner already swaps rules

1578 internally as explained above.

1580 \end{description}

1581 \<close>

1584 subsection \<open>Structured methods\<close>

1586 text \<open>

1587 \begin{matharray}{rcl}

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

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

1590 \end{matharray}

1592 @{rail \<open>

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

1594 \<close>}

1596 \begin{description}

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

1599 refinement over the Pure one (see \secref{sec:pure-meth-att}). Both

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

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

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

1604 classical rules (even if these would qualify as intuitionistic

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

1606 Isabelle/Pure (\secref{sec:pure-meth-att}).

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

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

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

1611 order.

1613 \end{description}

1614 \<close>

1617 subsection \<open>Fully automated methods\<close>

1619 text \<open>

1620 \begin{matharray}{rcl}

1621 @{method_def blast} & : & @{text method} \\

1622 @{method_def auto} & : & @{text method} \\

1623 @{method_def force} & : & @{text method} \\

1624 @{method_def fast} & : & @{text method} \\

1625 @{method_def slow} & : & @{text method} \\

1626 @{method_def best} & : & @{text method} \\

1627 @{method_def fastforce} & : & @{text method} \\

1628 @{method_def slowsimp} & : & @{text method} \\

1629 @{method_def bestsimp} & : & @{text method} \\

1630 @{method_def deepen} & : & @{text method} \\

1631 \end{matharray}

1633 @{rail \<open>

1634 @@{method blast} @{syntax nat}? (@{syntax clamod} * )

1635 ;

1636 @@{method auto} (@{syntax nat} @{syntax nat})? (@{syntax clasimpmod} * )

1637 ;

1638 @@{method force} (@{syntax clasimpmod} * )

1639 ;

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

1641 ;

1642 (@@{method fastforce} | @@{method slowsimp} | @@{method bestsimp})

1643 (@{syntax clasimpmod} * )

1644 ;

1645 @@{method deepen} (@{syntax nat} ?) (@{syntax clamod} * )

1646 ;

1647 @{syntax_def clamod}:

1648 (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thmrefs}

1649 ;

1650 @{syntax_def clasimpmod}: ('simp' (() | 'add' | 'del' | 'only') |

1651 ('cong' | 'split') (() | 'add' | 'del') |

1652 'iff' (((() | 'add') '?'?) | 'del') |

1653 (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thmrefs}

1654 \<close>}

1656 \begin{description}

1658 \item @{method blast} is a separate classical tableau prover that

1659 uses the same classical rule declarations as explained before.

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

1662 A successful proof is then reconstructed using regular Isabelle

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

1664 reasoning tools, but has major limitations too.

1666 \begin{itemize}

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

1669 integration with the Simplifier of @{method fastforce}.

1671 \item It does not perform higher-order unification, as needed by the

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

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

1674 range_eqI}.

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

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

1678 higher-order unification.) If other function variables are present

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

1680 argument not a bound variable}.

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

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

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

1686 \end{itemize}

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

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

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

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

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

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

1694 proof method instead.

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

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

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

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

1700 ones may take a long time.

1702 The optional depth arguments in @{text "(auto m n)"} refer to its

1703 builtin classical reasoning procedures: @{text m} (default 4) is for

1704 @{method blast}, which is tried first, and @{text n} (default 2) is

1705 for a slower but more general alternative that also takes wrappers

1706 into account.

1708 \item @{method force} is intended to prove the first subgoal

1709 completely, using many fancy proof tools and performing a rather

1710 exhaustive search. As a result, proof attempts may take rather long

1711 or diverge easily.

1713 \item @{method fast}, @{method best}, @{method slow} attempt to

1714 prove the first subgoal using sequent-style reasoning as explained

1715 before. Unlike @{method blast}, they construct proofs directly in

1716 Isabelle.

1718 There is a difference in search strategy and back-tracking: @{method

1719 fast} uses depth-first search and @{method best} uses best-first

1720 search (guided by a heuristic function: normally the total size of

1721 the proof state).

1723 Method @{method slow} is like @{method fast}, but conducts a broader

1724 search: it may, when backtracking from a failed proof attempt, undo

1725 even the step of proving a subgoal by assumption.

1727 \item @{method fastforce}, @{method slowsimp}, @{method bestsimp}

1728 are like @{method fast}, @{method slow}, @{method best},

1729 respectively, but use the Simplifier as additional wrapper. The name

1730 @{method fastforce}, reflects the behaviour of this popular method

1731 better without requiring an understanding of its implementation.

1733 \item @{method deepen} works by exhaustive search up to a certain

1734 depth. The start depth is 4 (unless specified explicitly), and the

1735 depth is increased iteratively up to 10. Unsafe rules are modified

1736 to preserve the formula they act on, so that it be used repeatedly.

1737 This method can prove more goals than @{method fast}, but is much

1738 slower, for example if the assumptions have many universal

1739 quantifiers.

1741 \end{description}

1743 Any of the above methods support additional modifiers of the context

1744 of classical (and simplifier) rules, but the ones related to the

1745 Simplifier are explicitly prefixed by @{text simp} here. The

1746 semantics of these ad-hoc rule declarations is analogous to the

1747 attributes given before. Facts provided by forward chaining are

1748 inserted into the goal before commencing proof search.

1749 \<close>

1752 subsection \<open>Partially automated methods\<close>

1754 text \<open>These proof methods may help in situations when the

1755 fully-automated tools fail. The result is a simpler subgoal that

1756 can be tackled by other means, such as by manual instantiation of

1757 quantifiers.

1759 \begin{matharray}{rcl}

1760 @{method_def safe} & : & @{text method} \\

1761 @{method_def clarify} & : & @{text method} \\

1762 @{method_def clarsimp} & : & @{text method} \\

1763 \end{matharray}

1765 @{rail \<open>

1766 (@@{method safe} | @@{method clarify}) (@{syntax clamod} * )

1767 ;

1768 @@{method clarsimp} (@{syntax clasimpmod} * )

1769 \<close>}

1771 \begin{description}

1773 \item @{method safe} repeatedly performs safe steps on all subgoals.

1774 It is deterministic, with at most one outcome.

1776 \item @{method clarify} performs a series of safe steps without

1777 splitting subgoals; see also @{method clarify_step}.

1779 \item @{method clarsimp} acts like @{method clarify}, but also does

1780 simplification. Note that if the Simplifier context includes a

1781 splitter for the premises, the subgoal may still be split.

1783 \end{description}

1784 \<close>

1787 subsection \<open>Single-step tactics\<close>

1789 text \<open>

1790 \begin{matharray}{rcl}

1791 @{method_def safe_step} & : & @{text method} \\

1792 @{method_def inst_step} & : & @{text method} \\

1793 @{method_def step} & : & @{text method} \\

1794 @{method_def slow_step} & : & @{text method} \\

1795 @{method_def clarify_step} & : & @{text method} \\

1796 \end{matharray}

1798 These are the primitive tactics behind the automated proof methods

1799 of the Classical Reasoner. By calling them yourself, you can

1800 execute these procedures one step at a time.

1802 \begin{description}

1804 \item @{method safe_step} performs a safe step on the first subgoal.

1805 The safe wrapper tacticals are applied to a tactic that may include

1806 proof by assumption or Modus Ponens (taking care not to instantiate

1807 unknowns), or substitution.

1809 \item @{method inst_step} is like @{method safe_step}, but allows

1810 unknowns to be instantiated.

1812 \item @{method step} is the basic step of the proof procedure, it

1813 operates on the first subgoal. The unsafe wrapper tacticals are

1814 applied to a tactic that tries @{method safe}, @{method inst_step},

1815 or applies an unsafe rule from the context.

1817 \item @{method slow_step} resembles @{method step}, but allows

1818 backtracking between using safe rules with instantiation (@{method

1819 inst_step}) and using unsafe rules. The resulting search space is

1820 larger.

1822 \item @{method clarify_step} performs a safe step on the first

1823 subgoal; no splitting step is applied. For example, the subgoal

1824 @{text "A \<and> B"} is left as a conjunction. Proof by assumption,

1825 Modus Ponens, etc., may be performed provided they do not

1826 instantiate unknowns. Assumptions of the form @{text "x = t"} may

1827 be eliminated. The safe wrapper tactical is applied.

1829 \end{description}

1830 \<close>

1833 subsection \<open>Modifying the search step\<close>

1835 text \<open>

1836 \begin{mldecls}

1837 @{index_ML_type wrapper: "(int -> tactic) -> (int -> tactic)"} \\[0.5ex]

1838 @{index_ML_op addSWrapper: "Proof.context *

1839 (string * (Proof.context -> wrapper)) -> Proof.context"} \\

1840 @{index_ML_op addSbefore: "Proof.context *

1841 (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\

1842 @{index_ML_op addSafter: "Proof.context *

1843 (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\

1844 @{index_ML_op delSWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]

1845 @{index_ML_op addWrapper: "Proof.context *

1846 (string * (Proof.context -> wrapper)) -> Proof.context"} \\

1847 @{index_ML_op addbefore: "Proof.context *

1848 (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\

1849 @{index_ML_op addafter: "Proof.context *

1850 (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\

1851 @{index_ML_op delWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]

1852 @{index_ML addSss: "Proof.context -> Proof.context"} \\

1853 @{index_ML addss: "Proof.context -> Proof.context"} \\

1854 \end{mldecls}

1856 The proof strategy of the Classical Reasoner is simple. Perform as

1857 many safe inferences as possible; or else, apply certain safe rules,

1858 allowing instantiation of unknowns; or else, apply an unsafe rule.

1859 The tactics also eliminate assumptions of the form @{text "x = t"}

1860 by substitution if they have been set up to do so. They may perform

1861 a form of Modus Ponens: if there are assumptions @{text "P \<longrightarrow> Q"} and

1862 @{text "P"}, then replace @{text "P \<longrightarrow> Q"} by @{text "Q"}.

1864 The classical reasoning tools --- except @{method blast} --- allow

1865 to modify this basic proof strategy by applying two lists of

1866 arbitrary \emph{wrapper tacticals} to it. The first wrapper list,

1867 which is considered to contain safe wrappers only, affects @{method

1868 safe_step} and all the tactics that call it. The second one, which

1869 may contain unsafe wrappers, affects the unsafe parts of @{method

1870 step}, @{method slow_step}, and the tactics that call them. A

1871 wrapper transforms each step of the search, for example by

1872 attempting other tactics before or after the original step tactic.

1873 All members of a wrapper list are applied in turn to the respective

1874 step tactic.

1876 Initially the two wrapper lists are empty, which means no

1877 modification of the step tactics. Safe and unsafe wrappers are added

1878 to a claset with the functions given below, supplying them with

1879 wrapper names. These names may be used to selectively delete

1880 wrappers.

1882 \begin{description}

1884 \item @{text "ctxt addSWrapper (name, wrapper)"} adds a new wrapper,

1885 which should yield a safe tactic, to modify the existing safe step

1886 tactic.

1888 \item @{text "ctxt addSbefore (name, tac)"} adds the given tactic as a

1889 safe wrapper, such that it is tried \emph{before} each safe step of

1890 the search.

1892 \item @{text "ctxt addSafter (name, tac)"} adds the given tactic as a

1893 safe wrapper, such that it is tried when a safe step of the search

1894 would fail.

1896 \item @{text "ctxt delSWrapper name"} deletes the safe wrapper with

1897 the given name.

1899 \item @{text "ctxt addWrapper (name, wrapper)"} adds a new wrapper to

1900 modify the existing (unsafe) step tactic.

1902 \item @{text "ctxt addbefore (name, tac)"} adds the given tactic as an

1903 unsafe wrapper, such that it its result is concatenated

1904 \emph{before} the result of each unsafe step.

1906 \item @{text "ctxt addafter (name, tac)"} adds the given tactic as an

1907 unsafe wrapper, such that it its result is concatenated \emph{after}

1908 the result of each unsafe step.

1910 \item @{text "ctxt delWrapper name"} deletes the unsafe wrapper with

1911 the given name.

1913 \item @{text "addSss"} adds the simpset of the context to its

1914 classical set. The assumptions and goal will be simplified, in a

1915 rather safe way, after each safe step of the search.

1917 \item @{text "addss"} adds the simpset of the context to its

1918 classical set. The assumptions and goal will be simplified, before

1919 the each unsafe step of the search.

1921 \end{description}

1922 \<close>

1925 section \<open>Object-logic setup \label{sec:object-logic}\<close>

1927 text \<open>

1928 \begin{matharray}{rcl}

1929 @{command_def "judgment"} & : & @{text "theory \<rightarrow> theory"} \\

1930 @{method_def atomize} & : & @{text method} \\

1931 @{attribute_def atomize} & : & @{text attribute} \\

1932 @{attribute_def rule_format} & : & @{text attribute} \\

1933 @{attribute_def rulify} & : & @{text attribute} \\

1934 \end{matharray}

1936 The very starting point for any Isabelle object-logic is a ``truth

1937 judgment'' that links object-level statements to the meta-logic

1938 (with its minimal language of @{text prop} that covers universal

1939 quantification @{text "\<And>"} and implication @{text "\<Longrightarrow>"}).

1941 Common object-logics are sufficiently expressive to internalize rule

1942 statements over @{text "\<And>"} and @{text "\<Longrightarrow>"} within their own

1943 language. This is useful in certain situations where a rule needs

1944 to be viewed as an atomic statement from the meta-level perspective,

1945 e.g.\ @{text "\<And>x. x \<in> A \<Longrightarrow> P x"} versus @{text "\<forall>x \<in> A. P x"}.

1947 From the following language elements, only the @{method atomize}

1948 method and @{attribute rule_format} attribute are occasionally

1949 required by end-users, the rest is for those who need to setup their

1950 own object-logic. In the latter case existing formulations of

1951 Isabelle/FOL or Isabelle/HOL may be taken as realistic examples.

1953 Generic tools may refer to the information provided by object-logic

1954 declarations internally.

1956 @{rail \<open>

1957 @@{command judgment} @{syntax name} '::' @{syntax type} @{syntax mixfix}?

1958 ;

1959 @@{attribute atomize} ('(' 'full' ')')?

1960 ;

1961 @@{attribute rule_format} ('(' 'noasm' ')')?

1962 \<close>}

1964 \begin{description}

1966 \item @{command "judgment"}~@{text "c :: \<sigma> (mx)"} declares constant

1967 @{text c} as the truth judgment of the current object-logic. Its

1968 type @{text \<sigma>} should specify a coercion of the category of

1969 object-level propositions to @{text prop} of the Pure meta-logic;

1970 the mixfix annotation @{text "(mx)"} would typically just link the

1971 object language (internally of syntactic category @{text logic})

1972 with that of @{text prop}. Only one @{command "judgment"}

1973 declaration may be given in any theory development.

1975 \item @{method atomize} (as a method) rewrites any non-atomic

1976 premises of a sub-goal, using the meta-level equations declared via

1977 @{attribute atomize} (as an attribute) beforehand. As a result,

1978 heavily nested goals become amenable to fundamental operations such

1979 as resolution (cf.\ the @{method (Pure) rule} method). Giving the ``@{text

1980 "(full)"}'' option here means to turn the whole subgoal into an

1981 object-statement (if possible), including the outermost parameters

1982 and assumptions as well.

1984 A typical collection of @{attribute atomize} rules for a particular

1985 object-logic would provide an internalization for each of the

1986 connectives of @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"}.

1987 Meta-level conjunction should be covered as well (this is

1988 particularly important for locales, see \secref{sec:locale}).

1990 \item @{attribute rule_format} rewrites a theorem by the equalities

1991 declared as @{attribute rulify} rules in the current object-logic.

1992 By default, the result is fully normalized, including assumptions

1993 and conclusions at any depth. The @{text "(no_asm)"} option

1994 restricts the transformation to the conclusion of a rule.

1996 In common object-logics (HOL, FOL, ZF), the effect of @{attribute

1997 rule_format} is to replace (bounded) universal quantification

1998 (@{text "\<forall>"}) and implication (@{text "\<longrightarrow>"}) by the corresponding

1999 rule statements over @{text "\<And>"} and @{text "\<Longrightarrow>"}.

2001 \end{description}

2002 \<close>

2005 section \<open>Tracing higher-order unification\<close>

2007 text \<open>

2008 \begin{tabular}{rcll}

2009 @{attribute_def unify_trace_simp} & : & @{text "attribute"} & default @{text "false"} \\

2010 @{attribute_def unify_trace_types} & : & @{text "attribute"} & default @{text "false"} \\

2011 @{attribute_def unify_trace_bound} & : & @{text "attribute"} & default @{text "50"} \\

2012 @{attribute_def unify_search_bound} & : & @{text "attribute"} & default @{text "60"} \\

2013 \end{tabular}

2014 \medskip

2016 Higher-order unification works well in most practical situations,

2017 but sometimes needs extra care to identify problems. These tracing

2018 options may help.

2020 \begin{description}

2022 \item @{attribute unify_trace_simp} controls tracing of the

2023 simplification phase of higher-order unification.

2025 \item @{attribute unify_trace_types} controls warnings of

2026 incompleteness, when unification is not considering all possible

2027 instantiations of schematic type variables.

2029 \item @{attribute unify_trace_bound} determines the depth where

2030 unification starts to print tracing information once it reaches

2031 depth; 0 for full tracing. At the default value, tracing

2032 information is almost never printed in practice.

2034 \item @{attribute unify_search_bound} prevents unification from

2035 searching past the given depth. Because of this bound, higher-order

2036 unification cannot return an infinite sequence, though it can return

2037 an exponentially long one. The search rarely approaches the default

2038 value in practice. If the search is cut off, unification prints a

2039 warning ``Unification bound exceeded''.

2041 \end{description}

2043 \begin{warn}

2044 Options for unification cannot be modified in a local context. Only

2045 the global theory content is taken into account.

2046 \end{warn}

2047 \<close>

2049 end