25422
|
1 |
(* Title: HOL/Extraction/Greatest_Common_Divisor.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Stefan Berghofer, TU Muenchen
|
|
4 |
Helmut Schwichtenberg, LMU Muenchen
|
|
5 |
*)
|
|
6 |
|
|
7 |
header {* Greatest common divisor *}
|
|
8 |
|
|
9 |
theory Greatest_Common_Divisor
|
|
10 |
imports QuotRem
|
|
11 |
begin
|
|
12 |
|
|
13 |
theorem greatest_common_divisor:
|
|
14 |
"\<And>n::nat. Suc m < n \<Longrightarrow> \<exists>k n1 m1. k * n1 = n \<and> k * m1 = Suc m \<and>
|
|
15 |
(\<forall>l l1 l2. l * l1 = n \<longrightarrow> l * l2 = Suc m \<longrightarrow> l \<le> k)"
|
|
16 |
proof (induct m rule: nat_wf_ind)
|
|
17 |
case (1 m n)
|
|
18 |
from division obtain r q where h1: "n = Suc m * q + r" and h2: "r \<le> m"
|
|
19 |
by iprover
|
|
20 |
show ?case
|
|
21 |
proof (cases r)
|
|
22 |
case 0
|
|
23 |
with h1 have "Suc m * q = n" by simp
|
|
24 |
moreover have "Suc m * 1 = Suc m" by simp
|
|
25 |
moreover {
|
|
26 |
fix l2 have "\<And>l l1. l * l1 = n \<Longrightarrow> l * l2 = Suc m \<Longrightarrow> l \<le> Suc m"
|
|
27 |
by (cases l2) simp_all }
|
|
28 |
ultimately show ?thesis by iprover
|
|
29 |
next
|
|
30 |
case (Suc nat)
|
|
31 |
with h2 have h: "nat < m" by simp
|
|
32 |
moreover from h have "Suc nat < Suc m" by simp
|
|
33 |
ultimately have "\<exists>k m1 r1. k * m1 = Suc m \<and> k * r1 = Suc nat \<and>
|
|
34 |
(\<forall>l l1 l2. l * l1 = Suc m \<longrightarrow> l * l2 = Suc nat \<longrightarrow> l \<le> k)"
|
|
35 |
by (rule 1)
|
|
36 |
then obtain k m1 r1 where
|
|
37 |
h1': "k * m1 = Suc m"
|
|
38 |
and h2': "k * r1 = Suc nat"
|
|
39 |
and h3': "\<And>l l1 l2. l * l1 = Suc m \<Longrightarrow> l * l2 = Suc nat \<Longrightarrow> l \<le> k"
|
|
40 |
by iprover
|
|
41 |
have mn: "Suc m < n" by (rule 1)
|
|
42 |
from h1 h1' h2' Suc have "k * (m1 * q + r1) = n"
|
|
43 |
by (simp add: add_mult_distrib2 nat_mult_assoc [symmetric])
|
|
44 |
moreover have "\<And>l l1 l2. l * l1 = n \<Longrightarrow> l * l2 = Suc m \<Longrightarrow> l \<le> k"
|
|
45 |
proof -
|
|
46 |
fix l l1 l2
|
|
47 |
assume ll1n: "l * l1 = n"
|
|
48 |
assume ll2m: "l * l2 = Suc m"
|
|
49 |
moreover have "l * (l1 - l2 * q) = Suc nat"
|
|
50 |
by (simp add: diff_mult_distrib2 h1 Suc [symmetric] mn ll1n ll2m [symmetric])
|
|
51 |
ultimately show "l \<le> k" by (rule h3')
|
|
52 |
qed
|
|
53 |
ultimately show ?thesis using h1' by iprover
|
|
54 |
qed
|
|
55 |
qed
|
|
56 |
|
|
57 |
extract greatest_common_divisor
|
|
58 |
|
|
59 |
text {*
|
|
60 |
The extracted program for computing the greatest common divisor is
|
|
61 |
@{thm [display] greatest_common_divisor_def}
|
|
62 |
*}
|
|
63 |
|
27982
|
64 |
instantiation nat :: default
|
|
65 |
begin
|
|
66 |
|
|
67 |
definition "default = (0::nat)"
|
|
68 |
|
|
69 |
instance ..
|
25422
|
70 |
|
27982
|
71 |
end
|
25422
|
72 |
|
27982
|
73 |
instantiation * :: (default, default) default
|
|
74 |
begin
|
|
75 |
|
|
76 |
definition "default = (default, default)"
|
|
77 |
|
|
78 |
instance ..
|
25422
|
79 |
|
|
80 |
end
|
27982
|
81 |
|
|
82 |
instantiation "fun" :: (type, default) default
|
|
83 |
begin
|
|
84 |
|
|
85 |
definition "default = (\<lambda>x. default)"
|
|
86 |
|
|
87 |
instance ..
|
|
88 |
|
|
89 |
end
|
|
90 |
|
|
91 |
consts_code
|
|
92 |
default ("(error \"default\")")
|
|
93 |
|
|
94 |
lemma "greatest_common_divisor 7 12 = (4, 3, 2)" by evaluation
|
|
95 |
lemma "greatest_common_divisor 7 12 = (4, 3, 2)" by eval
|
|
96 |
|
|
97 |
end
|