merged

--- a/NEWS	Sat Sep 03 22:05:25 2011 +0200
+++ b/NEWS	Sat Sep 03 22:11:49 2011 +0200
@@ -204,6 +204,7 @@
 removed, and other theorems have been renamed or replaced with more
 general versions. INCOMPATIBILITY.
 
+  finite_choice ~> finite_set_choice
   eventually_conjI ~> eventually_conj
   eventually_and ~> eventually_conj_iff
   eventually_false ~> eventually_False

--- a/src/HOL/Fields.thy	Sat Sep 03 22:05:25 2011 +0200
+++ b/src/HOL/Fields.thy	Sat Sep 03 22:11:49 2011 +0200
@@ -207,18 +207,6 @@
   thus ?thesis by (simp add: nonzero_inverse_minus_eq)
 qed
 
-lemma inverse_eq_imp_eq:
-  "inverse a = inverse b \<Longrightarrow> a = b"
-apply (cases "a=0 | b=0") 
- apply (force dest!: inverse_zero_imp_zero
-              simp add: eq_commute [of "0::'a"])
-apply (force dest!: nonzero_inverse_eq_imp_eq) 
-done
-
-lemma inverse_eq_iff_eq [simp]:
-  "inverse a = inverse b \<longleftrightarrow> a = b"
-  by (force dest!: inverse_eq_imp_eq)
-
 lemma inverse_inverse_eq [simp]:
   "inverse (inverse a) = a"
 proof cases
@@ -228,6 +216,14 @@
   thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
 qed
 
+lemma inverse_eq_imp_eq:
+  "inverse a = inverse b \<Longrightarrow> a = b"
+  by (drule arg_cong [where f="inverse"], simp)
+
+lemma inverse_eq_iff_eq [simp]:
+  "inverse a = inverse b \<longleftrightarrow> a = b"
+  by (force dest!: inverse_eq_imp_eq)
+
 end
 
 subsection {* Fields *}

--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sat Sep 03 22:05:25 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sat Sep 03 22:11:49 2011 +0200
@@ -270,13 +270,6 @@
 
 subsection {* Metric space *}
 
-(* TODO: move somewhere else *)
-lemma finite_choice: "finite A \<Longrightarrow> \<forall>x\<in>A. \<exists>y. P x y \<Longrightarrow> \<exists>f. \<forall>x\<in>A. P x (f x)"
-apply (induct set: finite, simp_all)
-apply (clarify, rename_tac y)
-apply (rule_tac x="f(x:=y)" in exI, simp)
-done
-
 instantiation vec :: (metric_space, finite) metric_space
 begin
 
@@ -311,7 +304,7 @@
       have "\<forall>i\<in>UNIV. \<exists>r>0. \<forall>y. dist y (x $ i) < r \<longrightarrow> y \<in> A i"
         using A unfolding open_dist by simp
       hence "\<exists>r. \<forall>i\<in>UNIV. 0 < r i \<and> (\<forall>y. dist y (x $ i) < r i \<longrightarrow> y \<in> A i)"
-        by (rule finite_choice [OF finite])
+        by (rule finite_set_choice [OF finite])
       then obtain r where r1: "\<forall>i. 0 < r i"
         and r2: "\<forall>i y. dist y (x $ i) < r i \<longrightarrow> y \<in> A i" by fast
       have "0 < Min (range r) \<and> (\<forall>y. dist y x < Min (range r) \<longrightarrow> y \<in> S)"

--- a/src/HOL/RComplete.thy	Sat Sep 03 22:05:25 2011 +0200
+++ b/src/HOL/RComplete.thy	Sat Sep 03 22:11:49 2011 +0200
@@ -255,12 +255,6 @@
 lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
   unfolding real_of_nat_def by simp
 
-lemma ceiling_floor [simp]: "ceiling (real (floor r)) = floor r"
-  unfolding real_of_int_def by simp
-
-lemma floor_ceiling [simp]: "floor (real (ceiling r)) = ceiling r"
-  unfolding real_of_int_def by simp
-
 lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)"
   unfolding real_of_int_def by (rule le_of_int_ceiling)
 
@@ -340,44 +334,30 @@
   by (unfold natfloor_def, simp)
 
 lemma natfloor_neg: "x <= 0 ==> natfloor x = 0"
-  apply (unfold natfloor_def)
-  apply (subgoal_tac "floor x <= floor 0")
-  apply simp
-  apply (erule floor_mono)
-done
+  unfolding natfloor_def by simp
+
+lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y"
+  by simp (* TODO: move to Int.thy *)
 
 lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y"
-  apply (case_tac "0 <= x")
-  apply (subst natfloor_def)+
-  apply (subst nat_le_eq_zle)
-  apply force
-  apply (erule floor_mono)
-  apply (subst natfloor_neg)
-  apply simp
-  apply simp
-done
+  unfolding natfloor_def by (intro nat_mono floor_mono)
 
 lemma le_natfloor: "real x <= a ==> x <= natfloor a"
   apply (unfold natfloor_def)
   apply (subst nat_int [THEN sym])
-  apply (subst nat_le_eq_zle)
-  apply simp
+  apply (rule nat_mono)
   apply (rule le_floor)
   apply simp
 done
 
+lemma natfloor_less_iff: "0 \<le> x \<Longrightarrow> natfloor x < n \<longleftrightarrow> x < real n"
+  unfolding natfloor_def real_of_nat_def
+  by (simp add: nat_less_iff floor_less_iff)
+
 lemma less_natfloor:
   assumes "0 \<le> x" and "x < real (n :: nat)"
   shows "natfloor x < n"
-proof (rule ccontr)
-  assume "\<not> ?thesis" hence *: "n \<le> natfloor x" by simp
-  note assms(2)
-  also have "real n \<le> real (natfloor x)"
-    using * unfolding real_of_nat_le_iff .
-  finally have "x < real (natfloor x)" .
-  with real_natfloor_le[OF assms(1)]
-  show False by auto
-qed
+  using assms by (simp add: natfloor_less_iff)
 
 lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)"
   apply (rule iffI)
@@ -408,14 +388,7 @@
 done
 
 lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n"
-  apply (unfold natfloor_def)
-  apply (subst (2) nat_int [THEN sym])
-  apply (subst eq_nat_nat_iff)
-  apply simp
-  apply simp
-  apply (rule floor_eq2)
-  apply auto
-done
+  unfolding natfloor_def by (simp add: floor_eq2 [where n="int n"])
 
 lemma real_natfloor_add_one_gt: "x < real(natfloor x) + 1"
   apply (case_tac "0 <= x")
@@ -434,110 +407,48 @@
 done
 
 lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a"
-  apply (unfold natfloor_def)
-  apply (subgoal_tac "real a = real (int a)")
-  apply (erule ssubst)
-  apply (simp add: nat_add_distrib del: real_of_int_of_nat_eq)
-  apply simp
-done
+  unfolding natfloor_def
+  unfolding real_of_int_of_nat_eq [symmetric] floor_add
+  by (simp add: nat_add_distrib)
 
 lemma natfloor_add_number_of [simp]:
     "~neg ((number_of n)::int) ==> 0 <= x ==>
       natfloor (x + number_of n) = natfloor x + number_of n"
-  apply (subst natfloor_add [THEN sym])
-  apply simp_all
-done
+  by (simp add: natfloor_add [symmetric])
 
 lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1"
-  apply (subst natfloor_add [THEN sym])
-  apply assumption
-  apply simp
-done
+  by (simp add: natfloor_add [symmetric] del: One_nat_def)
 
 lemma natfloor_subtract [simp]: "real a <= x ==>
     natfloor(x - real a) = natfloor x - a"
-  apply (unfold natfloor_def)
-  apply (subgoal_tac "real a = real (int a)")
-  apply (erule ssubst)
-  apply (simp del: real_of_int_of_nat_eq)
-  apply simp
-done
+  unfolding natfloor_def
+  unfolding real_of_int_of_nat_eq [symmetric] floor_subtract
+  by simp
 
 lemma natfloor_div_nat:
   assumes "1 <= x" and "y > 0"
   shows "natfloor (x / real y) = natfloor x div y"
-proof -
-  have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y"
-    by simp
-  then have a: "real(natfloor x) = real ((natfloor x) div y) * real y +
-    real((natfloor x) mod y)"
-    by (simp only: real_of_nat_add [THEN sym] real_of_nat_mult [THEN sym])
-  have "x = real(natfloor x) + (x - real(natfloor x))"
-    by simp
-  then have "x = real ((natfloor x) div y) * real y +
-      real((natfloor x) mod y) + (x - real(natfloor x))"
-    by (simp add: a)
-  then have "x / real y = ... / real y"
-    by simp
-  also have "... = real((natfloor x) div y) + real((natfloor x) mod y) /
-    real y + (x - real(natfloor x)) / real y"
-    by (auto simp add: algebra_simps add_divide_distrib diff_divide_distrib)
-  finally have "natfloor (x / real y) = natfloor(...)" by simp
-  also have "... = natfloor(real((natfloor x) mod y) /
-    real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))"
-    by (simp add: add_ac)
-  also have "... = natfloor(real((natfloor x) mod y) /
-    real y + (x - real(natfloor x)) / real y) + (natfloor x) div y"
-    apply (rule natfloor_add)
-    apply (rule add_nonneg_nonneg)
-    apply (rule divide_nonneg_pos)
-    apply simp
-    apply (simp add: assms)
-    apply (rule divide_nonneg_pos)
-    apply (simp add: algebra_simps)
-    apply (rule real_natfloor_le)
-    using assms apply auto
+proof (rule natfloor_eq)
+  have "(natfloor x) div y * y \<le> natfloor x"
+    by (rule add_leD1 [where k="natfloor x mod y"], simp)
+  thus "real (natfloor x div y) \<le> x / real y"
+    using assms by (simp add: le_divide_eq le_natfloor_eq)
+  have "natfloor x < (natfloor x) div y * y + y"
+    apply (subst mod_div_equality [symmetric])
+    apply (rule add_strict_left_mono)
+    apply (rule mod_less_divisor)
+    apply fact
     done
-  also have "natfloor(real((natfloor x) mod y) /
-    real y + (x - real(natfloor x)) / real y) = 0"
-    apply (rule natfloor_eq)
-    apply simp
-    apply (rule add_nonneg_nonneg)
-    apply (rule divide_nonneg_pos)
-    apply force
-    apply (force simp add: assms)
-    apply (rule divide_nonneg_pos)
-    apply (simp add: algebra_simps)
-    apply (rule real_natfloor_le)
-    apply (auto simp add: assms)
-    using assms apply arith
-    using assms apply (simp add: add_divide_distrib [THEN sym])
-    apply (subgoal_tac "real y = real y - 1 + 1")
-    apply (erule ssubst)
-    apply (rule add_le_less_mono)
-    apply (simp add: algebra_simps)
-    apply (subgoal_tac "1 + real(natfloor x mod y) =
-      real(natfloor x mod y + 1)")
-    apply (erule ssubst)
-    apply (subst real_of_nat_le_iff)
-    apply (subgoal_tac "natfloor x mod y < y")
-    apply arith
-    apply (rule mod_less_divisor)
-    apply auto
-    using real_natfloor_add_one_gt
-    apply (simp add: algebra_simps)
-    done
-  finally show ?thesis by simp
+  thus "x / real y < real (natfloor x div y) + 1"
+    using assms
+    by (simp add: divide_less_eq natfloor_less_iff left_distrib)
 qed
 
 lemma le_mult_natfloor:
   assumes "0 \<le> (a :: real)" and "0 \<le> b"
   shows "natfloor a * natfloor b \<le> natfloor (a * b)"
-  unfolding natfloor_def
-  apply (subst nat_mult_distrib[symmetric])
-  using assms apply simp
-  apply (subst nat_le_eq_zle)
-  using assms le_mult_floor by (auto intro!: mult_nonneg_nonneg)
+  using assms
+  by (simp add: le_natfloor_eq mult_nonneg_nonneg mult_mono' real_natfloor_le)
 
 lemma natceiling_zero [simp]: "natceiling 0 = 0"
   by (unfold natceiling_def, simp)
@@ -555,126 +466,57 @@
   by (unfold natceiling_def, simp)
 
 lemma real_natceiling_ge: "x <= real(natceiling x)"
-  apply (unfold natceiling_def)
-  apply (case_tac "x < 0")
-  apply simp
-  apply (subst real_nat_eq_real)
-  apply (subgoal_tac "ceiling 0 <= ceiling x")
-  apply simp
-  apply (rule ceiling_mono)
-  apply simp
-  apply simp
-done
+  unfolding natceiling_def by (cases "x < 0", simp_all)
 
 lemma natceiling_neg: "x <= 0 ==> natceiling x = 0"
-  apply (unfold natceiling_def)
-  apply simp
-done
+  unfolding natceiling_def by simp
 
 lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y"
-  apply (case_tac "0 <= x")
-  apply (subst natceiling_def)+
-  apply (subst nat_le_eq_zle)
-  apply (rule disjI2)
-  apply (subgoal_tac "real (0::int) <= real(ceiling y)")
-  apply simp
-  apply (rule order_trans)
-  apply simp
-  apply (erule order_trans)
-  apply simp
-  apply (erule ceiling_mono)
-  apply (subst natceiling_neg)
-  apply simp_all
-done
+  unfolding natceiling_def by (intro nat_mono ceiling_mono)
+
+lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n"
+  by auto (* TODO: move to Int.thy *)
 
 lemma natceiling_le: "x <= real a ==> natceiling x <= a"
-  apply (unfold natceiling_def)
-  apply (case_tac "x < 0")
-  apply simp
-  apply (subst (2) nat_int [THEN sym])
-  apply (subst nat_le_eq_zle)
-  apply simp
-  apply (rule ceiling_le)
-  apply simp
-done
+  unfolding natceiling_def real_of_nat_def
+  by (simp add: nat_le_iff ceiling_le_iff)
 
 lemma natceiling_le_eq: "0 <= x ==> (natceiling x <= a) = (x <= real a)"
-  apply (rule iffI)
-  apply (rule order_trans)
-  apply (rule real_natceiling_ge)
-  apply (subst real_of_nat_le_iff)
-  apply assumption
-  apply (erule natceiling_le)
-done
+  unfolding natceiling_def real_of_nat_def (* FIXME: unused assumption *)
+  by (simp add: nat_le_iff ceiling_le_iff)
 
 lemma natceiling_le_eq_number_of [simp]:
     "~ neg((number_of n)::int) ==> 0 <= x ==>
       (natceiling x <= number_of n) = (x <= number_of n)"
-  apply (subst natceiling_le_eq, assumption)
-  apply simp
-done
+  by (simp add: natceiling_le_eq)
 
 lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)"
-  apply (case_tac "0 <= x")
-  apply (subst natceiling_le_eq)
-  apply assumption
-  apply simp
-  apply (subst natceiling_neg)
-  apply simp
-  apply simp
-done
+  unfolding natceiling_def
+  by (simp add: nat_le_iff ceiling_le_iff)
 
 lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1"
-  apply (unfold natceiling_def)
-  apply (simplesubst nat_int [THEN sym]) back back
-  apply (subgoal_tac "nat(int n) + 1 = nat(int n + 1)")
-  apply (erule ssubst)
-  apply (subst eq_nat_nat_iff)
-  apply (subgoal_tac "ceiling 0 <= ceiling x")
-  apply simp
-  apply (rule ceiling_mono)
-  apply force
-  apply force
-  apply (rule ceiling_eq2)
-  apply (simp, simp)
-  apply (subst nat_add_distrib)
-  apply auto
-done
+  unfolding natceiling_def
+  by (simp add: ceiling_eq2 [where n="int n"])
 
 lemma natceiling_add [simp]: "0 <= x ==>
     natceiling (x + real a) = natceiling x + a"
-  apply (unfold natceiling_def)
-  apply (subgoal_tac "real a = real (int a)")
-  apply (erule ssubst)
-  apply (simp del: real_of_int_of_nat_eq)
-  apply (subst nat_add_distrib)
-  apply (subgoal_tac "0 = ceiling 0")
-  apply (erule ssubst)
-  apply (erule ceiling_mono)
-  apply simp_all
-done
+  unfolding natceiling_def
+  unfolding real_of_int_of_nat_eq [symmetric] ceiling_add
+  by (simp add: nat_add_distrib)
 
 lemma natceiling_add_number_of [simp]:
     "~ neg ((number_of n)::int) ==> 0 <= x ==>
       natceiling (x + number_of n) = natceiling x + number_of n"
-  apply (subst natceiling_add [THEN sym])
-  apply simp_all
-done
+  by (simp add: natceiling_add [symmetric])
 
 lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1"
-  apply (subst natceiling_add [THEN sym])
-  apply assumption
-  apply simp
-done
+  by (simp add: natceiling_add [symmetric] del: One_nat_def)
 
 lemma natceiling_subtract [simp]: "real a <= x ==>
     natceiling(x - real a) = natceiling x - a"
-  apply (unfold natceiling_def)
-  apply (subgoal_tac "real a = real (int a)")
-  apply (erule ssubst)
-  apply (simp del: real_of_int_of_nat_eq)
-  apply simp
-done
+  unfolding natceiling_def
+  unfolding real_of_int_of_nat_eq [symmetric] ceiling_subtract
+  by simp
 
 subsection {* Exponentiation with floor *}