
1 theory Generic 

2 imports Base Main 

3 begin 

4 

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

6 

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

8 

9 text {* Isabelle/Pure maintains a record of named configuration 

10 options within the theory or proof context, with values of type 

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

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

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

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

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

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

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

18 this: 

19 *} 

20 

21 declare [[show_main_goal = false]] 

22 

23 notepad 

24 begin 

25 note [[show_main_goal = true]] 

26 end 

27 

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

29 context into account and merely refer to the background theory. 

30 This is accommodated by configuration options being declared as 

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

32 

33 \begin{matharray}{rcll} 

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

35 \end{matharray} 

36 

37 @{rail " 

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

39 "} 

40 

41 \begin{description} 

42 

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

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

45 

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. 

50 

51 \end{description} 

52 *} 

53 

54 

55 section {* Basic proof tools *} 

56 

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

58 

59 text {* 

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} 

72 

73 @{rail " 

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 "} 

81 

82 \begin{description} 

83 

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. 

88 

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. 

92 

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

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

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

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

97 elimresolution, destructresolution, and forwardresolution, 

98 respectively \cite{isabelleimplementation}. The optional natural 

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

100 be performed here. 

101 

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

103 experimentation and tactic script emulation. Different modes of 

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

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

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

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

108 facts. 

109 

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

111 by intro or elimresolution, after having inserted any chained 

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

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

114 to common automated tools. 

115 

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

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

118 \secref{sec:proofmeth}). 

119 

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

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

122 \secref{sec:proofmeth}). 

123 

124 \end{description} 

125 

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 standard}@{text "\<^sup>*"} & : & @{text attribute} \\ 

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

137 \end{matharray} 

138 

139 @{rail " 

140 @@{attribute tagged} @{syntax name} @{syntax name} 

141 ; 

142 @@{attribute untagged} @{syntax name} 

143 ; 

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

145 ; 

146 (@@{attribute unfolded}  @@{attribute folded}) @{syntax thmrefs} 

147 ; 

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

149 "} 

150 

151 \begin{description} 

152 

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

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

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

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

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

158 

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

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

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

162 \cite{isabelleimplementation}. 

163 

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

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

166 definitions throughout a rule. 

167 

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

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

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

171 for objectlogic equality. 

172 

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

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

175 

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

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

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

179 

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

181 its own version of this operation. 

182 

183 \item @{attribute standard} puts a theorem into the standard form of 

184 objectrules at the outermost theory level. Note that this 

185 operation violates the local proof context (including active 

186 locales). 

187 

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

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

190 

191 \end{description} 

192 *} 

193 

194 

195 subsection {* Lowlevel equational reasoning *} 

196 

197 text {* 

198 \begin{matharray}{rcl} 

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

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

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

202 \end{matharray} 

203 

204 @{rail " 

205 @@{method subst} ('(' 'asm' ')')? \\ ('(' (@{syntax nat}+) ')')? @{syntax thmref} 

206 ; 

207 @@{method split} @{syntax thmrefs} 

208 "} 

209 

210 These methods provide lowlevel facilities for equational reasoning 

211 that are intended for specialized applications only. Normally, 

212 single step calculations would be performed in a structured text 

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

214 provide the canonical way for automated normalization (see 

215 \secref{sec:simplifier}). 

216 

217 \begin{description} 

218 

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

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

221 equality. 

222 

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

224 assumption. 

225 

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

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

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

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

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

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

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

233 

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

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

236 assume all substitutions are performed simultaneously. Otherwise 

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

238 

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

240 substitutions in the assumptions. The positions refer to the 

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

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

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

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

245 

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

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

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

249 

250 \item @{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} performs singlestep case 

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

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

253 structure of the rule. 

254 

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

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

257 @{attribute split}, for example. 

258 

259 \end{description} 

260 *} 

261 

262 

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

264 

265 text {* 

266 The following improper proof methods emulate traditional tactics. 

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

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

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

270 scope of some subgoal. 

271 

272 \begin{warn} 

273 Dynamic instantiations refer to universally quantified parameters 

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

275 term abbreviations of a (static) Isar context. 

276 \end{warn} 

277 

278 Tactic emulation methods, unlike their ML counterparts, admit 

279 simultaneous instantiation from both dynamic and static contexts. 

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

281 variables. Likewise, schematic variables refer to term 

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

283 schematic variable is interpreted as a schematic variable and left 

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

285 

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

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

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

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

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

291 \secref{sec:puremethatt}). 

292 

293 \begin{matharray}{rcl} 

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

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

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

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

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

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

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

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

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

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

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

305 \end{matharray} 

306 

307 @{rail " 

308 (@@{method rule_tac}  @@{method erule_tac}  @@{method drule_tac}  

309 @@{method frule_tac}  @@{method cut_tac}  @@{method thin_tac}) @{syntax goal_spec}? \\ 

310 ( dynamic_insts @'in' @{syntax thmref}  @{syntax thmrefs} ) 

311 ; 

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

313 ; 

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

315 ; 

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

317 ; 

318 (@@{method tactic}  @@{method raw_tactic}) @{syntax text} 

319 ; 

320 

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

322 "} 

323 

324 \begin{description} 

325 

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

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

328 res_inst_tac} etc. (see \cite{isabelleimplementation}) 

329 

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

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

332 \cite{isabelleimplementation}). 

333 

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

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

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

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

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

339 closed rule statements. 

340 

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

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

343 variables, to abbreviate the intended proposition; the first 

344 matching subgoal premise will be deleted. Removing useless premises 

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

346 run faster. 

347 

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

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

350 as new subgoals (in the original context). 

351 

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

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

354 \emph{suffix} of variables. 

355 

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

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

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

359 default value is 1. 

360 

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

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

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

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

365 current facts used for forwardchaining. 

366 

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

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

369 subgoals appear as conjunction of the logical framework instead of 

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

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

372 appear in production theories. 

373 

374 \end{description} 

375 *} 

376 

377 

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

379 

380 subsection {* Simplification methods *} 

381 

382 text {* 

383 \begin{matharray}{rcl} 

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

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

386 \end{matharray} 

387 

388 @{rail " 

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

390 ; 

391 

392 opt: '(' ('no_asm'  'no_asm_simp'  'no_asm_use'  'asm_lr' ) ')' 

393 ; 

394 @{syntax_def simpmod}: ('add'  'del'  'only'  'cong' (()  'add'  'del')  

395 'split' (()  'add'  'del')) ':' @{syntax thmrefs} 

396 "} 

397 

398 \begin{description} 

399 

400 \item @{method simp} invokes the Simplifier, after declaring 

401 additional rules according to the arguments given. Note that the 

402 @{text only} modifier first removes all other rewrite rules, 

403 congruences, and looper tactics (including splits), and then behaves 

404 like @{text add}. 

405 

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

407 congruence rules (see also \secref{sec:simpcong}), the default is 

408 to add. 

409 

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

411 Splitter (see also \cite{isabelleref}), the default is to add. 

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

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

414 ZF do this already). 

415 

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

417 all goals (backwards from the last to the first one). 

418 

419 \end{description} 

420 

421 By default the Simplifier methods take local assumptions fully into 

422 account, using equational assumptions in the subsequent 

423 normalization process, or simplifying assumptions themselves (cf.\ 

424 @{ML asm_full_simp_tac} in \cite{isabelleref}). In structured 

425 proofs this is usually quite well behaved in practice: just the 

426 local premises of the actual goal are involved, additional facts may 

427 be inserted via explicit forwardchaining (via @{command "then"}, 

428 @{command "from"}, @{command "using"} etc.). 

429 

430 Additional Simplifier options may be specified to tune the behavior 

431 further (mostly for unstructured scripts with many accidental local 

432 facts): ``@{text "(no_asm)"}'' means assumptions are ignored 

433 completely (cf.\ @{ML simp_tac}), ``@{text "(no_asm_simp)"}'' means 

434 assumptions are used in the simplification of the conclusion but are 

435 not themselves simplified (cf.\ @{ML asm_simp_tac}), and ``@{text 

436 "(no_asm_use)"}'' means assumptions are simplified but are not used 

437 in the simplification of each other or the conclusion (cf.\ @{ML 

438 full_simp_tac}). For compatibility reasons, there is also an option 

439 ``@{text "(asm_lr)"}'', which means that an assumption is only used 

440 for simplifying assumptions which are to the right of it (cf.\ @{ML 

441 asm_lr_simp_tac}). 

442 

443 The configuration option @{text "depth_limit"} limits the number of 

444 recursive invocations of the simplifier during conditional 

445 rewriting. 

446 

447 \medskip The Splitter package is usually configured to work as part 

448 of the Simplifier. The effect of repeatedly applying @{ML 

449 split_tac} can be simulated by ``@{text "(simp only: split: 

450 a\<^sub>1 \<dots> a\<^sub>n)"}''. There is also a separate @{text split} 

451 method available for singlestep case splitting. 

452 *} 

453 

454 

455 subsection {* Declaring rules *} 

456 

457 text {* 

458 \begin{matharray}{rcl} 

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

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

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

462 \end{matharray} 

463 

464 @{rail " 

465 (@@{attribute simp}  @@{attribute split}) (()  'add'  'del') 

466 "} 

467 

468 \begin{description} 

469 

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

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

472 internally \cite{isabelleref}. 

473 

474 \item @{attribute simp} declares simplification rules. 

475 

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

477 

478 \end{description} 

479 *} 

480 

481 

482 subsection {* Congruence rules\label{sec:simpcong} *} 

483 

484 text {* 

485 \begin{matharray}{rcl} 

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

487 \end{matharray} 

488 

489 @{rail " 

490 @@{attribute cong} (()  'add'  'del') 

491 "} 

492 

493 \begin{description} 

494 

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

496 context. 

497 

498 \end{description} 

499 

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

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

502 

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

504 example, some arguments can be simplified under additional 

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

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

507 

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

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

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

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

512 

513 %FIXME 

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

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

516 

517 \medskip The following congruence rule for bounded quantifiers also 

518 supplies contextual information  about the bound variable: 

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

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

521 

522 \medskip This congruence rule for conditional expressions can 

523 supply contextual information for simplifying the arms: 

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

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

526 

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

528 arguments. Here is an alternative congruence rule for conditional 

529 expressions that conforms to nonstrict functional evaluation: 

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

531 

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

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

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

535 *} 

536 

537 

538 subsection {* Simplification procedures *} 

539 

540 text {* Simplification procedures are ML functions that produce proven 

541 rewrite rules on demand. They are associated with higherorder 

542 patterns that approximate the lefthand sides of equations. The 

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

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

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

546 may be specifically fashioned for particular situations, resulting 

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

548 rules. 

549 

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

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

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

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

554 automatic preprocessing of objectlevel equivalences. 

555 

556 \begin{matharray}{rcl} 

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

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

559 \end{matharray} 

560 

561 @{rail " 

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

563 @{syntax text} \\ (@'identifier' (@{syntax nameref}+))? 

564 ; 

565 

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

567 "} 

568 

569 \begin{description} 

570 

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

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

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

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

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

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

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

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

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

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

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

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

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

584 represent the logical content of the abstract theory of this 

585 simproc. 

586 

587 Morphisms and identifiers are only relevant for simprocs that are 

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

589 

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

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

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

593 already adds the new simproc to the subsequent context. 

594 

595 \end{description} 

596 *} 

597 

598 

599 subsubsection {* Example *} 

600 

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

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

603 control over rule application, beyond higherorder pattern matching. 

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

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

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

607 

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

609 fn _ => fn _ => fn ct => 

610 if HOLogic.is_unit (term_of ct) then NONE 

611 else SOME (mk_meta_eq @{thm unit_eq}) 

612 *} 

613 

614 text {* Since the Simplifier applies simplification procedures 

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

616 reasonably fast. *} 

617 

618 

619 subsection {* Forward simplification *} 

620 

621 text {* 

622 \begin{matharray}{rcl} 

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

624 \end{matharray} 

625 

626 @{rail " 

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

628 ; 

629 

630 opt: '(' ('no_asm'  'no_asm_simp'  'no_asm_use') ')' 

631 "} 

632 

633 \begin{description} 

634 

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

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

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

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

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

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

641 

642 Note that forward simplification restricts the simplifier to its 

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

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

645 simplified} attribute should be only rarely required under normal 

646 circumstances. 

647 

648 \end{description} 

649 *} 

650 

651 

652 section {* The Classical Reasoner \label{sec:classical} *} 

653 

654 subsection {* Basic concepts *} 

655 

656 text {* Although Isabelle is generic, many users will be working in 

657 some extension of classical firstorder logic. Isabelle/ZF is built 

658 upon theory FOL, while Isabelle/HOL conceptually contains 

659 firstorder logic as a fragment. Theoremproving in predicate logic 

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

661 assist in this task. 

662 

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

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

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

666 context. These proof procedures are slow and simplistic compared 

667 with highend automated theorem provers, but they can save 

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

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

670 milliseconds (including full proof reconstruction): *} 

671 

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

673 by blast 

674 

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

676 by blast 

677 

678 text {* The proof tools are generic. They are not restricted to 

679 firstorder logic, and have been heavily used in the development of 

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

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

682 any proof can be viewed interactively. *} 

683 

684 

685 subsubsection {* The sequent calculus *} 

686 

687 text {* Isabelle supports natural deduction, which is easy to use for 

688 interactive proof. But natural deduction does not easily lend 

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

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

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

692 is easier to automate. 

693 

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

695 and @{text "\<Delta>"} are sets of formulae.\footnote{For firstorder 

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

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

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

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

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

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

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

703 valid. 

704 

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

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

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

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

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

710 is the rule 

711 \[ 

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

713 \] 

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

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

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

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

718 single rule 

719 \[ 

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

721 \] 

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

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

724 multipleconclusion logic. 

725 

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

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

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

729 \[ 

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

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

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

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

734 \] 

735 

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

737 desired theorem and apply rules backwards in a fairly arbitrary 

738 manner. This yields a surprisingly effective proof procedure. 

739 Quantifiers add only few complications, since Isabelle handles 

740 parameters and schematic variables. See \cite[Chapter 

741 10]{paulsonml2} for further discussion. *} 

742 

743 

744 subsubsection {* Simulating sequents by natural deduction *} 

745 

746 text {* Isabelle can represent sequents directly, as in the 

747 objectlogic LK. But natural deduction is easier to work with, and 

748 most objectlogics employ it. Fortunately, we can simulate the 

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

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

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

752 Elimresolution plays a key role in simulating sequent proofs. 

753 

754 We can easily handle reasoning on the left. Elimresolution with 

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

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

757 connectives, we use sequentstyle elimination rules instead of 

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

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

760 representation of sequents! 

761 \[ 

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

763 \] 

764 

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

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

767 other rightside formulae are represented as negated assumptions, 

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

769 must first be exchanged with @{text "Q\<^sub>1"}. Elimresolution with the 

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

771 

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

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

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

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

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

777 

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

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

780 

781 Swapped introduction rules are applied using elimresolution, which 

782 deletes the negated formula. Our representation of sequents also 

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

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

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

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

787 *} 

788 

789 

790 subsubsection {* Extra rules for the sequent calculus *} 

791 

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

793 @{text "(\<forall>E)"} must be replaced by sequentstyle elimination rules. 

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

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

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

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

798 

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

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

801 

802 Quantifier replication also requires special rules. In classical 

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

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

805 \[ 

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

807 \qquad 

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

809 \] 

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

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

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

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

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

815 \<longrightarrow> P y"}. 

816 

817 Forgoing quantifier replication loses completeness, but gains 

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

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

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

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

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

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

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

825 

826 Elimresolution with this rule will delete the universal formula 

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

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

829 

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

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

832 

833 All introduction rules mentioned above are also useful in swapped 

834 form. 

835 

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

837 with care. The classical reasoner distinguishes between safe and 

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

839 Depthfirst search may well go down a blind alley; bestfirst search 

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

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

842 *} 

843 

844 

845 subsection {* Rule declarations *} 

846 

847 text {* The proof tools of the Classical Reasoner depend on 

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

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

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

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

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

853 

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

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

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

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

858 unsafe, since it is applied via elimresolution, which discards the 

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

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

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

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

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

864 looping. In classical firstorder logic, all rules are safe except 

865 those mentioned above. 

866 

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

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

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

870 could generate exponentially many subgoals. Induction rules are 

871 unsafe because inductive proofs are difficult to set up 

872 automatically. Any inference is unsafe that instantiates an unknown 

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

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

875 unknowns shared with other subgoals. 

876 

877 \begin{matharray}{rcl} 

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

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

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

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

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

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

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

885 \end{matharray} 

886 

887 @{rail " 

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

889 ; 

890 @@{attribute rule} 'del' 

891 ; 

892 @@{attribute iff} (((()  'add') '?'?)  'del') 

893 "} 

894 

895 \begin{description} 

896 

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

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

899 within the context. 

900 

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

902 declare introduction, elimination, and destruction rules, 

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

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

905 "!"}'' classifies as \emph{safe}. Rule declarations marked by 

906 ``@{text "?"}'' coincide with those of Isabelle/Pure, cf.\ 

907 \secref{sec:puremethatt} (i.e.\ are only applied in single steps 

908 of the @{method rule} method). The optional natural number 

909 specifies an explicit weight argument, which is ignored by the 

910 automated reasoning tools, but determines the search order of single 

911 rule steps. 

912 

913 Introduction rules are those that can be applied using ordinary 

914 resolution. Their swapped forms are generated internally, which 

915 will be applied using elimresolution. Elimination rules are 

916 applied using elimresolution. Rules are sorted by the number of 

917 new subgoals they will yield; rules that generate the fewest 

918 subgoals will be tried first. Otherwise, later declarations take 

919 precedence over earlier ones. 

920 

921 Rules already present in the context with the same classification 

922 are ignored. A warning is printed if the rule has already been 

923 added with some other classification, but the rule is added anyway 

924 as requested. 

925 

926 \item @{attribute rule}~@{text del} deletes all occurrences of a 

927 rule from the classical context, regardless of its classification as 

928 introduction~/ elimination~/ destruction and safe~/ unsafe. 

929 

930 \item @{attribute iff} declares logical equivalences to the 

931 Simplifier and the Classical reasoner at the same time. 

932 Nonconditional rules result in a safe introduction and elimination 

933 pair; conditional ones are considered unsafe. Rules with negative 

934 conclusion are automatically inverted (using @{text "\<not>"}elimination 

935 internally). 

936 

937 The ``@{text "?"}'' version of @{attribute iff} declares rules to 

938 the Isabelle/Pure context only, and omits the Simplifier 

939 declaration. 

940 

941 \item @{attribute swapped} turns an introduction rule into an 

942 elimination, by resolving with the classical swap principle @{text 

943 "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"} in the second position. This is mainly for 

944 illustrative purposes: the Classical Reasoner already swaps rules 

945 internally as explained above. 

946 

947 \end{description} 

948 *} 

949 

950 

951 subsection {* Structured methods *} 

952 

953 text {* 

954 \begin{matharray}{rcl} 

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

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

957 \end{matharray} 

958 

959 @{rail " 

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

961 "} 

962 

963 \begin{description} 

964 

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

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

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

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

969 

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

971 classical rules (even if these would qualify as intuitionistic 

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

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

974 

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

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

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

978 order. 

979 

980 \end{description} 

981 *} 

982 

983 

984 subsection {* Automated methods *} 

985 

986 text {* 

987 \begin{matharray}{rcl} 

988 @{method_def blast} & : & @{text method} \\ 

989 @{method_def auto} & : & @{text method} \\ 

990 @{method_def force} & : & @{text method} \\ 

991 @{method_def fast} & : & @{text method} \\ 

992 @{method_def slow} & : & @{text method} \\ 

993 @{method_def best} & : & @{text method} \\ 

994 @{method_def fastforce} & : & @{text method} \\ 

995 @{method_def slowsimp} & : & @{text method} \\ 

996 @{method_def bestsimp} & : & @{text method} \\ 

997 @{method_def deepen} & : & @{text method} \\ 

998 \end{matharray} 

999 

1000 @{rail " 

1001 @@{method blast} @{syntax nat}? (@{syntax clamod} * ) 

1002 ; 

1003 @@{method auto} (@{syntax nat} @{syntax nat})? (@{syntax clasimpmod} * ) 

1004 ; 

1005 @@{method force} (@{syntax clasimpmod} * ) 

1006 ; 

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

1008 ; 

1009 (@@{method fastforce}  @@{method slowsimp}  @@{method bestsimp}) 

1010 (@{syntax clasimpmod} * ) 

1011 ; 

1012 @@{method deepen} (@{syntax nat} ?) (@{syntax clamod} * ) 

1013 ; 

1014 @{syntax_def clamod}: 

1015 (('intro'  'elim'  'dest') ('!'  ()  '?')  'del') ':' @{syntax thmrefs} 

1016 ; 

1017 @{syntax_def clasimpmod}: ('simp' (()  'add'  'del'  'only')  

1018 ('cong'  'split') (()  'add'  'del')  

1019 'iff' (((()  'add') '?'?)  'del')  

1020 (('intro'  'elim'  'dest') ('!'  ()  '?')  'del')) ':' @{syntax thmrefs} 

1021 "} 

1022 

1023 \begin{description} 

1024 

1025 \item @{method blast} is a separate classical tableau prover that 

1026 uses the same classical rule declarations as explained before. 

1027 

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

1029 A successful proof is then reconstructed using regular Isabelle 

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

1031 reasoning tools, but has major limitations too. 

1032 

1033 \begin{itemize} 

1034 

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

1036 integration with the Simplifier of @{method fastforce}. 

1037 

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

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

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

1041 range_eqI}. 

1042 

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

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

1045 higherorder unification.) If other function variables are present 

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

1047 argument not a bound variable}. 

1048 

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

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

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

1052 

1053 \end{itemize} 

1054 

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

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

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

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

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

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

1061 proof method instead. 

1062 

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

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

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

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

1067 ones may take a long time. 

1068 

1069 The optional depth arguments in @{text "(auto m n)"} refer to its 

1070 builtin classical reasoning procedures: @{text m} (default 4) is for 

1071 @{method blast}, which is tried first, and @{text n} (default 2) is 

1072 for a slower but more general alternative that also takes wrappers 

1073 into account. 

1074 

1075 \item @{method force} is intended to prove the first subgoal 

1076 completely, using many fancy proof tools and performing a rather 

1077 exhaustive search. As a result, proof attempts may take rather long 

1078 or diverge easily. 

1079 

1080 \item @{method fast}, @{method best}, @{method slow} attempt to 

1081 prove the first subgoal using sequentstyle reasoning as explained 

1082 before. Unlike @{method blast}, they construct proofs directly in 

1083 Isabelle. 

1084 

1085 There is a difference in search strategy and backtracking: @{method 

1086 fast} uses depthfirst search and @{method best} uses bestfirst 

1087 search (guided by a heuristic function: normally the total size of 

1088 the proof state). 

1089 

1090 Method @{method slow} is like @{method fast}, but conducts a broader 

1091 search: it may, when backtracking from a failed proof attempt, undo 

1092 even the step of proving a subgoal by assumption. 

1093 

1094 \item @{method fastforce}, @{method slowsimp}, @{method bestsimp} 

1095 are like @{method fast}, @{method slow}, @{method best}, 

1096 respectively, but use the Simplifier as additional wrapper. The name 

1097 @{method fastforce}, reflects the behaviour of this popular method 

1098 better without requiring an understanding of its implementation. 

1099 

1100 \item @{method deepen} works by exhaustive search up to a certain 

1101 depth. The start depth is 4 (unless specified explicitly), and the 

1102 depth is increased iteratively up to 10. Unsafe rules are modified 

1103 to preserve the formula they act on, so that it be used repeatedly. 

1104 This method can prove more goals than @{method fast}, but is much 

1105 slower, for example if the assumptions have many universal 

1106 quantifiers. 

1107 

1108 \end{description} 

1109 

1110 Any of the above methods support additional modifiers of the context 

1111 of classical (and simplifier) rules, but the ones related to the 

1112 Simplifier are explicitly prefixed by @{text simp} here. The 

1113 semantics of these adhoc rule declarations is analogous to the 

1114 attributes given before. Facts provided by forward chaining are 

1115 inserted into the goal before commencing proof search. 

1116 *} 

1117 

1118 

1119 subsection {* Semiautomated methods *} 

1120 

1121 text {* These proof methods may help in situations when the 

1122 fullyautomated tools fail. The result is a simpler subgoal that 

1123 can be tackled by other means, such as by manual instantiation of 

1124 quantifiers. 

1125 

1126 \begin{matharray}{rcl} 

1127 @{method_def safe} & : & @{text method} \\ 

1128 @{method_def clarify} & : & @{text method} \\ 

1129 @{method_def clarsimp} & : & @{text method} \\ 

1130 \end{matharray} 

1131 

1132 @{rail " 

1133 (@@{method safe}  @@{method clarify}) (@{syntax clamod} * ) 

1134 ; 

1135 @@{method clarsimp} (@{syntax clasimpmod} * ) 

1136 "} 

1137 

1138 \begin{description} 

1139 

1140 \item @{method safe} repeatedly performs safe steps on all subgoals. 

1141 It is deterministic, with at most one outcome. 

1142 

1143 \item @{method clarify} performs a series of safe steps without 

1144 splitting subgoals; see also @{ML clarify_step_tac}. 

1145 

1146 \item @{method clarsimp} acts like @{method clarify}, but also does 

1147 simplification. Note that if the Simplifier context includes a 

1148 splitter for the premises, the subgoal may still be split. 

1149 

1150 \end{description} 

1151 *} 

1152 

1153 

1154 subsection {* Singlestep tactics *} 

1155 

1156 text {* 

1157 \begin{matharray}{rcl} 

1158 @{index_ML safe_step_tac: "Proof.context > int > tactic"} \\ 

1159 @{index_ML inst_step_tac: "Proof.context > int > tactic"} \\ 

1160 @{index_ML step_tac: "Proof.context > int > tactic"} \\ 

1161 @{index_ML slow_step_tac: "Proof.context > int > tactic"} \\ 

1162 @{index_ML clarify_step_tac: "Proof.context > int > tactic"} \\ 

1163 \end{matharray} 

1164 

1165 These are the primitive tactics behind the (semi)automated proof 

1166 methods of the Classical Reasoner. By calling them yourself, you 

1167 can execute these procedures one step at a time. 

1168 

1169 \begin{description} 

1170 

1171 \item @{ML safe_step_tac}~@{text "ctxt i"} performs a safe step on 

1172 subgoal @{text i}. The safe wrapper tacticals are applied to a 

1173 tactic that may include proof by assumption or Modus Ponens (taking 

1174 care not to instantiate unknowns), or substitution. 

1175 

1176 \item @{ML inst_step_tac} is like @{ML safe_step_tac}, but allows 

1177 unknowns to be instantiated. 

1178 

1179 \item @{ML step_tac}~@{text "ctxt i"} is the basic step of the proof 

1180 procedure. The unsafe wrapper tacticals are applied to a tactic 

1181 that tries @{ML safe_tac}, @{ML inst_step_tac}, or applies an unsafe 

1182 rule from the context. 

1183 

1184 \item @{ML slow_step_tac} resembles @{ML step_tac}, but allows 

1185 backtracking between using safe rules with instantiation (@{ML 

1186 inst_step_tac}) and using unsafe rules. The resulting search space 

1187 is larger. 

1188 

1189 \item @{ML clarify_step_tac}~@{text "ctxt i"} performs a safe step 

1190 on subgoal @{text i}. No splitting step is applied; for example, 

1191 the subgoal @{text "A \<and> B"} is left as a conjunction. Proof by 

1192 assumption, Modus Ponens, etc., may be performed provided they do 

1193 not instantiate unknowns. Assumptions of the form @{text "x = t"} 

1194 may be eliminated. The safe wrapper tactical is applied. 

1195 

1196 \end{description} 

1197 *} 

1198 

1199 

1200 section {* Objectlogic setup \label{sec:objectlogic} *} 

1201 

1202 text {* 

1203 \begin{matharray}{rcl} 

1204 @{command_def "judgment"} & : & @{text "theory \<rightarrow> theory"} \\ 

1205 @{method_def atomize} & : & @{text method} \\ 

1206 @{attribute_def atomize} & : & @{text attribute} \\ 

1207 @{attribute_def rule_format} & : & @{text attribute} \\ 

1208 @{attribute_def rulify} & : & @{text attribute} \\ 

1209 \end{matharray} 

1210 

1211 The very starting point for any Isabelle objectlogic is a ``truth 

1212 judgment'' that links objectlevel statements to the metalogic 

1213 (with its minimal language of @{text prop} that covers universal 

1214 quantification @{text "\<And>"} and implication @{text "\<Longrightarrow>"}). 

1215 

1216 Common objectlogics are sufficiently expressive to internalize rule 

1217 statements over @{text "\<And>"} and @{text "\<Longrightarrow>"} within their own 

1218 language. This is useful in certain situations where a rule needs 

1219 to be viewed as an atomic statement from the metalevel perspective, 

1220 e.g.\ @{text "\<And>x. x \<in> A \<Longrightarrow> P x"} versus @{text "\<forall>x \<in> A. P x"}. 

1221 

1222 From the following language elements, only the @{method atomize} 

1223 method and @{attribute rule_format} attribute are occasionally 

1224 required by endusers, the rest is for those who need to setup their 

1225 own objectlogic. In the latter case existing formulations of 

1226 Isabelle/FOL or Isabelle/HOL may be taken as realistic examples. 

1227 

1228 Generic tools may refer to the information provided by objectlogic 

1229 declarations internally. 

1230 

1231 @{rail " 

1232 @@{command judgment} @{syntax name} '::' @{syntax type} @{syntax mixfix}? 

1233 ; 

1234 @@{attribute atomize} ('(' 'full' ')')? 

1235 ; 

1236 @@{attribute rule_format} ('(' 'noasm' ')')? 

1237 "} 

1238 

1239 \begin{description} 

1240 

1241 \item @{command "judgment"}~@{text "c :: \<sigma> (mx)"} declares constant 

1242 @{text c} as the truth judgment of the current objectlogic. Its 

1243 type @{text \<sigma>} should specify a coercion of the category of 

1244 objectlevel propositions to @{text prop} of the Pure metalogic; 

1245 the mixfix annotation @{text "(mx)"} would typically just link the 

1246 object language (internally of syntactic category @{text logic}) 

1247 with that of @{text prop}. Only one @{command "judgment"} 

1248 declaration may be given in any theory development. 

1249 

1250 \item @{method atomize} (as a method) rewrites any nonatomic 

1251 premises of a subgoal, using the metalevel equations declared via 

1252 @{attribute atomize} (as an attribute) beforehand. As a result, 

1253 heavily nested goals become amenable to fundamental operations such 

1254 as resolution (cf.\ the @{method (Pure) rule} method). Giving the ``@{text 

1255 "(full)"}'' option here means to turn the whole subgoal into an 

1256 objectstatement (if possible), including the outermost parameters 

1257 and assumptions as well. 

1258 

1259 A typical collection of @{attribute atomize} rules for a particular 

1260 objectlogic would provide an internalization for each of the 

1261 connectives of @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"}. 

1262 Metalevel conjunction should be covered as well (this is 

1263 particularly important for locales, see \secref{sec:locale}). 

1264 

1265 \item @{attribute rule_format} rewrites a theorem by the equalities 

1266 declared as @{attribute rulify} rules in the current objectlogic. 

1267 By default, the result is fully normalized, including assumptions 

1268 and conclusions at any depth. The @{text "(no_asm)"} option 

1269 restricts the transformation to the conclusion of a rule. 

1270 

1271 In common objectlogics (HOL, FOL, ZF), the effect of @{attribute 

1272 rule_format} is to replace (bounded) universal quantification 

1273 (@{text "\<forall>"}) and implication (@{text "\<longrightarrow>"}) by the corresponding 

1274 rule statements over @{text "\<And>"} and @{text "\<Longrightarrow>"}. 

1275 

1276 \end{description} 

1277 *} 

1278 

1279 end 