hurdUtilsContextScript.sml

1Theory hurdUtilsContext[bare]
2Libs
3  HolKernel Parse boolLib
4
5(* ------------------------------------------------------------------------- *)
6(* Small boolean lemmas hurdUtils.sml formerly derived at load time via      *)
7(* DECIDE (which fires TAUT_PROVE and hence prove).                          *)
8(* ------------------------------------------------------------------------- *)
9
10Theorem EQ_NEG_T:  !a. (~a <=> T) <=> (a <=> F)
11Proof REPEAT STRIP_TAC THEN BOOL_CASES_TAC ``a:bool`` THEN REWRITE_TAC []
12QED
13
14Theorem EQ_NEG_F:  !a. (~a <=> F) <=> (a <=> T)
15Proof REPEAT STRIP_TAC THEN BOOL_CASES_TAC ``a:bool`` THEN REWRITE_TAC []
16QED
17
18Theorem STRONG_CONJ_lem:  !a b. a /\ (a ==> b) ==> a /\ b
19Proof REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [] THEN RES_TAC
20QED