The Language Pt. 3
A proof consists of four types of sentences.- Deductions
- Variable declarations
- Constant declarations
- Namespace declarations
DEDUCTIONS
Proof sentences consist of a name atom, a colon, a list of comma-separated antecedant propositions, a deduction symbol, and a consequent proposition, followed by a justification or a subproof. Subproofs are proofs encased in either curly or square brackets. The last line of a subproof must have no step name, no antecedants and a consequent matching that of the step the subproof justifies. Some examples are:T4: u+w=v+w ⊨ u=v Rep(T3)
T4: ⊨ u=v { : u=v MP(T1,T2); }
VARIABLE DECLARATIONS
A variable declaration consists of the keyword Var, a semantic type, and an atom, optionally followed by an argument list, consisting of atoms that are also variables. If there is no argument list, the variable's semantic type will be exactly the one given. If there are arguments, the type of the variable will be the compound type which has the types of arguments as the domain list, and the given type as the range type. The variables used as arguments must be defined in the same scope as the declaration. Some examples of variable declarations are:- Var 0 x;
- Var 0 y;
- Var 0 z(x,y)
CONSTANT DECLARATIONS
A constant declaration consists of the keyword Const, a semantic type, an atom optionally followed by an argument list. This can in turn be optionally followed by the "≜" symbol and then a definition. If there is no argument list, the variable's semantic type will be exactly the one given. If there are arguments, the type of the variable will be the compound type which has the types of arguments as the domain list, and the given type as the range type. The variables used as arguments must be defined in the same scope as the declaration. Free variables occuring in the definition must either be the arguments in the argument list or variables declared outside of the present scope. The definition must have the same semantic type as the one given in the prototype.- Const 0 C;
- Const 0 g(x,y)≜f(x)+y;
- Const 0 a+b≜sum(a,b);
Const 0 .real.#=nat2real(.#);
The above example will have the effect of defining .real.0,.real.1,... as nat2real(.0),nat2real(.1). By using a namespace declaration such asUse namespace .real with {digit}+;
numbers without explicit namespaces will be implicitly assumed to have namespace .real.NAMESPACE DECLARATIONS
A namespace declaration has the form:Use namespace <namespace sequence> with <regular expression>.Some examples are
- Use namespace . with {equals};
- Use namespace .real.sub1 with T{alpha}*;
- Use namespace .real.sub2.a with {alnum}+⋃{plus};