319 subsubsection \<open>Antisymmetry\<close> |
319 subsubsection \<open>Antisymmetry\<close> |
320 |
320 |
321 definition antisym :: "'a rel \<Rightarrow> bool" |
321 definition 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)" |
322 where "antisym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r \<longrightarrow> x = y)" |
323 |
323 |
324 abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
324 definition antisymp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
325 where "antisymP r \<equiv> antisym {(x, y). r x y}" (* FIXME proper logical operation *) |
325 where "antisymp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> r y x \<longrightarrow> x = y)" |
326 |
326 |
327 lemma antisymI [intro?]: "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> x = y) \<Longrightarrow> antisym r" |
327 lemma 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 |
|
330 lemma antisymI [intro?]: |
|
331 "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> x = y) \<Longrightarrow> antisym r" |
328 unfolding antisym_def by iprover |
332 unfolding antisym_def by iprover |
329 |
333 |
330 lemma antisymD [dest?]: "antisym r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r \<Longrightarrow> a = b" |
334 lemma 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 |
|
338 lemma antisymD [dest?]: |
|
339 "antisym r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r \<Longrightarrow> a = b" |
331 unfolding antisym_def by iprover |
340 unfolding antisym_def by iprover |
332 |
341 |
333 lemma antisym_subset: "r \<subseteq> s \<Longrightarrow> antisym s \<Longrightarrow> antisym r" |
342 lemma antisympD [dest?]: |
|
343 "antisymp r \<Longrightarrow> r a b \<Longrightarrow> r b a \<Longrightarrow> a = b" |
|
344 by (fact antisymD [to_pred]) |
|
345 |
|
346 lemma antisym_subset: |
|
347 "r \<subseteq> s \<Longrightarrow> antisym s \<Longrightarrow> antisym r" |
334 unfolding antisym_def by blast |
348 unfolding antisym_def by blast |
335 |
349 |
336 lemma antisym_empty [simp]: "antisym {}" |
350 lemma antisymp_less_eq: |
|
351 "r \<le> s \<Longrightarrow> antisymp s \<Longrightarrow> antisymp r" |
|
352 by (fact antisym_subset [to_pred]) |
|
353 |
|
354 lemma antisym_empty [simp]: |
|
355 "antisym {}" |
337 unfolding antisym_def by blast |
356 unfolding antisym_def by blast |
338 |
357 |
339 lemma antisymP_equality [simp]: "antisymP op =" |
358 lemma antisym_bot [simp]: |
340 by (auto intro: antisymI) |
359 "antisymp \<bottom>" |
341 |
360 by (fact antisym_empty [to_pred]) |
342 lemma antisym_singleton [simp]: "antisym {x}" |
361 |
343 by (blast intro: antisymI) |
362 lemma antisymp_equality [simp]: |
|
363 "antisymp HOL.eq" |
|
364 by (auto intro: antisympI) |
|
365 |
|
366 lemma antisym_singleton [simp]: |
|
367 "antisym {x}" |
|
368 by (blast intro: antisymI) |
344 |
369 |
345 |
370 |
346 subsubsection \<open>Transitivity\<close> |
371 subsubsection \<open>Transitivity\<close> |
347 |
372 |
348 definition trans :: "'a rel \<Rightarrow> bool" |
373 definition trans :: "'a rel \<Rightarrow> bool" |
435 subsubsection \<open>Single valued relations\<close> |
460 subsubsection \<open>Single valued relations\<close> |
436 |
461 |
437 definition single_valued :: "('a \<times> 'b) set \<Rightarrow> bool" |
462 definition single_valued :: "('a \<times> 'b) set \<Rightarrow> bool" |
438 where "single_valued r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (\<forall>z. (x, z) \<in> r \<longrightarrow> y = z))" |
463 where "single_valued r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (\<forall>z. (x, z) \<in> r \<longrightarrow> y = z))" |
439 |
464 |
440 abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
465 definition single_valuedp :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
441 where "single_valuedP r \<equiv> single_valued {(x, y). r x y}" (* FIXME proper logical operation *) |
466 where "single_valuedp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> (\<forall>z. r x z \<longrightarrow> y = z))" |
442 |
467 |
443 lemma single_valuedI: "\<forall>x y. (x, y) \<in> r \<longrightarrow> (\<forall>z. (x, z) \<in> r \<longrightarrow> y = z) \<Longrightarrow> single_valued r" |
468 lemma single_valuedp_single_valued_eq [pred_set_conv]: |
444 unfolding single_valued_def . |
469 "single_valuedp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> single_valued r" |
445 |
470 by (simp add: single_valued_def single_valuedp_def) |
446 lemma single_valuedD: "single_valued r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (x, z) \<in> r \<Longrightarrow> y = z" |
471 |
|
472 lemma single_valuedI: |
|
473 "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (\<And>z. (x, z) \<in> r \<Longrightarrow> y = z)) \<Longrightarrow> single_valued r" |
|
474 unfolding single_valued_def by blast |
|
475 |
|
476 lemma single_valuedpI: |
|
477 "(\<And>x y. r x y \<Longrightarrow> (\<And>z. r x z \<Longrightarrow> y = z)) \<Longrightarrow> single_valuedp r" |
|
478 by (fact single_valuedI [to_pred]) |
|
479 |
|
480 lemma single_valuedD: |
|
481 "single_valued r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (x, z) \<in> r \<Longrightarrow> y = z" |
447 by (simp add: single_valued_def) |
482 by (simp add: single_valued_def) |
448 |
483 |
449 lemma single_valued_empty[simp]: "single_valued {}" |
484 lemma single_valuedpD: |
|
485 "single_valuedp r \<Longrightarrow> r x y \<Longrightarrow> r x z \<Longrightarrow> y = z" |
|
486 by (fact single_valuedD [to_pred]) |
|
487 |
|
488 lemma single_valued_empty [simp]: |
|
489 "single_valued {}" |
450 by (simp add: single_valued_def) |
490 by (simp add: single_valued_def) |
451 |
491 |
452 lemma single_valued_subset: "r \<subseteq> s \<Longrightarrow> single_valued s \<Longrightarrow> single_valued r" |
492 lemma single_valuedp_bot [simp]: |
|
493 "single_valuedp \<bottom>" |
|
494 by (fact single_valued_empty [to_pred]) |
|
495 |
|
496 lemma single_valued_subset: |
|
497 "r \<subseteq> s \<Longrightarrow> single_valued s \<Longrightarrow> single_valued r" |
453 unfolding single_valued_def by blast |
498 unfolding single_valued_def by blast |
|
499 |
|
500 lemma single_valuedp_less_eq: |
|
501 "r \<le> s \<Longrightarrow> single_valuedp s \<Longrightarrow> single_valuedp r" |
|
502 by (fact single_valued_subset [to_pred]) |
454 |
503 |
455 |
504 |
456 subsection \<open>Relation operations\<close> |
505 subsection \<open>Relation operations\<close> |
457 |
506 |
458 subsubsection \<open>The identity relation\<close> |
507 subsubsection \<open>The identity relation\<close> |