1 theory Eq |
|
2 imports Base |
|
3 begin |
|
4 |
|
5 chapter {* Equational reasoning *} |
|
6 |
|
7 text {* Equality is one of the most fundamental concepts of |
|
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. |
|
29 *} |
|
30 |
|
31 |
|
32 section {* Basic equality rules \label{sec:eq-rules} *} |
|
33 |
|
34 text {* FIXME *} |
|
35 |
|
36 |
|
37 section {* Conversions \label{sec:conv} *} |
|
38 |
|
39 text {* FIXME *} |
|
40 |
|
41 |
|
42 section {* Rewriting \label{sec:rewriting} *} |
|
43 |
|
44 text {* Rewriting normalizes a given term (theorem or goal) by |
|
45 replacing instances of given equalities @{text "t \<equiv> u"} in subterms. |
|
46 Rewriting continues until no rewrites are applicable to any subterm. |
|
47 This may be used to unfold simple definitions of the form @{text "f |
|
48 x\<^sub>1 \<dots> x\<^sub>n \<equiv> u"}, but is slightly more general than that. |
|
49 *} |
|
50 |
|
51 text %mlref {* |
|
52 \begin{mldecls} |
|
53 @{index_ML rewrite_rule: "thm list -> thm -> thm"} \\ |
|
54 @{index_ML rewrite_goals_rule: "thm list -> thm -> thm"} \\ |
|
55 @{index_ML rewrite_goal_tac: "thm list -> int -> tactic"} \\ |
|
56 @{index_ML rewrite_goals_tac: "thm list -> tactic"} \\ |
|
57 @{index_ML fold_goals_tac: "thm list -> tactic"} \\ |
|
58 \end{mldecls} |
|
59 |
|
60 \begin{description} |
|
61 |
|
62 \item @{ML rewrite_rule}~@{text "rules thm"} rewrites the whole |
|
63 theorem by the given rules. |
|
64 |
|
65 \item @{ML rewrite_goals_rule}~@{text "rules thm"} rewrites the |
|
66 outer premises of the given theorem. Interpreting the same as a |
|
67 goal state (\secref{sec:tactical-goals}) it means to rewrite all |
|
68 subgoals (in the same manner as @{ML rewrite_goals_tac}). |
|
69 |
|
70 \item @{ML rewrite_goal_tac}~@{text "rules i"} rewrites subgoal |
|
71 @{text "i"} by the given rewrite rules. |
|
72 |
|
73 \item @{ML rewrite_goals_tac}~@{text "rules"} rewrites all subgoals |
|
74 by the given rewrite rules. |
|
75 |
|
76 \item @{ML fold_goals_tac}~@{text "rules"} essentially uses @{ML |
|
77 rewrite_goals_tac} with the symmetric form of each member of @{text |
|
78 "rules"}, re-ordered to fold longer expression first. This supports |
|
79 to idea to fold primitive definitions that appear in expended form |
|
80 in the proof state. |
|
81 |
|
82 \end{description} |
|
83 *} |
|
84 |
|
85 end |
|