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