|
|
|
|
|
|
|
|
||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Issue: 5.9 Status: Definitive
DOCTYPE:Praxis title:varchar=title reference:varchar=reference status:varchar=status issue:varchar=issue date:varchar=date projectname:varchar=DocumentSet Issue 5.9, Definitive, 2nd February 2009
|
|
|
|
|
Originator |
|
|
|
|
SPARK Team |
|
|
|
|
Approver |
|
|
|
|
SPARK Team Line Manager |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
||
|
|
|
||
The contents of this manual are the subject of copyright and all rights in it are reserved. The manual may not be copied, in whole or in part, without the written consent of Praxis High Integrity Systems Limited.
Limited Warranty
Praxis High Integrity Systems Limited save as required by law makes no warranty or representation, either express or implied, with respect to this software, its quality, performance, merchantability or fitness for a purpose. As a result, the licence to use this software is sold ‘as is’ and you, the purchaser, are assuming the entire risk as to its quality and performance.
Praxis High Integrity Systems Limited accepts no liability for direct, indirect, special or consequential damages nor any other legal liability whatsoever and howsoever arising resulting from any defect in the software or its documentation, even if advised of the possibility of such damages. In particular Praxis High Integrity Systems Limited accepts no liability for any programs or data stored or processed using Praxis High Integrity Systems Limited products, including the costs of recovering such programs or data.
2 Guide To The Built-In Proof Rules
2.1 A Quick Overview Of The Rule Files
2.2 A Summary Of The Built-In Rules
3 Built-In Proof Rules Cross-References
3.1 Quick-Reference Index By Principal Functor
3.3 Full Expression-Pattern Index
5.4 Permissible Immediate Condition Predicates
5.5 Quantifiers In Proof Rules
6 Definition And Proof Of Proof Rules
6.4 Proofs Of Properties From Definitions
7 Using Buildchlib, The Rule-Library Builder
Document Control and References
SPADE is a registered trademark of Praxis High Integrity Systems Limited.
Note: The SPARK programming language is not sponsored by or affiliated with SPARC International Inc. and is not based on SPARC™ architecture.
Contents
This document provides technical information on the built-in proof rules of the SPADE Proof Checker and describes the process of creating user-defined proof rule files and proof rule libraries. This Rules Manual is a sister-document to the SPADE Proof Checker User Manual which describes use of the SPADE Proof Checker and its commands.
This document divides naturally into two separate parts: part one is concerned with the built-in proof rules supplied with the Checker, and comprises chapters 2 to 4, while part two, chapters 5 to 6 of this manual, describe how to create your own proof rules and libraries.
Chapter 2 is a guide to the main rule families of the built-in proof rules. Chapter 3 provides some indices into the built-in rule families, based on the structure of expression in which you are interested and/or rule family name. Chapter 4 is a complete listing of all the built-in proof rule files.
Chapter 5 describes the syntax of user-defined proof rule files so that you may write your own inference and substitution rules for use with the Checker. Chapter 6 considers the relationship between definitions of functions and their representation as proof rules, and considers how one may prove that properties of proof rules follow from a definition.
This manual is intended for both Windows and SUN users of the SPADE Proof Checker. Where file naming conventions are used, these are mostly in SUN (e.g. /home/user1/ion/myprog.vcg). Lowercase filenames are assumed throughout, though the built-in rule library uses uppercase names (INTINEQS.RUL).
2 Guide To The Built-In Proof Rules
2.1 A Quick Overview Of The Rule Files
The Checker’s built-in rule library of approximately 500 proof rules is organised as a collection of rule files. If the SPADE_CHECKER environment variable is set the Checker will look in this directory for the built-in rule library. If it is not set, it will look in <root>/lib/checker/rules. Each rule file has extension .RUL. Below is a list of the rule files included at present and a quick guide to their contents.
|
ARITH |
- |
manipulation of arithmetic expressions (by substitution) |
|
ARRAY |
- |
substitution rules for array-type expressions |
|
BITWISE |
- |
rules about the functions bit__and(_,_), bit__or(_,_) and bit__xor(_,_) |
|
ENUM |
- |
rules about enumerated types (pred, succ and ordering) |
|
ENUMERATION |
- |
additional useful inequalities for enumerated types |
|
FDLFUNCS |
- |
rules for built-in FDL functions abs(_), sqr(_), odd(_), X**Y |
|
GENINEQS |
- |
inequalities rules (for integers, reals and enumerated types) |
|
INTINEQS |
- |
inequalities rules relevant to integers only |
|
NUMINEQS |
- |
inequalities rules (for integers and reals) |
|
LOGIC |
- |
rules about the logical operators (and, or, not, ->, <->) |
|
MODULAR |
- |
rules about modular arithmetic (mod operator) |
|
QUANTIF |
- |
simple quantifier manipulation rules |
|
SEQ |
- |
rules about sequence types (length, append, first, last, etc.) |
|
SETS |
- |
rules about set types (in, not_in, \/, /\, \, subset_of) |
|
RECORD |
- |
special-invocation rules about record-type objects |
|
SPECIAL |
- |
special-invocation rules (simplify, standardisation, eq, etc.) |
It is useful to have a copy of these rulefiles handy for reference purposes when using the Checker. They are therefore included in full as chapter 4 of this manual.
In the next section, we shall consider the different “families” of rules in the built-in rule files, as an aid to familiarisation with the rule files.
2.2 A Summary Of The Built-In Rules
In this section, we consider the different rules by family. Each rule in the built-in rule files has a unique name which is composed of a family name and an instance number, e.g. arith(2) is the second rule of the arith family. When you use the infer/replace commands, giving the family-name of the rule you think will apply will lead to a faster search of the rulefiles than simply typing a wildcard rule name (though if the rule you need turns out not to be in the family you select, but in another, you will not succeed!). Obviously, the search will be faster still if you narrow down the search to a subrange of the rule family, or even to a specific rule. Thus, it is worthwhile to spend some time getting to know the different families of rules available.
2.2.1 Arithmetic rules (mainly in ARITH)
arith
Perform some elementary simplifications e.g.
X*1, 1*X-->X X+0, 0+X-->X
X*0,0*X --> 0 X-0 --> X
X div 1 --> X X/1 --> X
(X*N) div N --> X (N*X) div N --> X
(X/Y)*Y --> X (X/Y)*Y --> X
(X*Y)/Y --> Y (Y*X)/Y --> Y
assoc
Rules for the associativity of + and * (which may only be strictly applied, e.g. a+(b+c) may be rewritten to (a+b)+c, but these rules do not directly allow a+(b-c) to be rewritten to (a+b)-c: the “minus” rules (q.v.) are also needed in this latter case. This rule family also covers associativity of the logical operators and, or and <-> (in file LOGIC.RUL).
bitwise
(In BITWISE.RUL) Rules for the bitwise manipulation of modular types using the functions bit__and(_, _), bit__or(_, _) and bit__xor(_, _).
commut
Rules for the commutativity of + and *, so that A op B may be rewritten to B op A. This rule family also covers commutativity of the logical operators and, or and <-> (in file LOGIC.RUL).
distrib
Rules for the distributivity of * and div over + and -, and for distributivity of the logical operators and over or and or over and.
minus
A batch of rules for manipulating the unary and binary minus operators, e.g. so that A-B may be interchanged with A+(-B), -(-A) may be rewritten as A, etc.
modular
(In MODULAR.RUL) Rules defining the modular arithmetic operator, mod, and describing some of its properties.
intdiv
Substitution rules about the integer div operator. Rules include relationship between (A+B) div C and (A div C)+(B div C) when A (or B) is a multiple of C and arithmetic negation within div expressions.
2.2.2 FDL data-type rules (in ARRAY, ENUM, ENUMERATION, SEQ and SETS)
array
Substitution rules about the generic array-manipulation functions element(_,_) and update(_,_,_). These rules incorporate most of what you need to know about arrays, apart from for proofs of equality of two arrays in some circumstances. The simplification rules in this family can be performed automatically by the expression simplifier when the simplifier is enabled (with the simplify_during_load and/or simplify_in_infer flags set to on: see section 5.2.7 of the SPADE Proof Checker User Manual for further details of these flags).
mk__array
This is a single rule which allows the user to tell the Checker to simplify element accesses to SPARK array aggregate expressions formed with the mk__array functor. The expression to be simplified must be of the form element(ARR, [I]), and ARR must be an array aggregate expression, i.e. mk__array(...). The rationale behind the rule is described in comments preceding the body of the rule.
enum
These rules allow the manipulation of user-defined enumerated types, e.g. by allowing pred(succ(X)) and succ(pred(X)) to be replaced by X (where not at the relevant boundary) and by allowing various inferences about the inherited ordering of the enumerated constants.
enum_cases
This is a family of rules allowing you to infer
X=A1 or X=A2 or ... or X=An
for a variable X of enumerated type T, where
type T = (A1, A2, ..., An)
for some n in 2..25 inclusive. Rule enum_cases(N) is the rule for an enumeration containing N enumeration constants.
enumeration
This is a family of rules containing additional useful inequalities for enumerated types. It includes inequalties of the form A < B, A <= B, A > B, A >= B and also such forms involving pred and succ.
seqlen
These rules define the sequence function length(_), giving various substitutions for expressions involving it and some inequalities about it. (Refer also to section 3.2.6 of the Checker Manual).
append
These rules give properties of the FDL @ (append) operator, thus:
|
1-2 |
appending the empty sequence to either side of a list leaves the list unchanged. |
|
3 |
if A and B are actual lists [a1,...,an], [b1,...,bm], then A @ B is the list [a1,...,an,b1,...,bm]. |
|
4-5 |
a non-empty list S is equal to [first(S)] @ nonfirst(S), and to nonlast(S) @ [last(S)]. |
|
6 |
@ is associative, i.e. (X @ Y) @ Z = X @ (Y @ Z). |
first
These rules express properties of the FDL sequence function first(_), thus:
1 first([H,...]) is H
2 first([H,...] @ L) is H
3 first(X @ Y) is first(X) provided X <> [].
(N.B. to show first([] @ X) is first(X), use append(1-2) to rewrite [] @ X to X.)
last
These rules express properties of the FDL sequence function last(_), thus:
1 last([H]) is H.
2 last(X @ [H,...])islast([H,...]).
3 last([H|T]) islast(T) provided T <> [].
4 last(X @ Y) islast(Y) provided Y <> [].
nonfirst
These rules express properties of the FDL sequence function nonfirst(_), thus:
1 nonfirst([H|T]) is T.
2 nonfirst(T) is [] provided length(T)=1.
3 nonfirst(X @ Y) is nonfirst(X) @ Y provided X <> [].
4 nonfirst([H|T] @ Y) is T @ Y.
nonlast
These rules express properties of the FDL sequence function nonlast(_):
1 nonlast([H]) is [].
2 nonlast(T) is [] provided length(T)=1.
3 nonlast([H|T]) is [H|T1] provided nonlast(T)=T1.
4 nonlast(X @ Y) is X @ nonlast(Y) provided Y <> [].
5 nonlast(X @ [H]) is X.
seq
These rules express simple sequence equality properties: that two sequences are equal if and only if they are either both empty or they are both non-empty and have the same first and nonfirst (or last and nonlast) components.
sets
A family of rules for the FDL set operators. The main groupings are:
|
(1-3): |
simple X in A & X not_in A rules. |
|
(4-11): |
properties of set union (\/). |
|
(12-19): |
properties of set intersection (/\). |
|
(20-27): |
properties of set “lacking” (\). |
|
(28): |
X not_in (set []): nothing is in the empty set. |
|
(29-36): |
properties of the subset_of relation. |
|
(37): |
definition of strict_subset_of relation. |
|
(38-39): |
commutativity of \/ and /\. |
|
(40-41): |
associativity of \/ and /\. |
|
(42-43): |
distributivity of /\ over \/ and \/ over /\. |
2.2.3 Inequalities rules (mainly in GENINEQS, INTINEQS and NUMINEQS)
inequals
This is a large family of inference rules, covering addition/subtraction to one or both sides of an inequality, multiplication of both sides of an inequality, addition/subtraction of two inequalities and simple inequalities about the div operator. These rules, together with the Checker’s own inequalities inference capabilities, can cut down on much tedious manipulation, though some may still be necessary on occasion. This rule family is spread over three files: those in GENINEQS.RUL apply to any ordered type, those in NUMINEQS.RUL apply only to numeric types (i.e. integers and reals) and those in INTINEQS.RUL apply only to integers. The main groupings are:
|
1-6: |
subtraction from one side of inequality (e.g. i-N<j if...) |
|
7-18: |
addition to one side of inequality (e.g. i+N>j if...) |
|
19-22: |
addition of same no. both sides of < (e.g. i+N<j+N if...) |
|
23-26: |
addition of same no. both sides of > (e.g. i+N>N+j if...) |
|
27-30: |
addition of same no. both sides of <> (e.g. N+i<>N+j if...) |
|
31-33: |
subtract same no. both sides </>/<> (e.g. i-N>j-N if...) |
|
34-42: |
multiplication both sides by same no. (e.g. i*N<=j*N if...) |
|
43-48: |
addition > : A+C>B+D from (A...B or D), (C...D or B) |
|
49-54: |
addition < : A+C<B+D from (A...B or D), (C...D or B) |
|
55-60: |
addition <> : A+C<>B+D from (A...B or D), (C...D or B) |
|
61-64: |
addition of same no. both sides of = (e.g. i+N=N+j if...) |
|
65-68: |
addition of same no. both sides of <= (e.g. N+i<=j+N if...) |
|
69-72: |
addition of same no. both sides of >= (e.g. i+N>=j+N if...) |
|
73-75: |
subtract same no. both sides =/<=/>= (e.g. i-N>j-N if...) |
|
76: |
I*N=J*N may_be_deduced_from I=J. (* same no. each side =) |
|
77-79: |
addition >= : A+C>=B+D from (A...B or D), (C...D or B) |
|
80-82: |
addition <= : A+C>=B+D from (A...B or D), (C...D or B) |
|
83-85: |
addition = : A+C>=B+D from (A...B or D), (C...D or B) |
|
86-87: |
lower bounds for N*(A div N) for A>=0, N>0 |
|
88-89: |
upper bounds for N*(A div N) for A>=0 |
|
90-92: |
sign of A div N |
|
93-95: |
relations between I div N and J div N |
|
96-97: |
lower bounds for N*(A div N) for A>=0, N<0 |
|
98-100: |
sign of A div N |
|
101-103: |
strong to weak inequality for integers only |
|
104: |
infer X=Y from X*N=Y*N, given N<>0 |
|
105: |
infer X<>Y from X*N<>Y*N, given N<>0 |
|
106-107: |
infer X<=Y from X*N<=Y*N or X*N>=Y*N depending on sign of N |
|
108-109: |
infer X>=Y from X*N>=Y*N or X*N<=Y*N depending on sign of N |
|
110-111: |
infer X<Y from X*N<Y*N or X*N>Y*N depending on sign of N |
|
112-113: |
infer X>Y from X*N>Y*N or X*N<Y*N depending on sign of N |
|
114-121: |
rules about sign of X*Y (<=0, >=0, <0, >0) given signs of X, Y |
negation
These rules allow the interchanging of negated inequalities with their counterpart inequalities, e.g. (not a=b) and a<>b. All of these rules apply to any ordered type, hence their inclusion in GENINEQS.RUL.
strengthen
These rules allow a stronger inequality to be inferred from two weaker ones, e.g. a>=b and a<>b combine to give a>b. All of these rules apply to any ordered type, hence their inclusion in GENINEQS.RUL.
transitivity
These rules allow the combination of two inequalities to infer a third by transitivity, e.g. from a>b and b>c, we can infer a>c by transitivity, as > is a transitive operator, as are <, =, >= and <= (but not <> in quite the same way). All of these rules apply to any ordered type, hence their inclusion in GENINEQS.RUL.
To infer X <= Ytry transitivity (1-9)
To infer X >= Ytry transitivity (10-18)
To infer X < Ytry transitivity (19-23)
To infer X > Ytry transitivity (24-28)
To infer X = Ytry transitivity (29)
To infer X <> Ytry transitivity (30)
zero
This is a short family of rules about equality (or otherwise) to zero. The rules enable one to infer X*Y=0 if either X=0 or Y=0, to infer X=0 or Y=0 from X*Y=0, to infer X*Y<>0 if X<>0 and Y<>0 and to infer X<>0 from X*Y<>0 or from Y*X<>0.
2.2.4 Quantifier rules (in QUANTIF)
quant
A family of rules allowing standard quantifier manipulation of expressions, e.g. changing (not for_all(X,P(X))) into for_some(X,not P(X)), inferring for_some(X,P(X)) from for_some(X,P(X) and Q(X)), etc.
2.2.5 FDL function rules (in FDLFUNCS)
abs
A family of rules giving properties of the FDL abs(_) function.
sqr
Elementary properties of the sqr(X) (“square”, i.e. X*X) function.
odd
A collection of properties of the odd(_) function.
exp
Rules about the ** exponentiation operator added as an extension for SPARK Examiner output. Rules simplifying X**0, 0**X, 1**X, X**1, X**2, X**3, X**4, and defining (-X)**Y in terms of X**Y depending on whether Y is odd, plus recursive rules defining X**(Y+1) in terms of X**Y. The last six rules of this family allow the sign of X**Y to be inferred from knowledge of the sign of X and, as appropriate, whether or not Y is an odd power.
2.2.6 Logical operator rules (in LOGIC)
logical_not
These rules are elementary simplification rules for not, i.e. that (not true) is false, (not false) is true and (not not X) is X.
logical_and
These rules are elementary simplification rules for and, thus:
X and true à X true and X à X
X and false à false false and X à false
X and not X à false not X and X à false
X and X à X
logical_or
These rules are elementary simplification rules for or, thus:
X or false à X false or X à X
X or true à true true or X à true
X or not X à true not X or X à true
X or X à X
implies
These rules are elementary simplification rules for ->, thus:
X -> true à true X -> false à not X
true -> X à X false -> X à true
not X -> X à X X -> not X à not X
X -> X à true
equivalence
These rules are elementary simplification rules for <->, thus:
X <-> true à X true <-> X à X
X <-> false à not X false <-> X à not X
X <-> not X à false not X <-> X à false
X <-> X à true
logical
These rules provide other useful rules of classical logic, thus:
not (A or B) <-> (not A) and (not B)
not (A and B) <-> (not A) or (not B)
A -> B <-> (not A) or B
A <-> B <-> (A -> B) and (B -> A)
A -> (B -> C) <-> (A and B) -> C
2.2.7 Special rules (in SPECIAL and RECORD)
eq
This is the equality substitution rule: it allows you to replace A by B provided A=B (and A and B are different expressions). It is probably the most commonly-used substitution rule.
equiv
This is the equivalence substitution rule: you can use it to replace A by B (or vice versa) provided A <-> B. It is a special-invocation rule, i.e. you can only apply it if you specifically ask for it: it will not be applied by a wild-card rulename, for instance.
inference
This is a batch of simple rules for inferring compound logical expressions. For example, given a conclusion of the form A or B, this family of rules lets you prove A only, either directly or as a subgoal. This family of rules can be useful if, for instance, one has a logical expression as a goal, each of whose components are quantified formulae: using this family, the goal may be split into one or more subgoals so that the unwrap command can be used.
logic
These two rules must be invoked with the rulename logic if they are to be used, as without this trigger they will be ignored. They call the truth-table inference mechanism (used by the deduce command). One will allow you to infer X if X can be deduced in this way (from no hypotheses, i.e. if it is a truth-table tautology), while the other rule allows you to substitute Y for X if it can deduce that X <-> Y is logically true.
mk__record
These two special-invocation rules give the user access to record aggregate simplification facilities. The first rule allows a paricular field to be selected from within a SPARK record aggregate expression; it can be used to rewrite expressions of the form fld_F(mk__record(...)) to the value associated with the field F in the aggregate expression. The second rule allows the user to simplify updates to aggregate expressions: given an expression of the form upf_F(mk__record(...), V), we can rewrite to a new aggregate expression mk__record(...) in which field F is associated with the value of expression V.
record
This family of five rules must be invoked with the rulename record if they are to be used, as without this trigger they will be ignored. They allow the user to employ the built-in record simplification rules directly to substitute one equivalent expression for another. Thus, with this rule, the implicit workings of the Checker in manipulating record-type objects can be made explicit where desired. The rules are:
|
record(1): |
fld_F(upf_F(_, VALUE) may_be_replaced_by VALUE. |
|
record(2): |
upf_F(REC, fld_F(REC)) may_be_replaced_by REC. |
|
record(3): |
upf_F(upf_G(R, VG), VF) may_be_replaced_by upf_G(upf_F(R, VF), VG) if [ “F” <> “G” ]. |
|
record(4): |
fld_F(upf_G(R, V)) may_be_replaced_by fld_F(R) if [ “F” <> “G” ]. |
|
record(5): |
upf_F(upf_F(R, _), V) may_be_replaced_by upf_F(R, V). |
record_equality
A special-invocation family of rules which allow one to infer that two records are equal if all of their fields are equal, i.e. we can infer that R=S provided we can prove each of fld_field1(R)=fld_field1(S), ... , fld_fieldN(R)=fld_fieldN(S) in turn.
Rules record_equality(1-10) are for records with 1 to 10 fields respectively; rule record_equality(11) deals with records of 11 or more fields in a more general way.
simplify
These two rules must be invoked with the rulename simplify if they are to be used, as without this trigger they will be ignored. They call the Checker’s built-in expression simplifier directly. Both rules are substitution rules. If you provide a determinate expression Y which you wish to substitute for X, this rule will permit the substitution provided both X and Y simplify to the same expression; otherwise, if Y is uninstantiated, the rule will attempt to find the required Y by simplifying X.
standardisation
These three rules must be invoked with the rulename standardisation if they are to be used, as without this trigger they will be ignored. They call the standardiser directly. One rule allows you to infer X if X standardises to true. The other two rules allow substitution. If you provide a determinate expression Y which you wish to substitute for X, this rule will permit the substitution provided both X and Y have the same standard form; otherwise, if Y is not fully instantiated, the rule will attempt to find the required Y by standardising X.
unification
A special-invocation family of rules which, for any function (or operator) F, allows you to infer F(X1,...,Xn)=F(Y1,...,Yn) from X1=Y1, ..., Xn=Yn (for n in 1..9 at present).
In fact, you can get along without these rules (useful to know if F is a function with 10 or more arguments): if you want to prove F(X1,...,Xn)=F(Y1,...,Yn) and you can prove X1=Y1, ..., Xn=Yn, then just replace each Yi by Xi in F(X1,...,Xn)=F(Y1,...,Yn) to get the required result; if necessary, you can use proof by contradiction to explicitly introduce the F(Y1,...,Yn) expression first.
3 Built-In Proof Rules Cross-References
In this chapter, we provide three indices into the built-in proof rule files which were outlined in the previous chapter (and which are listed in full in the following chapter). The first index in section 3.1 shows, for each principal functor (i.e. main operator or function — the “root” of the expression tree in which you are interested), which rule families may be applicable. The second index in section 3.2 is alphabetically ordered by rule family name and shows, for each rule family, those principal functors for which the family may be of interest and in which rule files the rules are located. The third index, in section 3.3, is a more comprehensive version of the index in section 3.1: in 3.3, we show not only the principal functor, but also all instances of expression pattern and the rules which are applicable. Thus, taking rules inequals(18) and inequals(42) as an example, the index in 3.1 records that rule family inequals in NUMINEQS.RUL can be applied to expressions of the form _ <= _ while that in 3.3 records that the inequals rules in NUMINEQS.RUL can be applied to expressions of the form _ <= (_ + _) and of the form (_ * _) <= (_ * _) and other <= patterns (where _ is a place-marker for a general expression). In this sense, 31 is a “quick-reference” index, while 33 is a more substantial breakdown of relevant expression patterns.
As well as the convention that _ stands for an expression in this index, another convention used in section 3.2 is that an equality enclosed within braces thus — {_ = _} — means that this rule family can only be used for inferring equalities when the use_subst_rules_for_equality flag is set to on; in these circumstances, the equalities which can be inferred will be of the form of subexpressions recorded for that rule family and rule file in section 3.2; we give no further breakdown of these possible equality combinations in section 3.3. Finally, all ordering was via ASCII sort, though the rule families which apply to general expressions (_) are recorded at the end for the indices in sections 3.1 and 3.3.
The ordering used for the operators in these indices is:
|
* |
multiplication |
|
** |
exponentiation |
|
+ |
addition |
|
- |
minus (unary, then binary) |
|
-> |
implication |
|
/ |
real division |
|
/\ |
set intersection |
|
< |
strictly less-than |
|
<-> |
logical equivalence |
|
<= |
less-than or equal-to |
|
<> |
non-equality |
|
= |
equality |
|
> |
strictly greater-than |
|
>= |
greater-than or equal-to |
|
@ |
sequence append |
|
[_|_] |
list notation |
|
\ |
set lacking |
|
\/ |
set union |
3.1 Quick-Reference Index By Principal Functor
|
Expression |
Rule Families |
|||
|
_ * _ |
Abs distrib |
Arith Exp |
Assoc Minus |
commut sqr |
|
_ ** _ |
exp |
|
|
|
|
_ + _
|
arith intdiv |
assoc minus |
commut seqlen |
distrib |
|
- _ |
intdiv |
Minus |
|
|
|
_ - _ |
arith |
distrib |
minus |
seqlen |
|
_ > _ |
implies |
Inference |
logical |
|
|
_ / _ |
arith |
|
|
|
|
_ /\ _ |
sets |
|
|
|
|
_ < _ |
bitwise inequals transitivity |
Enum Modular |
enumeration negation |
exp strengthen |
|
_ <> _
|
assoc equivalence modular transitivity |
commut Inequals Negation Zero |
enum inference odd |
enumeration logical seq |
|
_ <= _
|
bitwise inequals |
Enum Modular |
enumeration negation |
exp transitivity |
|
_ = _
|
enum seq unification arith distrib implies logical_and nonfirst seqlen |
inequals strengthen zero array equivalence intdiv logical_not nonlast sets |
negation transitivity abs assoc exp last logical_or quant sqr |
odd record_equality append commut first logical minus record modular |
_ > _
|
abs inequals strengthen |
Enum negation transitivity |
enumeration seqlen |
exp sqr |
|
_ >= _ |
abs inequals transitivity |
enum negation |
enumeration seqlen |
exp sqr |
|
_ @ _ |
append |
nonfirst |
nonlast |
|
|
[_|_] |
nonlast |
|
|
|
|
_ \ _ |
sets |
|
|
|
|
_ \/ _ |
sets |
|
|
|
|
abs(_) |
abs |
sqr |
|
|
|
_ and _ |
assoc logical |
commut logical_and |
distrib |
inference |
Expression |
Rule Families |
|
|
|
|
bit__and(_,_) |
bitwise |
|
|
|
|
bit__or(_,_) |
bitwise |
|
|
|
|
bit__xor(_,) |
bitwise |
|
|
|
|
_ div _ |
arith |
intdiv |
|
|
|
Element(_,_) |
array |
mk__array |
|
|
|
first(_) |
first |
|
|
|
|
fld_X(_) |
record |
mk__record |
|
|
|
for_all(_,_) |
quant |
|
|
|
|
for_some(_,_) |
quant |
|
|
|
|
_ in _ |
sets |
|
|
|
|
last(_) |
last |
|
|
|
|
length(_) |
seqlen |
|
|
|
|
_ mod _ |
modular |
|
|
|
|
nonfirst(_) |
nonfirst |
|
|
|
|
Nonlast(_) |
nonlast |
|
|
|
|
not _
|
logical quant |
logical_not sets |
negation |
odd |
|
_ not_in _ |
sets |
|
|
|
|
odd(_) |
odd |
|
|
|
|
_ or _
|
abs enum logical_or |
assoc enum_cases quant |
commut inference sets |
distrib logical zero |
|
pred(_) |
enum |
enumeration |
|
|
|
sqr(_) |
sqr |
|
|
|
|
_ strict_subset_of _ |
sets |
|
|
|
|
_ subset_of _ |
sets |
|
|
|
|
succ(_) |
enum |
enumeration |
|
|
|
update(_,_,_) |
array |
|
|
|
|
upf_X(_,_) |
record |
mk__record |
|
|
|
_
|
eq simplify |
equiv standardisation |
inference |
logic |
|
Rule Family |
Rule File |
Patterns |
||
|
abs
|
FDLFUNCS
|
_ * _ abs(_) |
_ > _ _ or _ |
_ >= _ {_ = _} |
|
append |
SEQ |
_ = _ |
_ @ _ |
|
|
arith
|
ARITH
|
_ * _ _ / _ |
_ + _ _ div _ |
_ - _ {_ = _} |
|
array |
ARRAY |
element(_,_) |
update(_,_,_) |
{_ = _} |
|
assoc |
ARITH |
_ * _ |
_ + _ |
{_ = _} |
|
assoc
|
LOGIC
|
_ <-> _ _ = _ |
_ and _ |
_ or _ |
|
bitwise
|
BITWISE
|
_ < _ bit__and(_,_) |
_ <= _ bit__or(_,_) |
_ = _ bit__xor(_,_) |
|
commut |
ARITH |
_ * _ |
_ + _ |
{_ = _} |
|
commut |
LOGIC |
_ <-> _ {_ = _} |
_ and _ |
_ or _ |
|
distrib |
ARITH |
_ * _ {_ = _} |
_ + _ |
_ - _ |
|
distrib |
LOGIC |
_ and _ |
_ or _ |
{_ = _} |
|
enum |
ENUM
|
_ < _ _ = _ _ or _ |
_ <= _ _ > _ pred(_) |
_ <> _ _ >= _ succ(_) |
|
enum_cases |
ENUM |
_ or _ |
|
|
|
enumeration |
ENUMERATION |
_ <= _ _ > _ pred(_) |
_ < _ _ <> _ |
_ >= _ succ(_) |
|
eq |
SPECIAL |
_ |
|
|
|
equiv |
SPECIAL |
_ |
|
|
|
equivalence |
LOGIC |
_ <-> _ |
{_ = _} |
|
|
exp |
FDLFUNCS |
_ * _ _ <= _ {_ = _} |
_ ** _ _ > _ |
_ < _ _ >= _ |
|
first |
SEQ |
first(_) |
{_ = _} |
|
|
implies |
LOGIC |
_ -> _ |
{_ = _} |
|
|
inequals |
INTINEQS |
_ <= _ _ >= _ |
_ = _ |
_ > _ |
|
inequals |
NUMINEQS
|
_ < _ _ = _ |
_ <= _ _ > _ |
_ <> _ _ >= _ |
|
inference |
SPECIAL |
_ -> _ _ or _ |
_ <-> _ _ |
_ and _ |
|
intdiv |
ARITH
|
_ + _ {_ = _} |
- _ |
_ div _ |
|
last |
SEQ |
last(_) |
{_ = _} |
|
|
logic |
SPECIAL |
_ |
|
|
|
logical
|
LOGIC |
_ -> _ not _ |
_ <-> _ _ or _ |
_ and _ {_ = _} |
|
logical_and |
LOGIC |
_ and _ |
{_ = _} |
|
|
logical_not |
LOGIC |
not _ |
{_ = _} |
|
|
logical_or |
LOGIC |
_ or _ |
{_ = _} |
|
|
minus |
ARITH |
_ * _ _ - _ |
_ + _ {_ = _} |
- _ |
|
modular |
MODULAR |
_ < _ _ =_ |
_ <=_ _ mod _ |
_ <>_ |
|
mk__array |
ARRAY |
element(_, _) |
|
|
|
mk__record |
RECORD |
fld_X(_) |
upf_X(_, _) |
|
|
negation |
GENINEQS |
_ < _ _ = _ not _ |
_ <= _ _ > _ |
_ <> _ _ >= _ |
|
nonfirst |
SEQ |
_ @ _ |
nonfirst(_) |
{_ = _} |
|
nonlast |
SEQ |
_ @ _ {_ = _} |
[_|_] |
nonlast(_) |
|
odd |
FDLFUNCS
|
_ <> _ odd(_) |
_ = _ |
not _ |
|
quant |
QUANTIF
|
for_all(_,_) _ or _ |
for_some(_,_) {_ = _} |
not _ |
|
record |
RECORD |
fld_X(_) |
upf_X(_,_) |
{_ = _} |
|
record_equality |
RECORD |
_ = _ |
|
|
|
seq |
SEQ |
_ <-> _ |
_ = _ |
|
|
seqlen |
SEQ |
_ + _ _ >= _ |
_ - _ length(_) |
_ > _ {_ = _} |
|
sets |
SETS |
_ /\ _ _ in _ _ or _ {_ = _} |
_ \ _ not _ _ subset_of _ _ strict_subset_of _ |
_ \/ _ _ not_in _ |
|
simplify |
SPECIAL |
_ |
|
|
|
sqr |
FDLFUNCS |
_ * _ abs(_) |
_ > _ sqr(_) |
_ >= _ {_ = _} |
|
standardisation |
SPECIAL |
_ |
|
|
|
strengthen |
GENINEQS |
_ < _ |
_ = _ |
_ > _ |
|
transitivity |
GENINEQS
|
_ < _ _ = _ |
_ <= _ _ > _ |
_ <> _ _ >= _ |
|
unification |
SPECIAL |
_ = _ |
|
|
|
zero |
NUMINEQS |
_ <> _ |
_ = _ |
_ or _ |
3.3 Full Expression-Pattern Index
|
Expression |
Rule Families |
||
|
(_ * _) * _ |
assoc |
|
|
|
(_ + _) * _ |
distrib |
|
|
|
(- _) * (- _) |
minus |
|
|
|
(- _) * _ |
minus |
|
|
|
(_ - _) * _ |
distrib |
|
|
|
(_ / _) * _ |
arith |
|
|
|
0 * _ |
arith |
|
|
|
1 * _ |
arith |
|
|
|
_ * (_ * _) |
assoc |
|
|
|
_ * (_ ** (_ - 1)) |
exp |
|
|
|
_ * (_ ** _) |
exp |
|
|
|
_ * (_ + _) |
distrib |
|
|
|
_ * (- _) |
minus |
|
|
|
_ * (_ - _) |
distrib |
|
|
|
_ * (_ / _) |
arith |
|
|
|
_ * 0 |
arith |
|
|
|
_ * 1 |
arith |
|
|
|
_ * _ |
commut |
minus |
|
|
abs(_) * abs(_) |
abs |
|
|
|
sqr(_) * sqr(_) |
sqr |
|
|
|
(- _) ** _ |
exp |
|
|
|
0 ** _ |
exp |
|
|
|
1 ** _ |
exp |
|
|
|
_ ** (_ + 1) |
exp |
|
|
|
_ ** 0 |
exp |
|
|
|
_ ** 1 |
exp |
|
|
|
_ ** 2 |
exp |
|
|
|
_ ** 3 |
exp |
|
|
|
_ ** 4 |
exp |
|
|
|
_ ** _ |
exp |
|
|
|
(_ * _) + (_ * _) |
distrib |
|
|
|
(_ + _) + _ |
assoc |
|
|
|
(- _) + (- _) |
minus |
|
|
|
0 + _ |
arith |
|
|
|
_ + (_ + _) |
assoc |
|
|
|
_ + (- _) |
minus |
|
|
|
_ + 0 |
arith |
|
|
|
_ + _ |
commut |
|
|
|
_ + (_ div _) |
intdiv |
|
|
|
(_ div _) + _ |
intdiv |
|
|
|
(_ div _) + (_ div _) |
intdiv |
|
|
|
length(_) + length(_) |
seqlen |
|
|
|
length(nonfirst(_)) + 1 |
seqlen |
|
|
|
length(nonlast(_)) + 1 |
seqlen |
|
|
|
-(_ * _) |
minus |
|
|
|
-(_ + _) |
minus |
|
|
|
-(- _) |
minus |
|
|
|
-(_ - _) |
minus |
|
|
|
-(_ div _) |
intdiv |
|
|
|
- 0 |
minus |
|
|
|
(_ * _) - (_ * _) |
distrib |
|
|
|
(- _) - _ |
minus |
|
|
|
_ - 0 |
arith |
|
|
|
_ - _ |
minus |
|
|
|
length(_) - 1 |
seqlen |
|
|
|
_ -> (_ -> _) |
logical |
|
|
|
_ -> _ |
implies |
inference |
logical |
|
_ -> false |
implies |
|
|
|
_ -> (not _) |
implies |
|
|
|
_ -> true |
implies |
|
|
|
false -> _ |
implies |
|
|
|
(not _) -> _ |
implies |
|
|
|
true -> _ |
implies |
|
|
|
(_ * _) / _ |
arith |
|
|
|
_ / 1 |
arith |
|
|
|
(_ /\ _) /\ _ |
sets |
|
|
|
(_ \/ _) /\ (_ \/ _) |
sets |
|
|
|
_ /\ (_ /\ _) |
sets |
|
|
|
_ /\ (_ \/ _) |
sets |
|
|
|
_ /\ _ |
sets |
|
|
|
_ /\ set [] |
sets |
|
|
|
(set []) /\ _ |
sets |
|
|
|
(set _) /\ (set _) |
sets |
|
|
|
(_ * _) < (_ * _) |
inequals |
|
|
|
(_ * _) < 0 |
inequals |
|
|
|
(_ ** _) < 0 |
exp |
|
|
|
(_ + _) < (_ + _) |
inequals |
|
|
|
(_ - _) < (_ - _) |
inequals |
|
|
|
(_ - _) < _ |
inequals |
|
|
|
_ < (_ + _) |
inequals |
|
|
|
_ < _ |
enum strengthen |
inequals transitivity |
negation enumeration |
|
_ < _ mod _ |
modular |
|
|
|
_ mod _ < _ |
modular |
|
|
|
(_ <-> _) <-> _ |
assoc |
|
|
|
(_ = _) <-> (... or ...) |
seq |
|
|
|
_ <-> (_ <-> _) |
assoc |
|
|
|
_ <-> _ |
commut logical |
equivalence |
inference |
|
_ <-> false |
equivalence |
|
|
|
_ <-> (not _) |
equivalence |
|
|
|
_ <-> true |
equivalence |
|
|
|
false <-> _ |
equivalence |
|
|
|
(not _) <-> _ |
equivalence |
|
|
|
true <-> _ |
equivalence |
|
|
|
(_ * _) <= (_ * _) |
inequals |
|
|
|
(_ * _) <= 0 |
inequals |
|
|
|
(_ * (_ div _)) <= _ |
inequals |
|
|
|
((_ div _) * _) <= _ |
inequals |
|
|
|
(_ ** _) <= 0 |
exp |
|
|
|
(_ + 1) <= _ |
inequals |
|
|
|
(_ + _) <= (_ + _) |
inequals |
|
|
|
(_ - _) <= (_ - _) |
inequals |
|
|
|
(_ - _) <= _ |
inequals |
|
|
|
_ <= (_ + _) |
inequals |
|
|
|
_ <= _ |
enum transitivity |
inequals enumeration |
negation |
|
_ mod _ <= _ |
modular |
|
|
|
_ <= _ mod _ |
modular |
|
|
|
(_ div _) <= 0 |
inequals |
|
|
|
(_ + _) <> (_ + _) |
inequals |
|
|
|
(_ - _) <> (_ - _) |
inequals |
|
|
|
_ <> 0 |
zero |
|
|
|
_ <> _ |
enum |
inequals |
negation |
|
|
transitivity |
enumeration |
|
|
(_ * _) = (_ * _) |
inequals |
|
|
|
(_ * _) = 0 |
zero |
|
|
|
((_ div 2) * 2) = _ |
odd |
|
|
|
(_ + _) = (_ + _) |
inequals |
|
|
|
(_ - _) = (_ - _) |
inequals |
|
|
|
_ = _ |
abs |
enum |
inequals |
|
negation |
record_equality |
seq |
|
|
strengthen |
transitivity |
unification |
|
|
_ = pred(succ(_)) |
enum |
|
|
|
_ = succ(pred(_)) |
enum |
|
|
|
(_ div _) = (_ div _) |
inequals |
|
|
|
(_ mod _) = _ |
modular |
|
|
|
((_ mod _) mod _) = (_ mod _) |
modular |
|
|
|
_ mod _ = -(- _ mod - _) |
modular |
|
|
|
pred(succ(_)) = _ |
enum |
|
|
|
succ(pred(_)) = _ |
enum |
|
|
|
{_ = _} |
append |
arith |
array |
|
assoc |
commut |
distrib |
|
|
equivalence |
first |
implies |
|
|
intdiv |
last |
logical |
|
|
logical_and |
logical_not |
logical_or |
|
|
minus |
nonfirst |
nonlast |
|
|
quant |
record |
seqlen |
|
|
sets |
sqr |
|
|
|
(_ * _) > (_ * _) |
inequals |
|
|
|
(_ * _) > 0 |
inequals |
|
|
|
(_ ** _) > 0 |
exp |
|
|
|
(_ + _) > (_ + _) |
inequals |
|
|
|
(_ + _) > _ |
inequals |
|
|
|
(_ div _) <= (_ div _) |
inequals |
|
|
|
(_ * _) <> (_ * _) |
inequals |
|
|
|
(_ * _) <> 0 |
zero |
|
|
|
((_ div 2) * 2) <> _ |
odd |
|
|
|
(_ - _) > (_ - _) |
inequals |
|
|
|
_ > (_ - _) |
inequals |
|
|
|
_ > _ |
enum |
inequals |
negation |
|
strengthen |
transitivity |
enumeration |
|
|
abs(_) > 0 |
abs |
|
|
|
(_ div _) > 0 |
inequals |
|
|
|
length([_|_]) > 0 |
seqlen |
|
|
|
sqr(_) > 0 |
sqr |
|
|
|
(_ * _) >= (_ * _) |
inequals |
|
|
|
(_ * _) >= 0 |
inequals |
|
|
|
_ * _ div _ >= _ + _ + 1 |
inequals |
|
|
|
_ * _ div _ >= _ - _ + 1 |
inequals |
|
|
|
_ div _ * _ >= _ + _ + 1 |
inequals |
|
|
|
_ div _ * _ >= _ - _ + 1 |
inequals |
|
|
|
(_ ** _) >= 0 |
exp |
|
|
|
(_ + _) >= (_ + _) |
inequals |
|
|
|
(_ + _) >= _ |
inequals |
|
|
|
(_ - _) >= (_ - _) |
inequals |
|
|
|
_ >= (_ + 1) |
inequals |
|
|
|
_ >= (_ - _) |
inequals |
|
|
|
_ >= 1 |
inequals |
|
|
|
_ >= _ |
enum transitivity |
inequals enumeration |
negation |
|
abs(_) >= 0 |
abs |
|
|
|
(_ div _) >= 0 |
inequals |
|
|
|
(_ div _) >= (_ div _) |
inequals |
|
|
|
length([_|_]) >= 1 |
seqlen |
|
|
|
length(_) >= 0 |
seqlen |
|
|
|
sqr(_) >= 0 |
sqr |
|
|
|
(_ @ _) @ _ |
append |
|
|
|
[] @ _ |
append |
|
|
|
[_|_] @ [_|_] |
append |
|
|
|
[first(_)] @ nonfirst(_) |
append |
|
|
|
_ @ (_ @ _) |
append |
|
|
|
_ @ [] |
append |
|
|
|
_ @ nonlast(_) |
nonlast |
|
|
|
nonfirst(_) @ _ |
nonfirst |
|
|
|
nonlast(_) @ [last(_)] |
append |
|
|
|
[_|_] |
nonlast |
|
|
|
_ \ _ |
sets |
|
|
|
(set _) \ (set _) |
sets |
|
|
|
(_ /\ _) \/ (_ /\ _) |
sets |
|
|
|
(_ \/ _) \/ _ |
sets |
|
|
|
_ \/ (_ /\ _) |
sets |
|
|
|
_ \/ (_ \/ _) |
sets |
|
|
|
_ \/ (set []) |
sets |
|
|
|
(set []) \/ _ |
sets |
|
|
|
(set _) \/ (set _) |
sets |
|
|
|
abs(_ * _) |
abs |
|
|
|
abs(_) |
abs |
|
|
|
abs(abs(_)) |
abs |
|
|
|
abs(sqr(_)) |
sqr |
|
|
|
(_ -> _) and (_ -> _) |
logical |
|
|
|
_ and _ |
commut |
inference |
logical_and |
|
_ and (_ and _) |
assoc |
|
|
|
_ and false |
logical_and |
|
|
|
_ and (not _) |
logical_and |
|
|
|
_ and (_ or _) |
distrib |
|
|
|
_ and true |
logical_and |
|
|
|
(_ and _) and _ |
assoc |
|
|
|
false and _ |
logical_and |
|
|
|
(not _) and _ |
logical_and |
|
|
|
(not _) and (not _) |
logical |
|
|
|
(_ or _) and _ |
distrib |
|
|
|
(_ or _) and (_ or _) |
distrib |
|
|
|
true and _ |
logical_and |
|
|
|
(_ * _) div (_ * _) |
intdiv |
|
|
|
(_ * _) div _ |
arith |
intdiv |
|
|
(_ + _) div _ |
intdiv |
|
|
|
(- _) div (- _) |
intdiv |
|
|
|
(- _) div _ |
intdiv |
|
|
|
_ div (- _) |
intdiv |
|
|
|
_ div 1 |
arith |
|
|
|
_ div _ |
intdiv |
|
|
|
element(_,_) |
array |
|
|
|
element(mk__array(_),_) |
mk__array |
|
|
|
element(update(_,_,_),_) |
array |
|
|
|
first([_|_] @ _) |
first |
|
|
|
first(_ @ _) |
first |
|
|
|
first([_|_]) |
first |
|
|
|
first(_) |
first |
|
|
|
fld_X(mk__record(_..._)) |
mk__record |
|
|
|
fld_X(upf_X(_,_)) |
record |
|
|
|
fld_X(upf_Y(_,_)) |
record |
|
|
|
for_all(_,_ -> _) |
quant |
|
|
|
for_all(_,_ <-> _) |
quant |
|
|
|
for_all(_,_) |
quant |
|
|
|
for_all(_,_ and _) |
quant |
|
|
|
for_all(_,for_all(_,_)) |
quant |
|
|
|
for_all(_,(not _)) |
quant |
|
|
|
for_all(_,_ or _) |
quant |
|
|
|
for_some(_,_ -> _) |
quant |
|
|
|
for_some(_,_) |
quant |
|
|
|
for_some(_,for_all(_,_)) |
quant |
|
|
|
for_some(_,for_some(_,_)) |
quant |
|
|
|
for_some(_,(not _)) |
quant |
|
|
|
for_some(_,_ or _) |
quant |
|
|
|
_ in (_ /\ _) |
sets |
|
|
|
_ in (_ \ _) |
sets |
|
|
|
_ in (_ \/ _) |
sets |
|
|
|
_ in _ |
sets |
|
|
|
_ in (set _) |
sets |
|
|
|
last(_ @ [_|_]) |
last |
|
|
|
last(_ @ _) |
last |
|
|
|
last([_]) |
last |
|
|
|
last([_|_]) |
last |
|
|
|
last(_) |
last |
|
|
|
length(_ @ _) |
seqlen |
|
|
|
length([]) |
seqlen |
|
|
|
length([_|_]) |
seqlen |
|
|
|
length(_) |
seqlen |
|
|
|
length(nonfirst(_)) |
seqlen |
|
|
|
length(nonlast(_)) |
seqlen |
|
|
|
_ mod _ |
modular |
|
|
|
(_ * _) mod _ |
modular |
|
|
|
(_ mod _) mod _ |
modular |
|
|
|
nonfirst([_|_] @ _) |
nonfirst |
|
|
|
nonfirst(_ @ _) |
nonfirst |
|
|
|
nonfirst([_|_]) |
nonfirst |
|
|
|
nonfirst(_) |
nonfirst |
|
|
|
nonlast(_ @ [_]) |
nonlast |
|
|
|
nonlast(_ @ _) |
nonlast |
|
|
|
nonlast([_]) |
nonlast |
|
|
|
nonlast([_|_]) |
nonlast |
|
|
|
nonlast(_) |
nonlast |
|
|
|
not (_ < _) |
negation |
|
|
|
not (_ <= _) |
negation |
|
|
|
not (_ <> _) |
negation |
|
|
|
not (_ = _) |
negation |
|
|
|
not (_ > _) |
negation |
|
|
|
not (_ >= _) |
negation |
|
|
|
not (_ and _) |
logical |
|
|
|
not false |
logical_not |
|
|
|
not for_all(_,_) |
quant |
|
|
|
not for_all(_,(not _)) |
quant |
|
|
|
not for_some(_,_) |
quant |
|
|
|
not for_some(_,(not _)) |
quant |
|
|
|
not (_ in _) |
sets |
|
|
|
not (not _) |
logical_not |
|
|
|
not (_ not_in _) |
sets |
|
|
|
not odd(_ * _) |
odd |
|
|
|
not odd(_ + _) |
odd |
|
|
|
not odd(- _) |
odd |
|
|
|
not odd(_ - _) |
odd |
|
|
|
not odd(_) |
odd |
|
|
|
not odd(abs(_)) |
odd |
|
|
|
not odd(sqr(_)) |
odd |
|
|
|
not (_ or _) |
logical |
|
|
|
not true |
logical_not |
|
|
|
_ not_in (_ /\ _) |
sets |
|
|
|
_ not_in (_ \ _) |
sets |
|
|
|
_ not_in (_ \/ _) |
sets |
|
|
|
_ not_in _ |
sets |
|
|
|
_ not_in (set []) |
sets |
|
|
|
odd(_ * _) |
odd |
|
|
|
odd(_ + _) |
odd |
|
|
|
odd(- _) |
odd |
|
|
|
odd(_ - _) |
odd |
|
|
|
odd(_) |
odd |
|
|
|
odd(abs(_)) |
odd |
|
|
|
odd(sqr(_)) |
odd |
|
|
|
(_ = 0) or (_ = 0) |
zero |
|
|
|
(_ = _) or (_ = _) |
enum_cases |
|
|
|
(_ = _) or (_ >= _) |
enum |
|
|
|
(_ = _) or _ |
enum |
|
|
|
(_ = _) or _ |
enum_cases |
|
|
|
(_ = _) or (_ in _) |
sets |
|
|
|
abs(_)=_ or abs(_)=(- _) |
abs |
|
|
|
_ or _ |
commut |
inference |
logical_or |
|
_ or (_ and _) |
distrib |
|
|
|
_ or false |
logical_or |
|
|
|
_ or (not _) |
logical_or |
|
|
|
_ or (_ or _) |
assoc |
|
|
|
_ or true |
logical_or |
|
|
|
(_ and _) or _ |
distrib |
|
|
|
(_ and _) or (_ and _) |
distrib |
|
|
|
false or _ |
logical_or |
|
|
|
for_some(_,_) or ... |
quant |
|
|
|
(not _) or _ |
logical |
logical_or |
|
|
(not _) or (not _) |
logical |
|
|
|
(_ or _) or _ |
assoc |
|
|
|
true or _ |
logical_or |
|
|
|
pred(_) |
enum |
enumeration |
|
|
sqr(_ * _) |
sqr |
|
|
|
sqr(_) |
sqr |
|
|
|
sqr(abs(_)) |
sqr |
|
|
|
_ strict_subset_of _ |
sets |
|
|
|
(_ /\ _) subset_of _ |
sets |
|
|
|
(_ \ _) subset_of _ |
sets |
|
|
|
_ subset_of (_ \/ _) |
sets |
|
|
|
_ subset_of _ |
sets |
|
|
|
(set []) subset_of _ |
sets |
|
|
|
(set _) subset_of (set _) |
sets |
|
|
|
succ(_) |
enum |
enumeration |
|
|
update(_,_,element (_,_)) |
array |
|
|
|
update(update(_,_,_),_,_) |
array |
|
|
|
upf_X(_,fld_X(_)) |
record |
|
|
|
upf_X(mk__record(_),_) |
mk__record |
|
|
|
upf_X(upf_X(_,_),_) |
record |
|
|
|
upf_X(upf_Y(_,_),_) |
record |
|
|
|
_ |
eq logic |
equiv simplify |
inference standardisation |
/*---------------------------------------------------------------------------*
| % %%%% %%% %%%%% % % |
| % % % % % % % % © Praxis High Integrity Systems |
| % % % % % % % % |
| % % %%%% % % %%%%% |
| %%%%% % % % % % % |
| % % % % % % % % |
| % % % % %%% % % % |
*----------------------------------------------------------------------------| | $Id$
*----------------------------------------------------------------------------*
| This rulefile is for use with the SPADE Proof Checker. |
*----------------------------------------------------------------------------*
| RULE FAMILIES CONTAINED HEREIN :- |
| arith : simple arithmetic simplification rules |
| assoc : associativity of + and * |
| commut : commutativity of + and * |
| distrib : distributivity of * over + and - |
| minus : rules for unary and binary minus |
| intdiv : rules for the integer div operator |
*----------------------------------------------------------------------------*
| MODEL DECLARATIONS FOR THIS FILE :- |
| |
| rule_family arith: |
| X * Y requires [ X:ir, Y:ir ] & |
| X + Y requires [ X:ir, Y:ir ] & |
| X - Y requires [ X:ir, Y:ir ] & |
| X div Y requires [ X:i, Y:i ] & |
| X / Y requires [ X:ir, Y:ir ]. |
| |
| rule_family assoc: |
| X + Y requires [ X:ir, Y:ir ] & |
| X * Y requires [ X:ir, Y:ir ]. |
| |
| rule_family commut: |
| X + Y requires [ X:ir, Y:ir ] & |
| X * Y requires [ X:ir, Y:ir ]. |
| |
| rule_family distrib: |
| X + Y requires [ X:ir, Y:ir ] & |
| X - Y requires [ X:ir, Y:ir ] & |
| X * Y requires [ X:ir, Y:ir ]. |
| |
| rule_family minus: |
| - X requires [ X:ir ] & |
| X + Y requires [ X:ir, Y:ir ] & |
| X - Y requires [ X:ir, Y:ir ] & |
| X * Y requires [ X:ir, Y:ir ]. |
| |
| rule_family intdiv: |
| X div Y requires [ X:i, Y:i ] & |
| X + Y requires [ X:i, Y:i ] & |
| - X requires [ X:i ]. |
*---------------------------------------------------------------------------*/
/*** SIMPLIFICATION OF ARITHMETIC EXPRESSIONS Rules ***/
arith(1): X*1 may_be_replaced_by X.
arith(2): 1*X may_be_replaced_by X.
arith(3): X+0 may_be_replaced_by X.
arith(4): 0+X may_be_replaced_by X.
arith(5): X - 0 may_be_replaced_by X.
arith(6): X*0 may_be_replaced_by 0.
arith(7): 0*X may_be_replaced_by 0.
arith(8): X div 1 may_be_replaced_by X.
arith(9): (X*N) div N may_be_replaced_by X if [ N<>0 ].
arith(10): (N*X) div N may_be_replaced_by X if [ N<>0 ].
arith(11): X/1 may_be_replaced_by X.
arith(12): (X/Y)*Y may_be_replaced_by X if [ Y<>0 ].
arith(13): Y*(X/Y) may_be_replaced_by X if [ Y<>0 ].
arith(14): (X*Y)/Y may_be_replaced_by X if [ Y<>0 ].
arith(15): (Y*X)/Y may_be_replaced_by X if [ Y<>0 ].
/*** ASSOCIATIVITY of + & * Rules ***/
assoc(1): (A+B)+C may_be_replaced_by A+(B+C).
assoc(2): A+(B+C) may_be_replaced_by (A+B)+C.
assoc(3): (A*B)*C may_be_replaced_by A*(B*C).
assoc(4): A*(B*C) may_be_replaced_by (A*B)*C.
/*** COMMUTATIVITY of + & * Rules ***/
commut(1): A+B may_be_replaced_by B+A.
commut(2): A*B may_be_replaced_by B*A.
/*** DISTRIBUTIVITY of * over + & - Rules ***/
distrib(1): A*(B+C) & A*B+A*C are_interchangeable.
distrib(2): (B+C)*A & A*B+A*C are_interchangeable.
distrib(3): A*(B-C) & A*B-A*C are_interchangeable.
distrib(4): (B-C)*A & A*B-A*C are_interchangeable.
/*** Rules for manipulation of unary and binary MINUS operators ***/
minus(1): X-X may_be_replaced_by 0.
minus(2): -(0) may_be_replaced_by 0.
minus(3): -(-X) may_be_replaced_by X.
minus(4): -(A+B) & -A+(-B) are_interchangeable.
minus(5): -(A+B) & -A-B are_interchangeable.
minus(6): -A+(-B) & -A-B are_interchangeable.
minus(7): A+(-B) & A-B are_interchangeable.
minus(8): A+(-B) & -(B-A) are_interchangeable.
minus(9): A-B & -(B-A) are_interchangeable.
minus(10): -A*B & A*(-B) are_interchangeable.
minus(11): -A*B & -(A*B) are_interchangeable.
minus(12): -(A*B) & A*(-B) are_interchangeable.
minus(13): -A*(-B) & A*B are_interchangeable.
/*** Some rules for INTEGER DIVISION ***/
intdiv(1): (A+B) div C & A div C+B div C are_interchangeable
if [B=K*C, A*B>=0].
intdiv(2): (A+B) div C & A div C+B div C are_interchangeable
if [B=C*K, A*B>=0].
intdiv(3): (A+B) div C & A div C+B div C are_interchangeable
if [A=K*C, A*B>=0].
intdiv(4): (A+B) div C & A div C+B div C are_interchangeable
if [A=C*K, A*B>=0].
intdiv(5): (A+B) div C & A div C+D are_interchangeable
if [goal(integer(B)), goal(integer(C)), goal(C\=0),
goal(D iss B div C), goal(B iss D*C), A*B>=0].
intdiv(6): (A+B) div C & D+B div C are_interchangeable
if [goal(integer(A)), goal(integer(C)), goal(C\=0),
goal(D iss A div C), goal(A iss D*C), A*B>=0].
intdiv(7): -A div B & A div (-B) are_interchangeable.
intdiv(8): -A div B & -(A div B) are_interchangeable.
intdiv(9): A div (-B) & -(A div B) are_interchangeable.
intdiv(10): -A div (-B) & A div B are_interchangeable.
intdiv(11): (A*B) div B may_be_replaced_by A if [B<>0].
intdiv(12): (A*B) div (C*B) may_be_replaced_by A div C if [B<>0].
/*----------------------------------------------------------------------------*
| % %%%% %%%% % % % |
| % % % % % % % % % % COPYPRIGHT (C) 1988,93,96 |
| % % % % % % % % % % Praxis Critical Systems, |
| % % %%%% %%%% % % % % 20, Manvers Street, |
| %%%%% % % % % %%%%% % Bath BA1 1PX, |
| % % % % % % % % % England. |
| % % % % % % % % % |
*----------------------------------------------------------------------------*
| SPADE$CHECKER:ARRAY.RUL |
| Version 1.2, released January 1996 |
*----------------------------------------------------------------------------*
| This rulefile is for use with the SPADE Proof Checker. |
*----------------------------------------------------------------------------*
| RULE FAMILY CONTAINED HEREIN :- |
| array : basic properties of FDL array manipulation functions |
| mk__array : rules specific to SPARK array aggregates |
*----------------------------------------------------------------------------*
| MODEL DECLARATION FOR THIS FILE :- |
| |
| rule_family array: |
| element(X, Y) requires [ X:any, Y:any ] & |
| update(X, Y, Z) requires [ X:any, Y:any, Z:any ]. |
| |
| rule_family mk__array: |
| element(X, Y) requires [ X:any, Y:any ]. |
*----------------------------------------------------------------------------*/
/*** Rules specific to ARRAY MANIPULATIONS ***/
array(1): element(update(A,I,X),I) may_be_replaced_by X.
array(2): update(A,I,element(A,I)) may_be_replaced_by A.
array(3): element(update(A,J,X),K) & element(A,K) are_interchangeable if
[ J<>K ].
array(4): update(update(A,I,X),J,Y) & update(update(A,J,Y),I,X)
are_interchangeable if [ I<>J ].
array(5): update(update(A,I,X),I,Y) may_be_replaced_by update(A,I,Y).
/*** Rules specific to SPARK ARRAY AGGREGATES ***/
/* mk__array(1):
element(mk__array(LARGS, Inds := X), [I]) may_be_replaced_by X if
[ "satisfies_index_constraint(Inds, I)" ].
In the above rule, the quoted side-condition can be met as follows:
(1) if Inds is of the form "[J]", by satisfying I = J;
(2) if Inds is of the form "[J .. K]", by satisfying J <= I <= K;
(3) if Inds is of the form "Is & Js", by satisfying either Is or Js.
Note that the last case makes the definition recursive.
Equally, if we can prove that I does not satisfy the index constraints
represented by Inds, we can instead consider whether it satisfies any of
the index constraints in LARGS, and so on recursively until we either
succeed or reach a point where neither satisfaction nor non-satisfaction can
be proved (because of an insufficiently powerful inference engine, for
instance, or because the index I is insufficiently constrained by the
hypotheses of the VC).
Given the above, the following is a general-purpose rule for fetching the
value of an element of an array aggregate (where this is non-trivial): */
mk__array(1):
element(MK__ARRAY_PART, [I]) may_be_replaced_by VALUE if
[ goal(nonvar(MK__ARRAY_PART)),
goal(MK__ARRAY_PART =.. [mk__array|ARGUMENTS]),
goal(find_element(MK__ARRAY_PART, [I], VALUE)) ].
/* mk__array(2):
element(mk__ARRAYTYPE(LARGS, Inds := X), [I]) may_be_replaced_by X if
[ "satisfies_index_constraint(Inds, I)" ].
In the above rule, the quoted side-condition can be met as follows:
(1) if Inds is of the form "[J]", by satisfying I = J;
(2) if Inds is of the form "[J .. K]", by satisfying J <= I <= K;
(3) if Inds is of the form "Is & Js", by satisfying either Is or Js.
Note that the last case makes the definition recursive.
Given the above, the following is a general-purpose rule for fetching the
value of an element of a typed array aggregate (where non-trivial): */
mk__array(2):
element(MK__ARRAY_PART, [I]) may_be_replaced_by VALUE if
[ goal(nonvar(MK__ARRAY_PART)),
goal(MK__ARRAY_PART =.. [MK__ARRAYTYPE|ARGUMENTS]),
goal(mk__function_name(MK__ARRAYTYPE, _, array)),
goal(find_element(MK__ARRAY_PART, [I], VALUE)) ].
/* It is recommended that the user should avoid reasoning about the
equality (or otherwise) of two array aggregates. */
/*----------------------------------------------------------------------------*
| %%%% %%% %%%%% % % %%% %%% %%%% |
| % % % % % % % % % % COPYRIGHT (C) 2001 |
| % % % % % % % % % Praxis Critical Systems Ltd |
| %%%% % % % % % %%% %%%% Bath, UK. |
| % % % % % % % % % |
| % % % % % % % % % % % |
| %%%% %%% % % % %%% %%% %%%%% |
*----------------------------------------------------------------------------*
BITWISE.RUL -- $Id: BITWISE.RUL,v 1.3 2002/05/30 10:05:56 spark Exp $
*----------------------------------------------------------------------------*
| This rulefile is for use with the SPADE Proof Checker in conjunction with |
| VC files generated by the SPARK Examiner v6.0 or later |
*----------------------------------------------------------------------------*
| RULE FAMILIES CONTAINED HEREIN :- |
| bitwise : bitwise logical operators for SPARK Modular Types |
*----------------------------------------------------------------------------*
| MODEL DECLARATIONS FOR THIS FILE :- |
| |
| rule_family bitwise: |
| bit__and(I,J) requires [I : i, J : i] & |
| bit__or(I,J) requires [I : i, J : i] & |
| bit__xor(I,J) requires [I : i, J : i] & |
| bit__and(I,J) = K requires [I : i, J : i, K : i] & |
| bit__or(I,J) = K requires [I : i, J : i, K : i] & |
| bit__xor(I,J) = K requires [I : i, J : i, K : i] & |
| I < J requires [I : i, J : i] & |
| I <= J requires [I : i, J : i] & |
| I = J requires [I : i, J : i]. |
*----------------------------------------------------------------------------*/
/*** Simplification of bitwise operators ***/
bitwise(1): bit__and(X,X) may_be_replaced_by X if [ 0 <= X ].
bitwise(2): bit__or(X,X) may_be_replaced_by X if [ 0 <= X ].
bitwise(3): bit__xor(X,X) may_be_replaced_by 0 if [ 0 <= X ].
bitwise(4): bit__and(X, 2**N - 1) may_be_replaced_by X if [ 0 <= X, 0 <= N,
X <= 2**N - 1 ].
/*** Properties of zero ***/
bitwise(11): bit__and(X,0) may_be_replaced_by 0 if [ 0 <= X ].
bitwise(12): bit__or(X,0) may_be_replaced_by X if [ 0 <= X ].
bitwise(13): bit__xor(X,0) may_be_replaced_by X if [ 0 <= X ].
/*** Commutativity ***/
bitwise(21): bit__and(X,Y) may_be_replaced_by
bit__and(Y,X) if [ 0 <= X, 0 <= Y ].
bitwise(22): bit__or(X,Y) may_be_replaced_by
bit__or(Y,X) if [ 0 <= X, 0 <= Y ].
bitwise(23): bit__xor(X,Y) may_be_replaced_by
bit__xor(Y,X) if [ 0 <= X, 0 <= Y ].
/*** Associativity ***/
bitwise(31): bit__and(bit__and(X,Y), Z) may_be_replaced_by
bit__and(bit__and(X,Z), Y) if [ 0 <= X, 0 <= Y ].
bitwise(32): bit__or(bit__or(X,Y), Z) may_be_replaced_by
bit__or(bit__or(X,Z), Y) if [ 0 <= X, 0 <= Y ].
bitwise(33): bit__xor(bit__xor(X,Y), Z) may_be_replaced_by
bit__xor(bit__xor(X,Z), Y) if [ 0 <= X, 0 <= Y ].
/*** Distributivity of bit__and and bit__or (bit__xor requires negation)***/
bitwise(41): bit__or(bit__and(X,Y), Z) & bit__and(bit__or(X,Z), bit__or(Y,Z))
are_interchangeable if [ 0 <= X, 0 <= Y, 0 <= Z ].
bitwise(42): bit__and(bit__or(X,Y), Z) & bit__or(bit__and(X,Z), bit__and(Y,Z))
are_interchangeable if [ 0 <= X, 0 <= Y, 0 <= Z ].
/*** Lower bounds ***/
bitwise(51): 0 <= bit__and(X,Y) may_be_deduced_from [ 0 <= X, 0 <= Y ].
bitwise(52): 0 <= bit__or(X,Y) may_be_deduced_from [ 0 <= X, 0 <= Y ].
bitwise(53): 0 <= bit__xor(X,Y) may_be_deduced_from [ 0 <= X, 0 <= Y ].
bitwise(54): X <= bit__or(X,Y) may_be_deduced_from [ 0 <= X, 0 <= Y ].
bitwise(55): Y <= bit__or(X,Y) may_be_deduced_from [ 0 <= X, 0 <= Y ].
bitwise(56): X - Y <= bit__xor(X, Y) may_be_deduced_from [ 0 <= X, 0 <= Y ].
bitwise(57): Y - X <= bit__xor(X, Y) may_be_deduced_from [ 0 <= X, 0 <= Y ].
/*** Upper bounds ***/
bitwise(61): bit__and(X,Y) <= X may_be_deduced_from [ 0 <= X, 0 <= Y ].
bitwise(62): bit__and(X,Y) <= Y may_be_deduced_from [ 0 <= X, 0 <= Y ].
bitwise(63): bit__or(X,Y) <= X + Y may_be_deduced_from [ 0 <= X, 0 <= Y ].
bitwise(64): bit__xor(X,Y) <= X + Y may_be_deduced_from [ 0 <= X, 0 <= Y ].
bitwise(65): bit__and(X,Y) <= Z may_be_deduced_from [ 0 <= X, 0 <= Y,
X <= Z or Y <= Z].
bitwise(66): bit__or(X,Y) <= 2**N - 1 may_be_deduced_from [ 0 <= X, 0 <= Y,
0 <= N,
X <= 2**N - 1,
Y <= 2**N - 1 ].
bitwise(67): bit__xor(X,Y) <= 2**N - 1 may_be_deduced_from [ 0 <= X, 0 <= Y,
0 <= N,
X <= 2**N - 1,
Y <= 2**N - 1].
/*** Values ***/
bitwise(72): bit__or(X,Y) may_be_replaced_by X + Y - bit__and(X,Y)
if [ 0 <= X, 0 <= Y ].
bitwise(73): bit__xor(X,Y) may_be_replaced_by X + Y - 2 * bit__and(X,Y)
if [ 0 <= X, 0 <= Y ].
/*** Comparison ***/
bitwise(81): bit__and(X,Y) <= bit__or(X,Y) may_be_deduced_from
[ 0 <= X, 0 <= Y].
bitwise(82): bit__xor(X,Y) <= bit__or(X,Y) may_be_deduced_from
[ 0 <= X, 0 <= Y].
/*** Combination of X with ~X ***/
bitwise(91): bit__and(X, 2**N - X - 1) = 0 may_be_deduced_from
[ 0 <= X, 0 <= N, X <= 2**N - 1 ].
bitwise(92): bit__or(X, 2**N - X - 1) = 2**N - 1 may_be_deduced_from
[ 0 <= X, 0 <= N, X <= 2**N - 1 ].
bitwise(93): bit__xor(X, 2**N - X - 1) = 2**N - 1 may_be_deduced_from
[ 0 <= X, 0 <= N, X <= 2**N - 1 ].
/*** Maximum value argument ***/
bitwise(101): bit__and(X, 2**N - 1) = 2**N - 1 may_be_deduced_from
[ 0 <= X, 0 <= N, X <= 2**N - 1 ].
bitwise(102): bit__or(X, 2**N - 1) = 2**N - 1 may_be_deduced_from
[ 0 <= X, 0 <= N, X <= 2**N - 1 ].
bitwise(103): bit__xor(X, 2**N - 1) = 2**N - X - 1 may_be_deduced_from
[ 0 <= X, 0 <= N, X <= 2**N - 1 ].
/*** Definition of bit__and ***/
bitwise(111): bit__and(X, Y) may_be_replaced_by 2 * bit__and(X div 2, Y div 2) +
(X mod 2) * (Y mod 2) if [0 <= X, 0 <= Y ].
/*---------------------------------------------------------------------------*
| $Id: ENUM.RUL,v 1.3 2005/07/01 15:11:28 spark Exp $
*----------------------------------------------------------------------------*
| This rulefile is for use with the SPADE Proof Checker. |
*----------------------------------------------------------------------------*
| RULE FAMILIES CONTAINED HEREIN :- |
| enum : properties of enumerated types (pred & succ etc.) |
| enum_cases : list of cases for enumerations of size 2..25 elements |
*----------------------------------------------------------------------------*
| MODEL DECLARATIONS FOR THIS FILE :- |
| |
| rule_family enum: |
| X = Y requires [ X:e, Y:e ] & |
| X <= Y requires [ X:e, Y:e ] & |
| X < Y requires [ X:e, Y:e ] & |
| X >= Y requires [ X:e, Y:e ] & |
| X > Y requires [ X:e, Y:e ] & |
| X <> Y requires [ X:e, Y:e ] & |
| X or Y requires [ X:any, Y:any ] & |
| succ(X) requires [ X:e ] & |
| pred(X) requires [ X:e ]. |
| |
| rule_family enum_cases: |
| X or Y requires [ X:any, Y:any ]. |
*---------------------------------------------------------------------------*/
/*** Enumerated type rules ***/
enum(1): pred(succ(X))=X may_be_deduced_from
[ goal(enumeration_list(X,L)),
goal(\+ last(L,X)) ].
enum(2): X=pred(succ(X)) may_be_deduced_from
[ goal(enumeration_list(X,L)),
goal(\+ last(L,X)) ].
enum(3): succ(pred(X))=X may_be_deduced_from
[ goal(enumeration_list(X,L)),
goal(L\=[X|_]) ].
enum(4): X=succ(pred(X)) may_be_deduced_from
[ goal(enumeration_list(X,L)),
goal(L\=[X|_]) ].
enum(5): X <= Y may_be_deduced_from
[ goal(enumeration_list(X,L)),
goal(in_order(X,Y,L)) ].
enum(6): X < Y may_be_deduced_from
[ goal(enumeration_list(X,L)),
goal(in_order(X,Y,L)), goal(X\=Y) ].
enum(7): Y >= X may_be_deduced_from
[ goal(enumeration_list(X,L)),
goal(in_order(X,Y,L)) ].
enum(8): Y > X may_be_deduced_from
[ goal(enumeration_list(X,L)),
goal(in_order(X,Y,L)), goal(X\=Y) ].
enum(9): X<>Y may_be_deduced_from
[ goal(enumeration_list(X,L)), goal(is_in(X,L)),
goal(is_in(Y,L)), goal(X\=Y) ].
enum(10): X=E may_be_deduced_from
[ X<=E, goal(enumeration_list(E,[E|_])) ].
enum(11): X=E may_be_deduced_from
[ X<F, goal(enumeration_list(F,[E,F|_])) ].
enum(12): X=E may_be_deduced_from
[ X>=E, goal(enumeration_list(E,L)), goal(last(L,E)) ].
enum(13): X=E may_be_deduced_from
[ X>F, goal(enumeration_list(E,L)), goal(last(L,E)),
goal(sublist([F,E],L)) ].
enum(14): X=E1 or X>=E2 may_be_deduced_from
[ X>=E1, goal(enumeration_list(E1,L)),
goal(sublist([E1,E2],L)) ].
enum(15): X=E or REST may_be_deduced_from
[ goal(atom(E)), goal(enumeration_list(E,L)),
goal(build_other_cases(X,E,L,REST)),
goal(REST\=false) ].
enum(16): X=E may_be_deduced_from
[ goal(atom(E)), goal(enumeration_list(E,L)),
goal(build_other_cases(X,E,L,false)) ].
enum(17): succ(Y) may_be_replaced_by X if
[ goal(enumeration_list(Y,L)),
goal(sublist([Y,X],L)) ].
enum(18): pred(X) may_be_replaced_by Y if
[ goal(enumeration_list(X,L)),
goal(sublist([Y,X],L)) ].
enum_cases(2): X=A or X=B may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,[A,B])) ].
enum_cases(3): X=A or X=B or X=C may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,[A,B,C])) ].
enum_cases(4): X=A or X=B or X=C or X=D may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,[A,B,C,D])) ].
enum_cases(5): X=A or X=B or X=C or X=D or X=E may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,[A,B,C,D,E])) ].
enum_cases(6): X=A or X=B or X=C or X=D or X=E or X=F may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,[A,B,C,D,E,F])) ].
enum_cases(7): X=A or X=B or X=C or X=D or X=E or X=F or X=G
may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,[A,B,C,D,E,F,G])) ].
enum_cases(8): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H
may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,[A,B,C,D,E,F,G,H])) ].
enum_cases(9): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I
may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,[A,B,C,D,E,F,G,H,I])) ].
enum_cases(10): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I
or X=J may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,[A,B,C,D,E,F,G,H,I,J])) ].
enum_cases(11): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I
or X=J or X=K may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,[A,B,C,D,E,F,G,H,I,J,K])) ].
enum_cases(12): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I
or X=J or X=K or X=L may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,[A,B,C,D,E,F,G,H,I,J,K,L])) ].
enum_cases(13): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or
X=J or X=K or X=L or X=M may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,[A,B,C,D,E,F,G,H,I,J,K,L,M])) ].
enum_cases(14): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or
X=J or X=K or X=L or X=M or X=N may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,
[A,B,C,D,E,F,G,H,I,J,K,L,M,N])) ].
enum_cases(15): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or
X=J or X=K or X=L or X=M or X=N or X=O may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,
[A,B,C,D,E,F,G,H,I,J,K,L,M,N,O])) ].
enum_cases(16): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or
X=J or X=K or X=L or X=M or X=N or X=O or X=P
may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,
[A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P])) ].
enum_cases(17): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or
X=J or X=K or X=L or X=M or X=N or X=O or X=P or X=Q
may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,
[A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q])) ].
enum_cases(18): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or
X=J or X=K or X=L or X=M or X=N or X=O or X=P or X=Q or X=R
may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,
[A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R])) ].
enum_cases(19): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or
X=J or X=K or X=L or X=M or X=N or X=O or X=P or X=Q or X=R or
X=S may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,
[A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S])) ].
enum_cases(20): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or
X=J or X=K or X=L or X=M or X=N or X=O or X=P or X=Q or X=R or
X=S or X=T may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,
[A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T])) ].
enum_cases(21): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or
X=J or X=K or X=L or X=M or X=N or X=O or X=P or X=Q or X=R or
X=S or X=T or X=U may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,
[A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U])) ].
enum_cases(22): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or
X=J or X=K or X=L or X=M or X=N or X=O or X=P or X=Q or X=R or
X=S or X=T or X=U or X=V may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,
[A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V])) ].
enum_cases(23): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or
X=J or X=K or X=L or X=M or X=N or X=O or X=P or X=Q or X=R or
X=S or X=T or X=U or X=V or X=W may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,
[A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W])) ].
enum_cases(24): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or
X=J or X=K or X=L or X=M or X=N or X=O or X=P or X=Q or X=R or
X=S or X=T or X=U or X=V or X=W or X=Y may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,[A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,
P,Q,R,S,T,U,V,W,Y])) ].
enum_cases(25): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or
X=J or X=K or X=L or X=M or X=N or X=O or X=P or X=Q or X=R or
X=S or X=T or X=U or X=V or X=W or X=Y or X=Z
may_be_deduced_from
[ goal(atom(X)),
goal(checktype(X,TYPE)),
goal(type(TYPE,enumerated)),
goal(enumeration(TYPE,[A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,
P,Q,R,S,T,U,V,W,Y,Z])) ].
/*----------------------------------------------------------------------------*
| %%%%% % % % % % % %%%%% %%%% % %%%%% %%% %%% % % |
| % % % % % %% %% % % % % % % % % % % % |
| % %% % % % % % % % % % % % % % % % %% % |
| %%% % % % % % % % %%% %%%% % % % % % % % % % |
| % % %% % % % % % % % %%%%% % % % % % %% |
| % % % % % % % % % % % % % % % % % % |
| %%%%% % % %%% % % %%%%% % % % % % %%% %%% % % |
*----------------------------------------------------------------------------*
| This rulefile is for use with the SPADE Proof Checker. |
*----------------------------------------------------------------------------*
| RULE FAMILIES CONTAINED HEREIN :- |
| enumeration : more properties of enumerated types (pred & succ etc.) |
*----------------------------------------------------------------------------*
| $Id: ENUMERATION.RUL,v 1.3 2002/05/30 13:56:55 spark Exp $
| |
| Modification History |
| |
| Date CFR Description |
| ---- --- ----------- |
| 30/05/2002 1054 Add this file to Checker standard rule library |
| 30/05/2002 1054 Actions from review S.P0468.59.5 |
| |
*----------------------------------------------------------------------------*/
/*----------------------------------------------------------------------------*
| DECLARATIONS FOR THIS FILE :- |
*----------------------------------------------------------------------------*
| rule_family enumeration: |
| X <= Y requires [ X:e, Y:e ] & |
| X < Y requires [ X:e, Y:e ] & |
| X >= Y requires [ X:e, Y:e ] & |
| X > Y requires [ X:e, Y:e ] & |
| X <> Y requires [ X:e, Y:e ] & |
| succ(X) requires [ X:e ] & |
| pred(X) requires [ X:e ]. |
*----------------------------------------------------------------------------*/
/*** Enumerated type inequality rules ***/
/* Predecessor */
enumeration(1): X <= pred(Y) may_be_deduced_from [ X < Y ].
enumeration(2): pred(X) <= Y may_be_deduced_from
[ X <= Y, goal(checktype(X, T)),
goal(enumeration(T, [E|_])),
X <> E ].
enumeration(3): pred(X) >= Y may_be_deduced_from [ X > Y ].
enumeration(4): X >= pred(Y) may_be_deduced_from
[ X >= Y, goal(checktype(Y, T)),
goal(enumeration(T, [E|_])),
Y <> E ].
enumeration(5): X > Y may_be_deduced_from [ pred(X) >= Y ].
enumeration(6): X < Y may_be_deduced_from [ X <= pred(Y) ].
enumeration(7): X <= Y may_be_deduced_from [ pred(X) < Y ].
enumeration(8): X >= Y may_be_deduced_from [ X > pred(Y) ].
enumeration(9): pred(X) < Y may_be_deduced_from
[ X <= Y, goal(checktype(X, T)),
goal(enumeration(T, [E|_])),
X <> E ].
enumeration(10): X > pred(Y) may_be_deduced_from
[ X >= Y, goal(checktype(Y, T)),
goal(enumeration(T, [E|_])),
Y <> E ].
enumeration(11): pred(X) < X may_be_deduced_from
[ goal(checktype(X, T)),
goal(enumeration(T,[E|_])),
X <> E ].
enumeration(12): X > pred(X) may_be_deduced_from
[ goal(checktype(X, T)),
goal(enumeration(T,[E|_])),
X <> E ].
/* Successor */
enumeration(13): X <= succ(Y) may_be_deduced_from
[ X <= Y, goal(checktype(Y, T)),
goal(enumeration(T, L)),
goal(last(L, E)),
Y <> E ].
enumeration(14): succ(X) <= Y may_be_deduced_from [ X < Y ].
enumeration(15): succ(X) >= Y may_be_deduced_from
[ X >= Y, goal(checktype(X, T)),
goal(enumeration(T, L)),
goal(last(L, E)),
X <> E ].
enumeration(16): X >= succ(Y) may_be_deduced_from [ X > Y ].
enumeration(17): X < Y may_be_deduced_from [ succ(X) <= Y ].
enumeration(18): X > Y may_be_deduced_from [ X >= succ(Y) ].
enumeration(19): X >= Y may_be_deduced_from [ succ(X) > Y ].
enumeration(20): X <= Y may_be_deduced_from [ X < succ(Y) ].
enumeration(21): succ(X) > Y may_be_deduced_from
[ X >= Y, goal(checktype(X, T)),
goal(enumeration(T, L)),
goal(last(L, E)),
X <> E ].
enumeration(22): X < succ(Y) may_be_deduced_from
[ X <= Y, goal(checktype(Y, T)),
goal(enumeration(T, L)),
goal(last(L, E)),
Y <> E ].
enumeration(23): succ(X) > X may_be_deduced_from
[ goal(checktype(X, T)),
goal(enumeration(T, L)),
goal(last(L, E)),
X <> E ].
enumeration(24): X < succ(X) may_be_deduced_from
[ goal(checktype(X, T)),
goal(enumeration(T, L)),
goal(last(L, E)),
X <> E ].
/* General */
enumeration(25): X <> E may_be_deduced_from
[ X > Y, goal(checktype(X, T)),
goal(enumeration(T, [E|_])) ].
enumeration(26): X <> E may_be_deduced_from
[ X < Y, goal(checktype(X, T)),
goal(enumeration(T, L)),
goal(last(L, E)) ].
/*============================================================================*
Justifications
--------------
1: If X < Y, then X <= pred(Y) must hold. (Note that because X < Y, Y
cannot be equal to the first enumeration literal in its type.)
2: If X <= Y, then if pred(X) exists it must also be <= Y. (The additional
immediate conditions ensure X is not the first literal, so pred(X)
does indeed exist.)
3: This rule is equivalent to rule 1 (though with X and Y interchanged).
4: This rule is equivalent to rule 2 (though with X and Y interchanged).
5: Given pred(X) >= Y, X cannot be the first enumeration literal in its type
and given X > pred(X) (rule 12) we see X > Y by transitivity.
6: This rule is equivalent to rule 5 (though with X and Y interchanged).
7: Given pred(X) < Y, X cannot be the first enumeration literal in its type.
If pred(X) < Y it follows that X <= Y (since if X > Y were to hold, then
pred(X) would have to be at least Y).
8: This rule is equivalent to rule 7 (though with X and Y interchanged).
9: If X <= Y then provided X is not equal to the first enumeration literal
in its type, pred(X) exists and pred(X) < X (rule 11), so pred(X) < Y by
transitivity.
10: This rule is equivalent to rule 9 (though with X and Y interchanged).
11: If X is not equal to the first enumeration literal in its type, then
pred(X) exists. Whenever this is so, pred(X) precedes X in the type,
so pred(X) < X holds in such cases as required.
12: This rule is equivalent to rule 11.
13: If Y is not equal to the last enumeration literal in its type, then
succ(Y) exists and Y<succ(Y) (rule 24), so X <= succ(Y) by transitivity.
14: If X < Y, X cannot be the last enumeration literal in its type, so
succ(X) exists and must be at most Y (since if it were greater than Y,
then X would have to be at least Y, contradicting X < Y).
15: This rule is equivalent to rule 13 (though with X and Y interchanged).
16: This rule is equivalent to rule 14 (though with X and Y interchanged).
17: Given succ(X) <= Y, X is not the last enumeration literal in its type, so
X < succ(X) (rule 24), thus X < Y by transitivity.
18: This rule is equivalent to rule 17 (though with X and Y interchanged).
19: If succ(X) > Y, then X must be at least Y as required.
20: This rule is equivalent to rule 19 (though with X and Y interchanged).
21: If X is not the last enumeration literal in its type, then succ(X) > X
(rule 23), so succ(X) > Y follows from X >= Y by transitivity.
22: This rule is equivalent to rule 21 (though with X and Y interchanged).
23: If X is not equal to the last enumeration literal in its type, then
succ(X) exists. Whenever this is so, succ(X) succeeds X in the type,
so succ(X) > X holds in such cases as required.
24: This rule is equivalent to rule 23.
25: If X is bigger than something (Y), then X cannot be equal to the first
enumeration literal in its type.
26: If X is smaller than something (Y), then X cannot be equal to the last
enumeration literal in its type.
*============================================================================*/
/*---------------------------------------------------------------------------*
| %%%%% %%%% % %%%%% % % % % %%% %%% |
| % % % % % % % % % % % % % COPYPRIGHT (C) 1988-2004 |
| % % % % % % % %% % % % Praxis Critical Systems |
| %%% % % % %%% % % % % % % %%% |
| % % % % % % % % %% % % |
| % % % % % % % % % % % % % |
| % %%%% %%%%% % %%% % % %%% %%% |
*----------------------------------------------------------------------------*
| $Id: FDLFUNCS.RUL,v 1.2 2004/06/07 15:04:28 spark Exp $
|
*----------------------------------------------------------------------------*
| This rulefile is for use with the SPADE Proof Checker. |
*----------------------------------------------------------------------------*
| RULE FAMILIES CONTAINED HEREIN :- |
| abs : properties of the absolute value function abs(_) |
| sqr : properties of the square function sqr(_) |
| odd : properties of predicate odd(_) |
| exp : properties of the exponentiation operator ** |
*----------------------------------------------------------------------------*
| MODEL DECLARATIONS FOR THIS FILE :- |
| |
| rule_family abs: |
| abs(X) requires [ X:ir ] & |
| X >= Y requires [ X:ir, Y:ir ] & |
| X > Y requires [ X:ir, Y:ir ] & |
| X or Y requires [ X:any, Y:any ] & |
| X * Y requires [ X:ir, Y:ir ]. |
| |
| rule_family sqr: |
| sqr(X) requires [ X:ir ] & |
| X >= Y requires [ X:ir, Y:ir ] & |
| X > Y requires [ X:ir, Y:ir ] & |
| X * Y requires [ X:ir, Y:ir ] & |
| abs(X) requires [ X:ir ]. |
| |
| rule_family odd: |
| odd(X) requires [ X:i ] & |
| not X requires [ X:any ] & |
| X <> Y requires [ X:i, Y:i ] & |
| X = Y requires [ X:i, Y:i ]. |
| |
| rule_family exp: |
| X ** Y requires [ X:ir, Y:i ] & |
| X * Y requires [ X:ir, Y:ir ] & |
| X >= Y requires [ X:ir, Y:ir ] & |
| X <= Y requires [ X:ir, Y:ir ] & |
| X > Y requires [ X:ir, Y:ir ] & |
| X < Y requires [ X:ir, Y:ir ]. |
*---------------------------------------------------------------------------*/
/*** ABS: absolute value function properties ***/
abs(1): abs(X) may_be_replaced_by X if [ X>=0 ].
abs(2): abs(X) may_be_replaced_by -X if [ X<=0 ].
abs(3): abs(X)>=0 may_be_deduced.
abs(4): abs(X)>0 may_be_deduced_from [ X<>0 ].
abs(5): abs(X)=X or abs(X)=(-X) may_be_deduced.
abs(6): abs(abs(X)) may_be_replaced_by abs(X).
abs(7): abs(X*Y) & abs(X)*abs(Y) are_interchangeable.
/*** SQR: square function properties ***/
sqr(1): sqr(X) may_be_replaced_by X*X.
sqr(2): sqr(X)>=0 may_be_deduced.
sqr(3): sqr(X)>0 may_be_deduced_from [ X<>0 ].
sqr(4): sqr(X*Y) & sqr(X)*sqr(Y) are_interchangeable.
sqr(5): abs(sqr(X)) may_be_replaced_by sqr(X).
sqr(6): sqr(abs(X)) may_be_replaced_by sqr(X).
/*** ODD: odd function properties ***/
odd(1): odd(X) & (X div 2) * 2 <> X are_interchangeable.
odd(2): not odd(X) & (X div 2) * 2 = X are_interchangeable.
odd(3): odd(X) may_be_deduced_from [ X=2*K+1 ].
odd(4): not odd(X) may_be_deduced_from [ X=2*K ].
odd(5): odd(X) may_be_deduced_from [ odd(-X) ].
odd(6): odd(-X) may_be_deduced_from [ odd(X) ].
odd(7): not odd(X) may_be_deduced_from [ not odd(-X) ].
odd(8): not odd(-X) may_be_deduced_from [ not odd(X) ].
odd(9): odd(X+Y) may_be_deduced_from [ odd(X), not odd(Y) ].
odd(10): odd(X+Y) may_be_deduced_from [ not odd(X), odd(Y) ].
odd(11): not odd(X+Y) may_be_deduced_from [ not odd(X), not odd(Y) ].
odd(12): not odd(X+Y) may_be_deduced_from [ odd(X), odd(Y) ].
odd(13): odd(X-Y) may_be_deduced_from [ odd(X), not odd(Y) ].
odd(14): odd(X-Y) may_be_deduced_from [ not odd(X), odd(Y) ].
odd(15): not odd(X-Y) may_be_deduced_from [ not odd(X), not odd(Y) ].
odd(16): not odd(X-Y) may_be_deduced_from [ odd(X), odd(Y) ].
odd(17): odd(X*Y) may_be_deduced_from [ odd(X), odd(Y) ].
odd(18): not odd(X*Y) may_be_deduced_from [ not odd(X) ].
odd(19): not odd(X*Y) may_be_deduced_from [ not odd(Y) ].
odd(20): odd(sqr(X)) may_be_deduced_from [ odd(X) ].
odd(21): odd(X) may_be_deduced_from [ odd(sqr(X)) ].
odd(22): not odd(sqr(X)) may_be_deduced_from [ not odd(X) ].
odd(23): not odd(X) may_be_deduced_from [ not odd(sqr(X)) ].
odd(24): odd(abs(X)) may_be_deduced_from [ odd(X) ].
odd(25): odd(X) may_be_deduced_from [ odd(abs(X)) ].
odd(26): not odd(abs(X)) may_be_deduced_from [ not odd(X) ].
odd(27): not odd(X) may_be_deduced_from [ not odd(abs(X)) ].
/*** EXP: exponentiation operator properties - for non-negative exponents ***/
exp(1): X**0 may_be_replaced_by 1.
exp(2): 0**Y may_be_replaced_by 0 if [ Y>=1 ].
exp(3): 1**Y may_be_replaced_by 1 if [ Y>=0 ].
exp(4): X**Y & X*(X**(Y-1)) are_interchangeable if [ Y>0 ].
exp(5): X**(Y+1) & X*(X**Y) are_interchangeable if [ Y>=0 ].
exp(6): (-X)**Y may_be_replaced_by X**Y if [ not odd(Y) ].
exp(7): (-X)**Y may_be_replaced_by -(X**Y) if [ odd(Y) ].
exp(8): X**1 may_be_replaced_by X.
exp(9): X**2 may_be_replaced_by X*X.
exp(10): X**3 may_be_replaced_by X*X*X.
exp(11): X**4 may_be_replaced_by X*X*X*X.
exp(12): X**Y>=0 may_be_deduced_from [ X>=0, Y>=0 ].
exp(13): X**Y>=0 may_be_deduced_from [ not odd(Y) ].
exp(14): X**Y<=0 may_be_deduced_from [ X<=0, odd(Y) ].
exp(15): X**Y>0 may_be_deduced_from [ X>0 ].
exp(16): X**Y>0 may_be_deduced_from [ X<0, not odd(Y) ].
exp(17): X**Y<0 may_be_deduced_from [ X<0, odd(Y) ].
/*---------------------------------------------------------------------------*
| %%% %%%%% % % %%% % % %%%%% %%% %%% |
| % % % % % % % % % % % % % COPYPRIGHT (C) 1988,1991 |
| % % %% % % %% % % % % % Program Validation Ltd., |
| % %%% % % % % % % % %%% % % %%% 26, Queen’s Terrace, |
| % %% % % %% % % %% % % % % % Southampton SO1 1BQ, |
| % % % % % % % % % % % % % England. |
| %%%% %%%%% % % %%% % % %%%%% %% % %%% |
*----------------------------------------------------------------------------*
| SPADE$CHECKER:GENINEQS.RUL |
| Version 1.2, released January 1991 |
*----------------------------------------------------------------------------*
| This rulefile is for use with the SPADE Proof Checker. |
*----------------------------------------------------------------------------*
| RULE FAMILIES CONTAINED HEREIN :- |
| transitivity : transitivity of relational operators |
| strengthen : inequalities strengthening rules |
| negation : negation of inequalities rules |
*----------------------------------------------------------------------------*
| MODEL DECLARATIONS FOR THIS FILE :- |
| |
| rule_family transitivity: |
| X <= Y requires [ X:ire, Y:ire ] & |
| X >= Y requires [ X:ire, Y:ire ] & |
| X < Y requires [ X:ire, Y:ire ] & |
| X > Y requires [ X:ire, Y:ire ] & |
| X = Y requires [ X:any, Y:any ] & |
| X <> Y requires [ X:any, Y:any ]. |
| |
| rule_family strengthen: |
| X > Y requires [ X:ire, Y:ire ] & |
| X < Y requires [ X:ire, Y:ire ] & |
| X = Y requires [ X:ire, Y:ire ]. |
| |
| rule_family negation: |
| not X requires [ X:any ] & |
| X <> Y requires [ X:any, Y:any ] & |
| X = Y requires [ X:any, Y:any ] & |
| X <= Y requires [ X:ire, Y:ire ] & |
| X > Y requires [ X:ire, Y:ire ] & |
| X >= Y requires [ X:ire, Y:ire ] & |
| X < Y requires [ X:ire, Y:ire ]. |
*---------------------------------------------------------------------------*/
/*** TRANSITIVITY Rules ***/
transitivity(1): I<=K may_be_deduced_from [ I<=J, J<=K ].
transitivity(2): I<=K may_be_deduced_from [ I<=J, J<K ].
transitivity(3): I<=K may_be_deduced_from [ I<=J, J=K ].
transitivity(4): I<=K may_be_deduced_from [ I<J, J<=K ].
transitivity(5): I<=K may_be_deduced_from [ I<J, J<K ].
transitivity(6): I<=K may_be_deduced_from [ I<J, J=K ].
transitivity(7): I<=K may_be_deduced_from [ I=J, J<=K ].
transitivity(8): I<=K may_be_deduced_from [ I=J, J<K ].
transitivity(9): I<=K may_be_deduced_from [ I=J, J=K ].
transitivity(10): K>=I may_be_deduced_from [ I<=J, J<=K ].
transitivity(11): K>=I may_be_deduced_from [ I<=J, J<K ].
transitivity(12): K>=I may_be_deduced_from [ I<=J, J=K ].
transitivity(13): K>=I may_be_deduced_from [ I<J, J<=K ].
transitivity(14): K>=I may_be_deduced_from [ I<J, J<K ].
transitivity(15): K>=I may_be_deduced_from [ I<J, J=K ].
transitivity(16): K>=I may_be_deduced_from [ I=J, J<=K ].
transitivity(17): K>=I may_be_deduced_from [ I=J, J<K ].
transitivity(18): K>=I may_be_deduced_from [ I=J, J=K ].
transitivity(19): I<K may_be_deduced_from [ I<=J, J<K ].
transitivity(20): I<K may_be_deduced_from [ I<J, J<=K ].
transitivity(21): I<K may_be_deduced_from [ I<J, J<K ].
transitivity(22): I<K may_be_deduced_from [ I<J, J=K ].
transitivity(23): I<K may_be_deduced_from [ I=J, J<K ].
transitivity(24): K>I may_be_deduced_from [ I<=J, J<K ].
transitivity(25): K>I may_be_deduced_from [ I<J, J<=K ].
transitivity(26): K>I may_be_deduced_from [ I<J, J<K ].
transitivity(27): K>I may_be_deduced_from [ I<J, J=K ].
transitivity(28): K>I may_be_deduced_from [ I=J, J<K ].
transitivity(29): I=K may_be_deduced_from [ I=J, J=K ].
transitivity(30): I<>K may_be_deduced_from [ I<>J, J=K ].
/*** STRENGTHEN Rules ***/
strengthen(1): I>J may_be_deduced_from [ I>=J, I<>J ].
strengthen(2): J<I may_be_deduced_from [ I>=J, I<>J ].
strengthen(3): I=J may_be_deduced_from [ I>=J, I<=J ].
/*** Rules for manipulation of logical NOT operator ***/
negation(1): not(A=B) & A<>B are_interchangeable.
negation(2): not(A<>B) & A=B are_interchangeable.
negation(3): not(A>B) & A<=B are_interchangeable.
negation(4): not(A<=B) & A>B are_interchangeable.
negation(5): not(A<B) & A>=B are_interchangeable.
negation(6): not(A>=B) & A<B are_interchangeable.
negation(7): not(A=B) & B<>A are_interchangeable.
negation(8): not(A<>B) & B=A are_interchangeable.
negation(9): not(A>B) & B>=A are_interchangeable.
negation(10): not(A<=B) & B<A are_interchangeable.
negation(11): not(A<B) & B<=A are_interchangeable.
negation(12): not(A>=B) & B>A are_interchangeable.
/*---------------------------------------------------------------------------*
| %%% % % %%%%% %%% % % %%%%% %%% %%% |
| % % % % % % % % % % % % COPYPRIGHT (C) 1988,89,91 |
| % %% % % % %% % % % % % Program Validation Ltd., |
| % % % % % % % % % %%% % % %%% 26 Queen’s Terrace, |
| % % %% % % % %% % % % % % Southampton SO1 1BQ, |
| % % % % % % % % % % % % England. |
| %%% % % % %%% % % %%%%% %% % %%% |
*----------------------------------------------------------------------------*
| SPADE$CHECKER:INTINEQS.RUL |
| Version 1.2, released January 1991 |
*----------------------------------------------------------------------------*
| This rulefile is for use with the SPADE Proof Checker. |
*----------------------------------------------------------------------------*
| RULE FAMILY CONTAINED HEREIN :- |
| inequals : inequalities rules applicable to integers only |
*----------------------------------------------------------------------------*
| MODEL DECLARATION FOR THIS FILE :- |
| |
| rule_family inequals: |
| X >= Y requires [ X:i, Y:i ] & |
| X <= Y requires [ X:i, Y:i ] & |
| X > Y requires [ X:i, Y:i ] & |
| X = Y requires [ X:i, Y:i ]. |
*---------------------------------------------------------------------------*/
/*** Integer division basic properties ***/
inequals(86): N*(A div N)>=A-N+1 may_be_deduced_from [ N>0, A>=0 ].
inequals(87): (A div N)*N>=A-N+1 may_be_deduced_from [ N>0, A>=0 ].
inequals(88): N*(A div N)<=A may_be_deduced_from [ N<>0, A>=0 ].
inequals(89): (A div N)*N<=A may_be_deduced_from [ N<>0, A>=0 ].
inequals(90): A div N>=0 may_be_deduced_from [ A>=0, N>0 ].
inequals(91): A div N>0 may_be_deduced_from [ A>=N, N>0 ].
inequals(92): A div N>0 may_be_deduced_from [ A<=N, N<0 ].
inequals(93): I div N<=J div N may_be_deduced_from [ I<=J, N>0 ].
inequals(94): I div N>=J div N may_be_deduced_from [ I>=J, N>0 ].
inequals(95): I div M=J div N may_be_deduced_from [ I=J, M=N ].
inequals(96): N*(A div N)>=A+N+1 may_be_deduced_from [ N<0, A>=0 ].
inequals(97): (A div N)*N>=A+N+1 may_be_deduced_from [ N<0, A>=0 ].
inequals(98): A div B>=0 may_be_deduced_from [ A<=0, B<0 ].
inequals(99): A div B<=0 may_be_deduced_from [ A>=0, B<0 ].
inequals(100): A div B<=0 may_be_deduced_from [ A<=0, B>0 ].
/*** Other useful integers-only rules ***/
inequals(101): X>=Y+1 may_be_deduced_from [ X>Y ].
inequals(102): Y+1<=X may_be_deduced_from [ X>Y ].
inequals(103): X>=1 may_be_deduced_from [ X>0 ].
/*---------------------------------------------------------------------------*
| % % % % % % %%% % % %%%%% %%% %%% |
| % % % % %% %% % % % % % % % % COPYPRIGHT (C) 1988,89,93 |
| %% % % % % % % % %% % % % % % Program Validation Ltd., |
| % % % % % % % % % % % %%% % % %%% 26 Queen’s Terrace, |
| % %% % % % % % % %% % % % % % Southampton SO1 1BQ, |
| % % % % % % % % % % % % % % England. |
| % % %%% % % %%% % % %%%%% %% % %%% |
*----------------------------------------------------------------------------*
| SPADE$CHECKER:NUMINEQS.RUL |
| Version 1.2, released August 1993 |
*----------------------------------------------------------------------------*
| This rulefile is for use with the SPADE Proof Checker. |
*----------------------------------------------------------------------------*
| RULE FAMILIES CONTAINED HEREIN :- |
| inequals : inequalities rules for integers and reals |
| zero : equality/non-equality to 0 with multiplication rules |
*----------------------------------------------------------------------------*
| MODEL DECLARATIONS FOR THIS FILE :- |
| |
| rule_family inequals: |
| X < Y requires [ X:ir, Y:ir ] & |
| X <= Y requires [ X:ir, Y:ir ] & |
| X > Y requires [ X:ir, Y:ir ] & |
| X >= Y requires [ X:ir, Y:ir ] & |
| X <> Y requires [ X:ir, Y:ir ] & |
| X = Y requires [ X:ir, Y:ir ]. |
| |
| rule_family zero: |
| X = Y requires [ X:ir, Y:ir ] & |
| X <> Y requires [ X:ir, Y:ir ] & |
| X or Y requires [ X:any, Y:any ]. |
*---------------------------------------------------------------------------*/
/*** INEQUALS Rules ***/
/*** Addition or subtraction of a number from one side of an inequality ***/
inequals(1): I-N<J may_be_deduced_from [ I<J, N>=0 ].
inequals(2): I-N<J may_be_deduced_from [ I<=J, N>0 ].
inequals(3): I-N<=J may_be_deduced_from [ I<=J, N>=0 ].
inequals(4): J>I-N may_be_deduced_from [ I<J, N>=0 ].
inequals(5): J>I-N may_be_deduced_from [ I<=J, N>0 ].
inequals(6): J>=I-N may_be_deduced_from [ I<=J, N>=0 ].
inequals(7): I+N>J may_be_deduced_from [ I>J, N>=0 ].
inequals(8): I+N>J may_be_deduced_from [ I>=J, N>0 ].
inequals(9): I+N>=J may_be_deduced_from [ I>=J, N>=0 ].
inequals(10): N+I>J may_be_deduced_from [ I>J, N>=0 ].
inequals(11): N+I>J may_be_deduced_from [ I>=J, N>0 ].
inequals(12): N+I>=J may_be_deduced_from [ I>=J, N>=0 ].
inequals(13): J<I+N may_be_deduced_from [ I>J, N>=0 ].
inequals(14): J<I+N may_be_deduced_from [ I>=J, N>0 ].
inequals(15): J<=I+N may_be_deduced_from [ I>=J, N>=0 ].
inequals(16): J<N+I may_be_deduced_from [ I>J, N>=0 ].
inequals(17): J<N+I may_be_deduced_from [ I>=J, N>0 ].
inequals(18): J<=N+I may_be_deduced_from [ I>=J, N>=0 ].
/*** Addition and subtraction of a number on both sides of an inequality ***/
inequals(19): I+N<J+N may_be_deduced_from [ I<J ].
inequals(20): N+I<J+N may_be_deduced_from [ I<J ].
inequals(21): I+N<N+J may_be_deduced_from [ I<J ].
inequals(22): N+I<N+J may_be_deduced_from [ I<J ].
inequals(23): I+N>J+N may_be_deduced_from [ I>J ].
inequals(24): N+I>J+N may_be_deduced_from [ I>J ].
inequals(25): I+N>N+J may_be_deduced_from [ I>J ].
inequals(26): N+I>N+J may_be_deduced_from [ I>J ].
inequals(27): I+N<>J+N may_be_deduced_from [ I<>J ].
inequals(28): N+I<>J+N may_be_deduced_from [ I<>J ].
inequals(29): I+N<>N+J may_be_deduced_from [ I<>J ].
inequals(30): N+I<>N+J may_be_deduced_from [ I<>J ].
inequals(31): I-N<J-N may_be_deduced_from [ I<J ].
inequals(32): I-N>J-N may_be_deduced_from [ I>J ].
inequals(33): I-N<>J-N may_be_deduced_from [ I<>J ].
/*** Multiplication on both sides of an inequality by a number ***/
inequals(34): I*N<>J*N may_be_deduced_from [ I<>J, N<>0 ].
inequals(35): I*N>J*N may_be_deduced_from [ I>J, N>0 ].
inequals(36): I*N<J*N may_be_deduced_from [ I<J, N>0 ].
inequals(37): I*N>J*N may_be_deduced_from [ I<J, N<0 ].
inequals(38): I*N<J*N may_be_deduced_from [ I>J, N<0 ].
inequals(39): I*N>=J*N may_be_deduced_from [ I>=J, N>=0 ].
inequals(40): I*N<=J*N may_be_deduced_from [ I<=J, N>=0 ].
inequals(41): I*N>=J*N may_be_deduced_from [ I<=J, N<=0 ].
inequals(42): I*N<=J*N may_be_deduced_from [ I>=J, N<=0 ].
/*** Addition and subtraction of two inequalities ***/
inequals(43): A+C>B+D may_be_deduced_from [ A>=B, C>D ].
inequals(44): A+C>B+D may_be_deduced_from [ A>B, C>=D ].
inequals(45): A+C>B+D may_be_deduced_from [ A>=D, C>B ].
inequals(46): A+C>B+D may_be_deduced_from [ A>D, C>=B ].
inequals(47): A-D>B-C may_be_deduced_from [ A>=B, C>D ].
inequals(48): A-D>B-C may_be_deduced_from [ A>B, C>=D ].
inequals(49): A+C<B+D may_be_deduced_from [ A<=B, C<D ].
inequals(50): A+C<B+D may_be_deduced_from [ A<B, C<=D ].
inequals(51): A+C<B+D may_be_deduced_from [ A<=D, C<B ].
inequals(52): A+C<B+D may_be_deduced_from [ A<D, C<=B ].
inequals(53): A-D<B-C may_be_deduced_from [ A<=B, C<D ].
inequals(54): A-D<B-C may_be_deduced_from [ A<B, C<=D ].
inequals(55): A+C<>B+D may_be_deduced_from [ A<>B, C=D ].
inequals(56): A+C<>B+D may_be_deduced_from [ A=B, C<>D ].
inequals(57): A+C<>B+D may_be_deduced_from [ A<>D, B=C ].
inequals(58): A+C<>B+D may_be_deduced_from [ A=D, B<>C ].
inequals(59): A-D<>B-C may_be_deduced_from [ A<>B, C=D ].
inequals(60): A-D<>B-C may_be_deduced_from [ A=B, C<>D ].
/*** Addition and subtraction of a number on both sides of an inequality ***/
inequals(61): I+N=J+N may_be_deduced_from [ I=J ].
inequals(62): N+I=J+N may_be_deduced_from [ I=J ].
inequals(63): I+N=N+J may_be_deduced_from [ I=J ].
inequals(64): N+I=N+J may_be_deduced_from [ I=J ].
inequals(65): I+N<=J+N may_be_deduced_from [ I<=J ].
inequals(66): N+I<=J+N may_be_deduced_from [ I<=J ].
inequals(67): I+N<=N+J may_be_deduced_from [ I<=J ].
inequals(68): N+I<=N+J may_be_deduced_from [ I<=J ].
inequals(69): I+N>=J+N may_be_deduced_from [ I>=J ].
inequals(70): N+I>=J+N may_be_deduced_from [ I>=J ].
inequals(71): I+N>=N+J may_be_deduced_from [ I>=J ].
inequals(72): N+I>=N+J may_be_deduced_from [ I>=J ].
inequals(73): I-N=J-N may_be_deduced_from [ I=J ].
inequals(74): I-N<=J-N may_be_deduced_from [ I<=J ].
inequals(75): I-N>=J-N may_be_deduced_from [ I>=J ].
/*** Multiplication on both sides of an inequality by a number ***/
inequals(76): I*N=J*N may_be_deduced_from [ I=J ].
/*** Addition and subtraction of two inequalities ***/
inequals(77): A+C>=B+D may_be_deduced_from [ A>=B, C>=D ].
inequals(78): A+C>=B+D may_be_deduced_from [ A>=D, C>=B ].
inequals(79): A-D>=B-C may_be_deduced_from [ A>=B, C>=D ].
inequals(80): A+C<=B+D may_be_deduced_from [ A<=B, C<=D ].
inequals(81): A+C<=B+D may_be_deduced_from [ A<=D, C<=B ].
inequals(82): A-D<=B-C may_be_deduced_from [ A<=B, C<=D ].
inequals(83): A+C=B+D may_be_deduced_from [ A=B, C=D ].
inequals(84): A+C=B+D may_be_deduced_from [ A=D, B=C ].
inequals(85): A-D=B-C may_be_deduced_from [ A=B, C=D ].
/* Rule numbering gap: 86-103 are in INTINEQS; retained for compatibility */
/*** Additional rules for inequalities with multiplication ***/
inequals(104): X=Y may_be_deduced_from [ X*N=Y*N, N<>0 ].
inequals(105): X<>Y may_be_deduced_from [ X*N<>Y*N, N<>0 ].
inequals(106): X<=Y may_be_deduced_from [ X*N<=Y*N, N>0 ].
inequals(107): X<=Y may_be_deduced_from [ X*N>=Y*N, N<0 ].
inequals(108): X>=Y may_be_deduced_from [ X*N>=Y*N, N>0 ].
inequals(109): X>=Y may_be_deduced_from [ X*N<=Y*N, N<0 ].
inequals(110): X<Y may_be_deduced_from [ X*N<Y*N, N>0 ].
inequals(111): X<Y may_be_deduced_from [ X*N>Y*N, N<0 ].
inequals(112): X>Y may_be_deduced_from [ X*N>Y*N, N>0 ].
inequals(113): X>Y may_be_deduced_from [ X*N<Y*N, N<0 ].
inequals(114): X*Y<=0 may_be_deduced_from [ X>=0, Y<=0 ].
inequals(115): X*Y<=0 may_be_deduced_from [ X<=0, Y>=0 ].
inequals(116): X*Y>=0 may_be_deduced_from [ X>=0, Y>=0 ].
inequals(117): X*Y>=0 may_be_deduced_from [ X<=0, Y<=0 ].
inequals(118): X*Y<0 may_be_deduced_from [ X>0, Y<0 ].
inequals(119): X*Y<0 may_be_deduced_from [ X<0, Y>0 ].
inequals(120): X*Y>0 may_be_deduced_from [ X>0, Y>0 ].
inequals(121): X*Y>0 may_be_deduced_from [ X<0, Y<0 ].
/*** Rules for equality and non-equality to zero involving multiplication ***/
zero(1): X * Y = 0 may_be_deduced_from [ X = 0 ].
zero(2): X * Y = 0 may_be_deduced_from [ Y = 0 ].
zero(3): X=0 or Y=0 may_be_deduced_from [ X*Y=0 ].
zero(4): X * Y <> 0 may_be_deduced_from [ X<>0, Y<>0 ].
zero(5): X <> 0 may_be_deduced_from [ X * Y <> 0 ].
zero(6): Y <> 0 may_be_deduced_from [ X * Y <> 0 ].
/*---------------------------------------------------------------------------*
| % %%% %%% %%% %%% |
| % % % % % % % % COPYPRIGHT (C) 1989 |
| % % % % % % Program Validation Ltd., |
| % % % % % % 26 Queen’s Terrace, |
| % % % % %% % % Southampton SO1 1BQ, |
| % % % % % % % % England. |
| %%%%% %%% %%%% %%% %%% |
*----------------------------------------------------------------------------*
| SPADE$CHECKER:LOGIC.RUL |
| Version 1.0, released August 1989 |
*----------------------------------------------------------------------------*
| This rulefile is for use with the SPADE Proof Checker. |
*----------------------------------------------------------------------------*
| RULE FAMILIES CONTAINED HEREIN :- |
| assoc : associativity of “and”, “or” & “<->” |
| commut : commutativity of “and”, “or” & “<->” |
| distrib : distributivity of “and” over “or” and vice versa |
| equivalence : simplification of logical “<->” expressions |
| implies : simplification of logical “->” expressions |
| logical : general logical simplification rules |
| logical_and : simplification of logical “and” expressions |
| logical_not : simplification of logical “not” expressions |
| logical_or : simplification of logical “or” expressions |
*----------------------------------------------------------------------------*
| MODEL DECLARATIONS FOR THIS FILE :- |
| |
| rule_family assoc: |
| X and Y requires [ X:any, Y:any ] & |
| X or Y requires [ X:any, Y:any ] & |
| X <-> Y requires [ X:any, Y:any ]. |
| |
| rule_family commut: |
| X and Y requires [ X:any, Y:any ] & |
| X or Y requires [ X:any, Y:any ] & |
| X <-> Y requires [ X:any, Y:any ]. |
| |
| rule_family distrib: |
| X and Y requires [ X:any, Y:any ] & |
| X or Y requires [ X:any, Y:any ]. |
| |
| rule_family equivalence: |
| X <-> Y requires [ X:any, Y:any ]. |
| |
| rule_family implies: |
| X -> Y requires [ X:any, Y:any ]. |
| |
| rule_family logical_and: |
| X and Y requires [ X:any, Y:any ]. |
| |
| rule_family logical_not: |
| not X requires [ X:any ]. |
| |
| rule_family logical_or: |
| X or Y requires [ X:any, Y:any ]. |
| |
| rule_family logical: |
| not X requires [ X:any ] & |
| X and Y requires [ X:any, Y:any ] & |
| X or Y requires [ X:any, Y:any ] & |
| X -> Y requires [ X:any, Y:any ] & |
| X <-> Y requires [ X:any, Y:any ]. |
*---------------------------------------------------------------------------*/
/*** SIMPLIFICATION OF LOGICAL EXPRESSIONS Rules ***/
/*** Simplification of logical “not” expressions ***/
logical_not(1): not true may_be_replaced_by false.
logical_not(2): not false may_be_replaced_by true.
logical_not(3): not not A may_be_replaced_by A.
/*** Simplification of logical “and” expressions ***/
logical_and(1): A and true may_be_replaced_by A.
logical_and(2): true and A may_be_replaced_by A.
logical_and(3): A and false may_be_replaced_by false.
logical_and(4): false and A may_be_replaced_by false.
logical_and(5): A and A may_be_replaced_by A.
logical_and(6): A and not A may_be_replaced_by false.
logical_and(7): (not A) and A may_be_replaced_by false.
/*** Simplification of logical “or” expressions ***/
logical_or(1): A or false may_be_replaced_by A.
logical_or(2): false or A may_be_replaced_by A.
logical_or(3): A or true may_be_replaced_by true.
logical_or(4): true or A may_be_replaced_by true.
logical_or(5): A or A may_be_replaced_by A.
logical_or(6): A or not A may_be_replaced_by true.
logical_or(7): (not A) or A may_be_replaced_by true.
/*** Simplification of logical “->” expressions ***/
implies(1): A -> true may_be_replaced_by true.
implies(2): A -> false may_be_replaced_by not A.
implies(3): true -> A may_be_replaced_by A.
implies(4): false -> A may_be_replaced_by true.
implies(5): A -> A may_be_replaced_by true.
implies(6): A -> not A may_be_replaced_by not A.
implies(7): (not A) -> A may_be_replaced_by A.
/*** Simplification of logical “<->” expressions ***/
equivalence(1): A <-> true may_be_replaced_by A.
equivalence(2): true <-> A may_be_replaced_by A.
equivalence(3): A <-> false may_be_replaced_by not A.
equivalence(4): false <-> A may_be_replaced_by not A.
equivalence(5): A <-> A may_be_replaced_by true.
equivalence(6): A <-> not A may_be_replaced_by false.
equivalence(7): (not A) <-> A may_be_replaced_by false.
/*** ASSOCIATIVITY of “and”, “or” & “<->” Rules ***/
assoc(5): A and (B and C) & (A and B) and C are_interchangeable.
assoc(6): A or (B or C) & (A or B) or C are_interchangeable.
assoc(7): A <-> (B <-> C) & (A <-> B) <-> C are_interchangeable.
/*** COMMUTATIVITY of “and”, “or” & “<->” Rules ***/
commut(3): A and B may_be_replaced_by B and A.
commut(4): A or B may_be_replaced_by B or A.
commut(5): A <-> B may_be_replaced_by B <-> A.
/*** DISTRIBUTIVITY of “and” and “or” over each other Rules ***/
distrib(5): (A and B) or C &
(A or C) and (B or C) are_interchangeable.
distrib(6): (A and B) or C &
(C or A) and (C or B) are_interchangeable.
distrib(7): C or (A and B) &
(C or A) and (C or B) are_interchangeable.
distrib(8): C or (A and B) &
(A or C) and (B or C) are_interchangeable.
distrib(9): (A or B) and C &
(A and C) or (B and C) are_interchangeable.
distrib(10): (A or B) and C &
(C and A) or (C and B) are_interchangeable.
distrib(11): C and (A or B) &
(C and A) or (C and B) are_interchangeable.
distrib(12): C and (A or B) &
(A and C) or (B and C) are_interchangeable.
/*** Other handy logical equivalences (DeMorgan, etc.) ***/
logical(1): not (A or B) &
(not A) and (not B) are_interchangeable.
logical(2): not (A and B) &
(not A) or (not B) are_interchangeable.
logical(3): A -> B &
(not A) or B are_interchangeable.
logical(4): A <-> B &
(A -> B) and (B -> A) are_interchangeable.
logical(5): A -> (B -> C)
may_be_replaced_by (A and B) -> C.
/*----------------------------------------------------------------------------*
| % % %%%% %%%% % % % %%% %%%% |
| %% %% % % % % % % % % % % % COPYRIGHT (C) 2001-2005 |
| % % % % % % % % % % % % % % Praxis HIS Limited |
| % % % % % % % % % %%%%% %%%% Bath, UK. |
| % % % % % % % % % % % % % |
| % % % % % % % % % % % % % |
| % % %%%% %%%% %%%% %%%%% % % % % |
*----------------------------------------------------------------------------*
MODULAR.RUL -- $Id: MODULAR.RUL,v 1.4 2005/11/16 14:55:27 spark Exp $
*----------------------------------------------------------------------------*
| This rulefile is for use with the SPADE Proof Checker in conjunction with |
| VC files generated by the SPARK Examiner v6.0 or later |
*----------------------------------------------------------------------------*
| RULE FAMILIES CONTAINED HEREIN :- |
| modular : modular arithmetic |
*----------------------------------------------------------------------------*
| MODEL DECLARATIONS FOR THIS FILE :- |
| |
| rule_family modular: |
| X mod Y requires [X : i, Y : i] & |
| X <= Y requires [X : i, Y : i] & |
| X <> Y requires [X : i, Y : i] & |
| X < Y requires [X : i, Y : i] & |
| X = Y requires [X : i, Y : i]. |
*----------------------------------------------------------------------------*/
/*** Definition of mod (modulo) ***/
modular(1): X mod Y = X - N * Y may_be_deduced_from
[ N * Y <= X, X < (N + 1)* Y, 0 < Y ].
modular(2): X mod Y = X - N * Y may_be_deduced_from
[ X <= N * Y, (N + 1) * Y < X, Y < 0 ].
/*** Bounds for 0 < Y ***/
modular(10): 0 <= (X * Y + Z) mod Y may_be_deduced_from [ 0 <= Z, Z < Y ].
modular(11): (X * Y + Z) mod Y < Y may_be_deduced_from [ 0 <= Z, Z < Y ].
/*** Bounds for Y < 0 ***/
modular(20): Y < (X * Y + Z) mod Y may_be_deduced_from [ Y < Z, Z <= 0 ].
modular(21): (X * Y + Z) mod Y <= 0 may_be_deduced_from [ Y < Z, Z <= 0 ].
/** Properties ***/
modular(30): (X * Y + Z) mod Y = Z may_be_deduced_from [ 0 <= Z, Z < Y ].
modular(31): (X * Y + Z) mod Y = Z may_be_deduced_from [ Z <= 0, Y < Z ].
modular(32): N mod N may_be_replaced_by 0 if [ N <> 0 ].
modular(33): N mod N may_be_replaced_by 0 if [ N > 0 ].
modular(34): N mod N may_be_replaced_by 0 if [ N < 0 ].
modular(40): X * Y mod Y may_be_replaced_by 0 if [ Y <> 0 ].
modular(41): X mod Y may_be_replaced_by X if [ 0 <= X, X < Y ].
modular(42): X mod Y may_be_replaced_by X if [ Y < X, X <= 0 ].
modular(50): X mod Y mod Z = X mod Y may_be_deduced_from
[ 0 <= B, B < Y, Y <= Z, X = A*Y + B ].
modular(51): X mod Y mod Z = X mod Y may_be_deduced_from
[ Z <= Y, Y < B, B <= 0, X = A*Y + B ].
modular(52): X mod Y mod Z = X mod Z may_be_deduced_from
[ X = A * Y + B, B = C * Z + D, Y = Z * E,
0 <= B, B < Y, 0 <= D, D < Z ].
modular(53): X mod Y mod Z = X mod Z may_be_deduced_from
[ X = A * Y + B, B = C * Z + D, Y = Z * E,
0 <= B, B < Y, D <= 0, Z < D ].
modular(54): X mod Y mod Z = X mod Z may_be_deduced_from
[ X = A * Y + B, B = C * Z + D, Y = Z * E,
B <= 0, Y < B, 0 <= D, D < Z ].
modular(55): X mod Y mod Z = X mod Z may_be_deduced_from
[ X = A * Y + B, B = C * Z + D, Y = Z * E,
B <= 0, Y < B, D <= 0, Z < 0 ].
modular(60): X mod Y = -((-X) mod (-Y)) may_be_deduced_from
[ 0 <= B, B < Y, X = A * Y + B ].
modular(61): X mod Y = -((-X) mod (-Y)) may_be_deduced_from
[ Y < B, B <= 0, X = A * Y + B ].
/*---------------------------------------------------------------------------*
| %%% % % % % % %%%%% %%% %%%%% |
| % % % % % % % % % % % COPYPRIGHT (C) 1988,1991 |
| % % % % % % %% % % % % Program Validation Ltd., |
| % % % % % % % % % % % %%% 26, Queen’s Terrace, |
| % % % % % %%%%% % %% % % % Southampton SO1 1BQ, |
| % % % % % % % % % % % England. |
| %% % %%% % % % % % %%% % |
*----------------------------------------------------------------------------*
| SPADE$CHECKER:QUANTIF.RUL |
| Version 1.2, released January 1991 |
*----------------------------------------------------------------------------*
| This rulefile is for use with the SPADE Proof Checker. |
*----------------------------------------------------------------------------*
| RULE FAMILY CONTAINED HEREIN :- |
| quant : rules for quantified expressions |
*----------------------------------------------------------------------------*
| MODEL DECLARATION FOR THIS FILE :- |
| |
| rule_family quant: |
| for_all(X, Y) requires [ X:any, Y:any ] & |
| not X requires [ X:any ] & |
| for_some(X, Y) requires [ X:any, Y:any ] & |
| X or Y requires [ X:any, Y:any ]. |
*---------------------------------------------------------------------------*/
/*** COMMON QUANTIFICATION TECHNIQUES ***/
/*** Rewriting of quantified terms ***/
quant(1): for_all(X,Y) & (not for_some(X,not Y)) are_interchangeable.
quant(2): for_all(X,not Y) & (not for_some(X,Y)) are_interchangeable.
quant(3): for_some(X,Y) & (not for_all(X,not Y)) are_interchangeable.
quant(4): for_some(X,not Y) & (not for_all(X,Y)) are_interchangeable.
quant(5): for_all(X,for_all(Y,P)) & for_all(Y,for_all(X,P))
are_interchangeable.
quant(6): for_some(X,for_some(Y,P)) & for_some(Y,for_some(X,P))
are_interchangeable.
quant(7): for_some(Y,for_all(X,P)) may_be_replaced_by
for_all(X,for_some(Y,P)).
/*** Simple inferences ***/
quant(8): for_some(X,P) may_be_deduced_from [ for_all(X,P) ].
/*** Inferences involving ‘AND’ ***/
quant(9): for_all(X,A) may_be_deduced_from [ for_all(X,A and B) ].
quant(10): for_all(X,B) may_be_deduced_from [ for_all(X,A and B) ].
quant(11): for_all(X,A and B) may_be_deduced_from
[ for_all(X,A), for_all(X,B) ].
quant(12): for_some(X,A) may_be_deduced_from [ for_some(X,A and B) ].
quant(13): for_some(X,B) may_be_deduced_from [ for_some(X,A and B) ].
/*** Inferences involving ‘OR’ ***/
quant(14): for_some(X,A or B) may_be_deduced_from [ for_some(X,A) ].
quant(15): for_some(X,A or B) may_be_deduced_from [ for_some(X,B) ].
quant(16): for_some(X,A) or for_some(X,B) may_be_deduced_from
[ for_some(X,A or B) ].
quant(17): for_all(X,A or B) may_be_deduced_from [ for_all(X,A) ].
quant(18): for_all(X,A or B) may_be_deduced_from [ for_all(X,B) ].
/*** Inferences involving ‘->’ ***/
quant(19): for_some(X,A -> B) may_be_deduced_from [ for_some(X,not A) ].
quant(20): for_some(X,A -> B) may_be_deduced_from [ for_some(X,B) ].
quant(21): for_some(X,not A) or for_some(X,B) may_be_deduced_from
[ for_some(X,A -> B) ].
quant(22): for_all(X,A -> B) may_be_deduced_from [ for_all(X,not A) ].
quant(23): for_all(X,A -> B) may_be_deduced_from [ for_all(X,B) ].
/*** Inferences involving ‘<->’ ***/
quant(24): for_all(X,A -> B) may_be_deduced_from [ for_all(X,A <-> B) ].
quant(25): for_all(X,B -> A) may_be_deduced_from [ for_all(X,A <-> B) ].
quant(26): for_all(X,A <-> B) may_be_deduced_from
[ for_all(X,A -> B), for_all(X,B -> A) ].
quant(27): for_some(X,A -> B) may_be_deduced_from [ for_some(X,A <-> B) ].
quant(28): for_some(X,B -> A) may_be_deduced_from [ for_some(X,A <-> B) ].
/*----------------------------------------------------------------------------*
* $Id: RECORD.RUL,v 1.2 2005/07/01 15:11:28 spark Exp $
*----------------------------------------------------------------------------*
| This rulefile is for use with the SPADE Proof Checker. |
*----------------------------------------------------------------------------*
| RULE FAMILIES CONTAINED HEREIN :- |
| record : record-type simplification rules |
| record_equality : equality of two record-type objects |
| mk__record : rules specific to SPARK record aggregates |
*----------------------------------------------------------------------------*
| MODEL DECLARATIONS FOR THIS FILE :- |
| |
| rule_family record: |
| X requires [ X:any ]. |
| |
| rule_family record_equality: |
| X=Y requires [ X:any, Y:any ]. |
| |
| rule_family mk__record: |
| X requires [ X:any ]. |
*----------------------------------------------------------------------------*/
/*** RECORD SIMPLIFICATION rules ***/
/* record(1): fld_F(upf_F(_, VALUE)) may_be_replaced_by VALUE. */
RECORD1: FLD may_be_replaced_by VALUE if
[ goal(nonvar(RECORD1)),
goal(RECORD1=record(1)),
goal(record_function(_, FLD, access, F, [RECORD], TYPE)),
goal(record_function(_, RECORD, update, F, [_, VALUE], TYPE)) ].
/* record(2): upf_F(REC, fld_F(REC)) may_be_replaced_by REC. */
RECORD2: UPF may_be_replaced_by REC if
[ goal(nonvar(RECORD2)),
goal(RECORD2=record(2)),
goal(record_function(_, UPF, update, F, [REC, VALUE], TYPE)),
goal(record_function(_, VALUE, access, F, [REC], TYPE)) ].
/* record(3): upf_F(upf_G(R,VG),VF) may_be_replaced_by upf_G(upf_F(R,VF),VG) if [ "F" <> "G" ]. */
RECORD3: UPF_F may_be_replaced_by UPF_G if
[ goal(nonvar(RECORD3)),
goal(RECORD3=record(3)),
goal(record_function(_, UPF_F, update, F, [REC1, VF], TYPE)),
goal(record_function(_, REC1, update, G, [R, VG], TYPE)),
goal(F \= G),
goal(record_function(_, REC2, update, F, [R, VF], TYPE)),
goal(record_function(_, UPF_G, update, G, [REC2, VG], TYPE)) ].
/* record(4): fld_F(upf_G(R, V)) may_be_replaced_by fld_F(R) if [ "F" <> "G" ]. */
RECORD4: FLD_F_UPF_G may_be_replaced_by FLD_F_R if
[ goal(nonvar(RECORD4)),
goal(RECORD4=record(4)),
goal(record_function(_, FLD_F_UPF_G, access, F, [UPF_G], TYPE)),
goal(record_function(_, UPF_G, update, G, [R, V], TYPE)),
goal(F \= G),
goal(record_function(_, FLD_F_R, access, F, [R], TYPE)) ].
/* record(5): upf_F(upf_F(R, _), V) may_be_replaced_by upf_F(R, V). */
RECORD5: UPF_F_UPF_F_R may_be_replaced_by UPF_F_R if
[ goal(nonvar(RECORD5)),
goal(RECORD5=record(5)),
goal(record_function(_, UPF_F_UPF_F_R, update, F, [UPF_F, V], TYPE)),
goal(record_function(_, UPF_F, update, F, [R, _], TYPE)),
goal(record_function(_, UPF_F_R, update, F, [R, V], TYPE)) ].
/*** RECORD EQUALITY RULES ***/
/* record_equality(1): {for records with ONE field}
R=S may_be_deduced_from [ fld_F1(R)=fld_F1(S) ]. */
RECORD_EQUALITY1:
R = S may_be_deduced_from
[ goal(nonvar(RECORD_EQUALITY1)),
goal(RECORD_EQUALITY1=record_equality(1)),
goal(checktype(R,RECORD_TYPE)),
goal(type(RECORD_TYPE, record([[F1,_]]))),
goal(checktype(S,RECORD_TYPE)),
goal(record_function(_, R1, access, F1, [R], RECORD_TYPE)),
goal(record_function(_, S1, access, F1, [S], RECORD_TYPE)),
R1 = S1 ].
/* record_equality(2): {for records with TWO fields}
R=S may_be_deduced_from [ fld_F1(R)=fld_F1(S), fld_F2(R)=fld_F2(S) ]. */
RECORD_EQUALITY2:
R = S may_be_deduced_from
[ goal(nonvar(RECORD_EQUALITY2)),
goal(RECORD_EQUALITY2=record_equality(2)),
goal(checktype(R,RECORD_TYPE)),
goal(type(RECORD_TYPE, record([[F1,_],[F2,_]]))),
goal(checktype(S,RECORD_TYPE)),
goal(record_function(_, R1, access, F1, [R], RECORD_TYPE)),
goal(record_function(_, S1, access, F1, [S], RECORD_TYPE)),
goal(record_function(_, R2, access, F2, [R], RECORD_TYPE)),
goal(record_function(_, S2, access, F2, [S], RECORD_TYPE)),
R1 = S1, R2 = S2 ].
/* record_equality(3): {for records with THREE fields}
R=S may_be_deduced_from
[ fld_F1(R)=fld_F1(S), fld_F2(R)=fld_F2(S), fld_F3(R)=fld_F3(S) ]. */
RECORD_EQUALITY3:
R = S may_be_deduced_from
[ goal(nonvar(RECORD_EQUALITY3)),
goal(RECORD_EQUALITY3=record_equality(3)),
goal(checktype(R,RECORD_TYPE)),
goal(type(RECORD_TYPE, record([[F1,_],[F2,_],[F3,_]]))),
goal(checktype(S,RECORD_TYPE)),
goal(record_function(_, R1, access, F1, [R], RECORD_TYPE)),
goal(record_function(_, S1, access, F1, [S], RECORD_TYPE)),
goal(record_function(_, R2, access, F2, [R], RECORD_TYPE)),
goal(record_function(_, S2, access, F2, [S], RECORD_TYPE)),
goal(record_function(_, R3, access, F3, [R], RECORD_TYPE)),
goal(record_function(_, S3, access, F3, [S], RECORD_TYPE)),
R1 = S1, R2 = S2, R3 = S3 ].
/* record_equality(4): {for records with FOUR fields}
R=S may_be_deduced_from
[ fld_F1(R)=fld_F1(S), fld_F2(R)=fld_F2(S),
fld_F3(R)=fld_F3(S), fld_F4(R)=fld_F4(S) ]. */
RECORD_EQUALITY4:
R = S may_be_deduced_from
[ goal(nonvar(RECORD_EQUALITY4)),
goal(RECORD_EQUALITY4=record_equality(4)),
goal(checktype(R,RECORD_TYPE)),
goal(type(RECORD_TYPE,
record([[F1,_],[F2,_],[F3,_],[F4,_]]))),
goal(checktype(S,RECORD_TYPE)),
goal(record_function(_, R1, access, F1, [R], RECORD_TYPE)),
goal(record_function(_, S1, access, F1, [S], RECORD_TYPE)),
goal(record_function(_, R2, access, F2, [R], RECORD_TYPE)),
goal(record_function(_, S2, access, F2, [S], RECORD_TYPE)),
goal(record_function(_, R3, access, F3, [R], RECORD_TYPE)),
goal(record_function(_, S3, access, F3, [S], RECORD_TYPE)),
goal(record_function(_, R4, access, F4, [R], RECORD_TYPE)),
goal(record_function(_, S4, access, F4, [S], RECORD_TYPE)),
R1 = S1, R2 = S2, R3 = S3, R4 = S4 ].
/* record_equality(5): {for records with FIVE fields}
R=S may_be_deduced_from
[ fld_F1(R)=fld_F1(S), fld_F2(R)=fld_F2(S),
fld_F3(R)=fld_F3(S), fld_F4(R)=fld_F4(S),
fld_F5(R)=fld_F5(S) ]. */
RECORD_EQUALITY5:
R = S may_be_deduced_from
[ goal(nonvar(RECORD_EQUALITY5)),
goal(RECORD_EQUALITY5=record_equality(5)),
goal(checktype(R,RECORD_TYPE)),
goal(type(RECORD_TYPE,
record([[F1,_],[F2,_],[F3,_],[F4,_],[F5,_]]))),
goal(checktype(S,RECORD_TYPE)),
goal(record_function(_, R1, access, F1, [R], RECORD_TYPE)),
goal(record_function(_, S1, access, F1, [S], RECORD_TYPE)),
goal(record_function(_, R2, access, F2, [R], RECORD_TYPE)),
goal(record_function(_, S2, access, F2, [S], RECORD_TYPE)),
goal(record_function(_, R3, access, F3, [R], RECORD_TYPE)),
goal(record_function(_, S3, access, F3, [S], RECORD_TYPE)),
goal(record_function(_, R4, access, F4, [R], RECORD_TYPE)),
goal(record_function(_, S4, access, F4, [S], RECORD_TYPE)),
goal(record_function(_, R5, access, F5, [R], RECORD_TYPE)),
goal(record_function(_, S5, access, F5, [S], RECORD_TYPE)),
R1 = S1, R2 = S2, R3 = S3, R4 = S4, R5 = S5 ].
/* record_equality(6): {for records with SIX fields}
R=S may_be_deduced_from
[ fld_F1(R)=fld_F1(S), fld_F2(R)=fld_F2(S),
fld_F3(R)=fld_F3(S), fld_F4(R)=fld_F4(S),
fld_F5(R)=fld_F5(S), fld_F6(R)=fld_F6(S) ]. */
RECORD_EQUALITY6:
R = S may_be_deduced_from
[ goal(nonvar(RECORD_EQUALITY6)),
goal(RECORD_EQUALITY6=record_equality(6)),
goal(checktype(R,RECORD_TYPE)),
goal(type(RECORD_TYPE,
record([[F1,_],[F2,_],[F3,_],[F4,_],[F5,_],[F6,_]]))),
goal(checktype(S,RECORD_TYPE)),
goal(record_function(_, R1, access, F1, [R], RECORD_TYPE)),
goal(record_function(_, S1, access, F1, [S], RECORD_TYPE)),
goal(record_function(_, R2, access, F2, [R], RECORD_TYPE)),
goal(record_function(_, S2, access, F2, [S], RECORD_TYPE)),
goal(record_function(_, R3, access, F3, [R], RECORD_TYPE)),
goal(record_function(_, S3, access, F3, [S], RECORD_TYPE)),
goal(record_function(_, R4, access, F4, [R], RECORD_TYPE)),
goal(record_function(_, S4, access, F4, [S], RECORD_TYPE)),
goal(record_function(_, R5, access, F5, [R], RECORD_TYPE)),
goal(record_function(_, S5, access, F5, [S], RECORD_TYPE)),
goal(record_function(_, R6, access, F6, [R], RECORD_TYPE)),
goal(record_function(_, S6, access, F6, [S], RECORD_TYPE)),
R1 = S1, R2 = S2, R3 = S3, R4 = S4, R5 = S5, R6 = S6 ].
/* record_equality(7): {for records with SEVEN fields}
R=S may_be_deduced_from
[ fld_F1(R)=fld_F1(S), fld_F2(R)=fld_F2(S),
fld_F3(R)=fld_F3(S), fld_F4(R)=fld_F4(S),
fld_F5(R)=fld_F5(S), fld_F6(R)=fld_F6(S),
fld_F7(R)=fld_F7(S) ]. */
RECORD_EQUALITY7:
R = S may_be_deduced_from
[ goal(nonvar(RECORD_EQUALITY7)),
goal(RECORD_EQUALITY7=record_equality(7)),
goal(checktype(R,RECORD_TYPE)),
goal(type(RECORD_TYPE,
record([[F1,_],[F2,_],[F3,_],[F4,_],[F5,_],[F6,_],
[F7,_]]))),
goal(checktype(S,RECORD_TYPE)),
goal(record_function(_, R1, access, F1, [R], RECORD_TYPE)),
goal(record_function(_, S1, access, F1, [S], RECORD_TYPE)),
goal(record_function(_, R2, access, F2, [R], RECORD_TYPE)),
goal(record_function(_, S2, access, F2, [S], RECORD_TYPE)),
goal(record_function(_, R3, access, F3, [R], RECORD_TYPE)),
goal(record_function(_, S3, access, F3, [S], RECORD_TYPE)),
goal(record_function(_, R4, access, F4, [R], RECORD_TYPE)),
goal(record_function(_, S4, access, F4, [S], RECORD_TYPE)),
goal(record_function(_, R5, access, F5, [R], RECORD_TYPE)),
goal(record_function(_, S5, access, F5, [S], RECORD_TYPE)),
goal(record_function(_, R6, access, F6, [R], RECORD_TYPE)),
goal(record_function(_, S6, access, F6, [S], RECORD_TYPE)),
goal(record_function(_, R7, access, F7, [R], RECORD_TYPE)),
goal(record_function(_, S7, access, F7, [S], RECORD_TYPE)),
R1=S1, R2=S2, R3=S3, R4=S4, R5=S5, R6=S6, R7=S7 ].
/* record_equality(8): {for records with EIGHT fields}
R=S may_be_deduced_from
[ fld_F1(R)=fld_F1(S), fld_F2(R)=fld_F2(S),
fld_F3(R)=fld_F3(S), fld_F4(R)=fld_F4(S),
fld_F5(R)=fld_F5(S), fld_F6(R)=fld_F6(S),
fld_F7(R)=fld_F7(S), fld_F8(R)=fld_F8(S) ]. */
RECORD_EQUALITY8:
R = S may_be_deduced_from
[ goal(nonvar(RECORD_EQUALITY8)),
goal(RECORD_EQUALITY8=record_equality(8)),
goal(checktype(R,RECORD_TYPE)),
goal(type(RECORD_TYPE,
record([[F1,_],[F2,_],[F3,_],[F4,_],[F5,_],[F6,_],
[F7,_],[F8,_]]))),
goal(checktype(S,RECORD_TYPE)),
goal(record_function(_, R1, access, F1, [R], RECORD_TYPE)),
goal(record_function(_, S1, access, F1, [S], RECORD_TYPE)),
goal(record_function(_, R2, access, F2, [R], RECORD_TYPE)),
goal(record_function(_, S2, access, F2, [S], RECORD_TYPE)),
goal(record_function(_, R3, access, F3, [R], RECORD_TYPE)),
goal(record_function(_, S3, access, F3, [S], RECORD_TYPE)),
goal(record_function(_, R4, access, F4, [R], RECORD_TYPE)),
goal(record_function(_, S4, access, F4, [S], RECORD_TYPE)),
goal(record_function(_, R5, access, F5, [R], RECORD_TYPE)),
goal(record_function(_, S5, access, F5, [S], RECORD_TYPE)),
goal(record_function(_, R6, access, F6, [R], RECORD_TYPE)),
goal(record_function(_, S6, access, F6, [S], RECORD_TYPE)),
goal(record_function(_, R7, access, F7, [R], RECORD_TYPE)),
goal(record_function(_, S7, access, F7, [S], RECORD_TYPE)),
goal(record_function(_, R8, access, F8, [R], RECORD_TYPE)),
goal(record_function(_, S8, access, F8, [S], RECORD_TYPE)),
R1=S1, R2=S2, R3=S3, R4=S4, R5=S5, R6=S6, R7=S7, R8=S8 ].
/* record_equality(9): {for records with NINE fields}
R=S may_be_deduced_from
[ fld_F1(R)=fld_F1(S), fld_F2(R)=fld_F2(S),
fld_F3(R)=fld_F3(S), fld_F4(R)=fld_F4(S),
fld_F5(R)=fld_F5(S), fld_F6(R)=fld_F6(S),
fld_F7(R)=fld_F7(S), fld_F8(R)=fld_F8(S),
fld_F9(R)=fld_F9(S) ]. */
RECORD_EQUALITY9:
R = S may_be_deduced_from
[ goal(nonvar(RECORD_EQUALITY9)),
goal(RECORD_EQUALITY9=record_equality(9)),
goal(checktype(R,RECORD_TYPE)),
goal(type(RECORD_TYPE,
record([[F1,_],[F2,_],[F3,_],[F4,_],[F5,_],[F6,_],
[F7,_],[F8,_],[F9,_]]))),
goal(checktype(S,RECORD_TYPE)),
goal(record_function(_, R1, access, F1, [R], RECORD_TYPE)),
goal(record_function(_, S1, access, F1, [S], RECORD_TYPE)),
goal(record_function(_, R2, access, F2, [R], RECORD_TYPE)),
goal(record_function(_, S2, access, F2, [S], RECORD_TYPE)),
goal(record_function(_, R3, access, F3, [R], RECORD_TYPE)),
goal(record_function(_, S3, access, F3, [S], RECORD_TYPE)),
goal(record_function(_, R4, access, F4, [R], RECORD_TYPE)),
goal(record_function(_, S4, access, F4, [S], RECORD_TYPE)),
goal(record_function(_, R5, access, F5, [R], RECORD_TYPE)),
goal(record_function(_, S5, access, F5, [S], RECORD_TYPE)),
goal(record_function(_, R6, access, F6, [R], RECORD_TYPE)),
goal(record_function(_, S6, access, F6, [S], RECORD_TYPE)),
goal(record_function(_, R7, access, F7, [R], RECORD_TYPE)),
goal(record_function(_, S7, access, F7, [S], RECORD_TYPE)),
goal(record_function(_, R8, access, F8, [R], RECORD_TYPE)),
goal(record_function(_, S8, access, F8, [S], RECORD_TYPE)),
goal(record_function(_, R9, access, F9, [R], RECORD_TYPE)),
goal(record_function(_, S9, access, F9, [S], RECORD_TYPE)),
R1=S1, R2=S2, R3=S3, R4=S4, R5=S5, R6=S6, R7=S7, R8=S8,
R9=S9 ].
/* record_equality(10): {for records with TEN fields}
R=S may_be_deduced_from
[ fld_F1(R)=fld_F1(S), fld_F2(R)=fld_F2(S),
fld_F3(R)=fld_F3(S), fld_F4(R)=fld_F4(S),
fld_F5(R)=fld_F5(S), fld_F6(R)=fld_F6(S),
fld_F7(R)=fld_F7(S), fld_F8(R)=fld_F8(S),
fld_F9(R)=fld_F9(S), fld_F10(R)=fld_F10(S) ]. */
RECORD_EQUALITY10:
R = S may_be_deduced_from
[ goal(nonvar(RECORD_EQUALITY10)),
goal(RECORD_EQUALITY10=record_equality(10)),
goal(checktype(R,RECORD_TYPE)),
goal(type(RECORD_TYPE,
record([[F1,_],[F2,_],[F3,_],[F4,_],[F5,_],[F6,_],
[F7,_],[F8,_],[F9,_],[F10,_]]))),
goal(checktype(S,RECORD_TYPE)),
goal(record_function(_, R1, access, F1, [R], RECORD_TYPE)),
goal(record_function(_, S1, access, F1, [S], RECORD_TYPE)),
goal(record_function(_, R2, access, F2, [R], RECORD_TYPE)),
goal(record_function(_, S2, access, F2, [S], RECORD_TYPE)),
goal(record_function(_, R3, access, F3, [R], RECORD_TYPE)),
goal(record_function(_, S3, access, F3, [S], RECORD_TYPE)),
goal(record_function(_, R4, access, F4, [R], RECORD_TYPE)),
goal(record_function(_, S4, access, F4, [S], RECORD_TYPE)),
goal(record_function(_, R5, access, F5, [R], RECORD_TYPE)),
goal(record_function(_, S5, access, F5, [S], RECORD_TYPE)),
goal(record_function(_, R6, access, F6, [R], RECORD_TYPE)),
goal(record_function(_, S6, access, F6, [S], RECORD_TYPE)),
goal(record_function(_, R7, access, F7, [R], RECORD_TYPE)),
goal(record_function(_, S7, access, F7, [S], RECORD_TYPE)),
goal(record_function(_, R8, access, F8, [R], RECORD_TYPE)),
goal(record_function(_, S8, access, F8, [S], RECORD_TYPE)),
goal(record_function(_, R9, access, F9, [R], RECORD_TYPE)),
goal(record_function(_, S9, access, F9, [S], RECORD_TYPE)),
goal(record_function(_, R10, access, F10, [R], RECORD_TYPE)),
goal(record_function(_, S10, access, F10, [S], RECORD_TYPE)),
R1=S1, R2=S2, R3=S3, R4=S4, R5=S5, R6=S6, R7=S7, R8=S8,
R9=S9, R10=S10 ].
/* record_equality(11): {for records with ELEVEN or more fields}
R=S may_be_deduced_from
[ fld_F1(R)=fld_F1(S), fld_F2(R)=fld_F2(S),
fld_F3(R)=fld_F3(S), fld_F4(R)=fld_F4(S),
fld_F5(R)=fld_F5(S), fld_F6(R)=fld_F6(S),
fld_F7(R)=fld_F7(S), fld_F8(R)=fld_F8(S),
fld_F9(R)=fld_F9(S), fld_F10(R)=fld_F10(S), ... ]. */
RECORD_EQUALITY11:
R = S may_be_deduced_from
[ goal(nonvar(RECORD_EQUALITY11)),
goal(RECORD_EQUALITY11=record_equality(11)),
goal(checktype(R,RECORD_TYPE)),
goal(type(RECORD_TYPE,record(FIELD_LIST))),
goal(length(FIELD_LIST, NO_OF_FIELDS)),
goal(NO_OF_FIELDS > 10),
goal(checktype(S,RECORD_TYPE)),
goal(make_record_equality_goal(FIELD_LIST,R,S,GOAL)),
GOAL ].
/* mk__record(1):
fld_FIELD(mk__record(LARGS...(FIELD := VALUE)...))
may_be_replaced_by VALUE if
[ \+ ((FIELD := ...) is_in LARGS),
\+ ((FIELD := ...) is_in RARGS) ].
N.B.: Side conditions check uniqueness of assignment to FIELD. */
MK__RECORD1:
FLD_FIELD_MK__RECORD_LARGS_FIELD_VALUE_RARGS may_be_replaced_by VALUE if
[ goal(nonvar(MK__RECORD1)),
goal(MK__RECORD1 = mk__record(1)),
goal(record_function(_,
FLD_FIELD_MK__RECORD_LARGS_FIELD_VALUE_RARGS,
access, FIELD, [MK__RECORD_LARGS_FIELD_VALUE_RARGS], _)),
goal(nonvar(MK__RECORD_LARGS_FIELD_VALUE_RARGS)),
goal(MK__RECORD_LARGS_FIELD_VALUE_RARGS =..
[mk__record|LARGS_FIELD_VALUE_RARGS]),
goal(append(LARGS, [(FIELD := VALUE)|RARGS],
LARGS_FIELD_VALUE_RARGS)),
goal(\+ is_in((FIELD := _), LARGS)),
goal(\+ is_in((FIELD := _), RARGS)) ].
/* mk__record(2):
upf_FIELD(mk__record(LARGS...(FIELD := OLDVAL)...RARGS), NEWVAL)
may_be_replaced_by
mk__record(LARGS...(FIELD := NEWVAL)...RARGS) if
[ \+ ((FIELD := ...) is_in LARGS),
\+ ((FIELD := ...) is_in RARGS) ].
N.B.: Side conditions check uniqueness of assignment to FIELD. */
MK__RECORD2:
UPF_FIELD_MK__RECORD_LARGS_FIELD_OLDVAL_RARGS_NEWVAL
may_be_replaced_by
MK__RECORD_LARGS_FIELD_NEWVAL_RARGS if
[ goal(nonvar(MK__RECORD2)),
goal(MK__RECORD2 = mk__record(2)),
goal(record_function(_,
UPF_FIELD_MK__RECORD_LARGS_FIELD_OLDVAL_RARGS_NEWVAL,
update, FIELD,
[MK__RECORD_LARGS_FIELD_OLDVAL_RARGS, NEWVAL], _)),
goal(nonvar(MK__RECORD_LARGS_FIELD_OLDVAL_RARGS)),
goal(MK__RECORD_LARGS_FIELD_OLDVAL_RARGS =..
[mk__record|LARGS_FIELD_OLDVAL_RARGS]),
goal(append(LARGS, [(FIELD := OLDVAL)|RARGS],
LARGS_FIELD_OLDVAL_RARGS)),
goal(\+ is_in((FIELD := _), LARGS)),
goal(\+ is_in((FIELD := _), RARGS)),
goal(append(LARGS, [(FIELD := NEWVAL)|RARGS],
LARGS_FIELD_NEWVAL_RARGS)),
goal(MK__RECORD_LARGS_FIELD_NEWVAL_RARGS =..
[mk__record|LARGS_FIELD_NEWVAL_RARGS]) ].
/* mk__record(3):
fld_FIELD(mk__RECORDTYPE(LARGS...(FIELD := VALUE)...))
may_be_replaced_by VALUE if
[ \+ ((FIELD := ...) is_in LARGS),
\+ ((FIELD := ...) is_in RARGS) ].
N.B.: Side conditions check uniqueness of assignment to FIELD. */
MK__RECORD3:
FLD_FIELD_MK__RECORD_LARGS_FIELD_VALUE_RARGS may_be_replaced_by VALUE if
[ goal(nonvar(MK__RECORD3)),
goal(MK__RECORD3 = mk__record(3)),
goal(record_function(_,
FLD_FIELD_MK__RECORD_LARGS_FIELD_VALUE_RARGS,
access, FIELD, [MK__RECORD_LARGS_FIELD_VALUE_RARGS], _)),
goal(nonvar(MK__RECORD_LARGS_FIELD_VALUE_RARGS)),
goal(MK__RECORD_LARGS_FIELD_VALUE_RARGS =..
[MK__RECORDTYPE|LARGS_FIELD_VALUE_RARGS]),
goal(mk__function_name(MK__RECORDTYPE, _, record)),
goal(append(LARGS, [(FIELD := VALUE)|RARGS],
LARGS_FIELD_VALUE_RARGS)),
goal(\+ is_in((FIELD := _), LARGS)),
goal(\+ is_in((FIELD := _), RARGS)) ].
/* mk__record(4):
upf_FIELD(mk__RECORDTYPE(LARGS...(FIELD := OLDVAL)...RARGS), NEWVAL)
may_be_replaced_by
mk__RECORDTYPE(LARGS...(FIELD := NEWVAL)...RARGS) if
[ \+ ((FIELD := ...) is_in LARGS),
\+ ((FIELD := ...) is_in RARGS) ].
N.B.: Side conditions check uniqueness of assignment to FIELD. */
MK__RECORD4:
UPF_FIELD_MK__RECORD_LARGS_FIELD_OLDVAL_RARGS_NEWVAL
may_be_replaced_by
MK__RECORD_LARGS_FIELD_NEWVAL_RARGS if
[ goal(nonvar(MK__RECORD4)),
goal(MK__RECORD4 = mk__record(4)),
goal(record_function(_,
UPF_FIELD_MK__RECORD_LARGS_FIELD_OLDVAL_RARGS_NEWVAL,
update, FIELD,
[MK__RECORD_LARGS_FIELD_OLDVAL_RARGS, NEWVAL], _)),
goal(nonvar(MK__RECORD_LARGS_FIELD_OLDVAL_RARGS)),
goal(MK__RECORD_LARGS_FIELD_OLDVAL_RARGS =..
[MK__RECORDTYPE|LARGS_FIELD_OLDVAL_RARGS]),
goal(mk__function_name(MK__RECORDTYPE, _, record)),
goal(append(LARGS, [(FIELD := OLDVAL)|RARGS],
LARGS_FIELD_OLDVAL_RARGS)),
goal(\+ is_in((FIELD := _), LARGS)),
goal(\+ is_in((FIELD := _), RARGS)),
goal(append(LARGS, [(FIELD := NEWVAL)|RARGS],
LARGS_FIELD_NEWVAL_RARGS)),
goal(MK__RECORD_LARGS_FIELD_NEWVAL_RARGS =..
[MK__RECORDTYPE|LARGS_FIELD_NEWVAL_RARGS]) ].
/*---------------------------------------------------------------------------*
| %%% %%%%% %%% |
| % % % % % COPYPRIGHT (C) 1988,89,91 |
| % % % % Program Validation Ltd., |
| %%% %%% % % 26 Queen’s Terrace, |
| % % % % % Southampton SO1 1BQ, |
| % % % % % England. |
| %%% %%%%% %% % |
*----------------------------------------------------------------------------*
| SPADE$CHECKER:SEQ.RUL |
| Version 1.2, released January 1991 |
*----------------------------------------------------------------------------*
| This rulefile is for use with the SPADE Proof Checker. |
*----------------------------------------------------------------------------*
| RULE FAMILIES CONTAINED HEREIN :- |
| seqlen : properties of the length of sequence function |
| append : properties of the append operator |
| first : properties of the sequence function first |
| last : properties of the sequence function last |
| nonfirst : properties of the sequence function nonfirst |
| nonlast : properties of the sequence function nonlast |
| seq : equality properties of sequences |
*----------------------------------------------------------------------------*
| MODEL DECLARATIONS FOR THIS FILE :- |
| |
| rule_family seqlen: |
| X >= Y requires [ X:i, Y:i ] & |
| X > Y requires [ X:i, Y:i ] & |
| length(X) requires [ X:any ] & |
| X + Y requires [ X:i, Y:i ] & |
| X - Y requires [ X:i, Y:i ]. |
| |
| rule_family append: |
| X @ Y requires [ X:any, Y:any ]. |
| |
| rule_family first: |
| first(X) requires [ X:any ]. |
| |
| rule_family last: |
| last(X) requires [ X:any ]. |
| |
| rule_family nonfirst: |
| nonfirst(X) requires [ X:any ] & |
| X @ Y requires [ X:any, Y:any ]. |
| |
| rule_family nonlast: |
| nonlast(X) requires [ X:any ] & |
| [X|Y] requires [ X:any, Y:any ] & |
| X @ Y requires [ X:any, Y:any ]. |
| |
| rule_family seq: |
| X <-> Y requires [ X:any, Y:any ] & |
| X = Y requires [ X:any, Y:any ]. |
*---------------------------------------------------------------------------*/
/*** Sequence length rules ***/
seqlen(1): length(S)>=0 may_be_deduced.
seqlen(2): length([H|T])>0 may_be_deduced.
seqlen(3): length([H|T])>=1 may_be_deduced.
seqlen(4): length([]) may_be_replaced_by 0.
seqlen(5): length([H|T]) may_be_replaced_by N if
[ goal(length([H|T],N)) ].
seqlen(6): length(S @ T) & length(S)+length(T) are_interchangeable.
seqlen(7): length(S) & length(nonlast(S))+1 are_interchangeable if
[ S<>[] ].
seqlen(8): length(S) & length(nonlast(S))+1 are_interchangeable if
[ length(S)>=1 ].
seqlen(9): length(S)-1 & length(nonlast(S)) are_interchangeable if
[ S<>[] ].
seqlen(10): length(S)-1 & length(nonlast(S)) are_interchangeable if
[ length(S)>=1 ].
seqlen(11): length(S) & length(nonfirst(S))+1 are_interchangeable if
[ S<>[] ].
seqlen(12): length(S) & length(nonfirst(S))+1 are_interchangeable if
[ length(S)>=1 ].
seqlen(13): length(S)-1 & length(nonfirst(S)) are_interchangeable if
[ S<>[] ].
seqlen(14): length(S)-1 & length(nonfirst(S)) are_interchangeable if
[ length(S)>=1 ].
/*** Append rules ***/
append(1): ([] @ L) may_be_replaced_by L.
append(2): (L @ []) may_be_replaced_by L.
append(3): ([H1|T1] @ [H2|T2]) may_be_replaced_by L if
[ goal(append([H1|T1],[H2|T2],L)) ].
append(4): ([first(S)] @ nonfirst(S)) may_be_replaced_by S if [ S<>[] ].
append(5): (nonlast(S) @ [last(S)]) may_be_replaced_by S if [ S<>[] ].
append(6): ((X @ Y) @ Z) & (X @ (Y @ Z)) are_interchangeable.
/*** First rules ***/
first(1): first([H|T]) may_be_replaced_by H.
first(2): first([H|T] @ Y) may_be_replaced_by H.
first(3): first(X @ Y) & first(X) are_interchangeable if [ X<>[] ].
/*** Last rules ***/
last(1): last([H]) may_be_replaced_by H.
last(2): last(X @ [H|T]) may_be_replaced_by last([H|T]).
last(3): last([H|T]) & last(T) are_interchangeable if [ T<>[] ].
last(4): last(X @ Y) & last(Y) are_interchangeable if [ Y<>[] ].
/*** Nonfirst rules ***/
nonfirst(1): nonfirst([H|T]) may_be_replaced_by T.
nonfirst(2): nonfirst(T) may_be_replaced_by [] if [ length(T)=1 ].
nonfirst(3): nonfirst(X @ Y) & nonfirst(X) @ Y are_interchangeable if
[ X<>[] ].
nonfirst(4): nonfirst([H|T] @ Y) may_be_replaced_by T @ Y.
/*** Nonlast rules ***/
nonlast(1): nonlast([H]) may_be_replaced_by [].
nonlast(2): nonlast(T) may_be_replaced_by [] if [ length(T)=1 ].
nonlast(3): nonlast([H|T]) & [H|T1] are_interchangeable if
[ nonlast(T)=T1 ].
nonlast(4): nonlast(X @ Y) & X @ nonlast(Y) are_interchangeable if
[ Y<>[] ].
nonlast(5): nonlast(X @ [H]) may_be_replaced_by X.
/*** Sequence Equality rules ***/
seq(1): X = Y <-> ((first(X)=first(Y) and nonfirst(X)=nonfirst(Y))
or (X=[] and Y=[]))
may_be_deduced.
seq(2): X = Y may_be_deduced_from
[ first(X)=first(Y), nonfirst(X)=nonfirst(Y) ].
seq(3): X = Y <-> ((nonlast(X)=nonlast(Y) and last(X)=last(Y))
or (X=[] and Y=[]))
may_be_deduced.
seq(4): X = Y may_be_deduced_from
[ nonlast(X)=nonlast(Y), last(X)=last(Y) ].
/*---------------------------------------------------------------------------*
| %%% %%%%% %%%%% %%% |
| % % % % % % COPYPRIGHT (C) 1988,1991 |
| % % % % Program Validation Ltd., |
| %%% %%% % %%% 26, Queen’s Terrace, |
| % % % % Southampton SO1 1BQ, |
| % % % % % % England. |
| %%% %%%%% % %%% |
*----------------------------------------------------------------------------*
| SPADE$CHECKER:SETS.RUL |
| Version 1.2, released January 1991 |
*----------------------------------------------------------------------------*
| This rulefile is for use with the SPADE Proof Checker. |
*----------------------------------------------------------------------------*
| RULE FAMILY CONTAINED HEREIN :- |
| sets : properties of FDL set types |
*----------------------------------------------------------------------------*
| MODEL DECLARATION FOR THIS FILE :- |
| |
| rule_family sets: |
| X in Y requires [ X:any, Y:any ] & |
| X not_in Y requires [ X:any, Y:any ] & |
| not X requires [ X:any ] & |
| X \/ Y requires [ X:any, Y:any ] & |
| X /\ Y requires [ X:any, Y:any ] & |
| X \ Y requires [ X:any, Y:any ] & |
| X or Y requires [ X:any, Y:any ] & |
| X subset_of Y requires [ X:any, Y:any ] & |
| X strict_subset_of Y requires [ X:any, Y:any ]. |
*---------------------------------------------------------------------------*/
/*** Set rules ***/
/*** Element of ***/
sets(1): X in (set A) may_be_deduced_from [ goal(is_in(X,A)) ].
sets(2): (X not_in A) & (not (X in A)) are_interchangeable.
sets(3): (X in A) & (not (X not_in A)) are_interchangeable.
/*** Union ***/
sets(4): X in (A \/ B) may_be_deduced_from [ X in A ].
sets(5): X in (A \/ B) may_be_deduced_from [ X in B ].
sets(6): X not_in (A \/ B) may_be_deduced_from
[ X not_in A, X not_in B ].
sets(7): A \/ B may_be_replaced_by A if [ B subset_of A ].
sets(8): B \/ A may_be_replaced_by A if [ B subset_of A ].
sets(9): A \/ (set []) may_be_replaced_by A if [].
sets(10): (set []) \/ A may_be_replaced_by A if [].
sets(11): (set A) \/ (set B) may_be_replaced_by (set C) if
[ goal(set_union(A,B,C)) ].
/*** Intersection ***/
sets(12): X in (A /\ B) may_be_deduced_from [ X in A, X in B ].
sets(13): X not_in (A /\ B) may_be_deduced_from [ X not_in A ].
sets(14): X not_in (A /\ B) may_be_deduced_from [ X not_in B ].
sets(15): A /\ B may_be_replaced_by A if [ A subset_of B ].
sets(16): B /\ A may_be_replaced_by A if [ A subset_of B ].
sets(17): (set []) /\ B may_be_replaced_by (set []) if [].
sets(18): A /\ (set []) may_be_replaced_by (set []) if [].
sets(19): ((set A) /\ (set B)) may_be_replaced_by (set C) if
[ goal(set_intersect(A,B,C)) ].
/*** ‘Lacking’ ***/
sets(20): X in (A \ B) may_be_deduced_from [ X in A, X not_in B ].
sets(21): X not_in (A \ B) may_be_deduced_from [ X not_in A ].
sets(22): X not_in (A \ B) may_be_deduced_from [ X in B ].
sets(23): (A \ B) may_be_replaced_by A if [ B=(set []) ].
sets(24): (A \ B) may_be_replaced_by A if [ (A /\ B)=(set []) ].
sets(25): (A \ B) may_be_replaced_by A if [ (B /\ A)=(set []) ].
sets(26): (set A) \ (set B) may_be_replaced_by (set C) if
[ goal(set_lacking(A,B,C)) ].
sets(27): X=E or X in S may_be_deduced_from
[ X in (set U), goal(is_in(E,U),
set_lacking(U,[E],S)) ].
/*** Empty set ***/
sets(28): X not_in (set []) may_be_deduced.
/*** Subset rules ***/
sets(29): (set []) subset_of A may_be_deduced.
sets(30): A subset_of (A \/ B) may_be_deduced.
sets(31): A subset_of (B \/ A) may_be_deduced.
sets(32): (A /\ B) subset_of A may_be_deduced.
sets(33): (B /\ A) subset_of A may_be_deduced.
sets(34): (A \ B) subset_of A may_be_deduced.
sets(35): A subset_of B may_be_deduced_from [ A strict_subset_of B ].
sets(36): (set A) subset_of (set B) may_be_deduced_from
[ goal(subset(A,B)) ].
/*** Strict subset rule ***/
sets(37): A strict_subset_of B may_be_deduced_from
[ A subset_of B, A <> B ].
/*** Commutativity of /\, \/ ***/
sets(38): (X \/ Y) may_be_replaced_by (Y \/ X).
sets(39): (X /\ Y) may_be_replaced_by (Y /\ X).
/*** Associativity of /\, \/ ***/
sets(40): (X \/ (Y \/ Z)) & ((X \/ Y) \/ Z) are_interchangeable.
sets(41): (X /\ (Y /\ Z)) & ((X /\ Y) /\ Z) are_interchangeable.
/*** Distributivity of /\, \/ ***/
sets(42): (X /\ (Y \/ Z)) & ((X /\ Y) \/ (X /\ Z)) are_interchangeable.
sets(43): (X \/ (Y /\ Z)) & ((X \/ Y) /\ (X \/ Z)) are_interchangeable.
/*---------------------------------------------------------------------------*
| $Id: SPECIAL.RUL,v 1.2 2005/07/06 09:27:18 spark Exp $
| (C) Praxis High Integrity Systems
*----------------------------------------------------------------------------*
| This rulefile is for use with the SPADE Proof Checker. |
*----------------------------------------------------------------------------*
| RULE FAMILIES CONTAINED HEREIN :- |
| inference : simple inference rules (useful for subgoaling) |
| eq : equality substitution rule |
| equiv : equivalence substitution rule |
| simplify : simplification of expressions rule |
| logic : truth-table logic rules |
| standardisation : standardisation rules |
| unification : top-level unification rules |
*----------------------------------------------------------------------------*
| MODEL DECLARATIONS FOR THIS FILE :- |
| |
| rule_family inference: |
| X requires [ X:any ] & |
| X or Y requires [ X:any, Y:any ] & |
| X and Y requires [ X:any, Y:any ] & |
| X -> Y requires [ X:any, Y:any ] & |
| X <-> Y requires [ X:any, Y:any ]. |
| |
| rule_family eq: |
| X requires [ X:any ]. |
| |
| rule_family equiv: |
| X requires [ X:any ]. |
| |
| rule_family simplify: |
| X requires [ X:any ]. |
| |
| rule_family logic: |
| X requires [ X:any ]. |
| |
| rule_family standardisation: |
| X requires [ X:any ]. |
| |
| rule_family unification: |
| X requires [ X:any ]. |
*---------------------------------------------------------------------------*/
/*** Standard INFERENCE Rules ***/
inference(1): X may_be_deduced_from [ X ].
inference(2): X may_be_deduced_from [ Y -> X, Y ].
inference(3): X or Y may_be_deduced_from [ X ].
inference(4): X or Y may_be_deduced_from [ Y ].
inference(5): X and Y may_be_deduced_from [ X, Y ].
inference(6): X -> Y may_be_deduced_from [ not X ].
inference(7): X -> Y may_be_deduced_from [ Y ].
inference(8): X <-> Y may_be_deduced_from [ X -> Y, Y -> X ].
/*** SUBSTITUTION rule for equality-substitution ***/
eq(1): X may_be_replaced_by Y if [ X=Y, goal(X\=Y) ].
/*** SUBSTITUTION rule for equivalence-substitution ***/
EQUIV1: X may_be_replaced_by Y if
[ goal(nonvar(EQUIV1)),
goal(EQUIV1=equiv(1)),
X <-> Y,
goal(X\=Y) ].
/*** SIMPLIFY rule for simplification of expressions ***/
SIMPLIFY1: X may_be_replaced_by Y if
[ goal(nonvar(SIMPLIFY1)),
goal(SIMPLIFY1=simplify(1)),
goal(var(Y)),
goal(simplify(X, Y)),
goal(X \= Y) ].
SIMPLIFY2: X may_be_replaced_by Y if
[ goal(nonvar(SIMPLIFY2)),
goal(SIMPLIFY2=simplify(2)),
goal(novars(Y)),
goal(X \= Y),
goal(simplify(X, Z)),
goal(simplify(Y, Z)) ].
/*** LOGICAL DEDUCTION rule - only allowed by explicit call ***/
LOGIC1: X may_be_deduced_from
[ goal(nonvar(LOGIC1)),
goal(LOGIC1=logic(1)),
goal(try_deduce(X)) ].
LOGIC2: X may_be_replaced_by Y if
[ goal(nonvar(LOGIC2)),
goal(LOGIC2=logic(2)),
goal(novars(Y)),
goal(checktype(X,boolean)),
goal(try_deduce(X <-> Y)) ].
/*** STANDARDISATION rule - only allowed by explicit call ***/
STAND1: X may_be_replaced_by Y if
[ goal(nonvar(STAND1)),
goal(STAND1=standardisation(1)),
goal(novars(Y)),
goal(X\=Y),
goal(checktype(X,T)),
goal(norm_typed_expr(X,T,Z)),
goal(norm_typed_expr(Y,T,Z)) ].
STAND2: X may_be_replaced_by Y if
[ goal(nonvar(STAND2)),
goal(STAND2=standardisation(2)),
goal(var(Y)),
goal(checktype(X,T)),
goal(norm_typed_expr(X,T,Y)) ].
STAND3: X may_be_deduced_from
[ goal(nonvar(STAND3)),
goal(STAND3=standardisation(3)),
goal(norm_typed_expr(X,boolean,true)) ].
/*** UNIFICATION rules - only allowed by explicit call ***/
/* This rule family allows f(x1,...,xn)=f(y1,...,yn) to be deduced from
x1=y1, ..., xn=yn (for n in 1..9). unification(n) is for the case when
f takes n arguments. For any n, you can survive without these rules if
you wish: simply prove f(x1,...,xn)=f(y1,...,yn) by contradiction, then
establish contradiction by replacing each yi by xi (or vice versa), thereby
gaining the hypothesis f(x1,...,xn)<>f(x1,...,xn), which gives false. */
UNIF1: X = Y may_be_deduced_from
[ goal(nonvar(UNIF1)),
goal(UNIF1=unification(1)),
goal(X =.. [F|X1]),
goal(Y =.. [F|Y1]),
X1 = Y1 ].
UNIF2: X = Y may_be_deduced_from
[ goal(nonvar(UNIF2)),
goal(UNIF2=unification(2)),
goal(X =.. [F|X1,X2]),
goal(Y =.. [F|Y1,Y2]),
X1 = Y1, X2 = Y2 ].
UNIF3: X = Y may_be_deduced_from
[ goal(nonvar(UNIF3)),
goal(UNIF3=unification(3)),
goal(X =.. [F|X1,X2,X3]),
goal(Y =.. [F|Y1,Y2,Y3]),
X1 = Y1, X2 = Y2, X3 = Y3 ].
UNIF4: X = Y may_be_deduced_from
[ goal(nonvar(UNIF4)),
goal(UNIF4=unification(4)),
goal(X =.. [F|X1,X2,X3,X4]),
goal(Y =.. [F|Y1,Y2,Y3,Y4]),
X1 = Y1, X2 = Y2, X3 = Y3, X4 = Y4 ].
UNIF5: X = Y may_be_deduced_from
[ goal(nonvar(UNIF5)),
goal(UNIF5=unification(5)),
goal(X =.. [F|X1,X2,X3,X4,X5]),
goal(Y =.. [F|Y1,Y2,Y3,Y4,Y5]),
X1 = Y1, X2 = Y2, X3 = Y3, X4 = Y4, X5 = Y5 ].
UNIF6: X = Y may_be_deduced_from
[ goal(nonvar(UNIF6)),
goal(UNIF6=unification(6)),
goal(X =.. [F|X1,X2,X3,X4,X5,X6]),
goal(Y =.. [F|Y1,Y2,Y3,Y4,Y5,Y6]),
X1 = Y1, X2 = Y2, X3 = Y3, X4 = Y4, X5 = Y5, X6 = Y6 ].
UNIF7: X = Y may_be_deduced_from
[ goal(nonvar(UNIF7)),
goal(UNIF7=unification(7)),
goal(X =.. [F|X1,X2,X3,X4,X5,X6,X7]),
goal(Y =.. [F|Y1,Y2,Y3,Y4,Y5,Y6,Y7]),
X1=Y1, X2=Y2, X3=Y3, X4=Y4, X5=Y5, X6=Y6, X7=Y7 ].
UNIF8: X = Y may_be_deduced_from
[ goal(nonvar(UNIF8)),
goal(UNIF8=unification(8)),
goal(X =.. [F|X1,X2,X3,X4,X5,X6,X7,X8]),
goal(Y =.. [F|Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8]),
X1=Y1, X2=Y2, X3=Y3, X4=Y4, X5=Y5, X6=Y6, X7=Y7, X8=Y8 ].
UNIF9: X = Y may_be_deduced_from
[ goal(nonvar(UNIF9)),
goal(UNIF9=unification(9)),
goal(X =.. [F|X1,X2,X3,X4,X5,X6,X7,X8,X9]),
goal(Y =.. [F|Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9]),
X1=Y1,X2=Y2,X3=Y3,X4=Y4,X5=Y5,X6=Y6,X7=Y7,X8=Y8,X9=Y9 ].
The Checker supports two different types of rule, stored as databases of rules in a collection of rule files. The two types of rule are inference rules and substitution (or “rewrite”) rules. The inference rules allow the user to combine zero or more existing facts to infer new facts, while the replacement rules allow the user to replace a subexpression of the VC by an equivalent subexpression. Each type of rule has conditions associated with it which must hold if the rule is to be applicable: in the former case, these conditions are the facts to be combined, whereas in the latter case they are facts which must hold to ensure the equivalence is true, e.g. (A and B) may be replaced by A if the condition B=true is satisfied, so B=true is a (sufficient, but not necessary) condition for the equivalence to hold. Some of the facts (or conditions), for either type of rule, may be “meta-logical” in that they refer to type-checking constraints or other external conditions. Before we consider in greater detail the conditions which may be applied, we first turn our attention to the syntax of each type of rule in turn.
Please note that, in the following sections, the metalanguage used is a modification of Backus-Naur form employed in BS 6192: 1982 and outlined in chapter 2 of the SPADE FDL Manual.
Inference rules allow existing facts (i.e. hypotheses, their immediate consequences, trivial truths such as 2+1=3 and other immediate constraints) to be combined to infer new facts, which may then be added to the VC as new hypotheses. The general syntax of an inference rule is:
inference-rule = rulename “:” formula conditional-part.
where
conditional-part = “may_be_deduced_from” list-of- conditions
| “may_be_deduced”
rulename = family-name”(“ specific-rule-number “)”
family-name = prolog-atom
specific-rule-number = non-negative-integer
formula = well-formed-prolog-expression
list-of-conditions = “[” “]” | “[” condition { “,” condition } “]”
condition = ordinary-condition | immediate-condition
ordinary-condition = well-formed-prolog-expression
immediate-condition = “goal(“ well-formed- expression “)”
We discuss the list of conditions in section 5.3. The rulename, the syntax of which is the same for substitution rules also, allows the user to select a family of possible rules or an individual member of a family of rules or a range of elements of a family of rules when attempting to apply a rule. The names selected for user-defined rules should be chosen as convenient, but it is preferable to avoid using the names used in the built-in rules databases; these are listed and described in chapters 2 and 3.
The formula, as a well-formed Prolog expression, may contain Prolog variables; indeed, this is the norm: a rule without Prolog variables is rare, and is only used in practice to carry across relationships which must hold between program constants, e.g. that maxchars =< maxlen, where both are declared as “constants” in the FDL text and so do not change. By adding such rules about the relationships between program constants, we can declare properties which we require to hold for the eventual program, regardless of the actual values eventually chosen for these constants.
Returning to the use of Prolog variables in rules: they allow the rule to express a general property, and the rule is used by instantiating the Prolog variables to specific values. For example, the (hypothetical) inference rule
logic(1): A or B may_be_deduced_from [ B ].
may be used to infer (a>1 or b=2) from the fact that b=2. The Checker requires that all Prolog variables in the formula to be inferred be fully instantiated if the rule application is to succeed, so no Prolog variables may be introduced into a VC via the use of the rules databases. (N.B. The above rule is present in the built-in rules as inference(4) in SPECIAL.RUL.)
Substitution rules allow one subexpression of a VC to be replaced by another, equivalent, expression. There are two types of substitution rule: one-way and two-way rules. Their general syntax is described below, with the definition of the rulename and condition-list parts as for inference rules, described in the previous section.
replacement-rule = rulename “:” one-way-rule “.” | rulename “:” two-way-rule “.”
one-way-rule = expression “may_be_replaced_by” expression [ “if” list-of-conditions ]
two-way-rule = expression “&” expression “are_interchangeable”
[ “if” list-of-conditions ]
where
expression = well-formed-prolog-expression
As one would expect, one-way rules allow substitution one way round, whereas two-way rules allow interchange either way. Thus, the rules
subst(1): Amay_be_replaced_byBif[C1,C2, ...,Cn].
and
subst(2): A&Bare_interchangeableif[C1,C2, ...,Cn].
both allow A to be replaced by B provided the conditions [C1,...,Cn] are met; but only subst(2) allows us to substitute the other way, i.e. replacing B by A instead. One-way rules can be useful in preventing extra work for the Checker in symmetric rules and in directing the flow of substitutions to move towards greater simplicity. For example, the built-in rule
commut(1): A+B may_be_replaced_by B+A.
is best expressed this way, as the two-way version of this rule says the same thing twice, and would consequently cause the Checker possibly to find twice as many matches, making the rule search longer and slower. As an illustration of directing the flow of substitutions, consider the (hypothetical) rule
zero(1): A+0 may_be_replaced_by A.
(N.B. The above rule is present in the built-in rules, as arith(3).) It is imaginable that, in some circumstances, we may wish to replace A by A+0; however, in general the substitution will be the other way round, as suggested by the rule. In the rare event that we do wish to use the rule the other way round, we can still do so indirectly by inferring that A+0=A+0, then using rule zero(1) to replace one instance of A+0 in this by A to get A+0=A. We can then use equality substitution with this fact to replace A by A+0 in the desired place. Thus, one-way rules do not strictly affect the actual power of a proof rule, but merely suggest a particular common mode of use.
As with the inference rules, most substitution rules contain Prolog variables so that they express a general property, specific instantiations of which are used in applying such rules. To be used, a substitution rule also requires that both expressions (the expression to be replaced and the expression by which it is to be replaced) be fully instantiated, in line with a similar constraint on the use of inference rules. The list of conditions, both for substitution rules and for inference rules, are discussed in the next section.
The list of conditions associated with a rule is a list of zero or more Prolog expressions, each of which must be “satisfied” before the rule may be fully used. In the case of inference rules, if some, but not all of the conditions are satisfied, the rule may be used to generate subgoals to be worked on, the satisfaction of all of which allows the rule to be used. Such subgoaling may only be used, however, when none of the unsatisfied conditions is an “immediate” condition, and when all of the unsatisfied conditions are fully instantiated. (Please note that subgoaling cannot at present be used with substitution rules, so inference rules can be preferable on occasion.)
The conditions in a condition list are of two kinds, and the kind of the condition determines how it is to be satisfied. The two kinds are known as ordinary conditions and immediate conditions. Ordinary conditions are simply conditions which must follow from the hypotheses of the VC and/or from simple facts (such as 2>1). The Checker has a built-in inference mechanism which attempts to satisfy such conditions, and the success or failure of the Checker in attempting to satisfy such a condition depends on the available hypotheses of the VC and the power of the inference mechanism; failure to satisfy an ordinary condition does not mean it is false: only that it may be, or that the Checker cannot infer it at present without further strengthening of the VC (e.g. by the user inferring intermediate useful hypotheses, for instance).
Immediate conditions are satisfied in a different way. They take the form
goal( CONDITION )
where CONDITION is a well-formed Prolog expression. A condition such as this succeeds if and only if CONDITION, submitted to the Prolog system as a goal with the built-in call(_) predicate, succeeds. Thus, such conditions may call built-in Prolog code to perform some checking, simplification or action. These immediate goals do not make any use of the Checker’s inference mechanisms, but call Prolog predicates directly. An example of such a goal is
eq(1): A may_be_replaced_by B if [ A=B, goal(A\=B) ].
which allows A to be replaced by B provided A=B can be inferred from the VC, but only if A and B are not identical structures: the direct call to the built-in \= predicate ensures (since A and B are fully instantiated by this point, as subgoal satisfaction proceeds from left to right through the list of conditions) that A and B are distinct structures. Without this additional immediate condition, the rule would allow us to substitute A for itself (a harmless, but pointless, substitution).
The next section lists the useful built-in predicates which may be used as immediate conditions in condition lists: no other predicates may be used apart from these, and an attempt to do so will result in a warning message when a rulefile containing an illegal predicate is read by the Checker and the Checker will then refuse to use this rule.
5.4 Permissible Immediate Condition Predicates
The following predicates may be used as immediate conditions in user-defined proof rules for use with the Proof Checker. As well as using them directly, we may also use them with the standard combinator predicates
“_ , _” (and)
“_ ; _” (or).
checktype(EXPRESSION, TYPE_IDENTIFIER)
This predicate may be used to check that an expression is of an appropriate type, e.g. checktype(A,integer) before allowing A to be replaced by A+0.
EXPR1 = EXPR2
This form of equality tests for exact unifiability, so it is much stricter than equality in an ordinary goal. For example, the ordinary goal
3+1=4
will succeed, but the immediate goal
goal(3+1=4)
will not, as 3+1 and 4 are different objects.
EXPR1 \= EXPR2
This predicate succeeds as long as EXPR1 and EXPR2 cannot be unified. It is thus convenient for ensuring that two objects are distinct.
integer(EXPRESSION)
This built-in Prolog predicate succeeds if and only if its argument is instantiated to an integer.
intexp(EXPRESSION)
This predicate succeeds if and only if its argument is an expression composed entirely of integers (not constant- and variable-identifiers of type integer) and the built-in operators +, - (unary and binary), *, div and mod.
simplify(INPUT_EXPR, OUTPUT_EXPR)
This predicate carries out some limited simplification on an expression. An example rule, using this and the previous predicate, is:
simpint(1): X>Y may_be_deduced_from
[ goal( intexp(X-Y), simplify(X>Y,true) ) ].
is_in(ELEMENT, LIST)
This predicate succeeds if ELEMENT is an element of list LIST. This predicate will not be resatisfied on backtracking.
length(LIST, LENGTH)
This built-in predicate returns the length of a well-formed list.
append(LIST1, LIST2, LIST3)
This predicate succeeds if LIST1 can be appended to the front of LIST2 to give LIST3. It cannot be resatisfied on backtracking, so it cannot be used to do the inverse, i.e. generate pairs of lists which join together to give the third.
enumeration_list(ELEMENT, LIST)
This predicate succeeds if ELEMENT is an atom which is a constant within an enumeration type in which case the list of enumeration constants of which it is a member is returned as LIST. It is again a “succeed once or not at all” predicate. An example of its use might be:
enum(3): succ(pred(X))=X may_be_deduced_from
[ goal(enumeration_list(X,L)),
goal(L\=[X|_]) ].
sublist(LIST1, LIST2)
This predicate succeeds if LIST1 is a sublist of LIST2; it is again a “succeed once or not at all” predicate. An example of its use might be:
enum(17): succ(Y) may_be_replaced_by X if
[ goal(enumeration_list(Y,L)),
goal(sublist([Y,X],L)) ].
last(LIST, ELEMENT)
Given a list LIST, last returns the last element of the list as ELEMENT (or checks that a given value for ELEMENT is indeed the last element of LIST). It can only succeed at most once. To illustrate its use:
enum(1): pred(succ(X))=X may_be_deduced_from
[ goal(enumeration_list(X,L)),
goal(not last(L,X)) ].
in_order(EL1, EL2, LIST)
Given a list LIST and two elements EL1 and EL2 of this list, in_order succeeds if and only if either EL1 precedes EL2 in LIST or EL1 and EL2 are equal, e.g.
enum(5): X <= Y may_be_deduced_from
[ goal(enumeration_list(X,L)),
goal(in_order(X,Y,L)) ].
genvar(ATOM, VARIABLE)
This predicate should be used when you wish to include quantified expressions within proof rules (see section 5.5 below). You should give a Prolog atom as the first argument, this being the “root” variable name, i.e. the variable name you wish to use as the bound variable of a quantified expression assuming it is o.k. to do so: if this variable is not a program identifier, the second argument, VARIABLE, is instantiated to it; if, however, the identifier is already in use, a new unique identifier based on the atom that you gave as first argument is generated to avoid any problems. Thus, for example, goal(genvar(i,I)) will return either I=i, or I=i1 or I=i2 etc.
5.5 Quantifiers In Proof Rules
If we wish to introduce a quantified expression via a proof rule, to ensure correctness we should use the immediate goal genvar(_,_) described in section 5.4 above to generate a new unique bound variable name so that we are certain that we are not accidentally binding any occurrences of existing variables by mistake. Thus, a rule such as
positive_array(1): all_positive(A) may_be_deduced_from
[ for_all(i:integer,
(1 <= i and i <= maxindex) ->
element(a, [i]) > 0) ].
should, for certain correctness (avoiding confusion with any program identifier i) be written as
positive_array(1): all_positive(A) may_be_deduced_from
[ goal(genvar(i,I)),
for_all(I:integer,
(1 <= I and I <= maxindex) ->
element(a, [I]) > 0) ].
Finally, in any rule file, it is necessary to declare each rule family and to provide a very basic declaration of the types of its arguments. The rule family declaration has the form
rule_family FAMILYNAME : EXPRN1 requires TYPES1 & ...
& EXPRNn requires TYPESn.
(for some n >= 1). Each different type of expression EXPRNi requires a clause in the rule family declaration. What are these EXPRNi? Well, for an inference rule, such as
some_rule(1): f(A1,A2,...,An) may_be_deduced_from
CONDITIONS.
f(X1,X2,...,Xn) (where each Xi is a different Prolog variable) is the most general form of the expression f(A1,A2,...,An), where each Ai may be a variable or other pattern. Substitution rules come in two varieties; for a one-way rule, such as
some_rule(2): f(A1,...,An) may_be_replaced_by
g(B1,...,Bm) if CONDITIONS.
the only expression we need worry about is f(A1,...,An). For a two-way rule, however, such as
some_rule(3): f(A1,...,An) & g(B1,...,Bm)
are_interchangeable if CONDITIONS.
we must address both f(X1,...,Xn) and g(Y1,...,Ym) (assuming f and g are different). Remember, in all these cases, we are only concerned with the main operator or function of the expression: for all of the rules
silly_rule(1): A+B = C+D may_be_deduced_from
[ A+B>=C+D, A+B<=C+D ].
silly_rule(2): A-B = C may_be_deduced_from
[ B=0, not A<>C ].
silly_rule(3): A = B*C may_be_deduced_from
[ B*C=A or X, not X ].
the “most general expression” with the same main operator (in this case, =) is X=Y. (Remember, we are only looking at the expression to be inferred or, for substitution rules, the expression(s) to be replaced.) Note that, if we have a substitution rule in which one of the expressions to be considered is a Prolog variable, e.g.
silly_rule(4):X+Y&Zare_interchangeableif[X+Y=Z].
we must give a declaration for it (in this case, Z requires [Z:ir] would be appropriate, since Z must be numeric to be equal to X+Y). Such variable declarations (i.e. where there is no main operator or function) should come at the end of your rule family declaration, otherwise they may make some of your other rules inaccessible. Preferably, you should try to isolate such rules in a separate, type-compatible family.
If a rule family contains substitution rules which we wish to be able to use with the infer command (with the use_subst_rules_for_equality flag set to on), we must ensure that an appropriate clause of the form
A = B requires [ A:x, B:x ]
where x is i, ir, e, ire or any as appropriate. Such a clause may already be present if there are also equality inference rules (or rules allowing expressions of the form A=B to be rewritten to something else), but if there are none, it must be included as otherwise the Proof Checker will not search this rule family for matches when asked to infer an equality. Thus, by inclusion (or exclusion) of such a clause, one can affect whether substitution rules within a rule family may be used for equality inferences when the use_subst_rules_for_equality flag is on.
Finally, also note that, in the case of constants, we still have an expression, i.e. from
const_rule(1): max_index may_be_replaced_by 100.
const_rule(2): upper_bound & 200 are_interchangeable.
we get three expressions (max_index, upper_bound and 200: not 100, as the first rule is one-way only), each of which is its own “most general expression”.
To declare a rule family, we must first determine the collection of all such most general expressions. Each will have N Prolog variables in it, where N is the “arity” of the main operator or function. (The “arity” is the number of arguments, e.g. the arity of * is 2, of the built-in abs function 1, of a constant 0.) Thus, we only need one most general expression for each different operator or function. (In this context, the unary minus (-X) and binary minus (X-Y) operators are different.)
Having established this collection, we must next determine the permissible type of each Prolog variable in the expression. For example, if we are writing a rule which permits X+Y to be replaced by Y+X, both X and Y may be either integer or real: it doesn’t matter which. On the other hand, a rule which allows us to infer X>=Y+1 from X>Y is only valid if both X and Y are integers. The permissible type does not need to distinguish between subrange types, sets and sequences etc.: most FDL types are easily distinguished by context. It is only with integers, reals and enumerated types that we need to make a distinction (since all use the relational operators <=, >=, < and >). We have the following type classifications available to us:
i must be integer only: real but not integer is not sufficient.
ir must be integer or real (i.e. numeric).
e must be of an enumerated type (i.e. non-numeric).
ire any ordered type (i.e. integer, real or enumerated).
any all other types (e.g. boolean, set, sequence, record, array).
Because of the need from time to time to restrict arguments of rules to one of these classes, it is important that you do not mix types within a rule family in a particular file too much. For example, the rule (mentioned earlier)
some_inequality(1): X >= Y+1 may_be_deduced_from
[
X > Y ].
requires that both arguments of the >= operator should be in category i (integer only), whereas
some_inequality(2): X >= Y+Z may_be_deduced_from
[ X >= Y, Z <= 0 ].
only requires that both arguments to the >= be in ir (numeric — not ire, as we use addition, which is not defined for enumerated types), and
some_inequality(3): X >= Z may_be_deduced_from
[
X >= Y, Y >= Z ].
is o.k. for both arguments to the >= in ire (i.e. ir or e). Given this, it would be wise to put these three rules into three distinct families (or in three distinct files, or both). If we put them into the same family, we must declare
rulefamilysome_inequality:A>=Brequires[A:i,B:i].
as otherwise, the first rule might be used with arguments which are real but not integer, in which case this rule would be invalid.
For each different most general expression occurring within a family, you should provide a single declaration in which each Prolog variable in each declared expression is given a classification. The classification list (following the keyword requires) is zero or more matches of the form VARIABLE:CLASSIFICATION (where VARIABLE is the Prolog variable whose classification is being declared and CLASSIFICATION is one of i, ir, e, ire or any), separated by commas. In the case of constants, the classification list is the empty list [].
To give you a feel for the declarations necessary, all of the Proof Checker’s built-in rule files contain (as comments) the rule family declarations which would be needed if these rule files were not built-in (see chapter 4). Finally, note that a rule family’s declaration must precede the rule family in the rule file.
As the Proof Checker is written in Prolog, comments within rule files should be delimited by the /* and */ character sequences.
We strongly recommend that you should use comments freely within proof rule files, for instance to provide justifications for the rules, to give precise definitions of proof functions from which the rules are claimed to follow and to record any changes made to the rulefile.
6 Definition And Proof Of Proof Rules
In the previous chapter, we considered the syntax of user-definable proof rules. In this chapter, we give some advice on ensuring that the proof rules introduced to the Proof Checker in this way are “sensible”: non-contradictory and based on a precise definition of the functions involved. The main problem arises when one introduces one or more proof rules which are intended to capture the semantics of a proof function introduced in code annotations: are the conditions in the proof rules strong enough? Have all cases been covered? What is the true domain of the function? How can we prove that a collection of rules follow from a definition of a function? These are concerns which we address here.
In section 6.1 we consider the notion of a definition of a function and consider explicit and implicit definitions and the coverage of the function domain. In section 6.2 we consider what we mean by properties, and how we might go about proving, perhaps only semi-formally, that a property follows from some definitions. In section 6.3 we discuss issues to do with the domains of functions and what we can do to guard against definedness problems when employing “partial” functions. Finally, in section 6.4 we consider how we can use the SPADE Proof Checker to support the type of proof-work which might arise in section 6.2 — that property rules follow from definitions — and illustrate this with an example.
We assume that the reader is familiar with the notion of a mathematical function as something which, for particular argument values, returns a particular result value. Thus, abs(_) is a built-in FDL function which, when applied to the argument -3 returns 3. Note that abs(_) cannot return any other value when applied to -3: for every possible argument value, abs(_) can return at most one value, because it is a function (rather than a relation). However, there is more than one argument value which, when used as argument to abs(_), returns the result 3: both abs(-3) and abs(3) return 3 for instance. Equally, there are “result values” (in the type integer) for which no argument to abs(_) exists which returns such a value: e.g. abs(x) = -1 is impossible for any x. We can make all of these statements with confidence because we can state a definition for abs (whose signature we regard here as integer --> integer, ignoring for the moment its use with real arguments also):
abs(x) == x if x >= 0,
== -x if x < 0
(here, == should be read as “equals by definition”) and from this prove theorems:
for_all(x:integer, for_some(y:integer, abs(x) = y))
for_some(x:integer, for_some(y:integer,
abs(x) = abs(y) and x <> y))
for_some(x:integer, for_all(y:integer, abs(y) <> x)).
The first theorem reassures us that the function abs(_) is fully defined over the whole of the candidate domain integer: we can apply abs(_) to any integer and we will always get a result. (In other words, abs(_) is not partial with respect to the domain integer). The second theorem demonstrates that abs(_) is not one-to-one (since two different arguments may map to the same result) and the third theorem demonstrates that abs(_) is not onto (i.e. there exist elements in the range integer to which no argument value ever gets mapped).
In defining a function for use with the Checker, it is necessary first of all to give a signature (in the FDL text) giving the types of the function’s argument(s) and the type of its result. We call the cartesian product of the argument types (regarded as sets) the domain of the function and the result type its range. However, in this, any subtype (e.g. a subrange of the integers, or a subrange of an enumerated type) is regarded as its base type, so type smallint = 0..255 is regarded as the type integer, which is the unbounded set of integers. With this extension (which gives us static typechecking), we call the function a total function if it is properly defined for every possible element of the domain, and a partial function if it is only defined for a subset of this general domain. For partial functions, we should also ensure that we are applying the function to elements of the true domain (i.e. the subset of the domain over which the function is properly defined), using techniques which we shall discuss in section 6.3.
By far the most straightforward means of defining a function is through an explicit definition. An explicit definition of a function f takes the form
f(x1,...,xn) = a1(x1,...,xn) if p1(x1,...,xn),
= a2(x1,...,xn) if p2(x1,...,xn),
..........
= am(x1,...,xn) if pm(x1,...,xn).
In this definition, each ai is a function (hopefully simpler!) which applies when the predicate pi is true. It is important that the pi are disjoint, i.e. that for each possible (x1,...,xn) in the domain of f, at most one pi holds, since otherwise the definition may be self-contradictory; we should only ever relax this requirement if we can prove that all possible overlaps always give precisely the same results. If it is also the case that at least one pi holds, then f is a total function over this domain (provided each of the ai is suitably total over the required domains when pi is true). Thus, our example definition of abs(_) restricted to the integers in the preceding subsection is an explicit definition (it has the above form) and it is total, since for any integer x, it must satisfy one and only one of the predicates {x>=0, x<0}. With such explicit definitions, it can be straightforward to identify parts of the domain for which the function is not defined (because none of the pi cover this case, or because some of the ai are themselves partial over parts of the domain for which they are used). Note that there is an implicit universal quantification over the x1,...,xn in such explicit definitions.
Implicit definitions may be more difficult to use and to check for definedness than explicit ones. If we are lucky, it may be possible to rewrite them into an implicit form, e.g. if we regard
for_all(x:integer, for_all(y:integer,
y <> 0 -> (x div y) * y + x mod y = x))
as an implicit definition of mod (in terms of div, * and +) we can rewrite the equality to yield
for_all(x:integer, for_all(y:integer,
y <> 0 -> x mod y = x - (x div y) * y))
and use this for our definition of the (partial) function mod, since subtraction is available to us as the inverse to addition. However, for the more general case where we have
for_all(x1:t1, ..., for_all(xn:tn,
p(x1,...,xn,f(x1,...,xn)) )...)
as an implicit definition of f, it may not be so easy! If you think that (for function sr (integer): integer)
for_all(x:integer, sr(x) * sr(x) = x)
is a reasonable definition of a square root function, for instance, think again: first, is sr returning the positive or the negative square root (or will it sometimes return one, sometimes the other according to the value of x)? Secondly, when is sr undefined? (It is clearly partial, since no (non-imaginary) value when multiplied by itself gives -1 for instance, and no integer value squared gives 2. Are these the only problem values? Just think how much more difficult it is to decide this for less simple implicit definitions!)
Where implicit definitions do arise (as a result of their use in the routine’s specification for instance), concerns over definedness and determinism are more complex and will need to be thought about individually. However, there is a class of implicit definitions which can be handled more easily, to which we turn our attention next.
A recursive definition defines a function in terms of a number of base cases and a number of recursion cases. Thus, the simple example
for_all(n: integer,
{1} (n = 0 -> factorial(n) = 1) and
{2} (n > 0 -> factorial(n) = n * factorial(n-1)))
can be seen to be a reasonable recursive definition of the function factorial for all non-negative integers, since every possible non-negative integer argument to factorial will be covered by a number of applications of the second (recursion case) defining property followed by an application of the first (base case) property. In making this observation, we are effectively reasoning that the definition is well-formed by mathematical induction. Where we can come up with effective inductive arguments as to the definedness of such recursively-defined functions, we may be satisfied with our definition, though we must be careful that the base cases are sufficient to ensure termination in all cases of interest, and we should beware that the definition is sufficiently unambiguous for our purposes. As another example of a reasonable recursive definition, consider
type intseq = sequence of integer;
function sum_seq (intseq): integer;
for_all(s:intseq,
{1} (s = [] -> sum_seq(s) = 0) and
{2} (s <> [] -> sum_seq(s) = first(s) +
sum_seq(nonfirst(s)))).
This recursively defines a function which sums the elements of a sequence of integers, regarding the empty-list as having sum zero.
Typically, in a file of proof rules we may be more interested in giving particular properties of the functions which we have defined, rather than merely giving the definition repeatedly using this. For example, we may define a predicate
ordered(a,l,u)==
for_all(i:integer,(l<=iandi<u)->a[i]<=a[i+1])
which is true whenever array a is ordered over the range l..u. From this, we can make a number of observations, thus (all implicitly universally quantified):
l>u->ordered(a,l,u)
ordered(a,l,l)
ordered(a,l,m)andordered(a,m,u)->ordered(a,l,u)
ordered(a,l,u)anda[u]<=a[u+1]->ordered(a,l,u+1)
These observations may be more useful in proving the correctness of a sort algorithm than the strict definition above: ordered(a, l, l) may be of use for the initialisation path from the start of the routine to the (presumable) code loop(s) and the fourth property might be of use in proving the correctness of paths around the loop, for instance.
It is all very well to state these properties, but how do we ensure that they are not self-contradictory and that they capture all the required detail? (My first instinct was to write the third property above as
ordered(a,l,m)andordered(a,m+1,u)->ordered(a,l,u)
for instance, but this allows a[m] to be greater than a[m+1]: not a very satisfactory concept of ordering!) If we have not given a proper definition of the function, the answer may be: very little. If, however, we have given a strict definition (and, better still, this definition is explicit and total), we may use this definition to prove that the required properties are indeed consequences of it. For instance, let’s outline a proof of (the correct form of) property three above. As the definition of ordered is a single clause, it always applies (there are no distinct options to consider by cases). Thus, we can expand property three out to yield
H1:
for_all(i:integer, (l <= i and i < m) -> a[i] <=
a[i+1])
H2: for_all(i:integer,
(m <= i and i < u) -> a[i] <=
a[i+1])
-->
C1: for_all(i:integer, (l <= i and i < u)
-> a[i]
<=
a[i+1]).
(Here, I have rewritten the formula (A and B -> C), making C the conclusion C1, and A and B hypotheses H1 and H2 respectively, arriving at a form more reminiscent of Proof Checker formulae.) How do we prove the conclusion for all i in l..u-1? By cases: either i is in l..m-1, or i is in m..u-1. In the first case, we can use H1 to prove that a[i] <= a[i+1]. For case 2, i is in m..u-1, so we may now use H2 to prove the conclusion. Either way, the conclusion holds so we have proved C1 by cases. (Why does this not work for the erroneous property three given earlier? -- Try it!)
Thus, where we have an adequate definition, we can use this to prove properties and then utilise these properties as proof rules. In fact, we can perform the proofs that the properties follow from the definition using the Proof Checker, if we have restricted ourselves to first-order classical logic, as we shall consider in section 6.4. First, in the next section, we turn to a question which may have occurred to you in reading the above: what happens when the array indices go out of range in this argument?
A classic example of a partial function is the integer division operator, div; this only has a value if its second argument is non-zero. However, in most conventional imperative languages, all the arithmetic operators are partial: if x+y goes outside the subrange -32768..32767 (or some other integer subrange), we get a run-time error (or odd behaviour). We may guard against this where it is of concern to us by embedding check statements in our FDL model, e.g.
check d <> 0;
x := c div d;
We may think this is sufficient; is it? No! If c=-32768, d=-1, the correct result is 32768, which is outside our subrange; with the above check, we are proving that the result of the algorithm is mathematically defined on a machine with “better” arithmetic, but we have not completely established absence of overflow/run-time error. However, in principle it is possible to annotate our code in such a way as to establish this for most programs of interest.
If we introduce such checks, we may then establish that such subrange rules (i.e. restriction to true domain) are being respected by our algorithm. But we must be careful to include and establish these partiality conditions in our proof annotations (pre and post and assert statements, for instance) and to maintain these in our proof rules. Thus, in the preceding section we abstracted out of our definition of ordered the fact that the array-type object used as first argument to ordered has a valid index range outside which we should not access elements. We have a choice as to how best to ensure that no violation arises in practice; we may either modify the definition of ordered to read
ordered(a,l,u)==
for_all(i:integer,
(l<=ianda_low<=iandi<uandi<a_high)->
a[i]<=a[i+1])
(where the index range of a is a_low..a_high) and then reflect these extra constraints in each of our proof rules about ordered, or we may add extra conditions to any assertions about ordered, e.g. augmenting
ordered(a, l, u)
to
ordered(a, l, u) and a_low <= l and l <= a_high and
a_low <= u and u <= a_high.
The choice is in part a matter of personal preference: you should choose the route which you regard as most satisfactory for your approach to proof.
6.4 Proofs Of Properties From Definitions
As we saw in section 6.2, from a definition we may establish consequences for use as proof rules. One example was the ordered predicate; another is the predicate maxof, defined by
maxof(x,a,l,u)==
for_all(i:integer,(l<=iandi<=u)->a[i]<=x)
and for_some(i:integer,l<=iandi<=uanda[i]=x)
where
const low_int = integer: pending;
const high_int = integer: pending;
type indexrange = low_int..high_int;
type arrayofint = array [indexrange] of integer;
function maxof (integer, arrayofint, indexrange,
indexrange): boolean .
We claim that the four proof rules
max(1): not maxof(X,A,L,U) may_be_deduced_from [ L>U ].
max(2): maxof(element(A,[L]),A,L,L) may_be_deduced.
max(3): maxof(X,A,L,U+1) may_be_deduced_from
[ maxof(X,A,L,U), X >= element(A,[U+1]) ].
max(4): maxof(element(A,[U+1]),A,L,U+1)
may_be_deduced_from
[ maxof(X,A,L,U), element(A,[U+1]) >= X ].
are consequences of this definition; how can we prove this using the Checker for support?
First of all, we write the definition of maxof out as a single proof rule, thus:
maxdef(1):maxof(X,A,L,U) may_be_replaced_by
(for_all(i:integer,
(L<=iandi<=U)->
element(A,[i])<=X)
and
for_some(i:integer,
L<=iandi<=Uandelement(A,[i])=X)
).
and include this as the only rule in our rule file. Next, we create a .VCG file containing four formulae to prove, one for each of the rules to be established. Notice that to establish inference rules, which all of the above are, we map
X may_be_deduced_from Y to Y’ -> X
X may_be_deduced to X
(where Y’ is the formula (Y1 and ... and Yn) for list [Y1,...,Yn]). For substitution rules, we map
X may_be_replaced_by Y if Z to Z’ -> X=Y
X & Y are_interchangeable if Z to Z’ -> X=Y
X may_be_replaced_by Y to X=Y
X & Y are_interchangeable to X=Y .
Thus, for the above four proof rules, we get a .VCG file of the form shown overleaf:
****************************************************
RESULTS OF SPADE SEMANTIC ANALYSIS
PVL SPADE TOOL VERSION : 4.3
Program Validation Limited, Southampton, England
****************************************************
maxof proof rules
DATE : 25-DEC-1988 TIME : 00:00:00.00
VERIFICATION CONDITIONS
(not simplified)
For proof rule max(1) [empty-range case] :
maxof_proof_rule_1.
H1: l > u.
->
C1: not maxof(x, a, l, u).
For proof rule max(2) [unit-range case] :
maxof_proof_rule_2.
H1: true.
->
C1: maxof(element(a, [l]), a, l, l).
For proof rule max(3) [extension of range - case 1] :
maxof_proof_rule_3.
H1: maxof(x, a, l, u).
H2: x >= element(a, [u + 1]).
->
C1: maxof(x, a, l, u + 1).
For proof rule max(4) [extension of range - case 2] :
maxof_proof_rule_4.
H1: maxof(x, a, l, u).
H2: element(a, [u + 1]) >= x.
->
C1: maxof(element(a, [u + 1]), a, l, u + 1).
Figure 5(a): Formulae to establish correctness of max rules
Notice that in this .VCG file, all of the “variables” (x, a, l, u) are implicitly universally quantified. Also, it is important to ensure that such manually-produced .VCG files are in exactly the right format: see chapter 4 of the SPADE Proof Checker User Manual for some observations on the format of .VCG files. Finally, we also need a .FDL file declaring the objects used in the .VCG file, thus:
title maxof proof rules;
const low_int = integer: pending;
const high_int = integer: pending;
type indexrange = low_int .. high_int;
type arrayofint = array [indexrange] of integer;
proof function maxof (integer, arrayofint,
indexrange,
indexrange): boolean;
var a: arrayofint;
var l, u: indexrange;
var x: integer;
start
{*** DUMMY FDL MODEL - USED FOR TYPE INFORMATION
ONLY ***}
finish
We can then enter the Proof Checker and use the maxdef(1) proof rule to prove each of the four VCs in turn. Where such properties of defined functions are being used, this is a worthwhile exercise, both to vet the definition and rules by exercising the former and establishing the latter as consequences and to demonstrate consistency and increase one’s familiarity with and understanding of the proof functions employed.
7 Using Buildchlib, The Rule-Library Builder
The tool Buildchlib is no longer shipped with the Checker following the release of version 2.05. The use of user-defined rule files is still permitted, through the consult command. For further information contact Praxis High Integrity Systems.
Document Control and References
Praxis High Integrity Systems Limited, 20 Manvers Street, Bath BA1 1PX, UK.
Copyright Praxis High Integrity Systems Limited 2009. All rights reserved.
$CVSROOT/userdocs/Checker_Rules.doc (was formerly S.P0468.73.32)
Issue 0.1 (1st July 1997): Conversion to new standard document format.
Issue 0.2 (17th December 1997): Minor formatting changes made.
Issue 0.3 (21st January 1998): After initial review by Ian O’Neill.
Issue 1.0 (30th January 1998): After formal review.
Issue 2.0 (6th November 2001): Updated for release 1.46
Issue 2.1 (11th January 2002): Included two new rulefiles.
Issue 2.2 (30th May 2002): Included ENUMERATION.RUL (CFR 1052)
Issue 3.0 (24th June 2002): Definitive issue to accompany Checker 1.47 following review S.P0468.79.77.
Issue 4.0 (2nd April 2003): Updated to new template format.
Issue 5.0 (9th June 2003): Changes to new template, final format.
Issue 5.1 (7th June 2004): Correction to rule exp(6) in FDLFUNCS (CFR 1374)
Issue 5.2 (23rd November 2004): Changed company name only.
Issue 5.3 (1st July 2005): Updated rules following SICSTUS PROLOG Port.
Issue 5.4 (6th July 2005): Updated unification rules following CFR 1526.
Issue 5.5 (16th November 2005): Removal of buildchlib and new rule modular(32).
Issue 5.6 (22nd November 2005): Changed Line Manager.
Issue 5.7 (15th December 2005): Updated following review S.P0468.79.90.
Issue 5.8 (20th March 2006): Correction to rules intdiv(5) and intdiv(6).
Issue 5.9 (2nd February 2009): Modify copyright notice.
Nil.
None.