Filter
Top Products
72 CHAPTER 9. DERIVED RULES
Γ p ∧ q
Γ p
CONJUNCT1
Γ p ∧ q
Γ q
CONJUNCT2
All the other defined constants come equipped with a similar suite of rules. In
most cases the reader will be able to guess how the corresponding CAML function
is used, and can experiment a little on the lines of the above examples.
Γ p
Γ p =
EQT INTRO
Γ p =
Γ p
EQT ELIM
Γ p ⇒ q ∆ p
Γ ∪ ∆ ⇒ q
MP
Γ q
Γ − {p} p ⇒ q
DISCH
Γ p ⇒ q
Γ ∪ {p} q
UNDISCH
Γ ∀x. p
Γ p[t/x]
SPEC
Here p[t/x] denotes the result of substituting t for all free instances of x in
p. HOL automatically renames variables to avoid capture if necessary, by adding
prime characters. (This happens in the primitive function INST that is used in the
implementation.)
#let th1 = ASSUME ‘!x. x >= 0‘;;
th1 : thm = !x. x >= 0 |- !x. x >= 0
#let th2 = SPEC ‘y + 1‘ th1;;
th2 : thm = !x. x >= 0 |- y + 1 >= 0
#let th3 = ASSUME ‘!x. ?y. y > x‘;;
th3 : thm = !x. ?y. y > x |- !x. ?y. y > x
#let th4 = SPEC ‘y:num‘ th3;;
th4 : thm = !x. ?y. y > x |- ?y’. y’ > y
Note that the naive result of substituting would be the incorrect ?y. y > y.
Γ p
Γ ∀x. p
GEN
This rule will fail if the variable x is free in the assumptions Γ. Again, this
restriction arises naturally out of one in the underlying primitives, in this case in
ABS.