# HG changeset patch # User paulson # Date 1078740726 -3600 # Node ID 75910c7557c5c3dfbdac66d7caf2ef9cd196af62 # Parent 04135b0c06ffe4b89920bbd749c20ac1f72a6a2f generic theorems about exponentials; general tidying up diff -r 04135b0c06ff -r 75910c7557c5 src/HOL/Complex/Complex.thy --- 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"; diff -r 04135b0c06ff -r 75910c7557c5 src/HOL/Complex/NSComplex.thy --- 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"; diff -r 04135b0c06ff -r 75910c7557c5 src/HOL/Finite_Set.thy --- 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 diff -r 04135b0c06ff -r 75910c7557c5 src/HOL/Hyperreal/HyperPow.thy --- 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) \ r ^ Suc (Suc 0)" by (auto simp add: zero_le_mult_iff) @@ -46,8 +45,7 @@ lemma hrealpow_two_le_add_order: "(0::hypreal) \ 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: diff -r 04135b0c06ff -r 75910c7557c5 src/HOL/Integ/NatBin.thy --- 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"; *} diff -r 04135b0c06ff -r 75910c7557c5 src/HOL/Integ/Parity.thy --- 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 *} diff -r 04135b0c06ff -r 75910c7557c5 src/HOL/Main.thy --- 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 diff -r 04135b0c06ff -r 75910c7557c5 src/HOL/Numeral.thy --- 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" diff -r 04135b0c06ff -r 75910c7557c5 src/HOL/Real/RealDef.thy --- 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"; diff -r 04135b0c06ff -r 75910c7557c5 src/HOL/Real/RealPow.thy --- 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) \ 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 \ r; r \ (1::real) |] ==> r ^ Suc n \ 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";