--- a/src/HOL/Real/HahnBanach/Aux.thy Tue Sep 21 17:30:55 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy Tue Sep 21 17:31:20 1999 +0200
@@ -1,16 +1,31 @@
+(* Title: HOL/Real/HahnBanach/Aux.thy
+ ID: $Id$
+ Author: Gertrud Bauer, TU Munich
+*)
-theory Aux = Main + Real:;
+theory Aux = Real:;
+theorems case = case_split_thm; (* FIXME tmp *);
+
+lemmas CollectE = CollectD [elimify];
theorem [trans]: "[| (x::'a::order) <= y; x ~= y |] ==> x < y"; (* <= ~= < *)
- by (asm_simp add: order_less_le);
+ by (simp! add: order_less_le);
+
+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]);
lemma lt_imp_not_eq: "x < (y::'a::order) ==> x ~= y";
by (rule order_less_le[RS iffD1, RS conjunct2]);
-lemma Int_singeltonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v";
+lemma Int_singletonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v";
by (fast elim: equalityE);
+lemmas singletonE = singletonD[elimify];
+
lemma real_add_minus_eq: "x - y = 0r ==> x = y";
proof -;
assume "x - y = 0r";
@@ -18,7 +33,7 @@
also; have "... = 0r"; .;
finally; have "x + - y = 0r"; .;
hence "x = - (- y)"; by (rule real_add_minus_eq_minus);
- also; have "... = y"; by asm_simp;
+ also; have "... = y"; by (simp!);
finally; show "x = y"; .;
qed;
@@ -29,8 +44,8 @@
show "-1r < 0r";
by (rule real_minus_zero_less_iff[RS iffD1], simp, rule real_zero_less_one);
qed;
- also; have "... = 1r"; by asm_simp;
- finally; show ?thesis; by asm_simp;
+ also; have "... = 1r"; by (simp!);
+ finally; show ?thesis; by (simp!);
qed;
axioms real_mult_le_le_mono2: "[| 0r <= z; x <= y |] ==> x * z <= y * z";
@@ -39,21 +54,21 @@
axioms real_mult_less_le_mono: "[| 0r < z; x <= y |] ==> z * x <= z * y";
-axioms real_mult_diff_distrib: "a * (- x - y) = - a * x - a * y";
+axioms real_mult_diff_distrib: "a * (- x - (y::real)) = - a * x - a * y";
-axioms real_mult_diff_distrib2: "a * (x - y) = a * x - a * y";
+axioms real_mult_diff_distrib2: "a * (x - (y::real)) = a * x - a * y";
lemma less_imp_le: "(x::real) < y ==> x <= y";
- by (asm_simp only: real_less_imp_le);
+ by (simp! only: real_less_imp_le);
lemma le_noteq_imp_less: "[|x <= (r::'a::order); x ~= r |] ==> x < r";
proof -;
assume "x <= (r::'a::order)";
assume "x ~= r";
then; have "x < r | x = r";
- by (asm_simp add: order_le_less);
+ by (simp! add: order_le_less);
then; show ?thesis;
- by asm_simp;
+ by (simp!);
qed;
lemma minus_le: "- (x::real) <= y ==> - y <= x";
@@ -65,11 +80,11 @@
assume "- x < y"; show ?thesis;
proof -;
have "- y < - (- x)"; by (rule real_less_swap_iff [RS iffD1]);
- hence "- y < x"; by asm_simp;
+ hence "- y < x"; by (simp!);
thus ?thesis; by (rule real_less_imp_le);
qed;
next;
- assume "- x = y"; show ?thesis; by force;
+ assume "- x = y"; show ?thesis; by (force!);
qed;
qed;
@@ -82,14 +97,14 @@
show "- r <= x & x <= r";
proof;
have "- x <= rabs x"; by (rule rabs_ge_minus_self);
- hence "- x <= r"; by asm_simp;
- thus "- r <= x"; by (asm_simp add : minus_le [of "x" "r"]);
+ hence "- x <= r"; by (simp!);
+ thus "- r <= x"; by (simp! add : minus_le [of "x" "r"]);
have "x <= rabs x"; by (rule rabs_ge_self);
- thus "x <= r"; by asm_simp;
+ thus "x <= r"; by (simp!);
qed;
next;
assume "- r <= x & x <= r";
- show "rabs x <= r"; by fast;
+ show "rabs x <= r"; by (fast!);
qed;
next;
assume "rabs x ~= r";
@@ -113,10 +128,10 @@
show ?thesis;
proof (rule rabs_disj [RS disjE, of x]);
assume "rabs x = x";
- show ?thesis; by asm_simp;
+ show ?thesis; by (simp!);
next;
assume "rabs x = - x";
- from minus_le [of r x]; show ?thesis; by asm_simp;
+ from minus_le [of r x]; show ?thesis; by (simp!);
qed;
qed;
qed;
--- a/src/HOL/Real/HahnBanach/Bounds.thy Tue Sep 21 17:30:55 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Bounds.thy Tue Sep 21 17:31:20 1999 +0200
@@ -1,3 +1,7 @@
+(* Title: HOL/Real/HahnBanach/Bounds.thy
+ ID: $Id$
+ Author: Gertrud Bauer, TU Munich
+*)
theory Bounds = Main + Real:;
@@ -60,8 +64,6 @@
is_Sup :: "('a::order) set => 'a set => 'a => bool"
"is_Sup A B x == isLub A B x"
- (* was: x:A & is_Least (UpperBounds A B) x" *)
-
Sup :: "('a::order) set => 'a set => 'a"
"Sup A B == Eps (is_Sup A B)"
@@ -84,9 +86,6 @@
"INF x. P" == "INF x:UNIV. P";
-lemma [intro]: "[| x:A; !!y. y:B ==> y <= x |] ==> x: UpperBounds A B";
- by (unfold UpperBounds_def is_UpperBound_def) force;
-
lemma ub_ge_sup: "isUb A B y ==> is_Sup A B s ==> s <= y";
by (unfold is_Sup_def, rule isLub_le_isUb);
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Tue Sep 21 17:30:55 1999 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Tue Sep 21 17:31:20 1999 +0200
@@ -1,15 +1,17 @@
+(* Title: HOL/Real/HahnBanach/FunctionNorm.thy
+ ID: $Id$
+ Author: Gertrud Bauer, TU Munich
+*)
theory FunctionNorm = NormedSpace + FunctionOrder:;
-theorems [elim!!] = bspec;
-
constdefs
is_continous :: "['a set, 'a => real, 'a => real] => bool"
"is_continous V norm f == (is_linearform V f
& (EX c. ALL x:V. rabs (f x) <= c * norm x))";
-lemma lipschitz_continous_I:
+lemma lipschitz_continousI [intro]:
"[| is_linearform V f; !! x. x:V ==> rabs (f x) <= c * norm x |]
==> is_continous V norm f";
proof (unfold is_continous_def, intro exI conjI ballI);
@@ -17,10 +19,11 @@
fix x; assume "x:V"; show "rabs (f x) <= c * norm x"; by (rule r);
qed;
-lemma continous_linearform: "is_continous V norm f ==> is_linearform V f";
+lemma continous_linearform [intro!!]: "is_continous V norm f ==> is_linearform V f";
by (unfold is_continous_def) force;
-lemma continous_bounded: "is_continous V norm f ==> EX c. ALL x:V. rabs (f x) <= c * norm x";
+lemma continous_bounded [intro!!]:
+ "is_continous V norm f ==> EX c. ALL x:V. rabs (f x) <= c * norm x";
by (unfold is_continous_def) force;
constdefs
@@ -40,13 +43,7 @@
lemma B_not_empty: "0r : B V norm f";
by (unfold B_def, 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]);
-
-lemma ex_fnorm:
+lemma ex_fnorm [intro!!]:
"[| is_normed_vectorspace V norm; is_continous V norm f|]
==> is_function_norm V norm f (function_norm V norm f)";
proof (unfold function_norm_def is_function_norm_def is_continous_def Sup_def, elim conjE,
@@ -67,56 +64,70 @@
show "EX Y. isUb UNIV (B V norm f) Y";
proof (intro exI isUbI setleI ballI, unfold B_def,
- elim CollectD [elimify] disjE bexE conjE);
+ elim CollectE disjE bexE conjE);
fix x y; assume "x:V" "x ~= <0>" "y = rabs (f x) * rinv (norm x)";
from a; have le: "rabs (f x) <= c * norm x"; ..;
have "y = rabs (f x) * rinv (norm x)";.;
also; from _ le; have "... <= c * norm x * rinv (norm x)";
proof (rule real_mult_le_le_mono2);
show "0r <= rinv (norm x)";
- by (rule less_imp_le, rule real_rinv_gt_zero, rule normed_vs_norm_gt_zero);
+ proof (rule less_imp_le);
+ show "0r < rinv (norm x)";
+ proof (rule real_rinv_gt_zero);
+ show "0r < norm x"; ..;
+ qed;
+ qed;
+ (*** or: by (rule less_imp_le, rule real_rinv_gt_zero, rule normed_vs_norm_gt_zero); ***)
qed;
also; have "... = c * (norm x * rinv (norm x))"; by (rule real_mult_assoc);
also; have "(norm x * rinv (norm x)) = 1r";
proof (rule real_mult_inv_right);
show "norm x ~= 0r";
- by (rule not_sym, rule lt_imp_not_eq, rule normed_vs_norm_gt_zero);
+ proof (rule not_sym);
+ show "0r ~= norm x";
+ proof (rule lt_imp_not_eq);
+ show "0r < norm x"; ..;
+ qed;
+ qed;
+ (*** or: by (rule not_sym, rule lt_imp_not_eq, rule normed_vs_norm_gt_zero); ***)
qed;
- also; have "c * ... = c"; by asm_simp;
- also; have "... <= b"; by (asm_simp add: le_max1);
+ also; have "c * ... = c"; by (simp!);
+ also; have "... <= b"; by (simp! add: le_max1);
finally; show "y <= b"; .;
next;
- fix y; assume "y = 0r"; show "y <= b"; by (asm_simp add: le_max2);
+ fix y; assume "y = 0r"; show "y <= b"; by (simp! add: le_max2);
qed simp;
qed;
qed;
qed;
-lemma fnorm_ge_zero: "[| is_continous V norm f; is_normed_vectorspace V norm|]
+lemma fnorm_ge_zero [intro!!]: "[| is_continous V norm f; is_normed_vectorspace V norm|]
==> 0r <= function_norm V norm f";
proof -;
assume c: "is_continous V norm f" and n: "is_normed_vectorspace V norm";
- have "is_function_norm V norm f (function_norm V norm f)"; by (rule ex_fnorm);
+ have "is_function_norm V norm f (function_norm V norm f)"; ..;
hence s: "is_Sup UNIV (B V norm f) (function_norm V norm f)";
by (simp add: is_function_norm_def);
show ?thesis;
proof (unfold function_norm_def, rule sup_ub1);
show "ALL x:(B V norm f). 0r <= x";
- proof (intro ballI, unfold B_def, elim CollectD [elimify] bexE conjE disjE);
- fix x r; assume "is_normed_vectorspace V norm" "x : V" "x ~= <0>"
+ proof (intro ballI, unfold B_def, elim CollectE bexE conjE disjE);
+ fix x r; assume "x : V" "x ~= <0>"
"r = rabs (f x) * rinv (norm x)";
show "0r <= r";
- proof (asm_simp, rule real_le_mult_order);
- show "0r <= rabs (f x)"; by (asm_simp only: rabs_ge_zero);
+ proof (simp!, rule real_le_mult_order);
+ show "0r <= rabs (f x)"; by (simp! only: rabs_ge_zero);
show "0r <= rinv (norm x)";
proof (rule less_imp_le);
show "0r < rinv (norm x)";
- by (rule real_rinv_gt_zero, rule normed_vs_norm_gt_zero [of V norm]);
+ proof (rule real_rinv_gt_zero);
+ show "0r < norm x"; ..;
+ qed;
qed;
qed;
- qed asm_simp;
+ qed (simp!);
from ex_fnorm [OF n c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
- by (asm_simp add: is_function_norm_def function_norm_def);
+ by (simp! add: is_function_norm_def function_norm_def);
show "0r : B V norm f"; by (rule B_not_empty);
qed;
qed;
@@ -127,27 +138,31 @@
==> rabs (f x) <= (function_norm V norm f) * norm x";
proof -;
assume "is_normed_vectorspace V norm" "x:V" and c: "is_continous V norm f";
- have v: "is_vectorspace V"; by (rule normed_vs_vs);
+ have v: "is_vectorspace V"; ..;
assume "x:V";
show "?thesis";
proof (rule case [of "x = <0>"]);
assume "x ~= <0>";
show "?thesis";
proof -;
- have n: "0r <= norm x"; by (rule normed_vs_norm_ge_zero);
+ have n: "0r <= norm x"; ..;
have le: "rabs (f x) * rinv (norm x) <= function_norm V norm f";
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 (asm_simp add: is_function_norm_def function_norm_def);
+ by (simp! add: is_function_norm_def function_norm_def);
show "rabs (f x) * rinv (norm x) : B V norm f";
by (unfold B_def, intro CollectI disjI2 bexI [of _ x] conjI, simp);
qed;
- have "rabs (f x) = rabs (f x) * 1r"; by asm_simp;
+ have "rabs (f x) = rabs (f x) * 1r"; by (simp!);
also; have "1r = rinv (norm x) * norm x";
- by (rule real_mult_inv_left [RS sym], rule lt_imp_not_eq[RS not_sym],
- rule normed_vs_norm_gt_zero[of V norm]);
+ proof (rule real_mult_inv_left [RS sym]);
+ show "norm x ~= 0r";
+ proof (rule lt_imp_not_eq[RS not_sym]);
+ show "0r < norm x"; ..;
+ qed;
+ qed;
also; have "rabs (f x) * ... = rabs (f x) * rinv (norm x) * norm x";
- by (asm_simp add: real_mult_assoc [of "rabs (f x)"]);
+ by (simp! add: real_mult_assoc [of "rabs (f x)"]);
also; have "rabs (f x) * rinv (norm x) * norm x <= function_norm V norm f * norm x";
by (rule real_mult_le_le_mono2 [OF n le]);
finally; show "rabs (f x) <= function_norm V norm f * norm x"; .;
@@ -156,13 +171,13 @@
assume "x = <0>";
then; show "?thesis";
proof -;
- have "rabs (f x) = rabs (f <0>)"; by asm_simp;
- also; have "f <0> = 0r"; by (rule linearform_zero [OF v continous_linearform]);
+ have "rabs (f x) = rabs (f <0>)"; by (simp!);
+ also; from v continous_linearform; have "f <0> = 0r"; ..;
also; note rabs_zero;
also; have" 0r <= function_norm V norm f * norm x";
proof (rule real_le_mult_order);
- show "0r <= function_norm V norm f"; by (rule fnorm_ge_zero);
- show "0r <= norm x"; by (rule normed_vs_norm_ge_zero);
+ show "0r <= function_norm V norm f"; ..;
+ show "0r <= norm x"; ..;
qed;
finally; show "rabs (f x) <= function_norm V norm f * norm x"; .;
qed;
@@ -184,21 +199,24 @@
show "Sup UNIV (B V norm f) <= c";
proof (rule ub_ge_sup);
from ex_fnorm [OF _ c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
- by (asm_simp add: is_function_norm_def function_norm_def);
+ by (simp! add: is_function_norm_def function_norm_def);
show "isUb UNIV (B V norm f) c";
proof (intro isUbI setleI ballI);
fix y; assume "y: B V norm f";
- show le: "y <= c";
- proof (unfold B_def, elim CollectD [elimify] disjE bexE);
+ thus le: "y <= c";
+ proof (-, unfold B_def, elim CollectE disjE bexE);
fix x; assume Px: "x ~= <0> & y = rabs (f x) * rinv (norm x)";
assume x: "x : V";
- have lt: "0r < norm x";
- by (asm_simp add: normed_vs_norm_gt_zero);
- hence "0r ~= norm x"; by (asm_simp add: order_less_imp_not_eq);
- hence neq: "norm x ~= 0r"; by (rule not_sym);
-
+ have lt: "0r < norm x"; by (simp! add: normed_vs_norm_gt_zero);
+
+ have neq: "norm x ~= 0r";
+ proof (rule not_sym);
+ from lt; show "0r ~= norm x";
+ by (simp! add: order_less_imp_not_eq);
+ qed;
+
from lt; have "0r < rinv (norm x)";
- by (asm_simp add: real_rinv_gt_zero);
+ by (simp! add: real_rinv_gt_zero);
then; have inv_leq: "0r <= rinv (norm x)"; by (rule less_imp_le);
from Px; have "y = rabs (f x) * rinv (norm x)"; ..;
@@ -211,7 +229,7 @@
finally; show ?thesis; .;
next;
assume "y = 0r";
- show "y <= c"; by force;
+ show "y <= c"; by (force!);
qed;
qed force;
qed;
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy Tue Sep 21 17:30:55 1999 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy Tue Sep 21 17:31:20 1999 +0200
@@ -1,3 +1,7 @@
+(* Title: HOL/Real/HahnBanach/FunctionOrder.thy
+ ID: $Id$
+ Author: Gertrud Bauer, TU Munich
+*)
theory FunctionOrder = Subspace + Linearform:;
@@ -18,14 +22,30 @@
funct :: "'a graph => ('a => real)"
"funct g == %x. (@ y. (x, y):g)";
-lemma graph_I: "x:F ==> (x, f x) : graph F f";
+lemma graphI [intro!!]: "x:F ==> (x, f x) : graph F f";
by (unfold graph_def, intro CollectI exI) force;
-lemma graphD1: "(x, y): graph F f ==> x:F";
- by (unfold graph_def, elim CollectD [elimify] exE) force;
+lemma graphI2 [intro!!]: "x:F ==> EX t: (graph F f). t = (x, f x)";
+ by (unfold graph_def, force);
+
+lemma graphD1 [intro!!]: "(x, y): graph F f ==> x:F";
+ by (unfold graph_def, elim CollectE exE) force;
+
+lemma graphD2 [intro!!]: "(x, y): graph H h ==> y = h x";
+ by (unfold graph_def, elim CollectE exE) force;
-lemma graph_domain_funct: "(!!x y z. (x, y):g ==> (x, z):g ==> z = y) ==> graph (domain g) (funct g) = g";
-proof ( unfold domain_def, unfold funct_def, unfold graph_def, auto);
+lemma graph_extD1 [intro!!]: "[| graph H h <= graph H' h'; x:H |] ==> h x = h' x";
+ by (unfold graph_def, force);
+
+lemma graph_extD2 [intro!!]: "[| graph H h <= graph H' h' |] ==> H <= H'";
+ by (unfold graph_def, force);
+
+lemma graph_extI: "[| !! x. x: H ==> h x = h' x; H <= H'|] ==> graph H h <= graph H' h'";
+ by (unfold graph_def, force);
+
+lemma graph_domain_funct:
+ "(!!x y z. (x, y):g ==> (x, z):g ==> z = y) ==> graph (domain g) (funct g) = g";
+proof (unfold domain_def, unfold funct_def, unfold graph_def, auto);
fix a b; assume "(a, b) : g";
show "(a, SOME y. (a, y) : g) : g"; by (rule selectI2);
show "EX y. (a, y) : g"; ..;
@@ -36,22 +56,6 @@
qed;
qed;
-lemma graph_lemma1: "x:F ==> EX t: (graph F f). t = (x, f x)";
- by (unfold graph_def, force);
-
-lemma graph_lemma2: "(x, y): graph H h ==> y = h x";
- by (unfold graph_def, elim CollectD [elimify] exE) force;
-
-lemma graph_lemma3: "[| graph H h <= graph H' h'; x:H |] ==> h x = h' x";
- by (unfold graph_def, force);
-
-lemma graph_lemma4: "[| graph H h <= graph H' h' |] ==> H <= H'";
- by (unfold graph_def, force);
-
-lemma graph_lemma5: "[| !! x. x: H ==> h x = h' x; H <= H'|] ==> graph H h <= graph H' h'";
- by (unfold graph_def, force);
-
-
constdefs
norm_prev_extensions ::
"['a set, 'a => real, 'a set, 'a => real] => 'a graph set"
@@ -71,7 +75,7 @@
& (ALL x:H. h x <= p x))";
by (unfold norm_prev_extensions_def) force;
-lemma norm_prev_extension_I2 [intro]:
+lemma norm_prev_extensionI2 [intro]:
"[| is_linearform H h;
is_subspace H E;
is_subspace F H;
@@ -80,7 +84,7 @@
==> (graph H h : norm_prev_extensions E p F f)";
by (unfold norm_prev_extensions_def) force;
-lemma norm_prev_extension_I [intro]:
+lemma norm_prev_extensionI [intro]:
"(EX H h. graph H h = g
& is_linearform H h
& is_subspace H E
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Tue Sep 21 17:30:55 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Tue Sep 21 17:31:20 1999 +0200
@@ -1,10 +1,13 @@
+(* Title: HOL/Real/HahnBanach/HahnBanach.thy
+ ID: $Id$
+ Author: Gertrud Bauer, TU Munich
+*)
theory HahnBanach = HahnBanach_lemmas + HahnBanach_h0_lemmas:;
theorems [elim!!] = psubsetI;
-
theorem hahnbanach:
"[| is_vectorspace E; is_subspace F E; is_quasinorm E p; is_linearform F f;
ALL x:F. f x <= p x |]
@@ -14,12 +17,15 @@
proof -;
assume "is_vectorspace E" "is_subspace F E" "is_quasinorm E p" "is_linearform F f"
and "ALL x:F. f x <= p x";
- def M_def: M == "norm_prev_extensions E p F f";
+ def M == "norm_prev_extensions E p F f";
have aM: "graph F f : norm_prev_extensions E p F f";
- proof (rule norm_prev_extension_I2);
- show "is_subspace F F"; by (rule subspace_refl, rule subspace_vs);
- qed blast+;
+ proof (rule norm_prev_extensionI2);
+ show "is_subspace F F";
+ proof;
+ show "is_vectorspace F"; ..;
+ qed;
+ qed (blast!)+;
sect {* Part I a of the proof of the Hahn-Banach Theorem,
@@ -31,7 +37,7 @@
fix c; assume "c:chain M"; assume "EX x. x:c";
show "(Union c) : M";
- proof (unfold M_def, rule norm_prev_extension_I);
+ proof (unfold M_def, rule norm_prev_extensionI);
show "EX (H::'a set) h::'a => real. graph H h = Union c
& is_linearform H h
& is_subspace H E
@@ -47,24 +53,24 @@
proof (intro conjI);
show a: "graph ?H ?h = Union c";
proof (rule graph_domain_funct);
- fix x y z; assume "EX x. x : c" "(x, y) : Union c" "(x, z) : Union c";
+ fix x y z; assume "(x, y) : Union c" "(x, z) : Union c";
show "z = y"; by (rule sup_uniq);
qed;
show "is_linearform ?H ?h";
- by (asm_simp add: sup_lf a);
+ by (simp! add: sup_lf a);
show "is_subspace ?H E";
- by (rule sup_subE, rule a) asm_simp+;
+ by (rule sup_subE, rule a) (simp!)+;
show "is_subspace F ?H";
- by (rule sup_supF, rule a) asm_simp+;
+ by (rule sup_supF, rule a) (simp!)+;
show "graph F f <= graph ?H ?h";
- by (rule sup_ext, rule a) asm_simp+;
+ by (rule sup_ext, rule a) (simp!)+;
show "ALL x::'a:?H. ?h x <= p x";
- by (rule sup_norm_prev, rule a) asm_simp+;
+ by (rule sup_norm_prev, rule a) (simp!)+;
qed;
qed;
qed;
@@ -73,7 +79,7 @@
with aM; have bex_g: "EX g:M. ALL x:M. g <= x --> g = x";
- by (asm_simp add: Zorn's_Lemma);
+ by (simp! add: Zorn's_Lemma);
thus ?thesis;
proof;
fix g; assume g: "g:M" "ALL x:M. g <= x --> g = x";
@@ -84,7 +90,7 @@
& is_subspace F H
& (graph F f <= graph H h)
& (ALL x:H. h x <= p x) ";
- by (asm_simp add: norm_prev_extension_D);
+ by (simp! add: norm_prev_extension_D);
thus ?thesis;
proof (elim exE conjE);
fix H h; assume "graph H h = g" "is_linearform (H::'a set) h"
@@ -92,8 +98,8 @@
"(graph F f <= graph H h)"; assume h_bound: "ALL x:H. h x <= p x";
show ?thesis;
proof;
- have h: "is_vectorspace H"; by (rule subspace_vs);
- have f: "is_vectorspace F"; by (rule subspace_vs);
+ have h: "is_vectorspace H"; ..;
+ have f: "is_vectorspace F"; ..;
sect {* Part I a of the proof of the Hahn-Banach Theorem,
@@ -108,7 +114,7 @@
proof -;
have "EX H0 h0. g <= graph H0 h0 & g ~= graph H0 h0 & graph H0 h0 : M";
proof-;
- from subspace_subset [of H E]; have "H <= E"; ..;
+ have "H <= E"; ..;
hence "H < E"; ..;
hence "EX x0:E. x0~:H"; by (rule set_less_imp_diff_not_empty);
thus ?thesis;
@@ -117,11 +123,12 @@
have x0: "x0 ~= <0>";
proof (rule classical);
presume "x0 = <0>";
- have "x0 : H"; by (asm_simp add: zero_in_vs [OF h]);
- thus "x0 ~= <0>"; by contradiction;
+ also; have "<0> : H"; ..;
+ finally; have "x0 : H"; .;
+ thus ?thesis; by contradiction;
qed force;
- def H0_def: H0 == "vectorspace_sum H (lin x0)";
+ def H0 == "vectorspace_sum H (lin x0)";
have "EX h0. g <= graph H0 h0 & g ~= graph H0 h0 & graph H0 h0 : M";
proof -;
from h; have xi: "EX xi. (ALL y:H. - p (y [+] x0) - h y <= xi)
@@ -133,10 +140,10 @@
show "!! a b c d::real. d - b <= c + a ==> - a - b <= c - d";
proof -; (* arith *)
fix a b c d; assume "d - b <= c + (a::real)";
- have "- a - b = d - b + (- d - a)"; by asm_simp;
+ have "- a - b = d - b + (- d - a)"; by (simp!);
also; have "... <= c + a + (- d - a)";
by (rule real_add_le_mono1);
- also; have "... = c - d"; by asm_simp;
+ also; have "... = c - d"; by (simp!);
finally; show "- a - b <= c - d"; .;
qed;
show "h v - h u <= p (v [+] x0) + p (u [+] x0)";
@@ -145,17 +152,17 @@
by (rule linearform_diff_linear [RS sym]);
also; have "... <= p (v [-] u)";
proof -;
- from h; have "v [-] u : H"; by asm_simp;
+ from h; have "v [-] u : H"; by (simp!);
with h_bound; show ?thesis; ..;
qed;
also; have "v [-] u = x0 [+] [-] x0 [+] v [+] [-] u";
- by (asm_simp add: vs_add_minus_eq_diff);
+ by (simp! add: vs_add_minus_eq_diff);
also; have "... = v [+] x0 [+] [-] (u [+] x0)";
- by asm_simp;
+ by (simp!);
also; have "... = (v [+] x0) [-] (u [+] x0)";
- by (asm_simp only: vs_add_minus_eq_diff);
+ by (simp! only: vs_add_minus_eq_diff);
also; have "p ... <= p (v [+] x0) + p (u [+] x0)";
- by (rule quasinorm_diff_triangle_ineq) asm_simp+;
+ by (rule quasinorm_diff_triangle_ineq) (simp!)+;
finally; show ?thesis; .;
qed;
qed;
@@ -165,17 +172,17 @@
proof (elim exE, intro exI conjI);
fix xi; assume a: "(ALL y:H. - p (y [+] x0) - h y <= xi) &
(ALL y:H. xi <= p (y [+] x0) - h y)";
- def h0_def: h0 == "%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H )
+ def h0 == "%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H )
in (h y) + a * xi";
have "graph H h <= graph H0 h0";
- proof% (rule graph_lemma5);
+ proof (rule graph_extI);
fix t; assume "t:H";
show "h t = h0 t";
proof -;
have "(@ (y, a). t = y [+] a [*] x0 & y : H) = (t, 0r)";
- by (rule lemma1, rule x0);
- thus ?thesis; by (asm_simp add: Let_def);
+ by (rule decomp1, rule x0);
+ thus ?thesis; by (simp! add: Let_def);
qed;
next;
show "H <= H0";
@@ -187,82 +194,85 @@
qed;
qed;
qed;
- thus "g <= graph H0 h0"; by asm_simp;
+ thus "g <= graph H0 h0"; by (simp!);
have "graph H h ~= graph H0 h0";
proof;
assume "graph H h = graph H0 h0";
have x1: "(x0, h0 x0) : graph H0 h0";
- proof (rule graph_I);
+ proof (rule graphI);
show "x0:H0";
- proof (unfold H0_def, rule vs_sum_I);
- from h; show "<0> : H"; by (rule zero_in_vs);
+ proof (unfold H0_def, rule vs_sumI);
+ from h; show "<0> : H"; ..;
show "x0 : lin x0"; by (rule x_lin_x);
- show "x0 = <0> [+] x0"; by (rule vs_add_zero_left [RS sym]);
+ show "x0 = <0> [+] x0"; by (simp!);
qed;
qed;
have "(x0, h0 x0) ~: graph H h";
proof;
assume "(x0, h0 x0) : graph H h";
- have "x0:H"; by (rule graphD1);
+ have "x0:H"; ..;
thus "False"; by contradiction;
qed;
- hence "(x0, h0 x0) ~: graph H0 h0"; by asm_simp;
+ hence "(x0, h0 x0) ~: graph H0 h0"; by (simp!);
with x1; show "False"; by contradiction;
qed;
- thus "g ~= graph H0 h0"; by asm_simp;
+ thus "g ~= graph H0 h0"; by (simp!);
have "graph H0 h0 : norm_prev_extensions E p F f";
- proof (rule norm_prev_extension_I2);
+ proof (rule norm_prev_extensionI2);
show "is_linearform H0 h0";
- by (rule h0_lf, rule x0) asm_simp+;
+ by (rule h0_lf, rule x0) (simp!)+;
show "is_subspace H0 E";
proof -;
- have "is_subspace (vectorspace_sum H (lin x0)) E";
+ have "is_subspace (vectorspace_sum H (lin x0)) E";
by (rule vs_sum_subspace, rule lin_subspace);
- thus ?thesis; by asm_simp;
+ thus ?thesis; by (simp!);
qed;
show f_h0: "is_subspace F H0";
proof (rule subspace_trans [of F H H0]);
from h lin_vs; have "is_subspace H (vectorspace_sum H (lin x0))";
by (rule subspace_vs_sum1);
- thus "is_subspace H H0"; by asm_simp;
+ thus "is_subspace H H0"; by (simp!);
qed;
show "graph F f <= graph H0 h0";
- proof(rule graph_lemma5);
+ proof(rule graph_extI);
fix x; assume "x:F";
show "f x = h0 x";
proof -;
have "x:H";
proof (rule subsetD);
- show "F <= H"; by (rule subspace_subset);
+ show "F <= H"; ..;
qed;
have eq: "(@ (y, a). x = y [+] a [*] x0 & y : H) = (x, 0r)";
- by (rule lemma1, rule x0) asm_simp+;
+ by (rule decomp1, rule x0) (simp!)+;
have "h0 x = (let (y,a) = @ (y,a). x = y [+] a [*] x0 & y : H
in h y + a * xi)";
- by asm_simp;
+ by (simp!);
also; from eq; have "... = (let (y,a) = (x, 0r) in h y + a * xi)";
by simp;
also; have " ... = h x + 0r * xi";
- by (asm_simp add: Let_def);
- also; have "... = h x"; by asm_simp;
- also; have "... = f x"; by (rule graph_lemma3 [RS sym, of F f H h]);
+ by (simp! add: Let_def);
+ also; have "... = h x"; by (simp!);
+ also; have "... = f x";
+ proof (rule sym);
+ show "f x = h x"; ..;
+ qed;
finally; show ?thesis; by (rule sym);
qed;
next;
- from f_h0; show "F <= H0"; by (rule subspace_subset);
+ from f_h0; show "F <= H0"; ..;
qed;
show "ALL x:H0. h0 x <= p x";
- by (rule h0_norm_prev, rule x0) (assumption | asm_simp)+;
+ by (rule h0_norm_prev, rule x0) (assumption | (simp!))+;
qed;
- thus "graph H0 h0 : M"; by asm_simp;
+ thus "graph H0 h0 : M"; by (simp!);
qed;
qed;
thus ?thesis; ..;
@@ -279,9 +289,12 @@
show "is_linearform E h & (ALL x:F. h x = f x) & (ALL x:E. h x <= p x)";
proof (intro conjI);
- from eq; show "is_linearform E h"; by asm_simp;
- show "ALL x:F. h x = f x"; by (intro ballI, rule graph_lemma3 [RS sym]);
- from eq; show "ALL x:E. h x <= p x"; by force;
+ from eq; show "is_linearform E h"; by (simp!);
+ show "ALL x:F. h x = f x";
+ proof (intro ballI, rule sym);
+ fix x; assume "x:F"; show "f x = h x "; ..;
+ qed;
+ from eq; show "ALL x:E. h x <= p x"; by (force!);
qed;
qed;
qed;
@@ -302,17 +315,16 @@
assume e: "is_vectorspace E";
assume "is_subspace F E" "is_quasinorm E p" "is_linearform F f" "ALL x:F. rabs (f x) <= p x";
- have "ALL x:F. f x <= p x";
- by (asm_simp only: rabs_ineq);
+ have "ALL x:F. f x <= p x"; by (rule rabs_ineq [RS iffD1]);
hence "EX g. is_linearform E g & (ALL x:F. g x = f x) & (ALL x:E. g x <= p x)";
- by (asm_simp only: hahnbanach);
+ by (simp! only: hahnbanach);
thus ?thesis;
proof (elim exE conjE);
fix g; assume "is_linearform E g" "ALL x:F. g x = f x" "ALL x:E. g x <= p x";
show ?thesis;
proof (intro exI conjI)+;
- from e; show "ALL x:E. rabs (g x) <= p x";
- by (asm_simp add: rabs_ineq [OF subspace_refl]);
+ from e; show "ALL x:E. rabs (g x) <= p x";
+ by (simp! add: rabs_ineq [OF subspace_refl]);
qed;
qed;
qed;
@@ -334,10 +346,10 @@
assume a: "is_normed_vectorspace E norm";
assume b: "is_subspace F E" "is_linearform F f";
assume c: "is_continous F norm f";
- hence e: "is_vectorspace E"; by (asm_simp add: normed_vs_vs);
+ have e: "is_vectorspace E"; ..;
from _ e;
- have f: "is_normed_vectorspace F norm"; by (rule subspace_normed_vs);
- def p_def: p == "%x::'a. (function_norm F norm f) * norm x";
+ have f: "is_normed_vectorspace F norm"; ..;
+ def p == "%x::'a. (function_norm F norm f) * norm x";
let ?P' = "%g. is_linearform E g & (ALL x:F. g x = f x) & (ALL x:E. rabs (g x) <= p x)";
@@ -347,53 +359,52 @@
show "0r <= p x";
proof (unfold p_def, rule real_le_mult_order);
- from c f; show "0r <= function_norm F norm f";
- by (rule fnorm_ge_zero);
- from a; show "0r <= norm x"; by (rule normed_vs_norm_ge_zero);
+ from _ f; show "0r <= function_norm F norm f"; ..;
+ show "0r <= norm x"; ..;
qed;
show "p (a [*] x) = (rabs a) * (p x)";
proof -;
- have "p (a [*] x) = (function_norm F norm f) * norm (a [*] x)"; by asm_simp;
- also; from a; have "norm (a [*] x) = rabs a * norm x"; by (rule normed_vs_norm_mult_distrib);
+ have "p (a [*] x) = (function_norm F norm f) * norm (a [*] x)"; by (simp!);
+ also; have "norm (a [*] x) = rabs a * norm x"; by (rule normed_vs_norm_mult_distrib);
also; have "(function_norm F norm f) * ... = rabs a * ((function_norm F norm f) * norm x)";
- by (asm_simp only: real_mult_left_commute);
- also; have "... = (rabs a) * (p x)"; by asm_simp;
+ by (simp! only: real_mult_left_commute);
+ also; have "... = (rabs a) * (p x)"; by (simp!);
finally; show ?thesis; .;
qed;
show "p (x [+] y) <= p x + p y";
proof -;
- have "p (x [+] y) = (function_norm F norm f) * norm (x [+] y)"; by asm_simp;
+ have "p (x [+] y) = (function_norm F norm f) * norm (x [+] y)"; by (simp!);
also; have "... <= (function_norm F norm f) * (norm x + norm y)";
proof (rule real_mult_le_le_mono1);
- from c f; show "0r <= function_norm F norm f"; by (rule fnorm_ge_zero);
- show "norm (x [+] y) <= norm x + norm y"; by (rule normed_vs_norm_triangle_ineq);
+ from _ f; show "0r <= function_norm F norm f"; ..;
+ show "norm (x [+] y) <= norm x + norm y"; ..;
qed;
also; have "... = (function_norm F norm f) * (norm x) + (function_norm F norm f) * (norm y)";
- by (asm_simp only: real_add_mult_distrib2);
- finally; show ?thesis; by asm_simp;
+ by (simp! only: real_add_mult_distrib2);
+ finally; show ?thesis; by (simp!);
qed;
qed;
have "ALL x:F. rabs (f x) <= p x";
proof;
fix x; assume "x:F";
- from f; show "rabs (f x) <= p x"; by (asm_simp add: norm_fx_le_norm_f_norm_x);
+ from f; show "rabs (f x) <= p x"; by (simp! add: norm_fx_le_norm_f_norm_x);
qed;
with e b q; have "EX g. ?P' g";
- by (asm_simp add: rabs_hahnbanach);
+ by (simp! add: rabs_hahnbanach);
thus "?thesis";
proof (elim exE conjE, intro exI conjI);
fix g;
assume "is_linearform E g" and a: "ALL x:F. g x = f x" and "ALL x:E. rabs (g x) <= p x";
show ce: "is_continous E norm g";
- proof (rule lipschitz_continous_I);
+ proof (rule lipschitz_continousI);
fix x; assume "x:E";
show "rabs (g x) <= function_norm F norm f * norm x";
- by (rule bspec [of _ _ x], asm_simp);
+ by (rule bspec [of _ _ x], (simp!));
qed;
show "function_norm E norm g = function_norm F norm f";
proof (rule order_antisym);
@@ -403,28 +414,28 @@
proof;
fix x; assume "x:E";
show "rabs (g x) <= function_norm F norm f * norm x";
- by (rule bspec [of _ _ x], asm_simp);
+ by (rule bspec [of _ _ x], (simp!));
qed;
- from c f; show "0r <= function_norm F norm f"; by (rule fnorm_ge_zero);
+ from c f; show "0r <= function_norm F norm f"; ..;
qed;
show "function_norm F norm f <= function_norm E norm g";
proof (rule fnorm_le_ub);
show "ALL x:F. rabs (f x) <= function_norm E norm g * norm x";
proof;
- fix x; assume "x:F";
- from a; have "f x = g x"; by (rule bspec [of _ _ x, RS sym]);
+ fix x; assume "x : F";
+ from a; have "g x = f x"; ..;
hence "rabs (f x) = rabs (g x)"; by simp;
also; from _ _ ce; have "... <= function_norm E norm g * norm x";
proof (rule norm_fx_le_norm_f_norm_x);
- show "x:E";
+ show "x : E";
proof (rule subsetD);
- show "F<=E"; by (rule subspace_subset);
+ show "F <= E"; ..;
qed;
qed;
finally; show "rabs (f x) <= function_norm E norm g * norm x"; .;
qed;
- from _ e; show "is_normed_vectorspace F norm"; by (rule subspace_normed_vs);
- from ce; show "0r <= function_norm E norm g"; by (rule fnorm_ge_zero);
+ from _ e; show "is_normed_vectorspace F norm"; ..;
+ from ce; show "0r <= function_norm E norm g"; ..;
qed;
qed;
qed;
@@ -432,3 +443,4 @@
end;
+
--- a/src/HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy Tue Sep 21 17:30:55 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy Tue Sep 21 17:31:20 1999 +0200
@@ -1,8 +1,12 @@
+(* Title: HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy
+ ID: $Id$
+ Author: Gertrud Bauer, TU Munich
+*)
-theory HahnBanach_h0_lemmas = FunctionOrder + NormedSpace + Zorn_Lemma + FunctionNorm + RComplete:;
+theory HahnBanach_h0_lemmas = FunctionNorm:;
-theorems [intro!!] = zero_in_vs isLub_isUb;
+theorems [intro!!] = isLub_isUb;
lemma ex_xi: "[| is_vectorspace F; (!! u v. [| u:F; v:F |] ==> a u <= b v )|]
==> EX xi::real. (ALL y:F. (a::'a => real) y <= xi) & (ALL y:F. xi <= b y)";
@@ -11,7 +15,7 @@
assume r: "(!! u v. [| u:F; v:F |] ==> a u <= (b v::real))";
have "EX t. isLub UNIV {s::real . EX u:F. s = a u} t";
proof (rule reals_complete);
- have "a <0> : {s. EX u:F. s = a u}"; by force;
+ have "a <0> : {s. EX u:F. s = a u}"; by (force!);
thus "EX X. X : {s. EX u:F. s = a u}"; ..;
show "EX Y. isUb UNIV {s. EX u:F. s = a u} Y";
@@ -21,7 +25,7 @@
fix y; assume "y : {s. EX u:F. s = a u}";
show "y <= b <0>";
proof -;
- have "EX u:F. y = a u"; by fast;
+ have "EX u:F. y = a u"; by (fast!);
thus ?thesis;
proof;
fix u; assume "u:F";
@@ -45,7 +49,7 @@
show "a y <= t";
proof (rule isUbD);
show"isUb UNIV {s. EX u:F. s = a u} t"; ..;
- qed fast;
+ qed (fast!);
next;
fix y; assume "y:F";
show "t <= b y";
@@ -56,7 +60,7 @@
assume "au : {s. EX u:F. s = a u} ";
show "au <= b y";
proof -;
- have "EX u:F. au = a u"; by fast;
+ have "EX u:F. au = a u"; by (fast!);
thus "au <= b y";
proof;
fix u; assume "u:F";
@@ -73,8 +77,6 @@
qed;
-theorems [dest!!] = vs_sumD linD;
-
lemma h0_lf:
"[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) in (h y) + a * xi);
H0 = vectorspace_sum H (lin x0); is_subspace H E; is_linearform H h; x0 ~: H;
@@ -87,7 +89,7 @@
and [simp]: "x0 : E" "is_vectorspace E";
have h0: "is_vectorspace H0";
- proof (asm_simp, rule vs_sum_vs);
+ proof ((simp!), rule vs_sum_vs);
show "is_subspace (lin x0) E"; by (rule lin_subspace);
qed simp+;
@@ -98,11 +100,11 @@
by (rule vs_add_closed, rule h0);
have ex_x1: "? y1 a1. (x1 = y1 [+] a1 [*] x0 & y1 : H)";
- by (asm_simp add: vectorspace_sum_def lin_def) blast;
+ by (simp! add: vectorspace_sum_def lin_def) blast;
have ex_x2: "? y2 a2. (x2 = y2 [+] a2 [*] x0 & y2 : H)";
- by (asm_simp add: vectorspace_sum_def lin_def) blast;
+ by (simp! add: vectorspace_sum_def lin_def) blast;
from x1x2; have ex_x1x2: "? y a. (x1 [+] x2 = y [+] a [*] x0 & y : H)";
- by (asm_simp add: vectorspace_sum_def lin_def) force;
+ by (simp! add: vectorspace_sum_def lin_def) force;
from ex_x1 ex_x2 ex_x1x2;
show "h0 (x1 [+] x2) = h0 x1 + h0 x2";
proof (elim exE conjE);
@@ -112,33 +114,33 @@
"x1 [+] x2 = y [+] a [*] x0" "y : H";
have ya: "y1 [+] y2 = y & a1 + a2 = a";
- proof (rule lemma4);
+ proof (rule decomp4);
show "y1 [+] y2 [+] (a1 + a2) [*] x0 = y [+] a [*] x0";
proof -;
- have "y [+] a [*] x0 = x1 [+] x2"; by asm_simp;
- also; have "... = y1 [+] a1 [*] x0 [+] (y2 [+] a2 [*] x0)"; by asm_simp;
- also; have "... = y1 [+] y2 [+] (a1 [*] x0 [+] a2 [*] x0)";
- by asm_simp_tac;
+ have "y [+] a [*] x0 = x1 [+] x2"; by (simp!);
+ also; have "... = y1 [+] a1 [*] x0 [+] (y2 [+] a2 [*] x0)"; by (simp!);
+ also; from prems; have "... = y1 [+] y2 [+] (a1 [*] x0 [+] a2 [*] x0)";
+ by asm_simp_tac; (* FIXME !?? *)
also; have "... = y1 [+] y2 [+] (a1 + a2) [*] x0";
- by (asm_simp add: vs_add_mult_distrib2[of E]);
+ by (simp! add: vs_add_mult_distrib2[of E]);
finally; show ?thesis; by (rule sym);
qed;
- show "y1 [+] y2 : H"; by (rule subspace_add_closed);
+ show "y1 [+] y2 : H"; ..;
qed;
have y: "y1 [+] y2 = y"; by (rule conjunct1 [OF ya]);
have a: "a1 + a2 = a"; by (rule conjunct2 [OF ya]);
have "h0 (x1 [+] x2) = h y + a * xi";
- by (rule lemma3);
- also; have "... = h (y1 [+] y2) + (a1 + a2) * xi"; by (asm_simp add: y a);
+ by (rule decomp3);
+ also; have "... = h (y1 [+] y2) + (a1 + a2) * xi"; by (simp! add: y a);
also; have "... = h y1 + h y2 + a1 * xi + a2 * xi";
- by (asm_simp add: linearform_add_linear [of H] real_add_mult_distrib);
- also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"; by asm_simp;
+ by (simp! add: linearform_add_linear [of H] real_add_mult_distrib);
+ also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"; by (simp!);
also; have "... = h0 x1 + h0 x2";
proof -;
- have x1: "h0 x1 = h y1 + a1 * xi"; by (rule lemma3);
- have x2: "h0 x2 = h y2 + a2 * xi"; by (rule lemma3);
- from x1 x2; show ?thesis; by asm_simp;
+ have x1: "h0 x1 = h y1 + a1 * xi"; by (rule decomp3);
+ have x2: "h0 x2 = h y2 + a2 * xi"; by (rule decomp3);
+ from x1 x2; show ?thesis; by (simp!);
qed;
finally; show ?thesis; .;
qed;
@@ -149,9 +151,9 @@
have ax1: "c [*] x1 : H0";
by (rule vs_mult_closed, rule h0);
have ex_x1: "? y1 a1. (x1 = y1 [+] a1 [*] x0 & y1 : H)";
- by (asm_simp add: vectorspace_sum_def lin_def, fast);
+ by (simp! add: vectorspace_sum_def lin_def, fast);
have ex_x: "!! x. x: H0 ==> ? y a. (x = y [+] a [*] x0 & y : H)";
- by (asm_simp add: vectorspace_sum_def lin_def, fast);
+ by (simp! add: vectorspace_sum_def lin_def, fast);
note ex_ax1 = ex_x [of "c [*] x1", OF ax1];
from ex_x1 ex_ax1; show "h0 (c [*] x1) = c * (h0 x1)";
proof (elim exE conjE);
@@ -160,34 +162,34 @@
"c [*] x1 = y [+] a [*] x0" "y : H";
have ya: "c [*] y1 = y & c * a1 = a";
- proof (rule lemma4);
+ proof (rule decomp4);
show "c [*] y1 [+] (c * a1) [*] x0 = y [+] a [*] x0";
proof -;
- have "y [+] a [*] x0 = c [*] x1"; by asm_simp;
- also; have "... = c [*] (y1 [+] a1 [*] x0)"; by asm_simp;
- also; have "... = c [*] y1 [+] c [*] (a1 [*] x0)";
- by (asm_simp_tac add: vs_add_mult_distrib1);
- also; have "... = c [*] y1 [+] (c * a1) [*] x0";
- by (asm_simp_tac);
+ have "y [+] a [*] x0 = c [*] x1"; by (simp!);
+ also; have "... = c [*] (y1 [+] a1 [*] x0)"; by (simp!);
+ also; from prems; have "... = c [*] y1 [+] c [*] (a1 [*] x0)";
+ by (asm_simp_tac add: vs_add_mult_distrib1); (* FIXME *)
+ also; from prems; have "... = c [*] y1 [+] (c * a1) [*] x0";
+ by asm_simp_tac;
finally; show ?thesis; by (rule sym);
qed;
- show "c [*] y1: H"; by (rule subspace_mult_closed);
+ show "c [*] y1: H"; ..;
qed;
have y: "c [*] y1 = y"; by (rule conjunct1 [OF ya]);
have a: "c * a1 = a"; by (rule conjunct2 [OF ya]);
have "h0 (c [*] x1) = h y + a * xi";
- by (rule lemma3);
+ by (rule decomp3);
also; have "... = h (c [*] y1) + (c * a1) * xi";
- by (asm_simp add: y a);
+ by (simp! add: y a);
also; have "... = c * h y1 + c * a1 * xi";
- by (asm_simp add: linearform_mult_linear [of H] real_add_mult_distrib);
+ by (simp! add: linearform_mult_linear [of H] real_add_mult_distrib);
also; have "... = c * (h y1 + a1 * xi)";
- by (asm_simp add: real_add_mult_distrib2 real_mult_assoc);
+ by (simp! add: real_add_mult_distrib2 real_mult_assoc);
also; have "... = c * (h0 x1)";
proof -;
- have "h0 x1 = h y1 + a1 * xi"; by (rule lemma3);
- thus ?thesis; by asm_simp;
+ have "h0 x1 = h y1 + a1 * xi"; by (rule decomp3);
+ thus ?thesis; by (simp!);
qed;
finally; show ?thesis; .;
qed;
@@ -211,7 +213,7 @@
show "h0 x <= p x";
proof -;
have ex_x: "!! x. x : H0 ==> ? y a. (x = y [+] a [*] x0 & y : H)";
- by (asm_simp add: vectorspace_sum_def lin_def, fast);
+ by (simp! add: vectorspace_sum_def lin_def, fast);
have "? y a. (x = y [+] a [*] x0 & y : H)";
by (rule ex_x);
thus ?thesis;
@@ -220,16 +222,16 @@
show ?thesis;
proof -;
have "h0 x = h y + a * xi";
- by (rule lemma3);
+ by (rule decomp3);
also; have "... <= p (y [+] a [*] x0)";
- proof (rule real_linear [of a "0r", elimify], elim disjE); (* case distinction *)
+ proof (rule real_linear [of a "0r", elimify], elim disjE); (*** case distinction ***)
assume lz: "a < 0r";
hence nz: "a ~= 0r"; by force;
show ?thesis;
proof -;
from a1; have "- p (rinv a [*] y [+] x0) - h (rinv a [*] y) <= xi";
proof (rule bspec);
- show "(rinv a) [*] y : H"; by (rule subspace_mult_closed);
+ show "(rinv a) [*] y : H"; ..;
qed;
with lz; have "a * xi <= a * (- p (rinv a [*] y [+] x0) - h (rinv a [*] y))";
by (rule real_mult_less_le_anti);
@@ -241,52 +243,46 @@
by (rule rabs_minus_eqI2);
thus ?thesis; by simp;
qed;
- also; have "... = p (a [*] (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
- by (asm_simp, asm_simp_tac add: quasinorm_mult_distrib);
+ also; from prems; have "... = p (a [*] (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
+ by (simp!, asm_simp_tac add: quasinorm_mult_distrib);
also; have "... = p ((a * rinv a) [*] y [+] a [*] x0) - a * (h (rinv a [*] y))";
proof simp;
have "a [*] (rinv a [*] y [+] x0) = a [*] rinv a [*] y [+] a [*] x0";
- by (rule vs_add_mult_distrib1) asm_simp+;
+ by (rule vs_add_mult_distrib1) (simp!)+;
also; have "... = (a * rinv a) [*] y [+] a [*] x0";
- by asm_simp;
+ by (simp!);
finally; have "a [*] (rinv a [*] y [+] x0) = (a * rinv a) [*] y [+] a [*] x0";.;
thus "p (a [*] (rinv a [*] y [+] x0)) = p ((a * rinv a) [*] y [+] a [*] x0)";
by simp;
qed;
also; from nz; have "... = p (y [+] a [*] x0) - (a * (h (rinv a [*] y)))";
- by asm_simp;
- also; from nz; have "... = p (y [+] a [*] x0) - (h y)";
- proof asm_simp;
- have "a * (h (rinv a [*] y)) = h (a [*] (rinv a [*] y))";
+ by (simp!);
+ also; have "a * (h (rinv a [*] y)) = h y";
+ proof -;
+ from prems; have "a * (h (rinv a [*] y)) = h (a [*] (rinv a [*] y))";
by (asm_simp_tac add: linearform_mult_linear [RS sym]);
- also; have "... = h y";
- proof -;
- from nz; have "a [*] (rinv a [*] y) = y"; by asm_simp;
- thus ?thesis; by simp;
- qed;
- finally; have "a * (h (rinv a [*] y)) = h y"; .;
- thus "- (a * (h (rinv a [*] y))) = - (h y)"; by simp;
+ also; from nz; have "a [*] (rinv a [*] y) = y"; by (simp!);
+ finally; show ?thesis; .;
qed;
- finally; have "a * xi <= p (y [+] a [*] x0) - h y"; .;
+ finally; have "a * xi <= p (y [+] a [*] x0) - ..."; .;
hence "h y + a * xi <= h y + (p (y [+] a [*] x0) - h y)";
by (rule real_add_left_cancel_le [RS iffD2]); (* arith *)
thus ?thesis;
by force;
- qed;
-
+ qed;
next;
assume "a = 0r"; show ?thesis;
proof -;
- have "h y + a * xi = h y"; by asm_simp;
+ have "h y + a * xi = h y"; by (simp!);
also; from a; have "... <= p y"; ..;
also; have "... = p (y [+] a [*] x0)";
proof -;
- have "y = y [+] <0>"; by asm_simp;
+ have "y = y [+] <0>"; by (simp!);
also; have "... = y [+] a [*] x0";
proof -;
have "<0> = 0r [*] x0";
- by asm_simp;
- also; have "... = a [*] x0"; by asm_simp;
+ by (simp!);
+ also; have "... = a [*] x0"; by (simp!);
finally; have "<0> = a [*] x0";.;
thus ?thesis; by simp;
qed;
@@ -302,7 +298,7 @@
proof -;
from a2; have "xi <= p (rinv a [*] y [+] x0) - h (rinv a [*] y)";
proof (rule bspec);
- show "rinv a [*] y : H"; by (rule subspace_mult_closed);
+ show "rinv a [*] y : H"; ..;
qed;
with gz; have "a * xi <= a * (p (rinv a [*] y [+] x0) - h (rinv a [*] y))";
by (rule real_mult_less_le_mono);
@@ -314,27 +310,27 @@
by (rule rabs_eqI2);
thus ?thesis; by simp;
qed;
- also; have "... = p (a [*] (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
- by (asm_simp, asm_simp_tac add: quasinorm_mult_distrib);
+ also; from prems; have "... = p (a [*] (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
+ by (simp, asm_simp_tac add: quasinorm_mult_distrib);
also; have "... = p ((a * rinv a) [*] y [+] a [*] x0) - a * (h (rinv a [*] y))";
proof simp;
have "a [*] (rinv a [*] y [+] x0) = a [*] rinv a [*] y [+] a [*] x0";
- by (rule vs_add_mult_distrib1) asm_simp+;
+ by (rule vs_add_mult_distrib1) (simp!)+;
also; have "... = (a * rinv a) [*] y [+] a [*] x0";
- by asm_simp;
+ by (simp!);
finally; have "a [*] (rinv a [*] y [+] x0) = (a * rinv a) [*] y [+] a [*] x0";.;
thus "p (a [*] (rinv a [*] y [+] x0)) = p ((a * rinv a) [*] y [+] a [*] x0)";
by simp;
qed;
also; from nz; have "... = p (y [+] a [*] x0) - (a * (h (rinv a [*] y)))";
- by asm_simp;
+ by (simp!);
also; from nz; have "... = p (y [+] a [*] x0) - (h y)";
- proof asm_simp;
+ proof (simp!);
have "a * (h (rinv a [*] y)) = h (a [*] (rinv a [*] y))";
- by (rule linearform_mult_linear [RS sym]) asm_simp+;
+ by (rule linearform_mult_linear [RS sym]) (simp!)+;
also; have "... = h y";
proof -;
- from nz; have "a [*] (rinv a [*] y) = y"; by asm_simp;
+ from nz; have "a [*] (rinv a [*] y) = y"; by (simp!);
thus ?thesis; by simp;
qed;
finally; have "a * (h (rinv a [*] y)) = h y"; .;
@@ -347,7 +343,7 @@
by force;
qed;
qed;
- also; have "... = p x"; by asm_simp;
+ also; have "... = p x"; by (simp!);
finally; show ?thesis; .;
qed;
qed;
--- a/src/HOL/Real/HahnBanach/HahnBanach_lemmas.thy Tue Sep 21 17:30:55 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach_lemmas.thy Tue Sep 21 17:31:20 1999 +0200
@@ -1,9 +1,10 @@
-
-theory HahnBanach_lemmas = FunctionOrder + NormedSpace + Zorn_Lemma + FunctionNorm + RComplete:;
+(* Title: HOL/Real/HahnBanach/HahnBanach_lemmas.thy
+ ID: $Id$
+ Author: Gertrud Bauer, TU Munich
+*)
+theory HahnBanach_lemmas = FunctionNorm + Zorn_Lemma:;
-theorems [dest!!] = subsetD;
-theorems [intro!!] = subspace_subset;
lemma rabs_ineq: "[| is_subspace H E; is_vectorspace E; is_quasinorm E p; is_linearform H h |] \
\ ==> (ALL x:H. rabs (h x) <= p x) = ( ALL x:H. h x <= p x)" (concl is "?L = ?R");
@@ -17,7 +18,7 @@
proof (intro ballI);
fix x; assume "x:H";
have "h x <= rabs (h x)"; by (rule rabs_ge_self);
- also; have "rabs (h x) <= p x"; by fast;
+ also; have "rabs (h x) <= p x"; by (fast!);
finally; show "h x <= p x"; .;
qed;
next;
@@ -34,15 +35,12 @@
from H; have "- h x = h ([-] x)"; by (rule linearform_neg_linear [RS sym]);
also; from r; have "... <= p ([-] x)";
proof -;
- from H; have "[-] x : H"; by asm_simp;
+ from H; have "[-] x : H"; by (simp!);
with r; show ?thesis; ..;
qed;
also; have "... = p x";
proof (rule quasinorm_minus);
- show "x:E";
- proof (rule subsetD);
- show "H <= E"; ..;
- qed;
+ show "x:E"; ..;
qed;
finally; show "- h x <= p x"; .;
qed;
@@ -69,12 +67,12 @@
& (ALL x:H. h x <= p x)";
have "EX t : (graph H h). t = (x, h x)";
- by (rule graph_lemma1);
+ by (rule graphI2);
thus ?thesis;
proof (elim bexE);
fix t; assume "t : (graph H h)" and "t = (x, h x)";
have ex1: "EX g:c. t:g";
- by (asm_simp only: Union_iff);
+ by (simp! only: Union_iff);
thus ?thesis;
proof (elim bexE);
fix g; assume "g:c" "t:g";
@@ -85,9 +83,9 @@
qed;
have "EX H' h'. graph H' h' = g & ?P H' h'";
proof (rule norm_prev_extension_D);
- from gM; show "g: norm_prev_extensions E p F f"; by asm_simp;
+ from gM; show "g: norm_prev_extensions E p F f"; by (simp!);
qed;
- thus ?thesis; by (elim exE conjE, intro exI conjI) (asm_simp+);
+ thus ?thesis; by (elim exE conjE, intro exI conjI) (simp | simp!)+;
qed;
qed;
qed;
@@ -111,12 +109,13 @@
assume "t : graph H h" "t = (x, h x)" "graph H' h' : c" "t : graph H' h'"
"is_linearform H' h'" "is_subspace H' E" "is_subspace F H'"
"graph F f <= graph H' h'" "ALL x:H'. h' x <= p x";
- show x: "x:H'"; by (asm_simp, rule graphD1);
+ show x: "x:H'"; by (simp!, rule graphD1);
show "graph H' h' <= graph H h";
- by (asm_simp only: chain_ball_Union_upper);
+ by (simp! only: chain_ball_Union_upper);
qed;
qed;
+theorems [trans] = subsetD [COMP swap_prems_rl];
lemma some_H'h'2:
"[| M = norm_prev_extensions E p F f; c: chain M; graph H h = Union c; x:H; y:H|]
@@ -159,28 +158,33 @@
proof;
assume "(graph H'' h'') <= (graph H' h')";
show ?thesis;
- proof (intro exI conjI);
- have xh: "(x, h x): graph H' h'"; by (fast);
+ proof (intro exI conjI); note [trans] = subsetD;
+ have "(x, h x) : graph H'' h''"; by (simp!);
+ also; have "... <= graph H' h'"; by (simp!);
+ finally; have xh: "(x, h x): graph H' h'"; .;
thus x: "x:H'"; by (rule graphD1);
- show y: "y:H'"; by (asm_simp, rule graphD1);
+ show y: "y:H'"; by (simp!, rule graphD1);
show "(graph H' h') <= (graph H h)";
- by (asm_simp only: chain_ball_Union_upper);
+ by (simp! only: chain_ball_Union_upper);
qed;
next;
assume "(graph H' h') <= (graph H'' h'')";
show ?thesis;
proof (intro exI conjI);
- show x: "x:H''"; by (asm_simp, rule graphD1);
- have yh: "(y, h y): graph H'' h''"; by (fast);
+ show x: "x:H''"; by (simp!, rule graphD1);
+ have "(y, h y) : graph H' h'"; by (simp!);
+ also; have "... <= graph H'' h''"; by (simp!);
+ finally; have yh: "(y, h y): graph H'' h''"; .;
thus y: "y:H''"; by (rule graphD1);
show "(graph H'' h'') <= (graph H h)";
- by (asm_simp only: chain_ball_Union_upper);
+ by (simp! only: chain_ball_Union_upper);
qed;
qed;
qed;
qed;
-
+lemmas chainE2 = chainD2 [elimify];
+lemmas [intro!!] = subsetD chainD;
lemma sup_uniq: "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; is_linearform F f;
ALL x:F. f x <= p x; M == norm_prev_extensions E p F f; c : chain M;
@@ -188,33 +192,33 @@
==> z = y";
proof -;
assume "M == norm_prev_extensions E p F f" "c : chain M" "(x, y) : Union c" " (x, z) : Union c";
- have "EX H h. (x, y) : graph H h & (x, z) : graph H h";
- proof (elim UnionE chainD2 [elimify]);
+ hence "EX H h. (x, y) : graph H h & (x, z) : graph H h";
+ proof (elim UnionE chainE2);
fix G1 G2; assume "(x, y) : G1" "G1 : c" "(x, z) : G2" "G2 : c" "c <= M";
- have "G1 : M"; by (rule subsetD);
+ have "G1 : M"; ..;
hence e1: "EX H1 h1. graph H1 h1 = G1";
- by (force dest: norm_prev_extension_D);
- have "G2 : M"; by (rule subsetD);
+ by (force! dest: norm_prev_extension_D);
+ have "G2 : M"; ..;
hence e2: "EX H2 h2. graph H2 h2 = G2";
- by (force dest: norm_prev_extension_D);
+ by (force! dest: norm_prev_extension_D);
from e1 e2; show ?thesis;
proof (elim exE);
fix H1 h1 H2 h2; assume "graph H1 h1 = G1" "graph H2 h2 = G2";
- have "G1 <= G2 | G2 <= G1"; by (rule chainD);
+ have "G1 <= G2 | G2 <= G1"; ..;
thus ?thesis;
proof;
assume "G1 <= G2";
thus ?thesis;
proof (intro exI conjI);
- show "(x, y) : graph H2 h2"; by force;
- show "(x, z) : graph H2 h2"; by asm_simp;
+ show "(x, y) : graph H2 h2"; by (force!);
+ show "(x, z) : graph H2 h2"; by (simp!);
qed;
next;
assume "G2 <= G1";
thus ?thesis;
proof (intro exI conjI);
- show "(x, y) : graph H1 h1"; by asm_simp;
- show "(x, z) : graph H1 h1"; by force;
+ show "(x, y) : graph H1 h1"; by (simp!);
+ show "(x, z) : graph H1 h1"; by (force!);
qed;
qed;
qed;
@@ -222,8 +226,8 @@
thus ?thesis;
proof (elim exE conjE);
fix H h; assume "(x, y) : graph H h" "(x, z) : graph H h";
- have "y = h x"; by (rule graph_lemma2);
- also; have "h x = z"; by (rule graph_lemma2 [RS sym]);
+ have "y = h x"; ..;
+ also; have "... = z"; by (rule sym, rule);
finally; show "z = y"; by (rule sym);
qed;
qed;
@@ -254,17 +258,16 @@
fix H' h'; assume "x:H'" "y:H'"
and b: "graph H' h' <= graph H h"
and "is_linearform H' h'" "is_subspace H' E";
- have h'x: "h' x = h x"; by (rule graph_lemma3);
- have h'y: "h' y = h y"; by (rule graph_lemma3);
+ have h'x: "h' x = h x"; ..;
+ have h'y: "h' y = h y"; ..;
have h'xy: "h' (x [+] y) = h' x + h' y"; by (rule linearform_add_linear);
have "h' (x [+] y) = h (x [+] y)";
proof -;
- have "x [+] y : H'";
- by (rule subspace_add_closed);
- with b; show ?thesis; by (rule graph_lemma3);
+ have "x [+] y : H'"; ..;
+ with b; show ?thesis; ..;
qed;
with h'x h'y h'xy; show ?thesis;
- by asm_simp;
+ by (simp!);
qed;
qed;
@@ -281,16 +284,15 @@
fix H' h';
assume b: "graph H' h' <= graph H h";
assume "x:H'" "is_linearform H' h'" "is_subspace H' E";
- have h'x: "h' x = h x"; by (rule graph_lemma3);
+ have h'x: "h' x = h x"; ..;
have h'ax: "h' (a [*] x) = a * h' x"; by (rule linearform_mult_linear);
have "h' (a [*] x) = h (a [*] x)";
proof -;
- have "a [*] x : H'";
- by (rule subspace_mult_closed);
- with b; show ?thesis; by (rule graph_lemma3);
+ have "a [*] x : H'"; ..;
+ with b; show ?thesis; ..;
qed;
with h'x h'ax; show ?thesis;
- by asm_simp;
+ by (simp!);
qed;
qed;
qed;
@@ -303,14 +305,14 @@
assume "M = norm_prev_extensions E p F f" "c: chain M" "graph H h = Union c"
and e: "EX x. x:c";
- show ?thesis;
+ thus ?thesis;
proof (elim exE);
fix x; assume "x:c";
show ?thesis;
proof -;
have "x:norm_prev_extensions E p F f";
proof (rule subsetD);
- show "c <= norm_prev_extensions E p F f"; by (asm_simp add: chainD2);
+ show "c <= norm_prev_extensions E p F f"; by (simp! add: chainD2);
qed;
hence "(EX G g. graph G g = x
@@ -319,15 +321,15 @@
& is_subspace F G
& (graph F f <= graph G g)
& (ALL x:G. g x <= p x))";
- by (asm_simp add: norm_prev_extension_D);
+ by (simp! add: norm_prev_extension_D);
thus ?thesis;
proof (elim exE conjE);
fix G g; assume "graph G g = x" "graph F f <= graph G g";
show ?thesis;
proof -;
- have "graph F f <= graph G g"; by assumption;
- also; have "graph G g <= graph H h"; by (asm_simp, fast);
+ have "graph F f <= graph G g"; .;
+ also; have "graph G g <= graph H h"; by ((simp!), fast);
finally; show ?thesis; .;
qed;
qed;
@@ -343,22 +345,22 @@
"is_subspace F E";
show ?thesis;
- proof (rule subspace_I);
- show "<0> : F"; by (rule zero_in_subspace);
+ proof (rule subspaceI);
+ show "<0> : F"; ..;
show "F <= H";
- proof (rule graph_lemma4);
+ proof (rule graph_extD2);
show "graph F f <= graph H h";
by (rule sup_ext);
qed;
show "ALL x:F. ALL y:F. x [+] y : F";
proof (intro ballI);
fix x y; assume "x:F" "y:F";
- show "x [+] y : F"; by asm_simp;
+ show "x [+] y : F"; by (simp!);
qed;
show "ALL x:F. ALL a. a [*] x : F";
proof (intro ballI allI);
fix x a; assume "x:F";
- show "a [*] x : F"; by asm_simp;
+ show "a [*] x : F"; by (simp!);
qed;
qed;
qed;
@@ -371,13 +373,13 @@
"is_subspace F E";
show ?thesis;
- proof (rule subspace_I);
+ proof;
show "<0> : H";
proof (rule subsetD [of F H]);
have "is_subspace F H"; by (rule sup_supF);
- thus "F <= H"; by (rule subspace_subset);
- show "<0> :F"; by (rule zero_in_subspace);
+ thus "F <= H"; ..;
+ show "<0> : F"; ..;
qed;
show "H <= E";
@@ -394,8 +396,7 @@
fix H' h'; assume "x:H'" "is_subspace H' E";
show "x:E";
proof (rule subsetD);
- show "H' <= E";
- by (rule subspace_subset);
+ show "H' <= E"; ..;
qed;
qed;
qed;
@@ -413,10 +414,10 @@
thus ?thesis;
proof (elim exE conjE);
fix H' h'; assume "x:H'" "y:H'" "is_subspace H' E" "graph H' h' <= graph H h";
- have "H' <= H"; by (rule graph_lemma4);
+ have "H' <= H"; ..;
thus ?thesis;
proof (rule subsetD);
- show "x [+] y : H'"; by (rule subspace_add_closed);
+ show "x [+] y : H'"; ..;
qed;
qed;
qed;
@@ -434,10 +435,10 @@
thus ?thesis;
proof (elim exE conjE);
fix H' h'; assume "x:H'" "is_subspace H' E" "graph H' h' <= graph H h";
- have "H' <= H"; by (rule graph_lemma4);
+ have "H' <= H"; ..;
thus ?thesis;
proof (rule subsetD);
- show "a [*] x : H'"; by (rule subspace_mult_closed);
+ show "a [*] x : H'"; ..;
qed;
qed;
qed;
@@ -461,8 +462,8 @@
proof (elim exE conjE);
fix H' h'; assume "x: H'" "graph H' h' <= graph H h" and a: "ALL x: H'. h' x <= p x" ;
have "h x = h' x";
- proof(rule sym);
- show "h' x = h x"; by (rule graph_lemma3);
+ proof (rule sym);
+ show "h' x = h x"; ..;
qed;
also; from a; have "... <= p x "; ..;
finally; show ?thesis; .;
@@ -471,4 +472,4 @@
qed;
-end;
\ No newline at end of file
+end;
--- a/src/HOL/Real/HahnBanach/LinearSpace.thy Tue Sep 21 17:30:55 1999 +0200
+++ b/src/HOL/Real/HahnBanach/LinearSpace.thy Tue Sep 21 17:31:20 1999 +0200
@@ -1,5 +1,9 @@
+(* Title: HOL/Real/HahnBanach/LinearSpace.thy
+ ID: $Id$
+ Author: Gertrud Bauer, TU Munich
+*)
-theory LinearSpace = Main + RealAbs + Bounds + Aux:;
+theory LinearSpace = Bounds + Aux:;
section {* vector spaces *};
@@ -7,7 +11,7 @@
consts
sum :: "['a, 'a] => 'a" (infixl "[+]" 65)
prod :: "[real, 'a] => 'a" (infixr "[*]" 70)
- zero :: "'a" ("<0>");
+ zero :: 'a ("<0>");
constdefs
negate :: "'a => 'a" ("[-] _" [100] 100)
@@ -41,7 +45,7 @@
lemma vs_add_minus_eq_diff: "x [+] [-] y = x [-] y";
by (simp add: diff_def);
-lemma vs_I:
+lemma vsI [intro]:
"[| <0>:V; \
\ ALL x: V. ALL a::real. a [*] x: V; \
\ ALL x: V. ALL y: V. x [+] y = y [+] x; \
@@ -53,43 +57,49 @@
\ ALL x: V. ALL a::real. ALL b::real. (a + b) [*] x = a [*] x [+] b [*] x; \
\ ALL x: V. ALL a::real. ALL b::real. (a * b) [*] x = a [*] b [*] x; \
\ ALL x: V. 1r [*] x = x |] ==> is_vectorspace V";
- by (unfold is_vectorspace_def) auto;
+proof (unfold is_vectorspace_def, intro conjI ballI allI);
+ fix x y z; assume "x:V" "y:V" "z:V";
+ assume "ALL x: V. ALL y: V. ALL z: V. x [+] y [+] z = x [+] (y [+] z)";
+ thus "x [+] y [+] z = x [+] (y [+] z)"; by (elim bspec[elimify]);
+qed force+;
-lemma zero_in_vs [simp, dest]: "is_vectorspace V ==> <0>:V";
- by (unfold is_vectorspace_def) asm_simp;
+
-lemma vs_not_empty: "is_vectorspace V ==> (V ~= {})";
+lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> <0>:V";
+ by (unfold is_vectorspace_def) (simp!);
+
+lemma vs_not_empty [intro !!]: "is_vectorspace V ==> (V ~= {})";
by (unfold is_vectorspace_def) fast;
-lemma vs_add_closed [simp]: "[| is_vectorspace V; x: V; y: V|] ==> x [+] y: V";
- by (unfold is_vectorspace_def) asm_simp;
+lemma vs_add_closed [simp, intro!!]: "[| is_vectorspace V; x: V; y: V|] ==> x [+] y: V";
+ by (unfold is_vectorspace_def) (simp!);
-lemma vs_mult_closed [simp]: "[| is_vectorspace V; x: V |] ==> a [*] x: V";
- by (unfold is_vectorspace_def) asm_simp;
+lemma vs_mult_closed [simp, intro!!]: "[| is_vectorspace V; x: V |] ==> a [*] x: V";
+ by (unfold is_vectorspace_def) (simp!);
-lemma vs_diff_closed [simp]: "[| is_vectorspace V; x: V; y: V|] ==> x [-] y: V";
- by (unfold diff_def negate_def) asm_simp;
+lemma vs_diff_closed [simp, intro!!]: "[| is_vectorspace V; x: V; y: V|] ==> x [-] y: V";
+ by (unfold diff_def negate_def) (simp!);
-lemma vs_neg_closed [simp]: "[| is_vectorspace V; x: V |] ==> [-] x: V";
- by (unfold negate_def) asm_simp;
+lemma vs_neg_closed [simp, intro!!]: "[| is_vectorspace V; x: V |] ==> [-] x: V";
+ by (unfold negate_def) (simp!);
lemma vs_add_assoc [simp]:
"[| is_vectorspace V; x: V; y: V; z: V|] ==> x [+] y [+] z = x [+] (y [+] z)";
by (unfold is_vectorspace_def) fast;
lemma vs_add_commute [simp]: "[| is_vectorspace V; x:V; y:V |] ==> y [+] x = x [+] y";
- by (unfold is_vectorspace_def) asm_simp;
+ by (unfold is_vectorspace_def) (simp!);
lemma vs_add_left_commute [simp]:
"[| is_vectorspace V; x:V; y:V; z:V |] ==> x [+] (y [+] z) = y [+] (x [+] z)";
proof -;
assume vs: "is_vectorspace V" "x:V" "y:V" "z:V";
have "x [+] (y [+] z) = (x [+] y) [+] z";
- by (asm_simp only: vs_add_assoc);
+ by (simp! only: vs_add_assoc);
also; have "... = (y [+] x) [+] z";
- by (asm_simp only: vs_add_commute);
+ by (simp! only: vs_add_commute);
also; have "... = y [+] (x [+] z)";
- by (asm_simp only: vs_add_assoc);
+ by (simp! only: vs_add_assoc);
finally; show ?thesis; .;
qed;
@@ -97,44 +107,44 @@
theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute;
lemma vs_diff_self [simp]: "[| is_vectorspace V; x:V |] ==> x [-] x = <0>";
- by (unfold is_vectorspace_def) asm_simp;
+ by (unfold is_vectorspace_def) (simp!);
lemma vs_add_zero_left [simp]: "[| is_vectorspace V; x:V |] ==> <0> [+] x = x";
- by (unfold is_vectorspace_def) asm_simp;
+ by (unfold is_vectorspace_def) (simp!);
lemma vs_add_zero_right [simp]: "[| is_vectorspace V; x:V |] ==> x [+] <0> = x";
proof -;
assume vs: "is_vectorspace V" "x:V";
have "x [+] <0> = <0> [+] x";
- by asm_simp;
+ by (simp!);
also; have "... = x";
- by asm_simp;
+ by (simp!);
finally; show ?thesis; .;
qed;
lemma vs_add_mult_distrib1:
"[| is_vectorspace V; x:V; y:V |] ==> a [*] (x [+] y) = a [*] x [+] a [*] y";
- by (unfold is_vectorspace_def) asm_simp;
+ by (unfold is_vectorspace_def) (simp!);
lemma vs_add_mult_distrib2:
"[| is_vectorspace V; x:V |] ==> (a + b) [*] x = a [*] x [+] b [*] x";
- by (unfold is_vectorspace_def) asm_simp;
+ by (unfold is_vectorspace_def) (simp!);
lemma vs_mult_assoc: "[| is_vectorspace V; x:V |] ==> (a * b) [*] x = a [*] (b [*] x)";
- by (unfold is_vectorspace_def) asm_simp;
+ by (unfold is_vectorspace_def) (simp!);
lemma vs_mult_assoc2 [simp]: "[| is_vectorspace V; x:V |] ==> a [*] b [*] x = (a * b) [*] x";
- by (asm_simp only: vs_mult_assoc);
+ by (simp! only: vs_mult_assoc);
lemma vs_mult_1 [simp]: "[| is_vectorspace V; x:V |] ==> 1r [*] x = x";
- by (unfold is_vectorspace_def) asm_simp;
+ by (unfold is_vectorspace_def) (simp!);
lemma vs_diff_mult_distrib1:
"[| is_vectorspace V; x:V; y:V |] ==> a [*] (x [-] y) = a [*] x [-] a [*] y";
- by (asm_simp add: diff_def negate_def vs_add_mult_distrib1);
+ by (simp! add: diff_def negate_def vs_add_mult_distrib1);
lemma vs_minus_eq: "[| is_vectorspace V; x:V |] ==> - b [*] x = [-] (b [*] x)";
- by (asm_simp add: negate_def);
+ by (simp! add: negate_def);
lemma vs_diff_mult_distrib2:
"[| is_vectorspace V; x:V |] ==> (a - b) [*] x = a [*] x [-] (b [*] x)";
@@ -142,7 +152,7 @@
assume "is_vectorspace V" "x:V";
have " (a - b) [*] x = (a + - b ) [*] x"; by (unfold real_diff_def, simp);
also; have "... = a [*] x [+] (- b) [*] x"; by (rule vs_add_mult_distrib2);
- also; have "... = a [*] x [+] [-] (b [*] x)"; by (asm_simp add: vs_minus_eq);
+ also; have "... = a [*] x [+] [-] (b [*] x)"; by (simp! add: vs_minus_eq);
also; have "... = a [*] x [-] (b [*] x)"; by (unfold diff_def, simp);
finally; show ?thesis; .;
qed;
@@ -151,17 +161,17 @@
proof -;
assume vs: "is_vectorspace V" "x:V";
have "0r [*] x = (1r - 1r) [*] x";
- by (asm_simp only: real_diff_self);
+ by (simp! only: real_diff_self);
also; have "... = (1r + - 1r) [*] x";
by simp;
also; have "... = 1r [*] x [+] (- 1r) [*] x";
by (rule vs_add_mult_distrib2);
also; have "... = x [+] (- 1r) [*] x";
- by asm_simp;
+ by (simp!);
also; have "... = x [-] x";
by (rule vs_add_mult_minus_1_eq_diff);
also; have "... = <0>";
- by asm_simp;
+ by (simp!);
finally; show ?thesis; .;
qed;
@@ -169,40 +179,40 @@
proof -;
assume vs: "is_vectorspace V";
have "a [*] <0> = a [*] (<0> [-] (<0>::'a))";
- by (asm_simp);
+ by (simp!);
also; from zero_in_vs [of V]; have "... = a [*] <0> [-] a [*] <0>";
- by (asm_simp only: vs_diff_mult_distrib1);
+ by (simp! only: vs_diff_mult_distrib1);
also; have "... = <0>";
- by asm_simp;
+ by (simp!);
finally; show ?thesis; .;
qed;
lemma vs_minus_mult_cancel [simp]: "[| is_vectorspace V; x:V |] ==> (- a) [*] [-] x = a [*] x";
- by (unfold negate_def) asm_simp;
+ by (unfold negate_def) (simp!);
lemma vs_add_minus_left_eq_diff: "[| is_vectorspace V; x:V; y:V |] ==> [-] x [+] y = y [-] x";
proof -;
assume vs: "is_vectorspace V";
- assume x: "x:V"; hence nx: "[-] x:V"; by asm_simp;
+ assume x: "x:V"; hence nx: "[-] x:V"; by (simp!);
assume y: "y:V";
have "[-] x [+] y = y [+] [-] x";
- by (asm_simp add: vs_add_commute [RS sym, of V "[-] x"]);
+ by (simp! add: vs_add_commute [RS sym, of V "[-] x"]);
also; have "... = y [-] x";
by (simp only: vs_add_minus_eq_diff);
finally; show ?thesis; .;
qed;
lemma vs_add_minus [simp]: "[| is_vectorspace V; x:V|] ==> x [+] [-] x = <0>";
- by (asm_simp add: vs_add_minus_eq_diff);
+ by (simp! add: vs_add_minus_eq_diff);
lemma vs_add_minus_left [simp]: "[| is_vectorspace V; x:V |] ==> [-] x [+] x = <0>";
- by (asm_simp add: vs_add_minus_eq_diff);
+ by (simp! add: vs_add_minus_eq_diff);
lemma vs_minus_minus [simp]: "[| is_vectorspace V; x:V|] ==> [-] [-] x = x";
- by (unfold negate_def) asm_simp;
+ by (unfold negate_def) (simp!);
lemma vs_minus_zero [simp]: "[| is_vectorspace (V::'a set)|] ==> [-] (<0>::'a) = <0>";
- by (unfold negate_def) asm_simp;
+ by (unfold negate_def) (simp!);
lemma vs_minus_zero_iff [simp]:
"[| is_vectorspace V; x:V|] ==> ([-] x = <0>) = (x = <0>)" (concl is "?L = ?R");
@@ -226,20 +236,20 @@
qed;
lemma vs_add_minus_cancel [simp]: "[| is_vectorspace V; x:V; y:V|] ==> x [+] ([-] x [+] y) = y";
- by (asm_simp add: vs_add_assoc [RS sym] del: vs_add_commute);
+ by (simp! add: vs_add_assoc [RS sym] del: vs_add_commute);
lemma vs_minus_add_cancel [simp]: "[| is_vectorspace V; x:V; y:V |] ==> [-] x [+] (x [+] y) = y";
- by (asm_simp add: vs_add_assoc [RS sym] del: vs_add_commute);
+ by (simp! add: vs_add_assoc [RS sym] del: vs_add_commute);
lemma vs_minus_add_distrib [simp]:
"[| is_vectorspace V; x:V; y:V|] ==> [-] (x [+] y) = [-] x [+] [-] y";
- by (unfold negate_def, asm_simp add: vs_add_mult_distrib1);
+ by (unfold negate_def, simp! add: vs_add_mult_distrib1);
lemma vs_diff_zero [simp]: "[| is_vectorspace V; x:V |] ==> x [-] <0> = x";
- by (unfold diff_def) asm_simp;
+ by (unfold diff_def) (simp!);
lemma vs_diff_zero_right [simp]: "[| is_vectorspace V; x:V |] ==> <0> [-] x = [-] x";
- by (unfold diff_def) asm_simp;
+ by (unfold diff_def) (simp!);
lemma vs_add_left_cancel:
"[|is_vectorspace V; x:V; y:V; z:V|] ==> (x [+] y = x [+] z) = (y = z)"
@@ -248,35 +258,34 @@
assume vs: "is_vectorspace V" and x: "x:V" and y: "y:V" and z: "z:V";
assume l: ?L;
have "y = <0> [+] y";
- by asm_simp;
+ by (simp!);
also; have "... = [-] x [+] x [+] y";
- by asm_simp;
+ by (simp!);
also; from vs vs_neg_closed x y ; have "... = [-] x [+] (x [+] y)";
by (rule vs_add_assoc);
also; have "... = [-] x [+] (x [+] z)";
- by (asm_simp only: l);
+ by (simp! only: l);
also; from vs vs_neg_closed x z; have "... = [-] x [+] x [+] z";
by (rule vs_add_assoc [RS sym]);
also; have "... = z";
- by asm_simp;
+ by (simp!);
finally; show ?R;.;
next;
assume ?R;
- show ?L;
- by force;
+ thus ?L; by force;
qed;
lemma vs_add_right_cancel:
"[| is_vectorspace V; x:V; y:V; z:V |] ==> (y [+] x = z [+] x) = (y = z)";
- by (asm_simp only: vs_add_commute vs_add_left_cancel);
+ by (simp! only: vs_add_commute vs_add_left_cancel);
lemma vs_add_assoc_cong [tag FIXME simp]: "[| is_vectorspace V; x:V; y:V; x':V; y':V; z:V |] \
\ ==> x [+] y = x' [+] y' ==> x [+] (y [+] z) = x' [+] (y' [+] z)";
- by (asm_simp del: vs_add_commute vs_add_assoc add: vs_add_assoc [RS sym]);
+ by (simp! del: vs_add_commute vs_add_assoc add: vs_add_assoc [RS sym]);
lemma vs_mult_left_commute:
"[| is_vectorspace V; x:V; y:V; z:V |] ==> x [*] y [*] z = y [*] x [*] z";
- by (asm_simp add: real_mult_commute);
+ by (simp! add: real_mult_commute);
lemma vs_mult_left_cancel:
"[| is_vectorspace V; x:V; y:V; a ~= 0r |] ==> (a [*] x = a [*] y) = (x = y)"
@@ -288,20 +297,20 @@
assume a: "a ~= 0r";
assume l: ?L;
have "x = 1r [*] x";
- by (asm_simp);
+ by (simp!);
also; have "... = (rinv a * a) [*] x";
- by (asm_simp);
+ by (simp!);
also; have "... = rinv a [*] (a [*] x)";
- by (asm_simp only: vs_mult_assoc);
+ by (simp! only: vs_mult_assoc);
also; have "... = rinv a [*] (a [*] y)";
- by (asm_simp only: l);
+ by (simp! only: l);
also; have "... = y";
- by (asm_simp);
+ by (simp!);
finally; show ?R;.;
next;
assume ?R;
show ?L;
- by (asm_simp);
+ by (simp!);
qed;
lemma vs_eq_diff_eq:
@@ -310,32 +319,32 @@
proof -;
assume vs: "is_vectorspace V";
assume x: "x:V";
- assume y: "y:V"; hence n: "[-] y:V"; by asm_simp;
+ assume y: "y:V"; hence n: "[-] y:V"; by (simp!);
assume z: "z:V";
show "?L = ?R";
proof;
assume l: ?L;
have "x [+] y = z [-] y [+] y";
- by (asm_simp add: l);
+ by (simp! add: l);
also; have "... = z [+] [-] y [+] y";
- by (asm_simp only: vs_add_minus_eq_diff);
+ by (simp! only: vs_add_minus_eq_diff);
also; from vs z n y; have "... = z [+] ([-] y [+] y)";
- by (asm_simp only: vs_add_assoc);
+ by (simp! only: vs_add_assoc);
also; have "... = z [+] <0>";
- by (asm_simp only: vs_add_minus_left);
+ by (simp! only: vs_add_minus_left);
also; have "... = z";
- by (asm_simp only: vs_add_zero_right);
+ by (simp! only: vs_add_zero_right);
finally; show ?R;.;
next;
assume r: ?R;
have "z [-] y = (x [+] y) [-] y";
- by (asm_simp only: r);
+ by (simp! only: r);
also; have "... = x [+] y [+] [-] y";
- by (asm_simp only: vs_add_minus_eq_diff);
+ by (simp! only: vs_add_minus_eq_diff);
also; from vs x y n; have "... = x [+] (y [+] [-] y)";
by (rule vs_add_assoc);
also; have "... = x";
- by (asm_simp);
+ by (simp!);
finally; show ?L; by (rule sym);
qed;
qed;
@@ -343,19 +352,19 @@
lemma vs_add_minus_eq_minus: "[| is_vectorspace V; x:V; y:V; <0> = x [+] y|] ==> y = [-] x";
proof -;
assume vs: "is_vectorspace V";
- assume x: "x:V"; hence n: "[-] x : V"; by (asm_simp);
+ assume x: "x:V"; hence n: "[-] x : V"; by (simp!);
assume y: "y:V";
assume xy: "<0> = x [+] y";
from vs n; have "[-] x = [-] x [+] <0>";
- by asm_simp;
+ by (simp!);
also; have "... = [-] x [+] (x [+] y)";
- by (asm_simp);
+ by (simp!);
also; from vs n x y; have "... = [-] x [+] x [+] y";
by (rule vs_add_assoc [RS sym]);
also; from vs x y; have "... = (x [+] [-] x) [+] y";
- by (simp);
+ by simp;
also; from vs y; have "... = y";
- by (asm_simp);
+ by (simp!);
finally; show ?thesis;
by (rule sym);
qed;
@@ -366,10 +375,10 @@
have "x [+] [-] y = x [-] y"; by (unfold diff_def, simp);
also; have "... = <0>"; .;
finally; have e: "<0> = x [+] [-] y"; by (rule sym);
- have "x = [-] [-] x"; by asm_simp;
+ have "x = [-] [-] x"; by (simp!);
also; from _ _ _ e; have "[-] x = [-] y";
- by (rule vs_add_minus_eq_minus [RS sym, of V x "[-] y"]) asm_simp+;
- also; have "[-] ... = y"; by asm_simp;
+ by (rule vs_add_minus_eq_minus [RS sym, of V x "[-] y"]) (simp!)+;
+ also; have "[-] ... = y"; by (simp!);
finally; show "x = y"; .;
qed;
@@ -377,12 +386,12 @@
"[| is_vectorspace V; a:V; b:V; c:V; d:V; a [+] b = c [+] d|] ==> a [-] c = d [-] b";
proof -;
assume vs: "is_vectorspace V" "a:V" "b:V" "c:V" "d:V" and eq: "a [+] b = c [+] d";
- have "[-] c [+] (a [+] b) = [-] c [+] (c [+] d)"; by (asm_simp add: vs_add_left_cancel);
+ have "[-] c [+] (a [+] b) = [-] c [+] (c [+] d)"; by (simp! add: vs_add_left_cancel);
also; have "... = d"; by (rule vs_minus_add_cancel);
finally; have eq: "[-] c [+] (a [+] b) = d"; .;
from vs; have "a [-] c = ([-] c [+] (a [+] b)) [+] [-] b";
by (simp add: vs_add_ac diff_def);
- also; from eq; have "... = d [+] [-] b"; by (asm_simp add: vs_add_right_cancel);
+ also; from eq; have "... = d [+] [-] b"; by (simp! add: vs_add_right_cancel);
also; have "... = d [-] b"; by (simp add : diff_def);
finally; show "a [-] c = d [-] b"; .;
qed;
@@ -393,10 +402,10 @@
proof (rule classical);
assume "is_vectorspace V" "x:V" "a [*] x = <0>" "x ~= <0>";
assume "a ~= 0r";
- have "x = (rinv a * a) [*] x"; by asm_simp;
+ have "x = (rinv a * a) [*] x"; by (simp!);
also; have "... = (rinv a) [*] (a [*] x)"; by (rule vs_mult_assoc);
- also; have "... = (rinv a) [*] <0>"; by asm_simp;
- also; have "... = <0>"; by asm_simp;
+ also; have "... = (rinv a) [*] <0>"; by (simp!);
+ also; have "... = <0>"; by (simp!);
finally; have "x = <0>"; .;
thus "a = 0r"; by contradiction;
qed;
@@ -407,33 +416,33 @@
proof -;
assume vs: "is_vectorspace V";
assume x: "x:V";
- assume y: "y:V"; hence n: "[-] y:V"; by (asm_simp);
- assume z: "z:V"; hence xz: "x [+] z: V"; by (asm_simp);
+ assume y: "y:V"; hence n: "[-] y:V"; by (simp!);
+ assume z: "z:V"; hence xz: "x [+] z: V"; by (simp!);
assume u: "u:V";
show "?L = ?R";
proof;
assume l: ?L;
from vs u; have "u = <0> [+] u";
- by asm_simp;
+ by (simp!);
also; from vs y vs_neg_closed u; have "... = [-] y [+] y [+] u";
- by asm_simp;
+ by (simp!);
also; from vs n y u; have "... = [-] y [+] (y [+] u)";
- by (asm_simp only: vs_add_assoc);
+ by (simp! only: vs_add_assoc);
also; have "... = [-] y [+] (x [+] (y [+] z))";
- by (asm_simp only: l);
+ by (simp! only: l);
also; have "... = [-] y [+] (y [+] (x [+] z))";
- by (asm_simp only: vs_add_left_commute);
+ by (simp! only: vs_add_left_commute);
also; from vs n y xz; have "... = [-] y [+] y [+] (x [+] z)";
- by (asm_simp only: vs_add_assoc);
+ by (simp! only: vs_add_assoc);
also; have "... = (x [+] z)";
- by (asm_simp);
+ by (simp!);
finally; show ?R; by (rule sym);
next;
assume r: ?R;
have "x [+] (y [+] z) = y [+] (x [+] z)";
- by (asm_simp only: vs_add_left_commute [of V x y z]);
+ by (simp! only: vs_add_left_commute [of V x y z]);
also; have "... = y [+] u";
- by (asm_simp only: r);
+ by (simp! only: r);
finally; show ?L; .;
qed;
qed;
@@ -445,41 +454,41 @@
assume vs: "is_vectorspace V";
assume x: "x:V";
assume y: "y:V";
- assume z: "z:V"; hence xz: "x [+] z: V"; by (asm_simp);
- hence nz: "[-] z: V"; by (asm_simp);
+ assume z: "z:V"; hence xz: "x [+] z: V"; by (simp!);
+ hence nz: "[-] z: V"; by (simp!);
show "?L = ?R";
proof;
assume l: ?L;
- have n: "<0>:V"; by (asm_simp);
+ have n: "<0>:V"; by (simp!);
have "y [+] <0> = y";
- by (asm_simp only: vs_add_zero_right);
+ by (simp! only: vs_add_zero_right);
also; have "... = x [+] (y [+] z)";
- by (asm_simp only: l);
+ by (simp! only: l);
also; have "... = y [+] (x [+] z)";
- by (asm_simp only: vs_add_left_commute);
+ by (simp! only: vs_add_left_commute);
finally; have "y [+] <0> = y [+] (x [+] z)"; .;
with vs y n xz; have "<0> = x [+] z";
by (rule vs_add_left_cancel [RS iffD1]);
with vs x z; have "z = [-] x";
- by (asm_simp only: vs_add_minus_eq_minus);
+ by (simp! only: vs_add_minus_eq_minus);
then; show ?R;
- by (asm_simp);
+ by (simp!);
next;
assume r: ?R;
have "x [+] (y [+] z) = [-] z [+] (y [+] z)";
- by (asm_simp only: r);
+ by (simp! only: r);
also; from vs nz y z; have "... = y [+] ([-] z [+] z)";
- by (asm_simp only: vs_add_left_commute);
+ by (simp! only: vs_add_left_commute);
also; have "... = y [+] <0>";
- by (asm_simp);
+ by (simp!);
also; have "... = y";
- by (asm_simp);
+ by (simp!);
finally; show ?L; .;
qed;
qed;
lemma it: "[| x = y; x' = y'|] ==> x [+] x' = y [+] y'";
- by (asm_simp);
+ by (simp!);
end;
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/Linearform.thy Tue Sep 21 17:30:55 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Linearform.thy Tue Sep 21 17:31:20 1999 +0200
@@ -1,3 +1,7 @@
+(* Title: HOL/Real/HahnBanach/Linearform.thy
+ ID: $Id$
+ Author: Gertrud Bauer, TU Munich
+*)
theory Linearform = LinearSpace:;
@@ -12,39 +16,41 @@
lemma is_linearformI [intro]: "[| !! x y. [| x : V; y : V |] ==> f (x [+] y) = f x + f y;
!! x c. x : V ==> f (c [*] x) = c * f x |]
==> is_linearform V f";
- by (unfold is_linearform_def, force);
+ by (unfold is_linearform_def) force;
-lemma linearform_add_linear: "[| is_linearform V f; x:V; y:V |] ==> f (x [+] y) = f x + f y";
- by (unfold is_linearform_def, auto);
+lemma linearform_add_linear [intro!!]:
+ "[| is_linearform V f; x:V; y:V |] ==> f (x [+] y) = f x + f y";
+ by (unfold is_linearform_def) auto;
-lemma linearform_mult_linear: "[| is_linearform V f; x:V |] ==> f (a [*] x) = a * (f x)";
- by (unfold is_linearform_def, auto);
+lemma linearform_mult_linear [intro!!]:
+ "[| is_linearform V f; x:V |] ==> f (a [*] x) = a * (f x)";
+ by (unfold is_linearform_def) auto;
-lemma linearform_neg_linear:
+lemma linearform_neg_linear [intro!!]:
"[| is_vectorspace V; is_linearform V f; x:V|] ==> f ([-] x) = - f x";
proof -;
assume "is_linearform V f" "is_vectorspace V" "x:V";
- have "f ([-] x) = f ((- 1r) [*] x)"; by (asm_simp add: vs_mult_minus_1);
+ have "f ([-] x) = f ((- 1r) [*] x)"; by (simp! add: vs_mult_minus_1);
also; have "... = (- 1r) * (f x)"; by (rule linearform_mult_linear);
- also; have "... = - (f x)"; by asm_simp;
+ also; have "... = - (f x)"; by (simp!);
finally; show ?thesis; .;
qed;
-lemma linearform_diff_linear:
+lemma linearform_diff_linear [intro!!]:
"[| is_vectorspace V; is_linearform V f; x:V; y:V |] ==> f (x [-] y) = f x - f y";
proof -;
assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V";
have "f (x [-] y) = f (x [+] [-] y)"; by (simp only: diff_def);
- also; have "... = f x + f ([-] y)"; by (rule linearform_add_linear) (asm_simp+);
+ also; have "... = f x + f ([-] y)"; by (rule linearform_add_linear) (simp!)+;
also; have "f ([-] y) = - f y"; by (rule linearform_neg_linear);
- finally; show "f (x [-] y) = f x - f y"; by asm_simp;
+ finally; show "f (x [-] y) = f x - f y"; by (simp!);
qed;
-lemma linearform_zero: "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r";
+lemma linearform_zero [intro!!]: "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r";
proof -;
assume "is_vectorspace V" "is_linearform V f";
- have "f <0> = f (<0> [-] <0>)"; by asm_simp;
- also; have "... = f <0> - f <0>"; by (rule linearform_diff_linear) asm_simp+;
+ have "f <0> = f (<0> [-] <0>)"; by (simp!);
+ also; have "... = f <0> - f <0>"; by (rule linearform_diff_linear) (simp!)+;
also; have "... = 0r"; by simp;
finally; show "f <0> = 0r"; .;
qed;
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy Tue Sep 21 17:30:55 1999 +0200
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Tue Sep 21 17:31:20 1999 +0200
@@ -1,3 +1,7 @@
+(* Title: HOL/Real/HahnBanach/NormedSpace.thy
+ ID: $Id$
+ Author: Gertrud Bauer, TU Munich
+*)
theory NormedSpace = Subspace:;
@@ -20,31 +24,31 @@
==> is_quasinorm V norm";
by (unfold is_quasinorm_def, force);
-lemma quasinorm_ge_zero:
- "[|is_quasinorm V norm; x:V |] ==> 0r <= norm x";
+lemma quasinorm_ge_zero [intro!!]:
+ "[| is_quasinorm V norm; x:V |] ==> 0r <= norm x";
by (unfold is_quasinorm_def, force);
lemma quasinorm_mult_distrib:
- "[|is_quasinorm V norm; x:V |] ==> norm (a [*] x) = (rabs a) * (norm x)";
+ "[| is_quasinorm V norm; x:V |] ==> norm (a [*] x) = (rabs a) * (norm x)";
by (unfold is_quasinorm_def, force);
lemma quasinorm_triangle_ineq:
- "[|is_quasinorm V norm; x:V; y:V |] ==> norm (x [+] y) <= norm x + norm y";
+ "[| is_quasinorm V norm; x:V; y:V |] ==> norm (x [+] y) <= norm x + norm y";
by (unfold is_quasinorm_def, force);
lemma quasinorm_diff_triangle_ineq:
- "[|is_quasinorm V norm; x:V; y:V; is_vectorspace V |] ==> norm (x [-] y) <= norm x + norm y";
+ "[| is_quasinorm V norm; x:V; y:V; is_vectorspace V |] ==> norm (x [-] y) <= norm x + norm y";
proof -;
assume "is_quasinorm V norm" "x:V" "y:V" "is_vectorspace V";
have "norm (x [-] y) = norm (x [+] - 1r [*] y)"; by (simp add: diff_def negate_def);
- also; have "... <= norm x + norm (- 1r [*] y)"; by (rule quasinorm_triangle_ineq, asm_simp+);
+ also; have "... <= norm x + norm (- 1r [*] y)"; by (simp! add: quasinorm_triangle_ineq);
also; have "norm (- 1r [*] y) = rabs (- 1r) * norm y"; by (rule quasinorm_mult_distrib);
also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one);
finally; show "norm (x [-] y) <= norm x + norm y"; by simp;
qed;
lemma quasinorm_minus:
- "[|is_quasinorm V norm; x:V; is_vectorspace V |] ==> norm ([-] x) = norm x";
+ "[| is_quasinorm V norm; x:V; is_vectorspace V |] ==> norm ([-] x) = norm x";
proof -;
assume "is_quasinorm V norm" "x:V" "is_vectorspace V";
have "norm ([-] x) = norm (-1r [*] x)"; by (unfold negate_def) force;
@@ -61,18 +65,19 @@
"is_norm V norm == ALL x: V. is_quasinorm V norm
& (norm x = 0r) = (x = <0>)";
-lemma is_norm_I: "ALL x: V. is_quasinorm V norm & (norm x = 0r) = (x = <0>) ==> is_norm V norm";
+lemma is_normI [intro]:
+ "ALL x: V. is_quasinorm V norm & (norm x = 0r) = (x = <0>) ==> is_norm V norm";
by (unfold is_norm_def, force);
-lemma norm_is_quasinorm: "[| is_norm V norm; x:V |] ==> is_quasinorm V norm";
+lemma norm_is_quasinorm [intro!!]: "[| is_norm V norm; x:V |] ==> is_quasinorm V norm";
by (unfold is_norm_def, force);
lemma norm_zero_iff: "[| is_norm V norm; x:V |] ==> (norm x = 0r) = (x = <0>)";
by (unfold is_norm_def, force);
-lemma norm_ge_zero:
+lemma norm_ge_zero [intro!!]:
"[|is_norm V norm; x:V |] ==> 0r <= norm x";
- by (unfold is_norm_def, unfold is_quasinorm_def, force);
+ by (unfold is_norm_def is_quasinorm_def, force);
subsection {* normed vector space *};
@@ -83,60 +88,65 @@
is_vectorspace V &
is_norm V norm";
-lemma normed_vsI: "[| is_vectorspace V; is_norm V norm |] ==> is_normed_vectorspace V norm";
- by (unfold is_normed_vectorspace_def, intro conjI);
+lemma normed_vsI [intro]:
+ "[| is_vectorspace V; is_norm V norm |] ==> is_normed_vectorspace V norm";
+ by (unfold is_normed_vectorspace_def) blast;
-lemma normed_vs_vs: "is_normed_vectorspace V norm ==> is_vectorspace V";
- by (unfold is_normed_vectorspace_def, force);
+lemma normed_vs_vs [intro!!]: "is_normed_vectorspace V norm ==> is_vectorspace V";
+ by (unfold is_normed_vectorspace_def) force;
-lemma normed_vs_norm: "is_normed_vectorspace V norm ==> is_norm V norm";
- by (unfold is_normed_vectorspace_def, force);
+lemma normed_vs_norm [intro!!]: "is_normed_vectorspace V norm ==> is_norm V norm";
+ by (unfold is_normed_vectorspace_def, elim conjE);
-lemma normed_vs_norm_ge_zero: "[| is_normed_vectorspace V norm; x:V |] ==> 0r <= norm x";
- by (unfold is_normed_vectorspace_def, elim conjE, rule norm_ge_zero);
+lemma normed_vs_norm_ge_zero [intro!!]: "[| is_normed_vectorspace V norm; x:V |] ==> 0r <= norm x";
+ by (unfold is_normed_vectorspace_def, rule, elim conjE);
-lemma normed_vs_norm_gt_zero:
+lemma normed_vs_norm_gt_zero [intro!!]:
"[| is_normed_vectorspace V norm; x:V; x ~= <0> |] ==> 0r < norm x";
proof (unfold is_normed_vectorspace_def, elim conjE);
assume "x : V" "x ~= <0>" "is_vectorspace V" "is_norm V norm";
- have "0r <= norm x"; by (rule norm_ge_zero);
+ have "0r <= norm x"; ..;
also; have "0r ~= norm x";
- proof;
+ proof;
presume "norm x = 0r";
- have "x = <0>"; by (asm_simp add: norm_zero_iff);
+ also; have "?this = (x = <0>)"; by (rule norm_zero_iff);
+ finally; have "x = <0>"; .;
thus "False"; by contradiction;
qed (rule sym);
finally; show "0r < norm x"; .;
qed;
-lemma normed_vs_norm_mult_distrib:
+lemma normed_vs_norm_mult_distrib [intro!!]:
"[| is_normed_vectorspace V norm; x:V |] ==> norm (a [*] x) = (rabs a) * (norm x)";
- by (unfold is_normed_vectorspace_def, elim conjE,
- rule quasinorm_mult_distrib, rule norm_is_quasinorm);
+ by (rule quasinorm_mult_distrib, rule norm_is_quasinorm, rule normed_vs_norm);
-lemma normed_vs_norm_triangle_ineq:
+lemma normed_vs_norm_triangle_ineq [intro!!]:
"[| is_normed_vectorspace V norm; x:V; y:V |] ==> norm (x [+] y) <= norm x + norm y";
- by (unfold is_normed_vectorspace_def, elim conjE,
- rule quasinorm_triangle_ineq, rule norm_is_quasinorm);
+ by (rule quasinorm_triangle_ineq, rule norm_is_quasinorm, rule normed_vs_norm);
-lemma subspace_normed_vs:
- "[| is_subspace F E; is_vectorspace E; is_normed_vectorspace E norm |] ==> is_normed_vectorspace F norm";
+lemma subspace_normed_vs [intro!!]:
+ "[| is_subspace F E; is_vectorspace E; is_normed_vectorspace E norm |]
+ ==> is_normed_vectorspace F norm";
proof (rule normed_vsI);
assume "is_subspace F E" "is_vectorspace E" "is_normed_vectorspace E norm";
- show "is_vectorspace F"; by (rule subspace_vs);
+ show "is_vectorspace F"; ..;
show "is_norm F norm";
- proof (intro is_norm_I ballI conjI);
+ proof (intro is_normI ballI conjI);
show "is_quasinorm F norm";
- proof (rule is_quasinormI, rule normed_vs_norm_ge_zero [of E norm],
- rule normed_vs_norm_mult_distrib [of E norm], rule normed_vs_norm_triangle_ineq);
- qed ( rule subsetD [OF subspace_subset], assumption+)+;
+ proof;
+ fix x y a; presume "x : E";
+ show "0r <= norm x"; ..;
+ show "norm (a [*] x) = rabs a * norm x"; ..;
+ presume "y : E";
+ show "norm (x [+] y) <= norm x + norm y"; ..;
+ qed (simp!)+;
fix x; assume "x : F";
- have n: "is_norm E norm"; by (unfold is_normed_vectorspace_def, asm_simp);
- have "x:E"; by (rule subsetD [OF subspace_subset]);
- from n this; show "(norm x = 0r) = (x = <0>)"; by (rule norm_zero_iff);
+ show "(norm x = 0r) = (x = <0>)";
+ proof (rule norm_zero_iff);
+ show "is_norm E norm"; ..;
+ qed (simp!);
qed;
qed;
end;
-
--- a/src/HOL/Real/HahnBanach/Subspace.thy Tue Sep 21 17:30:55 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy Tue Sep 21 17:31:20 1999 +0200
@@ -1,3 +1,7 @@
+(* Title: HOL/Real/HahnBanach/Subspace.thy
+ ID: $Id$
+ Author: Gertrud Bauer, TU Munich
+*)
theory Subspace = LinearSpace:;
@@ -10,74 +14,75 @@
& (ALL x:U. ALL y:U. ALL a. x [+] y : U
& a [*] x : U)";
-lemma subspace_I:
+lemma subspaceI [intro]:
"[| <0>:U; U <= V; ALL x:U. ALL y:U. (x [+] y : U); ALL x:U. ALL a. a [*] x : U |]
\ ==> is_subspace U V";
- by (unfold is_subspace_def) blast;
+ by (unfold is_subspace_def) (simp!);
lemma "is_subspace U V ==> U ~= {}";
by (unfold is_subspace_def) force;
-lemma zero_in_subspace: "is_subspace U V ==> <0>:U";
+lemma zero_in_subspace [intro !!]: "is_subspace U V ==> <0>:U";
+ by (unfold is_subspace_def) (simp!);;
+
+lemma subspace_subset [intro !!]: "is_subspace U V ==> U <= V";
+ by (unfold is_subspace_def) (simp!);
+
+lemma subspace_subsetD [simp, intro!!]: "[| is_subspace U V; x:U |]==> x:V";
by (unfold is_subspace_def) force;
-lemma subspace_subset: "is_subspace U V ==> U <= V";
- by (unfold is_subspace_def) fast;
+lemma subspace_add_closed [simp, intro!!]: "[| is_subspace U V; x: U; y: U |] ==> x [+] y: U";
+ by (unfold is_subspace_def) (simp!);
-lemma subspace_subset2 [simp]: "[| is_subspace U V; x:U |]==> x:V";
- by (unfold is_subspace_def) fast;
-
-lemma subspace_add_closed [simp]: "[| is_subspace U V; x: U; y: U |] ==> x [+] y: U";
- by (unfold is_subspace_def) asm_simp;
+lemma subspace_mult_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> a [*] x: U";
+ by (unfold is_subspace_def) (simp!);
-lemma subspace_mult_closed [simp]: "[| is_subspace U V; x: U |] ==> a [*] x: U";
- by (unfold is_subspace_def) asm_simp;
+lemma subspace_diff_closed [simp, intro!!]: "[| is_subspace U V; x: U; y: U |] ==> x [-] y: U";
+ by (unfold diff_def negate_def) (simp!);
-lemma subspace_diff_closed [simp]: "[| is_subspace U V; x: U; y: U |] ==> x [-] y: U";
- by (unfold diff_def negate_def) asm_simp;
+lemma subspace_neg_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> [-] x: U";
+ by (unfold negate_def) (simp!);
-lemma subspace_neg_closed [simp]: "[| is_subspace U V; x: U |] ==> [-] x: U";
- by (unfold negate_def) asm_simp;
theorem subspace_vs [intro!!]:
"[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U";
proof -;
- presume "U <= V";
+ assume "is_subspace U V";
assume "is_vectorspace V";
assume "is_subspace U V";
show ?thesis;
- proof (rule vs_I);
- show "<0>:U"; by (rule zero_in_subspace);
- show "ALL x:U. ALL a. a [*] x : U"; by asm_simp;
- show "ALL x:U. ALL y:U. x [+] y : U"; by asm_simp;
- qed (asm_simp add: vs_add_mult_distrib1 vs_add_mult_distrib2)+;
-next;
- assume "is_subspace U V";
- show "U <= V"; by (rule subspace_subset);
+ proof;
+ show "<0>:U"; ..;
+ show "ALL x:U. ALL a. a [*] x : U"; by (simp!);
+ show "ALL x:U. ALL y:U. x [+] y : U"; by (simp!);
+ qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+;
qed;
-lemma subspace_refl: "is_vectorspace V ==> is_subspace V V";
-proof (unfold is_subspace_def, intro conjI);
+lemma subspace_refl [intro]: "is_vectorspace V ==> is_subspace V V";
+proof;
assume "is_vectorspace V";
- show "<0> : V"; by (rule zero_in_vs [of V], assumption);
- show "V <= V"; by (simp);
- show "ALL x::'a:V. ALL y::'a:V. ALL a::real. x [+] y : V & a [*] x : V"; by (asm_simp);
+ show "<0> : V"; ..;
+ show "V <= V"; ..;
+ show "ALL x:V. ALL y:V. x [+] y : V"; by (simp!);
+ show "ALL x:V. ALL a. a [*] x : V"; by (simp!);
qed;
lemma subspace_trans: "[| is_subspace U V; is_subspace V W |] ==> is_subspace U W";
-proof (rule subspace_I);
+proof;
assume "is_subspace U V" "is_subspace V W";
- show "<0> : U"; by (rule zero_in_subspace);;
- from subspace_subset [of U] subspace_subset [of V]; show uw: "U <= W"; by force;
+ show "<0> : U"; ..;
+ have "U <= V"; ..;
+ also; have "V <= W"; ..;
+ finally; show "U <= W"; .;
show "ALL x:U. ALL y:U. x [+] y : U";
proof (intro ballI);
fix x y; assume "x:U" "y:U";
- show "x [+] y : U"; by (rule subspace_add_closed);
+ show "x [+] y : U"; by (simp!);
qed;
show "ALL x:U. ALL a. a [*] x : U";
proof (intro ballI allI);
fix x a; assume "x:U";
- show "a [*] x : U"; by (rule subspace_mult_closed);
+ show "a [*] x : U"; by (simp!);
qed;
qed;
@@ -89,39 +94,45 @@
"lin x == {y. ? a. y = a [*] x}";
lemma linD: "x : lin v = (? a::real. x = a [*] v)";
- by (unfold lin_def) fast;
+ by (unfold lin_def) force;
lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x:lin x";
proof (unfold lin_def, intro CollectI exI);
assume "is_vectorspace V" "x:V";
- show "x = 1r [*] x"; by (asm_simp);
+ show "x = 1r [*] x"; by (simp!);
qed;
-lemma lin_subspace: "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V";
-proof (rule subspace_I);
+lemma lin_subspace [intro!!]: "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V";
+proof;
assume "is_vectorspace V" "x:V";
show "<0> : lin x";
proof (unfold lin_def, intro CollectI exI);
- show "<0> = 0r [*] x"; by asm_simp;
+ show "<0> = 0r [*] x"; by (simp!);
qed;
+
show "lin x <= V";
- proof (unfold lin_def, intro subsetI, elim CollectD [elimify] exE);
- fix xa a; assume "xa = a [*] x"; show "xa:V"; by asm_simp;
+ proof (unfold lin_def, intro subsetI, elim CollectE exE);
+ fix xa a; assume "xa = a [*] x";
+ show "xa:V"; by (simp!);
qed;
+
show "ALL x1 : lin x. ALL x2 : lin x. x1 [+] x2 : lin x";
proof (intro ballI);
- fix x1 x2; assume "x1 : lin x" "x2 : lin x"; show "x1 [+] x2 : lin x";
- proof (unfold lin_def, elim CollectD [elimify] exE, intro CollectI exI);
+ fix x1 x2; assume "x1 : lin x" "x2 : lin x";
+ thus "x1 [+] x2 : lin x";
+ proof (-, unfold lin_def, elim CollectE exE, intro CollectI exI); (* FIXME !? *)
fix a1 a2; assume "x1 = a1 [*] x" "x2 = a2 [*] x";
- show "x1 [+] x2 = (a1 + a2) [*] x"; by (asm_simp add: vs_add_mult_distrib2);
+ show "x1 [+] x2 = (a1 + a2) [*] x"; by (simp! add: vs_add_mult_distrib2);
qed;
qed;
+
show "ALL xa:lin x. ALL a. a [*] xa : lin x";
proof (intro ballI allI);
- fix x1 a; assume "x1 : lin x"; show "a [*] x1 : lin x";
- proof (unfold lin_def, elim CollectD [elimify] exE, intro CollectI exI);
+ fix x1 a; assume "x1 : lin x";
+ thus "a [*] x1 : lin x";
+ proof (-, unfold lin_def, elim CollectE exE, intro CollectI exI);
fix a1; assume "x1 = a1 [*] x";
- show "a [*] x1 = (a * a1) [*] x"; by asm_simp;
+ show "a [*] x1 = (a * a1) [*] x"; by (simp!);
qed;
qed;
qed;
@@ -130,7 +141,7 @@
lemma lin_vs [intro!!]: "[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)";
proof (rule subspace_vs);
assume "is_vectorspace V" "x:V";
- show "is_subspace (lin x) V"; by (rule lin_subspace);
+ show "is_subspace (lin x) V"; ..;
qed;
section {* sum of two vectorspaces *};
@@ -140,159 +151,181 @@
"vectorspace_sum U V == {x. ? u:U. ? v:V. x = u [+] v}";
lemma vs_sumD: "x:vectorspace_sum U V = (? u:U. ? v:V. x = u [+] v)";
- by (unfold vectorspace_sum_def) fast;
+ by (unfold vectorspace_sum_def) (simp!);
-lemma vs_sum_I: "[| x: U; y:V; (t::'a) = x [+] y |] ==> (t::'a) : vectorspace_sum U V";
+lemmas vs_sumE = vs_sumD [RS iffD1, elimify];
+
+lemma vs_sumI [intro!!]: "[| x: U; y:V; (t::'a) = x [+] y |] ==> (t::'a) : vectorspace_sum U V";
by (unfold vectorspace_sum_def, intro CollectI bexI);
lemma subspace_vs_sum1 [intro!!]:
"[| is_vectorspace U; is_vectorspace V |] ==> is_subspace U (vectorspace_sum U V)";
-proof (rule subspace_I);
+proof;
assume "is_vectorspace U" "is_vectorspace V";
- show "<0> : U"; by (rule zero_in_vs);
+ show "<0> : U"; ..;
show "U <= vectorspace_sum U V";
- proof (intro subsetI vs_sum_I);
+ proof (intro subsetI vs_sumI);
fix x; assume "x:U";
- show "x = x [+] <0>"; by asm_simp;
- show "<0> : V"; by asm_simp;
+ show "x = x [+] <0>"; by (simp!);
+ show "<0> : V"; by (simp!);
qed;
show "ALL x:U. ALL y:U. x [+] y : U";
proof (intro ballI);
- fix x y; assume "x:U" "y:U"; show "x [+] y : U"; by asm_simp;
+ fix x y; assume "x:U" "y:U"; show "x [+] y : U"; by (simp!);
qed;
show "ALL x:U. ALL a. a [*] x : U";
proof (intro ballI allI);
- fix x a; assume "x:U"; show "a [*] x : U"; by asm_simp;
+ fix x a; assume "x:U"; show "a [*] x : U"; by (simp!);
qed;
qed;
-lemma vs_sum_subspace:
- "[| is_subspace U E; is_subspace V E; is_vectorspace E |] ==> is_subspace (vectorspace_sum U V) E";
-proof (rule subspace_I);
- assume u: "is_subspace U E" and v: "is_subspace V E" and e: "is_vectorspace E";
+lemma vs_sum_subspace [intro!!]:
+ "[| is_subspace U E; is_subspace V E; is_vectorspace E |]
+ ==> is_subspace (vectorspace_sum U V) E";
+proof;
+ assume "is_subspace U E" "is_subspace V E" and e: "is_vectorspace E";
show "<0> : vectorspace_sum U V";
- by (intro vs_sum_I, rule vs_add_zero_left [RS sym],
- rule zero_in_subspace, rule zero_in_subspace, rule zero_in_vs);
-
+ proof (intro vs_sumI);
+ show "<0> : U"; ..;
+ show "<0> : V"; ..;
+ show "(<0>::'a) = <0> [+] <0>";
+ by (simp!);
+ qed;
+
show "vectorspace_sum U V <= E";
- proof (intro subsetI, elim vs_sumD [RS iffD1, elimify] bexE);
+ proof (intro subsetI, elim vs_sumE bexE);
fix x u v; assume "u : U" "v : V" "x = u [+] v";
- show "x:E"; by (asm_simp);
+ show "x:E"; by (simp!);
qed;
show "ALL x:vectorspace_sum U V. ALL y:vectorspace_sum U V. x [+] y : vectorspace_sum U V";
- proof (intro ballI, elim vs_sumD [RS iffD1, elimify] bexE, intro vs_sum_I);
- fix x y ux vx uy vy; assume "ux : U" "vx : V" "x = ux [+] vx" "uy : U" "vy : V" "y = uy [+] vy";
- show "x [+] y = (ux [+] uy) [+] (vx [+] vy)"; by asm_simp;
- qed asm_simp+;
+ proof (intro ballI);
+ fix x y; assume "x:vectorspace_sum U V" "y:vectorspace_sum U V";
+ thus "x [+] y : vectorspace_sum U V";
+ proof (elim vs_sumE bexE, intro vs_sumI);
+ fix ux vx uy vy;
+ assume "ux : U" "vx : V" "x = ux [+] vx" "uy : U" "vy : V" "y = uy [+] vy";
+ show "x [+] y = (ux [+] uy) [+] (vx [+] vy)"; by (simp!);
+ qed (simp!)+;
+ qed;
show "ALL x:vectorspace_sum U V. ALL a. a [*] x : vectorspace_sum U V";
- proof (intro ballI allI, elim vs_sumD [RS iffD1, elimify] bexE, intro vs_sum_I);
- fix a x u v; assume "u : U" "v : V" "x = u [+] v";
- show "a [*] x = (a [*] u) [+] (a [*] v)"; by (asm_simp add: vs_add_mult_distrib1 [OF e]);
- qed asm_simp+;
+ proof (intro ballI allI);
+ fix x a; assume "x:vectorspace_sum U V";
+ thus "a [*] x : vectorspace_sum U V";
+ proof (elim vs_sumE bexE, intro vs_sumI);
+ fix a x u v; assume "u : U" "v : V" "x = u [+] v";
+ show "a [*] x = (a [*] u) [+] (a [*] v)"; by (simp! add: vs_add_mult_distrib1);
+ qed (simp!)+;
+ qed;
qed;
-lemma vs_sum_vs:
- "[| is_subspace U E; is_subspace V E; is_vectorspace E |] ==> is_vectorspace (vectorspace_sum U V)";
- by (rule subspace_vs [OF vs_sum_subspace]);
+lemma vs_sum_vs [intro!!]:
+ "[| is_subspace U E; is_subspace V E; is_vectorspace E |]
+ ==> is_vectorspace (vectorspace_sum U V)";
+proof (rule subspace_vs);
+ assume "is_subspace U E" "is_subspace V E" "is_vectorspace E";
+ show "is_subspace (vectorspace_sum U V) E"; ..;
+qed;
section {* special case: direct sum of a vectorspace and a linear closure of a vector *};
-
-lemma lemma4: "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; x0 ~: H; x0 :E;
+lemma decomp4: "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; x0 ~: H; x0 :E;
x0 ~= <0>; y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0 |]
==> y1 = y2 & a1 = a2";
proof;
assume "is_vectorspace E" "is_subspace H E"
"y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= <0>"
"y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0";
- have h: "is_vectorspace H"; by (rule subspace_vs);
- have "y1 [-] y2 = a2 [*] x0 [-] a1 [*] x0";
- by (rule vs_add_diff_swap) asm_simp+;
+ have h: "is_vectorspace H"; ..;
+ have "y1 [-] y2 = a2 [*] x0 [-] a1 [*] x0";
+ by (simp! add: vs_add_diff_swap);
also; have "... = (a2 - a1) [*] x0";
by (rule vs_diff_mult_distrib2 [RS sym]);
finally; have eq: "y1 [-] y2 = (a2 - a1) [*] x0"; .;
- have y: "y1 [-] y2 : H"; by asm_simp;
- have x: "(a2 - a1) [*] x0 : lin x0"; by (asm_simp add: lin_def) force;
- from y; have y': "y1 [-] y2 : lin x0"; by (simp only: eq x);
- from x; have x': "(a2 - a1) [*] x0 : H"; by (simp only: eq [RS sym] y);
+ have y: "y1 [-] y2 : H"; by (simp!);
+ have x: "(a2 - a1) [*] x0 : lin x0"; by (simp! add: lin_def) force;
+ from eq y x; have y': "y1 [-] y2 : lin x0"; by simp;
+ from eq y x; have x': "(a2 - a1) [*] x0 : H"; by simp;
have int: "H Int (lin x0) = {<0>}";
proof;
show "H Int lin x0 <= {<0>}";
- proof (intro subsetI, unfold lin_def, elim IntE CollectD[elimify] exE,
- rule singleton_iff[RS iffD2]);
- fix x a; assume "x : H" and ax0: "x = a [*] x0";
- show "x = <0>";
- proof (rule case [of "a=0r"]);
- assume "a = 0r"; show ?thesis; by asm_simp;
- next;
- assume "a ~= 0r";
- have "(rinv a) [*] a [*] x0 : H";
- by (rule vs_mult_closed [OF h]) asm_simp;
- also; have "(rinv a) [*] a [*] x0 = x0"; by asm_simp;
- finally; have "x0 : H"; .;
- thus ?thesis; by contradiction;
- qed;
+ proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]);
+ fix x; assume "x:H" "x:lin x0";
+ thus "x = <0>";
+ proof (-, unfold lin_def, elim CollectE exE);
+ fix a; assume "x = a [*] x0";
+ show ?thesis;
+ proof (rule case [of "a = 0r"]);
+ assume "a = 0r"; show ?thesis; by (simp!);
+ next;
+ assume "a ~= 0r";
+ have "(rinv a) [*] a [*] x0 : H";
+ by (rule vs_mult_closed [OF h]) (simp!);
+ also; have "(rinv a) [*] a [*] x0 = x0"; by (simp!);
+ finally; have "x0 : H"; .;
+ thus ?thesis; by contradiction;
+ qed;
+ qed;
qed;
- show "{<0>} <= H Int lin x0";
- proof (intro subsetI, elim singletonD[elimify], intro IntI, asm_simp+);
- show "<0> : H"; by (rule zero_in_vs [OF h]);
- show "<0> : lin x0"; by (rule zero_in_vs [OF lin_vs]);
+ show "{<0>} <= H Int lin x0";
+ proof (intro subsetI, elim singletonE, intro IntI, simp+);
+ show "<0> : H"; ..;
+ from lin_vs; show "<0> : lin x0"; ..;
qed;
qed;
from h; show "y1 = y2";
proof (rule vs_add_minus_eq);
- show "y1 [-] y2 = <0>";
- by (rule Int_singeltonD [OF int y y']);
+ show "y1 [-] y2 = <0>";
+ by (rule Int_singletonD [OF int y y']);
qed;
show "a1 = a2";
proof (rule real_add_minus_eq [RS sym]);
show "a2 - a1 = 0r";
proof (rule vs_mult_zero_uniq);
- show "(a2 - a1) [*] x0 = <0>"; by (rule Int_singeltonD [OF int x' x]);
+ show "(a2 - a1) [*] x0 = <0>"; by (rule Int_singletonD [OF int x' x]);
qed;
qed;
qed;
-lemma lemma1:
+lemma decomp1:
"[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E; x0 ~= <0> |]
==> (@ (y, a). t = y [+] a [*] x0 & y : H) = (t, 0r)";
proof (rule, unfold split_paired_all);
assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E" "x0 ~= <0>";
- have h: "is_vectorspace H"; by (rule subspace_vs);
+ have h: "is_vectorspace H"; ..;
fix y a; presume t1: "t = y [+] a [*] x0" and "y : H";
have "y = t & a = 0r";
- by (rule lemma4) (assumption+, asm_simp);
- thus "(y, a) = (t, 0r)"; by asm_simp;
-qed asm_simp+;
+ by (rule decomp4) (assumption+, (simp!));
+ thus "(y, a) = (t, 0r)"; by (simp!);
+qed (simp!)+;
-lemma lemma3: "!! x0 h xi x y a H. [| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H)
- in (h y) + a * xi);
- x = y [+] a [*] x0;
- is_vectorspace E; is_subspace H E; y:H; x0 ~: H; x0:E; x0 ~= <0> |]
+lemma decomp3:
+ "[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H)
+ in (h y) + a * xi);
+ x = y [+] a [*] x0;
+ is_vectorspace E; is_subspace H E; y:H; x0 ~: H; x0:E; x0 ~= <0> |]
==> h0 x = h y + a * xi";
proof -;
- fix x0 h xi x y a H;
assume "h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H)
- in (h y) + a * xi)";
+ in (h y) + a * xi)";
assume "x = y [+] a [*] x0";
assume "is_vectorspace E" "is_subspace H E" "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
have "x : vectorspace_sum H (lin x0)";
- by (asm_simp add: vectorspace_sum_def lin_def, intro bexI exI conjI) force+;
+ by (simp! add: vectorspace_sum_def lin_def, intro bexI exI conjI) force+;
have "EX! xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)";
proof;
- show "EX xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)";
- by (asm_simp, rule exI, force);
+ show "EX xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)";
+ by (force!);
next;
fix xa ya;
assume "(%(y,a). x = y [+] a [*] x0 & y : H) xa"
@@ -300,18 +333,18 @@
show "xa = ya"; ;
proof -;
show "fst xa = fst ya & snd xa = snd ya ==> xa = ya";
- by(rule Pair_fst_snd_eq [RS iffD2]);
- have x: "x = (fst xa) [+] (snd xa) [*] x0 & (fst xa) : H"; by force;
- have y: "x = (fst ya) [+] (snd ya) [*] x0 & (fst ya) : H"; by force;
+ by (rule Pair_fst_snd_eq [RS iffD2]);
+ have x: "x = (fst xa) [+] (snd xa) [*] x0 & (fst xa) : H"; by (force!);
+ have y: "x = (fst ya) [+] (snd ya) [*] x0 & (fst ya) : H"; by (force!);
from x y; show "fst xa = fst ya & snd xa = snd ya";
- by (elim conjE) (rule lemma4, asm_simp+);
+ by (elim conjE) (rule decomp4, (simp!)+);
qed;
qed;
hence eq: "(@ (y, a). (x = y [+] a [*] x0 & y:H)) = (y, a)";
- by (rule select1_equality, force);
+ by (rule select1_equality) (force!);
thus "h0 x = h y + a * xi";
- by (asm_simp add: Let_def);
-qed;
+ by (simp! add: Let_def);
+qed;
end;
--- a/src/HOL/Real/HahnBanach/Zorn_Lemma.thy Tue Sep 21 17:30:55 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Zorn_Lemma.thy Tue Sep 21 17:31:20 1999 +0200
@@ -1,5 +1,9 @@
+(* Title: HOL/Real/HahnBanach/Zorn_Lemma.thy
+ ID: $Id$
+ Author: Gertrud Bauer, TU Munich
+*)
-theory Zorn_Lemma = Zorn:;
+theory Zorn_Lemma = Aux + Zorn:;
lemma Zorn's_Lemma: "a:S ==> (!!c. c: chain S ==> EX x. x:c ==> Union c : S) ==>
@@ -15,12 +19,12 @@
show "EX y:S. ALL z:c. z <= y";
proof (rule case [of "c={}"]);
assume "c={}";
- show ?thesis; by fast;
+ show ?thesis; by (fast!);
next;
assume "c~={}";
show ?thesis;
proof;
- have "EX x. x:c"; by fast;
+ have "EX x. x:c"; by (fast!);
thus "Union c : S"; by (rule s);
show "ALL z:c. z <= Union c"; by fast;
qed;