src/Doc/Implementation/Eq.thy
author wenzelm
Wed Mar 25 11:39:52 2015 +0100 (2015-03-25)
changeset 59809 87641097d0f3
parent 58618 782f0b662cae
child 61439 2bf52eec4e8a
permissions -rw-r--r--
tuned signature;
wenzelm@46295
     1
theory Eq
wenzelm@46295
     2
imports Base
wenzelm@46295
     3
begin
wenzelm@46295
     4
wenzelm@58618
     5
chapter \<open>Equational reasoning\<close>
wenzelm@46295
     6
wenzelm@58618
     7
text \<open>Equality is one of the most fundamental concepts of
wenzelm@46295
     8
  mathematics.  The Isabelle/Pure logic (\chref{ch:logic}) provides a
wenzelm@46295
     9
  builtin relation @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} that expresses equality
wenzelm@46295
    10
  of arbitrary terms (or propositions) at the framework level, as
wenzelm@46295
    11
  expressed by certain basic inference rules (\secref{sec:eq-rules}).
wenzelm@46295
    12
wenzelm@46295
    13
  Equational reasoning means to replace equals by equals, using
wenzelm@46295
    14
  reflexivity and transitivity to form chains of replacement steps,
wenzelm@46295
    15
  and congruence rules to access sub-structures.  Conversions
wenzelm@46295
    16
  (\secref{sec:conv}) provide a convenient framework to compose basic
wenzelm@46295
    17
  equational steps to build specific equational reasoning tools.
wenzelm@46295
    18
wenzelm@46295
    19
  Higher-order matching is able to provide suitable instantiations for
wenzelm@46295
    20
  giving equality rules, which leads to the versatile concept of
wenzelm@46295
    21
  @{text "\<lambda>"}-term rewriting (\secref{sec:rewriting}).  Internally
wenzelm@46295
    22
  this is based on the general-purpose Simplifier engine of Isabelle,
wenzelm@46295
    23
  which is more specific and more efficient than plain conversions.
wenzelm@46295
    24
wenzelm@46295
    25
  Object-logics usually introduce specific notions of equality or
wenzelm@46295
    26
  equivalence, and relate it with the Pure equality.  This enables to
wenzelm@46295
    27
  re-use the Pure tools for equational reasoning for particular
wenzelm@46295
    28
  object-logic connectives as well.
wenzelm@58618
    29
\<close>
wenzelm@46295
    30
wenzelm@46295
    31
wenzelm@58618
    32
section \<open>Basic equality rules \label{sec:eq-rules}\<close>
wenzelm@46295
    33
wenzelm@58618
    34
text \<open>Isabelle/Pure uses @{text "\<equiv>"} for equality of arbitrary
wenzelm@50085
    35
  terms, which includes equivalence of propositions of the logical
wenzelm@50085
    36
  framework.  The conceptual axiomatization of the constant @{text "\<equiv>
wenzelm@50085
    37
  :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} is given in \figref{fig:pure-equality}.  The
wenzelm@50085
    38
  inference kernel presents slightly different equality rules, which
wenzelm@50085
    39
  may be understood as derived rules from this minimal axiomatization.
wenzelm@50085
    40
  The Pure theory also provides some theorems that express the same
wenzelm@50085
    41
  reasoning schemes as theorems that can be composed like object-level
wenzelm@50085
    42
  rules as explained in \secref{sec:obj-rules}.
wenzelm@50085
    43
wenzelm@50085
    44
  For example, @{ML Thm.symmetric} as Pure inference is an ML function
wenzelm@50085
    45
  that maps a theorem @{text "th"} stating @{text "t \<equiv> u"} to one
wenzelm@50085
    46
  stating @{text "u \<equiv> t"}.  In contrast, @{thm [source]
wenzelm@50085
    47
  Pure.symmetric} as Pure theorem expresses the same reasoning in
wenzelm@50085
    48
  declarative form.  If used like @{text "th [THEN Pure.symmetric]"}
wenzelm@50085
    49
  in Isar source notation, it achieves a similar effect as the ML
wenzelm@50085
    50
  inference function, although the rule attribute @{attribute THEN} or
wenzelm@50085
    51
  ML operator @{ML "op RS"} involve the full machinery of higher-order
wenzelm@50085
    52
  unification (modulo @{text "\<beta>\<eta>"}-conversion) and lifting of @{text
wenzelm@58618
    53
  "\<And>/\<Longrightarrow>"} contexts.\<close>
wenzelm@50085
    54
wenzelm@58618
    55
text %mlref \<open>
wenzelm@50085
    56
  \begin{mldecls}
wenzelm@50085
    57
  @{index_ML Thm.reflexive: "cterm -> thm"} \\
wenzelm@50085
    58
  @{index_ML Thm.symmetric: "thm -> thm"} \\
wenzelm@50085
    59
  @{index_ML Thm.transitive: "thm -> thm -> thm"} \\
wenzelm@50085
    60
  @{index_ML Thm.abstract_rule: "string -> cterm -> thm -> thm"} \\
wenzelm@50085
    61
  @{index_ML Thm.combination: "thm -> thm -> thm"} \\[0.5ex]
wenzelm@50085
    62
  @{index_ML Thm.equal_intr: "thm -> thm -> thm"} \\
wenzelm@50085
    63
  @{index_ML Thm.equal_elim: "thm -> thm -> thm"} \\
wenzelm@50085
    64
  \end{mldecls}
wenzelm@50085
    65
wenzelm@53982
    66
  See also @{file "~~/src/Pure/thm.ML" } for further description of
wenzelm@50085
    67
  these inference rules, and a few more for primitive @{text "\<beta>"} and
wenzelm@50085
    68
  @{text "\<eta>"} conversions.  Note that @{text "\<alpha>"} conversion is
wenzelm@50085
    69
  implicit due to the representation of terms with de-Bruijn indices
wenzelm@58618
    70
  (\secref{sec:terms}).\<close>
wenzelm@46295
    71
wenzelm@46295
    72
wenzelm@58618
    73
section \<open>Conversions \label{sec:conv}\<close>
wenzelm@46295
    74
wenzelm@58618
    75
text \<open>
wenzelm@52422
    76
  %FIXME
wenzelm@50122
    77
wenzelm@50122
    78
  The classic article that introduces the concept of conversion (for
wenzelm@58555
    79
  Cambridge LCF) is @{cite "paulson:1983"}.
wenzelm@58618
    80
\<close>
wenzelm@46295
    81
wenzelm@46295
    82
wenzelm@58618
    83
section \<open>Rewriting \label{sec:rewriting}\<close>
wenzelm@46295
    84
wenzelm@58618
    85
text \<open>Rewriting normalizes a given term (theorem or goal) by
wenzelm@46295
    86
  replacing instances of given equalities @{text "t \<equiv> u"} in subterms.
wenzelm@46295
    87
  Rewriting continues until no rewrites are applicable to any subterm.
wenzelm@46295
    88
  This may be used to unfold simple definitions of the form @{text "f
wenzelm@46295
    89
  x\<^sub>1 \<dots> x\<^sub>n \<equiv> u"}, but is slightly more general than that.
wenzelm@58618
    90
\<close>
wenzelm@46295
    91
wenzelm@58618
    92
text %mlref \<open>
wenzelm@46295
    93
  \begin{mldecls}
wenzelm@54742
    94
  @{index_ML rewrite_rule: "Proof.context -> thm list -> thm -> thm"} \\
wenzelm@54742
    95
  @{index_ML rewrite_goals_rule: "Proof.context -> thm list -> thm -> thm"} \\
wenzelm@54742
    96
  @{index_ML rewrite_goal_tac: "Proof.context -> thm list -> int -> tactic"} \\
wenzelm@54742
    97
  @{index_ML rewrite_goals_tac: "Proof.context -> thm list -> tactic"} \\
wenzelm@54742
    98
  @{index_ML fold_goals_tac: "Proof.context -> thm list -> tactic"} \\
wenzelm@46295
    99
  \end{mldecls}
wenzelm@46295
   100
wenzelm@46295
   101
  \begin{description}
wenzelm@46295
   102
wenzelm@54742
   103
  \item @{ML rewrite_rule}~@{text "ctxt rules thm"} rewrites the whole
wenzelm@46486
   104
  theorem by the given rules.
wenzelm@46486
   105
wenzelm@54742
   106
  \item @{ML rewrite_goals_rule}~@{text "ctxt rules thm"} rewrites the
wenzelm@46486
   107
  outer premises of the given theorem.  Interpreting the same as a
wenzelm@46486
   108
  goal state (\secref{sec:tactical-goals}) it means to rewrite all
wenzelm@46486
   109
  subgoals (in the same manner as @{ML rewrite_goals_tac}).
wenzelm@46486
   110
wenzelm@54742
   111
  \item @{ML rewrite_goal_tac}~@{text "ctxt rules i"} rewrites subgoal
wenzelm@46295
   112
  @{text "i"} by the given rewrite rules.
wenzelm@46295
   113
wenzelm@54742
   114
  \item @{ML rewrite_goals_tac}~@{text "ctxt rules"} rewrites all subgoals
wenzelm@46295
   115
  by the given rewrite rules.
wenzelm@46295
   116
wenzelm@54742
   117
  \item @{ML fold_goals_tac}~@{text "ctxt rules"} essentially uses @{ML
wenzelm@46295
   118
  rewrite_goals_tac} with the symmetric form of each member of @{text
wenzelm@46295
   119
  "rules"}, re-ordered to fold longer expression first.  This supports
wenzelm@46295
   120
  to idea to fold primitive definitions that appear in expended form
wenzelm@46295
   121
  in the proof state.
wenzelm@46295
   122
wenzelm@46295
   123
  \end{description}
wenzelm@58618
   124
\<close>
wenzelm@46295
   125
wenzelm@46295
   126
end