doc-src/TutorialI/Advanced/simp.thy
author nipkow
Wed Oct 11 09:09:06 2000 +0200 (2000-10-11)
changeset 10186 499637e8f2c6
parent 9958 67f2920862c7
child 10281 9554ce1c2e54
permissions -rw-r--r--
*** empty log message ***
     1 (*<*)
     2 theory simp = Main:
     3 (*>*)
     4 
     5 section{*Simplification*}
     6 
     7 text{*\label{sec:simplification-II}\index{simplification|(}
     8 This section discusses some additional nifty features not covered so far and
     9 gives a short introduction to the simplification process itself. The latter
    10 is helpful to understand why a particular rule does or does not apply in some
    11 situation.
    12 *}
    13 
    14 subsection{*Advanced features*}
    15 
    16 subsubsection{*Congruence rules*}
    17 
    18 text{*\label{sec:simp-cong}
    19 It is hardwired into the simplifier that while simplifying the conclusion $Q$
    20 of $P \isasymImp Q$ it is legal to make uses of the assumptions $P$. This
    21 kind of contextual information can also be made available for other
    22 operators. For example, @{prop"xs = [] --> xs@xs = xs"} simplifies to @{term
    23 True} because we may use @{prop"xs = []"} when simplifying @{prop"xs@xs =
    24 xs"}. The generation of contextual information during simplification is
    25 controlled by so-called \bfindex{congruence rules}. This is the one for
    26 @{text"\<longrightarrow>"}:
    27 @{thm[display]imp_cong[no_vars]}
    28 It should be read as follows:
    29 In order to simplify @{prop"P-->Q"} to @{prop"P'-->Q'"},
    30 simplify @{prop P} to @{prop P'}
    31 and assume @{prop"P'"} when simplifying @{prop Q} to @{prop"Q'"}.
    32 
    33 Here are some more examples.  The congruence rules for bounded
    34 quantifiers supply contextual information about the bound variable:
    35 @{thm[display,eta_contract=false,margin=60]ball_cong[no_vars]}
    36 The congruence rule for conditional expressions supply contextual
    37 information for simplifying the arms:
    38 @{thm[display]if_cong[no_vars]}
    39 A congruence rule can also \emph{prevent} simplification of some arguments.
    40 Here is an alternative congruence rule for conditional expressions:
    41 @{thm[display]if_weak_cong[no_vars]}
    42 Only the first argument is simplified; the others remain unchanged.
    43 This makes simplification much faster and is faithful to the evaluation
    44 strategy in programming languages, which is why this is the default
    45 congruence rule for @{text if}. Analogous rules control the evaluaton of
    46 @{text case} expressions.
    47 
    48 You can delare your own congruence rules with the attribute @{text cong},
    49 either globally, in the usual manner,
    50 \begin{quote}
    51 \isacommand{declare} \textit{theorem-name} @{text"[cong]"}
    52 \end{quote}
    53 or locally in a @{text"simp"} call by adding the modifier
    54 \begin{quote}
    55 @{text"cong:"} \textit{list of theorem names}
    56 \end{quote}
    57 The effect is reversed by @{text"cong del"} instead of @{text cong}.
    58 
    59 \begin{warn}
    60 The congruence rule @{thm[source]conj_cong}
    61 @{thm[display]conj_cong[no_vars]}
    62 is occasionally useful but not a default rule; you have to use it explicitly.
    63 \end{warn}
    64 *}
    65 
    66 subsubsection{*Permutative rewrite rules*}
    67 
    68 text{*
    69 \index{rewrite rule!permutative|bold}
    70 \index{rewriting!ordered|bold}
    71 \index{ordered rewriting|bold}
    72 \index{simplification!ordered|bold}
    73 An equation is a \bfindex{permutative rewrite rule} if the left-hand
    74 side and right-hand side are the same up to renaming of variables.  The most
    75 common permutative rule is commutativity: @{prop"x+y = y+x"}.  Other examples
    76 include @{prop"(x-y)-z = (x-z)-y"} in arithmetic and @{prop"insert x (insert
    77 y A) = insert y (insert x A)"} for sets. Such rules are problematic because
    78 once they apply, they can be used forever. The simplifier is aware of this
    79 danger and treats permutative rules by means of a special strategy, called
    80 \bfindex{ordered rewriting}: a permutative rewrite
    81 rule is only applied if the term becomes ``smaller'' (w.r.t.\ some fixed
    82 lexicographic ordering on terms). For example, commutativity rewrites
    83 @{term"b+a"} to @{term"a+b"}, but then stops because @{term"a+b"} is strictly
    84 smaller than @{term"b+a"}.  Permutative rewrite rules can be turned into
    85 simplification rules in the usual manner via the @{text simp} attribute; the
    86 simplifier recognizes their special status automatically.
    87 
    88 Permutative rewrite rules are most effective in the case of
    89 associative-commutative operators.  (Associativity by itself is not
    90 permutative.)  When dealing with an AC-operator~$f$, keep the
    91 following points in mind:
    92 \begin{itemize}\index{associative-commutative operators}
    93   
    94 \item The associative law must always be oriented from left to right,
    95   namely $f(f(x,y),z) = f(x,f(y,z))$.  The opposite orientation, if
    96   used with commutativity, can lead to nontermination.
    97 
    98 \item To complete your set of rewrite rules, you must add not just
    99   associativity~(A) and commutativity~(C) but also a derived rule, {\bf
   100     left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
   101 \end{itemize}
   102 Ordered rewriting with the combination of A, C, and LC sorts a term
   103 lexicographically:
   104 \[\def\maps#1{~\stackrel{#1}{\leadsto}~}
   105  f(f(b,c),a) \maps{A} f(b,f(c,a)) \maps{C} f(b,f(a,c)) \maps{LC} f(a,f(b,c)) \]
   106 
   107 Note that ordered rewriting for @{text"+"} and @{text"*"} on numbers is rarely
   108 necessary because the builtin arithmetic capabilities often take care of
   109 this.
   110 *}
   111 
   112 subsection{*How it works*}
   113 
   114 text{*\label{sec:SimpHow}
   115 Roughly speaking, the simplifier proceeds bottom-up (subterms are simplified
   116 first) and a conditional equation is only applied if its condition could be
   117 proved (again by simplification). Below we explain some special features of the rewriting process.
   118 *}
   119 
   120 subsubsection{*Higher-order patterns*}
   121 
   122 text{*\index{simplification rule|(}
   123 So far we have pretended the simplifier can deal with arbitrary
   124 rewrite rules. This is not quite true.  Due to efficiency (and
   125 potentially also computability) reasons, the simplifier expects the
   126 left-hand side of each rule to be a so-called \emph{higher-order
   127 pattern}~\cite{nipkow-patterns}\indexbold{higher-order
   128 pattern}\indexbold{pattern, higher-order}. This restricts where
   129 unknowns may occur.  Higher-order patterns are terms in $\beta$-normal
   130 form (this will always be the case unless you have done something
   131 strange) where each occurrence of an unknown is of the form
   132 $\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound
   133 variables. Thus all ``standard'' rewrite rules, where all unknowns are
   134 of base type, for example @{thm add_assoc}, are OK: if an unknown is
   135 of base type, it cannot have any arguments. Additionally, the rule
   136 @{text"(\<forall>x. ?P x \<and> ?Q x) = ((\<forall>x. ?P x) \<and> (\<forall>x. ?Q x))"} is also OK, in
   137 both directions: all arguments of the unknowns @{text"?P"} and
   138 @{text"?Q"} are distinct bound variables.
   139 
   140 If the left-hand side is not a higher-order pattern, not all is lost
   141 and the simplifier will still try to apply the rule, but only if it
   142 matches ``directly'', i.e.\ without much $\lambda$-calculus hocus
   143 pocus. For example, @{text"?f ?x \<in> range ?f = True"} rewrites
   144 @{term"g a \<in> range g"} to @{term True}, but will fail to match
   145 @{text"g(h b) \<in> range(\<lambda>x. g(h x))"}.  However, you can
   146 replace the offending subterms (in our case @{text"?f ?x"}, which
   147 is not a pattern) by adding new variables and conditions: @{text"?y =
   148 ?f ?x \<Longrightarrow> ?y \<in> range ?f = True"} is fine
   149 as a conditional rewrite rule since conditions can be arbitrary
   150 terms. However, this trick is not a panacea because the newly
   151 introduced conditions may be hard to prove, which has to take place
   152 before the rule can actually be applied.
   153   
   154 There is basically no restriction on the form of the right-hand
   155 sides.  They may not contain extraneous term or type variables, though.
   156 *}
   157 
   158 subsubsection{*The preprocessor*}
   159 
   160 text{*
   161 When some theorem is declared a simplification rule, it need not be a
   162 conditional equation already.  The simplifier will turn it into a set of
   163 conditional equations automatically.  For example, given @{prop"f x =
   164 g x & h x = k x"} the simplifier will turn this into the two separate
   165 simplifiction rules @{prop"f x = g x"} and @{prop"h x = k x"}. In
   166 general, the input theorem is converted as follows:
   167 \begin{eqnarray}
   168 \neg P &\mapsto& P = False \nonumber\\
   169 P \longrightarrow Q &\mapsto& P \Longrightarrow Q \nonumber\\
   170 P \land Q &\mapsto& P,\ Q \nonumber\\
   171 \forall x.~P~x &\mapsto& P~\Var{x}\nonumber\\
   172 \forall x \in A.\ P~x &\mapsto& \Var{x} \in A \Longrightarrow P~\Var{x} \nonumber\\
   173 @{text if}\ P\ @{text then}\ Q\ @{text else}\ R &\mapsto&
   174  P \Longrightarrow Q,\ \neg P \Longrightarrow R \nonumber
   175 \end{eqnarray}
   176 Once this conversion process is finished, all remaining non-equations
   177 $P$ are turned into trivial equations $P = True$.
   178 For example, the formula @{prop"(p \<longrightarrow> q \<and> r) \<and> s"} is converted into the three rules
   179 \begin{center}
   180 @{prop"p \<Longrightarrow> q = True"},\quad  @{prop"p \<Longrightarrow> r = True"},\quad  @{prop"s = True"}.
   181 \end{center}
   182 \index{simplification rule|)}
   183 \index{simplification|)}
   184 *}
   185 (*<*)
   186 end
   187 (*>*)