Theory Field2 (Isabelle2011: January 2011)

theory Field2 (*No puedo ponerle de nombre Fields, ya existe*)
imports Previous
"~~/src/HOL/Algebra/Ring"
begin

section{*Previous relations between algebraic structures.*}

text{*We can create a lemma to check if one algebraic structure is a domain.*}
lemma domainI:
  fixes R (structure)
  assumes cring: "cring R"
      and one_not_zero: "\<one> ~= \<zero>"
      and integral: "!!a b. [| a ⊗ b = \<zero>; a ∈ carrier R; b ∈ carrier R |] ==> a = \<zero> | b = \<zero>"
  shows "domain R"
  unfolding domain_def
  apply (rule conjI)
  using cring apply fast
  unfolding domain_axioms_def
  apply (rule conjI)
  using one_not_zero apply fast
  using integral by fast

text{*Similarly with a field:*}

lemma fieldI:
  fixes R (structure)
  assumes dom: "domain R"
  and field_Units: "Units R = carrier R - {\<zero>}"
  shows "field R"
  unfolding field_def
  apply (intro conjI)
  using dom apply fast
  unfolding field_axioms_def using field_Units .

text{*A field is an additive monoid*}
lemma (in field) field_impl_monoid:
  "monoid (| carrier = carrier R, mult = add R, one = zero R |)),"
  using abelian_monoid.a_monoid [of R] 
  using field_axioms
  unfolding field_def
  unfolding domain_def
  unfolding cring_def
  unfolding ring_def
  unfolding abelian_group_def 
  by simp

text{*A field is a multiplicative monoid:*}
lemma field_is_monoid: fixes K (structure) 
  assumes field_K: "field K" shows "monoid K"
proof -
  from field_K show ?thesis
    unfolding field_def
    unfolding domain_def
    unfolding cring_def
    unfolding ring_def
    by best
qed

text{*Every field is a ring*}
lemma field_is_ring: fixes K (structure) 
  assumes field_K: "field K" shows "ring K"
proof -
  from field_K show ?thesis
    unfolding field_def
    unfolding domain_def
    unfolding cring_def
    by best
qed

subsection{*Previous properties*}

text{*First of all we are going to introduce some properties of fields. Most of them are also satisfied in rings
and in previous algebraic structures, so they will be trivial for us.*}

text{*This property is trivial and proved in the library: *}
lemma (in field) r_zero:
  "x ∈ carrier R ==> x ⊕ \<zero> = x" 
 using r_zero [of x] .

text{*However, we can make a long proof of the preceding fact.*}
lemma (in field) r_zero2: "x ∈ carrier R ==> x ⊕ \<zero> = x"
proof -
  assume x_in_R: "x ∈ carrier R"
  have l_zero: "\<zero> ⊕ x = x"
    --"Using 'rule' we can give a lemma which goal is the same that
    the goal that we want to prove. Then, the 'rule' will convert my goal to the
    premisses of the theorem."
  proof (rule abelian_monoid.l_zero [of R])
    show "abelian_monoid R"
      print_facts
      using field_axioms
      unfolding field_def
      unfolding domain_def
      unfolding cring_def
      unfolding ring_def
      unfolding abelian_group_def by fast
  next 
    --"Using 'next' we closed the previous proof, so we would lose
      the local results of it. We open a new context for the second goal
      that we have. It is more or less than if we close a 'for' or a 'while' in C++ or Java:
      we will lose the local variables, but we will keep the global ones." 
    show "x ∈ carrier R"
      using x_in_R .
  qed
  show ?thesis
    find_theorems "?x ⊕ ?y = ?y ⊕ ?x"
    using l_zero
    using a_comm [OF zero_closed x_in_R] by simp
qed

text{*This is also in the library (for commutative groups): *}
lemma (in field) a_comm:
  "!! x y. [|x ∈ carrier R; y ∈ carrier R|] ==> x ⊕ y = y ⊕ x"
  using cring_simprules (10) .

text{*But we can prove it: we have that the property is satisfied in a commutative group.
We will prove that a field is a commutative group and then we will use the property.*}
lemma (in field) a_comm2:
  "!! x y. [|x ∈ carrier R; y ∈ carrier R|] ==> x ⊕ y = y ⊕ x"
proof -
  fix x y
  assume x_in_R: "x ∈ carrier R" and y_in_R: "y ∈ carrier R"
  --"First we prove that the additive structure is a @{text comm_group}, the result is proved for @{text comm_monoid}."
  have c_gr: "comm_group (|carrier = carrier R, mult = op ⊕, one = \<zero>|)),"
  proof (rule abelian_group.a_comm_group [of R])
    show "abelian_group R"
      using field_axioms
      unfolding field_def
      unfolding domain_def
      unfolding cring_def
      unfolding ring_def by fast
  qed
  show "x ⊕ y = y ⊕ x"
    using comm_monoid.m_comm [of " (|carrier = carrier R, mult = op ⊕, one = \<zero>|))," x y]
    using c_gr
    unfolding comm_group_def
    using x_in_R
    using y_in_R by simp
qed


lemma (in field) a_assoc:
"!! x y z. [|x ∈ carrier R; y ∈ carrier R; z ∈ carrier R|] ==>(x ⊕ y) ⊕ z = x ⊕ (y ⊕ z)"
using a_assoc .

lemma (in field) r_neg:
"x ∈ carrier R ==> x ⊕ (\<ominus> x)=\<zero> "
using cring_simprules(17) .

lemma (in field) m_comm:
"!! x y. [| x ∈ carrier R; y ∈ carrier R|] ==> x ⊗ y = y ⊗ x"
using m_comm .

lemma (in field) m_assoc:
"!! x y z. [|x ∈ carrier R; y ∈ carrier R; z ∈ carrier R|] ==> (x ⊗ y) ⊗ z = x ⊗ (y ⊗ z)"
using m_assoc .

lemma (in field) r_one:
"x ∈ carrier R ==> x ⊗ \<one> = x"
using r_one .

lemma (in field ) r_inv:
"x∈ Units R ==> x ⊗ inv x = \<one> "
using Units_r_inv .

lemma (in field) r_distr:
"[|x∈ carrier R; y∈ carrier R;z∈ carrier R|] ==> x ⊗ (y ⊕ z) = x ⊗ y ⊕ x ⊗ z"
using r_distr .

lemma (in field) l_one:
"x ∈ carrier R ==> \<one> ⊗ x=x"
  using r_one
  using  one_closed
  using m_comm [of x \<one>]
  by simp

subsection{*Exercises in Halmos*}

text{*Definition of field and some properties are already included in the library, so we don't make it.*}

text{*Here we present some exercises proposed by Halmos. There are someone already solved in the library, so they
will be trivial for us.*}

text{*Exercise 1A*}
lemma (in field) l_zero:
  "x ∈ carrier R ==> \<zero> ⊕ x=x"
  using r_zero [of x]
  using zero_closed
  using a_comm [of x \<zero>] by simp

text{*Exercise 1B*}
lemma (in field) a_l_cancel:
  "[|x ∈ carrier R; y∈ carrier R;z ∈ carrier R|] ==> (x ⊕ y = x ⊕ z) = (y = z)"
  using a_l_cancel .

text{*Exercise 1C*}
lemma (in field) plus_minus_cancel:
  "[|x ∈ carrier R; y ∈ carrier R|] ==> x ⊕ (y \<ominus> x) = y"
proof -
  assume x_in_R: "x ∈ carrier R"
    and y_in_R: "y∈ carrier R"
  moreover have minus_x_in_R: "\<ominus> x ∈ carrier R"
    using a_inv_closed [OF x_in_R] .
  have prev_eq: "(x ⊕ \<ominus> x) ⊕ y = y"
    using x_in_R y_in_R
    by (simp add: r_neg l_zero)
  show ?thesis
    unfolding minus_eq [OF y_in_R x_in_R]
    unfolding a_comm [OF y_in_R minus_x_in_R]
    unfolding a_assoc [symmetric, OF x_in_R minus_x_in_R y_in_R]
    using prev_eq .
qed

text{*Corollary of 1C. It is in the library.*}
corollary (in field) minus_eq:
  "[|y ∈ carrier R; x ∈ carrier R|] ==> y \<ominus> x = y ⊕ (\<ominus> x)"    
  using minus_eq by simp

    
text{*Exercise 1D*}

lemma (in field) r_null:
  "x ∈ carrier R==> x ⊗ \<zero>=\<zero>"
  using r_null .

lemma (in field) l_null:
  "x ∈ carrier R==> \<zero> ⊗ x=\<zero>"
  using l_null .

text{*Exercise 1E*}
lemma (in field) l_minus_one:
  "x∈ carrier R ==> (\<ominus>\<one>) ⊗ x = \<ominus>x"
proof -
  assume x_in_R: "x ∈ carrier R"
  have "(\<ominus>\<one>) ⊗ x = \<ominus>(\<one> ⊗ x)"
    using l_minus[OF one_closed x_in_R] .
  also have "...= \<ominus>x" using l_one[OF x_in_R] by presburger
  finally show ?thesis .
qed

text{*Exercise 1F*}

lemma (in field) prod_minus:
  assumes x_in_R: "x ∈ carrier R" 
  and y_in_R: "y ∈ carrier R" 
  shows "(\<ominus>x) ⊗ (\<ominus>y) = x ⊗ y"
proof -
  have minus_x_in_R: "\<ominus> x ∈ carrier R" 
    and minus_y_in_R: "\<ominus> y ∈ carrier R"
    using a_inv_closed [OF x_in_R]
    using a_inv_closed [OF y_in_R] .
  show ?thesis
    unfolding l_minus [OF x_in_R minus_y_in_R]
    unfolding r_minus [OF x_in_R y_in_R] 
    unfolding minus_minus [OF m_closed [OF x_in_R y_in_R]] ..
qed

text{*Exercise 1G*}
text{*This exercise can be solved directly using integral property. However we will make it 
using @{text "Units = carrier R - {\<zero>\<^bsub>_R\<^esub>}"}. This is because field would not need to be derived from domain, the 
properties for domain follow from the assumptions of field (if we consider a field like a commutative ring in 
which @{text "Units = carrier R - {\<zero>\<^bsub>_R\<^esub>}"}*}

lemma (in field) integral:
  assumes x_y_eq_0: "x ⊗ y = \<zero>"
  and x_in_R: "x ∈ carrier R"
  and y_in_R: "y ∈ carrier R"
  shows "x = \<zero> | y = \<zero>"
proof (cases "x ≠ \<zero>")
    --"We give as a parametrer to 'cases' a boolean (x not 0);
    this will make appear two cases: when the boolean is true (case True)
    and when the boolean is false (case False).
    For us, case False will be trivial."
  case False show ?thesis
    using False --"This is the negation of the boolean that I have written in 'cases'."
    by fast --"Case False is trivial, it implies that x is zero and the lemma would be proved."
next 
    --"We want to separate in cases and for that we must use next, if not in this case, we could apply the premise False
    in case True"
  case True --"Next case: case True"
  note x_neq_0 = True
    --"With this command we are assigning a pseudonym to True because we will separate in cases y not 0 and then we will
    meet with cases True and False, again."
  show ?thesis
  proof (cases "y ≠ \<zero>")
    case False show ?thesis --"Trivial case"
      using False by simp
  next
    case True
    note y_neq_0 = True
      --"Really here we will not need the pseudonym (we will not make more distinction between cases), but we will
      use it to clarify the premises and its names."
    show ?thesis
    proof -
      have y_un: "y ∈ Units R"
        using y_in_R
        using field_Units
        using y_neq_0 by simp
      have inv_y_in_R: "inv y ∈ carrier R" 
        using Units_inv_closed [OF y_un] .
      --"Now we will begin with a 'calculation' in Isabelle. A calculation is a group of equalities which
        are linked amongst themselves. For that, we use the command 'also' and '@{text …}' "
      have "\<zero> = \<zero> ⊗ inv y"
        --"We can not use simp: left term of the equality is simpler than right one."        
        using l_null [symmetric, OF inv_y_in_R] .
      also have "… = (x ⊗ y) ⊗ inv y" 
        --"Here we make use of the original premise of the lemma: x * y = 0"
        unfolding x_y_eq_0 [symmetric] ..
      also have "… = x ⊗ (y ⊗ inv y)"
        unfolding m_assoc [OF x_in_R y_in_R inv_y_in_R] ..
      also have "… = x ⊗ \<one>"
        unfolding Units_r_inv [OF y_un] ..
      also have "… = x"
        unfolding r_one [OF x_in_R] ..
          --"At the beginning of our 'calculation' we have started with 0, so we
          have proved that 0 = x (through some intermediate steps).
          To close a 'calculation' it is used the command 'finally' which makes equal the left term of the first 'have'
          before the 'also' with the right term of the last."
      finally have "\<zero> = x" .
      --"Using 0 = x we can obtain a contradiction with our premises trivially."
      then show ?thesis using x_neq_0 by fast
    qed
  qed
qed
  
end