isabelle: src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy@ded1c636aece (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
65552 f533820e7248 theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications; wenzelm parents: 63167 diff changeset	7	imports "../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
	Wed, 07 Jun 2017 23:23:48 +0200
changeset 66034	ded1c636aece
parent 65552	f533820e7248
child 66453	cc19f7ca2ed6
permissions	-rw-r--r--