| Scheme = | ||
| [ scheme ] Scheme-Identifier { Scheme-Parameters } : | ||
| Scheme-Conclusion | ||
| [ provided | ||
| Scheme-Premise | ||
| { and Scheme-Premise } ] | ||
| Justification ; . | ||
| Scheme-Identifier = Identifier . | ||
| Scheme-Parameters = Scheme-Segment { , Scheme-Segment } . | ||
| Scheme-Conclusion = Sentence . | ||
| Scheme-Premise = Proposition . | ||
| Scheme-Segment = Predicate-Segment | Functor-Segment . | ||
| Predicate-Segment = | ||
| Predicate-Identifier { , Predicate-Identifier } [ Type-Expression-List ] . | ||
| Predicate-Identifier = Identifier . | ||
| Functor-Segment = | ||
| Functor-Identifier { , Functor-Identifier } ( [ Type-Expression-List ] ) Specification . | ||
| Functor-Identifier = Identifier . | ||
Scheme is an assertion where the second-order free variables are used. It states that the Scheme Conclusion holds provided that Scheme Premises hold. Note that, if there is no Scheme Premises then the Scheme Conclusion is always true. Of course, the Scheme should be justified.
As Scheme Parameters the predicates and functors can appear. They are used to formulate the Scheme Conclusion . Here, the difference between a Scheme and a Theorem appears. In theorems only first-order variables can be used.
The Scheme is refered to via its identifier - in this context called a Scheme Identifier .
If the header scheme is omited then the Scheme is local, i.e. it can be accessed only within an article that define it, and can not be accessed externally - in other articles. Schemes with headers enclosed are exported to the data base.
Ind - The Scheme of natural induction,
To justify a theorem of the form "for every natural number the
property P holds" with this Scheme, first, one must prove:
A: P[0]; B: for k being Nat holds P[k + 1]; |
and then the Scheme can be used as follows:
for k being Nat holds P[k] from Ind(A, B); |
Last modified: June 26, 2000