# HG changeset patch # User obua # Date 1084299068 -7200 # Node ID 83f1a514dcb4648deb6c5c22aea9943e32846cca # Parent 77ea79aed99d84ee8843b024b544b8d4f11d075f changes made due to new Ring_and_Field theory diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Algebra/abstract/Ring.ML --- a/src/HOL/Algebra/abstract/Ring.ML Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Algebra/abstract/Ring.ML Tue May 11 20:11:08 2004 +0200 @@ -5,9 +5,9 @@ *) (* -val a_assoc = thm "plus_ac0.assoc"; -val l_zero = thm "plus_ac0.zero"; -val a_comm = thm "plus_ac0.commute"; +val a_assoc = thm "semigroup_add.add_assoc"; +val l_zero = thm "comm_monoid_add.add_0"; +val a_comm = thm "ab_semigroup_add.add_commute"; section "Rings"; diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Algebra/abstract/Ring.thy --- a/src/HOL/Algebra/abstract/Ring.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Algebra/abstract/Ring.thy Tue May 11 20:11:08 2004 +0200 @@ -117,37 +117,37 @@ (* Basic facts --- move to HOL!!! *) -lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::plus_ac0)" +lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::comm_monoid_add)" by simp lemma natsum_Suc [simp]: - "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::plus_ac0)" + "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::comm_monoid_add)" by (simp add: atMost_Suc) lemma natsum_Suc2: - "setsum f {..Suc n} = (setsum (%i. f (Suc i)) {..n} + f 0::'a::plus_ac0)" + "setsum f {..Suc n} = (setsum (%i. f (Suc i)) {..n} + f 0::'a::comm_monoid_add)" proof (induct n) case 0 show ?case by simp next - case Suc thus ?case by (simp add: plus_ac0.assoc) + case Suc thus ?case by (simp add: semigroup_add.add_assoc) qed lemma natsum_cong [cong]: - "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::plus_ac0) |] ==> + "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::comm_monoid_add) |] ==> setsum f {..j} = setsum g {..k}" by (induct j) auto -lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::plus_ac0)" +lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::comm_monoid_add)" by (induct n) simp_all lemma natsum_add [simp]: - "!!f::nat=>'a::plus_ac0. + "!!f::nat=>'a::comm_monoid_add. setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}" -by (induct n) (simp_all add: plus_ac0) +by (induct n) (simp_all add: add_ac) (* Facts specific to rings *) -instance ring < plus_ac0 +instance ring < comm_monoid_add proof fix x y z show "(x::'a::ring) + y = y + x" by (rule a_comm) diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Algebra/poly/LongDiv.thy --- a/src/HOL/Algebra/poly/LongDiv.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Algebra/poly/LongDiv.thy Tue May 11 20:11:08 2004 +0200 @@ -22,7 +22,7 @@ apply (simp) apply (force) apply (simp) - apply (subst plus_ac0.commute[of m]) + apply (subst ab_semigroup_add.add_commute[of m]) apply (simp) done diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Complex/CLim.thy --- a/src/HOL/Complex/CLim.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Complex/CLim.thy Tue May 11 20:11:08 2004 +0200 @@ -17,7 +17,7 @@ by (simp add: numeral_2_eq_2) text{*Changing the quantified variable. Install earlier?*} -lemma all_shift: "(\x::'a::ring. P x) = (\x. P (x-a))"; +lemma all_shift: "(\x::'a::comm_ring_1. P x) = (\x. P (x-a))"; apply auto apply (drule_tac x="x+a" in spec) apply (simp add: diff_minus add_assoc) diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Complex/NSComplex.thy --- a/src/HOL/Complex/NSComplex.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Complex/NSComplex.thy Tue May 11 20:11:08 2004 +0200 @@ -412,7 +412,7 @@ lemma hcomplex_add_minus_eq_minus: "x + y = (0::hcomplex) ==> x = -y" -apply (drule Ring_and_Field.equals_zero_I) +apply (drule OrderedGroup.equals_zero_I) apply (simp add: minus_equation_iff [of x y]) done @@ -429,7 +429,7 @@ subsection{*More Multiplication Laws*} lemma hcomplex_mult_one_right: "z * (1::hcomplex) = z" -by (rule Ring_and_Field.mult_1_right) +by (rule OrderedGroup.mult_1_right) lemma hcomplex_mult_minus_one [simp]: "- 1 * (z::hcomplex) = -z" by simp @@ -454,7 +454,7 @@ by (simp add: hcomplex_diff_def hcomplex_minus hcomplex_add complex_diff_def) lemma hcomplex_diff_eq_eq [simp]: "((x::hcomplex) - y = z) = (x = z + y)" -by (rule Ring_and_Field.diff_eq_eq) +by (rule OrderedGroup.diff_eq_eq) lemma hcomplex_add_divide_distrib: "(x+y)/(z::hcomplex) = x/z + y/z" by (rule Ring_and_Field.add_divide_distrib) diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Finite_Set.thy Tue May 11 20:11:08 2004 +0200 @@ -742,15 +742,15 @@ subsection {* Generalized summation over a set *} constdefs - setsum :: "('a => 'b) => 'a set => 'b::plus_ac0" + setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add" "setsum f A == if finite A then fold (op + o f) 0 A else 0" syntax - "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("(3\_:_. _)" [0, 51, 10] 10) + "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add" ("(3\_:_. _)" [0, 51, 10] 10) syntax (xsymbols) - "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("(3\_\_. _)" [0, 51, 10] 10) + "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add" ("(3\_\_. _)" [0, 51, 10] 10) syntax (HTML output) - "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("(3\_\_. _)" [0, 51, 10] 10) + "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add" ("(3\_\_. _)" [0, 51, 10] 10) translations "\i:A. b" == "setsum (%i. b) A" -- {* Beware of argument permutation! *} @@ -761,7 +761,7 @@ lemma setsum_insert [simp]: "finite F ==> a \ F ==> setsum f (insert a F) = f a + setsum f F" by (simp add: setsum_def - LC.fold_insert [OF LC.intro] plus_ac0_left_commute) + LC.fold_insert [OF LC.intro] add_left_commute) lemma setsum_reindex [rule_format]: "finite B ==> inj_on f B --> setsum h (f ` B) = setsum (h \ f) B" @@ -820,7 +820,7 @@ ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B" -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *} apply (induct set: Finites, simp) - apply (simp add: plus_ac0 Int_insert_left insert_absorb) + apply (simp add: add_ac Int_insert_left insert_absorb) done lemma setsum_Un_disjoint: "finite A ==> finite B @@ -874,7 +874,7 @@ apply (case_tac "finite A") prefer 2 apply (simp add: setsum_def) apply (erule finite_induct, auto) - apply (simp add: plus_ac0) + apply (simp add: add_ac) done subsubsection {* Properties in more restricted classes of structures *} @@ -892,18 +892,18 @@ lemma setsum_constant_nat [simp]: "finite A ==> (\x: A. y) = (card A) * y" - -- {* Later generalized to any semiring. *} + -- {* Later generalized to any comm_semiring_1_cancel. *} by (erule finite_induct, auto) lemma setsum_Un: "finite A ==> finite B ==> (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)" -- {* For the natural numbers, we have subtraction. *} - by (subst setsum_Un_Int [symmetric], auto) + by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps) lemma setsum_Un_ring: "finite A ==> finite B ==> - (setsum f (A Un B) :: 'a :: ring) = + (setsum f (A Un B) :: 'a :: comm_ring_1) = setsum f A + setsum f B - setsum f (A Int B)" - by (subst setsum_Un_Int [symmetric], auto) + by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps) lemma setsum_diff1: "(setsum f (A - {a}) :: nat) = (if a:A then setsum f A - f a else setsum f A)" @@ -914,16 +914,16 @@ apply (drule_tac a = a in mk_disjoint_insert, auto) done -lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ring) A = +lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::comm_ring_1) A = - setsum f A" by (induct set: Finites, auto) -lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ring) - g x) A = +lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::comm_ring_1) - g x) A = setsum f A - setsum g A" by (simp add: diff_minus setsum_addf setsum_negf) lemma setsum_nonneg: "[| finite A; - \x \ A. (0::'a::ordered_semiring) \ f x |] ==> + \x \ A. (0::'a::ordered_semidom) \ f x |] ==> 0 \ setsum f A"; apply (induct set: Finites, auto) apply (subgoal_tac "0 + 0 \ f x + setsum f F", simp) @@ -983,16 +983,16 @@ subsection {* Generalized product over a set *} constdefs - setprod :: "('a => 'b) => 'a set => 'b::times_ac1" + setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult" "setprod f A == if finite A then fold (op * o f) 1 A else 1" syntax - "_setprod" :: "idt => 'a set => 'b => 'b::times_ac1" ("(3\_:_. _)" [0, 51, 10] 10) + "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3\_:_. _)" [0, 51, 10] 10) syntax (xsymbols) - "_setprod" :: "idt => 'a set => 'b => 'b::times_ac1" ("(3\_\_. _)" [0, 51, 10] 10) + "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3\_\_. _)" [0, 51, 10] 10) syntax (HTML output) - "_setprod" :: "idt => 'a set => 'b => 'b::times_ac1" ("(3\_\_. _)" [0, 51, 10] 10) + "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3\_\_. _)" [0, 51, 10] 10) translations "\i:A. b" == "setprod (%i. b) A" -- {* Beware of argument permutation! *} @@ -1002,7 +1002,7 @@ lemma setprod_insert [simp]: "[| finite A; a \ A |] ==> setprod f (insert a A) = f a * setprod f A" by (auto simp add: setprod_def LC_def LC.fold_insert - times_ac1_left_commute) + mult_left_commute) lemma setprod_reindex [rule_format]: "finite B ==> inj_on f B --> setprod h (f ` B) = setprod (h \ f) B" @@ -1043,7 +1043,7 @@ lemma setprod_1: "setprod (%i. 1) A = 1" apply (case_tac "finite A") - apply (erule finite_induct, auto simp add: times_ac1) + apply (erule finite_induct, auto simp add: mult_ac) apply (simp add: setprod_def) done @@ -1056,13 +1056,13 @@ lemma setprod_Un_Int: "finite A ==> finite B ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B" apply (induct set: Finites, simp) - apply (simp add: times_ac1 insert_absorb) - apply (simp add: times_ac1 Int_insert_left insert_absorb) + apply (simp add: mult_ac insert_absorb) + apply (simp add: mult_ac Int_insert_left insert_absorb) done lemma setprod_Un_disjoint: "finite A ==> finite B ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B" - apply (subst setprod_Un_Int [symmetric], auto simp add: times_ac1) + apply (subst setprod_Un_Int [symmetric], auto simp add: mult_ac) done lemma setprod_UN_disjoint: @@ -1110,9 +1110,9 @@ lemma setprod_timesf: "setprod (%x. f x * g x) A = (setprod f A * setprod g A)" apply (case_tac "finite A") - prefer 2 apply (simp add: setprod_def times_ac1) + prefer 2 apply (simp add: setprod_def mult_ac) apply (erule finite_induct, auto) - apply (simp add: times_ac1) + apply (simp add: mult_ac) done subsubsection {* Properties in more restricted classes of structures *} @@ -1127,13 +1127,13 @@ apply (auto simp add: power_Suc) done -lemma setprod_zero: "finite A ==> EX x: A. f x = (0::'a::semiring) ==> +lemma setprod_zero: "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0" apply (induct set: Finites, force, clarsimp) apply (erule disjE, auto) done -lemma setprod_nonneg [rule_format]: "(ALL x: A. (0::'a::ordered_ring) \ f x) +lemma setprod_nonneg [rule_format]: "(ALL x: A. (0::'a::ordered_idom) \ f x) --> 0 \ setprod f A" apply (case_tac "finite A") apply (induct set: Finites, force, clarsimp) @@ -1142,7 +1142,7 @@ apply (auto simp add: setprod_def) done -lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_ring) < f x) +lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x) --> 0 < setprod f A" apply (case_tac "finite A") apply (induct set: Finites, force, clarsimp) @@ -1152,13 +1152,13 @@ done lemma setprod_nonzero [rule_format]: - "(ALL x y. (x::'a::semiring) * y = 0 --> x = 0 | y = 0) ==> + "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==> finite A ==> (ALL x: A. f x \ (0::'a)) --> setprod f A \ 0" apply (erule finite_induct, auto) done lemma setprod_zero_eq: - "(ALL x y. (x::'a::semiring) * y = 0 --> x = 0 | y = 0) ==> + "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==> finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)" apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast) done diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Hyperreal/HyperDef.thy --- a/src/HOL/Hyperreal/HyperDef.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Hyperreal/HyperDef.thy Tue May 11 20:11:08 2004 +0200 @@ -332,7 +332,7 @@ lemma hypreal_add_zero_left: "(0::hypreal) + z = z" by (cases z, simp add: hypreal_zero_def hypreal_add) -instance hypreal :: plus_ac0 +instance hypreal :: comm_monoid_add by intro_classes (assumption | rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+ @@ -423,9 +423,6 @@ instance hypreal :: field proof fix x y z :: hypreal - show "(x + y) + z = x + (y + z)" by (rule hypreal_add_assoc) - show "x + y = y + x" by (rule hypreal_add_commute) - show "0 + x = x" by simp show "- x + x = 0" by (simp add: hypreal_add_minus_left) show "x - y = x + (-y)" by (simp add: hypreal_diff_def) show "(x * y) * z = x * (y * z)" by (rule hypreal_mult_assoc) @@ -512,7 +509,7 @@ lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)" apply auto -apply (rule Ring_and_Field.add_right_cancel [of _ "-y", THEN iffD1], auto) +apply (rule OrderedGroup.add_right_cancel [of _ "-y", THEN iffD1], auto) done lemma hypreal_mult_left_cancel: "(c::hypreal) \ 0 ==> (c*a=c*b) = (a=b)" diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Hyperreal/HyperNat.thy --- a/src/HOL/Hyperreal/HyperNat.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Hyperreal/HyperNat.thy Tue May 11 20:11:08 2004 +0200 @@ -158,7 +158,7 @@ apply (simp add: hypnat_zero_def hypnat_add) done -instance hypnat :: plus_ac0 +instance hypnat :: comm_monoid_add by intro_classes (assumption | rule hypnat_add_commute hypnat_add_assoc hypnat_add_zero_left)+ @@ -280,13 +280,10 @@ declare hypnat_zero_not_eq_one [THEN not_sym, simp] -text{*The Hypernaturals Form A Semiring*} -instance hypnat :: semiring +text{*The Hypernaturals Form A comm_semiring_1_cancel*} +instance hypnat :: comm_semiring_1_cancel proof fix i j k :: hypnat - show "(i + j) + k = i + (j + k)" by (rule hypnat_add_assoc) - show "i + j = j + i" by (rule hypnat_add_commute) - show "0 + i = i" by simp show "(i * j) * k = i * (j * k)" by (rule hypnat_mult_assoc) show "i * j = j * i" by (rule hypnat_mult_commute) show "1 * i = i" by (rule hypnat_mult_1) @@ -352,9 +349,9 @@ done -subsection{*The Hypernaturals Form an Ordered Semiring*} +subsection{*The Hypernaturals Form an Ordered comm_semiring_1_cancel*} -instance hypnat :: ordered_semiring +instance hypnat :: ordered_semidom proof fix x y z :: hypnat show "0 < (1::hypnat)" @@ -456,7 +453,7 @@ qed -subsection{*The Embedding @{term hypnat_of_nat} Preserves Ring and +subsection{*The Embedding @{term hypnat_of_nat} Preserves comm_ring_1 and Order Properties*} constdefs diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Hyperreal/MacLaurin.ML --- a/src/HOL/Hyperreal/MacLaurin.ML Tue May 11 14:00:02 2004 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,717 +0,0 @@ -(* Title : MacLaurin.thy - Author : Jacques D. Fleuriot - Copyright : 2001 University of Edinburgh - Description : MacLaurin series -*) - -Goal "sumr 0 n (%m. f (m + k)) = sumr 0 (n + k) f - sumr 0 k f"; -by (induct_tac "n" 1); -by Auto_tac; -qed "sumr_offset"; - -Goal "ALL f. sumr 0 n (%m. f (m + k)) = sumr 0 (n + k) f - sumr 0 k f"; -by (induct_tac "n" 1); -by Auto_tac; -qed "sumr_offset2"; - -Goal "sumr 0 (n + k) f = sumr 0 n (%m. f (m + k)) + sumr 0 k f"; -by (simp_tac (simpset() addsimps [sumr_offset]) 1); -qed "sumr_offset3"; - -Goal "ALL n f. sumr 0 (n + k) f = sumr 0 n (%m. f (m + k)) + sumr 0 k f"; -by (simp_tac (simpset() addsimps [sumr_offset]) 1); -qed "sumr_offset4"; - -Goal "0 < n ==> \ -\ sumr (Suc 0) (Suc n) (%n. (if even(n) then 0 else \ -\ ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n) = \ -\ sumr 0 (Suc n) (%n. (if even(n) then 0 else \ -\ ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n)"; -by (res_inst_tac [("n1","1")] (sumr_split_add RS subst) 1); -by Auto_tac; -qed "sumr_from_1_from_0"; - -(*---------------------------------------------------------------------------*) -(* Maclaurin's theorem with Lagrange form of remainder *) -(*---------------------------------------------------------------------------*) - -(* Annoying: Proof is now even longer due mostly to - change in behaviour of simplifier since Isabelle99 *) -Goal " [| 0 < h; 0 < n; diff 0 = f; \ -\ ALL m t. \ -\ m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t |] \ -\ ==> EX t. 0 < t & \ -\ t < h & \ -\ f h = \ -\ sumr 0 n (%m. (diff m 0 / real (fact m)) * h ^ m) + \ -\ (diff n t / real (fact n)) * h ^ n"; -by (case_tac "n = 0" 1); -by (Force_tac 1); -by (dtac not0_implies_Suc 1); -by (etac exE 1); -by (subgoal_tac - "EX B. f h = sumr 0 n (%m. (diff m 0 / real (fact m)) * (h ^ m)) \ -\ + (B * ((h ^ n) / real (fact n)))" 1); - -by (simp_tac (HOL_ss addsimps [real_add_commute, real_divide_def, - ARITH_PROVE "(x = z + (y::real)) = (x - y = z)"]) 2); -by (res_inst_tac - [("x","(f(h) - sumr 0 n (%m. (diff(m)(0) / real (fact m)) * (h ^ m))) \ -\ * real (fact n) / (h ^ n)")] exI 2); -by (simp_tac (HOL_ss addsimps [real_mult_assoc,real_divide_def]) 2); - by (rtac (CLAIM "x = (1::real) ==> a = a * (x::real)") 2); -by (asm_simp_tac (HOL_ss addsimps - [CLAIM "(a::real) * (b * (c * d)) = (d * a) * (b * c)"] - delsimps [realpow_Suc]) 2); -by (stac left_inverse 2); -by (stac left_inverse 3); -by (rtac (real_not_refl2 RS not_sym) 2); -by (etac zero_less_power 2); -by (rtac real_of_nat_fact_not_zero 2); -by (Simp_tac 2); -by (etac exE 1); -by (cut_inst_tac [("b","%t. f t - \ -\ (sumr 0 n (%m. (diff m 0 / real (fact m)) * (t ^ m)) + \ -\ (B * ((t ^ n) / real (fact n))))")] - (CLAIM "EX g. g = b") 1); -by (etac exE 1); -by (subgoal_tac "g 0 = 0 & g h =0" 1); -by (asm_simp_tac (simpset() addsimps - [ARITH_PROVE "(x - y = z) = (x = z + (y::real))"] - delsimps [sumr_Suc]) 2); -by (cut_inst_tac [("n","m"),("k","1")] sumr_offset2 2); -by (asm_full_simp_tac (simpset() addsimps - [ARITH_PROVE "(x = y - z) = (y = x + (z::real))"] - delsimps [sumr_Suc]) 2); -by (cut_inst_tac [("b","%m t. diff m t - \ -\ (sumr 0 (n - m) (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) \ -\ + (B * ((t ^ (n - m)) / real (fact(n - m)))))")] - (CLAIM "EX difg. difg = b") 1); -by (etac exE 1); -by (subgoal_tac "difg 0 = g" 1); -by (asm_simp_tac (simpset() delsimps [realpow_Suc,fact_Suc]) 2); -by (subgoal_tac "ALL m t. m < n & 0 <= t & t <= h --> \ -\ DERIV (difg m) t :> difg (Suc m) t" 1); -by (Clarify_tac 2); -by (rtac DERIV_diff 2); -by (Asm_simp_tac 2); -by DERIV_tac; -by DERIV_tac; -by (rtac lemma_DERIV_subst 3); -by (rtac DERIV_quotient 3); -by (rtac DERIV_const 4); -by (rtac DERIV_pow 3); -by (asm_simp_tac (simpset() addsimps [inverse_mult_distrib, - CLAIM_SIMP "(a::real) * b * c * (d * e) = a * b * (c * d) * e" - mult_ac,fact_diff_Suc]) 4); -by (Asm_simp_tac 3); -by (forw_inst_tac [("m","ma")] less_add_one 2); -by (Clarify_tac 2); -by (asm_simp_tac (simpset() addsimps - [CLAIM "Suc m = ma + d + 1 ==> m - ma = d"] - delsimps [sumr_Suc]) 2); -by (asm_simp_tac (simpset() addsimps [(simplify (simpset() delsimps [sumr_Suc]) - (read_instantiate [("k","1")] sumr_offset4))] - delsimps [sumr_Suc,fact_Suc,realpow_Suc]) 2); -by (rtac lemma_DERIV_subst 2); -by (rtac DERIV_add 2); -by (rtac DERIV_const 3); -by (rtac DERIV_sumr 2); -by (Clarify_tac 2); -by (Simp_tac 3); -by (simp_tac (simpset() addsimps [real_divide_def,real_mult_assoc] - delsimps [fact_Suc,realpow_Suc]) 2); -by (rtac DERIV_cmult 2); -by (rtac lemma_DERIV_subst 2); -by DERIV_tac; -by (stac fact_Suc 2); -by (stac real_of_nat_mult 2); -by (simp_tac (simpset() addsimps [inverse_mult_distrib] @ - mult_ac) 2); -by (subgoal_tac "ALL ma. ma < n --> \ -\ (EX t. 0 < t & t < h & difg (Suc ma) t = 0)" 1); -by (rotate_tac 11 1); -by (dres_inst_tac [("x","m")] spec 1); -by (etac impE 1); -by (Asm_simp_tac 1); -by (etac exE 1); -by (res_inst_tac [("x","t")] exI 1); -by (asm_full_simp_tac (simpset() addsimps - [ARITH_PROVE "(x - y = 0) = (y = (x::real))"] - delsimps [realpow_Suc,fact_Suc]) 1); -by (subgoal_tac "ALL m. m < n --> difg m 0 = 0" 1); -by (Clarify_tac 2); -by (Asm_simp_tac 2); -by (forw_inst_tac [("m","ma")] less_add_one 2); -by (Clarify_tac 2); -by (asm_simp_tac (simpset() delsimps [sumr_Suc]) 2); -by (asm_simp_tac (simpset() addsimps [(simplify (simpset() delsimps [sumr_Suc]) - (read_instantiate [("k","1")] sumr_offset4))] - delsimps [sumr_Suc,fact_Suc,realpow_Suc]) 2); -by (subgoal_tac "ALL m. m < n --> (EX t. 0 < t & t < h & \ -\ DERIV (difg m) t :> 0)" 1); -by (rtac allI 1 THEN rtac impI 1); -by (rotate_tac 12 1); -by (dres_inst_tac [("x","ma")] spec 1); -by (etac impE 1 THEN assume_tac 1); -by (etac exE 1); -by (res_inst_tac [("x","t")] exI 1); -(* do some tidying up *) -by (ALLGOALS(thin_tac "difg = \ -\ (%m t. diff m t - \ -\ (sumr 0 (n - m) \ -\ (%p. diff (m + p) 0 / real (fact p) * t ^ p) + \ -\ B * (t ^ (n - m) / real (fact (n - m)))))")); -by (ALLGOALS(thin_tac "g = \ -\ (%t. f t - \ -\ (sumr 0 n (%m. diff m 0 / real (fact m) * t ^ m) + \ -\ B * (t ^ n / real (fact n))))")); -by (ALLGOALS(thin_tac "f h = \ -\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \ -\ B * (h ^ n / real (fact n))")); -(* back to business *) -by (Asm_simp_tac 1); -by (rtac DERIV_unique 1); -by (Blast_tac 2); -by (Force_tac 1); -by (rtac allI 1 THEN induct_tac "ma" 1); -by (rtac impI 1 THEN rtac Rolle 1); -by (assume_tac 1); -by (Asm_full_simp_tac 1); -by (Asm_full_simp_tac 1); -by (subgoal_tac "ALL t. 0 <= t & t <= h --> g differentiable t" 1); -by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1); -by (blast_tac (claset() addDs [DERIV_isCont]) 1); -by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1); -by (Clarify_tac 1); -by (res_inst_tac [("x","difg (Suc 0) t")] exI 1); -by (Force_tac 1); -by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1); -by (Clarify_tac 1); -by (res_inst_tac [("x","difg (Suc 0) x")] exI 1); -by (Force_tac 1); -by (Step_tac 1); -by (Force_tac 1); -by (subgoal_tac "EX ta. 0 < ta & ta < t & \ -\ DERIV difg (Suc n) ta :> 0" 1); -by (rtac Rolle 2 THEN assume_tac 2); -by (Asm_full_simp_tac 2); -by (rotate_tac 2 2); -by (dres_inst_tac [("x","n")] spec 2); -by (ftac (ARITH_PROVE "n < m ==> n < Suc m") 2); -by (rtac DERIV_unique 2); -by (assume_tac 3); -by (Force_tac 2); -by (subgoal_tac - "ALL ta. 0 <= ta & ta <= t --> (difg (Suc n)) differentiable ta" 2); -by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 2); -by (blast_tac (claset() addSDs [DERIV_isCont]) 2); -by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 2); -by (Clarify_tac 2); -by (res_inst_tac [("x","difg (Suc (Suc n)) ta")] exI 2); -by (Force_tac 2); -by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 2); -by (Clarify_tac 2); -by (res_inst_tac [("x","difg (Suc (Suc n)) x")] exI 2); -by (Force_tac 2); -by (Step_tac 1); -by (res_inst_tac [("x","ta")] exI 1); -by (Force_tac 1); -qed "Maclaurin"; - -Goal "0 < h & 0 < n & diff 0 = f & \ -\ (ALL m t. \ -\ m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t) \ -\ --> (EX t. 0 < t & \ -\ t < h & \ -\ f h = \ -\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \ -\ diff n t / real (fact n) * h ^ n)"; -by (blast_tac (claset() addIs [Maclaurin]) 1); -qed "Maclaurin_objl"; - -Goal " [| 0 < h; diff 0 = f; \ -\ ALL m t. \ -\ m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t |] \ -\ ==> EX t. 0 < t & \ -\ t <= h & \ -\ f h = \ -\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \ -\ diff n t / real (fact n) * h ^ n"; -by (case_tac "n" 1); -by Auto_tac; -by (dtac Maclaurin 1 THEN Auto_tac); -qed "Maclaurin2"; - -Goal "0 < h & diff 0 = f & \ -\ (ALL m t. \ -\ m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t) \ -\ --> (EX t. 0 < t & \ -\ t <= h & \ -\ f h = \ -\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \ -\ diff n t / real (fact n) * h ^ n)"; -by (blast_tac (claset() addIs [Maclaurin2]) 1); -qed "Maclaurin2_objl"; - -Goal " [| h < 0; 0 < n; diff 0 = f; \ -\ ALL m t. \ -\ m < n & h <= t & t <= 0 --> DERIV (diff m) t :> diff (Suc m) t |] \ -\ ==> EX t. h < t & \ -\ t < 0 & \ -\ f h = \ -\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \ -\ diff n t / real (fact n) * h ^ n"; -by (cut_inst_tac [("f","%x. f (-x)"), - ("diff","%n x. ((- 1) ^ n) * diff n (-x)"), - ("h","-h"),("n","n")] Maclaurin_objl 1); -by (Asm_full_simp_tac 1); -by (etac impE 1 THEN Step_tac 1); -by (stac minus_mult_right 1); -by (rtac DERIV_cmult 1); -by (rtac lemma_DERIV_subst 1); -by (rtac (read_instantiate [("g","uminus")] DERIV_chain2) 1); -by (rtac DERIV_minus 2 THEN rtac DERIV_Id 2); -by (Force_tac 2); -by (Force_tac 1); -by (res_inst_tac [("x","-t")] exI 1); -by Auto_tac; -by (rtac (CLAIM "[| x = x'; y = y' |] ==> x + y = x' + (y'::real)") 1); -by (rtac sumr_fun_eq 1); -by (Asm_full_simp_tac 1); -by (auto_tac (claset(),simpset() addsimps [real_divide_def, - CLAIM "((a * b) * c) * d = (b * c) * (a * (d::real))", - power_mult_distrib RS sym])); -qed "Maclaurin_minus"; - -Goal "(h < 0 & 0 < n & diff 0 = f & \ -\ (ALL m t. \ -\ m < n & h <= t & t <= 0 --> DERIV (diff m) t :> diff (Suc m) t))\ -\ --> (EX t. h < t & \ -\ t < 0 & \ -\ f h = \ -\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \ -\ diff n t / real (fact n) * h ^ n)"; -by (blast_tac (claset() addIs [Maclaurin_minus]) 1); -qed "Maclaurin_minus_objl"; - -(* ------------------------------------------------------------------------- *) -(* More convenient "bidirectional" version. *) -(* ------------------------------------------------------------------------- *) - -(* not good for PVS sin_approx, cos_approx *) -Goal " [| diff 0 = f; \ -\ ALL m t. \ -\ m < n & abs t <= abs x --> DERIV (diff m) t :> diff (Suc m) t |] \ -\ ==> EX t. abs t <= abs x & \ -\ f x = \ -\ sumr 0 n (%m. diff m 0 / real (fact m) * x ^ m) + \ -\ diff n t / real (fact n) * x ^ n"; -by (case_tac "n = 0" 1); -by (Force_tac 1); -by (case_tac "x = 0" 1); -by (res_inst_tac [("x","0")] exI 1); -by (Asm_full_simp_tac 1); -by (res_inst_tac [("P","0 < n")] impE 1); -by (assume_tac 2 THEN assume_tac 2); -by (induct_tac "n" 1); -by (Simp_tac 1); -by Auto_tac; -by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1); -by Auto_tac; -by (cut_inst_tac [("f","diff 0"), - ("diff","diff"), - ("h","x"),("n","n")] Maclaurin_objl 2); -by (Step_tac 2); -by (blast_tac (claset() addDs - [ARITH_PROVE "[|(0::real) <= t;t <= x |] ==> abs t <= abs x"]) 2); -by (res_inst_tac [("x","t")] exI 2); -by (force_tac (claset() addIs - [ARITH_PROVE "[| 0 < t; (t::real) < x|] ==> abs t <= abs x"],simpset()) 2); -by (cut_inst_tac [("f","diff 0"), - ("diff","diff"), - ("h","x"),("n","n")] Maclaurin_minus_objl 1); -by (Step_tac 1); -by (blast_tac (claset() addDs - [ARITH_PROVE "[|x <= t;t <= (0::real) |] ==> abs t <= abs x"]) 1); -by (res_inst_tac [("x","t")] exI 1); -by (force_tac (claset() addIs - [ARITH_PROVE "[| x < t; (t::real) < 0|] ==> abs t <= abs x"],simpset()) 1); -qed "Maclaurin_bi_le"; - -Goal "[| diff 0 = f; \ -\ ALL m x. DERIV (diff m) x :> diff(Suc m) x; \ -\ x ~= 0; 0 < n \ -\ |] ==> EX t. 0 < abs t & abs t < abs x & \ -\ f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \ -\ (diff n t / real (fact n)) * x ^ n"; -by (res_inst_tac [("x","x"),("y","0")] linorder_cases 1); -by (Blast_tac 2); -by (dtac Maclaurin_minus 1); -by (dtac Maclaurin 5); -by (TRYALL(assume_tac)); -by (Blast_tac 1); -by (Blast_tac 2); -by (Step_tac 1); -by (ALLGOALS(res_inst_tac [("x","t")] exI)); -by (Step_tac 1); -by (ALLGOALS(arith_tac)); -qed "Maclaurin_all_lt"; - -Goal "diff 0 = f & \ -\ (ALL m x. DERIV (diff m) x :> diff(Suc m) x) & \ -\ x ~= 0 & 0 < n \ -\ --> (EX t. 0 < abs t & abs t < abs x & \ -\ f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \ -\ (diff n t / real (fact n)) * x ^ n)"; -by (blast_tac (claset() addIs [Maclaurin_all_lt]) 1); -qed "Maclaurin_all_lt_objl"; - -Goal "x = (0::real) \ -\ ==> 0 < n --> \ -\ sumr 0 n (%m. (diff m (0::real) / real (fact m)) * x ^ m) = \ -\ diff 0 0"; -by (Asm_simp_tac 1); -by (induct_tac "n" 1); -by Auto_tac; -qed_spec_mp "Maclaurin_zero"; - -Goal "[| diff 0 = f; \ -\ ALL m x. DERIV (diff m) x :> diff (Suc m) x \ -\ |] ==> EX t. abs t <= abs x & \ -\ f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \ -\ (diff n t / real (fact n)) * x ^ n"; -by (cut_inst_tac [("n","n"),("m","0")] - (ARITH_PROVE "n <= m | m < (n::nat)") 1); -by (etac disjE 1); -by (Force_tac 1); -by (case_tac "x = 0" 1); -by (forw_inst_tac [("diff","diff"),("n","n")] Maclaurin_zero 1); -by (assume_tac 1); -by (dtac (gr_implies_not0 RS not0_implies_Suc) 1); -by (res_inst_tac [("x","0")] exI 1); -by (Force_tac 1); -by (forw_inst_tac [("diff","diff"),("n","n")] Maclaurin_all_lt 1); -by (TRYALL(assume_tac)); -by (Step_tac 1); -by (res_inst_tac [("x","t")] exI 1); -by Auto_tac; -qed "Maclaurin_all_le"; - -Goal "diff 0 = f & \ -\ (ALL m x. DERIV (diff m) x :> diff (Suc m) x) \ -\ --> (EX t. abs t <= abs x & \ -\ f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \ -\ (diff n t / real (fact n)) * x ^ n)"; -by (blast_tac (claset() addIs [Maclaurin_all_le]) 1); -qed "Maclaurin_all_le_objl"; - -(* ------------------------------------------------------------------------- *) -(* Version for exp. *) -(* ------------------------------------------------------------------------- *) - -Goal "[| x ~= 0; 0 < n |] \ -\ ==> (EX t. 0 < abs t & \ -\ abs t < abs x & \ -\ exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) + \ -\ (exp t / real (fact n)) * x ^ n)"; -by (cut_inst_tac [("diff","%n. exp"),("f","exp"),("x","x"),("n","n")] - Maclaurin_all_lt_objl 1); -by Auto_tac; -qed "Maclaurin_exp_lt"; - -Goal "EX t. abs t <= abs x & \ -\ exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) + \ -\ (exp t / real (fact n)) * x ^ n"; -by (cut_inst_tac [("diff","%n. exp"),("f","exp"),("x","x"),("n","n")] - Maclaurin_all_le_objl 1); -by Auto_tac; -qed "Maclaurin_exp_le"; - -(* ------------------------------------------------------------------------- *) -(* Version for sin function *) -(* ------------------------------------------------------------------------- *) - -Goal "[| a < b; ALL x. a <= x & x <= b --> DERIV f x :> f'(x) |] \ -\ ==> EX z. a < z & z < b & (f b - f a = (b - a) * f'(z))"; -by (dtac MVT 1); -by (blast_tac (claset() addIs [DERIV_isCont]) 1); -by (force_tac (claset() addDs [order_less_imp_le], - simpset() addsimps [differentiable_def]) 1); -by (blast_tac (claset() addDs [DERIV_unique,order_less_imp_le]) 1); -qed "MVT2"; - -Goal "d < (4::nat) ==> d = 0 | d = 1 | d = 2 | d = 3"; -by (case_tac "d" 1 THEN Auto_tac); -qed "lemma_exhaust_less_4"; - -bind_thm ("real_mult_le_lemma", - simplify (simpset()) (inst "b" "1" mult_right_mono)); - - -Goal "abs(sin x - \ -\ sumr 0 n (%m. (if even m then 0 \ -\ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \ -\ x ^ m)) \ -\ <= inverse(real (fact n)) * abs(x) ^ n"; -by (cut_inst_tac [("f","sin"),("n","n"),("x","x"), - ("diff","%n x. if n mod 4 = 0 then sin(x) \ -\ else if n mod 4 = 1 then cos(x) \ -\ else if n mod 4 = 2 then -sin(x) \ -\ else -cos(x)")] Maclaurin_all_le_objl 1); -by (Step_tac 1); -by (Asm_full_simp_tac 1); -by (stac mod_Suc_eq_Suc_mod 1); -by (cut_inst_tac [("m1","m")] (CLAIM "0 < (4::nat)" RS mod_less_divisor - RS lemma_exhaust_less_4) 1); -by (Step_tac 1); -by (Asm_simp_tac 1); -by (Asm_simp_tac 1); -by (Asm_simp_tac 1); -by (rtac DERIV_minus 1 THEN Simp_tac 1); -by (Asm_simp_tac 1); -by (rtac lemma_DERIV_subst 1 THEN rtac DERIV_minus 1 THEN rtac DERIV_cos 1); -by (Simp_tac 1); -by (dtac ssubst 1 THEN assume_tac 2); -by (rtac (ARITH_PROVE "[|x = y; abs u <= (v::real) |] ==> abs ((x + u) - y) <= v") 1); -by (rtac sumr_fun_eq 1); -by (Step_tac 1); -by (rtac (CLAIM "x = y ==> x * z = y * (z::real)") 1); -by (stac even_even_mod_4_iff 1); -by (cut_inst_tac [("m1","r")] (CLAIM "0 < (4::nat)" RS mod_less_divisor - RS lemma_exhaust_less_4) 1); -by (Step_tac 1); -by (Asm_simp_tac 1); -by (asm_simp_tac (simpset() addsimps [even_num_iff]) 2); -by (asm_simp_tac (simpset() addsimps [even_num_iff]) 1); -by (asm_simp_tac (simpset() addsimps [even_num_iff]) 2); -by (dtac lemma_even_mod_4_div_2 1); -by (asm_full_simp_tac (simpset() addsimps [numeral_2_eq_2,real_divide_def]) 1); -by (dtac lemma_odd_mod_4_div_2 1); -by (asm_full_simp_tac (simpset() addsimps [numeral_2_eq_2, real_divide_def]) 1); -by (auto_tac (claset() addSIs [real_mult_le_lemma,mult_right_mono], - simpset() addsimps [real_divide_def,abs_mult,abs_inverse,power_abs RS -sym])); -qed "Maclaurin_sin_bound"; - -Goal "0 < n --> Suc (Suc (2 * n - 2)) = 2*n"; -by (induct_tac "n" 1); -by Auto_tac; -qed_spec_mp "Suc_Suc_mult_two_diff_two"; -Addsimps [Suc_Suc_mult_two_diff_two]; - -Goal "0 < n --> Suc (Suc (4*n - 2)) = 4*n"; -by (induct_tac "n" 1); -by Auto_tac; -qed_spec_mp "lemma_Suc_Suc_4n_diff_2"; -Addsimps [lemma_Suc_Suc_4n_diff_2]; - -Goal "0 < n --> Suc (2 * n - 1) = 2*n"; -by (induct_tac "n" 1); -by Auto_tac; -qed_spec_mp "Suc_mult_two_diff_one"; -Addsimps [Suc_mult_two_diff_one]; - -Goal "EX t. sin x = \ -\ (sumr 0 n (%m. (if even m then 0 \ -\ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \ -\ x ^ m)) \ -\ + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"; -by (cut_inst_tac [("f","sin"),("n","n"),("x","x"), - ("diff","%n x. sin(x + 1/2*real (n)*pi)")] - Maclaurin_all_lt_objl 1); -by (Safe_tac); -by (Simp_tac 1); -by (Simp_tac 1); -by (case_tac "n" 1); -by (Clarify_tac 1); -by (Asm_full_simp_tac 1); -by (dres_inst_tac [("x","0")] spec 1 THEN Asm_full_simp_tac 1); -by (Asm_full_simp_tac 1); -by (rtac ccontr 1); -by (Asm_full_simp_tac 1); -by (dres_inst_tac [("x","x")] spec 1 THEN Asm_full_simp_tac 1); -by (dtac ssubst 1 THEN assume_tac 2); -by (res_inst_tac [("x","t")] exI 1); -by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1); -by (rtac sumr_fun_eq 1); -by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex])); -by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc])); -(*Could sin_zero_iff help?*) -qed "Maclaurin_sin_expansion"; - -Goal "EX t. abs t <= abs x & \ -\ sin x = \ -\ (sumr 0 n (%m. (if even m then 0 \ -\ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \ -\ x ^ m)) \ -\ + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"; - -by (cut_inst_tac [("f","sin"),("n","n"),("x","x"), - ("diff","%n x. sin(x + 1/2*real (n)*pi)")] - Maclaurin_all_lt_objl 1); -by (Step_tac 1); -by (Simp_tac 1); -by (Simp_tac 1); -by (case_tac "n" 1); -by (Clarify_tac 1); -by (Asm_full_simp_tac 1); -by (Asm_full_simp_tac 1); -by (rtac ccontr 1); -by (Asm_full_simp_tac 1); -by (dres_inst_tac [("x","x")] spec 1 THEN Asm_full_simp_tac 1); -by (dtac ssubst 1 THEN assume_tac 2); -by (res_inst_tac [("x","t")] exI 1); -by (rtac conjI 1); -by (arith_tac 1); -by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1); -by (rtac sumr_fun_eq 1); -by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex])); -by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc])); -qed "Maclaurin_sin_expansion2"; - -Goal "[| 0 < n; 0 < x |] ==> \ -\ EX t. 0 < t & t < x & \ -\ sin x = \ -\ (sumr 0 n (%m. (if even m then 0 \ -\ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \ -\ x ^ m)) \ -\ + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"; -by (cut_inst_tac [("f","sin"),("n","n"),("h","x"), - ("diff","%n x. sin(x + 1/2*real (n)*pi)")] - Maclaurin_objl 1); -by (Step_tac 1); -by (Asm_full_simp_tac 1); -by (Simp_tac 1); -by (dtac ssubst 1 THEN assume_tac 2); -by (res_inst_tac [("x","t")] exI 1); -by (rtac conjI 1 THEN rtac conjI 2); -by (assume_tac 1 THEN assume_tac 1); -by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1); -by (rtac sumr_fun_eq 1); -by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex])); -by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc])); -qed "Maclaurin_sin_expansion3"; - -Goal "0 < x ==> \ -\ EX t. 0 < t & t <= x & \ -\ sin x = \ -\ (sumr 0 n (%m. (if even m then 0 \ -\ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \ -\ x ^ m)) \ -\ + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"; -by (cut_inst_tac [("f","sin"),("n","n"),("h","x"), - ("diff","%n x. sin(x + 1/2*real (n)*pi)")] - Maclaurin2_objl 1); -by (Step_tac 1); -by (Asm_full_simp_tac 1); -by (Simp_tac 1); -by (dtac ssubst 1 THEN assume_tac 2); -by (res_inst_tac [("x","t")] exI 1); -by (rtac conjI 1 THEN rtac conjI 2); -by (assume_tac 1 THEN assume_tac 1); -by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1); -by (rtac sumr_fun_eq 1); -by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex])); -by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc])); -qed "Maclaurin_sin_expansion4"; - -(*-----------------------------------------------------------------------------*) -(* Maclaurin expansion for cos *) -(*-----------------------------------------------------------------------------*) - -Goal "sumr 0 (Suc n) \ -\ (%m. (if even m \ -\ then (- 1) ^ (m div 2)/(real (fact m)) \ -\ else 0) * \ -\ 0 ^ m) = 1"; -by (induct_tac "n" 1); -by Auto_tac; -qed "sumr_cos_zero_one"; -Addsimps [sumr_cos_zero_one]; - -Goal "EX t. abs t <= abs x & \ -\ cos x = \ -\ (sumr 0 n (%m. (if even m \ -\ then (- 1) ^ (m div 2)/(real (fact m)) \ -\ else 0) * \ -\ x ^ m)) \ -\ + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"; -by (cut_inst_tac [("f","cos"),("n","n"),("x","x"), - ("diff","%n x. cos(x + 1/2*real (n)*pi)")] - Maclaurin_all_lt_objl 1); -by (Step_tac 1); -by (Simp_tac 1); -by (Simp_tac 1); -by (case_tac "n" 1); -by (Asm_full_simp_tac 1); -by (asm_full_simp_tac (simpset() delsimps [sumr_Suc]) 1); -by (rtac ccontr 1); -by (Asm_full_simp_tac 1); -by (dres_inst_tac [("x","x")] spec 1 THEN Asm_full_simp_tac 1); -by (dtac ssubst 1 THEN assume_tac 2); -by (res_inst_tac [("x","t")] exI 1); -by (rtac conjI 1); -by (arith_tac 1); -by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1); -by (rtac sumr_fun_eq 1); -by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex])); -by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add] delsimps - [fact_Suc,realpow_Suc])); -by (auto_tac (claset(),simpset() addsimps [real_mult_commute])); -qed "Maclaurin_cos_expansion"; - -Goal "[| 0 < x; 0 < n |] ==> \ -\ EX t. 0 < t & t < x & \ -\ cos x = \ -\ (sumr 0 n (%m. (if even m \ -\ then (- 1) ^ (m div 2)/(real (fact m)) \ -\ else 0) * \ -\ x ^ m)) \ -\ + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"; -by (cut_inst_tac [("f","cos"),("n","n"),("h","x"), - ("diff","%n x. cos(x + 1/2*real (n)*pi)")] - Maclaurin_objl 1); -by (Step_tac 1); -by (Asm_full_simp_tac 1); -by (Simp_tac 1); -by (dtac ssubst 1 THEN assume_tac 2); -by (res_inst_tac [("x","t")] exI 1); -by (rtac conjI 1 THEN rtac conjI 2); -by (assume_tac 1 THEN assume_tac 1); -by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1); -by (rtac sumr_fun_eq 1); -by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex])); -by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add] delsimps [fact_Suc,realpow_Suc])); -by (auto_tac (claset(),simpset() addsimps [real_mult_commute])); -qed "Maclaurin_cos_expansion2"; - -Goal "[| x < 0; 0 < n |] ==> \ -\ EX t. x < t & t < 0 & \ -\ cos x = \ -\ (sumr 0 n (%m. (if even m \ -\ then (- 1) ^ (m div 2)/(real (fact m)) \ -\ else 0) * \ -\ x ^ m)) \ -\ + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"; -by (cut_inst_tac [("f","cos"),("n","n"),("h","x"), - ("diff","%n x. cos(x + 1/2*real (n)*pi)")] - Maclaurin_minus_objl 1); -by (Step_tac 1); -by (Asm_full_simp_tac 1); -by (Simp_tac 1); -by (dtac ssubst 1 THEN assume_tac 2); -by (res_inst_tac [("x","t")] exI 1); -by (rtac conjI 1 THEN rtac conjI 2); -by (assume_tac 1 THEN assume_tac 1); -by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1); -by (rtac sumr_fun_eq 1); -by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex])); -by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add] delsimps [fact_Suc,realpow_Suc])); -by (auto_tac (claset(),simpset() addsimps [real_mult_commute])); -qed "Maclaurin_minus_cos_expansion"; - -(* ------------------------------------------------------------------------- *) -(* Version for ln(1 +/- x). Where is it?? *) -(* ------------------------------------------------------------------------- *) - diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Hyperreal/MacLaurin.thy --- a/src/HOL/Hyperreal/MacLaurin.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Hyperreal/MacLaurin.thy Tue May 11 20:11:08 2004 +0200 @@ -4,4 +4,46 @@ Description : MacLaurin series *) -MacLaurin = Log +theory MacLaurin = Log +files ("MacLaurin_lemmas.ML"): + +use "MacLaurin_lemmas.ML" + +lemma Maclaurin_sin_bound: + "abs(sin x - sumr 0 n (%m. (if even m then 0 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * + x ^ m)) <= inverse(real (fact n)) * abs(x) ^ n" +proof - + have "!! x (y::real). x <= 1 \ 0 <= y \ x * y \ 1 * y" + by (rule_tac mult_right_mono,simp_all) + note est = this[simplified] + show ?thesis + apply (cut_tac f=sin and n=n and x=x and + diff = "%n x. if n mod 4 = 0 then sin(x) else if n mod 4 = 1 then cos(x) else if n mod 4 = 2 then -sin(x) else -cos(x)" + in Maclaurin_all_le_objl) + apply (tactic{* (Step_tac 1) *}) + apply (simp) + apply (subst mod_Suc_eq_Suc_mod) + apply (tactic{* cut_inst_tac [("m1","m")] (CLAIM "0 < (4::nat)" RS mod_less_divisor RS lemma_exhaust_less_4) 1*}) + apply (tactic{* Step_tac 1 *}) + apply (simp)+ + apply (rule DERIV_minus, simp+) + apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp) + apply (tactic{* dtac ssubst 1 THEN assume_tac 2 *}) + apply (tactic {* rtac (ARITH_PROVE "[|x = y; abs u <= (v::real) |] ==> abs ((x + u) - y) <= v") 1 *}) + apply (rule sumr_fun_eq) + apply (tactic{* Step_tac 1 *}) + apply (tactic{*rtac (CLAIM "x = y ==> x * z = y * (z::real)") 1*}) + apply (subst even_even_mod_4_iff) + apply (tactic{* cut_inst_tac [("m1","r")] (CLAIM "0 < (4::nat)" RS mod_less_divisor RS lemma_exhaust_less_4) 1 *}) + apply (tactic{* Step_tac 1 *}) + apply (simp) + apply (simp_all add:even_num_iff) + apply (drule lemma_even_mod_4_div_2[simplified]) + apply(simp add: numeral_2_eq_2 real_divide_def) + apply (drule lemma_odd_mod_4_div_2 ); + apply (simp add: numeral_2_eq_2 real_divide_def) + apply (auto intro: real_mult_le_lemma mult_right_mono simp add: est mult_pos_le mult_ac real_divide_def abs_mult abs_inverse power_abs[symmetric]) + done +qed + +end \ No newline at end of file diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Hyperreal/MacLaurin_lemmas.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hyperreal/MacLaurin_lemmas.ML Tue May 11 20:11:08 2004 +0200 @@ -0,0 +1,672 @@ +(* Title : MacLaurin.thy + Author : Jacques D. Fleuriot + Copyright : 2001 University of Edinburgh + Description : MacLaurin series +*) + +Goal "sumr 0 n (%m. f (m + k)) = sumr 0 (n + k) f - sumr 0 k f"; +by (induct_tac "n" 1); +by Auto_tac; +qed "sumr_offset"; + +Goal "ALL f. sumr 0 n (%m. f (m + k)) = sumr 0 (n + k) f - sumr 0 k f"; +by (induct_tac "n" 1); +by Auto_tac; +qed "sumr_offset2"; + +Goal "sumr 0 (n + k) f = sumr 0 n (%m. f (m + k)) + sumr 0 k f"; +by (simp_tac (simpset() addsimps [sumr_offset]) 1); +qed "sumr_offset3"; + +Goal "ALL n f. sumr 0 (n + k) f = sumr 0 n (%m. f (m + k)) + sumr 0 k f"; +by (simp_tac (simpset() addsimps [sumr_offset]) 1); +qed "sumr_offset4"; + +Goal "0 < n ==> \ +\ sumr (Suc 0) (Suc n) (%n. (if even(n) then 0 else \ +\ ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n) = \ +\ sumr 0 (Suc n) (%n. (if even(n) then 0 else \ +\ ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n)"; +by (res_inst_tac [("n1","1")] (sumr_split_add RS subst) 1); +by Auto_tac; +qed "sumr_from_1_from_0"; + +(*---------------------------------------------------------------------------*) +(* Maclaurin's theorem with Lagrange form of remainder *) +(*---------------------------------------------------------------------------*) + +(* Annoying: Proof is now even longer due mostly to + change in behaviour of simplifier since Isabelle99 *) +Goal " [| 0 < h; 0 < n; diff 0 = f; \ +\ ALL m t. \ +\ m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t |] \ +\ ==> EX t. 0 < t & \ +\ t < h & \ +\ f h = \ +\ sumr 0 n (%m. (diff m 0 / real (fact m)) * h ^ m) + \ +\ (diff n t / real (fact n)) * h ^ n"; +by (case_tac "n = 0" 1); +by (Force_tac 1); +by (dtac not0_implies_Suc 1); +by (etac exE 1); +by (subgoal_tac + "EX B. f h = sumr 0 n (%m. (diff m 0 / real (fact m)) * (h ^ m)) \ +\ + (B * ((h ^ n) / real (fact n)))" 1); + +by (simp_tac (HOL_ss addsimps [real_add_commute, real_divide_def, + ARITH_PROVE "(x = z + (y::real)) = (x - y = z)"]) 2); +by (res_inst_tac + [("x","(f(h) - sumr 0 n (%m. (diff(m)(0) / real (fact m)) * (h ^ m))) \ +\ * real (fact n) / (h ^ n)")] exI 2); +by (simp_tac (HOL_ss addsimps [real_mult_assoc,real_divide_def]) 2); + by (rtac (CLAIM "x = (1::real) ==> a = a * (x::real)") 2); +by (asm_simp_tac (HOL_ss addsimps + [CLAIM "(a::real) * (b * (c * d)) = (d * a) * (b * c)"] + delsimps [realpow_Suc]) 2); +by (stac left_inverse 2); +by (stac left_inverse 3); +by (rtac (real_not_refl2 RS not_sym) 2); +by (etac zero_less_power 2); +by (rtac real_of_nat_fact_not_zero 2); +by (Simp_tac 2); +by (etac exE 1); +by (cut_inst_tac [("b","%t. f t - \ +\ (sumr 0 n (%m. (diff m 0 / real (fact m)) * (t ^ m)) + \ +\ (B * ((t ^ n) / real (fact n))))")] + (CLAIM "EX g. g = b") 1); +by (etac exE 1); +by (subgoal_tac "g 0 = 0 & g h =0" 1); +by (asm_simp_tac (simpset() addsimps + [ARITH_PROVE "(x - y = z) = (x = z + (y::real))"] + delsimps [sumr_Suc]) 2); +by (cut_inst_tac [("n","m"),("k","1")] sumr_offset2 2); +by (asm_full_simp_tac (simpset() addsimps + [ARITH_PROVE "(x = y - z) = (y = x + (z::real))"] + delsimps [sumr_Suc]) 2); +by (cut_inst_tac [("b","%m t. diff m t - \ +\ (sumr 0 (n - m) (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) \ +\ + (B * ((t ^ (n - m)) / real (fact(n - m)))))")] + (CLAIM "EX difg. difg = b") 1); +by (etac exE 1); +by (subgoal_tac "difg 0 = g" 1); +by (asm_simp_tac (simpset() delsimps [realpow_Suc,fact_Suc]) 2); +by (subgoal_tac "ALL m t. m < n & 0 <= t & t <= h --> \ +\ DERIV (difg m) t :> difg (Suc m) t" 1); +by (Clarify_tac 2); +by (rtac DERIV_diff 2); +by (Asm_simp_tac 2); +by DERIV_tac; +by DERIV_tac; +by (rtac lemma_DERIV_subst 3); +by (rtac DERIV_quotient 3); +by (rtac DERIV_const 4); +by (rtac DERIV_pow 3); +by (asm_simp_tac (simpset() addsimps [inverse_mult_distrib, + CLAIM_SIMP "(a::real) * b * c * (d * e) = a * b * (c * d) * e" + mult_ac,fact_diff_Suc]) 4); +by (Asm_simp_tac 3); +by (forw_inst_tac [("m","ma")] less_add_one 2); +by (Clarify_tac 2); +by (asm_simp_tac (simpset() addsimps + [CLAIM "Suc m = ma + d + 1 ==> m - ma = d"] + delsimps [sumr_Suc]) 2); +by (asm_simp_tac (simpset() addsimps [(simplify (simpset() delsimps [sumr_Suc]) + (read_instantiate [("k","1")] sumr_offset4))] + delsimps [sumr_Suc,fact_Suc,realpow_Suc]) 2); +by (rtac lemma_DERIV_subst 2); +by (rtac DERIV_add 2); +by (rtac DERIV_const 3); +by (rtac DERIV_sumr 2); +by (Clarify_tac 2); +by (Simp_tac 3); +by (simp_tac (simpset() addsimps [real_divide_def,real_mult_assoc] + delsimps [fact_Suc,realpow_Suc]) 2); +by (rtac DERIV_cmult 2); +by (rtac lemma_DERIV_subst 2); +by DERIV_tac; +by (stac fact_Suc 2); +by (stac real_of_nat_mult 2); +by (simp_tac (simpset() addsimps [inverse_mult_distrib] @ + mult_ac) 2); +by (subgoal_tac "ALL ma. ma < n --> \ +\ (EX t. 0 < t & t < h & difg (Suc ma) t = 0)" 1); +by (rotate_tac 11 1); +by (dres_inst_tac [("x","m")] spec 1); +by (etac impE 1); +by (Asm_simp_tac 1); +by (etac exE 1); +by (res_inst_tac [("x","t")] exI 1); +by (asm_full_simp_tac (simpset() addsimps + [ARITH_PROVE "(x - y = 0) = (y = (x::real))"] + delsimps [realpow_Suc,fact_Suc]) 1); +by (subgoal_tac "ALL m. m < n --> difg m 0 = 0" 1); +by (Clarify_tac 2); +by (Asm_simp_tac 2); +by (forw_inst_tac [("m","ma")] less_add_one 2); +by (Clarify_tac 2); +by (asm_simp_tac (simpset() delsimps [sumr_Suc]) 2); +by (asm_simp_tac (simpset() addsimps [(simplify (simpset() delsimps [sumr_Suc]) + (read_instantiate [("k","1")] sumr_offset4))] + delsimps [sumr_Suc,fact_Suc,realpow_Suc]) 2); +by (subgoal_tac "ALL m. m < n --> (EX t. 0 < t & t < h & \ +\ DERIV (difg m) t :> 0)" 1); +by (rtac allI 1 THEN rtac impI 1); +by (rotate_tac 12 1); +by (dres_inst_tac [("x","ma")] spec 1); +by (etac impE 1 THEN assume_tac 1); +by (etac exE 1); +by (res_inst_tac [("x","t")] exI 1); +(* do some tidying up *) +by (ALLGOALS(thin_tac "difg = \ +\ (%m t. diff m t - \ +\ (sumr 0 (n - m) \ +\ (%p. diff (m + p) 0 / real (fact p) * t ^ p) + \ +\ B * (t ^ (n - m) / real (fact (n - m)))))")); +by (ALLGOALS(thin_tac "g = \ +\ (%t. f t - \ +\ (sumr 0 n (%m. diff m 0 / real (fact m) * t ^ m) + \ +\ B * (t ^ n / real (fact n))))")); +by (ALLGOALS(thin_tac "f h = \ +\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \ +\ B * (h ^ n / real (fact n))")); +(* back to business *) +by (Asm_simp_tac 1); +by (rtac DERIV_unique 1); +by (Blast_tac 2); +by (Force_tac 1); +by (rtac allI 1 THEN induct_tac "ma" 1); +by (rtac impI 1 THEN rtac Rolle 1); +by (assume_tac 1); +by (Asm_full_simp_tac 1); +by (Asm_full_simp_tac 1); +by (subgoal_tac "ALL t. 0 <= t & t <= h --> g differentiable t" 1); +by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1); +by (blast_tac (claset() addDs [DERIV_isCont]) 1); +by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1); +by (Clarify_tac 1); +by (res_inst_tac [("x","difg (Suc 0) t")] exI 1); +by (Force_tac 1); +by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1); +by (Clarify_tac 1); +by (res_inst_tac [("x","difg (Suc 0) x")] exI 1); +by (Force_tac 1); +by (Step_tac 1); +by (Force_tac 1); +by (subgoal_tac "EX ta. 0 < ta & ta < t & \ +\ DERIV difg (Suc n) ta :> 0" 1); +by (rtac Rolle 2 THEN assume_tac 2); +by (Asm_full_simp_tac 2); +by (rotate_tac 2 2); +by (dres_inst_tac [("x","n")] spec 2); +by (ftac (ARITH_PROVE "n < m ==> n < Suc m") 2); +by (rtac DERIV_unique 2); +by (assume_tac 3); +by (Force_tac 2); +by (subgoal_tac + "ALL ta. 0 <= ta & ta <= t --> (difg (Suc n)) differentiable ta" 2); +by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 2); +by (blast_tac (claset() addSDs [DERIV_isCont]) 2); +by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 2); +by (Clarify_tac 2); +by (res_inst_tac [("x","difg (Suc (Suc n)) ta")] exI 2); +by (Force_tac 2); +by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 2); +by (Clarify_tac 2); +by (res_inst_tac [("x","difg (Suc (Suc n)) x")] exI 2); +by (Force_tac 2); +by (Step_tac 1); +by (res_inst_tac [("x","ta")] exI 1); +by (Force_tac 1); +qed "Maclaurin"; + +Goal "0 < h & 0 < n & diff 0 = f & \ +\ (ALL m t. \ +\ m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t) \ +\ --> (EX t. 0 < t & \ +\ t < h & \ +\ f h = \ +\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \ +\ diff n t / real (fact n) * h ^ n)"; +by (blast_tac (claset() addIs [Maclaurin]) 1); +qed "Maclaurin_objl"; + +Goal " [| 0 < h; diff 0 = f; \ +\ ALL m t. \ +\ m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t |] \ +\ ==> EX t. 0 < t & \ +\ t <= h & \ +\ f h = \ +\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \ +\ diff n t / real (fact n) * h ^ n"; +by (case_tac "n" 1); +by Auto_tac; +by (dtac Maclaurin 1 THEN Auto_tac); +qed "Maclaurin2"; + +Goal "0 < h & diff 0 = f & \ +\ (ALL m t. \ +\ m < n & 0 <= t & t <= h --> DERIV (diff m) t :> diff (Suc m) t) \ +\ --> (EX t. 0 < t & \ +\ t <= h & \ +\ f h = \ +\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \ +\ diff n t / real (fact n) * h ^ n)"; +by (blast_tac (claset() addIs [Maclaurin2]) 1); +qed "Maclaurin2_objl"; + +Goal " [| h < 0; 0 < n; diff 0 = f; \ +\ ALL m t. \ +\ m < n & h <= t & t <= 0 --> DERIV (diff m) t :> diff (Suc m) t |] \ +\ ==> EX t. h < t & \ +\ t < 0 & \ +\ f h = \ +\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \ +\ diff n t / real (fact n) * h ^ n"; +by (cut_inst_tac [("f","%x. f (-x)"), + ("diff","%n x. ((- 1) ^ n) * diff n (-x)"), + ("h","-h"),("n","n")] Maclaurin_objl 1); +by (Asm_full_simp_tac 1); +by (etac impE 1 THEN Step_tac 1); +by (stac minus_mult_right 1); +by (rtac DERIV_cmult 1); +by (rtac lemma_DERIV_subst 1); +by (rtac (read_instantiate [("g","uminus")] DERIV_chain2) 1); +by (rtac DERIV_minus 2 THEN rtac DERIV_Id 2); +by (Force_tac 2); +by (Force_tac 1); +by (res_inst_tac [("x","-t")] exI 1); +by Auto_tac; +by (rtac (CLAIM "[| x = x'; y = y' |] ==> x + y = x' + (y'::real)") 1); +by (rtac sumr_fun_eq 1); +by (Asm_full_simp_tac 1); +by (auto_tac (claset(),simpset() addsimps [real_divide_def, + CLAIM "((a * b) * c) * d = (b * c) * (a * (d::real))", + power_mult_distrib RS sym])); +qed "Maclaurin_minus"; + +Goal "(h < 0 & 0 < n & diff 0 = f & \ +\ (ALL m t. \ +\ m < n & h <= t & t <= 0 --> DERIV (diff m) t :> diff (Suc m) t))\ +\ --> (EX t. h < t & \ +\ t < 0 & \ +\ f h = \ +\ sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + \ +\ diff n t / real (fact n) * h ^ n)"; +by (blast_tac (claset() addIs [Maclaurin_minus]) 1); +qed "Maclaurin_minus_objl"; + +(* ------------------------------------------------------------------------- *) +(* More convenient "bidirectional" version. *) +(* ------------------------------------------------------------------------- *) + +(* not good for PVS sin_approx, cos_approx *) +Goal " [| diff 0 = f; \ +\ ALL m t. \ +\ m < n & abs t <= abs x --> DERIV (diff m) t :> diff (Suc m) t |] \ +\ ==> EX t. abs t <= abs x & \ +\ f x = \ +\ sumr 0 n (%m. diff m 0 / real (fact m) * x ^ m) + \ +\ diff n t / real (fact n) * x ^ n"; +by (case_tac "n = 0" 1); +by (Force_tac 1); +by (case_tac "x = 0" 1); +by (res_inst_tac [("x","0")] exI 1); +by (Asm_full_simp_tac 1); +by (res_inst_tac [("P","0 < n")] impE 1); +by (assume_tac 2 THEN assume_tac 2); +by (induct_tac "n" 1); +by (Simp_tac 1); +by Auto_tac; +by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1); +by Auto_tac; +by (cut_inst_tac [("f","diff 0"), + ("diff","diff"), + ("h","x"),("n","n")] Maclaurin_objl 2); +by (Step_tac 2); +by (blast_tac (claset() addDs + [ARITH_PROVE "[|(0::real) <= t;t <= x |] ==> abs t <= abs x"]) 2); +by (res_inst_tac [("x","t")] exI 2); +by (force_tac (claset() addIs + [ARITH_PROVE "[| 0 < t; (t::real) < x|] ==> abs t <= abs x"],simpset()) 2); +by (cut_inst_tac [("f","diff 0"), + ("diff","diff"), + ("h","x"),("n","n")] Maclaurin_minus_objl 1); +by (Step_tac 1); +by (blast_tac (claset() addDs + [ARITH_PROVE "[|x <= t;t <= (0::real) |] ==> abs t <= abs x"]) 1); +by (res_inst_tac [("x","t")] exI 1); +by (force_tac (claset() addIs + [ARITH_PROVE "[| x < t; (t::real) < 0|] ==> abs t <= abs x"],simpset()) 1); +qed "Maclaurin_bi_le"; + +Goal "[| diff 0 = f; \ +\ ALL m x. DERIV (diff m) x :> diff(Suc m) x; \ +\ x ~= 0; 0 < n \ +\ |] ==> EX t. 0 < abs t & abs t < abs x & \ +\ f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \ +\ (diff n t / real (fact n)) * x ^ n"; +by (res_inst_tac [("x","x"),("y","0")] linorder_cases 1); +by (Blast_tac 2); +by (dtac Maclaurin_minus 1); +by (dtac Maclaurin 5); +by (TRYALL(assume_tac)); +by (Blast_tac 1); +by (Blast_tac 2); +by (Step_tac 1); +by (ALLGOALS(res_inst_tac [("x","t")] exI)); +by (Step_tac 1); +by (ALLGOALS(arith_tac)); +qed "Maclaurin_all_lt"; + +Goal "diff 0 = f & \ +\ (ALL m x. DERIV (diff m) x :> diff(Suc m) x) & \ +\ x ~= 0 & 0 < n \ +\ --> (EX t. 0 < abs t & abs t < abs x & \ +\ f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \ +\ (diff n t / real (fact n)) * x ^ n)"; +by (blast_tac (claset() addIs [Maclaurin_all_lt]) 1); +qed "Maclaurin_all_lt_objl"; + +Goal "x = (0::real) \ +\ ==> 0 < n --> \ +\ sumr 0 n (%m. (diff m (0::real) / real (fact m)) * x ^ m) = \ +\ diff 0 0"; +by (Asm_simp_tac 1); +by (induct_tac "n" 1); +by Auto_tac; +qed_spec_mp "Maclaurin_zero"; + +Goal "[| diff 0 = f; \ +\ ALL m x. DERIV (diff m) x :> diff (Suc m) x \ +\ |] ==> EX t. abs t <= abs x & \ +\ f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \ +\ (diff n t / real (fact n)) * x ^ n"; +by (cut_inst_tac [("n","n"),("m","0")] + (ARITH_PROVE "n <= m | m < (n::nat)") 1); +by (etac disjE 1); +by (Force_tac 1); +by (case_tac "x = 0" 1); +by (forw_inst_tac [("diff","diff"),("n","n")] Maclaurin_zero 1); +by (assume_tac 1); +by (dtac (gr_implies_not0 RS not0_implies_Suc) 1); +by (res_inst_tac [("x","0")] exI 1); +by (Force_tac 1); +by (forw_inst_tac [("diff","diff"),("n","n")] Maclaurin_all_lt 1); +by (TRYALL(assume_tac)); +by (Step_tac 1); +by (res_inst_tac [("x","t")] exI 1); +by Auto_tac; +qed "Maclaurin_all_le"; + +Goal "diff 0 = f & \ +\ (ALL m x. DERIV (diff m) x :> diff (Suc m) x) \ +\ --> (EX t. abs t <= abs x & \ +\ f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + \ +\ (diff n t / real (fact n)) * x ^ n)"; +by (blast_tac (claset() addIs [Maclaurin_all_le]) 1); +qed "Maclaurin_all_le_objl"; + +(* ------------------------------------------------------------------------- *) +(* Version for exp. *) +(* ------------------------------------------------------------------------- *) + +Goal "[| x ~= 0; 0 < n |] \ +\ ==> (EX t. 0 < abs t & \ +\ abs t < abs x & \ +\ exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) + \ +\ (exp t / real (fact n)) * x ^ n)"; +by (cut_inst_tac [("diff","%n. exp"),("f","exp"),("x","x"),("n","n")] + Maclaurin_all_lt_objl 1); +by Auto_tac; +qed "Maclaurin_exp_lt"; + +Goal "EX t. abs t <= abs x & \ +\ exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) + \ +\ (exp t / real (fact n)) * x ^ n"; +by (cut_inst_tac [("diff","%n. exp"),("f","exp"),("x","x"),("n","n")] + Maclaurin_all_le_objl 1); +by Auto_tac; +qed "Maclaurin_exp_le"; + +(* ------------------------------------------------------------------------- *) +(* Version for sin function *) +(* ------------------------------------------------------------------------- *) + +Goal "[| a < b; ALL x. a <= x & x <= b --> DERIV f x :> f'(x) |] \ +\ ==> EX z. a < z & z < b & (f b - f a = (b - a) * f'(z))"; +by (dtac MVT 1); +by (blast_tac (claset() addIs [DERIV_isCont]) 1); +by (force_tac (claset() addDs [order_less_imp_le], + simpset() addsimps [differentiable_def]) 1); +by (blast_tac (claset() addDs [DERIV_unique,order_less_imp_le]) 1); +qed "MVT2"; + +Goal "d < (4::nat) ==> d = 0 | d = 1 | d = 2 | d = 3"; +by (case_tac "d" 1 THEN Auto_tac); +qed "lemma_exhaust_less_4"; + +bind_thm ("real_mult_le_lemma", + simplify (simpset()) (inst "b" "1" mult_right_mono)); + + +Goal "0 < n --> Suc (Suc (2 * n - 2)) = 2*n"; +by (induct_tac "n" 1); +by Auto_tac; +qed_spec_mp "Suc_Suc_mult_two_diff_two"; +Addsimps [Suc_Suc_mult_two_diff_two]; + +Goal "0 < n --> Suc (Suc (4*n - 2)) = 4*n"; +by (induct_tac "n" 1); +by Auto_tac; +qed_spec_mp "lemma_Suc_Suc_4n_diff_2"; +Addsimps [lemma_Suc_Suc_4n_diff_2]; + +Goal "0 < n --> Suc (2 * n - 1) = 2*n"; +by (induct_tac "n" 1); +by Auto_tac; +qed_spec_mp "Suc_mult_two_diff_one"; +Addsimps [Suc_mult_two_diff_one]; + +Goal "EX t. sin x = \ +\ (sumr 0 n (%m. (if even m then 0 \ +\ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \ +\ x ^ m)) \ +\ + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"; +by (cut_inst_tac [("f","sin"),("n","n"),("x","x"), + ("diff","%n x. sin(x + 1/2*real (n)*pi)")] + Maclaurin_all_lt_objl 1); +by (Safe_tac); +by (Simp_tac 1); +by (Simp_tac 1); +by (case_tac "n" 1); +by (Clarify_tac 1); +by (Asm_full_simp_tac 1); +by (dres_inst_tac [("x","0")] spec 1 THEN Asm_full_simp_tac 1); +by (Asm_full_simp_tac 1); +by (rtac ccontr 1); +by (Asm_full_simp_tac 1); +by (dres_inst_tac [("x","x")] spec 1 THEN Asm_full_simp_tac 1); +by (dtac ssubst 1 THEN assume_tac 2); +by (res_inst_tac [("x","t")] exI 1); +by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1); +by (rtac sumr_fun_eq 1); +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex])); +by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc])); +(*Could sin_zero_iff help?*) +qed "Maclaurin_sin_expansion"; + +Goal "EX t. abs t <= abs x & \ +\ sin x = \ +\ (sumr 0 n (%m. (if even m then 0 \ +\ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \ +\ x ^ m)) \ +\ + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"; + +by (cut_inst_tac [("f","sin"),("n","n"),("x","x"), + ("diff","%n x. sin(x + 1/2*real (n)*pi)")] + Maclaurin_all_lt_objl 1); +by (Step_tac 1); +by (Simp_tac 1); +by (Simp_tac 1); +by (case_tac "n" 1); +by (Clarify_tac 1); +by (Asm_full_simp_tac 1); +by (Asm_full_simp_tac 1); +by (rtac ccontr 1); +by (Asm_full_simp_tac 1); +by (dres_inst_tac [("x","x")] spec 1 THEN Asm_full_simp_tac 1); +by (dtac ssubst 1 THEN assume_tac 2); +by (res_inst_tac [("x","t")] exI 1); +by (rtac conjI 1); +by (arith_tac 1); +by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1); +by (rtac sumr_fun_eq 1); +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex])); +by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc])); +qed "Maclaurin_sin_expansion2"; + +Goal "[| 0 < n; 0 < x |] ==> \ +\ EX t. 0 < t & t < x & \ +\ sin x = \ +\ (sumr 0 n (%m. (if even m then 0 \ +\ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \ +\ x ^ m)) \ +\ + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"; +by (cut_inst_tac [("f","sin"),("n","n"),("h","x"), + ("diff","%n x. sin(x + 1/2*real (n)*pi)")] + Maclaurin_objl 1); +by (Step_tac 1); +by (Asm_full_simp_tac 1); +by (Simp_tac 1); +by (dtac ssubst 1 THEN assume_tac 2); +by (res_inst_tac [("x","t")] exI 1); +by (rtac conjI 1 THEN rtac conjI 2); +by (assume_tac 1 THEN assume_tac 1); +by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1); +by (rtac sumr_fun_eq 1); +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex])); +by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc])); +qed "Maclaurin_sin_expansion3"; + +Goal "0 < x ==> \ +\ EX t. 0 < t & t <= x & \ +\ sin x = \ +\ (sumr 0 n (%m. (if even m then 0 \ +\ else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * \ +\ x ^ m)) \ +\ + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"; +by (cut_inst_tac [("f","sin"),("n","n"),("h","x"), + ("diff","%n x. sin(x + 1/2*real (n)*pi)")] + Maclaurin2_objl 1); +by (Step_tac 1); +by (Asm_full_simp_tac 1); +by (Simp_tac 1); +by (dtac ssubst 1 THEN assume_tac 2); +by (res_inst_tac [("x","t")] exI 1); +by (rtac conjI 1 THEN rtac conjI 2); +by (assume_tac 1 THEN assume_tac 1); +by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1); +by (rtac sumr_fun_eq 1); +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex])); +by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc])); +qed "Maclaurin_sin_expansion4"; + +(*-----------------------------------------------------------------------------*) +(* Maclaurin expansion for cos *) +(*-----------------------------------------------------------------------------*) + +Goal "sumr 0 (Suc n) \ +\ (%m. (if even m \ +\ then (- 1) ^ (m div 2)/(real (fact m)) \ +\ else 0) * \ +\ 0 ^ m) = 1"; +by (induct_tac "n" 1); +by Auto_tac; +qed "sumr_cos_zero_one"; +Addsimps [sumr_cos_zero_one]; + +Goal "EX t. abs t <= abs x & \ +\ cos x = \ +\ (sumr 0 n (%m. (if even m \ +\ then (- 1) ^ (m div 2)/(real (fact m)) \ +\ else 0) * \ +\ x ^ m)) \ +\ + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"; +by (cut_inst_tac [("f","cos"),("n","n"),("x","x"), + ("diff","%n x. cos(x + 1/2*real (n)*pi)")] + Maclaurin_all_lt_objl 1); +by (Step_tac 1); +by (Simp_tac 1); +by (Simp_tac 1); +by (case_tac "n" 1); +by (Asm_full_simp_tac 1); +by (asm_full_simp_tac (simpset() delsimps [sumr_Suc]) 1); +by (rtac ccontr 1); +by (Asm_full_simp_tac 1); +by (dres_inst_tac [("x","x")] spec 1 THEN Asm_full_simp_tac 1); +by (dtac ssubst 1 THEN assume_tac 2); +by (res_inst_tac [("x","t")] exI 1); +by (rtac conjI 1); +by (arith_tac 1); +by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1); +by (rtac sumr_fun_eq 1); +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex])); +by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add] delsimps + [fact_Suc,realpow_Suc])); +by (auto_tac (claset(),simpset() addsimps [real_mult_commute])); +qed "Maclaurin_cos_expansion"; + +Goal "[| 0 < x; 0 < n |] ==> \ +\ EX t. 0 < t & t < x & \ +\ cos x = \ +\ (sumr 0 n (%m. (if even m \ +\ then (- 1) ^ (m div 2)/(real (fact m)) \ +\ else 0) * \ +\ x ^ m)) \ +\ + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"; +by (cut_inst_tac [("f","cos"),("n","n"),("h","x"), + ("diff","%n x. cos(x + 1/2*real (n)*pi)")] + Maclaurin_objl 1); +by (Step_tac 1); +by (Asm_full_simp_tac 1); +by (Simp_tac 1); +by (dtac ssubst 1 THEN assume_tac 2); +by (res_inst_tac [("x","t")] exI 1); +by (rtac conjI 1 THEN rtac conjI 2); +by (assume_tac 1 THEN assume_tac 1); +by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1); +by (rtac sumr_fun_eq 1); +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex])); +by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add] delsimps [fact_Suc,realpow_Suc])); +by (auto_tac (claset(),simpset() addsimps [real_mult_commute])); +qed "Maclaurin_cos_expansion2"; + +Goal "[| x < 0; 0 < n |] ==> \ +\ EX t. x < t & t < 0 & \ +\ cos x = \ +\ (sumr 0 n (%m. (if even m \ +\ then (- 1) ^ (m div 2)/(real (fact m)) \ +\ else 0) * \ +\ x ^ m)) \ +\ + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"; +by (cut_inst_tac [("f","cos"),("n","n"),("h","x"), + ("diff","%n x. cos(x + 1/2*real (n)*pi)")] + Maclaurin_minus_objl 1); +by (Step_tac 1); +by (Asm_full_simp_tac 1); +by (Simp_tac 1); +by (dtac ssubst 1 THEN assume_tac 2); +by (res_inst_tac [("x","t")] exI 1); +by (rtac conjI 1 THEN rtac conjI 2); +by (assume_tac 1 THEN assume_tac 1); +by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1); +by (rtac sumr_fun_eq 1); +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex])); +by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add] delsimps [fact_Suc,realpow_Suc])); +by (auto_tac (claset(),simpset() addsimps [real_mult_commute])); +qed "Maclaurin_minus_cos_expansion"; + +(* ------------------------------------------------------------------------- *) +(* Version for ln(1 +/- x). Where is it?? *) +(* ------------------------------------------------------------------------- *) + diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/IMP/Compiler.thy --- a/src/HOL/IMP/Compiler.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/IMP/Compiler.thy Tue May 11 20:11:08 2004 +0200 @@ -86,7 +86,7 @@ lemma [simp]: "\m n. closed m n (C1@C2) = (closed m (n+size C2) C1 \ closed (m+size C1) n C2)" -by(induct C1, simp, simp add:plus_ac0) +by(induct C1, simp, simp add:add_ac) theorem [simp]: "\m n. closed m n (compile c)" by(induct c, simp_all add:backws_def forws_def) diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Integ/Bin.thy --- a/src/HOL/Integ/Bin.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Integ/Bin.thy Tue May 11 20:11:08 2004 +0200 @@ -10,7 +10,7 @@ theory Bin = IntDef + Numeral: -axclass number_ring \ number, ring +axclass number_ring \ number, comm_ring_1 number_of_Pls: "number_of bin.Pls = 0" number_of_Min: "number_of bin.Min = - 1" number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) + @@ -118,7 +118,7 @@ subsection{*Comparisons, for Ordered Rings*} -lemma double_eq_0_iff: "(a + a = 0) = (a = (0::'a::ordered_ring))" +lemma double_eq_0_iff: "(a + a = 0) = (a = (0::'a::ordered_idom))" proof - have "a + a = (1+1)*a" by (simp add: left_distrib) with zero_less_two [where 'a = 'a] @@ -157,7 +157,7 @@ text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*} -lemma Ints_odd_nonzero: "a \ Ints ==> 1 + a + a \ (0::'a::ordered_ring)" +lemma Ints_odd_nonzero: "a \ Ints ==> 1 + a + a \ (0::'a::ordered_idom)" proof (unfold Ints_def) assume "a \ range of_int" then obtain z where a: "a = of_int z" .. @@ -175,17 +175,17 @@ lemma iszero_number_of_BIT: "iszero (number_of (w BIT x)::'a) = - (~x & iszero (number_of w::'a::{ordered_ring,number_ring}))" + (~x & iszero (number_of w::'a::{ordered_idom,number_ring}))" by (simp add: iszero_def compare_rls zero_reorient double_eq_0_iff number_of Ints_odd_nonzero [OF Ints_number_of]) lemma iszero_number_of_0: - "iszero (number_of (w BIT False) :: 'a::{ordered_ring,number_ring}) = + "iszero (number_of (w BIT False) :: 'a::{ordered_idom,number_ring}) = iszero (number_of w :: 'a)" by (simp only: iszero_number_of_BIT simp_thms) lemma iszero_number_of_1: - "~ iszero (number_of (w BIT True)::'a::{ordered_ring,number_ring})" + "~ iszero (number_of (w BIT True)::'a::{ordered_idom,number_ring})" by (simp only: iszero_number_of_BIT simp_thms) @@ -193,7 +193,7 @@ subsection{*The Less-Than Relation*} lemma less_number_of_eq_neg: - "((number_of x::'a::{ordered_ring,number_ring}) < number_of y) + "((number_of x::'a::{ordered_idom,number_ring}) < number_of y) = neg (number_of (bin_add x (bin_minus y)) :: 'a)" apply (subst less_iff_diff_less_0) apply (simp add: neg_def diff_minus number_of_add number_of_minus) @@ -202,14 +202,14 @@ text{*If @{term Numeral0} is rewritten to 0 then this rule can't be applied: @{term Numeral0} IS @{term "number_of Pls"} *} lemma not_neg_number_of_Pls: - "~ neg (number_of bin.Pls ::'a::{ordered_ring,number_ring})" + "~ neg (number_of bin.Pls ::'a::{ordered_idom,number_ring})" by (simp add: neg_def numeral_0_eq_0) lemma neg_number_of_Min: - "neg (number_of bin.Min ::'a::{ordered_ring,number_ring})" + "neg (number_of bin.Min ::'a::{ordered_idom,number_ring})" by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1) -lemma double_less_0_iff: "(a + a < 0) = (a < (0::'a::ordered_ring))" +lemma double_less_0_iff: "(a + a < 0) = (a < (0::'a::ordered_idom))" proof - have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib) also have "... = (a < 0)" @@ -231,7 +231,7 @@ text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*} lemma Ints_odd_less_0: - "a \ Ints ==> (1 + a + a < 0) = (a < (0::'a::ordered_ring))"; + "a \ Ints ==> (1 + a + a < 0) = (a < (0::'a::ordered_idom))"; proof (unfold Ints_def) assume "a \ range of_int" then obtain z where a: "a = of_int z" .. @@ -244,7 +244,7 @@ lemma neg_number_of_BIT: "neg (number_of (w BIT x)::'a) = - neg (number_of w :: 'a::{ordered_ring,number_ring})" + neg (number_of w :: 'a::{ordered_idom,number_ring})" by (simp add: number_of neg_def double_less_0_iff Ints_odd_less_0 [OF Ints_number_of]) @@ -257,7 +257,7 @@ standard] lemma le_number_of_eq: - "((number_of x::'a::{ordered_ring,number_ring}) \ number_of y) + "((number_of x::'a::{ordered_idom,number_ring}) \ number_of y) = (~ (neg (number_of (bin_add y (bin_minus x)) :: 'a)))" by (simp add: le_number_of_eq_not_less less_number_of_eq_neg) @@ -265,7 +265,7 @@ text{*Absolute value (@{term abs})*} lemma abs_number_of: - "abs(number_of x::'a::{ordered_ring,number_ring}) = + "abs(number_of x::'a::{ordered_idom,number_ring}) = (if number_of x < (0::'a) then -number_of x else number_of x)" by (simp add: abs_if) diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Integ/IntArith.thy --- a/src/HOL/Integ/IntArith.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Integ/IntArith.thy Tue May 11 20:11:08 2004 +0200 @@ -126,11 +126,11 @@ finally show ?thesis . qed -lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{ordered_ring,number_ring})" +lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{ordered_idom,number_ring})" by (simp add: abs_if) lemma abs_power_minus_one [simp]: - "abs(-1 ^ n) = (1::'a::{ordered_ring,number_ring,ringpower})" + "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,ringpower})" by (simp add: power_abs) lemma of_int_number_of_eq: diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Integ/IntDef.thy --- a/src/HOL/Integ/IntDef.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Integ/IntDef.thy Tue May 11 20:11:08 2004 +0200 @@ -153,7 +153,7 @@ lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute -lemmas zmult_ac = Ring_and_Field.mult_ac +lemmas zmult_ac = OrderedGroup.mult_ac lemma zadd_int: "(int m) + (int n) = int (m + n)" by (simp add: int_def add) @@ -164,7 +164,7 @@ lemma int_Suc: "int (Suc m) = 1 + (int m)" by (simp add: One_int_def zadd_int) -(*also for the instance declaration int :: plus_ac0*) +(*also for the instance declaration int :: comm_monoid_add*) lemma zadd_0: "(0::int) + z = z" apply (simp add: Zero_int_def int_def) apply (cases z, simp add: add) @@ -235,8 +235,8 @@ by (rule trans [OF zmult_commute zmult_1]) -text{*The Integers Form A Ring*} -instance int :: ring +text{*The Integers Form A comm_ring_1*} +instance int :: comm_ring_1 proof fix i j k :: int show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc) @@ -368,8 +368,8 @@ zabs_def: "abs(i::int) == if i < 0 then -i else i" -text{*The Integers Form an Ordered Ring*} -instance int :: ordered_ring +text{*The Integers Form an Ordered comm_ring_1*} +instance int :: ordered_idom proof fix i j k :: int show "i \ j ==> k + i \ k + j" by (rule zadd_left_mono) @@ -510,7 +510,7 @@ in theory @{text Ring_and_Field}. But is it really better than just rewriting with @{text abs_if}?*} lemma abs_split [arith_split]: - "P(abs(a::'a::ordered_ring)) = ((0 \ a --> P a) & (a < 0 --> P(-a)))" + "P(abs(a::'a::ordered_idom)) = ((0 \ a --> P a) & (a < 0 --> P(-a)))" by (force dest: order_less_le_trans simp add: abs_if linorder_not_less) @@ -519,11 +519,11 @@ constdefs - neg :: "'a::ordered_ring => bool" + neg :: "'a::ordered_idom => bool" "neg(Z) == Z < 0" (*For simplifying equalities*) - iszero :: "'a::semiring => bool" + iszero :: "'a::comm_semiring_1_cancel => bool" "iszero z == z = (0)" @@ -560,9 +560,9 @@ by (simp add: linorder_not_less neg_def) -subsection{*Embedding of the Naturals into any Semiring: @{term of_nat}*} +subsection{*Embedding of the Naturals into any comm_semiring_1_cancel: @{term of_nat}*} -consts of_nat :: "nat => 'a::semiring" +consts of_nat :: "nat => 'a::comm_semiring_1_cancel" primrec of_nat_0: "of_nat 0 = 0" @@ -581,27 +581,27 @@ apply (simp_all add: mult_ac add_ac right_distrib) done -lemma zero_le_imp_of_nat: "0 \ (of_nat m::'a::ordered_semiring)" +lemma zero_le_imp_of_nat: "0 \ (of_nat m::'a::ordered_semidom)" apply (induct m, simp_all) apply (erule order_trans) apply (rule less_add_one [THEN order_less_imp_le]) done lemma less_imp_of_nat_less: - "m < n ==> of_nat m < (of_nat n::'a::ordered_semiring)" + "m < n ==> of_nat m < (of_nat n::'a::ordered_semidom)" apply (induct m n rule: diff_induct, simp_all) apply (insert add_le_less_mono [OF zero_le_imp_of_nat zero_less_one], force) done lemma of_nat_less_imp_less: - "of_nat m < (of_nat n::'a::ordered_semiring) ==> m < n" + "of_nat m < (of_nat n::'a::ordered_semidom) ==> m < n" apply (induct m n rule: diff_induct, simp_all) apply (insert zero_le_imp_of_nat) apply (force simp add: linorder_not_less [symmetric]) done lemma of_nat_less_iff [simp]: - "(of_nat m < (of_nat n::'a::ordered_semiring)) = (m (of_nat n::'a::ordered_semiring)) = (m \ n)" + "(of_nat m \ (of_nat n::'a::ordered_semidom)) = (m \ n)" by (simp add: linorder_not_less [symmetric]) text{*Special cases where either operand is zero*} declare of_nat_le_iff [of 0, simplified, simp] declare of_nat_le_iff [of _ 0, simplified, simp] -text{*The ordering on the semiring is necessary to exclude the possibility of +text{*The ordering on the comm_semiring_1_cancel is necessary to exclude the possibility of a finite field, which indeed wraps back to zero.*} lemma of_nat_eq_iff [simp]: - "(of_nat m = (of_nat n::'a::ordered_semiring)) = (m = n)" + "(of_nat m = (of_nat n::'a::ordered_semidom)) = (m = n)" by (simp add: order_eq_iff) text{*Special cases where either operand is zero*} @@ -627,7 +627,7 @@ declare of_nat_eq_iff [of _ 0, simplified, simp] lemma of_nat_diff [simp]: - "n \ m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring)" + "n \ m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::comm_ring_1)" by (simp del: of_nat_add add: compare_rls of_nat_add [symmetric] split add: nat_diff_split) @@ -635,7 +635,7 @@ subsection{*The Set of Natural Numbers*} constdefs - Nats :: "'a::semiring set" + Nats :: "'a::comm_semiring_1_cancel set" "Nats == range of_nat" syntax (xsymbols) Nats :: "'a set" ("\") @@ -681,10 +681,10 @@ qed -subsection{*Embedding of the Integers into any Ring: @{term of_int}*} +subsection{*Embedding of the Integers into any comm_ring_1: @{term of_int}*} constdefs - of_int :: "int => 'a::ring" + of_int :: "int => 'a::comm_ring_1" "of_int z == contents (\(i,j) \ Rep_Integ z. { of_nat i - of_nat j })" @@ -719,7 +719,7 @@ done lemma of_int_le_iff [simp]: - "(of_int w \ (of_int z::'a::ordered_ring)) = (w \ z)" + "(of_int w \ (of_int z::'a::ordered_idom)) = (w \ z)" apply (cases w) apply (cases z) apply (simp add: compare_rls of_int le diff_int_def add minus @@ -731,16 +731,16 @@ declare of_int_le_iff [of _ 0, simplified, simp] lemma of_int_less_iff [simp]: - "(of_int w < (of_int z::'a::ordered_ring)) = (w < z)" + "(of_int w < (of_int z::'a::ordered_idom)) = (w < z)" by (simp add: linorder_not_le [symmetric]) text{*Special cases where either operand is zero*} declare of_int_less_iff [of 0, simplified, simp] declare of_int_less_iff [of _ 0, simplified, simp] -text{*The ordering on the ring is necessary. See @{text of_nat_eq_iff} above.*} +text{*The ordering on the comm_ring_1 is necessary. See @{text of_nat_eq_iff} above.*} lemma of_int_eq_iff [simp]: - "(of_int w = (of_int z::'a::ordered_ring)) = (w = z)" + "(of_int w = (of_int z::'a::ordered_idom)) = (w = z)" by (simp add: order_eq_iff) text{*Special cases where either operand is zero*} @@ -759,7 +759,7 @@ subsection{*The Set of Integers*} constdefs - Ints :: "'a::ring set" + Ints :: "'a::comm_ring_1 set" "Ints == range of_int" diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Integ/NatBin.thy --- a/src/HOL/Integ/NatBin.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Integ/NatBin.thy Tue May 11 20:11:08 2004 +0200 @@ -256,42 +256,42 @@ We cannot prove general results about the numeral @{term "-1"}, so we have to use @{term "- 1"} instead.*} -lemma power2_eq_square: "(a::'a::{semiring,ringpower})\ = a * a" +lemma power2_eq_square: "(a::'a::{comm_semiring_1_cancel,ringpower})\ = a * a" by (simp add: numeral_2_eq_2 Power.power_Suc) -lemma [simp]: "(0::'a::{semiring,ringpower})\ = 0" +lemma [simp]: "(0::'a::{comm_semiring_1_cancel,ringpower})\ = 0" by (simp add: power2_eq_square) -lemma [simp]: "(1::'a::{semiring,ringpower})\ = 1" +lemma [simp]: "(1::'a::{comm_semiring_1_cancel,ringpower})\ = 1" by (simp add: power2_eq_square) text{*Squares of literal numerals will be evaluated.*} declare power2_eq_square [of "number_of w", standard, simp] -lemma zero_le_power2 [simp]: "0 \ (a\::'a::{ordered_ring,ringpower})" +lemma zero_le_power2 [simp]: "0 \ (a\::'a::{ordered_idom,ringpower})" by (simp add: power2_eq_square zero_le_square) lemma zero_less_power2 [simp]: - "(0 < a\) = (a \ (0::'a::{ordered_ring,ringpower}))" + "(0 < a\) = (a \ (0::'a::{ordered_idom,ringpower}))" by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff) lemma zero_eq_power2 [simp]: - "(a\ = 0) = (a = (0::'a::{ordered_ring,ringpower}))" + "(a\ = 0) = (a = (0::'a::{ordered_idom,ringpower}))" by (force simp add: power2_eq_square mult_eq_0_iff) lemma abs_power2 [simp]: - "abs(a\) = (a\::'a::{ordered_ring,ringpower})" + "abs(a\) = (a\::'a::{ordered_idom,ringpower})" by (simp add: power2_eq_square abs_mult abs_mult_self) lemma power2_abs [simp]: - "(abs a)\ = (a\::'a::{ordered_ring,ringpower})" + "(abs a)\ = (a\::'a::{ordered_idom,ringpower})" by (simp add: power2_eq_square abs_mult_self) lemma power2_minus [simp]: - "(- a)\ = (a\::'a::{ring,ringpower})" + "(- a)\ = (a\::'a::{comm_ring_1,ringpower})" by (simp add: power2_eq_square) -lemma power_minus1_even: "(- 1) ^ (2*n) = (1::'a::{ring,ringpower})" +lemma power_minus1_even: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,ringpower})" apply (induct_tac "n") apply (auto simp add: power_Suc power_add) done @@ -303,11 +303,11 @@ by (simp add: power_even_eq) lemma power_minus_even [simp]: - "(-a) ^ (2*n) = (a::'a::{ring,ringpower}) ^ (2*n)" + "(-a) ^ (2*n) = (a::'a::{comm_ring_1,ringpower}) ^ (2*n)" by (simp add: power_minus1_even power_minus [of a]) lemma zero_le_even_power: - "0 \ (a::'a::{ordered_ring,ringpower}) ^ (2*n)" + "0 \ (a::'a::{ordered_idom,ringpower}) ^ (2*n)" proof (induct "n") case 0 show ?case by (simp add: zero_le_one) @@ -320,7 +320,7 @@ qed lemma odd_power_less_zero: - "(a::'a::{ordered_ring,ringpower}) < 0 ==> a ^ Suc(2*n) < 0" + "(a::'a::{ordered_idom,ringpower}) < 0 ==> a ^ Suc(2*n) < 0" proof (induct "n") case 0 show ?case by (simp add: Power.power_Suc) @@ -333,7 +333,7 @@ qed lemma odd_0_le_power_imp_0_le: - "0 \ a ^ Suc(2*n) ==> 0 \ (a::'a::{ordered_ring,ringpower})" + "0 \ a ^ Suc(2*n) ==> 0 \ (a::'a::{ordered_idom,ringpower})" apply (insert odd_power_less_zero [of a n]) apply (force simp add: linorder_not_less [symmetric]) done @@ -473,7 +473,7 @@ "((number_of (v BIT x) ::int) = number_of (w BIT y)) = (x=y & (((number_of v) ::int) = number_of w))" by (simp only: simp_thms number_of_BIT lemma1 lemma2 eq_commute - Ring_and_Field.add_left_cancel add_assoc Ring_and_Field.add_0 + OrderedGroup.add_left_cancel add_assoc OrderedGroup.add_0 split add: split_if cong: imp_cong) diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Integ/Parity.thy --- a/src/HOL/Integ/Parity.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Integ/Parity.thy Tue May 11 20:11:08 2004 +0200 @@ -249,7 +249,7 @@ by (rule neg_one_even_odd_power [THEN conjunct2, THEN mp], assumption) lemma neg_power_if: - "(-x::'a::{ring,ringpower}) ^ n = + "(-x::'a::{comm_ring_1,ringpower}) ^ n = (if even n then (x ^ n) else -(x ^ n))" by (induct n, simp_all split: split_if_asm add: power_Suc) @@ -257,13 +257,13 @@ subsection {* An Equivalence for @{term "0 \ a^n"} *} lemma even_power_le_0_imp_0: - "a ^ (2*k) \ (0::'a::{ordered_ring,ringpower}) ==> a=0" + "a ^ (2*k) \ (0::'a::{ordered_idom,ringpower}) ==> a=0" apply (induct k) apply (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc) done lemma zero_le_power_iff: - "(0 \ a^n) = (0 \ (a::'a::{ordered_ring,ringpower}) | even n)" + "(0 \ a^n) = (0 \ (a::'a::{ordered_idom,ringpower}) | even n)" (is "?P n") proof cases assume even: "even n" diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Integ/Presburger.thy --- a/src/HOL/Integ/Presburger.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Integ/Presburger.thy Tue May 11 20:11:08 2004 +0200 @@ -704,7 +704,7 @@ have "P x \ P (x - i * d)" using step.hyps by blast also have "\ \ P(x - (i + 1) * d)" using minus[THEN spec, of "x - i * d"] - by (simp add:int_distrib Ring_and_Field.diff_diff_eq[symmetric]) + by (simp add:int_distrib OrderedGroup.diff_diff_eq[symmetric]) ultimately show "P x \ P(x - (i + 1) * d)" by blast qed qed diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Integ/int_arith1.ML --- a/src/HOL/Integ/int_arith1.ML Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Integ/int_arith1.ML Tue May 11 20:11:08 2004 +0200 @@ -383,20 +383,20 @@ "(l::'a::number_ring) = m * n"], EqCancelNumerals.proc), ("intless_cancel_numerals", - ["(l::'a::{ordered_ring,number_ring}) + m < n", - "(l::'a::{ordered_ring,number_ring}) < m + n", - "(l::'a::{ordered_ring,number_ring}) - m < n", - "(l::'a::{ordered_ring,number_ring}) < m - n", - "(l::'a::{ordered_ring,number_ring}) * m < n", - "(l::'a::{ordered_ring,number_ring}) < m * n"], + ["(l::'a::{ordered_idom,number_ring}) + m < n", + "(l::'a::{ordered_idom,number_ring}) < m + n", + "(l::'a::{ordered_idom,number_ring}) - m < n", + "(l::'a::{ordered_idom,number_ring}) < m - n", + "(l::'a::{ordered_idom,number_ring}) * m < n", + "(l::'a::{ordered_idom,number_ring}) < m * n"], LessCancelNumerals.proc), ("intle_cancel_numerals", - ["(l::'a::{ordered_ring,number_ring}) + m <= n", - "(l::'a::{ordered_ring,number_ring}) <= m + n", - "(l::'a::{ordered_ring,number_ring}) - m <= n", - "(l::'a::{ordered_ring,number_ring}) <= m - n", - "(l::'a::{ordered_ring,number_ring}) * m <= n", - "(l::'a::{ordered_ring,number_ring}) <= m * n"], + ["(l::'a::{ordered_idom,number_ring}) + m <= n", + "(l::'a::{ordered_idom,number_ring}) <= m + n", + "(l::'a::{ordered_idom,number_ring}) - m <= n", + "(l::'a::{ordered_idom,number_ring}) <= m - n", + "(l::'a::{ordered_idom,number_ring}) * m <= n", + "(l::'a::{ordered_idom,number_ring}) <= m * n"], LeCancelNumerals.proc)]; @@ -488,7 +488,7 @@ val assoc_fold_simproc = Bin_Simprocs.prep_simproc - ("semiring_assoc_fold", ["(a::'a::semiring) * b"], + ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"], Semiring_Times_Assoc.proc); Addsimprocs [assoc_fold_simproc]; @@ -545,9 +545,9 @@ val fast_int_arith_simproc = Simplifier.simproc (Theory.sign_of (the_context())) "fast_int_arith" - ["(m::'a::{ordered_ring,number_ring}) < n", - "(m::'a::{ordered_ring,number_ring}) <= n", - "(m::'a::{ordered_ring,number_ring}) = n"] Fast_Arith.lin_arith_prover; + ["(m::'a::{ordered_idom,number_ring}) < n", + "(m::'a::{ordered_idom,number_ring}) <= n", + "(m::'a::{ordered_idom,number_ring}) = n"] Fast_Arith.lin_arith_prover; Addsimprocs [fast_int_arith_simproc] diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Integ/int_factor_simprocs.ML --- a/src/HOL/Integ/int_factor_simprocs.ML Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Integ/int_factor_simprocs.ML Tue May 11 20:11:08 2004 +0200 @@ -116,16 +116,16 @@ val ring_cancel_numeral_factors = map Bin_Simprocs.prep_simproc [("ring_eq_cancel_numeral_factor", - ["(l::'a::{ordered_ring,number_ring}) * m = n", - "(l::'a::{ordered_ring,number_ring}) = m * n"], + ["(l::'a::{ordered_idom,number_ring}) * m = n", + "(l::'a::{ordered_idom,number_ring}) = m * n"], EqCancelNumeralFactor.proc), ("ring_less_cancel_numeral_factor", - ["(l::'a::{ordered_ring,number_ring}) * m < n", - "(l::'a::{ordered_ring,number_ring}) < m * n"], + ["(l::'a::{ordered_idom,number_ring}) * m < n", + "(l::'a::{ordered_idom,number_ring}) < m * n"], LessCancelNumeralFactor.proc), ("ring_le_cancel_numeral_factor", - ["(l::'a::{ordered_ring,number_ring}) * m <= n", - "(l::'a::{ordered_ring,number_ring}) <= m * n"], + ["(l::'a::{ordered_idom,number_ring}) * m <= n", + "(l::'a::{ordered_idom,number_ring}) <= m * n"], LeCancelNumeralFactor.proc), ("int_div_cancel_numeral_factors", ["((l::int) * m) div n", "(l::int) div (m * n)"], @@ -249,7 +249,7 @@ val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac)) end; -(*mult_cancel_left requires an ordered ring, such as int. The version in +(*mult_cancel_left requires an ordered comm_ring_1, such as int. The version in rat_arith.ML works for all fields.*) structure EqCancelFactor = ExtractCommonTermFun (open CancelFactorCommon diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/IsaMakefile Tue May 11 20:11:08 2004 +0200 @@ -151,7 +151,7 @@ Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy\ Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\ Hyperreal/Lim.thy Hyperreal/Log.thy\ - Hyperreal/MacLaurin.ML Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy\ + Hyperreal/MacLaurin_lemmas.ML Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy\ Hyperreal/NSA.thy Hyperreal/NthRoot.thy Hyperreal/Poly.thy\ Hyperreal/SEQ.ML Hyperreal/SEQ.thy Hyperreal/Series.thy\ Hyperreal/Star.thy Hyperreal/Transcendental.ML\ diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/LOrder.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/LOrder.thy Tue May 11 20:11:08 2004 +0200 @@ -0,0 +1,331 @@ +(* Title: HOL/LOrder.thy + ID: $Id$ + Author: Steven Obua, TU Muenchen + License: GPL (GNU GENERAL PUBLIC LICENSE) +*) + +header {* Lattice Orders *} + +theory LOrder = HOL: + +text {* + The theory of lattices developed here is taken from the book: + \begin{itemize} + \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979. + \end{itemize} +*} + +constdefs + is_meet :: "(('a::order) \ 'a \ 'a) \ bool" + "is_meet m == ! a b x. m a b \ a \ m a b \ b \ (x \ a \ x \ b \ x \ m a b)" + is_join :: "(('a::order) \ 'a \ 'a) \ bool" + "is_join j == ! a b x. a \ j a b \ b \ j a b \ (a \ x \ b \ x \ j a b \ x)" + +lemma is_meet_unique: + assumes "is_meet u" "is_meet v" shows "u = v" +proof - + { + fix a b :: "'a \ 'a \ 'a" + assume a: "is_meet a" + assume b: "is_meet b" + { + fix x y + let ?za = "a x y" + let ?zb = "b x y" + from a have za_le: "?za <= x & ?za <= y" by (auto simp add: is_meet_def) + with b have "?za <= ?zb" by (auto simp add: is_meet_def) + } + } + note f_le = this + show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le) +qed + +lemma is_join_unique: + assumes "is_join u" "is_join v" shows "u = v" +proof - + { + fix a b :: "'a \ 'a \ 'a" + assume a: "is_join a" + assume b: "is_join b" + { + fix x y + let ?za = "a x y" + let ?zb = "b x y" + from a have za_le: "x <= ?za & y <= ?za" by (auto simp add: is_join_def) + with b have "?zb <= ?za" by (auto simp add: is_join_def) + } + } + note f_le = this + show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le) +qed + +axclass join_semilorder < order + join_exists: "? j. is_join j" + +axclass meet_semilorder < order + meet_exists: "? m. is_meet m" + +axclass lorder < join_semilorder, meet_semilorder + +constdefs + meet :: "('a::meet_semilorder) \ 'a \ 'a" + "meet == THE m. is_meet m" + join :: "('a::join_semilorder) \ 'a \ 'a" + "join == THE j. is_join j" + +lemma is_meet_meet: "is_meet (meet::'a \ 'a \ ('a::meet_semilorder))" +proof - + from meet_exists obtain k::"'a \ 'a \ 'a" where "is_meet k" .. + with is_meet_unique[of _ k] show ?thesis + by (simp add: meet_def theI[of is_meet]) +qed + +lemma meet_unique: "(is_meet m) = (m = meet)" +by (insert is_meet_meet, auto simp add: is_meet_unique) + +lemma is_join_join: "is_join (join::'a \ 'a \ ('a::join_semilorder))" +proof - + from join_exists obtain k::"'a \ 'a \ 'a" where "is_join k" .. + with is_join_unique[of _ k] show ?thesis + by (simp add: join_def theI[of is_join]) +qed + +lemma join_unique: "(is_join j) = (j = join)" +by (insert is_join_join, auto simp add: is_join_unique) + +lemma meet_left_le: "meet a b \ (a::'a::meet_semilorder)" +by (insert is_meet_meet, auto simp add: is_meet_def) + +lemma meet_right_le: "meet a b \ (b::'a::meet_semilorder)" +by (insert is_meet_meet, auto simp add: is_meet_def) + +lemma meet_imp_le: "x \ a \ x \ b \ x \ meet a (b::'a::meet_semilorder)" +by (insert is_meet_meet, auto simp add: is_meet_def) + +lemma join_left_le: "a \ join a (b::'a::join_semilorder)" +by (insert is_join_join, auto simp add: is_join_def) + +lemma join_right_le: "b \ join a (b::'a::join_semilorder)" +by (insert is_join_join, auto simp add: is_join_def) + +lemma join_imp_le: "a \ x \ b \ x \ join a b \ (x::'a::join_semilorder)" +by (insert is_join_join, auto simp add: is_join_def) + +lemmas meet_join_le = meet_left_le meet_right_le join_left_le join_right_le + +lemma is_meet_min: "is_meet (min::'a \ 'a \ ('a::linorder))" +by (auto simp add: is_meet_def min_def) + +lemma is_join_max: "is_join (max::'a \ 'a \ ('a::linorder))" +by (auto simp add: is_join_def max_def) + +instance linorder \ meet_semilorder +proof + from is_meet_min show "? (m::'a\'a\('a::linorder)). is_meet m" by auto +qed + +instance linorder \ join_semilorder +proof + from is_join_max show "? (j::'a\'a\('a::linorder)). is_join j" by auto +qed + +instance linorder \ lorder .. + +lemma meet_min: "meet = (min :: 'a\'a\('a::linorder))" +by (simp add: is_meet_meet is_meet_min is_meet_unique) + +lemma join_max: "join = (max :: 'a\'a\('a::linorder))" +by (simp add: is_join_join is_join_max is_join_unique) + +lemma meet_idempotent[simp]: "meet x x = x" +by (rule order_antisym, simp_all add: meet_left_le meet_imp_le) + +lemma join_idempotent[simp]: "join x x = x" +by (rule order_antisym, simp_all add: join_left_le join_imp_le) + +lemma meet_comm: "meet x y = meet y x" +by (rule order_antisym, (simp add: meet_left_le meet_right_le meet_imp_le)+) + +lemma join_comm: "join x y = join y x" +by (rule order_antisym, (simp add: join_right_le join_left_le join_imp_le)+) + +lemma meet_assoc: "meet (meet x y) z = meet x (meet y z)" (is "?l=?r") +proof - + have "?l <= meet x y & meet x y <= x & ?l <= z & meet x y <= y" by (simp add: meet_left_le meet_right_le) + hence "?l <= x & ?l <= y & ?l <= z" by auto + hence "?l <= ?r" by (simp add: meet_imp_le) + hence a:"?l <= meet x (meet y z)" by (simp add: meet_imp_le) + have "?r <= meet y z & meet y z <= y & meet y z <= z & ?r <= x" by (simp add: meet_left_le meet_right_le) + hence "?r <= x & ?r <= y & ?r <= z" by (auto) + hence "?r <= meet x y & ?r <= z" by (simp add: meet_imp_le) + hence b:"?r <= ?l" by (simp add: meet_imp_le) + from a b show "?l = ?r" by auto +qed + +lemma join_assoc: "join (join x y) z = join x (join y z)" (is "?l=?r") +proof - + have "join x y <= ?l & x <= join x y & z <= ?l & y <= join x y" by (simp add: join_left_le join_right_le) + hence "x <= ?l & y <= ?l & z <= ?l" by auto + hence "join y z <= ?l & x <= ?l" by (simp add: join_imp_le) + hence a:"?r <= ?l" by (simp add: join_imp_le) + have "join y z <= ?r & y <= join y z & z <= join y z & x <= ?r" by (simp add: join_left_le join_right_le) + hence "y <= ?r & z <= ?r & x <= ?r" by auto + hence "join x y <= ?r & z <= ?r" by (simp add: join_imp_le) + hence b:"?l <= ?r" by (simp add: join_imp_le) + from a b show "?l = ?r" by auto +qed + +lemma meet_left_comm: "meet a (meet b c) = meet b (meet a c)" +by (simp add: meet_assoc[symmetric, of a b c], simp add: meet_comm[of a b], simp add: meet_assoc) + +lemma meet_left_idempotent: "meet y (meet y x) = meet y x" +by (simp add: meet_assoc meet_comm meet_left_comm) + +lemma join_left_comm: "join a (join b c) = join b (join a c)" +by (simp add: join_assoc[symmetric, of a b c], simp add: join_comm[of a b], simp add: join_assoc) + +lemma join_left_idempotent: "join y (join y x) = join y x" +by (simp add: join_assoc join_comm join_left_comm) + +lemmas meet_aci = meet_assoc meet_comm meet_left_comm meet_left_idempotent + +lemmas join_aci = join_assoc join_comm join_left_comm join_left_idempotent + +lemma le_def_meet: "(x <= y) = (meet x y = x)" +proof - + have u: "x <= y \ meet x y = x" + proof + assume "x <= y" + hence "x <= meet x y & meet x y <= x" by (simp add: meet_imp_le meet_left_le) + thus "meet x y = x" by auto + qed + have v:"meet x y = x \ x <= y" + proof + have a:"meet x y <= y" by (simp add: meet_right_le) + assume "meet x y = x" + hence "x = meet x y" by auto + with a show "x <= y" by (auto) + qed + from u v show ?thesis by blast +qed + +lemma le_def_join: "(x <= y) = (join x y = y)" +proof - + have u: "x <= y \ join x y = y" + proof + assume "x <= y" + hence "join x y <= y & y <= join x y" by (simp add: join_imp_le join_right_le) + thus "join x y = y" by auto + qed + have v:"join x y = y \ x <= y" + proof + have a:"x <= join x y" by (simp add: join_left_le) + assume "join x y = y" + hence "y = join x y" by auto + with a show "x <= y" by (auto) + qed + from u v show ?thesis by blast +qed + +lemma meet_join_absorp: "meet x (join x y) = x" +proof - + have a:"meet x (join x y) <= x" by (simp add: meet_left_le) + have b:"x <= meet x (join x y)" by (rule meet_imp_le, simp_all add: join_left_le) + from a b show ?thesis by auto +qed + +lemma join_meet_absorp: "join x (meet x y) = x" +proof - + have a:"x <= join x (meet x y)" by (simp add: join_left_le) + have b:"join x (meet x y) <= x" by (rule join_imp_le, simp_all add: meet_left_le) + from a b show ?thesis by auto +qed + +lemma meet_mono: "y \ z \ meet x y \ meet x z" +proof - + assume a: "y <= z" + have "meet x y <= x & meet x y <= y" by (simp add: meet_left_le meet_right_le) + with a have "meet x y <= x & meet x y <= z" by auto + thus "meet x y <= meet x z" by (simp add: meet_imp_le) +qed + +lemma join_mono: "y \ z \ join x y \ join x z" +proof - + assume a: "y \ z" + have "x <= join x z & z <= join x z" by (simp add: join_left_le join_right_le) + with a have "x <= join x z & y <= join x z" by auto + thus "join x y <= join x z" by (simp add: join_imp_le) +qed + +lemma distrib_join_le: "join x (meet y z) \ meet (join x y) (join x z)" (is "_ <= ?r") +proof - + have a: "x <= ?r" by (rule meet_imp_le, simp_all add: join_left_le) + from meet_join_le have b: "meet y z <= ?r" + by (rule_tac meet_imp_le, (blast intro: order_trans)+) + from a b show ?thesis by (simp add: join_imp_le) +qed + +lemma distrib_meet_le: "join (meet x y) (meet x z) \ meet x (join y z)" (is "?l <= _") +proof - + have a: "?l <= x" by (rule join_imp_le, simp_all add: meet_left_le) + from meet_join_le have b: "?l <= join y z" + by (rule_tac join_imp_le, (blast intro: order_trans)+) + from a b show ?thesis by (simp add: meet_imp_le) +qed + +lemma meet_join_eq_imp_le: "a = c \ a = d \ b = c \ b = d \ meet a b \ join c d" +by (insert meet_join_le, blast intro: order_trans) + +lemma modular_le: "x \ z \ join x (meet y z) \ meet (join x y) z" (is "_ \ ?t <= _") +proof - + assume a: "x <= z" + have b: "?t <= join x y" by (rule join_imp_le, simp_all add: meet_join_le meet_join_eq_imp_le) + have c: "?t <= z" by (rule join_imp_le, simp_all add: meet_join_le a) + from b c show ?thesis by (simp add: meet_imp_le) +qed + +ML {* +val is_meet_unique = thm "is_meet_unique"; +val is_join_unique = thm "is_join_unique"; +val join_exists = thm "join_exists"; +val meet_exists = thm "meet_exists"; +val is_meet_meet = thm "is_meet_meet"; +val meet_unique = thm "meet_unique"; +val is_join_join = thm "is_join_join"; +val join_unique = thm "join_unique"; +val meet_left_le = thm "meet_left_le"; +val meet_right_le = thm "meet_right_le"; +val meet_imp_le = thm "meet_imp_le"; +val join_left_le = thm "join_left_le"; +val join_right_le = thm "join_right_le"; +val join_imp_le = thm "join_imp_le"; +val meet_join_le = thms "meet_join_le"; +val is_meet_min = thm "is_meet_min"; +val is_join_max = thm "is_join_max"; +val meet_min = thm "meet_min"; +val join_max = thm "join_max"; +val meet_idempotent = thm "meet_idempotent"; +val join_idempotent = thm "join_idempotent"; +val meet_comm = thm "meet_comm"; +val join_comm = thm "join_comm"; +val meet_assoc = thm "meet_assoc"; +val join_assoc = thm "join_assoc"; +val meet_left_comm = thm "meet_left_comm"; +val meet_left_idempotent = thm "meet_left_idempotent"; +val join_left_comm = thm "join_left_comm"; +val join_left_idempotent = thm "join_left_idempotent"; +val meet_aci = thms "meet_aci"; +val join_aci = thms "join_aci"; +val le_def_meet = thm "le_def_meet"; +val le_def_join = thm "le_def_join"; +val meet_join_absorp = thm "meet_join_absorp"; +val join_meet_absorp = thm "join_meet_absorp"; +val meet_mono = thm "meet_mono"; +val join_mono = thm "join_mono"; +val distrib_join_le = thm "distrib_join_le"; +val distrib_meet_le = thm "distrib_meet_le"; +val meet_join_eq_imp_le = thm "meet_join_eq_imp_le"; +val modular_le = thm "modular_le"; +*} + +end \ No newline at end of file diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Library/Multiset.thy Tue May 11 20:11:08 2004 +0200 @@ -108,7 +108,7 @@ theorems union_ac = union_assoc union_commute union_lcomm -instance multiset :: (type) plus_ac0 +instance multiset :: (type) comm_monoid_add proof fix a b c :: "'a multiset" show "(a + b) + c = a + (b + c)" by (rule union_assoc) diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Matrix/Matrix.thy --- a/src/HOL/Matrix/Matrix.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Matrix/Matrix.thy Tue May 11 20:11:08 2004 +0200 @@ -195,7 +195,7 @@ (* constdefs - one_matrix :: "nat \ ('a::semiring) matrix" + one_matrix :: "nat \ ('a::comm_semiring_1_cancel) matrix" "one_matrix n == Abs_matrix (% j i. if j = i & j < n then 1 else 0)" lemma Rep_one_matrix[simp]: "Rep_matrix (one_matrix n) j i = (if (j = i & j < n) then 1 else 0)" @@ -235,9 +235,9 @@ by (simp add: max_def nrows) constdefs - right_inverse_matrix :: "('a::semiring) matrix \ 'a matrix \ bool" + right_inverse_matrix :: "('a::comm_semiring_1_cancel) matrix \ 'a matrix \ bool" "right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X)))" - inverse_matrix :: "('a::semiring) matrix \ 'a matrix \ bool" + inverse_matrix :: "('a::comm_semiring_1_cancel) matrix \ 'a matrix \ bool" "inverse_matrix A X == (right_inverse_matrix A X) \ (right_inverse_matrix X A)" lemma right_inverse_matrix_dim: "right_inverse_matrix A X \ nrows A = ncols X" diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Nat.thy Tue May 11 20:11:08 2004 +0200 @@ -712,8 +712,8 @@ by (induct m) (simp_all add: add_mult_distrib) -text{*The Naturals Form A Semiring*} -instance nat :: semiring +text{*The Naturals Form A comm_semiring_1_cancel*} +instance nat :: comm_semiring_1_cancel proof fix i j k :: nat show "(i + j) + k = i + (j + k)" by (rule nat_add_assoc) @@ -760,8 +760,8 @@ done -text{*The Naturals Form an Ordered Semiring*} -instance nat :: ordered_semiring +text{*The Naturals Form an Ordered comm_semiring_1_cancel*} +instance nat :: ordered_semidom proof fix i j k :: nat show "0 < (1::nat)" by simp diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/NumberTheory/WilsonBij.thy --- a/src/HOL/NumberTheory/WilsonBij.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/NumberTheory/WilsonBij.thy Tue May 11 20:11:08 2004 +0200 @@ -75,7 +75,7 @@ lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)" -- {* same as @{text WilsonRuss} *} apply (unfold zcong_def) - apply (simp add: Ring_and_Field.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2) + apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2) apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans) apply (simp add: mult_commute) apply (subst zdvd_zminus_iff) diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/NumberTheory/WilsonRuss.thy --- a/src/HOL/NumberTheory/WilsonRuss.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/NumberTheory/WilsonRuss.thy Tue May 11 20:11:08 2004 +0200 @@ -86,7 +86,7 @@ lemma inv_not_p_minus_1_aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)" apply (unfold zcong_def) - apply (simp add: Ring_and_Field.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2) + apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2) apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans) apply (simp add: mult_commute) apply (subst zdvd_zminus_iff) diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/OrderedGroup.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/OrderedGroup.thy Tue May 11 20:11:08 2004 +0200 @@ -0,0 +1,950 @@ +(* Title: HOL/Group.thy + ID: $Id$ + Author: Gertrud Bauer and Markus Wenzel, TU Muenchen + Lawrence C Paulson, University of Cambridge + Revised and decoupled from Ring_and_Field.thy + by Steven Obua, TU Muenchen, in May 2004 + License: GPL (GNU GENERAL PUBLIC LICENSE) +*) + +header {* Ordered Groups *} + +theory OrderedGroup = Inductive + LOrder: + +text {* + The theory of partially ordered groups is taken from the books: + \begin{itemize} + \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 + \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963 + \end{itemize} + Most of the used notions can also be looked up in + \begin{itemize} + \item \emph{www.mathworld.com} by Eric Weisstein et. al. + \item \emph{Algebra I} by van der Waerden, Springer. + \end{itemize} +*} + +subsection {* Semigroups, Groups *} + +axclass semigroup_add \ plus + add_assoc: "(a + b) + c = a + (b + c)" + +axclass ab_semigroup_add \ semigroup_add + add_commute: "a + b = b + a" + +lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::ab_semigroup_add))" + by (rule mk_left_commute [of "op +", OF add_assoc add_commute]) + +theorems add_ac = add_assoc add_commute add_left_commute + +axclass semigroup_mult \ times + mult_assoc: "(a * b) * c = a * (b * c)" + +axclass ab_semigroup_mult \ semigroup_mult + mult_commute: "a * b = b * a" + +lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::ab_semigroup_mult))" + by (rule mk_left_commute [of "op *", OF mult_assoc mult_commute]) + +theorems mult_ac = mult_assoc mult_commute mult_left_commute + +axclass comm_monoid_add \ zero, ab_semigroup_add + add_0[simp]: "0 + a = a" + +axclass monoid_mult \ one, semigroup_mult + mult_1_left[simp]: "1 * a = a" + mult_1_right[simp]: "a * 1 = a" + +axclass comm_monoid_mult \ one, ab_semigroup_mult + mult_1: "1 * a = a" + +instance comm_monoid_mult \ monoid_mult +by (intro_classes, insert mult_1, simp_all add: mult_commute, auto) + +axclass cancel_semigroup_add \ semigroup_add + add_left_imp_eq: "a + b = a + c \ b = c" + add_right_imp_eq: "b + a = c + a \ b = c" + +axclass cancel_ab_semigroup_add \ ab_semigroup_add + add_imp_eq: "a + b = a + c \ b = c" + +instance cancel_ab_semigroup_add \ cancel_semigroup_add +proof + { + fix a b c :: 'a + assume "a + b = a + c" + thus "b = c" by (rule add_imp_eq) + } + note f = this + fix a b c :: 'a + assume "b + a = c + a" + hence "a + b = a + c" by (simp only: add_commute) + thus "b = c" by (rule f) +qed + +axclass ab_group_add \ minus, comm_monoid_add + left_minus[simp]: " - a + a = 0" + diff_minus: "a - b = a + (-b)" + +instance ab_group_add \ cancel_ab_semigroup_add +proof + fix a b c :: 'a + assume "a + b = a + c" + hence "-a + a + b = -a + a + c" by (simp only: add_assoc) + thus "b = c" by simp +qed + +lemma add_0_right [simp]: "a + 0 = (a::'a::comm_monoid_add)" +proof - + have "a + 0 = 0 + a" by (simp only: add_commute) + also have "... = a" by simp + finally show ?thesis . +qed + +lemma add_left_cancel [simp]: + "(a + b = a + c) = (b = (c::'a::cancel_semigroup_add))" +by (blast dest: add_left_imp_eq) + +lemma add_right_cancel [simp]: + "(b + a = c + a) = (b = (c::'a::cancel_semigroup_add))" + by (blast dest: add_right_imp_eq) + +lemma right_minus [simp]: "a + -(a::'a::ab_group_add) = 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::ab_group_add))" +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 minus_minus [simp]: "- (- (a::'a::ab_group_add)) = 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::ab_group_add)" +apply (rule right_minus_eq [THEN iffD1, symmetric]) +apply (simp add: diff_minus add_commute) +done + +lemma minus_zero [simp]: "- 0 = (0::'a::ab_group_add)" +by (simp add: equals_zero_I) + +lemma diff_self [simp]: "a - (a::'a::ab_group_add) = 0" + by (simp add: diff_minus) + +lemma diff_0 [simp]: "(0::'a::ab_group_add) - a = -a" +by (simp add: diff_minus) + +lemma diff_0_right [simp]: "a - (0::'a::ab_group_add) = a" +by (simp add: diff_minus) + +lemma diff_minus_eq_add [simp]: "a - - b = a + (b::'a::ab_group_add)" +by (simp add: diff_minus) + +lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::ab_group_add))" +proof + assume "- a = - b" + hence "- (- a) = - (- b)" + by simp + thus "a=b" by simp +next + assume "a=b" + thus "-a = -b" by simp +qed + +lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::ab_group_add))" +by (subst neg_equal_iff_equal [symmetric], simp) + +lemma neg_0_equal_iff_equal [simp]: "(0 = -a) = (0 = (a::'a::ab_group_add))" +by (subst neg_equal_iff_equal [symmetric], simp) + +text{*The next two equations can make the simplifier loop!*} + +lemma equation_minus_iff: "(a = - b) = (b = - (a::'a::ab_group_add))" +proof - + have "(- (-a) = - b) = (- a = b)" by (rule neg_equal_iff_equal) + thus ?thesis by (simp add: eq_commute) +qed + +lemma minus_equation_iff: "(- a = b) = (- (b::'a::ab_group_add) = a)" +proof - + have "(- a = - (-b)) = (a = -b)" by (rule neg_equal_iff_equal) + thus ?thesis by (simp add: eq_commute) +qed + +lemma minus_add_distrib [simp]: "- (a + b) = -a + -(b::'a::ab_group_add)" +apply (rule equals_zero_I) +apply (simp add: add_ac) +done + +lemma minus_diff_eq [simp]: "- (a - b) = b - (a::'a::ab_group_add)" +by (simp add: diff_minus add_commute) + +subsection {* (Partially) Ordered Groups *} + +axclass pordered_ab_semigroup_add \ order, ab_semigroup_add + add_left_mono: "a \ b \ c + a \ c + b" + +axclass pordered_cancel_ab_semigroup_add \ pordered_ab_semigroup_add, cancel_ab_semigroup_add + +instance pordered_cancel_ab_semigroup_add \ pordered_ab_semigroup_add .. + +axclass pordered_ab_semigroup_add_imp_le \ pordered_cancel_ab_semigroup_add + add_le_imp_le_left: "c + a \ c + b \ a \ b" + +axclass pordered_ab_group_add \ ab_group_add, pordered_ab_semigroup_add + +instance pordered_ab_group_add \ pordered_ab_semigroup_add_imp_le +proof + fix a b c :: 'a + assume "c + a \ c + b" + hence "(-c) + (c + a) \ (-c) + (c + b)" by (rule add_left_mono) + hence "((-c) + c) + a \ ((-c) + c) + b" by (simp only: add_assoc) + thus "a \ b" by simp +qed + +axclass ordered_cancel_ab_semigroup_add \ pordered_cancel_ab_semigroup_add, linorder + +instance ordered_cancel_ab_semigroup_add \ pordered_ab_semigroup_add_imp_le +proof + fix a b c :: 'a + assume le: "c + a <= c + b" + show "a <= b" + proof (rule ccontr) + assume w: "~ a \ b" + hence "b <= a" by (simp add: linorder_not_le) + hence le2: "c+b <= c+a" by (rule add_left_mono) + have "a = b" + apply (insert le) + apply (insert le2) + apply (drule order_antisym, simp_all) + done + with w show False + by (simp add: linorder_not_le [symmetric]) + qed +qed + +lemma add_right_mono: "a \ (b::'a::pordered_ab_semigroup_add) ==> a + c \ b + c" +by (simp add: add_commute[of _ c] add_left_mono) + +text {* non-strict, in both arguments *} +lemma add_mono: + "[|a \ b; c \ d|] ==> a + c \ b + (d::'a::pordered_ab_semigroup_add)" + apply (erule add_right_mono [THEN order_trans]) + apply (simp add: add_commute add_left_mono) + done + +lemma add_strict_left_mono: + "a < b ==> c + a < c + (b::'a::pordered_cancel_ab_semigroup_add)" + by (simp add: order_less_le add_left_mono) + +lemma add_strict_right_mono: + "a < b ==> a + c < b + (c::'a::pordered_cancel_ab_semigroup_add)" + by (simp add: add_commute [of _ c] add_strict_left_mono) + +text{*Strict monotonicity in both arguments*} +lemma add_strict_mono: "[|a a + c < b + (d::'a::pordered_cancel_ab_semigroup_add)" +apply (erule add_strict_right_mono [THEN order_less_trans]) +apply (erule add_strict_left_mono) +done + +lemma add_less_le_mono: + "[| ad |] ==> a + c < b + (d::'a::pordered_cancel_ab_semigroup_add)" +apply (erule add_strict_right_mono [THEN order_less_le_trans]) +apply (erule add_left_mono) +done + +lemma add_le_less_mono: + "[| a\b; c a + c < b + (d::'a::pordered_cancel_ab_semigroup_add)" +apply (erule add_right_mono [THEN order_le_less_trans]) +apply (erule add_strict_left_mono) +done + +lemma add_less_imp_less_left: + assumes less: "c + a < c + b" shows "a < (b::'a::pordered_ab_semigroup_add_imp_le)" +proof - + from less have le: "c + a <= c + b" by (simp add: order_le_less) + have "a <= b" + apply (insert le) + apply (drule add_le_imp_le_left) + by (insert le, drule add_le_imp_le_left, assumption) + moreover have "a \ b" + proof (rule ccontr) + assume "~(a \ b)" + then have "a = b" by simp + then have "c + a = c + b" by simp + with less show "False"by simp + qed + ultimately show "a < b" by (simp add: order_le_less) +qed + +lemma add_less_imp_less_right: + "a + c < b + c ==> a < (b::'a::pordered_ab_semigroup_add_imp_le)" +apply (rule add_less_imp_less_left [of c]) +apply (simp add: add_commute) +done + +lemma add_less_cancel_left [simp]: + "(c+a < c+b) = (a < (b::'a::pordered_ab_semigroup_add_imp_le))" +by (blast intro: add_less_imp_less_left add_strict_left_mono) + +lemma add_less_cancel_right [simp]: + "(a+c < b+c) = (a < (b::'a::pordered_ab_semigroup_add_imp_le))" +by (blast intro: add_less_imp_less_right add_strict_right_mono) + +lemma add_le_cancel_left [simp]: + "(c+a \ c+b) = (a \ (b::'a::pordered_ab_semigroup_add_imp_le))" +by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) + +lemma add_le_cancel_right [simp]: + "(a+c \ b+c) = (a \ (b::'a::pordered_ab_semigroup_add_imp_le))" +by (simp add: add_commute[of a c] add_commute[of b c]) + +lemma add_le_imp_le_right: + "a + c \ b + c ==> a \ (b::'a::pordered_ab_semigroup_add_imp_le)" +by simp + +lemma add_increasing: "[|0\a; b\c|] ==> b \ a + (c::'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add})" +by (insert add_mono [of 0 a b c], simp) + +subsection {* Ordering Rules for Unary Minus *} + +lemma le_imp_neg_le: + assumes "a \ (b::'a::{pordered_ab_semigroup_add_imp_le, ab_group_add})" shows "-b \ -a" +proof - + have "-a+a \ -a+b" + by (rule add_left_mono) + hence "0 \ -a+b" + by simp + hence "0 + (-b) \ (-a + b) + (-b)" + by (rule add_right_mono) + thus ?thesis + by (simp add: add_assoc) +qed + +lemma neg_le_iff_le [simp]: "(-b \ -a) = (a \ (b::'a::pordered_ab_group_add))" +proof + assume "- b \ - a" + hence "- (- a) \ - (- b)" + by (rule le_imp_neg_le) + thus "a\b" by simp +next + assume "a\b" + thus "-b \ -a" by (rule le_imp_neg_le) +qed + +lemma neg_le_0_iff_le [simp]: "(-a \ 0) = (0 \ (a::'a::pordered_ab_group_add))" +by (subst neg_le_iff_le [symmetric], simp) + +lemma neg_0_le_iff_le [simp]: "(0 \ -a) = (a \ (0::'a::pordered_ab_group_add))" +by (subst neg_le_iff_le [symmetric], simp) + +lemma neg_less_iff_less [simp]: "(-b < -a) = (a < (b::'a::pordered_ab_group_add))" +by (force simp add: order_less_le) + +lemma neg_less_0_iff_less [simp]: "(-a < 0) = (0 < (a::'a::pordered_ab_group_add))" +by (subst neg_less_iff_less [symmetric], simp) + +lemma neg_0_less_iff_less [simp]: "(0 < -a) = (a < (0::'a::pordered_ab_group_add))" +by (subst neg_less_iff_less [symmetric], simp) + +text{*The next several equations can make the simplifier loop!*} + +lemma less_minus_iff: "(a < - b) = (b < - (a::'a::pordered_ab_group_add))" +proof - + have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less) + thus ?thesis by simp +qed + +lemma minus_less_iff: "(- a < b) = (- b < (a::'a::pordered_ab_group_add))" +proof - + have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less) + thus ?thesis by simp +qed + +lemma le_minus_iff: "(a \ - b) = (b \ - (a::'a::pordered_ab_group_add))" +proof - + have mm: "!! a (b::'a). (-(-a)) < -b \ -(-b) < -a" by (simp only: minus_less_iff) + have "(- (- a) <= -b) = (b <= - a)" + apply (auto simp only: order_le_less) + apply (drule mm) + apply (simp_all) + apply (drule mm[simplified], assumption) + done + then show ?thesis by simp +qed + +lemma minus_le_iff: "(- a \ b) = (- b \ (a::'a::pordered_ab_group_add))" +by (auto simp add: order_le_less minus_less_iff) + +lemma add_diff_eq: "a + (b - c) = (a + b) - (c::'a::ab_group_add)" +by (simp add: diff_minus add_ac) + +lemma diff_add_eq: "(a - b) + c = (a + c) - (b::'a::ab_group_add)" +by (simp add: diff_minus add_ac) + +lemma diff_eq_eq: "(a-b = c) = (a = c + (b::'a::ab_group_add))" +by (auto simp add: diff_minus add_assoc) + +lemma eq_diff_eq: "(a = c-b) = (a + (b::'a::ab_group_add) = c)" +by (auto simp add: diff_minus add_assoc) + +lemma diff_diff_eq: "(a - b) - c = a - (b + (c::'a::ab_group_add))" +by (simp add: diff_minus add_ac) + +lemma diff_diff_eq2: "a - (b - c) = (a + c) - (b::'a::ab_group_add)" +by (simp add: diff_minus add_ac) + +lemma diff_add_cancel: "a - b + b = (a::'a::ab_group_add)" +by (simp add: diff_minus add_ac) + +lemma add_diff_cancel: "a + b - b = (a::'a::ab_group_add)" +by (simp add: diff_minus add_ac) + +text{*Further subtraction laws for ordered rings*} + +lemma less_iff_diff_less_0: "(a < b) = (a - b < (0::'a::pordered_ab_group_add))" +proof - + have "(a < b) = (a + (- b) < b + (-b))" + by (simp only: add_less_cancel_right) + also have "... = (a - b < 0)" by (simp add: diff_minus) + finally show ?thesis . +qed + +lemma diff_less_eq: "(a-b < c) = (a < c + (b::'a::pordered_ab_group_add))" +apply (subst less_iff_diff_less_0) +apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst]) +apply (simp add: diff_minus add_ac) +done + +lemma less_diff_eq: "(a < c-b) = (a + (b::'a::pordered_ab_group_add) < c)" +apply (subst less_iff_diff_less_0) +apply (rule less_iff_diff_less_0 [of _ "c-b", THEN ssubst]) +apply (simp add: diff_minus add_ac) +done + +lemma diff_le_eq: "(a-b \ c) = (a \ c + (b::'a::pordered_ab_group_add))" +by (auto simp add: order_le_less diff_less_eq diff_add_cancel add_diff_cancel) + +lemma le_diff_eq: "(a \ c-b) = (a + (b::'a::pordered_ab_group_add) \ c)" +by (auto simp add: order_le_less less_diff_eq diff_add_cancel add_diff_cancel) + +text{*This list of rewrites simplifies (in)equalities by bringing subtractions + to the top and then moving negative terms to the other side. + Use with @{text add_ac}*} +lemmas compare_rls = + diff_minus [symmetric] + add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2 + diff_less_eq less_diff_eq diff_le_eq le_diff_eq + diff_eq_eq eq_diff_eq + + +subsection{*Lemmas for the @{text cancel_numerals} simproc*} + +lemma eq_iff_diff_eq_0: "(a = b) = (a-b = (0::'a::ab_group_add))" +by (simp add: compare_rls) + +lemma le_iff_diff_le_0: "(a \ b) = (a-b \ (0::'a::pordered_ab_group_add))" +by (simp add: compare_rls) + +subsection {* Lattice Ordered (Abelian) Groups *} + +axclass lordered_ab_group_meet < pordered_ab_group_add, meet_semilorder + +axclass lordered_ab_group_join < pordered_ab_group_add, join_semilorder + +lemma add_meet_distrib_left: "a + (meet b c) = meet (a + b) (a + (c::'a::{pordered_ab_group_add, meet_semilorder}))" +apply (rule order_antisym) +apply (rule meet_imp_le, simp_all add: meet_join_le) +apply (rule add_le_imp_le_left [of "-a"]) +apply (simp only: add_assoc[symmetric], simp) +apply (rule meet_imp_le) +apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp add: meet_join_le)+ +done + +lemma add_join_distrib_left: "a + (join b c) = join (a + b) (a+ (c::'a::{pordered_ab_group_add, join_semilorder}))" +apply (rule order_antisym) +apply (rule add_le_imp_le_left [of "-a"]) +apply (simp only: add_assoc[symmetric], simp) +apply (rule join_imp_le) +apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp add: meet_join_le)+ +apply (rule join_imp_le) +apply (simp_all add: meet_join_le) +done + +lemma is_join_neg_meet: "is_join (% (a::'a::{pordered_ab_group_add, meet_semilorder}) b. - (meet (-a) (-b)))" +apply (auto simp add: is_join_def) +apply (rule_tac c="meet (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_meet_distrib_left meet_join_le) +apply (rule_tac c="meet (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_meet_distrib_left meet_join_le) +apply (subst neg_le_iff_le[symmetric]) +apply (simp add: meet_imp_le) +done + +lemma is_meet_neg_join: "is_meet (% (a::'a::{pordered_ab_group_add, join_semilorder}) b. - (join (-a) (-b)))" +apply (auto simp add: is_meet_def) +apply (rule_tac c="join (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_join_distrib_left meet_join_le) +apply (rule_tac c="join (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_join_distrib_left meet_join_le) +apply (subst neg_le_iff_le[symmetric]) +apply (simp add: join_imp_le) +done + +axclass lordered_ab_group \ pordered_ab_group_add, lorder + +instance lordered_ab_group_meet \ lordered_ab_group +proof + show "? j. is_join (j::'a\'a\('a::lordered_ab_group_meet))" by (blast intro: is_join_neg_meet) +qed + +instance lordered_ab_group_join \ lordered_ab_group +proof + show "? m. is_meet (m::'a\'a\('a::lordered_ab_group_join))" by (blast intro: is_meet_neg_join) +qed + +lemma add_join_distrib_right: "(join a b) + (c::'a::lordered_ab_group) = join (a+c) (b+c)" +proof - + have "c + (join a b) = join (c+a) (c+b)" by (simp add: add_join_distrib_left) + thus ?thesis by (simp add: add_commute) +qed + +lemma add_meet_distrib_right: "(meet a b) + (c::'a::lordered_ab_group) = meet (a+c) (b+c)" +proof - + have "c + (meet a b) = meet (c+a) (c+b)" by (simp add: add_meet_distrib_left) + thus ?thesis by (simp add: add_commute) +qed + +lemmas add_meet_join_distribs = add_meet_distrib_right add_meet_distrib_left add_join_distrib_right add_join_distrib_left + +lemma join_eq_neg_meet: "join a (b::'a::lordered_ab_group) = - meet (-a) (-b)" +by (simp add: is_join_unique[OF is_join_join is_join_neg_meet]) + +lemma meet_eq_neg_join: "meet a (b::'a::lordered_ab_group) = - join (-a) (-b)" +by (simp add: is_meet_unique[OF is_meet_meet is_meet_neg_join]) + +lemma add_eq_meet_join: "a + b = (join a b) + (meet a (b::'a::lordered_ab_group))" +proof - + have "0 = - meet 0 (a-b) + meet (a-b) 0" by (simp add: meet_comm) + hence "0 = join 0 (b-a) + meet (a-b) 0" by (simp add: meet_eq_neg_join) + hence "0 = (-a + join a b) + (meet a b + (-b))" + apply (simp add: add_join_distrib_left add_meet_distrib_right) + by (simp add: diff_minus add_commute) + thus ?thesis + apply (simp add: compare_rls) + apply (subst add_left_cancel[symmetric, of "a+b" "join a b + meet a b" "-a"]) + apply (simp only: add_assoc, simp add: add_assoc[symmetric]) + done +qed + +subsection {* Positive Part, Negative Part, Absolute Value *} + +constdefs + pprt :: "'a \ ('a::lordered_ab_group)" + "pprt x == join x 0" + nprt :: "'a \ ('a::lordered_ab_group)" + "nprt x == meet x 0" + +lemma prts: "a = pprt a + nprt a" +by (simp add: pprt_def nprt_def add_eq_meet_join[symmetric]) + +lemma zero_le_pprt[simp]: "0 \ pprt a" +by (simp add: pprt_def meet_join_le) + +lemma nprt_le_zero[simp]: "nprt a \ 0" +by (simp add: nprt_def meet_join_le) + +lemma le_eq_neg: "(a \ -b) = (a + b \ (0::_::lordered_ab_group))" (is "?l = ?r") +proof - + have a: "?l \ ?r" + apply (auto) + apply (rule add_le_imp_le_right[of _ "-b" _]) + apply (simp add: add_assoc) + done + have b: "?r \ ?l" + apply (auto) + apply (rule add_le_imp_le_right[of _ "b" _]) + apply (simp) + done + from a b show ?thesis by blast +qed + +lemma join_0_imp_0: "join a (-a) = 0 \ a = (0::'a::lordered_ab_group)" +proof - + { + fix a::'a + assume hyp: "join a (-a) = 0" + hence "join a (-a) + a = a" by (simp) + hence "join (a+a) 0 = a" by (simp add: add_join_distrib_right) + hence "join (a+a) 0 <= a" by (simp) + hence "0 <= a" by (blast intro: order_trans meet_join_le) + } + note p = this + thm p + assume hyp:"join a (-a) = 0" + hence hyp2:"join (-a) (-(-a)) = 0" by (simp add: join_comm) + from p[OF hyp] p[OF hyp2] show "a = 0" by simp +qed + +lemma meet_0_imp_0: "meet a (-a) = 0 \ a = (0::'a::lordered_ab_group)" +apply (simp add: meet_eq_neg_join) +apply (simp add: join_comm) +apply (subst join_0_imp_0) +by auto + +lemma join_0_eq_0[simp]: "(join a (-a) = 0) = (a = (0::'a::lordered_ab_group))" +by (auto, erule join_0_imp_0) + +lemma meet_0_eq_0[simp]: "(meet a (-a) = 0) = (a = (0::'a::lordered_ab_group))" +by (auto, erule meet_0_imp_0) + +lemma zero_le_double_add_iff_zero_le_single_add[simp]: "(0 \ a + a) = (0 \ (a::'a::lordered_ab_group))" +proof + assume "0 <= a + a" + hence a:"meet (a+a) 0 = 0" by (simp add: le_def_meet meet_comm) + have "(meet a 0)+(meet a 0) = meet (meet (a+a) 0) a" (is "?l=_") by (simp add: add_meet_join_distribs meet_aci) + hence "?l = 0 + meet a 0" by (simp add: a, simp add: meet_comm) + hence "meet a 0 = 0" by (simp only: add_right_cancel) + then show "0 <= a" by (simp add: le_def_meet meet_comm) +next + assume a: "0 <= a" + show "0 <= a + a" by (simp add: add_mono[OF a a, simplified]) +qed + +lemma double_add_le_zero_iff_single_add_le_zero[simp]: "(a + a <= 0) = ((a::'a::lordered_ab_group) <= 0)" +proof - + have "(a + a <= 0) = (0 <= -(a+a))" by (subst le_minus_iff, simp) + moreover have "\ = (a <= 0)" by (simp add: zero_le_double_add_iff_zero_le_single_add) + ultimately show ?thesis by blast +qed + +lemma double_add_less_zero_iff_single_less_zero[simp]: "(a+a<0) = ((a::'a::{pordered_ab_group_add,linorder}) < 0)" (is ?s) +proof cases + assume a: "a < 0" + thus ?s by (simp add: add_strict_mono[OF a a, simplified]) +next + assume "~(a < 0)" + hence a:"0 <= a" by (simp) + hence "0 <= a+a" by (simp add: add_mono[OF a a, simplified]) + hence "~(a+a < 0)" by simp + with a show ?thesis by simp +qed + +axclass lordered_ab_group_abs \ lordered_ab_group + abs_lattice: "abs x = join x (-x)" + +lemma abs_zero[simp]: "abs 0 = (0::'a::lordered_ab_group_abs)" +by (simp add: abs_lattice) + +lemma abs_eq_0[simp]: "(abs a = 0) = (a = (0::'a::lordered_ab_group_abs))" +by (simp add: abs_lattice) + +lemma abs_0_eq[simp]: "(0 = abs a) = (a = (0::'a::lordered_ab_group_abs))" +proof - + have "(0 = abs a) = (abs a = 0)" by (simp only: eq_ac) + thus ?thesis by simp +qed + +lemma neg_meet_eq_join[simp]: "- meet a (b::_::lordered_ab_group) = join (-a) (-b)" +by (simp add: meet_eq_neg_join) + +lemma neg_join_eq_meet[simp]: "- join a (b::_::lordered_ab_group) = meet (-a) (-b)" +by (simp del: neg_meet_eq_join add: join_eq_neg_meet) + +lemma join_eq_if: "join a (-a) = (if a < 0 then -a else (a::'a::{lordered_ab_group, linorder}))" +proof - + note b = add_le_cancel_right[of a a "-a",symmetric,simplified] + have c: "a + a = 0 \ -a = a" by (rule add_right_imp_eq[of _ a], simp) + show ?thesis + apply (auto simp add: join_max max_def b linorder_not_less) + apply (drule order_antisym, auto) + done +qed + +lemma abs_if_lattice: "\a\ = (if a < 0 then -a else (a::'a::{lordered_ab_group_abs, linorder}))" +proof - + show ?thesis by (simp add: abs_lattice join_eq_if) +qed + +lemma abs_ge_zero[simp]: "0 \ abs (a::'a::lordered_ab_group_abs)" +proof - + have a:"a <= abs a" and b:"-a <= abs a" by (auto simp add: abs_lattice meet_join_le) + show ?thesis by (rule add_mono[OF a b, simplified]) +qed + +lemma abs_le_zero_iff [simp]: "(abs a \ (0::'a::lordered_ab_group_abs)) = (a = 0)" +proof + assume "abs a <= 0" + hence "abs a = 0" by (auto dest: order_antisym) + thus "a = 0" by simp +next + assume "a = 0" + thus "abs a <= 0" by simp +qed + +lemma zero_less_abs_iff [simp]: "(0 < abs a) = (a \ (0::'a::lordered_ab_group_abs))" +by (simp add: order_less_le) + +lemma abs_not_less_zero [simp]: "~ abs a < (0::'a::lordered_ab_group_abs)" +proof - + have a:"!! x (y::_::order). x <= y \ ~(y < x)" by auto + show ?thesis by (simp add: a) +qed + +lemma abs_ge_self: "a \ abs (a::'a::lordered_ab_group_abs)" +by (simp add: abs_lattice meet_join_le) + +lemma abs_ge_minus_self: "-a \ abs (a::'a::lordered_ab_group_abs)" +by (simp add: abs_lattice meet_join_le) + +lemma le_imp_join_eq: "a \ b \ join a b = b" +by (simp add: le_def_join) + +lemma ge_imp_join_eq: "b \ a \ join a b = a" +by (simp add: le_def_join join_aci) + +lemma le_imp_meet_eq: "a \ b \ meet a b = a" +by (simp add: le_def_meet) + +lemma ge_imp_meet_eq: "b \ a \ meet a b = b" +by (simp add: le_def_meet meet_aci) + +lemma abs_prts: "abs (a::_::lordered_ab_group_abs) = pprt a - nprt a" +apply (simp add: pprt_def nprt_def diff_minus) +apply (simp add: add_meet_join_distribs join_aci abs_lattice[symmetric]) +apply (subst le_imp_join_eq, auto) +done + +lemma abs_minus_cancel [simp]: "abs (-a) = abs(a::'a::lordered_ab_group_abs)" +by (simp add: abs_lattice join_comm) + +lemma abs_idempotent [simp]: "abs (abs a) = abs (a::'a::lordered_ab_group_abs)" +apply (simp add: abs_lattice[of "abs a"]) +apply (subst ge_imp_join_eq) +apply (rule order_trans[of _ 0]) +by auto + +lemma zero_le_iff_zero_nprt: "(0 \ a) = (nprt a = 0)" +by (simp add: le_def_meet nprt_def meet_comm) + +lemma le_zero_iff_zero_pprt: "(a \ 0) = (pprt a = 0)" +by (simp add: le_def_join pprt_def join_comm) + +lemma le_zero_iff_pprt_id: "(0 \ a) = (pprt a = a)" +by (simp add: le_def_join pprt_def join_comm) + +lemma zero_le_iff_nprt_id: "(a \ 0) = (nprt a = a)" +by (simp add: le_def_meet nprt_def meet_comm) + +lemma iff2imp: "(A=B) \ (A \ B)" +by (simp) + +lemma imp_abs_id: "0 \ a \ abs a = (a::'a::lordered_ab_group_abs)" +by (simp add: iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_pprt_id] abs_prts) + +lemma imp_abs_neg_id: "a \ 0 \ abs a = -(a::'a::lordered_ab_group_abs)" +by (simp add: iff2imp[OF le_zero_iff_zero_pprt] iff2imp[OF zero_le_iff_nprt_id] abs_prts) + +lemma abs_leI: "[|a \ b; -a \ b|] ==> abs a \ (b::'a::lordered_ab_group_abs)" +by (simp add: abs_lattice join_imp_le) + +lemma le_minus_self_iff: "(a \ -a) = (a \ (0::'a::lordered_ab_group))" +proof - + from add_le_cancel_left[of "-a" "a+a" "0"] have "(a <= -a) = (a+a <= 0)" + by (simp add: add_assoc[symmetric]) + thus ?thesis by simp +qed + +lemma minus_le_self_iff: "(-a \ a) = (0 \ (a::'a::lordered_ab_group))" +proof - + from add_le_cancel_left[of "-a" "0" "a+a"] have "(-a <= a) = (0 <= a+a)" + by (simp add: add_assoc[symmetric]) + thus ?thesis by simp +qed + +lemma abs_le_D1: "abs a \ b ==> a \ (b::'a::lordered_ab_group_abs)" +by (insert abs_ge_self, blast intro: order_trans) + +lemma abs_le_D2: "abs a \ b ==> -a \ (b::'a::lordered_ab_group_abs)" +by (insert abs_le_D1 [of "-a"], simp) + +lemma abs_le_iff: "(abs a \ b) = (a \ b & -a \ (b::'a::lordered_ab_group_abs))" +by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2) + +lemma abs_triangle_ineq: "abs (a+b) \ abs a + abs (b::'a::lordered_ab_group_abs)" +proof - + have g:"abs a + abs b = join (a+b) (join (-a-b) (join (-a+b) (a + (-b))))" (is "_=join ?m ?n") + apply (simp add: abs_lattice add_meet_join_distribs join_aci) + by (simp only: diff_minus) + have a:"a+b <= join ?m ?n" by (simp add: meet_join_le) + have b:"-a-b <= ?n" by (simp add: meet_join_le) + have c:"?n <= join ?m ?n" by (simp add: meet_join_le) + from b c have d: "-a-b <= join ?m ?n" by simp + have e:"-a-b = -(a+b)" by (simp add: diff_minus) + from a d e have "abs(a+b) <= join ?m ?n" + by (drule_tac abs_leI, auto) + with g[symmetric] show ?thesis by simp +qed + +lemma abs_diff_triangle_ineq: + "\(a::'a::lordered_ab_group_abs) + b - (c+d)\ \ \a-c\ + \b-d\" +proof - + have "\a + b - (c+d)\ = \(a-c) + (b-d)\" by (simp add: diff_minus add_ac) + also have "... \ \a-c\ + \b-d\" by (rule abs_triangle_ineq) + finally show ?thesis . +qed + +ML {* +val add_zero_left = thm"add_0"; +val add_zero_right = thm"add_0_right"; +*} + +ML {* +val add_assoc = thm "add_assoc"; +val add_commute = thm "add_commute"; +val add_left_commute = thm "add_left_commute"; +val add_ac = thms "add_ac"; +val mult_assoc = thm "mult_assoc"; +val mult_commute = thm "mult_commute"; +val mult_left_commute = thm "mult_left_commute"; +val mult_ac = thms "mult_ac"; +val add_0 = thm "add_0"; +val mult_1_left = thm "mult_1_left"; +val mult_1_right = thm "mult_1_right"; +val mult_1 = thm "mult_1"; +val add_left_imp_eq = thm "add_left_imp_eq"; +val add_right_imp_eq = thm "add_right_imp_eq"; +val add_imp_eq = thm "add_imp_eq"; +val left_minus = thm "left_minus"; +val diff_minus = thm "diff_minus"; +val add_0_right = thm "add_0_right"; +val add_left_cancel = thm "add_left_cancel"; +val add_right_cancel = thm "add_right_cancel"; +val right_minus = thm "right_minus"; +val right_minus_eq = thm "right_minus_eq"; +val minus_minus = thm "minus_minus"; +val equals_zero_I = thm "equals_zero_I"; +val minus_zero = thm "minus_zero"; +val diff_self = thm "diff_self"; +val diff_0 = thm "diff_0"; +val diff_0_right = thm "diff_0_right"; +val diff_minus_eq_add = thm "diff_minus_eq_add"; +val neg_equal_iff_equal = thm "neg_equal_iff_equal"; +val neg_equal_0_iff_equal = thm "neg_equal_0_iff_equal"; +val neg_0_equal_iff_equal = thm "neg_0_equal_iff_equal"; +val equation_minus_iff = thm "equation_minus_iff"; +val minus_equation_iff = thm "minus_equation_iff"; +val minus_add_distrib = thm "minus_add_distrib"; +val minus_diff_eq = thm "minus_diff_eq"; +val add_left_mono = thm "add_left_mono"; +val add_le_imp_le_left = thm "add_le_imp_le_left"; +val add_right_mono = thm "add_right_mono"; +val add_mono = thm "add_mono"; +val add_strict_left_mono = thm "add_strict_left_mono"; +val add_strict_right_mono = thm "add_strict_right_mono"; +val add_strict_mono = thm "add_strict_mono"; +val add_less_le_mono = thm "add_less_le_mono"; +val add_le_less_mono = thm "add_le_less_mono"; +val add_less_imp_less_left = thm "add_less_imp_less_left"; +val add_less_imp_less_right = thm "add_less_imp_less_right"; +val add_less_cancel_left = thm "add_less_cancel_left"; +val add_less_cancel_right = thm "add_less_cancel_right"; +val add_le_cancel_left = thm "add_le_cancel_left"; +val add_le_cancel_right = thm "add_le_cancel_right"; +val add_le_imp_le_right = thm "add_le_imp_le_right"; +val add_increasing = thm "add_increasing"; +val le_imp_neg_le = thm "le_imp_neg_le"; +val neg_le_iff_le = thm "neg_le_iff_le"; +val neg_le_0_iff_le = thm "neg_le_0_iff_le"; +val neg_0_le_iff_le = thm "neg_0_le_iff_le"; +val neg_less_iff_less = thm "neg_less_iff_less"; +val neg_less_0_iff_less = thm "neg_less_0_iff_less"; +val neg_0_less_iff_less = thm "neg_0_less_iff_less"; +val less_minus_iff = thm "less_minus_iff"; +val minus_less_iff = thm "minus_less_iff"; +val le_minus_iff = thm "le_minus_iff"; +val minus_le_iff = thm "minus_le_iff"; +val add_diff_eq = thm "add_diff_eq"; +val diff_add_eq = thm "diff_add_eq"; +val diff_eq_eq = thm "diff_eq_eq"; +val eq_diff_eq = thm "eq_diff_eq"; +val diff_diff_eq = thm "diff_diff_eq"; +val diff_diff_eq2 = thm "diff_diff_eq2"; +val diff_add_cancel = thm "diff_add_cancel"; +val add_diff_cancel = thm "add_diff_cancel"; +val less_iff_diff_less_0 = thm "less_iff_diff_less_0"; +val diff_less_eq = thm "diff_less_eq"; +val less_diff_eq = thm "less_diff_eq"; +val diff_le_eq = thm "diff_le_eq"; +val le_diff_eq = thm "le_diff_eq"; +val compare_rls = thms "compare_rls"; +val eq_iff_diff_eq_0 = thm "eq_iff_diff_eq_0"; +val le_iff_diff_le_0 = thm "le_iff_diff_le_0"; +val add_meet_distrib_left = thm "add_meet_distrib_left"; +val add_join_distrib_left = thm "add_join_distrib_left"; +val is_join_neg_meet = thm "is_join_neg_meet"; +val is_meet_neg_join = thm "is_meet_neg_join"; +val add_join_distrib_right = thm "add_join_distrib_right"; +val add_meet_distrib_right = thm "add_meet_distrib_right"; +val add_meet_join_distribs = thms "add_meet_join_distribs"; +val join_eq_neg_meet = thm "join_eq_neg_meet"; +val meet_eq_neg_join = thm "meet_eq_neg_join"; +val add_eq_meet_join = thm "add_eq_meet_join"; +val prts = thm "prts"; +val zero_le_pprt = thm "zero_le_pprt"; +val nprt_le_zero = thm "nprt_le_zero"; +val le_eq_neg = thm "le_eq_neg"; +val join_0_imp_0 = thm "join_0_imp_0"; +val meet_0_imp_0 = thm "meet_0_imp_0"; +val join_0_eq_0 = thm "join_0_eq_0"; +val meet_0_eq_0 = thm "meet_0_eq_0"; +val zero_le_double_add_iff_zero_le_single_add = thm "zero_le_double_add_iff_zero_le_single_add"; +val double_add_le_zero_iff_single_add_le_zero = thm "double_add_le_zero_iff_single_add_le_zero"; +val double_add_less_zero_iff_single_less_zero = thm "double_add_less_zero_iff_single_less_zero"; +val abs_lattice = thm "abs_lattice"; +val abs_zero = thm "abs_zero"; +val abs_eq_0 = thm "abs_eq_0"; +val abs_0_eq = thm "abs_0_eq"; +val neg_meet_eq_join = thm "neg_meet_eq_join"; +val neg_join_eq_meet = thm "neg_join_eq_meet"; +val join_eq_if = thm "join_eq_if"; +val abs_if_lattice = thm "abs_if_lattice"; +val abs_ge_zero = thm "abs_ge_zero"; +val abs_le_zero_iff = thm "abs_le_zero_iff"; +val zero_less_abs_iff = thm "zero_less_abs_iff"; +val abs_not_less_zero = thm "abs_not_less_zero"; +val abs_ge_self = thm "abs_ge_self"; +val abs_ge_minus_self = thm "abs_ge_minus_self"; +val le_imp_join_eq = thm "le_imp_join_eq"; +val ge_imp_join_eq = thm "ge_imp_join_eq"; +val le_imp_meet_eq = thm "le_imp_meet_eq"; +val ge_imp_meet_eq = thm "ge_imp_meet_eq"; +val abs_prts = thm "abs_prts"; +val abs_minus_cancel = thm "abs_minus_cancel"; +val abs_idempotent = thm "abs_idempotent"; +val zero_le_iff_zero_nprt = thm "zero_le_iff_zero_nprt"; +val le_zero_iff_zero_pprt = thm "le_zero_iff_zero_pprt"; +val le_zero_iff_pprt_id = thm "le_zero_iff_pprt_id"; +val zero_le_iff_nprt_id = thm "zero_le_iff_nprt_id"; +val iff2imp = thm "iff2imp"; +val imp_abs_id = thm "imp_abs_id"; +val imp_abs_neg_id = thm "imp_abs_neg_id"; +val abs_leI = thm "abs_leI"; +val le_minus_self_iff = thm "le_minus_self_iff"; +val minus_le_self_iff = thm "minus_le_self_iff"; +val abs_le_D1 = thm "abs_le_D1"; +val abs_le_D2 = thm "abs_le_D2"; +val abs_le_iff = thm "abs_le_iff"; +val abs_triangle_ineq = thm "abs_triangle_ineq"; +val abs_diff_triangle_ineq = thm "abs_diff_triangle_ineq"; +*} + +end diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Power.thy --- a/src/HOL/Power.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Power.thy Tue May 11 20:11:08 2004 +0200 @@ -11,7 +11,7 @@ subsection{*Powers for Arbitrary (Semi)Rings*} -axclass ringpower \ semiring, power +axclass ringpower \ comm_semiring_1_cancel, power power_0 [simp]: "a ^ 0 = 1" power_Suc: "a ^ (Suc n) = a * (a ^ n)" @@ -46,31 +46,31 @@ done lemma zero_less_power: - "0 < (a::'a::{ordered_semiring,ringpower}) ==> 0 < a^n" + "0 < (a::'a::{ordered_semidom,ringpower}) ==> 0 < a^n" apply (induct_tac "n") apply (simp_all add: power_Suc zero_less_one mult_pos) done lemma zero_le_power: - "0 \ (a::'a::{ordered_semiring,ringpower}) ==> 0 \ a^n" + "0 \ (a::'a::{ordered_semidom,ringpower}) ==> 0 \ a^n" apply (simp add: order_le_less) apply (erule disjE) apply (simp_all add: zero_less_power zero_less_one power_0_left) done lemma one_le_power: - "1 \ (a::'a::{ordered_semiring,ringpower}) ==> 1 \ a^n" + "1 \ (a::'a::{ordered_semidom,ringpower}) ==> 1 \ a^n" apply (induct_tac "n") apply (simp_all add: power_Suc) apply (rule order_trans [OF _ mult_mono [of 1 _ 1]]) apply (simp_all add: zero_le_one order_trans [OF zero_le_one]) done -lemma gt1_imp_ge0: "1 < a ==> 0 \ (a::'a::ordered_semiring)" +lemma gt1_imp_ge0: "1 < a ==> 0 \ (a::'a::ordered_semidom)" by (simp add: order_trans [OF zero_le_one order_less_imp_le]) lemma power_gt1_lemma: - assumes gt1: "1 < (a::'a::{ordered_semiring,ringpower})" + assumes gt1: "1 < (a::'a::{ordered_semidom,ringpower})" shows "1 < a * a^n" proof - have "1*1 < a*1" using gt1 by simp @@ -81,11 +81,11 @@ qed lemma power_gt1: - "1 < (a::'a::{ordered_semiring,ringpower}) ==> 1 < a ^ (Suc n)" + "1 < (a::'a::{ordered_semidom,ringpower}) ==> 1 < a ^ (Suc n)" by (simp add: power_gt1_lemma power_Suc) lemma power_le_imp_le_exp: - assumes gt1: "(1::'a::{ringpower,ordered_semiring}) < a" + assumes gt1: "(1::'a::{ringpower,ordered_semidom}) < a" shows "!!n. a^m \ a^n ==> m \ n" proof (induct m) case 0 @@ -109,26 +109,26 @@ text{*Surely we can strengthen this? It holds for @{text "0 (a^m = a^n) = (m=n)" + "1 < (a::'a::{ordered_semidom,ringpower}) ==> (a^m = a^n) = (m=n)" by (force simp add: order_antisym power_le_imp_le_exp) text{*Can relax the first premise to @{term "0 m < n" + "[| (1::'a::{ringpower,ordered_semidom}) < a; a^m < a^n |] ==> m < n" by (simp add: order_less_le [of m n] order_less_le [of "a^m" "a^n"] power_le_imp_le_exp) lemma power_mono: - "[|a \ b; (0::'a::{ringpower,ordered_semiring}) \ a|] ==> a^n \ b^n" + "[|a \ b; (0::'a::{ringpower,ordered_semidom}) \ a|] ==> a^n \ b^n" apply (induct_tac "n") apply (simp_all add: power_Suc) apply (auto intro: mult_mono zero_le_power order_trans [of 0 a b]) done lemma power_strict_mono [rule_format]: - "[|a < b; (0::'a::{ringpower,ordered_semiring}) \ a|] + "[|a < b; (0::'a::{ringpower,ordered_semidom}) \ a|] ==> 0 < n --> a^n < b^n" apply (induct_tac "n") apply (auto simp add: mult_strict_mono zero_le_power power_Suc @@ -136,7 +136,7 @@ done lemma power_eq_0_iff [simp]: - "(a^n = 0) = (a = (0::'a::{ordered_ring,ringpower}) & 0 (0::'a::{ordered_ring,ringpower}) | n=0)" + "(0 < (abs a)^n) = (a \ (0::'a::{ordered_idom,ringpower}) | n=0)" proof (induct "n") case 0 show ?case by (simp add: zero_less_one) @@ -190,12 +190,12 @@ qed lemma zero_le_power_abs [simp]: - "(0::'a::{ordered_ring,ringpower}) \ (abs a)^n" + "(0::'a::{ordered_idom,ringpower}) \ (abs a)^n" apply (induct_tac "n") apply (auto simp add: zero_le_one zero_le_power) done -lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{ring,ringpower}) ^ n" +lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{comm_ring_1,ringpower}) ^ n" proof - have "-a = (- 1) * a" by (simp add: minus_mult_left [symmetric]) thus ?thesis by (simp only: power_mult_distrib) @@ -203,14 +203,14 @@ text{*Lemma for @{text power_strict_decreasing}*} lemma power_Suc_less: - "[|(0::'a::{ordered_semiring,ringpower}) < a; a < 1|] + "[|(0::'a::{ordered_semidom,ringpower}) < a; a < 1|] ==> a * a^n < a^n" apply (induct_tac n) apply (auto simp add: power_Suc mult_strict_left_mono) done lemma power_strict_decreasing: - "[|n < N; 0 < a; a < (1::'a::{ordered_semiring,ringpower})|] + "[|n < N; 0 < a; a < (1::'a::{ordered_semidom,ringpower})|] ==> a^N < a^n" apply (erule rev_mp) apply (induct_tac "N") @@ -223,7 +223,7 @@ text{*Proof resembles that of @{text power_strict_decreasing}*} lemma power_decreasing: - "[|n \ N; 0 \ a; a \ (1::'a::{ordered_semiring,ringpower})|] + "[|n \ N; 0 \ a; a \ (1::'a::{ordered_semidom,ringpower})|] ==> a^N \ a^n" apply (erule rev_mp) apply (induct_tac "N") @@ -235,13 +235,13 @@ done lemma power_Suc_less_one: - "[| 0 < a; a < (1::'a::{ordered_semiring,ringpower}) |] ==> a ^ Suc n < 1" + "[| 0 < a; a < (1::'a::{ordered_semidom,ringpower}) |] ==> a ^ Suc n < 1" apply (insert power_strict_decreasing [of 0 "Suc n" a], simp) done text{*Proof again resembles that of @{text power_strict_decreasing}*} lemma power_increasing: - "[|n \ N; (1::'a::{ordered_semiring,ringpower}) \ a|] ==> a^n \ a^N" + "[|n \ N; (1::'a::{ordered_semidom,ringpower}) \ a|] ==> a^n \ a^N" apply (erule rev_mp) apply (induct_tac "N") apply (auto simp add: power_Suc le_Suc_eq) @@ -253,13 +253,13 @@ text{*Lemma for @{text power_strict_increasing}*} lemma power_less_power_Suc: - "(1::'a::{ordered_semiring,ringpower}) < a ==> a^n < a * a^n" + "(1::'a::{ordered_semidom,ringpower}) < a ==> a^n < a * a^n" apply (induct_tac n) apply (auto simp add: power_Suc mult_strict_left_mono order_less_trans [OF zero_less_one]) done lemma power_strict_increasing: - "[|n < N; (1::'a::{ordered_semiring,ringpower}) < a|] ==> a^n < a^N" + "[|n < N; (1::'a::{ordered_semidom,ringpower}) < a|] ==> a^n < a^N" apply (erule rev_mp) apply (induct_tac "N") apply (auto simp add: power_less_power_Suc power_Suc less_Suc_eq) @@ -272,7 +272,7 @@ lemma power_le_imp_le_base: assumes le: "a ^ Suc n \ b ^ Suc n" - and xnonneg: "(0::'a::{ordered_semiring,ringpower}) \ a" + and xnonneg: "(0::'a::{ordered_semidom,ringpower}) \ a" and ynonneg: "0 \ b" shows "a \ b" proof (rule ccontr) @@ -286,7 +286,7 @@ lemma power_inject_base: "[| a ^ Suc n = b ^ Suc n; 0 \ a; 0 \ b |] - ==> a = (b::'a::{ordered_semiring,ringpower})" + ==> a = (b::'a::{ordered_semidom,ringpower})" by (blast intro: power_le_imp_le_base order_antisym order_eq_refl sym) diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Presburger.thy Tue May 11 20:11:08 2004 +0200 @@ -704,7 +704,7 @@ have "P x \ P (x - i * d)" using step.hyps by blast also have "\ \ P(x - (i + 1) * d)" using minus[THEN spec, of "x - i * d"] - by (simp add:int_distrib Ring_and_Field.diff_diff_eq[symmetric]) + by (simp add:int_distrib OrderedGroup.diff_diff_eq[symmetric]) ultimately show "P x \ P(x - (i + 1) * d)" by blast qed qed diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Real/PReal.thy --- a/src/HOL/Real/PReal.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Real/PReal.thy Tue May 11 20:11:08 2004 +0200 @@ -15,7 +15,7 @@ text{*As a special case, the sum of two positives is positive. One of the premises could be weakened to the relation @{text "\"}.*} -lemma pos_add_strict: "[|0 b < a + (c::'a::ordered_semiring)" +lemma pos_add_strict: "[|0 b < a + (c::'a::ordered_semidom)" by (insert add_strict_mono [of 0 a b c], simp) lemma interval_empty_iff: diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Real/RealDef.thy --- a/src/HOL/Real/RealDef.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Real/RealDef.thy Tue May 11 20:11:08 2004 +0200 @@ -169,7 +169,7 @@ lemma real_add_zero_left: "(0::real) + z = z" by (cases z, simp add: real_add real_zero_def preal_add_ac) -instance real :: plus_ac0 +instance real :: comm_monoid_add by (intro_classes, (assumption | rule real_add_commute real_add_assoc real_add_zero_left)+) @@ -281,9 +281,6 @@ instance real :: 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 (rule real_add_minus_left) show "x - y = x + (-y)" by (simp add: real_diff_def) show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc) @@ -312,7 +309,7 @@ minus_mult_left [symmetric, simp] lemma real_mult_1_right: "z * (1::real) = z" - by (rule Ring_and_Field.mult_1_right) + by (rule OrderedGroup.mult_1_right) subsection{*The @{text "\"} Ordering*} @@ -554,11 +551,11 @@ by (blast intro!: real_less_all_preal linorder_not_less [THEN iffD1]) lemma real_add_less_le_mono: "[| w'z |] ==> w' + z' < w + (z::real)" - by (rule Ring_and_Field.add_less_le_mono) + by (rule OrderedGroup.add_less_le_mono) lemma real_add_le_less_mono: "!!z z'::real. [| w'\w; z' w' + z' < w + z" - by (rule Ring_and_Field.add_le_less_mono) + by (rule OrderedGroup.add_le_less_mono) lemma real_le_square [simp]: "(0::real) \ x*x" by (rule Ring_and_Field.zero_le_square) @@ -597,7 +594,7 @@ text{*FIXME: delete or at least combine the next two lemmas*} lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)" -apply (drule Ring_and_Field.equals_zero_I [THEN sym]) +apply (drule OrderedGroup.equals_zero_I [THEN sym]) apply (cut_tac x = y in real_le_square) apply (auto, drule order_antisym, auto) done @@ -848,7 +845,7 @@ by (force simp add: Ring_and_Field.abs_less_iff) lemma abs_le_interval_iff: "(abs x \ r) = (-r\x & x\(r::real))" -by (force simp add: Ring_and_Field.abs_le_iff) +by (force simp add: OrderedGroup.abs_le_iff) (*FIXME: used only once, in SEQ.ML*) lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)" @@ -892,7 +889,7 @@ val abs_minus_eqI2 = thm"abs_minus_eqI2"; val abs_ge_zero = thm"abs_ge_zero"; val abs_idempotent = thm"abs_idempotent"; -val abs_zero_iff = thm"abs_zero_iff"; +val abs_eq_0 = thm"abs_eq_0"; val abs_ge_self = thm"abs_ge_self"; val abs_ge_minus_self = thm"abs_ge_minus_self"; val abs_mult = thm"abs_mult"; diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Ring_and_Field.thy Tue May 11 20:11:08 2004 +0200 @@ -2,286 +2,132 @@ ID: $Id$ Author: Gertrud Bauer and Markus Wenzel, TU Muenchen Lawrence C Paulson, University of Cambridge + Revised and splitted into Ring_and_Field.thy and Group.thy + by Steven Obua, TU Muenchen, in May 2004 License: GPL (GNU GENERAL PUBLIC LICENSE) *) -header {* Ring and field structures *} - -theory Ring_and_Field = Inductive: +header {* (Ordered) Rings and Fields *} -subsection {* Abstract algebraic structures *} - -subsection {* Types Classes @{text plus_ac0} and @{text times_ac1} *} +theory Ring_and_Field = OrderedGroup: -axclass plus_ac0 \ plus, zero - commute: "x + y = y + x" - assoc: "(x + y) + z = x + (y + z)" - zero [simp]: "0 + x = x" - -lemma plus_ac0_left_commute: "x + (y+z) = y + ((x+z)::'a::plus_ac0)" -by(rule mk_left_commute[of "op +",OF plus_ac0.assoc plus_ac0.commute]) +text {* + The theory of partially ordered rings is taken from the books: + \begin{itemize} + \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 + \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963 + \end{itemize} + Most of the used notions can also be looked up in + \begin{itemize} + \item \emph{www.mathworld.com} by Eric Weisstein et. al. + \item \emph{Algebra I} by van der Waerden, Springer. + \end{itemize} +*} -lemma plus_ac0_zero_right [simp]: "x + 0 = (x ::'a::plus_ac0)" -apply (rule plus_ac0.commute [THEN trans]) -apply (rule plus_ac0.zero) -done +axclass semiring \ ab_semigroup_add, semigroup_mult + left_distrib: "(a + b) * c = a * c + b * c" + right_distrib: "a * (b + c) = a * b + a * c" -lemmas plus_ac0 = plus_ac0.assoc plus_ac0.commute plus_ac0_left_commute - plus_ac0.zero plus_ac0_zero_right +axclass semiring_0 \ semiring, comm_monoid_add -axclass times_ac1 \ times, one - commute: "x * y = y * x" - assoc: "(x * y) * z = x * (y * z)" - one [simp]: "1 * x = x" +axclass comm_semiring \ ab_semigroup_add, ab_semigroup_mult + mult_commute: "a * b = b * a" + distrib: "(a + b) * c = a * c + b * c" -theorem times_ac1_left_commute: "(x::'a::times_ac1) * ((y::'a) * z) = - y * (x * z)" -by(rule mk_left_commute[of "op *",OF times_ac1.assoc times_ac1.commute]) - -theorem times_ac1_one_right [simp]: "(x::'a::times_ac1) * 1 = x" -proof - - have "x * 1 = 1 * x" - by (rule times_ac1.commute) - also have "... = x" - by (rule times_ac1.one) - finally show ?thesis . +instance comm_semiring \ semiring +proof + fix a b c :: 'a + show "(a + b) * c = a * c + b * c" by (simp add: distrib) + have "a * (b + c) = (b + c) * a" by (simp add: mult_ac) + also have "... = b * a + c * a" by (simp only: distrib) + also have "... = a * b + a * c" by (simp add: mult_ac) + finally show "a * (b + c) = a * b + a * c" by blast qed -theorems times_ac1 = times_ac1.assoc times_ac1.commute times_ac1_left_commute - times_ac1.one times_ac1_one_right - +axclass comm_semiring_0 \ comm_semiring, comm_monoid_add -text{*This class is the same as @{text plus_ac0}, while using the same axiom -names as the other axclasses.*} -axclass abelian_semigroup \ zero, plus - add_assoc: "(a + b) + c = a + (b + c)" - add_commute: "a + b = b + a" - add_0 [simp]: "0 + a = a" +instance comm_semiring_0 \ semiring_0 .. -text{*This class underlies both @{text semiring} and @{text ring}*} -axclass almost_semiring \ abelian_semigroup, one, times - mult_assoc: "(a * b) * c = a * (b * c)" - mult_commute: "a * b = b * a" - mult_1 [simp]: "1 * a = a" - - left_distrib: "(a + b) * c = a * c + b * c" +axclass axclass_0_neq_1 \ zero, one zero_neq_one [simp]: "0 \ 1" +axclass semiring_1 \ axclass_0_neq_1, semiring_0, monoid_mult -axclass semiring \ almost_semiring - add_left_imp_eq: "a + b = a + c ==> b=c" - --{*This axiom is needed for semirings only: for rings, etc., it is - redundant. Including it allows many more of the following results - to be proved for semirings too.*} +axclass comm_semiring_1 \ axclass_0_neq_1, comm_semiring_0, comm_monoid_mult (* previously almost_semiring *) + +instance comm_semiring_1 \ semiring_1 .. -instance abelian_semigroup \ plus_ac0 -proof - fix x y z :: 'a - show "x + y = y + x" by (rule add_commute) - show "x + y + z = x + (y + z)" by (rule add_assoc) - show "0+x = x" by (rule add_0) -qed +axclass axclass_no_zero_divisors \ zero, times + no_zero_divisors: "a \ 0 \ b \ 0 \ a * b \ 0" -instance almost_semiring \ times_ac1 -proof - fix x y z :: 'a - show "x * y = y * x" by (rule mult_commute) - show "x * y * z = x * (y * z)" by (rule mult_assoc) - show "1*x = x" by simp -qed +axclass comm_semiring_1_cancel \ comm_semiring_1, cancel_ab_semigroup_add (* previously semiring *) + +axclass ring \ semiring, ab_group_add + +instance ring \ semiring_0 .. -axclass abelian_group \ abelian_semigroup, minus - left_minus [simp]: "-a + a = 0" - diff_minus: "a - b = a + -b" +axclass comm_ring \ comm_semiring_0, ab_group_add + +instance comm_ring \ ring .. -axclass ring \ almost_semiring, abelian_group +instance comm_ring \ comm_semiring_0 .. + +axclass ring_1 \ ring, semiring_1 -text{*Proving axiom @{text add_left_imp_eq} makes all @{text semiring} - theorems available to members of @{term ring} *} -instance ring \ semiring -proof - fix a b c :: 'a - assume "a + b = a + c" - hence "-a + a + b = -a + a + c" by (simp only: add_assoc) - thus "b = c" by simp -qed +axclass comm_ring_1 \ comm_ring, comm_semiring_1 (* previously ring *) + +instance comm_ring_1 \ ring_1 .. -text{*This class underlies @{text ordered_semiring} and @{text ordered_ring}*} -axclass almost_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" +instance comm_ring_1 \ comm_semiring_1_cancel .. -axclass ordered_semiring \ almost_ordered_semiring - zero_less_one [simp]: "0 < 1" --{*This too is needed for semirings only.*} +axclass idom \ comm_ring_1, axclass_no_zero_divisors -axclass ordered_ring \ almost_ordered_semiring, ring - abs_if: "\a\ = (if a < 0 then -a else a)" - -axclass field \ ring, inverse +axclass field \ comm_ring_1, inverse left_inverse [simp]: "a \ 0 ==> inverse a * a = 1" divide_inverse: "a / b = a * inverse b" -axclass ordered_field \ ordered_ring, field +lemma mult_zero_left [simp]: "0 * a = (0::'a::{semiring_0, cancel_semigroup_add})" +proof - + have "0*a + 0*a = 0*a + 0" + by (simp add: left_distrib [symmetric]) + thus ?thesis + by (simp only: add_left_cancel) +qed +lemma mult_zero_right [simp]: "a * 0 = (0::'a::{semiring_0, cancel_semigroup_add})" +proof - + have "a*0 + a*0 = a*0 + 0" + by (simp add: right_distrib [symmetric]) + thus ?thesis + by (simp only: add_left_cancel) +qed + +lemma field_mult_eq_0_iff [simp]: "(a*b = (0::'a::field)) = (a = 0 | b = 0)" +proof cases + assume "a=0" thus ?thesis by simp +next + assume anz [simp]: "a\0" + { assume "a * b = 0" + hence "inverse a * (a * b) = 0" by simp + hence "b = 0" by (simp (no_asm_use) add: mult_assoc [symmetric])} + thus ?thesis by force +qed + +instance field \ idom +by (intro_classes, simp) + axclass division_by_zero \ zero, inverse inverse_zero [simp]: "inverse 0 = 0" - -subsection {* Derived Rules for Addition *} - -lemma add_0_right [simp]: "a + 0 = (a::'a::plus_ac0)" -proof - - have "a + 0 = 0 + a" by (rule plus_ac0.commute) - also have "... = a" by simp - finally show ?thesis . -qed - -lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::plus_ac0))" - by (rule mk_left_commute [of "op +", OF plus_ac0.assoc plus_ac0.commute]) - -theorems add_ac = add_assoc add_commute add_left_commute - -lemma right_minus [simp]: "a + -(a::'a::abelian_group) = 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::abelian_group))" -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 add_left_cancel [simp]: - "(a + b = a + c) = (b = (c::'a::semiring))" -by (blast dest: add_left_imp_eq) - -lemma add_right_cancel [simp]: - "(b + a = c + a) = (b = (c::'a::semiring))" - by (simp add: add_commute) - -lemma minus_minus [simp]: "- (- (a::'a::abelian_group)) = a" -apply (rule right_minus_eq [THEN iffD1]) -apply (simp add: diff_minus) -done - -lemma equals_zero_I: "a+b = 0 ==> -a = (b::'a::abelian_group)" -apply (rule right_minus_eq [THEN iffD1, symmetric]) -apply (simp add: diff_minus add_commute) -done - -lemma minus_zero [simp]: "- 0 = (0::'a::abelian_group)" -by (simp add: equals_zero_I) - -lemma diff_self [simp]: "a - (a::'a::abelian_group) = 0" - by (simp add: diff_minus) - -lemma diff_0 [simp]: "(0::'a::abelian_group) - a = -a" -by (simp add: diff_minus) - -lemma diff_0_right [simp]: "a - (0::'a::abelian_group) = a" -by (simp add: diff_minus) - -lemma diff_minus_eq_add [simp]: "a - - b = a + (b::'a::abelian_group)" -by (simp add: diff_minus) - -lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::abelian_group))" -proof - assume "- a = - b" - hence "- (- a) = - (- b)" - by simp - thus "a=b" by simp -next - assume "a=b" - thus "-a = -b" by simp -qed - -lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::abelian_group))" -by (subst neg_equal_iff_equal [symmetric], simp) - -lemma neg_0_equal_iff_equal [simp]: "(0 = -a) = (0 = (a::'a::abelian_group))" -by (subst neg_equal_iff_equal [symmetric], simp) - -lemma add_minus_self [simp]: "a + b - b = (a::'a::abelian_group)"; - by (simp add: diff_minus add_assoc) - -lemma add_minus_self_left [simp]: "a + (b - a) = (b::'a::abelian_group)"; -by (simp add: diff_minus add_left_commute [of a]) - -lemma add_minus_self_right [simp]: "a + b - a = (b::'a::abelian_group)"; -by (simp add: diff_minus add_left_commute [of a] add_assoc) - -lemma minus_add_self [simp]: "a - b + b = (a::'a::abelian_group)"; -by (simp add: diff_minus add_assoc) - -text{*The next two equations can make the simplifier loop!*} - -lemma equation_minus_iff: "(a = - b) = (b = - (a::'a::abelian_group))" -proof - - have "(- (-a) = - b) = (- a = b)" by (rule neg_equal_iff_equal) - thus ?thesis by (simp add: eq_commute) -qed - -lemma minus_equation_iff: "(- a = b) = (- (b::'a::abelian_group) = a)" -proof - - have "(- a = - (-b)) = (a = -b)" by (rule neg_equal_iff_equal) - thus ?thesis by (simp add: eq_commute) -qed - - -subsection {* Derived rules for multiplication *} - -lemma mult_1_right [simp]: "a * (1::'a::almost_semiring) = a" -proof - - have "a * 1 = 1 * a" by (simp add: mult_commute) - also have "... = a" by simp - finally show ?thesis . -qed - -lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::almost_semiring))" - by (rule mk_left_commute [of "op *", OF mult_assoc mult_commute]) - -theorems mult_ac = mult_assoc mult_commute mult_left_commute - -lemma mult_zero_left [simp]: "0 * a = (0::'a::semiring)" -proof - - have "0*a + 0*a = 0*a + 0" - by (simp add: left_distrib [symmetric]) - thus ?thesis by (simp only: add_left_cancel) -qed - -lemma mult_zero_right [simp]: "a * 0 = (0::'a::semiring)" - by (simp add: mult_commute) - - subsection {* Distribution rules *} -lemma right_distrib: "a * (b + c) = a * b + a * (c::'a::almost_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 text{*For the @{text combine_numerals} simproc*} lemma combine_common_factor: - "a*e + (b*e + c) = (a+b)*e + (c::'a::almost_semiring)" + "a*e + (b*e + c) = (a+b)*e + (c::'a::semiring)" by (simp add: left_distrib add_ac) -lemma minus_add_distrib [simp]: "- (a + b) = -a + -(b::'a::abelian_group)" -apply (rule equals_zero_I) -apply (simp add: plus_ac0) -done - lemma minus_mult_left: "- (a * b) = (-a) * (b::'a::ring)" apply (rule equals_zero_I) apply (simp add: left_distrib [symmetric]) @@ -303,237 +149,86 @@ minus_mult_left [symmetric] minus_mult_right [symmetric]) lemma left_diff_distrib: "(a - b) * c = a * c - b * (c::'a::ring)" -by (simp add: mult_commute [of _ c] right_diff_distrib) - -lemma minus_diff_eq [simp]: "- (a - b) = b - (a::'a::ring)" -by (simp add: diff_minus add_commute) - - -subsection {* Ordering Rules for Addition *} - -lemma add_right_mono: "a \ (b::'a::almost_ordered_semiring) ==> a + c \ b + c" -by (simp add: add_commute [of _ c] add_left_mono) +by (simp add: left_distrib diff_minus + minus_mult_left [symmetric] minus_mult_right [symmetric]) -text {* non-strict, in both arguments *} -lemma add_mono: - "[|a \ b; c \ d|] ==> a + c \ b + (d::'a::almost_ordered_semiring)" - apply (erule add_right_mono [THEN order_trans]) - apply (simp add: add_commute add_left_mono) - done +axclass pordered_semiring \ semiring_0, pordered_ab_semigroup_add + mult_left_mono: "a <= b \ 0 <= c \ c * a <= c * b" + mult_right_mono: "a <= b \ 0 <= c \ a * c <= b * c" -lemma add_strict_left_mono: - "a < b ==> c + a < c + (b::'a::almost_ordered_semiring)" - by (simp add: order_less_le add_left_mono) - -lemma add_strict_right_mono: - "a < b ==> a + c < b + (c::'a::almost_ordered_semiring)" - by (simp add: add_commute [of _ c] add_strict_left_mono) +axclass pordered_cancel_semiring \ pordered_semiring, cancel_ab_semigroup_add -text{*Strict monotonicity in both arguments*} -lemma add_strict_mono: "[|a a + c < b + (d::'a::almost_ordered_semiring)" -apply (erule add_strict_right_mono [THEN order_less_trans]) -apply (erule add_strict_left_mono) -done - -lemma add_less_le_mono: - "[| ad |] ==> a + c < b + (d::'a::almost_ordered_semiring)" -apply (erule add_strict_right_mono [THEN order_less_le_trans]) -apply (erule add_left_mono) -done +axclass ordered_semiring_strict \ semiring_0, ordered_cancel_ab_semigroup_add + mult_strict_left_mono: "a < b \ 0 < c \ c * a < c * b" + mult_strict_right_mono: "a < b \ 0 < c \ a * c < b * c" -lemma add_le_less_mono: - "[| a\b; c a + c < b + (d::'a::almost_ordered_semiring)" -apply (erule add_right_mono [THEN order_le_less_trans]) -apply (erule add_strict_left_mono) -done - -lemma add_less_imp_less_left: - assumes less: "c + a < c + b" shows "a < (b::'a::almost_ordered_semiring)" -proof (rule ccontr) - assume "~ a < b" - hence "b \ a" by (simp add: linorder_not_less) - hence "c+b \ c+a" by (rule add_left_mono) - with this and less show False - by (simp add: linorder_not_less [symmetric]) -qed - -lemma add_less_imp_less_right: - "a + c < b + c ==> a < (b::'a::almost_ordered_semiring)" -apply (rule add_less_imp_less_left [of c]) -apply (simp add: add_commute) +instance ordered_semiring_strict \ pordered_cancel_semiring +apply intro_classes +apply (case_tac "a < b & 0 < c") +apply (auto simp add: mult_strict_left_mono order_less_le) +apply (auto simp add: mult_strict_left_mono order_le_less) +apply (simp add: mult_strict_right_mono) done -lemma add_less_cancel_left [simp]: - "(c+a < c+b) = (a < (b::'a::almost_ordered_semiring))" -by (blast intro: add_less_imp_less_left add_strict_left_mono) - -lemma add_less_cancel_right [simp]: - "(a+c < b+c) = (a < (b::'a::almost_ordered_semiring))" -by (blast intro: add_less_imp_less_right add_strict_right_mono) +axclass pordered_comm_semiring \ comm_semiring_0, pordered_ab_semigroup_add + mult_mono: "a <= b \ 0 <= c \ c * a <= c * b" -lemma add_le_cancel_left [simp]: - "(c+a \ c+b) = (a \ (b::'a::almost_ordered_semiring))" -by (simp add: linorder_not_less [symmetric]) - -lemma add_le_cancel_right [simp]: - "(a+c \ b+c) = (a \ (b::'a::almost_ordered_semiring))" -by (simp add: linorder_not_less [symmetric]) - -lemma add_le_imp_le_left: - "c + a \ c + b ==> a \ (b::'a::almost_ordered_semiring)" -by simp +axclass pordered_cancel_comm_semiring \ pordered_comm_semiring, cancel_ab_semigroup_add -lemma add_le_imp_le_right: - "a + c \ b + c ==> a \ (b::'a::almost_ordered_semiring)" -by simp - -lemma add_increasing: "[|0\a; b\c|] ==> b \ a + (c::'a::almost_ordered_semiring)" -by (insert add_mono [of 0 a b c], simp) - - -subsection {* Ordering Rules for Unary Minus *} +instance pordered_cancel_comm_semiring \ pordered_comm_semiring .. -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) - hence "0 \ -a+b" - by simp - hence "0 + (-b) \ (-a + b) + (-b)" - by (rule add_right_mono) - thus ?thesis - by (simp add: add_assoc) -qed +axclass ordered_comm_semiring_strict \ comm_semiring_0, ordered_cancel_ab_semigroup_add + mult_strict_mono: "a < b \ 0 < c \ c * a < c * b" -lemma neg_le_iff_le [simp]: "(-b \ -a) = (a \ (b::'a::ordered_ring))" -proof - assume "- b \ - a" - hence "- (- a) \ - (- b)" - by (rule le_imp_neg_le) - thus "a\b" by simp -next - assume "a\b" - thus "-b \ -a" by (rule le_imp_neg_le) -qed +instance pordered_comm_semiring \ pordered_semiring +by (intro_classes, insert mult_mono, simp_all add: mult_commute, blast+) -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) +instance pordered_cancel_comm_semiring \ pordered_cancel_semiring .. -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) - -text{*The next several equations can make the simplifier loop!*} +instance ordered_comm_semiring_strict \ ordered_semiring_strict +by (intro_classes, insert mult_strict_mono, simp_all add: mult_commute, blast+) -lemma less_minus_iff: "(a < - b) = (b < - (a::'a::ordered_ring))" -proof - - have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less) - thus ?thesis by simp -qed - -lemma minus_less_iff: "(- a < b) = (- b < (a::'a::ordered_ring))" -proof - - have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less) - thus ?thesis by simp -qed - -lemma le_minus_iff: "(a \ - b) = (b \ - (a::'a::ordered_ring))" -apply (simp add: linorder_not_less [symmetric]) -apply (rule minus_less_iff) +instance ordered_comm_semiring_strict \ pordered_cancel_comm_semiring +apply (intro_classes) +apply (case_tac "a < b & 0 < c") +apply (auto simp add: mult_strict_left_mono order_less_le) +apply (auto simp add: mult_strict_left_mono order_le_less) done -lemma minus_le_iff: "(- a \ b) = (- b \ (a::'a::ordered_ring))" -apply (simp add: linorder_not_less [symmetric]) -apply (rule less_minus_iff) -done - - -subsection{*Subtraction Laws*} +axclass pordered_ring \ ring, pordered_semiring -lemma add_diff_eq: "a + (b - c) = (a + b) - (c::'a::abelian_group)" -by (simp add: diff_minus plus_ac0) +instance pordered_ring \ pordered_ab_group_add .. -lemma diff_add_eq: "(a - b) + c = (a + c) - (b::'a::abelian_group)" -by (simp add: diff_minus plus_ac0) - -lemma diff_eq_eq: "(a-b = c) = (a = c + (b::'a::abelian_group))" -by (auto simp add: diff_minus add_assoc) +instance pordered_ring \ pordered_cancel_semiring .. -lemma eq_diff_eq: "(a = c-b) = (a + (b::'a::abelian_group) = c)" -by (auto simp add: diff_minus add_assoc) - -lemma diff_diff_eq: "(a - b) - c = a - (b + (c::'a::abelian_group))" -by (simp add: diff_minus plus_ac0) - -lemma diff_diff_eq2: "a - (b - c) = (a + c) - (b::'a::abelian_group)" -by (simp add: diff_minus plus_ac0) +axclass lordered_ring \ pordered_ring, lordered_ab_group_abs -text{*Further subtraction laws for ordered rings*} +axclass axclass_abs_if \ minus, ord, zero + abs_if: "abs a = (if (a < 0) then (-a) else a)" -lemma less_iff_diff_less_0: "(a < b) = (a - b < (0::'a::ordered_ring))" -proof - - have "(a < b) = (a + (- b) < b + (-b))" - by (simp only: add_less_cancel_right) - also have "... = (a - b < 0)" by (simp add: diff_minus) - finally show ?thesis . -qed +axclass ordered_ring_strict \ ring, ordered_semiring_strict, axclass_abs_if -lemma diff_less_eq: "(a-b < c) = (a < c + (b::'a::ordered_ring))" -apply (subst less_iff_diff_less_0) -apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst]) -apply (simp add: diff_minus add_ac) -done +instance ordered_ring_strict \ lordered_ab_group .. -lemma less_diff_eq: "(a < c-b) = (a + (b::'a::ordered_ring) < c)" -apply (subst less_iff_diff_less_0) -apply (rule less_iff_diff_less_0 [of _ "c-b", THEN ssubst]) -apply (simp add: diff_minus add_ac) -done +instance ordered_ring_strict \ lordered_ring +by (intro_classes, simp add: abs_if join_eq_if) -lemma diff_le_eq: "(a-b \ c) = (a \ c + (b::'a::ordered_ring))" -by (simp add: linorder_not_less [symmetric] less_diff_eq) - -lemma le_diff_eq: "(a \ c-b) = (a + (b::'a::ordered_ring) \ c)" -by (simp add: linorder_not_less [symmetric] diff_less_eq) +axclass pordered_comm_ring \ comm_ring, pordered_comm_semiring -text{*This list of rewrites simplifies (in)equalities by bringing subtractions - to the top and then moving negative terms to the other side. - Use with @{text add_ac}*} -lemmas compare_rls = - diff_minus [symmetric] - add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2 - diff_less_eq less_diff_eq diff_le_eq le_diff_eq - diff_eq_eq eq_diff_eq +axclass ordered_semidom \ comm_semiring_1_cancel, ordered_comm_semiring_strict (* previously ordered_semiring *) + zero_less_one [simp]: "0 < 1" -text{*This list of rewrites decides ring equalities by ordered rewriting.*} -lemmas ring_eq_simps = - times_ac1.assoc times_ac1.commute times_ac1_left_commute - left_distrib right_distrib left_diff_distrib right_diff_distrib - plus_ac0.assoc plus_ac0.commute plus_ac0_left_commute - add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2 - diff_eq_eq eq_diff_eq +axclass ordered_idom \ comm_ring_1, ordered_comm_semiring_strict, axclass_abs_if (* previously ordered_ring *) -subsection{*Lemmas for the @{text cancel_numerals} simproc*} +instance ordered_idom \ ordered_ring_strict .. -lemma eq_iff_diff_eq_0: "(a = b) = (a-b = (0::'a::abelian_group))" -by (simp add: compare_rls) - -lemma le_iff_diff_le_0: "(a \ b) = (a-b \ (0::'a::ordered_ring))" -by (simp add: compare_rls) +axclass ordered_field \ field, ordered_idom lemma eq_add_iff1: "(a*e + c = b*e + d) = ((a-b)*e + c = (d::'a::ring))" +apply (simp add: diff_minus left_distrib) apply (simp add: diff_minus left_distrib add_ac) -apply (simp add: compare_rls minus_mult_left [symmetric]) +apply (simp add: compare_rls minus_mult_left [symmetric]) done lemma eq_add_iff2: @@ -543,167 +238,199 @@ done lemma less_add_iff1: - "(a*e + c < b*e + d) = ((a-b)*e + c < (d::'a::ordered_ring))" + "(a*e + c < b*e + d) = ((a-b)*e + c < (d::'a::pordered_ring))" apply (simp add: diff_minus left_distrib add_ac) apply (simp add: compare_rls minus_mult_left [symmetric]) done lemma less_add_iff2: - "(a*e + c < b*e + d) = (c < (b-a)*e + (d::'a::ordered_ring))" + "(a*e + c < b*e + d) = (c < (b-a)*e + (d::'a::pordered_ring))" apply (simp add: diff_minus left_distrib add_ac) apply (simp add: compare_rls minus_mult_left [symmetric]) done lemma le_add_iff1: - "(a*e + c \ b*e + d) = ((a-b)*e + c \ (d::'a::ordered_ring))" + "(a*e + c \ b*e + d) = ((a-b)*e + c \ (d::'a::pordered_ring))" apply (simp add: diff_minus left_distrib add_ac) apply (simp add: compare_rls minus_mult_left [symmetric]) done lemma le_add_iff2: - "(a*e + c \ b*e + d) = (c \ (b-a)*e + (d::'a::ordered_ring))" + "(a*e + c \ b*e + d) = (c \ (b-a)*e + (d::'a::pordered_ring))" apply (simp add: diff_minus left_distrib add_ac) apply (simp add: compare_rls minus_mult_left [symmetric]) done - subsection {* Ordering Rules for Multiplication *} -lemma mult_strict_right_mono: - "[|a < b; 0 < c|] ==> a * c < b * (c::'a::almost_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::almost_ordered_semiring)" - apply (case_tac "c=0", simp) - apply (force simp add: mult_strict_left_mono order_le_less) - done - -lemma mult_right_mono: - "[|a \ b; 0 \ c|] ==> a*c \ b * (c::'a::almost_ordered_semiring)" - by (simp add: mult_left_mono mult_commute [of _ c]) - lemma mult_left_le_imp_le: - "[|c*a \ c*b; 0 < c|] ==> a \ (b::'a::almost_ordered_semiring)" + "[|c*a \ c*b; 0 < c|] ==> a \ (b::'a::ordered_semiring_strict)" by (force simp add: mult_strict_left_mono linorder_not_less [symmetric]) lemma mult_right_le_imp_le: - "[|a*c \ b*c; 0 < c|] ==> a \ (b::'a::almost_ordered_semiring)" + "[|a*c \ b*c; 0 < c|] ==> a \ (b::'a::ordered_semiring_strict)" by (force simp add: mult_strict_right_mono linorder_not_less [symmetric]) lemma mult_left_less_imp_less: - "[|c*a < c*b; 0 \ c|] ==> a < (b::'a::almost_ordered_semiring)" + "[|c*a < c*b; 0 \ c|] ==> a < (b::'a::ordered_semiring_strict)" by (force simp add: mult_left_mono linorder_not_le [symmetric]) lemma mult_right_less_imp_less: - "[|a*c < b*c; 0 \ c|] ==> a < (b::'a::almost_ordered_semiring)" + "[|a*c < b*c; 0 \ c|] ==> a < (b::'a::ordered_semiring_strict)" by (force simp add: mult_right_mono linorder_not_le [symmetric]) lemma mult_strict_left_mono_neg: - "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring)" + "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring_strict)" apply (drule mult_strict_left_mono [of _ _ "-c"]) apply (simp_all add: minus_mult_left [symmetric]) done +lemma mult_left_mono_neg: + "[|b \ a; c \ 0|] ==> c * a \ c * (b::'a::pordered_ring)" +apply (drule mult_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)" + "[|b < a; c < 0|] ==> a * c < b * (c::'a::ordered_ring_strict)" apply (drule mult_strict_right_mono [of _ _ "-c"]) apply (simp_all add: minus_mult_right [symmetric]) done +lemma mult_right_mono_neg: + "[|b \ a; c \ 0|] ==> a * c \ (b::'a::pordered_ring) * c" +apply (drule mult_right_mono [of _ _ "-c"]) +apply (simp) +apply (simp_all add: minus_mult_right [symmetric]) +done subsection{* Products of Signs *} -lemma mult_pos: "[| (0::'a::almost_ordered_semiring) < a; 0 < b |] ==> 0 < a*b" +lemma mult_pos: "[| (0::'a::ordered_semiring_strict) < a; 0 < b |] ==> 0 < a*b" by (drule mult_strict_left_mono [of 0 b], auto) -lemma mult_pos_neg: "[| (0::'a::almost_ordered_semiring) < a; b < 0 |] ==> a*b < 0" +lemma mult_pos_le: "[| (0::'a::pordered_cancel_semiring) \ a; 0 \ b |] ==> 0 \ a*b" +by (drule mult_left_mono [of 0 b], auto) + +lemma mult_pos_neg: "[| (0::'a::ordered_semiring_strict) < 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" +lemma mult_pos_neg_le: "[| (0::'a::pordered_cancel_semiring) \ a; b \ 0 |] ==> a*b \ 0" +by (drule mult_left_mono [of b 0], auto) + +lemma mult_pos_neg2: "[| (0::'a::ordered_semiring_strict) < a; b < 0 |] ==> b*a < 0" +by (drule mult_strict_right_mono[of b 0], auto) + +lemma mult_pos_neg2_le: "[| (0::'a::pordered_cancel_semiring) \ a; b \ 0 |] ==> b*a \ 0" +by (drule mult_right_mono[of b 0], auto) + +lemma mult_neg: "[| a < (0::'a::ordered_ring_strict); b < 0 |] ==> 0 < a*b" by (drule mult_strict_right_mono_neg, auto) +lemma mult_neg_le: "[| a \ (0::'a::pordered_ring); b \ 0 |] ==> 0 \ a*b" +by (drule mult_right_mono_neg[of a 0 b ], auto) + lemma zero_less_mult_pos: - "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::almost_ordered_semiring)" + "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::ordered_semiring_strict)" 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_pos2: + "[| 0 < b*a; 0 < a|] ==> 0 < (b::'a::ordered_semiring_strict)" +apply (case_tac "b\0") + apply (auto simp add: order_le_less linorder_not_less) +apply (drule_tac mult_pos_neg2 [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)" + "((0::'a::ordered_ring_strict) < 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) +apply (blast dest: zero_less_mult_pos2) done text{*A field has no "zero divisors", and this theorem holds without the assumption of an ordering. See @{text field_mult_eq_0_iff} below.*} -lemma mult_eq_0_iff [simp]: "(a*b = (0::'a::ordered_ring)) = (a = 0 | b = 0)" +lemma mult_eq_0_iff [simp]: "(a*b = (0::'a::ordered_ring_strict)) = (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)" + "((0::'a::ordered_ring_strict) \ 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)" + "(a*b < (0::'a::ordered_ring_strict)) = (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)" + "(a*b \ (0::'a::ordered_ring_strict)) = (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" +lemma split_mult_pos_le: "(0 \ a & 0 \ b) | (a \ 0 & b \ 0) \ 0 \ a * (b::_::pordered_ring)" +by (auto simp add: mult_pos_le mult_neg_le) + +lemma split_mult_neg_le: "(0 \ a & b \ 0) | (a \ 0 & 0 \ b) \ a * b \ (0::_::pordered_cancel_semiring)" +by (auto simp add: mult_pos_neg_le mult_pos_neg2_le) + +lemma zero_le_square: "(0::'a::ordered_ring_strict) \ a*a" by (simp add: zero_le_mult_iff linorder_linear) -text{*Proving axiom @{text zero_less_one} makes all @{text ordered_semiring} - theorems available to members of @{term ordered_ring} *} -instance ordered_ring \ ordered_semiring +text{*Proving axiom @{text zero_less_one} makes all @{text ordered_semidom} + theorems available to members of @{term ordered_idom} *} + +instance ordered_idom \ ordered_semidom proof have "(0::'a) \ 1*1" by (rule zero_le_square) thus "(0::'a) < 1" by (simp add: order_le_less) qed +instance ordered_ring_strict \ axclass_no_zero_divisors +by (intro_classes, simp) + +instance ordered_idom \ idom .. + text{*All three types of comparision involving 0 and 1 are covered.*} declare zero_neq_one [THEN not_sym, simp] -lemma zero_le_one [simp]: "(0::'a::ordered_semiring) \ 1" +lemma zero_le_one [simp]: "(0::'a::ordered_semidom) \ 1" by (rule zero_less_one [THEN order_less_imp_le]) -lemma not_one_le_zero [simp]: "~ (1::'a::ordered_semiring) \ 0" -by (simp add: linorder_not_le zero_less_one) +lemma not_one_le_zero [simp]: "~ (1::'a::ordered_semidom) \ 0" +by (simp add: linorder_not_le) -lemma not_one_less_zero [simp]: "~ (1::'a::ordered_semiring) < 0" -by (simp add: linorder_not_less zero_le_one) - +lemma not_one_less_zero [simp]: "~ (1::'a::ordered_semidom) < 0" +by (simp add: linorder_not_less) subsection{*More Monotonicity*} lemma mult_left_mono_neg: - "[|b \ a; c \ 0|] ==> c * a \ c * (b::'a::ordered_ring)" + "[|b \ a; c \ 0|] ==> c * a \ c * (b::'a::pordered_ring)" apply (drule mult_left_mono [of _ _ "-c"]) apply (simp_all add: minus_mult_left [symmetric]) done lemma mult_right_mono_neg: - "[|b \ a; c \ 0|] ==> a * c \ b * (c::'a::ordered_ring)" - by (simp add: mult_left_mono_neg mult_commute [of _ c]) + "[|b \ a; c \ 0|] ==> a * c \ b * (c::'a::pordered_ring)" +apply (drule mult_right_mono [of _ _ "-c"]) +apply (simp_all add: minus_mult_right [symmetric]) +done text{*Strict monotonicity in both arguments*} lemma mult_strict_mono: - "[|ac|] ==> a * c < b * (d::'a::ordered_semiring)" + "[|ac|] ==> a * c < b * (d::'a::ordered_semiring_strict)" apply (case_tac "c=0") apply (simp add: mult_pos) apply (erule mult_strict_right_mono [THEN order_less_trans]) @@ -713,31 +440,30 @@ text{*This weaker variant has more natural premises*} lemma mult_strict_mono': - "[| a a; 0 \ c|] ==> a * c < b * (d::'a::ordered_semiring)" + "[| a a; 0 \ c|] ==> a * c < b * (d::'a::ordered_semiring_strict)" apply (rule mult_strict_mono) apply (blast intro: order_le_less_trans)+ done lemma mult_mono: "[|a \ b; c \ d; 0 \ b; 0 \ c|] - ==> a * c \ b * (d::'a::ordered_semiring)" + ==> a * c \ b * (d::'a::pordered_semiring)" apply (erule mult_right_mono [THEN order_trans], assumption) apply (erule mult_left_mono, assumption) done -lemma less_1_mult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::'a::ordered_semiring)" +lemma less_1_mult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::'a::ordered_semidom)" apply (insert mult_strict_mono [of 1 m 1 n]) apply (simp add: order_less_trans [OF zero_less_one]) done - subsection{*Cancellation Laws for Relationships With a Common Factor*} text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"}, also with the relations @{text "\"} and equality.*} lemma mult_less_cancel_right: - "(a*c < b*c) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring)))" + "(a*c < b*c) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring_strict)))" apply (case_tac "c = 0") apply (auto simp add: linorder_neq_iff mult_strict_right_mono mult_strict_right_mono_neg) @@ -750,20 +476,29 @@ done lemma mult_less_cancel_left: - "(c*a < c*b) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring)))" -by (simp add: mult_commute [of c] mult_less_cancel_right) + "(c*a < c*b) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring_strict)))" +apply (case_tac "c = 0") +apply (auto simp add: linorder_neq_iff mult_strict_left_mono + mult_strict_left_mono_neg) +apply (auto simp add: linorder_not_less + linorder_not_le [symmetric, of "c*a"] + linorder_not_le [symmetric, of a]) +apply (erule_tac [!] notE) +apply (auto simp add: order_less_imp_le mult_left_mono + mult_left_mono_neg) +done lemma mult_le_cancel_right: - "(a*c \ b*c) = ((0 a\b) & (c<0 --> b \ (a::'a::ordered_ring)))" + "(a*c \ b*c) = ((0 a\b) & (c<0 --> b \ (a::'a::ordered_ring_strict)))" by (simp add: linorder_not_less [symmetric] mult_less_cancel_right) lemma mult_le_cancel_left: - "(c*a \ c*b) = ((0 a\b) & (c<0 --> b \ (a::'a::ordered_ring)))" -by (simp add: mult_commute [of c] mult_le_cancel_right) + "(c*a \ c*b) = ((0 a\b) & (c<0 --> b \ (a::'a::ordered_ring_strict)))" +by (simp add: linorder_not_less [symmetric] mult_less_cancel_left) lemma mult_less_imp_less_left: assumes less: "c*a < c*b" and nonneg: "0 \ c" - shows "a < (b::'a::ordered_semiring)" + shows "a < (b::'a::ordered_semiring_strict)" proof (rule ccontr) assume "~ a < b" hence "b \ a" by (simp add: linorder_not_less) @@ -773,12 +508,19 @@ qed lemma mult_less_imp_less_right: - "[|a*c < b*c; 0 \ c|] ==> a < (b::'a::ordered_semiring)" - by (rule mult_less_imp_less_left, simp add: mult_commute) + assumes less: "a*c < b*c" and nonneg: "0 <= c" + shows "a < (b::'a::ordered_semiring_strict)" +proof (rule ccontr) + assume "~ a < b" + hence "b \ a" by (simp add: linorder_not_less) + hence "b*c \ a*c" by (rule mult_right_mono) + with this and less show False + by (simp add: linorder_not_less [symmetric]) +qed text{*Cancellation of equalities with a common factor*} lemma mult_cancel_right [simp]: - "(a*c = b*c) = (c = (0::'a::ordered_ring) | a=b)" + "(a*c = b*c) = (c = (0::'a::ordered_ring_strict) | a=b)" apply (cut_tac linorder_less_linear [of 0 c]) apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono simp add: linorder_neq_iff) @@ -787,10 +529,21 @@ text{*These cancellation theorems require an ordering. Versions are proved below that work for fields without an ordering.*} lemma mult_cancel_left [simp]: - "(c*a = c*b) = (c = (0::'a::ordered_ring) | a=b)" -by (simp add: mult_commute [of c] mult_cancel_right) + "(c*a = c*b) = (c = (0::'a::ordered_ring_strict) | a=b)" +apply (cut_tac linorder_less_linear [of 0 c]) +apply (force dest: mult_strict_left_mono_neg mult_strict_left_mono + simp add: linorder_neq_iff) +done - +text{*This list of rewrites decides ring equalities by ordered rewriting.*} +lemmas ring_eq_simps = + mult_ac + left_distrib right_distrib left_diff_distrib right_diff_distrib + add_ac + add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2 + diff_eq_eq eq_diff_eq + +thm ring_eq_simps subsection {* Fields *} lemma right_inverse [simp]: @@ -1571,14 +1324,14 @@ subsection {* Ordered Fields are Dense *} -lemma less_add_one: "a < (a+1::'a::ordered_semiring)" +lemma less_add_one: "a < (a+1::'a::ordered_semidom)" proof - - have "a+0 < (a+1::'a::ordered_semiring)" + have "a+0 < (a+1::'a::ordered_semidom)" by (blast intro: zero_less_one add_strict_left_mono) thus ?thesis by simp qed -lemma zero_less_two: "0 < (1+1::'a::ordered_semiring)" +lemma zero_less_two: "0 < (1+1::'a::ordered_semidom)" by (blast intro: order_less_trans zero_less_one less_add_one) lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::ordered_field)" @@ -1590,61 +1343,101 @@ lemma dense: "a < b ==> \r::'a::ordered_field. a < r & r < b" by (blast intro!: less_half_sum gt_half_sum) - subsection {* Absolute Value *} -lemma abs_zero [simp]: "abs 0 = (0::'a::ordered_ring)" -by (simp add: abs_if) - -lemma abs_one [simp]: "abs 1 = (1::'a::ordered_ring)" +lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)" by (simp add: abs_if zero_less_one [THEN order_less_not_sym]) -lemma abs_mult: "abs (a * b) = abs a * abs (b::'a::ordered_ring)" -apply (case_tac "a=0 | b=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_mult_self: "abs a * abs a = a * (a::'a::ordered_ring)" -by (simp add: abs_if) - -lemma abs_eq_0 [simp]: "(abs a = 0) = (a = (0::'a::ordered_ring))" -by (simp add: abs_if) - -lemma zero_less_abs_iff [simp]: "(0 < abs a) = (a \ (0::'a::ordered_ring))" -by (simp add: abs_if linorder_neq_iff) - -lemma abs_not_less_zero [simp]: "~ abs a < (0::'a::ordered_ring)" -apply (simp add: abs_if) -by (simp add: abs_if order_less_not_sym [of a 0]) - -lemma abs_le_zero_iff [simp]: "(abs a \ (0::'a::ordered_ring)) = (a = 0)" -by (simp add: order_le_less) +lemma abs_le_mult: "abs (a * b) \ (abs a) * (abs (b::'a::lordered_ring))" +proof - + let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b" + let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b" + have a: "(abs a) * (abs b) = ?x" + by (simp only: abs_prts[of a] abs_prts[of b] ring_eq_simps) + { + fix u v :: 'a + have bh: "\u = a; v = b\ \ u * v = ?y" + apply (subst prts[of u], subst prts[of v]) + apply (simp add: left_distrib right_distrib add_ac) + done + } + note b = this[OF refl[of a] refl[of b]] + note addm = add_mono[of "0::'a" _ "0::'a", simplified] + note addm2 = add_mono[of _ "0::'a" _ "0::'a", simplified] + have xy: "- ?x <= ?y" + apply (simp add: compare_rls) + apply (rule add_le_imp_le_left[of "-(pprt a * nprt b + nprt a * pprt b)"]) + apply (simp add: add_ac) + proof - + let ?r = "nprt a * nprt b +(nprt a * nprt b + (nprt a * pprt b + (pprt a * nprt b + (pprt a * pprt b + (pprt a * pprt b + + (- (nprt a * pprt b) + - (pprt a * nprt b)))))))" + let ?rr = "nprt a * nprt b + nprt a * nprt b + ((nprt a * pprt b) + (- (nprt a * pprt b))) + ((pprt a * nprt b) + - (pprt a * nprt b)) + + pprt a * pprt b + pprt a * pprt b" + have a:"?r = ?rr" by (simp only: add_ac) + have "0 <= ?rr" + apply (simp) + apply (rule addm)+ + apply (simp_all add: mult_neg_le mult_pos_le) + done + with a show "0 <= ?r" by simp + qed + have yx: "?y <= ?x" + apply (simp add: add_ac) + apply (simp add: compare_rls) + apply (rule add_le_imp_le_right[of _ "-(pprt a * pprt b)"]) + apply (simp add: add_ac) + apply (rule addm2, (simp add: mult_pos_neg_le mult_pos_neg2_le)+)+ + done + have i1: "a*b <= abs a * abs b" by (simp only: a b yx) + have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy) + show ?thesis + apply (rule abs_leI) + apply (simp add: i1) + apply (simp add: i2[simplified minus_le_iff]) + done +qed -lemma abs_minus_cancel [simp]: "abs (-a) = abs(a::'a::ordered_ring)" -apply (auto simp add: abs_if linorder_not_less order_less_not_sym [of 0 a]) -apply (drule order_antisym, assumption, simp) -done - -lemma abs_ge_zero [simp]: "(0::'a::ordered_ring) \ abs a" -apply (simp add: abs_if order_less_imp_le) -apply (simp add: linorder_not_less) -done +lemma abs_eq_mult: + assumes "(0 \ a \ a \ 0) \ (0 \ b \ b \ 0)" + shows "abs (a*b) = abs a * abs (b::'a::lordered_ring)" +proof - + have s: "(0 <= a*b) | (a*b <= 0)" + apply (auto) + apply (rule_tac split_mult_pos_le) + apply (rule_tac contrapos_np[of "a*b <= 0"]) + apply (simp) + apply (rule_tac split_mult_neg_le) + apply (insert prems) + apply (blast) + done + have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)" + by (simp add: prts[symmetric]) + show ?thesis + proof cases + assume "0 <= a * b" + then show ?thesis + apply (simp_all add: mulprts abs_prts) + apply (insert prems) + apply (auto simp add: ring_eq_simps iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt] + iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id] order_antisym mult_pos_neg_le[of a b] mult_pos_neg2_le[of b a]) + done + next + assume "~(0 <= a*b)" + with s have "a*b <= 0" by simp + then show ?thesis + apply (simp_all add: mulprts abs_prts) + apply (insert prems) + apply (auto simp add: ring_eq_simps iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt] + iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id] order_antisym mult_pos_le[of a b] mult_neg_le[of a b]) + done + qed +qed -lemma abs_idempotent [simp]: "abs (abs a) = abs (a::'a::ordered_ring)" - by (force elim: order_less_asym simp add: abs_if) - -lemma abs_zero_iff [simp]: "(abs a = 0) = (a = (0::'a::ordered_ring))" -by (simp add: abs_if) +lemma abs_mult: "abs (a * b) = abs a * abs (b::'a::ordered_idom)" +by (simp add: abs_eq_mult linorder_linear) -lemma abs_ge_self: "a \ abs (a::'a::ordered_ring)" -apply (simp add: abs_if) -apply (simp add: order_less_imp_le order_trans [of _ 0]) -done - -lemma abs_ge_minus_self: "-a \ abs (a::'a::ordered_ring)" -by (insert abs_ge_self [of "-a"], simp) +lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_idom)" +by (simp add: abs_if) lemma nonzero_abs_inverse: "a \ 0 ==> abs (inverse (a::'a::ordered_field)) = inverse (abs a)" @@ -1670,72 +1463,8 @@ apply (simp add: nonzero_abs_divide) done -lemma abs_leI: "[|a \ b; -a \ b|] ==> abs a \ (b::'a::ordered_ring)" -by (simp add: abs_if) - -lemma le_minus_self_iff: "(a \ -a) = (a \ (0::'a::ordered_ring))" -proof - assume ale: "a \ -a" - show "a\0" - apply (rule classical) - apply (simp add: linorder_not_le) - apply (blast intro: ale order_trans order_less_imp_le - neg_0_le_iff_le [THEN iffD1]) - done -next - assume "a\0" - hence "0 \ -a" by (simp only: neg_0_le_iff_le) - thus "a \ -a" by (blast intro: prems order_trans) -qed - -lemma minus_le_self_iff: "(-a \ a) = (0 \ (a::'a::ordered_ring))" -by (insert le_minus_self_iff [of "-a"], simp) - -lemma eq_minus_self_iff: "(a = -a) = (a = (0::'a::ordered_ring))" -by (force simp add: order_eq_iff le_minus_self_iff minus_le_self_iff) - -lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::ordered_ring))" -by (simp add: order_less_le le_minus_self_iff eq_minus_self_iff) - -lemma abs_le_D1: "abs a \ b ==> a \ (b::'a::ordered_ring)" -apply (simp add: abs_if split: split_if_asm) -apply (rule order_trans [of _ "-a"]) - apply (simp add: less_minus_self_iff order_less_imp_le, assumption) -done - -lemma abs_le_D2: "abs a \ b ==> -a \ (b::'a::ordered_ring)" -by (insert abs_le_D1 [of "-a"], simp) - -lemma abs_le_iff: "(abs a \ b) = (a \ b & -a \ (b::'a::ordered_ring))" -by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2) - -lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_ring))" -apply (simp add: order_less_le abs_le_iff) -apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff) -apply (simp add: le_minus_self_iff linorder_neq_iff) -done -(* -apply (simp add: order_less_le abs_le_iff) -apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff) - apply (simp add: linorder_not_less [symmetric]) -apply (simp add: le_minus_self_iff linorder_neq_iff) -apply (simp add: linorder_not_less [symmetric]) -done -*) - -lemma abs_triangle_ineq: "abs (a+b) \ abs a + abs (b::'a::ordered_ring)" -by (force simp add: abs_le_iff abs_ge_self abs_ge_minus_self add_mono) - -lemma abs_diff_triangle_ineq: - "\(a::'a::ordered_ring) + b - (c+d)\ \ \a-c\ + \b-d\" -proof - - have "\a + b - (c+d)\ = \(a-c) + (b-d)\" by (simp add: diff_minus add_ac) - also have "... \ \a-c\ + \b-d\" by (rule abs_triangle_ineq) - finally show ?thesis . -qed - lemma abs_mult_less: - "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::ordered_ring)" + "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::ordered_idom)" proof - assume ac: "abs a < c" hence cpos: "0 ('a::order) multiset)" @@ -80,7 +80,7 @@ (\i: A Int lessThan (length l). {# l!i #})" apply (rule_tac xs = l in rev_induct, simp) apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append - bag_of_sublist_lemma plus_ac0) + bag_of_sublist_lemma add_ac) done diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/arith_data.ML --- a/src/HOL/arith_data.ML Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/arith_data.ML Tue May 11 20:11:08 2004 +0200 @@ -386,10 +386,10 @@ val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s (fn prems => [cut_facts_tac prems 1, blast_tac (claset() addIs [add_mono]) 1])) -["(i <= j) & (k <= l) ==> i + k <= j + (l::'a::ordered_semiring)", - "(i = j) & (k <= l) ==> i + k <= j + (l::'a::ordered_semiring)", - "(i <= j) & (k = l) ==> i + k <= j + (l::'a::ordered_semiring)", - "(i = j) & (k = l) ==> i + k = j + (l::'a::ordered_semiring)" +["(i <= j) & (k <= l) ==> i + k <= j + (l::'a::ordered_semidom)", + "(i = j) & (k <= l) ==> i + k <= j + (l::'a::ordered_semidom)", + "(i <= j) & (k = l) ==> i + k <= j + (l::'a::ordered_semidom)", + "(i = j) & (k = l) ==> i + k = j + (l::'a::ordered_semidom)" ]; in diff -r 77ea79aed99d -r 83f1a514dcb4 src/HOL/ex/Lagrange.thy --- a/src/HOL/ex/Lagrange.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/ex/Lagrange.thy Tue May 11 20:11:08 2004 +0200 @@ -23,7 +23,7 @@ (*once a slow step, but now (2001) just three seconds!*) lemma Lagrange_lemma: - "!!x1::'a::ring. + "!!x1::'a::comm_ring_1. (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = sq(x1*y1 - x2*y2 - x3*y3 - x4*y4) + sq(x1*y2 + x2*y1 + x3*y4 - x4*y3) + @@ -34,7 +34,7 @@ (* A challenge by John Harrison. Takes about 4 mins on a 3GHz machine. -lemma "!!p1::'a::ring. +lemma "!!p1::'a::comm_ring_1. (sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) +