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