equal
deleted
inserted
replaced
324 by (auto simp: irrefl_on_def) |
324 by (auto simp: irrefl_on_def) |
325 |
325 |
326 lemma irreflp_on_subset: "irreflp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> irreflp_on B R" |
326 lemma irreflp_on_subset: "irreflp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> irreflp_on B R" |
327 by (auto simp: irreflp_on_def) |
327 by (auto simp: irreflp_on_def) |
328 |
328 |
329 lemma (in preorder) irreflp_less[simp]: "irreflp (<)" |
329 lemma (in preorder) irreflp_on_less[simp]: "irreflp_on A (<)" |
330 by (simp add: irreflpI) |
330 by (simp add: irreflp_onI) |
331 |
331 |
332 lemma (in preorder) irreflp_greater[simp]: "irreflp (>)" |
332 lemma (in preorder) irreflp_on_greater[simp]: "irreflp_on A (>)" |
333 by (simp add: irreflpI) |
333 by (simp add: irreflp_onI) |
334 |
334 |
335 subsubsection \<open>Asymmetry\<close> |
335 subsubsection \<open>Asymmetry\<close> |
336 |
336 |
337 inductive asym :: "'a rel \<Rightarrow> bool" |
337 inductive asym :: "'a rel \<Rightarrow> bool" |
338 where asymI: "(\<And>a b. (a, b) \<in> R \<Longrightarrow> (b, a) \<notin> R) \<Longrightarrow> asym R" |
338 where asymI: "(\<And>a b. (a, b) \<in> R \<Longrightarrow> (b, a) \<notin> R) \<Longrightarrow> asym R" |