|
41561
|
1 |
(* Title: HOL/SPARK/Examples/Sqrt/Sqrt.thy
|
|
|
2 |
Author: Stefan Berghofer
|
|
|
3 |
Copyright: secunet Security Networks AG
|
|
|
4 |
*)
|
|
|
5 |
|
|
|
6 |
theory Sqrt
|
|
|
7 |
imports SPARK
|
|
|
8 |
begin
|
|
|
9 |
|
|
|
10 |
spark_open "sqrt/isqrt.siv"
|
|
|
11 |
|
|
|
12 |
spark_vc function_isqrt_4
|
|
|
13 |
proof -
|
|
|
14 |
from `0 \<le> r` have "(r = 0 \<or> r = 1 \<or> r = 2) \<or> 2 < r" by auto
|
|
|
15 |
then show "2 * r \<le> 2147483646"
|
|
|
16 |
proof
|
|
|
17 |
assume "2 < r"
|
|
|
18 |
then have "0 < r" by simp
|
|
|
19 |
with `2 < r` have "2 * r < r * r" by (rule mult_strict_right_mono)
|
|
|
20 |
with `r * r \<le> n` and `n \<le> 2147483647` show ?thesis
|
|
|
21 |
by simp
|
|
|
22 |
qed auto
|
|
|
23 |
then show "2 * r \<le> 2147483647" by simp
|
|
|
24 |
qed
|
|
|
25 |
|
|
|
26 |
spark_end
|
|
|
27 |
|
|
|
28 |
end
|