The abstract of the Mizar article:

The Correctness of the Generic Algorithms of Brown and Henrici Concerning Addition and Multiplication in Fraction Fields

by

Christoph Schwarzweller

Received June 16, 1997

MML identifier: GCD_1

[ Mizar article, MML identifier index ]

environ

 vocabulary BINOP_1, VECTSP_1, LATTICES, ALGSTR_2, VECTSP_2, FUNCSDOM,
      RLVECT_1, FUNCT_1, ARYTM_3, ARYTM_1, GROUP_1, EQREL_1, BOOLE, SETFAM_1,
      COHSP_1, INT_2, RELAT_1, GCD_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, REAL_1, STRUCT_0, RLVECT_1, VECTSP_2,
      VECTSP_1, FUNCSDOM, BINOP_1;
 constructors FUNCSDOM, ALGSTR_2, VECTSP_2, REAL_1, MEMBERED;
 clusters STRUCT_0, VECTSP_1, VECTSP_2, SUBSET_1, ALGSTR_1, XBOOLE_0, MEMBERED;
 requirements SUBSET, BOOLE;


begin :: Basics

reserve X,Y for set;

:: Theorems about Integral Domains
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

definition
 cluster commutative right_unital -> left_unital (non empty multLoopStr);
end;

definition
 cluster commutative right-distributive -> distributive
    (non empty doubleLoopStr);
 cluster commutative left-distributive ->
            distributive (non empty doubleLoopStr);
end;

definition
 cluster -> well-unital Ring;
end;

definition
 cluster F_Real -> domRing-like;
end;

definition
 cluster strict Abelian add-associative right_zeroed right_complementable
         associative commutative domRing-like distributive
         well-unital non degenerated Field-like (non empty doubleLoopStr);
end;

reserve R for domRing-like commutative Ring;
reserve c for Element of R;

theorem :: GCD_1:1
for R being domRing-like commutative Ring
for a,b,c being Element of R holds
a <> 0.R implies ((a * b = a * c implies b = c) &
(b * a = c * a implies b = c));

:: Definition of Divisibility
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

definition
let R be non empty HGrStr;
let x,y be Element of R;
 pred x divides y means
:: GCD_1:def 1
 ex z being Element of R st y = x * z;
end;

definition
let R be well-unital (non empty multLoopStr);
let x,y be Element of R;
 redefine pred x divides y;
 reflexivity;
end;

definition
let R be non empty multLoopStr;
let x be Element of R;
 attr x is unital means
:: GCD_1:def 2
 x divides 1_ R;
end;

definition
let R be non empty multLoopStr;
let x,y be Element of R;
 pred x is_associated_to y means
:: GCD_1:def 3
 x divides y & y divides x;
 symmetry;
antonym x is_not_associated_to y;
end;

definition
let R be well-unital (non empty multLoopStr);
let x,y be Element of R;
 redefine pred x is_associated_to y;
 reflexivity;
end;

definition
let R be domRing-like commutative Ring;
let x,y be Element of R;
assume  y divides x;
assume  y <> 0.R;
  func x/y -> Element of R means
:: GCD_1:def 4
  it * y = x;
end;

:: Some Lemmata about Divisibility
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

theorem :: GCD_1:2
for R being associative (non empty multLoopStr)
for a,b,c being Element of R holds
a divides b & b divides c implies a divides c;

theorem :: GCD_1:3
for R being commutative associative (non empty multLoopStr)
for a,b,c,d being Element of R holds
(b divides a & d divides c) implies (b * d) divides (a * c);

theorem :: GCD_1:4
for R being associative (non empty multLoopStr)
for a,b,c being Element of R holds
a is_associated_to b & b is_associated_to c
 implies a is_associated_to c;

theorem :: GCD_1:5
for R being associative (non empty multLoopStr)
for a,b,c being Element of R holds
a divides b implies c * a divides c * b;

theorem :: GCD_1:6
for R being non empty multLoopStr
for a,b being Element of R holds
a divides a * b & (R is commutative implies b divides a * b);

theorem :: GCD_1:7
for R being associative (non empty multLoopStr)
for a,b,c being Element of R holds
a divides b implies a divides b * c;

theorem :: GCD_1:8
for a,b being Element of R holds
(b divides a & b <> 0.R)
implies (a/b = 0.R iff a = 0.R);

theorem :: GCD_1:9
for a being Element of R holds
a <> 0.R implies a/a = 1_ R;

theorem :: GCD_1:10
for R being non degenerated domRing-like commutative Ring
for a being Element of R holds a/1_ R = a;

theorem :: GCD_1:11
for a,b,c being Element of R holds
c <> 0.R implies
(((c divides (a * b) & c divides a) implies (a * b) / c = (a / c) * b) &
 ((c divides (a * b) & c divides b) implies (a * b) / c = a * (b / c)));

theorem :: GCD_1:12
for a,b,c being Element of R holds
(c <> 0.R & c divides a & c divides b & c divides (a + b))
implies (a/c) + (b/c) = (a + b)/c;

theorem :: GCD_1:13
  for a,b,c being Element of R holds
(c <> 0.R & c divides a & c divides b) implies
(a/c = b/c iff a = b);

theorem :: GCD_1:14
for a,b,c,d being Element of R holds
(b <> 0.R & d <> 0.R & b divides a & d divides c)
implies (a/b) * (c/d) = (a * c) / (b * d);

theorem :: GCD_1:15
for a,b,c being Element of R holds
((a <> 0.R) & ((a * b) divides (a * c)))
implies (b divides c);

theorem :: GCD_1:16
  for a being Element of R holds
a is_associated_to 0.R implies a = 0.R;

theorem :: GCD_1:17
for a,b being Element of R holds
(a <> 0.R & a * b = a) implies b = 1_ R;

theorem :: GCD_1:18
for a,b being Element of R holds
a is_associated_to b iff (ex c st (c is unital & a * c = b));

theorem :: GCD_1:19
for a,b,c being Element of R holds
c <> 0.R & c * a is_associated_to c * b
implies a is_associated_to b;

begin

:: Definition of Ample Set
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

definition
let R be non empty multLoopStr;
let a be Element of R;
  func Class a -> Subset of R means
:: GCD_1:def 5
  for b being Element of R holds
   b in it iff b is_associated_to a;
end;

definition
let R be well-unital (non empty multLoopStr);
let a be Element of R;
  cluster Class a -> non empty;
end;

theorem :: GCD_1:20
for R being associative (non empty multLoopStr)
for a,b being Element of R holds
Class a meets Class b implies Class a = Class b;

definition
  let R be non empty multLoopStr;
  func Classes R -> Subset-Family of R means
:: GCD_1:def 6
  for A being Subset of R holds
   A in it iff (ex a being Element of R st A = Class a);
end;

definition let R be non empty multLoopStr;
 cluster Classes R -> non empty;
end;

theorem :: GCD_1:21
for R being well-unital (non empty multLoopStr)
for X being Subset of R holds
X in Classes R implies X is non empty;

definition
let R be associative well-unital (non empty multLoopStr);
mode Am of R -> non empty Subset of R means
:: GCD_1:def 7
  (for a being Element of R ex z being Element of it
   st z is_associated_to a) &
  (for x,y being Element of it holds x <> y implies
   x is_not_associated_to y);
end;

definition
let R be associative well-unital (non empty multLoopStr);
mode AmpleSet of R -> non empty Subset of R means
:: GCD_1:def 8
  it is Am of R & 1_ R in it;
end;

theorem :: GCD_1:22
for R being associative well-unital (non empty multLoopStr)
for Amp being AmpleSet of R holds
(1_ R in Amp) &
(for a being Element of R ex z being Element of Amp
 st z is_associated_to a) &
(for x,y being Element of Amp holds x <> y implies
 x is_not_associated_to y);

theorem :: GCD_1:23
 for R being associative well-unital (non empty multLoopStr)
for Amp being AmpleSet of R
for x,y being Element of Amp holds
x is_associated_to y implies x = y;

theorem :: GCD_1:24
for Amp being AmpleSet of R holds
0.R is Element of Amp;

:: Definition of Normalform
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

definition
let R be associative well-unital (non empty multLoopStr);
let Amp be AmpleSet of R;
let x be Element of R;
 func NF(x,Amp) -> Element of R means
:: GCD_1:def 9
 it in Amp & it is_associated_to x;
end;

theorem :: GCD_1:25
for Amp being AmpleSet of R holds
NF(0.R,Amp) = 0.R & NF(1_ R,Amp) = 1_ R;

theorem :: GCD_1:26
 for Amp being AmpleSet of R
for a being Element of R holds
a in Amp iff a = NF(a,Amp);

:: Definition of multiplicative AmpleSet
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

definition
let R be associative well-unital (non empty multLoopStr);
let Amp be AmpleSet of R;
  attr Amp is multiplicative means
:: GCD_1:def 10
  for x,y being Element of Amp holds x * y in Amp;
end;

theorem :: GCD_1:27
for Amp being AmpleSet of R holds
Amp is multiplicative implies
(for x,y being Element of Amp holds
 (y divides x & y <> 0.R) implies x/y in Amp);

begin

:: Definition of GCD-Domain
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

definition
let R be non empty multLoopStr;
  attr R is gcd-like means
:: GCD_1:def 11
  for x,y being Element of R
   ex z being Element of R st
         z divides x &
         z divides y &
         (for zz being Element of R
          st (zz divides x & zz divides y)
          holds (zz divides z));
end;

definition
  cluster gcd-like domRing;
end;

definition
  cluster gcd-like associative commutative well-unital (non empty multLoopStr);
end;

definition
  cluster gcd-like associative commutative well-unital
    (non empty multLoopStr_0);
end;

definition
 cluster -> gcd-like
            (Field-like add-associative right_zeroed right_complementable
            left_unital right_unital left-distributive right-distributive
            commutative (non empty doubleLoopStr));
end;

definition
  cluster gcd-like associative commutative well-unital domRing-like
          well-unital distributive non degenerated
          Abelian add-associative right_zeroed right_complementable
          (non empty doubleLoopStr);
end;

definition
  mode gcdDomain is gcd-like domRing-like non degenerated commutative Ring;
end;

definition
let R be gcd-like associative well-unital (non empty multLoopStr);
let Amp be AmpleSet of R;
let x,y be Element of R;
  func gcd(x,y,Amp) -> Element of R means
:: GCD_1:def 12
         it in Amp &
         it divides x &
         it divides y &
        (for z being Element of R
         st (z divides x & z divides y)
         holds z divides it);
end;

reserve R for gcdDomain;

:: Lemmata about GCD
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

canceled;

theorem :: GCD_1:29
for Amp being AmpleSet of R
for a,b,c being Element of R holds
c divides gcd(a,b,Amp) implies (c divides a & c divides b);

theorem :: GCD_1:30
for Amp being AmpleSet of R
for a,b being Element of R holds
gcd(a,b,Amp) = gcd(b,a,Amp);

theorem :: GCD_1:31
for Amp being AmpleSet of R
for a being Element of R holds
gcd(a,0.R,Amp) = NF(a,Amp) &
gcd(0.R,a,Amp) = NF(a,Amp);

theorem :: GCD_1:32
for Amp being AmpleSet of R holds
gcd(0.R,0.R,Amp) = 0.R;

theorem :: GCD_1:33
for Amp being AmpleSet of R
for a being Element of R holds
gcd(a,1_ R,Amp) = 1_ R & gcd(1_ R,a,Amp) = 1_ R;

theorem :: GCD_1:34
for Amp being AmpleSet of R
for a,b being Element of R holds
gcd(a,b,Amp) = 0.R iff (a = 0.R & b = 0.R);

theorem :: GCD_1:35
for Amp being AmpleSet of R
for a,b,c being Element of R holds
(b is_associated_to c) implies
((gcd(a,b,Amp) is_associated_to gcd(a,c,Amp)) &
 (gcd(b,a,Amp) is_associated_to gcd(c,a,Amp)));

:: Main Theorems
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

theorem :: GCD_1:36
for Amp being AmpleSet of R
for a,b,c being Element of R holds
gcd(gcd(a,b,Amp),c,Amp) = gcd(a,gcd(b,c,Amp),Amp);

theorem :: GCD_1:37
for Amp being AmpleSet of R
for a,b,c being Element of R holds
gcd(a * c,b * c,Amp) is_associated_to (c * gcd(a,b,Amp));

theorem :: GCD_1:38
for Amp being AmpleSet of R
for a,b,c being Element of R holds
(gcd(a,b,Amp) = 1_ R) implies (gcd(a,(b * c),Amp) = gcd(a,c,Amp));

theorem :: GCD_1:39
for Amp being AmpleSet of R
for a,b,c being Element of R holds
((c = gcd(a,b,Amp)) & (c <> 0.R)) implies
gcd((a/c),(b/c),Amp) = 1_ R;

theorem :: GCD_1:40
for Amp being AmpleSet of R
for a,b,c being Element of R holds
gcd((a + (b * c)),c,Amp) = gcd(a,c,Amp);


begin

:: Brown & Henrici
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

theorem :: GCD_1:41
for Amp being AmpleSet of R
for r1,r2,s1,s2 being Element of R holds
(gcd(r1,r2,Amp) = 1_ R & gcd(s1,s2,Amp) = 1_ R &
 r2 <> 0.R & s2 <> 0.R) implies
gcd(((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp)))),
    (r2 * (s2/gcd(r2,s2,Amp))),Amp) =
gcd(((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp)))),
    gcd(r2,s2,Amp),Amp);

theorem :: GCD_1:42
for Amp being AmpleSet of R
for r1,r2,s1,s2 being Element of R holds
(gcd(r1,r2,Amp) = 1_ R & gcd(s1,s2,Amp) = 1_ R &
 r2 <> 0.R & s2 <> 0.R) implies
gcd(((r1/gcd(r1,s2,Amp)) * (s1/gcd(s1,r2,Amp))),
    ((r2/gcd(s1,r2,Amp)) * (s2/gcd(r1,s2,Amp))),Amp) = 1_ R;

begin

:: Properties of the Algorithms
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

definition
let R be gcd-like associative well-unital (non empty multLoopStr);
let Amp be AmpleSet of R;
let x,y be Element of R;
  pred x,y are_canonical_wrt Amp means
:: GCD_1:def 13
  gcd(x,y,Amp) = 1_ R;
end;

theorem :: GCD_1:43
for Amp,Amp' being AmpleSet of R
for x,y being Element of R holds
x,y are_canonical_wrt Amp iff x,y are_canonical_wrt Amp';

definition
let R be gcd-like associative well-unital (non empty multLoopStr);
let x,y be Element of R;
 pred x,y are_co-prime means
:: GCD_1:def 14
 ex Amp being AmpleSet of R st gcd(x,y,Amp) = 1_ R;
end;

definition
let R be gcdDomain;
let x,y be Element of R;
 redefine pred x,y are_co-prime;
 symmetry;
end;

theorem :: GCD_1:44
for Amp being AmpleSet of R
for x,y being Element of R holds
x,y are_co-prime implies gcd(x,y,Amp) = 1_ R;

definition
let R be gcd-like associative well-unital (non empty multLoopStr_0);
let Amp be AmpleSet of R;
let x,y be Element of R;
  pred x,y are_normalized_wrt Amp means
:: GCD_1:def 15
  gcd(x,y,Amp) = 1_ R & y in Amp & y <> 0.R;
end;

:: Addition
:::::::::::

definition
let R be gcdDomain;
let Amp be AmpleSet of R;
let r1,r2,s1,s2 be Element of R;
assume  r1,r2 are_co-prime & s1,s2 are_co-prime &
          r2 = NF(r2,Amp) & s2 = NF(s2,Amp);
  func add1(r1,r2,s1,s2,Amp) -> Element of R equals
:: GCD_1:def 16
  s1 if r1 = 0.R,
  r1 if s1 = 0.R,
  (r1 * s2) + (r2 * s1) if gcd(r2,s2,Amp) = 1_ R,
  0.R if (r1 * (s2/gcd(r2,s2,Amp))) +
                (s1 * (r2/gcd(r2,s2,Amp))) = 0.R
  otherwise ((r1 * (s2/gcd(r2,s2,Amp))) +
                  (s1 * (r2/gcd(r2,s2,Amp)))) /
                 gcd((r1 * (s2/gcd(r2,s2,Amp))) +
                     (s1 * (r2/gcd(r2,s2,Amp))),
                     gcd(r2,s2,Amp),Amp);
end;

definition
let R be gcdDomain;
let Amp be AmpleSet of R;
let r1,r2,s1,s2 be Element of R;
assume  r1,r2 are_co-prime & s1,s2 are_co-prime &
          r2 = NF(r2,Amp) & s2 = NF(s2,Amp);
  func add2(r1,r2,s1,s2,Amp) -> Element of R equals
:: GCD_1:def 17
  s2 if r1 = 0.R,
  r2 if s1 = 0.R,
  r2 * s2 if gcd(r2,s2,Amp) = 1_ R,
  1_ R if (r1 * (s2/gcd(r2,s2,Amp))) +
                (s1 * (r2/gcd(r2,s2,Amp))) = 0.R
                otherwise
  (r2 * (s2/gcd(r2,s2,Amp))) / gcd((r1 * (s2/gcd(r2,s2,Amp))) +
          (s1 * (r2/gcd(r2,s2,Amp))), gcd(r2,s2,Amp),Amp);
end;

theorem :: GCD_1:45
  for Amp being AmpleSet of R
for r1,r2,s1,s2 being Element of R holds
(Amp is multiplicative &
 r1,r2 are_normalized_wrt Amp &
 s1,s2 are_normalized_wrt Amp)
implies
 add1(r1,r2,s1,s2,Amp),add2(r1,r2,s1,s2,Amp)
 are_normalized_wrt Amp;

theorem :: GCD_1:46
  for Amp being AmpleSet of R
for r1,r2,s1,s2 being Element of R holds
(Amp is multiplicative &
 r1,r2 are_normalized_wrt Amp &
 s1,s2 are_normalized_wrt Amp)
implies
 add1(r1,r2,s1,s2,Amp) * (r2 * s2) =
 add2(r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2));

:: Multiplication
:::::::::::::::::

definition
let R be gcdDomain;
let Amp be AmpleSet of R;
let r1,r2,s1,s2 be Element of R;
  func mult1(r1,r2,s1,s2,Amp) -> Element of R equals
:: GCD_1:def 18
  0.R if r1 = 0.R or s1 = 0.R,
  r1 * s1 if r2 = 1_ R & s2 = 1_ R,
  (r1 * s1)/gcd(r1,s2,Amp) if s2 <> 0.R & r2 = 1_ R,
  (r1 * s1)/gcd(s1,r2,Amp) if r2 <> 0.R & s2 = 1_ R
  otherwise (r1/gcd(r1,s2,Amp)) * (s1/gcd(s1,r2,Amp));
end;

definition
let R be gcdDomain;
let Amp be AmpleSet of R;
let r1,r2,s1,s2 be Element of R;
assume  r1,r2 are_co-prime & s1,s2 are_co-prime &
           r2 = NF(r2,Amp) & s2 = NF(s2,Amp);
  func mult2(r1,r2,s1,s2,Amp) -> Element of R equals
:: GCD_1:def 19
  1_ R if r1 = 0.R or s1 = 0.R,
  1_ R if r2 = 1_ R & s2 = 1_ R,
  s2/gcd(r1,s2,Amp) if s2 <> 0.R & r2 = 1_ R,
  r2/gcd(s1,r2,Amp) if r2 <> 0.R & s2 = 1_ R
  otherwise (r2/gcd(s1,r2,Amp)) * (s2/gcd(r1,s2,Amp));
end;

theorem :: GCD_1:47
  for Amp being AmpleSet of R
for r1,r2,s1,s2 being Element of R holds
(Amp is multiplicative &
 r1,r2 are_normalized_wrt Amp &
 s1,s2 are_normalized_wrt Amp)
implies
 mult1(r1,r2,s1,s2,Amp),mult2(r1,r2,s1,s2,Amp)
 are_normalized_wrt Amp;

theorem :: GCD_1:48
  for Amp being AmpleSet of R
for r1,r2,s1,s2 being Element of R holds
(Amp is multiplicative &
 r1,r2 are_normalized_wrt Amp &
 s1,s2 are_normalized_wrt Amp)
implies
 mult1(r1,r2,s1,s2,Amp) * (r2 * s2) =
 mult2(r1,r2,s1,s2,Amp) * (r1 * s1);

canceled 2;

theorem :: GCD_1:51
   for F be add-associative right_zeroed right_complementable Abelian
        distributive (non empty doubleLoopStr),
     x,y being Element of F
  holds (-x)*y = -x*y & x*(-y) = -x*y;

canceled;

theorem :: GCD_1:53
  for F being Field-like commutative Ring
for a, b being Element of F st a <> 0.F & b <> 0.F holds
a"*b" = (b*a)";