MK_COMB : thm * thm -> thm
Proves equality of combinations constructed from equal
functions and operands.
When applied to theorems A1 |- f = g and A2 |- x = y, the inference
rule MK_COMB returns the theorem A1 u A2 |- f x = g y.
A1 |- f = g A2 |- x = y
A1 u A2 |- f x = g y
- FAILURE CONDITIONS
Fails unless both theorems are equational and f and g are
functions whose domain types are the same as the types of x and y
# let th1 = ABS `n:num` (ARITH_RULE `SUC n = n + 1`)
and th2 = NUM_REDUCE_CONV `2 + 2`;;
val th1 : thm = |- (\n. SUC n) = (\n. n + 1)
val th2 : thm = |- 2 + 2 = 4
# let th3 = MK_COMB(th1,th2);;
val th3 : thm = |- (\n. SUC n) (2 + 2) = (\n. n + 1) 4
# let th1 = NOT_DEF and th2 = TAUT `p /\ p <=> p`;;
val th1 : thm = |- (~) = (\p. p ==> F)
val th2 : thm = |- p /\ p <=> p
val it : thm = |- ~(p /\ p) <=> (\p. p ==> F) p
This is one of HOL Light's 10 primitive inference rules. It underlies, among
other things, the replacement of subterms in rewriting.
- SEE ALSO
AP_TERM, AP_THM, BETA_CONV, TRANS.