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