--- a/NEWS Wed May 12 11:17:59 2010 +0200
+++ b/NEWS Wed May 12 11:18:42 2010 +0200
@@ -149,6 +149,9 @@
* Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.
INCOMPATIBILITY.
+* Dropped normalizing_semiring etc; use the facts in semiring classes instead.
+INCOMPATIBILITY.
+
* Theory 'Finite_Set': various folding_* locales facilitate the application
of the various fold combinators on finite sets.
--- a/src/HOL/Metis_Examples/BT.thy Wed May 12 11:17:59 2010 +0200
+++ b/src/HOL/Metis_Examples/BT.thy Wed May 12 11:18:42 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 normalizing.semiring_rules(24) n_nodes.simps(2) reflect.simps(2))
+ by (metis add_commute n_nodes.simps(2) reflect.simps(2))
qed
declare [[ atp_problem_prefix = "BT__depth_reflect" ]]
--- a/src/HOL/Metis_Examples/BigO.thy Wed May 12 11:17:59 2010 +0200
+++ b/src/HOL/Metis_Examples/BigO.thy Wed May 12 11:18:42 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 normalizing.mul_1)
+ have F2: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_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)
@@ -66,11 +66,11 @@
apply auto
apply (case_tac "c = 0", simp)
apply (rule_tac x = "1" in exI, simp)
- apply (rule_tac x = "abs c" in exI, auto);
+ apply (rule_tac x = "abs c" in exI, auto)
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 normalizing.mul_1)
+ have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_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 normalizing.mul_1)
+ have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_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 normalizing.mul_1)
+ have "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_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)
@@ -131,26 +131,26 @@
apply (rule conjI)
apply (rule mult_pos_pos)
apply (assumption)+
-(*sledgehammer*);
+(*sledgehammer*)
apply (rule allI)
apply (drule_tac x = "xa" in spec)+
- apply (subgoal_tac "ca * abs(f xa) <= ca * (c * abs(g xa))");
+ apply (subgoal_tac "ca * abs(f xa) <= ca * (c * abs(g xa))")
apply (erule order_trans)
apply (simp add: mult_ac)
apply (rule mult_left_mono, assumption)
- apply (rule order_less_imp_le, assumption);
+ apply (rule order_less_imp_le, assumption)
done
declare [[ atp_problem_prefix = "BigO__bigo_refl" ]]
lemma bigo_refl [intro]: "f : O(f)"
apply (auto simp add: bigo_def)
-by (metis normalizing.mul_1 order_refl)
+by (metis mult_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 normalizing.mul_0 order_refl)
+by (metis mult_zero_left order_refl)
lemma bigo_zero2: "O(%x.0) = {%x.0}"
apply (auto simp add: bigo_def)
@@ -237,7 +237,7 @@
apply (rule bigo_plus_subset)
apply (simp add: bigo_alt_def set_plus_def func_plus)
apply clarify
-(*sledgehammer*);
+(*sledgehammer*)
apply (rule_tac x = "max c ca" in exI)
apply (rule conjI)
apply (metis Orderings.less_max_iff_disj)
@@ -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 normalizing.semiring_rules(24) diff_add_cancel diff_minus_eq_add le_less order_trans)
+ apply (metis add_right_mono add_commute 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 normalizing.mul_1 order_refl)
+by (metis mult_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 normalizing.mul_1 order_refl)
+by (metis mult_1 order_refl)
lemma bigo_abs3: "O(f) = O(%x. abs(f x))"
proof -
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed May 12 11:17:59 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed May 12 11:18:42 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 normalizing.mul_a using `u<1` by auto
+ unfolding mult_assoc[symmetric] 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 Wed May 12 11:17:59 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Wed May 12 11:18:42 2010 +0200
@@ -698,7 +698,8 @@
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:normalizing.semiring_rules)
+ case False
+ have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2" by(simp add: power2_eq_square)
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 Wed May 12 11:17:59 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed May 12 11:18:42 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 normalizing.semiring_rules, of k c d] note le_less_trans[OF this d(2)]
+ note this[unfolded real_scaleR_def real_norm_def mult_1_right mult_1, 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 normalizing.add_a
+ apply(subst real_sum_of_halves[of e,THEN sym]) unfolding add_assoc[symmetric]
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/Probability/Lebesgue.thy Wed May 12 11:17:59 2010 +0200
+++ b/src/HOL/Probability/Lebesgue.thy Wed May 12 11:18:42 2010 +0200
@@ -939,17 +939,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 normalizing.mul_pwr by auto
+ hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding power_add[symmetric] by auto
have "real (natfloor (f t * 2^m) * natfloor (2^(n-m))) \<le> real (natfloor (f t * 2 ^ n))"
apply (subst *)
- apply (subst normalizing.mul_a)
+ apply (subst mult_assoc[symmetric])
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) normalizing.mul_c)
- apply (subst normalizing.mul_a)
+ apply (subst (3) mult_commute)
+ apply (subst mult_assoc[symmetric])
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)
--- a/src/HOL/Semiring_Normalization.thy Wed May 12 11:17:59 2010 +0200
+++ b/src/HOL/Semiring_Normalization.thy Wed May 12 11:18:42 2010 +0200
@@ -52,286 +52,155 @@
setup Semiring_Normalizer.setup
-locale normalizing_semiring =
- fixes add mul pwr r0 r1
- assumes add_a:"(add x (add y z) = add (add x y) z)"
- and add_c: "add x y = add y x" and add_0:"add r0 x = x"
- and mul_a:"mul x (mul y z) = mul (mul x y) z" and mul_c:"mul x y = mul y x"
- and mul_1:"mul r1 x = x" and mul_0:"mul r0 x = r0"
- and mul_d:"mul x (add y z) = add (mul x y) (mul x z)"
- and pwr_0:"pwr x 0 = r1" and pwr_Suc:"pwr x (Suc n) = mul x (pwr x n)"
-begin
-
-lemma mul_pwr:"mul (pwr x p) (pwr x q) = pwr x (p + q)"
-proof (induct p)
- case 0
- then show ?case by (auto simp add: pwr_0 mul_1)
-next
- case Suc
- from this [symmetric] show ?case
- by (auto simp add: pwr_Suc mul_1 mul_a)
-qed
-
-lemma pwr_mul: "pwr (mul x y) q = mul (pwr x q) (pwr y q)"
-proof (induct q arbitrary: x y, auto simp add:pwr_0 pwr_Suc mul_1)
- fix q x y
- assume "\<And>x y. pwr (mul x y) q = mul (pwr x q) (pwr y q)"
- have "mul (mul x y) (mul (pwr x q) (pwr y q)) = mul x (mul y (mul (pwr x q) (pwr y q)))"
- by (simp add: mul_a)
- also have "\<dots> = (mul (mul y (mul (pwr y q) (pwr x q))) x)" by (simp add: mul_c)
- also have "\<dots> = (mul (mul y (pwr y q)) (mul (pwr x q) x))" by (simp add: mul_a)
- finally show "mul (mul x y) (mul (pwr x q) (pwr y q)) =
- mul (mul x (pwr x q)) (mul y (pwr y q))" by (simp add: mul_c)
-qed
-
-lemma pwr_pwr: "pwr (pwr x p) q = pwr x (p * q)"
-proof (induct p arbitrary: q)
- case 0
- show ?case using pwr_Suc mul_1 pwr_0 by (induct q) auto
-next
- case Suc
- thus ?case by (auto simp add: mul_pwr [symmetric] pwr_mul pwr_Suc)
-qed
-
-lemma semiring_ops:
- shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)"
- and "TERM r0" and "TERM r1" .
+lemma (in comm_semiring_1) semiring_ops:
+ shows "TERM (x + y)" and "TERM (x * y)" and "TERM (x ^ n)"
+ and "TERM 0" and "TERM 1" .
-lemma semiring_rules:
- "add (mul a m) (mul b m) = mul (add a b) m"
- "add (mul a m) m = mul (add a r1) m"
- "add m (mul a m) = mul (add a r1) m"
- "add m m = mul (add r1 r1) m"
- "add r0 a = a"
- "add a r0 = a"
- "mul a b = mul b a"
- "mul (add a b) c = add (mul a c) (mul b c)"
- "mul r0 a = r0"
- "mul a r0 = r0"
- "mul r1 a = a"
- "mul a r1 = a"
- "mul (mul lx ly) (mul rx ry) = mul (mul lx rx) (mul ly ry)"
- "mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry))"
- "mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry)"
- "mul (mul lx ly) rx = mul (mul lx rx) ly"
- "mul (mul lx ly) rx = mul lx (mul ly rx)"
- "mul lx (mul rx ry) = mul (mul lx rx) ry"
- "mul lx (mul rx ry) = mul rx (mul lx ry)"
- "add (add a b) (add c d) = add (add a c) (add b d)"
- "add (add a b) c = add a (add b c)"
- "add a (add c d) = add c (add a d)"
- "add (add a b) c = add (add a c) b"
- "add a c = add c a"
- "add a (add c d) = add (add a c) d"
- "mul (pwr x p) (pwr x q) = pwr x (p + q)"
- "mul x (pwr x q) = pwr x (Suc q)"
- "mul (pwr x q) x = pwr x (Suc q)"
- "mul x x = pwr x 2"
- "pwr (mul x y) q = mul (pwr x q) (pwr y q)"
- "pwr (pwr x p) q = pwr x (p * q)"
- "pwr x 0 = r1"
- "pwr x 1 = x"
- "mul x (add y z) = add (mul x y) (mul x z)"
- "pwr x (Suc q) = mul x (pwr x q)"
- "pwr x (2*n) = mul (pwr x n) (pwr x n)"
- "pwr x (Suc (2*n)) = mul x (mul (pwr x n) (pwr x n))"
-proof -
- show "add (mul a m) (mul b m) = mul (add a b) m" using mul_d mul_c by simp
-next show"add (mul a m) m = mul (add a r1) m" using mul_d mul_c mul_1 by simp
-next show "add m (mul a m) = mul (add a r1) m" using mul_c mul_d mul_1 add_c by simp
-next show "add m m = mul (add r1 r1) m" using mul_c mul_d mul_1 by simp
-next show "add r0 a = a" using add_0 by simp
-next show "add a r0 = a" using add_0 add_c by simp
-next show "mul a b = mul b a" using mul_c by simp
-next show "mul (add a b) c = add (mul a c) (mul b c)" using mul_c mul_d by simp
-next show "mul r0 a = r0" using mul_0 by simp
-next show "mul a r0 = r0" using mul_0 mul_c by simp
-next show "mul r1 a = a" using mul_1 by simp
-next show "mul a r1 = a" using mul_1 mul_c by simp
-next show "mul (mul lx ly) (mul rx ry) = mul (mul lx rx) (mul ly ry)"
- using mul_c mul_a by simp
-next show "mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry))"
- using mul_a by simp
-next
- have "mul (mul lx ly) (mul rx ry) = mul (mul rx ry) (mul lx ly)" by (rule mul_c)
- also have "\<dots> = mul rx (mul ry (mul lx ly))" using mul_a by simp
- finally
- show "mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry)"
- using mul_c by simp
-next show "mul (mul lx ly) rx = mul (mul lx rx) ly" using mul_c mul_a by simp
-next
- show "mul (mul lx ly) rx = mul lx (mul ly rx)" by (simp add: mul_a)
-next show "mul lx (mul rx ry) = mul (mul lx rx) ry" by (simp add: mul_a )
-next show "mul lx (mul rx ry) = mul rx (mul lx ry)" by (simp add: mul_a,simp add: mul_c)
-next show "add (add a b) (add c d) = add (add a c) (add b d)"
- using add_c add_a by simp
-next show "add (add a b) c = add a (add b c)" using add_a by simp
-next show "add a (add c d) = add c (add a d)"
- apply (simp add: add_a) by (simp only: add_c)
-next show "add (add a b) c = add (add a c) b" using add_a add_c by simp
-next show "add a c = add c a" by (rule add_c)
-next show "add a (add c d) = add (add a c) d" using add_a by simp
-next show "mul (pwr x p) (pwr x q) = pwr x (p + q)" by (rule mul_pwr)
-next show "mul x (pwr x q) = pwr x (Suc q)" using pwr_Suc by simp
-next show "mul (pwr x q) x = pwr x (Suc q)" using pwr_Suc mul_c by simp
-next show "mul x x = pwr x 2" by (simp add: nat_number' pwr_Suc pwr_0 mul_1 mul_c)
-next show "pwr (mul x y) q = mul (pwr x q) (pwr y q)" by (rule pwr_mul)
-next show "pwr (pwr x p) q = pwr x (p * q)" by (rule pwr_pwr)
-next show "pwr x 0 = r1" using pwr_0 .
-next show "pwr x 1 = x" unfolding One_nat_def by (simp add: nat_number' pwr_Suc pwr_0 mul_1 mul_c)
-next show "mul x (add y z) = add (mul x y) (mul x z)" using mul_d by simp
-next show "pwr x (Suc q) = mul x (pwr x q)" using pwr_Suc by simp
-next show "pwr x (2 * n) = mul (pwr x n) (pwr x n)" by (simp add: nat_number' mul_pwr)
-next show "pwr x (Suc (2 * n)) = mul x (mul (pwr x n) (pwr x n))"
- by (simp add: nat_number' pwr_Suc mul_pwr)
-qed
-
-end
-
-sublocale comm_semiring_1
- < normalizing!: normalizing_semiring plus times power zero one
-proof
-qed (simp_all add: algebra_simps)
+lemma (in comm_semiring_1) semiring_rules:
+ "(a * m) + (b * m) = (a + b) * m"
+ "(a * m) + m = (a + 1) * m"
+ "m + (a * m) = (a + 1) * m"
+ "m + m = (1 + 1) * m"
+ "0 + a = a"
+ "a + 0 = a"
+ "a * b = b * a"
+ "(a + b) * c = (a * c) + (b * c)"
+ "0 * a = 0"
+ "a * 0 = 0"
+ "1 * a = a"
+ "a * 1 = a"
+ "(lx * ly) * (rx * ry) = (lx * rx) * (ly * ry)"
+ "(lx * ly) * (rx * ry) = lx * (ly * (rx * ry))"
+ "(lx * ly) * (rx * ry) = rx * ((lx * ly) * ry)"
+ "(lx * ly) * rx = (lx * rx) * ly"
+ "(lx * ly) * rx = lx * (ly * rx)"
+ "lx * (rx * ry) = (lx * rx) * ry"
+ "lx * (rx * ry) = rx * (lx * ry)"
+ "(a + b) + (c + d) = (a + c) + (b + d)"
+ "(a + b) + c = a + (b + c)"
+ "a + (c + d) = c + (a + d)"
+ "(a + b) + c = (a + c) + b"
+ "a + c = c + a"
+ "a + (c + d) = (a + c) + d"
+ "(x ^ p) * (x ^ q) = x ^ (p + q)"
+ "x * (x ^ q) = x ^ (Suc q)"
+ "(x ^ q) * x = x ^ (Suc q)"
+ "x * x = x ^ 2"
+ "(x * y) ^ q = (x ^ q) * (y ^ q)"
+ "(x ^ p) ^ q = x ^ (p * q)"
+ "x ^ 0 = 1"
+ "x ^ 1 = x"
+ "x * (y + z) = (x * y) + (x * z)"
+ "x ^ (Suc q) = x * (x ^ q)"
+ "x ^ (2*n) = (x ^ n) * (x ^ n)"
+ "x ^ (Suc (2*n)) = x * ((x ^ n) * (x ^ n))"
+ by (simp_all add: algebra_simps power_add power2_eq_square power_mult_distrib power_mult)
lemmas (in comm_semiring_1) normalizing_comm_semiring_1_axioms =
comm_semiring_1_axioms [normalizer
- semiring ops: normalizing.semiring_ops
- semiring rules: normalizing.semiring_rules]
+ semiring ops: semiring_ops
+ semiring rules: semiring_rules]
declaration (in comm_semiring_1)
{* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_axioms} *}
-locale normalizing_ring = normalizing_semiring +
- fixes sub :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
- and neg :: "'a \<Rightarrow> 'a"
- assumes neg_mul: "neg x = mul (neg r1) x"
- and sub_add: "sub x y = add x (neg y)"
-begin
-
-lemma ring_ops: shows "TERM (sub x y)" and "TERM (neg x)" .
+lemma (in comm_ring_1) ring_ops: shows "TERM (x- y)" and "TERM (- x)" .
-lemmas ring_rules = neg_mul sub_add
-
-end
-
-sublocale comm_ring_1
- < normalizing!: normalizing_ring plus times power zero one minus uminus
-proof
-qed (simp_all add: diff_minus)
+lemma (in comm_ring_1) ring_rules:
+ "- x = (- 1) * x"
+ "x - y = x + (- y)"
+ by (simp_all add: diff_minus)
lemmas (in comm_ring_1) normalizing_comm_ring_1_axioms =
comm_ring_1_axioms [normalizer
- semiring ops: normalizing.semiring_ops
- semiring rules: normalizing.semiring_rules
- ring ops: normalizing.ring_ops
- ring rules: normalizing.ring_rules]
+ semiring ops: semiring_ops
+ semiring rules: semiring_rules
+ ring ops: ring_ops
+ ring rules: ring_rules]
declaration (in comm_ring_1)
{* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_ring_1_axioms} *}
-locale normalizing_semiring_cancel = normalizing_semiring +
- assumes add_cancel: "add (x::'a) y = add x z \<longleftrightarrow> y = z"
- and add_mul_solve: "add (mul w y) (mul x z) =
- add (mul w z) (mul x y) \<longleftrightarrow> w = x \<or> y = z"
-begin
-
-lemma noteq_reduce: "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> add (mul a c) (mul b d) \<noteq> add (mul a d) (mul b c)"
+lemma (in comm_semiring_1_cancel_norm) noteq_reduce:
+ "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> (a * c) + (b * d) \<noteq> (a * d) + (b * c)"
proof-
have "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> \<not> (a = b \<or> c = d)" by simp
- also have "\<dots> \<longleftrightarrow> add (mul a c) (mul b d) \<noteq> add (mul a d) (mul b c)"
- using add_mul_solve by blast
- finally show "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> add (mul a c) (mul b d) \<noteq> add (mul a d) (mul b c)"
+ also have "\<dots> \<longleftrightarrow> (a * c) + (b * d) \<noteq> (a * d) + (b * c)"
+ using add_mult_solve by blast
+ finally show "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> (a * c) + (b * d) \<noteq> (a * d) + (b * c)"
by simp
qed
-lemma add_scale_eq_noteq: "\<lbrakk>r \<noteq> r0 ; (a = b) \<and> ~(c = d)\<rbrakk>
- \<Longrightarrow> add a (mul r c) \<noteq> add b (mul r d)"
+lemma (in comm_semiring_1_cancel_norm) add_scale_eq_noteq:
+ "\<lbrakk>r \<noteq> 0 ; a = b \<and> c \<noteq> d\<rbrakk> \<Longrightarrow> a + (r * c) \<noteq> b + (r * d)"
proof(clarify)
- assume nz: "r\<noteq> r0" and cnd: "c\<noteq>d"
- and eq: "add b (mul r c) = add b (mul r d)"
- hence "mul r c = mul r d" using cnd add_cancel by simp
- hence "add (mul r0 d) (mul r c) = add (mul r0 c) (mul r d)"
- using mul_0 add_cancel by simp
- thus "False" using add_mul_solve nz cnd by simp
+ assume nz: "r\<noteq> 0" and cnd: "c\<noteq>d"
+ and eq: "b + (r * c) = b + (r * d)"
+ have "(0 * d) + (r * c) = (0 * c) + (r * d)"
+ using add_imp_eq eq mult_zero_left by simp
+ thus "False" using add_mult_solve[of 0 d] nz cnd by simp
qed
-lemma add_r0_iff: " x = add x a \<longleftrightarrow> a = r0"
+lemma (in comm_semiring_1_cancel_norm) add_0_iff:
+ "x = x + a \<longleftrightarrow> a = 0"
proof-
- have "a = r0 \<longleftrightarrow> add x a = add x r0" by (simp add: add_cancel)
- thus "x = add x a \<longleftrightarrow> a = r0" by (auto simp add: add_c add_0)
+ have "a = 0 \<longleftrightarrow> x + a = x + 0" using add_imp_eq[of x a 0] by auto
+ thus "x = x + a \<longleftrightarrow> a = 0" by (auto simp add: add_commute)
qed
-end
-
-sublocale comm_semiring_1_cancel_norm
- < normalizing!: normalizing_semiring_cancel plus times power zero one
-proof
-qed (simp_all add: add_mult_solve)
-
declare (in comm_semiring_1_cancel_norm)
normalizing_comm_semiring_1_axioms [normalizer del]
lemmas (in comm_semiring_1_cancel_norm)
normalizing_comm_semiring_1_cancel_norm_axioms =
comm_semiring_1_cancel_norm_axioms [normalizer
- semiring ops: normalizing.semiring_ops
- semiring rules: normalizing.semiring_rules
- idom rules: normalizing.noteq_reduce normalizing.add_scale_eq_noteq]
+ semiring ops: semiring_ops
+ semiring rules: semiring_rules
+ idom rules: noteq_reduce add_scale_eq_noteq]
declaration (in comm_semiring_1_cancel_norm)
{* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_cancel_norm_axioms} *}
-locale normalizing_ring_cancel = normalizing_semiring_cancel + normalizing_ring +
- assumes subr0_iff: "sub x y = r0 \<longleftrightarrow> x = y"
-
-sublocale idom
- < normalizing!: normalizing_ring_cancel plus times power zero one minus uminus
-proof
-qed simp
-
declare (in idom) normalizing_comm_ring_1_axioms [normalizer del]
lemmas (in idom) normalizing_idom_axioms = idom_axioms [normalizer
- semiring ops: normalizing.semiring_ops
- semiring rules: normalizing.semiring_rules
- ring ops: normalizing.ring_ops
- ring rules: normalizing.ring_rules
- idom rules: normalizing.noteq_reduce normalizing.add_scale_eq_noteq
- ideal rules: normalizing.subr0_iff normalizing.add_r0_iff]
+ semiring ops: semiring_ops
+ semiring rules: semiring_rules
+ ring ops: ring_ops
+ ring rules: ring_rules
+ idom rules: noteq_reduce add_scale_eq_noteq
+ ideal rules: right_minus_eq add_0_iff]
declaration (in idom)
{* Semiring_Normalizer.semiring_funs @{thm normalizing_idom_axioms} *}
-locale normalizing_field = normalizing_ring_cancel +
- fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
- and inverse:: "'a \<Rightarrow> 'a"
- assumes divide_inverse: "divide x y = mul x (inverse y)"
- and inverse_divide: "inverse x = divide r1 x"
-begin
-
-lemma field_ops: shows "TERM (divide x y)" and "TERM (inverse x)" .
+lemma (in field) field_ops:
+ shows "TERM (x / y)" and "TERM (inverse x)" .
-lemmas field_rules = divide_inverse inverse_divide
-
-end
-
-sublocale field
- < normalizing!: normalizing_field plus times power zero one minus uminus divide inverse
-proof
-qed (simp_all add: divide_inverse)
+lemmas (in field) field_rules = divide_inverse inverse_eq_divide
lemmas (in field) normalizing_field_axioms =
field_axioms [normalizer
- semiring ops: normalizing.semiring_ops
- semiring rules: normalizing.semiring_rules
- ring ops: normalizing.ring_ops
- ring rules: normalizing.ring_rules
- field ops: normalizing.field_ops
- field rules: normalizing.field_rules
- idom rules: normalizing.noteq_reduce normalizing.add_scale_eq_noteq
- ideal rules: normalizing.subr0_iff normalizing.add_r0_iff]
+ semiring ops: semiring_ops
+ semiring rules: semiring_rules
+ ring ops: ring_ops
+ ring rules: ring_rules
+ field ops: field_ops
+ field rules: field_rules
+ idom rules: noteq_reduce add_scale_eq_noteq
+ ideal rules: right_minus_eq add_0_iff]
declaration (in field)
{* Semiring_Normalizer.field_funs @{thm normalizing_field_axioms} *}
+hide_fact (open) normalizing_comm_semiring_1_axioms
+ normalizing_comm_semiring_1_cancel_norm_axioms semiring_ops semiring_rules
+
+hide_fact (open) normalizing_comm_ring_1_axioms
+ normalizing_idom_axioms ring_ops ring_rules
+
+hide_fact (open) normalizing_field_axioms field_ops field_rules
+
+hide_fact (open) add_scale_eq_noteq noteq_reduce
+
end
--- a/src/HOL/SetInterval.thy Wed May 12 11:17:59 2010 +0200
+++ b/src/HOL/SetInterval.thy Wed May 12 11:18:42 2010 +0200
@@ -231,6 +231,8 @@
lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}"
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
+lemma atLeastAtMost_singleton': "a = b \<Longrightarrow> {a .. b} = {a}" by simp
+
lemma atLeastatMost_subset_iff[simp]:
"{a..b} <= {c..d} \<longleftrightarrow> (~ a <= b) | c <= a & b <= d"
unfolding atLeastAtMost_def atLeast_def atMost_def
@@ -241,6 +243,15 @@
((~ a <= b) | c <= a & b <= d & (c < a | b < d)) & c <= d"
by(simp add: psubset_eq expand_set_eq less_le_not_le)(blast intro: order_trans)
+lemma atLeastAtMost_singleton_iff[simp]:
+ "{a .. b} = {c} \<longleftrightarrow> a = b \<and> b = c"
+proof
+ assume "{a..b} = {c}"
+ hence "\<not> (\<not> a \<le> b)" unfolding atLeastatMost_empty_iff[symmetric] by simp
+ moreover with `{a..b} = {c}` have "c \<le> a \<and> b \<le> c" by auto
+ ultimately show "a = b \<and> b = c" by auto
+qed simp
+
end
lemma (in linorder) atLeastLessThan_subset_iff:
--- a/src/HOL/ex/HarmonicSeries.thy Wed May 12 11:17:59 2010 +0200
+++ b/src/HOL/ex/HarmonicSeries.thy Wed May 12 11:18:42 2010 +0200
@@ -168,13 +168,7 @@
by simp
also have
"\<dots> = (\<Sum>n\<in>{2::nat..2}. 1/real n) + 1"
- proof -
- have "(2::nat)^0 = 1" by simp
- then have "(2::nat)^0+1 = 2" by simp
- moreover have "(2::nat)^1 = 2" by simp
- ultimately have "{((2::nat)^0)+1..2^1} = {2::nat..2}" by auto
- thus ?thesis by simp
- qed
+ by (auto simp: atLeastAtMost_singleton')
also have
"\<dots> = 1/2 + 1"
by simp