1(* Title: HOL/Relation.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Author: Stefan Berghofer, TU Muenchen 4*) 5 6section \<open>Relations -- as sets of pairs, and binary predicates\<close> 7 8theory Relation 9 imports Finite_Set 10begin 11 12text \<open>A preliminary: classical rules for reasoning on predicates\<close> 13 14declare predicate1I [Pure.intro!, intro!] 15declare predicate1D [Pure.dest, dest] 16declare predicate2I [Pure.intro!, intro!] 17declare predicate2D [Pure.dest, dest] 18declare bot1E [elim!] 19declare bot2E [elim!] 20declare top1I [intro!] 21declare top2I [intro!] 22declare inf1I [intro!] 23declare inf2I [intro!] 24declare inf1E [elim!] 25declare inf2E [elim!] 26declare sup1I1 [intro?] 27declare sup2I1 [intro?] 28declare sup1I2 [intro?] 29declare sup2I2 [intro?] 30declare sup1E [elim!] 31declare sup2E [elim!] 32declare sup1CI [intro!] 33declare sup2CI [intro!] 34declare Inf1_I [intro!] 35declare INF1_I [intro!] 36declare Inf2_I [intro!] 37declare INF2_I [intro!] 38declare Inf1_D [elim] 39declare INF1_D [elim] 40declare Inf2_D [elim] 41declare INF2_D [elim] 42declare Inf1_E [elim] 43declare INF1_E [elim] 44declare Inf2_E [elim] 45declare INF2_E [elim] 46declare Sup1_I [intro] 47declare SUP1_I [intro] 48declare Sup2_I [intro] 49declare SUP2_I [intro] 50declare Sup1_E [elim!] 51declare SUP1_E [elim!] 52declare Sup2_E [elim!] 53declare SUP2_E [elim!] 54 55 56subsection \<open>Fundamental\<close> 57 58subsubsection \<open>Relations as sets of pairs\<close> 59 60type_synonym 'a rel = "('a \<times> 'a) set" 61 62lemma subrelI: "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (x, y) \<in> s) \<Longrightarrow> r \<subseteq> s" 63 \<comment> \<open>Version of @{thm [source] subsetI} for binary relations\<close> 64 by auto 65 66lemma lfp_induct2: 67 "(a, b) \<in> lfp f \<Longrightarrow> mono f \<Longrightarrow> 68 (\<And>a b. (a, b) \<in> f (lfp f \<inter> {(x, y). P x y}) \<Longrightarrow> P a b) \<Longrightarrow> P a b" 69 \<comment> \<open>Version of @{thm [source] lfp_induct} for binary relations\<close> 70 using lfp_induct_set [of "(a, b)" f "case_prod P"] by auto 71 72 73subsubsection \<open>Conversions between set and predicate relations\<close> 74 75lemma pred_equals_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S) \<longleftrightarrow> R = S" 76 by (simp add: set_eq_iff fun_eq_iff) 77 78lemma pred_equals_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S) \<longleftrightarrow> R = S" 79 by (simp add: set_eq_iff fun_eq_iff) 80 81lemma pred_subset_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S) \<longleftrightarrow> R \<subseteq> S" 82 by (simp add: subset_iff le_fun_def) 83 84lemma pred_subset_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<le> (\<lambda>x y. (x, y) \<in> S) \<longleftrightarrow> R \<subseteq> S" 85 by (simp add: subset_iff le_fun_def) 86 87lemma bot_empty_eq [pred_set_conv]: "\<bottom> = (\<lambda>x. x \<in> {})" 88 by (auto simp add: fun_eq_iff) 89 90lemma bot_empty_eq2 [pred_set_conv]: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})" 91 by (auto simp add: fun_eq_iff) 92 93lemma top_empty_eq [pred_set_conv]: "\<top> = (\<lambda>x. x \<in> UNIV)" 94 by (auto simp add: fun_eq_iff) 95 96lemma top_empty_eq2 [pred_set_conv]: "\<top> = (\<lambda>x y. (x, y) \<in> UNIV)" 97 by (auto simp add: fun_eq_iff) 98 99lemma inf_Int_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)" 100 by (simp add: inf_fun_def) 101 102lemma inf_Int_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<sqinter> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)" 103 by (simp add: inf_fun_def) 104 105lemma sup_Un_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<squnion> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)" 106 by (simp add: sup_fun_def) 107 108lemma sup_Un_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<squnion> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)" 109 by (simp add: sup_fun_def) 110 111lemma INF_INT_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i\<in>S. r i))" 112 by (simp add: fun_eq_iff) 113 114lemma INF_INT_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i\<in>S. r i))" 115 by (simp add: fun_eq_iff) 116 117lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i\<in>S. r i))" 118 by (simp add: fun_eq_iff) 119 120lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i\<in>S. r i))" 121 by (simp add: fun_eq_iff) 122 123lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> (\<Inter>(Collect ` S)))" 124 by (simp add: fun_eq_iff) 125 126lemma INF_Int_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Inter>S)" 127 by (simp add: fun_eq_iff) 128 129lemma Inf_INT_eq2 [pred_set_conv]: "\<Sqinter>S = (\<lambda>x y. (x, y) \<in> (\<Inter>(Collect ` case_prod ` S)))" 130 by (simp add: fun_eq_iff) 131 132lemma INF_Int_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Inter>S)" 133 by (simp add: fun_eq_iff) 134 135lemma Sup_SUP_eq [pred_set_conv]: "\<Squnion>S = (\<lambda>x. x \<in> \<Union>(Collect ` S))" 136 by (simp add: fun_eq_iff) 137 138lemma SUP_Sup_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Union>S)" 139 by (simp add: fun_eq_iff) 140 141lemma Sup_SUP_eq2 [pred_set_conv]: "\<Squnion>S = (\<lambda>x y. (x, y) \<in> (\<Union>(Collect ` case_prod ` S)))" 142 by (simp add: fun_eq_iff) 143 144lemma SUP_Sup_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Union>S)" 145 by (simp add: fun_eq_iff) 146 147 148subsection \<open>Properties of relations\<close> 149 150subsubsection \<open>Reflexivity\<close> 151 152definition refl_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool" 153 where "refl_on A r \<longleftrightarrow> r \<subseteq> A \<times> A \<and> (\<forall>x\<in>A. (x, x) \<in> r)" 154 155abbreviation refl :: "'a rel \<Rightarrow> bool" \<comment> \<open>reflexivity over a type\<close> 156 where "refl \<equiv> refl_on UNIV" 157 158definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 159 where "reflp r \<longleftrightarrow> (\<forall>x. r x x)" 160 161lemma reflp_refl_eq [pred_set_conv]: "reflp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> refl r" 162 by (simp add: refl_on_def reflp_def) 163 164lemma refl_onI [intro?]: "r \<subseteq> A \<times> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> (x, x) \<in> r) \<Longrightarrow> refl_on A r" 165 unfolding refl_on_def by (iprover intro!: ballI) 166 167lemma refl_onD: "refl_on A r \<Longrightarrow> a \<in> A \<Longrightarrow> (a, a) \<in> r" 168 unfolding refl_on_def by blast 169 170lemma refl_onD1: "refl_on A r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> x \<in> A" 171 unfolding refl_on_def by blast 172 173lemma refl_onD2: "refl_on A r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> y \<in> A" 174 unfolding refl_on_def by blast 175 176lemma reflpI [intro?]: "(\<And>x. r x x) \<Longrightarrow> reflp r" 177 by (auto intro: refl_onI simp add: reflp_def) 178 179lemma reflpE: 180 assumes "reflp r" 181 obtains "r x x" 182 using assms by (auto dest: refl_onD simp add: reflp_def) 183 184lemma reflpD [dest?]: 185 assumes "reflp r" 186 shows "r x x" 187 using assms by (auto elim: reflpE) 188 189lemma refl_on_Int: "refl_on A r \<Longrightarrow> refl_on B s \<Longrightarrow> refl_on (A \<inter> B) (r \<inter> s)" 190 unfolding refl_on_def by blast 191 192lemma reflp_inf: "reflp r \<Longrightarrow> reflp s \<Longrightarrow> reflp (r \<sqinter> s)" 193 by (auto intro: reflpI elim: reflpE) 194 195lemma refl_on_Un: "refl_on A r \<Longrightarrow> refl_on B s \<Longrightarrow> refl_on (A \<union> B) (r \<union> s)" 196 unfolding refl_on_def by blast 197 198lemma reflp_sup: "reflp r \<Longrightarrow> reflp s \<Longrightarrow> reflp (r \<squnion> s)" 199 by (auto intro: reflpI elim: reflpE) 200 201lemma refl_on_INTER: "\<forall>x\<in>S. refl_on (A x) (r x) \<Longrightarrow> refl_on (\<Inter>(A ` S)) (\<Inter>(r ` S))" 202 unfolding refl_on_def by fast 203 204lemma refl_on_UNION: "\<forall>x\<in>S. refl_on (A x) (r x) \<Longrightarrow> refl_on (\<Union>(A ` S)) (\<Union>(r ` S))" 205 unfolding refl_on_def by blast 206 207lemma refl_on_empty [simp]: "refl_on {} {}" 208 by (simp add: refl_on_def) 209 210lemma refl_on_singleton [simp]: "refl_on {x} {(x, x)}" 211by (blast intro: refl_onI) 212 213lemma refl_on_def' [nitpick_unfold, code]: 214 "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)" 215 by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2) 216 217lemma reflp_equality [simp]: "reflp (=)" 218 by (simp add: reflp_def) 219 220lemma reflp_mono: "reflp R \<Longrightarrow> (\<And>x y. R x y \<longrightarrow> Q x y) \<Longrightarrow> reflp Q" 221 by (auto intro: reflpI dest: reflpD) 222 223 224subsubsection \<open>Irreflexivity\<close> 225 226definition irrefl :: "'a rel \<Rightarrow> bool" 227 where "irrefl r \<longleftrightarrow> (\<forall>a. (a, a) \<notin> r)" 228 229definition irreflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 230 where "irreflp R \<longleftrightarrow> (\<forall>a. \<not> R a a)" 231 232lemma irreflp_irrefl_eq [pred_set_conv]: "irreflp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> irrefl R" 233 by (simp add: irrefl_def irreflp_def) 234 235lemma irreflI [intro?]: "(\<And>a. (a, a) \<notin> R) \<Longrightarrow> irrefl R" 236 by (simp add: irrefl_def) 237 238lemma irreflpI [intro?]: "(\<And>a. \<not> R a a) \<Longrightarrow> irreflp R" 239 by (fact irreflI [to_pred]) 240 241lemma irrefl_distinct [code]: "irrefl r \<longleftrightarrow> (\<forall>(a, b) \<in> r. a \<noteq> b)" 242 by (auto simp add: irrefl_def) 243 244 245subsubsection \<open>Asymmetry\<close> 246 247inductive asym :: "'a rel \<Rightarrow> bool" 248 where asymI: "irrefl R \<Longrightarrow> (\<And>a b. (a, b) \<in> R \<Longrightarrow> (b, a) \<notin> R) \<Longrightarrow> asym R" 249 250inductive asymp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 251 where asympI: "irreflp R \<Longrightarrow> (\<And>a b. R a b \<Longrightarrow> \<not> R b a) \<Longrightarrow> asymp R" 252 253lemma asymp_asym_eq [pred_set_conv]: "asymp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> asym R" 254 by (auto intro!: asymI asympI elim: asym.cases asymp.cases simp add: irreflp_irrefl_eq) 255 256 257subsubsection \<open>Symmetry\<close> 258 259definition sym :: "'a rel \<Rightarrow> bool" 260 where "sym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r)" 261 262definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 263 where "symp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> r y x)" 264 265lemma symp_sym_eq [pred_set_conv]: "symp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> sym r" 266 by (simp add: sym_def symp_def) 267 268lemma symI [intro?]: "(\<And>a b. (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r) \<Longrightarrow> sym r" 269 by (unfold sym_def) iprover 270 271lemma sympI [intro?]: "(\<And>a b. r a b \<Longrightarrow> r b a) \<Longrightarrow> symp r" 272 by (fact symI [to_pred]) 273 274lemma symE: 275 assumes "sym r" and "(b, a) \<in> r" 276 obtains "(a, b) \<in> r" 277 using assms by (simp add: sym_def) 278 279lemma sympE: 280 assumes "symp r" and "r b a" 281 obtains "r a b" 282 using assms by (rule symE [to_pred]) 283 284lemma symD [dest?]: 285 assumes "sym r" and "(b, a) \<in> r" 286 shows "(a, b) \<in> r" 287 using assms by (rule symE) 288 289lemma sympD [dest?]: 290 assumes "symp r" and "r b a" 291 shows "r a b" 292 using assms by (rule symD [to_pred]) 293 294lemma sym_Int: "sym r \<Longrightarrow> sym s \<Longrightarrow> sym (r \<inter> s)" 295 by (fast intro: symI elim: symE) 296 297lemma symp_inf: "symp r \<Longrightarrow> symp s \<Longrightarrow> symp (r \<sqinter> s)" 298 by (fact sym_Int [to_pred]) 299 300lemma sym_Un: "sym r \<Longrightarrow> sym s \<Longrightarrow> sym (r \<union> s)" 301 by (fast intro: symI elim: symE) 302 303lemma symp_sup: "symp r \<Longrightarrow> symp s \<Longrightarrow> symp (r \<squnion> s)" 304 by (fact sym_Un [to_pred]) 305 306lemma sym_INTER: "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (\<Inter>(r ` S))" 307 by (fast intro: symI elim: symE) 308 309lemma symp_INF: "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (\<Sqinter>(r ` S))" 310 by (fact sym_INTER [to_pred]) 311 312lemma sym_UNION: "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (\<Union>(r ` S))" 313 by (fast intro: symI elim: symE) 314 315lemma symp_SUP: "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (\<Squnion>(r ` S))" 316 by (fact sym_UNION [to_pred]) 317 318 319subsubsection \<open>Antisymmetry\<close> 320 321definition antisym :: "'a rel \<Rightarrow> bool" 322 where "antisym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r \<longrightarrow> x = y)" 323 324definition antisymp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 325 where "antisymp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> r y x \<longrightarrow> x = y)" 326 327lemma antisymp_antisym_eq [pred_set_conv]: "antisymp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> antisym r" 328 by (simp add: antisym_def antisymp_def) 329 330lemma antisymI [intro?]: 331 "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> x = y) \<Longrightarrow> antisym r" 332 unfolding antisym_def by iprover 333 334lemma antisympI [intro?]: 335 "(\<And>x y. r x y \<Longrightarrow> r y x \<Longrightarrow> x = y) \<Longrightarrow> antisymp r" 336 by (fact antisymI [to_pred]) 337 338lemma antisymD [dest?]: 339 "antisym r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r \<Longrightarrow> a = b" 340 unfolding antisym_def by iprover 341 342lemma antisympD [dest?]: 343 "antisymp r \<Longrightarrow> r a b \<Longrightarrow> r b a \<Longrightarrow> a = b" 344 by (fact antisymD [to_pred]) 345 346lemma antisym_subset: 347 "r \<subseteq> s \<Longrightarrow> antisym s \<Longrightarrow> antisym r" 348 unfolding antisym_def by blast 349 350lemma antisymp_less_eq: 351 "r \<le> s \<Longrightarrow> antisymp s \<Longrightarrow> antisymp r" 352 by (fact antisym_subset [to_pred]) 353 354lemma antisym_empty [simp]: 355 "antisym {}" 356 unfolding antisym_def by blast 357 358lemma antisym_bot [simp]: 359 "antisymp \<bottom>" 360 by (fact antisym_empty [to_pred]) 361 362lemma antisymp_equality [simp]: 363 "antisymp HOL.eq" 364 by (auto intro: antisympI) 365 366lemma antisym_singleton [simp]: 367 "antisym {x}" 368 by (blast intro: antisymI) 369 370 371subsubsection \<open>Transitivity\<close> 372 373definition trans :: "'a rel \<Rightarrow> bool" 374 where "trans r \<longleftrightarrow> (\<forall>x y z. (x, y) \<in> r \<longrightarrow> (y, z) \<in> r \<longrightarrow> (x, z) \<in> r)" 375 376definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 377 where "transp r \<longleftrightarrow> (\<forall>x y z. r x y \<longrightarrow> r y z \<longrightarrow> r x z)" 378 379lemma transp_trans_eq [pred_set_conv]: "transp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> trans r" 380 by (simp add: trans_def transp_def) 381 382lemma transI [intro?]: "(\<And>x y z. (x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r) \<Longrightarrow> trans r" 383 by (unfold trans_def) iprover 384 385lemma transpI [intro?]: "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r" 386 by (fact transI [to_pred]) 387 388lemma transE: 389 assumes "trans r" and "(x, y) \<in> r" and "(y, z) \<in> r" 390 obtains "(x, z) \<in> r" 391 using assms by (unfold trans_def) iprover 392 393lemma transpE: 394 assumes "transp r" and "r x y" and "r y z" 395 obtains "r x z" 396 using assms by (rule transE [to_pred]) 397 398lemma transD [dest?]: 399 assumes "trans r" and "(x, y) \<in> r" and "(y, z) \<in> r" 400 shows "(x, z) \<in> r" 401 using assms by (rule transE) 402 403lemma transpD [dest?]: 404 assumes "transp r" and "r x y" and "r y z" 405 shows "r x z" 406 using assms by (rule transD [to_pred]) 407 408lemma trans_Int: "trans r \<Longrightarrow> trans s \<Longrightarrow> trans (r \<inter> s)" 409 by (fast intro: transI elim: transE) 410 411lemma transp_inf: "transp r \<Longrightarrow> transp s \<Longrightarrow> transp (r \<sqinter> s)" 412 by (fact trans_Int [to_pred]) 413 414lemma trans_INTER: "\<forall>x\<in>S. trans (r x) \<Longrightarrow> trans (\<Inter>(r ` S))" 415 by (fast intro: transI elim: transD) 416 417lemma transp_INF: "\<forall>x\<in>S. transp (r x) \<Longrightarrow> transp (\<Sqinter>(r ` S))" 418 by (fact trans_INTER [to_pred]) 419 420lemma trans_join [code]: "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)" 421 by (auto simp add: trans_def) 422 423lemma transp_trans: "transp r \<longleftrightarrow> trans {(x, y). r x y}" 424 by (simp add: trans_def transp_def) 425 426lemma transp_equality [simp]: "transp (=)" 427 by (auto intro: transpI) 428 429lemma trans_empty [simp]: "trans {}" 430 by (blast intro: transI) 431 432lemma transp_empty [simp]: "transp (\<lambda>x y. False)" 433 using trans_empty[to_pred] by (simp add: bot_fun_def) 434 435lemma trans_singleton [simp]: "trans {(a, a)}" 436 by (blast intro: transI) 437 438lemma transp_singleton [simp]: "transp (\<lambda>x y. x = a \<and> y = a)" 439 by (simp add: transp_def) 440 441context preorder 442begin 443 444lemma transp_le[simp]: "transp (\<le>)" 445by(auto simp add: transp_def intro: order_trans) 446 447lemma transp_less[simp]: "transp (<)" 448by(auto simp add: transp_def intro: less_trans) 449 450lemma transp_ge[simp]: "transp (\<ge>)" 451by(auto simp add: transp_def intro: order_trans) 452 453lemma transp_gr[simp]: "transp (>)" 454by(auto simp add: transp_def intro: less_trans) 455 456end 457 458subsubsection \<open>Totality\<close> 459 460definition total_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool" 461 where "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)" 462 463lemma total_onI [intro?]: 464 "(\<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r) \<Longrightarrow> total_on A r" 465 unfolding total_on_def by blast 466 467abbreviation "total \<equiv> total_on UNIV" 468 469lemma total_on_empty [simp]: "total_on {} r" 470 by (simp add: total_on_def) 471 472lemma total_on_singleton [simp]: "total_on {x} {(x, x)}" 473 unfolding total_on_def by blast 474 475 476subsubsection \<open>Single valued relations\<close> 477 478definition single_valued :: "('a \<times> 'b) set \<Rightarrow> bool" 479 where "single_valued r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (\<forall>z. (x, z) \<in> r \<longrightarrow> y = z))" 480 481definition single_valuedp :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" 482 where "single_valuedp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> (\<forall>z. r x z \<longrightarrow> y = z))" 483 484lemma single_valuedp_single_valued_eq [pred_set_conv]: 485 "single_valuedp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> single_valued r" 486 by (simp add: single_valued_def single_valuedp_def) 487 488lemma single_valuedI: 489 "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (\<And>z. (x, z) \<in> r \<Longrightarrow> y = z)) \<Longrightarrow> single_valued r" 490 unfolding single_valued_def by blast 491 492lemma single_valuedpI: 493 "(\<And>x y. r x y \<Longrightarrow> (\<And>z. r x z \<Longrightarrow> y = z)) \<Longrightarrow> single_valuedp r" 494 by (fact single_valuedI [to_pred]) 495 496lemma single_valuedD: 497 "single_valued r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (x, z) \<in> r \<Longrightarrow> y = z" 498 by (simp add: single_valued_def) 499 500lemma single_valuedpD: 501 "single_valuedp r \<Longrightarrow> r x y \<Longrightarrow> r x z \<Longrightarrow> y = z" 502 by (fact single_valuedD [to_pred]) 503 504lemma single_valued_empty [simp]: 505 "single_valued {}" 506 by (simp add: single_valued_def) 507 508lemma single_valuedp_bot [simp]: 509 "single_valuedp \<bottom>" 510 by (fact single_valued_empty [to_pred]) 511 512lemma single_valued_subset: 513 "r \<subseteq> s \<Longrightarrow> single_valued s \<Longrightarrow> single_valued r" 514 unfolding single_valued_def by blast 515 516lemma single_valuedp_less_eq: 517 "r \<le> s \<Longrightarrow> single_valuedp s \<Longrightarrow> single_valuedp r" 518 by (fact single_valued_subset [to_pred]) 519 520 521subsection \<open>Relation operations\<close> 522 523subsubsection \<open>The identity relation\<close> 524 525definition Id :: "'a rel" 526 where "Id = {p. \<exists>x. p = (x, x)}" 527 528lemma IdI [intro]: "(a, a) \<in> Id" 529 by (simp add: Id_def) 530 531lemma IdE [elim!]: "p \<in> Id \<Longrightarrow> (\<And>x. p = (x, x) \<Longrightarrow> P) \<Longrightarrow> P" 532 unfolding Id_def by (iprover elim: CollectE) 533 534lemma pair_in_Id_conv [iff]: "(a, b) \<in> Id \<longleftrightarrow> a = b" 535 unfolding Id_def by blast 536 537lemma refl_Id: "refl Id" 538 by (simp add: refl_on_def) 539 540lemma antisym_Id: "antisym Id" 541 \<comment> \<open>A strange result, since \<open>Id\<close> is also symmetric.\<close> 542 by (simp add: antisym_def) 543 544lemma sym_Id: "sym Id" 545 by (simp add: sym_def) 546 547lemma trans_Id: "trans Id" 548 by (simp add: trans_def) 549 550lemma single_valued_Id [simp]: "single_valued Id" 551 by (unfold single_valued_def) blast 552 553lemma irrefl_diff_Id [simp]: "irrefl (r - Id)" 554 by (simp add: irrefl_def) 555 556lemma trans_diff_Id: "trans r \<Longrightarrow> antisym r \<Longrightarrow> trans (r - Id)" 557 unfolding antisym_def trans_def by blast 558 559lemma total_on_diff_Id [simp]: "total_on A (r - Id) = total_on A r" 560 by (simp add: total_on_def) 561 562lemma Id_fstsnd_eq: "Id = {x. fst x = snd x}" 563 by force 564 565 566subsubsection \<open>Diagonal: identity over a set\<close> 567 568definition Id_on :: "'a set \<Rightarrow> 'a rel" 569 where "Id_on A = (\<Union>x\<in>A. {(x, x)})" 570 571lemma Id_on_empty [simp]: "Id_on {} = {}" 572 by (simp add: Id_on_def) 573 574lemma Id_on_eqI: "a = b \<Longrightarrow> a \<in> A \<Longrightarrow> (a, b) \<in> Id_on A" 575 by (simp add: Id_on_def) 576 577lemma Id_onI [intro!]: "a \<in> A \<Longrightarrow> (a, a) \<in> Id_on A" 578 by (rule Id_on_eqI) (rule refl) 579 580lemma Id_onE [elim!]: "c \<in> Id_on A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> c = (x, x) \<Longrightarrow> P) \<Longrightarrow> P" 581 \<comment> \<open>The general elimination rule.\<close> 582 unfolding Id_on_def by (iprover elim!: UN_E singletonE) 583 584lemma Id_on_iff: "(x, y) \<in> Id_on A \<longleftrightarrow> x = y \<and> x \<in> A" 585 by blast 586 587lemma Id_on_def' [nitpick_unfold]: "Id_on {x. A x} = Collect (\<lambda>(x, y). x = y \<and> A x)" 588 by auto 589 590lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> A" 591 by blast 592 593lemma refl_on_Id_on: "refl_on A (Id_on A)" 594 by (rule refl_onI [OF Id_on_subset_Times Id_onI]) 595 596lemma antisym_Id_on [simp]: "antisym (Id_on A)" 597 unfolding antisym_def by blast 598 599lemma sym_Id_on [simp]: "sym (Id_on A)" 600 by (rule symI) clarify 601 602lemma trans_Id_on [simp]: "trans (Id_on A)" 603 by (fast intro: transI elim: transD) 604 605lemma single_valued_Id_on [simp]: "single_valued (Id_on A)" 606 unfolding single_valued_def by blast 607 608 609subsubsection \<open>Composition\<close> 610 611inductive_set relcomp :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixr "O" 75) 612 for r :: "('a \<times> 'b) set" and s :: "('b \<times> 'c) set" 613 where relcompI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s" 614 615notation relcompp (infixr "OO" 75) 616 617lemmas relcomppI = relcompp.intros 618 619text \<open> 620 For historic reasons, the elimination rules are not wholly corresponding. 621 Feel free to consolidate this. 622\<close> 623 624inductive_cases relcompEpair: "(a, c) \<in> r O s" 625inductive_cases relcomppE [elim!]: "(r OO s) a c" 626 627lemma relcompE [elim!]: "xz \<in> r O s \<Longrightarrow> 628 (\<And>x y z. xz = (x, z) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> s \<Longrightarrow> P) \<Longrightarrow> P" 629 apply (cases xz) 630 apply simp 631 apply (erule relcompEpair) 632 apply iprover 633 done 634 635lemma R_O_Id [simp]: "R O Id = R" 636 by fast 637 638lemma Id_O_R [simp]: "Id O R = R" 639 by fast 640 641lemma relcomp_empty1 [simp]: "{} O R = {}" 642 by blast 643 644lemma relcompp_bot1 [simp]: "\<bottom> OO R = \<bottom>" 645 by (fact relcomp_empty1 [to_pred]) 646 647lemma relcomp_empty2 [simp]: "R O {} = {}" 648 by blast 649 650lemma relcompp_bot2 [simp]: "R OO \<bottom> = \<bottom>" 651 by (fact relcomp_empty2 [to_pred]) 652 653lemma O_assoc: "(R O S) O T = R O (S O T)" 654 by blast 655 656lemma relcompp_assoc: "(r OO s) OO t = r OO (s OO t)" 657 by (fact O_assoc [to_pred]) 658 659lemma trans_O_subset: "trans r \<Longrightarrow> r O r \<subseteq> r" 660 by (unfold trans_def) blast 661 662lemma transp_relcompp_less_eq: "transp r \<Longrightarrow> r OO r \<le> r " 663 by (fact trans_O_subset [to_pred]) 664 665lemma relcomp_mono: "r' \<subseteq> r \<Longrightarrow> s' \<subseteq> s \<Longrightarrow> r' O s' \<subseteq> r O s" 666 by blast 667 668lemma relcompp_mono: "r' \<le> r \<Longrightarrow> s' \<le> s \<Longrightarrow> r' OO s' \<le> r OO s " 669 by (fact relcomp_mono [to_pred]) 670 671lemma relcomp_subset_Sigma: "r \<subseteq> A \<times> B \<Longrightarrow> s \<subseteq> B \<times> C \<Longrightarrow> r O s \<subseteq> A \<times> C" 672 by blast 673 674lemma relcomp_distrib [simp]: "R O (S \<union> T) = (R O S) \<union> (R O T)" 675 by auto 676 677lemma relcompp_distrib [simp]: "R OO (S \<squnion> T) = R OO S \<squnion> R OO T" 678 by (fact relcomp_distrib [to_pred]) 679 680lemma relcomp_distrib2 [simp]: "(S \<union> T) O R = (S O R) \<union> (T O R)" 681 by auto 682 683lemma relcompp_distrib2 [simp]: "(S \<squnion> T) OO R = S OO R \<squnion> T OO R" 684 by (fact relcomp_distrib2 [to_pred]) 685 686lemma relcomp_UNION_distrib: "s O \<Union>(r ` I) = (\<Union>i\<in>I. s O r i) " 687 by auto 688 689lemma relcompp_SUP_distrib: "s OO \<Squnion>(r ` I) = (\<Squnion>i\<in>I. s OO r i)" 690 by (fact relcomp_UNION_distrib [to_pred]) 691 692lemma relcomp_UNION_distrib2: "\<Union>(r ` I) O s = (\<Union>i\<in>I. r i O s) " 693 by auto 694 695lemma relcompp_SUP_distrib2: "\<Squnion>(r ` I) OO s = (\<Squnion>i\<in>I. r i OO s)" 696 by (fact relcomp_UNION_distrib2 [to_pred]) 697 698lemma single_valued_relcomp: "single_valued r \<Longrightarrow> single_valued s \<Longrightarrow> single_valued (r O s)" 699 unfolding single_valued_def by blast 700 701lemma relcomp_unfold: "r O s = {(x, z). \<exists>y. (x, y) \<in> r \<and> (y, z) \<in> s}" 702 by (auto simp add: set_eq_iff) 703 704lemma relcompp_apply: "(R OO S) a c \<longleftrightarrow> (\<exists>b. R a b \<and> S b c)" 705 unfolding relcomp_unfold [to_pred] .. 706 707lemma eq_OO: "(=) OO R = R" 708 by blast 709 710lemma OO_eq: "R OO (=) = R" 711 by blast 712 713 714subsubsection \<open>Converse\<close> 715 716inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set" ("(_\<inverse>)" [1000] 999) 717 for r :: "('a \<times> 'b) set" 718 where "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>" 719 720notation conversep ("(_\<inverse>\<inverse>)" [1000] 1000) 721 722notation (ASCII) 723 converse ("(_^-1)" [1000] 999) and 724 conversep ("(_^--1)" [1000] 1000) 725 726lemma converseI [sym]: "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>" 727 by (fact converse.intros) 728 729lemma conversepI (* CANDIDATE [sym] *): "r a b \<Longrightarrow> r\<inverse>\<inverse> b a" 730 by (fact conversep.intros) 731 732lemma converseD [sym]: "(a, b) \<in> r\<inverse> \<Longrightarrow> (b, a) \<in> r" 733 by (erule converse.cases) iprover 734 735lemma conversepD (* CANDIDATE [sym] *): "r\<inverse>\<inverse> b a \<Longrightarrow> r a b" 736 by (fact converseD [to_pred]) 737 738lemma converseE [elim!]: "yx \<in> r\<inverse> \<Longrightarrow> (\<And>x y. yx = (y, x) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> P) \<Longrightarrow> P" 739 \<comment> \<open>More general than \<open>converseD\<close>, as it ``splits'' the member of the relation.\<close> 740 apply (cases yx) 741 apply simp 742 apply (erule converse.cases) 743 apply iprover 744 done 745 746lemmas conversepE [elim!] = conversep.cases 747 748lemma converse_iff [iff]: "(a, b) \<in> r\<inverse> \<longleftrightarrow> (b, a) \<in> r" 749 by (auto intro: converseI) 750 751lemma conversep_iff [iff]: "r\<inverse>\<inverse> a b = r b a" 752 by (fact converse_iff [to_pred]) 753 754lemma converse_converse [simp]: "(r\<inverse>)\<inverse> = r" 755 by (simp add: set_eq_iff) 756 757lemma conversep_conversep [simp]: "(r\<inverse>\<inverse>)\<inverse>\<inverse> = r" 758 by (fact converse_converse [to_pred]) 759 760lemma converse_empty[simp]: "{}\<inverse> = {}" 761 by auto 762 763lemma converse_UNIV[simp]: "UNIV\<inverse> = UNIV" 764 by auto 765 766lemma converse_relcomp: "(r O s)\<inverse> = s\<inverse> O r\<inverse>" 767 by blast 768 769lemma converse_relcompp: "(r OO s)\<inverse>\<inverse> = s\<inverse>\<inverse> OO r\<inverse>\<inverse>" 770 by (iprover intro: order_antisym conversepI relcomppI elim: relcomppE dest: conversepD) 771 772lemma converse_Int: "(r \<inter> s)\<inverse> = r\<inverse> \<inter> s\<inverse>" 773 by blast 774 775lemma converse_meet: "(r \<sqinter> s)\<inverse>\<inverse> = r\<inverse>\<inverse> \<sqinter> s\<inverse>\<inverse>" 776 by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD) 777 778lemma converse_Un: "(r \<union> s)\<inverse> = r\<inverse> \<union> s\<inverse>" 779 by blast 780 781lemma converse_join: "(r \<squnion> s)\<inverse>\<inverse> = r\<inverse>\<inverse> \<squnion> s\<inverse>\<inverse>" 782 by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD) 783 784lemma converse_INTER: "(\<Inter>(r ` S))\<inverse> = (\<Inter>x\<in>S. (r x)\<inverse>)" 785 by fast 786 787lemma converse_UNION: "(\<Union>(r ` S))\<inverse> = (\<Union>x\<in>S. (r x)\<inverse>)" 788 by blast 789 790lemma converse_mono[simp]: "r\<inverse> \<subseteq> s \<inverse> \<longleftrightarrow> r \<subseteq> s" 791 by auto 792 793lemma conversep_mono[simp]: "r\<inverse>\<inverse> \<le> s \<inverse>\<inverse> \<longleftrightarrow> r \<le> s" 794 by (fact converse_mono[to_pred]) 795 796lemma converse_inject[simp]: "r\<inverse> = s \<inverse> \<longleftrightarrow> r = s" 797 by auto 798 799lemma conversep_inject[simp]: "r\<inverse>\<inverse> = s \<inverse>\<inverse> \<longleftrightarrow> r = s" 800 by (fact converse_inject[to_pred]) 801 802lemma converse_subset_swap: "r \<subseteq> s \<inverse> \<longleftrightarrow> r \<inverse> \<subseteq> s" 803 by auto 804 805lemma conversep_le_swap: "r \<le> s \<inverse>\<inverse> \<longleftrightarrow> r \<inverse>\<inverse> \<le> s" 806 by (fact converse_subset_swap[to_pred]) 807 808lemma converse_Id [simp]: "Id\<inverse> = Id" 809 by blast 810 811lemma converse_Id_on [simp]: "(Id_on A)\<inverse> = Id_on A" 812 by blast 813 814lemma refl_on_converse [simp]: "refl_on A (converse r) = refl_on A r" 815 by (auto simp: refl_on_def) 816 817lemma sym_converse [simp]: "sym (converse r) = sym r" 818 unfolding sym_def by blast 819 820lemma antisym_converse [simp]: "antisym (converse r) = antisym r" 821 unfolding antisym_def by blast 822 823lemma trans_converse [simp]: "trans (converse r) = trans r" 824 unfolding trans_def by blast 825 826lemma sym_conv_converse_eq: "sym r \<longleftrightarrow> r\<inverse> = r" 827 unfolding sym_def by fast 828 829lemma sym_Un_converse: "sym (r \<union> r\<inverse>)" 830 unfolding sym_def by blast 831 832lemma sym_Int_converse: "sym (r \<inter> r\<inverse>)" 833 unfolding sym_def by blast 834 835lemma total_on_converse [simp]: "total_on A (r\<inverse>) = total_on A r" 836 by (auto simp: total_on_def) 837 838lemma finite_converse [iff]: "finite (r\<inverse>) = finite r" 839unfolding converse_def conversep_iff using [[simproc add: finite_Collect]] 840by (auto elim: finite_imageD simp: inj_on_def) 841 842lemma card_inverse[simp]: "card (R\<inverse>) = card R" 843proof - 844 have *: "\<And>R. prod.swap ` R = R\<inverse>" by auto 845 { 846 assume "\<not>finite R" 847 hence ?thesis 848 by auto 849 } moreover { 850 assume "finite R" 851 with card_image_le[of R prod.swap] card_image_le[of "R\<inverse>" prod.swap] 852 have ?thesis by (auto simp: *) 853 } ultimately show ?thesis by blast 854qed 855 856lemma conversep_noteq [simp]: "(\<noteq>)\<inverse>\<inverse> = (\<noteq>)" 857 by (auto simp add: fun_eq_iff) 858 859lemma conversep_eq [simp]: "(=)\<inverse>\<inverse> = (=)" 860 by (auto simp add: fun_eq_iff) 861 862lemma converse_unfold [code]: "r\<inverse> = {(y, x). (x, y) \<in> r}" 863 by (simp add: set_eq_iff) 864 865 866subsubsection \<open>Domain, range and field\<close> 867 868inductive_set Domain :: "('a \<times> 'b) set \<Rightarrow> 'a set" for r :: "('a \<times> 'b) set" 869 where DomainI [intro]: "(a, b) \<in> r \<Longrightarrow> a \<in> Domain r" 870 871lemmas DomainPI = Domainp.DomainI 872 873inductive_cases DomainE [elim!]: "a \<in> Domain r" 874inductive_cases DomainpE [elim!]: "Domainp r a" 875 876inductive_set Range :: "('a \<times> 'b) set \<Rightarrow> 'b set" for r :: "('a \<times> 'b) set" 877 where RangeI [intro]: "(a, b) \<in> r \<Longrightarrow> b \<in> Range r" 878 879lemmas RangePI = Rangep.RangeI 880 881inductive_cases RangeE [elim!]: "b \<in> Range r" 882inductive_cases RangepE [elim!]: "Rangep r b" 883 884definition Field :: "'a rel \<Rightarrow> 'a set" 885 where "Field r = Domain r \<union> Range r" 886 887lemma FieldI1: "(i, j) \<in> R \<Longrightarrow> i \<in> Field R" 888 unfolding Field_def by blast 889 890lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R" 891 unfolding Field_def by auto 892 893lemma Domain_fst [code]: "Domain r = fst ` r" 894 by force 895 896lemma Range_snd [code]: "Range r = snd ` r" 897 by force 898 899lemma fst_eq_Domain: "fst ` R = Domain R" 900 by force 901 902lemma snd_eq_Range: "snd ` R = Range R" 903 by force 904 905lemma range_fst [simp]: "range fst = UNIV" 906 by (auto simp: fst_eq_Domain) 907 908lemma range_snd [simp]: "range snd = UNIV" 909 by (auto simp: snd_eq_Range) 910 911lemma Domain_empty [simp]: "Domain {} = {}" 912 by auto 913 914lemma Range_empty [simp]: "Range {} = {}" 915 by auto 916 917lemma Field_empty [simp]: "Field {} = {}" 918 by (simp add: Field_def) 919 920lemma Domain_empty_iff: "Domain r = {} \<longleftrightarrow> r = {}" 921 by auto 922 923lemma Range_empty_iff: "Range r = {} \<longleftrightarrow> r = {}" 924 by auto 925 926lemma Domain_insert [simp]: "Domain (insert (a, b) r) = insert a (Domain r)" 927 by blast 928 929lemma Range_insert [simp]: "Range (insert (a, b) r) = insert b (Range r)" 930 by blast 931 932lemma Field_insert [simp]: "Field (insert (a, b) r) = {a, b} \<union> Field r" 933 by (auto simp add: Field_def) 934 935lemma Domain_iff: "a \<in> Domain r \<longleftrightarrow> (\<exists>y. (a, y) \<in> r)" 936 by blast 937 938lemma Range_iff: "a \<in> Range r \<longleftrightarrow> (\<exists>y. (y, a) \<in> r)" 939 by blast 940 941lemma Domain_Id [simp]: "Domain Id = UNIV" 942 by blast 943 944lemma Range_Id [simp]: "Range Id = UNIV" 945 by blast 946 947lemma Domain_Id_on [simp]: "Domain (Id_on A) = A" 948 by blast 949 950lemma Range_Id_on [simp]: "Range (Id_on A) = A" 951 by blast 952 953lemma Domain_Un_eq: "Domain (A \<union> B) = Domain A \<union> Domain B" 954 by blast 955 956lemma Range_Un_eq: "Range (A \<union> B) = Range A \<union> Range B" 957 by blast 958 959lemma Field_Un [simp]: "Field (r \<union> s) = Field r \<union> Field s" 960 by (auto simp: Field_def) 961 962lemma Domain_Int_subset: "Domain (A \<inter> B) \<subseteq> Domain A \<inter> Domain B" 963 by blast 964 965lemma Range_Int_subset: "Range (A \<inter> B) \<subseteq> Range A \<inter> Range B" 966 by blast 967 968lemma Domain_Diff_subset: "Domain A - Domain B \<subseteq> Domain (A - B)" 969 by blast 970 971lemma Range_Diff_subset: "Range A - Range B \<subseteq> Range (A - B)" 972 by blast 973 974lemma Domain_Union: "Domain (\<Union>S) = (\<Union>A\<in>S. Domain A)" 975 by blast 976 977lemma Range_Union: "Range (\<Union>S) = (\<Union>A\<in>S. Range A)" 978 by blast 979 980lemma Field_Union [simp]: "Field (\<Union>R) = \<Union>(Field ` R)" 981 by (auto simp: Field_def) 982 983lemma Domain_converse [simp]: "Domain (r\<inverse>) = Range r" 984 by auto 985 986lemma Range_converse [simp]: "Range (r\<inverse>) = Domain r" 987 by blast 988 989lemma Field_converse [simp]: "Field (r\<inverse>) = Field r" 990 by (auto simp: Field_def) 991 992lemma Domain_Collect_case_prod [simp]: "Domain {(x, y). P x y} = {x. \<exists>y. P x y}" 993 by auto 994 995lemma Range_Collect_case_prod [simp]: "Range {(x, y). P x y} = {y. \<exists>x. P x y}" 996 by auto 997 998lemma finite_Domain: "finite r \<Longrightarrow> finite (Domain r)" 999 by (induct set: finite) auto 1000 1001lemma finite_Range: "finite r \<Longrightarrow> finite (Range r)" 1002 by (induct set: finite) auto 1003 1004lemma finite_Field: "finite r \<Longrightarrow> finite (Field r)" 1005 by (simp add: Field_def finite_Domain finite_Range) 1006 1007lemma Domain_mono: "r \<subseteq> s \<Longrightarrow> Domain r \<subseteq> Domain s" 1008 by blast 1009 1010lemma Range_mono: "r \<subseteq> s \<Longrightarrow> Range r \<subseteq> Range s" 1011 by blast 1012 1013lemma mono_Field: "r \<subseteq> s \<Longrightarrow> Field r \<subseteq> Field s" 1014 by (auto simp: Field_def Domain_def Range_def) 1015 1016lemma Domain_unfold: "Domain r = {x. \<exists>y. (x, y) \<in> r}" 1017 by blast 1018 1019lemma Field_square [simp]: "Field (x \<times> x) = x" 1020 unfolding Field_def by blast 1021 1022 1023subsubsection \<open>Image of a set under a relation\<close> 1024 1025definition Image :: "('a \<times> 'b) set \<Rightarrow> 'a set \<Rightarrow> 'b set" (infixr "``" 90) 1026 where "r `` s = {y. \<exists>x\<in>s. (x, y) \<in> r}" 1027 1028lemma Image_iff: "b \<in> r``A \<longleftrightarrow> (\<exists>x\<in>A. (x, b) \<in> r)" 1029 by (simp add: Image_def) 1030 1031lemma Image_singleton: "r``{a} = {b. (a, b) \<in> r}" 1032 by (simp add: Image_def) 1033 1034lemma Image_singleton_iff [iff]: "b \<in> r``{a} \<longleftrightarrow> (a, b) \<in> r" 1035 by (rule Image_iff [THEN trans]) simp 1036 1037lemma ImageI [intro]: "(a, b) \<in> r \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> r``A" 1038 unfolding Image_def by blast 1039 1040lemma ImageE [elim!]: "b \<in> r `` A \<Longrightarrow> (\<And>x. (x, b) \<in> r \<Longrightarrow> x \<in> A \<Longrightarrow> P) \<Longrightarrow> P" 1041 unfolding Image_def by (iprover elim!: CollectE bexE) 1042 1043lemma rev_ImageI: "a \<in> A \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> b \<in> r `` A" 1044 \<comment> \<open>This version's more effective when we already have the required \<open>a\<close>\<close> 1045 by blast 1046 1047lemma Image_empty1 [simp]: "{} `` X = {}" 1048by auto 1049 1050lemma Image_empty2 [simp]: "R``{} = {}" 1051by blast 1052 1053lemma Image_Id [simp]: "Id `` A = A" 1054 by blast 1055 1056lemma Image_Id_on [simp]: "Id_on A `` B = A \<inter> B" 1057 by blast 1058 1059lemma Image_Int_subset: "R `` (A \<inter> B) \<subseteq> R `` A \<inter> R `` B" 1060 by blast 1061 1062lemma Image_Int_eq: "single_valued (converse R) \<Longrightarrow> R `` (A \<inter> B) = R `` A \<inter> R `` B" 1063 by (auto simp: single_valued_def) 1064 1065lemma Image_Un: "R `` (A \<union> B) = R `` A \<union> R `` B" 1066 by blast 1067 1068lemma Un_Image: "(R \<union> S) `` A = R `` A \<union> S `` A" 1069 by blast 1070 1071lemma Image_subset: "r \<subseteq> A \<times> B \<Longrightarrow> r``C \<subseteq> B" 1072 by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2) 1073 1074lemma Image_eq_UN: "r``B = (\<Union>y\<in> B. r``{y})" 1075 \<comment> \<open>NOT suitable for rewriting\<close> 1076 by blast 1077 1078lemma Image_mono: "r' \<subseteq> r \<Longrightarrow> A' \<subseteq> A \<Longrightarrow> (r' `` A') \<subseteq> (r `` A)" 1079 by blast 1080 1081lemma Image_UN: "r `` (\<Union>(B ` A)) = (\<Union>x\<in>A. r `` (B x))" 1082 by blast 1083 1084lemma UN_Image: "(\<Union>i\<in>I. X i) `` S = (\<Union>i\<in>I. X i `` S)" 1085 by auto 1086 1087lemma Image_INT_subset: "(r `` (\<Inter>(B ` A))) \<subseteq> (\<Inter>x\<in>A. r `` (B x))" 1088 by blast 1089 1090text \<open>Converse inclusion requires some assumptions\<close> 1091lemma Image_INT_eq: "single_valued (r\<inverse>) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> r `` (\<Inter>(B ` A)) = (\<Inter>x\<in>A. r `` B x)" 1092 apply (rule equalityI) 1093 apply (rule Image_INT_subset) 1094 apply (auto simp add: single_valued_def) 1095 apply blast 1096 done 1097 1098lemma Image_subset_eq: "r``A \<subseteq> B \<longleftrightarrow> A \<subseteq> - ((r\<inverse>) `` (- B))" 1099 by blast 1100 1101lemma Image_Collect_case_prod [simp]: "{(x, y). P x y} `` A = {y. \<exists>x\<in>A. P x y}" 1102 by auto 1103 1104lemma Sigma_Image: "(SIGMA x:A. B x) `` X = (\<Union>x\<in>X \<inter> A. B x)" 1105 by auto 1106 1107lemma relcomp_Image: "(X O Y) `` Z = Y `` (X `` Z)" 1108 by auto 1109 1110lemma finite_Image[simp]: assumes "finite R" shows "finite (R `` A)" 1111by(rule finite_subset[OF _ finite_Range[OF assms]]) auto 1112 1113 1114subsubsection \<open>Inverse image\<close> 1115 1116definition inv_image :: "'b rel \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a rel" 1117 where "inv_image r f = {(x, y). (f x, f y) \<in> r}" 1118 1119definition inv_imagep :: "('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 1120 where "inv_imagep r f = (\<lambda>x y. r (f x) (f y))" 1121 1122lemma [pred_set_conv]: "inv_imagep (\<lambda>x y. (x, y) \<in> r) f = (\<lambda>x y. (x, y) \<in> inv_image r f)" 1123 by (simp add: inv_image_def inv_imagep_def) 1124 1125lemma sym_inv_image: "sym r \<Longrightarrow> sym (inv_image r f)" 1126 unfolding sym_def inv_image_def by blast 1127 1128lemma trans_inv_image: "trans r \<Longrightarrow> trans (inv_image r f)" 1129 unfolding trans_def inv_image_def 1130 by (simp (no_asm)) blast 1131 1132lemma total_inv_image: "\<lbrakk>inj f; total r\<rbrakk> \<Longrightarrow> total (inv_image r f)" 1133 unfolding inv_image_def total_on_def by (auto simp: inj_eq) 1134 1135lemma in_inv_image[simp]: "(x, y) \<in> inv_image r f \<longleftrightarrow> (f x, f y) \<in> r" 1136 by (auto simp: inv_image_def) 1137 1138lemma converse_inv_image[simp]: "(inv_image R f)\<inverse> = inv_image (R\<inverse>) f" 1139 unfolding inv_image_def converse_unfold by auto 1140 1141lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)" 1142 by (simp add: inv_imagep_def) 1143 1144 1145subsubsection \<open>Powerset\<close> 1146 1147definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" 1148 where "Powp A = (\<lambda>B. \<forall>x \<in> B. A x)" 1149 1150lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)" 1151 by (auto simp add: Powp_def fun_eq_iff) 1152 1153lemmas Powp_mono [mono] = Pow_mono [to_pred] 1154 1155 1156subsubsection \<open>Expressing relation operations via \<^const>\<open>Finite_Set.fold\<close>\<close> 1157 1158lemma Id_on_fold: 1159 assumes "finite A" 1160 shows "Id_on A = Finite_Set.fold (\<lambda>x. Set.insert (Pair x x)) {} A" 1161proof - 1162 interpret comp_fun_commute "\<lambda>x. Set.insert (Pair x x)" 1163 by standard auto 1164 from assms show ?thesis 1165 unfolding Id_on_def by (induct A) simp_all 1166qed 1167 1168lemma comp_fun_commute_Image_fold: 1169 "comp_fun_commute (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A)" 1170proof - 1171 interpret comp_fun_idem Set.insert 1172 by (fact comp_fun_idem_insert) 1173 show ?thesis 1174 by standard (auto simp: fun_eq_iff comp_fun_commute split: prod.split) 1175qed 1176 1177lemma Image_fold: 1178 assumes "finite R" 1179 shows "R `` S = Finite_Set.fold (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A) {} R" 1180proof - 1181 interpret comp_fun_commute "(\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A)" 1182 by (rule comp_fun_commute_Image_fold) 1183 have *: "\<And>x F. Set.insert x F `` S = (if fst x \<in> S then Set.insert (snd x) (F `` S) else (F `` S))" 1184 by (force intro: rev_ImageI) 1185 show ?thesis 1186 using assms by (induct R) (auto simp: *) 1187qed 1188 1189lemma insert_relcomp_union_fold: 1190 assumes "finite S" 1191 shows "{x} O S \<union> X = Finite_Set.fold (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A') X S" 1192proof - 1193 interpret comp_fun_commute "\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A'" 1194 proof - 1195 interpret comp_fun_idem Set.insert 1196 by (fact comp_fun_idem_insert) 1197 show "comp_fun_commute (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A')" 1198 by standard (auto simp add: fun_eq_iff split: prod.split) 1199 qed 1200 have *: "{x} O S = {(x', z). x' = fst x \<and> (snd x, z) \<in> S}" 1201 by (auto simp: relcomp_unfold intro!: exI) 1202 show ?thesis 1203 unfolding * using \<open>finite S\<close> by (induct S) (auto split: prod.split) 1204qed 1205 1206lemma insert_relcomp_fold: 1207 assumes "finite S" 1208 shows "Set.insert x R O S = 1209 Finite_Set.fold (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A') (R O S) S" 1210proof - 1211 have "Set.insert x R O S = ({x} O S) \<union> (R O S)" 1212 by auto 1213 then show ?thesis 1214 by (auto simp: insert_relcomp_union_fold [OF assms]) 1215qed 1216 1217lemma comp_fun_commute_relcomp_fold: 1218 assumes "finite S" 1219 shows "comp_fun_commute (\<lambda>(x,y) A. 1220 Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S)" 1221proof - 1222 have *: "\<And>a b A. 1223 Finite_Set.fold (\<lambda>(w, z) A'. if b = w then Set.insert (a, z) A' else A') A S = {(a,b)} O S \<union> A" 1224 by (auto simp: insert_relcomp_union_fold[OF assms] cong: if_cong) 1225 show ?thesis 1226 by standard (auto simp: *) 1227qed 1228 1229lemma relcomp_fold: 1230 assumes "finite R" "finite S" 1231 shows "R O S = Finite_Set.fold 1232 (\<lambda>(x,y) A. Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S) {} R" 1233 using assms 1234 by (induct R) 1235 (auto simp: comp_fun_commute.fold_insert comp_fun_commute_relcomp_fold insert_relcomp_fold 1236 cong: if_cong) 1237 1238end 1239