3 begin |
3 begin |
4 |
4 |
5 section{* Examples of Inductive Definitions \label{sec:ind-examples} *} |
5 section{* Examples of Inductive Definitions \label{sec:ind-examples} *} |
6 |
6 |
7 text {* |
7 text {* |
8 Let us first give three examples showing how to define by hand inductive |
8 Let us first give three examples showing how to define inductive |
9 predicates and then also how to prove by hand characteristic properties |
9 predicates by hand and then also how to prove by hand characteristic properties |
10 about them, such as introduction rules and induction principles. From |
10 about them, such as introduction rules and induction principles. From |
11 these examples, we will figure out a general method for defining inductive |
11 these examples, we will figure out a general method for defining inductive |
12 predicates. The aim in this section is \emph{not} to write proofs that are as |
12 predicates. The aim in this section is \emph{not} to write proofs that are as |
13 beautiful as possible, but as close as possible to the ML-code we will |
13 beautiful as possible, but as close as possible to the ML-code we will |
14 develop later. |
14 develop later. |
64 done |
64 done |
65 |
65 |
66 text {* |
66 text {* |
67 The proofs for the introduction are slightly more complicated. We need to prove |
67 The proofs for the introduction are slightly more complicated. We need to prove |
68 the facs @{prop "trcl R x x"} and @{prop "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}. |
68 the facs @{prop "trcl R x x"} and @{prop "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}. |
69 In order to prove the first goal, we again unfold the definition and |
69 In order to prove the first fact, we again unfold the definition and |
70 then apply the introdution rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible. |
70 then apply the introdution rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible. |
71 We then end up in the goal state: |
71 We then end up in the goal state: |
72 *} |
72 *} |
73 |
73 |
74 (*<*)lemma "trcl R x x" |
74 (*<*)lemma "trcl R x x" |
268 text {* |
268 text {* |
269 Proving the introduction rule is a little more complicated, because the quantifier |
269 Proving the introduction rule is a little more complicated, because the quantifier |
270 and the implication in the premise. We first convert the meta-level universal quantifier |
270 and the implication in the premise. We first convert the meta-level universal quantifier |
271 and implication to their object-level counterparts. Unfolding the definition of |
271 and implication to their object-level counterparts. Unfolding the definition of |
272 @{text accpart} and applying the introduction rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} |
272 @{text accpart} and applying the introduction rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} |
273 yields the following proof state: |
273 yields the following goal state: |
274 *} |
274 *} |
275 |
275 |
276 (*<*)lemma accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x" |
276 (*<*)lemma accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x" |
277 apply (unfold accpart_def) |
277 apply (unfold accpart_def) |
278 apply (rule allI impI)+(*>*) |
278 apply (rule allI impI)+(*>*) |
279 txt {* @{subgoals [display]} *} |
279 txt {* @{subgoals [display]} *} |
280 (*<*)oops(*>*) |
280 (*<*)oops(*>*) |
281 |
281 |
282 text {* |
282 text {* |
283 Applying the second assumption produces a proof state with the new local assumption |
283 Applying the second assumption produces a goal state with the new local assumption |
284 @{term "R y x"}, which will then be used to solve the goal @{term "P y"} using the |
284 @{term "R y x"}, which will then be used to solve the goal @{term "P y"} using the |
285 first assumption. |
285 first assumption. |
286 *} |
286 *} |
287 |
287 |
288 lemma %small accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x" |
288 lemma %small accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x" |