new_basic_definition : term -> thm
Makes a simple new definition of the form c = t.
If t is a closed term and c a variable whose name has not been used as a
constant, then new_basic_definition `c = t` will define a new constant c
and return the theorem |- c = t for that new constant (not the variable in
the given term). There is an additional restriction that all type variables
involved in t must occur in the constant's type.
- FAILURE CONDITIONS
Fails if c is already a constant.
Here is a simple example
and of course we can equally well use logical equivalence:
# let googolplex = new_basic_definition
`googolplex = 10 EXP (10 EXP 100)`;;
val googolplex : thm = |- googolplex = 10 EXP (10 EXP 100)
The following example helps to explain why the restriction on type
variables is present:
# let true_def = new_basic_definition `true <=> T`;;
val true_def : thm = |- true <=> T
If we had been allowed to get back a definitional theorem, we could separately
type-instantiate it to the 1-element type 1 and the 2-element type bool. In
one case the RHS is true, and in the other it is false, yet both are asserted
equal to the constant trivial.
# new_basic_definition `trivial <=> !x y:A. x = y`;;
Failure "new_definition: Type variables not reflected in constant".
There are simpler or more convenient ways of making definitions, such as
define and new_definition, but this is the primitive principle underlying
- SEE ALSO
define, new_definition, new_inductive_definition, new_recursive_definition,