generic theorems about exponentials; general tidying up
authorpaulson
Mon Mar 08 11:12:06 2004 +0100 (2004-03-08)
changeset 1444375910c7557c5
parent 14442 04135b0c06ff
child 14444 24724afce166
generic theorems about exponentials; general tidying up
src/HOL/Complex/Complex.thy
src/HOL/Complex/NSComplex.thy
src/HOL/Finite_Set.thy
src/HOL/Hyperreal/HyperPow.thy
src/HOL/Integ/NatBin.thy
src/HOL/Integ/Parity.thy
src/HOL/Main.thy
src/HOL/Numeral.thy
src/HOL/Real/RealDef.thy
src/HOL/Real/RealPow.thy
     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.5    by (simp add: n_sub_lemma)
     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.15  lemma hrealpow_two_le_add_order:
    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.20  declare hrealpow_two_le_add_order [simp]
    4.21  
    4.22  lemma hrealpow_two_le_add_order2:
     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.4  apply (auto simp add: power_Suc power_add)
     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.11 +by (simp add: power_even_eq) 
    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.27 -by (simp add: zpower_even zpower_zadd_distrib)
    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.33  apply (simp only: number_of_add) 
    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.45 -apply (auto simp add: nat_add_distrib nat_mult_distrib zpower_even power2_eq_square neg_nat)
    5.46 +apply (auto simp add: nat_add_distrib nat_mult_distrib power_even_eq power2_eq_square neg_nat)
    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.52    by (simp add: Let_def)
    5.53  
    5.54 +lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring,ringpower})"
    5.55 +by (simp add: power_mult); 
    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.16  val abs_minus_add_cancel = thm"abs_minus_add_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";
    9.20  val abs_add_one_gt_zero = thm"abs_add_one_gt_zero";
    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.8 -by (simp add: power_abs)
    10.9 -
   10.10  lemma realpow_two_le [simp]: "(0::real) \<le> r^ Suc (Suc 0)"
   10.11  by (simp add: real_le_square)
   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";