(*:maxLineLen=78:*)
theory Eq
imports Base
begin
chapter \<open>Equational reasoning\<close>
text \<open>
Equality is one of the most fundamental concepts of mathematics. The
Isabelle/Pure logic (\chref{ch:logic}) provides a builtin relation \<open>\<equiv> :: \<alpha> \<Rightarrow>
\<alpha> \<Rightarrow> prop\<close> 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 \<open>\<lambda>\<close>-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.
\<close>
section \<open>Basic equality rules \label{sec:eq-rules}\<close>
text \<open>
Isabelle/Pure uses \<open>\<equiv>\<close> for equality of arbitrary terms, which includes
equivalence of propositions of the logical framework. The conceptual
axiomatization of the constant \<open>\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop\<close> is given in
\figref{fig:pure-equality}. The inference kernel presents slightly different
equality rules, which may be understood as derived rules from this minimal
axiomatization. The Pure theory also provides some theorems that express the
same reasoning schemes as theorems that can be composed like object-level
rules as explained in \secref{sec:obj-rules}.
For example, \<^ML>\<open>Thm.symmetric\<close> as Pure inference is an ML function that
maps a theorem \<open>th\<close> stating \<open>t \<equiv> u\<close> to one stating \<open>u \<equiv> t\<close>. In contrast,
@{thm [source] Pure.symmetric} as Pure theorem expresses the same reasoning
in declarative form. If used like \<open>th [THEN Pure.symmetric]\<close> in Isar source
notation, it achieves a similar effect as the ML inference function,
although the rule attribute @{attribute THEN} or ML operator \<^ML>\<open>op RS\<close>
involve the full machinery of higher-order unification (modulo
\<open>\<beta>\<eta>\<close>-conversion) and lifting of \<open>\<And>/\<Longrightarrow>\<close> contexts.
\<close>
text %mlref \<open>
\begin{mldecls}
@{define_ML Thm.reflexive: "cterm -> thm"} \\
@{define_ML Thm.symmetric: "thm -> thm"} \\
@{define_ML Thm.transitive: "thm -> thm -> thm"} \\
@{define_ML Thm.abstract_rule: "string -> cterm -> thm -> thm"} \\
@{define_ML Thm.combination: "thm -> thm -> thm"} \\[0.5ex]
@{define_ML Thm.equal_intr: "thm -> thm -> thm"} \\
@{define_ML Thm.equal_elim: "thm -> thm -> thm"} \\
\end{mldecls}
See also \<^file>\<open>~~/src/Pure/thm.ML\<close> for further description of these inference
rules, and a few more for primitive \<open>\<beta>\<close> and \<open>\<eta>\<close> conversions. Note that \<open>\<alpha>\<close>
conversion is implicit due to the representation of terms with de-Bruijn
indices (\secref{sec:terms}).
\<close>
section \<open>Conversions \label{sec:conv}\<close>
text \<open>
The classic article \<^cite>\<open>"paulson:1983"\<close> introduces the concept of
conversion for Cambridge LCF. This was historically important to implement
all kinds of ``simplifiers'', but the Isabelle Simplifier is done quite
differently, see \<^cite>\<open>\<open>\S9.3\<close> in "isabelle-isar-ref"\<close>.
\<close>
text %mlref \<open>
\begin{mldecls}
@{define_ML_structure Conv} \\
@{define_ML_type conv} \\
@{define_ML Simplifier.asm_full_rewrite : "Proof.context -> conv"} \\
\end{mldecls}
\<^descr> \<^ML_structure>\<open>Conv\<close> is a library of combinators to build conversions,
over type \<^ML_type>\<open>conv\<close> (see also \<^file>\<open>~~/src/Pure/conv.ML\<close>). This is one
of the few Isabelle/ML modules that are usually used with \<^verbatim>\<open>open\<close>: finding
examples works by searching for ``\<^verbatim>\<open>open Conv\<close>'' instead of ``\<^verbatim>\<open>Conv.\<close>''.
\<^descr> \<^ML>\<open>Simplifier.asm_full_rewrite\<close> invokes the Simplifier as a
conversion. There are a few related operations, corresponding to the various
modes of simplification.
\<close>
section \<open>Rewriting \label{sec:rewriting}\<close>
text \<open>
Rewriting normalizes a given term (theorem or goal) by replacing instances
of given equalities \<open>t \<equiv> u\<close> in subterms. Rewriting continues until no
rewrites are applicable to any subterm. This may be used to unfold simple
definitions of the form \<open>f x\<^sub>1 \<dots> x\<^sub>n \<equiv> u\<close>, but is slightly more general than
that. \<close>
text %mlref \<open>
\begin{mldecls}
@{define_ML rewrite_rule: "Proof.context -> thm list -> thm -> thm"} \\
@{define_ML rewrite_goals_rule: "Proof.context -> thm list -> thm -> thm"} \\
@{define_ML rewrite_goal_tac: "Proof.context -> thm list -> int -> tactic"} \\
@{define_ML rewrite_goals_tac: "Proof.context -> thm list -> tactic"} \\
@{define_ML fold_goals_tac: "Proof.context -> thm list -> tactic"} \\
\end{mldecls}
\<^descr> \<^ML>\<open>rewrite_rule\<close>~\<open>ctxt rules thm\<close> rewrites the whole theorem by the
given rules.
\<^descr> \<^ML>\<open>rewrite_goals_rule\<close>~\<open>ctxt rules thm\<close> rewrites the outer premises of
the given theorem. Interpreting the same as a goal state
(\secref{sec:tactical-goals}) it means to rewrite all subgoals (in the same
manner as \<^ML>\<open>rewrite_goals_tac\<close>).
\<^descr> \<^ML>\<open>rewrite_goal_tac\<close>~\<open>ctxt rules i\<close> rewrites subgoal \<open>i\<close> by the given
rewrite rules.
\<^descr> \<^ML>\<open>rewrite_goals_tac\<close>~\<open>ctxt rules\<close> rewrites all subgoals by the given
rewrite rules.
\<^descr> \<^ML>\<open>fold_goals_tac\<close>~\<open>ctxt rules\<close> essentially uses \<^ML>\<open>rewrite_goals_tac\<close>
with the symmetric form of each member of \<open>rules\<close>, re-ordered to fold longer
expression first. This supports to idea to fold primitive definitions that
appear in expended form in the proof state.
\<close>
end