src/HOL/Relation.thy
changeset 26271 e324f8918c98
parent 24915 fc90277c0dd7
child 26297 74012d599204
     1.1 --- a/src/HOL/Relation.thy	Fri Mar 14 12:18:56 2008 +0100
     1.2 +++ b/src/HOL/Relation.thy	Fri Mar 14 19:57:12 2008 +0100
     1.3 @@ -82,245 +82,245 @@
     1.4  subsection {* The identity relation *}
     1.5  
     1.6  lemma IdI [intro]: "(a, a) : Id"
     1.7 -  by (simp add: Id_def)
     1.8 +by (simp add: Id_def)
     1.9  
    1.10  lemma IdE [elim!]: "p : Id ==> (!!x. p = (x, x) ==> P) ==> P"
    1.11 -  by (unfold Id_def) (iprover elim: CollectE)
    1.12 +by (unfold Id_def) (iprover elim: CollectE)
    1.13  
    1.14  lemma pair_in_Id_conv [iff]: "((a, b) : Id) = (a = b)"
    1.15 -  by (unfold Id_def) blast
    1.16 +by (unfold Id_def) blast
    1.17  
    1.18  lemma reflexive_Id: "reflexive Id"
    1.19 -  by (simp add: refl_def)
    1.20 +by (simp add: refl_def)
    1.21  
    1.22  lemma antisym_Id: "antisym Id"
    1.23    -- {* A strange result, since @{text Id} is also symmetric. *}
    1.24 -  by (simp add: antisym_def)
    1.25 +by (simp add: antisym_def)
    1.26  
    1.27  lemma sym_Id: "sym Id"
    1.28 -  by (simp add: sym_def)
    1.29 +by (simp add: sym_def)
    1.30  
    1.31  lemma trans_Id: "trans Id"
    1.32 -  by (simp add: trans_def)
    1.33 +by (simp add: trans_def)
    1.34  
    1.35  
    1.36  subsection {* Diagonal: identity over a set *}
    1.37  
    1.38  lemma diag_empty [simp]: "diag {} = {}"
    1.39 -  by (simp add: diag_def) 
    1.40 +by (simp add: diag_def) 
    1.41  
    1.42  lemma diag_eqI: "a = b ==> a : A ==> (a, b) : diag A"
    1.43 -  by (simp add: diag_def)
    1.44 +by (simp add: diag_def)
    1.45  
    1.46  lemma diagI [intro!,noatp]: "a : A ==> (a, a) : diag A"
    1.47 -  by (rule diag_eqI) (rule refl)
    1.48 +by (rule diag_eqI) (rule refl)
    1.49  
    1.50  lemma diagE [elim!]:
    1.51    "c : diag A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P"
    1.52    -- {* The general elimination rule. *}
    1.53 -  by (unfold diag_def) (iprover elim!: UN_E singletonE)
    1.54 +by (unfold diag_def) (iprover elim!: UN_E singletonE)
    1.55  
    1.56  lemma diag_iff: "((x, y) : diag A) = (x = y & x : A)"
    1.57 -  by blast
    1.58 +by blast
    1.59  
    1.60  lemma diag_subset_Times: "diag A \<subseteq> A \<times> A"
    1.61 -  by blast
    1.62 +by blast
    1.63  
    1.64  
    1.65  subsection {* Composition of two relations *}
    1.66  
    1.67  lemma rel_compI [intro]:
    1.68    "(a, b) : s ==> (b, c) : r ==> (a, c) : r O s"
    1.69 -  by (unfold rel_comp_def) blast
    1.70 +by (unfold rel_comp_def) blast
    1.71  
    1.72  lemma rel_compE [elim!]: "xz : r O s ==>
    1.73    (!!x y z. xz = (x, z) ==> (x, y) : s ==> (y, z) : r  ==> P) ==> P"
    1.74 -  by (unfold rel_comp_def) (iprover elim!: CollectE splitE exE conjE)
    1.75 +by (unfold rel_comp_def) (iprover elim!: CollectE splitE exE conjE)
    1.76  
    1.77  lemma rel_compEpair:
    1.78    "(a, c) : r O s ==> (!!y. (a, y) : s ==> (y, c) : r ==> P) ==> P"
    1.79 -  by (iprover elim: rel_compE Pair_inject ssubst)
    1.80 +by (iprover elim: rel_compE Pair_inject ssubst)
    1.81  
    1.82  lemma R_O_Id [simp]: "R O Id = R"
    1.83 -  by fast
    1.84 +by fast
    1.85  
    1.86  lemma Id_O_R [simp]: "Id O R = R"
    1.87 -  by fast
    1.88 +by fast
    1.89  
    1.90  lemma rel_comp_empty1[simp]: "{} O R = {}"
    1.91 -  by blast
    1.92 +by blast
    1.93  
    1.94  lemma rel_comp_empty2[simp]: "R O {} = {}"
    1.95 -  by blast
    1.96 +by blast
    1.97  
    1.98  lemma O_assoc: "(R O S) O T = R O (S O T)"
    1.99 -  by blast
   1.100 +by blast
   1.101  
   1.102  lemma trans_O_subset: "trans r ==> r O r \<subseteq> r"
   1.103 -  by (unfold trans_def) blast
   1.104 +by (unfold trans_def) blast
   1.105  
   1.106  lemma rel_comp_mono: "r' \<subseteq> r ==> s' \<subseteq> s ==> (r' O s') \<subseteq> (r O s)"
   1.107 -  by blast
   1.108 +by blast
   1.109  
   1.110  lemma rel_comp_subset_Sigma:
   1.111      "s \<subseteq> A \<times> B ==> r \<subseteq> B \<times> C ==> (r O s) \<subseteq> A \<times> C"
   1.112 -  by blast
   1.113 +by blast
   1.114  
   1.115  
   1.116  subsection {* Reflexivity *}
   1.117  
   1.118  lemma reflI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl A r"
   1.119 -  by (unfold refl_def) (iprover intro!: ballI)
   1.120 +by (unfold refl_def) (iprover intro!: ballI)
   1.121  
   1.122  lemma reflD: "refl A r ==> a : A ==> (a, a) : r"
   1.123 -  by (unfold refl_def) blast
   1.124 +by (unfold refl_def) blast
   1.125  
   1.126  lemma reflD1: "refl A r ==> (x, y) : r ==> x : A"
   1.127 -  by (unfold refl_def) blast
   1.128 +by (unfold refl_def) blast
   1.129  
   1.130  lemma reflD2: "refl A r ==> (x, y) : r ==> y : A"
   1.131 -  by (unfold refl_def) blast
   1.132 +by (unfold refl_def) blast
   1.133  
   1.134  lemma refl_Int: "refl A r ==> refl B s ==> refl (A \<inter> B) (r \<inter> s)"
   1.135 -  by (unfold refl_def) blast
   1.136 +by (unfold refl_def) blast
   1.137  
   1.138  lemma refl_Un: "refl A r ==> refl B s ==> refl (A \<union> B) (r \<union> s)"
   1.139 -  by (unfold refl_def) blast
   1.140 +by (unfold refl_def) blast
   1.141  
   1.142  lemma refl_INTER:
   1.143    "ALL x:S. refl (A x) (r x) ==> refl (INTER S A) (INTER S r)"
   1.144 -  by (unfold refl_def) fast
   1.145 +by (unfold refl_def) fast
   1.146  
   1.147  lemma refl_UNION:
   1.148    "ALL x:S. refl (A x) (r x) \<Longrightarrow> refl (UNION S A) (UNION S r)"
   1.149 -  by (unfold refl_def) blast
   1.150 +by (unfold refl_def) blast
   1.151  
   1.152  lemma refl_diag: "refl A (diag A)"
   1.153 -  by (rule reflI [OF diag_subset_Times diagI])
   1.154 +by (rule reflI [OF diag_subset_Times diagI])
   1.155  
   1.156  
   1.157  subsection {* Antisymmetry *}
   1.158  
   1.159  lemma antisymI:
   1.160    "(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r"
   1.161 -  by (unfold antisym_def) iprover
   1.162 +by (unfold antisym_def) iprover
   1.163  
   1.164  lemma antisymD: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b"
   1.165 -  by (unfold antisym_def) iprover
   1.166 +by (unfold antisym_def) iprover
   1.167  
   1.168  lemma antisym_subset: "r \<subseteq> s ==> antisym s ==> antisym r"
   1.169 -  by (unfold antisym_def) blast
   1.170 +by (unfold antisym_def) blast
   1.171  
   1.172  lemma antisym_empty [simp]: "antisym {}"
   1.173 -  by (unfold antisym_def) blast
   1.174 +by (unfold antisym_def) blast
   1.175  
   1.176  lemma antisym_diag [simp]: "antisym (diag A)"
   1.177 -  by (unfold antisym_def) blast
   1.178 +by (unfold antisym_def) blast
   1.179  
   1.180  
   1.181  subsection {* Symmetry *}
   1.182  
   1.183  lemma symI: "(!!a b. (a, b) : r ==> (b, a) : r) ==> sym r"
   1.184 -  by (unfold sym_def) iprover
   1.185 +by (unfold sym_def) iprover
   1.186  
   1.187  lemma symD: "sym r ==> (a, b) : r ==> (b, a) : r"
   1.188 -  by (unfold sym_def, blast)
   1.189 +by (unfold sym_def, blast)
   1.190  
   1.191  lemma sym_Int: "sym r ==> sym s ==> sym (r \<inter> s)"
   1.192 -  by (fast intro: symI dest: symD)
   1.193 +by (fast intro: symI dest: symD)
   1.194  
   1.195  lemma sym_Un: "sym r ==> sym s ==> sym (r \<union> s)"
   1.196 -  by (fast intro: symI dest: symD)
   1.197 +by (fast intro: symI dest: symD)
   1.198  
   1.199  lemma sym_INTER: "ALL x:S. sym (r x) ==> sym (INTER S r)"
   1.200 -  by (fast intro: symI dest: symD)
   1.201 +by (fast intro: symI dest: symD)
   1.202  
   1.203  lemma sym_UNION: "ALL x:S. sym (r x) ==> sym (UNION S r)"
   1.204 -  by (fast intro: symI dest: symD)
   1.205 +by (fast intro: symI dest: symD)
   1.206  
   1.207  lemma sym_diag [simp]: "sym (diag A)"
   1.208 -  by (rule symI) clarify
   1.209 +by (rule symI) clarify
   1.210  
   1.211  
   1.212  subsection {* Transitivity *}
   1.213  
   1.214  lemma transI:
   1.215    "(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r"
   1.216 -  by (unfold trans_def) iprover
   1.217 +by (unfold trans_def) iprover
   1.218  
   1.219  lemma transD: "trans r ==> (a, b) : r ==> (b, c) : r ==> (a, c) : r"
   1.220 -  by (unfold trans_def) iprover
   1.221 +by (unfold trans_def) iprover
   1.222  
   1.223  lemma trans_Int: "trans r ==> trans s ==> trans (r \<inter> s)"
   1.224 -  by (fast intro: transI elim: transD)
   1.225 +by (fast intro: transI elim: transD)
   1.226  
   1.227  lemma trans_INTER: "ALL x:S. trans (r x) ==> trans (INTER S r)"
   1.228 -  by (fast intro: transI elim: transD)
   1.229 +by (fast intro: transI elim: transD)
   1.230  
   1.231  lemma trans_diag [simp]: "trans (diag A)"
   1.232 -  by (fast intro: transI elim: transD)
   1.233 +by (fast intro: transI elim: transD)
   1.234  
   1.235  
   1.236  subsection {* Converse *}
   1.237  
   1.238  lemma converse_iff [iff]: "((a,b): r^-1) = ((b,a) : r)"
   1.239 -  by (simp add: converse_def)
   1.240 +by (simp add: converse_def)
   1.241  
   1.242  lemma converseI[sym]: "(a, b) : r ==> (b, a) : r^-1"
   1.243 -  by (simp add: converse_def)
   1.244 +by (simp add: converse_def)
   1.245  
   1.246  lemma converseD[sym]: "(a,b) : r^-1 ==> (b, a) : r"
   1.247 -  by (simp add: converse_def)
   1.248 +by (simp add: converse_def)
   1.249  
   1.250  lemma converseE [elim!]:
   1.251    "yx : r^-1 ==> (!!x y. yx = (y, x) ==> (x, y) : r ==> P) ==> P"
   1.252      -- {* More general than @{text converseD}, as it ``splits'' the member of the relation. *}
   1.253 -  by (unfold converse_def) (iprover elim!: CollectE splitE bexE)
   1.254 +by (unfold converse_def) (iprover elim!: CollectE splitE bexE)
   1.255  
   1.256  lemma converse_converse [simp]: "(r^-1)^-1 = r"
   1.257 -  by (unfold converse_def) blast
   1.258 +by (unfold converse_def) blast
   1.259  
   1.260  lemma converse_rel_comp: "(r O s)^-1 = s^-1 O r^-1"
   1.261 -  by blast
   1.262 +by blast
   1.263  
   1.264  lemma converse_Int: "(r \<inter> s)^-1 = r^-1 \<inter> s^-1"
   1.265 -  by blast
   1.266 +by blast
   1.267  
   1.268  lemma converse_Un: "(r \<union> s)^-1 = r^-1 \<union> s^-1"
   1.269 -  by blast
   1.270 +by blast
   1.271  
   1.272  lemma converse_INTER: "(INTER S r)^-1 = (INT x:S. (r x)^-1)"
   1.273 -  by fast
   1.274 +by fast
   1.275  
   1.276  lemma converse_UNION: "(UNION S r)^-1 = (UN x:S. (r x)^-1)"
   1.277 -  by blast
   1.278 +by blast
   1.279  
   1.280  lemma converse_Id [simp]: "Id^-1 = Id"
   1.281 -  by blast
   1.282 +by blast
   1.283  
   1.284  lemma converse_diag [simp]: "(diag A)^-1 = diag A"
   1.285 -  by blast
   1.286 +by blast
   1.287  
   1.288  lemma refl_converse [simp]: "refl A (converse r) = refl A r"
   1.289 -  by (unfold refl_def) auto
   1.290 +by (unfold refl_def) auto
   1.291  
   1.292  lemma sym_converse [simp]: "sym (converse r) = sym r"
   1.293 -  by (unfold sym_def) blast
   1.294 +by (unfold sym_def) blast
   1.295  
   1.296  lemma antisym_converse [simp]: "antisym (converse r) = antisym r"
   1.297 -  by (unfold antisym_def) blast
   1.298 +by (unfold antisym_def) blast
   1.299  
   1.300  lemma trans_converse [simp]: "trans (converse r) = trans r"
   1.301 -  by (unfold trans_def) blast
   1.302 +by (unfold trans_def) blast
   1.303  
   1.304  lemma sym_conv_converse_eq: "sym r = (r^-1 = r)"
   1.305 -  by (unfold sym_def) fast
   1.306 +by (unfold sym_def) fast
   1.307  
   1.308  lemma sym_Un_converse: "sym (r \<union> r^-1)"
   1.309 -  by (unfold sym_def) blast
   1.310 +by (unfold sym_def) blast
   1.311  
   1.312  lemma sym_Int_converse: "sym (r \<inter> r^-1)"
   1.313 -  by (unfold sym_def) blast
   1.314 +by (unfold sym_def) blast
   1.315  
   1.316  
   1.317  subsection {* Domain *}
   1.318 @@ -328,87 +328,110 @@
   1.319  declare Domain_def [noatp]
   1.320  
   1.321  lemma Domain_iff: "(a : Domain r) = (EX y. (a, y) : r)"
   1.322 -  by (unfold Domain_def) blast
   1.323 +by (unfold Domain_def) blast
   1.324  
   1.325  lemma DomainI [intro]: "(a, b) : r ==> a : Domain r"
   1.326 -  by (iprover intro!: iffD2 [OF Domain_iff])
   1.327 +by (iprover intro!: iffD2 [OF Domain_iff])
   1.328  
   1.329  lemma DomainE [elim!]:
   1.330    "a : Domain r ==> (!!y. (a, y) : r ==> P) ==> P"
   1.331 -  by (iprover dest!: iffD1 [OF Domain_iff])
   1.332 +by (iprover dest!: iffD1 [OF Domain_iff])
   1.333  
   1.334  lemma Domain_empty [simp]: "Domain {} = {}"
   1.335 -  by blast
   1.336 +by blast
   1.337  
   1.338  lemma Domain_insert: "Domain (insert (a, b) r) = insert a (Domain r)"
   1.339 -  by blast
   1.340 +by blast
   1.341  
   1.342  lemma Domain_Id [simp]: "Domain Id = UNIV"
   1.343 -  by blast
   1.344 +by blast
   1.345  
   1.346  lemma Domain_diag [simp]: "Domain (diag A) = A"
   1.347 -  by blast
   1.348 +by blast
   1.349  
   1.350  lemma Domain_Un_eq: "Domain(A \<union> B) = Domain(A) \<union> Domain(B)"
   1.351 -  by blast
   1.352 +by blast
   1.353  
   1.354  lemma Domain_Int_subset: "Domain(A \<inter> B) \<subseteq> Domain(A) \<inter> Domain(B)"
   1.355 -  by blast
   1.356 +by blast
   1.357  
   1.358  lemma Domain_Diff_subset: "Domain(A) - Domain(B) \<subseteq> Domain(A - B)"
   1.359 -  by blast
   1.360 +by blast
   1.361  
   1.362  lemma Domain_Union: "Domain (Union S) = (\<Union>A\<in>S. Domain A)"
   1.363 -  by blast
   1.364 +by blast
   1.365 +
   1.366 +lemma Domain_converse[simp]: "Domain(r^-1) = Range r"
   1.367 +by(auto simp:Range_def)
   1.368  
   1.369  lemma Domain_mono: "r \<subseteq> s ==> Domain r \<subseteq> Domain s"
   1.370 -  by blast
   1.371 +by blast
   1.372  
   1.373  lemma fst_eq_Domain: "fst ` R = Domain R";
   1.374 -  apply auto
   1.375 -  apply (rule image_eqI, auto) 
   1.376 -  done
   1.377 +by (auto intro!:image_eqI)
   1.378  
   1.379  
   1.380  subsection {* Range *}
   1.381  
   1.382  lemma Range_iff: "(a : Range r) = (EX y. (y, a) : r)"
   1.383 -  by (simp add: Domain_def Range_def)
   1.384 +by (simp add: Domain_def Range_def)
   1.385  
   1.386  lemma RangeI [intro]: "(a, b) : r ==> b : Range r"
   1.387 -  by (unfold Range_def) (iprover intro!: converseI DomainI)
   1.388 +by (unfold Range_def) (iprover intro!: converseI DomainI)
   1.389  
   1.390  lemma RangeE [elim!]: "b : Range r ==> (!!x. (x, b) : r ==> P) ==> P"
   1.391 -  by (unfold Range_def) (iprover elim!: DomainE dest!: converseD)
   1.392 +by (unfold Range_def) (iprover elim!: DomainE dest!: converseD)
   1.393  
   1.394  lemma Range_empty [simp]: "Range {} = {}"
   1.395 -  by blast
   1.396 +by blast
   1.397  
   1.398  lemma Range_insert: "Range (insert (a, b) r) = insert b (Range r)"
   1.399 -  by blast
   1.400 +by blast
   1.401  
   1.402  lemma Range_Id [simp]: "Range Id = UNIV"
   1.403 -  by blast
   1.404 +by blast
   1.405  
   1.406  lemma Range_diag [simp]: "Range (diag A) = A"
   1.407 -  by auto
   1.408 +by auto
   1.409  
   1.410  lemma Range_Un_eq: "Range(A \<union> B) = Range(A) \<union> Range(B)"
   1.411 -  by blast
   1.412 +by blast
   1.413  
   1.414  lemma Range_Int_subset: "Range(A \<inter> B) \<subseteq> Range(A) \<inter> Range(B)"
   1.415 -  by blast
   1.416 +by blast
   1.417  
   1.418  lemma Range_Diff_subset: "Range(A) - Range(B) \<subseteq> Range(A - B)"
   1.419 -  by blast
   1.420 +by blast
   1.421  
   1.422  lemma Range_Union: "Range (Union S) = (\<Union>A\<in>S. Range A)"
   1.423 -  by blast
   1.424 +by blast
   1.425 +
   1.426 +lemma Range_converse[simp]: "Range(r^-1) = Domain r"
   1.427 +by blast
   1.428  
   1.429  lemma snd_eq_Range: "snd ` R = Range R";
   1.430 -  apply auto
   1.431 -  apply (rule image_eqI, auto) 
   1.432 -  done
   1.433 +by (auto intro!:image_eqI)
   1.434 +
   1.435 +
   1.436 +subsection {* Field *}
   1.437 +
   1.438 +lemma mono_Field: "r \<subseteq> s \<Longrightarrow> Field r \<subseteq> Field s"
   1.439 +by(auto simp:Field_def Domain_def Range_def)
   1.440 +
   1.441 +lemma Field_empty[simp]: "Field {} = {}"
   1.442 +by(auto simp:Field_def)
   1.443 +
   1.444 +lemma Field_insert[simp]: "Field (insert (a,b) r) = {a,b} \<union> Field r"
   1.445 +by(auto simp:Field_def)
   1.446 +
   1.447 +lemma Field_Un[simp]: "Field (r \<union> s) = Field r \<union> Field s"
   1.448 +by(auto simp:Field_def)
   1.449 +
   1.450 +lemma Field_Union[simp]: "Field (\<Union>R) = \<Union>(Field ` R)"
   1.451 +by(auto simp:Field_def)
   1.452 +
   1.453 +lemma Field_converse[simp]: "Field(r^-1) = Field r"
   1.454 +by(auto simp:Field_def)
   1.455  
   1.456  
   1.457  subsection {* Image of a set under a relation *}
   1.458 @@ -416,62 +439,62 @@
   1.459  declare Image_def [noatp]
   1.460  
   1.461  lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)"
   1.462 -  by (simp add: Image_def)
   1.463 +by (simp add: Image_def)
   1.464  
   1.465  lemma Image_singleton: "r``{a} = {b. (a, b) : r}"
   1.466 -  by (simp add: Image_def)
   1.467 +by (simp add: Image_def)
   1.468  
   1.469  lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a, b) : r)"
   1.470 -  by (rule Image_iff [THEN trans]) simp
   1.471 +by (rule Image_iff [THEN trans]) simp
   1.472  
   1.473  lemma ImageI [intro,noatp]: "(a, b) : r ==> a : A ==> b : r``A"
   1.474 -  by (unfold Image_def) blast
   1.475 +by (unfold Image_def) blast
   1.476  
   1.477  lemma ImageE [elim!]:
   1.478      "b : r `` A ==> (!!x. (x, b) : r ==> x : A ==> P) ==> P"
   1.479 -  by (unfold Image_def) (iprover elim!: CollectE bexE)
   1.480 +by (unfold Image_def) (iprover elim!: CollectE bexE)
   1.481  
   1.482  lemma rev_ImageI: "a : A ==> (a, b) : r ==> b : r `` A"
   1.483    -- {* This version's more effective when we already have the required @{text a} *}
   1.484 -  by blast
   1.485 +by blast
   1.486  
   1.487  lemma Image_empty [simp]: "R``{} = {}"
   1.488 -  by blast
   1.489 +by blast
   1.490  
   1.491  lemma Image_Id [simp]: "Id `` A = A"
   1.492 -  by blast
   1.493 +by blast
   1.494  
   1.495  lemma Image_diag [simp]: "diag A `` B = A \<inter> B"
   1.496 -  by blast
   1.497 +by blast
   1.498  
   1.499  lemma Image_Int_subset: "R `` (A \<inter> B) \<subseteq> R `` A \<inter> R `` B"
   1.500 -  by blast
   1.501 +by blast
   1.502  
   1.503  lemma Image_Int_eq:
   1.504       "single_valued (converse R) ==> R `` (A \<inter> B) = R `` A \<inter> R `` B"
   1.505 -  by (simp add: single_valued_def, blast) 
   1.506 +by (simp add: single_valued_def, blast) 
   1.507  
   1.508  lemma Image_Un: "R `` (A \<union> B) = R `` A \<union> R `` B"
   1.509 -  by blast
   1.510 +by blast
   1.511  
   1.512  lemma Un_Image: "(R \<union> S) `` A = R `` A \<union> S `` A"
   1.513 -  by blast
   1.514 +by blast
   1.515  
   1.516  lemma Image_subset: "r \<subseteq> A \<times> B ==> r``C \<subseteq> B"
   1.517 -  by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
   1.518 +by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
   1.519  
   1.520  lemma Image_eq_UN: "r``B = (\<Union>y\<in> B. r``{y})"
   1.521    -- {* NOT suitable for rewriting *}
   1.522 -  by blast
   1.523 +by blast
   1.524  
   1.525  lemma Image_mono: "r' \<subseteq> r ==> A' \<subseteq> A ==> (r' `` A') \<subseteq> (r `` A)"
   1.526 -  by blast
   1.527 +by blast
   1.528  
   1.529  lemma Image_UN: "(r `` (UNION A B)) = (\<Union>x\<in>A. r `` (B x))"
   1.530 -  by blast
   1.531 +by blast
   1.532  
   1.533  lemma Image_INT_subset: "(r `` INTER A B) \<subseteq> (\<Inter>x\<in>A. r `` (B x))"
   1.534 -  by blast
   1.535 +by blast
   1.536  
   1.537  text{*Converse inclusion requires some assumptions*}
   1.538  lemma Image_INT_eq:
   1.539 @@ -482,50 +505,50 @@
   1.540  done
   1.541  
   1.542  lemma Image_subset_eq: "(r``A \<subseteq> B) = (A \<subseteq> - ((r^-1) `` (-B)))"
   1.543 -  by blast
   1.544 +by blast
   1.545  
   1.546  
   1.547  subsection {* Single valued relations *}
   1.548  
   1.549  lemma single_valuedI:
   1.550    "ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z) ==> single_valued r"
   1.551 -  by (unfold single_valued_def)
   1.552 +by (unfold single_valued_def)
   1.553  
   1.554  lemma single_valuedD:
   1.555    "single_valued r ==> (x, y) : r ==> (x, z) : r ==> y = z"
   1.556 -  by (simp add: single_valued_def)
   1.557 +by (simp add: single_valued_def)
   1.558  
   1.559  lemma single_valued_rel_comp:
   1.560    "single_valued r ==> single_valued s ==> single_valued (r O s)"
   1.561 -  by (unfold single_valued_def) blast
   1.562 +by (unfold single_valued_def) blast
   1.563  
   1.564  lemma single_valued_subset:
   1.565    "r \<subseteq> s ==> single_valued s ==> single_valued r"
   1.566 -  by (unfold single_valued_def) blast
   1.567 +by (unfold single_valued_def) blast
   1.568  
   1.569  lemma single_valued_Id [simp]: "single_valued Id"
   1.570 -  by (unfold single_valued_def) blast
   1.571 +by (unfold single_valued_def) blast
   1.572  
   1.573  lemma single_valued_diag [simp]: "single_valued (diag A)"
   1.574 -  by (unfold single_valued_def) blast
   1.575 +by (unfold single_valued_def) blast
   1.576  
   1.577  
   1.578  subsection {* Graphs given by @{text Collect} *}
   1.579  
   1.580  lemma Domain_Collect_split [simp]: "Domain{(x,y). P x y} = {x. EX y. P x y}"
   1.581 -  by auto
   1.582 +by auto
   1.583  
   1.584  lemma Range_Collect_split [simp]: "Range{(x,y). P x y} = {y. EX x. P x y}"
   1.585 -  by auto
   1.586 +by auto
   1.587  
   1.588  lemma Image_Collect_split [simp]: "{(x,y). P x y} `` A = {y. EX x:A. P x y}"
   1.589 -  by auto
   1.590 +by auto
   1.591  
   1.592  
   1.593  subsection {* Inverse image *}
   1.594  
   1.595  lemma sym_inv_image: "sym r ==> sym (inv_image r f)"
   1.596 -  by (unfold sym_def inv_image_def) blast
   1.597 +by (unfold sym_def inv_image_def) blast
   1.598  
   1.599  lemma trans_inv_image: "trans r ==> trans (inv_image r f)"
   1.600    apply (unfold trans_def inv_image_def)