Theory Examples

theory Examples
imports Vector_Space RealDef
begin

section{*Examples*}

context vector_space
begin

text{*Here we show that every field is a vector space over itself 
  (we interpret the scalar product as 
  the ordinary multiplication of the field. We use make use of @{text vector_spaceI}.*}
lemma field_is_vector_space: 
  assumes field_K: "field K" 
  shows "vector_space K K op ⊗\<^bsub>K\<^esub> "
proof (rule vector_spaceI)
  show "field K" using field_K .
  show "abelian_group K" using field_K
    unfolding field_def
    unfolding domain_def
    unfolding cring_def
    unfolding ring_def
    by fast
next
  show "!!x a. [|x ∈ carrier K; a ∈ carrier K|] ==> a ⊗\<^bsub>K\<^esub> x ∈ carrier K"
    using monoid.m_closed [OF field_is_monoid [OF field_K]] by best
next
  show "!!x a b. [|x ∈ carrier K; a ∈ carrier K; b ∈ carrier K|] 
    ==> a ⊗\<^bsub>K\<^esub> b ⊗\<^bsub>K\<^esub> x = a ⊗\<^bsub>K\<^esub> (b ⊗\<^bsub>K\<^esub> x)"
    using monoid.m_assoc [OF field_is_monoid [OF field_K]] by best
next
  show "!!x. x ∈ carrier K ==> \<one>\<^bsub>K\<^esub> ⊗\<^bsub>K\<^esub> x = x"
    using monoid.l_one [OF field_is_monoid [OF field_K]] by best
next
  show "!!x y a. [|x ∈ carrier K; y ∈ carrier K; a ∈ carrier K|] 
    ==> a ⊗\<^bsub>K\<^esub> (x ⊕\<^bsub>K\<^esub> y) = a ⊗\<^bsub>K\<^esub> x ⊕\<^bsub>K\<^esub> a ⊗\<^bsub>K\<^esub> y"
    using ring.r_distr [OF field_is_ring [OF field_K]] by best
next
  show "!!x a b. [|x ∈ carrier K; a ∈ carrier K; b ∈ carrier K|] 
    ==> (a ⊕\<^bsub>K\<^esub> b) ⊗\<^bsub>K\<^esub> x = a ⊗\<^bsub>K\<^esub> x ⊕\<^bsub>K\<^esub> b ⊗\<^bsub>K\<^esub> x"
  proof -
    fix x and a and b
    assume x_in_K: "x ∈ carrier K"
      and a_in_K: "a∈ carrier K" and b_in_K:"b∈ carrier K"
    show "(a ⊕\<^bsub>K\<^esub> b) ⊗\<^bsub>K\<^esub> x = a ⊗\<^bsub>K\<^esub> x ⊕\<^bsub>K\<^esub> b ⊗\<^bsub>K\<^esub> x"
      using ring.l_distr 
      [OF field_is_ring [OF field_K] a_in_K b_in_K x_in_K] .
  qed
qed (auto)

end
end