--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/document/Eq.tex Thu Feb 09 19:34:23 2012 +0100
@@ -0,0 +1,135 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Eq}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Eq\isanewline
+\isakeyword{imports}\ Base\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Equational reasoning%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Equality is one of the most fundamental concepts of
+ mathematics. The Isabelle/Pure logic (\chref{ch:logic}) provides a
+ builtin relation \isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop} that expresses equality
+ of arbitrary terms (or propositions) at the framework level, as
+ expressed by certain basic inference rules (\secref{sec:eq-rules}).
+
+ Equational reasoning means to replace equals by equals, using
+ reflexivity and transitivity to form chains of replacement steps,
+ and congruence rules to access sub-structures. Conversions
+ (\secref{sec:conv}) provide a convenient framework to compose basic
+ equational steps to build specific equational reasoning tools.
+
+ Higher-order matching is able to provide suitable instantiations for
+ giving equality rules, which leads to the versatile concept of
+ \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-term rewriting (\secref{sec:rewriting}). Internally
+ this is based on the general-purpose Simplifier engine of Isabelle,
+ which is more specific and more efficient than plain conversions.
+
+ Object-logics usually introduce specific notions of equality or
+ equivalence, and relate it with the Pure equality. This enables to
+ re-use the Pure tools for equational reasoning for particular
+ object-logic connectives as well.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Basic equality rules \label{sec:eq-rules}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Conversions \label{sec:conv}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Rewriting \label{sec:rewriting}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Rewriting normalizes a given term (theorem or goal) by
+ replacing instances of given equalities \isa{t\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ u} in subterms.
+ Rewriting continues until no rewrites are applicable to any subterm.
+ This may be used to unfold simple definitions of the form \isa{f\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ u}, but is slightly more general than that.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexdef{}{ML}{rewrite\_goal\_tac}\verb|rewrite_goal_tac: thm list -> int -> tactic| \\
+ \indexdef{}{ML}{rewrite\_goals\_tac}\verb|rewrite_goals_tac: thm list -> tactic| \\
+ \indexdef{}{ML}{fold\_goals\_tac}\verb|fold_goals_tac: thm list -> tactic| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|rewrite_goal_tac|~\isa{rules\ i} rewrites subgoal
+ \isa{i} by the given rewrite rules.
+
+ \item \verb|rewrite_goals_tac|~\isa{rules} rewrites all subgoals
+ by the given rewrite rules.
+
+ \item \verb|fold_goals_tac|~\isa{rules} essentially uses \verb|rewrite_goals_tac| with the symmetric form of each member of \isa{rules}, re-ordered to fold longer expression first. This supports
+ to idea to fold primitive definitions that appear in expended form
+ in the proof state.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: