--- a/src/HOL/Fact.thy Tue Dec 20 17:40:21 2011 +0100
+++ b/src/HOL/Fact.thy Tue Dec 20 18:46:05 2011 +0100
@@ -285,6 +285,12 @@
(if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
by (cases m) auto
+lemma fact_le_power: "fact n \<le> n^n"
+proof (induct n)
+ case (Suc n)
+ then have "fact n \<le> Suc n ^ n" by (rule le_trans) (simp add: power_mono)
+ then show ?case by (simp add: add_le_mono)
+qed simp
subsection {* @{term fact} and @{term of_nat} *}
--- a/src/HOL/Library/Extended_Nat.thy Tue Dec 20 17:40:21 2011 +0100
+++ b/src/HOL/Library/Extended_Nat.thy Tue Dec 20 18:46:05 2011 +0100
@@ -49,6 +49,9 @@
declare [[coercion "enat::nat\<Rightarrow>enat"]]
+lemmas enat2_cases = enat.exhaust[case_product enat.exhaust]
+lemmas enat3_cases = enat.exhaust[case_product enat.exhaust enat.exhaust]
+
lemma not_infinity_eq [iff]: "(x \<noteq> \<infinity>) = (EX i. x = enat i)"
by (cases x) auto
@@ -165,9 +168,9 @@
instance proof
fix n m q :: enat
show "n + m + q = n + (m + q)"
- by (cases n, auto, cases m, auto, cases q, auto)
+ by (cases n m q rule: enat3_cases) auto
show "n + m = m + n"
- by (cases n, auto, cases m, auto)
+ by (cases n m rule: enat2_cases) auto
show "0 + n = n"
by (cases n) (simp_all add: zero_enat_def)
qed
@@ -341,6 +344,14 @@
"(\<infinity>::enat) < q \<longleftrightarrow> False"
by (simp_all add: less_eq_enat_def less_enat_def split: enat.splits)
+lemma number_of_le_enat_iff[simp]:
+ shows "number_of m \<le> enat n \<longleftrightarrow> number_of m \<le> n"
+by (auto simp: number_of_enat_def)
+
+lemma number_of_less_enat_iff[simp]:
+ shows "number_of m < enat n \<longleftrightarrow> number_of m < n"
+by (auto simp: number_of_enat_def)
+
lemma enat_ord_code [code]:
"enat m \<le> enat n \<longleftrightarrow> m \<le> n"
"enat m < enat n \<longleftrightarrow> m < n"
--- a/src/HOL/Library/Extended_Real.thy Tue Dec 20 17:40:21 2011 +0100
+++ b/src/HOL/Library/Extended_Real.thy Tue Dec 20 18:46:05 2011 +0100
@@ -55,11 +55,7 @@
instance ..
end
-definition "ereal_of_enat n = (case n of enat n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)"
-
declare [[coercion "ereal :: real \<Rightarrow> ereal"]]
-declare [[coercion "ereal_of_enat :: enat \<Rightarrow> ereal"]]
-declare [[coercion "(\<lambda>n. ereal (real n)) :: nat \<Rightarrow> ereal"]]
lemma ereal_uminus_uminus[simp]:
fixes a :: ereal shows "- (- a) = a"
@@ -1068,6 +1064,28 @@
qed (insert y, simp_all)
qed simp
+lemma ereal_divide_right_mono[simp]:
+ fixes x y z :: ereal
+ assumes "x \<le> y" "0 < z" shows "x / z \<le> y / z"
+using assms by (cases x y z rule: ereal3_cases) (auto intro: divide_right_mono)
+
+lemma ereal_divide_left_mono[simp]:
+ fixes x y z :: ereal
+ assumes "y \<le> x" "0 < z" "0 < x * y"
+ shows "z / x \<le> z / y"
+using assms by (cases x y z rule: ereal3_cases)
+ (auto intro: divide_left_mono simp: field_simps sign_simps split: split_if_asm)
+
+lemma ereal_divide_zero_left[simp]:
+ fixes a :: ereal
+ shows "0 / a = 0"
+ by (cases a) (auto simp: zero_ereal_def)
+
+lemma ereal_times_divide_eq_left[simp]:
+ fixes a b c :: ereal
+ shows "b / c * a = b * a / c"
+ by (cases a b c rule: ereal3_cases) (auto simp: field_simps sign_simps)
+
subsection "Complete lattice"
instantiation ereal :: lattice
@@ -1683,6 +1701,54 @@
finally show ?thesis .
qed
+subsection "Relation to @{typ enat}"
+
+definition "ereal_of_enat n = (case n of enat n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)"
+
+declare [[coercion "ereal_of_enat :: enat \<Rightarrow> ereal"]]
+declare [[coercion "(\<lambda>n. ereal (real n)) :: nat \<Rightarrow> ereal"]]
+
+lemma ereal_of_enat_simps[simp]:
+ "ereal_of_enat (enat n) = ereal n"
+ "ereal_of_enat \<infinity> = \<infinity>"
+ by (simp_all add: ereal_of_enat_def)
+
+lemma ereal_of_enat_le_iff[simp]:
+ "ereal_of_enat m \<le> ereal_of_enat n \<longleftrightarrow> m \<le> n"
+by (cases m n rule: enat2_cases) auto
+
+lemma number_of_le_ereal_of_enat_iff[simp]:
+ shows "number_of m \<le> ereal_of_enat n \<longleftrightarrow> number_of m \<le> n"
+by (cases n) (auto dest: natceiling_le intro: natceiling_le_eq[THEN iffD1])
+
+lemma ereal_of_enat_ge_zero_cancel_iff[simp]:
+ "0 \<le> ereal_of_enat n \<longleftrightarrow> 0 \<le> n"
+by (cases n) (auto simp: enat_0[symmetric])
+
+lemma ereal_of_enat_gt_zero_cancel_iff[simp]:
+ "0 < ereal_of_enat n \<longleftrightarrow> 0 < n"
+by (cases n) (auto simp: enat_0[symmetric])
+
+lemma ereal_of_enat_zero[simp]:
+ "ereal_of_enat 0 = 0"
+by (auto simp: enat_0[symmetric])
+
+lemma ereal_of_enat_add:
+ "ereal_of_enat (m + n) = ereal_of_enat m + ereal_of_enat n"
+by (cases m n rule: enat2_cases) auto
+
+lemma ereal_of_enat_sub:
+ assumes "n \<le> m" shows "ereal_of_enat (m - n) = ereal_of_enat m - ereal_of_enat n "
+using assms by (cases m n rule: enat2_cases) auto
+
+lemma ereal_of_enat_mult:
+ "ereal_of_enat (m * n) = ereal_of_enat m * ereal_of_enat n"
+by (cases m n rule: enat2_cases) auto
+
+lemmas ereal_of_enat_pushin = ereal_of_enat_add ereal_of_enat_sub ereal_of_enat_mult
+lemmas ereal_of_enat_pushout = ereal_of_enat_pushin[symmetric]
+
+
subsection "Limits on @{typ ereal}"
subsubsection "Topological space"
--- a/src/HOL/List.thy Tue Dec 20 17:40:21 2011 +0100
+++ b/src/HOL/List.thy Tue Dec 20 18:46:05 2011 +0100
@@ -3807,6 +3807,39 @@
finally show ?thesis by simp
qed
+lemma card_lists_distinct_length_eq:
+ assumes "k < card A"
+ shows "card {xs. length xs = k \<and> distinct xs \<and> set xs \<subseteq> A} = \<Prod>{card A - k + 1 .. card A}"
+using assms
+proof (induct k)
+ case 0
+ then have "{xs. length xs = 0 \<and> distinct xs \<and> set xs \<subseteq> A} = {[]}" by auto
+ then show ?case by simp
+next
+ case (Suc k)
+ let "?k_list" = "\<lambda>k xs. length xs = k \<and> distinct xs \<and> set xs \<subseteq> A"
+ have inj_Cons: "\<And>A. inj_on (\<lambda>(xs, n). n # xs) A" by (rule inj_onI) auto
+
+ from Suc have "k < card A" by simp
+ moreover have "finite A" using assms by (simp add: card_ge_0_finite)
+ moreover have "finite {xs. ?k_list k xs}"
+ using finite_lists_length_eq[OF `finite A`, of k]
+ by - (rule finite_subset, auto)
+ moreover have "\<And>i j. i \<noteq> j \<longrightarrow> {i} \<times> (A - set i) \<inter> {j} \<times> (A - set j) = {}"
+ by auto
+ moreover have "\<And>i. i \<in>Collect (?k_list k) \<Longrightarrow> card (A - set i) = card A - k"
+ by (simp add: card_Diff_subset distinct_card)
+ moreover have "{xs. ?k_list (Suc k) xs} =
+ (\<lambda>(xs, n). n#xs) ` \<Union>(\<lambda>xs. {xs} \<times> (A - set xs)) ` {xs. ?k_list k xs}"
+ by (auto simp: length_Suc_conv)
+ moreover
+ have "Suc (card A - Suc k) = card A - k" using Suc.prems by simp
+ then have "(card A - k) * \<Prod>{Suc (card A - k)..card A} = \<Prod>{Suc (card A - Suc k)..card A}"
+ by (subst setprod_insert[symmetric]) (simp add: atLeastAtMost_insertL)+
+ ultimately show ?case
+ by (simp add: card_image inj_Cons card_UN_disjoint Suc.hyps algebra_simps)
+qed
+
lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)"
apply(rule notI)
apply(drule finite_maxlen)
--- a/src/HOL/Log.thy Tue Dec 20 17:40:21 2011 +0100
+++ b/src/HOL/Log.thy Tue Dec 20 18:46:05 2011 +0100
@@ -60,6 +60,10 @@
lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
by (simp add: powr_def exp_add [symmetric] left_distrib)
+lemma powr_mult_base:
+ "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
+using assms by (auto simp: powr_add)
+
lemma powr_powr: "(x powr a) powr b = x powr (a * b)"
by (simp add: powr_def)
@@ -178,6 +182,10 @@
apply (rule powr_realpow [THEN sym], simp)
done
+lemma root_powr_inverse:
+ "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
+by (auto simp: root_def powr_realpow[symmetric] powr_powr)
+
lemma ln_powr: "0 < x ==> 0 < y ==> ln(x powr y) = y * ln x"
by (unfold powr_def, simp)
--- a/src/HOL/Nat.thy Tue Dec 20 17:40:21 2011 +0100
+++ b/src/HOL/Nat.thy Tue Dec 20 18:46:05 2011 +0100
@@ -721,10 +721,10 @@
by (rule monoI) simp
lemma min_0L [simp]: "min 0 n = (0::nat)"
-by (rule min_leastL) simp
+by (rule min_absorb1) simp
lemma min_0R [simp]: "min n 0 = (0::nat)"
-by (rule min_leastR) simp
+by (rule min_absorb2) simp
lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)"
by (simp add: mono_Suc min_of_mono)
@@ -738,10 +738,10 @@
by (simp split: nat.split)
lemma max_0L [simp]: "max 0 n = (n::nat)"
-by (rule max_leastL) simp
+by (rule max_absorb2) simp
lemma max_0R [simp]: "max n 0 = (n::nat)"
-by (rule max_leastR) simp
+by (rule max_absorb1) simp
lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc(max m n)"
by (simp add: mono_Suc max_of_mono)
@@ -1615,6 +1615,9 @@
lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)"
by arith
+lemma Suc_diff_Suc: "n < m \<Longrightarrow> Suc (m - Suc n) = m - n"
+by simp
+
text{*Lemmas for ex/Factorization*}
lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
--- a/src/HOL/Number_Theory/Binomial.thy Tue Dec 20 17:40:21 2011 +0100
+++ b/src/HOL/Number_Theory/Binomial.thy Tue Dec 20 18:46:05 2011 +0100
@@ -349,4 +349,17 @@
qed
qed
+lemma choose_le_pow:
+ assumes "r \<le> n" shows "n choose r \<le> n ^ r"
+proof -
+ have X: "\<And>r. r \<le> n \<Longrightarrow> \<Prod>{n - r..n} = (n - r) * \<Prod>{Suc (n - r)..n}"
+ by (subst setprod_insert[symmetric]) (auto simp: atLeastAtMost_insertL)
+ have "n choose r \<le> fact n div fact (n - r)"
+ using `r \<le> n` by (simp add: choose_altdef_nat div_le_mono2)
+ also have "\<dots> \<le> n ^ r" using `r \<le> n`
+ by (induct r rule: nat.induct)
+ (auto simp add: fact_div_fact Suc_diff_Suc X One_nat_def mult_le_mono)
+ finally show ?thesis .
+qed
+
end
--- a/src/HOL/Orderings.thy Tue Dec 20 17:40:21 2011 +0100
+++ b/src/HOL/Orderings.thy Tue Dec 20 18:46:05 2011 +0100
@@ -1050,33 +1050,20 @@
end
-lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
+lemma min_absorb1: "x \<le> y \<Longrightarrow> min x y = x"
by (simp add: min_def)
-lemma max_leastL: "(!!x. least <= x) ==> max least x = x"
+lemma max_absorb2: "x \<le> y ==> max x y = y"
by (simp add: max_def)
-lemma min_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> min x least = least"
-by (simp add: min_def) (blast intro: antisym)
-
-lemma max_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> max x least = x"
-by (simp add: max_def) (blast intro: antisym)
-
-lemma min_greatestL: "(\<And>x::'a::order. x \<le> greatest) \<Longrightarrow> min greatest x = x"
-by (simp add: min_def) (blast intro: antisym)
+lemma min_absorb2: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> min x y = y"
+by (simp add:min_def)
-lemma max_greatestL: "(\<And>x::'a::order. x \<le> greatest) \<Longrightarrow> max greatest x = greatest"
-by (simp add: max_def) (blast intro: antisym)
-
-lemma min_greatestR: "(\<And>x. x \<le> greatest) \<Longrightarrow> min x greatest = x"
-by (simp add: min_def)
-
-lemma max_greatestR: "(\<And>x. x \<le> greatest) \<Longrightarrow> max x greatest = greatest"
+lemma max_absorb1: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> max x y = x"
by (simp add: max_def)
-
subsection {* (Unique) top and bottom elements *}
class bot = order +
--- a/src/HOL/Probability/Probability_Measure.thy Tue Dec 20 17:40:21 2011 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy Tue Dec 20 18:46:05 2011 +0100
@@ -1028,7 +1028,6 @@
proof
show "positive ?P (measure ?P)"
proof (simp add: positive_def, safe)
- show "0 / \<mu> A = 0" using `\<mu> A \<noteq> 0` by (cases "\<mu> A") (auto simp: zero_ereal_def)
fix B assume "B \<in> events"
with real_measure[of "A \<inter> B"] real_measure[OF `A \<in> events`] `A \<in> sets M`
show "0 \<le> \<mu> (A \<inter> B) / \<mu> A" by (auto simp: Int)
--- a/src/HOL/SetInterval.thy Tue Dec 20 17:40:21 2011 +0100
+++ b/src/HOL/SetInterval.thy Tue Dec 20 18:46:05 2011 +0100
@@ -477,6 +477,9 @@
lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}"
by (auto simp add: atLeastAtMost_def)
+lemma atLeastAtMost_insertL: "m \<le> n \<Longrightarrow> insert m {Suc m..n} = {m ..n}"
+by auto
+
text {* The analogous result is useful on @{typ int}: *}
(* here, because we don't have an own int section *)
lemma atLeastAtMostPlus1_int_conv:
--- a/src/Tools/subtyping.ML Tue Dec 20 17:40:21 2011 +0100
+++ b/src/Tools/subtyping.ML Tue Dec 20 18:46:05 2011 +0100
@@ -32,6 +32,14 @@
fun make_data (coes, full_graph, coes_graph, tmaps) =
Data {coes = coes, full_graph = full_graph, coes_graph = coes_graph, tmaps = tmaps};
+fun merge_error_coes (a, b) =
+ error ("Cannot merge coercion tables.\nConflicting declarations for coercions from " ^
+ quote a ^ " to " ^ quote b ^ ".");
+
+fun merge_error_tmaps C =
+ error ("Cannot merge coercion map tables.\nConflicting declarations for the constructor " ^
+ quote C ^ ".");
+
structure Data = Generic_Data
(
type T = data;
@@ -42,10 +50,11 @@
Data {coes = coes2, full_graph = full_graph2, coes_graph = coes_graph2, tmaps = tmaps2}) =
make_data (Symreltab.merge (eq_pair (op aconv)
(eq_pair (eq_pair (eq_list (op =)) (eq_list (op =))) (eq_list (op aconv))))
- (coes1, coes2),
+ (coes1, coes2) handle Symreltab.DUP key => merge_error_coes key,
Graph.merge (op =) (full_graph1, full_graph2),
Graph.merge (op =) (coes_graph1, coes_graph2),
- Symtab.merge (eq_pair (op aconv) (op =)) (tmaps1, tmaps2));
+ Symtab.merge (eq_pair (op aconv) (op =)) (tmaps1, tmaps2)
+ handle Symtab.DUP key => merge_error_tmaps key);
);
fun map_data f =