1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
|
\DOC MK_COMB
\TYPE {MK_COMB : thm * thm -> thm}
\SYNOPSIS
Proves equality of combinations constructed from equal
functions and operands.
\KEYWORDS
rule, combination, equality.
\DESCRIBE
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
--------------------------- MK_COMB
A1 u A2 |- f x = g y
}
\FAILURE
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}
respectively.
\EXAMPLE
{
# 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
# MK_COMB(th1,th2);;
val it : thm = |- ~(p /\ p) <=> (\p. p ==> F) p
}
\COMMENTS
This is one of HOL Light's 10 primitive inference rules. It underlies, among
other things, the replacement of subterms in rewriting.
\SEEALSO
AP_TERM, AP_THM, BETA_CONV, TRANS.
\ENDDOC
|
