src/Doc/Eisbach/Manual.thy
changeset 60288 d7f636331176
child 60298 7c278b692aae
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Doc/Eisbach/Manual.thy	Sun May 17 23:03:49 2015 +0200
     1.3 @@ -0,0 +1,923 @@
     1.4 +(*:wrap=hard:maxLineLen=78:*)
     1.5 +
     1.6 +theory Manual
     1.7 +imports Base "../Eisbach_Tools"
     1.8 +begin
     1.9 +
    1.10 +chapter \<open>The method command\<close>
    1.11 +
    1.12 +text \<open>
    1.13 +  The @{command_def method} command provides the ability to write proof
    1.14 +  methods by combining existing ones with their usual syntax. Specifically it
    1.15 +  allows compound proof methods to be named, and to extend the name space of
    1.16 +  basic methods accordingly. Method definitions may abstract over parameters:
    1.17 +  terms, facts, or other methods.
    1.18 +
    1.19 +  \medskip The syntax diagram below refers to some syntactic categories that
    1.20 +  are further defined in @{cite "isabelle-isar-ref"}.
    1.21 +
    1.22 +  @{rail \<open>
    1.23 +    @@{command method} name args @'=' method
    1.24 +    ;
    1.25 +    args: term_args? method_args? \<newline> fact_args? decl_args?
    1.26 +    ;
    1.27 +    term_args: @'for' @{syntax "fixes"}
    1.28 +    ;
    1.29 +    method_args: @'methods' (name+)
    1.30 +    ;
    1.31 +    fact_args: @'uses' (name+)
    1.32 +    ;
    1.33 +    decl_args: @'declares' (name+)
    1.34 +  \<close>}
    1.35 +\<close>
    1.36 +
    1.37 +
    1.38 +section \<open>Basic method definitions\<close>
    1.39 +
    1.40 +text \<open>
    1.41 +  Consider the following proof that makes use of usual Isar method
    1.42 +  combinators.
    1.43 +\<close>
    1.44 +
    1.45 +    lemma "P \<and> Q \<longrightarrow> P"
    1.46 +      by ((rule impI, (erule conjE)?) | assumption)+
    1.47 +
    1.48 +text \<open>
    1.49 +  It is clear that this compound method will be applicable in more cases than
    1.50 +  this proof alone. With the @{command method} command we can define a proof
    1.51 +  method that makes the above functionality available generally.
    1.52 +\<close>
    1.53 +
    1.54 +    method prop_solver\<^sub>1 =
    1.55 +      ((rule impI, (erule conjE)?) | assumption)+
    1.56 +
    1.57 +    lemma "P \<and> Q \<and> R \<longrightarrow> P"
    1.58 +      by prop_solver\<^sub>1
    1.59 +
    1.60 +text \<open>
    1.61 +  In this example, the facts @{text impI} and @{text conjE} are static. They
    1.62 +  are evaluated once when the method is defined and cannot be changed later.
    1.63 +  This makes the method stable in the sense of \emph{static scoping}: naming
    1.64 +  another fact @{text impI} in a later context won't affect the behaviour of
    1.65 +  @{text "prop_solver\<^sub>1"}.
    1.66 +\<close>
    1.67 +
    1.68 +
    1.69 +section \<open>Term abstraction\<close>
    1.70 +
    1.71 +text \<open>
    1.72 +  Methods can also abstract over terms using the @{keyword_def "for"} keyword,
    1.73 +  optionally providing type constraints. For instance, the following proof
    1.74 +  method @{text intro_ex} takes a term @{term y} of any type, which it uses to
    1.75 +  instantiate the @{term x}-variable of @{text exI} (existential introduction)
    1.76 +  before applying the result as a rule. The instantiation is performed here by
    1.77 +  Isar's @{attribute_ref "where"} attribute. If the current subgoal is to find
    1.78 +  a witness for the given predicate @{term Q}, then this has the effect of
    1.79 +  committing to @{term y}.
    1.80 +\<close>
    1.81 +
    1.82 +    method intro_ex for Q :: "'a \<Rightarrow> bool" and y :: 'a =
    1.83 +      (rule exI ["where" P = Q and x = y])
    1.84 +
    1.85 +
    1.86 +text \<open>
    1.87 +  The term parameters @{term y} and @{term Q} can be used arbitrarily inside
    1.88 +  the method body, as part of attribute applications or arguments to other
    1.89 +  methods. The expression is type-checked as far as possible when the method
    1.90 +  is defined, however dynamic type errors can still occur when it is invoked
    1.91 +  (e.g.\ when terms are instantiated in a parameterized fact). Actual term
    1.92 +  arguments are supplied positionally, in the same order as in the method
    1.93 +  definition.
    1.94 +\<close>
    1.95 +
    1.96 +    lemma "P a \<Longrightarrow> \<exists>x. P x"
    1.97 +      by (intro_ex P a)
    1.98 +
    1.99 +
   1.100 +section \<open>Fact abstraction\<close>
   1.101 +
   1.102 +subsection \<open>Named theorems\<close>
   1.103 +
   1.104 +text \<open>
   1.105 +  A @{text "named theorem"} is a fact whose contents are produced dynamically
   1.106 +  within the current proof context. The Isar command @{command_ref
   1.107 +  "named_theorems"} provides simple access to this concept: it declares a
   1.108 +  dynamic fact with corresponding \emph{attribute}
   1.109 +  (see \autoref{s:attributes}) for managing this particular data slot in the
   1.110 +  context.
   1.111 +\<close>
   1.112 +
   1.113 +    named_theorems intros
   1.114 +
   1.115 +text \<open>
   1.116 +  So far @{text "intros"} refers to the empty fact. Using the Isar command
   1.117 +  @{command_ref "declare"} we may apply declaration attributes to the context.
   1.118 +  Below we declare both @{text "conjI"} and @{text "impI"} as @{text
   1.119 +  "intros"}, adding them to the named theorem slot.
   1.120 +\<close>
   1.121 +
   1.122 +    declare conjI [intros] and impI [intros]
   1.123 +
   1.124 +text \<open>
   1.125 +  We can refer to named theorems as dynamic facts within a particular proof
   1.126 +  context, which are evaluated whenever the method is invoked. Instead of
   1.127 +  having facts hard-coded into the method, as in @{text prop_solver\<^sub>1}, we can
   1.128 +  instead refer to these named theorems.
   1.129 +\<close>
   1.130 +
   1.131 +    named_theorems elims
   1.132 +    declare conjE [elims]
   1.133 +
   1.134 +    method prop_solver\<^sub>3 =
   1.135 +      ((rule intros, (erule elims)?) | assumption)+
   1.136 +
   1.137 +    lemma "P \<and> Q \<longrightarrow> P"
   1.138 +      by prop_solver\<^sub>3
   1.139 +
   1.140 +text \<open>
   1.141 +  Often these named theorems need to be augmented on the spot, when a method
   1.142 +  is invoked. The @{keyword_def "declares"} keyword in the signature of
   1.143 +  @{command method} adds the common method syntax @{text "method decl: facts"}
   1.144 +  for each named theorem @{text decl}.
   1.145 +\<close>
   1.146 +
   1.147 +    method prop_solver\<^sub>4 declares intros elims =
   1.148 +      ((rule intros, (erule elims)?) | assumption)+
   1.149 +
   1.150 +    lemma "P \<and> (P \<longrightarrow> Q) \<longrightarrow> Q \<and> P"
   1.151 +      by (prop_solver\<^sub>4 elims: impE intros: conjI)
   1.152 +
   1.153 +
   1.154 +subsection \<open>Simple fact abstraction\<close>
   1.155 +
   1.156 +text \<open>
   1.157 +  The @{keyword "declares"} keyword requires that a corresponding dynamic fact
   1.158 +  has been declared with @{command_ref named_theorems}. This is useful for
   1.159 +  managing collections of facts which are to be augmented with declarations,
   1.160 +  but is overkill if we simply want to pass a fact to a method.
   1.161 +
   1.162 +  We may use the @{keyword_def "uses"} keyword in the method header to provide
   1.163 +  a simple fact parameter. In contrast to @{keyword "declares"}, these facts
   1.164 +  are always implicitly empty unless augmented when the method is invoked.
   1.165 +\<close>
   1.166 +
   1.167 +    method rule_twice uses my_rule =
   1.168 +      (rule my_rule, rule my_rule)
   1.169 +
   1.170 +    lemma "P \<Longrightarrow> Q \<Longrightarrow> (P \<and> Q) \<and> Q"
   1.171 +      by (rule_twice my_rule: conjI)
   1.172 +
   1.173 +
   1.174 +section \<open>Higher-order methods\<close>
   1.175 +
   1.176 +text \<open>
   1.177 +  The \emph{structured concatenation} combinator ``@{text "method\<^sub>1 ;
   1.178 +  method\<^sub>2"}'' was introduced in Isabelle2015, motivated by development of
   1.179 +  Eisbach. It is similar to ``@{text "method\<^sub>1, method\<^sub>2"}'', but @{text
   1.180 +  method\<^sub>2} is invoked on on \emph{all} subgoals that have newly emerged from
   1.181 +  @{text method\<^sub>1}. This is useful to handle cases where the number of
   1.182 +  subgoals produced by a method is determined dynamically at run-time.
   1.183 +\<close>
   1.184 +
   1.185 +    method conj_with uses rule =
   1.186 +      (intro conjI ; intro rule)
   1.187 +
   1.188 +    lemma
   1.189 +      assumes A: "P"
   1.190 +      shows "P \<and> P \<and> P"
   1.191 +      by (conj_with rule: A)
   1.192 +
   1.193 +text \<open>
   1.194 +  Method definitions may take other methods as arguments, and thus implement
   1.195 +  method combinators with prefix syntax. For example, to more usefully exploit
   1.196 +  Isabelle's backtracking, the explicit requirement that a method solve all
   1.197 +  produced subgoals is frequently useful. This can easily be written as a
   1.198 +  \emph{higher-order method} using ``@{text ";"}''. The @{keyword "methods"}
   1.199 +  keyword denotes method parameters that are other proof methods to be invoked
   1.200 +  by the method being defined.
   1.201 +\<close>
   1.202 +
   1.203 +    method solve methods m = (m ; fail)
   1.204 +
   1.205 +text \<open>
   1.206 +  Given some method-argument @{text m}, @{text "solve \<open>m\<close>"} applies the
   1.207 +  method @{text m} and then fails whenever @{text m} produces any new unsolved
   1.208 +  subgoals --- i.e. when @{text m} fails to completely discharge the goal it
   1.209 +  was applied to.
   1.210 +\<close>
   1.211 +
   1.212 +
   1.213 +section \<open>Example\<close>
   1.214 +
   1.215 +text \<open>
   1.216 +  With these simple features we are ready to write our first non-trivial proof
   1.217 +  method. Returning to the first-order logic example, the following method
   1.218 +  definition applies various rules with their canonical methods.
   1.219 +\<close>
   1.220 +
   1.221 +    named_theorems subst
   1.222 +
   1.223 +    method prop_solver declares intros elims subst =
   1.224 +      (assumption |
   1.225 +        (rule intros) | erule elims |
   1.226 +        subst subst | subst (asm) subst |
   1.227 +        (erule notE ; solve \<open>prop_solver\<close>))+
   1.228 +
   1.229 +text \<open>
   1.230 +  The only non-trivial part above is the final alternative @{text "(erule notE
   1.231 +  ; solve \<open>prop_solver\<close>)"}. Here, in the case that all other alternatives
   1.232 +  fail, the method takes one of the assumptions @{term "\<not> P"} of the current
   1.233 +  goal and eliminates it with the rule @{text notE}, causing the goal to be
   1.234 +  proved to become @{term P}. The method then recursively invokes itself on
   1.235 +  the remaining goals. The job of the recursive call is to demonstrate that
   1.236 +  there is a contradiction in the original assumptions (i.e.\ that @{term P}
   1.237 +  can be derived from them). Note this recursive invocation is applied with
   1.238 +  the @{method solve} method combinator to ensure that a contradiction will
   1.239 +  indeed be shown. In the case where a contradiction cannot be found,
   1.240 +  backtracking will occur and a different assumption @{term "\<not> Q"} will be
   1.241 +  chosen for elimination.
   1.242 +
   1.243 +  Note that the recursive call to @{method prop_solver} does not have any
   1.244 +  parameters passed to it. Recall that fact parameters, e.g.\ @{text
   1.245 +  "intros"}, @{text "elims"}, and @{text "subst"}, are managed by declarations
   1.246 +  in the current proof context. They will therefore be passed to any recursive
   1.247 +  call to @{method prop_solver} and, more generally, any invocation of a
   1.248 +  method which declares these named theorems.
   1.249 +
   1.250 +  \medskip After declaring some standard rules to the context, the @{method
   1.251 +  prop_solver} becomes capable of solving non-trivial propositional
   1.252 +  tautologies.\<close>
   1.253 +
   1.254 +    lemmas [intros] =
   1.255 +      conjI  --  \<open>@{thm conjI}\<close>
   1.256 +      impI  --  \<open>@{thm impI}\<close>
   1.257 +      disjCI  --  \<open>@{thm disjCI}\<close>
   1.258 +      iffI  --  \<open>@{thm iffI}\<close>
   1.259 +      notI  --  \<open>@{thm notI}\<close>
   1.260 +      (*<*)TrueI(*>*)
   1.261 +    lemmas [elims] =
   1.262 +      impCE  --  \<open>@{thm impCE}\<close>
   1.263 +      conjE  --  \<open>@{thm conjE}\<close>
   1.264 +      disjE  --  \<open>@{thm disjE}\<close>
   1.265 +
   1.266 +    lemma "(A \<or> B) \<and> (A \<longrightarrow> C) \<and> (B \<longrightarrow> C) \<longrightarrow> C"
   1.267 +      by prop_solver
   1.268 +
   1.269 +
   1.270 +chapter \<open>The match method \label{s:matching}\<close>
   1.271 +
   1.272 +text \<open>
   1.273 +  So far we have seen methods defined as simple combinations of other methods.
   1.274 +  Some familiar programming language concepts have been introduced (i.e.\
   1.275 +  abstraction and recursion). The only control flow has been implicitly the
   1.276 +  result of backtracking. When designing more sophisticated proof methods this
   1.277 +  proves too restrictive and difficult to manage conceptually.
   1.278 +
   1.279 +  To address this, we introduce the @{method_def "match"} method, which
   1.280 +  provides more direct access to the higher-order matching facility at the
   1.281 +  core of Isabelle. It is implemented as a separate proof method (in
   1.282 +  Isabelle/ML), and thus can be directly applied to proofs, however it is most
   1.283 +  useful when applied in the context of writing Eisbach method definitions.
   1.284 +
   1.285 +  \medskip The syntax diagram below refers to some syntactic categories that
   1.286 +  are further defined in @{cite "isabelle-isar-ref"}.
   1.287 +
   1.288 +  @{rail \<open>
   1.289 +    @@{method match} kind @'in' (pattern '\<Rightarrow>' cartouche + '\<bar>')
   1.290 +    ;
   1.291 +    kind:
   1.292 +      (@'conclusion' | @'premises' ('(' 'local' ')')? |
   1.293 +       '(' term ')' | @{syntax thmrefs})
   1.294 +    ;
   1.295 +    pattern: fact_name? term args? \<newline> (@'for' fixes)?
   1.296 +    ;
   1.297 +    fact_name: @{syntax name} @{syntax attributes}? ':'
   1.298 +    ;
   1.299 +    args: '(' (('multi' | 'cut' nat?) + ',') ')'
   1.300 +  \<close>}
   1.301 +
   1.302 +  Matching allows methods to introspect the goal state, and to implement more
   1.303 +  explicit control flow. In the basic case, a term or fact @{text ts} is given
   1.304 +  to match against as a \emph{match target}, along with a collection of
   1.305 +  pattern-method pairs @{text "(p, m)"}: roughly speaking, when the pattern
   1.306 +  @{text p} matches any member of @{text ts}, the \emph{inner} method @{text
   1.307 +  m} will be executed.
   1.308 +\<close>
   1.309 +
   1.310 +    lemma
   1.311 +      assumes X:
   1.312 +        "Q \<longrightarrow> P"
   1.313 +        "Q"
   1.314 +      shows P
   1.315 +        by (match X in I: "Q \<longrightarrow> P" and I': "Q" \<Rightarrow> \<open>insert mp [OF I I']\<close>)
   1.316 +
   1.317 +text \<open>
   1.318 +  In this example we have a structured Isar proof, with the named
   1.319 +  assumption @{text "X"} and a conclusion @{term "P"}. With the match method
   1.320 +  we can find the local facts @{term "Q \<longrightarrow> P"} and @{term "Q"}, binding them to
   1.321 +  separately as @{text "I"} and @{text "I'"}. We then specialize the
   1.322 +  modus-ponens rule @{thm mp [of Q P]} to these facts to solve the goal.
   1.323 +\<close>
   1.324 +
   1.325 +
   1.326 +section \<open>Subgoal focus\<close>
   1.327 +
   1.328 +text\<open>
   1.329 +  In the previous example we were able to match against an assumption out of
   1.330 +  the Isar proof state. In general, however, proof subgoals can be
   1.331 +  \emph{unstructured}, with goal parameters and premises arising from rule
   1.332 +  application. To address this, @{method match} uses \emph{subgoal focusing}
   1.333 +  (see also \autoref{s:design}) to produce structured goals out of
   1.334 +  unstructured ones. In place of fact or term, we may give the
   1.335 +  keyword @{keyword_def "premises"} as the match target. This causes a subgoal
   1.336 +  focus on the first subgoal, lifting local goal parameters to fixed term
   1.337 +  variables and premises into hypothetical theorems. The match is performed
   1.338 +  against these theorems, naming them and binding them as appropriate.
   1.339 +  Similarly giving the keyword @{keyword_def "conclusion"} matches against the
   1.340 +  conclusion of the first subgoal.
   1.341 +
   1.342 +  An unstructured version of the previous example can then be similarly solved
   1.343 +  through focusing.
   1.344 +\<close>
   1.345 +
   1.346 +    lemma "Q \<longrightarrow> P \<Longrightarrow> Q \<Longrightarrow> P"
   1.347 +      by (match premises in
   1.348 +                I: "Q \<longrightarrow> P" and I': "Q" \<Rightarrow> \<open>insert mp [OF I I']\<close>)
   1.349 +
   1.350 +text \<open>
   1.351 +  Match variables may be specified by giving a list of @{keyword_ref
   1.352 +  "for"}-fixes after the pattern description. This marks those terms as bound
   1.353 +  variables, which may be used in the method body.
   1.354 +\<close>
   1.355 +
   1.356 +    lemma "Q \<longrightarrow> P \<Longrightarrow> Q \<Longrightarrow> P"
   1.357 +      by (match premises in I: "Q \<longrightarrow> A" and I': "Q" for A \<Rightarrow>
   1.358 +            \<open>match conclusion in A \<Rightarrow> \<open>insert mp [OF I I']\<close>\<close>)
   1.359 +
   1.360 +text \<open>
   1.361 +  In this example @{term A} is a match variable which is bound to @{term P}
   1.362 +  upon a successful match. The inner @{method match} then matches the
   1.363 +  now-bound @{term A} (bound to @{term P}) against the conclusion (also @{term
   1.364 +  P}), finally applying the specialized rule to solve the goal.
   1.365 +
   1.366 +  Schematic terms like @{text "?P"} may also be used to specify match
   1.367 +  variables, but the result of the match is not bound, and thus cannot be used
   1.368 +  in the inner method body.
   1.369 +
   1.370 +  \medskip In the following example we extract the predicate of an
   1.371 +  existentially quantified conclusion in the current subgoal and search the
   1.372 +  current premises for a matching fact. If both matches are successful, we
   1.373 +  then instantiate the existential introduction rule with both the witness and
   1.374 +  predicate, solving with the matched premise.
   1.375 +\<close>
   1.376 +
   1.377 +    method solve_ex =
   1.378 +      (match conclusion in "\<exists>x. Q x" for Q \<Rightarrow>
   1.379 +        \<open>match premises in U: "Q y" for y \<Rightarrow>
   1.380 +          \<open>rule exI [where P = Q and x = y, OF U]\<close>\<close>)
   1.381 +
   1.382 +text \<open>
   1.383 +  The first @{method match} matches the pattern @{term "\<exists>x. Q x"} against the
   1.384 +  current conclusion, binding the term @{term "Q"} in the inner match. Next
   1.385 +  the pattern @{text "Q y"} is matched against all premises of the current
   1.386 +  subgoal. In this case @{term "Q"} is fixed and @{term "y"} may be
   1.387 +  instantiated. Once a match is found, the local fact @{text U} is bound to
   1.388 +  the matching premise and the variable @{term "y"} is bound to the matching
   1.389 +  witness. The existential introduction rule @{text "exI:"}~@{thm exI} is then
   1.390 +  instantiated with @{term "y"} as the witness and @{term "Q"} as the
   1.391 +  predicate, with its proof obligation solved by the local fact U (using the
   1.392 +  Isar attribute @{attribute OF}). The following example is a trivial use of
   1.393 +  this method.
   1.394 +\<close>
   1.395 +
   1.396 +    lemma "halts p \<Longrightarrow> \<exists>x. halts x"
   1.397 +      by solve_ex
   1.398 +
   1.399 +
   1.400 +subsubsection \<open>Operating within a focus\<close>
   1.401 +
   1.402 +text \<open>
   1.403 +  Subgoal focusing provides a structured form of a subgoal, allowing for more
   1.404 +  expressive introspection of the goal state. This requires some consideration
   1.405 +  in order to be used effectively. When the keyword @{keyword "premises"} is
   1.406 +  given as the match target, the premises of the subgoal are lifted into
   1.407 +  hypothetical theorems, which can be found and named via match patterns.
   1.408 +  Additionally these premises are stripped from the subgoal, leaving only the
   1.409 +  conclusion. This renders them inaccessible to standard proof methods which
   1.410 +  operate on the premises, such as @{method frule} or @{method erule}. Naive
   1.411 +  usage of these methods within a match will most likely not function as the
   1.412 +  method author intended.
   1.413 +\<close>
   1.414 +
   1.415 +    method my_allE_bad for y :: 'a =
   1.416 +      (match premises in I: "\<forall>x :: 'a. ?Q x" \<Rightarrow>
   1.417 +        \<open>erule allE [where x = y]\<close>)
   1.418 +
   1.419 +text \<open>
   1.420 +  Here we take a single parameter @{term y} and specialize the universal
   1.421 +  elimination rule (@{thm allE}) to it, then attempt to apply this specialized
   1.422 +  rule with @{method erule}. The method @{method erule} will attempt to unify
   1.423 +  with a universal quantifier in the premises that matches the type of @{term
   1.424 +  y}. Since @{keyword "premises"} causes a focus, however, there are no
   1.425 +  subgoal premises to be found and thus @{method my_allE_bad} will always
   1.426 +  fail. If focusing instead left the premises in place, using methods
   1.427 +  like @{method erule} would lead to unintended behaviour, specifically during
   1.428 +  backtracking. In our example, @{method erule} could choose an alternate
   1.429 +  premise while backtracking, while leaving @{text I} bound to the original
   1.430 +  match. In the case of more complex inner methods, where either @{text I} or
   1.431 +  bound terms are used, this would almost certainly not be the intended
   1.432 +  behaviour.
   1.433 +
   1.434 +  An alternative implementation would be to specialize the elimination rule to
   1.435 +  the bound term and apply it directly.
   1.436 +\<close>
   1.437 +
   1.438 +    method my_allE_almost for y :: 'a =
   1.439 +      (match premises in I: "\<forall>x :: 'a. ?Q x" \<Rightarrow>
   1.440 +        \<open>rule allE [where x = y, OF I]\<close>)
   1.441 +
   1.442 +    lemma "\<forall>x. P x \<Longrightarrow> P y"
   1.443 +      by (my_allE_almost y)
   1.444 +
   1.445 +text \<open>
   1.446 +  This method will insert a specialized duplicate of a universally quantified
   1.447 +  premise. Although this will successfully apply in the presence of such a
   1.448 +  premise, it is not likely the intended behaviour. Repeated application of
   1.449 +  this method will produce an infinite stream of duplicate specialized
   1.450 +  premises, due to the original premise never being removed. To address this,
   1.451 +  matched premises may be declared with the @{attribute "thin"} attribute.
   1.452 +  This will hide the premise from subsequent inner matches, and remove it from
   1.453 +  the list of premises when the inner method has finished and the subgoal is
   1.454 +  unfocused. It can be considered analogous to the existing @{text thin_tac}.
   1.455 +
   1.456 +  To complete our example, the correct implementation of the method
   1.457 +  will @{attribute "thin"} the premise from the match and then apply it to the
   1.458 +  specialized elimination rule.\<close>
   1.459 +
   1.460 +    method my_allE for y :: 'a =
   1.461 +      (match premises in I [thin]: "\<forall>x :: 'a. ?Q x" \<Rightarrow>
   1.462 +         \<open>rule allE [where x = y, OF I]\<close>)
   1.463 +
   1.464 +    lemma "\<forall>x. P x \<Longrightarrow> \<forall>x. Q x \<Longrightarrow> P y \<and> Q y"
   1.465 +      by (my_allE y)+ (rule conjI)
   1.466 +
   1.467 +
   1.468 +subsection \<open>Attributes\<close>
   1.469 +
   1.470 +text \<open>
   1.471 +  Attributes may throw errors when applied to a given fact. For example, rule
   1.472 +  instantiation will fail of there is a type mismatch or if a given variable
   1.473 +  doesn't exist. Within a match or a method definition, it isn't generally
   1.474 +  possible to guarantee that applied attributes won't fail. For example, in
   1.475 +  the following method there is no guarantee that the two provided facts will
   1.476 +  necessarily compose.
   1.477 +\<close>
   1.478 +
   1.479 +    method my_compose uses rule1 rule2 =
   1.480 +      (rule rule1[OF rule2])
   1.481 +
   1.482 +text \<open>
   1.483 +  Some attributes (like @{attribute OF}) have been made partially
   1.484 +  Eisbach-aware. This means that they are able to form a closure despite not
   1.485 +  necessarily always being applicable. In the case of @{attribute OF}, it is
   1.486 +  up to the proof author to guard attribute application with an appropriate
   1.487 +  @{method match}, but there are still no static guarantees.
   1.488 +
   1.489 +  In contrast to @{attribute OF}, the @{attribute "where"} and @{attribute of}
   1.490 +  attributes attempt to provide static guarantees that they will apply
   1.491 +  whenever possible.
   1.492 +
   1.493 +  Within a match pattern for a fact, each outermost quantifier specifies the
   1.494 +  requirement that a matching fact must have a schematic variable at that
   1.495 +  point. This gives a corresponding name to this ``slot'' for the purposes of
   1.496 +  forming a static closure, allowing the @{attribute "where"} attribute to
   1.497 +  perform an instantiation at run-time.
   1.498 +\<close>
   1.499 +
   1.500 +    lemma
   1.501 +      assumes A: "Q \<Longrightarrow> False"
   1.502 +      shows "\<not> Q"
   1.503 +      by (match intros in X: "\<And>P. (P \<Longrightarrow> False) \<Longrightarrow> \<not> P" \<Rightarrow>
   1.504 +            \<open>rule X [where P = Q, OF A]\<close>)
   1.505 +
   1.506 +text \<open>
   1.507 +  Subgoal focusing converts the outermost quantifiers of premises into
   1.508 +  schematics when lifting them to hypothetical facts. This allows us to
   1.509 +  instantiate them with @{attribute "where"} when using an appropriate match
   1.510 +  pattern.
   1.511 +\<close>
   1.512 +
   1.513 +    lemma "(\<And>x :: 'a. A x \<Longrightarrow> B x) \<Longrightarrow> A y \<Longrightarrow> B y"
   1.514 +      by (match premises in I: "\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x" \<Rightarrow>
   1.515 +            \<open>rule I [where x = y]\<close>)
   1.516 +
   1.517 +text \<open>
   1.518 +  The @{attribute of} attribute behaves similarly. It is worth noting,
   1.519 +  however, that the positional instantiation of @{attribute of} occurs against
   1.520 +  the position of the variables as they are declared \emph{in the match
   1.521 +  pattern}.
   1.522 +\<close>
   1.523 +
   1.524 +    lemma
   1.525 +      fixes A B and x :: 'a and y :: 'b
   1.526 +      assumes asm: "(\<And>x y. A y x \<Longrightarrow> B x y )"
   1.527 +      shows "A y x \<Longrightarrow> B x y"
   1.528 +      by (match asm in I: "\<And>(x :: 'a) (y :: 'b). ?P x y \<Longrightarrow> ?Q x y" \<Rightarrow>
   1.529 +            \<open>rule I [of x y]\<close>)
   1.530 +
   1.531 +text \<open>
   1.532 +  In this example, the order of schematics in @{text asm} is actually @{text
   1.533 +  "?y ?x"}, but we instantiate our matched rule in the opposite order. This is
   1.534 +  because the effective rule @{term I} was bound from the match, which
   1.535 +  declared the @{typ 'a} slot first and the @{typ 'b} slot second.
   1.536 +
   1.537 +  To get the dynamic behaviour of @{attribute of} we can choose to invoke it
   1.538 +  \emph{unchecked}. This avoids trying to do any type inference for the
   1.539 +  provided parameters, instead storing them as their most general type and
   1.540 +  doing type matching at run-time. This, like @{attribute OF}, will throw
   1.541 +  errors if the expected slots don't exist or there is a type mismatch.
   1.542 +\<close>
   1.543 +
   1.544 +    lemma
   1.545 +      fixes A B and x :: 'a and y :: 'b
   1.546 +      assumes asm: "\<And>x y. A y x \<Longrightarrow> B x y"
   1.547 +      shows "A y x \<Longrightarrow> B x y"
   1.548 +      by (match asm in I: "PROP ?P" \<Rightarrow> \<open>rule I [of (unchecked) y x]\<close>)
   1.549 +
   1.550 +text \<open>
   1.551 +  Attributes may be applied to matched facts directly as they are matched. Any
   1.552 +  declarations will therefore be applied in the context of the inner method,
   1.553 +  as well as any transformations to the rule.
   1.554 +\<close>
   1.555 +
   1.556 +    lemma "(\<And>x :: 'a. A x \<Longrightarrow> B x) \<Longrightarrow> A y \<longrightarrow> B y"
   1.557 +      by (match premises in I[of y, intros]: "\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x" \<Rightarrow>
   1.558 +            \<open>prop_solver\<close>)
   1.559 +
   1.560 +text \<open>
   1.561 +  In this example, the pattern @{text "\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x"} matches against
   1.562 +  the only premise, giving an appropriately typed slot for @{term y}. After
   1.563 +  the match, the resulting rule is instantiated to @{term y} and then declared
   1.564 +  as an @{attribute intros} rule. This is then picked up by @{method
   1.565 +  prop_solver} to solve the goal.
   1.566 +\<close>
   1.567 +
   1.568 +
   1.569 +section \<open>Multi-match \label{sec:multi}\<close>
   1.570 +
   1.571 +text \<open>
   1.572 +  In all previous examples, @{method match} was only ever searching for a
   1.573 +  single rule or premise. Each local fact would therefore always have a length
   1.574 +  of exactly one. We may, however, wish to find \emph{all} matching results.
   1.575 +  To achieve this, we can simply mark a given pattern with the @{text
   1.576 +  "(multi)"} argument.
   1.577 +\<close>
   1.578 +
   1.579 +    lemma
   1.580 +      assumes asms: "A \<Longrightarrow> B" "A \<Longrightarrow> D"
   1.581 +      shows "(A \<longrightarrow> B) \<and> (A \<longrightarrow> D)"
   1.582 +      apply (match asms in I[intros]: "?P \<Longrightarrow> ?Q"  \<Rightarrow> \<open>solves \<open>prop_solver\<close>\<close>)?
   1.583 +      by (match asms in I[intros]: "?P \<Longrightarrow> ?Q" (multi) \<Rightarrow> \<open>prop_solver\<close>)
   1.584 +
   1.585 +text \<open>
   1.586 +  In the first @{method match}, without the @{text "(multi)"} argument, @{term
   1.587 +  I} is only ever be bound to one of the members of @{text asms}. This
   1.588 +  backtracks over both possibilities (see next section), however neither
   1.589 +  assumption in isolation is sufficient to solve to goal. The use of the
   1.590 +  @{method solves} combinator ensures that @{method prop_solver} has no effect
   1.591 +  on the goal when it doesn't solve it, and so the first match leaves the goal
   1.592 +  unchanged. In the second @{method match}, @{text I} is bound to all of
   1.593 +  @{text asms}, declaring both results as @{text intros}. With these rules
   1.594 +  @{method prop_solver} is capable of solving the goal.
   1.595 +
   1.596 +  Using for-fixed variables in patterns imposes additional constraints on the
   1.597 +  results. In all previous examples, the choice of using @{text ?P} or a
   1.598 +  for-fixed @{term P} only depended on whether or not @{term P} was mentioned
   1.599 +  in another pattern or the inner method. When using a multi-match, however,
   1.600 +  all for-fixed terms must agree in the results.
   1.601 +\<close>
   1.602 +
   1.603 +    lemma
   1.604 +      assumes asms: "A \<Longrightarrow> B" "A \<Longrightarrow> D" "D \<Longrightarrow> B"
   1.605 +      shows "(A \<longrightarrow> B) \<and> (A \<longrightarrow> D)"
   1.606 +      apply (match asms in I[intros]: "?P \<Longrightarrow> Q" (multi) for Q \<Rightarrow>
   1.607 +              \<open>solves \<open>prop_solver\<close>\<close>)?
   1.608 +      by (match asms in I[intros]: "P \<Longrightarrow> ?Q" (multi) for P \<Rightarrow>
   1.609 +              \<open>prop_solver\<close>)
   1.610 +
   1.611 +text \<open>
   1.612 +  Here we have two seemingly-equivalent applications of @{method match},
   1.613 +  however only the second one is capable of solving the goal. The first
   1.614 +  @{method match} selects the first and third members of @{text asms} (those
   1.615 +  that agree on their conclusion), which is not sufficient. The second
   1.616 +  @{method match} selects the first and second members of @{text asms} (those
   1.617 +  that agree on their assumption), which is enough for @{method prop_solver}
   1.618 +  to solve the goal.
   1.619 +\<close>
   1.620 +
   1.621 +
   1.622 +section \<open>Dummy patterns\<close>
   1.623 +
   1.624 +text \<open>
   1.625 +  Dummy patterns may be given as placeholders for unique schematics in
   1.626 +  patterns. They implicitly receive all currently bound variables as
   1.627 +  arguments, and are coerced into the @{typ prop} type whenever possible. For
   1.628 +  example, the trivial dummy pattern @{text "_"} will match any proposition.
   1.629 +  In contrast, by default the pattern @{text "?P"} is considered to have type
   1.630 +  @{typ bool}. It will not bind anything with meta-logical connectives (e.g.
   1.631 +  @{text "_ \<Longrightarrow> _"} or @{text "_ &&& _"}).
   1.632 +\<close>
   1.633 +
   1.634 +    lemma
   1.635 +      assumes asms: "A &&& B \<Longrightarrow> D"
   1.636 +      shows "(A \<and> B \<longrightarrow> D)"
   1.637 +      by (match asms in I:_ \<Rightarrow> \<open>prop_solver intros: I conjunctionI\<close>)
   1.638 +
   1.639 +
   1.640 +section \<open>Backtracking\<close>
   1.641 +
   1.642 +text \<open>
   1.643 +  Patterns are considered top-down, executing the inner method @{text m} of
   1.644 +  the first pattern which is satisfied by the current match target. By
   1.645 +  default, matching performs extensive backtracking by attempting all valid
   1.646 +  variable and fact bindings according to the given pattern. In particular,
   1.647 +  all unifiers for a given pattern will be explored, as well as each matching
   1.648 +  fact. The inner method @{text m} will be re-executed for each different
   1.649 +  variable/fact binding during backtracking. A successful match is considered
   1.650 +  a cut-point for backtracking. Specifically, once a match is made no other
   1.651 +  pattern-method pairs will be considered.
   1.652 +
   1.653 +  The method @{text foo} below fails for all goals that are conjunctions. Any
   1.654 +  such goal will match the first pattern, causing the second pattern (that
   1.655 +  would otherwise match all goals) to never be considered. If multiple
   1.656 +  unifiers exist for the pattern @{text "?P \<and> ?Q"} against the current goal,
   1.657 +  then the failing method @{method fail} will be (uselessly) tried for all of
   1.658 +  them.
   1.659 +\<close>
   1.660 +
   1.661 +    method foo =
   1.662 +      (match conclusion in "?P \<and> ?Q" \<Rightarrow> \<open>fail\<close> \<bar> "?R" \<Rightarrow> \<open>prop_solver\<close>)
   1.663 +
   1.664 +text \<open>
   1.665 +  This behaviour is in direct contrast to the backtracking done by Coq's Ltac,
   1.666 +  which will attempt all patterns in a match before failing. This means that
   1.667 +  the failure of an inner method that is executed after a successful match
   1.668 +  does not, in Ltac, cause the entire match to fail, whereas it does in
   1.669 +  Eisbach. In Eisbach the distinction is important due to the pervasive use of
   1.670 +  backtracking. When a method is used in a combinator chain, its failure
   1.671 +  becomes significant because it signals previously applied methods to move to
   1.672 +  the next result. Therefore, it is necessary for @{method match} to not mask
   1.673 +  such failure. One can always rewrite a match using the combinators ``@{text
   1.674 +  "?"}'' and ``@{text "|"}'' to try subsequent patterns in the case of an
   1.675 +  inner-method failure. The following proof method, for example, always
   1.676 +  invokes @{method prop_solver} for all goals because its first alternative
   1.677 +  either never matches or (if it does match) always fails.
   1.678 +\<close>
   1.679 +
   1.680 +    method foo\<^sub>1 =
   1.681 +      (match conclusion in "?P \<and> ?Q" \<Rightarrow> \<open>fail\<close>) |
   1.682 +      (match conclusion in "?R" \<Rightarrow> \<open>prop_solver\<close>)
   1.683 +
   1.684 +
   1.685 +subsection \<open>Cut\<close>
   1.686 +
   1.687 +text \<open>
   1.688 +  Backtracking may be controlled more precisely by marking individual patterns
   1.689 +  as \emph{cut}. This causes backtracking to not progress beyond this pattern:
   1.690 +  once a match is found no others will be considered.
   1.691 +\<close>
   1.692 +
   1.693 +    method foo\<^sub>2 =
   1.694 +      (match premises in I: "P \<and> Q" (cut) and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow>
   1.695 +        \<open>rule mp [OF I' I [THEN conjunct1]]\<close>)
   1.696 +
   1.697 +text \<open>
   1.698 +  In this example, once a conjunction is found (@{term "P \<and> Q"}), all possible
   1.699 +  implications of @{term "P"} in the premises are considered, evaluating the
   1.700 +  inner @{method rule} with each consequent. No other conjunctions will be
   1.701 +  considered, with method failure occurring once all implications of the
   1.702 +  form @{text "P \<longrightarrow> ?U"} have been explored. Here the left-right processing of
   1.703 +  individual patterns is important, as all patterns after of the cut will
   1.704 +  maintain their usual backtracking behaviour.
   1.705 +\<close>
   1.706 +
   1.707 +    lemma "A \<and> B \<Longrightarrow> A \<longrightarrow> D \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> C"
   1.708 +      by foo\<^sub>2
   1.709 +
   1.710 +    lemma "C \<and> D \<Longrightarrow> A \<and> B \<Longrightarrow> A \<longrightarrow> C  \<Longrightarrow> C"
   1.711 +      by (foo\<^sub>2 | prop_solver)
   1.712 +
   1.713 +text \<open>
   1.714 +  In this example, the first lemma is solved by @{text foo\<^sub>2}, by first
   1.715 +  picking @{term "A \<longrightarrow> D"} for @{text I'}, then backtracking and ultimately
   1.716 +  succeeding after picking @{term "A \<longrightarrow> C"}. In the second lemma, however,
   1.717 +  @{term "C \<and> D"} is matched first, the second pattern in the match cannot be
   1.718 +  found and so the method fails, falling through to @{method prop_solver}.
   1.719 +\<close>
   1.720 +
   1.721 +
   1.722 +subsection \<open>Multi-match revisited\<close>
   1.723 +
   1.724 +text \<open>
   1.725 +  A multi-match will produce a sequence of potential bindings for for-fixed
   1.726 +  variables, where each binding environment is the result of matching against
   1.727 +  at least one element from the match target. For each environment, the match
   1.728 +  result will be all elements of the match target which agree with the pattern
   1.729 +  under that environment. This can result in unexpected behaviour when giving
   1.730 +  very general patterns.
   1.731 +\<close>
   1.732 +
   1.733 +    lemma
   1.734 +      assumes asms: "\<And>x. A x \<and> B x" "\<And>y. A y \<and> C y" "\<And>z. B z \<and> C z"
   1.735 +      shows "A x \<and> C x"
   1.736 +      by (match asms in I: "\<And>x. P x \<and> ?Q x" (multi) for P \<Rightarrow>
   1.737 +         \<open>match (P) in "A" \<Rightarrow> \<open>fail\<close>
   1.738 +                       \<bar> _ \<Rightarrow> \<open>match I in "\<And>x. A x \<and> B x" \<Rightarrow> \<open>fail\<close>
   1.739 +                                                      \<bar> _ \<Rightarrow> \<open>rule I\<close>\<close>\<close>)
   1.740 +
   1.741 +text \<open>
   1.742 +  Intuitively it seems like this proof should fail to check. The first match
   1.743 +  result, which binds @{term I} to the first two members of @{text asms},
   1.744 +  fails the second inner match due to binding @{term P} to @{term A}.
   1.745 +  Backtracking then attempts to bind @{term I} to the third member of @{text
   1.746 +  asms}. This passes all inner matches, but fails when @{method rule} cannot
   1.747 +  successfully apply this to the current goal. After this, a valid match that
   1.748 +  is produced by the unifier is one which binds @{term P} to simply @{text
   1.749 +  "\<lambda>a. A ?x"}. The first inner match succeeds because @{text "\<lambda>a. A ?x"} does
   1.750 +  not match @{term A}. The next inner match succeeds because @{term I} has
   1.751 +  only been bound to the first member of @{text asms}. This is due to @{method
   1.752 +  match} considering @{text "\<lambda>a. A ?x"} and @{text "\<lambda>a. A ?y"} as distinct
   1.753 +  terms.
   1.754 +
   1.755 +  The simplest way to address this is to explicitly disallow term bindings
   1.756 +  which we would consider invalid.
   1.757 +\<close>
   1.758 +
   1.759 +    method abs_used for P =
   1.760 +      (match (P) in "\<lambda>a. ?P" \<Rightarrow> \<open>fail\<close> \<bar> _ \<Rightarrow> \<open>-\<close>)
   1.761 +
   1.762 +text \<open>
   1.763 +  This method has no effect on the goal state, but instead serves as a filter
   1.764 +  on the environment produced from match.
   1.765 +\<close>
   1.766 +
   1.767 +
   1.768 +section \<open>Uncurrying\<close>
   1.769 +
   1.770 +text \<open>
   1.771 +  The @{method match} method is not aware of the logical content of match
   1.772 +  targets. Each pattern is simply matched against the shallow structure of a
   1.773 +  fact or term. Most facts are in \emph{normal form}, which curries premises
   1.774 +  via meta-implication @{text "_ \<Longrightarrow> _"}.
   1.775 +\<close>
   1.776 +
   1.777 +    lemma
   1.778 +      assumes asms: "D \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> A"
   1.779 +      shows "D \<Longrightarrow> B \<Longrightarrow> C \<and> A"
   1.780 +      by (match asms in H:"D \<Longrightarrow> _" (multi) \<Rightarrow> \<open>prop_solver elims: H\<close>)
   1.781 +
   1.782 +text \<open>
   1.783 +  For the first member of @{text asms} the dummy pattern successfully matches
   1.784 +  against @{term "B \<Longrightarrow> C"} and so the proof is successful.
   1.785 +\<close>
   1.786 +
   1.787 +    lemma
   1.788 +      assumes asms: "A \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> C"
   1.789 +      shows "D \<or> (A \<and> B) \<Longrightarrow> C"
   1.790 +      apply (match asms in H:"_ \<Longrightarrow> C" (multi) \<Rightarrow> \<open>prop_solver elims: H\<close>)(*<*)?
   1.791 +      by (prop_solver elims: asms)(*>*)
   1.792 +
   1.793 +text \<open>
   1.794 +  This proof will fail to solve the goal. Our match pattern will only match
   1.795 +  rules which have a single premise, and conclusion @{term C}, so the first
   1.796 +  member of @{text asms} is not bound and thus the proof fails. Matching a
   1.797 +  pattern of the form @{term "P \<Longrightarrow> Q"} against this fact will bind @{term "P"}
   1.798 +  to @{term "A"} and @{term Q} to @{term "B \<Longrightarrow> C"}. Our pattern, with a
   1.799 +  concrete @{term "C"} in the conclusion, will fail to match this fact.
   1.800 +
   1.801 +  To express our desired match, we may \emph{uncurry} our rules before
   1.802 +  matching against them. This forms a meta-conjunction of all premises in a
   1.803 +  fact, so that only one implication remains. For example the uncurried
   1.804 +  version of @{term "A \<Longrightarrow> B \<Longrightarrow> C"} is @{term "A &&& B \<Longrightarrow> C"}. This will now match
   1.805 +  our desired pattern @{text "_ \<Longrightarrow> C"}, and can be \emph{curried} after the
   1.806 +  match to put it back into normal form.
   1.807 +\<close>
   1.808 +
   1.809 +    lemma
   1.810 +      assumes asms: "A \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> C"
   1.811 +      shows "D \<or> (A \<and> B) \<Longrightarrow> C"
   1.812 +      by (match asms[uncurry] in H[curry]:"_ \<Longrightarrow> C" (multi) \<Rightarrow>
   1.813 +          \<open>prop_solver elims: H\<close>)
   1.814 +
   1.815 +
   1.816 +section \<open>Reverse matching\<close>
   1.817 +
   1.818 +text \<open>
   1.819 +  The @{method match} method only attempts to perform matching of the pattern
   1.820 +  against the match target. Specifically this means that it will not
   1.821 +  instantiate schematic terms in the match target.
   1.822 +\<close>
   1.823 +
   1.824 +    lemma
   1.825 +      assumes asms: "\<And>x :: 'a. A x"
   1.826 +      shows "A y"
   1.827 +      apply (match asms in H:"A y" \<Rightarrow> \<open>rule H\<close>)?
   1.828 +      by (match asms in H:"P" for P \<Rightarrow>
   1.829 +          \<open>match ("A y") in "P" \<Rightarrow> \<open>rule H\<close>\<close>)
   1.830 +
   1.831 +text \<open>
   1.832 +  In the first @{method match} we attempt to find a member of @{text asms}
   1.833 +  which matches our goal precisely. This fails due to no such member existing.
   1.834 +  The second match reverses the role of the fact in the match, by first giving
   1.835 +  a general pattern @{term P}. This bound pattern is then matched against
   1.836 +  @{term "A y"}. In this case, @{term P} is bound to @{text "A ?x"} and so it
   1.837 +  successfully matches.
   1.838 +\<close>
   1.839 +
   1.840 +
   1.841 +section \<open>Type matching\<close>
   1.842 +
   1.843 +text \<open>
   1.844 +  The rule instantiation attributes @{attribute "where"} and @{attribute "of"}
   1.845 +  attempt to guarantee type-correctness wherever possible. This can require
   1.846 +  additional invocations of @{method match} in order to statically ensure that
   1.847 +  instantiation will succeed.
   1.848 +\<close>
   1.849 +
   1.850 +    lemma
   1.851 +      assumes asms: "\<And>x :: 'a. A x"
   1.852 +      shows "A y"
   1.853 +      by (match asms in H:"\<And>z :: 'b. P z" for P \<Rightarrow>
   1.854 +          \<open>match (y) in "y :: 'b" for y \<Rightarrow> \<open>rule H[where z=y]\<close>\<close>)
   1.855 +
   1.856 +text \<open>
   1.857 +  In this example the type @{text 'b} is matched to @{text 'a}, however
   1.858 +  statically they are formally distinct types. The first match binds @{text
   1.859 +  'b} while the inner match serves to coerce @{term y} into having the type
   1.860 +  @{text 'b}. This allows the rule instantiation to successfully apply.
   1.861 +\<close>
   1.862 +
   1.863 +
   1.864 +chapter \<open>Method development\<close>
   1.865 +
   1.866 +section \<open>Tracing methods\<close>
   1.867 +
   1.868 +text \<open>
   1.869 +  Method tracing is supported by auxiliary print methods provided by @{theory
   1.870 +  Eisbach_Tools}. These include @{method print_fact}, @{method print_term} and
   1.871 +  @{method print_type}. Whenever a print method is evaluated it leaves the
   1.872 +  goal unchanged and writes its argument as tracing output.
   1.873 +
   1.874 +  Print methods can be combined with the @{method fail} method to investigate
   1.875 +  the backtracking behaviour of a method.
   1.876 +\<close>
   1.877 +
   1.878 +    lemma
   1.879 +      assumes asms: A B C D
   1.880 +      shows D
   1.881 +      apply (match asms in H:_ \<Rightarrow> \<open>print_fact H, fail\<close>)(*<*)?
   1.882 +      by (simp add: asms)(*>*)
   1.883 +
   1.884 +text \<open>
   1.885 +  This proof will fail, but the tracing output will show the order that the
   1.886 +  assumptions are attempted.
   1.887 +\<close>
   1.888 +
   1.889 +
   1.890 +section \<open>Integrating with Isabelle/ML\<close>
   1.891 +
   1.892 +subsection \<open>Attributes\<close>
   1.893 +
   1.894 +text \<open>
   1.895 +  A custom rule attribute is a simple way to extend the functionality of
   1.896 +  Eisbach methods. The dummy rule attribute notation (@{text "[[ _ ]]"})
   1.897 +  invokes the given attribute against a dummy fact and evaluates to the result
   1.898 +  of that attribute. When used as a match target, this can serve as an
   1.899 +  effective auxiliary function.
   1.900 +\<close>
   1.901 +
   1.902 +    attribute_setup get_split_rule =
   1.903 +      \<open>Args.term >> (fn t =>
   1.904 +        Thm.rule_attribute (fn context => fn _ =>
   1.905 +          (case get_split_rule (Context.proof_of context) t of
   1.906 +            SOME thm => thm
   1.907 +          | NONE => Drule.dummy_thm)))\<close>
   1.908 +
   1.909 +text \<open>
   1.910 +  In this example, the new attribute @{attribute get_split_rule} lifts the ML
   1.911 +  function of the same name into an attribute. When applied to a cast
   1.912 +  distinction over a datatype, it retrieves its corresponding split rule.
   1.913 +
   1.914 +  We can then integrate this intro a method that applies the split rule, fist
   1.915 +  matching to ensure that fetching the rule was successful.
   1.916 +\<close>
   1.917 +
   1.918 +    method splits =
   1.919 +      (match conclusion in "?P f" for f \<Rightarrow>
   1.920 +        \<open>match [[get_split_rule f]] in U: "(_ :: bool) = _" \<Rightarrow>
   1.921 +          \<open>rule U[THEN iffD2]\<close>\<close>)
   1.922 +
   1.923 +    lemma "L \<noteq> [] \<Longrightarrow> case L of [] \<Rightarrow> False | _ \<Rightarrow> True"
   1.924 +      by (splits, prop_solver intros: allI)
   1.925 +
   1.926 +end