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