Quelle TPrimes.thy Sprache: Isabelle

(* EXTRACT from HOL/ex/Primes.thy*)

(*Euclid's algorithm
  This material now appears AFTER that of Forward.thy *)
theory TPrimes imports Main begin

fun gcd :: "nat \ nat \ nat" where
  "gcd m n = (if n=0 then m else gcd n (m mod n))"

text \<open>Now in Basic.thy!
@{thm[display]"dvd_def"}
\rulename{dvd_def}
\<close>

(*** Euclid's Algorithm ***)

lemma gcd_0 [simp]: "gcd m 0 = m"
apply (simp)
done

lemma gcd_non_0 [simp]: "0 gcd m n = gcd n (m mod n)"
apply (simp)
done

declare gcd.simps [simp del]

(*gcd(m,n) divides m and n.  The conjunctions don't seem provable separately*)
lemma gcd_dvd_both: "(gcd m n dvd m) \ (gcd m n dvd n)"
apply (induct_tac m n rule: gcd.induct)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (case_tac "n=0")
txt\<open>subgoals after the case tac
@{subgoals[display,indent=0,margin=65]}
\<close>
apply (simp_all)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
by (blast dest: dvd_mod_imp_dvd)

text \<open>
@{thm[display] dvd_mod_imp_dvd}
\rulename{dvd_mod_imp_dvd}

@{thm[display] dvd_trans}
\rulename{dvd_trans}
\<close>

lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1]
lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2]

text \<open>
\begin{quote}
@{thm[display] gcd_dvd1}
\rulename{gcd_dvd1}

@{thm[display] gcd_dvd2}
\rulename{gcd_dvd2}
\end{quote}
\<close>

(*Maximality: for all m,n,k naturals,
                if k divides m and k divides n then k divides gcd(m,n)*)
lemma gcd_greatest [rule_format]:
      "k dvd m \ k dvd n \ k dvd gcd m n"
apply (induct_tac m n rule: gcd.induct)
apply (case_tac "n=0")
txt\<open>subgoals after the case tac
@{subgoals[display,indent=0,margin=65]}
\<close>
apply (simp_all add: dvd_mod)
done

text \<open>
@{thm[display] dvd_mod}
\rulename{dvd_mod}
\<close>

(*just checking the claim that case_tac "n" works too*)
lemma "k dvd m \ k dvd n \ k dvd gcd m n"
apply (induct_tac m n rule: gcd.induct)
apply (case_tac "n")
apply (simp_all add: dvd_mod)
done

theorem gcd_greatest_iff [iff]:
        "(k dvd gcd m n) = (k dvd m \ k dvd n)"
by (blast intro!: gcd_greatest intro: dvd_trans)

(**** The material below was omitted from the book ****)

definition is_gcd :: "[nat,nat,nat] \ bool" where (*gcd as a relation*)
    "is_gcd p m n == p dvd m \ p dvd n \
                     (\<forall>d. d dvd m \<and> d dvd n \<longrightarrow> d dvd p)"

(*Function gcd yields the Greatest Common Divisor*)
lemma is_gcd: "is_gcd (gcd m n) m n"
apply (simp add: is_gcd_def gcd_greatest)
done

(*uniqueness of GCDs*)
lemma is_gcd_unique: "\ is_gcd m a b; is_gcd n a b \ \ m=n"
apply (simp add: is_gcd_def)
apply (blast intro: dvd_antisym)
done

text \<open>
@{thm[display] dvd_antisym}
\rulename{dvd_antisym}

\begin{isabelle}
proof\ (prove):\ step\ 1\isanewline
\isanewline
goal\ (lemma\ is_gcd_unique):\isanewline
\isasymlbrakk is_gcd\ m\ a\ b;\ is_gcd\ n\ a\ b\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n\isanewline
\ 1.\ \isasymlbrakk m\ dvd\ a\ \isasymand \ m\ dvd\ b\ \isasymand \ (\isasymforall d.\ d\ dvd\ a\ \isasymand \ d\ dvd\ b\ \isasymlongrightarrow \ d\ dvd\ m);\isanewline
\ \ \ \ \ \ \ n\ dvd\ a\ \isasymand \ n\ dvd\ b\ \isasymand \ (\isasymforall d.\ d\ dvd\ a\ \isasymand \ d\ dvd\ b\ \isasymlongrightarrow \ d\ dvd\ n)\isasymrbrakk \isanewline
\ \ \ \ \isasymLongrightarrow \ m\ =\ n
\end{isabelle}
\<close>

lemma gcd_assoc: "gcd (gcd k m) n = gcd k (gcd m n)"
  apply (rule is_gcd_unique)
  apply (rule is_gcd)
  apply (simp add: is_gcd_def)
  apply (blast intro: dvd_trans)
  done

text\<open>
\begin{isabelle}
proof\ (prove):\ step\ 3\isanewline
\isanewline
goal\ (lemma\ gcd_assoc):\isanewline
gcd\ (gcd\ (k,\ m),\ n)\ =\ gcd\ (k,\ gcd\ (m,\ n))\isanewline
\ 1.\ gcd\ (k,\ gcd\ (m,\ n))\ dvd\ k\ \isasymand \isanewline
\ \ \ \ gcd\ (k,\ gcd\ (m,\ n))\ dvd\ m\ \isasymand \ gcd\ (k,\ gcd\ (m,\ n))\ dvd\ n
\end{isabelle}
\<close>

lemma gcd_dvd_gcd_mult: "gcd m n dvd gcd (k*m) n"
  apply (auto intro: dvd_trans [of _ m])
  done

(*This is half of the proof (by dvd_antisym) of*)
lemma gcd_mult_cancel: "gcd k n = 1 \ gcd (k*m) n = gcd m n"
  oops

end

quality100%

¤ Dauer der Verarbeitung: 0.12 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.