author  berghofe 
Wed, 20 Feb 2002 15:47:42 +0100  
changeset 12905  bbbae3f359e6 
parent 12487  bbd564190c9b 
child 12913  5ac498bffb6b 
permissions  rwrr 
10358  1 
(* Title: HOL/Relation.thy 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

2 
ID: $Id$ 
1983  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
4 
Copyright 1996 University of Cambridge 

1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

5 
*) 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

6 

12905  7 
header {* Relations *} 
8 

9 
theory Relation = Product_Type: 

5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5608
diff
changeset

10 

fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5608
diff
changeset

11 
constdefs 
10358  12 
converse :: "('a * 'b) set => ('b * 'a) set" ("(_^1)" [1000] 999) 
13 
"r^1 == {(y, x). (x, y) : r}" 

14 
syntax (xsymbols) 

12905  15 
converse :: "('a * 'b) set => ('b * 'a) set" ("(_\<inverse>)" [1000] 999) 
7912  16 

10358  17 
constdefs 
12487  18 
rel_comp :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set" (infixr "O" 60) 
7912  19 
"r O s == {(x,z). ? y. (x,y):s & (y,z):r}" 
5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5608
diff
changeset

20 

11136  21 
Image :: "[('a * 'b) set, 'a set] => 'b set" (infixl "``" 90) 
10832  22 
"r `` s == {y. ? x:s. (x,y):r}" 
7912  23 

12905  24 
Id :: "('a * 'a) set"  {* the identity relation *} 
7912  25 
"Id == {p. ? x. p = (x,x)}" 
26 

12905  27 
diag :: "'a set => ('a * 'a) set"  {* diagonal: identity over a set *} 
5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5608
diff
changeset

28 
"diag(A) == UN x:A. {(x,x)}" 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5608
diff
changeset

29 

11136  30 
Domain :: "('a * 'b) set => 'a set" 
5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5608
diff
changeset

31 
"Domain(r) == {x. ? y. (x,y):r}" 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5608
diff
changeset

32 

11136  33 
Range :: "('a * 'b) set => 'b set" 
5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5608
diff
changeset

34 
"Range(r) == Domain(r^1)" 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5608
diff
changeset

35 

11136  36 
Field :: "('a * 'a) set => 'a set" 
10786  37 
"Field r == Domain r Un Range r" 
38 

12905  39 
refl :: "['a set, ('a * 'a) set] => bool"  {* reflexivity over a set *} 
8703  40 
"refl A r == r <= A <*> A & (ALL x: A. (x,x) : r)" 
6806
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
5978
diff
changeset

41 

12905  42 
sym :: "('a * 'a) set => bool"  {* symmetry predicate *} 
6806
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
5978
diff
changeset

43 
"sym(r) == ALL x y. (x,y): r > (y,x): r" 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
5978
diff
changeset

44 

12905  45 
antisym:: "('a * 'a) set => bool"  {* antisymmetry predicate *} 
6806
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
5978
diff
changeset

46 
"antisym(r) == ALL x y. (x,y):r > (y,x):r > x=y" 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
5978
diff
changeset

47 

12905  48 
trans :: "('a * 'a) set => bool"  {* transitivity predicate *} 
5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5608
diff
changeset

49 
"trans(r) == (!x y z. (x,y):r > (y,z):r > (x,z):r)" 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5608
diff
changeset

50 

11136  51 
single_valued :: "('a * 'b) set => bool" 
10797  52 
"single_valued r == !x y. (x,y):r > (!z. (x,z):r > y=z)" 
5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5608
diff
changeset

53 

7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6806
diff
changeset

54 
fun_rel_comp :: "['a => 'b, ('b * 'c) set] => ('a => 'c) set" 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6806
diff
changeset

55 
"fun_rel_comp f R == {g. !x. (f x, g x) : R}" 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6806
diff
changeset

56 

11136  57 
inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set" 
58 
"inv_image r f == {(x,y). (f(x), f(y)) : r}" 

59 

6806
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
5978
diff
changeset

60 
syntax 
12905  61 
reflexive :: "('a * 'a) set => bool"  {* reflexivity over a type *} 
6806
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
5978
diff
changeset

62 
translations 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
5978
diff
changeset

63 
"reflexive" == "refl UNIV" 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
5978
diff
changeset

64 

12905  65 

66 
subsection {* Identity relation *} 

67 

68 
lemma IdI [intro]: "(a, a) : Id" 

69 
by (simp add: Id_def) 

70 

71 
lemma IdE [elim!]: "p : Id ==> (!!x. p = (x, x) ==> P) ==> P" 

72 
by (unfold Id_def) (rules elim: CollectE) 

73 

74 
lemma pair_in_Id_conv [iff]: "((a, b) : Id) = (a = b)" 

75 
by (unfold Id_def) blast 

76 

77 
lemma reflexive_Id: "reflexive Id" 

78 
by (simp add: refl_def) 

79 

80 
lemma antisym_Id: "antisym Id" 

81 
 {* A strange result, since @{text Id} is also symmetric. *} 

82 
by (simp add: antisym_def) 

83 

84 
lemma trans_Id: "trans Id" 

85 
by (simp add: trans_def) 

86 

87 

88 
subsection {* Diagonal relation: identity restricted to some set *} 

89 

90 
lemma diag_eqI: "a = b ==> a : A ==> (a, b) : diag A" 

91 
by (simp add: diag_def) 

92 

93 
lemma diagI [intro!]: "a : A ==> (a, a) : diag A" 

94 
by (rule diag_eqI) (rule refl) 

95 

96 
lemma diagE [elim!]: 

97 
"c : diag A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P" 

98 
 {* The general elimination rule *} 

99 
by (unfold diag_def) (rules elim!: UN_E singletonE) 

100 

101 
lemma diag_iff: "((x, y) : diag A) = (x = y & x : A)" 

102 
by blast 

103 

104 
lemma diag_subset_Times: "diag A <= A <*> A" 

105 
by blast 

106 

107 

108 
subsection {* Composition of two relations *} 

109 

110 
lemma rel_compI [intro]: 

111 
"(a, b) : s ==> (b, c) : r ==> (a, c) : r O s" 

112 
by (unfold rel_comp_def) blast 

113 

114 
lemma rel_compE [elim!]: "xz : r O s ==> 

115 
(!!x y z. xz = (x, z) ==> (x, y) : s ==> (y, z) : r ==> P) ==> P" 

116 
by (unfold rel_comp_def) (rules elim!: CollectE splitE exE conjE) 

117 

118 
lemma rel_compEpair: 

119 
"(a, c) : r O s ==> (!!y. (a, y) : s ==> (y, c) : r ==> P) ==> P" 

120 
by (rules elim: rel_compE Pair_inject ssubst) 

121 

122 
lemma R_O_Id [simp]: "R O Id = R" 

123 
by fast 

124 

125 
lemma Id_O_R [simp]: "Id O R = R" 

126 
by fast 

127 

128 
lemma O_assoc: "(R O S) O T = R O (S O T)" 

129 
by blast 

130 

131 
lemma trans_O_subset: "trans r ==> r O r <= r" 

132 
by (unfold trans_def) blast 

133 

134 
lemma rel_comp_mono: "[ r'<=r; s'<=s ] ==> (r' O s') <= (r O s)" 

135 
by blast 

136 

137 
lemma rel_comp_subset_Sigma: 

138 
"[ s <= A <*> B; r <= B <*> C ] ==> (r O s) <= A <*> C" 

139 
by blast 

140 

141 
subsection {* Natural deduction for refl(r) *} 

142 

143 
lemma reflI: "r <= A <*> A ==> (!!x. x : A ==> (x, x) : r) ==> refl A r" 

144 
by (unfold refl_def) (rules intro!: ballI) 

145 

146 
lemma reflD: "refl A r ==> a : A ==> (a, a) : r" 

147 
by (unfold refl_def) blast 

148 

149 
subsection {* Natural deduction for antisym(r) *} 

150 

151 
lemma antisymI: 

152 
"(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r" 

153 
by (unfold antisym_def) rules 

154 

155 
lemma antisymD: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b" 

156 
by (unfold antisym_def) rules 

157 

158 
subsection {* Natural deduction for trans(r) *} 

159 

160 
lemma transI: 

161 
"(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r" 

162 
by (unfold trans_def) rules 

163 

164 
lemma transD: "trans r ==> (a, b) : r ==> (b, c) : r ==> (a, c) : r" 

165 
by (unfold trans_def) rules 

166 

167 
subsection {* Natural deduction for r^1 *} 

168 

169 
lemma converse_iff [iff]: "((a,b): r^1) = ((b,a):r)" 

170 
by (simp add: converse_def) 

171 

172 
lemma converseI: "(a,b):r ==> (b,a): r^1" 

173 
by (simp add: converse_def) 

174 

175 
lemma converseD: "(a,b) : r^1 ==> (b,a) : r" 

176 
by (simp add: converse_def) 

177 

178 
(*More general than converseD, as it "splits" the member of the relation*) 

179 

180 
lemma converseE [elim!]: 

181 
"yx : r^1 ==> (!!x y. yx = (y, x) ==> (x, y) : r ==> P) ==> P" 

182 
by (unfold converse_def) (rules elim!: CollectE splitE bexE) 

183 

184 
lemma converse_converse [simp]: "(r^1)^1 = r" 

185 
by (unfold converse_def) blast 

186 

187 
lemma converse_rel_comp: "(r O s)^1 = s^1 O r^1" 

188 
by blast 

189 

190 
lemma converse_Id [simp]: "Id^1 = Id" 

191 
by blast 

192 

193 
lemma converse_diag [simp]: "(diag A) ^1 = diag A" 

194 
by blast 

195 

196 
lemma refl_converse: "refl A r ==> refl A (converse r)" 

197 
by (unfold refl_def) blast 

198 

199 
lemma antisym_converse: "antisym (converse r) = antisym r" 

200 
by (unfold antisym_def) blast 

201 

202 
lemma trans_converse: "trans (converse r) = trans r" 

203 
by (unfold trans_def) blast 

204 

205 
subsection {* Domain *} 

206 

207 
lemma Domain_iff: "(a : Domain r) = (EX y. (a, y) : r)" 

208 
by (unfold Domain_def) blast 

209 

210 
lemma DomainI [intro]: "(a, b) : r ==> a : Domain r" 

211 
by (rules intro!: iffD2 [OF Domain_iff]) 

212 

213 
lemma DomainE [elim!]: 

214 
"a : Domain r ==> (!!y. (a, y) : r ==> P) ==> P" 

215 
by (rules dest!: iffD1 [OF Domain_iff]) 

216 

217 
lemma Domain_empty [simp]: "Domain {} = {}" 

218 
by blast 

219 

220 
lemma Domain_insert: "Domain (insert (a, b) r) = insert a (Domain r)" 

221 
by blast 

222 

223 
lemma Domain_Id [simp]: "Domain Id = UNIV" 

224 
by blast 

225 

226 
lemma Domain_diag [simp]: "Domain (diag A) = A" 

227 
by blast 

228 

229 
lemma Domain_Un_eq: "Domain(A Un B) = Domain(A) Un Domain(B)" 

230 
by blast 

231 

232 
lemma Domain_Int_subset: "Domain(A Int B) <= Domain(A) Int Domain(B)" 

233 
by blast 

234 

235 
lemma Domain_Diff_subset: "Domain(A)  Domain(B) <= Domain(A  B)" 

236 
by blast 

237 

238 
lemma Domain_Union: "Domain (Union S) = (UN A:S. Domain A)" 

239 
by blast 

240 

241 
lemma Domain_mono: "r <= s ==> Domain r <= Domain s" 

242 
by blast 

243 

244 

245 
subsection {* Range *} 

246 

247 
lemma Range_iff: "(a : Range r) = (EX y. (y, a) : r)" 

248 
by (simp add: Domain_def Range_def) 

249 

250 
lemma RangeI [intro]: "(a, b) : r ==> b : Range r" 

251 
by (unfold Range_def) (rules intro!: converseI DomainI) 

252 

253 
lemma RangeE [elim!]: "b : Range r ==> (!!x. (x, b) : r ==> P) ==> P" 

254 
by (unfold Range_def) (rules elim!: DomainE dest!: converseD) 

255 

256 
lemma Range_empty [simp]: "Range {} = {}" 

257 
by blast 

258 

259 
lemma Range_insert: "Range (insert (a, b) r) = insert b (Range r)" 

260 
by blast 

261 

262 
lemma Range_Id [simp]: "Range Id = UNIV" 

263 
by blast 

264 

265 
lemma Range_diag [simp]: "Range (diag A) = A" 

266 
by auto 

267 

268 
lemma Range_Un_eq: "Range(A Un B) = Range(A) Un Range(B)" 

269 
by blast 

270 

271 
lemma Range_Int_subset: "Range(A Int B) <= Range(A) Int Range(B)" 

272 
by blast 

273 

274 
lemma Range_Diff_subset: "Range(A)  Range(B) <= Range(A  B)" 

275 
by blast 

276 

277 
lemma Range_Union: "Range (Union S) = (UN A:S. Range A)" 

278 
by blast 

279 

280 

281 
subsection {* Image of a set under a relation *} 

282 

283 
ML {* overload_1st_set "Relation.Image" *} 

284 

285 
lemma Image_iff: "(b : r``A) = (EX x:A. (x,b):r)" 

286 
by (simp add: Image_def) 

287 

288 
lemma Image_singleton: "r``{a} = {b. (a,b):r}" 

289 
by (simp add: Image_def) 

290 

291 
lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a,b):r)" 

292 
by (rule Image_iff [THEN trans]) simp 

293 

294 
lemma ImageI [intro]: "[ (a,b): r; a:A ] ==> b : r``A" 

295 
by (unfold Image_def) blast 

296 

297 
lemma ImageE [elim!]: 

298 
"b : r `` A ==> (!!x. (x, b) : r ==> x : A ==> P) ==> P" 

299 
by (unfold Image_def) (rules elim!: CollectE bexE) 

300 

301 
lemma rev_ImageI: "a : A ==> (a, b) : r ==> b : r `` A" 

302 
 {* This version's more effective when we already have the required @{text a} *} 

303 
by blast 

304 

305 
lemma Image_empty [simp]: "R``{} = {}" 

306 
by blast 

307 

308 
lemma Image_Id [simp]: "Id `` A = A" 

309 
by blast 

310 

311 
lemma Image_diag [simp]: "diag A `` B = A Int B" 

312 
by blast 

313 

314 
lemma Image_Int_subset: "R `` (A Int B) <= R `` A Int R `` B" 

315 
by blast 

316 

317 
lemma Image_Un: "R `` (A Un B) = R `` A Un R `` B" 

318 
by blast 

319 

320 
lemma Image_subset: "r <= A <*> B ==> r``C <= B" 

321 
by (rules intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2) 

322 

323 
lemma Image_eq_UN: "r``B = (UN y: B. r``{y})" 

324 
 {* NOT suitable for rewriting *} 

325 
by blast 

326 

327 
lemma Image_mono: "[ r'<=r; A'<=A ] ==> (r' `` A') <= (r `` A)" 

328 
by blast 

329 

330 
lemma Image_UN: "(r `` (UNION A B)) = (UN x:A.(r `` (B x)))" 

331 
by blast 

332 

333 
lemma Image_INT_subset: "(r `` (INTER A B)) <= (INT x:A.(r `` (B x)))" 

334 
 {* Converse inclusion fails *} 

335 
by blast 

336 

337 
lemma Image_subset_eq: "(r``A <= B) = (A <=  ((r^1) `` (B)))" 

338 
by blast 

339 

340 
subsection "single_valued" 

341 

342 
lemma single_valuedI: 

343 
"ALL x y. (x,y):r > (ALL z. (x,z):r > y=z) ==> single_valued r" 

344 
by (unfold single_valued_def) 

345 

346 
lemma single_valuedD: 

347 
"single_valued r ==> (x, y) : r ==> (x, z) : r ==> y = z" 

348 
by (simp add: single_valued_def) 

349 

350 

351 
subsection {* Graphs given by @{text Collect} *} 

352 

353 
lemma Domain_Collect_split [simp]: "Domain{(x,y). P x y} = {x. EX y. P x y}" 

354 
by auto 

355 

356 
lemma Range_Collect_split [simp]: "Range{(x,y). P x y} = {y. EX x. P x y}" 

357 
by auto 

358 

359 
lemma Image_Collect_split [simp]: "{(x,y). P x y} `` A = {y. EX x:A. P x y}" 

360 
by auto 

361 

362 

363 
subsection {* Composition of function and relation *} 

364 

365 
lemma fun_rel_comp_mono: "A <= B ==> fun_rel_comp f A <= fun_rel_comp f B" 

366 
by (unfold fun_rel_comp_def) fast 

367 

368 
lemma fun_rel_comp_unique: 

369 
"ALL x. EX! y. (f x, y) : R ==> EX! g. g : fun_rel_comp f R" 

370 
apply (unfold fun_rel_comp_def) 

371 
apply (rule_tac a = "%x. THE y. (f x, y) : R" in ex1I) 

372 
apply (fast dest!: theI') 

373 
apply (fast intro: ext the1_equality [symmetric]) 

374 
done 

375 

376 

377 
subsection "inverse image" 

378 

379 
lemma trans_inv_image: 

380 
"trans r ==> trans (inv_image r f)" 

381 
apply (unfold trans_def inv_image_def) 

382 
apply (simp (no_asm)) 

383 
apply blast 

384 
done 

385 

1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

386 
end 