author wenzelm Tue, 29 Aug 2000 00:54:22 +0200 changeset 9712 e33422a2eb9c parent 9711 75df6a20b0b3 child 9713 2c5b42311eb0
updated cong stuff;
--- a/doc-src/Ref/simplifier.tex	Tue Aug 29 00:53:48 2000 +0200
+++ b/doc-src/Ref/simplifier.tex	Tue Aug 29 00:54:22 2000 +0200
@@ -1256,10 +1256,10 @@
\section{*Setting up the Simplifier}\label{sec:setting-up-simp}
\index{simplification!setting up}

-Setting up the simplifier for new logics is complicated.  This section
-describes how the simplifier is installed for intuitionistic
-first-order logic; the code is largely taken from {\tt
-  FOL/simpdata.ML} of the Isabelle sources.
+Setting up the simplifier for new logics is complicated in the general case.
+This section describes how the simplifier is installed for intuitionistic
+first-order logic; the code is largely taken from {\tt FOL/simpdata.ML} of the
+Isabelle sources.

The simplifier and the case splitting tactic, which reside on separate files,
are not part of Pure Isabelle.  They must be loaded explicitly by the
@@ -1407,20 +1407,10 @@

\subsection{Making the initial simpset}

-It is time to assemble these items.  We define the infix operator
-\ttindex{addcongs} to insert congruence rules; given a list of
-theorems, it converts their conclusions into meta-equalities and
-\begin{ttbox}
-    ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
-\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.
+It is time to assemble these items.  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.
\begin{ttbox}
val IFOL_simps =
[refl RS P_iff_T] \at conj_simps \at disj_simps \at not_simps \at
@@ -1432,6 +1422,11 @@
val notFalseI = int_prove_fun "~False";
val triv_rls = [TrueI,refl,iff_refl,notFalseI];
\end{ttbox}
+We also define the function \ttindex{mk_meta_cong} to convert the conclusion
+of congruence rules into meta-equalities.
+\begin{ttbox}
+fun mk_meta_cong rl = standard (mk_meta_eq (mk_meta_prems rl));
+\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_eq}.
@@ -1453,12 +1448,13 @@
fun safe_solver prems = FIRST'[match_tac (triv_rls {\at} prems),
eq_assume_tac, ematch_tac [FalseE]];

-val FOL_basic_ss =
+val FOL_basic_ss =
empty_ss setsubgoaler asm_simp_tac
FOL_basic_ss addsimps (IFOL_simps {\at}