59 subsection{*The Reflexive Transitive Closure*} |
59 subsection{*The Reflexive Transitive Closure*} |
60 |
60 |
61 consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" ("_*" [1000] 999) |
61 consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" ("_*" [1000] 999) |
62 inductive "r*" |
62 inductive "r*" |
63 intros |
63 intros |
64 rtc_refl[iff]: "(x,x) \<in> r*" |
64 refl[iff]: "(x,x) \<in> r*" |
65 rtc_step: "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*" |
65 step: "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*" |
66 |
66 |
67 lemma [intro]: "(x,y) : r \<Longrightarrow> (x,y) \<in> r*" |
67 lemma [intro]: "(x,y) : r \<Longrightarrow> (x,y) \<in> r*" |
68 by(blast intro: rtc_step); |
68 by(blast intro: rtc.step); |
69 |
69 |
70 lemma rtc_trans: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*" |
70 lemma rtc_trans: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*" |
71 apply(erule rtc.induct) |
71 apply(erule rtc.induct) |
72 oops |
72 oops |
73 |
73 |
74 lemma rtc_trans[rule_format]: |
74 lemma rtc_trans[rule_format]: |
75 "(x,y) \<in> r* \<Longrightarrow> (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*" |
75 "(x,y) \<in> r* \<Longrightarrow> (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*" |
76 apply(erule rtc.induct) |
76 apply(erule rtc.induct) |
77 apply(blast); |
77 apply(blast); |
78 apply(blast intro: rtc_step); |
78 apply(blast intro: rtc.step); |
79 done |
79 done |
80 |
80 |
81 text{* |
81 text{* |
82 \begin{exercise} |
82 \begin{exercise} |
83 Show that the converse of @{thm[source]rtc_step} also holds: |
83 Show that the converse of @{thm[source]rtc.step} also holds: |
84 @{prop[display]"[| (x,y) : r*; (y,z) : r |] ==> (x,z) : r*"} |
84 @{prop[display]"[| (x,y) : r*; (y,z) : r |] ==> (x,z) : r*"} |
85 \end{exercise}*} |
85 \end{exercise}*} |
86 |
86 |
87 subsection{*The accessible part of a relation*} |
87 subsection{*The accessible part of a relation*} |
88 |
88 |