author | wenzelm |

Sun May 17 23:03:49 2015 +0200 (2015-05-17) | |

changeset 60288 | d7f636331176 |

parent 60287 | adde5ce1e0a7 |

child 60289 | 1fb026be7536 |

added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;

1.1 --- a/NEWS Sun May 17 22:33:34 2015 +0200 1.2 +++ b/NEWS Sun May 17 23:03:49 2015 +0200 1.3 @@ -63,8 +63,9 @@ 1.4 by combining existing ones with their usual syntax. The "match" proof 1.5 method provides basic fact/term matching in addition to 1.6 premise/conclusion matching through Subgoal.focus, and binds fact names 1.7 -from matches as well as term patterns within matches. See also 1.8 -~~/src/HOL/Eisbach/Eisbach.thy and the included examples. 1.9 +from matches as well as term patterns within matches. The Isabelle 1.10 +documentation provides an entry "eisbach" for the Eisbach User Manual. 1.11 +Sources and various examples are in ~~/src/HOL/Eisbach/. 1.12 1.13 1.14 *** Prover IDE -- Isabelle/Scala/jEdit ***

2.1 --- a/doc/Contents Sun May 17 22:33:34 2015 +0200 2.2 +++ b/doc/Contents Sun May 17 23:03:49 2015 +0200 2.3 @@ -8,6 +8,7 @@ 2.4 codegen Tutorial on Code Generation 2.5 nitpick User's Guide to Nitpick 2.6 sledgehammer User's Guide to Sledgehammer 2.7 + eisbach The Eisbach User Manual 2.8 sugar LaTeX Sugar for Isabelle documents 2.9 2.10 Reference Manuals!

3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 3.2 +++ b/src/Doc/Eisbach/Base.thy Sun May 17 23:03:49 2015 +0200 3.3 @@ -0,0 +1,39 @@ 3.4 +section \<open>Basic setup that is not included in the document\<close> 3.5 + 3.6 +theory Base 3.7 +imports Main 3.8 +begin 3.9 + 3.10 +ML_file "~~/src/Doc/antiquote_setup.ML" 3.11 + 3.12 +ML\<open> 3.13 +fun get_split_rule ctxt target = 3.14 + let 3.15 + val (head, args) = strip_comb (Envir.eta_contract target); 3.16 + val (const_name, _) = dest_Const head; 3.17 + val const_name_components = Long_Name.explode const_name; 3.18 + 3.19 + val _ = 3.20 + if String.isPrefix "case_" (List.last const_name_components) then () 3.21 + else raise TERM ("Not a case statement", [target]); 3.22 + 3.23 + val type_name = Long_Name.implode (rev (tl (rev const_name_components))); 3.24 + val split = Proof_Context.get_thm ctxt (type_name ^ ".split"); 3.25 + val vars = Term.add_vars (Thm.prop_of split) []; 3.26 + 3.27 + val datatype_name = nth (rev const_name_components) 1; 3.28 + 3.29 + fun is_datatype (Type (a, _)) = Long_Name.base_name a = Long_Name.base_name datatype_name 3.30 + | is_datatype _ = false; 3.31 + 3.32 + val datatype_var = 3.33 + (case find_first (fn (_, T') => is_datatype T') vars of 3.34 + SOME var => Thm.cterm_of ctxt (Term.Var var) 3.35 + | NONE => error ("Couldn't find datatype in thm: " ^ datatype_name)); 3.36 + in 3.37 + SOME (Drule.cterm_instantiate [(datatype_var, Thm.cterm_of ctxt (List.last args))] split) 3.38 + end 3.39 + handle TERM _ => NONE; 3.40 +\<close> 3.41 + 3.42 +end

4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 4.2 +++ b/src/Doc/Eisbach/Manual.thy Sun May 17 23:03:49 2015 +0200 4.3 @@ -0,0 +1,923 @@ 4.4 +(*:wrap=hard:maxLineLen=78:*) 4.5 + 4.6 +theory Manual 4.7 +imports Base "../Eisbach_Tools" 4.8 +begin 4.9 + 4.10 +chapter \<open>The method command\<close> 4.11 + 4.12 +text \<open> 4.13 + The @{command_def method} command provides the ability to write proof 4.14 + methods by combining existing ones with their usual syntax. Specifically it 4.15 + allows compound proof methods to be named, and to extend the name space of 4.16 + basic methods accordingly. Method definitions may abstract over parameters: 4.17 + terms, facts, or other methods. 4.18 + 4.19 + \medskip The syntax diagram below refers to some syntactic categories that 4.20 + are further defined in @{cite "isabelle-isar-ref"}. 4.21 + 4.22 + @{rail \<open> 4.23 + @@{command method} name args @'=' method 4.24 + ; 4.25 + args: term_args? method_args? \<newline> fact_args? decl_args? 4.26 + ; 4.27 + term_args: @'for' @{syntax "fixes"} 4.28 + ; 4.29 + method_args: @'methods' (name+) 4.30 + ; 4.31 + fact_args: @'uses' (name+) 4.32 + ; 4.33 + decl_args: @'declares' (name+) 4.34 + \<close>} 4.35 +\<close> 4.36 + 4.37 + 4.38 +section \<open>Basic method definitions\<close> 4.39 + 4.40 +text \<open> 4.41 + Consider the following proof that makes use of usual Isar method 4.42 + combinators. 4.43 +\<close> 4.44 + 4.45 + lemma "P \<and> Q \<longrightarrow> P" 4.46 + by ((rule impI, (erule conjE)?) | assumption)+ 4.47 + 4.48 +text \<open> 4.49 + It is clear that this compound method will be applicable in more cases than 4.50 + this proof alone. With the @{command method} command we can define a proof 4.51 + method that makes the above functionality available generally. 4.52 +\<close> 4.53 + 4.54 + method prop_solver\<^sub>1 = 4.55 + ((rule impI, (erule conjE)?) | assumption)+ 4.56 + 4.57 + lemma "P \<and> Q \<and> R \<longrightarrow> P" 4.58 + by prop_solver\<^sub>1 4.59 + 4.60 +text \<open> 4.61 + In this example, the facts @{text impI} and @{text conjE} are static. They 4.62 + are evaluated once when the method is defined and cannot be changed later. 4.63 + This makes the method stable in the sense of \emph{static scoping}: naming 4.64 + another fact @{text impI} in a later context won't affect the behaviour of 4.65 + @{text "prop_solver\<^sub>1"}. 4.66 +\<close> 4.67 + 4.68 + 4.69 +section \<open>Term abstraction\<close> 4.70 + 4.71 +text \<open> 4.72 + Methods can also abstract over terms using the @{keyword_def "for"} keyword, 4.73 + optionally providing type constraints. For instance, the following proof 4.74 + method @{text intro_ex} takes a term @{term y} of any type, which it uses to 4.75 + instantiate the @{term x}-variable of @{text exI} (existential introduction) 4.76 + before applying the result as a rule. The instantiation is performed here by 4.77 + Isar's @{attribute_ref "where"} attribute. If the current subgoal is to find 4.78 + a witness for the given predicate @{term Q}, then this has the effect of 4.79 + committing to @{term y}. 4.80 +\<close> 4.81 + 4.82 + method intro_ex for Q :: "'a \<Rightarrow> bool" and y :: 'a = 4.83 + (rule exI ["where" P = Q and x = y]) 4.84 + 4.85 + 4.86 +text \<open> 4.87 + The term parameters @{term y} and @{term Q} can be used arbitrarily inside 4.88 + the method body, as part of attribute applications or arguments to other 4.89 + methods. The expression is type-checked as far as possible when the method 4.90 + is defined, however dynamic type errors can still occur when it is invoked 4.91 + (e.g.\ when terms are instantiated in a parameterized fact). Actual term 4.92 + arguments are supplied positionally, in the same order as in the method 4.93 + definition. 4.94 +\<close> 4.95 + 4.96 + lemma "P a \<Longrightarrow> \<exists>x. P x" 4.97 + by (intro_ex P a) 4.98 + 4.99 + 4.100 +section \<open>Fact abstraction\<close> 4.101 + 4.102 +subsection \<open>Named theorems\<close> 4.103 + 4.104 +text \<open> 4.105 + A @{text "named theorem"} is a fact whose contents are produced dynamically 4.106 + within the current proof context. The Isar command @{command_ref 4.107 + "named_theorems"} provides simple access to this concept: it declares a 4.108 + dynamic fact with corresponding \emph{attribute} 4.109 + (see \autoref{s:attributes}) for managing this particular data slot in the 4.110 + context. 4.111 +\<close> 4.112 + 4.113 + named_theorems intros 4.114 + 4.115 +text \<open> 4.116 + So far @{text "intros"} refers to the empty fact. Using the Isar command 4.117 + @{command_ref "declare"} we may apply declaration attributes to the context. 4.118 + Below we declare both @{text "conjI"} and @{text "impI"} as @{text 4.119 + "intros"}, adding them to the named theorem slot. 4.120 +\<close> 4.121 + 4.122 + declare conjI [intros] and impI [intros] 4.123 + 4.124 +text \<open> 4.125 + We can refer to named theorems as dynamic facts within a particular proof 4.126 + context, which are evaluated whenever the method is invoked. Instead of 4.127 + having facts hard-coded into the method, as in @{text prop_solver\<^sub>1}, we can 4.128 + instead refer to these named theorems. 4.129 +\<close> 4.130 + 4.131 + named_theorems elims 4.132 + declare conjE [elims] 4.133 + 4.134 + method prop_solver\<^sub>3 = 4.135 + ((rule intros, (erule elims)?) | assumption)+ 4.136 + 4.137 + lemma "P \<and> Q \<longrightarrow> P" 4.138 + by prop_solver\<^sub>3 4.139 + 4.140 +text \<open> 4.141 + Often these named theorems need to be augmented on the spot, when a method 4.142 + is invoked. The @{keyword_def "declares"} keyword in the signature of 4.143 + @{command method} adds the common method syntax @{text "method decl: facts"} 4.144 + for each named theorem @{text decl}. 4.145 +\<close> 4.146 + 4.147 + method prop_solver\<^sub>4 declares intros elims = 4.148 + ((rule intros, (erule elims)?) | assumption)+ 4.149 + 4.150 + lemma "P \<and> (P \<longrightarrow> Q) \<longrightarrow> Q \<and> P" 4.151 + by (prop_solver\<^sub>4 elims: impE intros: conjI) 4.152 + 4.153 + 4.154 +subsection \<open>Simple fact abstraction\<close> 4.155 + 4.156 +text \<open> 4.157 + The @{keyword "declares"} keyword requires that a corresponding dynamic fact 4.158 + has been declared with @{command_ref named_theorems}. This is useful for 4.159 + managing collections of facts which are to be augmented with declarations, 4.160 + but is overkill if we simply want to pass a fact to a method. 4.161 + 4.162 + We may use the @{keyword_def "uses"} keyword in the method header to provide 4.163 + a simple fact parameter. In contrast to @{keyword "declares"}, these facts 4.164 + are always implicitly empty unless augmented when the method is invoked. 4.165 +\<close> 4.166 + 4.167 + method rule_twice uses my_rule = 4.168 + (rule my_rule, rule my_rule) 4.169 + 4.170 + lemma "P \<Longrightarrow> Q \<Longrightarrow> (P \<and> Q) \<and> Q" 4.171 + by (rule_twice my_rule: conjI) 4.172 + 4.173 + 4.174 +section \<open>Higher-order methods\<close> 4.175 + 4.176 +text \<open> 4.177 + The \emph{structured concatenation} combinator ``@{text "method\<^sub>1 ; 4.178 + method\<^sub>2"}'' was introduced in Isabelle2015, motivated by development of 4.179 + Eisbach. It is similar to ``@{text "method\<^sub>1, method\<^sub>2"}'', but @{text 4.180 + method\<^sub>2} is invoked on on \emph{all} subgoals that have newly emerged from 4.181 + @{text method\<^sub>1}. This is useful to handle cases where the number of 4.182 + subgoals produced by a method is determined dynamically at run-time. 4.183 +\<close> 4.184 + 4.185 + method conj_with uses rule = 4.186 + (intro conjI ; intro rule) 4.187 + 4.188 + lemma 4.189 + assumes A: "P" 4.190 + shows "P \<and> P \<and> P" 4.191 + by (conj_with rule: A) 4.192 + 4.193 +text \<open> 4.194 + Method definitions may take other methods as arguments, and thus implement 4.195 + method combinators with prefix syntax. For example, to more usefully exploit 4.196 + Isabelle's backtracking, the explicit requirement that a method solve all 4.197 + produced subgoals is frequently useful. This can easily be written as a 4.198 + \emph{higher-order method} using ``@{text ";"}''. The @{keyword "methods"} 4.199 + keyword denotes method parameters that are other proof methods to be invoked 4.200 + by the method being defined. 4.201 +\<close> 4.202 + 4.203 + method solve methods m = (m ; fail) 4.204 + 4.205 +text \<open> 4.206 + Given some method-argument @{text m}, @{text "solve \<open>m\<close>"} applies the 4.207 + method @{text m} and then fails whenever @{text m} produces any new unsolved 4.208 + subgoals --- i.e. when @{text m} fails to completely discharge the goal it 4.209 + was applied to. 4.210 +\<close> 4.211 + 4.212 + 4.213 +section \<open>Example\<close> 4.214 + 4.215 +text \<open> 4.216 + With these simple features we are ready to write our first non-trivial proof 4.217 + method. Returning to the first-order logic example, the following method 4.218 + definition applies various rules with their canonical methods. 4.219 +\<close> 4.220 + 4.221 + named_theorems subst 4.222 + 4.223 + method prop_solver declares intros elims subst = 4.224 + (assumption | 4.225 + (rule intros) | erule elims | 4.226 + subst subst | subst (asm) subst | 4.227 + (erule notE ; solve \<open>prop_solver\<close>))+ 4.228 + 4.229 +text \<open> 4.230 + The only non-trivial part above is the final alternative @{text "(erule notE 4.231 + ; solve \<open>prop_solver\<close>)"}. Here, in the case that all other alternatives 4.232 + fail, the method takes one of the assumptions @{term "\<not> P"} of the current 4.233 + goal and eliminates it with the rule @{text notE}, causing the goal to be 4.234 + proved to become @{term P}. The method then recursively invokes itself on 4.235 + the remaining goals. The job of the recursive call is to demonstrate that 4.236 + there is a contradiction in the original assumptions (i.e.\ that @{term P} 4.237 + can be derived from them). Note this recursive invocation is applied with 4.238 + the @{method solve} method combinator to ensure that a contradiction will 4.239 + indeed be shown. In the case where a contradiction cannot be found, 4.240 + backtracking will occur and a different assumption @{term "\<not> Q"} will be 4.241 + chosen for elimination. 4.242 + 4.243 + Note that the recursive call to @{method prop_solver} does not have any 4.244 + parameters passed to it. Recall that fact parameters, e.g.\ @{text 4.245 + "intros"}, @{text "elims"}, and @{text "subst"}, are managed by declarations 4.246 + in the current proof context. They will therefore be passed to any recursive 4.247 + call to @{method prop_solver} and, more generally, any invocation of a 4.248 + method which declares these named theorems. 4.249 + 4.250 + \medskip After declaring some standard rules to the context, the @{method 4.251 + prop_solver} becomes capable of solving non-trivial propositional 4.252 + tautologies.\<close> 4.253 + 4.254 + lemmas [intros] = 4.255 + conjI -- \<open>@{thm conjI}\<close> 4.256 + impI -- \<open>@{thm impI}\<close> 4.257 + disjCI -- \<open>@{thm disjCI}\<close> 4.258 + iffI -- \<open>@{thm iffI}\<close> 4.259 + notI -- \<open>@{thm notI}\<close> 4.260 + (*<*)TrueI(*>*) 4.261 + lemmas [elims] = 4.262 + impCE -- \<open>@{thm impCE}\<close> 4.263 + conjE -- \<open>@{thm conjE}\<close> 4.264 + disjE -- \<open>@{thm disjE}\<close> 4.265 + 4.266 + lemma "(A \<or> B) \<and> (A \<longrightarrow> C) \<and> (B \<longrightarrow> C) \<longrightarrow> C" 4.267 + by prop_solver 4.268 + 4.269 + 4.270 +chapter \<open>The match method \label{s:matching}\<close> 4.271 + 4.272 +text \<open> 4.273 + So far we have seen methods defined as simple combinations of other methods. 4.274 + Some familiar programming language concepts have been introduced (i.e.\ 4.275 + abstraction and recursion). The only control flow has been implicitly the 4.276 + result of backtracking. When designing more sophisticated proof methods this 4.277 + proves too restrictive and difficult to manage conceptually. 4.278 + 4.279 + To address this, we introduce the @{method_def "match"} method, which 4.280 + provides more direct access to the higher-order matching facility at the 4.281 + core of Isabelle. It is implemented as a separate proof method (in 4.282 + Isabelle/ML), and thus can be directly applied to proofs, however it is most 4.283 + useful when applied in the context of writing Eisbach method definitions. 4.284 + 4.285 + \medskip The syntax diagram below refers to some syntactic categories that 4.286 + are further defined in @{cite "isabelle-isar-ref"}. 4.287 + 4.288 + @{rail \<open> 4.289 + @@{method match} kind @'in' (pattern '\<Rightarrow>' cartouche + '\<bar>') 4.290 + ; 4.291 + kind: 4.292 + (@'conclusion' | @'premises' ('(' 'local' ')')? | 4.293 + '(' term ')' | @{syntax thmrefs}) 4.294 + ; 4.295 + pattern: fact_name? term args? \<newline> (@'for' fixes)? 4.296 + ; 4.297 + fact_name: @{syntax name} @{syntax attributes}? ':' 4.298 + ; 4.299 + args: '(' (('multi' | 'cut' nat?) + ',') ')' 4.300 + \<close>} 4.301 + 4.302 + Matching allows methods to introspect the goal state, and to implement more 4.303 + explicit control flow. In the basic case, a term or fact @{text ts} is given 4.304 + to match against as a \emph{match target}, along with a collection of 4.305 + pattern-method pairs @{text "(p, m)"}: roughly speaking, when the pattern 4.306 + @{text p} matches any member of @{text ts}, the \emph{inner} method @{text 4.307 + m} will be executed. 4.308 +\<close> 4.309 + 4.310 + lemma 4.311 + assumes X: 4.312 + "Q \<longrightarrow> P" 4.313 + "Q" 4.314 + shows P 4.315 + by (match X in I: "Q \<longrightarrow> P" and I': "Q" \<Rightarrow> \<open>insert mp [OF I I']\<close>) 4.316 + 4.317 +text \<open> 4.318 + In this example we have a structured Isar proof, with the named 4.319 + assumption @{text "X"} and a conclusion @{term "P"}. With the match method 4.320 + we can find the local facts @{term "Q \<longrightarrow> P"} and @{term "Q"}, binding them to 4.321 + separately as @{text "I"} and @{text "I'"}. We then specialize the 4.322 + modus-ponens rule @{thm mp [of Q P]} to these facts to solve the goal. 4.323 +\<close> 4.324 + 4.325 + 4.326 +section \<open>Subgoal focus\<close> 4.327 + 4.328 +text\<open> 4.329 + In the previous example we were able to match against an assumption out of 4.330 + the Isar proof state. In general, however, proof subgoals can be 4.331 + \emph{unstructured}, with goal parameters and premises arising from rule 4.332 + application. To address this, @{method match} uses \emph{subgoal focusing} 4.333 + (see also \autoref{s:design}) to produce structured goals out of 4.334 + unstructured ones. In place of fact or term, we may give the 4.335 + keyword @{keyword_def "premises"} as the match target. This causes a subgoal 4.336 + focus on the first subgoal, lifting local goal parameters to fixed term 4.337 + variables and premises into hypothetical theorems. The match is performed 4.338 + against these theorems, naming them and binding them as appropriate. 4.339 + Similarly giving the keyword @{keyword_def "conclusion"} matches against the 4.340 + conclusion of the first subgoal. 4.341 + 4.342 + An unstructured version of the previous example can then be similarly solved 4.343 + through focusing. 4.344 +\<close> 4.345 + 4.346 + lemma "Q \<longrightarrow> P \<Longrightarrow> Q \<Longrightarrow> P" 4.347 + by (match premises in 4.348 + I: "Q \<longrightarrow> P" and I': "Q" \<Rightarrow> \<open>insert mp [OF I I']\<close>) 4.349 + 4.350 +text \<open> 4.351 + Match variables may be specified by giving a list of @{keyword_ref 4.352 + "for"}-fixes after the pattern description. This marks those terms as bound 4.353 + variables, which may be used in the method body. 4.354 +\<close> 4.355 + 4.356 + lemma "Q \<longrightarrow> P \<Longrightarrow> Q \<Longrightarrow> P" 4.357 + by (match premises in I: "Q \<longrightarrow> A" and I': "Q" for A \<Rightarrow> 4.358 + \<open>match conclusion in A \<Rightarrow> \<open>insert mp [OF I I']\<close>\<close>) 4.359 + 4.360 +text \<open> 4.361 + In this example @{term A} is a match variable which is bound to @{term P} 4.362 + upon a successful match. The inner @{method match} then matches the 4.363 + now-bound @{term A} (bound to @{term P}) against the conclusion (also @{term 4.364 + P}), finally applying the specialized rule to solve the goal. 4.365 + 4.366 + Schematic terms like @{text "?P"} may also be used to specify match 4.367 + variables, but the result of the match is not bound, and thus cannot be used 4.368 + in the inner method body. 4.369 + 4.370 + \medskip In the following example we extract the predicate of an 4.371 + existentially quantified conclusion in the current subgoal and search the 4.372 + current premises for a matching fact. If both matches are successful, we 4.373 + then instantiate the existential introduction rule with both the witness and 4.374 + predicate, solving with the matched premise. 4.375 +\<close> 4.376 + 4.377 + method solve_ex = 4.378 + (match conclusion in "\<exists>x. Q x" for Q \<Rightarrow> 4.379 + \<open>match premises in U: "Q y" for y \<Rightarrow> 4.380 + \<open>rule exI [where P = Q and x = y, OF U]\<close>\<close>) 4.381 + 4.382 +text \<open> 4.383 + The first @{method match} matches the pattern @{term "\<exists>x. Q x"} against the 4.384 + current conclusion, binding the term @{term "Q"} in the inner match. Next 4.385 + the pattern @{text "Q y"} is matched against all premises of the current 4.386 + subgoal. In this case @{term "Q"} is fixed and @{term "y"} may be 4.387 + instantiated. Once a match is found, the local fact @{text U} is bound to 4.388 + the matching premise and the variable @{term "y"} is bound to the matching 4.389 + witness. The existential introduction rule @{text "exI:"}~@{thm exI} is then 4.390 + instantiated with @{term "y"} as the witness and @{term "Q"} as the 4.391 + predicate, with its proof obligation solved by the local fact U (using the 4.392 + Isar attribute @{attribute OF}). The following example is a trivial use of 4.393 + this method. 4.394 +\<close> 4.395 + 4.396 + lemma "halts p \<Longrightarrow> \<exists>x. halts x" 4.397 + by solve_ex 4.398 + 4.399 + 4.400 +subsubsection \<open>Operating within a focus\<close> 4.401 + 4.402 +text \<open> 4.403 + Subgoal focusing provides a structured form of a subgoal, allowing for more 4.404 + expressive introspection of the goal state. This requires some consideration 4.405 + in order to be used effectively. When the keyword @{keyword "premises"} is 4.406 + given as the match target, the premises of the subgoal are lifted into 4.407 + hypothetical theorems, which can be found and named via match patterns. 4.408 + Additionally these premises are stripped from the subgoal, leaving only the 4.409 + conclusion. This renders them inaccessible to standard proof methods which 4.410 + operate on the premises, such as @{method frule} or @{method erule}. Naive 4.411 + usage of these methods within a match will most likely not function as the 4.412 + method author intended. 4.413 +\<close> 4.414 + 4.415 + method my_allE_bad for y :: 'a = 4.416 + (match premises in I: "\<forall>x :: 'a. ?Q x" \<Rightarrow> 4.417 + \<open>erule allE [where x = y]\<close>) 4.418 + 4.419 +text \<open> 4.420 + Here we take a single parameter @{term y} and specialize the universal 4.421 + elimination rule (@{thm allE}) to it, then attempt to apply this specialized 4.422 + rule with @{method erule}. The method @{method erule} will attempt to unify 4.423 + with a universal quantifier in the premises that matches the type of @{term 4.424 + y}. Since @{keyword "premises"} causes a focus, however, there are no 4.425 + subgoal premises to be found and thus @{method my_allE_bad} will always 4.426 + fail. If focusing instead left the premises in place, using methods 4.427 + like @{method erule} would lead to unintended behaviour, specifically during 4.428 + backtracking. In our example, @{method erule} could choose an alternate 4.429 + premise while backtracking, while leaving @{text I} bound to the original 4.430 + match. In the case of more complex inner methods, where either @{text I} or 4.431 + bound terms are used, this would almost certainly not be the intended 4.432 + behaviour. 4.433 + 4.434 + An alternative implementation would be to specialize the elimination rule to 4.435 + the bound term and apply it directly. 4.436 +\<close> 4.437 + 4.438 + method my_allE_almost for y :: 'a = 4.439 + (match premises in I: "\<forall>x :: 'a. ?Q x" \<Rightarrow> 4.440 + \<open>rule allE [where x = y, OF I]\<close>) 4.441 + 4.442 + lemma "\<forall>x. P x \<Longrightarrow> P y" 4.443 + by (my_allE_almost y) 4.444 + 4.445 +text \<open> 4.446 + This method will insert a specialized duplicate of a universally quantified 4.447 + premise. Although this will successfully apply in the presence of such a 4.448 + premise, it is not likely the intended behaviour. Repeated application of 4.449 + this method will produce an infinite stream of duplicate specialized 4.450 + premises, due to the original premise never being removed. To address this, 4.451 + matched premises may be declared with the @{attribute "thin"} attribute. 4.452 + This will hide the premise from subsequent inner matches, and remove it from 4.453 + the list of premises when the inner method has finished and the subgoal is 4.454 + unfocused. It can be considered analogous to the existing @{text thin_tac}. 4.455 + 4.456 + To complete our example, the correct implementation of the method 4.457 + will @{attribute "thin"} the premise from the match and then apply it to the 4.458 + specialized elimination rule.\<close> 4.459 + 4.460 + method my_allE for y :: 'a = 4.461 + (match premises in I [thin]: "\<forall>x :: 'a. ?Q x" \<Rightarrow> 4.462 + \<open>rule allE [where x = y, OF I]\<close>) 4.463 + 4.464 + lemma "\<forall>x. P x \<Longrightarrow> \<forall>x. Q x \<Longrightarrow> P y \<and> Q y" 4.465 + by (my_allE y)+ (rule conjI) 4.466 + 4.467 + 4.468 +subsection \<open>Attributes\<close> 4.469 + 4.470 +text \<open> 4.471 + Attributes may throw errors when applied to a given fact. For example, rule 4.472 + instantiation will fail of there is a type mismatch or if a given variable 4.473 + doesn't exist. Within a match or a method definition, it isn't generally 4.474 + possible to guarantee that applied attributes won't fail. For example, in 4.475 + the following method there is no guarantee that the two provided facts will 4.476 + necessarily compose. 4.477 +\<close> 4.478 + 4.479 + method my_compose uses rule1 rule2 = 4.480 + (rule rule1[OF rule2]) 4.481 + 4.482 +text \<open> 4.483 + Some attributes (like @{attribute OF}) have been made partially 4.484 + Eisbach-aware. This means that they are able to form a closure despite not 4.485 + necessarily always being applicable. In the case of @{attribute OF}, it is 4.486 + up to the proof author to guard attribute application with an appropriate 4.487 + @{method match}, but there are still no static guarantees. 4.488 + 4.489 + In contrast to @{attribute OF}, the @{attribute "where"} and @{attribute of} 4.490 + attributes attempt to provide static guarantees that they will apply 4.491 + whenever possible. 4.492 + 4.493 + Within a match pattern for a fact, each outermost quantifier specifies the 4.494 + requirement that a matching fact must have a schematic variable at that 4.495 + point. This gives a corresponding name to this ``slot'' for the purposes of 4.496 + forming a static closure, allowing the @{attribute "where"} attribute to 4.497 + perform an instantiation at run-time. 4.498 +\<close> 4.499 + 4.500 + lemma 4.501 + assumes A: "Q \<Longrightarrow> False" 4.502 + shows "\<not> Q" 4.503 + by (match intros in X: "\<And>P. (P \<Longrightarrow> False) \<Longrightarrow> \<not> P" \<Rightarrow> 4.504 + \<open>rule X [where P = Q, OF A]\<close>) 4.505 + 4.506 +text \<open> 4.507 + Subgoal focusing converts the outermost quantifiers of premises into 4.508 + schematics when lifting them to hypothetical facts. This allows us to 4.509 + instantiate them with @{attribute "where"} when using an appropriate match 4.510 + pattern. 4.511 +\<close> 4.512 + 4.513 + lemma "(\<And>x :: 'a. A x \<Longrightarrow> B x) \<Longrightarrow> A y \<Longrightarrow> B y" 4.514 + by (match premises in I: "\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x" \<Rightarrow> 4.515 + \<open>rule I [where x = y]\<close>) 4.516 + 4.517 +text \<open> 4.518 + The @{attribute of} attribute behaves similarly. It is worth noting, 4.519 + however, that the positional instantiation of @{attribute of} occurs against 4.520 + the position of the variables as they are declared \emph{in the match 4.521 + pattern}. 4.522 +\<close> 4.523 + 4.524 + lemma 4.525 + fixes A B and x :: 'a and y :: 'b 4.526 + assumes asm: "(\<And>x y. A y x \<Longrightarrow> B x y )" 4.527 + shows "A y x \<Longrightarrow> B x y" 4.528 + by (match asm in I: "\<And>(x :: 'a) (y :: 'b). ?P x y \<Longrightarrow> ?Q x y" \<Rightarrow> 4.529 + \<open>rule I [of x y]\<close>) 4.530 + 4.531 +text \<open> 4.532 + In this example, the order of schematics in @{text asm} is actually @{text 4.533 + "?y ?x"}, but we instantiate our matched rule in the opposite order. This is 4.534 + because the effective rule @{term I} was bound from the match, which 4.535 + declared the @{typ 'a} slot first and the @{typ 'b} slot second. 4.536 + 4.537 + To get the dynamic behaviour of @{attribute of} we can choose to invoke it 4.538 + \emph{unchecked}. This avoids trying to do any type inference for the 4.539 + provided parameters, instead storing them as their most general type and 4.540 + doing type matching at run-time. This, like @{attribute OF}, will throw 4.541 + errors if the expected slots don't exist or there is a type mismatch. 4.542 +\<close> 4.543 + 4.544 + lemma 4.545 + fixes A B and x :: 'a and y :: 'b 4.546 + assumes asm: "\<And>x y. A y x \<Longrightarrow> B x y" 4.547 + shows "A y x \<Longrightarrow> B x y" 4.548 + by (match asm in I: "PROP ?P" \<Rightarrow> \<open>rule I [of (unchecked) y x]\<close>) 4.549 + 4.550 +text \<open> 4.551 + Attributes may be applied to matched facts directly as they are matched. Any 4.552 + declarations will therefore be applied in the context of the inner method, 4.553 + as well as any transformations to the rule. 4.554 +\<close> 4.555 + 4.556 + lemma "(\<And>x :: 'a. A x \<Longrightarrow> B x) \<Longrightarrow> A y \<longrightarrow> B y" 4.557 + by (match premises in I[of y, intros]: "\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x" \<Rightarrow> 4.558 + \<open>prop_solver\<close>) 4.559 + 4.560 +text \<open> 4.561 + In this example, the pattern @{text "\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x"} matches against 4.562 + the only premise, giving an appropriately typed slot for @{term y}. After 4.563 + the match, the resulting rule is instantiated to @{term y} and then declared 4.564 + as an @{attribute intros} rule. This is then picked up by @{method 4.565 + prop_solver} to solve the goal. 4.566 +\<close> 4.567 + 4.568 + 4.569 +section \<open>Multi-match \label{sec:multi}\<close> 4.570 + 4.571 +text \<open> 4.572 + In all previous examples, @{method match} was only ever searching for a 4.573 + single rule or premise. Each local fact would therefore always have a length 4.574 + of exactly one. We may, however, wish to find \emph{all} matching results. 4.575 + To achieve this, we can simply mark a given pattern with the @{text 4.576 + "(multi)"} argument. 4.577 +\<close> 4.578 + 4.579 + lemma 4.580 + assumes asms: "A \<Longrightarrow> B" "A \<Longrightarrow> D" 4.581 + shows "(A \<longrightarrow> B) \<and> (A \<longrightarrow> D)" 4.582 + apply (match asms in I[intros]: "?P \<Longrightarrow> ?Q" \<Rightarrow> \<open>solves \<open>prop_solver\<close>\<close>)? 4.583 + by (match asms in I[intros]: "?P \<Longrightarrow> ?Q" (multi) \<Rightarrow> \<open>prop_solver\<close>) 4.584 + 4.585 +text \<open> 4.586 + In the first @{method match}, without the @{text "(multi)"} argument, @{term 4.587 + I} is only ever be bound to one of the members of @{text asms}. This 4.588 + backtracks over both possibilities (see next section), however neither 4.589 + assumption in isolation is sufficient to solve to goal. The use of the 4.590 + @{method solves} combinator ensures that @{method prop_solver} has no effect 4.591 + on the goal when it doesn't solve it, and so the first match leaves the goal 4.592 + unchanged. In the second @{method match}, @{text I} is bound to all of 4.593 + @{text asms}, declaring both results as @{text intros}. With these rules 4.594 + @{method prop_solver} is capable of solving the goal. 4.595 + 4.596 + Using for-fixed variables in patterns imposes additional constraints on the 4.597 + results. In all previous examples, the choice of using @{text ?P} or a 4.598 + for-fixed @{term P} only depended on whether or not @{term P} was mentioned 4.599 + in another pattern or the inner method. When using a multi-match, however, 4.600 + all for-fixed terms must agree in the results. 4.601 +\<close> 4.602 + 4.603 + lemma 4.604 + assumes asms: "A \<Longrightarrow> B" "A \<Longrightarrow> D" "D \<Longrightarrow> B" 4.605 + shows "(A \<longrightarrow> B) \<and> (A \<longrightarrow> D)" 4.606 + apply (match asms in I[intros]: "?P \<Longrightarrow> Q" (multi) for Q \<Rightarrow> 4.607 + \<open>solves \<open>prop_solver\<close>\<close>)? 4.608 + by (match asms in I[intros]: "P \<Longrightarrow> ?Q" (multi) for P \<Rightarrow> 4.609 + \<open>prop_solver\<close>) 4.610 + 4.611 +text \<open> 4.612 + Here we have two seemingly-equivalent applications of @{method match}, 4.613 + however only the second one is capable of solving the goal. The first 4.614 + @{method match} selects the first and third members of @{text asms} (those 4.615 + that agree on their conclusion), which is not sufficient. The second 4.616 + @{method match} selects the first and second members of @{text asms} (those 4.617 + that agree on their assumption), which is enough for @{method prop_solver} 4.618 + to solve the goal. 4.619 +\<close> 4.620 + 4.621 + 4.622 +section \<open>Dummy patterns\<close> 4.623 + 4.624 +text \<open> 4.625 + Dummy patterns may be given as placeholders for unique schematics in 4.626 + patterns. They implicitly receive all currently bound variables as 4.627 + arguments, and are coerced into the @{typ prop} type whenever possible. For 4.628 + example, the trivial dummy pattern @{text "_"} will match any proposition. 4.629 + In contrast, by default the pattern @{text "?P"} is considered to have type 4.630 + @{typ bool}. It will not bind anything with meta-logical connectives (e.g. 4.631 + @{text "_ \<Longrightarrow> _"} or @{text "_ &&& _"}). 4.632 +\<close> 4.633 + 4.634 + lemma 4.635 + assumes asms: "A &&& B \<Longrightarrow> D" 4.636 + shows "(A \<and> B \<longrightarrow> D)" 4.637 + by (match asms in I:_ \<Rightarrow> \<open>prop_solver intros: I conjunctionI\<close>) 4.638 + 4.639 + 4.640 +section \<open>Backtracking\<close> 4.641 + 4.642 +text \<open> 4.643 + Patterns are considered top-down, executing the inner method @{text m} of 4.644 + the first pattern which is satisfied by the current match target. By 4.645 + default, matching performs extensive backtracking by attempting all valid 4.646 + variable and fact bindings according to the given pattern. In particular, 4.647 + all unifiers for a given pattern will be explored, as well as each matching 4.648 + fact. The inner method @{text m} will be re-executed for each different 4.649 + variable/fact binding during backtracking. A successful match is considered 4.650 + a cut-point for backtracking. Specifically, once a match is made no other 4.651 + pattern-method pairs will be considered. 4.652 + 4.653 + The method @{text foo} below fails for all goals that are conjunctions. Any 4.654 + such goal will match the first pattern, causing the second pattern (that 4.655 + would otherwise match all goals) to never be considered. If multiple 4.656 + unifiers exist for the pattern @{text "?P \<and> ?Q"} against the current goal, 4.657 + then the failing method @{method fail} will be (uselessly) tried for all of 4.658 + them. 4.659 +\<close> 4.660 + 4.661 + method foo = 4.662 + (match conclusion in "?P \<and> ?Q" \<Rightarrow> \<open>fail\<close> \<bar> "?R" \<Rightarrow> \<open>prop_solver\<close>) 4.663 + 4.664 +text \<open> 4.665 + This behaviour is in direct contrast to the backtracking done by Coq's Ltac, 4.666 + which will attempt all patterns in a match before failing. This means that 4.667 + the failure of an inner method that is executed after a successful match 4.668 + does not, in Ltac, cause the entire match to fail, whereas it does in 4.669 + Eisbach. In Eisbach the distinction is important due to the pervasive use of 4.670 + backtracking. When a method is used in a combinator chain, its failure 4.671 + becomes significant because it signals previously applied methods to move to 4.672 + the next result. Therefore, it is necessary for @{method match} to not mask 4.673 + such failure. One can always rewrite a match using the combinators ``@{text 4.674 + "?"}'' and ``@{text "|"}'' to try subsequent patterns in the case of an 4.675 + inner-method failure. The following proof method, for example, always 4.676 + invokes @{method prop_solver} for all goals because its first alternative 4.677 + either never matches or (if it does match) always fails. 4.678 +\<close> 4.679 + 4.680 + method foo\<^sub>1 = 4.681 + (match conclusion in "?P \<and> ?Q" \<Rightarrow> \<open>fail\<close>) | 4.682 + (match conclusion in "?R" \<Rightarrow> \<open>prop_solver\<close>) 4.683 + 4.684 + 4.685 +subsection \<open>Cut\<close> 4.686 + 4.687 +text \<open> 4.688 + Backtracking may be controlled more precisely by marking individual patterns 4.689 + as \emph{cut}. This causes backtracking to not progress beyond this pattern: 4.690 + once a match is found no others will be considered. 4.691 +\<close> 4.692 + 4.693 + method foo\<^sub>2 = 4.694 + (match premises in I: "P \<and> Q" (cut) and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> 4.695 + \<open>rule mp [OF I' I [THEN conjunct1]]\<close>) 4.696 + 4.697 +text \<open> 4.698 + In this example, once a conjunction is found (@{term "P \<and> Q"}), all possible 4.699 + implications of @{term "P"} in the premises are considered, evaluating the 4.700 + inner @{method rule} with each consequent. No other conjunctions will be 4.701 + considered, with method failure occurring once all implications of the 4.702 + form @{text "P \<longrightarrow> ?U"} have been explored. Here the left-right processing of 4.703 + individual patterns is important, as all patterns after of the cut will 4.704 + maintain their usual backtracking behaviour. 4.705 +\<close> 4.706 + 4.707 + lemma "A \<and> B \<Longrightarrow> A \<longrightarrow> D \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> C" 4.708 + by foo\<^sub>2 4.709 + 4.710 + lemma "C \<and> D \<Longrightarrow> A \<and> B \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> C" 4.711 + by (foo\<^sub>2 | prop_solver) 4.712 + 4.713 +text \<open> 4.714 + In this example, the first lemma is solved by @{text foo\<^sub>2}, by first 4.715 + picking @{term "A \<longrightarrow> D"} for @{text I'}, then backtracking and ultimately 4.716 + succeeding after picking @{term "A \<longrightarrow> C"}. In the second lemma, however, 4.717 + @{term "C \<and> D"} is matched first, the second pattern in the match cannot be 4.718 + found and so the method fails, falling through to @{method prop_solver}. 4.719 +\<close> 4.720 + 4.721 + 4.722 +subsection \<open>Multi-match revisited\<close> 4.723 + 4.724 +text \<open> 4.725 + A multi-match will produce a sequence of potential bindings for for-fixed 4.726 + variables, where each binding environment is the result of matching against 4.727 + at least one element from the match target. For each environment, the match 4.728 + result will be all elements of the match target which agree with the pattern 4.729 + under that environment. This can result in unexpected behaviour when giving 4.730 + very general patterns. 4.731 +\<close> 4.732 + 4.733 + lemma 4.734 + assumes asms: "\<And>x. A x \<and> B x" "\<And>y. A y \<and> C y" "\<And>z. B z \<and> C z" 4.735 + shows "A x \<and> C x" 4.736 + by (match asms in I: "\<And>x. P x \<and> ?Q x" (multi) for P \<Rightarrow> 4.737 + \<open>match (P) in "A" \<Rightarrow> \<open>fail\<close> 4.738 + \<bar> _ \<Rightarrow> \<open>match I in "\<And>x. A x \<and> B x" \<Rightarrow> \<open>fail\<close> 4.739 + \<bar> _ \<Rightarrow> \<open>rule I\<close>\<close>\<close>) 4.740 + 4.741 +text \<open> 4.742 + Intuitively it seems like this proof should fail to check. The first match 4.743 + result, which binds @{term I} to the first two members of @{text asms}, 4.744 + fails the second inner match due to binding @{term P} to @{term A}. 4.745 + Backtracking then attempts to bind @{term I} to the third member of @{text 4.746 + asms}. This passes all inner matches, but fails when @{method rule} cannot 4.747 + successfully apply this to the current goal. After this, a valid match that 4.748 + is produced by the unifier is one which binds @{term P} to simply @{text 4.749 + "\<lambda>a. A ?x"}. The first inner match succeeds because @{text "\<lambda>a. A ?x"} does 4.750 + not match @{term A}. The next inner match succeeds because @{term I} has 4.751 + only been bound to the first member of @{text asms}. This is due to @{method 4.752 + match} considering @{text "\<lambda>a. A ?x"} and @{text "\<lambda>a. A ?y"} as distinct 4.753 + terms. 4.754 + 4.755 + The simplest way to address this is to explicitly disallow term bindings 4.756 + which we would consider invalid. 4.757 +\<close> 4.758 + 4.759 + method abs_used for P = 4.760 + (match (P) in "\<lambda>a. ?P" \<Rightarrow> \<open>fail\<close> \<bar> _ \<Rightarrow> \<open>-\<close>) 4.761 + 4.762 +text \<open> 4.763 + This method has no effect on the goal state, but instead serves as a filter 4.764 + on the environment produced from match. 4.765 +\<close> 4.766 + 4.767 + 4.768 +section \<open>Uncurrying\<close> 4.769 + 4.770 +text \<open> 4.771 + The @{method match} method is not aware of the logical content of match 4.772 + targets. Each pattern is simply matched against the shallow structure of a 4.773 + fact or term. Most facts are in \emph{normal form}, which curries premises 4.774 + via meta-implication @{text "_ \<Longrightarrow> _"}. 4.775 +\<close> 4.776 + 4.777 + lemma 4.778 + assumes asms: "D \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> A" 4.779 + shows "D \<Longrightarrow> B \<Longrightarrow> C \<and> A" 4.780 + by (match asms in H:"D \<Longrightarrow> _" (multi) \<Rightarrow> \<open>prop_solver elims: H\<close>) 4.781 + 4.782 +text \<open> 4.783 + For the first member of @{text asms} the dummy pattern successfully matches 4.784 + against @{term "B \<Longrightarrow> C"} and so the proof is successful. 4.785 +\<close> 4.786 + 4.787 + lemma 4.788 + assumes asms: "A \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> C" 4.789 + shows "D \<or> (A \<and> B) \<Longrightarrow> C" 4.790 + apply (match asms in H:"_ \<Longrightarrow> C" (multi) \<Rightarrow> \<open>prop_solver elims: H\<close>)(*<*)? 4.791 + by (prop_solver elims: asms)(*>*) 4.792 + 4.793 +text \<open> 4.794 + This proof will fail to solve the goal. Our match pattern will only match 4.795 + rules which have a single premise, and conclusion @{term C}, so the first 4.796 + member of @{text asms} is not bound and thus the proof fails. Matching a 4.797 + pattern of the form @{term "P \<Longrightarrow> Q"} against this fact will bind @{term "P"} 4.798 + to @{term "A"} and @{term Q} to @{term "B \<Longrightarrow> C"}. Our pattern, with a 4.799 + concrete @{term "C"} in the conclusion, will fail to match this fact. 4.800 + 4.801 + To express our desired match, we may \emph{uncurry} our rules before 4.802 + matching against them. This forms a meta-conjunction of all premises in a 4.803 + fact, so that only one implication remains. For example the uncurried 4.804 + version of @{term "A \<Longrightarrow> B \<Longrightarrow> C"} is @{term "A &&& B \<Longrightarrow> C"}. This will now match 4.805 + our desired pattern @{text "_ \<Longrightarrow> C"}, and can be \emph{curried} after the 4.806 + match to put it back into normal form. 4.807 +\<close> 4.808 + 4.809 + lemma 4.810 + assumes asms: "A \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> C" 4.811 + shows "D \<or> (A \<and> B) \<Longrightarrow> C" 4.812 + by (match asms[uncurry] in H[curry]:"_ \<Longrightarrow> C" (multi) \<Rightarrow> 4.813 + \<open>prop_solver elims: H\<close>) 4.814 + 4.815 + 4.816 +section \<open>Reverse matching\<close> 4.817 + 4.818 +text \<open> 4.819 + The @{method match} method only attempts to perform matching of the pattern 4.820 + against the match target. Specifically this means that it will not 4.821 + instantiate schematic terms in the match target. 4.822 +\<close> 4.823 + 4.824 + lemma 4.825 + assumes asms: "\<And>x :: 'a. A x" 4.826 + shows "A y" 4.827 + apply (match asms in H:"A y" \<Rightarrow> \<open>rule H\<close>)? 4.828 + by (match asms in H:"P" for P \<Rightarrow> 4.829 + \<open>match ("A y") in "P" \<Rightarrow> \<open>rule H\<close>\<close>) 4.830 + 4.831 +text \<open> 4.832 + In the first @{method match} we attempt to find a member of @{text asms} 4.833 + which matches our goal precisely. This fails due to no such member existing. 4.834 + The second match reverses the role of the fact in the match, by first giving 4.835 + a general pattern @{term P}. This bound pattern is then matched against 4.836 + @{term "A y"}. In this case, @{term P} is bound to @{text "A ?x"} and so it 4.837 + successfully matches. 4.838 +\<close> 4.839 + 4.840 + 4.841 +section \<open>Type matching\<close> 4.842 + 4.843 +text \<open> 4.844 + The rule instantiation attributes @{attribute "where"} and @{attribute "of"} 4.845 + attempt to guarantee type-correctness wherever possible. This can require 4.846 + additional invocations of @{method match} in order to statically ensure that 4.847 + instantiation will succeed. 4.848 +\<close> 4.849 + 4.850 + lemma 4.851 + assumes asms: "\<And>x :: 'a. A x" 4.852 + shows "A y" 4.853 + by (match asms in H:"\<And>z :: 'b. P z" for P \<Rightarrow> 4.854 + \<open>match (y) in "y :: 'b" for y \<Rightarrow> \<open>rule H[where z=y]\<close>\<close>) 4.855 + 4.856 +text \<open> 4.857 + In this example the type @{text 'b} is matched to @{text 'a}, however 4.858 + statically they are formally distinct types. The first match binds @{text 4.859 + 'b} while the inner match serves to coerce @{term y} into having the type 4.860 + @{text 'b}. This allows the rule instantiation to successfully apply. 4.861 +\<close> 4.862 + 4.863 + 4.864 +chapter \<open>Method development\<close> 4.865 + 4.866 +section \<open>Tracing methods\<close> 4.867 + 4.868 +text \<open> 4.869 + Method tracing is supported by auxiliary print methods provided by @{theory 4.870 + Eisbach_Tools}. These include @{method print_fact}, @{method print_term} and 4.871 + @{method print_type}. Whenever a print method is evaluated it leaves the 4.872 + goal unchanged and writes its argument as tracing output. 4.873 + 4.874 + Print methods can be combined with the @{method fail} method to investigate 4.875 + the backtracking behaviour of a method. 4.876 +\<close> 4.877 + 4.878 + lemma 4.879 + assumes asms: A B C D 4.880 + shows D 4.881 + apply (match asms in H:_ \<Rightarrow> \<open>print_fact H, fail\<close>)(*<*)? 4.882 + by (simp add: asms)(*>*) 4.883 + 4.884 +text \<open> 4.885 + This proof will fail, but the tracing output will show the order that the 4.886 + assumptions are attempted. 4.887 +\<close> 4.888 + 4.889 + 4.890 +section \<open>Integrating with Isabelle/ML\<close> 4.891 + 4.892 +subsection \<open>Attributes\<close> 4.893 + 4.894 +text \<open> 4.895 + A custom rule attribute is a simple way to extend the functionality of 4.896 + Eisbach methods. The dummy rule attribute notation (@{text "[[ _ ]]"}) 4.897 + invokes the given attribute against a dummy fact and evaluates to the result 4.898 + of that attribute. When used as a match target, this can serve as an 4.899 + effective auxiliary function. 4.900 +\<close> 4.901 + 4.902 + attribute_setup get_split_rule = 4.903 + \<open>Args.term >> (fn t => 4.904 + Thm.rule_attribute (fn context => fn _ => 4.905 + (case get_split_rule (Context.proof_of context) t of 4.906 + SOME thm => thm 4.907 + | NONE => Drule.dummy_thm)))\<close> 4.908 + 4.909 +text \<open> 4.910 + In this example, the new attribute @{attribute get_split_rule} lifts the ML 4.911 + function of the same name into an attribute. When applied to a cast 4.912 + distinction over a datatype, it retrieves its corresponding split rule. 4.913 + 4.914 + We can then integrate this intro a method that applies the split rule, fist 4.915 + matching to ensure that fetching the rule was successful. 4.916 +\<close> 4.917 + 4.918 + method splits = 4.919 + (match conclusion in "?P f" for f \<Rightarrow> 4.920 + \<open>match [[get_split_rule f]] in U: "(_ :: bool) = _" \<Rightarrow> 4.921 + \<open>rule U[THEN iffD2]\<close>\<close>) 4.922 + 4.923 + lemma "L \<noteq> [] \<Longrightarrow> case L of [] \<Rightarrow> False | _ \<Rightarrow> True" 4.924 + by (splits, prop_solver intros: allI) 4.925 + 4.926 +end

5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 5.2 +++ b/src/Doc/Eisbach/Preface.thy Sun May 17 23:03:49 2015 +0200 5.3 @@ -0,0 +1,35 @@ 5.4 +(*:wrap=hard:maxLineLen=78:*) 5.5 + 5.6 +theory Preface 5.7 +imports Base "../Eisbach_Tools" 5.8 +begin 5.9 + 5.10 +text \<open> 5.11 + \emph{Eisbach} is a collection of tools which form the basis for defining 5.12 + new proof methods in Isabelle/Isar~@{cite "Wenzel-PhD"}. It can be thought 5.13 + of as a ``proof method language'', but is more precisely an infrastructure 5.14 + for defining new proof methods out of existing ones. 5.15 + 5.16 + The core functionality of Eisbach is provided by the Isar @{command method} 5.17 + command. Here users may define new methods by combining existing ones with 5.18 + the usual Isar syntax These methods can be abstracted over terms, facts and 5.19 + other methods, as one might expect in any higher-order functional language. 5.20 + 5.21 + Additional functionality is provided by extending the space of methods and 5.22 + attributes. The new @{method match} method allows for explicit control-flow, 5.23 + by taking a match target and a list of pattern-method pairs. By using the 5.24 + functionality provided by Eisbach, additional support methods can be easily 5.25 + written. For example, the @{method catch} method, which provides basic 5.26 + try-catch functionality, only requires a few lines of ML. 5.27 + 5.28 + Eisbach is meant to allow users to write automation using only Isar syntax. 5.29 + Traditionally proof methods have been written in Isabelle/ML, which poses a 5.30 + high barrier-to-entry for many users. 5.31 + 5.32 + \medskip This manual is written for users familiar with Isabelle/Isar, but 5.33 + not necessarily Isabelle/ML. It covers the usage of the @{command method} as 5.34 + well as the @{method match} method, as well as discussing their integration 5.35 + with existing Isar concepts such as @{command named_theorems}. 5.36 +\<close> 5.37 + 5.38 +end 5.39 \ No newline at end of file

6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 6.2 +++ b/src/Doc/Eisbach/document/build Sun May 17 23:03:49 2015 +0200 6.3 @@ -0,0 +1,10 @@ 6.4 +#!/usr/bin/env bash 6.5 + 6.6 +set -e 6.7 + 6.8 +FORMAT="$1" 6.9 +VARIANT="$2" 6.10 + 6.11 +"$ISABELLE_TOOL" logo Eisbach 6.12 +"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" 6.13 +

7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 7.2 +++ b/src/Doc/Eisbach/document/root.tex Sun May 17 23:03:49 2015 +0200 7.3 @@ -0,0 +1,88 @@ 7.4 +\documentclass[12pt,a4paper,fleqn]{report} 7.5 +\usepackage[T1]{fontenc} 7.6 +\usepackage{latexsym,graphicx} 7.7 +\usepackage[refpage]{nomencl} 7.8 +\usepackage{iman,extra,isar,proof} 7.9 +\usepackage[nohyphen,strings]{underscore} 7.10 +\usepackage{isabelle} 7.11 +\usepackage{isabellesym} 7.12 +\usepackage{railsetup} 7.13 +\usepackage{ttbox} 7.14 +\usepackage{supertabular} 7.15 +\usepackage{style} 7.16 +\usepackage{pdfsetup} 7.17 + 7.18 + 7.19 +\hyphenation{Isabelle} 7.20 +\hyphenation{Eisbach} 7.21 + 7.22 +\isadroptag{theory} 7.23 +\title{\includegraphics[scale=0.5]{isabelle_eisbach} 7.24 + \\[4ex] The Eisbach User Manual} 7.25 +\author{Daniel Matichuk \\ 7.26 + Makarius Wenzel \\ 7.27 + Toby Murray 7.28 +} 7.29 + 7.30 + 7.31 +% Control fixmes etc. 7.32 +\newif\ifDraft \newif\ifFinal 7.33 +%\Drafttrue\Finalfalse 7.34 +\Draftfalse\Finaltrue 7.35 + 7.36 + 7.37 +\ifDraft 7.38 + \usepackage{draftcopy} 7.39 + \newcommand{\Comment}[1]{\textbf{\textsl{#1}}} 7.40 + \newenvironment{LongComment}[1] % multi-paragraph comment, argument is owner 7.41 + {\begingroup\par\noindent\slshape \textbf{Begin Comment[#1]}\par} 7.42 + {\par\noindent\textbf{End Comment}\endgroup\par} 7.43 + \newcommand{\FIXME}[1]{\textbf{\textsl{FIXME: #1}}} 7.44 + \newcommand{\TODO}[1]{\textbf{\textsl{TODO: #1}}} 7.45 +\else 7.46 + \newcommand{\Comment}[1]{\relax} 7.47 + \newenvironment{LongComment}[1]{\expandafter\comment}{\expandafter\endcomment} 7.48 + \newcommand{\FIXME}[1]{\relax} 7.49 + \newcommand{\TODO}[1]{\relax} 7.50 +\fi 7.51 + 7.52 +% This sort of command for each active author can be convenient 7.53 +\newcommand{\dan}[1]{\Comment{#1 [dan]}} 7.54 +\newcommand{\toby}[1]{\Comment{#1 [toby]}} 7.55 +\newcommand{\makarius}[1]{\Comment{#1 [makarius]}} 7.56 + 7.57 + 7.58 +\makeindex 7.59 + 7.60 +\chardef\charbackquote=`\` 7.61 +\newcommand{\backquote}{\mbox{\tt\charbackquote}} 7.62 + 7.63 + 7.64 +\begin{document} 7.65 + 7.66 +\maketitle 7.67 + 7.68 +\pagenumbering{roman} 7.69 +\chapter*{Preface} 7.70 +\input{Preface.tex} 7.71 +\tableofcontents 7.72 +\clearfirst 7.73 + 7.74 +\input{Manual.tex} 7.75 + 7.76 +\begingroup 7.77 +\tocentry{\bibname} 7.78 +\bibliographystyle{abbrv} \small\raggedright\frenchspacing 7.79 +\bibliography{manual} 7.80 +\endgroup 7.81 + 7.82 +\tocentry{\indexname} 7.83 +\printindex 7.84 + 7.85 +\end{document} 7.86 + 7.87 + 7.88 +%%% Local Variables: 7.89 +%%% mode: latex 7.90 +%%% TeX-master: t 7.91 +%%% End:

8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 8.2 +++ b/src/Doc/Eisbach/document/style.sty Sun May 17 23:03:49 2015 +0200 8.3 @@ -0,0 +1,68 @@ 8.4 +%% toc 8.5 +\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1} 8.6 +\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}} 8.7 + 8.8 +%% references 8.9 +\newcommand{\secref}[1]{\S\ref{#1}} 8.10 +\newcommand{\chref}[1]{chapter~\ref{#1}} 8.11 +\newcommand{\figref}[1]{figure~\ref{#1}} 8.12 + 8.13 +%% math 8.14 +\newcommand{\text}[1]{\mbox{#1}} 8.15 +\newcommand{\isasymvartheta}{\isamath{\theta}} 8.16 +\newcommand{\isactrlvec}[1]{\emph{$\vec{#1}$}} 8.17 +\newcommand{\isactrlBG}{\isacharbackquoteopen} 8.18 +\newcommand{\isactrlEN}{\isacharbackquoteclose} 8.19 + 8.20 +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} 8.21 + 8.22 +\pagestyle{headings} 8.23 +\sloppy 8.24 +\binperiod 8.25 + 8.26 +\parindent 0pt\parskip 0.5ex 8.27 + 8.28 +\renewcommand{\isadigit}[1]{\isamath{#1}} 8.29 + 8.30 +\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup} 8.31 + 8.32 +\isafoldtag{FIXME} 8.33 + 8.34 +\isakeeptag{mlref} 8.35 +\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{ML}~~}Reference}} 8.36 +\renewcommand{\endisatagmlref}{} 8.37 + 8.38 +\isakeeptag{mlantiq} 8.39 +\renewcommand{\isatagmlantiq}{\subsection*{\makebox[0pt][r]{\fbox{ML}~~}Antiquotations}} 8.40 +\renewcommand{\endisatagmlantiq}{} 8.41 + 8.42 +\isakeeptag{mlex} 8.43 +\renewcommand{\isatagmlex}{\subsection*{\makebox[0pt][r]{\fbox{ML}~~}Examples}} 8.44 +\renewcommand{\endisatagmlex}{} 8.45 + 8.46 +\renewcommand{\isatagML}{\begingroup\isabellestyle{default}\isastyle\def\isadigit##1{##1}} 8.47 +\renewcommand{\endisatagML}{\endgroup} 8.48 + 8.49 +\newcommand{\minorcmd}[1]{{\sf #1}} 8.50 +\newcommand{\isasymtype}{\minorcmd{type}} 8.51 +\newcommand{\isasymval}{\minorcmd{val}} 8.52 + 8.53 +\newcommand{\isasymFIX}{\isakeyword{fix}} 8.54 +\newcommand{\isasymASSUME}{\isakeyword{assume}} 8.55 +\newcommand{\isasymDEFINE}{\isakeyword{define}} 8.56 +\newcommand{\isasymNOTE}{\isakeyword{note}} 8.57 +\newcommand{\isasymGUESS}{\isakeyword{guess}} 8.58 +\newcommand{\isasymOBTAIN}{\isakeyword{obtain}} 8.59 +\newcommand{\isasymTHEORY}{\isakeyword{theory}} 8.60 +\newcommand{\isasymUSES}{\isakeyword{uses}} 8.61 +\newcommand{\isasymEND}{\isakeyword{end}} 8.62 +\newcommand{\isasymCONSTS}{\isakeyword{consts}} 8.63 +\newcommand{\isasymDEFS}{\isakeyword{defs}} 8.64 +\newcommand{\isasymTHEOREM}{\isakeyword{theorem}} 8.65 +\newcommand{\isasymDEFINITION}{\isakeyword{definition}} 8.66 + 8.67 +\isabellestyle{literal} 8.68 + 8.69 +\railtermfont{\isabellestyle{tt}} 8.70 +\railnontermfont{\isabellestyle{itunderscore}} 8.71 +\railnamefont{\isabellestyle{itunderscore}}

9.1 --- a/src/Doc/ROOT Sun May 17 22:33:34 2015 +0200 9.2 +++ b/src/Doc/ROOT Sun May 17 23:03:49 2015 +0200 9.3 @@ -59,6 +59,28 @@ 9.4 "root.tex" 9.5 "style.sty" 9.6 9.7 +session Eisbach (doc) in "Eisbach" = "HOL-Eisbach" + 9.8 + options [document_variants = "eisbach", quick_and_dirty, 9.9 + print_mode = "no_brackets,iff", show_question_marks = false] 9.10 + theories [document = false] 9.11 + Base 9.12 + theories 9.13 + Preface 9.14 + Manual 9.15 + document_files (in "..") 9.16 + "prepare_document" 9.17 + "pdfsetup.sty" 9.18 + "iman.sty" 9.19 + "extra.sty" 9.20 + "isar.sty" 9.21 + "ttbox.sty" 9.22 + "underscore.sty" 9.23 + "manual.bib" 9.24 + document_files 9.25 + "build" 9.26 + "root.tex" 9.27 + "style.sty" 9.28 + 9.29 session Functions (doc) in "Functions" = HOL + 9.30 options [document_variants = "functions", skip_proofs = false, quick_and_dirty] 9.31 theories Functions