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 \Equational reasoning\  wenzelm@46295  6 wenzelm@58618  7 text \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 "\ :: \ \ \ \ 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 "\"}-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 \  wenzelm@46295  30 wenzelm@46295  31 wenzelm@58618  32 section \Basic equality rules \label{sec:eq-rules}\  wenzelm@46295  33 wenzelm@58618  34 text \Isabelle/Pure uses @{text "\"} 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 "\  wenzelm@50085  37  :: \ \ \ \ 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 \ u"} to one  wenzelm@50085  46  stating @{text "u \ 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 "\\"}-conversion) and lifting of @{text  wenzelm@58618  53  "\/\"} contexts.\  wenzelm@50085  54 wenzelm@58618  55 text %mlref \  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 "\"} and  wenzelm@50085  68  @{text "\"} conversions. Note that @{text "\"} conversion is  wenzelm@50085  69  implicit due to the representation of terms with de-Bruijn indices  wenzelm@58618  70  (\secref{sec:terms}).\  wenzelm@46295  71 wenzelm@46295  72 wenzelm@58618  73 section \Conversions \label{sec:conv}\  wenzelm@46295  74 wenzelm@58618  75 text \  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 \  wenzelm@46295  81 wenzelm@46295  82 wenzelm@58618  83 section \Rewriting \label{sec:rewriting}\  wenzelm@46295  84 wenzelm@58618  85 text \Rewriting normalizes a given term (theorem or goal) by  wenzelm@46295  86  replacing instances of given equalities @{text "t \ 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 \ x\<^sub>n \ u"}, but is slightly more general than that.  wenzelm@58618  90 \  wenzelm@46295  91 wenzelm@58618  92 text %mlref \  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 \  wenzelm@46295  125 wenzelm@46295  126 end