modernized section about congruence rules;
authorwenzelm
Sun Nov 27 12:52:52 2011 +0100 (2011-11-27)
changeset 456454014bc2a09ff
parent 45644 8634b4e61b88
child 45646 02afa20cf397
modernized section about congruence rules;
doc-src/IsarRef/Thy/Generic.thy
doc-src/IsarRef/Thy/document/Generic.tex
doc-src/Ref/simplifier.tex
     1.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Sat Nov 26 17:10:03 2011 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Sun Nov 27 12:52:52 2011 +0100
     1.3 @@ -399,8 +399,8 @@
     1.4    like @{text add}.
     1.5  
     1.6    \medskip The @{text cong} modifiers add or delete Simplifier
     1.7 -  congruence rules (see also \cite{isabelle-ref}), the default is to
     1.8 -  add.
     1.9 +  congruence rules (see also \secref{sec:simp-cong}), the default is
    1.10 +  to add.
    1.11  
    1.12    \medskip The @{text split} modifiers add or delete rules for the
    1.13    Splitter (see also \cite{isabelle-ref}), the default is to add.
    1.14 @@ -453,12 +453,11 @@
    1.15    \begin{matharray}{rcl}
    1.16      @{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    1.17      @{attribute_def simp} & : & @{text attribute} \\
    1.18 -    @{attribute_def cong} & : & @{text attribute} \\
    1.19      @{attribute_def split} & : & @{text attribute} \\
    1.20    \end{matharray}
    1.21  
    1.22    @{rail "
    1.23 -    (@@{attribute simp} | @@{attribute cong} | @@{attribute split}) (() | 'add' | 'del')
    1.24 +    (@@{attribute simp} | @@{attribute split}) (() | 'add' | 'del')
    1.25    "}
    1.26  
    1.27    \begin{description}
    1.28 @@ -469,14 +468,68 @@
    1.29  
    1.30    \item @{attribute simp} declares simplification rules.
    1.31  
    1.32 -  \item @{attribute cong} declares congruence rules.
    1.33 -
    1.34    \item @{attribute split} declares case split rules.
    1.35  
    1.36    \end{description}
    1.37  *}
    1.38  
    1.39  
    1.40 +subsection {* Congruence rules\label{sec:simp-cong} *}
    1.41 +
    1.42 +text {*
    1.43 +  \begin{matharray}{rcl}
    1.44 +    @{attribute_def cong} & : & @{text attribute} \\
    1.45 +  \end{matharray}
    1.46 +
    1.47 +  @{rail "
    1.48 +    @@{attribute cong} (() | 'add' | 'del')
    1.49 +  "}
    1.50 +
    1.51 +  \begin{description}
    1.52 +
    1.53 +  \item @{attribute cong} declares congruence rules to the Simplifier
    1.54 +  context.
    1.55 +
    1.56 +  \end{description}
    1.57 +
    1.58 +  Congruence rules are equalities of the form @{text [display]
    1.59 +  "\<dots> \<Longrightarrow> f ?x\<^sub>1 \<dots> ?x\<^sub>n = f ?y\<^sub>1 \<dots> ?y\<^sub>n"}
    1.60 +
    1.61 +  This controls the simplification of the arguments of @{text f}.  For
    1.62 +  example, some arguments can be simplified under additional
    1.63 +  assumptions: @{text [display] "?P\<^sub>1 \<longleftrightarrow> ?Q\<^sub>1 \<Longrightarrow> (?Q\<^sub>1 \<Longrightarrow> ?P\<^sub>2 \<longleftrightarrow> ?Q\<^sub>2) \<Longrightarrow>
    1.64 +  (?P\<^sub>1 \<longrightarrow> ?P\<^sub>2) \<longleftrightarrow> (?Q\<^sub>1 \<longrightarrow> ?Q\<^sub>2)"}
    1.65 +
    1.66 +  Given this rule, the simplifier assumes @{text "?Q\<^sub>1"} and extracts
    1.67 +  rewrite rules from it when simplifying @{text "?P\<^sub>2"}.  Such local
    1.68 +  assumptions are effective for rewriting formulae such as @{text "x =
    1.69 +  0 \<longrightarrow> y + x = y"}.
    1.70 +
    1.71 +  %FIXME
    1.72 +  %The local assumptions are also provided as theorems to the solver;
    1.73 +  %see \secref{sec:simp-solver} below.
    1.74 +
    1.75 +  \medskip The following congruence rule for bounded quantifiers also
    1.76 +  supplies contextual information --- about the bound variable:
    1.77 +  @{text [display] "(?A = ?B) \<Longrightarrow> (\<And>x. x \<in> ?B \<Longrightarrow> ?P x \<longleftrightarrow> ?Q x) \<Longrightarrow>
    1.78 +    (\<forall>x \<in> ?A. ?P x) \<longleftrightarrow> (\<forall>x \<in> ?B. ?Q x)"}
    1.79 +
    1.80 +  \medskip This congruence rule for conditional expressions can
    1.81 +  supply contextual information for simplifying the arms:
    1.82 +  @{text [display] "?p = ?q \<Longrightarrow> (?q \<Longrightarrow> ?a = ?c) \<Longrightarrow> (\<not> ?q \<Longrightarrow> ?b = ?d) \<Longrightarrow>
    1.83 +    (if ?p then ?a else ?b) = (if ?q then ?c else ?d)"}
    1.84 +
    1.85 +  A congruence rule can also \emph{prevent} simplification of some
    1.86 +  arguments.  Here is an alternative congruence rule for conditional
    1.87 +  expressions that conforms to non-strict functional evaluation:
    1.88 +  @{text [display] "?p = ?q \<Longrightarrow> (if ?p then ?a else ?b) = (if ?q then ?a else ?b)"}
    1.89 +
    1.90 +  Only the first argument is simplified; the others remain unchanged.
    1.91 +  This can make simplification much faster, but may require an extra
    1.92 +  case split over the condition @{text "?q"} to prove the goal.
    1.93 +*}
    1.94 +
    1.95 +
    1.96  subsection {* Simplification procedures *}
    1.97  
    1.98  text {* Simplification procedures are ML functions that produce proven
     2.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Sat Nov 26 17:10:03 2011 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Sun Nov 27 12:52:52 2011 +0100
     2.3 @@ -653,8 +653,8 @@
     2.4    like \isa{add}.
     2.5  
     2.6    \medskip The \isa{cong} modifiers add or delete Simplifier
     2.7 -  congruence rules (see also \cite{isabelle-ref}), the default is to
     2.8 -  add.
     2.9 +  congruence rules (see also \secref{sec:simp-cong}), the default is
    2.10 +  to add.
    2.11  
    2.12    \medskip The \isa{split} modifiers add or delete rules for the
    2.13    Splitter (see also \cite{isabelle-ref}), the default is to add.
    2.14 @@ -704,7 +704,6 @@
    2.15  \begin{matharray}{rcl}
    2.16      \indexdef{}{command}{print\_simpset}\hypertarget{command.print-simpset}{\hyperlink{command.print-simpset}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}simpset}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
    2.17      \indexdef{}{attribute}{simp}\hypertarget{attribute.simp}{\hyperlink{attribute.simp}{\mbox{\isa{simp}}}} & : & \isa{attribute} \\
    2.18 -    \indexdef{}{attribute}{cong}\hypertarget{attribute.cong}{\hyperlink{attribute.cong}{\mbox{\isa{cong}}}} & : & \isa{attribute} \\
    2.19      \indexdef{}{attribute}{split}\hypertarget{attribute.split}{\hyperlink{attribute.split}{\mbox{\isa{split}}}} & : & \isa{attribute} \\
    2.20    \end{matharray}
    2.21  
    2.22 @@ -713,8 +712,6 @@
    2.23  \rail@bar
    2.24  \rail@term{\hyperlink{attribute.simp}{\mbox{\isa{simp}}}}[]
    2.25  \rail@nextbar{1}
    2.26 -\rail@term{\hyperlink{attribute.cong}{\mbox{\isa{cong}}}}[]
    2.27 -\rail@nextbar{2}
    2.28  \rail@term{\hyperlink{attribute.split}{\mbox{\isa{split}}}}[]
    2.29  \rail@endbar
    2.30  \rail@bar
    2.31 @@ -735,14 +732,87 @@
    2.32  
    2.33    \item \hyperlink{attribute.simp}{\mbox{\isa{simp}}} declares simplification rules.
    2.34  
    2.35 -  \item \hyperlink{attribute.cong}{\mbox{\isa{cong}}} declares congruence rules.
    2.36 -
    2.37    \item \hyperlink{attribute.split}{\mbox{\isa{split}}} declares case split rules.
    2.38  
    2.39    \end{description}%
    2.40  \end{isamarkuptext}%
    2.41  \isamarkuptrue%
    2.42  %
    2.43 +\isamarkupsubsection{Congruence rules\label{sec:simp-cong}%
    2.44 +}
    2.45 +\isamarkuptrue%
    2.46 +%
    2.47 +\begin{isamarkuptext}%
    2.48 +\begin{matharray}{rcl}
    2.49 +    \indexdef{}{attribute}{cong}\hypertarget{attribute.cong}{\hyperlink{attribute.cong}{\mbox{\isa{cong}}}} & : & \isa{attribute} \\
    2.50 +  \end{matharray}
    2.51 +
    2.52 +  \begin{railoutput}
    2.53 +\rail@begin{3}{}
    2.54 +\rail@term{\hyperlink{attribute.cong}{\mbox{\isa{cong}}}}[]
    2.55 +\rail@bar
    2.56 +\rail@nextbar{1}
    2.57 +\rail@term{\isa{add}}[]
    2.58 +\rail@nextbar{2}
    2.59 +\rail@term{\isa{del}}[]
    2.60 +\rail@endbar
    2.61 +\rail@end
    2.62 +\end{railoutput}
    2.63 +
    2.64 +
    2.65 +  \begin{description}
    2.66 +
    2.67 +  \item \hyperlink{attribute.cong}{\mbox{\isa{cong}}} declares congruence rules to the Simplifier
    2.68 +  context.
    2.69 +
    2.70 +  \end{description}
    2.71 +
    2.72 +  Congruence rules are equalities of the form \begin{isabelle}%
    2.73 +{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ f\ {\isaliteral{3F}{\isacharquery}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3F}{\isacharquery}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{3F}{\isacharquery}}y\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3F}{\isacharquery}}y\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}%
    2.74 +\end{isabelle}
    2.75 +
    2.76 +  This controls the simplification of the arguments of \isa{f}.  For
    2.77 +  example, some arguments can be simplified under additional
    2.78 +  assumptions: \begin{isabelle}%
    2.79 +{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\isanewline
    2.80 +\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}%
    2.81 +\end{isabelle}
    2.82 +
    2.83 +  Given this rule, the simplifier assumes \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} and extracts
    2.84 +  rewrite rules from it when simplifying \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}.  Such local
    2.85 +  assumptions are effective for rewriting formulae such as \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ y\ {\isaliteral{2B}{\isacharplus}}\ x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequote}}}.
    2.86 +
    2.87 +  %FIXME
    2.88 +  %The local assumptions are also provided as theorems to the solver;
    2.89 +  %see \secref{sec:simp-solver} below.
    2.90 +
    2.91 +  \medskip The following congruence rule for bounded quantifiers also
    2.92 +  supplies contextual information --- about the bound variable:
    2.93 +  \begin{isabelle}%
    2.94 +{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}A\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{3F}{\isacharquery}}B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}P\ x\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\isanewline
    2.95 +\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{3F}{\isacharquery}}A{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{3F}{\isacharquery}}B{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}Q\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}%
    2.96 +\end{isabelle}
    2.97 +
    2.98 +  \medskip This congruence rule for conditional expressions can
    2.99 +  supply contextual information for simplifying the arms:
   2.100 +  \begin{isabelle}%
   2.101 +{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}p\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}a\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{3F}{\isacharquery}}q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}b\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}d{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\isanewline
   2.102 +\ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{3F}{\isacharquery}}p\ then\ {\isaliteral{3F}{\isacharquery}}a\ else\ {\isaliteral{3F}{\isacharquery}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{3F}{\isacharquery}}q\ then\ {\isaliteral{3F}{\isacharquery}}c\ else\ {\isaliteral{3F}{\isacharquery}}d{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}%
   2.103 +\end{isabelle}
   2.104 +
   2.105 +  A congruence rule can also \emph{prevent} simplification of some
   2.106 +  arguments.  Here is an alternative congruence rule for conditional
   2.107 +  expressions that conforms to non-strict functional evaluation:
   2.108 +  \begin{isabelle}%
   2.109 +{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}p\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{3F}{\isacharquery}}p\ then\ {\isaliteral{3F}{\isacharquery}}a\ else\ {\isaliteral{3F}{\isacharquery}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{3F}{\isacharquery}}q\ then\ {\isaliteral{3F}{\isacharquery}}a\ else\ {\isaliteral{3F}{\isacharquery}}b{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}%
   2.110 +\end{isabelle}
   2.111 +
   2.112 +  Only the first argument is simplified; the others remain unchanged.
   2.113 +  This can make simplification much faster, but may require an extra
   2.114 +  case split over the condition \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}q{\isaliteral{22}{\isachardoublequote}}} to prove the goal.%
   2.115 +\end{isamarkuptext}%
   2.116 +\isamarkuptrue%
   2.117 +%
   2.118  \isamarkupsubsection{Simplification procedures%
   2.119  }
   2.120  \isamarkuptrue%
     3.1 --- a/doc-src/Ref/simplifier.tex	Sat Nov 26 17:10:03 2011 +0100
     3.2 +++ b/doc-src/Ref/simplifier.tex	Sun Nov 27 12:52:52 2011 +0100
     3.3 @@ -336,75 +336,6 @@
     3.4  \index{rewrite rules|)}
     3.5  
     3.6  
     3.7 -\subsection{*Congruence rules}\index{congruence rules}\label{sec:simp-congs}
     3.8 -\begin{ttbox}
     3.9 -addcongs   : simpset * thm list -> simpset \hfill{\bf infix 4}
    3.10 -delcongs   : simpset * thm list -> simpset \hfill{\bf infix 4}
    3.11 -addeqcongs : simpset * thm list -> simpset \hfill{\bf infix 4}
    3.12 -deleqcongs : simpset * thm list -> simpset \hfill{\bf infix 4}
    3.13 -\end{ttbox}
    3.14 -
    3.15 -Congruence rules are meta-equalities of the form
    3.16 -\[ \dots \Imp
    3.17 -   f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}).
    3.18 -\]
    3.19 -This governs the simplification of the arguments of~$f$.  For
    3.20 -example, some arguments can be simplified under additional assumptions:
    3.21 -\[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}}
    3.22 -   \Imp (\Var{P@1} \imp \Var{P@2}) \equiv (\Var{Q@1} \imp \Var{Q@2})
    3.23 -\]
    3.24 -Given this rule, the simplifier assumes $Q@1$ and extracts rewrite
    3.25 -rules from it when simplifying~$P@2$.  Such local assumptions are
    3.26 -effective for rewriting formulae such as $x=0\imp y+x=y$.  The local
    3.27 -assumptions are also provided as theorems to the solver; see
    3.28 -{\S}~\ref{sec:simp-solver} below.
    3.29 -
    3.30 -\begin{ttdescription}
    3.31 -  
    3.32 -\item[$ss$ \ttindexbold{addcongs} $thms$] adds congruence rules to the
    3.33 -  simpset $ss$.  These are derived from $thms$ in an appropriate way,
    3.34 -  depending on the underlying object-logic.
    3.35 -  
    3.36 -\item[$ss$ \ttindexbold{delcongs} $thms$] deletes congruence rules
    3.37 -  derived from $thms$.
    3.38 -  
    3.39 -\item[$ss$ \ttindexbold{addeqcongs} $thms$] adds congruence rules in
    3.40 -  their internal form (conclusions using meta-equality) to simpset
    3.41 -  $ss$.  This is the basic mechanism that \texttt{addcongs} is built
    3.42 -  on.  It should be rarely used directly.
    3.43 -  
    3.44 -\item[$ss$ \ttindexbold{deleqcongs} $thms$] deletes congruence rules
    3.45 -  in internal form from simpset $ss$.
    3.46 -  
    3.47 -\end{ttdescription}
    3.48 -
    3.49 -\medskip
    3.50 -
    3.51 -Here are some more examples.  The congruence rule for bounded
    3.52 -quantifiers also supplies contextual information, this time about the
    3.53 -bound variable:
    3.54 -\begin{eqnarray*}
    3.55 -  &&\List{\Var{A}=\Var{B};\; 
    3.56 -          \Forall x. x\in \Var{B} \Imp \Var{P}(x) = \Var{Q}(x)} \Imp{} \\
    3.57 - &&\qquad\qquad
    3.58 -    (\forall x\in \Var{A}.\Var{P}(x)) = (\forall x\in \Var{B}.\Var{Q}(x))
    3.59 -\end{eqnarray*}
    3.60 -The congruence rule for conditional expressions can supply contextual
    3.61 -information for simplifying the arms:
    3.62 -\[ \List{\Var{p}=\Var{q};~ \Var{q} \Imp \Var{a}=\Var{c};~
    3.63 -         \neg\Var{q} \Imp \Var{b}=\Var{d}} \Imp
    3.64 -   if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{c},\Var{d})
    3.65 -\]
    3.66 -A congruence rule can also {\em prevent\/} simplification of some arguments.
    3.67 -Here is an alternative congruence rule for conditional expressions:
    3.68 -\[ \Var{p}=\Var{q} \Imp
    3.69 -   if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{a},\Var{b})
    3.70 -\]
    3.71 -Only the first argument is simplified; the others remain unchanged.
    3.72 -This can make simplification much faster, but may require an extra case split
    3.73 -to prove the goal.  
    3.74 -
    3.75 -
    3.76  \subsection{*The subgoaler}\label{sec:simp-subgoaler}
    3.77  \begin{ttbox}
    3.78  setsubgoaler :