Theory Calculus_of_Subspaces

theory Calculus_of_Subspaces
  imports Subspaces Ideal
begin

section{*Calculus of Subspaces*}

text{*The theory Ideal is imported in order to use the definition of the 
  sum of two sets, given by the operation @{term set_add'}*}

context vector_space
begin

lemma
  subspace_inter_closed:
  assumes s: "subspace M"
  and sm: "subspace M'"
  shows "subspace (M ∩ M')"
proof (unfold subspace_def, rule conjI3)
  show "M ∩ M' ⊆ carrier V" using s sm unfolding subspace_def by blast
  show "M ∩ M' ≠ {}" using zero_in_subspace s sm by blast
  show "∀α∈carrier K. ∀β∈carrier K. ∀x∈M ∩ M'. ∀y∈M ∩ M'. α · x ⊕\<^bsub>V\<^esub> β · y ∈ M ∩ M'"
    using s sm unfolding subspace_def by blast
qed


subsection{*Theorem 1*}

text{*In the following result we have to avoid empty intersections,
  since the empty intersection is defined to be equal to @{term UNIV}. 
  @{term UNIV} is not a subspace, since it is not (in general, 
  it could be in some cases) a subset of @{term "carrier V"}.*}
text{*Nevertheless, this does not mean any limitation in practice,
  since any set will be always a subset of the subspace @{term "carrier V"}
  (see @{thm "subspace_V"})*}
text{*We need to prove that intersection of subspaces is a subspace
  to define later the subspace spanned by any set as the intersection of
  every subspace in which the set is contained. Thus, assuming that the intersection
  will be not empty (@{term "carrier V"} will be always a member of 
  such intersection) is natural.*}

lemma subspace_finite_inter_closed:
  assumes a: "finite A"
  and ne: "A ≠ {}"
  and kj: "∀j∈A. subspace (P j)"
  shows "subspace (\<Inter>j∈A. P j)"
  using a kj ne proof (induct A)
  case empty
  show ?case using empty.prems by simp
next
  case (insert x F)
  have Px: "subspace (P x)" using insert.prems (1) by blast
  show ?case
  proof (cases "F = {}")
    case True
    show ?thesis
      unfolding True using Px by fastsimp
  next
    case False
    have sF: "subspace (\<Inter>a∈F. P a)"
      using insert.hyps (3) using False using insert.prems (1) by blast
    show ?thesis
      unfolding INT_insert
      by (rule subspace_inter_closed [OF Px sF])
  qed
qed

text{*The same lemma than @{thm subspace_finite_inter_closed} 
  but for collections indexed by the natural numbers:*}

lemma subspace_finite_inter_index_closed:
  assumes smn: "∀j∈{..(n::nat)}. subspace (M j)"
  shows "subspace (\<Inter>j∈{..n}. M j)"
  using smn proof (induct n)
  case 0
  show ?case using 0 by simp
next
  case (Suc n)
  have prem: "∀j∈{..n}. subspace (M j)" and prem2: "subspace (M (Suc n))"
    using Suc.prems by simp_all
  hence prem1: "subspace (\<Inter> a≤n. M a)"
    using Suc.hyps by fast
  show ?case
    unfolding atMost_Suc
    unfolding INT_insert [of "Suc n" "{..n}"]
    by (rule subspace_inter_closed, rule prem2, rule prem1)
qed

text{*We now remove the requisite of the collection of subspaces being finite.
  Thus, the proof cannot be longer carried out by induction in the structure 
  of the set.*}

lemma subspace_infinite_inter_closed:
  assumes ne: "A ≠ {}"
  and kj: "∀j∈A. subspace (P j)"
  shows "subspace (\<Inter>j∈A. P j)"
proof (unfold subspace_def, rule)
  show "INTER A P ⊆ carrier V"
    unfolding INTER_def
    using ne using kj unfolding subspace_def by blast
  show "INTER A P ≠ {} ∧ 
    (∀α∈carrier K. ∀β∈carrier K. ∀x∈INTER A P. ∀y∈INTER A P. α · x ⊕\<^bsub>V\<^esub> β · y ∈ INTER A P)"
  proof (rule conjI)
    show "INTER A P ≠ {}"
    proof (unfold INTER_def, auto, rule exI [of _ "\<zero>\<^bsub>V\<^esub>"], rule)
      fix x assume x: "x ∈ A"
      show "\<zero>\<^bsub>V\<^esub> ∈ P x"
        using zero_in_subspace [of "P x"]
        using kj using x by fast
    qed
    show "∀α∈carrier K. ∀β∈carrier K. ∀x∈INTER A P. ∀y∈INTER A P. α · x ⊕\<^bsub>V\<^esub> β · y ∈ INTER A P"
    proof (rule ballI)+
      fix x y a b
      assume x: "x ∈ INTER A P" and y: "y ∈ INTER A P" 
        and a: "a ∈ carrier K" and b: "b ∈ carrier K"
      show "a · y ⊕\<^bsub>V\<^esub> b · x ∈ INTER A P"
      proof
        fix xa assume xa: "xa ∈ A"
        have xp: "x ∈ P xa" and yp: "y ∈ P xa" using x y xa by auto
        thus "a · y ⊕\<^bsub>V\<^esub> b · x ∈ P xa"
          using kj xa a b unfolding subspace_def by force
      qed
    qed
  qed
qed
      
text{*It is now clear than the previous results for finite intersections
  @{thm subspace_finite_inter_index_closed} and 
  @{thm subspace_finite_inter_closed} can be proved as a corollary of
  @{thm subspace_infinite_inter_closed}, but we prefer to leave their
  induction proofs since they illustrate different ways of proving similar results
  depending on the context or the premises.*}

text{*Here Halmos introduces the definition of the span of a set @{term "S ⊆ carrier V"}
  as the interection of all the subsets in which @{term "S"} is contained. We already have 
  a notion of the @{term span} of a set in our setting, as the set of all the elements
  which are equal to the linear combinations of the elements of this set. We will name this new 
  notion @{text subspace_span}, and then prove that they both are equal:*}

text{*We introduce an auxiliar definition of the set of subspaces in which one 
  set is enclosed:*}

definition subspace_encloser :: "('b => bool) => ('b => bool) set"
  where "subspace_encloser A = {M. subspace M ∧ A ⊆ M}"

text{*A trivial lemma stating that a set is always enclosed in the
  subspace @{term "carrier V"}:*}

lemma
  assumes m: "M ⊆ carrier V"
  shows "carrier V ∈ subspace_encloser M"
  unfolding subspace_encloser_def
  using subspace_V m by fast

text{*The definition of the subspace spanned by a set, following Halmos:*}

definition subspace_span :: "('b => bool) => 'b => bool"
  where "subspace_span A = (\<Inter>B∈(subspace_encloser A). B)"

text{*The previous lemma @{thm subspace_finite_inter_closed} is now used to 
  prove that @{term "subspace_span"} is a subspace itself.*}

lemma
  subspace_span_monotone:
  assumes s: "S ⊆ carrier V"
  shows "S ⊆ subspace_span S"
  unfolding subspace_span_def
  unfolding subspace_encloser_def by fast

lemma
  subspace_subspace_span:
  assumes s: "S ⊆ carrier V"
  shows "subspace (subspace_span S)"
  unfolding subspace_span_def subspace_encloser_def
proof (rule subspace_infinite_inter_closed)
  show "{M. subspace M ∧ S ⊆ M} ≠ {}"
    using subspace_V s by blast
  show "Ball {M. subspace M ∧ S ⊆ M} subspace" by fast
qed

subsection{*Theorem 2.*}

text{*The definition of @{term finsum} in Isabelle relies on the notion of 
  finiteness of the set which elements are added up. Working in a finite dimensional 
  vector space does not mean that every subset is finite, and thus the elements 
  in the span of such a set cannot be written as finite sums of its elements.*}

text{*The previous point is not explicit is Halmos, where it is never explained how
  to deal with infinite sums (or sums over not finite sets).*}

lemma
  subspace_span_empty:
  "subspace_span {} = {\<zero>\<^bsub>V\<^esub>}"
proof
  show "{\<zero>\<^bsub>V\<^esub>} ⊆ subspace_span {}"
    unfolding subspace_span_def subspace_encloser_def 
    using zero_in_subspace by blast
  show "subspace_span {} ⊆ {\<zero>\<^bsub>V\<^esub>}"
    unfolding subspace_span_def subspace_encloser_def
    using subspace_zero by force
qed

lemma theorem_2:
  assumes f: "finite S"
  and s: "S ⊆ carrier V"
  shows "span S = subspace_span S"
proof
  show "span S ⊆ subspace_span S"
    using f s proof (induct S)
    case empty
    show ?case unfolding span_empty subspace_span_empty ..
  next
    case (insert x F)
    show ?case unfolding subspace_span_def subspace_encloser_def unfolding span_def apply auto
    proof -
      fix xa and g
      assume cf_g: "g ∈ coefficients_function (carrier V)" 
        and s_xa: "subspace xa" 
        and x_in_xa: "x ∈ xa" and F_subset_xa: "F ⊆ xa"
      have gs_insert: "good_set (insert x F)"
        by (metis finite.insertI good_set_def insert(1) insert.prems)
      show "linear_combination g (insert x F) ∈ xa" 
      proof (rule subspace_linear_combination_closed)
        show "subspace xa" using s_xa .
        show "finite (insert x F)" using insert.hyps(1) by fast
        show "insert x F ⊆ xa" using x_in_xa F_subset_xa by fast
        show "g ∈ coefficients_function (insert x F)" sorry
      qed
    qed
  qed
  show "subspace_span S ⊆ span S" 
    unfolding subspace_span_def subspace_encloser_def unfolding span_def apply auto
    sorry
qed

subsection{*Theorem 3.*}

text{*The following theorem appears in Halmos as an easy consequence of the 
  previous one; probably it should be proved based on the fact that any linear 
  combination can be written down as the sum of two elements, being one in the 
  first set and the other in the second one.*}

term "I <+>\<^bsub>R\<^esub> J"
find_theorems "_ <+>\<^bsub>?F\<^esub> _"
lemma theorem_3:
  assumes I: "subspace I"
  and J: "subspace J"
  shows "subspace_span (I ∪ J) = I <+>\<^bsub>V\<^esub> J"
  unfolding AbelCoset.set_add_def'
proof
  show "subspace_span (I ∪ J) ⊆ (\<Union>h∈I. \<Union>k∈J. {h ⊕\<^bsub>V\<^esub> k})"
    sorry
  show "(\<Union>h∈I. \<Union>k∈J. {h ⊕\<^bsub>V\<^esub> k}) ⊆ subspace_span (I ∪ J)"
    sorry
qed

text{*The following definition is simply a rewriting rule, it may be
  skipped; note also that produces ambiguous parse trees when parsing
  deducing types from expressions, so it could be avoided if it produces
  any clashes:*}

definition set_add2 :: "'b set => 'b set => 'b set"  (infixl "+" 60)
  where "set_add2 A B = subspace_span (A ∪ B)"

corollary set_add2_set_add': 
  assumes I: "subspace I"
  and J: "subspace J"
  shows "I + J = I <+>\<^bsub>V\<^esub> J"
  unfolding set_add2_def using theorem_3 [OF I J] .

text{*The following definition is applied only to subspaces:*}

definition complement :: "'b set => 'b set => bool"
  where "complement I J = ((I ∩ J = {\<zero>\<^bsub>V\<^esub>}) ∧ (I + J = carrier V))"

end

end