equal
deleted
inserted
replaced
387 by (fact trans_Int [to_pred]) |
387 by (fact trans_Int [to_pred]) |
388 |
388 |
389 lemma trans_INTER: "\<forall>x\<in>S. trans (r x) \<Longrightarrow> trans (INTER S r)" |
389 lemma trans_INTER: "\<forall>x\<in>S. trans (r x) \<Longrightarrow> trans (INTER S r)" |
390 by (fast intro: transI elim: transD) |
390 by (fast intro: transI elim: transD) |
391 |
391 |
392 (* FIXME thm trans_INTER [to_pred] *) |
392 lemma transp_INF: "\<forall>x\<in>S. transp (r x) \<Longrightarrow> transp (INFIMUM S r)" |
393 |
393 by (fact trans_INTER [to_pred]) |
|
394 |
394 lemma trans_join [code]: "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)" |
395 lemma trans_join [code]: "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)" |
395 by (auto simp add: trans_def) |
396 by (auto simp add: trans_def) |
396 |
397 |
397 lemma transp_trans: "transp r \<longleftrightarrow> trans {(x, y). r x y}" |
398 lemma transp_trans: "transp r \<longleftrightarrow> trans {(x, y). r x y}" |
398 by (simp add: trans_def transp_def) |
399 by (simp add: trans_def transp_def) |
618 by (fact relcomp_distrib2 [to_pred]) |
619 by (fact relcomp_distrib2 [to_pred]) |
619 |
620 |
620 lemma relcomp_UNION_distrib: "s O UNION I r = (\<Union>i\<in>I. s O r i) " |
621 lemma relcomp_UNION_distrib: "s O UNION I r = (\<Union>i\<in>I. s O r i) " |
621 by auto |
622 by auto |
622 |
623 |
623 (* FIXME thm relcomp_UNION_distrib [to_pred] *) |
624 lemma relcompp_SUP_distrib: "s OO SUPREMUM I r = (\<Squnion>i\<in>I. s OO r i)" |
624 |
625 by (fact relcomp_UNION_distrib [to_pred]) |
|
626 |
625 lemma relcomp_UNION_distrib2: "UNION I r O s = (\<Union>i\<in>I. r i O s) " |
627 lemma relcomp_UNION_distrib2: "UNION I r O s = (\<Union>i\<in>I. r i O s) " |
626 by auto |
628 by auto |
627 |
629 |
628 (* FIXME thm relcomp_UNION_distrib2 [to_pred] *) |
630 lemma relcompp_SUP_distrib2: "SUPREMUM I r OO s = (\<Squnion>i\<in>I. r i OO s)" |
629 |
631 by (fact relcomp_UNION_distrib2 [to_pred]) |
|
632 |
630 lemma single_valued_relcomp: "single_valued r \<Longrightarrow> single_valued s \<Longrightarrow> single_valued (r O s)" |
633 lemma single_valued_relcomp: "single_valued r \<Longrightarrow> single_valued s \<Longrightarrow> single_valued (r O s)" |
631 unfolding single_valued_def by blast |
634 unfolding single_valued_def by blast |
632 |
635 |
633 lemma relcomp_unfold: "r O s = {(x, z). \<exists>y. (x, y) \<in> r \<and> (y, z) \<in> s}" |
636 lemma relcomp_unfold: "r O s = {(x, z). \<exists>y. (x, y) \<in> r \<and> (y, z) \<in> s}" |
634 by (auto simp add: set_eq_iff) |
637 by (auto simp add: set_eq_iff) |