Theory Field_ZF (Isabelle2013: February 2013)

(*
    This file is a part of IsarMathLib - 
    a library of formalized mathematics for Isabelle/Isar.

    Copyright (C) 2005, 2006  Slawomir Kolodynski

    This program is free software; Redistribution and use in source and binary forms, 
    with or without modification, are permitted provided that the following conditions are met:

   1. Redistributions of source code must retain the above copyright notice, 
   this list of conditions and the following disclaimer.
   2. Redistributions in binary form must reproduce the above copyright notice, 
   this list of conditions and the following disclaimer in the documentation and/or 
   other materials provided with the distribution.
   3. The name of the author may not be used to endorse or promote products 
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED 
WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF 
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. 
IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, 
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; 
OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, 
WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR 
OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, 
EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

*)
header{*\isaheader{Field\_ZF.thy}*}

theory Field_ZF imports Ring_ZF

begin

text{*This theory covers basic facts about fields.*}

section{*Definition and basic properties*}

text{*In this section we define what is a field and list the basic properties
  of fields. *}

text{*Field is a notrivial commutative ring such that all 
  non-zero elements have an inverse. We define the notion of being a field as
  a statement about three sets. The first set, denoted @{text "K"} is the 
  carrier of the field. The second set, denoted @{text "A"} represents the 
  additive operation on @{text "K"} (recall that in ZF set theory functions 
  are sets). The third set @{text "M"} represents the multiplicative operation 
  on @{text "K"}.*}

definition
  "IsAfield(K,A,M) ≡ 
  (IsAring(K,A,M) ∧ (M {is commutative on} K) ∧
  TheNeutralElement(K,A) ≠ TheNeutralElement(K,M) ∧ 
  (∀a∈K. a≠TheNeutralElement(K,A)-->
  (∃b∈K. M`⟨a,b⟩ = TheNeutralElement(K,M))))"

text{*The @{text "field0"} context extends the @{text "ring0"}
  context adding field-related assumptions and notation related to the 
  multiplicative inverse. *}

locale field0 = ring0 K A M for K A M +
  assumes mult_commute: "M {is commutative on} K"
  
  assumes not_triv: "\<zero> ≠ \<one>"

  assumes inv_exists: "∀a∈K. a≠\<zero> --> (∃b∈K. a·b = \<one>)"

  fixes non_zero ("K⇣₀")
  defines non_zero_def[simp]: "K⇣₀ ≡ K-{\<zero>}"

  fixes inv ("_¯ " [96] 97)
  defines inv_def[simp]: "a¯ ≡ GroupInv(K⇣₀,restrict(M,K⇣₀×K⇣₀))`(a)";

text{*The next lemma assures us that we are talking fields 
  in the @{text "field0"} context.*}

lemma (in field0) Field_ZF_1_L1: shows "IsAfield(K,A,M)"
  using ringAssum mult_commute not_triv inv_exists IsAfield_def
  by simp;

text{*We can use theorems proven in the @{text "field0"} context whenever we
  talk about a field.*}

lemma field_field0: assumes "IsAfield(K,A,M)"
  shows "field0(K,A,M)"
  using assms IsAfield_def field0_axioms.intro ring0_def field0_def 
  by simp;

text{*Let's have an explicit statement that the multiplication
  in fields is commutative.*}

lemma (in field0) field_mult_comm: assumes "a∈K"  "b∈K"
  shows "a·b = b·a"
  using mult_commute assms IsCommutative_def by simp;

text{*Fields do not have zero divisors.*}

lemma (in field0) field_has_no_zero_divs: shows "HasNoZeroDivs(K,A,M)"
proof -
  { fix a b assume A1: "a∈K"  "b∈K" and A2: "a·b = \<zero>"  and A3: "b≠\<zero>"
    from inv_exists A1 A3 obtain c where I: "c∈K" and II: "b·c = \<one>"
      by auto;
    from A2 have "a·b·c = \<zero>·c" by simp;
    with A1 I have "a·(b·c) = \<zero>" 
      using Ring_ZF_1_L11 Ring_ZF_1_L6 by simp
    with A1 II have "a=\<zero> "using Ring_ZF_1_L3 by simp } 
  then have "∀a∈K.∀b∈K. a·b = \<zero> --> a=\<zero> ∨ b=\<zero>" by auto;
    then show ?thesis using HasNoZeroDivs_def by auto;
qed;

text{*$K_0$ (the set of nonzero field elements is closed with respect
  to multiplication.*}

lemma (in field0) Field_ZF_1_L2: 
  shows "K⇣₀ {is closed under} M"
  using Ring_ZF_1_L4 field_has_no_zero_divs Ring_ZF_1_L12
    IsOpClosed_def by auto;

text{*Any nonzero element has a right inverse that is nonzero.*}

lemma (in field0) Field_ZF_1_L3: assumes A1: "a∈K⇣₀"
  shows "∃b∈K⇣₀. a·b = \<one>"
proof -
  from inv_exists A1 obtain b where "b∈K" and "a·b = \<one>"
    by auto;
  with not_triv A1 show "∃b∈K⇣₀. a·b = \<one>"
    using Ring_ZF_1_L6 by auto;
qed;

text{*If we remove zero, the field with multiplication
  becomes a group and we can use all theorems proven in 
  @{text "group0"} context.*}

theorem (in field0) Field_ZF_1_L4: shows 
  "IsAgroup(K⇣₀,restrict(M,K⇣₀×K⇣₀))"
  "group0(K⇣₀,restrict(M,K⇣₀×K⇣₀))"
  "\<one> = TheNeutralElement(K⇣₀,restrict(M,K⇣₀×K⇣₀))"
proof-
  let ?f = "restrict(M,K⇣₀×K⇣₀)"
  have 
    "M {is associative on} K"
    "K⇣₀ ⊆ K"  "K⇣₀ {is closed under} M"
    using Field_ZF_1_L1 IsAfield_def IsAring_def IsAgroup_def 
      IsAmonoid_def Field_ZF_1_L2 by auto;
  then have "?f {is associative on} K⇣₀"
    using func_ZF_4_L3 by simp;
  moreover
  from not_triv have 
    I: "\<one>∈K⇣₀ ∧ (∀a∈K⇣₀. ?f`⟨\<one>,a⟩ = a ∧  ?f`⟨a,\<one>⟩ = a)"
    using Ring_ZF_1_L2 Ring_ZF_1_L3 by auto;
  then have "∃n∈K⇣₀. ∀a∈K⇣₀. ?f`⟨n,a⟩ = a ∧  ?f`⟨a,n⟩ = a"
    by blast;
  ultimately have II: "IsAmonoid(K⇣₀,?f)" using IsAmonoid_def
    by simp;
  then have "monoid0(K⇣₀,?f)" using monoid0_def by simp;
  moreover note I
  ultimately show "\<one> = TheNeutralElement(K⇣₀,?f)"
    by (rule monoid0.group0_1_L4);
  then have "∀a∈K⇣₀.∃b∈K⇣₀. ?f`⟨a,b⟩ =  TheNeutralElement(K⇣₀,?f)"
    using Field_ZF_1_L3 by auto;
  with II show "IsAgroup(K⇣₀,?f)" by (rule definition_of_group)
  then show "group0(K⇣₀,?f)" using group0_def by simp
qed;

text{*The inverse of a nonzero field element is nonzero.*}

lemma (in field0) Field_ZF_1_L5: assumes A1: "a∈K"  "a≠\<zero>"
  shows "a¯ ∈ K⇣₀"  "(a¯)² ∈ K⇣₀"   "a¯ ∈ K"  "a¯ ≠ \<zero>"
proof -
  from A1 have "a ∈ K⇣₀" by simp;
  then show "a¯ ∈ K⇣₀" using Field_ZF_1_L4 group0.inverse_in_group
    by auto;
  then show  "(a¯)² ∈ K⇣₀"  "a¯ ∈ K"  "a¯ ≠ \<zero>" 
    using Field_ZF_1_L2 IsOpClosed_def by auto
qed;

text{*The inverse is really the inverse.*}

lemma (in field0) Field_ZF_1_L6: assumes A1: "a∈K"  "a≠\<zero>"
  shows "a·a¯ = \<one>"  "a¯·a = \<one>"
proof -
  let ?f = "restrict(M,K⇣₀×K⇣₀)"
  from A1 have 
    "group0(K⇣₀,?f)"
    "a ∈ K⇣₀"
    using Field_ZF_1_L4 by auto;
  then have 
    "?f`⟨a,GroupInv(K⇣₀, ?f)`(a)⟩ = TheNeutralElement(K⇣₀,?f) ∧
    ?f`⟨GroupInv(K⇣₀,?f)`(a),a⟩ = TheNeutralElement(K⇣₀, ?f)"
    by (rule group0.group0_2_L6);
  with A1 show "a·a¯ = \<one>"  "a¯·a = \<one>"
    using Field_ZF_1_L5 Field_ZF_1_L4 by auto;
qed;

text{*A lemma with two field elements and cancelling.*}

lemma (in field0) Field_ZF_1_L7: assumes "a∈K" "b∈K" "b≠\<zero>"
  shows 
  "a·b·b¯ = a"
  "a·b¯·b = a"
  using assms Field_ZF_1_L5 Ring_ZF_1_L11 Field_ZF_1_L6 Ring_ZF_1_L3
  by auto;

section{*Equations and identities*}

text{*This section deals with more specialized identities that are true in 
  fields.*}

text{*$a/(a^2) = a$.*}

lemma (in field0) Field_ZF_2_L1: assumes A1: "a∈K"  "a≠\<zero>"
  shows "a·(a¯)² = a¯"
proof -
  have "a·(a¯)² = a·(a¯·a¯)" by simp;
  also from A1 have "… =  (a·a¯)·a¯" 
    using Field_ZF_1_L5 Ring_ZF_1_L11 
    by simp;
  also from A1 have "… = a¯" 
    using Field_ZF_1_L6 Field_ZF_1_L5 Ring_ZF_1_L3
    by simp;
  finally show "a·(a¯)² = a¯" by simp;
qed;

text{*If we multiply two different numbers by a nonzero number, the results 
  will be different.*}

lemma (in field0) Field_ZF_2_L2: 
  assumes "a∈K"  "b∈K"  "c∈K"  "a≠b"  "c≠\<zero>"
  shows "a·c¯ ≠ b·c¯"
  using assms field_has_no_zero_divs Field_ZF_1_L5 Ring_ZF_1_L12B
  by simp;

text{*We can put a nonzero factor on the other side of non-identity 
  (is this the best way to call it?) changing it to the inverse.*}

lemma (in field0) Field_ZF_2_L3:
  assumes A1: "a∈K"  "b∈K"  "b≠\<zero>"  "c∈K"   and A2: "a·b ≠ c"
  shows "a ≠ c·b¯"
proof -
  from A1 A2 have "a·b·b¯ ≠ c·b¯" 
    using  Ring_ZF_1_L4 Field_ZF_2_L2 by simp;
  with A1 show "a ≠ c·b¯" using Field_ZF_1_L7
    by simp;
qed;

text{*If if the inverse of $b$ is different than $a$, then the
  inverse of $a$ is different than $b$.*}

lemma (in field0) Field_ZF_2_L4:
  assumes "a∈K"  "a≠\<zero>" and "b¯ ≠ a"
  shows "a¯ ≠ b"
  using assms Field_ZF_1_L4 group0.group0_2_L11B
  by simp;

text{*An identity with two field elements, one and an inverse.*}

lemma (in field0) Field_ZF_2_L5:
  assumes "a∈K"  "b∈K" "b≠\<zero>"
  shows "(\<one> \<ra> a·b)·b¯ = a \<ra> b¯"
  using assms Ring_ZF_1_L4 Field_ZF_1_L5 Ring_ZF_1_L2 ring_oper_distr 
    Field_ZF_1_L7 Ring_ZF_1_L3 by simp;

text{*An identity with three field elements, inverse and cancelling.*}

lemma (in field0) Field_ZF_2_L6: assumes A1: "a∈K"  "b∈K"  "b≠\<zero>"  "c∈K"
  shows "a·b·(c·b¯) = a·c"
proof -
  from A1 have T: "a·b ∈ K"  "b¯ ∈ K"
    using Ring_ZF_1_L4 Field_ZF_1_L5 by auto;
  with mult_commute A1 have "a·b·(c·b¯) = a·b·(b¯·c)"
    using IsCommutative_def by simp;
  moreover
  from A1 T have "a·b ∈ K"  "b¯ ∈ K"  "c∈K"
    by auto;
  then have "a·b·b¯·c = a·b·(b¯·c)"
    by (rule Ring_ZF_1_L11);
  ultimately have "a·b·(c·b¯) = a·b·b¯·c" by simp;
  with A1 show "a·b·(c·b¯) = a·c" 
    using Field_ZF_1_L7 by simp;
qed

section{*1/0=0*}

text{* In ZF if $f: X\rightarrow Y$ and $x\notin X$ we have $f(x)=\emptyset$.
  Since $\emptyset$ (the empty set) in ZF is the same as zero of natural numbers we
  can claim that $1/0=0$ in certain sense. In this section we prove a theorem that
  makes makes it explicit.*}

text{*The next locale extends the @{text "field0"} locale to introduce notation
  for division operation.*}

locale fieldd = field0 +
  fixes division
  defines division_def[simp]: "division ≡ {⟨p,fst(p)·snd(p)¯⟩. p∈K×K⇣₀}"

  fixes fdiv (infixl "\<fd>" 95)
  defines fdiv_def[simp]: "x\<fd>y ≡ division`⟨x,y⟩"


text{*Division is a function on $K\times K_0$ with values in $K$.*}

lemma (in fieldd) div_fun: shows "division: K×K⇣₀ -> K"
proof -
  have "∀p ∈ K×K⇣₀. fst(p)·snd(p)¯ ∈ K"
  proof
    fix p assume "p ∈ K×K⇣₀"
    hence "fst(p) ∈ K" and "snd(p) ∈ K⇣₀" by auto
    then show  "fst(p)·snd(p)¯ ∈ K" using Ring_ZF_1_L4 Field_ZF_1_L5 by auto
  qed
  then have "{⟨p,fst(p)·snd(p)¯⟩. p∈K×K⇣₀}: K×K⇣₀ -> K"
    by (rule ZF_fun_from_total)
  thus ?thesis by simp
qed

text{*So, really $1/0=0$. The essential lemma is @{text "apply_0"} from standard
  Isabelle's @{text "func.thy"}.*}

theorem (in fieldd) one_over_zero: shows "\<one>\<fd>\<zero> = 0"
proof-
  have "domain(division) = K×K⇣₀" using div_fun func1_1_L1
    by simp
  hence "⟨\<one>,\<zero>⟩ ∉ domain(division)" by auto
  then show ?thesis using apply_0 by simp
qed

end