uptodate_term

Theory.uptodate_term : term -> bool

Tells if a term is out of date.

Operations in the current theory segment of HOL allow one to redefine types and constants. This can cause theorems to become invalid. As a result, HOL has a rudimentary consistency maintenance system built around the notion of whether type operators and term constants are “up-to-date”.

An invocation uptodate_term M checks M to see if it has been built from any out-of-date components. The definition of out-of-date is mutually recursive among types, terms, and theorems. If M is a variable, it is out-of-date if its type is out-of-date. If M is a constant, it is out-of-date if it has been redeclared, or if its type is out-of-date, or if the witness theorem used to justify its existence is out-of-date. If M is a combination, it is out-of-date if either of its components are out-of-date. If M is an abstraction, it is out-of-date if either the bound variable or the body is out-of-date.

All items from ancestor theories are fixed, and unable to be overwritten, thus are always up-to-date.

Failure

Never fails.

Example

> Define `utdtfact x = if x=0 then 1 else x * utdtfact (x-1)`;
val it = ⊢ ∀x. utdtfact x = if x = 0 then 1 else x * utdtfact (x − 1): thm

> val M = Term `!x. 0 < utdtfact x`;
val M = “∀x. 0 < utdtfact x”: term

> uptodate_term M;
val it = true: bool

> delete_const "utdtfact";
val it = (): unit

> uptodate_term M;
val it = false: bool

See also

Theory.uptodate_type, Theory.uptodate_thm