author  berghofe 
Wed, 07 Feb 2007 17:28:09 +0100  
changeset 22262  96ba62dff413 
parent 22172  e7d6cb237b5e 
child 22422  ee19cdb07528 
permissions  rwrr 
10213  1 
(* Title: HOL/Transitive_Closure.thy 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1992 University of Cambridge 

5 
*) 

6 

12691  7 
header {* Reflexive and Transitive closure of a relation *} 
8 

15131  9 
theory Transitive_Closure 
22262  10 
imports Predicate 
21589  11 
uses "~~/src/Provers/trancl.ML" 
15131  12 
begin 
12691  13 

14 
text {* 

15 
@{text rtrancl} is reflexive/transitive closure, 

16 
@{text trancl} is transitive closure, 

17 
@{text reflcl} is reflexive closure. 

18 

19 
These postfix operators have \emph{maximum priority}, forcing their 

20 
operands to be atomic. 

21 
*} 

10213  22 

22262  23 
inductive2 
24 
rtrancl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(_^**)" [1000] 1000) 

25 
for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 

26 
where 

27 
rtrancl_refl [intro!, Pure.intro!, simp]: "r^** a a" 

28 
 rtrancl_into_rtrancl [Pure.intro]: "r^** a b ==> r b c ==> r^** a c" 

11327
cd2c27a23df1
Transitive closure is now defined via "inductive".
berghofe
parents:
11115
diff
changeset

29 

22262  30 
inductive2 
31 
trancl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(_^++)" [1000] 1000) 

32 
for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 

33 
where 

34 
r_into_trancl [intro, Pure.intro]: "r a b ==> r^++ a b" 

35 
 trancl_into_trancl [Pure.intro]: "r^++ a b ==> r b c ==> r^++ a c" 

13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

36 

22262  37 
constdefs 
38 
rtrancl_set :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_^*)" [1000] 999) 

39 
"r^* == Collect2 (member2 r)^**" 

40 

41 
trancl_set :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_^+)" [1000] 999) 

42 
"r^+ == Collect2 (member2 r)^++" 

10213  43 

19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19623
diff
changeset

44 
abbreviation 
22262  45 
reflcl :: "('a => 'a => bool) => 'a => 'a => bool" ("(_^==)" [1000] 1000) where 
46 
"r^== == join r op =" 

47 

48 
abbreviation 

49 
reflcl_set :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_^=)" [1000] 999) where 

19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19623
diff
changeset

50 
"r^= == r \<union> Id" 
10213  51 

21210  52 
notation (xsymbols) 
22262  53 
rtrancl ("(_\<^sup>*\<^sup>*)" [1000] 1000) and 
54 
trancl ("(_\<^sup>+\<^sup>+)" [1000] 1000) and 

55 
reflcl ("(_\<^sup>=\<^sup>=)" [1000] 1000) and 

56 
rtrancl_set ("(_\<^sup>*)" [1000] 999) and 

57 
trancl_set ("(_\<^sup>+)" [1000] 999) and 

58 
reflcl_set ("(_\<^sup>=)" [1000] 999) 

12691  59 

21210  60 
notation (HTML output) 
22262  61 
rtrancl ("(_\<^sup>*\<^sup>*)" [1000] 1000) and 
62 
trancl ("(_\<^sup>+\<^sup>+)" [1000] 1000) and 

63 
reflcl ("(_\<^sup>=\<^sup>=)" [1000] 1000) and 

64 
rtrancl_set ("(_\<^sup>*)" [1000] 999) and 

65 
trancl_set ("(_\<^sup>+)" [1000] 999) and 

66 
reflcl_set ("(_\<^sup>=)" [1000] 999) 

14565  67 

12691  68 

69 
subsection {* Reflexivetransitive closure *} 

70 

22262  71 
lemma rtrancl_set_eq [pred_set_conv]: "(member2 r)^** = member2 (r^*)" 
72 
by (simp add: rtrancl_set_def) 

73 

74 
lemma reflcl_set_eq [pred_set_conv]: "(join (member2 r) op =) = member2 (r Un Id)" 

75 
by (simp add: expand_fun_eq) 

76 

77 
lemmas rtrancl_refl [intro!, Pure.intro!, simp] = rtrancl_refl [to_set] 

78 
lemmas rtrancl_into_rtrancl [Pure.intro] = rtrancl_into_rtrancl [to_set] 

79 

12691  80 
lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*" 
81 
 {* @{text rtrancl} of @{text r} contains @{text r} *} 

82 
apply (simp only: split_tupled_all) 

83 
apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl]) 

84 
done 

85 

22262  86 
lemma r_into_rtrancl' [intro]: "r x y ==> r^** x y" 
87 
 {* @{text rtrancl} of @{text r} contains @{text r} *} 

88 
by (erule rtrancl.rtrancl_refl [THEN rtrancl.rtrancl_into_rtrancl]) 

89 

90 
lemma rtrancl_mono': "r \<le> s ==> r^** \<le> s^**" 

12691  91 
 {* monotonicity of @{text rtrancl} *} 
22262  92 
apply (rule predicate2I) 
12691  93 
apply (erule rtrancl.induct) 
22262  94 
apply (rule_tac [2] rtrancl.rtrancl_into_rtrancl, blast+) 
12691  95 
done 
96 

22262  97 
lemmas rtrancl_mono = rtrancl_mono' [to_set] 
98 

99 
theorem rtrancl_induct' [consumes 1, induct set: rtrancl]: 

100 
assumes a: "r^** a b" 

101 
and cases: "P a" "!!y z. [ r^** a y; r y z; P y ] ==> P z" 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12823
diff
changeset

102 
shows "P b" 
12691  103 
proof  
104 
from a have "a = a > P b" 

17589  105 
by (induct "%x y. x = a > P y" a b) (iprover intro: cases)+ 
106 
thus ?thesis by iprover 

12691  107 
qed 
108 

22262  109 
lemmas rtrancl_induct [consumes 1, induct set: rtrancl_set] = rtrancl_induct' [to_set] 
110 

111 
lemmas rtrancl_induct2' = 

112 
rtrancl_induct'[of _ "(ax,ay)" "(bx,by)", split_rule, 

113 
consumes 1, case_names refl step] 

114 

14404
4952c5a92e04
Transitive_Closure: added consumes and case_names attributes
nipkow
parents:
14398
diff
changeset

115 
lemmas rtrancl_induct2 = 
4952c5a92e04
Transitive_Closure: added consumes and case_names attributes
nipkow
parents:
14398
diff
changeset

116 
rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete), 
4952c5a92e04
Transitive_Closure: added consumes and case_names attributes
nipkow
parents:
14398
diff
changeset

117 
consumes 1, case_names refl step] 
18372  118 

19228  119 
lemma reflexive_rtrancl: "reflexive (r^*)" 
120 
by (unfold refl_def) fast 

121 

12691  122 
lemma trans_rtrancl: "trans(r^*)" 
123 
 {* transitivity of transitive closure!!  by induction *} 

12823  124 
proof (rule transI) 
125 
fix x y z 

126 
assume "(x, y) \<in> r\<^sup>*" 

127 
assume "(y, z) \<in> r\<^sup>*" 

17589  128 
thus "(x, z) \<in> r\<^sup>*" by induct (iprover!)+ 
12823  129 
qed 
12691  130 

131 
lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard] 

132 

22262  133 
lemma rtrancl_trans': 
134 
assumes xy: "r^** x y" 

135 
and yz: "r^** y z" 

136 
shows "r^** x z" using yz xy 

137 
by induct iprover+ 

138 

12691  139 
lemma rtranclE: 
18372  140 
assumes major: "(a::'a,b) : r^*" 
141 
and cases: "(a = b) ==> P" 

142 
"!!y. [ (a,y) : r^*; (y,b) : r ] ==> P" 

143 
shows P 

12691  144 
 {* elimination of @{text rtrancl}  by induction on a special formula *} 
18372  145 
apply (subgoal_tac "(a::'a) = b  (EX y. (a,y) : r^* & (y,b) : r)") 
146 
apply (rule_tac [2] major [THEN rtrancl_induct]) 

147 
prefer 2 apply blast 

148 
prefer 2 apply blast 

149 
apply (erule asm_rl exE disjE conjE cases)+ 

150 
done 

12691  151 

22080
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

152 
lemma rtrancl_Int_subset: "[ Id \<subseteq> s; r O (r^* \<inter> s) \<subseteq> s] ==> r^* \<subseteq> s" 
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

153 
apply (rule subsetI) 
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

154 
apply (rule_tac p="x" in PairE, clarify) 
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

155 
apply (erule rtrancl_induct, auto) 
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

156 
done 
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

157 

22262  158 
lemma converse_rtrancl_into_rtrancl': 
159 
"r a b \<Longrightarrow> r\<^sup>*\<^sup>* b c \<Longrightarrow> r\<^sup>*\<^sup>* a c" 

160 
by (rule rtrancl_trans') iprover+ 

161 

162 
lemmas converse_rtrancl_into_rtrancl = converse_rtrancl_into_rtrancl' [to_set] 

12691  163 

164 
text {* 

165 
\medskip More @{term "r^*"} equations and inclusions. 

166 
*} 

167 

22262  168 
lemma rtrancl_idemp' [simp]: "(r^**)^** = r^**" 
169 
apply (auto intro!: order_antisym) 

170 
apply (erule rtrancl_induct') 

171 
apply (rule rtrancl.rtrancl_refl) 

172 
apply (blast intro: rtrancl_trans') 

12691  173 
done 
174 

22262  175 
lemmas rtrancl_idemp [simp] = rtrancl_idemp' [to_set] 
176 

12691  177 
lemma rtrancl_idemp_self_comp [simp]: "R^* O R^* = R^*" 
178 
apply (rule set_ext) 

179 
apply (simp only: split_tupled_all) 

180 
apply (blast intro: rtrancl_trans) 

181 
done 

182 

183 
lemma rtrancl_subset_rtrancl: "r \<subseteq> s^* ==> r^* \<subseteq> s^*" 

14208  184 
by (drule rtrancl_mono, simp) 
12691  185 

22262  186 
lemma rtrancl_subset': "R \<le> S ==> S \<le> R^** ==> S^** = R^**" 
187 
apply (drule rtrancl_mono') 

188 
apply (drule rtrancl_mono', simp) 

12691  189 
done 
190 

22262  191 
lemmas rtrancl_subset = rtrancl_subset' [to_set] 
192 

193 
lemma rtrancl_Un_rtrancl': "(join (R^**) (S^**))^** = (join R S)^**" 

194 
by (blast intro!: rtrancl_subset' intro: rtrancl_mono' [THEN predicate2D]) 

12691  195 

22262  196 
lemmas rtrancl_Un_rtrancl = rtrancl_Un_rtrancl' [to_set] 
197 

198 
lemma rtrancl_reflcl' [simp]: "(R^==)^** = R^**" 

199 
by (blast intro!: rtrancl_subset') 

200 

201 
lemmas rtrancl_reflcl [simp] = rtrancl_reflcl' [to_set] 

12691  202 

203 
lemma rtrancl_r_diff_Id: "(r  Id)^* = r^*" 

204 
apply (rule sym) 

14208  205 
apply (rule rtrancl_subset, blast, clarify) 
12691  206 
apply (rename_tac a b) 
14208  207 
apply (case_tac "a = b", blast) 
12691  208 
apply (blast intro!: r_into_rtrancl) 
209 
done 

210 

22262  211 
lemma rtrancl_r_diff_Id': "(meet r op ~=)^** = r^**" 
212 
apply (rule sym) 

213 
apply (rule rtrancl_subset') 

214 
apply blast+ 

215 
done 

216 

217 
theorem rtrancl_converseD': 

218 
assumes r: "(r^1)^** x y" 

219 
shows "r^** y x" 

12823  220 
proof  
221 
from r show ?thesis 

22262  222 
by induct (iprover intro: rtrancl_trans' dest!: conversepD)+ 
12823  223 
qed 
12691  224 

22262  225 
lemmas rtrancl_converseD = rtrancl_converseD' [to_set] 
226 

227 
theorem rtrancl_converseI': 

228 
assumes r: "r^** y x" 

229 
shows "(r^1)^** x y" 

12823  230 
proof  
231 
from r show ?thesis 

22262  232 
by induct (iprover intro: rtrancl_trans' conversepI)+ 
12823  233 
qed 
12691  234 

22262  235 
lemmas rtrancl_converseI = rtrancl_converseI' [to_set] 
236 

12691  237 
lemma rtrancl_converse: "(r^1)^* = (r^*)^1" 
238 
by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI) 

239 

19228  240 
lemma sym_rtrancl: "sym r ==> sym (r^*)" 
241 
by (simp only: sym_conv_converse_eq rtrancl_converse [symmetric]) 

242 

22262  243 
theorem converse_rtrancl_induct'[consumes 1]: 
244 
assumes major: "r^** a b" 

245 
and cases: "P b" "!!y z. [ r y z; r^** z b; P z ] ==> P y" 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12823
diff
changeset

246 
shows "P a" 
12691  247 
proof  
22262  248 
from rtrancl_converseI' [OF major] 
12691  249 
show ?thesis 
22262  250 
by induct (iprover intro: cases dest!: conversepD rtrancl_converseD')+ 
12691  251 
qed 
252 

22262  253 
lemmas converse_rtrancl_induct[consumes 1] = converse_rtrancl_induct' [to_set] 
254 

255 
lemmas converse_rtrancl_induct2' = 

256 
converse_rtrancl_induct'[of _ "(ax,ay)" "(bx,by)", split_rule, 

257 
consumes 1, case_names refl step] 

258 

14404
4952c5a92e04
Transitive_Closure: added consumes and case_names attributes
nipkow
parents:
14398
diff
changeset

259 
lemmas converse_rtrancl_induct2 = 
4952c5a92e04
Transitive_Closure: added consumes and case_names attributes
nipkow
parents:
14398
diff
changeset

260 
converse_rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete), 
4952c5a92e04
Transitive_Closure: added consumes and case_names attributes
nipkow
parents:
14398
diff
changeset

261 
consumes 1, case_names refl step] 
12691  262 

22262  263 
lemma converse_rtranclE': 
264 
assumes major: "r^** x z" 

18372  265 
and cases: "x=z ==> P" 
22262  266 
"!!y. [ r x y; r^** y z ] ==> P" 
18372  267 
shows P 
22262  268 
apply (subgoal_tac "x = z  (EX y. r x y & r^** y z)") 
269 
apply (rule_tac [2] major [THEN converse_rtrancl_induct']) 

18372  270 
prefer 2 apply iprover 
271 
prefer 2 apply iprover 

272 
apply (erule asm_rl exE disjE conjE cases)+ 

273 
done 

12691  274 

22262  275 
lemmas converse_rtranclE = converse_rtranclE' [to_set] 
276 

277 
lemmas converse_rtranclE2' = converse_rtranclE' [of _ "(xa,xb)" "(za,zb)", split_rule] 

278 

279 
lemmas converse_rtranclE2 = converse_rtranclE [of "(xa,xb)" "(za,zb)", split_rule] 

12691  280 

281 
lemma r_comp_rtrancl_eq: "r O r^* = r^* O r" 

282 
by (blast elim: rtranclE converse_rtranclE 

283 
intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl) 

284 

20716
a6686a8e1b68
Changed precedence of "op O" (relation composition) from 60 to 75.
krauss
parents:
19656
diff
changeset

285 
lemma rtrancl_unfold: "r^* = Id Un r O r^*" 
15551  286 
by (auto intro: rtrancl_into_rtrancl elim: rtranclE) 
287 

12691  288 

289 
subsection {* Transitive closure *} 

10331  290 

22262  291 
lemma trancl_set_eq [pred_set_conv]: "(member2 r)^++ = member2 (r^+)" 
292 
by (simp add: trancl_set_def) 

293 

294 
lemmas r_into_trancl [intro, Pure.intro] = r_into_trancl [to_set] 

295 
lemmas trancl_into_trancl [Pure.intro] = trancl_into_trancl [to_set] 

296 

13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

297 
lemma trancl_mono: "!!p. p \<in> r^+ ==> r \<subseteq> s ==> p \<in> s^+" 
22262  298 
apply (simp add: split_tupled_all trancl_set_def) 
13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

299 
apply (erule trancl.induct) 
17589  300 
apply (iprover dest: subsetD)+ 
12691  301 
done 
302 

13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

303 
lemma r_into_trancl': "!!p. p : r ==> p : r^+" 
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

304 
by (simp only: split_tupled_all) (erule r_into_trancl) 
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

305 

12691  306 
text {* 
307 
\medskip Conversions between @{text trancl} and @{text rtrancl}. 

308 
*} 

309 

22262  310 
lemma trancl_into_rtrancl': "r^++ a b ==> r^** a b" 
17589  311 
by (erule trancl.induct) iprover+ 
12691  312 

22262  313 
lemmas trancl_into_rtrancl = trancl_into_rtrancl' [to_set] 
314 

315 
lemma rtrancl_into_trancl1': assumes r: "r^** a b" 

316 
shows "!!c. r b c ==> r^++ a c" using r 

17589  317 
by induct iprover+ 
12691  318 

22262  319 
lemmas rtrancl_into_trancl1 = rtrancl_into_trancl1' [to_set] 
320 

321 
lemma rtrancl_into_trancl2': "[ r a b; r^** b c ] ==> r^++ a c" 

12691  322 
 {* intro rule from @{text r} and @{text rtrancl} *} 
22262  323 
apply (erule rtrancl.cases, iprover) 
324 
apply (rule rtrancl_trans' [THEN rtrancl_into_trancl1']) 

325 
apply (simp  rule r_into_rtrancl')+ 

12691  326 
done 
327 

22262  328 
lemmas rtrancl_into_trancl2 = rtrancl_into_trancl2' [to_set] 
329 

330 
lemma trancl_induct' [consumes 1, induct set: trancl]: 

331 
assumes a: "r^++ a b" 

332 
and cases: "!!y. r a y ==> P y" 

333 
"!!y z. r^++ a y ==> r y z ==> P y ==> P z" 

13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

334 
shows "P b" 
12691  335 
 {* Nice induction rule for @{text trancl} *} 
336 
proof  

13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

337 
from a have "a = a > P b" 
17589  338 
by (induct "%x y. x = a > P y" a b) (iprover intro: cases)+ 
339 
thus ?thesis by iprover 

12691  340 
qed 
341 

22262  342 
lemmas trancl_induct [consumes 1, induct set: trancl_set] = trancl_induct' [to_set] 
343 

344 
lemmas trancl_induct2' = 

345 
trancl_induct'[of _ "(ax,ay)" "(bx,by)", split_rule, 

346 
consumes 1, case_names base step] 

347 

22172  348 
lemmas trancl_induct2 = 
349 
trancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete), 

350 
consumes 1, case_names base step] 

351 

22262  352 
lemma trancl_trans_induct': 
353 
assumes major: "r^++ x y" 

354 
and cases: "!!x y. r x y ==> P x y" 

355 
"!!x y z. [ r^++ x y; P x y; r^++ y z; P y z ] ==> P x z" 

18372  356 
shows "P x y" 
12691  357 
 {* Another induction rule for trancl, incorporating transitivity *} 
22262  358 
by (iprover intro: major [THEN trancl_induct'] cases) 
359 

360 
lemmas trancl_trans_induct = trancl_trans_induct' [to_set] 

12691  361 

22262  362 
lemma tranclE: 
363 
assumes H: "(a, b) : r^+" 

364 
and cases: "(a, b) : r ==> P" "\<And>c. (a, c) : r^+ ==> (c, b) : r ==> P" 

365 
shows P 

366 
using H [simplified trancl_set_def, simplified] 

367 
by cases (auto intro: cases [simplified trancl_set_def, simplified]) 

10980  368 

22080
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

369 
lemma trancl_Int_subset: "[ r \<subseteq> s; r O (r^+ \<inter> s) \<subseteq> s] ==> r^+ \<subseteq> s" 
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

370 
apply (rule subsetI) 
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

371 
apply (rule_tac p="x" in PairE, clarify) 
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

372 
apply (erule trancl_induct, auto) 
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

373 
done 
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

374 

20716
a6686a8e1b68
Changed precedence of "op O" (relation composition) from 60 to 75.
krauss
parents:
19656
diff
changeset

375 
lemma trancl_unfold: "r^+ = r Un r O r^+" 
15551  376 
by (auto intro: trancl_into_trancl elim: tranclE) 
377 

19623  378 
lemma trans_trancl[simp]: "trans(r^+)" 
12691  379 
 {* Transitivity of @{term "r^+"} *} 
13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

380 
proof (rule transI) 
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

381 
fix x y z 
18372  382 
assume xy: "(x, y) \<in> r^+" 
13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

383 
assume "(y, z) \<in> r^+" 
18372  384 
thus "(x, z) \<in> r^+" by induct (insert xy, iprover)+ 
13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

385 
qed 
12691  386 

387 
lemmas trancl_trans = trans_trancl [THEN transD, standard] 

388 

22262  389 
lemma trancl_trans': 
390 
assumes xy: "r^++ x y" 

391 
and yz: "r^++ y z" 

392 
shows "r^++ x z" using yz xy 

393 
by induct iprover+ 

394 

19623  395 
lemma trancl_id[simp]: "trans r \<Longrightarrow> r^+ = r" 
396 
apply(auto) 

397 
apply(erule trancl_induct) 

398 
apply assumption 

399 
apply(unfold trans_def) 

400 
apply(blast) 

401 
done 

402 

22262  403 
lemma rtrancl_trancl_trancl': assumes r: "r^** x y" 
404 
shows "!!z. r^++ y z ==> r^++ x z" using r 

405 
by induct (iprover intro: trancl_trans')+ 

12691  406 

22262  407 
lemmas rtrancl_trancl_trancl = rtrancl_trancl_trancl' [to_set] 
408 

409 
lemma trancl_into_trancl2': "r a b ==> r^++ b c ==> r^++ a c" 

410 
by (erule trancl_trans' [OF trancl.r_into_trancl]) 

411 

412 
lemmas trancl_into_trancl2 = trancl_into_trancl2' [to_set] 

12691  413 

414 
lemma trancl_insert: 

415 
"(insert (y, x) r)^+ = r^+ \<union> {(a, b). (a, y) \<in> r^* \<and> (x, b) \<in> r^*}" 

416 
 {* primitive recursion for @{text trancl} over finite relations *} 

417 
apply (rule equalityI) 

418 
apply (rule subsetI) 

419 
apply (simp only: split_tupled_all) 

14208  420 
apply (erule trancl_induct, blast) 
12691  421 
apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl r_into_trancl trancl_trans) 
422 
apply (rule subsetI) 

423 
apply (blast intro: trancl_mono rtrancl_mono 

424 
[THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2) 

425 
done 

426 

22262  427 
lemma trancl_converseI': "(r^++)^1 x y ==> (r^1)^++ x y" 
428 
apply (drule conversepD) 

429 
apply (erule trancl_induct') 

430 
apply (iprover intro: conversepI trancl_trans')+ 

12691  431 
done 
432 

22262  433 
lemmas trancl_converseI = trancl_converseI' [to_set] 
434 

435 
lemma trancl_converseD': "(r^1)^++ x y ==> (r^++)^1 x y" 

436 
apply (rule conversepI) 

437 
apply (erule trancl_induct') 

438 
apply (iprover dest: conversepD intro: trancl_trans')+ 

13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

439 
done 
12691  440 

22262  441 
lemmas trancl_converseD = trancl_converseD' [to_set] 
442 

443 
lemma trancl_converse': "(r^1)^++ = (r^++)^1" 

444 
by (fastsimp simp add: expand_fun_eq 

445 
intro!: trancl_converseI' dest!: trancl_converseD') 

446 

447 
lemmas trancl_converse = trancl_converse' [to_set] 

12691  448 

19228  449 
lemma sym_trancl: "sym r ==> sym (r^+)" 
450 
by (simp only: sym_conv_converse_eq trancl_converse [symmetric]) 

451 

22262  452 
lemma converse_trancl_induct': 
453 
assumes major: "r^++ a b" 

454 
and cases: "!!y. r y b ==> P(y)" 

455 
"!!y z.[ r y z; r^++ z b; P(z) ] ==> P(y)" 

18372  456 
shows "P a" 
22262  457 
apply (rule trancl_induct' [OF trancl_converseI', OF conversepI, OF major]) 
18372  458 
apply (rule cases) 
22262  459 
apply (erule conversepD) 
460 
apply (blast intro: prems dest!: trancl_converseD' conversepD) 

18372  461 
done 
12691  462 

22262  463 
lemmas converse_trancl_induct = converse_trancl_induct' [to_set] 
464 

465 
lemma tranclD': "R^++ x y ==> EX z. R x z \<and> R^** z y" 

466 
apply (erule converse_trancl_induct', auto) 

467 
apply (blast intro: rtrancl_trans') 

12691  468 
done 
469 

22262  470 
lemmas tranclD = tranclD' [to_set] 
471 

13867  472 
lemma irrefl_tranclI: "r^1 \<inter> r^* = {} ==> (x, x) \<notin> r^+" 
18372  473 
by (blast elim: tranclE dest: trancl_into_rtrancl) 
12691  474 

475 
lemma irrefl_trancl_rD: "!!X. ALL x. (x, x) \<notin> r^+ ==> (x, y) \<in> r ==> x \<noteq> y" 

476 
by (blast dest: r_into_trancl) 

477 

478 
lemma trancl_subset_Sigma_aux: 

479 
"(a, b) \<in> r^* ==> r \<subseteq> A \<times> A ==> a = b \<or> a \<in> A" 

18372  480 
by (induct rule: rtrancl_induct) auto 
12691  481 

482 
lemma trancl_subset_Sigma: "r \<subseteq> A \<times> A ==> r^+ \<subseteq> A \<times> A" 

13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

483 
apply (rule subsetI) 
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

484 
apply (simp only: split_tupled_all) 
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

485 
apply (erule tranclE) 
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

486 
apply (blast dest!: trancl_into_rtrancl trancl_subset_Sigma_aux)+ 
12691  487 
done 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

488 

22262  489 
lemma reflcl_trancl' [simp]: "(r^++)^== = r^**" 
490 
apply (safe intro!: order_antisym) 

491 
apply (erule trancl_into_rtrancl') 

492 
apply (blast elim: rtrancl.cases dest: rtrancl_into_trancl1') 

11084  493 
done 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

494 

22262  495 
lemmas reflcl_trancl [simp] = reflcl_trancl' [to_set] 
496 

11090  497 
lemma trancl_reflcl [simp]: "(r^=)^+ = r^*" 
11084  498 
apply safe 
14208  499 
apply (drule trancl_into_rtrancl, simp) 
500 
apply (erule rtranclE, safe) 

501 
apply (rule r_into_trancl, simp) 

11084  502 
apply (rule rtrancl_into_trancl1) 
14208  503 
apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD], fast) 
11084  504 
done 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

505 

11090  506 
lemma trancl_empty [simp]: "{}^+ = {}" 
11084  507 
by (auto elim: trancl_induct) 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

508 

11090  509 
lemma rtrancl_empty [simp]: "{}^* = Id" 
11084  510 
by (rule subst [OF reflcl_trancl]) simp 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

511 

22262  512 
lemma rtranclD': "R^** a b ==> a = b \<or> a \<noteq> b \<and> R^++ a b" 
513 
by (force simp add: reflcl_trancl' [symmetric] simp del: reflcl_trancl') 

514 

515 
lemmas rtranclD = rtranclD' [to_set] 

11084  516 

16514  517 
lemma rtrancl_eq_or_trancl: 
518 
"(x,y) \<in> R\<^sup>* = (x=y \<or> x\<noteq>y \<and> (x,y) \<in> R\<^sup>+)" 

519 
by (fast elim: trancl_into_rtrancl dest: rtranclD) 

10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

520 

12691  521 
text {* @{text Domain} and @{text Range} *} 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

522 

11090  523 
lemma Domain_rtrancl [simp]: "Domain (R^*) = UNIV" 
11084  524 
by blast 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

525 

11090  526 
lemma Range_rtrancl [simp]: "Range (R^*) = UNIV" 
11084  527 
by blast 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

528 

11090  529 
lemma rtrancl_Un_subset: "(R^* \<union> S^*) \<subseteq> (R Un S)^*" 
11084  530 
by (rule rtrancl_Un_rtrancl [THEN subst]) fast 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

531 

11090  532 
lemma in_rtrancl_UnI: "x \<in> R^* \<or> x \<in> S^* ==> x \<in> (R \<union> S)^*" 
11084  533 
by (blast intro: subsetD [OF rtrancl_Un_subset]) 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

534 

11090  535 
lemma trancl_domain [simp]: "Domain (r^+) = Domain r" 
11084  536 
by (unfold Domain_def) (blast dest: tranclD) 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

537 

11090  538 
lemma trancl_range [simp]: "Range (r^+) = Range r" 
11084  539 
by (simp add: Range_def trancl_converse [symmetric]) 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

540 

11115  541 
lemma Not_Domain_rtrancl: 
12691  542 
"x ~: Domain R ==> ((x, y) : R^*) = (x = y)" 
543 
apply auto 

544 
by (erule rev_mp, erule rtrancl_induct, auto) 

545 

11327
cd2c27a23df1
Transitive closure is now defined via "inductive".
berghofe
parents:
11115
diff
changeset

546 

12691  547 
text {* More about converse @{text rtrancl} and @{text trancl}, should 
548 
be merged with main body. *} 

12428
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

549 

14337
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

550 
lemma single_valued_confluent: 
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

551 
"\<lbrakk> single_valued r; (x,y) \<in> r^*; (x,z) \<in> r^* \<rbrakk> 
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

552 
\<Longrightarrow> (y,z) \<in> r^* \<or> (z,y) \<in> r^*" 
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

553 
apply(erule rtrancl_induct) 
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

554 
apply simp 
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

555 
apply(erule disjE) 
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

556 
apply(blast elim:converse_rtranclE dest:single_valuedD) 
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

557 
apply(blast intro:rtrancl_trans) 
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

558 
done 
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

559 

12691  560 
lemma r_r_into_trancl: "(a, b) \<in> R ==> (b, c) \<in> R ==> (a, c) \<in> R^+" 
12428
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

561 
by (fast intro: trancl_trans) 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

562 

f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

563 
lemma trancl_into_trancl [rule_format]: 
12691  564 
"(a, b) \<in> r\<^sup>+ ==> (b, c) \<in> r > (a,c) \<in> r\<^sup>+" 
565 
apply (erule trancl_induct) 

12428
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

566 
apply (fast intro: r_r_into_trancl) 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

567 
apply (fast intro: r_r_into_trancl trancl_trans) 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

568 
done 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

569 

22262  570 
lemma trancl_rtrancl_trancl': 
571 
"r\<^sup>+\<^sup>+ a b ==> r\<^sup>*\<^sup>* b c ==> r\<^sup>+\<^sup>+ a c" 

572 
apply (drule tranclD') 

12428
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

573 
apply (erule exE, erule conjE) 
22262  574 
apply (drule rtrancl_trans', assumption) 
575 
apply (drule rtrancl_into_trancl2', assumption, assumption) 

12428
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

576 
done 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

577 

22262  578 
lemmas trancl_rtrancl_trancl = trancl_rtrancl_trancl' [to_set] 
579 

12691  580 
lemmas transitive_closure_trans [trans] = 
581 
r_r_into_trancl trancl_trans rtrancl_trans 

582 
trancl_into_trancl trancl_into_trancl2 

583 
rtrancl_into_rtrancl converse_rtrancl_into_rtrancl 

584 
rtrancl_trancl_trancl trancl_rtrancl_trancl 

12428
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

585 

22262  586 
lemmas transitive_closure_trans' [trans] = 
587 
trancl_trans' rtrancl_trans' 

588 
trancl.trancl_into_trancl trancl_into_trancl2' 

589 
rtrancl.rtrancl_into_rtrancl converse_rtrancl_into_rtrancl' 

590 
rtrancl_trancl_trancl' trancl_rtrancl_trancl' 

591 

12428
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

592 
declare trancl_into_rtrancl [elim] 
11327
cd2c27a23df1
Transitive closure is now defined via "inductive".
berghofe
parents:
11115
diff
changeset

593 

22262  594 
declare rtranclE [cases set: rtrancl_set] 
595 
declare tranclE [cases set: trancl_set] 

11327
cd2c27a23df1
Transitive closure is now defined via "inductive".
berghofe
parents:
11115
diff
changeset

596 

15551  597 

598 

599 

600 

15076
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

601 
subsection {* Setup of transitivity reasoner *} 
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

602 

4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

603 
ML_setup {* 
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

604 

4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

605 
structure Trancl_Tac = Trancl_Tac_Fun ( 
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

606 
struct 
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

607 
val r_into_trancl = thm "r_into_trancl"; 
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

608 
val trancl_trans = thm "trancl_trans"; 
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

609 
val rtrancl_refl = thm "rtrancl_refl"; 
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

610 
val r_into_rtrancl = thm "r_into_rtrancl"; 
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

611 
val trancl_into_rtrancl = thm "trancl_into_rtrancl"; 
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

612 
val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl"; 
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

613 
val trancl_rtrancl_trancl = thm "trancl_rtrancl_trancl"; 
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

614 
val rtrancl_trans = thm "rtrancl_trans"; 
15096  615 

18372  616 
fun decomp (Trueprop $ t) = 
617 
let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) = 

22262  618 
let fun decr (Const ("Transitive_Closure.rtrancl_set", _ ) $ r) = (r,"r*") 
619 
 decr (Const ("Transitive_Closure.trancl_set", _ ) $ r) = (r,"r+") 

18372  620 
 decr r = (r,"r"); 
621 
val (rel,r) = decr rel; 

622 
in SOME (a,b,rel,r) end 

623 
 dec _ = NONE 

15076
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

624 
in dec t end; 
18372  625 

21589  626 
end); 
15076
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

627 

22262  628 
structure Tranclp_Tac = Trancl_Tac_Fun ( 
629 
struct 

630 
val r_into_trancl = thm "trancl.r_into_trancl"; 

631 
val trancl_trans = thm "trancl_trans'"; 

632 
val rtrancl_refl = thm "rtrancl.rtrancl_refl"; 

633 
val r_into_rtrancl = thm "r_into_rtrancl'"; 

634 
val trancl_into_rtrancl = thm "trancl_into_rtrancl'"; 

635 
val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl'"; 

636 
val trancl_rtrancl_trancl = thm "trancl_rtrancl_trancl'"; 

637 
val rtrancl_trans = thm "rtrancl_trans'"; 

638 

639 
fun decomp (Trueprop $ t) = 

640 
let fun dec (rel $ a $ b) = 

641 
let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*") 

642 
 decr (Const ("Transitive_Closure.trancl", _ ) $ r) = (r,"r+") 

643 
 decr r = (r,"r"); 

644 
val (rel,r) = decr rel; 

645 
in SOME (a, b, Envir.beta_eta_contract rel, r) end 

646 
 dec _ = NONE 

647 
in dec t end; 

648 

649 
end); 

650 

17876  651 
change_simpset (fn ss => ss 
652 
addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac)) 

22262  653 
addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac)) 
654 
addSolver (mk_solver "Tranclp" (fn _ => Tranclp_Tac.trancl_tac)) 

655 
addSolver (mk_solver "Rtranclp" (fn _ => Tranclp_Tac.rtrancl_tac))); 

15076
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

656 

4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

657 
*} 
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

658 

21589  659 
(* Optional methods *) 
15076
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

660 

4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

661 
method_setup trancl = 
21589  662 
{* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.trancl_tac) *} 
18372  663 
{* simple transitivity reasoner *} 
15076
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

664 
method_setup rtrancl = 
21589  665 
{* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *} 
15076
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

666 
{* simple transitivity reasoner *} 
22262  667 
method_setup tranclp = 
668 
{* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *} 

669 
{* simple transitivity reasoner (predicate version) *} 

670 
method_setup rtranclp = 

671 
{* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *} 

672 
{* simple transitivity reasoner (predicate version) *} 

15076
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

673 

10213  674 
end 