author  wenzelm 
Mon, 07 Oct 2013 21:24:44 +0200  
changeset 54313  da2e6282a4f5 
parent 48985  5386df44a037 
child 56059  2390391584c2 
permissions  rwrr 
48895  1 
(*<*)theory Even imports Main begin 
2 
ML_file "../../antiquote_setup.ML" 

3 
setup Antiquote_Setup.setup 

43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42637
diff
changeset

4 
(*>*) 
23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

5 

9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

6 
section{* The Set of Even Numbers *} 
10314  7 

23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

8 
text {* 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

9 
\index{even numbers!defining inductively(}% 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

10 
The set of even numbers can be inductively defined as the least set 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

11 
containing 0 and closed under the operation $+2$. Obviously, 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

12 
\emph{even} can also be expressed using the divides relation (@{text dvd}). 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

13 
We shall prove below that the two formulations coincide. On the way we 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

14 
shall examine the primary means of reasoning about inductively defined 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

15 
sets: rule induction. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

16 
*} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

17 

9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

18 
subsection{* Making an Inductive Definition *} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

19 

9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

20 
text {* 
23928  21 
Using \commdx{inductive\protect\_set}, we declare the constant @{text even} to be 
23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

22 
a set of natural numbers with the desired properties. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

23 
*} 
10314  24 

25330  25 
inductive_set even :: "nat set" where 
26 
zero[intro!]: "0 \<in> even"  

27 
step[intro!]: "n \<in> even \<Longrightarrow> (Suc (Suc n)) \<in> even" 

10314  28 

23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

29 
text {* 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

30 
An inductive definition consists of introduction rules. The first one 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

31 
above states that 0 is even; the second states that if $n$ is even, then so 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

32 
is~$n+2$. Given this declaration, Isabelle generates a fixed point 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

33 
definition for @{term even} and proves theorems about it, 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

34 
thus following the definitional approach (see {\S}\ref{sec:definitional}). 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

35 
These theorems 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

36 
include the introduction rules specified in the declaration, an elimination 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

37 
rule for case analysis and an induction rule. We can refer to these 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

38 
theorems by automaticallygenerated names. Here are two examples: 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

39 
@{named_thms[display,indent=0] even.zero[no_vars] (even.zero) even.step[no_vars] (even.step)} 
10314  40 

23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

41 
The introduction rules can be given attributes. Here 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

42 
both rules are specified as \isa{intro!},% 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

43 
\index{intro"!@\isa {intro"!} (attribute)} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

44 
directing the classical reasoner to 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

45 
apply them aggressively. Obviously, regarding 0 as even is safe. The 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

46 
@{text step} rule is also safe because $n+2$ is even if and only if $n$ is 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

47 
even. We prove this equivalence later. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

48 
*} 
10314  49 

23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

50 
subsection{*Using Introduction Rules*} 
10314  51 

23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

52 
text {* 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

53 
Our first lemma states that numbers of the form $2\times k$ are even. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

54 
Introduction rules are used to show that specific values belong to the 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

55 
inductive set. Such proofs typically involve 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

56 
induction, perhaps over some other inductive set. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

57 
*} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

58 

11705  59 
lemma two_times_even[intro!]: "2*k \<in> even" 
12328  60 
apply (induct_tac k) 
23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

61 
apply auto 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

62 
done 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

63 
(*<*) 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

64 
lemma "2*k \<in> even" 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

65 
apply (induct_tac k) 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

66 
(*>*) 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

67 
txt {* 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

68 
\noindent 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

69 
The first step is induction on the natural number @{text k}, which leaves 
10883  70 
two subgoals: 
71 
@{subgoals[display,indent=0,margin=65]} 

23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

72 
Here @{text auto} simplifies both subgoals so that they match the introduction 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

73 
rules, which are then applied automatically. 
10314  74 

23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

75 
Our ultimate goal is to prove the equivalence between the traditional 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

76 
definition of @{text even} (using the divides relation) and our inductive 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

77 
definition. One direction of this equivalence is immediate by the lemma 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

78 
just proved, whose @{text "intro!"} attribute ensures it is applied automatically. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

79 
*} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

80 
(*<*)oops(*>*) 
11705  81 
lemma dvd_imp_even: "2 dvd n \<Longrightarrow> n \<in> even" 
10883  82 
by (auto simp add: dvd_def) 
10314  83 

23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

84 
subsection{* Rule Induction \label{sec:ruleinduction} *} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

85 

9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

86 
text {* 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

87 
\index{rule induction(}% 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

88 
From the definition of the set 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

89 
@{term even}, Isabelle has 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

90 
generated an induction rule: 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

91 
@{named_thms [display,indent=0,margin=40] even.induct [no_vars] (even.induct)} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

92 
A property @{term P} holds for every even number provided it 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

93 
holds for~@{text 0} and is closed under the operation 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

94 
\isa{Suc(Suc \(\cdot\))}. Then @{term P} is closed under the introduction 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

95 
rules for @{term even}, which is the least set closed under those rules. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

96 
This type of inductive argument is called \textbf{rule induction}. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

97 

9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

98 
Apart from the double application of @{term Suc}, the induction rule above 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

99 
resembles the familiar mathematical induction, which indeed is an instance 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

100 
of rule induction; the natural numbers can be defined inductively to be 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

101 
the least set containing @{text 0} and closed under~@{term Suc}. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

102 

9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

103 
Induction is the usual way of proving a property of the elements of an 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

104 
inductively defined set. Let us prove that all members of the set 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

105 
@{term even} are multiples of two. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

106 
*} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

107 

11705  108 
lemma even_imp_dvd: "n \<in> even \<Longrightarrow> 2 dvd n" 
23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

109 
txt {* 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

110 
We begin by applying induction. Note that @{text even.induct} has the form 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

111 
of an elimination rule, so we use the method @{text erule}. We get two 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

112 
subgoals: 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

113 
*} 
10314  114 
apply (erule even.induct) 
23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

115 
txt {* 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

116 
@{subgoals[display,indent=0]} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

117 
We unfold the definition of @{text dvd} in both subgoals, proving the first 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

118 
one and simplifying the second: 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

119 
*} 
10883  120 
apply (simp_all add: dvd_def) 
23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

121 
txt {* 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

122 
@{subgoals[display,indent=0]} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

123 
The next command eliminates the existential quantifier from the assumption 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

124 
and replaces @{text n} by @{text "2 * k"}. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

125 
*} 
10314  126 
apply clarify 
23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

127 
txt {* 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

128 
@{subgoals[display,indent=0]} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

129 
To conclude, we tell Isabelle that the desired value is 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

130 
@{term "Suc k"}. With this hint, the subgoal falls to @{text simp}. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

131 
*} 
10883  132 
apply (rule_tac x = "Suc k" in exI, simp) 
23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

133 
(*<*)done(*>*) 
10314  134 

23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

135 
text {* 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

136 
Combining the previous two results yields our objective, the 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

137 
equivalence relating @{term even} and @{text dvd}. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

138 
% 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

139 
%we don't want [iff]: discuss? 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

140 
*} 
10314  141 

11705  142 
theorem even_iff_dvd: "(n \<in> even) = (2 dvd n)" 
10883  143 
by (blast intro: dvd_imp_even even_imp_dvd) 
10314  144 

23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

145 

9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

146 
subsection{* Generalization and Rule Induction \label{sec:genruleinduction} *} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

147 

9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

148 
text {* 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

149 
\index{generalizing for induction}% 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

150 
Before applying induction, we typically must generalize 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

151 
the induction formula. With rule induction, the required generalization 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

152 
can be hard to find and sometimes requires a complete reformulation of the 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

153 
problem. In this example, our first attempt uses the obvious statement of 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

154 
the result. It fails: 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

155 
*} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

156 

9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

157 
lemma "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> even" 
10314  158 
apply (erule even.induct) 
159 
oops 

23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

160 
(*<*) 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

161 
lemma "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> even" 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

162 
apply (erule even.induct) 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

163 
(*>*) 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

164 
txt {* 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

165 
Rule induction finds no occurrences of @{term "Suc(Suc n)"} in the 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

166 
conclusion, which it therefore leaves unchanged. (Look at 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

167 
@{text even.induct} to see why this happens.) We have these subgoals: 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

168 
@{subgoals[display,indent=0]} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

169 
The first one is hopeless. Rule induction on 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

170 
a nonvariable term discards information, and usually fails. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

171 
How to deal with such situations 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

172 
in general is described in {\S}\ref{sec:indvarinprems} below. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

173 
In the current case the solution is easy because 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

174 
we have the necessary inverse, subtraction: 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

175 
*} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

176 
(*<*)oops(*>*) 
11705  177 
lemma even_imp_even_minus_2: "n \<in> even \<Longrightarrow> n  2 \<in> even" 
10314  178 
apply (erule even.induct) 
23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

179 
apply auto 
10314  180 
done 
23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

181 
(*<*) 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

182 
lemma "n \<in> even \<Longrightarrow> n  2 \<in> even" 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

183 
apply (erule even.induct) 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

184 
(*>*) 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

185 
txt {* 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

186 
This lemma is trivially inductive. Here are the subgoals: 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

187 
@{subgoals[display,indent=0]} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

188 
The first is trivial because @{text "0  2"} simplifies to @{text 0}, which is 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

189 
even. The second is trivial too: @{term "Suc (Suc n)  2"} simplifies to 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

190 
@{term n}, matching the assumption.% 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

191 
\index{rule induction)} %the sequel isn't really about induction 
10314  192 

23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

193 
\medskip 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

194 
Using our lemma, we can easily prove the result we originally wanted: 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

195 
*} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

196 
(*<*)oops(*>*) 
10883  197 
lemma Suc_Suc_even_imp_even: "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> even" 
198 
by (drule even_imp_even_minus_2, simp) 

10326  199 

23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

200 
text {* 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

201 
We have just proved the converse of the introduction rule @{text even.step}. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

202 
This suggests proving the following equivalence. We give it the 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

203 
\attrdx{iff} attribute because of its obvious value for simplification. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

204 
*} 
10326  205 

206 
lemma [iff]: "((Suc (Suc n)) \<in> even) = (n \<in> even)" 

10883  207 
by (blast dest: Suc_Suc_even_imp_even) 
10314  208 

23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

209 

9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

210 
subsection{* Rule Inversion \label{sec:ruleinversion} *} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

211 

9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

212 
text {* 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

213 
\index{rule inversion(}% 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

214 
Case analysis on an inductive definition is called \textbf{rule 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

215 
inversion}. It is frequently used in proofs about operational 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

216 
semantics. It can be highly effective when it is applied 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

217 
automatically. Let us look at how rule inversion is done in 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

218 
Isabelle/HOL\@. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

219 

9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

220 
Recall that @{term even} is the minimal set closed under these two rules: 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

221 
@{thm [display,indent=0] even.intros [no_vars]} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

222 
Minimality means that @{term even} contains only the elements that these 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

223 
rules force it to contain. If we are told that @{term a} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

224 
belongs to 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

225 
@{term even} then there are only two possibilities. Either @{term a} is @{text 0} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

226 
or else @{term a} has the form @{term "Suc(Suc n)"}, for some suitable @{term n} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

227 
that belongs to 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

228 
@{term even}. That is the gist of the @{term cases} rule, which Isabelle proves 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

229 
for us when it accepts an inductive definition: 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

230 
@{named_thms [display,indent=0,margin=40] even.cases [no_vars] (even.cases)} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

231 
This general rule is less useful than instances of it for 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

232 
specific patterns. For example, if @{term a} has the form 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

233 
@{term "Suc(Suc n)"} then the first case becomes irrelevant, while the second 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

234 
case tells us that @{term n} belongs to @{term even}. Isabelle will generate 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

235 
this instance for us: 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

236 
*} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

237 

9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

238 
inductive_cases Suc_Suc_cases [elim!]: "Suc(Suc n) \<in> even" 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

239 

9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

240 
text {* 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

241 
The \commdx{inductive\protect\_cases} command generates an instance of 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

242 
the @{text cases} rule for the supplied pattern and gives it the supplied name: 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

243 
@{named_thms [display,indent=0] Suc_Suc_cases [no_vars] (Suc_Suc_cases)} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

244 
Applying this as an elimination rule yields one case where @{text even.cases} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

245 
would yield two. Rule inversion works well when the conclusions of the 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

246 
introduction rules involve datatype constructors like @{term Suc} and @{text "#"} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

247 
(list ``cons''); freeness reasoning discards all but one or two cases. 
10314  248 

23842
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

249 
In the \isacommand{inductive\_cases} command we supplied an 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

250 
attribute, @{text "elim!"}, 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

251 
\index{elim"!@\isa {elim"!} (attribute)}% 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

252 
indicating that this elimination rule can be 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

253 
applied aggressively. The original 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

254 
@{term cases} rule would loop if used in that manner because the 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

255 
pattern~@{term a} matches everything. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

256 

9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

257 
The rule @{text Suc_Suc_cases} is equivalent to the following implication: 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

258 
@{term [display,indent=0] "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> even"} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

259 
Just above we devoted some effort to reaching precisely 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

260 
this result. Yet we could have obtained it by a oneline declaration, 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

261 
dispensing with the lemma @{text even_imp_even_minus_2}. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

262 
This example also justifies the terminology 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

263 
\textbf{rule inversion}: the new rule inverts the introduction rule 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

264 
@{text even.step}. In general, a rule can be inverted when the set of elements 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

265 
it introduces is disjoint from those of the other introduction rules. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

266 

9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

267 
For oneoff applications of rule inversion, use the \methdx{ind_cases} method. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

268 
Here is an example: 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

269 
*} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

270 

9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

271 
(*<*)lemma "Suc(Suc n) \<in> even \<Longrightarrow> P"(*>*) 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

272 
apply (ind_cases "Suc(Suc n) \<in> even") 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

273 
(*<*)oops(*>*) 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

274 

9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

275 
text {* 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

276 
The specified instance of the @{text cases} rule is generated, then applied 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

277 
as an elimination rule. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

278 

9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

279 
To summarize, every inductive definition produces a @{text cases} rule. The 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

280 
\commdx{inductive\protect\_cases} command stores an instance of the 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

281 
@{text cases} rule for a given pattern. Within a proof, the 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

282 
@{text ind_cases} method applies an instance of the @{text cases} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

283 
rule. 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

284 

9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

285 
The even numbers example has shown how inductive definitions can be 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

286 
used. Later examples will show that they are actually worth using.% 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

287 
\index{rule inversion)}% 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

288 
\index{even numbers!defining inductively)} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

289 
*} 
9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

290 

9d87177f1f89
LaTeX code is now generated directly from theory file.
berghofe
parents:
23733
diff
changeset

291 
(*<*)end(*>*) 