mod Ex01b logic: 'cl'

incl Mtex

incl Mauxb

loc rem 
  1. CVICENIE Z PREDMETU SPECIFIKACIA A VERIFIKACIA PROGRAMOV

loc rem 
  VASE MENO: ?
  SKUPINA: ?
  VERZIA CL: 5.81.16
  DATUM: stvrtok 17.2.2005
  ******************************************************************************
  SKUSKA (toto je len zakladny ramec, viz. tiez 1. prednaska):
   A = aspon 90 bodov
   B = aspon 80 bodov
   C = aspon 70 bodov
   D = aspon 60 bodov
   E = aspon 50 bodov
  ******************************************************************************
  PMAIL: svp@nw.fmph.uniba.sk
         SUBJECT: prihlasenie sa do skupiny [2i1,2i2,2i3,2i4]
  WWW: http://www.ii.fmph.uniba.sk/cl/view.php/courses/svp

rem 
  \para \bf  Uvodna poznamka.  \end Toto cvicenie je venovane explicitnym 
  definiciam a primitivnej rekurzii. Zadanie sa sklada z tychto suborov: 
  \items 
   \item \para Subor \it  mtex.cl  \end obsahuje makra pre CL-TeX. 
   \item \para Subor(y) \it  maux*.cl  \end obsahuju definicie a vlastnosti 
         pomocnych funkcii a predikatov. 
   \item \para Subor(y) \it  ex01*.cl  \end obsahuju ulohy, ktore mate riesit na 
         tomto cviceni. 
  \end
  \para Tieto subory sa musia skompilovat v spravnom poradi; presny postup je 
  uvedeny v subore \it  readme.txt  \end. 

fun/0 Foo 'Tex_f0_foo'
  Foo = 0

pred/0 Poo 'Tex_p0_poo'
  Poo <-> \f

loc rem 
  ******************************************************************************
  ********************************* EXERCISES **********************************
  ******************************************************************************

rem 
  \para \bf  Literature.  \end 
  \items 
   \item \para \it  [1]  \end J. Komara and P. J. Voda. Metamathematics of 
         Computer Programming. 2001. 
  \end

rem 
  \para \bf  Chapter. Numeric Programs.  \end 

rem 
  \para \bf  Section. Primitive Recursion.  \end 

rem 
  \para \bf  [CL] Mathematical induction.  \end Syntax: 
  \items 
   \item \para The command \it  ind  \end \ft N \end \it  ;  \end \ft x \end 
         invokes mathematical induction on \ft x \end with the induction formula 
         \ft Tex2_bappl1(Tex0_phi,x) \end, where 
         \ft Tex2_bappl1(Tex0_phi,x) \end is the current goal possibly with 
         additional free variables as parameters. 
   \item \para The command \it  ind  \end \ft N \end \it  ;  \end \ft x \end 
         \it  ;  \end \ft Tex1_hat(y) \end invokes mathematical induction on 
         \ft x \end with the induction formula 
         \ft Tex2_forall(Tex1_hat(y),Tex3_bappl2(Tex0_phi,x,Tex1_hat(y))) \end, 
         where \ft Tex3_bappl2(Tex0_phi,x,Tex1_hat(y)) \end is the current goal 
         possibly with additional free variables as parameters. 
  \end

rem 
  \para \bf  Exponentiation.  \end 

fun/2 Exp 'Tex_f2_pa_exp'
  Exp(x,0) = 1
  Exp(x,y+1) = x*Exp(x,y)

rem 
  \para \bf  Exercise.  \end Prove 
  \eq Exp_zero
    Exp(x,y) = 0 <-> x = 0 & y > 0
  \end
  \eq Exp_one
    Exp(x,y) = 1 <-> x = 1 \/ y = 0
  \end

thm Exp_zero
  Exp(x,y) = 0 <-> x = 0 & y > 0
proof 
 ind N; y @ 0; y
  proved
  split Exp(x,y) = 0 <-> x = 0 & y > 0.1,0,2,0,0
   proved
   proved...

thm Exp_one
  Exp(x,y) = 1 <-> x = 1 \/ y = 0
proof 
 ind N; y @ 0; y
  proved
  split Exp(x,y) = 1 <-> x = 1 \/ y = 0.1,0,2,0,0
   proved
   proved...

rem 
  \para \bf  Exercise.  \end Prove 
  \eq Exp_plus
    Exp(x,y+z) = Exp(x,y)*Exp(x,z)
  \end
  \eq Exp_minus
    x > 0 & y >= z -> Exp(x,y-z) = Exp(x,y)/Exp(x,z)
  \end

thm Exp_plus
  Exp(x,y+z) = Exp(x,y)*Exp(x,z)
proof 
 ind N; y @ 0; y
  proved
  proved..

thm Exp_minus
  x > 0 & y >= z -> Exp(x,y-z) = Exp(x,y)/Exp(x,z)
proof 
 ind N; y; z @ 0; y
  proved
  case N; z @ 0; z1
   proved
   inst \a z(y >= z -> Exp(x,y-z) = Exp(x,y)/Exp(x,z)); z1 proved....

rem 
  \para \bf  Exercise.  \end Prove 
  \eq Exp_eq
    x > 1 -> Exp(x,y) = Exp(x,z) <-> y = z
  \end
  \eq Exp_le
    x > 1 -> Exp(x,y) <= Exp(x,z) <-> y <= z
  \end
  \eq Exp_lt
    x > 1 -> Exp(x,y) < Exp(x,z) <-> y < z
  \end

thm Exp_eq
  x > 1 -> Exp(x,y) = Exp(x,z) <-> y = z
proof 
 split* Exp(x,y) = Exp(x,z) <-> y = z.2,0,0
  ind N; y; z @ 0; y
   cut z = 0
    proved
    proved.
   case N; z @ 0; z1
    proved
    inst \a z(Exp(x,z1) = Exp(x,z) -> y = z); z1 proved...
  proved..

thm Exp_le
  x > 1 -> Exp(x,y) <= Exp(x,z) <-> y <= z
proof 
 ind N; z; y @ 0; z
  cut y = 0
   proved
   use Exp_zero.0; x; y-1 proved..
  case N; y @ 0; y1
   inst \a y(Exp(x,y) <= Exp(x,z) <-> y <= z).0; 0 proved.
   inst \a y(Exp(x,y) <= Exp(x,z) <-> y <= z).0; y1 proved....

thm Exp_lt
  x > 1 -> Exp(x,y) < Exp(x,z) <-> y < z
proof 
 ind N; z; y @ 0; z
  use Exp_zero.0; x; y proved.
  case N; y @ 0; y1
   use Exp_zero.0; x; z proved.
   inst \a y(Exp(x,y) < Exp(x,z) <-> y < z).0; y1 proved....

rem 
  \para \bf  Exercise.  \end Prove 

thm Exp_min
  x > 0 -> Exp(x,Min(y,z)) = Min(Exp(x,y),Exp(x,z))
proof 
 cut x > 1
  case Dich; y,z @ x1,y1; x1,y1
   case Dich; Exp(x,y),Exp(x,z) @ x1,y1; x1,y1
    proved
    use Exp_lt.0; x; z; y proved..
   case Dich; x*Exp(x,y-1),Exp(x,z) @ x1,y1; x1,y1
    use Exp_le.0; x; y; z proved.
    proved..
  case N; Min(y,z) @ 0; x1
   case Dich; y,z @ x1,y1; x1,y1
    case Dich; 1,Exp(1,z) @ x1,y1; x1,y1
     proved
     use Exp_one.0; 1; z proved..
    case Dich; Exp(1,y-1),1 @ x1,y1; x1,y1
     use Exp_one.0; 1; y-1 proved.
     proved..
   case Dich; Exp(1,y),Exp(1,z) @ x2,y1; x2,y1
    use Exp_one.0; 1; x1
     use Exp_one.0; 1; y proved..
    use Exp_one.0; 1; x1
     use Exp_one.0; 1; z proved......

thm Exp_max
  x > 0 -> Exp(x,Max(y,z)) = Max(Exp(x,y),Exp(x,z))
proof 
 case N; Max(y,z) @ 0; x1
  case Dich; z,y @ x1,y1; x1,y1
   proved
   proved.
  case Dich; Exp(x,z),Exp(x,y) @ x2,y1; x2,y1
   case Dich; z,y @ x2,y1; x2,y1
    proved
    use Exp_le.0; x; y; z
     cut x > 1
      proved
      use Exp_one.0; 1; x1
       use Exp_one.0; 1; y proved.....
   case Dich; z,y @ x2,y1; x2,y1
    use Exp_le.0; x; z; y
     use Exp_one.0; 1; z
      use Exp_one.0; 1; x1 proved...
    proved....

rem 
  \para \bf  Summation function.  \end 

fun Sum 'Tex_f1_pa_sum'
  Sum(0) = 0
  Sum(n+1) = Sum(n)+n+1

rem 
  \para \bf  Exercise.  \end Prove 
  \eq Sum_zero
    Sum(n) = 0 <-> n = 0
  \end
  \eq Sum_closed_form
    Sum(n) = n*(n+1)/2
  \end

thm Sum_zero
  Sum(n) = 0 <-> n = 0
proof 
 ind N; n @ 0; n
  proved
  proved..

thm Sum_closed_form
  Sum(n) = n*(n+1)/2
proof 
 ind N; n @ 0; n
  proved
  proved..

rem 
  \para \bf  Square root function.  \end 

fun Sqrt 'Tex_f1_pa_sqrt'
  Sqrt(0) = 0
  Sqrt(x+1) = Sqrt(x) <- x+1 < Sq(Sqrt(x)+1)
  Sqrt(x+1) = Sqrt(x)+1 <- x+1 = Sq(Sqrt(x)+1)

rem 
  \para \bf  Exercise.  \end Prove 
  \eq Spec_sqrt
    Sq Sqrt(x) <= x & x < Sq(Sqrt(x)+1)
  \end

thm Spec_sqrt
  Sq Sqrt(x) <= x & x < Sq(Sqrt(x)+1)
proof 
 ind N; x @ 0; x
  proved
  case Trich; x+1,2*Sqrt(x)+Sqrt(x)*Sqrt(x)+1 @ x1,y; x1,y; x1,y
   proved
   proved
   proved...

rem 
  \para \bf  Primitive recursion with substitution in parameters.  \end 

rem 
  \para \bf  Modified subtraction.  \end 

fun/2 Minus 'Tex_f2_pa_minus'
  Minus(0,y) = 0
  Minus(x+1,0) = x+1
  Minus(x+1,y+1) = Minus(x,y)

rem 
  \para \bf  Exercise.  \end Prove 
  \eq Spec_minus_ge
    x >= y -> x = y+Minus(x,y)
  \end
  \eq Spec_minus_le
    x <= y -> Minus(x,y) = 0
  \end

thm Spec_minus_ge
  x >= y -> x = y+Minus(x,y)
proof 
 ind N; x; y @ 0; x
  proved
  case N; y @ 0; y1
   proved
   inst \a y(x >= y -> x = y+Minus(x,y)); y1 proved....

thm Spec_minus_le
  x <= y -> Minus(x,y) = 0
proof 
 ind N; y; x @ 0; y
  proved
  case N; x @ 0; x1
   proved
   inst \a x(x <= y -> Minus(x,y) = 0); x1 proved....