author  wenzelm 
Sat, 05 Apr 2014 15:03:40 +0200  
changeset 56421  1ffd7eaa778b 
parent 54742  7a86358a3c0b 
permissions  rwrr 
46295  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:eqrules}). 

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 substructures. Conversions 

16 
(\secref{sec:conv}) provide a convenient framework to compose basic 

17 
equational steps to build specific equational reasoning tools. 

18 

19 
Higherorder 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 generalpurpose Simplifier engine of Isabelle, 

23 
which is more specific and more efficient than plain conversions. 

24 

25 
Objectlogics usually introduce specific notions of equality or 

26 
equivalence, and relate it with the Pure equality. This enables to 

27 
reuse the Pure tools for equational reasoning for particular 

28 
objectlogic connectives as well. 

29 
*} 

30 

31 

32 
section {* Basic equality rules \label{sec:eqrules} *} 

33 

50085  34 
text {* Isabelle/Pure uses @{text "\<equiv>"} for equality of arbitrary 
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:pureequality}. 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 objectlevel 

42 
rules as explained in \secref{sec:objrules}. 

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 higherorder 

52 
unification (modulo @{text "\<beta>\<eta>"}conversion) and lifting of @{text 

53 
"\<And>/\<Longrightarrow>"} contexts. *} 

54 

55 
text %mlref {* 

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 deBruijn indices 

70 
(\secref{sec:terms}). *} 

46295  71 

72 

73 
section {* Conversions \label{sec:conv} *} 

74 

50122  75 
text {* 
52422  76 
%FIXME 
50122  77 

78 
The classic article that introduces the concept of conversion (for 

79 
Cambridge LCF) is \cite{paulson:1983}. 

80 
*} 

46295  81 

82 

83 
section {* Rewriting \label{sec:rewriting} *} 

84 

85 
text {* Rewriting normalizes a given term (theorem or goal) by 

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. 

90 
*} 

91 

92 
text %mlref {* 

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:tacticalgoals}) 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"}, reordered 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} 

124 
*} 

125 

126 
end 