equal
deleted
inserted
replaced
244 |
244 |
245 lemma refl_on_def' [nitpick_unfold, code]: |
245 lemma refl_on_def' [nitpick_unfold, code]: |
246 "refl_on A r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<in> A \<and> y \<in> A) \<and> (\<forall>x \<in> A. (x, x) \<in> r)" |
246 "refl_on A r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<in> A \<and> y \<in> A) \<and> (\<forall>x \<in> A. (x, x) \<in> r)" |
247 by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2) |
247 by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2) |
248 |
248 |
249 lemma reflp_equality [simp]: "reflp (=)" |
249 lemma reflp_on_equality [simp]: "reflp_on A (=)" |
250 by (simp add: reflp_def) |
250 by (simp add: reflp_on_def) |
251 |
251 |
252 lemma reflp_on_mono: |
252 lemma reflp_on_mono: |
253 "reflp_on A R \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> Q x y) \<Longrightarrow> reflp_on A Q" |
253 "reflp_on A R \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> Q x y) \<Longrightarrow> reflp_on A Q" |
254 by (auto intro: reflp_onI dest: reflp_onD) |
254 by (auto intro: reflp_onI dest: reflp_onD) |
255 |
255 |