# HG changeset patch
# User hoelzl
# Date 1366059115 -7200
# Node ID 5188a18c33b114a1dc8cb9c9e7fd52f5a6246816
# Parent  21d7933de1ebf7bc3f1b09862d18629832e65eac
use automatic type coerctions in Sqrt example

diff -r 21d7933de1eb -r 5188a18c33b1 src/HOL/ex/Sqrt.thy
--- a/src/HOL/ex/Sqrt.thy	Mon Apr 15 12:03:16 2013 +0200
+++ b/src/HOL/ex/Sqrt.thy	Mon Apr 15 22:51:55 2013 +0200
@@ -12,20 +12,20 @@
 
 theorem sqrt_prime_irrational:
   assumes "prime (p::nat)"
-  shows "sqrt (real p) \<notin> \<rat>"
+  shows "sqrt p \<notin> \<rat>"
 proof
   from `prime p` have p: "1 < p" by (simp add: prime_nat_def)
-  assume "sqrt (real p) \<in> \<rat>"
+  assume "sqrt p \<in> \<rat>"
   then obtain m n :: nat where
-      n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
+      n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
     and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)
   have eq: "m\<twosuperior> = p * n\<twosuperior>"
   proof -
-    from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
-    then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)"
+    from n and sqrt_rat have "m = \<bar>sqrt p\<bar> * n" by simp
+    then have "m\<twosuperior> = (sqrt p)\<twosuperior> * n\<twosuperior>"
       by (auto simp add: power2_eq_square)
-    also have "(sqrt (real p))\<twosuperior> = real p" by simp
-    also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp
+    also have "(sqrt p)\<twosuperior> = p" by simp
+    also have "\<dots> * n\<twosuperior> = p * n\<twosuperior>" by simp
     finally show ?thesis ..
   qed
   have "p dvd m \<and> p dvd n"
@@ -44,9 +44,8 @@
   with p show False by simp
 qed
 
-corollary sqrt_real_2_not_rat: "sqrt (real (2::nat)) \<notin> \<rat>"
-  by (rule sqrt_prime_irrational) (rule two_is_prime_nat)
-
+corollary sqrt_2_not_rat: "sqrt 2 \<notin> \<rat>"
+  using sqrt_prime_irrational[of 2] by simp
 
 subsection {* Variations *}
 
@@ -58,18 +57,18 @@
 
 theorem
   assumes "prime (p::nat)"
-  shows "sqrt (real p) \<notin> \<rat>"
+  shows "sqrt p \<notin> \<rat>"
 proof
   from `prime p` have p: "1 < p" by (simp add: prime_nat_def)
-  assume "sqrt (real p) \<in> \<rat>"
+  assume "sqrt p \<in> \<rat>"
   then obtain m n :: nat where
-      n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
+      n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
     and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)
-  from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
-  then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)"
+  from n and sqrt_rat have "m = \<bar>sqrt p\<bar> * n" by simp
+  then have "m\<twosuperior> = (sqrt p)\<twosuperior> * n\<twosuperior>"
     by (auto simp add: power2_eq_square)
-  also have "(sqrt (real p))\<twosuperior> = real p" by simp
-  also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp
+  also have "(sqrt p)\<twosuperior> = p" by simp
+  also have "\<dots> * n\<twosuperior> = p * n\<twosuperior>" by simp
   finally have eq: "m\<twosuperior> = p * n\<twosuperior>" ..
   then have "p dvd m\<twosuperior>" ..
   with `prime p` pos2 have dvd_m: "p dvd m" by (rule prime_dvd_power_nat)
@@ -91,7 +90,7 @@
 proof cases
   assume "sqrt 2 powr sqrt 2 \<in> \<rat>"
   then have "?P (sqrt 2) (sqrt 2)"
-    by (metis sqrt_real_2_not_rat [simplified])
+    by (metis sqrt_2_not_rat)
   then show ?thesis by blast
 next
   assume 1: "sqrt 2 powr sqrt 2 \<notin> \<rat>"
@@ -99,8 +98,9 @@
     using powr_realpow [of _ 2]
     by (simp add: powr_powr power2_eq_square [symmetric])
   then have "?P (sqrt 2 powr sqrt 2) (sqrt 2)"
-    by (metis 1 Rats_number_of sqrt_real_2_not_rat [simplified])
+    by (metis 1 Rats_number_of sqrt_2_not_rat)
   then show ?thesis by blast
 qed
 
 end
+