Dear the receiver:
hello, Please forgive me that I don't know how to call you.I am a PVS user of
1. I want to use pvs to express the axiomatization of Propositional Projection Temporal Logic(PPTL),but I don't know how to express "prj",that is (P1,P2,P3,....Pm) prj Q ,where Pi(1<=i<=m) and Q is a formula in PPTL.I'd like to use " list",is it suitable?
2. in following specification ,there is a mistake in if _expression_ ,but I can't understand why and how to correct ,so can you help me if you have time ? Thank you very much.
a part of the specification is :
sequ[ T : TYPE ] : THEORY
BEGIN
sequ : TYPE = [# infinite : bool, len : nat, seq : ARRAY[{ i:nat | infinite or i<=len } -> T ] #]
END sequ
ftp : var sequ[form] %form is formulas
prjns(ftp)(i:nat,l:nat,n:{j:nat|j>=1}) : sequ[form] =
let m=(n-1)*(l-i+1) in (#infinte := infinite(ftp),len := len(ftp)+m,seq :=
( LAMBDA (k: nat):
(if ( k <= l ) then seq(ftp)(k)
elsif (k< m+l) then
(LAMBDA (t:{j:nat|1<=j<=l-i+1}): seq(ftp)(i+t-1))
else (LAMBDA (x:{j:nat|l<j<=len(ftp)}): seq(ftp)(x)) endif))#)
this is the mistake:
Expecting an _expression_
No resolution for IF with arguments of possible types:
(k <= l) : booleans.bool
seq(ftp)(k) : form_adt.form
IF (k < m + l)
THEN (LAMBDA (t: {j: nat | b2n(1 <= j) <= l - i + 1}): seq(ftp)(i + t - 1))
ELSE (LAMBDA (x: {j: nat | b2n(l < j) <= len(ftp)}): seq(ftp)(x)) : [{j:
naturalnumbers.nat |
reals.<=
(bit.b2n
(reals.<= (1,j)),
(number_fields.-)
((number_fields.+)
l),
i))} ->
form_adt.form]
P.S : thank you a lot,