moved activation of coercion inference into RealDef and declared function real a coercion.
authornipkow
Wed Dec 01 20:59:29 2010 +0100 (2010-12-01)
changeset 408644abaaadfdaf2
parent 40854 f2c9ebbe04aa
child 40865 ed30aeccf949
moved activation of coercion inference into RealDef and declared function real a coercion.
Made use of it in theory Ln.
src/HOL/Complex_Main.thy
src/HOL/Ln.thy
src/HOL/RealDef.thy
     1.1 --- a/src/HOL/Complex_Main.thy	Wed Dec 01 06:50:54 2010 -0800
     1.2 +++ b/src/HOL/Complex_Main.thy	Wed Dec 01 20:59:29 2010 +0100
     1.3 @@ -10,9 +10,6 @@
     1.4    Ln
     1.5    Taylor
     1.6    Deriv
     1.7 -uses "~~/src/Tools/subtyping.ML"
     1.8  begin
     1.9  
    1.10 -setup Subtyping.setup
    1.11 -
    1.12  end
     2.1 --- a/src/HOL/Ln.thy	Wed Dec 01 06:50:54 2010 -0800
     2.2 +++ b/src/HOL/Ln.thy	Wed Dec 01 20:59:29 2010 +0100
     2.3 @@ -9,13 +9,13 @@
     2.4  begin
     2.5  
     2.6  lemma exp_first_two_terms: "exp x = 1 + x + suminf (%n. 
     2.7 -  inverse(real (fact (n+2))) * (x ^ (n+2)))"
     2.8 +  inverse(fact (n+2)) * (x ^ (n+2)))"
     2.9  proof -
    2.10 -  have "exp x = suminf (%n. inverse(real (fact n)) * (x ^ n))"
    2.11 +  have "exp x = suminf (%n. inverse(fact n) * (x ^ n))"
    2.12      by (simp add: exp_def)
    2.13 -  also from summable_exp have "... = (SUM n : {0..<2}. 
    2.14 -      inverse(real (fact n)) * (x ^ n)) + suminf (%n.
    2.15 -      inverse(real (fact (n+2))) * (x ^ (n+2)))" (is "_ = ?a + _")
    2.16 +  also from summable_exp have "... = (SUM n::nat : {0..<2}. 
    2.17 +      inverse(fact n) * (x ^ n)) + suminf (%n.
    2.18 +      inverse(fact(n+2)) * (x ^ (n+2)))" (is "_ = ?a + _")
    2.19      by (rule suminf_split_initial_segment)
    2.20    also have "?a = 1 + x"
    2.21      by (simp add: numerals)
    2.22 @@ -23,7 +23,7 @@
    2.23  qed
    2.24  
    2.25  lemma exp_tail_after_first_two_terms_summable: 
    2.26 -  "summable (%n. inverse(real (fact (n+2))) * (x ^ (n+2)))"
    2.27 +  "summable (%n. inverse(fact (n+2)) * (x ^ (n+2)))"
    2.28  proof -
    2.29    note summable_exp
    2.30    thus ?thesis
    2.31 @@ -31,20 +31,19 @@
    2.32  qed
    2.33  
    2.34  lemma aux1: assumes a: "0 <= x" and b: "x <= 1"
    2.35 -    shows "inverse (real (fact ((n::nat) + 2))) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)"
    2.36 +    shows "inverse (fact ((n::nat) + 2)) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)"
    2.37  proof (induct n)
    2.38 -  show "inverse (real (fact ((0::nat) + 2))) * x ^ (0 + 2) <= 
    2.39 +  show "inverse (fact ((0::nat) + 2)) * x ^ (0 + 2) <= 
    2.40        x ^ 2 / 2 * (1 / 2) ^ 0"
    2.41      by (simp add: real_of_nat_Suc power2_eq_square)
    2.42  next
    2.43    fix n :: nat
    2.44 -  assume c: "inverse (real (fact (n + 2))) * x ^ (n + 2)
    2.45 +  assume c: "inverse (fact (n + 2)) * x ^ (n + 2)
    2.46         <= x ^ 2 / 2 * (1 / 2) ^ n"
    2.47 -  show "inverse (real (fact (Suc n + 2))) * x ^ (Suc n + 2)
    2.48 +  show "inverse (fact (Suc n + 2)) * x ^ (Suc n + 2)
    2.49             <= x ^ 2 / 2 * (1 / 2) ^ Suc n"
    2.50    proof -
    2.51 -    have "inverse(real (fact (Suc n + 2))) <= 
    2.52 -        (1 / 2) *inverse (real (fact (n+2)))"
    2.53 +    have "inverse(fact (Suc n + 2)) <= (1/2) * inverse (fact (n+2))"
    2.54      proof -
    2.55        have "Suc n + 2 = Suc (n + 2)" by simp
    2.56        then have "fact (Suc n + 2) = Suc (n + 2) * fact (n + 2)" 
    2.57 @@ -57,12 +56,12 @@
    2.58          by (rule real_of_nat_mult)
    2.59        finally have "real (fact (Suc n + 2)) = 
    2.60           real (Suc (n + 2)) * real (fact (n + 2))" .
    2.61 -      then have "inverse(real (fact (Suc n + 2))) = 
    2.62 -         inverse(real (Suc (n + 2))) * inverse(real (fact (n + 2)))"
    2.63 +      then have "inverse(fact (Suc n + 2)) = 
    2.64 +         inverse(Suc (n + 2)) * inverse(fact (n + 2))"
    2.65          apply (rule ssubst)
    2.66          apply (rule inverse_mult_distrib)
    2.67          done
    2.68 -      also have "... <= (1/2) * inverse(real (fact (n + 2)))"
    2.69 +      also have "... <= (1/2) * inverse(fact (n + 2))"
    2.70          apply (rule mult_right_mono)
    2.71          apply (subst inverse_eq_divide)
    2.72          apply simp
    2.73 @@ -78,8 +77,8 @@
    2.74        apply (rule mult_nonneg_nonneg, rule a)+
    2.75        apply (rule zero_le_power, rule a)
    2.76        done
    2.77 -    ultimately have "inverse (real (fact (Suc n + 2))) *  x ^ (Suc n + 2) <=
    2.78 -        (1 / 2 * inverse (real (fact (n + 2)))) * x ^ (n + 2)"
    2.79 +    ultimately have "inverse (fact (Suc n + 2)) *  x ^ (Suc n + 2) <=
    2.80 +        (1 / 2 * inverse (fact (n + 2))) * x ^ (n + 2)"
    2.81        apply (rule mult_mono)
    2.82        apply (rule mult_nonneg_nonneg)
    2.83        apply simp
    2.84 @@ -88,7 +87,7 @@
    2.85        apply (rule zero_le_power)
    2.86        apply (rule a)
    2.87        done
    2.88 -    also have "... = 1 / 2 * (inverse (real (fact (n + 2))) * x ^ (n + 2))"
    2.89 +    also have "... = 1 / 2 * (inverse (fact (n + 2)) * x ^ (n + 2))"
    2.90        by simp
    2.91      also have "... <= 1 / 2 * (x ^ 2 / 2 * (1 / 2) ^ n)"
    2.92        apply (rule mult_left_mono)
    2.93 @@ -122,12 +121,12 @@
    2.94  proof -
    2.95    assume a: "0 <= x"
    2.96    assume b: "x <= 1"
    2.97 -  have c: "exp x = 1 + x + suminf (%n. inverse(real (fact (n+2))) * 
    2.98 +  have c: "exp x = 1 + x + suminf (%n. inverse(fact (n+2)) * 
    2.99        (x ^ (n+2)))"
   2.100      by (rule exp_first_two_terms)
   2.101 -  moreover have "suminf (%n. inverse(real (fact (n+2))) * (x ^ (n+2))) <= x^2"
   2.102 +  moreover have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <= x^2"
   2.103    proof -
   2.104 -    have "suminf (%n. inverse(real (fact (n+2))) * (x ^ (n+2))) <=
   2.105 +    have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <=
   2.106          suminf (%n. (x^2/2) * ((1/2)^n))"
   2.107        apply (rule summable_le)
   2.108        apply (auto simp only: aux1 prems)
     3.1 --- a/src/HOL/RealDef.thy	Wed Dec 01 06:50:54 2010 -0800
     3.2 +++ b/src/HOL/RealDef.thy	Wed Dec 01 20:59:29 2010 +0100
     3.3 @@ -9,6 +9,7 @@
     3.4  
     3.5  theory RealDef
     3.6  imports Rat
     3.7 +uses "~~/src/Tools/subtyping.ML"
     3.8  begin
     3.9  
    3.10  text {*
    3.11 @@ -1109,6 +1110,11 @@
    3.12    real_of_nat_def [code_unfold]: "real == real_of_nat"
    3.13    real_of_int_def [code_unfold]: "real == real_of_int"
    3.14  
    3.15 +setup Subtyping.setup
    3.16 +
    3.17 +declare [[coercion "real::nat\<Rightarrow>real"]]
    3.18 +declare [[coercion "real::int\<Rightarrow>real"]]
    3.19 +
    3.20  lemma real_eq_of_nat: "real = of_nat"
    3.21    unfolding real_of_nat_def ..
    3.22