# HG changeset patch
# User nipkow
# Date 1324311053 -3600
# Node ID d7eabc09b6389cf57f8c50d1e3d5089d6db0efcc
# Parent  758671e966a0ebbc9c5592ae33702607ebc49434# Parent  1ce1bc9ff64aed007d225ab954d76edff87509e2
merged

diff -r 758671e966a0 -r d7eabc09b638 src/HOL/ex/Sqrt.thy
--- a/src/HOL/ex/Sqrt.thy	Mon Dec 19 13:58:54 2011 +0100
+++ b/src/HOL/ex/Sqrt.thy	Mon Dec 19 17:10:53 2011 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOL/ex/Sqrt.thy
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Markus Wenzel, Tobias Nipkow, TU Muenchen
 *)
 
 header {*  Square roots of primes are irrational *}
@@ -47,7 +47,7 @@
   with p show False by simp
 qed
 
-corollary "sqrt (real (2::nat)) \<notin> \<rat>"
+corollary sqrt_real_2_not_rat: "sqrt (real (2::nat)) \<notin> \<rat>"
   by (rule sqrt_prime_irrational) (rule two_is_prime_nat)
 
 
@@ -87,4 +87,22 @@
   with p show False by simp
 qed
 
+
+text{* Another old chestnut, which is a consequence of the irrationality of 2. *}
+
+lemma "\<exists>a b::real. a \<notin> \<rat> \<and> b \<notin> \<rat> \<and> a powr b \<in> \<rat>" (is "EX a b. ?P a b")
+proof cases
+  assume "sqrt 2 powr sqrt 2 \<in> \<rat>"
+  hence "?P (sqrt 2) (sqrt 2)" by(metis sqrt_real_2_not_rat[simplified])
+  thus ?thesis by blast
+next
+  assume 1: "sqrt 2 powr sqrt 2 \<notin> \<rat>"
+  have "(sqrt 2 powr sqrt 2) powr sqrt 2 = 2"
+    using powr_realpow[of _ 2]
+    by (simp add: powr_powr power2_eq_square[symmetric])
+  hence "?P (sqrt 2 powr sqrt 2) (sqrt 2)"
+    by (metis 1 Rats_number_of sqrt_real_2_not_rat[simplified])
+  thus ?thesis by blast
+qed
+
 end