author | wenzelm |
Sun, 06 Jan 2019 15:04:34 +0100 | |
changeset 69605 | a96320074298 |
parent 66992 | 69673025292e |
permissions | -rw-r--r-- |
41561 | 1 |
(* Title: HOL/SPARK/Examples/Sqrt/Sqrt.thy |
2 |
Author: Stefan Berghofer |
|
3 |
Copyright: secunet Security Networks AG |
|
4 |
*) |
|
5 |
||
6 |
theory Sqrt |
|
66992
69673025292e
less global theories -- avoid confusion about special cases;
wenzelm
parents:
66453
diff
changeset
|
7 |
imports "HOL-SPARK.SPARK" |
41561 | 8 |
begin |
9 |
||
69605 | 10 |
spark_open \<open>sqrt/isqrt\<close> |
41561 | 11 |
|
12 |
spark_vc function_isqrt_4 |
|
13 |
proof - |
|
63167 | 14 |
from \<open>0 \<le> r\<close> have "(r = 0 \<or> r = 1 \<or> r = 2) \<or> 2 < r" by auto |
41561 | 15 |
then show "2 * r \<le> 2147483646" |
16 |
proof |
|
17 |
assume "2 < r" |
|
18 |
then have "0 < r" by simp |
|
63167 | 19 |
with \<open>2 < r\<close> have "2 * r < r * r" by (rule mult_strict_right_mono) |
20 |
with \<open>r * r \<le> n\<close> and \<open>n \<le> 2147483647\<close> show ?thesis |
|
41561 | 21 |
by simp |
22 |
qed auto |
|
23 |
then show "2 * r \<le> 2147483647" by simp |
|
24 |
qed |
|
25 |
||
26 |
spark_end |
|
27 |
||
28 |
end |