1 theory Ind_Examples |
1 theory Ind_Examples |
2 imports Main |
2 imports Main LaTeXsugar |
3 begin |
3 begin |
4 |
4 |
5 section{* Examples of inductive definitions *} |
5 section{* Examples of Inductive Definitions \label{sec:ind-examples} *} |
6 |
6 |
7 text {* |
7 text {* |
8 \label{sec:ind-examples} |
8 |
9 In this section, we will give three examples showing how to define inductive |
9 In this section, we will give three examples showing how to define inductive |
10 predicates by hand and prove characteristic properties such as introduction |
10 predicates by hand and prove characteristic properties such as introduction |
11 rules and an induction rule. From these examples, we will then figure out a |
11 rules and an induction rule. From these examples, we will then figure out a |
12 general method for defining inductive predicates, which will be described in |
12 general method for defining inductive predicates. It should be noted that |
13 \S\ref{sec:ind-general-method}. This description will serve as a basis for the |
13 our aim in this section is not to write proofs that are as beautiful as |
14 actual implementation to be developed in \S\ref{sec:ind-interface} -- \S\ref{sec:ind-proofs}. |
14 possible, but as close as possible to the ML code producing the proofs that |
15 It should be noted that our aim in this section is not to write proofs that |
15 we will develop later. As a first example, we consider the transitive |
16 are as beautiful as possible, but as close as possible to the ML code producing |
16 closure of a relation @{text R}. It is an inductive predicate characterized |
17 the proofs that we will develop later. |
17 by the two introduction rules |
18 As a first example, we consider the \emph{transitive closure} @{text "trcl R"} |
18 |
19 of a relation @{text R}. It is characterized by the following |
19 \begin{center} |
20 two introduction rules |
20 @{term[mode=Axiom] "trcl R x x"} \hspace{5mm} |
21 \[ |
21 @{term[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"} |
22 \begin{array}{l} |
22 \end{center} |
23 @{term "trcl R x x"} \\ |
23 |
24 @{term [mode=no_brackets] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"} |
24 (FIXME first rule should be an ``axiom'') |
25 \end{array} |
25 |
26 \] |
26 Note that the @{text trcl} predicate has two different kinds of parameters: the |
27 Note that the @{text trcl} predicate has two different kinds of parameters: the |
27 first parameter @{text R} stays \emph{fixed} throughout the definition, whereas |
28 first parameter @{text R} stays \emph{fixed} throughout the definition, whereas |
28 the second and third parameter changes in the ``recursive call''. |
29 the second and third parameter changes in the ``recursive call''. |
29 |
30 Since an inductively defined predicate is the \emph{least} predicate closed under |
30 Since an inductively defined predicate is the least predicate closed under |
31 a collection of introduction rules, we define the predicate @{text "trcl R x y"} in |
31 a collection of introduction rules, we define the predicate @{text "trcl R x y"} in |
32 such a way that it holds if and only if @{text "P x y"} holds for every predicate |
32 such a way that it holds if and only if @{text "P x y"} holds for every predicate |
33 @{text P} closed under the above rules. This gives rise to a definition containing |
33 @{text P} closed under the rules above. This gives rise to the definition |
34 a universal quantifier over the predicate @{text P}: |
34 *} |
35 *} |
35 |
36 |
36 definition "trcl R x y \<equiv> |
37 definition "trcl \<equiv> \<lambda>R x y. |
37 \<forall>P. (\<forall>x. P x x) \<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P x y" |
38 \<forall>P. (\<forall>x. P x x) \<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P x y" |
38 |
39 |
39 text {* |
40 text {* |
40 where we quantify over the predicate @{text P}. |
41 \noindent |
41 |
42 Since the predicate @{term "trcl R x y"} yields an element of the type of object |
42 Since the predicate @{term "trcl R x y"} yields an element of the type of object |
43 level truth values @{text bool}, the meta-level implications @{text "\<Longrightarrow>"} in the |
43 level truth values @{text bool}, the meta-level implications @{text "\<Longrightarrow>"} in the |
44 above introduction rules have to be converted to object-level implications |
44 above introduction rules have to be converted to object-level implications |
45 @{text "\<longrightarrow>"}. Moreover, we use object-level universal quantifiers @{text "\<forall>"} |
45 @{text "\<longrightarrow>"}. Moreover, we use object-level universal quantifiers @{text "\<forall>"} |
46 rather than meta-level universal quantifiers @{text "\<And>"} for quantifying over |
46 rather than meta-level universal quantifiers @{text "\<And>"} for quantifying over |
47 the variable parameters of the introduction rules. Isabelle already offers some |
47 the variable parameters of the introduction rules. Isabelle already offers some |
48 infrastructure for converting between meta-level and object-level connectives, |
48 infrastructure for converting between meta-level and object-level connectives, |
49 which we will use later on. |
49 which we will use later on. |
50 |
50 |
51 With this definition of the transitive closure, the proof of the (weak) induction |
51 With this definition of the transitive closure, the proof of the (weak) induction |
52 theorem is almost immediate. It suffices to convert all the meta-level connectives |
52 theorem is almost immediate. It suffices to convert all the meta-level connectives |
53 in the induction rule to object-level connectives using the @{text atomize} proof |
53 in the induction rule to object-level connectives using the @{text atomize} proof |
54 method, expand the definition of @{text trcl}, eliminate the universal quantifier |
54 method, expand the definition of @{text trcl}, eliminate the universal quantifier |
55 contained in it, and then solve the goal by assumption. |
55 contained in it, and then solve the goal by assumption. |
56 *} |
56 *} |
57 |
57 |
58 lemma trcl_induct: |
58 lemma trcl_induct: |
59 assumes trcl: "trcl R x y" |
59 assumes trcl: "trcl R x y" |
60 shows "(\<And>x. P x x) \<Longrightarrow> (\<And>x y z. R x y \<Longrightarrow> P y z \<Longrightarrow> P x z) \<Longrightarrow> P x y" |
60 shows "(\<And>x. P x x) \<Longrightarrow> (\<And>x y z. R x y \<Longrightarrow> P y z \<Longrightarrow> P x z) \<Longrightarrow> P x y" |
67 (*<*) |
67 (*<*) |
68 lemma "trcl R x x" |
68 lemma "trcl R x x" |
69 apply (unfold trcl_def) |
69 apply (unfold trcl_def) |
70 apply (rule allI impI)+ |
70 apply (rule allI impI)+ |
71 (*>*) |
71 (*>*) |
|
72 |
72 txt {* |
73 txt {* |
73 \noindent |
74 |
74 The above induction rule is \emph{weak} in the sense that the induction step may |
75 The above induction rule is \emph{weak} in the sense that the induction step may |
75 only be proved using the assumptions @{term "R x y"} and @{term "P y z"}, but not |
76 only be proved using the assumptions @{term "R x y"} and @{term "P y z"}, but not |
76 using the additional assumption \mbox{@{term "trcl R y z"}}. A stronger induction rule |
77 using the additional assumption \mbox{@{term "trcl R y z"}}. A stronger induction rule |
77 containing this additional assumption can be derived from the weaker one with the |
78 containing this additional assumption can be derived from the weaker one with the |
78 help of the introduction rules for @{text trcl}. |
79 help of the introduction rules for @{text trcl}. |
79 |
80 |
80 We now turn to the proofs of the introduction rules, which are slightly more complicated. |
81 We now turn to the proofs of the introduction rules, which are slightly more complicated. |
81 In order to prove the first introduction rule, we again unfold the definition and |
82 In order to prove the first introduction rule, we again unfold the definition and |
82 then apply the introdution rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible. |
83 then apply the introdution rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible. |
83 We then end up in a proof state of the following form: |
84 We then end up in a proof state of the following form: |
84 @{subgoals [display]} |
85 |
85 The two assumptions correspond to the introduction rules, where @{term "trcl R"} has been |
86 @{subgoals [display]} |
86 replaced by @{term "P"}. Thus, all we have to do is to eliminate the universal quantifier |
87 |
87 in front of the first assumption, and then solve the goal by assumption: |
88 The two assumptions correspond to the introduction rules, where @{term "trcl R"} has been |
88 *} |
89 replaced by @{term "P"}. Thus, all we have to do is to eliminate the universal quantifier |
|
90 in front of the first assumption, and then solve the goal by assumption: |
|
91 *} |
89 (*<*)oops(*>*) |
92 (*<*)oops(*>*) |
|
93 |
90 lemma trcl_base: "trcl R x x" |
94 lemma trcl_base: "trcl R x x" |
91 apply (unfold trcl_def) |
95 apply (unfold trcl_def) |
92 apply (rule allI impI)+ |
96 apply (rule allI impI)+ |
93 apply (drule spec) |
97 apply (drule spec) |
94 apply assumption |
98 apply assumption |
95 done |
99 done |
|
100 |
96 (*<*) |
101 (*<*) |
97 lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z" |
102 lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z" |
98 apply (unfold trcl_def) |
103 apply (unfold trcl_def) |
99 apply (rule allI impI)+ |
104 apply (rule allI impI)+ |
100 (*>*) |
105 (*>*) |
|
106 |
101 txt {* |
107 txt {* |
102 \noindent |
108 |
103 Since the second introduction rule has premises, its proof is not as easy as the previous |
109 Since the second introduction rule has premises, its proof is not as easy as the previous |
104 one. After unfolding the definitions and applying the introduction rules for @{text "\<forall>"} |
110 one. After unfolding the definitions and applying the introduction rules for @{text "\<forall>"} |
105 and @{text "\<longrightarrow>"}, we get the proof state |
111 and @{text "\<longrightarrow>"}, we get the proof state |
106 @{subgoals [display]} |
112 @{subgoals [display]} |
107 The third and fourth assumption corresponds to the first and second introduction rule, |
113 The third and fourth assumption corresponds to the first and second introduction rule, |
108 respectively, whereas the first and second assumption corresponds to the premises of |
114 respectively, whereas the first and second assumption corresponds to the premises of |
109 the introduction rule. Since we want to prove the second introduction rule, we apply |
115 the introduction rule. Since we want to prove the second introduction rule, we apply |
110 the fourth assumption to the goal @{term "P x z"}. In order for the assumption to |
116 the fourth assumption to the goal @{term "P x z"}. In order for the assumption to |
111 be applicable, we have to eliminate the universal quantifiers and turn the object-level |
117 be applicable, we have to eliminate the universal quantifiers and turn the object-level |
112 implications into meta-level ones. This can be accomplished using the @{text rule_format} |
118 implications into meta-level ones. This can be accomplished using the @{text rule_format} |
113 attribute. Applying the assumption produces two new subgoals, which can be solved using |
119 attribute. Applying the assumption produces two new subgoals, which can be solved using |
114 the first and second assumption. The second assumption again involves a quantifier and |
120 the first and second assumption. The second assumption again involves a quantifier and |
115 implications that have to be eliminated before it can be applied. To avoid problems |
121 implications that have to be eliminated before it can be applied. To avoid problems |
116 with higher order unification, it is advisable to provide an instantiation for the |
122 with higher order unification, it is advisable to provide an instantiation for the |
117 universally quantified predicate variable in the assumption. |
123 universally quantified predicate variable in the assumption. |
118 *} |
124 *} |
119 (*<*)oops(*>*) |
125 (*<*)oops(*>*) |
|
126 |
120 lemma trcl_step: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z" |
127 lemma trcl_step: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z" |
121 apply (unfold trcl_def) |
128 apply (unfold trcl_def) |
122 apply (rule allI impI)+ |
129 apply (rule allI impI)+ |
123 proof - |
130 proof - |
124 case goal1 |
131 case goal1 |
129 OF goal1(3-4)]) |
136 OF goal1(3-4)]) |
130 done |
137 done |
131 qed |
138 qed |
132 |
139 |
133 text {* |
140 text {* |
134 \noindent |
141 |
135 This method of defining inductive predicates easily generalizes to mutually inductive |
142 This method of defining inductive predicates easily generalizes to mutually inductive |
136 predicates, like the predicates @{text even} and @{text odd} characterized by the |
143 predicates, like the predicates @{text even} and @{text odd} characterized by the |
137 following introduction rules: |
144 following introduction rules: |
138 \[ |
145 |
139 \begin{array}{l} |
146 \begin{center} |
140 @{term "even (0::nat)"} \\ |
147 @{term[mode=Axiom] "even (0::nat)"} \hspace{5mm} |
141 @{term "odd m \<Longrightarrow> even (Suc m)"} \\ |
148 @{term[mode=Rule] "odd m \<Longrightarrow> even (Suc m)"} \hspace{5mm} |
142 @{term "even m \<Longrightarrow> odd (Suc m)"} |
149 @{term[mode=Rule] "even m \<Longrightarrow> odd (Suc m)"} |
143 \end{array} |
150 \end{center} |
144 \] |
151 |
145 Since the predicates are mutually inductive, each of the definitions contain two |
152 Since the predicates are mutually inductive, each of the definitions contain two |
146 quantifiers over the predicates @{text P} and @{text Q}. |
153 quantifiers over the predicates @{text P} and @{text Q}. |
147 *} |
154 *} |
148 |
155 |
149 definition "even \<equiv> \<lambda>n. |
156 definition "even n \<equiv> |
150 \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> P n" |
157 \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) |
151 |
158 \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> P n" |
152 definition "odd \<equiv> \<lambda>n. |
159 |
153 \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q n" |
160 definition "odd n \<equiv> |
154 |
161 \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) |
155 text {* |
162 \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q n" |
156 \noindent |
163 |
157 For proving the induction rule, we use exactly the same technique as in the transitive |
164 text {* |
158 closure example: |
165 For proving the induction rule, we use exactly the same technique as in the transitive |
|
166 closure example: |
159 *} |
167 *} |
160 |
168 |
161 lemma even_induct: |
169 lemma even_induct: |
162 assumes even: "even n" |
170 assumes even: "even n" |
163 shows "P 0 \<Longrightarrow> |
171 shows "P 0 \<Longrightarrow> |
169 apply (drule spec [where x=Q]) |
177 apply (drule spec [where x=Q]) |
170 apply assumption |
178 apply assumption |
171 done |
179 done |
172 |
180 |
173 text {* |
181 text {* |
174 \noindent |
182 A similar induction rule having @{term "Q n"} as a conclusion can be proved for |
175 A similar induction rule having @{term "Q n"} as a conclusion can be proved for |
183 the @{text odd} predicate. |
176 the @{text odd} predicate. |
184 The proofs of the introduction rules are also very similar to the ones in the |
177 The proofs of the introduction rules are also very similar to the ones in the |
185 previous example. We only show the proof of the second introduction rule, |
178 previous example. We only show the proof of the second introduction rule, |
186 since it is almost the same as the one for the third introduction rule, |
179 since it is almost the same as the one for the third introduction rule, |
187 and the proof of the first rule is trivial. |
180 and the proof of the first rule is trivial. |
|
181 *} |
188 *} |
182 |
189 |
183 lemma evenS: "odd m \<Longrightarrow> even (Suc m)" |
190 lemma evenS: "odd m \<Longrightarrow> even (Suc m)" |
184 apply (unfold odd_def even_def) |
191 apply (unfold odd_def even_def) |
185 apply (rule allI impI)+ |
192 apply (rule allI impI)+ |
208 apply (rule goal1(1) [THEN spec [where x=P], THEN spec [where x=Q], |
215 apply (rule goal1(1) [THEN spec [where x=P], THEN spec [where x=Q], |
209 THEN mp, THEN mp, THEN mp, OF goal1(2-4)]) |
216 THEN mp, THEN mp, THEN mp, OF goal1(2-4)]) |
210 done |
217 done |
211 qed |
218 qed |
212 (*>*) |
219 (*>*) |
213 text {* |
220 |
214 \noindent |
221 text {* |
215 As a final example, we will consider the definition of the accessible |
222 As a final example, we will consider the definition of the accessible |
216 part of a relation @{text R} characterized by the introduction rule |
223 part of a relation @{text R} characterized by the introduction rule |
217 \[ |
224 |
218 @{term "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"} |
225 \begin{center} |
219 \] |
226 @{term[mode=Rule] "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"} |
220 whose premise involves a universal quantifier and an implication. The |
227 \end{center} |
221 definition of @{text accpart} is as follows: |
228 |
222 *} |
229 whose premise involves a universal quantifier and an implication. The |
223 |
230 definition of @{text accpart} is as follows: |
224 definition "accpart \<equiv> \<lambda>R x. \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x" |
231 *} |
225 |
232 |
226 text {* |
233 definition "accpart R x \<equiv> \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x" |
227 \noindent |
234 |
228 The proof of the induction theorem is again straightforward: |
235 text {* |
|
236 The proof of the induction theorem is again straightforward: |
229 *} |
237 *} |
230 |
238 |
231 lemma accpart_induct: |
239 lemma accpart_induct: |
232 assumes acc: "accpart R x" |
240 assumes acc: "accpart R x" |
233 shows "(\<And>x. (\<And>y. R y x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x" |
241 shows "(\<And>x. (\<And>y. R y x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x" |
240 (*<*) |
248 (*<*) |
241 lemma accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x" |
249 lemma accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x" |
242 apply (unfold accpart_def) |
250 apply (unfold accpart_def) |
243 apply (rule allI impI)+ |
251 apply (rule allI impI)+ |
244 (*>*) |
252 (*>*) |
|
253 |
245 txt {* |
254 txt {* |
246 \noindent |
255 |
247 Proving the introduction rule is a little more complicated, due to the quantifier |
256 Proving the introduction rule is a little more complicated, due to the quantifier |
248 and the implication in the premise. We first convert the meta-level universal quantifier |
257 and the implication in the premise. We first convert the meta-level universal quantifier |
249 and implication to their object-level counterparts. Unfolding the definition of |
258 and implication to their object-level counterparts. Unfolding the definition of |
250 @{text accpart} and applying the introduction rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} |
259 @{text accpart} and applying the introduction rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} |
251 yields the following proof state: |
260 yields the following proof state: |
252 @{subgoals [display]} |
261 @{subgoals [display]} |
253 Applying the second assumption produces a proof state with the new local assumption |
262 Applying the second assumption produces a proof state with the new local assumption |
254 @{term "R y x"}, which will then be used to solve the goal @{term "P y"} using the |
263 @{term "R y x"}, which will then be used to solve the goal @{term "P y"} using the |
255 first assumption. |
264 first assumption. |
256 *} |
265 *} |
257 (*<*)oops(*>*) |
266 (*<*)oops(*>*) |
|
267 |
258 lemma accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x" |
268 lemma accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x" |
259 apply (unfold accpart_def) |
269 apply (unfold accpart_def) |
260 apply (rule allI impI)+ |
270 apply (rule allI impI)+ |
261 proof - |
271 proof - |
262 case goal1 |
272 case goal1 |