equal
deleted
inserted
replaced
10 uses ("Tools/float_syntax.ML") |
10 uses ("Tools/float_syntax.ML") |
11 begin |
11 begin |
12 |
12 |
13 declare abs_mult_self [simp] |
13 declare abs_mult_self [simp] |
14 |
14 |
15 instantiation real :: recpower |
15 instance real :: recpower .. |
16 begin |
|
17 |
|
18 primrec power_real where |
|
19 "r ^ 0 = (1\<Colon>real)" |
|
20 | "r ^ Suc n = (r\<Colon>real) * r ^ n" |
|
21 |
|
22 instance proof |
|
23 fix z :: real |
|
24 fix n :: nat |
|
25 show "z^0 = 1" by simp |
|
26 show "z^(Suc n) = z * (z^n)" by simp |
|
27 qed |
|
28 |
|
29 declare power_real.simps [simp del] |
|
30 |
|
31 end |
|
32 |
|
33 |
16 |
34 lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n" |
17 lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n" |
35 by simp |
18 by simp |
36 |
19 |
37 lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n" |
20 lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n" |
45 lemma realpow_Suc_le_self: "[| 0 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> r" |
28 lemma realpow_Suc_le_self: "[| 0 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> r" |
46 by (insert power_decreasing [of 1 "Suc n" r], simp) |
29 by (insert power_decreasing [of 1 "Suc n" r], simp) |
47 |
30 |
48 lemma realpow_minus_mult [rule_format]: |
31 lemma realpow_minus_mult [rule_format]: |
49 "0 < n --> (x::real) ^ (n - 1) * x = x ^ n" |
32 "0 < n --> (x::real) ^ (n - 1) * x = x ^ n" |
50 unfolding One_nat_def |
|
51 apply (simp split add: nat_diff_split) |
33 apply (simp split add: nat_diff_split) |
52 done |
34 done |
53 |
35 |
54 lemma realpow_two_mult_inverse [simp]: |
36 lemma realpow_two_mult_inverse [simp]: |
55 "r \<noteq> 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)" |
37 "r \<noteq> 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)" |