src/HOL/ex/Sqrt.thy
 changeset 53015 a1119cf551e8 parent 51708 5188a18c33b1 child 53598 2bd8d459ebae
```     1.1 --- a/src/HOL/ex/Sqrt.thy	Tue Aug 13 14:20:22 2013 +0200
1.2 +++ b/src/HOL/ex/Sqrt.thy	Tue Aug 13 16:25:47 2013 +0200
1.3 @@ -19,23 +19,23 @@
1.4    then obtain m n :: nat where
1.5        n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
1.6      and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)
1.7 -  have eq: "m\<twosuperior> = p * n\<twosuperior>"
1.8 +  have eq: "m\<^sup>2 = p * n\<^sup>2"
1.9    proof -
1.10      from n and sqrt_rat have "m = \<bar>sqrt p\<bar> * n" by simp
1.11 -    then have "m\<twosuperior> = (sqrt p)\<twosuperior> * n\<twosuperior>"
1.12 +    then have "m\<^sup>2 = (sqrt p)\<^sup>2 * n\<^sup>2"
1.13        by (auto simp add: power2_eq_square)
1.14 -    also have "(sqrt p)\<twosuperior> = p" by simp
1.15 -    also have "\<dots> * n\<twosuperior> = p * n\<twosuperior>" by simp
1.16 +    also have "(sqrt p)\<^sup>2 = p" by simp
1.17 +    also have "\<dots> * n\<^sup>2 = p * n\<^sup>2" by simp
1.18      finally show ?thesis ..
1.19    qed
1.20    have "p dvd m \<and> p dvd n"
1.21    proof
1.22 -    from eq have "p dvd m\<twosuperior>" ..
1.23 +    from eq have "p dvd m\<^sup>2" ..
1.24      with `prime p` pos2 show "p dvd m" by (rule prime_dvd_power_nat)
1.25      then obtain k where "m = p * k" ..
1.26 -    with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac)
1.27 -    with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square)
1.28 -    then have "p dvd n\<twosuperior>" ..
1.29 +    with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square mult_ac)
1.30 +    with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)
1.31 +    then have "p dvd n\<^sup>2" ..
1.32      with `prime p` pos2 show "p dvd n" by (rule prime_dvd_power_nat)
1.33    qed
1.34    then have "p dvd gcd m n" ..
1.35 @@ -65,17 +65,17 @@
1.36        n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
1.37      and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)
1.38    from n and sqrt_rat have "m = \<bar>sqrt p\<bar> * n" by simp
1.39 -  then have "m\<twosuperior> = (sqrt p)\<twosuperior> * n\<twosuperior>"
1.40 +  then have "m\<^sup>2 = (sqrt p)\<^sup>2 * n\<^sup>2"
1.41      by (auto simp add: power2_eq_square)
1.42 -  also have "(sqrt p)\<twosuperior> = p" by simp
1.43 -  also have "\<dots> * n\<twosuperior> = p * n\<twosuperior>" by simp
1.44 -  finally have eq: "m\<twosuperior> = p * n\<twosuperior>" ..
1.45 -  then have "p dvd m\<twosuperior>" ..
1.46 +  also have "(sqrt p)\<^sup>2 = p" by simp
1.47 +  also have "\<dots> * n\<^sup>2 = p * n\<^sup>2" by simp
1.48 +  finally have eq: "m\<^sup>2 = p * n\<^sup>2" ..
1.49 +  then have "p dvd m\<^sup>2" ..
1.50    with `prime p` pos2 have dvd_m: "p dvd m" by (rule prime_dvd_power_nat)
1.51    then obtain k where "m = p * k" ..
1.52 -  with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac)
1.53 -  with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square)
1.54 -  then have "p dvd n\<twosuperior>" ..
1.55 +  with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square mult_ac)
1.56 +  with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)
1.57 +  then have "p dvd n\<^sup>2" ..
1.58    with `prime p` pos2 have "p dvd n" by (rule prime_dvd_power_nat)
1.59    with dvd_m have "p dvd gcd m n" by (rule gcd_greatest_nat)
1.60    with gcd have "p dvd 1" by simp
```