Quelle Greatest_Common_Divisor.thy
Sprache: Isabelle
(* Title: HOL/Proofs/Extraction/Greatest_Common_Divisor.thy Author: Stefan Berghofer, TU Muenchen Author: Helmut Schwichtenberg, LMU Muenchen
*)
section \<open>Greatest common divisor\<close>
theory Greatest_Common_Divisor imports QuotRem begin
theorem greatest_common_divisor: "\n::nat. Suc m < n \ \<exists>k n1 m1. k * n1 = n \<and> k * m1 = Suc m \<and>
(\<forall>l l1 l2. l * l1 = n \<longrightarrow> l * l2 = Suc m \<longrightarrow> l \<le> k)" proof (induct m rule: nat_wf_ind) case (1 m n) from division obtain r q where h1: "n = Suc m * q + r"and h2: "r \ m" by iprover show ?case proof (cases r) case 0 with h1 have"Suc m * q = n"by simp moreoverhave"Suc m * 1 = Suc m"by simp moreoverhave"l * l1 = n \ l * l2 = Suc m \ l \ Suc m" for l l1 l2 by (cases l2) simp_all ultimatelyshow ?thesis by iprover next case (Suc nat) with h2 have h: "nat < m"by simp moreoverfrom h have"Suc nat < Suc m"by simp ultimatelyhave"\k m1 r1. k * m1 = Suc m \ k * r1 = Suc nat \
(\<forall>l l1 l2. l * l1 = Suc m \<longrightarrow> l * l2 = Suc nat \<longrightarrow> l \<le> k)" by (rule 1) thenobtain k m1 r1 where h1': "k * m1 = Suc m" and h2': "k * r1 = Suc nat" and h3': "\l l1 l2. l * l1 = Suc m \ l * l2 = Suc nat \ l \ k" by iprover have mn: "Suc m < n"by (rule 1) from h1 h1' h2' Suc have"k * (m1 * q + r1) = n" by (simp add: add_mult_distrib2 mult.assoc [symmetric]) moreoverhave"l \ k" if ll1n: "l * l1 = n" and ll2m: "l * l2 = Suc m" for l l1 l2 proof - have"l * (l1 - l2 * q) = Suc nat" by (simp add: diff_mult_distrib2 h1 Suc [symmetric] mn ll1n ll2m [symmetric]) with ll2m show"l \ k" by (rule h3') qed ultimatelyshow ?thesis using h1' by iprover qed qed
extract greatest_common_divisor
text\<open>
The extracted program for computing the greatest common divisor is
@{thm [display] greatest_common_divisor_def} \<close>
instantiation nat :: default begin
definition"default = (0::nat)"
instance ..
end
instantiation prod :: (default, default) default begin
definition"default = (default, default)"
instance ..
end
instantiation"fun" :: (type, default) default begin
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
