1(*  Title:      HOL/SPARK/Examples/Sqrt/Sqrt.thy
2    Author:     Stefan Berghofer
3    Copyright:  secunet Security Networks AG
4*)
5
6theory Sqrt
7imports "HOL-SPARK.SPARK"
8begin
9
10spark_open \<open>sqrt/isqrt\<close>
11
12spark_vc function_isqrt_4
13proof -
14  from \<open>0 \<le> r\<close> 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 \<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
21      by simp
22  qed auto
23  then show "2 * r \<le> 2147483647" by simp
24qed
25
26spark_end
27
28end
29