# HG changeset patch # User wenzelm # Date 884622360 -3600 # Node ID 03003b966e913552d38564322866e6408c62b019 # Parent e7a4683c0026c586bc264a146ee0fc9d6190836d tuned; diff -r e7a4683c0026 -r 03003b966e91 doc-src/Ref/ref.ind --- a/doc-src/Ref/ref.ind Mon Jan 12 16:56:39 1998 +0100 +++ b/doc-src/Ref/ref.ind Mon Jan 12 17:26:00 1998 +0100 @@ -53,7 +53,7 @@ \item {\tt AddSIs}, \bold{137} \item {\tt addSIs}, \bold{132} \item {\tt addSolver}, \bold{111} - \item {\tt addsplits}, \bold{112}, 125, 126 + \item {\tt addsplits}, \bold{112}, 124, 126 \item {\tt addss}, \bold{133}, 134 \item {\tt addSSolver}, \bold{111} \item {\tt all_tac}, \bold{31} @@ -168,7 +168,7 @@ \item {\tt compWrapper}, \bold{133} \item {\tt concl_of}, \bold{40} \item {\tt COND}, \bold{33} - \item congruence rules, 108 + \item congruence rules, 109 \item {\tt Const}, \bold{60}, 86, 96 \item {\tt Constant}, 83, 96 \item constants, \bold{60} @@ -413,7 +413,7 @@ \item meta-rules, \see{meta-rules}{1}, 42--48 \item {\tt METAHYPS}, 16, \bold{34} \item mixfix declarations, 52, 73--78 - \item {\tt mk_case_split_tac}, \bold{126} + \item {\tt mk_case_split_tac}, \bold{125} \item {\tt mk_simproc}, \bold{120} \item {\tt ML} section, 53, 95, 97 \item model checkers, 79 @@ -425,7 +425,7 @@ \indexspace \item name tokens, \bold{70} - \item {\tt nat_cancel}, \bold{121} + \item {\tt nat_cancel}, \bold{108} \item {\tt net_bimatch_tac}, \bold{25} \item {\tt net_biresolve_tac}, \bold{25} \item {\tt net_match_tac}, \bold{25} @@ -636,7 +636,7 @@ \item simplification, 103--126 \subitem forward rules, 113 \subitem from classical reasoner, 133 - \subitem setting up, 122 + \subitem setting up, 121 \subitem tactics, 112 \item simplification sets, 106 \item {\tt simplify}, 113 @@ -661,7 +661,7 @@ \item sort hypotheses, 41 \item sorts \subitem printing of, 4 - \item {\tt split_tac}, \bold{126} + \item {\tt split_tac}, \bold{125} \item {\tt ssubst} theorem, \bold{99} \item {\tt stac}, \bold{100} \item stamps, \bold{51}, 59 diff -r e7a4683c0026 -r 03003b966e91 doc-src/Ref/simplifier.tex --- a/doc-src/Ref/simplifier.tex Mon Jan 12 16:56:39 1998 +0100 +++ b/doc-src/Ref/simplifier.tex Mon Jan 12 17:26:00 1998 +0100 @@ -19,10 +19,11 @@ \label{sec:simp-for-dummies} Basic use of the simplifier is particularly easy because each theory -is equipped with an implicit {\em current - simpset}\index{simpset!current}. This provides sensible default -information in many cases. A suite of commands refer to the implicit -simpset of the current theory context. +is equipped with sensible default information controlling the rewrite +process --- namely the implicit {\em current + simpset}\index{simpset!current}. A suite of simple commands is +provided that refer to the implicit simpset of the current theory +context. \begin{warn} Make sure that you are working within the correct theory context. @@ -54,9 +55,9 @@ simplify each other or the actual goal). \item[\ttindexbold{Asm_full_simp_tac}] is like \verb$Asm_simp_tac$, - but also simplifies the assumptions one by one. Working from - \emph{left to right}, it uses each assumption in the simplification - of those following. + but also simplifies the assumptions one by one. Strictly working + from \emph{left to right}, it uses each assumption in the + simplification of those following. \item[set \ttindexbold{trace_simp};] makes the simplifier output internal operations. This includes rewrite steps, but also @@ -237,8 +238,9 @@ \item[\ttindexbold{merge_ss} ($ss@1$, $ss@2$)] merges simpsets $ss@1$ and $ss@2$ by building the union of their respective rewrite rules, simplification procedures and congruences. The other components - (tactics etc.) cannot be merged, though; they are simply inherited - from either simpset. + (tactics etc.) cannot be merged, though; they are taken from either + simpset\footnote{Actually from $ss@1$, but it would unwise to count + on that.}. \end{ttdescription} @@ -351,7 +353,8 @@ delsimprocs : simpset * simproc list -> simpset \end{ttbox} -Simplification procedures are {\ML} functions that may produce +Simplification procedures are {\ML} objects of abstract type +\texttt{simproc}. Basically they are just functions that may produce \emph{proven} rewrite rules on demand. They are associated with certain patterns that conceptually represent left-hand sides of equations; these are shown by \texttt{print_ss}. During its @@ -371,6 +374,19 @@ \end{ttdescription} +For example, simplification procedures \ttindexbold{nat_cancel} of +\texttt{HOL/Arith} cancel common summands and constant factors out of +several relations of sums over natural numbers. + +Consider the following goal, which after cancelling $a$ on both sides +contains a factor of $2$. Simplifying with the simpset of +\texttt{Arith.thy} will do the cancellation automatically: +\begin{ttbox} +{\out 1. x + a + x < y + y + 2 + a + a + a + a + a} +by (Simp_tac 1); +{\out 1. x < Suc (a + (a + y))} +\end{ttbox} + \subsection{*Congruence rules}\index{congruence rules}\label{sec:simp-congs} \begin{ttbox} @@ -683,17 +699,17 @@ asm_full_simplify : simpset -> thm -> thm \end{ttbox} -These are forward rules, simplifying theorems in a similar way as the -corresponding simplification tactics do. The forward rules affect the whole - - subgoals of a proof state. The -looper~/ solver process as described in \S\ref{sec:simp-looper} and -\S\ref{sec:simp-solver} does not apply here, though. +These functions provide \emph{forward} rules for simplification. +Their effect is analogous to the corresponding tactics described in +\S\ref{simp-tactics}, but affect the whole theorem instead of just a +certain subgoal. Also note that the looper~/ solver process as +described in \S\ref{sec:simp-looper} and \S\ref{sec:simp-solver} is +omitted in forward simplification. \begin{warn} Forward simplification should be used rarely in ordinary proof scripts. It as mainly intended to provide an internal interface to - the simplifier for ML coded special utilities. + the simplifier for special utilities. \end{warn} @@ -712,7 +728,7 @@ \Var{P}(Suc(x))} \Imp \Var{P}(\Var{n})$. \end{ttdescription} We augment the implicit simpset inherited from \texttt{Nat} with the -basic rewrite rules for natural numbers: +basic rewrite rules for addition of natural numbers: \begin{ttbox} Addsimps [add_0, add_Suc]; \end{ttbox} @@ -753,15 +769,16 @@ \subsection{An example of tracing} \index{tracing!of simplification|(}\index{*trace_simp} -Let us prove a similar result involving more complex terms. The two -equations together can be used to prove that addition is commutative. + +Let us prove a similar result involving more complex terms. We prove +that addition is commutative. \begin{ttbox} goal Nat.thy "m+Suc(n) = Suc(m+n)"; {\out Level 0} {\out m + Suc(n) = Suc(m + n)} {\out 1. m + Suc(n) = Suc(m + n)} \end{ttbox} -We again perform induction on~$m$ and get two subgoals: +Performing induction on~$m$ yields two subgoals: \begin{ttbox} by (res_inst_tac [("n","m")] induct 1); {\out Level 1} @@ -814,9 +831,11 @@ \end{ttbox} \index{tracing!of simplification|)} + \subsection{Free variables and simplification} -Here is a conjecture to be proved for an arbitrary function~$f$ satisfying -the law $f(Suc(\Var{n})) = Suc(f(\Var{n}))$: + +Here is a conjecture to be proved for an arbitrary function~$f$ +satisfying the law $f(Suc(\Var{n})) = Suc(f(\Var{n}))$: \begin{ttbox} val [prem] = goal Nat.thy "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)"; @@ -971,8 +990,11 @@ end \end{ttbox} The \texttt{primrec} declaration automatically adds rewrite rules for -\texttt{sum} to the default simpset. We now insert the AC-rules for~$+$: +\texttt{sum} to the default simpset. We now remove the +\texttt{nat_cancel} simplification procedures (in order not to spoil +the example) and insert the AC-rules for~$+$: \begin{ttbox} +Delsimprocs nat_cancel; Addsimps add_ac; \end{ttbox} Our desired theorem now reads ${\tt sum} \, (\lambda i.i) \, (n+1) = @@ -1028,8 +1050,8 @@ \subsection{Re-orienting equalities} -Ordered rewriting with the derived rule {\tt symmetry} can reverse equality -signs: +Ordered rewriting with the derived rule {\tt symmetry} can reverse +equations: \begin{ttbox} val symmetry = prove_goal HOL.thy "(x=y) = (y=x)" (fn _ => [Blast_tac 1]); @@ -1104,12 +1126,13 @@ \begin{ttbox} local val lhss = - [read_cterm (sign_of Prod.thy) ("f::'a*'b=>'c", TVar (("'a", 0), []))]; + [read_cterm (sign_of Prod.thy) ("f::'a*'b=>'c", TVar (("'z", 0), []))]; val rew = mk_meta_eq pair_eta_expand; \medskip fun proc _ _ (Abs _) = Some rew | proc _ _ _ = None; in - val pair_eta_expand_proc = Simplifier.mk_simproc "pair_eta_expand" lhss proc; + val pair_eta_expand_proc = + Simplifier.mk_simproc "pair_eta_expand" lhss proc; end; \end{ttbox} This is an example of using \texttt{pair_eta_expand_proc}: @@ -1126,26 +1149,6 @@ matching. Usually, procedures would do some more work, in particular prove particular theorems depending on the current redex. -For example, simplification procedures \ttindexbold{nat_cancel} of -\texttt{HOL/Arith} cancel common summands and constant factors out of -several relations of sums over natural numbers. - -Consider the following goal, which after cancelling $a$ on both sides -contains a factor of $2$. Simplifying with the simpset of -\texttt{Arith.thy} will do the cancellation automatically: -\begin{ttbox} -{\out 1. x + a + x < y + y + 2 + a + a + a + a + a} -by (Simp_tac 1); -{\out 1. x < Suc (a + (a + y))} -\end{ttbox} - -\medskip - -The {\ML} sources for these simplification procedures consist of a -generic part (files \texttt{cancel_sums.ML} and -\texttt{cancel_factor.ML} in \texttt{Provers/Arith}), and a -\texttt{HOL} specific part in \texttt{HOL/arith_data.ML}. - \section{*Setting up the simplifier}\label{sec:setting-up-simp} \index{simplification!setting up} @@ -1163,10 +1166,10 @@ use "$ISABELLE_HOME/src/Provers/splitter.ML"; \end{ttbox} -Simplification works by reducing various object-equalities to -meta-equality. It requires rules stating that equal terms and equivalent -formulae are also equal at the meta-level. The rule declaration part of -the file {\tt FOL/IFOL.thy} contains the two lines +Simplification requires reflecting various object-equalities to +meta-level rewrite rules. This demands rules stating that equal terms +and equivalent formulae are also equal at the meta-level. The rule +declaration part of the file {\tt FOL/IFOL.thy} contains the two lines \begin{ttbox}\index{*eq_reflection theorem}\index{*iff_reflection theorem} eq_reflection "(x=y) ==> (x==y)" iff_reflection "(P<->Q) ==> (P==Q)" @@ -1183,10 +1186,11 @@ \subsection{A collection of standard rewrite rules} -The file begins by proving lots of standard rewrite rules about the logical -connectives. These include cancellation and associative laws. To prove -them easily, it defines a function that echoes the desired law and then -supplies it the theorem prover for intuitionistic \FOL: + +We first prove lots of standard rewrite rules about the logical +connectives. These include cancellation and associative laws. We +define a function that echoes the desired law and then supplies it the +prover for intuitionistic \FOL: \begin{ttbox} fun int_prove_fun s = (writeln s; @@ -1370,10 +1374,11 @@ \subsection{Case splitting} -To set up case splitting, we must prove the theorem below and pass it to -\ttindexbold{mk_case_split_tac}. The tactic \ttindexbold{split_tac} uses -{\tt mk_meta_eq}, defined above, to convert the splitting rules to -meta-equalities. + +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 {\tt 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"