| author | wenzelm |
| Mon, 13 Apr 2020 22:08:14 +0200 | |
| changeset 71751 | abf3e80bd815 |
| parent 69605 | a96320074298 |
| permissions | -rw-r--r-- |
| 45610 | 1 |
(* Title: HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy |
| 45044 | 2 |
Author: Stefan Berghofer |
3 |
Copyright: secunet Security Networks AG |
|
4 |
*) |
|
5 |
||
6 |
theory Simple_Greatest_Common_Divisor |
|
|
66992
69673025292e
less global theories -- avoid confusion about special cases;
wenzelm
parents:
66453
diff
changeset
|
7 |
imports "HOL-SPARK.SPARK" |
| 45044 | 8 |
begin |
9 |
||
10 |
spark_proof_functions |
|
11 |
gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int" |
|
12 |
||
| 69605 | 13 |
spark_open \<open>simple_greatest_common_divisor/g_c_d\<close> |
| 45044 | 14 |
|
15 |
spark_vc procedure_g_c_d_4 |
|
| 63167 | 16 |
using \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> |
| 45044 | 17 |
by (simp add: gcd_non_0_int) |
18 |
||
19 |
spark_vc procedure_g_c_d_9 |
|
| 63167 | 20 |
using \<open>0 \<le> c\<close> \<open>gcd c 0 = gcd m n\<close> |
| 45044 | 21 |
by simp |
22 |
||
23 |
spark_end |
|
24 |
||
25 |
end |