--- a/CookBook/Tactical.thy Thu Feb 05 22:40:22 2009 +0000
+++ b/CookBook/Tactical.thy Thu Feb 05 22:40:46 2009 +0000
@@ -1,5 +1,5 @@
theory Tactical
-imports Base
+imports Base FirstSteps
begin
chapter {* Tactical Reasoning\label{chp:tactical} *}
@@ -12,9 +12,8 @@
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.
-
-
+ all of them are solved. However, there are also more structured operations
+ that help with handling of variables and assumptions.
*}
section {* Tactical Reasoning *}
@@ -50,19 +49,23 @@
end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?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} under the
- assumptions @{text As} (empty in the proof at hand) with the variables
+ tac"} sets up a goal state for proving the goal @{text C}
+ (that is @{prop "P \<or> Q \<Longrightarrow> Q \<or> 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 functions @{ML etac}, @{ML rtac} and @{ML atac} correspond to
@{text erule}, @{text rule} and @{text assumption}, respectively.
- The operator @{ML THEN} strings tactics together.
+ The operator @{ML THEN} strings the tactics together.
\begin{readmore}
- To learn more about the function @{ML Goal.prove} see \isccite{sec:results} and
- the file @{ML_file "Pure/goal.ML"}. For more information about the internals of goals see
- \isccite{sec:tactical-goals}.
+ To learn more about the function @{ML Goal.prove} see \isccite{sec:results}
+ and the file @{ML_file "Pure/goal.ML"}. For more information about the
+ internals of goals see \isccite{sec:tactical-goals}. See @{ML_file
+ "Pure/tactic.ML"} and @{ML_file "Pure/tctical.ML"} for the code of basic
+ tactics and tactic combinators; see also Chapters 3 and 4 in the old
+ Isabelle Reference Manual.
\end{readmore}
Note that we used antiquotations for referencing the theorems. We could also
@@ -92,9 +95,9 @@
done
text {*
- The apply-step applies the @{ML foo_tac} and therefore solves the goal completely.
- Inside @{text "tactic \<verbopen> \<dots> \<verbclose>"}
- we can call any function that returns a tactic.
+ By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} in the apply-step,
+ you can call @{ML foo_tac} or any function that returns a tactic from the
+ user level of Isabelle.
As can be seen, each tactic in @{ML foo_tac} has a hard-coded number that
stands for the subgoal analysed by the tactic. In our case, we only focus on the first
@@ -111,7 +114,8 @@
text {*
and then give the number for the subgoal explicitly when the tactic is
- called. So in the next proof we discharge first the second subgoal,
+ called. For every operator that combines tactics, such a primed version
+ exists. So in the next proof we can first discharge the second subgoal,
and after that the first.
*}
@@ -122,20 +126,31 @@
done
text {*
- The tactic @{ML foo_tac} is very specific for analysing goals of the form
- @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not of this form, then @{ML foo_tac}
- throws the error message about an empty result sequence---meaning the tactic
- failed. The reason for this 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
+ (FIXME: maybe add something about how each goal state is interpreted
+ as a theorem)
+
+ The tactic @{ML foo_tac} (and @{ML foo_tac'}) are very specific for
+ analysing goals only of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not
+ of this form, then @{ML foo_tac} throws 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
+ 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"}
- Consequently, if a tactic fails, then it returns the empty sequence. This
- is by the way the default behaviour for a failing tactic; tactics should
- not raise exceptions.
+ It is custom that if a tactic fails, it should return the empty sequence:
+ tactics should not raise exceptions willy-nilly.
- In the following example there are two possibilities for how to apply the tactic.
+ The lazy list of possible successor states shows through to 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'}.
*}
lemma "\<lbrakk>P \<or> Q; P \<or> Q\<rbrakk> \<Longrightarrow> Q \<or> P"
@@ -144,82 +159,111 @@
done
text {*
- The application of the tactic results in a sequence of two possible
- proofs. The Isabelle command \isacommand{back} allows us to explore both
- possibilities.
-
+ By using \isacommand{back}, we construct the proof that uses the
+ second assumption to complete the proof. In more interesting
+ situations, different possibilities can lead to different proofs.
+
\begin{readmore}
See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy
sequences. However in day-to-day Isabelle programming, one rarely
constructs sequences explicitly, but uses the predefined functions
- instead. See @{ML_file "Pure/tactic.ML"} and
- @{ML_file "Pure/tctical.ML"} for the code of basic tactics and tactic
- combinators; see also Chapters 3 and 4 in
- the old Isabelle Reference Manual.
+ instead.
\end{readmore}
*}
-
section {* Basic Tactics *}
-lemma shows "False \<Longrightarrow> False"
+text {*
+ As seen above, the function @{ML atac} corresponds to the assumption tactic.
+*}
+
+lemma shows "P \<Longrightarrow> P"
apply(tactic {* atac 1 *})
done
-lemma shows "True \<and> True"
+text {*
+ Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond
+ to @{ML_text rule}, @{ML_text drule}, @{ML_text erule} and @{ML_text frule},
+ respectively. Below are three examples with the resulting goal state. How
+ they work should therefore be self-explanatory.
+*}
+
+lemma shows "P \<and> Q"
apply(tactic {* rtac @{thm conjI} 1 *})
-txt {* @{subgoals [display]} *}
+txt{*@{subgoals [display]}*}
(*<*)oops(*>*)
-lemma
- shows "Foo"
- and "True \<and> True"
-apply(tactic {* rtac @{thm conjI} 2 *})
-txt {* @{subgoals [display]} *}
-(*<*)oops(*>*)
-
-lemma shows "False \<and> False \<Longrightarrow> False"
+lemma shows "P \<and> Q \<Longrightarrow> False"
apply(tactic {* etac @{thm conjE} 1 *})
-txt {* @{subgoals [display]} *}
+txt{*@{subgoals [display]}*}
(*<*)oops(*>*)
lemma shows "False \<and> True \<Longrightarrow> False"
apply(tactic {* dtac @{thm conjunct2} 1 *})
-txt {* @{subgoals [display]} *}
+txt{*@{subgoals [display]}*}
(*<*)oops(*>*)
text {*
- similarly @{ML ftac}
+ As mentioned above, most basic tactics take a number as argument, which
+ addresses to subgoal they are analysing.
+*}
+
+lemma shows "Foo" and "P \<and> Q"
+apply(tactic {* rtac @{thm conjI} 2 *})
+txt {*@{subgoals [display]}*}
+(*<*)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
*}
-text {* diagnostics *}
-lemma shows "True \<Longrightarrow> False"
+ML{*val resolve_tac_xmp = resolve_tac [@{thm impI}, @{thm conjI}]*}
+
+text {*
+ an example for @{ML resolve_tac} is the following proof where first an outermost
+ implication is analysed and then an outermost conjunction.
+*}
+
+lemma shows "C \<longrightarrow> (A \<and> B)" and "(A \<longrightarrow> B) \<and> C"
+apply(tactic {* resolve_tac_xmp 1 *})
+apply(tactic {* resolve_tac_xmp 2 *})
+txt{* @{subgoals [display]} *}
+(*<*)oops(*>*)
+
+text {*
+ Similarly versions exists for @{ML atac} (@{ML assume_tac}), @{ML etac}
+ (@{ML eresolve_tac}) and so on.
+
+ The tactic @{ML print_tac} is useful for low-level debugging of tactics: it
+ prints out a message and the current goal state.
+*}
+
+lemma shows "False \<Longrightarrow> True"
apply(tactic {* print_tac "foo message" *})
(*<*)oops(*>*)
-text {* Let us assume the following four string conversion functions: *}
-
-ML{*fun str_of_cterm ctxt t =
- Syntax.string_of_term ctxt (term_of t)
-
-fun str_of_cterms ctxt ts =
- commas (map (str_of_cterm ctxt) ts)
+text {*
+ Also for useful for debugging, but not exclusively, are the tactics @{ML all_tac} and
+ @{ML no_tac}. The former always succeeds (but does not change the goal state), and
+ the latter always fails.
-fun str_of_thm ctxt thm =
- let
- val {prop, ...} = crep_thm thm
- in
- str_of_cterm ctxt prop
- end
+ (FIXME explain RS MRS)
-fun str_of_thms ctxt thms =
- commas (map (str_of_thm ctxt) thms)*}
-
-text {*
- and the following function
+ Often proofs involve elaborate operations on assumptions and variables
+ @{text "\<And>"}-quantified in the goal state. 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.
*}
+text_raw{*
+\begin{figure}
+\begin{isabelle}
+*}
ML{*fun sp_tac {prems, params, asms, concl, context, schematics} =
let
val str_of_params = str_of_cterms context params
@@ -236,20 +280,28 @@
in
no_tac
end*}
+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}}
+\end{figure}
+*}
text {*
- then the tactic @{ML SUBPROOF} fixes the parameters and binds the various components
- of a proof state into a record. For example
+ 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 "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
+lemma shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
txt {*
- prints out
+ which yields the printout:
- \begin{center}
+ \begin{quote}\small
\begin{tabular}{ll}
params: & @{term x}, @{term y}\\
schematics: & @{term z}\\
@@ -257,18 +309,31 @@
concl: & @{term "B y x \<longrightarrow> C (z y) x"}\\
prems: & @{term "A x y"}
\end{tabular}
- \end{center}
+ \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
+ the subproof. Similarly the schematic variable @{term z}. The assumption
+ is bound once as @{ML_type cterm} to the record-variable @{text asms} and
+ another time as @{ML_type thm} to @{text prems}.
- Continuing the proof script with
+ 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.
+ Since in the function @{ML sp_tac} we returned the tactic @{ML no_tac}, the subproof
+ obviously fails. The question-mark allows us to recover from this failure
+ in a graceful manner so that the warning messages are not overwritten
+ by the error message.
+
+ If we continue the proof script by applying the @{text impI}-rule
*}
apply(rule impI)
apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
txt {*
- prints out
+ then @{ML SUBPROOF} prints out
- \begin{center}
+ \begin{quote}\small
\begin{tabular}{ll}
params: & @{term x}, @{term y}\\
schematics: & @{term z}\\
@@ -276,36 +341,85 @@
concl: & @{term "C (z y) x"}\\
prems: & @{term "A x y"}, @{term "B y x"}
\end{tabular}
- \end{center}
+ \end{quote}
*}
(*<*)oops(*>*)
+text {*
+ where we now also have @{term "B y x"} as assumption.
+
+ One convenience of @{ML SUBPROOF} is that we can apply assumption
+ 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}:
+*}
+
+lemma shows "\<And>x y. \<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
+apply(tactic
+ {* SUBPROOF (fn {prems, ...} => resolve_tac prems 1) @{context} 1 *})
+txt{* yields
+ @{subgoals [display]} *}
+(*<*)oops(*>*)
+
text {*
- @{ML PRIMITIVE}? @{ML SUBGOAL} see page 32 in ref
+ The restriction in this tactic is that it cannot instantiate any
+ schematic variables. This might be seen as a defect, but is actually
+ an advantage in the situations for which @{ML SUBPROOF} was designed:
+ the reason is that instantiation of schematic variables can potentially
+ has affect several goals and can render them unprovable.
+
+ A similar but less powerful function is @{ML SUBGOAL}. It allows you to
+ inspect a subgoal specified by a number.
*}
-text {*
- @{ML all_tac} @{ML no_tac}
+ML %linenumbers{*fun select_tac (t,i) =
+ case t of
+ @{term "Trueprop"} $ t' => select_tac (t',i)
+ | @{term "op \<and>"} $ _ $ _ => rtac @{thm conjI} i
+ | @{term "op \<longrightarrow>"} $ _ $ _ => rtac @{thm impI} i
+ | @{term "Not"} $ _ => rtac @{thm notI} i
+ | Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i
+ | _ => no_tac*}
+
+lemma shows "A \<and> B" "A \<longrightarrow> B" "\<forall>x. C x"
+apply(tactic {* SUBGOAL select_tac 1 *})
+apply(tactic {* SUBGOAL select_tac 3 *})
+apply(tactic {* SUBGOAL select_tac 4 *})
+txt{* @{subgoals [display]} *}
+(*<*)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.
+
+ A variant of @{ML SUBGOAL} is @{ML CSUBGOAL} which allows access to the goal
+ as @{ML_type cterm} instead of a @{ML_type term}.
*}
+
section {* Operations on Tactics *}
-text {* THEN *}
+text {* @{ML THEN} *}
-lemma shows "(True \<and> True) \<and> False"
-apply(tactic {* (rtac @{thm conjI} 1) THEN (rtac @{thm conjI} 1) *})
+lemma shows "(Foo \<and> Bar) \<and> False"
+apply(tactic {* (rtac @{thm conjI} 1)
+ THEN (rtac @{thm conjI} 1) *})
txt {* @{subgoals [display]} *}
(*<*)oops(*>*)
-lemma shows "True \<and> False"
-apply(tactic {* (rtac @{thm disjI1} 1) ORELSE (rtac @{thm conjI} 1) *})
+ML{*val orelse_xmp = (rtac @{thm disjI1} ORELSE' rtac @{thm conjI})*}
+
+lemma shows "True \<and> False" and "Foo \<or> Bar"
+apply(tactic {* orelse_xmp 1 *})
+apply(tactic {* orelse_xmp 3 *})
txt {* @{subgoals [display]} *}
(*<*)oops(*>*)
text {*
- @{ML EVERY} @{ML REPEAT}
+ @{ML EVERY} @{ML REPEAT} @{ML DETERM}
@{ML rewrite_goals_tac}
@{ML cut_facts_tac}