[STATEMENT]
lemma Red_F_subs_Red_F_diff_Red_F: "Red_F N \<subseteq> Red_F (N - Red_F N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Red_F N \<subseteq> Red_F (N - Red_F N)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Red_F N \<Longrightarrow> x \<in> Red_F (N - Red_F N)
[PROOF STEP]
fix C
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Red_F N \<Longrightarrow> x \<in> Red_F (N - Red_F N)
[PROOF STEP]
assume c_rf: "C \<in> Red_F N"
[PROOF STATE]
proof (state)
this:
C \<in> Red_F N

goal (1 subgoal):
 1. \<And>x. x \<in> Red_F N \<Longrightarrow> x \<in> Red_F (N - Red_F N)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C \<in> Red_F N
[PROOF STEP]
obtain CC :: "'f set" where
    cc_subs: "CC \<subseteq> N - Red_F N" and
    cc_fin: "finite CC" and
    cc_ent_c: "CC \<Turnstile> {C}" and
    cc_lt_c: "\<forall>C' \<in> CC. C' \<prec> C"
[PROOF STATE]
proof (prove)
using this:
C \<in> Red_F N

goal (1 subgoal):
 1. (\<And>CC. \<lbrakk>CC \<subseteq> N - Red_F N; finite CC; CC \<Turnstile> {C}; \<forall>C'\<in>CC. C' \<prec> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Red_F_imp_ex_non_Red_F[of C N]
[PROOF STATE]
proof (prove)
using this:
C \<in> Red_F N
C \<in> Red_F N \<Longrightarrow> \<exists>CC\<subseteq>N - Red_F N. finite CC \<and> CC \<Turnstile> {C} \<and> (\<forall>C'\<in>CC. C' \<prec> C)

goal (1 subgoal):
 1. (\<And>CC. \<lbrakk>CC \<subseteq> N - Red_F N; finite CC; CC \<Turnstile> {C}; \<forall>C'\<in>CC. C' \<prec> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
CC \<subseteq> N - Red_F N
finite CC
CC \<Turnstile> {C}
\<forall>C'\<in>CC. C' \<prec> C

goal (1 subgoal):
 1. \<And>x. x \<in> Red_F N \<Longrightarrow> x \<in> Red_F (N - Red_F N)
[PROOF STEP]
have "\<forall>D \<in> CC. D \<notin> Red_F N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>D\<in>CC. D \<notin> Red_F N
[PROOF STEP]
using cc_subs
[PROOF STATE]
proof (prove)
using this:
CC \<subseteq> N - Red_F N

goal (1 subgoal):
 1. \<forall>D\<in>CC. D \<notin> Red_F N
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<forall>D\<in>CC. D \<notin> Red_F N

goal (1 subgoal):
 1. \<And>x. x \<in> Red_F N \<Longrightarrow> x \<in> Red_F (N - Red_F N)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>D\<in>CC. D \<notin> Red_F N
[PROOF STEP]
have cc_nr:
    "\<forall>C \<in> CC. \<forall>DD \<subseteq> N. finite DD \<and> DD \<Turnstile> {C} \<longrightarrow> (\<exists>D \<in> DD. \<not> D \<prec> C)"
[PROOF STATE]
proof (prove)
using this:
\<forall>D\<in>CC. D \<notin> Red_F N

goal (1 subgoal):
 1. \<forall>C\<in>CC. \<forall>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<longrightarrow> (\<exists>D\<in>DD. \<not> D \<prec> C)
[PROOF STEP]
unfolding Red_F_def
[PROOF STATE]
proof (prove)
using this:
\<forall>D\<in>CC. D \<notin> {C. \<exists>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<and> (\<forall>D\<in>DD. D \<prec> C)}

goal (1 subgoal):
 1. \<forall>C\<in>CC. \<forall>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<longrightarrow> (\<exists>D\<in>DD. \<not> D \<prec> C)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>C\<in>CC. \<forall>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<longrightarrow> (\<exists>D\<in>DD. \<not> D \<prec> C)

goal (1 subgoal):
 1. \<And>x. x \<in> Red_F N \<Longrightarrow> x \<in> Red_F (N - Red_F N)
[PROOF STEP]
have "CC \<subseteq> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CC \<subseteq> N
[PROOF STEP]
using cc_subs
[PROOF STATE]
proof (prove)
using this:
CC \<subseteq> N - Red_F N

goal (1 subgoal):
 1. CC \<subseteq> N
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
CC \<subseteq> N

goal (1 subgoal):
 1. \<And>x. x \<in> Red_F N \<Longrightarrow> x \<in> Red_F (N - Red_F N)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
CC \<subseteq> N
[PROOF STEP]
have "CC \<subseteq> N - {C. \<exists>DD \<subseteq> N. finite DD \<and> DD \<Turnstile> {C} \<and> (\<forall>D \<in> DD. D \<prec> C)}"
[PROOF STATE]
proof (prove)
using this:
CC \<subseteq> N

goal (1 subgoal):
 1. CC \<subseteq> N - {C. \<exists>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<and> (\<forall>D\<in>DD. D \<prec> C)}
[PROOF STEP]
using cc_nr
[PROOF STATE]
proof (prove)
using this:
CC \<subseteq> N
\<forall>C\<in>CC. \<forall>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<longrightarrow> (\<exists>D\<in>DD. \<not> D \<prec> C)

goal (1 subgoal):
 1. CC \<subseteq> N - {C. \<exists>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<and> (\<forall>D\<in>DD. D \<prec> C)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
CC \<subseteq> N - {C. \<exists>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<and> (\<forall>D\<in>DD. D \<prec> C)}

goal (1 subgoal):
 1. \<And>x. x \<in> Red_F N \<Longrightarrow> x \<in> Red_F (N - Red_F N)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
CC \<subseteq> N - {C. \<exists>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<and> (\<forall>D\<in>DD. D \<prec> C)}
[PROOF STEP]
show "C \<in> Red_F (N - Red_F N)"
[PROOF STATE]
proof (prove)
using this:
CC \<subseteq> N - {C. \<exists>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<and> (\<forall>D\<in>DD. D \<prec> C)}

goal (1 subgoal):
 1. C \<in> Red_F (N - Red_F N)
[PROOF STEP]
using cc_fin cc_ent_c cc_lt_c
[PROOF STATE]
proof (prove)
using this:
CC \<subseteq> N - {C. \<exists>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<and> (\<forall>D\<in>DD. D \<prec> C)}
finite CC
CC \<Turnstile> {C}
\<forall>C'\<in>CC. C' \<prec> C

goal (1 subgoal):
 1. C \<in> Red_F (N - Red_F N)
[PROOF STEP]
unfolding Red_F_def
[PROOF STATE]
proof (prove)
using this:
CC \<subseteq> N - {C. \<exists>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<and> (\<forall>D\<in>DD. D \<prec> C)}
finite CC
CC \<Turnstile> {C}
\<forall>C'\<in>CC. C' \<prec> C

goal (1 subgoal):
 1. C \<in> {C. \<exists>DD\<subseteq>N - {C. \<exists>DD\<subseteq>N. finite DD \<and> DD \<Turnstile> {C} \<and> (\<forall>D\<in>DD. D \<prec> C)}. finite DD \<and> DD \<Turnstile> {C} \<and> (\<forall>D\<in>DD. D \<prec> C)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C \<in> Red_F (N - Red_F N)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Hermite_of_row_i_range_res:
  assumes ji: "j<i" and not_zero_i_A: "\<not> is_zero_row i A" and r: "res_function res"
  shows "Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> 0)
  \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> 0)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
let ?n="(LEAST n. A $ i $ n \<noteq> 0)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
define M where "M = mult_row A i (ass (A $ i $ ?n) div A $ i $ ?n)"
[PROOF STATE]
proof (state)
this:
M = mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b)))

goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
let ?R="row_add M j i ((res (M $ i $ ?n) (M $ j $ ?n)
    - M $ j $ ?n) div M $ i $ ?n)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
have Hii: "Hermite_of_row_i ass res A i $ i $ ?n = M $ i $ ?n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b)) = M $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))
[PROOF STEP]
unfolding M_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b)) = mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))
[PROOF STEP]
by (rule Hermite_of_row_i_works2[OF not_zero_i_A])
[PROOF STATE]
proof (state)
this:
Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b)) = M $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))

goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
have rw: "Hermite_of_row_i ass res A i $ j $ ?n = ?R $ j $ ?n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) = row_add M j i ((res (M $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) (M $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))) - M $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div M $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))
[PROOF STEP]
unfolding M_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) = row_add (mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b)))) j i ((res (mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) (mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))) - mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))
[PROOF STEP]
by (rule Hermite_of_row_i_works[OF ji not_zero_i_A])
[PROOF STATE]
proof (state)
this:
Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) = row_add M j i ((res (M $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) (M $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))) - M $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div M $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))

goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
have "\<forall>b ba. \<exists>bb. ba + bb * b = res b ba"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b ba. \<exists>bb. ba + bb * b = res b ba
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
res_function res

goal (1 subgoal):
 1. \<forall>b ba. \<exists>bb. ba + bb * b = res b ba
[PROOF STEP]
unfolding res_function_def
[PROOF STATE]
proof (prove)
using this:
\<forall>c. (\<forall>a b. cong a b c = (res c a = res c b)) \<and> pairwise (\<lambda>a b. \<not> cong a b c) (range (res c)) \<and> (\<forall>a. \<exists>k. res c a = a + k * c)

goal (1 subgoal):
 1. \<forall>b ba. \<exists>bb. ba + bb * b = res b ba
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>b ba. \<exists>bb. ba + bb * b = res b ba

goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>b ba. \<exists>bb. ba + bb * b = res b ba

goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
using rw
[PROOF STATE]
proof (prove)
using this:
\<forall>b ba. \<exists>bb. ba + bb * b = res b ba
Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) = row_add M j i ((res (M $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) (M $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))) - M $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div M $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))

goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
unfolding image_def Hii row_add_def
[PROOF STATE]
proof (prove)
using this:
\<forall>b ba. \<exists>bb. ba + bb * b = res b ba
Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) = (\<chi>ia ja. if ia = j then M $ j $ ja + (res (M $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) (M $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))) - M $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div M $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b)) * M $ i $ ja else M $ ia $ ja) $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))

goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> {y. \<exists>x\<in>UNIV. y = res (M $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) x}
[PROOF STEP]
by auto
      (metis (lifting) add_diff_cancel_left' nonzero_mult_div_cancel_left mult.commute mult_eq_0_iff)
[PROOF STATE]
proof (state)
this:
Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))

goal:
No subgoals!
[PROOF STEP]
qed


[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


[STATEMENT]
lemma direct_decompD:
  assumes "direct_decomp A ss"
  shows "qs \<in> listset ss \<Longrightarrow> sum_list qs \<in> A" and "inj_on sum_list (listset ss)"
    and "sum_list ` listset ss = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qs \<in> listset ss \<Longrightarrow> sum_list qs \<in> A) &&& inj_on sum_list (listset ss) &&& sum_list ` listset ss = A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
direct_decomp A ss

goal (1 subgoal):
 1. (qs \<in> listset ss \<Longrightarrow> sum_list qs \<in> A) &&& inj_on sum_list (listset ss) &&& sum_list ` listset ss = A
[PROOF STEP]
by (auto simp: direct_decomp_def bij_betw_def)


[STATEMENT]
lemma (in Ring) carr_dsum_prod:"carr_dsumag I M \<subseteq> carr_prodag I M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. carr_dsumag I M \<subseteq> carr_prodag I M
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> carr_dsumag I M \<Longrightarrow> x \<in> carr_prodag I M
[PROOF STEP]
apply (simp add:carr_dsumag_def finiteHom_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma local_flow_tank: "local_flow (f k) UNIV UNIV (\<phi> k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local_flow (f k) UNIV UNIV (\<phi> k)
[PROOF STEP]
apply (unfold_locales, unfold local_lipschitz_def lipschitz_on_def, simp_all, clarsimp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x t. \<exists>u>0. (\<exists>ta. dist t ta \<le> u) \<longrightarrow> (\<exists>L\<ge>0. \<forall>xa\<in>cball x u. \<forall>y\<in>cball x u. 0 \<le> L \<cdot> dist xa y)
 2. \<And>t s. \<forall>i. (i = 1 \<longrightarrow>  D (\<lambda>x. k \<cdot> x + s $ 1) = (\<lambda>x. k) on {0--t}) \<and> (i \<noteq> 1 \<longrightarrow> (i = 2 \<longrightarrow>  D (\<lambda>x. x + s $ 2) = (\<lambda>x. 1) on {0--t}) \<and> (i \<noteq> 2 \<longrightarrow>  D (\<lambda>x. s $ i) = (\<lambda>x. 0) on {0--t}))
 3. \<And>s. \<phi> k 0 s = s
[PROOF STEP]
apply(rule_tac x="1/2" in exI, clarsimp, rule_tac x=1 in exI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x t ta. dist t ta \<cdot> 2 \<le> 1 \<Longrightarrow> 0 \<le> 1 \<and> (\<forall>xa\<in>cball x (1 / 2). \<forall>y\<in>cball x (1 / 2). 0 \<le> 1 \<cdot> dist xa y)
 2. \<And>t s. \<forall>i. (i = 1 \<longrightarrow>  D (\<lambda>x. k \<cdot> x + s $ 1) = (\<lambda>x. k) on {0--t}) \<and> (i \<noteq> 1 \<longrightarrow> (i = 2 \<longrightarrow>  D (\<lambda>x. x + s $ 2) = (\<lambda>x. 1) on {0--t}) \<and> (i \<noteq> 2 \<longrightarrow>  D (\<lambda>x. s $ i) = (\<lambda>x. 0) on {0--t}))
 3. \<And>s. \<phi> k 0 s = s
[PROOF STEP]
apply(simp add: dist_norm norm_vec_def L2_set_def, unfold UNIV_4)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x t ta. \<bar>t - ta\<bar> \<cdot> 2 \<le> 1 \<Longrightarrow> \<forall>xa\<in>cball x (1 / 2). \<forall>y\<in>cball x (1 / 2). 0 \<le> (\<Sum>i\<in>insert 1 (insert 2 (insert 3 (\<eta> 4))). (xa $ i - y $ i)\<^sup>2)
 2. \<And>t s. \<forall>i. (i = 1 \<longrightarrow>  D (\<lambda>x. k \<cdot> x + s $ 1) = (\<lambda>x. k) on {0--t}) \<and> (i \<noteq> 1 \<longrightarrow> (i = 2 \<longrightarrow>  D (\<lambda>x. x + s $ 2) = (\<lambda>x. 1) on {0--t}) \<and> (i \<noteq> 2 \<longrightarrow>  D (\<lambda>x. s $ i) = (\<lambda>x. 0) on {0--t}))
 3. \<And>s. \<phi> k 0 s = s
[PROOF STEP]
by (auto intro!: poly_derivatives simp: vec_eq_iff)


[STATEMENT]
lemma psubst_eq_subst:
  assumes "\<phi> \<in> fmla" "x \<in> var" and "t \<in> trm"
  shows "psubst \<phi> [(t,x)] = subst \<phi> t x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. psubst \<phi> [(t, x)] = subst \<phi> t x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. psubst \<phi> [(t, x)] = subst \<phi> t x
[PROOF STEP]
have "psubst \<phi> [(t,x)] = rawpsubst \<phi> [(t,x)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. psubst \<phi> [(t, x)] = rawpsubst \<phi> [(t, x)]
[PROOF STEP]
apply(rule psubst_eq_rawpsubst)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<phi> \<in> fmla
 2. snd ` set [(t, x)] \<subseteq> var
 3. fst ` set [(t, x)] \<subseteq> trm
 4. distinct (map snd [(t, x)])
 5. \<And>i j. \<lbrakk>i < j; j < length [(t, x)]\<rbrakk> \<Longrightarrow> snd ([(t, x)] ! j) \<notin> FvarsT (fst ([(t, x)] ! i))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
x \<in> var
t \<in> trm

goal (5 subgoals):
 1. \<phi> \<in> fmla
 2. snd ` set [(t, x)] \<subseteq> var
 3. fst ` set [(t, x)] \<subseteq> trm
 4. distinct (map snd [(t, x)])
 5. \<And>i j. \<lbrakk>i < j; j < length [(t, x)]\<rbrakk> \<Longrightarrow> snd ([(t, x)] ! j) \<notin> FvarsT (fst ([(t, x)] ! i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
psubst \<phi> [(t, x)] = rawpsubst \<phi> [(t, x)]

goal (1 subgoal):
 1. psubst \<phi> [(t, x)] = subst \<phi> t x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
psubst \<phi> [(t, x)] = rawpsubst \<phi> [(t, x)]

goal (1 subgoal):
 1. psubst \<phi> [(t, x)] = subst \<phi> t x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
psubst \<phi> [(t, x)] = subst \<phi> t x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subst_all_num[simp]:
  assumes "\<phi> \<in> fmla" "x \<in> var" "y \<in> var" "n \<in> num"
  shows "x \<noteq> y \<Longrightarrow> subst (all x \<phi>) n y = all x (subst \<phi> n y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> subst (all x \<phi>) n y = all x (subst \<phi> n y)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
x \<in> var
y \<in> var
n \<in> num

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> subst (all x \<phi>) n y = all x (subst \<phi> n y)
[PROOF STEP]
by simp