author  paulson 
Wed, 15 Aug 2007 12:52:56 +0200  
changeset 24286  7619080e49f0 
parent 23709  fd31da8f752a 
child 24915  fc90277c0dd7 
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 

15131  9 
theory Relation 
23709  10 
imports Product_Type FixedPoint 
15131  11 
begin 
5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5608
diff
changeset

12 

12913  13 
subsection {* Definitions *} 
14 

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

15 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

16 
converse :: "('a * 'b) set => ('b * 'a) set" 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

17 
("(_^1)" [1000] 999) where 
10358  18 
"r^1 == {(y, x). (x, y) : r}" 
7912  19 

21210  20 
notation (xsymbols) 
19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19363
diff
changeset

21 
converse ("(_\<inverse>)" [1000] 999) 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19363
diff
changeset

22 

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

23 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

24 
rel_comp :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set" 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

25 
(infixr "O" 75) where 
12913  26 
"r O s == {(x,z). EX y. (x, y) : s & (y, z) : r}" 
27 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

28 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

29 
Image :: "[('a * 'b) set, 'a set] => 'b set" 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

30 
(infixl "``" 90) where 
12913  31 
"r `` s == {y. EX x:s. (x,y):r}" 
7912  32 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

33 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

34 
Id :: "('a * 'a) set" where  {* the identity relation *} 
12913  35 
"Id == {p. EX x. p = (x,x)}" 
7912  36 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

37 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

38 
diag :: "'a set => ('a * 'a) set" where  {* diagonal: identity over a set *} 
13830  39 
"diag A == \<Union>x\<in>A. {(x,x)}" 
12913  40 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

41 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

42 
Domain :: "('a * 'b) set => 'a set" where 
12913  43 
"Domain r == {x. EX y. (x,y):r}" 
5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5608
diff
changeset

44 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

45 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

46 
Range :: "('a * 'b) set => 'b set" where 
12913  47 
"Range r == Domain(r^1)" 
5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5608
diff
changeset

48 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

49 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

50 
Field :: "('a * 'a) set => 'a set" where 
13830  51 
"Field r == Domain r \<union> Range r" 
10786  52 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

53 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

54 
refl :: "['a set, ('a * 'a) set] => bool" where  {* reflexivity over a set *} 
12913  55 
"refl A r == r \<subseteq> A \<times> A & (ALL x: A. (x,x) : r)" 
6806
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
5978
diff
changeset

56 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

57 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

58 
sym :: "('a * 'a) set => bool" where  {* symmetry predicate *} 
12913  59 
"sym r == ALL x y. (x,y): r > (y,x): r" 
6806
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
5978
diff
changeset

60 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

61 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

62 
antisym :: "('a * 'a) set => bool" where  {* antisymmetry predicate *} 
12913  63 
"antisym r == ALL x y. (x,y):r > (y,x):r > x=y" 
6806
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
5978
diff
changeset

64 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

65 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

66 
trans :: "('a * 'a) set => bool" where  {* transitivity predicate *} 
12913  67 
"trans r == (ALL x y z. (x,y):r > (y,z):r > (x,z):r)" 
5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5608
diff
changeset

68 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

69 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

70 
single_valued :: "('a * 'b) set => bool" where 
12913  71 
"single_valued r == ALL x y. (x,y):r > (ALL z. (x,z):r > y=z)" 
7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6806
diff
changeset

72 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

73 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

74 
inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set" where 
12913  75 
"inv_image r f == {(x, y). (f x, f y) : r}" 
11136  76 

19363  77 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

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

80 

12905  81 

12913  82 
subsection {* The identity relation *} 
12905  83 

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

85 
by (simp add: Id_def) 

86 

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

17589  88 
by (unfold Id_def) (iprover elim: CollectE) 
12905  89 

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

91 
by (unfold Id_def) blast 

92 

93 
lemma reflexive_Id: "reflexive Id" 

94 
by (simp add: refl_def) 

95 

96 
lemma antisym_Id: "antisym Id" 

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

98 
by (simp add: antisym_def) 

99 

19228  100 
lemma sym_Id: "sym Id" 
101 
by (simp add: sym_def) 

102 

12905  103 
lemma trans_Id: "trans Id" 
104 
by (simp add: trans_def) 

105 

106 

12913  107 
subsection {* Diagonal: identity over a set *} 
12905  108 

13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13639
diff
changeset

109 
lemma diag_empty [simp]: "diag {} = {}" 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13639
diff
changeset

110 
by (simp add: diag_def) 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13639
diff
changeset

111 

12905  112 
lemma diag_eqI: "a = b ==> a : A ==> (a, b) : diag A" 
113 
by (simp add: diag_def) 

114 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23709
diff
changeset

115 
lemma diagI [intro!,noatp]: "a : A ==> (a, a) : diag A" 
12905  116 
by (rule diag_eqI) (rule refl) 
117 

118 
lemma diagE [elim!]: 

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

12913  120 
 {* The general elimination rule. *} 
17589  121 
by (unfold diag_def) (iprover elim!: UN_E singletonE) 
12905  122 

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

124 
by blast 

125 

12913  126 
lemma diag_subset_Times: "diag A \<subseteq> A \<times> A" 
12905  127 
by blast 
128 

129 

130 
subsection {* Composition of two relations *} 

131 

12913  132 
lemma rel_compI [intro]: 
12905  133 
"(a, b) : s ==> (b, c) : r ==> (a, c) : r O s" 
134 
by (unfold rel_comp_def) blast 

135 

12913  136 
lemma rel_compE [elim!]: "xz : r O s ==> 
12905  137 
(!!x y z. xz = (x, z) ==> (x, y) : s ==> (y, z) : r ==> P) ==> P" 
17589  138 
by (unfold rel_comp_def) (iprover elim!: CollectE splitE exE conjE) 
12905  139 

140 
lemma rel_compEpair: 

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

17589  142 
by (iprover elim: rel_compE Pair_inject ssubst) 
12905  143 

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

145 
by fast 

146 

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

148 
by fast 

149 

23185  150 
lemma rel_comp_empty1[simp]: "{} O R = {}" 
151 
by blast 

152 

153 
lemma rel_comp_empty2[simp]: "R O {} = {}" 

154 
by blast 

155 

12905  156 
lemma O_assoc: "(R O S) O T = R O (S O T)" 
157 
by blast 

158 

12913  159 
lemma trans_O_subset: "trans r ==> r O r \<subseteq> r" 
12905  160 
by (unfold trans_def) blast 
161 

12913  162 
lemma rel_comp_mono: "r' \<subseteq> r ==> s' \<subseteq> s ==> (r' O s') \<subseteq> (r O s)" 
12905  163 
by blast 
164 

165 
lemma rel_comp_subset_Sigma: 

12913  166 
"s \<subseteq> A \<times> B ==> r \<subseteq> B \<times> C ==> (r O s) \<subseteq> A \<times> C" 
12905  167 
by blast 
168 

12913  169 

170 
subsection {* Reflexivity *} 

171 

172 
lemma reflI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl A r" 

17589  173 
by (unfold refl_def) (iprover intro!: ballI) 
12905  174 

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

176 
by (unfold refl_def) blast 

177 

19228  178 
lemma reflD1: "refl A r ==> (x, y) : r ==> x : A" 
179 
by (unfold refl_def) blast 

180 

181 
lemma reflD2: "refl A r ==> (x, y) : r ==> y : A" 

182 
by (unfold refl_def) blast 

183 

184 
lemma refl_Int: "refl A r ==> refl B s ==> refl (A \<inter> B) (r \<inter> s)" 

185 
by (unfold refl_def) blast 

186 

187 
lemma refl_Un: "refl A r ==> refl B s ==> refl (A \<union> B) (r \<union> s)" 

188 
by (unfold refl_def) blast 

189 

190 
lemma refl_INTER: 

191 
"ALL x:S. refl (A x) (r x) ==> refl (INTER S A) (INTER S r)" 

192 
by (unfold refl_def) fast 

193 

194 
lemma refl_UNION: 

195 
"ALL x:S. refl (A x) (r x) \<Longrightarrow> refl (UNION S A) (UNION S r)" 

196 
by (unfold refl_def) blast 

197 

198 
lemma refl_diag: "refl A (diag A)" 

199 
by (rule reflI [OF diag_subset_Times diagI]) 

200 

12913  201 

202 
subsection {* Antisymmetry *} 

12905  203 

204 
lemma antisymI: 

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

17589  206 
by (unfold antisym_def) iprover 
12905  207 

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

17589  209 
by (unfold antisym_def) iprover 
12905  210 

19228  211 
lemma antisym_subset: "r \<subseteq> s ==> antisym s ==> antisym r" 
212 
by (unfold antisym_def) blast 

12913  213 

19228  214 
lemma antisym_empty [simp]: "antisym {}" 
215 
by (unfold antisym_def) blast 

216 

217 
lemma antisym_diag [simp]: "antisym (diag A)" 

218 
by (unfold antisym_def) blast 

219 

220 

221 
subsection {* Symmetry *} 

222 

223 
lemma symI: "(!!a b. (a, b) : r ==> (b, a) : r) ==> sym r" 

224 
by (unfold sym_def) iprover 

15177  225 

226 
lemma symD: "sym r ==> (a, b) : r ==> (b, a) : r" 

227 
by (unfold sym_def, blast) 

12905  228 

19228  229 
lemma sym_Int: "sym r ==> sym s ==> sym (r \<inter> s)" 
230 
by (fast intro: symI dest: symD) 

231 

232 
lemma sym_Un: "sym r ==> sym s ==> sym (r \<union> s)" 

233 
by (fast intro: symI dest: symD) 

234 

235 
lemma sym_INTER: "ALL x:S. sym (r x) ==> sym (INTER S r)" 

236 
by (fast intro: symI dest: symD) 

237 

238 
lemma sym_UNION: "ALL x:S. sym (r x) ==> sym (UNION S r)" 

239 
by (fast intro: symI dest: symD) 

240 

241 
lemma sym_diag [simp]: "sym (diag A)" 

242 
by (rule symI) clarify 

243 

244 

245 
subsection {* Transitivity *} 

246 

12905  247 
lemma transI: 
248 
"(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r" 

17589  249 
by (unfold trans_def) iprover 
12905  250 

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

17589  252 
by (unfold trans_def) iprover 
12905  253 

19228  254 
lemma trans_Int: "trans r ==> trans s ==> trans (r \<inter> s)" 
255 
by (fast intro: transI elim: transD) 

256 

257 
lemma trans_INTER: "ALL x:S. trans (r x) ==> trans (INTER S r)" 

258 
by (fast intro: transI elim: transD) 

259 

260 
lemma trans_diag [simp]: "trans (diag A)" 

261 
by (fast intro: transI elim: transD) 

262 

12905  263 

12913  264 
subsection {* Converse *} 
265 

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

12905  267 
by (simp add: converse_def) 
268 

13343  269 
lemma converseI[sym]: "(a, b) : r ==> (b, a) : r^1" 
12905  270 
by (simp add: converse_def) 
271 

13343  272 
lemma converseD[sym]: "(a,b) : r^1 ==> (b, a) : r" 
12905  273 
by (simp add: converse_def) 
274 

275 
lemma converseE [elim!]: 

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

12913  277 
 {* More general than @{text converseD}, as it ``splits'' the member of the relation. *} 
17589  278 
by (unfold converse_def) (iprover elim!: CollectE splitE bexE) 
12905  279 

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

281 
by (unfold converse_def) blast 

282 

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

284 
by blast 

285 

19228  286 
lemma converse_Int: "(r \<inter> s)^1 = r^1 \<inter> s^1" 
287 
by blast 

288 

289 
lemma converse_Un: "(r \<union> s)^1 = r^1 \<union> s^1" 

290 
by blast 

291 

292 
lemma converse_INTER: "(INTER S r)^1 = (INT x:S. (r x)^1)" 

293 
by fast 

294 

295 
lemma converse_UNION: "(UNION S r)^1 = (UN x:S. (r x)^1)" 

296 
by blast 

297 

12905  298 
lemma converse_Id [simp]: "Id^1 = Id" 
299 
by blast 

300 

12913  301 
lemma converse_diag [simp]: "(diag A)^1 = diag A" 
12905  302 
by blast 
303 

19228  304 
lemma refl_converse [simp]: "refl A (converse r) = refl A r" 
305 
by (unfold refl_def) auto 

12905  306 

19228  307 
lemma sym_converse [simp]: "sym (converse r) = sym r" 
308 
by (unfold sym_def) blast 

309 

310 
lemma antisym_converse [simp]: "antisym (converse r) = antisym r" 

12905  311 
by (unfold antisym_def) blast 
312 

19228  313 
lemma trans_converse [simp]: "trans (converse r) = trans r" 
12905  314 
by (unfold trans_def) blast 
315 

19228  316 
lemma sym_conv_converse_eq: "sym r = (r^1 = r)" 
317 
by (unfold sym_def) fast 

318 

319 
lemma sym_Un_converse: "sym (r \<union> r^1)" 

320 
by (unfold sym_def) blast 

321 

322 
lemma sym_Int_converse: "sym (r \<inter> r^1)" 

323 
by (unfold sym_def) blast 

324 

12913  325 

12905  326 
subsection {* Domain *} 
327 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23709
diff
changeset

328 
declare Domain_def [noatp] 
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23709
diff
changeset

329 

12905  330 
lemma Domain_iff: "(a : Domain r) = (EX y. (a, y) : r)" 
331 
by (unfold Domain_def) blast 

332 

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

17589  334 
by (iprover intro!: iffD2 [OF Domain_iff]) 
12905  335 

336 
lemma DomainE [elim!]: 

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

17589  338 
by (iprover dest!: iffD1 [OF Domain_iff]) 
12905  339 

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

341 
by blast 

342 

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

344 
by blast 

345 

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

347 
by blast 

348 

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

350 
by blast 

351 

13830  352 
lemma Domain_Un_eq: "Domain(A \<union> B) = Domain(A) \<union> Domain(B)" 
12905  353 
by blast 
354 

13830  355 
lemma Domain_Int_subset: "Domain(A \<inter> B) \<subseteq> Domain(A) \<inter> Domain(B)" 
12905  356 
by blast 
357 

12913  358 
lemma Domain_Diff_subset: "Domain(A)  Domain(B) \<subseteq> Domain(A  B)" 
12905  359 
by blast 
360 

13830  361 
lemma Domain_Union: "Domain (Union S) = (\<Union>A\<in>S. Domain A)" 
12905  362 
by blast 
363 

12913  364 
lemma Domain_mono: "r \<subseteq> s ==> Domain r \<subseteq> Domain s" 
12905  365 
by blast 
366 

22172  367 
lemma fst_eq_Domain: "fst ` R = Domain R"; 
368 
apply auto 

369 
apply (rule image_eqI, auto) 

370 
done 

371 

12905  372 

373 
subsection {* Range *} 

374 

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

376 
by (simp add: Domain_def Range_def) 

377 

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

17589  379 
by (unfold Range_def) (iprover intro!: converseI DomainI) 
12905  380 

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

17589  382 
by (unfold Range_def) (iprover elim!: DomainE dest!: converseD) 
12905  383 

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

385 
by blast 

386 

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

388 
by blast 

389 

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

391 
by blast 

392 

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

394 
by auto 

395 

13830  396 
lemma Range_Un_eq: "Range(A \<union> B) = Range(A) \<union> Range(B)" 
12905  397 
by blast 
398 

13830  399 
lemma Range_Int_subset: "Range(A \<inter> B) \<subseteq> Range(A) \<inter> Range(B)" 
12905  400 
by blast 
401 

12913  402 
lemma Range_Diff_subset: "Range(A)  Range(B) \<subseteq> Range(A  B)" 
12905  403 
by blast 
404 

13830  405 
lemma Range_Union: "Range (Union S) = (\<Union>A\<in>S. Range A)" 
12905  406 
by blast 
407 

22172  408 
lemma snd_eq_Range: "snd ` R = Range R"; 
409 
apply auto 

410 
apply (rule image_eqI, auto) 

411 
done 

412 

12905  413 

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

415 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23709
diff
changeset

416 
declare Image_def [noatp] 
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23709
diff
changeset

417 

12913  418 
lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)" 
12905  419 
by (simp add: Image_def) 
420 

12913  421 
lemma Image_singleton: "r``{a} = {b. (a, b) : r}" 
12905  422 
by (simp add: Image_def) 
423 

12913  424 
lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a, b) : r)" 
12905  425 
by (rule Image_iff [THEN trans]) simp 
426 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23709
diff
changeset

427 
lemma ImageI [intro,noatp]: "(a, b) : r ==> a : A ==> b : r``A" 
12905  428 
by (unfold Image_def) blast 
429 

430 
lemma ImageE [elim!]: 

12913  431 
"b : r `` A ==> (!!x. (x, b) : r ==> x : A ==> P) ==> P" 
17589  432 
by (unfold Image_def) (iprover elim!: CollectE bexE) 
12905  433 

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

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

436 
by blast 

437 

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

439 
by blast 

440 

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

442 
by blast 

443 

13830  444 
lemma Image_diag [simp]: "diag A `` B = A \<inter> B" 
445 
by blast 

446 

447 
lemma Image_Int_subset: "R `` (A \<inter> B) \<subseteq> R `` A \<inter> R `` B" 

12905  448 
by blast 
449 

13830  450 
lemma Image_Int_eq: 
451 
"single_valued (converse R) ==> R `` (A \<inter> B) = R `` A \<inter> R `` B" 

452 
by (simp add: single_valued_def, blast) 

12905  453 

13830  454 
lemma Image_Un: "R `` (A \<union> B) = R `` A \<union> R `` B" 
12905  455 
by blast 
456 

13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13639
diff
changeset

457 
lemma Un_Image: "(R \<union> S) `` A = R `` A \<union> S `` A" 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13639
diff
changeset

458 
by blast 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13639
diff
changeset

459 

12913  460 
lemma Image_subset: "r \<subseteq> A \<times> B ==> r``C \<subseteq> B" 
17589  461 
by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2) 
12905  462 

13830  463 
lemma Image_eq_UN: "r``B = (\<Union>y\<in> B. r``{y})" 
12905  464 
 {* NOT suitable for rewriting *} 
465 
by blast 

466 

12913  467 
lemma Image_mono: "r' \<subseteq> r ==> A' \<subseteq> A ==> (r' `` A') \<subseteq> (r `` A)" 
12905  468 
by blast 
469 

13830  470 
lemma Image_UN: "(r `` (UNION A B)) = (\<Union>x\<in>A. r `` (B x))" 
471 
by blast 

472 

473 
lemma Image_INT_subset: "(r `` INTER A B) \<subseteq> (\<Inter>x\<in>A. r `` (B x))" 

12905  474 
by blast 
475 

13830  476 
text{*Converse inclusion requires some assumptions*} 
477 
lemma Image_INT_eq: 

478 
"[single_valued (r\<inverse>); A\<noteq>{}] ==> r `` INTER A B = (\<Inter>x\<in>A. r `` B x)" 

479 
apply (rule equalityI) 

480 
apply (rule Image_INT_subset) 

481 
apply (simp add: single_valued_def, blast) 

482 
done 

12905  483 

12913  484 
lemma Image_subset_eq: "(r``A \<subseteq> B) = (A \<subseteq>  ((r^1) `` (B)))" 
12905  485 
by blast 
486 

487 

12913  488 
subsection {* Single valued relations *} 
489 

490 
lemma single_valuedI: 

12905  491 
"ALL x y. (x,y):r > (ALL z. (x,z):r > y=z) ==> single_valued r" 
492 
by (unfold single_valued_def) 

493 

494 
lemma single_valuedD: 

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

496 
by (simp add: single_valued_def) 

497 

19228  498 
lemma single_valued_rel_comp: 
499 
"single_valued r ==> single_valued s ==> single_valued (r O s)" 

500 
by (unfold single_valued_def) blast 

501 

502 
lemma single_valued_subset: 

503 
"r \<subseteq> s ==> single_valued s ==> single_valued r" 

504 
by (unfold single_valued_def) blast 

505 

506 
lemma single_valued_Id [simp]: "single_valued Id" 

507 
by (unfold single_valued_def) blast 

508 

509 
lemma single_valued_diag [simp]: "single_valued (diag A)" 

510 
by (unfold single_valued_def) blast 

511 

12905  512 

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

514 

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

516 
by auto 

517 

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

519 
by auto 

520 

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

522 
by auto 

523 

524 

12913  525 
subsection {* Inverse image *} 
12905  526 

19228  527 
lemma sym_inv_image: "sym r ==> sym (inv_image r f)" 
528 
by (unfold sym_def inv_image_def) blast 

529 

12913  530 
lemma trans_inv_image: "trans r ==> trans (inv_image r f)" 
12905  531 
apply (unfold trans_def inv_image_def) 
532 
apply (simp (no_asm)) 

533 
apply blast 

534 
done 

535 

23709  536 

537 
subsection {* Version of @{text lfp_induct} for binary relations *} 

538 

539 
lemmas lfp_induct2 = 

540 
lfp_induct_set [of "(a, b)", split_format (complete)] 

541 

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

542 
end 