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 |
8 Let us first give three examples showing how to define inductive predicates |
9 In this section, we will give three examples showing how to define inductive |
9 by hand and prove characteristic properties such as introduction rules and |
10 predicates by hand and prove characteristic properties such as introduction |
10 an induction rule. From these examples, we will then figure out a general |
11 rules and an induction rule. From these examples, we will then figure out a |
11 method for defining inductive predicates. The aim in this section is not to |
12 general method for defining inductive predicates. It should be noted that |
12 write proofs that are as beautiful as possible, but as close as possible to |
13 our aim in this section is not to write proofs that are as beautiful as |
13 the ML-code producing the proofs that we will develop later. |
14 possible, but as close as possible to the ML code producing the proofs that |
14 |
15 we will develop later. As a first example, we consider the transitive |
15 As a first example, we consider the transitive closure of a relation @{text |
16 closure of a relation @{text R}. It is an inductive predicate characterized |
16 R}. It is an inductive predicate characterized by the two introduction rules |
17 by the two introduction rules |
|
18 |
17 |
19 \begin{center} |
18 \begin{center} |
20 @{term[mode=Axiom] "trcl R x x"} \hspace{5mm} |
19 @{term[mode=Axiom] "trcl R x x"} \hspace{5mm} |
21 @{term[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"} |
20 @{term[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"} |
22 \end{center} |
21 \end{center} |
35 |
34 |
36 definition "trcl R x y \<equiv> |
35 definition "trcl R x y \<equiv> |
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" |
36 \<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 |
37 |
39 text {* |
38 text {* |
40 where we quantify over the predicate @{text P}. |
39 where we quantify over the predicate @{text P}. Note that we have to use the |
41 |
40 object implication @{text "\<longrightarrow>"} and object quantification @{text "\<forall>"} for stating |
42 Since the predicate @{term "trcl R x y"} yields an element of the type of object |
41 this definition. |
43 level truth values @{text bool}, the meta-level implications @{text "\<Longrightarrow>"} in the |
42 |
44 above introduction rules have to be converted to object-level implications |
43 With this definition of the transitive closure, the proof of the induction |
45 @{text "\<longrightarrow>"}. Moreover, we use object-level universal quantifiers @{text "\<forall>"} |
|
46 rather than meta-level universal quantifiers @{text "\<And>"} for quantifying over |
|
47 the variable parameters of the introduction rules. Isabelle already offers some |
|
48 infrastructure for converting between meta-level and object-level connectives, |
|
49 which we will use later on. |
|
50 |
|
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 |
44 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 |
45 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 |
46 method, expand the definition of @{text trcl}, eliminate the universal quantifier |
55 contained in it, and then solve the goal by assumption. |
47 contained in it, and then solve the goal by assumption. |
|
48 |
|
49 (FIXME: add linenumbers to the proof below and the text above) |
56 *} |
50 *} |
57 |
51 |
58 lemma trcl_induct: |
52 lemma trcl_induct: |
59 assumes trcl: "trcl R x y" |
53 assumes asm: "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" |
54 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" |
61 apply (atomize (full)) |
55 apply(atomize (full)) |
62 apply (cut_tac trcl) |
56 apply(cut_tac asm) |
63 apply (unfold trcl_def) |
57 apply(unfold trcl_def) |
64 apply (drule spec [where x=P]) |
58 apply(drule spec[where x=P]) |
65 apply assumption |
59 apply(assumption) |
66 done |
60 done |
67 (*<*) |
61 |
68 lemma "trcl R x x" |
62 text {* |
69 apply (unfold trcl_def) |
|
70 apply (rule allI impI)+ |
|
71 (*>*) |
|
72 |
|
73 txt {* |
|
74 |
|
75 The above induction rule is \emph{weak} in the sense that the induction step may |
|
76 only be proved using the assumptions @{term "R x y"} and @{term "P y z"}, but not |
|
77 using the additional assumption \mbox{@{term "trcl R y z"}}. A stronger induction rule |
|
78 containing this additional assumption can be derived from the weaker one with the |
|
79 help of the introduction rules for @{text trcl}. |
|
80 |
|
81 We now turn to the proofs of the introduction rules, which are slightly more complicated. |
63 We now turn to the proofs of the introduction rules, which are slightly more complicated. |
82 In order to prove the first introduction rule, we again unfold the definition and |
64 In order to prove the first introduction rule, we again unfold the definition and |
83 then apply the introdution rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible. |
65 then apply the introdution rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible. |
84 We then end up in a proof state of the following form: |
66 We then end up in a proof state of the following form: |
85 |
67 |
86 @{subgoals [display]} |
68 *} |
87 |
69 |
88 The two assumptions correspond to the introduction rules, where @{term "trcl R"} has been |
70 (*<*)lemma "trcl R x x" |
89 replaced by @{term "P"}. Thus, all we have to do is to eliminate the universal quantifier |
71 apply (unfold trcl_def) |
90 in front of the first assumption, and then solve the goal by assumption: |
72 apply (rule allI impI)+(*>*) |
91 *} |
73 txt {* @{subgoals [display]} *} |
92 (*<*)oops(*>*) |
74 (*<*)oops(*>*) |
93 |
75 |
|
76 text {* |
|
77 The two assumptions correspond to the introduction rules, where @{text "trcl |
|
78 R"} has been replaced by P. Thus, all we have to do is to eliminate the |
|
79 universal quantifier in front of the first assumption, and then solve the |
|
80 goal by assumption: |
|
81 *} |
|
82 |
|
83 |
94 lemma trcl_base: "trcl R x x" |
84 lemma trcl_base: "trcl R x x" |
95 apply (unfold trcl_def) |
85 apply(unfold trcl_def) |
96 apply (rule allI impI)+ |
86 apply(rule allI impI)+ |
97 apply (drule spec) |
87 apply(drule spec) |
98 apply assumption |
88 apply(assumption) |
99 done |
89 done |
100 |
90 |
101 (*<*) |
91 text {* |
102 lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z" |
|
103 apply (unfold trcl_def) |
|
104 apply (rule allI impI)+ |
|
105 (*>*) |
|
106 |
|
107 txt {* |
|
108 |
|
109 Since the second introduction rule has premises, its proof is not as easy as the previous |
92 Since the second introduction rule has premises, its proof is not as easy as the previous |
110 one. After unfolding the definitions and applying the introduction rules for @{text "\<forall>"} |
93 one. After unfolding the definitions and applying the introduction rules for @{text "\<forall>"} |
111 and @{text "\<longrightarrow>"}, we get the proof state |
94 and @{text "\<longrightarrow>"}, we get the proof state |
112 @{subgoals [display]} |
95 *} |
|
96 |
|
97 |
|
98 (*<*)lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z" |
|
99 apply (unfold trcl_def) |
|
100 apply (rule allI impI)+(*>*) |
|
101 txt {*@{subgoals [display]} *} |
|
102 (*<*)oops(*>*) |
|
103 |
|
104 text {* |
113 The third and fourth assumption corresponds to the first and second introduction rule, |
105 The third and fourth assumption corresponds to the first and second introduction rule, |
114 respectively, whereas the first and second assumption corresponds to the premises of |
106 respectively, whereas the first and second assumption corresponds to the premises of |
115 the introduction rule. Since we want to prove the second introduction rule, we apply |
107 the introduction rule. Since we want to prove the second introduction rule, we apply |
116 the fourth assumption to the goal @{term "P x z"}. In order for the assumption to |
108 the fourth assumption to the goal @{term "P x z"}. In order for the assumption to |
117 be applicable, we have to eliminate the universal quantifiers and turn the object-level |
109 be applicable, we have to eliminate the universal quantifiers and turn the object-level |