author  haftmann 
Tue, 01 Sep 2009 15:39:33 +0200  
changeset 32479  521cc9bf2958 
parent 28952  15a4b2cf8c34 
child 36778  739a9379e29b 
permissions  rwrr 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28001
diff
changeset

1 
(* Title: HOL/ex/Sqrt_Script.thy 
13957  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
3 
Copyright 2001 University of Cambridge 

4 
*) 

5 

6 
header {* Square roots of primes are irrational (script version) *} 

7 

15149  8 
theory Sqrt_Script 
32479  9 
imports Complex_Main "~~/src/HOL/Number_Theory/Primes" 
15149  10 
begin 
13957  11 

12 
text {* 

13 
\medskip Contrast this linear Isabelle/Isar script with Markus 

14 
Wenzel's more mathematical version. 

15 
*} 

16 

17 
subsection {* Preliminaries *} 

18 

32479  19 
lemma prime_nonzero: "prime (p::nat) \<Longrightarrow> p \<noteq> 0" 
20 
by (force simp add: prime_nat_def) 

13957  21 

22 
lemma prime_dvd_other_side: 

32479  23 
"(n::nat) * n = p * (k * k) \<Longrightarrow> prime p \<Longrightarrow> p dvd n" 
24 
apply (subgoal_tac "p dvd n * n", blast dest: prime_dvd_mult_nat) 

27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
21404
diff
changeset

25 
apply auto 
13957  26 
done 
27 

32479  28 
lemma reduction: "prime (p::nat) \<Longrightarrow> 
13957  29 
0 < k \<Longrightarrow> k * k = p * (j * j) \<Longrightarrow> k < p * j \<and> 0 < j" 
30 
apply (rule ccontr) 

31 
apply (simp add: linorder_not_less) 

32 
apply (erule disjE) 

33 
apply (frule mult_le_mono, assumption) 

34 
apply auto 

32479  35 
apply (force simp add: prime_nat_def) 
13957  36 
done 
37 

38 
lemma rearrange: "(j::nat) * (p * j) = k * k \<Longrightarrow> k * k = p * (j * j)" 

39 
by (simp add: mult_ac) 

40 

41 
lemma prime_not_square: 

32479  42 
"prime (p::nat) \<Longrightarrow> (\<And>k. 0 < k \<Longrightarrow> m * m \<noteq> p * (k * k))" 
13957  43 
apply (induct m rule: nat_less_induct) 
44 
apply clarify 

45 
apply (frule prime_dvd_other_side, assumption) 

46 
apply (erule dvdE) 

47 
apply (simp add: nat_mult_eq_cancel_disj prime_nonzero) 

48 
apply (blast dest: rearrange reduction) 

49 
done 

50 

51 

52 
subsection {* Main theorem *} 

53 

54 
text {* 

55 
The square root of any prime number (including @{text 2}) is 

56 
irrational. 

57 
*} 

58 

59 
theorem prime_sqrt_irrational: 

32479  60 
"prime (p::nat) \<Longrightarrow> x * x = real p \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<notin> \<rat>" 
28001  61 
apply (rule notI) 
62 
apply (erule Rats_abs_nat_div_natE) 

13957  63 
apply (simp del: real_of_nat_mult 
28001  64 
add: real_abs_def divide_eq_eq prime_not_square real_of_nat_mult [symmetric]) 
13957  65 
done 
66 

67 
lemmas two_sqrt_irrational = 

32479  68 
prime_sqrt_irrational [OF two_is_prime_nat] 
13957  69 

70 
end 