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