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