author nipkow Thu Sep 14 17:46:00 2000 +0200 (2000-09-14) changeset 9958 67f2920862c7 child 10186 499637e8f2c6 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

   118 *}

   119

   120 subsubsection{*Higher-order patterns*}

   121

   122 subsubsection{*Local assumptions*}

   123

   124 subsubsection{*The preprocessor*}

   125

   126 text{*

   127 \index{simplification|)}

   128 *}

   129 (*<*)

   130 end

   131 (*>*)