[STATEMENT]
lemma prod_in_span[intro!]:
  assumes "b \<in> carrier_vec n" "S \<subseteq> carrier_vec n" "a = 0 \<or> b \<in> span S"
  shows "a \<cdot>\<^sub>v b \<in> span S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<cdot>\<^sub>v b \<in> local.span S
[PROOF STEP]
proof(cases "a = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = (0::'a) \<Longrightarrow> a \<cdot>\<^sub>v b \<in> local.span S
 2. a \<noteq> (0::'a) \<Longrightarrow> a \<cdot>\<^sub>v b \<in> local.span S
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a = (0::'a)

goal (2 subgoals):
 1. a = (0::'a) \<Longrightarrow> a \<cdot>\<^sub>v b \<in> local.span S
 2. a \<noteq> (0::'a) \<Longrightarrow> a \<cdot>\<^sub>v b \<in> local.span S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = (0::'a)

goal (1 subgoal):
 1. a \<cdot>\<^sub>v b \<in> local.span S
[PROOF STEP]
by (auto simp:lmult_0[OF assms(1)] span_zero)
[PROOF STATE]
proof (state)
this:
a \<cdot>\<^sub>v b \<in> local.span S

goal (1 subgoal):
 1. a \<noteq> (0::'a) \<Longrightarrow> a \<cdot>\<^sub>v b \<in> local.span S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<noteq> (0::'a) \<Longrightarrow> a \<cdot>\<^sub>v b \<in> local.span S
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<noteq> (0::'a)

goal (1 subgoal):
 1. a \<noteq> (0::'a) \<Longrightarrow> a \<cdot>\<^sub>v b \<in> local.span S
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
b \<in> carrier_vec n
S \<subseteq> carrier_vec n
a = (0::'a) \<or> b \<in> local.span S
a \<noteq> (0::'a)
[PROOF STEP]
have "b \<in> span S"
[PROOF STATE]
proof (prove)
using this:
b \<in> carrier_vec n
S \<subseteq> carrier_vec n
a = (0::'a) \<or> b \<in> local.span S
a \<noteq> (0::'a)

goal (1 subgoal):
 1. b \<in> local.span S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in> local.span S

goal (1 subgoal):
 1. a \<noteq> (0::'a) \<Longrightarrow> a \<cdot>\<^sub>v b \<in> local.span S
[PROOF STEP]
from this[THEN in_spanE]
[PROOF STATE]
proof (chain)
picking this:
\<exists>a A. b = lincomb a A \<and> finite A \<and> A \<subseteq> S
[PROOF STEP]
obtain aa A where a[intro!]: "b = lincomb aa A" "finite A" "A \<subseteq> S"
[PROOF STATE]
proof (prove)
using this:
\<exists>a A. b = lincomb a A \<and> finite A \<and> A \<subseteq> S

goal (1 subgoal):
 1. (\<And>aa A. \<lbrakk>b = lincomb aa A; finite A; A \<subseteq> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b = lincomb aa A
finite A
A \<subseteq> S

goal (1 subgoal):
 1. a \<noteq> (0::'a) \<Longrightarrow> a \<cdot>\<^sub>v b \<in> local.span S
[PROOF STEP]
hence [intro!]:"(\<lambda>v. aa v \<cdot>\<^sub>v v) \<in> A \<rightarrow> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
b = lincomb aa A
finite A
A \<subseteq> S

goal (1 subgoal):
 1. (\<lambda>v. aa v \<cdot>\<^sub>v v) \<in> A \<rightarrow> carrier_vec n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
b = lincomb aa A
finite A
A \<subseteq> S
b \<in> carrier_vec n
S \<subseteq> carrier_vec n
a = (0::'a) \<or> b \<in> local.span S

goal (1 subgoal):
 1. (\<lambda>v. aa v \<cdot>\<^sub>v v) \<in> A \<rightarrow> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>v. aa v \<cdot>\<^sub>v v) \<in> A \<rightarrow> carrier_vec n

goal (1 subgoal):
 1. a \<noteq> (0::'a) \<Longrightarrow> a \<cdot>\<^sub>v b \<in> local.span S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<cdot>\<^sub>v b \<in> local.span S
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. a \<cdot>\<^sub>v b = lincomb ?a ?A
 2. finite ?A
 3. ?A \<subseteq> S
[PROOF STEP]
show "a \<cdot>\<^sub>v b = lincomb (\<lambda> v. a * aa v) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<cdot>\<^sub>v b = lincomb (\<lambda>v. a * aa v) A
[PROOF STEP]
using a(1)
[PROOF STATE]
proof (prove)
using this:
b = lincomb aa A

goal (1 subgoal):
 1. a \<cdot>\<^sub>v b = lincomb (\<lambda>v. a * aa v) A
[PROOF STEP]
unfolding lincomb_def smult_smult_assoc[symmetric]
[PROOF STATE]
proof (prove)
using this:
b = (\<Oplus>\<^bsub>V\<^esub>v\<in>A. aa v \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. a \<cdot>\<^sub>v b = (\<Oplus>\<^bsub>V\<^esub>v\<in>A. a \<cdot>\<^sub>v (aa v \<cdot>\<^sub>v v))
[PROOF STEP]
by(subst finsum_smult[symmetric]) force+
[PROOF STATE]
proof (state)
this:
a \<cdot>\<^sub>v b = lincomb (\<lambda>v. a * aa v) A

goal (2 subgoals):
 1. finite A
 2. A \<subseteq> S
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
a \<cdot>\<^sub>v b \<in> local.span S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma det_nonzero_congruence:
  assumes eq:"A * M = B * M" and det:"det (M::'a mat) \<noteq> 0"
  and M: "M \<in> carrier_mat n n" and carr:"A \<in> carrier_mat n n" "B \<in> carrier_mat n n"
  shows "A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A = B
[PROOF STEP]
have "1\<^sub>m n \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1\<^sub>m n \<in> carrier_mat n n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1\<^sub>m n \<in> carrier_mat n n

goal (1 subgoal):
 1. A = B
[PROOF STEP]
from det_non_zero_imp_unit[OF M det] gauss_jordan_check_invertable[OF M this]
[PROOF STATE]
proof (chain)
picking this:
M \<in> Units (ring_mat TYPE('a) n ?b)
(M \<in> Units (ring_mat TYPE('a) n ?b)) = (fst (gauss_jordan M (1\<^sub>m n)) = 1\<^sub>m n)
[PROOF STEP]
have gj_fst:"(fst (gauss_jordan M (1\<^sub>m n)) = 1\<^sub>m n)"
[PROOF STATE]
proof (prove)
using this:
M \<in> Units (ring_mat TYPE('a) n ?b)
(M \<in> Units (ring_mat TYPE('a) n ?b)) = (fst (gauss_jordan M (1\<^sub>m n)) = 1\<^sub>m n)

goal (1 subgoal):
 1. fst (gauss_jordan M (1\<^sub>m n)) = 1\<^sub>m n
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
fst (gauss_jordan M (1\<^sub>m n)) = 1\<^sub>m n

goal (1 subgoal):
 1. A = B
[PROOF STEP]
define Mi where "Mi = snd (gauss_jordan M (1\<^sub>m n))"
[PROOF STATE]
proof (state)
this:
Mi = snd (gauss_jordan M (1\<^sub>m n))

goal (1 subgoal):
 1. A = B
[PROOF STEP]
with gj_fst
[PROOF STATE]
proof (chain)
picking this:
fst (gauss_jordan M (1\<^sub>m n)) = 1\<^sub>m n
Mi = snd (gauss_jordan M (1\<^sub>m n))
[PROOF STEP]
have gj:"gauss_jordan M (1\<^sub>m n) = (1\<^sub>m n, Mi)"
[PROOF STATE]
proof (prove)
using this:
fst (gauss_jordan M (1\<^sub>m n)) = 1\<^sub>m n
Mi = snd (gauss_jordan M (1\<^sub>m n))

goal (1 subgoal):
 1. gauss_jordan M (1\<^sub>m n) = (1\<^sub>m n, Mi)
[PROOF STEP]
unfolding fst_def snd_def
[PROOF STATE]
proof (prove)
using this:
(case gauss_jordan M (1\<^sub>m n) of (x1, x2) \<Rightarrow> x1) = 1\<^sub>m n
Mi = (case gauss_jordan M (1\<^sub>m n) of (x1, x2) \<Rightarrow> x2)

goal (1 subgoal):
 1. gauss_jordan M (1\<^sub>m n) = (1\<^sub>m n, Mi)
[PROOF STEP]
by (auto split:prod.split)
[PROOF STATE]
proof (state)
this:
gauss_jordan M (1\<^sub>m n) = (1\<^sub>m n, Mi)

goal (1 subgoal):
 1. A = B
[PROOF STEP]
from gauss_jordan_compute_inverse(1,3)[OF M gj]
[PROOF STATE]
proof (chain)
picking this:
M * Mi = 1\<^sub>m n
Mi \<in> carrier_mat n n
[PROOF STEP]
have Mi: "Mi \<in> carrier_mat n n" and is1:"M * Mi = 1\<^sub>m n"
[PROOF STATE]
proof (prove)
using this:
M * Mi = 1\<^sub>m n
Mi \<in> carrier_mat n n

goal (1 subgoal):
 1. Mi \<in> carrier_mat n n &&& M * Mi = 1\<^sub>m n
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
Mi \<in> carrier_mat n n
M * Mi = 1\<^sub>m n

goal (1 subgoal):
 1. A = B
[PROOF STEP]
from arg_cong[OF eq, of "\<lambda> M. M * Mi"]
[PROOF STATE]
proof (chain)
picking this:
A * M * Mi = B * M * Mi
[PROOF STEP]
show "A = B"
[PROOF STATE]
proof (prove)
using this:
A * M * Mi = B * M * Mi

goal (1 subgoal):
 1. A = B
[PROOF STEP]
unfolding carr[THEN assoc_mult_mat[OF _ M Mi]] is1 carr[THEN right_mult_one_mat]
[PROOF STATE]
proof (prove)
using this:
A = B

goal (1 subgoal):
 1. A = B
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A = B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mat_of_rows_mult_as_finsum:
  assumes "v \<in> carrier_vec (length lst)" "\<And> i. i < length lst \<Longrightarrow> lst ! i \<in> carrier_vec n"
  defines "f l \<equiv> sum (\<lambda> i. if l = lst ! i then v $ i else 0) {0..<length lst}"
  shows mat_of_cols_mult_as_finsum:"mat_of_cols n lst *\<^sub>v v = lincomb f (set lst)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cols n lst *\<^sub>v v = lincomb f (set lst)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat_of_cols n lst *\<^sub>v v = lincomb f (set lst)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
v \<in> carrier_vec (length lst)
?i1 < length lst \<Longrightarrow> lst ! ?i1 \<in> carrier_vec n
f ?l1 \<equiv> \<Sum>i = 0..<length lst. if ?l1 = lst ! i then v $ i else (0::'a)
[PROOF STEP]
have "\<forall> i < length lst. lst ! i \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec (length lst)
?i1 < length lst \<Longrightarrow> lst ! ?i1 \<in> carrier_vec n
f ?l1 \<equiv> \<Sum>i = 0..<length lst. if ?l1 = lst ! i then v $ i else (0::'a)

goal (1 subgoal):
 1. \<forall>i<length lst. lst ! i \<in> carrier_vec n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i<length lst. lst ! i \<in> carrier_vec n

goal (1 subgoal):
 1. mat_of_cols n lst *\<^sub>v v = lincomb f (set lst)
[PROOF STEP]
note an = all_nth_imp_all_set[OF this]
[PROOF STATE]
proof (state)
this:
?x \<in> set lst \<Longrightarrow> ?x \<in> carrier_vec n

goal (1 subgoal):
 1. mat_of_cols n lst *\<^sub>v v = lincomb f (set lst)
[PROOF STEP]
hence slc:"set lst \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
?x \<in> set lst \<Longrightarrow> ?x \<in> carrier_vec n

goal (1 subgoal):
 1. set lst \<subseteq> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set lst \<subseteq> carrier_vec n

goal (1 subgoal):
 1. mat_of_cols n lst *\<^sub>v v = lincomb f (set lst)
[PROOF STEP]
hence dn [simp]:"\<And> x. x \<in> set lst \<Longrightarrow> dim_vec x = n"
[PROOF STATE]
proof (prove)
using this:
set lst \<subseteq> carrier_vec n

goal (1 subgoal):
 1. \<And>x. x \<in> set lst \<Longrightarrow> dim_vec x = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x1 \<in> set lst \<Longrightarrow> dim_vec ?x1 = n

goal (1 subgoal):
 1. mat_of_cols n lst *\<^sub>v v = lincomb f (set lst)
[PROOF STEP]
have dl [simp]:"dim_vec (lincomb f (set lst)) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (lincomb f (set lst)) = n
[PROOF STEP]
using an
[PROOF STATE]
proof (prove)
using this:
?x \<in> set lst \<Longrightarrow> ?x \<in> carrier_vec n

goal (1 subgoal):
 1. dim_vec (lincomb f (set lst)) = n
[PROOF STEP]
by (intro lincomb_dim,auto)
[PROOF STATE]
proof (state)
this:
dim_vec (lincomb f (set lst)) = n

goal (1 subgoal):
 1. mat_of_cols n lst *\<^sub>v v = lincomb f (set lst)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cols n lst *\<^sub>v v = lincomb f (set lst)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i < dim_vec (lincomb f (set lst)) \<Longrightarrow> (mat_of_cols n lst *\<^sub>v v) $ i = lincomb f (set lst) $ i
 2. dim_vec (mat_of_cols n lst *\<^sub>v v) = dim_vec (lincomb f (set lst))
[PROOF STEP]
show "dim_vec (mat_of_cols n lst *\<^sub>v v) = dim_vec (lincomb f (set lst))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (mat_of_cols n lst *\<^sub>v v) = dim_vec (lincomb f (set lst))
[PROOF STEP]
using assms(1,2)
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec (length lst)
?i1 < length lst \<Longrightarrow> lst ! ?i1 \<in> carrier_vec n

goal (1 subgoal):
 1. dim_vec (mat_of_cols n lst *\<^sub>v v) = dim_vec (lincomb f (set lst))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_vec (mat_of_cols n lst *\<^sub>v v) = dim_vec (lincomb f (set lst))

goal (1 subgoal):
 1. \<And>i. i < dim_vec (lincomb f (set lst)) \<Longrightarrow> (mat_of_cols n lst *\<^sub>v v) $ i = lincomb f (set lst) $ i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < dim_vec (lincomb f (set lst)) \<Longrightarrow> (mat_of_cols n lst *\<^sub>v v) $ i = lincomb f (set lst) $ i
[PROOF STEP]
assume i:"i < dim_vec (lincomb f (set lst))"
[PROOF STATE]
proof (state)
this:
i < dim_vec (lincomb f (set lst))

goal (1 subgoal):
 1. \<And>i. i < dim_vec (lincomb f (set lst)) \<Longrightarrow> (mat_of_cols n lst *\<^sub>v v) $ i = lincomb f (set lst) $ i
[PROOF STEP]
hence i':"i < n"
[PROOF STATE]
proof (prove)
using this:
i < dim_vec (lincomb f (set lst))

goal (1 subgoal):
 1. i < n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < n

goal (1 subgoal):
 1. \<And>i. i < dim_vec (lincomb f (set lst)) \<Longrightarrow> (mat_of_cols n lst *\<^sub>v v) $ i = lincomb f (set lst) $ i
[PROOF STEP]
with an
[PROOF STATE]
proof (chain)
picking this:
?x \<in> set lst \<Longrightarrow> ?x \<in> carrier_vec n
i < n
[PROOF STEP]
have fcarr:"(\<lambda>v. f v \<cdot>\<^sub>v v) \<in> set lst \<rightarrow> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
?x \<in> set lst \<Longrightarrow> ?x \<in> carrier_vec n
i < n

goal (1 subgoal):
 1. (\<lambda>v. f v \<cdot>\<^sub>v v) \<in> set lst \<rightarrow> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>v. f v \<cdot>\<^sub>v v) \<in> set lst \<rightarrow> carrier_vec n

goal (1 subgoal):
 1. \<And>i. i < dim_vec (lincomb f (set lst)) \<Longrightarrow> (mat_of_cols n lst *\<^sub>v v) $ i = lincomb f (set lst) $ i
[PROOF STEP]
from i'
[PROOF STATE]
proof (chain)
picking this:
i < n
[PROOF STEP]
have "(mat_of_cols n lst *\<^sub>v v) $ i = row (mat_of_cols n lst) i \<bullet> v"
[PROOF STATE]
proof (prove)
using this:
i < n

goal (1 subgoal):
 1. (mat_of_cols n lst *\<^sub>v v) $ i = row (mat_of_cols n lst) i \<bullet> v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(mat_of_cols n lst *\<^sub>v v) $ i = row (mat_of_cols n lst) i \<bullet> v

goal (1 subgoal):
 1. \<And>i. i < dim_vec (lincomb f (set lst)) \<Longrightarrow> (mat_of_cols n lst *\<^sub>v v) $ i = lincomb f (set lst) $ i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(mat_of_cols n lst *\<^sub>v v) $ i = row (mat_of_cols n lst) i \<bullet> v

goal (1 subgoal):
 1. \<And>i. i < dim_vec (lincomb f (set lst)) \<Longrightarrow> (mat_of_cols n lst *\<^sub>v v) $ i = lincomb f (set lst) $ i
[PROOF STEP]
have "\<dots> = (\<Sum>ia = 0..<dim_vec v. lst ! ia $ i * v $ ia)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (mat_of_cols n lst) i \<bullet> v = (\<Sum>ia = 0..<dim_vec v. lst ! ia $ i * v $ ia)
[PROOF STEP]
unfolding mat_of_cols_def row_def scalar_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia = 0..<dim_vec v. vec (dim_col (mat n (length lst) (\<lambda>(i, j). lst ! j $ i))) (\<lambda>j. mat n (length lst) (\<lambda>(i, j). lst ! j $ i) $$ (i, j)) $ ia * v $ ia) = (\<Sum>ia = 0..<dim_vec v. lst ! ia $ i * v $ ia)
[PROOF STEP]
apply(rule sum.cong[OF refl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {0..<dim_vec v} \<Longrightarrow> vec (dim_col (mat n (length lst) (\<lambda>(i, j). lst ! j $ i))) (\<lambda>j. mat n (length lst) (\<lambda>(i, j). lst ! j $ i) $$ (i, j)) $ x * v $ x = lst ! x $ i * v $ x
[PROOF STEP]
using i an assms(1)
[PROOF STATE]
proof (prove)
using this:
i < dim_vec (lincomb f (set lst))
?x \<in> set lst \<Longrightarrow> ?x \<in> carrier_vec n
v \<in> carrier_vec (length lst)

goal (1 subgoal):
 1. \<And>x. x \<in> {0..<dim_vec v} \<Longrightarrow> vec (dim_col (mat n (length lst) (\<lambda>(i, j). lst ! j $ i))) (\<lambda>j. mat n (length lst) (\<lambda>(i, j). lst ! j $ i) $$ (i, j)) $ x * v $ x = lst ! x $ i * v $ x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row (mat_of_cols n lst) i \<bullet> v = (\<Sum>ia = 0..<dim_vec v. lst ! ia $ i * v $ ia)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (lincomb f (set lst)) \<Longrightarrow> (mat_of_cols n lst *\<^sub>v v) $ i = lincomb f (set lst) $ i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
row (mat_of_cols n lst) i \<bullet> v = (\<Sum>ia = 0..<dim_vec v. lst ! ia $ i * v $ ia)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (lincomb f (set lst)) \<Longrightarrow> (mat_of_cols n lst *\<^sub>v v) $ i = lincomb f (set lst) $ i
[PROOF STEP]
have "\<dots> = (\<Sum>ia = 0..<length lst. lst ! ia $ i * v $ ia)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia = 0..<dim_vec v. lst ! ia $ i * v $ ia) = (\<Sum>ia = 0..<length lst. lst ! ia $ i * v $ ia)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec (length lst)

goal (1 subgoal):
 1. (\<Sum>ia = 0..<dim_vec v. lst ! ia $ i * v $ ia) = (\<Sum>ia = 0..<length lst. lst ! ia $ i * v $ ia)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>ia = 0..<dim_vec v. lst ! ia $ i * v $ ia) = (\<Sum>ia = 0..<length lst. lst ! ia $ i * v $ ia)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (lincomb f (set lst)) \<Longrightarrow> (mat_of_cols n lst *\<^sub>v v) $ i = lincomb f (set lst) $ i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>ia = 0..<dim_vec v. lst ! ia $ i * v $ ia) = (\<Sum>ia = 0..<length lst. lst ! ia $ i * v $ ia)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (lincomb f (set lst)) \<Longrightarrow> (mat_of_cols n lst *\<^sub>v v) $ i = lincomb f (set lst) $ i
[PROOF STEP]
have "\<dots> = (\<Sum>x\<in>set lst. f x * x $ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia = 0..<length lst. lst ! ia $ i * v $ ia) = (\<Sum>x\<in>set lst. f x * x $ i)
[PROOF STEP]
unfolding f_def sum_distrib_right
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia = 0..<length lst. lst ! ia $ i * v $ ia) = (\<Sum>x\<in>set lst. \<Sum>n = 0..<length lst. (if x = lst ! n then v $ n else (0::'a)) * x $ i)
[PROOF STEP]
apply (subst sum.swap)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia = 0..<length lst. lst ! ia $ i * v $ ia) = (\<Sum>j = 0..<length lst. \<Sum>ia\<in>set lst. (if ia = lst ! j then v $ j else (0::'a)) * ia $ i)
[PROOF STEP]
apply(rule sum.cong[OF refl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {0..<length lst} \<Longrightarrow> lst ! x $ i * v $ x = (\<Sum>ia\<in>set lst. (if ia = lst ! x then v $ x else (0::'a)) * ia $ i)
[PROOF STEP]
unfolding if_distrib if_distribR mult_zero_left sum.delta[OF finite_set]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {0..<length lst} \<Longrightarrow> if lst ! x \<in> set lst then lst ! x $ i * v $ x = v $ x * lst ! x $ i else lst ! x $ i * v $ x = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>ia = 0..<length lst. lst ! ia $ i * v $ ia) = (\<Sum>x\<in>set lst. f x * x $ i)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (lincomb f (set lst)) \<Longrightarrow> (mat_of_cols n lst *\<^sub>v v) $ i = lincomb f (set lst) $ i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>ia = 0..<length lst. lst ! ia $ i * v $ ia) = (\<Sum>x\<in>set lst. f x * x $ i)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (lincomb f (set lst)) \<Longrightarrow> (mat_of_cols n lst *\<^sub>v v) $ i = lincomb f (set lst) $ i
[PROOF STEP]
have "\<dots> = (\<Sum>x\<in>set lst. (f x \<cdot>\<^sub>v x) $ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>set lst. f x * x $ i) = (\<Sum>x\<in>set lst. (f x \<cdot>\<^sub>v x) $ i)
[PROOF STEP]
apply(rule sum.cong[OF refl],subst index_smult_vec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set lst \<Longrightarrow> i < dim_vec x
 2. \<And>x. x \<in> set lst \<Longrightarrow> f x * x $ i = f x * x $ i
[PROOF STEP]
using i slc
[PROOF STATE]
proof (prove)
using this:
i < dim_vec (lincomb f (set lst))
set lst \<subseteq> carrier_vec n

goal (2 subgoals):
 1. \<And>x. x \<in> set lst \<Longrightarrow> i < dim_vec x
 2. \<And>x. x \<in> set lst \<Longrightarrow> f x * x $ i = f x * x $ i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set lst. f x * x $ i) = (\<Sum>x\<in>set lst. (f x \<cdot>\<^sub>v x) $ i)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (lincomb f (set lst)) \<Longrightarrow> (mat_of_cols n lst *\<^sub>v v) $ i = lincomb f (set lst) $ i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set lst. f x * x $ i) = (\<Sum>x\<in>set lst. (f x \<cdot>\<^sub>v x) $ i)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (lincomb f (set lst)) \<Longrightarrow> (mat_of_cols n lst *\<^sub>v v) $ i = lincomb f (set lst) $ i
[PROOF STEP]
have "\<dots> = (\<Oplus>\<^bsub>V\<^esub>v\<in>set lst. f v \<cdot>\<^sub>v v) $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>set lst. (f x \<cdot>\<^sub>v x) $ i) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set lst. f v \<cdot>\<^sub>v v) $ i
[PROOF STEP]
unfolding finsum_index[OF i' fcarr slc]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>set lst. (f x \<cdot>\<^sub>v x) $ i) = (\<Sum>x\<in>set lst. (f x \<cdot>\<^sub>v x) $ i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set lst. (f x \<cdot>\<^sub>v x) $ i) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set lst. f v \<cdot>\<^sub>v v) $ i

goal (1 subgoal):
 1. \<And>i. i < dim_vec (lincomb f (set lst)) \<Longrightarrow> (mat_of_cols n lst *\<^sub>v v) $ i = lincomb f (set lst) $ i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(mat_of_cols n lst *\<^sub>v v) $ i = (\<Oplus>\<^bsub>V\<^esub>v\<in>set lst. f v \<cdot>\<^sub>v v) $ i
[PROOF STEP]
show "(mat_of_cols n lst *\<^sub>v v) $ i = lincomb f (set lst) $ i"
[PROOF STATE]
proof (prove)
using this:
(mat_of_cols n lst *\<^sub>v v) $ i = (\<Oplus>\<^bsub>V\<^esub>v\<in>set lst. f v \<cdot>\<^sub>v v) $ i

goal (1 subgoal):
 1. (mat_of_cols n lst *\<^sub>v v) $ i = lincomb f (set lst) $ i
[PROOF STEP]
by (auto simp:lincomb_def)
[PROOF STATE]
proof (state)
this:
(mat_of_cols n lst *\<^sub>v v) $ i = lincomb f (set lst) $ i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mat_of_cols n lst *\<^sub>v v = lincomb f (set lst)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma oassert_iff[simp]:
  "oassert \<Phi> = Some x \<longleftrightarrow> \<Phi>"
  "oassert \<Phi> = None \<longleftrightarrow> \<not>\<Phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (oassert \<Phi> = Some x) = \<Phi> &&& (oassert \<Phi> = None) = (\<not> \<Phi>)
[PROOF STEP]
by (cases \<Phi>) auto


[STATEMENT]
lemma oreturn_rule[ospec_rules]: "\<lbrakk> P r \<rbrakk> \<Longrightarrow> ospec (Some r) P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P r \<Longrightarrow> ospec (Some r) P
[PROOF STEP]
by simp


[STATEMENT]
lemma obind_rule[ospec_rules]: "\<lbrakk> ospec m Q; \<And>r. Q r \<Longrightarrow> ospec (f r) P \<rbrakk> \<Longrightarrow> ospec (m \<bind> f) P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ospec m Q; \<And>r. Q r \<Longrightarrow> ospec (f r) P\<rbrakk> \<Longrightarrow> ospec (m \<bind> f) P
[PROOF STEP]
apply (cases m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ospec m Q; \<And>r. Q r \<Longrightarrow> ospec (f r) P; m = None\<rbrakk> \<Longrightarrow> ospec (m \<bind> f) P
 2. \<And>a. \<lbrakk>ospec m Q; \<And>r. Q r \<Longrightarrow> ospec (f r) P; m = Some a\<rbrakk> \<Longrightarrow> ospec (m \<bind> f) P
[PROOF STEP]
apply (auto split: Option.bind_splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ospec_alt: "ospec m P = (case m of None \<Rightarrow> False | Some x \<Rightarrow> P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ospec m P = (case m of None \<Rightarrow> False | Some x \<Rightarrow> P x)
[PROOF STEP]
by (auto split: option.splits)


[STATEMENT]
lemma ospec_bind_simp: "ospec (m \<bind> f) P \<longleftrightarrow> (ospec m (\<lambda>r. ospec (f r) P))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ospec (m \<bind> f) P = ospec m (\<lambda>r. ospec (f r) P)
[PROOF STEP]
apply (cases m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. m = None \<Longrightarrow> ospec (m \<bind> f) P = ospec m (\<lambda>r. ospec (f r) P)
 2. \<And>a. m = Some a \<Longrightarrow> ospec (m \<bind> f) P = ospec m (\<lambda>r. ospec (f r) P)
[PROOF STEP]
apply (auto split: Option.bind_splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ospec_cons:
  assumes "ospec m Q"
  assumes "\<And>r. Q r \<Longrightarrow> P r"
  shows "ospec m P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ospec m P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ospec m Q
Q ?r \<Longrightarrow> P ?r

goal (1 subgoal):
 1. ospec m P
[PROOF STEP]
by (cases m) auto


[STATEMENT]
lemma oreturn_synth: "ospec (Some x) (\<lambda>r. r=x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ospec (Some x) (\<lambda>r. r = x)
[PROOF STEP]
by simp


[STATEMENT]
lemma ospecD: "ospec x P \<Longrightarrow> x = Some y \<Longrightarrow> P y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ospec x P; x = Some y\<rbrakk> \<Longrightarrow> P y
[PROOF STEP]
by simp


[STATEMENT]
lemma ospecD2: "ospec x P \<Longrightarrow> \<exists>y. x = Some y \<and> P y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ospec x P \<Longrightarrow> \<exists>y. x = Some y \<and> P y
[PROOF STEP]
by(cases x) simp_all


[STATEMENT]
lemma fun_set_rel_def: "\<langle>R\<rangle>fun_set_rel = (R\<rightarrow>bool_rel) O br Collect (\<lambda>_. True)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>R\<rangle>fun_set_rel = (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True)
[PROOF STEP]
by (simp add: relAPP_def fun_set_rel_internal_def)


[STATEMENT]
lemma fun_set_rel_sv[relator_props]:
  "\<lbrakk>single_valued R; Range R = UNIV\<rbrakk> \<Longrightarrow> single_valued (\<langle>R\<rangle>fun_set_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>single_valued R; Range R = UNIV\<rbrakk> \<Longrightarrow> single_valued (\<langle>R\<rangle>fun_set_rel)
[PROOF STEP]
unfolding fun_set_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>single_valued R; Range R = UNIV\<rbrakk> \<Longrightarrow> single_valued ((R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True))
[PROOF STEP]
by (tagged_solver (keep))


[STATEMENT]
lemma fun_set_rel_RUNIV[relator_props]:
  assumes SV: "single_valued R"
  shows "Range (\<langle>R\<rangle>fun_set_rel) = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Range (\<langle>R\<rangle>fun_set_rel) = UNIV
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Range (\<langle>R\<rangle>fun_set_rel) = UNIV
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Range (\<langle>R\<rangle>fun_set_rel) = UNIV
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Range (\<langle>R\<rangle>fun_set_rel) = UNIV
[PROOF STEP]
have "\<exists>a. (a,b)\<in>\<langle>R\<rangle>fun_set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. (a, b) \<in> \<langle>R\<rangle>fun_set_rel
[PROOF STEP]
unfolding fun_set_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. (a, b) \<in> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True)
[PROOF STEP]
apply (rule exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (?a, b) \<in> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True)
[PROOF STEP]
apply (rule relcompI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (?a, ?b2) \<in> R \<rightarrow> bool_rel
 2. (?b2, b) \<in> br Collect (\<lambda>_. True)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (?a, ?b2) \<in> R \<rightarrow> bool_rel
 2. (?b2, b) \<in> br Collect (\<lambda>_. True)
[PROOF STEP]
show "((\<lambda>x. x\<in>b),b)\<in>br Collect (\<lambda>_. True)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. x \<in> b, b) \<in> br Collect (\<lambda>_. True)
[PROOF STEP]
by (auto simp: br_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. x \<in> b, b) \<in> br Collect (\<lambda>_. True)

goal (1 subgoal):
 1. (?a, \<lambda>x. x \<in> b) \<in> R \<rightarrow> bool_rel
[PROOF STEP]
show "(\<lambda>x'. \<exists>x. (x',x)\<in>R \<and> x\<in>b,\<lambda>x. x \<in> b)\<in>R \<rightarrow> bool_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x'. \<exists>x. (x', x) \<in> R \<and> x \<in> b, \<lambda>x. x \<in> b) \<in> R \<rightarrow> bool_rel
[PROOF STEP]
by (auto dest: single_valuedD[OF SV])
[PROOF STATE]
proof (state)
this:
(\<lambda>x'. \<exists>x. (x', x) \<in> R \<and> x \<in> b, \<lambda>x. x \<in> b) \<in> R \<rightarrow> bool_rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a. (a, b) \<in> \<langle>R\<rangle>fun_set_rel

goal (1 subgoal):
 1. Range (\<langle>R\<rangle>fun_set_rel) = UNIV
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<exists>a. (a, ?b2) \<in> \<langle>R\<rangle>fun_set_rel

goal (1 subgoal):
 1. Range (\<langle>R\<rangle>fun_set_rel) = UNIV
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>a. (a, ?b2) \<in> \<langle>R\<rangle>fun_set_rel

goal (1 subgoal):
 1. Range (\<langle>R\<rangle>fun_set_rel) = UNIV
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Range (\<langle>R\<rangle>fun_set_rel) = UNIV

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fs_mem_refine[autoref_rules]: "(\<lambda>x f. f x,(\<in>)) \<in> R \<rightarrow> \<langle>R\<rangle>fun_set_rel \<rightarrow> bool_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x f. f x, (\<in>)) \<in> R \<rightarrow> \<langle>R\<rangle>fun_set_rel \<rightarrow> bool_rel
[PROOF STEP]
apply (intro fun_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> R; (aa, a'a) \<in> \<langle>R\<rangle>fun_set_rel\<rbrakk> \<Longrightarrow> (aa a, a' \<in> a'a) \<in> bool_rel
[PROOF STEP]
apply (auto simp add: fun_set_rel_def br_def dest: fun_relD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fun_set_Collect_refine[autoref_rules]:
  "(\<lambda>x. x, Collect)\<in>(R\<rightarrow>bool_rel) \<rightarrow> \<langle>R\<rangle>fun_set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. x, Collect) \<in> (R \<rightarrow> bool_rel) \<rightarrow> \<langle>R\<rangle>fun_set_rel
[PROOF STEP]
unfolding fun_set_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. x, Collect) \<in> (R \<rightarrow> bool_rel) \<rightarrow> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True)
[PROOF STEP]
by (auto simp: br_def)


[STATEMENT]
lemma fun_set_empty_refine[autoref_rules]:
  "(\<lambda>_. False,{})\<in>\<langle>R\<rangle>fun_set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>_. False, {}) \<in> \<langle>R\<rangle>fun_set_rel
[PROOF STEP]
by (force simp add: fun_set_rel_def br_def)


[STATEMENT]
lemma fun_set_UNIV_refine[autoref_rules]:
  "(\<lambda>_. True,UNIV)\<in>\<langle>R\<rangle>fun_set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>_. True, UNIV) \<in> \<langle>R\<rangle>fun_set_rel
[PROOF STEP]
by (force simp add: fun_set_rel_def br_def)


[STATEMENT]
lemma fun_set_union_refine[autoref_rules]:
  "(\<lambda>a b x. a x \<or> b x,(\<union>))\<in>\<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a b x. a x \<or> b x, (\<union>)) \<in> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>a b x. a x \<or> b x, (\<union>)) \<in> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel
[PROOF STEP]
have A: "\<And>a b. (\<lambda>x. x\<in>a \<or> x\<in>b, a \<union> b) \<in> br Collect (\<lambda>_. True)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (\<lambda>x. x \<in> a \<or> x \<in> b, a \<union> b) \<in> br Collect (\<lambda>_. True)
[PROOF STEP]
by (auto simp: br_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. x \<in> ?a \<or> x \<in> ?b, ?a \<union> ?b) \<in> br Collect (\<lambda>_. True)

goal (1 subgoal):
 1. (\<lambda>a b x. a x \<or> b x, (\<union>)) \<in> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a b x. a x \<or> b x, (\<union>)) \<in> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel
[PROOF STEP]
apply (simp add: fun_set_rel_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a b x. a x \<or> b x, (\<union>)) \<in> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True) \<rightarrow> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True) \<rightarrow> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True)
[PROOF STEP]
apply (intro fun_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True); (aa, a'a) \<in> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True)\<rbrakk> \<Longrightarrow> (\<lambda>x. a x \<or> aa x, a' \<union> a'a) \<in> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z xa ya za. \<lbrakk>(x, y) \<in> R \<rightarrow> bool_rel; (y, z) \<in> br Collect (\<lambda>_. True); (xa, ya) \<in> R \<rightarrow> bool_rel; (ya, za) \<in> br Collect (\<lambda>_. True)\<rbrakk> \<Longrightarrow> (\<lambda>xb. x xb \<or> xa xb, z \<union> za) \<in> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y z xa ya za. \<lbrakk>(x, y) \<in> R \<rightarrow> bool_rel; (y, z) \<in> br Collect (\<lambda>_. True); (xa, ya) \<in> R \<rightarrow> bool_rel; (ya, za) \<in> br Collect (\<lambda>_. True)\<rbrakk> \<Longrightarrow> (\<lambda>xb. x xb \<or> xa xb, ?b12 x y z xa ya za) \<in> R \<rightarrow> bool_rel
 2. \<And>x y z xa ya za. \<lbrakk>(x, y) \<in> R \<rightarrow> bool_rel; (y, z) \<in> br Collect (\<lambda>_. True); (xa, ya) \<in> R \<rightarrow> bool_rel; (ya, za) \<in> br Collect (\<lambda>_. True)\<rbrakk> \<Longrightarrow> (?b12 x y z xa ya za, z \<union> za) \<in> br Collect (\<lambda>_. True)
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y z xa ya za. \<lbrakk>(x, y) \<in> R \<rightarrow> bool_rel; (y, z) \<in> br Collect (\<lambda>_. True); (xa, ya) \<in> R \<rightarrow> bool_rel; (ya, za) \<in> br Collect (\<lambda>_. True)\<rbrakk> \<Longrightarrow> (?b12 x y z xa ya za, z \<union> za) \<in> br Collect (\<lambda>_. True)
 2. \<And>x y z xa ya za. \<lbrakk>(x, y) \<in> R \<rightarrow> bool_rel; (y, z) \<in> br Collect (\<lambda>_. True); (xa, ya) \<in> R \<rightarrow> bool_rel; (ya, za) \<in> br Collect (\<lambda>_. True)\<rbrakk> \<Longrightarrow> (\<lambda>xb. x xb \<or> xa xb, ?b12 x y z xa ya za) \<in> R \<rightarrow> bool_rel
[PROOF STEP]
apply (rule A)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z xa ya za. \<lbrakk>(x, y) \<in> R \<rightarrow> bool_rel; (y, z) \<in> br Collect (\<lambda>_. True); (xa, ya) \<in> R \<rightarrow> bool_rel; (ya, za) \<in> br Collect (\<lambda>_. True)\<rbrakk> \<Longrightarrow> (\<lambda>xb. x xb \<or> xa xb, \<lambda>x. x \<in> z \<or> x \<in> za) \<in> R \<rightarrow> bool_rel
[PROOF STEP]
apply (auto simp: br_def dest: fun_relD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>a b x. a x \<or> b x, (\<union>)) \<in> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fun_set_inter_refine[autoref_rules]:
  "(\<lambda>a b x. a x \<and> b x,(\<inter>))\<in>\<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a b x. a x \<and> b x, (\<inter>)) \<in> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>a b x. a x \<and> b x, (\<inter>)) \<in> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel
[PROOF STEP]
have A: "\<And>a b. (\<lambda>x. x\<in>a \<and> x\<in>b, a \<inter> b) \<in> br Collect (\<lambda>_. True)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (\<lambda>x. x \<in> a \<and> x \<in> b, a \<inter> b) \<in> br Collect (\<lambda>_. True)
[PROOF STEP]
by (auto simp: br_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. x \<in> ?a \<and> x \<in> ?b, ?a \<inter> ?b) \<in> br Collect (\<lambda>_. True)

goal (1 subgoal):
 1. (\<lambda>a b x. a x \<and> b x, (\<inter>)) \<in> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a b x. a x \<and> b x, (\<inter>)) \<in> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel
[PROOF STEP]
apply (simp add: fun_set_rel_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a b x. a x \<and> b x, (\<inter>)) \<in> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True) \<rightarrow> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True) \<rightarrow> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True)
[PROOF STEP]
apply (intro fun_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True); (aa, a'a) \<in> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True)\<rbrakk> \<Longrightarrow> (\<lambda>x. a x \<and> aa x, a' \<inter> a'a) \<in> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z xa ya za. \<lbrakk>(x, y) \<in> R \<rightarrow> bool_rel; (y, z) \<in> br Collect (\<lambda>_. True); (xa, ya) \<in> R \<rightarrow> bool_rel; (ya, za) \<in> br Collect (\<lambda>_. True)\<rbrakk> \<Longrightarrow> (\<lambda>xb. x xb \<and> xa xb, z \<inter> za) \<in> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y z xa ya za. \<lbrakk>(x, y) \<in> R \<rightarrow> bool_rel; (y, z) \<in> br Collect (\<lambda>_. True); (xa, ya) \<in> R \<rightarrow> bool_rel; (ya, za) \<in> br Collect (\<lambda>_. True)\<rbrakk> \<Longrightarrow> (\<lambda>xb. x xb \<and> xa xb, ?b12 x y z xa ya za) \<in> R \<rightarrow> bool_rel
 2. \<And>x y z xa ya za. \<lbrakk>(x, y) \<in> R \<rightarrow> bool_rel; (y, z) \<in> br Collect (\<lambda>_. True); (xa, ya) \<in> R \<rightarrow> bool_rel; (ya, za) \<in> br Collect (\<lambda>_. True)\<rbrakk> \<Longrightarrow> (?b12 x y z xa ya za, z \<inter> za) \<in> br Collect (\<lambda>_. True)
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y z xa ya za. \<lbrakk>(x, y) \<in> R \<rightarrow> bool_rel; (y, z) \<in> br Collect (\<lambda>_. True); (xa, ya) \<in> R \<rightarrow> bool_rel; (ya, za) \<in> br Collect (\<lambda>_. True)\<rbrakk> \<Longrightarrow> (?b12 x y z xa ya za, z \<inter> za) \<in> br Collect (\<lambda>_. True)
 2. \<And>x y z xa ya za. \<lbrakk>(x, y) \<in> R \<rightarrow> bool_rel; (y, z) \<in> br Collect (\<lambda>_. True); (xa, ya) \<in> R \<rightarrow> bool_rel; (ya, za) \<in> br Collect (\<lambda>_. True)\<rbrakk> \<Longrightarrow> (\<lambda>xb. x xb \<and> xa xb, ?b12 x y z xa ya za) \<in> R \<rightarrow> bool_rel
[PROOF STEP]
apply (rule A)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z xa ya za. \<lbrakk>(x, y) \<in> R \<rightarrow> bool_rel; (y, z) \<in> br Collect (\<lambda>_. True); (xa, ya) \<in> R \<rightarrow> bool_rel; (ya, za) \<in> br Collect (\<lambda>_. True)\<rbrakk> \<Longrightarrow> (\<lambda>xb. x xb \<and> xa xb, \<lambda>x. x \<in> z \<and> x \<in> za) \<in> R \<rightarrow> bool_rel
[PROOF STEP]
apply (auto simp: br_def dest: fun_relD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>a b x. a x \<and> b x, (\<inter>)) \<in> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fun_set_diff_refine[autoref_rules]:
  "(\<lambda>a b x. a x \<and> \<not>b x,(-))\<in>\<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a b x. a x \<and> \<not> b x, (-)) \<in> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>a b x. a x \<and> \<not> b x, (-)) \<in> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel
[PROOF STEP]
have A: "\<And>a b. (\<lambda>x. x\<in>a \<and> \<not>x\<in>b, a - b) \<in> br Collect (\<lambda>_. True)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (\<lambda>x. x \<in> a \<and> x \<notin> b, a - b) \<in> br Collect (\<lambda>_. True)
[PROOF STEP]
by (auto simp: br_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. x \<in> ?a \<and> x \<notin> ?b, ?a - ?b) \<in> br Collect (\<lambda>_. True)

goal (1 subgoal):
 1. (\<lambda>a b x. a x \<and> \<not> b x, (-)) \<in> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a b x. a x \<and> \<not> b x, (-)) \<in> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel
[PROOF STEP]
apply (simp add: fun_set_rel_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a b x. a x \<and> \<not> b x, (-)) \<in> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True) \<rightarrow> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True) \<rightarrow> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True)
[PROOF STEP]
apply (intro fun_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True); (aa, a'a) \<in> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True)\<rbrakk> \<Longrightarrow> (\<lambda>x. a x \<and> \<not> aa x, a' - a'a) \<in> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z xa ya za. \<lbrakk>(x, y) \<in> R \<rightarrow> bool_rel; (y, z) \<in> br Collect (\<lambda>_. True); (xa, ya) \<in> R \<rightarrow> bool_rel; (ya, za) \<in> br Collect (\<lambda>_. True)\<rbrakk> \<Longrightarrow> (\<lambda>xb. x xb \<and> \<not> xa xb, z - za) \<in> (R \<rightarrow> bool_rel) O br Collect (\<lambda>_. True)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y z xa ya za. \<lbrakk>(x, y) \<in> R \<rightarrow> bool_rel; (y, z) \<in> br Collect (\<lambda>_. True); (xa, ya) \<in> R \<rightarrow> bool_rel; (ya, za) \<in> br Collect (\<lambda>_. True)\<rbrakk> \<Longrightarrow> (\<lambda>xb. x xb \<and> \<not> xa xb, ?b12 x y z xa ya za) \<in> R \<rightarrow> bool_rel
 2. \<And>x y z xa ya za. \<lbrakk>(x, y) \<in> R \<rightarrow> bool_rel; (y, z) \<in> br Collect (\<lambda>_. True); (xa, ya) \<in> R \<rightarrow> bool_rel; (ya, za) \<in> br Collect (\<lambda>_. True)\<rbrakk> \<Longrightarrow> (?b12 x y z xa ya za, z - za) \<in> br Collect (\<lambda>_. True)
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y z xa ya za. \<lbrakk>(x, y) \<in> R \<rightarrow> bool_rel; (y, z) \<in> br Collect (\<lambda>_. True); (xa, ya) \<in> R \<rightarrow> bool_rel; (ya, za) \<in> br Collect (\<lambda>_. True)\<rbrakk> \<Longrightarrow> (?b12 x y z xa ya za, z - za) \<in> br Collect (\<lambda>_. True)
 2. \<And>x y z xa ya za. \<lbrakk>(x, y) \<in> R \<rightarrow> bool_rel; (y, z) \<in> br Collect (\<lambda>_. True); (xa, ya) \<in> R \<rightarrow> bool_rel; (ya, za) \<in> br Collect (\<lambda>_. True)\<rbrakk> \<Longrightarrow> (\<lambda>xb. x xb \<and> \<not> xa xb, ?b12 x y z xa ya za) \<in> R \<rightarrow> bool_rel
[PROOF STEP]
apply (rule A)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z xa ya za. \<lbrakk>(x, y) \<in> R \<rightarrow> bool_rel; (y, z) \<in> br Collect (\<lambda>_. True); (xa, ya) \<in> R \<rightarrow> bool_rel; (ya, za) \<in> br Collect (\<lambda>_. True)\<rbrakk> \<Longrightarrow> (\<lambda>xb. x xb \<and> \<not> xa xb, \<lambda>x. x \<in> z \<and> x \<notin> za) \<in> R \<rightarrow> bool_rel
[PROOF STEP]
apply (auto simp: br_def dest: fun_relD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>a b x. a x \<and> \<not> b x, (-)) \<in> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel \<rightarrow> \<langle>R\<rangle>fun_set_rel

goal:
No subgoals!
[PROOF STEP]
qed