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