boolSimpsContextScript.sml

1Theory boolSimpsContext[bare]
2Ancestors
3  combin
4Libs
5  HolKernel Parse boolLib
6
7(* ------------------------------------------------------------------------- *)
8(* Lemmas boolSimps.sml formerly proved as it loaded.                        *)
9(* ------------------------------------------------------------------------- *)
10
11Theorem literal_cong:
12  (v:'a = v') ==> (literal_case (f:'a -> 'b) v = literal_case f (I v'))
13Proof
14  DISCH_THEN SUBST_ALL_TAC THEN
15  REWRITE_TAC [literal_case_THM, combinTheory.I_THM]
16QED
17
18Theorem literal_I_thm:
19  literal_case (f:'a -> 'b) (I x) = f x
20Proof
21  REWRITE_TAC [combinTheory.I_THM, literal_case_THM]
22QED
23
24Theorem let_cong:
25  (v:'a = v') ==> (LET (f:'a -> 'b) v = LET f (I v'))
26Proof
27  DISCH_THEN SUBST_ALL_TAC THEN
28  REWRITE_TAC [LET_THM, combinTheory.I_THM]
29QED
30
31Theorem let_I_thm:
32  LET (f:'a -> 'b) (I x) = f x
33Proof
34  REWRITE_TAC [combinTheory.I_THM, LET_THM]
35QED
36
37Theorem NESTED_COND:
38  !p (q:'a) (r:'a) s.
39    (COND p (COND p q r) s = COND p q s) /\
40    (COND p q (COND p r s) = COND p q s) /\
41    (COND p (COND (~p) q r) s = COND p r s) /\
42    (COND p q (COND (~p) r s) = COND p q r)
43Proof
44  REPEAT GEN_TAC THEN COND_CASES_TAC THEN REWRITE_TAC []
45QED