equal
deleted
inserted
replaced
153 (*<*) by (blast intro: ub1 ub2 lub order_trans) (*>*) |
153 (*<*) by (blast intro: ub1 ub2 lub order_trans) (*>*) |
154 |
154 |
155 lemma (in Semilat) le_iff_plus_unchanged: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^sub>r y) = (x \<squnion>\<^sub>f y = y)" |
155 lemma (in Semilat) le_iff_plus_unchanged: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^sub>r y) = (x \<squnion>\<^sub>f y = y)" |
156 (*<*) |
156 (*<*) |
157 apply (rule iffI) |
157 apply (rule iffI) |
158 apply (blast intro: antisym_r refl_r lub ub2) |
158 apply (blast intro: antisym_r lub ub2) |
159 apply (erule subst) |
159 apply (erule subst) |
160 apply simp |
160 apply simp |
161 done |
161 done |
162 (*>*) |
162 (*>*) |
163 |
163 |
164 lemma (in Semilat) le_iff_plus_unchanged2: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^sub>r y) = (y \<squnion>\<^sub>f x = y)" |
164 lemma (in Semilat) le_iff_plus_unchanged2: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^sub>r y) = (y \<squnion>\<^sub>f x = y)" |
165 (*<*) |
165 (*<*) |
166 apply (rule iffI) |
166 apply (rule iffI) |
167 apply (blast intro: order_antisym lub order_refl ub1) |
167 apply (blast intro: order_antisym lub ub1) |
168 apply (erule subst) |
168 apply (erule subst) |
169 apply simp |
169 apply simp |
170 done |
170 done |
171 (*>*) |
171 (*>*) |
172 |
172 |