equal
deleted
inserted
replaced
171 lemma reflpE: |
171 lemma reflpE: |
172 assumes "reflp r" |
172 assumes "reflp r" |
173 obtains "r x x" |
173 obtains "r x x" |
174 using assms by (auto dest: refl_onD simp add: reflp_def) |
174 using assms by (auto dest: refl_onD simp add: reflp_def) |
175 |
175 |
|
176 lemma reflpD: |
|
177 assumes "reflp r" |
|
178 shows "r x x" |
|
179 using assms by (auto elim: reflpE) |
|
180 |
176 lemma refl_on_Int: "refl_on A r ==> refl_on B s ==> refl_on (A \<inter> B) (r \<inter> s)" |
181 lemma refl_on_Int: "refl_on A r ==> refl_on B s ==> refl_on (A \<inter> B) (r \<inter> s)" |
177 by (unfold refl_on_def) blast |
182 by (unfold refl_on_def) blast |
178 |
183 |
179 lemma reflp_inf: |
184 lemma reflp_inf: |
180 "reflp r \<Longrightarrow> reflp s \<Longrightarrow> reflp (r \<sqinter> s)" |
185 "reflp r \<Longrightarrow> reflp s \<Longrightarrow> reflp (r \<sqinter> s)" |