equal
deleted
inserted
replaced
439 by (auto intro: antisymI elim: asym.cases) |
439 by (auto intro: antisymI elim: asym.cases) |
440 |
440 |
441 lemma antisymp_if_asymp: "asymp R \<Longrightarrow> antisymp R" |
441 lemma antisymp_if_asymp: "asymp R \<Longrightarrow> antisymp R" |
442 by (rule antisym_if_asym[to_pred]) |
442 by (rule antisym_if_asym[to_pred]) |
443 |
443 |
|
444 lemma (in preorder) antisymp_less[simp]: "antisymp (<)" |
|
445 by (rule antisymp_if_asymp[OF asymp_less]) |
|
446 |
|
447 lemma (in preorder) antisymp_greater[simp]: "antisymp (>)" |
|
448 by (rule antisymp_if_asymp[OF asymp_greater]) |
|
449 |
|
450 lemma (in order) antisymp_le[simp]: "antisymp (\<le>)" |
|
451 by (simp add: antisympI) |
|
452 |
|
453 lemma (in order) antisymp_ge[simp]: "antisymp (\<ge>)" |
|
454 by (simp add: antisympI) |
|
455 |
444 |
456 |
445 subsubsection \<open>Transitivity\<close> |
457 subsubsection \<open>Transitivity\<close> |
446 |
458 |
447 definition trans :: "'a rel \<Rightarrow> bool" |
459 definition trans :: "'a rel \<Rightarrow> bool" |
448 where "trans r \<longleftrightarrow> (\<forall>x y z. (x, y) \<in> r \<longrightarrow> (y, z) \<in> r \<longrightarrow> (x, z) \<in> r)" |
460 where "trans r \<longleftrightarrow> (\<forall>x y z. (x, y) \<in> r \<longrightarrow> (y, z) \<in> r \<longrightarrow> (x, z) \<in> r)" |