1load"simpLib"; 2open Simplifier Simpsets arith_ss ; 3infix ++; 4trace_level := 5; 5quotation := true; open Parse; 6 7(* reduction in operand *) 8SIMP_PROVE bool_ss [] (--`((P:'a) = P') ==> (P' = P)`--); 9 10(* reduction in operand *) 11SIMP_PROVE bool_ss [] (--`((P:'a) = P') ==> ((Q P:'b) = Q P')`--); 12 13(* reduction in operator *) 14SIMP_PROVE bool_ss [] (--`(P = P') ==> (P (Q:'a) = (P' Q:'b))`--); 15 16(* reductions in both *) 17SIMP_PROVE bool_ss [] (--`(P = P') /\ (Q = Q') ==> ((P:'b->'a) Q = P' Q')`--); 18 19(* reduction inside abs. *) 20SIMP_PROVE bool_ss [] (--`(P = P') ==> ((!x:'a. P x) = (!x. P' x))`--); 21 22(* solving side conditions with a dproc (SATISFY) *) 23 24(* making reductions with a dproc *) 25(*Fails! *) 26val ss = mk_simpset [BOOL_ss,SATISFY_ss]; 27SIMP_PROVE ss [] (--`Q 0 1 ==> ?x y. Q x y`--);; 28SIMP_PROVE ss [] (--`Q 1 1 /\ (!z:num. R z 0) ==> ?x y z. Q x y /\ R z 0`--);; 29 30(* making reductions with a conversion (BETA_CONV) *) 31SIMP_PROVE bool_ss [] (--`(\x. Q x 0:num) 1 = Q 1 0`--);; 32 33(* unwinding *) 34val ss = mk_simpset [BOOL_ss,UNWIND_ss]; 35SIMP_CONV ss [] (--`?a b:num. (0 = a) /\ P a b`--);; 36SIMP_CONV ss [] (--`!a b:num. (1 + 2 = a) ==> P a b`--);; 37SIMP_CONV ss [] (--`!a b:num. G ==> R /\ (3 = a) ==> P a b`--);; 38 39(* reprocessing of non-trivial context 40Before adding reprocessing the "else" branch of the following 41would not have been simplified *) 42 43SIMP_PROVE bool_ss [boolTheory.DE_MORGAN_THM] 44 (--`((P \/ Q) => x | ~P) = (P \/ Q ==> x)`--); 45 46 47(* multiple beta convs *) 48SIMP_CONV bool_ss [] (--`(\x y z. P x y z:num) 1 2 3`--); 49 50(* arithmetic *) 51trace_level := 1;; 52SIMP_PROVE arith_ss [] (--`P (x + 2) = (P (2 + x):'a)`--); 53 54SIMP_CONV arith_ss [] (--`1 < 2 => 3 | 4`--); 55SIMP_CONV arith_ss [] (--`(x > z + 1) /\ ( y + 1 > x + 1) => (y > x) | Z`--); 56SIMP_CONV arith_ss [] (--`(x > 20 + 1) /\ ( y + 1 > x + 1) => (y > 15) | Z`--); 57profile2 SIMP_CONV arith_ss (--`(x > z + 1) /\ ( y + 1 > x + 1) => (y > x) | Z`--); 58 59 60(* cached arithmetic *) 61CACHED_ARITH [] (--`1 < 2`--);; 62CACHED_ARITH [] (--`1 < 2`--);; (* cache hit - success *) 63CACHED_ARITH [] (--`3 < 1`--);; 64CACHED_ARITH [] (--`3 < 1`--);; (* cache hit, failure *) 65 66(* semi-congruence closure via conditional rewriting *) 67val CC = SIMP_PROVE bool_ss [] (--`!P:'a->'b. (x = x') ==> (P x = P x')`--); 68val CC2 = SIMP_PROVE bool_ss [] (--`!P:'a->'b->'c. (x = x') /\ (y = y') ==> (P x y = P x' y')`--); 69SIMP_PROVE arith_ss [CC,CC2] (--`y >= z ==> z >= y ==> (P y (x + 2):bool = P z (2 + x))`--); 70