author | wenzelm |
Fri, 01 Jul 2016 16:52:35 +0200 | |
changeset 63361 | d10eab0672f9 |
parent 61986 | 2461779da2b8 |
permissions | -rw-r--r-- |
39157
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
37678
diff
changeset
|
1 |
(* Title: HOL/Proofs/Extraction/Greatest_Common_Divisor.thy |
25422 | 2 |
Author: Stefan Berghofer, TU Muenchen |
39157
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
37678
diff
changeset
|
3 |
Author: Helmut Schwichtenberg, LMU Muenchen |
25422 | 4 |
*) |
5 |
||
61986 | 6 |
section \<open>Greatest common divisor\<close> |
25422 | 7 |
|
8 |
theory Greatest_Common_Divisor |
|
9 |
imports QuotRem |
|
10 |
begin |
|
11 |
||
12 |
theorem greatest_common_divisor: |
|
63361 | 13 |
"\<And>n::nat. Suc m < n \<Longrightarrow> |
14 |
\<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)" |
|
25422 | 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 |
|
63361 | 25 |
moreover have "l * l1 = n \<Longrightarrow> l * l2 = Suc m \<Longrightarrow> l \<le> Suc m" for l l1 l2 |
26 |
by (cases l2) simp_all |
|
25422 | 27 |
ultimately show ?thesis by iprover |
28 |
next |
|
29 |
case (Suc nat) |
|
30 |
with h2 have h: "nat < m" by simp |
|
31 |
moreover from h have "Suc nat < Suc m" by simp |
|
32 |
ultimately have "\<exists>k m1 r1. k * m1 = Suc m \<and> k * r1 = Suc nat \<and> |
|
63361 | 33 |
(\<forall>l l1 l2. l * l1 = Suc m \<longrightarrow> l * l2 = Suc nat \<longrightarrow> l \<le> k)" |
25422 | 34 |
by (rule 1) |
63361 | 35 |
then obtain k m1 r1 where h1': "k * m1 = Suc m" |
25422 | 36 |
and h2': "k * r1 = Suc nat" |
37 |
and h3': "\<And>l l1 l2. l * l1 = Suc m \<Longrightarrow> l * l2 = Suc nat \<Longrightarrow> l \<le> k" |
|
38 |
by iprover |
|
39 |
have mn: "Suc m < n" by (rule 1) |
|
63361 | 40 |
from h1 h1' h2' Suc have "k * (m1 * q + r1) = n" |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
45170
diff
changeset
|
41 |
by (simp add: add_mult_distrib2 mult.assoc [symmetric]) |
63361 | 42 |
moreover have "l \<le> k" if ll1n: "l * l1 = n" and ll2m: "l * l2 = Suc m" for l l1 l2 |
25422 | 43 |
proof - |
63361 | 44 |
have "l * (l1 - l2 * q) = Suc nat" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
27982
diff
changeset
|
45 |
by (simp add: diff_mult_distrib2 h1 Suc [symmetric] mn ll1n ll2m [symmetric]) |
63361 | 46 |
with ll2m show "l \<le> k" by (rule h3') |
25422 | 47 |
qed |
48 |
ultimately show ?thesis using h1' by iprover |
|
49 |
qed |
|
50 |
qed |
|
51 |
||
52 |
extract greatest_common_divisor |
|
53 |
||
61986 | 54 |
text \<open> |
63361 | 55 |
The extracted program for computing the greatest common divisor is |
56 |
@{thm [display] greatest_common_divisor_def} |
|
61986 | 57 |
\<close> |
25422 | 58 |
|
27982 | 59 |
instantiation nat :: default |
60 |
begin |
|
61 |
||
62 |
definition "default = (0::nat)" |
|
63 |
||
64 |
instance .. |
|
25422 | 65 |
|
27982 | 66 |
end |
25422 | 67 |
|
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
36862
diff
changeset
|
68 |
instantiation prod :: (default, default) default |
27982 | 69 |
begin |
70 |
||
71 |
definition "default = (default, default)" |
|
72 |
||
73 |
instance .. |
|
25422 | 74 |
|
75 |
end |
|
27982 | 76 |
|
77 |
instantiation "fun" :: (type, default) default |
|
78 |
begin |
|
79 |
||
80 |
definition "default = (\<lambda>x. default)" |
|
81 |
||
82 |
instance .. |
|
83 |
||
84 |
end |
|
85 |
||
86 |
lemma "greatest_common_divisor 7 12 = (4, 3, 2)" by eval |
|
87 |
||
88 |
end |