updated Eisbach manual, using version 3149f9146eb5 of its Bitbucket repository;
authorwenzelm
Fri May 22 18:13:31 2015 +0200 (2015-05-22)
changeset 602987c278b692aae
parent 60297 1f9e08394d46
child 60299 5ae2a2e74c93
updated Eisbach manual, using version 3149f9146eb5 of its Bitbucket repository;
src/Doc/Eisbach/Manual.thy
src/Doc/Eisbach/Preface.thy
     1.1 --- a/src/Doc/Eisbach/Manual.thy	Fri May 22 15:13:49 2015 +0200
     1.2 +++ b/src/Doc/Eisbach/Manual.thy	Fri May 22 18:13:31 2015 +0200
     1.3 @@ -102,9 +102,8 @@
     1.4    A @{text "named theorem"} is a fact whose contents are produced dynamically
     1.5    within the current proof context. The Isar command @{command_ref
     1.6    "named_theorems"} provides simple access to this concept: it declares a
     1.7 -  dynamic fact with corresponding \emph{attribute}
     1.8 -  (see \autoref{s:attributes}) for managing this particular data slot in the
     1.9 -  context.
    1.10 +  dynamic fact with corresponding \emph{attribute} for managing
    1.11 +  this particular data slot in the context.
    1.12  \<close>
    1.13  
    1.14      named_theorems intros
    1.15 @@ -178,7 +177,7 @@
    1.16    @{text method\<^sub>1}. This is useful to handle cases where the number of
    1.17    subgoals produced by a method is determined dynamically at run-time.
    1.18  \<close>
    1.19 -
    1.20 +text_raw\<open>\vbox{\<close>
    1.21      method conj_with uses rule =
    1.22        (intro conjI ; intro rule)
    1.23  
    1.24 @@ -186,7 +185,7 @@
    1.25        assumes A: "P"
    1.26        shows "P \<and> P \<and> P"
    1.27        by (conj_with rule: A)
    1.28 -
    1.29 +text_raw\<open>}\<close>
    1.30  text \<open>
    1.31    Method definitions may take other methods as arguments, and thus implement
    1.32    method combinators with prefix syntax. For example, to more usefully exploit
    1.33 @@ -254,7 +253,7 @@
    1.34        disjCI  --  \<open>@{thm disjCI}\<close>
    1.35        iffI  --  \<open>@{thm iffI}\<close>
    1.36        notI  --  \<open>@{thm notI}\<close>
    1.37 -      (*<*)TrueI(*>*)
    1.38 +
    1.39      lemmas [elims] =
    1.40        impCE  --  \<open>@{thm impCE}\<close>
    1.41        conjE  --  \<open>@{thm conjE}\<close>
    1.42 @@ -327,7 +326,7 @@
    1.43    the Isar proof state. In general, however, proof subgoals can be
    1.44    \emph{unstructured}, with goal parameters and premises arising from rule
    1.45    application. To address this, @{method match} uses \emph{subgoal focusing}
    1.46 -  (see also \autoref{s:design}) to produce structured goals out of
    1.47 +  to produce structured goals out of
    1.48    unstructured ones. In place of fact or term, we may give the
    1.49    keyword @{keyword_def "premises"} as the match target. This causes a subgoal
    1.50    focus on the first subgoal, lifting local goal parameters to fixed term
    1.51 @@ -394,7 +393,7 @@
    1.52        by solve_ex
    1.53  
    1.54  
    1.55 -subsubsection \<open>Operating within a focus\<close>
    1.56 +subsection \<open>Operating within a focus\<close>
    1.57  
    1.58  text \<open>
    1.59    Subgoal focusing provides a structured form of a subgoal, allowing for more
    1.60 @@ -461,8 +460,42 @@
    1.61      lemma "\<forall>x. P x \<Longrightarrow> \<forall>x. Q x \<Longrightarrow> P y \<and> Q y"
    1.62        by (my_allE y)+ (rule conjI)
    1.63  
    1.64 +subsubsection \<open>Inner focusing\<close>
    1.65  
    1.66 -subsection \<open>Attributes\<close>
    1.67 +text \<open>
    1.68 +  Premises are \emph{accumulated} for the purposes of subgoal focusing.
    1.69 +  In contrast to using standard methods like @{method frule} within
    1.70 +  focused match, another @{method match} will have access to all the premises
    1.71 +  of the outer focus.
    1.72 +  \<close>
    1.73 +
    1.74 +    lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
    1.75 +      by (match premises in H: A \<Rightarrow> \<open>intro conjI, rule H,
    1.76 +            match premises in H': B \<Rightarrow> \<open>rule H'\<close>\<close>)
    1.77 +
    1.78 +text \<open>
    1.79 +  In this example, the inner @{method match} can find the focused premise
    1.80 +  @{term B}. In contrast, the @{method assumption} method would fail here
    1.81 +  due to @{term B} not being logically accessible.
    1.82 +\<close>
    1.83 +
    1.84 +    lemma
    1.85 +    "A \<Longrightarrow> A \<and> (B \<longrightarrow> B)"
    1.86 +      by (match premises in H: A \<Rightarrow> \<open>intro conjI, rule H, rule impI,
    1.87 +            match premises (local) in A \<Rightarrow> \<open>fail\<close>
    1.88 +                                 \<bar> H': B \<Rightarrow> \<open>rule H'\<close>\<close>)
    1.89 +
    1.90 +text \<open>
    1.91 +  In this example, the only premise that exists in the first focus is
    1.92 +  @{term "A"}. Prior to the inner match, the rule @{text impI} changes
    1.93 +  the goal @{term "B \<longrightarrow> B"} into @{term "B \<Longrightarrow> B"}. A standard premise
    1.94 +  match would also include @{term A} as an original premise of the outer
    1.95 +  match. The @{text local} argument limits the match to
    1.96 +  newly focused premises.
    1.97 +
    1.98 +\<close>
    1.99 +
   1.100 +section \<open>Attributes\<close>
   1.101  
   1.102  text \<open>
   1.103    Attributes may throw errors when applied to a given fact. For example, rule
   1.104 @@ -474,7 +507,7 @@
   1.105  \<close>
   1.106  
   1.107      method my_compose uses rule1 rule2 =
   1.108 -      (rule rule1[OF rule2])
   1.109 +      (rule rule1 [OF rule2])
   1.110  
   1.111  text \<open>
   1.112    Some attributes (like @{attribute OF}) have been made partially
   1.113 @@ -493,13 +526,13 @@
   1.114    forming a static closure, allowing the @{attribute "where"} attribute to
   1.115    perform an instantiation at run-time.
   1.116  \<close>
   1.117 -
   1.118 +text_raw\<open>\vbox{\<close>
   1.119      lemma
   1.120        assumes A: "Q \<Longrightarrow> False"
   1.121        shows "\<not> Q"
   1.122        by (match intros in X: "\<And>P. (P \<Longrightarrow> False) \<Longrightarrow> \<not> P" \<Rightarrow>
   1.123              \<open>rule X [where P = Q, OF A]\<close>)
   1.124 -
   1.125 +text_raw\<open>}\<close>
   1.126  text \<open>
   1.127    Subgoal focusing converts the outermost quantifiers of premises into
   1.128    schematics when lifting them to hypothetical facts. This allows us to
   1.129 @@ -551,7 +584,7 @@
   1.130  \<close>
   1.131  
   1.132      lemma "(\<And>x :: 'a. A x \<Longrightarrow> B x) \<Longrightarrow> A y \<longrightarrow> B y"
   1.133 -      by (match premises in I[of y, intros]: "\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x" \<Rightarrow>
   1.134 +      by (match premises in I [of y, intros]: "\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x" \<Rightarrow>
   1.135              \<open>prop_solver\<close>)
   1.136  
   1.137  text \<open>
   1.138 @@ -574,10 +607,11 @@
   1.139  \<close>
   1.140  
   1.141      lemma
   1.142 -      assumes asms: "A \<Longrightarrow> B" "A \<Longrightarrow> D"
   1.143 +      assumes asms: "A \<Longrightarrow> B"  "A \<Longrightarrow> D"
   1.144        shows "(A \<longrightarrow> B) \<and> (A \<longrightarrow> D)"
   1.145 -      apply (match asms in I[intros]: "?P \<Longrightarrow> ?Q"  \<Rightarrow> \<open>solves \<open>prop_solver\<close>\<close>)?
   1.146 -      by (match asms in I[intros]: "?P \<Longrightarrow> ?Q" (multi) \<Rightarrow> \<open>prop_solver\<close>)
   1.147 +      apply (match asms in I [intros]: "?P \<Longrightarrow> ?Q"  \<Rightarrow> \<open>solves \<open>prop_solver\<close>\<close>)?
   1.148 +      apply (match asms in I [intros]: "?P \<Longrightarrow> ?Q" (multi) \<Rightarrow> \<open>prop_solver\<close>)
   1.149 +      done
   1.150  
   1.151  text \<open>
   1.152    In the first @{method match}, without the @{text "(multi)"} argument, @{term
   1.153 @@ -598,12 +632,13 @@
   1.154  \<close>
   1.155  
   1.156      lemma
   1.157 -      assumes asms: "A \<Longrightarrow> B" "A \<Longrightarrow> D" "D \<Longrightarrow> B"
   1.158 +      assumes asms: "A \<Longrightarrow> B"  "A \<Longrightarrow> D"  "D \<Longrightarrow> B"
   1.159        shows "(A \<longrightarrow> B) \<and> (A \<longrightarrow> D)"
   1.160 -      apply (match asms in I[intros]: "?P \<Longrightarrow> Q" (multi) for Q \<Rightarrow>
   1.161 +      apply (match asms in I [intros]: "?P \<Longrightarrow> Q" (multi) for Q \<Rightarrow>
   1.162                \<open>solves \<open>prop_solver\<close>\<close>)?
   1.163 -      by (match asms in I[intros]: "P \<Longrightarrow> ?Q" (multi) for P \<Rightarrow>
   1.164 +      apply (match asms in I [intros]: "P \<Longrightarrow> ?Q" (multi) for P \<Rightarrow>
   1.165                \<open>prop_solver\<close>)
   1.166 +      done
   1.167  
   1.168  text \<open>
   1.169    Here we have two seemingly-equivalent applications of @{method match},
   1.170 @@ -631,7 +666,7 @@
   1.171      lemma
   1.172        assumes asms: "A &&& B \<Longrightarrow> D"
   1.173        shows "(A \<and> B \<longrightarrow> D)"
   1.174 -      by (match asms in I:_ \<Rightarrow> \<open>prop_solver intros: I conjunctionI\<close>)
   1.175 +      by (match asms in I: _ \<Rightarrow> \<open>prop_solver intros: I conjunctionI\<close>)
   1.176  
   1.177  
   1.178  section \<open>Backtracking\<close>
   1.179 @@ -649,22 +684,17 @@
   1.180  
   1.181    The method @{text foo} below fails for all goals that are conjunctions. Any
   1.182    such goal will match the first pattern, causing the second pattern (that
   1.183 -  would otherwise match all goals) to never be considered. If multiple
   1.184 -  unifiers exist for the pattern @{text "?P \<and> ?Q"} against the current goal,
   1.185 -  then the failing method @{method fail} will be (uselessly) tried for all of
   1.186 -  them.
   1.187 +  would otherwise match all goals) to never be considered.
   1.188  \<close>
   1.189  
   1.190      method foo =
   1.191        (match conclusion in "?P \<and> ?Q" \<Rightarrow> \<open>fail\<close> \<bar> "?R" \<Rightarrow> \<open>prop_solver\<close>)
   1.192  
   1.193  text \<open>
   1.194 -  This behaviour is in direct contrast to the backtracking done by Coq's Ltac,
   1.195 -  which will attempt all patterns in a match before failing. This means that
   1.196 -  the failure of an inner method that is executed after a successful match
   1.197 -  does not, in Ltac, cause the entire match to fail, whereas it does in
   1.198 -  Eisbach. In Eisbach the distinction is important due to the pervasive use of
   1.199 -  backtracking. When a method is used in a combinator chain, its failure
   1.200 +  The failure of an inner method that is executed after a successful match
   1.201 +  will cause the entire match to fail. This distinction is important
   1.202 +  due to the pervasive use of backtracking. When a method is used in a
   1.203 +  combinator chain, its failure
   1.204    becomes significant because it signals previously applied methods to move to
   1.205    the next result. Therefore, it is necessary for @{method match} to not mask
   1.206    such failure. One can always rewrite a match using the combinators ``@{text
   1.207 @@ -713,6 +743,11 @@
   1.208    succeeding after picking @{term "A \<longrightarrow> C"}. In the second lemma, however,
   1.209    @{term "C \<and> D"} is matched first, the second pattern in the match cannot be
   1.210    found and so the method fails, falling through to @{method prop_solver}.
   1.211 +
   1.212 +  More precise control is also possible by giving a positive
   1.213 +  number @{text n} as an argument to @{text cut}. This will limit the number
   1.214 +  of backtracking results of that match to be at most @{text n}.
   1.215 +  The match argument @{text "(cut 1)"} is the same as simply @{text "(cut)"}.
   1.216  \<close>
   1.217  
   1.218  
   1.219 @@ -728,7 +763,7 @@
   1.220  \<close>
   1.221  
   1.222      lemma
   1.223 -      assumes asms: "\<And>x. A x \<and> B x" "\<And>y. A y \<and> C y" "\<And>z. B z \<and> C z"
   1.224 +      assumes asms: "\<And>x. A x \<and> B x"  "\<And>y. A y \<and> C y"  "\<And>z. B z \<and> C z"
   1.225        shows "A x \<and> C x"
   1.226        by (match asms in I: "\<And>x. P x \<and> ?Q x" (multi) for P \<Rightarrow>
   1.227           \<open>match (P) in "A" \<Rightarrow> \<open>fail\<close>
   1.228 @@ -771,21 +806,23 @@
   1.229    via meta-implication @{text "_ \<Longrightarrow> _"}.
   1.230  \<close>
   1.231  
   1.232 +text_raw \<open>\vbox{\<close>
   1.233      lemma
   1.234 -      assumes asms: "D \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> A"
   1.235 +      assumes asms: "D \<Longrightarrow> B \<Longrightarrow> C"  "D \<Longrightarrow> A"
   1.236        shows "D \<Longrightarrow> B \<Longrightarrow> C \<and> A"
   1.237 -      by (match asms in H:"D \<Longrightarrow> _" (multi) \<Rightarrow> \<open>prop_solver elims: H\<close>)
   1.238 -
   1.239 +      by (match asms in H: "D \<Longrightarrow> _" (multi) \<Rightarrow> \<open>prop_solver elims: H\<close>)
   1.240 +text_raw \<open>}\<close>
   1.241  text \<open>
   1.242    For the first member of @{text asms} the dummy pattern successfully matches
   1.243    against @{term "B \<Longrightarrow> C"} and so the proof is successful.
   1.244  \<close>
   1.245  
   1.246      lemma
   1.247 -      assumes asms: "A \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> C"
   1.248 +      assumes asms: "A \<Longrightarrow> B \<Longrightarrow> C"  "D \<Longrightarrow> C"
   1.249        shows "D \<or> (A \<and> B) \<Longrightarrow> C"
   1.250 -      apply (match asms in H:"_ \<Longrightarrow> C" (multi) \<Rightarrow> \<open>prop_solver elims: H\<close>)(*<*)?
   1.251 -      by (prop_solver elims: asms)(*>*)
   1.252 +      apply (match asms in H: "_ \<Longrightarrow> C" (multi) \<Rightarrow> \<open>prop_solver elims: H\<close>)(*<*)?
   1.253 +      apply (prop_solver elims: asms)
   1.254 +      done(*>*)
   1.255  
   1.256  text \<open>
   1.257    This proof will fail to solve the goal. Our match pattern will only match
   1.258 @@ -804,9 +841,9 @@
   1.259  \<close>
   1.260  
   1.261      lemma
   1.262 -      assumes asms: "A \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> C"
   1.263 +      assumes asms: "A \<Longrightarrow> B \<Longrightarrow> C"  "D \<Longrightarrow> C"
   1.264        shows "D \<or> (A \<and> B) \<Longrightarrow> C"
   1.265 -      by (match asms[uncurry] in H[curry]:"_ \<Longrightarrow> C" (multi) \<Rightarrow>
   1.266 +      by (match asms [uncurry] in H [curry]: "_ \<Longrightarrow> C" (multi) \<Rightarrow>
   1.267            \<open>prop_solver elims: H\<close>)
   1.268  
   1.269  
   1.270 @@ -821,9 +858,10 @@
   1.271      lemma
   1.272        assumes asms: "\<And>x :: 'a. A x"
   1.273        shows "A y"
   1.274 -      apply (match asms in H:"A y" \<Rightarrow> \<open>rule H\<close>)?
   1.275 -      by (match asms in H:"P" for P \<Rightarrow>
   1.276 -          \<open>match ("A y") in "P" \<Rightarrow> \<open>rule H\<close>\<close>)
   1.277 +      apply (match asms in H: "A y" \<Rightarrow> \<open>rule H\<close>)?
   1.278 +      apply (match asms in H: P for P \<Rightarrow>
   1.279 +          \<open>match ("A y") in P \<Rightarrow> \<open>rule H\<close>\<close>)
   1.280 +      done
   1.281  
   1.282  text \<open>
   1.283    In the first @{method match} we attempt to find a member of @{text asms}
   1.284 @@ -847,8 +885,8 @@
   1.285      lemma
   1.286        assumes asms: "\<And>x :: 'a. A x"
   1.287        shows "A y"
   1.288 -      by (match asms in H:"\<And>z :: 'b. P z" for P \<Rightarrow>
   1.289 -          \<open>match (y) in "y :: 'b" for y \<Rightarrow> \<open>rule H[where z=y]\<close>\<close>)
   1.290 +      by (match asms in H: "\<And>z :: 'b. P z" for P \<Rightarrow>
   1.291 +          \<open>match (y) in "y :: 'b" for y \<Rightarrow> \<open>rule H [where z = y]\<close>\<close>)
   1.292  
   1.293  text \<open>
   1.294    In this example the type @{text 'b} is matched to @{text 'a}, however
   1.295 @@ -875,8 +913,9 @@
   1.296      lemma
   1.297        assumes asms: A B C D
   1.298        shows D
   1.299 -      apply (match asms in H:_ \<Rightarrow> \<open>print_fact H, fail\<close>)(*<*)?
   1.300 -      by (simp add: asms)(*>*)
   1.301 +      apply (match asms in H: _ \<Rightarrow> \<open>print_fact H, fail\<close>)(*<*)?
   1.302 +      apply (simp add: asms)
   1.303 +      done(*>*)
   1.304  
   1.305  text \<open>
   1.306    This proof will fail, but the tracing output will show the order that the
   1.307 @@ -886,7 +925,7 @@
   1.308  
   1.309  section \<open>Integrating with Isabelle/ML\<close>
   1.310  
   1.311 -subsection \<open>Attributes\<close>
   1.312 +subsubsection \<open>Attributes\<close>
   1.313  
   1.314  text \<open>
   1.315    A custom rule attribute is a simple way to extend the functionality of
   1.316 @@ -905,19 +944,28 @@
   1.317  
   1.318  text \<open>
   1.319    In this example, the new attribute @{attribute get_split_rule} lifts the ML
   1.320 -  function of the same name into an attribute. When applied to a cast
   1.321 +  function of the same name into an attribute. When applied to a case
   1.322    distinction over a datatype, it retrieves its corresponding split rule.
   1.323  
   1.324 -  We can then integrate this intro a method that applies the split rule, fist
   1.325 +  We can then integrate this intro a method that applies the split rule, first
   1.326    matching to ensure that fetching the rule was successful.
   1.327  \<close>
   1.328 -
   1.329 +(*<*)declare TrueI [intros](*>*)
   1.330      method splits =
   1.331        (match conclusion in "?P f" for f \<Rightarrow>
   1.332          \<open>match [[get_split_rule f]] in U: "(_ :: bool) = _" \<Rightarrow>
   1.333 -          \<open>rule U[THEN iffD2]\<close>\<close>)
   1.334 +          \<open>rule U [THEN iffD2]\<close>\<close>)
   1.335  
   1.336      lemma "L \<noteq> [] \<Longrightarrow> case L of [] \<Rightarrow> False | _ \<Rightarrow> True"
   1.337 -      by (splits, prop_solver intros: allI)
   1.338 +      apply splits
   1.339 +      apply (prop_solver intros: allI)
   1.340 +      done
   1.341 +
   1.342 +text \<open>
   1.343 +  Here the new @{method splits} method transforms the goal to use only logical
   1.344 +  connectives: @{term "L = [] \<longrightarrow> False \<and> (\<forall>x y. L = x # y \<longrightarrow> True)"}. This goal
   1.345 +  is then in a form solvable by @{method prop_solver} when given the universal
   1.346 +  quantifier introduction rule @{text allI}.
   1.347 +\<close>
   1.348  
   1.349  end
     2.1 --- a/src/Doc/Eisbach/Preface.thy	Fri May 22 15:13:49 2015 +0200
     2.2 +++ b/src/Doc/Eisbach/Preface.thy	Fri May 22 18:13:31 2015 +0200
     2.3 @@ -12,7 +12,7 @@
     2.4  
     2.5    The core functionality of Eisbach is provided by the Isar @{command method}
     2.6    command. Here users may define new methods by combining existing ones with
     2.7 -  the usual Isar syntax These methods can be abstracted over terms, facts and
     2.8 +  the usual Isar syntax. These methods can be abstracted over terms, facts and
     2.9    other methods, as one might expect in any higher-order functional language.
    2.10  
    2.11    Additional functionality is provided by extending the space of methods and