1\DOC bool_ss
2
3\TYPE {bool_ss : simpset}
4
5\SYNOPSIS
6Basic simpset containing standard propositional and first order logic
7simplifications, plus beta conversion.
8
9\KEYWORDS
10simplification
11
12\LIBRARY
13boolSimps
14
15\DESCRIBE
16The {bool_ss} simpset is almost at the base of the system-provided
17simpset hierarchy.  Though not very powerful, it does include the
18following ad hoc collection of rewrite rules for propositions and
19first order terms:
20{
21   |- !A B. ~(A ==> B) = A /\ ~B
22   |- !A B. (~(A /\ B) = ~A \/ ~B) /\
23            (~(A \/ B) = ~A /\ ~B)
24   |- !P. ~(!x. P x) = ?x. ~P x
25   |- !P. ~(?x. P x) = !x. ~P x
26   |- (~p = ~q) = (p = q)
27   |- !x. (x = x) = T
28   |- !t. ((T = t) = t) /\
29          ((t = T) = t) /\
30          ((F = t) = ~t) /\
31          ((t = F) = ~t)
32   |- (!t. ~~t = t) /\ (~T = F) /\ (~F = T)
33   |- !t. (T /\ t = t) /\
34          (t /\ T = t) /\
35          (F /\ t = F) /\
36          (t /\ F = F) /\
37          (t /\ t = t)
38   |- !t. (T \/ t = T) /\
39          (t \/ T = T) /\
40          (F \/ t = t) /\
41          (t \/ F = t) /\
42          (t \/ t = t)
43   |- !t. (T ==> t = t) /\
44          (t ==> T = T) /\
45          (F ==> t = T) /\
46          (t ==> t = T) /\
47          (t ==> F = ~t)
48   |- !t1 t2. ((if T then t1 else t2) = t1) /\
49              ((if F then t1 else t2) = t2)
50   |- !t. (!x. t) = t
51   |- !t. (?x. t) = t
52   |- !b t. (if b then t else t) = t
53   |- !a. ?x. x = a
54   |- !a. ?x. a = x
55   |- !a. ?!x. x = a,
56   |- !a. ?!x. a = x,
57   |- (!b e. (if b then T else e) = b \/ e) /\
58      (!b t. (if b then t else T) = b ==> t) /\
59      (!b e. (if b then F else e) = ~b /\ e) /\
60      (!b t. (if b then t else F) = b /\ t)
61   |- !t. t \/ ~t
62   |- !t. ~t \/ t
63   |- !t. ~(t /\ ~t)
64   |- !x. (@y. y = x) = x
65   |- !x. (@y. x = y) = x
66   |- !f v. (!x. (x = v) ==> f x) = f v
67   |- !f v. (!x. (v = x) ==> f x) = f v
68   |- !P a. (?x. (x = a) /\ P x) = P a
69   |- !P a. (?x. (a = x) /\ P x) = P a
70}
71Also included in {bool_ss} is a conversion to perform beta reduction, as
72well as the following congruence rules, which allow the simplifier to glean
73additional contextual information as it descends through implications and
74conditionals.
75{
76   |- !x x' y y'.
77       (x = x') ==>
78       (x' ==> (y = y')) ==> (x ==> y = x' ==> y')
79
80   |- !P Q x x' y y'.
81       (P = Q) ==>
82       (Q ==> (x = x')) ==>
83       (~Q ==> (y = y')) ==> ((if P then x else y) = (if Q then x' else y'))
84}
85
86\FAILURE
87Can't fail, as it is not a functional value.
88
89\USES
90The {bool_ss} simpset is an appropriate simpset from which to build
91new user-defined simpsets. It is also useful in its own right, for
92example when a delicate simplification is desired, where other more
93powerful simpsets might cause undue disruption to a goal.  If even
94less system rewriting is desired, the {pure_ss} value can be used.
95
96\SEEALSO
97pureSimps.pure_ss, bossLib.std_ss, bossLib.arith_ss, bossLib.list_ss,
98bossLib.SIMP_CONV, bossLib.SIMP_TAC, bossLib.RW_TAC.
99
100\ENDDOC
101