1(* Copyright (c) 2009-2010 Tjark Weber. All rights reserved. *) 2 3(* Various theorems for HolSmtLib *) 4 5 val T = tautLib.TAUT_PROVE 6 val P = bossLib.PROVE [] 7 val S = simpLib.SIMP_PROVE (simpLib.++ (simpLib.++ (simpLib.++ 8 (bossLib.list_ss, boolSimps.COND_elim_ss), wordsLib.WORD_ss), 9 wordsLib.WORD_BIT_EQ_ss)) [boolTheory.EQ_SYM_EQ] 10 val A = intLib.ARITH_PROVE 11 val R = realLib.REAL_ARITH 12 val W = wordsLib.WORD_DECIDE 13 val B = blastLib.BBLAST_PROVE 14 15 (* simplify 't' using 'thms', then prove the simplified term using 16 'TAUT_PROVE' *) 17 fun U thms t = 18 let 19 val t_eq_t' = simpLib.SIMP_CONV (simpLib.++ (simpLib.++ (simpLib.++ 20 (bossLib.std_ss, boolSimps.COND_elim_ss), wordsLib.WORD_ss), 21 wordsLib.WORD_BIT_EQ_ss)) thms t 22 val t' = tautLib.TAUT_PROVE (boolSyntax.rhs (Thm.concl t_eq_t')) 23 in 24 Thm.EQ_MP (Thm.SYM t_eq_t') t' 25 end 26 27 val s = Theory.save_thm 28 29 val _ = Theory.new_theory "HolSmt" 30 val _ = ParseExtras.temp_loose_equality() 31 32 33 (* constants used by Z3 *) 34 35 (* exclusive or *) 36 val xor_def = bossLib.Define `xor x y = ~(x <=> y)` 37 38 (* array_ext[T] yields an index i such that select A i <> select B i 39 (provided A and B are different arrays of type T) *) 40 val array_ext_def = bossLib.Define `array_ext A B = @i. A i <> B i` 41 42 (* used for Z3 proof reconstruction *) 43 44 val _ = s ("ALL_DISTINCT_NIL", S ``ALL_DISTINCT [] = T``) 45 val _ = s ("ALL_DISTINCT_CONS", S 46 ``!h t. ALL_DISTINCT (h::t) = ~MEM h t /\ ALL_DISTINCT t``) 47 val _ = s ("NOT_MEM_NIL", S ``!x. ~MEM x [] = T``) 48 val _ = s ("NOT_MEM_CONS", S ``!x h t. ~MEM x (h::t) = (x <> h) /\ ~MEM x t``) 49 val _ = s ("AND_T", T ``!p. p /\ T <=> p``) 50 val _ = s ("T_AND", T ``!p q. (T /\ p <=> T /\ q) ==> (p <=> q)``) 51 val _ = s ("F_OR", T ``!p q. (F \/ p <=> F \/ q) ==> (p <=> q)``) 52 val _ = s ("CONJ_CONG", T 53 ``!p q r s. (p <=> q) ==> (r <=> s) ==> (p /\ r <=> q /\ s)``) 54 val _ = s ("NOT_NOT_ELIM", T ``!p. ~~p ==> p``) 55 val _ = s ("NOT_FALSE", T ``!p. p ==> ~p ==> F``) 56 val _ = s ("NNF_CONJ", T 57 ``!p q r s. (~p <=> r) ==> (~q <=> s) ==> (~(p /\ q) <=> r \/ s)``) 58 val _ = s ("NNF_DISJ", T 59 ``!p q r s. (~p <=> r) ==> (~q <=> s) ==> (~(p \/ q) <=> r /\ s)``) 60 val _ = s ("NNF_NOT_NOT", T ``!p q. (p <=> q) ==> (~~p <=> q)``) 61 val _ = s ("NEG_IFF_1_1", T ``!p q. (q <=> p) ==> ~(p <=> ~q)``) 62 val _ = s ("NEG_IFF_1_2", T ``!p q. ~(p <=> ~q) ==> (q <=> p)``) 63 val _ = s ("NEG_IFF_2_1", T ``!p q. (p <=> ~q) ==> ~(p <=> q)``) 64 val _ = s ("NEG_IFF_2_2", T ``!p q. ~(p <=> q) ==> (p <=> ~q)``) 65 val _ = s ("DISJ_ELIM_1", T ``!p q r. (p \/ q ==> r) ==> p ==> r``) 66 val _ = s ("DISJ_ELIM_2", T ``!p q r. (p \/ q ==> r) ==> q ==> r``) 67 val _ = s ("IMP_DISJ_1", T ``!p q. (p ==> q) ==> ~p \/ q``) 68 val _ = s ("IMP_DISJ_2", T ``!p q. (~p ==> q) ==> p \/ q``) 69 val _ = s ("IMP_FALSE", T ``!p. (~p ==> F) ==> p``) 70 val _ = s ("AND_IMP_INTRO_SYM", T ``!p q r. p /\ q ==> r <=> p ==> q ==> r``) 71 val _ = s ("VALID_IFF_TRUE", T ``!p. p ==> (p <=> T)``) 72 73 (* used for Z3's proof rule def-axiom *) 74 75 val _ = s ("d001", T ``~(p <=> q) \/ ~p \/ q``) 76 val _ = s ("d002", T ``~(p <=> q) \/ p \/ ~q``) 77 val _ = s ("d003", T ``(p <=> ~q) \/ ~p \/ q``) 78 val _ = s ("d004", T ``(~p <=> q) \/ p \/ ~q``) 79 val _ = s ("d005", T ``(p <=> q) \/ ~p \/ ~q``) 80 val _ = s ("d006", T ``(p <=> q) \/ p \/ q``) 81 val _ = s ("d007", T ``~(~p <=> q) \/ p \/ q``) 82 val _ = s ("d008", T ``~(p <=> ~q) \/ p \/ q``) 83 val _ = s ("d009", T ``~p \/ q \/ ~(p <=> q)``) 84 val _ = s ("d010", T ``p \/ ~q \/ ~(p <=> q)``) 85 val _ = s ("d011", T ``p \/ q \/ ~(~p <=> q)``) 86 val _ = s ("d012", T ``p \/ q \/ ~(p <=> ~q)``) 87 val _ = s ("d013", T ``(~p /\ ~q) \/ p \/ q``) 88 val _ = s ("d014", T ``(~p /\ q) \/ p \/ ~q``) 89 val _ = s ("d015", T ``(p /\ ~q) \/ ~p \/ q``) 90 val _ = s ("d016", T ``(p /\ q) \/ ~p \/ ~q``) 91 val _ = s ("d017", P ``p \/ (y = if p then x else y)``) 92 val _ = s ("d018", P ``~p \/ (x = if p then x else y)``) 93 val _ = s ("d019", P ``p \/ ((if p then x else y) = y)``) 94 val _ = s ("d020", P ``~p \/ ((if p then x else y) = x)``) 95 val _ = s ("d021", P ``p \/ q \/ ~(if p then r else q)``) 96 val _ = s ("d022", P ``~p \/ q \/ ~(if p then q else r)``) 97 val _ = s ("d023", P ``(if p then q else r) \/ ~p \/ ~q``) 98 val _ = s ("d024", P ``(if p then q else r) \/ p \/ ~r``) 99 val _ = s ("d025", P ``(if p then ~q else r) \/ ~p \/ q``) 100 val _ = s ("d026", P ``(if p then q else ~r) \/ p \/ r``) 101 val _ = s ("d027", P ``~(if p then q else r) \/ ~p \/ q``) 102 val _ = s ("d028", P ``~(if p then q else r) \/ p \/ r``) 103 104 (* used for Z3's proof rule rewrite *) 105 106 val _ = s ("r001", P ``(x = y) <=> (y = x)``) 107 val _ = s ("r002", P ``(x = x) <=> T``) 108 val _ = s ("r003", T ``(p <=> T) <=> p``) 109 val _ = s ("r004", T ``(T <=> p) <=> p``) 110 val _ = s ("r005", T ``(p <=> F) <=> ~p``) 111 val _ = s ("r006", T ``(F <=> p) <=> ~p``) 112 val _ = s ("r007", T ``(~p <=> ~q) <=> (p <=> q)``) 113 val _ = s ("r008", T ``~(p <=> ~q) <=> (p <=> q)``) 114 val _ = s ("r009", T ``~(~p <=> q) <=> (p <=> q)``) 115 116 val _ = s ("r010", P ``(if T then x else y) = x``) 117 val _ = s ("r011", P ``(if F then x else y) = y``) 118 val _ = s ("r012", T ``(if p then q else T) <=> (~p \/ q)``) 119 val _ = s ("r013", T ``(if p then q else T) <=> (q \/ ~p)``) 120 val _ = s ("r014", T ``(if p then q else ~q) <=> (p <=> q)``) 121 val _ = s ("r015", T ``(if p then q else ~q) <=> (q <=> p)``) 122 val _ = s ("r016", T ``(if p then ~q else q) <=> (p <=> ~q)``) 123 val _ = s ("r017", T ``(if p then ~q else q) <=> (~q <=> p)``) 124 val _ = s ("r018", P ``(if ~p then x else y) = (if p then y else x)``) 125 val _ = s ("r019", P 126 ``(if p then (if q then x else y) else x) = (if p /\ ~q then y else x)``) 127 val _ = s ("r020", P 128 ``(if p then (if q then x else y) else x) = (if ~q /\ p then y else x)``) 129 val _ = s ("r021", P 130 ``(if p then (if q then x else y) else y) = (if p /\ q then x else y)``) 131 val _ = s ("r022", P 132 ``(if p then (if q then x else y) else y) = (if q /\ p then x else y)``) 133 val _ = s ("r023", P 134 ``(if p then x else (if p then y else z)) = (if p then x else z)``) 135 val _ = s ("r024", P 136 ``(if p then x else (if q then x else y)) = (if p \/ q then x else y)``) 137 val _ = s ("r025", P 138 ``(if p then x else (if q then x else y)) = (if q \/ p then x else y)``) 139 val _ = s ("r026", P 140 ``(if p then x = y else x = z) <=> (x = if p then y else z)``) 141 val _ = s ("r027", P 142 ``(if p then x = y else y = z) <=> (y = if p then x else z)``) 143 val _ = s ("r028", P 144 ``(if p then x = y else z = y) <=> (y = if p then x else z)``) 145 146 val _ = s ("r029", T ``(~p ==> q) <=> (p \/ q)``) 147 val _ = s ("r030", T ``(~p ==> q) <=> (q \/ p)``) 148 val _ = s ("r031", T ``(p ==> q) <=> (~p \/ q)``) 149 val _ = s ("r032", T ``(p ==> q) <=> (q \/ ~p)``) 150 val _ = s ("r033", T ``(T ==> p) <=> p``) 151 val _ = s ("r034", T ``(p ==> T) <=> T``) 152 val _ = s ("r035", T ``(F ==> p) <=> T``) 153 val _ = s ("r036", T ``(p ==> p) <=> T``) 154 val _ = s ("r037", T ``((p <=> q) ==> r) <=> (r \/ (q <=> ~p))``) 155 156 val _ = s ("r038", T ``~T <=> F``) 157 val _ = s ("r039", T ``~F <=> T``) 158 val _ = s ("r040", T ``~~p <=> p``) 159 160 val _ = s ("r041", T ``p \/ q <=> q \/ p``) 161 val _ = s ("r042", T ``p \/ T <=> T``) 162 val _ = s ("r043", T ``p \/ ~p <=> T``) 163 val _ = s ("r044", T ``~p \/ p <=> T``) 164 val _ = s ("r045", T ``T \/ p <=> T``) 165 val _ = s ("r046", T ``p \/ F <=> p``) 166 val _ = s ("r047", T ``F \/ p <=> p``) 167 168 val _ = s ("r048", T ``p /\ q <=> q /\ p``) 169 val _ = s ("r049", T ``p /\ T <=> p``) 170 val _ = s ("r050", T ``T /\ p <=> p``) 171 val _ = s ("r051", T ``p /\ F <=> F``) 172 val _ = s ("r052", T ``F /\ p <=> F``) 173 val _ = s ("r053", T ``p /\ q <=> ~(~p \/ ~q)``) 174 val _ = s ("r054", T ``~p /\ q <=> ~(p \/ ~q)``) 175 val _ = s ("r055", T ``p /\ ~q <=> ~(~p \/ q)``) 176 val _ = s ("r056", T ``~p /\ ~q <=> ~(p \/ q)``) 177 val _ = s ("r057", T ``p /\ q <=> ~(~q \/ ~p)``) 178 val _ = s ("r058", T ``~p /\ q <=> ~(~q \/ p)``) 179 val _ = s ("r059", T ``p /\ ~q <=> ~(q \/ ~p)``) 180 val _ = s ("r060", T ``~p /\ ~q <=> ~(q \/ p)``) 181 182 val _ = s ("r061", U [combinTheory.APPLY_UPDATE_ID] ``(x =+ f x) f = f``) 183 184 val _ = s ("r062", S ``ALL_DISTINCT [x; x] <=> F``) 185 val _ = s ("r063", S ``ALL_DISTINCT [x; y] <=> x <> y``) 186 val _ = s ("r064", S ``ALL_DISTINCT [x; y] <=> y <> x``) 187 188 val _ = s ("r065", A ``((x :int) = y) <=> (x + -1 * y = 0)``) 189 val _ = s ("r066", A ``((x :int) = y + z) <=> (x + -1 * z = y)``) 190 val _ = s ("r067", A ``((x :int) = y + -1 * z) <=> (x + (-1 * y + z) = 0)``) 191 val _ = s ("r068", A ``((x :int) = -1 * y + z) <=> (y + (-1 * z + x) = 0)``) 192 val _ = s ("r069", A ``((x :int) = y + z) <=> (x + (-1 * y + -1 * z) = 0)``) 193 val _ = s ("r070", A ``((x :int) = y + z) <=> (y + (z + -1 * x) = 0)``) 194 val _ = s ("r071", A ``((x :int) = y + z) <=> (y + (-1 * x + z) = 0)``) 195 val _ = s ("r072", A ``((x :int) = y + z) <=> (z + -1 * x = -y)``) 196 val _ = s ("r073", A ``((x :int) = -y + z) <=> (z + -1 * x = y)``) 197 val _ = s ("r074", A ``(-1 * (x :int) = -y) <=> (x = y)``) 198 val _ = s ("r075", A ``(-1 * (x :int) + y = z) <=> (x + -1 * y = -z)``) 199 val _ = s ("r076", A ``((x :int) + y = 0) <=> (y = -x)``) 200 val _ = s ("r077", A ``((x :int) + y = z) <=> (y + -1 * z = -x)``) 201 val _ = s ("r078", A 202 ``((a :int) + (-1 * x + (v * y + w * z)) = 0) <=> (x + (-v * y + -w * z) = a)``) 203 204 val _ = s ("r079", A ``0 + (x :int) = x``) 205 val _ = s ("r080", A ``(x :int) + 0 = x``) 206 val _ = s ("r081", A ``(x :int) + y = y + x``) 207 val _ = s ("r082", A ``(x :int) + x = 2 * x``) 208 val _ = s ("r083", A ``(x :int) + y + z = x + (y + z)``) 209 val _ = s ("r084", A ``(x :int) + y + z = x + (z + y)``) 210 val _ = s ("r085", A ``(x :int) + (y + z) = y + (z + x)``) 211 val _ = s ("r086", A ``(x :int) + (y + z) = y + (x + z)``) 212 val _ = s ("r087", A ``(x :int) + (y + (z + u)) = y + (z + (u + x))``) 213 214 val _ = s ("r088", A ``(x :int) >= x <=> T``) 215 val _ = s ("r089", A ``(x :int) >= y <=> x + -1 * y >= 0``) 216 val _ = s ("r090", A ``(x :int) >= y <=> y + -1 * x <= 0``) 217 val _ = s ("r091", A ``(x :int) >= y + z <=> y + (z + -1 * x) <= 0``) 218 val _ = s ("r092", A ``-1 * (x :int) >= 0 <=> x <= 0``) 219 val _ = s ("r093", A ``-1 * (x :int) >= -y <=> x <= y``) 220 val _ = s ("r094", A ``-1 * (x :int) + y >= 0 <=> x + -1 * y <= 0``) 221 val _ = s ("r095", A ``(x :int) + -1 * y >= 0 <=> y <= x``) 222 223 val _ = s ("r096", A ``(x :int) > y <=> ~(y >= x)``) 224 val _ = s ("r097", A ``(x :int) > y <=> ~(x <= y)``) 225 val _ = s ("r098", A ``(x :int) > y <=> ~(x + -1 * y <= 0)``) 226 val _ = s ("r099", A ``(x :int) > y <=> ~(y + -1 * x >= 0)``) 227 val _ = s ("r100", A ``(x :int) > y + z <=> ~(z + -1 * x >= -y)``) 228 229 val _ = s ("r101", A ``x <= (x :int) <=> T``) 230 val _ = s ("r102", A ``0 <= (1 :int) <=> T``) 231 val _ = s ("r103", A ``(x :int) <= y <=> y >= x``) 232 val _ = s ("r104", A ``0 <= -(x :int) + y <=> y >= x``) 233 val _ = s ("r105", A ``-1 * (x :int) <= 0 <=> x >= 0``) 234 val _ = s ("r106", A ``(x :int) <= y <=> x + -1 * y <= 0``) 235 val _ = s ("r107", A ``(x :int) <= y <=> y + -1 * x >= 0``) 236 val _ = s ("r108", A ``-1 * (x :int) + y <= 0 <=> x + -1 * y >= 0``) 237 val _ = s ("r109", A ``-1 * (x :int) + y <= -z <=> x + -1 * y >= z``) 238 val _ = s ("r110", A ``-(x :int) + y <= z <=> y + -1 * z <= x``) 239 val _ = s ("r111", A ``(x :int) + -1 * y <= z <=> x + (-1 * y + -1 * z) <= 0``) 240 val _ = s ("r112", A ``(x :int) <= y + z <=> x + -1 * z <= y``) 241 val _ = s ("r113", A ``(x :int) <= y + z <=> z + -1 * x >= -y``) 242 val _ = s ("r114", A ``(x :int) <= y + z <=> x + (-1 * y + -1 * z) <= 0``) 243 244 val _ = s ("r115", A ``(x :int) < y <=> ~(y <= x)``) 245 val _ = s ("r116", A ``(x :int) < y <=> ~(x >= y)``) 246 val _ = s ("r117", A ``(x :int) < y <=> ~(y + -1 * x <= 0)``) 247 val _ = s ("r118", A ``(x :int) < y <=> ~(x + -1 * y >= 0)``) 248 val _ = s ("r119", A ``(x :int) < y + -1 * z <=> ~(x + -1 * y + z >= 0)``) 249 val _ = s ("r120", A ``(x :int) < y + -1 * z <=> ~(x + (-1 * y + z) >= 0)``) 250 val _ = s ("r121", A ``(x :int) < -y + z <=> ~(z + -1 * x <= y)``) 251 val _ = s ("r122", A ``(x :int) < -y + (z + u) <=> ~(z + (u + -1 * x) <= y)``) 252 val _ = s ("r123", A 253 ``(x :int) < -y + (z + (u + v)) <=> ~(z + (u + (v + -1 * x)) <= y)``) 254 255 val _ = s ("r124", A ``-(x :int) + y < z <=> ~(y + -1 * z >= x)``) 256 val _ = s ("r125", A ``(x :int) + y < z <=> ~(z + -1 * y <= x)``) 257 val _ = s ("r126", A ``0 < -(x :int) + y <=> ~(y <= x)``) 258 259 val _ = s ("r127", A ``(x :int) - 0 = x``) 260 val _ = s ("r128", A ``0 - (x :int) = -x``) 261 val _ = s ("r129", A ``0 - (x :int) = -1 * x``) 262 val _ = s ("r130", A ``(x :int) - y = -y + x``) 263 val _ = s ("r131", A ``(x :int) - y = x + -1 * y``) 264 val _ = s ("r132", A ``(x :int) - y = -1 * y + x``) 265 val _ = s ("r133", A ``(x :int) - 1 = -1 + x``) 266 val _ = s ("r134", A ``(x :int) + y - z = x + (y + -1 * z)``) 267 val _ = s ("r135", A ``(x :int) + y - z = x + (-1 * z + y)``) 268 269 val _ = s ("r136", R ``(0 = -u * (x :real)) <=> (u * x = 0)``) 270 val _ = s ("r137", R ``(a = -u * (x :real)) <=> (u * x = -a)``) 271 val _ = s ("r138", R ``((a :real) = x + (y + z)) <=> (x + (y + (-1 * a + z)) = 0)``) 272 val _ = s ("r139", R ``((a :real) = x + (y + z)) <=> (x + (y + (z + -1 * a)) = 0)``) 273 val _ = s ("r140", R ``((a :real) = -u * y + v * z) <=> (u * y + (-v * z + a) = 0)``) 274 val _ = s ("r141", R ``((a :real) = -u * y + -v * z) <=> (u * y + (a + v * z) = 0)``) 275 val _ = s ("r142", R ``(-(a :real) = -u * x + v * y) <=> (u * x + -v * y = a)``) 276 val _ = s ("r143", R 277 ``((a :real) = -u * x + (-v * y + w * z)) <=> (u * x + (v * y + (-w * z + a)) = 0)``) 278 val _ = s ("r144", R 279 ``((a :real) = -u * x + (v * y + w * z)) <=> (u * x + (-v * y + -w * z) = -a)``) 280 val _ = s ("r145", R 281 ``((a :real) = -u * x + (v * y + -w * z)) <=> (u * x + (-v * y + w * z) = -a)``) 282 val _ = s ("r146", R 283 ``((a :real) = -u * x + (-v * y + w * z)) <=> (u * x + (v * y + -w * z) = -a)``) 284 val _ = s ("r147", R ``((a :real) = -u * x + (-v * y + -w * z)) <=> (u * x + (v * y + w * z) = -a)``) 285 val _ = s ("r148", R ``(-(a :real) = -u * x + (v * y + w * z)) <=> (u * x + (-v * y + -w * z) = a)``) 286 val _ = s ("r149", R ``(-(a :real) = -u * x + (v * y + -w * z)) <=> (u * x + (-v * y + w * z) = a)``) 287 val _ = s ("r150", R ``(-(a :real) = -u * x + (-v * y + w * z)) <=> (u * x + (v * y + -w * z) = a)``) 288 val _ = s ("r151", R ``(-(a :real) = -u * x + (-v * y + -w * z)) <=> (u * x + (v * y + w * z) = a)``) 289 val _ = s ("r152", R ``((a :real) = -u * x + (-1 * y + w * z)) <=> (u * x + (y + -w * z) = -a)``) 290 val _ = s ("r153", R ``((a :real) = -u * x + (-1 * y + -w * z)) <=> (u * x + (y + w * z) = -a)``) 291 val _ = s ("r154", R ``(-u * (x :real) + -v * y = -a) <=> (u * x + v * y = a)``) 292 val _ = s ("r155", R ``(-1 * (x :real) + (-v * y + -w * z) = -a) <=> (x + (v * y + w * z) = a)``) 293 val _ = s ("r156", R ``(-u * (x :real) + (v * y + w * z) = -a) <=> (u * x + (-v * y + -w * z) = a)``) 294 val _ = s ("r157", R ``(-u * (x :real) + (-v * y + w * z) = -a) <=> (u * x + (v * y + -w * z) = a)``) 295 val _ = s ("r158", R ``(-u * (x :real) + (-v * y + -w * z) = -a) <=> (u * x + (v * y + w * z) = a)``) 296 297 val _ = s ("r159", R ``(x :real) + -1 * y >= 0 <=> y <= x``) 298 val _ = s ("r160", R ``(x :real) >= y <=> x + -1 * y >= 0``) 299 300 val _ = s ("r161", R ``(x :real) > y <=> ~(x + -1 * y <= 0)``) 301 302 val _ = s ("r162", R ``(x :real) <= y <=> x + -1 * y <= 0``) 303 val _ = s ("r163", R ``(x :real) <= y + z <=> x + -1 * z <= y``) 304 val _ = s ("r164", R ``-u * (x :real) <= a <=> u * x >= -a``) 305 val _ = s ("r165", R ``-u * (x :real) <= -a <=> u * x >= a``) 306 val _ = s ("r166", R ``-u * (x :real) + v * y <= 0 <=> u * x + -v * y >= 0``) 307 val _ = s ("r167", R ``-u * (x :real) + v * y <= a <=> u * x + -v * y >= -a``) 308 val _ = s ("r168", R ``-u * (x :real) + v * y <= -a <=> u * x + -v * y >= a``) 309 val _ = s ("r169", R ``-u * (x :real) + -v * y <= a <=> u * x + v * y >= -a``) 310 val _ = s ("r170", R ``-u * (x :real) + -v * y <= -a <=> u * x + v * y >= a``) 311 val _ = s ("r171", R 312 ``-u * (x :real) + (v * y + w * z) <= 0 <=> u * x + (-v * y + -w * z) >= 0``) 313 val _ = s ("r172", R 314 ``-u * (x :real) + (v * y + -w * z) <= 0 <=> u * x + (-v * y + w * z) >= 0``) 315 val _ = s ("r173", R 316 ``-u * (x :real) + (-v * y + w * z) <= 0 <=> u * x + (v * y + -w * z) >= 0``) 317 val _ = s ("r174", R 318 ``-u * (x :real) + (-v * y + -w * z) <= 0 <=> u * x + (v * y + w * z) >= 0``) 319 val _ = s ("r175", R 320 ``-u * (x :real) + (v * y + w * z) <= a <=> u * x + (-v * y + -w * z) >= -a``) 321 val _ = s ("r176", R 322 ``-u * (x :real) + (v * y + w * z) <= -a <=> u * x + (-v * y + -w * z) >= a``) 323 val _ = s ("r177", R 324 ``-u * (x :real) + (v * y + -w * z) <= a <=> u * x + (-v * y + w * z) >= -a``) 325 val _ = s ("r178", R 326 ``-u * (x :real) + (v * y + -w * z) <= -a <=> u * x + (-v * y + w * z) >= a``) 327 val _ = s ("r179", R 328 ``-u * (x :real) + (-v * y + w * z) <= a <=> u * x + (v * y + -w * z) >= -a``) 329 val _ = s ("r180", R 330 ``-u * (x :real) + (-v * y + w * z) <= -a <=> u * x + (v * y + -w * z) >= a``) 331 val _ = s ("r181", R 332 ``-u * (x :real) + (-v * y + -w * z) <= a <=> u * x + (v * y + w * z) >= -a``) 333 val _ = s ("r182", R 334 ``-u * (x :real) + (-v * y + -w * z) <= -a <=> u * x + (v * y + w * z) >= a``) 335 val _ = s ("r183", R 336 ``(-1 * (x :real) + (v * y + w * z) <= -a) <=> (x + (-v * y + -w * z) >= a)``) 337 338 val _ = s ("r184", R ``(x :real) < y <=> ~(x >= y)``) 339 val _ = s ("r185", R ``-u * (x :real) < a <=> ~(u * x <= -a)``) 340 val _ = s ("r186", R ``-u * (x :real) < -a <=> ~(u * x <= a)``) 341 val _ = s ("r187", R ``-u * (x :real) + v * y < 0 <=> ~(u * x + -v * y <= 0)``) 342 val _ = s ("r188", R ``-u * (x :real) + -v * y < 0 <=> ~(u * x + v * y <= 0)``) 343 val _ = s ("r189", R ``-u * (x :real) + v * y < a <=> ~(u * x + -v * y <= -a)``) 344 val _ = s ("r190", R ``-u * (x :real) + v * y < -a <=> ~(u * x + -v * y <= a)``) 345 val _ = s ("r191", R ``-u * (x :real) + -v * y < a <=> ~(u * x + v * y <= -a)``) 346 val _ = s ("r192", R ``-u * (x :real) + -v * y < -a <=> ~(u * x + v * y <= a)``) 347 val _ = s ("r193", R 348 ``-u * (x :real) + (v * y + w * z) < a <=> ~(u * x + (-v * y + -w * z) <= -a)``) 349 val _ = s ("r194", R 350 ``-u * (x :real) + (v * y + w * z) < -a <=> ~(u * x + (-v * y + -w * z) <= a)``) 351 val _ = s ("r195", R 352 ``-u * (x :real) + (v * y + -w * z) < a <=> ~(u * x + (-v * y + w * z) <= -a)``) 353 val _ = s ("r196", R 354 ``-u * (x :real) + (v * y + -w * z) < -a <=> ~(u * x + (-v * y + w * z) <= a)``) 355 val _ = s ("r197", R 356 ``-u * (x :real) + (-v * y + w * z) < a <=> ~(u * x + (v * y + -w * z) <= -a)``) 357 val _ = s ("r198", R 358 ``-u * (x :real) + (-v * y + w * z) < -a <=> ~(u * x + (v * y + -w * z) <= a)``) 359 val _ = s ("r199", R 360 ``-u * (x :real) + (-v * y + -w * z) < a <=> ~(u * x + (v * y + w * z) <= -a)``) 361 val _ = s ("r200", R 362 ``-u * (x :real) + (-v * y + -w * z) < -a <=> ~(u * x + (v * y + w * z) <= a)``) 363 val _ = s ("r201", R 364 ``-u * (x :real) + (-v * y + w * z) < 0 <=> ~(u * x + (v * y + -w * z) <= 0)``) 365 val _ = s ("r202", R 366 ``-u * (x :real) + (-v * y + -w * z) < 0 <=> ~(u * x + (v * y + w * z) <= 0)``) 367 val _ = s ("r203", R 368 ``-1 * (x :real) + (v * y + w * z) < a <=> ~(x + (-v * y + -w * z) <= -a)``) 369 val _ = s ("r204", R 370 ``-1 * (x :real) + (v * y + w * z) < -a <=> ~(x + (-v * y + -w * z) <= a)``) 371 val _ = s ("r205", R 372 ``-1 * (x :real) + (v * y + -w * z) < a <=> ~(x + (-v * y + w * z) <= -a)``) 373 val _ = s ("r206", R 374 ``-1 * (x :real) + (v * y + -w * z) < -a <=> ~(x + (-v * y + w * z) <= a)``) 375 val _ = s ("r207", R 376 ``-1 * (x :real) + (-v * y + w * z) < a <=> ~(x + (v * y + -w * z) <= -a)``) 377 val _ = s ("r208", R 378 ``-1 * (x :real) + (-v * y + w * z) < -a <=> ~(x + (v * y + -w * z) <= a)``) 379 val _ = s ("r209", R 380 ``-1 * (x :real) + (-v * y + -w * z) < a <=> ~(x + (v * y + w * z) <= -a)``) 381 val _ = s ("r210", R 382 ``-1 * (x :real) + (-v * y + -w * z) < -a <=> ~(x + (v * y + w * z) <= a)``) 383 val _ = s ("r211", R 384 ``-u * (x :real) + (-1 * y + -w * z) < -a <=> ~(u * x + (y + w * z) <= a)``) 385 val _ = s ("r212", R 386 ``-u * (x :real) + (v * y + -1 * z) < -a <=> ~(u * x + (-v * y + z) <= a)``) 387 388 val _ = s ("r213", R ``0 + (x :real) = x``) 389 val _ = s ("r214", R ``(x :real) + 0 = x``) 390 val _ = s ("r215", R ``(x :real) + y = y + x``) 391 val _ = s ("r216", R ``(x :real) + x = 2 * x``) 392 val _ = s ("r217", R ``(x :real) + y + z = x + (y + z)``) 393 val _ = s ("r218", R ``(x :real) + y + z = x + (z + y)``) 394 val _ = s ("r219", R ``(x :real) + (y + z) = y + (z + x)``) 395 val _ = s ("r220", R ``(x :real) + (y + z) = y + (x + z)``) 396 397 val _ = s ("r221", R ``0 - (x :real) = -x``) 398 val _ = s ("r222", R ``0 - u * (x :real) = -u * x``) 399 val _ = s ("r223", R ``(x :real) - 0 = x``) 400 val _ = s ("r224", R ``(x :real) - y = x + -1 * y``) 401 val _ = s ("r225", R ``(x :real) - y = -1 * y + x``) 402 val _ = s ("r226", R ``(x :real) - u * y = x + -u * y``) 403 val _ = s ("r227", R ``(x :real) - u * y = -u * y + x``) 404 val _ = s ("r228", R ``(x :real) + y - z = x + (y + -1 * z)``) 405 val _ = s ("r229", R ``(x :real) + y - z = x + (-1 * z + y)``) 406 val _ = s ("r230", R ``(x :real) + y - u * z = -u * z + (x + y)``) 407 val _ = s ("r231", R ``(x :real) + y - u * z = x + (-u * z + y)``) 408 val _ = s ("r232", R ``(x :real) + y - u * z = x + (y + -u * z)``) 409 410 val _ = s ("r233", R ``0 * (x :real) = 0``) 411 val _ = s ("r234", R ``1 * (x :real) = x``) 412 413 val _ = s ("r235", W ``0w + x = x``) 414 val _ = s ("r236", W ``(x :'a word) + y = y + x``) 415 val _ = s ("r237", W ``1w + (1w + x) = 2w + x``) 416 val _ = s ("r238", Drule.EQT_ELIM 417 (wordsLib.WORD_ARITH_CONV ``((x :'a word) + z = y + x) <=> (y = z)``)) 418 419 val _ = s ("r239", Drule.UNDISCH_ALL (bossLib.PROVE 420 [wordsTheory.word_concat_0] ``FINITE univ(:'a) ==> x < dimword(:'b) ==> 421 ((0w :'a word) @@ (n2w x :'b word) = (n2w x :'c word))``)) 422 val _ = s ("r240", Drule.UNDISCH (simpLib.SIMP_PROVE bossLib.std_ss 423 [wordsTheory.w2w_n2w, Thm.SYM (Drule.SPEC_ALL wordsTheory.MOD_DIMINDEX)] 424 ``x < dimword(:'a) ==> (w2w (n2w x :'a word) = (n2w x :'b word))``)) 425 val _ = s ("r241", Drule.UNDISCH_ALL (bossLib.PROVE 426 [wordsTheory.word_concat_0_eq] ``FINITE univ(:'a) ==> 427 dimindex(:'b) <= dimindex(:'c) ==> y < dimword(:'b) ==> 428 (((0w :'a word) @@ (x :'b word) = (n2w y :'c word)) <=> (x = n2w y))``)) 429 val _ = s ("r242", Drule.UNDISCH_ALL (bossLib.PROVE 430 [wordsTheory.word_concat_0_eq] ``FINITE univ(:'a) ==> 431 dimindex(:'b) <= dimindex(:'c) ==> y < dimword(:'b) ==> 432 (((0w :'a word) @@ (x :'b word) = (n2w y :'c word)) <=> (n2w y = x))``)) 433 val _ = s ("r243", Drule.UNDISCH_ALL (bossLib.PROVE 434 [wordsTheory.word_concat_0_eq] ``FINITE univ(:'a) ==> 435 dimindex(:'b) <= dimindex(:'c) ==> y < dimword(:'b) ==> 436 (((n2w y :'c word) = (0w :'a word) @@ (x :'b word)) <=> (x = n2w y))``)) 437 val _ = s ("r244", Drule.UNDISCH_ALL (bossLib.PROVE 438 [wordsTheory.word_concat_0_eq] ``FINITE univ(:'a) ==> 439 dimindex(:'b) <= dimindex(:'c) ==> y < dimword(:'b) ==> 440 (((n2w y :'c word) = (0w :'a word) @@ (x :'b word)) <=> (n2w y = x))``)) 441 442 val _ = s ("r245", W ``x && y = y && x``) 443 val _ = s ("r246", W ``x && y && z = y && x && z``) 444 val _ = s ("r247", W ``x && y && z = (x && y) && z``) 445 val _ = s ("r248", W ``(1w = (x :word1) && y) <=> (1w = x) /\ (1w = y)``) 446 val _ = s ("r249", W ``(1w = (x :word1) && y) <=> (1w = y) /\ (1w = x)``) 447 val _ = s ("r250", W ``(7 >< 0) (x :word8) = x``) 448 val _ = s ("r251", W ``x <+ y <=> ~(y <=+ x)``) 449 val _ = s ("r252", W ``(x :'a word) * y = y * x``) 450 val _ = s ("r253", W ``(0 >< 0) (x :word1) = x``) 451 val _ = s ("r254", W ``(x && y) && z = x && y && z``) 452 val _ = s ("r255", W ``0w || x = x``) 453 454 (* used for Z3's proof rule th_lemma *) 455 456 val _ = s ("t001", U [boolTheory.EQ_SYM_EQ, combinTheory.UPDATE_def] 457 ``(x = y) \/ (f x = (y =+ z) f x)``) 458 val _ = s ("t002", U [boolTheory.EQ_SYM_EQ, combinTheory.UPDATE_def] 459 ``(x = y) \/ (f y = (x =+ z) f y)``) 460 val _ = s ("t003", U [boolTheory.EQ_SYM_EQ, combinTheory.UPDATE_def] 461 ``(x = y) \/ ((y =+ z) f x = f x)``) 462 val _ = s ("t004", U [boolTheory.EQ_SYM_EQ, combinTheory.UPDATE_def] 463 ``(x = y) \/ ((x =+ z) f y = f y)``) 464 val _ = s ("t005", Tactical.prove 465 (``(f = g) \/ (f (array_ext f g) <> g (array_ext f g))``, 466 Tactical.THEN (Tactic.DISJ_CASES_TAC 467 (Thm.SPEC ``?x. f x <> g x`` boolTheory.EXCLUDED_MIDDLE), 468 Tactical.THEN (Rewrite.REWRITE_TAC [array_ext_def], 469 bossLib.METIS_TAC [])))) 470 471 val _ = s ("t006", A ``((x :int) <> y) \/ (x <= y)``) 472 val _ = s ("t007", A ``((x :int) <> y) \/ (x >= y)``) 473 val _ = s ("t008", A ``((x :int) <> y) \/ (x + -1 * y >= 0)``) 474 val _ = s ("t009", A ``((x :int) <> y) \/ (x + -1 * y <= 0)``) 475 val _ = s ("t010", A ``((x :int) = y) \/ ~(x <= y) \/ ~(x >= y)``) 476 val _ = s ("t011", A ``~((x :int) <= 0) \/ x <= 1``) 477 val _ = s ("t012", A ``~((x :int) <= -1) \/ x <= 0``) 478 val _ = s ("t013", A ``~((x :int) >= 0) \/ x >= -1``) 479 val _ = s ("t014", A ``~((x :int) >= 0) \/ ~(x <= -1)``) 480 val _ = s ("t015", A ``(x :int) >= y \/ x <= y``) 481 482 val _ = s ("t016", R ``(x :real) <> y \/ x + -1 * y >= 0``) 483 484 val _ = s ("t017", Tactical.prove (``(x :'a word) <> ~x``, 485 let 486 val RW = bossLib.RW_TAC (bossLib.++ (bossLib.bool_ss, fcpLib.FCP_ss)) 487 in 488 Tactical.THEN (RW [], 489 Tactical.THEN (Tactic.EXISTS_TAC ``0 :num``, 490 Tactical.THEN (RW [wordsTheory.DIMINDEX_GT_0, 491 wordsTheory.word_1comp_def], 492 tautLib.TAUT_TAC))) 493 end)) 494 val _ = s ("t018", W ``(x = y) ==> x ' i ==> y ' i``) 495 val _ = s ("t019", S ``(1w = ~(x :word1)) \/ x ' 0``) 496 val _ = s ("t020", S ``(x :word1) ' 0 ==> (0w = ~x)``) 497 val _ = s ("t021", S ``(x :word1) ' 0 ==> (1w = x)``) 498 val _ = s ("t022", S ``~((x :word1) ' 0) ==> (0w = x)``) 499 val _ = s ("t023", S ``~((x :word1) ' 0) ==> (1w = ~x)``) 500 val _ = s ("t024", S ``(0w = ~(x :word1)) \/ ~(x ' 0)``) 501 val _ = s ("t025", U [] 502 ``(1w = ~(x :word1) || ~y) \/ ~(~(x ' 0) \/ ~(y ' 0))``) 503 val _ = s ("t026", U [] 504 ``(0w = (x :word8)) \/ x ' 0 \/ x ' 1 \/ x ' 2 \/ x ' 3 \/ x ' 4 \/ x ' 5 \/ x ' 6 \/ x ' 7``) 505 val _ = s ("t027", S 506 ``(((x :word1) = 1w) <=> p) <=> (x = if p then 1w else 0w)``) 507 val _ = s ("t028", S 508 ``((1w = (x :word1)) <=> p) <=> (x = if p then 1w else 0w)``) 509 val _ = s ("t029", S 510 ``(p <=> ((x :word1) = 1w)) <=> (x = if p then 1w else 0w)``) 511 val _ = s ("t030", S 512 ``(p <=> (1w = (x :word1))) <=> (x = if p then 1w else 0w)``) 513 val _ = s ("t031", B 514 ``(0w:word32 = 0xFFFFFFFFw * sw2sw (x :word8)) ==> ~(x ' 0)``) 515 val _ = s ("t032", B 516 ``(0w:word32 = 0xFFFFFFFFw * sw2sw (x :word8)) ==> ~(x ' 1 <=> ~(x ' 0))``) 517 val _ = s ("t033", B ``(0w:word32 = 0xFFFFFFFFw * sw2sw (x :word8)) ==> 518 ~(x ' 2 <=> ~(x ' 0) /\ ~(x ' 1))``) 519 val _ = s ("t034", 520 bossLib.METIS_PROVE [simpLib.SIMP_PROVE bossLib.bool_ss 521 [wordsTheory.WORD_ADD_BIT0, wordsLib.WORD_DECIDE ``1w :'a word ' 0``] 522 ``x ' 0 ==> ~(1w + (x :'a word)) ' 0``] 523 ``(1w + (x :'a word) = y) ==> x ' 0 ==> ~(y ' 0)``) 524 val _ = s ("t035", S ``(1w = x :word1) \/ (0 >< 0) x <> (1w :word1)``) 525 526 (* used to prove hypotheses of other proforma theorems (recursively) *) 527 528 val _ = s ("p001", wordsTheory.ZERO_LT_dimword) (* ``0 < dimword(:'a)`` *) 529 val _ = s ("p002", wordsTheory.ONE_LT_dimword) (* ``1 < dimword(:'a)`` *) 530 val _ = s ("p003", S ``255 < dimword (:8)``) 531 val _ = s ("p004", S ``FINITE univ(:unit)``) 532 val _ = s ("p005", S ``FINITE univ(:16)``) 533 val _ = s ("p006", S ``FINITE univ(:24)``) 534 val _ = s ("p007", S ``FINITE univ(:30)``) 535 val _ = s ("p008", S ``FINITE univ(:31)``) 536 val _ = s ("p009", S ``dimindex (:8) <= dimindex (:32)``) 537 538 val _ = Theory.export_theory () 539