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 \<open>simple_greatest_common_divisor/g_c_d\<close> 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