--- a/doc-src/IsarImplementation/Thy/Eq.thy Mon Aug 27 16:48:41 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,85 +0,0 @@
-theory Eq
-imports Base
-begin
-
-chapter {* Equational reasoning *}
-
-text {* Equality is one of the most fundamental concepts of
- mathematics. The Isabelle/Pure logic (\chref{ch:logic}) provides a
- builtin relation @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> 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
- @{text "\<lambda>"}-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.
-*}
-
-
-section {* Basic equality rules \label{sec:eq-rules} *}
-
-text {* FIXME *}
-
-
-section {* Conversions \label{sec:conv} *}
-
-text {* FIXME *}
-
-
-section {* Rewriting \label{sec:rewriting} *}
-
-text {* Rewriting normalizes a given term (theorem or goal) by
- replacing instances of given equalities @{text "t \<equiv> u"} in subterms.
- Rewriting continues until no rewrites are applicable to any subterm.
- This may be used to unfold simple definitions of the form @{text "f
- x\<^sub>1 \<dots> x\<^sub>n \<equiv> u"}, but is slightly more general than that.
-*}
-
-text %mlref {*
- \begin{mldecls}
- @{index_ML rewrite_rule: "thm list -> thm -> thm"} \\
- @{index_ML rewrite_goals_rule: "thm list -> thm -> thm"} \\
- @{index_ML rewrite_goal_tac: "thm list -> int -> tactic"} \\
- @{index_ML rewrite_goals_tac: "thm list -> tactic"} \\
- @{index_ML fold_goals_tac: "thm list -> tactic"} \\
- \end{mldecls}
-
- \begin{description}
-
- \item @{ML rewrite_rule}~@{text "rules thm"} rewrites the whole
- theorem by the given rules.
-
- \item @{ML rewrite_goals_rule}~@{text "rules thm"} 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}).
-
- \item @{ML rewrite_goal_tac}~@{text "rules i"} rewrites subgoal
- @{text "i"} by the given rewrite rules.
-
- \item @{ML rewrite_goals_tac}~@{text "rules"} rewrites all subgoals
- by the given rewrite rules.
-
- \item @{ML fold_goals_tac}~@{text "rules"} essentially uses @{ML
- rewrite_goals_tac} with the symmetric form of each member of @{text
- "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