doc-src/Ref/simplifier.tex

 Delsimps    : thm list -> unit
 Addsimprocs : simproc list -> unit
 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}
 functions manipulate basic components of the associated current
 simpset.  Internally, all rewrite rules have to be expressed as

   procedures $procs$ from the current simpset.
   
 \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}
 
 When a new theory is built, its implicit simpset is initialized by the

 \end{warn}
 
 
 \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}
-\end{ttbox}
-
-The looper is a tactic that is applied after simplification, in case
+delsplits : simpset * thm list -> simpset \hfill{\bf infix 4}
+\end{ttbox}
+
+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
 reverse order.
 

 Another possibility is to apply an elimination rule on the
 assumptions.  More adventurous loopers could start an induction.
 
 \begin{ttdescription}
   
-\item[$ss$ \ttindexbold{setloop} $tacf$] installs $tacf$ as the looper
-  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{setloop} $tacf$] installs $tacf$ as the only looper
+  tactic of $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}
 \index{simplification!tactics}\index{tactics!simplification}
 \begin{ttbox}

 quantifiers from the front of the given theorem.  Usually there are none
 anyway.
 \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}.
 \begin{ttbox}
 fun atomize th = case concl_of th of 

   | _                               => [th];
 \end{ttbox}
 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
   iff_reflection} converts if-and-only-if rewrites.  The latter possibility
 can arise in two other ways: the negative theorem~$\neg P$ is converted to

 val iff_reflection_F = P_iff_F RS iff_reflection;
 \ttbreak
 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}
 
 It is time to assemble these items.  We define the infix operator

 \begin{ttbox}
 infix 4 addcongs;
 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
 expressed as the equivalence $(a=a)\bimp\texttt{True}$; the rewrite rule $a=a$ is
 clearly useless.

 val triv_rls = [TrueI,refl,iff_refl,notFalseI];
 \end{ttbox}
 %
 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.
 
 Other simpsets built from \texttt{FOL_basic_ss} will inherit these items.

 
 val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
                             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)
                            addcongs [imp_cong];
 \end{ttbox}

 \]
 By adding the congruence rule \texttt{conj_cong}, we could obtain a similar
 effect for conjunctions.
 
 
-\subsection{Case splitting}
-
-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.
-\begin{ttbox}
-val meta_iffD = 
-    prove_goal FOL.thy "[| P==Q; Q |] ==> P"
-        (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1])
+\subsection{Splitter setup}\index{simplification!setting up the splitter}
+
+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_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}
 
 
 \subsection{Theory setup}\index{simplification!setting up the theory}
 \begin{ttbox}\indexbold{*Simplifier.setup}\index{*setup!simplifier}