Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Sqrt.thy   Sprache: Isabelle

Original von: Isabelle©

(*  Title:      HOL/ex/Sqrt.thy
    Author:     Markus Wenzel, Tobias Nipkow, TU Muenchen
*)


section \<open>Square roots of primes are irrational\<close>

theory Sqrt
imports Complex_Main "HOL-Computational_Algebra.Primes"
begin

text \<open>The square root of any prime number (including 2) is irrational.\<close>

theorem sqrt_prime_irrational:
  assumes "prime (p::nat)"
  shows "sqrt p \ \"
proof
  from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_nat_iff)
  assume "sqrt p \ \"
  then obtain m n :: nat where
      n: "n \ 0" and sqrt_rat: "\sqrt p\ = m / n"
    and "coprime m n" by (rule Rats_abs_nat_div_natE)
  have eq: "m\<^sup>2 = p * n\<^sup>2"
  proof -
    from n and sqrt_rat have "m = \sqrt p\ * n" by simp
    then have "m\<^sup>2 = (sqrt p)\<^sup>2 * n\<^sup>2"
      by (auto simp add: power2_eq_square)
    also have "(sqrt p)\<^sup>2 = p" by simp
    also have "\ * n\<^sup>2 = p * n\<^sup>2" by simp
    finally show ?thesis using of_nat_eq_iff by blast
  qed
  have "p dvd m \ p dvd n"
  proof
    from eq have "p dvd m\<^sup>2" ..
    with \<open>prime p\<close> show "p dvd m" by (rule prime_dvd_power_nat)
    then obtain k where "m = p * k" ..
    with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square ac_simps)
    with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)
    then have "p dvd n\<^sup>2" ..
    with \<open>prime p\<close> show "p dvd n" by (rule prime_dvd_power_nat)
  qed
  then have "p dvd gcd m n" by simp
  with \<open>coprime m n\<close> have "p = 1" by simp
  with p show False by simp
qed

corollary sqrt_2_not_rat: "sqrt 2 \ \"
  using sqrt_prime_irrational[of 2] by simp


subsection \<open>Variations\<close>

text \<open>
  Here is an alternative version of the main proofusing mostly
  linear forward-reasoning.  While this results in less top-down
  structure, it is probably closer to proofs seen in mathematics.
\<close>

theorem
  assumes "prime (p::nat)"
  shows "sqrt p \ \"
proof
  from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_nat_iff)
  assume "sqrt p \ \"
  then obtain m n :: nat where
      n: "n \ 0" and sqrt_rat: "\sqrt p\ = m / n"
    and "coprime m n" by (rule Rats_abs_nat_div_natE)
  from n and sqrt_rat have "m = \sqrt p\ * n" by simp
  then have "m\<^sup>2 = (sqrt p)\<^sup>2 * n\<^sup>2"
    by (auto simp add: power2_eq_square)
  also have "(sqrt p)\<^sup>2 = p" by simp
  also have "\ * n\<^sup>2 = p * n\<^sup>2" by simp
  finally have eq: "m\<^sup>2 = p * n\<^sup>2" using of_nat_eq_iff by blast
  then have "p dvd m\<^sup>2" ..
  with \<open>prime p\<close> have dvd_m: "p dvd m" by (rule prime_dvd_power_nat)
  then obtain k where "m = p * k" ..
  with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square ac_simps)
  with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)
  then have "p dvd n\<^sup>2" ..
  with \<open>prime p\<close> have "p dvd n" by (rule prime_dvd_power_nat)
  with dvd_m have "p dvd gcd m n" by (rule gcd_greatest)
  with \<open>coprime m n\<close> have "p = 1" by simp
  with p show False by simp
qed


text \<open>Another old chestnut, which is a consequence of the irrationality of 2.\<close>

lemma "\a b::real. a \ \ \ b \ \ \ a powr b \ \" (is "\a b. ?P a b")
proof cases
  assume "sqrt 2 powr sqrt 2 \ \"
  then have "?P (sqrt 2) (sqrt 2)"
    by (metis sqrt_2_not_rat)
  then show ?thesis by blast
next
  assume 1: "sqrt 2 powr sqrt 2 \ \"
  have "(sqrt 2 powr sqrt 2) powr sqrt 2 = 2"
    using powr_realpow [of _ 2]
    by (simp add: powr_powr power2_eq_square [symmetric])
  then have "?P (sqrt 2 powr sqrt 2) (sqrt 2)"
    by (metis 1 Rats_number_of sqrt_2_not_rat)
  then show ?thesis by blast
qed

end

¤ Dauer der Verarbeitung: 0.0 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




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.


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik