mod Ex07b logic: 'cl'

incl Mtex

incl Mauxb

loc rem 
  7. CVICENIE Z PREDMETU SPECIFIKACIA A VERIFIKACIA PROGRAMOV

rem 
  VASE MENO: ?
  SKUPINA: ?
  VERZIA CL: 5.81.16
  DATUM: stvrtok 31.3.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 [14:50,16:30,18:10]
  WWW: http://www.ii.fmph.uniba.sk/cl/view.php/courses/svp
  konzultacie: stvrtok 13:00-14:00 miestnost I25

rem 
  

rem 
  \para \bf  Uvodna poznamka.  \end Toto cvicenie je venovane zoznamom 
  (triedenie, aplikacie). 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  ex07*.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  Section. Applications of Lists.  \end 

rem 
  \para \bf  Subsection. Finite Sets.  \end 

rem 
  \para \bf  Set membership.  \end 

pred/2 Inset 'Tex_p2_set_in'
  Inset(a,s) <-> Set(s) & a in s

rem 
  \para \bf  Exercise.  \end Prove 
  \eq Spec_inset
    Set(s) -> Inset(a,s) <-> a in s
  \end

thm Spec_inset
  Set(s) -> Inset(a,s) <-> a in s
proof 
 exp Inset; a,s proved..

rem 
  \para \bf  Set insertion.  \end 

fun/2 Insert 'Tex_f2_set_insert'
  Insert(0,a) = a,0
  Insert((s1,s),a) = s1,Insert(s,a) <- s1 < a
  Insert((s1,s),a) = s1,s <- s1 = a
  Insert((s1,s),a) = a,s1,s <- s1 > a

rem 
  \para \bf  Exercise.  \end Prove 
  \eq Spec_insert_in
    Set(s) -> b in Insert(s,a) <-> b = a \/ b in s
  \end
  \eq Spec_insert_set
    Set(s) -> Set Insert(s,a)
  \end

thm Spec_insert_in
  Set(s) -> b in Insert(s,a) <-> b = a \/ b in s
proof 
 ind Ln; s @ 0; v,w
  proved
  case Trich; v,a @ x,y; x,y; x,y
   use Set_pair.2,0,1,0,4,0,0; v; w proved.
   proved
   proved...

lemma Lemma1
  Lt(v,w) & v < a -> Lt(v,Insert(w,a))
proof 
 ind Ln; w @ 0; v1,w
  use Lt_pair.2,1,0; v; a; 0 proved.
  use Lt_pair.2,0,0; v; v1; w
   case Trich; v1,a @ x,y; x,y; x,y
    use Lt_pair.2,1,0; v; v1; Insert(w,a) proved.
    proved
    use Lt_pair.2,1,0; v; a; v1,w proved.....

thm Spec_insert_set
  Set(s) -> Set Insert(s,a)
proof 
 ind Ln; s @ 0; v,w
  use Set_singleton; a proved.
  case Trich; v,a @ x,y; x,y; x,y
   use Set_pair.2,0,0; v; w
    use Lemma1; v; w; a
     use Set_pair.2,1,0; v; Insert(w,a) proved...
   proved
   use Set_lt.1,0,2,1,0; v; w; a
    use Set_pair.2,1,0; a; v,w proved.....

rem 
  \para \bf  Set deletion.  \end 

fun/2 Delete 'Tex_f2_set_delete'
  Delete((s1,s),a) = s1,Delete(s,a) <- s1 < a
  Delete((s1,s),a) = s <- s1 = a
  Delete((s1,s),a) = s1,s <- s1 > a

rem 
  \para \bf  Exercise.  \end Prove 
  \eq Spec_delete_in
    Set(s) -> b in Delete(s,a) <-> b in s & b != a
  \end
  \eq Spec_delete_set
    Set(s) -> Set Delete(s,a)
  \end

thm Spec_delete_in
  Set(s) -> b in Delete(s,a) <-> b in s & b != a
proof 
 ind Ln; s @ 0; v,w
  proved
  use Set_pair.2,0,1,0,4,0,0; v; w
   case Trich; v,a @ x,y; x,y; x,y
    cut b = v
     proved
     proved.
    cut b = a
     use Set_in; a; w; a proved.
     proved.
    cut b = a
     use Set_in; v; w; a proved.
     proved.....

lemma Lemma2
  Lt(v,w) & v < a -> Lt(v,Delete(w,a))
proof 
 ind Ln; w @ 0; v1,w
  proved
  use Lt_pair.2,0,0; v; v1; w
   case Trich; v1,a @ x,y; x,y; x,y
    use Lt_pair.2,1,0; v; v1; Delete(w,a) proved.
    proved
    proved....

thm Spec_delete_set
  Set(s) -> Set Delete(s,a)
proof 
 ind Ln; s @ 0; v,w
  proved
  use Set_pair.2,0,1,0,4,0,0; v; w
   case Trich; v,a @ x,y; x,y; x,y
    use Set_pair.2,0,1,0,4,1,0; v; w
     use Lemma2; v; w; a
      use Set_pair.2,1,0; v; Delete(w,a) proved...
    proved
    proved....