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