src/HOL/SPARK/Examples/Sqrt/Sqrt.thy
author wenzelm
Fri, 03 Nov 2017 13:43:31 +0100
changeset 66992 69673025292e
parent 66453 cc19f7ca2ed6
child 69605 a96320074298
permissions -rw-r--r--
less global theories -- avoid confusion about special cases;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     1
(*  Title:      HOL/SPARK/Examples/Sqrt/Sqrt.thy
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     2
    Author:     Stefan Berghofer
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     3
    Copyright:  secunet Security Networks AG
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     4
*)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     5
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     6
theory Sqrt
66992
69673025292e less global theories -- avoid confusion about special cases;
wenzelm
parents: 66453
diff changeset
     7
imports "HOL-SPARK.SPARK"
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     8
begin
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     9
56798
939e88e79724 Discontinued old spark_open; spark_open_siv is now spark_open
berghofe
parents: 41561
diff changeset
    10
spark_open "sqrt/isqrt"
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    11
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    12
spark_vc function_isqrt_4
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    13
proof -
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 58130
diff changeset
    14
  from \<open>0 \<le> r\<close> have "(r = 0 \<or> r = 1 \<or> r = 2) \<or> 2 < r" by auto
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    15
  then show "2 * r \<le> 2147483646"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    16
  proof
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    17
    assume "2 < r"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    18
    then have "0 < r" by simp
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 58130
diff changeset
    19
    with \<open>2 < r\<close> have "2 * r < r * r" by (rule mult_strict_right_mono)
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 58130
diff changeset
    20
    with \<open>r * r \<le> n\<close> and \<open>n \<le> 2147483647\<close> show ?thesis
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    21
      by simp
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    22
  qed auto
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    23
  then show "2 * r \<le> 2147483647" by simp
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    24
qed
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    25
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    26
spark_end
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    27
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    28
end