Quelle  boxes_def.pvs

boxes_def : THEORY
BEGIN

  IMPORTING util,
            structures@listn[real],
     reals@product_below

  Box(n:posnat) : TYPE = [#
    vars_lb : listn(n),
    vars_ub : listn(n)
  #]

  setnth_box(v:nat,f:[real->real],n:posnat)(box:Box(n)) : Box(n) = (#
    vars_lb := setnth(box`vars_lb,v,f),
    vars_ub := setnth(box`vars_ub,v,f)
  #)

  map_box(n:posnat,f:[listn(n)->listn(n)])(box:Box(n)) : Box(n) = (#
    vars_lb := f(box`vars_lb),
    vars_ub := f(box`vars_ub)
  #)

  unitbox(n:posnat) : Box(n) = (#
    vars_lb := array2list(n)(zeroes),
    vars_ub := array2list(n)(ones)
  #)

  Boxes(n:posnat) : TYPE = [#
    inside,
    outside,
    unknown : list[Box(n)]
  #]

  mk_boxes(n:posnat,inside,outside,unknown:list[Box(n)]) : Boxes(n) = (#
    inside  := inside,
    outside := outside,
    unknown := unknown
  #)

  volume(n:posnat,box:Box(n)): real =
    product[below(n)](0,n-1,LAMBDA(i:below(n)):nth(box`vars_ub,i)-nth(box`vars_lb,i))
    
END boxes_def