(* Title: HOL/ex/Sqrt_Script.thy Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 2001 University of Cambridge
*)
section \<open>Square roots of primes are irrational (script version)\<close>
text\<open>
Contrast this linear Isabelle/Isar script with the more mathematical version in\<^file>\<open>~~/src/HOL/Examples/Sqrt.thy\<close> by Makarius Wenzel. \<close>
theory Sqrt_Script imports Complex_Main "HOL-Computational_Algebra.Primes" begin
subsection \<open>Preliminaries\<close>
lemma prime_nonzero: "prime (p::nat) \ p \ 0" by (force simp add: prime_nat_iff)
lemma prime_dvd_other_side: "(n::nat) * n = p * (k * k) \ prime p \ p dvd n" apply (subgoal_tac "p dvd n * n", blast dest: prime_dvd_mult_nat) apply auto done
lemma reduction: "prime (p::nat) \
0 < k \<Longrightarrow> k * k = p * (j * j) \<Longrightarrow> k < p * j \<and> 0 < j" apply (rule ccontr) apply (simp add: linorder_not_less) apply (erule disjE) apply (frule mult_le_mono, assumption) apply auto apply (force simp add: prime_nat_iff) done
lemma rearrange: "(j::nat) * (p * j) = k * k \ k * k = p * (j * j)" by (simp add: ac_simps)
lemma prime_not_square: "prime (p::nat) \ (\k. 0 < k \ m * m \ p * (k * k))" apply (induct m rule: nat_less_induct) apply clarify apply (frule prime_dvd_other_side, assumption) apply (erule dvdE) apply (simp add: nat_mult_eq_cancel_disj prime_nonzero) apply (blast dest: rearrange reduction) done
subsection \<open>Main theorem\<close>
text\<open>
The square root of any prime number (including \<open>2\<close>) is
irrational. \<close>
theorem prime_sqrt_irrational: "prime (p::nat) \ x * x = real p \ 0 \ x \ x \ \" apply (rule notI) apply (erule Rats_abs_nat_div_natE) apply (simp del: of_nat_mult
add: abs_if divide_eq_eq prime_not_square of_nat_mult [symmetric]) done
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.
