1\DOC uptodate_term
2
3\TYPE {uptodate_term : term -> bool}
4
5\SYNOPSIS
6Tells if a term is out of date.
7
8\KEYWORDS
9term.
10
11\DESCRIBE
12Operations in the current theory segment of HOL allow one to redefine
13types and constants. This can cause theorems to become invalid. As a
14result, HOL has a rudimentary consistency maintenance system built
15around the notion of whether type operators and term constants are
16``up-to-date''.
17
18An invocation {uptodate_term M} checks {M} to see if it has been built
19from any out-of-date components. The definition of {out-of-date} is
20mutually recursive among types, terms, and theorems. If {M} is a
21variable, it is out-of-date if its type is out-of-date. If {M} is a
22constant, it is out-of-date if it has been redeclared, or if its type is
23out-of-date, or if the witness theorem used to justify its existence
24is out-of-date.  If {M} is a combination, it is out-of-date if either
25of its components are out-of-date. If {M} is an abstraction, it is
26out-of-date if either the bound variable or the body is out-of-date.
27
28All items from ancestor theories are fixed, and unable to
29be overwritten, thus are always up-to-date.
30
31\FAILURE
32Never fails.
33
34\EXAMPLE
35{
36- Define `fact x = if x=0 then 1 else x * fact (x-1)`;
37Equations stored under "fact_def".
38Induction stored under "fact_ind".
39> val it = |- fact x = (if x = 0 then 1 else x * fact (x - 1)) : thm
40
41- val M = Term `!x. 0 < fact x`;
42> val M = `!x. 0 < fact x` : term
43
44- uptodate_term M;
45> val it = true : bool
46
47- delete_const "fact";
48> val it = () : unit
49
50- uptodate_term M;
51> val it = false : bool
52}
53
54\SEEALSO
55Theory.uptodate_type, Theory.uptodate_thm.
56
57\ENDDOC
58