:: Euclide Algorithm
::  by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received October 8, 1993
:: Copyright (c) 1993 Association of Mizar Users

environ

 vocabularies INT_1, NAT_1, ARYTM_3, ARYTM_1, ABSVALUE, FUNCT_1, CQC_LANG,
      AMI_3, AMI_1, CAT_1, FUNCT_4, RELAT_1, BOOLE, AMI_2, INT_2, PARTFUN1,
      FUNCOP_1, AMI_4;
 notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, NUMBERS, XCMPLX_0, RELAT_1,
      FUNCT_1, FUNCT_2, INT_1, NAT_1, NAT_D, FUNCOP_1, INT_2, STRUCT_0,
      PARTFUN1, AMI_1, AMI_3, XXREAL_0;
 constructors ENUMSET1, FRAENKEL, XXREAL_0, REAL_1, NAT_1, NAT_D, INT_2, AMI_3;
 registrations SUBSET_1, SETFAM_1, ORDINAL1, RELSET_1, ARYTM_3, FRAENKEL,
      NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, CARD_3, STRUCT_0, AMI_3, AMI_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: Preliminaries

reserve i,j,k for Element of NAT;

scheme :: AMI_4:sch 1
 Euklides' { F(Element of NAT)->Element of NAT,G(Element of NAT)->
Element of NAT,a()->Element of NAT,b()->Element of NAT } :
  ex k st F(k) = a() hcf b() & G(k) = 0
   provided
 0 < b() and
 b() < a() and
 F(0) = a() and
 G(0) = b() and
 for k st G(k) > 0 holds F(k+1) = G(k) & G(k+1) = F(k) mod G(k);

begin :: Euclide algorithm

definition
 func Euclide-Algorithm -> programmed FinPartState of SCM equals
:: AMI_4:def 1

 (il.0 .--> (dl.2 := dl.1)) +*
  ((il.1 .--> Divide(dl.0,dl.1)) +*
   ((il.2 .--> (dl.0 := dl.2)) +*
    ((il.3 .--> (dl.1 >0_goto il.0)) +*
     (il.4 .--> halt SCM))));
end;

canceled 3;

theorem :: AMI_4:4
 dom (Euclide-Algorithm qua Function) = { il.0,il.1,il.2,il.3,il.4 };

begin :: Natural semantics of the program

theorem :: AMI_4:5
  for s being State of SCM st Euclide-Algorithm c= s
  for k st IC (Computation s).k = il.0
  holds IC (Computation s).(k+1) = il.1 &
   (Computation s).(k+1).dl.0 = (Computation s).k.dl.0 &
   (Computation s).(k+1).dl.1 = (Computation s).k.dl.1 &
   (Computation s).(k+1).dl.2 = (Computation s).k.dl.1;

theorem :: AMI_4:6
  for s being State of SCM st Euclide-Algorithm c= s
  for k st IC (Computation s).k = il.1
  holds IC (Computation s).(k+1) = il.2 &
   (Computation s).(k+1).dl.0 =
    (Computation s).k.dl.0 div (Computation s).k.dl.1 &
   (Computation s).(k+1).dl.1 =
    (Computation s).k.dl.0 mod (Computation s).k.dl.1 &
   (Computation s).(k+1).dl.2 = (Computation s).k.dl.2;

theorem :: AMI_4:7
  for s being State of SCM st Euclide-Algorithm c= s
  for k st IC (Computation s).k = il.2
  holds IC (Computation s).(k+1) = il.3 &
   (Computation s).(k+1).dl.0 = (Computation s).k.dl.2 &
   (Computation s).(k+1).dl.1 = (Computation s).k.dl.1 &
   (Computation s).(k+1).dl.2 = (Computation s).k.dl.2;

theorem :: AMI_4:8
  for s being State of SCM st Euclide-Algorithm c= s
  for k st IC (Computation s).k = il.3
  holds
   ((Computation s).k.dl.1 > 0 implies IC (Computation s).(k+1) = il.0) &
   ((Computation s).k.dl.1 <= 0 implies IC (Computation s).(k+1) = il.4) &
   (Computation s).(k+1).dl.0 = (Computation s).k.dl.0 &
   (Computation s).(k+1).dl.1 = (Computation s).k.dl.1;

theorem :: AMI_4:9
  for s being State of SCM st Euclide-Algorithm c= s
  for k,i st IC (Computation s).k = il.4
  holds (Computation s).(k+i) = (Computation s).k;

theorem :: AMI_4:10
  for s being State of SCM st s starts_at il.0 & Euclide-Algorithm c= s
  for x, y being Integer st s.dl.0 = x & s.dl.1 = y & x > 0 & y > 0
  holds (Result s).dl.0 = x gcd y;

definition
 func Euclide-Function -> PartFunc of FinPartSt SCM, FinPartSt SCM means
:: AMI_4:def 2
  for p,q being FinPartState of SCM holds [p,q] in it
   iff ex x,y being Integer st x > 0 & y > 0 &
    p = (dl.0,dl.1) --> (x,y) & q = dl.0 .--> (x gcd y);
end;

theorem :: AMI_4:11
 for p being set holds p in dom Euclide-Function iff
   ex x,y being Integer st x > 0 & y > 0 & p = (dl.0,dl.1) --> (x,y);

theorem :: AMI_4:12
 for i,j being Integer st i > 0 & j > 0 holds
  Euclide-Function.((dl.0,dl.1) --> (i,j)) = dl.0 .--> (i gcd j);

theorem :: AMI_4:13
    (Start-At il.0) +* Euclide-Algorithm computes Euclide-Function;