--- a/src/HOL/Real/HahnBanach/Aux.thy Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/HahnBanach/Aux.thy Sat Dec 30 22:13:18 2000 +0100
@@ -17,40 +17,40 @@
text {* \medskip Lemmas about sets. *}
-lemma Int_singletonD: "A \<inter> B = {v} \<Longrightarrow> x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x = v"
+lemma Int_singletonD: "A \\<inter> B = {v} \\<Longrightarrow> x \\<in> A \\<Longrightarrow> x \\<in> B \\<Longrightarrow> x = v"
by (fast elim: equalityE)
-lemma set_less_imp_diff_not_empty: "H < E \<Longrightarrow> \<exists>x0 \<in> E. x0 \<notin> H"
+lemma set_less_imp_diff_not_empty: "H < E \\<Longrightarrow> \\<exists>x0 \\<in> E. x0 \\<notin> H"
by (auto simp add: psubset_eq)
text{* \medskip Some lemmas about orders. *}
-lemma lt_imp_not_eq: "x < (y::'a::order) \<Longrightarrow> x \<noteq> y"
+lemma lt_imp_not_eq: "x < (y::'a::order) \\<Longrightarrow> x \\<noteq> y"
by (simp add: order_less_le)
lemma le_noteq_imp_less:
- "x \<le> (r::'a::order) \<Longrightarrow> x \<noteq> r \<Longrightarrow> x < r"
+ "x \\<le> (r::'a::order) \\<Longrightarrow> x \\<noteq> r \\<Longrightarrow> x < r"
proof -
- assume "x \<le> r" and ne:"x \<noteq> r"
- hence "x < r \<or> x = r" by (simp add: order_le_less)
+ assume "x \\<le> r" and ne:"x \\<noteq> r"
+ hence "x < r \\<or> x = r" by (simp add: order_le_less)
with ne show ?thesis by simp
qed
text {* \medskip Some lemmas for the reals. *}
-lemma real_add_minus_eq: "x - y = (#0::real) \<Longrightarrow> x = y"
+lemma real_add_minus_eq: "x - y = (#0::real) \\<Longrightarrow> x = y"
by simp
lemma abs_minus_one: "abs (- (#1::real)) = #1"
by simp
lemma real_mult_le_le_mono1a:
- "(#0::real) \<le> z \<Longrightarrow> x \<le> y \<Longrightarrow> z * x \<le> z * y"
+ "(#0::real) \\<le> z \\<Longrightarrow> x \\<le> y \\<Longrightarrow> z * x \\<le> z * y"
proof -
- assume z: "(#0::real) \<le> z" and "x \<le> y"
- hence "x < y \<or> x = y" by (auto simp add: order_le_less)
+ assume z: "(#0::real) \\<le> z" and "x \\<le> y"
+ hence "x < y \\<or> x = y" by (auto simp add: order_le_less)
thus ?thesis
proof
assume "x < y" show ?thesis by (rule real_mult_le_less_mono2) simp
@@ -60,10 +60,10 @@
qed
lemma real_mult_le_le_mono2:
- "(#0::real) \<le> z \<Longrightarrow> x \<le> y \<Longrightarrow> x * z \<le> y * z"
+ "(#0::real) \\<le> z \\<Longrightarrow> x \\<le> y \\<Longrightarrow> x * z \\<le> y * z"
proof -
- assume "(#0::real) \<le> z" "x \<le> y"
- hence "x < y \<or> x = y" by (auto simp add: order_le_less)
+ assume "(#0::real) \\<le> z" "x \\<le> y"
+ hence "x < y \\<or> x = y" by (auto simp add: order_le_less)
thus ?thesis
proof
assume "x < y"
@@ -75,29 +75,29 @@
qed
lemma real_mult_less_le_anti:
- "z < (#0::real) \<Longrightarrow> x \<le> y \<Longrightarrow> z * y \<le> z * x"
+ "z < (#0::real) \\<Longrightarrow> x \\<le> y \\<Longrightarrow> z * y \\<le> z * x"
proof -
- assume "z < #0" "x \<le> y"
+ assume "z < #0" "x \\<le> y"
hence "#0 < - z" by simp
- hence "#0 \<le> - z" by (rule real_less_imp_le)
- hence "x * (- z) \<le> y * (- z)"
+ hence "#0 \\<le> - z" by (rule order_less_imp_le)
+ hence "x * (- z) \\<le> y * (- z)"
by (rule real_mult_le_le_mono2)
- hence "- (x * z) \<le> - (y * z)"
+ hence "- (x * z) \\<le> - (y * z)"
by (simp only: real_minus_mult_eq2)
thus ?thesis by (simp only: real_mult_commute)
qed
lemma real_mult_less_le_mono:
- "(#0::real) < z \<Longrightarrow> x \<le> y \<Longrightarrow> z * x \<le> z * y"
+ "(#0::real) < z \\<Longrightarrow> x \\<le> y \\<Longrightarrow> z * x \\<le> z * y"
proof -
- assume "#0 < z" "x \<le> y"
- have "#0 \<le> z" by (rule real_less_imp_le)
- hence "x * z \<le> y * z"
+ assume "#0 < z" "x \\<le> y"
+ have "#0 \\<le> z" by (rule order_less_imp_le)
+ hence "x * z \\<le> y * z"
by (rule real_mult_le_le_mono2)
thus ?thesis by (simp only: real_mult_commute)
qed
-lemma real_inverse_gt_zero1: "#0 < (x::real) \<Longrightarrow> #0 < inverse x"
+lemma real_inverse_gt_zero1: "#0 < (x::real) \\<Longrightarrow> #0 < inverse x"
proof -
assume "#0 < x"
have "0 < x" by simp
@@ -105,17 +105,17 @@
thus ?thesis by simp
qed
-lemma real_mult_inv_right1: "(x::real) \<noteq> #0 \<Longrightarrow> x * inverse x = #1"
+lemma real_mult_inv_right1: "(x::real) \\<noteq> #0 \\<Longrightarrow> x * inverse x = #1"
by simp
-lemma real_mult_inv_left1: "(x::real) \<noteq> #0 \<Longrightarrow> inverse x * x = #1"
+lemma real_mult_inv_left1: "(x::real) \\<noteq> #0 \\<Longrightarrow> inverse x * x = #1"
by simp
lemma real_le_mult_order1a:
- "(#0::real) \<le> x \<Longrightarrow> #0 \<le> y \<Longrightarrow> #0 \<le> x * y"
+ "(#0::real) \\<le> x \\<Longrightarrow> #0 \\<le> y \\<Longrightarrow> #0 \\<le> x * y"
proof -
- assume "#0 \<le> x" "#0 \<le> y"
- have "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x * y"
+ assume "#0 \\<le> x" "#0 \\<le> y"
+ have "0 \\<le> x \\<Longrightarrow> 0 \\<le> y \\<Longrightarrow> 0 \\<le> x * y"
by (rule real_le_mult_order)
thus ?thesis by (simp!)
qed
@@ -141,11 +141,11 @@
finally show ?thesis .
qed
-lemma real_minus_le: "- (x::real) \<le> y \<Longrightarrow> - y \<le> x"
+lemma real_minus_le: "- (x::real) \\<le> y \\<Longrightarrow> - y \\<le> x"
by simp
lemma real_diff_ineq_swap:
- "(d::real) - b \<le> c + a \<Longrightarrow> - a - b \<le> c - d"
+ "(d::real) - b \\<le> c + a \\<Longrightarrow> - a - b \\<le> c - d"
by simp
end
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Sat Dec 30 22:13:18 2000 +0100
@@ -10,10 +10,10 @@
subsection {* Continuous linear forms*}
text {*
- A linear form @{text f} on a normed vector space @{text "(V, \<parallel>\<cdot>\<parallel>)"}
+ A linear form @{text f} on a normed vector space @{text "(V, \\<parallel>\\<cdot>\\<parallel>)"}
is \emph{continuous}, iff it is bounded, i.~e.
\begin{center}
- @{text "\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+ @{text "\\<exists>c \\<in> R. \\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c \\<cdot> \\<parallel>x\\<parallel>"}
\end{center}
In our application no other functions than linear forms are
considered, so we can define continuous linear forms as bounded
@@ -22,25 +22,25 @@
constdefs
is_continuous ::
- "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
- "is_continuous V norm f \<equiv>
- is_linearform V f \<and> (\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x)"
+ "'a::{plus, minus, zero} set \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> bool"
+ "is_continuous V norm f \\<equiv>
+ is_linearform V f \\<and> (\\<exists>c. \\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x)"
lemma continuousI [intro]:
- "is_linearform V f \<Longrightarrow> (\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * norm x)
- \<Longrightarrow> is_continuous V norm f"
+ "is_linearform V f \\<Longrightarrow> (\\<And>x. x \\<in> V \\<Longrightarrow> \\<bar>f x\\<bar> \\<le> c * norm x)
+ \\<Longrightarrow> is_continuous V norm f"
proof (unfold is_continuous_def, intro exI conjI ballI)
- assume r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * norm x"
- fix x assume "x \<in> V" show "\<bar>f x\<bar> \<le> c * norm x" by (rule r)
+ assume r: "\\<And>x. x \\<in> V \\<Longrightarrow> \\<bar>f x\\<bar> \\<le> c * norm x"
+ fix x assume "x \\<in> V" show "\\<bar>f x\\<bar> \\<le> c * norm x" by (rule r)
qed
lemma continuous_linearform [intro?]:
- "is_continuous V norm f \<Longrightarrow> is_linearform V f"
+ "is_continuous V norm f \\<Longrightarrow> is_linearform V f"
by (unfold is_continuous_def) blast
lemma continuous_bounded [intro?]:
"is_continuous V norm f
- \<Longrightarrow> \<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
+ \\<Longrightarrow> \\<exists>c. \\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x"
by (unfold is_continuous_def) blast
subsection{* The norm of a linear form *}
@@ -49,34 +49,34 @@
text {*
The least real number @{text c} for which holds
\begin{center}
- @{text "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+ @{text "\\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c \\<cdot> \\<parallel>x\\<parallel>"}
\end{center}
is called the \emph{norm} of @{text f}.
- For non-trivial vector spaces @{text "V \<noteq> {0}"} the norm can be
+ For non-trivial vector spaces @{text "V \\<noteq> {0}"} the norm can be
defined as
\begin{center}
- @{text "\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>"}
+ @{text "\\<parallel>f\\<parallel> = \<sup>x \\<noteq> 0. \\<bar>f x\\<bar> / \\<parallel>x\\<parallel>"}
\end{center}
For the case @{text "V = {0}"} the supremum would be taken from an
- empty set. Since @{text \<real>} is unbounded, there would be no supremum.
+ empty set. Since @{text \\<real>} is unbounded, there would be no supremum.
To avoid this situation it must be guaranteed that there is an
- element in this set. This element must be @{text "{} \<ge> 0"} so that
+ element in this set. This element must be @{text "{} \\<ge> 0"} so that
@{text function_norm} has the norm properties. Furthermore
it does not have to change the norm in all other cases, so it must
- be @{text 0}, as all other elements of are @{text "{} \<ge> 0"}.
+ be @{text 0}, as all other elements of are @{text "{} \\<ge> 0"}.
Thus we define the set @{text B} the supremum is taken from as
\begin{center}
- @{text "{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}"}
+ @{text "{0} \\<union> {\\<bar>f x\\<bar> / \\<parallel>x\\<parallel>. x \\<noteq> 0 \\<and> x \\<in> F}"}
\end{center}
*}
constdefs
- B :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a::{plus, minus, zero} \<Rightarrow> real) \<Rightarrow> real set"
- "B V norm f \<equiv>
- {#0} \<union> {\<bar>f x\<bar> * inverse (norm x) | x. x \<noteq> 0 \<and> x \<in> V}"
+ B :: "'a set \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> ('a::{plus, minus, zero} \\<Rightarrow> real) \\<Rightarrow> real set"
+ "B V norm f \\<equiv>
+ {#0} \\<union> {\\<bar>f x\\<bar> * inverse (norm x) | x. x \\<noteq> 0 \\<and> x \\<in> V}"
text {*
@{text n} is the function norm of @{text f}, iff @{text n} is the
@@ -85,8 +85,8 @@
constdefs
is_function_norm ::
- "('a::{minus,plus,zero} \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> bool"
- "is_function_norm f V norm fn \<equiv> is_Sup UNIV (B V norm f) fn"
+ "('a::{minus,plus,zero} \\<Rightarrow> real) \\<Rightarrow> 'a set \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> real \\<Rightarrow> bool"
+ "is_function_norm f V norm fn \\<equiv> is_Sup UNIV (B V norm f) fn"
text {*
@{text function_norm} is equal to the supremum of @{text B}, if the
@@ -94,159 +94,159 @@
*}
constdefs
- function_norm :: "('a::{minus,plus,zero} \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> real"
- "function_norm f V norm \<equiv> Sup UNIV (B V norm f)"
+ function_norm :: "('a::{minus,plus,zero} \\<Rightarrow> real) \\<Rightarrow> 'a set \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> real"
+ "function_norm f V norm \\<equiv> Sup UNIV (B V norm f)"
syntax
- function_norm :: "('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> real" ("\<parallel>_\<parallel>_,_")
+ function_norm :: "('a \\<Rightarrow> real) \\<Rightarrow> 'a set \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> real" ("\\<parallel>_\\<parallel>_,_")
-lemma B_not_empty: "#0 \<in> B V norm f"
+lemma B_not_empty: "#0 \\<in> B V norm f"
by (unfold B_def) blast
text {*
The following lemma states that every continuous linear form on a
- normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
+ normed space @{text "(V, \\<parallel>\\<cdot>\\<parallel>)"} has a function norm.
*}
lemma ex_fnorm [intro?]:
- "is_normed_vectorspace V norm \<Longrightarrow> is_continuous V norm f
- \<Longrightarrow> is_function_norm f V norm \<parallel>f\<parallel>V,norm"
+ "is_normed_vectorspace V norm \\<Longrightarrow> is_continuous V norm f
+ \\<Longrightarrow> is_function_norm f V norm \\<parallel>f\\<parallel>V,norm"
proof (unfold function_norm_def is_function_norm_def
is_continuous_def Sup_def, elim conjE, rule someI2_ex)
assume "is_normed_vectorspace V norm"
assume "is_linearform V f"
- and e: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
+ and e: "\\<exists>c. \\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x"
txt {* The existence of the supremum is shown using the
completeness of the reals. Completeness means, that
every non-empty bounded set of reals has a
supremum. *}
- show "\<exists>a. is_Sup UNIV (B V norm f) a"
+ show "\\<exists>a. is_Sup UNIV (B V norm f) a"
proof (unfold is_Sup_def, rule reals_complete)
txt {* First we have to show that @{text B} is non-empty: *}
- show "\<exists>X. X \<in> B V norm f"
+ show "\\<exists>X. X \\<in> B V norm f"
proof
- show "#0 \<in> (B V norm f)" by (unfold B_def) blast
+ show "#0 \\<in> (B V norm f)" by (unfold B_def) blast
qed
txt {* Then we have to show that @{text B} is bounded: *}
- from e show "\<exists>Y. isUb UNIV (B V norm f) Y"
+ from e show "\\<exists>Y. isUb UNIV (B V norm f) Y"
proof
txt {* We know that @{text f} is bounded by some value @{text c}. *}
- fix c assume a: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
- def b \<equiv> "max c #0"
+ fix c assume a: "\\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x"
+ def b \\<equiv> "max c #0"
show "?thesis"
proof (intro exI isUbI setleI ballI, unfold B_def,
elim UnE CollectE exE conjE singletonE)
txt {* To proof the thesis, we have to show that there is some
- constant @{text b}, such that @{text "y \<le> b"} for all
- @{text "y \<in> B"}. Due to the definition of @{text B} there are
- two cases for @{text "y \<in> B"}. If @{text "y = 0"} then
- @{text "y \<le> max c 0"}: *}
+ constant @{text b}, such that @{text "y \\<le> b"} for all
+ @{text "y \\<in> B"}. Due to the definition of @{text B} there are
+ two cases for @{text "y \\<in> B"}. If @{text "y = 0"} then
+ @{text "y \\<le> max c 0"}: *}
fix y assume "y = (#0::real)"
- show "y \<le> b" by (simp! add: le_maxI2)
+ show "y \\<le> b" by (simp! add: le_maxI2)
- txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
- @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
+ txt {* The second case is @{text "y = \\<bar>f x\\<bar> / \\<parallel>x\\<parallel>"} for some
+ @{text "x \\<in> V"} with @{text "x \\<noteq> 0"}. *}
next
fix x y
- assume "x \<in> V" "x \<noteq> 0"
+ assume "x \\<in> V" "x \\<noteq> 0"
txt {* The thesis follows by a short calculation using the
fact that @{text f} is bounded. *}
- assume "y = \<bar>f x\<bar> * inverse (norm x)"
- also have "... \<le> c * norm x * inverse (norm x)"
+ assume "y = \\<bar>f x\\<bar> * inverse (norm x)"
+ also have "... \\<le> c * norm x * inverse (norm x)"
proof (rule real_mult_le_le_mono2)
- show "#0 \<le> inverse (norm x)"
- by (rule real_less_imp_le, rule real_inverse_gt_zero1,
+ show "#0 \\<le> inverse (norm x)"
+ by (rule order_less_imp_le, rule real_inverse_gt_zero1,
rule normed_vs_norm_gt_zero)
- from a show "\<bar>f x\<bar> \<le> c * norm x" ..
+ from a show "\\<bar>f x\\<bar> \\<le> c * norm x" ..
qed
also have "... = c * (norm x * inverse (norm x))"
by (rule real_mult_assoc)
also have "(norm x * inverse (norm x)) = (#1::real)"
proof (rule real_mult_inv_right1)
- show nz: "norm x \<noteq> #0"
+ show nz: "norm x \\<noteq> #0"
by (rule not_sym, rule lt_imp_not_eq,
rule normed_vs_norm_gt_zero)
qed
- also have "c * ... \<le> b " by (simp! add: le_maxI1)
- finally show "y \<le> b" .
+ also have "c * ... \\<le> b " by (simp! add: le_maxI1)
+ finally show "y \\<le> b" .
qed simp
qed
qed
qed
-text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
+text {* The norm of a continuous function is always @{text "\\<ge> 0"}. *}
lemma fnorm_ge_zero [intro?]:
- "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm
- \<Longrightarrow> #0 \<le> \<parallel>f\<parallel>V,norm"
+ "is_continuous V norm f \\<Longrightarrow> is_normed_vectorspace V norm
+ \\<Longrightarrow> #0 \\<le> \\<parallel>f\\<parallel>V,norm"
proof -
assume c: "is_continuous V norm f"
and n: "is_normed_vectorspace V norm"
txt {* The function norm is defined as the supremum of @{text B}.
- So it is @{text "\<ge> 0"} if all elements in @{text B} are
- @{text "\<ge> 0"}, provided the supremum exists and @{text B} is not
+ So it is @{text "\\<ge> 0"} if all elements in @{text B} are
+ @{text "\\<ge> 0"}, provided the supremum exists and @{text B} is not
empty. *}
show ?thesis
proof (unfold function_norm_def, rule sup_ub1)
- show "\<forall>x \<in> (B V norm f). #0 \<le> x"
+ show "\\<forall>x \\<in> (B V norm f). #0 \\<le> x"
proof (intro ballI, unfold B_def,
elim UnE singletonE CollectE exE conjE)
fix x r
- assume "x \<in> V" "x \<noteq> 0"
- and r: "r = \<bar>f x\<bar> * inverse (norm x)"
+ assume "x \\<in> V" "x \\<noteq> 0"
+ and r: "r = \\<bar>f x\\<bar> * inverse (norm x)"
- have ge: "#0 \<le> \<bar>f x\<bar>" by (simp! only: abs_ge_zero)
- have "#0 \<le> inverse (norm x)"
- by (rule real_less_imp_le, rule real_inverse_gt_zero1, rule)(***
- proof (rule real_less_imp_le);
+ have ge: "#0 \\<le> \\<bar>f x\\<bar>" by (simp! only: abs_ge_zero)
+ have "#0 \\<le> inverse (norm x)"
+ by (rule order_less_imp_le, rule real_inverse_gt_zero1, rule)(***
+ proof (rule order_less_imp_le);
show "#0 < inverse (norm x)";
proof (rule real_inverse_gt_zero);
show "#0 < norm x"; ..;
qed;
qed; ***)
- with ge show "#0 \<le> r"
+ with ge show "#0 \\<le> r"
by (simp only: r, rule real_le_mult_order1a)
qed (simp!)
txt {* Since @{text f} is continuous the function norm exists: *}
- have "is_function_norm f V norm \<parallel>f\<parallel>V,norm" ..
+ have "is_function_norm f V norm \\<parallel>f\\<parallel>V,norm" ..
thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
by (unfold is_function_norm_def function_norm_def)
txt {* @{text B} is non-empty by construction: *}
- show "#0 \<in> B V norm f" by (rule B_not_empty)
+ show "#0 \\<in> B V norm f" by (rule B_not_empty)
qed
qed
text {*
\medskip The fundamental property of function norms is:
\begin{center}
- @{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
+ @{text "\\<bar>f x\\<bar> \\<le> \\<parallel>f\\<parallel> \\<cdot> \\<parallel>x\\<parallel>"}
\end{center}
*}
lemma norm_fx_le_norm_f_norm_x:
- "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm \<Longrightarrow> x \<in> V
- \<Longrightarrow> \<bar>f x\<bar> \<le> \<parallel>f\<parallel>V,norm * norm x"
+ "is_continuous V norm f \\<Longrightarrow> is_normed_vectorspace V norm \\<Longrightarrow> x \\<in> V
+ \\<Longrightarrow> \\<bar>f x\\<bar> \\<le> \\<parallel>f\\<parallel>V,norm * norm x"
proof -
- assume "is_normed_vectorspace V norm" "x \<in> V"
+ assume "is_normed_vectorspace V norm" "x \\<in> V"
and c: "is_continuous V norm f"
have v: "is_vectorspace V" ..
@@ -260,46 +260,46 @@
@{text "f 0 = 0"}. *}
assume "x = 0"
- have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by (simp!)
+ have "\\<bar>f x\\<bar> = \\<bar>f 0\\<bar>" by (simp!)
also from v continuous_linearform have "f 0 = #0" ..
also note abs_zero
- also have "#0 \<le> \<parallel>f\<parallel>V,norm * norm x"
+ also have "#0 \\<le> \\<parallel>f\\<parallel>V,norm * norm x"
proof (rule real_le_mult_order1a)
- show "#0 \<le> \<parallel>f\<parallel>V,norm" ..
- show "#0 \<le> norm x" ..
+ show "#0 \\<le> \\<parallel>f\\<parallel>V,norm" ..
+ show "#0 \\<le> norm x" ..
qed
finally
- show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>V,norm * norm x" .
+ show "\\<bar>f x\\<bar> \\<le> \\<parallel>f\\<parallel>V,norm * norm x" .
next
- assume "x \<noteq> 0"
+ assume "x \\<noteq> 0"
have n: "#0 < norm x" ..
- hence nz: "norm x \<noteq> #0"
+ hence nz: "norm x \\<noteq> #0"
by (simp only: lt_imp_not_eq)
- txt {* For the case @{text "x \<noteq> 0"} we derive the following fact
+ txt {* For the case @{text "x \\<noteq> 0"} we derive the following fact
from the definition of the function norm:*}
- have l: "\<bar>f x\<bar> * inverse (norm x) \<le> \<parallel>f\<parallel>V,norm"
+ have l: "\\<bar>f x\\<bar> * inverse (norm x) \\<le> \\<parallel>f\\<parallel>V,norm"
proof (unfold function_norm_def, rule sup_ub)
from ex_fnorm [OF _ c]
show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
by (simp! add: is_function_norm_def function_norm_def)
- show "\<bar>f x\<bar> * inverse (norm x) \<in> B V norm f"
+ show "\\<bar>f x\\<bar> * inverse (norm x) \\<in> B V norm f"
by (unfold B_def, intro UnI2 CollectI exI [of _ x]
conjI, simp)
qed
txt {* The thesis now follows by a short calculation: *}
- have "\<bar>f x\<bar> = \<bar>f x\<bar> * #1" by (simp!)
+ have "\\<bar>f x\\<bar> = \\<bar>f x\\<bar> * #1" by (simp!)
also from nz have "#1 = inverse (norm x) * norm x"
by (simp add: real_mult_inv_left1)
- also have "\<bar>f x\<bar> * ... = \<bar>f x\<bar> * inverse (norm x) * norm x"
+ also have "\\<bar>f x\\<bar> * ... = \\<bar>f x\\<bar> * inverse (norm x) * norm x"
by (simp! add: real_mult_assoc)
- also from n l have "... \<le> \<parallel>f\<parallel>V,norm * norm x"
+ also from n l have "... \\<le> \\<parallel>f\\<parallel>V,norm * norm x"
by (simp add: real_mult_le_le_mono2)
- finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>V,norm * norm x" .
+ finally show "\\<bar>f x\\<bar> \\<le> \\<parallel>f\\<parallel>V,norm * norm x" .
qed
qed
@@ -307,72 +307,72 @@
\medskip The function norm is the least positive real number for
which the following inequation holds:
\begin{center}
- @{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+ @{text "\\<bar>f x\\<bar> \\<le> c \\<cdot> \\<parallel>x\\<parallel>"}
\end{center}
*}
lemma fnorm_le_ub:
- "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm \<Longrightarrow>
- \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x \<Longrightarrow> #0 \<le> c
- \<Longrightarrow> \<parallel>f\<parallel>V,norm \<le> c"
+ "is_continuous V norm f \\<Longrightarrow> is_normed_vectorspace V norm \\<Longrightarrow>
+ \\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x \\<Longrightarrow> #0 \\<le> c
+ \\<Longrightarrow> \\<parallel>f\\<parallel>V,norm \\<le> c"
proof (unfold function_norm_def)
assume "is_normed_vectorspace V norm"
assume c: "is_continuous V norm f"
- assume fb: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
- and "#0 \<le> c"
+ assume fb: "\\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x"
+ and "#0 \\<le> c"
- txt {* Suppose the inequation holds for some @{text "c \<ge> 0"}. If
+ txt {* Suppose the inequation holds for some @{text "c \\<ge> 0"}. If
@{text c} is an upper bound of @{text B}, then @{text c} is greater
than the function norm since the function norm is the least upper
bound. *}
- show "Sup UNIV (B V norm f) \<le> c"
+ show "Sup UNIV (B V norm f) \\<le> c"
proof (rule sup_le_ub)
from ex_fnorm [OF _ c]
show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
by (simp! add: is_function_norm_def function_norm_def)
txt {* @{text c} is an upper bound of @{text B}, i.e. every
- @{text "y \<in> B"} is less than @{text c}. *}
+ @{text "y \\<in> B"} is less than @{text c}. *}
show "isUb UNIV (B V norm f) c"
proof (intro isUbI setleI ballI)
- fix y assume "y \<in> B V norm f"
- thus le: "y \<le> c"
+ fix y assume "y \\<in> B V norm f"
+ thus le: "y \\<le> c"
proof (unfold B_def, elim UnE CollectE exE conjE singletonE)
- txt {* The first case for @{text "y \<in> B"} is @{text "y = 0"}. *}
+ txt {* The first case for @{text "y \\<in> B"} is @{text "y = 0"}. *}
assume "y = #0"
- show "y \<le> c" by (blast!)
+ show "y \\<le> c" by (blast!)
- txt{* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
- @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
+ txt{* The second case is @{text "y = \\<bar>f x\\<bar> / \\<parallel>x\\<parallel>"} for some
+ @{text "x \\<in> V"} with @{text "x \\<noteq> 0"}. *}
next
fix x
- assume "x \<in> V" "x \<noteq> 0"
+ assume "x \\<in> V" "x \\<noteq> 0"
have lz: "#0 < norm x"
by (simp! add: normed_vs_norm_gt_zero)
- have nz: "norm x \<noteq> #0"
+ have nz: "norm x \\<noteq> #0"
proof (rule not_sym)
- from lz show "#0 \<noteq> norm x"
+ from lz show "#0 \\<noteq> norm x"
by (simp! add: order_less_imp_not_eq)
qed
from lz have "#0 < inverse (norm x)"
by (simp! add: real_inverse_gt_zero1)
- hence inverse_gez: "#0 \<le> inverse (norm x)"
- by (rule real_less_imp_le)
+ hence inverse_gez: "#0 \\<le> inverse (norm x)"
+ by (rule order_less_imp_le)
- assume "y = \<bar>f x\<bar> * inverse (norm x)"
- also from inverse_gez have "... \<le> c * norm x * inverse (norm x)"
+ assume "y = \\<bar>f x\\<bar> * inverse (norm x)"
+ also from inverse_gez have "... \\<le> c * norm x * inverse (norm x)"
proof (rule real_mult_le_le_mono2)
- show "\<bar>f x\<bar> \<le> c * norm x" by (rule bspec)
+ show "\\<bar>f x\\<bar> \\<le> c * norm x" by (rule bspec)
qed
- also have "... \<le> c" by (simp add: nz real_mult_assoc)
+ also have "... \\<le> c" by (simp add: nz real_mult_assoc)
finally show ?thesis .
qed
qed blast
--- a/src/HOL/Real/HahnBanach/ROOT.ML Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/HahnBanach/ROOT.ML Sat Dec 30 22:13:18 2000 +0100
@@ -5,4 +5,4 @@
The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
*)
-time_use_thy "HahnBanach";
+with_path "../../Hyperreal" time_use_thy "HahnBanach";
--- a/src/HOL/Real/PNat.ML Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/PNat.ML Sat Dec 30 22:13:18 2000 +0100
@@ -232,18 +232,6 @@
(*** pnat_less ***)
-Goalw [pnat_less_def]
- "[| x < (y::pnat); y < z |] ==> x < z";
-by ((etac less_trans 1) THEN assume_tac 1);
-qed "pnat_less_trans";
-
-Goalw [pnat_less_def] "x < (y::pnat) ==> ~ y < x";
-by (etac less_not_sym 1);
-qed "pnat_less_not_sym";
-
-(* [| x < y; ~P ==> y < x |] ==> P *)
-bind_thm ("pnat_less_asym", pnat_less_not_sym RS contrapos_np);
-
Goalw [pnat_less_def] "~ y < (y::pnat)";
by Auto_tac;
qed "pnat_less_not_refl";
@@ -296,77 +284,6 @@
(*** pnat_le ***)
-Goalw [pnat_le_def] "~ (x::pnat) < y ==> y <= x";
-by (assume_tac 1);
-qed "pnat_leI";
-
-Goalw [pnat_le_def] "(x::pnat) <= y ==> ~ y < x";
-by (assume_tac 1);
-qed "pnat_leD";
-
-bind_thm ("pnat_leE", make_elim pnat_leD);
-
-Goal "(~ (x::pnat) < y) = (y <= x)";
-by (blast_tac (claset() addIs [pnat_leI] addEs [pnat_leE]) 1);
-qed "pnat_not_less_iff_le";
-
-Goalw [pnat_le_def] "~(x::pnat) <= y ==> y < x";
-by (Blast_tac 1);
-qed "pnat_not_leE";
-
-Goalw [pnat_le_def] "(x::pnat) < y ==> x <= y";
-by (blast_tac (claset() addEs [pnat_less_asym]) 1);
-qed "pnat_less_imp_le";
-
-(** Equivalence of m<=n and m<n | m=n **)
-
-Goalw [pnat_le_def] "m <= n ==> m < n | m=(n::pnat)";
-by (cut_facts_tac [pnat_less_linear] 1);
-by (blast_tac (claset() addEs [pnat_less_irrefl,pnat_less_asym]) 1);
-qed "pnat_le_imp_less_or_eq";
-
-Goalw [pnat_le_def] "m<n | m=n ==> m <=(n::pnat)";
-by (cut_facts_tac [pnat_less_linear] 1);
-by (blast_tac (claset() addSEs [pnat_less_irrefl] addEs [pnat_less_asym]) 1);
-qed "pnat_less_or_eq_imp_le";
-
-Goal "(m <= (n::pnat)) = (m < n | m=n)";
-by (REPEAT(ares_tac [iffI,pnat_less_or_eq_imp_le,pnat_le_imp_less_or_eq] 1));
-qed "pnat_le_eq_less_or_eq";
-
-Goal "n <= (n::pnat)";
-by (simp_tac (simpset() addsimps [pnat_le_eq_less_or_eq]) 1);
-qed "pnat_le_refl";
-
-Goal "[| i < j; j <= k |] ==> i < (k::pnat)";
-by (dtac pnat_le_imp_less_or_eq 1);
-by (blast_tac (claset() addIs [pnat_less_trans]) 1);
-qed "pnat_less_le_trans";
-
-Goal "[| i <= j; j <= k |] ==> i <= (k::pnat)";
-by (EVERY1[dtac pnat_le_imp_less_or_eq,
- dtac pnat_le_imp_less_or_eq,
- rtac pnat_less_or_eq_imp_le,
- blast_tac (claset() addIs [pnat_less_trans])]);
-qed "pnat_le_trans";
-
-Goal "[| m <= n; n <= m |] ==> m = (n::pnat)";
-by (EVERY1[dtac pnat_le_imp_less_or_eq,
- dtac pnat_le_imp_less_or_eq,
- blast_tac (claset() addIs [pnat_less_asym])]);
-qed "pnat_le_anti_sym";
-
-Goal "(m::pnat) < n = (m <= n & m ~= n)";
-by (rtac iffI 1);
-by (rtac conjI 1);
-by (etac pnat_less_imp_le 1);
-by (etac pnat_less_not_refl2 1);
-by (blast_tac (claset() addSDs [pnat_le_imp_less_or_eq]) 1);
-qed "pnat_less_le";
-
-
-(***) (***) (***) (***) (***) (***) (***) (***)
-
(*** alternative definition for pnat_le ***)
Goalw [pnat_le_def,pnat_less_def]
"((m::pnat) <= n) = (Rep_pnat m <= Rep_pnat n)";
@@ -403,7 +320,7 @@
Goal "m + k <= n --> m <= (n::pnat)";
by (simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le,
- sum_Rep_pnat_sum RS sym]) 1);
+ sum_Rep_pnat_sum RS sym]) 1);
qed_spec_mp "pnat_add_leD1";
Goal "!!n::pnat. m + k <= n ==> k <= n";
@@ -448,39 +365,6 @@
(*** Monotonicity of Addition ***)
-(*strict, in 1st argument*)
-Goalw [pnat_less_def] "!!i j k::pnat. i < j ==> i + k < j + k";
-by (auto_tac (claset() addIs [add_less_mono1],
- simpset() addsimps [sum_Rep_pnat_sum RS sym]));
-qed "pnat_add_less_mono1";
-
-Goalw [pnat_less_def] "!!i j k::pnat. [|i < j; k < l|] ==> i + k < j + l";
-by (auto_tac (claset() addIs [add_less_mono],
- simpset() addsimps [sum_Rep_pnat_sum RS sym]));
-qed "pnat_add_less_mono";
-
-Goalw [pnat_less_def]
-"!!f. [| !!i j::pnat. i<j ==> f(i) < f(j); \
-\ i <= j \
-\ |] ==> f(i) <= (f(j)::pnat)";
-by (auto_tac (claset() addSDs [inj_Rep_pnat RS injD],
- simpset() addsimps [pnat_le_iff_Rep_pnat_le,
- order_le_less]));
-qed "pnat_less_mono_imp_le_mono";
-
-Goal "!!i j k::pnat. i<=j ==> i + k <= j + k";
-by (res_inst_tac [("f", "%j. j+k")] pnat_less_mono_imp_le_mono 1);
-by (etac pnat_add_less_mono1 1);
-by (assume_tac 1);
-qed "pnat_add_le_mono1";
-
-Goal "!!k l::pnat. [|i<=j; k<=l |] ==> i + k <= j + l";
-by (etac (pnat_add_le_mono1 RS pnat_le_trans) 1);
-by (simp_tac (simpset() addsimps [pnat_add_commute]) 1);
-(*j moves to the end because it is free while k, l are bound*)
-by (etac pnat_add_le_mono1 1);
-qed "pnad_add_le_mono";
-
Goal "1 * Rep_pnat n = Rep_pnat n";
by (Asm_simp_tac 1);
qed "Rep_pnat_mult_1";
@@ -489,8 +373,7 @@
by (Asm_simp_tac 1);
qed "Rep_pnat_mult_1_right";
-Goal
- "(Rep_pnat x * Rep_pnat y): pnat";
+Goal "(Rep_pnat x * Rep_pnat y): pnat";
by (cut_facts_tac [[Rep_pnat_gt_zero,
Rep_pnat_gt_zero] MRS mult_less_mono1,Collect_pnat_gt_0] 1);
by (etac ssubst 1);
@@ -499,8 +382,7 @@
Goalw [pnat_mult_def]
"Rep_pnat x * Rep_pnat y = Rep_pnat (x * y)";
-by (simp_tac (simpset() addsimps [mult_Rep_pnat RS
- Abs_pnat_inverse]) 1);
+by (simp_tac (simpset() addsimps [mult_Rep_pnat RS Abs_pnat_inverse]) 1);
qed "mult_Rep_pnat_mult";
Goalw [pnat_mult_def] "m * n = n * (m::pnat)";
--- a/src/HOL/Real/PRat.ML Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/PRat.ML Sat Dec 30 22:13:18 2000 +0100
@@ -614,21 +614,11 @@
by (fast_tac (claset() addIs [prat_less_trans]) 1);
qed "prat_le_less_trans";
-Goal "!! (i::prat). [| i < j; j <= k |] ==> i < k";
-by (dtac prat_le_imp_less_or_eq 1);
-by (fast_tac (claset() addIs [prat_less_trans]) 1);
-qed "prat_less_le_trans";
-
Goal "[| i <= j; j <= k |] ==> i <= (k::prat)";
by (EVERY1 [dtac prat_le_imp_less_or_eq, dtac prat_le_imp_less_or_eq,
rtac prat_less_or_eq_imp_le, fast_tac (claset() addIs [prat_less_trans])]);
qed "prat_le_trans";
-Goal "[| z <= w; w <= z |] ==> z = (w::prat)";
-by (EVERY1 [dtac prat_le_imp_less_or_eq, dtac prat_le_imp_less_or_eq,
- fast_tac (claset() addEs [prat_less_irrefl,prat_less_asym])]);
-qed "prat_le_anti_sym";
-
Goal "[| ~ y < x; y ~= x |] ==> x < (y::prat)";
by (rtac not_prat_leE 1);
by (fast_tac (claset() addDs [prat_le_imp_less_or_eq]) 1);
--- a/src/HOL/Real/PReal.ML Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/PReal.ML Sat Dec 30 22:13:18 2000 +0100
@@ -158,7 +158,7 @@
qed "preal_less_not_refl";
(*** y < y ==> P ***)
-bind_thm("preal_less_irrefl",preal_less_not_refl RS notE);
+bind_thm("preal_less_irrefl", preal_less_not_refl RS notE);
Goal "!!(x::preal). x < y ==> x ~= y";
by (auto_tac (claset(),simpset() addsimps [preal_less_not_refl]));
@@ -750,17 +750,17 @@
qed "preal_less_le_iff";
Goalw [preal_le_def,preal_less_def,psubset_def]
- "z < w ==> z <= (w::preal)";
+ "z < w ==> z <= (w::preal)";
by (Fast_tac 1);
qed "preal_less_imp_le";
Goalw [preal_le_def,preal_less_def,psubset_def]
- "!!(x::preal). x <= y ==> x < y | x = y";
+ "!!(x::preal). x <= y ==> x < y | x = y";
by (auto_tac (claset() addIs [inj_Rep_preal RS injD],simpset()));
qed "preal_le_imp_less_or_eq";
Goalw [preal_le_def,preal_less_def,psubset_def]
- "!!(x::preal). x < y | x = y ==> x <=y";
+ "!!(x::preal). x < y | x = y ==> x <=y";
by Auto_tac;
qed "preal_less_or_eq_imp_le";
@@ -768,19 +768,10 @@
by (Simp_tac 1);
qed "preal_le_refl";
-Goal "[| i <= j; j < k |] ==> i < (k::preal)";
-by (dtac preal_le_imp_less_or_eq 1);
-by (fast_tac (claset() addIs [preal_less_trans]) 1);
-qed "preal_le_less_trans";
-
-Goal "[| i < j; j <= k |] ==> i < (k::preal)";
-by (dtac preal_le_imp_less_or_eq 1);
-by (fast_tac (claset() addIs [preal_less_trans]) 1);
-qed "preal_less_le_trans";
-
Goal "[| i <= j; j <= k |] ==> i <= (k::preal)";
by (EVERY1 [dtac preal_le_imp_less_or_eq, dtac preal_le_imp_less_or_eq,
- rtac preal_less_or_eq_imp_le, fast_tac (claset() addIs [preal_less_trans])]);
+ rtac preal_less_or_eq_imp_le,
+ fast_tac (claset() addIs [preal_less_trans])]);
qed "preal_le_trans";
Goal "[| z <= w; w <= z |] ==> z = (w::preal)";
@@ -788,10 +779,17 @@
fast_tac (claset() addEs [preal_less_irrefl,preal_less_asym])]);
qed "preal_le_anti_sym";
-Goal "[| ~ y < x; y ~= x |] ==> x < (y::preal)";
-by (rtac not_preal_leE 1);
-by (fast_tac (claset() addDs [preal_le_imp_less_or_eq]) 1);
-qed "not_less_not_eq_preal_less";
+Goal "!!w::preal. (w ~= z) = (w<z | z<w)";
+by (cut_inst_tac [("r1.0","w"),("r2.0","z")] preal_linear 1);
+by (auto_tac (claset() addEs [preal_less_irrefl], simpset()));
+qed "preal_neq_iff";
+
+(* Axiom 'order_less_le' of class 'order': *)
+Goal "(w::preal) < z = (w <= z & w ~= z)";
+by (simp_tac (simpset() addsimps [preal_less_le_iff RS sym, preal_neq_iff]) 1);
+by (blast_tac (claset() addSEs [preal_less_asym]) 1);
+qed "preal_less_le";
+
(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)
@@ -833,9 +831,7 @@
by (auto_tac (claset(),simpset() addsimps [prat_less_def]));
qed "lemma_ex_mem_less_left_add1";
-Goal
- "A < B ==> \
-\ {} < {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
+Goal "A < B ==> {} < {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
by (dtac lemma_ex_mem_less_left_add1 1);
by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
qed "preal_less_set_not_empty";
@@ -860,7 +856,7 @@
(** Part 3 of Dedekind sections def **)
Goal "A < B ==> ALL y: {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
- \ ALL z. z < y --> z : {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
+ \ ALL z. z < y --> z : {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
by Auto_tac;
by (dres_inst_tac [("x","n")] prat_add_less2_mono2 1);
by (dtac (Rep_preal RS prealE_lemma3b) 1);
@@ -979,8 +975,8 @@
by (dtac preal_le_imp_less_or_eq 1);
by (Step_tac 1);
by (auto_tac (claset() addSIs [preal_le_refl,
- preal_less_imp_le,preal_add_less2_mono1],
- simpset() addsimps [preal_add_commute]));
+ preal_less_imp_le,preal_add_less2_mono1],
+ simpset() addsimps [preal_add_commute]));
qed "preal_add_left_le_mono1";
Goal "!!(q1::preal). q1 <= q2 ==> q1 + x <= q2 + x";
--- a/src/HOL/Real/RComplete.ML Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/RComplete.ML Sat Dec 30 22:13:18 2000 +0100
@@ -8,6 +8,10 @@
claset_ref() := claset() delWrapper "bspec";
+Goal "x/#2 + x/#2 = (x::real)";
+by (Simp_tac 1);
+qed "real_sum_of_halves";
+
(*---------------------------------------------------------
Completeness of reals: use supremum property of
preal and theorems about real_preal. Theorems
@@ -30,7 +34,7 @@
by Auto_tac;
by (dtac bspec 1 THEN assume_tac 1);
by (ftac bspec 1 THEN assume_tac 1);
-by (dtac real_less_trans 1 THEN assume_tac 1);
+by (dtac order_less_trans 1 THEN assume_tac 1);
by (dtac ((rename_numerals real_gt_zero_preal_Ex) RS iffD1) 1
THEN etac exE 1);
by (res_inst_tac [("x","ya")] exI 1);
@@ -137,14 +141,6 @@
by (Auto_tac);
qed "lemma_le_swap2";
-Goal "[| (x::real) + (-X) + #1 <= S; xa < x |] ==> xa + (-X) + #1 <= S";
-by (Auto_tac);
-qed "lemma_real_complete2";
-
-Goal "[| (x::real) + (-X) + #1 <= S; xa < x |] ==> xa <= S + X + (-#1)"; (**)
-by (Auto_tac);
-qed "lemma_real_complete2a";
-
Goal "[| (x::real) + (-X) + #1 <= S; xa <= x |] ==> xa <= S + X + (-#1)";
by (Auto_tac);
qed "lemma_real_complete2b";
@@ -184,7 +180,7 @@
by (ftac isLubD2 1 THEN assume_tac 2);
by (Blast_tac 1);
by (rtac lemma_real_complete2b 1);
-by (etac real_less_imp_le 2);
+by (etac order_less_imp_le 2);
by (blast_tac (claset() addSIs [isLubD2]) 1 THEN Step_tac 1);
by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
by (blast_tac (claset() addDs [isUbD] addSIs [setleI RS isUbI]
@@ -218,16 +214,16 @@
by (blast_tac (claset() addSIs [isUbI,setleI]) 2);
by (dres_inst_tac [("y","t+(-x)")] isLub_le_isUb 1);
by (dres_inst_tac [("x","-t")] real_add_left_le_mono1 2);
-by (auto_tac (claset() addDs [real_le_less_trans,
- (real_minus_zero_less_iff2 RS iffD2)],
- simpset() addsimps [real_less_not_refl,real_add_assoc RS sym]));
+by (auto_tac (claset() addDs [order_le_less_trans,
+ real_minus_zero_less_iff2 RS iffD2],
+ simpset() addsimps [real_add_assoc RS sym]));
qed "reals_Archimedean";
Goal "EX n. (x::real) < real_of_posnat n";
by (res_inst_tac [("R1.0","x"),("R2.0","#0")] real_linear_less2 1);
by (res_inst_tac [("x","0")] exI 1);
by (res_inst_tac [("x","0")] exI 2);
-by (auto_tac (claset() addEs [real_less_trans],
+by (auto_tac (claset() addEs [order_less_trans],
simpset() addsimps [real_of_posnat_one,real_zero_less_one]));
by (ftac ((rename_numerals real_inverse_gt_zero) RS reals_Archimedean) 1);
by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
--- a/src/HOL/Real/ROOT.ML Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/ROOT.ML Sat Dec 30 22:13:18 2000 +0100
@@ -3,9 +3,8 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-Construction of the Reals using Dedekind Cuts, Ultrapower Construction
-of the hyperreals, and mechanization of Nonstandard Real Analysis
- by Jacques Fleuriot
+Construction of the Reals using Dedekind Cuts
+by Jacques Fleuriot
*)
-with_path "Hyperreal" time_use_thy "Hyperreal";
+time_use_thy "Real";
--- a/src/HOL/Real/RealAbs.ML Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/RealAbs.ML Sat Dec 30 22:13:18 2000 +0100
@@ -49,11 +49,11 @@
by (Asm_simp_tac 1);
qed "abs_eqI1";
-Goalw [real_abs_def] "(#0::real)<x ==> abs x = x";
+Goalw [real_abs_def] "(#0::real) < x ==> abs x = x";
by (Asm_simp_tac 1);
qed "abs_eqI2";
-Goalw [real_abs_def,real_le_def] "x<(#0::real) ==> abs x = -x";
+Goalw [real_abs_def,real_le_def] "x < (#0::real) ==> abs x = -x";
by (Asm_simp_tac 1);
qed "abs_minus_eqI2";
@@ -130,62 +130,41 @@
qed "abs_add_minus_less";
(* lemmas manipulating terms *)
-Goal "((#0::real)*x<r)=(#0<r)";
+Goal "((#0::real)*x < r)=(#0 < r)";
by (Simp_tac 1);
qed "real_mult_0_less";
-Goal "[| (#0::real)<y; x<r; y*r<t*s |] ==> y*x<t*s";
+Goal "[| (#0::real) < y; x < r; y*r < t*s |] ==> y*x < t*s";
by (blast_tac (claset() addSIs [rename_numerals real_mult_less_mono2]
- addIs [real_less_trans]) 1);
+ addIs [order_less_trans]) 1);
qed "real_mult_less_trans";
-Goal "[| (#0::real)<=y; x<r; y*r<t*s; #0<t*s|] ==> y*x<t*s";
-by (dtac real_le_imp_less_or_eq 1);
+Goal "[| (#0::real)<=y; x < r; y*r < t*s; #0 < t*s|] ==> y*x < t*s";
+by (dtac order_le_imp_less_or_eq 1);
by (fast_tac (HOL_cs addEs [real_mult_0_less RS iffD2,
real_mult_less_trans]) 1);
qed "real_mult_le_less_trans";
-Goal "[| abs x<r; abs y<s |] ==> abs(x*y)<r*(s::real)";
+Goal "[| abs x < r; abs y < s |] ==> abs(x*y) < r*(s::real)";
by (simp_tac (simpset() addsimps [abs_mult]) 1);
by (rtac real_mult_le_less_trans 1);
by (rtac abs_ge_zero 1);
by (assume_tac 1);
by (rtac (rename_numerals real_mult_order) 2);
-by (auto_tac (claset() addSIs [real_mult_less_mono1,
- abs_ge_zero] addIs [real_le_less_trans],simpset()));
+by (auto_tac (claset() addSIs [real_mult_less_mono1, abs_ge_zero]
+ addIs [order_le_less_trans],
+ simpset()));
qed "abs_mult_less";
-Goal "[| abs x < r; abs y < s |] ==> abs(x)*abs(y)<r*(s::real)";
+Goal "[| abs x < r; abs y < s |] ==> abs(x)*abs(y) < r*(s::real)";
by (auto_tac (claset() addIs [abs_mult_less],
simpset() addsimps [abs_mult RS sym]));
qed "abs_mult_less2";
-Goal "(#1::real) < abs x ==> abs y <= abs(x*y)";
-by (cut_inst_tac [("x1","y")] (abs_ge_zero RS real_le_imp_less_or_eq) 1);
-by (EVERY1[etac disjE,rtac real_less_imp_le]);
-by (dres_inst_tac [("W","#1")] real_less_sum_gt_zero 1);
-by (forw_inst_tac [("y","abs x + (-#1)")]
- (rename_numerals real_mult_order) 1);
-by (rtac real_sum_gt_zero_less 2);
-by (asm_full_simp_tac (simpset()
- addsimps [real_add_mult_distrib2,
- real_mult_commute, abs_mult]) 2);
-by (dtac sym 2);
-by (auto_tac (claset(),simpset() addsimps [abs_mult]));
-qed "abs_mult_le";
-
-Goal "[| (#1::real) < abs x; r < abs y|] ==> r < abs(x*y)";
-by (blast_tac (HOL_cs addIs [abs_mult_le, real_less_le_trans]) 1);
-qed "abs_mult_gt";
-
-Goal "abs(x)<r ==> (#0::real)<r";
-by (blast_tac (claset() addSIs [real_le_less_trans,abs_ge_zero]) 1);
+Goal "abs(x) < r ==> (#0::real) < r";
+by (blast_tac (claset() addSIs [order_le_less_trans,abs_ge_zero]) 1);
qed "abs_less_gt_zero";
-Goalw [real_abs_def] "abs #1 = (#1::real)";
-by (Simp_tac 1);
-qed "abs_one";
-
Goalw [real_abs_def] "abs (-#1) = (#1::real)";
by (Simp_tac 1);
qed "abs_minus_one";
@@ -195,7 +174,7 @@
by Auto_tac;
qed "abs_disj";
-Goalw [real_abs_def] "(abs x < r) = (-r<x & x<(r::real))";
+Goalw [real_abs_def] "(abs x < r) = (-r < x & x < (r::real))";
by Auto_tac;
qed "abs_interval_iff";
@@ -219,7 +198,7 @@
Addsimps [abs_not_less_zero];
Goal "abs h < abs y - abs x ==> abs (x + h) < abs (y::real)";
-by (auto_tac (claset() addIs [abs_triangle_ineq RS real_le_less_trans],
+by (auto_tac (claset() addIs [abs_triangle_ineq RS order_le_less_trans],
simpset()));
qed "abs_circle";
@@ -242,13 +221,13 @@
Goal "~ abs(x) + (#1::real) < x";
by (rtac real_leD 1);
-by (auto_tac (claset() addIs [abs_ge_self RS real_le_trans], simpset()));
+by (auto_tac (claset() addIs [abs_ge_self RS order_trans], simpset()));
qed "abs_add_one_not_less_self";
Addsimps [abs_add_one_not_less_self];
(* used in vector theory *)
Goal "abs(w + x + (y::real)) <= abs(w) + abs(x) + abs(y)";
-by (auto_tac (claset() addSIs [abs_triangle_ineq RS real_le_trans,
+by (auto_tac (claset() addSIs [abs_triangle_ineq RS order_trans,
real_add_left_le_mono1],
simpset() addsimps [real_add_assoc]));
qed "abs_triangle_ineq_three";
--- a/src/HOL/Real/RealArith0.ML Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/RealArith0.ML Sat Dec 30 22:13:18 2000 +0100
@@ -22,7 +22,7 @@
simpset() addsimps [linorder_neq_iff,
rename_numerals real_inverse_gt_zero]));
qed "real_0_less_inverse_iff";
-AddIffs [real_0_less_inverse_iff];
+Addsimps [real_0_less_inverse_iff];
Goal "(inverse x < (#0::real)) = (x < #0)";
by (case_tac "x=#0" 1);
@@ -31,34 +31,23 @@
simpset() addsimps [linorder_neq_iff,
rename_numerals real_inverse_gt_zero]));
qed "real_inverse_less_0_iff";
-AddIffs [real_inverse_less_0_iff];
+Addsimps [real_inverse_less_0_iff];
Goal "((#0::real) <= inverse x) = (#0 <= x)";
by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
qed "real_0_le_inverse_iff";
-AddIffs [real_0_le_inverse_iff];
+Addsimps [real_0_le_inverse_iff];
Goal "(inverse x <= (#0::real)) = (x <= #0)";
by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
qed "real_inverse_le_0_iff";
-AddIffs [real_inverse_le_0_iff];
+Addsimps [real_inverse_le_0_iff];
Goalw [real_divide_def] "x/(#0::real) = #0";
by (stac (rename_numerals INVERSE_ZERO) 1);
by (Simp_tac 1);
qed "REAL_DIVIDE_ZERO";
-(*generalize?*)
-Goal "((#0::real) < #1/x) = (#0 < x)";
-by (simp_tac (simpset() addsimps [real_divide_def]) 1);
-qed "real_0_less_recip_iff";
-AddIffs [real_0_less_recip_iff];
-
-Goal "(#1/x < (#0::real)) = (x < #0)";
-by (simp_tac (simpset() addsimps [real_divide_def]) 1);
-qed "real_recip_less_0_iff";
-AddIffs [real_recip_less_0_iff];
-
Goal "inverse (x::real) = #1/x";
by (simp_tac (simpset() addsimps [real_divide_def]) 1);
qed "real_inverse_eq_divide";
@@ -90,12 +79,12 @@
by (rtac ccontr 1);
by (blast_tac (claset() addDs [rename_numerals real_inverse_not_zero]) 1);
qed "real_inverse_zero_iff";
-AddIffs [real_inverse_zero_iff];
+Addsimps [real_inverse_zero_iff];
Goal "(x/y = #0) = (x=#0 | y=(#0::real))";
by (auto_tac (claset(), simpset() addsimps [real_divide_def]));
qed "real_divide_eq_0_iff";
-AddIffs [real_divide_eq_0_iff];
+Addsimps [real_divide_eq_0_iff];
(**** Factor cancellation theorems for "real" ****)
@@ -259,7 +248,7 @@
val neg_exchanges = true
)
-val real_cancel_numeral_factors =
+val real_cancel_numeral_factors_relations =
map prep_simproc
[("realeq_cancel_numeral_factor",
prep_pats ["(l::real) * m = n", "(l::real) = m * n"],
@@ -269,10 +258,16 @@
LessCancelNumeralFactor.proc),
("realle_cancel_numeral_factor",
prep_pats ["(l::real) * m <= n", "(l::real) <= m * n"],
- LeCancelNumeralFactor.proc),
- ("realdiv_cancel_numeral_factor",
- prep_pats ["((l::real) * m) / n", "(l::real) / (m * n)"],
- DivCancelNumeralFactor.proc)];
+ LeCancelNumeralFactor.proc)];
+
+val real_cancel_numeral_factors_divide = prep_simproc
+ ("realdiv_cancel_numeral_factor",
+ prep_pats ["((l::real) * m) / n", "(l::real) / (m * n)"],
+ DivCancelNumeralFactor.proc);
+
+val real_cancel_numeral_factors =
+ real_cancel_numeral_factors_relations @
+ [real_cancel_numeral_factors_divide];
end;
@@ -624,7 +619,8 @@
AddIffs [real_0_le_diff_iff];
(*
-?? still needed ??
+FIXME: we should have this, as for type int, but many proofs would break.
+It replaces x+-y by x-y.
Addsimps [symmetric real_diff_def];
*)
--- a/src/HOL/Real/RealBin.ML Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/RealBin.ML Sat Dec 30 22:13:18 2000 +0100
@@ -82,7 +82,7 @@
\ iszero (number_of (bin_add v (bin_minus v')))";
by (simp_tac
(HOL_ss addsimps [real_number_of_def,
- real_of_int_eq_iff, eq_number_of_eq]) 1);
+ real_of_int_eq_iff, eq_number_of_eq]) 1);
qed "eq_real_number_of";
Addsimps [eq_real_number_of];
@@ -148,6 +148,11 @@
bind_thm ("real_mult_le_0_iff",
rename_numerals real_mult_le_zero_iff);
+bind_thm ("real_inverse_less_0", rename_numerals real_inverse_less_zero);
+bind_thm ("real_inverse_gt_0", rename_numerals real_inverse_gt_zero);
+
+Addsimps [rename_numerals real_le_square];
+
(*Perhaps add some theorems that aren't in the default simpset, as
done in Integ/NatBin.ML*)
--- a/src/HOL/Real/RealDef.ML Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/RealDef.ML Sat Dec 30 22:13:18 2000 +0100
@@ -543,8 +543,6 @@
by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
qed "real_mult_not_zero";
-bind_thm ("real_mult_not_zeroE",real_mult_not_zero RS notE);
-
Goal "inverse(inverse (x::real)) = x";
by (real_div_undefined_case_tac "x=0" 1);
by (res_inst_tac [("c1","inverse x")] (real_mult_right_cancel RS iffD1) 1);
@@ -656,8 +654,8 @@
by (res_inst_tac [("z","R")] eq_Abs_real 1);
by (auto_tac (claset(),simpset() addsimps [real_less_def]));
by (dtac preal_lemma_for_not_refl 1);
-by (assume_tac 1 THEN rotate_tac 2 1);
-by (auto_tac (claset(),simpset() addsimps [preal_less_not_refl]));
+by (assume_tac 1);
+by Auto_tac;
qed "real_less_not_refl";
(*** y < y ==> P ***)
@@ -936,10 +934,6 @@
by (Blast_tac 1);
qed "not_real_leE";
-Goalw [real_le_def] "z < w ==> z <= (w::real)";
-by (blast_tac (claset() addEs [real_less_asym]) 1);
-qed "real_less_imp_le";
-
Goalw [real_le_def] "!!(x::real). x <= y ==> x < y | x = y";
by (cut_facts_tac [real_linear] 1);
by (blast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
@@ -958,8 +952,6 @@
by (simp_tac (simpset() addsimps [real_le_less]) 1);
qed "real_le_refl";
-AddIffs [real_le_refl];
-
(* Axiom 'linorder_linear' of class 'linorder': *)
Goal "(z::real) <= w | w <= z";
by (simp_tac (simpset() addsimps [real_le_less]) 1);
@@ -967,19 +959,10 @@
by (Blast_tac 1);
qed "real_le_linear";
-Goal "[| i <= j; j < k |] ==> i < (k::real)";
-by (dtac real_le_imp_less_or_eq 1);
-by (blast_tac (claset() addIs [real_less_trans]) 1);
-qed "real_le_less_trans";
-
-Goal "!! (i::real). [| i < j; j <= k |] ==> i < k";
-by (dtac real_le_imp_less_or_eq 1);
-by (blast_tac (claset() addIs [real_less_trans]) 1);
-qed "real_less_le_trans";
-
Goal "[| i <= j; j <= k |] ==> i <= (k::real)";
by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq,
- rtac real_less_or_eq_imp_le, blast_tac (claset() addIs [real_less_trans])]);
+ rtac real_less_or_eq_imp_le,
+ blast_tac (claset() addIs [real_less_trans])]);
qed "real_le_trans";
Goal "[| z <= w; w <= z |] ==> z = (w::real)";
--- a/src/HOL/Real/RealDef.thy Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/RealDef.thy Sat Dec 30 22:13:18 2000 +0100
@@ -7,6 +7,9 @@
RealDef = PReal +
+instance preal :: order (preal_le_refl,preal_le_trans,preal_le_anti_sym,
+ preal_less_le)
+
constdefs
realrel :: "((preal * preal) * (preal * preal)) set"
"realrel == {p. ? x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
@@ -18,8 +21,11 @@
real :: {ord, zero, plus, times, minus, inverse}
consts
+ "1r" :: real ("1r")
- "1r" :: real ("1r")
+ (*Overloaded constant: denotes the Real subset of enclosing types such as
+ hypreal and complex*)
+ SReal :: "'a set"
defs
@@ -58,18 +64,21 @@
defs
real_add_def
- "P + Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
- (%(x1,y1). (%(x2,y2). realrel^^{(x1+x2, y1+y2)}) p2) p1)"
+ "P+Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
+ (%(x1,y1). (%(x2,y2). realrel^^{(x1+x2, y1+y2)}) p2) p1)"
real_mult_def
- "P * Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
- (%(x1,y1). (%(x2,y2). realrel^^{(x1*x2+y1*y2,x1*y2+x2*y1)}) p2) p1)"
+ "P*Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
+ (%(x1,y1). (%(x2,y2). realrel^^{(x1*x2+y1*y2,x1*y2+x2*y1)})
+ p2) p1)"
real_less_def
- "P < Q == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 &
- (x1,y1):Rep_real(P) &
- (x2,y2):Rep_real(Q)"
+ "P<Q == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 &
+ (x1,y1):Rep_real(P) & (x2,y2):Rep_real(Q)"
real_le_def
"P <= (Q::real) == ~(Q < P)"
+syntax (symbols)
+ SReal :: "'a set" ("\\<real>")
+
end
--- a/src/HOL/Real/RealOrd.ML Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/RealOrd.ML Sat Dec 30 22:13:18 2000 +0100
@@ -78,16 +78,16 @@
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);
+ 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 [real_le_imp_less_or_eq,
+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 [real_le_imp_less_or_eq RS disjE]
+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";
@@ -113,8 +113,8 @@
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 preal_le_less_trans 1 THEN assume_tac 1);
+ 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";
@@ -131,28 +131,28 @@
qed "real_mult_less_zero1";
Goal "[| 0 <= x; 0 <= y |] ==> (0::real) <= x * y";
-by (REPEAT(dtac real_le_imp_less_or_eq 1));
-by (auto_tac (claset() addIs [real_mult_order, real_less_imp_le],
+by (REPEAT(dtac order_le_imp_less_or_eq 1));
+by (auto_tac (claset() addIs [real_mult_order, order_less_imp_le],
simpset()));
qed "real_le_mult_order";
Goal "[| 0 < x; 0 <= y |] ==> (0::real) <= x * y";
-by (dtac real_le_imp_less_or_eq 1);
-by (auto_tac (claset() addIs [real_mult_order,
- real_less_imp_le],simpset()));
+by (dtac order_le_imp_less_or_eq 1);
+by (auto_tac (claset() addIs [real_mult_order, order_less_imp_le],
+ simpset()));
qed "real_less_le_mult_order";
Goal "[| x <= 0; y <= 0 |] ==> (0::real) <= x * y";
by (rtac real_less_or_eq_imp_le 1);
-by (dtac real_le_imp_less_or_eq 1 THEN etac disjE 1);
+by (dtac order_le_imp_less_or_eq 1 THEN etac disjE 1);
by Auto_tac;
-by (dtac real_le_imp_less_or_eq 1);
+by (dtac order_le_imp_less_or_eq 1);
by (auto_tac (claset() addDs [real_mult_less_zero1],simpset()));
qed "real_mult_le_zero1";
Goal "[| 0 <= x; y < 0 |] ==> x * y <= (0::real)";
by (rtac real_less_or_eq_imp_le 1);
-by (dtac real_le_imp_less_or_eq 1 THEN etac disjE 1);
+by (dtac order_le_imp_less_or_eq 1 THEN etac disjE 1);
by Auto_tac;
by (dtac (real_minus_zero_less_iff RS iffD2) 1);
by (rtac (real_minus_zero_less_iff RS subst) 1);
@@ -201,12 +201,12 @@
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 real_less_le_trans) 1);
+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 real_le_less_trans) 1);
+by (etac (real_add_le_mono1 RS order_le_less_trans) 1);
by (Simp_tac 1);
qed "real_add_le_less_mono";
@@ -231,20 +231,20 @@
qed "real_le_add_left_cancel";
Goal "[| 0 < x; 0 < y |] ==> (0::real) < x + y";
-by (etac real_less_trans 1);
+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 real_le_imp_less_or_eq 1));
-by (auto_tac (claset() addIs [real_add_order, real_less_imp_le],
+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 real_less_trans 1);
+by (etac order_less_trans 1);
by (etac real_add_less_mono2 1);
qed "real_add_less_mono";
@@ -254,7 +254,7 @@
Goal "[|i<=j; k<=l |] ==> i + k <= j + (l::real)";
by (dtac real_add_le_mono1 1);
-by (etac real_le_trans 1);
+by (etac order_trans 1);
by (Simp_tac 1);
qed "real_add_le_mono";
@@ -283,14 +283,14 @@
Addsimps [real_le_minus_iff];
Goal "0 <= 1r";
-by (rtac (real_zero_less_one RS real_less_imp_le) 1);
+by (rtac (real_zero_less_one RS order_less_imp_le) 1);
qed "real_zero_le_one";
Addsimps [real_zero_le_one];
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,
- real_mult_less_zero1,real_less_imp_le],
+ real_mult_less_zero1,order_less_imp_le],
simpset()));
qed "real_le_square";
Addsimps [real_le_square];
@@ -353,7 +353,7 @@
by (induct_tac "n" 1);
by (auto_tac (claset(),
simpset () addsimps [real_of_posnat_Suc,real_of_posnat_one,
- real_of_posnat_gt_zero, real_less_imp_le]));
+ real_of_posnat_gt_zero, order_less_imp_le]));
qed "real_of_posnat_less_one";
Addsimps [real_of_posnat_less_one];
@@ -378,7 +378,7 @@
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 real_le_imp_less_or_eq, Step_tac]);
+by (EVERY1[dtac order_le_imp_less_or_eq, Step_tac]);
by (dtac real_mult_less_zero1 1 THEN assume_tac 1);
by (auto_tac (claset() addIs [real_zero_less_one RS real_less_asym],
simpset()));
@@ -418,40 +418,33 @@
qed "real_one_less_two";
Goal "0 < 1r + 1r";
-by (rtac ([real_zero_less_one,
- real_one_less_two] MRS real_less_trans) 1);
+by (rtac ([real_zero_less_one, real_one_less_two] MRS order_less_trans) 1);
qed "real_zero_less_two";
Goal "1r + 1r ~= 0";
by (rtac (real_zero_less_two RS real_not_refl2 RS not_sym) 1);
qed "real_two_not_zero";
-
Addsimps [real_two_not_zero];
-Goal "x * inverse (1r + 1r) + x * inverse(1r + 1r) = x";
-by (stac real_add_self 1);
-by (full_simp_tac (simpset() addsimps [real_mult_assoc]) 1);
-qed "real_sum_of_halves";
-
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);
+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);
+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_zero
- RS real_mult_less_mono1) 1);
+by (forw_inst_tac [("x","x*z")]
+ (real_inverse_gt_zero RS real_mult_less_mono1) 1);
by (auto_tac (claset(),
- simpset() addsimps
- [real_mult_assoc,real_not_refl2 RS not_sym]));
+ 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";
@@ -460,13 +453,13 @@
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);
+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);
+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];
@@ -484,7 +477,7 @@
Goal "[| (0::real) <= z; x < y |] ==> x*z <= y*z";
-by (EVERY1 [rtac real_less_or_eq_imp_le, dtac real_le_imp_less_or_eq]);
+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";
@@ -493,86 +486,68 @@
qed "real_mult_le_less_mono2";
Goal "[| (0::real) <= z; x <= y |] ==> z*x <= z*y";
-by (dres_inst_tac [("x","x")] real_le_imp_less_or_eq 1);
+by (dres_inst_tac [("x","x")] order_le_imp_less_or_eq 1);
by (auto_tac (claset() addIs [real_mult_le_less_mono2], simpset()));
qed "real_mult_le_le_mono1";
-Goal "[| (0::real) < r1; r1 < r2; 0 < x; x < y|] ==> r1 * x < r2 * y";
-by (dres_inst_tac [("x","x")] real_mult_less_mono2 1);
-by (dres_inst_tac [("R1.0","0")] real_less_trans 2);
-by (dres_inst_tac [("x","r1")] real_mult_less_mono1 3);
-by Auto_tac;
-by (blast_tac (claset() addIs [real_less_trans]) 1);
+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";
-Goal "[| (0::real) < r1; r1 < r2; 0 < y|] ==> 0 < r2 * y";
-by (rtac real_mult_order 1);
-by (assume_tac 2);
-by (blast_tac (claset() addIs [real_less_trans]) 1);
-qed "real_mult_order_trans";
-
-Goal "[| (0::real) < r1; r1 < r2; 0 <= x; x < y|] ==> r1 * x < r2 * y";
-by (auto_tac (claset() addSDs [real_le_imp_less_or_eq]
- addIs [real_mult_less_mono,real_mult_order_trans],
- simpset()));
-qed "real_mult_less_mono3";
+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 "[| (0::real) <= r1; r1 < r2; 0 <= x; x < y|] ==> r1 * x < r2 * y";
-by (auto_tac (claset() addSDs [real_le_imp_less_or_eq]
- addIs [real_mult_less_mono,real_mult_order_trans,
- real_mult_order],
- simpset()));
-by (dres_inst_tac [("R2.0","x")] real_less_trans 1);
-by (assume_tac 1);
-by (blast_tac (claset() addIs [real_mult_order]) 1);
-qed "real_mult_less_mono4";
-
-Goal "[| (0::real) < r1; r1 <= r2; 0 <= x; x <= y |] ==> r1 * x <= r2 * y";
+Goal "[| r1 <= r2; x <= y; (0::real) < r1; 0 <= x |] ==> r1 * x <= r2 * y";
+by (subgoal_tac "0<r2" 1);
+by (blast_tac (claset() addIs [order_less_le_trans]) 2);
by (rtac real_less_or_eq_imp_le 1);
-by (REPEAT(dtac real_le_imp_less_or_eq 1));
-by (auto_tac (claset() addIs [real_mult_less_mono,
- real_mult_order_trans,real_mult_order],
+by (REPEAT(dtac order_le_imp_less_or_eq 1));
+by (auto_tac (claset() addIs [real_mult_less_mono, real_mult_order],
simpset()));
qed "real_mult_le_mono";
Goal "[| (0::real) < r1; r1 < r2; 0 <= x; x <= y |] ==> r1 * x <= r2 * y";
-by (rtac real_less_or_eq_imp_le 1);
-by (REPEAT(dtac real_le_imp_less_or_eq 1));
-by (auto_tac (claset() addIs [real_mult_less_mono, real_mult_order_trans,
- real_mult_order],
- simpset()));
+by (blast_tac (claset() addIs [real_mult_le_mono, order_less_imp_le]) 1);
qed "real_mult_le_mono2";
Goal "[| (0::real) <= r1; r1 < r2; 0 <= x; x <= y |] ==> r1 * x <= r2 * y";
-by (dtac real_le_imp_less_or_eq 1);
+by (dtac order_le_imp_less_or_eq 1);
by (auto_tac (claset() addIs [real_mult_le_mono2],simpset()));
-by (dtac real_le_trans 1 THEN assume_tac 1);
+by (dtac order_trans 1 THEN assume_tac 1);
by (auto_tac (claset() addIs [real_less_le_mult_order], simpset()));
qed "real_mult_le_mono3";
Goal "[| (0::real) <= r1; r1 <= r2; 0 <= x; x <= y |] ==> r1 * x <= r2 * y";
-by (dres_inst_tac [("x","r1")] real_le_imp_less_or_eq 1);
+by (dres_inst_tac [("x","r1")] order_le_imp_less_or_eq 1);
by (auto_tac (claset() addIs [real_mult_le_mono3, real_mult_le_le_mono1],
simpset()));
qed "real_mult_le_mono4";
Goal "1r <= x ==> 0 < x";
by (rtac ccontr 1 THEN dtac real_leI 1);
-by (dtac real_le_trans 1 THEN assume_tac 1);
-by (auto_tac (claset() addDs [real_zero_less_one RSN (2,real_le_less_trans)],
- simpset() addsimps [real_less_not_refl]));
+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 "[| 1r < r; 1r <= x |] ==> x <= r * x";
-by (dtac (real_gt_zero RS real_less_imp_le) 1);
+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 "[| 1r <= r; 1r <= x |] ==> x <= r * x";
-by (dtac real_le_imp_less_or_eq 1);
-by (auto_tac (claset() addIs [real_mult_self_le],
- simpset() addsimps [real_le_refl]));
+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 "(EX n. inverse (real_of_posnat n) < r) = (EX n. 1r < r * real_of_posnat n)";
@@ -599,9 +574,9 @@
Goal "(inverse (real_of_posnat n) <= r) = (1r <= r * real_of_posnat n)";
by (Step_tac 1);
by (dres_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS
- real_less_imp_le RS real_mult_le_le_mono1) 1);
+ order_less_imp_le RS real_mult_le_le_mono1) 1);
by (dres_inst_tac [("n3","n")] (real_of_posnat_gt_zero RS
- real_inverse_gt_zero RS real_less_imp_le RS
+ real_inverse_gt_zero RS order_less_imp_le RS
real_mult_le_le_mono1) 2);
by (auto_tac (claset(), simpset() addsimps real_mult_ac));
qed "real_of_posnat_inverse_le_iff";
@@ -636,7 +611,7 @@
qed "real_of_posnat_inverse_eq_iff";
Goal "[| 0 < r; r < x |] ==> inverse x < inverse (r::real)";
-by (ftac real_less_trans 1 THEN assume_tac 1);
+by (ftac order_less_trans 1 THEN assume_tac 1);
by (ftac real_inverse_gt_zero 1);
by (forw_inst_tac [("x","x")] real_inverse_gt_zero 1);
by (forw_inst_tac [("x","r"),("z","inverse r")] real_mult_less_mono1 1);
@@ -657,7 +632,7 @@
Addsimps [real_add_inverse_real_of_posnat_less];
Goal "r <= r + inverse (real_of_posnat n)";
-by (rtac real_less_imp_le 1);
+by (rtac order_less_imp_le 1);
by (Simp_tac 1);
qed "real_add_inverse_real_of_posnat_le";
Addsimps [real_add_inverse_real_of_posnat_le];
@@ -670,7 +645,7 @@
Addsimps [real_add_minus_inverse_real_of_posnat_less];
Goal "r + (-inverse (real_of_posnat n)) <= r";
-by (rtac real_less_imp_le 1);
+by (rtac order_less_imp_le 1);
by (Simp_tac 1);
qed "real_add_minus_inverse_real_of_posnat_le";
Addsimps [real_add_minus_inverse_real_of_posnat_le];
--- a/src/HOL/Real/RealPow.ML Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/RealPow.ML Sat Dec 30 22:13:18 2000 +0100
@@ -29,8 +29,7 @@
Goal "abs (r::real) ^ n = abs (r ^ n)";
by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps
- [abs_mult,abs_one]));
+by (auto_tac (claset(), simpset() addsimps [abs_mult]));
qed "realpow_abs";
Goal "(r::real) ^ (n + m) = (r ^ n) * (r ^ m)";
@@ -49,7 +48,7 @@
Goal "(#0::real) < r --> #0 <= r ^ n";
by (induct_tac "n" 1);
-by (auto_tac (claset() addDs [real_less_imp_le]
+by (auto_tac (claset() addDs [order_less_imp_le]
addIs [rename_numerals real_le_mult_order],
simpset()));
qed_spec_mp "realpow_ge_zero";
@@ -87,20 +86,15 @@
simpset()));
qed_spec_mp "realpow_less";
-Goal "#1 ^ n = (#1::real)";
+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 (simp_tac (simpset() addsimps [abs_one]) 1);
-qed "abs_minus_realpow_one";
-Addsimps [abs_minus_realpow_one];
-
Goal "abs((#-1) ^ n) = (#1::real)";
by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps [abs_mult,abs_one]));
+by (auto_tac (claset(), simpset() addsimps [abs_mult]));
qed "abs_realpow_minus_one";
Addsimps [abs_realpow_minus_one];
@@ -129,59 +123,30 @@
Goal "(#1::real) < r ==> #1 < r^2";
by Auto_tac;
by (cut_facts_tac [rename_numerals real_zero_less_one] 1);
-by (forw_inst_tac [("R1.0","#0")] real_less_trans 1);
+by (forw_inst_tac [("x","#0")] order_less_trans 1);
by (assume_tac 1);
by (dres_inst_tac [("z","r"),("x","#1")]
(rename_numerals real_mult_less_mono1) 1);
-by (auto_tac (claset() addIs [real_less_trans],simpset()));
+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 (claset() addSDs [real_le_imp_less_or_eq],
- simpset()));
-by (dtac (rename_numerals (real_zero_less_one RS real_mult_less_mono)) 1);
-by (auto_tac (claset() addSIs [real_less_imp_le],
- simpset() addsimps [real_zero_less_one]));
+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 ^ (Suc n)";
-by (forw_inst_tac [("n","n")] realpow_ge_one 1);
-by (dtac real_le_imp_less_or_eq 1 THEN Step_tac 1);
-by (dtac sym 2);
-by (ftac (rename_numerals (real_zero_less_one RS real_less_trans)) 1);
-by (dres_inst_tac [("y","r ^ n")]
- (rename_numerals real_mult_less_mono2) 1);
-by (assume_tac 1);
-by (auto_tac (claset() addDs [real_less_trans],
- simpset()));
-qed "realpow_Suc_gt_one";
-
Goal "(#1::real) <= r ==> #1 <= r ^ n";
-by (dtac real_le_imp_less_or_eq 1);
+by (dtac order_le_imp_less_or_eq 1);
by (auto_tac (claset() addDs [realpow_ge_one], simpset()));
qed "realpow_ge_one2";
-Goal "(#0::real) < r ==> #0 < r ^ Suc n";
-by (forw_inst_tac [("n","n")] realpow_ge_zero 1);
-by (forw_inst_tac [("n1","n")]
- ((real_not_refl2 RS not_sym) RS realpow_not_zero RS not_sym) 1);
-by (auto_tac (claset() addSDs [real_le_imp_less_or_eq]
- addIs [rename_numerals real_mult_order],
- simpset()));
-qed "realpow_Suc_gt_zero";
-
-Goal "(#0::real) <= r ==> #0 <= r ^ Suc n";
-by (etac (real_le_imp_less_or_eq RS disjE) 1);
-by (etac (realpow_ge_zero) 1);
-by (dtac sym 1);
-by (Asm_simp_tac 1);
-qed "realpow_Suc_ge_zero";
-
Goal "(#1::real) <= #2 ^ n";
-by (res_inst_tac [("j","#1 ^ n")] real_le_trans 1);
+by (res_inst_tac [("y","#1 ^ n")] order_trans 1);
by (rtac realpow_le 2);
-by (auto_tac (claset() addIs [real_less_imp_le],simpset()));
+by (auto_tac (claset() addIs [order_less_imp_le],simpset()));
qed "two_realpow_ge_one";
Goal "real_of_nat n < #2 ^ n";
@@ -217,8 +182,9 @@
Goal "#0 <= r & r < (#1::real) --> r ^ Suc n <= r ^ n";
by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [real_less_imp_le] addSDs
- [real_le_imp_less_or_eq],simpset()));
+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";
@@ -228,12 +194,12 @@
Addsimps [realpow_zero_le];
Goal "#0 < r & r < (#1::real) --> r ^ Suc n <= r ^ n";
-by (blast_tac (claset() addSIs [real_less_imp_le,
+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 (real_le_imp_less_or_eq RS disjE) 1);
+by (etac (order_le_imp_less_or_eq RS disjE) 1);
by (rtac realpow_Suc_le2 1);
by Auto_tac;
qed "realpow_Suc_le3";
@@ -257,13 +223,12 @@
Goal "[| #0 < r; r < (#1::real) |] ==> r ^ Suc n <= r";
by (dres_inst_tac [("n","1"),("N","Suc n")]
- (real_less_imp_le RS realpow_le_le) 1);
+ (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,
- real_le_less_trans]) 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";
@@ -277,8 +242,7 @@
qed_spec_mp "realpow_less_Suc";
Goal "(#1::real) < r --> r ^ n <= r ^ Suc n";
-by (blast_tac (claset() addSIs [real_less_imp_le,
- realpow_less_Suc]) 1);
+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";
@@ -288,8 +252,8 @@
by (ALLGOALS(dtac (rename_numerals real_mult_self_le)));
by (assume_tac 1);
by (assume_tac 2);
-by (auto_tac (claset() addIs [real_le_trans],
- simpset() addsimps [less_Suc_eq]));
+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";
@@ -299,18 +263,18 @@
by (ALLGOALS(dtac (rename_numerals real_mult_self_le2)));
by (assume_tac 1);
by (assume_tac 2);
-by (auto_tac (claset() addIs [real_le_trans],
- simpset() addsimps [less_Suc_eq]));
+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()));
+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()));
+by (auto_tac (claset() addIs [realpow_gt_ge2], simpset()));
qed "realpow_ge_ge2";
Goal "(#1::real) < r ==> r <= r ^ Suc n";
@@ -390,17 +354,13 @@
Goal "(#0::real) <= x --> #0 <= y --> x ^ Suc n <= y ^ Suc n --> x <= y";
by (induct_tac "n" 1);
by Auto_tac;
-by (rtac real_leI 1);
-by (auto_tac (claset(),
- simpset() addsimps [inst "x" "#0" order_le_less,
- real_mult_le_0_iff]));
-by (subgoal_tac "inverse x * (x * (x * x ^ n)) <= inverse y * (y * (y * y ^ n))" 1);
-by (rtac real_mult_le_mono 2);
-by (asm_full_simp_tac (simpset() addsimps [realpow_ge_zero, real_0_le_mult_iff]) 4);
-by (asm_full_simp_tac (simpset() addsimps [real_inverse_le_iff]) 3);
-by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
-by (rtac real_inverse_gt_zero 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";