ringpower to recpower
authorpaulson
Thu Jun 24 17:52:55 2004 +0200 (2004-06-24)
changeset 1500444ac09ba7213
parent 15003 6145dd7538d7
child 15005 546c8e7e28d4
ringpower to recpower
src/HOL/Finite_Set.thy
src/HOL/Power.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Thu Jun 24 17:52:02 2004 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Thu Jun 24 17:52:55 2004 +0200
     1.3 @@ -1138,20 +1138,19 @@
     1.4      "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
     1.5    by (induct set: Finites) auto
     1.6  
     1.7 -lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::ringpower)) =
     1.8 -    y^(card A)"
     1.9 +lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::recpower)) = y^(card A)"
    1.10    apply (erule finite_induct)
    1.11    apply (auto simp add: power_Suc)
    1.12    done
    1.13  
    1.14 -lemma setprod_zero: "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==>
    1.15 -    setprod f A = 0"
    1.16 +lemma setprod_zero:
    1.17 +     "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0"
    1.18    apply (induct set: Finites, force, clarsimp)
    1.19    apply (erule disjE, auto)
    1.20    done
    1.21  
    1.22 -lemma setprod_nonneg [rule_format]: "(ALL x: A. (0::'a::ordered_idom) \<le> f x)
    1.23 -     --> 0 \<le> setprod f A"
    1.24 +lemma setprod_nonneg [rule_format]:
    1.25 +     "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A"
    1.26    apply (case_tac "finite A")
    1.27    apply (induct set: Finites, force, clarsimp)
    1.28    apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
     2.1 --- a/src/HOL/Power.thy	Thu Jun 24 17:52:02 2004 +0200
     2.2 +++ b/src/HOL/Power.thy	Thu Jun 24 17:52:55 2004 +0200
     2.3 @@ -11,55 +11,55 @@
     2.4  
     2.5  subsection{*Powers for Arbitrary (Semi)Rings*}
     2.6  
     2.7 -axclass ringpower \<subseteq> comm_semiring_1_cancel, power
     2.8 -  power_0 [simp]:   "a ^ 0       = 1"
     2.9 -  power_Suc: "a ^ (Suc n) = a * (a ^ n)"
    2.10 +axclass recpower \<subseteq> comm_semiring_1_cancel, power
    2.11 +  power_0 [simp]: "a ^ 0       = 1"
    2.12 +  power_Suc:      "a ^ (Suc n) = a * (a ^ n)"
    2.13  
    2.14 -lemma power_0_Suc [simp]: "(0::'a::ringpower) ^ (Suc n) = 0"
    2.15 +lemma power_0_Suc [simp]: "(0::'a::recpower) ^ (Suc n) = 0"
    2.16  by (simp add: power_Suc)
    2.17  
    2.18  text{*It looks plausible as a simprule, but its effect can be strange.*}
    2.19 -lemma power_0_left: "0^n = (if n=0 then 1 else (0::'a::ringpower))"
    2.20 +lemma power_0_left: "0^n = (if n=0 then 1 else (0::'a::recpower))"
    2.21  by (induct_tac "n", auto)
    2.22  
    2.23 -lemma power_one [simp]: "1^n = (1::'a::ringpower)"
    2.24 +lemma power_one [simp]: "1^n = (1::'a::recpower)"
    2.25  apply (induct_tac "n")
    2.26  apply (auto simp add: power_Suc)
    2.27  done
    2.28  
    2.29 -lemma power_one_right [simp]: "(a::'a::ringpower) ^ 1 = a"
    2.30 +lemma power_one_right [simp]: "(a::'a::recpower) ^ 1 = a"
    2.31  by (simp add: power_Suc)
    2.32  
    2.33 -lemma power_add: "(a::'a::ringpower) ^ (m+n) = (a^m) * (a^n)"
    2.34 +lemma power_add: "(a::'a::recpower) ^ (m+n) = (a^m) * (a^n)"
    2.35  apply (induct_tac "n")
    2.36  apply (simp_all add: power_Suc mult_ac)
    2.37  done
    2.38  
    2.39 -lemma power_mult: "(a::'a::ringpower) ^ (m*n) = (a^m) ^ n"
    2.40 +lemma power_mult: "(a::'a::recpower) ^ (m*n) = (a^m) ^ n"
    2.41  apply (induct_tac "n")
    2.42  apply (simp_all add: power_Suc power_add)
    2.43  done
    2.44  
    2.45 -lemma power_mult_distrib: "((a::'a::ringpower) * b) ^ n = (a^n) * (b^n)"
    2.46 +lemma power_mult_distrib: "((a::'a::recpower) * b) ^ n = (a^n) * (b^n)"
    2.47  apply (induct_tac "n")
    2.48  apply (auto simp add: power_Suc mult_ac)
    2.49  done
    2.50  
    2.51  lemma zero_less_power:
    2.52 -     "0 < (a::'a::{ordered_semidom,ringpower}) ==> 0 < a^n"
    2.53 +     "0 < (a::'a::{ordered_semidom,recpower}) ==> 0 < a^n"
    2.54  apply (induct_tac "n")
    2.55  apply (simp_all add: power_Suc zero_less_one mult_pos)
    2.56  done
    2.57  
    2.58  lemma zero_le_power:
    2.59 -     "0 \<le> (a::'a::{ordered_semidom,ringpower}) ==> 0 \<le> a^n"
    2.60 +     "0 \<le> (a::'a::{ordered_semidom,recpower}) ==> 0 \<le> a^n"
    2.61  apply (simp add: order_le_less)
    2.62  apply (erule disjE)
    2.63  apply (simp_all add: zero_less_power zero_less_one power_0_left)
    2.64  done
    2.65  
    2.66  lemma one_le_power:
    2.67 -     "1 \<le> (a::'a::{ordered_semidom,ringpower}) ==> 1 \<le> a^n"
    2.68 +     "1 \<le> (a::'a::{ordered_semidom,recpower}) ==> 1 \<le> a^n"
    2.69  apply (induct_tac "n")
    2.70  apply (simp_all add: power_Suc)
    2.71  apply (rule order_trans [OF _ mult_mono [of 1 _ 1]])
    2.72 @@ -70,7 +70,7 @@
    2.73    by (simp add: order_trans [OF zero_le_one order_less_imp_le])
    2.74  
    2.75  lemma power_gt1_lemma:
    2.76 -  assumes gt1: "1 < (a::'a::{ordered_semidom,ringpower})"
    2.77 +  assumes gt1: "1 < (a::'a::{ordered_semidom,recpower})"
    2.78    shows "1 < a * a^n"
    2.79  proof -
    2.80    have "1*1 < a*1" using gt1 by simp
    2.81 @@ -81,11 +81,11 @@
    2.82  qed
    2.83  
    2.84  lemma power_gt1:
    2.85 -     "1 < (a::'a::{ordered_semidom,ringpower}) ==> 1 < a ^ (Suc n)"
    2.86 +     "1 < (a::'a::{ordered_semidom,recpower}) ==> 1 < a ^ (Suc n)"
    2.87  by (simp add: power_gt1_lemma power_Suc)
    2.88  
    2.89  lemma power_le_imp_le_exp:
    2.90 -  assumes gt1: "(1::'a::{ringpower,ordered_semidom}) < a"
    2.91 +  assumes gt1: "(1::'a::{recpower,ordered_semidom}) < a"
    2.92    shows "!!n. a^m \<le> a^n ==> m \<le> n"
    2.93  proof (induct m)
    2.94    case 0
    2.95 @@ -109,26 +109,26 @@
    2.96  
    2.97  text{*Surely we can strengthen this? It holds for @{text "0<a<1"} too.*}
    2.98  lemma power_inject_exp [simp]:
    2.99 -     "1 < (a::'a::{ordered_semidom,ringpower}) ==> (a^m = a^n) = (m=n)"
   2.100 +     "1 < (a::'a::{ordered_semidom,recpower}) ==> (a^m = a^n) = (m=n)"
   2.101    by (force simp add: order_antisym power_le_imp_le_exp)
   2.102  
   2.103  text{*Can relax the first premise to @{term "0<a"} in the case of the
   2.104  natural numbers.*}
   2.105  lemma power_less_imp_less_exp:
   2.106 -     "[| (1::'a::{ringpower,ordered_semidom}) < a; a^m < a^n |] ==> m < n"
   2.107 +     "[| (1::'a::{recpower,ordered_semidom}) < a; a^m < a^n |] ==> m < n"
   2.108  by (simp add: order_less_le [of m n] order_less_le [of "a^m" "a^n"]
   2.109                power_le_imp_le_exp)
   2.110  
   2.111  
   2.112  lemma power_mono:
   2.113 -     "[|a \<le> b; (0::'a::{ringpower,ordered_semidom}) \<le> a|] ==> a^n \<le> b^n"
   2.114 +     "[|a \<le> b; (0::'a::{recpower,ordered_semidom}) \<le> a|] ==> a^n \<le> b^n"
   2.115  apply (induct_tac "n")
   2.116  apply (simp_all add: power_Suc)
   2.117  apply (auto intro: mult_mono zero_le_power order_trans [of 0 a b])
   2.118  done
   2.119  
   2.120  lemma power_strict_mono [rule_format]:
   2.121 -     "[|a < b; (0::'a::{ringpower,ordered_semidom}) \<le> a|]
   2.122 +     "[|a < b; (0::'a::{recpower,ordered_semidom}) \<le> a|]
   2.123        ==> 0 < n --> a^n < b^n"
   2.124  apply (induct_tac "n")
   2.125  apply (auto simp add: mult_strict_mono zero_le_power power_Suc
   2.126 @@ -136,51 +136,51 @@
   2.127  done
   2.128  
   2.129  lemma power_eq_0_iff [simp]:
   2.130 -     "(a^n = 0) = (a = (0::'a::{ordered_idom,ringpower}) & 0<n)"
   2.131 +     "(a^n = 0) = (a = (0::'a::{ordered_idom,recpower}) & 0<n)"
   2.132  apply (induct_tac "n")
   2.133  apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
   2.134  done
   2.135  
   2.136  lemma field_power_eq_0_iff [simp]:
   2.137 -     "(a^n = 0) = (a = (0::'a::{field,ringpower}) & 0<n)"
   2.138 +     "(a^n = 0) = (a = (0::'a::{field,recpower}) & 0<n)"
   2.139  apply (induct_tac "n")
   2.140  apply (auto simp add: power_Suc field_mult_eq_0_iff zero_neq_one[THEN not_sym])
   2.141  done
   2.142  
   2.143 -lemma field_power_not_zero: "a \<noteq> (0::'a::{field,ringpower}) ==> a^n \<noteq> 0"
   2.144 +lemma field_power_not_zero: "a \<noteq> (0::'a::{field,recpower}) ==> a^n \<noteq> 0"
   2.145  by force
   2.146  
   2.147  lemma nonzero_power_inverse:
   2.148 -  "a \<noteq> 0 ==> inverse ((a::'a::{field,ringpower}) ^ n) = (inverse a) ^ n"
   2.149 +  "a \<noteq> 0 ==> inverse ((a::'a::{field,recpower}) ^ n) = (inverse a) ^ n"
   2.150  apply (induct_tac "n")
   2.151  apply (auto simp add: power_Suc nonzero_inverse_mult_distrib mult_commute)
   2.152  done
   2.153  
   2.154  text{*Perhaps these should be simprules.*}
   2.155  lemma power_inverse:
   2.156 -  "inverse ((a::'a::{field,division_by_zero,ringpower}) ^ n) = (inverse a) ^ n"
   2.157 +  "inverse ((a::'a::{field,division_by_zero,recpower}) ^ n) = (inverse a) ^ n"
   2.158  apply (induct_tac "n")
   2.159  apply (auto simp add: power_Suc inverse_mult_distrib)
   2.160  done
   2.161  
   2.162  lemma nonzero_power_divide:
   2.163 -    "b \<noteq> 0 ==> (a/b) ^ n = ((a::'a::{field,ringpower}) ^ n) / (b ^ n)"
   2.164 +    "b \<noteq> 0 ==> (a/b) ^ n = ((a::'a::{field,recpower}) ^ n) / (b ^ n)"
   2.165  by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
   2.166  
   2.167  lemma power_divide:
   2.168 -    "(a/b) ^ n = ((a::'a::{field,division_by_zero,ringpower}) ^ n / b ^ n)"
   2.169 +    "(a/b) ^ n = ((a::'a::{field,division_by_zero,recpower}) ^ n / b ^ n)"
   2.170  apply (case_tac "b=0", simp add: power_0_left)
   2.171  apply (rule nonzero_power_divide)
   2.172  apply assumption
   2.173  done
   2.174  
   2.175 -lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_idom,ringpower}) ^ n"
   2.176 +lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_idom,recpower}) ^ n"
   2.177  apply (induct_tac "n")
   2.178  apply (auto simp add: power_Suc abs_mult)
   2.179  done
   2.180  
   2.181  lemma zero_less_power_abs_iff [simp]:
   2.182 -     "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_idom,ringpower}) | n=0)"
   2.183 +     "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_idom,recpower}) | n=0)"
   2.184  proof (induct "n")
   2.185    case 0
   2.186      show ?case by (simp add: zero_less_one)
   2.187 @@ -190,12 +190,12 @@
   2.188  qed
   2.189  
   2.190  lemma zero_le_power_abs [simp]:
   2.191 -     "(0::'a::{ordered_idom,ringpower}) \<le> (abs a)^n"
   2.192 +     "(0::'a::{ordered_idom,recpower}) \<le> (abs a)^n"
   2.193  apply (induct_tac "n")
   2.194  apply (auto simp add: zero_le_one zero_le_power)
   2.195  done
   2.196  
   2.197 -lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{comm_ring_1,ringpower}) ^ n"
   2.198 +lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{comm_ring_1,recpower}) ^ n"
   2.199  proof -
   2.200    have "-a = (- 1) * a"  by (simp add: minus_mult_left [symmetric])
   2.201    thus ?thesis by (simp only: power_mult_distrib)
   2.202 @@ -203,14 +203,14 @@
   2.203  
   2.204  text{*Lemma for @{text power_strict_decreasing}*}
   2.205  lemma power_Suc_less:
   2.206 -     "[|(0::'a::{ordered_semidom,ringpower}) < a; a < 1|]
   2.207 +     "[|(0::'a::{ordered_semidom,recpower}) < a; a < 1|]
   2.208        ==> a * a^n < a^n"
   2.209  apply (induct_tac n)
   2.210  apply (auto simp add: power_Suc mult_strict_left_mono)
   2.211  done
   2.212  
   2.213  lemma power_strict_decreasing:
   2.214 -     "[|n < N; 0 < a; a < (1::'a::{ordered_semidom,ringpower})|]
   2.215 +     "[|n < N; 0 < a; a < (1::'a::{ordered_semidom,recpower})|]
   2.216        ==> a^N < a^n"
   2.217  apply (erule rev_mp)
   2.218  apply (induct_tac "N")
   2.219 @@ -223,7 +223,7 @@
   2.220  
   2.221  text{*Proof resembles that of @{text power_strict_decreasing}*}
   2.222  lemma power_decreasing:
   2.223 -     "[|n \<le> N; 0 \<le> a; a \<le> (1::'a::{ordered_semidom,ringpower})|]
   2.224 +     "[|n \<le> N; 0 \<le> a; a \<le> (1::'a::{ordered_semidom,recpower})|]
   2.225        ==> a^N \<le> a^n"
   2.226  apply (erule rev_mp)
   2.227  apply (induct_tac "N")
   2.228 @@ -235,13 +235,13 @@
   2.229  done
   2.230  
   2.231  lemma power_Suc_less_one:
   2.232 -     "[| 0 < a; a < (1::'a::{ordered_semidom,ringpower}) |] ==> a ^ Suc n < 1"
   2.233 +     "[| 0 < a; a < (1::'a::{ordered_semidom,recpower}) |] ==> a ^ Suc n < 1"
   2.234  apply (insert power_strict_decreasing [of 0 "Suc n" a], simp)
   2.235  done
   2.236  
   2.237  text{*Proof again resembles that of @{text power_strict_decreasing}*}
   2.238  lemma power_increasing:
   2.239 -     "[|n \<le> N; (1::'a::{ordered_semidom,ringpower}) \<le> a|] ==> a^n \<le> a^N"
   2.240 +     "[|n \<le> N; (1::'a::{ordered_semidom,recpower}) \<le> a|] ==> a^n \<le> a^N"
   2.241  apply (erule rev_mp)
   2.242  apply (induct_tac "N")
   2.243  apply (auto simp add: power_Suc le_Suc_eq)
   2.244 @@ -253,13 +253,13 @@
   2.245  
   2.246  text{*Lemma for @{text power_strict_increasing}*}
   2.247  lemma power_less_power_Suc:
   2.248 -     "(1::'a::{ordered_semidom,ringpower}) < a ==> a^n < a * a^n"
   2.249 +     "(1::'a::{ordered_semidom,recpower}) < a ==> a^n < a * a^n"
   2.250  apply (induct_tac n)
   2.251  apply (auto simp add: power_Suc mult_strict_left_mono order_less_trans [OF zero_less_one])
   2.252  done
   2.253  
   2.254  lemma power_strict_increasing:
   2.255 -     "[|n < N; (1::'a::{ordered_semidom,ringpower}) < a|] ==> a^n < a^N"
   2.256 +     "[|n < N; (1::'a::{ordered_semidom,recpower}) < a|] ==> a^n < a^N"
   2.257  apply (erule rev_mp)
   2.258  apply (induct_tac "N")
   2.259  apply (auto simp add: power_less_power_Suc power_Suc less_Suc_eq)
   2.260 @@ -272,7 +272,7 @@
   2.261  
   2.262  lemma power_le_imp_le_base:
   2.263    assumes le: "a ^ Suc n \<le> b ^ Suc n"
   2.264 -      and xnonneg: "(0::'a::{ordered_semidom,ringpower}) \<le> a"
   2.265 +      and xnonneg: "(0::'a::{ordered_semidom,recpower}) \<le> a"
   2.266        and ynonneg: "0 \<le> b"
   2.267    shows "a \<le> b"
   2.268   proof (rule ccontr)
   2.269 @@ -286,7 +286,7 @@
   2.270  
   2.271  lemma power_inject_base:
   2.272       "[| a ^ Suc n = b ^ Suc n; 0 \<le> a; 0 \<le> b |]
   2.273 -      ==> a = (b::'a::{ordered_semidom,ringpower})"
   2.274 +      ==> a = (b::'a::{ordered_semidom,recpower})"
   2.275  by (blast intro: power_le_imp_le_base order_antisym order_eq_refl sym)
   2.276  
   2.277  
   2.278 @@ -296,7 +296,7 @@
   2.279    "p ^ 0 = 1"
   2.280    "p ^ (Suc n) = (p::nat) * (p ^ n)"
   2.281  
   2.282 -instance nat :: ringpower
   2.283 +instance nat :: recpower
   2.284  proof
   2.285    fix z n :: nat
   2.286    show "z^0 = 1" by simp