author nipkow Wed, 01 Dec 2010 20:59:29 +0100 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 | comparison | revisions src/HOL/Ln.thy file | annotate | diff | comparison | revisions src/HOL/RealDef.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Complex_Main.thy	Wed Dec 01 06:50:54 2010 -0800
+++ b/src/HOL/Complex_Main.thy	Wed Dec 01 20:59:29 2010 +0100
@@ -10,9 +10,6 @@
Ln
Taylor
Deriv
-uses "~~/src/Tools/subtyping.ML"
begin

-setup Subtyping.setup
-
end```
```--- a/src/HOL/Ln.thy	Wed Dec 01 06:50:54 2010 -0800
+++ b/src/HOL/Ln.thy	Wed Dec 01 20:59:29 2010 +0100
@@ -9,13 +9,13 @@
begin

lemma exp_first_two_terms: "exp x = 1 + x + suminf (%n.
-  inverse(real (fact (n+2))) * (x ^ (n+2)))"
+  inverse(fact (n+2)) * (x ^ (n+2)))"
proof -
-  have "exp x = suminf (%n. inverse(real (fact n)) * (x ^ n))"
+  have "exp x = suminf (%n. inverse(fact n) * (x ^ n))"
-  also from summable_exp have "... = (SUM n : {0..<2}.
-      inverse(real (fact n)) * (x ^ n)) + suminf (%n.
-      inverse(real (fact (n+2))) * (x ^ (n+2)))" (is "_ = ?a + _")
+  also from summable_exp have "... = (SUM n::nat : {0..<2}.
+      inverse(fact n) * (x ^ n)) + suminf (%n.
+      inverse(fact(n+2)) * (x ^ (n+2)))" (is "_ = ?a + _")
by (rule suminf_split_initial_segment)
also have "?a = 1 + x"
@@ -23,7 +23,7 @@
qed

lemma exp_tail_after_first_two_terms_summable:
-  "summable (%n. inverse(real (fact (n+2))) * (x ^ (n+2)))"
+  "summable (%n. inverse(fact (n+2)) * (x ^ (n+2)))"
proof -
note summable_exp
thus ?thesis
@@ -31,20 +31,19 @@
qed

lemma aux1: assumes a: "0 <= x" and b: "x <= 1"
-    shows "inverse (real (fact ((n::nat) + 2))) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)"
+    shows "inverse (fact ((n::nat) + 2)) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)"
proof (induct n)
-  show "inverse (real (fact ((0::nat) + 2))) * x ^ (0 + 2) <=
+  show "inverse (fact ((0::nat) + 2)) * x ^ (0 + 2) <=
x ^ 2 / 2 * (1 / 2) ^ 0"
next
fix n :: nat
-  assume c: "inverse (real (fact (n + 2))) * x ^ (n + 2)
+  assume c: "inverse (fact (n + 2)) * x ^ (n + 2)
<= x ^ 2 / 2 * (1 / 2) ^ n"
-  show "inverse (real (fact (Suc n + 2))) * x ^ (Suc n + 2)
+  show "inverse (fact (Suc n + 2)) * x ^ (Suc n + 2)
<= x ^ 2 / 2 * (1 / 2) ^ Suc n"
proof -
-    have "inverse(real (fact (Suc n + 2))) <=
-        (1 / 2) *inverse (real (fact (n+2)))"
+    have "inverse(fact (Suc n + 2)) <= (1/2) * inverse (fact (n+2))"
proof -
have "Suc n + 2 = Suc (n + 2)" by simp
then have "fact (Suc n + 2) = Suc (n + 2) * fact (n + 2)"
@@ -57,12 +56,12 @@
by (rule real_of_nat_mult)
finally have "real (fact (Suc n + 2)) =
real (Suc (n + 2)) * real (fact (n + 2))" .
-      then have "inverse(real (fact (Suc n + 2))) =
-         inverse(real (Suc (n + 2))) * inverse(real (fact (n + 2)))"
+      then have "inverse(fact (Suc n + 2)) =
+         inverse(Suc (n + 2)) * inverse(fact (n + 2))"
apply (rule ssubst)
apply (rule inverse_mult_distrib)
done
-      also have "... <= (1/2) * inverse(real (fact (n + 2)))"
+      also have "... <= (1/2) * inverse(fact (n + 2))"
apply (rule mult_right_mono)
apply (subst inverse_eq_divide)
apply simp
@@ -78,8 +77,8 @@
apply (rule mult_nonneg_nonneg, rule a)+
apply (rule zero_le_power, rule a)
done
-    ultimately have "inverse (real (fact (Suc n + 2))) *  x ^ (Suc n + 2) <=
-        (1 / 2 * inverse (real (fact (n + 2)))) * x ^ (n + 2)"
+    ultimately have "inverse (fact (Suc n + 2)) *  x ^ (Suc n + 2) <=
+        (1 / 2 * inverse (fact (n + 2))) * x ^ (n + 2)"
apply (rule mult_mono)
apply (rule mult_nonneg_nonneg)
apply simp
@@ -88,7 +87,7 @@
apply (rule zero_le_power)
apply (rule a)
done
-    also have "... = 1 / 2 * (inverse (real (fact (n + 2))) * x ^ (n + 2))"
+    also have "... = 1 / 2 * (inverse (fact (n + 2)) * x ^ (n + 2))"
by simp
also have "... <= 1 / 2 * (x ^ 2 / 2 * (1 / 2) ^ n)"
apply (rule mult_left_mono)
@@ -122,12 +121,12 @@
proof -
assume a: "0 <= x"
assume b: "x <= 1"
-  have c: "exp x = 1 + x + suminf (%n. inverse(real (fact (n+2))) *
+  have c: "exp x = 1 + x + suminf (%n. inverse(fact (n+2)) *
(x ^ (n+2)))"
by (rule exp_first_two_terms)
-  moreover have "suminf (%n. inverse(real (fact (n+2))) * (x ^ (n+2))) <= x^2"
+  moreover have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <= x^2"
proof -
-    have "suminf (%n. inverse(real (fact (n+2))) * (x ^ (n+2))) <=
+    have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <=
suminf (%n. (x^2/2) * ((1/2)^n))"
apply (rule summable_le)
apply (auto simp only: aux1 prems)```
```--- a/src/HOL/RealDef.thy	Wed Dec 01 06:50:54 2010 -0800
+++ b/src/HOL/RealDef.thy	Wed Dec 01 20:59:29 2010 +0100
@@ -9,6 +9,7 @@

theory RealDef
imports Rat
+uses "~~/src/Tools/subtyping.ML"
begin

text {*
@@ -1109,6 +1110,11 @@
real_of_nat_def [code_unfold]: "real == real_of_nat"
real_of_int_def [code_unfold]: "real == real_of_int"

+setup Subtyping.setup
+
+declare [[coercion "real::nat\<Rightarrow>real"]]
+declare [[coercion "real::int\<Rightarrow>real"]]
+
lemma real_eq_of_nat: "real = of_nat"
unfolding real_of_nat_def ..
```