--- a/src/HOL/Real/HahnBanach/Aux.thy Fri Jan 05 10:15:48 2001 +0100
+++ b/src/HOL/Real/HahnBanach/Aux.thy Fri Jan 05 10:17:19 2001 +0100
@@ -17,53 +17,44 @@
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"
-proof -
- 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
- next
- assume "x = y" thus ?thesis by simp
- qed
-qed
+ "(#0::real) \<le> z \<Longrightarrow> x \<le> y \<Longrightarrow> z * x \<le> z * y"
+ by (simp add: real_mult_le_mono2)
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 +66,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 order_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 order_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,20 +96,15 @@
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"
-proof -
- 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
+ "(#0::real) \<le> x \<Longrightarrow> #0 \<le> y \<Longrightarrow> #0 \<le> x * y"
+ by (simp add: real_0_le_mult_iff)
lemma real_mult_diff_distrib:
"a * (- x - (y::real)) = - a * x - a * y"
@@ -141,11 +127,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