tuned structure; dropped already existing syntax declarations
authorhaftmann
Sun Feb 26 20:43:33 2012 +0100 (2012-02-26)
changeset 466921f8b766224f6
parent 46691 72d81e789106
child 46693 78bada13da46
tuned structure; dropped already existing syntax declarations
src/HOL/Relation.thy
     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.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 -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 *}