File: AP_TERM.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 (26 lines) | stat: -rw-r--r-- 539 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
 
\DOC AP_TERM

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

\SYNOPSIS
Applies a function to both sides of an equational theorem.

\KEYWORDS
rule.

\DESCRIBE
When applied to a term {f} and a theorem {A |- x = y}, the
inference rule {AP_TERM} returns the theorem {A |- f x = f y}.
{
      A |- x = y
   ----------------  AP_TERM "f"
    A |- f x = f y
}
\FAILURE
Fails unless the theorem is equational and the supplied term is a function
whose domain type is the same as the type of both sides of the equation.

\SEEALSO
AP_THM, MK_COMB.

\ENDDOC