1(* Title: HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy 2 Author: Stefan Berghofer 3 Copyright: secunet Security Networks AG 4*) 5 6theory Greatest_Common_Divisor 7imports "HOL-SPARK.SPARK" 8begin 9 10spark_proof_functions 11 gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int" 12 13spark_open \<open>greatest_common_divisor/g_c_d\<close> 14 15spark_vc procedure_g_c_d_4 16proof - 17 from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign) 18 with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1 19 by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric]) 20next 21 from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> show ?C2 22 by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric] gcd_non_0_int) 23qed 24 25spark_vc procedure_g_c_d_11 26proof - 27 from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d = 0\<close> 28 have "d dvd c" 29 by (auto simp add: sdiv_pos_pos dvd_def ac_simps) 30 with \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> show ?C1 31 by simp 32qed 33 34spark_end 35 36end 37