--- 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 @@
apply (auto simp add: complex_mod_mult)
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 @@
apply (auto simp add: hcmod_mult)
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)"
by (simp add: n_sub_lemma)
+
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)"
by (auto simp add: zero_le_mult_iff)
@@ -46,8 +45,7 @@
lemma hrealpow_two_le_add_order:
"(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)"
-apply (simp only: hrealpow_two_le hypreal_le_add_order)
-done
+by (simp only: hrealpow_two_le hypreal_le_add_order)
declare hrealpow_two_le_add_order [simp]
lemma hrealpow_two_le_add_order2:
--- 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 @@
apply (auto simp add: power_Suc power_add)
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"
+by (simp add: power_even_eq)
+
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"
-by (simp add: zpower_zpower mult_commute)
-
-lemma zpower_odd: "(z::int) ^ (2*a + 1) = z * (z^a)^2"
-by (simp add: zpower_even zpower_zadd_distrib)
-
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 (simp only: number_of_add)
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)
-apply (auto simp add: nat_add_distrib nat_mult_distrib zpower_even power2_eq_square neg_nat)
+apply (auto simp add: nat_add_distrib nat_mult_distrib power_even_eq power2_eq_square neg_nat)
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)"
by (simp add: Let_def)
+lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring,ringpower})"
+by (simp add: power_mult);
+
+lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring,ringpower})"
+by (simp add: power_mult power_Suc);
+
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 @@
header {* Main HOL *}
-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))"
by (force simp add: Ring_and_Field.abs_less_iff)
@@ -983,7 +980,6 @@
val abs_triangle_ineq = thm"abs_triangle_ineq";
val abs_minus_cancel = thm"abs_minus_cancel";
val abs_minus_add_cancel = thm"abs_minus_add_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";
val abs_add_one_gt_zero = thm"abs_add_one_gt_zero";
--- 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)"
-by (simp add: power_abs)
-
lemma realpow_two_le [simp]: "(0::real) \<le> r^ Suc (Suc 0)"
by (simp add: real_le_square)
@@ -65,15 +62,6 @@
apply (auto simp add: two_realpow_ge_one)
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";