src/HOL/SMT_Examples/SMT_Examples.thy
 author huffman Sun Apr 01 16:09:58 2012 +0200 (2012-04-01) changeset 47255 30a1692557b0 parent 47155 ade3fc826af3 child 48069 e9b2782c4f99 permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
 boehmes@36899 1 (* Title: HOL/SMT_Examples/SMT_Examples.thy boehmes@36898 2 Author: Sascha Boehme, TU Muenchen boehmes@36898 3 *) boehmes@36898 4 boehmes@36899 5 header {* Examples for the SMT binding *} boehmes@36898 6 boehmes@36898 7 theory SMT_Examples boehmes@36899 8 imports Complex_Main boehmes@36898 9 begin boehmes@36898 10 blanchet@47152 11 declare [[smt_oracle = false]] blanchet@47152 12 declare [[smt_certificates = "SMT_Examples.certs"]] blanchet@47152 13 declare [[smt_read_only_certificates = true]] boehmes@36898 14 boehmes@36898 15 boehmes@36898 16 boehmes@36898 17 section {* Propositional and first-order logic *} boehmes@36898 18 boehmes@36898 19 lemma "True" by smt boehmes@36898 20 boehmes@36898 21 lemma "p \ \p" by smt boehmes@36898 22 boehmes@36898 23 lemma "(p \ True) = p" by smt boehmes@36898 24 boehmes@36898 25 lemma "(p \ q) \ \p \ q" by smt boehmes@36898 26 boehmes@36898 27 lemma "(a \ b) \ (c \ d) \ (a \ b) \ (c \ d)" boehmes@36898 28 by smt boehmes@36898 29 boehmes@36898 30 lemma "(p1 \ p2) \ p3 \ (p1 \ (p3 \ p2) \ (p1 \ p3)) \ p1" by smt boehmes@36898 31 boehmes@36898 32 lemma "P=P=P=P=P=P=P=P=P=P" by smt boehmes@36898 33 blanchet@46084 34 lemma boehmes@36898 35 assumes "a | b | c | d" boehmes@36898 36 and "e | f | (a & d)" boehmes@36898 37 and "~(a | (c & ~c)) | b" boehmes@36898 38 and "~(b & (x | ~x)) | c" boehmes@36898 39 and "~(d | False) | c" boehmes@36898 40 and "~(c | (~p & (p | (q & ~q))))" boehmes@36898 41 shows False boehmes@36898 42 using assms by smt boehmes@36898 43 boehmes@36898 44 axiomatization symm_f :: "'a \ 'a \ 'a" where boehmes@36898 45 symm_f: "symm_f x y = symm_f y x" boehmes@36898 46 lemma "a = a \ symm_f a b = symm_f b a" by (smt symm_f) boehmes@36898 47 blanchet@46084 48 (* boehmes@36898 49 Taken from ~~/src/HOL/ex/SAT_Examples.thy. boehmes@36898 50 Translated from TPTP problem library: PUZ015-2.006.dimacs boehmes@36898 51 *) blanchet@46084 52 lemma boehmes@36898 53 assumes "~x0" boehmes@36898 54 and "~x30" boehmes@36898 55 and "~x29" boehmes@36898 56 and "~x59" boehmes@36898 57 and "x1 | x31 | x0" boehmes@36898 58 and "x2 | x32 | x1" boehmes@36898 59 and "x3 | x33 | x2" boehmes@36898 60 and "x4 | x34 | x3" boehmes@36898 61 and "x35 | x4" boehmes@36898 62 and "x5 | x36 | x30" boehmes@36898 63 and "x6 | x37 | x5 | x31" boehmes@36898 64 and "x7 | x38 | x6 | x32" boehmes@36898 65 and "x8 | x39 | x7 | x33" boehmes@36898 66 and "x9 | x40 | x8 | x34" boehmes@36898 67 and "x41 | x9 | x35" boehmes@36898 68 and "x10 | x42 | x36" boehmes@36898 69 and "x11 | x43 | x10 | x37" boehmes@36898 70 and "x12 | x44 | x11 | x38" boehmes@36898 71 and "x13 | x45 | x12 | x39" boehmes@36898 72 and "x14 | x46 | x13 | x40" boehmes@36898 73 and "x47 | x14 | x41" boehmes@36898 74 and "x15 | x48 | x42" boehmes@36898 75 and "x16 | x49 | x15 | x43" boehmes@36898 76 and "x17 | x50 | x16 | x44" boehmes@36898 77 and "x18 | x51 | x17 | x45" boehmes@36898 78 and "x19 | x52 | x18 | x46" boehmes@36898 79 and "x53 | x19 | x47" boehmes@36898 80 and "x20 | x54 | x48" boehmes@36898 81 and "x21 | x55 | x20 | x49" boehmes@36898 82 and "x22 | x56 | x21 | x50" boehmes@36898 83 and "x23 | x57 | x22 | x51" boehmes@36898 84 and "x24 | x58 | x23 | x52" boehmes@36898 85 and "x59 | x24 | x53" boehmes@36898 86 and "x25 | x54" boehmes@36898 87 and "x26 | x25 | x55" boehmes@36898 88 and "x27 | x26 | x56" boehmes@36898 89 and "x28 | x27 | x57" boehmes@36898 90 and "x29 | x28 | x58" boehmes@36898 91 and "~x1 | ~x31" boehmes@36898 92 and "~x1 | ~x0" boehmes@36898 93 and "~x31 | ~x0" boehmes@36898 94 and "~x2 | ~x32" boehmes@36898 95 and "~x2 | ~x1" boehmes@36898 96 and "~x32 | ~x1" boehmes@36898 97 and "~x3 | ~x33" boehmes@36898 98 and "~x3 | ~x2" boehmes@36898 99 and "~x33 | ~x2" boehmes@36898 100 and "~x4 | ~x34" boehmes@36898 101 and "~x4 | ~x3" boehmes@36898 102 and "~x34 | ~x3" boehmes@36898 103 and "~x35 | ~x4" boehmes@36898 104 and "~x5 | ~x36" boehmes@36898 105 and "~x5 | ~x30" boehmes@36898 106 and "~x36 | ~x30" boehmes@36898 107 and "~x6 | ~x37" boehmes@36898 108 and "~x6 | ~x5" boehmes@36898 109 and "~x6 | ~x31" boehmes@36898 110 and "~x37 | ~x5" boehmes@36898 111 and "~x37 | ~x31" boehmes@36898 112 and "~x5 | ~x31" boehmes@36898 113 and "~x7 | ~x38" boehmes@36898 114 and "~x7 | ~x6" boehmes@36898 115 and "~x7 | ~x32" boehmes@36898 116 and "~x38 | ~x6" boehmes@36898 117 and "~x38 | ~x32" boehmes@36898 118 and "~x6 | ~x32" boehmes@36898 119 and "~x8 | ~x39" boehmes@36898 120 and "~x8 | ~x7" boehmes@36898 121 and "~x8 | ~x33" boehmes@36898 122 and "~x39 | ~x7" boehmes@36898 123 and "~x39 | ~x33" boehmes@36898 124 and "~x7 | ~x33" boehmes@36898 125 and "~x9 | ~x40" boehmes@36898 126 and "~x9 | ~x8" boehmes@36898 127 and "~x9 | ~x34" boehmes@36898 128 and "~x40 | ~x8" boehmes@36898 129 and "~x40 | ~x34" boehmes@36898 130 and "~x8 | ~x34" boehmes@36898 131 and "~x41 | ~x9" boehmes@36898 132 and "~x41 | ~x35" boehmes@36898 133 and "~x9 | ~x35" boehmes@36898 134 and "~x10 | ~x42" boehmes@36898 135 and "~x10 | ~x36" boehmes@36898 136 and "~x42 | ~x36" boehmes@36898 137 and "~x11 | ~x43" boehmes@36898 138 and "~x11 | ~x10" boehmes@36898 139 and "~x11 | ~x37" boehmes@36898 140 and "~x43 | ~x10" boehmes@36898 141 and "~x43 | ~x37" boehmes@36898 142 and "~x10 | ~x37" boehmes@36898 143 and "~x12 | ~x44" boehmes@36898 144 and "~x12 | ~x11" boehmes@36898 145 and "~x12 | ~x38" boehmes@36898 146 and "~x44 | ~x11" boehmes@36898 147 and "~x44 | ~x38" boehmes@36898 148 and "~x11 | ~x38" boehmes@36898 149 and "~x13 | ~x45" boehmes@36898 150 and "~x13 | ~x12" boehmes@36898 151 and "~x13 | ~x39" boehmes@36898 152 and "~x45 | ~x12" boehmes@36898 153 and "~x45 | ~x39" boehmes@36898 154 and "~x12 | ~x39" boehmes@36898 155 and "~x14 | ~x46" boehmes@36898 156 and "~x14 | ~x13" boehmes@36898 157 and "~x14 | ~x40" boehmes@36898 158 and "~x46 | ~x13" boehmes@36898 159 and "~x46 | ~x40" boehmes@36898 160 and "~x13 | ~x40" boehmes@36898 161 and "~x47 | ~x14" boehmes@36898 162 and "~x47 | ~x41" boehmes@36898 163 and "~x14 | ~x41" boehmes@36898 164 and "~x15 | ~x48" boehmes@36898 165 and "~x15 | ~x42" boehmes@36898 166 and "~x48 | ~x42" boehmes@36898 167 and "~x16 | ~x49" boehmes@36898 168 and "~x16 | ~x15" boehmes@36898 169 and "~x16 | ~x43" boehmes@36898 170 and "~x49 | ~x15" boehmes@36898 171 and "~x49 | ~x43" boehmes@36898 172 and "~x15 | ~x43" boehmes@36898 173 and "~x17 | ~x50" boehmes@36898 174 and "~x17 | ~x16" boehmes@36898 175 and "~x17 | ~x44" boehmes@36898 176 and "~x50 | ~x16" boehmes@36898 177 and "~x50 | ~x44" boehmes@36898 178 and "~x16 | ~x44" boehmes@36898 179 and "~x18 | ~x51" boehmes@36898 180 and "~x18 | ~x17" boehmes@36898 181 and "~x18 | ~x45" boehmes@36898 182 and "~x51 | ~x17" boehmes@36898 183 and "~x51 | ~x45" boehmes@36898 184 and "~x17 | ~x45" boehmes@36898 185 and "~x19 | ~x52" boehmes@36898 186 and "~x19 | ~x18" boehmes@36898 187 and "~x19 | ~x46" boehmes@36898 188 and "~x52 | ~x18" boehmes@36898 189 and "~x52 | ~x46" boehmes@36898 190 and "~x18 | ~x46" boehmes@36898 191 and "~x53 | ~x19" boehmes@36898 192 and "~x53 | ~x47" boehmes@36898 193 and "~x19 | ~x47" boehmes@36898 194 and "~x20 | ~x54" boehmes@36898 195 and "~x20 | ~x48" boehmes@36898 196 and "~x54 | ~x48" boehmes@36898 197 and "~x21 | ~x55" boehmes@36898 198 and "~x21 | ~x20" boehmes@36898 199 and "~x21 | ~x49" boehmes@36898 200 and "~x55 | ~x20" boehmes@36898 201 and "~x55 | ~x49" boehmes@36898 202 and "~x20 | ~x49" boehmes@36898 203 and "~x22 | ~x56" boehmes@36898 204 and "~x22 | ~x21" boehmes@36898 205 and "~x22 | ~x50" boehmes@36898 206 and "~x56 | ~x21" boehmes@36898 207 and "~x56 | ~x50" boehmes@36898 208 and "~x21 | ~x50" boehmes@36898 209 and "~x23 | ~x57" boehmes@36898 210 and "~x23 | ~x22" boehmes@36898 211 and "~x23 | ~x51" boehmes@36898 212 and "~x57 | ~x22" boehmes@36898 213 and "~x57 | ~x51" boehmes@36898 214 and "~x22 | ~x51" boehmes@36898 215 and "~x24 | ~x58" boehmes@36898 216 and "~x24 | ~x23" boehmes@36898 217 and "~x24 | ~x52" boehmes@36898 218 and "~x58 | ~x23" boehmes@36898 219 and "~x58 | ~x52" boehmes@36898 220 and "~x23 | ~x52" boehmes@36898 221 and "~x59 | ~x24" boehmes@36898 222 and "~x59 | ~x53" boehmes@36898 223 and "~x24 | ~x53" boehmes@36898 224 and "~x25 | ~x54" boehmes@36898 225 and "~x26 | ~x25" boehmes@36898 226 and "~x26 | ~x55" boehmes@36898 227 and "~x25 | ~x55" boehmes@36898 228 and "~x27 | ~x26" boehmes@36898 229 and "~x27 | ~x56" boehmes@36898 230 and "~x26 | ~x56" boehmes@36898 231 and "~x28 | ~x27" boehmes@36898 232 and "~x28 | ~x57" boehmes@36898 233 and "~x27 | ~x57" boehmes@36898 234 and "~x29 | ~x28" boehmes@36898 235 and "~x29 | ~x58" boehmes@36898 236 and "~x28 | ~x58" boehmes@36898 237 shows False boehmes@36898 238 using assms by smt boehmes@36898 239 boehmes@36898 240 lemma "\x::int. P x \ (\y::int. P x \ P y)" boehmes@36898 241 by smt boehmes@36898 242 blanchet@46084 243 lemma boehmes@36898 244 assumes "(\x y. P x y = x)" boehmes@36898 245 shows "(\y. P x y) = P x c" boehmes@36898 246 using assms by smt boehmes@36898 247 blanchet@46084 248 lemma boehmes@36898 249 assumes "(\x y. P x y = x)" boehmes@36898 250 and "(\x. \y. P x y) = (\x. P x c)" boehmes@36898 251 shows "(EX y. P x y) = P x c" boehmes@36898 252 using assms by smt boehmes@36898 253 boehmes@36898 254 lemma boehmes@36898 255 assumes "if P x then \(\y. P y) else (\y. \P y)" boehmes@36898 256 shows "P x \ P y" boehmes@36898 257 using assms by smt boehmes@36898 258 boehmes@36898 259 boehmes@36898 260 section {* Arithmetic *} boehmes@36898 261 boehmes@36898 262 subsection {* Linear arithmetic over integers and reals *} boehmes@36898 263 boehmes@36898 264 lemma "(3::int) = 3" by smt boehmes@36898 265 boehmes@36898 266 lemma "(3::real) = 3" by smt boehmes@36898 267 boehmes@36898 268 lemma "(3 :: int) + 1 = 4" by smt boehmes@36898 269 boehmes@36898 270 lemma "x + (y + z) = y + (z + (x::int))" by smt boehmes@36898 271 boehmes@36898 272 lemma "max (3::int) 8 > 5" by smt boehmes@36898 273 boehmes@36898 274 lemma "abs (x :: real) + abs y \ abs (x + y)" by smt boehmes@36898 275 boehmes@36898 276 lemma "P ((2::int) < 3) = P True" by smt boehmes@36898 277 boehmes@36898 278 lemma "x + 3 \ 4 \ x < (1::int)" by smt boehmes@36898 279 boehmes@36898 280 lemma boehmes@36898 281 assumes "x \ (3::int)" and "y = x + 4" blanchet@46084 282 shows "y - x > 0" boehmes@36898 283 using assms by smt boehmes@36898 284 boehmes@36898 285 lemma "let x = (2 :: int) in x + x \ 5" by smt boehmes@36898 286 boehmes@36898 287 lemma boehmes@36898 288 fixes x :: real boehmes@36898 289 assumes "3 * x + 7 * a < 4" and "3 < 2 * x" boehmes@36898 290 shows "a < 0" boehmes@36898 291 using assms by smt boehmes@36898 292 boehmes@36898 293 lemma "(0 \ y + -1 * x \ \ 0 \ x \ 0 \ (x::int)) = (\ False)" by smt boehmes@36898 294 boehmes@36898 295 lemma " boehmes@36898 296 (n < m & m < n') | (n < m & m = n') | (n < n' & n' < m) | boehmes@36898 297 (n = n' & n' < m) | (n = m & m < n') | boehmes@36898 298 (n' < m & m < n) | (n' < m & m = n) | boehmes@36898 299 (n' < n & n < m) | (n' = n & n < m) | (n' = m & m < n) | boehmes@36898 300 (m < n & n < n') | (m < n & n' = n) | (m < n' & n' < n) | boehmes@36898 301 (m = n & n < n') | (m = n' & n' < n) | boehmes@36898 302 (n' = m & m = (n::int))" boehmes@36898 303 by smt boehmes@36898 304 blanchet@46084 305 text{* boehmes@36898 306 The following example was taken from HOL/ex/PresburgerEx.thy, where it says: boehmes@36898 307 boehmes@36898 308 This following theorem proves that all solutions to the boehmes@36898 309 recurrence relation \$x_{i+2} = |x_{i+1}| - x_i\$ are periodic with boehmes@36898 310 period 9. The example was brought to our attention by John boehmes@36898 311 Harrison. It does does not require Presburger arithmetic but merely boehmes@36898 312 quantifier-free linear arithmetic and holds for the rationals as well. boehmes@36898 313 blanchet@46084 314 Warning: it takes (in 2006) over 4.2 minutes! boehmes@36898 315 boehmes@36898 316 There, it is proved by "arith". SMT is able to prove this within a fraction boehmes@36898 317 of one second. With proof reconstruction, it takes about 13 seconds on a Core2 boehmes@36898 318 processor. boehmes@36898 319 *} boehmes@36898 320 boehmes@36898 321 lemma "\ x3 = abs x2 - x1; x4 = abs x3 - x2; x5 = abs x4 - x3; boehmes@36898 322 x6 = abs x5 - x4; x7 = abs x6 - x5; x8 = abs x7 - x6; boehmes@36898 323 x9 = abs x8 - x7; x10 = abs x9 - x8; x11 = abs x10 - x9 \ boehmes@36898 324 \ x1 = x10 & x2 = (x11::int)" boehmes@36898 325 by smt boehmes@36898 326 boehmes@36898 327 boehmes@36898 328 lemma "let P = 2 * x + 1 > x + (x::real) in P \ False \ P" by smt boehmes@36898 329 boehmes@37151 330 lemma "x + (let y = x mod 2 in 2 * y + 1) \ x + (1::int)" by smt boehmes@36898 331 boehmes@37151 332 lemma "x + (let y = x mod 2 in y + y) < x + (3::int)" by smt boehmes@36898 333 boehmes@36898 334 lemma boehmes@36898 335 assumes "x \ (0::real)" boehmes@36898 336 shows "x + x \ (let P = (abs x > 1) in if P \ \P then 4 else 2) * x" boehmes@36898 337 using assms by smt boehmes@36898 338 blanchet@46084 339 lemma blanchet@46084 340 assumes "(n + m) mod 2 = 0" and "n mod 4 = 3" blanchet@46084 341 shows "n mod 2 = 1 & m mod 2 = (1::int)" boehmes@37151 342 using assms by smt boehmes@37151 343 boehmes@36898 344 boehmes@36898 345 boehmes@36898 346 subsection {* Linear arithmetic with quantifiers *} boehmes@36898 347 boehmes@36898 348 lemma "~ (\x::int. False)" by smt boehmes@36898 349 boehmes@36898 350 lemma "~ (\x::real. False)" by smt boehmes@36898 351 boehmes@36898 352 lemma "\x::int. 0 < x" boehmes@40163 353 using [[smt_oracle=true]] (* no Z3 proof *) boehmes@36898 354 by smt boehmes@36898 355 boehmes@36898 356 lemma "\x::real. 0 < x" boehmes@40163 357 using [[smt_oracle=true]] (* no Z3 proof *) boehmes@36898 358 by smt boehmes@36898 359 boehmes@36898 360 lemma "\x::int. \y. y > x" boehmes@40163 361 using [[smt_oracle=true]] (* no Z3 proof *) boehmes@36898 362 by smt boehmes@36898 363 boehmes@36898 364 lemma "\x y::int. (x = 0 \ y = 1) \ x \ y" by smt boehmes@36898 365 boehmes@36898 366 lemma "\x::int. \y. x < y \ y < 0 \ y >= 0" by smt boehmes@36898 367 boehmes@36899 368 lemma "\x y::int. x < y \ (2 * x + 1) < (2 * y)" by smt boehmes@36898 369 boehmes@36898 370 lemma "\x y::int. (2 * x + 1) \ (2 * y)" by smt boehmes@36898 371 boehmes@36898 372 lemma "\x y::int. x + y > 2 \ x + y = 2 \ x + y < 2" by smt boehmes@36898 373 boehmes@36898 374 lemma "\x::int. if x > 0 then x + 1 > 0 else 1 > x" by smt boehmes@36898 375 boehmes@36898 376 lemma "if (ALL x::int. x < 0 \ x > 0) then False else True" by smt boehmes@36898 377 boehmes@36898 378 lemma "(if (ALL x::int. x < 0 \ x > 0) then -1 else 3) > (0::int)" by smt boehmes@36898 379 boehmes@36898 380 lemma "~ (\x y z::int. 4 * x + -6 * y = (1::int))" by smt boehmes@36898 381 boehmes@36898 382 lemma "\x::int. \x y. 0 < x \ 0 < y \ (0::int) < x + y" by smt boehmes@36898 383 boehmes@36898 384 lemma "\u::int. \(x::int) y::real. 0 < x \ 0 < y \ -1 < x" by smt boehmes@36898 385 boehmes@36898 386 lemma "\x::int. (\y. y \ x \ y > 0) \ x > 0" by smt boehmes@36898 387 boehmes@37124 388 lemma "\x::int. SMT.trigger [[SMT.pat x]] (x < a \ 2 * x < 2 * a)" by smt boehmes@36898 389 boehmes@42318 390 lemma "\(a::int) b::int. 0 < b \ b < 1" by smt boehmes@42318 391 boehmes@36898 392 boehmes@36898 393 subsection {* Non-linear arithmetic over integers and reals *} boehmes@36898 394 boehmes@36898 395 lemma "a > (0::int) \ a*b > 0 \ b > 0" boehmes@41303 396 using [[smt_oracle=true]] boehmes@41282 397 by smt boehmes@36899 398 boehmes@41282 399 lemma "(a::int) * (x + 1 + y) = a * x + a * (y + 1)" boehmes@41282 400 by smt boehmes@36898 401 boehmes@41282 402 lemma "((x::real) * (1 + y) - x * (1 - y)) = (2 * x * y)" boehmes@41303 403 by smt boehmes@36898 404 boehmes@36898 405 lemma boehmes@36898 406 "(U::int) + (1 + p) * (b + e) + p * d = boehmes@36898 407 U + (2 * (1 + p) * (b + e) + (1 + p) * d + d * p) - (1 + p) * (b + d + e)" boehmes@41303 408 by smt boehmes@36898 409 boehmes@43893 410 lemma [z3_rule]: boehmes@43893 411 fixes x :: "int" boehmes@43893 412 assumes "x * y \ 0" and "\ y \ 0" and "\ x \ 0" boehmes@43893 413 shows False boehmes@43893 414 using assms by (metis mult_le_0_iff) boehmes@43893 415 boehmes@43893 416 lemma "x * y \ (0 :: int) \ x \ 0 \ y \ 0" by smt boehmes@43893 417 boehmes@43893 418 boehmes@36898 419 boehmes@36898 420 subsection {* Linear arithmetic for natural numbers *} boehmes@36898 421 boehmes@36898 422 lemma "2 * (x::nat) ~= 1" by smt boehmes@36898 423 boehmes@36898 424 lemma "a < 3 \ (7::nat) > 2 * a" by smt boehmes@36898 425 boehmes@36898 426 lemma "let x = (1::nat) + y in x - y > 0 * x" by smt boehmes@36898 427 boehmes@36898 428 lemma boehmes@36898 429 "let x = (1::nat) + y in boehmes@36898 430 let P = (if x > 0 then True else False) in boehmes@36898 431 False \ P = (x - 1 = y) \ (\P \ False)" boehmes@36898 432 by smt boehmes@36898 433 boehmes@36898 434 lemma "int (nat \x::int\) = \x\" by smt boehmes@36898 435 boehmes@36898 436 definition prime_nat :: "nat \ bool" where boehmes@36898 437 "prime_nat p = (1 < p \ (\m. m dvd p --> m = 1 \ m = p))" boehmes@36898 438 lemma "prime_nat (4*m + 1) \ m \ (1::nat)" by (smt prime_nat_def) boehmes@36898 439 boehmes@36898 440 boehmes@36898 441 section {* Pairs *} boehmes@36898 442 boehmes@41132 443 lemma "fst (x, y) = a \ x = a" boehmes@41132 444 using fst_conv boehmes@41132 445 by smt boehmes@36898 446 boehmes@41132 447 lemma "p1 = (x, y) \ p2 = (y, x) \ fst p1 = snd p2" boehmes@41132 448 using fst_conv snd_conv boehmes@41132 449 by smt boehmes@36898 450 boehmes@36898 451 boehmes@36898 452 section {* Higher-order problems and recursion *} boehmes@36898 453 boehmes@41132 454 lemma "i \ i1 \ i \ i2 \ (f (i1 := v1, i2 := v2)) i = f i" boehmes@41132 455 using fun_upd_same fun_upd_apply boehmes@41132 456 by smt boehmes@36898 457 boehmes@36898 458 lemma "(f g (x::'a::type) = (g x \ True)) \ (f g x = True) \ (g x = True)" boehmes@36898 459 by smt boehmes@36898 460 blanchet@47111 461 lemma "id x = x \ id True = True" by (smt id_def) boehmes@36898 462 boehmes@41132 463 lemma "i \ i1 \ i \ i2 \ ((f (i1 := v1)) (i2 := v2)) i = f i" boehmes@41132 464 using fun_upd_same fun_upd_apply boehmes@41132 465 by smt boehmes@36898 466 boehmes@41786 467 lemma boehmes@41786 468 "f (\x. g x) \ True" boehmes@41786 469 "f (\x. g x) \ True" boehmes@41786 470 by smt+ boehmes@36899 471 boehmes@42319 472 lemma True using let_rsp by smt boehmes@36899 473 boehmes@42321 474 lemma "le = op \ \ le (3::int) 42" by smt boehmes@42321 475 boehmes@36898 476 lemma "map (\i::nat. i + 1) [0, 1] = [1, 2]" by (smt map.simps) boehmes@36898 477 boehmes@36899 478 boehmes@36898 479 lemma "(ALL x. P x) | ~ All P" by smt boehmes@36898 480 boehmes@36898 481 fun dec_10 :: "nat \ nat" where boehmes@36898 482 "dec_10 n = (if n < 10 then n else dec_10 (n - 10))" boehmes@36898 483 lemma "dec_10 (4 * dec_10 4) = 6" by (smt dec_10.simps) boehmes@36898 484 boehmes@36899 485 boehmes@36898 486 axiomatization boehmes@36898 487 eval_dioph :: "int list \ nat list \ int" boehmes@36898 488 where boehmes@36898 489 eval_dioph_mod: boehmes@36898 490 "eval_dioph ks xs mod int n = eval_dioph ks (map (\x. x mod n) xs) mod int n" boehmes@36898 491 and boehmes@36898 492 eval_dioph_div_mult: boehmes@36898 493 "eval_dioph ks (map (\x. x div n) xs) * int n + boehmes@36898 494 eval_dioph ks (map (\x. x mod n) xs) = eval_dioph ks xs" boehmes@36898 495 lemma boehmes@36898 496 "(eval_dioph ks xs = l) = boehmes@36898 497 (eval_dioph ks (map (\x. x mod 2) xs) mod 2 = l mod 2 \ boehmes@36898 498 eval_dioph ks (map (\x. x div 2) xs) = boehmes@36898 499 (l - eval_dioph ks (map (\x. x mod 2) xs)) div 2)" boehmes@41132 500 using [[smt_oracle=true]] (*FIXME*) boehmes@36898 501 by (smt eval_dioph_mod[where n=2] eval_dioph_div_mult[where n=2]) boehmes@36898 502 boehmes@36898 503 boehmes@45393 504 context complete_lattice boehmes@45393 505 begin boehmes@45393 506 blanchet@46084 507 lemma boehmes@45393 508 assumes "Sup { a | i::bool . True } \ Sup { b | i::bool . True }" boehmes@45393 509 and "Sup { b | i::bool . True } \ Sup { a | i::bool . True }" boehmes@45393 510 shows "Sup { a | i::bool . True } \ Sup { a | i::bool . True }" blanchet@46084 511 using assms by (smt order_trans) boehmes@45393 512 boehmes@45393 513 end boehmes@45393 514 boehmes@45393 515 boehmes@45393 516 boehmes@36898 517 section {* Monomorphization examples *} boehmes@36898 518 boehmes@36899 519 definition Pred :: "'a \ bool" where "Pred x = True" boehmes@36899 520 lemma poly_Pred: "Pred x \ (Pred [x] \ \Pred[x])" by (simp add: Pred_def) boehmes@36899 521 lemma "Pred (1::int)" by (smt poly_Pred) boehmes@36898 522 boehmes@36899 523 axiomatization g :: "'a \ nat" boehmes@36899 524 axiomatization where boehmes@36899 525 g1: "g (Some x) = g [x]" and boehmes@36899 526 g2: "g None = g []" and boehmes@36898 527 g3: "g xs = length xs" boehmes@36898 528 lemma "g (Some (3::int)) = g (Some True)" by (smt g1 g2 g3 list.size) boehmes@36898 529 boehmes@36898 530 end