1(*:maxLineLen=78:*) 2 3theory Manual 4imports Base "HOL-Eisbach.Eisbach_Tools" 5begin 6 7chapter \<open>The method command\<close> 8 9text \<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. 15 16 \<^medskip> 17 The syntax diagram below refers to some syntactic categories that are 18 further defined in @{cite "isabelle-isar-ref"}. 19 20 @{rail \<open> 21 @@{command method} name args @'=' method 22 ; 23 args: term_args? method_args? \<newline> fact_args? decl_args? 24 ; 25 term_args: @'for' @{syntax "fixes"} 26 ; 27 method_args: @'methods' (name+) 28 ; 29 fact_args: @'uses' (name+) 30 ; 31 decl_args: @'declares' (name+) 32 \<close>} 33\<close> 34 35 36section \<open>Basic method definitions\<close> 37 38text \<open> 39 Consider the following proof that makes use of usual Isar method 40 combinators. 41\<close> 42 43 lemma "P \<and> Q \<longrightarrow> P" 44 by ((rule impI, (erule conjE)?) | assumption)+ 45 46text \<open> 47 It is clear that this compound method will be applicable in more cases than 48 this proof alone. With the @{command method} command we can define a proof 49 method that makes the above functionality available generally. 50\<close> 51 52 method prop_solver\<^sub>1 = 53 ((rule impI, (erule conjE)?) | assumption)+ 54 55 lemma "P \<and> Q \<and> R \<longrightarrow> P" 56 by prop_solver\<^sub>1 57 58text \<open> 59 In this example, the facts \<open>impI\<close> and \<open>conjE\<close> are static. They are evaluated 60 once when the method is defined and cannot be changed later. This makes the 61 method stable in the sense of \<^emph>\<open>static scoping\<close>: naming another fact \<open>impI\<close> 62 in a later context won't affect the behaviour of \<open>prop_solver\<^sub>1\<close>. 63\<close> 64 65 66section \<open>Term abstraction\<close> 67 68text \<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 \<open>intro_ex\<close> takes a term @{term y} of any type, which it uses to 72 instantiate the @{term x}-variable of \<open>exI\<close> (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> 78 79 method intro_ex for Q :: "'a \<Rightarrow> bool" and y :: 'a = 80 (rule exI ["where" P = Q and x = y]) 81 82 83text \<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> 92 93 lemma "P a \<Longrightarrow> \<exists>x. P x" 94 by (intro_ex P a) 95 96 97section \<open>Fact abstraction\<close> 98 99subsection \<open>Named theorems\<close> 100 101text \<open> 102 A \<^emph>\<open>named theorem\<close> is a fact whose contents are produced dynamically within 103 the current proof context. The Isar command @{command_ref "named_theorems"} 104 provides simple access to this concept: it declares a dynamic fact with 105 corresponding \<^emph>\<open>attribute\<close> for managing this particular data slot in the 106 context. 107\<close> 108 109 named_theorems intros 110 111text \<open> 112 So far \<open>intros\<close> refers to the empty fact. Using the Isar command 113 @{command_ref "declare"} we may apply declaration attributes to the context. 114 Below we declare both \<open>conjI\<close> and \<open>impI\<close> as \<open>intros\<close>, adding them to the 115 named theorem slot. 116\<close> 117 118 declare conjI [intros] and impI [intros] 119 120text \<open> 121 We can refer to named theorems as dynamic facts within a particular proof 122 context, which are evaluated whenever the method is invoked. Instead of 123 having facts hard-coded into the method, as in \<open>prop_solver\<^sub>1\<close>, we can 124 instead refer to these named theorems. 125\<close> 126 127 named_theorems elims 128 declare conjE [elims] 129 130 method prop_solver\<^sub>3 = 131 ((rule intros, (erule elims)?) | assumption)+ 132 133 lemma "P \<and> Q \<longrightarrow> P" 134 by prop_solver\<^sub>3 135 136text \<open> 137 Often these named theorems need to be augmented on the spot, when a method 138 is invoked. The @{keyword_def "declares"} keyword in the signature of 139 @{command method} adds the common method syntax \<open>method decl: facts\<close> for 140 each named theorem \<open>decl\<close>. 141\<close> 142 143 method prop_solver\<^sub>4 declares intros elims = 144 ((rule intros, (erule elims)?) | assumption)+ 145 146 lemma "P \<and> (P \<longrightarrow> Q) \<longrightarrow> Q \<and> P" 147 by (prop_solver\<^sub>4 elims: impE intros: conjI) 148 149 150subsection \<open>Simple fact abstraction\<close> 151 152text \<open> 153 The @{keyword "declares"} keyword requires that a corresponding dynamic fact 154 has been declared with @{command_ref named_theorems}. This is useful for 155 managing collections of facts which are to be augmented with declarations, 156 but is overkill if we simply want to pass a fact to a method. 157 158 We may use the @{keyword_def "uses"} keyword in the method header to provide 159 a simple fact parameter. In contrast to @{keyword "declares"}, these facts 160 are always implicitly empty unless augmented when the method is invoked. 161\<close> 162 163 method rule_twice uses my_rule = 164 (rule my_rule, rule my_rule) 165 166 lemma "P \<Longrightarrow> Q \<Longrightarrow> (P \<and> Q) \<and> Q" 167 by (rule_twice my_rule: conjI) 168 169 170section \<open>Higher-order methods\<close> 171 172text \<open> 173 The \<^emph>\<open>structured concatenation\<close> combinator ``\<open>method\<^sub>1 ; method\<^sub>2\<close>'' was 174 introduced in Isabelle2015, motivated by development of Eisbach. It is 175 similar to ``\<open>method\<^sub>1, method\<^sub>2\<close>'', but \<open>method\<^sub>2\<close> is invoked on on \<^emph>\<open>all\<close> 176 subgoals that have newly emerged from \<open>method\<^sub>1\<close>. This is useful to handle 177 cases where the number of subgoals produced by a method is determined 178 dynamically at run-time. 179\<close> 180 181 method conj_with uses rule = 182 (intro conjI ; intro rule) 183 184 lemma 185 assumes A: "P" 186 shows "P \<and> P \<and> P" 187 by (conj_with rule: A) 188 189text \<open> 190 Method definitions may take other methods as arguments, and thus implement 191 method combinators with prefix syntax. For example, to more usefully exploit 192 Isabelle's backtracking, the explicit requirement that a method solve all 193 produced subgoals is frequently useful. This can easily be written as a 194 \<^emph>\<open>higher-order method\<close> using ``\<open>;\<close>''. The @{keyword "methods"} keyword 195 denotes method parameters that are other proof methods to be invoked by the 196 method being defined. 197\<close> 198 199 method solve methods m = (m ; fail) 200 201text \<open> 202 Given some method-argument \<open>m\<close>, \<open>solve \<open>m\<close>\<close> applies the method \<open>m\<close> and then 203 fails whenever \<open>m\<close> produces any new unsolved subgoals --- i.e. when \<open>m\<close> 204 fails to completely discharge the goal it was applied to. 205\<close> 206 207 208section \<open>Example\<close> 209 210text \<open> 211 With these simple features we are ready to write our first non-trivial proof 212 method. Returning to the first-order logic example, the following method 213 definition applies various rules with their canonical methods. 214\<close> 215 216 named_theorems subst 217 218 method prop_solver declares intros elims subst = 219 (assumption | 220 (rule intros) | erule elims | 221 subst subst | subst (asm) subst | 222 (erule notE ; solve \<open>prop_solver\<close>))+ 223 224text \<open> 225 The only non-trivial part above is the final alternative \<open>(erule notE ; 226 solve \<open>prop_solver\<close>)\<close>. Here, in the case that all other alternatives fail, 227 the method takes one of the assumptions @{term "\<not> P"} of the current goal 228 and eliminates it with the rule \<open>notE\<close>, causing the goal to be proved to 229 become @{term P}. The method then recursively invokes itself on the 230 remaining goals. The job of the recursive call is to demonstrate that there 231 is a contradiction in the original assumptions (i.e.\ that @{term P} can be 232 derived from them). Note this recursive invocation is applied with the 233 @{method solve} method combinator to ensure that a contradiction will indeed 234 be shown. In the case where a contradiction cannot be found, backtracking 235 will occur and a different assumption @{term "\<not> Q"} will be chosen for 236 elimination. 237 238 Note that the recursive call to @{method prop_solver} does not have any 239 parameters passed to it. Recall that fact parameters, e.g.\ \<open>intros\<close>, 240 \<open>elims\<close>, and \<open>subst\<close>, are managed by declarations in the current proof 241 context. They will therefore be passed to any recursive call to @{method 242 prop_solver} and, more generally, any invocation of a method which declares 243 these named theorems. 244 245 \<^medskip> 246 After declaring some standard rules to the context, the @{method 247 prop_solver} becomes capable of solving non-trivial propositional 248 tautologies. 249\<close> 250 251 lemmas [intros] = 252 conjI \<comment> \<open>@{thm conjI}\<close> 253 impI \<comment> \<open>@{thm impI}\<close> 254 disjCI \<comment> \<open>@{thm disjCI}\<close> 255 iffI \<comment> \<open>@{thm iffI}\<close> 256 notI \<comment> \<open>@{thm notI}\<close> 257 258 lemmas [elims] = 259 impCE \<comment> \<open>@{thm impCE}\<close> 260 conjE \<comment> \<open>@{thm conjE}\<close> 261 disjE \<comment> \<open>@{thm disjE}\<close> 262 263 lemma "(A \<or> B) \<and> (A \<longrightarrow> C) \<and> (B \<longrightarrow> C) \<longrightarrow> C" 264 by prop_solver 265 266 267chapter \<open>The match method \label{s:matching}\<close> 268 269text \<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. 275 276 To address this, we introduce the @{method_def match} method, which provides 277 more direct access to the higher-order matching facility at the core of 278 Isabelle. It is implemented as a separate proof method (in Isabelle/ML), and 279 thus can be directly applied to proofs, however it is most useful when 280 applied in the context of writing Eisbach method definitions. 281 282 \<^medskip> 283 The syntax diagram below refers to some syntactic categories that are 284 further defined in @{cite "isabelle-isar-ref"}. 285 286 @{rail \<open> 287 @@{method match} kind @'in' (pattern '\<Rightarrow>' @{syntax text} + '\<bar>') 288 ; 289 kind: 290 (@'conclusion' | @'premises' ('(' 'local' ')')? | 291 '(' term ')' | @{syntax thms}) 292 ; 293 pattern: fact_name? term args? \<newline> (@'for' fixes)? 294 ; 295 fact_name: @{syntax name} @{syntax attributes}? ':' 296 ; 297 args: '(' (('multi' | 'cut' nat?) + ',') ')' 298 \<close>} 299 300 Matching allows methods to introspect the goal state, and to implement more 301 explicit control flow. In the basic case, a term or fact \<open>ts\<close> is given to 302 match against as a \<^emph>\<open>match target\<close>, along with a collection of 303 pattern-method pairs \<open>(p, m)\<close>: roughly speaking, when the pattern \<open>p\<close> 304 matches any member of \<open>ts\<close>, the \<^emph>\<open>inner\<close> method \<open>m\<close> will be executed. 305\<close> 306 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>) 313 314text \<open> 315 In this example we have a structured Isar proof, with the named assumption 316 \<open>X\<close> and a conclusion @{term "P"}. With the match method we can find the 317 local facts @{term "Q \<longrightarrow> P"} and @{term "Q"}, binding them to separately as 318 \<open>I\<close> and \<open>I'\<close>. We then specialize the modus-ponens rule @{thm mp [of Q P]} to 319 these facts to solve the goal. 320\<close> 321 322 323section \<open>Subgoal focus\<close> 324 325text\<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>\<open>unstructured\<close>, with goal parameters and premises arising from rule 329 application. To address this, @{method match} uses \<^emph>\<open>subgoal focusing\<close> to 330 produce structured goals out of unstructured ones. In place of fact or term, 331 we may give the keyword @{keyword_def "premises"} as the match target. This 332 causes a subgoal focus on the first subgoal, lifting local goal parameters 333 to fixed term variables and premises into hypothetical theorems. The match 334 is performed against these theorems, naming them and binding them as 335 appropriate. Similarly giving the keyword @{keyword_def "conclusion"} 336 matches against the conclusion of the first subgoal. 337 338 An unstructured version of the previous example can then be similarly solved 339 through focusing. 340\<close> 341 342 lemma "Q \<longrightarrow> P \<Longrightarrow> Q \<Longrightarrow> P" 343 by (match premises in 344 I: "Q \<longrightarrow> P" and I': "Q" \<Rightarrow> \<open>insert mp [OF I I']\<close>) 345 346text \<open> 347 Match variables may be specified by giving a list of @{keyword_ref 348 "for"}-fixes after the pattern description. This marks those terms as bound 349 variables, which may be used in the method body. 350\<close> 351 352 lemma "Q \<longrightarrow> P \<Longrightarrow> Q \<Longrightarrow> P" 353 by (match premises in I: "Q \<longrightarrow> A" and I': "Q" for A \<Rightarrow> 354 \<open>match conclusion in A \<Rightarrow> \<open>insert mp [OF I I']\<close>\<close>) 355 356text \<open> 357 In this example @{term A} is a match variable which is bound to @{term P} 358 upon a successful match. The inner @{method match} then matches the 359 now-bound @{term A} (bound to @{term P}) against the conclusion (also @{term 360 P}), finally applying the specialized rule to solve the goal. 361 362 Schematic terms like \<open>?P\<close> may also be used to specify match variables, but 363 the result of the match is not bound, and thus cannot be used in the inner 364 method body. 365 366 \<^medskip> 367 In the following example we extract the predicate of an existentially 368 quantified conclusion in the current subgoal and search the current premises 369 for a matching fact. If both matches are successful, we then instantiate the 370 existential introduction rule with both the witness and predicate, solving 371 with the matched premise. 372\<close> 373 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>) 378 379text \<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 \<open>Q y\<close> is matched against all premises of the current subgoal. In 383 this case @{term "Q"} is fixed and @{term "y"} may be instantiated. Once a 384 match is found, the local fact \<open>U\<close> is bound to the matching premise and the 385 variable @{term "y"} is bound to the matching witness. The existential 386 introduction rule \<open>exI:\<close>~@{thm exI} is then instantiated with @{term "y"} as 387 the witness and @{term "Q"} as the predicate, with its proof obligation 388 solved by the local fact U (using the Isar attribute @{attribute OF}). The 389 following example is a trivial use of this method. 390\<close> 391 392 lemma "halts p \<Longrightarrow> \<exists>x. halts x" 393 by solve_ex 394 395 396subsection \<open>Operating within a focus\<close> 397 398text \<open> 399 Subgoal focusing provides a structured form of a subgoal, allowing for more 400 expressive introspection of the goal state. This requires some consideration 401 in order to be used effectively. When the keyword @{keyword "premises"} is 402 given as the match target, the premises of the subgoal are lifted into 403 hypothetical theorems, which can be found and named via match patterns. 404 Additionally these premises are stripped from the subgoal, leaving only the 405 conclusion. This renders them inaccessible to standard proof methods which 406 operate on the premises, such as @{method frule} or @{method erule}. Naive 407 usage of these methods within a match will most likely not function as the 408 method author intended. 409\<close> 410 411 method my_allE_bad for y :: 'a = 412 (match premises in I: "\<forall>x :: 'a. ?Q x" \<Rightarrow> 413 \<open>erule allE [where x = y]\<close>) 414 415text \<open> 416 Here we take a single parameter @{term y} and specialize the universal 417 elimination rule (@{thm allE}) to it, then attempt to apply this specialized 418 rule with @{method erule}. The method @{method erule} will attempt to unify 419 with a universal quantifier in the premises that matches the type of @{term 420 y}. Since @{keyword "premises"} causes a focus, however, there are no 421 subgoal premises to be found and thus @{method my_allE_bad} will always 422 fail. If focusing instead left the premises in place, using methods like 423 @{method erule} would lead to unintended behaviour, specifically during 424 backtracking. In our example, @{method erule} could choose an alternate 425 premise while backtracking, while leaving \<open>I\<close> bound to the original match. 426 In the case of more complex inner methods, where either \<open>I\<close> or bound terms 427 are used, this would almost certainly not be the intended behaviour. 428 429 An alternative implementation would be to specialize the elimination rule to 430 the bound term and apply it directly. 431\<close> 432 433 method my_allE_almost for y :: 'a = 434 (match premises in I: "\<forall>x :: 'a. ?Q x" \<Rightarrow> 435 \<open>rule allE [where x = y, OF I]\<close>) 436 437 lemma "\<forall>x. P x \<Longrightarrow> P y" 438 by (my_allE_almost y) 439 440text \<open> 441 This method will insert a specialized duplicate of a universally quantified 442 premise. Although this will successfully apply in the presence of such a 443 premise, it is not likely the intended behaviour. Repeated application of 444 this method will produce an infinite stream of duplicate specialized 445 premises, due to the original premise never being removed. To address this, 446 matched premises may be declared with the @{attribute thin} attribute. This 447 will hide the premise from subsequent inner matches, and remove it from the 448 list of premises when the inner method has finished and the subgoal is 449 unfocused. It can be considered analogous to the existing \<open>thin_tac\<close>. 450 451 To complete our example, the correct implementation of the method will 452 @{attribute thin} the premise from the match and then apply it to the 453 specialized elimination rule.\<close> 454 455 method my_allE for y :: 'a = 456 (match premises in I [thin]: "\<forall>x :: 'a. ?Q x" \<Rightarrow> 457 \<open>rule allE [where x = y, OF I]\<close>) 458 459 lemma "\<forall>x. P x \<Longrightarrow> \<forall>x. Q x \<Longrightarrow> P y \<and> Q y" 460 by (my_allE y)+ (rule conjI) 461 462 463subsubsection \<open>Inner focusing\<close> 464 465text \<open> 466 Premises are \<^emph>\<open>accumulated\<close> for the purposes of subgoal focusing. In 467 contrast to using standard methods like @{method frule} within focused 468 match, another @{method match} will have access to all the premises of the 469 outer focus. 470\<close> 471 472 lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B" 473 by (match premises in H: A \<Rightarrow> \<open>intro conjI, rule H, 474 match premises in H': B \<Rightarrow> \<open>rule H'\<close>\<close>) 475 476text \<open> 477 In this example, the inner @{method match} can find the focused premise 478 @{term B}. In contrast, the @{method assumption} method would fail here due 479 to @{term B} not being logically accessible. 480\<close> 481 482 lemma "A \<Longrightarrow> A \<and> (B \<longrightarrow> B)" 483 by (match premises in H: A \<Rightarrow> \<open>intro conjI, rule H, rule impI, 484 match premises (local) in A \<Rightarrow> \<open>fail\<close> 485 \<bar> H': B \<Rightarrow> \<open>rule H'\<close>\<close>) 486 487text \<open> 488 In this example, the only premise that exists in the first focus is @{term 489 "A"}. Prior to the inner match, the rule \<open>impI\<close> changes the goal @{term "B \<longrightarrow> 490 B"} into @{term "B \<Longrightarrow> B"}. A standard premise match would also include @{term 491 A} as an original premise of the outer match. The \<open>local\<close> argument limits 492 the match to newly focused premises. 493\<close> 494 495 496section \<open>Attributes\<close> 497 498text \<open> 499 Attributes may throw errors when applied to a given fact. For example, rule 500 instantiation will fail of there is a type mismatch or if a given variable 501 doesn't exist. Within a match or a method definition, it isn't generally 502 possible to guarantee that applied attributes won't fail. For example, in 503 the following method there is no guarantee that the two provided facts will 504 necessarily compose. 505\<close> 506 507 method my_compose uses rule1 rule2 = 508 (rule rule1 [OF rule2]) 509 510text \<open> 511 Some attributes (like @{attribute OF}) have been made partially 512 Eisbach-aware. This means that they are able to form a closure despite not 513 necessarily always being applicable. In the case of @{attribute OF}, it is 514 up to the proof author to guard attribute application with an appropriate 515 @{method match}, but there are still no static guarantees. 516 517 In contrast to @{attribute OF}, the @{attribute "where"} and @{attribute of} 518 attributes attempt to provide static guarantees that they will apply 519 whenever possible. 520 521 Within a match pattern for a fact, each outermost quantifier specifies the 522 requirement that a matching fact must have a schematic variable at that 523 point. This gives a corresponding name to this ``slot'' for the purposes of 524 forming a static closure, allowing the @{attribute "where"} attribute to 525 perform an instantiation at run-time. 526\<close> 527 528 lemma 529 assumes A: "Q \<Longrightarrow> False" 530 shows "\<not> Q" 531 by (match intros in X: "\<And>P. (P \<Longrightarrow> False) \<Longrightarrow> \<not> P" \<Rightarrow> 532 \<open>rule X [where P = Q, OF A]\<close>) 533 534text \<open> 535 Subgoal focusing converts the outermost quantifiers of premises into 536 schematics when lifting them to hypothetical facts. This allows us to 537 instantiate them with @{attribute "where"} when using an appropriate match 538 pattern. 539\<close> 540 541 lemma "(\<And>x :: 'a. A x \<Longrightarrow> B x) \<Longrightarrow> A y \<Longrightarrow> B y" 542 by (match premises in I: "\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x" \<Rightarrow> 543 \<open>rule I [where x = y]\<close>) 544 545text \<open> 546 The @{attribute of} attribute behaves similarly. It is worth noting, 547 however, that the positional instantiation of @{attribute of} occurs against 548 the position of the variables as they are declared \<^emph>\<open>in the match pattern\<close>. 549\<close> 550 551 lemma 552 fixes A B and x :: 'a and y :: 'b 553 assumes asm: "(\<And>x y. A y x \<Longrightarrow> B x y )" 554 shows "A y x \<Longrightarrow> B x y" 555 by (match asm in I: "\<And>(x :: 'a) (y :: 'b). ?P x y \<Longrightarrow> ?Q x y" \<Rightarrow> 556 \<open>rule I [of x y]\<close>) 557 558text \<open> 559 In this example, the order of schematics in \<open>asm\<close> is actually \<open>?y ?x\<close>, but 560 we instantiate our matched rule in the opposite order. This is because the 561 effective rule @{term I} was bound from the match, which declared the @{typ 562 'a} slot first and the @{typ 'b} slot second. 563 564 To get the dynamic behaviour of @{attribute of} we can choose to invoke it 565 \<^emph>\<open>unchecked\<close>. This avoids trying to do any type inference for the provided 566 parameters, instead storing them as their most general type and doing type 567 matching at run-time. This, like @{attribute OF}, will throw errors if the 568 expected slots don't exist or there is a type mismatch. 569\<close> 570 571 lemma 572 fixes A B and x :: 'a and y :: 'b 573 assumes asm: "\<And>x y. A y x \<Longrightarrow> B x y" 574 shows "A y x \<Longrightarrow> B x y" 575 by (match asm in I: "PROP ?P" \<Rightarrow> \<open>rule I [of (unchecked) y x]\<close>) 576 577text \<open> 578 Attributes may be applied to matched facts directly as they are matched. Any 579 declarations will therefore be applied in the context of the inner method, 580 as well as any transformations to the rule. 581\<close> 582 583 lemma "(\<And>x :: 'a. A x \<Longrightarrow> B x) \<Longrightarrow> A y \<longrightarrow> B y" 584 by (match premises in I [of y, intros]: "\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x" \<Rightarrow> 585 \<open>prop_solver\<close>) 586 587text \<open> 588 In this example, the pattern \<open>\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x\<close> matches against the 589 only premise, giving an appropriately typed slot for @{term y}. After the 590 match, the resulting rule is instantiated to @{term y} and then declared as 591 an @{attribute intros} rule. This is then picked up by @{method prop_solver} 592 to solve the goal. 593\<close> 594 595 596section \<open>Multi-match \label{sec:multi}\<close> 597 598text \<open> 599 In all previous examples, @{method match} was only ever searching for a 600 single rule or premise. Each local fact would therefore always have a length 601 of exactly one. We may, however, wish to find \<^emph>\<open>all\<close> matching results. To 602 achieve this, we can simply mark a given pattern with the \<open>(multi)\<close> 603 argument. 604\<close> 605 606 lemma 607 assumes asms: "A \<Longrightarrow> B" "A \<Longrightarrow> D" 608 shows "(A \<longrightarrow> B) \<and> (A \<longrightarrow> D)" 609 apply (match asms in I [intros]: "?P \<Longrightarrow> ?Q" \<Rightarrow> \<open>solves \<open>prop_solver\<close>\<close>)? 610 apply (match asms in I [intros]: "?P \<Longrightarrow> ?Q" (multi) \<Rightarrow> \<open>prop_solver\<close>) 611 done 612 613text \<open> 614 In the first @{method match}, without the \<open>(multi)\<close> argument, @{term I} is 615 only ever be bound to one of the members of \<open>asms\<close>. This backtracks over 616 both possibilities (see next section), however neither assumption in 617 isolation is sufficient to solve to goal. The use of the @{method solves} 618 combinator ensures that @{method prop_solver} has no effect on the goal when 619 it doesn't solve it, and so the first match leaves the goal unchanged. In 620 the second @{method match}, \<open>I\<close> is bound to all of \<open>asms\<close>, declaring both 621 results as \<open>intros\<close>. With these rules @{method prop_solver} is capable of 622 solving the goal. 623 624 Using for-fixed variables in patterns imposes additional constraints on the 625 results. In all previous examples, the choice of using \<open>?P\<close> or a for-fixed 626 @{term P} only depended on whether or not @{term P} was mentioned in another 627 pattern or the inner method. When using a multi-match, however, all 628 for-fixed terms must agree in the results. 629\<close> 630 631 lemma 632 assumes asms: "A \<Longrightarrow> B" "A \<Longrightarrow> D" "D \<Longrightarrow> B" 633 shows "(A \<longrightarrow> B) \<and> (A \<longrightarrow> D)" 634 apply (match asms in I [intros]: "?P \<Longrightarrow> Q" (multi) for Q \<Rightarrow> 635 \<open>solves \<open>prop_solver\<close>\<close>)? 636 apply (match asms in I [intros]: "P \<Longrightarrow> ?Q" (multi) for P \<Rightarrow> 637 \<open>prop_solver\<close>) 638 done 639 640text \<open> 641 Here we have two seemingly-equivalent applications of @{method match}, 642 however only the second one is capable of solving the goal. The first 643 @{method match} selects the first and third members of \<open>asms\<close> (those that 644 agree on their conclusion), which is not sufficient. The second @{method 645 match} selects the first and second members of \<open>asms\<close> (those that agree on 646 their assumption), which is enough for @{method prop_solver} to solve the 647 goal. 648\<close> 649 650 651section \<open>Dummy patterns\<close> 652 653text \<open> 654 Dummy patterns may be given as placeholders for unique schematics in 655 patterns. They implicitly receive all currently bound variables as 656 arguments, and are coerced into the @{typ prop} type whenever possible. For 657 example, the trivial dummy pattern \<open>_\<close> will match any proposition. In 658 contrast, by default the pattern \<open>?P\<close> is considered to have type @{typ 659 bool}. It will not bind anything with meta-logical connectives (e.g. \<open>_ \<Longrightarrow> _\<close> 660 or \<open>_ &&& _\<close>). 661\<close> 662 663 lemma 664 assumes asms: "A &&& B \<Longrightarrow> D" 665 shows "(A \<and> B \<longrightarrow> D)" 666 by (match asms in I: _ \<Rightarrow> \<open>prop_solver intros: I conjunctionI\<close>) 667 668 669section \<open>Backtracking\<close> 670 671text \<open> 672 Patterns are considered top-down, executing the inner method \<open>m\<close> of the 673 first pattern which is satisfied by the current match target. By default, 674 matching performs extensive backtracking by attempting all valid variable 675 and fact bindings according to the given pattern. In particular, all 676 unifiers for a given pattern will be explored, as well as each matching 677 fact. The inner method \<open>m\<close> will be re-executed for each different 678 variable/fact binding during backtracking. A successful match is considered 679 a cut-point for backtracking. Specifically, once a match is made no other 680 pattern-method pairs will be considered. 681 682 The method \<open>foo\<close> below fails for all goals that are conjunctions. Any such 683 goal will match the first pattern, causing the second pattern (that would 684 otherwise match all goals) to never be considered. 685\<close> 686 687 method foo = 688 (match conclusion in "?P \<and> ?Q" \<Rightarrow> \<open>fail\<close> \<bar> "?R" \<Rightarrow> \<open>prop_solver\<close>) 689 690text \<open> 691 The failure of an inner method that is executed after a successful match 692 will cause the entire match to fail. This distinction is important due to 693 the pervasive use of backtracking. When a method is used in a combinator 694 chain, its failure becomes significant because it signals previously applied 695 methods to move to the next result. Therefore, it is necessary for @{method 696 match} to not mask such failure. One can always rewrite a match using the 697 combinators ``\<open>?\<close>'' and ``\<open>|\<close>'' to try subsequent patterns in the case of an 698 inner-method failure. The following proof method, for example, always 699 invokes @{method prop_solver} for all goals because its first alternative 700 either never matches or (if it does match) always fails. 701\<close> 702 703 method foo\<^sub>1 = 704 (match conclusion in "?P \<and> ?Q" \<Rightarrow> \<open>fail\<close>) | 705 (match conclusion in "?R" \<Rightarrow> \<open>prop_solver\<close>) 706 707 708subsection \<open>Cut\<close> 709 710text \<open> 711 Backtracking may be controlled more precisely by marking individual patterns 712 as \<open>cut\<close>. This causes backtracking to not progress beyond this pattern: once 713 a match is found no others will be considered. 714\<close> 715 716 method foo\<^sub>2 = 717 (match premises in I: "P \<and> Q" (cut) and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> 718 \<open>rule mp [OF I' I [THEN conjunct1]]\<close>) 719 720text \<open> 721 In this example, once a conjunction is found (@{term "P \<and> Q"}), all possible 722 implications of @{term "P"} in the premises are considered, evaluating the 723 inner @{method rule} with each consequent. No other conjunctions will be 724 considered, with method failure occurring once all implications of the form 725 \<open>P \<longrightarrow> ?U\<close> have been explored. Here the left-right processing of individual 726 patterns is important, as all patterns after of the cut will maintain their 727 usual backtracking behaviour. 728\<close> 729 730 lemma "A \<and> B \<Longrightarrow> A \<longrightarrow> D \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> C" 731 by foo\<^sub>2 732 733 lemma "C \<and> D \<Longrightarrow> A \<and> B \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> C" 734 by (foo\<^sub>2 | prop_solver) 735 736text \<open> 737 In this example, the first lemma is solved by \<open>foo\<^sub>2\<close>, by first picking 738 @{term "A \<longrightarrow> D"} for \<open>I'\<close>, then backtracking and ultimately succeeding after 739 picking @{term "A \<longrightarrow> C"}. In the second lemma, however, @{term "C \<and> D"} is 740 matched first, the second pattern in the match cannot be found and so the 741 method fails, falling through to @{method prop_solver}. 742 743 More precise control is also possible by giving a positive number \<open>n\<close> as an 744 argument to \<open>cut\<close>. This will limit the number of backtracking results of 745 that match to be at most \<open>n\<close>. The match argument \<open>(cut 1)\<close> is the same as 746 simply \<open>(cut)\<close>. 747\<close> 748 749 750subsection \<open>Multi-match revisited\<close> 751 752text \<open> 753 A multi-match will produce a sequence of potential bindings for for-fixed 754 variables, where each binding environment is the result of matching against 755 at least one element from the match target. For each environment, the match 756 result will be all elements of the match target which agree with the pattern 757 under that environment. This can result in unexpected behaviour when giving 758 very general patterns. 759\<close> 760 761 lemma 762 assumes asms: "\<And>x. A x \<and> B x" "\<And>y. A y \<and> C y" "\<And>z. B z \<and> C z" 763 shows "A x \<and> C x" 764 by (match asms in I: "\<And>x. P x \<and> ?Q x" (multi) for P \<Rightarrow> 765 \<open>match (P) in "A" \<Rightarrow> \<open>fail\<close> 766 \<bar> _ \<Rightarrow> \<open>match I in "\<And>x. A x \<and> B x" \<Rightarrow> \<open>fail\<close> 767 \<bar> _ \<Rightarrow> \<open>rule I\<close>\<close>\<close>) 768 769text \<open> 770 Intuitively it seems like this proof should fail to check. The first match 771 result, which binds @{term I} to the first two members of \<open>asms\<close>, fails the 772 second inner match due to binding @{term P} to @{term A}. Backtracking then 773 attempts to bind @{term I} to the third member of \<open>asms\<close>. This passes all 774 inner matches, but fails when @{method rule} cannot successfully apply this 775 to the current goal. After this, a valid match that is produced by the 776 unifier is one which binds @{term P} to simply \<open>\<lambda>a. A ?x\<close>. The first inner 777 match succeeds because \<open>\<lambda>a. A ?x\<close> does not match @{term A}. The next inner 778 match succeeds because @{term I} has only been bound to the first member of 779 \<open>asms\<close>. This is due to @{method match} considering \<open>\<lambda>a. A ?x\<close> and \<open>\<lambda>a. A ?y\<close> 780 as distinct terms. 781 782 The simplest way to address this is to explicitly disallow term bindings 783 which we would consider invalid. 784\<close> 785 786 method abs_used for P = 787 (match (P) in "\<lambda>a. ?P" \<Rightarrow> \<open>fail\<close> \<bar> _ \<Rightarrow> \<open>-\<close>) 788 789text \<open> 790 This method has no effect on the goal state, but instead serves as a filter 791 on the environment produced from match. 792\<close> 793 794 795section \<open>Uncurrying\<close> 796 797text \<open> 798 The @{method match} method is not aware of the logical content of match 799 targets. Each pattern is simply matched against the shallow structure of a 800 fact or term. Most facts are in \<^emph>\<open>normal form\<close>, which curries premises via 801 meta-implication \<open>_ \<Longrightarrow> _\<close>. 802\<close> 803 804 lemma 805 assumes asms: "D \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> A" 806 shows "D \<Longrightarrow> B \<Longrightarrow> C \<and> A" 807 by (match asms in H: "D \<Longrightarrow> _" (multi) \<Rightarrow> \<open>prop_solver elims: H\<close>) 808 809text \<open> 810 For the first member of \<open>asms\<close> the dummy pattern successfully matches 811 against @{term "B \<Longrightarrow> C"} and so the proof is successful. 812\<close> 813 814 lemma 815 assumes asms: "A \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> C" 816 shows "D \<or> (A \<and> B) \<Longrightarrow> C" 817 apply (match asms in H: "_ \<Longrightarrow> C" (multi) \<Rightarrow> \<open>prop_solver elims: H\<close>)(*<*)? 818 apply (prop_solver elims: asms) 819 done(*>*) 820 821text \<open> 822 This proof will fail to solve the goal. Our match pattern will only match 823 rules which have a single premise, and conclusion @{term C}, so the first 824 member of \<open>asms\<close> is not bound and thus the proof fails. Matching a pattern 825 of the form @{term "P \<Longrightarrow> Q"} against this fact will bind @{term "P"} to 826 @{term "A"} and @{term Q} to @{term "B \<Longrightarrow> C"}. Our pattern, with a concrete 827 @{term "C"} in the conclusion, will fail to match this fact. 828 829 To express our desired match, we may \<^emph>\<open>uncurry\<close> our rules before matching 830 against them. This forms a meta-conjunction of all premises in a fact, so 831 that only one implication remains. For example the uncurried version of 832 @{term "A \<Longrightarrow> B \<Longrightarrow> C"} is @{term "A &&& B \<Longrightarrow> C"}. This will now match our 833 desired pattern \<open>_ \<Longrightarrow> C\<close>, and can be \<^emph>\<open>curried\<close> after the match to put it 834 back into normal form. 835\<close> 836 837 lemma 838 assumes asms: "A \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> C" 839 shows "D \<or> (A \<and> B) \<Longrightarrow> C" 840 by (match asms [uncurry] in H [curry]: "_ \<Longrightarrow> C" (multi) \<Rightarrow> 841 \<open>prop_solver elims: H\<close>) 842 843 844section \<open>Reverse matching\<close> 845 846text \<open> 847 The @{method match} method only attempts to perform matching of the pattern 848 against the match target. Specifically this means that it will not 849 instantiate schematic terms in the match target. 850\<close> 851 852 lemma 853 assumes asms: "\<And>x :: 'a. A x" 854 shows "A y" 855 apply (match asms in H: "A y" \<Rightarrow> \<open>rule H\<close>)? 856 apply (match asms in H: P for P \<Rightarrow> 857 \<open>match ("A y") in P \<Rightarrow> \<open>rule H\<close>\<close>) 858 done 859 860text \<open> 861 In the first @{method match} we attempt to find a member of \<open>asms\<close> which 862 matches our goal precisely. This fails due to no such member existing. The 863 second match reverses the role of the fact in the match, by first giving a 864 general pattern @{term P}. This bound pattern is then matched against @{term 865 "A y"}. In this case, @{term P} is bound to \<open>A ?x\<close> and so it successfully 866 matches. 867\<close> 868 869 870section \<open>Type matching\<close> 871 872text \<open> 873 The rule instantiation attributes @{attribute "where"} and @{attribute "of"} 874 attempt to guarantee type-correctness wherever possible. This can require 875 additional invocations of @{method match} in order to statically ensure that 876 instantiation will succeed. 877\<close> 878 879 lemma 880 assumes asms: "\<And>x :: 'a. A x" 881 shows "A y" 882 by (match asms in H: "\<And>z :: 'b. P z" for P \<Rightarrow> 883 \<open>match (y) in "y :: 'b" for y \<Rightarrow> \<open>rule H [where z = y]\<close>\<close>) 884 885text \<open> 886 In this example the type \<open>'b\<close> is matched to \<open>'a\<close>, however statically they 887 are formally distinct types. The first match binds \<open>'b\<close> while the inner 888 match serves to coerce @{term y} into having the type \<open>'b\<close>. This allows the 889 rule instantiation to successfully apply. 890\<close> 891 892 893chapter \<open>Method development\<close> 894 895section \<open>Tracing methods\<close> 896 897text \<open> 898 Method tracing is supported by auxiliary print methods provided by @{theory 899 "HOL-Eisbach.Eisbach_Tools"}. These include @{method print_fact}, @{method 900 print_term} and @{method print_type}. Whenever a print method is evaluated 901 it leaves the goal unchanged and writes its argument as tracing output. 902 903 Print methods can be combined with the @{method fail} method to investigate 904 the backtracking behaviour of a method. 905\<close> 906 907 lemma 908 assumes asms: A B C D 909 shows D 910 apply (match asms in H: _ \<Rightarrow> \<open>print_fact H, fail\<close>)(*<*)? 911 apply (simp add: asms) 912 done(*>*) 913 914text \<open> 915 This proof will fail, but the tracing output will show the order that the 916 assumptions are attempted. 917\<close> 918 919 920section \<open>Integrating with Isabelle/ML\<close> 921 922subsubsection \<open>Attributes\<close> 923 924text \<open> 925 A custom rule attribute is a simple way to extend the functionality of 926 Eisbach methods. The dummy rule attribute notation (\<open>[[ _ ]]\<close>) invokes the 927 given attribute against a dummy fact and evaluates to the result of that 928 attribute. When used as a match target, this can serve as an effective 929 auxiliary function. 930\<close> 931 932 attribute_setup get_split_rule = 933 \<open>Args.term >> (fn t => 934 Thm.rule_attribute [] (fn context => fn _ => 935 (case get_split_rule (Context.proof_of context) t of 936 SOME thm => thm 937 | NONE => Drule.dummy_thm)))\<close> 938 939text \<open> 940 In this example, the new attribute @{attribute get_split_rule} lifts the ML 941 function of the same name into an attribute. When applied to a case 942 distinction over a datatype, it retrieves its corresponding split rule. 943 944 We can then integrate this intro a method that applies the split rule, first 945 matching to ensure that fetching the rule was successful. 946\<close> 947(*<*)declare TrueI [intros](*>*) 948 method splits = 949 (match conclusion in "?P f" for f \<Rightarrow> 950 \<open>match [[get_split_rule f]] in U: "(_ :: bool) = _" \<Rightarrow> 951 \<open>rule U [THEN iffD2]\<close>\<close>) 952 953 lemma "L \<noteq> [] \<Longrightarrow> case L of [] \<Rightarrow> False | _ \<Rightarrow> True" 954 apply splits 955 apply (prop_solver intros: allI) 956 done 957 958text \<open> 959 Here the new @{method splits} method transforms the goal to use only logical 960 connectives: @{term "L = [] \<longrightarrow> False \<and> (\<forall>x y. L = x # y \<longrightarrow> True)"}. This goal 961 is then in a form solvable by @{method prop_solver} when given the universal 962 quantifier introduction rule \<open>allI\<close>. 963\<close> 964 965end 966