--- a/src/HOL/Real/HahnBanach/Aux.thy Wed Jul 19 18:57:27 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy Thu Jul 20 12:04:47 2000 +0200
@@ -38,19 +38,6 @@
qed
text_raw {* \medskip *}
-text {* Some lemmas about linear orders. *}
-
-theorem linorder_linear_split:
-"[| x < a ==> Q; x = a ==> Q; a < (x::'a::linorder) ==> Q |] ==> Q"
- by (rule linorder_less_linear [of x a, elimify]) force+
-
-lemma le_max1: "x <= max x (y::'a::linorder)"
- by (simp add: le_max_iff_disj[of x x y])
-
-lemma le_max2: "y <= max x (y::'a::linorder)"
- by (simp add: le_max_iff_disj[of y x y])
-
-text_raw {* \medskip *}
text{* Some lemmas for the reals. *}
lemma real_add_minus_eq: "x - y = (#0::real) ==> x = y"
@@ -66,9 +53,9 @@
hence "x < y | x = y" by (force simp add: order_le_less)
thus ?thesis
proof (elim disjE)
- assume "x < y" show ?thesis by (rule real_mult_le_less_mono2) simp
+ assume "x < y" show ?thesis by (rule real_mult_le_less_mono2) simp
next
- assume "x = y" thus ?thesis by simp
+ assume "x = y" thus ?thesis by simp
qed
qed
@@ -79,9 +66,9 @@
hence "x < y | x = y" by (force simp add: order_le_less)
thus ?thesis
proof (elim disjE)
- assume "x < y" show ?thesis by (rule real_mult_le_less_mono1) simp
+ assume "x < y" show ?thesis by (rule real_mult_le_less_mono1) simp
next
- assume "x = y" thus ?thesis by simp
+ assume "x = y" thus ?thesis by simp
qed
qed
@@ -108,27 +95,27 @@
thus ?thesis by (simp only: real_mult_commute)
qed
-lemma real_rinv_gt_zero1: "#0 < x ==> #0 < rinv x";
-proof -;
- assume "#0 < x";
- have "0 < x"; by simp;
- hence "0 < rinv x"; by (rule real_rinv_gt_zero);
- thus ?thesis; by simp;
-qed;
+lemma real_rinv_gt_zero1: "#0 < x ==> #0 < rinv x"
+proof -
+ assume "#0 < x"
+ have "0 < x" by simp
+ hence "0 < rinv x" by (rule real_rinv_gt_zero)
+ thus ?thesis by simp
+qed
lemma real_mult_inv_right1: "x \\<noteq> #0 ==> x*rinv(x) = #1"
- by simp
+ by simp
lemma real_mult_inv_left1: "x \\<noteq> #0 ==> rinv(x) * x = #1"
- by simp
+ by simp
lemma real_le_mult_order1a:
- "[| (#0::real) <= x; #0 <= y |] ==> #0 <= x * y"
+ "[| (#0::real) <= x; #0 <= y |] ==> #0 <= x * y"
proof -
assume "#0 <= x" "#0 <= y"
- have "[|0 <= x; 0 <= y|] ==> 0 <= x * y"
- by (rule real_le_mult_order)
- thus ?thesis by (simp!)
+ have "[|0 <= x; 0 <= y|] ==> 0 <= x * y"
+ by (rule real_le_mult_order)
+ thus ?thesis by (simp!)
qed
lemma real_mult_diff_distrib:
@@ -138,7 +125,7 @@
also have "a * ... = a * - x + a * - y"
by (simp only: real_add_mult_distrib2)
also have "... = - a * x - a * y"
- by simp;
+ by simp
finally show ?thesis .
qed
@@ -148,7 +135,7 @@
also have "a * ... = a * x + a * - y"
by (simp only: real_add_mult_distrib2)
also have "... = a * x - a * y"
- by simp;
+ by simp
finally show ?thesis .
qed
@@ -156,7 +143,7 @@
by simp
lemma real_diff_ineq_swap:
- "(d::real) - b <= c + a ==> - a - b <= c - d"
+ "(d::real) - b <= c + a ==> - a - b <= c - d"
by simp
end
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Wed Jul 19 18:57:27 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Thu Jul 20 12:04:47 2000 +0200
@@ -136,7 +136,7 @@
$y\in B$. If $y = 0$ then $y \leq \idt{max}\ap c\ap 0$: *}
fix y assume "y = (#0::real)"
- show "y <= b" by (simp! add: le_max2)
+ show "y <= b" by (simp! add: le_maxI2)
txt{* The second case is
$y = {|f\ap x|}/{\norm x}$ for some
@@ -184,7 +184,7 @@
by (rule not_sym, rule lt_imp_not_eq,
rule normed_vs_norm_gt_zero)
qed
- also have "c * ... <= b " by (simp! add: le_max1)
+ also have "c * ... <= b " by (simp! add: le_maxI1)
finally show "y <= b" .
qed simp
qed
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Wed Jul 19 18:57:27 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Thu Jul 20 12:04:47 2000 +0200
@@ -78,23 +78,23 @@
-- {* Define $M$ as the set of all norm-preserving extensions of $F$. \skp *}
{
fix c assume "c \\<in> chain M" "\\<exists>x. x \\<in> c"
- have "\\<Union> c \\<in> M"
+ have "\\<Union>c \\<in> M"
-- {* Show that every non-empty chain $c$ of $M$ has an upper bound in $M$: *}
-- {* $\Union c$ is greater than any element of the chain $c$, so it suffices to show $\Union c \in M$. *}
proof (unfold M_def, rule norm_pres_extensionI)
- show "\\<exists>H h. graph H h = \\<Union> c
+ show "\\<exists>H h. graph H h = \\<Union>c
\\<and> is_linearform H h
\\<and> is_subspace H E
\\<and> is_subspace F H
\\<and> graph F f \\<subseteq> graph H h
\\<and> (\\<forall>x \\<in> H. h x <= p x)"
proof (intro exI conjI)
- let ?H = "domain (\\<Union> c)"
- let ?h = "funct (\\<Union> c)"
+ let ?H = "domain (\\<Union>c)"
+ let ?h = "funct (\\<Union>c)"
- show a: "graph ?H ?h = \\<Union> c"
+ show a: "graph ?H ?h = \\<Union>c"
proof (rule graph_domain_funct)
- fix x y z assume "(x, y) \\<in> \\<Union> c" "(x, z) \\<in> \\<Union> c"
+ fix x y z assume "(x, y) \\<in> \\<Union>c" "(x, z) \\<in> \\<Union>c"
show "z = y" by (rule sup_definite)
qed
show "is_linearform ?H ?h"
@@ -214,7 +214,7 @@
fix t assume "t \\<in> H"
have "(SOME (y, a). t = y + a \\<cdot> x' \\<and> y \\<in> H)
= (t, #0)"
- by (rule decomp_H'_H) (assumption+, rule x');
+ by (rule decomp_H'_H) (assumption+, rule x')
thus "h t = h' t" by (simp! add: Let_def)
next
show "H \\<subseteq> H'"
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Wed Jul 19 18:57:27 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Thu Jul 20 12:04:47 2000 +0200
@@ -270,10 +270,10 @@
txt{* Now we show
$h\ap y + a \cdot \xi\leq p\ap (y\plus a \mult x_0)$
- by case analysis on $a$. \label{linorder_linear_split}*};
+ by case analysis on $a$. *};
also; have "... <= p (y + a \\<cdot> x0)";
- proof (rule linorder_linear_split);
+ proof (rule linorder_less_split);
assume z: "a = #0";
with vs y a; show ?thesis; by simp;
--- a/src/HOL/Real/HahnBanach/HahnBanachLemmas.thy Wed Jul 19 18:57:27 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachLemmas.thy Thu Jul 20 12:04:47 2000 +0200
@@ -1,3 +1,3 @@
-theory HahnBanachLemmas = HahnBanachSupLemmas + HahnBanachExtLemmas:;
-end;
+theory HahnBanachLemmas = HahnBanachSupLemmas + HahnBanachExtLemmas:
+end
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Wed Jul 19 18:57:27 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Thu Jul 20 12:04:47 2000 +0200
@@ -25,17 +25,17 @@
lemma some_H'h't:
"[| M = norm_pres_extensions E p F f; c \\<in> chain M;
- graph H h = \\<Union> c; x \\<in> H |]
+ graph H h = \\<Union>c; x \\<in> H |]
==> \\<exists>H' h'. graph H' h' \\<in> c \\<and> (x, h x) \\<in> graph H' h'
\\<and> is_linearform H' h' \\<and> is_subspace H' E
\\<and> is_subspace F H' \\<and> graph F f \\<subseteq> graph H' h'
\\<and> (\\<forall>x \\<in> H'. h' x <= p x)"
proof -
assume m: "M = norm_pres_extensions E p F f" and "c \\<in> chain M"
- and u: "graph H h = \\<Union> c" "x \\<in> H"
+ and u: "graph H h = \\<Union>c" "x \\<in> H"
have h: "(x, h x) \\<in> graph H h" ..
- with u have "(x, h x) \\<in> \\<Union> c" by simp
+ with u have "(x, h x) \\<in> \\<Union>c" by simp
hence ex1: "\\<exists>g \\<in> c. (x, h x) \\<in> g"
by (simp only: Union_iff)
thus ?thesis
@@ -75,13 +75,13 @@
lemma some_H'h':
"[| M = norm_pres_extensions E p F f; c \\<in> chain M;
- graph H h = \\<Union> c; x \\<in> H |]
+ graph H h = \\<Union>c; x \\<in> H |]
==> \\<exists>H' h'. x \\<in> H' \\<and> graph H' h' \\<subseteq> graph H h
\\<and> is_linearform H' h' \\<and> is_subspace H' E \\<and> is_subspace F H'
\\<and> graph F f \\<subseteq> graph H' h' \\<and> (\\<forall>x \\<in> H'. h' x <= p x)"
proof -
assume "M = norm_pres_extensions E p F f" and cM: "c \\<in> chain M"
- and u: "graph H h = \\<Union> c" "x \\<in> H"
+ and u: "graph H h = \\<Union>c" "x \\<in> H"
have "\\<exists>H' h'. graph H' h' \\<in> c \\<and> (x, h x) \\<in> graph H' h'
\\<and> is_linearform H' h' \\<and> is_subspace H' E
@@ -109,13 +109,13 @@
lemma some_H'h'2:
"[| M = norm_pres_extensions E p F f; c \\<in> chain M;
- graph H h = \\<Union> c; x \\<in> H; y \\<in> H |]
+ graph H h = \\<Union>c; x \\<in> H; y \\<in> H |]
==> \\<exists>H' h'. x \\<in> H' \\<and> y \\<in> H' \\<and> graph H' h' \\<subseteq> graph H h
\\<and> is_linearform H' h' \\<and> is_subspace H' E \\<and> is_subspace F H'
\\<and> graph F f \\<subseteq> graph H' h' \\<and> (\\<forall>x \\<in> H'. h' x <= p x)"
proof -
assume "M = norm_pres_extensions E p F f" "c \\<in> chain M"
- "graph H h = \\<Union> c" "x \\<in> H" "y \\<in> H"
+ "graph H h = \\<Union>c" "x \\<in> H" "y \\<in> H"
txt {* $x$ is in the domain $H'$ of some function $h'$,
such that $h$ extends $h'$. *}
@@ -188,10 +188,10 @@
lemma sup_definite:
"[| M == norm_pres_extensions E p F f; c \\<in> chain M;
- (x, y) \\<in> \\<Union> c; (x, z) \\<in> \\<Union> c |] ==> z = y"
+ (x, y) \\<in> \\<Union>c; (x, z) \\<in> \\<Union>c |] ==> z = y"
proof -
assume "c \\<in> chain M" "M == norm_pres_extensions E p F f"
- "(x, y) \\<in> \\<Union> c" "(x, z) \\<in> \\<Union> c"
+ "(x, y) \\<in> \\<Union>c" "(x, z) \\<in> \\<Union>c"
thus ?thesis
proof (elim UnionE chainE2)
@@ -245,10 +245,10 @@
lemma sup_lf:
"[| M = norm_pres_extensions E p F f; c \\<in> chain M;
- graph H h = \\<Union> c |] ==> is_linearform H h"
+ graph H h = \\<Union>c |] ==> is_linearform H h"
proof -
assume "M = norm_pres_extensions E p F f" "c \\<in> chain M"
- "graph H h = \\<Union> c"
+ "graph H h = \\<Union>c"
show "is_linearform H h"
proof
@@ -306,11 +306,11 @@
for every element of the chain.*}
lemma sup_ext:
- "[| graph H h = \\<Union> c; M = norm_pres_extensions E p F f;
+ "[| graph H h = \\<Union>c; M = norm_pres_extensions E p F f;
c \\<in> chain M; \\<exists>x. x \\<in> c |] ==> graph F f \\<subseteq> graph H h"
proof -
assume "M = norm_pres_extensions E p F f" "c \\<in> chain M"
- "graph H h = \\<Union> c"
+ "graph H h = \\<Union>c"
assume "\\<exists>x. x \\<in> c"
thus ?thesis
proof
@@ -332,8 +332,8 @@
fix G g assume "graph F f \\<subseteq> graph G g"
also assume "graph G g = x"
also have "... \\<in> c" .
- hence "x \\<subseteq> \\<Union> c" by fast
- also have [RS sym]: "graph H h = \\<Union> c" .
+ hence "x \\<subseteq> \\<Union>c" by fast
+ also have [RS sym]: "graph H h = \\<Union>c" .
finally show ?thesis .
qed
qed
@@ -345,12 +345,12 @@
vector space. *}
lemma sup_supF:
- "[| graph H h = \\<Union> c; M = norm_pres_extensions E p F f;
+ "[| graph H h = \\<Union>c; M = norm_pres_extensions E p F f;
c \\<in> chain M; \\<exists>x. x \\<in> c; is_subspace F E; is_vectorspace E |]
==> is_subspace F H"
proof -
assume "M = norm_pres_extensions E p F f" "c \\<in> chain M" "\\<exists>x. x \\<in> c"
- "graph H h = \\<Union> c" "is_subspace F E" "is_vectorspace E"
+ "graph H h = \\<Union>c" "is_subspace F E" "is_vectorspace E"
show ?thesis
proof
@@ -377,12 +377,12 @@
of $E$. *}
lemma sup_subE:
- "[| graph H h = \\<Union> c; M = norm_pres_extensions E p F f;
+ "[| graph H h = \\<Union>c; M = norm_pres_extensions E p F f;
c \\<in> chain M; \\<exists>x. x \\<in> c; is_subspace F E; is_vectorspace E |]
==> is_subspace H E"
proof -
assume "M = norm_pres_extensions E p F f" "c \\<in> chain M" "\\<exists>x. x \\<in> c"
- "graph H h = \\<Union> c" "is_subspace F E" "is_vectorspace E"
+ "graph H h = \\<Union>c" "is_subspace F E" "is_vectorspace E"
show ?thesis
proof
@@ -461,11 +461,11 @@
*}
lemma sup_norm_pres:
- "[| graph H h = \\<Union> c; M = norm_pres_extensions E p F f;
+ "[| graph H h = \\<Union>c; M = norm_pres_extensions E p F f;
c \\<in> chain M |] ==> \\<forall>x \\<in> H. h x <= p x"
proof
assume "M = norm_pres_extensions E p F f" "c \\<in> chain M"
- "graph H h = \\<Union> c"
+ "graph H h = \\<Union>c"
fix x assume "x \\<in> H"
have "\\<exists>H' h'. x \\<in> H' \\<and> graph H' h' \\<subseteq> graph H h
\\<and> is_linearform H' h' \\<and> is_subspace H' E \\<and> is_subspace F H'
--- a/src/HOL/Real/HahnBanach/document/notation.tex Wed Jul 19 18:57:27 2000 +0200
+++ b/src/HOL/Real/HahnBanach/document/notation.tex Thu Jul 20 12:04:47 2000 +0200
@@ -24,7 +24,8 @@
\newcommand{\Le}{\leq}
\newcommand{\Lt}{\lt}
\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
-\newcommand{\ap}{\mathpalette{\mathbin{\!}}{\mathbin{\!}}{\mathbin{}}{\mathbin{}}}
+%\newcommand{\ap}{\mathpalette{\mathbin{\!}}{\mathbin{\!}}{\mathbin{}}{\mathbin{}}}
+\newcommand{\ap}{\mathpalette{\mathbin{}}{\mathbin{}}{\mathbin{}}{\mathbin{}}}
\newcommand{\Union}{\bigcup}
\newcommand{\Un}{\cup}
\newcommand{\Int}{\cap}