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
|
let AND_IMP = prove
(`!a b c. a /\ b ==> c <=> a ==> b ==> c`,CONV_TAC TAUT);;
let AND_IMP2 = prove
(`!a b c. a /\ b ==> c <=> (a<=>T) ==> b ==> c`,CONV_TAC TAUT);;
let AND_IMP3 = prove
(`!a b c. ~a /\ b ==> c <=> (a<=>F) ==> b ==> c`,CONV_TAC TAUT);;
let NOT_NOT = GEN_ALL (hd (CONJUNCTS (SPEC_ALL NOT_CLAUSES)));;
let AND_INV = prove
(`!a. (~a /\ a) <=> F`,CONV_TAC TAUT);;
let AND_INV_IMP = prove
(`!a. a ==> ~a ==> F`,CONV_TAC TAUT);;
let OR_DUAL = prove
(`(~(a \/ b) ==> F) = (~a ==> ~b ==> F)`,CONV_TAC TAUT);;
let OR_DUAL2 = prove
(`(~(a \/ b) ==> F) = ((a==>F) ==> ~b ==> F)`,CONV_TAC TAUT);;
let OR_DUAL3 = prove
(`(~(~a \/ b) ==> F) = (a ==> ~b ==> F)`,CONV_TAC TAUT);;
let AND_INV2 = prove
(`(~a ==> F) ==> (a==>F) ==> F`,CONV_TAC TAUT)
let NOT_ELIM2 = prove
(`(~a ==> F) <=> a`,CONV_TAC TAUT)
let IMP_F_EQ_F = prove
(`!t. (t ==> F) <=> (t <=> F)`,CONV_TAC TAUT);;
|
