underAIs : (thm -> thm) -> (thm -> thm)
STRUCTURE
SYNOPSIS
Applies a derived rule underneath external “guarding” of universal variables and implications.
DESCRIPTION
A call to underAIs f th strips away external guarding in th, applies the function f, and then restores the original guarding. In this context, “guarding” is the presence of universal quantifications and antecedents in implications. Thus, this function sees the theorem ∀x. p x ==> ∀y. q y ∧ r x y ==> s as the body s, guarded by the universal variables x and y and the assumptions p x and q y ∧ r x y. Negations in the body are not viewed as implications.
FAILURE
As all theorems are of this shape, the stripping and restoration of guarding always succeeds. However, this function will fail if f fails when applied to the theorem A' |- s, with s the body (as above), and A' the original hypotheses of theorem augmented with the antecendents of guarding implications.
EXAMPLE
> underAIs (EXISTS (“∃m. (k * n) MOD m = 0”, “n:num”))
           arithmeticTheory.MOD_EQ_0;
val it = ⊢ ∀n. 0 < n ⇒ ∀k. ∃m. (k * n) MOD m = 0: thm
SEEALSO
HOL  Trindemossen-1