isabelle: src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy@3cc55085d490 (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
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 66992 diff changeset	13	spark_open \<open>simple_greatest_common_divisor/g_c_d\<close>
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
	Sat, 01 Apr 2023 19:15:38 +0200
changeset 77775	3cc55085d490
parent 69605	a96320074298
permissions	-rw-r--r--