author | wenzelm |
Wed, 30 Dec 2015 18:25:39 +0100 | |
changeset 61986 | 2461779da2b8 |
parent 58889 | 5b7a9633cfa8 |
child 63361 | d10eab0672f9 |
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: |
|
13 |
"\<And>n::nat. Suc m < n \<Longrightarrow> \<exists>k n1 m1. k * n1 = n \<and> k * m1 = Suc m \<and> |
|
14 |
(\<forall>l l1 l2. l * l1 = n \<longrightarrow> l * l2 = Suc m \<longrightarrow> l \<le> k)" |
|
15 |
proof (induct m rule: nat_wf_ind) |
|
16 |
case (1 m n) |
|
17 |
from division obtain r q where h1: "n = Suc m * q + r" and h2: "r \<le> m" |
|
18 |
by iprover |
|
19 |
show ?case |
|
20 |
proof (cases r) |
|
21 |
case 0 |
|
22 |
with h1 have "Suc m * q = n" by simp |
|
23 |
moreover have "Suc m * 1 = Suc m" by simp |
|
24 |
moreover { |
|
25 |
fix l2 have "\<And>l l1. l * l1 = n \<Longrightarrow> l * l2 = Suc m \<Longrightarrow> l \<le> Suc m" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
27982
diff
changeset
|
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> |
|
33 |
(\<forall>l l1 l2. l * l1 = Suc m \<longrightarrow> l * l2 = Suc nat \<longrightarrow> l \<le> k)" |
|
34 |
by (rule 1) |
|
35 |
then obtain k m1 r1 where |
|
36 |
h1': "k * m1 = Suc m" |
|
37 |
and h2': "k * r1 = Suc nat" |
|
38 |
and h3': "\<And>l l1 l2. l * l1 = Suc m \<Longrightarrow> l * l2 = Suc nat \<Longrightarrow> l \<le> k" |
|
39 |
by iprover |
|
40 |
have mn: "Suc m < n" by (rule 1) |
|
41 |
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
|
42 |
by (simp add: add_mult_distrib2 mult.assoc [symmetric]) |
25422 | 43 |
moreover have "\<And>l l1 l2. l * l1 = n \<Longrightarrow> l * l2 = Suc m \<Longrightarrow> l \<le> k" |
44 |
proof - |
|
45 |
fix l l1 l2 |
|
46 |
assume ll1n: "l * l1 = n" |
|
47 |
assume ll2m: "l * l2 = Suc m" |
|
48 |
moreover 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
|
49 |
by (simp add: diff_mult_distrib2 h1 Suc [symmetric] mn ll1n ll2m [symmetric]) |
25422 | 50 |
ultimately show "l \<le> k" by (rule h3') |
51 |
qed |
|
52 |
ultimately show ?thesis using h1' by iprover |
|
53 |
qed |
|
54 |
qed |
|
55 |
||
56 |
extract greatest_common_divisor |
|
57 |
||
61986 | 58 |
text \<open> |
25422 | 59 |
The extracted program for computing the greatest common divisor is |
60 |
@{thm [display] greatest_common_divisor_def} |
|
61986 | 61 |
\<close> |
25422 | 62 |
|
27982 | 63 |
instantiation nat :: default |
64 |
begin |
|
65 |
||
66 |
definition "default = (0::nat)" |
|
67 |
||
68 |
instance .. |
|
25422 | 69 |
|
27982 | 70 |
end |
25422 | 71 |
|
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
36862
diff
changeset
|
72 |
instantiation prod :: (default, default) default |
27982 | 73 |
begin |
74 |
||
75 |
definition "default = (default, default)" |
|
76 |
||
77 |
instance .. |
|
25422 | 78 |
|
79 |
end |
|
27982 | 80 |
|
81 |
instantiation "fun" :: (type, default) default |
|
82 |
begin |
|
83 |
||
84 |
definition "default = (\<lambda>x. default)" |
|
85 |
||
86 |
instance .. |
|
87 |
||
88 |
end |
|
89 |
||
90 |
lemma "greatest_common_divisor 7 12 = (4, 3, 2)" by eval |
|
91 |
||
92 |
end |