# HG changeset patch # User wenzelm # Date 964955029 -7200 # Node ID b24516d96847a8cec8c4de3b29d44802a0c033c1 # Parent b0ce3b7c9c26f6e943732ed2c47cf5efd41521d2 adapted obtain; tuned; diff -r b0ce3b7c9c26 -r b24516d96847 src/HOL/Isar_examples/MutilatedCheckerboard.thy --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Sun Jul 30 13:02:56 2000 +0200 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Sun Jul 30 13:03:49 2000 +0200 @@ -35,21 +35,19 @@ proof; assume "t : tiling A" (is "_ : ?T"); thus "u : ?T --> t Int u = {} --> t Un u : ?T" (is "?P t"); - proof induct; - show "?P {}"; by simp; - + proof (induct (stripped) t); + assume "u : ?T" "{} Int u = {}" + thus "{} Un u : ?T" by simp; + next fix a t; assume "a : A" "t : ?T" "?P t" "a <= - t"; - show "?P (a Un t)"; - proof (intro impI); - assume "u : ?T" "(a Un t) Int u = {}"; - have hyp: "t Un u: ?T"; by (blast!); - have "a <= - (t Un u)"; by (blast!); - with _ hyp; have "a Un (t Un u) : ?T"; by (rule tiling.Un); - also; have "a Un (t Un u) = (a Un t) Un u"; - by (simp only: Un_assoc); - finally; show "... : ?T"; .; - qed; + assume "u : ?T" "(a Un t) Int u = {}"; + have hyp: "t Un u: ?T"; by (blast!); + have "a <= - (t Un u)"; by (blast!); + with _ hyp; have "a Un (t Un u) : ?T"; by (rule tiling.Un); + also; have "a Un (t Un u) = (a Un t) Un u"; + by (simp only: Un_assoc); + finally; show "... : ?T"; .; qed; qed; @@ -139,7 +137,7 @@ also; have "{(i, 2 * n), (i, 2 * n + 1)} = ?a"; by blast; finally; show "... : domino"; .; from hyp; show "?B n : ?T"; .; - show "?a <= - ?B n"; by force; + show "?a <= - ?B n"; by blast; qed; finally; show "?P (Suc n)"; .; qed; @@ -220,21 +218,21 @@ "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"; proof -; fix b; assume "b < 2"; - have "EX i j. ?e a b = {(i, j)}"; by (rule domino_singleton); - thus "?thesis b"; - proof (elim exE); - have "?e (a Un t) b = ?e a b Un ?e t b"; by (rule evnodd_Un); - also; fix i j; assume "?e a b = {(i, j)}"; - also; have "... Un ?e t b = insert (i, j) (?e t b)"; by simp; - also; have "card ... = Suc (card (?e t b))"; - proof (rule card_insert_disjoint); - show "finite (?e t b)"; - by (rule evnodd_finite, rule tiling_domino_finite); - have "(i, j) : ?e a b"; by (simp!); - thus "(i, j) ~: ?e t b"; by (force! dest: evnoddD); - qed; - finally; show ?thesis; .; + have "?e (a Un t) b = ?e a b Un ?e t b"; by (rule evnodd_Un); + also; obtain i j where "?e a b = {(i, j)}"; + proof -; + have "EX i j. ?e a b = {(i, j)}"; by (rule domino_singleton); + thus ?thesis; by blast; qed; + also; have "... Un ?e t b = insert (i, j) (?e t b)"; by simp; + also; have "card ... = Suc (card (?e t b))"; + proof (rule card_insert_disjoint); + show "finite (?e t b)"; + by (rule evnodd_finite, rule tiling_domino_finite); + have "(i, j) : ?e a b"; by (simp!); + thus "(i, j) ~: ?e t b"; by (blast! dest: evnoddD); + qed; + finally; show "?thesis b"; .; qed; hence "card (?e (a Un t) 0) = Suc (card (?e t 0))"; by simp; also; from hyp; have "card (?e t 0) = card (?e t 1)"; .; @@ -276,7 +274,7 @@ < card (?e ?t' 0)"; proof (rule card_Diff1_less); from _ fin; show "finite (?e ?t' 0)"; - by (rule finite_subset) force; + by (rule finite_subset) auto; show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0"; by simp; qed; thus ?thesis; by simp; diff -r b0ce3b7c9c26 -r b24516d96847 src/HOL/Isar_examples/W_correct.thy --- a/src/HOL/Isar_examples/W_correct.thy Sun Jul 30 13:02:56 2000 +0200 +++ b/src/HOL/Isar_examples/W_correct.thy Sun Jul 30 13:03:49 2000 +0200 @@ -62,7 +62,8 @@ by (simp add: app_subst_list); hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"; by (rule has_type.Abs); - thus "?P a (Abs e) (t1 -> t2)"; by (simp add: app_subst_list); + thus "?P a (Abs e) (t1 -> t2)"; + by (simp add: app_subst_list); next; case App; thus "?P a (App e1 e2) t1"; by simp; @@ -77,15 +78,15 @@ primrec "W (Var i) a n = - (if i < length a then Ok (id_subst, a ! i, n) else Fail)" + (if i < length a then Ok (id_subst, a ! i, n) else Fail)" "W (Abs e) a n = - ((s, t, m) := W e (TVar n # a) (Suc n); - Ok (s, (s n) -> t, m))" + ((s, t, m) := W e (TVar n # a) (Suc n); + Ok (s, (s n) -> t, m))" "W (App e1 e2) a n = - ((s1, t1, m1) := W e1 a n; - (s2, t2, m2) := W e2 ($s1 a) m1; - u := mgu ($ s2 t1) (t2 -> TVar m2); - Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))"; + ((s1, t1, m1) := W e1 a n; + (s2, t2, m2) := W e2 ($s1 a) m1; + u := mgu ($ s2 t1) (t2 -> TVar m2); + Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))"; subsection {* Correctness theorem *}; @@ -95,56 +96,52 @@ assume W_ok: "W e a n = Ok (s, t, m)"; have "ALL a s t m n. Ok (s, t, m) = W e a n --> $ s a |- e :: t" (is "?P e"); - proof (induct e); - fix i; show "?P (Var i)"; by simp; - next; - fix e; assume hyp: "?P e"; - show "?P (Abs e)"; - proof (intro allI impI); - fix a s t m n; + proof (induct (stripped) e); + fix a s t m n; + { + fix i; + assume "Ok (s, t, m) = W (Var i) a n"; + thus "$ s a |- Var i :: t"; by (simp split: if_splits); + next; + fix e; assume hyp: "?P e"; assume "Ok (s, t, m) = W (Abs e) a n"; - thus "$ s a |- Abs e :: t"; - obtain t' where "t = s n -> t'" "Ok (s, t', m) = W e (TVar n # a) (Suc n)"; - by (rule rev_mp) (simp split: split_bind); - with hyp; show ?thesis; by (force intro: has_type.Abs); - qed; - qed; - next; - fix e1 e2; assume hyp1: "?P e1" and hyp2: "?P e2"; - show "?P (App e1 e2)"; - proof (intro allI impI); - fix a s t m n; assume "Ok (s, t, m) = W (App e1 e2) a n"; - thus "$ s a |- App e1 e2 :: t"; - obtain s1 t1 n1 s2 t2 n2 u where + then; obtain t' where "t = s n -> t'" + and "Ok (s, t', m) = W e (TVar n # a) (Suc n)"; + by (auto split: bind_splits); + with hyp; show "$ s a |- Abs e :: t"; + by (force intro: has_type.Abs); + next; + fix e1 e2; assume hyp1: "?P e1" and hyp2: "?P e2"; + assume "Ok (s, t, m) = W (App e1 e2) a n"; + then; obtain s1 t1 n1 s2 t2 n2 u where s: "s = $ u o $ s2 o s1" and t: "t = u n2" and mgu_ok: "mgu ($ s2 t1) (t2 -> TVar n2) = Ok u" and W1_ok: "W e1 a n = Ok (s1, t1, n1)" and W2_ok: "W e2 ($ s1 a) n1 = Ok (s2, t2, n2)"; - by (rule rev_mp) (simp split: split_bind); - show ?thesis; - proof (rule has_type.App); - from s; have s': "$ u ($ s2 ($ s1 a)) = $s a"; - by (simp add: subst_comp_tel o_def); - show "$s a |- e1 :: $ u t2 -> t"; - proof -; - from hyp1 W1_ok [RS sym]; have "$ s1 a |- e1 :: t1"; - by blast; - hence "$ u ($ s2 ($ s1 a)) |- e1 :: $ u ($ s2 t1)"; - by (intro has_type_subst_closed); - with s' t mgu_ok; show ?thesis; by simp; - qed; - show "$ s a |- e2 :: $ u t2"; - proof -; - from hyp2 W2_ok [RS sym]; - have "$ s2 ($ s1 a) |- e2 :: t2"; by blast; - hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2"; - by (rule has_type_subst_closed); - with s'; show ?thesis; by simp; - qed; + by (auto split: bind_splits); + show "$ s a |- App e1 e2 :: t"; + proof (rule has_type.App); + from s; have s': "$ u ($ s2 ($ s1 a)) = $s a"; + by (simp add: subst_comp_tel o_def); + show "$s a |- e1 :: $ u t2 -> t"; + proof -; + from hyp1 W1_ok [RS sym]; have "$ s1 a |- e1 :: t1"; + by blast; + hence "$ u ($ s2 ($ s1 a)) |- e1 :: $ u ($ s2 t1)"; + by (intro has_type_subst_closed); + with s' t mgu_ok; show ?thesis; by simp; + qed; + show "$ s a |- e2 :: $ u t2"; + proof -; + from hyp2 W2_ok [RS sym]; + have "$ s2 ($ s1 a) |- e2 :: t2"; by blast; + hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2"; + by (rule has_type_subst_closed); + with s'; show ?thesis; by simp; qed; qed; - qed; + }; qed; with W_ok [RS sym]; show ?thesis; by blast; qed; diff -r b0ce3b7c9c26 -r b24516d96847 src/HOL/Real/HahnBanach/HahnBanach.thy --- a/src/HOL/Real/HahnBanach/HahnBanach.thy Sun Jul 30 13:02:56 2000 +0200 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Sun Jul 30 13:03:49 2000 +0200 @@ -126,189 +126,185 @@ proof fix g assume "g \\ M" "\\x \\ M. g \\ x --> g = x" -- {* We consider such a maximal element $g \in M$. \skp *} - show ?thesis - obtain H h where "graph H h = g" "is_linearform H h" - "is_subspace H E" "is_subspace F H" "graph F f \\ graph H h" - "\\x \\ H. h x <= p x" - -- {* $g$ is a norm-preserving extension of $f$, in other words: *} - -- {* $g$ is the graph of some linear form $h$ defined on a subspace $H$ of $E$, *} - -- {* and $h$ is an extension of $f$ that is again bounded by $p$. \skp *} + obtain H h where "graph H h = g" "is_linearform H h" + "is_subspace H E" "is_subspace F H" "graph F f \\ graph H h" + "\\x \\ H. h x <= p x" + -- {* $g$ is a norm-preserving extension of $f$, in other words: *} + -- {* $g$ is the graph of some linear form $h$ defined on a subspace $H$ of $E$, *} + -- {* and $h$ is an extension of $f$ that is again bounded by $p$. \skp *} + proof - + have "\\H h. graph H h = g \\ is_linearform H h + \\ is_subspace H E \\ is_subspace F H + \\ graph F f \\ graph H h + \\ (\\x \\ H. h x <= p x)" + by (simp! add: norm_pres_extension_D) + thus ?thesis by (elim exE conjE) rule + qed + have h: "is_vectorspace H" .. + have "H = E" + -- {* We show that $h$ is defined on whole $E$ by classical contradiction. \skp *} + proof (rule classical) + assume "H \\ E" + -- {* Assume $h$ is not defined on whole $E$. Then show that $h$ can be extended *} + -- {* in a norm-preserving way to a function $h'$ with the graph $g'$. \skp *} + have "\\g' \\ M. g \\ g' \\ g \\ g'" proof - - have "\\H h. graph H h = g \\ is_linearform H h - \\ is_subspace H E \\ is_subspace F H - \\ graph F f \\ graph H h - \\ (\\x \\ H. h x <= p x)" - by (simp! add: norm_pres_extension_D) - thus ?thesis by (elim exE conjE) rule - qed - have h: "is_vectorspace H" .. - have "H = E" - -- {* We show that $h$ is defined on whole $E$ by classical contradiction. \skp *} - proof (rule classical) - assume "H \\ E" - -- {* Assume $h$ is not defined on whole $E$. Then show that $h$ can be extended *} - -- {* in a norm-preserving way to a function $h'$ with the graph $g'$. \skp *} - have "\\g' \\ M. g \\ g' \\ g \\ g'" - obtain x' where "x' \\ E" "x' \\ H" - -- {* Pick $x' \in E \setminus H$. \skp *} - proof - - have "\\x' \\ E. x' \\ H" - proof (rule set_less_imp_diff_not_empty) - have "H \\ E" .. - thus "H \\ E" .. - qed - thus ?thesis by blast + obtain x' where "x' \\ E" "x' \\ H" + -- {* Pick $x' \in E \setminus H$. \skp *} + proof - + have "\\x' \\ E. x' \\ H" + proof (rule set_less_imp_diff_not_empty) + have "H \\ E" .. + thus "H \\ E" .. qed - have x': "x' \\ 0" - proof (rule classical) - presume "x' = 0" - with h have "x' \\ H" by simp - thus ?thesis by contradiction - qed blast - def H' == "H + lin x'" - -- {* Define $H'$ as the direct sum of $H$ and the linear closure of $x'$. \skp *} - show ?thesis - obtain xi where "\\y \\ H. - p (y + x') - h y <= xi - \\ xi <= p (y + x') - h y" - -- {* Pick a real number $\xi$ that fulfills certain inequations; this will *} - -- {* be used to establish that $h'$ is a norm-preserving extension of $h$. - \label{ex-xi-use}\skp *} + thus ?thesis by blast + qed + have x': "x' \\ 0" + proof (rule classical) + presume "x' = 0" + with h have "x' \\ H" by simp + thus ?thesis by contradiction + qed blast + def H' == "H + lin x'" + -- {* Define $H'$ as the direct sum of $H$ and the linear closure of $x'$. \skp *} + obtain xi where "\\y \\ H. - p (y + x') - h y <= xi + \\ xi <= p (y + x') - h y" + -- {* Pick a real number $\xi$ that fulfills certain inequations; this will *} + -- {* be used to establish that $h'$ is a norm-preserving extension of $h$. + \label{ex-xi-use}\skp *} + proof - + from h have "\\xi. \\y \\ H. - p (y + x') - h y <= xi + \\ xi <= p (y + x') - h y" + proof (rule ex_xi) + fix u v assume "u \\ H" "v \\ H" + from h have "h v - h u = h (v - u)" + by (simp! add: linearform_diff) + also have "... <= p (v - u)" + by (simp!) + also have "v - u = x' + - x' + v + - u" + by (simp! add: diff_eq1) + also have "... = v + x' + - (u + x')" + by (simp!) + also have "... = (v + x') - (u + x')" + by (simp! add: diff_eq1) + also have "p ... <= p (v + x') + p (u + x')" + by (rule seminorm_diff_subadditive) (simp_all!) + finally have "h v - h u <= p (v + x') + p (u + x')" . + thus "- p (u + x') - h u <= p (v + x') - h v" + by (rule real_diff_ineq_swap) + qed + thus ?thesis by rule rule + qed + + def h' == "\\x. let (y,a) = SOME (y,a). x = y + a \\ x' \\ y \\ H + in (h y) + a * xi" + -- {* Define the extension $h'$ of $h$ to $H'$ using $\xi$. \skp *} + show ?thesis + proof + show "g \\ graph H' h' \\ g \\ graph H' h'" + -- {* Show that $h'$ is an extension of $h$ \dots \skp *} + proof + show "g \\ graph H' h'" proof - - from h have "\\xi. \\y \\ H. - p (y + x') - h y <= xi - \\ xi <= p (y + x') - h y" - proof (rule ex_xi) - fix u v assume "u \\ H" "v \\ H" - from h have "h v - h u = h (v - u)" - by (simp! add: linearform_diff) - also have "... <= p (v - u)" - by (simp!) - also have "v - u = x' + - x' + v + - u" - by (simp! add: diff_eq1) - also have "... = v + x' + - (u + x')" - by (simp!) - also have "... = (v + x') - (u + x')" - by (simp! add: diff_eq1) - also have "p ... <= p (v + x') + p (u + x')" - by (rule seminorm_diff_subadditive) (simp!)+ - finally have "h v - h u <= p (v + x') + p (u + x')" . - - thus "- p (u + x') - h u <= p (v + x') - h v" - by (rule real_diff_ineq_swap) - qed - thus ?thesis by rule rule + have "graph H h \\ graph H' h'" + proof (rule graph_extI) + fix t assume "t \\ H" + have "(SOME (y, a). t = y + a \\ x' \\ y \\ H) + = (t, #0)" + by (rule decomp_H'_H) (assumption+, rule x') + thus "h t = h' t" by (simp! add: Let_def) + next + show "H \\ H'" + proof (rule subspace_subset) + show "is_subspace H H'" + proof (unfold H'_def, rule subspace_vs_sum1) + show "is_vectorspace H" .. + show "is_vectorspace (lin x')" .. + qed + qed + qed + thus ?thesis by (simp!) qed - - def h' == "\\x. let (y,a) = SOME (y,a). x = y + a \\ x' \\ y \\ H - in (h y) + a * xi" - -- {* Define the extension $h'$ of $h$ to $H'$ using $\xi$. \skp *} - show ?thesis - proof - show "g \\ graph H' h' \\ g \\ graph H' h'" - -- {* Show that $h'$ is an extension of $h$ \dots \skp *} + show "g \\ graph H' h'" + proof - + have "graph H h \\ graph H' h'" proof - show "g \\ graph H' h'" - proof - - have "graph H h \\ graph H' h'" - proof (rule graph_extI) - fix t assume "t \\ H" - have "(SOME (y, a). t = y + a \\ x' \\ y \\ H) - = (t, #0)" - by (rule decomp_H'_H) (assumption+, rule x') - thus "h t = h' t" by (simp! add: Let_def) - next - show "H \\ H'" - proof (rule subspace_subset) - show "is_subspace H H'" - proof (unfold H'_def, rule subspace_vs_sum1) - show "is_vectorspace H" .. - show "is_vectorspace (lin x')" .. - qed - qed - qed - thus ?thesis by (simp!) - qed - show "g \\ graph H' h'" - proof - - have "graph H h \\ graph H' h'" - proof - assume e: "graph H h = graph H' h'" - have "x' \\ H'" - proof (unfold H'_def, rule vs_sumI) - show "x' = 0 + x'" by (simp!) - from h show "0 \\ H" .. - show "x' \\ lin x'" by (rule x_lin_x) - qed - hence "(x', h' x') \\ graph H' h'" .. - with e have "(x', h' x') \\ graph H h" by simp - hence "x' \\ H" .. - thus False by contradiction - qed - thus ?thesis by (simp!) - qed + assume e: "graph H h = graph H' h'" + have "x' \\ H'" + proof (unfold H'_def, rule vs_sumI) + show "x' = 0 + x'" by (simp!) + from h show "0 \\ H" .. + show "x' \\ lin x'" by (rule x_lin_x) + qed + hence "(x', h' x') \\ graph H' h'" .. + with e have "(x', h' x') \\ graph H h" by simp + hence "x' \\ H" .. + thus False by contradiction qed - show "graph H' h' \\ M" - -- {* and $h'$ is norm-preserving. \skp *} - proof - - have "graph H' h' \\ norm_pres_extensions E p F f" - proof (rule norm_pres_extensionI2) - show "is_linearform H' h'" - by (rule h'_lf) (simp! add: x')+ - show "is_subspace H' E" - by (unfold H'_def) - (rule vs_sum_subspace [OF _ lin_subspace]) - have "is_subspace F H" . - also from h lin_vs - have [fold H'_def]: "is_subspace H (H + lin x')" .. - finally (subspace_trans [OF _ h]) - show f_h': "is_subspace F H'" . - - show "graph F f \\ graph H' h'" - proof (rule graph_extI) - fix x assume "x \\ F" - have "f x = h x" .. - also have " ... = h x + #0 * xi" by simp - also - have "... = (let (y,a) = (x, #0) in h y + a * xi)" - by (simp add: Let_def) - also have - "(x, #0) = (SOME (y, a). x = y + a \\ x' \\ y \\ H)" - by (rule decomp_H'_H [RS sym]) (simp! add: x')+ - also have - "(let (y,a) = (SOME (y,a). x = y + a \\ x' \\ y \\ H) - in h y + a * xi) = h' x" by (simp!) - finally show "f x = h' x" . - next - from f_h' show "F \\ H'" .. - qed - - show "\\x \\ H'. h' x <= p x" - by (rule h'_norm_pres) (assumption+, rule x') - qed - thus "graph H' h' \\ M" by (simp!) - qed + thus ?thesis by (simp!) qed qed + show "graph H' h' \\ M" + -- {* and $h'$ is norm-preserving. \skp *} + proof - + have "graph H' h' \\ norm_pres_extensions E p F f" + proof (rule norm_pres_extensionI2) + show "is_linearform H' h'" + by (rule h'_lf) (simp! add: x')+ + show "is_subspace H' E" + by (unfold H'_def) + (rule vs_sum_subspace [OF _ lin_subspace]) + have "is_subspace F H" . + also from h lin_vs + have [fold H'_def]: "is_subspace H (H + lin x')" .. + finally (subspace_trans [OF _ h]) + show f_h': "is_subspace F H'" . + + show "graph F f \\ graph H' h'" + proof (rule graph_extI) + fix x assume "x \\ F" + have "f x = h x" .. + also have " ... = h x + #0 * xi" by simp + also + have "... = (let (y,a) = (x, #0) in h y + a * xi)" + by (simp add: Let_def) + also have + "(x, #0) = (SOME (y, a). x = y + a \\ x' \\ y \\ H)" + by (rule decomp_H'_H [RS sym]) (simp! add: x')+ + also have + "(let (y,a) = (SOME (y,a). x = y + a \\ x' \\ y \\ H) + in h y + a * xi) = h' x" by (simp!) + finally show "f x = h' x" . + next + from f_h' show "F \\ H'" .. + qed + + show "\\x \\ H'. h' x <= p x" + by (rule h'_norm_pres) (assumption+, rule x') + qed + thus "graph H' h' \\ M" by (simp!) + qed qed - hence "\\ (\\x \\ M. g \\ x --> g = x)" by simp - -- {* So the graph $g$ of $h$ cannot be maximal. Contradiction! \skp *} - thus "H = E" by contradiction qed - thus "\\h. is_linearform E h \\ (\\x \\ F. h x = f x) - \\ (\\x \\ E. h x <= p x)" - proof (intro exI conjI) - assume eq: "H = E" - from eq show "is_linearform E h" by (simp!) - show "\\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 "\\x \\ E. h x <= p x" by (force!) + hence "\\ (\\x \\ M. g \\ x --> g = x)" by simp + -- {* So the graph $g$ of $h$ cannot be maximal. Contradiction! \skp *} + thus "H = E" by contradiction + qed + thus "\\h. is_linearform E h \\ (\\x \\ F. h x = f x) + \\ (\\x \\ E. h x <= p x)" + proof (intro exI conjI) + assume eq: "H = E" + from eq show "is_linearform E h" by (simp!) + show "\\x \\ F. h x = f x" + proof + fix x assume "x \\ F" have "f x = h x " .. + thus "h x = f x" .. qed + from eq show "\\x \\ E. h x <= p x" by (force!) qed qed -qed - +qed subsection {* Alternative formulation *} @@ -325,25 +321,25 @@ *} theorem abs_HahnBanach: - "[| is_vectorspace E; is_subspace F E; is_linearform F f; - is_seminorm E p; \\x \\ F. |f x| <= p x |] - ==> \\g. is_linearform E g \\ (\\x \\ F. g x = f x) - \\ (\\x \\ E. |g x| <= p x)" +"[| is_vectorspace E; is_subspace F E; is_linearform F f; +is_seminorm E p; \\x \\ F. |f x| <= p x |] +==> \\g. is_linearform E g \\ (\\x \\ F. g x = f x) + \\ (\\x \\ E. |g x| <= p x)" proof - - assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" - "is_linearform F f" "\\x \\ F. |f x| <= p x" - have "\\x \\ F. f x <= p x" by (rule abs_ineq_iff [RS iffD1]) - hence "\\g. is_linearform E g \\ (\\x \\ F. g x = f x) - \\ (\\x \\ E. g x <= p x)" - by (simp! only: HahnBanach) - thus ?thesis - proof (elim exE conjE) - fix g assume "is_linearform E g" "\\x \\ F. g x = f x" - "\\x \\ E. g x <= p x" - hence "\\x \\ E. |g x| <= p x" - by (simp! add: abs_ineq_iff [OF subspace_refl]) - thus ?thesis by (intro exI conjI) - qed +assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" +"is_linearform F f" "\\x \\ F. |f x| <= p x" +have "\\x \\ F. f x <= p x" by (rule abs_ineq_iff [RS iffD1]) +hence "\\g. is_linearform E g \\ (\\x \\ F. g x = f x) + \\ (\\x \\ E. g x <= p x)" +by (simp! only: HahnBanach) +thus ?thesis +proof (elim exE conjE) +fix g assume "is_linearform E g" "\\x \\ F. g x = f x" + "\\x \\ E. g x <= p x" +hence "\\x \\ E. |g x| <= p x" + by (simp! add: abs_ineq_iff [OF subspace_refl]) +thus ?thesis by (intro exI conjI) +qed qed subsection {* The Hahn-Banach Theorem for normed spaces *} @@ -353,169 +349,169 @@ $E$ such that $\fnorm{f} = \fnorm {g}$. *} theorem norm_HahnBanach: - "[| is_normed_vectorspace E norm; is_subspace F E; - is_linearform F f; is_continuous F norm f |] - ==> \\g. is_linearform E g - \\ is_continuous E norm g - \\ (\\x \\ F. g x = f x) - \\ \\g\\E,norm = \\f\\F,norm" +"[| is_normed_vectorspace E norm; is_subspace F E; +is_linearform F f; is_continuous F norm f |] +==> \\g. is_linearform E g + \\ is_continuous E norm g + \\ (\\x \\ F. g x = f x) + \\ \\g\\E,norm = \\f\\F,norm" proof - - assume e_norm: "is_normed_vectorspace E norm" - assume f: "is_subspace F E" "is_linearform F f" - assume f_cont: "is_continuous F norm f" - have e: "is_vectorspace E" .. - hence f_norm: "is_normed_vectorspace F norm" .. +assume e_norm: "is_normed_vectorspace E norm" +assume f: "is_subspace F E" "is_linearform F f" +assume f_cont: "is_continuous F norm f" +have e: "is_vectorspace E" .. +hence f_norm: "is_normed_vectorspace F norm" .. + +txt{* We define a function $p$ on $E$ as follows: +\begin{matharray}{l} +p \: x = \fnorm f \cdot \norm x\\ +\end{matharray} +*} + +def p == "\\x. \\f\\F,norm * norm x" + +txt{* $p$ is a seminorm on $E$: *} + +have q: "is_seminorm E p" +proof +fix x y a assume "x \\ E" "y \\ E" + +txt{* $p$ is positive definite: *} - txt{* We define a function $p$ on $E$ as follows: - \begin{matharray}{l} - p \: x = \fnorm f \cdot \norm x\\ - \end{matharray} - *} +show "#0 <= p x" +proof (unfold p_def, rule real_le_mult_order1a) + from f_cont f_norm show "#0 <= \\f\\F,norm" .. + show "#0 <= norm x" .. +qed + +txt{* $p$ is absolutely homogenous: *} - def p == "\\x. \\f\\F,norm * norm x" - - txt{* $p$ is a seminorm on $E$: *} +show "p (a \\ x) = |a| * p x" +proof - + have "p (a \\ x) = \\f\\F,norm * norm (a \\ x)" + by (simp!) + also have "norm (a \\ x) = |a| * norm x" + by (rule normed_vs_norm_abs_homogenous) + also have "\\f\\F,norm * ( |a| * norm x ) + = |a| * (\\f\\F,norm * norm x)" + by (simp! only: real_mult_left_commute) + also have "... = |a| * p x" by (simp!) + finally show ?thesis . +qed + +txt{* Furthermore, $p$ is subadditive: *} - have q: "is_seminorm E p" - proof - fix x y a assume "x \\ E" "y \\ E" - - txt{* $p$ is positive definite: *} +show "p (x + y) <= p x + p y" +proof - + have "p (x + y) = \\f\\F,norm * norm (x + y)" + by (simp!) + also + have "... <= \\f\\F,norm * (norm x + norm y)" + proof (rule real_mult_le_le_mono1a) + from f_cont f_norm show "#0 <= \\f\\F,norm" .. + show "norm (x + y) <= norm x + norm y" .. + qed + also have "... = \\f\\F,norm * norm x + + \\f\\F,norm * norm y" + by (simp! only: real_add_mult_distrib2) + finally show ?thesis by (simp!) +qed +qed - show "#0 <= p x" - proof (unfold p_def, rule real_le_mult_order1a) - from f_cont f_norm show "#0 <= \\f\\F,norm" .. - show "#0 <= norm x" .. - qed +txt{* $f$ is bounded by $p$. *} + +have "\\x \\ F. |f x| <= p x" +proof +fix x assume "x \\ F" + from f_norm show "|f x| <= p x" + by (simp! add: norm_fx_le_norm_f_norm_x) +qed + +txt{* Using the fact that $p$ is a seminorm and +$f$ is bounded by $p$ we can apply the Hahn-Banach Theorem +for real vector spaces. +So $f$ can be extended in a norm-preserving way to some function +$g$ on the whole vector space $E$. *} + +with e f q +have "\\g. is_linearform E g \\ (\\x \\ F. g x = f x) + \\ (\\x \\ E. |g x| <= p x)" +by (simp! add: abs_HahnBanach) - txt{* $p$ is absolutely homogenous: *} +thus ?thesis +proof (elim exE conjE) +fix g +assume "is_linearform E g" and a: "\\x \\ F. g x = f x" + and b: "\\x \\ E. |g x| <= p x" + +show "\\g. is_linearform E g + \\ is_continuous E norm g + \\ (\\x \\ F. g x = f x) + \\ \\g\\E,norm = \\f\\F,norm" +proof (intro exI conjI) + +txt{* We furthermore have to show that +$g$ is also continuous: *} + + show g_cont: "is_continuous E norm g" + proof + fix x assume "x \\ E" + with b show "|g x| <= \\f\\F,norm * norm x" + by (simp add: p_def) + qed - show "p (a \\ x) = |a| * p x" - proof - - have "p (a \\ x) = \\f\\F,norm * norm (a \\ x)" + txt {* To complete the proof, we show that + $\fnorm g = \fnorm f$. \label{order_antisym} *} + + show "\\g\\E,norm = \\f\\F,norm" + (is "?L = ?R") + proof (rule order_antisym) + + txt{* First we show $\fnorm g \leq \fnorm f$. The function norm + $\fnorm g$ is defined as the smallest $c\in\bbbR$ such that + \begin{matharray}{l} + \All {x\in E} {|g\ap x| \leq c \cdot \norm x} + \end{matharray} + Furthermore holds + \begin{matharray}{l} + \All {x\in E} {|g\ap x| \leq \fnorm f \cdot \norm x} + \end{matharray} + *} + + have "\\x \\ E. |g x| <= \\f\\F,norm * norm x" + proof + fix x assume "x \\ E" + show "|g x| <= \\f\\F,norm * norm x" by (simp!) - also have "norm (a \\ x) = |a| * norm x" - by (rule normed_vs_norm_abs_homogenous) - also have "\\f\\F,norm * ( |a| * norm x ) - = |a| * (\\f\\F,norm * norm x)" - by (simp! only: real_mult_left_commute) - also have "... = |a| * p x" by (simp!) - finally show ?thesis . qed - txt{* Furthermore, $p$ is subadditive: *} - - show "p (x + y) <= p x + p y" - proof - - have "p (x + y) = \\f\\F,norm * norm (x + y)" - by (simp!) - also - have "... <= \\f\\F,norm * (norm x + norm y)" - proof (rule real_mult_le_le_mono1a) - from f_cont f_norm show "#0 <= \\f\\F,norm" .. - show "norm (x + y) <= norm x + norm y" .. - qed - also have "... = \\f\\F,norm * norm x - + \\f\\F,norm * norm y" - by (simp! only: real_add_mult_distrib2) - finally show ?thesis by (simp!) + with g_cont e_norm show "?L <= ?R" + proof (rule fnorm_le_ub) + from f_cont f_norm show "#0 <= \\f\\F,norm" .. qed - qed - - txt{* $f$ is bounded by $p$. *} - have "\\x \\ F. |f x| <= p x" - proof - fix x assume "x \\ F" - from f_norm show "|f x| <= p x" - by (simp! add: norm_fx_le_norm_f_norm_x) - qed - - txt{* Using the fact that $p$ is a seminorm and - $f$ is bounded by $p$ we can apply the Hahn-Banach Theorem - for real vector spaces. - So $f$ can be extended in a norm-preserving way to some function - $g$ on the whole vector space $E$. *} - - with e f q - have "\\g. is_linearform E g \\ (\\x \\ F. g x = f x) - \\ (\\x \\ E. |g x| <= p x)" - by (simp! add: abs_HahnBanach) - - thus ?thesis - proof (elim exE conjE) - fix g - assume "is_linearform E g" and a: "\\x \\ F. g x = f x" - and b: "\\x \\ E. |g x| <= p x" - - show "\\g. is_linearform E g - \\ is_continuous E norm g - \\ (\\x \\ F. g x = f x) - \\ \\g\\E,norm = \\f\\F,norm" - proof (intro exI conjI) - - txt{* We furthermore have to show that - $g$ is also continuous: *} + txt{* The other direction is achieved by a similar + argument. *} - show g_cont: "is_continuous E norm g" - proof - fix x assume "x \\ E" - with b show "|g x| <= \\f\\F,norm * norm x" - by (simp add: p_def) - qed - - txt {* To complete the proof, we show that - $\fnorm g = \fnorm f$. \label{order_antisym} *} - - show "\\g\\E,norm = \\f\\F,norm" - (is "?L = ?R") - proof (rule order_antisym) - - txt{* First we show $\fnorm g \leq \fnorm f$. The function norm - $\fnorm g$ is defined as the smallest $c\in\bbbR$ such that - \begin{matharray}{l} - \All {x\in E} {|g\ap x| \leq c \cdot \norm x} - \end{matharray} - Furthermore holds - \begin{matharray}{l} - \All {x\in E} {|g\ap x| \leq \fnorm f \cdot \norm x} - \end{matharray} - *} - - have "\\x \\ E. |g x| <= \\f\\F,norm * norm x" - proof - fix x assume "x \\ E" - show "|g x| <= \\f\\F,norm * norm x" - by (simp!) - qed - - with g_cont e_norm show "?L <= ?R" - proof (rule fnorm_le_ub) - from f_cont f_norm show "#0 <= \\f\\F,norm" .. - qed - - txt{* The other direction is achieved by a similar - argument. *} - - have "\\x \\ F. |f x| <= \\g\\E,norm * norm x" - proof - fix x assume "x \\ F" - from a have "g x = f x" .. - hence "|f x| = |g x|" by simp - also from g_cont - have "... <= \\g\\E,norm * norm x" - proof (rule norm_fx_le_norm_f_norm_x) - show "x \\ E" .. - qed - finally show "|f x| <= \\g\\E,norm * norm x" . - qed - thus "?R <= ?L" - proof (rule fnorm_le_ub [OF f_cont f_norm]) - from g_cont show "#0 <= \\g\\E,norm" .. - qed + have "\\x \\ F. |f x| <= \\g\\E,norm * norm x" + proof + fix x assume "x \\ F" + from a have "g x = f x" .. + hence "|f x| = |g x|" by simp + also from g_cont + have "... <= \\g\\E,norm * norm x" + proof (rule norm_fx_le_norm_f_norm_x) + show "x \\ E" .. qed + finally show "|f x| <= \\g\\E,norm * norm x" . + qed + thus "?R <= ?L" + proof (rule fnorm_le_ub [OF f_cont f_norm]) + from g_cont show "#0 <= \\g\\E,norm" .. qed qed qed +qed +qed -end \ No newline at end of file +end