[STATEMENT]
lemma mat_of_cblinfun_Proj_ccspan:
  fixes S :: "'a::onb_enum list"
  shows "mat_of_cblinfun (Proj (ccspan (set S))) =
    (let d = length (canonical_basis :: 'a list) in
      mk_projector_orthog d (gram_schmidt0 d (map vec_of_basis_enum S)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (Proj (ccspan (set S))) = (let d = length canonical_basis in mk_projector_orthog d (gram_schmidt0 d (map vec_of_basis_enum S)))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat_of_cblinfun (Proj (ccspan (set S))) = (let d = length canonical_basis in mk_projector_orthog d (gram_schmidt0 d (map vec_of_basis_enum S)))
[PROOF STEP]
define d gs
    where "d = length (canonical_basis :: 'a list)"
      and "gs = gram_schmidt0 d (map vec_of_basis_enum S)"
[PROOF STATE]
proof (state)
this:
d = length canonical_basis
gs = gram_schmidt0 d (map vec_of_basis_enum S)

goal (1 subgoal):
 1. mat_of_cblinfun (Proj (ccspan (set S))) = (let d = length canonical_basis in mk_projector_orthog d (gram_schmidt0 d (map vec_of_basis_enum S)))
[PROOF STEP]
interpret complex_vec_space d
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat_of_cblinfun (Proj (ccspan (set S))) = (let d = length canonical_basis in mk_projector_orthog d (gram_schmidt0 d (map vec_of_basis_enum S)))
[PROOF STEP]
have gs_dim: "x \<in> set gs \<Longrightarrow> dim_vec x = d" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set gs \<Longrightarrow> dim_vec x = d
[PROOF STEP]
by (smt carrier_vecD carrier_vec_dim_vec d_def dim_vec_of_basis_enum' ex_map_conv gram_schmidt0_result(1) gs_def subset_code(1))
[PROOF STATE]
proof (state)
this:
?x1 \<in> set gs \<Longrightarrow> dim_vec ?x1 = d

goal (1 subgoal):
 1. mat_of_cblinfun (Proj (ccspan (set S))) = (let d = length canonical_basis in mk_projector_orthog d (gram_schmidt0 d (map vec_of_basis_enum S)))
[PROOF STEP]
have ortho_gs: "is_ortho_set (set (map basis_enum_of_vec gs :: 'a list))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_ortho_set (set (map basis_enum_of_vec gs))
[PROOF STEP]
apply (subst corthogonal_vec_of_basis_enum[THEN iffD1], auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. corthogonal (map (vec_of_basis_enum \<circ> basis_enum_of_vec) gs)
[PROOF STEP]
by (smt carrier_dim_vec cof_vec_space.gram_schmidt0_result(1) d_def dim_vec_of_basis_enum' gram_schmidt0_result(3) gs_def imageE map_idI map_map o_apply set_map subset_code(1) basis_enum_of_vec_inverse)
[PROOF STATE]
proof (state)
this:
is_ortho_set (set (map basis_enum_of_vec gs))

goal (1 subgoal):
 1. mat_of_cblinfun (Proj (ccspan (set S))) = (let d = length canonical_basis in mk_projector_orthog d (gram_schmidt0 d (map vec_of_basis_enum S)))
[PROOF STEP]
have distinct_gs: "distinct (map basis_enum_of_vec gs :: 'a list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map basis_enum_of_vec gs)
[PROOF STEP]
by (metis (mono_tags, opaque_lifting) carrier_vec_dim_vec cof_vec_space.gram_schmidt0_result(2) d_def dim_vec_of_basis_enum' distinct_map gs_def gs_dim image_iff inj_on_inverseI set_map subsetI basis_enum_of_vec_inverse)
[PROOF STATE]
proof (state)
this:
distinct (map basis_enum_of_vec gs)

goal (1 subgoal):
 1. mat_of_cblinfun (Proj (ccspan (set S))) = (let d = length canonical_basis in mk_projector_orthog d (gram_schmidt0 d (map vec_of_basis_enum S)))
[PROOF STEP]
have "mk_projector_orthog d gs
      = mk_projector_orthog d (map vec_of_basis_enum (map basis_enum_of_vec gs :: 'a list))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_projector_orthog d gs = mk_projector_orthog d (map vec_of_basis_enum (map basis_enum_of_vec gs))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_projector_orthog d gs = mk_projector_orthog d (map (vec_of_basis_enum \<circ> basis_enum_of_vec) gs)
[PROOF STEP]
apply (subst map_cong[where ys=gs and g=id], simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set gs \<Longrightarrow> (vec_of_basis_enum \<circ> basis_enum_of_vec) x = id x
 2. mk_projector_orthog d gs = mk_projector_orthog d (map id gs)
[PROOF STEP]
using gs_dim
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> set gs \<Longrightarrow> dim_vec ?x1 = d

goal (2 subgoals):
 1. \<And>x. x \<in> set gs \<Longrightarrow> (vec_of_basis_enum \<circ> basis_enum_of_vec) x = id x
 2. mk_projector_orthog d gs = mk_projector_orthog d (map id gs)
[PROOF STEP]
by (auto intro!: vec_of_basis_enum_inverse simp: d_def)
[PROOF STATE]
proof (state)
this:
mk_projector_orthog d gs = mk_projector_orthog d (map vec_of_basis_enum (map basis_enum_of_vec gs))

goal (1 subgoal):
 1. mat_of_cblinfun (Proj (ccspan (set S))) = (let d = length canonical_basis in mk_projector_orthog d (gram_schmidt0 d (map vec_of_basis_enum S)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mk_projector_orthog d gs = mk_projector_orthog d (map vec_of_basis_enum (map basis_enum_of_vec gs))

goal (1 subgoal):
 1. mat_of_cblinfun (Proj (ccspan (set S))) = (let d = length canonical_basis in mk_projector_orthog d (gram_schmidt0 d (map vec_of_basis_enum S)))
[PROOF STEP]
have "\<dots> = mat_of_cblinfun (Proj (ccspan (set (map basis_enum_of_vec gs :: 'a list))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_projector_orthog d (map vec_of_basis_enum (map basis_enum_of_vec gs)) = mat_of_cblinfun (Proj (ccspan (set (map basis_enum_of_vec gs))))
[PROOF STEP]
unfolding d_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_projector_orthog (length canonical_basis) (map vec_of_basis_enum (map basis_enum_of_vec gs)) = mat_of_cblinfun (Proj (ccspan (set (map basis_enum_of_vec gs))))
[PROOF STEP]
apply (subst mk_projector_orthog_correct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. is_ortho_set (set (map basis_enum_of_vec gs))
 2. distinct (map basis_enum_of_vec gs)
 3. mat_of_cblinfun (Proj (ccspan (set (map basis_enum_of_vec gs)))) = mat_of_cblinfun (Proj (ccspan (set (map basis_enum_of_vec gs))))
[PROOF STEP]
using ortho_gs distinct_gs
[PROOF STATE]
proof (prove)
using this:
is_ortho_set (set (map basis_enum_of_vec gs))
distinct (map basis_enum_of_vec gs)

goal (3 subgoals):
 1. is_ortho_set (set (map basis_enum_of_vec gs))
 2. distinct (map basis_enum_of_vec gs)
 3. mat_of_cblinfun (Proj (ccspan (set (map basis_enum_of_vec gs)))) = mat_of_cblinfun (Proj (ccspan (set (map basis_enum_of_vec gs))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mk_projector_orthog d (map vec_of_basis_enum (map basis_enum_of_vec gs)) = mat_of_cblinfun (Proj (ccspan (set (map basis_enum_of_vec gs))))

goal (1 subgoal):
 1. mat_of_cblinfun (Proj (ccspan (set S))) = (let d = length canonical_basis in mk_projector_orthog d (gram_schmidt0 d (map vec_of_basis_enum S)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mk_projector_orthog d (map vec_of_basis_enum (map basis_enum_of_vec gs)) = mat_of_cblinfun (Proj (ccspan (set (map basis_enum_of_vec gs))))

goal (1 subgoal):
 1. mat_of_cblinfun (Proj (ccspan (set S))) = (let d = length canonical_basis in mk_projector_orthog d (gram_schmidt0 d (map vec_of_basis_enum S)))
[PROOF STEP]
have "\<dots> = mat_of_cblinfun (Proj (ccspan (set S)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (Proj (ccspan (set (map basis_enum_of_vec gs)))) = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
apply (rule arg_cong[where f="\<lambda>x. mat_of_cblinfun (Proj x)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccspan (set (map basis_enum_of_vec gs)) = ccspan (set S)
[PROOF STEP]
unfolding gs_def d_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccspan (set (map basis_enum_of_vec (gram_schmidt0 (length canonical_basis) (map vec_of_basis_enum S)))) = ccspan (set S)
[PROOF STEP]
apply (subst ccspan_gram_schmidt0_invariant)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. set (map vec_of_basis_enum S) \<subseteq> carrier_vec (length canonical_basis)
 2. ccspan (set (map basis_enum_of_vec (map vec_of_basis_enum S))) = ccspan (set S)
[PROOF STEP]
by (auto simp add: carrier_vecI dim_vec_of_basis_enum')
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (Proj (ccspan (set (map basis_enum_of_vec gs)))) = mat_of_cblinfun (Proj (ccspan (set S)))

goal (1 subgoal):
 1. mat_of_cblinfun (Proj (ccspan (set S))) = (let d = length canonical_basis in mk_projector_orthog d (gram_schmidt0 d (map vec_of_basis_enum S)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mk_projector_orthog d gs = mat_of_cblinfun (Proj (ccspan (set S)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mk_projector_orthog d gs = mat_of_cblinfun (Proj (ccspan (set S)))

goal (1 subgoal):
 1. mat_of_cblinfun (Proj (ccspan (set S))) = (let d = length canonical_basis in mk_projector_orthog d (gram_schmidt0 d (map vec_of_basis_enum S)))
[PROOF STEP]
unfolding d_def gs_def
[PROOF STATE]
proof (prove)
using this:
mk_projector_orthog (length canonical_basis) (gram_schmidt0 (length canonical_basis) (map vec_of_basis_enum S)) = mat_of_cblinfun (Proj (ccspan (set S)))

goal (1 subgoal):
 1. mat_of_cblinfun (Proj (ccspan (set S))) = (let d = length canonical_basis in mk_projector_orthog d (gram_schmidt0 d (map vec_of_basis_enum S)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat_of_cblinfun (Proj (ccspan (set S))) = (let d = length canonical_basis in mk_projector_orthog d (gram_schmidt0 d (map vec_of_basis_enum S)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_sum_orient:
  "sum f {k..<j} + sum f {l..<k} = sum f {l..<k} + sum f {k..<j}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {k..<j} + sum f {l..<k} = sum f {l..<k} + sum f {k..<j}
[PROOF STEP]
by (fact add.commute)


[STATEMENT]
lemma add_sum_int:
  fixes j k l :: int
  shows "j < k \<Longrightarrow> k < l \<Longrightarrow>
    sum f {j..<k} + sum f {k..<l} = sum f {j..<l}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j < k; k < l\<rbrakk> \<Longrightarrow> sum f {j..<k} + sum f {k..<l} = sum f {j..<l}
[PROOF STEP]
by (simp_all add: sum.union_inter [symmetric] ivl_disj_un)


[STATEMENT]
lemma \<Delta>_shift:
  "\<Delta> (\<lambda>k. l + f k) = \<Delta> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta> (\<lambda>k. l + f k) = \<Delta> f
[PROOF STEP]
by (simp add: \<Delta>_def fun_eq_iff)


[STATEMENT]
lemma \<Delta>_same_shift:
  assumes "\<Delta> f = \<Delta> g"
  shows "\<exists>l. plus l \<circ> f \<circ> of_int = g \<circ> of_int"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. (+) l \<circ> f \<circ> of_int = g \<circ> of_int
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l. (+) l \<circ> f \<circ> of_int = g \<circ> of_int
[PROOF STEP]
let ?F = "\<lambda>k. f (of_int k)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l. (+) l \<circ> f \<circ> of_int = g \<circ> of_int
[PROOF STEP]
let ?G = "\<lambda>k. g (of_int k)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l. (+) l \<circ> f \<circ> of_int = g \<circ> of_int
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<Delta> f = \<Delta> g
[PROOF STEP]
have "\<And>k. \<Delta> f (of_int k) = \<Delta> g (of_int k)"
[PROOF STATE]
proof (prove)
using this:
\<Delta> f = \<Delta> g

goal (1 subgoal):
 1. \<And>k. \<Delta> f (of_int k) = \<Delta> g (of_int k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Delta> f (of_int ?k) = \<Delta> g (of_int ?k)

goal (1 subgoal):
 1. \<exists>l. (+) l \<circ> f \<circ> of_int = g \<circ> of_int
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Delta> f (of_int ?k) = \<Delta> g (of_int ?k)
[PROOF STEP]
have k_incr: "\<And>k. ?F (k + 1) - ?G (k + 1) = ?F k - ?G k"
[PROOF STATE]
proof (prove)
using this:
\<Delta> f (of_int ?k) = \<Delta> g (of_int ?k)

goal (1 subgoal):
 1. \<And>k. f (of_int (k + 1)) - g (of_int (k + 1)) = f (of_int k) - g (of_int k)
[PROOF STEP]
by (simp add: \<Delta>_def algebra_simps)
[PROOF STATE]
proof (state)
this:
f (of_int (?k + 1)) - g (of_int (?k + 1)) = f (of_int ?k) - g (of_int ?k)

goal (1 subgoal):
 1. \<exists>l. (+) l \<circ> f \<circ> of_int = g \<circ> of_int
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f (of_int (?k + 1)) - g (of_int (?k + 1)) = f (of_int ?k) - g (of_int ?k)
[PROOF STEP]
have "\<And>k. ?F ((k - 1) + 1) - ?G ((k - 1) + 1) =
    ?F (k - 1) - ?G (k - 1)"
[PROOF STATE]
proof (prove)
using this:
f (of_int (?k + 1)) - g (of_int (?k + 1)) = f (of_int ?k) - g (of_int ?k)

goal (1 subgoal):
 1. \<And>k. f (of_int (k - 1 + 1)) - g (of_int (k - 1 + 1)) = f (of_int (k - 1)) - g (of_int (k - 1))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f (of_int (?k - 1 + 1)) - g (of_int (?k - 1 + 1)) = f (of_int (?k - 1)) - g (of_int (?k - 1))

goal (1 subgoal):
 1. \<exists>l. (+) l \<circ> f \<circ> of_int = g \<circ> of_int
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f (of_int (?k - 1 + 1)) - g (of_int (?k - 1 + 1)) = f (of_int (?k - 1)) - g (of_int (?k - 1))
[PROOF STEP]
have k_decr: "\<And>k. ?F (k - 1) - ?G (k - 1) = ?F k - ?G k"
[PROOF STATE]
proof (prove)
using this:
f (of_int (?k - 1 + 1)) - g (of_int (?k - 1 + 1)) = f (of_int (?k - 1)) - g (of_int (?k - 1))

goal (1 subgoal):
 1. \<And>k. f (of_int (k - 1)) - g (of_int (k - 1)) = f (of_int k) - g (of_int k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (of_int (?k - 1)) - g (of_int (?k - 1)) = f (of_int ?k) - g (of_int ?k)

goal (1 subgoal):
 1. \<exists>l. (+) l \<circ> f \<circ> of_int = g \<circ> of_int
[PROOF STEP]
have "\<And>k. ?F k - ?G k = ?F 0 - ?G 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. f (of_int k) - g (of_int k) = f (of_int 0) - g (of_int 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. f (of_int k) - g (of_int k) = f (of_int 0) - g (of_int 0)
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. f (of_int k) - g (of_int k) = f (of_int 0) - g (of_int 0)
[PROOF STEP]
show "?F k - ?G k = ?F 0 - ?G 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (of_int k) - g (of_int k) = f (of_int 0) - g (of_int 0)
[PROOF STEP]
by (induct k rule: int_induct)
        (simp_all add: k_incr k_decr del: of_int_add of_int_diff of_int_0)
[PROOF STATE]
proof (state)
this:
f (of_int k) - g (of_int k) = f (of_int 0) - g (of_int 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f (of_int ?k) - g (of_int ?k) = f (of_int 0) - g (of_int 0)

goal (1 subgoal):
 1. \<exists>l. (+) l \<circ> f \<circ> of_int = g \<circ> of_int
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f (of_int ?k) - g (of_int ?k) = f (of_int 0) - g (of_int 0)
[PROOF STEP]
have "\<And>k. (plus (?G 0 - ?F 0) \<circ> ?F) k = ?G k"
[PROOF STATE]
proof (prove)
using this:
f (of_int ?k) - g (of_int ?k) = f (of_int 0) - g (of_int 0)

goal (1 subgoal):
 1. \<And>k. ((+) (g (of_int 0) - f (of_int 0)) \<circ> (\<lambda>k. f (of_int k))) k = g (of_int k)
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
((+) (g (of_int 0) - f (of_int 0)) \<circ> (\<lambda>k. f (of_int k))) ?k = g (of_int ?k)

goal (1 subgoal):
 1. \<exists>l. (+) l \<circ> f \<circ> of_int = g \<circ> of_int
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((+) (g (of_int 0) - f (of_int 0)) \<circ> (\<lambda>k. f (of_int k))) ?k = g (of_int ?k)
[PROOF STEP]
have "plus (?G 0 - ?F 0) \<circ> ?F = ?G"
[PROOF STATE]
proof (prove)
using this:
((+) (g (of_int 0) - f (of_int 0)) \<circ> (\<lambda>k. f (of_int k))) ?k = g (of_int ?k)

goal (1 subgoal):
 1. (+) (g (of_int 0) - f (of_int 0)) \<circ> (\<lambda>k. f (of_int k)) = (\<lambda>k. g (of_int k))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(+) (g (of_int 0) - f (of_int 0)) \<circ> (\<lambda>k. f (of_int k)) = (\<lambda>k. g (of_int k))

goal (1 subgoal):
 1. \<exists>l. (+) l \<circ> f \<circ> of_int = g \<circ> of_int
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(+) (g (of_int 0) - f (of_int 0)) \<circ> (\<lambda>k. f (of_int k)) = (\<lambda>k. g (of_int k))
[PROOF STEP]
have "plus (?G 0 - ?F 0) \<circ> f \<circ> of_int = g \<circ> of_int"
[PROOF STATE]
proof (prove)
using this:
(+) (g (of_int 0) - f (of_int 0)) \<circ> (\<lambda>k. f (of_int k)) = (\<lambda>k. g (of_int k))

goal (1 subgoal):
 1. (+) (g (of_int 0) - f (of_int 0)) \<circ> f \<circ> of_int = g \<circ> of_int
[PROOF STEP]
by (simp only: comp_def)
[PROOF STATE]
proof (state)
this:
(+) (g (of_int 0) - f (of_int 0)) \<circ> f \<circ> of_int = g \<circ> of_int

goal (1 subgoal):
 1. \<exists>l. (+) l \<circ> f \<circ> of_int = g \<circ> of_int
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(+) (g (of_int 0) - f (of_int 0)) \<circ> f \<circ> of_int = g \<circ> of_int
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(+) (g (of_int 0) - f (of_int 0)) \<circ> f \<circ> of_int = g \<circ> of_int

goal (1 subgoal):
 1. \<exists>l. (+) l \<circ> f \<circ> of_int = g \<circ> of_int
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>l. (+) l \<circ> f \<circ> of_int = g \<circ> of_int

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<Delta>_add:
  "\<Delta> (\<lambda>k. f k + g k) k = \<Delta> f k + \<Delta> g k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta> (\<lambda>k. f k + g k) k = \<Delta> f k + \<Delta> g k
[PROOF STEP]
by (simp add: \<Delta>_def)


[STATEMENT]
lemma \<Delta>_factor:
  "\<Delta> (\<lambda>k. c * k) k = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta> ((*) c) k = c
[PROOF STEP]
by (simp add: \<Delta>_def algebra_simps)


[STATEMENT]
lemma \<Sigma>_same [simp]:
  "\<Sigma> f j j = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sigma> f j j = (0::'a)
[PROOF STEP]
by (simp add: \<Sigma>_def)


[STATEMENT]
lemma \<Sigma>_positive:
  "j < l \<Longrightarrow> \<Sigma> f j l = sum (f \<circ> of_int) {j..<l}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < l \<Longrightarrow> \<Sigma> f j l = sum (f \<circ> of_int) {j..<l}
[PROOF STEP]
by (simp add: \<Sigma>_def)


[STATEMENT]
lemma \<Sigma>_negative:
  "j > l \<Longrightarrow> \<Sigma> f j l = - \<Sigma> f l j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l < j \<Longrightarrow> \<Sigma> f j l = - \<Sigma> f l j
[PROOF STEP]
by (simp add: \<Sigma>_def)


[STATEMENT]
lemma \<Sigma>_comp_of_int:
  "\<Sigma> (f \<circ> of_int) = \<Sigma> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sigma> (f \<circ> of_int) = \<Sigma> f
[PROOF STEP]
by (simp add: \<Sigma>_def fun_eq_iff)


[STATEMENT]
lemma \<Sigma>_const:
  "\<Sigma> (\<lambda>k. c) j l = of_int (l - j) * c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sigma> (\<lambda>k. c) j l = of_int (l - j) * c
[PROOF STEP]
by (simp add: \<Sigma>_def algebra_simps)


[STATEMENT]
lemma \<Sigma>_add:
  "\<Sigma> (\<lambda>k. f k + g k) j l = \<Sigma> f j l + \<Sigma> g j l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sigma> (\<lambda>k. f k + g k) j l = \<Sigma> f j l + \<Sigma> g j l
[PROOF STEP]
by (simp add: \<Sigma>_def sum.distrib)


[STATEMENT]
lemma \<Sigma>_factor:
  "\<Sigma> (\<lambda>k. c * f k) j l = (c::'a::ring) * \<Sigma> (\<lambda>k. f k) j l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sigma> (\<lambda>k. c * f k) j l = c * \<Sigma> f j l
[PROOF STEP]
by (simp add: \<Sigma>_def sum_distrib_left)


[STATEMENT]
lemma \<Sigma>_concat:
  "\<Sigma> f j k + \<Sigma> f k l = \<Sigma> f j l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sigma> f j k + \<Sigma> f k l = \<Sigma> f j l
[PROOF STEP]
by (simp add: \<Sigma>_def algebra_simps add_sum_int)
    (simp_all add: add_sum_orient [of "\<lambda>k. f (of_int k)" k j l]
      add_sum_orient [of "\<lambda>k. f (of_int k)" j l k]
      add_sum_orient [of "\<lambda>k. f (of_int k)" j k l] add_sum_int)


[STATEMENT]
lemma \<Sigma>_incr_upper:
  "\<Sigma> f j (l + 1) = \<Sigma> f j l + f (of_int l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sigma> f j (l + 1) = \<Sigma> f j l + f (of_int l)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Sigma> f j (l + 1) = \<Sigma> f j l + f (of_int l)
[PROOF STEP]
have "{l..<l+1} = {l}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {l..<l + 1} = {l}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{l..<l + 1} = {l}

goal (1 subgoal):
 1. \<Sigma> f j (l + 1) = \<Sigma> f j l + f (of_int l)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{l..<l + 1} = {l}
[PROOF STEP]
have "\<Sigma> f l (l + 1) = f (of_int l)"
[PROOF STATE]
proof (prove)
using this:
{l..<l + 1} = {l}

goal (1 subgoal):
 1. \<Sigma> f l (l + 1) = f (of_int l)
[PROOF STEP]
by (simp add: \<Sigma>_def)
[PROOF STATE]
proof (state)
this:
\<Sigma> f l (l + 1) = f (of_int l)

goal (1 subgoal):
 1. \<Sigma> f j (l + 1) = \<Sigma> f j l + f (of_int l)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Sigma> f l (l + 1) = f (of_int l)

goal (1 subgoal):
 1. \<Sigma> f j (l + 1) = \<Sigma> f j l + f (of_int l)
[PROOF STEP]
have "\<Sigma> f j (l + 1) = \<Sigma> f j l + \<Sigma> f l (l + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sigma> f j (l + 1) = \<Sigma> f j l + \<Sigma> f l (l + 1)
[PROOF STEP]
by (simp add: \<Sigma>_concat)
[PROOF STATE]
proof (state)
this:
\<Sigma> f j (l + 1) = \<Sigma> f j l + \<Sigma> f l (l + 1)

goal (1 subgoal):
 1. \<Sigma> f j (l + 1) = \<Sigma> f j l + f (of_int l)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Sigma> f l (l + 1) = f (of_int l)
\<Sigma> f j (l + 1) = \<Sigma> f j l + \<Sigma> f l (l + 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Sigma> f l (l + 1) = f (of_int l)
\<Sigma> f j (l + 1) = \<Sigma> f j l + \<Sigma> f l (l + 1)

goal (1 subgoal):
 1. \<Sigma> f j (l + 1) = \<Sigma> f j l + f (of_int l)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Sigma> f j (l + 1) = \<Sigma> f j l + f (of_int l)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<Delta>_\<Sigma>:
  "\<Delta> (\<Sigma> f j) = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta> (\<Sigma> f j) = f
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<Delta> (\<Sigma> f j) x = f x
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<Delta> (\<Sigma> f j) x = f x
[PROOF STEP]
show "\<Delta> (\<Sigma> f j) k = f k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta> (\<Sigma> f j) k = f k
[PROOF STEP]
by (simp add: \<Delta>_def \<Sigma>_incr_upper)
[PROOF STATE]
proof (state)
this:
\<Delta> (\<Sigma> f j) k = f k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<Sigma>_\<Delta>:
  "\<Sigma> (\<Delta> f) j l = f (of_int l) - f (of_int j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sigma> (\<Delta> f) j l = f (of_int l) - f (of_int j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Sigma> (\<Delta> f) j l = f (of_int l) - f (of_int j)
[PROOF STEP]
from \<Delta>_\<Sigma>
[PROOF STATE]
proof (chain)
picking this:
\<Delta> (\<Sigma> ?f ?j) = ?f
[PROOF STEP]
have "\<Delta> (\<Sigma> (\<Delta> f) j) = \<Delta> f"
[PROOF STATE]
proof (prove)
using this:
\<Delta> (\<Sigma> ?f ?j) = ?f

goal (1 subgoal):
 1. \<Delta> (\<Sigma> (\<Delta> f) j) = \<Delta> f
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Delta> (\<Sigma> (\<Delta> f) j) = \<Delta> f

goal (1 subgoal):
 1. \<Sigma> (\<Delta> f) j l = f (of_int l) - f (of_int j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Delta> (\<Sigma> (\<Delta> f) j) = \<Delta> f
[PROOF STEP]
obtain k where "plus k \<circ> \<Sigma> (\<Delta> f) j \<circ> of_int = f \<circ> of_int"
[PROOF STATE]
proof (prove)
using this:
\<Delta> (\<Sigma> (\<Delta> f) j) = \<Delta> f

goal (1 subgoal):
 1. (\<And>k. (+) k \<circ> \<Sigma> (\<Delta> f) j \<circ> of_int = f \<circ> of_int \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (blast dest: \<Delta>_same_shift)
[PROOF STATE]
proof (state)
this:
(+) k \<circ> \<Sigma> (\<Delta> f) j \<circ> of_int = f \<circ> of_int

goal (1 subgoal):
 1. \<Sigma> (\<Delta> f) j l = f (of_int l) - f (of_int j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(+) k \<circ> \<Sigma> (\<Delta> f) j \<circ> of_int = f \<circ> of_int
[PROOF STEP]
have "\<And>q. f (of_int q) = k + \<Sigma> (\<Delta> f) j q"
[PROOF STATE]
proof (prove)
using this:
(+) k \<circ> \<Sigma> (\<Delta> f) j \<circ> of_int = f \<circ> of_int

goal (1 subgoal):
 1. \<And>q. f (of_int q) = k + \<Sigma> (\<Delta> f) j q
[PROOF STEP]
by (simp add: fun_eq_iff)
[PROOF STATE]
proof (state)
this:
f (of_int ?q) = k + \<Sigma> (\<Delta> f) j ?q

goal (1 subgoal):
 1. \<Sigma> (\<Delta> f) j l = f (of_int l) - f (of_int j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f (of_int ?q) = k + \<Sigma> (\<Delta> f) j ?q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f (of_int ?q) = k + \<Sigma> (\<Delta> f) j ?q

goal (1 subgoal):
 1. \<Sigma> (\<Delta> f) j l = f (of_int l) - f (of_int j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Sigma> (\<Delta> f) j l = f (of_int l) - f (of_int j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_R [forward]: "c \<noteq> R \<Longrightarrow> c = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<noteq> R \<Longrightarrow> c = B
[PROOF STEP]
using color.exhaust
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y = R \<Longrightarrow> ?P; ?y = B \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. c \<noteq> R \<Longrightarrow> c = B
[PROOF STEP]
by blast


[STATEMENT]
lemma not_B [forward]: "c \<noteq> B \<Longrightarrow> c = R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<noteq> B \<Longrightarrow> c = R
[PROOF STEP]
using color.exhaust
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y = R \<Longrightarrow> ?P; ?y = B \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. c \<noteq> B \<Longrightarrow> c = R
[PROOF STEP]
by blast


[STATEMENT]
lemma red_not_leaf [forward]: "cl t = R \<Longrightarrow> t \<noteq> Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl t = R \<Longrightarrow> t \<noteq> Leaf
[PROOF STEP]
by auto


[STATEMENT]
lemma cl_invI: "cl_inv l \<Longrightarrow> cl_inv r \<Longrightarrow> cl_inv (Node l B k v r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv l; cl_inv r\<rbrakk> \<Longrightarrow> cl_inv (Node l B k v r)
[PROOF STEP]
by auto2


[STATEMENT]
lemma bd_invI: "bd_inv l \<Longrightarrow> bd_inv r \<Longrightarrow> black_depth l = black_depth r \<Longrightarrow> bd_inv (Node l c k v r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv l; bd_inv r; black_depth l = black_depth r\<rbrakk> \<Longrightarrow> bd_inv (Node l c k v r)
[PROOF STEP]
by auto2


[STATEMENT]
lemma is_rbt_rec [forward]: "is_rbt (Node l c k v r) \<Longrightarrow> is_rbt l \<and> is_rbt r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt (Node l c k v r) \<Longrightarrow> is_rbt l \<and> is_rbt r
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt (Node l c k v r) \<Longrightarrow> is_rbt l \<and> is_rbt r
[PROOF STEP]
@case "c = R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt (Node l c k v r) \<Longrightarrow> is_rbt l \<and> is_rbt r
[PROOF STEP]
@qed


[STATEMENT]
lemma two_distrib [rewrite]: "(2::nat) * (a + 1) = 2 * a + 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * (a + 1) = 2 * a + 2
[PROOF STEP]
by simp


[STATEMENT]
theorem rbt_balanced: "is_rbt t \<Longrightarrow> max_depth t \<le> 2 * min_depth t + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt t \<Longrightarrow> max_depth t \<le> 2 * min_depth t + 1
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt t \<Longrightarrow> max_depth t \<le> 2 * min_depth t + 1
[PROOF STEP]
@induct t for "is_rbt t \<longrightarrow> black_depth t \<le> min_depth t" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt t \<Longrightarrow> max_depth t \<le> 2 * min_depth t + 1
[PROOF STEP]
@subgoal "t = Node l c k v r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt t \<Longrightarrow> max_depth t \<le> 2 * min_depth t + 1
[PROOF STEP]
@case "c = R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt t \<Longrightarrow> max_depth t \<le> 2 * min_depth t + 1
[PROOF STEP]
@endgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt t \<Longrightarrow> max_depth t \<le> 2 * min_depth t + 1
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt t \<Longrightarrow> max_depth t \<le> 2 * min_depth t + 1
[PROOF STEP]
@induct t for "is_rbt t \<longrightarrow> (if cl t = R then max_depth t \<le> 2 * black_depth t + 1
                               else max_depth t \<le> 2 * black_depth t)" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt t \<Longrightarrow> max_depth t \<le> 2 * min_depth t + 1
[PROOF STEP]
@subgoal "t = Node l c k v r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt t \<Longrightarrow> max_depth t \<le> 2 * min_depth t + 1
[PROOF STEP]
@case "c = R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt t \<Longrightarrow> max_depth t \<le> 2 * min_depth t + 1
[PROOF STEP]
@endgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt t \<Longrightarrow> max_depth t \<le> 2 * min_depth t + 1
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt t \<Longrightarrow> max_depth t \<le> 2 * min_depth t + 1
[PROOF STEP]
@have "max_depth t \<le> 2 * black_depth t + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt t \<Longrightarrow> max_depth t \<le> 2 * min_depth t + 1
[PROOF STEP]
@qed


[STATEMENT]
lemma cl_inv'B [forward, backward1]:
  "cl_inv' t \<Longrightarrow> cl t = B \<Longrightarrow> cl_inv t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv' t; cl t = B\<rbrakk> \<Longrightarrow> cl_inv t
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv' t; cl t = B\<rbrakk> \<Longrightarrow> cl_inv t
[PROOF STEP]
@case "t = Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv' t; cl t = B\<rbrakk> \<Longrightarrow> cl_inv t
[PROOF STEP]
@qed


[STATEMENT]
lemma cl_inv'R [forward]:
  "cl_inv' (Node l R k v r) \<Longrightarrow> cl l = B \<Longrightarrow> cl r = B \<Longrightarrow> cl_inv (Node l R k v r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv' (Node l R k v r); cl l = B; cl r = B\<rbrakk> \<Longrightarrow> cl_inv (Node l R k v r)
[PROOF STEP]
by auto2


[STATEMENT]
lemma cl_inv_to_cl_inv' [forward]: "cl_inv t \<Longrightarrow> cl_inv' t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_inv t \<Longrightarrow> cl_inv' t
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_inv t \<Longrightarrow> cl_inv' t
[PROOF STEP]
@case "t = Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_inv t \<Longrightarrow> cl_inv' t
[PROOF STEP]
@case "cl t = R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_inv t \<Longrightarrow> cl_inv' t
[PROOF STEP]
@qed


[STATEMENT]
lemma cl_inv'I [forward_arg]:
  "cl_inv l \<Longrightarrow> cl_inv r \<Longrightarrow> cl_inv' (Node l c k v r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv l; cl_inv r\<rbrakk> \<Longrightarrow> cl_inv' (Node l c k v r)
[PROOF STEP]
by auto


[STATEMENT]
lemma rbt_in_traverse_fst [rewrite]: "map fst (rbt_in_traverse_pairs t) = rbt_in_traverse t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map fst (rbt_in_traverse_pairs t) = rbt_in_traverse t
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map fst (rbt_in_traverse_pairs t) = rbt_in_traverse t
[PROOF STEP]
@induct t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map fst (rbt_in_traverse_pairs t) = rbt_in_traverse t
[PROOF STEP]
@qed


[STATEMENT]
lemma rbt_sorted_lr [forward]:
  "rbt_sorted (Node l c k v r) \<Longrightarrow> rbt_sorted l \<and> rbt_sorted r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_sorted (Node l c k v r) \<Longrightarrow> rbt_sorted l \<and> rbt_sorted r
[PROOF STEP]
by auto2


[STATEMENT]
lemma rbt_inorder_preserve_set [rewrite]:
  "rbt_set t = set (rbt_in_traverse t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_set t = set (rbt_in_traverse t)
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_set t = set (rbt_in_traverse t)
[PROOF STEP]
@induct t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_set t = set (rbt_in_traverse t)
[PROOF STEP]
@qed


[STATEMENT]
lemma rbt_inorder_sorted [rewrite]:
  "rbt_sorted t \<longleftrightarrow> strict_sorted (map fst (rbt_in_traverse_pairs t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_sorted t = strict_sorted (map fst (rbt_in_traverse_pairs t))
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_sorted t = strict_sorted (map fst (rbt_in_traverse_pairs t))
[PROOF STEP]
@induct t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_sorted t = strict_sorted (map fst (rbt_in_traverse_pairs t))
[PROOF STEP]
@qed


[STATEMENT]
lemma balance_non_Leaf [resolve]: "balance l k v r \<noteq> Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. balance l k v r \<noteq> Leaf
[PROOF STEP]
by auto2


[STATEMENT]
lemma balance_bdinv [forward_arg]:
  "bd_inv l \<Longrightarrow> bd_inv r \<Longrightarrow> black_depth l = black_depth r \<Longrightarrow> bd_inv (balance l k v r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv l; bd_inv r; black_depth l = black_depth r\<rbrakk> \<Longrightarrow> bd_inv (balance l k v r)
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv l; bd_inv r; black_depth l = black_depth r\<rbrakk> \<Longrightarrow> bd_inv (balance l k v r)
[PROOF STEP]
@have "bd_inv (balanceR l k v r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv l; bd_inv r; black_depth l = black_depth r\<rbrakk> \<Longrightarrow> bd_inv (balance l k v r)
[PROOF STEP]
@qed


[STATEMENT]
lemma balance_bd [rewrite]:
  "bd_inv l \<Longrightarrow> bd_inv r \<Longrightarrow> black_depth l = black_depth r \<Longrightarrow>
   black_depth (balance l k v r) = black_depth l + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv l; bd_inv r; black_depth l = black_depth r\<rbrakk> \<Longrightarrow> black_depth (balance l k v r) = black_depth l + 1
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv l; bd_inv r; black_depth l = black_depth r\<rbrakk> \<Longrightarrow> black_depth (balance l k v r) = black_depth l + 1
[PROOF STEP]
@have "black_depth (balanceR l k v r) = black_depth l + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv l; bd_inv r; black_depth l = black_depth r\<rbrakk> \<Longrightarrow> black_depth (balance l k v r) = black_depth l + 1
[PROOF STEP]
@qed


[STATEMENT]
lemma balance_cl1 [forward]:
  "cl_inv' l \<Longrightarrow> cl_inv r \<Longrightarrow> cl_inv (balance l k v r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv' l; cl_inv r\<rbrakk> \<Longrightarrow> cl_inv (balance l k v r)
[PROOF STEP]
by auto2


[STATEMENT]
lemma balance_cl2 [forward]:
  "cl_inv l \<Longrightarrow> cl_inv' r \<Longrightarrow> cl_inv (balance l k v r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv l; cl_inv' r\<rbrakk> \<Longrightarrow> cl_inv (balance l k v r)
[PROOF STEP]
by auto2


[STATEMENT]
lemma balanceR_inorder_pairs [rewrite]:
  "rbt_in_traverse_pairs (balanceR l k v r) = rbt_in_traverse_pairs l @ (k, v) # rbt_in_traverse_pairs r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (balanceR l k v r) = rbt_in_traverse_pairs l @ (k, v) # rbt_in_traverse_pairs r
[PROOF STEP]
by auto2


[STATEMENT]
lemma balance_inorder_pairs [rewrite]:
  "rbt_in_traverse_pairs (balance l k v r) = rbt_in_traverse_pairs l @ (k, v) # rbt_in_traverse_pairs r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (balance l k v r) = rbt_in_traverse_pairs l @ (k, v) # rbt_in_traverse_pairs r
[PROOF STEP]
by auto2


[STATEMENT]
lemma ins_non_Leaf [resolve]: "ins x v t \<noteq> Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ins x v t \<noteq> Leaf
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ins x v t \<noteq> Leaf
[PROOF STEP]
@case "t = Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ins x v t \<noteq> Leaf
[PROOF STEP]
@qed


[STATEMENT]
lemma cl_inv_ins [forward]:
  "cl_inv t \<Longrightarrow> cl_inv' (ins x v t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_inv t \<Longrightarrow> cl_inv' (ins x v t)
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_inv t \<Longrightarrow> cl_inv' (ins x v t)
[PROOF STEP]
@induct t for "cl_inv t \<longrightarrow> (if cl t = B then cl_inv (ins x v t) else cl_inv' (ins x v t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_inv t \<Longrightarrow> cl_inv' (ins x v t)
[PROOF STEP]
@qed


[STATEMENT]
lemma bd_inv_ins:
  "bd_inv t \<Longrightarrow> bd_inv (ins x v t) \<and> black_depth t = black_depth (ins x v t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bd_inv t \<Longrightarrow> bd_inv (ins x v t) \<and> black_depth t = black_depth (ins x v t)
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bd_inv t \<Longrightarrow> bd_inv (ins x v t) \<and> black_depth t = black_depth (ins x v t)
[PROOF STEP]
@induct t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bd_inv t \<Longrightarrow> bd_inv (ins x v t) \<and> black_depth t = black_depth (ins x v t)
[PROOF STEP]
@qed


[STATEMENT]
lemma ins_inorder_pairs [rewrite]:
  "rbt_sorted t \<Longrightarrow> rbt_in_traverse_pairs (ins x v t) = ordered_insert_pairs x v (rbt_in_traverse_pairs t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_sorted t \<Longrightarrow> rbt_in_traverse_pairs (ins x v t) = ordered_insert_pairs x v (rbt_in_traverse_pairs t)
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_sorted t \<Longrightarrow> rbt_in_traverse_pairs (ins x v t) = ordered_insert_pairs x v (rbt_in_traverse_pairs t)
[PROOF STEP]
@induct t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_sorted t \<Longrightarrow> rbt_in_traverse_pairs (ins x v t) = ordered_insert_pairs x v (rbt_in_traverse_pairs t)
[PROOF STEP]
@qed


[STATEMENT]
lemma paint_cl_inv' [forward]: "cl_inv' t \<Longrightarrow> cl_inv' (paint c t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_inv' t \<Longrightarrow> cl_inv' (paint c t)
[PROOF STEP]
by auto2


[STATEMENT]
lemma paint_bd_inv [forward]: "bd_inv t \<Longrightarrow> bd_inv (paint c t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bd_inv t \<Longrightarrow> bd_inv (paint c t)
[PROOF STEP]
by auto2


[STATEMENT]
lemma paint_bd [rewrite]:
  "bd_inv t \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> cl t = B \<Longrightarrow> black_depth (paint R t) = black_depth t - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv t; t \<noteq> Leaf; cl t = B\<rbrakk> \<Longrightarrow> black_depth (paint R t) = black_depth t - 1
[PROOF STEP]
by auto2


[STATEMENT]
lemma paint_in_traverse_pairs [rewrite]:
  "rbt_in_traverse_pairs (paint c t) = rbt_in_traverse_pairs t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (paint c t) = rbt_in_traverse_pairs t
[PROOF STEP]
by auto2


[STATEMENT]
theorem insert_is_rbt [forward]:
  "is_rbt t \<Longrightarrow> is_rbt (rbt_insert x v t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt t \<Longrightarrow> is_rbt (rbt_insert x v t)
[PROOF STEP]
by auto2


[STATEMENT]
theorem insert_sorted [forward]:
  "rbt_sorted t \<Longrightarrow> rbt_sorted (rbt_insert x v t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_sorted t \<Longrightarrow> rbt_sorted (rbt_insert x v t)
[PROOF STEP]
by auto2


[STATEMENT]
theorem insert_rbt_map [rewrite]:
  "rbt_sorted t \<Longrightarrow> rbt_map (rbt_insert x v t) = (rbt_map t) {x \<rightarrow> v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_sorted t \<Longrightarrow> rbt_map (rbt_insert x v t) =  rbt_map t { x \<rightarrow> v }
[PROOF STEP]
by auto2


[STATEMENT]
theorem rbt_search_correct [rewrite]:
  "rbt_sorted t \<Longrightarrow> rbt_search t x = (rbt_map t)\<langle>x\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_sorted t \<Longrightarrow> rbt_search t x = rbt_map t\<langle>x\<rangle>
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_sorted t \<Longrightarrow> rbt_search t x = rbt_map t\<langle>x\<rangle>
[PROOF STEP]
@induct t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_sorted t \<Longrightarrow> rbt_search t x = rbt_map t\<langle>x\<rangle>
[PROOF STEP]
@qed


[STATEMENT]
lemma balL_bd [forward_arg]:
  "bd_inv l \<Longrightarrow> bd_inv r \<Longrightarrow> cl r = B \<Longrightarrow> black_depth l + 1 = black_depth r \<Longrightarrow>
   bd_inv (balL l k v r) \<and> black_depth (balL l k v r) = black_depth l + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv l; bd_inv r; cl r = B; black_depth l + 1 = black_depth r\<rbrakk> \<Longrightarrow> bd_inv (balL l k v r) \<and> black_depth (balL l k v r) = black_depth l + 1
[PROOF STEP]
by auto2


[STATEMENT]
lemma balL_bd' [forward_arg]:
  "bd_inv l \<Longrightarrow> bd_inv r \<Longrightarrow> cl_inv r \<Longrightarrow> black_depth l + 1 = black_depth r \<Longrightarrow>
   bd_inv (balL l k v r) \<and> black_depth (balL l k v r) = black_depth l + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv l; bd_inv r; cl_inv r; black_depth l + 1 = black_depth r\<rbrakk> \<Longrightarrow> bd_inv (balL l k v r) \<and> black_depth (balL l k v r) = black_depth l + 1
[PROOF STEP]
by auto2


[STATEMENT]
lemma balL_cl [forward_arg]:
  "cl_inv' l \<Longrightarrow> cl_inv r \<Longrightarrow> cl r = B \<Longrightarrow> cl_inv (balL l k v r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv' l; cl_inv r; cl r = B\<rbrakk> \<Longrightarrow> cl_inv (balL l k v r)
[PROOF STEP]
by auto2


[STATEMENT]
lemma balL_cl' [forward]:
  "cl_inv' l \<Longrightarrow> cl_inv r \<Longrightarrow> cl_inv' (balL l k v r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv' l; cl_inv r\<rbrakk> \<Longrightarrow> cl_inv' (balL l k v r)
[PROOF STEP]
by auto2


[STATEMENT]
lemma balR_bd [forward_arg]:
  "bd_inv l \<Longrightarrow> bd_inv r \<Longrightarrow> cl_inv l \<Longrightarrow> black_depth l = black_depth r + 1 \<Longrightarrow>
   bd_inv (balR l k v r) \<and> black_depth (balR l k v r) = black_depth l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv l; bd_inv r; cl_inv l; black_depth l = black_depth r + 1\<rbrakk> \<Longrightarrow> bd_inv (balR l k v r) \<and> black_depth (balR l k v r) = black_depth l
[PROOF STEP]
by auto2


[STATEMENT]
lemma balR_cl [forward_arg]:
  "cl_inv l \<Longrightarrow> cl_inv' r \<Longrightarrow> cl l = B \<Longrightarrow> cl_inv (balR l k v r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv l; cl_inv' r; cl l = B\<rbrakk> \<Longrightarrow> cl_inv (balR l k v r)
[PROOF STEP]
by auto2


[STATEMENT]
lemma balR_cl' [forward]:
  "cl_inv l \<Longrightarrow> cl_inv' r \<Longrightarrow> cl_inv' (balR l k v r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv l; cl_inv' r\<rbrakk> \<Longrightarrow> cl_inv' (balR l k v r)
[PROOF STEP]
by auto2


[STATEMENT]
lemma balL_in_traverse_pairs [rewrite]:
  "rbt_in_traverse_pairs (balL l k v r) = rbt_in_traverse_pairs l @ (k, v) # rbt_in_traverse_pairs r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (balL l k v r) = rbt_in_traverse_pairs l @ (k, v) # rbt_in_traverse_pairs r
[PROOF STEP]
by auto2


[STATEMENT]
lemma balR_in_traverse_pairs [rewrite]:
  "rbt_in_traverse_pairs (balR l k v r) = rbt_in_traverse_pairs l @ (k, v) # rbt_in_traverse_pairs r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (balR l k v r) = rbt_in_traverse_pairs l @ (k, v) # rbt_in_traverse_pairs r
[PROOF STEP]
by auto2


[STATEMENT]
lemma combine_bd [forward_arg]:
  "bd_inv lt \<Longrightarrow> bd_inv rt \<Longrightarrow> black_depth lt = black_depth rt \<Longrightarrow>
   bd_inv (combine lt rt) \<and> black_depth (combine lt rt) = black_depth lt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv lt; bd_inv rt; black_depth lt = black_depth rt\<rbrakk> \<Longrightarrow> bd_inv (combine lt rt) \<and> black_depth (combine lt rt) = black_depth lt
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv lt; bd_inv rt; black_depth lt = black_depth rt\<rbrakk> \<Longrightarrow> bd_inv (combine lt rt) \<and> black_depth (combine lt rt) = black_depth lt
[PROOF STEP]
@fun_induct "combine lt rt" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv lt; bd_inv rt; black_depth lt = black_depth rt\<rbrakk> \<Longrightarrow> bd_inv (combine lt rt) \<and> black_depth (combine lt rt) = black_depth lt
[PROOF STEP]
@subgoal "(lt = Node l1 c1 k1 v1 r1, rt = Node l2 c2 k2 v2 r2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv lt; bd_inv rt; black_depth lt = black_depth rt\<rbrakk> \<Longrightarrow> bd_inv (combine lt rt) \<and> black_depth (combine lt rt) = black_depth lt
[PROOF STEP]
@unfold "combine (Node l1 c1 k1 v1 r1) (Node l2 c2 k2 v2 r2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv lt; bd_inv rt; black_depth lt = black_depth rt\<rbrakk> \<Longrightarrow> bd_inv (combine lt rt) \<and> black_depth (combine lt rt) = black_depth lt
[PROOF STEP]
@case "c1 = B" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv lt; bd_inv rt; black_depth lt = black_depth rt\<rbrakk> \<Longrightarrow> bd_inv (combine lt rt) \<and> black_depth (combine lt rt) = black_depth lt
[PROOF STEP]
@case "c2 = B" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv lt; bd_inv rt; black_depth lt = black_depth rt\<rbrakk> \<Longrightarrow> bd_inv (combine lt rt) \<and> black_depth (combine lt rt) = black_depth lt
[PROOF STEP]
@case "cl (combine r1 l2) = B" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv lt; bd_inv rt; black_depth lt = black_depth rt\<rbrakk> \<Longrightarrow> bd_inv (combine lt rt) \<and> black_depth (combine lt rt) = black_depth lt
[PROOF STEP]
@have "cl (Node (combine r1 l2) B k2 v2 r2) = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv lt; bd_inv rt; black_depth lt = black_depth rt\<rbrakk> \<Longrightarrow> bd_inv (combine lt rt) \<and> black_depth (combine lt rt) = black_depth lt
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv lt; bd_inv rt; black_depth lt = black_depth rt\<rbrakk> \<Longrightarrow> bd_inv (combine lt rt) \<and> black_depth (combine lt rt) = black_depth lt
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv lt; bd_inv rt; black_depth lt = black_depth rt\<rbrakk> \<Longrightarrow> bd_inv (combine lt rt) \<and> black_depth (combine lt rt) = black_depth lt
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv lt; bd_inv rt; black_depth lt = black_depth rt\<rbrakk> \<Longrightarrow> bd_inv (combine lt rt) \<and> black_depth (combine lt rt) = black_depth lt
[PROOF STEP]
@endgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv lt; bd_inv rt; black_depth lt = black_depth rt\<rbrakk> \<Longrightarrow> bd_inv (combine lt rt) \<and> black_depth (combine lt rt) = black_depth lt
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv lt; bd_inv rt; black_depth lt = black_depth rt\<rbrakk> \<Longrightarrow> bd_inv (combine lt rt) \<and> black_depth (combine lt rt) = black_depth lt
[PROOF STEP]
@qed


[STATEMENT]
lemma combine_cl:
  "cl_inv lt \<Longrightarrow> cl_inv rt \<Longrightarrow>
   (cl lt = B \<longrightarrow> cl rt = B \<longrightarrow> cl_inv (combine lt rt)) \<and> cl_inv' (combine lt rt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv lt; cl_inv rt\<rbrakk> \<Longrightarrow> (cl lt = B \<longrightarrow> cl rt = B \<longrightarrow> cl_inv (combine lt rt)) \<and> cl_inv' (combine lt rt)
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv lt; cl_inv rt\<rbrakk> \<Longrightarrow> (cl lt = B \<longrightarrow> cl rt = B \<longrightarrow> cl_inv (combine lt rt)) \<and> cl_inv' (combine lt rt)
[PROOF STEP]
@fun_induct "combine lt rt" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv lt; cl_inv rt\<rbrakk> \<Longrightarrow> (cl lt = B \<longrightarrow> cl rt = B \<longrightarrow> cl_inv (combine lt rt)) \<and> cl_inv' (combine lt rt)
[PROOF STEP]
@subgoal "(lt = Node l1 c1 k1 v1 r1, rt = Node l2 c2 k2 v2 r2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv lt; cl_inv rt\<rbrakk> \<Longrightarrow> (cl lt = B \<longrightarrow> cl rt = B \<longrightarrow> cl_inv (combine lt rt)) \<and> cl_inv' (combine lt rt)
[PROOF STEP]
@unfold "combine (Node l1 c1 k1 v1 r1) (Node l2 c2 k2 v2 r2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv lt; cl_inv rt\<rbrakk> \<Longrightarrow> (cl lt = B \<longrightarrow> cl rt = B \<longrightarrow> cl_inv (combine lt rt)) \<and> cl_inv' (combine lt rt)
[PROOF STEP]
@case "c1 = B" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv lt; cl_inv rt\<rbrakk> \<Longrightarrow> (cl lt = B \<longrightarrow> cl rt = B \<longrightarrow> cl_inv (combine lt rt)) \<and> cl_inv' (combine lt rt)
[PROOF STEP]
@case "c2 = B" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv lt; cl_inv rt\<rbrakk> \<Longrightarrow> (cl lt = B \<longrightarrow> cl rt = B \<longrightarrow> cl_inv (combine lt rt)) \<and> cl_inv' (combine lt rt)
[PROOF STEP]
@case "cl (combine r1 l2) = B" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv lt; cl_inv rt\<rbrakk> \<Longrightarrow> (cl lt = B \<longrightarrow> cl rt = B \<longrightarrow> cl_inv (combine lt rt)) \<and> cl_inv' (combine lt rt)
[PROOF STEP]
@have "cl (Node (combine r1 l2) B k2 v2 r2) = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv lt; cl_inv rt\<rbrakk> \<Longrightarrow> (cl lt = B \<longrightarrow> cl rt = B \<longrightarrow> cl_inv (combine lt rt)) \<and> cl_inv' (combine lt rt)
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv lt; cl_inv rt\<rbrakk> \<Longrightarrow> (cl lt = B \<longrightarrow> cl rt = B \<longrightarrow> cl_inv (combine lt rt)) \<and> cl_inv' (combine lt rt)
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv lt; cl_inv rt\<rbrakk> \<Longrightarrow> (cl lt = B \<longrightarrow> cl rt = B \<longrightarrow> cl_inv (combine lt rt)) \<and> cl_inv' (combine lt rt)
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv lt; cl_inv rt\<rbrakk> \<Longrightarrow> (cl lt = B \<longrightarrow> cl rt = B \<longrightarrow> cl_inv (combine lt rt)) \<and> cl_inv' (combine lt rt)
[PROOF STEP]
@endgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv lt; cl_inv rt\<rbrakk> \<Longrightarrow> (cl lt = B \<longrightarrow> cl rt = B \<longrightarrow> cl_inv (combine lt rt)) \<and> cl_inv' (combine lt rt)
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cl_inv lt; cl_inv rt\<rbrakk> \<Longrightarrow> (cl lt = B \<longrightarrow> cl rt = B \<longrightarrow> cl_inv (combine lt rt)) \<and> cl_inv' (combine lt rt)
[PROOF STEP]
@qed


[STATEMENT]
lemma combine_in_traverse_pairs [rewrite]:
  "rbt_in_traverse_pairs (combine lt rt) = rbt_in_traverse_pairs lt @ rbt_in_traverse_pairs rt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (combine lt rt) = rbt_in_traverse_pairs lt @ rbt_in_traverse_pairs rt
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (combine lt rt) = rbt_in_traverse_pairs lt @ rbt_in_traverse_pairs rt
[PROOF STEP]
@fun_induct "combine lt rt" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (combine lt rt) = rbt_in_traverse_pairs lt @ rbt_in_traverse_pairs rt
[PROOF STEP]
@subgoal "(lt = Node l1 c1 k1 v1 r1, rt = Node l2 c2 k2 v2 r2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (combine lt rt) = rbt_in_traverse_pairs lt @ rbt_in_traverse_pairs rt
[PROOF STEP]
@unfold "combine (Node l1 c1 k1 v1 r1) (Node l2 c2 k2 v2 r2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (combine lt rt) = rbt_in_traverse_pairs lt @ rbt_in_traverse_pairs rt
[PROOF STEP]
@case "c1 = R" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (combine lt rt) = rbt_in_traverse_pairs lt @ rbt_in_traverse_pairs rt
[PROOF STEP]
@case "c2 = R" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (combine lt rt) = rbt_in_traverse_pairs lt @ rbt_in_traverse_pairs rt
[PROOF STEP]
@case "cl (combine r1 l2) = R" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (combine lt rt) = rbt_in_traverse_pairs lt @ rbt_in_traverse_pairs rt
[PROOF STEP]
@have "rbt_in_traverse_pairs (combine (Node l1 c1 k1 v1 r1) (Node l2 c2 k2 v2 r2)) =
             rbt_in_traverse_pairs l1 @ (k1, v1) # rbt_in_traverse_pairs (combine r1 l2) @ (k2, v2) # rbt_in_traverse_pairs r2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (combine lt rt) = rbt_in_traverse_pairs lt @ rbt_in_traverse_pairs rt
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (combine lt rt) = rbt_in_traverse_pairs lt @ rbt_in_traverse_pairs rt
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (combine lt rt) = rbt_in_traverse_pairs lt @ rbt_in_traverse_pairs rt
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (combine lt rt) = rbt_in_traverse_pairs lt @ rbt_in_traverse_pairs rt
[PROOF STEP]
@case "c1 = B" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (combine lt rt) = rbt_in_traverse_pairs lt @ rbt_in_traverse_pairs rt
[PROOF STEP]
@case "c2 = B" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (combine lt rt) = rbt_in_traverse_pairs lt @ rbt_in_traverse_pairs rt
[PROOF STEP]
@case "cl (combine r1 l2) = R" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (combine lt rt) = rbt_in_traverse_pairs lt @ rbt_in_traverse_pairs rt
[PROOF STEP]
@have "rbt_in_traverse_pairs (combine (Node l1 c1 k1 v1 r1) (Node l2 c2 k2 v2 r2)) =
             rbt_in_traverse_pairs l1 @ (k1, v1) # rbt_in_traverse_pairs (combine r1 l2) @ (k2, v2) # rbt_in_traverse_pairs r2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (combine lt rt) = rbt_in_traverse_pairs lt @ rbt_in_traverse_pairs rt
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (combine lt rt) = rbt_in_traverse_pairs lt @ rbt_in_traverse_pairs rt
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (combine lt rt) = rbt_in_traverse_pairs lt @ rbt_in_traverse_pairs rt
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (combine lt rt) = rbt_in_traverse_pairs lt @ rbt_in_traverse_pairs rt
[PROOF STEP]
@endgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (combine lt rt) = rbt_in_traverse_pairs lt @ rbt_in_traverse_pairs rt
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_in_traverse_pairs (combine lt rt) = rbt_in_traverse_pairs lt @ rbt_in_traverse_pairs rt
[PROOF STEP]
@qed


[STATEMENT]
lemma del_bd [forward_arg]:
  "bd_inv t \<Longrightarrow> cl_inv t \<Longrightarrow> bd_inv (del x t) \<and> (
    if cl t = R then black_depth (del x t) = black_depth t
    else black_depth (del x t) = black_depth t - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv t; cl_inv t\<rbrakk> \<Longrightarrow> bd_inv (del x t) \<and> (if cl t = R then black_depth (del x t) = black_depth t else black_depth (del x t) = black_depth t - 1)
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv t; cl_inv t\<rbrakk> \<Longrightarrow> bd_inv (del x t) \<and> (if cl t = R then black_depth (del x t) = black_depth t else black_depth (del x t) = black_depth t - 1)
[PROOF STEP]
@induct t @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv t; cl_inv t\<rbrakk> \<Longrightarrow> bd_inv (del x t) \<and> (if cl t = R then black_depth (del x t) = black_depth t else black_depth (del x t) = black_depth t - 1)
[PROOF STEP]
@subgoal "t = Node l c k v r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv t; cl_inv t\<rbrakk> \<Longrightarrow> bd_inv (del x t) \<and> (if cl t = R then black_depth (del x t) = black_depth t else black_depth (del x t) = black_depth t - 1)
[PROOF STEP]
@unfold "del x (Node l c k v r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv t; cl_inv t\<rbrakk> \<Longrightarrow> bd_inv (del x t) \<and> (if cl t = R then black_depth (del x t) = black_depth t else black_depth (del x t) = black_depth t - 1)
[PROOF STEP]
@case "x = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv t; cl_inv t\<rbrakk> \<Longrightarrow> bd_inv (del x t) \<and> (if cl t = R then black_depth (del x t) = black_depth t else black_depth (del x t) = black_depth t - 1)
[PROOF STEP]
@case "x < k" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv t; cl_inv t\<rbrakk> \<Longrightarrow> bd_inv (del x t) \<and> (if cl t = R then black_depth (del x t) = black_depth t else black_depth (del x t) = black_depth t - 1)
[PROOF STEP]
@case "l = Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv t; cl_inv t\<rbrakk> \<Longrightarrow> bd_inv (del x t) \<and> (if cl t = R then black_depth (del x t) = black_depth t else black_depth (del x t) = black_depth t - 1)
[PROOF STEP]
@case "cl l = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv t; cl_inv t\<rbrakk> \<Longrightarrow> bd_inv (del x t) \<and> (if cl t = R then black_depth (del x t) = black_depth t else black_depth (del x t) = black_depth t - 1)
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv t; cl_inv t\<rbrakk> \<Longrightarrow> bd_inv (del x t) \<and> (if cl t = R then black_depth (del x t) = black_depth t else black_depth (del x t) = black_depth t - 1)
[PROOF STEP]
@case "x > k" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv t; cl_inv t\<rbrakk> \<Longrightarrow> bd_inv (del x t) \<and> (if cl t = R then black_depth (del x t) = black_depth t else black_depth (del x t) = black_depth t - 1)
[PROOF STEP]
@case "r = Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv t; cl_inv t\<rbrakk> \<Longrightarrow> bd_inv (del x t) \<and> (if cl t = R then black_depth (del x t) = black_depth t else black_depth (del x t) = black_depth t - 1)
[PROOF STEP]
@case "cl r = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv t; cl_inv t\<rbrakk> \<Longrightarrow> bd_inv (del x t) \<and> (if cl t = R then black_depth (del x t) = black_depth t else black_depth (del x t) = black_depth t - 1)
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv t; cl_inv t\<rbrakk> \<Longrightarrow> bd_inv (del x t) \<and> (if cl t = R then black_depth (del x t) = black_depth t else black_depth (del x t) = black_depth t - 1)
[PROOF STEP]
@endgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv t; cl_inv t\<rbrakk> \<Longrightarrow> bd_inv (del x t) \<and> (if cl t = R then black_depth (del x t) = black_depth t else black_depth (del x t) = black_depth t - 1)
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bd_inv t; cl_inv t\<rbrakk> \<Longrightarrow> bd_inv (del x t) \<and> (if cl t = R then black_depth (del x t) = black_depth t else black_depth (del x t) = black_depth t - 1)
[PROOF STEP]
@qed


[STATEMENT]
lemma del_cl:
  "cl_inv t \<Longrightarrow> if cl t = R then cl_inv (del x t) else cl_inv' (del x t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_inv t \<Longrightarrow> if cl t = R then cl_inv (del x t) else cl_inv' (del x t)
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_inv t \<Longrightarrow> if cl t = R then cl_inv (del x t) else cl_inv' (del x t)
[PROOF STEP]
@induct t @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_inv t \<Longrightarrow> if cl t = R then cl_inv (del x t) else cl_inv' (del x t)
[PROOF STEP]
@subgoal "t = Node l c k v r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_inv t \<Longrightarrow> if cl t = R then cl_inv (del x t) else cl_inv' (del x t)
[PROOF STEP]
@unfold "del x (Node l c k v r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_inv t \<Longrightarrow> if cl t = R then cl_inv (del x t) else cl_inv' (del x t)
[PROOF STEP]
@case "x = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_inv t \<Longrightarrow> if cl t = R then cl_inv (del x t) else cl_inv' (del x t)
[PROOF STEP]
@case "x < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_inv t \<Longrightarrow> if cl t = R then cl_inv (del x t) else cl_inv' (del x t)
[PROOF STEP]
@endgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_inv t \<Longrightarrow> if cl t = R then cl_inv (del x t) else cl_inv' (del x t)
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cl_inv t \<Longrightarrow> if cl t = R then cl_inv (del x t) else cl_inv' (del x t)
[PROOF STEP]
@qed


[STATEMENT]
lemma del_in_traverse_pairs [rewrite]:
  "rbt_sorted t \<Longrightarrow> rbt_in_traverse_pairs (del x t) = remove_elt_pairs x (rbt_in_traverse_pairs t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_sorted t \<Longrightarrow> rbt_in_traverse_pairs (del x t) = remove_elt_pairs x (rbt_in_traverse_pairs t)
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_sorted t \<Longrightarrow> rbt_in_traverse_pairs (del x t) = remove_elt_pairs x (rbt_in_traverse_pairs t)
[PROOF STEP]
@induct t @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_sorted t \<Longrightarrow> rbt_in_traverse_pairs (del x t) = remove_elt_pairs x (rbt_in_traverse_pairs t)
[PROOF STEP]
@subgoal "t = Node l c k v r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_sorted t \<Longrightarrow> rbt_in_traverse_pairs (del x t) = remove_elt_pairs x (rbt_in_traverse_pairs t)
[PROOF STEP]
@unfold "del x (Node l c k v r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_sorted t \<Longrightarrow> rbt_in_traverse_pairs (del x t) = remove_elt_pairs x (rbt_in_traverse_pairs t)
[PROOF STEP]
@endgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_sorted t \<Longrightarrow> rbt_in_traverse_pairs (del x t) = remove_elt_pairs x (rbt_in_traverse_pairs t)
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_sorted t \<Longrightarrow> rbt_in_traverse_pairs (del x t) = remove_elt_pairs x (rbt_in_traverse_pairs t)
[PROOF STEP]
@qed


[STATEMENT]
theorem delete_is_rbt [forward]:
  "is_rbt t \<Longrightarrow> is_rbt (delete x t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rbt t \<Longrightarrow> is_rbt (delete x t)
[PROOF STEP]
by auto2


[STATEMENT]
theorem delete_sorted [forward]:
  "rbt_sorted t \<Longrightarrow> rbt_sorted (delete x t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_sorted t \<Longrightarrow> rbt_sorted (delete x t)
[PROOF STEP]
by auto2


[STATEMENT]
theorem delete_rbt_map [rewrite]:
  "rbt_sorted t \<Longrightarrow> rbt_map (delete x t) = delete_map x (rbt_map t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_sorted t \<Longrightarrow> rbt_map (delete x t) = delete_map x (rbt_map t)
[PROOF STEP]
by auto2


[STATEMENT]
lemma class_field: "field (class_ring :: 'a :: field ring)" (is "field ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. field class_ring
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. field class_ring
[PROOF STEP]
interpret cring ?r
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cring class_ring
[PROOF STEP]
..
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. field class_ring
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. field class_ring
[PROOF STEP]
fix x :: 'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. field class_ring
[PROOF STEP]
have "x \<noteq> 0 \<Longrightarrow> \<exists>xa. xa * x = 1 \<and> x * xa = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> (0::'a) \<Longrightarrow> \<exists>xa. xa * x = (1::'a) \<and> x * xa = (1::'a)
[PROOF STEP]
by (intro exI[of _ "inverse x"], auto)
[PROOF STATE]
proof (state)
this:
x \<noteq> (0::'a) \<Longrightarrow> \<exists>xa. xa * x = (1::'a) \<and> x * xa = (1::'a)

goal (1 subgoal):
 1. field class_ring
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<noteq> (0::'a) \<Longrightarrow> \<exists>xa. xa * ?x2 = (1::'a) \<and> ?x2 * xa = (1::'a)

goal (1 subgoal):
 1. field class_ring
[PROOF STEP]
note [simp] = this
[PROOF STATE]
proof (state)
this:
?x2 \<noteq> (0::'a) \<Longrightarrow> \<exists>xa. xa * ?x2 = (1::'a) \<and> ?x2 * xa = (1::'a)

goal (1 subgoal):
 1. field class_ring
[PROOF STEP]
show "field ?r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. field class_ring
[PROOF STEP]
by (unfold_locales, auto simp: Units_def)
[PROOF STATE]
proof (state)
this:
field class_ring

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matrix_vs: "vectorspace (class_ring :: 'a :: field ring) (module_mat TYPE('a) nr nc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vectorspace class_ring (module_mat TYPE('a) nr nc)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vectorspace class_ring (module_mat TYPE('a) nr nc)
[PROOF STEP]
interpret abelian_group "module_mat TYPE('a) nr nc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abelian_group (module_mat TYPE('a) nr nc)
[PROOF STEP]
by (rule abelian_group_mat)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vectorspace class_ring (module_mat TYPE('a) nr nc)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vectorspace class_ring (module_mat TYPE('a) nr nc)
[PROOF STEP]
unfolding class_field_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vectorspace class_ring (module_mat TYPE('a) nr nc)
[PROOF STEP]
by (unfold_locales, unfold matrix_vs_simps,
      auto simp: add_smult_distrib_left_mat add_smult_distrib_right_mat)
[PROOF STATE]
proof (state)
this:
vectorspace class_ring (module_mat TYPE('a) nr nc)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vec_module: "module (class_ring :: 'a :: field ring) (module_vec TYPE('a) n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. module class_ring (module_vec TYPE('a) n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. module class_ring (module_vec TYPE('a) n)
[PROOF STEP]
interpret abelian_group "module_vec TYPE('a) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abelian_group (module_vec TYPE('a) n)
[PROOF STEP]
apply (unfold_locales)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> carrier (add_monoid (module_vec TYPE('a) n)); y \<in> carrier (add_monoid (module_vec TYPE('a) n))\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>add_monoid (module_vec TYPE('a) n)\<^esub> y \<in> carrier (add_monoid (module_vec TYPE('a) n))
 2. \<And>x y z. \<lbrakk>x \<in> carrier (add_monoid (module_vec TYPE('a) n)); y \<in> carrier (add_monoid (module_vec TYPE('a) n)); z \<in> carrier (add_monoid (module_vec TYPE('a) n))\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>add_monoid (module_vec TYPE('a) n)\<^esub> y \<otimes>\<^bsub>add_monoid (module_vec TYPE('a) n)\<^esub> z = x \<otimes>\<^bsub>add_monoid (module_vec TYPE('a) n)\<^esub> (y \<otimes>\<^bsub>add_monoid (module_vec TYPE('a) n)\<^esub> z)
 3. \<one>\<^bsub>add_monoid (module_vec TYPE('a) n)\<^esub> \<in> carrier (add_monoid (module_vec TYPE('a) n))
 4. \<And>x. x \<in> carrier (add_monoid (module_vec TYPE('a) n)) \<Longrightarrow> \<one>\<^bsub>add_monoid (module_vec TYPE('a) n)\<^esub> \<otimes>\<^bsub>add_monoid (module_vec TYPE('a) n)\<^esub> x = x
 5. \<And>x. x \<in> carrier (add_monoid (module_vec TYPE('a) n)) \<Longrightarrow> x \<otimes>\<^bsub>add_monoid (module_vec TYPE('a) n)\<^esub> \<one>\<^bsub>add_monoid (module_vec TYPE('a) n)\<^esub> = x
 6. \<And>x y. \<lbrakk>x \<in> carrier (add_monoid (module_vec TYPE('a) n)); y \<in> carrier (add_monoid (module_vec TYPE('a) n))\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>add_monoid (module_vec TYPE('a) n)\<^esub> y = y \<otimes>\<^bsub>add_monoid (module_vec TYPE('a) n)\<^esub> x
 7. carrier (add_monoid (module_vec TYPE('a) n)) \<subseteq> Units (add_monoid (module_vec TYPE('a) n))
[PROOF STEP]
unfolding module_vec_def Units_def
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>); y \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> y \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>)
 2. \<And>x y z. \<lbrakk>x \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>); y \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>); z \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> y \<otimes>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> z = x \<otimes>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> (y \<otimes>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> z)
 3. \<one>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>)
 4. \<And>x. x \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>) \<Longrightarrow> \<one>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> \<otimes>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> x = x
 5. \<And>x. x \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>) \<Longrightarrow> x \<otimes>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> \<one>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> = x
 6. \<And>x y. \<lbrakk>x \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>); y \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> y = y \<otimes>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> x
 7. carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>) \<subseteq> {y \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>). \<exists>x\<in>carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>). x \<otimes>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> y = \<one>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> \<and> y \<otimes>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> x = \<one>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub>}
[PROOF STEP]
using add_inv_exists_vec
[PROOF STATE]
proof (prove)
using this:
?v \<in> carrier_vec ?n \<Longrightarrow> \<exists>w\<in>carrier_vec ?n. w + ?v = 0\<^sub>v ?n \<and> ?v + w = 0\<^sub>v ?n

goal (7 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>); y \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> y \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>)
 2. \<And>x y z. \<lbrakk>x \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>); y \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>); z \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> y \<otimes>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> z = x \<otimes>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> (y \<otimes>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> z)
 3. \<one>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>)
 4. \<And>x. x \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>) \<Longrightarrow> \<one>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> \<otimes>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> x = x
 5. \<And>x. x \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>) \<Longrightarrow> x \<otimes>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> \<one>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> = x
 6. \<And>x y. \<lbrakk>x \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>); y \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>)\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> y = y \<otimes>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> x
 7. carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>) \<subseteq> {y \<in> carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>). \<exists>x\<in>carrier (add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>). x \<otimes>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> y = \<one>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> \<and> y \<otimes>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub> x = \<one>\<^bsub>add_monoid \<lparr>carrier = carrier_vec n, mult = undefined, one = undefined, zero = 0\<^sub>v n, add = (+), smult = (\<cdot>\<^sub>v)\<rparr>\<^esub>}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. module class_ring (module_vec TYPE('a) n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. module class_ring (module_vec TYPE('a) n)
[PROOF STEP]
unfolding class_field_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. module class_ring (module_vec TYPE('a) n)
[PROOF STEP]
apply (unfold_locales)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a x. \<lbrakk>a \<in> carrier class_ring; x \<in> carrier (module_vec TYPE('a) n)\<rbrakk> \<Longrightarrow> a \<odot>\<^bsub>module_vec TYPE('a) n\<^esub> x \<in> carrier (module_vec TYPE('a) n)
 2. \<And>a b x. \<lbrakk>a \<in> carrier class_ring; b \<in> carrier class_ring; x \<in> carrier (module_vec TYPE('a) n)\<rbrakk> \<Longrightarrow> (a \<oplus>\<^bsub>class_ring\<^esub> b) \<odot>\<^bsub>module_vec TYPE('a) n\<^esub> x = a \<odot>\<^bsub>module_vec TYPE('a) n\<^esub> x \<oplus>\<^bsub>module_vec TYPE('a) n\<^esub> b \<odot>\<^bsub>module_vec TYPE('a) n\<^esub> x
 3. \<And>a x y. \<lbrakk>a \<in> carrier class_ring; x \<in> carrier (module_vec TYPE('a) n); y \<in> carrier (module_vec TYPE('a) n)\<rbrakk> \<Longrightarrow> a \<odot>\<^bsub>module_vec TYPE('a) n\<^esub> (x \<oplus>\<^bsub>module_vec TYPE('a) n\<^esub> y) = a \<odot>\<^bsub>module_vec TYPE('a) n\<^esub> x \<oplus>\<^bsub>module_vec TYPE('a) n\<^esub> a \<odot>\<^bsub>module_vec TYPE('a) n\<^esub> y
 4. \<And>a b x. \<lbrakk>a \<in> carrier class_ring; b \<in> carrier class_ring; x \<in> carrier (module_vec TYPE('a) n)\<rbrakk> \<Longrightarrow> a \<otimes>\<^bsub>class_ring\<^esub> b \<odot>\<^bsub>module_vec TYPE('a) n\<^esub> x = a \<odot>\<^bsub>module_vec TYPE('a) n\<^esub> (b \<odot>\<^bsub>module_vec TYPE('a) n\<^esub> x)
 5. \<And>x. x \<in> carrier (module_vec TYPE('a) n) \<Longrightarrow> \<one>\<^bsub>class_ring\<^esub> \<odot>\<^bsub>module_vec TYPE('a) n\<^esub> x = x
[PROOF STEP]
unfolding class_ring_simps
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a x. \<lbrakk>a \<in> UNIV; x \<in> carrier (module_vec TYPE('a) n)\<rbrakk> \<Longrightarrow> a \<odot>\<^bsub>module_vec TYPE('a) n\<^esub> x \<in> carrier (module_vec TYPE('a) n)
 2. \<And>a b x. \<lbrakk>a \<in> UNIV; b \<in> UNIV; x \<in> carrier (module_vec TYPE('a) n)\<rbrakk> \<Longrightarrow> (a + b) \<odot>\<^bsub>module_vec TYPE('a) n\<^esub> x = a \<odot>\<^bsub>module_vec TYPE('a) n\<^esub> x \<oplus>\<^bsub>module_vec TYPE('a) n\<^esub> b \<odot>\<^bsub>module_vec TYPE('a) n\<^esub> x
 3. \<And>a x y. \<lbrakk>a \<in> UNIV; x \<in> carrier (module_vec TYPE('a) n); y \<in> carrier (module_vec TYPE('a) n)\<rbrakk> \<Longrightarrow> a \<odot>\<^bsub>module_vec TYPE('a) n\<^esub> (x \<oplus>\<^bsub>module_vec TYPE('a) n\<^esub> y) = a \<odot>\<^bsub>module_vec TYPE('a) n\<^esub> x \<oplus>\<^bsub>module_vec TYPE('a) n\<^esub> a \<odot>\<^bsub>module_vec TYPE('a) n\<^esub> y
 4. \<And>a b x. \<lbrakk>a \<in> UNIV; b \<in> UNIV; x \<in> carrier (module_vec TYPE('a) n)\<rbrakk> \<Longrightarrow> a * b \<odot>\<^bsub>module_vec TYPE('a) n\<^esub> x = a \<odot>\<^bsub>module_vec TYPE('a) n\<^esub> (b \<odot>\<^bsub>module_vec TYPE('a) n\<^esub> x)
 5. \<And>x. x \<in> carrier (module_vec TYPE('a) n) \<Longrightarrow> (1::'a) \<odot>\<^bsub>module_vec TYPE('a) n\<^esub> x = x
[PROOF STEP]
unfolding module_vec_simps
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a x. \<lbrakk>a \<in> UNIV; x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>v x \<in> carrier_vec n
 2. \<And>a b x. \<lbrakk>a \<in> UNIV; b \<in> UNIV; x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> (a + b) \<cdot>\<^sub>v x = a \<cdot>\<^sub>v x + b \<cdot>\<^sub>v x
 3. \<And>a x y. \<lbrakk>a \<in> UNIV; x \<in> carrier_vec n; y \<in> carrier_vec n\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>v (x + y) = a \<cdot>\<^sub>v x + a \<cdot>\<^sub>v y
 4. \<And>a b x. \<lbrakk>a \<in> UNIV; b \<in> UNIV; x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> a * b \<cdot>\<^sub>v x = a \<cdot>\<^sub>v (b \<cdot>\<^sub>v x)
 5. \<And>x. x \<in> carrier_vec n \<Longrightarrow> (1::'a) \<cdot>\<^sub>v x = x
[PROOF STEP]
using add_smult_distrib_vec
[PROOF STATE]
proof (prove)
using this:
(?a + ?b) \<cdot>\<^sub>v ?v = ?a \<cdot>\<^sub>v ?v + ?b \<cdot>\<^sub>v ?v

goal (5 subgoals):
 1. \<And>a x. \<lbrakk>a \<in> UNIV; x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>v x \<in> carrier_vec n
 2. \<And>a b x. \<lbrakk>a \<in> UNIV; b \<in> UNIV; x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> (a + b) \<cdot>\<^sub>v x = a \<cdot>\<^sub>v x + b \<cdot>\<^sub>v x
 3. \<And>a x y. \<lbrakk>a \<in> UNIV; x \<in> carrier_vec n; y \<in> carrier_vec n\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>v (x + y) = a \<cdot>\<^sub>v x + a \<cdot>\<^sub>v y
 4. \<And>a b x. \<lbrakk>a \<in> UNIV; b \<in> UNIV; x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> a * b \<cdot>\<^sub>v x = a \<cdot>\<^sub>v (b \<cdot>\<^sub>v x)
 5. \<And>x. x \<in> carrier_vec n \<Longrightarrow> (1::'a) \<cdot>\<^sub>v x = x
[PROOF STEP]
by (auto simp: smult_add_distrib_vec)
[PROOF STATE]
proof (state)
this:
module class_ring (module_vec TYPE('a) n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vec_vs: "vectorspace (class_ring :: 'a :: field ring) (module_vec TYPE('a) n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vectorspace class_ring (module_vec TYPE('a) n)
[PROOF STEP]
unfolding vectorspace_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. module class_ring (module_vec TYPE('a) n) \<and> field class_ring
[PROOF STEP]
using vec_module class_field
[PROOF STATE]
proof (prove)
using this:
module class_ring (module_vec TYPE(?'a) ?n)
field class_ring

goal (1 subgoal):
 1. module class_ring (module_vec TYPE('a) n) \<and> field class_ring
[PROOF STEP]
by (auto simp: class_field_def)


[STATEMENT]
lemma finsum_vec[simp]: "finsum_vec TYPE('a) n = finsum V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finsum_vec TYPE('a) n = finsum V
[PROOF STEP]
by (force simp: finsum_vec_def monoid_vec_def finsum_def finprod_def)


[STATEMENT]
lemma finsum_scalar_prod_sum:
  assumes f: "f : U \<rightarrow> carrier_vec n"
      and w: "w: carrier_vec n"
  shows "finsum V f U \<bullet> w = sum (\<lambda>u. f u \<bullet> w) U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finsum V f U \<bullet> w = (\<Sum>u\<in>U. f u \<bullet> w)
[PROOF STEP]
using w f
[PROOF STATE]
proof (prove)
using this:
w \<in> carrier_vec n
f \<in> U \<rightarrow> carrier_vec n

goal (1 subgoal):
 1. finsum V f U \<bullet> w = (\<Sum>u\<in>U. f u \<bullet> w)
[PROOF STEP]
proof (induct U rule: infinite_finite_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; w \<in> carrier_vec n; f \<in> A \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f A \<bullet> w = (\<Sum>u\<in>A. f u \<bullet> w)
 2. \<lbrakk>w \<in> carrier_vec n; f \<in> {} \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f {} \<bullet> w = (\<Sum>u\<in>{}. f u \<bullet> w)
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>w \<in> carrier_vec n; f \<in> F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f F \<bullet> w = (\<Sum>u\<in>F. f u \<bullet> w); w \<in> carrier_vec n; f \<in> insert x F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f (insert x F) \<bullet> w = (\<Sum>u\<in>insert x F. f u \<bullet> w)
[PROOF STEP]
case (insert u U)
[PROOF STATE]
proof (state)
this:
finite U
u \<notin> U
\<lbrakk>w \<in> carrier_vec n; f \<in> U \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f U \<bullet> w = (\<Sum>u\<in>U. f u \<bullet> w)
w \<in> carrier_vec n
f \<in> insert u U \<rightarrow> carrier_vec n

goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; w \<in> carrier_vec n; f \<in> A \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f A \<bullet> w = (\<Sum>u\<in>A. f u \<bullet> w)
 2. \<lbrakk>w \<in> carrier_vec n; f \<in> {} \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f {} \<bullet> w = (\<Sum>u\<in>{}. f u \<bullet> w)
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>w \<in> carrier_vec n; f \<in> F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f F \<bullet> w = (\<Sum>u\<in>F. f u \<bullet> w); w \<in> carrier_vec n; f \<in> insert x F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f (insert x F) \<bullet> w = (\<Sum>u\<in>insert x F. f u \<bullet> w)
[PROOF STEP]
hence f: "f : U \<rightarrow> carrier_vec n" "f u : carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
finite U
u \<notin> U
\<lbrakk>w \<in> carrier_vec n; f \<in> U \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f U \<bullet> w = (\<Sum>u\<in>U. f u \<bullet> w)
w \<in> carrier_vec n
f \<in> insert u U \<rightarrow> carrier_vec n

goal (1 subgoal):
 1. f \<in> U \<rightarrow> carrier_vec n &&& f u \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> U \<rightarrow> carrier_vec n
f u \<in> carrier_vec n

goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; w \<in> carrier_vec n; f \<in> A \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f A \<bullet> w = (\<Sum>u\<in>A. f u \<bullet> w)
 2. \<lbrakk>w \<in> carrier_vec n; f \<in> {} \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f {} \<bullet> w = (\<Sum>u\<in>{}. f u \<bullet> w)
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>w \<in> carrier_vec n; f \<in> F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f F \<bullet> w = (\<Sum>u\<in>F. f u \<bullet> w); w \<in> carrier_vec n; f \<in> insert x F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f (insert x F) \<bullet> w = (\<Sum>u\<in>insert x F. f u \<bullet> w)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finsum V f (insert u U) \<bullet> w = (\<Sum>u\<in>insert u U. f u \<bullet> w)
[PROOF STEP]
unfolding finsum_insert[OF insert(1) insert(2) f]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f u + finsum V f U) \<bullet> w = (\<Sum>u\<in>insert u U. f u \<bullet> w)
[PROOF STEP]
apply (subst add_scalar_prod_distrib)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. f u \<in> carrier_vec ?n1
 2. finsum V f U \<in> carrier_vec ?n1
 3. w \<in> carrier_vec ?n1
 4. f u \<bullet> w + finsum V f U \<bullet> w = (\<Sum>u\<in>insert u U. f u \<bullet> w)
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
finite U
u \<notin> U
\<lbrakk>w \<in> carrier_vec n; f \<in> U \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f U \<bullet> w = (\<Sum>u\<in>U. f u \<bullet> w)
w \<in> carrier_vec n
f \<in> insert u U \<rightarrow> carrier_vec n

goal (4 subgoals):
 1. f u \<in> carrier_vec ?n1
 2. finsum V f U \<in> carrier_vec ?n1
 3. w \<in> carrier_vec ?n1
 4. f u \<bullet> w + finsum V f U \<bullet> w = (\<Sum>u\<in>insert u U. f u \<bullet> w)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finsum V f (insert u U) \<bullet> w = (\<Sum>u\<in>insert u U. f u \<bullet> w)

goal (2 subgoals):
 1. \<And>A. \<lbrakk>infinite A; w \<in> carrier_vec n; f \<in> A \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f A \<bullet> w = (\<Sum>u\<in>A. f u \<bullet> w)
 2. \<lbrakk>w \<in> carrier_vec n; f \<in> {} \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f {} \<bullet> w = (\<Sum>u\<in>{}. f u \<bullet> w)
[PROOF STEP]
qed auto


[STATEMENT]
lemma vec_neg[simp]: assumes "x : carrier_vec n" shows "\<ominus>\<^bsub>V\<^esub> x = - x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<ominus>\<^bsub>V\<^esub> x = - x
[PROOF STEP]
unfolding a_inv_def m_inv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE y. y \<in> carrier (add_monoid V) \<and> x \<otimes>\<^bsub>add_monoid V\<^esub> y = \<one>\<^bsub>add_monoid V\<^esub> \<and> y \<otimes>\<^bsub>add_monoid V\<^esub> x = \<one>\<^bsub>add_monoid V\<^esub>) = - x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE y. y \<in> carrier_vec n \<and> x + y = 0\<^sub>v n \<and> y + x = 0\<^sub>v n) = - x
[PROOF STEP]
apply (rule the_equality, intro conjI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. - x \<in> carrier_vec n
 2. x + - x = 0\<^sub>v n
 3. - x + x = 0\<^sub>v n
 4. \<And>y. y \<in> carrier_vec n \<and> x + y = 0\<^sub>v n \<and> y + x = 0\<^sub>v n \<Longrightarrow> y = - x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier_vec n

goal (4 subgoals):
 1. - x \<in> carrier_vec n
 2. x + - x = 0\<^sub>v n
 3. - x + x = 0\<^sub>v n
 4. \<And>y. y \<in> carrier_vec n \<and> x + y = 0\<^sub>v n \<and> y + x = 0\<^sub>v n \<Longrightarrow> y = - x
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>x \<in> carrier_vec n; y \<in> carrier_vec n; x + y = 0\<^sub>v n; y + x = 0\<^sub>v n\<rbrakk> \<Longrightarrow> y = - x
[PROOF STEP]
using M.minus_unique uminus_carrier_vec uminus_r_inv_vec
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y + ?x = 0\<^sub>v n; ?x + ?y' = 0\<^sub>v n; ?x \<in> carrier_vec n; ?y \<in> carrier_vec n; ?y' \<in> carrier_vec n\<rbrakk> \<Longrightarrow> ?y = ?y'
(- ?v \<in> carrier_vec ?n) = (?v \<in> carrier_vec ?n)
?v \<in> carrier_vec ?n \<Longrightarrow> ?v + - ?v = 0\<^sub>v ?n

goal (1 subgoal):
 1. \<And>y. \<lbrakk>x \<in> carrier_vec n; y \<in> carrier_vec n; x + y = 0\<^sub>v n; y + x = 0\<^sub>v n\<rbrakk> \<Longrightarrow> y = - x
[PROOF STEP]
by blast


[STATEMENT]
lemma finsum_dim:
  "finite A \<Longrightarrow> f \<in> A \<rightarrow> carrier_vec n \<Longrightarrow> dim_vec (finsum V f A) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; f \<in> A \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> dim_vec (finsum V f A) = n
[PROOF STEP]
proof(induct set:finite)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f \<in> {} \<rightarrow> carrier_vec n \<Longrightarrow> dim_vec (finsum V f {}) = n
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; f \<in> F \<rightarrow> carrier_vec n \<Longrightarrow> dim_vec (finsum V f F) = n; f \<in> insert x F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> dim_vec (finsum V f (insert x F)) = n
[PROOF STEP]
case (insert a A)
[PROOF STATE]
proof (state)
this:
finite A
a \<notin> A
f \<in> A \<rightarrow> carrier_vec n \<Longrightarrow> dim_vec (finsum V f A) = n
f \<in> insert a A \<rightarrow> carrier_vec n

goal (2 subgoals):
 1. f \<in> {} \<rightarrow> carrier_vec n \<Longrightarrow> dim_vec (finsum V f {}) = n
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; f \<in> F \<rightarrow> carrier_vec n \<Longrightarrow> dim_vec (finsum V f F) = n; f \<in> insert x F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> dim_vec (finsum V f (insert x F)) = n
[PROOF STEP]
hence dfa: "dim_vec (f a) = n"
[PROOF STATE]
proof (prove)
using this:
finite A
a \<notin> A
f \<in> A \<rightarrow> carrier_vec n \<Longrightarrow> dim_vec (finsum V f A) = n
f \<in> insert a A \<rightarrow> carrier_vec n

goal (1 subgoal):
 1. dim_vec (f a) = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_vec (f a) = n

goal (2 subgoals):
 1. f \<in> {} \<rightarrow> carrier_vec n \<Longrightarrow> dim_vec (finsum V f {}) = n
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; f \<in> F \<rightarrow> carrier_vec n \<Longrightarrow> dim_vec (finsum V f F) = n; f \<in> insert x F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> dim_vec (finsum V f (insert x F)) = n
[PROOF STEP]
have f: "f \<in> A \<rightarrow> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> A \<rightarrow> carrier_vec n
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
finite A
a \<notin> A
f \<in> A \<rightarrow> carrier_vec n \<Longrightarrow> dim_vec (finsum V f A) = n
f \<in> insert a A \<rightarrow> carrier_vec n

goal (1 subgoal):
 1. f \<in> A \<rightarrow> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> A \<rightarrow> carrier_vec n

goal (2 subgoals):
 1. f \<in> {} \<rightarrow> carrier_vec n \<Longrightarrow> dim_vec (finsum V f {}) = n
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; f \<in> F \<rightarrow> carrier_vec n \<Longrightarrow> dim_vec (finsum V f F) = n; f \<in> insert x F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> dim_vec (finsum V f (insert x F)) = n
[PROOF STEP]
hence fa: "f a \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow> carrier_vec n

goal (1 subgoal):
 1. f a \<in> carrier_vec n
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow> carrier_vec n
finite A
a \<notin> A
f \<in> A \<rightarrow> carrier_vec n \<Longrightarrow> dim_vec (finsum V f A) = n
f \<in> insert a A \<rightarrow> carrier_vec n

goal (1 subgoal):
 1. f a \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f a \<in> carrier_vec n

goal (2 subgoals):
 1. f \<in> {} \<rightarrow> carrier_vec n \<Longrightarrow> dim_vec (finsum V f {}) = n
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; f \<in> F \<rightarrow> carrier_vec n \<Longrightarrow> dim_vec (finsum V f F) = n; f \<in> insert x F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> dim_vec (finsum V f (insert x F)) = n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (finsum V f (insert a A)) = n
[PROOF STEP]
unfolding finsum_insert[OF insert(1) insert(2) f fa]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (f a + finsum V f A) = n
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
finite A
a \<notin> A
f \<in> A \<rightarrow> carrier_vec n \<Longrightarrow> dim_vec (finsum V f A) = n
f \<in> insert a A \<rightarrow> carrier_vec n

goal (1 subgoal):
 1. dim_vec (f a + finsum V f A) = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_vec (finsum V f (insert a A)) = n

goal (1 subgoal):
 1. f \<in> {} \<rightarrow> carrier_vec n \<Longrightarrow> dim_vec (finsum V f {}) = n
[PROOF STEP]
qed simp


[STATEMENT]
lemma lincomb_dim:
  assumes fin: "finite X"
    and X: "X \<subseteq> carrier_vec n"
  shows "dim_vec (lincomb a X) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (lincomb a X) = n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dim_vec (lincomb a X) = n
[PROOF STEP]
let ?f = "\<lambda>v. a v \<cdot>\<^sub>v v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dim_vec (lincomb a X) = n
[PROOF STEP]
have f: "?f \<in> X \<rightarrow> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>v. a v \<cdot>\<^sub>v v) \<in> X \<rightarrow> carrier_vec n
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> a x \<cdot>\<^sub>v x \<in> carrier_vec n
[PROOF STEP]
using X
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier_vec n

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

goal (1 subgoal):
 1. dim_vec (lincomb a X) = n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (lincomb a X) = n
[PROOF STEP]
unfolding lincomb_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (\<Oplus>\<^bsub>V\<^esub>v\<in>X. a v \<cdot>\<^sub>v v) = n
[PROOF STEP]
using finsum_dim[OF fin f]
[PROOF STATE]
proof (prove)
using this:
dim_vec (\<Oplus>\<^bsub>V\<^esub>v\<in>X. a v \<cdot>\<^sub>v v) = n

goal (1 subgoal):
 1. dim_vec (\<Oplus>\<^bsub>V\<^esub>v\<in>X. a v \<cdot>\<^sub>v v) = n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
dim_vec (lincomb a X) = n

goal:
No subgoals!
[PROOF STEP]
qed