255 apply (unfold order_def) |
255 apply (unfold order_def) |
256 apply blast |
256 apply blast |
257 done |
257 done |
258 |
258 |
259 lemma OK_plus_OK_eq_Err_conv [simp]: |
259 lemma OK_plus_OK_eq_Err_conv [simp]: |
260 "\<lbrakk> x:A; y:A; semilat(err A, le r, fe) \<rbrakk> \<Longrightarrow> |
260 assumes "x:A" and "y:A" and "semilat(err A, le r, fe)" |
261 ((OK x) +_fe (OK y) = Err) = (~(? z:A. x <=_r z & y <=_r z))" |
261 shows "((OK x) +_fe (OK y) = Err) = (~(? z:A. x <=_r z & y <=_r z))" |
262 proof - |
262 proof - |
263 have plus_le_conv3: "\<And>A x y z f r. |
263 have plus_le_conv3: "\<And>A x y z f r. |
264 \<lbrakk> semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A \<rbrakk> |
264 \<lbrakk> semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A \<rbrakk> |
265 \<Longrightarrow> x <=_r z \<and> y <=_r z" |
265 \<Longrightarrow> x <=_r z \<and> y <=_r z" |
266 by (rule semilat.plus_le_conv [THEN iffD1]) |
266 by (rule semilat.plus_le_conv [THEN iffD1]) |
267 case rule_context |
267 from prems show ?thesis |
268 thus ?thesis |
|
269 apply (rule_tac iffI) |
268 apply (rule_tac iffI) |
270 apply clarify |
269 apply clarify |
271 apply (drule OK_le_err_OK [THEN iffD2]) |
270 apply (drule OK_le_err_OK [THEN iffD2]) |
272 apply (drule OK_le_err_OK [THEN iffD2]) |
271 apply (drule OK_le_err_OK [THEN iffD2]) |
273 apply (drule semilat.lub[of _ _ _ "OK x" _ "OK y"]) |
272 apply (drule semilat.lub[of _ _ _ "OK x" _ "OK y"]) |