1open HolKernel boolLib simpLib Parse realSimps
2
3open bossLib
4open testutils
5
6val s = SIMP_CONV (bossLib.std_ss ++ REAL_REDUCE_ss) []
7
8fun test (problem, result) = let
9  val t2s = trace ("Unicode", 0) term_to_string
10  val padr = StringCvt.padRight #" "
11  val padl = StringCvt.padLeft #" "
12  val p_s = padr 30 (t2s problem)
13  val r_s = padl 10 (t2s result)
14  val _ = tprint (p_s ^ " = " ^ r_s)
15  val th = QCONV s problem
16  val answer = rhs (concl th)
17in
18  if aconv answer result then OK()
19  else die ("FAILED!\n  Got "^term_to_string answer)
20end;
21
22val tests = [(``~~3r``, ``3r``),
23             (``3r + 4``, ``7r``),
24             (``3 - 4r``, ``~1r``),
25             (``abs (~20r)``, ``20r``),
26             (``abs (1/6)``, ``1/6``),
27             (``abs (~3/6)``, ``1/2``),
28             (``abs 0``, ``0``),
29             (``3r * 3/4``, ``9/4``),
30             (``6/~8``, ``~3/4``),
31             (``1/3 + 1/2``, ``5/6``),
32             (``1/2 = 0``, ``F``),
33             (``0 + 3r``, ``3r``),
34             (``3r * 0``, ``0r``),
35             (``~0r``, ``0r``),
36             (``1r - 0``, ``1r``),
37             (``1 / 10 + 0r``, ``1r/10``),
38             (``0r + 1 / 10``, ``1r/10``),
39             (``1/2 * 0r``, ``0r``),
40             (``0r * 1/2``, ``0r``)]
41
42val _ = List.app test tests
43
44val _ = List.app
45          (fn (s1,s2) => tpp_expected
46                           {testf=standard_tpp_message, input=s1, output=s2})
47          [("realinv 2", "2�����"), ("inv (TC R)", "R��� ���")]
48val _ = tpp "��p ��� q"                                                   (* UOK *)
49
50fun UNCH_test (n,c,t) =
51  shouldfail {checkexn = fn Conv.UNCHANGED => true | _ => false,
52              printarg = fn t => "UNCHANGED " ^ n ^ ": " ^ term_to_string t,
53              printresult = thm_to_string, testfn = c} t
54fun nftest (r as (n,c,t1,t2)) =
55    let
56      fun test (t1,t2) = (Exn.capture c t1, Exn.capture c t2)
57      fun check t res =
58          case res of
59              Exn.Res (Exn.Res rth, Exn.Exn Conv.UNCHANGED) =>
60                rhs (concl rth) ~~ t
61            | _ => false
62      fun pr1 t (Exn.Exn e) = "On first call, unexpected exn: " ^
63                                General.exnMessage e
64        | pr1 t (Exn.Res th) = if is_eq (concl th) andalso
65                                  rhs (concl th) ~~ t
66                               then ""
67                               else "On first call, unexpected thm:\n  " ^
68                                    thm_to_string th
69      fun nlnzero "" = "" | nlnzero s = s ^ "\n"
70      fun pr2 (Exn.Exn Conv.UNCHANGED) s = s
71        | pr2 (Exn.Exn e) s = nlnzero s ^ "On 2nd call, unexpected exn: " ^
72                              General.exnMessage e
73        | pr2 (Exn.Res th) s = nlnzero s ^ "On 2nd call, unexpected thm:\n  " ^
74                               thm_to_string th
75      fun pr t (r1,r2) = pr2 r2 (pr1 t r1)
76    in
77      tprint (n ^ ": " ^ term_to_string t1);
78      require_msg (check t2) (pr t2) test (t1,t2)
79    end
80fun simpl ths = SIMP_CONV (BasicProvers.srw_ss()) ths
81fun asimpl ths = SIMP_CONV (BasicProvers.srw_ss() ++ numSimps.ARITH_ss) ths
82val simp = simpl []
83val _ = List.app nftest [
84      ("MULCANON01", REALMULCANON, ���x:real * y * x���, ���x pow 2 * y���),
85      ("MULCANON02", REALMULCANON, ���x:real * y * x * 2���, ���2 * (x pow 2 * y)���),
86      ("MULCANON03", REALMULCANON,
87       ���10 * (x:real) * y * x pow 3 * y * x pow 4 * z * 6���,
88       ���60 * (x pow 8 * y pow 2 * z)���),
89      ("MULCANON04", REALMULCANON, ���x * 1r * z���, ���x:real * z���),
90      ("MULCANON05", REALMULCANON, ���x * y * inv x * a���, ���a * y * NZ x���),
91      ("MULCANON06", REALMULCANON, ���b * x pow 2 * y * inv x * a���,
92       ���a * b * x * y���),
93      ("MULCANON07", REALMULCANON, ���b * x * y * inv (x pow 2) * 2 * a���,
94       ���2 * (a * b * inv x * y)���),
95      ("MULCANON08", REALMULCANON, ���b * x * y * inv (x pow 2) * a * inv x���,
96       ���a * b * inv x pow 2 * y���),
97      ("MULCANON09", REALMULCANON, ���x * 2r���, ���2r * x���),
98      ("MULCANON10", REALMULCANON, ���x * 2r * y���, ���2r * (x * y)���),
99      ("MULCANON11", REALMULCANON, ���x * 3 * y * x pow n * z���,
100       ���3 * (x * y * z * x pow n)���),
101      ("MULCANON12", REALMULCANON, ���2 pow x * z * 10 * 2 pow n���,
102       ���10 * (z * 2 pow n * 2 pow x)���),
103      ("MULCANON13", REALMULCANON, ���-(2 pow x) * z * -10 * 2 pow n���,
104       ���10 * (z * 2 pow n * 2 pow x)���),
105      ("MULCANON14", REALMULCANON, ���inv 2 pow x * z * 2 pow x���, ���z:real���),
106      ("MULCANON15", REALMULCANON, ���inv (2 pow x) * z * 3 * 2 pow x���,
107       ���3 * z:real���),
108      ("MULCANON16", REALMULCANON, ���inv (2 pow x) * z * 3���,
109       ���3 * (z * inv (2 pow x))���),
110      ("MULCANON17", REALMULCANON, ���4 * (inv 2 * z)���, ���2r * z���),
111      ("MULCANON18", REALMULCANON,
112       ���2 * (inv 3 * z * 2 * inv 10)���, ���(2r/15) * z���),
113      ("MULCANON19", REALMULCANON, ���2 * (inv 3 * z * 6 * inv 4)���, ���z:real���),
114      ("MULCANON21", REALMULCANON, ���-z * x: real���, ���-(x * z:real)���),
115      ("MULCANON22", REALMULCANON, ���2 * (-inv 3 * z * 6 * inv 4)���, ���-z:real���),
116      ("MULCANON23", REALMULCANON,
117       ���(2/3) * (z * y:real)���, ���(2/3) * (y * z:real)���),
118      ("MULCANON24", REALMULCANON,
119       ���2 pow x * y pow 2 * 2 pow x * inv y���, ���y * (2 pow x) pow 2���),
120      ("MULCANON25", REALMULCANON,
121       ���x * y * (2 pow b) pow 2 * inv 2 pow b���, ���x * y * 2 pow b���),
122      ("MULCANON26", REALMULCANON, ���2 * x * inv 2 pow 2���, ���1/2 * x:real���),
123      ("MULRELNORM01", simp,
124       ���z <> 0 ��� 2r * z pow 2 * inv yy = 5 * z pow 2 * inv y * a���,
125       ���z <> 0 ��� 2 * inv yy = 5 * (a * inv y)���),
126      ("MULRELNORM02", simp, ���z * 4 = inv x * 6���, ���2 * z = 3 * inv x���),
127      ("MULRELNORM03", simp,
128       ���y <> 0 ==> 2 * inv y pow 2 <= 9 * inv y * z���,
129       ���y <> 0 ==> 2 <= 9 * (y * z)���),
130      ("MULRELNORM04", simp,
131       ���inv (2 pow x) * inv y pow 2 <= 9 * inv y * inv 2 pow x���,
132       ���inv y pow 2 <= 9 * inv y���),
133      ("MULRELNORM05", simp,
134       ���y <> 0 ==>
135        inv (2 pow x) * inv y pow 2 <= 9 * inv y pow 6 * inv 2 pow x���,
136       ���y <> 0 ==> y pow 4 <= 9���),
137      ("MULRELNORM06", simp,
138       ���0 < x ==> 3 * x pow 2 <= x���, ���0 < x ==> 3 * x <= 1r���),
139      ("MULRELNORM07", simp,
140       ���0 < x ==> 3 * x pow 2 <= inv x���, ���0 < x ==> 3 * x pow 3 <= 1r���),
141      ("MULRELNORM08", simp, ���2 * x <= inv 2 * y * z���, ���4r * x <= y * z���),
142      ("MULRELNORM09", simp, ���2 * x <= 1/2 * (y * z:real)���, ���4r * x <= y * z���),
143      ("MULRELNORM10", simp,
144       ���3/4 * x <= 5/6 * (y * z:real)���, ���9r * x <= 10 * (y * z)���),
145      ("MULRELNORM11", simp, ���0r < x ==> x <= x * y���, ���0r < x ==> 1 <= y���),
146      ("MULRELNORM12", simpl [ASSUME ���x <> 0r���, ASSUME ���x < 0r���,
147                              ASSUME ���x < 1r���],
148       ���inv x < 1r���, ���T���),
149      ("MULRELNORM13", simp, ���x <> 0 /\ x < 0 ==> inv x < 1r���,
150       ���x <> 0 /\ x < 0 ==> x < 1���),
151      ("MULRELNORM14", simp, ���x <> 0 /\ 0 < x ==> inv x < 1r���,
152       ���x <> 0 /\ 0 < x ==> 1 < x���),
153      ("MULRELNORM15", simp, ���2r * x = 1/2 * z���, ���4 * x = z���),
154      ("MULRELNORM16", asimpl [ASSUME ���m < lg : num���],
155       ���inv (2 pow m) < 2 * inv (2 pow lg)���,
156       ���2 pow lg < 2 * 2 pow m���),
157      ("ADDCANON1", REALADDCANON, ���10 + x * 2 + x * y + 6 + x���,
158       ���3 * x + x * y + 16���)
159    ]
160
161val simpc = SIMP_CONV (srw_ss() ++ ARITH_ss ++ REAL_ARITH_ss)
162val _ = shouldfail {
163      checkexn = (fn UNCHANGED => true | _ => false),
164      printarg =
165      fn _ => "simp w/o nat d.p. but with real d.p. leaves input unchanged",
166      printresult = thm_to_string,
167      testfn = simpc [Excl "NUM_ARITH_DP"]
168    } ���4n < x ==> 2 < x���
169val _ = shouldfail {
170      checkexn = (fn UNCHANGED => true | _ => false),
171      printarg =
172      fn _ => "simp with nat d.p. but w/o real d.p. leaves input unchanged",
173      printresult = thm_to_string,
174      testfn = simpc [Excl "REAL_ARITH_DP"]
175    } ���4r < x ==> 2 < x���
176
177val _ = tprint "Removing nat d.p. still lets real d.p. work"
178val _ = require_msg (check_result (aconv ���bool$T���))
179                    term_to_string
180                    (rhs o concl o simpc [Excl "NUM_ARITH_DP"])
181                    ���4r < x ==> 2 < x���
182val _ = tprint "Removing real d.p. still lets nat d.p. work"
183val _ = require_msg (check_result (aconv ���bool$T���))
184                    term_to_string
185                    (rhs o concl o simpc [Excl "REAL_ARITH_DP"])
186                    ���4n < x ==> 2 < x���
187
188
189
190val _ = Process.exit Process.success
191