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

src/Doc/Eisbach/Manual.thy

author | wenzelm |

Sun May 17 23:03:49 2015 +0200 (2015-05-17) | |

changeset 60288 | d7f636331176 |

child 60298 | 7c278b692aae |

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

added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;

1 (*:wrap=hard:maxLineLen=78:*)

3 theory Manual

4 imports Base "../Eisbach_Tools"

5 begin

7 chapter \<open>The method command\<close>

9 text \<open>

10 The @{command_def method} command provides the ability to write proof

11 methods by combining existing ones with their usual syntax. Specifically it

12 allows compound proof methods to be named, and to extend the name space of

13 basic methods accordingly. Method definitions may abstract over parameters:

14 terms, facts, or other methods.

16 \medskip The syntax diagram below refers to some syntactic categories that

17 are further defined in @{cite "isabelle-isar-ref"}.

19 @{rail \<open>

20 @@{command method} name args @'=' method

21 ;

22 args: term_args? method_args? \<newline> fact_args? decl_args?

23 ;

24 term_args: @'for' @{syntax "fixes"}

25 ;

26 method_args: @'methods' (name+)

27 ;

28 fact_args: @'uses' (name+)

29 ;

30 decl_args: @'declares' (name+)

31 \<close>}

32 \<close>

35 section \<open>Basic method definitions\<close>

37 text \<open>

38 Consider the following proof that makes use of usual Isar method

39 combinators.

40 \<close>

42 lemma "P \<and> Q \<longrightarrow> P"

43 by ((rule impI, (erule conjE)?) | assumption)+

45 text \<open>

46 It is clear that this compound method will be applicable in more cases than

47 this proof alone. With the @{command method} command we can define a proof

48 method that makes the above functionality available generally.

49 \<close>

51 method prop_solver\<^sub>1 =

52 ((rule impI, (erule conjE)?) | assumption)+

54 lemma "P \<and> Q \<and> R \<longrightarrow> P"

55 by prop_solver\<^sub>1

57 text \<open>

58 In this example, the facts @{text impI} and @{text conjE} are static. They

59 are evaluated once when the method is defined and cannot be changed later.

60 This makes the method stable in the sense of \emph{static scoping}: naming

61 another fact @{text impI} in a later context won't affect the behaviour of

62 @{text "prop_solver\<^sub>1"}.

63 \<close>

66 section \<open>Term abstraction\<close>

68 text \<open>

69 Methods can also abstract over terms using the @{keyword_def "for"} keyword,

70 optionally providing type constraints. For instance, the following proof

71 method @{text intro_ex} takes a term @{term y} of any type, which it uses to

72 instantiate the @{term x}-variable of @{text exI} (existential introduction)

73 before applying the result as a rule. The instantiation is performed here by

74 Isar's @{attribute_ref "where"} attribute. If the current subgoal is to find

75 a witness for the given predicate @{term Q}, then this has the effect of

76 committing to @{term y}.

77 \<close>

79 method intro_ex for Q :: "'a \<Rightarrow> bool" and y :: 'a =

80 (rule exI ["where" P = Q and x = y])

83 text \<open>

84 The term parameters @{term y} and @{term Q} can be used arbitrarily inside

85 the method body, as part of attribute applications or arguments to other

86 methods. The expression is type-checked as far as possible when the method

87 is defined, however dynamic type errors can still occur when it is invoked

88 (e.g.\ when terms are instantiated in a parameterized fact). Actual term

89 arguments are supplied positionally, in the same order as in the method

90 definition.

91 \<close>

93 lemma "P a \<Longrightarrow> \<exists>x. P x"

94 by (intro_ex P a)

97 section \<open>Fact abstraction\<close>

99 subsection \<open>Named theorems\<close>

101 text \<open>

102 A @{text "named theorem"} is a fact whose contents are produced dynamically

103 within the current proof context. The Isar command @{command_ref

104 "named_theorems"} provides simple access to this concept: it declares a

105 dynamic fact with corresponding \emph{attribute}

106 (see \autoref{s:attributes}) for managing this particular data slot in the

107 context.

108 \<close>

110 named_theorems intros

112 text \<open>

113 So far @{text "intros"} refers to the empty fact. Using the Isar command

114 @{command_ref "declare"} we may apply declaration attributes to the context.

115 Below we declare both @{text "conjI"} and @{text "impI"} as @{text

116 "intros"}, adding them to the named theorem slot.

117 \<close>

119 declare conjI [intros] and impI [intros]

121 text \<open>

122 We can refer to named theorems as dynamic facts within a particular proof

123 context, which are evaluated whenever the method is invoked. Instead of

124 having facts hard-coded into the method, as in @{text prop_solver\<^sub>1}, we can

125 instead refer to these named theorems.

126 \<close>

128 named_theorems elims

129 declare conjE [elims]

131 method prop_solver\<^sub>3 =

132 ((rule intros, (erule elims)?) | assumption)+

134 lemma "P \<and> Q \<longrightarrow> P"

135 by prop_solver\<^sub>3

137 text \<open>

138 Often these named theorems need to be augmented on the spot, when a method

139 is invoked. The @{keyword_def "declares"} keyword in the signature of

140 @{command method} adds the common method syntax @{text "method decl: facts"}

141 for each named theorem @{text decl}.

142 \<close>

144 method prop_solver\<^sub>4 declares intros elims =

145 ((rule intros, (erule elims)?) | assumption)+

147 lemma "P \<and> (P \<longrightarrow> Q) \<longrightarrow> Q \<and> P"

148 by (prop_solver\<^sub>4 elims: impE intros: conjI)

151 subsection \<open>Simple fact abstraction\<close>

153 text \<open>

154 The @{keyword "declares"} keyword requires that a corresponding dynamic fact

155 has been declared with @{command_ref named_theorems}. This is useful for

156 managing collections of facts which are to be augmented with declarations,

157 but is overkill if we simply want to pass a fact to a method.

159 We may use the @{keyword_def "uses"} keyword in the method header to provide

160 a simple fact parameter. In contrast to @{keyword "declares"}, these facts

161 are always implicitly empty unless augmented when the method is invoked.

162 \<close>

164 method rule_twice uses my_rule =

165 (rule my_rule, rule my_rule)

167 lemma "P \<Longrightarrow> Q \<Longrightarrow> (P \<and> Q) \<and> Q"

168 by (rule_twice my_rule: conjI)

171 section \<open>Higher-order methods\<close>

173 text \<open>

174 The \emph{structured concatenation} combinator ``@{text "method\<^sub>1 ;

175 method\<^sub>2"}'' was introduced in Isabelle2015, motivated by development of

176 Eisbach. It is similar to ``@{text "method\<^sub>1, method\<^sub>2"}'', but @{text

177 method\<^sub>2} is invoked on on \emph{all} subgoals that have newly emerged from

178 @{text method\<^sub>1}. This is useful to handle cases where the number of

179 subgoals produced by a method is determined dynamically at run-time.

180 \<close>

182 method conj_with uses rule =

183 (intro conjI ; intro rule)

185 lemma

186 assumes A: "P"

187 shows "P \<and> P \<and> P"

188 by (conj_with rule: A)

190 text \<open>

191 Method definitions may take other methods as arguments, and thus implement

192 method combinators with prefix syntax. For example, to more usefully exploit

193 Isabelle's backtracking, the explicit requirement that a method solve all

194 produced subgoals is frequently useful. This can easily be written as a

195 \emph{higher-order method} using ``@{text ";"}''. The @{keyword "methods"}

196 keyword denotes method parameters that are other proof methods to be invoked

197 by the method being defined.

198 \<close>

200 method solve methods m = (m ; fail)

202 text \<open>

203 Given some method-argument @{text m}, @{text "solve \<open>m\<close>"} applies the

204 method @{text m} and then fails whenever @{text m} produces any new unsolved

205 subgoals --- i.e. when @{text m} fails to completely discharge the goal it

206 was applied to.

207 \<close>

210 section \<open>Example\<close>

212 text \<open>

213 With these simple features we are ready to write our first non-trivial proof

214 method. Returning to the first-order logic example, the following method

215 definition applies various rules with their canonical methods.

216 \<close>

218 named_theorems subst

220 method prop_solver declares intros elims subst =

221 (assumption |

222 (rule intros) | erule elims |

223 subst subst | subst (asm) subst |

224 (erule notE ; solve \<open>prop_solver\<close>))+

226 text \<open>

227 The only non-trivial part above is the final alternative @{text "(erule notE

228 ; solve \<open>prop_solver\<close>)"}. Here, in the case that all other alternatives

229 fail, the method takes one of the assumptions @{term "\<not> P"} of the current

230 goal and eliminates it with the rule @{text notE}, causing the goal to be

231 proved to become @{term P}. The method then recursively invokes itself on

232 the remaining goals. The job of the recursive call is to demonstrate that

233 there is a contradiction in the original assumptions (i.e.\ that @{term P}

234 can be derived from them). Note this recursive invocation is applied with

235 the @{method solve} method combinator to ensure that a contradiction will

236 indeed be shown. In the case where a contradiction cannot be found,

237 backtracking will occur and a different assumption @{term "\<not> Q"} will be

238 chosen for elimination.

240 Note that the recursive call to @{method prop_solver} does not have any

241 parameters passed to it. Recall that fact parameters, e.g.\ @{text

242 "intros"}, @{text "elims"}, and @{text "subst"}, are managed by declarations

243 in the current proof context. They will therefore be passed to any recursive

244 call to @{method prop_solver} and, more generally, any invocation of a

245 method which declares these named theorems.

247 \medskip After declaring some standard rules to the context, the @{method

248 prop_solver} becomes capable of solving non-trivial propositional

249 tautologies.\<close>

251 lemmas [intros] =

252 conjI -- \<open>@{thm conjI}\<close>

253 impI -- \<open>@{thm impI}\<close>

254 disjCI -- \<open>@{thm disjCI}\<close>

255 iffI -- \<open>@{thm iffI}\<close>

256 notI -- \<open>@{thm notI}\<close>

257 (*<*)TrueI(*>*)

258 lemmas [elims] =

259 impCE -- \<open>@{thm impCE}\<close>

260 conjE -- \<open>@{thm conjE}\<close>

261 disjE -- \<open>@{thm disjE}\<close>

263 lemma "(A \<or> B) \<and> (A \<longrightarrow> C) \<and> (B \<longrightarrow> C) \<longrightarrow> C"

264 by prop_solver

267 chapter \<open>The match method \label{s:matching}\<close>

269 text \<open>

270 So far we have seen methods defined as simple combinations of other methods.

271 Some familiar programming language concepts have been introduced (i.e.\

272 abstraction and recursion). The only control flow has been implicitly the

273 result of backtracking. When designing more sophisticated proof methods this

274 proves too restrictive and difficult to manage conceptually.

276 To address this, we introduce the @{method_def "match"} method, which

277 provides more direct access to the higher-order matching facility at the

278 core of Isabelle. It is implemented as a separate proof method (in

279 Isabelle/ML), and thus can be directly applied to proofs, however it is most

280 useful when applied in the context of writing Eisbach method definitions.

282 \medskip The syntax diagram below refers to some syntactic categories that

283 are further defined in @{cite "isabelle-isar-ref"}.

285 @{rail \<open>

286 @@{method match} kind @'in' (pattern '\<Rightarrow>' cartouche + '\<bar>')

287 ;

288 kind:

289 (@'conclusion' | @'premises' ('(' 'local' ')')? |

290 '(' term ')' | @{syntax thmrefs})

291 ;

292 pattern: fact_name? term args? \<newline> (@'for' fixes)?

293 ;

294 fact_name: @{syntax name} @{syntax attributes}? ':'

295 ;

296 args: '(' (('multi' | 'cut' nat?) + ',') ')'

297 \<close>}

299 Matching allows methods to introspect the goal state, and to implement more

300 explicit control flow. In the basic case, a term or fact @{text ts} is given

301 to match against as a \emph{match target}, along with a collection of

302 pattern-method pairs @{text "(p, m)"}: roughly speaking, when the pattern

303 @{text p} matches any member of @{text ts}, the \emph{inner} method @{text

304 m} will be executed.

305 \<close>

307 lemma

308 assumes X:

309 "Q \<longrightarrow> P"

310 "Q"

311 shows P

312 by (match X in I: "Q \<longrightarrow> P" and I': "Q" \<Rightarrow> \<open>insert mp [OF I I']\<close>)

314 text \<open>

315 In this example we have a structured Isar proof, with the named

316 assumption @{text "X"} and a conclusion @{term "P"}. With the match method

317 we can find the local facts @{term "Q \<longrightarrow> P"} and @{term "Q"}, binding them to

318 separately as @{text "I"} and @{text "I'"}. We then specialize the

319 modus-ponens rule @{thm mp [of Q P]} to these facts to solve the goal.

320 \<close>

323 section \<open>Subgoal focus\<close>

325 text\<open>

326 In the previous example we were able to match against an assumption out of

327 the Isar proof state. In general, however, proof subgoals can be

328 \emph{unstructured}, with goal parameters and premises arising from rule

329 application. To address this, @{method match} uses \emph{subgoal focusing}

330 (see also \autoref{s:design}) to produce structured goals out of

331 unstructured ones. In place of fact or term, we may give the

332 keyword @{keyword_def "premises"} as the match target. This causes a subgoal

333 focus on the first subgoal, lifting local goal parameters to fixed term

334 variables and premises into hypothetical theorems. The match is performed

335 against these theorems, naming them and binding them as appropriate.

336 Similarly giving the keyword @{keyword_def "conclusion"} matches against the

337 conclusion of the first subgoal.

339 An unstructured version of the previous example can then be similarly solved

340 through focusing.

341 \<close>

343 lemma "Q \<longrightarrow> P \<Longrightarrow> Q \<Longrightarrow> P"

344 by (match premises in

345 I: "Q \<longrightarrow> P" and I': "Q" \<Rightarrow> \<open>insert mp [OF I I']\<close>)

347 text \<open>

348 Match variables may be specified by giving a list of @{keyword_ref

349 "for"}-fixes after the pattern description. This marks those terms as bound

350 variables, which may be used in the method body.

351 \<close>

353 lemma "Q \<longrightarrow> P \<Longrightarrow> Q \<Longrightarrow> P"

354 by (match premises in I: "Q \<longrightarrow> A" and I': "Q" for A \<Rightarrow>

355 \<open>match conclusion in A \<Rightarrow> \<open>insert mp [OF I I']\<close>\<close>)

357 text \<open>

358 In this example @{term A} is a match variable which is bound to @{term P}

359 upon a successful match. The inner @{method match} then matches the

360 now-bound @{term A} (bound to @{term P}) against the conclusion (also @{term

361 P}), finally applying the specialized rule to solve the goal.

363 Schematic terms like @{text "?P"} may also be used to specify match

364 variables, but the result of the match is not bound, and thus cannot be used

365 in the inner method body.

367 \medskip In the following example we extract the predicate of an

368 existentially quantified conclusion in the current subgoal and search the

369 current premises for a matching fact. If both matches are successful, we

370 then instantiate the existential introduction rule with both the witness and

371 predicate, solving with the matched premise.

372 \<close>

374 method solve_ex =

375 (match conclusion in "\<exists>x. Q x" for Q \<Rightarrow>

376 \<open>match premises in U: "Q y" for y \<Rightarrow>

377 \<open>rule exI [where P = Q and x = y, OF U]\<close>\<close>)

379 text \<open>

380 The first @{method match} matches the pattern @{term "\<exists>x. Q x"} against the

381 current conclusion, binding the term @{term "Q"} in the inner match. Next

382 the pattern @{text "Q y"} is matched against all premises of the current

383 subgoal. In this case @{term "Q"} is fixed and @{term "y"} may be

384 instantiated. Once a match is found, the local fact @{text U} is bound to

385 the matching premise and the variable @{term "y"} is bound to the matching

386 witness. The existential introduction rule @{text "exI:"}~@{thm exI} is then

387 instantiated with @{term "y"} as the witness and @{term "Q"} as the

388 predicate, with its proof obligation solved by the local fact U (using the

389 Isar attribute @{attribute OF}). The following example is a trivial use of

390 this method.

391 \<close>

393 lemma "halts p \<Longrightarrow> \<exists>x. halts x"

394 by solve_ex

397 subsubsection \<open>Operating within a focus\<close>

399 text \<open>

400 Subgoal focusing provides a structured form of a subgoal, allowing for more

401 expressive introspection of the goal state. This requires some consideration

402 in order to be used effectively. When the keyword @{keyword "premises"} is

403 given as the match target, the premises of the subgoal are lifted into

404 hypothetical theorems, which can be found and named via match patterns.

405 Additionally these premises are stripped from the subgoal, leaving only the

406 conclusion. This renders them inaccessible to standard proof methods which

407 operate on the premises, such as @{method frule} or @{method erule}. Naive

408 usage of these methods within a match will most likely not function as the

409 method author intended.

410 \<close>

412 method my_allE_bad for y :: 'a =

413 (match premises in I: "\<forall>x :: 'a. ?Q x" \<Rightarrow>

414 \<open>erule allE [where x = y]\<close>)

416 text \<open>

417 Here we take a single parameter @{term y} and specialize the universal

418 elimination rule (@{thm allE}) to it, then attempt to apply this specialized

419 rule with @{method erule}. The method @{method erule} will attempt to unify

420 with a universal quantifier in the premises that matches the type of @{term

421 y}. Since @{keyword "premises"} causes a focus, however, there are no

422 subgoal premises to be found and thus @{method my_allE_bad} will always

423 fail. If focusing instead left the premises in place, using methods

424 like @{method erule} would lead to unintended behaviour, specifically during

425 backtracking. In our example, @{method erule} could choose an alternate

426 premise while backtracking, while leaving @{text I} bound to the original

427 match. In the case of more complex inner methods, where either @{text I} or

428 bound terms are used, this would almost certainly not be the intended

429 behaviour.

431 An alternative implementation would be to specialize the elimination rule to

432 the bound term and apply it directly.

433 \<close>

435 method my_allE_almost for y :: 'a =

436 (match premises in I: "\<forall>x :: 'a. ?Q x" \<Rightarrow>

437 \<open>rule allE [where x = y, OF I]\<close>)

439 lemma "\<forall>x. P x \<Longrightarrow> P y"

440 by (my_allE_almost y)

442 text \<open>

443 This method will insert a specialized duplicate of a universally quantified

444 premise. Although this will successfully apply in the presence of such a

445 premise, it is not likely the intended behaviour. Repeated application of

446 this method will produce an infinite stream of duplicate specialized

447 premises, due to the original premise never being removed. To address this,

448 matched premises may be declared with the @{attribute "thin"} attribute.

449 This will hide the premise from subsequent inner matches, and remove it from

450 the list of premises when the inner method has finished and the subgoal is

451 unfocused. It can be considered analogous to the existing @{text thin_tac}.

453 To complete our example, the correct implementation of the method

454 will @{attribute "thin"} the premise from the match and then apply it to the

455 specialized elimination rule.\<close>

457 method my_allE for y :: 'a =

458 (match premises in I [thin]: "\<forall>x :: 'a. ?Q x" \<Rightarrow>

459 \<open>rule allE [where x = y, OF I]\<close>)

461 lemma "\<forall>x. P x \<Longrightarrow> \<forall>x. Q x \<Longrightarrow> P y \<and> Q y"

462 by (my_allE y)+ (rule conjI)

465 subsection \<open>Attributes\<close>

467 text \<open>

468 Attributes may throw errors when applied to a given fact. For example, rule

469 instantiation will fail of there is a type mismatch or if a given variable

470 doesn't exist. Within a match or a method definition, it isn't generally

471 possible to guarantee that applied attributes won't fail. For example, in

472 the following method there is no guarantee that the two provided facts will

473 necessarily compose.

474 \<close>

476 method my_compose uses rule1 rule2 =

477 (rule rule1[OF rule2])

479 text \<open>

480 Some attributes (like @{attribute OF}) have been made partially

481 Eisbach-aware. This means that they are able to form a closure despite not

482 necessarily always being applicable. In the case of @{attribute OF}, it is

483 up to the proof author to guard attribute application with an appropriate

484 @{method match}, but there are still no static guarantees.

486 In contrast to @{attribute OF}, the @{attribute "where"} and @{attribute of}

487 attributes attempt to provide static guarantees that they will apply

488 whenever possible.

490 Within a match pattern for a fact, each outermost quantifier specifies the

491 requirement that a matching fact must have a schematic variable at that

492 point. This gives a corresponding name to this ``slot'' for the purposes of

493 forming a static closure, allowing the @{attribute "where"} attribute to

494 perform an instantiation at run-time.

495 \<close>

497 lemma

498 assumes A: "Q \<Longrightarrow> False"

499 shows "\<not> Q"

500 by (match intros in X: "\<And>P. (P \<Longrightarrow> False) \<Longrightarrow> \<not> P" \<Rightarrow>

501 \<open>rule X [where P = Q, OF A]\<close>)

503 text \<open>

504 Subgoal focusing converts the outermost quantifiers of premises into

505 schematics when lifting them to hypothetical facts. This allows us to

506 instantiate them with @{attribute "where"} when using an appropriate match

507 pattern.

508 \<close>

510 lemma "(\<And>x :: 'a. A x \<Longrightarrow> B x) \<Longrightarrow> A y \<Longrightarrow> B y"

511 by (match premises in I: "\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x" \<Rightarrow>

512 \<open>rule I [where x = y]\<close>)

514 text \<open>

515 The @{attribute of} attribute behaves similarly. It is worth noting,

516 however, that the positional instantiation of @{attribute of} occurs against

517 the position of the variables as they are declared \emph{in the match

518 pattern}.

519 \<close>

521 lemma

522 fixes A B and x :: 'a and y :: 'b

523 assumes asm: "(\<And>x y. A y x \<Longrightarrow> B x y )"

524 shows "A y x \<Longrightarrow> B x y"

525 by (match asm in I: "\<And>(x :: 'a) (y :: 'b). ?P x y \<Longrightarrow> ?Q x y" \<Rightarrow>

526 \<open>rule I [of x y]\<close>)

528 text \<open>

529 In this example, the order of schematics in @{text asm} is actually @{text

530 "?y ?x"}, but we instantiate our matched rule in the opposite order. This is

531 because the effective rule @{term I} was bound from the match, which

532 declared the @{typ 'a} slot first and the @{typ 'b} slot second.

534 To get the dynamic behaviour of @{attribute of} we can choose to invoke it

535 \emph{unchecked}. This avoids trying to do any type inference for the

536 provided parameters, instead storing them as their most general type and

537 doing type matching at run-time. This, like @{attribute OF}, will throw

538 errors if the expected slots don't exist or there is a type mismatch.

539 \<close>

541 lemma

542 fixes A B and x :: 'a and y :: 'b

543 assumes asm: "\<And>x y. A y x \<Longrightarrow> B x y"

544 shows "A y x \<Longrightarrow> B x y"

545 by (match asm in I: "PROP ?P" \<Rightarrow> \<open>rule I [of (unchecked) y x]\<close>)

547 text \<open>

548 Attributes may be applied to matched facts directly as they are matched. Any

549 declarations will therefore be applied in the context of the inner method,

550 as well as any transformations to the rule.

551 \<close>

553 lemma "(\<And>x :: 'a. A x \<Longrightarrow> B x) \<Longrightarrow> A y \<longrightarrow> B y"

554 by (match premises in I[of y, intros]: "\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x" \<Rightarrow>

555 \<open>prop_solver\<close>)

557 text \<open>

558 In this example, the pattern @{text "\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x"} matches against

559 the only premise, giving an appropriately typed slot for @{term y}. After

560 the match, the resulting rule is instantiated to @{term y} and then declared

561 as an @{attribute intros} rule. This is then picked up by @{method

562 prop_solver} to solve the goal.

563 \<close>

566 section \<open>Multi-match \label{sec:multi}\<close>

568 text \<open>

569 In all previous examples, @{method match} was only ever searching for a

570 single rule or premise. Each local fact would therefore always have a length

571 of exactly one. We may, however, wish to find \emph{all} matching results.

572 To achieve this, we can simply mark a given pattern with the @{text

573 "(multi)"} argument.

574 \<close>

576 lemma

577 assumes asms: "A \<Longrightarrow> B" "A \<Longrightarrow> D"

578 shows "(A \<longrightarrow> B) \<and> (A \<longrightarrow> D)"

579 apply (match asms in I[intros]: "?P \<Longrightarrow> ?Q" \<Rightarrow> \<open>solves \<open>prop_solver\<close>\<close>)?

580 by (match asms in I[intros]: "?P \<Longrightarrow> ?Q" (multi) \<Rightarrow> \<open>prop_solver\<close>)

582 text \<open>

583 In the first @{method match}, without the @{text "(multi)"} argument, @{term

584 I} is only ever be bound to one of the members of @{text asms}. This

585 backtracks over both possibilities (see next section), however neither

586 assumption in isolation is sufficient to solve to goal. The use of the

587 @{method solves} combinator ensures that @{method prop_solver} has no effect

588 on the goal when it doesn't solve it, and so the first match leaves the goal

589 unchanged. In the second @{method match}, @{text I} is bound to all of

590 @{text asms}, declaring both results as @{text intros}. With these rules

591 @{method prop_solver} is capable of solving the goal.

593 Using for-fixed variables in patterns imposes additional constraints on the

594 results. In all previous examples, the choice of using @{text ?P} or a

595 for-fixed @{term P} only depended on whether or not @{term P} was mentioned

596 in another pattern or the inner method. When using a multi-match, however,

597 all for-fixed terms must agree in the results.

598 \<close>

600 lemma

601 assumes asms: "A \<Longrightarrow> B" "A \<Longrightarrow> D" "D \<Longrightarrow> B"

602 shows "(A \<longrightarrow> B) \<and> (A \<longrightarrow> D)"

603 apply (match asms in I[intros]: "?P \<Longrightarrow> Q" (multi) for Q \<Rightarrow>

604 \<open>solves \<open>prop_solver\<close>\<close>)?

605 by (match asms in I[intros]: "P \<Longrightarrow> ?Q" (multi) for P \<Rightarrow>

606 \<open>prop_solver\<close>)

608 text \<open>

609 Here we have two seemingly-equivalent applications of @{method match},

610 however only the second one is capable of solving the goal. The first

611 @{method match} selects the first and third members of @{text asms} (those

612 that agree on their conclusion), which is not sufficient. The second

613 @{method match} selects the first and second members of @{text asms} (those

614 that agree on their assumption), which is enough for @{method prop_solver}

615 to solve the goal.

616 \<close>

619 section \<open>Dummy patterns\<close>

621 text \<open>

622 Dummy patterns may be given as placeholders for unique schematics in

623 patterns. They implicitly receive all currently bound variables as

624 arguments, and are coerced into the @{typ prop} type whenever possible. For

625 example, the trivial dummy pattern @{text "_"} will match any proposition.

626 In contrast, by default the pattern @{text "?P"} is considered to have type

627 @{typ bool}. It will not bind anything with meta-logical connectives (e.g.

628 @{text "_ \<Longrightarrow> _"} or @{text "_ &&& _"}).

629 \<close>

631 lemma

632 assumes asms: "A &&& B \<Longrightarrow> D"

633 shows "(A \<and> B \<longrightarrow> D)"

634 by (match asms in I:_ \<Rightarrow> \<open>prop_solver intros: I conjunctionI\<close>)

637 section \<open>Backtracking\<close>

639 text \<open>

640 Patterns are considered top-down, executing the inner method @{text m} of

641 the first pattern which is satisfied by the current match target. By

642 default, matching performs extensive backtracking by attempting all valid

643 variable and fact bindings according to the given pattern. In particular,

644 all unifiers for a given pattern will be explored, as well as each matching

645 fact. The inner method @{text m} will be re-executed for each different

646 variable/fact binding during backtracking. A successful match is considered

647 a cut-point for backtracking. Specifically, once a match is made no other

648 pattern-method pairs will be considered.

650 The method @{text foo} below fails for all goals that are conjunctions. Any

651 such goal will match the first pattern, causing the second pattern (that

652 would otherwise match all goals) to never be considered. If multiple

653 unifiers exist for the pattern @{text "?P \<and> ?Q"} against the current goal,

654 then the failing method @{method fail} will be (uselessly) tried for all of

655 them.

656 \<close>

658 method foo =

659 (match conclusion in "?P \<and> ?Q" \<Rightarrow> \<open>fail\<close> \<bar> "?R" \<Rightarrow> \<open>prop_solver\<close>)

661 text \<open>

662 This behaviour is in direct contrast to the backtracking done by Coq's Ltac,

663 which will attempt all patterns in a match before failing. This means that

664 the failure of an inner method that is executed after a successful match

665 does not, in Ltac, cause the entire match to fail, whereas it does in

666 Eisbach. In Eisbach the distinction is important due to the pervasive use of

667 backtracking. When a method is used in a combinator chain, its failure

668 becomes significant because it signals previously applied methods to move to

669 the next result. Therefore, it is necessary for @{method match} to not mask

670 such failure. One can always rewrite a match using the combinators ``@{text

671 "?"}'' and ``@{text "|"}'' to try subsequent patterns in the case of an

672 inner-method failure. The following proof method, for example, always

673 invokes @{method prop_solver} for all goals because its first alternative

674 either never matches or (if it does match) always fails.

675 \<close>

677 method foo\<^sub>1 =

678 (match conclusion in "?P \<and> ?Q" \<Rightarrow> \<open>fail\<close>) |

679 (match conclusion in "?R" \<Rightarrow> \<open>prop_solver\<close>)

682 subsection \<open>Cut\<close>

684 text \<open>

685 Backtracking may be controlled more precisely by marking individual patterns

686 as \emph{cut}. This causes backtracking to not progress beyond this pattern:

687 once a match is found no others will be considered.

688 \<close>

690 method foo\<^sub>2 =

691 (match premises in I: "P \<and> Q" (cut) and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow>

692 \<open>rule mp [OF I' I [THEN conjunct1]]\<close>)

694 text \<open>

695 In this example, once a conjunction is found (@{term "P \<and> Q"}), all possible

696 implications of @{term "P"} in the premises are considered, evaluating the

697 inner @{method rule} with each consequent. No other conjunctions will be

698 considered, with method failure occurring once all implications of the

699 form @{text "P \<longrightarrow> ?U"} have been explored. Here the left-right processing of

700 individual patterns is important, as all patterns after of the cut will

701 maintain their usual backtracking behaviour.

702 \<close>

704 lemma "A \<and> B \<Longrightarrow> A \<longrightarrow> D \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> C"

705 by foo\<^sub>2

707 lemma "C \<and> D \<Longrightarrow> A \<and> B \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> C"

708 by (foo\<^sub>2 | prop_solver)

710 text \<open>

711 In this example, the first lemma is solved by @{text foo\<^sub>2}, by first

712 picking @{term "A \<longrightarrow> D"} for @{text I'}, then backtracking and ultimately

713 succeeding after picking @{term "A \<longrightarrow> C"}. In the second lemma, however,

714 @{term "C \<and> D"} is matched first, the second pattern in the match cannot be

715 found and so the method fails, falling through to @{method prop_solver}.

716 \<close>

719 subsection \<open>Multi-match revisited\<close>

721 text \<open>

722 A multi-match will produce a sequence of potential bindings for for-fixed

723 variables, where each binding environment is the result of matching against

724 at least one element from the match target. For each environment, the match

725 result will be all elements of the match target which agree with the pattern

726 under that environment. This can result in unexpected behaviour when giving

727 very general patterns.

728 \<close>

730 lemma

731 assumes asms: "\<And>x. A x \<and> B x" "\<And>y. A y \<and> C y" "\<And>z. B z \<and> C z"

732 shows "A x \<and> C x"

733 by (match asms in I: "\<And>x. P x \<and> ?Q x" (multi) for P \<Rightarrow>

734 \<open>match (P) in "A" \<Rightarrow> \<open>fail\<close>

735 \<bar> _ \<Rightarrow> \<open>match I in "\<And>x. A x \<and> B x" \<Rightarrow> \<open>fail\<close>

736 \<bar> _ \<Rightarrow> \<open>rule I\<close>\<close>\<close>)

738 text \<open>

739 Intuitively it seems like this proof should fail to check. The first match

740 result, which binds @{term I} to the first two members of @{text asms},

741 fails the second inner match due to binding @{term P} to @{term A}.

742 Backtracking then attempts to bind @{term I} to the third member of @{text

743 asms}. This passes all inner matches, but fails when @{method rule} cannot

744 successfully apply this to the current goal. After this, a valid match that

745 is produced by the unifier is one which binds @{term P} to simply @{text

746 "\<lambda>a. A ?x"}. The first inner match succeeds because @{text "\<lambda>a. A ?x"} does

747 not match @{term A}. The next inner match succeeds because @{term I} has

748 only been bound to the first member of @{text asms}. This is due to @{method

749 match} considering @{text "\<lambda>a. A ?x"} and @{text "\<lambda>a. A ?y"} as distinct

750 terms.

752 The simplest way to address this is to explicitly disallow term bindings

753 which we would consider invalid.

754 \<close>

756 method abs_used for P =

757 (match (P) in "\<lambda>a. ?P" \<Rightarrow> \<open>fail\<close> \<bar> _ \<Rightarrow> \<open>-\<close>)

759 text \<open>

760 This method has no effect on the goal state, but instead serves as a filter

761 on the environment produced from match.

762 \<close>

765 section \<open>Uncurrying\<close>

767 text \<open>

768 The @{method match} method is not aware of the logical content of match

769 targets. Each pattern is simply matched against the shallow structure of a

770 fact or term. Most facts are in \emph{normal form}, which curries premises

771 via meta-implication @{text "_ \<Longrightarrow> _"}.

772 \<close>

774 lemma

775 assumes asms: "D \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> A"

776 shows "D \<Longrightarrow> B \<Longrightarrow> C \<and> A"

777 by (match asms in H:"D \<Longrightarrow> _" (multi) \<Rightarrow> \<open>prop_solver elims: H\<close>)

779 text \<open>

780 For the first member of @{text asms} the dummy pattern successfully matches

781 against @{term "B \<Longrightarrow> C"} and so the proof is successful.

782 \<close>

784 lemma

785 assumes asms: "A \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> C"

786 shows "D \<or> (A \<and> B) \<Longrightarrow> C"

787 apply (match asms in H:"_ \<Longrightarrow> C" (multi) \<Rightarrow> \<open>prop_solver elims: H\<close>)(*<*)?

788 by (prop_solver elims: asms)(*>*)

790 text \<open>

791 This proof will fail to solve the goal. Our match pattern will only match

792 rules which have a single premise, and conclusion @{term C}, so the first

793 member of @{text asms} is not bound and thus the proof fails. Matching a

794 pattern of the form @{term "P \<Longrightarrow> Q"} against this fact will bind @{term "P"}

795 to @{term "A"} and @{term Q} to @{term "B \<Longrightarrow> C"}. Our pattern, with a

796 concrete @{term "C"} in the conclusion, will fail to match this fact.

798 To express our desired match, we may \emph{uncurry} our rules before

799 matching against them. This forms a meta-conjunction of all premises in a

800 fact, so that only one implication remains. For example the uncurried

801 version of @{term "A \<Longrightarrow> B \<Longrightarrow> C"} is @{term "A &&& B \<Longrightarrow> C"}. This will now match

802 our desired pattern @{text "_ \<Longrightarrow> C"}, and can be \emph{curried} after the

803 match to put it back into normal form.

804 \<close>

806 lemma

807 assumes asms: "A \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> C"

808 shows "D \<or> (A \<and> B) \<Longrightarrow> C"

809 by (match asms[uncurry] in H[curry]:"_ \<Longrightarrow> C" (multi) \<Rightarrow>

810 \<open>prop_solver elims: H\<close>)

813 section \<open>Reverse matching\<close>

815 text \<open>

816 The @{method match} method only attempts to perform matching of the pattern

817 against the match target. Specifically this means that it will not

818 instantiate schematic terms in the match target.

819 \<close>

821 lemma

822 assumes asms: "\<And>x :: 'a. A x"

823 shows "A y"

824 apply (match asms in H:"A y" \<Rightarrow> \<open>rule H\<close>)?

825 by (match asms in H:"P" for P \<Rightarrow>

826 \<open>match ("A y") in "P" \<Rightarrow> \<open>rule H\<close>\<close>)

828 text \<open>

829 In the first @{method match} we attempt to find a member of @{text asms}

830 which matches our goal precisely. This fails due to no such member existing.

831 The second match reverses the role of the fact in the match, by first giving

832 a general pattern @{term P}. This bound pattern is then matched against

833 @{term "A y"}. In this case, @{term P} is bound to @{text "A ?x"} and so it

834 successfully matches.

835 \<close>

838 section \<open>Type matching\<close>

840 text \<open>

841 The rule instantiation attributes @{attribute "where"} and @{attribute "of"}

842 attempt to guarantee type-correctness wherever possible. This can require

843 additional invocations of @{method match} in order to statically ensure that

844 instantiation will succeed.

845 \<close>

847 lemma

848 assumes asms: "\<And>x :: 'a. A x"

849 shows "A y"

850 by (match asms in H:"\<And>z :: 'b. P z" for P \<Rightarrow>

851 \<open>match (y) in "y :: 'b" for y \<Rightarrow> \<open>rule H[where z=y]\<close>\<close>)

853 text \<open>

854 In this example the type @{text 'b} is matched to @{text 'a}, however

855 statically they are formally distinct types. The first match binds @{text

856 'b} while the inner match serves to coerce @{term y} into having the type

857 @{text 'b}. This allows the rule instantiation to successfully apply.

858 \<close>

861 chapter \<open>Method development\<close>

863 section \<open>Tracing methods\<close>

865 text \<open>

866 Method tracing is supported by auxiliary print methods provided by @{theory

867 Eisbach_Tools}. These include @{method print_fact}, @{method print_term} and

868 @{method print_type}. Whenever a print method is evaluated it leaves the

869 goal unchanged and writes its argument as tracing output.

871 Print methods can be combined with the @{method fail} method to investigate

872 the backtracking behaviour of a method.

873 \<close>

875 lemma

876 assumes asms: A B C D

877 shows D

878 apply (match asms in H:_ \<Rightarrow> \<open>print_fact H, fail\<close>)(*<*)?

879 by (simp add: asms)(*>*)

881 text \<open>

882 This proof will fail, but the tracing output will show the order that the

883 assumptions are attempted.

884 \<close>

887 section \<open>Integrating with Isabelle/ML\<close>

889 subsection \<open>Attributes\<close>

891 text \<open>

892 A custom rule attribute is a simple way to extend the functionality of

893 Eisbach methods. The dummy rule attribute notation (@{text "[[ _ ]]"})

894 invokes the given attribute against a dummy fact and evaluates to the result

895 of that attribute. When used as a match target, this can serve as an

896 effective auxiliary function.

897 \<close>

899 attribute_setup get_split_rule =

900 \<open>Args.term >> (fn t =>

901 Thm.rule_attribute (fn context => fn _ =>

902 (case get_split_rule (Context.proof_of context) t of

903 SOME thm => thm

904 | NONE => Drule.dummy_thm)))\<close>

906 text \<open>

907 In this example, the new attribute @{attribute get_split_rule} lifts the ML

908 function of the same name into an attribute. When applied to a cast

909 distinction over a datatype, it retrieves its corresponding split rule.

911 We can then integrate this intro a method that applies the split rule, fist

912 matching to ensure that fetching the rule was successful.

913 \<close>

915 method splits =

916 (match conclusion in "?P f" for f \<Rightarrow>

917 \<open>match [[get_split_rule f]] in U: "(_ :: bool) = _" \<Rightarrow>

918 \<open>rule U[THEN iffD2]\<close>\<close>)

920 lemma "L \<noteq> [] \<Longrightarrow> case L of [] \<Rightarrow> False | _ \<Rightarrow> True"

921 by (splits, prop_solver intros: allI)

923 end