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