isabelle: src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy@cd8ab1a7a286 (annotated)

45610 11095c312709 tuned header; wenzelm parents: 45065 diff changeset	1	(* Title: HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy
45044 2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	2	Author: Stefan Berghofer
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	3	Copyright: secunet Security Networks AG
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	4	*)
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	5
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	6	theory Simple_Greatest_Common_Divisor
66992 69673025292e less global theories -- avoid confusion about special cases; wenzelm parents: 66453 diff changeset	7	imports "HOL-SPARK.SPARK"
45044 2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	8	begin
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	9
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	10	spark_proof_functions
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	11	gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	12
56798 939e88e79724 Discontinued old spark_open; spark_open_siv is now spark_open berghofe parents: 45610 diff changeset	13	spark_open "simple_greatest_common_divisor/g_c_d"
45044 2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	14
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	15	spark_vc procedure_g_c_d_4
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58130 diff changeset	16	using \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close>
45044 2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	17	by (simp add: gcd_non_0_int)
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	18
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	19	spark_vc procedure_g_c_d_9
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58130 diff changeset	20	using \<open>0 \<le> c\<close> \<open>gcd c 0 = gcd m n\<close>
45044 2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	21	by simp
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	22
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	23	spark_end
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	24
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	25	end

author	wenzelm
	Sun, 27 May 2018 22:37:08 +0200
changeset 68300	cd8ab1a7a286
parent 66992	69673025292e
child 69605	a96320074298
permissions	-rw-r--r--