:: The correctness of the Generic Algorithms of Brown and Henrici
:: concerning Addition and Multiplication in Fraction Fields
::  by Christoph Schwarzweller
::
:: Received June 16, 1997
:: Copyright (c) 1997-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies BINOP_1, VECTSP_1, XBOOLE_0, ALGSTR_0, SUBSET_1, MESFUNC1,
      RELAT_1, LATTICES, ARYTM_3, FUNCSDOM, VECTSP_2, SUPINF_2, CARD_1,
      STRUCT_0, RLVECT_1, ARYTM_1, GROUP_1, EQREL_1, TARSKI, SETFAM_1,
      MSSUBFAM, INT_2, GCD_1, FUNCT_7, NUMBERS;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, STRUCT_0, ALGSTR_0,
      RLVECT_1, GROUP_1, VECTSP_2, VECTSP_1;
 constructors BINOP_2, VECTSP_2, MONOID_0;
 registrations XBOOLE_0, SUBSET_1, MEMBERED, STRUCT_0, VECTSP_1, MONOID_0,
      XREAL_0;
 requirements SUBSET, BOOLE;


begin :: Basics

reserve X,Y for set;

:: Theorems about Integral Domains

registration
  cluster commutative right_unital -> left_unital for non empty multLoopStr;
end;

registration
  cluster commutative right-distributive -> distributive for non empty
    doubleLoopStr;
  cluster commutative left-distributive -> distributive for non empty
    doubleLoopStr;
end;

registration
  cluster -> well-unital for Ring;
end;

registration
  cluster F_Real -> domRing-like;
end;

registration
  cluster strict Abelian add-associative right_zeroed right_complementable
associative commutative domRing-like distributive well-unital non degenerated
    almost_left_invertible for 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 multMagma;
  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 right_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;
end;

notation
  let R be non empty multLoopStr;
  let x,y be Element of R;
  antonym x is_not_associated_to y for x is_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;

registration
  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;

registration
  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;

registration
  cluster gcd-like for domRing;
end;

registration
  cluster gcd-like associative commutative well-unital for
non empty multLoopStr;
end;

registration
  cluster gcd-like associative commutative well-unital for non empty
    multLoopStr_0;
end;

registration
  cluster -> gcd-like for almost_left_invertible add-associative right_zeroed
    right_complementable left_unital well-unital left-distributive
    right-distributive commutative non empty doubleLoopStr;
end;

registration
  cluster gcd-like associative commutative well-unital domRing-like unital
    distributive non degenerated Abelian add-associative right_zeroed
    right_complementable for 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

theorem :: GCD_1:28
  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:29
  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:30
  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:31
  for Amp being AmpleSet of R holds gcd(0.R,0.R,Amp) = 0.R;

theorem :: GCD_1:32
  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:33
  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:34
  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:35
  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:36
  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:37
  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:38
  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:39
  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

::$N Brown Theorem
theorem :: GCD_1:40
  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 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);

::$N Henrici Theorem
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/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:42
  for Amp,Amp9 being AmpleSet of R for x,y being Element of R st x
  ,y are_canonical_wrt Amp holds x,y are_canonical_wrt Amp9;

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:43
  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 that
 r1,r2 are_co-prime and
 s1,s2 are_co-prime and
 r2 = NF(r2,Amp) and
 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 that
 r1,r2 are_co-prime and
 s1,s2 are_co-prime and
 r2 = NF(r2,Amp) and
 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:44
  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:45
  for Amp being AmpleSet of R for r1,r2,s1,s2 being Element of R holds
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 that
 r1,r2 are_co-prime and
 s1,s2 are_co-prime and
 r2 = NF(r2,Amp) and
 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: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 mult1(r1,r2,s1,s2,Amp),mult2(r1,r2,s1,s2,Amp) are_normalized_wrt
  Amp;

theorem :: GCD_1:47
  for Amp being AmpleSet of R for r1,r2,s1,s2 being Element of R holds
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);

theorem :: GCD_1:48
  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;

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