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