# HG changeset patch # User paulson # Date 1069409740 -3600 # Node ID 95b42e69436c0446128ed6f727f1cc964644dae7 # Parent 3d0c6238162a66931a21a597f2458ddf9a9244b8 HOL: installation of Ring_and_Field as the basis for Naturals and Reals diff -r 3d0c6238162a -r 95b42e69436c src/HOL/Complex/ROOT.ML --- a/src/HOL/Complex/ROOT.ML Thu Nov 20 10:42:00 2003 +0100 +++ b/src/HOL/Complex/ROOT.ML Fri Nov 21 11:15:40 2003 +0100 @@ -5,7 +5,6 @@ The Complex Numbers *) -no_document time_use_thy "Ring_and_Field"; with_path "../Real" use_thy "Real"; with_path "../Hyperreal" use_thy "Hyperreal"; time_use_thy "Complex_Main"; diff -r 3d0c6238162a -r 95b42e69436c src/HOL/Hyperreal/NthRoot.ML --- a/src/HOL/Hyperreal/NthRoot.ML Thu Nov 20 10:42:00 2003 +0100 +++ b/src/HOL/Hyperreal/NthRoot.ML Fri Nov 21 11:15:40 2003 +0100 @@ -35,14 +35,12 @@ by (ALLGOALS(rtac ccontr)); by (ALLGOALS(dtac not_real_leE)); by (dtac realpow_ge_self2 1 THEN assume_tac 1); -by (dres_inst_tac [("n","n")] (conjI - RSN (2,conjI RS realpow_less)) 1); +by (dres_inst_tac [("n","n")] realpow_less 1); by (REPEAT(assume_tac 1)); by (dtac real_le_trans 1 THEN assume_tac 1); by (dres_inst_tac [("y","y ^ n")] order_less_le_trans 1); by (assume_tac 1 THEN etac real_less_irrefl 1); -by (dres_inst_tac [("n","n")] ((real_zero_less_one) RS (conjI - RSN (2,conjI RS realpow_less))) 1); +by (dres_inst_tac [("n","n")] ((real_zero_less_one) RS realpow_less) 1); by (Auto_tac); qed "lemma_nth_realpow_isUb_ex"; @@ -164,8 +162,8 @@ by (auto_tac (claset() addSIs [realpow_pos_nth],simpset())); by (cut_inst_tac [("R1.0","r"),("R2.0","y")] real_linear 1); by (Auto_tac); -by (dres_inst_tac [("x","r")] (conjI RS realpow_less) 1); -by (dres_inst_tac [("x","y")] (conjI RS realpow_less) 3); +by (dres_inst_tac [("x","r")] realpow_less 1); +by (dres_inst_tac [("x","y")] realpow_less 4); by (auto_tac (claset(),simpset() addsimps [real_less_not_refl])); qed "realpow_pos_nth_unique"; diff -r 3d0c6238162a -r 95b42e69436c src/HOL/Hyperreal/Transcendental.ML --- a/src/HOL/Hyperreal/Transcendental.ML Thu Nov 20 10:42:00 2003 +0100 +++ b/src/HOL/Hyperreal/Transcendental.ML Fri Nov 21 11:15:40 2003 +0100 @@ -28,10 +28,8 @@ by (forw_inst_tac [("n","n")] realpow_gt_zero 2); by (auto_tac (claset(),simpset() addsimps [real_0_less_mult_iff])); by (res_inst_tac [("R1.0","u"),("R2.0","x")] real_linear_less2 1); -by (dres_inst_tac [("n3","n"),("x","u")] - (zero_less_Suc RSN (3,conjI RSN (2,conjI RS realpow_less))) 1); -by (dres_inst_tac [("n3","n"),("x","x")] - (zero_less_Suc RSN (3,conjI RSN (2,conjI RS realpow_less))) 4); +by (dres_inst_tac [("n1","n"),("x","u")] (zero_less_Suc RSN (3, realpow_less)) 1); +by (dres_inst_tac [("n1","n"),("x","x")] (zero_less_Suc RSN (3, realpow_less)) 4); by (auto_tac (claset(),simpset() addsimps [real_less_not_refl])); qed "real_root_pos"; diff -r 3d0c6238162a -r 95b42e69436c src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Nov 20 10:42:00 2003 +0100 +++ b/src/HOL/IsaMakefile Fri Nov 21 11:15:40 2003 +0100 @@ -96,7 +96,8 @@ Nat.thy NatArith.ML NatArith.thy Numeral.thy \ Power.ML Power.thy PreList.thy Product_Type.ML Product_Type.thy ROOT.ML \ Recdef.thy Record.thy Relation.ML Relation.thy Relation_Power.ML \ - Relation_Power.thy Set.ML Set.thy SetInterval.ML SetInterval.thy \ + Relation_Power.thy Ring_and_Field.thy\ + Set.ML Set.thy SetInterval.ML SetInterval.thy \ Sum_Type.ML Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \ Tools/datatype_codegen.ML Tools/datatype_package.ML Tools/datatype_prop.ML \ Tools/datatype_realizer.ML Tools/datatype_rep_proofs.ML \ @@ -144,7 +145,7 @@ Real/RealArith0.ML Real/RealArith0.thy Real/real_arith0.ML \ Real/RealArith.thy Real/real_arith.ML Real/RealBin.ML \ Real/RealBin.thy Real/RealDef.ML Real/RealDef.thy Real/RealInt.ML \ - Real/RealInt.thy Real/RealOrd.ML Real/RealOrd.thy Real/RealPow.ML \ + Real/RealInt.thy Real/RealOrd.thy \ Real/RealPow.thy Real/document/root.tex Real/real_arith.ML\ Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy Hyperreal/ExtraThms2.ML\ Hyperreal/ExtraThms2.thy Hyperreal/Fact.ML Hyperreal/Fact.thy\ @@ -198,8 +199,7 @@ $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \ Library/FuncSet.thy Library/Library.thy \ Library/List_Prefix.thy Library/Multiset.thy Library/NatPair.thy \ - Library/Permutation.thy Library/Primes.thy \ - Library/Quotient.thy Library/Ring_and_Field.thy \ + Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \ Library/Ring_and_Field_Example.thy Library/Nat_Infinity.thy \ Library/README.html Library/Continuity.thy \ Library/Nested_Environment.thy Library/Rational_Numbers.thy \ diff -r 3d0c6238162a -r 95b42e69436c src/HOL/Library/Ring_and_Field.thy --- a/src/HOL/Library/Ring_and_Field.thy Thu Nov 20 10:42:00 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,376 +0,0 @@ -(* Title: HOL/Library/Ring_and_Field.thy - ID: $Id$ - Author: Gertrud Bauer and Markus Wenzel, TU Muenchen - License: GPL (GNU GENERAL PUBLIC LICENSE) -*) - -header {* - \title{Ring and field structures} - \author{Gertrud Bauer and Markus Wenzel} -*} - -theory Ring_and_Field = Main: - -subsection {* Abstract algebraic structures *} - -axclass ring \ zero, one, plus, minus, times - add_assoc: "(a + b) + c = a + (b + c)" - add_commute: "a + b = b + a" - left_zero [simp]: "0 + a = a" - left_minus [simp]: "- a + a = 0" - diff_minus: "a - b = a + (-b)" - - mult_assoc: "(a * b) * c = a * (b * c)" - mult_commute: "a * b = b * a" - left_one [simp]: "1 * a = a" - - left_distrib: "(a + b) * c = a * c + b * c" - -axclass ordered_ring \ ring, linorder - add_left_mono: "a \ b ==> c + a \ c + b" - mult_strict_left_mono: "a < b ==> 0 < c ==> c * a < c * b" - abs_if: "\a\ = (if a < 0 then -a else a)" - -axclass field \ ring, inverse - left_inverse [simp]: "a \ 0 ==> inverse a * a = 1" - divide_inverse: "b \ 0 ==> a / b = a * inverse b" - zero_neq_one [simp]: "0 \ 1" - -axclass ordered_field \ ordered_ring, field - -axclass division_by_zero \ zero, inverse - inverse_zero: "inverse 0 = 0" - divide_zero: "a / 0 = 0" - - - -subsection {* Derived rules for addition *} - -lemma right_zero [simp]: "a + 0 = (a::'a::ring)" -proof - - have "a + 0 = 0 + a" by (simp only: add_commute) - also have "... = a" by simp - finally show ?thesis . -qed - -lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::ring))" - by (rule mk_left_commute [of "op +", OF add_assoc add_commute]) - -theorems ring_add_ac = add_assoc add_commute add_left_commute - -lemma right_minus [simp]: "a + -(a::'a::ring) = 0" -proof - - have "a + -a = -a + a" by (simp add: ring_add_ac) - also have "... = 0" by simp - finally show ?thesis . -qed - -lemma right_minus_eq: "(a - b = 0) = (a = (b::'a::ring))" -proof - have "a = a - b + b" by (simp add: diff_minus ring_add_ac) - also assume "a - b = 0" - finally show "a = b" by simp -next - assume "a = b" - 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 - assume eq: "a + b = a + c" - then have "(-a + a) + b = (-a + a) + c" - by (simp only: eq add_assoc) - then show "b = c" by simp -next - assume eq: "b = c" - then show "a + b = a + c" by simp -qed - -lemma add_right_cancel [simp]: - "(b + a = c + a) = (b = (c::'a::ring))" - by (simp add: add_commute) - -lemma minus_minus [simp]: "- (- (a::'a::ring)) = a" - proof (rule add_left_cancel [of "-a", THEN iffD1]) - show "(-a + -(-a) = -a + a)" - by simp - qed - -lemma equals_zero_I: "a+b = 0 ==> -a = (b::'a::ring)" -apply (rule right_minus_eq [THEN iffD1, symmetric]) -apply (simp add: diff_minus add_commute) -done - -lemma minus_zero [simp]: "- 0 = (0::'a::ring)" -by (simp add: equals_zero_I) - -lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::ring))" - proof - assume "- a = - b" - then have "- (- a) = - (- b)" - by simp - then show "a=b" - by simp - next - assume "a=b" - then show "-a = -b" - by simp - qed - -lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::ring))" -by (subst neg_equal_iff_equal [symmetric], simp) - -lemma neg_0_equal_iff_equal [simp]: "(0 = -a) = (0 = (a::'a::ring))" -by (subst neg_equal_iff_equal [symmetric], simp) - - -subsection {* Derived rules for multiplication *} - -lemma right_one [simp]: "a = a * (1::'a::field)" -proof - - have "a = 1 * a" by simp - also have "... = a * 1" by (simp add: mult_commute) - finally show ?thesis . -qed - -lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::ring))" - by (rule mk_left_commute [of "op *", OF mult_assoc mult_commute]) - -theorems ring_mult_ac = mult_assoc mult_commute mult_left_commute - -lemma right_inverse [simp]: "a \ 0 ==> a * inverse (a::'a::field) = 1" -proof - - have "a * inverse a = inverse a * a" by (simp add: ring_mult_ac) - also assume "a \ 0" - hence "inverse a * a = 1" by simp - finally show ?thesis . -qed - -lemma right_inverse_eq: "b \ 0 ==> (a / b = 1) = (a = (b::'a::field))" -proof - assume neq: "b \ 0" - { - hence "a = (a / b) * b" by (simp add: divide_inverse ring_mult_ac) - also assume "a / b = 1" - finally show "a = b" by simp - next - assume "a = b" - with neq show "a / b = 1" by (simp add: divide_inverse) - } -qed - -lemma divide_self [simp]: "a \ 0 ==> a / (a::'a::field) = 1" - by (simp add: divide_inverse) - -lemma mult_left_zero [simp]: - "0 * a = (0::'a::ring)" -proof - - have "0*a + 0*a = 0*a + 0" - by (simp add: left_distrib [symmetric]) - then show ?thesis by (simp only: add_left_cancel) -qed - -lemma mult_right_zero [simp]: - "a * 0 = (0::'a::ring)" - by (simp add: mult_commute) - - -subsection {* Distribution rules *} - -lemma right_distrib: "a * (b + c) = a * b + a * (c::'a::ring)" -proof - - have "a * (b + c) = (b + c) * a" by (simp add: ring_mult_ac) - also have "... = b * a + c * a" by (simp only: left_distrib) - also have "... = a * b + a * c" by (simp add: ring_mult_ac) - finally show ?thesis . -qed - -theorems ring_distrib = right_distrib left_distrib - -lemma minus_add_distrib [simp]: "- (a + b) = -a + -(b::'a::ring)" -apply (rule equals_zero_I) -apply (simp add: ring_add_ac) -done - -lemma minus_mult_left: "- (a * b) = (-a) * (b::'a::ring)" -apply (rule equals_zero_I) -apply (simp add: left_distrib [symmetric]) -done - -lemma minus_mult_right: "- (a * b) = a * -(b::'a::ring)" -apply (rule equals_zero_I) -apply (simp add: right_distrib [symmetric]) -done - -lemma right_diff_distrib: "a * (b - c) = a * b - a * (c::'a::ring)" -by (simp add: right_distrib diff_minus - minus_mult_left [symmetric] minus_mult_right [symmetric]) - - -subsection {* Ordering rules *} - -lemma add_right_mono: "a \ (b::'a::ordered_ring) ==> a + c \ b + c" -by (simp add: add_commute [of _ c] add_left_mono) - -lemma le_imp_neg_le: "a \ (b::'a::ordered_ring) ==> -b \ -a" - proof - - assume "a\b" - then have "-a+a \ -a+b" - by (rule add_left_mono) - then have "0 \ -a+b" - by simp - then have "0 + (-b) \ (-a + b) + (-b)" - by (rule add_right_mono) - then show ?thesis - by (simp add: add_assoc) - qed - -lemma neg_le_iff_le [simp]: "(-b \ -a) = (a \ (b::'a::ordered_ring))" - proof - assume "- b \ - a" - then have "- (- a) \ - (- b)" - by (rule le_imp_neg_le) - then show "a\b" - by simp - next - assume "a\b" - then show "-b \ -a" - by (rule le_imp_neg_le) - qed - -lemma neg_le_0_iff_le [simp]: "(-a \ 0) = (0 \ (a::'a::ordered_ring))" -by (subst neg_le_iff_le [symmetric], simp) - -lemma neg_0_le_iff_le [simp]: "(0 \ -a) = (a \ (0::'a::ordered_ring))" -by (subst neg_le_iff_le [symmetric], simp) - -lemma neg_less_iff_less [simp]: "(-b < -a) = (a < (b::'a::ordered_ring))" -by (force simp add: order_less_le) - -lemma neg_less_0_iff_less [simp]: "(-a < 0) = (0 < (a::'a::ordered_ring))" -by (subst neg_less_iff_less [symmetric], simp) - -lemma neg_0_less_iff_less [simp]: "(0 < -a) = (a < (0::'a::ordered_ring))" -by (subst neg_less_iff_less [symmetric], simp) - -lemma mult_strict_right_mono: - "[|a < b; 0 < c|] ==> a * c < b * (c::'a::ordered_ring)" -by (simp add: mult_commute [of _ c] mult_strict_left_mono) - -lemma mult_left_mono: "[|a \ b; 0 < c|] ==> c * a \ c * (b::'a::ordered_ring)" -by (force simp add: mult_strict_left_mono order_le_less) - -lemma mult_right_mono: "[|a \ b; 0 < c|] ==> a*c \ b * (c::'a::ordered_ring)" -by (force simp add: mult_strict_right_mono order_le_less) - -lemma mult_strict_left_mono_neg: - "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring)" -apply (drule mult_strict_left_mono [of _ _ "-c"]) -apply (simp_all add: minus_mult_left [symmetric]) -done - -lemma mult_strict_right_mono_neg: - "[|b < a; c < 0|] ==> a * c < b * (c::'a::ordered_ring)" -apply (drule mult_strict_right_mono [of _ _ "-c"]) -apply (simp_all add: minus_mult_right [symmetric]) -done - -lemma mult_left_mono_neg: - "[|b \ a; c < 0|] ==> c * a \ c * (b::'a::ordered_ring)" -by (force simp add: mult_strict_left_mono_neg order_le_less) - -lemma mult_right_mono_neg: - "[|b \ a; c < 0|] ==> a * c \ b * (c::'a::ordered_ring)" -by (force simp add: mult_strict_right_mono_neg order_le_less) - - -subsection{* Products of Signs *} - -lemma mult_pos: "[| (0::'a::ordered_ring) < a; 0 < b |] ==> 0 < a*b" -by (drule mult_strict_left_mono [of 0 b], auto) - -lemma mult_pos_neg: "[| (0::'a::ordered_ring) < a; b < 0 |] ==> a*b < 0" -by (drule mult_strict_left_mono [of b 0], auto) - -lemma mult_neg: "[| a < (0::'a::ordered_ring); b < 0 |] ==> 0 < a*b" -by (drule mult_strict_right_mono_neg, auto) - -lemma zero_less_mult_pos: "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::ordered_ring)" -apply (case_tac "b\0") - apply (auto simp add: order_le_less linorder_not_less) -apply (drule_tac mult_pos_neg [of a b]) - apply (auto dest: order_less_not_sym) -done - -lemma zero_less_mult_iff: - "((0::'a::ordered_ring) < a*b) = (0 < a & 0 < b | a < 0 & b < 0)" -apply (auto simp add: order_le_less linorder_not_less mult_pos mult_neg) -apply (blast dest: zero_less_mult_pos) -apply (simp add: mult_commute [of a b]) -apply (blast dest: zero_less_mult_pos) -done - - -lemma mult_eq_0_iff [iff]: "(a*b = (0::'a::ordered_ring)) = (a = 0 | b = 0)" -apply (case_tac "a < 0") -apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff) -apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+ -done - -lemma zero_le_mult_iff: - "((0::'a::ordered_ring) \ a*b) = (0 \ a & 0 \ b | a \ 0 & b \ 0)" -by (auto simp add: order_le_less linorder_not_less zero_less_mult_iff) - -lemma mult_less_0_iff: - "(a*b < (0::'a::ordered_ring)) = (0 < a & b < 0 | a < 0 & 0 < b)" -apply (insert zero_less_mult_iff [of "-a" b]) -apply (force simp add: minus_mult_left[symmetric]) -done - -lemma mult_le_0_iff: - "(a*b \ (0::'a::ordered_ring)) = (0 \ a & b \ 0 | a \ 0 & 0 \ b)" -apply (insert zero_le_mult_iff [of "-a" b]) -apply (force simp add: minus_mult_left[symmetric]) -done - -lemma zero_le_square: "(0::'a::ordered_ring) \ a*a" -by (simp add: zero_le_mult_iff linorder_linear) - - -subsection {* Absolute Value *} - -text{*But is it really better than just rewriting with @{text abs_if}?*} -lemma abs_split: - "P(abs(a::'a::ordered_ring)) = ((0 \ a --> P a) & (a < 0 --> P(-a)))" -by (force dest: order_less_le_trans simp add: abs_if linorder_not_less) - -lemma abs_zero [simp]: "abs 0 = (0::'a::ordered_ring)" -by (simp add: abs_if) - -lemma abs_mult: "abs (x * y) = abs x * abs (y::'a::ordered_ring)" -apply (case_tac "x=0 | y=0", force) -apply (auto elim: order_less_asym - simp add: abs_if mult_less_0_iff linorder_neq_iff - minus_mult_left [symmetric] minus_mult_right [symmetric]) -done - -lemma abs_eq_0 [iff]: "(abs x = 0) = (x = (0::'a::ordered_ring))" -by (simp add: abs_if) - -lemma zero_less_abs_iff [iff]: "(0 < abs x) = (x ~= (0::'a::ordered_ring))" -by (simp add: abs_if linorder_neq_iff) - - -subsection {* Fields *} - -lemma zero_less_one: "(0::'a::ordered_field) < 1" -apply (insert zero_le_square [of 1]) -apply (simp add: order_less_le) -done - - -end diff -r 3d0c6238162a -r 95b42e69436c src/HOL/Library/Ring_and_Field_Example.thy --- a/src/HOL/Library/Ring_and_Field_Example.thy Thu Nov 20 10:42:00 2003 +0100 +++ b/src/HOL/Library/Ring_and_Field_Example.thy Fri Nov 21 11:15:40 2003 +0100 @@ -1,8 +1,9 @@ header {* \title{}\subsection{Example: The ordered ring of integers} *} -theory Ring_and_Field_Example = Ring_and_Field: +theory Ring_and_Field_Example = Main: +text{*The Integers Form an Ordered Ring*} instance int :: ordered_ring proof fix i j k :: int @@ -15,6 +16,7 @@ show "i * j = j * i" by simp show "1 * i = i" by simp show "(i + j) * k = i * k + j * k" by (simp add: int_distrib) + show "0 \ (1::int)" by simp show "i \ j ==> k + i \ k + j" by simp show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2) show "\i\ = (if i < 0 then -i else i)" by (simp only: zabs_def) diff -r 3d0c6238162a -r 95b42e69436c src/HOL/MicroJava/BV/Product.thy --- a/src/HOL/MicroJava/BV/Product.thy Thu Nov 20 10:42:00 2003 +0100 +++ b/src/HOL/MicroJava/BV/Product.thy Fri Nov 21 11:15:40 2003 +0100 @@ -44,7 +44,7 @@ "order(Product.le rA rB) = (order rA & order rB)" apply (unfold order_def) apply simp -apply blast +apply meson done diff -r 3d0c6238162a -r 95b42e69436c src/HOL/Nat.thy --- a/src/HOL/Nat.thy Thu Nov 20 10:42:00 2003 +0100 +++ b/src/HOL/Nat.thy Fri Nov 21 11:15:40 2003 +0100 @@ -8,7 +8,7 @@ header {* Natural numbers *} -theory Nat = Wellfounded_Recursion: +theory Nat = Wellfounded_Recursion + Ring_and_Field: subsection {* Type @{text ind} *} @@ -584,6 +584,7 @@ done + subsection {* @{term min} and @{term max} *} lemma min_0L [simp]: "min 0 n = (0::nat)" @@ -833,6 +834,30 @@ apply (induct_tac [2] n, simp_all) done +text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *} +lemma mult_less_mono2: "(i::nat) < j ==> 0 < k ==> k * i < k * j" + apply (erule_tac m1 = 0 in less_imp_Suc_add [THEN exE], simp) + apply (induct_tac x) + apply (simp_all add: add_less_mono) + done + +text{*The Naturals Form an Ordered Semiring*} +instance nat :: ordered_semiring +proof + fix i j k :: nat + show "(i + j) + k = i + (j + k)" by (rule add_assoc) + show "i + j = j + i" by (rule add_commute) + show "0 + i = i" by simp + show "(i * j) * k = i * (j * k)" by (rule mult_assoc) + show "i * j = j * i" by (rule mult_commute) + show "1 * i = i" by simp + show "(i + j) * k = i * k + j * k" by (simp add: add_mult_distrib) + show "0 \ (1::nat)" by simp + show "i \ j ==> k + i \ k + j" by simp + show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2) +qed + + subsection {* Difference *} @@ -964,13 +989,6 @@ apply (erule mult_le_mono2) done -text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *} -lemma mult_less_mono2: "(i::nat) < j ==> 0 < k ==> k * i < k * j" - apply (erule_tac m1 = 0 in less_imp_Suc_add [THEN exE], simp) - apply (induct_tac x) - apply (simp_all add: add_less_mono) - done - lemma mult_less_mono1: "(i::nat) < j ==> 0 < k ==> i * k < j * k" by (drule mult_less_mono2) (simp_all add: mult_commute) @@ -1041,4 +1059,5 @@ apply (fastsimp dest: mult_less_mono2) done + end diff -r 3d0c6238162a -r 95b42e69436c src/HOL/Real/Complex_Numbers.thy --- a/src/HOL/Real/Complex_Numbers.thy Thu Nov 20 10:42:00 2003 +0100 +++ b/src/HOL/Real/Complex_Numbers.thy Fri Nov 21 11:15:40 2003 +0100 @@ -8,29 +8,6 @@ theory Complex_Numbers = RealPow + Ring_and_Field: -subsection {* The field of real numbers *} (* FIXME move *) - -instance real :: field - by intro_classes (simp_all add: real_add_mult_distrib real_divide_def) - -lemma real_power_two: "(r::real)\ = r * r" - by (simp add: numeral_2_eq_2) - -lemma real_sqr_ge_zero [iff]: "0 \ (r::real)\" - by (simp add: real_power_two) - -lemma real_sqr_gt_zero: "(r::real) \ 0 ==> 0 < r\" -proof - - assume "r \ 0" - hence "0 \ r\" by simp - also have "0 \ r\" by (simp add: real_sqr_ge_zero) - finally show ?thesis . -qed - -lemma real_sqr_not_zero: "r \ 0 ==> (r::real)\ \ 0" - by simp - - subsection {* Representation of complex numbers *} datatype complex = Complex real real @@ -121,7 +98,7 @@ show "z - w = z + -w" by (simp add: add_complex_def minus_complex_def uminus_complex_def) show "(u * v) * w = u * (v * w)" - by (simp add: mult_complex_def ring_mult_ac ring_distrib real_diff_def) (* FIXME *) + by (simp add: mult_complex_def mult_ac ring_distrib real_diff_def) (* FIXME *) show "z * w = w * z" by (simp add: mult_complex_def) show "1 * z = z" diff -r 3d0c6238162a -r 95b42e69436c src/HOL/Real/ROOT.ML --- a/src/HOL/Real/ROOT.ML Thu Nov 20 10:42:00 2003 +0100 +++ b/src/HOL/Real/ROOT.ML Fri Nov 21 11:15:40 2003 +0100 @@ -7,5 +7,4 @@ by Jacques Fleuriot *) -no_document time_use_thy "Ring_and_Field"; time_use_thy "Real"; diff -r 3d0c6238162a -r 95b42e69436c src/HOL/Real/RealAbs.thy --- a/src/HOL/Real/RealAbs.thy Thu Nov 20 10:42:00 2003 +0100 +++ b/src/HOL/Real/RealAbs.thy Fri Nov 21 11:15:40 2003 +0100 @@ -5,10 +5,4 @@ Description : Absolute value function for the reals *) -RealAbs = RealArith + - - -defs - real_abs_def "abs r == (if (0::real) <= r then r else -r)" - -end +RealAbs = RealArith diff -r 3d0c6238162a -r 95b42e69436c src/HOL/Real/RealOrd.ML --- a/src/HOL/Real/RealOrd.ML Thu Nov 20 10:42:00 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,587 +0,0 @@ -(* Title: HOL/Real/Real.ML - ID: $Id$ - Author: Jacques D. Fleuriot and Lawrence C. Paulson - Copyright: 1998 University of Cambridge - Description: Type "real" is a linear order -*) - -(**** The simproc abel_cancel ****) - -(*** Two lemmas needed for the simprocs ***) - -(*Deletion of other terms in the formula, seeking the -x at the front of z*) -Goal "((x::real) + (y + z) = y + u) = ((x + z) = u)"; -by (stac real_add_left_commute 1); -by (rtac real_add_left_cancel 1); -qed "real_add_cancel_21"; - -(*A further rule to deal with the case that - everything gets cancelled on the right.*) -Goal "((x::real) + (y + z) = y) = (x = -z)"; -by (stac real_add_left_commute 1); -by (res_inst_tac [("t", "y")] (real_add_zero_right RS subst) 1 - THEN stac real_add_left_cancel 1); -by (simp_tac (simpset() addsimps [real_eq_diff_eq RS sym]) 1); -qed "real_add_cancel_end"; - - -structure Real_Cancel_Data = -struct - val ss = HOL_ss - val eq_reflection = eq_reflection - - val sg_ref = Sign.self_ref (Theory.sign_of (the_context ())) - val T = HOLogic.realT - val zero = Const ("0", T) - val restrict_to_left = restrict_to_left - val add_cancel_21 = real_add_cancel_21 - val add_cancel_end = real_add_cancel_end - val add_left_cancel = real_add_left_cancel - val add_assoc = real_add_assoc - val add_commute = real_add_commute - val add_left_commute = real_add_left_commute - val add_0 = real_add_zero_left - val add_0_right = real_add_zero_right - - val eq_diff_eq = real_eq_diff_eq - val eqI_rules = [real_less_eqI, real_eq_eqI, real_le_eqI] - fun dest_eqI th = - #1 (HOLogic.dest_bin "op =" HOLogic.boolT - (HOLogic.dest_Trueprop (concl_of th))) - - val diff_def = real_diff_def - val minus_add_distrib = real_minus_add_distrib - val minus_minus = real_minus_minus - val minus_0 = real_minus_zero - val add_inverses = [real_add_minus, real_add_minus_left] - val cancel_simps = [real_add_minus_cancel, real_minus_add_cancel] -end; - -structure Real_Cancel = Abel_Cancel (Real_Cancel_Data); - -Addsimprocs [Real_Cancel.sum_conv, Real_Cancel.rel_conv]; - -Goal "- (z - y) = y - (z::real)"; -by (Simp_tac 1); -qed "real_minus_diff_eq"; -Addsimps [real_minus_diff_eq]; - - -(**** Theorems about the ordering ****) - -Goal "(0 < x) = (EX y. x = real_of_preal y)"; -by (auto_tac (claset(), simpset() addsimps [real_of_preal_zero_less])); -by (cut_inst_tac [("x","x")] real_of_preal_trichotomy 1); -by (blast_tac (claset() addSEs [real_less_irrefl, - real_of_preal_not_minus_gt_zero RS notE]) 1); -qed "real_gt_zero_preal_Ex"; - -Goal "real_of_preal z < x ==> EX y. x = real_of_preal y"; -by (blast_tac (claset() addSDs [real_of_preal_zero_less RS real_less_trans] - addIs [real_gt_zero_preal_Ex RS iffD1]) 1); -qed "real_gt_preal_preal_Ex"; - -Goal "real_of_preal z <= x ==> EX y. x = real_of_preal y"; -by (blast_tac (claset() addDs [order_le_imp_less_or_eq, - real_gt_preal_preal_Ex]) 1); -qed "real_ge_preal_preal_Ex"; - -Goal "y <= 0 ==> ALL x. y < real_of_preal x"; -by (auto_tac (claset() addEs [order_le_imp_less_or_eq RS disjE] - addIs [real_of_preal_zero_less RSN(2,real_less_trans)], - simpset() addsimps [real_of_preal_zero_less])); -qed "real_less_all_preal"; - -Goal "~ 0 < y ==> ALL x. y < real_of_preal x"; -by (blast_tac (claset() addSIs [real_less_all_preal,real_leI]) 1); -qed "real_less_all_real2"; - -Goal "[| R + L = S; (0::real) < L |] ==> R < S"; -by (rtac (real_less_sum_gt_0_iff RS iffD1) 1); -by (auto_tac (claset(), simpset() addsimps real_add_ac)); -qed "real_lemma_add_positive_imp_less"; - -Goal "EX T::real. 0 < T & R + T = S ==> R < S"; -by (blast_tac (claset() addIs [real_lemma_add_positive_imp_less]) 1); -qed "real_ex_add_positive_left_less"; - -(*Alternative definition for real_less. NOT for rewriting*) -Goal "(R < S) = (EX T::real. 0 < T & R + T = S)"; -by (blast_tac (claset() addSIs [real_less_add_positive_left_Ex, - real_ex_add_positive_left_less]) 1); -qed "real_less_iff_add"; - -Goal "(real_of_preal m1 <= real_of_preal m2) = (m1 <= m2)"; -by (auto_tac (claset() addSIs [preal_leI], - simpset() addsimps [real_less_le_iff RS sym])); -by (dtac order_le_less_trans 1 THEN assume_tac 1); -by (etac preal_less_irrefl 1); -qed "real_of_preal_le_iff"; - -Goal "[| 0 < x; 0 < y |] ==> (0::real) < x * y"; -by (auto_tac (claset(), simpset() addsimps [real_gt_zero_preal_Ex])); -by (res_inst_tac [("x","y*ya")] exI 1); -by (full_simp_tac (simpset() addsimps [real_of_preal_mult]) 1); -qed "real_mult_order"; - -Goal "[| x < 0; y < 0 |] ==> (0::real) < x * y"; -by (REPEAT(dtac (real_minus_zero_less_iff RS iffD2) 1)); -by (dtac real_mult_order 1 THEN assume_tac 1); -by (Asm_full_simp_tac 1); -qed "neg_real_mult_order"; - -Goal "[| 0 < x; y < 0 |] ==> x*y < (0::real)"; -by (dtac (real_minus_zero_less_iff RS iffD2) 1); -by (dtac real_mult_order 1 THEN assume_tac 1); -by (rtac (real_minus_zero_less_iff RS iffD1) 1); -by (Asm_full_simp_tac 1); -qed "real_mult_less_0"; - -Goalw [real_one_def] "0 < (1::real)"; -by (auto_tac (claset() addIs [real_gt_zero_preal_Ex RS iffD2], - simpset() addsimps [real_of_preal_def])); -qed "real_zero_less_one"; - -(*** Monotonicity results ***) - -Goal "(v+z < w+z) = (v < (w::real))"; -by (Simp_tac 1); -qed "real_add_right_cancel_less"; - -Goal "(z+v < z+w) = (v < (w::real))"; -by (Simp_tac 1); -qed "real_add_left_cancel_less"; - -Addsimps [real_add_right_cancel_less, real_add_left_cancel_less]; - -Goal "(v+z <= w+z) = (v <= (w::real))"; -by (Simp_tac 1); -qed "real_add_right_cancel_le"; - -Goal "(z+v <= z+w) = (v <= (w::real))"; -by (Simp_tac 1); -qed "real_add_left_cancel_le"; - -Addsimps [real_add_right_cancel_le, real_add_left_cancel_le]; - -(*"v<=w ==> v+z <= w+z"*) -bind_thm ("real_add_less_mono1", real_add_right_cancel_less RS iffD2); - -(*"v<=w ==> v+z <= w+z"*) -bind_thm ("real_add_le_mono1", real_add_right_cancel_le RS iffD2); - -Goal "!!z z'::real. [| w' w' + z' < w + z"; -by (etac (real_add_less_mono1 RS order_less_le_trans) 1); -by (Simp_tac 1); -qed "real_add_less_le_mono"; - -Goal "!!z z'::real. [| w'<=w; z' w' + z' < w + z"; -by (etac (real_add_le_mono1 RS order_le_less_trans) 1); -by (Simp_tac 1); -qed "real_add_le_less_mono"; - -Goal "!!(A::real). A < B ==> C + A < C + B"; -by (Simp_tac 1); -qed "real_add_less_mono2"; - -Goal "!!(A::real). A + C < B + C ==> A < B"; -by (Full_simp_tac 1); -qed "real_less_add_right_cancel"; - -Goal "!!(A::real). C + A < C + B ==> A < B"; -by (Full_simp_tac 1); -qed "real_less_add_left_cancel"; - -Goal "!!(A::real). A + C <= B + C ==> A <= B"; -by (Full_simp_tac 1); -qed "real_le_add_right_cancel"; - -Goal "!!(A::real). C + A <= C + B ==> A <= B"; -by (Full_simp_tac 1); -qed "real_le_add_left_cancel"; - -Goal "[| 0 < x; 0 < y |] ==> (0::real) < x + y"; -by (etac order_less_trans 1); -by (dtac real_add_less_mono2 1); -by (Full_simp_tac 1); -qed "real_add_order"; - -Goal "[| 0 <= x; 0 <= y |] ==> (0::real) <= x + y"; -by (REPEAT(dtac order_le_imp_less_or_eq 1)); -by (auto_tac (claset() addIs [real_add_order, order_less_imp_le], - simpset())); -qed "real_le_add_order"; - -Goal "[| R1 < S1; R2 < S2 |] ==> R1 + R2 < S1 + (S2::real)"; -by (dtac real_add_less_mono1 1); -by (etac order_less_trans 1); -by (etac real_add_less_mono2 1); -qed "real_add_less_mono"; - -Goal "!!(q1::real). q1 <= q2 ==> x + q1 <= x + q2"; -by (Simp_tac 1); -qed "real_add_left_le_mono1"; - -Goal "[|i<=j; k<=l |] ==> i + k <= j + (l::real)"; -by (dtac real_add_le_mono1 1); -by (etac order_trans 1); -by (Simp_tac 1); -qed "real_add_le_mono"; - -Goal "EX (x::real). x < y"; -by (rtac (real_add_zero_right RS subst) 1); -by (res_inst_tac [("x","y + (- (1::real))")] exI 1); -by (auto_tac (claset() addSIs [real_add_less_mono2], - simpset() addsimps [real_minus_zero_less_iff2, real_zero_less_one])); -qed "real_less_Ex"; - -Goal "(0::real) < r ==> u + (-r) < u"; -by (res_inst_tac [("C","r")] real_less_add_right_cancel 1); -by (simp_tac (simpset() addsimps [real_add_assoc]) 1); -qed "real_add_minus_positive_less_self"; - -Goal "(-s <= -r) = ((r::real) <= s)"; -by (rtac sym 1); -by (Step_tac 1); -by (dres_inst_tac [("x","-s")] real_add_left_le_mono1 1); -by (dres_inst_tac [("x","r")] real_add_left_le_mono1 2); -by Auto_tac; -by (dres_inst_tac [("z","-r")] real_add_le_mono1 1); -by (dres_inst_tac [("z","s")] real_add_le_mono1 2); -by (auto_tac (claset(), simpset() addsimps [real_add_assoc])); -qed "real_le_minus_iff"; -Addsimps [real_le_minus_iff]; - -Goal "(0::real) <= x*x"; -by (res_inst_tac [("R2.0","0"),("R1.0","x")] real_linear_less2 1); -by (auto_tac (claset() addIs [real_mult_order, - neg_real_mult_order,order_less_imp_le], - simpset())); -qed "real_le_square"; -Addsimps [real_le_square]; - -(*---------------------------------------------------------------------------- - An embedding of the naturals in the reals - ----------------------------------------------------------------------------*) - -Goalw [real_of_posnat_def] "real_of_posnat 0 = (1::real)"; -by (simp_tac (simpset() addsimps [pnat_one_iff RS sym,real_of_preal_def, - symmetric real_one_def]) 1); -qed "real_of_posnat_one"; - -Goalw [real_of_posnat_def] "real_of_posnat (Suc 0) = (1::real) + (1::real)"; -by (simp_tac (simpset() addsimps [real_of_preal_def,real_one_def, - pnat_two_eq,real_add,prat_of_pnat_add RS sym, - preal_of_prat_add RS sym] @ pnat_add_ac) 1); -qed "real_of_posnat_two"; - -Goalw [real_of_posnat_def] - "real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + (1::real)"; -by (full_simp_tac (simpset() addsimps [real_of_posnat_one RS sym, - real_of_posnat_def,real_of_preal_add RS sym,preal_of_prat_add RS sym, - prat_of_pnat_add RS sym,pnat_of_nat_add]) 1); -qed "real_of_posnat_add"; - -Goal "real_of_posnat (n + 1) = real_of_posnat n + (1::real)"; -by (res_inst_tac [("x1","(1::real)")] (real_add_right_cancel RS iffD1) 1); -by (rtac (real_of_posnat_add RS subst) 1); -by (full_simp_tac (simpset() addsimps [real_of_posnat_two,real_add_assoc]) 1); -qed "real_of_posnat_add_one"; - -Goal "real_of_posnat (Suc n) = real_of_posnat n + (1::real)"; -by (stac (real_of_posnat_add_one RS sym) 1); -by (Simp_tac 1); -qed "real_of_posnat_Suc"; - -Goal "inj(real_of_posnat)"; -by (rtac injI 1); -by (rewtac real_of_posnat_def); -by (dtac (inj_real_of_preal RS injD) 1); -by (dtac (inj_preal_of_prat RS injD) 1); -by (dtac (inj_prat_of_pnat RS injD) 1); -by (etac (inj_pnat_of_nat RS injD) 1); -qed "inj_real_of_posnat"; - -Goalw [real_of_nat_def] "real (0::nat) = 0"; -by (simp_tac (simpset() addsimps [real_of_posnat_one]) 1); -qed "real_of_nat_zero"; - -Goalw [real_of_nat_def] "real (Suc 0) = (1::real)"; -by (simp_tac (simpset() addsimps [real_of_posnat_two, real_add_assoc]) 1); -qed "real_of_nat_one"; -Addsimps [real_of_nat_zero, real_of_nat_one]; - -Goalw [real_of_nat_def] - "real (m + n) = real (m::nat) + real n"; -by (simp_tac (simpset() addsimps - [real_of_posnat_add,real_add_assoc RS sym]) 1); -qed "real_of_nat_add"; -Addsimps [real_of_nat_add]; - -(*Not for addsimps: often the LHS is used to represent a positive natural*) -Goalw [real_of_nat_def] "real (Suc n) = real n + (1::real)"; -by (simp_tac (simpset() addsimps [real_of_posnat_Suc] @ real_add_ac) 1); -qed "real_of_nat_Suc"; - -Goalw [real_of_nat_def, real_of_posnat_def] - "(real (n::nat) < real m) = (n < m)"; -by Auto_tac; -qed "real_of_nat_less_iff"; -AddIffs [real_of_nat_less_iff]; - -Goal "(real (n::nat) <= real m) = (n <= m)"; -by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); -qed "real_of_nat_le_iff"; -AddIffs [real_of_nat_le_iff]; - -Goal "inj (real :: nat => real)"; -by (rtac injI 1); -by (auto_tac (claset() addSIs [inj_real_of_posnat RS injD], - simpset() addsimps [real_of_nat_def,real_add_right_cancel])); -qed "inj_real_of_nat"; - -Goal "0 <= real (n::nat)"; -by (induct_tac "n" 1); -by (auto_tac (claset(), - simpset () addsimps [real_of_nat_Suc])); -by (dtac real_add_le_less_mono 1); -by (rtac real_zero_less_one 1); -by (asm_full_simp_tac (simpset() addsimps [order_less_imp_le]) 1); -qed "real_of_nat_ge_zero"; -AddIffs [real_of_nat_ge_zero]; - -Goal "real (m * n) = real (m::nat) * real n"; -by (induct_tac "m" 1); -by (auto_tac (claset(), - simpset() addsimps [real_of_nat_Suc, - real_add_mult_distrib, real_add_commute])); -qed "real_of_nat_mult"; -Addsimps [real_of_nat_mult]; - -Goal "(real (n::nat) = real m) = (n = m)"; -by (auto_tac (claset() addDs [inj_real_of_nat RS injD], simpset())); -qed "real_of_nat_inject"; -AddIffs [real_of_nat_inject]; - -Goal "n <= m --> real (m - n) = real (m::nat) - real n"; -by (induct_tac "m" 1); -by (auto_tac (claset(), - simpset() addsimps [real_diff_def, Suc_diff_le, le_Suc_eq, - real_of_nat_Suc, real_of_nat_zero] @ real_add_ac)); -qed_spec_mp "real_of_nat_diff"; - -Goal "(real (n::nat) = 0) = (n = 0)"; -by (auto_tac ((claset() addIs [inj_real_of_nat RS injD], simpset()) delIffs [real_of_nat_inject])); -qed "real_of_nat_zero_iff"; - -Goal "neg z ==> real (nat z) = 0"; -by (asm_simp_tac (simpset() addsimps [neg_nat, real_of_nat_zero]) 1); -qed "real_of_nat_neg_int"; -Addsimps [real_of_nat_neg_int]; - - -(*---------------------------------------------------------------------------- - inverse, etc. - ----------------------------------------------------------------------------*) - -Goal "0 < x ==> 0 < inverse (x::real)"; -by (EVERY1[rtac ccontr, dtac real_leI]); -by (forward_tac [real_minus_zero_less_iff2 RS iffD2] 1); -by (forward_tac [real_not_refl2 RS not_sym] 1); -by (dtac (real_not_refl2 RS not_sym RS real_inverse_not_zero) 1); -by (EVERY1[dtac order_le_imp_less_or_eq, Step_tac]); -by (dtac neg_real_mult_order 1 THEN assume_tac 1); -by (auto_tac (claset() addIs [real_zero_less_one RS real_less_asym], - simpset())); -qed "real_inverse_gt_0"; - -Goal "x < 0 ==> inverse (x::real) < 0"; -by (ftac real_not_refl2 1); -by (dtac (real_minus_zero_less_iff RS iffD2) 1); -by (rtac (real_minus_zero_less_iff RS iffD1) 1); -by (stac (real_minus_inverse RS sym) 1); -by (auto_tac (claset() addIs [real_inverse_gt_0], simpset())); -qed "real_inverse_less_0"; - -Goal "[| (0::real) < z; x < y |] ==> x*z < y*z"; -by (rotate_tac 1 1); -by (dtac real_less_sum_gt_zero 1); -by (rtac real_sum_gt_zero_less 1); -by (dtac real_mult_order 1 THEN assume_tac 1); -by (asm_full_simp_tac - (simpset() addsimps [real_add_mult_distrib2, real_mult_commute ]) 1); -qed "real_mult_less_mono1"; - -Goal "[| (0::real) < z; x < y |] ==> z * x < z * y"; -by (asm_simp_tac - (simpset() addsimps [real_mult_commute,real_mult_less_mono1]) 1); -qed "real_mult_less_mono2"; - -Goal "[| (0::real) < z; x * z < y * z |] ==> x < y"; -by (forw_inst_tac [("x","x*z")] - (real_inverse_gt_0 RS real_mult_less_mono1) 1); -by (auto_tac (claset(), - simpset() addsimps [real_mult_assoc,real_not_refl2 RS not_sym])); -qed "real_mult_less_cancel1"; - -Goal "[| (0::real) < z; z*x < z*y |] ==> x < y"; -by (etac real_mult_less_cancel1 1); -by (asm_full_simp_tac (simpset() addsimps [real_mult_commute]) 1); -qed "real_mult_less_cancel2"; - -Goal "(0::real) < z ==> (x*z < y*z) = (x < y)"; -by (blast_tac - (claset() addIs [real_mult_less_mono1, real_mult_less_cancel1]) 1); -qed "real_mult_less_iff1"; - -Goal "(0::real) < z ==> (z*x < z*y) = (x < y)"; -by (blast_tac - (claset() addIs [real_mult_less_mono2, real_mult_less_cancel2]) 1); -qed "real_mult_less_iff2"; - -Addsimps [real_mult_less_iff1,real_mult_less_iff2]; - -(* 05/00 *) -Goalw [real_le_def] "(0::real) < z ==> (x*z <= y*z) = (x <= y)"; -by (Auto_tac); -qed "real_mult_le_cancel_iff1"; - -Goalw [real_le_def] "(0::real) < z ==> (z*x <= z*y) = (x <= y)"; -by (Auto_tac); -qed "real_mult_le_cancel_iff2"; - -Addsimps [real_mult_le_cancel_iff1,real_mult_le_cancel_iff2]; - - -Goal "[| (0::real) <= z; x < y |] ==> x*z <= y*z"; -by (EVERY1 [rtac real_less_or_eq_imp_le, dtac order_le_imp_less_or_eq]); -by (auto_tac (claset() addIs [real_mult_less_mono1],simpset())); -qed "real_mult_le_less_mono1"; - -Goal "[| u u*x < v* y"; -by (etac (real_mult_less_mono1 RS order_less_trans) 1); -by (assume_tac 1); -by (etac real_mult_less_mono2 1); -by (assume_tac 1); -qed "real_mult_less_mono"; - -(*Variant of the theorem above; sometimes it's stronger*) -Goal "[| x < y; r1 < r2; (0::real) <= r1; 0 <= x|] ==> r1 * x < r2 * y"; -by (subgoal_tac "0 0 < x"; -by (rtac ccontr 1 THEN dtac real_leI 1); -by (dtac order_trans 1 THEN assume_tac 1); -by (auto_tac (claset() addDs [real_zero_less_one RSN (2,order_le_less_trans)], - simpset())); -qed "real_gt_zero"; - -Goal "[| (1::real) < r; (1::real) <= x |] ==> x <= r * x"; -by (dtac (real_gt_zero RS order_less_imp_le) 1); -by (auto_tac (claset() addSDs [real_mult_le_less_mono1], - simpset())); -qed "real_mult_self_le"; - -Goal "[| (1::real) <= r; (1::real) <= x |] ==> x <= r * x"; -by (dtac order_le_imp_less_or_eq 1); -by (auto_tac (claset() addIs [real_mult_self_le], simpset())); -qed "real_mult_self_le2"; - -Goal "[| 0 < r; r < x |] ==> inverse x < inverse (r::real)"; -by (ftac order_less_trans 1 THEN assume_tac 1); -by (ftac real_inverse_gt_0 1); -by (forw_inst_tac [("x","x")] real_inverse_gt_0 1); -by (forw_inst_tac [("x","r"),("z","inverse r")] real_mult_less_mono1 1); -by (assume_tac 1); -by (asm_full_simp_tac (simpset() addsimps [real_not_refl2 RS - not_sym RS real_mult_inv_right]) 1); -by (ftac real_inverse_gt_0 1); -by (forw_inst_tac [("x","(1::real)"),("z","inverse x")] real_mult_less_mono2 1); -by (assume_tac 1); -by (asm_full_simp_tac (simpset() addsimps [real_not_refl2 RS - not_sym RS real_mult_inv_left,real_mult_assoc RS sym]) 1); -qed "real_inverse_less_swap"; - -Goal "(x*y = 0) = (x = 0 | y = (0::real))"; -by Auto_tac; -by (blast_tac (claset() addIs [ccontr] addDs [real_mult_not_zero]) 1); -qed "real_mult_is_0"; -AddIffs [real_mult_is_0]; - -Goal "[| x ~= 0; y ~= 0 |] \ -\ ==> inverse x + inverse y = (x + y) * inverse (x * (y::real))"; -by (asm_full_simp_tac (simpset() addsimps - [real_inverse_distrib,real_add_mult_distrib, - real_mult_assoc RS sym]) 1); -by (stac real_mult_assoc 1); -by (rtac (real_mult_left_commute RS subst) 1); -by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1); -qed "real_inverse_add"; - -(* 05/00 *) -Goal "(0 <= -R) = (R <= (0::real))"; -by (auto_tac (claset() addDs [sym], - simpset() addsimps [real_le_less])); -qed "real_minus_zero_le_iff"; - -Goal "(-R <= 0) = ((0::real) <= R)"; -by (auto_tac (claset(),simpset() addsimps - [real_minus_zero_less_iff2,real_le_less])); -qed "real_minus_zero_le_iff2"; - -Addsimps [real_minus_zero_le_iff, real_minus_zero_le_iff2]; - -Goal "x * x + y * y = 0 ==> x = (0::real)"; -by (dtac real_add_minus_eq_minus 1); -by (cut_inst_tac [("x","x")] real_le_square 1); -by (Auto_tac THEN dtac real_le_anti_sym 1); -by Auto_tac; -qed "real_sum_squares_cancel"; - -Goal "x * x + y * y = 0 ==> y = (0::real)"; -by (res_inst_tac [("y","x")] real_sum_squares_cancel 1); -by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1); -qed "real_sum_squares_cancel2"; - -(*---------------------------------------------------------------------------- - Some convenient biconditionals for products of signs (lcp) - ----------------------------------------------------------------------------*) - -Goal "((0::real) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)"; -by (auto_tac (claset(), - simpset() addsimps [order_le_less, linorder_not_less, - real_mult_order, neg_real_mult_order])); -by (ALLGOALS (rtac ccontr)); -by (auto_tac (claset(), simpset() addsimps [order_le_less, linorder_not_less])); -by (ALLGOALS (etac rev_mp)); -by (ALLGOALS (dtac real_mult_less_0 THEN' assume_tac)); -by (auto_tac (claset() addDs [order_less_not_sym], - simpset() addsimps [real_mult_commute])); -qed "real_0_less_mult_iff"; - -Goal "((0::real) <= x*y) = (0 <= x & 0 <= y | x <= 0 & y <= 0)"; -by (auto_tac (claset(), - simpset() addsimps [order_le_less, linorder_not_less, - real_0_less_mult_iff])); -qed "real_0_le_mult_iff"; - -Goal "(x*y < (0::real)) = (0 < x & y < 0 | x < 0 & 0 < y)"; -by (auto_tac (claset(), - simpset() addsimps [real_0_le_mult_iff, - linorder_not_le RS sym])); -by (auto_tac (claset() addDs [order_less_not_sym], - simpset() addsimps [linorder_not_le])); -qed "real_mult_less_0_iff"; - -Goal "(x*y <= (0::real)) = (0 <= x & y <= 0 | x <= 0 & 0 <= y)"; -by (auto_tac (claset() addDs [order_less_not_sym], - simpset() addsimps [real_0_less_mult_iff, - linorder_not_less RS sym])); -qed "real_mult_le_0_iff"; - diff -r 3d0c6238162a -r 95b42e69436c src/HOL/Real/RealOrd.thy --- a/src/HOL/Real/RealOrd.thy Thu Nov 20 10:42:00 2003 +0100 +++ b/src/HOL/Real/RealOrd.thy Fri Nov 21 11:15:40 2003 +0100 @@ -2,15 +2,696 @@ ID: $Id$ Author: Jacques D. Fleuriot and Lawrence C. Paulson Copyright: 1998 University of Cambridge - Description: Type "real" is a linear order and also - satisfies plus_ac0: + is an AC-operator with zero *) -RealOrd = RealDef + +header{*The Reals Form an Ordered Field, etc.*} + +theory RealOrd = RealDef: + +instance real :: order + by (intro_classes, + (assumption | + rule real_le_refl real_le_trans real_le_anti_sym real_less_le)+) + +instance real :: linorder + by (intro_classes, rule real_le_linear) + +instance real :: plus_ac0 + by (intro_classes, + (assumption | + rule real_add_commute real_add_assoc real_add_zero_left)+) + + +defs (overloaded) + real_abs_def: "abs (r::real) == (if 0 \ r then r else -r)" + + + + +subsection{* The Simproc @{text abel_cancel}*} + +(*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)" +apply (subst real_add_left_commute) +apply (rule real_add_left_cancel) +done + +(*A further rule to deal with the case that + everything gets cancelled on the right.*) +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 (no_asm) add: real_eq_diff_eq [symmetric]) +done + + +ML +{* +val real_add_cancel_21 = thm "real_add_cancel_21"; +val real_add_cancel_end = thm "real_add_cancel_end"; + +structure Real_Cancel_Data = +struct + val ss = HOL_ss + val eq_reflection = eq_reflection + + val sg_ref = Sign.self_ref (Theory.sign_of (the_context ())) + val T = HOLogic.realT + val zero = Const ("0", T) + val restrict_to_left = restrict_to_left + val add_cancel_21 = real_add_cancel_21 + val add_cancel_end = real_add_cancel_end + val add_left_cancel = real_add_left_cancel + val add_assoc = real_add_assoc + val add_commute = real_add_commute + val add_left_commute = real_add_left_commute + val add_0 = real_add_zero_left + val add_0_right = real_add_zero_right + + val eq_diff_eq = real_eq_diff_eq + val eqI_rules = [real_less_eqI, real_eq_eqI, real_le_eqI] + fun dest_eqI th = + #1 (HOLogic.dest_bin "op =" HOLogic.boolT + (HOLogic.dest_Trueprop (concl_of th))) + + val diff_def = real_diff_def + val minus_add_distrib = real_minus_add_distrib + val minus_minus = real_minus_minus + val minus_0 = real_minus_zero + val add_inverses = [real_add_minus, real_add_minus_left] + val cancel_simps = [real_add_minus_cancel, real_minus_add_cancel] +end; + +structure Real_Cancel = Abel_Cancel (Real_Cancel_Data); + +Addsimprocs [Real_Cancel.sum_conv, Real_Cancel.rel_conv]; +*} + +lemma real_minus_diff_eq: "- (z - y) = y - (z::real)" +apply (simp (no_asm)) +done +declare real_minus_diff_eq [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" +apply (blast dest!: real_of_preal_zero_less [THEN real_less_trans] + intro: real_gt_zero_preal_Ex [THEN iffD1]) +done + +lemma real_ge_preal_preal_Ex: "real_of_preal z \ x ==> \y. x = real_of_preal y" +apply (blast dest: order_le_imp_less_or_eq real_gt_preal_preal_Ex) +done + +lemma real_less_all_preal: "y \ 0 ==> \x. y < real_of_preal x" +apply (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) +done + +lemma real_less_all_real2: "~ 0 < y ==> \x. y < real_of_preal x" +apply (blast intro!: real_less_all_preal real_leI) +done + +lemma real_lemma_add_positive_imp_less: "[| R + L = S; (0::real) < L |] ==> R < S" +apply (rule real_less_sum_gt_0_iff [THEN iffD1]) +apply (auto simp add: real_add_ac) +done + +lemma real_ex_add_positive_left_less: "\T::real. 0 < T & R + T = S ==> R < S" +apply (blast intro: real_lemma_add_positive_imp_less) +done + +(*Alternative definition for real_less. NOT for rewriting*) +lemma real_less_iff_add: "(R < S) = (\T::real. 0 < T & R + T = S)" +apply (blast intro!: real_less_add_positive_left_Ex real_ex_add_positive_left_less) +done + +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 + +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 neg_real_mult_order: "[| x < 0; y < 0 |] ==> (0::real) < x * y" +apply (drule real_minus_zero_less_iff [THEN iffD2])+ +apply (drule real_mult_order , assumption) +apply simp +done + +lemma real_mult_less_0: "[| 0 < x; y < 0 |] ==> x*y < (0::real)" +apply (drule real_minus_zero_less_iff [THEN iffD2]) +apply (drule real_mult_order , assumption) +apply (rule real_minus_zero_less_iff [THEN iffD1]) +apply simp +done + +lemma real_zero_less_one: "0 < (1::real)" +apply (unfold real_one_def) +apply (auto intro: real_gt_zero_preal_Ex [THEN iffD2] + simp add: real_of_preal_def) +done + + +subsection{*Monotonicity of Addition*} + +lemma real_add_right_cancel_less: "(v+z < w+z) = (v < (w::real))" +apply (simp (no_asm)) +done + +lemma real_add_left_cancel_less: "(z+v < z+w) = (v < (w::real))" +apply (simp (no_asm)) +done + +declare real_add_right_cancel_less [simp] real_add_left_cancel_less [simp] + +lemma real_add_right_cancel_le: "(v+z \ w+z) = (v \ (w::real))" +apply (simp (no_asm)) +done + +lemma real_add_left_cancel_le: "(z+v \ z+w) = (v \ (w::real))" +apply (simp (no_asm)) +done + +declare real_add_right_cancel_le [simp] real_add_left_cancel_le [simp] + +(*"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" +apply (erule real_add_less_mono1 [THEN order_less_le_trans]) +apply (simp (no_asm)) +done + +lemma real_add_le_less_mono: "!!z z'::real. [| w'\w; z' w' + z' < w + z" +apply (erule real_add_le_mono1 [THEN order_le_less_trans]) +apply (simp (no_asm)) +done + +lemma real_add_less_mono2: "!!(A::real). A < B ==> C + A < C + B" +apply (simp (no_asm)) +done + +lemma real_less_add_right_cancel: "!!(A::real). A + C < B + C ==> A < B" +apply (simp (no_asm_use)) +done + +lemma real_less_add_left_cancel: "!!(A::real). C + A < C + B ==> A < B" +apply (simp (no_asm_use)) +done + +lemma real_le_add_right_cancel: "!!(A::real). A + C \ B + C ==> A \ B" +apply (simp (no_asm_use)) +done + +lemma real_le_add_left_cancel: "!!(A::real). C + A \ C + B ==> A \ B" +apply (simp (no_asm_use)) +done + +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 (no_asm_use)) +done + +lemma real_le_add_order: "[| 0 \ x; 0 \ y |] ==> (0::real) \ x + y" +apply (drule order_le_imp_less_or_eq)+ +apply (auto intro: real_add_order order_less_imp_le) +done + +lemma real_add_less_mono: "[| R1 < S1; R2 < S2 |] ==> R1 + R2 < S1 + (S2::real)" +apply (drule real_add_less_mono1) +apply (erule order_less_trans) +apply (erule real_add_less_mono2) +done + +lemma real_add_left_le_mono1: "!!(q1::real). q1 \ q2 ==> x + q1 \ x + q2" +apply (simp (no_asm)) +done + +lemma real_add_le_mono: "[|i\j; k\l |] ==> i + k \ j + (l::real)" +apply (drule real_add_le_mono1) +apply (erule order_trans) +apply (simp (no_asm)) +done + +lemma real_less_Ex: "\(x::real). x < y" +apply (rule real_add_zero_right [THEN subst]) +apply (rule_tac x = "y + (- (1::real))" in exI) +apply (auto intro!: real_add_less_mono2 simp add: real_minus_zero_less_iff2 real_zero_less_one) +done + +lemma real_add_minus_positive_less_self: "(0::real) < r ==> u + (-r) < u" +apply (rule_tac C = "r" in real_less_add_right_cancel) +apply (simp (no_asm) add: real_add_assoc) +done + +lemma real_le_minus_iff: "(-s \ -r) = ((r::real) \ s)" +apply (rule sym) +apply safe +apply (drule_tac x = "-s" in real_add_left_le_mono1) +apply (drule_tac [2] x = "r" in real_add_left_le_mono1) +apply auto +apply (drule_tac z = "-r" in real_add_le_mono1) +apply (drule_tac [2] z = "s" in real_add_le_mono1) +apply (auto simp add: real_add_assoc) +done +declare real_le_minus_iff [simp] + +lemma real_le_square: "(0::real) \ x*x" +apply (rule_tac real_linear_less2 [of x 0]) +apply (auto intro: real_mult_order neg_real_mult_order order_less_imp_le) +done +declare real_le_square [simp] + +lemma real_mult_less_mono1: "[| (0::real) < z; x < y |] ==> x*z < y*z" +apply (rotate_tac 1) +apply (drule real_less_sum_gt_zero) +apply (rule real_sum_gt_zero_less) +apply (drule real_mult_order , assumption) +apply (simp add: real_add_mult_distrib2 real_mult_commute) +done + +lemma real_mult_less_mono2: "[| (0::real) < z; x < y |] ==> z * x < z * y" +apply (simp (no_asm_simp) add: real_mult_commute real_mult_less_mono1) +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 + + + +(*---------------------------------------------------------------------------- + An embedding of the naturals in the reals + ----------------------------------------------------------------------------*) + +lemma real_of_posnat_one: "real_of_posnat 0 = (1::real)" + +apply (unfold real_of_posnat_def) +apply (simp (no_asm) add: pnat_one_iff [symmetric] real_of_preal_def symmetric real_one_def) +done + +lemma real_of_posnat_two: "real_of_posnat (Suc 0) = (1::real) + (1::real)" +apply (simp add: real_of_posnat_def real_of_preal_def real_one_def pnat_two_eq + real_add + prat_of_pnat_add [symmetric] preal_of_prat_add [symmetric] + pnat_add_ac) +done + +lemma real_of_posnat_add: + "real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + (1::real)" +apply (unfold real_of_posnat_def) +apply (simp (no_asm_use) add: real_of_posnat_one [symmetric] real_of_posnat_def real_of_preal_add [symmetric] preal_of_prat_add [symmetric] prat_of_pnat_add [symmetric] pnat_of_nat_add) +done + +lemma real_of_posnat_add_one: "real_of_posnat (n + 1) = real_of_posnat n + (1::real)" +apply (rule_tac x1 = " (1::real) " in real_add_right_cancel [THEN iffD1]) +apply (rule real_of_posnat_add [THEN subst]) +apply (simp (no_asm_use) add: real_of_posnat_two real_add_assoc) +done -instance real :: order (real_le_refl,real_le_trans,real_le_anti_sym,real_less_le) -instance real :: linorder (real_le_linear) +lemma real_of_posnat_Suc: "real_of_posnat (Suc n) = real_of_posnat n + (1::real)" +apply (subst real_of_posnat_add_one [symmetric]) +apply (simp (no_asm)) +done + +lemma inj_real_of_posnat: "inj(real_of_posnat)" +apply (rule inj_onI) +apply (unfold real_of_posnat_def) +apply (drule inj_real_of_preal [THEN injD]) +apply (drule inj_preal_of_prat [THEN injD]) +apply (drule inj_prat_of_pnat [THEN injD]) +apply (erule inj_pnat_of_nat [THEN injD]) +done + +lemma real_of_nat_zero: "real (0::nat) = 0" +apply (unfold real_of_nat_def) +apply (simp (no_asm) add: real_of_posnat_one) +done + +lemma real_of_nat_one: "real (Suc 0) = (1::real)" +apply (unfold real_of_nat_def) +apply (simp (no_asm) add: real_of_posnat_two real_add_assoc) +done +declare real_of_nat_zero [simp] real_of_nat_one [simp] + +lemma real_of_nat_add: + "real (m + n) = real (m::nat) + real n" +apply (simp add: real_of_nat_def real_add_assoc) +apply (simp add: real_of_posnat_add real_add_assoc [symmetric]) +done +declare real_of_nat_add [simp] + +(*Not for addsimps: often the LHS is used to represent a positive natural*) +lemma real_of_nat_Suc: "real (Suc n) = real n + (1::real)" +apply (unfold real_of_nat_def) +apply (simp (no_asm) add: real_of_posnat_Suc real_add_ac) +done + +lemma real_of_nat_less_iff: + "(real (n::nat) < real m) = (n < m)" +apply (unfold real_of_nat_def real_of_posnat_def) +apply auto +done +declare real_of_nat_less_iff [iff] + +lemma real_of_nat_le_iff: "(real (n::nat) \ real m) = (n \ m)" +apply (simp (no_asm) add: linorder_not_less [symmetric]) +done +declare real_of_nat_le_iff [iff] + +lemma inj_real_of_nat: "inj (real :: nat => real)" +apply (rule inj_onI) +apply (auto intro!: inj_real_of_posnat [THEN injD] + simp add: real_of_nat_def real_add_right_cancel) +done + +lemma real_of_nat_ge_zero: "0 \ real (n::nat)" +apply (induct_tac "n") +apply (auto simp add: real_of_nat_Suc) +apply (drule real_add_le_less_mono) +apply (rule real_zero_less_one) +apply (simp add: order_less_imp_le) +done +declare real_of_nat_ge_zero [iff] + +lemma real_of_nat_mult: "real (m * n) = real (m::nat) * real n" +apply (induct_tac "m") +apply (auto simp add: real_of_nat_Suc real_add_mult_distrib real_add_commute) +done +declare real_of_nat_mult [simp] + +lemma real_of_nat_inject: "(real (n::nat) = real m) = (n = m)" +apply (auto dest: inj_real_of_nat [THEN injD]) +done +declare real_of_nat_inject [iff] + +lemma real_of_nat_diff [rule_format (no_asm)]: "n \ m --> real (m - n) = real (m::nat) - real n" +apply (induct_tac "m") +apply (auto simp add: real_diff_def Suc_diff_le le_Suc_eq real_of_nat_Suc real_of_nat_zero real_add_ac) +done + +lemma real_of_nat_zero_iff: "(real (n::nat) = 0) = (n = 0)" + proof + assume "real n = 0" + have "real n = real (0::nat)" by simp + then show "n = 0" by (simp only: real_of_nat_inject) + next + show "n = 0 \ real n = 0" by simp + qed + +lemma real_of_nat_neg_int: "neg z ==> real (nat z) = 0" +apply (simp (no_asm_simp) add: neg_nat real_of_nat_zero) +done +declare real_of_nat_neg_int [simp] + + +(*---------------------------------------------------------------------------- + inverse, etc. + ----------------------------------------------------------------------------*) + +lemma real_inverse_gt_0: "0 < x ==> 0 < inverse (x::real)" +apply (rule ccontr) +apply (drule real_leI) +apply (frule real_minus_zero_less_iff2 [THEN iffD2]) +apply (frule real_not_refl2 [THEN not_sym]) +apply (drule real_not_refl2 [THEN not_sym, THEN real_inverse_not_zero]) +apply (drule order_le_imp_less_or_eq) +apply safe; +apply (drule neg_real_mult_order, assumption) +apply (auto intro: real_zero_less_one [THEN real_less_asym]) +done + +lemma real_inverse_less_0: "x < 0 ==> inverse (x::real) < 0" +apply (frule real_not_refl2) +apply (drule real_minus_zero_less_iff [THEN iffD2]) +apply (rule real_minus_zero_less_iff [THEN iffD1]) +apply (subst real_minus_inverse [symmetric]) +apply (auto intro: real_inverse_gt_0) +done + +lemma real_mult_less_cancel1: "[| (0::real) < z; x * z < y * z |] ==> x < y" +apply (frule_tac x = "x*z" in real_inverse_gt_0 [THEN real_mult_less_mono1]) +apply (auto simp add: real_mult_assoc real_not_refl2 [THEN not_sym]) +done + +lemma real_mult_less_cancel2: "[| (0::real) < z; z*x < z*y |] ==> x < y" +apply (erule real_mult_less_cancel1) +apply (simp add: real_mult_commute) +done + +lemma real_mult_less_iff1: "(0::real) < z ==> (x*z < y*z) = (x < y)" +apply (blast intro: real_mult_less_mono1 real_mult_less_cancel1) +done + +lemma real_mult_less_iff2: "(0::real) < z ==> (z*x < z*y) = (x < y)" +apply (blast intro: real_mult_less_mono2 real_mult_less_cancel2) +done + +declare real_mult_less_iff1 [simp] real_mult_less_iff2 [simp] + +(* 05/00 *) +lemma real_mult_le_cancel_iff1: "(0::real) < z ==> (x*z \ y*z) = (x \ y)" +apply (unfold real_le_def) +apply auto +done + +lemma real_mult_le_cancel_iff2: "(0::real) < z ==> (z*x \ z*y) = (x \ y)" +apply (unfold real_le_def) +apply auto +done + +declare real_mult_le_cancel_iff1 [simp] real_mult_le_cancel_iff2 [simp] + + +lemma real_mult_le_less_mono1: "[| (0::real) \ z; x < y |] ==> x*z \ y*z" +apply (rule real_less_or_eq_imp_le) +apply (drule order_le_imp_less_or_eq) +apply (auto intro: real_mult_less_mono1) +done + +lemma real_mult_less_mono: "[| u u*x < v* y" +apply (erule real_mult_less_mono1 [THEN order_less_trans]) +apply assumption +apply (erule real_mult_less_mono2) +apply assumption +done -instance real :: plus_ac0 (real_add_commute,real_add_assoc,real_add_zero_left) +(*Variant of the theorem above; sometimes it's stronger*) +lemma real_mult_less_mono': "[| x < y; r1 < r2; (0::real) \ r1; 0 \ x|] ==> r1 * x < r2 * y" +apply (subgoal_tac "0 x ==> 0 < x" +apply (rule ccontr , drule real_leI) +apply (drule order_trans , assumption) +apply (auto dest: real_zero_less_one [THEN [2] order_le_less_trans]) +done + +lemma real_mult_self_le: "[| (1::real) < r; (1::real) \ x |] ==> x \ r * x" +apply (drule real_gt_zero [THEN order_less_imp_le]) +apply (auto dest!: real_mult_le_less_mono1) +done + +lemma real_mult_self_le2: "[| (1::real) \ r; (1::real) \ x |] ==> x \ r * x" +apply (drule order_le_imp_less_or_eq) +apply (auto intro: real_mult_self_le) +done + +lemma real_inverse_less_swap: "[| 0 < r; r < x |] ==> inverse x < inverse (r::real)" +apply (frule order_less_trans , assumption) +apply (frule real_inverse_gt_0) +apply (frule_tac x = "x" in real_inverse_gt_0) +apply (frule_tac x = "r" and z = "inverse r" in real_mult_less_mono1) +apply assumption +apply (simp add: real_not_refl2 [THEN not_sym, THEN real_mult_inv_right]) +apply (frule real_inverse_gt_0) +apply (frule_tac x = " (1::real) " and z = "inverse x" in real_mult_less_mono2) +apply assumption +apply (simp add: real_not_refl2 [THEN not_sym, THEN real_mult_inv_left] real_mult_assoc [symmetric]) +done + +lemma real_mult_is_0: "(x*y = 0) = (x = 0 | y = (0::real))" +apply auto +done +declare real_mult_is_0 [iff] + +lemma real_inverse_add: "[| x \ 0; y \ 0 |] + ==> inverse x + inverse y = (x + y) * inverse (x * (y::real))" +apply (simp add: real_inverse_distrib real_add_mult_distrib real_mult_assoc [symmetric]) +apply (subst real_mult_assoc) +apply (rule real_mult_left_commute [THEN subst]) +apply (simp add: real_add_commute) +done + +(* 05/00 *) +lemma real_minus_zero_le_iff: "(0 \ -R) = (R \ (0::real))" +apply (auto dest: sym simp add: real_le_less) +done + +lemma real_minus_zero_le_iff2: "(-R \ 0) = ((0::real) \ R)" +apply (auto simp add: real_minus_zero_less_iff2 real_le_less) +done + +declare real_minus_zero_le_iff [simp] real_minus_zero_le_iff2 [simp] + +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 (auto , drule real_le_anti_sym) +apply auto +done + +lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)" +apply (rule_tac y = "x" in real_sum_squares_cancel) +apply (simp add: real_add_commute) +done + +(*---------------------------------------------------------------------------- + Some convenient biconditionals for products of signs (lcp) + ----------------------------------------------------------------------------*) + +lemma real_0_less_mult_iff: "((0::real) < x*y) = (0x*y) = (0\x & 0\y | x\0 & y\0)" + by (rule zero_le_mult_iff) + +lemma real_mult_less_0_iff: "(x*y < (0::real)) = (0 (0::real)) = (0\x & y\0 | x\0 & 0\y)" + by (rule mult_le_0_iff) + + +ML +{* +val real_abs_def = thm "real_abs_def"; + +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"; +val real_ge_preal_preal_Ex = thm "real_ge_preal_preal_Ex"; +val real_less_all_preal = thm "real_less_all_preal"; +val real_less_all_real2 = thm "real_less_all_real2"; +val real_lemma_add_positive_imp_less = thm "real_lemma_add_positive_imp_less"; +val real_ex_add_positive_left_less = thm "real_ex_add_positive_left_less"; +val real_less_iff_add = thm "real_less_iff_add"; +val real_of_preal_le_iff = thm "real_of_preal_le_iff"; +val real_mult_order = thm "real_mult_order"; +val neg_real_mult_order = thm "neg_real_mult_order"; +val real_mult_less_0 = thm "real_mult_less_0"; +val real_zero_less_one = thm "real_zero_less_one"; +val real_add_right_cancel_less = thm "real_add_right_cancel_less"; +val real_add_left_cancel_less = thm "real_add_left_cancel_less"; +val real_add_right_cancel_le = thm "real_add_right_cancel_le"; +val real_add_left_cancel_le = thm "real_add_left_cancel_le"; +val real_add_less_mono1 = thm "real_add_less_mono1"; +val real_add_le_mono1 = thm "real_add_le_mono1"; +val real_add_less_le_mono = thm "real_add_less_le_mono"; +val real_add_le_less_mono = thm "real_add_le_less_mono"; +val real_add_less_mono2 = thm "real_add_less_mono2"; +val real_less_add_right_cancel = thm "real_less_add_right_cancel"; +val real_less_add_left_cancel = thm "real_less_add_left_cancel"; +val real_le_add_right_cancel = thm "real_le_add_right_cancel"; +val real_le_add_left_cancel = thm "real_le_add_left_cancel"; +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_less_Ex = thm "real_less_Ex"; +val real_add_minus_positive_less_self = thm "real_add_minus_positive_less_self"; +val real_le_minus_iff = thm "real_le_minus_iff"; +val real_le_square = thm "real_le_square"; +val real_mult_less_mono1 = thm "real_mult_less_mono1"; +val real_mult_less_mono2 = thm "real_mult_less_mono2"; +val real_of_posnat_one = thm "real_of_posnat_one"; +val real_of_posnat_two = thm "real_of_posnat_two"; +val real_of_posnat_add = thm "real_of_posnat_add"; +val real_of_posnat_add_one = thm "real_of_posnat_add_one"; +val real_of_posnat_Suc = thm "real_of_posnat_Suc"; +val inj_real_of_posnat = thm "inj_real_of_posnat"; +val real_of_nat_zero = thm "real_of_nat_zero"; +val real_of_nat_one = thm "real_of_nat_one"; +val real_of_nat_add = thm "real_of_nat_add"; +val real_of_nat_Suc = thm "real_of_nat_Suc"; +val real_of_nat_less_iff = thm "real_of_nat_less_iff"; +val real_of_nat_le_iff = thm "real_of_nat_le_iff"; +val inj_real_of_nat = thm "inj_real_of_nat"; +val real_of_nat_ge_zero = thm "real_of_nat_ge_zero"; +val real_of_nat_mult = thm "real_of_nat_mult"; +val real_of_nat_inject = thm "real_of_nat_inject"; +val real_of_nat_diff = thm "real_of_nat_diff"; +val real_of_nat_zero_iff = thm "real_of_nat_zero_iff"; +val real_of_nat_neg_int = thm "real_of_nat_neg_int"; +val real_inverse_gt_0 = thm "real_inverse_gt_0"; +val real_inverse_less_0 = thm "real_inverse_less_0"; +val real_mult_less_cancel1 = thm "real_mult_less_cancel1"; +val real_mult_less_cancel2 = thm "real_mult_less_cancel2"; +val real_mult_less_iff1 = thm "real_mult_less_iff1"; +val real_mult_less_iff2 = thm "real_mult_less_iff2"; +val real_mult_le_cancel_iff1 = thm "real_mult_le_cancel_iff1"; +val real_mult_le_cancel_iff2 = thm "real_mult_le_cancel_iff2"; +val real_mult_le_less_mono1 = thm "real_mult_le_less_mono1"; +val real_mult_less_mono = thm "real_mult_less_mono"; +val real_mult_less_mono' = thm "real_mult_less_mono'"; +val real_gt_zero = thm "real_gt_zero"; +val real_mult_self_le = thm "real_mult_self_le"; +val real_mult_self_le2 = thm "real_mult_self_le2"; +val real_inverse_less_swap = thm "real_inverse_less_swap"; +val real_mult_is_0 = thm "real_mult_is_0"; +val real_inverse_add = thm "real_inverse_add"; +val real_minus_zero_le_iff = thm "real_minus_zero_le_iff"; +val real_minus_zero_le_iff2 = thm "real_minus_zero_le_iff2"; +val real_sum_squares_cancel = thm "real_sum_squares_cancel"; +val real_sum_squares_cancel2 = thm "real_sum_squares_cancel2"; +val real_0_less_mult_iff = thm "real_0_less_mult_iff"; +val real_0_le_mult_iff = thm "real_0_le_mult_iff"; +val real_mult_less_0_iff = thm "real_mult_less_0_iff"; +val real_mult_le_0_iff = thm "real_mult_le_0_iff"; +*} end diff -r 3d0c6238162a -r 95b42e69436c src/HOL/Real/RealPow.ML --- a/src/HOL/Real/RealPow.ML Thu Nov 20 10:42:00 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,388 +0,0 @@ -(* Title : RealPow.ML - ID : $Id$ - Author : Jacques D. Fleuriot - Copyright : 1998 University of Cambridge - Description : Natural Powers of reals theory - -FIXME: most of the theorems for Suc (Suc 0) are redundant! -*) - -bind_thm ("realpow_Suc", thm "realpow_Suc"); - -Goal "(0::real) ^ (Suc n) = 0"; -by Auto_tac; -qed "realpow_zero"; -Addsimps [realpow_zero]; - -Goal "r ~= (0::real) --> r ^ n ~= 0"; -by (induct_tac "n" 1); -by Auto_tac; -qed_spec_mp "realpow_not_zero"; - -Goal "r ^ n = (0::real) ==> r = 0"; -by (rtac ccontr 1); -by (auto_tac (claset() addDs [realpow_not_zero], simpset())); -qed "realpow_zero_zero"; - -Goal "inverse ((r::real) ^ n) = (inverse r) ^ n"; -by (induct_tac "n" 1); -by (auto_tac (claset(), simpset() addsimps [real_inverse_distrib])); -qed "realpow_inverse"; - -Goal "abs(r ^ n) = abs(r::real) ^ n"; -by (induct_tac "n" 1); -by (auto_tac (claset(), simpset() addsimps [abs_mult])); -qed "realpow_abs"; - -Goal "(r::real) ^ (n + m) = (r ^ n) * (r ^ m)"; -by (induct_tac "n" 1); -by (auto_tac (claset(),simpset() addsimps real_mult_ac)); -qed "realpow_add"; - -Goal "(r::real) ^ 1 = r"; -by (Simp_tac 1); -qed "realpow_one"; -Addsimps [realpow_one]; - -Goal "(r::real)^ (Suc (Suc 0)) = r * r"; -by (Simp_tac 1); -qed "realpow_two"; - -Goal "(0::real) < r --> 0 < r ^ n"; -by (induct_tac "n" 1); -by (auto_tac (claset() addIs [real_mult_order], - simpset() addsimps [real_zero_less_one])); -qed_spec_mp "realpow_gt_zero"; - -Goal "(0::real) <= r --> 0 <= r ^ n"; -by (induct_tac "n" 1); -by (auto_tac (claset(), simpset() addsimps [real_0_le_mult_iff])); -qed_spec_mp "realpow_ge_zero"; - -Goal "(0::real) <= x & x <= y --> x ^ n <= y ^ n"; -by (induct_tac "n" 1); -by (auto_tac (claset() addSIs [real_mult_le_mono], simpset())); -by (asm_simp_tac (simpset() addsimps [realpow_ge_zero]) 1); -qed_spec_mp "realpow_le"; - -Goal "(0::real) < x & x < y & 0 < n --> x ^ n < y ^ n"; -by (induct_tac "n" 1); -by (auto_tac (claset() addIs [real_mult_less_mono, gr0I] - addDs [realpow_gt_zero], - simpset())); -qed_spec_mp "realpow_less"; - -Goal "1 ^ n = (1::real)"; -by (induct_tac "n" 1); -by Auto_tac; -qed "realpow_eq_one"; -Addsimps [realpow_eq_one]; - -Goal "abs((-1) ^ n) = (1::real)"; -by (induct_tac "n" 1); -by (auto_tac (claset(), simpset() addsimps [abs_mult])); -qed "abs_realpow_minus_one"; -Addsimps [abs_realpow_minus_one]; - -Goal "((r::real) * s) ^ n = (r ^ n) * (s ^ n)"; -by (induct_tac "n" 1); -by (auto_tac (claset(),simpset() addsimps real_mult_ac)); -qed "realpow_mult"; - -Goal "(0::real) <= r^ Suc (Suc 0)"; -by (simp_tac (simpset() addsimps [real_le_square]) 1); -qed "realpow_two_le"; -Addsimps [realpow_two_le]; - -Goal "abs((x::real)^Suc (Suc 0)) = x^Suc (Suc 0)"; -by (simp_tac (simpset() addsimps [abs_eqI1, - real_le_square]) 1); -qed "abs_realpow_two"; -Addsimps [abs_realpow_two]; - -Goal "abs(x::real)^Suc (Suc 0) = x^Suc (Suc 0)"; -by (simp_tac (simpset() addsimps [realpow_abs RS sym,abs_eqI1] - delsimps [realpow_Suc]) 1); -qed "realpow_two_abs"; -Addsimps [realpow_two_abs]; - -Goal "(1::real) < r ==> 1 < r^ (Suc (Suc 0))"; -by Auto_tac; -by (cut_facts_tac [real_zero_less_one] 1); -by (forw_inst_tac [("x","0")] order_less_trans 1); -by (assume_tac 1); -by (dres_inst_tac [("z","r"),("x","1")] - (real_mult_less_mono1) 1); -by (auto_tac (claset() addIs [order_less_trans], simpset())); -qed "realpow_two_gt_one"; - -Goal "(1::real) < r --> 1 <= r ^ n"; -by (induct_tac "n" 1); -by Auto_tac; -by (subgoal_tac "1*1 <= r * r^n" 1); -by (rtac real_mult_le_mono 2); -by Auto_tac; -qed_spec_mp "realpow_ge_one"; - -Goal "(1::real) <= r ==> 1 <= r ^ n"; -by (dtac order_le_imp_less_or_eq 1); -by (auto_tac (claset() addDs [realpow_ge_one], simpset())); -qed "realpow_ge_one2"; - -Goal "(1::real) <= 2 ^ n"; -by (res_inst_tac [("y","1 ^ n")] order_trans 1); -by (rtac realpow_le 2); -by (auto_tac (claset() addIs [order_less_imp_le], simpset())); -qed "two_realpow_ge_one"; - -Goal "real (n::nat) < 2 ^ n"; -by (induct_tac "n" 1); -by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc])); -by (stac real_mult_2 1); -by (rtac real_add_less_le_mono 1); -by (auto_tac (claset(), simpset() addsimps [two_realpow_ge_one])); -qed "two_realpow_gt"; -Addsimps [two_realpow_gt,two_realpow_ge_one]; - -Goal "(-1) ^ (2*n) = (1::real)"; -by (induct_tac "n" 1); -by Auto_tac; -qed "realpow_minus_one"; -Addsimps [realpow_minus_one]; - -Goal "(-1) ^ Suc (2*n) = -(1::real)"; -by Auto_tac; -qed "realpow_minus_one_odd"; -Addsimps [realpow_minus_one_odd]; - -Goal "(-1) ^ Suc (Suc (2*n)) = (1::real)"; -by Auto_tac; -qed "realpow_minus_one_even"; -Addsimps [realpow_minus_one_even]; - -Goal "(0::real) < r & r < (1::real) --> r ^ Suc n < r ^ n"; -by (induct_tac "n" 1); -by Auto_tac; -qed_spec_mp "realpow_Suc_less"; - -Goal "0 <= r & r < (1::real) --> r ^ Suc n <= r ^ n"; -by (induct_tac "n" 1); -by (auto_tac (claset() addIs [order_less_imp_le] - addSDs [order_le_imp_less_or_eq], - simpset())); -qed_spec_mp "realpow_Suc_le"; - -Goal "(0::real) <= 0 ^ n"; -by (case_tac "n" 1); -by Auto_tac; -qed "realpow_zero_le"; -Addsimps [realpow_zero_le]; - -Goal "0 < r & r < (1::real) --> r ^ Suc n <= r ^ n"; -by (blast_tac (claset() addSIs [order_less_imp_le, - realpow_Suc_less]) 1); -qed_spec_mp "realpow_Suc_le2"; - -Goal "[| 0 <= r; r < (1::real) |] ==> r ^ Suc n <= r ^ n"; -by (etac (order_le_imp_less_or_eq RS disjE) 1); -by (rtac realpow_Suc_le2 1); -by Auto_tac; -qed "realpow_Suc_le3"; - -Goal "0 <= r & r < (1::real) & n < N --> r ^ N <= r ^ n"; -by (induct_tac "N" 1); -by (ALLGOALS Asm_simp_tac); -by (Clarify_tac 1); -by (subgoal_tac "r * r ^ na <= 1 * r ^ n" 1); -by (Asm_full_simp_tac 1); -by (rtac real_mult_le_mono 1); -by (auto_tac (claset(), simpset() addsimps [realpow_ge_zero, less_Suc_eq])); -qed_spec_mp "realpow_less_le"; - -Goal "[| 0 <= r; r < (1::real); n <= N |] ==> r ^ N <= r ^ n"; -by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1); -by (auto_tac (claset() addIs [realpow_less_le], - simpset())); -qed "realpow_le_le"; - -Goal "[| 0 < r; r < (1::real) |] ==> r ^ Suc n <= r"; -by (dres_inst_tac [("n","1"),("N","Suc n")] - (order_less_imp_le RS realpow_le_le) 1); -by Auto_tac; -qed "realpow_Suc_le_self"; - -Goal "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1"; -by (blast_tac (claset() addIs [realpow_Suc_le_self, order_le_less_trans]) 1); -qed "realpow_Suc_less_one"; - -Goal "(1::real) <= r --> r ^ n <= r ^ Suc n"; -by (induct_tac "n" 1); -by Auto_tac; -qed_spec_mp "realpow_le_Suc"; - -Goal "(1::real) < r --> r ^ n < r ^ Suc n"; -by (induct_tac "n" 1); -by Auto_tac; -qed_spec_mp "realpow_less_Suc"; - -Goal "(1::real) < r --> r ^ n <= r ^ Suc n"; -by (blast_tac (claset() addSIs [order_less_imp_le, realpow_less_Suc]) 1); -qed_spec_mp "realpow_le_Suc2"; - -Goal "(1::real) < r & n < N --> r ^ n <= r ^ N"; -by (induct_tac "N" 1); -by Auto_tac; -by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one)); -by (ALLGOALS(dtac (real_mult_self_le))); -by (assume_tac 1); -by (assume_tac 2); -by (auto_tac (claset() addIs [order_trans], - simpset() addsimps [less_Suc_eq])); -qed_spec_mp "realpow_gt_ge"; - -Goal "(1::real) <= r & n < N --> r ^ n <= r ^ N"; -by (induct_tac "N" 1); -by Auto_tac; -by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one2)); -by (ALLGOALS(dtac (real_mult_self_le2))); -by (assume_tac 1); -by (assume_tac 2); -by (auto_tac (claset() addIs [order_trans], - simpset() addsimps [less_Suc_eq])); -qed_spec_mp "realpow_gt_ge2"; - -Goal "[| (1::real) < r; n <= N |] ==> r ^ n <= r ^ N"; -by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1); -by (auto_tac (claset() addIs [realpow_gt_ge], simpset())); -qed "realpow_ge_ge"; - -Goal "[| (1::real) <= r; n <= N |] ==> r ^ n <= r ^ N"; -by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1); -by (auto_tac (claset() addIs [realpow_gt_ge2], simpset())); -qed "realpow_ge_ge2"; - -Goal "(1::real) < r ==> r <= r ^ Suc n"; -by (dres_inst_tac [("n","1"),("N","Suc n")] - realpow_ge_ge 1); -by Auto_tac; -qed_spec_mp "realpow_Suc_ge_self"; - -Goal "(1::real) <= r ==> r <= r ^ Suc n"; -by (dres_inst_tac [("n","1"),("N","Suc n")] - realpow_ge_ge2 1); -by Auto_tac; -qed_spec_mp "realpow_Suc_ge_self2"; - -Goal "[| (1::real) < r; 0 < n |] ==> r <= r ^ n"; -by (dtac (less_not_refl2 RS not0_implies_Suc) 1); -by (auto_tac (claset() addSIs - [realpow_Suc_ge_self],simpset())); -qed "realpow_ge_self"; - -Goal "[| (1::real) <= r; 0 < n |] ==> r <= r ^ n"; -by (dtac (less_not_refl2 RS not0_implies_Suc) 1); -by (auto_tac (claset() addSIs [realpow_Suc_ge_self2],simpset())); -qed "realpow_ge_self2"; - -Goal "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"; -by (induct_tac "n" 1); -by (auto_tac (claset(),simpset() - addsimps [real_mult_commute])); -qed_spec_mp "realpow_minus_mult"; -Addsimps [realpow_minus_mult]; - -Goal "r ~= 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)"; -by (asm_simp_tac (simpset() addsimps [realpow_two, - real_mult_assoc RS sym]) 1); -qed "realpow_two_mult_inverse"; -Addsimps [realpow_two_mult_inverse]; - -(* 05/00 *) -Goal "(-x)^Suc (Suc 0) = (x::real)^Suc (Suc 0)"; -by (Simp_tac 1); -qed "realpow_two_minus"; -Addsimps [realpow_two_minus]; - -Goalw [real_diff_def] "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"; -by (simp_tac (simpset() addsimps - [real_add_mult_distrib2, real_add_mult_distrib] @ real_mult_ac) 1); -qed "realpow_two_diff"; - -Goalw [real_diff_def] "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"; -by (cut_inst_tac [("x","x"),("y","y")] realpow_two_diff 1); -by (auto_tac (claset(), simpset() delsimps [realpow_Suc])); -qed "realpow_two_disj"; - -(* used in Transc *) -Goal "[|(x::real) ~= 0; m <= n |] ==> x ^ (n - m) = x ^ n * inverse (x ^ m)"; -by (auto_tac (claset(), - simpset() addsimps [le_eq_less_or_eq, less_iff_Suc_add, realpow_add, - realpow_not_zero] @ real_mult_ac)); -qed "realpow_diff"; - -Goal "real (m::nat) ^ n = real (m ^ n)"; -by (induct_tac "n" 1); -by (auto_tac (claset(), - simpset() addsimps [real_of_nat_one, real_of_nat_mult])); -qed "realpow_real_of_nat"; - -Goal "0 < real (Suc (Suc 0) ^ n)"; -by (induct_tac "n" 1); -by (auto_tac (claset(), - simpset() addsimps [real_of_nat_mult, real_0_less_mult_iff])); -qed "realpow_real_of_nat_two_pos"; -Addsimps [realpow_real_of_nat_two_pos]; - - -Goal "(0::real) <= x --> 0 <= y --> x ^ Suc n <= y ^ Suc n --> x <= y"; -by (induct_tac "n" 1); -by Auto_tac; -by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); -by (swap_res_tac [real_mult_less_mono'] 1); -by Auto_tac; -by (auto_tac (claset(), simpset() addsimps [real_0_le_mult_iff])); -by (auto_tac (claset(), simpset() addsimps [linorder_not_less RS sym])); -by (dres_inst_tac [("n","n")] realpow_gt_zero 1); -by Auto_tac; -qed_spec_mp "realpow_increasing"; - -Goal "[| (0::real) <= x; 0 <= y; x ^ Suc n = y ^ Suc n |] ==> x = y"; -by (blast_tac (claset() addIs [realpow_increasing, order_antisym, - order_eq_refl, sym]) 1); -qed_spec_mp "realpow_Suc_cancel_eq"; - - -(*** Logical equivalences for inequalities ***) - -Goal "(x^n = 0) = (x = (0::real) & 0 (0::real) --> r ^ n \ 0" +apply (induct_tac "n") +apply auto +done + +lemma realpow_zero_zero: "r ^ n = (0::real) ==> r = 0" +apply (rule ccontr) +apply (auto dest: realpow_not_zero) +done + +lemma realpow_inverse: "inverse ((r::real) ^ n) = (inverse r) ^ n" +apply (induct_tac "n") +apply (auto simp add: real_inverse_distrib) +done + +lemma realpow_abs: "abs(r ^ n) = abs(r::real) ^ n" +apply (induct_tac "n") +apply (auto simp add: abs_mult) +done + +lemma realpow_add: "(r::real) ^ (n + m) = (r ^ n) * (r ^ m)" +apply (induct_tac "n") +apply (auto simp add: real_mult_ac) +done + +lemma realpow_one: "(r::real) ^ 1 = r" +apply (simp (no_asm)) +done +declare realpow_one [simp] + +lemma realpow_two: "(r::real)^ (Suc (Suc 0)) = r * r" +apply (simp (no_asm)) +done + +lemma realpow_gt_zero [rule_format (no_asm)]: "(0::real) < r --> 0 < r ^ n" +apply (induct_tac "n") +apply (auto intro: real_mult_order simp add: real_zero_less_one) +done + +lemma realpow_ge_zero [rule_format (no_asm)]: "(0::real) \ r --> 0 \ r ^ n" +apply (induct_tac "n") +apply (auto simp add: real_0_le_mult_iff) +done + +lemma realpow_le [rule_format (no_asm)]: "(0::real) \ x & x \ y --> x ^ n \ y ^ n" +apply (induct_tac "n") +apply (auto intro!: real_mult_le_mono) +apply (simp (no_asm_simp) add: realpow_ge_zero) +done + +lemma realpow_0_left [rule_format, simp]: + "0 < n --> 0 ^ n = (0::real)" +apply (induct_tac "n") +apply (auto ); +done + +lemma realpow_less' [rule_format]: + "[|(0::real) \ x; x < y |] ==> 0 < n --> x ^ n < y ^ n" +apply (induct n) +apply (auto simp add: real_mult_less_mono' realpow_ge_zero); +done + +text{*Legacy: weaker version of the theorem above*} +lemma realpow_less [rule_format]: + "[|(0::real) < x; x < y; 0 < n|] ==> x ^ n < y ^ n" +apply (rule realpow_less') +apply (auto ); +done + +lemma realpow_eq_one: "1 ^ n = (1::real)" +apply (induct_tac "n") +apply auto +done +declare realpow_eq_one [simp] + +lemma abs_realpow_minus_one: "abs((-1) ^ n) = (1::real)" +apply (induct_tac "n") +apply (auto simp add: abs_mult) +done +declare abs_realpow_minus_one [simp] + +lemma realpow_mult: "((r::real) * s) ^ n = (r ^ n) * (s ^ n)" +apply (induct_tac "n") +apply (auto simp add: real_mult_ac) +done + +lemma realpow_two_le: "(0::real) \ r^ Suc (Suc 0)" +apply (simp (no_asm) add: real_le_square) +done +declare realpow_two_le [simp] + +lemma abs_realpow_two: "abs((x::real)^Suc (Suc 0)) = x^Suc (Suc 0)" +apply (simp (no_asm) add: abs_eqI1 real_le_square) +done +declare abs_realpow_two [simp] + +lemma realpow_two_abs: "abs(x::real)^Suc (Suc 0) = x^Suc (Suc 0)" +apply (simp (no_asm) add: realpow_abs [symmetric] abs_eqI1 del: realpow_Suc) +done +declare realpow_two_abs [simp] + +lemma realpow_two_gt_one: "(1::real) < r ==> 1 < r^ (Suc (Suc 0))" +apply auto +apply (cut_tac real_zero_less_one) +apply (frule_tac x = "0" in order_less_trans) +apply assumption +apply (drule_tac z = "r" and x = "1" in real_mult_less_mono1) +apply (auto intro: order_less_trans) +done + +lemma realpow_ge_one [rule_format (no_asm)]: "(1::real) < r --> 1 \ r ^ n" +apply (induct_tac "n") +apply auto +apply (subgoal_tac "1*1 \ r * r^n") +apply (rule_tac [2] real_mult_le_mono) +apply auto +done + +lemma realpow_ge_one2: "(1::real) \ r ==> 1 \ r ^ n" +apply (drule order_le_imp_less_or_eq) +apply (auto dest: realpow_ge_one) +done + +lemma two_realpow_ge_one: "(1::real) \ 2 ^ n" +apply (rule_tac y = "1 ^ n" in order_trans) +apply (rule_tac [2] realpow_le) +apply (auto intro: order_less_imp_le) +done + +lemma two_realpow_gt: "real (n::nat) < 2 ^ n" +apply (induct_tac "n") +apply (auto simp add: real_of_nat_Suc) +apply (subst real_mult_2) +apply (rule real_add_less_le_mono) +apply (auto simp add: two_realpow_ge_one) +done +declare two_realpow_gt [simp] two_realpow_ge_one [simp] + +lemma realpow_minus_one: "(-1) ^ (2*n) = (1::real)" +apply (induct_tac "n") +apply auto +done +declare realpow_minus_one [simp] + +lemma realpow_minus_one_odd: "(-1) ^ Suc (2*n) = -(1::real)" +apply auto +done +declare realpow_minus_one_odd [simp] + +lemma realpow_minus_one_even: "(-1) ^ Suc (Suc (2*n)) = (1::real)" +apply auto +done +declare realpow_minus_one_even [simp] + +lemma realpow_Suc_less [rule_format (no_asm)]: "(0::real) < r & r < (1::real) --> r ^ Suc n < r ^ n" +apply (induct_tac "n") +apply auto +done + +lemma realpow_Suc_le [rule_format (no_asm)]: "0 \ r & r < (1::real) --> r ^ Suc n \ r ^ n" +apply (induct_tac "n") +apply (auto intro: order_less_imp_le dest!: order_le_imp_less_or_eq) +done + +lemma realpow_zero_le: "(0::real) \ 0 ^ n" +apply (case_tac "n") +apply auto +done +declare realpow_zero_le [simp] + +lemma realpow_Suc_le2 [rule_format (no_asm)]: "0 < r & r < (1::real) --> r ^ Suc n \ r ^ n" +apply (blast intro!: order_less_imp_le realpow_Suc_less) +done + +lemma realpow_Suc_le3: "[| 0 \ r; r < (1::real) |] ==> r ^ Suc n \ r ^ n" +apply (erule order_le_imp_less_or_eq [THEN disjE]) +apply (rule realpow_Suc_le2) +apply auto +done + +lemma realpow_less_le [rule_format (no_asm)]: "0 \ r & r < (1::real) & n < N --> r ^ N \ r ^ n" +apply (induct_tac "N") +apply (simp_all (no_asm_simp)) +apply clarify +apply (subgoal_tac "r * r ^ na \ 1 * r ^ n") +apply simp +apply (rule real_mult_le_mono) +apply (auto simp add: realpow_ge_zero less_Suc_eq) +done + +lemma realpow_le_le: "[| 0 \ r; r < (1::real); n \ N |] ==> r ^ N \ r ^ n" +apply (drule_tac n = "N" in le_imp_less_or_eq) +apply (auto intro: realpow_less_le) +done + +lemma realpow_Suc_le_self: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n \ r" +apply (drule_tac n = "1" and N = "Suc n" in order_less_imp_le [THEN realpow_le_le]) +apply auto +done + +lemma realpow_Suc_less_one: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1" +apply (blast intro: realpow_Suc_le_self order_le_less_trans) +done + +lemma realpow_le_Suc [rule_format (no_asm)]: "(1::real) \ r --> r ^ n \ r ^ Suc n" +apply (induct_tac "n") +apply auto +done + +lemma realpow_less_Suc [rule_format (no_asm)]: "(1::real) < r --> r ^ n < r ^ Suc n" +apply (induct_tac "n") +apply auto +done + +lemma realpow_le_Suc2 [rule_format (no_asm)]: "(1::real) < r --> r ^ n \ r ^ Suc n" +apply (blast intro!: order_less_imp_le realpow_less_Suc) +done + +lemma realpow_gt_ge [rule_format (no_asm)]: "(1::real) < r & n < N --> r ^ n \ r ^ N" +apply (induct_tac "N") +apply auto +apply (frule_tac [!] n = "na" in realpow_ge_one) +apply (drule_tac [!] real_mult_self_le) +apply assumption +prefer 2 apply (assumption) +apply (auto intro: order_trans simp add: less_Suc_eq) +done + +lemma realpow_gt_ge2 [rule_format (no_asm)]: "(1::real) \ r & n < N --> r ^ n \ r ^ N" +apply (induct_tac "N") +apply auto +apply (frule_tac [!] n = "na" in realpow_ge_one2) +apply (drule_tac [!] real_mult_self_le2) +apply assumption +prefer 2 apply (assumption) +apply (auto intro: order_trans simp add: less_Suc_eq) +done + +lemma realpow_ge_ge: "[| (1::real) < r; n \ N |] ==> r ^ n \ r ^ N" +apply (drule_tac n = "N" in le_imp_less_or_eq) +apply (auto intro: realpow_gt_ge) +done + +lemma realpow_ge_ge2: "[| (1::real) \ r; n \ N |] ==> r ^ n \ r ^ N" +apply (drule_tac n = "N" in le_imp_less_or_eq) +apply (auto intro: realpow_gt_ge2) +done + +lemma realpow_Suc_ge_self [rule_format (no_asm)]: "(1::real) < r ==> r \ r ^ Suc n" +apply (drule_tac n = "1" and N = "Suc n" in realpow_ge_ge) +apply auto +done + +lemma realpow_Suc_ge_self2 [rule_format (no_asm)]: "(1::real) \ r ==> r \ r ^ Suc n" +apply (drule_tac n = "1" and N = "Suc n" in realpow_ge_ge2) +apply auto +done + +lemma realpow_ge_self: "[| (1::real) < r; 0 < n |] ==> r \ r ^ n" +apply (drule less_not_refl2 [THEN not0_implies_Suc]) +apply (auto intro!: realpow_Suc_ge_self) +done + +lemma realpow_ge_self2: "[| (1::real) \ r; 0 < n |] ==> r \ r ^ n" +apply (drule less_not_refl2 [THEN not0_implies_Suc]) +apply (auto intro!: realpow_Suc_ge_self2) +done + +lemma realpow_minus_mult [rule_format (no_asm)]: "0 < n --> (x::real) ^ (n - 1) * x = x ^ n" +apply (induct_tac "n") +apply (auto simp add: real_mult_commute) +done +declare realpow_minus_mult [simp] + +lemma realpow_two_mult_inverse: "r \ 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)" +apply (simp (no_asm_simp) add: realpow_two real_mult_assoc [symmetric]) +done +declare realpow_two_mult_inverse [simp] + +(* 05/00 *) +lemma realpow_two_minus: "(-x)^Suc (Suc 0) = (x::real)^Suc (Suc 0)" +apply (simp (no_asm)) +done +declare realpow_two_minus [simp] + +lemma realpow_two_diff: "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)" +apply (unfold real_diff_def) +apply (simp add: real_add_mult_distrib2 real_add_mult_distrib real_mult_ac) +done + +lemma realpow_two_disj: "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)" +apply (cut_tac x = "x" and y = "y" in realpow_two_diff) +apply (auto simp del: realpow_Suc) +done + +(* used in Transc *) +lemma realpow_diff: "[|(x::real) \ 0; m \ n |] ==> x ^ (n - m) = x ^ n * inverse (x ^ m)" +apply (auto simp add: le_eq_less_or_eq less_iff_Suc_add realpow_add realpow_not_zero real_mult_ac) +done + +lemma realpow_real_of_nat: "real (m::nat) ^ n = real (m ^ n)" +apply (induct_tac "n") +apply (auto simp add: real_of_nat_one real_of_nat_mult) +done + +lemma realpow_real_of_nat_two_pos: "0 < real (Suc (Suc 0) ^ n)" +apply (induct_tac "n") +apply (auto simp add: real_of_nat_mult real_0_less_mult_iff) +done +declare realpow_real_of_nat_two_pos [simp] + +lemma realpow_increasing: + assumes xnonneg: "(0::real) \ x" + and ynonneg: "0 \ y" + and le: "x ^ Suc n \ y ^ Suc n" + shows "x \ y" + proof (rule ccontr) + assume "~ x \ y" + then have "y x; 0 \ y; x ^ Suc n = y ^ Suc n |] ==> x = y" +apply (blast intro: realpow_increasing order_antisym order_eq_refl sym) +done + + +(*** Logical equivalences for inequalities ***) + +lemma realpow_eq_0_iff: "(x^n = 0) = (x = (0::real) & 0 (0::real) | n=0)" +apply (induct_tac "n") +apply (auto simp add: real_0_less_mult_iff) +done +declare zero_less_realpow_abs_iff [simp] + +lemma zero_le_realpow_abs: "(0::real) \ (abs x)^n" +apply (induct_tac "n") +apply (auto simp add: real_0_le_mult_iff) +done +declare zero_le_realpow_abs [simp] + + +(*** Literal arithmetic involving powers, type real ***) + +lemma real_of_int_power: "real (x::int) ^ n = real (x ^ n)" +apply (induct_tac "n") +apply (simp_all (no_asm_simp) add: nat_mult_distrib) +done +declare real_of_int_power [symmetric, simp] + +lemma power_real_number_of: "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)" +apply (simp only: real_number_of_def real_of_int_power) +done + +declare power_real_number_of [of _ "number_of w", standard, simp] + + +lemma real_power_two: "(r::real)\ = r * r" + by (simp add: numeral_2_eq_2) + +lemma real_sqr_ge_zero [iff]: "0 \ (r::real)\" + by (simp add: real_power_two) + +lemma real_sqr_gt_zero: "(r::real) \ 0 ==> 0 < r\" +proof - + assume "r \ 0" + hence "0 \ r\" by simp + also have "0 \ r\" by (simp add: real_sqr_ge_zero) + finally show ?thesis . +qed + +lemma real_sqr_not_zero: "r \ 0 ==> (r::real)\ \ 0" + by simp + + +ML +{* +val realpow_0 = thm "realpow_0"; +val realpow_Suc = thm "realpow_Suc"; + +val realpow_zero = thm "realpow_zero"; +val realpow_not_zero = thm "realpow_not_zero"; +val realpow_zero_zero = thm "realpow_zero_zero"; +val realpow_inverse = thm "realpow_inverse"; +val realpow_abs = thm "realpow_abs"; +val realpow_add = thm "realpow_add"; +val realpow_one = thm "realpow_one"; +val realpow_two = thm "realpow_two"; +val realpow_gt_zero = thm "realpow_gt_zero"; +val realpow_ge_zero = thm "realpow_ge_zero"; +val realpow_le = thm "realpow_le"; +val realpow_0_left = thm "realpow_0_left"; +val realpow_less = thm "realpow_less"; +val realpow_eq_one = thm "realpow_eq_one"; +val abs_realpow_minus_one = thm "abs_realpow_minus_one"; +val realpow_mult = thm "realpow_mult"; +val realpow_two_le = thm "realpow_two_le"; +val abs_realpow_two = thm "abs_realpow_two"; +val realpow_two_abs = thm "realpow_two_abs"; +val realpow_two_gt_one = thm "realpow_two_gt_one"; +val realpow_ge_one = thm "realpow_ge_one"; +val realpow_ge_one2 = thm "realpow_ge_one2"; +val two_realpow_ge_one = thm "two_realpow_ge_one"; +val two_realpow_gt = thm "two_realpow_gt"; +val realpow_minus_one = thm "realpow_minus_one"; +val realpow_minus_one_odd = thm "realpow_minus_one_odd"; +val realpow_minus_one_even = thm "realpow_minus_one_even"; +val realpow_Suc_less = thm "realpow_Suc_less"; +val realpow_Suc_le = thm "realpow_Suc_le"; +val realpow_zero_le = thm "realpow_zero_le"; +val realpow_Suc_le2 = thm "realpow_Suc_le2"; +val realpow_Suc_le3 = thm "realpow_Suc_le3"; +val realpow_less_le = thm "realpow_less_le"; +val realpow_le_le = thm "realpow_le_le"; +val realpow_Suc_le_self = thm "realpow_Suc_le_self"; +val realpow_Suc_less_one = thm "realpow_Suc_less_one"; +val realpow_le_Suc = thm "realpow_le_Suc"; +val realpow_less_Suc = thm "realpow_less_Suc"; +val realpow_le_Suc2 = thm "realpow_le_Suc2"; +val realpow_gt_ge = thm "realpow_gt_ge"; +val realpow_gt_ge2 = thm "realpow_gt_ge2"; +val realpow_ge_ge = thm "realpow_ge_ge"; +val realpow_ge_ge2 = thm "realpow_ge_ge2"; +val realpow_Suc_ge_self = thm "realpow_Suc_ge_self"; +val realpow_Suc_ge_self2 = thm "realpow_Suc_ge_self2"; +val realpow_ge_self = thm "realpow_ge_self"; +val realpow_ge_self2 = thm "realpow_ge_self2"; +val realpow_minus_mult = thm "realpow_minus_mult"; +val realpow_two_mult_inverse = thm "realpow_two_mult_inverse"; +val realpow_two_minus = thm "realpow_two_minus"; +val realpow_two_diff = thm "realpow_two_diff"; +val realpow_two_disj = thm "realpow_two_disj"; +val realpow_diff = thm "realpow_diff"; +val realpow_real_of_nat = thm "realpow_real_of_nat"; +val realpow_real_of_nat_two_pos = thm "realpow_real_of_nat_two_pos"; +val realpow_increasing = thm "realpow_increasing"; +val realpow_Suc_cancel_eq = thm "realpow_Suc_cancel_eq"; +val realpow_eq_0_iff = thm "realpow_eq_0_iff"; +val zero_less_realpow_abs_iff = thm "zero_less_realpow_abs_iff"; +val zero_le_realpow_abs = thm "zero_le_realpow_abs"; +val real_of_int_power = thm "real_of_int_power"; +val power_real_number_of = thm "power_real_number_of"; +val real_power_two = thm "real_power_two"; +val real_sqr_ge_zero = thm "real_sqr_ge_zero"; +val real_sqr_gt_zero = thm "real_sqr_gt_zero"; +val real_sqr_not_zero = thm "real_sqr_not_zero"; +*} + + end diff -r 3d0c6238162a -r 95b42e69436c src/HOL/Ring_and_Field.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Ring_and_Field.thy Fri Nov 21 11:15:40 2003 +0100 @@ -0,0 +1,382 @@ +(* Title: HOL/Ring_and_Field.thy + ID: $Id$ + Author: Gertrud Bauer and Markus Wenzel, TU Muenchen + License: GPL (GNU GENERAL PUBLIC LICENSE) +*) + +header {* + \title{Ring and field structures} + \author{Gertrud Bauer and Markus Wenzel} +*} + +theory Ring_and_Field = Inductive: + +text{*Lemmas and extension to semirings by L. C. Paulson*} + +subsection {* Abstract algebraic structures *} + +axclass semiring \ zero, one, plus, times + add_assoc: "(a + b) + c = a + (b + c)" + add_commute: "a + b = b + a" + left_zero [simp]: "0 + a = a" + + mult_assoc: "(a * b) * c = a * (b * c)" + mult_commute: "a * b = b * a" + left_one [simp]: "1 * a = a" + + left_distrib: "(a + b) * c = a * c + b * c" + zero_neq_one [simp]: "0 \ 1" + +axclass ring \ semiring, minus + left_minus [simp]: "- a + a = 0" + diff_minus: "a - b = a + (-b)" + +axclass ordered_semiring \ semiring, linorder + add_left_mono: "a \ b ==> c + a \ c + b" + mult_strict_left_mono: "a < b ==> 0 < c ==> c * a < c * b" + +axclass ordered_ring \ ordered_semiring, ring + abs_if: "\a\ = (if a < 0 then -a else a)" + +axclass field \ ring, inverse + left_inverse [simp]: "a \ 0 ==> inverse a * a = 1" + divide_inverse: "b \ 0 ==> a / b = a * inverse b" + +axclass ordered_field \ ordered_ring, field + +axclass division_by_zero \ zero, inverse + inverse_zero: "inverse 0 = 0" + divide_zero: "a / 0 = 0" + + +subsection {* Derived rules for addition *} + +lemma right_zero [simp]: "a + 0 = (a::'a::semiring)" +proof - + have "a + 0 = 0 + a" by (simp only: add_commute) + also have "... = a" by simp + finally show ?thesis . +qed + +lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::semiring))" + by (rule mk_left_commute [of "op +", OF add_assoc add_commute]) + +theorems add_ac = add_assoc add_commute add_left_commute + +lemma right_minus [simp]: "a + -(a::'a::ring) = 0" +proof - + have "a + -a = -a + a" by (simp add: add_ac) + also have "... = 0" by simp + finally show ?thesis . +qed + +lemma right_minus_eq: "(a - b = 0) = (a = (b::'a::ring))" +proof + have "a = a - b + b" by (simp add: diff_minus add_ac) + also assume "a - b = 0" + finally show "a = b" by simp +next + assume "a = b" + 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 + assume eq: "a + b = a + c" + then have "(-a + a) + b = (-a + a) + c" + by (simp only: eq add_assoc) + then show "b = c" by simp +next + assume eq: "b = c" + then show "a + b = a + c" by simp +qed + +lemma add_right_cancel [simp]: + "(b + a = c + a) = (b = (c::'a::ring))" + by (simp add: add_commute) + +lemma minus_minus [simp]: "- (- (a::'a::ring)) = a" + proof (rule add_left_cancel [of "-a", THEN iffD1]) + show "(-a + -(-a) = -a + a)" + by simp + qed + +lemma equals_zero_I: "a+b = 0 ==> -a = (b::'a::ring)" +apply (rule right_minus_eq [THEN iffD1, symmetric]) +apply (simp add: diff_minus add_commute) +done + +lemma minus_zero [simp]: "- 0 = (0::'a::ring)" +by (simp add: equals_zero_I) + +lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::ring))" + proof + assume "- a = - b" + then have "- (- a) = - (- b)" + by simp + then show "a=b" + by simp + next + assume "a=b" + then show "-a = -b" + by simp + qed + +lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::ring))" +by (subst neg_equal_iff_equal [symmetric], simp) + +lemma neg_0_equal_iff_equal [simp]: "(0 = -a) = (0 = (a::'a::ring))" +by (subst neg_equal_iff_equal [symmetric], simp) + + +subsection {* Derived rules for multiplication *} + +lemma right_one [simp]: "a = a * (1::'a::semiring)" +proof - + have "a = 1 * a" by simp + also have "... = a * 1" by (simp add: mult_commute) + finally show ?thesis . +qed + +lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::semiring))" + by (rule mk_left_commute [of "op *", OF mult_assoc mult_commute]) + +theorems mult_ac = mult_assoc mult_commute mult_left_commute + +lemma right_inverse [simp]: "a \ 0 ==> a * inverse (a::'a::field) = 1" +proof - + have "a * inverse a = inverse a * a" by (simp add: mult_ac) + also assume "a \ 0" + hence "inverse a * a = 1" by simp + finally show ?thesis . +qed + +lemma right_inverse_eq: "b \ 0 ==> (a / b = 1) = (a = (b::'a::field))" +proof + assume neq: "b \ 0" + { + hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac) + also assume "a / b = 1" + finally show "a = b" by simp + next + assume "a = b" + with neq show "a / b = 1" by (simp add: divide_inverse) + } +qed + +lemma divide_self [simp]: "a \ 0 ==> a / (a::'a::field) = 1" + by (simp add: divide_inverse) + +lemma mult_left_zero [simp]: "0 * a = (0::'a::ring)" +proof - + have "0*a + 0*a = 0*a + 0" + by (simp add: left_distrib [symmetric]) + then show ?thesis by (simp only: add_left_cancel) +qed + +lemma mult_right_zero [simp]: "a * 0 = (0::'a::ring)" + by (simp add: mult_commute) + + +subsection {* Distribution rules *} + +lemma right_distrib: "a * (b + c) = a * b + a * (c::'a::semiring)" +proof - + have "a * (b + c) = (b + c) * a" by (simp add: mult_ac) + also have "... = b * a + c * a" by (simp only: left_distrib) + also have "... = a * b + a * c" by (simp add: mult_ac) + finally show ?thesis . +qed + +theorems ring_distrib = right_distrib left_distrib + +lemma minus_add_distrib [simp]: "- (a + b) = -a + -(b::'a::ring)" +apply (rule equals_zero_I) +apply (simp add: add_ac) +done + +lemma minus_mult_left: "- (a * b) = (-a) * (b::'a::ring)" +apply (rule equals_zero_I) +apply (simp add: left_distrib [symmetric]) +done + +lemma minus_mult_right: "- (a * b) = a * -(b::'a::ring)" +apply (rule equals_zero_I) +apply (simp add: right_distrib [symmetric]) +done + +lemma right_diff_distrib: "a * (b - c) = a * b - a * (c::'a::ring)" +by (simp add: right_distrib diff_minus + minus_mult_left [symmetric] minus_mult_right [symmetric]) + + +subsection {* Ordering rules *} + +lemma add_right_mono: "a \ (b::'a::ordered_semiring) ==> a + c \ b + c" +by (simp add: add_commute [of _ c] add_left_mono) + +lemma le_imp_neg_le: + assumes "a \ (b::'a::ordered_ring)" shows "-b \ -a" + proof - + have "-a+a \ -a+b" + by (rule add_left_mono) + then have "0 \ -a+b" + by simp + then have "0 + (-b) \ (-a + b) + (-b)" + by (rule add_right_mono) + then show ?thesis + by (simp add: add_assoc) + qed + +lemma neg_le_iff_le [simp]: "(-b \ -a) = (a \ (b::'a::ordered_ring))" + proof + assume "- b \ - a" + then have "- (- a) \ - (- b)" + by (rule le_imp_neg_le) + then show "a\b" + by simp + next + assume "a\b" + then show "-b \ -a" + by (rule le_imp_neg_le) + qed + +lemma neg_le_0_iff_le [simp]: "(-a \ 0) = (0 \ (a::'a::ordered_ring))" +by (subst neg_le_iff_le [symmetric], simp) + +lemma neg_0_le_iff_le [simp]: "(0 \ -a) = (a \ (0::'a::ordered_ring))" +by (subst neg_le_iff_le [symmetric], simp) + +lemma neg_less_iff_less [simp]: "(-b < -a) = (a < (b::'a::ordered_ring))" +by (force simp add: order_less_le) + +lemma neg_less_0_iff_less [simp]: "(-a < 0) = (0 < (a::'a::ordered_ring))" +by (subst neg_less_iff_less [symmetric], simp) + +lemma neg_0_less_iff_less [simp]: "(0 < -a) = (a < (0::'a::ordered_ring))" +by (subst neg_less_iff_less [symmetric], simp) + +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) + +lemma mult_left_mono: + "[|a \ b; 0 < c|] ==> c * a \ c * (b::'a::ordered_semiring)" +by (force simp add: mult_strict_left_mono order_le_less) + +lemma mult_right_mono: + "[|a \ b; 0 < c|] ==> a*c \ b * (c::'a::ordered_semiring)" +by (force simp add: mult_strict_right_mono order_le_less) + +lemma mult_strict_left_mono_neg: + "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring)" +apply (drule mult_strict_left_mono [of _ _ "-c"]) +apply (simp_all add: minus_mult_left [symmetric]) +done + +lemma mult_strict_right_mono_neg: + "[|b < a; c < 0|] ==> a * c < b * (c::'a::ordered_ring)" +apply (drule mult_strict_right_mono [of _ _ "-c"]) +apply (simp_all add: minus_mult_right [symmetric]) +done + +lemma mult_left_mono_neg: + "[|b \ a; c < 0|] ==> c * a \ c * (b::'a::ordered_ring)" +by (force simp add: mult_strict_left_mono_neg order_le_less) + +lemma mult_right_mono_neg: + "[|b \ a; c < 0|] ==> a * c \ b * (c::'a::ordered_ring)" +by (force simp add: mult_strict_right_mono_neg order_le_less) + + +subsection{* Products of Signs *} + +lemma mult_pos: "[| (0::'a::ordered_ring) < a; 0 < b |] ==> 0 < a*b" +by (drule mult_strict_left_mono [of 0 b], auto) + +lemma mult_pos_neg: "[| (0::'a::ordered_ring) < a; b < 0 |] ==> a*b < 0" +by (drule mult_strict_left_mono [of b 0], auto) + +lemma mult_neg: "[| a < (0::'a::ordered_ring); b < 0 |] ==> 0 < a*b" +by (drule mult_strict_right_mono_neg, auto) + +lemma zero_less_mult_pos: "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::ordered_ring)" +apply (case_tac "b\0") + apply (auto simp add: order_le_less linorder_not_less) +apply (drule_tac mult_pos_neg [of a b]) + apply (auto dest: order_less_not_sym) +done + +lemma zero_less_mult_iff: + "((0::'a::ordered_ring) < a*b) = (0 < a & 0 < b | a < 0 & b < 0)" +apply (auto simp add: order_le_less linorder_not_less mult_pos mult_neg) +apply (blast dest: zero_less_mult_pos) +apply (simp add: mult_commute [of a b]) +apply (blast dest: zero_less_mult_pos) +done + + +lemma mult_eq_0_iff [iff]: "(a*b = (0::'a::ordered_ring)) = (a = 0 | b = 0)" +apply (case_tac "a < 0") +apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff) +apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+ +done + +lemma zero_le_mult_iff: + "((0::'a::ordered_ring) \ a*b) = (0 \ a & 0 \ b | a \ 0 & b \ 0)" +by (auto simp add: eq_commute [of 0] order_le_less linorder_not_less + zero_less_mult_iff) + +lemma mult_less_0_iff: + "(a*b < (0::'a::ordered_ring)) = (0 < a & b < 0 | a < 0 & 0 < b)" +apply (insert zero_less_mult_iff [of "-a" b]) +apply (force simp add: minus_mult_left[symmetric]) +done + +lemma mult_le_0_iff: + "(a*b \ (0::'a::ordered_ring)) = (0 \ a & b \ 0 | a \ 0 & 0 \ b)" +apply (insert zero_le_mult_iff [of "-a" b]) +apply (force simp add: minus_mult_left[symmetric]) +done + +lemma zero_le_square: "(0::'a::ordered_ring) \ a*a" +by (simp add: zero_le_mult_iff linorder_linear) + +lemma zero_less_one: "(0::'a::ordered_ring) < 1" +apply (insert zero_le_square [of 1]) +apply (simp add: order_less_le) +done + + +subsection {* Absolute Value *} + +text{*But is it really better than just rewriting with @{text abs_if}?*} +lemma abs_split: + "P(abs(a::'a::ordered_ring)) = ((0 \ a --> P a) & (a < 0 --> P(-a)))" +by (force dest: order_less_le_trans simp add: abs_if linorder_not_less) + +lemma abs_zero [simp]: "abs 0 = (0::'a::ordered_ring)" +by (simp add: abs_if) + +lemma abs_mult: "abs (x * y) = abs x * abs (y::'a::ordered_ring)" +apply (case_tac "x=0 | y=0", force) +apply (auto elim: order_less_asym + simp add: abs_if mult_less_0_iff linorder_neq_iff + minus_mult_left [symmetric] minus_mult_right [symmetric]) +done + +lemma abs_eq_0 [iff]: "(abs x = 0) = (x = (0::'a::ordered_ring))" +by (simp add: abs_if) + +lemma zero_less_abs_iff [iff]: "(0 < abs x) = (x ~= (0::'a::ordered_ring))" +by (simp add: abs_if linorder_neq_iff) + + +subsection {* Fields *} + + +end