author paulson Mon Mar 08 11:12:06 2004 +0100 (2004-03-08) changeset 14443 75910c7557c5 parent 14442 04135b0c06ff child 14444 24724afce166
generic theorems about exponentials; general tidying up
 src/HOL/Complex/Complex.thy file | annotate | diff | revisions src/HOL/Complex/NSComplex.thy file | annotate | diff | revisions src/HOL/Finite_Set.thy file | annotate | diff | revisions src/HOL/Hyperreal/HyperPow.thy file | annotate | diff | revisions src/HOL/Integ/NatBin.thy file | annotate | diff | revisions src/HOL/Integ/Parity.thy file | annotate | diff | revisions src/HOL/Main.thy file | annotate | diff | revisions src/HOL/Numeral.thy file | annotate | diff | revisions src/HOL/Real/RealDef.thy file | annotate | diff | revisions src/HOL/Real/RealPow.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Complex/Complex.thy	Mon Mar 08 11:11:58 2004 +0100
1.2 +++ b/src/HOL/Complex/Complex.thy	Mon Mar 08 11:12:06 2004 +0100
1.3 @@ -601,10 +601,6 @@
1.4  apply (auto simp add: complex_mod_mult)
1.5  done
1.6
1.7 -lemma complexpow_minus:
1.8 -     "(-x::complex) ^ n = (if even n then (x ^ n) else -(x ^ n))"
1.9 -by (induct_tac "n", auto)
1.10 -
1.11  lemma complexpow_i_squared [simp]: "ii ^ 2 = -(1::complex)"
1.12  by (simp add: i_def complex_mult complex_one_def complex_minus numeral_2_eq_2)
1.13
1.14 @@ -1065,7 +1061,6 @@
1.15  val complex_Re_le_cmod = thm"complex_Re_le_cmod";
1.16  val complex_mod_gt_zero = thm"complex_mod_gt_zero";
1.17  val complex_mod_complexpow = thm"complex_mod_complexpow";
1.18 -val complexpow_minus = thm"complexpow_minus";
1.19  val complex_mod_inverse = thm"complex_mod_inverse";
1.20  val complex_mod_divide = thm"complex_mod_divide";
1.21  val complexpow_i_squared = thm"complexpow_i_squared";
```
```     2.1 --- a/src/HOL/Complex/NSComplex.thy	Mon Mar 08 11:11:58 2004 +0100
2.2 +++ b/src/HOL/Complex/NSComplex.thy	Mon Mar 08 11:12:06 2004 +0100
2.3 @@ -932,17 +932,13 @@
2.4  apply (auto simp add: hcmod_mult)
2.5  done
2.6
2.7 -lemma hcomplexpow_minus:
2.8 -     "(-x::hcomplex) ^ n = (if even n then (x ^ n) else -(x ^ n))"
2.9 -by (induct_tac "n", auto)
2.10 -
2.11  lemma hcpow_minus:
2.12       "(-x::hcomplex) hcpow n =
2.13        (if ( *pNat* even) n then (x hcpow n) else -(x hcpow n))"
2.14  apply (rule eq_Abs_hcomplex [of x])
2.15  apply (rule eq_Abs_hypnat [of n])
2.16  apply (auto simp add: hcpow hyperpow starPNat hcomplex_minus, ultra)
2.17 -apply (auto simp add: complexpow_minus, ultra)
2.18 +apply (auto simp add: neg_power_if, ultra)
2.19  done
2.20
2.21  lemma hcpow_mult: "((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)"
2.22 @@ -1709,7 +1705,6 @@
2.23  val hcomplex_of_hypreal_hyperpow = thm"hcomplex_of_hypreal_hyperpow";
2.24  val hcmod_hcomplexpow = thm"hcmod_hcomplexpow";
2.25  val hcmod_hcpow = thm"hcmod_hcpow";
2.26 -val hcomplexpow_minus = thm"hcomplexpow_minus";
2.27  val hcpow_minus = thm"hcpow_minus";
2.28  val hcmod_hcomplex_inverse = thm"hcmod_hcomplex_inverse";
2.29  val hcmod_divide = thm"hcmod_divide";
```
```     3.1 --- a/src/HOL/Finite_Set.thy	Mon Mar 08 11:11:58 2004 +0100
3.2 +++ b/src/HOL/Finite_Set.thy	Mon Mar 08 11:12:06 2004 +0100
3.3 @@ -1423,4 +1423,5 @@
3.4      "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
3.6
3.7 +
3.8  end
```
```     4.1 --- a/src/HOL/Hyperreal/HyperPow.thy	Mon Mar 08 11:11:58 2004 +0100
4.2 +++ b/src/HOL/Hyperreal/HyperPow.thy	Mon Mar 08 11:12:06 2004 +0100
4.3 @@ -37,8 +37,7 @@
4.4                          hyprel``{%n::nat. (X n) ^ (Y n)})"
4.5
4.6  lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
4.7 -apply (simp (no_asm))
4.8 -done
4.9 +by simp
4.10
4.11  lemma hrealpow_two_le: "(0::hypreal) \<le> r ^ Suc (Suc 0)"
4.12  by (auto simp add: zero_le_mult_iff)
4.13 @@ -46,8 +45,7 @@
4.14
4.16       "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)"
4.17 -apply (simp only: hrealpow_two_le hypreal_le_add_order)
4.18 -done
4.19 +by (simp only: hrealpow_two_le hypreal_le_add_order)
4.21
```
```     5.1 --- a/src/HOL/Integ/NatBin.thy	Mon Mar 08 11:11:58 2004 +0100
5.2 +++ b/src/HOL/Integ/NatBin.thy	Mon Mar 08 11:12:06 2004 +0100
5.3 @@ -296,6 +296,12 @@
5.5  done
5.6
5.7 +lemma power_even_eq: "(a::'a::ringpower) ^ (2*n) = (a^n)^2"
5.8 +by (simp add: power_mult power_mult_distrib power2_eq_square)
5.9 +
5.10 +lemma power_odd_eq: "(a::int) ^ Suc(2*n) = a * (a^n)^2"
5.12 +
5.13  lemma power_minus_even [simp]:
5.14       "(-a) ^ (2*n) = (a::'a::{ring,ringpower}) ^ (2*n)"
5.15  by (simp add: power_minus1_even power_minus [of a])
5.16 @@ -510,15 +516,8 @@
5.17  declare power_nat_number_of [of _ "number_of w", standard, simp]
5.18
5.19
5.20 -
5.21  text{*For the integers*}
5.22
5.23 -lemma zpower_even: "(z::int) ^ (2*a) = (z^a)^2"
5.24 -by (simp add: zpower_zpower mult_commute)
5.25 -
5.26 -lemma zpower_odd: "(z::int) ^ (2*a + 1) = z * (z^a)^2"
5.28 -
5.29  lemma zpower_number_of_even:
5.30       "(z::int) ^ number_of (w BIT False) =
5.31        (let w = z ^ (number_of w) in  w*w)"
5.32 @@ -526,7 +525,7 @@
5.34  apply (rule_tac x = "number_of w" in spec, clarify)
5.35  apply (case_tac " (0::int) <= x")
5.36 -apply (auto simp add: nat_mult_distrib zpower_even power2_eq_square)
5.37 +apply (auto simp add: nat_mult_distrib power_even_eq power2_eq_square)
5.38  done
5.39
5.40  lemma zpower_number_of_odd:
5.41 @@ -537,7 +536,7 @@
5.42  apply (simp del: nat_number_of  add: nat_number_of_def number_of_BIT Let_def)
5.43  apply (simp only: number_of_add nat_numeral_1_eq_1 not_neg_eq_ge_0 neg_eq_less_0)
5.44  apply (rule_tac x = "number_of w" in spec, clarify)
5.47  done
5.48
5.49  declare zpower_number_of_even [of "number_of v", standard, simp]
5.50 @@ -604,6 +603,12 @@
5.51  lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
5.53
5.54 +lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring,ringpower})"
5.56 +
5.57 +lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring,ringpower})"
5.58 +by (simp add: power_mult power_Suc);
5.59 +
5.60
5.61  subsection{*Literal arithmetic and @{term of_nat}*}
5.62
5.63 @@ -769,8 +774,6 @@
5.64  val of_nat_number_of_eq = thm"of_nat_number_of_eq";
5.65  val nat_power_eq = thm"nat_power_eq";
5.66  val power_nat_number_of = thm"power_nat_number_of";
5.67 -val zpower_even = thm"zpower_even";
5.68 -val zpower_odd = thm"zpower_odd";
5.69  val zpower_number_of_even = thm"zpower_number_of_even";
5.70  val zpower_number_of_odd = thm"zpower_number_of_odd";
5.71  val nat_number_of_Pls = thm"nat_number_of_Pls";
5.72 @@ -801,7 +804,6 @@
5.73  val nat_mult_eq_cancel_disj = thm"nat_mult_eq_cancel_disj";
5.74  val nat_mult_div_cancel_disj = thm"nat_mult_div_cancel_disj";
5.75
5.76 -val power_minus1_even = thm"power_minus1_even";
5.77  val power_minus_even = thm"power_minus_even";
5.78  val zero_le_even_power = thm"zero_le_even_power";
5.79  *}
```
```     6.1 --- a/src/HOL/Integ/Parity.thy	Mon Mar 08 11:11:58 2004 +0100
6.2 +++ b/src/HOL/Integ/Parity.thy	Mon Mar 08 11:12:06 2004 +0100
6.3 @@ -249,6 +249,11 @@
6.4       "odd x ==> (-1::'a::{number_ring,ringpower})^x = -1"
6.5    by (rule neg_one_even_odd_power [THEN conjunct2, THEN mp], assumption)
6.6
6.7 +lemma neg_power_if:
6.8 +     "(-x::'a::{ring,ringpower}) ^ n =
6.9 +      (if even n then (x ^ n) else -(x ^ n))"
6.10 +  by (induct n, simp_all split: split_if_asm add: power_Suc)
6.11 +
6.12
6.13  subsection {* Miscellaneous *}
6.14
```
```     7.1 --- a/src/HOL/Main.thy	Mon Mar 08 11:11:58 2004 +0100
7.2 +++ b/src/HOL/Main.thy	Mon Mar 08 11:12:06 2004 +0100
7.3 @@ -6,7 +6,7 @@
7.4
7.5  header {* Main HOL *}
7.6
7.7 -theory Main = Map + Hilbert_Choice + Extraction + Refute:
7.8 +theory Main = Map + Infinite_Set + Extraction + Refute:
7.9
7.10  text {*
7.11    Theory @{text Main} includes everything.  Note that theory @{text
```
```     8.1 --- a/src/HOL/Numeral.thy	Mon Mar 08 11:11:58 2004 +0100
8.2 +++ b/src/HOL/Numeral.thy	Mon Mar 08 11:12:06 2004 +0100
8.3 @@ -69,8 +69,6 @@
8.4
8.5
8.6  consts
8.7 -  ring_of :: "bin => 'a::ring"
8.8 -
8.9    NCons     :: "[bin,bool]=>bin"
8.10    bin_succ  :: "bin=>bin"
8.11    bin_pred  :: "bin=>bin"
8.12 @@ -85,12 +83,6 @@
8.13    NCons_BIT:  "NCons (w BIT x) b = (w BIT x) BIT b"
8.14
8.15
8.16 -primrec
8.17 -  ring_of_Pls: "ring_of bin.Pls = 0"
8.18 -  ring_of_Min: "ring_of bin.Min = - (1::'a::ring)"
8.19 -  ring_of_BIT: "ring_of(w BIT x) = (if x then 1 else 0) +
8.20 -	                               (ring_of w) + (ring_of w)"
8.21 -
8.22  primrec
8.23    bin_succ_Pls: "bin_succ bin.Pls = bin.Pls BIT True"
8.24    bin_succ_Min: "bin_succ bin.Min = bin.Pls"
```
```     9.1 --- a/src/HOL/Real/RealDef.thy	Mon Mar 08 11:11:58 2004 +0100
9.2 +++ b/src/HOL/Real/RealDef.thy	Mon Mar 08 11:12:06 2004 +0100
9.3 @@ -924,9 +924,6 @@
9.4  lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))"
9.5  by (unfold real_abs_def, simp)
9.6
9.7 -lemma abs_minus_one [simp]: "abs (-1) = (1::real)"
9.8 -by (unfold real_abs_def, simp)
9.9 -
9.10  lemma abs_interval_iff: "(abs x < r) = (-r < x & x < (r::real))"
9.11  by (force simp add: Ring_and_Field.abs_less_iff)
9.12
9.13 @@ -983,7 +980,6 @@
9.14  val abs_triangle_ineq = thm"abs_triangle_ineq";
9.15  val abs_minus_cancel = thm"abs_minus_cancel";
9.17 -val abs_minus_one = thm"abs_minus_one";
9.18  val abs_interval_iff = thm"abs_interval_iff";
9.19  val abs_le_interval_iff = thm"abs_le_interval_iff";
```
```    10.1 --- a/src/HOL/Real/RealPow.thy	Mon Mar 08 11:11:58 2004 +0100
10.2 +++ b/src/HOL/Real/RealPow.thy	Mon Mar 08 11:12:06 2004 +0100
10.3 @@ -42,9 +42,6 @@
10.4  apply (rule power_strict_mono, auto)
10.5  done
10.6
10.7 -lemma abs_realpow_minus_one [simp]: "abs((-1) ^ n) = (1::real)"
10.9 -
10.10  lemma realpow_two_le [simp]: "(0::real) \<le> r^ Suc (Suc 0)"
10.12
10.13 @@ -65,15 +62,6 @@
10.14  apply (auto simp add: two_realpow_ge_one)
10.15  done
10.16
10.17 -lemma realpow_minus_one [simp]: "(-1) ^ (2*n) = (1::real)"
10.18 -by (induct_tac "n", auto)
10.19 -
10.20 -lemma realpow_minus_one_odd [simp]: "(-1) ^ Suc (2*n) = -(1::real)"
10.21 -by auto
10.22 -
10.23 -lemma realpow_minus_one_even [simp]: "(-1) ^ Suc (Suc (2*n)) = (1::real)"
10.24 -by auto
10.25 -
10.26  lemma realpow_Suc_le_self: "[| 0 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> r"
10.27  by (insert power_decreasing [of 1 "Suc n" r], simp)
10.28
10.29 @@ -264,15 +252,11 @@
10.30  val realpow_zero_zero = thm "realpow_zero_zero";
10.31  val realpow_two = thm "realpow_two";
10.32  val realpow_less = thm "realpow_less";
10.33 -val abs_realpow_minus_one = thm "abs_realpow_minus_one";
10.34  val realpow_two_le = thm "realpow_two_le";
10.35  val abs_realpow_two = thm "abs_realpow_two";
10.36  val realpow_two_abs = thm "realpow_two_abs";
10.37  val two_realpow_ge_one = thm "two_realpow_ge_one";
10.38  val two_realpow_gt = thm "two_realpow_gt";
10.39 -val realpow_minus_one = thm "realpow_minus_one";
10.40 -val realpow_minus_one_odd = thm "realpow_minus_one_odd";
10.41 -val realpow_minus_one_even = thm "realpow_minus_one_even";
10.42  val realpow_Suc_le_self = thm "realpow_Suc_le_self";
10.43  val realpow_Suc_less_one = thm "realpow_Suc_less_one";
10.44  val realpow_minus_mult = thm "realpow_minus_mult";
```