1 theory Tactical

     2 imports Base FirstSteps

     3 begin

     4 

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

     6 

     7 text {*

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

     9   implement automatic proof procedures. Such proof procedures usually lessen

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

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

    12   state using tactics. This is similar to the \isacommand{apply}-style

    13   reasoning at the user-level, where goals are modified in a sequence of proof

    14   steps until all of them are solved. However, there are also more structured

    15   operations available on the ML-level that help with the handling of

    16   variables and assumptions.

    17 

    18 *}

    19 

    20 section {* Basics of Reasoning with Tactics*}

    21 

    22 text {*

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

    24   into ML. Suppose 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} 

    54   (that is @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"} in the proof at hand) under the

    55   assumptions @{text As} (happens to be empty) with the variables

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

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

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

    59   The functions @{ML etac}, @{ML rtac} and @{ML atac} in the code above correspond to 

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

    61   The operator @{ML THEN} strings the tactics together. 

    62 

    63   \begin{readmore}

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

    65   and the file @{ML_file "Pure/goal.ML"}.  See @{ML_file

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

    67   tactics and tactic combinators; see also Chapters 3 and 4 in the old

    68   Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation Manual. 

    69   \end{readmore}

    70 

    71   Note that in the code above we use antiquotations for referencing the theorems. Many theorems

    72   also have ML-bindings with the same name. Therefore, we could also just have

    73   written @{ML "etac disjE 1"}, or in case where there are no ML-binding obtain

    74   the theorem dynamically using the function @{ML thm}; for example 

    75   \mbox{@{ML  "etac (thm \"disjE\") 1"}}. Both ways however are considered bad style! 

    76   The reason

    77   is that the binding for @{ML disjE} can be re-assigned by the user and thus

    78   one does not have complete control over which theorem is actually

    79   applied. This problem is nicely prevented by using antiquotations, because

    80   then the theorems are fixed statically at compile-time.

    81 

    82   During the development of automatic proof procedures, you will often find it 

    83   necessary to test a tactic on examples. This can be conveniently 

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

    85   Consider the following sequence of tactics

    86 *}

    87 

    88 ML{*val foo_tac = 

    89       (etac @{thm disjE} 1

    90        THEN rtac @{thm disjI2} 1

    91        THEN atac 1

    92        THEN rtac @{thm disjI1} 1

    93        THEN atac 1)*}

    94 

    95 text {* and the Isabelle proof: *}

    96 

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

    98 apply(tactic {* foo_tac *})

    99 done

   100 

   101 text {*

   102   By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} you can call from the 

   103   user-level of Isabelle the tactic @{ML foo_tac} or 

   104   any other function that returns a tactic.

   105 

   106   The tactic @{ML foo_tac} is just a sequence of simple tactics stringed

   107   together by @{ML THEN}. As can be seen, each simple tactic in @{ML foo_tac}

   108   has a hard-coded number that stands for the subgoal analysed by the

   109   tactic (@{text "1"} stands for the first, or top-most, subgoal). This hard-coding

   110   of goals is sometimes wanted, but usually it is not. To avoid the explicit numbering, 

   111   you can write\label{tac:footacprime}

   112 *}

   113 

   114 ML{*val foo_tac' = 

   115       (etac @{thm disjE} 

   116        THEN' rtac @{thm disjI2} 

   117        THEN' atac 

   118        THEN' rtac @{thm disjI1} 

   119        THEN' atac)*}

   120 

   121 text {* 

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

   123   called. So in the next proof you can first discharge the second subgoal, and

   124   subsequently the first.

   125 *}

   126 

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

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

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

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

   131 done

   132 

   133 text {*

   134   This kind of addressing is more difficult to achieve when the goal is 

   135   hard-coded inside the tactic. For most operators that combine tactics 

   136   (@{ML THEN} is only one such operator) a ``primed'' version exists.

   137 

   138   The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for

   139   analysing goals being only of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not

   140   of this form, then these tactics return the error message:

   141 

   142   \begin{isabelle}

   143   @{text "*** empty result sequence -- proof command failed"}\\

   144   @{text "*** At command \"apply\"."}

   145   \end{isabelle}

   146 

   147   This means they failed. The reason for this error message is that tactics 

   148   are functions mapping a goal state to a (lazy) sequence of successor states. 

   149   Hence the type of a tactic is:

   150 *}

   151   

   152 ML{*type tactic = thm -> thm Seq.seq*}

   153 

   154 text {*

   155   By convention, if a tactic fails, then it should return the empty sequence. 

   156   Therefore, if you write your own tactics, they  should not raise exceptions 

   157   willy-nilly; only in very grave failure situations should a tactic raise the 

   158   exception @{text THM}.

   159 

   160   The simplest tactics are @{ML no_tac} and @{ML all_tac}. The first returns

   161   the empty sequence and is defined as

   162 *}

   163 

   164 ML{*fun no_tac thm = Seq.empty*}

   165 

   166 text {*

   167   which means @{ML no_tac} always fails. The second returns the given theorem wrapped 

   168   in a single member sequence; it is defined as

   169 *}

   170 

   171 ML{*fun all_tac thm = Seq.single thm*}

   172 

   173 text {*

   174   which means @{ML all_tac} always succeeds, but also does not make any progress 

   175   with the proof.

   176 

   177   The lazy list of possible successor goal states shows through at the user-level 

   178   of Isabelle when using the command \isacommand{back}. For instance in the 

   179   following proof there are two possibilities for how to apply 

   180   @{ML foo_tac'}: either using the first assumption or the second.

   181 *}

   182 

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

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

   185 back

   186 done

   187 

   188 

   189 text {*

   190   By using \isacommand{back}, we construct the proof that uses the

   191   second assumption. While in the proof above, it does not really matter which 

   192   assumption is used, in more interesting cases provability might depend

   193   on exploring different possibilities.

   194   

   195   \begin{readmore}

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

   197   sequences. In day-to-day Isabelle programming, however, one rarely 

   198   constructs sequences explicitly, but uses the predefined tactics and 

   199   tactic combinators instead.

   200   \end{readmore}

   201 

   202   It might be surprising that tactics, which transform

   203   one goal state to the next, are functions from theorems to theorem 

   204   (sequences). The surprise resolves by knowing that every 

   205   goal state is indeed a theorem. To shed more light on this,

   206   let us modify the code of @{ML all_tac} to obtain the following

   207   tactic

   208 *}

   209 

   210 ML{*fun my_print_tac ctxt thm =

   211 let

   212   val _ = warning (str_of_thm ctxt thm)

   213 in 

   214   Seq.single thm

   215 end*}

   216 

   217 text_raw {*

   218   \begin{figure}[p]

   219   \begin{boxedminipage}{\textwidth}

   220   \begin{isabelle}

   221 *}

   222 lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B" 

   223 apply(tactic {* my_print_tac @{context} *})

   224 

   225 txt{* \begin{minipage}{\textwidth}

   226       @{subgoals [display]} 

   227       \end{minipage}\medskip      

   228 

   229       \begin{minipage}{\textwidth}

   230       \small\colorbox{gray!20}{

   231       \begin{tabular}{@ {}l@ {}}

   232       internal goal state:\\

   233       @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}

   234       \end{tabular}}

   235       \end{minipage}\medskip

   236 *}

   237 

   238 apply(rule conjI)

   239 apply(tactic {* my_print_tac @{context} *})

   240 

   241 txt{* \begin{minipage}{\textwidth}

   242       @{subgoals [display]} 

   243       \end{minipage}\medskip

   244 

   245       \begin{minipage}{\textwidth}

   246       \small\colorbox{gray!20}{

   247       \begin{tabular}{@ {}l@ {}}

   248       internal goal state:\\

   249       @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}

   250       \end{tabular}}

   251       \end{minipage}\medskip

   252 *}

   253 

   254 apply(assumption)

   255 apply(tactic {* my_print_tac @{context} *})

   256 

   257 txt{* \begin{minipage}{\textwidth}

   258       @{subgoals [display]} 

   259       \end{minipage}\medskip

   260 

   261       \begin{minipage}{\textwidth}

   262       \small\colorbox{gray!20}{

   263       \begin{tabular}{@ {}l@ {}}

   264       internal goal state:\\

   265       @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}

   266       \end{tabular}}

   267       \end{minipage}\medskip

   268 *}

   269 

   270 apply(assumption)

   271 apply(tactic {* my_print_tac @{context} *})

   272 

   273 txt{* \begin{minipage}{\textwidth}

   274       @{subgoals [display]} 

   275       \end{minipage}\medskip 

   276   

   277       \begin{minipage}{\textwidth}

   278       \small\colorbox{gray!20}{

   279       \begin{tabular}{@ {}l@ {}}

   280       internal goal state:\\

   281       @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}

   282       \end{tabular}}

   283       \end{minipage}\medskip   

   284    *}

   285 done

   286 text_raw {*  

   287   \end{isabelle}

   288   \end{boxedminipage}

   289   \caption{The figure shows a proof where each intermediate goal state is

   290   printed by the Isabelle system and by @{ML my_print_tac}. The latter shows

   291   the goal state as represented internally (highlighted boxes). This

   292   tactic shows that every goal state in Isabelle is represented by a theorem:

   293   when you start the proof of \mbox{@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}} the theorem is

   294   @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when you finish the proof the

   295   theorem is @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}.\label{fig:goalstates}}

   296   \end{figure}

   297 *}

   298 

   299 

   300 text {*

   301   which prints out the given theorem (using the string-function defined in

   302   Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. With this

   303   tactic we are in the position to inspect every goal state in a

   304   proof. Consider now the proof in Figure~\ref{fig:goalstates}: as can be seen, 

   305   internally every goal state is an implication of the form

   306 

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

   308 

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

   310   the subgoals. So after setting up the lemma, the goal state is always of the

   311   form @{text "C \<Longrightarrow> (C)"}; when the proof is finished we are left with @{text

   312   "(C)"}. Since the goal @{term C} can potentially be an implication, there is

   313   a ``protector'' wrapped around it (in from of an outermost constant @{text

   314   "Const (\"prop\", bool \<Rightarrow> bool)"}; however this constant

   315   is invisible in the figure). This wrapper prevents that premises of @{text C} are

   316   mis-interpreted as open subgoals. While tactics can operate on the subgoals

   317   (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion

   318   @{term C} intact, with the exception of possibly instantiating schematic

   319   variables. If you use the predefined tactics, which we describe in the next

   320   section, this will always be the case.

   321  

   322   \begin{readmore}

   323   For more information about the internals of goals see \isccite{sec:tactical-goals}.

   324   \end{readmore}

   325 

   326 *}

   327 

   328 section {* Simple Tactics *}

   329 

   330 text {*

   331   Let us start with explaining the simple tactic @{ML print_tac}, which is quite useful 

   332   for low-level debugging of tactics. It just prints out a message and the current 

   333   goal state. Unlike @{ML my_print_tac} shown earlier, it prints the goal state 

   334   as the user would see it.  For example, processing the proof

   335 *}

   336  

   337 lemma shows "False \<Longrightarrow> True"

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

   339 txt{*gives:\medskip

   340 

   341      \begin{minipage}{\textwidth}\small

   342      @{text "foo message"}\\[3mm] 

   343      @{prop "False \<Longrightarrow> True"}\\

   344      @{text " 1. False \<Longrightarrow> True"}\\

   345      \end{minipage}

   346    *}

   347 (*<*)oops(*>*)

   348 

   349 text {*

   350   Another simple tactic is the function @{ML atac}, which, as shown in the previous

   351   section, corresponds to the assumption command.

   352 *}

   353 

   354 lemma shows "P \<Longrightarrow> P"

   355 apply(tactic {* atac 1 *})

   356 txt{*\begin{minipage}{\textwidth}

   357      @{subgoals [display]}

   358      \end{minipage}*}

   359 (*<*)oops(*>*)

   360 

   361 text {*

   362   Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond

   363   to @{text rule}, @{text drule}, @{text erule} and @{text frule}, 

   364   respectively. Each of them takes a theorem as argument and attempts to 

   365   apply it to a goal. Below are three self-explanatory examples.

   366 *}

   367 

   368 lemma shows "P \<and> Q"

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

   370 txt{*\begin{minipage}{\textwidth}

   371      @{subgoals [display]}

   372      \end{minipage}*}

   373 (*<*)oops(*>*)

   374 

   375 lemma shows "P \<and> Q \<Longrightarrow> False"

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

   377 txt{*\begin{minipage}{\textwidth}

   378      @{subgoals [display]}

   379      \end{minipage}*}

   380 (*<*)oops(*>*)

   381 

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

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

   384 txt{*\begin{minipage}{\textwidth}

   385      @{subgoals [display]}

   386      \end{minipage}*}

   387 (*<*)oops(*>*)

   388 

   389 text {*

   390   Note the number in each tactic call. Also as mentioned in the previous section, most 

   391   basic tactics take such a number as argument: this argument addresses the subgoal 

   392   the tacics are analysing. In the proof below, we first split up the conjunction in  

   393   the second subgoal by focusing on this subgoal first.

   394 *}

   395 

   396 lemma shows "Foo" and "P \<and> Q"

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

   398 txt {*\begin{minipage}{\textwidth}

   399       @{subgoals [display]}

   400       \end{minipage}*}

   401 (*<*)oops(*>*)

   402 

   403 text {*

   404   The function @{ML resolve_tac} is similar to @{ML rtac}, except that it

   405   expects a list of theorems as arguments. From this list it will apply the

   406   first applicable theorem (later theorems that are also applicable can be

   407   explored via the lazy sequences mechanism). Given the code

   408 *}

   409 

   410 ML{*val resolve_tac_xmp = resolve_tac [@{thm impI}, @{thm conjI}]*}

   411 

   412 text {*

   413   an example for @{ML resolve_tac} is the following proof where first an outermost 

   414   implication is analysed and then an outermost conjunction.

   415 *}

   416 

   417 lemma shows "C \<longrightarrow> (A \<and> B)" and "(A \<longrightarrow> B) \<and> C"

   418 apply(tactic {* resolve_tac_xmp 1 *})

   419 apply(tactic {* resolve_tac_xmp 2 *})

   420 txt{*\begin{minipage}{\textwidth}

   421      @{subgoals [display]} 

   422      \end{minipage}*}

   423 (*<*)oops(*>*)

   424 

   425 text {* 

   426   Similar versions taking a list of theorems exist for the tactics 

   427   @{ML dtac} (@{ML dresolve_tac}), @{ML etac} (@{ML eresolve_tac}) and so on.

   428 

   429 

   430   Another simple tactic is @{ML cut_facts_tac}. It inserts a list of theorems

   431   into the assumptions of the current goal state. For example

   432 *}

   433 

   434 lemma shows "True \<noteq> False"

   435 apply(tactic {* cut_facts_tac [@{thm True_def}, @{thm False_def}] 1 *})

   436 txt{*produces the goal state\medskip

   437 

   438      \begin{minipage}{\textwidth}

   439      @{subgoals [display]} 

   440      \end{minipage}*}

   441 (*<*)oops(*>*)

   442 

   443 text {*

   444   Since rules are applied using higher-order unification, an automatic proof

   445   procedure might become too fragile, if it just applies inference rules as 

   446   shown above. The reason is that a number of rules introduce meta-variables 

   447   into the goal state. Consider for example the proof

   448 *}

   449 

   450 lemma shows "\<forall>x\<in>A. P x \<Longrightarrow> Q x"

   451 apply(tactic {* dtac @{thm bspec} 1 *})

   452 txt{*\begin{minipage}{\textwidth}

   453      @{subgoals [display]} 

   454      \end{minipage}*}

   455 (*<*)oops(*>*)

   456 

   457 text {*

   458   where the application of rule @{text bspec} generates two subgoals involving the

   459   meta-variable @{text "?x"}. Now, if you are not careful, tactics 

   460   applied to the first subgoal might instantiate this meta-variable in such a 

   461   way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"}

   462   should be, then this situation can be avoided by introducing a more

   463   constraint version of the @{text bspec}-rule. Such constraints can be given by

   464   pre-instantiating theorems with other theorems. One function to do this is

   465   @{ML RS}

   466   

   467   @{ML_response_fake [display,gray]

   468   "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}

   469 

   470   which in the example instantiates the first premise of the @{text conjI}-rule 

   471   with the rule @{text disjI1}. If the instantiation is impossible, as in the 

   472   case of

   473 

   474   @{ML_response_fake_both [display,gray]

   475   "@{thm conjI} RS @{thm mp}" 

   476 "*** Exception- THM (\"RSN: no unifiers\", 1, 

   477 [\"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\", \"\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\"]) raised"}

   478 

   479   then the function raises an exception. The function @{ML RSN} is similar to @{ML RS}, but 

   480   takes an additional number as argument that makes explicit which premise 

   481   should be instantiated. 

   482 

   483   To improve readability of the theorems we produce below, we shall use the

   484   function @{ML no_vars} from Section~\ref{sec:printing}, which transforms

   485   schematic variables into free ones.  Using this function for the first @{ML

   486   RS}-expression above produces the more readable result:

   487 

   488   @{ML_response_fake [display,gray]

   489   "no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> Q"}

   490 

   491   If you want to instantiate more than one premise of a theorem, you can use 

   492   the function @{ML MRS}:

   493 

   494   @{ML_response_fake [display,gray]

   495   "no_vars @{context} ([@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI})" 

   496   "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> (Pa \<or> Q)"}

   497 

   498   If you need to instantiate lists of theorems, you can use the

   499   functions @{ML RL} and @{ML MRL}. For example in the code below,

   500   every theorem in the second list is instantiated with every 

   501   theorem in the first.

   502 

   503   @{ML_response_fake [display,gray]

   504    "[@{thm impI}, @{thm disjI2}] RL [@{thm conjI}, @{thm disjI1}]" 

   505 "[\<lbrakk>P \<Longrightarrow> Q; Qa\<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) \<and> Qa,

   506  \<lbrakk>Q; Qa\<rbrakk> \<Longrightarrow> (P \<or> Q) \<and> Qa,

   507  (P \<Longrightarrow> Q) \<Longrightarrow> (P \<longrightarrow> Q) \<or> Qa,

   508  Q \<Longrightarrow> (P \<or> Q) \<or> Qa]"}

   509 

   510   \begin{readmore}

   511   The combinators for instantiating theorems are defined in @{ML_file "Pure/drule.ML"}.

   512   \end{readmore}

   513 

   514   Often proofs on the ML-level involve elaborate operations on assumptions and 

   515   @{text "\<And>"}-quantified variables. To do such operations using the basic tactics 

   516   shown so far is very unwieldy and brittle. Some convenience and

   517   safety is provided by the tactic @{ML SUBPROOF}. This tactic fixes the parameters 

   518   and binds the various components of a goal state to a record. 

   519   To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which

   520   takes a record and just prints out the content of this record (using the 

   521   string transformation functions from in Section~\ref{sec:printing}). Consider

   522   now the proof:

   523 *}

   524 

   525 text_raw{*

   526 \begin{figure}[t]

   527 \begin{minipage}{\textwidth}

   528 \begin{isabelle}

   529 *}

   530 ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = 

   531 let 

   532   val str_of_params = str_of_cterms context params

   533   val str_of_asms = str_of_cterms context asms

   534   val str_of_concl = str_of_cterm context concl

   535   val str_of_prems = str_of_thms context prems   

   536   val str_of_schms = str_of_cterms context (snd schematics)    

   537  

   538   val _ = (warning ("params: " ^ str_of_params);

   539            warning ("schematics: " ^ str_of_schms);

   540            warning ("assumptions: " ^ str_of_asms);

   541            warning ("conclusion: " ^ str_of_concl);

   542            warning ("premises: " ^ str_of_prems))

   543 in

   544   no_tac 

   545 end*}

   546 text_raw{*

   547 \end{isabelle}

   548 \end{minipage}

   549 \caption{A function that prints out the various parameters provided by the tactic

   550  @{ML SUBPROOF}. It uses the functions defined in Section~\ref{sec:printing} for

   551   extracting strings from @{ML_type cterm}s and @{ML_type thm}s.\label{fig:sptac}}

   552 \end{figure}

   553 *}

   554 

   555 

   556 lemma shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"

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

   558 

   559 txt {*

   560   The tactic produces the following printout:

   561 

   562   \begin{quote}\small

   563   \begin{tabular}{ll}

   564   params:      & @{term x}, @{term y}\\

   565   schematics:  & @{term z}\\

   566   assumptions: & @{term "A x y"}\\

   567   conclusion:  & @{term "B y x \<longrightarrow> C (z y) x"}\\

   568   premises:    & @{term "A x y"}

   569   \end{tabular}

   570   \end{quote}

   571 

   572   Notice in the actual output the brown colour of the variables @{term x} and 

   573   @{term y}. Although they are parameters in the original goal, they are fixed inside

   574   the subproof. By convention these fixed variables are printed in brown colour.

   575   Similarly the schematic variable @{term z}. The assumption, or premise, 

   576   @{prop "A x y"} is bound as @{ML_type cterm} to the record-variable 

   577   @{text asms}, but also as @{ML_type thm} to @{text prems}.

   578 

   579   Notice also that we had to append @{text [quotes] "?"} to the

   580   \isacommand{apply}-command. The reason is that @{ML SUBPROOF} normally

   581   expects that the subgoal is solved completely.  Since in the function @{ML

   582   sp_tac} we returned the tactic @{ML no_tac}, the subproof obviously

   583   fails. The question-mark allows us to recover from this failure in a

   584   graceful manner so that the warning messages are not overwritten by an 

   585   ``empty sequence'' error message.

   586 

   587   If we continue the proof script by applying the @{text impI}-rule

   588 *}

   589 

   590 apply(rule impI)

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

   592 

   593 txt {*

   594   then the tactic prints out: 

   595 

   596   \begin{quote}\small

   597   \begin{tabular}{ll}

   598   params:      & @{term x}, @{term y}\\

   599   schematics:  & @{term z}\\

   600   assumptions: & @{term "A x y"}, @{term "B y x"}\\

   601   conclusion:  & @{term "C (z y) x"}\\

   602   premises:    & @{term "A x y"}, @{term "B y x"}

   603   \end{tabular}

   604   \end{quote}

   605 *}

   606 (*<*)oops(*>*)

   607 

   608 text {*

   609   Now also @{term "B y x"} is an assumption bound to @{text asms} and @{text prems}.

   610 

   611   One convenience of @{ML SUBPROOF} is that we can apply the assumptions

   612   using the usual tactics, because the parameter @{text prems} 

   613   contains them as theorems. With this you can easily 

   614   implement a tactic that behaves almost like @{ML atac}:

   615 *}

   616 

   617 ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*}

   618 

   619 text {*

   620   If you apply @{ML atac'} to the next lemma

   621 *}

   622 

   623 lemma shows "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"

   624 apply(tactic {* atac' @{context} 1 *})

   625 txt{* it will produce

   626       @{subgoals [display]} *}

   627 (*<*)oops(*>*)

   628 

   629 text {*

   630   The restriction in this tactic which is not present in @{ML atac} is 

   631   that it cannot instantiate any

   632   schematic variable. This might be seen as a defect, but it is actually

   633   an advantage in the situations for which @{ML SUBPROOF} was designed: 

   634   the reason is that, as mentioned before, instantiation of schematic variables can affect 

   635   several goals and can render them unprovable. @{ML SUBPROOF} is meant 

   636   to avoid this.

   637 

   638   Notice that @{ML atac'} inside @{ML SUBPROOF} calls @{ML resolve_tac} with 

   639   the subgoal number @{text "1"} and also the outer call to @{ML SUBPROOF} in 

   640   the \isacommand{apply}-step uses @{text "1"}. This is another advantage 

   641   of @{ML SUBPROOF}: the addressing  inside it is completely 

   642   local to the tactic inside the subproof. It is therefore possible to also apply 

   643   @{ML atac'} to the second goal by just writing:

   644 *}

   645 

   646 lemma shows "True" and "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"

   647 apply(tactic {* atac' @{context} 2 *})

   648 apply(rule TrueI)

   649 done

   650 

   651 

   652 text {*

   653   \begin{readmore}

   654   The function @{ML SUBPROOF} is defined in @{ML_file "Pure/subgoal.ML"} and

   655   also described in \isccite{sec:results}. 

   656   \end{readmore}

   657 

   658   Similar but less powerful functions than @{ML SUBPROOF} are @{ML SUBGOAL}

   659   and @{ML CSUBGOAL}. They allow you to inspect a given subgoal (the former

   660   presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type

   661   cterm}). With this you can implement a tactic that applies a rule according

   662   to the topmost logic connective in the subgoal (to illustrate this we only

   663   analyse a few connectives). The code of the tactic is as

   664   follows.\label{tac:selecttac}

   665 

   666 *}

   667 

   668 ML %linenosgray{*fun select_tac (t, i) =

   669   case t of

   670      @{term "Trueprop"} $ t' => select_tac (t', i)

   671    | @{term "op \<Longrightarrow>"} $ _ $ t' => select_tac (t', i)

   672    | @{term "op \<and>"} $ _ $ _ => rtac @{thm conjI} i

   673    | @{term "op \<longrightarrow>"} $ _ $ _ => rtac @{thm impI} i

   674    | @{term "Not"} $ _ => rtac @{thm notI} i

   675    | Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i

   676    | _ => all_tac*}

   677 

   678 text {*

   679   The input of the function is a term representing the subgoal and a number

   680   specifying the subgoal of interest. In Line 3 you need to descend under the

   681   outermost @{term "Trueprop"} in order to get to the connective you like to

   682   analyse. Otherwise goals like @{prop "A \<and> B"} are not properly

   683   analysed. Similarly with meta-implications in the next line.  While for the

   684   first five patterns we can use the @{text "@term"}-antiquotation to

   685   construct the patterns, the pattern in Line 8 cannot be constructed in this

   686   way. The reason is that an antiquotation would fix the type of the

   687   quantified variable. So you really have to construct the pattern using the

   688   basic term-constructors. This is not necessary in other cases, because their

   689   type is always fixed to function types involving only the type @{typ

   690   bool}. (See Section \ref{sec:terms_types_manually} about constructing terms

   691   manually.) For the catch-all pattern, we chose to just return @{ML all_tac}. 

   692   Consequently, @{ML select_tac} never fails.

   693 

   694 

   695   Let us now see how to apply this tactic. Consider the four goals:

   696 *}

   697 

   698 

   699 lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"

   700 apply(tactic {* SUBGOAL select_tac 4 *})

   701 apply(tactic {* SUBGOAL select_tac 3 *})

   702 apply(tactic {* SUBGOAL select_tac 2 *})

   703 apply(tactic {* SUBGOAL select_tac 1 *})

   704 txt{* \begin{minipage}{\textwidth}

   705       @{subgoals [display]}

   706       \end{minipage} *}

   707 (*<*)oops(*>*)

   708 

   709 text {*

   710   where in all but the last the tactic applied an introduction rule. 

   711   Note that we applied the tactic to the goals in ``reverse'' order. 

   712   This is a trick in order to be independent from the subgoals that are 

   713   produced by the rule. If we had applied it in the other order 

   714 *}

   715 

   716 lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"

   717 apply(tactic {* SUBGOAL select_tac 1 *})

   718 apply(tactic {* SUBGOAL select_tac 3 *})

   719 apply(tactic {* SUBGOAL select_tac 4 *})

   720 apply(tactic {* SUBGOAL select_tac 5 *})

   721 (*<*)oops(*>*)

   722 

   723 text {*

   724   then we have to be careful to not apply the tactic to the two subgoals produced by 

   725   the first goal. To do this can result in quite messy code. In contrast, 

   726   the ``reverse application'' is easy to implement.

   727 

   728   Of course, this example is

   729   contrived: there are much simpler methods available in Isabelle for

   730   implementing a proof procedure analysing a goal according to its topmost

   731   connective. These simpler methods use tactic combinators, which we will

   732   explain in the next section.

   733 

   734 *}

   735 

   736 section {* Tactic Combinators *}

   737 

   738 text {* 

   739   The purpose of tactic combinators is to build compound tactics out of

   740   smaller tactics. In the previous section we already used @{ML THEN}, which

   741   just strings together two tactics in a sequence. For example:

   742 *}

   743 

   744 lemma shows "(Foo \<and> Bar) \<and> False"

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

   746 txt {* \begin{minipage}{\textwidth}

   747        @{subgoals [display]} 

   748        \end{minipage} *}

   749 (*<*)oops(*>*)

   750 

   751 text {*

   752   If you want to avoid the hard-coded subgoal addressing, then you can use

   753   the ``primed'' version of @{ML THEN}. For example:

   754 *}

   755 

   756 lemma shows "(Foo \<and> Bar) \<and> False"

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

   758 txt {* \begin{minipage}{\textwidth}

   759        @{subgoals [display]} 

   760        \end{minipage} *}

   761 (*<*)oops(*>*)

   762 

   763 text {* 

   764   Here you only have to specify the subgoal of interest only once and

   765   it is consistently applied to the component tactics.

   766   For most tactic combinators such a ``primed'' version exists and

   767   in what follows we will usually prefer it over the ``unprimed'' one. 

   768 

   769   If there is a list of tactics that should all be tried out in 

   770   sequence, you can use the combinator @{ML EVERY'}. For example

   771   the function @{ML foo_tac'} from page~\pageref{tac:footacprime} can also 

   772   be written as:

   773 *}

   774 

   775 ML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2}, 

   776                         atac, rtac @{thm disjI1}, atac]*}

   777 

   778 text {*

   779   There is even another way of implementing this tactic: in automatic proof

   780   procedures (in contrast to tactics that might be called by the user) there

   781   are often long lists of tactics that are applied to the first

   782   subgoal. Instead of writing the code above and then calling @{ML "foo_tac'' 1"}, 

   783   you can also just write

   784 *}

   785 

   786 ML{*val foo_tac1 = EVERY1 [etac @{thm disjE}, rtac @{thm disjI2}, 

   787                        atac, rtac @{thm disjI1}, atac]*}

   788 

   789 text {*

   790   and call @{ML foo_tac1}.  

   791 

   792   With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML EVERY1} it must be

   793   guaranteed that all component tactics successfully apply; otherwise the

   794   whole tactic will fail. If you rather want to try out a number of tactics,

   795   then you can use the combinator @{ML ORELSE'} for two tactics, and @{ML

   796   FIRST'} (or @{ML FIRST1}) for a list of tactics. For example, the tactic

   797 

   798 *}

   799 

   800 ML{*val orelse_xmp = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*}

   801 

   802 text {*

   803   will first try out whether rule @{text disjI} applies and after that 

   804   @{text conjI}. To see this consider the proof

   805 *}

   806 

   807 lemma shows "True \<and> False" and "Foo \<or> Bar"

   808 apply(tactic {* orelse_xmp 2 *})

   809 apply(tactic {* orelse_xmp 1 *})

   810 txt {* which results in the goal state

   811 

   812        \begin{minipage}{\textwidth}

   813        @{subgoals [display]} 

   814        \end{minipage}

   815 *}

   816 (*<*)oops(*>*)

   817 

   818 

   819 text {*

   820   Using @{ML FIRST'} we can simplify our @{ML select_tac} from Page~\pageref{tac:selecttac} 

   821   as follows:

   822 *}

   823 

   824 ML{*val select_tac' = FIRST' [rtac @{thm conjI}, rtac @{thm impI}, 

   825                           rtac @{thm notI}, rtac @{thm allI}, K all_tac]*}

   826 

   827 text {*

   828   Since we like to mimic the behaviour of @{ML select_tac} as closely as possible, 

   829   we must include @{ML all_tac} at the end of the list, otherwise the tactic will

   830   fail if no rule applies (we also have to wrap @{ML all_tac} using the 

   831   @{ML K}-combinator, because it does not take a subgoal number as argument). You can 

   832   test the tactic on the same goals:

   833 *}

   834 

   835 lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"

   836 apply(tactic {* select_tac' 4 *})

   837 apply(tactic {* select_tac' 3 *})

   838 apply(tactic {* select_tac' 2 *})

   839 apply(tactic {* select_tac' 1 *})

   840 txt{* \begin{minipage}{\textwidth}

   841       @{subgoals [display]}

   842       \end{minipage} *}

   843 (*<*)oops(*>*)

   844 

   845 text {* 

   846   Since such repeated applications of a tactic to the reverse order of 

   847   \emph{all} subgoals is quite common, there is the tactic combinator 

   848   @{ML ALLGOALS} that simplifies this. Using this combinator you can simply 

   849   write: *}

   850 

   851 lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"

   852 apply(tactic {* ALLGOALS select_tac' *})

   853 txt{* \begin{minipage}{\textwidth}

   854       @{subgoals [display]}

   855       \end{minipage} *}

   856 (*<*)oops(*>*)

   857 

   858 text {*

   859   Remember that we chose to implement @{ML select_tac'} so that it 

   860   always  succeeds. This can be potentially very confusing for the user, 

   861   for example,  in cases where the goal is the form

   862 *}

   863 

   864 lemma shows "E \<Longrightarrow> F"

   865 apply(tactic {* select_tac' 1 *})

   866 txt{* \begin{minipage}{\textwidth}

   867       @{subgoals [display]}

   868       \end{minipage} *}

   869 (*<*)oops(*>*)

   870 

   871 text {*

   872   In this case no rule applies. The problem for the user is that there is little 

   873   chance to see whether or not progress in the proof has been made. By convention

   874   therefore, tactics visible to the user should either change something or fail.

   875   

   876   To comply with this convention, we could simply delete the @{ML "K all_tac"}

   877   from the end of the theorem list. As a result @{ML select_tac'} would only

   878   succeed on goals where it can make progress. But for the sake of argument,

   879   let us suppose that this deletion is \emph{not} an option. In such cases, you can

   880   use the combinator @{ML CHANGED} to make sure the subgoal has been changed

   881   by the tactic. Because now

   882 

   883 *}

   884 

   885 lemma shows "E \<Longrightarrow> F"

   886 apply(tactic {* CHANGED (select_tac' 1) *})(*<*)?(*>*)

   887 txt{* gives the error message:

   888   \begin{isabelle}

   889   @{text "*** empty result sequence -- proof command failed"}\\

   890   @{text "*** At command \"apply\"."}

   891   \end{isabelle} 

   892 *}(*<*)oops(*>*)

   893 

   894 

   895 text {*

   896   We can further extend @{ML select_tac'} so that it not just applies to the topmost

   897   connective, but also to the ones immediately ``underneath'', i.e.~analyse the goal 

   898   completely. For this you can use the tactic combinator @{ML REPEAT}. As an example 

   899   suppose the following tactic

   900 *}

   901 

   902 ML{*val repeat_xmp = REPEAT (CHANGED (select_tac' 1)) *}

   903 

   904 text {* which applied to the proof *}

   905 

   906 lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"

   907 apply(tactic {* repeat_xmp *})

   908 txt{* produces

   909 

   910       \begin{minipage}{\textwidth}

   911       @{subgoals [display]}

   912       \end{minipage} *}

   913 (*<*)oops(*>*)

   914 

   915 text {*

   916   Here it is crucial that @{ML select_tac'} is prefixed with @{ML CHANGED}, 

   917   because otherwise @{ML REPEAT} runs into an infinite loop (it applies the

   918   tactic as long as it succeeds). The function

   919   @{ML REPEAT1} is similar, but runs the tactic at least once (failing if 

   920   this is not possible).

   921 

   922   If you are after the ``primed'' version of @{ML repeat_xmp}, then you 

   923   need to implement it as

   924 *}

   925 

   926 ML{*val repeat_xmp' = REPEAT o CHANGED o select_tac'*}

   927 

   928 text {*

   929   since there are no ``primed'' versions of @{ML REPEAT} and @{ML CHANGED}.

   930 

   931   If you look closely at the goal state above, the tactics @{ML repeat_xmp}

   932   and @{ML repeat_xmp'} are not yet quite what we are after: the problem is

   933   that goals 2 and 3 are not analysed. This is because the tactic

   934   is applied repeatedly only to the first subgoal. To analyse also all

   935   resulting subgoals, you can use the tactic combinator @{ML REPEAT_ALL_NEW}. 

   936   Suppose the tactic

   937 *}

   938 

   939 ML{*val repeat_all_new_xmp = REPEAT_ALL_NEW (CHANGED o select_tac')*}

   940 

   941 text {* 

   942   you see that the following goal

   943 *}

   944 

   945 lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"

   946 apply(tactic {* repeat_all_new_xmp 1 *})

   947 txt{* \begin{minipage}{\textwidth}

   948       @{subgoals [display]}

   949       \end{minipage} *}

   950 (*<*)oops(*>*)

   951 

   952 text {*

   953   is completely analysed according to the theorems we chose to

   954   include in @{ML select_tac'}. 

   955 

   956   Recall that tactics produce a lazy sequence of successor goal states. These

   957   states can be explored using the command \isacommand{back}. For example

   958 

   959 *}

   960 

   961 lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"

   962 apply(tactic {* etac @{thm disjE} 1 *})

   963 txt{* applies the rule to the first assumption yielding the goal state:\smallskip

   964       

   965       \begin{minipage}{\textwidth}

   966       @{subgoals [display]}

   967       \end{minipage}\smallskip 

   968 

   969       After typing

   970   *}

   971 (*<*)

   972 oops

   973 lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"

   974 apply(tactic {* etac @{thm disjE} 1 *})

   975 (*>*)

   976 back

   977 txt{* the rule now applies to the second assumption.\smallskip

   978 

   979       \begin{minipage}{\textwidth}

   980       @{subgoals [display]}

   981       \end{minipage} *}

   982 (*<*)oops(*>*)

   983 

   984 text {*

   985   Sometimes this leads to confusing behaviour of tactics and also has

   986   the potential to explode the search space for tactics.

   987   These problems can be avoided by prefixing the tactic with the tactic 

   988   combinator @{ML DETERM}.

   989 *}

   990 

   991 lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"

   992 apply(tactic {* DETERM (etac @{thm disjE} 1) *})

   993 txt {*\begin{minipage}{\textwidth}

   994       @{subgoals [display]}

   995       \end{minipage} *}

   996 (*<*)oops(*>*)

   997 text {*

   998   This combinator will prune the search space to just the first successful application.

   999   Attempting to apply \isacommand{back} in this goal states gives the

  1000   error message:

  1001 

  1002   \begin{isabelle}

  1003   @{text "*** back: no alternatives"}\\

  1004   @{text "*** At command \"back\"."}

  1005   \end{isabelle}

  1006 

  1007   \begin{readmore}

  1008   Most tactic combinators described in this section are defined in @{ML_file "Pure/tctical.ML"}.

  1009   \end{readmore}

  1010 

  1011 *}

  1012 

  1013 section {* Simplifier Tactics *}

  1014 

  1015 text {*

  1016   A lot of convenience in the reasoning with Isabelle derives from its

  1017   powerful simplifier. The power of simplifier is a strength and a weakness at

  1018   the same time, because you can easily make the simplifier to run into a  loop and its

  1019   behaviour can be difficult to predict. There is also a multitude

  1020   of options that you can configurate to control the behaviour of the simplifier. 

  1021   We describe some of them in this and the next section.

  1022 

  1023   There are the following five main tactics behind 

  1024   the simplifier (in parentheses is their user-level counterpart):

  1025 

  1026   \begin{isabelle}

  1027   \begin{center}

  1028   \begin{tabular}{l@ {\hspace{2cm}}l}

  1029    @{ML simp_tac}            & @{text "(simp (no_asm))"} \\

  1030    @{ML asm_simp_tac}        & @{text "(simp (no_asm_simp))"} \\

  1031    @{ML full_simp_tac}       & @{text "(simp (no_asm_use))"} \\

  1032    @{ML asm_lr_simp_tac}     & @{text "(simp (asm_lr))"} \\

  1033    @{ML asm_full_simp_tac}   & @{text "(simp)"}

  1034   \end{tabular}

  1035   \end{center}

  1036   \end{isabelle}

  1037 

  1038   All of the tactics take a simpset and an interger as argument (the latter as usual 

  1039   to specify  the goal to be analysed). So the proof

  1040 *}

  1041 

  1042 lemma "Suc (1 + 2) < 3 + 2"

  1043 apply(simp)

  1044 done

  1045 

  1046 text {*

  1047   corresponds on the ML-level to the tactic

  1048 *}

  1049 

  1050 lemma "Suc (1 + 2) < 3 + 2"

  1051 apply(tactic {* asm_full_simp_tac @{simpset} 1 *})

  1052 done

  1053 

  1054 text {*

  1055   If the simplifier cannot make any progress, then it leaves the goal unchanged,

  1056   i.e.~does not raise any error message. That means if you use it to unfold a 

  1057   definition for a constant and this constant is not present in the goal state, 

  1058   you can still safely apply the simplifier.

  1059 

  1060   When using the simplifier, the crucial information you have to provide is

  1061   the simpset. If this information is not handled with care, then the

  1062   simplifier can easily run into a loop. Therefore a good rule of thumb is to

  1063   use simpsets that are as minimal as possible. It might be surprising that a

  1064   simpset is more complex than just a simple collection of theorems used as

  1065   simplification rules. One reason for the complexity is that the simplifier

  1066   must be able to rewrite inside terms and should also be able to rewrite

  1067   according to rules that have precoditions.

  1068 

  1069 

  1070   The rewriting inside terms requires congruence rules, which

  1071   are meta-equalities typical of the form

  1072 

  1073   \begin{isabelle}

  1074   \begin{center}

  1075   \mbox{\inferrule{@{text "t\<^isub>1 \<equiv> s\<^isub>1 \<dots> t\<^isub>n \<equiv> s\<^isub>n"}}

  1076                   {@{text "constr t\<^isub>1\<dots>t\<^isub>n \<equiv> constr s\<^isub>1\<dots>s\<^isub>n"}}}

  1077   \end{center}

  1078   \end{isabelle}

  1079 

  1080   with @{text "constr"} being a term-constructor, like @{const "If"} or @{const "Let"}. 

  1081   Every simpset contains only

  1082   one concruence rule for each term-constructor, which however can be

  1083   overwritten. The user can declare lemmas to be congruence rules using the

  1084   attribute @{text "[cong]"}. In HOL, the user usually states these lemmas as

  1085   equations, which are then internally transformed into meta-equations.

  1086 

  1087 

  1088   The rewriting with rules involving preconditions requires what is in

  1089   Isabelle called a subgoaler, a solver and a looper. These can be arbitrary

  1090   tactics that can be installed in a simpset and which are called during

  1091   various stages during simplification. However, simpsets also include

  1092   simprocs, which can produce rewrite rules on demand (see next

  1093   section). Another component are split-rules, which can simplify for example

  1094   the ``then'' and ``else'' branches of if-statements under the corresponding

  1095   precoditions.

  1096 

  1097 

  1098   \begin{readmore}

  1099   For more information about the simplifier see @{ML_file "Pure/meta_simplifier.ML"}

  1100   and @{ML_file "Pure/simplifier.ML"}. The simplifier for HOL is set up in 

  1101   @{ML_file "HOL/Tools/simpdata.ML"}. Generic splitters are implemented in 

  1102   @{ML_file  "Provers/splitter.ML"}.

  1103   \end{readmore}

  1104 

  1105   \begin{readmore}

  1106   FIXME: Find the right place Discrimination nets are implemented

  1107   in @{ML_file "Pure/net.ML"}.

  1108   \end{readmore}

  1109 

  1110   The most common combinators to modify simpsets are

  1111 

  1112   \begin{isabelle}

  1113   \begin{tabular}{ll}

  1114   @{ML addsimps}   & @{ML delsimps}\\

  1115   @{ML addcongs}   & @{ML delcongs}\\

  1116   @{ML addsimprocs} & @{ML delsimprocs}\\

  1117   \end{tabular}

  1118   \end{isabelle}

  1119 

  1120   (FIXME: What about splitters? @{ML addsplits}, @{ML delsplits})

  1121 *}

  1122 

  1123 text_raw {*

  1124 \begin{figure}[t]

  1125 \begin{minipage}{\textwidth}

  1126 \begin{isabelle}*}

  1127 ML{*fun print_ss ctxt ss =

  1128 let

  1129   val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss

  1130 

  1131   fun name_thm (nm, thm) =

  1132       "  " ^ nm ^ ": " ^ (str_of_thm ctxt thm)

  1133   fun name_ctrm (nm, ctrm) =

  1134       "  " ^ nm ^ ": " ^ (str_of_cterms ctxt ctrm)

  1135