src/HOL/Complex/ex/Sqrt_Script.thy
 author nipkow Thu Aug 19 12:35:45 2004 +0200 (2004-08-19) changeset 15149 c5c4884634b7 parent 14288 d149e3cbdb39 child 16663 13e9c402308b permissions -rw-r--r--
new import syntax
 paulson@13957 1 (* Title: HOL/Hyperreal/ex/Sqrt_Script.thy paulson@13957 2 ID: \$Id\$ paulson@13957 3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory paulson@13957 4 Copyright 2001 University of Cambridge paulson@13957 5 *) paulson@13957 6 paulson@13957 7 header {* Square roots of primes are irrational (script version) *} paulson@13957 8 nipkow@15149 9 theory Sqrt_Script nipkow@15149 10 imports Primes Complex_Main nipkow@15149 11 begin paulson@13957 12 paulson@13957 13 text {* paulson@13957 14 \medskip Contrast this linear Isabelle/Isar script with Markus paulson@13957 15 Wenzel's more mathematical version. paulson@13957 16 *} paulson@13957 17 paulson@13957 18 subsection {* Preliminaries *} paulson@13957 19 paulson@13957 20 lemma prime_nonzero: "p \ prime \ p \ 0" paulson@13957 21 by (force simp add: prime_def) paulson@13957 22 paulson@13957 23 lemma prime_dvd_other_side: paulson@13957 24 "n * n = p * (k * k) \ p \ prime \ p dvd n" paulson@13957 25 apply (subgoal_tac "p dvd n * n", blast dest: prime_dvd_mult) paulson@13957 26 apply (rule_tac j = "k * k" in dvd_mult_left, simp) paulson@13957 27 done paulson@13957 28 paulson@13957 29 lemma reduction: "p \ prime \ paulson@13957 30 0 < k \ k * k = p * (j * j) \ k < p * j \ 0 < j" paulson@13957 31 apply (rule ccontr) paulson@13957 32 apply (simp add: linorder_not_less) paulson@13957 33 apply (erule disjE) paulson@13957 34 apply (frule mult_le_mono, assumption) paulson@13957 35 apply auto paulson@13957 36 apply (force simp add: prime_def) paulson@13957 37 done paulson@13957 38 paulson@13957 39 lemma rearrange: "(j::nat) * (p * j) = k * k \ k * k = p * (j * j)" paulson@13957 40 by (simp add: mult_ac) paulson@13957 41 paulson@13957 42 lemma prime_not_square: paulson@13957 43 "p \ prime \ (\k. 0 < k \ m * m \ p * (k * k))" paulson@13957 44 apply (induct m rule: nat_less_induct) paulson@13957 45 apply clarify paulson@13957 46 apply (frule prime_dvd_other_side, assumption) paulson@13957 47 apply (erule dvdE) paulson@13957 48 apply (simp add: nat_mult_eq_cancel_disj prime_nonzero) paulson@13957 49 apply (blast dest: rearrange reduction) paulson@13957 50 done paulson@13957 51 paulson@13957 52 paulson@13957 53 subsection {* The set of rational numbers *} paulson@13957 54 paulson@13957 55 constdefs paulson@13957 56 rationals :: "real set" ("\") paulson@13957 57 "\ \ {x. \m n. n \ 0 \ \x\ = real (m::nat) / real (n::nat)}" paulson@13957 58 paulson@13957 59 paulson@13957 60 subsection {* Main theorem *} paulson@13957 61 paulson@13957 62 text {* paulson@13957 63 The square root of any prime number (including @{text 2}) is paulson@13957 64 irrational. paulson@13957 65 *} paulson@13957 66 paulson@13957 67 theorem prime_sqrt_irrational: paulson@13957 68 "p \ prime \ x * x = real p \ 0 \ x \ x \ \" paulson@13957 69 apply (simp add: rationals_def real_abs_def) paulson@13957 70 apply clarify paulson@13957 71 apply (erule_tac P = "real m / real n * ?x = ?y" in rev_mp) paulson@13957 72 apply (simp del: real_of_nat_mult paulson@14288 73 add: divide_eq_eq prime_not_square real_of_nat_mult [symmetric]) paulson@13957 74 done paulson@13957 75 paulson@13957 76 lemmas two_sqrt_irrational = paulson@13957 77 prime_sqrt_irrational [OF two_is_prime] paulson@13957 78 paulson@13957 79 end