1 theory Tactical

     2 imports Base

     3 begin

     4 

     5 chapter {* Tactical Reasoning\label{chp:tactical} *}

     6 

     7 text {*

     8 

     9   The main reason for descending to the ML-level of Isabelle is to be able to

    10   implement automatic proof procedures. Such proof procedures usually lessen

    11   considerably the burden of manual reasoning, for example, when introducing

    12   new definitions. These proof procedures are centred around refining a goal

    13   state using tactics. This is similar to the @{text apply}-style reasoning at

    14   the user level, where goals are modified in a sequence of proof steps until

    15   all of them are solved.

    16 

    17 

    18 *}

    19 

    20 section {* Tactical Reasoning *}

    21 

    22 text {*

    23   To see how tactics work, let us first transcribe a simple @{text apply}-style proof 

    24   into ML. Consider the following proof.

    25 *}

    26 

    27 lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"

    28 apply(erule disjE)

    29 apply(rule disjI2)

    30 apply(assumption)

    31 apply(rule disjI1)

    32 apply(assumption)

    33 done

    34 

    35 text {*

    36   This proof translates to the following ML-code.

    37   

    38 @{ML_response_fake [display,gray]

    39 "let

    40   val ctxt = @{context}

    41   val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}

    42 in

    43   Goal.prove ctxt [\"P\", \"Q\"] [] goal 

    44    (fn _ => 

    45       etac @{thm disjE} 1

    46       THEN rtac @{thm disjI2} 1

    47       THEN atac 1

    48       THEN rtac @{thm disjI1} 1

    49       THEN atac 1)

    50 end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}

    51   

    52   To start the proof, the function @{ML "Goal.prove"}~@{text "ctxt xs As C

    53   tac"} sets up a goal state for proving the goal @{text C} under the

    54   assumptions @{text As} (empty in the proof at hand) with the variables

    55   @{text xs} that will be generalised once the goal is proved (in our case

    56   @{text P} and @{text Q}). The @{text "tac"} is the tactic that proves the goal;

    57   it can make use of the local assumptions (there are none in this example). 

    58   The functions @{ML etac}, @{ML rtac} and @{ML atac} correspond to 

    59   @{text erule}, @{text rule} and @{text assumption}, respectively. 

    60   The operator @{ML THEN} strings tactics together.

    61 

    62   \begin{readmore}

    63   To learn more about the function @{ML Goal.prove} see \isccite{sec:results} and

    64   the file @{ML_file "Pure/goal.ML"}. For more information about the internals of goals see 

    65   \isccite{sec:tactical-goals}. 

    66   \end{readmore}

    67 

    68   Note that we used antiquotations for referencing the theorems. We could also

    69   just have written @{ML "etac disjE 1"} and so on, but this is considered bad

    70   style. The reason is that the binding for @{ML disjE} can be re-assigned by 

    71   the user and thus one does not have complete control over which theorem is

    72   actually applied. This problem is nicely prevented by using antiquotations, 

    73   because then the theorems are fixed statically at compile-time.

    74 

    75   During the development of automatic proof procedures, it will often be necessary 

    76   to test a tactic on examples. This can be conveniently 

    77   done with the command \isacommand{apply}@{text "(tactic \<verbopen> \<dots> \<verbclose>)"}. 

    78   Consider the following sequence of tactics

    79 *}

    80 

    81 ML{*val foo_tac = 

    82       (etac @{thm disjE} 1

    83        THEN rtac @{thm disjI2} 1

    84        THEN atac 1

    85        THEN rtac @{thm disjI1} 1

    86        THEN atac 1)*}

    87 

    88 text {* and the Isabelle proof: *}

    89 

    90 lemma "P \<or> Q \<Longrightarrow> Q \<or> P"

    91 apply(tactic {* foo_tac *})

    92 done

    93 

    94 text {*

    95   The apply-step applies the @{ML foo_tac} and therefore solves the goal completely.  

    96   Inside @{text "tactic \<verbopen> \<dots> \<verbclose>"} 

    97   we can call any function that returns a tactic.

    98 

    99   As can be seen, each tactic in @{ML foo_tac} has a hard-coded number that

   100   stands for the subgoal analysed by the tactic. In our case, we only focus on the first

   101   subgoal. This is sometimes wanted, but usually not. To avoid the explicit numbering in the 

   102   tactic, you can write

   103 *}

   104 

   105 ML{*val foo_tac' = 

   106       (etac @{thm disjE} 

   107        THEN' rtac @{thm disjI2} 

   108        THEN' atac 

   109        THEN' rtac @{thm disjI1} 

   110        THEN' atac)*}

   111 

   112 text {* 

   113   and then give the number for the subgoal explicitly when the tactic is

   114   called. So in the next proof we discharge first the second subgoal,

   115   and after that the first.

   116 *}

   117 

   118 lemma "P1 \<or> Q1 \<Longrightarrow> Q1 \<or> P1"

   119    and "P2 \<or> Q2 \<Longrightarrow> Q2 \<or> P2"

   120 apply(tactic {* foo_tac' 2 *})

   121 apply(tactic {* foo_tac' 1 *})

   122 done

   123 

   124 text {*

   125   The tactic @{ML foo_tac} is very specific for analysing goals of the form

   126   @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not of this form, then @{ML foo_tac}

   127   throws the error message about an empty result sequence---meaning the tactic

   128   failed. The reason for this message is that tactics are functions that map 

   129   a goal state to a (lazy) sequence of successor states, hence the type of a 

   130   tactic is

   131   

   132   @{text [display, gray] "type tactic = thm -> thm Seq.seq"}

   133 

   134   Consequently, if a tactic fails, then it returns the empty sequence. This

   135   is by the way the default behaviour for a failing tactic; tactics should 

   136   not raise exceptions.

   137 

   138   In the following example there are two possibilities for how to apply the tactic.

   139 *}

   140 

   141 lemma "\<lbrakk>P \<or> Q; P \<or> Q\<rbrakk> \<Longrightarrow> Q \<or> P"

   142 apply(tactic {* foo_tac' 1 *})

   143 back

   144 done

   145 

   146 text {*

   147   The application of the tactic results in a sequence of two possible

   148   proofs. The Isabelle command \isacommand{back} allows us to explore both 

   149   possibilities.

   150 

   151   \begin{readmore}

   152   See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy

   153   sequences. However in day-to-day Isabelle programming, one rarely 

   154   constructs sequences explicitly, but uses the predefined functions

   155   instead. See @{ML_file "Pure/tactic.ML"} and 

   156   @{ML_file "Pure/tctical.ML"} for the code of basic tactics and tactic

   157   combinators; see also Chapters 3 and 4 in 

   158   the old Isabelle Reference Manual.

   159   \end{readmore}

   160 

   161 *}

   162 

   163 

   164 section {* Basic Tactics *}

   165 

   166 lemma shows "False \<Longrightarrow> False"

   167 apply(tactic {* atac 1 *})

   168 done

   169 

   170 lemma shows "True \<and> True"

   171 apply(tactic {* rtac @{thm conjI} 1 *})

   172 txt {* @{subgoals [display]} *}

   173 (*<*)oops(*>*)

   174 

   175 lemma 

   176   shows "Foo"

   177   and "True \<and> True"

   178 apply(tactic {* rtac @{thm conjI} 2 *})

   179 txt {* @{subgoals [display]} *}

   180 (*<*)oops(*>*)

   181 

   182 lemma shows "False \<and> False \<Longrightarrow> False"

   183 apply(tactic {* etac @{thm conjE} 1 *})

   184 txt {* @{subgoals [display]} *}

   185 (*<*)oops(*>*)

   186 

   187 lemma shows "False \<and> True \<Longrightarrow> False"

   188 apply(tactic {* dtac @{thm conjunct2} 1 *})

   189 txt {* @{subgoals [display]} *}

   190 (*<*)oops(*>*)

   191 

   192 text {*

   193   similarly @{ML ftac}

   194 *}

   195 

   196 text {* diagnostics *} 

   197 lemma shows "True \<Longrightarrow> False"

   198 apply(tactic {* print_tac "foo message" *})

   199 (*<*)oops(*>*)

   200 

   201 text {*

   202   @{ML PRIMITIVE}? @{ML SUBGOAL} see page 32 in ref

   203 *}

   204 

   205 text {* 

   206   @{ML all_tac} @{ML no_tac}

   207 *}

   208 

   209 section {* Operations on Tactics *}

   210 

   211 text {* THEN *}

   212 

   213 lemma shows "(True \<and> True) \<and> False"

   214 apply(tactic {* (rtac @{thm conjI} 1) THEN (rtac @{thm conjI} 1) *})

   215 txt {* @{subgoals [display]} *}

   216 (*<*)oops(*>*)

   217 

   218 lemma shows "True \<and> False"

   219 apply(tactic {* (rtac @{thm disjI1} 1) ORELSE (rtac @{thm conjI} 1) *})

   220 txt {* @{subgoals [display]} *}

   221 (*<*)oops(*>*)

   222 

   223 

   224 text {*

   225   @{ML EVERY} @{ML REPEAT} @{ML SUBPROOF}

   226 

   227   @{ML rewrite_goals_tac}

   228   @{ML cut_facts_tac}

   229   @{ML ObjectLogic.full_atomize_tac}

   230   @{ML ObjectLogic.rulify_tac}

   231   @{ML resolve_tac}

   232 *}

   233 

   234 

   235 

   236 text {*

   237 

   238 

   239   A goal (or goal state) is a special @{ML_type thm}, which by

   240   convention is an implication of the form:

   241 

   242   @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #(C)"}

   243 

   244   where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the open 

   245   subgoals. 

   246   Since the goal @{term C} can potentially be an implication, there is a

   247   @{text "#"} wrapped around it, which prevents that premises are 

   248   misinterpreted as open subgoals. The wrapper @{text "# :: prop \<Rightarrow>

   249   prop"} is just the identity function and used as a syntactic marker. 

   250   

   251  

   252 

   253  

   254 

   255   While tactics can operate on the subgoals (the @{text "A\<^isub>i"} above), they 

   256   are expected to leave the conclusion @{term C} intact, with the 

   257   exception of possibly instantiating schematic variables. 

   258  

   259 

   260 

   261 *}

   262 

   263 

   264 

   265 end