Re: [work] [PVS-Help] Discharging TCC

[Cesar Munoz <munoz@xxxxxxxxxx>]

Hi Anup,

You can prove this TCC 

add_TCC1: OBLIGATION
  FORALL (l: list[T], a: T): cons?[T](append[T](l, cons[T](a,
null[T])));

the same way you prove the other lemmas in your theory: by induction on
"l". Try, for example, induct-and-simplify.

Cesar

On Sat, 2007-08-04 at 23:08 +0530, Anup Bhattacharjee wrote:
> Can you help me to understand how to discharge the tcc in this theory
> list_props[T: TYPE]: THEORY
> BEGIN
>     importing list_adt
>     l,l1,l2: VAR list[T]
>     cons_l: VAR (cons?[T])
>     a,b,c: VAR T
>     P: VAR [list[T] -> bool] 
>     add(l,a): (cons?[T]) = append(l, cons(a, null))
>     length_add: LEMMA length(add(l,a)) = length(l) + 1
>     length_non_zero: LEMMA length(l) = 0 IFF l = null
>     cons_to_add: LEMMA FORALL cons_l: EXISTS a, l: cons_l=add(l,a) 
>      add_induction:PROPOSITION P(null) AND (FORALL l,a: P(l) IMPLIES
> P(add(l,a))) IMPLIES (FORALL l: P(l))
> END list_props
> 
> Thanks in advance.
> Anup
-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace         mailto:Cesar.A.Munoz@nasa.gov
100 Exploration Way  Room 214       http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4