diff -r d69214e47ef9 -r efb5fff99c96 ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Thu Aug 20 23:30:51 2009 +0200 +++ b/ProgTutorial/Tactical.thy Fri Aug 21 11:42:14 2009 +0200 @@ -49,41 +49,43 @@ THEN atac 1) end" "?P \ ?Q \ ?Q \ ?P"} - To start the proof, the function @{ML "Goal.prove"}~@{text "ctxt xs As C - tac"} sets up a goal state for proving the goal @{text C} - (that is @{prop "P \ Q \ Q \ P"} in the proof at hand) under the - assumptions @{text As} (happens to be empty) with the variables - @{text xs} that will be generalised once the goal is proved (in our case - @{text P} and @{text Q}). The @{text "tac"} is the tactic that proves the goal; - it can make use of the local assumptions (there are none in this example). - The tactics @{ML_ind etac}, @{ML_ind rtac} and @{ML_ind atac} - in the code above correspond - roughly to @{text erule}, @{text rule} and @{text assumption}, respectively. - The operator @{ML_ind THEN} strings the tactics together. + To start the proof, the function @{ML_ind "Goal.prove"}~@{text "ctxt xs As C + tac"} sets up a goal state for proving the goal @{text C} (that is @{prop "P + \ Q \ Q \ P"} in the proof at hand) under the assumptions @{text As} + (happens to be empty) with the variables @{text xs} that will be generalised + once the goal is proved (in our case @{text P} and @{text + Q}).\footnote{FIXME: explain prove earlier} The @{text "tac"} is the tactic + that proves the goal; it can make use of the local assumptions (there are + none in this example). The tactics @{ML_ind etac}, @{ML_ind rtac} and + @{ML_ind atac} in the code above correspond roughly to @{text erule}, @{text + rule} and @{text assumption}, respectively. The operator @{ML_ind THEN} + strings the tactics together. \begin{readmore} - To learn more about the function @{ML_ind prove in Goal} see \isccite{sec:results} - and the file @{ML_file "Pure/goal.ML"}. See @{ML_file + To learn more about the function @{ML_ind prove in Goal} see + \isccite{sec:results} and the file @{ML_file "Pure/goal.ML"}. See @{ML_file "Pure/tactic.ML"} and @{ML_file "Pure/tactical.ML"} for the code of basic tactics and tactic combinators; see also Chapters 3 and 4 in the old - Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation Manual. + Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation + Manual. \end{readmore} - Note that in the code above we use 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 where there is no ML-binding obtain - the theorem dynamically using the function @{ML thm}; for example - \mbox{@{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. + Note that in the code above we use 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 where there + is no ML-binding obtain the theorem dynamically using the function @{ML + thm}; for example \mbox{@{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 - done with the command \isacommand{apply}@{text "(tactic \ \ \)"}. + During the development of automatic proof procedures, you will often find it + necessary to test a tactic on examples. This can be conveniently done with + the command \isacommand{apply}@{text "(tactic \ \ \)"}. Consider the following sequence of tactics + *} ML{*val foo_tac = @@ -302,7 +304,6 @@ \end{figure} *} - text {* which prints out the given theorem (using the string-function defined in Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. With this @@ -315,9 +316,7 @@ where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the subgoals. So after setting up the lemma, the goal state is always of the form @{text "C \ #C"}; when the proof is finished we are left with @{text - "#C"}.\footnote{This only applies to single statements. If the lemma - contains more than one statement, then one has more such implications.} - Since the goal @{term C} can potentially be an implication, there is a + "#C"}. Since the goal @{term C} can potentially be an implication, there is a ``protector'' wrapped around it (the wrapper is the outermost constant @{text "Const (\"prop\", bool \ bool)"}; in the figure we make it visible as an @{text #}). This wrapper prevents that premises of @{text C} are @@ -1267,6 +1266,7 @@ simplification rules, congruence rules and simprocs.\label{fig:printss}} \end{figure} *} + text {* To see how they work, consider the function in Figure~\ref{fig:printss}, which prints out some parts of a simpset. If you use it to print out the components of the