src/HOL/Relation.thy
 changeset 46692 1f8b766224f6 parent 46691 72d81e789106 child 46694 0988b22e2626
```     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 -
1.34 -notation (xsymbols)
1.35 -  converse  ("(_\<inverse>)" [1000] 999)
1.36 -
1.37 -definition
1.38 -  rel_comp  :: "[('a * 'b) set, ('b * 'c) set] => ('a * 'c) set"
1.39 -    (infixr "O" 75) where
1.40 -  "r O s = {(x,z). EX y. (x, y) : r & (y, z) : s}"
1.41 -
1.42 -definition
1.43 -  Image :: "[('a * 'b) set, 'a set] => 'b set"
1.44 -    (infixl "``" 90) where
1.45 -  "r `` s = {y. EX x:s. (x,y):r}"
1.46 +lemma subrelI: -- {* Version of @{thm [source] subsetI} for binary relations *}
1.47 +  "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (x, y) \<in> s) \<Longrightarrow> r \<subseteq> s"
1.48 +  by auto
1.49
1.50 -definition
1.51 -  Id :: "('a * 'a) set" where -- {* the identity relation *}
1.52 -  "Id = {p. EX x. p = (x,x)}"
1.53 -
1.54 -definition
1.55 -  Id_on  :: "'a set => ('a * 'a) set" where -- {* diagonal: identity over a set *}
1.56 -  "Id_on A = (\<Union>x\<in>A. {(x,x)})"
1.57 +lemma lfp_induct2: -- {* Version of @{thm [source] lfp_induct} for binary relations *}
1.58 +  "(a, b) \<in> lfp f \<Longrightarrow> mono f \<Longrightarrow>
1.59 +    (\<And>a b. (a, b) \<in> f (lfp f \<inter> {(x, y). P x y}) \<Longrightarrow> P a b) \<Longrightarrow> P a b"
1.60 +  using lfp_induct_set [of "(a, b)" f "prod_case P"] by auto
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.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.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.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.240
1.241 @@ -214,9 +291,25 @@
1.242  lemma trans_Id: "trans Id"
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.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.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.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.418 -
1.419 -
1.420 -subsubsection {* Totality *}
1.421 -
1.422 -lemma total_on_empty[simp]: "total_on {} r"
1.424 -
1.425 -lemma total_on_diff_Id[simp]: "total_on A (r-Id) = total_on A r"
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.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.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 -by auto
1.561 -
1.562 -lemma Range_Collect_split [simp]: "Range{(x,y). P x y} = {y. EX x. P x y}"
1.563 -by auto
1.564 -
1.565 -lemma Image_Collect_split [simp]: "{(x,y). P x y} `` A = {y. EX x:A. P x y}"
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 *}
```