334 "x = x div 3 * 3 + x mod 3" |
334 "x = x div 3 * 3 + x mod 3" |
335 using [[z3_extensions]] |
335 using [[z3_extensions]] |
336 by smt+ |
336 by smt+ |
337 |
337 |
338 lemma |
338 lemma |
339 "abs (x::int) \<ge> 0" |
339 "\<bar>x::int\<bar> \<ge> 0" |
340 "(abs x = 0) = (x = 0)" |
340 "(\<bar>x\<bar> = 0) = (x = 0)" |
341 "(x \<ge> 0) = (abs x = x)" |
341 "(x \<ge> 0) = (\<bar>x\<bar> = x)" |
342 "(x \<le> 0) = (abs x = -x)" |
342 "(x \<le> 0) = (\<bar>x\<bar> = -x)" |
343 "abs (abs x) = abs x" |
343 "\<bar>\<bar>x\<bar>\<bar> = \<bar>x\<bar>" |
344 by smt+ |
344 by smt+ |
345 |
345 |
346 lemma |
346 lemma |
347 "min (x::int) y \<le> x" |
347 "min (x::int) y \<le> x" |
348 "min x y \<le> y" |
348 "min x y \<le> y" |
349 "z < x \<and> z < y \<longrightarrow> z < min x y" |
349 "z < x \<and> z < y \<longrightarrow> z < min x y" |
350 "min x y = min y x" |
350 "min x y = min y x" |
351 "x \<ge> 0 \<longrightarrow> min x 0 = 0" |
351 "x \<ge> 0 \<longrightarrow> min x 0 = 0" |
352 "min x y \<le> abs (x + y)" |
352 "min x y \<le> \<bar>x + y\<bar>" |
353 by smt+ |
353 by smt+ |
354 |
354 |
355 lemma |
355 lemma |
356 "max (x::int) y \<ge> x" |
356 "max (x::int) y \<ge> x" |
357 "max x y \<ge> y" |
357 "max x y \<ge> y" |
358 "z > x \<and> z > y \<longrightarrow> z > max x y" |
358 "z > x \<and> z > y \<longrightarrow> z > max x y" |
359 "max x y = max y x" |
359 "max x y = max y x" |
360 "x \<ge> 0 \<longrightarrow> max x 0 = x" |
360 "x \<ge> 0 \<longrightarrow> max x 0 = x" |
361 "max x y \<ge> - abs x - abs y" |
361 "max x y \<ge> - \<bar>x\<bar> - \<bar>y\<bar>" |
362 by smt+ |
362 by smt+ |
363 |
363 |
364 lemma |
364 lemma |
365 "0 < (x::int) \<and> x \<le> 1 \<longrightarrow> x = 1" |
365 "0 < (x::int) \<and> x \<le> 1 \<longrightarrow> x = 1" |
366 "x \<le> x" |
366 "x \<le> x" |
446 "x < 0 \<longrightarrow> 2 * x / 3 > x" |
446 "x < 0 \<longrightarrow> 2 * x / 3 > x" |
447 using [[z3_extensions]] |
447 using [[z3_extensions]] |
448 by smt+ |
448 by smt+ |
449 |
449 |
450 lemma |
450 lemma |
451 "abs (x::real) \<ge> 0" |
451 "\<bar>x::real\<bar> \<ge> 0" |
452 "(abs x = 0) = (x = 0)" |
452 "(\<bar>x\<bar> = 0) = (x = 0)" |
453 "(x \<ge> 0) = (abs x = x)" |
453 "(x \<ge> 0) = (\<bar>x\<bar> = x)" |
454 "(x \<le> 0) = (abs x = -x)" |
454 "(x \<le> 0) = (\<bar>x\<bar> = -x)" |
455 "abs (abs x) = abs x" |
455 "\<bar>\<bar>x\<bar>\<bar> = \<bar>x\<bar>" |
456 by smt+ |
456 by smt+ |
457 |
457 |
458 lemma |
458 lemma |
459 "min (x::real) y \<le> x" |
459 "min (x::real) y \<le> x" |
460 "min x y \<le> y" |
460 "min x y \<le> y" |
461 "z < x \<and> z < y \<longrightarrow> z < min x y" |
461 "z < x \<and> z < y \<longrightarrow> z < min x y" |
462 "min x y = min y x" |
462 "min x y = min y x" |
463 "x \<ge> 0 \<longrightarrow> min x 0 = 0" |
463 "x \<ge> 0 \<longrightarrow> min x 0 = 0" |
464 "min x y \<le> abs (x + y)" |
464 "min x y \<le> \<bar>x + y\<bar>" |
465 by smt+ |
465 by smt+ |
466 |
466 |
467 lemma |
467 lemma |
468 "max (x::real) y \<ge> x" |
468 "max (x::real) y \<ge> x" |
469 "max x y \<ge> y" |
469 "max x y \<ge> y" |
470 "z > x \<and> z > y \<longrightarrow> z > max x y" |
470 "z > x \<and> z > y \<longrightarrow> z > max x y" |
471 "max x y = max y x" |
471 "max x y = max y x" |
472 "x \<ge> 0 \<longrightarrow> max x 0 = x" |
472 "x \<ge> 0 \<longrightarrow> max x 0 = x" |
473 "max x y \<ge> - abs x - abs y" |
473 "max x y \<ge> - \<bar>x\<bar> - \<bar>y\<bar>" |
474 by smt+ |
474 by smt+ |
475 |
475 |
476 lemma |
476 lemma |
477 "x \<le> (x::real)" |
477 "x \<le> (x::real)" |
478 "x \<le> y \<longrightarrow> 3 * x \<le> 3 * y" |
478 "x \<le> y \<longrightarrow> 3 * x \<le> 3 * y" |