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
    "HOL-Library.Set_Algebras"
begin


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

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

lemma assoc_add_vecset:
  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

lemma comm_add_vecset:
  assumes "(A :: 'a :: ab_semigroup_add vec set) ⊆ carrier_vec n"
    and "B ⊆ carrier_vec n"
  shows "A + B = B + A"
  unfolding set_plus_def using comm_add_vec assms by blast


end