--- a/src/HOL/Library/Quotient_Product.thy Fri May 07 09:51:55 2010 +0200
+++ b/src/HOL/Library/Quotient_Product.thy Fri May 07 10:00:24 2010 +0200
@@ -93,6 +93,25 @@
shows "(((Abs1 ---> Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> id) split) = split"
by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+lemma [quot_respect]:
+ shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===>
+ prod_rel R2 R1 ===> prod_rel R2 R1 ===> op =) prod_rel prod_rel"
+ by auto
+
+lemma [quot_preserve]:
+ assumes q1: "Quotient R1 abs1 rep1"
+ and q2: "Quotient R2 abs2 rep2"
+ shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) --->
+ prod_fun rep1 rep2 ---> prod_fun rep1 rep2 ---> id) prod_rel = prod_rel"
+ by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+
+lemma [quot_preserve]:
+ shows"(prod_rel ((rep1 ---> rep1 ---> id) R1) ((rep2 ---> rep2 ---> id) R2)
+ (l1, l2) (r1, r2)) = (R1 (rep1 l1) (rep1 r1) \<and> R2 (rep2 l2) (rep2 r2))"
+ by simp
+
+declare Pair_eq[quot_preserve]
+
lemma prod_fun_id[id_simps]:
shows "prod_fun id id = id"
by (simp add: prod_fun_def)
--- a/src/HOL/Metis_Examples/BT.thy Fri May 07 09:51:55 2010 +0200
+++ b/src/HOL/Metis_Examples/BT.thy Fri May 07 10:00:24 2010 +0200
@@ -88,7 +88,7 @@
case Lf thus ?case by (metis reflect.simps(1))
next
case (Br a t1 t2) thus ?case
- by (metis class_semiring.semiring_rules(24) n_nodes.simps(2) reflect.simps(2))
+ by (metis normalizing.semiring_rules(24) n_nodes.simps(2) reflect.simps(2))
qed
declare [[ atp_problem_prefix = "BT__depth_reflect" ]]
--- a/src/HOL/Metis_Examples/BigO.thy Fri May 07 09:51:55 2010 +0200
+++ b/src/HOL/Metis_Examples/BigO.thy Fri May 07 10:00:24 2010 +0200
@@ -41,7 +41,7 @@
fix c :: 'a and x :: 'b
assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> \<bar>x\<^isub>1\<bar>" by (metis abs_ge_zero)
- have F2: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+ have F2: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
have F3: "\<forall>x\<^isub>1 x\<^isub>3. x\<^isub>3 \<le> \<bar>h x\<^isub>1\<bar> \<longrightarrow> x\<^isub>3 \<le> c * \<bar>f x\<^isub>1\<bar>" by (metis A1 order_trans)
have F4: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
by (metis abs_mult)
@@ -70,7 +70,7 @@
proof -
fix c :: 'a and x :: 'b
assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
- have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+ have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
have F2: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
by (metis abs_mult)
have "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_mult_pos abs_one)
@@ -92,7 +92,7 @@
proof -
fix c :: 'a and x :: 'b
assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
- have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+ have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
have F2: "\<forall>x\<^isub>3 x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> x\<^isub>1 \<longrightarrow> \<bar>x\<^isub>3 * x\<^isub>1\<bar> = \<bar>x\<^isub>3\<bar> * x\<^isub>1" by (metis abs_mult_pos)
hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_one)
hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^isub>3\<bar>" by (metis F2 A1 abs_ge_zero order_trans)
@@ -111,7 +111,7 @@
proof -
fix c :: 'a and x :: 'b
assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
- have "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+ have "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>"
by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one)
hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero abs_mult_pos abs_mult)
@@ -145,12 +145,12 @@
declare [[ atp_problem_prefix = "BigO__bigo_refl" ]]
lemma bigo_refl [intro]: "f : O(f)"
apply (auto simp add: bigo_def)
-by (metis class_semiring.mul_1 order_refl)
+by (metis normalizing.mul_1 order_refl)
declare [[ atp_problem_prefix = "BigO__bigo_zero" ]]
lemma bigo_zero: "0 : O(g)"
apply (auto simp add: bigo_def func_zero)
-by (metis class_semiring.mul_0 order_refl)
+by (metis normalizing.mul_0 order_refl)
lemma bigo_zero2: "O(%x.0) = {%x.0}"
apply (auto simp add: bigo_def)
@@ -307,7 +307,7 @@
apply (auto simp add: diff_minus fun_Compl_def func_plus)
prefer 2
apply (drule_tac x = x in spec)+
- apply (metis add_right_mono class_semiring.semiring_rules(24) diff_add_cancel diff_minus_eq_add le_less order_trans)
+ apply (metis add_right_mono normalizing.semiring_rules(24) diff_add_cancel diff_minus_eq_add le_less order_trans)
proof -
fix x :: 'a
assume "\<forall>x. lb x \<le> f x"
@@ -318,13 +318,13 @@
lemma bigo_abs: "(%x. abs(f x)) =o O(f)"
apply (unfold bigo_def)
apply auto
-by (metis class_semiring.mul_1 order_refl)
+by (metis normalizing.mul_1 order_refl)
declare [[ atp_problem_prefix = "BigO__bigo_abs2" ]]
lemma bigo_abs2: "f =o O(%x. abs(f x))"
apply (unfold bigo_def)
apply auto
-by (metis class_semiring.mul_1 order_refl)
+by (metis normalizing.mul_1 order_refl)
lemma bigo_abs3: "O(f) = O(%x. abs(f x))"
proof -
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri May 07 09:51:55 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri May 07 10:00:24 2010 +0200
@@ -1877,7 +1877,7 @@
using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_norm
unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_scaleR
apply (rule mult_left_le_imp_le[of "1 - u"])
- unfolding class_semiring.mul_a using `u<1` by auto
+ unfolding normalizing.mul_a using `u<1` by auto
thus "y \<in> s" using assms(1)[unfolded convex_def, rule_format, of "inverse(1 - u) *\<^sub>R (y - u *\<^sub>R x)" x "1 - u" u]
using as unfolding scaleR_scaleR by auto qed auto
thus "u *\<^sub>R x \<in> s - frontier s" using frontier_def and interior_subset by auto qed
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Fri May 07 09:51:55 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri May 07 10:00:24 2010 +0200
@@ -698,7 +698,7 @@
unfolding o_def apply(rule,rule has_derivative_lift_dot) using assms(3) by auto
then guess x .. note x=this
show ?thesis proof(cases "f a = f b")
- case False have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2" by(simp add:class_semiring.semiring_rules)
+ case False have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2" by(simp add:normalizing.semiring_rules)
also have "\<dots> = (f b - f a) \<bullet> (f b - f a)" unfolding power2_norm_eq_inner ..
also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)" using x unfolding inner_simps by auto
also have "\<dots> \<le> norm (f b - f a) * norm (f' x (b - a))" by(rule norm_cauchy_schwarz)
--- a/src/HOL/Multivariate_Analysis/Integration.thy Fri May 07 09:51:55 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri May 07 10:00:24 2010 +0200
@@ -2533,7 +2533,7 @@
show "content x \<ge> 0" unfolding as snd_conv * interval_doublesplit by(rule content_pos_le)
qed have **:"norm (1::real) \<le> 1" by auto note division_doublesplit[OF p'',unfolded interval_doublesplit]
note dsum_bound[OF this **,unfolded interval_doublesplit[THEN sym]]
- note this[unfolded real_scaleR_def real_norm_def class_semiring.semiring_rules, of k c d] note le_less_trans[OF this d(2)]
+ note this[unfolded real_scaleR_def real_norm_def normalizing.semiring_rules, of k c d] note le_less_trans[OF this d(2)]
from this[unfolded abs_of_nonneg[OF *]] show "(\<Sum>ka\<in>snd ` p. content (ka \<inter> {x. \<bar>x $ k - c\<bar> \<le> d})) < e"
apply(subst vsum_nonzero_image_lemma[of "snd ` p" content "{}", unfolded o_def,THEN sym])
apply(rule finite_imageI p' content_empty)+ unfolding forall_in_division[OF p'']
@@ -4723,7 +4723,7 @@
have "\<And>e sg dsa dia ig. norm(sg) \<le> dsa \<longrightarrow> abs(dsa - dia) < e / 2 \<longrightarrow> norm(sg - ig) < e / 2
\<longrightarrow> norm(ig) < dia + e"
proof safe case goal1 show ?case apply(rule le_less_trans[OF norm_triangle_sub[of ig sg]])
- apply(subst real_sum_of_halves[of e,THEN sym]) unfolding class_semiring.add_a
+ apply(subst real_sum_of_halves[of e,THEN sym]) unfolding normalizing.add_a
apply(rule add_le_less_mono) defer apply(subst norm_minus_commute,rule goal1)
apply(rule order_trans[OF goal1(1)]) using goal1(2) by arith
qed note norm=this[rule_format]
--- a/src/HOL/PReal.thy Fri May 07 09:51:55 2010 +0200
+++ b/src/HOL/PReal.thy Fri May 07 10:00:24 2010 +0200
@@ -47,10 +47,6 @@
by (blast intro: cut_of_rat [OF zero_less_one])
definition
- preal_of_rat :: "rat => preal" where
- "preal_of_rat q = Abs_preal {x::rat. 0 < x & x < q}"
-
-definition
psup :: "preal set => preal" where
[code del]: "psup P = Abs_preal (\<Union>X \<in> P. Rep_preal X)"
@@ -101,7 +97,7 @@
definition
preal_one_def:
- "1 == preal_of_rat 1"
+ "1 == Abs_preal {x. 0 < x & x < 1}"
instance ..
@@ -172,25 +168,6 @@
lemmas not_in_Rep_preal_ub = not_in_preal_ub [OF Rep_preal]
-
-subsection{*@{term preal_of_prat}: the Injection from prat to preal*}
-
-lemma rat_less_set_mem_preal: "0 < y ==> {u::rat. 0 < u & u < y} \<in> preal"
-by (simp add: preal_def cut_of_rat)
-
-lemma rat_subset_imp_le:
- "[|{u::rat. 0 < u & u < x} \<subseteq> {u. 0 < u & u < y}; 0<x|] ==> x \<le> y"
-apply (simp add: linorder_not_less [symmetric])
-apply (blast dest: dense intro: order_less_trans)
-done
-
-lemma rat_set_eq_imp_eq:
- "[|{u::rat. 0 < u & u < x} = {u. 0 < u & u < y};
- 0 < x; 0 < y|] ==> x = y"
-by (blast intro: rat_subset_imp_le order_antisym)
-
-
-
subsection{*Properties of Ordering*}
instance preal :: order
@@ -355,12 +332,6 @@
show "a + b = b + a" by (rule preal_add_commute)
qed
-lemma preal_add_left_commute: "x + (y + z) = y + ((x + z)::preal)"
-by (rule add_left_commute)
-
-text{* Positive Real addition is an AC operator *}
-lemmas preal_add_ac = preal_add_assoc preal_add_commute preal_add_left_commute
-
subsection{*Properties of Multiplication*}
@@ -490,19 +461,10 @@
show "a * b = b * a" by (rule preal_mult_commute)
qed
-lemma preal_mult_left_commute: "x * (y * z) = y * ((x * z)::preal)"
-by (rule mult_left_commute)
-
-
-text{* Positive Real multiplication is an AC operator *}
-lemmas preal_mult_ac =
- preal_mult_assoc preal_mult_commute preal_mult_left_commute
-
text{* Positive real 1 is the multiplicative identity element *}
lemma preal_mult_1: "(1::preal) * z = z"
-unfolding preal_one_def
proof (induct z)
fix A :: "rat set"
assume A: "A \<in> preal"
@@ -543,17 +505,14 @@
qed
qed
qed
- thus "preal_of_rat 1 * Abs_preal A = Abs_preal A"
- by (simp add: preal_of_rat_def preal_mult_def mult_set_def
+ thus "1 * Abs_preal A = Abs_preal A"
+ by (simp add: preal_one_def preal_mult_def mult_set_def
rat_mem_preal A)
qed
instance preal :: comm_monoid_mult
by intro_classes (rule preal_mult_1)
-lemma preal_mult_1_right: "z * (1::preal) = z"
-by (rule mult_1_right)
-
subsection{*Distribution of Multiplication across Addition*}
@@ -839,9 +798,9 @@
apply (simp add: inverse_set_def)
done
-lemma Rep_preal_of_rat:
- "0 < q ==> Rep_preal (preal_of_rat q) = {x. 0 < x \<and> x < q}"
-by (simp add: preal_of_rat_def rat_mem_preal)
+lemma Rep_preal_one:
+ "Rep_preal 1 = {x. 0 < x \<and> x < 1}"
+by (simp add: preal_one_def rat_mem_preal)
lemma subset_inverse_mult_lemma:
assumes xpos: "0 < x" and xless: "x < 1"
@@ -871,8 +830,8 @@
qed
lemma subset_inverse_mult:
- "Rep_preal(preal_of_rat 1) \<subseteq> Rep_preal(inverse R * R)"
-apply (auto simp add: Bex_def Rep_preal_of_rat mem_Rep_preal_inverse_iff
+ "Rep_preal 1 \<subseteq> Rep_preal(inverse R * R)"
+apply (auto simp add: Bex_def Rep_preal_one mem_Rep_preal_inverse_iff
mem_Rep_preal_mult_iff)
apply (blast dest: subset_inverse_mult_lemma)
done
@@ -894,15 +853,14 @@
qed
lemma inverse_mult_subset:
- "Rep_preal(inverse R * R) \<subseteq> Rep_preal(preal_of_rat 1)"
-apply (auto simp add: Bex_def Rep_preal_of_rat mem_Rep_preal_inverse_iff
+ "Rep_preal(inverse R * R) \<subseteq> Rep_preal 1"
+apply (auto simp add: Bex_def Rep_preal_one mem_Rep_preal_inverse_iff
mem_Rep_preal_mult_iff)
apply (simp add: zero_less_mult_iff preal_imp_pos [OF Rep_preal])
apply (blast intro: inverse_mult_subset_lemma)
done
lemma preal_mult_inverse: "inverse R * R = (1::preal)"
-unfolding preal_one_def
apply (rule Rep_preal_inject [THEN iffD1])
apply (rule equalityI [OF inverse_mult_subset subset_inverse_mult])
done
@@ -950,12 +908,6 @@
apply (simp add: Rep_preal_self_subset Rep_preal_sum_not_eq [THEN not_sym])
done
-lemma preal_self_less_add_right: "(R::preal) < S + R"
-by (simp add: preal_add_commute preal_self_less_add_left)
-
-lemma preal_not_eq_self: "x \<noteq> x + (y::preal)"
-by (insert preal_self_less_add_left [of x y], auto)
-
subsection{*Subtraction for Positive Reals*}
@@ -1117,25 +1069,12 @@
lemma preal_add_left_less_cancel: "T + R < T + S ==> R < (S::preal)"
by (auto elim: preal_add_right_less_cancel simp add: preal_add_commute [of T])
-lemma preal_add_less_cancel_right: "((R::preal) + T < S + T) = (R < S)"
-by (blast intro: preal_add_less2_mono1 preal_add_right_less_cancel)
-
lemma preal_add_less_cancel_left: "(T + (R::preal) < T + S) = (R < S)"
by (blast intro: preal_add_less2_mono2 preal_add_left_less_cancel)
-lemma preal_add_le_cancel_right: "((R::preal) + T \<le> S + T) = (R \<le> S)"
-by (simp add: linorder_not_less [symmetric] preal_add_less_cancel_right)
-
lemma preal_add_le_cancel_left: "(T + (R::preal) \<le> T + S) = (R \<le> S)"
by (simp add: linorder_not_less [symmetric] preal_add_less_cancel_left)
-lemma preal_add_less_mono:
- "[| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::preal)"
-apply (auto dest!: less_add_left_Ex simp add: preal_add_ac)
-apply (rule preal_add_assoc [THEN subst])
-apply (rule preal_self_less_add_right)
-done
-
lemma preal_add_right_cancel: "(R::preal) + T = S + T ==> R = S"
apply (insert linorder_less_linear [of R S], safe)
apply (drule_tac [!] T = T in preal_add_less2_mono1, auto)
@@ -1144,17 +1083,6 @@
lemma preal_add_left_cancel: "C + A = C + B ==> A = (B::preal)"
by (auto intro: preal_add_right_cancel simp add: preal_add_commute)
-lemma preal_add_left_cancel_iff: "(C + A = C + B) = ((A::preal) = B)"
-by (fast intro: preal_add_left_cancel)
-
-lemma preal_add_right_cancel_iff: "(A + C = B + C) = ((A::preal) = B)"
-by (fast intro: preal_add_right_cancel)
-
-lemmas preal_cancels =
- preal_add_less_cancel_right preal_add_less_cancel_left
- preal_add_le_cancel_right preal_add_le_cancel_left
- preal_add_left_cancel_iff preal_add_right_cancel_iff
-
instance preal :: linordered_cancel_ab_semigroup_add
proof
fix a b c :: preal
@@ -1232,117 +1160,4 @@
apply (auto simp add: preal_less_def)
done
-
-subsection{*The Embedding from @{typ rat} into @{typ preal}*}
-
-lemma preal_of_rat_add_lemma1:
- "[|x < y + z; 0 < x; 0 < y|] ==> x * y * inverse (y + z) < (y::rat)"
-apply (frule_tac c = "y * inverse (y + z) " in mult_strict_right_mono)
-apply (simp add: zero_less_mult_iff)
-apply (simp add: mult_ac)
-done
-
-lemma preal_of_rat_add_lemma2:
- assumes "u < x + y"
- and "0 < x"
- and "0 < y"
- and "0 < u"
- shows "\<exists>v w::rat. w < y & 0 < v & v < x & 0 < w & u = v + w"
-proof (intro exI conjI)
- show "u * x * inverse(x+y) < x" using prems
- by (simp add: preal_of_rat_add_lemma1)
- show "u * y * inverse(x+y) < y" using prems
- by (simp add: preal_of_rat_add_lemma1 add_commute [of x])
- show "0 < u * x * inverse (x + y)" using prems
- by (simp add: zero_less_mult_iff)
- show "0 < u * y * inverse (x + y)" using prems
- by (simp add: zero_less_mult_iff)
- show "u = u * x * inverse (x + y) + u * y * inverse (x + y)" using prems
- by (simp add: left_distrib [symmetric] right_distrib [symmetric] mult_ac)
-qed
-
-lemma preal_of_rat_add:
- "[| 0 < x; 0 < y|]
- ==> preal_of_rat ((x::rat) + y) = preal_of_rat x + preal_of_rat y"
-apply (unfold preal_of_rat_def preal_add_def)
-apply (simp add: rat_mem_preal)
-apply (rule_tac f = Abs_preal in arg_cong)
-apply (auto simp add: add_set_def)
-apply (blast dest: preal_of_rat_add_lemma2)
-done
-
-lemma preal_of_rat_mult_lemma1:
- "[|x < y; 0 < x; 0 < z|] ==> x * z * inverse y < (z::rat)"
-apply (frule_tac c = "z * inverse y" in mult_strict_right_mono)
-apply (simp add: zero_less_mult_iff)
-apply (subgoal_tac "y * (z * inverse y) = z * (y * inverse y)")
-apply (simp_all add: mult_ac)
-done
-
-lemma preal_of_rat_mult_lemma2:
- assumes xless: "x < y * z"
- and xpos: "0 < x"
- and ypos: "0 < y"
- shows "x * z * inverse y * inverse z < (z::rat)"
-proof -
- have "0 < y * z" using prems by simp
- hence zpos: "0 < z" using prems by (simp add: zero_less_mult_iff)
- have "x * z * inverse y * inverse z = x * inverse y * (z * inverse z)"
- by (simp add: mult_ac)
- also have "... = x/y" using zpos
- by (simp add: divide_inverse)
- also from xless have "... < z"
- by (simp add: pos_divide_less_eq [OF ypos] mult_commute)
- finally show ?thesis .
-qed
-
-lemma preal_of_rat_mult_lemma3:
- assumes uless: "u < x * y"
- and "0 < x"
- and "0 < y"
- and "0 < u"
- shows "\<exists>v w::rat. v < x & w < y & 0 < v & 0 < w & u = v * w"
-proof -
- from dense [OF uless]
- obtain r where "u < r" "r < x * y" by blast
- thus ?thesis
- proof (intro exI conjI)
- show "u * x * inverse r < x" using prems
- by (simp add: preal_of_rat_mult_lemma1)
- show "r * y * inverse x * inverse y < y" using prems
- by (simp add: preal_of_rat_mult_lemma2)
- show "0 < u * x * inverse r" using prems
- by (simp add: zero_less_mult_iff)
- show "0 < r * y * inverse x * inverse y" using prems
- by (simp add: zero_less_mult_iff)
- have "u * x * inverse r * (r * y * inverse x * inverse y) =
- u * (r * inverse r) * (x * inverse x) * (y * inverse y)"
- by (simp only: mult_ac)
- thus "u = u * x * inverse r * (r * y * inverse x * inverse y)" using prems
- by simp
- qed
-qed
-
-lemma preal_of_rat_mult:
- "[| 0 < x; 0 < y|]
- ==> preal_of_rat ((x::rat) * y) = preal_of_rat x * preal_of_rat y"
-apply (unfold preal_of_rat_def preal_mult_def)
-apply (simp add: rat_mem_preal)
-apply (rule_tac f = Abs_preal in arg_cong)
-apply (auto simp add: zero_less_mult_iff mult_strict_mono mult_set_def)
-apply (blast dest: preal_of_rat_mult_lemma3)
-done
-
-lemma preal_of_rat_less_iff:
- "[| 0 < x; 0 < y|] ==> (preal_of_rat x < preal_of_rat y) = (x < y)"
-by (force simp add: preal_of_rat_def preal_less_def rat_mem_preal)
-
-lemma preal_of_rat_le_iff:
- "[| 0 < x; 0 < y|] ==> (preal_of_rat x \<le> preal_of_rat y) = (x \<le> y)"
-by (simp add: preal_of_rat_less_iff linorder_not_less [symmetric])
-
-lemma preal_of_rat_eq_iff:
- "[| 0 < x; 0 < y|] ==> (preal_of_rat x = preal_of_rat y) = (x = y)"
-by (simp add: preal_of_rat_le_iff order_eq_iff)
-
end
--- a/src/HOL/Probability/Lebesgue.thy Fri May 07 09:51:55 2010 +0200
+++ b/src/HOL/Probability/Lebesgue.thy Fri May 07 10:00:24 2010 +0200
@@ -938,17 +938,17 @@
proof safe
fix t assume t: "t \<in> space M"
{ fix m n :: nat assume "m \<le> n"
- hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding class_semiring.mul_pwr by auto
+ hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding normalizing.mul_pwr by auto
have "real (natfloor (f t * 2^m) * natfloor (2^(n-m))) \<le> real (natfloor (f t * 2 ^ n))"
apply (subst *)
- apply (subst class_semiring.mul_a)
+ apply (subst normalizing.mul_a)
apply (subst real_of_nat_le_iff)
apply (rule le_mult_natfloor)
using nonneg[OF t] by (auto intro!: mult_nonneg_nonneg)
hence "real (natfloor (f t * 2^m)) * 2^n \<le> real (natfloor (f t * 2^n)) * 2^m"
apply (subst *)
- apply (subst (3) class_semiring.mul_c)
- apply (subst class_semiring.mul_a)
+ apply (subst (3) normalizing.mul_c)
+ apply (subst normalizing.mul_a)
by (auto intro: mult_right_mono simp: natfloor_power real_of_nat_power[symmetric]) }
thus "incseq (\<lambda>n. ?u n t)" unfolding u_at_t[OF t] unfolding incseq_def
by (auto simp add: le_divide_eq divide_le_eq less_divide_eq)