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
    moreover have "Suc m * 1 = Suc m" by simp
    moreover have "l * l1 = n \ l * l2 = Suc m \ l \ Suc m" for l l1 l2
      by (cases l2) simp_all
    ultimately show ?thesis by iprover
  next
    case (Suc nat)
    with h2 have h: "nat < m" by simp
    moreover from h have "Suc nat < Suc m" by simp
    ultimately have "\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)
    then obtain 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])
    moreover have "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
    ultimately show ?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

definition "default = (\x. default)"

instance ..

end

lemma "greatest_common_divisor 7 12 = (4, 3, 2)" by eval

end

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.