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.77 -by(simp add:refl_on_def)
    1.78 +lemma refl_on_empty [simp]: "refl_on {} {}"
    1.79 +  by (simp add:refl_on_def)
    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.331 -by(simp add:total_on_def)
   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.348 -by (simp add: single_valued_def)
   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.382 -by (simp add: Id_def)
   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.394 -by (simp add: refl_on_def)
   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.399 -by (simp add: antisym_def)
   1.400 +  by (simp add: antisym_def)
   1.401  
   1.402  lemma sym_Id: "sym Id"
   1.403 -by (simp add: sym_def)
   1.404 +  by (simp add: sym_def)
   1.405  
   1.406  lemma trans_Id: "trans Id"
   1.407 -by (simp add: trans_def)
   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.424 -by (simp add: Id_on_def) 
   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.428 -by (simp add: Id_on_def)
   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.938 -by (simp add: Image_def)
   1.939 +  by (simp add: Image_def)
   1.940  
   1.941  lemma Image_singleton: "r``{a} = {b. (a, b) : r}"
   1.942 -by (simp add: Image_def)
   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)"
  1.1059    by (simp add: inv_imagep_def)
  1.1060 @@ -883,7 +1021,8 @@
  1.1061  
  1.1062  subsubsection {* Powerset *}
  1.1063  
  1.1064 -definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
  1.1065 +definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
  1.1066 +where
  1.1067    "Powp A = (\<lambda>B. \<forall>x \<in> B. A x)"
  1.1068  
  1.1069  lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)"