====== PVS 6.0 Prelude ====== % 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 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(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