schneiderUtilsContextScript.sml

1Theory schneiderUtilsContext[bare]
2Libs
3  HolKernel Parse boolLib
4
5(* ------------------------------------------------------------------------- *)
6(* Absorption lemmas schneiderUtils.sml formerly proved as it loaded.        *)
7(* The third theorem (a case-split for booleans) is already in boolTheory as *)
8(* FORALL_BOOL and is used directly there.                                   *)
9(* ------------------------------------------------------------------------- *)
10
11Theorem LEFT_ABSORB_DISJ:  !a b. a \/ b <=> a \/ (~a /\ b)
12Proof
13  REPEAT GEN_TAC THEN BOOL_CASES_TAC ``a:bool`` THEN REWRITE_TAC []
14QED
15
16Theorem RIGHT_ABSORB_DISJ:  !a b. a \/ b <=> (a /\ ~b) \/ b
17Proof
18  REPEAT GEN_TAC THEN BOOL_CASES_TAC ``b:bool`` THEN REWRITE_TAC []
19QED
20
21Theorem LEFT_DISJ_TAC_lem:  !a b. a \/ b <=> ~b ==> a
22Proof
23  REPEAT GEN_TAC THEN BOOL_CASES_TAC ``a:bool`` THEN REWRITE_TAC []
24QED
25
26Theorem RIGHT_DISJ_TAC_lem:  !a b. a \/ b <=> ~a ==> b
27Proof
28  REPEAT GEN_TAC THEN BOOL_CASES_TAC ``a:bool`` THEN REWRITE_TAC []
29QED