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