# HG changeset patch # User paulson # Date 1071502705 -3600 # Node ID 7f115e5c5de4d4d0a8a5039e788a658e93eb460c # Parent f4d806fd72ced144042d764b310159118845c2f1 more general lemmas for Ring_and_Field diff -r f4d806fd72ce -r 7f115e5c5de4 doc-src/TutorialI/Types/Numbers.thy --- a/doc-src/TutorialI/Types/Numbers.thy Sat Dec 13 09:33:52 2003 +0100 +++ b/doc-src/TutorialI/Types/Numbers.thy Mon Dec 15 16:38:25 2003 +0100 @@ -200,8 +200,8 @@ @{thm[display] realpow_abs[no_vars]} \rulename{realpow_abs} -@{thm[display] real_dense[no_vars]} -\rulename{real_dense} +@{thm[display] dense[no_vars]} +\rulename{dense} @{thm[display] realpow_abs[no_vars]} \rulename{realpow_abs} @@ -218,16 +218,16 @@ @{thm[display] divide_divide_eq_left[no_vars]} \rulename{divide_divide_eq_left} -@{thm[display] real_minus_divide_eq[no_vars]} -\rulename{real_minus_divide_eq} +@{thm[display] minus_divide_left[no_vars]} +\rulename{minus_divide_left} -@{thm[display] real_divide_minus_eq[no_vars]} -\rulename{real_divide_minus_eq} +@{thm[display] minus_divide_right[no_vars]} +\rulename{minus_divide_right} This last NOT a simprule -@{thm[display] real_add_divide_distrib[no_vars]} -\rulename{real_add_divide_distrib} +@{thm[display] add_divide_distrib[no_vars]} +\rulename{add_divide_distrib} *} lemma "3/4 < (7/8 :: real)" diff -r f4d806fd72ce -r 7f115e5c5de4 doc-src/TutorialI/Types/document/Numbers.tex --- a/doc-src/TutorialI/Types/document/Numbers.tex Sat Dec 13 09:33:52 2003 +0100 +++ b/doc-src/TutorialI/Types/document/Numbers.tex Mon Dec 15 16:38:25 2003 +0100 @@ -277,7 +277,7 @@ \rulename{zmod_zmult2_eq} \begin{isabelle}% -{\isasymbar}x\ {\isacharasterisk}\ y{\isasymbar}\ {\isacharequal}\ {\isasymbar}x{\isasymbar}\ {\isacharasterisk}\ {\isasymbar}y{\isasymbar}% +{\isasymbar}a\ {\isacharasterisk}\ b{\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\ {\isacharasterisk}\ {\isasymbar}b{\isasymbar}% \end{isabelle} \rulename{abs_mult}% \end{isamarkuptext}% @@ -325,9 +325,9 @@ \rulename{realpow_abs} \begin{isabelle}% -x\ {\isacharless}\ y\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachardot}\ x\ {\isacharless}\ r\ {\isasymand}\ r\ {\isacharless}\ y% +a\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachardot}\ a\ {\isacharless}\ r\ {\isasymand}\ r\ {\isacharless}\ b% \end{isabelle} -\rulename{real_dense} +\rulename{dense} \begin{isabelle}% {\isasymbar}r\ {\isacharcircum}\ n{\isasymbar}\ {\isacharequal}\ {\isasymbar}r{\isasymbar}\ {\isacharcircum}\ n% @@ -355,21 +355,21 @@ \rulename{divide_divide_eq_left} \begin{isabelle}% -{\isacharminus}\ x\ {\isacharslash}\ y\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}x\ {\isacharslash}\ y{\isacharparenright}% +{\isacharminus}\ {\isacharparenleft}a\ {\isacharslash}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharminus}\ a\ {\isacharslash}\ b% \end{isabelle} -\rulename{real_minus_divide_eq} +\rulename{minus_divide_left} \begin{isabelle}% -x\ {\isacharslash}\ {\isacharminus}\ y\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}x\ {\isacharslash}\ y{\isacharparenright}% +{\isacharminus}\ {\isacharparenleft}a\ {\isacharslash}\ b{\isacharparenright}\ {\isacharequal}\ a\ {\isacharslash}\ {\isacharminus}\ b% \end{isabelle} -\rulename{real_divide_minus_eq} +\rulename{minus_divide_right} This last NOT a simprule \begin{isabelle}% -{\isacharparenleft}x\ {\isacharplus}\ y{\isacharparenright}\ {\isacharslash}\ z\ {\isacharequal}\ x\ {\isacharslash}\ z\ {\isacharplus}\ y\ {\isacharslash}\ z% +{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharslash}\ c\ {\isacharequal}\ a\ {\isacharslash}\ c\ {\isacharplus}\ b\ {\isacharslash}\ c% \end{isabelle} -\rulename{real_add_divide_distrib}% +\rulename{add_divide_distrib}% \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}{\isadigit{3}}{\isacharslash}{\isadigit{4}}\ {\isacharless}\ {\isacharparenleft}{\isadigit{7}}{\isacharslash}{\isadigit{8}}\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequote}\isanewline diff -r f4d806fd72ce -r 7f115e5c5de4 doc-src/TutorialI/Types/numerics.tex --- a/doc-src/TutorialI/Types/numerics.tex Sat Dec 13 09:33:52 2003 +0100 +++ b/doc-src/TutorialI/Types/numerics.tex Mon Dec 15 16:38:25 2003 +0100 @@ -397,7 +397,7 @@ Density, however, is trivial to express: \begin{isabelle} x\ <\ y\ \isasymLongrightarrow \ \isasymexists r.\ x\ <\ r\ \isasymand \ r\ <\ y% -\rulename{real_dense} +\rulename{dense} \end{isabelle} Here is a selection of rules about the division operator. The following @@ -417,17 +417,17 @@ Signs are extracted from quotients in the hope that complementary terms can then be cancelled: \begin{isabelle} --\ x\ /\ y\ =\ -\ (x\ /\ y) -\rulename{real_minus_divide_eq}\isanewline -x\ /\ -\ y\ =\ -\ (x\ /\ y) -\rulename{real_divide_minus_eq} +-\ (a\ /\ b)\ =\ -\ a\ /\ b +\rulename{minus_divide_left}\isanewline +-\ (a\ /\ b)\ =\ a\ /\ -\ b +\rulename{minus_divide_right} \end{isabelle} The following distributive law is available, but it is not installed as a simplification rule. \begin{isabelle} -(x\ +\ y)\ /\ z\ =\ x\ /\ z\ +\ y\ /\ z% -\rulename{real_add_divide_distrib} +(a\ +\ b)\ /\ c\ =\ a\ /\ c\ +\ b\ /\ c% +\rulename{add_divide_distrib} \end{isabelle} As with the other numeric types, the simplifier can sort the operands of diff -r f4d806fd72ce -r 7f115e5c5de4 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sat Dec 13 09:33:52 2003 +0100 +++ b/src/HOL/HOL.thy Mon Dec 15 16:38:25 2003 +0100 @@ -645,6 +645,9 @@ "op <=" :: "['a::ord, 'a] => bool" ("(_/ \ _)" [50, 51] 50) +lemma Not_eq_iff: "((~P) = (~Q)) = (P = Q)" +by blast + subsubsection {* Monotonicity *} locale mono = @@ -716,6 +719,9 @@ apply (erule contrapos_np, simp) done +lemma order_eq_iff: "!!x::'a::order. (x = y) = (x \ y & y \ x)" +by (blast intro: order_antisym) + text {* Transitivity. *} diff -r f4d806fd72ce -r 7f115e5c5de4 src/HOL/Integ/IntArith.thy --- a/src/HOL/Integ/IntArith.thy Sat Dec 13 09:33:52 2003 +0100 +++ b/src/HOL/Integ/IntArith.thy Mon Dec 15 16:38:25 2003 +0100 @@ -93,7 +93,8 @@ but arith_tac is not parameterized by such simp rules *) -lemma zabs_split: "P(abs(i::int)) = ((0 \ i --> P i) & (i < 0 --> P(-i)))" +lemma zabs_split [arith_split]: + "P(abs(i::int)) = ((0 \ i --> P i) & (i < 0 --> P(-i)))" by (simp add: zabs_def) lemma zero_le_zabs [iff]: "0 \ abs (z::int)" @@ -104,8 +105,6 @@ z is an integer literal.*} declare int_eq_iff [of _ "number_of v", standard, simp] -declare zabs_split [arith_split] - lemma zabs_eq_iff: "(abs (z::int) = w) = (z = w \ 0 \ z \ z = -w \ z < 0)" by (auto simp add: zabs_def) @@ -113,7 +112,7 @@ lemma int_nat_eq [simp]: "int (nat z) = (if 0 \ z then z else 0)" by simp -lemma split_nat[arith_split]: +lemma split_nat [arith_split]: "P(nat(i::int)) = ((\n. i = int n \ P n) & (i < 0 \ P 0))" (is "?P = (?L & ?R)") proof (cases "i < 0") diff -r f4d806fd72ce -r 7f115e5c5de4 src/HOL/Real/RealArith.thy --- a/src/HOL/Real/RealArith.thy Sat Dec 13 09:33:52 2003 +0100 +++ b/src/HOL/Real/RealArith.thy Mon Dec 15 16:38:25 2003 +0100 @@ -76,14 +76,12 @@ subsection{*Absolute Value Function for the Reals*} -lemma abs_nat_number_of: +lemma abs_nat_number_of [simp]: "abs (number_of v :: real) = (if neg (number_of v) then number_of (bin_minus v) else number_of v)" -apply (simp add: real_abs_def bin_arith_simps minus_real_number_of le_real_number_of_eq_not_less less_real_number_of real_of_int_le_iff) -done - -declare abs_nat_number_of [simp] +by (simp add: real_abs_def bin_arith_simps minus_real_number_of + le_real_number_of_eq_not_less less_real_number_of real_of_int_le_iff) (*---------------------------------------------------------------------------- @@ -101,85 +99,30 @@ lemma abs_minus_eqI2: "x < (0::real) ==> abs x = -x" by (unfold real_abs_def real_le_def, simp) -lemma abs_mult_inverse: "abs (x * inverse y) = (abs x) * inverse (abs (y::real))" -by (simp add: abs_mult abs_inverse) - -text{*Much easier to prove using arithmetic than abstractly!!*} -lemma abs_triangle_ineq: "abs(x+y) \ abs x + abs (y::real)" -by (unfold real_abs_def, simp) - -(*Unused, but perhaps interesting as an example*) -lemma abs_triangle_ineq_four: "abs(w + x + y + z) \ abs(w) + abs(x) + abs(y) + abs(z::real)" -by (simp add: abs_triangle_ineq [THEN order_trans]) - lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))" by (unfold real_abs_def, simp) -lemma abs_triangle_minus_ineq: "abs(x + (-y)) \ abs x + abs (y::real)" -by (unfold real_abs_def, simp) - -lemma abs_add_less [rule_format (no_asm)]: "abs x < r --> abs y < s --> abs(x+y) < r+(s::real)" -by (unfold real_abs_def, simp) - -lemma abs_add_minus_less: - "abs x < r --> abs y < s --> abs(x+ (-y)) < r+(s::real)" -by (unfold real_abs_def, simp) - lemma abs_minus_one [simp]: "abs (-1) = (1::real)" by (unfold real_abs_def, simp) lemma abs_interval_iff: "(abs x < r) = (-r < x & x < (r::real))" -by (unfold real_abs_def, auto) +by (force simp add: Ring_and_Field.abs_less_iff) lemma abs_le_interval_iff: "(abs x \ r) = (-r\x & x\(r::real))" -by (unfold real_abs_def, auto) +by (force simp add: Ring_and_Field.abs_le_iff) -lemma abs_add_pos_gt_zero: "(0::real) < k ==> 0 < k + abs(x)" +lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)" by (unfold real_abs_def, auto) -lemma abs_add_one_gt_zero: "(0::real) < 1 + abs(x)" -by (unfold real_abs_def, auto) -declare abs_add_one_gt_zero [simp] +lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)" +by (auto intro: abs_eqI1 simp add: real_of_nat_ge_zero) -lemma abs_circle: "abs h < abs y - abs x ==> abs (x + h) < abs (y::real)" -by (auto intro: abs_triangle_ineq [THEN order_le_less_trans]) - -lemma abs_real_of_nat_cancel: "abs (real x) = real (x::nat)" -by (auto intro: abs_eqI1 simp add: real_of_nat_ge_zero) -declare abs_real_of_nat_cancel [simp] - -lemma abs_add_one_not_less_self: "~ abs(x) + (1::real) < x" +lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x" apply (rule real_leD) apply (auto intro: abs_ge_self [THEN order_trans]) done -declare abs_add_one_not_less_self [simp] -(* 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_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) -apply (case_tac "0 \ x - y", auto) -done - -lemma abs_diff_less_imp_gt_zero2: "abs(x - y) < x ==> (0::real) < x" -apply (unfold real_abs_def) -apply (case_tac "0 \ x - y", auto) -done - -lemma abs_diff_less_imp_gt_zero3: "abs(x - y) < y ==> (0::real) < x" -by (auto simp add: abs_interval_iff) - -lemma abs_diff_less_imp_gt_zero4: "abs(x - y) < -y ==> x < (0::real)" -by (auto simp add: abs_interval_iff) - -lemma abs_triangle_ineq_minus_cancel: - "abs(x) \ abs(x + (-y)) + abs((y::real))" -apply (unfold real_abs_def, auto) -done - +text{*Used only in Hyperreal/Lim.ML*} lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \ abs(x + -l) + abs(y + -m)" apply (simp add: real_add_assoc) apply (rule_tac x1 = y in real_add_left_commute [THEN ssubst]) @@ -220,29 +163,16 @@ val abs_ge_minus_self = thm"abs_ge_minus_self"; val abs_mult = thm"abs_mult"; val abs_inverse = thm"abs_inverse"; -val abs_mult_inverse = thm"abs_mult_inverse"; val abs_triangle_ineq = thm"abs_triangle_ineq"; -val abs_triangle_ineq_four = thm"abs_triangle_ineq_four"; val abs_minus_cancel = thm"abs_minus_cancel"; val abs_minus_add_cancel = thm"abs_minus_add_cancel"; -val abs_triangle_minus_ineq = thm"abs_triangle_minus_ineq"; -val abs_add_less = thm"abs_add_less"; -val abs_add_minus_less = thm"abs_add_minus_less"; val abs_minus_one = thm"abs_minus_one"; val abs_interval_iff = thm"abs_interval_iff"; val abs_le_interval_iff = thm"abs_le_interval_iff"; -val abs_add_pos_gt_zero = thm"abs_add_pos_gt_zero"; val abs_add_one_gt_zero = thm"abs_add_one_gt_zero"; -val abs_circle = thm"abs_circle"; val abs_le_zero_iff = thm"abs_le_zero_iff"; val abs_real_of_nat_cancel = thm"abs_real_of_nat_cancel"; val abs_add_one_not_less_self = thm"abs_add_one_not_less_self"; -val abs_triangle_ineq_three = thm"abs_triangle_ineq_three"; -val abs_diff_less_imp_gt_zero = thm"abs_diff_less_imp_gt_zero"; -val abs_diff_less_imp_gt_zero2 = thm"abs_diff_less_imp_gt_zero2"; -val abs_diff_less_imp_gt_zero3 = thm"abs_diff_less_imp_gt_zero3"; -val abs_diff_less_imp_gt_zero4 = thm"abs_diff_less_imp_gt_zero4"; -val abs_triangle_ineq_minus_cancel = thm"abs_triangle_ineq_minus_cancel"; val abs_sum_triangle_ineq = thm"abs_sum_triangle_ineq"; val abs_mult_less = thm"abs_mult_less"; diff -r f4d806fd72ce -r 7f115e5c5de4 src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Sat Dec 13 09:33:52 2003 +0100 +++ b/src/HOL/Ring_and_Field.thy Mon Dec 15 16:38:25 2003 +0100 @@ -1434,11 +1434,55 @@ apply (simp add: nonzero_abs_divide) done -(*TOO DIFFICULT: 6 CASES +lemma abs_leI: "[|a \ b; -a \ b|] ==> abs a \ (b::'a::ordered_ring)" +by (simp add: abs_if) + +lemma le_minus_self_iff: "(a \ -a) = (a \ (0::'a::ordered_ring))" +proof + assume ale: "a \ -a" + show "a\0" + apply (rule classical) + apply (simp add: linorder_not_le) + apply (blast intro: ale order_trans order_less_imp_le + neg_0_le_iff_le [THEN iffD1]) + done +next + assume "a\0" + hence "0 \ -a" by (simp only: neg_0_le_iff_le) + thus "a \ -a" by (blast intro: prems order_trans) +qed + +lemma minus_le_self_iff: "(-a \ a) = (0 \ (a::'a::ordered_ring))" +by (insert le_minus_self_iff [of "-a"], simp) + +lemma eq_minus_self_iff: "(a = -a) = (a = (0::'a::ordered_ring))" +by (force simp add: order_eq_iff le_minus_self_iff minus_le_self_iff) + +lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::ordered_ring))" +by (simp add: order_less_le le_minus_self_iff eq_minus_self_iff) + +lemma abs_le_D1: "abs a \ b ==> a \ (b::'a::ordered_ring)" +apply (simp add: abs_if split: split_if_asm) +apply (rule order_trans [of _ "-a"]) + apply (simp add: less_minus_self_iff order_less_imp_le, assumption) +done + +lemma abs_le_D2: "abs a \ b ==> -a \ (b::'a::ordered_ring)" +by (insert abs_le_D1 [of "-a"], simp) + +lemma abs_le_iff: "(abs a \ b) = (a \ b & -a \ (b::'a::ordered_ring))" +by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2) + +lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_ring))" +apply (simp add: order_less_le abs_le_iff) +apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff) + apply (simp add: linorder_not_less [symmetric]) +apply (simp add: le_minus_self_iff linorder_neq_iff) +apply (simp add: linorder_not_less [symmetric]) +done + lemma abs_triangle_ineq: "abs (a+b) \ abs a + abs (b::'a::ordered_ring)" -apply (simp add: abs_if) -apply (auto ); -*) +by (force simp add: abs_le_iff abs_ge_self abs_ge_minus_self add_mono) lemma abs_mult_less: "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::ordered_ring)"