folMappingContextScript.sml

1Theory folMappingContext[bare]
2Libs
3  HolKernel Parse boolLib tautLib
4
5(* ------------------------------------------------------------------------- *)
6(* Worker theorems for first-order proof translation.  Formerly proved by    *)
7(* folMapping.sml as it loaded.                                              *)
8(* ------------------------------------------------------------------------- *)
9
10Theorem HIDE_LITERAL:  !a. a ==> ~a ==> F
11Proof tautLib.TAUT_TAC
12QED
13
14Theorem SHOW_LITERAL:  !x. (~x ==> F) ==> x
15Proof tautLib.TAUT_TAC
16QED
17
18Theorem INITIALIZE_CLAUSE:  !a b. a \/ b ==> ~a ==> b
19Proof tautLib.TAUT_TAC
20QED
21
22Theorem FINALIZE_CLAUSE:  !a b. (~a ==> b) ==> (a \/ b)
23Proof tautLib.TAUT_TAC
24QED
25
26Theorem RESOLUTION:  !a. a /\ ~a ==> F
27Proof tautLib.TAUT_TAC
28QED
29
30Theorem EQUAL_STEP:  !a b c. ((a ==> (b = c)) /\ b) ==> ~a \/ c
31Proof tautLib.TAUT_TAC
32QED
33
34Theorem EXCLUDED_MIDDLE':  !t. ~t \/ t
35Proof tautLib.TAUT_TAC
36QED