--- a/doc-src/Ref/simplifier.tex Thu Sep 24 15:36:16 1998 +0200
+++ b/doc-src/Ref/simplifier.tex Thu Sep 24 16:53:00 1998 +0200
@@ -135,6 +135,8 @@
Delsimprocs : simproc list -> unit
Addcongs : thm list -> unit
Delcongs : thm list -> unit
+Addsplits : thm list -> unit
+Delsplits : thm list -> unit
\end{ttbox}
Depending on the theory context, the \texttt{Add} and \texttt{Del}
@@ -164,7 +166,13 @@
\item[\ttindexbold{Addcongs} $thms$;] adds congruence rules to the
current simpset.
-\item[\ttindexbold{Delcongs} $thms$;] deletes congruence rules to the
+\item[\ttindexbold{Delcongs} $thms$;] deletes congruence rules from the
+ current simpset.
+
+\item[\ttindexbold{Addsplits} $thms$;] adds splitting rules to the
+ current simpset.
+
+\item[\ttindexbold{Delsplits} $thms$;] deletes splitting rules from the
current simpset.
\end{ttdescription}
@@ -597,12 +605,14 @@
\subsection{*The looper}\label{sec:simp-looper}
\begin{ttbox}
-setloop : simpset * (int -> tactic) -> simpset \hfill{\bf infix 4}
-addloop : simpset * (int -> tactic) -> simpset \hfill{\bf infix 4}
+setloop : simpset * (int -> tactic) -> simpset \hfill{\bf infix 4}
+addloop : simpset * (string * (int -> tactic)) -> simpset \hfill{\bf infix 4}
+delloop : simpset * string -> simpset \hfill{\bf infix 4}
addsplits : simpset * thm list -> simpset \hfill{\bf infix 4}
+delsplits : simpset * thm list -> simpset \hfill{\bf infix 4}
\end{ttbox}
-The looper is a tactic that is applied after simplification, in case
+The looper is a list of tactics that are applied after simplification, in case
the solver failed to solve the simplified goal. If the looper
succeeds, the simplification process is started all over again. Each
of the subgoals generated by the looper is attacked in turn, in
@@ -614,18 +624,59 @@
\begin{ttdescription}
-\item[$ss$ \ttindexbold{setloop} $tacf$] installs $tacf$ as the looper
- of $ss$.
+\item[$ss$ \ttindexbold{setloop} $tacf$] installs $tacf$ as the only looper
+ tactic of $ss$.
-\item[$ss$ \ttindexbold{addloop} $tacf$] adds $tacf$ as an additional
- looper; it will be tried after the loopers which had already been
- present in $ss$.
+\item[$ss$ \ttindexbold{addloop} $(name,tacf)$] adds $tacf$ as an additional
+ looper tactic with name $name$; it will be tried after the looper tactics
+ that had already been present in $ss$.
+
+\item[$ss$ \ttindexbold{delloop} $name$] deletes the looper tactic $name$
+ from $ss$.
\item[$ss$ \ttindexbold{addsplits} $thms$] adds
- \texttt{(split_tac~$thms$)} as an additional looper.
+ split tactics for $thms$ as additional looper tactics of $ss$.
+
+\item[$ss$ \ttindexbold{addsplits} $thms$] deletes the
+ split tactics for $thms$ from the looper tactics of $ss$.
\end{ttdescription}
+The splitter replaces applications of a given function; the right-hand side
+of the replacement can be anything. For example, here is a splitting rule
+for conditional expressions:
+\[ \Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp (\Var{Q} \imp \Var{P}(\Var{x}))
+\conj (\lnot\Var{Q} \imp \Var{P}(\Var{y}))
+\]
+Another example is the elimination operator (which happens to be
+called~$split$) for Cartesian products:
+\[ \Var{P}(split(\Var{f},\Var{p})) \bimp (\forall a~b. \Var{p} =
+\langle a,b\rangle \imp \Var{P}(\Var{f}(a,b)))
+\]
+
+For technical reasons, there is a distinction between case splitting in the
+conclusion and in the premises of a subgoal. The former is done by
+\texttt{split_tac} with rules like \texttt{split_if},
+which does not split the subgoal, while the latter is done by
+\texttt{split_asm_tac} with rules like \texttt{split_if_asm},
+which splits the subgoal.
+The operator \texttt{addsplits} automatically takes care of which tactic to
+call, analyzing the form of the rules given as argument.
+\begin{warn}
+Due to \texttt{split_asm_tac}, the simplifier may split subgoals!
+\end{warn}
+
+Case splits should be allowed only when necessary; they are expensive
+and hard to control. Here is an example of use, where \texttt{split_if}
+is the first rule above:
+\begin{ttbox}
+by (simp_tac (simpset() addloop ("split if",split_tac [split_if])) 1);
+\end{ttbox}
+Users would usually prefer the following shortcut using
+\ttindex{addsplits}:
+\begin{ttbox}
+by (simp_tac (simpset() addsplits [split_if]) 1);
+\end{ttbox}
\section{The simplification tactics}\label{simp-tactics}
@@ -1266,6 +1317,7 @@
\begin{ttbox}
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
\end{ttbox}
+
The function \texttt{atomize} analyses a theorem in order to extract
atomic rewrite rules. The head of all the patterns, matched by the
wildcard~\texttt{_}, is the coercion function \texttt{Trueprop}.
@@ -1282,22 +1334,25 @@
There are several cases, depending upon the form of the conclusion:
\begin{itemize}
\item Conjunction: extract rewrites from both conjuncts.
-
\item Implication: convert $P\imp Q$ to the meta-implication $P\Imp Q$ and
extract rewrites from~$Q$; these will be conditional rewrites with the
condition~$P$.
-
\item Universal quantification: remove the quantifier, replacing the bound
variable by a schematic variable, and extract rewrites from the body.
-
\item \texttt{True} and \texttt{False} contain no useful rewrites.
-
\item Anything else: return the theorem in a singleton list.
\end{itemize}
The resulting theorems are not literally atomic --- they could be
-disjunctive, for example --- but are broken down as much as possible. See
-the file \texttt{ZF/simpdata.ML} for a sophisticated translation of
-set-theoretic formulae into rewrite rules.
+disjunctive, for example --- but are broken down as much as possible.
+See the file \texttt{ZF/simpdata.ML} for a sophisticated translation of
+set-theoretic formulae into rewrite rules.
+
+For standard situations like the above,
+there is a generic auxiliary function \ttindexbold{mk_atomize} that takes a
+list of pairs $(name, thms)$, where $name$ is an operator name and
+$thms$ is a list of theorems to resolve with in case the pattern matches,
+and returns a suitable \texttt{atomize} function.
+
The simplified rewrites must now be converted into meta-equalities. The
rule \texttt{eq_reflection} converts equality rewrites, while {\tt
@@ -1313,17 +1368,17 @@
val P_iff_T = int_prove_fun "P ==> (P <-> True)";
val iff_reflection_T = P_iff_T RS iff_reflection;
\end{ttbox}
-The function \texttt{mk_meta_eq} converts a theorem to a meta-equality
+The function \texttt{mk_eq} converts a theorem to a meta-equality
using the case analysis described above.
\begin{ttbox}
-fun mk_meta_eq th = case concl_of th of
+fun mk_eq th = case concl_of th of
_ $ (Const("op =",_)$_$_) => th RS eq_reflection
| _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
| _ $ (Const("Not",_)$_) => th RS iff_reflection_F
| _ => th RS iff_reflection_T;
\end{ttbox}
-The three functions \texttt{gen_all}, \texttt{atomize} and \texttt{mk_meta_eq} will
-be composed together and supplied below to \texttt{setmksimps}.
+The three functions \texttt{gen_all}, \texttt{atomize} and \texttt{mk_eq}
+will be composed together and supplied below to \texttt{setmksimps}.
\subsection{Making the initial simpset}
@@ -1337,12 +1392,6 @@
fun ss addcongs congs =
ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
\end{ttbox}
-Furthermore, we define the infix operator \ttindex{addsplits}
-providing a convenient interface for adding split tactics.
-\begin{ttbox}
-infix 4 addsplits;
-fun ss addsplits splits = ss addloop (split_tac splits);
-\end{ttbox}
The list \texttt{IFOL_simps} contains the default rewrite rules for
intuitionistic first-order logic. The first of these is the reflexive law
@@ -1362,7 +1411,7 @@
%
The basic simpset for intuitionistic \FOL{} is
\ttindexbold{FOL_basic_ss}. It preprocess rewrites using {\tt
- gen_all}, \texttt{atomize} and \texttt{mk_meta_eq}. It solves simplified
+ gen_all}, \texttt{atomize} and \texttt{mk_eq}. It solves simplified
subgoals using \texttt{triv_rls} and assumptions, and by detecting
contradictions. It uses \ttindex{asm_simp_tac} to tackle subgoals of
conditional rewrites.
@@ -1385,8 +1434,7 @@
addsimprocs [defALL_regroup, defEX_regroup]
setSSolver safe_solver
setSolver unsafe_solver
- setmksimps (map mk_meta_eq o
- atomize o gen_all);
+ setmksimps (map mk_eq o atomize o gen_all);
val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps {\at}
int_ex_simps {\at} int_all_simps)
@@ -1401,42 +1449,33 @@
effect for conjunctions.
-\subsection{Case splitting}
+\subsection{Splitter setup}\index{simplification!setting up the splitter}
-To set up case splitting, we must prove the theorem \texttt{meta_iffD}
-below and pass it to \ttindexbold{mk_case_split_tac}. The tactic
-\ttindexbold{split_tac} uses \texttt{mk_meta_eq}, defined above, to
-convert the splitting rules to meta-equalities.
+To set up case splitting, we have to call the \ML{} functor \ttindex{
+SplitterFun}, which takes the argument signature \texttt{SPLITTER_DATA}.
+So we prove the theorem \texttt{meta_eq_to_iff} below and store it, together
+with the \texttt{mk_eq} function described above and several standard
+theorems, in the structure \texttt{SplitterData}. Calling the functor with
+this data yields a new instantiation of the splitter for our logic.
\begin{ttbox}
-val meta_iffD =
- prove_goal FOL.thy "[| P==Q; Q |] ==> P"
- (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1])
+val meta_eq_to_iff = prove_goal IFOL.thy "x==y ==> x<->y"
+ (fn [prem] => [rewtac prem, rtac iffI 1, atac 1, atac 1]);
\ttbreak
-fun split_tac splits =
- mk_case_split_tac meta_iffD (map mk_meta_eq splits);
-\end{ttbox}
-%
-The splitter replaces applications of a given function; the right-hand side
-of the replacement can be anything. For example, here is a splitting rule
-for conditional expressions:
-\[ \Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp (\Var{Q} \imp \Var{P}(\Var{x}))
-\conj (\lnot\Var{Q} \imp \Var{P}(\Var{y}))
-\]
-Another example is the elimination operator (which happens to be
-called~$split$) for Cartesian products:
-\[ \Var{P}(split(\Var{f},\Var{p})) \bimp (\forall a~b. \Var{p} =
-\langle a,b\rangle \imp \Var{P}(\Var{f}(a,b)))
-\]
-Case splits should be allowed only when necessary; they are expensive
-and hard to control. Here is an example of use, where \texttt{expand_if}
-is the first rule above:
-\begin{ttbox}
-by (simp_tac (simpset() addloop (split_tac [expand_if])) 1);
-\end{ttbox}
-Users would usually prefer the following shortcut using
-\ttindex{addsplits}:
-\begin{ttbox}
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+structure SplitterData =
+ struct
+ structure Simplifier = Simplifier
+ val mk_eq = mk_eq
+ val meta_eq_to_iff = meta_eq_to_iff
+ val iffD = iffD2
+ val disjE = disjE
+ val conjE = conjE
+ val exE = exE
+ val contrapos = contrapos
+ val contrapos2 = contrapos2
+ val notnotD = notnotD
+ end;
+\ttbreak
+structure Splitter = SplitterFun(SplitterData);
\end{ttbox}