# HG changeset patch # User wenzelm # Date 1010952891 -3600 # Node ID c06aee15dc00ed2c5bc2e24bedb33df2fbfcda73 # Parent 4e45fb10c811a6c37ee3cd3b30d6f9c9ca7c8502 \ syntax moved to HOL/Numerals; diff -r 4e45fb10c811 -r c06aee15dc00 src/HOL/Real/ex/Sqrt.thy --- a/src/HOL/Real/ex/Sqrt.thy Sun Jan 13 21:14:31 2002 +0100 +++ b/src/HOL/Real/ex/Sqrt.thy Sun Jan 13 21:14:51 2002 +0100 @@ -8,16 +8,6 @@ theory Sqrt = Primes + Real: -syntax (xsymbols) (* FIXME move to main HOL (!?) *) - "_square" :: "'a => 'a" ("(_\)" [1000] 999) -syntax (HTML output) - "_square" :: "'a => 'a" ("(_\)" [1000] 999) -syntax (output) - "_square" :: "'a => 'a" ("(_^2)" [1000] 999) -translations - "x\" == "x^Suc (Suc 0)" - - subsection {* The set of rational numbers *} constdefs @@ -86,19 +76,20 @@ have eq: "m\ = p * n\" proof - from n x_rat have "real m = \x\ * real n" by simp - hence "real (m\) = x\ * real (n\)" by (simp split: abs_split) + hence "real (m\) = x\ * real (n\)" + by (simp add: power_two real_power_two split: abs_split) also from x_sqrt have "... = real (p * n\)" by simp finally show ?thesis .. qed have "p dvd m \ p dvd n" proof from eq have "p dvd m\" .. - with p_prime show "p dvd m" by (rule prime_dvd_square) + with p_prime show "p dvd m" by (rule prime_dvd_power_two) then obtain k where "m = p * k" .. - with eq have "p * n\ = p\ * k\" by (auto simp add: mult_ac) - with p have "n\ = p * k\" by simp + with eq have "p * n\ = p\ * k\" by (auto simp add: power_two mult_ac) + with p have "n\ = p * k\" by (simp add: power_two) hence "p dvd n\" .. - with p_prime show "p dvd n" by (rule prime_dvd_square) + with p_prime show "p dvd n" by (rule prime_dvd_power_two) qed hence "p dvd gcd (m, n)" .. with gcd have "p dvd 1" by simp @@ -141,16 +132,17 @@ then obtain m n where n: "n \ 0" and x_rat: "\x\ = real m / real n" and gcd: "gcd (m, n) = 1" .. from n x_rat have "real m = \x\ * real n" by simp - hence "real (m\) = x\ * real (n\)" by (simp split: abs_split) + hence "real (m\) = x\ * real (n\)" + by (simp add: power_two real_power_two split: abs_split) also from x_sqrt have "... = real (p * n\)" by simp finally have eq: "m\ = p * n\" .. hence "p dvd m\" .. - with p_prime have dvd_m: "p dvd m" by (rule prime_dvd_square) + with p_prime have dvd_m: "p dvd m" by (rule prime_dvd_power_two) then obtain k where "m = p * k" .. - with eq have "p * n\ = p\ * k\" by (auto simp add: mult_ac) - with p have "n\ = p * k\" by simp + with eq have "p * n\ = p\ * k\" by (auto simp add: power_two mult_ac) + with p have "n\ = p * k\" by (simp add: power_two) hence "p dvd n\" .. - with p_prime have "p dvd n" by (rule prime_dvd_square) + with p_prime have "p dvd n" by (rule prime_dvd_power_two) with dvd_m have "p dvd gcd (m, n)" by (rule gcd_greatest) with gcd have "p dvd 1" by simp hence "p \ 1" by (simp add: dvd_imp_le)