--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Tactical.thy Fri Jan 30 08:24:48 2009 +0000
@@ -0,0 +1,265 @@
+theory Tactical
+imports Base
+begin
+
+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.
+
+
+*}
+
+section {* Tactical Reasoning *}
+
+text {*
+ To see how tactics work, let us first transcribe a simple @{text apply}-style proof
+ into ML. Consider the following proof.
+*}
+
+lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
+apply(erule disjE)
+apply(rule disjI2)
+apply(assumption)
+apply(rule disjI1)
+apply(assumption)
+done
+
+text {*
+ This proof translates to the following ML-code.
+
+@{ML_response_fake [display,gray]
+"let
+ val ctxt = @{context}
+ val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}
+in
+ Goal.prove ctxt [\"P\", \"Q\"] [] goal
+ (fn _ =>
+ etac @{thm disjE} 1
+ THEN rtac @{thm disjI2} 1
+ THEN atac 1
+ THEN rtac @{thm disjI1} 1
+ THEN atac 1)
+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
+ @{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.
+
+ \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}.
+ \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.
+
+ During the development of automatic proof procedures, it will often be necessary
+ to test a tactic on examples. This can be conveniently
+ done with the command \isacommand{apply}@{text "(tactic \<verbopen> \<dots> \<verbclose>)"}.
+ Consider the following sequence of tactics
+*}
+
+ML{*val foo_tac =
+ (etac @{thm disjE} 1
+ THEN rtac @{thm disjI2} 1
+ THEN atac 1
+ THEN rtac @{thm disjI1} 1
+ THEN atac 1)*}
+
+text {* and the Isabelle proof: *}
+
+lemma "P \<or> Q \<Longrightarrow> Q \<or> P"
+apply(tactic {* foo_tac *})
+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.
+
+ 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
+ subgoal. This is sometimes wanted, but usually not. To avoid the explicit numbering in the
+ tactic, you can write
+*}
+
+ML{*val foo_tac' =
+ (etac @{thm disjE}
+ THEN' rtac @{thm disjI2}
+ THEN' atac
+ THEN' rtac @{thm disjI1}
+ THEN' atac)*}
+
+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,
+ and after that the first.
+*}
+
+lemma "P1 \<or> Q1 \<Longrightarrow> Q1 \<or> P1"
+ and "P2 \<or> Q2 \<Longrightarrow> Q2 \<or> P2"
+apply(tactic {* foo_tac' 2 *})
+apply(tactic {* foo_tac' 1 *})
+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
+
+ @{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.
+
+ In the following example there are two possibilities for how to apply the tactic.
+*}
+
+lemma "\<lbrakk>P \<or> Q; P \<or> Q\<rbrakk> \<Longrightarrow> Q \<or> P"
+apply(tactic {* foo_tac' 1 *})
+back
+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.
+
+ \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.
+ \end{readmore}
+
+*}
+
+
+section {* Basic Tactics *}
+
+lemma shows "False \<Longrightarrow> False"
+apply(tactic {* atac 1 *})
+done
+
+lemma shows "True \<and> True"
+apply(tactic {* rtac @{thm conjI} 1 *})
+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"
+apply(tactic {* etac @{thm conjE} 1 *})
+txt {* @{subgoals [display]} *}
+(*<*)oops(*>*)
+
+lemma shows "False \<and> True \<Longrightarrow> False"
+apply(tactic {* dtac @{thm conjunct2} 1 *})
+txt {* @{subgoals [display]} *}
+(*<*)oops(*>*)
+
+text {*
+ similarly @{ML ftac}
+*}
+
+text {* diagnostics *}
+lemma shows "True \<Longrightarrow> False"
+apply(tactic {* print_tac "foo message" *})
+(*<*)oops(*>*)
+
+text {*
+ @{ML PRIMITIVE}? @{ML SUBGOAL} see page 32 in ref
+*}
+
+text {*
+ @{ML all_tac} @{ML no_tac}
+*}
+
+section {* Operations on Tactics *}
+
+text {* THEN *}
+
+lemma shows "(True \<and> True) \<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) *})
+txt {* @{subgoals [display]} *}
+(*<*)oops(*>*)
+
+
+text {*
+ @{ML EVERY} @{ML REPEAT} @{ML SUBPROOF}
+
+ @{ML rewrite_goals_tac}
+ @{ML cut_facts_tac}
+ @{ML ObjectLogic.full_atomize_tac}
+ @{ML ObjectLogic.rulify_tac}
+ @{ML resolve_tac}
+*}
+
+
+
+text {*
+
+
+ A goal (or goal state) is a special @{ML_type thm}, which by
+ convention is an implication of the form:
+
+ @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #(C)"}
+
+ where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the open
+ subgoals.
+ Since the goal @{term C} can potentially be an implication, there is a
+ @{text "#"} wrapped around it, which prevents that premises are
+ misinterpreted as open subgoals. The wrapper @{text "# :: prop \<Rightarrow>
+ prop"} is just the identity function and used as a syntactic marker.
+
+
+
+
+
+ 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.
+
+
+
+*}
+
+
+
+end
\ No newline at end of file