% The PVS prelude.

% The prelude consists of theories that are built in to the PVS system.
% It is typechecked the same as any other PVS theory, but there are hooks
% in the typechecker that require most of these theories to be available,
% hence the order of the theories is important.  For example, no formulas
% may be declared before the booleans are available, as the formula is
% expected to have type bool.  Since definitions implicitly involve both
% formulas and equality, the booleans theory may not include any
% definitions.  Formulas are given below as AXIOMs, POSTULATEs, and LEMMAs.
% POSTULATEs are formulas that can be proved using the decision procedures,
% but would have to be given as axioms in a pure development of the theory.
% AXIOMs are formulas that cannot be proved, and LEMMAS are formulas that
% have been proved.

% --------------------------------------------------------------------
% PVS
% Copyright (C) 2006, SRI International.  All Rights Reserved.

% This program is free software; you can redistribute it and/or
% modify it under the terms of the GNU General Public License
% as published by the Free Software Foundation; either version 2
% of the License, or (at your option) any later version.

% This program is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
% GNU General Public License for more details.

% You should have received a copy of the GNU General Public License
% along with this program; if not, write to the Free Software
% Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
% --------------------------------------------------------------------

% booleans declares the type boolean and its abbreviation bool, along
% with the boolean constants true and false and the boolean connectives.
% The properties of the connectives are given later, but the connectives
% are built in to the typechecker so must be provided early on.
% Note: the boolean type could be defined as the enumeration type {false,
% true}, but booleans are primitive; the correct handling of enumeration
% types requires the boolean type.

booleans: THEORY
 BEGIN

  boolean: NONEMPTY_TYPE
  bool: NONEMPTY_TYPE = boolean
  FALSE, TRUE: bool
  NOT, ¬: [bool -> bool]
  AND, &, ∧, OR, ∨, IMPLIES, =>, ⇒, WHEN, IFF, <=>, ⇔: [bool, bool -> bool]

 END booleans


% equalities contains the declaration for =.  It has a single type
% parameter.  Properties of equality are given in equality_props.

equalities [T: TYPE]: THEORY
 BEGIN

  =: [T, T -> boolean]

 END equalities


notequal[T: TYPE]: THEORY
 BEGIN
  x, y: VAR T

  /=(x, y): boolean = NOT (x = y);
  ≠: [T, T -> bool] = /=
 END notequal


% if_def provides the polymorphic declaration of the IF-THEN-ELSE
% connective.  Note that the declaration for IF is for a 3-ary function,
% and that the IF-THEN-ELSE form is simply an alternative syntax.

if_def [T: TYPE]: THEORY
 BEGIN

  IF:[boolean, T, T -> T]

 END if_def


% boolean_props provides lemmas about the boolean constants and
% connectives.  The lemmas define them in terms of IF-THEN-ELSE, though
% these lemmas should never be needed since the prover "knows" the
% connectives as primitives.  WHEN is a special case - it is translated to
% IMPLIES with the arguments reversed by the typechecker.

boolean_props: THEORY
 BEGIN
  A, B: VAR bool

  bool_exclusive: POSTULATE not (false = true)
  bool_inclusive: POSTULATE A = false or A = true

  not_def:       POSTULATE (not A) = IF A THEN false ELSE true ENDIF
  and_def:       POSTULATE (A and B) = IF A THEN B ELSE false ENDIF
  syand_def:     POSTULATE & = and
  or_def:        POSTULATE (A or B) = IF A THEN true ELSE B ENDIF
  implies_def:   POSTULATE (A implies B) = IF A THEN B ELSE true ENDIF
  syimplies_def: POSTULATE => = implies
  when_def:      POSTULATE (A when B) = (B implies A)
  iff_def:       POSTULATE (A iff B) = ((A and B) or (not A and not B))
  syiff_def:     POSTULATE <=> = iff

  excluded_middle: LEMMA A OR NOT A  

 END boolean_props


% xor_def provides the definition for XOR.  Note that this is not built in
% to the prover, so this definition will need to be expanded in order to use
% it.

xor_def: THEORY
 BEGIN
  A, B: VAR bool
  XOR(A, B): bool = (A /= B)
  
  xor_def: LEMMA (A xor B) = IF A THEN NOT B ELSE B ENDIF
 END xor_def


% quantifier_props defines some useful properties of quantifiers.  Note
% that these work well with the higher-order matching facility of the prover.

quantifier_props [t: TYPE]: THEORY
 BEGIN
  x: VAR t
  p, q: VAR [t -> bool]

  not_exists: LEMMA (EXISTS x: p(x)) = NOT (FORALL x: NOT p(x))

  exists_not: LEMMA (EXISTS x: NOT p(x)) = NOT (FORALL x: p(x))

  exists_or: LEMMA
    (EXISTS x: p(x) OR q(x)) = ((EXISTS x: p(x)) OR (EXISTS x: q(x)))

  exists_implies: LEMMA
    (EXISTS x: p(x) IMPLIES q(x)) = ((EXISTS x: NOT p(x)) OR (EXISTS x: q(x)))

  exists_and: LEMMA
    (EXISTS x: p(x) AND q(x)) IMPLIES ((EXISTS x: p(x)) AND (EXISTS x: q(x)))

  not_forall: LEMMA (FORALL x: p(x)) = NOT (EXISTS x: NOT p(x))

  forall_not: LEMMA (FORALL x: NOT p(x)) = NOT (EXISTS x: p(x))

  forall_and: LEMMA
    (FORALL x: p(x) AND q(x)) = ((FORALL x: p(x)) AND (FORALL x: q(x)))

  forall_or: LEMMA
    ((FORALL x: p(x)) OR (FORALL x: q(x))) IMPLIES (FORALL x: p(x) OR q(x))

 END quantifier_props  


% defined_types provides the declarations for types pred and setof

defined_types [t: TYPE]: THEORY
 BEGIN
  pred: TYPE = [t -> bool]
  PRED: TYPE = [t -> bool]
  predicate: TYPE = [t -> bool]
  PREDICATE: TYPE = [t -> bool]
  setof: TYPE = [t -> bool]
  SETOF: TYPE = [t -> bool]
 END defined_types


% exists1 provides a unique existence function; it takes a predicate
% and asserts that there is one and only one element of the type that
% satisfies the predicate.  The expression "exists1! (x:t): p(x)" is
% translated to "exists1(LAMBDA (x:t): p(x))".

exists1 [T: TYPE]: THEORY
 BEGIN
  x, y: VAR T
  p, q: VAR pred[T]

  unique?(p): bool = FORALL x, y: p(x) AND p(y) IMPLIES x = y

  exists1(p): bool = (EXISTS x: p(x)) AND unique?(p)

  unique_lem: LEMMA
    (FORALL x: p(x) IMPLIES q(x)) IMPLIES (unique?(q) IMPLIES unique?(p))

  exists1_lem: LEMMA (exists1! x: p(x)) IMPLIES (EXISTS x: p(x))

 END exists1


% equality_props provides some properties of IF and =.

equality_props[T: TYPE]: THEORY
 BEGIN

  x, y, z: VAR T
  b: VAR bool
  
  IF_true: POSTULATE IF true THEN x ELSE y ENDIF = x

  IF_false: POSTULATE IF false THEN x ELSE y ENDIF = y

  IF_same: LEMMA IF b THEN x ELSE x ENDIF = x

  reflexivity_of_equals: POSTULATE x = x

  transitivity_of_equals: POSTULATE x = y AND y = z IMPLIES x = z

  symmetry_of_equals: POSTULATE x = y IMPLIES y = x

 END equality_props


% if_props

if_props [s, t: TYPE]: THEORY
 BEGIN
  a, b, c: VAR bool
  x, y: VAR s
  f: VAR [s -> t]
  
  lift_if1: LEMMA
    f(IF a THEN x ELSE y ENDIF) = IF a THEN f(x) ELSE f(y) ENDIF

  lift_if2: LEMMA
    IF (IF a THEN b ELSE c ENDIF) THEN x ELSE y ENDIF
     = IF a THEN (IF b THEN x ELSE y ENDIF)
            ELSE (IF c THEN x ELSE y ENDIF) ENDIF

 END if_props


% functions provides the basic properties of functions.  Because of the
% type equivalence of [[t1,...,tn] -> t] and [t1,...,tn -> t], this
% theory handles any function arity.  However, this doesn't handle
% dependent function types, since the domain and range can't be separated.

functions [D, R: TYPE]: THEORY
 BEGIN
  f, g: VAR [D -> R]
  x, x1, x2: VAR D
  y: VAR R
  Drel: VAR PRED[[D, D]]
  Rrel: VAR PRED[[R, R]]

  extensionality_postulate: POSTULATE
     (FORALL (x: D): f(x) = g(x)) IFF f = g

  % The extensionality lemma is provided as it is easier to use
  % as a rewrite than the above postulate.
  extensionality: LEMMA
     (FORALL (x: D): f(x) = g(x)) IMPLIES f = g

  congruence: POSTULATE f = g AND x1 = x2 IMPLIES f(x1) = g(x2)

  eta: LEMMA (LAMBDA (x: D): f(x)) = f

  injective?(f): bool = (FORALL x1, x2: (f(x1) = f(x2) => (x1 = x2)))

  surjective?(f): bool = (FORALL y: (EXISTS x: f(x) = y))

  bijective?(f): bool = injective?(f) & surjective?(f)

  bij_is_inj: JUDGEMENT (bijective?) SUBTYPE_OF (injective?)
  
  bij_is_surj: JUDGEMENT (bijective?) SUBTYPE_OF (surjective?)

  domain(f): TYPE = D

  range(f): TYPE = R

  graph(f)(x, y): bool = (f(x) = y)

  preserves(f, Drel, Rrel): bool =
      FORALL x1, x2: Drel(x1, x2) IMPLIES Rrel(f(x1), f(x2))

  % Curried form
  preserves(Drel, Rrel)(f): bool = preserves(f, Drel, Rrel)

  inverts(f, Drel, Rrel): bool =
      FORALL x1, x2: Drel(x1, x2) IMPLIES Rrel(f(x2), f(x1))

  % Curried form
  inverts(Drel, Rrel)(f): bool = inverts(f, Drel, Rrel)

 END functions


functions_alt [D, R: TYPE, Drel: PRED[[D, D]], Rrel: PRED[[R, R]]]: THEORY
 BEGIN
  f: VAR [D -> R]
  preserves: [[D -> R] -> bool] = preserves(Drel, Rrel)
  inverts: [[D -> R] -> bool] = inverts(Drel, Rrel)
 END functions_alt


transpose[T1, T2, T3: TYPE]: THEORY
 BEGIN
  f: VAR [T1 -> [T2 -> T3]]
  x: VAR T1
  y: VAR T2

  transpose(f)(y)(x): T3 = f(x)(y)
 END transpose


% restrict is the restriction operator on functions, allowing a
% function defined on a supertype to be applied to a subtype.  Note
% that it is a conversion, so will be inserted automatically when needed.
% Note also that the typechecker expands restrict automatically in some
% cases if it is fully applied, i.e., restrict(f)(x) is replaced with f(x).

restrict [T: TYPE, S: TYPE FROM T, R: TYPE]: THEORY
 BEGIN

  f: VAR [T -> R]
  s: VAR S

  restrict(f)(s): R = f(s)
  CONVERSION restrict

  injective_restrict: LEMMA
    injective?(f) IMPLIES injective?(restrict(f))

  restrict_of_inj_is_inj: JUDGEMENT
    restrict(f: (injective?[T,R])) HAS_TYPE (injective?[S,R])

 END restrict


% restrict_props provides the lemma that extending a function from a given
% domain type to the same type is the identity.  This usually comes about
% because of theory instantiation, and the typechecker has this rule built
% in, so it won't be needed in general.

restrict_props[T: TYPE, R: TYPE]: THEORY
 BEGIN
  f: VAR [T -> R]
  restrict_full: LEMMA restrict[T, T, R](f) = f
 END restrict_props


% extend is the inverse of restrict.  The difference is that a default
% value must be provided, which keeps it from being a conversion, in
% general (but see extend_bool).

extend [T: TYPE, S: TYPE FROM T, R: TYPE, d: R]: THEORY
 BEGIN

  f: VAR [S -> R]
  t: VAR T

  extend(f)(t): R = IF S_pred(t) THEN f(t) ELSE d ENDIF

  restrict_extend: LEMMA restrict[T,S,R](extend(f)) = f

 END extend


% extend_bool provides a conversion for boolean valued extensions,
% providing the default value of false.  Thus a set of nats "is" a set
% of ints.

extend_bool [T: TYPE, S: TYPE FROM T]: THEORY
 BEGIN

  CONVERSION extend[T, S, bool, false]

 END extend_bool


% extend_props provides the lemma that extending a function from a given
% domain type to the same type is the identity.  This usually comes about
% because of theory instantiation, and the typechecker has this rule built
% in, so it won't be needed in general.

extend_props [T: TYPE, R: TYPE, d: R]: THEORY
 BEGIN
  f: VAR [T -> R]
  extend_full: LEMMA extend[T, T, R, d](f) = f
 END extend_props

%-------------------------------------------------------------------------
%
%  Cases in which the introduction of extend preserves properties.
%
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  extend_func_props
%-------------------------------------------------------------------------
extend_func_props[T: TYPE, S: TYPE FROM T, R: TYPE, d: R]: THEORY
 BEGIN

  surjective_extend: JUDGEMENT
    extend[T, S, R, d](f: (surjective?[S, R])) HAS_TYPE (surjective?[T, R])

 END extend_func_props


% The K combinator is used to trigger lambda conversions.
% Due to user demand, it is turned off by default.

K_conversion [T1, T2: TYPE]: THEORY
 BEGIN
  K_conversion(x:T1)(y:T2): T1 = x
%  CONVERSION K_conversion
 END K_conversion

K_props [T1, T2: TYPE, S: TYPE FROM T1]: THEORY
 BEGIN
  K_preserves: JUDGEMENT K_conversion[T1, T2](x:S)(y:T2) HAS_TYPE S
  K_preserves1: JUDGEMENT K_conversion[T1, T2](x:S) HAS_TYPE [T2 -> S]
 END K_props

% identity simply defines the identity function.  The identity is used for
% conversion expressions.  For example, "foo: T" is translated to
% "(LAMBDA (x:T): x)(foo)"

identity [T: TYPE]: THEORY
 BEGIN
  x: VAR T
  I: (bijective?[T, T]) = (LAMBDA x: x)
  id: (bijective?[T, T]) = (LAMBDA x: x)
  identity: (bijective?[T, T]) = (LAMBDA x: x)
 END identity


identity_props [T: TYPE, S: TYPE FROM T]: THEORY
 BEGIN
  x: VAR S
  I_preserves: JUDGEMENT I[T](x) HAS_TYPE S
  id_preserves: JUDGEMENT id[T](x) HAS_TYPE S
  identity_preserves: JUDGEMENT identity[T](x) HAS_TYPE S
 END identity_props


% relations defines properties that are useful in specifying binary
% relations.

relations [T: TYPE]: THEORY
 BEGIN

  R: VAR PRED[[T, T]]
  x, y, z: VAR T

  eq: pred[[T, T]] = (LAMBDA x, y: x = y)

  reflexive?(R): bool = FORALL x: R(x, x)

  irreflexive?(R): bool = FORALL x: NOT R(x, x)

  symmetric?(R): bool = FORALL x, y: R(x, y) IMPLIES R(y, x)

  antisymmetric?(R): bool = FORALL x, y: R(x, y) & R(y, x) => x = y

  connected?(R): bool = FORALL x, y: x /= y IMPLIES R(x, y) OR R(y, x)

  transitive?(R): bool = FORALL x, y, z: R(x, y) & R(y, z) => R(x, z)

  equivalence?(R): bool = reflexive?(R) AND symmetric?(R) AND transitive?(R)

  equivalence: TYPE = (equivalence?)

  equiv_is_reflexive:  JUDGEMENT (equivalence?) SUBTYPE_OF (reflexive?)
  equiv_is_symmetric:  JUDGEMENT (equivalence?) SUBTYPE_OF (symmetric?)
  equiv_is_transitive: JUDGEMENT (equivalence?) SUBTYPE_OF (transitive?)

  % Reflexive closure
  RC(R)(x, y): bool = (x = y) OR R(x, y)

  % Transitive closure
  TC(R)(x, y): INDUCTIVE bool = R(x,y) OR (EXISTS z: TC(R)(x,z) AND TC(R)(z,y))

  % Reflexive-transitive closure
  RTC(R)(x, y): bool = (x = y) OR TC(R)(x, y)

 END relations


% orders defines the usual ordering relations.  Be careful not to read too
% much into these definitions; < and <= are variables ranging over binary
% relations, not actual orders.  Their use below is suggestive of the
% defining properties.

orders [T: TYPE]: THEORY
 BEGIN
  x, y: VAR T
  <=, < : VAR pred[[T, T]]
  p: VAR pred[T]

  preorder?(<=): bool = reflexive?(<=) & transitive?(<=)

  preorder_is_reflexive:  JUDGEMENT (preorder?) SUBTYPE_OF (reflexive?[T])
  preorder_is_transitive: JUDGEMENT (preorder?) SUBTYPE_OF (transitive?[T])
  equiv_is_preorder:      JUDGEMENT (equivalence?[T]) SUBTYPE_OF (preorder?)

  partial_order?(<=): bool = preorder?(<=) & antisymmetric?(<=)

  po_is_preorder:      JUDGEMENT (partial_order?) SUBTYPE_OF (preorder?)
  po_is_antisymmetric: JUDGEMENT
    (partial_order?) SUBTYPE_OF (antisymmetric?[T])

  strict_order?(<): bool = irreflexive?(<) & transitive?(<)

  strict_is_irreflexive: JUDGEMENT
    (strict_order?) SUBTYPE_OF (irreflexive?[T])
  strict_order_is_antisymmetric: JUDGEMENT
    (strict_order?) SUBTYPE_OF (antisymmetric?[T])
  strict_is_transitive: JUDGEMENT
    (strict_order?) SUBTYPE_OF (transitive?[T])

  dichotomous?(<=): bool = (FORALL x, y: (x <= y OR y <= x))

  total_order?(<=): bool = partial_order?(<=) & dichotomous?(<=)

  total_is_po:          JUDGEMENT (total_order?) SUBTYPE_OF (partial_order?)
  total_is_dichotomous: JUDGEMENT (total_order?) SUBTYPE_OF (dichotomous?)

  linear_order?(<=): bool = total_order?(<=)

  linear_is_total: JUDGEMENT (linear_order?) SUBTYPE_OF (total_order?)
  total_is_linear: JUDGEMENT (total_order?)  SUBTYPE_OF (linear_order?)

  trichotomous?(<): bool = (FORALL x, y: x < y OR y < x OR x = y)

  strict_total_order?(<): bool = strict_order?(<) & trichotomous?(<)

  strict_total_is_strict: JUDGEMENT
    (strict_total_order?) SUBTYPE_OF (strict_order?)
  strict_total_is_trichotomous: JUDGEMENT
    (strict_total_order?) SUBTYPE_OF (trichotomous?)

  well_founded?(<): bool =
     (FORALL p:
        (EXISTS y: p(y))
	   IMPLIES (EXISTS (y:(p)): (FORALL (x:(p)): (NOT x < y))))

  strict_well_founded?(<): bool = strict_order?(<) & well_founded?(<)

  strict_well_founded_is_strict: JUDGEMENT
    (strict_well_founded?) SUBTYPE_OF (strict_order?)
  strict_well_founded_is_well_founded: JUDGEMENT
    (strict_well_founded?) SUBTYPE_OF (well_founded?)

  well_ordered?(<): bool = strict_total_order?(<) & well_founded?(<)

  well_ordered_is_strict_total: JUDGEMENT
    (well_ordered?) SUBTYPE_OF (strict_total_order?)
  well_ordered_is_well_founded: JUDGEMENT
    (well_ordered?) SUBTYPE_OF (well_founded?)

  nonempty_pred: TYPE = {p: pred[T] | EXISTS (x: T): p(x)}

  pe: VAR pred[T]

  upper_bound?(<)(x, pe): bool = FORALL (y: (pe)): y < x

  upper_bound?(<)(pe)(x): bool = upper_bound?(<)(x, pe)

  lower_bound?(<)(x, pe): bool = FORALL (y: (pe)): x < y

  lower_bound?(<)(pe)(x): bool = lower_bound?(<)(x, pe)

  least_upper_bound?(<)(x, pe): bool =
    upper_bound?(<)(x, pe) AND
      FORALL y: upper_bound?(<)(y, pe) IMPLIES (x < y OR x = y)

  least_upper_bound?(<)(pe)(x): bool = least_upper_bound?(<)(x, pe)

  greatest_lower_bound?(<)(x, pe): bool =
    lower_bound?(<)(x, pe) AND
      FORALL y: lower_bound?(<)(y, pe) IMPLIES (y < x OR x = y)

  greatest_lower_bound?(<)(pe)(x): bool = greatest_lower_bound?(<)(x, pe)

 END orders


orders_alt [T: TYPE, < : pred[[T, T]], pe: nonempty_pred[T]]: THEORY
 BEGIN
  x: VAR T
  upper_bound?: [T -> bool] = upper_bound?(<)(pe)
  least_upper_bound?: [T -> bool] = least_upper_bound?(<)(pe)
  lower_bound?: [T -> bool] = lower_bound?(<)(pe)
  greatest_lower_bound?: [T -> bool] = greatest_lower_bound?(<)(pe)
  
  least_upper_bound_is_upper_bound: JUDGEMENT
    (least_upper_bound?) SUBTYPE_OF (upper_bound?)

  greatest_lower_bound_is_lower_bound: JUDGEMENT
    (greatest_lower_bound?) SUBTYPE_OF (lower_bound?)
 END orders_alt


%-------------------------------------------------------------------------
%
%  Cases in which the introduction of restrict preserves properties.
%
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  restrict_order_props
%-------------------------------------------------------------------------
restrict_order_props[T: TYPE, S: TYPE FROM T]: THEORY
 BEGIN

  reflexive_restrict: JUDGEMENT
    restrict(R: (reflexive?[T])) HAS_TYPE (reflexive?[S])

  irreflexive_restrict: JUDGEMENT
    restrict(R: (irreflexive?[T])) HAS_TYPE (irreflexive?[S])

  symmetric_restrict: JUDGEMENT
    restrict(R: (symmetric?[T])) HAS_TYPE (symmetric?[S])

  antisymmetric_restrict: JUDGEMENT
    restrict(R: (antisymmetric?[T])) HAS_TYPE (antisymmetric?[S])

  connected_restrict: JUDGEMENT
    restrict(R: (connected?[T])) HAS_TYPE (connected?[S])

  transitive_restrict: JUDGEMENT
    restrict(R: (transitive?[T])) HAS_TYPE (transitive?[S])

  equivalence_restrict: JUDGEMENT
    restrict(R: (equivalence?[T])) HAS_TYPE (equivalence?[S])

  preorder_restrict: JUDGEMENT
    restrict(R: (preorder?[T])) HAS_TYPE (preorder?[S])

  partial_order_restrict: JUDGEMENT
    restrict(R: (partial_order?[T])) HAS_TYPE (partial_order?[S])

  strict_order_restrict: JUDGEMENT
    restrict(R: (strict_order?[T])) HAS_TYPE (strict_order?[S])

  dichotomous_restrict: JUDGEMENT
    restrict(R: (dichotomous?[T])) HAS_TYPE (dichotomous?[S])

  total_order_restrict: JUDGEMENT
    restrict(R: (total_order?[T])) HAS_TYPE (total_order?[S])

  trichotomous_restrict: JUDGEMENT
    restrict(R: (trichotomous?[T])) HAS_TYPE (trichotomous?[S])

  strict_total_order_restrict: JUDGEMENT
    restrict(R: (strict_total_order?[T])) HAS_TYPE (strict_total_order?[S])

  well_founded_restrict: JUDGEMENT
    restrict(R: (well_founded?[T])) HAS_TYPE (well_founded?[S])

  well_ordered_restrict: JUDGEMENT
    restrict(R: (well_ordered?[T])) HAS_TYPE (well_ordered?[S])

 END restrict_order_props


% Courtesy of Jerry James
extend_order_props[T: TYPE, S: TYPE FROM T]: THEORY
 BEGIN

  irreflexive_extend: JUDGEMENT
    extend[[T, T], [S, S], bool, FALSE](R: (irreflexive?[S]))
        HAS_TYPE (irreflexive?[T])

  symmetric_extend: JUDGEMENT
    extend[[T, T], [S, S], bool, FALSE](R: (symmetric?[S]))
        HAS_TYPE (symmetric?[T])

  antisymmetric_extend: JUDGEMENT
    extend[[T, T], [S, S], bool, FALSE](R: (antisymmetric?[S]))
        HAS_TYPE (antisymmetric?[T])

  transitive_extend: JUDGEMENT
    extend[[T, T], [S, S], bool, FALSE](R: (transitive?[S]))
        HAS_TYPE (transitive?[T])

  strict_order_extend: JUDGEMENT
    extend[[T, T], [S, S], bool, FALSE](R: (strict_order?[S]))
        HAS_TYPE (strict_order?[T])

 END extend_order_props


% wf_induction defines induction for any type that has a well-founded
% relation.

wf_induction [T: TYPE, < : (well_founded?[T])]: THEORY
 BEGIN

  wf_induction: LEMMA
    (FORALL (p: pred[T]):
      (FORALL (x: T):
        (FORALL (y: T): y<x IMPLIES p(y))
           IMPLIES p(x))
    IMPLIES
      (FORALL (x:T): p(x)))

 END wf_induction


% measure_induction builds on well-founded induction.  It allows
% induction over a type T for which a measure function m is defined.

measure_induction [T: TYPE, M: TYPE, m: [T -> M], < : (well_founded?[M])]: THEORY
 BEGIN

 measure_induction: LEMMA
  (FORALL (p: pred[T]):
     (FORALL (x: T): 
         (FORALL (y: T): m(y) < m(x) IMPLIES  p(y))
             IMPLIES p(x))
    IMPLIES (FORALL (x: T): p(x)))

 END measure_induction


% epsilons provides a "choice" function that does not have a nonemptiness
% requirement on the predicate.  Given a predicate over the type t,
% epsilon produces an element of satisfying that predicate if one exists,
% and otherwise produces an arbitrary element of that type.
% "epsilon! (x:t): p(x)" is translated to "epsilon(LAMBDA (x:t): p(x))".
% Note that the type parameter is given as nonempty, which means that
% there is an nonempty ASSUMPTION automatically generated for this theory.

epsilons [T: NONEMPTY_TYPE]: THEORY
 BEGIN
  p: VAR pred[T]
  x: VAR T

  epsilon(p): T

  epsilon_ax: AXIOM (EXISTS x: p(x)) => p(epsilon(p))

 END epsilons


% sets provides the polymorphic set type, along with the usual set
% operations.  It is important to bear in mind that a set is just
% a predicate.

sets [T: TYPE]: THEORY
 BEGIN

  set: TYPE = setof[T]

  x, y: VAR T

  a, b, c: VAR set

  p: VAR PRED[T]

  member(x, a): bool = a(x)

  empty?(a): bool = (FORALL x: NOT member(x, a))

  emptyset: set = {x | false}

  nonempty?(a): bool = NOT empty?(a)

  nonempty_set: TYPE = (nonempty?)

  full?(a): bool = (FORALL x: member(x, a))

  fullset: set = {x | true}

  nontrivial?(a): bool = a /= emptyset & a /= fullset

  subset?(a, b): bool = (FORALL x: member(x, a) => member(x, b))

  strict_subset?(a, b): bool = subset?(a, b) & a /= b

  union(a, b): set = {x | member(x, a) OR member(x, b)}

  intersection(a, b): set = {x | member(x, a) AND member(x, b)}

  disjoint?(a, b): bool = empty?(intersection(a, b))

  complement(a): set = {x | NOT member(x, a)} 

  difference(a, b): set = {x | member(x, a) AND NOT member(x, b)}

  symmetric_difference(a, b): set =
    union(difference(a, b), difference(b, a))

  every(p)(a): bool = FORALL (x:(a)): p(x)

  every(p, a): bool = FORALL (x:(a)): p(x)

  some(p)(a): bool = EXISTS (x:(a)): p(x)

  some(p, a): bool = EXISTS (x:(a)): p(x)

  singleton?(a): bool = (EXISTS (x:(a)): (FORALL (y:(a)): x = y))

  singleton(x): (singleton?) = {y | y = x}

  % CONVERSION+ singleton

  add(x, a): (nonempty?) = {y | x = y OR member(y, a)}

  remove(x, a): set = {y | x /= y AND member(y, a)}

  % A choice function for nonempty sets
  % No longer defined, so that grind will not expand epsilon.
  % It's generally easier to use typepred on choose than to bring in epsilon_ax
  % Can always bring in choose_is_epsilon axiom if the expansion is desired.
  choose(p: (nonempty?)): (p) % = epsilon(p)

  choose_is_epsilon: AXIOM FORALL (p: (nonempty?)): choose(p) = epsilon(p)

  the(p: (singleton?)): (p)

  the_lem: LEMMA FORALL (p: (singleton?)): the(p) = epsilon(p)

  the_prop: LEMMA FORALL (p: (singleton?)): p(the(p))

  singleton_elt(a: (singleton?)): T = the! x: member(x, a)

  CONVERSION+ singleton_elt

  is_singleton: LEMMA
    FORALL a: (nonempty?(a) AND FORALL x, y: a(x) AND a(y) IMPLIES (x=y))
      IMPLIES singleton?(a)

  singleton_elt_lem: LEMMA singleton?(a) and a(x) IMPLIES singleton_elt(a) = x

  singleton_elt_def: LEMMA singleton?(a) IMPLIES singleton_elt(a) = choose(a)

  singleton_singleton: LEMMA singleton?(a) IMPLIES (EXISTS x: a = singleton(x))

  singleton_rew: LEMMA singleton_elt(singleton(x)) = x

  AUTO_REWRITE+ singleton_rew

  rest(a): set = IF empty?(a) THEN a ELSE remove(choose(a), a) ENDIF

  setofsets: TYPE = setof[setof[T]]
  
  A, B : Var setofsets

  powerset(a): setofsets = {b | subset?(b, a)}

  Union(A): set = {x | EXISTS (a: (A)): a(x)}

  Intersection(A): set = {x | FORALL (a: (A)): a(x)}

  nonempty_singleton: JUDGEMENT (singleton?) SUBTYPE_OF (nonempty?)
  nonempty_union1: JUDGEMENT union(a: (nonempty?), b: set) HAS_TYPE (nonempty?)
  nonempty_union2: JUDGEMENT union(a: set, b: (nonempty?)) HAS_TYPE (nonempty?)

 END sets


% Lemmas about sets - many of these came from Bruno Dutertre in the
% more_set_lemmas theory of the finite_sets library

sets_lemmas [T: TYPE]: THEORY
 BEGIN

  x, y: VAR T
  a, b, c: VAR set[T]
  A, B : Var setofsets[T]

  extensionality: LEMMA
      (FORALL x: member(x, a) IFF member(x, b)) IMPLIES (a = b)

  emptyset_is_empty?: LEMMA  empty?(a) IFF a = emptyset

  empty_no_members: LEMMA NOT member(x, emptyset)

  emptyset_min: LEMMA subset?(a, emptyset) IMPLIES a = emptyset

  nonempty_member: LEMMA nonempty?(a) IFF EXISTS x: member(x, a)

  fullset_member: LEMMA member(x, fullset)

  fullset_max: LEMMA subset?(fullset, a)  IMPLIES a = fullset

  fullset_is_full?: LEMMA full?(a) IFF a = fullset
  
  nonempty_exists: LEMMA nonempty?(a) IFF EXISTS (x: (a)): TRUE

  subset_emptyset: LEMMA subset?(emptyset, a)

  subset_fullset: LEMMA subset?(a, fullset)

  subset_reflexive: LEMMA subset?(a, a)

  subset_antisymmetric: LEMMA subset?(a, b) AND subset?(b, a) IMPLIES a = b

  subset_transitive: LEMMA
    subset?(a, b) AND subset?(b, c) IMPLIES subset?(a, c)

  subset_partial_order: LEMMA partial_order?(subset?[T])

  subset_is_partial_order: JUDGEMENT
    subset?[T] HAS_TYPE (partial_order?[set[T]])

  strict_subset_irreflexive: LEMMA NOT strict_subset?(a, a)

  strict_subset_transitive: LEMMA
    strict_subset?(a, b) AND strict_subset?(b, c) IMPLIES
     strict_subset?(a, c)

  strict_subset_strict_order: LEMMA strict_order?(strict_subset?[T])

  strict_subset_is_strict_order: JUDGEMENT
    strict_subset?[T] HAS_TYPE (strict_order?[set[T]])

  union_idempotent: LEMMA union(a, a) = a

  union_commutative: LEMMA union(a, b) = union(b, a)

  union_associative: LEMMA union(union(a, b), c) = union(a, union(b, c))

  union_empty: LEMMA union(a, emptyset) = a

  union_full: LEMMA union(a, fullset) = fullset

  union_subset1: LEMMA subset?(a, union(a, b))

  union_subset2: LEMMA subset?(a, b) IMPLIES union(a, b) = b

  subset_union: LEMMA subset?(union(a, b), c) = (subset?(a, c) AND subset?(b, c)) 

  union_upper_bound : LEMMA
    subset?(a, c) and subset?(b, c) IMPLIES subset?(union(a, b), c)
  
  union_difference: LEMMA union(a, b) = union(a, difference(b, a))

  union_diff_subset: LEMMA subset?(a, b) IMPLIES union(a, difference(b, a)) = b

  intersection_idempotent: LEMMA intersection(a, a) = a

  intersection_commutative: LEMMA intersection(a, b) = intersection(b, a)

  intersection_associative: LEMMA
    intersection(intersection(a, b), c) = intersection(a, intersection(b, c))

  intersection_empty: LEMMA intersection(a, emptyset) = emptyset

  intersection_full: LEMMA intersection(a, fullset) = a

  intersection_subset1: LEMMA subset?(intersection(a, b), a)

  intersection_subset2: LEMMA subset?(a, b) IMPLIES intersection(a, b) = a

  intersection_lower_bound: LEMMA
    subset?(c, a) and subset?(c, b) IMPLIES subset?(c, intersection(a, b))

  distribute_intersection_union: LEMMA
    intersection(a, union(b, c))
        = union(intersection(a, b), intersection(a, c))

  distribute_union_intersection: LEMMA
    union(a, intersection(b, c)) = intersection(union(a, b), union(a, c))

  complement_emptyset: LEMMA complement(emptyset[T]) = fullset

  complement_fullset: LEMMA complement(fullset[T]) = emptyset

  complement_complement: LEMMA complement(complement(a)) = a

  complement_equal: LEMMA complement(a) = complement(b) IFF a = b

  subset_complement: LEMMA
    subset?(complement(a), complement(b)) IFF subset?(b, a)

  demorgan1: LEMMA
    complement(union(a, b)) = intersection(complement(a), complement(b))

  demorgan2: LEMMA
    complement(intersection(a, b)) = union(complement(a), complement(b))

  difference_emptyset1: LEMMA difference(a, emptyset) = a

  difference_emptyset2: LEMMA difference(emptyset, a) = emptyset

  difference_fullset1: LEMMA difference(a, fullset) = emptyset

  difference_fullset2: LEMMA difference(fullset, a) = complement(a)

  difference_intersection: LEMMA
    difference(a, b) = intersection(a, complement(b))

  difference_difference1: LEMMA
    difference(difference(a, b), c) = difference(a, union(b, c))

  difference_difference2: LEMMA
    difference(a, difference(b, c))
      = union(difference(a, b), intersection(a, c))

  difference_subset : LEMMA  subset?(difference(a, b), a)

  difference_subset2: LEMMA
    subset?(a, b) IMPLIES difference(a, b) = emptyset

  difference_disjoint: LEMMA disjoint?(a, difference(b, a))

  difference_disjoint2: LEMMA disjoint?(a, b) IMPLIES difference(a, b) = a

  diff_union_inter: LEMMA
    difference(union(a, b), a) = difference(b, intersection(a, b))

  nonempty_add: LEMMA NOT empty?(add(x, a))

  member_add: LEMMA member(x, a) IMPLIES add(x, a) = a

  member_add_reduce: LEMMA member(x, add(y, a)) = (x = y or member(x, a))

  member_remove: LEMMA NOT member(x, a) IMPLIES remove(x, a) = a

  add_remove_member: LEMMA member(x, a) IMPLIES add(x, remove(x, a)) = a

  remove_add_member: LEMMA NOT member(x, a) IMPLIES remove(x, add(x, a)) = a

  subset_add: LEMMA subset?(a, add(x, a))

  add_as_union: LEMMA add(x, a) = union(a, singleton(x))

  singleton_as_add: LEMMA singleton(x) = add(x, emptyset)

  subset_remove: LEMMA subset?(remove(x, a), a)

  remove_as_difference: LEMMA remove(x, a) = difference(a, singleton(x))

  remove_member_singleton: LEMMA remove(x, singleton(x)) = emptyset

  choose_rest: LEMMA NOT empty?(a) IMPLIES add(choose(a), rest(a)) = a

  choose_member: LEMMA NOT empty?(a) IMPLIES member(choose(a), a)
  
  choose_not_member: LEMMA
      NOT empty?(a) IMPLIES NOT member(choose(a), rest(a))
  
  rest_not_equal: LEMMA NOT empty?(a) IMPLIES rest(a) /= a

  rest_member: LEMMA member(x,rest(a)) IMPLIES member(x,a)

  rest_subset : LEMMA subset?(rest(a), a)

  choose_add: LEMMA choose(add(x, a)) = x OR member(choose(add(x, a)), a)

  choose_rest_or: LEMMA
    member(x,a) IMPLIES member(x,rest(a)) OR x = choose(a)

  choose_singleton: LEMMA choose(singleton(x)) = x

  rest_singleton: LEMMA rest(singleton(x)) = emptyset[T]
  
  singleton_subset: LEMMA member(x, a) IFF subset?(singleton(x), a)

  rest_empty_lem: LEMMA NOT empty?(a) AND empty?(rest(a))
                          IMPLIES a = singleton(choose(a))

  singleton_disjoint: LEMMA NOT member(x, a) IMPLIES disjoint?(singleton(x), a)

  disjoint_remove_left: LEMMA
    disjoint?(a, b) IMPLIES disjoint?(remove(x, a), b)

  disjoint_remove_right: LEMMA
    disjoint?(a, b) IMPLIES disjoint?(a, remove(x, b))

  union_disj_remove_left: LEMMA
    disjoint?(a, b) AND a(x) IMPLIES
      union(remove(x, a), b) = remove(x, union(a, b))

  union_disj_remove_right: LEMMA
    disjoint?(a, b) AND b(x) IMPLIES
      union(a, remove(x, b)) = remove(x, union(a, b))

  subset_powerset: LEMMA subset?(a, b) IFF member(a, powerset(b))

  empty_powerset: LEMMA empty?(a) IFF singleton?(powerset(a))

  powerset_emptyset: LEMMA member(emptyset, powerset(a))

  nonempty_powerset: JUDGEMENT powerset(a) HAS_TYPE (nonempty?[set[T]])

  powerset_union: LEMMA Union(powerset(a)) = a

  powerset_intersection: LEMMA empty?(Intersection(powerset(a)))

  powerset_subset: LEMMA subset?(a, b) IFF subset?(powerset(a), powerset(b))

  Union_empty: LEMMA empty?(Union(A)) IFF empty?(A) OR every(empty?)(A)

  Union_full: LEMMA
    full?(Union(A)) IFF (FORALL x: EXISTS (a: (A)): member(x, a))

  Union_member: LEMMA member(x,Union(A)) IFF (EXISTS (a:(A)): member(x,a))

  Union_subset: LEMMA FORALL (a: (A)): subset?(a, Union(A))

  Union_surjective: JUDGEMENT
    Union HAS_TYPE (surjective?[setofsets[T], set[T]])

  Union_emptyset_rew: LEMMA Union(emptyset[set[T]]) = emptyset

  Union_union_rew: LEMMA nonempty?(A) IMPLIES
                            Union(A) = union(choose(A), Union(rest(A)))

  Intersection_empty: LEMMA
    empty?(Intersection(A)) IFF
     (FORALL x: EXISTS (a: (A)): NOT member(x, a))

  Intersection_full: LEMMA full?(Intersection(A)) IFF every(full?)(A)

  Intersection_member: LEMMA
    member(x,Intersection(A)) IFF (FORALL (a:(A)): member(x,a))

  %% The Intersection function should only be applied to nonempty sets of
  %% sets.  This is why.
  Intersection_empty_full: COROLLARY full?(Intersection(emptyset[set[T]]))

  Intersection_surjective: JUDGEMENT
    Intersection HAS_TYPE (surjective?[setofsets[T], set[T]])

  Intersection_intersection_rew: LEMMA
    nonempty?(A) IMPLIES
      Intersection(A) = intersection(choose(A), Intersection(rest(A)))

  Complement(A): setofsets[T] = {a | EXISTS (b: (A)): a = complement(b)}

  Complement_empty: LEMMA empty?(Complement(A)) IFF empty?(A)

  Complement_full: LEMMA full?(Complement(A)) IFF full?(A)

  Complement_Complement: LEMMA Complement(Complement(A)) = A

  subset_Complement: LEMMA
    subset?(Complement(A), Complement(B)) IFF subset?(A, B)

  Complement_bijective: JUDGEMENT
    Complement HAS_TYPE (bijective?[setofsets[T], setofsets[T]])

  Demorgan1: LEMMA complement(Union(A)) = Intersection(Complement(A))
  Demorgan2: LEMMA complement(Intersection(A)) = Union(Complement(A))

END sets_lemmas


%-------------------------------------------------------------------------
%
%  An alternate formulation of function inverses.  The version above
%  requires that the domain type be nonempty.  This causes two
%  difficulties:
%
%  (1) Functions from empty types to empty types have inverses, but the
%      function_inverse theory cannot describe them.
%
%  (2) Bijections always have inverses, but function_inverse (uselessly)
%      generates TCCs requiring that the domain type be nonempty.
%
%  Furthermore, for non-injective functions, the function_inverse theory
%  only gives a way of generating *some* inverse, using the Axiom of Choice.
%  There is no way to ask whether some function *is* an inverse of the given
%  function.
%
%  This theory is presented in two parts.  The first part makes no
%  assumptions about the domain and range types at all.  It presents
%  basic definitions, and some results that can be proven with no
%  information on the types.  The second part uses an assumption on the
%  input types, which is constructed to be as easily satisfiable as
%  possible.  However, this is still not as convenient as the
%  function_inverse version when the domain type is known to be nonempty.
%
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%-------------------------------------------------------------------------
function_inverse_def[D: TYPE, R: TYPE]: THEORY
 BEGIN

  d: VAR D
  r: VAR R
  f: VAR [D -> R]
  g: VAR [R -> D]

  left_inverse?(g, f): bool = FORALL d: g(f(d)) = d
  right_inverse?(g, f): bool = FORALL r: f(g(r)) = r
  inverse?(g, f): bool = FORALL r: (EXISTS d: f(d) = r) => f(g(r)) = r

  left_inverse?(f)(g): MACRO bool = left_inverse?(g, f)
  right_inverse?(f)(g): MACRO bool = right_inverse?(g, f)
  inverse?(f)(g): MACRO bool = inverse?(g, f)

  %%% Left inverses / injective functions

  left_inverse_is_inverse: LEMMA
    FORALL f, (g: (left_inverse?(f))): inverse?(g, f)

  left_inj_surj: LEMMA
    FORALL f, (g: (left_inverse?(f))): injective?(f) AND surjective?(g)

  inj_left_alt: LEMMA
    FORALL (f: (injective?[D, R])), (g: (inverse?(f))): left_inverse?(g, f)

  surj_inv_alt: COROLLARY
    FORALL (f: (injective?[D, R])), (g: (inverse?(f))): surjective?(g)

  injective_inverse_alt: LEMMA
    FORALL (f: (injective?[D, R])), (g: (inverse?(f))): r = f(d) => g(r) = d

  comp_inverse_left_inj_alt: LEMMA
    FORALL (f: (injective?[D, R])), (g: (inverse?(f))): g(f(d)) = d

  noninjective_inverse_exists: LEMMA
    FORALL f: injective?(f) OR (EXISTS g: inverse?(g, f))

  %%% Right inverses / surjective functions

  right_inverse_is_inverse: LEMMA
    FORALL f, (g: (right_inverse?(f))): inverse?(g, f)

  right_surj_inj: LEMMA
    FORALL f, (g: (right_inverse?(f))): surjective?(f) AND injective?(g)

  surj_right_alt: LEMMA
    FORALL (f: (surjective?[D, R])), (g: (inverse?(f))): right_inverse?(g, f)

  inj_inv_alt: COROLLARY
    FORALL (f: (surjective?[D, R])), (g: (inverse?(f))): injective?(g)

  surjective_inverse_alt: LEMMA
    FORALL (f: (surjective?[D, R])), (g: (inverse?(f))): g(r) = d => r = f(d)

  comp_inverse_right_surj_alt: LEMMA
    FORALL (f: (surjective?[D, R])), (g: (inverse?(f))): f(g(r)) = r

  surjective_inverse_exists: LEMMA
    FORALL (f: (surjective?[D, R])): EXISTS g: inverse?(g, f)

  %%% Left-right inverses / bijective functions

  left_right_bij: COROLLARY
    FORALL f, g:
      right_inverse?(g, f) AND left_inverse?(g, f) =>
       bijective?(f) AND bijective?(g)

  bij_left_right: COROLLARY
    FORALL (f: (bijective?[D, R])), (g: (inverse?(f))):
      right_inverse?(g, f) AND left_inverse?(g, f)

  bij_inv_is_bij_alt: COROLLARY
    FORALL (f: (bijective?[D, R])), (g: (inverse?(f))): bijective?(g)

  bijective_inverse_alt: COROLLARY
    FORALL (f: (bijective?[D, R])), (g: (inverse?(f))): g(r) = d IFF r = f(d)

  comp_inverse_right_alt: COROLLARY
    FORALL (f: (bijective?[D, R])), (g: (inverse?(f))): f(g(r)) = r

  comp_inverse_left_alt: COROLLARY
    FORALL (f: (bijective?[D, R])), (g: (inverse?(f))): g(f(d)) = d

  bijective_inverse_exists: LEMMA
    FORALL (f: (bijective?[D, R])): exists1(inverse?(f))

  % The following are provided as support for discharging the
  % assumption TCCs arising from the use of function_inverse_alt

  exists_inv1: LEMMA
    (EXISTS g: TRUE) IFF ((EXISTS (d: D): TRUE) OR (FORALL (r: R): FALSE))
  exists_inv2: LEMMA
    (EXISTS (f: (surjective?[D, R])): TRUE) =>
       ((EXISTS (d: D): TRUE) OR (FORALL (r: R): FALSE))
  exists_inv3: LEMMA
    (EXISTS f: NOT injective?(f)) =>
       ((EXISTS (d: D): TRUE) OR (FORALL (r: R): FALSE))

 END function_inverse_def


% function_inverse.  In practice this definition will only be useful
% for injective functions.  This is not defined in functions because the
% epsilon! operator forces the domain type to be nonempty.  Note
% that this theory may not be instantiated through dependent function
% types.

function_inverse[D: NONEMPTY_TYPE, R: TYPE]: THEORY
 BEGIN
  x: VAR D
  y: VAR R
  f: VAR [D -> R]
  g: VAR [R -> D]

  inverse(f)(y): D = (epsilon! x: f(x) = y)

  unique_bijective_inverse: JUDGEMENT
    inverse(f:(bijective?[D,R]))(y) HAS_TYPE {x:D | f(x) = y}

  bijective_inverse_is_bijective: JUDGEMENT
    inverse(f:(bijective?[D,R])) HAS_TYPE (bijective?[R,D])

  surjective_inverse: LEMMA
    FORALL (f:(surjective?[D, R])):
       inverse(f)(y) = x IMPLIES y = f(x)

  inverse_surjective: LEMMA
    FORALL (f:(surjective?[D, R])):
       f(inverse(f)(y)) = y

  injective_inverse: LEMMA
    FORALL (f:(injective?[D, R])):
       y = f(x) IMPLIES inverse(f)(y) = x

  inverse_injective: LEMMA
    FORALL (f:(injective?[D, R])):
       inverse(f)(f(x)) = x

  bijective_inverse: LEMMA
    FORALL (f:(bijective?[D, R])):
       inverse(f)(y) = x IFF y = f(x)

  bij_inv_is_bij: LEMMA
    bijective?(f) IMPLIES bijective?(inverse(f))

%   left_inverse?(g, f): bool = (FORALL x: g(f(x)) = x)

%   right_inverse?(g, f): bool = (FORALL y: f(g(y)) = y)

  surj_right: LEMMA surjective?(f) IFF right_inverse?(inverse(f), f)

  inj_left: LEMMA injective?(f) IFF left_inverse?(inverse(f), f)

  inj_inv: LEMMA surjective?(f) IMPLIES injective?(inverse(f))

  surj_inv: LEMMA injective?(f) IMPLIES surjective?(inverse(f))

  inv_inj_is_surj: JUDGEMENT
    inverse(f: (injective?[D, R])) HAS_TYPE (surjective?[R, D])
  inv_surj_is_inj: JUDGEMENT
    inverse(f: (surjective?[D, R])) HAS_TYPE (injective?[R, D])

  comp_inverse_right_surj: LEMMA
	FORALL (f:(surjective?[D,R])): f(inverse(f)(y)) = y

  comp_inverse_left_inj: LEMMA
	FORALL (f:(injective?[D,R])): inverse(f)(f(x)) = x

  comp_inverse_right: LEMMA
	FORALL (f:(bijective?[D,R])): f(inverse(f)(y)) = y

  comp_inverse_left: LEMMA
	FORALL (f:(bijective?[D,R])): inverse(f)(f(x)) = x

 END function_inverse


% This theory was provided by Jerry James
function_inverse_alt[D: TYPE, R: TYPE]: THEORY
 BEGIN

  ASSUMING

   % The function_inverse theory, in effect, forces its users to prove the
   % first disjunction; however, any of them give us the ability to define
   % inverses.  Note that the first two disjunctions are implied by each of
   % the others.  The axiom is expressed this way for the convenience of its
   % users, who may have any one of these pieces of evidence of invertibility
   % at hand.
   inverse_types: ASSUMPTION
     (EXISTS (d: D): TRUE) OR
     (FORALL (r: R): FALSE)

  ENDASSUMING

  d: VAR D
  r: VAR R
  f: VAR [D -> R]
  g: VAR [R -> D]

  inverses(f): TYPE+ = (inverse?(f))

  inverse_alt(f): inverses(f) = choose({g: inverses(f) | TRUE})


  bijective_inverse_is_inverse_alt: COROLLARY
    FORALL (f: (bijective?[D, R])), (g: inverses(f)): g = inverse_alt(f)

  unique_bijective_inverse_alt: JUDGEMENT
    inverse_alt(f: (bijective?[D,R]))(r) HAS_TYPE {d | f(d) = r}

  bijective_inverse_alt_is_bijective: JUDGEMENT
    inverse_alt(f: (bijective?[D,R])) HAS_TYPE (bijective?[R,D])

  inv_inj_is_surj_alt: JUDGEMENT
    inverse_alt(f: (injective?[D, R])) HAS_TYPE (surjective?[R, D])

  inv_surj_is_inj_alt: JUDGEMENT
    inverse_alt(f: (surjective?[D, R])) HAS_TYPE (injective?[R, D])

 END function_inverse_alt


% function_image provides the image and inverse_image functions.
% inverse_image is not the same as inverse; it is defined for all
% functions, not just injections, and returns a set.

function_image [D, R: TYPE]: THEORY
 BEGIN
  f: VAR [D -> R]
  x: VAR D
  y: VAR R
  X, X1, X2: VAR set[D]
  Y, Y1, Y2: VAR set[R]

  fun_exists: LEMMA (EXISTS y: TRUE) OR (NOT EXISTS x: TRUE)
                          IMPLIES (EXISTS f: TRUE)

  image(f, X): set[R] = {y: R | (EXISTS (x:(X)): y = f(x))}

  image(f)(X): set[R] = image(f, X)

  inverse_image(f, Y): set[D] = {x: D | member(f(x), Y)}

  inverse_image(f)(Y): set[D] = inverse_image(f, Y)

  image_inverse_image: LEMMA
    subset?(image(f, inverse_image(f, Y)), Y)

  inverse_image_image: LEMMA
    subset?(X, inverse_image(f, image(f, X)))

  image_subset: LEMMA
    subset?(X1, X2) IMPLIES subset?(image(f, X1), image(f, X2))

  inverse_image_subset: LEMMA
    subset?(Y1, Y2) IMPLIES subset?(inverse_image(f, Y1), inverse_image(f, Y2))

  image_union: LEMMA
    image(f, union(X1, X2)) = union(image(f, X1), image(f, X2))

  image_intersection: LEMMA
    subset?(image(f, intersection(X1, X2)),
            intersection(image(f, X1), image(f, X2)))

  inverse_image_union: LEMMA
    inverse_image(f, union(Y1, Y2))
      = union(inverse_image(f, Y1), inverse_image(f, Y2))

  inverse_image_intersection: LEMMA
    inverse_image(f, intersection(Y1, Y2))
      = intersection(inverse_image(f, Y1), inverse_image(f, Y2))

  inverse_image_complement: LEMMA
    inverse_image(f, complement(Y)) = complement(inverse_image(f, Y))

 END function_image


% functions_props defines function composition.  It can't be defined in
% functions because it involves three type parameters.

function_props [T1, T2, T3: TYPE]: THEORY
 BEGIN
  x: VAR T1
  f1: VAR [T1 -> T2]
  f2: VAR [T2 -> T3]
  X: VAR set[T1]
  R1: VAR PRED[[T1, T1]]
  R2: VAR PRED[[T2, T2]]
  R3: VAR PRED[[T3, T3]]

  o(f2, f1)(x): T3 = f2(f1(x))

  composition_injective: JUDGEMENT
    o(f2: (injective?[T2, T3]), f1: (injective?[T1, T2]))
      HAS_TYPE (injective?[T1, T3])

  composition_surjective: JUDGEMENT
    o(f2: (surjective?[T2, T3]), f1: (surjective?[T1, T2]))
      HAS_TYPE (surjective?[T1, T3])

  composition_bijective: JUDGEMENT
    o(f2: (bijective?[T2, T3]), f1: (bijective?[T1, T2]))
      HAS_TYPE (bijective?[T1, T3])

  image_composition: LEMMA
    image(f2, image(f1, X)) = image(f2 o f1, X)

  preserves_composition: LEMMA
    preserves(f1, R1, R2) AND preserves(f2, R2, R3)
      IMPLIES preserves(f2 o f1, R1, R3)

  inverts_composition1: LEMMA
    preserves(f1, R1, R2) AND inverts(f2, R2, R3)
      IMPLIES inverts(f2 o f1, R1, R3)

  inverts_composition2: LEMMA
    inverts(f1, R1, R2) AND preserves(f2, R2, R3)
      IMPLIES inverts(f2 o f1, R1, R3)
      
 END function_props


function_props_alt [T1, T2, T3: TYPE, R1: PRED[[T1, T1]],
                    R2: PRED[[T2, T2]], R3: PRED[[T3, T3]]]: THEORY
 BEGIN 
   composition_preserves: JUDGEMENT
     o(f2: (preserves[T2, T3, R2, R3]), f1: (preserves[T1, T2, R1, R2]))
       HAS_TYPE (preserves[T1, T3, R1, R3])

   composition_inverts1: JUDGEMENT
     o(f2: (preserves[T2, T3, R2, R3]), f1: (inverts[T1, T2, R1, R2]))
       HAS_TYPE (inverts[T1, T3, R1, R3])

   composition_inverts2: JUDGEMENT
     o(f2: (inverts[T2, T3, R2, R3]), f1: (preserves[T1, T2, R1, R2]))
       HAS_TYPE (inverts[T1, T3, R1, R3])
 END function_props_alt  


% function_props2 defines the associativity of function composition.  It
% can't be defined in function_props because it involves four type
% parameters.

function_props2 [T1, T2, T3, T4: TYPE]: THEORY
 BEGIN
  f1: VAR [T1 -> T2]
  f2: VAR [T2 -> T3]
  f3: VAR [T3 -> T4]

  assoc: LEMMA (f3 o f2) o f1 = f3 o (f2 o f1)
 END function_props2


% relation_defs defines operators on relations between possibly different
% types.  Note that some of the names are overloaded with those given in
% functions - in practice this should not cause any problems.

relation_defs [T1, T2: TYPE]: THEORY
 BEGIN
  R, S: VAR pred[[T1, T2]]
  x: VAR T1
  y: VAR T2
  X: VAR set[T1]
  Y: VAR set[T2]

  domain?(R)(x: T1): bool = EXISTS (y: T2): R(x, y)

  range?(R)(y: T2): bool = EXISTS (x: T1): R(x, y)

  domain(R): TYPE = {x: T1 | EXISTS (y: T2): R(x, y)}

  range(R): TYPE = {y: T2 | EXISTS (x: T1): R(x, y)}

  rinverse(R)(y, x): bool = R(x, y)

  rcomplement(R)(x, y): bool = NOT R(x, y)

  runion(R, S)(x, y): bool = R(x, y) OR S(x, y)

  rintersection(R, S)(x, y): bool = R(x, y) AND S(x, y)

  image(R, X): set[T2] = {y: T2 | EXISTS (x: (X)): R(x, y)}

  image(R)(X): set[T2] = image(R, X)

  preimage(R, Y): set[T1] = {x: T1 | EXISTS (y: (Y)): R(x, y)}

  preimage(R)(Y): set[T1] = preimage(R, Y)

  postcondition(R, X): set[T2] = {y: T2 | EXISTS (x: (X)): R(x, y)}

  postcondition(R)(X): set[T2] = postcondition(R, X)

  precondition(R, Y): set[T1] = {x: T1 | FORALL (y: T2 | R(x, y)): Y(y)}

  precondition(R)(Y): set[T1] = precondition(R, Y)

  converse(R): pred[[T2, T1]] = (LAMBDA (y: T2), (x: T1): R(x, y))

  isomorphism?(R): bool =
    (EXISTS (f: (bijective?[T1, T2])): R = graph(f))

  total?(R): bool = FORALL (x: T1): EXISTS (y: T2): R(x, y)

  onto?(R): bool = FORALL (y: T2): EXISTS (x: T1): R(x, y)

 END relation_defs


% relation_props

relation_props [T1, T2, T3: TYPE]: THEORY
 BEGIN
  R1: VAR pred[[T1, T2]]
  R2: VAR pred[[T2, T3]]
  x: VAR T1
  y: VAR T2
  z: VAR T3

  o(R1, R2)(x, z): bool = EXISTS y: R1(x, y) AND R2(y, z)

  total_composition: LEMMA total?(R1) & total?(R2) => total?(R1 o R2)

  onto_composition: LEMMA onto?(R1) & onto?(R2) => onto?(R1 o R2)

  composition_total: JUDGEMENT
    o(R1: (total?[T1, T2]), R2: (total?[T2, T3])) HAS_TYPE (total?[T1, T3])

  composition_onto: JUDGEMENT
    o(R1: (onto?[T1, T2]), R2: (onto?[T2, T3])) HAS_TYPE (onto?[T1, T3])

 END relation_props


relation_props2 [T1, T2, T3, T4: TYPE]: THEORY
 BEGIN
  R1: VAR pred[[T1, T2]]
  R2: VAR pred[[T2, T3]]
  R3: VAR pred[[T3, T4]]

  assoc: LEMMA (R1 o R2) o R3 = R1 o (R2 o R3)
 END relation_props2


%-------------------------------------------------------------------------
%
%  Properties of converses of relations on a single type.
%
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%-------------------------------------------------------------------------
relation_converse_props[T: TYPE]: THEORY
 BEGIN

  reflexive_converse: JUDGEMENT
    converse(R: (reflexive?[T])) HAS_TYPE (reflexive?[T])

  irreflexive_converse: JUDGEMENT
    converse(R: (irreflexive?[T])) HAS_TYPE (irreflexive?[T])

  symmetric_converse: JUDGEMENT
    converse(R: (symmetric?[T])) HAS_TYPE (symmetric?[T])

  antisymmetric_converse: JUDGEMENT
    converse(R: (antisymmetric?[T])) HAS_TYPE (antisymmetric?[T])

  connected_converse: JUDGEMENT
    converse(R: (connected?[T])) HAS_TYPE (connected?[T])

  transitive_converse: JUDGEMENT
    converse(R: (transitive?[T])) HAS_TYPE (transitive?[T])

  equivalence_converse: JUDGEMENT
    converse(R: (equivalence?[T])) HAS_TYPE (equivalence?[T])

  preorder_converse: JUDGEMENT
    converse(R: (preorder?[T])) HAS_TYPE (preorder?[T])

  partial_order_converse: JUDGEMENT
    converse(R: (partial_order?[T])) HAS_TYPE (partial_order?[T])

  strict_order_converse: JUDGEMENT
    converse(R: (strict_order?[T])) HAS_TYPE (strict_order?[T])

  dichotomous_converse: JUDGEMENT
    converse(R: (dichotomous?[T])) HAS_TYPE (dichotomous?[T])

  total_order_converse: JUDGEMENT
    converse(R: (total_order?[T])) HAS_TYPE (total_order?[T])

  trichotomous_converse: JUDGEMENT
    converse(R: (trichotomous?[T])) HAS_TYPE (trichotomous?[T])

  strict_total_order_converse: JUDGEMENT
    converse(R: (strict_total_order?[T])) HAS_TYPE (strict_total_order?[T])

 END relation_converse_props


indexed_sets[index, T: TYPE]: THEORY
 BEGIN
  i: VAR index
  x: VAR T
  A, B: VAR [index -> set[T]]
  S: VAR set[T]

  IUnion(A): set[T] = {x | EXISTS i: A(i)(x)}

  IIntersection(A): set[T] = {x | FORALL i: A(i)(x)}

  IUnion_Union: LEMMA
    IUnion(A) = Union(image(A)(fullset[index]))

  IIntersection_Intersection: LEMMA
    IIntersection(A) = Intersection(image(A)(fullset[index]))

  IUnion_union: LEMMA
    IUnion(LAMBDA i: union(A(i), B(i))) = union(IUnion(A), IUnion(B))

  IIntersection_intersection: LEMMA
    IIntersection(LAMBDA i: intersection(A(i), B(i)))
        = intersection(IIntersection(A), IIntersection(B))

  IUnion_intersection: LEMMA
    IUnion(LAMBDA i: intersection(A(i), S))
        = intersection(IUnion(A), S)

  IIntersection_union: LEMMA
    IIntersection(LAMBDA i: union(A(i), S))
        = union(IIntersection(A), S)
 END indexed_sets


% operator_defs

operator_defs[T: TYPE]: THEORY
 BEGIN
  o, *: VAR [T, T -> T]
  -: VAR [T -> T]
  x, y, z: VAR T

  commutative?(o):     bool = (FORALL x, y: x o y = y o x)

  associative?(o):     bool = (FORALL x, y, z: (x o y) o z = x o (y o z))

  left_identity?(o)(y): bool = (FORALL x: y o x = x)

  right_identity?(o)(y): bool = (FORALL x: x o y = x)

  identity?(o)(y):     bool = (FORALL x: x o y = x AND y o x = x)

  has_identity?(o):    bool = (EXISTS y: identity?(o)(y))

  zero?(o)(y):         bool = (FORALL x: x o y = y AND y o x = y)

  has_zero?(o):        bool = (EXISTS y: zero?(o)(y))

  inverses?(o)(-)(y):  bool = (FORALL x: x o -x = y AND (-x) o x = y)

  has_inverses?(o):    bool = (EXISTS -, y: inverses?(o)(-)(y))

  distributive?(*, o): bool = (FORALL x, y, z: x * (y o z) = (x * y) o (x * z))

 END operator_defs


% numbers provides the number type, which is the highest numeric type.
% Its primary purpose is to provide a way to extend the reals, for
% example, the extended reals can be declared as a subtype of number that
% contains all the reals and the points at infinity.

numbers: THEORY
 BEGIN

  number: NONEMPTY_TYPE

 END numbers


% number-fields provides the field axioms.  This allows development of,
% for example, complex numbers or nonstandard reals as subtypes, without
% having to extend the field operators.  Extended reals are not a subtype
% of number_field, as division by zero is allowed in the extended reals.
% Note that order relations are not defined here.

number_fields: THEORY
 BEGIN
  number_field: NONEMPTY_TYPE FROM number
  numfield: NONEMPTY_TYPE = number_field
  number_field?(n: number): bool = number_field_pred(n)

  % The following declarations, if they could be expanded, are built in to
  %  the typechecker and prover:
  % 0, 1, 2, ... : number_field
  % AXIOM 0 /= 1 AND 0 /= 2 AND 1 /= 2 AND ...

  nonzero_number: NONEMPTY_TYPE = {r: number_field | r /= 0} CONTAINING 1
  nznum: NONEMPTY_TYPE = nonzero_number

  +, -, *: [numfield, numfield -> numfield]
  /: [numfield, nznum -> numfield]
  -: [numfield -> numfield]

  % Field Axioms - these are not provable using the decision
  % procedures, as the operators are translated to uninterpreted
  % functions, so that x * x = -1 is consistent.  When the
  % arguments are (a subtype of) real, then the translation is to
  % interpreted symbols.

  x, y, z: VAR numfield
  n0x: VAR nznum

  commutative_add : POSTULATE x + y = y + x

  associative_add : POSTULATE x + (y + z) = (x + y) + z

  identity_add    : POSTULATE x + 0 = x

  inverse_add     : AXIOM x + -x = 0

  minus_add       : AXIOM x - y = x + -y

  commutative_mult: AXIOM x * y = y * x

  associative_mult: AXIOM x * (y * z) =  (x * y) * z

  identity_mult   : AXIOM 1 * x = x

  inverse_mult    : AXIOM n0x * (1/n0x) = 1

  div_def         : AXIOM y/n0x = y * (1/n0x)

  distributive    : POSTULATE x * (y + z) = (x * y) + (x * z)

 END number_fields
  

% reals defines the real numbers as an uninterpreted subtype of number.
% Though not explicitly specified, all numeric constants are known to be
% of type real (hence number). Note that / is defined only when the second
% argument is nonzero.  This theory should not generally be used in
% auto-rewrite, since the inequalities are already known to the decision
% procedures, and tend to get rewritten to disjunctions, and leads to
% unnecessary case splits.

reals: THEORY
 BEGIN

  real: NONEMPTY_TYPE FROM number_field

  real?(n:number): bool = number_field_pred(n) AND real_pred(n)

  % The following declarations, if they could be expanded, are built in to
  %  the typechecker:
  % AXIOM real_pred(0) AND real_pred(1) AND real_pred(2) AND ...
  % JUDGEMENT 0, 1, 2, ... HAS_TYPE real

  nonzero_real: NONEMPTY_TYPE = {r: real | r /= 0} CONTAINING 1
  nzreal: NONEMPTY_TYPE = nonzero_real
  % nzreal_is_nznum: JUDGEMENT nonzero_real SUBTYPE_OF nonzero_number

  x, y: VAR real
  n0z: VAR nzreal

  closed_plus:    AXIOM real_pred(x + y)
  closed_minus:   AXIOM real_pred(x - y)
  closed_times:   AXIOM real_pred(x * y)
  closed_divides: AXIOM real_pred(x / n0z)
  closed_neg:     AXIOM real_pred(-x)

  real_plus_real_is_real:  JUDGEMENT +(x,y) HAS_TYPE real
  real_minus_real_is_real: JUDGEMENT -(x,y) HAS_TYPE real
  real_times_real_is_real: JUDGEMENT *(x,y) HAS_TYPE real
  real_div_nzreal_is_real: JUDGEMENT /(x,n0z) HAS_TYPE real

  minus_real_is_real: JUDGEMENT -(x) HAS_TYPE real

  <(x, y):  bool
  <=(x, y): bool = x < y OR x = y;
  >(x, y):  bool = y < x;
  >=(x, y): bool = y <= x

  reals_totally_ordered: POSTULATE strict_total_order?(<)

  % Built in:
  % AXIOM 0 < 1 AND 1 < 2 AND ...

 END reals


% real_axioms provides the usual commutativity, associativity, etc.
% axioms about the real numbers.  Note that many of these properties
% also hold for the rationals, integers, and natural numbers.  These
% properties are all known to the decision procedures of PVS, so should
% rarely need to be cited.  These axioms were taken from
% Royden's "Real Analysis" pp.29-31

real_axioms: THEORY
 BEGIN
  x, y, z: VAR real
  n0x: VAR nzreal

  % Field Axioms are now in number_fields

  % Order Axioms

  posreal_add_closed : POSTULATE x > 0 AND y > 0 IMPLIES x + y > 0

  posreal_mult_closed: AXIOM x > 0 AND y > 0 IMPLIES x * y > 0

  posreal_neg        : POSTULATE x > 0 IMPLIES NOT -x > 0

  trichotomy         : POSTULATE x > 0 OR x = 0 OR 0 > x


  % Completeness Axiom defined in bounded_reals

 END real_axioms


bounded_real_defs: THEORY
BEGIN

  x, y: VAR real

  % Completeness Axiom

  S: VAR (nonempty?[real])

  upper_bound?(x, S): bool = FORALL (s: (S)): s <= x

  upper_bound?(S)(x): bool = upper_bound?(x, S)

  lower_bound?(x, S): bool = FORALL (s: (S)): x <= s

  lower_bound?(S)(x): bool = lower_bound?(x, S)

  least_upper_bound?(x, S): bool =
    upper_bound?(x, S) AND
      FORALL y: upper_bound?(y, S) IMPLIES (x <= y)

  least_upper_bound?(S)(x): bool = least_upper_bound?(x, S)

  greatest_lower_bound?(x, S): bool =
    lower_bound?(x, S) AND
      FORALL y: lower_bound?(y, S) IMPLIES (y <= x)

  greatest_lower_bound?(S)(x): bool = greatest_lower_bound?(x, S)

  real_complete: AXIOM
    FORALL S:
      (EXISTS y: upper_bound?(y, S)) IMPLIES
        (EXISTS y: least_upper_bound?(y, S))

  real_lower_complete: LEMMA
    FORALL S:
      (EXISTS y: lower_bound?(y, S)) IMPLIES 
        (EXISTS x: greatest_lower_bound?(x, S))


  % lub and glb

  bounded_above?(S): bool = (EXISTS x: upper_bound?(x, S))

  bounded_below?(S): bool = (EXISTS x: lower_bound?(x, S))

  bounded?(S): bool = bounded_above?(S) AND bounded_below?(S)

  bounded_set: TYPE = (bounded?)

  SA: VAR (bounded_above?)

  lub_exists: LEMMA (EXISTS x: least_upper_bound?(x, SA))

  lub(SA): {x | least_upper_bound?(x, SA)}

  lub_lem: LEMMA lub(SA) = x IFF least_upper_bound?(x, SA)

  SB: VAR (bounded_below?)

  glb_exists: LEMMA (EXISTS x: greatest_lower_bound?(x, SB))

  glb(SB): {x | greatest_lower_bound?(x, SB)}

  glb_lem: LEMMA glb(SB) = x IFF greatest_lower_bound?(x, SB)

END bounded_real_defs


bounded_real_defs_alt [S: (nonempty?[real])]: THEORY
 BEGIN
  x: VAR real
  
  upper_bound?: [real -> bool] = upper_bound?(S)
  lower_bound?: [real -> bool] = lower_bound?(S)
  least_upper_bound?: [real -> bool] = least_upper_bound?(S)
  greatest_lower_bound?: [real -> bool] = greatest_lower_bound?(S)

  lub_is_upper_bound: JUDGEMENT
    (least_upper_bound?) SUBTYPE_OF (upper_bound?)

  glb_is_lower_bound: JUDGEMENT
    (greatest_lower_bound?) SUBTYPE_OF (lower_bound?)
    
 END bounded_real_defs_alt


% reals_types declares some useful subtypes of the reals and some
% associated judgements.

real_types: THEORY
 BEGIN
  x: VAR real

  nonneg_real: NONEMPTY_TYPE = {x: real        | x >= 0} CONTAINING 0
  nonpos_real: NONEMPTY_TYPE = {x: real        | x <= 0} CONTAINING 0
  posreal:     NONEMPTY_TYPE = {x: nonneg_real | x > 0}  CONTAINING 1
  negreal:     NONEMPTY_TYPE = {x: nonpos_real | x < 0}  CONTAINING -1
  nnreal: TYPE = nonneg_real
  npreal: TYPE = nonpos_real

  posreal_is_nzreal: JUDGEMENT posreal SUBTYPE_OF nzreal
  negreal_is_nzreal: JUDGEMENT negreal SUBTYPE_OF nzreal

  nzx, nzy: VAR nzreal
  px, py:   VAR posreal
  nx, ny:   VAR negreal
  nnx, nny: VAR nonneg_real
  npx, npy: VAR nonpos_real

  nonneg_real_add_closed: LEMMA nnx + nny >= 0
  nonpos_real_add_closed: LEMMA npx + npy <= 0
  negreal_add_closed    : LEMMA nx + ny < 0

  nonneg_real_mult_closed: LEMMA nnx * nny >= 0

  nzreal_times_nzreal_is_nzreal: JUDGEMENT *(nzx, nzy) HAS_TYPE nzreal
  nzreal_div_nzreal_is_nzreal:   JUDGEMENT /(nzx, nzy) HAS_TYPE nzreal
  minus_nzreal_is_nzreal:        JUDGEMENT -(nzx)      HAS_TYPE nzreal

  nnreal_plus_nnreal_is_nnreal:  JUDGEMENT +(nnx, nny) HAS_TYPE nnreal
  nnreal_times_nnreal_is_nnreal: JUDGEMENT *(nnx, nny) HAS_TYPE nnreal
  nnreal_div_posreal_is_nnreal:  JUDGEMENT /(nnx, py)  HAS_TYPE nnreal
  nnreal_div_negreal_is_npreal:  JUDGEMENT /(nnx, ny)  HAS_TYPE npreal

  npreal_plus_npreal_is_npreal:  JUDGEMENT +(npx, npy) HAS_TYPE npreal
  npreal_times_npreal_is_nnreal: JUDGEMENT *(npx, npy) HAS_TYPE nnreal
  npreal_div_posreal_is_npreal:  JUDGEMENT /(npx, py)  HAS_TYPE npreal
  npreal_div_negreal_is_nnreal:  JUDGEMENT /(npx, ny)  HAS_TYPE nnreal

  posreal_plus_nnreal_is_posreal:   JUDGEMENT +(px, nny) HAS_TYPE posreal
  nnreal_plus_posreal_is_posreal:   JUDGEMENT +(nnx, py) HAS_TYPE posreal
  posreal_times_posreal_is_posreal: JUDGEMENT *(px, py) HAS_TYPE posreal
  posreal_div_posreal_is_posreal:   JUDGEMENT /(px, py) HAS_TYPE posreal

  negreal_plus_negreal_is_negreal:  JUDGEMENT +(nx, ny) HAS_TYPE negreal
  negreal_times_negreal_is_posreal: JUDGEMENT *(nx, ny) HAS_TYPE posreal
  negreal_div_negreal_is_posreal:   JUDGEMENT /(nx, ny) HAS_TYPE posreal

 END real_types


% rationals defines the rational numbers as an uninterpreted subtype of real.
% The basic number operations are redeclared in order to specify that
% they are closed, e.g. the sum of two rationals is a rational.

rationals: THEORY
 BEGIN

  rational: NONEMPTY_TYPE FROM real
  rat: NONEMPTY_TYPE = rational

  rational?(n: number): bool =
    number_field_pred(n) AND real_pred(n) AND rational_pred(n)

  % The following declarations, if they could be expanded, are built in to
  %  the typechecker:
  % AXIOM rational_pred(0) AND rational_pred(1) AND rational_pred(2) AND ...
  % JUDGEMENT 0, 1, 2, ... HAS_TYPE rational

  nonzero_rational: NONEMPTY_TYPE = {r: rational | r /= 0} CONTAINING 1
  nzrat: NONEMPTY_TYPE = nonzero_rational
  % nzrat_is_nzreal: JUDGEMENT nonzero_rational SUBTYPE_OF nonzero_real

  x, y: VAR rat
  n0z: VAR nzrat

  closed_plus:    AXIOM rational_pred(x + y)
  closed_minus:   AXIOM rational_pred(x - y)
  closed_times:   AXIOM rational_pred(x * y)
  closed_divides: AXIOM rational_pred(x / n0z)
  closed_neg:     AXIOM rational_pred(-x)

  rat_plus_rat_is_rat:  JUDGEMENT +(x,y) HAS_TYPE rat
  rat_minus_rat_is_rat: JUDGEMENT -(x,y) HAS_TYPE rat
  rat_times_rat_is_rat: JUDGEMENT *(x,y) HAS_TYPE rat
  rat_div_nzrat_is_rat: JUDGEMENT /(x,n0z) HAS_TYPE rat

  minus_rat_is_rat: JUDGEMENT -(x) HAS_TYPE rat

  nonneg_rat: NONEMPTY_TYPE = {r: rational   | r >= 0} CONTAINING 0
  nonpos_rat: NONEMPTY_TYPE = {r: rational   | r <= 0} CONTAINING 0
  posrat:     NONEMPTY_TYPE = {r: nonneg_rat | r > 0}  CONTAINING 1
  negrat:     NONEMPTY_TYPE = {r: nonpos_rat | r < 0}  CONTAINING -1
  nnrat: NONEMPTY_TYPE = nonneg_rat
  nprat: NONEMPTY_TYPE = nonpos_rat

  nnx, nny: VAR nonneg_rat
  npx, npy: VAR nonpos_rat
  px, py: VAR posrat
  nx, ny: VAR negrat
  n0x, n0y: VAR nzrat

  % nnrat_is_nnreal:   JUDGEMENT nonneg_rat SUBTYPE_OF nonneg_real
  % nprat_is_npreal:   JUDGEMENT nonpos_rat SUBTYPE_OF nonpos_real
  % posrat_is_posreal: JUDGEMENT posrat     SUBTYPE_OF posreal
  % negrat_is_negreal: JUDGEMENT negrat     SUBTYPE_OF negreal
  posrat_is_nzrat:   JUDGEMENT posrat     SUBTYPE_OF nzrat
  negrat_is_nzrat:   JUDGEMENT negrat     SUBTYPE_OF nzrat

  nzrat_times_nzrat_is_nzrat: JUDGEMENT *(n0x, n0y) HAS_TYPE nzrat
  nzrat_div_nzrat_is_nzrat:   JUDGEMENT /(n0x, n0y) HAS_TYPE nzrat
  minus_nzrat_is_nzrat:       JUDGEMENT -(n0x)      HAS_TYPE nzrat

  nnrat_plus_nnrat_is_nnrat:  JUDGEMENT +(nnx, nny) HAS_TYPE nonneg_rat
  nnrat_times_nnrat_is_nnrat: JUDGEMENT *(nnx, nny) HAS_TYPE nonneg_rat
  nnrat_div_posrat_is_nnrat:  JUDGEMENT /(nnx, py)  HAS_TYPE nonneg_rat
  nnrrat_div_negrat_is_nprat: JUDGEMENT /(nnx, ny)  HAS_TYPE nprat

  nprat_plus_nprat_is_nprat:  JUDGEMENT +(npx, npy) HAS_TYPE nprat
  nprat_times_nprat_is_nnrat: JUDGEMENT *(npx, npy) HAS_TYPE nnrat
  nprat_div_posrat_is_nprat:  JUDGEMENT /(npx, py)  HAS_TYPE nprat
  nprat_div_negrat_is_nnrat:  JUDGEMENT /(npx, ny)  HAS_TYPE nnrat

  posrat_plus_nnrat_is_posrat:   JUDGEMENT +(px, nny) HAS_TYPE posrat
  nnrat_plus_posrat_is_posrat:   JUDGEMENT +(nnx, py) HAS_TYPE posrat
  posrat_times_posrat_is_posrat: JUDGEMENT *(px, py)  HAS_TYPE posrat
  posrat_div_posrat_is_posrat:   JUDGEMENT /(px, py)  HAS_TYPE posrat

  negrat_plus_negrat_is_negrat:  JUDGEMENT +(nx, ny) HAS_TYPE negrat
  negrat_times_negrat_is_posrat: JUDGEMENT *(nx, ny) HAS_TYPE posrat
  negrat_div_negrat_is_posrat:   JUDGEMENT /(nx, ny) HAS_TYPE posrat

 END rationals


% integers defines the integers as an uninterpreted subtype of rational.
% The basic number operations are redeclared in order to specify that
% they are closed, e.g. the sum of two integers is an integer.

integers: THEORY
 BEGIN

  integer: NONEMPTY_TYPE FROM rational
  int: NONEMPTY_TYPE = integer

  integer?(n:number): bool =
    number_field_pred(n) AND real_pred(n)
      AND rational_pred(n) AND integer_pred(n)

  % The following declarations, if they could be expanded, are built in to
  %  the typechecker:
  % AXIOM integer_pred(0) AND integer_pred(1) AND integer_pred(2) AND ...
  % JUDGEMENT 0, 1, 2, ... HAS_TYPE integer

  nonzero_integer: NONEMPTY_TYPE = {i: int | i /= 0} CONTAINING 1
  nzint: NONEMPTY_TYPE = nonzero_integer
  % nzint_is_nzrat: JUDGEMENT nonzero_integer SUBTYPE_OF nonzero_rational

  i, j: VAR int
  n0i, n0j: VAR nzint

  closed_plus:  AXIOM integer_pred(i + j)
  closed_minus: AXIOM integer_pred(i - j)
  closed_times: AXIOM integer_pred(i * j)
  closed_neg:   AXIOM integer_pred(-i)

  upfrom(i): NONEMPTY_TYPE = {s: int | s >= i} CONTAINING i
  above(i):  NONEMPTY_TYPE = {s: int | s > i} CONTAINING i + 1

  int_plus_int_is_int:  JUDGEMENT +(i,j) HAS_TYPE int
  int_minus_int_is_int: JUDGEMENT -(i,j) HAS_TYPE int
  int_times_int_is_int: JUDGEMENT *(i,j) HAS_TYPE int

  minus_int_is_int: JUDGEMENT -(i) HAS_TYPE int
  minus_nzint_is_nzint: JUDGEMENT -(n0i) HAS_TYPE nzint
 
  nonneg_int: NONEMPTY_TYPE = {i: int        | i >= 0} CONTAINING 0
  nonpos_int: NONEMPTY_TYPE = {i: int        | i <= 0} CONTAINING 0
  posint:     NONEMPTY_TYPE = {i: nonneg_int | i > 0}  CONTAINING 1
  negint:     NONEMPTY_TYPE = {i: nonpos_int | i < 0}  CONTAINING -1

  posnat: NONEMPTY_TYPE = posint

  nni, nnj: VAR nonneg_int
  npi, npj: VAR nonpos_int
  pi, pj: VAR posint
  ni, nj: VAR negint

  % Built in:
  % JUDGEMENT 1, 2, 3, ... HAS_TYPE posint

  % nnint_is_nnrat:   JUDGEMENT nonneg_int SUBTYPE_OF nonneg_rat
  % npint_is_nprat:   JUDGEMENT nonpos_int SUBTYPE_OF nonpos_rat
  % posint_is_posrat: JUDGEMENT posint     SUBTYPE_OF posrat
  % negint_is_negrat: JUDGEMENT negint     SUBTYPE_OF negrat
  posint_is_nzint:  JUDGEMENT posint     SUBTYPE_OF nzint
  negint_is_nzint:  JUDGEMENT negint     SUBTYPE_OF nzint

  nzint_times_nzint_is_nzint:    JUDGEMENT *(n0i, n0j) HAS_TYPE nzint
  
  nnint_plus_nnint_is_nnint:	 JUDGEMENT +(nni, nnj) HAS_TYPE nonneg_int
  nnint_times_nnint_is_nnint:    JUDGEMENT *(nni, nnj) HAS_TYPE nonneg_int
  
  npint_plus_npint_is_npint:	 JUDGEMENT +(npi, npj) HAS_TYPE nonpos_int
  npint_times_npint_is_nnint:    JUDGEMENT *(npi, npj) HAS_TYPE nonneg_int
  
  posint_plus_nnint_is_posint:   JUDGEMENT +(pi, nnj)  HAS_TYPE posint
  nnint_plus_posint_is_posint:   JUDGEMENT +(nni, pj)  HAS_TYPE posint
  posint_times_posint_is_posint: JUDGEMENT *(pi, pj)   HAS_TYPE posint
  
  negint_plus_negint_is_negint:  JUDGEMENT +(ni, nj)   HAS_TYPE negint
  negint_times_negint_is_posint: JUDGEMENT *(ni, nj)   HAS_TYPE posint

  % Note: subrange may be an empty type
  subrange(i, j): TYPE = {k: int | i <= k AND k <= j}

  even?(i): bool = EXISTS j: i = j * 2
  odd?(i): bool  = EXISTS j: i = j * 2 + 1

  even_int: NONEMPTY_TYPE = (even?) CONTAINING 0
  odd_int:  NONEMPTY_TYPE = (odd?)  CONTAINING 1

  % The following declarations, if they could be expanded, are built in to
  %  the typechecker:
  % JUDGEMENT 0, 2, 4, ... HAS_TYPE even_int
  % JUDGEMENT 1, 3, 5, ... HAS_TYPE odd_int
  
  e1, e2: VAR even_int
  o1, o2: VAR odd_int

  odd_is_nzint: JUDGEMENT odd_int SUBTYPE_OF nzint

  even_plus_even_is_even:  JUDGEMENT +(e1,e2) HAS_TYPE even_int
  even_minus_even_is_even: JUDGEMENT -(e1,e2) HAS_TYPE even_int
  odd_plus_odd_is_even:    JUDGEMENT +(o1,o2) HAS_TYPE even_int
  odd_minus_odd_is_even:   JUDGEMENT -(o1,o2) HAS_TYPE even_int
  odd_plus_even_is_odd:	   JUDGEMENT +(o1,e2) HAS_TYPE odd_int
  odd_minus_even_is_odd:   JUDGEMENT -(o1,e2) HAS_TYPE odd_int
  even_plus_odd_is_odd:	   JUDGEMENT +(e1,o2) HAS_TYPE odd_int
  even_minus_odd_is_odd:   JUDGEMENT -(e1,o2) HAS_TYPE odd_int
  even_times_int_is_even:  JUDGEMENT *(e1,i)  HAS_TYPE even_int
  int_times_even_is_even:  JUDGEMENT *(i,e2)  HAS_TYPE even_int
  odd_times_odd_is_odd:	   JUDGEMENT *(o1,o2) HAS_TYPE odd_int
  minus_even_is_even:	   JUDGEMENT -(e1)    HAS_TYPE even_int
  minus_odd_is_odd:	   JUDGEMENT -(o1)    HAS_TYPE odd_int

 END integers


% naturalnumbers defines the natural numbers as a subtype of integer.
% The sum and product operations are redeclared in order to specify that
% they are closed, e.g. the sum of two natural numbers is a natural
% number.  The successor and predecessor functions are defined here.

naturalnumbers: THEORY
 BEGIN

  naturalnumber: TYPE = nonneg_int
  nat: NONEMPTY_TYPE = naturalnumber

  % The following declaration, if it could be expanded, is built in to
  %  the typechecker:
  % JUDGEMENT 0, 1, 2, ... HAS_TYPE naturalnumber

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

  upfrom_nat_is_nat:   JUDGEMENT upfrom(i) SUBTYPE_OF nat
  upfrom_posnat_is_posnat: JUDGEMENT upfrom(n) SUBTYPE_OF posnat
  above_nat_is_posnat: JUDGEMENT above(i) SUBTYPE_OF posnat
  subrange_nat_is_nat: JUDGEMENT subrange(i,j) SUBTYPE_OF nat
  subrange_posnat_is_posnat: JUDGEMENT subrange(n,j) SUBTYPE_OF posnat

  upto(i):   NONEMPTY_TYPE = {s: nat | s <= i} CONTAINING i
  below(i):  TYPE = {s: nat | s < i}  % may be empty

%  nat_plus_nat_is_nat: JUDGEMENT +(i,j) HAS_TYPE nat
%  nat_times_nat_is_nat: JUDGEMENT *(i,j) HAS_TYPE nat
  
  succ(i): nat = i + 1

  pred(i): nat = IF i > 0 THEN i - 1 ELSE 0 ENDIF;

  ~(i, j): nat = IF i > j THEN i - j ELSE 0 ENDIF

  wf_nat: AXIOM well_founded?(LAMBDA i, j: i < j)

  p: VAR pred[nat]

  nat_induction: LEMMA
    (p(0) AND (FORALL j: p(j) IMPLIES p(j+1)))
        IMPLIES (FORALL i: p(i))

  % Strong induction on naturals.

  NAT_induction: LEMMA 
    (FORALL j: (FORALL k: k < j IMPLIES p(k)) IMPLIES p(j))
       IMPLIES (FORALL i: p(i))

  % This seems out of place - it is here so we can prove it by induction
  x: VAR int
  even_or_odd: THEOREM even?(x) IFF NOT odd?(x)

  odd_iff_not_even:  LEMMA odd?(x)  IFF NOT even?(x)
  even_iff_not_odd:  LEMMA even?(x) IFF NOT odd?(x)
  odd_or_even_int:   LEMMA odd?(x)  OR even?(x)
  odd_iff_even_succ: LEMMA odd?(x)  IFF even?(x+1)
  even_iff_odd_succ: LEMMA even?(x) IFF odd?(x+1)

  even_plus1:        LEMMA even?(x) IFF NOT even?(x+1)
  odd_plus1:         LEMMA odd?(x) IFF NOT odd?(x+1)

  even_div2:         LEMMA even?(x) IMPLIES integer_pred(x/2)
  odd_div2:          LEMMA odd?(x)  IMPLIES integer_pred((x-1)/2)

 END naturalnumbers


min_nat[T: TYPE FROM nat]: THEORY
 BEGIN
  S: VAR (nonempty?[T])
  a, x: VAR T

  min(S): {a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}

  minimum?(a, S) : bool = S(a) AND (FORALL x: S(x) IMPLIES a <= x)

  min_def : LEMMA 
     FORALL (S: (nonempty?[T])) : min(S) = a IFF minimum?(a, S)

 END min_nat


% real_defs defines some useful real functions and
% provides all the judgements for the subtypes nzreal, nonneg_real,
% posreal, rat, nzrat, nonneg_rat, posrat, int, nzint, nat, and posint.
% For abs, we don't declare all these possibilities, since abs is the
% identity on the nonneg and pos number types.  Note that for abs, max,
% and min the range type is dependent on the domain, providing information
% in the type that is usually provided through separate lemmas.

real_defs: THEORY
 BEGIN
  m, n: VAR real

  sgn(m): int = IF m >= 0 THEN 1 ELSE -1 ENDIF

  abs(m): {n: nonneg_real | n >= m AND n >= -m}
    = IF m < 0 THEN -m ELSE m ENDIF

  nonzero_abs_is_pos: JUDGEMENT abs(x:nzreal) HAS_TYPE {y: posreal | y >= x}
  rat_abs_is_nonneg: JUDGEMENT abs(q:rat) HAS_TYPE {r: nonneg_rat | r >= q}
  nzrat_abs_is_pos: JUDGEMENT abs(q:nzrat) HAS_TYPE {r: posrat | r >= q}
  int_abs_is_nonneg: JUDGEMENT abs(i:int) HAS_TYPE {j: nonneg_int | j >= i}
  nzint_abs_is_pos: JUDGEMENT abs(i:nzint) HAS_TYPE {j: posint | j >= i}

  max(m, n): {p: real | p >= m AND p >= n}
    = IF m < n THEN n ELSE m ENDIF

  min(m, n): {p: real | p <= m AND p <= n}
    = IF m > n THEN n ELSE m ENDIF

  % real subtype judgements

  nzreal_max: JUDGEMENT
    max(x,y:nzreal) HAS_TYPE {z: nzreal | z >= x AND z >= y}
  nzreal_min: JUDGEMENT
    min(x,y:nzreal) HAS_TYPE {z: nzreal | z <= x AND z <= y}

  nonneg_real_max: JUDGEMENT
    max(x,y:nonneg_real) HAS_TYPE {z: nonneg_real | z >= x AND z >= y}
  nonneg_real_min: JUDGEMENT
    min(x,y:nonneg_real) HAS_TYPE {z: nonneg_real | z <= x AND z <= y}

  posreal_max: JUDGEMENT
    max(x,y:posreal) HAS_TYPE {z: posreal | z >= x AND z >= y}
  posreal_min: JUDGEMENT
    min(x,y:posreal) HAS_TYPE {z: posreal | z <= x AND z <= y}

  % rat subtype judgements

  rat_max: JUDGEMENT
    max(q,r:rat) HAS_TYPE {s: rat | s >= q AND s >= r}
  rat_min: JUDGEMENT
    min(q,r:rat) HAS_TYPE {s: rat | s <= q AND s <= r}

  nzrat_max: JUDGEMENT
    max(q,r:nzrat) HAS_TYPE {s: nzrat | s >= q AND s >= r}
  nzrat_min: JUDGEMENT
    min(q,r:nzrat) HAS_TYPE {s: nzrat | s <= q AND s <= r}

  nonneg_rat_max: JUDGEMENT
    max(q,r:nonneg_rat) HAS_TYPE {s: nonneg_rat | s >= q AND s >= r}
  nonneg_rat_min: JUDGEMENT
    min(q,r:nonneg_rat) HAS_TYPE {s: nonneg_rat | s <= q AND s <= r}

  posrat_max: JUDGEMENT
    max(q,r:posrat) HAS_TYPE {s: posrat | s >= q AND s >= r}
  posrat_min: JUDGEMENT
    min(q,r:posrat) HAS_TYPE {s: posrat | s <= q AND s <= r}

  % int subtype judgements

  int_max: JUDGEMENT
    max(i,j:int) HAS_TYPE {k: int | i <= k AND j <= k}
  int_min: JUDGEMENT
    min(i,j:int) HAS_TYPE {k: int | k <= i AND k <= j}

  nzint_max: JUDGEMENT
    max(i,j:nzint) HAS_TYPE {k: nzint | i <= k AND j <= k}
  nzint_min: JUDGEMENT
    min(i,j:nzint) HAS_TYPE {k: nzint | k <= i AND k <= j}

  nat_max: JUDGEMENT
    max(i,j:nat) HAS_TYPE {k: nat | i <= k AND j <= k}
  nat_min: JUDGEMENT
    min(i,j:nat) HAS_TYPE {k: nat | k <= i AND k <= j}

  posint_max: JUDGEMENT
    max(i,j:posint) HAS_TYPE {k: posint | i <= k AND j <= k}
  posint_min: JUDGEMENT
    min(i,j:posint) HAS_TYPE {k: posint | k <= i AND k <= j}

  % Useful facts about maximum and minimum of two reals
  %
  % Author : Alfons Geser, National Institute of Aerospace
  % Date   : Aug 26, 2003
  a,b,c : VAR real

  min_le : LEMMA min(a,b) <= c IFF (a <= c OR b <= c)
  min_lt : LEMMA min(a,b) < c IFF (a < c OR b < c)
  min_ge : LEMMA min(a,b) >= c IFF (a >= c AND b >= c)
  min_gt : LEMMA min(a,b) > c IFF (a > c AND b > c)
  le_min : LEMMA a <= min(b,c) IFF (a <= b AND a <= c)
  lt_min : LEMMA a < min(b,c) IFF (a < b AND a < c)
  ge_min : LEMMA a >= min(b,c) IFF (a >= b OR a >= c)
  gt_min : LEMMA a > min(b,c) IFF (a > b OR a > c)

  max_le : LEMMA max(a,b) <= c IFF (a <= c AND b <= c)
  max_lt : LEMMA max(a,b) < c IFF (a < c AND b < c)
  max_ge : LEMMA max(a,b) >= c IFF (a >= c OR b >= c)
  max_gt : LEMMA max(a,b) > c IFF (a > c OR b > c)
  le_max : LEMMA a <= max(b,c) IFF (a <= b OR a <= c)
  lt_max : LEMMA a < max(b,c) IFF (a < b OR a < c)
  ge_max : LEMMA a >= max(b,c) IFF (a >= b AND a >= c)
  gt_max : LEMMA a > max(b,c) IFF (a > b AND a > c)

 END real_defs


% real_props contains useful properties about real numbers.  Most of
% these are known to the decision procedures of PVS, but there are some
% nonlinear ones that cannot be gotten automatically.  Nonlinear
% expressions are those that involve multiplication or division by two
% non-numeric terms.  Thus x*y and x/c are nonlinear, while 2001*x + 39*z is
% linear.  Note that it doesn't matter whether the terms are constants
% or variables, only whether they are actual numbers.

real_props: THEORY
 BEGIN
  w, x, y, z: VAR real
  n0w, n0x, n0y, n0z: VAR nonzero_real
  nnw, nnx, nny, nnz: VAR nonneg_real
  pw, px, py, pz: VAR posreal
  npw, npx, npy, npz: VAR nonpos_real
  nw, nx, ny, nz: VAR negreal

  inv_ne_0: LEMMA 1/n0x /= 0

  % Cancellation Laws for equality

  both_sides_plus1: LEMMA (x + z = y + z) IFF x = y

  both_sides_plus2: LEMMA (z + x = z + y) IFF x = y

  both_sides_minus1: LEMMA (x - z = y - z) IFF x = y

  both_sides_minus2: LEMMA (z - x = z - y) IFF x = y

  both_sides_times1: LEMMA (x * n0z = y * n0z) IFF x = y

  both_sides_times2: LEMMA (n0z * x = n0z * y) IFF x = y

  both_sides_div1: LEMMA (x/n0z = y/n0z) IFF x = y

  both_sides_div2: LEMMA (n0z/n0x = n0z/n0y) IFF n0x = n0y

  times_plus: LEMMA (x + y) * (z + w) = x*z + x*w + y*z + y*w

  times_div1: LEMMA x * (y/n0z) = (x * y)/n0z

  times_div2: LEMMA (x/n0z) * y = (x * y)/n0z

  div_times: LEMMA (x/n0x) * (y/n0y) = (x*y)/(n0x*n0y)

  div_eq_zero: LEMMA x/n0z = 0 IFF x = 0

  div_simp: LEMMA n0x/n0x = 1

  div_cancel1: LEMMA n0z * (x/n0z) = x

  div_cancel2: LEMMA (x/n0z) * n0z = x

  div_cancel3: LEMMA x/n0z = y IFF x = y * n0z

  div_cancel4: LEMMA x = y/n0z IFF x * n0z = y

  cross_mult: LEMMA (x/n0x = y/n0y) IFF (x * n0y = y * n0x)

  add_div: LEMMA (x/n0x) + (y/n0y) = (x * n0y + y * n0x)/(n0x * n0y)

  minus_div1: LEMMA (x/n0x) - (y/n0y) = (x * n0y - y * n0x)/(n0x * n0y)

  minus_div2: LEMMA (x/n0x - y/n0x) = (x - y)/n0x

  div_distributes: LEMMA (x/n0z) + (y/n0z) =  (x + y)/n0z

  div_distributes_minus: LEMMA (x/n0z) - (y/n0z) =  (x - y)/n0z

  div_div1: LEMMA (x / (n0y / n0z)) = ((x * n0z) / n0y)

  div_div2: LEMMA ((x / n0y) / n0z) = (x / (n0y * n0z))

  idem_add_is_zero: LEMMA x + x = x IMPLIES x = 0

  zero_times1: LEMMA 0 * x = 0

  zero_times2: LEMMA x * 0 = 0

  zero_times3: LEMMA x * y = 0 IFF x = 0 OR y = 0

  neg_times_neg: LEMMA (-x) * (-y) = x * y

  zero_is_neg_zero: LEMMA -0 = 0


  % Order lemmas for <

  strict_lt : LEMMA strict_total_order?(<)

  trich_lt: LEMMA x < y OR x = y OR y < x

  tri_unique_lt1: LEMMA x < y IMPLIES (x /= y AND NOT(y < x))

  tri_unique_lt2: LEMMA x = y IMPLIES (NOT(x < y) AND NOT(y < x))

  zero_not_lt_zero: LEMMA NOT 0 < 0

  neg_lt: LEMMA 0 < -x IFF x < 0

  pos_times_lt: LEMMA 0 < x * y IFF (0 < x AND 0 < y) OR (x < 0 AND y < 0)

  neg_times_lt: LEMMA x * y < 0 IFF (0 < x AND y < 0) OR (x < 0 AND 0 < y)

  quotient_pos_lt: FORMULA 0 < 1/n0x IFF 0 < n0x
  
  quotient_neg_lt: FORMULA 1/n0x < 0 IFF n0x < 0

  pos_div_lt: LEMMA 0 < x/n0y IFF (0 < x AND 0 < n0y) OR (x < 0 AND n0y < 0)

  neg_div_lt: LEMMA x/n0y < 0 IFF (0 < x AND n0y < 0) OR (x < 0 AND 0 < n0y)

  div_mult_pos_lt1: LEMMA z/py < x IFF z < x * py

  div_mult_pos_lt2: LEMMA x < z/py IFF x * py < z

  div_mult_neg_lt1: LEMMA z/ny < x IFF x * ny < z

  div_mult_neg_lt2: LEMMA x < z/ny IFF z < x * ny
  

  % Cancellation laws for <

  both_sides_plus_lt1: LEMMA x + z < y + z IFF x < y

  both_sides_plus_lt2: LEMMA z + x < z + y IFF x < y

  both_sides_minus_lt1: LEMMA x - z < y - z IFF x < y

  both_sides_minus_lt2: LEMMA z - x < z - y IFF y < x

  both_sides_times_pos_lt1: LEMMA x * pz < y * pz IFF x < y

  both_sides_times_pos_lt2: LEMMA pz * x < pz * y IFF x < y

  both_sides_times_neg_lt1: LEMMA x * nz < y * nz IFF y < x

  both_sides_times_neg_lt2: LEMMA nz * x < nz * y IFF y < x

  both_sides_div_pos_lt1: LEMMA x/pz < y/pz IFF x < y

  both_sides_div_pos_lt2: LEMMA pz/px < pz/py IFF py < px

  both_sides_div_pos_lt3: LEMMA nz/px < nz/py IFF px < py

  both_sides_div_neg_lt1: LEMMA x/nz < y/nz IFF y < x

  both_sides_div_neg_lt2: LEMMA pz/nx < pz/ny IFF ny < nx

  both_sides_div_neg_lt3: LEMMA nz/nx < nz/ny IFF nx < ny

  lt_plus_lt1: LEMMA x <= y AND z < w IMPLIES x + z < y + w

  lt_plus_lt2: LEMMA x < y AND z <= w IMPLIES x + z < y + w

  lt_minus_lt1: LEMMA x <= y AND w < z IMPLIES x - z < y - w

  lt_minus_lt2: LEMMA x < y AND w <= z IMPLIES x - z < y - w

  lt_times_lt_pos1: LEMMA px <= y AND nnz < w IMPLIES px * nnz < y * w

  lt_times_lt_pos2: LEMMA nnx < y AND pz <= w IMPLIES nnx * pz < y * w

  lt_div_lt_pos1: LEMMA px <= y AND pz < w IMPLIES px/w < y/pz

  lt_div_lt_pos2: LEMMA nnx < y AND pz <= w IMPLIES nnx/w < y/pz

  lt_times_lt_neg1: LEMMA x <= ny AND z < npw IMPLIES ny * npw < x * z

  lt_times_lt_neg2: LEMMA x < npy AND z <= nw IMPLIES npy * nw < x * z

  lt_div_lt_neg1: LEMMA x <= ny AND z < nw IMPLIES ny/z < x/nw

  lt_div_lt_neg2: LEMMA x < npy AND z <= nw IMPLIES npy/z < x/nw


  % Order lemmas for <=

  total_le: LEMMA total_order?(<=)

  dich_le: LEMMA x <= y OR y <= x

  zero_le_zero: LEMMA 0 <= 0

  neg_le: LEMMA 0 <= -x IFF x <= 0

  pos_times_le: LEMMA 0 <= x * y IFF (0 <= x AND 0 <= y) OR (x <= 0 AND y <= 0)

  neg_times_le: LEMMA x * y <= 0 IFF (0 <= x AND y <= 0) OR (x <= 0 AND 0 <= y)

  quotient_pos_le: FORMULA 0 <= 1/n0x IFF 0 <= n0x
  
  quotient_neg_le: FORMULA 1/n0x <= 0 IFF n0x <= 0

  pos_div_le: LEMMA
    0 <= x/n0y IFF (0 <= x AND 0 <= n0y) OR (x <= 0 AND n0y <= 0)

  neg_div_le: LEMMA
    x/n0y <= 0 IFF (0 <= x AND n0y <= 0) OR (x <= 0 AND 0 <= n0y)

  div_mult_pos_le1: LEMMA z/py <= x IFF z <= x * py

  div_mult_pos_le2: LEMMA x <= z/py IFF x * py <= z

  div_mult_neg_le1: LEMMA z/ny <= x IFF x * ny <= z

  div_mult_neg_le2: LEMMA x <= z/ny IFF z <= x * ny


  % Cancellation laws for <=

  both_sides_plus_le1: LEMMA x + z <= y + z IFF x <= y

  both_sides_plus_le2: LEMMA z + x <= z + y IFF x <= y

  both_sides_minus_le1: LEMMA x - z <= y - z IFF x <= y

  both_sides_minus_le2: LEMMA z - x <= z - y IFF y <= x

  both_sides_times_pos_le1: LEMMA x * pz <= y * pz IFF x <= y

  both_sides_times_pos_le2: LEMMA pz * x <= pz * y IFF x <= y

  both_sides_times_neg_le1: LEMMA x * nz <= y * nz IFF y <= x

  both_sides_times_neg_le2: LEMMA nz * x <= nz * y IFF y <= x

  both_sides_div_pos_le1: LEMMA x/pz <= y/pz IFF x <= y

  both_sides_div_pos_le2: LEMMA pz/px <= pz/py IFF py <= px

  both_sides_div_pos_le3: LEMMA nz/px <= nz/py IFF px <= py

  both_sides_div_neg_le1: LEMMA x/nz <= y/nz IFF y <= x

  both_sides_div_neg_le2: LEMMA pz/nx <= pz/ny IFF ny <= nx

  both_sides_div_neg_le3: LEMMA nz/nx <= nz/ny IFF nx <= ny

  le_plus_le: LEMMA x <= y AND z <= w IMPLIES x + z <= y + w

  le_minus_le: LEMMA x <= y AND w <= z IMPLIES x - z <= y - w

  le_times_le_pos: LEMMA nnx <= y AND nnz <= w IMPLIES nnx * nnz <= y * w

  le_div_le_pos: LEMMA nnx <= y AND pz <= w IMPLIES nnx/w <= y/pz

  le_times_le_neg: LEMMA x <= npy AND z <= npw IMPLIES npy * npw <= x * z

  le_div_le_neg: LEMMA x <= npy AND z <= nw IMPLIES npy/z <= x/nw


  % Order lemmas for >

  strict_gt : LEMMA strict_total_order?(>)

  trich_gt: LEMMA x > y OR x = y OR y > x

  tri_unique_gt1: LEMMA x > y IMPLIES (x /= y AND NOT(y > x))

  tri_unique_gt2: LEMMA x = y IMPLIES (NOT(x > y) AND NOT(y > x))

  zero_not_gt_zero: LEMMA NOT 0 > 0

  neg_gt: LEMMA 0 > -x IFF x > 0

  pos_times_gt: LEMMA x * y > 0 IFF (0 > x AND 0 > y) OR (x > 0 AND y > 0)

  neg_times_gt: LEMMA 0 > x * y IFF (0 > x AND y > 0) OR (x > 0 AND 0 > y)

  quotient_pos_gt: FORMULA 1/n0x > 0 IFF n0x > 0
  
  quotient_neg_gt: FORMULA 0 > 1/n0x IFF 0 > n0x

  pos_div_gt: LEMMA x/n0y > 0 IFF (0 > x AND 0 > n0y) OR (x > 0 AND n0y > 0)

  neg_div_gt: LEMMA 0 > x/n0y IFF (0 > x AND n0y > 0) OR (x > 0 AND 0 > n0y)

  % Cancellation laws for >

  both_sides_plus_gt1: LEMMA x + z > y + z IFF x > y

  both_sides_plus_gt2: LEMMA z + x > z + y IFF x > y

  both_sides_minus_gt1: LEMMA x - z > y - z IFF x > y

  both_sides_minus_gt2: LEMMA z - x > z - y IFF y > x

  both_sides_times_pos_gt1: LEMMA x * pz > y * pz IFF x > y

  both_sides_times_pos_gt2: LEMMA pz * x > pz * y IFF x > y

  both_sides_times_neg_gt1: LEMMA x * nz > y * nz IFF y > x

  both_sides_times_neg_gt2: LEMMA nz * x > nz * y IFF y > x

  both_sides_div_pos_gt1: LEMMA x/pz > y/pz IFF x > y

  both_sides_div_pos_gt2: LEMMA pz/px > pz/py IFF py > px

  both_sides_div_pos_gt3: LEMMA nz/px > nz/py IFF px > py

  both_sides_div_neg_gt1: LEMMA x/nz > y/nz IFF y > x

  both_sides_div_neg_gt2: LEMMA pz/nx > pz/ny IFF ny > nx

  both_sides_div_neg_gt3: LEMMA nz/nx > nz/ny IFF nx > ny

  gt_plus_gt1: LEMMA x >= y AND z > w IMPLIES x + z > y + w

  gt_plus_gt2: LEMMA x > y AND z >= w IMPLIES x + z > y + w

  gt_minus_gt1: LEMMA x >= y AND w > z IMPLIES x - z > y - w

  gt_minus_gt2: LEMMA x > y AND w >= z IMPLIES x - z > y - w

  gt_times_gt_pos1: LEMMA x >= py AND z > nnw IMPLIES x * z > py * nnw

  gt_times_gt_pos2: LEMMA x > nny AND z >= pw IMPLIES x * z > nny * pw

  gt_div_gt_pos1: LEMMA x >= py AND z > pw IMPLIES x/pw > py/z

  gt_div_gt_pos2: LEMMA x > nny AND z >= pw IMPLIES x/pw > nny/z

  gt_times_gt_neg1: LEMMA nx >= y AND npz > w IMPLIES y * w > nx * npz

  gt_times_gt_neg2: LEMMA npx > y AND nz >= w IMPLIES y * w > npx * nz

  gt_div_gt_neg1: LEMMA nx >= y AND nz > w IMPLIES y/nz > nx/w

  gt_div_gt_neg2: LEMMA npx > y AND nz >= w IMPLIES y/nz > npx/w


  % Order lemmas for >=

  total_ge : LEMMA total_order?(>=)

  dich_ge: LEMMA x >= y OR y >= x

  zero_ge_zero: LEMMA 0 >= 0

  neg_ge: LEMMA 0 >= -x IFF x >= 0

  pos_times_ge: LEMMA x * y >= 0 IFF (0 >= x AND 0 >= y) OR (x >= 0 AND y >= 0)

  neg_times_ge: LEMMA 0 >= x * y IFF (0 >= x AND y >= 0) OR (x >= 0 AND 0 >= y)

  quotient_pos_ge: FORMULA 1/n0x >= 0 IFF n0x >= 0
  
  quotient_neg_ge: FORMULA 0 >= 1/n0x IFF 0 >= n0x

  pos_div_ge: LEMMA
    x/n0y >= 0 IFF (0 >= x AND 0 >= n0y) OR (x >= 0 AND n0y >= 0)

  neg_div_ge: LEMMA
    0 >= x/n0y IFF (0 >= x AND n0y >= 0) OR (x >= 0 AND 0 >= n0y)

  div_mult_pos_ge1: LEMMA z/py >= x IFF z >= x * py

  div_mult_pos_ge2: LEMMA x >= z/py IFF x * py >= z

  div_mult_neg_ge1: LEMMA z/ny >= x IFF x * ny >= z

  div_mult_neg_ge2: LEMMA x >= z/ny IFF z >= x * ny


  % Cancellation laws for >=

  both_sides_plus_ge1: LEMMA x + z >= y + z IFF x >= y

  both_sides_plus_ge2: LEMMA z + x >= z + y IFF x >= y

  both_sides_minus_ge1: LEMMA x - z >= y - z IFF x >= y

  both_sides_minus_ge2: LEMMA z - x >= z - y IFF y >= x

  both_sides_times_pos_ge1: LEMMA x * pz >= y * pz IFF x >= y

  both_sides_times_pos_ge2: LEMMA pz * x >= pz * y IFF x >= y

  both_sides_times_neg_ge1: LEMMA x * nz >= y * nz IFF y >= x

  both_sides_times_neg_ge2: LEMMA nz * x >= nz * y IFF y >= x

  both_sides_div_pos_ge1: LEMMA x/pz >= y/pz IFF x >= y

  both_sides_div_pos_ge2: LEMMA pz/px >= pz/py IFF py >= px

  both_sides_div_pos_ge3: LEMMA nz/px >= nz/py IFF px >= py

  both_sides_div_neg_ge1: LEMMA x/nz >= y/nz IFF y >= x

  both_sides_div_neg_ge2: LEMMA pz/nx >= pz/ny IFF ny >= nx

  both_sides_div_neg_ge3: LEMMA nz/nx >= nz/ny IFF nx >= ny

  ge_plus_ge: LEMMA x >= y AND z >= w IMPLIES x + z >= y + w

  ge_minus_ge: LEMMA x >= y AND w >= z IMPLIES x - z >= y - w

  ge_times_ge_pos: LEMMA x >= nny AND z >= nnw IMPLIES x * z >= nny * nnw

  ge_div_ge_pos: LEMMA x >= nny AND z >= pw IMPLIES x/pw >= nny/z

  ge_times_ge_neg: LEMMA npx >= y AND npz >= w IMPLIES y * w >= npx * npz

  ge_div_ge_neg: LEMMA npx >= y AND nz >= w IMPLIES y/nz >= npx/w

  nonzero_times1: LEMMA n0x * y = 0 IFF y = 0

  nonzero_times2: LEMMA x * n0y = 0 IFF x = 0

  nonzero_times3: LEMMA n0x * n0y = 0 IFF FALSE

  % Useful lemmas about the multiplicative identity

  eq1_gt: FORMULA x > 1 AND x * y = 1 IMPLIES y < 1

  eq1_ge: FORMULA x >= 1 AND x * y = 1 IMPLIES y <= 1
  
  eqm1_gt: FORMULA x > 1 AND x * y = -1 IMPLIES y > -1

  eqm1_ge: FORMULA x >= 1 AND x * y = -1 IMPLIES y >= -1

  eqm1_lt: FORMULA x < -1 AND x * y = -1 IMPLIES y < 1

  eqm1_le: FORMULA x <= -1 AND x * y = -1 IMPLIES y <= 1

  sqrt_1: LEMMA x * x = 1 IFF x = 1 OR x = -1

  sqrt_1_lt: LEMMA x * x < 1 IMPLIES abs(x) < 1

  sqrt_1_le: LEMMA x * x <= 1 IMPLIES abs(x) <= 1

  idem_mult: LEMMA x * x = x IFF x = 0 OR x = 1


  i, j: VAR int

  product_1: LEMMA i >= 0 AND j >= 0 AND i*j = 1 IMPLIES i = 1 AND j = 1

  product_m1: LEMMA i >= 0 AND j <= 0 AND i*j = -1 IMPLIES i = 1 AND j = -1


  % Properties of absolute value

  triangle: LEMMA abs(x+y) <= abs(x) + abs(y)  

  abs_mult: LEMMA abs(x * y) = abs(x) * abs(y)

  abs_div: LEMMA abs(x / n0y) = abs(x) / abs(n0y)

  abs_abs: LEMMA abs(abs(x)) = abs(x)

  abs_square: LEMMA abs(x * x) = x * x

  abs_limits: LEMMA -(abs(x) + abs(y)) <= x + y AND x + y <= abs(x) + abs(y)


  % The axiom of Archimedes 

  axiom_of_archimedes: LEMMA
    FORALL (x: real): EXISTS (i: int): x < i

  archimedean: LEMMA
    FORALL (px: posreal): EXISTS (n: posnat): 1/n < px

  real_lt_is_strict_total_order: JUDGEMENT
    < HAS_TYPE (strict_total_order?[real])

  real_le_is_total_order: JUDGEMENT <= HAS_TYPE (total_order?[real])

  real_gt_is_strict_total_order: JUDGEMENT
    > HAS_TYPE (strict_total_order?[real])

  real_ge_is_total_order: JUDGEMENT >= HAS_TYPE (total_order?[real])

 END real_props

%% Contains extra properties about reals needed by the formula
%% manipulation strategies in package Manip.  Can be seen as an
%% extension of the real_props theory in the prelude.

extra_real_props: THEORY
BEGIN

%% Same variable declarations as real_props in the prelude:

  w, x, y, z: VAR real
  n0w, n0x, n0y, n0z: VAR nonzero_real
  nnw, nnx, nny, nnz: VAR nonneg_real
  pw, px, py, pz: VAR posreal
  npw, npx, npy, npz: VAR nonpos_real
  nw, nx, ny, nz: VAR negreal


%% Lemmas used to handle cases where a multiplier or divisor can be
%% either positive or negative.

pos_neg_split: LEMMA  EXISTS px, nx: n0x = px or n0x = nx


div_mult_pos_neg_lt1: LEMMA
    z/n0y < x IFF IF n0y > 0 THEN z < x * n0y ELSE x * n0y < z ENDIF

div_mult_pos_neg_lt2: LEMMA
    x < z/n0y IFF IF n0y > 0 THEN x * n0y < z ELSE z < x * n0y ENDIF

div_mult_pos_neg_le1: LEMMA
    z/n0y <= x IFF IF n0y > 0 THEN z <= x * n0y ELSE x * n0y <= z ENDIF

div_mult_pos_neg_le2: LEMMA
    x <= z/n0y IFF IF n0y > 0 THEN x * n0y <= z ELSE z <= x * n0y ENDIF

div_mult_pos_neg_gt1: LEMMA
    z/n0y > x IFF IF n0y > 0 THEN z > x * n0y ELSE x * n0y > z ENDIF

div_mult_pos_neg_gt2: LEMMA
    x > z/n0y IFF IF n0y > 0 THEN x * n0y > z ELSE z > x * n0y ENDIF

div_mult_pos_neg_ge1: LEMMA
    z/n0y >= x IFF IF n0y > 0 THEN z >= x * n0y ELSE x * n0y >= z ENDIF

div_mult_pos_neg_ge2: LEMMA
    x >= z/n0y IFF IF n0y > 0 THEN x * n0y >= z ELSE z >= x * n0y ENDIF


both_sides_times_pos_neg_lt1: LEMMA
  IF n0z > 0 THEN x * n0z < y * n0z ELSE y * n0z < x * n0z ENDIF IFF x < y

both_sides_times_pos_neg_lt2: LEMMA
  IF n0z > 0 THEN n0z * x < n0z * y ELSE n0z * y < n0z * x ENDIF IFF x < y

both_sides_times_pos_neg_le1: LEMMA
  IF n0z > 0 THEN x * n0z <= y * n0z ELSE y * n0z <= x * n0z ENDIF IFF x <= y

both_sides_times_pos_neg_le2: LEMMA
  IF n0z > 0 THEN n0z * x <= n0z * y ELSE n0z * y <= n0z * x ENDIF IFF x <= y

both_sides_times_pos_neg_gt1: LEMMA
  IF n0z > 0 THEN x * n0z > y * n0z ELSE y * n0z > x * n0z ENDIF IFF x > y

both_sides_times_pos_neg_gt2: LEMMA
  IF n0z > 0 THEN n0z * x > n0z * y ELSE n0z * y > n0z * x ENDIF IFF x > y

both_sides_times_pos_neg_ge1: LEMMA
  IF n0z > 0 THEN x * n0z >= y * n0z ELSE y * n0z >= x * n0z ENDIF IFF x >= y

both_sides_times_pos_neg_ge2: LEMMA
  IF n0z > 0 THEN n0z * x >= n0z * y ELSE n0z * y >= n0z * x ENDIF IFF x >= y


%% The naming scheme below follows that of the both_sides_div_+/-_R1/2/3
%% series in real_props as consistently as possible.

both_sides_div_pos_neg_lt1: LEMMA
  IF n0z > 0 THEN x/n0z < y/n0z ELSE y/n0z < x/n0z ENDIF IFF x < y

both_sides_div_pos_neg_lt2: LEMMA
  IF n0z > 0 THEN n0z/px < n0z/py ELSE n0z/py < n0z/px ENDIF IFF py < px

both_sides_div_pos_neg_lt3: LEMMA
  IF n0z > 0 THEN n0z/nx < n0z/ny ELSE n0z/ny < n0z/nx ENDIF IFF ny < nx

both_sides_div_pos_neg_le1: LEMMA
  IF n0z > 0 THEN x/n0z <= y/n0z ELSE y/n0z <= x/n0z ENDIF IFF x <= y

both_sides_div_pos_neg_le2: LEMMA
  IF n0z > 0 THEN n0z/px <= n0z/py ELSE n0z/py <= n0z/px ENDIF IFF py <= px

both_sides_div_pos_neg_le3: LEMMA
  IF n0z > 0 THEN n0z/nx <= n0z/ny ELSE n0z/ny <= n0z/nx ENDIF IFF ny <= nx

both_sides_div_pos_neg_gt1: LEMMA
  IF n0z > 0 THEN x/n0z > y/n0z ELSE y/n0z > x/n0z ENDIF IFF x > y

both_sides_div_pos_neg_gt2: LEMMA
  IF n0z > 0 THEN n0z/px > n0z/py ELSE n0z/py > n0z/px ENDIF IFF py > px

both_sides_div_pos_neg_gt3: LEMMA
  IF n0z > 0 THEN n0z/nx > n0z/ny ELSE n0z/ny > n0z/nx ENDIF IFF ny > nx

both_sides_div_pos_neg_ge1: LEMMA
  IF n0z > 0 THEN x/n0z >= y/n0z ELSE y/n0z >= x/n0z ENDIF IFF x >= y

both_sides_div_pos_neg_ge2: LEMMA
  IF n0z > 0 THEN n0z/px >= n0z/py ELSE n0z/py >= n0z/px ENDIF IFF py >= px

both_sides_div_pos_neg_ge3: LEMMA
  IF n0z > 0 THEN n0z/nx >= n0z/ny ELSE n0z/ny >= n0z/nx ENDIF IFF ny >= nx


%% Less restrictive lemmas used by strategy MULT-BY than the 
%% both_sides_times series in real_props.  Allows multiplier to be
%% zero in some cases.  Variable z changed to w so it would
%% precede x,y during INST and make all lemmas consistent.

  both_sides_times1_imp: LEMMA x = y IMPLIES x * w = y * w

  both_sides_times2_imp: LEMMA x = y IMPLIES w * x = w * y

  both_sides_times_pos_le1_imp: LEMMA x <= y IMPLIES x * nnw <= y * nnw

  both_sides_times_pos_le2_imp: LEMMA x <= y IMPLIES nnw * x <= nnw * y

  both_sides_times_neg_le1_imp: LEMMA y <= x IMPLIES x * npw <= y * npw

  both_sides_times_neg_le2_imp: LEMMA y <= x IMPLIES npw * x <= npw * y

  both_sides_times_pos_ge1_imp: LEMMA x >= y IMPLIES x * nnw >= y * nnw

  both_sides_times_pos_ge2_imp: LEMMA x >= y IMPLIES nnw * x >= nnw * y

  both_sides_times_neg_ge1_imp: LEMMA y >= x IMPLIES x * npw >= y * npw

  both_sides_times_neg_ge2_imp: LEMMA y >= x IMPLIES npw * x >= npw * y


  both_sides_times_pos_neg_le1_imp: LEMMA
    x <= y IMPLIES IF w >= 0 THEN x * w <= y * w ELSE y * w <= x * w ENDIF

  both_sides_times_pos_neg_le2_imp: LEMMA
    x <= y IMPLIES IF w >= 0 THEN w * x <= w * y ELSE w * y <= w * x ENDIF

  both_sides_times_pos_neg_ge1_imp: LEMMA
    x >= y IMPLIES IF w >= 0 THEN x * w >= y * w ELSE y * w >= x * w ENDIF

  both_sides_times_pos_neg_ge2_imp: LEMMA
    x >= y IMPLIES IF w >= 0 THEN w * x >= w * y ELSE w * y >= w * x ENDIF


%% Additional lemmas needed to fill in gaps left by real_props.

  zero_times4: LEMMA 0 = x * y IFF x = 0 OR y = 0

  times_div_cancel1: LEMMA (n0z * x) / n0z = x

  times_div_cancel2: LEMMA (x * n0z) / n0z = x

%% Replacements for real_props lemmas to correct inconsistent naming.

  div_mult_pos_gt1: LEMMA z/py > x IFF z > x * py

  div_mult_pos_gt2: LEMMA x > z/py IFF x * py > z

  div_mult_neg_gt1: LEMMA z/ny > x IFF x * ny > z

  div_mult_neg_gt2: LEMMA x > z/ny IFF z > x * ny


%% Transitivity lemmas for inequality reasoning.  Normally unnecessary
%% but sometimes helpful for forcing case splits.

lt_cut: LEMMA x < y AND y < z IMPLIES x < z
le_cut: LEMMA x <= y AND y <= z IMPLIES x <= z
gt_cut: LEMMA x > y AND y > z IMPLIES x > z
ge_cut: LEMMA x >= y AND y >= z IMPLIES x >= z


%% Rules used to deduce inequalities on products of reals.  These rules
%% stipulate only sufficient conditions for the inequalities to hold.
%% The most common and useful cases are included, although additional
%% cases might be desirable later.

le_times_le_any1: LEMMA
	IF w >= 0 IFF x >= 0
	   THEN IF y >= 0 IFF z >= 0
		   THEN abs(w) <= abs(y) AND abs(x) <= abs(z)
		   ELSE (w = 0 OR x = 0) AND (y = 0 OR z = 0)
	        ENDIF
	   ELSE IF y >= 0 IFF z >= 0
		   THEN true
		   ELSE abs(w) >= abs(y) AND abs(x) >= abs(z)
	        ENDIF
        ENDIF
	  IMPLIES w * x <= y * z

ge_times_ge_any1: LEMMA
	IF y >= 0 IFF z >= 0
	   THEN IF w >= 0 IFF x >= 0
		   THEN abs(w) >= abs(y) AND abs(x) >= abs(z)
		   ELSE (w = 0 OR x = 0) AND (y = 0 OR z = 0)
	        ENDIF
	   ELSE IF w >= 0 IFF x >= 0
		   THEN true
		   ELSE abs(w) <= abs(y) AND abs(x) <= abs(z)
	        ENDIF
        ENDIF
	  IMPLIES w * x >= y * z

lt_times_lt_any1: LEMMA
	IF w = 0 OR x = 0
	   THEN 0 < y AND 0 < z OR y < 0 AND z < 0
	ELSIF w > 0 IFF x > 0
	   THEN (y > 0 IFF z > 0) AND
                (abs(w) <= abs(y) AND abs(x) <  abs(z) OR
                 abs(w) <  abs(y) AND abs(x) <= abs(z))
	ELSIF y > 0 IFF z > 0
           THEN true
	   ELSE abs(w) >= abs(y) AND abs(x) >  abs(z) OR
                abs(w) >  abs(y) AND abs(x) >= abs(z)
        ENDIF
	  IMPLIES w * x < y * z

gt_times_gt_any1: LEMMA
	IF y = 0 OR z = 0
	   THEN 0 < w AND 0 < x OR w < 0 AND x < 0
	ELSIF y > 0 IFF z > 0
	   THEN (w > 0 IFF x > 0) AND
                (abs(w) >= abs(y) AND abs(x) >  abs(z) OR
                 abs(w) >  abs(y) AND abs(x) >= abs(z))
	ELSIF w > 0 IFF x > 0
           THEN true
	   ELSE abs(w) <= abs(y) AND abs(x) <  abs(z) OR
                abs(w) <  abs(y) AND abs(x) <= abs(z)
        ENDIF
	  IMPLIES w * x > y * z


%% Contrapositive forms of series R_times_R_any1.  They stipulate
%% necessary conditions for the inequalities to hold.

le_times_le_any2: LEMMA
	w * x <= y * z IMPLIES
	IF y = 0 OR z = 0
	   THEN (0 >= w OR 0 >= x) AND (w >= 0 OR x >= 0)
	ELSIF y > 0 IFF z > 0
	   THEN (w > 0 IFF x > 0) IMPLIES
                (abs(w) <  abs(y) OR abs(x) <= abs(z)) AND
                (abs(w) <= abs(y) OR abs(x) <  abs(z))
	ELSE NOT (w > 0 IFF x > 0) AND
	     (abs(w) >  abs(y) OR abs(x) >= abs(z)) AND
             (abs(w) >= abs(y) OR abs(x) >  abs(z))
        ENDIF

ge_times_ge_any2: LEMMA
	w * x >= y * z IMPLIES
	IF w = 0 OR x = 0
	   THEN (0 >= y OR 0 >= z) AND (y >= 0 OR z >= 0)
	ELSIF w > 0 IFF x > 0
	   THEN (y > 0 IFF z > 0) IMPLIES
                (abs(w) >  abs(y) OR abs(x) >= abs(z)) AND
                (abs(w) >= abs(y) OR abs(x) > abs(z))
	ELSE NOT (y > 0 IFF z > 0) AND
             (abs(w) <  abs(y) OR abs(x) <= abs(z)) AND
             (abs(w) <= abs(y) OR abs(x) <  abs(z))
        ENDIF

lt_times_lt_any2: LEMMA
	w * x < y * z IMPLIES
	IF y >= 0 IFF z >= 0
	   THEN IF w >= 0 IFF x >= 0
		   THEN abs(w) < abs(y) OR abs(x) < abs(z)
		   ELSE (w /= 0 AND x /= 0) OR (y /= 0 AND z /= 0)
	        ENDIF
	   ELSE NOT (w >= 0 IFF x >= 0) AND
		(abs(w) > abs(y) OR abs(x) > abs(z))
        ENDIF

gt_times_gt_any2: LEMMA
	w * x > y * z IMPLIES
	IF w >= 0 IFF x >= 0
	   THEN IF y >= 0 IFF z >= 0
		   THEN abs(w) > abs(y) OR abs(x) > abs(z)
		   ELSE (w /= 0 AND x /= 0) OR (y /= 0 AND z /= 0)
	        ENDIF
	   ELSE NOT (y >= 0 IFF z >= 0) AND
		(abs(w) < abs(y) OR abs(x) < abs(z))
        ENDIF


END extra_real_props

%%% This file contains some simplification rules missing in real_props.
%%% Part of the Field package of Cesar Munoz
extra_tegies : THEORY
BEGIN
  x,y : VAR real
  n0z : VAR nzreal

  neg_mult : LEMMA
    -x*y =  -(x*y)

  mult_neg : LEMMA
    x*-y =  -(x*y)

  neg_add : LEMMA
    -x + y =  y - x

  add_neg : LEMMA
    x + -y =  x - y

  neg_div : LEMMA
    -x/n0z = -(x/n0z)

  div_neg : LEMMA
    x/-n0z = -(x/n0z)

  one_times: LEMMA
    1*x = x

  neg_one_times: LEMMA
    -1*x = -x

  zero_div: LEMMA
    0/n0z = 0

  neg_neg: LEMMA
    --x = x

END extra_tegies



% rational_props contains the properties of rational numbers.  This mostly
% consists of subtypes and judgements, as most of the properties given in
% real_props are inherited.

rational_props: THEORY
 BEGIN
  x, y: VAR real
  i: VAR int
  n0j: VAR nzint
  p: VAR posnat
  r: VAR rat

  rational_pred_ax: AXIOM EXISTS i, n0j: r = i/n0j
  rational_pred_ax2: LEMMA EXISTS i, p: r = i/p

  density_positive : LEMMA
      0 <= x AND x < y IMPLIES (EXISTS r: x < r AND r < y)
  
  density: LEMMA x < y IMPLIES (EXISTS r: x < r AND r < y)

 END rational_props


% integer_props contains the properties of integers and naturalnumbers.

integer_props: THEORY
 BEGIN
  m, n: VAR nat
  i, j, k: VAR int
  n0j: VAR nzint

  N: VAR (nonempty?[nat])

  I: VAR (nonempty?[int])

  integer_pred_ax: LEMMA EXISTS n: i = n OR i = -n

  div_simple: LEMMA (EXISTS k: i = k*n0j) = integer_pred(i/n0j)

  lub_nat: LEMMA
    upper_bound?(m, N)
      => EXISTS (n:(N)): least_upper_bound?(n, N)

  lub_int: LEMMA
    upper_bound?(i, I)
      => EXISTS (j:(I)): least_upper_bound?(j, I)

  glb_nat: LEMMA
    EXISTS (n:(N)): greatest_lower_bound?(n, N)

  glb_int: LEMMA
    lower_bound?(i, I)
      => EXISTS (j:(I)): greatest_lower_bound?(j, I)

 END integer_props


% The definitions for floor and ceiling, courtesy of
%   Paul S. Miner   		           email: p.s.miner@larc.nasa.gov
%   Mail Stop 130			     fax: (804) 864-4234
%   NASA Langley Research Center	   phone: (804) 864-6201
%   Hampton, Virginia 23681-0001

floor_ceil: THEORY
 BEGIN
  
  x, y: VAR real
  py:  VAR posreal
  j: VAR nonzero_integer
  i, k: VAR integer
  
  floor_exists: LEMMA EXISTS i: i <= x & x < i + 1
  
  ceiling_exists: LEMMA EXISTS i: x <= i & i < x + 1
  
  floor(x): {i | i <= x & x < i + 1}
  
  fractional(x): {x | 0 <= x & x < 1} = x - floor(x)
  
  ceiling(x): {i | x <= i & i < x + 1}
  
  floor_def: LEMMA floor(x) <= x & x < floor(x) + 1
  
  ceiling_def: LEMMA x <= ceiling(x) & ceiling(x) < x + 1
  
  floor_ceiling_reflect1: LEMMA floor(-x) = -ceiling(x)
  
  floor_ceiling_reflect2: LEMMA ceiling(-x) = -floor(x)
  
  nonneg_floor_is_nat: JUDGEMENT floor(x:nonneg_real) HAS_TYPE nat
  nonneg_ceiling_is_nat: JUDGEMENT ceiling(x:nonneg_real) HAS_TYPE nat
  
  floor_int: LEMMA floor(i) = i
  
  ceiling_int: LEMMA ceiling(i) = i
  
  floor_plus_int: LEMMA floor(x + i) = floor(x) + i
  
  ceiling_plus_int: LEMMA ceiling(x + i) = ceiling(x) + i
  
  floor_ceiling_nonint: LEMMA NOT integer?(x) => ceiling(x) - floor(x) = 1

  floor_ceiling_int: lemma floor(i)=ceiling(i)
  
  floor_neg: LEMMA 
        floor(x) = IF integer?(x) THEN -floor(-x) ELSE -floor(-x) - 1 ENDIF
  
  real_parts: LEMMA x = floor(x) + fractional(x)
  
  floor_plus: LEMMA 
        floor(x + y) = floor(x) + floor(y) + floor(fractional(x) + fractional(y))
  
  ceiling_plus: LEMMA
        ceiling(x + y) = floor(x) + floor(y) + ceiling(fractional(x) + fractional(y))
  
  floor_split: lemma i = floor(i/2)+ceiling(i/2)

  floor_within_1: lemma x - floor(x) < 1

  ceiling_within_1: lemma ceiling(x) - x < 1

  floor_val:   LEMMA i >= k*j AND i < (k+1)*j IMPLIES floor(i/j) = k 

  floor_small: LEMMA  abs(i) < abs(j) IMPLIES
                         floor(i/j) = IF i/j >= 0 THEN 0 ELSE -1 ENDIF

  floor_eq_0:  LEMMA floor(x) = 0 IMPLIES x >= 0 AND x < 1

  fractional_plus: LEMMA
        fractional(x+y) = fractional(fractional(x) + fractional(y))

  floor_div: LEMMA floor(x/py) = i IFF py*i <= x AND x < py*(i+1)
  floor_0:   LEMMA floor(x)    = 0 IFF 0    <= x AND x < 1

 END floor_ceil


% exponentiation provides the definitions expt and ^.  expt multiplies a
% real by itself the number of times specified, where 0 times returns a 1
% (thus expt(0,0) = 1).  ^ is defined in terms of expt to work for
% integers, but in this case if the integer negative then the real
% argument must be nonzero; this leads to the dependent type given below.

exponentiation: THEORY
 BEGIN
  r: VAR real
  q: VAR rat
  nnq: VAR nonneg_rat
  m, n: VAR nat
  pm, pn: VAR posnat
  i, j: VAR int
  n0i, n0j: VAR nzint
  x, y: VAR real
  px, py: VAR posreal
  n0x, n0y: VAR nzreal
  gt1x, gt1y: VAR {r: posreal | r > 1}
  lt1x, lt1y: VAR {r: posreal | r < 1}
  ge1x, ge1y: VAR {r: posreal | r >= 1}
  le1x, le1y: VAR {r: posreal | r <= 1}

  expt(r, n): RECURSIVE real =
    IF n = 0 THEN 1
    ELSE r * expt(r, n-1)
    ENDIF
   MEASURE n;

  expt_pos_aux: LEMMA expt(px, n) > 0

  expt_nonzero_aux: LEMMA expt(n0x, n) /= 0;

  nnreal_expt:  JUDGEMENT expt(x:nnreal,  n:nat) HAS_TYPE nnreal
  posreal_expt: JUDGEMENT expt(x:posreal, n:nat) HAS_TYPE posreal
  nzreal_expt:  JUDGEMENT expt(x:nzreal,  n:nat) HAS_TYPE nzreal
  rat_expt:     JUDGEMENT expt(x:rat,     n:nat) HAS_TYPE rat
  nnrat_expt:   JUDGEMENT expt(x:nnrat,   n:nat) HAS_TYPE nnrat
  posrat_expt:  JUDGEMENT expt(x:posrat,  n:nat) HAS_TYPE posrat
  int_expt:     JUDGEMENT expt(x:int,     n:nat) HAS_TYPE int
  nat_expt:     JUDGEMENT expt(x:nat,     n:nat) HAS_TYPE nat
  posnat_expt:  JUDGEMENT expt(x:posnat,  n:nat) HAS_TYPE posnat

  ^(r: real, i:{i:int | r /= 0 OR i >= 0}): real
    = IF i >= 0 THEN expt(r, i) ELSE 1/expt(r, -i) ENDIF

  expt_pos: LEMMA px^i > 0

  expt_nonzero: LEMMA n0x^i /= 0

  nnreal_exp:  JUDGEMENT ^(x:nnreal,  i:int | x/=0 OR i>=0) HAS_TYPE nnreal
  posreal_exp: JUDGEMENT ^(x:posreal, i:int) HAS_TYPE posreal
  nzreal_exp:  JUDGEMENT ^(x:nzreal,  i:int) HAS_TYPE nzreal
  rat_exp:     JUDGEMENT ^(x:rat,     i:int | x/=0 OR i>=0) HAS_TYPE rat
  nnrat_exp:   JUDGEMENT ^(x:nnrat,   i:int | x/=0 OR i>=0) HAS_TYPE nnrat
  posrat_exp:  JUDGEMENT ^(x:posrat,  i:int) HAS_TYPE posrat
  int_exp:     JUDGEMENT ^(x:int, n:nat)    HAS_TYPE int
  nat_exp:     JUDGEMENT ^(x:nat, n:nat)    HAS_TYPE nat
  posint_exp:  JUDGEMENT ^(x:posint, n:nat) HAS_TYPE posint

  % Properties of expt

  expt_x0_aux: LEMMA expt(x, 0) = 1

  expt_x1_aux: LEMMA expt(x, 1) = x

  expt_1n_aux: LEMMA expt(1, n) = 1

  increasing_expt_aux: LEMMA expt(gt1x, m+2) > gt1x

  decreasing_expt_aux: LEMMA expt(lt1x, m+2) < lt1x

  expt_1_aux: LEMMA expt(px, n + 1) = 1 IFF px = 1

  expt_plus_aux: LEMMA expt(n0x, m + n) = expt(n0x, m) * expt(n0x, n)

  expt_minus_aux: LEMMA
    m >= n IMPLIES expt(n0x, m - n) = expt(n0x, m)/expt(n0x, n)

  expt_times_aux: LEMMA expt(n0x, m * n) = expt(expt(n0x, m), n)

  expt_divide_aux: LEMMA 1/expt(n0x, m * n) = expt(1/expt(n0x, m), n)

  both_sides_expt1_aux: LEMMA expt(px, m+1) = expt(px, n+1) IFF m = n OR px = 1

  both_sides_expt2_aux: LEMMA expt(px, pm) = expt(py, pm) IFF px = py

  both_sides_expt_pos_lt_aux: LEMMA
    expt(px, m+1) < expt(py, m+1) IFF px < py

  both_sides_expt_gt1_lt_aux: LEMMA
    expt(gt1x, m+1) < expt(gt1x, n+1) IFF m < n

  both_sides_expt_lt1_lt_aux: LEMMA
    expt(lt1x, m+1) < expt(lt1x, n+1) IFF n < m

  both_sides_expt_pos_le_aux: LEMMA
    expt(px, m+1) <= expt(py, m+1) IFF px <= py

  both_sides_expt_gt1_le_aux: LEMMA
    expt(gt1x, m+1) <= expt(gt1x, n+1) IFF m <= n

  both_sides_expt_lt1_le_aux: LEMMA
    expt(lt1x, m+1) <= expt(lt1x, n+1) IFF n <= m

  both_sides_expt_pos_gt_aux: LEMMA
    expt(px, m+1) > expt(py, m+1) IFF px > py

  both_sides_expt_gt1_gt_aux: LEMMA
    expt(gt1x, m+1) > expt(gt1x, n+1) IFF m > n

  both_sides_expt_lt1_gt_aux: LEMMA
    expt(lt1x, m+1) > expt(lt1x, n+1) IFF n > m

  both_sides_expt_pos_ge_aux: LEMMA
    expt(px, m+1) >= expt(py, m+1) IFF px >= py

  both_sides_expt_gt1_ge_aux: LEMMA
    expt(gt1x, m+1) >= expt(gt1x, n+1) IFF m >= n

  both_sides_expt_lt1_ge_aux: LEMMA
    expt(lt1x, m+1) >= expt(lt1x, n+1) IFF n >= m

  expt_of_mult: LEMMA expt(x * y, n) = expt(x, n) * expt(y, n)

  expt_of_div: LEMMA expt(x / n0y, n) = expt(x, n) / expt(n0y, n)

  expt_of_inv: LEMMA expt(1 / n0x, n) = 1 / expt(n0x, n)

  expt_of_abs: LEMMA expt(abs(x), n) = abs(expt(x, n))

  abs_of_expt_inv: LEMMA abs(1 / expt(n0x, n)) = 1 / expt(abs(n0x),n)

  % Properties of ^

  expt_x0: LEMMA x^0 = 1

  expt_x1: LEMMA x^1 = x
  expt_x2: LEMMA x^2 = x*x
  expt_x3: LEMMA x^3 = x*x*x
  expt_x4: LEMMA x^4 = x*x*x*x

  expt_1i: LEMMA 1^i = 1

  expt_eq_0: LEMMA x^pn = 0 IFF x = 0

  expt_plus: LEMMA n0x^(i + j) = n0x^i * n0x^j

  expt_times: LEMMA n0x^(i * j) = (n0x^i)^j

  expt_inverse: LEMMA n0x^(-i) = 1/(n0x^i)

  expt_div: LEMMA n0x^i/n0x^j = n0x^(i-j)

  both_sides_expt1: LEMMA px ^ n0i = px ^ n0j IFF n0i = n0j OR px = 1

  both_sides_expt2: LEMMA px ^ n0i = py ^ n0i IFF px = py

  b: VAR above(1)

  pos_expt_gt: LEMMA n < b^n

  expt_ge1: LEMMA b^n >= 1

  both_sides_expt_pos_lt: LEMMA px ^ pm < py ^ pm IFF px < py

  both_sides_expt_gt1_lt: LEMMA gt1x ^ i < gt1x ^ j IFF i < j

  both_sides_expt_lt1_lt: LEMMA lt1x ^ i < lt1x ^ j IFF j < i

  both_sides_expt_pos_le: LEMMA px ^ pm <= py ^ pm IFF px <= py

  both_sides_expt_gt1_le: LEMMA gt1x ^ i <= gt1x ^ j IFF i <= j

  both_sides_expt_lt1_le: LEMMA lt1x ^ i <= lt1x ^ j IFF j <= i

  both_sides_expt_pos_gt: LEMMA px ^ pm > py ^ pm IFF px > py

  both_sides_expt_gt1_gt: LEMMA gt1x ^ i > gt1x ^ j IFF i > j

  both_sides_expt_lt1_gt: LEMMA lt1x ^ i > lt1x ^ j IFF j > i

  both_sides_expt_pos_ge: LEMMA px ^ pm >= py ^ pm IFF px >= py

  both_sides_expt_gt1_ge: LEMMA gt1x ^ i >= gt1x ^ j IFF i >= j

  both_sides_expt_lt1_ge: LEMMA lt1x ^ i >= lt1x ^ j IFF j >= i

  expt_gt1_pos: LEMMA gt1x^pm >= gt1x

  expt_gt1_neg: LEMMA gt1x^(-pm) < 1

  expt_gt1_nonpos: LEMMA gt1x^(-m) <= 1

  mult_expt: LEMMA (n0x * n0y) ^i = n0x^i * n0y^i

  div_expt : LEMMA (n0x / n0y)^i = n0x^i / n0y^i

  inv_expt : LEMMA (1 / n0x)^i = 1 / n0x^i

  abs_expt: LEMMA abs(n0x)^i = abs(n0x^i)

  abs_hat_nat : LEMMA abs(x)^n = abs(x^n)

  expt_minus1_abs:   LEMMA abs((-1)^i) = 1
  even_m1_pow: LEMMA even?(i) IMPLIES (-1)^i = 1
  not_even_m1_pow: LEMMA NOT even?(i) IMPLIES (-1)^i = -1

  expt_lt1_bound1: LEMMA  expt(lt1x, n) <= 1

  expt_lt1_bound2: LEMMA  expt(lt1x, pn) < 1

  expt_gt1_bound1: LEMMA  1 <= expt(gt1x, n)

  expt_gt1_bound2: LEMMA  1 < expt(gt1x, pn)

  large_expt: LEMMA 1 < px  IMPLIES (FORALL py: EXISTS n: py < expt(px, n))

  small_expt: LEMMA px < 1  IMPLIES (FORALL py: EXISTS n: expt(px, n) < py)

  exponent_adjust: LEMMA b^i+b^(i-pm) < b^(i+1)

  exp_of_exists: lemma exists i: b^i <= py & py < b^(i+1)

 END exponentiation


% Euclidean division courtesy of Bruno Dutertre

euclidean_division : THEORY
 BEGIN
  a, i : VAR nat
  b : VAR posnat
  n : VAR int

  %-----------------------------------------------
  %  Type mod(b) = 0.. b-1
  %  (replace below[b] to reduce number of TCCs)
  %-----------------------------------------------

  mod(b) : NONEMPTY_TYPE = { i | i <  b}

  %-----------------------
  %  Euclidean division
  %-----------------------

  euclid_nat : LEMMA
        EXISTS (q : nat), (r : mod(b)) : a = b * q + r

  euclid_int : PROPOSITION
        EXISTS (q : int), (r : mod(b)) : n = b * q + r

  unique_quotient : PROPOSITION
        FORALL (q1, q2 : int), (r1, r2 : mod(b)) :
            b * q1 + r1 = b * q2 + r2 IMPLIES q1 = q2

  unique_remainder : COROLLARY
        FORALL (q1, q2 : int), (r1, r2 : mod(b)) :
            b * q1 + r1 = b * q2 + r2 IMPLIES r1 = r2

  unique_division : COROLLARY
        FORALL (q1, q2 : int), (r1, r2 : mod(b)) :
            b * q1 + r1 = b * q2 + r2 IMPLIES q1 = q2 AND r1 = r2

 END euclidean_division


%  Divisibility relation
%  For integers and natural numbers
%  Provided by Bruno Dutertre
divides : THEORY
 BEGIN
  n, m, l, x, y : VAR int
  p, q : VAR nat
  nz : VAR nzint

  %--------------------
  %  Divides relation
  %--------------------

  divides(n, m): bool = EXISTS x : m = n * x

  divides(n)(m): bool = divides(n, m)

  mult_divides1: JUDGEMENT *(n, m) HAS_TYPE (divides(n))
  mult_divides2: JUDGEMENT *(n, m) HAS_TYPE (divides(m))

  %----------------
  %  Easy lemmas
  %----------------

  divides_sum : LEMMA
     divides(x, n) AND divides(x, m) IMPLIES divides(x, n + m)

  divides_diff : LEMMA
     divides(x, n) AND divides(x, m) IMPLIES divides(x, n - m)

  divides_opposite : LEMMA
     divides(x, - n) IFF divides(x, n)

  opposite_divides : LEMMA
     divides(- x, n) IFF divides(x, n)

  divides_prod1 : LEMMA
     divides(x, n) IMPLIES divides(x, n * m)

  divides_prod2 : LEMMA
     divides(x, n) IMPLIES divides(x, m * n)

  %---------------
  %  Elimination
  %---------------

  divides_prod_elim1 : LEMMA
     divides(nz * n, nz * m) IFF divides(n, m)

  divides_prod_elim2 : LEMMA
     divides(n* nz, m * nz) IFF divides(n, m)

  %------------------------------------
  %  Reflexivity and transitivity
  %------------------------------------

  divides_reflexive: LEMMA divides(n, n)

  divides_transitive: LEMMA
     divides(n, m) AND divides(m, l) IMPLIES divides(n, l)

  %-----------------------------------------
  %  Mutual divisors are equal or opposite
  %-----------------------------------------

  product_one : LEMMA 
     x * y = 1 IFF (x = 1 AND y = 1) OR (x = -1 AND y = -1)

  mutual_divisors : LEMMA 
     divides(n, m) AND divides(m, n) IMPLIES n = m OR n = - m

  mutual_divisors_nat: LEMMA
     divides(p, q) AND divides(q, p) IMPLIES p = q
  
  %--------------------------------------
  %  special properties of zero and one
  %--------------------------------------

  one_divides : LEMMA divides(1, n)

  divides_zero : LEMMA divides(n, 0)

  zero_div_zero : LEMMA divides(0, n) IFF n = 0

  divisors_of_one : LEMMA divides(n, 1) IFF n = 1 OR n = -1

  one_div_one : LEMMA divides(p, 1) IFF p = 1

  %--------------------------------
  %  comparisons divisor/multiple
  %--------------------------------

  divisor_smaller: LEMMA divides(p, q) IMPLIES q=0 OR p <= q

  divides_next: LEMMA divides(n, n + 1) IFF n = 1 OR n = -1

  p1: VAR above(1)
  divides_plus_1: LEMMA
    divides(p1, nz) => NOT divides(p1, nz + 1)
  
 END divides


% Modulo arithmetic defines rem and associated properties
% Provided by Bruno Dutertre
modulo_arithmetic : THEORY
 BEGIN
  x, y, z, t, q, i : VAR int
  n0x : VAR nzint
  px, py, b: VAR posnat
  n: VAR nat

  %---------------------
  %  Remainder of x/b
  %---------------------

  rem(b)(x): {r: mod(b) | EXISTS q: x = b * q + r}

  rem_def: LEMMA
     FORALL (r : mod(b)): rem(b)(x) = r IFF EXISTS q: x = b * q + r

  rem_def2: LEMMA
     FORALL (r : mod(b)): rem(b)(x) = r IFF divides(b, x - r)

  rem_def3: LEMMA
     FORALL (r : mod(b)): rem(b)(x) = r IFF divides(b, r - x)


  %------------------------
  %  Remainder for easy x
  %------------------------

  rem_mod: LEMMA FORALL (r : mod(b)): rem(b)(r) = r

  rem_mod2: LEMMA 0 <= x AND x < b IMPLIES rem(b)(x) = x

  rem_zero: LEMMA rem(b)(0) = 0

  rem_self: LEMMA rem(b)(b) = 0

  rem_multiple1: LEMMA rem(b)(b * x) = 0

  rem_multiple2: LEMMA rem(b)(x * b) = 0

  rem_one: LEMMA b /= 1 IMPLIES rem(b)(1) = 1

  rem_minus_one: LEMMA rem(b)(-1) = b-1


  %-------------------------
  %  Congruence properties
  %-------------------------

  same_remainder: LEMMA
     rem(b)(x) = rem(b)(y) IFF divides(b, x - y)


  rem_rem: LEMMA rem(b)(rem(b)(x)) = rem(b)(x)


  rem_sum: LEMMA
     rem(b)(x) = rem(b)(y) AND rem(b)(z) = rem(b)(t) 
        IMPLIES rem(b)(x + z) = rem(b)(y + t)

  rem_sum1: LEMMA rem(b)(rem(b)(x) + y) = rem(b)(x + y)

  rem_sum2: LEMMA rem(b)(x + rem(b)(y)) = rem(b)(x + y)


  rem_diff: LEMMA
     rem(b)(x) = rem(b)(y) AND rem(b)(z) = rem(b)(t)
        IMPLIES rem(b)(x - z) = rem(b)(y - t)

  rem_diff1: LEMMA rem(b)(rem(b)(x) - y) = rem(b)(x - y)

  rem_diff2: LEMMA rem(b)(x - rem(b)(y)) = rem(b)(x - y)



  rem_prod1: LEMMA rem(b)(rem(b)(x) * y) = rem(b)(x * y)

  rem_prod2: LEMMA rem(b)(x * rem(b)(y)) = rem(b)(x * y)

  rem_prod: LEMMA
     rem(b)(x) = rem(b)(y) AND rem(b)(z) = rem(b)(t)
        IMPLIES rem(b)(x * z) = rem(b)(y * t)


  rem_expt: LEMMA
      rem(b)(x) = rem(b)(y) IMPLIES rem(b)(expt(x, n)) = rem(b)(expt(y, n))

  rem_expt1: LEMMA rem(b)(expt(rem(b)(x), n)) = rem(b)(expt(x, n))



  rem_sum_elim1: LEMMA
     rem(b)(x + y) = rem(b)(x + z) IFF rem(b)(y) = rem(b)(z)

  rem_sum_elim2: LEMMA
     rem(b)(y + x) = rem(b)(z + x) IFF rem(b)(y) = rem(b)(z)

  rem_diff_elim1: LEMMA
     rem(b)(x - y) = rem(b)(x - z) IFF rem(b)(y) = rem(b)(z)

  rem_diff_elim2: LEMMA
     rem(b)(y - x) = rem(b)(z - x) IFF rem(b)(y) = rem(b)(z)

  rem_opposite_elim: LEMMA
     rem(b)(- x) = rem(b)(- y) IFF rem(b)(x) = rem(b)(y)

  % Provide a name for the function asserted to exist by euclid_int
  ndiv(x,b) : {q: int | x = b * q + rem(b)(x)}

  ndiv_lt: LEMMA ndiv(x,b) <= x/b

  JUDGEMENT ndiv(n,b) HAS_TYPE upto(n)

  rem_floor: LEMMA FORALL b, x: x = rem(b)(x) + b * floor(x / b)

  rem_base: LEMMA
    FORALL b, x, i, n:
      rem(b)(x) = rem(b + n)(x + i) IFF divides(b + n, i - n * floor(x / b))

  rem_sum_floor: LEMMA
    FORALL b, x, i:
      rem(b)(x + i) = rem(b)(x) + i - b * floor((rem(b)(x) + i) / b)

  rem_sum_assoc: COROLLARY
    FORALL b, x, n: rem(b)(x + n) = rem(b)(x) + n IFF rem(b)(x) < b - n

  rem_add_one: LEMMA
    FORALL b, x:
      rem(b)(x + 1) = rem(b)(x) + 1 OR
       (rem(b)(x) = b - 1 AND rem(b)(x + 1) = 0)

  rem_wrap: LEMMA
    FORALL b, x, (n: below(b)):
      rem(b)(x) < rem(b)(x + n) IFF rem(b)(x) < b - n AND n > 0

  rem_wrap_eq: COROLLARY
    FORALL b, x, (n: below(b)):
      rem(b)(x) <= rem(b)(x + n) IFF rem(b)(x) < b - n OR divides(b, n)

 END modulo_arithmetic


% subrange_induction defines induction schemas for subranges.  This is a
% parameterized theory so that it may be used as a name to the prover
% induction commands.  subrange_induction is the weak form, and
% SUBRANGE_induction is the strong form of induction.

subrange_inductions[i: int, j: upfrom(i)]: THEORY
 BEGIN
  k, m: VAR subrange(i, j)
  p: VAR pred[subrange(i, j)]

  subrange_induction: LEMMA
    (p(i) AND (FORALL k: k < j AND p(k) IMPLIES p(k + 1)))
        IMPLIES (FORALL k: p(k))

  SUBRANGE_induction: LEMMA
    (FORALL k: (FORALL m: m < k IMPLIES p(m)) IMPLIES p(k))
      IMPLIES (FORALL k: p(k))

 END subrange_inductions


% bounded_int_inductions provides the weak and strong forms of induction for
% the various bounded subtypes of int.

bounded_int_inductions[m: int]: THEORY
 BEGIN
  pf: VAR pred[upfrom(m)]
  jf, kf: VAR upfrom(m)

  upfrom_induction: LEMMA
    (pf(m) AND (FORALL jf: pf(jf) IMPLIES pf(jf + 1)))
       IMPLIES (FORALL jf: pf(jf))

  UPFROM_induction: LEMMA
    (FORALL jf: (FORALL kf: kf < jf IMPLIES pf(kf)) IMPLIES pf(jf))
      IMPLIES (FORALL jf: pf(jf))

  pa: VAR pred[above(m)]
  ja, ka: VAR above(m)

  above_induction: LEMMA
    (pa(m+1) AND (FORALL ja: pa(ja) IMPLIES pa(ja + 1)))
      IMPLIES (FORALL ja: pa(ja))

  ABOVE_induction: LEMMA
    (FORALL ja: (FORALL ka: ka < ja IMPLIES pa(ka)) IMPLIES pa(ja))
      IMPLIES (FORALL ja: pa(ja))

 END bounded_int_inductions


% bounded_nat_inductions provides the weak and strong forms of induction for
% the various bounded subtypes of nat.

bounded_nat_inductions[m: nat]: THEORY
 BEGIN
  pt: VAR pred[upto(m)]
  jt, kt: VAR upto(m)

  upto_induction: LEMMA
    (pt(0) AND (FORALL jt: jt < m AND pt(jt) IMPLIES pt(jt + 1)))
      IMPLIES (FORALL jt: pt(jt))

  UPTO_induction: LEMMA
    (FORALL jt: (FORALL kt: kt < jt IMPLIES pt(kt)) IMPLIES pt(jt))
      IMPLIES (FORALL jt: pt(jt))

  pb: VAR pred[below(m)]
  jb, kb: VAR below(m)

  below_induction: LEMMA
    ((m > 0 IMPLIES pb(0))
        AND (FORALL jb: jb < m - 1 AND pb(jb) IMPLIES pb(jb + 1)))
      IMPLIES (FORALL jb: pb(jb))

  BELOW_induction: LEMMA
    (FORALL jb: (FORALL kb: kb < jb IMPLIES pb(kb)) IMPLIES pb(jb))
      IMPLIES (FORALL jb: pb(jb))

 END bounded_nat_inductions


% subrange_type

subrange_type[m, n: int] : THEORY
 BEGIN
  subrange: TYPE = subrange(m, n)
 END subrange_type


% int_types defines some useful subtypes of the integers for
% backward compatibility.

int_types[m: int] : THEORY
 BEGIN
  upfrom: NONEMPTY_TYPE = upfrom(m)
  above:  NONEMPTY_TYPE = above(m)
 END int_types


% nat_types defines some useful subtypes of the natural numbers for
% backward compatibility.

nat_types[m: nat] : THEORY
 BEGIN
  upto:   NONEMPTY_TYPE = upto(m)
  below:  TYPE = below(m)
 END nat_types


nat_fun_props : THEORY
%------------------------------------------------------------------------
%      Author:  Bruno Dutertre 
%
%      Special properties of injective/surgective functions over nats
%------------------------------------------------------------------------

BEGIN

  n, m : VAR nat

  injection_n_to_m: THEOREM
	(EXISTS (f: [below(n) -> below(m)]): injective?(f)) IMPLIES n <= m

  injection_n_to_m_var: THEOREM
	(EXISTS (f: [below(n) -> below(m)]): injective?(f)) IFF n <= m

  surjection_n_to_m: THEOREM
	(EXISTS (f: [below(n) -> below(m)]): surjective?(f)) IMPLIES m <= n

  surjection_n_to_m_var: THEOREM
	(EXISTS (f: [below(n) -> below(m)]): surjective?(f)) IFF 
	    (m > 0 AND m <= n) OR (m = 0 AND n = 0)

  bijection_n_to_m: THEOREM
	(EXISTS (f: [below(n) -> below(m)]): bijective?(f)) IFF n = m


  injection_n_to_m2: THEOREM
	(EXISTS (f: [upto(n) -> upto(m)]): injective?(f)) IFF n <= m

  surjection_n_to_m2: THEOREM
	(EXISTS (f: [upto(n) -> upto(m)]): surjective?(f)) IFF m <= n

  bijection_n_to_m2: THEOREM
	(EXISTS (f: [upto(n) -> upto(m)]): bijective?(f)) IFF n = m


  surj_equiv_inj: THEOREM
	FORALL (f: [below(n) -> below(n)]): surjective?(f) IFF injective?(f)
	
  inj_equiv_bij: THEOREM
	FORALL (f: [below(n) -> below(n)]): bijective?(f) IFF injective?(f)

  surj_equiv_bij: THEOREM
	FORALL (f: [below(n) -> below(n)]): bijective?(f) IFF surjective?(f)


  surj_equiv_inj2: THEOREM
	FORALL (f: [upto(n) -> upto(n)]): surjective?(f) IFF injective?(f)
	
  inj_equiv_bij2: THEOREM
	FORALL (f: [upto(n) -> upto(n)]): bijective?(f) IFF injective?(f)

  surj_equiv_bij2: THEOREM
	FORALL (f: [upto(n) -> upto(n)]): bijective?(f) IFF surjective?(f)

END nat_fun_props


%------------------------------------------------------------------------
%
%  finite sets (basic definitions and closure properties)
%  -----------------------------------------------------
%      Authors:  Damir Jamsek
%                Ricky W. Butler
%                Sam Owre
%                C. Michael Holloway
%
%  This theory defines finite sets as the subtype of sets[T] that
%  satisfy the predicate "is_finite".  This predicate states
%  that there is an injective function into below[N] for some N.
%
%------------------------------------------------------------------------
%
% finite_sets_def, card_def, and finite_sets are combined here to make
% things a bit more backward compatible.  These were all originally
% part of the finite_sets library.

finite_sets[T: TYPE]: THEORY
% beginning of original finite_sets_def theory
 BEGIN
  x, y, z: VAR T
  s: VAR set[T]
  N: VAR nat

  is_finite(s): bool = (EXISTS N, (f: [(s) -> below[N]]):
                          injective?(f)) 

  finite_set: TYPE = (is_finite) CONTAINING emptyset[T]

  non_empty_finite_set: TYPE = {s: finite_set | NOT empty?(s)}

  is_finite_surj: LEMMA (EXISTS (N: nat), (f: [below[N] -> (s)]):
                            surjective?(f)) IFF is_finite(s) 


  A, B: VAR finite_set
  NA, NB: VAR non_empty_finite_set

  finite_subset:       LEMMA subset?(s,A) IMPLIES is_finite(s)
  finite_intersection: LEMMA is_finite(intersection(A,B))
  finite_add:          LEMMA is_finite(add(x,A))

  % -------- Judgements --------------------------------------------------

  nonempty_finite_is_nonempty: JUDGEMENT
    non_empty_finite_set SUBTYPE_OF (nonempty?[T])

  finite_singleton: JUDGEMENT singleton(x) HAS_TYPE finite_set

  finite_union: JUDGEMENT union(A, B) HAS_TYPE finite_set
  finite_intersection1: JUDGEMENT intersection(s, A) HAS_TYPE finite_set
  finite_intersection2: JUDGEMENT intersection(A, s) HAS_TYPE finite_set
  finite_difference: JUDGEMENT difference(A, s) HAS_TYPE finite_set

  nonempty_finite_union1: JUDGEMENT union(NA, B) HAS_TYPE non_empty_finite_set

  nonempty_finite_union2: JUDGEMENT union(A, NB) HAS_TYPE non_empty_finite_set

  nonempty_add_finite: JUDGEMENT add(x, A) HAS_TYPE non_empty_finite_set

  finite_remove: JUDGEMENT remove(x, A) HAS_TYPE finite_set

  finite_rest: JUDGEMENT rest(A) HAS_TYPE finite_set

  finite_emptyset: JUDGEMENT emptyset HAS_TYPE finite_set

  nonempty_singleton_finite: JUDGEMENT
   singleton(x) HAS_TYPE non_empty_finite_set


  % -------- Base type is finite -----------------------------------------

  is_finite_type: bool = (EXISTS N, (g:[T -> below[N]]): injective?(g))

  finite_full:         LEMMA is_finite_type IFF is_finite(fullset[T])
  finite_type_set:     LEMMA is_finite_type IMPLIES is_finite(s)
  finite_complement:   LEMMA is_finite_type IMPLIES is_finite(complement(s))

% end of original finite_sets_def

% beginning of original card_def theory

%------------------------------------------------------------------------
%
%  Fundamental definition of card
%
%      Authors:  Bruno Dutertre 
%                Ricky W. Butler
%------------------------------------------------------------------------

  S, S2: VAR finite_set
  n, m: VAR nat
  p : VAR posnat

  inj_set(S): (nonempty?[nat]) = 
                 { n | EXISTS (f : [(S)->below[n]]) : injective?(f) }

  Card(S): nat = min(inj_set(S))

  inj_Card    : LEMMA Card(S) = n IMPLIES 
                          (EXISTS (f : [(S) -> below[n]]) : injective?(f))

  reduce_inj  : LEMMA (FORALL (f : [(S)->below[p]]) :
                          injective?(f) AND NOT surjective?(f) IMPLIES 
                              (EXISTS (g: [(S)->below[p-1]]): injective?(g)))

  Card_injection: LEMMA (EXISTS (f : [(S)->below[n]]) : injective?(f)) 
                            IMPLIES Card(S) <= n
  
  Card_surjection : LEMMA (EXISTS (f : [(S)->below[n]]) : surjective?(f)) 
                              IMPLIES n <= Card(S) 
        
  Card_bijection : THEOREM
        Card(S) = n IFF (EXISTS (f : [(S)->below[n]]) : bijective?(f))

  Card_disj_union: THEOREM disjoint?(S,S2) IMPLIES 
                              Card(union(S,S2)) = Card(S) + Card(S2)

% ------------------------------------------------------------------------
  card(S): {n: nat| n = Card(S)}               % inhibit expansion

  card_def        : THEOREM card(S) = Card(S)  % But if you really need to

% end of original card_def theory

% beginning of original finite_sets theory 

  card_emptyset   : THEOREM card(emptyset[T]) = 0

  empty_card      : THEOREM empty?(S) IFF card(S) = 0

  card_empty?     : THEOREM (card(S) = 0) = empty?(S)

  card_is_0       : THEOREM (card(S) = 0) = (S = emptyset)

  nonempty_card   : THEOREM nonempty?(S) IFF card(S) > 0

  card_singleton  : THEOREM card(singleton(x)) = 1

  card_one        : THEOREM card(S) = 1 IFF (EXISTS x : S = singleton(x))

  card_disj_union : THEOREM disjoint?(A,B) IMPLIES 
                              card(union(A,B)) = card(A) + card(B)

  card_diff_subset: THEOREM subset?(A, B) IMPLIES 
                                  card(difference(B, A)) = card(B) - card(A)

  card_subset     : THEOREM subset?(A,B) IMPLIES card(A) <= card(B)

  card_plus       : THEOREM card(A) + card(B) = 
                                card(union(A, B)) + card(intersection(A,B))  

  card_union      : THEOREM card(union(A,B)) = card(A) + card(B) -
                                               card(intersection(A,B))

  card_add        : THEOREM card(add(x, S)) = card(S) 
                                                   + IF S(x) THEN 0 ELSE 1 ENDIF
  card_add_gt0    : THEOREM card(add(x,S)) > 0

  card_remove     : THEOREM card(remove(x, S)) = card(S)
                                                   - IF S(x) THEN 1 ELSE 0 ENDIF

  card_rest       : THEOREM NOT empty?(S) IMPLIES card(rest(S)) = card(S) - 1

  same_card_subset: THEOREM subset?(A, B) AND card(A) = card(B) 
                               IMPLIES A = B

  smaller_card_subset : THEOREM subset?(A, B) AND card(A) < card(B) IMPLIES
                                 (EXISTS x : member(x, B) AND NOT member(x, A))

  card_strict_subset: THEOREM strict_subset?(A,B) IMPLIES card(A) < card(B)

  card_1_has_1    : THEOREM card(S) >= 1 IMPLIES (EXISTS (x: T): S(x))

  card_2_has_2    : THEOREM card(S) >= 2 IMPLIES
                              (EXISTS (x,y: T): x /= y AND S(x) AND S(y))

  card_intersection_le: THEOREM card(intersection(A,B)) <= card(A) AND
                              card(intersection(A,B)) <= card(B)

  card_bij        : THEOREM card(S) = N
                             IFF (EXISTS (f: [(S) -> below[N]]): bijective?(f))

  card_bij_inv    : THEOREM card(S) = N
                             IFF (EXISTS (f: [below[N] -> (S)]): bijective?(f))

  bij_exists      : COROLLARY (EXISTS (f: [(S) -> below(card(S))]):
                                       bijective?(f))

  bij(S: finite_set): {f:[(S) -> below(card(S))] | bijective?(f)}

  ibij(S: non_empty_finite_set): {f:[below(card(S)) -> (S)] | bijective?(f)} =
       inverse(bij(S))

  bij_ibij: LEMMA FORALL (S: non_empty_finite_set, ii: below(card(S))):
      bij(S)(ibij(S)(ii)) = ii

  ibij_bij: LEMMA FORALL (S: non_empty_finite_set, x:T):
      S(x) IMPLIES ibij(S)(bij(S)(x)) = x

  is_finite_exists_N: LEMMA FORALL (g: [below[N] -> T]):
            is_finite({r: T | EXISTS (n: below[N]): r = g(n)})

%  card_n_has_n    : THEOREM card(S) >= n IMPLIES
%                              (EXISTS (X: [below[N] -> T]):
%                                   (FORALL (i: below[N]): S(X(i))) AND
%                                   (FORALL (i,j: below[N]): X(i) /= X(j)))

  P, P1, P2: VAR pred[T]

  finite_pred: LEMMA is_finite(fullset[T]) IMPLIES
                        is_finite[T]({x: T | P(x)})

  finite_pred2:  LEMMA is_finite(P) IMPLIES
                         is_finite[T]({x: T | P(x)})

  card_implies: LEMMA is_finite(fullset[T]) AND
                      (FORALL (x: T): P1(x) IMPLIES P2(x)) 
             IMPLIES card({x: T | P1(x)}) <= card({x: T | P2(x)})

  finite_induction: THEOREM
    FORALL (p: pred[set[T]]):
      (FORALL (n: nat), (S: set[T]):
         (EXISTS (f: [(S) -> below[n]]): injective?(f)) => p(S))
       => (FORALL (FS: finite_set): p(FS))
               
END finite_sets


% Courtesy Jerry James
restrict_set_props[T: TYPE, S: TYPE FROM T]: THEORY
 BEGIN

  restrict_finite: LEMMA
    FORALL (a: set[T]): is_finite(a) => is_finite(restrict[T, S, bool](a))

  finite_restrict: JUDGEMENT
    restrict[T, S, bool](a: finite_set[T]) HAS_TYPE finite_set[S]

  empty_restrict: JUDGEMENT
    restrict[T, S, bool](a: (empty?[T])) HAS_TYPE (empty?[S])

  card_restrict: LEMMA
    FORALL (a: finite_set[T]): card(restrict[T, S, bool](a)) <= card(a)

 END restrict_set_props


% Courtesy Jerry James
extend_set_props[T: TYPE, S: TYPE FROM T]: THEORY
 BEGIN

  finite_extension: LEMMA
    FORALL (a: set[S]):
      is_finite(extend[T, S, bool, FALSE](a)) IFF is_finite(a)

  finite_extend: JUDGEMENT
    extend[T, S, bool, FALSE](a: finite_set[S]) HAS_TYPE finite_set[T]

  empty_extend: JUDGEMENT
    extend[T, S, bool, FALSE](a: (empty?[S])) HAS_TYPE (empty?[T])

  nonempty_extend: JUDGEMENT
    extend[T, S, bool, FALSE](a: (nonempty?[S])) HAS_TYPE (nonempty?[T])

  singleton_extend: JUDGEMENT
    extend[T, S, bool, FALSE](a: (singleton?[S])) HAS_TYPE (singleton?[T])

  card_extend: LEMMA
    FORALL (a: finite_set[S]): card(extend[T, S, bool, FALSE](a)) = card(a)

  empty?_extend: LEMMA
    FORALL (a: set[S]): 
      empty?(extend[T, S, bool, FALSE](a)) IFF empty?(a)

  nonempty?_extend: LEMMA
    FORALL (a: set[S]): 
      nonempty?(extend[T, S, bool, FALSE](a)) IFF nonempty?(a)

  singleton?_extend: LEMMA
    FORALL (a: set[S]): 
      singleton?(extend[T, S, bool, FALSE](a)) IFF singleton?(a)

  subset_extend: LEMMA
    FORALL (a, b: set[S]): 
      subset?(extend[T, S, bool, FALSE](a), extend[T, S, bool, FALSE](b)) IFF
         subset?(a, b)

  union_extend: LEMMA
    FORALL (a, b: set[S]): 
      union(extend[T, S, bool, FALSE](a), extend[T, S, bool, FALSE](b))
        = extend[T, S, bool, FALSE](union(a, b))

  intersection_extend: LEMMA
    FORALL (a, b: set[S]): 
      intersection(extend[T, S, bool, FALSE](a), extend[T, S, bool, FALSE](b))
        = extend[T, S, bool, FALSE](intersection(a, b))

  difference_extend: LEMMA
    FORALL (a, b: set[S]): 
      difference(extend[T, S, bool, FALSE](a), extend[T, S, bool, FALSE](b))
        = extend[T, S, bool, FALSE](difference(a, b))

  add_extend: LEMMA
    FORALL (x: S, a: set[S]): 
      add(x, extend[T, S, bool, FALSE](a))
        = extend[T, S, bool, FALSE](add(x, a))

  remove_extend: LEMMA
    FORALL (x: S, a: set[S]): 
      remove(x, extend[T, S, bool, FALSE](a))
        = extend[T, S, bool, FALSE](remove(x, a))

 END extend_set_props


%-------------------------------------------------------------------------
%
%  Additions to the function_image theory.  These additions
%  show that the image of a finite set is finite, and that any injective
%  function is bijective with its image.
%
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%-------------------------------------------------------------------------
function_image_aux[D: TYPE, R: TYPE]: THEORY
 BEGIN

  S: VAR finite_set[D]
  f: VAR [D -> R]
  inj: VAR (injective?[D, R])

  finite_image: JUDGEMENT image(f, S) HAS_TYPE finite_set[R]

  card_image: LEMMA FORALL f, S: card(image(f, S)) <= card(S)

  card_injective_image: LEMMA FORALL inj, S: card(image(inj, S)) = card(S)

  bijective_image: LEMMA
    FORALL inj: bijective?[D, (image(inj, fullset[D]))](inj)

 END function_image_aux


% function_iterate provides the iterate function, which composes a
% function with itself a specified number of times.  The function must
% have the same domain and range.  Two useful properties of iterate are
% also provided.

function_iterate[T: TYPE]: THEORY
 BEGIN
  f: VAR [T -> T]
  m, n: VAR nat
  x: VAR T

  iterate(f, n)(x): RECURSIVE T =
    IF n = 0 THEN x ELSE f(iterate(f, n-1)(x)) ENDIF
    MEASURE n

  iterate_add: LEMMA
    iterate(f, m) o iterate(f, n) = iterate(f, m + n)

  iterate_add_applied: LEMMA 
    iterate(f,m)(iterate(f, n)(x)) = iterate(f, m + n)(x)

  iterate_add_one: LEMMA 
    iterate(f, n)(f(x)) = iterate(f, n+1)(x)

  iterate_mult: LEMMA
    iterate(iterate(f, m), n) = iterate(f, m * n)

  iterate_invariant: LEMMA
    f(iterate(f, n)(x)) = iterate(f, n)(f(x))
  
 END function_iterate


% sequences provides the polymorphic sequence type, as a function from
% nat to the base type.  The usual sequence functions are also provided.
% Note that these are infinite sequences, and do not contain finite
% sequences as a subtype.

sequences[T: TYPE]: THEORY
 BEGIN

  sequence: TYPE = [nat->T]
  i, n: VAR nat
  x: VAR T
  p: VAR pred[T]
  seq: VAR sequence
  Trel: VAR PRED[[T, T]]

  nth(seq, n): T = seq(n)

  suffix(seq, n): sequence =
    (LAMBDA i: seq(i+n))

  first(seq): T = nth(seq, 0)

  rest(seq): sequence = suffix(seq, 1)

  delete(n, seq): sequence =
    (LAMBDA i: (IF i < n THEN seq(i) ELSE seq(i + 1) ENDIF))

  insert(x, n, seq): sequence =
    (LAMBDA i: (IF i < n THEN seq(i)
                ELSIF i = n THEN x
                ELSE seq(i - 1) ENDIF))

  add(x, seq): sequence = insert(x, 0, seq)

  insert_delete: LEMMA insert(nth(seq, n), n, delete(n, seq)) = seq

  add_first_rest: LEMMA add(first(seq), rest(seq)) = seq

  every(p)(seq): bool = (FORALL n: p(nth(seq, n)))

  every(p, seq): bool = (FORALL n: p(nth(seq, n)))

  some(p)(seq): bool = (EXISTS n: p(nth(seq, n)))

  some(p, seq): bool = (EXISTS n: p(nth(seq, n)))

  sequence_induction: LEMMA
    p(nth(seq, 0)) AND (FORALL n: p(nth(seq, n)) IMPLIES p(nth(seq, n + 1)))
      IMPLIES every(p)(seq)

  ascends?(seq, Trel): bool = preserves(seq, (LAMBDA i, n: i <= n), Trel)

  descends?(seq, Trel): bool = inverts(seq, (LAMBDA i, n: i <= n), Trel)

 END sequences


% seq_functions defines the map function that generates the image of a
% sequence under a function.

seq_functions[D, R: TYPE]: THEORY
 BEGIN
  f: VAR [D -> R]
  s: VAR sequence[D]
  n: VAR nat

  map(f)(s): sequence[R] = (LAMBDA n: f(nth(s, n)))

  map(f, s): sequence[R] = (LAMBDA n: f(nth(s, n)))

 END seq_functions


% This theory defines finite sequences as a dependent type.  Two finite
% sequences are concatenated with the operator 'o', and a subsequence can be
% extracted with the operator '^'.  Note that ^ allows any natural numbers
% m and n to define the range; if m > n then the empty sequence is returned

finite_sequences [T: TYPE]: THEORY
 BEGIN
  finite_sequence: TYPE = [# length: nat, seq: [below[length] -> T] #]
  finseq: TYPE = finite_sequence

  fs, fs1, fs2, fs3: VAR finseq
  m, n: VAR nat

  empty_seq: finseq =
    (# length := 0,
       seq := (LAMBDA (x: below[0]): epsilon! (t:T): true) #)

  finseq_appl(fs): [below[length(fs)] -> T] = fs`seq;

  CONVERSION finseq_appl;

  o(fs1, fs2): finseq =
     LET l1 = fs1`length,
         lsum = l1 + fs2`length
      IN (# length := lsum,
            seq := (LAMBDA (n:below[lsum]):
                      IF n < l1
                         THEN fs1`seq(n)
                         ELSE fs2`seq(n-l1)
                      ENDIF) #);

  p: VAR [nat, nat]

  ^(fs, p): finseq =
    LET (m, n) = p
     IN IF m > n OR m >= fs`length
        THEN empty_seq
        ELSE LET len = min(n - m + 1, fs`length - m)
              IN (# length := len,
                    seq := (LAMBDA (x: below[len]): fs`seq(x + m)) #)
        ENDIF;

  % This is the same as above, but returns domain [m..n-1] rather than [m..n]
  % More generally useful, but the above is kept for backward compatibility
  ^^(fs, p): finseq =
    LET (m, n) = p
     IN IF m >= n OR m >= fs`length
        THEN empty_seq
        ELSE LET len = min(n - m, fs`length - m)
              IN (# length := len,
                    seq := (LAMBDA (x: below[len]): fs`seq(x + m)) #)
        ENDIF

  extract1(fs:{fs | fs`length = 1}): T = fs`seq(0)

  CONVERSION extract1

  o_assoc: LEMMA fs1 o (fs2 o fs3) = (fs1 o fs2) o fs3

 END finite_sequences


more_finseq [T: TYPE]: THEORY
  BEGIN
   seq: TYPE = finseq[T]

   rr, ss, tt: VAR seq

   x, y, z: VAR T

   prefix?(rr, ss): bool =
     rr`length <= ss`length AND
       (FORALL (i: below(rr`length)): rr`seq(i) = ss`seq(i))

   prefix_closed?(X : set[seq]): bool =
     FORALL ss: X(ss) IMPLIES (FORALL (rr | prefix?(rr, ss)): X(rr))

   add(x, rr): finseq[T] =
     rr WITH [`length := rr`length + 1,
              `seq(rr`length) := x]

  END more_finseq


% ordstruct provides the building blocks for defining the
% ordinals up to epsilon_0.

ordstruct: DATATYPE
 BEGIN
  zero: zero?
  add(coef: posnat, exp: ordstruct, rest: ordstruct): nonzero?
 END ordstruct


% ordinals uses the ordstruct datatype to define the ordinals up to
% epsilon_0, by providing an ordering on ordstruct and defining the
% ordinals to be those elements of type ordstruct that are in a
% Cantor normal form with respect to the ordering.  Thus
%    add(i, u, v) = (omega^u)*i + v
%    add(i, u, add(j, v, w)) = (omega^u)*i + (omega^v)*j + w, where u>v.  

ordinals: THEORY
 BEGIN
  i, j, k: VAR posnat
  m, n, o: VAR nat
  u, v, w, x, y, z: VAR ordstruct
  size: [ordstruct->nat] = reduce[nat](0, (LAMBDA i, m, n: 1 + m+n));

  <(x, y): RECURSIVE bool =
     CASES x OF
        zero: NOT zero?(y),
        add(i, u, v): CASES y OF
                        zero: FALSE,
                        add(j, z, w): (u<z) OR
                                      (u=z) AND (i<j) OR
                                      (u=z) AND (i=j) AND (v<w)
                      ENDCASES
     ENDCASES
   MEASURE size(x);

  >(x, y): bool = y < x;
  <=(x, y): bool = x < y OR x = y;
  >=(x, y): bool = y < x OR y = x

  ordinal?(x): RECURSIVE bool =
    CASES x OF
      zero: TRUE,
      add(i, u, v): (ordinal?(u) AND ordinal?(v) AND 
                      CASES v OF
                        zero: TRUE,
                        add(k, r, s): r < u
                      ENDCASES)
    ENDCASES
   MEASURE size

  ordinal: NONEMPTY_TYPE = (ordinal?)

  r, s, t: VAR ordinal
  
  ordinal_irreflexive: LEMMA NOT r < r

  ordinal_antisym: LEMMA r < s IMPLIES NOT s < r

  ordinal_antisymmetric: LEMMA r <= s AND s <= r IMPLIES r = s

  ordinal_transitive: LEMMA r < s AND s < t IMPLIES r < t

  ordinal_trichotomy: LEMMA r < s OR r = s OR s < r

  p: VAR pred[ordinal]

  ordinal_induction: AXIOM
    (FORALL r: (FORALL s: s < r IMPLIES p(s)) IMPLIES p(r))
      IMPLIES (FORALL r: p(r))

  well_founded_le: LEMMA
    well_founded?(LAMBDA (r, s: (ordinal?)): r < s)

 END ordinals


% lex2 provides a lexical ordering for pairs of natural numbers.
% This illustrates the use of ordinals.

lex2: THEORY
  BEGIN

  i, j, m, n: VAR nat

  lex2(m, n): ordinal = 
    (IF m=0
       THEN IF n = 0
               THEN zero
               ELSE add(n, zero, zero)
            ENDIF
       ELSIF n = 0 THEN add(m, add(1,zero,zero),zero)
       ELSE add(m, add(1,zero,zero), add(n,zero, zero))
     ENDIF)

  lex2_lt: LEMMA
    lex2(i, j) < lex2(m, n) =
     (i < m OR (i = m AND j < n))

 END lex2


% list provides the datatype definition for lists.

list [T: TYPE]: DATATYPE 
 BEGIN
  null: null?
  cons (car: T, cdr:list):cons?

 END list


% list_props provides the length, append, and reverse functions.
% These could have been defined using the reduce function generated
% for the list datatype, but this is harder to work with in an
% interactive proof.

list_props [T: TYPE]: THEORY
 BEGIN
  l, l1, l2, l3: VAR list[T]
  x: VAR T
  P, Q: VAR PRED[T]

  length(l): RECURSIVE nat =
    CASES l OF
      null: 0,
      cons(x, y): length(y) + 1
    ENDCASES
   MEASURE reduce_nat(0, (LAMBDA (x: T), (n: nat): n + 1))

  member(x, l): RECURSIVE bool =
    CASES l OF
      null: FALSE,
      cons(hd, tl): x = hd OR member(x, tl)
    ENDCASES
   MEASURE length(l)

  member_null: LEMMA member(x, l) IMPLIES NOT null?(l)

  nth(l, (n:below[length(l)])): RECURSIVE T =
    IF n = 0 THEN car(l) ELSE nth(cdr(l), n-1) ENDIF
   MEASURE length(l)

  append(l1, l2): RECURSIVE list[T] =
    CASES l1 OF
      null: l2,
      cons(x, y): cons(x, append(y, l2))
    ENDCASES
    MEASURE length(l1)

  reverse(l): RECURSIVE list[T] =
    CASES l OF
      null: l,
      cons(x, y): append(reverse(y), cons(x, null))
    ENDCASES
    MEASURE length

  append_null: LEMMA append(l, null) = l

  append_assoc: LEMMA
     append(append(l1, l2), l3) = append(l1, append(l2, l3))

  reverse_append: LEMMA
    reverse(append(l1, l2)) = append(reverse(l2), reverse(l1))

  reverse_reverse: LEMMA reverse(reverse(l)) = l

  length_append: LEMMA length(append(l1, l2)) = length(l1) + length(l2)

  length_reverse: LEMMA length(reverse(l)) = length(l)

  a, b, c: VAR T

  list_rep: LEMMA (: a, b, c :) = cons(a, cons(b, cons(c, null)))

  every_append: LEMMA
    every(P)(append(l1, l2)) IFF (every(P)(l1) AND every(P)(l2))

  every_disjunct1: LEMMA
    every(P)(l) IMPLIES every(LAMBDA (x: T): P(x) OR Q(x))(l)

  every_disjunct2: LEMMA
    every(Q)(l) IMPLIES every(LAMBDA (x: T): P(x) OR Q(x))(l)

  every_conjunct: LEMMA
    every(LAMBDA (x: T): P(x) AND Q(x))(l) => (every(P)(l) AND every(Q)(l))

  every_conjunct2: LEMMA
    (every(P)(l) AND every(Q)(l)) => every(LAMBDA (x: T): P(x) AND Q(x))(l)

  every_member: LEMMA every({c: T | member(c, l)})(l)

  every_nth: LEMMA
      every(P)(l) IFF FORALL (i:below(length(l))): P(nth(l,i))

 END list_props


% map_props gives the commutativity properties of composition and map,
% for both sequences and lists.

map_props [T1, T2, T3: TYPE]: THEORY
 BEGIN
  f1: VAR [T1 -> T2]
  f2: VAR [T2 -> T3]
  s: VAR sequence[T1]
  l: VAR list[T1]

  map_list_composition: LEMMA map(f2)(map(f1)(l)) = map(f2 o f1)(l)

  map_seq_composition: LEMMA map(f2)(map(f1)(s)) = map(f2 o f1)(s)

 END map_props

more_map_props [T1, T2: TYPE]: THEORY
 BEGIN
  f: VAR [T1 -> T2]
  l: VAR list[T1]

  map_length: LEMMA length(map(f)(l)) = length(l)

  map_nth_rw: LEMMA
    FORALL (i: below(length(l))):
      nth(map(f)(l), i) = f(nth(l, i))

END more_map_props


% filters defines filter functions for sets and lists, which take a set
% (list) and a predicate and return the set (list) of those elements
% that satisfy the predicate.  Both the curried and uncurried forms are
% given.  Note that filter on lists could be defined using reduce, but
% becomes harder to work with in an interactive proof.

filters[T: TYPE]: THEORY
 BEGIN
  s: VAR set[T]
  l: VAR list[T]
  p: VAR pred[T]
  
  filter(s, p): set[T] = {x: T | s(x) & p(x)}

  filter(p)(s): set[T] = {x: T | s(x) & p(x)}

  filter(l, p): RECURSIVE list[T] =
    CASES l OF
      null: null,
      cons(x, y): IF p(x) THEN cons(x, filter(y, p)) ELSE filter(y, p) ENDIF
    ENDCASES
    MEASURE length(l)

  filter(p)(l): RECURSIVE list[T] =
    CASES l OF
      null: null,
      cons(x, y): IF p(x) THEN cons(x, filter(p)(y)) ELSE filter(p)(y) ENDIF
    ENDCASES
    MEASURE length(l)
 END filters


% list2finseq

list2finseq[T: TYPE]: THEORY
 BEGIN
  l: VAR list[T]
  fs: VAR finseq[T]
  n: VAR nat

  list2finseq(l): finseq[T] =
    (# length := length(l),
       seq := (LAMBDA (x: below[length(l)]): nth(l, x)) #)

  finseq2list_rec(fs, (n: nat | n <= length(fs))): RECURSIVE list[T] =
    IF n = 0
       THEN null
       ELSE cons(fs`seq(length(fs) - n),
                 finseq2list_rec(fs, n-1))
    ENDIF
    MEASURE n

  finseq2list(fs): list[T] = finseq2list_rec(fs, length(fs))

  CONVERSION list2finseq, finseq2list

 END list2finseq


% list2set

list2set[T:TYPE]: THEORY
 BEGIN
  l: VAR list[T]
  x: VAR T

  list2set(l) : RECURSIVE set[T] =
    CASES l OF
      null: emptyset[T],
      cons(x, y): add(x, list2set(y))
    ENDCASES
   MEASURE length

  CONVERSION list2set

 END list2set


% The disjointness theory defines the pairwise_disjoint? function.
% This is used in generating the disjointness axiom for large datatypes
% or enumeration types.  This is because for N constructors, N(N-1)/2
% terms need to be constructed.  Thus care must be taken if the list
% is longer than a few hundred elements.

disjointness: THEORY
 BEGIN
  l: VAR list[bool]
  pairwise_disjoint?(l): RECURSIVE boolean =
    cases l of
      null: true,
      cons(x,y): every(LAMBDA (z:bool): NOT (x AND z))(y)
                  AND pairwise_disjoint?(y)
    endcases
   MEASURE length(l)
 END disjointness


% characters - this follows the ASCII control codes, of which only the
% first 128 are defined:
%
%     |  0 NUL|  1 SOH|  2 STX|  3 ETX|  4 EOT|  5 ENQ|  6 ACK|  7 BEL|
%     |  8 BS |  9 HT | 10 NL | 11 VT | 12 NP | 13 CR | 14 SO | 15 SI |
%     | 16 DLE| 17 DC1| 18 DC2| 19 DC3| 20 DC4| 21 NAK| 22 SYN| 23 ETB|
%     | 24 CAN| 25 EM | 26 SUB| 27 ESC| 28 FS | 29 GS | 30 RS | 31 US |
%     | 32 SP | 33  ! | 34  " | 35  # | 36  $ | 37  % | 38  & | 39  ' |
%     | 40  ( | 41  ) | 42  * | 43  + | 44  , | 45  - | 46  . | 47  / |
%     | 48  0 | 49  1 | 50  2 | 51  3 | 52  4 | 53  5 | 54  6 | 55  7 |
%     | 56  8 | 57  9 | 58  : | 59  ; | 60  < | 61  = | 62  > | 63  ? |
%     | 64  @ | 65  A | 66  B | 67  C | 68  D | 69  E | 70  F | 71  G |
%     | 72  H | 73  I | 74  J | 75  K | 76  L | 77  M | 78  N | 79  O |
%     | 80  P | 81  Q | 82  R | 83  S | 84  T | 85  U | 86  V | 87  W |
%     | 88  X | 89  Y | 90  Z | 91  [ | 92  \ | 93  ] | 94  ^ | 95  _ |
%     | 96  ` | 97  a | 98  b | 99  c |100  d |101  e |102  f |103  g |
%     |104  h |105  i |106  j |107  k |108  l |109  m |110  n |111  o |
%     |112  p |113  q |114  r |115  s |116  t |117  u |118  v |119  w |
%     |120  x |121  y |122  z |123  { |124  | |125  } |126  ~ |127 DEL|

character: DATATYPE
 BEGIN
  char(code:below[256]):char?
 END character


% strings - the strings theory introduces the char type and represents
% strings as a finite sequence of chars.  The lemmas are useful for
% rewriting.  This theory is useful to auto-rewrite with, but make sure
% that list2finseq is not also an auto-rewrite rule.
%
% strings are input as a sequence of characters between double
% quotes.  The \ is an escape character, whose value depends on the
% following character(s).  \" and \\ are used to embed a " and \ in a string.
% A \0 followed by an octal number (< 0400), a \ followed by 
% a decimal number (< 256) or a \x or \X followed by a
% hexidecimal number (< FF) represents that character number. 
% Decimal numbers must be written without leading zeros, as 
% otherwise they will get interpreted as octal (for instance 
% "\065" = "\53" = "\x35"). If the character following such an escape 
% is a digit one has to use the maximal number of digits in the escape 
% (for instance "\00530" = "50" while "\0530" is illegal). Therefore, 
% if one wants to put escape (\27) followed by a 0 into a string one 
% has to use two escapes ("\27\30") or an octal or hex escape 
% ("\00330" = "\x1b0") because \270 is illegal (270 > 255) and 
% \027 is interpreted as octal.
% The other possibilities are:
%  \a  - 007 (C-g, Bell)
%  \b  - 008 (C-h, Backspace)
%  \t  - 009 (C-i, Tab)
%  \n  - 010 (C-j, Newline)
%  \v  - 011 (C-k, VT)
%  \f  - 012 (C-l, Newpage)
%  \r  - 013 (C-m, Return)

strings: THEORY
 BEGIN
  char: TYPE = (char?)
  string: TYPE = finite_sequence[char]

  l1, l2: VAR list[char]

  c1, c2: VAR char

  fseq_lem: LEMMA
    (list2finseq(l1) = list2finseq(l2)) = (l1 = l2)

  cons_lem: LEMMA (cons(c1,l1) = cons(c2,l2)) = (c1 = c2 & l1 = l2)

  char_lem: LEMMA (c1 = c2) = (code(c1) = code(c2))
 END strings


lift[T: TYPE]: DATATYPE
 BEGIN
  bottom: bottom?
  up(down: T): up?
 END lift


union[T1, T2: TYPE]: DATATYPE
 BEGIN
  inl(left: T1): inl?
  inr(right: T2): inr?
 END union


% Defines fixpoints for sets, needed to support the mucalculus model checker.

mucalculus[T:TYPE]: THEORY
 BEGIN

  s: VAR T
  p, p1, p2: VAR pred[T]
  predicate_transformer: TYPE = [pred[T]->pred[T]]
  pt: VAR predicate_transformer
  setofpred: VAR pred[pred[T]]

  <=(p1,p2): bool = FORALL s: p1(s) IMPLIES p2(s)

  monotonic?(pt): bool =
      FORALL p1, p2: p1 <= p2 IMPLIES pt(p1) <= pt(p2)

  pp: VAR (monotonic?)

  fixpoint?(pp, p): bool = (pp(p) = p)

  fixpoint?(pp)(p): bool = fixpoint?(pp, p)

  glb(setofpred): pred[T] =
      LAMBDA s: (FORALL p: member(p,setofpred) IMPLIES p(s))

  % least fixpoint
  lfp(pp): pred[T] = glb({p | pp(p) <= p})

  lfp_induction: FORMULA pp(p) <= p IMPLIES lfp(pp) <= p

  mu(pp): pred[T] = lfp(pp)

  lfp?(pp, p1): bool =
    fixpoint?(pp, p1) AND FORALL p2: fixpoint?(pp,p2) IMPLIES p1 <= p2

  lfp?(pp)(p1): bool = lfp?(pp, p1)

  lub(setofpred): pred[T] = LAMBDA s: EXISTS p: member(p,setofpred) AND p(s)

  % greatest fixpoint
  gfp(pp): pred[T] = lub({p | p <= (pp(p))})

  gfp_induction: FORMULA p <= pp(p) IMPLIES p <= gfp(pp)

  nu(pp): pred[T] = gfp(pp)

  gfp?(pp, p1): bool =
    fixpoint?(pp,p1) AND FORALL p2: fixpoint?(pp,p2) IMPLIES p2 <= p1

  gfp?(pp)(p1): bool = gfp?(pp, p1)

 END mucalculus


% Basic CTL temporal operators (without fairness) defined in mu-calculus

ctlops[state : TYPE]: THEORY
 BEGIN
  u,v,w: VAR state
  f,g,Q,P,p1,p2: VAR pred[state]
  Z: VAR pred[[state, state]]

  N: VAR [state, state -> bool]

  CONVERSION+ K_conversion

  EX(N,f)(u):bool = (EXISTS v: (f(v) AND N(u, v)))

  EG(N,f):pred[state] = nu(LAMBDA Q: (f AND EX(N,Q)))

  EU(N,f,g):pred[state] = mu(LAMBDA Q: (g OR (f AND EX(N,Q))))

  % Other operator definitions
  EF(N,f):pred[state] = EU(N, TRUE, f)
  AX(N,f):pred[state] = NOT EX(N, NOT f)
  AF(N,f):pred[state] = NOT EG(N, NOT f)
  AG(N,f):pred[state] = NOT EF(N, NOT f)
  AU(N,f,g):pred[state] = NOT EU(N, NOT g, (NOT f AND NOT g)) AND AF(N, g)

  CONVERSION- K_conversion
 END ctlops


% Fair versions of CTL operators where
% fairAG(N, f)(Ff)(s) means f always holds along every N-path
% from s along which the fairness predicate Ff holds infinitely
% often.  This is different from the usual linear-time notion of 
% fairness where the strong form asserts that if an action A is 
% enabled infinitely often, it is taken infinitely often, and the 
% weak form asserts that if any action that is continuously enabled 
% is taken infinitely often.  

fairctlops  [ state : TYPE ]: THEORY
 BEGIN
  u,v,w: VAR state
  f,g,Q,P,p1,p2: VAR pred[state]
  N: VAR [state, state->bool]
  Ff: VAR pred[state] % Fair formula

  CONVERSION+ K_conversion

  fairEG(N, f)(Ff): pred[state] =
    nu(LAMBDA P: EU(N, f, f AND Ff AND EX(N, P)))

  fairAF(N,f)(Ff):pred[state]  = NOT fairEG(N, NOT f)(Ff)

  fair?(N,Ff):pred[state] = fairEG(N,LAMBDA u: TRUE)(Ff)

  fairEX(N,f)(Ff):pred[state] = EX(N,f AND fair?(N,Ff))

  fairEU(N,f,g)(Ff):pred[state] = EU(N,f,g AND fair?(N,Ff))

  fairEF(N,f)(Ff):pred[state] = EF(N,f AND fair?(N,Ff))

  fairAX(N,f)(Ff):pred[state] = NOT fairEX(N, NOT f)(Ff)

  fairAG(N,f)(Ff):pred[state] = NOT fairEF(N,NOT f)(Ff)

  fairAU(N,f,g)(Ff):pred[state] =
	NOT fairEU(N,NOT g,NOT f AND NOT g)(Ff)
	    AND fairAF(N,g)(Ff)

  CONVERSION- K_conversion

 END fairctlops


% Fair versions of CTL operators with lists of fairness conditions.
% FairAG(N,f)(Fflist)(s) means f always holds on every N-path from
% s along which each predicate in Fflist holds infinitely often.

Fairctlops[state : TYPE]: THEORY
 BEGIN
  u,v,w: VAR state
  f,g,Q,P,p1,p2: VAR pred[state]
  N: VAR [state, state->bool]
  Fflist, Gflist: VAR list[pred[state]] % Fair formula

  CONVERSION+ K_conversion

  CheckFair(Q, N, f, Fflist): RECURSIVE pred[state] =
    (CASES Fflist OF
     cons(Ff, Gflist):
	     EU(N, f, f AND Ff AND
		      EX(N, CheckFair(Q, N, f, Gflist))),
     null : Q
     ENDCASES)
    MEASURE length(Fflist)

  FairEG(N, f)(Fflist): pred[state] =
    nu(LAMBDA P: CheckFair(P, N, f, Fflist))

  FairAF(N,f)(Fflist):pred[state]  = NOT FairEG(N, NOT f)(Fflist)

  Fair?(N,Fflist):pred[state] = FairEG(N,LAMBDA u: TRUE)(Fflist)

  FairEX(N,f)(Fflist):pred[state] = EX(N,f AND Fair?(N,Fflist))

  FairEU(N,f,g)(Fflist):pred[state] = EU(N,f,g AND Fair?(N,Fflist))

  FairEF(N,f)(Fflist):pred[state] = EF(N,f AND Fair?(N,Fflist))

  FairAX(N,f)(Fflist):pred[state] = NOT FairEX(N, NOT f)(Fflist)

  FairAG(N,f)(Fflist):pred[state] = NOT FairEF(N,NOT f)(Fflist)

  FairAU(N,f,g)(Fflist):pred[state] =
	NOT FairEU(N,NOT g,NOT f AND NOT g)(Fflist)
	    AND FairAF(N,g)(Fflist)

  % Turn off K_conversion so that it is not a conversion by default.
  CONVERSION- K_conversion
 END Fairctlops


bit: THEORY
% -----------------------------------------------------------------------
% The bit theory defines bits and their properties. Bits are interpreted
% as the natural numbers 0 and 1.
% -----------------------------------------------------------------------
BEGIN

  bit  : TYPE = bool
  nbit : TYPE = below(2)  %  could be {n: nat | n = 0 OR n = 1}

  b: VAR bit

  bit_cases: LEMMA b = FALSE OR b = TRUE

  b0: [below(1) -> bit] = (LAMBDA (i: below(1)): FALSE)
  b1: [below(1) -> bit] = (LAMBDA (i: below(1)): TRUE)

  b2n(b:bool)     : nbit = IF b THEN 1 ELSE 0 ENDIF 
  n2b(nb: nbit)   : bool = (nb = 1)

  CONVERSION b2n

END bit


%------------------------------------------------------------------------
%
% Definition of a bitvector
% -----------------------------------------
%
%   Defines:
%  
%       bvec: TYPE = [below(N) -> bit]
%
%       ^(bv, (i: below(N))): bit
%
%   Establishes:
%  
%
%------------------------------------------------------------------------
bv[N: nat]: THEORY
BEGIN

  bvec : TYPE = [below(N) -> bit]

  b: VAR bit
  bv: VAR bvec
  i: VAR below[N]

  bvec0(i): bit = FALSE
  bvec1(i): bit = TRUE
  fill(b)(i): bit = b;

  %-----------------------------------------------------------------------    
  % The implementation of the bitvector can be hidden through use of
  % the ^ function below.
  %-----------------------------------------------------------------------  
    
  ^(bv, i): bit = bv(i)

END bv


exp2: THEORY
BEGIN

  n,m, x1, x2: VAR nat
  
  exp2(n: nat): RECURSIVE posnat = IF n = 0 THEN 1 ELSE 2 * exp2(n - 1) ENDIF
    MEASURE n

  JUDGEMENT exp2(n: nat) HAS_TYPE above(n)

% === Properties of exp2 ===================================================

  exp2_def	 : LEMMA exp2(n) = 2^n
 
  exp2_pos	 : LEMMA exp2(n) > 0
 
  exp2_n	 : LEMMA exp2(n+1) = 2*exp2(n)
 
  exp2_sum	 : LEMMA exp2(n + m) = exp2(n) * exp2(m)
 
  exp2_minus	 : LEMMA (FORALL n,(k:upto(n)): exp2(n-k)=exp2(n)/exp2(k))
 
  exp2_strictpos : LEMMA n > 0 IMPLIES exp2(n) > 1
 
  exp2_lt	 : LEMMA n < m IMPLIES exp2(n) < exp2(m)

  exp_prop       : LEMMA x1 < exp2(n) AND  x2 < exp2(m) 
                           IMPLIES x1 * exp2(m) + x2 < exp2(n + m)

END exp2


% bv_cnv: THEORY

% BEGIN

%   CONVERSION fill[1]

% END bv_cnv


bv_concat_def [n:nat, m:nat ]: THEORY
%------------------------------------------------------------------------
% This theory defines the concatenation operator o for bitvectors:
%
%   o: [bvec[n], bvec[m] -> bvec[n+m]] 
%
% The theory is instantiated with the sizes of the input bit vectors.
%------------------------------------------------------------------------

BEGIN

  o(bvn: bvec[n], bvm: bvec[m]): bvec[n+m] =
       (LAMBDA (nm: below(n+m)): IF nm < m THEN bvm(nm)
                                 ELSE bvn(nm - m)
                                 ENDIF)

END bv_concat_def


bv_bitwise [N: nat] : THEORY
% -----------------------------------------------------------------------
% Defines bit-wise logical operations on bit vectors.
%
%    Introduces:
%       OR : bv1 OR bv2
%       &  : bv1 & bv2
%       IFF: bv1 IFF bv2
%       NOT: NOT bv1
%       XOR: bv1 XOR bv2
% -----------------------------------------------------------------------  
BEGIN

  i: VAR below(N) 
  OR(bv1,bv2: bvec[N]) : bvec[N] = (LAMBDA i: bv1(i) OR bv2(i));
  
  AND(bv1,bv2: bvec[N]): bvec[N] = (LAMBDA i: bv1(i) AND bv2(i)) ;

  IFF(bv1,bv2: bvec[N]): bvec[N] = (LAMBDA i: bv1(i) IFF bv2(i)) ;

  NOT(bv: bvec[N])     : bvec[N] = (LAMBDA i: NOT bv(i)) ;

  XOR(bv1,bv2: bvec[N]): bvec[N] = (LAMBDA i: XOR(bv1(i),bv2(i))) ;

% === The following lemmas can be used to hide the implementation
%     details of the bitvector

  bv, bv1, bv2: VAR bvec[N]

  bv_OR  : LEMMA (bv1 OR bv2)^i = (bv1^i OR bv2^i)

  bv_AND : LEMMA (bv1 AND bv2)^i = (bv1^i AND bv2^i)

  bv_IFF : LEMMA (bv1 IFF bv2)^i = (bv1^i IFF bv2^i)

  bv_XOR : LEMMA XOR(bv1,bv2)^i = XOR(bv1^i,bv2^i)

  bv_NOT : LEMMA (NOT bv)^i = NOT(bv^i)

END bv_bitwise


%------------------------------------------------------------------------
%
% Interpretation of a bitvector as a natural number
% -------------------------------------------------
%
%   Defines:
%  
%       bv2nat: function[bvec[N] -> below(exp2(N))] 
%       nat2bv: function[below(exp2(N)) -> bvec[N]]
%
%   Establishes:
%  
%       bv2nat_bij: THEOREM bijective?(bv2nat)
%       bv2nat_inv: THEOREM bv2nat(nat2bv(val)) = val  
%
%  
%   See note at end of theory for reasons why nat2bv should be avoided
%   in specifications.
%
%------------------------------------------------------------------------
bv_nat[N: nat]: THEORY
BEGIN

% === Interpretation of a bit vector as a natural number ================

  bv2nat_rec(n: upto(N), bv:bvec[N]): RECURSIVE nat =
      IF n = 0 THEN 0
      ELSE exp2(n-1) * bv^(n-1) + bv2nat_rec(n - 1, bv)
      ENDIF
    MEASURE n

  bv_lem: LEMMA FORALL (n: below(N), bv: bvec[N]): bv(n) = FALSE OR bv(n) = TRUE 

  bv2nat_rec_bound: LEMMA FORALL (n: upto(N), bv: bvec[N]): 
                                  bv2nat_rec(n, bv) < exp2(n)

  bv2nat(bv:bvec[N]): below(exp2(N)) = bv2nat_rec(N, bv)

% ===== Properties of bv2nat ===================================

  n           : VAR upto(N)
  val         : VAR below(exp2(N))
  bv, bv1, bv2: VAR bvec[N]

  bv2nat_inj_rec: LEMMA
      bv2nat_rec(n, bv1) = bv2nat_rec(n, bv2)
        <=>  (FORALL (m: below(N)): (m < n) IMPLIES bv1(m) = bv2(m))

  bv2nat_surj_rec: LEMMA FORALL (y:below(exp2(n))): 
                                   EXISTS bv:bv2nat_rec(n, bv) = y

  bv2nat_inj     : THEOREM % injective?(bv2nat)
                            (FORALL (x, y: bvec[N]): (bv2nat(x) = bv2nat(y) 
                                      IMPLIES (x = y)))

  bv2nat_surj    : THEOREM % surjective?(bv2nat)
                              (FORALL (y: below(exp2(N))): 
                                     (EXISTS (x: bvec[N]): bv2nat(x) = y))


  bv2nat_bij        : THEOREM bijective?(bv2nat)    

  bv2nat_rec_fill_F : LEMMA bv2nat_rec(n, fill[N](FALSE)) = 0
  bv2nat_rec_fill_T : LEMMA bv2nat_rec(n, fill[N](TRUE)) = exp2(n)-1

  bv2nat_fill_F     : LEMMA bv2nat(fill[N](FALSE)) = 0
  bv2nat_fill_T     : LEMMA bv2nat(fill[N](TRUE)) = exp2(N)-1

  bv2nat_eq0        : LEMMA bv2nat(bv) = 0     IMPLIES (bv = fill[N](FALSE))
  bv2nat_eq_max     : LEMMA bv2nat(bv) = exp2(N)-1 IMPLIES bv = (fill[N](TRUE)) 

  bv2nat_top_bit    : THEOREM N > 0 IMPLIES
                             IF bv2nat(bv) < exp2(N-1) THEN bv^(N-1) = FALSE
                                                       ELSE bv^(N-1) = TRUE ENDIF

  bv2nat_topbit    : THEOREM N > 0 IMPLIES bv^(N-1) = (bv2nat(bv) >= exp2(N-1))

% =================== Properties of nat2bv ===================================

  nat2bv(val: below(exp2(N))): {bv: bvec[N] | bv2nat(bv) = val}

  nat2bv_def       : LEMMA  nat2bv = inverse(bv2nat)

  nat2bv_bij       : THEOREM bijective?[below(exp2(N)),bvec[N]](nat2bv)

  nat2bv_inv       : THEOREM nat2bv(bv2nat(bv)) = bv

  nat2bv_rew       : LEMMA nat2bv(val) = bv IFF bv2nat(bv) = val

  bv2nat_inv       : THEOREM bv2nat(nat2bv(val)) = val

END bv_nat


empty_bv: THEORY

BEGIN

  empty_bv: [below[0] -> bool] = (LAMBDA (x: below[0]): TRUE) ;

END empty_bv


bv_caret[N: nat]: THEORY
%-----------------------------------------------------------------------
% An extractor operation decomposes a bvec into smaller
% bit vectors.  In the following, we define a number of
% extractors for bvec. 
%
%    Introduces:
%       bv^(m,n) creates bv[m-n+1] from bits m through n
%    
%       bv^^(m,n) can return an empty bitvector if n > m
%  
%-----------------------------------------------------------------------  
BEGIN

  %-----------------------------------------------------------------------  
  % The following operator (^) extracts a contiguous fragment of
  % a bit vector between two given positions.
  %-----------------------------------------------------------------------  

%  ^(bv: bvec[N], p:[m: below(N), upto(m)]): bvec[LET (m, n) = p IN m - n + 1] =
%             LET (m, n) = p IN
%                (LAMBDA  (ii: below(m - n + 1)): bv(ii + n)) ;


   ^(bv: bvec[N], sp:[i1: below(N), upto(i1)]): bvec[proj_1(sp)-proj_2(sp)+1] =
       (LAMBDA  (ii: below(proj_1(sp) - proj_2(sp) + 1)):
		  bv(ii + proj_2(sp))) ;

%  ^^(bv: bvec[N], p:[m:below[N],nat]): bvec[LET (m, n) = p IN 
%                                        IF m < n THEN 0 ELSE m - n + 1 ENDIF] =
%      LET (m, n) = p IN
%        IF m < n THEN empty_bv 
%        ELSE (LAMBDA (ii: below[m-n+1]): bv(ii + n))
%        ENDIF


% === Useful Lemmas and Theorems =========================================

  bv: VAR bvec[N]

  bv_caret_all  : LEMMA N > 0 IMPLIES bv^(N-1, 0) = bv

%    dcaret_lem : LEMMA (FORALL (i: below(N), j: upto(i)): bv^^(i,j) = bv^(i,j))

  bv_caret_ii_0 : LEMMA (FORALL (i: below(N)): bv^(i,i)^0 = bv^i)

  bv_caret_elim : LEMMA (FORALL (i: below(N), j: upto(i), k: below(i-j+1)): 
                               bv ^ (i, j) ^ k = bv^(j+k))

END bv_caret 


mod: THEORY
%------------------------------------------------------------------------
%
%  mod function as defined in `Concrete Mathematics'
%  The Ada definition of mod is consistent with this definition
%
% Author:
%   Paul S. Miner                | email: p.s.miner@larc.nasa.gov
%   1 South Wright St. / MS 130  |   fax: (804) 864-4234
%   NASA Langley Research Center | phone: (804) 864-6201
%   Hampton, Virginia 23681      |
%------------------------------------------------------------------------

  BEGIN

  i,k,cc: VAR int
  m: VAR posnat
  n,a,b,c,x: VAR nat   

  j: VAR nonzero_integer

  ml3: LEMMA abs(i -  m * floor(i/m)) < m
  ml4: LEMMA abs(i +  m * floor(-i/m)) < m

  mod(i,j): {k| abs(k) < abs(j)} = i-j*floor(i/j)

  mod_pos:  LEMMA mod(i,m) >= 0 AND mod(i,m) < m

  JUDGEMENT mod(i:int, m: posnat) HAS_TYPE below(m)


  mod_even   : LEMMA integer_pred(i/j) IMPLIES mod(i,j) = 0

  mod_neg    : LEMMA mod(-i,j) = IF integer_pred(i/j) THEN 0
                                 ELSE j - mod(i,j)
                                 ENDIF

  mod_neg_d  : LEMMA mod(i,-j) = IF integer_pred(i/j) THEN 0
                                 ELSE mod(i,j) - j 
                                 ENDIF

  mod_eq_arg : LEMMA mod(j,j) = 0
  
  mod_lt     : LEMMA abs(i) < abs(j) IMPLIES mod(i,j) = 
                                  IF sgn(i) = sgn(j) OR i = 0 THEN i
                                  ELSE i + j
                                  ENDIF

  mod_lt_nat : LEMMA n < m IMPLIES mod(n,m) = n

  mod_lt_int : LEMMA -m < i AND i < m IMPLIES mod(i,m) = 
                                  IF i >= 0 THEN i ELSE i + m
                                  ENDIF


  mod_sum_pos: LEMMA mod(i+k*m,m) = mod(i,m)

  mod_gt : LEMMA m <= i AND i < 2*m IMPLIES mod(i,m) = i-m 

  mod_sum    : LEMMA mod(i+k*j,j) = mod(i,j)

  mod_sum_nat: LEMMA (FORALL (n1,n2: below(m)):
                          mod(n1+n2,m) = IF n1 + n2 < m THEN n1+n2
                                         ELSE n1 + n2 - m
                                         ENDIF)

  mod_it_is  : LEMMA a = b + m*c AND b < m IMPLIES
                        b = mod(a,m)

  mod_zero   : LEMMA mod(0,j) = 0

  mod_one    : LEMMA mod(1,j) = IF abs(j) = 1 THEN 0
                                   ELSIF j > 0 THEN 1
                                   ELSE j + 1
                                   ENDIF

  mod_of_mod     : LEMMA mod(i + mod(k,m), m) = mod(i+k, m)

  mod_of_mod_neg : LEMMA mod(i - mod(k,m), m) = mod(i-k, m)

  mod_inj_plus       : LEMMA a < m AND n < m AND c < m AND
                       mod(a + n, m) = mod(a + c, m) IMPLIES n = c

  mod_inj_minus       : LEMMA a < m AND n < m AND c < m AND
                        mod(a - n, m) = mod(a - c, m) IMPLIES n = c


  mod_wrap_around: LEMMA n < m AND (c <= m AND c >= m-n) IMPLIES
                              mod(n+c, m) = n - (m-c)

  mod_wrap2:       LEMMA c < m IMPLIES mod(m+c, m) = c

% Injection-like properties for mod for limited ranges

  mod_inj1:        LEMMA x < m AND n < m AND c < m AND
                       mod(x + n, m) = mod(x + c, m) IMPLIES n = c

  mod_inj2:        LEMMA x < m AND n < m AND c < m AND
                        mod(x - n, m) = mod(x - c, m) IMPLIES n = c

  mod_wrap_inj: LEMMA n < m AND a < m AND b < m AND a > 0 AND
                            mod(n + a, m) = mod(n - b, m) IMPLIES a + b = m

  mod_wrap_inj_eq: LEMMA
      x < m AND a < m AND b < m AND a > 0
        IMPLIES (mod(x + a, m) = mod(x - b, m)) = (a + b = m)

  kk, vv: VAR nat
  mod_neg_limited: LEMMA 0 <= kk AND  kk < m AND vv < m AND
                      vv - kk < 0 IMPLIES mod(vv - kk,m) = m + vv - kk


  odd_mod: LEMMA even?(m) => (odd?(mod(i, m)) IFF odd?(i))

  even_mod: LEMMA even?(m) => (even?(mod(i, m)) IFF even?(i))

  mj: VAR posnat
  mod_mult      : LEMMA mod(mod(i,mj*m),m) = mod(i,m)

END mod


%------------------------------------------------------------------------
%
% Natural arithmetic over bitvectors
% -----------------------------------------
%
%   Defines:
%  
%         > :  bv1 > bv2
%         >=:  bv1 >= bv2
%         < :  bv1 < bv2
%         <=:  bv1 <= bv1
%         + :  bv1 + i
%         - :  bv1 - i
%         + :  bv1 + bv2
%         * :  bv1 * bv2
%
%   Establishes:
%   
%     bv_plus    : LEMMA bv2nat(bv + i) = mod(bv2nat(bv) + i, exp2(N))) 
%					       
%     bv_add     : LEMMA bv2nat(bv1 + bv2) =
%			       IF bv2nat(bv1) + bv2nat(bv2) < exp2(N)
%			       THEN bv2nat(bv1) + bv2nat(bv2)
%			       ELSE bv2nat(bv1) + bv2nat(bv2) - exp2(N) ENDIF
%   
%	
%  Note that + has been defined in a manner that avoids the introduction of 
%  nat2bv.  Also nat2bv has been defined in a manner that prevents GRIND from
%  expanding nat2bv into an expression involving "epsilon".  The needed
%  property about nat2bv is available in its type.
% 
%------------------------------------------------------------------------
bv_arith_nat_defs[N: nat]: THEORY
BEGIN

% ----- Definition of inequalities over the bit vectors.

  < (bv1: bvec[N], bv2: bvec[N]): bool = bv2nat(bv1) <  bv2nat(bv2) ;
  <=(bv1: bvec[N], bv2: bvec[N]): bool = bv2nat(bv1) <= bv2nat(bv2) ;

  > (bv1: bvec[N], bv2: bvec[N]): bool = bv2nat(bv1) >  bv2nat(bv2) ;
  >=(bv1: bvec[N], bv2: bvec[N]): bool = bv2nat(bv1) >= bv2nat(bv2) ;


% ----- Increments a bit vector by a integer modulo 2**N 


  +(bv: bvec[N], i: int): {bvn: bvec[N] | 
                             bv2nat(bvn) = mod(bv2nat(bv) + i, exp2(N))}

  bv_plus : LEMMA (FORALL (bv: bvec[N], i: int):
                         bv2nat(bv + i) = mod(bv2nat(bv) + i, exp2(N))) ;

% ----- Decrements a bit vector by a integer modulo 2**N.

  -(bv: bvec[N], i: int): bvec[N] = bv + (-i) ;

  bv_minus     : LEMMA (FORALL (bv: bvec[N], i: int):
                    bv2nat(bv - i) = mod(bv2nat(bv) - i, exp2(N))) ;


% ----- Addition of two bit vectors interpreted as natural numbers.

  +(bv1: bvec[N], bv2: bvec[N]): {bv: bvec[N] | bv2nat(bv) = 
                              IF bv2nat(bv1) + bv2nat(bv2) < exp2(N)
                              THEN bv2nat(bv1) + bv2nat(bv2)
                              ELSE bv2nat(bv1) + bv2nat(bv2) - exp2(N) 
                              ENDIF}

% ----- Multiplication of two bit vectors interpreted as natural numbers.

  *(bv1: bvec[N], bv2: bvec[N]): {bv: bvec[2*N] | bv2nat(bv) = 
                                          bv2nat(bv1) * bv2nat(bv2)} ;

% Properties of these functions are in the bitvector library

END bv_arith_nat_defs


%------------------------------------------------------------------------
%
% Integer interpretation of a bitvector (twos-complement interpretation)
% ----------------------------------------------------------------------
%
%   Defines:
%
%      minint: int = -exp2(N-1)
%      maxint: int =  exp2(N-1) - 1
%      rng_2s_comp: TYPE = {i: int | minint <= i AND i <= maxint}
%      bv2int : [bvec[N] -> rng_2s_comp] 
%      int2bv : [rng_2s_comp  -> bvec[N]]
%  
%   Establishes:
%  
%      bv2int_bij : THEOREM bijective?(bv2int)
%      bv2int_inv : THEOREM bv2int(int2bv(iv))=iv
%
%   Note.  The int2bv should be avoided in practice.  It is necessary
%          for the development of the library.
%
%------------------------------------------------------------------------
bv_int_defs[N: posnat]: THEORY
BEGIN

  minint: int = -exp2(N-1)
  maxint: int =  exp2(N-1) - 1

  bv_maxint_to_minint:    LEMMA maxint = -minint - 1
  bv_minint_to_maxint:    LEMMA minint = -maxint - 1

  in_rng_2s_comp(i: int): bool = (minint <= i AND i <= maxint)
  rng_2s_comp: TYPE = {i: int | minint <= i AND i <= maxint}

  bv2int(bv: bvec[N]): rng_2s_comp = IF bv2nat(bv) < exp2(N-1) THEN bv2nat(bv)
                                     ELSE bv2nat(bv) - exp2(N) ENDIF

  int2bv(iv: rng_2s_comp): {bv: bvec[N] | bv2int(bv) = iv}

END bv_int_defs


%------------------------------------------------------------------------
%
% Defines functions over bit vectors interpreted as natural numbers.
%
%    Introduces:
%
%         - :  bv1 - bv2
%         - : [bvec -> bvec] 
%         - : [bvec, bvec -> bvec]
%         overflow    : [bvec, bvec -> bool]  
%         underflow   : [bvec, bvec -> bool]  
%   
%------------------------------------------------------------------------
bv_arithmetic_defs[N: posnat]: THEORY
BEGIN

  bv, bv1, bv2 : VAR bvec[N]

% ---------- 2's complement negation of a bit vector ----------
    
  -(bv: bvec[N]): { bvn: bvec[N] | bv2int(bvn) = 
                              IF bv2int(bv) = minint[N] THEN bv2int(bv)
                              ELSE -(bv2int(bv)) ENDIF}

% ---------- 2's complement subtraction of two bit vectors ----------
    
  -(bv1, bv2): bvec[N] = (bv1 + (-bv2))

% ---------- Define conditions for 2's complement overflow  ----------

    
  overflow(bv1,bv2): bool = (bv2int(bv1) + bv2int(bv2)) > maxint[N]
                             OR (bv2int(bv1) + bv2int(bv2)) < minint[N]

% === Properties of these additional functions in lib/bitvectors/bv_arithmetic=

% ---------- Integer <, <=, >, >=, +, * ----------
% Note that we can't use these operators, as they will always be ambiguous

  bv_slt(bv1, bv2): bool = bv2int(bv1) < bv2int(bv2)

  bv_sle(bv1, bv2): bool = bv2int(bv1) <= bv2int(bv2)

  bv_sgt(bv1, bv2): bool = bv2int(bv1) > bv2int(bv2)

  bv_sge(bv1, bv2): bool = bv2int(bv1) >= bv2int(bv2)

  bv_splus(bv1, (bv2 | NOT overflow(bv1, bv2))): bvec[N] =
    int2bv(bv2int(bv1) + bv2int(bv2))

  mult_overflow(bv1, bv2): bool = (bv2int(bv1) * bv2int(bv2)) > maxint[N]
                               OR (bv2int(bv1) * bv2int(bv2)) < minint[N]

  bv_stimes(bv1, (bv2 | NOT mult_overflow(bv1, bv2))): bvec[N] =
    int2bv(bv2int(bv1) * bv2int(bv2))

END bv_arithmetic_defs


bv_extend_defs [N: posnat] : THEORY
% -----------------------------------------------------------------------  
%    Introduces:
%	zero_extend: [k: above(N) -> [bvec[N] -> bvec[l]]] =
%	sign_extend: [k: above(N) -> [bvec[N] -> bvec[l]]] =
%	zero_extend_lsend: [k: above(N) -> [bvec[N] -> bvec[l]]]
%	lsb_extend: [k: above(N) -> [bvec[N] -> bvec[l]]] =
%   
% -----------------------------------------------------------------------  

BEGIN
    
  bv: VAR bvec[N]
  k: VAR above(N)
  
  %------------------------------------------------------------------------
  % zero_extend returns a function that extends a bit vector to length k 
  % such that its interpretation as a natural number remains unchanged.
  % That is, it fills 0's at the most significant positions.
  %------------------------------------------------------------------------

  zero_extend(k: above(N)): [bvec[N] -> bvec[k]] =
       (LAMBDA bv: fill[k-N](FALSE) o bv )

  %------------------------------------------------------------------------
  % sign_extend returns a function that extends a bit vector to length k
  % by repeating the most significant bit of the given bit vector.
  % The set above(N) contains nat numbers greater than n.
  %------------------------------------------------------------------------

  sign_extend(k: above(N)): [bvec[N] -> bvec[k]] =
       (LAMBDA bv:  fill[k-N](bv^(N-1)) o bv )
  %------------------------------------------------------------------------
  % zero_extend_lsend returns a function that extends a bit vector to
  % length k by padding 0's at the least significant end of bvec.
  % That is, the bv2nat interpretation of the argument increases by 2**(k-N)
  %------------------------------------------------------------------------
    
  zero_extend_lsend(k: above(N)): [bvec[N] -> bvec[k]] =
        (LAMBDA bv:  bv o fill[k-N](FALSE))
  
  %------------------------------------------------------------------------
  % lsb_extend returns a function that extends a bit vector to
  % length k by repeating the lsb of the bit vector at its
  % least significant end.
  %------------------------------------------------------------------------
    
  lsb_extend(k: above(N)): [bvec[N] -> bvec[k]] =
       (LAMBDA bv: bv o fill[k-N](bv^0))

  pad_left(k: above(N), b: bit)(bv): bvec[k] = fill[k-N](b) o bv

  pad_right(k: above(N), b: bit)(bv): bvec[k] = bv o fill[k-N](b)

END bv_extend_defs


%-------------------------------------------------------------------------
%
%  Basic properties of infinite sets.  This theory defines infinite sets
%  as the subtype of set[T] that satisfies the predicate "is_infinite".
%  This predicate states that there is no injective function into below[N]
%  for any N.
%
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%-------------------------------------------------------------------------
infinite_sets_def[T: TYPE]: THEORY
 BEGIN

  S, R: VAR set[T]


  % ==========================================================================
  % The main definition
  % ==========================================================================

  is_infinite(S): MACRO bool = NOT is_finite(S)  
  infinite_set: TYPE = {S | NOT is_finite(S)}

  Inf: VAR infinite_set
  Fin: VAR finite_set[T]
  t: VAR T


  % ==========================================================================
  % Properties of infinite sets
  % ==========================================================================

  infinite_nonempty: JUDGEMENT infinite_set SUBTYPE_OF (nonempty?[T])

  infinite_add: JUDGEMENT add(t, Inf) HAS_TYPE infinite_set

  infinite_remove: JUDGEMENT remove(t, Inf) HAS_TYPE infinite_set

  infinite_superset: THEOREM FORALL Inf, S: subset?(Inf, S) => is_infinite(S)

  infinite_union_left: JUDGEMENT union(Inf, S) HAS_TYPE infinite_set
  infinite_union_right: JUDGEMENT union(S, Inf) HAS_TYPE infinite_set

  infinite_union: THEOREM
    FORALL S, R:
      is_infinite(union(S, R)) => is_infinite(S) OR is_infinite(R)

  infinite_intersection: THEOREM
    FORALL S, R:
      is_infinite(intersection(S, R)) => is_infinite(S) AND is_infinite(R)

  infinite_difference: JUDGEMENT difference(Inf, Fin) HAS_TYPE infinite_set

  infinite_rest: JUDGEMENT rest(Inf) HAS_TYPE infinite_set

  infinite_fullset: THEOREM
    (EXISTS S: is_infinite(S)) => is_infinite(fullset[T])

 END infinite_sets_def


finite_sets_of_sets[T: TYPE]: THEORY
 BEGIN

  a: VAR set[T]

  powerset_natfun_rec(A: finite_set[T],
                      n: upto(card(A)),
                      f: (bijective?[(A), below(card(A))]),
                      B: (powerset(A))):
        RECURSIVE nat =
   IF n = 0 THEN 0
   ELSE LET nval = exp2(n-1) * IF member(inverse(f)(n-1), B) THEN 1 ELSE 0 ENDIF
         IN nval + powerset_natfun_rec(A, n-1, f, B)
   ENDIF
  MEASURE n

  powerset_natfun_rec_bound: LEMMA
   FORALL (A: finite_set[T],
           n: upto(card(A)),
           f: (bijective?[(A), below(card(A))]),
           B: (powerset(A))):
     powerset_natfun_rec(A, n, f, B) < exp2(n)

  powerset_natfun(A: finite_set[T])(B: (powerset(A))): below(exp2(card(A))) =
    LET f = choose(bijective?[(A), below(card(A))])
     IN powerset_natfun_rec(A, card(A), f, B)

  powerset_natfun_inj_rec: LEMMA
   FORALL (A: finite_set[T],
           n: upto(card(A)),
           f: (bijective?[(A), below(card(A))]),
           B1, B2: (powerset(A))):
    powerset_natfun_rec(A, n, f, B1) = powerset_natfun_rec(A, n, f, B2)
      <=> (FORALL (m: upto(card(A))):
            (m < n) IMPLIES
               (member(inverse(f)(m), B1) IFF member(inverse(f)(m), B2)))

  powerset_natfun_inj: LEMMA
    FORALL (A: finite_set[T]):
      FORALL (B1, B2: (powerset(A))):
        powerset_natfun(A)(B1) = powerset_natfun(A)(B2) IMPLIES B1 = B2

  powerset_finite: JUDGEMENT
    powerset(A: finite_set[T]) HAS_TYPE finite_set[set[T]]

  SS: VAR setofsets[T]

  Union_finite: THEOREM
    FORALL SS: is_finite(Union(SS)) IFF is_finite(SS) AND every(is_finite)(SS)

  finite_Union_finite: LEMMA is_finite(SS) AND every(is_finite[T])(SS) IMPLIES
                             is_finite(Union(SS))

  Union_infinite: COROLLARY
    FORALL SS:
      is_infinite(Union(SS)) IFF is_infinite(SS) OR some(is_infinite)(SS)

  Intersection_finite: THEOREM
    FORALL SS:
      nonempty?(SS) AND every(is_finite)(SS) => is_finite(Intersection(SS))

  Intersection_infinite: COROLLARY
    FORALL SS: is_infinite(Intersection(SS)) => every(is_infinite)(SS)

  Complement_finite: THEOREM
    FORALL SS: is_finite(Complement(SS)) IFF is_finite(SS)

  Complement_is_finite: JUDGEMENT
    Complement(SS: finite_set[set[T]]) HAS_TYPE finite_set[set[T]]

  Complement_infinite: COROLLARY
    FORALL SS: is_infinite(Complement(SS)) IFF is_infinite(SS)

  Complement_is_infinite: JUDGEMENT
    Complement(SS: infinite_set[set[T]]) HAS_TYPE infinite_set[set[T]]

 END finite_sets_of_sets


% Equivalence classes, quotient types, etc.
%
% Bart Jacobs, Dep. Comp. Sci., Univ. Nijmegen.
% 
% With suggestions and remarks from: 
% Ulrich Hensel, Marieke Huisman, Hendrik Tews.
%
% With modifications and additions by Sam Owre, SRI International

EquivalenceClosure[T : TYPE] : THEORY
BEGIN

  R, S : VAR PRED[[T, T]]
  x, y : VAR T

  % Higher order definition of equivalence relation closure.

  EquivClos(R) : equivalence[T] =
    { (x, y) | FORALL(S : equivalence[T]) : subset?(R, S) IMPLIES S(x, y) }

  EquivClosSuperset : LEMMA
    subset?(R, EquivClos(R))

  EquivClosMonotone : LEMMA
    subset?(R, S) IMPLIES subset?(EquivClos(R), EquivClos(S))

  EquivClosLeast : LEMMA
    equivalence?(S) AND subset?(R, S) IMPLIES subset?(EquivClos(R), S)

  EquivClosIdempotent : LEMMA
    EquivClos(EquivClos(R)) = EquivClos(R)

  EquivalenceCharacterization : LEMMA
    equivalence?(S) IFF (S = EquivClos(S))

END EquivalenceClosure


QuotientDefinition[T : TYPE] : THEORY
BEGIN

  R : VAR set[[T, T]]
  S : VAR equivalence[T]
  x, y, z : VAR T

  EquivClass(R)(x) : set[T] = { z | R(x, z) }

  EquivClassNonEmpty : LEMMA
    nonempty?[T](EquivClass(S)(x))

  EquivClassEq : LEMMA
    EquivClass(S)(x) = EquivClass(S)(y) IFF S(x, y)

  repEC(S)(x): T = choose(EquivClass(S)(x))

  % The next two lemmas facilitate working with representatives.

  EquivClassChoose : LEMMA
    S(x, repEC(S)(x))

  ChooseEquivClassChoose : LEMMA
    EquivClass(S)(repEC(S)(x)) = EquivClass(S)(x)

  Quotient(S) : TYPE =
    { P : set[T] | EXISTS x : P = EquivClass(S)(x) }

  rep(S)(P: Quotient(S)): T = choose(P)

  rep_is_repEC: LEMMA
     rep(S)(EquivClass(S)(x)) = repEC(S)(x)

  rep_lemma: LEMMA
     EquivClass(S)(x)(rep(S)(EquivClass(S)(x)))

  % Note that quotient_map has a different range type than EquivClass,
  % and EquivClass(S) is not surjective.
  quotient_map(S)(x) : Quotient(S) =
    EquivClass(S)(x)

  quotient_map_surjective : LEMMA
    surjective?(quotient_map(S))

  % Quotients are also defined for arbitrary relations, via the
  % Equivalence Closure (EC).

  ECQuotient(R) : TYPE =              
    Quotient(EquivClos(R))

  ECquotient_map(R)(x) : ECQuotient(R) =
    quotient_map(EquivClos(R))(x)

END QuotientDefinition

KernelDefinition[X: TYPE, X1: TYPE FROM X, Y : TYPE] : THEORY
BEGIN

  f : VAR [X1 -> Y]
  R : VAR PRED[[X, X]]
  x1, x2 : VAR X1

  % The following definition would be part of the 'functions' theory
  % but equivalence is defined afterwards.

  EquivalenceKernel(f) : equivalence[X1] =
    { (x1, x2) | f(x1) = f(x2) }

  PreservesEq(R)(f) : bool =
    subset?(restrict[[X, X],[X1, X1], bool](R), EquivalenceKernel(f))

  PreservesEqClosure : LEMMA
    PreservesEq(R) = PreservesEq(EquivClos[X1](R))

  PreservesEq_is_preserving: LEMMA
    PreservesEq(R) = preserves(restrict[[X, X], [X1, X1], bool](R), =[Y])

END KernelDefinition

QuotientKernelProperties[X : TYPE, X1: TYPE FROM X] : THEORY
BEGIN

  S : VAR equivalence[X1]
  R : VAR PRED[[X, X]]

  Kernel_quotient_map : LEMMA
    EquivalenceKernel[X, X1, Quotient(S)](quotient_map(S)) = S

  PreservesEq_quotient_map : LEMMA
    PreservesEq[X, X1, Quotient(S)](S)(quotient_map(S))

  quotient_map_is_Quotient_EqivalenceRespecting: JUDGEMENT
    quotient_map(S) HAS_TYPE (PreservesEq[X, X1, Quotient(S)](S))

  Kernel_ECquotient_map : LEMMA
    EquivalenceKernel[X, X1, ECQuotient(S)](quotient_map(S)) = S

  PreservesEq_ECquotient_map : LEMMA
    PreservesEq[X, X1, ECQuotient(S)](S)(quotient_map(S))

  quotient_map_is_ECQuotient_EqivalenceRespecting: JUDGEMENT
    quotient_map(S) HAS_TYPE (PreservesEq[X, X1, ECQuotient(S)](S))

END QuotientKernelProperties


QuotientSubDefinition[X : TYPE, X1: TYPE FROM X] : THEORY
BEGIN

  x: VAR X1
  S : VAR {R: equivalence[X] | PreservesEq[X, X, bool](R)(X1_pred)}

  QuotientSub(S) : TYPE =
    { P :set[X] | EXISTS x : P = EquivClass(S)(x) }

  quotient_sub_map(S)(x) : QuotientSub(S) =
    EquivClass(S)(x)

END QuotientSubDefinition


QuotientExtensionProperties[X : TYPE, X1: TYPE FROM X, Y : TYPE] : THEORY
BEGIN

  S : VAR {R: equivalence[X] | PreservesEq[X, X, bool](R)(X1_pred)}

  lift(S)
      (g : (PreservesEq[X, X1, Y](S)))
      (P : QuotientSub[X, X1](S))
      : Y
    = g(rep(S)(P))

  lift_commutation : LEMMA
    FORALL (S),
           (g : (PreservesEq[X, X1, Y](S))) : 
      lift(S)(g) o quotient_sub_map[X, X1](S) = g

  lift_unicity : LEMMA
    FORALL (S | PreservesEq[X, X, bool](S)(X1_pred)),
           (g : (PreservesEq[X, X1, Y](S))) :
      FORALL(h : [QuotientSub[X, X1](S) -> Y]) :
        h o quotient_sub_map[X, X1](S) = g IMPLIES h = lift(S)(g)

END QuotientExtensionProperties


QuotientDistributive[X, Y: TYPE] : THEORY
BEGIN

% This theory makes clear that quotients commute with products: there is an isomorphism 
%
%     [X/S, Y] iso [X,Y]/EqualityExtension(S)
%
% given by the canonical map (from right to left). Such distributivity
% results can be used to define functions with several parameters on a
% quotient.  In the presence of function types, this can also be done
% via Currying.  The result is included here mainly as a test for the
% formalisation of quotients.
%

  S : VAR equivalence[X]
  z, w : VAR [X, Y]

  EqualityExtension(S) : set[[[X, Y], [X, Y]]] =
    { (z, w) | S(z`1, w`1) AND z`2 = w`2  }

  EqualityExtension_is_equivalence: JUDGEMENT
    EqualityExtension(S) HAS_TYPE equivalence[[X, Y]]

  EqualityExtensionPreservesEq : LEMMA
    PreservesEq[[X, Y], [X, Y], [Quotient(S), Y]]
        (EqualityExtension(S))
        (LAMBDA(x : X, y : Y) : (quotient_map(S)(x), y))

  QuotientDistributive : LEMMA
    bijective?[Quotient(EqualityExtension(S)), [Quotient(S), Y]]
      (lift[[X, Y], [X, Y], [Quotient(S), Y]](EqualityExtension(S))
           (LAMBDA(x : X, y : Y) : (quotient_map(S)(x), y)))

  %     [X/S, Y/R] iso [X,Y]/RelExtension(S,R)

  R: VAR equivalence[Y]

  RelExtension(S, R) : equivalence[[X, Y]] =
    { (z, w) | S(z`1, w`1) AND R(z`2, w`2) }

  RelExtensionPreservesEq : LEMMA
    PreservesEq[[X, Y], [X, Y], [Quotient(S), Quotient(R)]]
        (RelExtension(S,R))
        (LAMBDA(x : X, y : Y) : (quotient_map(S)(x), quotient_map(R)(y)))

  RelQuotientDistributive : LEMMA
    bijective?[Quotient(RelExtension(S,R)), [Quotient(S), Quotient(R)]]
      (lift[[X, Y], [X, Y], [Quotient(S), Quotient(R)]](RelExtension(S, R))
           (LAMBDA(x : X, y : Y) : (quotient_map(S)(x), quotient_map(R)(y))))

  %     F: [X -> equivalence[Y]]
  %        [x:X -> Y/F(x)] iso [X -> Y]/FunExtension(F)
  F: VAR [X -> equivalence[Y]]
  f, g : VAR [X -> Y]

  FunExtension(F) : equivalence[[X -> Y]] =
    { (f, g) | FORALL (x : X) : F(x)(f(x), g(x)) }

  FunExtensionPreservesEq : LEMMA
    PreservesEq[[X -> Y], [X -> Y], [x : X -> Quotient(F(x))]]
        (FunExtension(F))
        (LAMBDA(f : [X -> Y]) : LAMBDA (x : X) : quotient_map(F(x))(f(x)))

  FunQuotientDistributive : LEMMA
    bijective?[Quotient(FunExtension(F)), [x : X -> Quotient(F(x))]]
      (lift[[X -> Y], [X -> Y], [x : X -> Quotient(F(x))]](FunExtension(F))
           (LAMBDA(f : [X -> Y]) : (LAMBDA (x : X): (quotient_map(F(x))(f(x))))))

END QuotientDistributive


QuotientIteration[X : TYPE] : THEORY
BEGIN

% In this theory it will be shown how successive quotients can be reduced
% to a single quotient:
% 
%     (X/S)/R iso X/action(S)(R)
%
% again via the canonical map.

  S : VAR equivalence[X]
  x, y : VAR X

  action(S)(R : equivalence[Quotient(S)])(x, y) : bool =
    R(EquivClass(S)(x), EquivClass(S)(y))

  action_equivalence_is_equivalence: JUDGEMENT
    action(S)(R : equivalence[Quotient(S)]) HAS_TYPE equivalence[X]

  QuotientAction : LEMMA
    FORALL(R : equivalence[Quotient(S)]) :
      bijective?[Quotient(R), Quotient(action(S)(R))]
        (lift[Quotient(S), Quotient(S), Quotient(action(S)(R))](R)
           (lift[X, X, Quotient(action(S)(R))](S)
              (quotient_map[X](action(S)(R)))))

END QuotientIteration


% The following theory illustrates how the lift type can be used
% to describe partial functions from X to Y, namely as total
% functions from X to lift[Y].

PartialFunctionDefinitions[X, Y : TYPE] : THEORY
BEGIN

% Two representations of partial functions are described,
% and shown to be isomorphic. In practice, the formulation
% based on lift is more convenient, because definitions
% are easier and fewer TCCs are generated.

  SubsetPartialFunction : TYPE =
    [# dom : PRED[X], fun : [(dom) -> Y] #]

  LiftPartialFunction : TYPE =
    [X -> lift[Y]]

  f : VAR LiftPartialFunction
  g : VAR SubsetPartialFunction
  h : VAR [X -> Y]

  SPartFun_appl(g): [(dom(g)) -> Y] = g`fun

  SPartFun_to_LPartFun(g) : LiftPartialFunction =
    LAMBDA(x : X) : IF dom(g)(x) THEN up(fun(g)(x)) ELSE bottom ENDIF

  LPartFun_to_SPartFun(f) : SubsetPartialFunction =
    (# 
      dom := {x : X | up?(f(x))}, 
      fun := LAMBDA(y : {x : X | up?(f(x))}) : down(f(y))
    #)

  TotalFun_to_SPartFun(h): SubsetPartialFunction =
    (#
      dom := {x : X | TRUE},
      fun := h
    #)

  TotalFun_to_LPartFun(h): LiftPartialFunction =
    LAMBDA(x : X) : up(h(x))

  CONVERSION SPartFun_appl,
             SPartFun_to_LPartFun, LPartFun_to_SPartFun,
             TotalFun_to_SPartFun, TotalFun_to_LPartFun

  SPartFun_to_LPartFun_to_SPartFun : LEMMA
    LPartFun_to_SPartFun(SPartFun_to_LPartFun(g)) = g

  LPartFun_to_SPartFun_to_LPartFun : LEMMA
    SPartFun_to_LPartFun(LPartFun_to_SPartFun(f)) = f

END PartialFunctionDefinitions


PartialFunctionComposition[X, Y, Z : TYPE] : THEORY
BEGIN

  f : VAR LiftPartialFunction[X, Y]
  g : VAR LiftPartialFunction[Y, Z]

  o(g, f) : LiftPartialFunction[X, Z] =
    LAMBDA(x : X) :
      CASES f(x) OF
        bottom : bottom,
        up(y) : g(y)
      ENDCASES

  h : VAR SubsetPartialFunction[X, Y]
  k : VAR SubsetPartialFunction[Y, Z]

  CompDom(k, h) : PRED[X] =
    { x : X | dom(h)(x) AND dom(k)(fun(h)(x)) };

  o(k, h) : SubsetPartialFunction[X, Z] =
    (# 
      dom := CompDom(k, h),
      fun := LAMBDA(x : (CompDom(k, h))) : fun(k)(fun(h)(x))
    #)

  SPartFun_to_LPartFun_CompositionPreservation : LEMMA
    SPartFun_to_LPartFun(k o h)
      = SPartFun_to_LPartFun(k) o SPartFun_to_LPartFun(h)

  LPartFun_to_SPartFun_CompositionPreservation : LEMMA
    LPartFun_to_SPartFun(g o f)
      = LPartFun_to_SPartFun(g) o LPartFun_to_SPartFun(f)

END PartialFunctionComposition

% PVSio support theories

%% stdlang 
%% Basic language definitions

stdlang : THEORY
BEGIN

  void : TYPE = bool

  skip : void = true
  fail : void = false

  try(s1:void,s2:void)  : MACRO void = s1 OR s2
  try(s:void)           : MACRO void = try(s,skip)
  ifthen(b:bool,s:void) : MACRO void = IF b THEN s ELSE skip ENDIF
  ifelse(b:bool,s:void) : MACRO void = IF b THEN skip ELSE s ENDIF

  Dummy : TYPE  = bool
  dummy : MACRO Dummy = false

END stdlang


%% stdexc.pvs
%% Definition of exception type

stdexc[T:TYPE+] : THEORY
BEGIN

  ExceptionTag : TYPE = string

  Exception : TYPE = [#
    tag : ExceptionTag,
    val : T
  #]

  make_exc(e:ExceptionTag,t:T) : Exception = (#
    tag := e,
    val := t
  #)

END stdexc

%% stdcatch.pvs
%% Definition of catch and throw 

stdcatch[T1,T2:TYPE+] : THEORY
BEGIN

  catch_lift(tag:ExceptionTag[T2],
             t1:[Dummy->T1],
             t2:[Exception[T2]->T1]) : T1

  catch(tag:ExceptionTag[T2],
        t1:T1,
        t2:[Exception[T2]->T1]) : MACRO T1 =
    catch_lift(tag,LAMBDA(d:Dummy):t1,t2)

  catch_list_lift(l:list[ExceptionTag[T2]],
                  f1:[Dummy->T1],
                  f2:[Exception[T2]->T1]) : RECURSIVE T1 =
    CASES l OF
      null : f1(dummy),
      cons(e,r) : catch_lift(e,
                             LAMBDA(d:Dummy):catch_list_lift(r,f1,f2),
                             f2)
    ENDCASES
    MEASURE l BY <<  

  catch(l:list[ExceptionTag[T2]],t1:T1,t2:[Exception[T2]->T1]) : MACRO T1 =
    catch_list_lift(l,LAMBDA(d:Dummy):t1,t2)

  throw(tag:ExceptionTag[T2],e:Exception[T2]):T1

  throw(tag:ExceptionTag[T2],val:T2) : MACRO T1 =
    throw(tag,make_exc(tag,val))

END stdcatch

%% stdprog.pvs
%% Imperative aspects such as errors, exceptions, mutables and loops

stdprog[T:TYPE+] : THEORY
BEGIN

  prog(s:void,t:T): T = t

  % Errors and Exceptions
  error(mssg:string):T 

  % Exists the current evaluation and returns to the Ground Evaluator
  exit : T

  catch(tag:ExceptionTag[void],t1,t2:T): MACRO T =
    catch_lift[T,void](tag,LAMBDA(d:Dummy):t1,LAMBDA(e:Exception[void]):t2)

  throw(tag:ExceptionTag[void]): MACRO T = throw[T,void](tag,fail)

  catch(l:list[ExceptionTag[void]],t1,t2:T) : MACRO T =
    catch_list_lift[T,void](l,LAMBDA(d:Dummy):t1,LAMBDA(e:Exception[void]):t2)

  % Mutable data
  UndefinedMutableVariable : ExceptionTag[void] = "UndefinedMutableVariable"

  Mutable : TYPE+

  ref(t:T) : Mutable

  new      : Mutable 

  undef(v:Mutable)    : bool

  val_lisp(v:Mutable) : T

  val(v:Mutable): T = 
    if undef(v) then 
      throw(UndefinedMutableVariable)
    else val_lisp(v)
    endif

  def(v:Mutable,t:T) : T = t

  set(v:Mutable,t:T) : void = 
    let nt = def(v,t) in
    skip

  CONVERSION val

  % Global uninitilized variables
  Global : TYPE+ = Mutable

  % Loops
  loop_lift(f:[Dummy->void]): T

  loop(s:void): MACRO T = loop_lift(LAMBDA(d:Dummy):s)

  return(t:T):void = fail

  % Formatting text
  format(s:string,t:T):string

END stdprog

%% stdglobal.pvs
%% Global variables

stdglobal[T:TYPE+,t:T] : THEORY
BEGIN

  Global  : TYPE+ = Mutable[T]

END stdglobal

%% stdpvs.pvs
%% PVS printing and parsing

stdpvs[T:TYPE+] : THEORY
BEGIN

  typeof(t:T) : string

  str2pvs(s:string):T 

  pvs2str_lisp(t:T) : string

  pvs2str(t:T) : MACRO string =
    catch("cant-translate",	
	  pvs2str_lisp(t),
          LAMBDA(e:Exception[void]):"<?>")

  Slisp : TYPE+  

  slisp(l:list[T]) : Slisp

  {||}(l:list[T]) : Slisp = slisp(l)

END stdpvs

%% stdstr.pvs
%% String operations

stdstr: THEORY
BEGIN

  NotARealNumber : ExceptionTag[string] = "NotARealNumber"
  NotAnInteger   : ExceptionTag[string] = "NotAnInteger"

% Char from code n
  charcode(n:nat) : string

% Prints standard table of characters
  chartable       : void 

  emptystr      : string = ""
  space         : string = " "
  newline       : string 
  tab           : string 
  doublequote   : string = charcode(34)
  singlequote   : string = "'"
  backquote     : string = "`"
  spaces(n:nat) : string 

  upcase(s:string):string
  downcase(s:string):string
  capitalize(s:string):string
  
  %% Index of leftmost occurrence of s1 in s2, 2, starting from 0, or -1 if none
  strfind(s1,s2:string):int

  %% Substring S[i..j] if i <= j, S[j..i] if j <= i, empty if indices are out of range
  substr(s:string,i,j:nat):string

  %% Real to string
  real2str(r:real): string

  %% Bool to string
  bool2str(b:bool): string =
    IF b THEN "TRUE" ELSE "FALSE" ENDIF

  tostr(r:real): MACRO string = real2str(r)
  tostr(b:bool): MACRO string = bool2str(b)

  %% String to real
  str2real(s:string): rat
  str2int(s:string) : int 
  str2bool(s,answer:string):bool = downcase(s) = downcase(answer)

  %% String is a number
  number?(s:string):bool

  %% String is an integer
  int?(s:string):bool

 %% String concatenation
  concat(s1:string,s2:string):string = s1 o s2
  ;+(s1:string,s2:string): MACRO string = concat(s1,s2)
  ;+(r:real,s:string): MACRO string = concat(tostr(r),s)
  ;+(s:string,r:real): MACRO string = concat(s,tostr(r))
  ;+(b:bool,s:string): MACRO string = concat(tostr(b),s)
  ;+(s:string,b:bool): MACRO string = concat(s,tostr(b))

  %% Concatenates n-times string s
  pad(n:nat,s:string): RECURSIVE string = 
    IF n=0 THEN emptystr
    ELSE s+pad(n-1,s)
    ENDIF
    MEASURE n

  %% String comparison
  %% = 0 if s1 = s2
  %% < 0 if s1 < s2
  %% > 0 if s1 > s2

  strcmp(s1,s2:string,sensitive:bool):int

  strcmp(s1,s2:string): MACRO int = 
    strcmp(s1,s2,true)

  %% A substring of s2, with all the characters in s1 stripped of 
  %% the beginning and end
  strtrim(s1,s2:string):string

  %% Returns a substring of s2, with all the characters in s1 stripped of 
  %% the beginning 
  strtrim_left(s1,s2:string):string

  %% Returns a substring of s2, with all the characters in s1 stripped of 
  %% the end
  strtrim_right(s1,s2:string):string

  %% Returns a substring of s, with all the space characters stripped of 
  %% the beginning and end
  trim(s:string):string

  %% Returns a substring of s, with all the space characters stripped of 
  %% the beginning 
  trim_left(s:string):string

  %% Returns a substring of s, with all the space characters stripped of 
  %% the end
  trim_right(s:string):string

  %% Returns the name part of a file name
  filename(s:string):string

  %% Returns the directory part of a file name
  directory(s:string):string

END stdstr

%% stdio.pvs
%% Input/output operations

stdio : THEORY
BEGIN

%% I/O Exceptions
  FileNotFound          : ExceptionTag[string] = "FileNotFound"
  FileAlreadyExists     : ExceptionTag[string] = "FileAlreadyExists"
  WrongInputStreamMode  : ExceptionTag[string] = "WrongInputStreamMode"
  WrongOutputStreamMode : ExceptionTag[string] = "WrongOutputStreamMode"
  ClosedStream          : ExceptionTag[string] = "ClosedStream"
  EndOfFile             : ExceptionTag[string] = "EndOfFile"
  
  IOExceptionTags : list[ExceptionTag[string]] = 
    (: NotARealNumber, NotAnInteger, FileNotFound,
       FileAlreadyExists, WrongInputStreamMode, WrongOutputStreamMode,
       ClosedStream, EndOfFile :)

%% Assert
  assert(b:bool,str:string):void =
    try(b,error[void]("[Assertion Failure] "+str) & fail)

%% While loops
  break : MACRO void = return(skip)

  while(b:bool,s:void) : MACRO void =
    loop(if b then s else break endif)

  for(si:void,b:bool,sinc,s:void): MACRO void =
    si & while(b,s&sinc)

%% Print, Println 

  %% Prints lisp format of string s
  printstr(s:string):void = skip

  print(s:string)   : MACRO void = printstr(s)
  print(r:real)     : MACRO void = print(r+emptystr)
  print(b:bool)     : MACRO void = print(b+emptystr)
  println(s:string) : MACRO void = print(s+newline)
  println(r:real)   : MACRO void = print(r+newline)
  println(b:bool)   : MACRO void = print(b+newline)

%% Reading

  % Querying from stdin with prompt message
  query_token(mssg,s:string): string
  query_word(mssg:string)   : MACRO string = query_token(mssg,emptystr) 
  query_line(mssg:string)   : string
  query_real(mssg:string)   : rat
  query_int(mssg:string)    : int
  query_bool(mssg,answer:string):bool = str2bool(query_word(mssg),answer)

  % Reads from stdin
  read_token(s:string): MACRO string = query_token(emptystr,s) 
  read_word : MACRO string = query_word(emptystr)
  read_line : MACRO string = query_line(emptystr)
  read_real : MACRO rat    = query_real(emptystr)
  read_int  : MACRO int    = query_int(emptystr)
  read_bool(answer:string): MACRO bool   = query_bool(emptystr,answer)

%% Character Streams
  Stream   : TYPE+ 
  IStream  : TYPE+ FROM Stream
  OStream  : TYPE+ FROM Stream

  fclose(f:Stream)     :void =   %% Close an stream
    skip
  fexists(s:string)    :bool     %% true IFF file s exists
  fopen?(f:Stream)     :bool     %% Open stream?
  strstream?(f:Stream) :bool     %% String stream?
  filestream?(f:Stream):bool     %% File stream?
  sdtstream?(f:Stream) :bool =   %% Standard stream?
    NOT (filestream?(f) OR strstream?(f))
  finput?(f:Stream)    :bool     %% Input stream?
  foutput?(f:Stream)   :bool     %% Output stream?

%% Standard I/O Steams
  stdin    : IStream 
  stdout   : OStream 
  stderr   : OStream

  Mode   : TYPE = {input,output,create,append,overwrite,rename,str}

  mode2str(m:Mode) : string = CASES m OF
    input     : "input",
    output    : "output",
    create    : "create",
    append    : "append",
    overwrite : "overwrite",
    rename    : "rename",
    str       : "str"
  ENDCASES

  tostr(m:Mode) : MACRO string = mode2str(m) 

  fopenin_lisp(s:string)        : IStream 
  fopenout_lisp(s:string,n:nat) : OStream 
  sopenin(s:string)             : IStream
  sopenout(s:string)            : OStream

  % Opens a file as an input stream
  fopenin(m:Mode,s:string) : IStream = 
    IF    m = input AND length(s)=0 THEN stdin 
    ELSIF m = input THEN fopenin_lisp(s)
    ELSIF m = str   THEN sopenin(s)
    ELSE throw(WrongInputStreamMode,tostr(m))
    ENDIF

  fopenin(s:string) : IStream = 
    fopenin_lisp(s)

  % Opens a file as an oput stream
  fopenout(m:Mode,s:string): OStream =
    IF    m = output AND length(s)=0 THEN stdout
    ELSIF m = output    THEN fopenout_lisp(s,0) 
    ELSIF m = create    THEN fopenout_lisp(s,1)
    ELSIF m = append    THEN fopenout_lisp(s,2)
    ELSIF m = overwrite THEN fopenout_lisp(s,3)
    ELSIF m = rename    THEN fopenout_lisp(s,4)
    ELSIF m = str       THEN sopenout(s)
    ELSE throw(WrongOutputStreamMode,tostr(m))
    ENDIF

  fopenout(s:string) : OStream =
    fopenout(output,s)

  fname_lisp(f:Stream)           :string
  fgetstr_lisp(f:OStream)        :string
  eof_lisp(f:IStream)            :bool           
  flength_lisp(f:Stream)         :nat          
  fgetpos_lisp(f:Stream)         :nat         
  fsetpos_lisp(f:Stream,n:nat)   :void   
  fprint_lisp(f:OStream,s:string):void = skip

  % Gets the full name of a file string
  fname(f:Stream):string =
    if filestream?(f) then 
      fname_lisp(f)
    else
      emptystr
    endif

  % Gets string from an *output string* stream 
  fgetstr(f:OStream):string =
    if fopen?(f) then fgetstr_lisp(f)
    else throw(ClosedStream,fname(f))
    endif

  %% true IFF f has reached EOF
  eof?(f:IStream):bool =
    if fopen?(f) then eof_lisp(f)
    else throw(ClosedStream,fname(f))
    endif

  %% Length of stream 
  flength(f:Stream):nat =
    if fopen?(f) then flength_lisp(f)
    else throw(ClosedStream,fname(f))
    endif

  %% Gets current position 
  fgetpos(f:Stream):nat = 
    if fopen?(f) then fgetpos_lisp(f)
    else throw(ClosedStream,fname(f))
    endif

  % Prints to a stream
  fprint(f:OStream,s:string):void = 
    if fopen?(f) then fprint_lisp(f,s)
    else throw(ClosedStream,fname(f))
    endif
  fprint(f:OStream,r:real)    : MACRO void = fprint(f,r+emptystr)
  fprint(f:OStream,b:bool)    : MACRO void = fprint(f,b+emptystr)
  
  %% Sets current positions
  fsetpos(f:Stream,n:nat):void =
    if fopen?(f) then fsetpos_lisp(f,n)
    else throw(ClosedStream,fname(f))
    endif

  % Printlns to a stream
  fprintln(f:OStream,s:string): MACRO void = fprint(f,s+newline)
  fprintln(f:OStream,r:real)  : MACRO void = fprint(f,r+newline)
  fprintln(f:OStream,b:bool)  : MACRO void = fprint(f,b+newline)

  % Prints to a stream and echoes to stdout
  echo(f:OStream,s:string): MACRO void = print(s) & fprint(f,s) 
  echo(f:OStream,r:real)  : MACRO void = print(r) & fprint(f,r) 
  echo(f:OStream,b:bool)  : MACRO void = print(b) & fprint(f,b) 

  % Printlns to a stream and echo to stdout
  echoln(f:OStream,s:string): MACRO void = println(s) & fprintln(f,s)
  echoln(f:OStream,r:real)  : MACRO void = println(r) & fprintln(f,r) 
  echoln(f:OStream,b:bool)  : MACRO void = println(b) & fprintln(f,b) 

%% Input functions
  fread_token_lisp(f:IStream,s:string) : string
  fread_line_lisp(f:IStream) : string
  fread_real_lisp(f:IStream) : rat
  fread_int_lisp(f:IStream)  : int

  fcheck(f:IStream): bool = 
    (fopen?(f)   OR throw(ClosedStream,fname(f))) AND
    (NOT eof?(f) OR throw(EndOfFile,fname(f)))

  % Reads a token from f separated by characters in s from a stream
  fread_token(f:IStream,s:string) : string =
    prog(fcheck(f),fread_token_lisp(f,s))

  % Reads a word from f
  fread_word(f:IStream) : MACRO string =
    fread_token(f,emptystr)

  % Reads a line from f
  fread_line(f:IStream) : string =
    prog(fcheck(f),fread_line_lisp(f))

  % Reads a real number from f
  fread_real(f:IStream) : rat =
    prog(fcheck(f),fread_real_lisp(f))

  % Reads an integer from f
  fread_int(f:IStream)  : int =
    prog(fcheck(f),fread_int_lisp(f))

  % Reads a boolean from f
  fread_bool(f:IStream,answer:string): MACRO bool=
    str2bool(fread_word(f),answer)

END stdio

%% stdmath.pvs
%% PVSio math library 

stdmath : THEORY
BEGIN

  %% sq is available in the theory reals@sq
  %% div and mod are available through the theories
  %% ints@div_nat, ints@mod_nat

%% Math Exceptions
  MathExceptions : list[ExceptionTag[string]] = 
   (: NotARealNumber, NotAnInteger :)

  PI                : posreal 
  SIN(x:real)       : {x:real| -1 <= x and x <= 1}
  COS(y:real)       : {x:real| -1 <= x and x <= 1}
  EXP(x:real)       : posreal
  RANDOM            : {y:nnreal | 0 <= y AND y <= 1} 
  NRANDOM(n:posnat) : {y:nat | 0 <= y AND y < n} 

  sqrt_lisp(x:nnreal) : nnreal
  log_lisp(x:posreal) : real
  atan_lisp(x,y:real) : real
  asin_lisp(x:real)   : real    
  acos_lisp(x:real)   : real    

  SQRT(x:real):nnreal =
    IF x < 0 THEN 
      throw[nnreal,string](NotARealNumber,"SQRT("+x+")")
    ELSE sqrt_lisp(x)
    ENDIF

  LOG(x:real):real =
    IF x <= 0 THEN 
      throw[real,string](NotARealNumber,"LOG("+x+")")
    ELSE log_lisp(x)
    ENDIF

  TAN(x:real):real =
    LET d = COS(x) IN
    IF d = 0 THEN 
      throw[real,string](NotARealNumber,"TAN("+x+"0)")
    ELSE
      SIN(x)/COS(x)
    ENDIF

  ATAN(y,x:real):real = 
    IF x=0 AND y= 0 THEN 
      throw[real,string](NotARealNumber,"ATAN(0,0)")
    ELSE atan_lisp(y,x)
    ENDIF

  ASIN(x:real) : real =
    IF x < -1 OR x > 1 THEN
      throw[real,string](NotARealNumber,"ASIN("+x+")")
    ELSE asin_lisp(x)
    ENDIF
 
  ACOS(x:real) : real =
    IF x < -1 OR x > 1 THEN
      throw[real,string](NotARealNumber,"ACOS("+x+")")
    ELSE acos_lisp(x)
    ENDIF

  BRANDOM: bool =
    (NRANDOM(2) = 0)

END stdmath

%% stdfmap.pvs
%% Iterations on files and format printing

stdfmap[T:TYPE+] : THEORY
BEGIN

  % Iterates a function on a file n times
  fmap(f:IStream,fread:[IStream->string],t:T,st:[[string,T]->T],n:nat) : 
    RECURSIVE T =
    IF fopen?(f) THEN
      IF n=0 or eof?(f) THEN t
      ELSE
        LET s  = fread(f) IN
        LET nt = st(s,t) IN
          fmap(f,fread,nt,st,n-1)
      ENDIF
    ELSE throw(ClosedStream,fname(f))
    ENDIF
    MEASURE n

  % Iterates a function on a file n times until the end
  fmap(f:IStream,fread:[IStream->string],t:T,st:[[string,T]->T]) : T =
    let l  = flength(f) in
    let nt = fmap(f,fread,t,st,l) in  
    prog(fclose(f),nt)

  % Iterates a function on a file line by line until the end
  fmap_line(f:IStream,t:T,st:[[string,T]->T]):T =
    let l  = flength(f) in
    let nt = fmap(f,fread_line,t,st,l) in  
    prog(fclose(f),nt)

  % Formatting text to a file
  printf(s:string,t:T): MACRO void =
    print(format(s,t))

  fprintf(f:OStream,s:string,t:T): MACRO void =
    fprint(f,format(s,t))

END stdfmap

%% stdindent.pvs
%% Indentations

stdindent : THEORY
BEGIN

  %% Indentation
  Indent : TYPE+
  
  create_indent(n:nat,s:string):Indent
  push_indent(i:Indent,n:nat):void
  pop_indent(i:Indent):void
  top_indent(i:Indent):nat
  get_indent(i:Indent):nat
  set_indent(i:Indent,n:nat):void
  get_prefix(i:Indent):string
  set_prefix(i:Indent,s:string):void

  create_indent(n:nat)         : MACRO Indent = create_indent(n,emptystr)
  open_block(i:Indent,n:nat)   : MACRO void = push_indent(i,n)
  open_block(i:Indent)         : MACRO void = push_indent(i,get_indent(i))
  close_block(i:Indent)        : MACRO void = pop_indent(i)

  indent(i:Indent):string = get_prefix(i)+spaces(top_indent(i))
  indent(i:Indent,s:string):string = indent(i)+s

  prindent(i:Indent,s:string):void = print(indent(i,s))
  prindentln(i:Indent,s:string):void = println(indent(i,s))

  fprindent(f:OStream,i:Indent,s:string):void = fprint(f,indent(i,s))
  fprindentln(f:OStream,i:Indent,s:string):void = fprintln(f,indent(i,s))

  %% Formatting functions

  center(col:nat,s:string):string = format("~"+col+":@<~a~>",s)

  flushleft(col:nat,s:string) :string = format("~"+col+"a",s)

  flushright(col:nat,s:string):string = format("~"+col+"@a",s)

END stdindent

%% stdtokenizer.pvs
%% Tokenizers

stdtokenizer : THEORY
BEGIN
 
  %% Error Codes
  %% Negative numbers are user defined
  NoError           : nat = 0
  FileNotFound      : nat = 1
  EndOfTokenizer    : nat = 2
  InvalidToken      : nat = 3
  ExpectingWord     : nat = 4
  ExpectingTestWord : nat = 5
  ExpectingInt      : nat = 6
  ExpectingTestInt  : nat = 7
  ExpectingReal     : nat = 8
  ExpectingTestReal : nat = 9

  Tokenizer : TYPE = [#
    stream   : ARRAY[nat->string],
    lines    : ARRAY[nat->nat],
    casesen  : boolean,
    separ    : string,
    error    : int,
    val_int  : int,
    val_real : real,
    length   : nat,
    pos      : upto(length)
  #]

  init_tokenizer(casesen:bool,separ:string) : Tokenizer = (#
    stream   := LAMBDA(x:nat):emptystr,
    lines    := LAMBDA(x:nat):0,
    casesen  := casesen,
    separ    := separ,
    error    := NoError,
    val_int  := 0,
    val_real := 0, 
    length   := 0,
    pos      := 0
  #)

  empty_tokenizer : Tokenizer = (#
    stream   := LAMBDA(x:nat):emptystr,
    lines    := LAMBDA(x:nat):0,
    casesen  := true,
    separ    := emptystr,
    error    := NoError,
    val_int  := 0,
    val_real := 0, 
    length   := 0,
    pos      := 0
  #)

  TokenizerOfLength(l:int): TYPE = {t:Tokenizer | t`length = l}

  set_casesen(t:Tokenizer,c:bool):Tokenizer =
    t with [`casesen := c]

  %% Error?
  error?(t:Tokenizer): MACRO bool = 
    t`error /= NoError
 
  %% Set Error
  set_error(t:Tokenizer,code:int): TokenizerOfLength(t`length) =
    t WITH [`error:= code]

  %% Last processed token
  last_token(t:Tokenizer): string =
    IF t`pos = 0 THEN emptystr
    ELSE t`stream(t`pos-1)
    ENDIF

  %% Peek token at current position + offset n
  peek(t:Tokenizer,n:posnat): MACRO string = t`stream(t`pos+n-1)

  %% Next unprocessed token
  next_token(t:Tokenizer) : MACRO string = peek(t,1)

  tostr(t:Tokenizer,i:upto(t`length)) : RECURSIVE string =
    IF i = t`length THEN emptystr
    ELSIF i=t`pos THEN
      "["+t`stream(i)+"] " + tostr(t,i+1)
    ELSE 
      t`stream(i)+space + tostr(t,i+1)
    ENDIF
    MEASURE t`length - i

  add_token(s:string,t:Tokenizer,l:nat): MACRO Tokenizer =
    LET n = t`length IN
    t WITH [`stream(n) := s,
            `lines(n)  := l,
            `length    := n + 1]

  read_token(t:Tokenizer)(f:IStream):string = fread_token(f,t`separ)

  line_tokenizer(s:string,tl:[Tokenizer,nat]):[Tokenizer,nat] =
    LET (t,l) = tl IN
    LET g = fopenin(str,s) IN
    LET f = (LAMBDA(mys:string,myt:Tokenizer):add_token(mys,myt,l)) IN
    LET nt = fmap(g,read_token(t),t,f,length(s)) IN
    prog(fclose(g),(nt,l+1))

  %% Create a tokenizer from a files
  file2tokenizer(s:string,t:Tokenizer):Tokenizer=
    IF fexists(s) THEN 
      LET (nt,l) = fmap_line(fopenin(s),
                             (t,1),
                             line_tokenizer) IN 
        nt
    ELSE	
      LET filename = s IN
      t WITH [
        `stream(0) := filename,
        `error     := FileNotFound
      ]
    ENDIF

  file2tokenizer(s:string):Tokenizer=
    file2tokenizer(s,empty_tokenizer)

  %% Create a tokenizer from a string
  str2tokenizer(s:string,t:Tokenizer):Tokenizer= 
    LET f = fopenin(str,s) IN
    LET (nt,l) = fmap_line(f,(t,1),line_tokenizer) IN 
        nt

  str2tokenizer(s:string):Tokenizer=
    str2tokenizer(s,empty_tokenizer)

  % EOT = End of tokenizer
  eot?(t:Tokenizer) : bool = t`pos = t`length

  % Current line
  get_line(t:Tokenizer) : MACRO nat = t`lines(t`pos) 

  consume(t:Tokenizer,n:posnat) : TokenizerOfLength(t`length) = 
    IF error?(t) THEN t
    ELSIF eot?(t) OR t`pos + n > t`length THEN 
      t WITH [`error := EndOfTokenizer]
    ELSE 
      t WITH [`pos := t`pos + n]
    ENDIF

  go_next(t:Tokenizer) : MACRO TokenizerOfLength(t`length) = 
    consume(t,1)
 
  go_back(t:Tokenizer) : TokenizerOfLength(t`length) = 
    IF t`pos = 0 THEN t
    ELSE 
      t WITH [`pos := t`pos - 1]
    ENDIF

  pos_go_next : LEMMA
    FORALL (t1:Tokenizer):
      LET t2= go_next(t1) IN
      NOT error?(t2) IMPLIES t2`pos = t1`pos+1

  %% Accepts a word that satisfies test
  accept_word(t:Tokenizer,test:[string->bool])
    : TokenizerOfLength(t`length) =
    IF error?(t) THEN t
    ELSIF eot?(t) THEN 
      t WITH [`error := EndOfTokenizer]
    ELSIF number?(t`stream(t`pos)) THEN
      t WITH [`error := ExpectingWord]
    ELSIF test(t`stream(t`pos)) THEN 
      t WITH [`pos := t`pos + 1]
    ELSE 
      t WITH [`error := ExpectingTestWord]
    ENDIF

  pos_accept_word : LEMMA
    FORALL (t1:Tokenizer,test:[string->bool]):
      LET t2= accept_word(t1,test) IN
      NOT error?(t2) IMPLIES t2`pos = t1`pos+1

  the_word(s:string)(token:string):bool =
     str2bool(s,token)

  %% Accepts the word s
  accept_word(t:Tokenizer,s:string) : MACRO TokenizerOfLength(t`length) =
    accept_word(t,the_word(s))

  any_word(token:string):bool = TRUE

  %% Accepts any word
  accept_word(t:Tokenizer) : MACRO TokenizerOfLength(t`length) =
    accept_word(t,any_word)

  %% Accepts an integer that satisfies test
  accept_int(t:Tokenizer,test:[int->bool])
    : TokenizerOfLength(t`length) =
    IF error?(t) THEN t
    ELSIF eot?(t) THEN 
      t WITH [`error := EndOfTokenizer]
    ELSIF NOT int?(t`stream(t`pos)) THEN
      t WITH [`error := ExpectingInt]
    ELSE
      LET i = str2int(t`stream(t`pos)) IN
      IF test(i) THEN 
        t WITH [`pos := t`pos + 1, `val_int := i, `val_real := i]

      ELSE 
        t WITH [`error := ExpectingTestInt]
      ENDIF
    ENDIF

  pos_accept_int : LEMMA
    FORALL (t1:Tokenizer,test:[int->bool]):
      LET t2= accept_int(t1,test) IN
      NOT error?(t2) IMPLIES t2`pos = t1`pos+1

  any_int(i:int):bool = TRUE

  %% Accepts any integer 
  accept_int(t:Tokenizer) : MACRO TokenizerOfLength(t`length) =
    accept_int(t,any_int)

  %% Accepts a real that satisfies test
  accept_real(t:Tokenizer,test:[real->bool])
    : TokenizerOfLength(t`length) =
    IF error?(t) THEN t
    ELSIF eot?(t) THEN 
      t WITH [`error := EndOfTokenizer]
    ELSIF NOT number?(t`stream(t`pos)) THEN
      t WITH [`error := ExpectingReal]
    ELSE
      LET r = str2real(t`stream(t`pos)) IN
      IF test(r) THEN 
        t WITH [`pos := t`pos + 1, `val_real := r]

      ELSE 
        t WITH [`error := ExpectingTestReal]
      ENDIF
    ENDIF

  pos_accept_real : LEMMA
    FORALL (t1:Tokenizer,test:[real->bool]):
      LET t2= accept_real(t1,test) IN
      NOT error?(t2) IMPLIES t2`pos = t1`pos+1

  any_real(r:real):bool = TRUE

  %% Accepts any real
  accept_real(t:Tokenizer) : MACRO TokenizerOfLength(t`length) =
    accept_real(t,any_real)

  %% Messengers

  Messenger : TYPE = [int->string]

  std_mssg(t:Tokenizer)(code:int):string =
    IF    code <= 0 THEN emptystr
    ELSIF code = FileNotFound THEN
      "File not found: "+doublequote+next_token(t)+doublequote+"."
    ELSIF code = EndOfTokenizer THEN
      "Found EOT."
    ELSIF code = InvalidToken THEN 
      "Invalid Token: "+doublequote+next_token(t)+doublequote+"."
    ELSIF code = ExpectingWord THEN 
      "Expecting a word. Found: "+doublequote+next_token(t)+doublequote+"."
    ELSIF code = ExpectingTestWord THEN 
      "Expecting word that satisfies test. Found: "+doublequote+next_token(t)+
      doublequote+"."
    ELSIF code = ExpectingInt THEN 
      "Expecting an integer. Found: "+doublequote+next_token(t)+doublequote+"."
    ELSIF code = ExpectingTestInt THEN 
      "Expecting integer that satisfies test. Found: "+
      doublequote+next_token(t)+doublequote+"."
    ELSIF code = ExpectingReal THEN 
      "Expecting a real. Found: "+doublequote+next_token(t)+doublequote+"."
    ELSIF code = ExpectingTestReal THEN 
      "Expecting real that satisfies test. Found: "+doublequote+next_token(t)+
      doublequote+"."
    ELSE
      emptystr
    ENDIF

  print_error(t:Tokenizer,m:Messenger): MACRO void = 
    IF error?(t) THEN  
      println("Syntax Error. "+"Line "+get_line(t)+": "+m(error(t))) &
      fail
    ELSE
      skip
    ENDIF

  print_error(t:Tokenizer): MACRO void = 
    print_error(t,std_mssg(t))

  ;*(m:Messenger,cs:[int,string]) : Messenger =
    LET (code,s) = cs IN m WITH [`code := s]
  
  tokenizer2str(t:Tokenizer):string = 
    tostr(t,0)+newline+std_mssg(t)(t`error)

  CONVERSION tokenizer2str

  tostr(t:Tokenizer): MACRO string = tokenizer2str(t)

END stdtokenizer

%% stdpvsio.pvs
%% PVSio interface

stdpvsio : THEORY
BEGIN

  help_pvs_attachment(s:string) : void 

  help_pvs_theory_attachments(s:string) : void 

  pvsio_version : string

  set_promptin(s:string) : void

  set_promptout(s:string) : void

END stdpvsio

%% stdsys.pvs
%% PVSio sytem library 

stdsys : THEORY
BEGIN
  
  Time : TYPE = [# 
    second : below(60),
    minute : below(60),
    hour   : below(24),
    day    : subrange(1,31),
    month  : subrange(1,12),
    year   : nat,
    dow    : below(7), % Day of week: 0 Monday
    dst    : bool,     % Dayligth saving time?
    tz     : {x:rat| -24 <= x AND x <= 24} % Time zone 
  #]

  tinybang : Time = (#
    day    := 1,
    dow    := 0,
    dst    := false,
    hour   := 0,
    minute := 0,
    month  := 1,
    second := 0,
    tz     := 0,
    year   := 0
  #)

  days_of_week(dow:below(7)):string =
    if    dow=0 then "Monday"
    elsif dow=1 then "Tuesday"
    elsif dow=2 then "Wednesday"
    elsif dow=3 then "Thursday" 
    elsif dow=4 then "Friday"
    elsif dow=5 then "Saturday"
    else  "Sunday"
    endif
 
  months(month:subrange(1,12)):string =
    if    month=1  then "January"
    elsif month=2  then "February"
    elsif month=3  then "March"
    elsif month=4  then "April"
    elsif month=5  then "May"
    elsif month=6  then "June"
    elsif month=7  then "July"
    elsif month=8  then "August"
    elsif month=9  then "September"
    elsif month=10 then "October"
    elsif month=11 then "November"
    else "December"
    endif

  tostr(t:Time): string =
    days_of_week(dow(t))+" "+months(month(t))+
    format(" ~2,'0d ",day(t))+year(t)+
    format(", ~2,'0d:~2,'0d:~2,'0d ",(hour(t),minute(t),second(t)))+
    format("(GMT~@d)",-tz(t))

  get_time : Time     % Get current time

  today : string =
    let t = get_time in
    format("~d/~2,'0d/~d",(month(t),day(t),year(t)))

  date : string =
    let t = get_time in
     tostr(get_time)

  sleep(n:nat): void  % Sleep n seconds 

  get_env(name,default:string):string % Get environment variable (default)

  get_env(name:string): MACRO string = get_env(name,emptystr)

  printf(s:string) : MACRO void =
    print(format(s,""))

  fprintf(f:OStream,s:string): MACRO void =
    fprint(f,format(s,""))

  Blisp : TYPE+  

  blisp(b:bool) : Blisp

  {||}(b:bool) : Blisp = blisp(b)

END stdsys