(* Title: HOL/SPARK/Examples/Sqrt/Sqrt.thy Author: Stefan Berghofer Copyright: secunet Security Networks AG *) theory Sqrt imports "HOL-SPARK.SPARK" begin spark_open ‹sqrt/isqrt› spark_vc function_isqrt_4 proof - from ‹0 ≤ r› have "(r = 0 ∨ r = 1 ∨ r = 2) ∨ 2 < r" by auto then show "2 * r ≤ 2147483646" proof assume "2 < r" then have "0 < r" by simp with ‹2 < r› have "2 * r < r * r" by (rule mult_strict_right_mono) with ‹r * r ≤ n› and ‹n ≤ 2147483647› show ?thesis by simp qed auto then show "2 * r ≤ 2147483647" by simp qed spark_end end