src/Doc/Implementation/Eq.thy

tuned;

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 Thm.symmetric} 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 "op RS"} 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}
  @{index_ML Thm.reflexive: "cterm -> thm"} \\
  @{index_ML Thm.symmetric: "thm -> thm"} \\
  @{index_ML Thm.transitive: "thm -> thm -> thm"} \\
  @{index_ML Thm.abstract_rule: "string -> cterm -> thm -> thm"} \\
  @{index_ML Thm.combination: "thm -> thm -> thm"} \\[0.5ex]
  @{index_ML Thm.equal_intr: "thm -> thm -> thm"} \\
  @{index_ML Thm.equal_elim: "thm -> thm -> thm"} \\
  \end{mldecls}

  See also @{file "~~/src/Pure/thm.ML" } 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>
  %FIXME

  The classic article that introduces the concept of conversion (for
  Cambridge LCF) is @{cite "paulson:1983"}.
\<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}
  @{index_ML rewrite_rule: "Proof.context -> thm list -> thm -> thm"} \\
  @{index_ML rewrite_goals_rule: "Proof.context -> thm list -> thm -> thm"} \\
  @{index_ML rewrite_goal_tac: "Proof.context -> thm list -> int -> tactic"} \\
  @{index_ML rewrite_goals_tac: "Proof.context -> thm list -> tactic"} \\
  @{index_ML fold_goals_tac: "Proof.context -> thm list -> tactic"} \\
  \end{mldecls}

  \<^descr> @{ML rewrite_rule}~\<open>ctxt rules thm\<close> rewrites the whole
  theorem by the given rules.

  \<^descr> @{ML rewrite_goals_rule}~\<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 rewrite_goals_tac}).

  \<^descr> @{ML rewrite_goal_tac}~\<open>ctxt rules i\<close> rewrites subgoal
  \<open>i\<close> by the given rewrite rules.

  \<^descr> @{ML rewrite_goals_tac}~\<open>ctxt rules\<close> rewrites all subgoals
  by the given rewrite rules.

  \<^descr> @{ML fold_goals_tac}~\<open>ctxt rules\<close> essentially uses @{ML
  rewrite_goals_tac} 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