# HG changeset patch
# User wenzelm
# Date 1431896629 -7200
# Node ID d7f636331176ed8baa0c6f40d9fbb18838829156
# Parent adde5ce1e0a735315b514d4bc846754aaaa20eb8
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
diff -r adde5ce1e0a7 -r d7f636331176 NEWS
--- a/NEWS Sun May 17 22:33:34 2015 +0200
+++ b/NEWS Sun May 17 23:03:49 2015 +0200
@@ -63,8 +63,9 @@
by combining existing ones with their usual syntax. The "match" proof
method provides basic fact/term matching in addition to
premise/conclusion matching through Subgoal.focus, and binds fact names
-from matches as well as term patterns within matches. See also
-~~/src/HOL/Eisbach/Eisbach.thy and the included examples.
+from matches as well as term patterns within matches. The Isabelle
+documentation provides an entry "eisbach" for the Eisbach User Manual.
+Sources and various examples are in ~~/src/HOL/Eisbach/.
*** Prover IDE -- Isabelle/Scala/jEdit ***
diff -r adde5ce1e0a7 -r d7f636331176 doc/Contents
--- a/doc/Contents Sun May 17 22:33:34 2015 +0200
+++ b/doc/Contents Sun May 17 23:03:49 2015 +0200
@@ -8,6 +8,7 @@
codegen Tutorial on Code Generation
nitpick User's Guide to Nitpick
sledgehammer User's Guide to Sledgehammer
+ eisbach The Eisbach User Manual
sugar LaTeX Sugar for Isabelle documents
Reference Manuals!
diff -r adde5ce1e0a7 -r d7f636331176 src/Doc/Eisbach/Base.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Eisbach/Base.thy Sun May 17 23:03:49 2015 +0200
@@ -0,0 +1,39 @@
+section \Basic setup that is not included in the document\
+
+theory Base
+imports Main
+begin
+
+ML_file "~~/src/Doc/antiquote_setup.ML"
+
+ML\
+fun get_split_rule ctxt target =
+ let
+ val (head, args) = strip_comb (Envir.eta_contract target);
+ val (const_name, _) = dest_Const head;
+ val const_name_components = Long_Name.explode const_name;
+
+ val _ =
+ if String.isPrefix "case_" (List.last const_name_components) then ()
+ else raise TERM ("Not a case statement", [target]);
+
+ val type_name = Long_Name.implode (rev (tl (rev const_name_components)));
+ val split = Proof_Context.get_thm ctxt (type_name ^ ".split");
+ val vars = Term.add_vars (Thm.prop_of split) [];
+
+ val datatype_name = nth (rev const_name_components) 1;
+
+ fun is_datatype (Type (a, _)) = Long_Name.base_name a = Long_Name.base_name datatype_name
+ | is_datatype _ = false;
+
+ val datatype_var =
+ (case find_first (fn (_, T') => is_datatype T') vars of
+ SOME var => Thm.cterm_of ctxt (Term.Var var)
+ | NONE => error ("Couldn't find datatype in thm: " ^ datatype_name));
+ in
+ SOME (Drule.cterm_instantiate [(datatype_var, Thm.cterm_of ctxt (List.last args))] split)
+ end
+ handle TERM _ => NONE;
+\
+
+end
diff -r adde5ce1e0a7 -r d7f636331176 src/Doc/Eisbach/Manual.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Eisbach/Manual.thy Sun May 17 23:03:49 2015 +0200
@@ -0,0 +1,923 @@
+(*:wrap=hard:maxLineLen=78:*)
+
+theory Manual
+imports Base "../Eisbach_Tools"
+begin
+
+chapter \The method command\
+
+text \
+ The @{command_def method} command provides the ability to write proof
+ methods by combining existing ones with their usual syntax. Specifically it
+ allows compound proof methods to be named, and to extend the name space of
+ basic methods accordingly. Method definitions may abstract over parameters:
+ terms, facts, or other methods.
+
+ \medskip The syntax diagram below refers to some syntactic categories that
+ are further defined in @{cite "isabelle-isar-ref"}.
+
+ @{rail \
+ @@{command method} name args @'=' method
+ ;
+ args: term_args? method_args? \ fact_args? decl_args?
+ ;
+ term_args: @'for' @{syntax "fixes"}
+ ;
+ method_args: @'methods' (name+)
+ ;
+ fact_args: @'uses' (name+)
+ ;
+ decl_args: @'declares' (name+)
+ \}
+\
+
+
+section \Basic method definitions\
+
+text \
+ Consider the following proof that makes use of usual Isar method
+ combinators.
+\
+
+ lemma "P \ Q \ P"
+ by ((rule impI, (erule conjE)?) | assumption)+
+
+text \
+ It is clear that this compound method will be applicable in more cases than
+ this proof alone. With the @{command method} command we can define a proof
+ method that makes the above functionality available generally.
+\
+
+ method prop_solver\<^sub>1 =
+ ((rule impI, (erule conjE)?) | assumption)+
+
+ lemma "P \ Q \ R \ P"
+ by prop_solver\<^sub>1
+
+text \
+ In this example, the facts @{text impI} and @{text conjE} are static. They
+ are evaluated once when the method is defined and cannot be changed later.
+ This makes the method stable in the sense of \emph{static scoping}: naming
+ another fact @{text impI} in a later context won't affect the behaviour of
+ @{text "prop_solver\<^sub>1"}.
+\
+
+
+section \Term abstraction\
+
+text \
+ Methods can also abstract over terms using the @{keyword_def "for"} keyword,
+ optionally providing type constraints. For instance, the following proof
+ method @{text intro_ex} takes a term @{term y} of any type, which it uses to
+ instantiate the @{term x}-variable of @{text exI} (existential introduction)
+ before applying the result as a rule. The instantiation is performed here by
+ Isar's @{attribute_ref "where"} attribute. If the current subgoal is to find
+ a witness for the given predicate @{term Q}, then this has the effect of
+ committing to @{term y}.
+\
+
+ method intro_ex for Q :: "'a \ bool" and y :: 'a =
+ (rule exI ["where" P = Q and x = y])
+
+
+text \
+ The term parameters @{term y} and @{term Q} can be used arbitrarily inside
+ the method body, as part of attribute applications or arguments to other
+ methods. The expression is type-checked as far as possible when the method
+ is defined, however dynamic type errors can still occur when it is invoked
+ (e.g.\ when terms are instantiated in a parameterized fact). Actual term
+ arguments are supplied positionally, in the same order as in the method
+ definition.
+\
+
+ lemma "P a \ \x. P x"
+ by (intro_ex P a)
+
+
+section \Fact abstraction\
+
+subsection \Named theorems\
+
+text \
+ A @{text "named theorem"} is a fact whose contents are produced dynamically
+ within the current proof context. The Isar command @{command_ref
+ "named_theorems"} provides simple access to this concept: it declares a
+ dynamic fact with corresponding \emph{attribute}
+ (see \autoref{s:attributes}) for managing this particular data slot in the
+ context.
+\
+
+ named_theorems intros
+
+text \
+ So far @{text "intros"} refers to the empty fact. Using the Isar command
+ @{command_ref "declare"} we may apply declaration attributes to the context.
+ Below we declare both @{text "conjI"} and @{text "impI"} as @{text
+ "intros"}, adding them to the named theorem slot.
+\
+
+ declare conjI [intros] and impI [intros]
+
+text \
+ We can refer to named theorems as dynamic facts within a particular proof
+ context, which are evaluated whenever the method is invoked. Instead of
+ having facts hard-coded into the method, as in @{text prop_solver\<^sub>1}, we can
+ instead refer to these named theorems.
+\
+
+ named_theorems elims
+ declare conjE [elims]
+
+ method prop_solver\<^sub>3 =
+ ((rule intros, (erule elims)?) | assumption)+
+
+ lemma "P \ Q \ P"
+ by prop_solver\<^sub>3
+
+text \
+ Often these named theorems need to be augmented on the spot, when a method
+ is invoked. The @{keyword_def "declares"} keyword in the signature of
+ @{command method} adds the common method syntax @{text "method decl: facts"}
+ for each named theorem @{text decl}.
+\
+
+ method prop_solver\<^sub>4 declares intros elims =
+ ((rule intros, (erule elims)?) | assumption)+
+
+ lemma "P \ (P \ Q) \ Q \ P"
+ by (prop_solver\<^sub>4 elims: impE intros: conjI)
+
+
+subsection \Simple fact abstraction\
+
+text \
+ The @{keyword "declares"} keyword requires that a corresponding dynamic fact
+ has been declared with @{command_ref named_theorems}. This is useful for
+ managing collections of facts which are to be augmented with declarations,
+ but is overkill if we simply want to pass a fact to a method.
+
+ We may use the @{keyword_def "uses"} keyword in the method header to provide
+ a simple fact parameter. In contrast to @{keyword "declares"}, these facts
+ are always implicitly empty unless augmented when the method is invoked.
+\
+
+ method rule_twice uses my_rule =
+ (rule my_rule, rule my_rule)
+
+ lemma "P \ Q \ (P \ Q) \ Q"
+ by (rule_twice my_rule: conjI)
+
+
+section \Higher-order methods\
+
+text \
+ The \emph{structured concatenation} combinator ``@{text "method\<^sub>1 ;
+ method\<^sub>2"}'' was introduced in Isabelle2015, motivated by development of
+ Eisbach. It is similar to ``@{text "method\<^sub>1, method\<^sub>2"}'', but @{text
+ method\<^sub>2} is invoked on on \emph{all} subgoals that have newly emerged from
+ @{text method\<^sub>1}. This is useful to handle cases where the number of
+ subgoals produced by a method is determined dynamically at run-time.
+\
+
+ method conj_with uses rule =
+ (intro conjI ; intro rule)
+
+ lemma
+ assumes A: "P"
+ shows "P \ P \ P"
+ by (conj_with rule: A)
+
+text \
+ Method definitions may take other methods as arguments, and thus implement
+ method combinators with prefix syntax. For example, to more usefully exploit
+ Isabelle's backtracking, the explicit requirement that a method solve all
+ produced subgoals is frequently useful. This can easily be written as a
+ \emph{higher-order method} using ``@{text ";"}''. The @{keyword "methods"}
+ keyword denotes method parameters that are other proof methods to be invoked
+ by the method being defined.
+\
+
+ method solve methods m = (m ; fail)
+
+text \
+ Given some method-argument @{text m}, @{text "solve \m\"} applies the
+ method @{text m} and then fails whenever @{text m} produces any new unsolved
+ subgoals --- i.e. when @{text m} fails to completely discharge the goal it
+ was applied to.
+\
+
+
+section \Example\
+
+text \
+ With these simple features we are ready to write our first non-trivial proof
+ method. Returning to the first-order logic example, the following method
+ definition applies various rules with their canonical methods.
+\
+
+ named_theorems subst
+
+ method prop_solver declares intros elims subst =
+ (assumption |
+ (rule intros) | erule elims |
+ subst subst | subst (asm) subst |
+ (erule notE ; solve \prop_solver\))+
+
+text \
+ The only non-trivial part above is the final alternative @{text "(erule notE
+ ; solve \prop_solver\)"}. Here, in the case that all other alternatives
+ fail, the method takes one of the assumptions @{term "\ P"} of the current
+ goal and eliminates it with the rule @{text notE}, causing the goal to be
+ proved to become @{term P}. The method then recursively invokes itself on
+ the remaining goals. The job of the recursive call is to demonstrate that
+ there is a contradiction in the original assumptions (i.e.\ that @{term P}
+ can be derived from them). Note this recursive invocation is applied with
+ the @{method solve} method combinator to ensure that a contradiction will
+ indeed be shown. In the case where a contradiction cannot be found,
+ backtracking will occur and a different assumption @{term "\ Q"} will be
+ chosen for elimination.
+
+ Note that the recursive call to @{method prop_solver} does not have any
+ parameters passed to it. Recall that fact parameters, e.g.\ @{text
+ "intros"}, @{text "elims"}, and @{text "subst"}, are managed by declarations
+ in the current proof context. They will therefore be passed to any recursive
+ call to @{method prop_solver} and, more generally, any invocation of a
+ method which declares these named theorems.
+
+ \medskip After declaring some standard rules to the context, the @{method
+ prop_solver} becomes capable of solving non-trivial propositional
+ tautologies.\
+
+ lemmas [intros] =
+ conjI -- \@{thm conjI}\
+ impI -- \@{thm impI}\
+ disjCI -- \@{thm disjCI}\
+ iffI -- \@{thm iffI}\
+ notI -- \@{thm notI}\
+ (*<*)TrueI(*>*)
+ lemmas [elims] =
+ impCE -- \@{thm impCE}\
+ conjE -- \@{thm conjE}\
+ disjE -- \@{thm disjE}\
+
+ lemma "(A \ B) \ (A \ C) \ (B \ C) \ C"
+ by prop_solver
+
+
+chapter \The match method \label{s:matching}\
+
+text \
+ So far we have seen methods defined as simple combinations of other methods.
+ Some familiar programming language concepts have been introduced (i.e.\
+ abstraction and recursion). The only control flow has been implicitly the
+ result of backtracking. When designing more sophisticated proof methods this
+ proves too restrictive and difficult to manage conceptually.
+
+ To address this, we introduce the @{method_def "match"} method, which
+ provides more direct access to the higher-order matching facility at the
+ core of Isabelle. It is implemented as a separate proof method (in
+ Isabelle/ML), and thus can be directly applied to proofs, however it is most
+ useful when applied in the context of writing Eisbach method definitions.
+
+ \medskip The syntax diagram below refers to some syntactic categories that
+ are further defined in @{cite "isabelle-isar-ref"}.
+
+ @{rail \
+ @@{method match} kind @'in' (pattern '\' cartouche + '\')
+ ;
+ kind:
+ (@'conclusion' | @'premises' ('(' 'local' ')')? |
+ '(' term ')' | @{syntax thmrefs})
+ ;
+ pattern: fact_name? term args? \ (@'for' fixes)?
+ ;
+ fact_name: @{syntax name} @{syntax attributes}? ':'
+ ;
+ args: '(' (('multi' | 'cut' nat?) + ',') ')'
+ \}
+
+ Matching allows methods to introspect the goal state, and to implement more
+ explicit control flow. In the basic case, a term or fact @{text ts} is given
+ to match against as a \emph{match target}, along with a collection of
+ pattern-method pairs @{text "(p, m)"}: roughly speaking, when the pattern
+ @{text p} matches any member of @{text ts}, the \emph{inner} method @{text
+ m} will be executed.
+\
+
+ lemma
+ assumes X:
+ "Q \ P"
+ "Q"
+ shows P
+ by (match X in I: "Q \ P" and I': "Q" \ \insert mp [OF I I']\)
+
+text \
+ In this example we have a structured Isar proof, with the named
+ assumption @{text "X"} and a conclusion @{term "P"}. With the match method
+ we can find the local facts @{term "Q \ P"} and @{term "Q"}, binding them to
+ separately as @{text "I"} and @{text "I'"}. We then specialize the
+ modus-ponens rule @{thm mp [of Q P]} to these facts to solve the goal.
+\
+
+
+section \Subgoal focus\
+
+text\
+ In the previous example we were able to match against an assumption out of
+ the Isar proof state. In general, however, proof subgoals can be
+ \emph{unstructured}, with goal parameters and premises arising from rule
+ application. To address this, @{method match} uses \emph{subgoal focusing}
+ (see also \autoref{s:design}) to produce structured goals out of
+ unstructured ones. In place of fact or term, we may give the
+ keyword @{keyword_def "premises"} as the match target. This causes a subgoal
+ focus on the first subgoal, lifting local goal parameters to fixed term
+ variables and premises into hypothetical theorems. The match is performed
+ against these theorems, naming them and binding them as appropriate.
+ Similarly giving the keyword @{keyword_def "conclusion"} matches against the
+ conclusion of the first subgoal.
+
+ An unstructured version of the previous example can then be similarly solved
+ through focusing.
+\
+
+ lemma "Q \ P \ Q \ P"
+ by (match premises in
+ I: "Q \ P" and I': "Q" \ \insert mp [OF I I']\)
+
+text \
+ Match variables may be specified by giving a list of @{keyword_ref
+ "for"}-fixes after the pattern description. This marks those terms as bound
+ variables, which may be used in the method body.
+\
+
+ lemma "Q \ P \ Q \ P"
+ by (match premises in I: "Q \ A" and I': "Q" for A \
+ \match conclusion in A \ \insert mp [OF I I']\\)
+
+text \
+ In this example @{term A} is a match variable which is bound to @{term P}
+ upon a successful match. The inner @{method match} then matches the
+ now-bound @{term A} (bound to @{term P}) against the conclusion (also @{term
+ P}), finally applying the specialized rule to solve the goal.
+
+ Schematic terms like @{text "?P"} may also be used to specify match
+ variables, but the result of the match is not bound, and thus cannot be used
+ in the inner method body.
+
+ \medskip In the following example we extract the predicate of an
+ existentially quantified conclusion in the current subgoal and search the
+ current premises for a matching fact. If both matches are successful, we
+ then instantiate the existential introduction rule with both the witness and
+ predicate, solving with the matched premise.
+\
+
+ method solve_ex =
+ (match conclusion in "\x. Q x" for Q \
+ \match premises in U: "Q y" for y \
+ \rule exI [where P = Q and x = y, OF U]\\)
+
+text \
+ The first @{method match} matches the pattern @{term "\x. Q x"} against the
+ current conclusion, binding the term @{term "Q"} in the inner match. Next
+ the pattern @{text "Q y"} is matched against all premises of the current
+ subgoal. In this case @{term "Q"} is fixed and @{term "y"} may be
+ instantiated. Once a match is found, the local fact @{text U} is bound to
+ the matching premise and the variable @{term "y"} is bound to the matching
+ witness. The existential introduction rule @{text "exI:"}~@{thm exI} is then
+ instantiated with @{term "y"} as the witness and @{term "Q"} as the
+ predicate, with its proof obligation solved by the local fact U (using the
+ Isar attribute @{attribute OF}). The following example is a trivial use of
+ this method.
+\
+
+ lemma "halts p \ \x. halts x"
+ by solve_ex
+
+
+subsubsection \Operating within a focus\
+
+text \
+ Subgoal focusing provides a structured form of a subgoal, allowing for more
+ expressive introspection of the goal state. This requires some consideration
+ in order to be used effectively. When the keyword @{keyword "premises"} is
+ given as the match target, the premises of the subgoal are lifted into
+ hypothetical theorems, which can be found and named via match patterns.
+ Additionally these premises are stripped from the subgoal, leaving only the
+ conclusion. This renders them inaccessible to standard proof methods which
+ operate on the premises, such as @{method frule} or @{method erule}. Naive
+ usage of these methods within a match will most likely not function as the
+ method author intended.
+\
+
+ method my_allE_bad for y :: 'a =
+ (match premises in I: "\x :: 'a. ?Q x" \
+ \erule allE [where x = y]\)
+
+text \
+ Here we take a single parameter @{term y} and specialize the universal
+ elimination rule (@{thm allE}) to it, then attempt to apply this specialized
+ rule with @{method erule}. The method @{method erule} will attempt to unify
+ with a universal quantifier in the premises that matches the type of @{term
+ y}. Since @{keyword "premises"} causes a focus, however, there are no
+ subgoal premises to be found and thus @{method my_allE_bad} will always
+ fail. If focusing instead left the premises in place, using methods
+ like @{method erule} would lead to unintended behaviour, specifically during
+ backtracking. In our example, @{method erule} could choose an alternate
+ premise while backtracking, while leaving @{text I} bound to the original
+ match. In the case of more complex inner methods, where either @{text I} or
+ bound terms are used, this would almost certainly not be the intended
+ behaviour.
+
+ An alternative implementation would be to specialize the elimination rule to
+ the bound term and apply it directly.
+\
+
+ method my_allE_almost for y :: 'a =
+ (match premises in I: "\x :: 'a. ?Q x" \
+ \rule allE [where x = y, OF I]\)
+
+ lemma "\x. P x \ P y"
+ by (my_allE_almost y)
+
+text \
+ This method will insert a specialized duplicate of a universally quantified
+ premise. Although this will successfully apply in the presence of such a
+ premise, it is not likely the intended behaviour. Repeated application of
+ this method will produce an infinite stream of duplicate specialized
+ premises, due to the original premise never being removed. To address this,
+ matched premises may be declared with the @{attribute "thin"} attribute.
+ This will hide the premise from subsequent inner matches, and remove it from
+ the list of premises when the inner method has finished and the subgoal is
+ unfocused. It can be considered analogous to the existing @{text thin_tac}.
+
+ To complete our example, the correct implementation of the method
+ will @{attribute "thin"} the premise from the match and then apply it to the
+ specialized elimination rule.\
+
+ method my_allE for y :: 'a =
+ (match premises in I [thin]: "\x :: 'a. ?Q x" \
+ \rule allE [where x = y, OF I]\)
+
+ lemma "\x. P x \ \x. Q x \ P y \ Q y"
+ by (my_allE y)+ (rule conjI)
+
+
+subsection \Attributes\
+
+text \
+ Attributes may throw errors when applied to a given fact. For example, rule
+ instantiation will fail of there is a type mismatch or if a given variable
+ doesn't exist. Within a match or a method definition, it isn't generally
+ possible to guarantee that applied attributes won't fail. For example, in
+ the following method there is no guarantee that the two provided facts will
+ necessarily compose.
+\
+
+ method my_compose uses rule1 rule2 =
+ (rule rule1[OF rule2])
+
+text \
+ Some attributes (like @{attribute OF}) have been made partially
+ Eisbach-aware. This means that they are able to form a closure despite not
+ necessarily always being applicable. In the case of @{attribute OF}, it is
+ up to the proof author to guard attribute application with an appropriate
+ @{method match}, but there are still no static guarantees.
+
+ In contrast to @{attribute OF}, the @{attribute "where"} and @{attribute of}
+ attributes attempt to provide static guarantees that they will apply
+ whenever possible.
+
+ Within a match pattern for a fact, each outermost quantifier specifies the
+ requirement that a matching fact must have a schematic variable at that
+ point. This gives a corresponding name to this ``slot'' for the purposes of
+ forming a static closure, allowing the @{attribute "where"} attribute to
+ perform an instantiation at run-time.
+\
+
+ lemma
+ assumes A: "Q \ False"
+ shows "\ Q"
+ by (match intros in X: "\P. (P \ False) \ \ P" \
+ \rule X [where P = Q, OF A]\)
+
+text \
+ Subgoal focusing converts the outermost quantifiers of premises into
+ schematics when lifting them to hypothetical facts. This allows us to
+ instantiate them with @{attribute "where"} when using an appropriate match
+ pattern.
+\
+
+ lemma "(\x :: 'a. A x \ B x) \ A y \ B y"
+ by (match premises in I: "\x :: 'a. ?P x \ ?Q x" \
+ \rule I [where x = y]\)
+
+text \
+ The @{attribute of} attribute behaves similarly. It is worth noting,
+ however, that the positional instantiation of @{attribute of} occurs against
+ the position of the variables as they are declared \emph{in the match
+ pattern}.
+\
+
+ lemma
+ fixes A B and x :: 'a and y :: 'b
+ assumes asm: "(\x y. A y x \ B x y )"
+ shows "A y x \ B x y"
+ by (match asm in I: "\(x :: 'a) (y :: 'b). ?P x y \ ?Q x y" \
+ \rule I [of x y]\)
+
+text \
+ In this example, the order of schematics in @{text asm} is actually @{text
+ "?y ?x"}, but we instantiate our matched rule in the opposite order. This is
+ because the effective rule @{term I} was bound from the match, which
+ declared the @{typ 'a} slot first and the @{typ 'b} slot second.
+
+ To get the dynamic behaviour of @{attribute of} we can choose to invoke it
+ \emph{unchecked}. This avoids trying to do any type inference for the
+ provided parameters, instead storing them as their most general type and
+ doing type matching at run-time. This, like @{attribute OF}, will throw
+ errors if the expected slots don't exist or there is a type mismatch.
+\
+
+ lemma
+ fixes A B and x :: 'a and y :: 'b
+ assumes asm: "\x y. A y x \ B x y"
+ shows "A y x \ B x y"
+ by (match asm in I: "PROP ?P" \ \rule I [of (unchecked) y x]\)
+
+text \
+ Attributes may be applied to matched facts directly as they are matched. Any
+ declarations will therefore be applied in the context of the inner method,
+ as well as any transformations to the rule.
+\
+
+ lemma "(\x :: 'a. A x \ B x) \ A y \ B y"
+ by (match premises in I[of y, intros]: "\x :: 'a. ?P x \ ?Q x" \
+ \prop_solver\)
+
+text \
+ In this example, the pattern @{text "\x :: 'a. ?P x \ ?Q x"} matches against
+ the only premise, giving an appropriately typed slot for @{term y}. After
+ the match, the resulting rule is instantiated to @{term y} and then declared
+ as an @{attribute intros} rule. This is then picked up by @{method
+ prop_solver} to solve the goal.
+\
+
+
+section \Multi-match \label{sec:multi}\
+
+text \
+ In all previous examples, @{method match} was only ever searching for a
+ single rule or premise. Each local fact would therefore always have a length
+ of exactly one. We may, however, wish to find \emph{all} matching results.
+ To achieve this, we can simply mark a given pattern with the @{text
+ "(multi)"} argument.
+\
+
+ lemma
+ assumes asms: "A \ B" "A \ D"
+ shows "(A \ B) \ (A \ D)"
+ apply (match asms in I[intros]: "?P \ ?Q" \