isabelle: src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy@74202654e4ee (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
58130 5e9170812356 ported to use new-style datatypes blanchet parents: 56798 diff changeset	7	imports "../SPARK" GCD
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
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	16	using `0 < d` `gcd c d = gcd m n`
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
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	20	using `0 \<le> c` `gcd c 0 = gcd m n`
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	blanchet
	Tue, 06 Jan 2015 09:59:43 +0100
changeset 59299	74202654e4ee
parent 58130	5e9170812356
child 63167	0909deb8059b
permissions	-rw-r--r--