author paulson Mon, 08 Mar 2004 11:12:06 +0100 changeset 14443 75910c7557c5 parent 14442 04135b0c06ff child 14444 24724afce166
generic theorems about exponentials; general tidying up
 src/HOL/Complex/Complex.thy file | annotate | diff | comparison | revisions src/HOL/Complex/NSComplex.thy file | annotate | diff | comparison | revisions src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions src/HOL/Hyperreal/HyperPow.thy file | annotate | diff | comparison | revisions src/HOL/Integ/NatBin.thy file | annotate | diff | comparison | revisions src/HOL/Integ/Parity.thy file | annotate | diff | comparison | revisions src/HOL/Main.thy file | annotate | diff | comparison | revisions src/HOL/Numeral.thy file | annotate | diff | comparison | revisions src/HOL/Real/RealDef.thy file | annotate | diff | comparison | revisions src/HOL/Real/RealPow.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Complex/Complex.thy	Mon Mar 08 11:11:58 2004 +0100
+++ b/src/HOL/Complex/Complex.thy	Mon Mar 08 11:12:06 2004 +0100
@@ -601,10 +601,6 @@
done

-lemma complexpow_minus:
-     "(-x::complex) ^ n = (if even n then (x ^ n) else -(x ^ n))"
-by (induct_tac "n", auto)
-
lemma complexpow_i_squared [simp]: "ii ^ 2 = -(1::complex)"
by (simp add: i_def complex_mult complex_one_def complex_minus numeral_2_eq_2)

@@ -1065,7 +1061,6 @@
val complex_Re_le_cmod = thm"complex_Re_le_cmod";
val complex_mod_gt_zero = thm"complex_mod_gt_zero";
val complex_mod_complexpow = thm"complex_mod_complexpow";
-val complexpow_minus = thm"complexpow_minus";
val complex_mod_inverse = thm"complex_mod_inverse";
val complex_mod_divide = thm"complex_mod_divide";
val complexpow_i_squared = thm"complexpow_i_squared";```
```--- a/src/HOL/Complex/NSComplex.thy	Mon Mar 08 11:11:58 2004 +0100
+++ b/src/HOL/Complex/NSComplex.thy	Mon Mar 08 11:12:06 2004 +0100
@@ -932,17 +932,13 @@
done

-lemma hcomplexpow_minus:
-     "(-x::hcomplex) ^ n = (if even n then (x ^ n) else -(x ^ n))"
-by (induct_tac "n", auto)
-
lemma hcpow_minus:
"(-x::hcomplex) hcpow n =
(if ( *pNat* even) n then (x hcpow n) else -(x hcpow n))"
apply (rule eq_Abs_hcomplex [of x])
apply (rule eq_Abs_hypnat [of n])
apply (auto simp add: hcpow hyperpow starPNat hcomplex_minus, ultra)
-apply (auto simp add: complexpow_minus, ultra)
+apply (auto simp add: neg_power_if, ultra)
done

lemma hcpow_mult: "((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)"
@@ -1709,7 +1705,6 @@
val hcomplex_of_hypreal_hyperpow = thm"hcomplex_of_hypreal_hyperpow";
val hcmod_hcomplexpow = thm"hcmod_hcomplexpow";
val hcmod_hcpow = thm"hcmod_hcpow";
-val hcomplexpow_minus = thm"hcomplexpow_minus";
val hcpow_minus = thm"hcpow_minus";
val hcmod_hcomplex_inverse = thm"hcmod_hcomplex_inverse";
val hcmod_divide = thm"hcmod_divide";```
```--- a/src/HOL/Finite_Set.thy	Mon Mar 08 11:11:58 2004 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Mar 08 11:12:06 2004 +0100
@@ -1423,4 +1423,5 @@
"finite A ==> card {B. B <= A & card B = k} = (card A choose k)"

+
end```
```--- a/src/HOL/Hyperreal/HyperPow.thy	Mon Mar 08 11:11:58 2004 +0100
+++ b/src/HOL/Hyperreal/HyperPow.thy	Mon Mar 08 11:12:06 2004 +0100
@@ -37,8 +37,7 @@
hyprel``{%n::nat. (X n) ^ (Y n)})"

lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
-apply (simp (no_asm))
-done
+by simp

lemma hrealpow_two_le: "(0::hypreal) \<le> r ^ Suc (Suc 0)"
@@ -46,8 +45,7 @@

"(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)"
-done

```--- a/src/HOL/Integ/NatBin.thy	Mon Mar 08 11:11:58 2004 +0100
+++ b/src/HOL/Integ/NatBin.thy	Mon Mar 08 11:12:06 2004 +0100
@@ -296,6 +296,12 @@
done

+lemma power_even_eq: "(a::'a::ringpower) ^ (2*n) = (a^n)^2"
+by (simp add: power_mult power_mult_distrib power2_eq_square)
+
+lemma power_odd_eq: "(a::int) ^ Suc(2*n) = a * (a^n)^2"
+
lemma power_minus_even [simp]:
"(-a) ^ (2*n) = (a::'a::{ring,ringpower}) ^ (2*n)"
by (simp add: power_minus1_even power_minus [of a])
@@ -510,15 +516,8 @@
declare power_nat_number_of [of _ "number_of w", standard, simp]

-
text{*For the integers*}

-lemma zpower_even: "(z::int) ^ (2*a) = (z^a)^2"
-
-lemma zpower_odd: "(z::int) ^ (2*a + 1) = z * (z^a)^2"
-
lemma zpower_number_of_even:
"(z::int) ^ number_of (w BIT False) =
(let w = z ^ (number_of w) in  w*w)"
@@ -526,7 +525,7 @@
apply (rule_tac x = "number_of w" in spec, clarify)
apply (case_tac " (0::int) <= x")
-apply (auto simp add: nat_mult_distrib zpower_even power2_eq_square)
+apply (auto simp add: nat_mult_distrib power_even_eq power2_eq_square)
done

lemma zpower_number_of_odd:
@@ -537,7 +536,7 @@
apply (simp del: nat_number_of  add: nat_number_of_def number_of_BIT Let_def)
apply (simp only: number_of_add nat_numeral_1_eq_1 not_neg_eq_ge_0 neg_eq_less_0)
apply (rule_tac x = "number_of w" in spec, clarify)
done

declare zpower_number_of_even [of "number_of v", standard, simp]
@@ -604,6 +603,12 @@
lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"

+lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring,ringpower})"
+
+lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring,ringpower})"
+

subsection{*Literal arithmetic and @{term of_nat}*}

@@ -769,8 +774,6 @@
val of_nat_number_of_eq = thm"of_nat_number_of_eq";
val nat_power_eq = thm"nat_power_eq";
val power_nat_number_of = thm"power_nat_number_of";
-val zpower_even = thm"zpower_even";
-val zpower_odd = thm"zpower_odd";
val zpower_number_of_even = thm"zpower_number_of_even";
val zpower_number_of_odd = thm"zpower_number_of_odd";
val nat_number_of_Pls = thm"nat_number_of_Pls";
@@ -801,7 +804,6 @@
val nat_mult_eq_cancel_disj = thm"nat_mult_eq_cancel_disj";
val nat_mult_div_cancel_disj = thm"nat_mult_div_cancel_disj";

-val power_minus1_even = thm"power_minus1_even";
val power_minus_even = thm"power_minus_even";
val zero_le_even_power = thm"zero_le_even_power";
*}```
```--- a/src/HOL/Integ/Parity.thy	Mon Mar 08 11:11:58 2004 +0100
+++ b/src/HOL/Integ/Parity.thy	Mon Mar 08 11:12:06 2004 +0100
@@ -249,6 +249,11 @@
"odd x ==> (-1::'a::{number_ring,ringpower})^x = -1"
by (rule neg_one_even_odd_power [THEN conjunct2, THEN mp], assumption)

+lemma neg_power_if:
+     "(-x::'a::{ring,ringpower}) ^ n =
+      (if even n then (x ^ n) else -(x ^ n))"
+  by (induct n, simp_all split: split_if_asm add: power_Suc)
+

subsection {* Miscellaneous *}
```
```--- a/src/HOL/Main.thy	Mon Mar 08 11:11:58 2004 +0100
+++ b/src/HOL/Main.thy	Mon Mar 08 11:12:06 2004 +0100
@@ -6,7 +6,7 @@

-theory Main = Map + Hilbert_Choice + Extraction + Refute:
+theory Main = Map + Infinite_Set + Extraction + Refute:

text {*
Theory @{text Main} includes everything.  Note that theory @{text```
```--- a/src/HOL/Numeral.thy	Mon Mar 08 11:11:58 2004 +0100
+++ b/src/HOL/Numeral.thy	Mon Mar 08 11:12:06 2004 +0100
@@ -69,8 +69,6 @@

consts
-  ring_of :: "bin => 'a::ring"
-
NCons     :: "[bin,bool]=>bin"
bin_succ  :: "bin=>bin"
bin_pred  :: "bin=>bin"
@@ -85,12 +83,6 @@
NCons_BIT:  "NCons (w BIT x) b = (w BIT x) BIT b"

-primrec
-  ring_of_Pls: "ring_of bin.Pls = 0"
-  ring_of_Min: "ring_of bin.Min = - (1::'a::ring)"
-  ring_of_BIT: "ring_of(w BIT x) = (if x then 1 else 0) +
-	                               (ring_of w) + (ring_of w)"
-
primrec
bin_succ_Pls: "bin_succ bin.Pls = bin.Pls BIT True"
bin_succ_Min: "bin_succ bin.Min = bin.Pls"```
```--- a/src/HOL/Real/RealDef.thy	Mon Mar 08 11:11:58 2004 +0100
+++ b/src/HOL/Real/RealDef.thy	Mon Mar 08 11:12:06 2004 +0100
@@ -924,9 +924,6 @@
lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))"
by (unfold real_abs_def, simp)

-lemma abs_minus_one [simp]: "abs (-1) = (1::real)"
-by (unfold real_abs_def, simp)
-
lemma abs_interval_iff: "(abs x < r) = (-r < x & x < (r::real))"

@@ -983,7 +980,6 @@
val abs_triangle_ineq = thm"abs_triangle_ineq";
val abs_minus_cancel = thm"abs_minus_cancel";
-val abs_minus_one = thm"abs_minus_one";
val abs_interval_iff = thm"abs_interval_iff";
val abs_le_interval_iff = thm"abs_le_interval_iff";
```--- a/src/HOL/Real/RealPow.thy	Mon Mar 08 11:11:58 2004 +0100
+++ b/src/HOL/Real/RealPow.thy	Mon Mar 08 11:12:06 2004 +0100
@@ -42,9 +42,6 @@
apply (rule power_strict_mono, auto)
done

-lemma abs_realpow_minus_one [simp]: "abs((-1) ^ n) = (1::real)"
-
lemma realpow_two_le [simp]: "(0::real) \<le> r^ Suc (Suc 0)"

@@ -65,15 +62,6 @@
done

-lemma realpow_minus_one [simp]: "(-1) ^ (2*n) = (1::real)"
-by (induct_tac "n", auto)
-
-lemma realpow_minus_one_odd [simp]: "(-1) ^ Suc (2*n) = -(1::real)"
-by auto
-
-lemma realpow_minus_one_even [simp]: "(-1) ^ Suc (Suc (2*n)) = (1::real)"
-by auto
-
lemma realpow_Suc_le_self: "[| 0 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> r"
by (insert power_decreasing [of 1 "Suc n" r], simp)

@@ -264,15 +252,11 @@
val realpow_zero_zero = thm "realpow_zero_zero";
val realpow_two = thm "realpow_two";
val realpow_less = thm "realpow_less";
-val abs_realpow_minus_one = thm "abs_realpow_minus_one";
val realpow_two_le = thm "realpow_two_le";
val abs_realpow_two = thm "abs_realpow_two";
val realpow_two_abs = thm "realpow_two_abs";
val two_realpow_ge_one = thm "two_realpow_ge_one";
val two_realpow_gt = thm "two_realpow_gt";
-val realpow_minus_one = thm "realpow_minus_one";
-val realpow_minus_one_odd = thm "realpow_minus_one_odd";
-val realpow_minus_one_even = thm "realpow_minus_one_even";
val realpow_Suc_le_self = thm "realpow_Suc_le_self";
val realpow_Suc_less_one = thm "realpow_Suc_less_one";
val realpow_minus_mult = thm "realpow_minus_mult";```