1.1 --- a/src/HOL/Relation.thy Sun Feb 26 20:10:14 2012 +0100
1.2 +++ b/src/HOL/Relation.thy Sun Feb 26 20:43:33 2012 +0100
1.3 @@ -8,21 +8,6 @@
1.4 imports Datatype Finite_Set
1.5 begin
1.6
1.7 -notation
1.8 - bot ("\<bottom>") and
1.9 - top ("\<top>") and
1.10 - inf (infixl "\<sqinter>" 70) and
1.11 - sup (infixl "\<squnion>" 65) and
1.12 - Inf ("\<Sqinter>_" [900] 900) and
1.13 - Sup ("\<Squnion>_" [900] 900)
1.14 -
1.15 -syntax (xsymbols)
1.16 - "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
1.17 - "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
1.18 - "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
1.19 - "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
1.20 -
1.21 -
1.22 subsection {* Classical rules for reasoning on predicates *}
1.23
1.24 (* CANDIDATE declare predicate1I [Pure.intro!, intro!] *)
1.25 @@ -113,43 +98,17 @@
1.26
1.27 type_synonym 'a rel = "('a * 'a) set"
1.28
1.29 -definition
1.30 - converse :: "('a * 'b) set => ('b * 'a) set"
1.31 - ("(_^-1)" [1000] 999) where
1.32 - "r^-1 = {(y, x). (x, y) : r}"
1.33 +lemma subrelI: -- {* Version of @{thm [source] subsetI} for binary relations *}
1.34 + "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (x, y) \<in> s) \<Longrightarrow> r \<subseteq> s"
1.35 + by auto
1.36
1.37 -notation (xsymbols)
1.38 - converse ("(_\<inverse>)" [1000] 999)
1.39 +lemma lfp_induct2: -- {* Version of @{thm [source] lfp_induct} for binary relations *}
1.40 + "(a, b) \<in> lfp f \<Longrightarrow> mono f \<Longrightarrow>
1.41 + (\<And>a b. (a, b) \<in> f (lfp f \<inter> {(x, y). P x y}) \<Longrightarrow> P a b) \<Longrightarrow> P a b"
1.42 + using lfp_induct_set [of "(a, b)" f "prod_case P"] by auto
1.43
1.44 -definition
1.45 - rel_comp :: "[('a * 'b) set, ('b * 'c) set] => ('a * 'c) set"
1.46 - (infixr "O" 75) where
1.47 - "r O s = {(x,z). EX y. (x, y) : r & (y, z) : s}"
1.48
1.49 -definition
1.50 - Image :: "[('a * 'b) set, 'a set] => 'b set"
1.51 - (infixl "``" 90) where
1.52 - "r `` s = {y. EX x:s. (x,y):r}"
1.53 -
1.54 -definition
1.55 - Id :: "('a * 'a) set" where -- {* the identity relation *}
1.56 - "Id = {p. EX x. p = (x,x)}"
1.57 -
1.58 -definition
1.59 - Id_on :: "'a set => ('a * 'a) set" where -- {* diagonal: identity over a set *}
1.60 - "Id_on A = (\<Union>x\<in>A. {(x,x)})"
1.61 -
1.62 -definition
1.63 - Domain :: "('a * 'b) set => 'a set" where
1.64 - "Domain r = {x. EX y. (x,y):r}"
1.65 -
1.66 -definition
1.67 - Range :: "('a * 'b) set => 'b set" where
1.68 - "Range r = Domain(r^-1)"
1.69 -
1.70 -definition
1.71 - Field :: "('a * 'a) set => 'a set" where
1.72 - "Field r = Domain r \<union> Range r"
1.73 +subsubsection {* Reflexivity *}
1.74
1.75 definition
1.76 refl_on :: "['a set, ('a * 'a) set] => bool" where -- {* reflexivity over a set *}
1.77 @@ -159,39 +118,157 @@
1.78 refl :: "('a * 'a) set => bool" where -- {* reflexivity over a type *}
1.79 "refl \<equiv> refl_on UNIV"
1.80
1.81 -definition
1.82 - sym :: "('a * 'a) set => bool" where -- {* symmetry predicate *}
1.83 - "sym r \<longleftrightarrow> (ALL x y. (x,y): r --> (y,x): r)"
1.84 +lemma refl_onI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl_on A r"
1.85 +by (unfold refl_on_def) (iprover intro!: ballI)
1.86 +
1.87 +lemma refl_onD: "refl_on A r ==> a : A ==> (a, a) : r"
1.88 +by (unfold refl_on_def) blast
1.89 +
1.90 +lemma refl_onD1: "refl_on A r ==> (x, y) : r ==> x : A"
1.91 +by (unfold refl_on_def) blast
1.92 +
1.93 +lemma refl_onD2: "refl_on A r ==> (x, y) : r ==> y : A"
1.94 +by (unfold refl_on_def) blast
1.95 +
1.96 +lemma refl_on_Int: "refl_on A r ==> refl_on B s ==> refl_on (A \<inter> B) (r \<inter> s)"
1.97 +by (unfold refl_on_def) blast
1.98 +
1.99 +lemma refl_on_Un: "refl_on A r ==> refl_on B s ==> refl_on (A \<union> B) (r \<union> s)"
1.100 +by (unfold refl_on_def) blast
1.101 +
1.102 +lemma refl_on_INTER:
1.103 + "ALL x:S. refl_on (A x) (r x) ==> refl_on (INTER S A) (INTER S r)"
1.104 +by (unfold refl_on_def) fast
1.105 +
1.106 +lemma refl_on_UNION:
1.107 + "ALL x:S. refl_on (A x) (r x) \<Longrightarrow> refl_on (UNION S A) (UNION S r)"
1.108 +by (unfold refl_on_def) blast
1.109 +
1.110 +lemma refl_on_empty[simp]: "refl_on {} {}"
1.111 +by(simp add:refl_on_def)
1.112 +
1.113 +lemma refl_on_def' [nitpick_unfold, code]:
1.114 + "refl_on A r = ((\<forall>(x, y) \<in> r. x : A \<and> y : A) \<and> (\<forall>x \<in> A. (x, x) : r))"
1.115 +by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
1.116 +
1.117 +
1.118 +subsubsection {* Antisymmetry *}
1.119
1.120 definition
1.121 antisym :: "('a * 'a) set => bool" where -- {* antisymmetry predicate *}
1.122 "antisym r \<longleftrightarrow> (ALL x y. (x,y):r --> (y,x):r --> x=y)"
1.123
1.124 +lemma antisymI:
1.125 + "(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r"
1.126 +by (unfold antisym_def) iprover
1.127 +
1.128 +lemma antisymD: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b"
1.129 +by (unfold antisym_def) iprover
1.130 +
1.131 +lemma antisym_subset: "r \<subseteq> s ==> antisym s ==> antisym r"
1.132 +by (unfold antisym_def) blast
1.133 +
1.134 +lemma antisym_empty [simp]: "antisym {}"
1.135 +by (unfold antisym_def) blast
1.136 +
1.137 +
1.138 +subsubsection {* Symmetry *}
1.139 +
1.140 +definition
1.141 + sym :: "('a * 'a) set => bool" where -- {* symmetry predicate *}
1.142 + "sym r \<longleftrightarrow> (ALL x y. (x,y): r --> (y,x): r)"
1.143 +
1.144 +lemma symI: "(!!a b. (a, b) : r ==> (b, a) : r) ==> sym r"
1.145 +by (unfold sym_def) iprover
1.146 +
1.147 +lemma symD: "sym r ==> (a, b) : r ==> (b, a) : r"
1.148 +by (unfold sym_def, blast)
1.149 +
1.150 +lemma sym_Int: "sym r ==> sym s ==> sym (r \<inter> s)"
1.151 +by (fast intro: symI dest: symD)
1.152 +
1.153 +lemma sym_Un: "sym r ==> sym s ==> sym (r \<union> s)"
1.154 +by (fast intro: symI dest: symD)
1.155 +
1.156 +lemma sym_INTER: "ALL x:S. sym (r x) ==> sym (INTER S r)"
1.157 +by (fast intro: symI dest: symD)
1.158 +
1.159 +lemma sym_UNION: "ALL x:S. sym (r x) ==> sym (UNION S r)"
1.160 +by (fast intro: symI dest: symD)
1.161 +
1.162 +
1.163 +subsubsection {* Transitivity *}
1.164 +
1.165 definition
1.166 trans :: "('a * 'a) set => bool" where -- {* transitivity predicate *}
1.167 "trans r \<longleftrightarrow> (ALL x y z. (x,y):r --> (y,z):r --> (x,z):r)"
1.168
1.169 +lemma trans_join [code]:
1.170 + "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
1.171 + by (auto simp add: trans_def)
1.172 +
1.173 +lemma transI:
1.174 + "(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r"
1.175 +by (unfold trans_def) iprover
1.176 +
1.177 +lemma transD: "trans r ==> (a, b) : r ==> (b, c) : r ==> (a, c) : r"
1.178 +by (unfold trans_def) iprover
1.179 +
1.180 +lemma trans_Int: "trans r ==> trans s ==> trans (r \<inter> s)"
1.181 +by (fast intro: transI elim: transD)
1.182 +
1.183 +lemma trans_INTER: "ALL x:S. trans (r x) ==> trans (INTER S r)"
1.184 +by (fast intro: transI elim: transD)
1.185 +
1.186 +
1.187 +subsubsection {* Irreflexivity *}
1.188 +
1.189 definition
1.190 irrefl :: "('a * 'a) set => bool" where
1.191 "irrefl r \<longleftrightarrow> (\<forall>x. (x,x) \<notin> r)"
1.192
1.193 +lemma irrefl_distinct [code]:
1.194 + "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
1.195 + by (auto simp add: irrefl_def)
1.196 +
1.197 +
1.198 +subsubsection {* Totality *}
1.199 +
1.200 definition
1.201 total_on :: "'a set => ('a * 'a) set => bool" where
1.202 "total_on A r \<longleftrightarrow> (\<forall>x\<in>A.\<forall>y\<in>A. x\<noteq>y \<longrightarrow> (x,y)\<in>r \<or> (y,x)\<in>r)"
1.203
1.204 abbreviation "total \<equiv> total_on UNIV"
1.205
1.206 +lemma total_on_empty[simp]: "total_on {} r"
1.207 +by(simp add:total_on_def)
1.208 +
1.209 +
1.210 +subsubsection {* Single valued relations *}
1.211 +
1.212 definition
1.213 single_valued :: "('a * 'b) set => bool" where
1.214 "single_valued r \<longleftrightarrow> (ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z))"
1.215
1.216 -definition
1.217 - inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set" where
1.218 - "inv_image r f = {(x, y). (f x, f y) : r}"
1.219 +lemma single_valuedI:
1.220 + "ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z) ==> single_valued r"
1.221 +by (unfold single_valued_def)
1.222 +
1.223 +lemma single_valuedD:
1.224 + "single_valued r ==> (x, y) : r ==> (x, z) : r ==> y = z"
1.225 +by (simp add: single_valued_def)
1.226 +
1.227 +lemma single_valued_subset:
1.228 + "r \<subseteq> s ==> single_valued s ==> single_valued r"
1.229 +by (unfold single_valued_def) blast
1.230
1.231
1.232 subsubsection {* The identity relation *}
1.233
1.234 +definition
1.235 + Id :: "('a * 'a) set" where -- {* the identity relation *}
1.236 + "Id = {p. EX x. p = (x,x)}"
1.237 +
1.238 lemma IdI [intro]: "(a, a) : Id"
1.239 by (simp add: Id_def)
1.240
1.241 @@ -214,9 +291,25 @@
1.242 lemma trans_Id: "trans Id"
1.243 by (simp add: trans_def)
1.244
1.245 +lemma single_valued_Id [simp]: "single_valued Id"
1.246 + by (unfold single_valued_def) blast
1.247 +
1.248 +lemma irrefl_diff_Id [simp]: "irrefl (r - Id)"
1.249 + by (simp add:irrefl_def)
1.250 +
1.251 +lemma trans_diff_Id: "trans r \<Longrightarrow> antisym r \<Longrightarrow> trans (r - Id)"
1.252 + unfolding antisym_def trans_def by blast
1.253 +
1.254 +lemma total_on_diff_Id [simp]: "total_on A (r - Id) = total_on A r"
1.255 + by (simp add: total_on_def)
1.256 +
1.257
1.258 subsubsection {* Diagonal: identity over a set *}
1.259
1.260 +definition
1.261 + Id_on :: "'a set => ('a * 'a) set" where -- {* diagonal: identity over a set *}
1.262 + "Id_on A = (\<Union>x\<in>A. {(x,x)})"
1.263 +
1.264 lemma Id_on_empty [simp]: "Id_on {} = {}"
1.265 by (simp add: Id_on_def)
1.266
1.267 @@ -241,9 +334,29 @@
1.268 lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> A"
1.269 by blast
1.270
1.271 +lemma refl_on_Id_on: "refl_on A (Id_on A)"
1.272 +by (rule refl_onI [OF Id_on_subset_Times Id_onI])
1.273 +
1.274 +lemma antisym_Id_on [simp]: "antisym (Id_on A)"
1.275 +by (unfold antisym_def) blast
1.276 +
1.277 +lemma sym_Id_on [simp]: "sym (Id_on A)"
1.278 +by (rule symI) clarify
1.279 +
1.280 +lemma trans_Id_on [simp]: "trans (Id_on A)"
1.281 +by (fast intro: transI elim: transD)
1.282 +
1.283 +lemma single_valued_Id_on [simp]: "single_valued (Id_on A)"
1.284 + by (unfold single_valued_def) blast
1.285 +
1.286
1.287 subsubsection {* Composition of two relations *}
1.288
1.289 +definition
1.290 + rel_comp :: "[('a * 'b) set, ('b * 'c) set] => ('a * 'c) set"
1.291 + (infixr "O" 75) where
1.292 + "r O s = {(x,z). EX y. (x, y) : r & (y, z) : s}"
1.293 +
1.294 lemma rel_compI [intro]:
1.295 "(a, b) : r ==> (b, c) : s ==> (a, c) : r O s"
1.296 by (unfold rel_comp_def) blast
1.297 @@ -293,136 +406,21 @@
1.298 lemma rel_comp_UNION_distrib2: "UNION I r O s = UNION I (%i. r i O s)"
1.299 by auto
1.300
1.301 -
1.302 -subsubsection {* Reflexivity *}
1.303 -
1.304 -lemma refl_onI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl_on A r"
1.305 -by (unfold refl_on_def) (iprover intro!: ballI)
1.306 -
1.307 -lemma refl_onD: "refl_on A r ==> a : A ==> (a, a) : r"
1.308 -by (unfold refl_on_def) blast
1.309 -
1.310 -lemma refl_onD1: "refl_on A r ==> (x, y) : r ==> x : A"
1.311 -by (unfold refl_on_def) blast
1.312 -
1.313 -lemma refl_onD2: "refl_on A r ==> (x, y) : r ==> y : A"
1.314 -by (unfold refl_on_def) blast
1.315 -
1.316 -lemma refl_on_Int: "refl_on A r ==> refl_on B s ==> refl_on (A \<inter> B) (r \<inter> s)"
1.317 -by (unfold refl_on_def) blast
1.318 -
1.319 -lemma refl_on_Un: "refl_on A r ==> refl_on B s ==> refl_on (A \<union> B) (r \<union> s)"
1.320 -by (unfold refl_on_def) blast
1.321 -
1.322 -lemma refl_on_INTER:
1.323 - "ALL x:S. refl_on (A x) (r x) ==> refl_on (INTER S A) (INTER S r)"
1.324 -by (unfold refl_on_def) fast
1.325 -
1.326 -lemma refl_on_UNION:
1.327 - "ALL x:S. refl_on (A x) (r x) \<Longrightarrow> refl_on (UNION S A) (UNION S r)"
1.328 -by (unfold refl_on_def) blast
1.329 -
1.330 -lemma refl_on_empty[simp]: "refl_on {} {}"
1.331 -by(simp add:refl_on_def)
1.332 -
1.333 -lemma refl_on_Id_on: "refl_on A (Id_on A)"
1.334 -by (rule refl_onI [OF Id_on_subset_Times Id_onI])
1.335 -
1.336 -lemma refl_on_def' [nitpick_unfold, code]:
1.337 - "refl_on A r = ((\<forall>(x, y) \<in> r. x : A \<and> y : A) \<and> (\<forall>x \<in> A. (x, x) : r))"
1.338 -by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
1.339 -
1.340 -
1.341 -subsubsection {* Antisymmetry *}
1.342 -
1.343 -lemma antisymI:
1.344 - "(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r"
1.345 -by (unfold antisym_def) iprover
1.346 -
1.347 -lemma antisymD: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b"
1.348 -by (unfold antisym_def) iprover
1.349 -
1.350 -lemma antisym_subset: "r \<subseteq> s ==> antisym s ==> antisym r"
1.351 -by (unfold antisym_def) blast
1.352 -
1.353 -lemma antisym_empty [simp]: "antisym {}"
1.354 -by (unfold antisym_def) blast
1.355 -
1.356 -lemma antisym_Id_on [simp]: "antisym (Id_on A)"
1.357 -by (unfold antisym_def) blast
1.358 -
1.359 -
1.360 -subsubsection {* Symmetry *}
1.361 -
1.362 -lemma symI: "(!!a b. (a, b) : r ==> (b, a) : r) ==> sym r"
1.363 -by (unfold sym_def) iprover
1.364 -
1.365 -lemma symD: "sym r ==> (a, b) : r ==> (b, a) : r"
1.366 -by (unfold sym_def, blast)
1.367 -
1.368 -lemma sym_Int: "sym r ==> sym s ==> sym (r \<inter> s)"
1.369 -by (fast intro: symI dest: symD)
1.370 -
1.371 -lemma sym_Un: "sym r ==> sym s ==> sym (r \<union> s)"
1.372 -by (fast intro: symI dest: symD)
1.373 -
1.374 -lemma sym_INTER: "ALL x:S. sym (r x) ==> sym (INTER S r)"
1.375 -by (fast intro: symI dest: symD)
1.376 -
1.377 -lemma sym_UNION: "ALL x:S. sym (r x) ==> sym (UNION S r)"
1.378 -by (fast intro: symI dest: symD)
1.379 -
1.380 -lemma sym_Id_on [simp]: "sym (Id_on A)"
1.381 -by (rule symI) clarify
1.382 -
1.383 -
1.384 -subsubsection {* Transitivity *}
1.385 -
1.386 -lemma trans_join [code]:
1.387 - "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
1.388 - by (auto simp add: trans_def)
1.389 -
1.390 -lemma transI:
1.391 - "(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r"
1.392 -by (unfold trans_def) iprover
1.393 -
1.394 -lemma transD: "trans r ==> (a, b) : r ==> (b, c) : r ==> (a, c) : r"
1.395 -by (unfold trans_def) iprover
1.396 -
1.397 -lemma trans_Int: "trans r ==> trans s ==> trans (r \<inter> s)"
1.398 -by (fast intro: transI elim: transD)
1.399 -
1.400 -lemma trans_INTER: "ALL x:S. trans (r x) ==> trans (INTER S r)"
1.401 -by (fast intro: transI elim: transD)
1.402 -
1.403 -lemma trans_Id_on [simp]: "trans (Id_on A)"
1.404 -by (fast intro: transI elim: transD)
1.405 -
1.406 -lemma trans_diff_Id: " trans r \<Longrightarrow> antisym r \<Longrightarrow> trans (r-Id)"
1.407 -unfolding antisym_def trans_def by blast
1.408 -
1.409 -
1.410 -subsubsection {* Irreflexivity *}
1.411 -
1.412 -lemma irrefl_distinct [code]:
1.413 - "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
1.414 - by (auto simp add: irrefl_def)
1.415 -
1.416 -lemma irrefl_diff_Id[simp]: "irrefl(r-Id)"
1.417 -by(simp add:irrefl_def)
1.418 -
1.419 -
1.420 -subsubsection {* Totality *}
1.421 -
1.422 -lemma total_on_empty[simp]: "total_on {} r"
1.423 -by(simp add:total_on_def)
1.424 -
1.425 -lemma total_on_diff_Id[simp]: "total_on A (r-Id) = total_on A r"
1.426 -by(simp add: total_on_def)
1.427 +lemma single_valued_rel_comp:
1.428 + "single_valued r ==> single_valued s ==> single_valued (r O s)"
1.429 +by (unfold single_valued_def) blast
1.430
1.431
1.432 subsubsection {* Converse *}
1.433
1.434 +definition
1.435 + converse :: "('a * 'b) set => ('b * 'a) set"
1.436 + ("(_^-1)" [1000] 999) where
1.437 + "r^-1 = {(y, x). (x, y) : r}"
1.438 +
1.439 +notation (xsymbols)
1.440 + converse ("(_\<inverse>)" [1000] 999)
1.441 +
1.442 lemma converse_iff [iff]: "((a,b): r^-1) = ((b,a) : r)"
1.443 by (simp add: converse_def)
1.444
1.445 @@ -485,8 +483,33 @@
1.446 lemma total_on_converse[simp]: "total_on A (r^-1) = total_on A r"
1.447 by (auto simp: total_on_def)
1.448
1.449 +lemma finite_converse [iff]: "finite (r^-1) = finite r"
1.450 + apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
1.451 + apply simp
1.452 + apply (rule iffI)
1.453 + apply (erule finite_imageD [unfolded inj_on_def])
1.454 + apply (simp split add: split_split)
1.455 + apply (erule finite_imageI)
1.456 + apply (simp add: converse_def image_def, auto)
1.457 + apply (rule bexI)
1.458 + prefer 2 apply assumption
1.459 + apply simp
1.460 + done
1.461
1.462 -subsubsection {* Domain *}
1.463 +
1.464 +subsubsection {* Domain, range and field *}
1.465 +
1.466 +definition
1.467 + Domain :: "('a * 'b) set => 'a set" where
1.468 + "Domain r = {x. EX y. (x,y):r}"
1.469 +
1.470 +definition
1.471 + Range :: "('a * 'b) set => 'b set" where
1.472 + "Range r = Domain(r^-1)"
1.473 +
1.474 +definition
1.475 + Field :: "('a * 'a) set => 'a set" where
1.476 + "Field r = Domain r \<union> Range r"
1.477
1.478 declare Domain_def [no_atp]
1.479
1.480 @@ -546,8 +569,11 @@
1.481 lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
1.482 by auto
1.483
1.484 +lemma Domain_Collect_split [simp]: "Domain {(x, y). P x y} = {x. EX y. P x y}"
1.485 +by auto
1.486
1.487 -subsubsection {* Range *}
1.488 +lemma finite_Domain: "finite r ==> finite (Domain r)"
1.489 + by (induct set: finite) (auto simp add: Domain_insert)
1.490
1.491 lemma Range_iff: "(a : Range r) = (EX y. (y, a) : r)"
1.492 by (simp add: Domain_def Range_def)
1.493 @@ -595,8 +621,11 @@
1.494 lemma snd_eq_Range: "snd ` R = Range R"
1.495 by force
1.496
1.497 +lemma Range_Collect_split [simp]: "Range {(x, y). P x y} = {y. EX x. P x y}"
1.498 +by auto
1.499
1.500 -subsubsection {* Field *}
1.501 +lemma finite_Range: "finite r ==> finite (Range r)"
1.502 + by (induct set: finite) (auto simp add: Range_insert)
1.503
1.504 lemma mono_Field: "r \<subseteq> s \<Longrightarrow> Field r \<subseteq> Field s"
1.505 by(auto simp:Field_def Domain_def Range_def)
1.506 @@ -616,9 +645,20 @@
1.507 lemma Field_converse[simp]: "Field(r^-1) = Field r"
1.508 by(auto simp:Field_def)
1.509
1.510 +lemma finite_Field: "finite r ==> finite (Field r)"
1.511 + -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
1.512 + apply (induct set: finite)
1.513 + apply (auto simp add: Field_def Domain_insert Range_insert)
1.514 + done
1.515 +
1.516
1.517 subsubsection {* Image of a set under a relation *}
1.518
1.519 +definition
1.520 + Image :: "[('a * 'b) set, 'a set] => 'b set"
1.521 + (infixl "``" 90) where
1.522 + "r `` s = {y. EX x:s. (x,y):r}"
1.523 +
1.524 declare Image_def [no_atp]
1.525
1.526 lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)"
1.527 @@ -690,46 +730,16 @@
1.528 lemma Image_subset_eq: "(r``A \<subseteq> B) = (A \<subseteq> - ((r^-1) `` (-B)))"
1.529 by blast
1.530
1.531 -
1.532 -subsubsection {* Single valued relations *}
1.533 -
1.534 -lemma single_valuedI:
1.535 - "ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z) ==> single_valued r"
1.536 -by (unfold single_valued_def)
1.537 -
1.538 -lemma single_valuedD:
1.539 - "single_valued r ==> (x, y) : r ==> (x, z) : r ==> y = z"
1.540 -by (simp add: single_valued_def)
1.541 -
1.542 -lemma single_valued_rel_comp:
1.543 - "single_valued r ==> single_valued s ==> single_valued (r O s)"
1.544 -by (unfold single_valued_def) blast
1.545 -
1.546 -lemma single_valued_subset:
1.547 - "r \<subseteq> s ==> single_valued s ==> single_valued r"
1.548 -by (unfold single_valued_def) blast
1.549 -
1.550 -lemma single_valued_Id [simp]: "single_valued Id"
1.551 -by (unfold single_valued_def) blast
1.552 -
1.553 -lemma single_valued_Id_on [simp]: "single_valued (Id_on A)"
1.554 -by (unfold single_valued_def) blast
1.555 -
1.556 -
1.557 -subsubsection {* Graphs given by @{text Collect} *}
1.558 -
1.559 -lemma Domain_Collect_split [simp]: "Domain{(x,y). P x y} = {x. EX y. P x y}"
1.560 +lemma Image_Collect_split [simp]: "{(x, y). P x y} `` A = {y. EX x:A. P x y}"
1.561 by auto
1.562
1.563 -lemma Range_Collect_split [simp]: "Range{(x,y). P x y} = {y. EX x. P x y}"
1.564 -by auto
1.565 -
1.566 -lemma Image_Collect_split [simp]: "{(x,y). P x y} `` A = {y. EX x:A. P x y}"
1.567 -by auto
1.568 -
1.569
1.570 subsubsection {* Inverse image *}
1.571
1.572 +definition
1.573 + inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set" where
1.574 + "inv_image r f = {(x, y). (f x, f y) : r}"
1.575 +
1.576 lemma sym_inv_image: "sym r ==> sym (inv_image r f)"
1.577 by (unfold sym_def inv_image_def) blast
1.578
1.579 @@ -746,47 +756,6 @@
1.580 unfolding inv_image_def converse_def by auto
1.581
1.582
1.583 -subsubsection {* Finiteness *}
1.584 -
1.585 -lemma finite_converse [iff]: "finite (r^-1) = finite r"
1.586 - apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
1.587 - apply simp
1.588 - apply (rule iffI)
1.589 - apply (erule finite_imageD [unfolded inj_on_def])
1.590 - apply (simp split add: split_split)
1.591 - apply (erule finite_imageI)
1.592 - apply (simp add: converse_def image_def, auto)
1.593 - apply (rule bexI)
1.594 - prefer 2 apply assumption
1.595 - apply simp
1.596 - done
1.597 -
1.598 -lemma finite_Domain: "finite r ==> finite (Domain r)"
1.599 - by (induct set: finite) (auto simp add: Domain_insert)
1.600 -
1.601 -lemma finite_Range: "finite r ==> finite (Range r)"
1.602 - by (induct set: finite) (auto simp add: Range_insert)
1.603 -
1.604 -lemma finite_Field: "finite r ==> finite (Field r)"
1.605 - -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
1.606 - apply (induct set: finite)
1.607 - apply (auto simp add: Field_def Domain_insert Range_insert)
1.608 - done
1.609 -
1.610 -
1.611 -subsubsection {* Miscellaneous *}
1.612 -
1.613 -text {* Version of @{thm[source] lfp_induct} for binary relations *}
1.614 -
1.615 -lemmas lfp_induct2 =
1.616 - lfp_induct_set [of "(a, b)", split_format (complete)]
1.617 -
1.618 -text {* Version of @{thm[source] subsetI} for binary relations *}
1.619 -
1.620 -lemma subrelI: "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (x, y) \<in> s) \<Longrightarrow> r \<subseteq> s"
1.621 -by auto
1.622 -
1.623 -
1.624 subsection {* Relations as binary predicates *}
1.625
1.626 subsubsection {* Composition *}