1(*  Title:      HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy
2    Author:     Stefan Berghofer
3    Copyright:  secunet Security Networks AG
4*)
5
6theory Simple_Greatest_Common_Divisor
7imports "HOL-SPARK.SPARK"
8begin
9
10spark_proof_functions
11  gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"
12
13spark_open "simple_greatest_common_divisor/g_c_d"
14
15spark_vc procedure_g_c_d_4
16  using \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close>
17  by (simp add: gcd_non_0_int)
18
19spark_vc procedure_g_c_d_9
20  using \<open>0 \<le> c\<close> \<open>gcd c 0 = gcd m n\<close>
21  by simp
22
23spark_end
24
25end
26