Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/SPARK/Examples/Sqrt/Sqrt.thy
author wenzelm
Mon, 11 Feb 2013 14:39:04 +0100
changeset 51085 d90218288d51
parent 41561 d1318f3c86ba
child 56798 939e88e79724
permissions -rw-r--r--
make WWW_Find work again, now that its ML modules reside within a theory context (cf. bf5b45870110) -- patch by Rafal Kolanski;

(*  Title:      HOL/SPARK/Examples/Sqrt/Sqrt.thy
    Author:     Stefan Berghofer
    Copyright:  secunet Security Networks AG
*)

theory Sqrt
imports SPARK
begin

spark_open "sqrt/isqrt.siv"

spark_vc function_isqrt_4
proof -
  from `0 \<le> r` have "(r = 0 \<or> r = 1 \<or> r = 2) \<or> 2 < r" by auto
  then show "2 * r \<le> 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 \<le> n` and `n \<le> 2147483647` show ?thesis
      by simp
  qed auto
  then show "2 * r \<le> 2147483647" by simp
qed

spark_end

end
isabelle