equal
deleted
inserted
replaced
318 lemma irrefl_on_distinct [code]: "irrefl_on A r \<longleftrightarrow> (\<forall>(a, b) \<in> r. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<noteq> b)" |
318 lemma irrefl_on_distinct [code]: "irrefl_on A r \<longleftrightarrow> (\<forall>(a, b) \<in> r. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<noteq> b)" |
319 by (auto simp add: irrefl_on_def) |
319 by (auto simp add: irrefl_on_def) |
320 |
320 |
321 lemmas irrefl_distinct = irrefl_on_distinct \<comment> \<open>For backward compatibility\<close> |
321 lemmas irrefl_distinct = irrefl_on_distinct \<comment> \<open>For backward compatibility\<close> |
322 |
322 |
|
323 lemma irrefl_on_subset: "irrefl_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> irrefl_on B r" |
|
324 by (auto simp: irrefl_on_def) |
|
325 |
|
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) |
|
328 |
323 lemma (in preorder) irreflp_less[simp]: "irreflp (<)" |
329 lemma (in preorder) irreflp_less[simp]: "irreflp (<)" |
324 by (simp add: irreflpI) |
330 by (simp add: irreflpI) |
325 |
331 |
326 lemma (in preorder) irreflp_greater[simp]: "irreflp (>)" |
332 lemma (in preorder) irreflp_greater[simp]: "irreflp (>)" |
327 by (simp add: irreflpI) |
333 by (simp add: irreflpI) |