# HG changeset patch
# User noschinl
# Date 1324403165 -3600
# Node ID 0724e56b5dea19b70fc5343753d166f2618e5746
# Parent  32f769f94ea4442a52dc7fdd5d84053b85244e10# Parent  d7d6c8cfb6f677402b349f709d70b3d07b6d53b6
merged

diff -r d7d6c8cfb6f6 -r 0724e56b5dea src/HOL/Fact.thy
--- 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} *}
 
diff -r d7d6c8cfb6f6 -r 0724e56b5dea src/HOL/Library/Extended_Nat.thy
--- 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"
diff -r d7d6c8cfb6f6 -r 0724e56b5dea src/HOL/Library/Extended_Real.thy
--- 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"
diff -r d7d6c8cfb6f6 -r 0724e56b5dea src/HOL/List.thy
--- 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)
diff -r d7d6c8cfb6f6 -r 0724e56b5dea src/HOL/Log.thy
--- 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)
 
diff -r d7d6c8cfb6f6 -r 0724e56b5dea src/HOL/Nat.thy
--- 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"
diff -r d7d6c8cfb6f6 -r 0724e56b5dea src/HOL/Number_Theory/Binomial.thy
--- 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
diff -r d7d6c8cfb6f6 -r 0724e56b5dea src/HOL/Orderings.thy
--- 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 +
diff -r d7d6c8cfb6f6 -r 0724e56b5dea src/HOL/Probability/Probability_Measure.thy
--- 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)
diff -r d7d6c8cfb6f6 -r 0724e56b5dea src/HOL/SetInterval.thy
--- 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:
diff -r d7d6c8cfb6f6 -r 0724e56b5dea src/Tools/subtyping.ML
--- 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 =