259 by (auto intro!: asymI asympI elim: asym.cases asymp.cases simp add: irreflp_irrefl_eq) |
259 by (auto intro!: asymI asympI elim: asym.cases asymp.cases simp add: irreflp_irrefl_eq) |
260 |
260 |
261 lemma asymD: "\<lbrakk>asym R; (x,y) \<in> R\<rbrakk> \<Longrightarrow> (y,x) \<notin> R" |
261 lemma asymD: "\<lbrakk>asym R; (x,y) \<in> R\<rbrakk> \<Longrightarrow> (y,x) \<notin> R" |
262 by (simp add: asym.simps) |
262 by (simp add: asym.simps) |
263 |
263 |
|
264 lemma asympD: "asymp R \<Longrightarrow> R x y \<Longrightarrow> \<not> R y x" |
|
265 by (rule asymD[to_pred]) |
|
266 |
264 lemma asym_iff: "asym R \<longleftrightarrow> (\<forall>x y. (x,y) \<in> R \<longrightarrow> (y,x) \<notin> R)" |
267 lemma asym_iff: "asym R \<longleftrightarrow> (\<forall>x y. (x,y) \<in> R \<longrightarrow> (y,x) \<notin> R)" |
265 by (blast intro: asymI dest: asymD) |
268 by (blast intro: asymI dest: asymD) |
266 |
269 |
267 context preorder begin |
270 lemma (in preorder) asymp_less[simp]: "asymp (<)" |
268 |
|
269 lemma asymp_less[simp]: "asymp (<)" |
|
270 by (auto intro: asympI dual_order.asym) |
271 by (auto intro: asympI dual_order.asym) |
271 |
272 |
272 lemma asymp_greater[simp]: "asymp (>)" |
273 lemma (in preorder) asymp_greater[simp]: "asymp (>)" |
273 by (auto intro: asympI dual_order.asym) |
274 by (auto intro: asympI dual_order.asym) |
274 |
|
275 end |
|
276 |
275 |
277 |
276 |
278 subsubsection \<open>Symmetry\<close> |
277 subsubsection \<open>Symmetry\<close> |
279 |
278 |
280 definition sym :: "'a rel \<Rightarrow> bool" |
279 definition sym :: "'a rel \<Rightarrow> bool" |