author nipkow Wed Dec 01 20:59:29 2010 +0100 (2010-12-01) changeset 40864 4abaaadfdaf2 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 file | annotate | diff | revisions src/HOL/Ln.thy file | annotate | diff | revisions src/HOL/RealDef.thy file | annotate | diff | revisions
```     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.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.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
```