--- /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