# HG changeset patch # User wenzelm # Date 937927880 -7200 # Node ID c5a3f980a7afae8b0a2a0eabdcdf48609af57c8d # Parent bfa85f42962947cf936096c1586466136b5c4e7d accomodate refined facts handling; diff -r bfa85f429629 -r c5a3f980a7af src/HOL/Real/HahnBanach/Aux.thy --- 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; diff -r bfa85f429629 -r c5a3f980a7af src/HOL/Real/HahnBanach/Bounds.thy --- 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); diff -r bfa85f429629 -r c5a3f980a7af src/HOL/Real/HahnBanach/FunctionNorm.thy --- 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; diff -r bfa85f429629 -r c5a3f980a7af src/HOL/Real/HahnBanach/FunctionOrder.thy --- 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 diff -r bfa85f429629 -r c5a3f980a7af src/HOL/Real/HahnBanach/HahnBanach.thy --- 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; + diff -r bfa85f429629 -r c5a3f980a7af src/HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy --- 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; diff -r bfa85f429629 -r c5a3f980a7af src/HOL/Real/HahnBanach/HahnBanach_lemmas.thy --- 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; diff -r bfa85f429629 -r c5a3f980a7af src/HOL/Real/HahnBanach/LinearSpace.thy --- 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 diff -r bfa85f429629 -r c5a3f980a7af src/HOL/Real/HahnBanach/Linearform.thy --- 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; diff -r bfa85f429629 -r c5a3f980a7af src/HOL/Real/HahnBanach/NormedSpace.thy --- 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; - diff -r bfa85f429629 -r c5a3f980a7af src/HOL/Real/HahnBanach/Subspace.thy --- 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; diff -r bfa85f429629 -r c5a3f980a7af src/HOL/Real/HahnBanach/Zorn_Lemma.thy --- 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;