# HG changeset patch
# User wenzelm
# Date 1432311211 -7200
# Node ID 7c278b692aae516cf376bf8ad52ce2eeb1955fa5
# Parent  1f9e08394d465fd1d208be83ac27127ef3b13a53
updated Eisbach manual, using version 3149f9146eb5 of its Bitbucket repository;

diff -r 1f9e08394d46 -r 7c278b692aae src/Doc/Eisbach/Manual.thy
--- a/src/Doc/Eisbach/Manual.thy	Fri May 22 15:13:49 2015 +0200
+++ b/src/Doc/Eisbach/Manual.thy	Fri May 22 18:13:31 2015 +0200
@@ -102,9 +102,8 @@
   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.
+  dynamic fact with corresponding \emph{attribute} for managing
+  this particular data slot in the context.
 \<close>
 
     named_theorems intros
@@ -178,7 +177,7 @@
   @{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.
 \<close>
-
+text_raw\<open>\vbox{\<close>
     method conj_with uses rule =
       (intro conjI ; intro rule)
 
@@ -186,7 +185,7 @@
       assumes A: "P"
       shows "P \<and> P \<and> P"
       by (conj_with rule: A)
-
+text_raw\<open>}\<close>
 text \<open>
   Method definitions may take other methods as arguments, and thus implement
   method combinators with prefix syntax. For example, to more usefully exploit
@@ -254,7 +253,7 @@
       disjCI  --  \<open>@{thm disjCI}\<close>
       iffI  --  \<open>@{thm iffI}\<close>
       notI  --  \<open>@{thm notI}\<close>
-      (*<*)TrueI(*>*)
+
     lemmas [elims] =
       impCE  --  \<open>@{thm impCE}\<close>
       conjE  --  \<open>@{thm conjE}\<close>
@@ -327,7 +326,7 @@
   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
+  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
@@ -394,7 +393,7 @@
       by solve_ex
 
 
-subsubsection \<open>Operating within a focus\<close>
+subsection \<open>Operating within a focus\<close>
 
 text \<open>
   Subgoal focusing provides a structured form of a subgoal, allowing for more
@@ -461,8 +460,42 @@
     lemma "\<forall>x. P x \<Longrightarrow> \<forall>x. Q x \<Longrightarrow> P y \<and> Q y"
       by (my_allE y)+ (rule conjI)
 
+subsubsection \<open>Inner focusing\<close>
 
-subsection \<open>Attributes\<close>
+text \<open>
+  Premises are \emph{accumulated} for the purposes of subgoal focusing.
+  In contrast to using standard methods like @{method frule} within
+  focused match, another @{method match} will have access to all the premises
+  of the outer focus.
+  \<close>
+
+    lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
+      by (match premises in H: A \<Rightarrow> \<open>intro conjI, rule H,
+            match premises in H': B \<Rightarrow> \<open>rule H'\<close>\<close>)
+
+text \<open>
+  In this example, the inner @{method match} can find the focused premise
+  @{term B}. In contrast, the @{method assumption} method would fail here
+  due to @{term B} not being logically accessible.
+\<close>
+
+    lemma
+    "A \<Longrightarrow> A \<and> (B \<longrightarrow> B)"
+      by (match premises in H: A \<Rightarrow> \<open>intro conjI, rule H, rule impI,
+            match premises (local) in A \<Rightarrow> \<open>fail\<close>
+                                 \<bar> H': B \<Rightarrow> \<open>rule H'\<close>\<close>)
+
+text \<open>
+  In this example, the only premise that exists in the first focus is
+  @{term "A"}. Prior to the inner match, the rule @{text impI} changes
+  the goal @{term "B \<longrightarrow> B"} into @{term "B \<Longrightarrow> B"}. A standard premise
+  match would also include @{term A} as an original premise of the outer
+  match. The @{text local} argument limits the match to
+  newly focused premises.
+
+\<close>
+
+section \<open>Attributes\<close>
 
 text \<open>
   Attributes may throw errors when applied to a given fact. For example, rule
@@ -474,7 +507,7 @@
 \<close>
 
     method my_compose uses rule1 rule2 =
-      (rule rule1[OF rule2])
+      (rule rule1 [OF rule2])
 
 text \<open>
   Some attributes (like @{attribute OF}) have been made partially
@@ -493,13 +526,13 @@
   forming a static closure, allowing the @{attribute "where"} attribute to
   perform an instantiation at run-time.
 \<close>
-
+text_raw\<open>\vbox{\<close>
     lemma
       assumes A: "Q \<Longrightarrow> False"
       shows "\<not> Q"
       by (match intros in X: "\<And>P. (P \<Longrightarrow> False) \<Longrightarrow> \<not> P" \<Rightarrow>
             \<open>rule X [where P = Q, OF A]\<close>)
-
+text_raw\<open>}\<close>
 text \<open>
   Subgoal focusing converts the outermost quantifiers of premises into
   schematics when lifting them to hypothetical facts. This allows us to
@@ -551,7 +584,7 @@
 \<close>
 
     lemma "(\<And>x :: 'a. A x \<Longrightarrow> B x) \<Longrightarrow> A y \<longrightarrow> B y"
-      by (match premises in I[of y, intros]: "\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x" \<Rightarrow>
+      by (match premises in I [of y, intros]: "\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x" \<Rightarrow>
             \<open>prop_solver\<close>)
 
 text \<open>
@@ -574,10 +607,11 @@
 \<close>
 
     lemma
-      assumes asms: "A \<Longrightarrow> B" "A \<Longrightarrow> D"
+      assumes asms: "A \<Longrightarrow> B"  "A \<Longrightarrow> D"
       shows "(A \<longrightarrow> B) \<and> (A \<longrightarrow> D)"
-      apply (match asms in I[intros]: "?P \<Longrightarrow> ?Q"  \<Rightarrow> \<open>solves \<open>prop_solver\<close>\<close>)?
-      by (match asms in I[intros]: "?P \<Longrightarrow> ?Q" (multi) \<Rightarrow> \<open>prop_solver\<close>)
+      apply (match asms in I [intros]: "?P \<Longrightarrow> ?Q"  \<Rightarrow> \<open>solves \<open>prop_solver\<close>\<close>)?
+      apply (match asms in I [intros]: "?P \<Longrightarrow> ?Q" (multi) \<Rightarrow> \<open>prop_solver\<close>)
+      done
 
 text \<open>
   In the first @{method match}, without the @{text "(multi)"} argument, @{term
@@ -598,12 +632,13 @@
 \<close>
 
     lemma
-      assumes asms: "A \<Longrightarrow> B" "A \<Longrightarrow> D" "D \<Longrightarrow> B"
+      assumes asms: "A \<Longrightarrow> B"  "A \<Longrightarrow> D"  "D \<Longrightarrow> B"
       shows "(A \<longrightarrow> B) \<and> (A \<longrightarrow> D)"
-      apply (match asms in I[intros]: "?P \<Longrightarrow> Q" (multi) for Q \<Rightarrow>
+      apply (match asms in I [intros]: "?P \<Longrightarrow> Q" (multi) for Q \<Rightarrow>
               \<open>solves \<open>prop_solver\<close>\<close>)?
-      by (match asms in I[intros]: "P \<Longrightarrow> ?Q" (multi) for P \<Rightarrow>
+      apply (match asms in I [intros]: "P \<Longrightarrow> ?Q" (multi) for P \<Rightarrow>
               \<open>prop_solver\<close>)
+      done
 
 text \<open>
   Here we have two seemingly-equivalent applications of @{method match},
@@ -631,7 +666,7 @@
     lemma
       assumes asms: "A &&& B \<Longrightarrow> D"
       shows "(A \<and> B \<longrightarrow> D)"
-      by (match asms in I:_ \<Rightarrow> \<open>prop_solver intros: I conjunctionI\<close>)
+      by (match asms in I: _ \<Rightarrow> \<open>prop_solver intros: I conjunctionI\<close>)
 
 
 section \<open>Backtracking\<close>
@@ -649,22 +684,17 @@
 
   The method @{text foo} below fails for all goals that are conjunctions. Any
   such goal will match the first pattern, causing the second pattern (that
-  would otherwise match all goals) to never be considered. If multiple
-  unifiers exist for the pattern @{text "?P \<and> ?Q"} against the current goal,
-  then the failing method @{method fail} will be (uselessly) tried for all of
-  them.
+  would otherwise match all goals) to never be considered.
 \<close>
 
     method foo =
       (match conclusion in "?P \<and> ?Q" \<Rightarrow> \<open>fail\<close> \<bar> "?R" \<Rightarrow> \<open>prop_solver\<close>)
 
 text \<open>
-  This behaviour is in direct contrast to the backtracking done by Coq's Ltac,
-  which will attempt all patterns in a match before failing. This means that
-  the failure of an inner method that is executed after a successful match
-  does not, in Ltac, cause the entire match to fail, whereas it does in
-  Eisbach. In Eisbach the distinction is important due to the pervasive use of
-  backtracking. When a method is used in a combinator chain, its failure
+  The failure of an inner method that is executed after a successful match
+  will cause the entire match to fail. This distinction is important
+  due to the pervasive use of backtracking. When a method is used in a
+  combinator chain, its failure
   becomes significant because it signals previously applied methods to move to
   the next result. Therefore, it is necessary for @{method match} to not mask
   such failure. One can always rewrite a match using the combinators ``@{text
@@ -713,6 +743,11 @@
   succeeding after picking @{term "A \<longrightarrow> C"}. In the second lemma, however,
   @{term "C \<and> D"} is matched first, the second pattern in the match cannot be
   found and so the method fails, falling through to @{method prop_solver}.
+
+  More precise control is also possible by giving a positive
+  number @{text n} as an argument to @{text cut}. This will limit the number
+  of backtracking results of that match to be at most @{text n}.
+  The match argument @{text "(cut 1)"} is the same as simply @{text "(cut)"}.
 \<close>
 
 
@@ -728,7 +763,7 @@
 \<close>
 
     lemma
-      assumes asms: "\<And>x. A x \<and> B x" "\<And>y. A y \<and> C y" "\<And>z. B z \<and> C z"
+      assumes asms: "\<And>x. A x \<and> B x"  "\<And>y. A y \<and> C y"  "\<And>z. B z \<and> C z"
       shows "A x \<and> C x"
       by (match asms in I: "\<And>x. P x \<and> ?Q x" (multi) for P \<Rightarrow>
          \<open>match (P) in "A" \<Rightarrow> \<open>fail\<close>
@@ -771,21 +806,23 @@
   via meta-implication @{text "_ \<Longrightarrow> _"}.
 \<close>
 
+text_raw \<open>\vbox{\<close>
     lemma
-      assumes asms: "D \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> A"
+      assumes asms: "D \<Longrightarrow> B \<Longrightarrow> C"  "D \<Longrightarrow> A"
       shows "D \<Longrightarrow> B \<Longrightarrow> C \<and> A"
-      by (match asms in H:"D \<Longrightarrow> _" (multi) \<Rightarrow> \<open>prop_solver elims: H\<close>)
-
+      by (match asms in H: "D \<Longrightarrow> _" (multi) \<Rightarrow> \<open>prop_solver elims: H\<close>)
+text_raw \<open>}\<close>
 text \<open>
   For the first member of @{text asms} the dummy pattern successfully matches
   against @{term "B \<Longrightarrow> C"} and so the proof is successful.
 \<close>
 
     lemma
-      assumes asms: "A \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> C"
+      assumes asms: "A \<Longrightarrow> B \<Longrightarrow> C"  "D \<Longrightarrow> C"
       shows "D \<or> (A \<and> B) \<Longrightarrow> C"
-      apply (match asms in H:"_ \<Longrightarrow> C" (multi) \<Rightarrow> \<open>prop_solver elims: H\<close>)(*<*)?
-      by (prop_solver elims: asms)(*>*)
+      apply (match asms in H: "_ \<Longrightarrow> C" (multi) \<Rightarrow> \<open>prop_solver elims: H\<close>)(*<*)?
+      apply (prop_solver elims: asms)
+      done(*>*)
 
 text \<open>
   This proof will fail to solve the goal. Our match pattern will only match
@@ -804,9 +841,9 @@
 \<close>
 
     lemma
-      assumes asms: "A \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> C"
+      assumes asms: "A \<Longrightarrow> B \<Longrightarrow> C"  "D \<Longrightarrow> C"
       shows "D \<or> (A \<and> B) \<Longrightarrow> C"
-      by (match asms[uncurry] in H[curry]:"_ \<Longrightarrow> C" (multi) \<Rightarrow>
+      by (match asms [uncurry] in H [curry]: "_ \<Longrightarrow> C" (multi) \<Rightarrow>
           \<open>prop_solver elims: H\<close>)
 
 
@@ -821,9 +858,10 @@
     lemma
       assumes asms: "\<And>x :: 'a. A x"
       shows "A y"
-      apply (match asms in H:"A y" \<Rightarrow> \<open>rule H\<close>)?
-      by (match asms in H:"P" for P \<Rightarrow>
-          \<open>match ("A y") in "P" \<Rightarrow> \<open>rule H\<close>\<close>)
+      apply (match asms in H: "A y" \<Rightarrow> \<open>rule H\<close>)?
+      apply (match asms in H: P for P \<Rightarrow>
+          \<open>match ("A y") in P \<Rightarrow> \<open>rule H\<close>\<close>)
+      done
 
 text \<open>
   In the first @{method match} we attempt to find a member of @{text asms}
@@ -847,8 +885,8 @@
     lemma
       assumes asms: "\<And>x :: 'a. A x"
       shows "A y"
-      by (match asms in H:"\<And>z :: 'b. P z" for P \<Rightarrow>
-          \<open>match (y) in "y :: 'b" for y \<Rightarrow> \<open>rule H[where z=y]\<close>\<close>)
+      by (match asms in H: "\<And>z :: 'b. P z" for P \<Rightarrow>
+          \<open>match (y) in "y :: 'b" for y \<Rightarrow> \<open>rule H [where z = y]\<close>\<close>)
 
 text \<open>
   In this example the type @{text 'b} is matched to @{text 'a}, however
@@ -875,8 +913,9 @@
     lemma
       assumes asms: A B C D
       shows D
-      apply (match asms in H:_ \<Rightarrow> \<open>print_fact H, fail\<close>)(*<*)?
-      by (simp add: asms)(*>*)
+      apply (match asms in H: _ \<Rightarrow> \<open>print_fact H, fail\<close>)(*<*)?
+      apply (simp add: asms)
+      done(*>*)
 
 text \<open>
   This proof will fail, but the tracing output will show the order that the
@@ -886,7 +925,7 @@
 
 section \<open>Integrating with Isabelle/ML\<close>
 
-subsection \<open>Attributes\<close>
+subsubsection \<open>Attributes\<close>
 
 text \<open>
   A custom rule attribute is a simple way to extend the functionality of
@@ -905,19 +944,28 @@
 
 text \<open>
   In this example, the new attribute @{attribute get_split_rule} lifts the ML
-  function of the same name into an attribute. When applied to a cast
+  function of the same name into an attribute. When applied to a case
   distinction over a datatype, it retrieves its corresponding split rule.
 
-  We can then integrate this intro a method that applies the split rule, fist
+  We can then integrate this intro a method that applies the split rule, first
   matching to ensure that fetching the rule was successful.
 \<close>
-
+(*<*)declare TrueI [intros](*>*)
     method splits =
       (match conclusion in "?P f" for f \<Rightarrow>
         \<open>match [[get_split_rule f]] in U: "(_ :: bool) = _" \<Rightarrow>
-          \<open>rule U[THEN iffD2]\<close>\<close>)
+          \<open>rule U [THEN iffD2]\<close>\<close>)
 
     lemma "L \<noteq> [] \<Longrightarrow> case L of [] \<Rightarrow> False | _ \<Rightarrow> True"
-      by (splits, prop_solver intros: allI)
+      apply splits
+      apply (prop_solver intros: allI)
+      done
+
+text \<open>
+  Here the new @{method splits} method transforms the goal to use only logical
+  connectives: @{term "L = [] \<longrightarrow> False \<and> (\<forall>x y. L = x # y \<longrightarrow> True)"}. This goal
+  is then in a form solvable by @{method prop_solver} when given the universal
+  quantifier introduction rule @{text allI}.
+\<close>
 
 end
diff -r 1f9e08394d46 -r 7c278b692aae src/Doc/Eisbach/Preface.thy
--- a/src/Doc/Eisbach/Preface.thy	Fri May 22 15:13:49 2015 +0200
+++ b/src/Doc/Eisbach/Preface.thy	Fri May 22 18:13:31 2015 +0200
@@ -12,7 +12,7 @@
 
   The core functionality of Eisbach is provided by the Isar @{command method}
   command. Here users may define new methods by combining existing ones with
-  the usual Isar syntax These methods can be abstracted over terms, facts and
+  the usual Isar syntax. These methods can be abstracted over terms, facts and
   other methods, as one might expect in any higher-order functional language.
 
   Additional functionality is provided by extending the space of methods and