BoolconvContextScript.sml

1Theory BoolconvContext[bare]
2Libs
3  HolKernel Parse boolLib
4
5(* ------------------------------------------------------------------------- *)
6(* Conjunctions of boolean simplifications Boolconv.sml formerly proved as   *)
7(* it loaded.                                                                *)
8(* ------------------------------------------------------------------------- *)
9
10Theorem BOOLCONV_NOT:
11  (~T <=> F) /\ (~F <=> T) /\ !t. ~~t <=> t
12Proof REWRITE_TAC [NOT_CLAUSES]
13QED
14
15Theorem BOOLCONV_AND:
16  (!t. T /\ t <=> t) /\ (!t. t /\ T <=> t) /\
17  (!t. F /\ t <=> F) /\ (!t. t /\ F <=> F) /\ (!t. t /\ t <=> t)
18Proof REWRITE_TAC [AND_CLAUSES]
19QED
20
21Theorem BOOLCONV_OR:
22  (!t. T \/ t <=> T) /\ (!t. t \/ T <=> T) /\
23  (!t. F \/ t <=> t) /\ (!t. t \/ F <=> t) /\ (!t. t \/ t <=> t)
24Proof REWRITE_TAC [OR_CLAUSES]
25QED
26
27Theorem BOOLCONV_IMP:
28  (!t. (T ==> t) <=> t) /\ (!t. (t ==> T) <=> T) /\
29  (!t. (F ==> t) <=> T) /\ (!t. (t ==> F) <=> ~t) /\
30  (!t. (t ==> t) <=> T)
31Proof REWRITE_TAC [IMP_CLAUSES]
32QED
33
34Theorem BOOLCONV_BEQ:
35  (!t. (T <=> t) <=> t) /\ (!t. (t <=> T) <=> t) /\
36  (!t. (F <=> t) <=> ~t) /\ (!t. (t <=> F) <=> ~t) /\
37  (!t:bool. (t <=> t) <=> T)
38Proof REWRITE_TAC [EQ_CLAUSES]
39QED
40
41Theorem BOOLCONV_COND:
42  (!t1 t2. (if T then t1 else t2) = (t1:'a)) /\
43  (!t1 t2. (if F then t1 else t2) = (t2:'a)) /\
44  (!b t.   (if b then t else t) = (t:'a))
45Proof REWRITE_TAC [COND_CLAUSES, COND_ID]
46QED