folToolsContextScript.sml

1Theory folToolsContext[bare]
2Ancestors
3  normalForms
4Libs
5  HolKernel Parse boolLib
6
7(* ------------------------------------------------------------------------- *)
8(* Equality and boolean lemmas for folTools.  Formerly proved as folTools    *)
9(* loaded, which made those proofs sensitive to link-order-dependent         *)
10(* ambient state (parser and current theory).                                *)
11(* ------------------------------------------------------------------------- *)
12
13Theorem EQ_SYMTRANS:
14  !x y z. ~(x:'a = y) \/ ~(x = z) \/ (y = z)
15Proof
16  REPEAT STRIP_TAC THEN
17  ASM_CASES_TAC ``x:'a = y`` THEN
18  ASM_REWRITE_TAC
19    [ONCE_REWRITE_RULE [boolTheory.DISJ_SYM]
20       (REWRITE_RULE[] boolTheory.BOOL_CASES_AX)]
21QED
22
23Theorem EQ_COMB:
24  !f g x y. ~(f:'a->'b = g) \/ ~(x = y) \/ (f x = g y)
25Proof
26  REPEAT GEN_TAC THEN
27  ASM_CASES_TAC ``x:'a = y`` THEN
28  ASM_CASES_TAC ``f:'a->'b = g`` THEN
29  ASM_REWRITE_TAC []
30QED
31
32Theorem EQ_BOOL_CONJ:
33  (!x y. ~x \/ ~(x = y) \/ y) /\
34  (!x y. x \/ (x = y) \/ y) /\
35  (!x y. ~x \/ (x = y) \/ ~y)
36Proof
37  REPEAT CONJ_TAC THEN
38  REPEAT GEN_TAC THEN
39  ASM_CASES_TAC ``x:bool`` THEN
40  ASM_CASES_TAC ``y:bool`` THEN
41  ASM_REWRITE_TAC []
42QED