# HG changeset patch
# User paulson
# Date 1072098774 -3600
# Node ID 1dd7439477dd9b900178a7eb0e3a1e961298dd30
# Parent  f508492af9b44da5f1c14bfa5a5d337e7f1b40bd
simplifying

diff -r f508492af9b4 -r 1dd7439477dd src/HOL/Hyperreal/HyperOrd.thy
--- a/src/HOL/Hyperreal/HyperOrd.thy	Mon Dec 22 12:50:22 2003 +0100
+++ b/src/HOL/Hyperreal/HyperOrd.thy	Mon Dec 22 14:12:54 2003 +0100
@@ -40,6 +40,109 @@
       (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) \<le> q2  ==> x + q1 \<le> 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<y |] ==> z*x<z*y"
+apply (simp (no_asm_simp) add: hypreal_mult_commute hypreal_mult_less_mono1)
+done
+
+subsection{*The Hyperreals Form an Ordered Field*}
+
+instance hypreal :: inverse ..
+
+instance hypreal :: ordered_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
+  show "x - y = x + (-y)" by (simp add: hypreal_diff_def)
+  show "(x * y) * z = x * (y * z)" by (rule hypreal_mult_assoc)
+  show "x * y = y * x" by (rule hypreal_mult_commute)
+  show "1 * x = x" by simp
+  show "(x + y) * z = x * z + y * z" by (simp add: hypreal_add_mult_distrib)
+  show "0 \<noteq> (1::hypreal)" by (rule hypreal_zero_not_eq_one)
+  show "x \<le> y ==> z + x \<le> 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 "\<bar>x\<bar> = (if x < 0 then -x else x)"
+    by (auto dest: order_le_less_trans simp add: hrabs_def linorder_not_le)
+  show "x \<noteq> 0 ==> inverse x * x = 1" by simp
+  show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: hypreal_divide_def)
+qed
+
+(*** Monotonicity results ***)
+
+lemma hypreal_add_right_cancel_less: "(v+z < w+z) = (v < (w::hypreal))"
+  by (rule Ring_and_Field.add_less_cancel_right)
+
+lemma hypreal_add_left_cancel_less: "(z+v < z+w) = (v < (w::hypreal))"
+  by (rule Ring_and_Field.add_less_cancel_left)
+
+lemma hypreal_add_right_cancel_le: "(v+z \<le> w+z) = (v \<le> (w::hypreal))"
+  by (rule Ring_and_Field.add_le_cancel_right)
+
+lemma hypreal_add_left_cancel_le: "(z+v \<le> z+w) = (v \<le> (w::hypreal))"
+  by (rule Ring_and_Field.add_le_cancel_left)
+
+lemma hypreal_add_less_mono: "[| (z1::hypreal) < y1; z2 < y2 |] ==> z1 + z2 < y1 + y2"
+ by (rule Ring_and_Field.add_strict_mono)
+
+lemma hypreal_add_le_mono1: "(q1::hypreal) \<le> q2  ==> q1 + x \<le> q2 + x"
+  by (rule Ring_and_Field.add_right_mono)
+
+lemma hypreal_add_le_mono: "[|(i::hypreal)\<le>j;  k\<le>l |] ==> i + k \<le> j + l"
+ by (rule Ring_and_Field.add_mono)
+
+lemma hypreal_add_less_le_mono: "[|(i::hypreal)<j;  k\<le>l |] ==> i + k < j + l"
+by (auto dest!: order_le_imp_less_or_eq intro: hypreal_add_less_mono1 hypreal_add_less_mono)
+
+lemma hypreal_add_less_mono2: "!!(A::hypreal). A < B ==> C + A < C + B"
+by (auto intro: hypreal_add_less_mono1 simp add: hypreal_add_commute)
+
+lemma hypreal_add_le_less_mono: "[|(i::hypreal)\<le>j;  k<l |] ==> i + k < j + l"
+apply (erule add_right_mono [THEN order_le_less_trans])
+apply (erule add_strict_left_mono) 
+done
+
+lemma hypreal_less_add_right_cancel: "(A::hypreal) + C < B + C ==> A < B"
+apply (simp (no_asm_use))
+done
+
+lemma hypreal_less_add_left_cancel: "(C::hypreal) + A < C + B ==> A < B"
+apply (simp (no_asm_use))
+done
+
+lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) \<le> y|] ==> r < x + y"
+by (auto dest: hypreal_add_less_le_mono)
+
+
 (**** The simproc abel_cancel ****)
 
 (*** Two lemmas needed for the simprocs ***)
@@ -99,11 +202,53 @@
 Addsimprocs [Hyperreal_Cancel.sum_conv, Hyperreal_Cancel.rel_conv];
 *}
 
-lemma hypreal_minus_diff_eq: "- (z - y) = y - (z::hypreal)"
-apply (simp (no_asm))
+lemma hypreal_le_add_right_cancel: "!!(A::hypreal). A + C \<le> B + C ==> A \<le> B"
+apply (drule_tac x = "-C" in hypreal_add_le_mono1)
+apply (simp add: hypreal_add_assoc)
+done
+
+lemma hypreal_le_add_left_cancel: "!!(A::hypreal). C + A \<le> C + B ==> A \<le> B"
+apply (drule_tac x = "-C" in hypreal_add_left_le_mono1)
+apply (simp add: hypreal_add_assoc [symmetric])
+done
+
+lemma hypreal_mult_less_zero: "[| 0 < x; y < 0 |] ==> x*y < (0::hypreal)"
+apply (drule hypreal_minus_zero_less_iff [THEN iffD2])
+apply (drule hypreal_mult_order, assumption)
+apply (rule hypreal_minus_zero_less_iff [THEN iffD1], simp)
+done
+
+lemma hypreal_mult_less_zero1: "[| x < 0; y < 0 |] ==> (0::hypreal) < x * y"
+apply (drule hypreal_minus_zero_less_iff [THEN iffD2])+
+apply (drule hypreal_mult_order, assumption, simp)
 done
-declare hypreal_minus_diff_eq [simp]
+
+lemma hypreal_le_square: "(0::hypreal) \<le> x*x"
+apply (rule_tac x = 0 and y = x in hypreal_linear_less2)
+apply (auto intro: hypreal_mult_order hypreal_mult_less_zero1 order_less_imp_le)
+done
+declare hypreal_le_square [simp]
+
+lemma hypreal_add_order: "[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y"
+apply (erule order_less_trans)
+apply (drule hypreal_add_less_mono2, simp)
+done
 
+lemma hypreal_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::hypreal) \<le> x + y"
+apply (drule order_le_imp_less_or_eq)+
+apply (auto intro: hypreal_add_order order_less_imp_le)
+done
+
+text{*The precondition could be weakened to @{term "0\<le>x"}*}
+lemma hypreal_mult_less_mono:
+     "[| u<v;  x<y;  (0::hypreal) < v;  0 < x |] ==> u*x < v* y"
+ by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le)
+
+lemma hypreal_inverse_gt_0: "0 < x ==> 0 < inverse (x::hypreal)"
+  by (rule Ring_and_Field.positive_imp_inverse_positive)
+
+lemma hypreal_inverse_less_0: "x < 0 ==> inverse (x::hypreal) < 0"
+  by (rule Ring_and_Field.negative_imp_inverse_negative)
 
 lemma hypreal_less_swap_iff: "((x::hypreal) < y) = (-y < -x)"
 apply (subst hypreal_less_minus_iff)
@@ -118,191 +263,12 @@
 apply (auto simp add: hypreal_less hypreal_minus, ultra+)
 done
 
-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_add_less_mono2: "!!(A::hypreal). A < B ==> C + A < C + B"
-by (auto intro: hypreal_add_less_mono1 simp add: hypreal_add_commute)
-
 lemma hypreal_lt_zero_iff: "(x < (0::hypreal)) = (x < -x)"
 apply (rule hypreal_minus_zero_less_iff [THEN subst])
 apply (subst hypreal_gt_zero_iff)
 apply (simp (no_asm_use))
 done
 
-lemma hypreal_add_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 simp add: hypreal_less_def hypreal_add)
-apply (auto intro!: exI simp add: hypreal_less_def hypreal_add, ultra)
-done
-
-lemma hypreal_add_order_le: "[| 0 < x; 0 \<le> y |] ==> (0::hypreal) < x + y"
-by (auto dest: sym order_le_imp_less_or_eq intro: hypreal_add_order)
-
-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_mult_less_zero1: "[| x < 0; y < 0 |] ==> (0::hypreal) < x * y"
-apply (drule hypreal_minus_zero_less_iff [THEN iffD2])+
-apply (drule hypreal_mult_order, assumption, simp)
-done
-
-lemma hypreal_mult_less_zero: "[| 0 < x; y < 0 |] ==> x*y < (0::hypreal)"
-apply (drule hypreal_minus_zero_less_iff [THEN iffD2])
-apply (drule hypreal_mult_order, assumption)
-apply (rule hypreal_minus_zero_less_iff [THEN iffD1], simp)
-done
-
-lemma hypreal_zero_less_one: "0 < (1::hypreal)"
-apply (unfold hypreal_one_def hypreal_zero_def hypreal_less_def)
-apply (rule_tac x = "%n. 0" in exI)
-apply (rule_tac x = "%n. 1" in exI)
-apply (auto simp add: real_zero_less_one FreeUltrafilterNat_Nat_set)
-done
-
-lemma hypreal_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::hypreal) \<le> x + y"
-apply (drule order_le_imp_less_or_eq)+
-apply (auto intro: hypreal_add_order order_less_imp_le)
-done
-
-(*** Monotonicity results ***)
-
-lemma hypreal_add_right_cancel_less: "(v+z < w+z) = (v < (w::hypreal))"
-apply (simp (no_asm))
-done
-
-lemma hypreal_add_left_cancel_less: "(z+v < z+w) = (v < (w::hypreal))"
-apply (simp (no_asm))
-done
-
-declare hypreal_add_right_cancel_less [simp] 
-        hypreal_add_left_cancel_less [simp]
-
-lemma hypreal_add_right_cancel_le: "(v+z \<le> w+z) = (v \<le> (w::hypreal))"
-apply (simp (no_asm))
-done
-
-lemma hypreal_add_left_cancel_le: "(z+v \<le> z+w) = (v \<le> (w::hypreal))"
-apply (simp (no_asm))
-done
-
-declare hypreal_add_right_cancel_le [simp] hypreal_add_left_cancel_le [simp]
-
-lemma hypreal_add_less_mono: "[| (z1::hypreal) < y1; z2 < y2 |] ==> z1 + z2 < y1 + y2"
-apply (drule hypreal_less_minus_iff [THEN iffD1])
-apply (drule hypreal_less_minus_iff [THEN iffD1])
-apply (drule hypreal_add_order, assumption)
-apply (erule_tac V = "0 < y2 + - z2" in thin_rl)
-apply (drule_tac C = "z1 + z2" in hypreal_add_less_mono1)
-apply (auto simp add: hypreal_minus_add_distrib [symmetric]
-              hypreal_add_ac simp del: hypreal_minus_add_distrib)
-done
-
-lemma hypreal_add_left_le_mono1: "(q1::hypreal) \<le> q2  ==> x + q1 \<le> 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_add_le_mono1: "(q1::hypreal) \<le> q2  ==> q1 + x \<le> q2 + x"
-by (auto dest: hypreal_add_left_le_mono1 simp add: hypreal_add_commute)
-
-lemma hypreal_add_le_mono: "[|(i::hypreal)\<le>j;  k\<le>l |] ==> i + k \<le> j + l"
-apply (erule hypreal_add_le_mono1 [THEN order_trans])
-apply (simp (no_asm))
-done
-
-lemma hypreal_add_less_le_mono: "[|(i::hypreal)<j;  k\<le>l |] ==> i + k < j + l"
-by (auto dest!: order_le_imp_less_or_eq intro: hypreal_add_less_mono1 hypreal_add_less_mono)
-
-lemma hypreal_add_le_less_mono: "[|(i::hypreal)\<le>j;  k<l |] ==> i + k < j + l"
-by (auto dest!: order_le_imp_less_or_eq intro: hypreal_add_less_mono2 hypreal_add_less_mono)
-
-lemma hypreal_less_add_right_cancel: "(A::hypreal) + C < B + C ==> A < B"
-apply (simp (no_asm_use))
-done
-
-lemma hypreal_less_add_left_cancel: "(C::hypreal) + A < C + B ==> A < B"
-apply (simp (no_asm_use))
-done
-
-lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) \<le> y|] ==> r < x + y"
-by (auto dest: hypreal_add_less_le_mono)
-
-lemma hypreal_le_add_right_cancel: "!!(A::hypreal). A + C \<le> B + C ==> A \<le> B"
-apply (drule_tac x = "-C" in hypreal_add_le_mono1)
-apply (simp add: hypreal_add_assoc)
-done
-
-lemma hypreal_le_add_left_cancel: "!!(A::hypreal). C + A \<le> C + B ==> A \<le> B"
-apply (drule_tac x = "-C" in hypreal_add_left_le_mono1)
-apply (simp add: hypreal_add_assoc [symmetric])
-done
-
-lemma hypreal_le_square: "(0::hypreal) \<le> x*x"
-apply (rule_tac x = 0 and y = x in hypreal_linear_less2)
-apply (auto intro: hypreal_mult_order hypreal_mult_less_zero1 order_less_imp_le)
-done
-declare hypreal_le_square [simp]
-
-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<y |] ==> z*x<z*y"
-apply (simp (no_asm_simp) add: hypreal_mult_commute hypreal_mult_less_mono1)
-done
-
-subsection{*The Hyperreals Form an Ordered Field*}
-
-instance hypreal :: inverse ..
-
-instance hypreal :: ordered_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
-  show "x - y = x + (-y)" by (simp add: hypreal_diff_def)
-  show "(x * y) * z = x * (y * z)" by (rule hypreal_mult_assoc)
-  show "x * y = y * x" by (rule hypreal_mult_commute)
-  show "1 * x = x" by simp
-  show "(x + y) * z = x * z + y * z" by (simp add: hypreal_add_mult_distrib)
-  show "0 \<noteq> (1::hypreal)" by (rule hypreal_zero_not_eq_one)
-  show "x \<le> y ==> z + x \<le> 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 "\<bar>x\<bar> = (if x < 0 then -x else x)"
-    by (auto dest: order_le_less_trans simp add: hrabs_def linorder_not_le)
-  show "x \<noteq> 0 ==> inverse x * x = 1" by simp
-  show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: hypreal_divide_def)
-qed
-
-text{*The precondition could be weakened to @{term "0\<le>x"}*}
-lemma hypreal_mult_less_mono:
-     "[| u<v;  x<y;  (0::hypreal) < v;  0 < x |] ==> u*x < v* y"
- by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le)
-
-lemma hypreal_inverse_gt_0: "0 < x ==> 0 < inverse (x::hypreal)"
-  by (rule Ring_and_Field.positive_imp_inverse_positive)
-
-lemma hypreal_inverse_less_0: "x < 0 ==> inverse (x::hypreal) < 0"
-  by (rule Ring_and_Field.negative_imp_inverse_negative)
-
 
 (*----------------------------------------------------------------------------
                Existence of infinite hyperreal number
@@ -420,12 +386,9 @@
 val hypreal_add_less_mono1 = thm"hypreal_add_less_mono1";
 val hypreal_add_less_mono2 = thm"hypreal_add_less_mono2";
 val hypreal_lt_zero_iff = thm"hypreal_lt_zero_iff";
-val hypreal_add_order = thm"hypreal_add_order";
-val hypreal_add_order_le = thm"hypreal_add_order_le";
 val hypreal_mult_order = thm"hypreal_mult_order";
 val hypreal_mult_less_zero1 = thm"hypreal_mult_less_zero1";
 val hypreal_mult_less_zero = thm"hypreal_mult_less_zero";
-val hypreal_zero_less_one = thm"hypreal_zero_less_one";
 val hypreal_le_add_order = thm"hypreal_le_add_order";
 val hypreal_add_right_cancel_less = thm"hypreal_add_right_cancel_less";
 val hypreal_add_left_cancel_less = thm"hypreal_add_left_cancel_less";
diff -r f508492af9b4 -r 1dd7439477dd src/HOL/Real/RealOrd.thy
--- a/src/HOL/Real/RealOrd.thy	Mon Dec 22 12:50:22 2003 +0100
+++ b/src/HOL/Real/RealOrd.thy	Mon Dec 22 14:12:54 2003 +0100
@@ -163,9 +163,6 @@
 apply (simp add: real_add_mult_distrib2)
 done
 
-(** For the cancellation simproc.
-    The idea is to cancel like terms on opposite sides by subtraction **)
-
 lemma real_less_sum_gt_0_iff: "(0 < S + (-W::real)) = (W < S)"
 by (blast intro: real_less_sum_gt_zero real_sum_gt_zero_less)
 
@@ -321,16 +318,16 @@
 lemma real_le_add_left_cancel: "!!(A::real). C + A \<le> C + B ==> A \<le> B"
   by (rule (*Ring_and_Field.*)add_le_imp_le_left)
 
-lemma real_add_right_cancel_less [simp]: "(v+z < w+z) = (v < (w::real))"
+lemma real_add_right_cancel_less: "(v+z < w+z) = (v < (w::real))"
   by (rule Ring_and_Field.add_less_cancel_right)
 
-lemma real_add_left_cancel_less [simp]: "(z+v < z+w) = (v < (w::real))"
+lemma real_add_left_cancel_less: "(z+v < z+w) = (v < (w::real))"
   by (rule Ring_and_Field.add_less_cancel_left)
 
-lemma real_add_right_cancel_le [simp]: "(v+z \<le> w+z) = (v \<le> (w::real))"
+lemma real_add_right_cancel_le: "(v+z \<le> w+z) = (v \<le> (w::real))"
   by (rule Ring_and_Field.add_le_cancel_right)
 
-lemma real_add_left_cancel_le [simp]: "(z+v \<le> z+w) = (v \<le> (w::real))"
+lemma real_add_left_cancel_le: "(z+v \<le> z+w) = (v \<le> (w::real))"
   by (rule Ring_and_Field.add_le_cancel_left)
 
 
@@ -778,7 +775,6 @@
 val real_less_add_positive_left_Ex = thm"real_less_add_positive_left_Ex";
 val real_less_sum_gt_zero = thm"real_less_sum_gt_zero";
 val real_sum_gt_zero_less = thm"real_sum_gt_zero_less";
-val real_less_sum_gt_0_iff = thm"real_less_sum_gt_0_iff";
 
 val real_gt_zero_preal_Ex = thm "real_gt_zero_preal_Ex";
 val real_gt_preal_preal_Ex = thm "real_gt_preal_preal_Ex";