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