author | haftmann |
Sun, 16 Oct 2016 09:31:06 +0200 | |
changeset 64246 | 15d1ee6e847b |
parent 63167 | 0909deb8059b |
child 65552 | f533820e7248 |
permissions | -rw-r--r-- |
41561 | 1 |
(* Title: HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy |
2 |
Author: Stefan Berghofer |
|
3 |
Copyright: secunet Security Networks AG |
|
4 |
*) |
|
5 |
||
6 |
theory Greatest_Common_Divisor |
|
58130 | 7 |
imports "../../SPARK" GCD |
41561 | 8 |
begin |
9 |
||
10 |
spark_proof_functions |
|
11 |
gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int" |
|
12 |
||
56798
939e88e79724
Discontinued old spark_open; spark_open_siv is now spark_open
berghofe
parents:
41561
diff
changeset
|
13 |
spark_open "greatest_common_divisor/g_c_d" |
41561 | 14 |
|
15 |
spark_vc procedure_g_c_d_4 |
|
16 |
proof - |
|
63167 | 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 |
|
64246 | 19 |
by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric]) |
41561 | 20 |
next |
63167 | 21 |
from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> show ?C2 |
64246 | 22 |
by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric] gcd_non_0_int) |
41561 | 23 |
qed |
24 |
||
25 |
spark_vc procedure_g_c_d_11 |
|
26 |
proof - |
|
63167 | 27 |
from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d = 0\<close> |
41561 | 28 |
have "d dvd c" |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
56798
diff
changeset
|
29 |
by (auto simp add: sdiv_pos_pos dvd_def ac_simps) |
63167 | 30 |
with \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> show ?C1 |
41561 | 31 |
by simp |
32 |
qed |
|
33 |
||
34 |
spark_end |
|
35 |
||
36 |
end |