mesonLibContextScript.sml

1Theory mesonLibContext[bare]
2Libs
3  HolKernel Parse boolLib tautLib
4
5(* ------------------------------------------------------------------------- *)
6(* Lemmas mesonLib.sml formerly proved as it loaded.                         *)
7(* ------------------------------------------------------------------------- *)
8
9Theorem meson_imp_conv:  a \/ b <=> ~b ==> a
10Proof tautLib.TAUT_TAC
11QED
12
13Theorem meson_not_imp_p:  (~p ==> p) <=> p
14Proof tautLib.TAUT_TAC
15QED
16
17Theorem meson_p_imp_not_p:  (p ==> ~p) <=> ~p
18Proof tautLib.TAUT_TAC
19QED
20
21Theorem meson_eq_thms:
22  (x:'a = x) /\ (~(x:'a = y) \/ ~(x = z) \/ (y = z))
23Proof
24  REWRITE_TAC [] THEN ASM_CASES_TAC ``x:'a = y`` THEN
25  ASM_REWRITE_TAC [ONCE_REWRITE_RULE [boolTheory.DISJ_SYM]
26                    (REWRITE_RULE [] boolTheory.BOOL_CASES_AX)]
27QED
28
29Theorem meson_imp_elim:  (a ==> b) <=> ~a \/ b
30Proof tautLib.TAUT_TAC
31QED
32
33Theorem meson_eq_elim:  (a = b) ==> b \/ ~a
34Proof tautLib.TAUT_TAC
35QED