--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/Tactical.thy Thu Mar 19 13:28:16 2009 +0100
@@ -0,0 +1,2121 @@
+theory Tactical
+imports Base FirstSteps
+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 \isacommand{apply}-style
+ reasoning at the user-level, where goals are modified in a sequence of proof
+ steps until all of them are solved. However, there are also more structured
+ operations available on the ML-level that help with the handling of
+ variables and assumptions.
+
+*}
+
+section {* Basics of Reasoning with Tactics*}
+
+text {*
+ To see how tactics work, let us first transcribe a simple \isacommand{apply}-style proof
+ into ML. Suppose 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}
+ (that is @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"} in the proof at hand) under the
+ assumptions @{text As} (happens to be empty) 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} in the code above correspond to
+ @{text erule}, @{text rule} and @{text assumption}, respectively.
+ The operator @{ML THEN} strings the 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"}. 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, and Chapter 3 in the Isabelle/Isar Implementation Manual.
+ \end{readmore}
+
+ Note that in the code above we use antiquotations for referencing the theorems. Many theorems
+ also have ML-bindings with the same name. Therefore, we could also just have
+ written @{ML "etac disjE 1"}, or in case where there are no ML-binding obtain
+ the theorem dynamically using the function @{ML thm}; for example
+ \mbox{@{ML "etac (thm \"disjE\") 1"}}. Both ways however are 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, you will often find it
+ 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 {*
+ By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} you can call from the
+ user-level of Isabelle the tactic @{ML foo_tac} or
+ any other function that returns a tactic.
+
+ The tactic @{ML foo_tac} is just a sequence of simple tactics stringed
+ together by @{ML THEN}. As can be seen, each simple tactic in @{ML foo_tac}
+ has a hard-coded number that stands for the subgoal analysed by the
+ tactic (@{text "1"} stands for the first, or top-most, subgoal). This hard-coding
+ of goals is sometimes wanted, but usually it is not. To avoid the explicit numbering,
+ you can write\label{tac:footacprime}
+*}
+
+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 you can first discharge the second subgoal, and
+ subsequently 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 {*
+ This kind of addressing is more difficult to achieve when the goal is
+ hard-coded inside the tactic. For most operators that combine tactics
+ (@{ML THEN} is only one such operator) a ``primed'' version exists.
+
+ The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for
+ analysing goals being only of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not
+ of this form, then these tactics return the error message:
+
+ \begin{isabelle}
+ @{text "*** empty result sequence -- proof command failed"}\\
+ @{text "*** At command \"apply\"."}
+ \end{isabelle}
+
+ This means they failed. The reason for this error message is that tactics
+ are functions mapping a goal state to a (lazy) sequence of successor states.
+ Hence the type of a tactic is:
+*}
+
+ML{*type tactic = thm -> thm Seq.seq*}
+
+text {*
+ By convention, if a tactic fails, then it should return the empty sequence.
+ Therefore, if you write your own tactics, they should not raise exceptions
+ willy-nilly; only in very grave failure situations should a tactic raise the
+ exception @{text THM}.
+
+ The simplest tactics are @{ML no_tac} and @{ML all_tac}. The first returns
+ the empty sequence and is defined as
+*}
+
+ML{*fun no_tac thm = Seq.empty*}
+
+text {*
+ which means @{ML no_tac} always fails. The second returns the given theorem wrapped
+ in a single member sequence; it is defined as
+*}
+
+ML{*fun all_tac thm = Seq.single thm*}
+
+text {*
+ which means @{ML all_tac} always succeeds, but also does not make any progress
+ with the proof.
+
+ The lazy list of possible successor goal states shows through at the user-level
+ of Isabelle when using the command \isacommand{back}. For instance in the
+ following proof there are two possibilities for how to apply
+ @{ML foo_tac'}: either using the first assumption or the second.
+*}
+
+lemma "\<lbrakk>P \<or> Q; P \<or> Q\<rbrakk> \<Longrightarrow> Q \<or> P"
+apply(tactic {* foo_tac' 1 *})
+back
+done
+
+
+text {*
+ By using \isacommand{back}, we construct the proof that uses the
+ second assumption. While in the proof above, it does not really matter which
+ assumption is used, in more interesting cases provability might depend
+ on exploring different possibilities.
+
+ \begin{readmore}
+ See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy
+ sequences. In day-to-day Isabelle programming, however, one rarely
+ constructs sequences explicitly, but uses the predefined tactics and
+ tactic combinators instead.
+ \end{readmore}
+
+ It might be surprising that tactics, which transform
+ one goal state to the next, are functions from theorems to theorem
+ (sequences). The surprise resolves by knowing that every
+ goal state is indeed a theorem. To shed more light on this,
+ let us modify the code of @{ML all_tac} to obtain the following
+ tactic
+*}
+
+ML{*fun my_print_tac ctxt thm =
+let
+ val _ = warning (str_of_thm ctxt thm)
+in
+ Seq.single thm
+end*}
+
+text_raw {*
+ \begin{figure}[p]
+ \begin{boxedminipage}{\textwidth}
+ \begin{isabelle}
+*}
+lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"
+apply(tactic {* my_print_tac @{context} *})
+
+txt{* \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}\medskip
+
+ \begin{minipage}{\textwidth}
+ \small\colorbox{gray!20}{
+ \begin{tabular}{@ {}l@ {}}
+ internal goal state:\\
+ @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+ \end{tabular}}
+ \end{minipage}\medskip
+*}
+
+apply(rule conjI)
+apply(tactic {* my_print_tac @{context} *})
+
+txt{* \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}\medskip
+
+ \begin{minipage}{\textwidth}
+ \small\colorbox{gray!20}{
+ \begin{tabular}{@ {}l@ {}}
+ internal goal state:\\
+ @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+ \end{tabular}}
+ \end{minipage}\medskip
+*}
+
+apply(assumption)
+apply(tactic {* my_print_tac @{context} *})
+
+txt{* \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}\medskip
+
+ \begin{minipage}{\textwidth}
+ \small\colorbox{gray!20}{
+ \begin{tabular}{@ {}l@ {}}
+ internal goal state:\\
+ @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+ \end{tabular}}
+ \end{minipage}\medskip
+*}
+
+apply(assumption)
+apply(tactic {* my_print_tac @{context} *})
+
+txt{* \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}\medskip
+
+ \begin{minipage}{\textwidth}
+ \small\colorbox{gray!20}{
+ \begin{tabular}{@ {}l@ {}}
+ internal goal state:\\
+ @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}
+ \end{tabular}}
+ \end{minipage}\medskip
+ *}
+done
+text_raw {*
+ \end{isabelle}
+ \end{boxedminipage}
+ \caption{The figure shows a proof where each intermediate goal state is
+ printed by the Isabelle system and by @{ML my_print_tac}. The latter shows
+ the goal state as represented internally (highlighted boxes). This
+ tactic shows that every goal state in Isabelle is represented by a theorem:
+ when you start the proof of \mbox{@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}} the theorem is
+ @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when you finish the proof the
+ theorem is @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}.\label{fig:goalstates}}
+ \end{figure}
+*}
+
+
+text {*
+ which prints out the given theorem (using the string-function defined in
+ Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. With this
+ tactic we are in the position to inspect every goal state in a
+ proof. Consider now the proof in Figure~\ref{fig:goalstates}: as can be seen,
+ internally every goal state 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 subgoals. So after setting up the lemma, the goal state is always of the
+ form @{text "C \<Longrightarrow> (C)"}; when the proof is finished we are left with @{text
+ "(C)"}. Since the goal @{term C} can potentially be an implication, there is
+ a ``protector'' wrapped around it (in from of an outermost constant @{text
+ "Const (\"prop\", bool \<Rightarrow> bool)"}; however this constant
+ is invisible in the figure). This wrapper prevents that premises of @{text C} are
+ mis-interpreted as open subgoals. 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. If you use the predefined tactics, which we describe in the next
+ section, this will always be the case.
+
+ \begin{readmore}
+ For more information about the internals of goals see \isccite{sec:tactical-goals}.
+ \end{readmore}
+
+*}
+
+section {* Simple Tactics *}
+
+text {*
+ Let us start with explaining the simple tactic @{ML print_tac}, which is quite useful
+ for low-level debugging of tactics. It just prints out a message and the current
+ goal state. Unlike @{ML my_print_tac} shown earlier, it prints the goal state
+ as the user would see it. For example, processing the proof
+*}
+
+lemma shows "False \<Longrightarrow> True"
+apply(tactic {* print_tac "foo message" *})
+txt{*gives:\medskip
+
+ \begin{minipage}{\textwidth}\small
+ @{text "foo message"}\\[3mm]
+ @{prop "False \<Longrightarrow> True"}\\
+ @{text " 1. False \<Longrightarrow> True"}\\
+ \end{minipage}
+ *}
+(*<*)oops(*>*)
+
+text {*
+ Another simple tactic is the function @{ML atac}, which, as shown in the previous
+ section, corresponds to the assumption command.
+*}
+
+lemma shows "P \<Longrightarrow> P"
+apply(tactic {* atac 1 *})
+txt{*\begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}*}
+(*<*)oops(*>*)
+
+text {*
+ Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond
+ to @{text rule}, @{text drule}, @{text erule} and @{text frule},
+ respectively. Each of them takes a theorem as argument and attempts to
+ apply it to a goal. Below are three self-explanatory examples.
+*}
+
+lemma shows "P \<and> Q"
+apply(tactic {* rtac @{thm conjI} 1 *})
+txt{*\begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}*}
+(*<*)oops(*>*)
+
+lemma shows "P \<and> Q \<Longrightarrow> False"
+apply(tactic {* etac @{thm conjE} 1 *})
+txt{*\begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}*}
+(*<*)oops(*>*)
+
+lemma shows "False \<and> True \<Longrightarrow> False"
+apply(tactic {* dtac @{thm conjunct2} 1 *})
+txt{*\begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}*}
+(*<*)oops(*>*)
+
+text {*
+ Note the number in each tactic call. Also as mentioned in the previous section, most
+ basic tactics take such a number as argument: this argument addresses the subgoal
+ the tacics are analysing. In the proof below, we first split up the conjunction in
+ the second subgoal by focusing on this subgoal first.
+*}
+
+lemma shows "Foo" and "P \<and> Q"
+apply(tactic {* rtac @{thm conjI} 2 *})
+txt {*\begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}*}
+(*<*)oops(*>*)
+
+text {*
+ The function @{ML resolve_tac} is similar to @{ML rtac}, except that it
+ expects a list of theorems as arguments. From this list it will apply the
+ first applicable theorem (later theorems that are also applicable can be
+ explored via the lazy sequences mechanism). Given the code
+*}
+
+ML{*val resolve_tac_xmp = resolve_tac [@{thm impI}, @{thm conjI}]*}
+
+text {*
+ an example for @{ML resolve_tac} is the following proof where first an outermost
+ implication is analysed and then an outermost conjunction.
+*}
+
+lemma shows "C \<longrightarrow> (A \<and> B)" and "(A \<longrightarrow> B) \<and> C"
+apply(tactic {* resolve_tac_xmp 1 *})
+apply(tactic {* resolve_tac_xmp 2 *})
+txt{*\begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}*}
+(*<*)oops(*>*)
+
+text {*
+ Similar versions taking a list of theorems exist for the tactics
+ @{ML dtac} (@{ML dresolve_tac}), @{ML etac} (@{ML eresolve_tac}) and so on.
+
+
+ Another simple tactic is @{ML cut_facts_tac}. It inserts a list of theorems
+ into the assumptions of the current goal state. For example
+*}
+
+lemma shows "True \<noteq> False"
+apply(tactic {* cut_facts_tac [@{thm True_def}, @{thm False_def}] 1 *})
+txt{*produces the goal state\medskip
+
+ \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}*}
+(*<*)oops(*>*)
+
+text {*
+ Since rules are applied using higher-order unification, an automatic proof
+ procedure might become too fragile, if it just applies inference rules as
+ shown above. The reason is that a number of rules introduce meta-variables
+ into the goal state. Consider for example the proof
+*}
+
+lemma shows "\<forall>x\<in>A. P x \<Longrightarrow> Q x"
+apply(tactic {* dtac @{thm bspec} 1 *})
+txt{*\begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}*}
+(*<*)oops(*>*)
+
+text {*
+ where the application of rule @{text bspec} generates two subgoals involving the
+ meta-variable @{text "?x"}. Now, if you are not careful, tactics
+ applied to the first subgoal might instantiate this meta-variable in such a
+ way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"}
+ should be, then this situation can be avoided by introducing a more
+ constraint version of the @{text bspec}-rule. Such constraints can be given by
+ pre-instantiating theorems with other theorems. One function to do this is
+ @{ML RS}
+
+ @{ML_response_fake [display,gray]
+ "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
+
+ which in the example instantiates the first premise of the @{text conjI}-rule
+ with the rule @{text disjI1}. If the instantiation is impossible, as in the
+ case of
+
+ @{ML_response_fake_both [display,gray]
+ "@{thm conjI} RS @{thm mp}"
+"*** Exception- THM (\"RSN: no unifiers\", 1,
+[\"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\", \"\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\"]) raised"}
+
+ then the function raises an exception. The function @{ML RSN} is similar to @{ML RS}, but
+ takes an additional number as argument that makes explicit which premise
+ should be instantiated.
+
+ To improve readability of the theorems we produce below, we shall use the
+ function @{ML no_vars} from Section~\ref{sec:printing}, which transforms
+ schematic variables into free ones. Using this function for the first @{ML
+ RS}-expression above produces the more readable result:
+
+ @{ML_response_fake [display,gray]
+ "no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> Q"}
+
+ If you want to instantiate more than one premise of a theorem, you can use
+ the function @{ML MRS}:
+
+ @{ML_response_fake [display,gray]
+ "no_vars @{context} ([@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI})"
+ "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> (Pa \<or> Q)"}
+
+ If you need to instantiate lists of theorems, you can use the
+ functions @{ML RL} and @{ML MRL}. For example in the code below,
+ every theorem in the second list is instantiated with every
+ theorem in the first.
+
+ @{ML_response_fake [display,gray]
+ "[@{thm impI}, @{thm disjI2}] RL [@{thm conjI}, @{thm disjI1}]"
+"[\<lbrakk>P \<Longrightarrow> Q; Qa\<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) \<and> Qa,
+ \<lbrakk>Q; Qa\<rbrakk> \<Longrightarrow> (P \<or> Q) \<and> Qa,
+ (P \<Longrightarrow> Q) \<Longrightarrow> (P \<longrightarrow> Q) \<or> Qa,
+ Q \<Longrightarrow> (P \<or> Q) \<or> Qa]"}
+
+ \begin{readmore}
+ The combinators for instantiating theorems are defined in @{ML_file "Pure/drule.ML"}.
+ \end{readmore}
+
+ Often proofs on the ML-level involve elaborate operations on assumptions and
+ @{text "\<And>"}-quantified variables. To do such operations using the basic tactics
+ shown so far is very unwieldy and brittle. Some convenience and
+ safety is provided by the tactic @{ML SUBPROOF}. This tactic fixes the parameters
+ and binds the various components of a goal state to a record.
+ To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which
+ takes a record and just prints out the content of this record (using the
+ string transformation functions from in Section~\ref{sec:printing}). Consider
+ now the proof:
+*}
+
+text_raw{*
+\begin{figure}[t]
+\begin{minipage}{\textwidth}
+\begin{isabelle}
+*}
+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 ("assumptions: " ^ str_of_asms);
+ warning ("conclusion: " ^ str_of_concl);
+ warning ("premises: " ^ str_of_prems))
+in
+ no_tac
+end*}
+text_raw{*
+\end{isabelle}
+\end{minipage}
+\caption{A function that prints out the various parameters provided by the tactic
+ @{ML SUBPROOF}. It uses the functions defined in Section~\ref{sec:printing} for
+ extracting strings from @{ML_type cterm}s and @{ML_type thm}s.\label{fig:sptac}}
+\end{figure}
+*}
+
+
+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 {*
+ The tactic produces the following printout:
+
+ \begin{quote}\small
+ \begin{tabular}{ll}
+ params: & @{term x}, @{term y}\\
+ schematics: & @{term z}\\
+ assumptions: & @{term "A x y"}\\
+ conclusion: & @{term "B y x \<longrightarrow> C (z y) x"}\\
+ premises: & @{term "A x y"}
+ \end{tabular}
+ \end{quote}
+
+ Notice in the actual output the brown colour of the variables @{term x} and
+ @{term y}. Although they are parameters in the original goal, they are fixed inside
+ the subproof. By convention these fixed variables are printed in brown colour.
+ Similarly the schematic variable @{term z}. The assumption, or premise,
+ @{prop "A x y"} is bound as @{ML_type cterm} to the record-variable
+ @{text asms}, but also as @{ML_type thm} to @{text prems}.
+
+ Notice also that we had to append @{text [quotes] "?"} to the
+ \isacommand{apply}-command. The reason is that @{ML SUBPROOF} normally
+ expects that the subgoal is solved completely. Since in the function @{ML
+ sp_tac} we returned the tactic @{ML no_tac}, the subproof obviously
+ fails. The question-mark allows us to recover from this failure in a
+ graceful manner so that the warning messages are not overwritten by an
+ ``empty sequence'' error message.
+
+ If we continue the proof script by applying the @{text impI}-rule
+*}
+
+apply(rule impI)
+apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
+
+txt {*
+ then the tactic prints out:
+
+ \begin{quote}\small
+ \begin{tabular}{ll}
+ params: & @{term x}, @{term y}\\
+ schematics: & @{term z}\\
+ assumptions: & @{term "A x y"}, @{term "B y x"}\\
+ conclusion: & @{term "C (z y) x"}\\
+ premises: & @{term "A x y"}, @{term "B y x"}
+ \end{tabular}
+ \end{quote}
+*}
+(*<*)oops(*>*)
+
+text {*
+ Now also @{term "B y x"} is an assumption bound to @{text asms} and @{text prems}.
+
+ One convenience of @{ML SUBPROOF} is that we can apply the assumptions
+ using the usual tactics, because the parameter @{text prems}
+ contains them as theorems. With this you can easily
+ implement a tactic that behaves almost like @{ML atac}:
+*}
+
+ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*}
+
+text {*
+ If you apply @{ML atac'} to the next lemma
+*}
+
+lemma shows "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
+apply(tactic {* atac' @{context} 1 *})
+txt{* it will produce
+ @{subgoals [display]} *}
+(*<*)oops(*>*)
+
+text {*
+ The restriction in this tactic which is not present in @{ML atac} is
+ that it cannot instantiate any
+ schematic variable. This might be seen as a defect, but it is actually
+ an advantage in the situations for which @{ML SUBPROOF} was designed:
+ the reason is that, as mentioned before, instantiation of schematic variables can affect
+ several goals and can render them unprovable. @{ML SUBPROOF} is meant
+ to avoid this.
+
+ Notice that @{ML atac'} inside @{ML SUBPROOF} calls @{ML resolve_tac} with
+ the subgoal number @{text "1"} and also the outer call to @{ML SUBPROOF} in
+ the \isacommand{apply}-step uses @{text "1"}. This is another advantage
+ of @{ML SUBPROOF}: the addressing inside it is completely
+ local to the tactic inside the subproof. It is therefore possible to also apply
+ @{ML atac'} to the second goal by just writing:
+*}
+
+lemma shows "True" and "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
+apply(tactic {* atac' @{context} 2 *})
+apply(rule TrueI)
+done
+
+
+text {*
+ \begin{readmore}
+ The function @{ML SUBPROOF} is defined in @{ML_file "Pure/subgoal.ML"} and
+ also described in \isccite{sec:results}.
+ \end{readmore}
+
+ Similar but less powerful functions than @{ML SUBPROOF} are @{ML SUBGOAL}
+ and @{ML CSUBGOAL}. They allow you to inspect a given subgoal (the former
+ presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type
+ cterm}). With this you can implement a tactic that applies a rule according
+ to the topmost logic connective in the subgoal (to illustrate this we only
+ analyse a few connectives). The code of the tactic is as
+ follows.\label{tac:selecttac}
+
+*}
+
+ML %linenosgray{*fun select_tac (t, i) =
+ case t of
+ @{term "Trueprop"} $ t' => select_tac (t', i)
+ | @{term "op \<Longrightarrow>"} $ _ $ t' => select_tac (t', i)
+ | @{term "op \<and>"} $ _ $ _ => rtac @{thm conjI} i
+ | @{term "op \<longrightarrow>"} $ _ $ _ => rtac @{thm impI} i
+ | @{term "Not"} $ _ => rtac @{thm notI} i
+ | Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i
+ | _ => all_tac*}
+
+text {*
+ The input of the function is a term representing the subgoal and a number
+ specifying the subgoal of interest. In Line 3 you need to descend under the
+ outermost @{term "Trueprop"} in order to get to the connective you like to
+ analyse. Otherwise goals like @{prop "A \<and> B"} are not properly
+ analysed. Similarly with meta-implications in the next line. While for the
+ first five patterns we can use the @{text "@term"}-antiquotation to
+ construct the patterns, the pattern in Line 8 cannot be constructed in this
+ way. The reason is that an antiquotation would fix the type of the
+ quantified variable. So you really have to construct the pattern using the
+ basic term-constructors. This is not necessary in other cases, because their
+ type is always fixed to function types involving only the type @{typ
+ bool}. (See Section \ref{sec:terms_types_manually} about constructing terms
+ manually.) For the catch-all pattern, we chose to just return @{ML all_tac}.
+ Consequently, @{ML select_tac} never fails.
+
+
+ Let us now see how to apply this tactic. Consider the four goals:
+*}
+
+
+lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
+apply(tactic {* SUBGOAL select_tac 4 *})
+apply(tactic {* SUBGOAL select_tac 3 *})
+apply(tactic {* SUBGOAL select_tac 2 *})
+apply(tactic {* SUBGOAL select_tac 1 *})
+txt{* \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage} *}
+(*<*)oops(*>*)
+
+text {*
+ where in all but the last the tactic applied an introduction rule.
+ Note that we applied the tactic to the goals in ``reverse'' order.
+ This is a trick in order to be independent from the subgoals that are
+ produced by the rule. If we had applied it in the other order
+*}
+
+lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
+apply(tactic {* SUBGOAL select_tac 1 *})
+apply(tactic {* SUBGOAL select_tac 3 *})
+apply(tactic {* SUBGOAL select_tac 4 *})
+apply(tactic {* SUBGOAL select_tac 5 *})
+(*<*)oops(*>*)
+
+text {*
+ then we have to be careful to not apply the tactic to the two subgoals produced by
+ the first goal. To do this can result in quite messy code. In contrast,
+ the ``reverse application'' is easy to implement.
+
+ Of course, this example is
+ contrived: there are much simpler methods available in Isabelle for
+ implementing a proof procedure analysing a goal according to its topmost
+ connective. These simpler methods use tactic combinators, which we will
+ explain in the next section.
+
+*}
+
+section {* Tactic Combinators *}
+
+text {*
+ The purpose of tactic combinators is to build compound tactics out of
+ smaller tactics. In the previous section we already used @{ML THEN}, which
+ just strings together two tactics in a sequence. For example:
+*}
+
+lemma shows "(Foo \<and> Bar) \<and> False"
+apply(tactic {* rtac @{thm conjI} 1 THEN rtac @{thm conjI} 1 *})
+txt {* \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage} *}
+(*<*)oops(*>*)
+
+text {*
+ If you want to avoid the hard-coded subgoal addressing, then you can use
+ the ``primed'' version of @{ML THEN}. For example:
+*}
+
+lemma shows "(Foo \<and> Bar) \<and> False"
+apply(tactic {* (rtac @{thm conjI} THEN' rtac @{thm conjI}) 1 *})
+txt {* \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage} *}
+(*<*)oops(*>*)
+
+text {*
+ Here you only have to specify the subgoal of interest only once and
+ it is consistently applied to the component tactics.
+ For most tactic combinators such a ``primed'' version exists and
+ in what follows we will usually prefer it over the ``unprimed'' one.
+
+ If there is a list of tactics that should all be tried out in
+ sequence, you can use the combinator @{ML EVERY'}. For example
+ the function @{ML foo_tac'} from page~\pageref{tac:footacprime} can also
+ be written as:
+*}
+
+ML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2},
+ atac, rtac @{thm disjI1}, atac]*}
+
+text {*
+ There is even another way of implementing this tactic: in automatic proof
+ procedures (in contrast to tactics that might be called by the user) there
+ are often long lists of tactics that are applied to the first
+ subgoal. Instead of writing the code above and then calling @{ML "foo_tac'' 1"},
+ you can also just write
+*}
+
+ML{*val foo_tac1 = EVERY1 [etac @{thm disjE}, rtac @{thm disjI2},
+ atac, rtac @{thm disjI1}, atac]*}
+
+text {*
+ and call @{ML foo_tac1}.
+
+ With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML EVERY1} it must be
+ guaranteed that all component tactics successfully apply; otherwise the
+ whole tactic will fail. If you rather want to try out a number of tactics,
+ then you can use the combinator @{ML ORELSE'} for two tactics, and @{ML
+ FIRST'} (or @{ML FIRST1}) for a list of tactics. For example, the tactic
+
+*}
+
+ML{*val orelse_xmp = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*}
+
+text {*
+ will first try out whether rule @{text disjI} applies and after that
+ @{text conjI}. To see this consider the proof
+*}
+
+lemma shows "True \<and> False" and "Foo \<or> Bar"
+apply(tactic {* orelse_xmp 2 *})
+apply(tactic {* orelse_xmp 1 *})
+txt {* which results in the goal state
+
+ \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}
+*}
+(*<*)oops(*>*)
+
+
+text {*
+ Using @{ML FIRST'} we can simplify our @{ML select_tac} from Page~\pageref{tac:selecttac}
+ as follows:
+*}
+
+ML{*val select_tac' = FIRST' [rtac @{thm conjI}, rtac @{thm impI},
+ rtac @{thm notI}, rtac @{thm allI}, K all_tac]*}
+
+text {*
+ Since we like to mimic the behaviour of @{ML select_tac} as closely as possible,
+ we must include @{ML all_tac} at the end of the list, otherwise the tactic will
+ fail if no rule applies (we also have to wrap @{ML all_tac} using the
+ @{ML K}-combinator, because it does not take a subgoal number as argument). You can
+ test the tactic on the same goals:
+*}
+
+lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
+apply(tactic {* select_tac' 4 *})
+apply(tactic {* select_tac' 3 *})
+apply(tactic {* select_tac' 2 *})
+apply(tactic {* select_tac' 1 *})
+txt{* \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage} *}
+(*<*)oops(*>*)
+
+text {*
+ Since such repeated applications of a tactic to the reverse order of
+ \emph{all} subgoals is quite common, there is the tactic combinator
+ @{ML ALLGOALS} that simplifies this. Using this combinator you can simply
+ write: *}
+
+lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
+apply(tactic {* ALLGOALS select_tac' *})
+txt{* \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage} *}
+(*<*)oops(*>*)
+
+text {*
+ Remember that we chose to implement @{ML select_tac'} so that it
+ always succeeds. This can be potentially very confusing for the user,
+ for example, in cases where the goal is the form
+*}
+
+lemma shows "E \<Longrightarrow> F"
+apply(tactic {* select_tac' 1 *})
+txt{* \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage} *}
+(*<*)oops(*>*)
+
+text {*
+ In this case no rule applies. The problem for the user is that there is little
+ chance to see whether or not progress in the proof has been made. By convention
+ therefore, tactics visible to the user should either change something or fail.
+
+ To comply with this convention, we could simply delete the @{ML "K all_tac"}
+ from the end of the theorem list. As a result @{ML select_tac'} would only
+ succeed on goals where it can make progress. But for the sake of argument,
+ let us suppose that this deletion is \emph{not} an option. In such cases, you can
+ use the combinator @{ML CHANGED} to make sure the subgoal has been changed
+ by the tactic. Because now
+
+*}
+
+lemma shows "E \<Longrightarrow> F"
+apply(tactic {* CHANGED (select_tac' 1) *})(*<*)?(*>*)
+txt{* gives the error message:
+ \begin{isabelle}
+ @{text "*** empty result sequence -- proof command failed"}\\
+ @{text "*** At command \"apply\"."}
+ \end{isabelle}
+*}(*<*)oops(*>*)
+
+
+text {*
+ We can further extend @{ML select_tac'} so that it not just applies to the topmost
+ connective, but also to the ones immediately ``underneath'', i.e.~analyse the goal
+ completely. For this you can use the tactic combinator @{ML REPEAT}. As an example
+ suppose the following tactic
+*}
+
+ML{*val repeat_xmp = REPEAT (CHANGED (select_tac' 1)) *}
+
+text {* which applied to the proof *}
+
+lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
+apply(tactic {* repeat_xmp *})
+txt{* produces
+
+ \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage} *}
+(*<*)oops(*>*)
+
+text {*
+ Here it is crucial that @{ML select_tac'} is prefixed with @{ML CHANGED},
+ because otherwise @{ML REPEAT} runs into an infinite loop (it applies the
+ tactic as long as it succeeds). The function
+ @{ML REPEAT1} is similar, but runs the tactic at least once (failing if
+ this is not possible).
+
+ If you are after the ``primed'' version of @{ML repeat_xmp}, then you
+ need to implement it as
+*}
+
+ML{*val repeat_xmp' = REPEAT o CHANGED o select_tac'*}
+
+text {*
+ since there are no ``primed'' versions of @{ML REPEAT} and @{ML CHANGED}.
+
+ If you look closely at the goal state above, the tactics @{ML repeat_xmp}
+ and @{ML repeat_xmp'} are not yet quite what we are after: the problem is
+ that goals 2 and 3 are not analysed. This is because the tactic
+ is applied repeatedly only to the first subgoal. To analyse also all
+ resulting subgoals, you can use the tactic combinator @{ML REPEAT_ALL_NEW}.
+ Suppose the tactic
+*}
+
+ML{*val repeat_all_new_xmp = REPEAT_ALL_NEW (CHANGED o select_tac')*}
+
+text {*
+ you see that the following goal
+*}
+
+lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
+apply(tactic {* repeat_all_new_xmp 1 *})
+txt{* \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage} *}
+(*<*)oops(*>*)
+
+text {*
+ is completely analysed according to the theorems we chose to
+ include in @{ML select_tac'}.
+
+ Recall that tactics produce a lazy sequence of successor goal states. These
+ states can be explored using the command \isacommand{back}. For example
+
+*}
+
+lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
+apply(tactic {* etac @{thm disjE} 1 *})
+txt{* applies the rule to the first assumption yielding the goal state:\smallskip
+
+ \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}\smallskip
+
+ After typing
+ *}
+(*<*)
+oops
+lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
+apply(tactic {* etac @{thm disjE} 1 *})
+(*>*)
+back
+txt{* the rule now applies to the second assumption.\smallskip
+
+ \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage} *}
+(*<*)oops(*>*)
+
+text {*
+ Sometimes this leads to confusing behaviour of tactics and also has
+ the potential to explode the search space for tactics.
+ These problems can be avoided by prefixing the tactic with the tactic
+ combinator @{ML DETERM}.
+*}
+
+lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
+apply(tactic {* DETERM (etac @{thm disjE} 1) *})
+txt {*\begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage} *}
+(*<*)oops(*>*)
+text {*
+ This combinator will prune the search space to just the first successful application.
+ Attempting to apply \isacommand{back} in this goal states gives the
+ error message:
+
+ \begin{isabelle}
+ @{text "*** back: no alternatives"}\\
+ @{text "*** At command \"back\"."}
+ \end{isabelle}
+
+ \begin{readmore}
+ Most tactic combinators described in this section are defined in @{ML_file "Pure/tctical.ML"}.
+ \end{readmore}
+
+*}
+
+section {* Simplifier Tactics *}
+
+text {*
+ A lot of convenience in the reasoning with Isabelle derives from its
+ powerful simplifier. The power of simplifier is a strength and a weakness at
+ the same time, because you can easily make the simplifier to run into a loop and its
+ behaviour can be difficult to predict. There is also a multitude
+ of options that you can configurate to control the behaviour of the simplifier.
+ We describe some of them in this and the next section.
+
+ There are the following five main tactics behind
+ the simplifier (in parentheses is their user-level counterpart):
+
+ \begin{isabelle}
+ \begin{center}
+ \begin{tabular}{l@ {\hspace{2cm}}l}
+ @{ML simp_tac} & @{text "(simp (no_asm))"} \\
+ @{ML asm_simp_tac} & @{text "(simp (no_asm_simp))"} \\
+ @{ML full_simp_tac} & @{text "(simp (no_asm_use))"} \\
+ @{ML asm_lr_simp_tac} & @{text "(simp (asm_lr))"} \\
+ @{ML asm_full_simp_tac} & @{text "(simp)"}
+ \end{tabular}
+ \end{center}
+ \end{isabelle}
+
+ All of the tactics take a simpset and an interger as argument (the latter as usual
+ to specify the goal to be analysed). So the proof
+*}
+
+lemma "Suc (1 + 2) < 3 + 2"
+apply(simp)
+done
+
+text {*
+ corresponds on the ML-level to the tactic
+*}
+
+lemma "Suc (1 + 2) < 3 + 2"
+apply(tactic {* asm_full_simp_tac @{simpset} 1 *})
+done
+
+text {*
+ If the simplifier cannot make any progress, then it leaves the goal unchanged,
+ i.e.~does not raise any error message. That means if you use it to unfold a
+ definition for a constant and this constant is not present in the goal state,
+ you can still safely apply the simplifier.
+
+ When using the simplifier, the crucial information you have to provide is
+ the simpset. If this information is not handled with care, then the
+ simplifier can easily run into a loop. Therefore a good rule of thumb is to
+ use simpsets that are as minimal as possible. It might be surprising that a
+ simpset is more complex than just a simple collection of theorems used as
+ simplification rules. One reason for the complexity is that the simplifier
+ must be able to rewrite inside terms and should also be able to rewrite
+ according to rules that have precoditions.
+
+
+ The rewriting inside terms requires congruence rules, which
+ are meta-equalities typical of the form
+
+ \begin{isabelle}
+ \begin{center}
+ \mbox{\inferrule{@{text "t\<^isub>1 \<equiv> s\<^isub>1 \<dots> t\<^isub>n \<equiv> s\<^isub>n"}}
+ {@{text "constr t\<^isub>1\<dots>t\<^isub>n \<equiv> constr s\<^isub>1\<dots>s\<^isub>n"}}}
+ \end{center}
+ \end{isabelle}
+
+ with @{text "constr"} being a term-constructor, like @{const "If"} or @{const "Let"}.
+ Every simpset contains only
+ one concruence rule for each term-constructor, which however can be
+ overwritten. The user can declare lemmas to be congruence rules using the
+ attribute @{text "[cong]"}. In HOL, the user usually states these lemmas as
+ equations, which are then internally transformed into meta-equations.
+
+
+ The rewriting with rules involving preconditions requires what is in
+ Isabelle called a subgoaler, a solver and a looper. These can be arbitrary
+ tactics that can be installed in a simpset and which are called during
+ various stages during simplification. However, simpsets also include
+ simprocs, which can produce rewrite rules on demand (see next
+ section). Another component are split-rules, which can simplify for example
+ the ``then'' and ``else'' branches of if-statements under the corresponding
+ precoditions.
+
+
+ \begin{readmore}
+ For more information about the simplifier see @{ML_file "Pure/meta_simplifier.ML"}
+ and @{ML_file "Pure/simplifier.ML"}. The simplifier for HOL is set up in
+ @{ML_file "HOL/Tools/simpdata.ML"}. Generic splitters are implemented in
+ @{ML_file "Provers/splitter.ML"}.
+ \end{readmore}
+
+ \begin{readmore}
+ FIXME: Find the right place Discrimination nets are implemented
+ in @{ML_file "Pure/net.ML"}.
+ \end{readmore}
+
+ The most common combinators to modify simpsets are
+
+ \begin{isabelle}
+ \begin{tabular}{ll}
+ @{ML addsimps} & @{ML delsimps}\\
+ @{ML addcongs} & @{ML delcongs}\\
+ @{ML addsimprocs} & @{ML delsimprocs}\\
+ \end{tabular}
+ \end{isabelle}
+
+ (FIXME: What about splitters? @{ML addsplits}, @{ML delsplits})
+*}
+
+text_raw {*
+\begin{figure}[t]
+\begin{minipage}{\textwidth}
+\begin{isabelle}*}
+ML{*fun print_ss ctxt ss =
+let
+ val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss
+
+ fun name_thm (nm, thm) =
+ " " ^ nm ^ ": " ^ (str_of_thm ctxt thm)
+ fun name_ctrm (nm, ctrm) =
+ " " ^ nm ^ ": " ^ (str_of_cterms ctxt ctrm)
+
+ val s1 = ["Simplification rules:"]
+ val s2 = map name_thm simps
+ val s3 = ["Congruences rules:"]
+ val s4 = map name_thm congs
+ val s5 = ["Simproc patterns:"]
+ val s6 = map name_ctrm procs
+in
+ (s1 @ s2 @ s3 @ s4 @ s5 @ s6)
+ |> separate "\n"
+ |> implode
+ |> warning
+end*}
+text_raw {*
+\end{isabelle}
+\end{minipage}
+\caption{The function @{ML MetaSimplifier.dest_ss} returns a record containing
+ all printable information stored in a simpset. We are here only interested in the
+ simplifcation rules, congruence rules and simprocs.\label{fig:printss}}
+\end{figure} *}
+
+text {*
+ To see how they work, consider the function in Figure~\ref{fig:printss}, which
+ prints out some parts of a simpset. If you use it to print out the components of the
+ empty simpset, i.e.~ @{ML empty_ss}
+
+ @{ML_response_fake [display,gray]
+ "print_ss @{context} empty_ss"
+"Simplification rules:
+Congruences rules:
+Simproc patterns:"}
+
+ you can see it contains nothing. This simpset is usually not useful, except as a
+ building block to build bigger simpsets. For example you can add to @{ML empty_ss}
+ the simplification rule @{thm [source] Diff_Int} as follows:
+*}
+
+ML{*val ss1 = empty_ss addsimps [@{thm Diff_Int} RS @{thm eq_reflection}] *}
+
+text {*
+ Printing then out the components of the simpset gives:
+
+ @{ML_response_fake [display,gray]
+ "print_ss @{context} ss1"
+"Simplification rules:
+ ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
+Congruences rules:
+Simproc patterns:"}
+
+ (FIXME: Why does it print out ??.unknown)
+
+ Adding also the congruence rule @{thm [source] UN_cong}
+*}
+
+ML{*val ss2 = ss1 addcongs [@{thm UN_cong} RS @{thm eq_reflection}] *}
+
+text {*
+ gives
+
+ @{ML_response_fake [display,gray]
+ "print_ss @{context} ss2"
+"Simplification rules:
+ ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
+Congruences rules:
+ UNION: \<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk> \<Longrightarrow> \<Union>x\<in>A. C x \<equiv> \<Union>x\<in>B. D x
+Simproc patterns:"}
+
+ Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss}
+ expects this form of the simplification and congruence rules. However, even
+ when adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet.
+
+ In the context of HOL, the first really useful simpset is @{ML HOL_basic_ss}. While
+ printing out the components of this simpset
+
+ @{ML_response_fake [display,gray]
+ "print_ss @{context} HOL_basic_ss"
+"Simplification rules:
+Congruences rules:
+Simproc patterns:"}
+
+ also produces ``nothing'', the printout is misleading. In fact
+ the @{ML HOL_basic_ss} is setup so that it can solve goals of the
+ form
+
+ \begin{isabelle}
+ @{thm TrueI}, @{thm refl[no_vars]}, @{term "t \<equiv> t"} and @{thm FalseE[no_vars]};
+ \end{isabelle}
+
+ and also resolve with assumptions. For example:
+*}
+
+lemma
+ "True" and "t = t" and "t \<equiv> t" and "False \<Longrightarrow> Foo" and "\<lbrakk>A; B; C\<rbrakk> \<Longrightarrow> A"
+apply(tactic {* ALLGOALS (simp_tac HOL_basic_ss) *})
+done
+
+text {*
+ This behaviour is not because of simplification rules, but how the subgoaler, solver
+ and looper are set up in @{ML HOL_basic_ss}.
+
+ The simpset @{ML HOL_ss} is an extention of @{ML HOL_basic_ss} containing
+ already many useful simplification and congruence rules for the logical
+ connectives in HOL.
+
+ @{ML_response_fake [display,gray]
+ "print_ss @{context} HOL_ss"
+"Simplification rules:
+ Pure.triv_forall_equality: (\<And>x. PROP V) \<equiv> PROP V
+ HOL.the_eq_trivial: THE x. x = y \<equiv> y
+ HOL.the_sym_eq_trivial: THE ya. y = ya \<equiv> y
+ \<dots>
+Congruences rules:
+ HOL.simp_implies: \<dots>
+ \<Longrightarrow> (PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q')
+ op -->: \<lbrakk>P \<equiv> P'; P' \<Longrightarrow> Q \<equiv> Q'\<rbrakk> \<Longrightarrow> P \<longrightarrow> Q \<equiv> P' \<longrightarrow> Q'
+Simproc patterns:
+ \<dots>"}
+
+
+ The simplifier is often used to unfold definitions in a proof. For this the
+ simplifier contains the @{ML rewrite_goals_tac}. Suppose for example the
+ definition
+*}
+
+definition "MyTrue \<equiv> True"
+
+text {*
+ then in the following proof we can unfold this constant
+*}
+
+lemma shows "MyTrue \<Longrightarrow> True \<and> True"
+apply(rule conjI)
+apply(tactic {* rewrite_goals_tac [@{thm MyTrue_def}] *})
+txt{* producing the goal state
+
+ \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage} *}
+(*<*)oops(*>*)
+
+text {*
+ As you can see, the tactic unfolds the definitions in all subgoals.
+*}
+
+
+text_raw {*
+\begin{figure}[p]
+\begin{boxedminipage}{\textwidth}
+\begin{isabelle} *}
+types prm = "(nat \<times> nat) list"
+consts perm :: "prm \<Rightarrow> 'a \<Rightarrow> 'a" ("_ \<bullet> _" [80,80] 80)
+
+primrec (perm_nat)
+ "[]\<bullet>c = c"
+ "(ab#pi)\<bullet>c = (if (pi\<bullet>c)=fst ab then snd ab
+ else (if (pi\<bullet>c)=snd ab then fst ab else (pi\<bullet>c)))"
+
+primrec (perm_prod)
+ "pi\<bullet>(x, y) = (pi\<bullet>x, pi\<bullet>y)"
+
+primrec (perm_list)
+ "pi\<bullet>[] = []"
+ "pi\<bullet>(x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
+
+lemma perm_append[simp]:
+ fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+ shows "((pi\<^isub>1@pi\<^isub>2)\<bullet>c) = (pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c))"
+by (induct pi\<^isub>1) (auto)
+
+lemma perm_eq[simp]:
+ fixes c::"nat" and pi::"prm"
+ shows "(pi\<bullet>c = pi\<bullet>d) = (c = d)"
+by (induct pi) (auto)
+
+lemma perm_rev[simp]:
+ fixes c::"nat" and pi::"prm"
+ shows "pi\<bullet>((rev pi)\<bullet>c) = c"
+by (induct pi arbitrary: c) (auto)
+
+lemma perm_compose:
+ fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+ shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>(pi\<^isub>1\<bullet>c)"
+by (induct pi\<^isub>2) (auto)
+text_raw {*
+\end{isabelle}
+\end{boxedminipage}
+\caption{A simple theory about permutations over @{typ nat}. The point is that the
+ lemma @{thm [source] perm_compose} cannot be directly added to the simplifier, as
+ it would cause the simplifier to loop. It can still be used as a simplification
+ rule if the permutation is sufficiently protected.\label{fig:perms}
+ (FIXME: Uses old primrec.)}
+\end{figure} *}
+
+
+text {*
+ The simplifier is often used in order to bring terms into a normal form.
+ Unfortunately, often the situation arises that the corresponding
+ simplification rules will cause the simplifier to run into an infinite
+ loop. Consider for example the simple theory about permutations over natural
+ numbers shown in Figure~\ref{fig:perms}. The purpose of the lemmas is to
+ push permutations as far inside as possible, where they might disappear by
+ Lemma @{thm [source] perm_rev}. However, to fully normalise all instances,
+ it would be desirable to add also the lemma @{thm [source] perm_compose} to
+ the simplifier for pushing permutations over other permutations. Unfortunately,
+ the right-hand side of this lemma is again an instance of the left-hand side
+ and so causes an infinite loop. The seems to be no easy way to reformulate
+ this rule and so one ends up with clunky proofs like:
+*}
+
+lemma
+ fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+ shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
+apply(simp)
+apply(rule trans)
+apply(rule perm_compose)
+apply(simp)
+done
+
+text {*
+ It is however possible to create a single simplifier tactic that solves
+ such proofs. The trick is to introduce an auxiliary constant for permutations
+ and split the simplification into two phases (below actually three). Let
+ assume the auxiliary constant is
+*}
+
+definition
+ perm_aux :: "prm \<Rightarrow> 'a \<Rightarrow> 'a" ("_ \<bullet>aux _" [80,80] 80)
+where
+ "pi \<bullet>aux c \<equiv> pi \<bullet> c"
+
+text {* Now the two lemmas *}
+
+lemma perm_aux_expand:
+ fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+ shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = pi\<^isub>1 \<bullet>aux (pi\<^isub>2\<bullet>c)"
+unfolding perm_aux_def by (rule refl)
+
+lemma perm_compose_aux:
+ fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+ shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>aux c) = (pi\<^isub>1\<bullet>pi\<^isub>2) \<bullet>aux (pi\<^isub>1\<bullet>c)"
+unfolding perm_aux_def by (rule perm_compose)
+
+text {*
+ are simple consequence of the definition and @{thm [source] perm_compose}.
+ More importantly, the lemma @{thm [source] perm_compose_aux} can be safely
+ added to the simplifier, because now the right-hand side is not anymore an instance
+ of the left-hand side. In a sense it freezes all redexes of permutation compositions
+ after one step. In this way, we can split simplification of permutations
+ into three phases without the user not noticing anything about the auxiliary
+ contant. We first freeze any instance of permutation compositions in the term using
+ lemma @{thm [source] "perm_aux_expand"} (Line 9);
+ then simplifiy all other permutations including pusing permutations over
+ other permutations by rule @{thm [source] perm_compose_aux} (Line 10); and
+ finally ``unfreeze'' all instances of permutation compositions by unfolding
+ the definition of the auxiliary constant.
+*}
+
+ML %linenosgray{*val perm_simp_tac =
+let
+ val thms1 = [@{thm perm_aux_expand}]
+ val thms2 = [@{thm perm_append}, @{thm perm_eq}, @{thm perm_rev},
+ @{thm perm_compose_aux}] @ @{thms perm_prod.simps} @
+ @{thms perm_list.simps} @ @{thms perm_nat.simps}
+ val thms3 = [@{thm perm_aux_def}]
+in
+ simp_tac (HOL_basic_ss addsimps thms1)
+ THEN' simp_tac (HOL_basic_ss addsimps thms2)
+ THEN' simp_tac (HOL_basic_ss addsimps thms3)
+end*}
+
+text {*
+ For all three phases we have to build simpsets addig specific lemmas. As is sufficient
+ for our purposes here, we can add these lemma to @{ML HOL_basic_ss} in order to obtain
+ the desired results. Now we can solve the following lemma
+*}
+
+lemma
+ fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+ shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
+apply(tactic {* perm_simp_tac 1 *})
+done
+
+
+text {*
+ in one step. This tactic can deal with most instances of normalising permutations;
+ in order to solve all cases we have to deal with corner-cases such as the
+ lemma being an exact instance of the permutation composition lemma. This can
+ often be done easier by implementing a simproc or a conversion. Both will be
+ explained in the next two chapters.
+
+ (FIXME: Is it interesting to say something about @{term "op =simp=>"}?)
+
+ (FIXME: What are the second components of the congruence rules---something to
+ do with weak congruence constants?)
+
+ (FIXME: Anything interesting to say about @{ML Simplifier.clear_ss}?)
+
+ (FIXME: @{ML ObjectLogic.full_atomize_tac},
+ @{ML ObjectLogic.rulify_tac})
+
+*}
+
+section {* Simprocs *}
+
+text {*
+ In Isabelle you can also implement custom simplification procedures, called
+ \emph{simprocs}. Simprocs can be triggered by the simplifier on a specified
+ term-pattern and rewrite a term according to a theorem. They are useful in
+ cases where a rewriting rule must be produced on ``demand'' or when
+ rewriting by simplification is too unpredictable and potentially loops.
+
+ To see how simprocs work, let us first write a simproc that just prints out
+ the pattern which triggers it and otherwise does nothing. For this
+ you can use the function:
+*}
+
+ML %linenosgray{*fun fail_sp_aux simpset redex =
+let
+ val ctxt = Simplifier.the_context simpset
+ val _ = warning ("The redex: " ^ (str_of_cterm ctxt redex))
+in
+ NONE
+end*}
+
+text {*
+ This function takes a simpset and a redex (a @{ML_type cterm}) as
+ arguments. In Lines 3 and~4, we first extract the context from the given
+ simpset and then print out a message containing the redex. The function
+ returns @{ML NONE} (standing for an optional @{ML_type thm}) since at the
+ moment we are \emph{not} interested in actually rewriting anything. We want
+ that the simproc is triggered by the pattern @{term "Suc n"}. This can be
+ done by adding the simproc to the current simpset as follows
+*}
+
+simproc_setup %gray fail_sp ("Suc n") = {* K fail_sp_aux *}
+
+text {*
+ where the second argument specifies the pattern and the right-hand side
+ contains the code of the simproc (we have to use @{ML K} since we ignoring
+ an argument about morphisms\footnote{FIXME: what does the morphism do?}).
+ After this, the simplifier is aware of the simproc and you can test whether
+ it fires on the lemma:
+*}
+
+lemma shows "Suc 0 = 1"
+apply(simp)
+(*<*)oops(*>*)
+
+text {*
+ This will print out the message twice: once for the left-hand side and
+ once for the right-hand side. The reason is that during simplification the
+ simplifier will at some point reduce the term @{term "1::nat"} to @{term "Suc
+ 0"}, and then the simproc ``fires'' also on that term.
+
+ We can add or delete the simproc from the current simpset by the usual
+ \isacommand{declare}-statement. For example the simproc will be deleted
+ with the declaration
+*}
+
+declare [[simproc del: fail_sp]]
+
+text {*
+ If you want to see what happens with just \emph{this} simproc, without any
+ interference from other rewrite rules, you can call @{text fail_sp}
+ as follows:
+*}
+
+lemma shows "Suc 0 = 1"
+apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc fail_sp}]) 1*})
+(*<*)oops(*>*)
+
+text {*
+ Now the message shows up only once since the term @{term "1::nat"} is
+ left unchanged.
+
+ Setting up a simproc using the command \isacommand{simproc\_setup} will
+ always add automatically the simproc to the current simpset. If you do not
+ want this, then you have to use a slightly different method for setting
+ up the simproc. First the function @{ML fail_sp_aux} needs to be modified
+ to
+*}
+
+ML{*fun fail_sp_aux' simpset redex =
+let
+ val ctxt = Simplifier.the_context simpset
+ val _ = warning ("The redex: " ^ (Syntax.string_of_term ctxt redex))
+in
+ NONE
+end*}
+
+text {*
+ Here the redex is given as a @{ML_type term}, instead of a @{ML_type cterm}
+ (therefore we printing it out using the function @{ML string_of_term in Syntax}).
+ We can turn this function into a proper simproc using the function
+ @{ML Simplifier.simproc_i}:
+*}
+
+
+ML{*val fail_sp' =
+let
+ val thy = @{theory}
+ val pat = [@{term "Suc n"}]
+in
+ Simplifier.simproc_i thy "fail_sp'" pat (K fail_sp_aux')
+end*}
+
+text {*
+ Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
+ The function also takes a list of patterns that can trigger the simproc.
+ Now the simproc is set up and can be explicitly added using
+ @{ML addsimprocs} to a simpset whenerver
+ needed.
+
+ Simprocs are applied from inside to outside and from left to right. You can
+ see this in the proof
+*}
+
+lemma shows "Suc (Suc 0) = (Suc 1)"
+apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [fail_sp']) 1*})
+(*<*)oops(*>*)
+
+text {*
+ The simproc @{ML fail_sp'} prints out the sequence
+
+@{text [display]
+"> Suc 0
+> Suc (Suc 0)
+> Suc 1"}
+
+ To see how a simproc applies a theorem, let us implement a simproc that
+ rewrites terms according to the equation:
+*}
+
+lemma plus_one:
+ shows "Suc n \<equiv> n + 1" by simp
+
+text {*
+ Simprocs expect that the given equation is a meta-equation, however the
+ equation can contain preconditions (the simproc then will only fire if the
+ preconditions can be solved). To see that one has relatively precise control over
+ the rewriting with simprocs, let us further assume we want that the simproc
+ only rewrites terms ``greater'' than @{term "Suc 0"}. For this we can write
+*}
+
+
+ML{*fun plus_one_sp_aux ss redex =
+ case redex of
+ @{term "Suc 0"} => NONE
+ | _ => SOME @{thm plus_one}*}
+
+text {*
+ and set up the simproc as follows.
+*}
+
+ML{*val plus_one_sp =
+let
+ val thy = @{theory}
+ val pat = [@{term "Suc n"}]
+in
+ Simplifier.simproc_i thy "sproc +1" pat (K plus_one_sp_aux)
+end*}
+
+text {*
+ Now the simproc is set up so that it is triggered by terms
+ of the form @{term "Suc n"}, but inside the simproc we only produce
+ a theorem if the term is not @{term "Suc 0"}. The result you can see
+ in the following proof
+*}
+
+lemma shows "P (Suc (Suc (Suc 0))) (Suc 0)"
+apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [plus_one_sp]) 1*})
+txt{*
+ where the simproc produces the goal state
+
+ \begin{minipage}{\textwidth}
+ @{subgoals[display]}
+ \end{minipage}
+*}
+(*<*)oops(*>*)
+
+text {*
+ As usual with rewriting you have to worry about looping: you already have
+ a loop with @{ML plus_one_sp}, if you apply it with the default simpset (because
+ the default simpset contains a rule which just does the opposite of @{ML plus_one_sp},
+ namely rewriting @{text [quotes] "+ 1"} to a successor). So you have to be careful
+ in choosing the right simpset to which you add a simproc.
+
+ Next let us implement a simproc that replaces terms of the form @{term "Suc n"}
+ with the number @{text n} increase by one. First we implement a function that
+ takes a term and produces the corresponding integer value.
+*}
+
+ML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t
+ | dest_suc_trm t = snd (HOLogic.dest_number t)*}
+
+text {*
+ It uses the library function @{ML dest_number in HOLogic} that transforms
+ (Isabelle) terms, like @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so
+ on, into integer values. This function raises the exception @{ML TERM}, if
+ the term is not a number. The next function expects a pair consisting of a term
+ @{text t} (containing @{term Suc}s) and the corresponding integer value @{text n}.
+*}
+
+ML %linenosgray{*fun get_thm ctxt (t, n) =
+let
+ val num = HOLogic.mk_number @{typ "nat"} n
+ val goal = Logic.mk_equals (t, num)
+in
+ Goal.prove ctxt [] [] goal (K (arith_tac ctxt 1))
+end*}
+
+text {*
+ From the integer value it generates the corresponding number term, called
+ @{text num} (Line 3), and then generates the meta-equation @{text "t \<equiv> num"}
+ (Line 4), which it proves by the arithmetic tactic in Line 6.
+
+ For our purpose at the moment, proving the meta-equation using @{ML arith_tac} is
+ fine, but there is also an alternative employing the simplifier with a very
+ restricted simpset. For the kind of lemmas we want to prove, the simpset
+ @{text "num_ss"} in the code will suffice.
+*}
+
+ML{*fun get_thm_alt ctxt (t, n) =
+let
+ val num = HOLogic.mk_number @{typ "nat"} n
+ val goal = Logic.mk_equals (t, num)
+ val num_ss = HOL_ss addsimps [@{thm One_nat_def}, @{thm Let_def}] @
+ @{thms nat_number} @ @{thms neg_simps} @ @{thms plus_nat.simps}
+in
+ Goal.prove ctxt [] [] goal (K (simp_tac num_ss 1))
+end*}
+
+text {*
+ The advantage of @{ML get_thm_alt} is that it leaves very little room for
+ something to go wrong; in contrast it is much more difficult to predict
+ what happens with @{ML arith_tac}, especially in more complicated
+ circumstances. The disatvantage of @{ML get_thm_alt} is to find a simpset
+ that is sufficiently powerful to solve every instance of the lemmas
+ we like to prove. This requires careful tuning, but is often necessary in
+ ``production code''.\footnote{It would be of great help if there is another
+ way than tracing the simplifier to obtain the lemmas that are successfully
+ applied during simplification. Alas, there is none.}
+
+ Anyway, either version can be used in the function that produces the actual
+ theorem for the simproc.
+*}
+
+ML{*fun nat_number_sp_aux ss t =
+let
+ val ctxt = Simplifier.the_context ss
+in
+ SOME (get_thm ctxt (t, dest_suc_trm t))
+ handle TERM _ => NONE
+end*}
+
+text {*
+ This function uses the fact that @{ML dest_suc_trm} might throw an exception
+ @{ML TERM}. In this case there is nothing that can be rewritten and therefore no
+ theorem is produced (i.e.~the function returns @{ML NONE}). To try out the simproc
+ on an example, you can set it up as follows:
+*}
+
+ML{*val nat_number_sp =
+let
+ val thy = @{theory}
+ val pat = [@{term "Suc n"}]
+in
+ Simplifier.simproc_i thy "nat_number" pat (K nat_number_sp_aux)
+end*}
+
+text {*
+ Now in the lemma
+ *}
+
+lemma "P (Suc (Suc 2)) (Suc 99) (0::nat) (Suc 4 + Suc 0) (Suc (0 + 0))"
+apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number_sp]) 1*})
+txt {*
+ you obtain the more legible goal state
+
+ \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}
+ *}
+(*<*)oops(*>*)
+
+text {*
+ where the simproc rewrites all @{term "Suc"}s except in the last argument. There it cannot
+ rewrite anything, because it does not know how to transform the term @{term "Suc (0 + 0)"}
+ into a number. To solve this problem have a look at the next exercise.
+
+ \begin{exercise}\label{ex:addsimproc}
+ Write a simproc that replaces terms of the form @{term "t\<^isub>1 + t\<^isub>2"} by their
+ result. You can assume the terms are ``proper'' numbers, that is of the form
+ @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so on.
+ \end{exercise}
+
+ (FIXME: We did not do anything with morphisms. Anything interesting
+ one can say about them?)
+*}
+
+section {* Conversions\label{sec:conversion} *}
+
+text {*
+
+ Conversions are a thin layer on top of Isabelle's inference kernel, and
+ can be viewed as a controllable, bare-bone version of Isabelle's simplifier.
+ One difference between conversions and the simplifier is that the former
+ act on @{ML_type cterm}s while the latter acts on @{ML_type thm}s.
+ However, we will also show in this section how conversions can be applied
+ to theorems via tactics. The type for conversions is
+*}
+
+ML{*type conv = cterm -> thm*}
+
+text {*
+ whereby the produced theorem is always a meta-equality. A simple conversion
+ is the function @{ML "Conv.all_conv"}, which maps a @{ML_type cterm} to an
+ instance of the (meta)reflexivity theorem. For example:
+
+ @{ML_response_fake [display,gray]
+ "Conv.all_conv @{cterm \"Foo \<or> Bar\"}"
+ "Foo \<or> Bar \<equiv> Foo \<or> Bar"}
+
+ Another simple conversion is @{ML Conv.no_conv} which always raises the
+ exception @{ML CTERM}.
+
+ @{ML_response_fake [display,gray]
+ "Conv.no_conv @{cterm True}"
+ "*** Exception- CTERM (\"no conversion\", []) raised"}
+
+ A more interesting conversion is the function @{ML "Thm.beta_conversion"}: it
+ produces a meta-equation between a term and its beta-normal form. For example
+
+ @{ML_response_fake [display,gray]
+ "let
+ val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
+ val two = @{cterm \"2::nat\"}
+ val ten = @{cterm \"10::nat\"}
+in
+ Thm.beta_conversion true (Thm.capply (Thm.capply add two) ten)
+end"
+ "((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10"}
+
+ Note that the actual response in this example is @{term "2 + 10 \<equiv> 2 + (10::nat)"},
+ since the pretty-printer for @{ML_type cterm}s already beta-normalises terms.
+ But how we constructed the term (using the function
+ @{ML Thm.capply}, which is the application @{ML $} for @{ML_type cterm}s)
+ ensures that the left-hand side must contain beta-redexes. Indeed
+ if we obtain the ``raw'' representation of the produced theorem, we
+ can see the difference:
+
+ @{ML_response [display,gray]
+"let
+ val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
+ val two = @{cterm \"2::nat\"}
+ val ten = @{cterm \"10::nat\"}
+ val thm = Thm.beta_conversion true (Thm.capply (Thm.capply add two) ten)
+in
+ #prop (rep_thm thm)
+end"
+"Const (\"==\",\<dots>) $
+ (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $
+ (Const (\"HOL.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"}
+
+ The argument @{ML true} in @{ML Thm.beta_conversion} indicates that
+ the right-hand side will be fully beta-normalised. If instead
+ @{ML false} is given, then only a single beta-reduction is performed
+ on the outer-most level. For example
+
+ @{ML_response_fake [display,gray]
+ "let
+ val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
+ val two = @{cterm \"2::nat\"}
+in
+ Thm.beta_conversion false (Thm.capply add two)
+end"
+ "((\<lambda>x y. x + y) 2) \<equiv> \<lambda>y. 2 + y"}
+
+ Again, we actually see as output only the fully normalised term
+ @{text "\<lambda>y. 2 + y"}.
+
+ The main point of conversions is that they can be used for rewriting
+ @{ML_type cterm}s. To do this you can use the function @{ML
+ "Conv.rewr_conv"}, which expects a meta-equation as an argument. Suppose we
+ want to rewrite a @{ML_type cterm} according to the meta-equation:
+*}
+
+lemma true_conj1: "True \<and> P \<equiv> P" by simp
+
+text {*
+ You can see how this function works in the example rewriting
+ @{term "True \<and> (Foo \<longrightarrow> Bar)"} to @{term "Foo \<longrightarrow> Bar"}.
+
+ @{ML_response_fake [display,gray]
+"let
+ val ctrm = @{cterm \"True \<and> (Foo \<longrightarrow> Bar)\"}
+in
+ Conv.rewr_conv @{thm true_conj1} ctrm
+end"
+ "True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar"}
+
+ Note, however, that the function @{ML Conv.rewr_conv} only rewrites the
+ outer-most level of the @{ML_type cterm}. If the given @{ML_type cterm} does not match
+ exactly the
+ left-hand side of the theorem, then @{ML Conv.rewr_conv} raises
+ the exception @{ML CTERM}.
+
+ This very primitive way of rewriting can be made more powerful by
+ combining several conversions into one. For this you can use conversion
+ combinators. The simplest conversion combinator is @{ML then_conv},
+ which applies one conversion after another. For example
+
+ @{ML_response_fake [display,gray]
+"let
+ val conv1 = Thm.beta_conversion false
+ val conv2 = Conv.rewr_conv @{thm true_conj1}
+ val ctrm = Thm.capply @{cterm \"\<lambda>x. x \<and> False\"} @{cterm \"True\"}
+in
+ (conv1 then_conv conv2) ctrm
+end"
+ "(\<lambda>x. x \<and> False) True \<equiv> False"}
+
+ where we first beta-reduce the term and then rewrite according to
+ @{thm [source] true_conj1}. (Recall the problem with the pretty-printer
+ normalising all terms.)
+
+ The conversion combinator @{ML else_conv} tries out the
+ first one, and if it does not apply, tries the second. For example
+
+ @{ML_response_fake [display,gray]
+"let
+ val conv = Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv
+ val ctrm1 = @{cterm \"True \<and> Q\"}
+ val ctrm2 = @{cterm \"P \<or> (True \<and> Q)\"}
+in
+ (conv ctrm1, conv ctrm2)
+end"
+"(True \<and> Q \<equiv> Q, P \<or> True \<and> Q \<equiv> P \<or> True \<and> Q)"}
+
+ Here the conversion of @{thm [source] true_conj1} only applies
+ in the first case, but fails in the second. The whole conversion
+ does not fail, however, because the combinator @{ML Conv.else_conv} will then
+ try out @{ML Conv.all_conv}, which always succeeds.
+
+ The conversion combinator @{ML Conv.try_conv} constructs a conversion
+ which is tried out on a term, but in case of failure just does nothing.
+ For example
+
+ @{ML_response_fake [display,gray]
+ "Conv.try_conv (Conv.rewr_conv @{thm true_conj1}) @{cterm \"True \<or> P\"}"
+ "True \<or> P \<equiv> True \<or> P"}
+
+ Apart from the function @{ML beta_conversion in Thm}, which is able to fully
+ beta-normalise a term, the conversions so far are restricted in that they
+ only apply to the outer-most level of a @{ML_type cterm}. In what follows we
+ will lift this restriction. The combinator @{ML Conv.arg_conv} will apply
+ the conversion to the first argument of an application, that is the term
+ must be of the form @{ML "t1 $ t2" for t1 t2} and the conversion is applied
+ to @{text t2}. For example
+
+ @{ML_response_fake [display,gray]
+"let
+ val conv = Conv.rewr_conv @{thm true_conj1}
+ val ctrm = @{cterm \"P \<or> (True \<and> Q)\"}
+in
+ Conv.arg_conv conv ctrm
+end"
+"P \<or> (True \<and> Q) \<equiv> P \<or> Q"}
+
+ The reason for this behaviour is that @{text "(op \<or>)"} expects two
+ arguments. Therefore the term must be of the form @{text "(Const \<dots> $ t1) $ t2"}. The
+ conversion is then applied to @{text "t2"} which in the example above
+ stands for @{term "True \<and> Q"}. The function @{ML Conv.fun_conv} applies
+ the conversion to the first argument of an application.
+
+ The function @{ML Conv.abs_conv} applies a conversion under an abstractions.
+ For example:
+
+ @{ML_response_fake [display,gray]
+"let
+ val conv = K (Conv.rewr_conv @{thm true_conj1})
+ val ctrm = @{cterm \"\<lambda>P. True \<and> P \<and> Foo\"}
+in
+ Conv.abs_conv conv @{context} ctrm
+end"
+ "\<lambda>P. True \<and> P \<and> Foo \<equiv> \<lambda>P. P \<and> Foo"}
+
+ Note that this conversion needs a context as an argument. The conversion that
+ goes under an application is @{ML Conv.combination_conv}. It expects two conversions
+ as arguments, each of which is applied to the corresponding ``branch'' of the
+ application.
+
+ We can now apply all these functions in a conversion that recursively
+ descends a term and applies a ``@{thm [source] true_conj1}''-conversion
+ in all possible positions.
+*}
+
+ML %linenosgray{*fun all_true1_conv ctxt ctrm =
+ case (Thm.term_of ctrm) of
+ @{term "op \<and>"} $ @{term True} $ _ =>
+ (Conv.arg_conv (all_true1_conv ctxt) then_conv
+ Conv.rewr_conv @{thm true_conj1}) ctrm
+ | _ $ _ => Conv.combination_conv
+ (all_true1_conv ctxt) (all_true1_conv ctxt) ctrm
+ | Abs _ => Conv.abs_conv (fn (_, ctxt) => all_true1_conv ctxt) ctxt ctrm
+ | _ => Conv.all_conv ctrm*}
+
+text {*
+ This function ``fires'' if the terms is of the form @{text "True \<and> \<dots>"};
+ it descends under applications (Line 6 and 7) and abstractions
+ (Line 8); otherwise it leaves the term unchanged (Line 9). In Line 2
+ we need to transform the @{ML_type cterm} into a @{ML_type term} in order
+ to be able to pattern-match the term. To see this
+ conversion in action, consider the following example:
+
+@{ML_response_fake [display,gray]
+"let
+ val ctxt = @{context}
+ val ctrm = @{cterm \"distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}
+in
+ all_true1_conv ctxt ctrm
+end"
+ "distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x"}
+
+ To see how much control you have about rewriting by using conversions, let us
+ make the task a bit more complicated by rewriting according to the rule
+ @{text true_conj1}, but only in the first arguments of @{term If}s. Then
+ the conversion should be as follows.
+*}
+
+ML{*fun if_true1_conv ctxt ctrm =
+ case Thm.term_of ctrm of
+ Const (@{const_name If}, _) $ _ =>
+ Conv.arg_conv (all_true1_conv ctxt) ctrm
+ | _ $ _ => Conv.combination_conv
+ (if_true1_conv ctxt) (if_true1_conv ctxt) ctrm
+ | Abs _ => Conv.abs_conv (fn (_, ctxt) => if_true1_conv ctxt) ctxt ctrm
+ | _ => Conv.all_conv ctrm *}
+
+text {*
+ Here is an example for this conversion:
+
+ @{ML_response_fake [display,gray]
+"let
+ val ctxt = @{context}
+ val ctrm =
+ @{cterm \"if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False\"}
+in
+ if_true1_conv ctxt ctrm
+end"
+"if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False
+\<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False"}
+*}
+
+text {*
+ So far we only applied conversions to @{ML_type cterm}s. Conversions can, however,
+ also work on theorems using the function @{ML "Conv.fconv_rule"}. As an example,
+ consider the conversion @{ML all_true1_conv} and the lemma:
+*}
+
+lemma foo_test: "P \<or> (True \<and> \<not>P)" by simp
+
+text {*
+ Using the conversion you can transform this theorem into a new theorem
+ as follows
+
+ @{ML_response_fake [display,gray]
+ "Conv.fconv_rule (all_true1_conv @{context}) @{thm foo_test}"
+ "?P \<or> \<not> ?P"}
+
+ Finally, conversions can also be turned into tactics and then applied to
+ goal states. This can be done with the help of the function @{ML CONVERSION},
+ and also some predefined conversion combinators that traverse a goal
+ state. The combinators for the goal state are: @{ML Conv.params_conv} for
+ converting under parameters (i.e.~where goals are of the form @{text "\<And>x. P \<Longrightarrow>
+ Q"}); the function @{ML Conv.prems_conv} for applying a conversion to all
+ premises of a goal, and @{ML Conv.concl_conv} for applying a conversion to
+ the conclusion of a goal.
+
+ Assume we want to apply @{ML all_true1_conv} only in the conclusion
+ of the goal, and @{ML if_true1_conv} should only apply to the premises.
+ Here is a tactic doing exactly that:
+*}
+
+ML{*fun true1_tac ctxt = CSUBGOAL (fn (goal, i) =>
+ CONVERSION
+ (Conv.params_conv ~1 (fn ctxt =>
+ (Conv.prems_conv ~1 (if_true1_conv ctxt) then_conv
+ Conv.concl_conv ~1 (all_true1_conv ctxt))) ctxt) i)*}
+
+text {*
+ We call the conversions with the argument @{ML "~1"}. This is to
+ analyse all parameters, premises and conclusions. If we call them with
+ a non-negative number, say @{text n}, then these conversions will
+ only be called on @{text n} premises (similar for parameters and
+ conclusions). To test the tactic, consider the proof
+*}
+
+lemma
+ "if True \<and> P then P else True \<and> False \<Longrightarrow>
+ (if True \<and> Q then True \<and> Q else P) \<longrightarrow> True \<and> (True \<and> Q)"
+apply(tactic {* true1_tac @{context} 1 *})
+txt {* where the tactic yields the goal state
+
+ \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}*}
+(*<*)oops(*>*)
+
+text {*
+ As you can see, the premises are rewritten according to @{ML if_true1_conv}, while
+ the conclusion according to @{ML all_true1_conv}.
+
+ To sum up this section, conversions are not as powerful as the simplifier
+ and simprocs; the advantage of conversions, however, is that you never have
+ to worry about non-termination.
+
+ \begin{exercise}\label{ex:addconversion}
+ Write a tactic that does the same as the simproc in exercise
+ \ref{ex:addsimproc}, but is based in conversions. That means replace terms
+ of the form @{term "t\<^isub>1 + t\<^isub>2"} by their result. You can make
+ the same assumptions as in \ref{ex:addsimproc}.
+ \end{exercise}
+
+ \begin{exercise}\label{ex:compare}
+ Compare your solutions of Exercises~\ref{ex:addsimproc} and \ref{ex:addconversion},
+ and try to determine which way of rewriting such terms is faster. For this you might
+ have to construct quite large terms. Also see Recipe \ref{rec:timing} for information
+ about timing.
+ \end{exercise}
+
+ \begin{readmore}
+ See @{ML_file "Pure/conv.ML"} for more information about conversion combinators.
+ Further conversions are defined in @{ML_file "Pure/thm.ML"},
+ @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/meta_simplifier.ML"}.
+ \end{readmore}
+
+*}
+
+text {*
+ (FIXME: check whether @{ML Pattern.match_rew} and @{ML Pattern.rewrite_term}
+ are of any use/efficient)
+*}
+
+
+section {* Structured Proofs (TBD) *}
+
+text {* TBD *}
+
+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