src/HOL/Relation.thy
 changeset 46752 e9e7209eb375 parent 46696 28a01ea3523a child 46767 807a5d219c23
```     1.1 --- a/src/HOL/Relation.thy	Thu Mar 01 17:13:54 2012 +0000
1.2 +++ b/src/HOL/Relation.thy	Thu Mar 01 19:34:52 2012 +0100
1.3 @@ -113,28 +113,33 @@
1.4
1.5  subsubsection {* Reflexivity *}
1.6
1.7 -definition
1.8 -  refl_on :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" where
1.9 -  "refl_on A r \<longleftrightarrow> r \<subseteq> A \<times> A & (ALL x: A. (x,x) : r)"
1.10 +definition refl_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
1.11 +where
1.12 +  "refl_on A r \<longleftrightarrow> r \<subseteq> A \<times> A \<and> (\<forall>x\<in>A. (x, x) \<in> r)"
1.13
1.14 -abbreviation
1.15 -  refl :: "('a * 'a) set => bool" where -- {* reflexivity over a type *}
1.16 +abbreviation refl :: "'a rel \<Rightarrow> bool"
1.17 +where -- {* reflexivity over a type *}
1.18    "refl \<equiv> refl_on UNIV"
1.19
1.20 -definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
1.21 +definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
1.22 +where
1.23    "reflp r \<longleftrightarrow> refl {(x, y). r x y}"
1.24
1.25 +lemma reflp_refl_eq [pred_set_conv]:
1.26 +  "reflp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> refl r"
1.27 +  by (simp add: refl_on_def reflp_def)
1.28 +
1.29  lemma refl_onI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl_on A r"
1.30 -by (unfold refl_on_def) (iprover intro!: ballI)
1.31 +  by (unfold refl_on_def) (iprover intro!: ballI)
1.32
1.33  lemma refl_onD: "refl_on A r ==> a : A ==> (a, a) : r"
1.34 -by (unfold refl_on_def) blast
1.35 +  by (unfold refl_on_def) blast
1.36
1.37  lemma refl_onD1: "refl_on A r ==> (x, y) : r ==> x : A"
1.38 -by (unfold refl_on_def) blast
1.39 +  by (unfold refl_on_def) blast
1.40
1.41  lemma refl_onD2: "refl_on A r ==> (x, y) : r ==> y : A"
1.42 -by (unfold refl_on_def) blast
1.43 +  by (unfold refl_on_def) blast
1.44
1.45  lemma reflpI:
1.46    "(\<And>x. r x x) \<Longrightarrow> reflp r"
1.47 @@ -146,32 +151,40 @@
1.48    using assms by (auto dest: refl_onD simp add: reflp_def)
1.49
1.50  lemma refl_on_Int: "refl_on A r ==> refl_on B s ==> refl_on (A \<inter> B) (r \<inter> s)"
1.51 -by (unfold refl_on_def) blast
1.52 +  by (unfold refl_on_def) blast
1.53 +
1.54 +lemma reflp_inf:
1.55 +  "reflp r \<Longrightarrow> reflp s \<Longrightarrow> reflp (r \<sqinter> s)"
1.56 +  by (auto intro: reflpI elim: reflpE)
1.57
1.58  lemma refl_on_Un: "refl_on A r ==> refl_on B s ==> refl_on (A \<union> B) (r \<union> s)"
1.59 -by (unfold refl_on_def) blast
1.60 +  by (unfold refl_on_def) blast
1.61 +
1.62 +lemma reflp_sup:
1.63 +  "reflp r \<Longrightarrow> reflp s \<Longrightarrow> reflp (r \<squnion> s)"
1.64 +  by (auto intro: reflpI elim: reflpE)
1.65
1.66  lemma refl_on_INTER:
1.67    "ALL x:S. refl_on (A x) (r x) ==> refl_on (INTER S A) (INTER S r)"
1.68 -by (unfold refl_on_def) fast
1.69 +  by (unfold refl_on_def) fast
1.70
1.71  lemma refl_on_UNION:
1.72    "ALL x:S. refl_on (A x) (r x) \<Longrightarrow> refl_on (UNION S A) (UNION S r)"
1.73 -by (unfold refl_on_def) blast
1.74 +  by (unfold refl_on_def) blast
1.75
1.76 -lemma refl_on_empty[simp]: "refl_on {} {}"
1.78 +lemma refl_on_empty [simp]: "refl_on {} {}"
1.80
1.81  lemma refl_on_def' [nitpick_unfold, code]:
1.82 -  "refl_on A r = ((\<forall>(x, y) \<in> r. x : A \<and> y : A) \<and> (\<forall>x \<in> A. (x, x) : r))"
1.83 -by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
1.84 +  "refl_on A r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<in> A \<and> y \<in> A) \<and> (\<forall>x \<in> A. (x, x) \<in> r)"
1.85 +  by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
1.86
1.87
1.88  subsubsection {* Irreflexivity *}
1.89
1.90 -definition
1.91 -  irrefl :: "('a * 'a) set => bool" where
1.92 -  "irrefl r \<longleftrightarrow> (\<forall>x. (x,x) \<notin> r)"
1.93 +definition irrefl :: "'a rel \<Rightarrow> bool"
1.94 +where
1.95 +  "irrefl r \<longleftrightarrow> (\<forall>x. (x, x) \<notin> r)"
1.96
1.97  lemma irrefl_distinct [code]:
1.98    "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
1.99 @@ -180,166 +193,231 @@
1.100
1.101  subsubsection {* Symmetry *}
1.102
1.103 -definition
1.104 -  sym :: "('a * 'a) set => bool" where
1.105 -  "sym r \<longleftrightarrow> (ALL x y. (x,y): r --> (y,x): r)"
1.106 +definition sym :: "'a rel \<Rightarrow> bool"
1.107 +where
1.108 +  "sym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r)"
1.109 +
1.110 +definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
1.111 +where
1.112 +  "symp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> r y x)"
1.113
1.114 -lemma symI: "(!!a b. (a, b) : r ==> (b, a) : r) ==> sym r"
1.115 -by (unfold sym_def) iprover
1.116 +lemma symp_sym_eq [pred_set_conv]:
1.117 +  "symp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> sym r"
1.118 +  by (simp add: sym_def symp_def)
1.119
1.120 -lemma symD: "sym r ==> (a, b) : r ==> (b, a) : r"
1.121 -by (unfold sym_def, blast)
1.122 -
1.123 -definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
1.124 -  "symp r \<longleftrightarrow> sym {(x, y). r x y}"
1.125 +lemma symI:
1.126 +  "(\<And>a b. (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r) \<Longrightarrow> sym r"
1.127 +  by (unfold sym_def) iprover
1.128
1.129  lemma sympI:
1.130 -  "(\<And>x y. r x y \<Longrightarrow> r y x) \<Longrightarrow> symp r"
1.131 -  by (auto intro: symI simp add: symp_def)
1.132 +  "(\<And>a b. r a b \<Longrightarrow> r b a) \<Longrightarrow> symp r"
1.133 +  by (fact symI [to_pred])
1.134 +
1.135 +lemma symE:
1.136 +  assumes "sym r" and "(b, a) \<in> r"
1.137 +  obtains "(a, b) \<in> r"
1.138 +  using assms by (simp add: sym_def)
1.139
1.140  lemma sympE:
1.141 -  assumes "symp r" and "r x y"
1.142 -  obtains "r y x"
1.143 -  using assms by (auto dest: symD simp add: symp_def)
1.144 +  assumes "symp r" and "r b a"
1.145 +  obtains "r a b"
1.146 +  using assms by (rule symE [to_pred])
1.147 +
1.148 +lemma symD:
1.149 +  assumes "sym r" and "(b, a) \<in> r"
1.150 +  shows "(a, b) \<in> r"
1.151 +  using assms by (rule symE)
1.152
1.153 -lemma sym_Int: "sym r ==> sym s ==> sym (r \<inter> s)"
1.154 -by (fast intro: symI dest: symD)
1.155 +lemma sympD:
1.156 +  assumes "symp r" and "r b a"
1.157 +  shows "r a b"
1.158 +  using assms by (rule symD [to_pred])
1.159 +
1.160 +lemma sym_Int:
1.161 +  "sym r \<Longrightarrow> sym s \<Longrightarrow> sym (r \<inter> s)"
1.162 +  by (fast intro: symI elim: symE)
1.163
1.164 -lemma sym_Un: "sym r ==> sym s ==> sym (r \<union> s)"
1.165 -by (fast intro: symI dest: symD)
1.166 +lemma symp_inf:
1.167 +  "symp r \<Longrightarrow> symp s \<Longrightarrow> symp (r \<sqinter> s)"
1.168 +  by (fact sym_Int [to_pred])
1.169 +
1.170 +lemma sym_Un:
1.171 +  "sym r \<Longrightarrow> sym s \<Longrightarrow> sym (r \<union> s)"
1.172 +  by (fast intro: symI elim: symE)
1.173 +
1.174 +lemma symp_sup:
1.175 +  "symp r \<Longrightarrow> symp s \<Longrightarrow> symp (r \<squnion> s)"
1.176 +  by (fact sym_Un [to_pred])
1.177
1.178 -lemma sym_INTER: "ALL x:S. sym (r x) ==> sym (INTER S r)"
1.179 -by (fast intro: symI dest: symD)
1.180 +lemma sym_INTER:
1.181 +  "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (INTER S r)"
1.182 +  by (fast intro: symI elim: symE)
1.183 +
1.184 +(* FIXME thm sym_INTER [to_pred] *)
1.185
1.186 -lemma sym_UNION: "ALL x:S. sym (r x) ==> sym (UNION S r)"
1.187 -by (fast intro: symI dest: symD)
1.188 +lemma sym_UNION:
1.189 +  "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (UNION S r)"
1.190 +  by (fast intro: symI elim: symE)
1.191 +
1.192 +(* FIXME thm sym_UNION [to_pred] *)
1.193
1.194
1.195  subsubsection {* Antisymmetry *}
1.196
1.197 -definition
1.198 -  antisym :: "('a * 'a) set => bool" where
1.199 -  "antisym r \<longleftrightarrow> (ALL x y. (x,y):r --> (y,x):r --> x=y)"
1.200 +definition antisym :: "'a rel \<Rightarrow> bool"
1.201 +where
1.202 +  "antisym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r \<longrightarrow> x = y)"
1.203 +
1.204 +abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
1.205 +where
1.206 +  "antisymP r \<equiv> antisym {(x, y). r x y}"
1.207
1.208  lemma antisymI:
1.209    "(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r"
1.210 -by (unfold antisym_def) iprover
1.211 +  by (unfold antisym_def) iprover
1.212
1.213  lemma antisymD: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b"
1.214 -by (unfold antisym_def) iprover
1.215 -
1.216 -abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
1.217 -  "antisymP r \<equiv> antisym {(x, y). r x y}"
1.218 +  by (unfold antisym_def) iprover
1.219
1.220  lemma antisym_subset: "r \<subseteq> s ==> antisym s ==> antisym r"
1.221 -by (unfold antisym_def) blast
1.222 +  by (unfold antisym_def) blast
1.223
1.224  lemma antisym_empty [simp]: "antisym {}"
1.225 -by (unfold antisym_def) blast
1.226 +  by (unfold antisym_def) blast
1.227
1.228
1.229  subsubsection {* Transitivity *}
1.230
1.231 -definition
1.232 -  trans :: "('a * 'a) set => bool" where
1.233 -  "trans r \<longleftrightarrow> (ALL x y z. (x,y):r --> (y,z):r --> (x,z):r)"
1.234 +definition trans :: "'a rel \<Rightarrow> bool"
1.235 +where
1.236 +  "trans r \<longleftrightarrow> (\<forall>x y z. (x, y) \<in> r \<longrightarrow> (y, z) \<in> r \<longrightarrow> (x, z) \<in> r)"
1.237 +
1.238 +definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
1.239 +where
1.240 +  "transp r \<longleftrightarrow> (\<forall>x y z. r x y \<longrightarrow> r y z \<longrightarrow> r x z)"
1.241 +
1.242 +lemma transp_trans_eq [pred_set_conv]:
1.243 +  "transp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> trans r"
1.244 +  by (simp add: trans_def transp_def)
1.245 +
1.246 +abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
1.247 +where -- {* FIXME drop *}
1.248 +  "transP r \<equiv> trans {(x, y). r x y}"
1.249
1.250  lemma transI:
1.251 -  "(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r"
1.252 -by (unfold trans_def) iprover
1.253 -
1.254 -lemma transD: "trans r ==> (a, b) : r ==> (b, c) : r ==> (a, c) : r"
1.255 -by (unfold trans_def) iprover
1.256 -
1.257 -abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
1.258 -  "transP r \<equiv> trans {(x, y). r x y}"
1.259 -
1.260 -definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
1.261 -  "transp r \<longleftrightarrow> trans {(x, y). r x y}"
1.262 +  "(\<And>x y z. (x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r) \<Longrightarrow> trans r"
1.263 +  by (unfold trans_def) iprover
1.264
1.265  lemma transpI:
1.266    "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r"
1.267 -  by (auto intro: transI simp add: transp_def)
1.268 -
1.269 +  by (fact transI [to_pred])
1.270 +
1.271 +lemma transE:
1.272 +  assumes "trans r" and "(x, y) \<in> r" and "(y, z) \<in> r"
1.273 +  obtains "(x, z) \<in> r"
1.274 +  using assms by (unfold trans_def) iprover
1.275 +
1.276  lemma transpE:
1.277    assumes "transp r" and "r x y" and "r y z"
1.278    obtains "r x z"
1.279 -  using assms by (auto dest: transD simp add: transp_def)
1.280 +  using assms by (rule transE [to_pred])
1.281 +
1.282 +lemma transD:
1.283 +  assumes "trans r" and "(x, y) \<in> r" and "(y, z) \<in> r"
1.284 +  shows "(x, z) \<in> r"
1.285 +  using assms by (rule transE)
1.286 +
1.287 +lemma transpD:
1.288 +  assumes "transp r" and "r x y" and "r y z"
1.289 +  shows "r x z"
1.290 +  using assms by (rule transD [to_pred])
1.291
1.292 -lemma trans_Int: "trans r ==> trans s ==> trans (r \<inter> s)"
1.293 -by (fast intro: transI elim: transD)
1.294 +lemma trans_Int:
1.295 +  "trans r \<Longrightarrow> trans s \<Longrightarrow> trans (r \<inter> s)"
1.296 +  by (fast intro: transI elim: transE)
1.297
1.298 -lemma trans_INTER: "ALL x:S. trans (r x) ==> trans (INTER S r)"
1.299 -by (fast intro: transI elim: transD)
1.300 +lemma transp_inf:
1.301 +  "transp r \<Longrightarrow> transp s \<Longrightarrow> transp (r \<sqinter> s)"
1.302 +  by (fact trans_Int [to_pred])
1.303 +
1.304 +lemma trans_INTER:
1.305 +  "\<forall>x\<in>S. trans (r x) \<Longrightarrow> trans (INTER S r)"
1.306 +  by (fast intro: transI elim: transD)
1.307 +
1.308 +(* FIXME thm trans_INTER [to_pred] *)
1.309
1.310  lemma trans_join [code]:
1.311    "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
1.312    by (auto simp add: trans_def)
1.313
1.314 +lemma transp_trans:
1.315 +  "transp r \<longleftrightarrow> trans {(x, y). r x y}"
1.316 +  by (simp add: trans_def transp_def)
1.317 +
1.318
1.319  subsubsection {* Totality *}
1.320
1.321 -definition
1.322 -  total_on :: "'a set => ('a * 'a) set => bool" where
1.323 -  "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.324 +definition total_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
1.325 +where
1.326 +  "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.327
1.328  abbreviation "total \<equiv> total_on UNIV"
1.329
1.330 -lemma total_on_empty[simp]: "total_on {} r"
1.332 +lemma total_on_empty [simp]: "total_on {} r"
1.333 +  by (simp add: total_on_def)
1.334
1.335
1.336  subsubsection {* Single valued relations *}
1.337
1.338 -definition
1.339 -  single_valued :: "('a * 'b) set => bool" where
1.340 -  "single_valued r \<longleftrightarrow> (ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z))"
1.341 -
1.342 -lemma single_valuedI:
1.343 -  "ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z) ==> single_valued r"
1.344 -by (unfold single_valued_def)
1.345 -
1.346 -lemma single_valuedD:
1.347 -  "single_valued r ==> (x, y) : r ==> (x, z) : r ==> y = z"
1.349 +definition single_valued :: "('a \<times> 'b) set \<Rightarrow> bool"
1.350 +where
1.351 +  "single_valued r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (\<forall>z. (x, z) \<in> r \<longrightarrow> y = z))"
1.352
1.353  abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
1.354    "single_valuedP r \<equiv> single_valued {(x, y). r x y}"
1.355
1.356 +lemma single_valuedI:
1.357 +  "ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z) ==> single_valued r"
1.358 +  by (unfold single_valued_def)
1.359 +
1.360 +lemma single_valuedD:
1.361 +  "single_valued r ==> (x, y) : r ==> (x, z) : r ==> y = z"
1.362 +  by (simp add: single_valued_def)
1.363 +
1.364  lemma single_valued_subset:
1.365    "r \<subseteq> s ==> single_valued s ==> single_valued r"
1.366 -by (unfold single_valued_def) blast
1.367 +  by (unfold single_valued_def) blast
1.368
1.369
1.370  subsection {* Relation operations *}
1.371
1.372  subsubsection {* The identity relation *}
1.373
1.374 -definition
1.375 -  Id :: "('a * 'a) set" where
1.376 -  "Id = {p. EX x. p = (x,x)}"
1.377 +definition Id :: "'a rel"
1.378 +where
1.379 +  "Id = {p. \<exists>x. p = (x, x)}"
1.380
1.381  lemma IdI [intro]: "(a, a) : Id"
1.383 +  by (simp add: Id_def)
1.384
1.385  lemma IdE [elim!]: "p : Id ==> (!!x. p = (x, x) ==> P) ==> P"
1.386 -by (unfold Id_def) (iprover elim: CollectE)
1.387 +  by (unfold Id_def) (iprover elim: CollectE)
1.388
1.389  lemma pair_in_Id_conv [iff]: "((a, b) : Id) = (a = b)"
1.390 -by (unfold Id_def) blast
1.391 +  by (unfold Id_def) blast
1.392
1.393  lemma refl_Id: "refl Id"
1.395 +  by (simp add: refl_on_def)
1.396
1.397  lemma antisym_Id: "antisym Id"
1.398    -- {* A strange result, since @{text Id} is also symmetric. *}
1.400 +  by (simp add: antisym_def)
1.401
1.402  lemma sym_Id: "sym Id"
1.404 +  by (simp add: sym_def)
1.405
1.406  lemma trans_Id: "trans Id"
1.408 +  by (simp add: trans_def)
1.409
1.410  lemma single_valued_Id [simp]: "single_valued Id"
1.411    by (unfold single_valued_def) blast
1.412 @@ -356,45 +434,45 @@
1.413
1.414  subsubsection {* Diagonal: identity over a set *}
1.415
1.416 -definition
1.417 -  Id_on  :: "'a set => ('a * 'a) set" where
1.418 -  "Id_on A = (\<Union>x\<in>A. {(x,x)})"
1.419 +definition Id_on  :: "'a set \<Rightarrow> 'a rel"
1.420 +where
1.421 +  "Id_on A = (\<Union>x\<in>A. {(x, x)})"
1.422
1.423  lemma Id_on_empty [simp]: "Id_on {} = {}"
1.425 +  by (simp add: Id_on_def)
1.426
1.427  lemma Id_on_eqI: "a = b ==> a : A ==> (a, b) : Id_on A"
1.429 +  by (simp add: Id_on_def)
1.430
1.431  lemma Id_onI [intro!,no_atp]: "a : A ==> (a, a) : Id_on A"
1.432 -by (rule Id_on_eqI) (rule refl)
1.433 +  by (rule Id_on_eqI) (rule refl)
1.434
1.435  lemma Id_onE [elim!]:
1.436    "c : Id_on A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P"
1.437    -- {* The general elimination rule. *}
1.438 -by (unfold Id_on_def) (iprover elim!: UN_E singletonE)
1.439 +  by (unfold Id_on_def) (iprover elim!: UN_E singletonE)
1.440
1.441  lemma Id_on_iff: "((x, y) : Id_on A) = (x = y & x : A)"
1.442 -by blast
1.443 +  by blast
1.444
1.445  lemma Id_on_def' [nitpick_unfold]:
1.446    "Id_on {x. A x} = Collect (\<lambda>(x, y). x = y \<and> A x)"
1.447 -by auto
1.448 +  by auto
1.449
1.450  lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> A"
1.451 -by blast
1.452 +  by blast
1.453
1.454  lemma refl_on_Id_on: "refl_on A (Id_on A)"
1.455 -by (rule refl_onI [OF Id_on_subset_Times Id_onI])
1.456 +  by (rule refl_onI [OF Id_on_subset_Times Id_onI])
1.457
1.458  lemma antisym_Id_on [simp]: "antisym (Id_on A)"
1.459 -by (unfold antisym_def) blast
1.460 +  by (unfold antisym_def) blast
1.461
1.462  lemma sym_Id_on [simp]: "sym (Id_on A)"
1.463 -by (rule symI) clarify
1.464 +  by (rule symI) clarify
1.465
1.466  lemma trans_Id_on [simp]: "trans (Id_on A)"
1.467 -by (fast intro: transI elim: transD)
1.468 +  by (fast intro: transI elim: transD)
1.469
1.470  lemma single_valued_Id_on [simp]: "single_valued (Id_on A)"
1.471    by (unfold single_valued_def) blast
1.472 @@ -402,184 +480,228 @@
1.473
1.474  subsubsection {* Composition *}
1.475
1.476 -definition rel_comp  :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a * 'c) set" (infixr "O" 75)
1.477 +inductive_set rel_comp  :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixr "O" 75)
1.478 +  for r :: "('a \<times> 'b) set" and s :: "('b \<times> 'c) set"
1.479  where
1.480 -  "r O s = {(x, z). \<exists>y. (x, y) \<in> r \<and> (y, z) \<in> s}"
1.481 +  rel_compI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s"
1.482
1.483 -lemma rel_compI [intro]:
1.484 -  "(a, b) : r ==> (b, c) : s ==> (a, c) : r O s"
1.485 -by (unfold rel_comp_def) blast
1.486 +abbreviation pred_comp (infixr "OO" 75) where
1.487 +  "pred_comp \<equiv> rel_compp"
1.488
1.489 -lemma rel_compE [elim!]: "xz : r O s ==>
1.490 -  (!!x y z. xz = (x, z) ==> (x, y) : r ==> (y, z) : s  ==> P) ==> P"
1.491 -by (unfold rel_comp_def) (iprover elim!: CollectE splitE exE conjE)
1.492 +lemmas pred_compI = rel_compp.intros
1.493
1.494 -inductive pred_comp :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> bool" (infixr "OO" 75)
1.495 -for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and s :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
1.496 -where
1.497 -  pred_compI [intro]: "r a b \<Longrightarrow> s b c \<Longrightarrow> (r OO s) a c"
1.498 +text {*
1.499 +  For historic reasons, the elimination rules are not wholly corresponding.
1.500 +  Feel free to consolidate this.
1.501 +*}
1.502
1.503 +inductive_cases rel_compEpair: "(a, c) \<in> r O s"
1.504  inductive_cases pred_compE [elim!]: "(r OO s) a c"
1.505
1.506 -lemma pred_comp_rel_comp_eq [pred_set_conv]:
1.507 -  "((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O s)"
1.508 -  by (auto simp add: fun_eq_iff)
1.509 +lemma rel_compE [elim!]: "xz \<in> r O s \<Longrightarrow>
1.510 +  (\<And>x y z. xz = (x, z) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> s  \<Longrightarrow> P) \<Longrightarrow> P"
1.511 +  by (cases xz) (simp, erule rel_compEpair, iprover)
1.512 +
1.513 +lemmas pred_comp_rel_comp_eq = rel_compp_rel_comp_eq
1.514 +
1.515 +lemma R_O_Id [simp]:
1.516 +  "R O Id = R"
1.517 +  by fast
1.518
1.519 -lemma rel_compEpair:
1.520 -  "(a, c) : r O s ==> (!!y. (a, y) : r ==> (y, c) : s ==> P) ==> P"
1.521 -by (iprover elim: rel_compE Pair_inject ssubst)
1.522 +lemma Id_O_R [simp]:
1.523 +  "Id O R = R"
1.524 +  by fast
1.525 +
1.526 +lemma rel_comp_empty1 [simp]:
1.527 +  "{} O R = {}"
1.528 +  by blast
1.529
1.530 -lemma R_O_Id [simp]: "R O Id = R"
1.531 -by fast
1.532 +(* CANDIDATE lemma pred_comp_bot1 [simp]:
1.533 +  ""
1.534 +  by (fact rel_comp_empty1 [to_pred]) *)
1.535
1.536 -lemma Id_O_R [simp]: "Id O R = R"
1.537 -by fast
1.538 +lemma rel_comp_empty2 [simp]:
1.539 +  "R O {} = {}"
1.540 +  by blast
1.541
1.542 -lemma rel_comp_empty1[simp]: "{} O R = {}"
1.543 -by blast
1.544 +(* CANDIDATE lemma pred_comp_bot2 [simp]:
1.545 +  ""
1.546 +  by (fact rel_comp_empty2 [to_pred]) *)
1.547
1.548 -lemma rel_comp_empty2[simp]: "R O {} = {}"
1.549 -by blast
1.550 +lemma O_assoc:
1.551 +  "(R O S) O T = R O (S O T)"
1.552 +  by blast
1.553 +
1.554 +lemma pred_comp_assoc:
1.555 +  "(r OO s) OO t = r OO (s OO t)"
1.556 +  by (fact O_assoc [to_pred])
1.557
1.558 -lemma O_assoc: "(R O S) O T = R O (S O T)"
1.559 -by blast
1.560 +lemma trans_O_subset:
1.561 +  "trans r \<Longrightarrow> r O r \<subseteq> r"
1.562 +  by (unfold trans_def) blast
1.563 +
1.564 +lemma transp_pred_comp_less_eq:
1.565 +  "transp r \<Longrightarrow> r OO r \<le> r "
1.566 +  by (fact trans_O_subset [to_pred])
1.567
1.568 -lemma trans_O_subset: "trans r ==> r O r \<subseteq> r"
1.569 -by (unfold trans_def) blast
1.570 +lemma rel_comp_mono:
1.571 +  "r' \<subseteq> r \<Longrightarrow> s' \<subseteq> s \<Longrightarrow> r' O s' \<subseteq> r O s"
1.572 +  by blast
1.573
1.574 -lemma rel_comp_mono: "r' \<subseteq> r ==> s' \<subseteq> s ==> (r' O s') \<subseteq> (r O s)"
1.575 -by blast
1.576 +lemma pred_comp_mono:
1.577 +  "r' \<le> r \<Longrightarrow> s' \<le> s \<Longrightarrow> r' OO s' \<le> r OO s "
1.578 +  by (fact rel_comp_mono [to_pred])
1.579
1.580  lemma rel_comp_subset_Sigma:
1.581 -    "r \<subseteq> A \<times> B ==> s \<subseteq> B \<times> C ==> (r O s) \<subseteq> A \<times> C"
1.582 -by blast
1.583 +  "r \<subseteq> A \<times> B \<Longrightarrow> s \<subseteq> B \<times> C \<Longrightarrow> r O s \<subseteq> A \<times> C"
1.584 +  by blast
1.585 +
1.586 +lemma rel_comp_distrib [simp]:
1.587 +  "R O (S \<union> T) = (R O S) \<union> (R O T)"
1.588 +  by auto
1.589
1.590 -lemma rel_comp_distrib[simp]: "R O (S \<union> T) = (R O S) \<union> (R O T)"
1.591 -by auto
1.592 +lemma pred_comp_distrib (* CANDIDATE [simp] *):
1.593 +  "R OO (S \<squnion> T) = R OO S \<squnion> R OO T"
1.594 +  by (fact rel_comp_distrib [to_pred])
1.595 +
1.596 +lemma rel_comp_distrib2 [simp]:
1.597 +  "(S \<union> T) O R = (S O R) \<union> (T O R)"
1.598 +  by auto
1.599
1.600 -lemma rel_comp_distrib2[simp]: "(S \<union> T) O R = (S O R) \<union> (T O R)"
1.601 -by auto
1.602 +lemma pred_comp_distrib2 (* CANDIDATE [simp] *):
1.603 +  "(S \<squnion> T) OO R = S OO R \<squnion> T OO R"
1.604 +  by (fact rel_comp_distrib2 [to_pred])
1.605 +
1.606 +lemma rel_comp_UNION_distrib:
1.607 +  "s O UNION I r = (\<Union>i\<in>I. s O r i) "
1.608 +  by auto
1.609
1.610 -lemma rel_comp_UNION_distrib: "s O UNION I r = UNION I (%i. s O r i)"
1.611 -by auto
1.612 +(* FIXME thm rel_comp_UNION_distrib [to_pred] *)
1.613
1.614 -lemma rel_comp_UNION_distrib2: "UNION I r O s = UNION I (%i. r i O s)"
1.615 -by auto
1.616 +lemma rel_comp_UNION_distrib2:
1.617 +  "UNION I r O s = (\<Union>i\<in>I. r i O s) "
1.618 +  by auto
1.619 +
1.620 +(* FIXME thm rel_comp_UNION_distrib2 [to_pred] *)
1.621
1.622  lemma single_valued_rel_comp:
1.623 -  "single_valued r ==> single_valued s ==> single_valued (r O s)"
1.624 -by (unfold single_valued_def) blast
1.625 +  "single_valued r \<Longrightarrow> single_valued s \<Longrightarrow> single_valued (r O s)"
1.626 +  by (unfold single_valued_def) blast
1.627 +
1.628 +lemma rel_comp_unfold:
1.629 +  "r O s = {(x, z). \<exists>y. (x, y) \<in> r \<and> (y, z) \<in> s}"
1.630 +  by (auto simp add: set_eq_iff)
1.631
1.632
1.633  subsubsection {* Converse *}
1.634
1.635 -definition
1.636 -  converse :: "('a * 'b) set => ('b * 'a) set"
1.637 -    ("(_^-1)" [1000] 999) where
1.638 -  "r^-1 = {(y, x). (x, y) : r}"
1.639 +inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set" ("(_^-1)" [1000] 999)
1.640 +  for r :: "('a \<times> 'b) set"
1.641 +where
1.642 +  "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r^-1"
1.643
1.644  notation (xsymbols)
1.645    converse  ("(_\<inverse>)" [1000] 999)
1.646
1.647 -lemma converseI [sym]: "(a, b) : r ==> (b, a) : r^-1"
1.648 -  by (simp add: converse_def)
1.649 -
1.650 -lemma converseD [sym]: "(a,b) : r^-1 ==> (b, a) : r"
1.651 -  by (simp add: converse_def)
1.652 -
1.653 -lemma converseE [elim!]:
1.654 -  "yx : r^-1 ==> (!!x y. yx = (y, x) ==> (x, y) : r ==> P) ==> P"
1.655 -    -- {* More general than @{text converseD}, as it ``splits'' the member of the relation. *}
1.656 -  by (unfold converse_def) (iprover elim!: CollectE splitE bexE)
1.657 -
1.658 -lemma converse_iff [iff]: "((a,b): r^-1) = ((b,a) : r)"
1.659 -  by (simp add: converse_def)
1.660 -
1.661 -inductive conversep :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(_^--1)" [1000] 1000)
1.662 -  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
1.663 -  conversepI: "r a b \<Longrightarrow> r^--1 b a"
1.664 +notation
1.665 +  conversep ("(_^--1)" [1000] 1000)
1.666
1.667  notation (xsymbols)
1.668    conversep  ("(_\<inverse>\<inverse>)" [1000] 1000)
1.669
1.670 -lemma conversepD:
1.671 -  assumes ab: "r^--1 a b"
1.672 -  shows "r b a" using ab
1.673 -  by cases simp
1.674 +lemma converseI [sym]:
1.675 +  "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>"
1.676 +  by (fact converse.intros)
1.677 +
1.678 +lemma conversepI (* CANDIDATE [sym] *):
1.679 +  "r a b \<Longrightarrow> r\<inverse>\<inverse> b a"
1.680 +  by (fact conversep.intros)
1.681 +
1.682 +lemma converseD [sym]:
1.683 +  "(a, b) \<in> r\<inverse> \<Longrightarrow> (b, a) \<in> r"
1.684 +  by (erule converse.cases) iprover
1.685 +
1.686 +lemma conversepD (* CANDIDATE [sym] *):
1.687 +  "r\<inverse>\<inverse> b a \<Longrightarrow> r a b"
1.688 +  by (fact converseD [to_pred])
1.689 +
1.690 +lemma converseE [elim!]:
1.691 +  -- {* More general than @{text converseD}, as it ``splits'' the member of the relation. *}
1.692 +  "yx \<in> r\<inverse> \<Longrightarrow> (\<And>x y. yx = (y, x) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> P) \<Longrightarrow> P"
1.693 +  by (cases yx) (simp, erule converse.cases, iprover)
1.694
1.695 -lemma conversep_iff [iff]: "r^--1 a b = r b a"
1.696 -  by (iprover intro: conversepI dest: conversepD)
1.697 +lemmas conversepE (* CANDIDATE [elim!] *) = conversep.cases
1.698 +
1.699 +lemma converse_iff [iff]:
1.700 +  "(a, b) \<in> r\<inverse> \<longleftrightarrow> (b, a) \<in> r"
1.701 +  by (auto intro: converseI)
1.702 +
1.703 +lemma conversep_iff [iff]:
1.704 +  "r\<inverse>\<inverse> a b = r b a"
1.705 +  by (fact converse_iff [to_pred])
1.706
1.707 -lemma conversep_converse_eq [pred_set_conv]:
1.708 -  "(\<lambda>x y. (x, y) \<in> r)^--1 = (\<lambda>x y. (x, y) \<in> r^-1)"
1.709 -  by (auto simp add: fun_eq_iff)
1.710 +lemma converse_converse [simp]:
1.711 +  "(r\<inverse>)\<inverse> = r"
1.712 +  by (simp add: set_eq_iff)
1.713
1.714 -lemma conversep_conversep [simp]: "(r^--1)^--1 = r"
1.715 -  by (iprover intro: order_antisym conversepI dest: conversepD)
1.716 +lemma conversep_conversep [simp]:
1.717 +  "(r\<inverse>\<inverse>)\<inverse>\<inverse> = r"
1.718 +  by (fact converse_converse [to_pred])
1.719 +
1.720 +lemma converse_rel_comp: "(r O s)^-1 = s^-1 O r^-1"
1.721 +  by blast
1.722
1.723  lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
1.724    by (iprover intro: order_antisym conversepI pred_compI
1.725      elim: pred_compE dest: conversepD)
1.726
1.727 +lemma converse_Int: "(r \<inter> s)^-1 = r^-1 \<inter> s^-1"
1.728 +  by blast
1.729 +
1.730  lemma converse_meet: "(r \<sqinter> s)^--1 = r^--1 \<sqinter> s^--1"
1.731    by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD)
1.732
1.733 +lemma converse_Un: "(r \<union> s)^-1 = r^-1 \<union> s^-1"
1.734 +  by blast
1.735 +
1.736  lemma converse_join: "(r \<squnion> s)^--1 = r^--1 \<squnion> s^--1"
1.737    by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD)
1.738
1.739 -lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>"
1.740 -  by (auto simp add: fun_eq_iff)
1.741 -
1.742 -lemma conversep_eq [simp]: "(op =)^--1 = op ="
1.743 -  by (auto simp add: fun_eq_iff)
1.744 -
1.745 -lemma converse_converse [simp]: "(r^-1)^-1 = r"
1.746 -by (unfold converse_def) blast
1.747 -
1.748 -lemma converse_rel_comp: "(r O s)^-1 = s^-1 O r^-1"
1.749 -by blast
1.750 -
1.751 -lemma converse_Int: "(r \<inter> s)^-1 = r^-1 \<inter> s^-1"
1.752 -by blast
1.753 -
1.754 -lemma converse_Un: "(r \<union> s)^-1 = r^-1 \<union> s^-1"
1.755 -by blast
1.756 -
1.757  lemma converse_INTER: "(INTER S r)^-1 = (INT x:S. (r x)^-1)"
1.758 -by fast
1.759 +  by fast
1.760
1.761  lemma converse_UNION: "(UNION S r)^-1 = (UN x:S. (r x)^-1)"
1.762 -by blast
1.763 +  by blast
1.764
1.765  lemma converse_Id [simp]: "Id^-1 = Id"
1.766 -by blast
1.767 +  by blast
1.768
1.769  lemma converse_Id_on [simp]: "(Id_on A)^-1 = Id_on A"
1.770 -by blast
1.771 +  by blast
1.772
1.773  lemma refl_on_converse [simp]: "refl_on A (converse r) = refl_on A r"
1.774 -by (unfold refl_on_def) auto
1.775 +  by (unfold refl_on_def) auto
1.776
1.777  lemma sym_converse [simp]: "sym (converse r) = sym r"
1.778 -by (unfold sym_def) blast
1.779 +  by (unfold sym_def) blast
1.780
1.781  lemma antisym_converse [simp]: "antisym (converse r) = antisym r"
1.782 -by (unfold antisym_def) blast
1.783 +  by (unfold antisym_def) blast
1.784
1.785  lemma trans_converse [simp]: "trans (converse r) = trans r"
1.786 -by (unfold trans_def) blast
1.787 +  by (unfold trans_def) blast
1.788
1.789  lemma sym_conv_converse_eq: "sym r = (r^-1 = r)"
1.790 -by (unfold sym_def) fast
1.791 +  by (unfold sym_def) fast
1.792
1.793  lemma sym_Un_converse: "sym (r \<union> r^-1)"
1.794 -by (unfold sym_def) blast
1.795 +  by (unfold sym_def) blast
1.796
1.797  lemma sym_Int_converse: "sym (r \<inter> r^-1)"
1.798 -by (unfold sym_def) blast
1.799 +  by (unfold sym_def) blast
1.800
1.801 -lemma total_on_converse[simp]: "total_on A (r^-1) = total_on A r"
1.802 -by (auto simp: total_on_def)
1.803 +lemma total_on_converse [simp]: "total_on A (r^-1) = total_on A r"
1.804 +  by (auto simp: total_on_def)
1.805
1.806  lemma finite_converse [iff]: "finite (r^-1) = finite r"
1.807    apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
1.808 @@ -588,50 +710,61 @@
1.809      apply (erule finite_imageD [unfolded inj_on_def])
1.810      apply (simp split add: split_split)
1.811     apply (erule finite_imageI)
1.812 -  apply (simp add: converse_def image_def, auto)
1.813 +  apply (simp add: set_eq_iff image_def, auto)
1.814    apply (rule bexI)
1.815     prefer 2 apply assumption
1.816    apply simp
1.817    done
1.818
1.819 +lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>"
1.820 +  by (auto simp add: fun_eq_iff)
1.821 +
1.822 +lemma conversep_eq [simp]: "(op =)^--1 = op ="
1.823 +  by (auto simp add: fun_eq_iff)
1.824 +
1.825 +lemma converse_unfold:
1.826 +  "r\<inverse> = {(y, x). (x, y) \<in> r}"
1.827 +  by (simp add: set_eq_iff)
1.828 +
1.829
1.830  subsubsection {* Domain, range and field *}
1.831
1.832 -definition
1.833 -  Domain :: "('a * 'b) set => 'a set" where
1.834 -  "Domain r = {x. EX y. (x,y):r}"
1.835 +definition Domain :: "('a \<times> 'b) set \<Rightarrow> 'a set"
1.836 +where
1.837 +  "Domain r = {x. \<exists>y. (x, y) \<in> r}"
1.838
1.839 -definition
1.840 -  Range  :: "('a * 'b) set => 'b set" where
1.841 -  "Range r = Domain(r^-1)"
1.842 +definition Range  :: "('a \<times> 'b) set \<Rightarrow> 'b set"
1.843 +where
1.844 +  "Range r = Domain (r\<inverse>)"
1.845
1.846 -definition
1.847 -  Field :: "('a * 'a) set => 'a set" where
1.848 +definition Field :: "'a rel \<Rightarrow> 'a set"
1.849 +where
1.850    "Field r = Domain r \<union> Range r"
1.851
1.852  declare Domain_def [no_atp]
1.853
1.854  lemma Domain_iff: "(a : Domain r) = (EX y. (a, y) : r)"
1.855 -by (unfold Domain_def) blast
1.856 +  by (unfold Domain_def) blast
1.857
1.858  lemma DomainI [intro]: "(a, b) : r ==> a : Domain r"
1.859 -by (iprover intro!: iffD2 [OF Domain_iff])
1.860 +  by (iprover intro!: iffD2 [OF Domain_iff])
1.861
1.862  lemma DomainE [elim!]:
1.863    "a : Domain r ==> (!!y. (a, y) : r ==> P) ==> P"
1.864 -by (iprover dest!: iffD1 [OF Domain_iff])
1.865 +  by (iprover dest!: iffD1 [OF Domain_iff])
1.866
1.867  lemma Range_iff: "(a : Range r) = (EX y. (y, a) : r)"
1.868 -by (simp add: Domain_def Range_def)
1.869 +  by (simp add: Domain_def Range_def)
1.870
1.871  lemma RangeI [intro]: "(a, b) : r ==> b : Range r"
1.872 -by (unfold Range_def) (iprover intro!: converseI DomainI)
1.873 +  by (unfold Range_def) (iprover intro!: converseI DomainI)
1.874
1.875  lemma RangeE [elim!]: "b : Range r ==> (!!x. (x, b) : r ==> P) ==> P"
1.876 -by (unfold Range_def) (iprover elim!: DomainE dest!: converseD)
1.877 +  by (unfold Range_def) (iprover elim!: DomainE dest!: converseD)
1.878
1.879  inductive DomainP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
1.880 -  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
1.881 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
1.882 +where
1.883    DomainPI [intro]: "r a b \<Longrightarrow> DomainP r a"
1.884
1.885  inductive_cases DomainPE [elim!]: "DomainP r a"
1.886 @@ -640,7 +773,8 @@
1.887    by (blast intro!: Orderings.order_antisym predicate1I)
1.888
1.889  inductive RangeP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool"
1.890 -  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
1.891 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
1.892 +where
1.893    RangePI [intro]: "r a b \<Longrightarrow> RangeP r b"
1.894
1.895  inductive_cases RangePE [elim!]: "RangeP r b"
1.896 @@ -679,8 +813,8 @@
1.897  lemma Domain_Union: "Domain (Union S) = (\<Union>A\<in>S. Domain A)"
1.898    by blast
1.899
1.900 -lemma Domain_converse[simp]: "Domain(r^-1) = Range r"
1.901 -  by(auto simp: Range_def)
1.902 +lemma Domain_converse [simp]: "Domain (r\<inverse>) = Range r"
1.903 +  by auto
1.904
1.905  lemma Domain_mono: "r \<subseteq> s ==> Domain r \<subseteq> Domain s"
1.906    by blast
1.907 @@ -731,7 +865,7 @@
1.908  lemma Range_Union: "Range (Union S) = (\<Union>A\<in>S. Range A)"
1.909    by blast
1.910
1.911 -lemma Range_converse [simp]: "Range(r^-1) = Domain r"
1.912 +lemma Range_converse [simp]: "Range (r\<inverse>) = Domain r"
1.913    by blast
1.914
1.915  lemma snd_eq_Range: "snd ` R = Range R"
1.916 @@ -767,73 +901,76 @@
1.917     apply (auto simp add: Field_def Domain_insert Range_insert)
1.918    done
1.919
1.920 +lemma Domain_unfold:
1.921 +  "Domain r = {x. \<exists>y. (x, y) \<in> r}"
1.922 +  by (fact Domain_def)
1.923 +
1.924
1.925  subsubsection {* Image of a set under a relation *}
1.926
1.927 -definition
1.928 -  Image :: "[('a * 'b) set, 'a set] => 'b set"
1.929 -    (infixl "``" 90) where
1.930 -  "r `` s = {y. EX x:s. (x,y):r}"
1.931 +definition Image :: "('a \<times> 'b) set \<Rightarrow> 'a set \<Rightarrow> 'b set" (infixl "``" 90)
1.932 +where
1.933 +  "r `` s = {y. \<exists>x\<in>s. (x, y) \<in> r}"
1.934
1.935  declare Image_def [no_atp]
1.936
1.937  lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)"
1.939 +  by (simp add: Image_def)
1.940
1.941  lemma Image_singleton: "r``{a} = {b. (a, b) : r}"
1.943 +  by (simp add: Image_def)
1.944
1.945  lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a, b) : r)"
1.946 -by (rule Image_iff [THEN trans]) simp
1.947 +  by (rule Image_iff [THEN trans]) simp
1.948
1.949  lemma ImageI [intro,no_atp]: "(a, b) : r ==> a : A ==> b : r``A"
1.950 -by (unfold Image_def) blast
1.951 +  by (unfold Image_def) blast
1.952
1.953  lemma ImageE [elim!]:
1.954 -    "b : r `` A ==> (!!x. (x, b) : r ==> x : A ==> P) ==> P"
1.955 -by (unfold Image_def) (iprover elim!: CollectE bexE)
1.956 +  "b : r `` A ==> (!!x. (x, b) : r ==> x : A ==> P) ==> P"
1.957 +  by (unfold Image_def) (iprover elim!: CollectE bexE)
1.958
1.959  lemma rev_ImageI: "a : A ==> (a, b) : r ==> b : r `` A"
1.960    -- {* This version's more effective when we already have the required @{text a} *}
1.961 -by blast
1.962 +  by blast
1.963
1.964  lemma Image_empty [simp]: "R``{} = {}"
1.965 -by blast
1.966 +  by blast
1.967
1.968  lemma Image_Id [simp]: "Id `` A = A"
1.969 -by blast
1.970 +  by blast
1.971
1.972  lemma Image_Id_on [simp]: "Id_on A `` B = A \<inter> B"
1.973 -by blast
1.974 +  by blast
1.975
1.976  lemma Image_Int_subset: "R `` (A \<inter> B) \<subseteq> R `` A \<inter> R `` B"
1.977 -by blast
1.978 +  by blast
1.979
1.980  lemma Image_Int_eq:
1.981       "single_valued (converse R) ==> R `` (A \<inter> B) = R `` A \<inter> R `` B"
1.982 -by (simp add: single_valued_def, blast)
1.983 +     by (simp add: single_valued_def, blast)
1.984
1.985  lemma Image_Un: "R `` (A \<union> B) = R `` A \<union> R `` B"
1.986 -by blast
1.987 +  by blast
1.988
1.989  lemma Un_Image: "(R \<union> S) `` A = R `` A \<union> S `` A"
1.990 -by blast
1.991 +  by blast
1.992
1.993  lemma Image_subset: "r \<subseteq> A \<times> B ==> r``C \<subseteq> B"
1.994 -by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
1.995 +  by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
1.996
1.997  lemma Image_eq_UN: "r``B = (\<Union>y\<in> B. r``{y})"
1.998    -- {* NOT suitable for rewriting *}
1.999 -by blast
1.1000 +  by blast
1.1001
1.1002  lemma Image_mono: "r' \<subseteq> r ==> A' \<subseteq> A ==> (r' `` A') \<subseteq> (r `` A)"
1.1003 -by blast
1.1004 +  by blast
1.1005
1.1006  lemma Image_UN: "(r `` (UNION A B)) = (\<Union>x\<in>A. r `` (B x))"
1.1007 -by blast
1.1008 +  by blast
1.1009
1.1010  lemma Image_INT_subset: "(r `` INTER A B) \<subseteq> (\<Inter>x\<in>A. r `` (B x))"
1.1011 -by blast
1.1012 +  by blast
1.1013
1.1014  text{*Converse inclusion requires some assumptions*}
1.1015  lemma Image_INT_eq:
1.1016 @@ -844,26 +981,27 @@
1.1017  done
1.1018
1.1019  lemma Image_subset_eq: "(r``A \<subseteq> B) = (A \<subseteq> - ((r^-1) `` (-B)))"
1.1020 -by blast
1.1021 +  by blast
1.1022
1.1023  lemma Image_Collect_split [simp]: "{(x, y). P x y} `` A = {y. EX x:A. P x y}"
1.1024 -by auto
1.1025 +  by auto
1.1026
1.1027
1.1028  subsubsection {* Inverse image *}
1.1029
1.1030 -definition
1.1031 -  inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set" where
1.1032 -  "inv_image r f = {(x, y). (f x, f y) : r}"
1.1033 +definition inv_image :: "'b rel \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a rel"
1.1034 +where
1.1035 +  "inv_image r f = {(x, y). (f x, f y) \<in> r}"
1.1036
1.1037 -definition inv_imagep :: "('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
1.1038 +definition inv_imagep :: "('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
1.1039 +where
1.1040    "inv_imagep r f = (\<lambda>x y. r (f x) (f y))"
1.1041
1.1042  lemma [pred_set_conv]: "inv_imagep (\<lambda>x y. (x, y) \<in> r) f = (\<lambda>x y. (x, y) \<in> inv_image r f)"
1.1043    by (simp add: inv_image_def inv_imagep_def)
1.1044
1.1045  lemma sym_inv_image: "sym r ==> sym (inv_image r f)"
1.1046 -by (unfold sym_def inv_image_def) blast
1.1047 +  by (unfold sym_def inv_image_def) blast
1.1048
1.1049  lemma trans_inv_image: "trans r ==> trans (inv_image r f)"
1.1050    apply (unfold trans_def inv_image_def)
1.1051 @@ -875,7 +1013,7 @@
1.1052    by (auto simp:inv_image_def)
1.1053
1.1054  lemma converse_inv_image[simp]: "(inv_image R f)^-1 = inv_image (R^-1) f"
1.1055 -unfolding inv_image_def converse_def by auto
1.1056 +  unfolding inv_image_def converse_unfold by auto
1.1057
1.1058  lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)"