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