--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Thu Apr 13 15:01:50 2000 +0200
@@ -52,27 +52,27 @@
txt {* The set $S$ is non-empty, since $a\ap\zero \in S$: *};
- from vs; have "a <0> : ?S"; by force;
+ from vs; have "a 00 : ?S"; by force;
thus "EX X. X : ?S"; ..;
txt {* $b\ap \zero$ is an upper bound of $S$: *};
show "EX Y. isUb UNIV ?S Y";
proof;
- show "isUb UNIV ?S (b <0>)";
+ show "isUb UNIV ?S (b 00)";
proof (intro isUbI setleI ballI);
- show "b <0> : UNIV"; ..;
+ show "b 00 : UNIV"; ..;
next;
txt {* Every element $y\in S$ is less than $b\ap \zero$: *};
fix y; assume y: "y : ?S";
from y; have "EX u:F. y = a u"; by fast;
- thus "y <= b <0>";
+ thus "y <= b 00";
proof;
fix u; assume "u:F";
assume "y = a u";
- also; have "a u <= b <0>"; by (rule r) (simp!)+;
+ also; have "a u <= b 00"; by (rule r) (simp!)+;
finally; show ?thesis; .;
qed;
qed;
@@ -121,18 +121,18 @@
is a linear extension of $h$ to $H_0$. *};
lemma h0_lf:
- "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H
+ "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H
in h y + a * xi);
H0 == H + lin x0; is_subspace H E; is_linearform H h; x0 ~: H;
- x0 : E; x0 ~= <0>; is_vectorspace E |]
+ x0 : E; x0 ~= 00; is_vectorspace E |]
==> is_linearform H0 h0";
proof -;
assume h0_def:
- "h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H
+ "h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H
in h y + a * xi)"
and H0_def: "H0 == H + lin x0"
and vs: "is_subspace H E" "is_linearform H h" "x0 ~: H"
- "x0 ~= <0>" "x0 : E" "is_vectorspace E";
+ "x0 ~= 00" "x0 : E" "is_vectorspace E";
have h0: "is_vectorspace H0";
proof (unfold H0_def, rule vs_sum_vs);
@@ -150,27 +150,27 @@
have x1x2: "x1 + x2 : H0";
by (rule vs_add_closed, rule h0);
from x1;
- have ex_x1: "EX y1 a1. x1 = y1 + a1 <*> x0 & y1 : H";
+ have ex_x1: "EX y1 a1. x1 = y1 + a1 (*) x0 & y1 : H";
by (unfold H0_def vs_sum_def lin_def) fast;
from x2;
- have ex_x2: "EX y2 a2. x2 = y2 + a2 <*> x0 & y2 : H";
+ have ex_x2: "EX y2 a2. x2 = y2 + a2 (*) x0 & y2 : H";
by (unfold H0_def vs_sum_def lin_def) fast;
from x1x2;
- have ex_x1x2: "EX y a. x1 + x2 = y + a <*> x0 & y : H";
+ have ex_x1x2: "EX y a. x1 + x2 = y + a (*) x0 & y : H";
by (unfold H0_def vs_sum_def lin_def) fast;
from ex_x1 ex_x2 ex_x1x2;
show "h0 (x1 + x2) = h0 x1 + h0 x2";
proof (elim exE conjE);
fix y1 y2 y a1 a2 a;
- assume y1: "x1 = y1 + a1 <*> x0" and y1': "y1 : H"
- and y2: "x2 = y2 + a2 <*> x0" and y2': "y2 : H"
- and y: "x1 + x2 = y + a <*> x0" and y': "y : H";
+ assume y1: "x1 = y1 + a1 (*) x0" and y1': "y1 : H"
+ and y2: "x2 = y2 + a2 (*) x0" and y2': "y2 : H"
+ and y: "x1 + x2 = y + a (*) x0" and y': "y : H";
have ya: "y1 + y2 = y & a1 + a2 = a";
proof (rule decomp_H0);;
txt_raw {* \label{decomp-H0-use} *};;
- show "y1 + y2 + (a1 + a2) <*> x0 = y + a <*> x0";
+ show "y1 + y2 + (a1 + a2) (*) x0 = y + a (*) x0";
by (simp! add: vs_add_mult_distrib2 [of E]);
show "y1 + y2 : H"; ..;
qed;
@@ -199,31 +199,31 @@
next;
fix c x1; assume x1: "x1 : H0";
- have ax1: "c <*> x1 : H0";
+ have ax1: "c (*) x1 : H0";
by (rule vs_mult_closed, rule h0);
from x1; have ex_x: "!! x. x: H0
- ==> EX y a. x = y + a <*> x0 & y : H";
+ ==> EX y a. x = y + a (*) x0 & y : H";
by (unfold H0_def vs_sum_def lin_def) fast;
- from x1; have ex_x1: "EX y1 a1. x1 = y1 + a1 <*> x0 & y1 : H";
+ from x1; have ex_x1: "EX y1 a1. x1 = y1 + a1 (*) x0 & y1 : H";
by (unfold H0_def vs_sum_def lin_def) fast;
- with ex_x [of "c <*> x1", OF ax1];
- show "h0 (c <*> x1) = c * (h0 x1)";
+ with ex_x [of "c (*) x1", OF ax1];
+ show "h0 (c (*) x1) = c * (h0 x1)";
proof (elim exE conjE);
fix y1 y a1 a;
- assume y1: "x1 = y1 + a1 <*> x0" and y1': "y1 : H"
- and y: "c <*> x1 = y + a <*> x0" and y': "y : H";
+ assume y1: "x1 = y1 + a1 (*) x0" and y1': "y1 : H"
+ and y: "c (*) x1 = y + a (*) x0" and y': "y : H";
- have ya: "c <*> y1 = y & c * a1 = a";
+ have ya: "c (*) y1 = y & c * a1 = a";
proof (rule decomp_H0);
- show "c <*> y1 + (c * a1) <*> x0 = y + a <*> x0";
+ show "c (*) y1 + (c * a1) (*) x0 = y + a (*) x0";
by (simp! add: add: vs_add_mult_distrib1);
- show "c <*> y1 : H"; ..;
+ show "c (*) y1 : H"; ..;
qed;
- have "h0 (c <*> x1) = h y + a * xi";
+ have "h0 (c (*) x1) = h y + a * xi";
by (rule h0_definite);
- also; have "... = h (c <*> y1) + (c * a1) * xi";
+ also; have "... = h (c (*) y1) + (c * a1) * xi";
by (simp add: ya);
also; from vs y1'; have "... = c * h y1 + c * a1 * xi";
by (simp add: linearform_mult [of H]);
@@ -240,31 +240,31 @@
is bounded by the seminorm $p$. *};
lemma h0_norm_pres:
- "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H
+ "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H
in h y + a * xi);
- H0 == H + lin x0; x0 ~: H; x0 : E; x0 ~= <0>; is_vectorspace E;
+ H0 == H + lin x0; x0 ~: H; x0 : E; x0 ~= 00; is_vectorspace E;
is_subspace H E; is_seminorm E p; is_linearform H h; ALL y:H. h y <= p y;
ALL y:H. - p (y + x0) - h y <= xi & xi <= p (y + x0) - h y |]
==> ALL x:H0. h0 x <= p x";
proof;
assume h0_def:
- "h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H
+ "h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H
in (h y) + a * xi)"
and H0_def: "H0 == H + lin x0"
- and vs: "x0 ~: H" "x0 : E" "x0 ~= <0>" "is_vectorspace E"
+ and vs: "x0 ~: H" "x0 : E" "x0 ~= 00" "is_vectorspace E"
"is_subspace H E" "is_seminorm E p" "is_linearform H h"
and a: "ALL y:H. h y <= p y";
presume a1: "ALL ya:H. - p (ya + x0) - h ya <= xi";
presume a2: "ALL ya:H. xi <= p (ya + x0) - h ya";
fix x; assume "x : H0";
have ex_x:
- "!! x. x : H0 ==> EX y a. x = y + a <*> x0 & y : H";
+ "!! x. x : H0 ==> EX y a. x = y + a (*) x0 & y : H";
by (unfold H0_def vs_sum_def lin_def) fast;
- have "EX y a. x = y + a <*> x0 & y : H";
+ have "EX y a. x = y + a (*) x0 & y : H";
by (rule ex_x);
thus "h0 x <= p x";
proof (elim exE conjE);
- fix y a; assume x: "x = y + a <*> x0" and y: "y : H";
+ fix y a; assume x: "x = y + a (*) x0" and y: "y : H";
have "h0 x = h y + a * xi";
by (rule h0_definite);
@@ -272,7 +272,7 @@
$h\ap y + a \cdot \xi\leq p\ap (y\plus a \mult x_0)$
by case analysis on $a$. \label{linorder_linear_split}*};
- also; have "... <= p (y + a <*> x0)";
+ also; have "... <= p (y + a (*) x0)";
proof (rule linorder_linear_split);
assume z: "a = 0r";
@@ -284,27 +284,27 @@
next;
assume lz: "a < 0r"; hence nz: "a ~= 0r"; by simp;
from a1;
- have "- p (rinv a <*> y + x0) - h (rinv a <*> y) <= xi";
+ have "- p (rinv a (*) y + x0) - h (rinv a (*) y) <= xi";
by (rule bspec) (simp!);
txt {* The thesis for this case now follows by a short
calculation. *};
hence "a * xi
- <= a * (- p (rinv a <*> y + x0) - h (rinv a <*> y))";
+ <= a * (- p (rinv a (*) y + x0) - h (rinv a (*) y))";
by (rule real_mult_less_le_anti [OF lz]);
- also; have "... = - a * (p (rinv a <*> y + x0))
- - a * (h (rinv a <*> y))";
+ also; have "... = - a * (p (rinv a (*) y + x0))
+ - a * (h (rinv a (*) y))";
by (rule real_mult_diff_distrib);
- also; from lz vs y; have "- a * (p (rinv a <*> y + x0))
- = p (a <*> (rinv a <*> y + x0))";
+ also; from lz vs y; have "- a * (p (rinv a (*) y + x0))
+ = p (a (*) (rinv a (*) y + x0))";
by (simp add: seminorm_rabs_homogenous rabs_minus_eqI2);
- also; from nz vs y; have "... = p (y + a <*> x0)";
+ also; from nz vs y; have "... = p (y + a (*) x0)";
by (simp add: vs_add_mult_distrib1);
- also; from nz vs y; have "a * (h (rinv a <*> y)) = h y";
+ also; from nz vs y; have "a * (h (rinv a (*) y)) = h y";
by (simp add: linearform_mult [RS sym]);
- finally; have "a * xi <= p (y + a <*> x0) - h y"; .;
+ finally; have "a * xi <= p (y + a (*) x0) - h y"; .;
- hence "h y + a * xi <= h y + p (y + a <*> x0) - h y";
+ hence "h y + a * xi <= h y + p (y + a (*) x0) - h y";
by (simp add: real_add_left_cancel_le);
thus ?thesis; by simp;
@@ -314,30 +314,30 @@
next;
assume gz: "0r < a"; hence nz: "a ~= 0r"; by simp;
from a2;
- have "xi <= p (rinv a <*> y + x0) - h (rinv a <*> y)";
+ have "xi <= p (rinv a (*) y + x0) - h (rinv a (*) y)";
by (rule bspec) (simp!);
txt {* The thesis for this case follows by a short
calculation: *};
with gz; have "a * xi
- <= a * (p (rinv a <*> y + x0) - h (rinv a <*> y))";
+ <= a * (p (rinv a (*) y + x0) - h (rinv a (*) y))";
by (rule real_mult_less_le_mono);
- also; have "... = a * p (rinv a <*> y + x0)
- - a * h (rinv a <*> y)";
+ also; have "... = a * p (rinv a (*) y + x0)
+ - a * h (rinv a (*) y)";
by (rule real_mult_diff_distrib2);
also; from gz vs y;
- have "a * p (rinv a <*> y + x0)
- = p (a <*> (rinv a <*> y + x0))";
+ have "a * p (rinv a (*) y + x0)
+ = p (a (*) (rinv a (*) y + x0))";
by (simp add: seminorm_rabs_homogenous rabs_eqI2);
also; from nz vs y;
- have "... = p (y + a <*> x0)";
+ have "... = p (y + a (*) x0)";
by (simp add: vs_add_mult_distrib1);
- also; from nz vs y; have "a * h (rinv a <*> y) = h y";
+ also; from nz vs y; have "a * h (rinv a (*) y) = h y";
by (simp add: linearform_mult [RS sym]);
- finally; have "a * xi <= p (y + a <*> x0) - h y"; .;
+ finally; have "a * xi <= p (y + a (*) x0) - h y"; .;
- hence "h y + a * xi <= h y + (p (y + a <*> x0) - h y)";
+ hence "h y + a * xi <= h y + (p (y + a (*) x0) - h y)";
by (simp add: real_add_left_cancel_le);
thus ?thesis; by simp;
qed;