| | | B.4.9 typeaxiom: Instantiate Type Axiom |
typeaxiom V1, V2, ... in V
In proving mode.
For every constant declaration c:T in the environment of the current proof state, the system implicitly adds an invisible "type axiom" pT(c) to the state which may be used as additional knowledge by a decision procedure unaware about the properties of type T (e.g., an assumption x >= 0 for a constant x:NAT). This may not be sufficient in case of a function f:S -> T where for some application f(a) a type axiom pT(f(a)) should be added to the prove state (e.g., an assumption f(a) >= 0 for a function f:S -> NAT and constant a:S). Likewise, this may not be sufficient for an array a: ARRAY S OF T where for some array access a[i] a type axiom pT(a[i]) should be added.
The command typeaxiom takes a value V which denotes a function with n parameters (respectively an array); it also takes n argument terms V1, V2, ..., Vn whose types match the parameter types (respectively one argument term V1 whose type matches the index type of the array). The command generates a child state which is identical to the current state but has the "type axiom" for the application of the function to the terms added as an explicit assumption. The types of the argument terms need not equal the types of the parameter terms; if necessary, a second child state with a side condition p(V1, V2, ..., Vn) as a goal is generated. If no type axiom can be derived from the function/array or the types of the argument terms do not match the types of the parameters, no child state is generated.
An additional proof state may be generated for a type checking condition corresponding to the values V1, V2, ..., and the matching of their types to the types of the instantiation parameters.
The command makes knowledge implicit in the domains of function types explicit as assumptions in those (rather rare) cases where a proof state can be only closed by a decision procedure with the help of this knowledge. It is useful for functions whose domain involves subtypes of some base type, e.g. for functions whose domains involve the domain of natural numbers NAT or involve a type generated by the constructor SUBTYPE.
| | | B.4.9 typeaxiom: Instantiate Type Axiom |