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