1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
\DOC inductive_type_store
\TYPE {inductive_type_store : (string * (int * thm * thm)) list ref}
\SYNOPSIS
List of inductive types defined with corresponding theorems.
\DESCRIBE
The reference variable {inductive_type_store} holds an association list that
associates with the name of each inductive type defined so far (e.g. {"list"}
or {"1"}) a triple: the number of constructors, the induction theorem and the
recursion theorem for it. The two theorems are exactly of the form returned by
{define_type}.
\FAILURE
Not applicable.
\EXAMPLE
This example is characteristic:
{
# assoc "list" (!inductive_type_store);;
val it : int * thm * thm =
(2, |- !P. P [] /\ (!a0 a1. P a1 ==> P (CONS a0 a1)) ==> (!x. P x),
|- !NIL' CONS'.
?fn. fn [] = NIL' /\
(!a0 a1. fn (CONS a0 a1) = CONS' a0 a1 (fn a1)))
}
\noindent while the following shows that there is an entry for the Boolean
type, for the sake of regularity, even though it is not normally considered an
inductive type:
{
# assoc "bool" (!inductive_type_store);;
val it : int * thm * thm =
(2, |- !P. P F /\ P T ==> (!x. P x), |- !a b. ?f. f F = a /\ f T = b)
}
\USES
This list is mainly for internal use. For example it is employed by {define} to
automatically prove the existence of recursive functions over inductive types.
Users may find the information helpful to implement their own proof tools.
However, while the list may be inspected, it should not be modified explicitly
or there may be unwanted side-effects on {define}.
\SEEALSO
define, define_type, new_recursive_definition, prove_recursive_functions_exist.
\ENDDOC
|
