isabelle: src/HOL/SPARK/Examples/Sqrt/Sqrt.thy@64b47495676d (annotated)

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
66453 cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 63167 diff changeset	7	imports 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

author	wenzelm
	Wed, 04 Oct 2017 12:00:53 +0200
changeset 66787	64b47495676d
parent 66453	cc19f7ca2ed6
child 66992	69673025292e
permissions	-rw-r--r--