--- a/src/HOL/Power.thy Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/Power.thy Fri Apr 16 04:07:10 2004 +0200
@@ -24,7 +24,7 @@
lemma power_one [simp]: "1^n = (1::'a::ringpower)"
apply (induct_tac "n")
-apply (auto simp add: power_Suc)
+apply (auto simp add: power_Suc)
done
lemma power_one_right [simp]: "(a::'a::ringpower) ^ 1 = a"
@@ -41,7 +41,7 @@
done
lemma power_mult_distrib: "((a::'a::ringpower) * b) ^ n = (a^n) * (b^n)"
-apply (induct_tac "n")
+apply (induct_tac "n")
apply (auto simp add: power_Suc mult_ac)
done
@@ -54,7 +54,7 @@
lemma zero_le_power:
"0 \<le> (a::'a::{ordered_semiring,ringpower}) ==> 0 \<le> a^n"
apply (simp add: order_le_less)
-apply (erule disjE)
+apply (erule disjE)
apply (simp_all add: zero_less_power zero_less_one power_0_left)
done
@@ -62,25 +62,22 @@
"1 \<le> (a::'a::{ordered_semiring,ringpower}) ==> 1 \<le> a^n"
apply (induct_tac "n")
apply (simp_all add: power_Suc)
-apply (rule order_trans [OF _ mult_mono [of 1 _ 1]])
-apply (simp_all add: zero_le_one order_trans [OF zero_le_one])
+apply (rule order_trans [OF _ mult_mono [of 1 _ 1]])
+apply (simp_all add: zero_le_one order_trans [OF zero_le_one])
done
lemma gt1_imp_ge0: "1 < a ==> 0 \<le> (a::'a::ordered_semiring)"
by (simp add: order_trans [OF zero_le_one order_less_imp_le])
lemma power_gt1_lemma:
- assumes gt1: "1 < (a::'a::{ordered_semiring,ringpower})"
- shows "1 < a * a^n"
+ assumes gt1: "1 < (a::'a::{ordered_semiring,ringpower})"
+ shows "1 < a * a^n"
proof -
- have "1*1 < a * a^n"
- proof (rule order_less_le_trans)
- show "1*1 < a*1" by (simp add: gt1)
- show "a*1 \<le> a * a^n"
- by (simp only: mult_mono gt1 gt1_imp_ge0 one_le_power order_less_imp_le
- zero_le_one order_refl)
- qed
- thus ?thesis by simp
+ have "1*1 < a*1" using gt1 by simp
+ also have "\<dots> \<le> a * a^n" using gt1
+ by (simp only: mult_mono gt1_imp_ge0 one_le_power order_less_imp_le
+ zero_le_one order_refl)
+ finally show ?thesis by simp
qed
lemma power_gt1:
@@ -88,52 +85,52 @@
by (simp add: power_gt1_lemma power_Suc)
lemma power_le_imp_le_exp:
- assumes gt1: "(1::'a::{ringpower,ordered_semiring}) < a"
- shows "!!n. a^m \<le> a^n ==> m \<le> n"
-proof (induct "m")
+ assumes gt1: "(1::'a::{ringpower,ordered_semiring}) < a"
+ shows "!!n. a^m \<le> a^n ==> m \<le> n"
+proof (induct m)
case 0
- show ?case by simp
+ show ?case by simp
next
case (Suc m)
- show ?case
- proof (cases n)
- case 0
- from prems have "a * a^m \<le> 1" by (simp add: power_Suc)
- with gt1 show ?thesis
- by (force simp only: power_gt1_lemma
- linorder_not_less [symmetric])
- next
- case (Suc n)
- from prems show ?thesis
- by (force dest: mult_left_le_imp_le
- simp add: power_Suc order_less_trans [OF zero_less_one gt1])
- qed
+ show ?case
+ proof (cases n)
+ case 0
+ from prems have "a * a^m \<le> 1" by (simp add: power_Suc)
+ with gt1 show ?thesis
+ by (force simp only: power_gt1_lemma
+ linorder_not_less [symmetric])
+ next
+ case (Suc n)
+ from prems show ?thesis
+ by (force dest: mult_left_le_imp_le
+ simp add: power_Suc order_less_trans [OF zero_less_one gt1])
+ qed
qed
-text{*Surely we can strengthen this? It holds for 0<a<1 too.*}
+text{*Surely we can strengthen this? It holds for @{text "0<a<1"} too.*}
lemma power_inject_exp [simp]:
"1 < (a::'a::{ordered_semiring,ringpower}) ==> (a^m = a^n) = (m=n)"
- by (force simp add: order_antisym power_le_imp_le_exp)
+ by (force simp add: order_antisym power_le_imp_le_exp)
text{*Can relax the first premise to @{term "0<a"} in the case of the
natural numbers.*}
lemma power_less_imp_less_exp:
"[| (1::'a::{ringpower,ordered_semiring}) < a; a^m < a^n |] ==> m < n"
-by (simp add: order_less_le [of m n] order_less_le [of "a^m" "a^n"]
- power_le_imp_le_exp)
+by (simp add: order_less_le [of m n] order_less_le [of "a^m" "a^n"]
+ power_le_imp_le_exp)
lemma power_mono:
"[|a \<le> b; (0::'a::{ringpower,ordered_semiring}) \<le> a|] ==> a^n \<le> b^n"
-apply (induct_tac "n")
+apply (induct_tac "n")
apply (simp_all add: power_Suc)
apply (auto intro: mult_mono zero_le_power order_trans [of 0 a b])
done
lemma power_strict_mono [rule_format]:
- "[|a < b; (0::'a::{ringpower,ordered_semiring}) \<le> a|]
- ==> 0 < n --> a^n < b^n"
-apply (induct_tac "n")
+ "[|a < b; (0::'a::{ringpower,ordered_semiring}) \<le> a|]
+ ==> 0 < n --> a^n < b^n"
+apply (induct_tac "n")
apply (auto simp add: mult_strict_mono zero_le_power power_Suc
order_le_less_trans [of 0 a b])
done
@@ -166,15 +163,15 @@
apply (auto simp add: power_Suc inverse_mult_distrib)
done
-lemma nonzero_power_divide:
+lemma nonzero_power_divide:
"b \<noteq> 0 ==> (a/b) ^ n = ((a::'a::{field,ringpower}) ^ n) / (b ^ n)"
by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
-lemma power_divide:
+lemma power_divide:
"(a/b) ^ n = ((a::'a::{field,division_by_zero,ringpower}) ^ n / b ^ n)"
apply (case_tac "b=0", simp add: power_0_left)
-apply (rule nonzero_power_divide)
-apply assumption
+apply (rule nonzero_power_divide)
+apply assumption
done
lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_ring,ringpower}) ^ n"
@@ -183,7 +180,7 @@
done
lemma zero_less_power_abs_iff [simp]:
- "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_ring,ringpower}) | n=0)"
+ "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_ring,ringpower}) | n=0)"
proof (induct "n")
case 0
show ?case by (simp add: zero_less_one)
@@ -208,19 +205,19 @@
lemma power_Suc_less:
"[|(0::'a::{ordered_semiring,ringpower}) < a; a < 1|]
==> a * a^n < a^n"
-apply (induct_tac n)
-apply (auto simp add: power_Suc mult_strict_left_mono)
+apply (induct_tac n)
+apply (auto simp add: power_Suc mult_strict_left_mono)
done
lemma power_strict_decreasing:
"[|n < N; 0 < a; a < (1::'a::{ordered_semiring,ringpower})|]
==> a^N < a^n"
-apply (erule rev_mp)
-apply (induct_tac "N")
-apply (auto simp add: power_Suc power_Suc_less less_Suc_eq)
-apply (rename_tac m)
+apply (erule rev_mp)
+apply (induct_tac "N")
+apply (auto simp add: power_Suc power_Suc_less less_Suc_eq)
+apply (rename_tac m)
apply (subgoal_tac "a * a^m < 1 * a^n", simp)
-apply (rule mult_strict_mono)
+apply (rule mult_strict_mono)
apply (auto simp add: zero_le_power zero_less_one order_less_imp_le)
done
@@ -228,47 +225,47 @@
lemma power_decreasing:
"[|n \<le> N; 0 \<le> a; a \<le> (1::'a::{ordered_semiring,ringpower})|]
==> a^N \<le> a^n"
-apply (erule rev_mp)
-apply (induct_tac "N")
-apply (auto simp add: power_Suc le_Suc_eq)
-apply (rename_tac m)
+apply (erule rev_mp)
+apply (induct_tac "N")
+apply (auto simp add: power_Suc le_Suc_eq)
+apply (rename_tac m)
apply (subgoal_tac "a * a^m \<le> 1 * a^n", simp)
-apply (rule mult_mono)
+apply (rule mult_mono)
apply (auto simp add: zero_le_power zero_le_one)
done
lemma power_Suc_less_one:
"[| 0 < a; a < (1::'a::{ordered_semiring,ringpower}) |] ==> a ^ Suc n < 1"
-apply (insert power_strict_decreasing [of 0 "Suc n" a], simp)
+apply (insert power_strict_decreasing [of 0 "Suc n" a], simp)
done
text{*Proof again resembles that of @{text power_strict_decreasing}*}
lemma power_increasing:
"[|n \<le> N; (1::'a::{ordered_semiring,ringpower}) \<le> a|] ==> a^n \<le> a^N"
-apply (erule rev_mp)
-apply (induct_tac "N")
-apply (auto simp add: power_Suc le_Suc_eq)
+apply (erule rev_mp)
+apply (induct_tac "N")
+apply (auto simp add: power_Suc le_Suc_eq)
apply (rename_tac m)
apply (subgoal_tac "1 * a^n \<le> a * a^m", simp)
-apply (rule mult_mono)
+apply (rule mult_mono)
apply (auto simp add: order_trans [OF zero_le_one] zero_le_power)
done
text{*Lemma for @{text power_strict_increasing}*}
lemma power_less_power_Suc:
"(1::'a::{ordered_semiring,ringpower}) < a ==> a^n < a * a^n"
-apply (induct_tac n)
-apply (auto simp add: power_Suc mult_strict_left_mono order_less_trans [OF zero_less_one])
+apply (induct_tac n)
+apply (auto simp add: power_Suc mult_strict_left_mono order_less_trans [OF zero_less_one])
done
lemma power_strict_increasing:
"[|n < N; (1::'a::{ordered_semiring,ringpower}) < a|] ==> a^n < a^N"
-apply (erule rev_mp)
-apply (induct_tac "N")
-apply (auto simp add: power_less_power_Suc power_Suc less_Suc_eq)
+apply (erule rev_mp)
+apply (induct_tac "N")
+apply (auto simp add: power_less_power_Suc power_Suc less_Suc_eq)
apply (rename_tac m)
apply (subgoal_tac "1 * a^n < a * a^m", simp)
-apply (rule mult_strict_mono)
+apply (rule mult_strict_mono)
apply (auto simp add: order_less_trans [OF zero_less_one] zero_le_power
order_less_imp_le)
done
@@ -282,13 +279,13 @@
assume "~ a \<le> b"
then have "b < a" by (simp only: linorder_not_le)
then have "b ^ Suc n < a ^ Suc n"
- by (simp only: prems power_strict_mono)
+ by (simp only: prems power_strict_mono)
from le and this show "False"
by (simp add: linorder_not_less [symmetric])
qed
-
+
lemma power_inject_base:
- "[| a ^ Suc n = b ^ Suc n; 0 \<le> a; 0 \<le> b |]
+ "[| a ^ Suc n = b ^ Suc n; 0 \<le> a; 0 \<le> b |]
==> a = (b::'a::{ordered_semiring,ringpower})"
by (blast intro: power_le_imp_le_base order_antisym order_eq_refl sym)
@@ -298,7 +295,7 @@
primrec (power)
"p ^ 0 = 1"
"p ^ (Suc n) = (p::nat) * (p ^ n)"
-
+
instance nat :: ringpower
proof
fix z n :: nat
@@ -321,7 +318,7 @@
lemma nat_power_less_imp_less: "!!i::nat. [| 0 < i; i^m < i^n |] ==> m < n"
apply (rule ccontr)
apply (drule leI [THEN le_imp_power_dvd, THEN dvd_imp_le, THEN leD])
-apply (erule zero_less_power, auto)
+apply (erule zero_less_power, auto)
done
lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"
@@ -341,7 +338,7 @@
subsection{*Binomial Coefficients*}
-text{*This development is based on the work of Andy Gordon and
+text{*This development is based on the work of Andy Gordon and
Florian Kammueller*}
consts
@@ -400,7 +397,7 @@
apply (induct_tac "n")
apply (simp add: binomial_0, clarify)
apply (case_tac "k")
-apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq
+apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq
binomial_eq_0)
done
@@ -408,7 +405,7 @@
need to reason about division.*}
lemma binomial_Suc_Suc_eq_times:
"k \<le> n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"
-by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc
+by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc
del: mult_Suc mult_Suc_right)
text{*Another version, with -1 instead of Suc.*}
@@ -460,7 +457,7 @@
val power_le_imp_le_base = thm"power_le_imp_le_base";
val power_inject_base = thm"power_inject_base";
*}
-
+
text{*ML bindings for the remaining theorems*}
ML
{*