added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
authorwenzelm
Sun May 17 23:03:49 2015 +0200 (2015-05-17)
changeset 60288d7f636331176
parent 60287 adde5ce1e0a7
child 60289 1fb026be7536
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
NEWS
doc/Contents
src/Doc/Eisbach/Base.thy
src/Doc/Eisbach/Manual.thy
src/Doc/Eisbach/Preface.thy
src/Doc/Eisbach/document/build
src/Doc/Eisbach/document/root.tex
src/Doc/Eisbach/document/style.sty
src/Doc/ROOT
     1.1 --- a/NEWS	Sun May 17 22:33:34 2015 +0200
     1.2 +++ b/NEWS	Sun May 17 23:03:49 2015 +0200
     1.3 @@ -63,8 +63,9 @@
     1.4  by combining existing ones with their usual syntax. The "match" proof
     1.5  method provides basic fact/term matching in addition to
     1.6  premise/conclusion matching through Subgoal.focus, and binds fact names
     1.7 -from matches as well as term patterns within matches. See also
     1.8 -~~/src/HOL/Eisbach/Eisbach.thy and the included examples.
     1.9 +from matches as well as term patterns within matches. The Isabelle
    1.10 +documentation provides an entry "eisbach" for the Eisbach User Manual.
    1.11 +Sources and various examples are in ~~/src/HOL/Eisbach/.
    1.12  
    1.13  
    1.14  *** Prover IDE -- Isabelle/Scala/jEdit ***
     2.1 --- a/doc/Contents	Sun May 17 22:33:34 2015 +0200
     2.2 +++ b/doc/Contents	Sun May 17 23:03:49 2015 +0200
     2.3 @@ -8,6 +8,7 @@
     2.4    codegen         Tutorial on Code Generation
     2.5    nitpick         User's Guide to Nitpick
     2.6    sledgehammer    User's Guide to Sledgehammer
     2.7 +  eisbach         The Eisbach User Manual
     2.8    sugar           LaTeX Sugar for Isabelle documents
     2.9  
    2.10  Reference Manuals!
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Doc/Eisbach/Base.thy	Sun May 17 23:03:49 2015 +0200
     3.3 @@ -0,0 +1,39 @@
     3.4 +section \<open>Basic setup that is not included in the document\<close>
     3.5 +
     3.6 +theory Base
     3.7 +imports Main
     3.8 +begin
     3.9 +
    3.10 +ML_file "~~/src/Doc/antiquote_setup.ML"
    3.11 +
    3.12 +ML\<open>
    3.13 +fun get_split_rule ctxt target =
    3.14 +  let
    3.15 +    val (head, args) = strip_comb (Envir.eta_contract target);
    3.16 +    val (const_name, _) = dest_Const head;
    3.17 +    val const_name_components = Long_Name.explode const_name;
    3.18 +
    3.19 +    val _ =
    3.20 +      if String.isPrefix "case_" (List.last const_name_components) then ()
    3.21 +      else raise TERM ("Not a case statement", [target]);
    3.22 +
    3.23 +    val type_name = Long_Name.implode (rev (tl (rev const_name_components)));
    3.24 +    val split = Proof_Context.get_thm ctxt (type_name ^ ".split");
    3.25 +    val vars = Term.add_vars (Thm.prop_of split) [];
    3.26 +
    3.27 +    val datatype_name = nth (rev const_name_components) 1;
    3.28 +
    3.29 +    fun is_datatype (Type (a, _)) = Long_Name.base_name a = Long_Name.base_name datatype_name
    3.30 +      | is_datatype _ = false;
    3.31 +
    3.32 +    val datatype_var =
    3.33 +      (case find_first (fn (_, T') => is_datatype T') vars of
    3.34 +        SOME var => Thm.cterm_of ctxt (Term.Var var)
    3.35 +      | NONE => error ("Couldn't find datatype in thm: " ^ datatype_name));
    3.36 +  in
    3.37 +    SOME (Drule.cterm_instantiate [(datatype_var, Thm.cterm_of ctxt (List.last args))] split)
    3.38 +  end
    3.39 +  handle TERM _ => NONE;
    3.40 +\<close>
    3.41 +
    3.42 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Doc/Eisbach/Manual.thy	Sun May 17 23:03:49 2015 +0200
     4.3 @@ -0,0 +1,923 @@
     4.4 +(*:wrap=hard:maxLineLen=78:*)
     4.5 +
     4.6 +theory Manual
     4.7 +imports Base "../Eisbach_Tools"
     4.8 +begin
     4.9 +
    4.10 +chapter \<open>The method command\<close>
    4.11 +
    4.12 +text \<open>
    4.13 +  The @{command_def method} command provides the ability to write proof
    4.14 +  methods by combining existing ones with their usual syntax. Specifically it
    4.15 +  allows compound proof methods to be named, and to extend the name space of
    4.16 +  basic methods accordingly. Method definitions may abstract over parameters:
    4.17 +  terms, facts, or other methods.
    4.18 +
    4.19 +  \medskip The syntax diagram below refers to some syntactic categories that
    4.20 +  are further defined in @{cite "isabelle-isar-ref"}.
    4.21 +
    4.22 +  @{rail \<open>
    4.23 +    @@{command method} name args @'=' method
    4.24 +    ;
    4.25 +    args: term_args? method_args? \<newline> fact_args? decl_args?
    4.26 +    ;
    4.27 +    term_args: @'for' @{syntax "fixes"}
    4.28 +    ;
    4.29 +    method_args: @'methods' (name+)
    4.30 +    ;
    4.31 +    fact_args: @'uses' (name+)
    4.32 +    ;
    4.33 +    decl_args: @'declares' (name+)
    4.34 +  \<close>}
    4.35 +\<close>
    4.36 +
    4.37 +
    4.38 +section \<open>Basic method definitions\<close>
    4.39 +
    4.40 +text \<open>
    4.41 +  Consider the following proof that makes use of usual Isar method
    4.42 +  combinators.
    4.43 +\<close>
    4.44 +
    4.45 +    lemma "P \<and> Q \<longrightarrow> P"
    4.46 +      by ((rule impI, (erule conjE)?) | assumption)+
    4.47 +
    4.48 +text \<open>
    4.49 +  It is clear that this compound method will be applicable in more cases than
    4.50 +  this proof alone. With the @{command method} command we can define a proof
    4.51 +  method that makes the above functionality available generally.
    4.52 +\<close>
    4.53 +
    4.54 +    method prop_solver\<^sub>1 =
    4.55 +      ((rule impI, (erule conjE)?) | assumption)+
    4.56 +
    4.57 +    lemma "P \<and> Q \<and> R \<longrightarrow> P"
    4.58 +      by prop_solver\<^sub>1
    4.59 +
    4.60 +text \<open>
    4.61 +  In this example, the facts @{text impI} and @{text conjE} are static. They
    4.62 +  are evaluated once when the method is defined and cannot be changed later.
    4.63 +  This makes the method stable in the sense of \emph{static scoping}: naming
    4.64 +  another fact @{text impI} in a later context won't affect the behaviour of
    4.65 +  @{text "prop_solver\<^sub>1"}.
    4.66 +\<close>
    4.67 +
    4.68 +
    4.69 +section \<open>Term abstraction\<close>
    4.70 +
    4.71 +text \<open>
    4.72 +  Methods can also abstract over terms using the @{keyword_def "for"} keyword,
    4.73 +  optionally providing type constraints. For instance, the following proof
    4.74 +  method @{text intro_ex} takes a term @{term y} of any type, which it uses to
    4.75 +  instantiate the @{term x}-variable of @{text exI} (existential introduction)
    4.76 +  before applying the result as a rule. The instantiation is performed here by
    4.77 +  Isar's @{attribute_ref "where"} attribute. If the current subgoal is to find
    4.78 +  a witness for the given predicate @{term Q}, then this has the effect of
    4.79 +  committing to @{term y}.
    4.80 +\<close>
    4.81 +
    4.82 +    method intro_ex for Q :: "'a \<Rightarrow> bool" and y :: 'a =
    4.83 +      (rule exI ["where" P = Q and x = y])
    4.84 +
    4.85 +
    4.86 +text \<open>
    4.87 +  The term parameters @{term y} and @{term Q} can be used arbitrarily inside
    4.88 +  the method body, as part of attribute applications or arguments to other
    4.89 +  methods. The expression is type-checked as far as possible when the method
    4.90 +  is defined, however dynamic type errors can still occur when it is invoked
    4.91 +  (e.g.\ when terms are instantiated in a parameterized fact). Actual term
    4.92 +  arguments are supplied positionally, in the same order as in the method
    4.93 +  definition.
    4.94 +\<close>
    4.95 +
    4.96 +    lemma "P a \<Longrightarrow> \<exists>x. P x"
    4.97 +      by (intro_ex P a)
    4.98 +
    4.99 +
   4.100 +section \<open>Fact abstraction\<close>
   4.101 +
   4.102 +subsection \<open>Named theorems\<close>
   4.103 +
   4.104 +text \<open>
   4.105 +  A @{text "named theorem"} is a fact whose contents are produced dynamically
   4.106 +  within the current proof context. The Isar command @{command_ref
   4.107 +  "named_theorems"} provides simple access to this concept: it declares a
   4.108 +  dynamic fact with corresponding \emph{attribute}
   4.109 +  (see \autoref{s:attributes}) for managing this particular data slot in the
   4.110 +  context.
   4.111 +\<close>
   4.112 +
   4.113 +    named_theorems intros
   4.114 +
   4.115 +text \<open>
   4.116 +  So far @{text "intros"} refers to the empty fact. Using the Isar command
   4.117 +  @{command_ref "declare"} we may apply declaration attributes to the context.
   4.118 +  Below we declare both @{text "conjI"} and @{text "impI"} as @{text
   4.119 +  "intros"}, adding them to the named theorem slot.
   4.120 +\<close>
   4.121 +
   4.122 +    declare conjI [intros] and impI [intros]
   4.123 +
   4.124 +text \<open>
   4.125 +  We can refer to named theorems as dynamic facts within a particular proof
   4.126 +  context, which are evaluated whenever the method is invoked. Instead of
   4.127 +  having facts hard-coded into the method, as in @{text prop_solver\<^sub>1}, we can
   4.128 +  instead refer to these named theorems.
   4.129 +\<close>
   4.130 +
   4.131 +    named_theorems elims
   4.132 +    declare conjE [elims]
   4.133 +
   4.134 +    method prop_solver\<^sub>3 =
   4.135 +      ((rule intros, (erule elims)?) | assumption)+
   4.136 +
   4.137 +    lemma "P \<and> Q \<longrightarrow> P"
   4.138 +      by prop_solver\<^sub>3
   4.139 +
   4.140 +text \<open>
   4.141 +  Often these named theorems need to be augmented on the spot, when a method
   4.142 +  is invoked. The @{keyword_def "declares"} keyword in the signature of
   4.143 +  @{command method} adds the common method syntax @{text "method decl: facts"}
   4.144 +  for each named theorem @{text decl}.
   4.145 +\<close>
   4.146 +
   4.147 +    method prop_solver\<^sub>4 declares intros elims =
   4.148 +      ((rule intros, (erule elims)?) | assumption)+
   4.149 +
   4.150 +    lemma "P \<and> (P \<longrightarrow> Q) \<longrightarrow> Q \<and> P"
   4.151 +      by (prop_solver\<^sub>4 elims: impE intros: conjI)
   4.152 +
   4.153 +
   4.154 +subsection \<open>Simple fact abstraction\<close>
   4.155 +
   4.156 +text \<open>
   4.157 +  The @{keyword "declares"} keyword requires that a corresponding dynamic fact
   4.158 +  has been declared with @{command_ref named_theorems}. This is useful for
   4.159 +  managing collections of facts which are to be augmented with declarations,
   4.160 +  but is overkill if we simply want to pass a fact to a method.
   4.161 +
   4.162 +  We may use the @{keyword_def "uses"} keyword in the method header to provide
   4.163 +  a simple fact parameter. In contrast to @{keyword "declares"}, these facts
   4.164 +  are always implicitly empty unless augmented when the method is invoked.
   4.165 +\<close>
   4.166 +
   4.167 +    method rule_twice uses my_rule =
   4.168 +      (rule my_rule, rule my_rule)
   4.169 +
   4.170 +    lemma "P \<Longrightarrow> Q \<Longrightarrow> (P \<and> Q) \<and> Q"
   4.171 +      by (rule_twice my_rule: conjI)
   4.172 +
   4.173 +
   4.174 +section \<open>Higher-order methods\<close>
   4.175 +
   4.176 +text \<open>
   4.177 +  The \emph{structured concatenation} combinator ``@{text "method\<^sub>1 ;
   4.178 +  method\<^sub>2"}'' was introduced in Isabelle2015, motivated by development of
   4.179 +  Eisbach. It is similar to ``@{text "method\<^sub>1, method\<^sub>2"}'', but @{text
   4.180 +  method\<^sub>2} is invoked on on \emph{all} subgoals that have newly emerged from
   4.181 +  @{text method\<^sub>1}. This is useful to handle cases where the number of
   4.182 +  subgoals produced by a method is determined dynamically at run-time.
   4.183 +\<close>
   4.184 +
   4.185 +    method conj_with uses rule =
   4.186 +      (intro conjI ; intro rule)
   4.187 +
   4.188 +    lemma
   4.189 +      assumes A: "P"
   4.190 +      shows "P \<and> P \<and> P"
   4.191 +      by (conj_with rule: A)
   4.192 +
   4.193 +text \<open>
   4.194 +  Method definitions may take other methods as arguments, and thus implement
   4.195 +  method combinators with prefix syntax. For example, to more usefully exploit
   4.196 +  Isabelle's backtracking, the explicit requirement that a method solve all
   4.197 +  produced subgoals is frequently useful. This can easily be written as a
   4.198 +  \emph{higher-order method} using ``@{text ";"}''. The @{keyword "methods"}
   4.199 +  keyword denotes method parameters that are other proof methods to be invoked
   4.200 +  by the method being defined.
   4.201 +\<close>
   4.202 +
   4.203 +    method solve methods m = (m ; fail)
   4.204 +
   4.205 +text \<open>
   4.206 +  Given some method-argument @{text m}, @{text "solve \<open>m\<close>"} applies the
   4.207 +  method @{text m} and then fails whenever @{text m} produces any new unsolved
   4.208 +  subgoals --- i.e. when @{text m} fails to completely discharge the goal it
   4.209 +  was applied to.
   4.210 +\<close>
   4.211 +
   4.212 +
   4.213 +section \<open>Example\<close>
   4.214 +
   4.215 +text \<open>
   4.216 +  With these simple features we are ready to write our first non-trivial proof
   4.217 +  method. Returning to the first-order logic example, the following method
   4.218 +  definition applies various rules with their canonical methods.
   4.219 +\<close>
   4.220 +
   4.221 +    named_theorems subst
   4.222 +
   4.223 +    method prop_solver declares intros elims subst =
   4.224 +      (assumption |
   4.225 +        (rule intros) | erule elims |
   4.226 +        subst subst | subst (asm) subst |
   4.227 +        (erule notE ; solve \<open>prop_solver\<close>))+
   4.228 +
   4.229 +text \<open>
   4.230 +  The only non-trivial part above is the final alternative @{text "(erule notE
   4.231 +  ; solve \<open>prop_solver\<close>)"}. Here, in the case that all other alternatives
   4.232 +  fail, the method takes one of the assumptions @{term "\<not> P"} of the current
   4.233 +  goal and eliminates it with the rule @{text notE}, causing the goal to be
   4.234 +  proved to become @{term P}. The method then recursively invokes itself on
   4.235 +  the remaining goals. The job of the recursive call is to demonstrate that
   4.236 +  there is a contradiction in the original assumptions (i.e.\ that @{term P}
   4.237 +  can be derived from them). Note this recursive invocation is applied with
   4.238 +  the @{method solve} method combinator to ensure that a contradiction will
   4.239 +  indeed be shown. In the case where a contradiction cannot be found,
   4.240 +  backtracking will occur and a different assumption @{term "\<not> Q"} will be
   4.241 +  chosen for elimination.
   4.242 +
   4.243 +  Note that the recursive call to @{method prop_solver} does not have any
   4.244 +  parameters passed to it. Recall that fact parameters, e.g.\ @{text
   4.245 +  "intros"}, @{text "elims"}, and @{text "subst"}, are managed by declarations
   4.246 +  in the current proof context. They will therefore be passed to any recursive
   4.247 +  call to @{method prop_solver} and, more generally, any invocation of a
   4.248 +  method which declares these named theorems.
   4.249 +
   4.250 +  \medskip After declaring some standard rules to the context, the @{method
   4.251 +  prop_solver} becomes capable of solving non-trivial propositional
   4.252 +  tautologies.\<close>
   4.253 +
   4.254 +    lemmas [intros] =
   4.255 +      conjI  --  \<open>@{thm conjI}\<close>
   4.256 +      impI  --  \<open>@{thm impI}\<close>
   4.257 +      disjCI  --  \<open>@{thm disjCI}\<close>
   4.258 +      iffI  --  \<open>@{thm iffI}\<close>
   4.259 +      notI  --  \<open>@{thm notI}\<close>
   4.260 +      (*<*)TrueI(*>*)
   4.261 +    lemmas [elims] =
   4.262 +      impCE  --  \<open>@{thm impCE}\<close>
   4.263 +      conjE  --  \<open>@{thm conjE}\<close>
   4.264 +      disjE  --  \<open>@{thm disjE}\<close>
   4.265 +
   4.266 +    lemma "(A \<or> B) \<and> (A \<longrightarrow> C) \<and> (B \<longrightarrow> C) \<longrightarrow> C"
   4.267 +      by prop_solver
   4.268 +
   4.269 +
   4.270 +chapter \<open>The match method \label{s:matching}\<close>
   4.271 +
   4.272 +text \<open>
   4.273 +  So far we have seen methods defined as simple combinations of other methods.
   4.274 +  Some familiar programming language concepts have been introduced (i.e.\
   4.275 +  abstraction and recursion). The only control flow has been implicitly the
   4.276 +  result of backtracking. When designing more sophisticated proof methods this
   4.277 +  proves too restrictive and difficult to manage conceptually.
   4.278 +
   4.279 +  To address this, we introduce the @{method_def "match"} method, which
   4.280 +  provides more direct access to the higher-order matching facility at the
   4.281 +  core of Isabelle. It is implemented as a separate proof method (in
   4.282 +  Isabelle/ML), and thus can be directly applied to proofs, however it is most
   4.283 +  useful when applied in the context of writing Eisbach method definitions.
   4.284 +
   4.285 +  \medskip The syntax diagram below refers to some syntactic categories that
   4.286 +  are further defined in @{cite "isabelle-isar-ref"}.
   4.287 +
   4.288 +  @{rail \<open>
   4.289 +    @@{method match} kind @'in' (pattern '\<Rightarrow>' cartouche + '\<bar>')
   4.290 +    ;
   4.291 +    kind:
   4.292 +      (@'conclusion' | @'premises' ('(' 'local' ')')? |
   4.293 +       '(' term ')' | @{syntax thmrefs})
   4.294 +    ;
   4.295 +    pattern: fact_name? term args? \<newline> (@'for' fixes)?
   4.296 +    ;
   4.297 +    fact_name: @{syntax name} @{syntax attributes}? ':'
   4.298 +    ;
   4.299 +    args: '(' (('multi' | 'cut' nat?) + ',') ')'
   4.300 +  \<close>}
   4.301 +
   4.302 +  Matching allows methods to introspect the goal state, and to implement more
   4.303 +  explicit control flow. In the basic case, a term or fact @{text ts} is given
   4.304 +  to match against as a \emph{match target}, along with a collection of
   4.305 +  pattern-method pairs @{text "(p, m)"}: roughly speaking, when the pattern
   4.306 +  @{text p} matches any member of @{text ts}, the \emph{inner} method @{text
   4.307 +  m} will be executed.
   4.308 +\<close>
   4.309 +
   4.310 +    lemma
   4.311 +      assumes X:
   4.312 +        "Q \<longrightarrow> P"
   4.313 +        "Q"
   4.314 +      shows P
   4.315 +        by (match X in I: "Q \<longrightarrow> P" and I': "Q" \<Rightarrow> \<open>insert mp [OF I I']\<close>)
   4.316 +
   4.317 +text \<open>
   4.318 +  In this example we have a structured Isar proof, with the named
   4.319 +  assumption @{text "X"} and a conclusion @{term "P"}. With the match method
   4.320 +  we can find the local facts @{term "Q \<longrightarrow> P"} and @{term "Q"}, binding them to
   4.321 +  separately as @{text "I"} and @{text "I'"}. We then specialize the
   4.322 +  modus-ponens rule @{thm mp [of Q P]} to these facts to solve the goal.
   4.323 +\<close>
   4.324 +
   4.325 +
   4.326 +section \<open>Subgoal focus\<close>
   4.327 +
   4.328 +text\<open>
   4.329 +  In the previous example we were able to match against an assumption out of
   4.330 +  the Isar proof state. In general, however, proof subgoals can be
   4.331 +  \emph{unstructured}, with goal parameters and premises arising from rule
   4.332 +  application. To address this, @{method match} uses \emph{subgoal focusing}
   4.333 +  (see also \autoref{s:design}) to produce structured goals out of
   4.334 +  unstructured ones. In place of fact or term, we may give the
   4.335 +  keyword @{keyword_def "premises"} as the match target. This causes a subgoal
   4.336 +  focus on the first subgoal, lifting local goal parameters to fixed term
   4.337 +  variables and premises into hypothetical theorems. The match is performed
   4.338 +  against these theorems, naming them and binding them as appropriate.
   4.339 +  Similarly giving the keyword @{keyword_def "conclusion"} matches against the
   4.340 +  conclusion of the first subgoal.
   4.341 +
   4.342 +  An unstructured version of the previous example can then be similarly solved
   4.343 +  through focusing.
   4.344 +\<close>
   4.345 +
   4.346 +    lemma "Q \<longrightarrow> P \<Longrightarrow> Q \<Longrightarrow> P"
   4.347 +      by (match premises in
   4.348 +                I: "Q \<longrightarrow> P" and I': "Q" \<Rightarrow> \<open>insert mp [OF I I']\<close>)
   4.349 +
   4.350 +text \<open>
   4.351 +  Match variables may be specified by giving a list of @{keyword_ref
   4.352 +  "for"}-fixes after the pattern description. This marks those terms as bound
   4.353 +  variables, which may be used in the method body.
   4.354 +\<close>
   4.355 +
   4.356 +    lemma "Q \<longrightarrow> P \<Longrightarrow> Q \<Longrightarrow> P"
   4.357 +      by (match premises in I: "Q \<longrightarrow> A" and I': "Q" for A \<Rightarrow>
   4.358 +            \<open>match conclusion in A \<Rightarrow> \<open>insert mp [OF I I']\<close>\<close>)
   4.359 +
   4.360 +text \<open>
   4.361 +  In this example @{term A} is a match variable which is bound to @{term P}
   4.362 +  upon a successful match. The inner @{method match} then matches the
   4.363 +  now-bound @{term A} (bound to @{term P}) against the conclusion (also @{term
   4.364 +  P}), finally applying the specialized rule to solve the goal.
   4.365 +
   4.366 +  Schematic terms like @{text "?P"} may also be used to specify match
   4.367 +  variables, but the result of the match is not bound, and thus cannot be used
   4.368 +  in the inner method body.
   4.369 +
   4.370 +  \medskip In the following example we extract the predicate of an
   4.371 +  existentially quantified conclusion in the current subgoal and search the
   4.372 +  current premises for a matching fact. If both matches are successful, we
   4.373 +  then instantiate the existential introduction rule with both the witness and
   4.374 +  predicate, solving with the matched premise.
   4.375 +\<close>
   4.376 +
   4.377 +    method solve_ex =
   4.378 +      (match conclusion in "\<exists>x. Q x" for Q \<Rightarrow>
   4.379 +        \<open>match premises in U: "Q y" for y \<Rightarrow>
   4.380 +          \<open>rule exI [where P = Q and x = y, OF U]\<close>\<close>)
   4.381 +
   4.382 +text \<open>
   4.383 +  The first @{method match} matches the pattern @{term "\<exists>x. Q x"} against the
   4.384 +  current conclusion, binding the term @{term "Q"} in the inner match. Next
   4.385 +  the pattern @{text "Q y"} is matched against all premises of the current
   4.386 +  subgoal. In this case @{term "Q"} is fixed and @{term "y"} may be
   4.387 +  instantiated. Once a match is found, the local fact @{text U} is bound to
   4.388 +  the matching premise and the variable @{term "y"} is bound to the matching
   4.389 +  witness. The existential introduction rule @{text "exI:"}~@{thm exI} is then
   4.390 +  instantiated with @{term "y"} as the witness and @{term "Q"} as the
   4.391 +  predicate, with its proof obligation solved by the local fact U (using the
   4.392 +  Isar attribute @{attribute OF}). The following example is a trivial use of
   4.393 +  this method.
   4.394 +\<close>
   4.395 +
   4.396 +    lemma "halts p \<Longrightarrow> \<exists>x. halts x"
   4.397 +      by solve_ex
   4.398 +
   4.399 +
   4.400 +subsubsection \<open>Operating within a focus\<close>
   4.401 +
   4.402 +text \<open>
   4.403 +  Subgoal focusing provides a structured form of a subgoal, allowing for more
   4.404 +  expressive introspection of the goal state. This requires some consideration
   4.405 +  in order to be used effectively. When the keyword @{keyword "premises"} is
   4.406 +  given as the match target, the premises of the subgoal are lifted into
   4.407 +  hypothetical theorems, which can be found and named via match patterns.
   4.408 +  Additionally these premises are stripped from the subgoal, leaving only the
   4.409 +  conclusion. This renders them inaccessible to standard proof methods which
   4.410 +  operate on the premises, such as @{method frule} or @{method erule}. Naive
   4.411 +  usage of these methods within a match will most likely not function as the
   4.412 +  method author intended.
   4.413 +\<close>
   4.414 +
   4.415 +    method my_allE_bad for y :: 'a =
   4.416 +      (match premises in I: "\<forall>x :: 'a. ?Q x" \<Rightarrow>
   4.417 +        \<open>erule allE [where x = y]\<close>)
   4.418 +
   4.419 +text \<open>
   4.420 +  Here we take a single parameter @{term y} and specialize the universal
   4.421 +  elimination rule (@{thm allE}) to it, then attempt to apply this specialized
   4.422 +  rule with @{method erule}. The method @{method erule} will attempt to unify
   4.423 +  with a universal quantifier in the premises that matches the type of @{term
   4.424 +  y}. Since @{keyword "premises"} causes a focus, however, there are no
   4.425 +  subgoal premises to be found and thus @{method my_allE_bad} will always
   4.426 +  fail. If focusing instead left the premises in place, using methods
   4.427 +  like @{method erule} would lead to unintended behaviour, specifically during
   4.428 +  backtracking. In our example, @{method erule} could choose an alternate
   4.429 +  premise while backtracking, while leaving @{text I} bound to the original
   4.430 +  match. In the case of more complex inner methods, where either @{text I} or
   4.431 +  bound terms are used, this would almost certainly not be the intended
   4.432 +  behaviour.
   4.433 +
   4.434 +  An alternative implementation would be to specialize the elimination rule to
   4.435 +  the bound term and apply it directly.
   4.436 +\<close>
   4.437 +
   4.438 +    method my_allE_almost for y :: 'a =
   4.439 +      (match premises in I: "\<forall>x :: 'a. ?Q x" \<Rightarrow>
   4.440 +        \<open>rule allE [where x = y, OF I]\<close>)
   4.441 +
   4.442 +    lemma "\<forall>x. P x \<Longrightarrow> P y"
   4.443 +      by (my_allE_almost y)
   4.444 +
   4.445 +text \<open>
   4.446 +  This method will insert a specialized duplicate of a universally quantified
   4.447 +  premise. Although this will successfully apply in the presence of such a
   4.448 +  premise, it is not likely the intended behaviour. Repeated application of
   4.449 +  this method will produce an infinite stream of duplicate specialized
   4.450 +  premises, due to the original premise never being removed. To address this,
   4.451 +  matched premises may be declared with the @{attribute "thin"} attribute.
   4.452 +  This will hide the premise from subsequent inner matches, and remove it from
   4.453 +  the list of premises when the inner method has finished and the subgoal is
   4.454 +  unfocused. It can be considered analogous to the existing @{text thin_tac}.
   4.455 +
   4.456 +  To complete our example, the correct implementation of the method
   4.457 +  will @{attribute "thin"} the premise from the match and then apply it to the
   4.458 +  specialized elimination rule.\<close>
   4.459 +
   4.460 +    method my_allE for y :: 'a =
   4.461 +      (match premises in I [thin]: "\<forall>x :: 'a. ?Q x" \<Rightarrow>
   4.462 +         \<open>rule allE [where x = y, OF I]\<close>)
   4.463 +
   4.464 +    lemma "\<forall>x. P x \<Longrightarrow> \<forall>x. Q x \<Longrightarrow> P y \<and> Q y"
   4.465 +      by (my_allE y)+ (rule conjI)
   4.466 +
   4.467 +
   4.468 +subsection \<open>Attributes\<close>
   4.469 +
   4.470 +text \<open>
   4.471 +  Attributes may throw errors when applied to a given fact. For example, rule
   4.472 +  instantiation will fail of there is a type mismatch or if a given variable
   4.473 +  doesn't exist. Within a match or a method definition, it isn't generally
   4.474 +  possible to guarantee that applied attributes won't fail. For example, in
   4.475 +  the following method there is no guarantee that the two provided facts will
   4.476 +  necessarily compose.
   4.477 +\<close>
   4.478 +
   4.479 +    method my_compose uses rule1 rule2 =
   4.480 +      (rule rule1[OF rule2])
   4.481 +
   4.482 +text \<open>
   4.483 +  Some attributes (like @{attribute OF}) have been made partially
   4.484 +  Eisbach-aware. This means that they are able to form a closure despite not
   4.485 +  necessarily always being applicable. In the case of @{attribute OF}, it is
   4.486 +  up to the proof author to guard attribute application with an appropriate
   4.487 +  @{method match}, but there are still no static guarantees.
   4.488 +
   4.489 +  In contrast to @{attribute OF}, the @{attribute "where"} and @{attribute of}
   4.490 +  attributes attempt to provide static guarantees that they will apply
   4.491 +  whenever possible.
   4.492 +
   4.493 +  Within a match pattern for a fact, each outermost quantifier specifies the
   4.494 +  requirement that a matching fact must have a schematic variable at that
   4.495 +  point. This gives a corresponding name to this ``slot'' for the purposes of
   4.496 +  forming a static closure, allowing the @{attribute "where"} attribute to
   4.497 +  perform an instantiation at run-time.
   4.498 +\<close>
   4.499 +
   4.500 +    lemma
   4.501 +      assumes A: "Q \<Longrightarrow> False"
   4.502 +      shows "\<not> Q"
   4.503 +      by (match intros in X: "\<And>P. (P \<Longrightarrow> False) \<Longrightarrow> \<not> P" \<Rightarrow>
   4.504 +            \<open>rule X [where P = Q, OF A]\<close>)
   4.505 +
   4.506 +text \<open>
   4.507 +  Subgoal focusing converts the outermost quantifiers of premises into
   4.508 +  schematics when lifting them to hypothetical facts. This allows us to
   4.509 +  instantiate them with @{attribute "where"} when using an appropriate match
   4.510 +  pattern.
   4.511 +\<close>
   4.512 +
   4.513 +    lemma "(\<And>x :: 'a. A x \<Longrightarrow> B x) \<Longrightarrow> A y \<Longrightarrow> B y"
   4.514 +      by (match premises in I: "\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x" \<Rightarrow>
   4.515 +            \<open>rule I [where x = y]\<close>)
   4.516 +
   4.517 +text \<open>
   4.518 +  The @{attribute of} attribute behaves similarly. It is worth noting,
   4.519 +  however, that the positional instantiation of @{attribute of} occurs against
   4.520 +  the position of the variables as they are declared \emph{in the match
   4.521 +  pattern}.
   4.522 +\<close>
   4.523 +
   4.524 +    lemma
   4.525 +      fixes A B and x :: 'a and y :: 'b
   4.526 +      assumes asm: "(\<And>x y. A y x \<Longrightarrow> B x y )"
   4.527 +      shows "A y x \<Longrightarrow> B x y"
   4.528 +      by (match asm in I: "\<And>(x :: 'a) (y :: 'b). ?P x y \<Longrightarrow> ?Q x y" \<Rightarrow>
   4.529 +            \<open>rule I [of x y]\<close>)
   4.530 +
   4.531 +text \<open>
   4.532 +  In this example, the order of schematics in @{text asm} is actually @{text
   4.533 +  "?y ?x"}, but we instantiate our matched rule in the opposite order. This is
   4.534 +  because the effective rule @{term I} was bound from the match, which
   4.535 +  declared the @{typ 'a} slot first and the @{typ 'b} slot second.
   4.536 +
   4.537 +  To get the dynamic behaviour of @{attribute of} we can choose to invoke it
   4.538 +  \emph{unchecked}. This avoids trying to do any type inference for the
   4.539 +  provided parameters, instead storing them as their most general type and
   4.540 +  doing type matching at run-time. This, like @{attribute OF}, will throw
   4.541 +  errors if the expected slots don't exist or there is a type mismatch.
   4.542 +\<close>
   4.543 +
   4.544 +    lemma
   4.545 +      fixes A B and x :: 'a and y :: 'b
   4.546 +      assumes asm: "\<And>x y. A y x \<Longrightarrow> B x y"
   4.547 +      shows "A y x \<Longrightarrow> B x y"
   4.548 +      by (match asm in I: "PROP ?P" \<Rightarrow> \<open>rule I [of (unchecked) y x]\<close>)
   4.549 +
   4.550 +text \<open>
   4.551 +  Attributes may be applied to matched facts directly as they are matched. Any
   4.552 +  declarations will therefore be applied in the context of the inner method,
   4.553 +  as well as any transformations to the rule.
   4.554 +\<close>
   4.555 +
   4.556 +    lemma "(\<And>x :: 'a. A x \<Longrightarrow> B x) \<Longrightarrow> A y \<longrightarrow> B y"
   4.557 +      by (match premises in I[of y, intros]: "\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x" \<Rightarrow>
   4.558 +            \<open>prop_solver\<close>)
   4.559 +
   4.560 +text \<open>
   4.561 +  In this example, the pattern @{text "\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x"} matches against
   4.562 +  the only premise, giving an appropriately typed slot for @{term y}. After
   4.563 +  the match, the resulting rule is instantiated to @{term y} and then declared
   4.564 +  as an @{attribute intros} rule. This is then picked up by @{method
   4.565 +  prop_solver} to solve the goal.
   4.566 +\<close>
   4.567 +
   4.568 +
   4.569 +section \<open>Multi-match \label{sec:multi}\<close>
   4.570 +
   4.571 +text \<open>
   4.572 +  In all previous examples, @{method match} was only ever searching for a
   4.573 +  single rule or premise. Each local fact would therefore always have a length
   4.574 +  of exactly one. We may, however, wish to find \emph{all} matching results.
   4.575 +  To achieve this, we can simply mark a given pattern with the @{text
   4.576 +  "(multi)"} argument.
   4.577 +\<close>
   4.578 +
   4.579 +    lemma
   4.580 +      assumes asms: "A \<Longrightarrow> B" "A \<Longrightarrow> D"
   4.581 +      shows "(A \<longrightarrow> B) \<and> (A \<longrightarrow> D)"
   4.582 +      apply (match asms in I[intros]: "?P \<Longrightarrow> ?Q"  \<Rightarrow> \<open>solves \<open>prop_solver\<close>\<close>)?
   4.583 +      by (match asms in I[intros]: "?P \<Longrightarrow> ?Q" (multi) \<Rightarrow> \<open>prop_solver\<close>)
   4.584 +
   4.585 +text \<open>
   4.586 +  In the first @{method match}, without the @{text "(multi)"} argument, @{term
   4.587 +  I} is only ever be bound to one of the members of @{text asms}. This
   4.588 +  backtracks over both possibilities (see next section), however neither
   4.589 +  assumption in isolation is sufficient to solve to goal. The use of the
   4.590 +  @{method solves} combinator ensures that @{method prop_solver} has no effect
   4.591 +  on the goal when it doesn't solve it, and so the first match leaves the goal
   4.592 +  unchanged. In the second @{method match}, @{text I} is bound to all of
   4.593 +  @{text asms}, declaring both results as @{text intros}. With these rules
   4.594 +  @{method prop_solver} is capable of solving the goal.
   4.595 +
   4.596 +  Using for-fixed variables in patterns imposes additional constraints on the
   4.597 +  results. In all previous examples, the choice of using @{text ?P} or a
   4.598 +  for-fixed @{term P} only depended on whether or not @{term P} was mentioned
   4.599 +  in another pattern or the inner method. When using a multi-match, however,
   4.600 +  all for-fixed terms must agree in the results.
   4.601 +\<close>
   4.602 +
   4.603 +    lemma
   4.604 +      assumes asms: "A \<Longrightarrow> B" "A \<Longrightarrow> D" "D \<Longrightarrow> B"
   4.605 +      shows "(A \<longrightarrow> B) \<and> (A \<longrightarrow> D)"
   4.606 +      apply (match asms in I[intros]: "?P \<Longrightarrow> Q" (multi) for Q \<Rightarrow>
   4.607 +              \<open>solves \<open>prop_solver\<close>\<close>)?
   4.608 +      by (match asms in I[intros]: "P \<Longrightarrow> ?Q" (multi) for P \<Rightarrow>
   4.609 +              \<open>prop_solver\<close>)
   4.610 +
   4.611 +text \<open>
   4.612 +  Here we have two seemingly-equivalent applications of @{method match},
   4.613 +  however only the second one is capable of solving the goal. The first
   4.614 +  @{method match} selects the first and third members of @{text asms} (those
   4.615 +  that agree on their conclusion), which is not sufficient. The second
   4.616 +  @{method match} selects the first and second members of @{text asms} (those
   4.617 +  that agree on their assumption), which is enough for @{method prop_solver}
   4.618 +  to solve the goal.
   4.619 +\<close>
   4.620 +
   4.621 +
   4.622 +section \<open>Dummy patterns\<close>
   4.623 +
   4.624 +text \<open>
   4.625 +  Dummy patterns may be given as placeholders for unique schematics in
   4.626 +  patterns. They implicitly receive all currently bound variables as
   4.627 +  arguments, and are coerced into the @{typ prop} type whenever possible. For
   4.628 +  example, the trivial dummy pattern @{text "_"} will match any proposition.
   4.629 +  In contrast, by default the pattern @{text "?P"} is considered to have type
   4.630 +  @{typ bool}. It will not bind anything with meta-logical connectives (e.g.
   4.631 +  @{text "_ \<Longrightarrow> _"} or @{text "_ &&& _"}).
   4.632 +\<close>
   4.633 +
   4.634 +    lemma
   4.635 +      assumes asms: "A &&& B \<Longrightarrow> D"
   4.636 +      shows "(A \<and> B \<longrightarrow> D)"
   4.637 +      by (match asms in I:_ \<Rightarrow> \<open>prop_solver intros: I conjunctionI\<close>)
   4.638 +
   4.639 +
   4.640 +section \<open>Backtracking\<close>
   4.641 +
   4.642 +text \<open>
   4.643 +  Patterns are considered top-down, executing the inner method @{text m} of
   4.644 +  the first pattern which is satisfied by the current match target. By
   4.645 +  default, matching performs extensive backtracking by attempting all valid
   4.646 +  variable and fact bindings according to the given pattern. In particular,
   4.647 +  all unifiers for a given pattern will be explored, as well as each matching
   4.648 +  fact. The inner method @{text m} will be re-executed for each different
   4.649 +  variable/fact binding during backtracking. A successful match is considered
   4.650 +  a cut-point for backtracking. Specifically, once a match is made no other
   4.651 +  pattern-method pairs will be considered.
   4.652 +
   4.653 +  The method @{text foo} below fails for all goals that are conjunctions. Any
   4.654 +  such goal will match the first pattern, causing the second pattern (that
   4.655 +  would otherwise match all goals) to never be considered. If multiple
   4.656 +  unifiers exist for the pattern @{text "?P \<and> ?Q"} against the current goal,
   4.657 +  then the failing method @{method fail} will be (uselessly) tried for all of
   4.658 +  them.
   4.659 +\<close>
   4.660 +
   4.661 +    method foo =
   4.662 +      (match conclusion in "?P \<and> ?Q" \<Rightarrow> \<open>fail\<close> \<bar> "?R" \<Rightarrow> \<open>prop_solver\<close>)
   4.663 +
   4.664 +text \<open>
   4.665 +  This behaviour is in direct contrast to the backtracking done by Coq's Ltac,
   4.666 +  which will attempt all patterns in a match before failing. This means that
   4.667 +  the failure of an inner method that is executed after a successful match
   4.668 +  does not, in Ltac, cause the entire match to fail, whereas it does in
   4.669 +  Eisbach. In Eisbach the distinction is important due to the pervasive use of
   4.670 +  backtracking. When a method is used in a combinator chain, its failure
   4.671 +  becomes significant because it signals previously applied methods to move to
   4.672 +  the next result. Therefore, it is necessary for @{method match} to not mask
   4.673 +  such failure. One can always rewrite a match using the combinators ``@{text
   4.674 +  "?"}'' and ``@{text "|"}'' to try subsequent patterns in the case of an
   4.675 +  inner-method failure. The following proof method, for example, always
   4.676 +  invokes @{method prop_solver} for all goals because its first alternative
   4.677 +  either never matches or (if it does match) always fails.
   4.678 +\<close>
   4.679 +
   4.680 +    method foo\<^sub>1 =
   4.681 +      (match conclusion in "?P \<and> ?Q" \<Rightarrow> \<open>fail\<close>) |
   4.682 +      (match conclusion in "?R" \<Rightarrow> \<open>prop_solver\<close>)
   4.683 +
   4.684 +
   4.685 +subsection \<open>Cut\<close>
   4.686 +
   4.687 +text \<open>
   4.688 +  Backtracking may be controlled more precisely by marking individual patterns
   4.689 +  as \emph{cut}. This causes backtracking to not progress beyond this pattern:
   4.690 +  once a match is found no others will be considered.
   4.691 +\<close>
   4.692 +
   4.693 +    method foo\<^sub>2 =
   4.694 +      (match premises in I: "P \<and> Q" (cut) and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow>
   4.695 +        \<open>rule mp [OF I' I [THEN conjunct1]]\<close>)
   4.696 +
   4.697 +text \<open>
   4.698 +  In this example, once a conjunction is found (@{term "P \<and> Q"}), all possible
   4.699 +  implications of @{term "P"} in the premises are considered, evaluating the
   4.700 +  inner @{method rule} with each consequent. No other conjunctions will be
   4.701 +  considered, with method failure occurring once all implications of the
   4.702 +  form @{text "P \<longrightarrow> ?U"} have been explored. Here the left-right processing of
   4.703 +  individual patterns is important, as all patterns after of the cut will
   4.704 +  maintain their usual backtracking behaviour.
   4.705 +\<close>
   4.706 +
   4.707 +    lemma "A \<and> B \<Longrightarrow> A \<longrightarrow> D \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> C"
   4.708 +      by foo\<^sub>2
   4.709 +
   4.710 +    lemma "C \<and> D \<Longrightarrow> A \<and> B \<Longrightarrow> A \<longrightarrow> C  \<Longrightarrow> C"
   4.711 +      by (foo\<^sub>2 | prop_solver)
   4.712 +
   4.713 +text \<open>
   4.714 +  In this example, the first lemma is solved by @{text foo\<^sub>2}, by first
   4.715 +  picking @{term "A \<longrightarrow> D"} for @{text I'}, then backtracking and ultimately
   4.716 +  succeeding after picking @{term "A \<longrightarrow> C"}. In the second lemma, however,
   4.717 +  @{term "C \<and> D"} is matched first, the second pattern in the match cannot be
   4.718 +  found and so the method fails, falling through to @{method prop_solver}.
   4.719 +\<close>
   4.720 +
   4.721 +
   4.722 +subsection \<open>Multi-match revisited\<close>
   4.723 +
   4.724 +text \<open>
   4.725 +  A multi-match will produce a sequence of potential bindings for for-fixed
   4.726 +  variables, where each binding environment is the result of matching against
   4.727 +  at least one element from the match target. For each environment, the match
   4.728 +  result will be all elements of the match target which agree with the pattern
   4.729 +  under that environment. This can result in unexpected behaviour when giving
   4.730 +  very general patterns.
   4.731 +\<close>
   4.732 +
   4.733 +    lemma
   4.734 +      assumes asms: "\<And>x. A x \<and> B x" "\<And>y. A y \<and> C y" "\<And>z. B z \<and> C z"
   4.735 +      shows "A x \<and> C x"
   4.736 +      by (match asms in I: "\<And>x. P x \<and> ?Q x" (multi) for P \<Rightarrow>
   4.737 +         \<open>match (P) in "A" \<Rightarrow> \<open>fail\<close>
   4.738 +                       \<bar> _ \<Rightarrow> \<open>match I in "\<And>x. A x \<and> B x" \<Rightarrow> \<open>fail\<close>
   4.739 +                                                      \<bar> _ \<Rightarrow> \<open>rule I\<close>\<close>\<close>)
   4.740 +
   4.741 +text \<open>
   4.742 +  Intuitively it seems like this proof should fail to check. The first match
   4.743 +  result, which binds @{term I} to the first two members of @{text asms},
   4.744 +  fails the second inner match due to binding @{term P} to @{term A}.
   4.745 +  Backtracking then attempts to bind @{term I} to the third member of @{text
   4.746 +  asms}. This passes all inner matches, but fails when @{method rule} cannot
   4.747 +  successfully apply this to the current goal. After this, a valid match that
   4.748 +  is produced by the unifier is one which binds @{term P} to simply @{text
   4.749 +  "\<lambda>a. A ?x"}. The first inner match succeeds because @{text "\<lambda>a. A ?x"} does
   4.750 +  not match @{term A}. The next inner match succeeds because @{term I} has
   4.751 +  only been bound to the first member of @{text asms}. This is due to @{method
   4.752 +  match} considering @{text "\<lambda>a. A ?x"} and @{text "\<lambda>a. A ?y"} as distinct
   4.753 +  terms.
   4.754 +
   4.755 +  The simplest way to address this is to explicitly disallow term bindings
   4.756 +  which we would consider invalid.
   4.757 +\<close>
   4.758 +
   4.759 +    method abs_used for P =
   4.760 +      (match (P) in "\<lambda>a. ?P" \<Rightarrow> \<open>fail\<close> \<bar> _ \<Rightarrow> \<open>-\<close>)
   4.761 +
   4.762 +text \<open>
   4.763 +  This method has no effect on the goal state, but instead serves as a filter
   4.764 +  on the environment produced from match.
   4.765 +\<close>
   4.766 +
   4.767 +
   4.768 +section \<open>Uncurrying\<close>
   4.769 +
   4.770 +text \<open>
   4.771 +  The @{method match} method is not aware of the logical content of match
   4.772 +  targets. Each pattern is simply matched against the shallow structure of a
   4.773 +  fact or term. Most facts are in \emph{normal form}, which curries premises
   4.774 +  via meta-implication @{text "_ \<Longrightarrow> _"}.
   4.775 +\<close>
   4.776 +
   4.777 +    lemma
   4.778 +      assumes asms: "D \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> A"
   4.779 +      shows "D \<Longrightarrow> B \<Longrightarrow> C \<and> A"
   4.780 +      by (match asms in H:"D \<Longrightarrow> _" (multi) \<Rightarrow> \<open>prop_solver elims: H\<close>)
   4.781 +
   4.782 +text \<open>
   4.783 +  For the first member of @{text asms} the dummy pattern successfully matches
   4.784 +  against @{term "B \<Longrightarrow> C"} and so the proof is successful.
   4.785 +\<close>
   4.786 +
   4.787 +    lemma
   4.788 +      assumes asms: "A \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> C"
   4.789 +      shows "D \<or> (A \<and> B) \<Longrightarrow> C"
   4.790 +      apply (match asms in H:"_ \<Longrightarrow> C" (multi) \<Rightarrow> \<open>prop_solver elims: H\<close>)(*<*)?
   4.791 +      by (prop_solver elims: asms)(*>*)
   4.792 +
   4.793 +text \<open>
   4.794 +  This proof will fail to solve the goal. Our match pattern will only match
   4.795 +  rules which have a single premise, and conclusion @{term C}, so the first
   4.796 +  member of @{text asms} is not bound and thus the proof fails. Matching a
   4.797 +  pattern of the form @{term "P \<Longrightarrow> Q"} against this fact will bind @{term "P"}
   4.798 +  to @{term "A"} and @{term Q} to @{term "B \<Longrightarrow> C"}. Our pattern, with a
   4.799 +  concrete @{term "C"} in the conclusion, will fail to match this fact.
   4.800 +
   4.801 +  To express our desired match, we may \emph{uncurry} our rules before
   4.802 +  matching against them. This forms a meta-conjunction of all premises in a
   4.803 +  fact, so that only one implication remains. For example the uncurried
   4.804 +  version of @{term "A \<Longrightarrow> B \<Longrightarrow> C"} is @{term "A &&& B \<Longrightarrow> C"}. This will now match
   4.805 +  our desired pattern @{text "_ \<Longrightarrow> C"}, and can be \emph{curried} after the
   4.806 +  match to put it back into normal form.
   4.807 +\<close>
   4.808 +
   4.809 +    lemma
   4.810 +      assumes asms: "A \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> C"
   4.811 +      shows "D \<or> (A \<and> B) \<Longrightarrow> C"
   4.812 +      by (match asms[uncurry] in H[curry]:"_ \<Longrightarrow> C" (multi) \<Rightarrow>
   4.813 +          \<open>prop_solver elims: H\<close>)
   4.814 +
   4.815 +
   4.816 +section \<open>Reverse matching\<close>
   4.817 +
   4.818 +text \<open>
   4.819 +  The @{method match} method only attempts to perform matching of the pattern
   4.820 +  against the match target. Specifically this means that it will not
   4.821 +  instantiate schematic terms in the match target.
   4.822 +\<close>
   4.823 +
   4.824 +    lemma
   4.825 +      assumes asms: "\<And>x :: 'a. A x"
   4.826 +      shows "A y"
   4.827 +      apply (match asms in H:"A y" \<Rightarrow> \<open>rule H\<close>)?
   4.828 +      by (match asms in H:"P" for P \<Rightarrow>
   4.829 +          \<open>match ("A y") in "P" \<Rightarrow> \<open>rule H\<close>\<close>)
   4.830 +
   4.831 +text \<open>
   4.832 +  In the first @{method match} we attempt to find a member of @{text asms}
   4.833 +  which matches our goal precisely. This fails due to no such member existing.
   4.834 +  The second match reverses the role of the fact in the match, by first giving
   4.835 +  a general pattern @{term P}. This bound pattern is then matched against
   4.836 +  @{term "A y"}. In this case, @{term P} is bound to @{text "A ?x"} and so it
   4.837 +  successfully matches.
   4.838 +\<close>
   4.839 +
   4.840 +
   4.841 +section \<open>Type matching\<close>
   4.842 +
   4.843 +text \<open>
   4.844 +  The rule instantiation attributes @{attribute "where"} and @{attribute "of"}
   4.845 +  attempt to guarantee type-correctness wherever possible. This can require
   4.846 +  additional invocations of @{method match} in order to statically ensure that
   4.847 +  instantiation will succeed.
   4.848 +\<close>
   4.849 +
   4.850 +    lemma
   4.851 +      assumes asms: "\<And>x :: 'a. A x"
   4.852 +      shows "A y"
   4.853 +      by (match asms in H:"\<And>z :: 'b. P z" for P \<Rightarrow>
   4.854 +          \<open>match (y) in "y :: 'b" for y \<Rightarrow> \<open>rule H[where z=y]\<close>\<close>)
   4.855 +
   4.856 +text \<open>
   4.857 +  In this example the type @{text 'b} is matched to @{text 'a}, however
   4.858 +  statically they are formally distinct types. The first match binds @{text
   4.859 +  'b} while the inner match serves to coerce @{term y} into having the type
   4.860 +  @{text 'b}. This allows the rule instantiation to successfully apply.
   4.861 +\<close>
   4.862 +
   4.863 +
   4.864 +chapter \<open>Method development\<close>
   4.865 +
   4.866 +section \<open>Tracing methods\<close>
   4.867 +
   4.868 +text \<open>
   4.869 +  Method tracing is supported by auxiliary print methods provided by @{theory
   4.870 +  Eisbach_Tools}. These include @{method print_fact}, @{method print_term} and
   4.871 +  @{method print_type}. Whenever a print method is evaluated it leaves the
   4.872 +  goal unchanged and writes its argument as tracing output.
   4.873 +
   4.874 +  Print methods can be combined with the @{method fail} method to investigate
   4.875 +  the backtracking behaviour of a method.
   4.876 +\<close>
   4.877 +
   4.878 +    lemma
   4.879 +      assumes asms: A B C D
   4.880 +      shows D
   4.881 +      apply (match asms in H:_ \<Rightarrow> \<open>print_fact H, fail\<close>)(*<*)?
   4.882 +      by (simp add: asms)(*>*)
   4.883 +
   4.884 +text \<open>
   4.885 +  This proof will fail, but the tracing output will show the order that the
   4.886 +  assumptions are attempted.
   4.887 +\<close>
   4.888 +
   4.889 +
   4.890 +section \<open>Integrating with Isabelle/ML\<close>
   4.891 +
   4.892 +subsection \<open>Attributes\<close>
   4.893 +
   4.894 +text \<open>
   4.895 +  A custom rule attribute is a simple way to extend the functionality of
   4.896 +  Eisbach methods. The dummy rule attribute notation (@{text "[[ _ ]]"})
   4.897 +  invokes the given attribute against a dummy fact and evaluates to the result
   4.898 +  of that attribute. When used as a match target, this can serve as an
   4.899 +  effective auxiliary function.
   4.900 +\<close>
   4.901 +
   4.902 +    attribute_setup get_split_rule =
   4.903 +      \<open>Args.term >> (fn t =>
   4.904 +        Thm.rule_attribute (fn context => fn _ =>
   4.905 +          (case get_split_rule (Context.proof_of context) t of
   4.906 +            SOME thm => thm
   4.907 +          | NONE => Drule.dummy_thm)))\<close>
   4.908 +
   4.909 +text \<open>
   4.910 +  In this example, the new attribute @{attribute get_split_rule} lifts the ML
   4.911 +  function of the same name into an attribute. When applied to a cast
   4.912 +  distinction over a datatype, it retrieves its corresponding split rule.
   4.913 +
   4.914 +  We can then integrate this intro a method that applies the split rule, fist
   4.915 +  matching to ensure that fetching the rule was successful.
   4.916 +\<close>
   4.917 +
   4.918 +    method splits =
   4.919 +      (match conclusion in "?P f" for f \<Rightarrow>
   4.920 +        \<open>match [[get_split_rule f]] in U: "(_ :: bool) = _" \<Rightarrow>
   4.921 +          \<open>rule U[THEN iffD2]\<close>\<close>)
   4.922 +
   4.923 +    lemma "L \<noteq> [] \<Longrightarrow> case L of [] \<Rightarrow> False | _ \<Rightarrow> True"
   4.924 +      by (splits, prop_solver intros: allI)
   4.925 +
   4.926 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Doc/Eisbach/Preface.thy	Sun May 17 23:03:49 2015 +0200
     5.3 @@ -0,0 +1,35 @@
     5.4 +(*:wrap=hard:maxLineLen=78:*)
     5.5 +
     5.6 +theory Preface
     5.7 +imports Base "../Eisbach_Tools"
     5.8 +begin
     5.9 +
    5.10 +text \<open>
    5.11 +  \emph{Eisbach} is a collection of tools which form the basis for defining
    5.12 +  new proof methods in Isabelle/Isar~@{cite "Wenzel-PhD"}. It can be thought
    5.13 +  of as a ``proof method language'', but is more precisely an infrastructure
    5.14 +  for defining new proof methods out of existing ones.
    5.15 +
    5.16 +  The core functionality of Eisbach is provided by the Isar @{command method}
    5.17 +  command. Here users may define new methods by combining existing ones with
    5.18 +  the usual Isar syntax These methods can be abstracted over terms, facts and
    5.19 +  other methods, as one might expect in any higher-order functional language.
    5.20 +
    5.21 +  Additional functionality is provided by extending the space of methods and
    5.22 +  attributes. The new @{method match} method allows for explicit control-flow,
    5.23 +  by taking a match target and a list of pattern-method pairs. By using the
    5.24 +  functionality provided by Eisbach, additional support methods can be easily
    5.25 +  written. For example, the @{method catch} method, which provides basic
    5.26 +  try-catch functionality, only requires a few lines of ML.
    5.27 +
    5.28 +  Eisbach is meant to allow users to write automation using only Isar syntax.
    5.29 +  Traditionally proof methods have been written in Isabelle/ML, which poses a
    5.30 +  high barrier-to-entry for many users.
    5.31 +
    5.32 +  \medskip This manual is written for users familiar with Isabelle/Isar, but
    5.33 +  not necessarily Isabelle/ML. It covers the usage of the @{command method} as
    5.34 +  well as the @{method match} method, as well as discussing their integration
    5.35 +  with existing Isar concepts such as @{command named_theorems}.
    5.36 +\<close>
    5.37 +
    5.38 +end
    5.39 \ No newline at end of file
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Doc/Eisbach/document/build	Sun May 17 23:03:49 2015 +0200
     6.3 @@ -0,0 +1,10 @@
     6.4 +#!/usr/bin/env bash
     6.5 +
     6.6 +set -e
     6.7 +
     6.8 +FORMAT="$1"
     6.9 +VARIANT="$2"
    6.10 +
    6.11 +"$ISABELLE_TOOL" logo Eisbach
    6.12 +"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
    6.13 +
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Doc/Eisbach/document/root.tex	Sun May 17 23:03:49 2015 +0200
     7.3 @@ -0,0 +1,88 @@
     7.4 +\documentclass[12pt,a4paper,fleqn]{report}
     7.5 +\usepackage[T1]{fontenc}
     7.6 +\usepackage{latexsym,graphicx}
     7.7 +\usepackage[refpage]{nomencl}
     7.8 +\usepackage{iman,extra,isar,proof}
     7.9 +\usepackage[nohyphen,strings]{underscore}
    7.10 +\usepackage{isabelle}
    7.11 +\usepackage{isabellesym}
    7.12 +\usepackage{railsetup}
    7.13 +\usepackage{ttbox}
    7.14 +\usepackage{supertabular}
    7.15 +\usepackage{style}
    7.16 +\usepackage{pdfsetup}
    7.17 +
    7.18 +
    7.19 +\hyphenation{Isabelle}
    7.20 +\hyphenation{Eisbach}
    7.21 +
    7.22 +\isadroptag{theory}
    7.23 +\title{\includegraphics[scale=0.5]{isabelle_eisbach}
    7.24 +  \\[4ex] The Eisbach User Manual}
    7.25 +\author{Daniel Matichuk \\
    7.26 +  Makarius Wenzel \\
    7.27 +  Toby Murray
    7.28 +}
    7.29 +
    7.30 +
    7.31 +% Control fixmes etc.
    7.32 +\newif\ifDraft \newif\ifFinal
    7.33 +%\Drafttrue\Finalfalse
    7.34 +\Draftfalse\Finaltrue
    7.35 +
    7.36 +
    7.37 +\ifDraft
    7.38 +  \usepackage{draftcopy}
    7.39 +  \newcommand{\Comment}[1]{\textbf{\textsl{#1}}}
    7.40 +  \newenvironment{LongComment}[1] % multi-paragraph comment, argument is owner
    7.41 +    {\begingroup\par\noindent\slshape \textbf{Begin Comment[#1]}\par}
    7.42 +    {\par\noindent\textbf{End Comment}\endgroup\par}
    7.43 +  \newcommand{\FIXME}[1]{\textbf{\textsl{FIXME: #1}}}
    7.44 +  \newcommand{\TODO}[1]{\textbf{\textsl{TODO: #1}}}
    7.45 +\else
    7.46 +  \newcommand{\Comment}[1]{\relax}
    7.47 +  \newenvironment{LongComment}[1]{\expandafter\comment}{\expandafter\endcomment}
    7.48 +  \newcommand{\FIXME}[1]{\relax}
    7.49 +  \newcommand{\TODO}[1]{\relax}
    7.50 +\fi
    7.51 +
    7.52 +% This sort of command for each active author can be convenient
    7.53 +\newcommand{\dan}[1]{\Comment{#1 [dan]}}
    7.54 +\newcommand{\toby}[1]{\Comment{#1 [toby]}}
    7.55 +\newcommand{\makarius}[1]{\Comment{#1 [makarius]}}
    7.56 +
    7.57 +
    7.58 +\makeindex
    7.59 +
    7.60 +\chardef\charbackquote=`\`
    7.61 +\newcommand{\backquote}{\mbox{\tt\charbackquote}}
    7.62 +
    7.63 +
    7.64 +\begin{document}
    7.65 +
    7.66 +\maketitle
    7.67 +
    7.68 +\pagenumbering{roman}
    7.69 +\chapter*{Preface}
    7.70 +\input{Preface.tex}
    7.71 +\tableofcontents
    7.72 +\clearfirst
    7.73 +
    7.74 +\input{Manual.tex}
    7.75 +
    7.76 +\begingroup
    7.77 +\tocentry{\bibname}
    7.78 +\bibliographystyle{abbrv} \small\raggedright\frenchspacing
    7.79 +\bibliography{manual}
    7.80 +\endgroup
    7.81 +
    7.82 +\tocentry{\indexname}
    7.83 +\printindex
    7.84 +
    7.85 +\end{document}
    7.86 +
    7.87 +
    7.88 +%%% Local Variables:
    7.89 +%%% mode: latex
    7.90 +%%% TeX-master: t
    7.91 +%%% End:
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Doc/Eisbach/document/style.sty	Sun May 17 23:03:49 2015 +0200
     8.3 @@ -0,0 +1,68 @@
     8.4 +%% toc
     8.5 +\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
     8.6 +\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
     8.7 +
     8.8 +%% references
     8.9 +\newcommand{\secref}[1]{\S\ref{#1}}
    8.10 +\newcommand{\chref}[1]{chapter~\ref{#1}}
    8.11 +\newcommand{\figref}[1]{figure~\ref{#1}}
    8.12 +
    8.13 +%% math
    8.14 +\newcommand{\text}[1]{\mbox{#1}}
    8.15 +\newcommand{\isasymvartheta}{\isamath{\theta}}
    8.16 +\newcommand{\isactrlvec}[1]{\emph{$\vec{#1}$}}
    8.17 +\newcommand{\isactrlBG}{\isacharbackquoteopen}
    8.18 +\newcommand{\isactrlEN}{\isacharbackquoteclose}
    8.19 +
    8.20 +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    8.21 +
    8.22 +\pagestyle{headings}
    8.23 +\sloppy
    8.24 +\binperiod
    8.25 +
    8.26 +\parindent 0pt\parskip 0.5ex
    8.27 +
    8.28 +\renewcommand{\isadigit}[1]{\isamath{#1}}
    8.29 +
    8.30 +\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
    8.31 +
    8.32 +\isafoldtag{FIXME}
    8.33 +
    8.34 +\isakeeptag{mlref}
    8.35 +\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{ML}~~}Reference}}
    8.36 +\renewcommand{\endisatagmlref}{}
    8.37 +
    8.38 +\isakeeptag{mlantiq}
    8.39 +\renewcommand{\isatagmlantiq}{\subsection*{\makebox[0pt][r]{\fbox{ML}~~}Antiquotations}}
    8.40 +\renewcommand{\endisatagmlantiq}{}
    8.41 +
    8.42 +\isakeeptag{mlex}
    8.43 +\renewcommand{\isatagmlex}{\subsection*{\makebox[0pt][r]{\fbox{ML}~~}Examples}}
    8.44 +\renewcommand{\endisatagmlex}{}
    8.45 +
    8.46 +\renewcommand{\isatagML}{\begingroup\isabellestyle{default}\isastyle\def\isadigit##1{##1}}
    8.47 +\renewcommand{\endisatagML}{\endgroup}
    8.48 +
    8.49 +\newcommand{\minorcmd}[1]{{\sf #1}}
    8.50 +\newcommand{\isasymtype}{\minorcmd{type}}
    8.51 +\newcommand{\isasymval}{\minorcmd{val}}
    8.52 +
    8.53 +\newcommand{\isasymFIX}{\isakeyword{fix}}
    8.54 +\newcommand{\isasymASSUME}{\isakeyword{assume}}
    8.55 +\newcommand{\isasymDEFINE}{\isakeyword{define}}
    8.56 +\newcommand{\isasymNOTE}{\isakeyword{note}}
    8.57 +\newcommand{\isasymGUESS}{\isakeyword{guess}}
    8.58 +\newcommand{\isasymOBTAIN}{\isakeyword{obtain}}
    8.59 +\newcommand{\isasymTHEORY}{\isakeyword{theory}}
    8.60 +\newcommand{\isasymUSES}{\isakeyword{uses}}
    8.61 +\newcommand{\isasymEND}{\isakeyword{end}}
    8.62 +\newcommand{\isasymCONSTS}{\isakeyword{consts}}
    8.63 +\newcommand{\isasymDEFS}{\isakeyword{defs}}
    8.64 +\newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
    8.65 +\newcommand{\isasymDEFINITION}{\isakeyword{definition}}
    8.66 +
    8.67 +\isabellestyle{literal}
    8.68 +
    8.69 +\railtermfont{\isabellestyle{tt}}
    8.70 +\railnontermfont{\isabellestyle{itunderscore}}
    8.71 +\railnamefont{\isabellestyle{itunderscore}}
     9.1 --- a/src/Doc/ROOT	Sun May 17 22:33:34 2015 +0200
     9.2 +++ b/src/Doc/ROOT	Sun May 17 23:03:49 2015 +0200
     9.3 @@ -59,6 +59,28 @@
     9.4      "root.tex"
     9.5      "style.sty"
     9.6  
     9.7 +session Eisbach (doc) in "Eisbach" = "HOL-Eisbach" +
     9.8 +  options [document_variants = "eisbach", quick_and_dirty,
     9.9 +    print_mode = "no_brackets,iff", show_question_marks = false]
    9.10 +  theories [document = false]
    9.11 +    Base
    9.12 +  theories
    9.13 +    Preface
    9.14 +    Manual
    9.15 +  document_files (in "..")
    9.16 +    "prepare_document"
    9.17 +    "pdfsetup.sty"
    9.18 +    "iman.sty"
    9.19 +    "extra.sty"
    9.20 +    "isar.sty"
    9.21 +    "ttbox.sty"
    9.22 +    "underscore.sty"
    9.23 +    "manual.bib"
    9.24 +  document_files
    9.25 +    "build"
    9.26 +    "root.tex"
    9.27 +    "style.sty"
    9.28 +
    9.29  session Functions (doc) in "Functions" = HOL +
    9.30    options [document_variants = "functions", skip_proofs = false, quick_and_dirty]
    9.31    theories Functions