# HG changeset patch
# User nipkow
# Date 1324311045 -3600
# Node ID 1ce1bc9ff64aed007d225ab954d76edff87509e2
# Parent  eaf6728d25129049898f0d23acc7af76ed29bd87
added old chestnut

diff -r eaf6728d2512 -r 1ce1bc9ff64a src/HOL/ex/Sqrt.thy
--- a/src/HOL/ex/Sqrt.thy	Sun Dec 18 14:28:14 2011 +0100
+++ b/src/HOL/ex/Sqrt.thy	Mon Dec 19 17:10:45 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