%% Examples of strategies in Field 6.0
%% Cesar Munoz 
%% http://shemesh.larc.nasa.gov/fm/pvs/Field
%% NASA LaRC

field_examples : THEORY
BEGIN

  a,b,c    : VAR real
  pa,pb,pc : VAR posreal
  nza,nzb  : VAR nzreal

  f1 : LEMMA 
    a > 1 AND b > 1 =>
    (a+1)/((a+1)/(b+1)) - b = 1
%|- f1 : PROOF (then (skeep) (field)) QED

  f2 : LEMMA 
    b >1 AND a > 1 =>
    (b-1)/((b-1)/(a-1)) - a = -1 
%|- f2 : PROOF (then (skeep) (field)) QED

  f3 : LEMMA 
    b >1 AND a > 1 =>
    (b-1)/((b-1)/(a-1)) - a < 0
%|- f3 : PROOF (then (skeep) (field)) QED

  f4 : LEMMA 
    (pa+1)/((pa+1)/(pb+1)) - pb >= 1
%|- f4 : PROOF (then (skeep) (field)) QED

  f5 : LEMMA 
    (1+pb+(pa*pb+pa))/(1+pa) - pb = 1
%|- f5 : PROOF (then (skeep) (field)) QED

  f6 : LEMMA 
    a > 1 IMPLIES
    a/((a-1) * (a+1)) - 1 /((a-1)*(a+1)) >= 1 /(a+1) - 1
%|- f6 : PROOF (then (skeep) (field)) QED

  f7: LEMMA 
    1 - pa*(pb+1) = (pa-1)/(pb+1) IMPLIES
    1/(1+ pb/(1+ 1/(1+pb))) = pa 
%|- f7 : PROOF (then (skeep) (field)) QED

  f8: LEMMA 
    1 - pa*(pb+1) = (pa-1)/(pb+1) IMPLIES
    1/(1+ pb/(1+ 1/(1+pb))) >= pa
%|- f8 : PROOF (then (skeep) (field)) QED

  f9: LEMMA 
    1 - pa*(pb+1) = (pa-1)/(pb+1) IMPLIES
    1/(1+ pb/(1+ 1/(1+pb))) <= pa   
%|- f9 : PROOF (then (skeep) (field)) QED

  f10 : LEMMA 
    a*(pa+b)/(pa+1) - b*(pa+a)/(pa+1) = 0 IMPLIES a = b
%|- f10 : PROOF (then (skeep) (field - :cancel? t)) QED

  f11 : LEMMA 
    a /= 1 IMPLIES
    1 / (1-a) = 1 + a + a * a + (a*a*a)/(1-a)
%|- f11 : PROOF (then (skeep) (field 2)) QED

  cf1 : LEMMA
    4*(pa*pb) + (pa*6)*pa = pa*((c+1)*2) =>
    2*pb + 3*pa - 1 = c
%|- cf1 : PROOF (then (skeep) (cancel-formula -)) QED

  cf2 : LEMMA 
    4*(pa*pb) + (pa*6)*pa <= pa*((c+1)*2) =>
    2*pb + 3*pa - c <= 1
%|- cf2 : PROOF (then (skeep) (cancel-formula -)) QED
 
  cf3 : LEMMA 
    4*((pa+1)*pb) + ((pa+1)*6)*(pa+1) = -(pa+1)*((c+1)*2) IMPLIES
    2*pb + 3*(pa+1) + c + 1  = 0
%|- cf3 : PROOF (then (skeep) (cancel-formula -)) QED

  cf4 : LEMMA 
   c+2 < 0 IMPLIES
   c*(c+2)*pa + pa*2*(c+2) > pb*pa*(c+2)
%|- cf4 : PROOF (then (skeep) (cancel-formula)) QED

  cf5 : LEMMA  
   c+2 < 0 AND
   c*(c+2)*pa + pa*2*(c+2) < b*pa*(c+2) IMPLIES
   b < 0
%|- cf5 : PROOF (then (skeep) (cancel-formula -2)) QED

  gr1 : LEMMA 
    a /= -4 IMPLIES
    (a+3)*(a*a+9*a+20)/(a+4) = (a+3)*(a+5)
%|- gr1 : PROOF (grind-reals) QED

  gr2 : LEMMA 
    a /= 6 AND a /= 0 AND b = 3/(a*a-6*a) IMPLIES
    (a+3)/(a*(a-6)) = 1/(a-6)+b 
%|- gr2 : PROOF (grind-reals) QED

  gr3 : LEMMA 
    a /= 6 AND a /=0 IMPLIES
    (a+3)/(a*(a-6)) = 1/(a-6)+3/(a*(a-6))
%|- gr3 : PROOF (grind-reals) QED

%%% The following examples are taken from developments at NASA LaRC
  IMPORTING reals@sqrt

  A           : VAR nzreal
  B,C,Delta,x : VAR real
  eps         : VAR {x:real|x=1 OR x=-1}

  quadratic : LEMMA 
    Delta = (B * B) - (4 * (A * C)) AND
    Delta >= 0 AND
    x = (eps * sqrt(Delta) - B) / (2 * A)
    IMPLIES A * x * x + B * x + C = 0
%|- quadratic : PROOF
%|- (then (skeep :preds? t) (replaces (-6 -8)) (field 2))
%|- QED
  
  t,vix,viy,vox,voy,s : VAR real
  D                   : VAR posreal

  kb3d : LEMMA 
    vox > 0 AND
    s*s - D*D > D AND
    s * vix * voy - s * viy * vox /= 0 AND
    ((s * s - D * D) * voy - D * vox * sqrt(s * s - D * D)) / 
     (s * (vix * voy - vox * viy)) * s * vox /= 0 AND
    voy * sqrt(s * s - D * D) - D * vox /= 0 
    IMPLIES
    (viy * sqrt(s * s - D * D) - vix * D) /
    (voy * sqrt(s * s - D * D) - vox * D)
     =
    (D * D - s * s) /
    (((s * s - D * D) * voy - D * vox * sqrt(s * s - D * D)) / 
      (s * (vix * voy - vox * viy)) * s * vox) + 
    vix / vox
%|- kb3d : PROOF (grind-reals) QED

END field_examples