Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 621


Synopsis:        PVS2.4 typecheck or parse error
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue Nov 27 14:08:38 2001
Originator:      Bruno Dutertre
Organization:    sdl.sri.com
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  This is a multi-part message in MIME format.
  --------------45B001C1407BA0798CAC0F90
  Content-Type: text/plain; charset=us-ascii
  Content-Transfer-Encoding: 7bit
  
  Sam,
  
  PVS2.4 gives a strange error message when
  typechecking theory clock_props2:
  
  "} expected here"
  
  It sounds like a syntax error but parsing
  without typecking works fine.
  
  Bruno
  --------------45B001C1407BA0798CAC0F90
  Content-Type: text/plain; charset=us-ascii;
   name="clock_props2.dmp"
  Content-Transfer-Encoding: 7bit
  Content-Disposition: inline;
   filename="clock_props2.dmp"
  
  
  $$$clock_props2.pvs
  clock_props2 [ (IMPORTING clocks)
   	H : clock] : THEORY
  
    BEGIN
  
    t : VAR time
  
    i, j, n : VAR nat
  
    x, y, z : VAR (H)
  
  
    IMPORTING realsets_minmax
  
  
    %-----------------------------------
    %  inclusion, maximum of cut(H, x)
    %-----------------------------------
  
    subset_cut : LEMMA
  	x < y IMPLIES subset?(add(x, cut(H, x)), cut(H, y))
  
    max_cut : LEMMA
  	NOT empty?(cut(H, x)) IMPLIES
  	    cut(H, max(cut(H, x))) = remove(max(cut(H, x)), cut(H, x))
  		
  
  
  
    %-------------------------------
    %  index for each element of H
    %-------------------------------
  
    ord(x) : nat = card(cut(H, x))
  
  
    ord_lt : PROPOSITION  x < y IFF ord(x) < ord(y)
  
    ord_le : PROPOSITION  x <= y IFF ord(x) <= ord(y) 
  	
    ord_gt : PROPOSITION  x > y IFF ord(x) > ord(y)
  
    ord_ge : PROPOSITION  x >= y IFF ord(x) >= ord(y)
  
    ord_eq : PROPOSITION  ord(x) = ord(y) IMPLIES x = y
  
  
    ord_prefix : PROPOSITION
  	n < ord(x) IMPLIES EXISTS (y | y < x) : ord(y) = n
  
  
  
    %---------------------------
    %  First and last elements
    %---------------------------
  
    first?(x) : bool = ord(x) = 0
  
    last?(x) : bool = FORALL y : y <= x
  
    unique_first : LEMMA
  	first?(x) AND first?(y) IMPLIES x = y
  
    unique_last : LEMMA
  	last?(x) AND last?(y) IMPLIES x = y
  
  
    first_def : LEMMA
  	first?(x) IFF FORALL y : x <= y
  
  
  
    %-----------------------------
    %  Predecessor and successor
    %-----------------------------
  
    %  Existence
  
    predecessor : LEMMA
  	FORALL (x | not first?(x)) :
  	    EXISTS (y | not last?(y)) : ord(y) = ord(x) - 1
  
    successor : LEMMA
  	FORALL (x | not last?(x)) :
  	    EXISTS (y | not first?(y)) : ord(y) = ord(x) + 1
  
  
    %  Definitions
  
    pre(u : (H) | not first?(u)) : { (x | not last?(x)) | ord(x) = ord(u) - 1 A
 ND x < u}
  
    next(v : (H) | not last?(v)) : { (x | not first?(x)) | ord(x) = ord(v) + 1 
 AND v < x}
  
    pre_def : PROPOSITION
  	FORALL (x | not first?(x)), y :
  	    pre(x) = y IFF maximum?(y, cut(H, x))
  
    next_def : PROPOSITION
  	FORALL (x | not last?(x)), y :
  	    next(x) = y IFF maximum?(x, cut(H, y))
  
  
    %  rewrite rules
  
    pre_lt : PROPOSITION
  	FORALL (u1, u2 : { x | not first?(x)}) :
  	    pre(u1) < pre(u2) IFF u1 < u2
  
    pre_le : PROPOSITION
  	FORALL (u1, u2 : { x | not first?(x)}) :
  	    pre(u1) <= pre(u2) IFF u1 <= u2
  	
    pre_gt : PROPOSITION
  	FORALL (u1, u2 : { x | not first?(x)}) :
  	    pre(u1) > pre(u2) IFF u1 > u2
  
    pre_ge : PROPOSITION
  	FORALL (u1, u2 : { x | not first?(x)}) :
  	    pre(u1) >= pre(u2) IFF u1 >= u2
  
    pre_eq : PROPOSITION
  	FORALL (u1, u2 : { x | not first?(x)}) :
  	    pre(u1) = pre(u2) IMPLIES u1 = u2
  
  
    next_lt : PROPOSITION
  	FORALL (v1, v2 : { x | not last?(x) }) :
  	    next(v1) < next(v2) IFF v1 < v2
  
    next_le : PROPOSITION
  	FORALL (v1, v2 : { x | not last?(x)}) :
  	    next(v1) <= next(v2) IFF v1 <= v2
  	
    next_gt : PROPOSITION
  	FORALL (v1, v2 : { x | not last?(x)}) :
  	    next(v1) > next(v2) IFF v1 > v2
  
    next_ge : PROPOSITION
  	FORALL (v1, v2 : { x | not last?(x)}) :
  	    next(v1) >= next(v2) IFF v1 >= v2
  
    next_eq : PROPOSITION
  	FORALL (v1, v2 : { x | not last?(x)}) :
  	    next(v1) = next(v2) IMPLIES v1 = v2
  
  
  
    pre_next : PROPOSITION
  	FORALL (x | not last?(x)) : pre(next(x)) = x
  
    next_pre : PROPOSITION
  	FORALL (x | not first?(x)) : next(pre(x)) = x
  
  
    ord_pre : PROPOSITION
  	FORALL (x | not first?(x)) : ord(pre(x)) = ord(x) - 1
  
    ord_next : PROPOSITION
  	FORALL (x | not last?(x)) : ord(next(x)) = ord(x) + 1
  
  
  
    pre_lt2 : PROPOSITION
  	FORALL (x | not first?(x)), y : pre(x) < y  IFF x <= y
  
    pre_le2 : PROPOSITION
  	FORALL (x | not first?(x)), y : y <= pre(x) IFF y < x
  
    pre_gt2 : PROPOSITION
  	FORALL (x | not first?(x)), y : y > pre(x)  IFF y >= x
  
    pre_ge2 : PROPOSITION
  	FORALL (x | not first?(x)), y : pre(x) >= y IFF x > y
  
    next_lt2 : PROPOSITION
  	FORALL (x | not last?(x)), y : y < next(x)  IFF y <= x
  
    next_le2 : PROPOSITION
  	FORALL (x | not last?(x)), y : next(x) <= y IFF x < y
  
    next_gt2 : PROPOSITION
  	FORALL (x | not last?(x)), y : next(x) > y  IFF x >= y
  
    next_ge2 : PROPOSITION
  	FORALL (x | not last?(x)), y : y >= next(x) IFF y > x
  
  
    %--------------------
    %  Other properties
    %--------------------
  
    step_pre : PROPOSITION
  	FORALL (x | not first?(x)), t :
  	    pre(x) < t AND t < x IMPLIES not H(t)
  
    step_pre3 : PROPOSITION
  	FORALL (x | not first?(x)), y :
  	    pre(x) <= y AND y < x IMPLIES y = pre(x)
  
    step_pre4 : PROPOSITION
  	FORALL (x | not first?(x)), y :
  	    pre(x) < y AND y <= x IMPLIES y = x
  	
  
  
    step_next : PROPOSITION
  	FORALL (x | not last?(x)), t :
  	    x < t AND t < next(x) IMPLIES not H(t)
  	
    step_next3 : PROPOSITION
  	FORALL (x | not last?(x)), y :
  	    x <= y AND y < next(x) IMPLIES y = x
  
    step_next4 : PROPOSITION
  	FORALL (x | not last?(x)), y :
  	    x < y AND y <= next(x) IMPLIES y = next(x)
  
  
  
    between_pre_next : PROPOSITION
  	FORALL (x | NOT first?(x) AND NOT last?(x)), y :
  	    pre(x) < y AND y < next(x) IMPLIES y = x
  
  
    before_first : PROPOSITION
  	first?(x) AND t < x IMPLIES not H(t)
  
    after_last : PROPOSITION
  	last?(x) AND  x < t IMPLIES not H(t)
  
  
    first_min : PROPOSITION
  	FORALL (x | first?(x)), y : x <= y
  
    first_min2 : PROPOSITION
  	y < x IMPLIES not first?(x)
  
    last_max : PROPOSITION
  	FORALL (x | last?(x)), y : y <= x
  
    last_max2 : PROPOSITION
  	x < y IMPLIES not last?(x)
  
    single_element : PROPOSITION
  	FORALL (x | first?(x) AND last?(x)), y : y = x
  
  
    first_exists : PROPOSITION
  	FORALL y : EXISTS (x | x <= y) : first?(x)
  
  
  
  
    %-----------------------------------------------
    %  previous(t): instant of H strictly before t
    %-----------------------------------------------
  
    u, v : VAR { t | EXISTS x : x < t }
  
    previous(u) : { x | x < u AND FORALL y : y < u IMPLIES y <= x }
  
  
    previous_le : PROPOSITION
  	u <= v IMPLIES previous(u) <= previous(v)
  
    previous_ge : PROPOSITION
  	u >= v IMPLIES previous(u) >= previous(v)
  
    previous_lt : PROPOSITION
  	previous(u) < previous(v) IMPLIES u < v
  
    previous_gt : PROPOSITION
  	previous(u) > previous(v) IMPLIES u > v
  
  
    previous_lt2 : PROPOSITION
  	previous(u) < previous(v) IFF EXISTS x : u <= x AND x < v
  
    previous_gt2 : PROPOSITION
  	previous(u) > previous(v) IFF EXISTS x : u > x AND x >= v
  
    END clock_props2
  
  $$$clock_props2.prf
  (|clock_props2| (|subset_cut| "" (GRIND) NIL)
   (|max_cut_TCC1| "" (SKOSIMP) (("" (REWRITE "finite_has_max[time]") NIL)))
   (|max_cut| "" (SKOSIMP)
    (("" (ASSERT)
      (("" (DELETE 1)
        (("" (AUTO-REWRITE "max_cut_TCC1")
          (("" (USE "max_lemma[time]")
            (("" (APPLY-EXTENSIONALITY :HIDE? T)
              (("" (TYPEPRED "max(cut(H, x!1))")
                (("" (GRIND :EXCLUDE ("max") :IF-MATCH NIL)
                  (("" (INST - "x!2") (("" (ASSERT) NIL)))))))))))))))))))
   (|ord_lt| "" (CASE "FORALL x, y  : x < y IMPLIES ord(x) < ord(y)")
    (("1" (SKOLEM!)
      (("1" (INST-CP - "x!1" "y!1") (("1" (INST - "y!1" "x!1") (("1" (GROUND) N
 IL)))))))
     ("2" (DELETE 2)
      (("2" (AUTO-REWRITE "cut" "member" "finite_add[time]" "card_add[time]")
        (("2" (SKOSIMP)
          (("2" (EXPAND "ord")
            (("2" (FORWARD-CHAIN "subset_cut")
              (("2" (FORWARD-CHAIN "card_subset") (("2" (ASSERT) NIL)))))))))))
 ))))
   (|ord_le| "" (SKOLEM!) (("" (USE "ord_lt" ("x" "y!1")) (("" (GROUND) NIL))))
 )
   (|ord_gt| "" (SKOLEM!) (("" (USE "ord_lt" ("x" "y!1")) (("" (GROUND) NIL))))
 )
   (|ord_ge| "" (SKOLEM!) (("" (USE "ord_le" ("x" "y!1")) (("" (GROUND) NIL))))
 )
   (|ord_eq| "" (SKOSIMP)
    (("" (USE "ord_lt" ("y" "y!1")) (("" (USE "ord_lt" ("x" "y!1")) (("" (ASSER
 T) NIL)))))))
   (|ord_prefix| "" (CASE "FORALL i, j, x : i < j AND ord(x) = j IMPLIES EXISTS
  y : ord(y) = i")
    (("1" (SKOSIMP)
      (("1" (INST - "n!1" "ord(x!1)" "x!1")
        (("1" (ASSERT)
          (("1" (SKOLEM!) (("1" (INST?) (("1" (REWRITE "ord_lt") (("1" (ASSERT)
  NIL)))))))))))))
     ("2" (DELETE 2)
      (("2" (INDUCT "j")
        (("1" (SKOSIMP) (("1" (ASSERT) NIL)))
         ("2"
          (AUTO-REWRITE "max_cut_TCC1" "max_cut" "ord" "cut" "card_remove[time]
 "
                        "finite_remove[time]" "member[time]")
          (("2" (SKOSIMP*)
            (("2" (ASSERT)
              (("2" (CASE "empty?(cut(H, x!1))")
                (("1" (REWRITE "empty_card") NIL)
                 ("2" (ASSERT)
                  (("2" (CASE "H(max(cut(H, x!1)))")
                    (("1" (ASSERT)
                      (("1" (INST - "i!1" "max(cut(H, x!1))")
                        (("1" (GROUND) (("1" (INST + "max(cut(H, x!1))") (("1" 
 (ASSERT) NIL)))))))))
                     ("2" (ASSERT)
                      (("2" (TYPEPRED "max[time](cut(H, x!1))")
                        (("2" (ASSERT) NIL)))))))))))))))))))))))
   (|unique_first| "" (APPLY (THEN (SKOSIMP) (EXPAND "first?") (REWRITE "ord_eq
 " +) (ASSERT))) NIL)
   (|unique_last| "" (SKOSIMP)
    (("" (EXPAND "last?") (("" (INST - "y!1") (("" (INST - "x!1") (("" (ASSERT)
  NIL)))))))))
   (|first_def| "" (GRIND :EXCLUDE ("ord") :REWRITES ("ord_le") :IF-MATCH NIL)
    (("" (USE "ord_prefix") (("" (ASSERT) (("" (SKOLEM!) (("" (INST?) (("" (ASS
 ERT) NIL)))))))))))
   (|predecessor| "" (GRIND :EXCLUDE ("ord") :IF-MATCH NIL)
    (("" (USE "ord_prefix" ("n" "ord(x!1) - 1"))
      (("" (ASSERT) (("" (SKOLEM!) (("" (INST?) (("" (INST - "x!1") (("" (ASSER
 T) NIL)))))))))))))
   (|successor| "" (GRIND :EXCLUDE ("ord") :IF-MATCH NIL :REWRITES ("ord_le"))
    (("" (CASE "ord(y!1) = ord(x!1) + 1")
      (("1" (INST?) (("1" (ASSERT) NIL)))
       ("2" (ASSERT)
        (("2" (USE "ord_prefix" ("n" "ord(x!1) + 1"))
          (("2" (GROUND) (("2" (SKOLEM!) (("2" (INST?) (("2" (ASSERT) NIL))))))
 )))))))))
   (|pre_TCC1| "" (LEMMA "predecessor")
    (("" (INST + "lambda (x | not first?(x)) : epsilon! (y | not last?(y)) : or
 d(y) = ord(x) - 1")
      (("1" (SKOLEM!)
        (("1" (INST?)
          (("1" (LEMMA "epsilon_ax" ("p" "lambda (y | not last?(y)) : ord(y) = 
 ord(x!1) - 1"))
            (("1" (GROUND) (("1" (REWRITE "ord_lt") (("1" (ASSERT) NIL)))))
             ("2" (SKOLEM!) (("2" (INST + "y!1") NIL)))))))))
       ("2" (SKOLEM!) (("2" (INST - "x!1") (("2" (SKOLEM!) (("2" (INST + "y!1")
  NIL)))))))))))
   (|next_TCC1| "" (LEMMA "successor")
    (("" (INST + "lambda (x | not last?(x)) : epsilon! (y | not first?(y)) : or
 d(y) = ord(x) + 1")
      (("1" (SKOLEM!)
        (("1" (INST?)
          (("1" (LEMMA "epsilon_ax" ("p" "lambda (y | not first?(y)) : ord(y) =
  ord(x!1) + 1"))
            (("1" (GROUND) (("1" (REWRITE "ord_lt") (("1" (ASSERT) NIL)))))
             ("2" (SKOLEM!) (("2" (INST + "y!1") NIL)))))))))
       ("2" (SKOLEM!) (("2" (INST - "x!1") (("2" (SKOLEM!) (("2" (INST + "y!1")
  NIL)))))))))))
   (|xxxx_TCC1| "" (INST + "pre") (("" (SKOLEM!) (("" (ASSERT) NIL)))))
   (|test| "" (APPLY-EXTENSIONALITY)
    (("1" (REWRITE "ord_eq") NIL)
     ("2" (SKOSIMP)
      (("2" (GROUND)
        (("1" (EXPAND "last?") (("1" (INST?) (("1" (REWRITE "ord_le") NIL)))))
         ("2" (REWRITE "ord_lt") NIL)))))))
   (|pre_def| "" (GRIND :EXCLUDE ("ord") :IF-MATCH NIL)
    (("1" (REWRITE "ord_le") (("1" (REWRITE "ord_lt") (("1" (ASSERT) NIL)))))
     ("2" (INST - "pre(x!1)")
      (("2" (REWRITE "ord_lt") (("2" (REWRITE "ord_le") (("2" (REWRITE "ord_eq"
  2) NIL)))))))))
   (|next_def| "" (GRIND :EXCLUDE ("ord" "last?") :IF-MATCH NIL)
    (("1" (REWRITE "ord_lt") (("1" (REWRITE "ord_le") (("1" (ASSERT) NIL)))))
     ("2" (REWRITE "ord_lt")
      (("2" (INST - "next(x!1)")
        (("1" (REWRITE "ord_le") NIL) ("2" (REWRITE "ord_lt") (("2" (REWRITE "o
 rd_eq") NIL)))))))))
   (|pre_lt| "" (AUTO-REWRITE "ord_lt") (("" (SKOLEM!) (("" (GROUND) NIL)))))
   (|pre_le| "" (AUTO-REWRITE "ord_le") (("" (SKOLEM!) (("" (GROUND) NIL)))))
   (|pre_gt| "" (AUTO-REWRITE "ord_gt") (("" (SKOLEM!) (("" (GROUND) NIL)))))
   (|pre_ge| "" (SKOLEM!)
    (("" (GROUND)
      (("1" (REWRITE "ord_ge") (("1" (REWRITE "ord_ge" +) (("1" (ASSERT) NIL)))
 ))
       ("2" (REWRITE "ord_ge" +) (("2" (REWRITE "ord_ge") (("2" (ASSERT) NIL)))
 ))))))
   (|pre_eq| "" (SKOSIMP) (("" (REWRITE "ord_eq" +) NIL)))
   (|next_lt| "" (SKOLEM!) (("" (AUTO-REWRITE "ord_lt") (("" (GROUND) NIL)))))
   (|next_le| "" (SKOLEM!) (("" (AUTO-REWRITE "ord_le") (("" (GROUND) NIL)))))
   (|next_gt| "" (SKOLEM!) (("" (AUTO-REWRITE "ord_gt") (("" (GROUND) NIL)))))
   (|next_ge| "" (SKOLEM!)
    (("" (GROUND)
      (("1" (REWRITE "ord_ge") (("1" (REWRITE "ord_ge" +) (("1" (ASSERT) NIL)))
 ))
       ("2" (REWRITE "ord_ge") (("2" (REWRITE "ord_ge" +) (("2" (ASSERT) NIL)))
 ))))))
   (|next_eq| "" (SKOSIMP) (("" (REWRITE "ord_eq" +) NIL)))
   (|pre_next| "" (SKOLEM!) (("" (REWRITE "ord_eq") NIL)))
   (|next_pre| "" (SKOLEM!) (("" (REWRITE "ord_eq") NIL)))
   (|ord_pre| "" (SKOSIMP) (("" (ASSERT) NIL))) (|ord_next| "" (SKOSIMP) (("" (
 ASSERT) NIL)))
   (|pre_lt2| "" (SKOLEM!)
    (("" (GROUND) (("" (REWRITE "ord_le") (("" (REWRITE "ord_lt") (("" (ASSERT)
  NIL)))))))))
   (|pre_le2| "" (SKOLEM!)
    (("" (GROUND) (("" (REWRITE "ord_le") (("" (REWRITE "ord_lt") (("" (ASSERT)
  NIL)))))))))
   (|pre_gt2| "" (SKOLEM!)
    (("" (GROUND) (("" (REWRITE "ord_ge") (("" (REWRITE "ord_gt") (("" (ASSERT)
  NIL)))))))))
   (|pre_ge2| "" (SKOLEM!)
    (("" (GROUND) (("" (REWRITE "ord_ge") (("" (REWRITE "ord_gt") (("" (ASSERT)
  NIL)))))))))
   (|next_lt2| "" (SKOLEM!)
    (("" (GROUND) (("" (REWRITE "ord_le") (("" (REWRITE "ord_lt") (("" (ASSERT)
  NIL)))))))))
   (|next_le2| "" (SKOLEM!)
    (("" (GROUND) (("" (REWRITE "ord_le") (("" (REWRITE "ord_lt") (("" (ASSERT)
  NIL)))))))))
   (|next_gt2| "" (SKOLEM!)
    (("" (GROUND) (("" (REWRITE "ord_ge") (("" (REWRITE "ord_gt") (("" (ASSERT)
  NIL)))))))))
   (|next_ge2| "" (SKOLEM!)
    (("" (GROUND) (("" (REWRITE "ord_ge") (("" (REWRITE "ord_gt") (("" (ASSERT)
  NIL)))))))))
   (|step_pre| "" (AUTO-REWRITE "ord_lt") (("" (SKOSIMP) (("" (ASSERT) (("" (AS
 SERT) NIL)))))))
   (|step_pre3| "" (SKOSIMP) (("" (USE "step_pre") (("" (ASSERT) NIL)))))
   (|step_pre4| "" (SKOSIMP) (("" (USE "step_pre") (("" (ASSERT) NIL)))))
   (|step_next| "" (AUTO-REWRITE "ord_lt") (("" (SKOSIMP) (("" (ASSERT) (("" (A
 SSERT) NIL)))))))
   (|step_next3| "" (SKOSIMP) (("" (USE "step_next") (("" (ASSERT) NIL)))))
   (|step_next4| "" (SKOSIMP) (("" (USE "step_next") (("" (ASSERT) NIL)))))
   (|between_pre_next_TCC1| "" (SKOSIMP) (("" (ASSERT) NIL)))
   (|between_pre_next_TCC2| "" (SKOSIMP) (("" (ASSERT) NIL)))
   (|between_pre_next| "" (SKOSIMP)
    (("" (USE "step_next3") (("" (USE "step_pre4") (("" (ASSERT) NIL)))))))
   (|before_first| "" (SKOSIMP)
    (("" (EXPAND "first?") (("" (REWRITE "ord_lt") (("" (ASSERT) NIL)))))))
   (|after_last| "" (EXPAND "last?") (("" (SKOSIMP) (("" (INST - "t!1") (("" (A
 SSERT) NIL)))))))
   (|first_min| "" (GRIND :EXCLUDE ("ord")) (("" (REWRITE "ord_le") (("" (ASSER
 T) NIL)))))
   (|first_min2| "" (SKOSIMP)
    (("" (REWRITE "ord_lt") (("" (EXPAND "first?") (("" (ASSERT) NIL)))))))
   (|last_max| "" (GRIND) NIL)
   (|last_max2| "" (GRIND :IF-MATCH NIL) (("" (INST - "y!1") (("" (ASSERT) NIL)
 ))))
   (|single_element| "" (SKOLEM!)
    (("" (CASE "x!1 <= y!1 AND y!1 <= x!1")
      (("1" (GROUND) NIL) ("2" (AUTO-REWRITE "first_min" "last_max") (("2" (ASS
 ERT) NIL)))))))
   (|first_exists| "" (SKOLEM!)
    (("" (EXPAND "first?")
      (("" (CASE "0 < ord(y!1)")
        (("1" (FORWARD-CHAIN "ord_prefix") (("1" (SKOLEM!) (("1" (INST?) NIL)))
 ))
         ("2" (INST?) (("2" (ASSERT) NIL)))))))))
   (|previous_TCC1| "" (CASE "FORALL u : has_max(cut(H, u))")
    (("1" (INST + "lambda u : max(cut(H, u))")
      (("1" (SKOSIMP)
        (("1" (INST?)
          (("1" (ASSERT)
            (("1" (TYPEPRED "max[time](cut(H, u!1))")
              (("1" (AUTO-REWRITE "cut")
                (("1" (GROUND)
                  (("1" (SKOSIMP) (("1" (USE "max_is_max" ("W" "cut(H, u!1)")) 
 NIL)))))))))))))))))
     ("2" (DELETE 2)
      (("2" (SKOLEM-TYPEPRED)
        (("2" (REWRITE "finite_has_max[time]")
          (("2" (DELETE +)
            (("2" (GRIND :IF-MATCH NIL) (("2" (INST - "x!1") (("2" (ASSERT) NIL
 )))))))))))))))
   (|previous_le| "" (SKOSIMP)
    (("" (TYPEPRED "previous(v!1)") (("" (INST - "previous(u!1)") (("" (ASSERT)
  NIL)))))))
   (|previous_ge| "" (SKOSIMP) (("" (USE "previous_le" ("u" "v!1" "v" "u!1")) (
 ("" (ASSERT) NIL)))))
   (|previous_lt| "" (SKOSIMP) (("" (USE "previous_ge" ("u" "u!1" "v" "v!1")) (
 ("" (ASSERT) NIL)))))
   (|previous_gt| "" (SKOSIMP) (("" (USE "previous_le" ("u" "u!1" "v" "v!1")) (
 ("" (ASSERT) NIL)))))
   (|previous_lt2| "" (SKOLEM!)
    (("" (GROUND)
      (("1" (TYPEPRED "previous(u!1)")
        (("1" (INST - "previous(v!1)") (("1" (INST + "previous(v!1)") (("1" (AS
 SERT) NIL)))))))
       ("2" (SKOSIMP)
        (("2" (TYPEPRED "previous(v!1)") (("2" (INST - "x!1") (("2" (ASSERT) NI
 L)))))))))))
   (|previous_gt2| "" (SKOLEM!)
    (("" (USE "previous_lt2" ("u" "v!1" "v" "u!1"))
      (("" (GROUND)
        (("1" (SKOSIMP) (("1" (INST + "x!1") (("1" (ASSERT) NIL)))))
         ("2" (SKOSIMP) (("2" (INST + "x!1") (("2" (ASSERT) NIL))))))))))))
  $$$realsets_minmax.pvs
  %----------------------------------------------------------
  %  Maximal and minimal element of a finite set of reals
  %  Like finite_set_minmax in the finite_set
  %  library but without need for an extra 
  %  theory parameter
  %----------------------------------------------------------
  
  realsets_minmax [T: TYPE FROM real ] : THEORY
  
    BEGIN
  
    IMPORTING finite_sets@finite_sets, finite_sets@finite_sets_inductions
   
    S: VAR set[T]
  
    A, B: VAR non_empty_finite_set[T]
  
    x, y, z: VAR T
  
    u: VAR real
  
  
    %----------------------------------
    %  min(A): smallest element of A
    %----------------------------------
  
    minimum(S, x): bool = S(x) AND (FORALL (t: (S)): x <= t)
  
    unique_minimum: LEMMA
  	minimum(S, x) AND minimum(S, y) IMPLIES x = y
  
    minimum_exists: LEMMA EXISTS x: minimum(A, x)
  
  
    min(A): { x | A(x) AND minimum(A, x) }  
  
  
    min_prop1: LEMMA FORALL (x: (A)): min(A) <= x
  
    min_prop2: LEMMA u <= min(A) IFF (FORALL (x: (A)): u <= x)
  
    min_prop3: LEMMA u < min(A) IFF (FORALL (x: (A)): u < x)
  
  
    min_def: LEMMA min(A) = x IFF A(x) AND (FORALL (t: (A)): x <= t)
  
  
    min_singleton: LEMMA min(singleton(x)) = x
  
    min_subset: LEMMA subset?(A, B) IMPLIES min(B) <= min(A)
  
    min_subset2: LEMMA subset?(A, B) AND A(min(B)) IMPLIES min(A) = min(B)
  
    min_inter1: LEMMA
       not empty?(intersection(A, S)) IMPLIES min(A) <= min(intersection(A, S))
  
    min_inter2: LEMMA 
       not empty?(intersection(S, A)) IMPLIES min(A) <= min(intersection(S, A))
  
    min_union: LEMMA min(union(A, B)) = min(min(A), min(B))
  
    min_add: LEMMA min(add(x, A)) = min(x, min(A))
  
  
    %--------------------------------
    %  max(A): largest element of A
    %--------------------------------
  
    maximum(S, x): bool = S(x) AND (FORALL (t: (S)): t <= x)
  
    unique_maximum: LEMMA
  	maximum(S, x) AND maximum(S, y) IMPLIES x = y
  
    maximum_exists: LEMMA EXISTS x: maximum(A, x)
  
  
    max(A): { x | A(x) AND maximum(A, x) }  
  
  
    max_prop1: LEMMA FORALL (x: (A)): x <= max(A)
  
    max_prop2: LEMMA max(A) <= u IFF (FORALL (x: (A)): x <= u)
  
    max_prop3: LEMMA max(A) < u IFF (FORALL (x: (A)): x < u)
  
  
    max_def: LEMMA max(A) = x IFF A(x) AND (FORALL (t: (A)): t <= x)
  
  
    max_singleton: LEMMA max(singleton(x)) = x
  
    max_subset: LEMMA subset?(A, B) IMPLIES max(A) <= max(B)
  
    max_subset2: LEMMA subset?(A, B) AND A(max(B)) IMPLIES max(A) = max(B)
  
    max_inter1: LEMMA
       not empty?(intersection(A, S)) IMPLIES max(intersection(A, S)) <= max(A)
  
    max_inter2: LEMMA 
       not empty?(intersection(S, A)) IMPLIES max(intersection(S, A)) <= max(A)
  
    max_union: LEMMA max(union(A, B)) = max(max(A), max(B))
  
    max_add: LEMMA max(add(x, A)) = max(x, max(A))
  
  
    END realsets_minmax
  
  $$$realsets_minmax.prf
  (|realsets_minmax| (|unique_minimum| "" (GRIND :IF-MATCH ALL) NIL NIL)
   (|minimum_exists| ""
    (INDUCT "A" :NAME "nonempty_finite_set_induct[T]")
    (("1" (GRIND) NIL NIL)
     ("2" (SKOSIMP*)
      (("2" (INST + "min(e!1, x!1)")
        (("1" (GRIND :IF-MATCH NIL)
          (("1" (INST?) NIL NIL)
           ("2" (INST - "t!1") (("2" (ASSERT) NIL NIL)) NIL))
          NIL)
         ("2" (DELETE -1 2) (("2" (GRIND) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|min_TCC1| "" (INST + "lambda A: epsilon! (x: (A)): minimum(A, x)")
    (("1" (SKOLEM!)
      (("1" (USE "epsilon_ax[(A!1)]")
        (("1" (GROUND)
          (("1" (DELETE 2)
            (("1" (USE "minimum_exists")
              (("1" (SKOLEM!) (("1" (INST?) (("1" (GRIND) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("2" (DELETE 2)
          (("2" (TYPEPRED "A!1")
            (("2" (GRIND :EXCLUDE ("is_finite")) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL)
     ("2" (GRIND :EXCLUDE ("is_finite")) NIL NIL))
    NIL)
   (|min_prop1| "" (SKOLEM!)
    (("" (TYPEPRED "min(A!1)")
      (("" (EXPAND "minimum") (("" (INST?) NIL NIL)) NIL)) NIL))
    NIL)
   (|min_prop2| "" (SKOLEM!)
    (("" (REDUCE) (("" (USE "min_prop1") (("" (ASSERT) NIL NIL)) NIL))
      NIL))
    NIL)
   (|min_prop3| "" (SKOLEM!)
    (("" (REDUCE) (("" (USE "min_prop1") (("" (ASSERT) NIL NIL)) NIL))
      NIL))
    NIL)
   (|min_def| "" (SKOLEM!)
    (("" (REWRITE "minimum" :DIR RL)
      (("" (GROUND)
        (("" (USE "unique_minimum") (("" (ASSERT) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|min_singleton| "" (GRIND :REWRITES "min_def") NIL NIL)
   (|min_subset| "" (SKOSIMP)
    (("" (REWRITE "min_prop2")
      (("" (SKOLEM!)
        (("" (REWRITE "min_prop1") (("" (GRIND) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|min_subset2| "" (SKOSIMP)
    (("" (ASSERT)
      (("" (REWRITE "min_def")
        (("" (SKOLEM!)
          (("" (REWRITE "min_prop1") (("" (GRIND) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|min_inter1| "" (SKOLEM!)
    (("" (REWRITE "min_subset") (("" (GRIND) NIL NIL)) NIL)) NIL)
   (|min_inter2| "" (SKOLEM!)
    (("" (REWRITE "min_subset") (("" (GRIND) NIL NIL)) NIL)) NIL)
   (|min_union| "" (SKOLEM!)
    (("" (REWRITE "min_def")
      (("1" (GROUND)
        (("1" (GRIND) NIL NIL)
         ("2" (GRIND :EXCLUDE "min")
          (("1" (USE "min_prop1" ("A" "A!1" "x" "t!1"))
            (("1" (ASSERT) NIL NIL)) NIL)
           ("2" (USE "min_prop1" ("A" "B!1" "x" "t!1"))
            (("2" (ASSERT) NIL NIL)) NIL))
          NIL))
        NIL)
       ("2" (GRIND) NIL NIL))
      NIL))
    NIL)
   (|min_add| "" (SKOLEM!)
    (("" (REWRITE "min_def")
      (("1" (GRIND :IF-MATCH NIL)
        (("1" (REWRITE "min_prop1") NIL NIL)
         ("2" (USE "min_prop1" ("A" "A!1" "x" "t!1"))
          (("2" (ASSERT) NIL NIL)) NIL))
        NIL)
       ("2" (GRIND) NIL NIL))
      NIL))
    NIL)
   (|unique_maximum| "" (GRIND :IF-MATCH ALL) NIL NIL)
   (|maximum_exists| ""
    (INDUCT "A" :NAME "nonempty_finite_set_induct[T]")
    (("1" (GRIND) NIL NIL)
     ("2" (SKOSIMP*)
      (("2" (INST + "max(e!1, x!1)")
        (("1" (GRIND :IF-MATCH NIL)
          (("1" (INST?) NIL NIL)
           ("2" (INST - "t!1") (("2" (ASSERT) NIL NIL)) NIL))
          NIL)
         ("2" (DELETE -1 2) (("2" (GRIND) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|max_TCC1| "" (INST + "lambda A: epsilon! (x: (A)): maximum(A, x)")
    (("1" (SKOLEM!)
      (("1" (USE "epsilon_ax[(A!1)]")
        (("1" (GROUND)
          (("1" (DELETE 2)
            (("1" (USE "maximum_exists")
              (("1" (SKOLEM!) (("1" (INST?) (("1" (GRIND) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("2" (DELETE 2)
          (("2" (TYPEPRED "A!1")
            (("2" (GRIND :EXCLUDE ("is_finite")) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL)
     ("2" (GRIND :EXCLUDE ("is_finite")) NIL NIL))
    NIL)
   (|max_prop1| "" (SKOLEM!)
    (("" (TYPEPRED "max(A!1)")
      (("" (EXPAND "maximum") (("" (INST?) NIL NIL)) NIL)) NIL))
    NIL)
   (|max_prop2| "" (SKOLEM!)
    (("" (REDUCE) (("" (USE "max_prop1") (("" (ASSERT) NIL NIL)) NIL))
      NIL))
    NIL)
   (|max_prop3| "" (SKOLEM!)
    (("" (REDUCE) (("" (USE "max_prop1") (("" (ASSERT) NIL NIL)) NIL))
      NIL))
    NIL)
   (|max_def| "" (SKOLEM!)
    (("" (REWRITE "maximum" :DIR RL)
      (("" (GROUND)
        (("" (USE "unique_maximum") (("" (ASSERT) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|max_singleton| "" (GRIND :REWRITES "max_def") NIL NIL)
   (|max_subset| "" (SKOSIMP)
    (("" (REWRITE "max_prop2")
      (("" (SKOLEM!)
        (("" (USE "max_prop1" ("A" "B!1" "x" "x!1"))
          (("" (GRIND) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|max_subset2| "" (SKOSIMP)
    (("" (ASSERT)
      (("" (REWRITE "max_def")
        (("" (SKOLEM!)
          (("" (USE "max_prop1" ("A" "B!1" "x" "t!1"))
            (("" (GRIND) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|max_inter1| "" (SKOLEM!)
    (("" (REWRITE "max_subset") (("" (GRIND) NIL NIL)) NIL)) NIL)
   (|max_inter2| "" (SKOLEM!)
    (("" (REWRITE "max_subset") (("" (GRIND) NIL NIL)) NIL)) NIL)
   (|max_union| "" (SKOLEM!)
    (("" (REWRITE "max_def")
      (("1" (GROUND)
        (("1" (GRIND) NIL NIL)
         ("2" (GRIND :EXCLUDE "max")
          (("1" (USE "max_prop1" ("A" "A!1" "x" "t!1"))
            (("1" (ASSERT) NIL NIL)) NIL)
           ("2" (USE "max_prop1" ("A" "B!1" "x" "t!1"))
            (("2" (ASSERT) NIL NIL)) NIL))
          NIL))
        NIL)
       ("2" (GRIND) NIL NIL))
      NIL))
    NIL)
   (|max_add| "" (SKOLEM!)
    (("" (REWRITE "max_def")
      (("1" (GRIND :IF-MATCH NIL)
        (("1" (USE "max_prop1" ("A" "A!1" "x" "t!1")) NIL NIL)
         ("2" (USE "max_prop1" ("A" "A!1" "x" "t!1"))
          (("2" (ASSERT) NIL NIL)) NIL))
        NIL)
       ("2" (GRIND) NIL NIL))
      NIL))
    NIL))
  
  
  $$$time.pvs
  time : THEORY
  
    BEGIN
  
    time : NONEMPTY_TYPE = nonneg_real
  
    END time
  
  $$$clocks.pvs
  clocks : THEORY
  
    BEGIN
  
    IMPORTING time
  
  
    %--------------
    %  Definition
    %--------------
  
    t, u : VAR time
  
    E, E1, E2 : VAR set[time]
  
  
    cut(E, t) : set[time] = { u | E(u) AND u < t }
  
    cut_union : LEMMA
  	cut(union(E1, E2), t) = union(cut(E1, t), cut(E2, t))
  
    cut_subset : LEMMA
  	subset?(E1, E2) IMPLIES subset?(cut(E1, t), cut(E2, t))
  
    cut_emptyset : LEMMA
  	cut(emptyset, t) = emptyset
  
    is_clock(E) : bool = FORALL t : is_finite(cut(E, t))
  
    emptyset_is_clock : LEMMA is_clock(emptyset[time])
  
    clock : NONEMPTY_TYPE = (is_clock)
  
  
  
    %----------------------
    %  Closure properties
    %----------------------
  
    H, H1, H2 : VAR clock
  
    clock_subset : LEMMA subset?(E, H) IMPLIES is_clock(E)
  
  
    clock_union: JUDGEMENT union(H1, H2) HAS_TYPE clock
  
    clock_inter1: JUDGEMENT intersection(H, E) HAS_TYPE clock
  
    clock_inter2: JUDGEMENT intersection(E, H) HAS_TYPE  clock
  
    clock_emptyset: JUDGEMENT emptyset HAS_TYPE clock
  
    clock_singleton: JUDGEMENT singleton(t) HAS_TYPE clock
  
    clock_add: JUDGEMENT add(t, H) HAS_TYPE clock
  
    clock_remove: JUDGEMENT remove(t, H) HAS_TYPE clock
  
    clock_rest: JUDGEMENT rest(H) HAS_TYPE clock
  
    cut_finite: JUDGEMENT cut(H, t) HAS_TYPE finite_set[time]
  
  
    END clocks
  
  $$$clocks.prf
  (|clocks|
   (|cut_union| "" (SKOLEM!)
    (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL))
    NIL)
   (|cut_subset| "" (SKOSIMP)
    (("" (GRIND :IF-MATCH NIL) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL))
      NIL))
    NIL)
   (|cut_emptyset| "" (SKOLEM!)
    (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL))
    NIL)
   (|emptyset_is_clock| ""
    (GRIND :EXCLUDE ("emptyset" "is_finite") :REWRITES
     ("cut_emptyset" "finite_emptyset[time]"))
    NIL NIL)
   (|clock_TCC1| "" (LEMMA "emptyset_is_clock")
    (("" (INST + "emptyset") NIL NIL)) NIL)
   (|clock_subset| ""
    (GRIND :EXCLUDE ("subset?" "is_finite") :REWRITES ("cut_subset"))
    (("" (USE "finite_subset" ("S" "cut(E!1, t!1)"))
      (("" (ASSERT) NIL NIL)) NIL))
    NIL)
   (|clock_union| ""
    (GRIND :EXCLUDE ("union" "is_finite") :REWRITES
     ("finite_union[time]" "cut_union"))
    NIL NIL)
   (|clock_inter1| "" (SKOLEM!)
    (("" (USE "clock_subset")
      (("" (AUTO-REWRITE "intersection_subset1[time]")
        (("" (ASSERT) NIL NIL)) NIL))
      NIL))
    NIL)
   (|clock_inter2| "" (SKOLEM!)
    (("" (REWRITE "intersection_commutative")
      (("" (REWRITE "clock_inter1") NIL NIL)) NIL))
    NIL)
   (|clock_emptyset| "" (REWRITE "emptyset_is_clock") NIL NIL)
   (|clock_singleton| ""
    (GRIND :EXCLUDE ("singleton" "is_finite") :REWRITES
     ("finite_singleton[time]"))
    (("" (CASE "subset?(cut(singleton(t!1), t!2), singleton(t!1))")
      (("1" (FORWARD-CHAIN "finite_subset") NIL NIL)
       ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL))
      NIL))
    NIL)
   (|clock_add| ""
    (AUTO-REWRITE "add_as_union[time]" "clock_singleton" "clock_union")
    (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL)
   (|clock_remove| "" (SKOLEM!)
    (("" (USE "clock_subset")
      (("" (ASSERT) (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|clock_rest| "" (SKOLEM!)
    (("" (USE "clock_subset")
      (("" (ASSERT) (("" (REWRITE "rest_subset") NIL NIL)) NIL)) NIL))
    NIL)
   (|cut_finite| "" (SUBTYPE-TCC) NIL NIL))
  
  
  --------------45B001C1407BA0798CAC0F90--
  

How-To-Repeat: 

Fix: 
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools