1 (*<*)theory Star = Main:(*>*) |
1 (*<*)theory Star = Main:(*>*) |
2 |
2 |
3 section{*The transitive and reflexive closure*} |
3 section{*The reflexive transitive closure*} |
4 |
4 |
5 text{* |
5 text{* |
6 A perfect example of an inductive definition is the transitive, reflexive |
6 A perfect example of an inductive definition is the reflexive transitive |
7 closure of a relation. This concept was already introduced in |
7 closure of a relation. This concept was already introduced in |
8 \S\ref{sec:rtrancl}, but it was not shown how it is defined. In fact, |
8 \S\ref{sec:rtrancl}, but it was not shown how it is defined. In fact, |
9 the operator @{text"^*"} is not defined inductively but via a least |
9 the operator @{text"^*"} is not defined inductively but via a least |
10 fixpoint because at that point in the theory hierarchy |
10 fixpoint because at that point in the theory hierarchy |
11 inductive definitions are not yet available. But now they are: |
11 inductive definitions are not yet available. But now they are: |
12 *} |
12 *} |
13 |
13 |
14 consts trc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" ("_*" [1000] 999) |
14 consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" ("_*" [1000] 999) |
15 inductive "r*" |
15 inductive "r*" |
16 intros |
16 intros |
17 trc_refl[intro!]: "(x,x) \<in> r*" |
17 rtc_refl[intro!]: "(x,x) \<in> r*" |
18 trc_step: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r \<rbrakk> \<Longrightarrow> (x,z) \<in> r*" |
18 rtc_step: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r \<rbrakk> \<Longrightarrow> (x,z) \<in> r*" |
19 |
19 |
20 lemma [intro]: "(x,y) : r \<Longrightarrow> (x,y) \<in> r*" |
20 lemma [intro]: "(x,y) : r \<Longrightarrow> (x,y) \<in> r*" |
21 by(blast intro: trc_step); |
21 by(blast intro: rtc_step); |
22 |
22 |
23 lemma step2[rule_format]: |
23 lemma step2[rule_format]: |
24 "(y,z) \<in> r* \<Longrightarrow> (x,y) \<in> r \<longrightarrow> (x,z) \<in> r*" |
24 "(y,z) \<in> r* \<Longrightarrow> (x,y) \<in> r \<longrightarrow> (x,z) \<in> r*" |
25 apply(erule trc.induct) |
25 apply(erule rtc.induct) |
26 apply(blast); |
26 apply(blast); |
27 apply(blast intro: trc_step); |
27 apply(blast intro: rtc_step); |
28 done |
28 done |
29 |
29 |
30 lemma trc_trans[rule_format]: |
30 lemma rtc_trans[rule_format]: |
31 "(x,y) \<in> r* \<Longrightarrow> \<forall>z. (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*" |
31 "(x,y) \<in> r* \<Longrightarrow> \<forall>z. (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*" |
32 apply(erule trc.induct) |
32 apply(erule rtc.induct) |
33 apply blast; |
33 apply blast; |
34 apply(blast intro: step2); |
34 apply(blast intro: step2); |
35 done |
35 done |
36 |
36 |
37 consts trc2 :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" |
37 consts rtc2 :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" |
38 inductive "trc2 r" |
38 inductive "rtc2 r" |
39 intros |
39 intros |
40 "(x,y) \<in> r \<Longrightarrow> (x,y) \<in> trc2 r" |
40 "(x,y) \<in> r \<Longrightarrow> (x,y) \<in> rtc2 r" |
41 "(x,x) \<in> trc2 r" |
41 "(x,x) \<in> rtc2 r" |
42 "\<lbrakk> (x,y) \<in> trc2 r; (y,z) \<in> trc2 r \<rbrakk> \<Longrightarrow> (x,z) \<in> trc2 r" |
42 "\<lbrakk> (x,y) \<in> rtc2 r; (y,z) \<in> rtc2 r \<rbrakk> \<Longrightarrow> (x,z) \<in> rtc2 r" |
43 |
43 |
|
44 text{* |
|
45 The equivalence of the two definitions is easily shown by the obvious rule |
|
46 inductions: |
|
47 *} |
44 |
48 |
45 lemma "((x,y) \<in> trc2 r) = ((x,y) \<in> r*)" |
49 lemma "(x,y) \<in> rtc2 r \<Longrightarrow> (x,y) \<in> r*" |
46 apply(rule iffI); |
50 apply(erule rtc2.induct); |
47 apply(erule trc2.induct); |
|
48 apply(blast); |
|
49 apply(blast); |
51 apply(blast); |
50 apply(blast intro: trc_trans); |
52 apply(blast); |
51 apply(erule trc.induct); |
53 apply(blast intro: rtc_trans); |
52 apply(blast intro: trc2.intros); |
54 done |
53 apply(blast intro: trc2.intros); |
55 |
|
56 lemma "(x,y) \<in> r* \<Longrightarrow> (x,y) \<in> rtc2 r" |
|
57 apply(erule rtc.induct); |
|
58 apply(blast intro: rtc2.intros); |
|
59 apply(blast intro: rtc2.intros); |
54 done |
60 done |
55 |
61 |
56 (*<*)end(*>*) |
62 (*<*)end(*>*) |