%% PVS Version 4.1 - Allegro CL Enterprise Edition 8.0 [Linux (x86)] (Apr 20, 2007 0:08)
%% 8.0 [Linux (x86)] (Apr 20, 2007 0:08)
$$$obt.pvs
obt [T : TYPE,  <= : (total_order?[T])] : THEORY
BEGIN
IMPORTING binary_tree[T]

A, B, C: VAR binary_tree
x, y, z: VAR T
pp: VAR pred[T]
i, j, k: VAR nat

size(A) : nat =
  reduce_nat(0, (LAMBDA x, i, j: i + j + 1))(A)

ordered?(A) : RECURSIVE bool =
  (IF node?(A) THEN (every((LAMBDA y: y<=val(A)), left(A)) AND
                     every((LAMBDA y: val(A)<=y), right(A)) AND
                     ordered?(left(A)) AND
                     ordered?(right(A)))
         ELSE TRUE ENDIF)
  MEASURE size

insert(x, A): RECURSIVE binary_tree[T] =
  (CASES A OF
    leaf: node(x, leaf, leaf),
    node(y, B, C): (IF x<=y THEN node(y, insert(x, B), C)
                            ELSE node(y, B, insert(x, C))
                    ENDIF)
   ENDCASES)
  MEASURE size(A)

ordered?_insert_step: LEMMA
   pp(x) AND every(pp, A) IMPLIES every(pp, insert(x, A))

ordered?_insert: THEOREM
   ordered?(A) IMPLIES ordered?(insert(x, A))

search(x, A): RECURSIVE bool =
  (CASES A OF
    leaf: FALSE,
    node(y, B, C): (IF x = y THEN TRUE
                         ELSIF x<=y THEN search(x, B)
                           ELSE search(x, C)
                    ENDIF)
   ENDCASES)
  MEASURE size(A)

search_insert: THEOREM search(y, insert(x, A)) = (x = y OR search(y, A))

END obt

$$$obt.prf
(obt (ordered?_TCC1 0 (ordered?_TCC1-1 nil 3386618414 3386618434 ("" (termination-tcc) nil nil) proved ((reduce_nat adt-def-decl "[binary_tree -> nat]" binary_tree_adt nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (size const-decl "nat" obt nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) 694 320 nil nil)) (ordered?_TCC2 0 (ordered?_TCC2-1 nil 3386618414 3386618435 ("" (termination-tcc) nil nil) proved ((reduce_nat adt-def-decl "[binary_tree -> nat]" binary_tree_adt nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (size const-decl "nat" obt nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) 300 230 nil nil)) (insert_TCC1 0 (insert_TCC1-1 nil 3386618414 3386618435 ("" (termination-tcc) nil nil) proved ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (reduce_nat adt-def-decl "[binary_tree -> nat]" binary_tree_adt nil) (size const-decl "nat" obt nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) 249 200 nil nil)) (insert_TCC2 0 (insert_TCC2-1 nil 3386618414 3386618435 ("" (termination-tcc) nil nil) proved ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (reduce_nat adt-def-decl "[binary_tree -> nat]" binary_tree_adt nil) (size const-decl "nat" obt nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) 252 190 nil nil)) (ordered?_insert_step 0 (ordered?_insert_step-1 nil 3386621172 3386621180 ("" (induct-and-simplify "A") nil nil) proved ((binary_tree type-decl nil binary_tree_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" binary_tree_adt nil) (insert def-decl "binary_tree[T]" obt nil) (T formal-type-decl nil obt nil) (binary_tree_induction formula-decl nil binary_tree_adt nil)) 7230 240 t shostak)) (ordered?_insert 0 (ordered?_insert-2 "" 3386621159 3386621159 ("" (induct-and-simplify "A" :rewrites "ordered?_insert_step") (("" (rewrite "ordered?_insert_step") (("" (typepred "<=") (("" (grind :if-match all) nil nil)) nil)) nil)) nil) proved nil 90560 750 t shostak) (ordered?_insert-1 nil 3386620246 3386620674 ("" (induct "A") (("1" (skosimp) (("1" (expand "insert") (("1" (expand "ordered?" +) (("1" (assert) (("1" (expand "every") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "insert" +) (("2" (prop) (("1" (inst?) (("1" (expand "ordered?" (-4 1)) (("1" (prop) (("1" (rewrite "ordered?_insert_step") nil nil)) nil)) nil)) nil) ("2" (inst? -2) (("2" (expand "ordered?" (-3 2)) (("2" (prop) (("2" (rewrite "ordered?_insert_step") (("2" (typepred "<=") (("2" (expand "total_order?") (("2" (flatten) (("2" (expand "dichotomous?") (("2" (inst?) (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((<= formal-const-decl "(total_order?[T])" obt nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (reflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (antisymmetric? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (dichotomous? const-decl "bool" orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (ordered?_insert_step formula-decl nil obt nil) (every adt-def-decl "boolean" binary_tree_adt nil) (binary_tree type-decl nil binary_tree_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (ordered? def-decl "bool" obt nil) (insert def-decl "binary_tree[T]" obt nil) (T formal-type-decl nil obt nil) (binary_tree_induction formula-decl nil binary_tree_adt nil)) 428250 290 t shostak)) (search_insert 0 (search_insert-1 nil 3386621197 3386621202 ("" (induct-and-simplify "A") nil nil) proved ((binary_tree type-decl nil binary_tree_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (search def-decl "bool" obt nil) (insert def-decl "binary_tree[T]" obt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T formal-type-decl nil obt nil) (binary_tree_induction formula-decl nil binary_tree_adt nil)) 4208 390 t shostak)))

$$$leaftree.pvs
leaftree[T : TYPE] : DATATYPE
 BEGIN
  leaf(val : T) : leaf?
  node(subs : list[leaftree]): node?
 END leaftree

$$$dt.pvs
dt[t1, t2: TYPE, c: t1]: DATATYPE
 BEGIN
  b: b?
  c(a1:[t1 -> t2], a2: dt): c?
 END dt

$$$disj_union.pvs
disj_union[A, B: TYPE] : DATATYPE
  BEGIN
    inl(left : A): inl?
    inr(right : B): inr?
  END disj_union

$$$combinators.pvs
combinators  : THEORY
  BEGIN
  combinators: DATATYPE
       BEGIN
         K: K?
         S: S?
         app(operator, operand: combinators): app?
       END combinators

  x, y, z: VAR combinators

  reduces_to: PRED[[combinators, combinators]]

  K: AXIOM reduces_to(app(app(K, x), y), x)
  S: AXIOM reduces_to(app(app(app(S, x), y), z), app(app(x, z), app(y, z)))

  END combinators

$$$colors.pvs
colors: THEORY
BEGIN
  colors: DATATYPE
     BEGIN
       red: red?
       white: white?
       blue: blue?
     END colors
END colors

$$$binary_tree.pvs
binary_tree[T : TYPE] : DATATYPE
BEGIN
  leaf : leaf?
  node(val : T, left : binary_tree, right : binary_tree) : node?
END binary_tree

$$$binary_props.pvs
binary_props[T : TYPE] : THEORY

  BEGIN
  IMPORTING binary_tree[T]
  A, B, C, D: VAR binary_tree[T]
  x, y, z: VAR T

  leaf_leaf : LEMMA leaf?(leaf)
  node_node : LEMMA node?(node(x, B, C))

  leaf_leaf1: LEMMA A = leaf IMPLIES leaf?(A)

  node_node1: LEMMA A = node(x, B, C) IMPLIES node?(A)

  val_node: LEMMA val(node(x, B, C)) = x

  leaf_node: LEMMA NOT (leaf?(A) AND node?(A))

  node_leaf: LEMMA leaf?(A) OR node?(A)

  leaf_ext: LEMMA (FORALL (A, B: (leaf?)): A = B)
         
  node_ext:  LEMMA (FORALL (A : (node?)) : 
                    node(val(A), left(A), right(A)) = A)

  END binary_props

$$$binary_props.prf
(binary_props (leaf_leaf 0 (leaf_leaf-1 nil 3386894500 3386894505 ("" (assert) nil nil) proved nil 5067 20 t shostak)) (node_node 0 (node_node-1 nil 3386894511 3386894514 ("" (assert) nil nil) proved nil 2321 20 t shostak)) (leaf_leaf1 0 (leaf_leaf1-1 nil 3386894522 3386894542 ("" (assert) (("" (skosimp) (("" (assert) nil nil)) nil)) nil) proved nil 20058 20 t shostak)) (node_node1 0 (node_node1-1 nil 3386894549 3386894560 ("" (skosimp) (("" (assert) nil nil)) nil) proved nil 10190 30 t shostak)) (val_node 0 (val_node-1 nil 3386894566 3386894576 ("" (assert) nil nil) proved nil 10239 10 t shostak)) (leaf_node 0 (leaf_node-1 nil 3386894580 3386894594 ("" (assert) (("" (skosimp) (("" (assert) nil nil)) nil)) nil) proved nil 13088 30 t shostak)) (node_leaf 0 (node_leaf-1 nil 3386894598 3386894607 ("" (skosimp) (("" (assert) nil nil)) nil) proved nil 9713 10 t shostak)) (leaf_ext 0 (leaf_ext-1 nil 3386894613 3386894622 ("" (skosimp) (("" (assert) nil nil)) nil) proved nil 8507 20 t shostak)) (node_ext 0 (node_ext-1 nil 3386894627 3386894657 ("" (skosimp) (("" (assert) (("" (apply-extensionality) nil nil)) nil)) nil) proved ((node? adt-recognizer-decl "[binary_tree -> boolean]" binary_tree_adt nil) (boolean nonempty-type-decl nil booleans nil) (binary_tree type-decl nil binary_tree_adt nil) (T formal-type-decl nil binary_props nil) (binary_tree_node_extensionality formula-decl nil binary_tree_adt nil) (right adt-accessor-decl "[(node?) -> binary_tree]" binary_tree_adt nil) (left adt-accessor-decl "[(node?) -> binary_tree]" binary_tree_adt nil) (val adt-accessor-decl "[(node?) -> T]" binary_tree_adt nil) (node adt-constructor-decl "[[T, binary_tree, binary_tree] -> (node?)]" binary_tree_adt nil)) 29634 50 t shostak)))

$$$arith.pvs
arith: DATATYPE WITH SUBTYPES expr, term
 BEGIN
  num(n:int): num?              :term
  sum(t1:term,t2:term):   sum?  :term
% ...
  eq(t1: term, t2: term): eq?   :expr
  ift(e: expr, t1: term, t2: term): ift? :term
% ...
 END arith

arith_eval: THEORY
 BEGIN
  IMPORTING arith

  value: DATATYPE
   BEGIN
    bool(b:bool): bool?
    int(i:int): int?
   END value

  eval(a: arith): RECURSIVE
         {v: value | IF expr(a) THEN bool?(v) ELSE int?(v) ENDIF} =
   CASES a OF
    num(n):       int(n),
    sum(n1, n2):  int(i(eval(n1)) + i(eval(n2))),
    eq(n1, n2):   bool(i(eval(n1)) = i(eval(n2))),
    ift(e, n1, n2): IF b(eval(e)) THEN eval(n1) ELSE eval(n2) ENDIF    
   ENDCASES
   MEASURE a BY <<

 END arith_eval

$$$ackerman.pvs
ackermann: THEORY

BEGIN

i, j, k, m, n: VAR nat

ack(m,n): RECURSIVE nat =
  (IF m=0 THEN n+1
          ELSIF n=0 THEN ack(m-1,1)
                    ELSE ack(m-1, ack(m, n-1))
        ENDIF)
  MEASURE lex2(m, n)

ackr(n, (f: [nat->nat])): RECURSIVE nat =
  (IF n = 0 THEN f(1) ELSE f(ackr(n - 1, f)) ENDIF)
 MEASURE n

ackrmn(m)(n): RECURSIVE nat = 
 (IF m = 0 THEN n + 1 ELSE ackr(n, ackrmn(m - 1)) ENDIF)
 MEASURE m

ack_ackrmn: THEOREM
  ack(m, n) = ackrmn(m)(n)

END ackermann

$$$ackerman.prf
(|ackermann| (|ack_TCC1| "" (SUBTYPE-TCC) NIL)
 (|ack_TCC2| "" (TERMINATION-TCC) NIL)
 (|ack_TCC3| "" (SUBTYPE-TCC) NIL) (|ack_TCC4| "" (SUBTYPE-TCC) NIL)
 (|ack_TCC5| "" (TERMINATION-TCC) NIL)
 (|ack_TCC6| "" (TERMINATION-TCC) NIL NIL)
 (|ackr_TCC1| "" (SUBTYPE-TCC) NIL)
 (|ackr_TCC2| "" (TERMINATION-TCC) NIL)
 (|ack_ackrmn| "" (INDUCT "m")
  (("1" (GRIND) NIL)
   ("2" (SKOSIMP)
    (("2" (INDUCT "n")
      (("1" (GRIND) NIL)
       ("2" (SKOSIMP)
        (("2" (EXPAND "ack" +)
          (("2" (EXPAND "ackrmn" +)
            (("2" (EXPAND "ackr" +)
              (("2" (INST?)
                (("2" (EXPAND "ackrmn" -1)
                  (("2" (ASSERT) NIL))))))))))))))))))))


$$$top.pvs
top: THEORY
BEGIN
 IMPORTING ackermann, arith, binary_props, binary_tree, colors,
           combinators, disj_union, dt, leaftree, obt
END top