% 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. % 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) 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 % 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 % 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?) 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_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)))) 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 nonempty_pred 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 % 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. 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, whihc 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) full?(a): bool = (FORALL x: member(x, a)) fullset: set = {x | true} 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} 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 choose(p: (nonempty?)): (p) = epsilon(p) the(p: (singleton?)): (p) = epsilon(p) 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 nonempty_exists: LEMMA nonempty?(a) IFF EXISTS (x: (a)): TRUE 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_emptyset: LEMMA subset?(emptyset, a) subset_fullset: LEMMA subset?(a, fullset) 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 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 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_disjoint: LEMMA disjoint?(a, difference(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_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)) nonempty_powerset: JUDGEMENT powerset(a) HAS_TYPE (nonempty?[set[T]]) END sets_lemmas % 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)) injective_inverse: LEMMA (FORALL (f:(injective?[D, R])): y = f(x) IMPLIES inverse(f)(y) = 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 % 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: VAR pred[[T1, T2]] X: VAR set[T1] Y: VAR set[T2] domain(R): TYPE = {x: T1 | EXISTS (y: T2): R(x, y)} range(R): TYPE = {y: T2 | EXISTS (x: T1): R(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 | FORALL (x: (X)): R(x, y)} postcondition(R)(X): set[T2] = postcondition(R, X) precondition(R, Y): set[T1] = {x: T1 | FORALL (y: (Y)): R(x, 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 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 minus_nzint_is_nzint: JUDGEMENT -(n0i) 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_id_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)) 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} = 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} 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 y = x/n0z IFF y * n0z = x 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) div_mult_pos_gt1: LEMMA x > z/py IFF x * py > z div_mult_pos_gt2: LEMMA z/py > x IFF z > x * py div_mult_neg_gt1: LEMMA x > z/ny IFF z > x * ny div_mult_neg_gt2: LEMMA z/ny > x IFF x * ny > z % 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 >= strict_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 END real_props % 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 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 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_1i: LEMMA 1^i = 1 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) 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 END divides % Modulo arithmetic defines rem and associated properties % Provided by Bruno Dutertre modulo_arithmetic : THEORY BEGIN x, y, z, t, q : 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) 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_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_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)) bij_exists : COROLLARY (EXISTS (f: [(S) -> below(card(S))]): bijective?(f)) % 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))) END finite_sets % 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 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 % 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_member: LEMMA every({c: T | member(c, l)})(l) 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 % 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 string_rep lemma shows how % strings are represented internally. The other 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 \ followed by a decimal number (< 256) or a \x or \X followed by a % hexidecimal number (< FF) represents that character number. 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] string_rep: LEMMA "foo" = list2finseq(cons(char(102), cons(char(111), cons(char(111), null)))) 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}) 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))}) 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 finite_sets_of_sets[T: TYPE]: THEORY BEGIN A, B: VAR finite_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) HAS_TYPE finite_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 IMPORTING EquivalenceClosure[X] 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