1(*  Title:      HOL/Proofs/Extraction/Greatest_Common_Divisor.thy
2    Author:     Stefan Berghofer, TU Muenchen
3    Author:     Helmut Schwichtenberg, LMU Muenchen
4*)
5
6section \<open>Greatest common divisor\<close>
7
8theory Greatest_Common_Divisor
9imports QuotRem
10begin
11
12theorem greatest_common_divisor:
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)"
16proof (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 have "l * l1 = n \<Longrightarrow> l * l2 = Suc m \<Longrightarrow> l \<le> Suc m" for l l1 l2
26      by (cases l2) simp_all
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 h1': "k * m1 = Suc m"
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)
40    from h1 h1' h2' Suc have "k * (m1 * q + r1) = n"
41      by (simp add: add_mult_distrib2 mult.assoc [symmetric])
42    moreover have "l \<le> k" if ll1n: "l * l1 = n" and ll2m: "l * l2 = Suc m" for l l1 l2
43    proof -
44      have "l * (l1 - l2 * q) = Suc nat"
45        by (simp add: diff_mult_distrib2 h1 Suc [symmetric] mn ll1n ll2m [symmetric])
46      with ll2m show "l \<le> k" by (rule h3')
47    qed
48    ultimately show ?thesis using h1' by iprover
49  qed
50qed
51
52extract greatest_common_divisor
53
54text \<open>
55  The extracted program for computing the greatest common divisor is
56  @{thm [display] greatest_common_divisor_def}
57\<close>
58
59instantiation nat :: default
60begin
61
62definition "default = (0::nat)"
63
64instance ..
65
66end
67
68instantiation prod :: (default, default) default
69begin
70
71definition "default = (default, default)"
72
73instance ..
74
75end
76
77instantiation "fun" :: (type, default) default
78begin
79
80definition "default = (\<lambda>x. default)"
81
82instance ..
83
84end
85
86lemma "greatest_common_divisor 7 12 = (4, 3, 2)" by eval
87
88end
89