diff -r 0c32a609fcad -r a0bdee64194c doc-src/Ref/simplifier.tex --- a/doc-src/Ref/simplifier.tex Thu Feb 05 10:26:16 1998 +0100 +++ b/doc-src/Ref/simplifier.tex Thu Feb 05 10:26:59 1998 +0100 @@ -91,13 +91,13 @@ by (Asm_simp_tac 1); \end{ttbox} -\medskip {\tt Asm_full_simp_tac} is the most powerful of this quartet +\medskip \texttt{Asm_full_simp_tac} is the most powerful of this quartet of tactics but may also loop where some of the others terminate. For example, \begin{ttbox} {\out 1. ALL x. f x = g (f (g x)) ==> f 0 = f 0 + 0} \end{ttbox} -is solved by {\tt Simp_tac}, but {\tt Asm_simp_tac} and {\tt +is solved by \texttt{Simp_tac}, but \texttt{Asm_simp_tac} and {\tt Asm_simp_tac} loop because the rewrite rule $f\,\Var{x} = g\,(f\,(g\,\Var{x}))$ extracted from the assumption does not terminate. Isabelle notices certain simple forms of nontermination, @@ -366,10 +366,10 @@ \begin{ttdescription} -\item[$ss$ \ttindexbold{addsimprocs} $procs$] adds simplification +\item[$ss$ \ttindexbold{addsimprocs} $procs$] adds the simplification procedures $procs$ to the current simpset. -\item[$ss$ \ttindexbold{delsimprocs} $procs$] deletes simplification +\item[$ss$ \ttindexbold{delsimprocs} $procs$] deletes the simplification procedures $procs$ from the current simpset. \end{ttdescription} @@ -505,7 +505,7 @@ The solver is a pair of tactics that attempt to solve a subgoal after simplification. Typically it just proves trivial subgoals such as -{\tt True} and $t=t$. It could use sophisticated means such as {\tt +\texttt{True} and $t=t$. It could use sophisticated means such as {\tt blast_tac}, though that could make simplification expensive. Rewriting does not instantiate unknowns. For example, rewriting @@ -564,7 +564,7 @@ the solver. For this reason, solver tactics must be prepared to solve goals of the form $t = \Var{x}$, usually by reflexivity. In particular, reflexivity should be tried before any of the fancy -tactics like {\tt blast_tac}. +tactics like \texttt{blast_tac}. It may even happen that due to simplification the subgoal is no longer an equality. For example $False \bimp \Var{Q}$ could be rewritten to @@ -846,7 +846,7 @@ {\out val prem = "f(Suc(?n)) = Suc(f(?n))} {\out [!!n. f(Suc(n)) = Suc(f(n))]" : thm} \end{ttbox} -In the theorem~{\tt prem}, note that $f$ is a free variable while +In the theorem~\texttt{prem}, note that $f$ is a free variable while $\Var{n}$ is a schematic variable. \begin{ttbox} by (res_inst_tac [("n","i")] induct 1); @@ -958,7 +958,7 @@ \item To complete your set of rewrite rules, you must add not just associativity~(A) and commutativity~(C) but also a derived rule, {\bf - left-commutativity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$. + left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$. \end{itemize} Ordered rewriting with the combination of A, C, and~LC sorts a term lexicographically: @@ -973,14 +973,14 @@ This example is again set in \HOL\ (see \texttt{HOL/ex/NatSum}). Theory \thydx{Arith} contains natural numbers arithmetic. Its associated simpset contains many arithmetic laws including -distributivity of~$\times$ over~$+$, while {\tt add_ac} is a list +distributivity of~$\times$ over~$+$, while \texttt{add_ac} is a list consisting of the A, C and LC laws for~$+$ on type \texttt{nat}. Let us prove the theorem \[ \sum@{i=1}^n i = n\times(n+1)/2. \] % -A functional~{\tt sum} represents the summation operator under the -interpretation ${\tt sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$. We -extend {\tt Arith} as follows: +A functional~\texttt{sum} represents the summation operator under the +interpretation $\texttt{sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$. We +extend \texttt{Arith} as follows: \begin{ttbox} NatSum = Arith + consts sum :: [nat=>nat, nat] => nat @@ -997,7 +997,7 @@ Delsimprocs nat_cancel; Addsimps add_ac; \end{ttbox} -Our desired theorem now reads ${\tt sum} \, (\lambda i.i) \, (n+1) = +Our desired theorem now reads $\texttt{sum} \, (\lambda i.i) \, (n+1) = n\times(n+1)/2$. The Isabelle goal has both sides multiplied by~$2$: \begin{ttbox} goal NatSum.thy "2 * sum (\%i.i) (Suc n) = n * Suc n"; @@ -1032,7 +1032,7 @@ {\out 2 * sum (\%i. i) (Suc n) = n * Suc n} {\out No subgoals!} \end{ttbox} -Simplification cannot prove the induction step if we omit {\tt add_ac} from +Simplification cannot prove the induction step if we omit \texttt{add_ac} from the simpset. Observe that like terms have not been collected: \begin{ttbox} {\out Level 3} @@ -1050,7 +1050,7 @@ \subsection{Re-orienting equalities} -Ordered rewriting with the derived rule {\tt symmetry} can reverse +Ordered rewriting with the derived rule \texttt{symmetry} can reverse equations: \begin{ttbox} val symmetry = prove_goal HOL.thy "(x=y) = (y=x)" @@ -1058,16 +1058,16 @@ \end{ttbox} This is frequently useful. Assumptions of the form $s=t$, where $t$ occurs in the conclusion but not~$s$, can often be brought into the right form. -For example, ordered rewriting with {\tt symmetry} can prove the goal +For example, ordered rewriting with \texttt{symmetry} can prove the goal \[ f(a)=b \conj f(a)=c \imp b=c. \] -Here {\tt symmetry} reverses both $f(a)=b$ and $f(a)=c$ +Here \texttt{symmetry} reverses both $f(a)=b$ and $f(a)=c$ because $f(a)$ is lexicographically greater than $b$ and~$c$. These re-oriented equations, as rewrite rules, replace $b$ and~$c$ in the conclusion by~$f(a)$. Another example is the goal $\neg(t=u) \imp \neg(u=t)$. The differing orientations make this appear difficult to prove. Ordered -rewriting with {\tt symmetry} makes the equalities agree. (Without +rewriting with \texttt{symmetry} makes the equalities agree. (Without knowing more about~$t$ and~$u$ we cannot say whether they both go to $t=u$ or~$u=t$.) Then the simplifier can prove the goal outright. @@ -1126,7 +1126,8 @@ \begin{ttbox} local val lhss = - [read_cterm (sign_of Prod.thy) ("f::'a*'b=>'c", TVar (("'z", 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; @@ -1165,10 +1166,10 @@ use "$ISABELLE_HOME/src/Provers/splitter.ML"; \end{ttbox} -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 +Simplification requires converting 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 +\texttt{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)" @@ -1177,7 +1178,7 @@ particular logic. In Constructive Type Theory, equality is a ternary relation of the form $a=b\in A$; the type~$A$ determines the meaning of the equality essentially as a partial equivalence relation. The -present simplifier cannot be used. Rewriting in {\tt CTT} uses +present simplifier cannot be used. Rewriting in \texttt{CTT} uses another simplifier, which resides in the file {\tt Provers/typedsimp.ML} and is not documented. Even this does not work for later variants of Constructive Type Theory that use @@ -1198,7 +1199,7 @@ (IntPr.fast_tac 1) ])); \end{ttbox} The following rewrite rules about conjunction are a selection of those -proved on {\tt FOL/simpdata.ML}. Later, these will be supplied to the +proved on \texttt{FOL/simpdata.ML}. Later, these will be supplied to the standard simpset. \begin{ttbox} val conj_simps = map int_prove_fun @@ -1225,20 +1226,20 @@ setmksimps : simpset * (thm -> thm list) -> simpset \hfill{\bf infix 4} \end{ttbox} The next step is to define the function for preprocessing rewrite rules. -This will be installed by calling {\tt setmksimps} below. Preprocessing +This will be installed by calling \texttt{setmksimps} below. Preprocessing occurs whenever rewrite rules are added, whether by user command or automatically. Preprocessing involves extracting atomic rewrites at the object-level, then reflecting them to the meta-level. -To start, the function {\tt gen_all} strips any meta-level +To start, the function \texttt{gen_all} strips any meta-level 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 {\tt atomize} analyses a theorem in order to extract +The function \texttt{atomize} analyses a theorem in order to extract atomic rewrite rules. The head of all the patterns, matched by the -wildcard~{\tt _}, is the coercion function {\tt Trueprop}. +wildcard~\texttt{_}, is the coercion function \texttt{Trueprop}. \begin{ttbox} fun atomize th = case concl_of th of _ $ (Const("op &",_) $ _ $ _) => atomize(th RS conjunct1) \at @@ -1260,21 +1261,21 @@ \item Universal quantification: remove the quantifier, replacing the bound variable by a schematic variable, and extract rewrites from the body. -\item {\tt True} and {\tt False} contain no useful rewrites. +\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 {\tt ZF/simpdata.ML} for a sophisticated translation of +the file \texttt{ZF/simpdata.ML} for a sophisticated translation of set-theoretic formulae into rewrite rules. The simplified rewrites must now be converted into meta-equalities. The -rule {\tt eq_reflection} converts equality rewrites, while {\tt +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 -$P\equiv{\tt False}$, and any other theorem~$P$ is converted to -$P\equiv{\tt True}$. The rules {\tt iff_reflection_F} and {\tt +$P\equiv\texttt{False}$, and any other theorem~$P$ is converted to +$P\equiv\texttt{True}$. The rules \texttt{iff_reflection_F} and {\tt iff_reflection_T} accomplish this conversion. \begin{ttbox} val P_iff_F = int_prove_fun "~P ==> (P <-> False)"; @@ -1283,7 +1284,7 @@ val P_iff_T = int_prove_fun "P ==> (P <-> True)"; val iff_reflection_T = P_iff_T RS iff_reflection; \end{ttbox} -The function {\tt mk_meta_eq} converts a theorem to a meta-equality +The function \texttt{mk_meta_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 @@ -1292,13 +1293,13 @@ | _ $ (Const("Not",_)$_) => th RS iff_reflection_F | _ => th RS iff_reflection_T; \end{ttbox} -The three functions {\tt gen_all}, {\tt atomize} and {\tt mk_meta_eq} will -be composed together and supplied below to {\tt setmksimps}. +The three functions \texttt{gen_all}, \texttt{atomize} and \texttt{mk_meta_eq} will +be composed together and supplied below to \texttt{setmksimps}. \subsection{Making the initial simpset} -It is time to assemble these items. We open module {\tt Simplifier} +It is time to assemble these items. We open module \texttt{Simplifier} to gain direct access to its components. We define the infix operator \ttindex{addcongs} to insert congruence rules; given a list of theorems, it converts their conclusions into meta-equalities and @@ -1317,16 +1318,16 @@ fun ss addsplits splits = ss addloop (split_tac splits); \end{ttbox} -The list {\tt IFOL_simps} contains the default rewrite rules for -first-order logic. The first of these is the reflexive law expressed -as the equivalence $(a=a)\bimp{\tt True}$; the rewrite rule $a=a$ is +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 imp_simps \at iff_simps \at quant_simps; \end{ttbox} -The list {\tt triv_rls} contains trivial theorems for the solver. Any +The list \texttt{triv_rls} contains trivial theorems for the solver. Any subgoal that is simplified to one of these will be removed. \begin{ttbox} val notFalseI = int_prove_fun "~False"; @@ -1335,15 +1336,15 @@ % The basic simpset for intuitionistic \FOL{} is \ttindexbold{FOL_basic_ss}. It preprocess rewrites using {\tt - gen_all}, {\tt atomize} and {\tt mk_meta_eq}. It solves simplified -subgoals using {\tt triv_rls} and assumptions, and by detecting + gen_all}, \texttt{atomize} and \texttt{mk_meta_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 {\tt FOL_basic_ss} will inherit these items. +Other simpsets built from \texttt{FOL_basic_ss} will inherit these items. In particular, \ttindexbold{IFOL_ss}, which introduces {\tt IFOL_simps} as rewrite rules. \ttindexbold{FOL_ss} will later -extend {\tt IFOL_ss} with classical rewrite rules such as $\neg\neg +extend \texttt{IFOL_ss} with classical rewrite rules such as $\neg\neg P\bimp P$. \index{*setmksimps}\index{*setSSolver}\index{*setSolver}\index{*setsubgoaler} \index{*addsimps}\index{*addcongs} @@ -1355,20 +1356,22 @@ eq_assume_tac, ematch_tac [FalseE]]; val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac - addsimprocs [defALL_regroup,defEX_regroup] + addsimprocs [defALL_regroup, defEX_regroup] setSSolver safe_solver setSolver unsafe_solver - setmksimps (map mk_meta_eq o atomize o gen_all); + setmksimps (map mk_meta_eq o + atomize o gen_all); -val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps {\at} int_ex_simps {\at} int_all_simps) +val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps {\at} + int_ex_simps {\at} int_all_simps) addcongs [imp_cong]; \end{ttbox} -This simpset takes {\tt imp_cong} as a congruence rule in order to use +This simpset takes \texttt{imp_cong} as a congruence rule in order to use contextual information to simplify the conclusions of implications: \[ \List{\Var{P}\bimp\Var{P'};\; \Var{P'} \Imp \Var{Q}\bimp\Var{Q'}} \Imp (\Var{P}\imp\Var{Q}) \bimp (\Var{P'}\imp\Var{Q'}) \] -By adding the congruence rule {\tt conj_cong}, we could obtain a similar +By adding the congruence rule \texttt{conj_cong}, we could obtain a similar effect for conjunctions. @@ -1376,7 +1379,7 @@ 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 +\ttindexbold{split_tac} uses \texttt{mk_meta_eq}, defined above, to convert the splitting rules to meta-equalities. \begin{ttbox} val meta_iffD = @@ -1399,7 +1402,7 @@ \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 {\tt expand_if} +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);