13957
|
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 |
|
15149
|
9 |
theory Sqrt_Script
|
|
10 |
imports Primes Complex_Main
|
|
11 |
begin
|
13957
|
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 |
|
16663
|
20 |
lemma prime_nonzero: "prime p \<Longrightarrow> p \<noteq> 0"
|
13957
|
21 |
by (force simp add: prime_def)
|
|
22 |
|
|
23 |
lemma prime_dvd_other_side:
|
16663
|
24 |
"n * n = p * (k * k) \<Longrightarrow> prime p \<Longrightarrow> p dvd n"
|
13957
|
25 |
apply (subgoal_tac "p dvd n * n", blast dest: prime_dvd_mult)
|
|
26 |
apply (rule_tac j = "k * k" in dvd_mult_left, simp)
|
|
27 |
done
|
|
28 |
|
16663
|
29 |
lemma reduction: "prime p \<Longrightarrow>
|
13957
|
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:
|
16663
|
43 |
"prime p \<Longrightarrow> (\<And>k. 0 < k \<Longrightarrow> m * m \<noteq> p * (k * k))"
|
13957
|
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 {* The set of rational numbers *}
|
|
54 |
|
19736
|
55 |
definition
|
13957
|
56 |
rationals :: "real set" ("\<rat>")
|
19736
|
57 |
"\<rat> = {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
|
13957
|
58 |
|
|
59 |
|
|
60 |
subsection {* Main theorem *}
|
|
61 |
|
|
62 |
text {*
|
|
63 |
The square root of any prime number (including @{text 2}) is
|
|
64 |
irrational.
|
|
65 |
*}
|
|
66 |
|
|
67 |
theorem prime_sqrt_irrational:
|
16663
|
68 |
"prime p \<Longrightarrow> x * x = real p \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<notin> \<rat>"
|
13957
|
69 |
apply (simp add: rationals_def real_abs_def)
|
|
70 |
apply clarify
|
|
71 |
apply (erule_tac P = "real m / real n * ?x = ?y" in rev_mp)
|
|
72 |
apply (simp del: real_of_nat_mult
|
14288
|
73 |
add: divide_eq_eq prime_not_square real_of_nat_mult [symmetric])
|
13957
|
74 |
done
|
|
75 |
|
|
76 |
lemmas two_sqrt_irrational =
|
|
77 |
prime_sqrt_irrational [OF two_is_prime]
|
|
78 |
|
|
79 |
end
|