# HG changeset patch # User paulson # Date 1071850408 -3600 # Node ID f17ca9f6dc8c28a8fd359c8f12e210b128545fea # Parent cc0b4bbfbc43ae37eef0684381487cd9933e94e1 tidying first part of HyperArith0.ML, using generic lemmas diff -r cc0b4bbfbc43 -r f17ca9f6dc8c src/HOL/Complex/ex/Sqrt.thy --- a/src/HOL/Complex/ex/Sqrt.thy Fri Dec 19 10:38:48 2003 +0100 +++ b/src/HOL/Complex/ex/Sqrt.thy Fri Dec 19 17:13:28 2003 +0100 @@ -43,7 +43,7 @@ proof - from gcd have "real ?k / real ?l = real (?gcd * ?k) / real (?gcd * ?l)" - by (simp add: real_mult_div_cancel1) + by (simp add: mult_divide_cancel_left) also from gcd_k and gcd_l have "\ = real m / real n" by simp also from x_rat have "\ = \x\" .. finally show ?thesis .. diff -r cc0b4bbfbc43 -r f17ca9f6dc8c src/HOL/Hyperreal/HyperArith0.ML --- a/src/HOL/Hyperreal/HyperArith0.ML Fri Dec 19 10:38:48 2003 +0100 +++ b/src/HOL/Hyperreal/HyperArith0.ML Fri Dec 19 17:13:28 2003 +0100 @@ -8,196 +8,6 @@ Also, common factor cancellation *) -Goal "x - - y = x + (y::hypreal)"; -by (Simp_tac 1); -qed "hypreal_diff_minus_eq"; -Addsimps [hypreal_diff_minus_eq]; - -Goal "((x * y = 0) = (x = 0 | y = (0::hypreal)))"; -by Auto_tac; -qed "hypreal_mult_is_0"; -AddIffs [hypreal_mult_is_0]; - -(** Division and inverse **) - -Goal "0/x = (0::hypreal)"; -by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1); -qed "hypreal_0_divide"; -Addsimps [hypreal_0_divide]; - -Goal "((0::hypreal) < inverse x) = (0 < x)"; -by (case_tac "x=0" 1); -by (asm_simp_tac (HOL_ss addsimps [HYPREAL_INVERSE_ZERO]) 1); -by (auto_tac (claset() addDs [hypreal_inverse_less_0], - simpset() addsimps [linorder_neq_iff, - hypreal_inverse_gt_0])); -qed "hypreal_0_less_inverse_iff"; -Addsimps [hypreal_0_less_inverse_iff]; - -Goal "(inverse x < (0::hypreal)) = (x < 0)"; -by (case_tac "x=0" 1); -by (asm_simp_tac (HOL_ss addsimps [HYPREAL_INVERSE_ZERO]) 1); -by (auto_tac (claset() addDs [hypreal_inverse_less_0], - simpset() addsimps [linorder_neq_iff, - hypreal_inverse_gt_0])); -qed "hypreal_inverse_less_0_iff"; -Addsimps [hypreal_inverse_less_0_iff]; - -Goal "((0::hypreal) <= inverse x) = (0 <= x)"; -by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); -qed "hypreal_0_le_inverse_iff"; -Addsimps [hypreal_0_le_inverse_iff]; - -Goal "(inverse x <= (0::hypreal)) = (x <= 0)"; -by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); -qed "hypreal_inverse_le_0_iff"; -Addsimps [hypreal_inverse_le_0_iff]; - -Goalw [hypreal_divide_def] "x/(0::hypreal) = 0"; -by (stac (HYPREAL_INVERSE_ZERO) 1); -by (Simp_tac 1); -qed "HYPREAL_DIVIDE_ZERO"; - -Goal "inverse (x::hypreal) = 1/x"; -by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1); -qed "hypreal_inverse_eq_divide"; - -Goal "((0::hypreal) < x/y) = (0 < x & 0 < y | x < 0 & y < 0)"; -by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_0_less_mult_iff]) 1); -qed "hypreal_0_less_divide_iff"; -Addsimps [inst "x" "number_of ?w" hypreal_0_less_divide_iff]; - -Goal "(x/y < (0::hypreal)) = (0 < x & y < 0 | x < 0 & 0 < y)"; -by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_less_0_iff]) 1); -qed "hypreal_divide_less_0_iff"; -Addsimps [inst "x" "number_of ?w" hypreal_divide_less_0_iff]; - -Goal "((0::hypreal) <= x/y) = ((x <= 0 | 0 <= y) & (0 <= x | y <= 0))"; -by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_0_le_mult_iff]) 1); -by Auto_tac; -qed "hypreal_0_le_divide_iff"; -Addsimps [inst "x" "number_of ?w" hypreal_0_le_divide_iff]; - -Goal "(x/y <= (0::hypreal)) = ((x <= 0 | y <= 0) & (0 <= x | 0 <= y))"; -by (simp_tac (simpset() addsimps [hypreal_divide_def, - hypreal_mult_le_0_iff]) 1); -by Auto_tac; -qed "hypreal_divide_le_0_iff"; -Addsimps [inst "x" "number_of ?w" hypreal_divide_le_0_iff]; - -Goal "(inverse(x::hypreal) = 0) = (x = 0)"; -by (auto_tac (claset(), - simpset() addsimps [HYPREAL_INVERSE_ZERO])); -by (rtac ccontr 1); -by (blast_tac (claset() addDs [hypreal_inverse_not_zero]) 1); -qed "hypreal_inverse_zero_iff"; -Addsimps [hypreal_inverse_zero_iff]; - -Goal "(x/y = 0) = (x=0 | y=(0::hypreal))"; -by (auto_tac (claset(), simpset() addsimps [hypreal_divide_def])); -qed "hypreal_divide_eq_0_iff"; -Addsimps [hypreal_divide_eq_0_iff]; - -Goal "h ~= (0::hypreal) ==> h/h = 1"; -by (asm_simp_tac - (simpset() addsimps [hypreal_divide_def, hypreal_mult_inverse_left]) 1); -qed "hypreal_divide_self_eq"; -Addsimps [hypreal_divide_self_eq]; - - -(**** Factor cancellation theorems for "hypreal" ****) - -(** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =, - but not (yet?) for k*m < n*k. **) - -bind_thm ("hypreal_mult_minus_right", hypreal_minus_mult_eq2 RS sym); - -Goal "(-y < -x) = ((x::hypreal) < y)"; -by (arith_tac 1); -qed "hypreal_minus_less_minus"; -Addsimps [hypreal_minus_less_minus]; - -Goal "[| i j*k < i*k"; -by (rtac (hypreal_minus_less_minus RS iffD1) 1); -by (auto_tac (claset(), - simpset() delsimps [hypreal_minus_mult_eq2 RS sym] - addsimps [hypreal_minus_mult_eq2, - hypreal_mult_less_mono1])); -qed "hypreal_mult_less_mono1_neg"; - -Goal "[| i k*j < k*i"; -by (rtac (hypreal_minus_less_minus RS iffD1) 1); -by (auto_tac (claset(), - simpset() delsimps [hypreal_minus_mult_eq1 RS sym] - addsimps [hypreal_minus_mult_eq1, - hypreal_mult_less_mono2])); -qed "hypreal_mult_less_mono2_neg"; - -Goal "[| i <= j; k <= (0::hypreal) |] ==> j*k <= i*k"; -by (auto_tac (claset(), - simpset() addsimps [order_le_less, hypreal_mult_less_mono1_neg])); -qed "hypreal_mult_le_mono1_neg"; - -Goal "[| i <= j; k <= (0::hypreal) |] ==> k*j <= k*i"; -by (dtac hypreal_mult_le_mono1_neg 1); -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute]))); -qed "hypreal_mult_le_mono2_neg"; - -Goal "(m*k < n*k) = (((0::hypreal) < k & m m<=n) & (k < 0 --> n<=m))"; -by (simp_tac (simpset() addsimps [linorder_not_less RS sym, - hypreal_mult_less_cancel2]) 1); -qed "hypreal_mult_le_cancel2"; - -Goal "(k*m < k*n) = (((0::hypreal) < k & m m<=n) & (k < 0 --> n<=m))"; -by (simp_tac (simpset() addsimps [linorder_not_less RS sym, - hypreal_mult_less_cancel1]) 1); -qed "hypreal_mult_le_cancel1"; - -Goal "!!k::hypreal. (k*m = k*n) = (k = 0 | m=n)"; -by (case_tac "k=0" 1); -by (auto_tac (claset(), simpset() addsimps [hypreal_mult_left_cancel])); -qed "hypreal_mult_eq_cancel1"; - -Goal "!!k::hypreal. (m*k = n*k) = (k = 0 | m=n)"; -by (case_tac "k=0" 1); -by (auto_tac (claset(), simpset() addsimps [hypreal_mult_right_cancel])); -qed "hypreal_mult_eq_cancel2"; - -Goal "!!k::hypreal. k~=0 ==> (k*m) / (k*n) = (m/n)"; -by (asm_simp_tac - (simpset() addsimps [hypreal_divide_def, hypreal_inverse_distrib]) 1); -by (subgoal_tac "k * m * (inverse k * inverse n) = \ -\ (k * inverse k) * (m * inverse n)" 1); -by (asm_full_simp_tac (simpset() addsimps []) 1); -by (asm_full_simp_tac (HOL_ss addsimps hypreal_mult_ac) 1); -qed "hypreal_mult_div_cancel1"; - -(*For ExtractCommonTerm*) -Goal "(k*m) / (k*n) = (if k = (0::hypreal) then 0 else m/n)"; -by (simp_tac (simpset() addsimps [hypreal_mult_div_cancel1]) 1); -qed "hypreal_mult_div_cancel_disj"; - - local open Hyperreal_Numeral_Simprocs in @@ -224,7 +34,7 @@ val prove_conv = Bin_Simprocs.prove_conv val mk_bal = HOLogic.mk_binop "HOL.divide" val dest_bal = HOLogic.dest_bin "HOL.divide" hyprealT - val cancel = hypreal_mult_div_cancel1 RS trans + val cancel = mult_divide_cancel_left RS trans val neg_exchanges = false ) @@ -233,7 +43,7 @@ val prove_conv = Bin_Simprocs.prove_conv val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin "op =" hyprealT - val cancel = hypreal_mult_eq_cancel1 RS trans + val cancel = mult_cancel_left RS trans val neg_exchanges = false ) @@ -242,7 +52,7 @@ val prove_conv = Bin_Simprocs.prove_conv val mk_bal = HOLogic.mk_binrel "op <" val dest_bal = HOLogic.dest_bin "op <" hyprealT - val cancel = hypreal_mult_less_cancel1 RS trans + val cancel = mult_less_cancel_left RS trans val neg_exchanges = true ) @@ -251,7 +61,7 @@ val prove_conv = Bin_Simprocs.prove_conv val mk_bal = HOLogic.mk_binrel "op <=" val dest_bal = HOLogic.dest_bin "op <=" hyprealT - val cancel = hypreal_mult_le_cancel1 RS trans + val cancel = mult_le_cancel_left RS trans val neg_exchanges = true ) @@ -341,7 +151,7 @@ val prove_conv = Bin_Simprocs.prove_conv val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin "op =" hyprealT - val simplify_meta_eq = cancel_simplify_meta_eq hypreal_mult_eq_cancel1 + val simplify_meta_eq = cancel_simplify_meta_eq mult_cancel_left ); @@ -350,7 +160,7 @@ val prove_conv = Bin_Simprocs.prove_conv val mk_bal = HOLogic.mk_binop "HOL.divide" val dest_bal = HOLogic.dest_bin "HOL.divide" hyprealT - val simplify_meta_eq = cancel_simplify_meta_eq hypreal_mult_div_cancel_disj + val simplify_meta_eq = cancel_simplify_meta_eq mult_divide_cancel_eq_if ); val hypreal_cancel_factor = @@ -387,119 +197,9 @@ *) -(*** Simplification of inequalities involving literal divisors ***) - -Goal "0 ((x::hypreal) <= y/z) = (x*z <= y)"; -by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1); -by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2); -by (etac ssubst 1); -by (stac hypreal_mult_le_cancel2 1); -by (Asm_simp_tac 1); -qed "pos_hypreal_le_divide_eq"; -Addsimps [inst "z" "number_of ?w" pos_hypreal_le_divide_eq]; - -Goal "z<0 ==> ((x::hypreal) <= y/z) = (y <= x*z)"; -by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1); -by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2); -by (etac ssubst 1); -by (stac hypreal_mult_le_cancel2 1); -by (Asm_simp_tac 1); -qed "neg_hypreal_le_divide_eq"; -Addsimps [inst "z" "number_of ?w" neg_hypreal_le_divide_eq]; - -Goal "0 (y/z <= (x::hypreal)) = (y <= x*z)"; -by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1); -by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2); -by (etac ssubst 1); -by (stac hypreal_mult_le_cancel2 1); -by (Asm_simp_tac 1); -qed "pos_hypreal_divide_le_eq"; -Addsimps [inst "z" "number_of ?w" pos_hypreal_divide_le_eq]; - -Goal "z<0 ==> (y/z <= (x::hypreal)) = (x*z <= y)"; -by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1); -by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2); -by (etac ssubst 1); -by (stac hypreal_mult_le_cancel2 1); -by (Asm_simp_tac 1); -qed "neg_hypreal_divide_le_eq"; -Addsimps [inst "z" "number_of ?w" neg_hypreal_divide_le_eq]; - -Goal "0 ((x::hypreal) < y/z) = (x*z < y)"; -by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1); -by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2); -by (etac ssubst 1); -by (stac hypreal_mult_less_cancel2 1); -by (Asm_simp_tac 1); -qed "pos_hypreal_less_divide_eq"; -Addsimps [inst "z" "number_of ?w" pos_hypreal_less_divide_eq]; - -Goal "z<0 ==> ((x::hypreal) < y/z) = (y < x*z)"; -by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1); -by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2); -by (etac ssubst 1); -by (stac hypreal_mult_less_cancel2 1); -by (Asm_simp_tac 1); -qed "neg_hypreal_less_divide_eq"; -Addsimps [inst "z" "number_of ?w" neg_hypreal_less_divide_eq]; - -Goal "0 (y/z < (x::hypreal)) = (y < x*z)"; -by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1); -by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2); -by (etac ssubst 1); -by (stac hypreal_mult_less_cancel2 1); -by (Asm_simp_tac 1); -qed "pos_hypreal_divide_less_eq"; -Addsimps [inst "z" "number_of ?w" pos_hypreal_divide_less_eq]; - -Goal "z<0 ==> (y/z < (x::hypreal)) = (x*z < y)"; -by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1); -by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2); -by (etac ssubst 1); -by (stac hypreal_mult_less_cancel2 1); -by (Asm_simp_tac 1); -qed "neg_hypreal_divide_less_eq"; -Addsimps [inst "z" "number_of ?w" neg_hypreal_divide_less_eq]; - -Goal "z~=0 ==> ((x::hypreal) = y/z) = (x*z = y)"; -by (subgoal_tac "(x*z = y) = (x*z = (y/z)*z)" 1); -by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2); -by (etac ssubst 1); -by (stac hypreal_mult_eq_cancel2 1); -by (Asm_simp_tac 1); -qed "hypreal_eq_divide_eq"; -Addsimps [inst "z" "number_of ?w" hypreal_eq_divide_eq]; - -Goal "z~=0 ==> (y/z = (x::hypreal)) = (y = x*z)"; -by (subgoal_tac "(y = x*z) = ((y/z)*z = x*z)" 1); -by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2); -by (etac ssubst 1); -by (stac hypreal_mult_eq_cancel2 1); -by (Asm_simp_tac 1); -qed "hypreal_divide_eq_eq"; -Addsimps [inst "z" "number_of ?w" hypreal_divide_eq_eq]; - -Goal "(m/k = n/k) = (k = 0 | m = (n::hypreal))"; -by (case_tac "k=0" 1); -by (asm_simp_tac (simpset() addsimps [HYPREAL_DIVIDE_ZERO]) 1); -by (asm_simp_tac (simpset() addsimps [hypreal_divide_eq_eq, hypreal_eq_divide_eq, - hypreal_mult_eq_cancel2]) 1); -qed "hypreal_divide_eq_cancel2"; - -Goal "(k/m = k/n) = (k = 0 | m = (n::hypreal))"; -by (case_tac "m=0 | n = 0" 1); -by (auto_tac (claset(), - simpset() addsimps [HYPREAL_DIVIDE_ZERO, hypreal_divide_eq_eq, - hypreal_eq_divide_eq, hypreal_mult_eq_cancel1])); -qed "hypreal_divide_eq_cancel1"; (** Division by 1, -1 **) -Goal "(x::hypreal)/1 = x"; -by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1); -qed "hypreal_divide_1"; -Addsimps [hypreal_divide_1]; - Goal "x/-1 = -(x::hypreal)"; by (Simp_tac 1); qed "hypreal_divide_minus1"; @@ -510,11 +210,6 @@ qed "hypreal_minus1_divide"; Addsimps [hypreal_minus1_divide]; -Goal "[| (0::hypreal) < d1; 0 < d2 |] ==> EX e. 0 < e & e < d1 & e < d2"; -by (res_inst_tac [("x","(min d1 d2)/2")] exI 1); -by (asm_simp_tac (simpset() addsimps [min_def]) 1); -qed "hypreal_lbound_gt_zero"; - (*** General rewrites to improve automation, like those for type "int" ***) @@ -561,21 +256,6 @@ Addsimps [hypreal_le_minus_iff]; -(*Distributive laws for literals*) -Addsimps (map (inst "w" "number_of ?v") - [hypreal_add_mult_distrib, hypreal_add_mult_distrib2, - hypreal_diff_mult_distrib, hypreal_diff_mult_distrib2]); - -Addsimps (map (inst "x" "number_of ?v") - [hypreal_less_minus, hypreal_le_minus, hypreal_equation_minus]); -Addsimps (map (inst "y" "number_of ?v") - [hypreal_minus_less, hypreal_minus_le, hypreal_minus_equation]); - -Addsimps (map (simplify (simpset()) o inst "x" "1") - [hypreal_less_minus, hypreal_le_minus, hypreal_equation_minus]); -Addsimps (map (simplify (simpset()) o inst "y" "1") - [hypreal_minus_less, hypreal_minus_le, hypreal_minus_equation]); - (*** Simprules combining x+y and 0 ***) Goal "(x+y = (0::hypreal)) = (y = -x)"; @@ -629,21 +309,3 @@ qed "hypreal_minus_diff_eq"; Addsimps [hypreal_minus_diff_eq]; - -(*** Density of the Hyperreals ***) - -Goal "x < y ==> x < (x+y) / (2::hypreal)"; -by Auto_tac; -qed "hypreal_less_half_sum"; - -Goal "x < y ==> (x+y)/(2::hypreal) < y"; -by Auto_tac; -qed "hypreal_gt_half_sum"; - -Goal "x < y ==> EX r::hypreal. x < r & r < y"; -by (blast_tac (claset() addSIs [hypreal_less_half_sum, hypreal_gt_half_sum]) 1); -qed "hypreal_dense"; - - -(*Replaces "inverse #nn" by 1/#nn *) -Addsimps [inst "x" "number_of ?w" hypreal_inverse_eq_divide]; diff -r cc0b4bbfbc43 -r f17ca9f6dc8c src/HOL/Hyperreal/HyperDef.thy --- a/src/HOL/Hyperreal/HyperDef.thy Fri Dec 19 10:38:48 2003 +0100 +++ b/src/HOL/Hyperreal/HyperDef.thy Fri Dec 19 17:13:28 2003 +0100 @@ -990,13 +990,6 @@ by (simp add: hypreal_divide_def) declare hypreal_zero_divide [simp] hypreal_divide_one [simp] -lemma hypreal_times_divide1_eq [simp]: "(x::hypreal) * (y/z) = (x*y)/z" -by (simp add: hypreal_divide_def hypreal_mult_assoc) - -lemma hypreal_times_divide2_eq [simp]: "(y/z) * (x::hypreal) = (y*x)/z" -by (simp add: hypreal_divide_def hypreal_mult_ac) - - lemma hypreal_divide_divide1_eq [simp]: "(x::hypreal) / (y/z) = (x*z)/y" by (simp add: hypreal_divide_def hypreal_inverse_distrib hypreal_mult_ac) @@ -1296,8 +1289,6 @@ val hypreal_of_real_divide = thm "hypreal_of_real_divide"; val hypreal_zero_divide = thm "hypreal_zero_divide"; val hypreal_divide_one = thm "hypreal_divide_one"; -val hypreal_times_divide1_eq = thm "hypreal_times_divide1_eq"; -val hypreal_times_divide2_eq = thm "hypreal_times_divide2_eq"; val hypreal_divide_divide1_eq = thm "hypreal_divide_divide1_eq"; val hypreal_divide_divide2_eq = thm "hypreal_divide_divide2_eq"; val hypreal_minus_divide_eq = thm "hypreal_minus_divide_eq"; diff -r cc0b4bbfbc43 -r f17ca9f6dc8c src/HOL/Hyperreal/HyperOrd.thy --- a/src/HOL/Hyperreal/HyperOrd.thy Fri Dec 19 10:38:48 2003 +0100 +++ b/src/HOL/Hyperreal/HyperOrd.thy Fri Dec 19 17:13:28 2003 +0100 @@ -7,6 +7,14 @@ theory HyperOrd = HyperDef: +instance hypreal :: division_by_zero +proof + fix x :: hypreal + show "inverse 0 = (0::hypreal)" by (rule HYPREAL_INVERSE_ZERO) + show "x/0 = 0" by (rule HYPREAL_DIVISION_BY_ZERO) +qed + + defs (overloaded) hrabs_def: "abs (r::hypreal) == (if 0 \ r then r else -r)" @@ -247,17 +255,6 @@ done declare hypreal_le_square [simp] -lemma hypreal_less_minus_square: "- (x*x) \ (0::hypreal)" -apply (unfold hypreal_le_def) -apply (auto dest!: hypreal_le_square [THEN order_le_less_trans] - simp add: hypreal_minus_zero_less_iff) -done -declare hypreal_less_minus_square [simp] - -lemma hypreal_mult_0_less: "(0*x x*z < y*z" apply (rotate_tac 1) apply (drule hypreal_less_minus_iff [THEN iffD1]) @@ -449,8 +446,6 @@ val hypreal_le_add_right_cancel = thm"hypreal_le_add_right_cancel"; val hypreal_le_add_left_cancel = thm"hypreal_le_add_left_cancel"; val hypreal_le_square = thm"hypreal_le_square"; -val hypreal_less_minus_square = thm"hypreal_less_minus_square"; -val hypreal_mult_0_less = thm"hypreal_mult_0_less"; val hypreal_mult_less_mono1 = thm"hypreal_mult_less_mono1"; val hypreal_mult_less_mono2 = thm"hypreal_mult_less_mono2"; val hypreal_mult_less_mono = thm"hypreal_mult_less_mono"; diff -r cc0b4bbfbc43 -r f17ca9f6dc8c src/HOL/Hyperreal/HyperPow.ML --- a/src/HOL/Hyperreal/HyperPow.ML Fri Dec 19 10:38:48 2003 +0100 +++ b/src/HOL/Hyperreal/HyperPow.ML Fri Dec 19 17:13:28 2003 +0100 @@ -19,8 +19,6 @@ Goal "r ~= (0::hypreal) --> inverse(r ^ n) = (inverse r) ^ n"; by (induct_tac "n" 1); by Auto_tac; -by (forw_inst_tac [("n","n")] hrealpow_not_zero 1); -by (auto_tac (claset(), simpset() addsimps [hypreal_inverse_distrib])); qed_spec_mp "hrealpow_inverse"; Goal "abs (r::hypreal) ^ n = abs (r ^ n)"; @@ -105,13 +103,10 @@ by (auto_tac (claset() addIs [order_antisym], simpset())); qed "hypreal_add_nonneg_eq_0_iff"; -Goal "(x*y = 0) = (x = 0 | y = (0::hypreal))"; -by Auto_tac; -qed "hypreal_mult_is_0"; - Goal "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))"; by (simp_tac (HOL_ss addsimps [hypreal_le_square, hypreal_le_add_order, - hypreal_add_nonneg_eq_0_iff, hypreal_mult_is_0]) 1); + hypreal_add_nonneg_eq_0_iff]) 1); +by Auto_tac; qed "hypreal_three_squares_add_zero_iff"; Goal "(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) = (x = 0 & y = 0 & z = 0)"; diff -r cc0b4bbfbc43 -r f17ca9f6dc8c src/HOL/Hyperreal/Integration.ML --- a/src/HOL/Hyperreal/Integration.ML Fri Dec 19 10:38:48 2003 +0100 +++ b/src/HOL/Hyperreal/Integration.ML Fri Dec 19 17:13:28 2003 +0100 @@ -356,8 +356,9 @@ "abs((rsum(D,p) f - k2) - (rsum(D,p) f - k1)) < abs(k1 - k2)" 1); by (arith_tac 1); by (dtac real_add_less_mono 1 THEN assume_tac 1); -by (auto_tac (claset(),HOL_ss addsimps [real_add_mult_distrib RS sym, - real_mult_2_right RS sym,real_mult_less_cancel2])); +by (auto_tac (claset(), + HOL_ss addsimps [real_add_mult_distrib RS sym, + real_mult_2_right RS sym, mult_less_cancel_right])); by (ALLGOALS(arith_tac)); qed "Integral_unique"; diff -r cc0b4bbfbc43 -r f17ca9f6dc8c src/HOL/Hyperreal/Lim.ML --- a/src/HOL/Hyperreal/Lim.ML Fri Dec 19 10:38:48 2003 +0100 +++ b/src/HOL/Hyperreal/Lim.ML Fri Dec 19 17:13:28 2003 +0100 @@ -7,6 +7,9 @@ val times_divide_eq_right = thm"times_divide_eq_right"; +val inverse_mult_distrib = thm"inverse_mult_distrib"; +val inverse_minus_eq = thm "inverse_minus_eq"; + fun ARITH_PROVE str = prove_goal thy str (fn prems => [cut_facts_tac prems 1,arith_tac 1]); @@ -1020,8 +1023,8 @@ by (simp_tac (simpset() addsimps [hypreal_add_divide_distrib]) 1); by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1)); by (auto_tac (claset(), - simpset() delsimps [hypreal_times_divide1_eq] - addsimps [hypreal_times_divide1_eq RS sym])); + simpset() delsimps [times_divide_eq_right] + addsimps [times_divide_eq_right RS sym])); by (dres_inst_tac [("D","Db")] lemma_nsderiv2 1); by (dtac (approx_minus_iff RS iffD2 RS (bex_Infinitesimal_iff2 RS iffD2)) 4); by (auto_tac (claset() addSIs [approx_add_mono1], @@ -1136,8 +1139,8 @@ by (thin_tac "(( *f* f) (hypreal_of_real(x) + h) + \ \ - hypreal_of_real (f x)) / h = hypreal_of_real(D) + y" 2); by (assume_tac 1); -by (asm_full_simp_tac (simpset() addsimps [hypreal_times_divide1_eq RS sym] - delsimps [hypreal_times_divide1_eq]) 1); +by (asm_full_simp_tac (simpset() addsimps [times_divide_eq_right RS sym] + delsimps [times_divide_eq_right]) 1); by (auto_tac (claset(), simpset() addsimps [hypreal_add_mult_distrib])); qed "increment_thm"; @@ -1324,7 +1327,8 @@ (simpset() addsimps [hypreal_inverse_add, hypreal_inverse_distrib RS sym, hypreal_minus_inverse RS sym] @ hypreal_add_ac @ hypreal_mult_ac - delsimps [hypreal_minus_mult_eq1 RS sym, + delsimps [inverse_mult_distrib,inverse_minus_eq, + hypreal_minus_mult_eq1 RS sym, hypreal_minus_mult_eq2 RS sym] ) 1); by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym, hypreal_add_mult_distrib2] @@ -1818,7 +1822,7 @@ by (REPEAT(dres_inst_tac [("x","a")] spec 1)); by (Asm_full_simp_tac 1); by (asm_full_simp_tac - (simpset() addsimps [real_inverse_eq_divide, pos_real_divide_le_eq]) 1); + (simpset() addsimps [inverse_eq_divide, pos_real_divide_le_eq]) 1); by (cut_inst_tac [("x","k"),("y","M-f a")] real_0_less_mult_iff 1); by (Asm_full_simp_tac 1); (*last one*) @@ -1880,7 +1884,7 @@ by (asm_full_simp_tac (simpset() addsimps [real_0_less_mult_iff]) 2); by (dres_inst_tac [("x","h")] spec 1); by (asm_full_simp_tac - (simpset() addsimps [real_abs_def, real_inverse_eq_divide, + (simpset() addsimps [real_abs_def, inverse_eq_divide, pos_real_le_divide_eq, pos_real_less_divide_eq] addsplits [split_if_asm]) 1); qed "DERIV_left_inc"; @@ -1894,7 +1898,7 @@ by (asm_full_simp_tac (simpset() addsimps [real_mult_less_0_iff]) 2); by (dres_inst_tac [("x","-h")] spec 1); by (asm_full_simp_tac - (simpset() addsimps [real_abs_def, real_inverse_eq_divide, + (simpset() addsimps [real_abs_def, inverse_eq_divide, pos_real_less_divide_eq, symmetric real_diff_def] addsplits [split_if_asm] @@ -2165,7 +2169,7 @@ by (dtac ((real_not_refl2 RS not_sym) RS DERIV_const_ratio_const2) 2 THEN assume_tac 2); by (ALLGOALS (dres_inst_tac [("f","%u. (b-a)*u")] arg_cong)); -by (auto_tac (claset(), simpset() addsimps [real_inverse_eq_divide])); +by (auto_tac (claset(), simpset() addsimps [inverse_eq_divide])); by (asm_full_simp_tac (simpset() addsimps [real_add_commute, eq_commute]) 1); qed "DERIV_const_average"; diff -r cc0b4bbfbc43 -r f17ca9f6dc8c src/HOL/Hyperreal/Log.ML --- a/src/HOL/Hyperreal/Log.ML Fri Dec 19 10:38:48 2003 +0100 +++ b/src/HOL/Hyperreal/Log.ML Fri Dec 19 17:13:28 2003 +0100 @@ -74,7 +74,7 @@ Goalw [powr_def] "[| x powr a < x powr b; 1 < x |] ==> a < b"; by (auto_tac (claset() addDs [ln_gt_zero], - simpset() addsimps [rename_numerals real_mult_less_cancel2])); + simpset() addsimps [mult_less_cancel_right])); qed "powr_less_cancel"; Goal "1 < x ==> (x powr a < x powr b) = (a < b)"; diff -r cc0b4bbfbc43 -r f17ca9f6dc8c src/HOL/Hyperreal/NSA.ML --- a/src/HOL/Hyperreal/NSA.ML Fri Dec 19 10:38:48 2003 +0100 +++ b/src/HOL/Hyperreal/NSA.ML Fri Dec 19 17:13:28 2003 +0100 @@ -330,11 +330,11 @@ by (ftac hrabs_less_gt_zero 1); by (dres_inst_tac [("x","r/t")] bspec 1); by (blast_tac (claset() addIs [SReal_divide]) 1); -by (asm_full_simp_tac (simpset() addsimps [hypreal_0_less_divide_iff]) 1); +by (asm_full_simp_tac (simpset() addsimps [thm"Ring_and_Field.zero_less_divide_iff"]) 1); by (case_tac "x=0 | y=0" 1); by (cut_inst_tac [("u","abs x"),("v","r/t"),("x","abs y")] hypreal_mult_less_mono 2); -by (auto_tac (claset(), simpset() addsimps [hypreal_0_less_divide_iff])); +by (auto_tac (claset(), simpset() addsimps [thm"Ring_and_Field.zero_less_divide_iff"])); qed "Infinitesimal_HFinite_mult"; Goal "[| x : Infinitesimal; y : HFinite |] ==> (y * x) : Infinitesimal"; @@ -347,7 +347,6 @@ "x: HInfinite ==> inverse x: Infinitesimal"; by Auto_tac; by (eres_inst_tac [("x","inverse r")] ballE 1); -by (stac hrabs_inverse 1); by (forw_inst_tac [("x1","r"),("z","abs x")] (hypreal_inverse_gt_0 RS order_less_trans) 1); by (assume_tac 1); @@ -2212,7 +2211,7 @@ Goal "0 < u ==> \ \ (u < inverse (real(Suc n))) = (real(Suc n) < inverse u)"; -by (asm_full_simp_tac (simpset() addsimps [real_inverse_eq_divide]) 1); +by (asm_full_simp_tac (simpset() addsimps [inverse_eq_divide]) 1); by (stac pos_real_less_divide_eq 1); by (assume_tac 1); by (stac pos_real_less_divide_eq 1); @@ -2235,7 +2234,7 @@ Goal "(inverse (real(Suc n)) <= r) = (1 <= r * real(Suc n))"; by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); -by (simp_tac (simpset() addsimps [real_inverse_eq_divide]) 1); +by (simp_tac (simpset() addsimps [inverse_eq_divide]) 1); by (stac pos_real_less_divide_eq 1); by (simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero]) 1); by (simp_tac (simpset() addsimps [real_mult_commute]) 1); diff -r cc0b4bbfbc43 -r f17ca9f6dc8c src/HOL/Hyperreal/SEQ.ML --- a/src/HOL/Hyperreal/SEQ.ML Fri Dec 19 10:38:48 2003 +0100 +++ b/src/HOL/Hyperreal/SEQ.ML Fri Dec 19 17:13:28 2003 +0100 @@ -1270,7 +1270,7 @@ ([LIMSEQ_const, LIMSEQ_realpow_zero] MRS LIMSEQ_mult) 1); by (auto_tac (claset(), simpset() addsimps [real_divide_def, realpow_inverse])); -by (asm_simp_tac (simpset() addsimps [real_inverse_eq_divide, +by (asm_simp_tac (simpset() addsimps [inverse_eq_divide, pos_real_divide_less_eq]) 1); qed "LIMSEQ_divide_realpow_zero"; diff -r cc0b4bbfbc43 -r f17ca9f6dc8c src/HOL/Hyperreal/Transcendental.ML --- a/src/HOL/Hyperreal/Transcendental.ML Fri Dec 19 10:38:48 2003 +0100 +++ b/src/HOL/Hyperreal/Transcendental.ML Fri Dec 19 17:13:28 2003 +0100 @@ -456,7 +456,7 @@ by (res_inst_tac [("x","0")] exI 1 THEN Step_tac 1); by (subgoal_tac "0 < abs (x ^ n)" 1); by (res_inst_tac [("z","abs (x ^ n)")] (CLAIM_SIMP - "[| (0::real) x<=y" [real_mult_le_cancel1]) 1); + "[| (0::real) x<=y" [mult_le_cancel_left]) 1); by (auto_tac (claset(), simpset() addsimps [real_mult_assoc,realpow_abs])); by (dres_inst_tac [("x","0")] spec 2 THEN Force_tac 2); @@ -481,7 +481,7 @@ simpset() addsimps [realpow_abs,real_divide_eq_inverse RS sym])); by (res_inst_tac [("z","abs(x)")] (CLAIM_SIMP - "[|(0::real) x x x<=y" [real_mult_le_cancel1]) 2); + "[| (0::real) x<=y" [mult_le_cancel_left]) 2); by (auto_tac (claset() addIs [abs_ge_zero RS real_le_trans],simpset())); by (dtac real_le_imp_less_or_eq 1); by Auto_tac; @@ -639,7 +639,7 @@ by (res_inst_tac [("y","K * abs x")] order_le_less_trans 1); by (res_inst_tac [("R2.0","K * e")] real_less_trans 2); by (res_inst_tac [("z","inverse K")] (CLAIM_SIMP - "[|(0::real) x x x * y ~= (0::real)" by simp -lemma real_inverse_eq_divide: "inverse (x::real) = 1/x" - by (rule Ring_and_Field.inverse_eq_divide) - lemma real_inverse_inverse: "inverse(inverse (x::real)) = x" by (rule Ring_and_Field.inverse_inverse_eq) @@ -337,38 +334,6 @@ by (rule Ring_and_Field.add_le_cancel_left) -subsection{*Factor Cancellation Theorems for Type @{text real}*} - -lemma real_mult_less_cancel2: - "(m*k < n*k) = (((0::real) < k & m m<=n) & (k < 0 --> n<=m))" - by (rule Ring_and_Field.mult_le_cancel_right) - -lemma real_mult_less_cancel1: - "(k*m < k*n) = (((0::real) < k & m m<=n) & (k < 0 --> n<=m))" - by (rule Ring_and_Field.mult_le_cancel_left) - -lemma real_mult_eq_cancel1: "!!k::real. (k*m = k*n) = (k = 0 | m=n)" - by (rule Ring_and_Field.mult_cancel_left) - -lemma real_mult_eq_cancel2: "!!k::real. (m*k = n*k) = (k = 0 | m=n)" - by (rule Ring_and_Field.mult_cancel_right) - -lemma real_mult_div_cancel1: "!!k::real. k~=0 ==> (k*m) / (k*n) = (m/n)" - by (rule Ring_and_Field.mult_divide_cancel_left) - -lemma real_mult_div_cancel_disj: - "(k*m) / (k*n) = (if k = (0::real) then 0 else m/n)" - by (rule Ring_and_Field.mult_divide_cancel_eq_if) - - subsection{*Inverse and Division*} lemma real_inverse_gt_0: "0 < x ==> 0 < inverse (x::real)" diff -r cc0b4bbfbc43 -r f17ca9f6dc8c src/HOL/Real/real_arith.ML --- a/src/HOL/Real/real_arith.ML Fri Dec 19 10:38:48 2003 +0100 +++ b/src/HOL/Real/real_arith.ML Fri Dec 19 17:13:28 2003 +0100 @@ -30,15 +30,17 @@ and d = gcd(m,m') and n=m/d and n'=m'/d. *) -val real_inverse_eq_divide = thm"real_inverse_eq_divide"; -val real_mult_less_cancel2 = thm"real_mult_less_cancel2"; -val real_mult_le_cancel2 = thm"real_mult_le_cancel2"; -val real_mult_less_cancel1 = thm"real_mult_less_cancel1"; -val real_mult_le_cancel1 = thm"real_mult_le_cancel1"; -val real_mult_eq_cancel1 = thm"real_mult_eq_cancel1"; -val real_mult_eq_cancel2 = thm"real_mult_eq_cancel2"; -val real_mult_div_cancel1 = thm"real_mult_div_cancel1"; -val real_mult_div_cancel_disj = thm"real_mult_div_cancel_disj"; +val inverse_eq_divide = thm"Ring_and_Field.inverse_eq_divide"; + +val mult_less_cancel_left = thm"Ring_and_Field.mult_less_cancel_left"; +val mult_le_cancel_left = thm"Ring_and_Field.mult_le_cancel_left"; +val mult_less_cancel_right = thm"Ring_and_Field.mult_less_cancel_right"; +val mult_le_cancel_right = thm"Ring_and_Field.mult_le_cancel_right"; +val mult_cancel_left = thm"Ring_and_Field.mult_cancel_left"; +val mult_cancel_right = thm"Ring_and_Field.mult_cancel_right"; + +val mult_divide_cancel_left = thm"Ring_and_Field.mult_divide_cancel_left"; +val mult_divide_cancel_eq_if = thm"Ring_and_Field.mult_divide_cancel_eq_if"; local @@ -67,7 +69,7 @@ val prove_conv = Bin_Simprocs.prove_conv val mk_bal = HOLogic.mk_binop "HOL.divide" val dest_bal = HOLogic.dest_bin "HOL.divide" HOLogic.realT - val cancel = real_mult_div_cancel1 RS trans + val cancel = mult_divide_cancel_left RS trans val neg_exchanges = false ) @@ -76,7 +78,7 @@ val prove_conv = Bin_Simprocs.prove_conv val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT - val cancel = real_mult_eq_cancel1 RS trans + val cancel = mult_cancel_left RS trans val neg_exchanges = false ) @@ -85,7 +87,7 @@ val prove_conv = Bin_Simprocs.prove_conv val mk_bal = HOLogic.mk_binrel "op <" val dest_bal = HOLogic.dest_bin "op <" HOLogic.realT - val cancel = real_mult_less_cancel1 RS trans + val cancel = mult_less_cancel_left RS trans val neg_exchanges = true ) @@ -94,7 +96,7 @@ val prove_conv = Bin_Simprocs.prove_conv val mk_bal = HOLogic.mk_binrel "op <=" val dest_bal = HOLogic.dest_bin "op <=" HOLogic.realT - val cancel = real_mult_le_cancel1 RS trans + val cancel = mult_le_cancel_left RS trans val neg_exchanges = true ) @@ -185,7 +187,7 @@ val prove_conv = Bin_Simprocs.prove_conv val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT - val simplify_meta_eq = cancel_simplify_meta_eq real_mult_eq_cancel1 + val simplify_meta_eq = cancel_simplify_meta_eq mult_cancel_left ); @@ -194,7 +196,7 @@ val prove_conv = Bin_Simprocs.prove_conv val mk_bal = HOLogic.mk_binop "HOL.divide" val dest_bal = HOLogic.dest_bin "HOL.divide" HOLogic.realT - val simplify_meta_eq = cancel_simplify_meta_eq real_mult_div_cancel_disj + val simplify_meta_eq = cancel_simplify_meta_eq mult_divide_cancel_eq_if ); val real_cancel_factor = diff -r cc0b4bbfbc43 -r f17ca9f6dc8c src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Fri Dec 19 10:38:48 2003 +0100 +++ b/src/HOL/Ring_and_Field.thy Fri Dec 19 17:13:28 2003 +0100 @@ -1398,7 +1398,7 @@ lemma abs_idempotent [simp]: "abs (abs a) = abs (a::'a::ordered_ring)" by (force elim: order_less_asym simp add: abs_if) -lemma abs_zero_iff [iff]: "(abs a = 0) = (a = (0::'a::ordered_ring))" +lemma abs_zero_iff [simp]: "(abs a = 0) = (a = (0::'a::ordered_ring))" by (simp add: abs_if) lemma abs_ge_self: "a \ abs (a::'a::ordered_ring)"