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