# HG changeset patch # User Christian Urban # Date 1234141920 0 # Node ID f49dc7e962357e5622ed88adaca2bd3e2c520fc4 # Parent 5dcad9348e4d9cff0049f3cb26d7cbdebe2df031 added more to the Tactical section diff -r 5dcad9348e4d -r f49dc7e96235 CookBook/Parsing.thy --- a/CookBook/Parsing.thy Sun Feb 08 08:45:25 2009 +0000 +++ b/CookBook/Parsing.thy Mon Feb 09 01:12:00 2009 +0000 @@ -529,7 +529,7 @@ text {* There are a number of special purpose parsers that help with parsing specifications - of functions, inductive definitions and so on. For example the function + of functions, inductive definitions and so on. For example the @{ML OuterParse.target} reads a target in order to indicate a locale. @{ML_response [display,gray] @@ -543,9 +543,11 @@ is wrapping the result into an option type and returning @{ML NONE} if no target is present. - The function @{ML OuterParse.fixes} reads a list of constants - that can include type annotations and syntax translations. - The list is separated by \isacommand{and}. For example: + The function @{ML OuterParse.fixes} reads an \isacommand{and}-separated + list of constants that can include type annotations and syntax translations. + For example:\footnote{Note that in the code we need to write + @{text "\\\"int \ bool\\\""} in order to properly escape the double quotes + in the compound type.} *} text {* @@ -561,9 +563,12 @@ (bar, SOME \, NoSyn), (blonk, NONE, NoSyn)],[])"} - Whenever types are given, then they are stored in the @{ML SOME}s. - Note that we had to write @{text "\\\"int \ bool\\\""} to properly escape - the double quotes in the compound type. + Whenever types are given, then they are stored in the @{ML SOME}s. + If a syntax translation is present for a constant, then it is + stored in the @{ML Mixfix} data structure; no syntax translation is + indicated by @{ML NoSyn}. + + (FIXME: should for-fixes take any syntax annotation?) @{ML OuterParse.for_fixes} is an ``optional'' that prefixes @{ML OuterParse.fixes} with the comman \isacommand{for}. diff -r 5dcad9348e4d -r f49dc7e96235 CookBook/Tactical.thy --- a/CookBook/Tactical.thy Sun Feb 08 08:45:25 2009 +0000 +++ b/CookBook/Tactical.thy Mon Feb 09 01:12:00 2009 +0000 @@ -5,16 +5,15 @@ chapter {* Tactical Reasoning\label{chp:tactical} *} text {* - - The main reason for descending to the ML-level of Isabelle is to be - able to implement automatic proof procedures. Such proof procedures usually - lessen considerably the burden of manual reasoning, for example, when - introducing new definitions. These proof procedures are centred around - refining a goal state using tactics. This is similar to the @{text - apply}-style reasoning at the user level, where goals are modified in a - sequence of proof steps until all of them are solved. However, there are - also more structured operations available on the ML-level that help with - the handling of variables and assumptions. + The main reason for descending to the ML-level of Isabelle is to be able to + implement automatic proof procedures. Such proof procedures usually lessen + considerably the burden of manual reasoning, for example, when introducing + new definitions. These proof procedures are centred around refining a goal + state using tactics. This is similar to the \isacommand{apply}-style + reasoning at the user level, where goals are modified in a sequence of proof + steps until all of them are solved. However, there are also more structured + operations available on the ML-level that help with the handling of + variables and assumptions. *} @@ -59,10 +58,7 @@ it can make use of the local assumptions (there are none in this example). The functions @{ML etac}, @{ML rtac} and @{ML atac} correspond to @{text erule}, @{text rule} and @{text assumption}, respectively. - The operator @{ML THEN} strings the tactics together. A difference - between the \isacommand{apply}-script and the ML-code is that the - former causes the lemma to be stored under the name @{text "disj_swap"}, - whereas the latter does not include any code for this. + The operator @{ML THEN} strings the tactics together. \begin{readmore} To learn more about the function @{ML Goal.prove} see \isccite{sec:results} @@ -73,12 +69,15 @@ Isabelle Reference Manual. \end{readmore} - Note that we used antiquotations for referencing the theorems. We could also - just have written @{ML "etac disjE 1"} and so on, but this is considered bad - style. The reason is that the binding for @{ML disjE} can be re-assigned by - the user and thus one does not have complete control over which theorem is - actually applied. This problem is nicely prevented by using antiquotations, - because then the theorems are fixed statically at compile-time. + Note that we used antiquotations for referencing the theorems. Many theorems + also have ML-bindings with the same name. Therefore, we could also just have + written @{ML "etac disjE 1"}, or in case there are no ML-binding obtained + the theorem dynamically using the theorem @{ML thm}; for example @{ML "etac + (thm \"disjE\") 1"}. Both ways however are considered bad style. The reason + is that the binding for @{ML disjE} can be re-assigned by the user and thus + one does not have complete control over which theorem is actually + applied. This problem is nicely prevented by using antiquotations, because + then the theorems are fixed statically at compile-time. During the development of automatic proof procedures, you will often find it necessary to test a tactic on examples. This can be conveniently @@ -107,9 +106,9 @@ The tactic @{ML foo_tac} is just a sequence of simple tactics stringed together by @{ML THEN}. As can be seen, each simple tactic in @{ML foo_tac} has a hard-coded number that stands for the subgoal analysed by the - tactic (@{text "1"} stands for the first, or top-most, subgoal). This is - sometimes wanted, but usually not. To avoid the explicit numbering in - the tactic, you can write + tactic (@{text "1"} stands for the first, or top-most, subgoal). This hard-coding + of goals is sometimes wanted, but usually it is not. To avoid the explicit numbering, + you can write *} ML{*val foo_tac' = @@ -121,9 +120,8 @@ text {* and then give the number for the subgoal explicitly when the tactic is - called. For every operator that combines tactics (@{ML THEN} is only one - such operator), a primed version exists. So in the next proof you - can first discharge the second subgoal, and after that the first. + called. So in the next proof you can first discharge the second subgoal, and + after that the first. *} lemma "P1 \ Q1 \ Q1 \ P1" @@ -134,25 +132,26 @@ text {* This kind of addressing is more difficult to achieve when the goal is - hard-coded inside the tactic. + hard-coded inside the tactic. For every operator that combines tactics + (@{ML THEN} is only one such operator) a ``primed'' version exists. The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for analysing goals being only of the form @{prop "P \ Q \ Q \ P"}. If the goal is not - of this form, then @{ML foo_tac} throws the error message: + of this form, then they throw the error message: \begin{isabelle} @{text "*** empty result sequence -- proof command failed"}\\ @{text "*** At command \"apply\"."} \end{isabelle} - Meaning the tactic failed. The reason for this error message is that tactics + Meaning the tactics failed. The reason for this error message is that tactics are functions that map a goal state to a (lazy) sequence of successor states, hence the type of a tactic is: @{text [display, gray] "type tactic = thm -> thm Seq.seq"} It is custom that if a tactic fails, it should return the empty sequence: - your own tactics should not raise exceptions willy-nilly. + therefore your own tactics should not raise exceptions willy-nilly. The simplest tactics are @{ML no_tac} and @{ML all_tac}. The first returns the empty sequence and is defined as @@ -171,7 +170,7 @@ which means @{ML all_tac} always succeeds (but also does not make any progress with the proof). - The lazy list of possible successor states shows through to the user-level + The lazy list of possible successor states shows through at the user-level of Isabelle when using the command \isacommand{back}. For instance in the following proof, there are two possibilities for how to apply @{ML foo_tac'}. @@ -214,12 +213,12 @@ text {* which prints out the given theorem (using the string-function defined in Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. We - now can inspect every proof state in the follwing proof. On the left-hand - side we show the goal state as shown by the system; on the right-hand - side the print out from @{ML my_print_tac}. + now can inspect every proof state in a proof. Consider the proof below: on + the left-hand side we show the goal state as shown by Isabelle; on the + right-hand side the print out from @{ML my_print_tac}. *} -lemma shows "\A; B\ \ A \ B" +lemma shows "\A; B\ \ A \ B" apply(tactic {* my_print_tac @{context} *}) txt{* \small @@ -275,12 +274,12 @@ @{text[display] "A\<^isub>1 \ \ \ A\<^isub>n \ (C)"} where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the - subgoals. So in the first step the goal state is always of the form + subgoals. So after setting up the lemma, the goal state is always of the form @{text "C \ (C)"}. Since the goal @{term C} can potentially be an implication, there is a ``protector'' wrapped around it (in from of an outermost constant @{text "Const (\"prop\", bool \ bool)"} applied to each goal; however this constant is invisible in the print out above). This - prevents that premises are misinterpreted as open subgoals. + prevents that premises of @{text C} are misinterpreted as open subgoals. While tactics can operate on the subgoals (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion @{term C} intact, with the exception of possibly instantiating schematic variables. @@ -290,7 +289,17 @@ section {* Simple Tactics *} text {* - As seen above, the function @{ML atac} corresponds to the assumption tactic. + A simple tactic is @{ML print_tac}, which is useful for low-level debugging of tactics. + It just prints out a message and the current goal state. +*} + +lemma shows "False \ True" +apply(tactic {* print_tac "foo message" *}) +(*<*)oops(*>*) + +text {* + Another simple tactic is the function @{ML atac}, which, as shown in the previous + section, corresponds to the assumption command. *} lemma shows "P \ P" @@ -327,8 +336,9 @@ (*<*)oops(*>*) text {* - As mentioned above, most basic tactics take a number as argument, which - addresses to subgoal they are analysing. + As mentioned in the previous section, most basic tactics take a number as + argument, which addresses the subgoal they are analysing. In the proof below, + we first break up the second subgoal by focusing on this subgoal first. *} lemma shows "Foo" and "P \ Q" @@ -339,10 +349,10 @@ (*<*)oops(*>*) text {* - Corresponding to @{ML rtac}, there is also the tactic @{ML resolve_tac}, which - however expects a list of theorems as arguments. From this list it will apply with - the first applicable theorem (later theorems that are also applicable can be - explored via the lazy sequences mechanism). Given the abbreviation + The function @{ML resolve_tac} is similar to @{ML rtac}, except that it + expects a list of theorems as arguments. From this list it will apply the + first applicable theorem (later theorems that are also applicable can be + explored via the lazy sequences mechanism). Given the code *} ML{*val resolve_tac_xmp = resolve_tac [@{thm impI}, @{thm conjI}]*} @@ -362,25 +372,71 @@ text {* Similarly versions exists for @{ML atac} (@{ML assume_tac}), @{ML etac} - (@{ML eresolve_tac}) and so on. + (@{ML eresolve_tac}) and so on. + + (FIXME: @{ML cut_facts_tac}) - The tactic @{ML print_tac} is useful for low-level debugging of tactics: it - prints out a message and the current goal state. + Since rules are applied using higher-order unification, an automatic proof + procedure might become too fragile, if it just applies inference rules shown + in the fashion above. More constraints can be introduced by + pre-instantiating theorems with other theorems. You can do this using the + function @{ML RS}. For example + + @{ML_response_fake [display,gray] + "@{thm disjI1} RS @{thm conjI}" "\?P1; ?Q\ \ (?P1 \ ?Q1) \ ?Q"} + + instantiates the first premise of the @{text conjI}-rule with the + rule @{text disjI1}. The function @{ML RSN} is similar, but + takes a number and makes explicit which premise should be instantiated. + To improve readability we are going use the following function *} - -lemma shows "False \ True" -apply(tactic {* print_tac "foo message" *}) -(*<*)oops(*>*) + +ML{*fun no_vars ctxt thm = +let + val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt +in + thm' +end*} text {* - - (FIXME explain RS MRS) + to transform the schematic variables of a theorem into free variables. + This means for the @{ML RS}-expression above: + + @{ML_response_fake [display,gray] + "no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\P; Q\ \ (P \ Qa) \ Q"} + + If you want to instantiate more than one premise, you can use the function + @{ML MRS}: + + @{ML_response_fake [display,gray] + "no_vars @{context} ([@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI})" + "\P; Q\ \ (P \ Qa) \ (Pa \ Q)"} + + If you need to instantiate lists of theorems, you can use the + functions @{ML RL} and @{ML MRL}. For example below every + theorem in the first list is instantiated against every theorem + in the second. + + @{ML_response_fake [display,gray] + "[@{thm impI}, @{thm disjI2}] RL [@{thm conjI}, @{thm disjI1}]" +"[\P \ Q; Qa\ \ (P \ Q) \ Qa, + \Q; Qa\ \ (P \ Q) \ Qa, + (P \ Q) \ (P \ Q) \ Qa, + Q \ (P \ Q) \ Qa]"} + + \begin{readmore} + The combinators for instantiating theorems are defined in @{ML_file "Pure/drule.ML"}. + \end{readmore} Often proofs involve elaborate operations on assumptions and @{text "\"}-quantified variables. To do such operations on the ML-level using the basic tactics is very unwieldy and brittle. Some convenience and safety is provided by the tactic @{ML SUBPROOF}. This tactic fixes the parameters and binds the various components of a proof state into a record. + To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which + takes a record as argument and just prints out the content of this record (using the + string transformation functions defined in Section~\ref{sec:printing}). Consider + now the proof *} text_raw{* @@ -406,17 +462,11 @@ text_raw{* \end{isabelle} \caption{A function that prints out the various parameters provided by the tactic - @{ML SUBPROOF}. It uses the functions extracting strings from @{ML_type cterm}s - and @{ML_type thm}s, which are defined in Section~\ref{sec:printing}.\label{fig:sptac}} + @{ML SUBPROOF}. It uses the functions defined in Section~\ref{sec:printing} for + extracting strings from @{ML_type cterm}s and @{ML_type thm}s.\label{fig:sptac}} \end{figure} *} -text {* - To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which - takes a record as argument and just prints out the content of this record (using the - string transformation functions defined in Section~\ref{sec:printing}). Consider - now the proof -*} lemma shows "\x y. A x y \ B y x \ C (?z y) x" apply(tactic {* SUBPROOF sp_tac @{context} 1 *})? @@ -435,10 +485,10 @@ \end{quote} Note in the actual output the brown colour of the variables @{term x} and - @{term y}. Although parameters in the original goal, they are fixed inside + @{term y}. Although they are parameters in the original goal, they are fixed inside the subproof. Similarly the schematic variable @{term z}. The assumption - @{prop "A x y"} is bound once as @{ML_type cterm} to the record-variable - @{text asms} and another time as @{ML_type thm} to @{text prems}. + @{prop "A x y"} is bound as @{ML_type cterm} to the record-variable + @{text asms} but also as @{ML_type thm} to @{text prems}. Notice also that we had to append @{text "?"} to \isacommand{apply}. The reason is that @{ML SUBPROOF} normally expects that the subgoal is solved completely. @@ -471,10 +521,10 @@ text {* where we now also have @{term "B y x"} as an assumption. - One convenience of @{ML SUBPROOF} is that we can apply assumption + One convenience of @{ML SUBPROOF} is that we can apply the assumptions using the usual tactics, because the parameter @{text prems} - contains the assumptions as theorems. With this we can easily - implement a tactic that almost behaves like @{ML atac}: + contains them as theorems. With this we can easily + implement a tactic that almost behaves like @{ML atac}, namely: *} ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*} @@ -496,23 +546,26 @@ number @{text "1"} and also the ``outer'' call to @{ML SUBPROOF} in the \isacommand{apply}-step uses @{text "1"}. Another advantage of @{ML SUBGOAL} is that the addressing inside it is completely - local to the proof inside. It is therefore possible to also apply + local to the subproof inside. It is therefore possible to also apply @{ML atac'} to the second goal: *} lemma shows "True" and "\x y. \B x y; A x y; C x y\ \ A x y" apply(tactic {* atac' @{context} 2 *}) -txt{* This gives: - @{subgoals [display]} *} -(*<*)oops(*>*) +apply(rule TrueI) +done text {* + \begin{readmore} + The function @{ML SUBPROOF} is defined in @{ML_file "Pure/subgoal.ML"} and + also described in \isccite{sec:results}. + \end{readmore} + A similar but less powerful function than @{ML SUBPROOF} is @{ML SUBGOAL}. - It allows you to inspect a subgoal specified by a number. With this we can - implement a little tactic that applies a rule corresponding to its - topmost connective. The tactic should only apply ``safe'' rules (that is - which do not render the goal unprovable). For this we can write: + It allows you to inspect a specified subgoal. With this you can implement + a tactic that applies a rule according to its topmost connective (we only + analyse a few connectives). The tactic is as follows: *} ML %linenumbers{*fun select_tac (t,i) = @@ -524,7 +577,21 @@ | Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i | _ => all_tac*} -lemma shows "A \ B" "A \ B" "\x. C x" "D \ E" +text {* + In line 3 you need to decend under the outermost @{term "Trueprop"} in order + to get to the connective you like to analyse. Otherwise goals @{prop "A \ B"} + are not bropek up. In line 7, the pattern cannot be constructed using the + @{text "@term"}-antiquotation, because that would fix the type of the + quantified variable. In this case you really have to construct the pattern + by using the term-constructors. The other cases work, because their type + is always bool. In case that the goal does not fall into any of the categorories, + then we chose to just return @{ML all_tac} (i.e., the tactic never fails). + + Let us now see how to apply this tactic. +*} + + +lemma shows "A \ B" and "A \ B \C" and "\x. D x" and "E \ F" apply(tactic {* SUBGOAL select_tac 4 *}) apply(tactic {* SUBGOAL select_tac 3 *}) apply(tactic {* SUBGOAL select_tac 2 *}) @@ -533,29 +600,72 @@ (*<*)oops(*>*) text {* - However, this example is contrived, as there are much simpler ways - to implement a proof procedure like the one above. They will be explained - in the next section. + Note that we applied it in ``reverse'' order. This is a trick in + order to be independent from what subgoals the rule produced. If we had + it applied in the other order +*} + +lemma shows "A \ B" and "A \ B \C" and "\x. D x" and "E \ F" +apply(tactic {* SUBGOAL select_tac 1 *}) +apply(tactic {* SUBGOAL select_tac 3 *}) +apply(tactic {* SUBGOAL select_tac 4 *}) +apply(tactic {* SUBGOAL select_tac 5 *}) +(*<*)oops(*>*) - (Notice that we applied the goals in reverse order) +text {* + then we have to be careful to not apply the tactic to the two subgoals the + first goal produced. This can be messy in an automated proof script. The + reverse application, on the other hand, is easy to implement. - A variant of @{ML SUBGOAL} is @{ML CSUBGOAL} which allows access to the goal - as @{ML_type cterm} instead of a @{ML_type term}. + However, this example is contrived: there are much simpler ways to implement + such proof procedure that analyses a goal according to its topmost + connective. They will be explained in the next section. +*} + +section {* Tactic Combinators *} + +text {* + To be able to implement powerful tactics out of smaller component tactics, + Isabelle provides tactic combinators. In the previous section we already + used @{ML THEN} which strings two tactics together in sequence. For example: *} +lemma shows "(Foo \ Bar) \ False" +apply(tactic {* rtac @{thm conjI} 1 THEN rtac @{thm conjI} 1 *}) +txt {* \begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage} *} +(*<*)oops(*>*) -section {* Operations on Tactics *} - -text {* @{ML THEN} *} +text {* + If you want to avoid the hard-coded subgoal addressing, then you can use + @{ML THEN'}. For example: +*} lemma shows "(Foo \ Bar) \ False" -apply(tactic {* (rtac @{thm conjI} 1) - THEN (rtac @{thm conjI} 1) *}) -txt {* @{subgoals [display]} *} +apply(tactic {* (rtac @{thm conjI} THEN' rtac @{thm conjI}) 1 *}) +txt {* \begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage} *} (*<*)oops(*>*) +text {* + For most tactic combinators such a ``primed'' version exists. + In what follows we will, whenever appropriate, prefer the primed version of + the tactic combinator and omit to mention the simple one. + + With @{ML THEN} and @{ML THEN'} it must be guaranteed that both tactics + sucessfully apply; otherwise the whole tactic will fail. If you want to + try out either one tactic, then you can use @{ML ORELSE'}. For + example +*} + ML{*val orelse_xmp = (rtac @{thm disjI1} ORELSE' rtac @{thm conjI})*} +text {* + will first try out rule @{text disjI} and after that @{text conjI}. +*} + lemma shows "True \ False" and "Foo \ Bar" apply(tactic {* orelse_xmp 1 *}) apply(tactic {* orelse_xmp 3 *}) @@ -564,15 +674,22 @@ text {* - @{ML EVERY} @{ML REPEAT} @{ML DETERM} + applies + + + @{ML REPEAT} @{ML DETERM} +*} + +section {* Rewriting and Simplifier Tactics *} + +text {* @{ML rewrite_goals_tac} - @{ML cut_facts_tac} @{ML ObjectLogic.full_atomize_tac} @{ML ObjectLogic.rulify_tac} - @{ML resolve_tac} *} + section {* Structured Proofs *} lemma True diff -r 5dcad9348e4d -r f49dc7e96235 cookbook.pdf Binary file cookbook.pdf has changed