# HG changeset patch # User paulson # Date 1072388912 -3600 # Node ID ff3210fe968fc469d45613e28ae5d83d97d1917f # Parent fd063037fdf5fd4a50802fca077f6fc70f629f92 re-organized some hyperreal and real lemmas diff -r fd063037fdf5 -r ff3210fe968f src/HOL/Hyperreal/HyperArith.thy --- a/src/HOL/Hyperreal/HyperArith.thy Wed Dec 24 08:54:30 2003 +0100 +++ b/src/HOL/Hyperreal/HyperArith.thy Thu Dec 25 22:48:32 2003 +0100 @@ -4,6 +4,16 @@ setup hypreal_arith_setup +text{*Used once in NSA*} +lemma hypreal_add_minus_eq_minus: "x + y = (0::hypreal) ==> x = -y" +apply arith +done + +ML +{* +val hypreal_add_minus_eq_minus = thm "hypreal_add_minus_eq_minus"; +*} + subsubsection{*Division By @{term 1} and @{term "-1"}*} lemma hypreal_divide_minus1 [simp]: "x/-1 = -(x::hypreal)" diff -r fd063037fdf5 -r ff3210fe968f src/HOL/Hyperreal/HyperBin.ML --- a/src/HOL/Hyperreal/HyperBin.ML Wed Dec 24 08:54:30 2003 +0100 +++ b/src/HOL/Hyperreal/HyperBin.ML Thu Dec 25 22:48:32 2003 +0100 @@ -148,21 +148,6 @@ (**** Simprocs for numeric literals ****) -(** Combining of literal coefficients in sums of products **) - -Goal "(x < y) = (x-y < (0::hypreal))"; -by (simp_tac (simpset() addsimps [hypreal_diff_less_eq]) 1); -qed "hypreal_less_iff_diff_less_0"; - -Goal "(x = y) = (x-y = (0::hypreal))"; -by (simp_tac (simpset() addsimps [hypreal_diff_eq_eq]) 1); -qed "hypreal_eq_iff_diff_eq_0"; - -Goal "(x <= y) = (x-y <= (0::hypreal))"; -by (simp_tac (simpset() addsimps [hypreal_diff_le_eq]) 1); -qed "hypreal_le_iff_diff_le_0"; - - (** For combine_numerals **) Goal "i*u + (j*u + k) = (i+j)*u + (k::hypreal)"; @@ -173,12 +158,12 @@ (** For cancel_numerals **) val rel_iff_rel_0_rls = - map (inst "y" "?u+?v") - [hypreal_less_iff_diff_less_0, hypreal_eq_iff_diff_eq_0, - hypreal_le_iff_diff_le_0] @ - map (inst "y" "n") - [hypreal_less_iff_diff_less_0, hypreal_eq_iff_diff_eq_0, - hypreal_le_iff_diff_le_0]; + map (inst "b" "?u+?v") + [less_iff_diff_less_0, eq_iff_diff_eq_0, + le_iff_diff_le_0] @ + map (inst "b" "n") + [less_iff_diff_less_0, eq_iff_diff_eq_0, + le_iff_diff_le_0]; Goal "!!i::hypreal. (i*u + m = j*u + n) = ((i-j)*u + m = n)"; by (asm_simp_tac @@ -582,9 +567,9 @@ Addsimprocs [Hyperreal_Times_Assoc.conv]; (*Simplification of x-y < 0, etc.*) -AddIffs [hypreal_less_iff_diff_less_0 RS sym]; -AddIffs [hypreal_eq_iff_diff_eq_0 RS sym]; -AddIffs [hypreal_le_iff_diff_le_0 RS sym]; +AddIffs [less_iff_diff_less_0 RS sym]; +AddIffs [eq_iff_diff_eq_0 RS sym]; +AddIffs [le_iff_diff_le_0 RS sym]; (** number_of related to hypreal_of_real **) diff -r fd063037fdf5 -r ff3210fe968f src/HOL/Hyperreal/HyperDef.thy --- a/src/HOL/Hyperreal/HyperDef.thy Wed Dec 24 08:54:30 2003 +0100 +++ b/src/HOL/Hyperreal/HyperDef.thy Thu Dec 25 22:48:32 2003 +0100 @@ -84,12 +84,14 @@ hypreal_le_def: "P <= (Q::hypreal) == ~(Q < P)" -(*------------------------------------------------------------------------ - Proof that the set of naturals is not finite - ------------------------------------------------------------------------*) + hrabs_def: "abs (r::hypreal) == (if 0 \ r then r else -r)" + + +subsection{*The Set of Naturals is not Finite*} (*** based on James' proof that the set of naturals is not finite ***) -lemma finite_exhausts [rule_format (no_asm)]: "finite (A::nat set) --> (\n. \m. Suc (n + m) \ A)" +lemma finite_exhausts [rule_format]: + "finite (A::nat set) --> (\n. \m. Suc (n + m) \ A)" apply (rule impI) apply (erule_tac F = A in finite_induct) apply (blast, erule exE) @@ -98,16 +100,18 @@ apply (auto simp add: add_ac) done -lemma finite_not_covers [rule_format (no_asm)]: "finite (A :: nat set) --> (\n. n \A)" +lemma finite_not_covers [rule_format (no_asm)]: + "finite (A :: nat set) --> (\n. n \A)" by (rule impI, drule finite_exhausts, blast) lemma not_finite_nat: "~ finite(UNIV:: nat set)" by (fast dest!: finite_exhausts) -(*------------------------------------------------------------------------ - Existence of free ultrafilter over the naturals and proof of various - properties of the FreeUltrafilterNat- an arbitrary free ultrafilter - ------------------------------------------------------------------------*) + +subsection{*Existence of Free Ultrafilter over the Naturals*} + +text{*Also, proof of various properties of @{term FreeUltrafilterNat}: +an arbitrary free ultrafilter*} lemma FreeUltrafilterNat_Ex: "\U. U: FreeUltrafilter (UNIV::nat set)" by (rule not_finite_nat [THEN FreeUltrafilter_Ex]) @@ -137,33 +141,39 @@ Filter_empty_not_mem) done -lemma FreeUltrafilterNat_Int: "[| X: FreeUltrafilterNat; Y: FreeUltrafilterNat |] +lemma FreeUltrafilterNat_Int: + "[| X: FreeUltrafilterNat; Y: FreeUltrafilterNat |] ==> X Int Y \ FreeUltrafilterNat" apply (cut_tac FreeUltrafilterNat_mem) apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter mem_FiltersetD1) done -lemma FreeUltrafilterNat_subset: "[| X: FreeUltrafilterNat; X <= Y |] +lemma FreeUltrafilterNat_subset: + "[| X: FreeUltrafilterNat; X <= Y |] ==> Y \ FreeUltrafilterNat" apply (cut_tac FreeUltrafilterNat_mem) apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter mem_FiltersetD2) done -lemma FreeUltrafilterNat_Compl: "X: FreeUltrafilterNat ==> -X \ FreeUltrafilterNat" +lemma FreeUltrafilterNat_Compl: + "X: FreeUltrafilterNat ==> -X \ FreeUltrafilterNat" apply safe apply (drule FreeUltrafilterNat_Int, assumption, auto) done -lemma FreeUltrafilterNat_Compl_mem: "X\ FreeUltrafilterNat ==> -X \ FreeUltrafilterNat" +lemma FreeUltrafilterNat_Compl_mem: + "X\ FreeUltrafilterNat ==> -X \ FreeUltrafilterNat" apply (cut_tac FreeUltrafilterNat_mem [THEN FreeUltrafilter_iff [THEN iffD1]]) apply (safe, drule_tac x = X in bspec) apply (auto simp add: UNIV_diff_Compl) done -lemma FreeUltrafilterNat_Compl_iff1: "(X \ FreeUltrafilterNat) = (-X: FreeUltrafilterNat)" +lemma FreeUltrafilterNat_Compl_iff1: + "(X \ FreeUltrafilterNat) = (-X: FreeUltrafilterNat)" by (blast dest: FreeUltrafilterNat_Compl FreeUltrafilterNat_Compl_mem) -lemma FreeUltrafilterNat_Compl_iff2: "(X: FreeUltrafilterNat) = (-X \ FreeUltrafilterNat)" +lemma FreeUltrafilterNat_Compl_iff2: + "(X: FreeUltrafilterNat) = (-X \ FreeUltrafilterNat)" by (auto simp add: FreeUltrafilterNat_Compl_iff1 [symmetric]) lemma FreeUltrafilterNat_UNIV [simp]: "(UNIV::nat set) \ FreeUltrafilterNat" @@ -172,7 +182,8 @@ lemma FreeUltrafilterNat_Nat_set [simp]: "UNIV \ FreeUltrafilterNat" by auto -lemma FreeUltrafilterNat_Nat_set_refl [intro]: "{n. P(n) = P(n)} \ FreeUltrafilterNat" +lemma FreeUltrafilterNat_Nat_set_refl [intro]: + "{n. P(n) = P(n)} \ FreeUltrafilterNat" by simp lemma FreeUltrafilterNat_P: "{n::nat. P} \ FreeUltrafilterNat ==> P" @@ -184,9 +195,8 @@ lemma FreeUltrafilterNat_all: "\n. P(n) ==> {n. P(n)} \ FreeUltrafilterNat" by (auto intro: FreeUltrafilterNat_Nat_set) -(*------------------------------------------------------- - Define and use Ultrafilter tactics - -------------------------------------------------------*) + +text{*Define and use Ultrafilter tactics*} use "fuf.ML" method_setup fuf = {* @@ -204,21 +214,18 @@ "ultrafilter tactic" -(*------------------------------------------------------- - Now prove one further property of our free ultrafilter - -------------------------------------------------------*) -lemma FreeUltrafilterNat_Un: "X Un Y: FreeUltrafilterNat +text{*One further property of our free ultrafilter*} +lemma FreeUltrafilterNat_Un: + "X Un Y: FreeUltrafilterNat ==> X: FreeUltrafilterNat | Y: FreeUltrafilterNat" apply auto apply ultra done -(*------------------------------------------------------- - Properties of hyprel - -------------------------------------------------------*) -(** Proving that hyprel is an equivalence relation **) -(** Natural deduction for hyprel **) +subsection{*Properties of @{term hyprel}*} + +text{*Proving that @{term hyprel} is an equivalence relation*} lemma hyprel_iff: "((X,Y): hyprel) = ({n. X n = Y n}: FreeUltrafilterNat)" by (unfold hyprel_def, fast) @@ -281,9 +288,8 @@ by (cut_tac x = x in Rep_hypreal, auto) -(*------------------------------------------------------------------------ - hypreal_of_real: the injection from real to hypreal - ------------------------------------------------------------------------*) +subsection{*@{term hypreal_of_real}: + the Injection from @{typ real} to @{typ hypreal}*} lemma inj_hypreal_of_real: "inj(hypreal_of_real)" apply (rule inj_onI) @@ -302,7 +308,61 @@ apply (force simp add: Rep_hypreal_inverse) done -(**** hypreal_minus: additive inverse on hypreal ****) + +subsection{*Hyperreal Addition*} + +lemma hypreal_add_congruent2: + "congruent2 hyprel (%X Y. hyprel``{%n. X n + Y n})" +apply (unfold congruent2_def, auto, ultra) +done + +lemma hypreal_add: + "Abs_hypreal(hyprel``{%n. X n}) + Abs_hypreal(hyprel``{%n. Y n}) = + Abs_hypreal(hyprel``{%n. X n + Y n})" +apply (unfold hypreal_add_def) +apply (simp add: UN_equiv_class2 [OF equiv_hyprel hypreal_add_congruent2]) +done + +lemma hypreal_add_commute: "(z::hypreal) + w = w + z" +apply (rule_tac z = z in eq_Abs_hypreal) +apply (rule_tac z = w in eq_Abs_hypreal) +apply (simp add: real_add_ac hypreal_add) +done + +lemma hypreal_add_assoc: "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)" +apply (rule_tac z = z1 in eq_Abs_hypreal) +apply (rule_tac z = z2 in eq_Abs_hypreal) +apply (rule_tac z = z3 in eq_Abs_hypreal) +apply (simp add: hypreal_add real_add_assoc) +done + +(*For AC rewriting*) +lemma hypreal_add_left_commute: "(x::hypreal)+(y+z)=y+(x+z)" + apply (rule mk_left_commute [of "op +"]) + apply (rule hypreal_add_assoc) + apply (rule hypreal_add_commute) + done + +(* hypreal addition is an AC operator *) +lemmas hypreal_add_ac = + hypreal_add_assoc hypreal_add_commute hypreal_add_left_commute + +lemma hypreal_add_zero_left [simp]: "(0::hypreal) + z = z" +apply (unfold hypreal_zero_def) +apply (rule_tac z = z in eq_Abs_hypreal) +apply (simp add: hypreal_add) +done + +instance hypreal :: plus_ac0 + by (intro_classes, + (assumption | + rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+) + +lemma hypreal_add_zero_right [simp]: "z + (0::hypreal) = z" +by (simp add: hypreal_add_zero_left hypreal_add_commute) + + +subsection{*Additive inverse on @{typ hypreal}*} lemma hypreal_minus_congruent: "congruent hyprel (%X. hyprel``{%n. - (X n)})" @@ -337,59 +397,12 @@ apply (auto simp add: hypreal_zero_def hypreal_minus) done - -(**** hyperreal addition: hypreal_add ****) - -lemma hypreal_add_congruent2: - "congruent2 hyprel (%X Y. hyprel``{%n. X n + Y n})" -apply (unfold congruent2_def, auto, ultra) -done - -lemma hypreal_add: - "Abs_hypreal(hyprel``{%n. X n}) + Abs_hypreal(hyprel``{%n. Y n}) = - Abs_hypreal(hyprel``{%n. X n + Y n})" -apply (unfold hypreal_add_def) -apply (simp add: UN_equiv_class2 [OF equiv_hyprel hypreal_add_congruent2]) -done - -lemma hypreal_diff: "Abs_hypreal(hyprel``{%n. X n}) - Abs_hypreal(hyprel``{%n. Y n}) = +lemma hypreal_diff: + "Abs_hypreal(hyprel``{%n. X n}) - Abs_hypreal(hyprel``{%n. Y n}) = Abs_hypreal(hyprel``{%n. X n - Y n})" apply (simp add: hypreal_diff_def hypreal_minus hypreal_add) done -lemma hypreal_add_commute: "(z::hypreal) + w = w + z" -apply (rule_tac z = z in eq_Abs_hypreal) -apply (rule_tac z = w in eq_Abs_hypreal) -apply (simp add: real_add_ac hypreal_add) -done - -lemma hypreal_add_assoc: "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)" -apply (rule_tac z = z1 in eq_Abs_hypreal) -apply (rule_tac z = z2 in eq_Abs_hypreal) -apply (rule_tac z = z3 in eq_Abs_hypreal) -apply (simp add: hypreal_add real_add_assoc) -done - -(*For AC rewriting*) -lemma hypreal_add_left_commute: "(x::hypreal)+(y+z)=y+(x+z)" - apply (rule mk_left_commute [of "op +"]) - apply (rule hypreal_add_assoc) - apply (rule hypreal_add_commute) - done - -(* hypreal addition is an AC operator *) -lemmas hypreal_add_ac = - hypreal_add_assoc hypreal_add_commute hypreal_add_left_commute - -lemma hypreal_add_zero_left [simp]: "(0::hypreal) + z = z" -apply (unfold hypreal_zero_def) -apply (rule_tac z = z in eq_Abs_hypreal) -apply (simp add: hypreal_add) -done - -lemma hypreal_add_zero_right [simp]: "z + (0::hypreal) = z" -by (simp add: hypreal_add_zero_left hypreal_add_commute) - lemma hypreal_add_minus [simp]: "z + -z = (0::hypreal)" apply (unfold hypreal_zero_def) apply (rule_tac z = z in eq_Abs_hypreal) @@ -399,42 +412,6 @@ lemma hypreal_add_minus_left [simp]: "-z + z = (0::hypreal)" by (simp add: hypreal_add_commute hypreal_add_minus) -lemma hypreal_minus_ex: "\y. (x::hypreal) + y = 0" -by (fast intro: hypreal_add_minus) - -lemma hypreal_minus_ex1: "EX! y. (x::hypreal) + y = 0" -apply (auto intro: hypreal_add_minus) -apply (drule_tac f = "%x. ya+x" in arg_cong) -apply (simp add: hypreal_add_assoc [symmetric]) -apply (simp add: hypreal_add_commute) -done - -lemma hypreal_minus_left_ex1: "EX! y. y + (x::hypreal) = 0" -apply (auto intro: hypreal_add_minus_left) -apply (drule_tac f = "%x. x+ya" in arg_cong) -apply (simp add: hypreal_add_assoc) -apply (simp add: hypreal_add_commute) -done - -lemma hypreal_add_minus_eq_minus: "x + y = (0::hypreal) ==> x = -y" -apply (cut_tac z = y in hypreal_add_minus_left) -apply (rule_tac x1 = y in hypreal_minus_left_ex1 [THEN ex1E], blast) -done - -lemma hypreal_as_add_inverse_ex: "\y::hypreal. x = -y" -apply (cut_tac x = x in hypreal_minus_ex) -apply (erule exE, drule hypreal_add_minus_eq_minus, fast) -done - -lemma hypreal_minus_add_distrib [simp]: "-(x + (y::hypreal)) = -x + -y" -apply (rule_tac z = x in eq_Abs_hypreal) -apply (rule_tac z = y in eq_Abs_hypreal) -apply (auto simp add: hypreal_minus hypreal_add real_minus_add_distrib) -done - -lemma hypreal_minus_distrib1: "-(y + -(x::hypreal)) = x + -y" -by (simp add: hypreal_add_commute) - lemma hypreal_add_left_cancel: "((x::hypreal) + y = x + z) = (y = z)" apply safe apply (drule_tac f = "%t.-x + t" in arg_cong) @@ -450,7 +427,8 @@ lemma hypreal_minus_add_cancelA [simp]: "(-z) + (z + w) = (w::hypreal)" by (simp add: hypreal_add_assoc [symmetric]) -(**** hyperreal multiplication: hypreal_mult ****) + +subsection{*Hyperreal Multiplication*} lemma hypreal_mult_congruent2: "congruent2 hyprel (%X Y. hyprel``{%n. X n * Y n})" @@ -530,30 +508,30 @@ lemma hypreal_minus_mult_commute: "(-x) * y = (x::hypreal) * -y" by auto -(*----------------------------------------------------------------------------- - A few more theorems - ----------------------------------------------------------------------------*) -lemma hypreal_add_assoc_cong: "(z::hypreal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)" -by (simp add: hypreal_add_assoc [symmetric]) +subsection{*A few more theorems *} -lemma hypreal_add_mult_distrib: "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)" +lemma hypreal_add_mult_distrib: + "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)" apply (rule_tac z = z1 in eq_Abs_hypreal) apply (rule_tac z = z2 in eq_Abs_hypreal) apply (rule_tac z = w in eq_Abs_hypreal) apply (simp add: hypreal_mult hypreal_add real_add_mult_distrib) done -lemma hypreal_add_mult_distrib2: "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)" +lemma hypreal_add_mult_distrib2: + "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)" by (simp add: hypreal_mult_commute [of w] hypreal_add_mult_distrib) -lemma hypreal_diff_mult_distrib: "((z1::hypreal) - z2) * w = (z1 * w) - (z2 * w)" +lemma hypreal_diff_mult_distrib: + "((z1::hypreal) - z2) * w = (z1 * w) - (z2 * w)" apply (unfold hypreal_diff_def) apply (simp add: hypreal_add_mult_distrib) done -lemma hypreal_diff_mult_distrib2: "(w::hypreal) * (z1 - z2) = (w * z1) - (w * z2)" +lemma hypreal_diff_mult_distrib2: + "(w::hypreal) * (z1 - z2) = (w * z1) - (w * z2)" by (simp add: hypreal_mult_commute [of w] hypreal_diff_mult_distrib) (*** one and zero are distinct ***) @@ -563,7 +541,7 @@ done -(**** multiplicative inverse on hypreal ****) +subsection{*Multiplicative Inverse on @{typ hypreal} *} lemma hypreal_inverse_congruent: "congruent hyprel (%X. hyprel``{%n. if X n = 0 then 0 else inverse(X n)})" @@ -586,19 +564,15 @@ lemma HYPREAL_DIVISION_BY_ZERO: "a / (0::hypreal) = 0" by (simp add: hypreal_divide_def HYPREAL_INVERSE_ZERO) -lemma hypreal_inverse_inverse [simp]: "inverse (inverse (z::hypreal)) = z" -apply (case_tac "z=0", simp add: HYPREAL_INVERSE_ZERO) -apply (rule_tac z = z in eq_Abs_hypreal) -apply (simp add: hypreal_inverse hypreal_zero_def) -done - -lemma hypreal_inverse_1 [simp]: "inverse((1::hypreal)) = (1::hypreal)" -apply (unfold hypreal_one_def) -apply (simp add: hypreal_inverse real_zero_not_eq_one [THEN not_sym]) -done +instance hypreal :: division_by_zero +proof + fix x :: hypreal + show "inverse 0 = (0::hypreal)" by (rule HYPREAL_INVERSE_ZERO) + show "x/0 = 0" by (rule HYPREAL_DIVISION_BY_ZERO) +qed -(*** existence of inverse ***) +subsection{*Existence of Inverse*} lemma hypreal_mult_inverse [simp]: "x \ 0 ==> x*inverse(x) = (1::hypreal)" @@ -609,99 +583,33 @@ apply (blast intro!: real_mult_inv_right FreeUltrafilterNat_subset) done -lemma hypreal_mult_inverse_left [simp]: "x \ 0 ==> inverse(x)*x = (1::hypreal)" +lemma hypreal_mult_inverse_left [simp]: + "x \ 0 ==> inverse(x)*x = (1::hypreal)" by (simp add: hypreal_mult_inverse hypreal_mult_commute) -lemma hypreal_mult_left_cancel: "(c::hypreal) \ 0 ==> (c*a=c*b) = (a=b)" -apply auto -apply (drule_tac f = "%x. x*inverse c" in arg_cong) -apply (simp add: hypreal_mult_inverse hypreal_mult_ac) -done - -lemma hypreal_mult_right_cancel: "(c::hypreal) \ 0 ==> (a*c=b*c) = (a=b)" -apply safe -apply (drule_tac f = "%x. x*inverse c" in arg_cong) -apply (simp add: hypreal_mult_inverse hypreal_mult_ac) -done + +subsection{*Theorems for Ordering*} + +text{*TODO: define @{text "\"} as the primitive concept and quickly +establish membership in class @{text linorder}. Then proofs could be +simplified, since properties of @{text "<"} would be generic.*} -lemma hypreal_inverse_not_zero: "x \ 0 ==> inverse (x::hypreal) \ 0" -apply (unfold hypreal_zero_def) -apply (rule_tac z = x in eq_Abs_hypreal) -apply (simp add: hypreal_inverse hypreal_mult) -done - - -lemma hypreal_mult_not_0: "[| x \ 0; y \ 0 |] ==> x * y \ (0::hypreal)" -apply safe -apply (drule_tac f = "%z. inverse x*z" in arg_cong) -apply (simp add: hypreal_mult_assoc [symmetric]) -done - -lemma hypreal_mult_zero_disj: "x*y = (0::hypreal) ==> x = 0 | y = 0" -by (auto intro: ccontr dest: hypreal_mult_not_0) - -lemma hypreal_minus_inverse: "inverse(-x) = -inverse(x::hypreal)" -apply (case_tac "x=0", simp add: HYPREAL_INVERSE_ZERO) -apply (rule hypreal_mult_right_cancel [of "-x", THEN iffD1], simp) -apply (subst hypreal_mult_inverse_left, auto) +text{*TODO: The following theorem should be used througout the proofs + as it probably makes many of them more straightforward.*} +lemma hypreal_less: + "(Abs_hypreal(hyprel``{%n. X n}) < Abs_hypreal(hyprel``{%n. Y n})) = + ({n. X n < Y n} \ FreeUltrafilterNat)" +apply (unfold hypreal_less_def) +apply (auto intro!: lemma_hyprel_refl, ultra) done -lemma hypreal_inverse_distrib: "inverse(x*y) = inverse(x)*inverse(y::hypreal)" -apply (case_tac "x=0", simp add: HYPREAL_INVERSE_ZERO) -apply (case_tac "y=0", simp add: HYPREAL_INVERSE_ZERO) -apply (frule_tac y = y in hypreal_mult_not_0, assumption) -apply (rule_tac c1 = x in hypreal_mult_left_cancel [THEN iffD1]) -apply (auto simp add: hypreal_mult_assoc [symmetric]) -apply (rule_tac c1 = y in hypreal_mult_left_cancel [THEN iffD1]) -apply (auto simp add: hypreal_mult_left_commute) -apply (simp add: hypreal_mult_assoc [symmetric]) -done - -(*------------------------------------------------------------------ - Theorems for ordering - ------------------------------------------------------------------*) - (* prove introduction and elimination rules for hypreal_less *) -lemma hypreal_less_iff: - "(P < (Q::hypreal)) = (\X Y. X \ Rep_hypreal(P) & - Y \ Rep_hypreal(Q) & - {n. X n < Y n} \ FreeUltrafilterNat)" - -apply (unfold hypreal_less_def, fast) -done - -lemma hypreal_lessI: - "[| {n. X n < Y n} \ FreeUltrafilterNat; - X \ Rep_hypreal(P); - Y \ Rep_hypreal(Q) |] ==> P < (Q::hypreal)" -apply (unfold hypreal_less_def, fast) -done - - -lemma hypreal_lessE: - "!! R1. [| R1 < (R2::hypreal); - !!X Y. {n. X n < Y n} \ FreeUltrafilterNat ==> P; - !!X. X \ Rep_hypreal(R1) ==> P; - !!Y. Y \ Rep_hypreal(R2) ==> P |] - ==> P" - -apply (unfold hypreal_less_def, auto) -done - -lemma hypreal_lessD: - "R1 < (R2::hypreal) ==> (\X Y. {n. X n < Y n} \ FreeUltrafilterNat & - X \ Rep_hypreal(R1) & - Y \ Rep_hypreal(R2))" -apply (unfold hypreal_less_def, fast) -done - lemma hypreal_less_not_refl: "~ (R::hypreal) < R" apply (rule_tac z = R in eq_Abs_hypreal) apply (auto simp add: hypreal_less_def, ultra) done -(*** y < y ==> P ***) lemmas hypreal_less_irrefl = hypreal_less_not_refl [THEN notE, standard] declare hypreal_less_irrefl [elim!] @@ -720,25 +628,10 @@ apply (simp add: hypreal_less_not_refl) done -(*------------------------------------------------------- - TODO: The following theorem should have been proved - first and then used througout the proofs as it probably - makes many of them more straightforward. - -------------------------------------------------------*) -lemma hypreal_less: - "(Abs_hypreal(hyprel``{%n. X n}) < - Abs_hypreal(hyprel``{%n. Y n})) = - ({n. X n < Y n} \ FreeUltrafilterNat)" -apply (unfold hypreal_less_def) -apply (auto intro!: lemma_hyprel_refl, ultra) -done -(*---------------------------------------------------------------------------- - Trichotomy: the hyperreals are linearly ordered - ---------------------------------------------------------------------------*) +subsection{*Trichotomy: the hyperreals are Linearly Ordered*} lemma lemma_hyprel_0_mem: "\x. x: hyprel `` {%n. 0}" - apply (unfold hyprel_def) apply (rule_tac x = "%n. 0" in exI, safe) apply (auto intro!: FreeUltrafilterNat_Nat_set) @@ -763,9 +656,7 @@ apply (insert hypreal_trichotomy [of x], blast) done -(*---------------------------------------------------------------------------- - More properties of < - ----------------------------------------------------------------------------*) +subsection{*More properties of Less Than*} lemma hypreal_less_minus_iff: "((x::hypreal) < y) = (0 < y + -x)" apply (rule_tac z = x in eq_Abs_hypreal) @@ -789,24 +680,8 @@ apply (rule_tac x1 = "-x" in hypreal_add_right_cancel [THEN iffD1], auto) done -(* 07/00 *) -lemma hypreal_diff_zero [simp]: "(0::hypreal) - x = -x" -by (simp add: hypreal_diff_def) -lemma hypreal_diff_zero_right [simp]: "x - (0::hypreal) = x" -by (simp add: hypreal_diff_def) - -lemma hypreal_diff_self [simp]: "x - x = (0::hypreal)" -by (simp add: hypreal_diff_def) - -lemma hypreal_eq_minus_iff3: "(x = y + z) = (x + -z = (y::hypreal))" -by (auto simp add: hypreal_add_assoc) - -lemma hypreal_not_eq_minus_iff: "(x \ a) = (x + -a \ (0::hypreal))" -by (auto dest: hypreal_eq_minus_iff [THEN iffD2]) - - -(*** linearity ***) +subsection{*Linearity*} lemma hypreal_linear: "(x::hypreal) < y | x = y | y < x" apply (subst hypreal_eq_minus_iff2) @@ -823,10 +698,8 @@ apply (cut_tac x = x and y = y in hypreal_linear, auto) done -(*------------------------------------------------------------------------------ - Properties of <= - ------------------------------------------------------------------------------*) -(*------ hypreal le iff reals le a.e ------*) + +subsection{*Properties of The @{text "\"} Relation*} lemma hypreal_le: "(Abs_hypreal(hyprel``{%n. X n}) <= @@ -837,8 +710,6 @@ apply (ultra+) done -(*---------------------------------------------------------*) -(*---------------------------------------------------------*) lemma hypreal_leI: "~(w < z) ==> z <= (w::hypreal)" apply (unfold hypreal_le_def, assumption) @@ -894,17 +765,21 @@ apply (fast elim: hypreal_less_irrefl hypreal_less_asym) done -lemma not_less_not_eq_hypreal_less: "[| ~ y < x; y \ x |] ==> x < (y::hypreal)" -apply (rule not_hypreal_leE) -apply (fast dest: hypreal_le_imp_less_or_eq) -done - (* Axiom 'order_less_le' of class 'order': *) lemma hypreal_less_le: "((w::hypreal) < z) = (w <= z & w \ z)" apply (simp add: hypreal_le_def hypreal_neq_iff) apply (blast intro: hypreal_less_asym) done +instance hypreal :: order + by (intro_classes, + (assumption | + rule hypreal_le_refl hypreal_le_trans hypreal_le_anti_sym + hypreal_less_le)+) + +instance hypreal :: linorder + by (intro_classes, rule hypreal_le_linear) + lemma hypreal_minus_zero_less_iff [simp]: "(0 < -R) = (R < (0::hypreal))" apply (rule_tac z = R in eq_Abs_hypreal) apply (auto simp add: hypreal_zero_def hypreal_less hypreal_minus) @@ -925,9 +800,141 @@ apply (simp add: hypreal_minus_zero_less_iff2) done -(*---------------------------------------------------------- - hypreal_of_real preserves field and order properties - -----------------------------------------------------------*) + +lemma hypreal_self_eq_minus_self_zero: "x = -x ==> x = (0::hypreal)" +apply (rule_tac z = x in eq_Abs_hypreal) +apply (auto simp add: hypreal_minus hypreal_zero_def, ultra) +done + +lemma hypreal_add_self_zero_cancel [simp]: "(x + x = 0) = (x = (0::hypreal))" +apply (rule_tac z = x in eq_Abs_hypreal) +apply (auto simp add: hypreal_add hypreal_zero_def) +done + +lemma hypreal_add_self_zero_cancel2 [simp]: + "(x + x + y = y) = (x = (0::hypreal))" +apply auto +apply (drule hypreal_eq_minus_iff [THEN iffD1]) +apply (auto simp add: hypreal_add_assoc hypreal_self_eq_minus_self_zero) +done + +lemma hypreal_minus_eq_swap: "(b = -a) = (-b = (a::hypreal))" +by auto + +lemma hypreal_minus_eq_cancel [simp]: "(-b = -a) = (b = (a::hypreal))" +by (simp add: hypreal_minus_eq_swap) + +lemma hypreal_add_less_mono1: "(A::hypreal) < B ==> A + C < B + C" +apply (rule_tac z = A in eq_Abs_hypreal) +apply (rule_tac z = B in eq_Abs_hypreal) +apply (rule_tac z = C in eq_Abs_hypreal) +apply (auto intro!: exI simp add: hypreal_less_def hypreal_add, ultra) +done + +lemma hypreal_mult_order: "[| 0 < x; 0 < y |] ==> (0::hypreal) < x * y" +apply (unfold hypreal_zero_def) +apply (rule_tac z = x in eq_Abs_hypreal) +apply (rule_tac z = y in eq_Abs_hypreal) +apply (auto intro!: exI simp add: hypreal_less_def hypreal_mult, ultra) +apply (auto intro: real_mult_order) +done + +lemma hypreal_add_left_le_mono1: "(q1::hypreal) \ q2 ==> x + q1 \ x + q2" +apply (drule order_le_imp_less_or_eq) +apply (auto intro: order_less_imp_le hypreal_add_less_mono1 simp add: hypreal_add_commute) +done + +lemma hypreal_mult_less_mono1: "[| (0::hypreal) < z; x < y |] ==> x*z < y*z" +apply (rotate_tac 1) +apply (drule hypreal_less_minus_iff [THEN iffD1]) +apply (rule hypreal_less_minus_iff [THEN iffD2]) +apply (drule hypreal_mult_order, assumption) +apply (simp add: hypreal_add_mult_distrib2 hypreal_mult_commute) +done + +lemma hypreal_mult_less_mono2: "[| (0::hypreal) z*x (1::hypreal)" by (rule hypreal_zero_not_eq_one) + show "x \ y ==> z + x \ z + y" by (rule hypreal_add_left_le_mono1) + show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: hypreal_mult_less_mono2) + show "\x\ = (if x < 0 then -x else x)" + by (auto dest: order_le_less_trans simp add: hrabs_def linorder_not_le) + show "x \ 0 ==> inverse x * x = 1" by simp + show "y \ 0 ==> x / y = x * inverse y" by (simp add: hypreal_divide_def) +qed + +lemma hypreal_minus_add_distrib [simp]: "-(x + (y::hypreal)) = -x + -y" + by (rule Ring_and_Field.minus_add_distrib) + +(*Used ONCE: in NSA.ML*) +lemma hypreal_minus_distrib1: "-(y + -(x::hypreal)) = x + -y" +by (simp add: hypreal_add_commute) + +(*Used ONCE: in Lim.ML*) +lemma hypreal_eq_minus_iff3: "(x = y + z) = (x + -z = (y::hypreal))" +by (auto simp add: hypreal_add_assoc) + +lemma hypreal_not_eq_minus_iff: "(x \ a) = (x + -a \ (0::hypreal))" +by (auto dest: hypreal_eq_minus_iff [THEN iffD2]) + +lemma hypreal_mult_left_cancel: "(c::hypreal) \ 0 ==> (c*a=c*b) = (a=b)" +apply auto +done + +lemma hypreal_mult_right_cancel: "(c::hypreal) \ 0 ==> (a*c=b*c) = (a=b)" +apply auto +done + +lemma hypreal_inverse_not_zero: "x \ 0 ==> inverse (x::hypreal) \ 0" + by (rule Ring_and_Field.nonzero_imp_inverse_nonzero) + +lemma hypreal_mult_not_0: "[| x \ 0; y \ 0 |] ==> x * y \ (0::hypreal)" +by simp + +lemma hypreal_minus_inverse: "inverse(-x) = -inverse(x::hypreal)" + by (rule Ring_and_Field.inverse_minus_eq) + +lemma hypreal_inverse_distrib: "inverse(x*y) = inverse(x)*inverse(y::hypreal)" + by (rule Ring_and_Field.inverse_mult_distrib) + + +subsection{* Division lemmas *} + +lemma hypreal_divide_one: "x/(1::hypreal) = x" +by (simp add: hypreal_divide_def) + + +(** As with multiplication, pull minus signs OUT of the / operator **) + +lemma hypreal_add_divide_distrib: "(x+y)/(z::hypreal) = x/z + y/z" + by (rule Ring_and_Field.add_divide_distrib) + +lemma hypreal_inverse_add: + "[|(x::hypreal) \ 0; y \ 0 |] + ==> inverse(x) + inverse(y) = (x + y)*inverse(x*y)" +by (simp add: Ring_and_Field.inverse_add mult_assoc) + + +subsection{*@{term hypreal_of_real} Preserves Field and Order Properties*} + lemma hypreal_of_real_add [simp]: "hypreal_of_real (z1 + z2) = hypreal_of_real z1 + hypreal_of_real z2" apply (unfold hypreal_of_real_def) @@ -953,10 +960,12 @@ apply (unfold hypreal_le_def real_le_def, auto) done -lemma hypreal_of_real_eq_iff [simp]: "(hypreal_of_real z1 = hypreal_of_real z2) = (z1 = z2)" +lemma hypreal_of_real_eq_iff [simp]: + "(hypreal_of_real z1 = hypreal_of_real z2) = (z1 = z2)" by (force intro: order_antisym hypreal_of_real_le_iff [THEN iffD1]) -lemma hypreal_of_real_minus [simp]: "hypreal_of_real (-r) = - hypreal_of_real r" +lemma hypreal_of_real_minus [simp]: + "hypreal_of_real (-r) = - hypreal_of_real r" apply (unfold hypreal_of_real_def) apply (auto simp add: hypreal_minus) done @@ -970,146 +979,20 @@ lemma hypreal_of_real_zero_iff: "(hypreal_of_real r = 0) = (r = 0)" by (auto intro: FreeUltrafilterNat_P simp add: hypreal_of_real_def hypreal_zero_def FreeUltrafilterNat_Nat_set) -lemma hypreal_of_real_inverse [simp]: "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)" +lemma hypreal_of_real_inverse [simp]: + "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)" apply (case_tac "r=0") apply (simp add: DIVISION_BY_ZERO INVERSE_ZERO HYPREAL_INVERSE_ZERO) apply (rule_tac c1 = "hypreal_of_real r" in hypreal_mult_left_cancel [THEN iffD1]) apply (auto simp add: hypreal_of_real_zero_iff hypreal_of_real_mult [symmetric]) done -lemma hypreal_of_real_divide [simp]: "hypreal_of_real (z1 / z2) = hypreal_of_real z1 / hypreal_of_real z2" +lemma hypreal_of_real_divide [simp]: + "hypreal_of_real (z1 / z2) = hypreal_of_real z1 / hypreal_of_real z2" by (simp add: hypreal_divide_def real_divide_def) -(*** Division lemmas ***) - -lemma hypreal_zero_divide: "(0::hypreal)/x = 0" -by (simp add: hypreal_divide_def) - -lemma hypreal_divide_one: "x/(1::hypreal) = x" -by (simp add: hypreal_divide_def) -declare hypreal_zero_divide [simp] hypreal_divide_one [simp] - -lemma hypreal_divide_divide1_eq [simp]: "(x::hypreal) / (y/z) = (x*z)/y" -by (simp add: hypreal_divide_def hypreal_inverse_distrib hypreal_mult_ac) - -lemma hypreal_divide_divide2_eq [simp]: "((x::hypreal) / y) / z = x/(y*z)" -by (simp add: hypreal_divide_def hypreal_inverse_distrib hypreal_mult_assoc) - - -(** As with multiplication, pull minus signs OUT of the / operator **) - -lemma hypreal_minus_divide_eq [simp]: "(-x) / (y::hypreal) = - (x/y)" -by (simp add: hypreal_divide_def) - -lemma hypreal_divide_minus_eq [simp]: "(x / -(y::hypreal)) = - (x/y)" -by (simp add: hypreal_divide_def hypreal_minus_inverse) - -lemma hypreal_add_divide_distrib: "(x+y)/(z::hypreal) = x/z + y/z" -by (simp add: hypreal_divide_def hypreal_add_mult_distrib) - -lemma hypreal_inverse_add: "[|(x::hypreal) \ 0; y \ 0 |] - ==> inverse(x) + inverse(y) = (x + y)*inverse(x*y)" -apply (simp add: hypreal_inverse_distrib hypreal_add_mult_distrib hypreal_mult_assoc [symmetric]) -apply (subst hypreal_mult_assoc) -apply (rule hypreal_mult_left_commute [THEN subst]) -apply (simp add: hypreal_add_commute) -done - -lemma hypreal_self_eq_minus_self_zero: "x = -x ==> x = (0::hypreal)" -apply (rule_tac z = x in eq_Abs_hypreal) -apply (auto simp add: hypreal_minus hypreal_zero_def, ultra) -done - -lemma hypreal_add_self_zero_cancel [simp]: "(x + x = 0) = (x = (0::hypreal))" -apply (rule_tac z = x in eq_Abs_hypreal) -apply (auto simp add: hypreal_add hypreal_zero_def) -done - -lemma hypreal_add_self_zero_cancel2 [simp]: "(x + x + y = y) = (x = (0::hypreal))" -apply auto -apply (drule hypreal_eq_minus_iff [THEN iffD1]) -apply (auto simp add: hypreal_add_assoc hypreal_self_eq_minus_self_zero) -done - -lemma hypreal_add_self_zero_cancel2a [simp]: "(x + (x + y) = y) = (x = (0::hypreal))" -by (simp add: hypreal_add_assoc [symmetric]) - -lemma hypreal_minus_eq_swap: "(b = -a) = (-b = (a::hypreal))" -by auto - -lemma hypreal_minus_eq_cancel [simp]: "(-b = -a) = (b = (a::hypreal))" -by (simp add: hypreal_minus_eq_swap) - -lemma hypreal_less_eq_diff: "(x (x (y<=x) = (y'<=x')" -apply (drule hypreal_less_eqI) -apply (simp add: hypreal_le_def) -done - -lemma hypreal_eq_eqI: "(x::hypreal) - y = x' - y' ==> (x=y) = (x'=y')" -apply safe -apply (simp_all add: hypreal_eq_diff_eq hypreal_diff_eq_eq) -done +subsection{*Misc Others*} lemma hypreal_zero_num: "0 = Abs_hypreal (hyprel `` {%n. 0})" by (simp add: hypreal_zero_def [THEN meta_eq_to_obj_eq, symmetric]) @@ -1122,8 +1005,19 @@ apply (auto simp add: hypreal_less hypreal_zero_num) done + +lemma hypreal_hrabs: + "abs (Abs_hypreal (hyprel `` {X})) = + Abs_hypreal(hyprel `` {%n. abs (X n)})" +apply (auto simp add: hrabs_def hypreal_zero_def hypreal_le hypreal_minus) +apply (ultra, arith)+ +done + ML {* +val hrabs_def = thm "hrabs_def"; +val hypreal_hrabs = thm "hypreal_hrabs"; + val hypreal_zero_def = thm "hypreal_zero_def"; val hypreal_one_def = thm "hypreal_one_def"; val hypreal_minus_def = thm "hypreal_minus_def"; @@ -1189,11 +1083,6 @@ val hypreal_add_zero_right = thm "hypreal_add_zero_right"; val hypreal_add_minus = thm "hypreal_add_minus"; val hypreal_add_minus_left = thm "hypreal_add_minus_left"; -val hypreal_minus_ex = thm "hypreal_minus_ex"; -val hypreal_minus_ex1 = thm "hypreal_minus_ex1"; -val hypreal_minus_left_ex1 = thm "hypreal_minus_left_ex1"; -val hypreal_add_minus_eq_minus = thm "hypreal_add_minus_eq_minus"; -val hypreal_as_add_inverse_ex = thm "hypreal_as_add_inverse_ex"; val hypreal_minus_add_distrib = thm "hypreal_minus_add_distrib"; val hypreal_minus_distrib1 = thm "hypreal_minus_distrib1"; val hypreal_add_left_cancel = thm "hypreal_add_left_cancel"; @@ -1214,7 +1103,6 @@ val hypreal_mult_minus_1 = thm "hypreal_mult_minus_1"; val hypreal_mult_minus_1_right = thm "hypreal_mult_minus_1_right"; val hypreal_minus_mult_commute = thm "hypreal_minus_mult_commute"; -val hypreal_add_assoc_cong = thm "hypreal_add_assoc_cong"; val hypreal_add_mult_distrib = thm "hypreal_add_mult_distrib"; val hypreal_add_mult_distrib2 = thm "hypreal_add_mult_distrib2"; val hypreal_diff_mult_distrib = thm "hypreal_diff_mult_distrib"; @@ -1224,35 +1112,24 @@ val hypreal_inverse = thm "hypreal_inverse"; val HYPREAL_INVERSE_ZERO = thm "HYPREAL_INVERSE_ZERO"; val HYPREAL_DIVISION_BY_ZERO = thm "HYPREAL_DIVISION_BY_ZERO"; -val hypreal_inverse_inverse = thm "hypreal_inverse_inverse"; -val hypreal_inverse_1 = thm "hypreal_inverse_1"; val hypreal_mult_inverse = thm "hypreal_mult_inverse"; val hypreal_mult_inverse_left = thm "hypreal_mult_inverse_left"; val hypreal_mult_left_cancel = thm "hypreal_mult_left_cancel"; val hypreal_mult_right_cancel = thm "hypreal_mult_right_cancel"; val hypreal_inverse_not_zero = thm "hypreal_inverse_not_zero"; val hypreal_mult_not_0 = thm "hypreal_mult_not_0"; -val hypreal_mult_zero_disj = thm "hypreal_mult_zero_disj"; val hypreal_minus_inverse = thm "hypreal_minus_inverse"; val hypreal_inverse_distrib = thm "hypreal_inverse_distrib"; -val hypreal_less_iff = thm "hypreal_less_iff"; -val hypreal_lessI = thm "hypreal_lessI"; -val hypreal_lessE = thm "hypreal_lessE"; -val hypreal_lessD = thm "hypreal_lessD"; val hypreal_less_not_refl = thm "hypreal_less_not_refl"; val hypreal_not_refl2 = thm "hypreal_not_refl2"; val hypreal_less_trans = thm "hypreal_less_trans"; val hypreal_less_asym = thm "hypreal_less_asym"; val hypreal_less = thm "hypreal_less"; val hypreal_trichotomy = thm "hypreal_trichotomy"; -val hypreal_trichotomyE = thm "hypreal_trichotomyE"; val hypreal_less_minus_iff = thm "hypreal_less_minus_iff"; val hypreal_less_minus_iff2 = thm "hypreal_less_minus_iff2"; val hypreal_eq_minus_iff = thm "hypreal_eq_minus_iff"; val hypreal_eq_minus_iff2 = thm "hypreal_eq_minus_iff2"; -val hypreal_diff_zero = thm "hypreal_diff_zero"; -val hypreal_diff_zero_right = thm "hypreal_diff_zero_right"; -val hypreal_diff_self = thm "hypreal_diff_self"; val hypreal_eq_minus_iff3 = thm "hypreal_eq_minus_iff3"; val hypreal_not_eq_minus_iff = thm "hypreal_not_eq_minus_iff"; val hypreal_linear = thm "hypreal_linear"; @@ -1270,7 +1147,6 @@ val hypreal_le_linear = thm "hypreal_le_linear"; val hypreal_le_trans = thm "hypreal_le_trans"; val hypreal_le_anti_sym = thm "hypreal_le_anti_sym"; -val not_less_not_eq_hypreal_less = thm "not_less_not_eq_hypreal_less"; val hypreal_less_le = thm "hypreal_less_le"; val hypreal_minus_zero_less_iff = thm "hypreal_minus_zero_less_iff"; val hypreal_minus_zero_less_iff2 = thm "hypreal_minus_zero_less_iff2"; @@ -1287,34 +1163,14 @@ val hypreal_of_real_zero_iff = thm "hypreal_of_real_zero_iff"; val hypreal_of_real_inverse = thm "hypreal_of_real_inverse"; val hypreal_of_real_divide = thm "hypreal_of_real_divide"; -val hypreal_zero_divide = thm "hypreal_zero_divide"; val hypreal_divide_one = thm "hypreal_divide_one"; -val hypreal_divide_divide1_eq = thm "hypreal_divide_divide1_eq"; -val hypreal_divide_divide2_eq = thm "hypreal_divide_divide2_eq"; -val hypreal_minus_divide_eq = thm "hypreal_minus_divide_eq"; -val hypreal_divide_minus_eq = thm "hypreal_divide_minus_eq"; val hypreal_add_divide_distrib = thm "hypreal_add_divide_distrib"; val hypreal_inverse_add = thm "hypreal_inverse_add"; val hypreal_self_eq_minus_self_zero = thm "hypreal_self_eq_minus_self_zero"; val hypreal_add_self_zero_cancel = thm "hypreal_add_self_zero_cancel"; val hypreal_add_self_zero_cancel2 = thm "hypreal_add_self_zero_cancel2"; -val hypreal_add_self_zero_cancel2a = thm "hypreal_add_self_zero_cancel2a"; val hypreal_minus_eq_swap = thm "hypreal_minus_eq_swap"; val hypreal_minus_eq_cancel = thm "hypreal_minus_eq_cancel"; -val hypreal_less_eq_diff = thm "hypreal_less_eq_diff"; -val hypreal_add_diff_eq = thm "hypreal_add_diff_eq"; -val hypreal_diff_add_eq = thm "hypreal_diff_add_eq"; -val hypreal_diff_diff_eq = thm "hypreal_diff_diff_eq"; -val hypreal_diff_diff_eq2 = thm "hypreal_diff_diff_eq2"; -val hypreal_diff_less_eq = thm "hypreal_diff_less_eq"; -val hypreal_less_diff_eq = thm "hypreal_less_diff_eq"; -val hypreal_diff_le_eq = thm "hypreal_diff_le_eq"; -val hypreal_le_diff_eq = thm "hypreal_le_diff_eq"; -val hypreal_diff_eq_eq = thm "hypreal_diff_eq_eq"; -val hypreal_eq_diff_eq = thm "hypreal_eq_diff_eq"; -val hypreal_less_eqI = thm "hypreal_less_eqI"; -val hypreal_le_eqI = thm "hypreal_le_eqI"; -val hypreal_eq_eqI = thm "hypreal_eq_eqI"; val hypreal_zero_num = thm "hypreal_zero_num"; val hypreal_one_num = thm "hypreal_one_num"; val hypreal_omega_gt_zero = thm "hypreal_omega_gt_zero"; diff -r fd063037fdf5 -r ff3210fe968f src/HOL/Hyperreal/HyperOrd.thy --- a/src/HOL/Hyperreal/HyperOrd.thy Wed Dec 24 08:54:30 2003 +0100 +++ b/src/HOL/Hyperreal/HyperOrd.thy Thu Dec 25 22:48:32 2003 +0100 @@ -7,95 +7,6 @@ theory HyperOrd = HyperDef: -instance hypreal :: division_by_zero -proof - fix x :: hypreal - show "inverse 0 = (0::hypreal)" by (rule HYPREAL_INVERSE_ZERO) - show "x/0 = 0" by (rule HYPREAL_DIVISION_BY_ZERO) -qed - - -defs (overloaded) - hrabs_def: "abs (r::hypreal) == (if 0 \ r then r else -r)" - - -lemma hypreal_hrabs: - "abs (Abs_hypreal (hyprel `` {X})) = - Abs_hypreal(hyprel `` {%n. abs (X n)})" -apply (auto simp add: hrabs_def hypreal_zero_def hypreal_le hypreal_minus) -apply (ultra, arith)+ -done - -instance hypreal :: order - by (intro_classes, - (assumption | - rule hypreal_le_refl hypreal_le_trans hypreal_le_anti_sym - hypreal_less_le)+) - -instance hypreal :: linorder - by (intro_classes, rule hypreal_le_linear) - -instance hypreal :: plus_ac0 - by (intro_classes, - (assumption | - rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+) - -lemma hypreal_add_less_mono1: "(A::hypreal) < B ==> A + C < B + C" -apply (rule_tac z = A in eq_Abs_hypreal) -apply (rule_tac z = B in eq_Abs_hypreal) -apply (rule_tac z = C in eq_Abs_hypreal) -apply (auto intro!: exI simp add: hypreal_less_def hypreal_add, ultra) -done - -lemma hypreal_mult_order: "[| 0 < x; 0 < y |] ==> (0::hypreal) < x * y" -apply (unfold hypreal_zero_def) -apply (rule_tac z = x in eq_Abs_hypreal) -apply (rule_tac z = y in eq_Abs_hypreal) -apply (auto intro!: exI simp add: hypreal_less_def hypreal_mult, ultra) -apply (auto intro: real_mult_order) -done - -lemma hypreal_add_left_le_mono1: "(q1::hypreal) \ q2 ==> x + q1 \ x + q2" -apply (drule order_le_imp_less_or_eq) -apply (auto intro: order_less_imp_le hypreal_add_less_mono1 simp add: hypreal_add_commute) -done - -lemma hypreal_mult_less_mono1: "[| (0::hypreal) < z; x < y |] ==> x*z < y*z" -apply (rotate_tac 1) -apply (drule hypreal_less_minus_iff [THEN iffD1]) -apply (rule hypreal_less_minus_iff [THEN iffD2]) -apply (drule hypreal_mult_order, assumption) -apply (simp add: hypreal_add_mult_distrib2 hypreal_mult_commute) -done - -lemma hypreal_mult_less_mono2: "[| (0::hypreal) z*x (1::hypreal)" by (rule hypreal_zero_not_eq_one) - show "x \ y ==> z + x \ z + y" by (rule hypreal_add_left_le_mono1) - show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: hypreal_mult_less_mono2) - show "\x\ = (if x < 0 then -x else x)" - by (auto dest: order_le_less_trans simp add: hrabs_def linorder_not_le) - show "x \ 0 ==> inverse x * x = 1" by simp - show "y \ 0 ==> x / y = x * inverse y" by (simp add: hypreal_divide_def) -qed (*** Monotonicity results ***) @@ -277,9 +188,6 @@ ML {* -val hrabs_def = thm "hrabs_def"; -val hypreal_hrabs = thm "hypreal_hrabs"; - val hypreal_add_less_mono1 = thm"hypreal_add_less_mono1"; val hypreal_add_less_mono2 = thm"hypreal_add_less_mono2"; val hypreal_mult_order = thm"hypreal_mult_order"; diff -r fd063037fdf5 -r ff3210fe968f src/HOL/Hyperreal/Integration.ML --- a/src/HOL/Hyperreal/Integration.ML Wed Dec 24 08:54:30 2003 +0100 +++ b/src/HOL/Hyperreal/Integration.ML Thu Dec 25 22:48:32 2003 +0100 @@ -183,7 +183,7 @@ by (dres_inst_tac [("x","psize D - Suc n")] spec 2); by (thin_tac "ALL n. psize D <= n --> D n = b" 2); by (Asm_full_simp_tac 2); -by (Blast_tac 1); +by (arith_tac 1); qed "partition_ub"; Goal "[| partition(a,b) D; n < psize D |] ==> D(n) < b"; diff -r fd063037fdf5 -r ff3210fe968f src/HOL/Hyperreal/NSA.ML --- a/src/HOL/Hyperreal/NSA.ML Wed Dec 24 08:54:30 2003 +0100 +++ b/src/HOL/Hyperreal/NSA.ML Thu Dec 25 22:48:32 2003 +0100 @@ -350,7 +350,7 @@ by (forw_inst_tac [("x1","r"),("z","abs x")] (hypreal_inverse_gt_0 RS order_less_trans) 1); by (assume_tac 1); -by (dtac ((hypreal_inverse_inverse RS sym) RS subst) 1); +by (dtac ((inverse_inverse_eq RS sym) RS subst) 1); by (rtac (hypreal_inverse_less_iff RS iffD1) 1); by (auto_tac (claset(), simpset() addsimps [SReal_inverse])); qed "HInfinite_inverse_Infinitesimal"; @@ -2244,7 +2244,7 @@ Goal "(u = inverse (real(Suc n))) = (real(Suc n) = inverse u)"; by (auto_tac (claset(), - simpset() addsimps [real_inverse_inverse, real_of_nat_Suc_gt_zero, + simpset() addsimps [inverse_inverse_eq, real_of_nat_Suc_gt_zero, real_not_refl2 RS not_sym])); qed "real_of_nat_inverse_eq_iff"; diff -r fd063037fdf5 -r ff3210fe968f src/HOL/Hyperreal/SEQ.ML --- a/src/HOL/Hyperreal/SEQ.ML Wed Dec 24 08:54:30 2003 +0100 +++ b/src/HOL/Hyperreal/SEQ.ML Thu Dec 25 22:48:32 2003 +0100 @@ -1130,9 +1130,9 @@ by (ftac order_less_trans 1 THEN assume_tac 1); by (forw_inst_tac [("x","f n")] real_inverse_gt_0 1); by (asm_simp_tac (simpset() addsimps [abs_eqI2]) 1); -by (res_inst_tac [("t","r")] (real_inverse_inverse RS subst) 1); +by (res_inst_tac [("t","r")] (inverse_inverse_eq RS subst) 1); by (auto_tac (claset() addIs [inverse_less_iff_less RS iffD2], - simpset() delsimps [thm"Ring_and_Field.inverse_inverse_eq"])); + simpset() delsimps [inverse_inverse_eq])); qed "LIMSEQ_inverse_zero"; Goal "ALL y. EX N. ALL n. N <= n --> y < f(n) \ diff -r fd063037fdf5 -r ff3210fe968f src/HOL/Integ/int_arith1.ML --- a/src/HOL/Integ/int_arith1.ML Wed Dec 24 08:54:30 2003 +0100 +++ b/src/HOL/Integ/int_arith1.ML Thu Dec 25 22:48:32 2003 +0100 @@ -5,6 +5,43 @@ Simprocs and decision procedure for linear arithmetic. *) +(** Misc ML bindings **) + +val left_inverse = thm "left_inverse"; +val right_inverse = thm "right_inverse"; +val inverse_less_iff_less = thm"Ring_and_Field.inverse_less_iff_less"; +val inverse_eq_divide = thm"Ring_and_Field.inverse_eq_divide"; +val inverse_minus_eq = thm "inverse_minus_eq"; +val inverse_mult_distrib = thm "inverse_mult_distrib"; +val inverse_add = thm "inverse_add"; +val inverse_inverse_eq = thm "inverse_inverse_eq"; + +val add_right_mono = thm"Ring_and_Field.add_right_mono"; +val times_divide_eq_left = thm "times_divide_eq_left"; +val times_divide_eq_right = thm "times_divide_eq_right"; +val minus_minus = thm "minus_minus"; +val minus_mult_left = thm "minus_mult_left"; +val minus_mult_right = thm "minus_mult_right"; + +val pos_real_less_divide_eq = thm"pos_less_divide_eq"; +val pos_real_divide_less_eq = thm"pos_divide_less_eq"; +val pos_real_le_divide_eq = thm"pos_le_divide_eq"; +val pos_real_divide_le_eq = thm"pos_divide_le_eq"; + +val mult_less_cancel_left = thm"Ring_and_Field.mult_less_cancel_left"; +val mult_le_cancel_left = thm"Ring_and_Field.mult_le_cancel_left"; +val mult_less_cancel_right = thm"Ring_and_Field.mult_less_cancel_right"; +val mult_le_cancel_right = thm"Ring_and_Field.mult_le_cancel_right"; +val mult_cancel_left = thm"Ring_and_Field.mult_cancel_left"; +val mult_cancel_right = thm"Ring_and_Field.mult_cancel_right"; + +val field_mult_cancel_left = thm "field_mult_cancel_left"; +val field_mult_cancel_right = thm "field_mult_cancel_right"; + +val mult_divide_cancel_left = thm"Ring_and_Field.mult_divide_cancel_left"; +val mult_divide_cancel_right = thm "Ring_and_Field.mult_divide_cancel_right"; +val mult_divide_cancel_eq_if = thm"Ring_and_Field.mult_divide_cancel_eq_if"; + val NCons_Pls = thm"NCons_Pls"; val NCons_Min = thm"NCons_Min"; val NCons_BIT = thm"NCons_BIT"; diff -r fd063037fdf5 -r ff3210fe968f src/HOL/Real/HahnBanach/Subspace.thy --- a/src/HOL/Real/HahnBanach/Subspace.thy Wed Dec 24 08:54:30 2003 +0100 +++ b/src/HOL/Real/HahnBanach/Subspace.thy Thu Dec 25 22:48:32 2003 +0100 @@ -329,13 +329,13 @@ proof (rule add_minus_eq) show "u1 \ E" .. show "u2 \ E" .. - from u u' and direct show "u1 - u2 = 0" by blast + from u u' and direct show "u1 - u2 = 0" by force qed show "v1 = v2" proof (rule add_minus_eq [symmetric]) show "v1 \ E" .. show "v2 \ E" .. - from v v' and direct show "v2 - v1 = 0" by blast + from v v' and direct show "v2 - v1 = 0" by force qed qed diff -r fd063037fdf5 -r ff3210fe968f src/HOL/Real/RealArith.thy --- a/src/HOL/Real/RealArith.thy Wed Dec 24 08:54:30 2003 +0100 +++ b/src/HOL/Real/RealArith.thy Thu Dec 25 22:48:32 2003 +0100 @@ -31,9 +31,7 @@ by auto -(** Simprules combining x-y and 0; see also real_less_iff_diff_less_0, etc., - in RealBin -**) +(** Simprules combining x-y and 0 (needed??) **) lemma real_0_less_diff_iff [iff]: "((0::real) < x-y) = (y < x)" by auto diff -r fd063037fdf5 -r ff3210fe968f src/HOL/Real/RealBin.ML --- a/src/HOL/Real/RealBin.ML Wed Dec 24 08:54:30 2003 +0100 +++ b/src/HOL/Real/RealBin.ML Thu Dec 25 22:48:32 2003 +0100 @@ -192,17 +192,6 @@ (**** Simprocs for numeric literals ****) -(** Combining of literal coefficients in sums of products **) - -Goal "(x = y) = (x-y = (0::real))"; -by (simp_tac (simpset() addsimps compare_rls) 1); -qed "real_eq_iff_diff_eq_0"; - -Goal "(x <= y) = (x-y <= (0::real))"; -by (simp_tac (simpset() addsimps compare_rls) 1); -qed "real_le_iff_diff_le_0"; - - (** For combine_numerals **) Goal "i*u + (j*u + k) = (i+j)*u + (k::real)"; @@ -212,12 +201,10 @@ (** For cancel_numerals **) -val rel_iff_rel_0_rls = map (inst "y" "?u+?v") - [real_less_eq_diff, real_eq_iff_diff_eq_0, - real_le_iff_diff_le_0] @ - map (inst "y" "n") - [real_less_eq_diff, real_eq_iff_diff_eq_0, - real_le_iff_diff_le_0]; +val rel_iff_rel_0_rls = map (inst "b" "?u+?v") + [less_iff_diff_less_0, eq_iff_diff_eq_0, le_iff_diff_le_0] @ + map (inst "b" "n") + [less_iff_diff_less_0, eq_iff_diff_eq_0, le_iff_diff_le_0]; Goal "!!i::real. (i*u + m = j*u + n) = ((i-j)*u + m = n)"; by (asm_simp_tac (simpset() addsimps [real_diff_def, real_add_mult_distrib]@ @@ -603,9 +590,9 @@ Addsimprocs [Real_Times_Assoc.conv]; (*Simplification of x-y < 0, etc.*) -AddIffs [real_less_eq_diff RS sym]; -AddIffs [real_eq_iff_diff_eq_0 RS sym]; -AddIffs [real_le_iff_diff_le_0 RS sym]; +AddIffs [less_iff_diff_less_0 RS sym]; +AddIffs [eq_iff_diff_eq_0 RS sym]; +AddIffs [le_iff_diff_le_0 RS sym]; (** <= monotonicity results: needed for arithmetic **) diff -r fd063037fdf5 -r ff3210fe968f src/HOL/Real/RealDef.thy --- a/src/HOL/Real/RealDef.thy Wed Dec 24 08:54:30 2003 +0100 +++ b/src/HOL/Real/RealDef.thy Thu Dec 25 22:48:32 2003 +0100 @@ -93,17 +93,17 @@ real_of_nat_def: "real n == real_of_posnat n + (- 1)" real_add_def: - "P+Q == Abs_REAL(UN p1:Rep_REAL(P). UN p2:Rep_REAL(Q). + "P+Q == Abs_REAL(\p1\Rep_REAL(P). \p2\Rep_REAL(Q). (%(x1,y1). (%(x2,y2). realrel``{(x1+x2, y1+y2)}) p2) p1)" real_mult_def: - "P*Q == Abs_REAL(UN p1:Rep_REAL(P). UN p2:Rep_REAL(Q). + "P*Q == Abs_REAL(\p1\Rep_REAL(P). \p2\Rep_REAL(Q). (%(x1,y1). (%(x2,y2). realrel``{(x1*x2+y1*y2,x1*y2+x2*y1)}) p2) p1)" real_less_def: "Px1 y1 x2 y2. x1 + y2 < x2 + y1 & - (x1,y1):Rep_REAL(P) & (x2,y2):Rep_REAL(Q)" + (x1,y1)\Rep_REAL(P) & (x2,y2)\Rep_REAL(Q)" real_le_def: "P \ (Q::real) == ~(Q < P)" @@ -112,7 +112,7 @@ Nats :: "'a set" ("\") -(*** Proving that realrel is an equivalence relation ***) +subsection{*Proving that realrel is an equivalence relation*} lemma preal_trans_lemma: "[| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] @@ -225,7 +225,7 @@ declare real_minus_zero_iff [simp] -(*** Congruence property for addition ***) +subsection{*Congruence property for addition*} lemma real_add_congruent2_lemma: "[|a + ba = aa + b; ab + bc = ac + bb|] @@ -298,9 +298,10 @@ declare real_add_minus_left [simp] -(*** Congruence property for multiplication ***) +subsection{*Congruence property for multiplication*} -lemma real_mult_congruent2_lemma: "!!(x1::preal). [| x1 + y2 = x2 + y1 |] ==> +lemma real_mult_congruent2_lemma: + "!!(x1::preal). [| x1 + y2 = x2 + y1 |] ==> x * x1 + y * y1 + (x * y2 + x2 * y) = x * x2 + y * y2 + (x * y1 + x1 * y)" apply (simp add: preal_add_left_commute preal_add_assoc [symmetric] preal_add_mult_distrib2 [symmetric]) @@ -407,7 +408,8 @@ (** Lemmas **) -lemma real_add_assoc_cong: "(z::real) + v = z' + v' ==> z + (v + w) = z' + (v' + w)" +lemma real_add_assoc_cong: + "(z::real) + v = z' + v' ==> z + (v + w) = z' + (v' + w)" by (simp add: real_add_assoc [symmetric]) lemma real_add_mult_distrib: "((z1::real) + z2) * w = (z1 * w) + (z2 * w)" @@ -428,13 +430,13 @@ lemma real_diff_mult_distrib2: "(w::real) * (z1 - z2) = (w * z1) - (w * z2)" by (simp add: real_mult_commute [of w] real_diff_mult_distrib) -(*** one and zero are distinct ***) +text{*one and zero are distinct*} lemma real_zero_not_eq_one: "0 ~= (1::real)" apply (unfold real_zero_def real_one_def) apply (auto simp add: preal_self_less_add_left [THEN preal_not_refl2]) done -(*** existence of inverse ***) +subsection{*existence of inverse*} (** lemma -- alternative definition of 0 **) lemma real_zero_iff: "0 = Abs_REAL (realrel `` {(x, x)})" apply (unfold real_zero_def) @@ -449,7 +451,9 @@ apply (auto dest!: preal_less_add_left_Ex simp add: real_zero_iff [symmetric]) apply (rule_tac x = "Abs_REAL (realrel `` { (preal_of_prat (prat_of_pnat 1), pinv (D) + preal_of_prat (prat_of_pnat 1))}) " in exI) apply (rule_tac [2] x = "Abs_REAL (realrel `` { (pinv (D) + preal_of_prat (prat_of_pnat 1), preal_of_prat (prat_of_pnat 1))}) " in exI) -apply (auto simp add: real_mult pnat_one_def preal_mult_1_right preal_add_mult_distrib2 preal_add_mult_distrib preal_mult_1 preal_mult_inv_right preal_add_ac preal_mult_ac) +apply (auto simp add: real_mult pnat_one_def preal_mult_1_right + preal_add_mult_distrib2 preal_add_mult_distrib preal_mult_1 + preal_mult_inv_right preal_add_ac preal_mult_ac) done lemma real_mult_inv_left_ex: "x ~= 0 ==> \y. y*x = (1::real)" @@ -471,21 +475,21 @@ declare real_mult_inv_right [simp] -(*--------------------------------------------------------- - Theorems for ordering - --------------------------------------------------------*) -(* prove introduction and elimination rules for real_less *) +subsection{*Theorems for Ordering*} + +(* real_less is a strict order: irreflexive *) -(* real_less is a strong order i.e. nonreflexive and transitive *) - -(*** lemmas ***) -lemma preal_lemma_eq_rev_sum: "!!(x::preal). [| x = y; x1 = y1 |] ==> x + y1 = x1 + y" +text{*lemmas*} +lemma preal_lemma_eq_rev_sum: + "!!(x::preal). [| x = y; x1 = y1 |] ==> x + y1 = x1 + y" by (simp add: preal_add_commute) -lemma preal_add_left_commute_cancel: "!!(b::preal). x + (b + y) = x1 + (b + y1) ==> x + y = x1 + y1" +lemma preal_add_left_commute_cancel: + "!!(b::preal). x + (b + y) = x1 + (b + y1) ==> x + y = x1 + y1" by (simp add: preal_add_ac) -lemma preal_lemma_for_not_refl: "!!(x::preal). [| x + y2a = x2a + y; +lemma preal_lemma_for_not_refl: + "!!(x::preal). [| x + y2a = x2a + y; x + y2b = x2b + y |] ==> x2a + y2b = x2b + y2a" apply (drule preal_lemma_eq_rev_sum, assumption) @@ -569,10 +573,11 @@ apply (simp add: preal_add_assoc [symmetric] preal_self_less_add_left) done -lemma real_of_preal_iff: "(\m. Abs_REAL (realrel `` {(x,y)}) = real_of_preal m) = (y < x)" +lemma real_of_preal_iff: + "(\m. Abs_REAL (realrel `` {(x,y)}) = real_of_preal m) = (y < x)" by (blast intro!: real_of_preal_ExI real_of_preal_ExD) -(*** Gleason prop 9-4.4 p 127 ***) +text{*Gleason prop 9-4.4 p 127*} lemma real_of_preal_trichotomy: "\m. (x::real) = real_of_preal m | x = 0 | x = -(real_of_preal m)" apply (unfold real_of_preal_def real_zero_def) @@ -583,7 +588,8 @@ apply (auto simp add: preal_add_commute) done -lemma real_of_preal_trichotomyE: "!!P. [| !!m. x = real_of_preal m ==> P; +lemma real_of_preal_trichotomyE: + "!!P. [| !!m. x = real_of_preal m ==> P; x = 0 ==> P; !!m. x = -(real_of_preal m) ==> P |] ==> P" apply (cut_tac x = x in real_of_preal_trichotomy, auto) @@ -606,7 +612,8 @@ apply (simp add: preal_self_less_add_left del: preal_add_less_iff2) done -lemma real_of_preal_less_iff1: "(real_of_preal m1 < real_of_preal m2) = (m1 < m2)" +lemma real_of_preal_less_iff1: + "(real_of_preal m1 < real_of_preal m2) = (m1 < m2)" by (blast intro: real_of_preal_lessI real_of_preal_lessD) declare real_of_preal_less_iff1 [simp] @@ -677,7 +684,8 @@ apply (blast dest: real_less_trans elim: real_less_irrefl) done -lemma real_of_preal_minus_less_rev1: "- real_of_preal m1 < - real_of_preal m2 +lemma real_of_preal_minus_less_rev1: + "- real_of_preal m1 < - real_of_preal m2 ==> real_of_preal m2 < real_of_preal m1" apply (auto simp add: real_of_preal_def real_less_def real_minus) apply (rule exI)+ @@ -688,7 +696,8 @@ apply (auto simp add: preal_add_ac) done -lemma real_of_preal_minus_less_rev2: "real_of_preal m1 < real_of_preal m2 +lemma real_of_preal_minus_less_rev2: + "real_of_preal m1 < real_of_preal m2 ==> - real_of_preal m2 < - real_of_preal m1" apply (auto simp add: real_of_preal_def real_less_def real_minus) apply (rule exI)+ @@ -699,7 +708,8 @@ apply (auto simp add: preal_add_ac) done -lemma real_of_preal_minus_less_rev_iff: "(- real_of_preal m1 < - real_of_preal m2) = +lemma real_of_preal_minus_less_rev_iff: + "(- real_of_preal m1 < - real_of_preal m2) = (real_of_preal m2 < real_of_preal m1)" apply (blast intro!: real_of_preal_minus_less_rev1 real_of_preal_minus_less_rev2) done @@ -721,7 +731,8 @@ by (cut_tac real_linear, blast) -lemma real_linear_less2: "!!(R1::real). [| R1 < R2 ==> P; R1 = R2 ==> P; +lemma real_linear_less2: + "!!(R1::real). [| R1 < R2 ==> P; R1 = R2 ==> P; R2 < R1 ==> P |] ==> P" apply (cut_tac x = R1 and y = R2 in real_linear, auto) done diff -r fd063037fdf5 -r ff3210fe968f src/HOL/Real/RealOrd.thy --- a/src/HOL/Real/RealOrd.thy Wed Dec 24 08:54:30 2003 +0100 +++ b/src/HOL/Real/RealOrd.thy Thu Dec 25 22:48:32 2003 +0100 @@ -56,7 +56,7 @@ done (* Axiom 'order_less_le' of class 'order': *) -lemma real_less_le: "((w::real) < z) = (w \ z & w ~= z)" +lemma real_less_le: "((w::real) < z) = (w \ z & w \ z)" apply (simp add: real_le_def real_neq_iff) apply (blast elim!: real_less_asym) done @@ -84,11 +84,13 @@ apply (blast elim!: real_less_irrefl real_of_preal_not_minus_gt_zero [THEN notE]) done -lemma real_gt_preal_preal_Ex: "real_of_preal z < x ==> \y. x = real_of_preal y" +lemma real_gt_preal_preal_Ex: + "real_of_preal z < x ==> \y. x = real_of_preal y" by (blast dest!: real_of_preal_zero_less [THEN real_less_trans] intro: real_gt_zero_preal_Ex [THEN iffD1]) -lemma real_ge_preal_preal_Ex: "real_of_preal z \ x ==> \y. x = real_of_preal y" +lemma real_ge_preal_preal_Ex: + "real_of_preal z \ x ==> \y. x = real_of_preal y" by (blast dest: order_le_imp_less_or_eq real_gt_preal_preal_Ex) lemma real_less_all_preal: "y \ 0 ==> \x. y < real_of_preal x" @@ -99,7 +101,8 @@ lemma real_less_all_real2: "~ 0 < y ==> \x. y < real_of_preal x" by (blast intro!: real_less_all_preal real_leI) -lemma real_of_preal_le_iff: "(real_of_preal m1 \ real_of_preal m2) = (m1 \ m2)" +lemma real_of_preal_le_iff: + "(real_of_preal m1 \ real_of_preal m2) = (m1 \ m2)" apply (auto intro!: preal_leI simp add: linorder_not_less [symmetric]) done @@ -241,7 +244,7 @@ apply (auto simp add: real_zero_not_eq_one) done -lemma DIVISION_BY_ZERO [simp]: "a / (0::real) = 0" +lemma DIVISION_BY_ZERO: "a / (0::real) = 0" by (simp add: real_divide_def INVERSE_ZERO) instance real :: division_by_zero @@ -251,27 +254,24 @@ show "x/0 = 0" by (rule DIVISION_BY_ZERO) qed -lemma real_mult_left_cancel: "(c::real) ~= 0 ==> (c*a=c*b) = (a=b)" +lemma real_mult_left_cancel: "(c::real) \ 0 ==> (c*a=c*b) = (a=b)" by auto -lemma real_mult_right_cancel: "(c::real) ~= 0 ==> (a*c=b*c) = (a=b)" +lemma real_mult_right_cancel: "(c::real) \ 0 ==> (a*c=b*c) = (a=b)" by auto -lemma real_mult_left_cancel_ccontr: "c*a ~= c*b ==> a ~= b" +lemma real_mult_left_cancel_ccontr: "c*a \ c*b ==> a \ b" by auto -lemma real_mult_right_cancel_ccontr: "a*c ~= b*c ==> a ~= b" +lemma real_mult_right_cancel_ccontr: "a*c \ b*c ==> a \ b" by auto -lemma real_inverse_not_zero: "x ~= 0 ==> inverse(x::real) ~= 0" +lemma real_inverse_not_zero: "x \ 0 ==> inverse(x::real) \ 0" by (rule Ring_and_Field.nonzero_imp_inverse_nonzero) -lemma real_mult_not_zero: "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::real)" +lemma real_mult_not_zero: "[| x \ 0; y \ 0 |] ==> x * y \ (0::real)" by simp -lemma real_inverse_inverse: "inverse(inverse (x::real)) = x" - by (rule Ring_and_Field.inverse_inverse_eq) - lemma real_inverse_1: "inverse((1::real)) = (1::real)" by (rule Ring_and_Field.inverse_1) @@ -301,7 +301,8 @@ apply (erule add_left_mono) done -lemma real_add_le_less_mono: "!!z z'::real. [| w'\w; z' w' + z' < w + z" +lemma real_add_le_less_mono: + "!!z z'::real. [| w'\w; z' w' + z' < w + z" apply (erule add_right_mono [THEN order_le_less_trans]) apply (erule add_strict_left_mono) done @@ -371,7 +372,8 @@ lemma real_mult_is_0 [iff]: "(x*y = 0) = (x = 0 | y = (0::real))" by (rule Ring_and_Field.mult_eq_0_iff) -lemma real_inverse_add: "[| x \ 0; y \ 0 |] +lemma real_inverse_add: + "[| x \ 0; y \ 0 |] ==> inverse x + inverse y = (x + y) * inverse (x * (y::real))" by (simp add: Ring_and_Field.inverse_add mult_assoc) @@ -436,13 +438,15 @@ apply (simp (no_asm_use) add: real_of_posnat_one [symmetric] real_of_posnat_def real_of_preal_add [symmetric] preal_of_prat_add [symmetric] prat_of_pnat_add [symmetric] pnat_of_nat_add) done -lemma real_of_posnat_add_one: "real_of_posnat (n + 1) = real_of_posnat n + (1::real)" +lemma real_of_posnat_add_one: + "real_of_posnat (n + 1) = real_of_posnat n + (1::real)" apply (rule_tac x1 = " (1::real) " in real_add_right_cancel [THEN iffD1]) apply (rule real_of_posnat_add [THEN subst]) apply (simp (no_asm_use) add: real_of_posnat_two real_add_assoc) done -lemma real_of_posnat_Suc: "real_of_posnat (Suc n) = real_of_posnat n + (1::real)" +lemma real_of_posnat_Suc: + "real_of_posnat (Suc n) = real_of_posnat n + (1::real)" by (subst real_of_posnat_add_one [symmetric], simp) lemma inj_real_of_posnat: "inj(real_of_posnat)" @@ -535,7 +539,7 @@ done lemma real_inverse_unique: "x*y = (1::real) ==> y = inverse x" -apply (case_tac "x ~= 0") +apply (case_tac "x \ 0") apply (rule_tac c1 = x in real_mult_left_cancel [THEN iffD1], auto) done @@ -564,7 +568,8 @@ done declare real_of_nat_ge_zero_cancel_iff [simp] -lemma real_of_nat_num_if: "real n = (if n=0 then 0 else 1 + real ((n::nat) - 1))" +lemma real_of_nat_num_if: + "real n = (if n=0 then 0 else 1 + real ((n::nat) - 1))" apply (case_tac "n", simp) apply (simp add: real_of_nat_Suc add_commute) done @@ -721,7 +726,6 @@ val real_mult_right_cancel_ccontr = thm"real_mult_right_cancel_ccontr"; val real_inverse_not_zero = thm"real_inverse_not_zero"; val real_mult_not_zero = thm"real_mult_not_zero"; -val real_inverse_inverse = thm"real_inverse_inverse"; val real_inverse_1 = thm"real_inverse_1"; val real_minus_inverse = thm"real_minus_inverse"; val real_inverse_distrib = thm"real_inverse_distrib"; diff -r fd063037fdf5 -r ff3210fe968f src/HOL/Real/real_arith0.ML --- a/src/HOL/Real/real_arith0.ML Wed Dec 24 08:54:30 2003 +0100 +++ b/src/HOL/Real/real_arith0.ML Thu Dec 25 22:48:32 2003 +0100 @@ -6,43 +6,6 @@ Instantiation of the generic linear arithmetic package for type real. *) -(** Misc ML bindings **) -(*FIXME: move to Integ or earlier*) - -val left_inverse = thm "left_inverse"; -val right_inverse = thm "right_inverse"; -val inverse_less_iff_less = thm"Ring_and_Field.inverse_less_iff_less"; -val inverse_eq_divide = thm"Ring_and_Field.inverse_eq_divide"; -val inverse_minus_eq = thm "inverse_minus_eq"; -val inverse_mult_distrib = thm "inverse_mult_distrib"; -val inverse_add = thm "inverse_add"; - -val add_right_mono = thm"Ring_and_Field.add_right_mono"; -val times_divide_eq_left = thm "times_divide_eq_left"; -val times_divide_eq_right = thm "times_divide_eq_right"; -val minus_minus = thm "minus_minus"; -val minus_mult_left = thm "minus_mult_left"; -val minus_mult_right = thm "minus_mult_right"; - -val pos_real_less_divide_eq = thm"pos_less_divide_eq"; -val pos_real_divide_less_eq = thm"pos_divide_less_eq"; -val pos_real_le_divide_eq = thm"pos_le_divide_eq"; -val pos_real_divide_le_eq = thm"pos_divide_le_eq"; - -val mult_less_cancel_left = thm"Ring_and_Field.mult_less_cancel_left"; -val mult_le_cancel_left = thm"Ring_and_Field.mult_le_cancel_left"; -val mult_less_cancel_right = thm"Ring_and_Field.mult_less_cancel_right"; -val mult_le_cancel_right = thm"Ring_and_Field.mult_le_cancel_right"; -val mult_cancel_left = thm"Ring_and_Field.mult_cancel_left"; -val mult_cancel_right = thm"Ring_and_Field.mult_cancel_right"; - -val field_mult_cancel_left = thm "field_mult_cancel_left"; -val field_mult_cancel_right = thm "field_mult_cancel_right"; - -val mult_divide_cancel_left = thm"Ring_and_Field.mult_divide_cancel_left"; -val mult_divide_cancel_right = thm "Ring_and_Field.mult_divide_cancel_right"; -val mult_divide_cancel_eq_if = thm"Ring_and_Field.mult_divide_cancel_eq_if"; - local