# HG changeset patch # User paulson # Date 1070362095 -3600 # Node ID 342451d763f95d0c28d28ad06a91fbd3169b5475 # Parent 502a7c95de73c21eba24c313bf1ed42ee1c2476b More re-organising of numerical theorems diff -r 502a7c95de73 -r 342451d763f9 doc-src/TutorialI/Advanced/document/simp.tex --- a/doc-src/TutorialI/Advanced/document/simp.tex Fri Nov 28 12:09:37 2003 +0100 +++ b/doc-src/TutorialI/Advanced/document/simp.tex Tue Dec 02 11:48:15 2003 +0100 @@ -160,7 +160,7 @@ Each occurrence of an unknown is of the form $\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound variables. Thus all ordinary rewrite rules, where all unknowns are -of base type, for example \isa{{\isacharquery}m\ {\isacharplus}\ {\isacharquery}n\ {\isacharplus}\ {\isacharquery}k\ {\isacharequal}\ {\isacharquery}m\ {\isacharplus}\ {\isacharparenleft}{\isacharquery}n\ {\isacharplus}\ {\isacharquery}k{\isacharparenright}}, are acceptable: if an unknown is +of base type, for example \isa{{\isacharquery}a\ {\isacharplus}\ {\isacharquery}b\ {\isacharplus}\ {\isacharquery}c\ {\isacharequal}\ {\isacharquery}a\ {\isacharplus}\ {\isacharparenleft}{\isacharquery}b\ {\isacharplus}\ {\isacharquery}c{\isacharparenright}}, are acceptable: if an unknown is of base type, it cannot have any arguments. Additionally, the rule \isa{{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymand}\ {\isacharquery}Q\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}Q\ x{\isacharparenright}{\isacharparenright}} is also acceptable, in both directions: all arguments of the unknowns \isa{{\isacharquery}P} and diff -r 502a7c95de73 -r 342451d763f9 doc-src/TutorialI/Types/document/Numbers.tex --- a/doc-src/TutorialI/Types/document/Numbers.tex Fri Nov 28 12:09:37 2003 +0100 +++ b/doc-src/TutorialI/Types/document/Numbers.tex Tue Dec 02 11:48:15 2003 +0100 @@ -57,17 +57,17 @@ \rulename{add_2_eq_Suc'} \begin{isabelle}% -m\ {\isacharplus}\ n\ {\isacharplus}\ k\ {\isacharequal}\ m\ {\isacharplus}\ {\isacharparenleft}n\ {\isacharplus}\ k{\isacharparenright}% +a\ {\isacharplus}\ b\ {\isacharplus}\ c\ {\isacharequal}\ a\ {\isacharplus}\ {\isacharparenleft}b\ {\isacharplus}\ c{\isacharparenright}% \end{isabelle} \rulename{add_assoc} \begin{isabelle}% -m\ {\isacharplus}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m% +a\ {\isacharplus}\ b\ {\isacharequal}\ b\ {\isacharplus}\ a% \end{isabelle} \rulename{add_commute} \begin{isabelle}% -x\ {\isacharplus}\ {\isacharparenleft}y\ {\isacharplus}\ z{\isacharparenright}\ {\isacharequal}\ y\ {\isacharplus}\ {\isacharparenleft}x\ {\isacharplus}\ z{\isacharparenright}% +a\ {\isacharplus}\ {\isacharparenleft}b\ {\isacharplus}\ c{\isacharparenright}\ {\isacharequal}\ b\ {\isacharplus}\ {\isacharparenleft}a\ {\isacharplus}\ c{\isacharparenright}% \end{isabelle} \rulename{add_left_commute} diff -r 502a7c95de73 -r 342451d763f9 doc-src/TutorialI/Types/document/Records.tex --- a/doc-src/TutorialI/Types/document/Records.tex Fri Nov 28 12:09:37 2003 +0100 +++ b/doc-src/TutorialI/Types/document/Records.tex Tue Dec 02 11:48:15 2003 +0100 @@ -166,8 +166,8 @@ \medskip \begin{tabular}{l} - \isa{point}~\isa{{\isacharequal}}~\isa{{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharcolon}\ int{\isasymrparr}} \\ - \isa{{\isacharprime}a\ point{\isacharunderscore}scheme}~\isa{{\isacharequal}}~\isa{{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a{\isasymrparr}} \\ + \isa{point}~\isa{{\isacharequal}}~\isa{point} \\ + \isa{{\isacharprime}a\ point{\isacharunderscore}scheme}~\isa{{\isacharequal}}~\isa{{\isacharprime}a\ point{\isacharunderscore}scheme} \\ \end{tabular} \medskip diff -r 502a7c95de73 -r 342451d763f9 src/HOL/Hyperreal/HyperOrd.ML --- a/src/HOL/Hyperreal/HyperOrd.ML Fri Nov 28 12:09:37 2003 +0100 +++ b/src/HOL/Hyperreal/HyperOrd.ML Tue Dec 02 11:48:15 2003 +0100 @@ -382,7 +382,7 @@ Goalw [omega_def,hypreal_of_real_def] "~ (EX x. hypreal_of_real x = omega)"; by (auto_tac (claset(), - simpset() addsimps [real_of_nat_Suc, real_diff_eq_eq RS sym, + simpset() addsimps [real_of_nat_Suc, diff_eq_eq RS sym, lemma_finite_omega_set RS FreeUltrafilterNat_finite])); qed "not_ex_hypreal_of_real_eq_omega"; diff -r 502a7c95de73 -r 342451d763f9 src/HOL/Hyperreal/Lim.ML --- a/src/HOL/Hyperreal/Lim.ML Fri Nov 28 12:09:37 2003 +0100 +++ b/src/HOL/Hyperreal/Lim.ML Tue Dec 02 11:48:15 2003 +0100 @@ -1791,7 +1791,7 @@ by (subgoal_tac "\\x. a \\ x & x \\ b --> isCont (%x. inverse(M - f x)) x" 1); by Safe_tac; by (EVERY[rtac isCont_inverse 2, rtac isCont_diff 2, rtac notI 4]); -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [real_diff_eq_eq]))); +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [diff_eq_eq]))); by (Blast_tac 2); by (subgoal_tac "\\k. \\x. a \\ x & x \\ b --> (%x. inverse(M - (f x))) x \\ k" 1); @@ -1800,7 +1800,7 @@ by (subgoal_tac "\\x. a \\ x & x \\ b --> 0 < inverse(M - f(x))" 1); by (Asm_full_simp_tac 1); by Safe_tac; -by (asm_full_simp_tac (simpset() addsimps [real_less_diff_eq]) 2); +by (asm_full_simp_tac (simpset() addsimps [less_diff_eq]) 2); by (subgoal_tac "\\x. a \\ x & x \\ b --> (%x. inverse(M - (f x))) x < (k + 1)" 1); by Safe_tac; @@ -1815,7 +1815,7 @@ by (dres_inst_tac [("P", "%N. N ?Q N"), ("x","M - inverse(k + 1)")] spec 1); by (Step_tac 1 THEN dtac real_leI 1); -by (dtac (real_le_diff_eq RS iffD1) 1); +by (dtac (le_diff_eq RS iffD1) 1); by (REPEAT(dres_inst_tac [("x","a")] spec 1)); by (Asm_full_simp_tac 1); by (asm_full_simp_tac @@ -1956,7 +1956,7 @@ by (res_inst_tac [("x","x - a")] exI 1); by (res_inst_tac [("x","b - x")] exI 2); by Auto_tac; -by (auto_tac (claset(),simpset() addsimps [real_less_diff_eq])); +by (auto_tac (claset(),simpset() addsimps [less_diff_eq])); qed "lemma_interval_lt"; Goal "[| a < x; x < b |] ==> \ @@ -2098,7 +2098,7 @@ by (dtac MVT 1 THEN assume_tac 1); by (blast_tac (claset() addIs [differentiableI]) 1); by (auto_tac (claset() addSDs [DERIV_unique],simpset() - addsimps [real_diff_eq_eq])); + addsimps [diff_eq_eq])); qed "DERIV_isconst_end"; Goal "[| a < b; \ diff -r 502a7c95de73 -r 342451d763f9 src/HOL/Hyperreal/NSA.ML --- a/src/HOL/Hyperreal/NSA.ML Fri Nov 28 12:09:37 2003 +0100 +++ b/src/HOL/Hyperreal/NSA.ML Tue Dec 02 11:48:15 2003 +0100 @@ -2174,7 +2174,7 @@ by (rtac bexI 1); by (rtac lemma_hyprel_refl 2); by Auto_tac; -by (simp_tac (simpset() addsimps [real_of_nat_Suc, real_diff_less_eq RS sym, +by (simp_tac (simpset() addsimps [real_of_nat_Suc, diff_less_eq RS sym, FreeUltrafilterNat_omega]) 1); qed "HInfinite_omega"; Addsimps [HInfinite_omega]; @@ -2218,7 +2218,7 @@ Goal "0 < u ==> finite {n. u < inverse(real(Suc n))}"; by (asm_simp_tac (simpset() addsimps [real_of_nat_less_inverse_iff]) 1); by (asm_simp_tac (simpset() addsimps [real_of_nat_Suc, - real_less_diff_eq RS sym]) 1); + less_diff_eq RS sym]) 1); by (rtac finite_real_of_nat_less_real 1); qed "finite_inverse_real_of_posnat_gt_real"; @@ -2246,7 +2246,7 @@ by (asm_simp_tac (simpset() addsimps [real_of_nat_inverse_eq_iff]) 1); by (cut_inst_tac [("x","inverse u - 1")] lemma_finite_omega_set 1); by (asm_full_simp_tac (simpset() addsimps [real_of_nat_Suc, - real_diff_eq_eq RS sym, eq_commute]) 1); + diff_eq_eq RS sym, eq_commute]) 1); qed "lemma_finite_omega_set2"; Goal "0 < u ==> finite {n. u <= inverse(real(Suc n))}"; diff -r 502a7c95de73 -r 342451d763f9 src/HOL/Hyperreal/SEQ.ML --- a/src/HOL/Hyperreal/SEQ.ML Fri Nov 28 12:09:37 2003 +0100 +++ b/src/HOL/Hyperreal/SEQ.ML Tue Dec 02 11:48:15 2003 +0100 @@ -503,7 +503,7 @@ by (Force_tac 1); by (rtac (lemma_finite_NSBseq RS finite_subset) 2); by (auto_tac (claset() addIs [finite_real_of_nat_less_real], - simpset() addsimps [real_of_nat_Suc, real_less_diff_eq RS sym])); + simpset() addsimps [real_of_nat_Suc, less_diff_eq RS sym])); val lemma_finite_NSBseq2 = result(); Goal "ALL N. real(Suc N) < abs (X (f N)) \ @@ -1130,7 +1130,7 @@ by (asm_simp_tac (simpset() addsimps [abs_eqI2]) 1); by (res_inst_tac [("t","r")] (real_inverse_inverse RS subst) 1); by (auto_tac (claset() addIs [real_inverse_less_iff RS iffD2], - simpset() delsimps [real_inverse_inverse])); + simpset() delsimps [thm"Ring_and_Field.inverse_inverse_eq"])); qed "LIMSEQ_inverse_zero"; Goal "ALL y. EX N. ALL n. N <= n --> y < f(n) \ diff -r 502a7c95de73 -r 342451d763f9 src/HOL/Hyperreal/Transcendental.ML --- a/src/HOL/Hyperreal/Transcendental.ML Fri Nov 28 12:09:37 2003 +0100 +++ b/src/HOL/Hyperreal/Transcendental.ML Tue Dec 02 11:48:15 2003 +0100 @@ -680,7 +680,7 @@ by (asm_full_simp_tac (simpset() addsimps [LIM_def]) 1); by (Step_tac 1); by (res_inst_tac [("x","abs K - abs x")] exI 1); -by (auto_tac (claset(),simpset() addsimps [real_less_diff_eq])); +by (auto_tac (claset(),simpset() addsimps [less_diff_eq])); by (dtac (abs_triangle_ineq RS order_le_less_trans) 1); by (res_inst_tac [("y","0")] order_le_less_trans 1); by Auto_tac; @@ -703,7 +703,7 @@ by (asm_full_simp_tac (simpset() addsimps [LIM_def]) 1); by (Step_tac 1); by (res_inst_tac [("x","abs K - abs x")] exI 1); -by (auto_tac (claset(),simpset() addsimps [real_less_diff_eq])); +by (auto_tac (claset(),simpset() addsimps [less_diff_eq])); by (dtac (abs_triangle_ineq RS order_le_less_trans) 1); by (res_inst_tac [("y","0")] order_le_less_trans 1); by Auto_tac; @@ -1097,9 +1097,9 @@ Goal "1 <= y ==> EX x. 0 <= x & x <= y - 1 & exp(x) = y"; by (rtac IVT 1); -by (auto_tac (claset() addIs [DERIV_exp RS DERIV_isCont],simpset() - addsimps [real_le_diff_eq])); -by (dtac (CLAIM_SIMP "x <= y ==> (0::real) <= y - x" [real_le_diff_eq]) 1); +by (auto_tac (claset() addIs [DERIV_exp RS DERIV_isCont], + simpset() addsimps [le_diff_eq])); +by (dtac (CLAIM_SIMP "x <= y ==> (0::real) <= y - x" [le_diff_eq]) 1); by (dtac exp_ge_add_one_self 1); by (Asm_full_simp_tac 1); qed "lemma_exp_total"; @@ -2051,10 +2051,13 @@ Goalw [tan_def,real_divide_def] "[| cos x ~= 0; cos y ~= 0 |] \ \ ==> 1 - tan(x)*tan(y) = cos (x + y)/(cos x * cos y)"; -by (auto_tac (claset(),simpset() addsimps [real_inverse_distrib RS sym] - @ real_mult_ac)); +by (auto_tac (claset(), + simpset() delsimps [thm"Ring_and_Field.inverse_mult_distrib"] + addsimps [real_inverse_distrib RS sym] @ real_mult_ac)); by (res_inst_tac [("c1","cos x * cos y")] (real_mult_right_cancel RS subst) 1); -by (auto_tac (claset(), simpset() addsimps [real_mult_assoc, +by (auto_tac (claset(), + simpset() delsimps [thm"Ring_and_Field.inverse_mult_distrib"] + addsimps [real_mult_assoc, real_mult_not_zero,real_diff_mult_distrib,cos_add])); val lemma_tan_add1 = result(); Addsimps [lemma_tan_add1]; diff -r 502a7c95de73 -r 342451d763f9 src/HOL/Real/RComplete.ML --- a/src/HOL/Real/RComplete.ML Fri Nov 28 12:09:37 2003 +0100 +++ b/src/HOL/Real/RComplete.ML Tue Dec 02 11:48:15 2003 +0100 @@ -161,7 +161,7 @@ by (dres_inst_tac [("y","(y + (- X) + 1)")] isLub_le_isUb 2 THEN assume_tac 2); by (full_simp_tac - (simpset() addsimps [real_diff_def, real_diff_le_eq RS sym] @ + (simpset() addsimps [real_diff_def, diff_le_eq RS sym] @ real_add_ac) 2); by (rtac (setleI RS isUbI) 1); by (Step_tac 1); @@ -217,7 +217,7 @@ [real_of_nat_Suc, real_add_mult_distrib2]) 1); by (blast_tac (claset() addIs [isLubD2]) 2); by (asm_full_simp_tac - (simpset() addsimps [real_le_diff_eq RS sym, real_diff_def]) 1); + (simpset() addsimps [le_diff_eq RS sym, real_diff_def]) 1); by (subgoal_tac "isUb (UNIV::real set) \ \ {z. EX n. z = x*(real (Suc n))} (t + (-x))" 1); by (blast_tac (claset() addSIs [isUbI,setleI]) 2); diff -r 502a7c95de73 -r 342451d763f9 src/HOL/Real/RealArith.thy --- a/src/HOL/Real/RealArith.thy Fri Nov 28 12:09:37 2003 +0100 +++ b/src/HOL/Real/RealArith.thy Tue Dec 02 11:48:15 2003 +0100 @@ -181,7 +181,8 @@ (* used in vector theory *) lemma abs_triangle_ineq_three: "abs(w + x + (y::real)) <= abs(w) + abs(x) + abs(y)" -by (auto intro!: abs_triangle_ineq [THEN order_trans] real_add_left_le_mono1 simp add: real_add_assoc) +by (auto intro!: abs_triangle_ineq [THEN order_trans] real_add_left_mono + simp add: real_add_assoc) lemma abs_diff_less_imp_gt_zero: "abs(x - y) < y ==> (0::real) < y" apply (unfold real_abs_def) diff -r 502a7c95de73 -r 342451d763f9 src/HOL/Real/RealBin.ML --- a/src/HOL/Real/RealBin.ML Fri Nov 28 12:09:37 2003 +0100 +++ b/src/HOL/Real/RealBin.ML Tue Dec 02 11:48:15 2003 +0100 @@ -194,16 +194,12 @@ (** Combining of literal coefficients in sums of products **) -Goal "(x < y) = (x-y < (0::real))"; -by (simp_tac (simpset() addsimps [real_diff_less_eq]) 1); -qed "real_less_iff_diff_less_0"; - Goal "(x = y) = (x-y = (0::real))"; -by (simp_tac (simpset() addsimps [real_diff_eq_eq]) 1); +by (simp_tac (simpset() addsimps compare_rls) 1); qed "real_eq_iff_diff_eq_0"; Goal "(x <= y) = (x-y <= (0::real))"; -by (simp_tac (simpset() addsimps [real_diff_le_eq]) 1); +by (simp_tac (simpset() addsimps compare_rls) 1); qed "real_le_iff_diff_le_0"; @@ -217,10 +213,10 @@ (** For cancel_numerals **) val rel_iff_rel_0_rls = map (inst "y" "?u+?v") - [real_less_iff_diff_less_0, real_eq_iff_diff_eq_0, + [real_less_eq_diff, real_eq_iff_diff_eq_0, real_le_iff_diff_le_0] @ map (inst "y" "n") - [real_less_iff_diff_less_0, real_eq_iff_diff_eq_0, + [real_less_eq_diff, real_eq_iff_diff_eq_0, real_le_iff_diff_le_0]; Goal "!!i::real. (i*u + m = j*u + n) = ((i-j)*u + m = n)"; @@ -610,7 +606,7 @@ Addsimprocs [Real_Times_Assoc.conv]; (*Simplification of x-y < 0, etc.*) -AddIffs [real_less_iff_diff_less_0 RS sym]; +AddIffs [real_less_eq_diff RS sym]; AddIffs [real_eq_iff_diff_eq_0 RS sym]; AddIffs [real_le_iff_diff_le_0 RS sym]; diff -r 502a7c95de73 -r 342451d763f9 src/HOL/Real/RealDef.thy --- a/src/HOL/Real/RealDef.thy Fri Nov 28 12:09:37 2003 +0100 +++ b/src/HOL/Real/RealDef.thy Tue Dec 02 11:48:15 2003 +0100 @@ -7,11 +7,26 @@ theory RealDef = PReal: +(*MOVE TO THEORY PREAL*) instance preal :: order proof qed (assumption | rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+ +instance preal :: order + by (intro_classes, + (assumption | + rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+) + +lemma preal_le_linear: "x <= y | y <= (x::preal)" +apply (insert preal_linear [of x y]) +apply (auto simp add: order_less_le) +done + +instance preal :: linorder + by (intro_classes, rule preal_le_linear) + + constdefs realrel :: "((preal * preal) * (preal * preal)) set" "realrel == {p. \x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}" @@ -99,7 +114,8 @@ (*** Proving that realrel is an equivalence relation ***) -lemma preal_trans_lemma: "[| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] +lemma preal_trans_lemma: + "[| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] ==> x1 + y3 = x3 + y1" apply (rule_tac C = y2 in preal_add_right_cancel) apply (rotate_tac 1, drule sym) @@ -109,8 +125,6 @@ apply (simp add: preal_add_ac) done -(** Natural deduction for realrel **) - lemma realrel_iff [simp]: "(((x1,y1),(x2,y2)): realrel) = (x1 + y2 = x2 + y1)" by (unfold realrel_def, blast) @@ -284,70 +298,6 @@ declare real_add_minus_left [simp] -lemma real_add_minus_cancel: "z + ((- z) + w) = (w::real)" -by (simp add: real_add_assoc [symmetric]) - -lemma real_minus_add_cancel: "(-z) + (z + w) = (w::real)" -by (simp add: real_add_assoc [symmetric]) - -declare real_add_minus_cancel [simp] real_minus_add_cancel [simp] - -lemma real_minus_ex: "\y. (x::real) + y = 0" -by (blast intro: real_add_minus) - -lemma real_minus_ex1: "EX! y. (x::real) + y = 0" -apply (auto intro: real_add_minus) -apply (drule_tac f = "%x. ya+x" in arg_cong) -apply (simp add: real_add_assoc [symmetric]) -apply (simp add: real_add_commute) -done - -lemma real_minus_left_ex1: "EX! y. y + (x::real) = 0" -apply (auto intro: real_add_minus_left) -apply (drule_tac f = "%x. x+ya" in arg_cong) -apply (simp add: real_add_assoc) -apply (simp add: real_add_commute) -done - -lemma real_add_minus_eq_minus: "x + y = (0::real) ==> x = -y" -apply (cut_tac z = y in real_add_minus_left) -apply (rule_tac x1 = y in real_minus_left_ex1 [THEN ex1E], blast) -done - -lemma real_as_add_inverse_ex: "\(y::real). x = -y" -apply (cut_tac x = x in real_minus_ex) -apply (erule exE, drule real_add_minus_eq_minus, fast) -done - -lemma real_minus_add_distrib: "-(x + y) = (-x) + (- y :: real)" -apply (rule_tac z = x in eq_Abs_REAL) -apply (rule_tac z = y in eq_Abs_REAL) -apply (auto simp add: real_minus real_add) -done - -declare real_minus_add_distrib [simp] - -lemma real_add_left_cancel: "((x::real) + y = x + z) = (y = z)" -apply safe -apply (drule_tac f = "%t. (-x) + t" in arg_cong) -apply (simp add: real_add_assoc [symmetric]) -done - -lemma real_add_right_cancel: "(y + (x::real)= z + x) = (y = z)" -by (simp add: real_add_commute real_add_left_cancel) - -lemma real_diff_0: "(0::real) - x = -x" -by (simp add: real_diff_def) - -lemma real_diff_0_right: "x - (0::real) = x" -by (simp add: real_diff_def) - -lemma real_diff_self: "x - x = (0::real)" -by (simp add: real_diff_def) - -declare real_diff_0 [simp] real_diff_0_right [simp] real_diff_self [simp] - - (*** Congruence property for multiplication ***) lemma real_mult_congruent2_lemma: "!!(x1::preal). [| x1 + y2 = x2 + y1 |] ==> @@ -491,22 +441,6 @@ apply (auto simp add: preal_add_commute) done - -(*MOVE UP*) -instance preal :: order - by (intro_classes, - (assumption | - rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+) - -lemma preal_le_linear: "x <= y | y <= (x::preal)" -apply (insert preal_linear [of x y]) -apply (auto simp add: order_less_le) -done - -instance preal :: linorder - by (intro_classes, rule preal_le_linear) - - lemma real_mult_inv_right_ex: "!!(x::real). x ~= 0 ==> \y. x*y = (1::real)" apply (unfold real_zero_def real_one_def) @@ -772,11 +706,15 @@ declare real_of_preal_minus_less_rev_iff [simp] -(*** linearity ***) + +subsection{*Linearity of the Ordering*} + lemma real_linear: "(x::real) < y | x = y | y < x" apply (rule_tac x = x in real_of_preal_trichotomyE) apply (rule_tac [!] x = y in real_of_preal_trichotomyE) -apply (auto dest!: preal_le_anti_sym simp add: preal_less_le_iff real_of_preal_minus_less_zero real_of_preal_zero_less real_of_preal_minus_less_all) +apply (auto dest!: preal_le_anti_sym + simp add: preal_less_le_iff real_of_preal_minus_less_zero + real_of_preal_zero_less real_of_preal_minus_less_all) done lemma real_neq_iff: "!!w::real. (w ~= z) = (w z \ (w::real)" - -apply (unfold real_le_def, assumption) -done - -lemma real_leD: "z\w ==> ~(w<(z::real))" -by (unfold real_le_def, assumption) - -lemmas real_leE = real_leD [elim_format] - -lemma real_less_le_iff: "(~(w < z)) = (z \ (w::real))" -by (blast intro!: real_leI real_leD) - -lemma not_real_leE: "~ z \ w ==> w<(z::real)" -by (unfold real_le_def, blast) - -lemma real_le_imp_less_or_eq: "!!(x::real). x \ y ==> x < y | x = y" -apply (unfold real_le_def) -apply (cut_tac real_linear) -apply (blast elim: real_less_irrefl real_less_asym) -done - -lemma real_less_or_eq_imp_le: "z z \(w::real)" -apply (unfold real_le_def) -apply (cut_tac real_linear) -apply (fast elim: real_less_irrefl real_less_asym) -done - -lemma real_le_less: "(x \ (y::real)) = (x < y | x=y)" -by (blast intro!: real_less_or_eq_imp_le dest!: real_le_imp_less_or_eq) - -lemma real_le_refl: "w \ (w::real)" -by (simp add: real_le_less) - -lemma real_le_trans: "[| i \ j; j \ k |] ==> i \ (k::real)" -apply (drule real_le_imp_less_or_eq) -apply (drule real_le_imp_less_or_eq) -apply (rule real_less_or_eq_imp_le) -apply (blast intro: real_less_trans) -done - -lemma real_le_anti_sym: "[| z \ w; w \ z |] ==> z = (w::real)" -apply (drule real_le_imp_less_or_eq) -apply (drule real_le_imp_less_or_eq) -apply (fast elim: real_less_irrefl real_less_asym) -done - -(* Axiom 'order_less_le' of class 'order': *) -lemma real_less_le: "((w::real) < z) = (w \ z & w ~= z)" -apply (simp add: real_le_def real_neq_iff) -apply (blast elim!: real_less_asym) -done - -instance real :: order - by (intro_classes, - (assumption | - rule real_le_refl real_le_trans real_le_anti_sym real_less_le)+) - -(* Axiom 'linorder_linear' of class 'linorder': *) -lemma real_le_linear: "(z::real) \ w | w \ z" -apply (simp add: real_le_less) -apply (cut_tac real_linear, blast) -done - -instance real :: linorder - by (intro_classes, rule real_le_linear) - - lemma real_minus_zero_less_iff: "(0 < -R) = (R < (0::real))" apply (rule_tac x = R in real_of_preal_trichotomyE) apply (auto simp add: real_of_preal_not_minus_gt_zero real_of_preal_not_less_zero real_of_preal_zero_less real_of_preal_minus_less_zero) @@ -870,123 +738,6 @@ done declare real_minus_zero_less_iff2 [simp] -(*Alternative definition for real_less*) -lemma real_less_add_positive_left_Ex: "R < S ==> \T::real. 0 < T & R + T = S" -apply (rule_tac x = R in real_of_preal_trichotomyE) -apply (rule_tac [!] x = S in real_of_preal_trichotomyE) -apply (auto dest!: preal_less_add_left_Ex simp add: real_of_preal_not_minus_gt_all real_of_preal_add real_of_preal_not_less_zero real_less_not_refl real_of_preal_not_minus_gt_zero) -apply (rule_tac x = "real_of_preal D" in exI) -apply (rule_tac [2] x = "real_of_preal m+real_of_preal ma" in exI) -apply (rule_tac [3] x = "real_of_preal D" in exI) -apply (auto simp add: real_of_preal_zero_less real_of_preal_sum_zero_less real_add_assoc) -done - -(** change naff name(s)! **) -lemma real_less_sum_gt_zero: "(W < S) ==> (0 < S + (-W::real))" -apply (drule real_less_add_positive_left_Ex) -apply (auto simp add: real_add_minus real_add_zero_right real_add_ac) -done - -lemma real_lemma_change_eq_subj: "!!S::real. T = S + W ==> S = T + (-W)" -by (simp add: real_add_ac) - -(* FIXME: long! *) -lemma real_sum_gt_zero_less: "(0 < S + (-W::real)) ==> (W < S)" -apply (rule ccontr) -apply (drule real_leI [THEN real_le_imp_less_or_eq]) -apply (auto simp add: real_less_not_refl) -apply (drule real_less_add_positive_left_Ex, clarify, simp) -apply (drule real_lemma_change_eq_subj, auto) -apply (drule real_less_sum_gt_zero) -apply (auto elim: real_less_asym simp add: real_add_left_commute [of W] real_add_ac) -done - -lemma real_less_sum_gt_0_iff: "(0 < S + (-W::real)) = (W < S)" -by (blast intro: real_less_sum_gt_zero real_sum_gt_zero_less) - - -lemma real_less_eq_diff: "(x z) = (x \ z + (y::real))" -apply (unfold real_le_def) -apply (simp add: real_less_diff_eq) -done - -lemma real_le_diff_eq: "(x \ z-y) = (x + (y::real) \ z)" -apply (unfold real_le_def) -apply (simp add: real_diff_less_eq) -done - -lemma real_diff_eq_eq: "(x-y = z) = (x = z + (y::real))" -apply (unfold real_diff_def) -apply (auto simp add: real_add_assoc) -done - -lemma real_eq_diff_eq: "(x = z-y) = (x + (y::real) = z)" -apply (unfold real_diff_def) -apply (auto simp add: real_add_assoc) -done - -(*This list of rewrites simplifies (in)equalities by bringing subtractions - to the top and then moving negative terms to the other side. - Use with real_add_ac*) -lemmas real_compare_rls = - real_diff_def [symmetric] - real_add_diff_eq real_diff_add_eq real_diff_diff_eq real_diff_diff_eq2 - real_diff_less_eq real_less_diff_eq real_diff_le_eq real_le_diff_eq - real_diff_eq_eq real_eq_diff_eq - - -(** For the cancellation simproc. - The idea is to cancel like terms on opposite sides by subtraction **) - -lemma real_less_eqI: "(x::real) - y = x' - y' ==> (x (y\x) = (y'\x')" -apply (drule real_less_eqI) -apply (simp add: real_le_def) -done - -lemma real_eq_eqI: "(x::real) - y = x' - y' ==> (x=y) = (x'=y')" -apply safe -apply (simp_all add: real_eq_diff_eq real_diff_eq_eq) -done - - ML {* val real_le_def = thm "real_le_def"; @@ -1020,122 +771,9 @@ val real_add_zero_right = thm"real_add_zero_right"; val real_add_minus = thm"real_add_minus"; val real_add_minus_left = thm"real_add_minus_left"; -val real_add_minus_cancel = thm"real_add_minus_cancel"; -val real_minus_add_cancel = thm"real_minus_add_cancel"; -val real_minus_ex = thm"real_minus_ex"; -val real_minus_ex1 = thm"real_minus_ex1"; -val real_minus_left_ex1 = thm"real_minus_left_ex1"; -val real_add_minus_eq_minus = thm"real_add_minus_eq_minus"; -val real_as_add_inverse_ex = thm"real_as_add_inverse_ex"; -val real_minus_add_distrib = thm"real_minus_add_distrib"; -val real_add_left_cancel = thm"real_add_left_cancel"; -val real_add_right_cancel = thm"real_add_right_cancel"; -val real_diff_0 = thm"real_diff_0"; -val real_diff_0_right = thm"real_diff_0_right"; -val real_diff_self = thm"real_diff_self"; -val real_mult_congruent2_lemma = thm"real_mult_congruent2_lemma"; -val real_mult_congruent2 = thm"real_mult_congruent2"; -val real_mult = thm"real_mult"; -val real_mult_commute = thm"real_mult_commute"; -val real_mult_assoc = thm"real_mult_assoc"; -val real_mult_left_commute = thm"real_mult_left_commute"; -val real_mult_1 = thm"real_mult_1"; -val real_mult_1_right = thm"real_mult_1_right"; -val real_mult_0 = thm"real_mult_0"; -val real_mult_0_right = thm"real_mult_0_right"; -val real_mult_minus_eq1 = thm"real_mult_minus_eq1"; -val real_minus_mult_eq1 = thm"real_minus_mult_eq1"; -val real_mult_minus_eq2 = thm"real_mult_minus_eq2"; -val real_minus_mult_eq2 = thm"real_minus_mult_eq2"; -val real_mult_minus_1 = thm"real_mult_minus_1"; -val real_mult_minus_1_right = thm"real_mult_minus_1_right"; -val real_minus_mult_cancel = thm"real_minus_mult_cancel"; -val real_minus_mult_commute = thm"real_minus_mult_commute"; -val real_add_assoc_cong = thm"real_add_assoc_cong"; -val real_add_mult_distrib = thm"real_add_mult_distrib"; -val real_add_mult_distrib2 = thm"real_add_mult_distrib2"; -val real_diff_mult_distrib = thm"real_diff_mult_distrib"; -val real_diff_mult_distrib2 = thm"real_diff_mult_distrib2"; -val real_zero_not_eq_one = thm"real_zero_not_eq_one"; -val real_zero_iff = thm"real_zero_iff"; -val preal_le_linear = thm"preal_le_linear"; -val real_mult_inv_right_ex = thm"real_mult_inv_right_ex"; -val real_mult_inv_left_ex = thm"real_mult_inv_left_ex"; -val real_mult_inv_left = thm"real_mult_inv_left"; -val real_mult_inv_right = thm"real_mult_inv_right"; -val preal_lemma_eq_rev_sum = thm"preal_lemma_eq_rev_sum"; -val preal_add_left_commute_cancel = thm"preal_add_left_commute_cancel"; -val preal_lemma_for_not_refl = thm"preal_lemma_for_not_refl"; -val real_less_not_refl = thm"real_less_not_refl"; -val real_less_irrefl = thm"real_less_irrefl"; -val real_not_refl2 = thm"real_not_refl2"; -val preal_lemma_trans = thm"preal_lemma_trans"; -val real_less_trans = thm"real_less_trans"; -val real_less_not_sym = thm"real_less_not_sym"; -val real_less_asym = thm"real_less_asym"; -val real_of_preal_add = thm"real_of_preal_add"; -val real_of_preal_mult = thm"real_of_preal_mult"; -val real_of_preal_ExI = thm"real_of_preal_ExI"; -val real_of_preal_ExD = thm"real_of_preal_ExD"; -val real_of_preal_iff = thm"real_of_preal_iff"; -val real_of_preal_trichotomy = thm"real_of_preal_trichotomy"; -val real_of_preal_trichotomyE = thm"real_of_preal_trichotomyE"; -val real_of_preal_lessD = thm"real_of_preal_lessD"; -val real_of_preal_lessI = thm"real_of_preal_lessI"; -val real_of_preal_less_iff1 = thm"real_of_preal_less_iff1"; -val real_of_preal_minus_less_self = thm"real_of_preal_minus_less_self"; -val real_of_preal_minus_less_zero = thm"real_of_preal_minus_less_zero"; -val real_of_preal_not_minus_gt_zero = thm"real_of_preal_not_minus_gt_zero"; -val real_of_preal_zero_less = thm"real_of_preal_zero_less"; -val real_of_preal_not_less_zero = thm"real_of_preal_not_less_zero"; -val real_minus_minus_zero_less = thm"real_minus_minus_zero_less"; -val real_of_preal_sum_zero_less = thm"real_of_preal_sum_zero_less"; -val real_of_preal_minus_less_all = thm"real_of_preal_minus_less_all"; -val real_of_preal_not_minus_gt_all = thm"real_of_preal_not_minus_gt_all"; -val real_of_preal_minus_less_rev1 = thm"real_of_preal_minus_less_rev1"; -val real_of_preal_minus_less_rev2 = thm"real_of_preal_minus_less_rev2"; -val real_of_preal_minus_less_rev_iff = thm"real_of_preal_minus_less_rev_iff"; -val real_linear = thm"real_linear"; -val real_neq_iff = thm"real_neq_iff"; -val real_linear_less2 = thm"real_linear_less2"; -val real_leI = thm"real_leI"; -val real_leD = thm"real_leD"; -val real_leE = thm"real_leE"; -val real_less_le_iff = thm"real_less_le_iff"; -val not_real_leE = thm"not_real_leE"; -val real_le_imp_less_or_eq = thm"real_le_imp_less_or_eq"; -val real_less_or_eq_imp_le = thm"real_less_or_eq_imp_le"; -val real_le_less = thm"real_le_less"; -val real_le_refl = thm"real_le_refl"; -val real_le_linear = thm"real_le_linear"; -val real_le_trans = thm"real_le_trans"; -val real_le_anti_sym = thm"real_le_anti_sym"; -val real_less_le = thm"real_less_le"; -val real_minus_zero_less_iff = thm"real_minus_zero_less_iff"; -val real_minus_zero_less_iff2 = thm"real_minus_zero_less_iff2"; -val real_less_add_positive_left_Ex = thm"real_less_add_positive_left_Ex"; -val real_less_sum_gt_zero = thm"real_less_sum_gt_zero"; -val real_lemma_change_eq_subj = thm"real_lemma_change_eq_subj"; -val real_sum_gt_zero_less = thm"real_sum_gt_zero_less"; -val real_less_sum_gt_0_iff = thm"real_less_sum_gt_0_iff"; -val real_less_eq_diff = thm"real_less_eq_diff"; -val real_add_diff_eq = thm"real_add_diff_eq"; -val real_diff_add_eq = thm"real_diff_add_eq"; -val real_diff_diff_eq = thm"real_diff_diff_eq"; -val real_diff_diff_eq2 = thm"real_diff_diff_eq2"; -val real_diff_less_eq = thm"real_diff_less_eq"; -val real_less_diff_eq = thm"real_less_diff_eq"; -val real_diff_le_eq = thm"real_diff_le_eq"; -val real_le_diff_eq = thm"real_le_diff_eq"; -val real_diff_eq_eq = thm"real_diff_eq_eq"; -val real_eq_diff_eq = thm"real_eq_diff_eq"; -val real_less_eqI = thm"real_less_eqI"; -val real_le_eqI = thm"real_le_eqI"; -val real_eq_eqI = thm"real_eq_eqI"; val real_add_ac = thms"real_add_ac"; val real_mult_ac = thms"real_mult_ac"; -val real_compare_rls = thms"real_compare_rls"; *} diff -r 502a7c95de73 -r 342451d763f9 src/HOL/Real/RealOrd.thy --- a/src/HOL/Real/RealOrd.thy Fri Nov 28 12:09:37 2003 +0100 +++ b/src/HOL/Real/RealOrd.thy Tue Dec 02 11:48:15 2003 +0100 @@ -13,7 +13,388 @@ -subsection{* The Simproc @{text abel_cancel}*} +subsection{*Properties of Less-Than Or Equals*} + +lemma real_leI: "~(w < z) ==> z \ (w::real)" +apply (unfold real_le_def, assumption) +done + +lemma real_leD: "z\w ==> ~(w<(z::real))" +by (unfold real_le_def, assumption) + +lemmas real_leE = real_leD [elim_format] + +lemma real_less_le_iff: "(~(w < z)) = (z \ (w::real))" +by (blast intro!: real_leI real_leD) + +lemma not_real_leE: "~ z \ w ==> w<(z::real)" +by (unfold real_le_def, blast) + +lemma real_le_imp_less_or_eq: "!!(x::real). x \ y ==> x < y | x = y" +apply (unfold real_le_def) +apply (cut_tac real_linear) +apply (blast elim: real_less_irrefl real_less_asym) +done + +lemma real_less_or_eq_imp_le: "z z \(w::real)" +apply (unfold real_le_def) +apply (cut_tac real_linear) +apply (fast elim: real_less_irrefl real_less_asym) +done + +lemma real_le_less: "(x \ (y::real)) = (x < y | x=y)" +by (blast intro!: real_less_or_eq_imp_le dest!: real_le_imp_less_or_eq) + +lemma real_le_refl: "w \ (w::real)" +by (simp add: real_le_less) + +lemma real_le_trans: "[| i \ j; j \ k |] ==> i \ (k::real)" +apply (drule real_le_imp_less_or_eq) +apply (drule real_le_imp_less_or_eq) +apply (rule real_less_or_eq_imp_le) +apply (blast intro: real_less_trans) +done + +lemma real_le_anti_sym: "[| z \ w; w \ z |] ==> z = (w::real)" +apply (drule real_le_imp_less_or_eq) +apply (drule real_le_imp_less_or_eq) +apply (fast elim: real_less_irrefl real_less_asym) +done + +(* Axiom 'order_less_le' of class 'order': *) +lemma real_less_le: "((w::real) < z) = (w \ z & w ~= z)" +apply (simp add: real_le_def real_neq_iff) +apply (blast elim!: real_less_asym) +done + +instance real :: order + by (intro_classes, + (assumption | + rule real_le_refl real_le_trans real_le_anti_sym real_less_le)+) + +(* Axiom 'linorder_linear' of class 'linorder': *) +lemma real_le_linear: "(z::real) \ w | w \ z" +apply (simp add: real_le_less) +apply (cut_tac real_linear, blast) +done + +instance real :: linorder + by (intro_classes, rule real_le_linear) + + +subsection{*Theorems About the Ordering*} + +lemma real_gt_zero_preal_Ex: "(0 < x) = (\y. x = real_of_preal y)" +apply (auto simp add: real_of_preal_zero_less) +apply (cut_tac x = x in real_of_preal_trichotomy) +apply (blast elim!: real_less_irrefl real_of_preal_not_minus_gt_zero [THEN notE]) +done + +lemma real_gt_preal_preal_Ex: "real_of_preal z < x ==> \y. x = real_of_preal y" +by (blast dest!: real_of_preal_zero_less [THEN real_less_trans] + intro: real_gt_zero_preal_Ex [THEN iffD1]) + +lemma real_ge_preal_preal_Ex: "real_of_preal z \ x ==> \y. x = real_of_preal y" +by (blast dest: order_le_imp_less_or_eq real_gt_preal_preal_Ex) + +lemma real_less_all_preal: "y \ 0 ==> \x. y < real_of_preal x" +by (auto elim: order_le_imp_less_or_eq [THEN disjE] + intro: real_of_preal_zero_less [THEN [2] real_less_trans] + simp add: real_of_preal_zero_less) + +lemma real_less_all_real2: "~ 0 < y ==> \x. y < real_of_preal x" +by (blast intro!: real_less_all_preal real_leI) + +lemma real_of_preal_le_iff: "(real_of_preal m1 \ real_of_preal m2) = (m1 \ m2)" +apply (auto intro!: preal_leI simp add: real_less_le_iff [symmetric]) +apply (drule order_le_less_trans, assumption) +apply (erule preal_less_irrefl) +done + + +subsection{*Monotonicity of Addition*} + +lemma real_add_left_cancel: "((x::real) + y = x + z) = (y = z)" +apply safe +apply (drule_tac f = "%t. (-x) + t" in arg_cong) +apply (simp add: real_add_assoc [symmetric]) +done + + +lemma real_mult_order: "[| 0 < x; 0 < y |] ==> (0::real) < x * y" +apply (auto simp add: real_gt_zero_preal_Ex) +apply (rule_tac x = "y*ya" in exI) +apply (simp (no_asm_use) add: real_of_preal_mult) +done + +lemma real_minus_add_distrib [simp]: "-(x + y) = (-x) + (- y :: real)" +apply (rule_tac z = x in eq_Abs_REAL) +apply (rule_tac z = y in eq_Abs_REAL) +apply (auto simp add: real_minus real_add) +done + +(*Alternative definition for real_less*) +lemma real_less_add_positive_left_Ex: "R < S ==> \T::real. 0 < T & R + T = S" +apply (rule_tac x = R in real_of_preal_trichotomyE) +apply (rule_tac [!] x = S in real_of_preal_trichotomyE) +apply (auto dest!: preal_less_add_left_Ex simp add: real_of_preal_not_minus_gt_all real_of_preal_add real_of_preal_not_less_zero real_less_not_refl real_of_preal_not_minus_gt_zero) +apply (rule_tac x = "real_of_preal D" in exI) +apply (rule_tac [2] x = "real_of_preal m+real_of_preal ma" in exI) +apply (rule_tac [3] x = "real_of_preal D" in exI) +apply (auto simp add: real_of_preal_zero_less real_of_preal_sum_zero_less real_add_assoc) +apply (simp add: real_add_assoc [symmetric]) +done + +lemma real_less_sum_gt_zero: "(W < S) ==> (0 < S + (-W::real))" +apply (drule real_less_add_positive_left_Ex) +apply (auto simp add: real_add_minus real_add_zero_right real_add_ac) +done + +lemma real_lemma_change_eq_subj: "!!S::real. T = S + W ==> S = T + (-W)" +by (simp add: real_add_ac) + +(* FIXME: long! *) +lemma real_sum_gt_zero_less: "(0 < S + (-W::real)) ==> (W < S)" +apply (rule ccontr) +apply (drule real_leI [THEN real_le_imp_less_or_eq]) +apply (auto simp add: real_less_not_refl) +apply (drule real_less_add_positive_left_Ex, clarify, simp) +apply (drule real_lemma_change_eq_subj, auto) +apply (drule real_less_sum_gt_zero) +apply (auto elim: real_less_asym simp add: real_add_left_commute [of W] real_add_ac) +done + +lemma real_mult_less_mono2: "[| (0::real) < z; x < y |] ==> z * x < z * y" +apply (rule real_sum_gt_zero_less) +apply (drule real_less_sum_gt_zero [of x y]) +apply (drule real_mult_order, assumption) +apply (simp add: real_add_mult_distrib2) +done + +(** For the cancellation simproc. + The idea is to cancel like terms on opposite sides by subtraction **) + +lemma real_less_sum_gt_0_iff: "(0 < S + (-W::real)) = (W < S)" +by (blast intro: real_less_sum_gt_zero real_sum_gt_zero_less) + +lemma real_less_eq_diff: "(x (x (y\x) = (y'\x')" +apply (drule real_less_eqI) +apply (simp add: real_le_def) +done + +lemma real_add_left_mono: "x \ y ==> z + x \ z + (y::real)" +apply (rule real_le_eqI [THEN iffD1]) + prefer 2 apply assumption; +apply (simp add: real_diff_def real_add_ac); +done + + +subsection{*The Reals Form an Ordered Field*} + +instance real :: inverse .. + +instance real :: ordered_field +proof + fix x y z :: real + show "(x + y) + z = x + (y + z)" by (rule real_add_assoc) + show "x + y = y + x" by (rule real_add_commute) + show "0 + x = x" by simp + show "- x + x = 0" by simp + show "x - y = x + (-y)" by (simp add: real_diff_def) + show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc) + show "x * y = y * x" by (rule real_mult_commute) + show "1 * x = x" by simp + show "(x + y) * z = x * z + y * z" by (simp add: real_add_mult_distrib) + show "0 \ (1::real)" by (rule real_zero_not_eq_one) + show "x \ y ==> z + x \ z + y" by (rule real_add_left_mono) + show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: real_mult_less_mono2) + show "\x\ = (if x < 0 then -x else x)" + by (auto dest: order_le_less_trans simp add: real_abs_def linorder_not_le) + show "x \ 0 ==> inverse x * x = 1" by simp + show "y \ 0 ==> x / y = x * inverse y" by (simp add: real_divide_def) +qed + + +lemma real_zero_less_one: "0 < (1::real)" + by (rule Ring_and_Field.zero_less_one) + +lemma real_add_less_mono: "[| R1 < S1; R2 < S2 |] ==> R1+R2 < S1+(S2::real)" + by (rule Ring_and_Field.add_strict_mono) + +lemma real_add_le_mono: "[|i\j; k\l |] ==> i + k \ j + (l::real)" + by (rule Ring_and_Field.add_mono) + +lemma real_le_minus_iff: "(-s \ -r) = ((r::real) \ s)" + by (rule Ring_and_Field.neg_le_iff_le) + +lemma real_le_square [simp]: "(0::real) \ x*x" + by (rule Ring_and_Field.zero_le_square) + + +subsection{*Division Lemmas*} + +(** Inverse of zero! Useful to simplify certain equations **) + +lemma INVERSE_ZERO: "inverse 0 = (0::real)" +apply (unfold real_inverse_def) +apply (rule someI2) +apply (auto simp add: real_zero_not_eq_one) +done + +lemma DIVISION_BY_ZERO [simp]: "a / (0::real) = 0" + by (simp add: real_divide_def INVERSE_ZERO) + +instance real :: division_by_zero +proof + fix x :: real + show "inverse 0 = (0::real)" by (rule INVERSE_ZERO) + show "x/0 = 0" by (rule DIVISION_BY_ZERO) +qed + +lemma real_mult_left_cancel: "(c::real) ~= 0 ==> (c*a=c*b) = (a=b)" +by auto + +lemma real_mult_right_cancel: "(c::real) ~= 0 ==> (a*c=b*c) = (a=b)" +by auto + +lemma real_mult_left_cancel_ccontr: "c*a ~= c*b ==> a ~= b" +by auto + +lemma real_mult_right_cancel_ccontr: "a*c ~= b*c ==> a ~= b" +by auto + +lemma real_inverse_not_zero: "x ~= 0 ==> inverse(x::real) ~= 0" + by (rule Ring_and_Field.nonzero_imp_inverse_nonzero) + +lemma real_mult_not_zero: "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::real)" +by simp + +lemma real_inverse_inverse: "inverse(inverse (x::real)) = x" + by (rule Ring_and_Field.inverse_inverse_eq) + +lemma real_inverse_1: "inverse((1::real)) = (1::real)" + by (rule Ring_and_Field.inverse_1) + +lemma real_minus_inverse: "inverse(-x) = -inverse(x::real)" + by (rule Ring_and_Field.inverse_minus_eq) + +lemma real_inverse_distrib: "inverse(x*y) = inverse(x)*inverse(y::real)" + by (rule Ring_and_Field.inverse_mult_distrib) + +lemma real_times_divide1_eq: "(x::real) * (y/z) = (x*y)/z" +by (simp add: real_divide_def real_mult_assoc) + +lemma real_times_divide2_eq: "(y/z) * (x::real) = (y*x)/z" +by (simp add: real_divide_def real_mult_ac) + +declare real_times_divide1_eq [simp] real_times_divide2_eq [simp] + +lemma real_divide_divide1_eq: "(x::real) / (y/z) = (x*z)/y" +by (simp add: real_divide_def real_inverse_distrib real_mult_ac) + +lemma real_divide_divide2_eq: "((x::real) / y) / z = x/(y*z)" +by (simp add: real_divide_def real_inverse_distrib real_mult_assoc) + +declare real_divide_divide1_eq [simp] real_divide_divide2_eq [simp] + +(** As with multiplication, pull minus signs OUT of the / operator **) + +lemma real_minus_divide_eq: "(-x) / (y::real) = - (x/y)" +by (simp add: real_divide_def) +declare real_minus_divide_eq [simp] + +lemma real_divide_minus_eq: "(x / -(y::real)) = - (x/y)" +by (simp add: real_divide_def real_minus_inverse) +declare real_divide_minus_eq [simp] + +lemma real_add_divide_distrib: "(x+y)/(z::real) = x/z + y/z" +by (simp add: real_divide_def real_add_mult_distrib) + +(*The following would e.g. convert (x+y)/2 to x/2 + y/2. Sometimes that + leads to cancellations in x or y, but is also prevents "multiplying out" + the 2 in e.g. (x+y)/2 = 5. + +Addsimps [inst "z" "number_of ?w" real_add_divide_distrib] +**) + + + +subsection{*More Lemmas*} + +lemma real_add_right_cancel: "(y + (x::real)= z + x) = (y = z)" + by (rule Ring_and_Field.add_right_cancel) + +lemma real_add_less_mono1: "v < (w::real) ==> v + z < w + z" + by (rule Ring_and_Field.add_strict_right_mono) + +lemma real_add_le_mono1: "v \ (w::real) ==> v + z \ w + z" + by (rule Ring_and_Field.add_right_mono) + +lemma real_add_less_le_mono: "[| w'z |] ==> w' + z' < w + (z::real)" +apply (erule add_strict_right_mono [THEN order_less_le_trans]) +apply (erule add_left_mono) +done + +lemma real_add_le_less_mono: "!!z z'::real. [| w'\w; z' w' + z' < w + z" +apply (erule add_right_mono [THEN order_le_less_trans]) +apply (erule add_strict_left_mono) +done + +lemma real_less_add_right_cancel: "!!(A::real). A + C < B + C ==> A < B" + by (rule Ring_and_Field.add_less_imp_less_right) + +lemma real_less_add_left_cancel: "!!(A::real). C + A < C + B ==> A < B" + by (rule Ring_and_Field.add_less_imp_less_left) + +lemma real_le_add_right_cancel: "!!(A::real). A + C \ B + C ==> A \ B" + by (rule Ring_and_Field.add_le_imp_le_right) + + lemma add_le_imp_le_left: + "c + a \ c + b ==> a \ (b::'a::ordered_ring)" + by simp + +lemma real_le_add_left_cancel: "!!(A::real). C + A \ C + B ==> A \ B" + by (rule (*Ring_and_Field.*)add_le_imp_le_left) + +lemma real_minus_diff_eq: "- (z - y) = y - (z::real)" + by (rule Ring_and_Field.minus_diff_eq) + +lemma real_add_right_cancel_less [simp]: "(v+z < w+z) = (v < (w::real))" + by (rule Ring_and_Field.add_less_cancel_right) + +lemma real_add_left_cancel_less [simp]: "(z+v < z+w) = (v < (w::real))" + by (rule Ring_and_Field.add_less_cancel_left) + +lemma real_add_right_cancel_le [simp]: "(v+z \ w+z) = (v \ (w::real))" + by (rule Ring_and_Field.add_le_cancel_right) + +lemma real_add_left_cancel_le [simp]: "(z+v \ z+w) = (v \ (w::real))" + by (rule Ring_and_Field.add_le_cancel_left) + + +subsection{*For the @{text abel_cancel} Simproc (DELETE)*} + +lemma real_eq_eqI: "(x::real) - y = x' - y' ==> (x=y) = (x'=y')" +apply safe +apply (simp_all add: eq_diff_eq diff_eq_eq) +done + +lemma real_add_minus_cancel: "z + ((- z) + w) = (w::real)" +by (simp add: real_add_assoc [symmetric]) + +lemma real_minus_add_cancel: "(-z) + (z + w) = (w::real)" +by (simp add: real_add_assoc [symmetric]) (*Deletion of other terms in the formula, seeking the -x at the front of z*) lemma real_add_cancel_21: "((x::real) + (y + z) = y + u) = ((x + z) = u)" @@ -26,7 +407,7 @@ lemma real_add_cancel_end: "((x::real) + (y + z) = y) = (x = -z)" apply (subst real_add_left_commute) apply (rule_tac t = y in real_add_zero_right [THEN subst], subst real_add_left_cancel) -apply (simp add: real_eq_diff_eq [symmetric]) +apply (simp add: real_diff_def eq_diff_eq [symmetric]) done @@ -34,6 +415,14 @@ {* val real_add_cancel_21 = thm "real_add_cancel_21"; val real_add_cancel_end = thm "real_add_cancel_end"; +val real_add_left_cancel = thm"real_add_left_cancel"; +val real_eq_diff_eq = thm"eq_diff_eq"; +val real_less_eqI = thm"real_less_eqI"; +val real_le_eqI = thm"real_le_eqI"; +val real_eq_eqI = thm"real_eq_eqI"; +val real_add_minus_cancel = thm"real_add_minus_cancel"; +val real_minus_add_cancel = thm"real_minus_add_cancel"; +val real_minus_add_distrib = thm"real_minus_add_distrib"; structure Real_Cancel_Data = struct @@ -72,245 +461,6 @@ Addsimprocs [Real_Cancel.sum_conv, Real_Cancel.rel_conv]; *} -lemma real_minus_diff_eq [simp]: "- (z - y) = y - (z::real)" -by simp - - -subsection{*Theorems About the Ordering*} - -lemma real_gt_zero_preal_Ex: "(0 < x) = (\y. x = real_of_preal y)" -apply (auto simp add: real_of_preal_zero_less) -apply (cut_tac x = x in real_of_preal_trichotomy) -apply (blast elim!: real_less_irrefl real_of_preal_not_minus_gt_zero [THEN notE]) -done - -lemma real_gt_preal_preal_Ex: "real_of_preal z < x ==> \y. x = real_of_preal y" -by (blast dest!: real_of_preal_zero_less [THEN real_less_trans] - intro: real_gt_zero_preal_Ex [THEN iffD1]) - -lemma real_ge_preal_preal_Ex: "real_of_preal z \ x ==> \y. x = real_of_preal y" -by (blast dest: order_le_imp_less_or_eq real_gt_preal_preal_Ex) - -lemma real_less_all_preal: "y \ 0 ==> \x. y < real_of_preal x" -by (auto elim: order_le_imp_less_or_eq [THEN disjE] - intro: real_of_preal_zero_less [THEN [2] real_less_trans] - simp add: real_of_preal_zero_less) - -lemma real_less_all_real2: "~ 0 < y ==> \x. y < real_of_preal x" -by (blast intro!: real_less_all_preal real_leI) - -lemma real_of_preal_le_iff: "(real_of_preal m1 \ real_of_preal m2) = (m1 \ m2)" -apply (auto intro!: preal_leI simp add: real_less_le_iff [symmetric]) -apply (drule order_le_less_trans, assumption) -apply (erule preal_less_irrefl) -done - -subsection{*Monotonicity of Addition*} - -lemma real_add_right_cancel_less [simp]: "(v+z < w+z) = (v < (w::real))" -by simp - -lemma real_add_left_cancel_less [simp]: "(z+v < z+w) = (v < (w::real))" -by simp - -lemma real_add_right_cancel_le [simp]: "(v+z \ w+z) = (v \ (w::real))" -by simp - -lemma real_add_left_cancel_le [simp]: "(z+v \ z+w) = (v \ (w::real))" -by simp - -lemma real_mult_order: "[| 0 < x; 0 < y |] ==> (0::real) < x * y" -apply (auto simp add: real_gt_zero_preal_Ex) -apply (rule_tac x = "y*ya" in exI) -apply (simp (no_asm_use) add: real_of_preal_mult) -done - -lemma real_mult_less_mono2: "[| (0::real) < z; x < y |] ==> z * x < z * y" -apply (rule real_sum_gt_zero_less) -apply (drule real_less_sum_gt_zero [of x y]) -apply (drule real_mult_order, assumption) -apply (simp add: real_add_mult_distrib2) -done - - -subsection{*The Reals Form an Ordered Field*} - -instance real :: inverse .. - -instance real :: ordered_field -proof - fix x y z :: real - show "(x + y) + z = x + (y + z)" by (rule real_add_assoc) - show "x + y = y + x" by (rule real_add_commute) - show "0 + x = x" by simp - show "- x + x = 0" by simp - show "x - y = x + (-y)" by (simp add: real_diff_def) - show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc) - show "x * y = y * x" by (rule real_mult_commute) - show "1 * x = x" by simp - show "(x + y) * z = x * z + y * z" by (simp add: real_add_mult_distrib) - show "0 \ (1::real)" by (rule real_zero_not_eq_one) - show "x \ y ==> z + x \ z + y" by simp - show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: real_mult_less_mono2) - show "\x\ = (if x < 0 then -x else x)" - by (auto dest: order_le_less_trans simp add: real_abs_def linorder_not_le) - show "x \ 0 ==> inverse x * x = 1" by simp - show "y \ 0 ==> x / y = x * inverse y" by (simp add: real_divide_def) -qed - -(*"v\w ==> v+z \ w+z"*) -lemmas real_add_less_mono1 = real_add_right_cancel_less [THEN iffD2, standard] - -(*"v\w ==> v+z \ w+z"*) -lemmas real_add_le_mono1 = real_add_right_cancel_le [THEN iffD2, standard] - -lemma real_add_less_le_mono: "!!z z'::real. [| w'z |] ==> w' + z' < w + z" -by (erule real_add_less_mono1 [THEN order_less_le_trans], simp) - -lemma real_add_le_less_mono: "!!z z'::real. [| w'\w; z' w' + z' < w + z" -by (erule real_add_le_mono1 [THEN order_le_less_trans], simp) - -lemma real_add_less_mono2: "!!(A::real). A < B ==> C + A < C + B" -by simp - -lemma real_less_add_right_cancel: "!!(A::real). A + C < B + C ==> A < B" -apply simp -done - -lemma real_less_add_left_cancel: "!!(A::real). C + A < C + B ==> A < B" -apply simp -done - -lemma real_le_add_right_cancel: "!!(A::real). A + C \ B + C ==> A \ B" -apply simp -done - -lemma real_le_add_left_cancel: "!!(A::real). C + A \ C + B ==> A \ B" -apply simp -done - -lemma real_zero_less_one: "0 < (1::real)" - by (rule Ring_and_Field.zero_less_one) - -lemma real_add_less_mono: "[| R1 < S1; R2 < S2 |] ==> R1+R2 < S1+(S2::real)" - by (rule Ring_and_Field.add_strict_mono) - -lemma real_add_left_le_mono1: "!!(q1::real). q1 \ q2 ==> x + q1 \ x + q2" -by simp - -lemma real_add_le_mono: "[|i\j; k\l |] ==> i + k \ j + (l::real)" - by (rule Ring_and_Field.add_mono) - -lemma real_le_minus_iff: "(-s \ -r) = ((r::real) \ s)" - by (rule Ring_and_Field.neg_le_iff_le) - -lemma real_le_square [simp]: "(0::real) \ x*x" - by (rule Ring_and_Field.zero_le_square) - - -subsection{*Division Lemmas*} - -(** Inverse of zero! Useful to simplify certain equations **) - -lemma INVERSE_ZERO [simp]: "inverse 0 = (0::real)" -apply (unfold real_inverse_def) -apply (rule someI2) -apply (auto simp add: real_zero_not_eq_one) -done - -lemma DIVISION_BY_ZERO [simp]: "a / (0::real) = 0" -by (simp add: real_divide_def INVERSE_ZERO) - -lemma real_mult_left_cancel: "(c::real) ~= 0 ==> (c*a=c*b) = (a=b)" -apply auto -done - -lemma real_mult_right_cancel: "(c::real) ~= 0 ==> (a*c=b*c) = (a=b)" -apply (auto ); -done - -lemma real_mult_left_cancel_ccontr: "c*a ~= c*b ==> a ~= b" -by auto - -lemma real_mult_right_cancel_ccontr: "a*c ~= b*c ==> a ~= b" -by auto - -lemma real_inverse_not_zero: "x ~= 0 ==> inverse(x::real) ~= 0" - by (rule Ring_and_Field.nonzero_imp_inverse_nonzero) - -lemma real_mult_not_zero: "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::real)" -apply (simp add: ); -done - -lemma real_inverse_inverse: "inverse(inverse (x::real)) = x" -apply (case_tac "x=0", simp) -apply (rule_tac c1 = "inverse x" in real_mult_right_cancel [THEN iffD1]) -apply (erule real_inverse_not_zero) -apply (auto dest: real_inverse_not_zero) -done -declare real_inverse_inverse [simp] - -lemma real_inverse_1: "inverse((1::real)) = (1::real)" -apply (unfold real_inverse_def) -apply (cut_tac real_zero_not_eq_one [THEN not_sym, THEN real_mult_inv_left_ex]) -apply (auto simp add: real_zero_not_eq_one [THEN not_sym]) -done -declare real_inverse_1 [simp] - -lemma real_minus_inverse: "inverse(-x) = -inverse(x::real)" -apply (case_tac "x=0", simp) -apply (rule_tac c1 = "-x" in real_mult_right_cancel [THEN iffD1]) - prefer 2 apply (subst real_mult_inv_left, auto) -done - -lemma real_inverse_distrib: "inverse(x*y) = inverse(x)*inverse(y::real)" -apply (case_tac "x=0", simp) -apply (case_tac "y=0", simp) -apply (frule_tac y = y in real_mult_not_zero, assumption) -apply (rule_tac c1 = x in real_mult_left_cancel [THEN iffD1]) -apply (auto simp add: real_mult_assoc [symmetric]) -apply (rule_tac c1 = y in real_mult_left_cancel [THEN iffD1]) -apply (auto simp add: real_mult_left_commute) -apply (simp add: real_mult_assoc [symmetric]) -done - -lemma real_times_divide1_eq: "(x::real) * (y/z) = (x*y)/z" -by (simp add: real_divide_def real_mult_assoc) - -lemma real_times_divide2_eq: "(y/z) * (x::real) = (y*x)/z" -by (simp add: real_divide_def real_mult_ac) - -declare real_times_divide1_eq [simp] real_times_divide2_eq [simp] - -lemma real_divide_divide1_eq: "(x::real) / (y/z) = (x*z)/y" -by (simp add: real_divide_def real_inverse_distrib real_mult_ac) - -lemma real_divide_divide2_eq: "((x::real) / y) / z = x/(y*z)" -by (simp add: real_divide_def real_inverse_distrib real_mult_assoc) - -declare real_divide_divide1_eq [simp] real_divide_divide2_eq [simp] - -(** As with multiplication, pull minus signs OUT of the / operator **) - -lemma real_minus_divide_eq: "(-x) / (y::real) = - (x/y)" -by (simp add: real_divide_def) -declare real_minus_divide_eq [simp] - -lemma real_divide_minus_eq: "(x / -(y::real)) = - (x/y)" -by (simp add: real_divide_def real_minus_inverse) -declare real_divide_minus_eq [simp] - -lemma real_add_divide_distrib: "(x+y)/(z::real) = x/z + y/z" -by (simp add: real_divide_def real_add_mult_distrib) - -(*The following would e.g. convert (x+y)/2 to x/2 + y/2. Sometimes that - leads to cancellations in x or y, but is also prevents "multiplying out" - the 2 in e.g. (x+y)/2 = 5. - -Addsimps [inst "z" "number_of ?w" real_add_divide_distrib] -**) - - subsection{*An Embedding of the Naturals in the Reals*} @@ -356,7 +506,7 @@ lemma real_of_nat_add [simp]: "real (m + n) = real (m::nat) + real n" -apply (simp add: real_of_nat_def real_add_assoc) +apply (simp add: real_of_nat_def add_ac) apply (simp add: real_of_posnat_add real_add_assoc [symmetric]) done @@ -409,20 +559,11 @@ qed lemma real_of_nat_neg_int [simp]: "neg z ==> real (nat z) = 0" -apply (simp add: neg_nat real_of_nat_zero) -done +by (simp add: neg_nat real_of_nat_zero) subsection{*Inverse and Division*} -instance real :: division_by_zero -proof - fix x :: real - show "inverse 0 = (0::real)" by (rule INVERSE_ZERO) - show "x/0 = 0" by (rule DIVISION_BY_ZERO) -qed - - lemma real_inverse_gt_0: "0 < x ==> 0 < inverse (x::real)" by (rule Ring_and_Field.inverse_gt_0) @@ -483,8 +624,8 @@ done lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)" -apply (drule real_add_minus_eq_minus) -apply (cut_tac x = x in real_le_square) +apply (drule Ring_and_Field.equals_zero_I [THEN sym]) +apply (cut_tac x = y in real_le_square) apply (auto, drule real_le_anti_sym, auto) done @@ -510,10 +651,12 @@ subsection{*Hardly Used Theorems to be Deleted*} +lemma real_add_less_mono2: "!!(A::real). A < B ==> C + A < C + B" +by simp + lemma real_add_order: "[| 0 < x; 0 < y |] ==> (0::real) < x + y" apply (erule order_less_trans) -apply (drule real_add_less_mono2) -apply simp +apply (drule real_add_less_mono2, simp) done lemma real_le_add_order: "[| 0 \ x; 0 \ y |] ==> (0::real) \ x + y" @@ -531,8 +674,7 @@ lemma real_of_posnat_gt_zero: "0 < real_of_posnat n" apply (unfold real_of_posnat_def) -apply (rule real_gt_zero_preal_Ex [THEN iffD2]) -apply blast +apply (rule real_gt_zero_preal_Ex [THEN iffD2], blast) done declare real_of_posnat_gt_zero [simp] @@ -544,8 +686,7 @@ declare real_of_posnat_ge_zero [simp] lemma real_of_posnat_not_eq_zero: "real_of_posnat n ~= 0" -apply (rule real_of_posnat_gt_zero [THEN real_not_refl2, THEN not_sym]) -done +by (rule real_of_posnat_gt_zero [THEN real_not_refl2, THEN not_sym]) declare real_of_posnat_not_eq_zero [simp] declare real_of_posnat_not_eq_zero [THEN real_mult_inv_left, simp] @@ -580,14 +721,14 @@ lemma real_of_posnat_inv_Ex_iff: "(EX n. inverse(real_of_posnat n) < r) = (EX n. 1 < r * real_of_posnat n)" apply safe -apply (drule_tac n1 = "n" in real_of_posnat_gt_zero [THEN real_mult_less_mono1]) +apply (drule_tac n1 = n in real_of_posnat_gt_zero [THEN real_mult_less_mono1]) apply (drule_tac [2] n2=n in real_of_posnat_gt_zero [THEN real_inverse_gt_0, THEN real_mult_less_mono1]) apply (auto simp add: real_of_posnat_gt_zero [THEN real_not_refl2, THEN not_sym] real_mult_assoc) done lemma real_of_posnat_inv_iff: "(inverse(real_of_posnat n) < r) = (1 < r * real_of_posnat n)" apply safe -apply (drule_tac n1 = "n" in real_of_posnat_gt_zero [THEN real_mult_less_mono1]) +apply (drule_tac n1 = n in real_of_posnat_gt_zero [THEN real_mult_less_mono1]) apply (drule_tac [2] n2=n in real_of_posnat_gt_zero [THEN real_inverse_gt_0, THEN real_mult_less_mono1]) apply (auto simp add: real_mult_assoc) done @@ -607,37 +748,32 @@ lemma real_of_posnat_less_iff: "(real_of_posnat n < real_of_posnat m) = (n < m)" -apply (unfold real_of_posnat_def) -apply auto +apply (unfold real_of_posnat_def, auto) done declare real_of_posnat_less_iff [simp] lemma real_of_posnat_le_iff: "(real_of_posnat n <= real_of_posnat m) = (n <= m)" -apply (auto dest: inj_real_of_posnat [THEN injD] simp add: real_le_less le_eq_less_or_eq) -done +by (auto dest: inj_real_of_posnat [THEN injD] simp add: real_le_less le_eq_less_or_eq) declare real_of_posnat_le_iff [simp] lemma real_mult_less_cancel3: "[| (0::real) x x (u < inverse (real_of_posnat n)) = (real_of_posnat n < inverse(u))" apply safe apply (rule_tac n2=n in real_of_posnat_gt_zero [THEN real_inverse_gt_0, THEN real_mult_less_cancel3]) -apply (rule_tac [2] x1 = "u" in real_inverse_gt_0 [THEN real_mult_less_cancel3]) +apply (rule_tac [2] x1 = u in real_inverse_gt_0 [THEN real_mult_less_cancel3]) apply (auto simp add: real_not_refl2 [THEN not_sym]) -apply (rule_tac z = "u" in real_mult_less_cancel4) -apply (rule_tac [3] n1 = "n" in real_of_posnat_gt_zero [THEN real_mult_less_cancel4]) +apply (rule_tac z = u in real_mult_less_cancel4) +apply (rule_tac [3] n1 = n in real_of_posnat_gt_zero [THEN real_mult_less_cancel4]) apply (auto simp add: real_not_refl2 [THEN not_sym] real_mult_assoc [symmetric]) done lemma real_of_posnat_inv_eq_iff: "0 < u ==> (u = inverse(real_of_posnat n)) = (real_of_posnat n = inverse u)" -apply auto -done +by auto lemma real_add_one_minus_inv_ge_zero: "0 <= 1 + -inverse(real_of_posnat n)" apply (rule_tac C = "inverse (real_of_posnat n) " in real_le_add_right_cancel) @@ -645,30 +781,23 @@ done lemma real_mult_add_one_minus_ge_zero: "0 < r ==> 0 <= r*(1 + -inverse(real_of_posnat n))" -apply (drule real_add_one_minus_inv_ge_zero [THEN real_mult_le_less_mono1]) -apply auto -done +by (drule real_add_one_minus_inv_ge_zero [THEN real_mult_le_less_mono1], auto) lemma real_inverse_unique: "x*y = (1::real) ==> y = inverse x" apply (case_tac "x ~= 0") -apply (rule_tac c1 = "x" in real_mult_left_cancel [THEN iffD1]) -apply auto +apply (rule_tac c1 = x in real_mult_left_cancel [THEN iffD1], auto) done lemma real_inverse_gt_one: "[| (0::real) < x; x < 1 |] ==> 1 < inverse x" -apply (auto dest: real_inverse_less_swap) -done +by (auto dest: real_inverse_less_swap) lemma real_of_nat_gt_zero_cancel_iff: "(0 < real (n::nat)) = (0 < n)" -apply (rule real_of_nat_less_iff [THEN subst]) -apply auto -done +by (rule real_of_nat_less_iff [THEN subst], auto) declare real_of_nat_gt_zero_cancel_iff [simp] lemma real_of_nat_le_zero_cancel_iff: "(real (n::nat) <= 0) = (n = 0)" apply (rule real_of_nat_zero [THEN subst]) -apply (subst real_of_nat_le_iff) -apply auto +apply (subst real_of_nat_le_iff, auto) done declare real_of_nat_le_zero_cancel_iff [simp] @@ -689,19 +818,98 @@ apply (auto simp add: real_of_nat_Suc) done -(*RING AND FIELD*) - lemma mult_less_imp_less_left: - "[|c*a < c*b; 0 < c|] ==> a < (b::'a::ordered_ring)" - by (force elim: order_less_asym simp add: mult_less_cancel_left) - - lemma mult_less_imp_less_right: - "[|a*c < b*c; 0 < c|] ==> a < (b::'a::ordered_ring)" - by (force elim: order_less_asym simp add: mult_less_cancel_right) - ML {* val real_abs_def = thm "real_abs_def"; +val real_less_eq_diff = thm "real_less_eq_diff"; + +val real_add_right_cancel = thm"real_add_right_cancel"; +val real_mult_congruent2_lemma = thm"real_mult_congruent2_lemma"; +val real_mult_congruent2 = thm"real_mult_congruent2"; +val real_mult = thm"real_mult"; +val real_mult_commute = thm"real_mult_commute"; +val real_mult_assoc = thm"real_mult_assoc"; +val real_mult_left_commute = thm"real_mult_left_commute"; +val real_mult_1 = thm"real_mult_1"; +val real_mult_1_right = thm"real_mult_1_right"; +val real_mult_0 = thm"real_mult_0"; +val real_mult_0_right = thm"real_mult_0_right"; +val real_mult_minus_eq1 = thm"real_mult_minus_eq1"; +val real_minus_mult_eq1 = thm"real_minus_mult_eq1"; +val real_mult_minus_eq2 = thm"real_mult_minus_eq2"; +val real_minus_mult_eq2 = thm"real_minus_mult_eq2"; +val real_mult_minus_1 = thm"real_mult_minus_1"; +val real_mult_minus_1_right = thm"real_mult_minus_1_right"; +val real_minus_mult_cancel = thm"real_minus_mult_cancel"; +val real_minus_mult_commute = thm"real_minus_mult_commute"; +val real_add_assoc_cong = thm"real_add_assoc_cong"; +val real_add_mult_distrib = thm"real_add_mult_distrib"; +val real_add_mult_distrib2 = thm"real_add_mult_distrib2"; +val real_diff_mult_distrib = thm"real_diff_mult_distrib"; +val real_diff_mult_distrib2 = thm"real_diff_mult_distrib2"; +val real_zero_not_eq_one = thm"real_zero_not_eq_one"; +val real_zero_iff = thm"real_zero_iff"; +val preal_le_linear = thm"preal_le_linear"; +val real_mult_inv_right_ex = thm"real_mult_inv_right_ex"; +val real_mult_inv_left_ex = thm"real_mult_inv_left_ex"; +val real_mult_inv_left = thm"real_mult_inv_left"; +val real_mult_inv_right = thm"real_mult_inv_right"; +val preal_lemma_eq_rev_sum = thm"preal_lemma_eq_rev_sum"; +val preal_add_left_commute_cancel = thm"preal_add_left_commute_cancel"; +val preal_lemma_for_not_refl = thm"preal_lemma_for_not_refl"; +val real_less_not_refl = thm"real_less_not_refl"; +val real_less_irrefl = thm"real_less_irrefl"; +val real_not_refl2 = thm"real_not_refl2"; +val preal_lemma_trans = thm"preal_lemma_trans"; +val real_less_trans = thm"real_less_trans"; +val real_less_not_sym = thm"real_less_not_sym"; +val real_less_asym = thm"real_less_asym"; +val real_of_preal_add = thm"real_of_preal_add"; +val real_of_preal_mult = thm"real_of_preal_mult"; +val real_of_preal_ExI = thm"real_of_preal_ExI"; +val real_of_preal_ExD = thm"real_of_preal_ExD"; +val real_of_preal_iff = thm"real_of_preal_iff"; +val real_of_preal_trichotomy = thm"real_of_preal_trichotomy"; +val real_of_preal_trichotomyE = thm"real_of_preal_trichotomyE"; +val real_of_preal_lessD = thm"real_of_preal_lessD"; +val real_of_preal_lessI = thm"real_of_preal_lessI"; +val real_of_preal_less_iff1 = thm"real_of_preal_less_iff1"; +val real_of_preal_minus_less_self = thm"real_of_preal_minus_less_self"; +val real_of_preal_minus_less_zero = thm"real_of_preal_minus_less_zero"; +val real_of_preal_not_minus_gt_zero = thm"real_of_preal_not_minus_gt_zero"; +val real_of_preal_zero_less = thm"real_of_preal_zero_less"; +val real_of_preal_not_less_zero = thm"real_of_preal_not_less_zero"; +val real_minus_minus_zero_less = thm"real_minus_minus_zero_less"; +val real_of_preal_sum_zero_less = thm"real_of_preal_sum_zero_less"; +val real_of_preal_minus_less_all = thm"real_of_preal_minus_less_all"; +val real_of_preal_not_minus_gt_all = thm"real_of_preal_not_minus_gt_all"; +val real_of_preal_minus_less_rev1 = thm"real_of_preal_minus_less_rev1"; +val real_of_preal_minus_less_rev2 = thm"real_of_preal_minus_less_rev2"; +val real_of_preal_minus_less_rev_iff = thm"real_of_preal_minus_less_rev_iff"; +val real_linear = thm"real_linear"; +val real_neq_iff = thm"real_neq_iff"; +val real_linear_less2 = thm"real_linear_less2"; +val real_leI = thm"real_leI"; +val real_leD = thm"real_leD"; +val real_leE = thm"real_leE"; +val real_less_le_iff = thm"real_less_le_iff"; +val not_real_leE = thm"not_real_leE"; +val real_le_imp_less_or_eq = thm"real_le_imp_less_or_eq"; +val real_less_or_eq_imp_le = thm"real_less_or_eq_imp_le"; +val real_le_less = thm"real_le_less"; +val real_le_refl = thm"real_le_refl"; +val real_le_linear = thm"real_le_linear"; +val real_le_trans = thm"real_le_trans"; +val real_le_anti_sym = thm"real_le_anti_sym"; +val real_less_le = thm"real_less_le"; +val real_minus_zero_less_iff = thm"real_minus_zero_less_iff"; +val real_minus_zero_less_iff2 = thm"real_minus_zero_less_iff2"; +val real_less_add_positive_left_Ex = thm"real_less_add_positive_left_Ex"; +val real_less_sum_gt_zero = thm"real_less_sum_gt_zero"; +val real_sum_gt_zero_less = thm"real_sum_gt_zero_less"; +val real_less_sum_gt_0_iff = thm"real_less_sum_gt_0_iff"; + val real_minus_diff_eq = thm "real_minus_diff_eq"; val real_gt_zero_preal_Ex = thm "real_gt_zero_preal_Ex"; val real_gt_preal_preal_Ex = thm "real_gt_preal_preal_Ex"; @@ -727,7 +935,6 @@ val real_add_order = thm "real_add_order"; val real_le_add_order = thm "real_le_add_order"; val real_add_less_mono = thm "real_add_less_mono"; -val real_add_left_le_mono1 = thm "real_add_left_le_mono1"; val real_add_le_mono = thm "real_add_le_mono"; val real_le_minus_iff = thm "real_le_minus_iff"; val real_le_square = thm "real_le_square"; @@ -820,6 +1027,13 @@ val real_minus_divide_eq = thm"real_minus_divide_eq"; val real_divide_minus_eq = thm"real_divide_minus_eq"; val real_add_divide_distrib = thm"real_add_divide_distrib"; + +val diff_less_eq = thm"diff_less_eq"; +val less_diff_eq = thm"less_diff_eq"; +val diff_eq_eq = thm"diff_eq_eq"; +val diff_le_eq = thm"diff_le_eq"; +val le_diff_eq = thm"le_diff_eq"; +val compare_rls = thms "compare_rls"; *} end diff -r 502a7c95de73 -r 342451d763f9 src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Fri Nov 28 12:09:37 2003 +0100 +++ b/src/HOL/Ring_and_Field.thy Tue Dec 02 11:48:15 2003 +0100 @@ -50,7 +50,7 @@ divide_zero [simp]: "a / 0 = 0" -subsection {* Derived rules for addition *} +subsection {* Derived Rules for Addition *} lemma right_zero [simp]: "a + 0 = (a::'a::semiring)" proof - @@ -81,9 +81,6 @@ thus "a - b = 0" by (simp add: diff_minus) qed -lemma diff_self [simp]: "a - (a::'a::ring) = 0" - by (simp add: diff_minus) - lemma add_left_cancel [simp]: "(a + b = a + c) = (b = (c::'a::ring))" proof @@ -114,6 +111,15 @@ lemma minus_zero [simp]: "- 0 = (0::'a::ring)" by (simp add: equals_zero_I) +lemma diff_self [simp]: "a - (a::'a::ring) = 0" + by (simp add: diff_minus) + +lemma diff_0 [simp]: "(0::'a::ring) - a = -a" +by (simp add: diff_minus) + +lemma diff_0_right [simp]: "a - (0::'a::ring) = a" +by (simp add: diff_minus) + lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::ring))" proof assume "- a = - b" @@ -147,7 +153,7 @@ theorems mult_ac = mult_assoc mult_commute mult_left_commute lemma right_inverse [simp]: - assumes not0: "a ~= 0" shows "a * inverse (a::'a::field) = 1" + assumes not0: "a \ 0" shows "a * inverse (a::'a::field) = 1" proof - have "a * inverse a = inverse a * a" by (simp add: mult_ac) also have "... = 1" using not0 by simp @@ -215,8 +221,11 @@ by (simp add: right_distrib diff_minus minus_mult_left [symmetric] minus_mult_right [symmetric]) +lemma minus_diff_eq [simp]: "- (a - b) = b - (a::'a::ring)" +by (simp add: diff_minus add_commute) -subsection {* Ordering rules *} + +subsection {* Ordering Rules for Addition *} lemma add_right_mono: "a \ (b::'a::ordered_semiring) ==> a + c \ b + c" by (simp add: add_commute [of _ c] add_left_mono) @@ -241,6 +250,47 @@ apply (erule add_strict_left_mono) done +lemma add_less_imp_less_left: + assumes less: "c + a < c + b" shows "a < (b::'a::ordered_ring)" + proof - + have "-c + (c + a) < -c + (c + b)" + by (rule add_strict_left_mono [OF less]) + thus "a < b" by (simp add: add_assoc [symmetric]) + qed + +lemma add_less_imp_less_right: + "a + c < b + c ==> a < (b::'a::ordered_ring)" +apply (rule add_less_imp_less_left [of c]) +apply (simp add: add_commute) +done + +lemma add_less_cancel_left [simp]: + "(c+a < c+b) = (a < (b::'a::ordered_ring))" +by (blast intro: add_less_imp_less_left add_strict_left_mono) + +lemma add_less_cancel_right [simp]: + "(a+c < b+c) = (a < (b::'a::ordered_ring))" +by (blast intro: add_less_imp_less_right add_strict_right_mono) + +lemma add_le_cancel_left [simp]: + "(c+a \ c+b) = (a \ (b::'a::ordered_ring))" +by (simp add: linorder_not_less [symmetric]) + +lemma add_le_cancel_right [simp]: + "(a+c \ b+c) = (a \ (b::'a::ordered_ring))" +by (simp add: linorder_not_less [symmetric]) + +lemma add_le_imp_le_left: + "c + a \ c + b ==> a \ (b::'a::ordered_ring)" +by simp + +lemma add_le_imp_le_right: + "a + c \ b + c ==> a \ (b::'a::ordered_ring)" +by simp + + +subsection {* Ordering Rules for Unary Minus *} + lemma le_imp_neg_le: assumes "a \ (b::'a::ordered_ring)" shows "-b \ -a" proof - @@ -280,6 +330,67 @@ lemma neg_0_less_iff_less [simp]: "(0 < -a) = (a < (0::'a::ordered_ring))" by (subst neg_less_iff_less [symmetric], simp) + +subsection{*Subtraction Laws*} + +lemma add_diff_eq: "a + (b - c) = (a + b) - (c::'a::ring)" +by (simp add: diff_minus add_ac) + +lemma diff_add_eq: "(a - b) + c = (a + c) - (b::'a::ring)" +by (simp add: diff_minus add_ac) + +lemma diff_eq_eq: "(a-b = c) = (a = c + (b::'a::ring))" +by (auto simp add: diff_minus add_assoc) + +lemma eq_diff_eq: "(a = c-b) = (a + (b::'a::ring) = c)" +by (auto simp add: diff_minus add_assoc) + +lemma diff_diff_eq: "(a - b) - c = a - (b + (c::'a::ring))" +by (simp add: diff_minus add_ac) + +lemma diff_diff_eq2: "a - (b - c) = (a + c) - (b::'a::ring)" +by (simp add: diff_minus add_ac) + +text{*Further subtraction laws for ordered rings*} + +lemma less_eq_diff: "(a < b) = (a - b < (0::'a::ordered_ring))" +proof - + have "(a < b) = (a + (- b) < b + (-b))" + by (simp only: add_less_cancel_right) + also have "... = (a - b < 0)" by (simp add: diff_minus) + finally show ?thesis . +qed + +lemma diff_less_eq: "(a-b < c) = (a < c + (b::'a::ordered_ring))" +apply (subst less_eq_diff) +apply (rule less_eq_diff [of _ c, THEN ssubst]) +apply (simp add: diff_minus add_ac) +done + +lemma less_diff_eq: "(a < c-b) = (a + (b::'a::ordered_ring) < c)" +apply (subst less_eq_diff) +apply (rule less_eq_diff [of _ "c-b", THEN ssubst]) +apply (simp add: diff_minus add_ac) +done + +lemma diff_le_eq: "(a-b \ c) = (a \ c + (b::'a::ordered_ring))" +by (simp add: linorder_not_less [symmetric] less_diff_eq) + +lemma le_diff_eq: "(a \ c-b) = (a + (b::'a::ordered_ring) \ c)" +by (simp add: linorder_not_less [symmetric] diff_less_eq) + +text{*This list of rewrites simplifies (in)equalities by bringing subtractions + to the top and then moving negative terms to the other side. + Use with @{text add_ac}*} +lemmas compare_rls = + diff_minus [symmetric] + add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2 + diff_less_eq less_diff_eq diff_le_eq le_diff_eq + diff_eq_eq eq_diff_eq + + +subsection {* Ordering Rules for Multiplication *} + lemma mult_strict_right_mono: "[|a < b; 0 < c|] ==> a * c < b * (c::'a::ordered_semiring)" by (simp add: mult_commute [of _ c] mult_strict_left_mono) @@ -484,6 +595,21 @@ subsection {* Fields *} +text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement + of an ordering.*} +lemma field_mult_eq_0_iff: "(a*b = (0::'a::field)) = (a = 0 | b = 0)" + proof cases + assume "a=0" thus ?thesis by simp + next + assume anz [simp]: "a\0" + thus ?thesis + proof auto + assume "a * b = 0" + hence "inverse a * (a * b) = 0" by simp + thus "b = 0" by (simp (no_asm_use) add: mult_assoc [symmetric]) + qed + qed + text{*Cancellation of equalities with a common factor*} lemma field_mult_cancel_right_lemma: assumes cnz: "c \ (0::'a::field)" @@ -578,6 +704,67 @@ "(inverse a = inverse b) = (a = (b::'a::{field,division_by_zero}))" by (force dest!: inverse_eq_imp_eq) +lemma nonzero_inverse_inverse_eq: + assumes [simp]: "a \ 0" shows "inverse(inverse (a::'a::field)) = a" + proof - + have "(inverse (inverse a) * inverse a) * a = a" + by (simp add: nonzero_imp_inverse_nonzero) + thus ?thesis + by (simp add: mult_assoc) + qed + +lemma inverse_inverse_eq [simp]: + "inverse(inverse (a::'a::{field,division_by_zero})) = a" + proof cases + assume "a=0" thus ?thesis by simp + next + assume "a\0" + thus ?thesis by (simp add: nonzero_inverse_inverse_eq) + qed + +lemma inverse_1 [simp]: "inverse 1 = (1::'a::field)" + proof - + have "inverse 1 * 1 = (1::'a::field)" + by (rule left_inverse [OF zero_neq_one [symmetric]]) + thus ?thesis by simp + qed + +lemma nonzero_inverse_mult_distrib: + assumes anz: "a \ 0" + and bnz: "b \ 0" + shows "inverse(a*b) = inverse(b) * inverse(a::'a::field)" + proof - + have "inverse(a*b) * (a * b) * inverse(b) = inverse(b)" + by (simp add: field_mult_eq_0_iff anz bnz) + hence "inverse(a*b) * a = inverse(b)" + by (simp add: mult_assoc bnz) + hence "inverse(a*b) * a * inverse(a) = inverse(b) * inverse(a)" + by simp + thus ?thesis + by (simp add: mult_assoc anz) + qed + +text{*This version builds in division by zero while also re-orienting + the right-hand side.*} +lemma inverse_mult_distrib [simp]: + "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})" + proof cases + assume "a \ 0 & b \ 0" + thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_commute) + next + assume "~ (a \ 0 & b \ 0)" + thus ?thesis by force + qed + +text{*There is no slick version using division by zero.*} +lemma inverse_add: + "[|a \ 0; b \ 0|] + ==> inverse a + inverse b = (a+b) * inverse a * inverse (b::'a::field)" +apply (simp add: left_distrib mult_assoc) +apply (simp add: mult_commute [of "inverse a"]) +apply (simp add: mult_assoc [symmetric] add_commute) +done + subsection {* Ordered Fields *}