# Theory Sum_Vec_Set

section ‹Sum of Vector Sets›

text ‹We use Isabelle's Set-Algebra theory to be able to write V + W for sets of vectors V and W,
and prove some obvious properties about them.›
theory Sum_Vec_Set
imports
Missing_Matrix

begin

assumes "(A :: 'a :: monoid_add vec set)  carrier_vec n"
shows "A + {0v n} = A"
unfolding set_plus_def using assms by force

assumes "(A :: 'a :: monoid_add vec set)  carrier_vec n"
shows "{0v n} + A = A"
unfolding set_plus_def using assms by force

assumes "(A :: 'a :: semigroup_add vec set)  carrier_vec n"
and "B  carrier_vec n"
and "C  carrier_vec n"
shows "A + (B + C) = (A + B) + C"
proof -
{
fix x
assume "x  A + (B + C)"
then obtain a b c where "x = a + (b + c)" and *: "a  A" "b  B" "c  C"
unfolding set_plus_def by auto
with assms have "x = (a + b) + c" using assoc_add_vec[of a n b c] by force
with * have "x  (A + B) + C" by auto
}
moreover
{
fix x
assume "x  (A + B) + C"
then obtain a b c where "x = (a + b) + c" and *: "a  A" "b  B" "c  C"
unfolding set_plus_def by auto
with assms have "x = a + (b + c)" using assoc_add_vec[of a n b c] by force
with * have "x  A + (B + C)" by auto
}
ultimately show ?thesis by blast
qed

lemma sum_carrier_vec[intro]: "A  carrier_vec n  B  carrier_vec n  A + B  carrier_vec n"
unfolding set_plus_def by force