[STATEMENT]
lemma plus_eq_Err_conv [simp]:
  assumes "x\<in>A"  "y\<in>A"  "semilat(err A, Err.le r, lift2 f)"
  shows "(x \<squnion>\<^sub>f y = Err) = (\<not>(\<exists>z\<in>A. x \<sqsubseteq>\<^sub>r z \<and> y \<sqsubseteq>\<^sub>r z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<squnion>\<^bsub>f\<^esub> y = Err) = (\<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<squnion>\<^bsub>f\<^esub> y = Err) = (\<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x \<squnion>\<^bsub>f\<^esub> y = Err) = (\<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z))
[PROOF STEP]
have plus_le_conv2:
    "\<And>r f z. \<lbrakk> z \<in> err A; semilat (err A, r, f); OK x \<in> err A; OK y \<in> err A;
                 OK x \<squnion>\<^sub>f OK y \<sqsubseteq>\<^sub>r z\<rbrakk> \<Longrightarrow> OK x \<sqsubseteq>\<^sub>r z \<and> OK y \<sqsubseteq>\<^sub>r z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r f z. \<lbrakk>z \<in> err A; semilat (err A, r, f); OK x \<in> err A; OK y \<in> err A; OK x \<squnion>\<^bsub>f\<^esub> OK y \<sqsubseteq>\<^bsub>r\<^esub> z\<rbrakk> \<Longrightarrow> OK x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> OK y \<sqsubseteq>\<^bsub>r\<^esub> z
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r f z. \<lbrakk>z \<in> err A; semilat (err A, r, f); OK x \<in> err A; OK y \<in> err A; OK x \<squnion>\<^bsub>f\<^esub> OK y \<sqsubseteq>\<^bsub>r\<^esub> z\<rbrakk> \<Longrightarrow> OK x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> OK y \<sqsubseteq>\<^bsub>r\<^esub> z
[PROOF STEP]
by (rule Semilat.plus_le_conv [OF Semilat.intro, THEN iffD1])
[PROOF STATE]
proof (state)
this:
\<lbrakk>?z \<in> err A; semilat (err A, ?r, ?f); OK x \<in> err A; OK y \<in> err A; OK x \<squnion>\<^bsub>?f\<^esub> OK y \<sqsubseteq>\<^bsub>?r\<^esub> ?z\<rbrakk> \<Longrightarrow> OK x \<sqsubseteq>\<^bsub>?r\<^esub> ?z \<and> OK y \<sqsubseteq>\<^bsub>?r\<^esub> ?z

goal (1 subgoal):
 1. (x \<squnion>\<^bsub>f\<^esub> y = Err) = (\<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z))
[PROOF STEP]
(*>*)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?z \<in> err A; semilat (err A, ?r, ?f); OK x \<in> err A; OK y \<in> err A; OK x \<squnion>\<^bsub>?f\<^esub> OK y \<sqsubseteq>\<^bsub>?r\<^esub> ?z\<rbrakk> \<Longrightarrow> OK x \<sqsubseteq>\<^bsub>?r\<^esub> ?z \<and> OK y \<sqsubseteq>\<^bsub>?r\<^esub> ?z

goal (1 subgoal):
 1. (x \<squnion>\<^bsub>f\<^esub> y = Err) = (\<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
y \<in> A
semilat (err A, Err.le r, lift2 f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> A
y \<in> A
semilat (err A, Err.le r, lift2 f)

goal (1 subgoal):
 1. (x \<squnion>\<^bsub>f\<^esub> y = Err) = (\<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z))
[PROOF STEP]
apply (rule_tac iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); x \<squnion>\<^bsub>f\<^esub> y = Err\<rbrakk> \<Longrightarrow> \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)
 2. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> z; y \<sqsubseteq>\<^bsub>r\<^esub> z\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply (drule OK_le_err_OK [THEN iffD2])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; y \<sqsubseteq>\<^bsub>r\<^esub> z; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply (drule OK_le_err_OK [THEN iffD2])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply (drule Semilat.lub[OF Semilat.intro, of _ _ _ "OK x" _ "OK y"])
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> ?z13 z
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> ?z13 z
 3. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK x \<in> err A
 4. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK y \<in> err A
 5. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> ?z13 z \<in> err A
 6. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK x \<squnion>\<^bsub>lift2 f\<^esub> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> ?z13 z\<rbrakk> \<Longrightarrow> False
 7. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK x \<in> err A
 3. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK y \<in> err A
 4. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
 5. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK x \<squnion>\<^bsub>lift2 f\<^esub> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> False
 6. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK x \<in> err A
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK y \<in> err A
 3. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
 4. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK x \<squnion>\<^bsub>lift2 f\<^esub> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> False
 5. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK y \<in> err A
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
 3. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK x \<squnion>\<^bsub>lift2 f\<^esub> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK x \<squnion>\<^bsub>lift2 f\<^esub> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = Err; z \<in> A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z; OK x \<squnion>\<^bsub>lift2 f\<^esub> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply (case_tac "x \<squnion>\<^sub>f y")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = Err\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
 2. \<And>x2. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK x2\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK x2\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply (rename_tac "z")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
[PROOF STEP]
apply (subgoal_tac "OK z: err A")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
[PROOF STEP]
apply (frule plus_le_conv2)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A\<rbrakk> \<Longrightarrow> semilat (err A, ?r22 z, ?f22 z)
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A\<rbrakk> \<Longrightarrow> OK x \<in> err A
 3. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A\<rbrakk> \<Longrightarrow> OK y \<in> err A
 4. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A\<rbrakk> \<Longrightarrow> OK x \<squnion>\<^bsub>?f22 z\<^esub> OK y \<sqsubseteq>\<^bsub>?r22 z\<^esub> OK z
 5. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A; OK x \<sqsubseteq>\<^bsub>?r22 z\<^esub> OK z \<and> OK y \<sqsubseteq>\<^bsub>?r22 z\<^esub> OK z\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
 6. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A\<rbrakk> \<Longrightarrow> OK x \<in> err A
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A\<rbrakk> \<Longrightarrow> OK y \<in> err A
 3. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A\<rbrakk> \<Longrightarrow> OK x \<squnion>\<^bsub>lift2 f\<^esub> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z
 4. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z \<and> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
 5. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A\<rbrakk> \<Longrightarrow> OK y \<in> err A
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A\<rbrakk> \<Longrightarrow> OK x \<squnion>\<^bsub>lift2 f\<^esub> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z
 3. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z \<and> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
 4. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A\<rbrakk> \<Longrightarrow> OK x \<squnion>\<^bsub>lift2 f\<^esub> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z \<and> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
 3. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<forall>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<longrightarrow> \<not> y \<sqsubseteq>\<^bsub>r\<^esub> z; x \<squnion>\<^bsub>f\<^esub> y = OK z; z \<in> A\<rbrakk> \<Longrightarrow> z \<sqsubseteq>\<^bsub>r\<^esub> z
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z \<and> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
 3. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
[PROOF STEP]
apply (blast dest: Semilat.orderI [OF Semilat.intro] order_refl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z; OK z \<in> err A; OK x \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z \<and> OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> OK z\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y = Err
 2. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z); x \<squnion>\<^bsub>f\<^esub> y = OK z\<rbrakk> \<Longrightarrow> OK z \<in> err A
[PROOF STEP]
apply (erule subst)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; semilat (err A, Err.le r, lift2 f); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y \<in> err A
[PROOF STEP]
apply (unfold semilat_def err_def' closed_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>x \<in> A; y \<in> A; case (insert Err {x. \<exists>y\<in>A. x = OK y}, Err.le r, lift2 f) of (A, r, f) \<Rightarrow> order r \<and> (\<forall>x\<in>A. \<forall>y\<in>A. x \<squnion>\<^bsub>f\<^esub> y \<in> A) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> x \<squnion>\<^bsub>f\<^esub> y) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. y \<sqsubseteq>\<^bsub>r\<^esub> x \<squnion>\<^bsub>f\<^esub> y) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z \<longrightarrow> x \<squnion>\<^bsub>f\<^esub> y \<sqsubseteq>\<^bsub>r\<^esub> z); \<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z)\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y \<in> insert Err {x. \<exists>y\<in>A. x = OK y}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(x \<squnion>\<^bsub>f\<^esub> y = Err) = (\<not> (\<exists>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z))

goal:
No subgoals!
[PROOF STEP]
qed