equal
deleted
inserted
replaced
621 lemma transp_def: "transp R \<longleftrightarrow> (\<forall>x y z. R x y \<longrightarrow> R y z \<longrightarrow> R x z)" |
621 lemma transp_def: "transp R \<longleftrightarrow> (\<forall>x y z. R x y \<longrightarrow> R y z \<longrightarrow> R x z)" |
622 by (simp add: transp_on_def) |
622 by (simp add: transp_on_def) |
623 |
623 |
624 text \<open>@{thm [source] trans_def} and @{thm [source] transp_def} are for backward compatibility.\<close> |
624 text \<open>@{thm [source] trans_def} and @{thm [source] transp_def} are for backward compatibility.\<close> |
625 |
625 |
626 lemma transp_trans_eq [pred_set_conv]: "transp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> trans r" |
626 lemma transp_on_trans_on_eq[pred_set_conv]: "transp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> trans_on A r" |
627 by (simp add: trans_def transp_def) |
627 by (simp add: trans_on_def transp_on_def) |
|
628 |
|
629 lemmas transp_trans_eq = transp_on_trans_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close> |
628 |
630 |
629 lemma transI [intro?]: "(\<And>x y z. (x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r) \<Longrightarrow> trans r" |
631 lemma transI [intro?]: "(\<And>x y z. (x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r) \<Longrightarrow> trans r" |
630 by (unfold trans_def) iprover |
632 by (unfold trans_def) iprover |
631 |
633 |
632 lemma transpI [intro?]: "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r" |
634 lemma transpI [intro?]: "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r" |