mod Ul03 logic: 'cl'

loc rem 
  PREMIOVA ULOHA Z PREDMETU SPECIFIKACIA A VERIFIKACIA PROGRAMOV

rem 
  VASE MENO: Vladimir Tomecek
  SKUPINA: 2i4
  VERZIA CL: 5.81.16
  DATUM: pondelok 14.3.2005
  ******************************************************************************
  PRENOS: <cl>/2i/prenos/ulohy/ul03/<vase meno>/ul03.cl
          kde <cl> je adresar /data/VYUKA/INF/CL na barbie.nw.fmph.uniba.sk
          ************************************************
          *** odovzdat do 22.3.2001 (utorok) do 18:00 ***
          ************************************************
  ******************************************************************************
  PMAIL: svp@nw.fmph.uniba.sk
  WWW: http://www.ii.fmph.uniba.sk/cl/view.php/courses/svp

rem 
  \para \bf  Hodnotenie.  \end 
  \items 
   \item \para Pocet bodov za ulohu: \it  8  \end. 
   \item \para Hodnotime len prvych 10 spravnych rieseni. 
   \item \para Ulohy rieste \bf  samostatne!  \end 
  \end

appldisp/2 Tex_f2_ln_sub
  Subsup(Fenced(Op('(',0),Arg(0),Op(')',0)),75,Arg(1),None)

appldisp/1 Tex_f1_g
  Std('g',0)

appldisp/3 Tex_f3_h
  Std('h',0)

appldisp/2 Tex_f2_f
  Std('f',0)

fun/0 Foo 'Tex_f0_foo'
  Foo = 0

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

rem 
  \para \bf  Finite sequences.  \end 

fun L 
  L(0) = 0
  L(v,w) = L(w)+1

fun/2 Sub 'Tex_f2_ln_sub'
  Sub((v,w),0) = v
  Sub((v,w),i+1) = Sub(w,i)

thm L_zero
  L(x) = 0 <-> x = 0
proof 
 case Ln; x @ 0; v,w
  proved
  proved..

thm L_conc
  L(x++y) = L(x)+L(y)
proof 
 ind Ln; x @ 0; v,w
  proved
  proved..

thm Sub_conc_left
  i < L(x) -> Sub(x++y,i) = Sub(x,i)
proof 
 ind Ln; x; i @ 0; v,w
  proved
  case N; i @ 0; i1
   proved
   inst \a i(i < L(w) -> Sub(w++y,i) = Sub(w,i)); i1 proved....

thm Sub_conc_right
  i < L(y) -> Sub(x++y,L(x)+i) = Sub(y,i)
proof 
 ind Ln; x @ 0; v,w
  proved
  proved..

thm Eq_seq
  x = y <-> L(x) = L(y) & \a i(i < L(x) -> Sub(x,i) = Sub(y,i))
proof 
 ind Ln; x; y @ 0; v1,w1
  use L_zero.0; y proved.
  case Ln; y @ 0; v2,w2
   proved
   weak y = v2,w2
    inst \a y(w1 = y <-> L(w1) = L(y) & \a i(i < L(w1) -> Sub(w1,i) = Sub(y,i))).0; w2
     weak \a y(w1 = y <-> L(w1) = L(y) & \a i(i < L(w1) -> Sub(w1,i) = Sub(y,i)))
      weak w1 = w2 <-> L(w1) = L(w2) & \a i(i < L(w1) -> Sub(w1,i) = Sub(w2,i))
       cut L(w2) = L(w1)
        weak L(w2) = L(w1)
         split* v1 = v2 & \a i(i < L(w1) -> Sub(w1,i) = Sub(w2,i)) <-> 
                \a i(i <= L(w1) -> Sub((v1,w1),i) = Sub((v2,w2),i)).2,0,1,0,4,0,
                                                                    0,0
          weak v1 = v2
           eigen* \a i(i <= L(w1) -> Sub((v2,w1),i) = Sub((v2,w2),i)).0; i
            case N; i @ 0; j
             proved
             inst \a i(i < L(w1) -> Sub(w1,i) = Sub(w2,i)); j proved....
          inst \a i(i <= L(w1) -> Sub((v1,w1),i) = Sub((v2,w2),i)); 0 proved.
          eigen* \a i(i < L(w1) -> Sub(w1,i) = Sub(w2,i)).0; i
           inst \a i(i <= L(w1) -> Sub((v1,w1),i) = Sub((v2,w2),i)); i+1 proved....
        proved........

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

theory Admissibility_of_primitive_recursion

fun G 'Tex_f1_g'

fun/3 H1 'Tex_f3_h'

rem 
  \para \bf  Introduction.  \end Our goal is to formalize primitive recursion 
  \def 
    fun/2 F 'Tex_f2_f'
    F(0,y) = G(y)
    F(x+1,y) = H1(x,y,F(x,y))
  \end
  \para within Peano arithmetic. 

rem 
  \para \bf  Course of values sequences.  \end 

pred/3 Cvs 
  Cvs(s,x,y) <-> 
    L(s) = x+1 & Sub(s,0) = G(y) & \a i(i < x -> Sub(s,i+1) = H1(i,y,Sub(s,i)))

rem 
  \para \bf  The graph.  \end 

pred/3 Gr 
  Gr(x,y,z) <-> \e s(Cvs(s,x,y) & Sub(s,x) = z)

rem 
  \para \bf  Exercise.  \end Prove 
  \eq Gre
    \e zGr(x,y,z)
  \end
  \eq Gru
    Gr(x,y,z1) & Gr(x,y,z2) -> z1 = z2
  \end

thm Gre
  \e zGr(x,y,z)
proof 
 ind N; x @ 0; x
  inst* \e zGr(0,y,z); G(y)
   exp Gr; 0,y,G(y)
    inst* \e s(Cvs(s,0,y) & Sub(s,0) = G(y)); G(y),0
     exp Cvs; (G(y),0),0,y proved....
  eigen \e zGr(x,y,z); z
   inst* \e zGr(x+1,y,z); H1(x,y,z)
    weak* \e zGr(x+1,y,z)
     exp Gr; x,y,z
      eigen \e s(Cvs(s,x,y) & Sub(s,x) = z).0; s
       exp Cvs; s,x,y
        exp Gr; x+1,y,H1(x,y,z)
         inst* \e s1(Cvs(s1,x+1,y) & Sub(s1,x+1) = H1(x,y,z)); s++(H1(x,y,z),0)
          weak* \e s1(Cvs(s1,x+1,y) & Sub(s1,x+1) = H1(x,y,z))
           split* Cvs(s++(H1(x,y,z),0),x+1,y) & 
                  Sub(s++(H1(x,y,z),0),x+1) = H1(x,y,z).4,0,0,0
            exp Cvs; s++(H1(x,y,z),0),x+1,y
             split* L(s++(H1(x,y,z),0)) = x+2 & 
                    Sub(s++(H1(x,y,z),0),0) = G(y) & 
                    \a i(i <= x -> 
                         Sub(s++(H1(x,y,z),0),i+1) = 
                         H1(i,y,Sub(s++(H1(x,y,z),0),i))).4,0,0,0,0
              use L_conc; s; H1(x,y,z),0 proved.
              use Sub_conc_left; 0; s; H1(x,y,z),0 proved.
              eigen* \a i(i <= x -> 
                          Sub(s++(H1(x,y,z),0),i+1) = 
                          H1(i,y,Sub(s++(H1(x,y,z),0),i))).0; i
               use Sub_conc_left; i; s; H1(x,y,z),0
                cut i < x
                 inst \a i(i < x -> Sub(s,i+1) = H1(i,y,Sub(s,i))); i
                  use Sub_conc_left; i+1; s; H1(x,y,z),0 proved..
                 use Sub_conc_right; 0; H1(x,y,z),0; s proved......
            use Sub_conc_right; 0; H1(x,y,z),0; s proved.............

lemma Lemma1
  Cvs(s1,x,y) & Cvs(s2,x,y) -> s1 = s2
proof 
 exp Cvs; s1,x,y
  exp Cvs; s2,x,y
   use Eq_seq.2,1,0; s1; s2
    weak L(s1) = x+1
     weak L(s2) = x+1
      split \a i(i <= x -> Sub(s1,i) = Sub(s2,i)) -> s1 = s2.2,1,0
       weak* s1 = s2
        eigen* \a i(i <= x -> Sub(s1,i) = Sub(s2,i)).0; i
         ind N; i @ 0; i
          proved
          inst \a i(i < x -> Sub(s1,i+1) = H1(i,y,Sub(s1,i))); i
           inst \a i(i < x -> Sub(s2,i+1) = H1(i,y,Sub(s2,i))); i proved.....
       proved.......

thm Gru
  Gr(x,y,z1) & Gr(x,y,z2) -> z1 = z2
proof 
 exp Gr; x,y,z1
  exp Gr; x,y,z2
   eigen \e s(Cvs(s,x,y) & Sub(s,x) = z1).0; s1
    eigen \e s(Cvs(s,x,y) & Sub(s,x) = z2).0; s2
     use Lemma1; s1; x; y; s2 proved......

rem 
  \para \bf  Contextual definition.  \end 

fun/2 F 'Tex_f2_f'

axiom Fdef
  F(x,y) = z <-> Gr(x,y,z)

rem 
  \para \bf  Exercise.  \end Prove 
  \eq F0
    F(0,y) = G(y)
  \end
  \eq F1
    F(x+1,y) = H1(x,y,F(x,y))
  \end

thm F0
  F(0,y) = G(y)
proof 
 use Fdef.2,1,0; 0; y; G(y)
  split Gr(0,y,G(y)) -> F(0,y) = G(y).2,1,0
   weak* F(0,y) = G(y)
    exp Gr; 0,y,G(y)
     inst* \e s(Cvs(s,0,y) & Sub(s,0) = G(y)); G(y),0
      weak* \e s(Cvs(s,0,y) & Sub(s,0) = G(y))
       exp Cvs; (G(y),0),0,y proved.....
   proved...

thm F1
  F(x+1,y) = H1(x,y,F(x,y))
proof 
 ind N; x @ 0; x
  use Fdef.2,1,0; 1; y; H1(0,y,F(0,y))
   split Gr(1,y,H1(0,y,F(0,y))) -> F(1,y) = H1(0,y,F(0,y)).2,1,0
    weak* F(1,y) = H1(0,y,F(0,y))
     exp Gr; 1,y,H1(0,y,F(0,y))
      inst* \e s(Cvs(s,1,y) & Sub(s,1) = H1(0,y,F(0,y))); F(0,y),H1(0,y,F(0,y)),0
       weak* \e s(Cvs(s,1,y) & Sub(s,1) = H1(0,y,F(0,y)))
        exp Cvs; (F(0,y),H1(0,y,F(0,y)),0),1,y
         use F0; y
          eigen* \a i(i = 0 -> 
                      Sub((H1(0,y,G(y)),0),i) = 
                      H1(i,y,Sub((G(y),H1(0,y,G(y)),0),i))).0; i proved.......
    proved..
  use Fdef.2,1,0; x+2; y; H1(x+1,y,H1(x,y,F(x,y)))
   split Gr(x+2,y,H1(x+1,y,H1(x,y,F(x,y)))) -> 
         F(x+2,y) = H1(x+1,y,H1(x,y,F(x,y))).2,1,0
    weak* F(x+2,y) = H1(x+1,y,H1(x,y,F(x,y)))
     use Fdef.2,0,0; x+1; y; H1(x,y,F(x,y))
      exp Gr; x+1,y,H1(x,y,F(x,y))
       eigen \e s(Cvs(s,x+1,y) & Sub(s,x+1) = H1(x,y,F(x,y))).0; s
        exp Gr; x+2,y,H1(x+1,y,H1(x,y,F(x,y)))
         inst* \e s1(Cvs(s1,x+2,y) & Sub(s1,x+2) = H1(x+1,y,H1(x,y,F(x,y)))); s++(H1(x+1,y,H1(x,y,F(x,y))),0)
          weak* \e s1(Cvs(s1,x+2,y) & Sub(s1,x+2) = H1(x+1,y,H1(x,y,F(x,y))))
           exp Cvs; s,x+1,y
            split* Cvs(s++(H1(x+1,y,H1(x,y,F(x,y))),0),x+2,y) & 
                   Sub(s++(H1(x+1,y,H1(x,y,F(x,y))),0),x+2) = 
                   H1(x+1,y,H1(x,y,F(x,y))).4,0,0,0
             exp Cvs; s++(H1(x+1,y,H1(x,y,F(x,y))),0),x+2,y
              split* L(s++(H1(x+1,y,H1(x,y,F(x,y))),0)) = x+3 & 
                     Sub(s++(H1(x+1,y,H1(x,y,F(x,y))),0),0) = G(y) & 
                     \a i(i <= x+1 -> 
                          Sub(s++(H1(x+1,y,H1(x,y,F(x,y))),0),i+1) = 
                          H1(i,y,Sub(s++(H1(x+1,y,H1(x,y,F(x,y))),0),i))).4,0,0,
                                                                          0,0
               use L_conc; s; H1(x+1,y,H1(x,y,F(x,y))),0 proved.
               use Sub_conc_left; 0; s; H1(x+1,y,H1(x,y,F(x,y))),0 proved.
               eigen* \a i(i <= x+1 -> 
                           Sub(s++(H1(x+1,y,H1(x,y,F(x,y))),0),i+1) = 
                           H1(i,y,Sub(s++(H1(x+1,y,H1(x,y,F(x,y))),0),i))).0; i
                cut i = x+1
                 use Sub_conc_right; 0; H1(x+1,y,H1(x,y,F(x,y))),0; s
                  use Sub_conc_left; x+1; s; H1(x+1,y,H1(x,y,F(x,y))),0 proved..
                 use Sub_conc_left; i+1; s; H1(x+1,y,H1(x,y,F(x,y))),0
                  use Sub_conc_left; i; s; H1(x+1,y,H1(x,y,F(x,y))),0
                   inst \a i(i <= x -> Sub(s,i+1) = H1(i,y,Sub(s,i))); i proved.......
             use Sub_conc_right; 0; H1(x+1,y,H1(x,y,F(x,y))),0; s proved..........
    proved....

end theory Admissibility_of_primitive_recursion