(* Title: HOL/SPARK/Examples/Sqrt/Sqrt.thy Author: Stefan Berghofer Copyright: secunet Security Networks AG
*)
theory Sqrt imports"HOL-SPARK.SPARK" begin
spark_open \<open>sqrt/isqrt\<close>
spark_vc function_isqrt_4 proof - from\<open>0 \<le> r\<close> have "(r = 0 \<or> r = 1 \<or> r = 2) \<or> 2 < r" by auto thenshow"2 * r \ 2147483646" proof assume"2 < r" thenhave"0 < r"by simp with\<open>2 < r\<close> have "2 * r < r * r" by (rule mult_strict_right_mono) with\<open>r * r \<le> n\<close> and \<open>n \<le> 2147483647\<close> show ?thesis by simp qed auto thenshow"2 * r \ 2147483647" by simp qed
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
