--- a/src/HOL/Ring_and_Field.thy Thu Jun 14 18:33:29 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy Thu Jun 14 18:33:31 2007 +0200
@@ -170,6 +170,7 @@
class division_by_zero = zero + inverse +
assumes inverse_zero [simp]: "inverse \<^loc>0 = \<^loc>0"
+
subsection {* Distribution rules *}
theorems ring_distrib = right_distrib left_distrib
@@ -343,6 +344,7 @@
apply (simp add: compare_rls minus_mult_left [symmetric])
done
+
subsection {* Ordering Rules for Multiplication *}
lemma mult_left_le_imp_le:
@@ -386,6 +388,7 @@
apply (simp_all add: minus_mult_right [symmetric])
done
+
subsection{* Products of Signs *}
lemma mult_pos_pos: "[| (0::'a::ordered_semiring_strict) < a; 0 < b |] ==> 0 < a*b"
@@ -501,6 +504,7 @@
lemma not_one_less_zero [simp]: "~ (1::'a::ordered_semidom) < 0"
by (simp add: linorder_not_less)
+
subsection{*More Monotonicity*}
text{*Strict monotonicity in both arguments*}
@@ -559,6 +563,7 @@
apply simp
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"},
@@ -621,7 +626,7 @@
proof (rule ccontr)
assume "~ a < b"
hence "b \<le> a" by (simp add: linorder_not_less)
- hence "c*b \<le> c*a" by (rule mult_left_mono)
+ hence "c*b \<le> c*a" using nonneg by (rule mult_left_mono)
with this and less show False
by (simp add: linorder_not_less [symmetric])
qed
@@ -632,7 +637,7 @@
proof (rule ccontr)
assume "~ a < b"
hence "b \<le> a" by (simp add: linorder_not_less)
- hence "b*c \<le> a*c" by (rule mult_right_mono)
+ hence "b*c \<le> a*c" using nonneg by (rule mult_right_mono)
with this and less show False
by (simp add: linorder_not_less [symmetric])
qed
@@ -746,6 +751,7 @@
add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
diff_eq_eq eq_diff_eq *)
+
subsection {* Fields *}
lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = 1) = (a = (b::'a::field))"
@@ -968,6 +974,7 @@
"inverse (a/b) = b / (a::'a::{field,division_by_zero})"
by (simp add: divide_inverse mult_commute)
+
subsection {* Calculations with fractions *}
lemma nonzero_mult_divide_cancel_left:
@@ -1038,6 +1045,7 @@
apply assumption
done
+
subsubsection{*Special Cancellation Simprules for Division*}
lemma mult_divide_cancel_left_if [simp]:
@@ -1136,6 +1144,7 @@
apply simp_all
done
+
subsection {* Ordered Fields *}
lemma positive_imp_inverse_positive:
@@ -1171,15 +1180,15 @@
qed
lemma inverse_positive_imp_positive:
- assumes inv_gt_0: "0 < inverse a"
- and [simp]: "a \<noteq> 0"
- shows "0 < (a::'a::ordered_field)"
- proof -
+ assumes inv_gt_0: "0 < inverse a"
+ and nz: "a \<noteq> 0"
+ shows "0 < (a::'a::ordered_field)"
+proof -
have "0 < inverse (inverse a)"
- by (rule positive_imp_inverse_positive)
+ using inv_gt_0 by (rule positive_imp_inverse_positive)
thus "0 < a"
- by (simp add: nonzero_inverse_inverse_eq)
- qed
+ using nz by (simp add: nonzero_inverse_inverse_eq)
+qed
lemma inverse_positive_iff_positive [simp]:
"(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))"
@@ -1188,15 +1197,15 @@
done
lemma inverse_negative_imp_negative:
- assumes inv_less_0: "inverse a < 0"
- and [simp]: "a \<noteq> 0"
- shows "a < (0::'a::ordered_field)"
- proof -
+ assumes inv_less_0: "inverse a < 0"
+ and nz: "a \<noteq> 0"
+ shows "a < (0::'a::ordered_field)"
+proof -
have "inverse (inverse a) < 0"
- by (rule negative_imp_inverse_negative)
+ using inv_less_0 by (rule negative_imp_inverse_negative)
thus "a < 0"
- by (simp add: nonzero_inverse_inverse_eq)
- qed
+ using nz by (simp add: nonzero_inverse_inverse_eq)
+qed
lemma inverse_negative_iff_negative [simp]:
"(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))"
@@ -1334,6 +1343,7 @@
"(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{ordered_field,division_by_zero}))"
by (simp add: linorder_not_less [symmetric] one_less_inverse_iff)
+
subsection{*Simplification of Inequalities Involving Literal Divisors*}
lemma pos_le_divide_eq: "0 < (c::'a::ordered_field) ==> (a \<le> b/c) = (a*c \<le> b)"
@@ -1500,6 +1510,7 @@
apply (erule nonzero_divide_eq_eq)
done
+
subsection{*Division and Signs*}
lemma zero_less_divide_iff:
@@ -1578,6 +1589,7 @@
apply simp
done
+
subsection{*Cancellation Laws for Division*}
lemma divide_cancel_right [simp]:
@@ -1592,6 +1604,7 @@
apply (simp add: divide_inverse field_mult_cancel_left)
done
+
subsection {* Division and the Number One *}
text{*Simplify expressions equated with 1*}
@@ -1629,6 +1642,7 @@
declare zero_le_divide_1_iff [simp]
declare divide_le_0_1_iff [simp]
+
subsection {* Ordering Rules for Division *}
lemma divide_strict_right_mono:
@@ -1706,6 +1720,7 @@
shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
by (auto simp add: divide_less_eq)
+
subsection{*Conditional Simplification Rules: No Case Splits*}
lemma le_divide_eq_1_pos [simp]:
@@ -1758,6 +1773,7 @@
shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
by (auto simp add: divide_eq_eq)
+
subsection {* Reasoning about inequalities with division *}
lemma mult_right_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
@@ -1823,6 +1839,7 @@
declare times_divide_eq [simp]
+
subsection {* Ordered Fields are Dense *}
lemma less_add_one: "a < (a+1::'a::ordered_semidom)"
@@ -1995,6 +2012,7 @@
apply (simp add: order_less_imp_le);
done;
+
subsection {* Bounds of products via negative and positive Part *}
lemma mult_le_prts:
@@ -2063,6 +2081,7 @@
then show ?thesis by simp
qed
+
subsection {* Theorems for proof tools *}
lemma add_mono_thms_ordered_semiring: