File: AP_THM.doc

package info (click to toggle)
hol88 2.02.19940316dfsg-5
  • links: PTS
  • area: main
  • in suites: bookworm
  • size: 65,816 kB
  • sloc: ml: 199,939; ansic: 9,666; sh: 6,913; makefile: 6,032; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (30 lines) | stat: -rw-r--r-- 637 bytes parent folder | download | duplicates (11) 
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
 
\DOC AP_THM

\TYPE {AP_THM : (thm -> term -> thm)}

\SYNOPSIS
Proves equality of equal functions applied to a term.

\KEYWORDS
rule.

\DESCRIBE
When applied to a theorem {A |- f = g} and a term {x}, the inference
rule {AP_THM} returns the theorem {A |- f x = g x}.
{
      A |- f = g
   ----------------  AP_THM (A |- f = g) "x"
    A |- f x = g x
}
\FAILURE
Fails unless the conclusion of the theorem is an equation, both sides
of which are functions whose domain type is the same as that of the
supplied term.

\COMMENTS
The type of {AP_THM} is shown by the system as {thm -> conv}.

\SEEALSO
AP_TERM, ETA_CONV, EXT, MK_COMB.

\ENDDOC