src/HOL/ex/Sqrt_Script.thy
 author nipkow Fri Mar 06 17:38:47 2009 +0100 (2009-03-06) changeset 30313 b2441b0c8d38 parent 28952 15a4b2cf8c34 child 32479 521cc9bf2958 permissions -rw-r--r--
 haftmann@28952 ` 1` ```(* Title: HOL/ex/Sqrt_Script.thy ``` paulson@13957 ` 2` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` paulson@13957 ` 3` ``` Copyright 2001 University of Cambridge ``` paulson@13957 ` 4` ```*) ``` paulson@13957 ` 5` paulson@13957 ` 6` ```header {* Square roots of primes are irrational (script version) *} ``` paulson@13957 ` 7` nipkow@15149 ` 8` ```theory Sqrt_Script ``` haftmann@28952 ` 9` ```imports Complex_Main Primes ``` nipkow@15149 ` 10` ```begin ``` paulson@13957 ` 11` paulson@13957 ` 12` ```text {* ``` paulson@13957 ` 13` ``` \medskip Contrast this linear Isabelle/Isar script with Markus ``` paulson@13957 ` 14` ``` Wenzel's more mathematical version. ``` paulson@13957 ` 15` ```*} ``` paulson@13957 ` 16` paulson@13957 ` 17` ```subsection {* Preliminaries *} ``` paulson@13957 ` 18` nipkow@16663 ` 19` ```lemma prime_nonzero: "prime p \ p \ 0" ``` paulson@13957 ` 20` ``` by (force simp add: prime_def) ``` paulson@13957 ` 21` paulson@13957 ` 22` ```lemma prime_dvd_other_side: ``` nipkow@16663 ` 23` ``` "n * n = p * (k * k) \ prime p \ p dvd n" ``` paulson@13957 ` 24` ``` apply (subgoal_tac "p dvd n * n", blast dest: prime_dvd_mult) ``` haftmann@27651 ` 25` ``` apply auto ``` paulson@13957 ` 26` ``` done ``` paulson@13957 ` 27` nipkow@16663 ` 28` ```lemma reduction: "prime p \ ``` paulson@13957 ` 29` ``` 0 < k \ k * k = p * (j * j) \ k < p * j \ 0 < j" ``` paulson@13957 ` 30` ``` apply (rule ccontr) ``` paulson@13957 ` 31` ``` apply (simp add: linorder_not_less) ``` paulson@13957 ` 32` ``` apply (erule disjE) ``` paulson@13957 ` 33` ``` apply (frule mult_le_mono, assumption) ``` paulson@13957 ` 34` ``` apply auto ``` paulson@13957 ` 35` ``` apply (force simp add: prime_def) ``` paulson@13957 ` 36` ``` done ``` paulson@13957 ` 37` paulson@13957 ` 38` ```lemma rearrange: "(j::nat) * (p * j) = k * k \ k * k = p * (j * j)" ``` paulson@13957 ` 39` ``` by (simp add: mult_ac) ``` paulson@13957 ` 40` paulson@13957 ` 41` ```lemma prime_not_square: ``` nipkow@16663 ` 42` ``` "prime p \ (\k. 0 < k \ m * m \ p * (k * k))" ``` paulson@13957 ` 43` ``` apply (induct m rule: nat_less_induct) ``` paulson@13957 ` 44` ``` apply clarify ``` paulson@13957 ` 45` ``` apply (frule prime_dvd_other_side, assumption) ``` paulson@13957 ` 46` ``` apply (erule dvdE) ``` paulson@13957 ` 47` ``` apply (simp add: nat_mult_eq_cancel_disj prime_nonzero) ``` paulson@13957 ` 48` ``` apply (blast dest: rearrange reduction) ``` paulson@13957 ` 49` ``` done ``` paulson@13957 ` 50` paulson@13957 ` 51` paulson@13957 ` 52` ```subsection {* Main theorem *} ``` paulson@13957 ` 53` paulson@13957 ` 54` ```text {* ``` paulson@13957 ` 55` ``` The square root of any prime number (including @{text 2}) is ``` paulson@13957 ` 56` ``` irrational. ``` paulson@13957 ` 57` ```*} ``` paulson@13957 ` 58` paulson@13957 ` 59` ```theorem prime_sqrt_irrational: ``` nipkow@16663 ` 60` ``` "prime p \ x * x = real p \ 0 \ x \ x \ \" ``` nipkow@28001 ` 61` ``` apply (rule notI) ``` nipkow@28001 ` 62` ``` apply (erule Rats_abs_nat_div_natE) ``` paulson@13957 ` 63` ``` apply (simp del: real_of_nat_mult ``` nipkow@28001 ` 64` ``` add: real_abs_def divide_eq_eq prime_not_square real_of_nat_mult [symmetric]) ``` paulson@13957 ` 65` ``` done ``` paulson@13957 ` 66` paulson@13957 ` 67` ```lemmas two_sqrt_irrational = ``` paulson@13957 ` 68` ``` prime_sqrt_irrational [OF two_is_prime] ``` paulson@13957 ` 69` paulson@13957 ` 70` ```end ```