1.1 --- a/src/HOL/Complex/ex/Sqrt.thy	Tue Aug 26 11:42:46 2008 +0200
     1.2 +++ b/src/HOL/Complex/ex/Sqrt.thy	Tue Aug 26 12:07:06 2008 +0200
     1.3 @@ -10,56 +10,10 @@
     1.4  imports Primes Complex_Main
     1.5  begin
     1.6  
     1.7 -subsection {* Preliminaries *}
     1.8 +text {* The definition and the key representation theorem for the set of
     1.9 +rational numbers has been moved to a core theory.  *}
    1.10  
    1.11 -text {*
    1.12 -  The set of rational numbers, including the key representation
    1.13 -  theorem.
    1.14 -*}
    1.15 -
    1.16 -definition
    1.17 -  rationals  ("\<rat>") where
    1.18 -  "\<rat> = {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
    1.19 -
    1.20 -theorem rationals_rep [elim?]:
    1.21 -  assumes "x \<in> \<rat>"
    1.22 -  obtains m n where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd m n = 1"
    1.23 -proof -
    1.24 -  from `x \<in> \<rat>` obtain m n :: nat where
    1.25 -      n: "n \<noteq> 0" and x_rat: "\<bar>x\<bar> = real m / real n"
    1.26 -    unfolding rationals_def by blast
    1.27 -  let ?gcd = "gcd m n"
    1.28 -  from n have gcd: "?gcd \<noteq> 0" by (simp add: gcd_zero)
    1.29 -  let ?k = "m div ?gcd"
    1.30 -  let ?l = "n div ?gcd"
    1.31 -  let ?gcd' = "gcd ?k ?l"
    1.32 -  have "?gcd dvd m" .. then have gcd_k: "?gcd * ?k = m"
    1.33 -    by (rule dvd_mult_div_cancel)
    1.34 -  have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n"
    1.35 -    by (rule dvd_mult_div_cancel)
    1.36 -
    1.37 -  from n and gcd_l have "?l \<noteq> 0"
    1.38 -    by (auto iff del: neq0_conv)
    1.39 -  moreover
    1.40 -  have "\<bar>x\<bar> = real ?k / real ?l"
    1.41 -  proof -
    1.42 -    from gcd have "real ?k / real ?l =
    1.43 -        real (?gcd * ?k) / real (?gcd * ?l)" by simp
    1.44 -    also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp
    1.45 -    also from x_rat have "\<dots> = \<bar>x\<bar>" ..
    1.46 -    finally show ?thesis ..
    1.47 -  qed
    1.48 -  moreover
    1.49 -  have "?gcd' = 1"
    1.50 -  proof -
    1.51 -    have "?gcd * ?gcd' = gcd (?gcd * ?k) (?gcd * ?l)"
    1.52 -      by (rule gcd_mult_distrib2)
    1.53 -    with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
    1.54 -    with gcd show ?thesis by simp
    1.55 -  qed
    1.56 -  ultimately show ?thesis ..
    1.57 -qed
    1.58 -
    1.59 +declare Rats_abs_nat_div_natE[elim?]
    1.60  
    1.61  subsection {* Main theorem *}
    1.62