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 {* 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)

fun str_of_thm ctxt thm =
  let
    val {prop, ...} = crep_thm thm
  in 
    str_of_cterm ctxt prop
  end

fun str_of_thms ctxt thms =  
  commas (map (str_of_thm ctxt) thms)*}

text {*
  and the following function
*}

ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = 
  let 
    val str_of_params = str_of_cterms context params
    val str_of_asms = str_of_cterms context asms
    val str_of_concl = str_of_cterm context concl
    val str_of_prems = str_of_thms context prems   
    val str_of_schms = str_of_cterms context (snd schematics)    
 
    val _ = (warning ("params: " ^ str_of_params);
             warning ("schematics: " ^ str_of_schms);
             warning ("asms: " ^ str_of_asms);
             warning ("concl: " ^ str_of_concl);
             warning ("prems: " ^ str_of_prems))
  in
    no_tac 
  end*}

text {*
  then the tactic @{ML SUBPROOF} fixes the parameters and binds the various components
  of a proof state into a record. For example 
*}

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 

  \begin{center}
  \begin{tabular}{ll}
  params:     & @{term x}, @{term y}\\
  schematics: & @{term z}\\
  asms:       & @{term "A x y"}\\
  concl:      & @{term "B y x \<longrightarrow> C (z y) x"}\\
  prems:      & @{term "A x y"}
  \end{tabular}
  \end{center}

  Continuing the proof script with
*}

apply(rule impI)
apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?

txt {*
  prints out 

  \begin{center}
  \begin{tabular}{ll}
  params:     & @{term x}, @{term y}\\
  schematics: & @{term z}\\
  asms:       & @{term "A x y"}, @{term "B y x"}\\
  concl:      & @{term "C (z y) x"}\\
  prems:      & @{term "A x y"}, @{term "B y x"}
  \end{tabular}
  \end{center}
*}
(*<*)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 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. 
 


*}

section {* Structured Proofs *}

lemma True
proof

  {
    fix A B C
    assume r: "A & B \<Longrightarrow> C"
    assume A B
    then have "A & B" ..
    then have C by (rule r)
  }

  {
    fix A B C
    assume r: "A & B \<Longrightarrow> C"
    assume A B
    note conjI [OF this]
    note r [OF this]
  }
oops

ML {* fun prop ctxt s =
  Thm.cterm_of (ProofContext.theory_of ctxt) (Syntax.read_prop ctxt s) *}

ML {* 
  val ctxt0 = @{context};
  val ctxt = ctxt0;
  val (_, ctxt) = Variable.add_fixes ["A", "B", "C"] ctxt;
  val ([r], ctxt) = Assumption.add_assumes [prop ctxt "A & B \<Longrightarrow> C"] ctxt;
  val (this, ctxt) = Assumption.add_assumes [prop ctxt "A", prop ctxt "B"] ctxt;
  val this = [@{thm conjI} OF this]; 
  val this = r OF this;
  val this = Assumption.export false ctxt ctxt0 this 
  val this = Variable.export ctxt ctxt0 [this] 
*}


end