# 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 \\<in> M" "\\<forall>x \\<in> M. g \\<subseteq> 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 \\<subseteq> graph H h" 
-        "\\<forall>x \\<in> 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 \\<subseteq> graph H h" 
+      "\\<forall>x \\<in> 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 "\\<exists>H h. graph H h = g \\<and> is_linearform H h 
+        \\<and> is_subspace H E \\<and> is_subspace F H
+        \\<and> graph F f \\<subseteq> graph H h
+        \\<and> (\\<forall>x \\<in> H. h x <= p x)" 
+        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 \\<noteq> 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 "\\<exists>g' \\<in> M. g \\<subseteq> g' \\<and> g \\<noteq> g'"
       proof -
-        have "\\<exists>H h. graph H h = g \\<and> is_linearform H h 
-          \\<and> is_subspace H E \\<and> is_subspace F H
-          \\<and> graph F f \\<subseteq> graph H h
-          \\<and> (\\<forall>x \\<in> H. h x <= p x)" 
-          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 \\<noteq> 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 "\\<exists>g' \\<in> M. g \\<subseteq> g' \\<and> g \\<noteq> g'" 
-          obtain x' where "x' \\<in> E" "x' \\<notin> H" 
-          -- {* Pick $x' \in E \setminus H$. \skp *}
-          proof -
-            have "\\<exists>x' \\<in> E. x' \\<notin> H"
-            proof (rule set_less_imp_diff_not_empty)
-              have "H \\<subseteq> E" ..
-              thus "H \\<subset> E" ..
-            qed
-            thus ?thesis by blast
+        obtain x' where "x' \\<in> E" "x' \\<notin> H" 
+        -- {* Pick $x' \in E \setminus H$. \skp *}
+        proof -
+          have "\\<exists>x' \\<in> E. x' \\<notin> H"
+          proof (rule set_less_imp_diff_not_empty)
+            have "H \\<subseteq> E" ..
+            thus "H \\<subset> E" ..
           qed
-          have x': "x' \\<noteq> 0"
-          proof (rule classical)
-            presume "x' = 0"
-            with h have "x' \\<in> 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 "\\<forall>y \\<in> H. - p (y + x') - h y <= xi 
-                              \\<and> 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' \\<noteq> 0"
+        proof (rule classical)
+          presume "x' = 0"
+          with h have "x' \\<in> 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 "\\<forall>y \\<in> H. - p (y + x') - h y <= xi 
+                          \\<and> 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 "\\<exists>xi. \\<forall>y \\<in> H. - p (y + x') - h y <= xi 
+                          \\<and> xi <= p (y + x') - h y" 
+          proof (rule ex_xi)
+            fix u v assume "u \\<in> H" "v \\<in> 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' == "\\<lambda>x. let (y,a) = SOME (y,a). x = y + a \\<cdot> x' \\<and> y \\<in> H
+                       in (h y) + a * xi"
+        -- {* Define the extension $h'$ of $h$ to $H'$ using $\xi$. \skp *}
+        show ?thesis
+        proof
+          show "g \\<subseteq> graph H' h' \\<and> g \\<noteq> graph H' h'" 
+          -- {* Show that $h'$ is an extension of $h$ \dots \skp *}
+          proof
+            show "g \\<subseteq> graph H' h'"
             proof -
-	      from h have "\\<exists>xi. \\<forall>y \\<in> H. - p (y + x') - h y <= xi 
-                              \\<and> xi <= p (y + x') - h y" 
-              proof (rule ex_xi)
-                fix u v assume "u \\<in> H" "v \\<in> 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 \\<subseteq> graph H' h'"
+              proof (rule graph_extI)
+                fix t assume "t \\<in> H" 
+                have "(SOME (y, a). t = y + a \\<cdot> x' \\<and> y \\<in> H)
+                     = (t, #0)"
+                  by (rule decomp_H'_H) (assumption+, rule x')
+                thus "h t = h' t" by (simp! add: Let_def)
+              next
+                show "H \\<subseteq> 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' == "\\<lambda>x. let (y,a) = SOME (y,a). x = y + a \\<cdot> x' \\<and> y \\<in> H
-                           in (h y) + a * xi"
-            -- {* Define the extension $h'$ of $h$ to $H'$ using $\xi$. \skp *}
-            show ?thesis
-            proof
-              show "g \\<subseteq> graph H' h' \\<and> g \\<noteq> graph H' h'" 
-              -- {* Show that $h'$ is an extension of $h$ \dots \skp *}
+            show "g \\<noteq> graph H' h'"
+            proof -
+              have "graph H h \\<noteq> graph H' h'"
               proof
-		show "g \\<subseteq> graph H' h'"
-		proof -
-		  have  "graph H h \\<subseteq> graph H' h'"
-                  proof (rule graph_extI)
-		    fix t assume "t \\<in> H" 
-		    have "(SOME (y, a). t = y + a \\<cdot> x' \\<and> y \\<in> H)
-                         = (t, #0)"
-		      by (rule decomp_H'_H) (assumption+, rule x')
-		    thus "h t = h' t" by (simp! add: Let_def)
-		  next
-		    show "H \\<subseteq> 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 \\<noteq> graph H' h'"
-		proof -
-		  have "graph H h \\<noteq> graph H' h'"
-		  proof
-		    assume e: "graph H h = graph H' h'"
-		    have "x' \\<in> H'" 
-		    proof (unfold H'_def, rule vs_sumI)
-		      show "x' = 0 + x'" by (simp!)
-		      from h show "0 \\<in> H" ..
-		      show "x' \\<in> lin x'" by (rule x_lin_x)
-		    qed
-		    hence "(x', h' x') \\<in> graph H' h'" ..
-		    with e have "(x', h' x') \\<in> graph H h" by simp
-		    hence "x' \\<in> H" ..
-		    thus False by contradiction
-		  qed
-		  thus ?thesis by (simp!)
-		qed
+                assume e: "graph H h = graph H' h'"
+                have "x' \\<in> H'" 
+                proof (unfold H'_def, rule vs_sumI)
+                  show "x' = 0 + x'" by (simp!)
+                  from h show "0 \\<in> H" ..
+                  show "x' \\<in> lin x'" by (rule x_lin_x)
+                qed
+                hence "(x', h' x') \\<in> graph H' h'" ..
+                with e have "(x', h' x') \\<in> graph H h" by simp
+                hence "x' \\<in> H" ..
+                thus False by contradiction
               qed
-	      show "graph H' h' \\<in> M" 
-              -- {* and $h'$ is norm-preserving. \skp *} 
-              proof -
-		have "graph H' h' \\<in> 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 \\<subseteq> graph H' h'"
-		  proof (rule graph_extI)
-		    fix x assume "x \\<in> 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 \\<cdot> x' \\<and> y \\<in> H)"
-		      by (rule decomp_H'_H [RS sym]) (simp! add: x')+
-		    also have 
-		      "(let (y,a) = (SOME (y,a). x = y + a \\<cdot> x' \\<and> y \\<in> H)
-                        in h y + a * xi) = h' x" by (simp!)
-		    finally show "f x = h' x" .
-		  next
-		    from f_h' show "F \\<subseteq> H'" ..
-		  qed
-		
-		  show "\\<forall>x \\<in> H'. h' x <= p x"
-		    by (rule h'_norm_pres) (assumption+, rule x')
-		qed
-		thus "graph H' h' \\<in> M" by (simp!)
-	      qed
+              thus ?thesis by (simp!)
             qed
           qed
+          show "graph H' h' \\<in> M" 
+          -- {* and $h'$ is norm-preserving. \skp *}
+          proof -
+            have "graph H' h' \\<in> 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 \\<subseteq> graph H' h'"
+              proof (rule graph_extI)
+                fix x assume "x \\<in> 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 \\<cdot> x' \\<and> y \\<in> H)"
+                  by (rule decomp_H'_H [RS sym]) (simp! add: x')+
+                also have 
+                  "(let (y,a) = (SOME (y,a). x = y + a \\<cdot> x' \\<and> y \\<in> H)
+                    in h y + a * xi) = h' x" by (simp!)
+                finally show "f x = h' x" .
+              next
+                from f_h' show "F \\<subseteq> H'" ..
+              qed
+            
+              show "\\<forall>x \\<in> H'. h' x <= p x"
+                by (rule h'_norm_pres) (assumption+, rule x')
+            qed
+            thus "graph H' h' \\<in> M" by (simp!)
+          qed
         qed
-        hence "\\<not> (\\<forall>x \\<in> M. g \\<subseteq> x --> g = x)" by simp
-        -- {* So the graph $g$ of $h$ cannot be maximal. Contradiction! \skp *}
-        thus "H = E" by contradiction
       qed
-      thus "\\<exists>h. is_linearform E h \\<and> (\\<forall>x \\<in> F. h x = f x) 
-          \\<and> (\\<forall>x \\<in> E. h x <= p x)" 
-      proof (intro exI conjI)
-        assume eq: "H = E"
-	from eq show "is_linearform E h" by (simp!)
-	show "\\<forall>x \\<in> F. h x = f x" 
-	proof (intro ballI, rule sym)
-	  fix x assume "x \\<in> F" show "f x = h x " ..
-	qed
-	from eq show "\\<forall>x \\<in> E. h x <= p x" by (force!)
+      hence "\\<not> (\\<forall>x \\<in> M. g \\<subseteq> x --> g = x)" by simp
+	-- {* So the graph $g$ of $h$ cannot be maximal. Contradiction! \skp *}
+      thus "H = E" by contradiction
+    qed
+    thus "\\<exists>h. is_linearform E h \\<and> (\\<forall>x \\<in> F. h x = f x) 
+      \\<and> (\\<forall>x \\<in> E. h x <= p x)" 
+    proof (intro exI conjI)
+      assume eq: "H = E"
+      from eq show "is_linearform E h" by (simp!)
+      show "\\<forall>x \\<in> F. h x = f x"
+      proof
+	fix x assume "x \\<in> F" have "f x = h x " ..
+	thus "h x = f x" ..
       qed
+      from eq show "\\<forall>x \\<in> 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; \\<forall>x \\<in> F. |f x| <= p x |]
-  ==> \\<exists>g. is_linearform E g \\<and> (\\<forall>x \\<in> F. g x = f x)
-   \\<and> (\\<forall>x \\<in> E. |g x| <= p x)"
+"[| is_vectorspace E; is_subspace F E; is_linearform F f; 
+is_seminorm E p; \\<forall>x \\<in> F. |f x| <= p x |]
+==> \\<exists>g. is_linearform E g \\<and> (\\<forall>x \\<in> F. g x = f x)
+ \\<and> (\\<forall>x \\<in> E. |g x| <= p x)"
 proof -
-  assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" 
-    "is_linearform F f"  "\\<forall>x \\<in> F. |f x| <= p x"
-  have "\\<forall>x \\<in> F. f x <= p x"  by (rule abs_ineq_iff [RS iffD1])
-  hence "\\<exists>g. is_linearform E g \\<and> (\\<forall>x \\<in> F. g x = f x) 
-              \\<and> (\\<forall>x \\<in> E. g x <= p x)"
-    by (simp! only: HahnBanach)
-  thus ?thesis 
-  proof (elim exE conjE)
-    fix g assume "is_linearform E g" "\\<forall>x \\<in> F. g x = f x" 
-                  "\\<forall>x \\<in> E. g x <= p x"
-    hence "\\<forall>x \\<in> 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"  "\\<forall>x \\<in> F. |f x| <= p x"
+have "\\<forall>x \\<in> F. f x <= p x"  by (rule abs_ineq_iff [RS iffD1])
+hence "\\<exists>g. is_linearform E g \\<and> (\\<forall>x \\<in> F. g x = f x) 
+          \\<and> (\\<forall>x \\<in> E. g x <= p x)"
+by (simp! only: HahnBanach)
+thus ?thesis 
+proof (elim exE conjE)
+fix g assume "is_linearform E g" "\\<forall>x \\<in> F. g x = f x" 
+              "\\<forall>x \\<in> E. g x <= p x"
+hence "\\<forall>x \\<in> 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 |] 
-  ==> \\<exists>g. is_linearform E g
-         \\<and> is_continuous E norm g 
-         \\<and> (\\<forall>x \\<in> F. g x = f x) 
-         \\<and> \\<parallel>g\\<parallel>E,norm = \\<parallel>f\\<parallel>F,norm"
+"[| is_normed_vectorspace E norm; is_subspace F E; 
+is_linearform F f; is_continuous F norm f |] 
+==> \\<exists>g. is_linearform E g
+     \\<and> is_continuous E norm g 
+     \\<and> (\\<forall>x \\<in> F. g x = f x) 
+     \\<and> \\<parallel>g\\<parallel>E,norm = \\<parallel>f\\<parallel>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 == "\\<lambda>x. \\<parallel>f\\<parallel>F,norm * norm x"
+
+txt{* $p$ is a seminorm on $E$: *}
+
+have q: "is_seminorm E p"
+proof
+fix x y a assume "x \\<in> E" "y \\<in> 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 <= \\<parallel>f\\<parallel>F,norm" ..
+  show "#0 <= norm x" ..
+qed
+
+txt{* $p$ is absolutely homogenous: *}
 
-  def p == "\\<lambda>x. \\<parallel>f\\<parallel>F,norm * norm x"
-  
-  txt{* $p$ is a seminorm on $E$: *}
+show "p (a \\<cdot> x) = |a| * p x"
+proof - 
+  have "p (a \\<cdot> x) = \\<parallel>f\\<parallel>F,norm * norm (a \\<cdot> x)"
+    by (simp!)
+  also have "norm (a \\<cdot> x) = |a| * norm x" 
+    by (rule normed_vs_norm_abs_homogenous)
+  also have "\\<parallel>f\\<parallel>F,norm * ( |a| * norm x ) 
+    = |a| * (\\<parallel>f\\<parallel>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 \\<in> E" "y \\<in> E"
-
-    txt{* $p$ is positive definite: *}
+show "p (x + y) <= p x + p y"
+proof -
+  have "p (x + y) = \\<parallel>f\\<parallel>F,norm * norm (x + y)"
+    by (simp!)
+  also 
+  have "... <= \\<parallel>f\\<parallel>F,norm * (norm x + norm y)"
+  proof (rule real_mult_le_le_mono1a)
+    from f_cont f_norm show "#0 <= \\<parallel>f\\<parallel>F,norm" ..
+    show "norm (x + y) <= norm x + norm y" ..
+  qed
+  also have "... = \\<parallel>f\\<parallel>F,norm * norm x 
+                    + \\<parallel>f\\<parallel>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 <= \\<parallel>f\\<parallel>F,norm" ..
-      show "#0 <= norm x" ..
-    qed
+txt{* $f$ is bounded by $p$. *} 
+
+have "\\<forall>x \\<in> F. |f x| <= p x"
+proof
+fix x assume "x \\<in> 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 "\\<exists>g. is_linearform E g \\<and> (\\<forall>x \\<in> F. g x = f x) 
+        \\<and> (\\<forall>x \\<in> 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: "\\<forall>x \\<in> F. g x = f x" 
+   and b: "\\<forall>x \\<in> E. |g x| <= p x"
+
+show "\\<exists>g. is_linearform E g 
+        \\<and> is_continuous E norm g 
+        \\<and> (\\<forall>x \\<in> F. g x = f x) 
+        \\<and> \\<parallel>g\\<parallel>E,norm = \\<parallel>f\\<parallel>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 \\<in> E"
+    with b show "|g x| <= \\<parallel>f\\<parallel>F,norm * norm x"
+      by (simp add: p_def) 
+  qed 
 
-    show "p (a \\<cdot> x) = |a| * p x"
-    proof - 
-      have "p (a \\<cdot> x) = \\<parallel>f\\<parallel>F,norm * norm (a \\<cdot> x)"
+  txt {* To complete the proof, we show that 
+  $\fnorm g = \fnorm f$. \label{order_antisym} *}
+
+  show "\\<parallel>g\\<parallel>E,norm = \\<parallel>f\\<parallel>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 "\\<forall>x \\<in> E. |g x| <= \\<parallel>f\\<parallel>F,norm * norm x"
+    proof
+      fix x assume "x \\<in> E" 
+      show "|g x| <= \\<parallel>f\\<parallel>F,norm * norm x"
         by (simp!)
-      also have "norm (a \\<cdot> x) = |a| * norm x" 
-        by (rule normed_vs_norm_abs_homogenous)
-      also have "\\<parallel>f\\<parallel>F,norm * ( |a| * norm x ) 
-        = |a| * (\\<parallel>f\\<parallel>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) = \\<parallel>f\\<parallel>F,norm * norm (x + y)"
-        by (simp!)
-      also 
-      have "... <= \\<parallel>f\\<parallel>F,norm * (norm x + norm y)"
-      proof (rule real_mult_le_le_mono1a)
-        from f_cont f_norm show "#0 <= \\<parallel>f\\<parallel>F,norm" ..
-        show "norm (x + y) <= norm x + norm y" ..
-      qed
-      also have "... = \\<parallel>f\\<parallel>F,norm * norm x 
-                        + \\<parallel>f\\<parallel>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 <= \\<parallel>f\\<parallel>F,norm" ..
     qed
-  qed
-
-  txt{* $f$ is bounded by $p$. *} 
 
-  have "\\<forall>x \\<in> F. |f x| <= p x"
-  proof
-    fix x assume "x \\<in> 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 "\\<exists>g. is_linearform E g \\<and> (\\<forall>x \\<in> F. g x = f x) 
-            \\<and> (\\<forall>x \\<in> 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: "\\<forall>x \\<in> F. g x = f x" 
-       and b: "\\<forall>x \\<in> E. |g x| <= p x"
-
-    show "\\<exists>g. is_linearform E g 
-            \\<and> is_continuous E norm g 
-            \\<and> (\\<forall>x \\<in> F. g x = f x) 
-            \\<and> \\<parallel>g\\<parallel>E,norm = \\<parallel>f\\<parallel>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 \\<in> E"
-        with b show "|g x| <= \\<parallel>f\\<parallel>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 "\\<parallel>g\\<parallel>E,norm = \\<parallel>f\\<parallel>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 "\\<forall>x \\<in> E. |g x| <= \\<parallel>f\\<parallel>F,norm * norm x"
-        proof
-          fix x assume "x \\<in> E" 
-          show "|g x| <= \\<parallel>f\\<parallel>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 <= \\<parallel>f\\<parallel>F,norm" ..
-        qed
-
-        txt{* The other direction is achieved by a similar 
-        argument. *}
-
-        have "\\<forall>x \\<in> F. |f x| <= \\<parallel>g\\<parallel>E,norm * norm x"
-        proof
-          fix x assume "x \\<in> F" 
-          from a have "g x = f x" ..
-          hence "|f x| = |g x|" by simp
-          also from g_cont
-          have "... <= \\<parallel>g\\<parallel>E,norm * norm x"
-          proof (rule norm_fx_le_norm_f_norm_x)
-            show "x \\<in> E" ..
-          qed
-          finally show "|f x| <= \\<parallel>g\\<parallel>E,norm * norm x" .
-        qed 
-        thus "?R <= ?L" 
-        proof (rule fnorm_le_ub [OF f_cont f_norm])
-          from g_cont show "#0 <= \\<parallel>g\\<parallel>E,norm" ..
-        qed
+    have "\\<forall>x \\<in> F. |f x| <= \\<parallel>g\\<parallel>E,norm * norm x"
+    proof
+      fix x assume "x \\<in> F" 
+      from a have "g x = f x" ..
+      hence "|f x| = |g x|" by simp
+      also from g_cont
+      have "... <= \\<parallel>g\\<parallel>E,norm * norm x"
+      proof (rule norm_fx_le_norm_f_norm_x)
+        show "x \\<in> E" ..
       qed
+      finally show "|f x| <= \\<parallel>g\\<parallel>E,norm * norm x" .
+    qed 
+    thus "?R <= ?L" 
+    proof (rule fnorm_le_ub [OF f_cont f_norm])
+      from g_cont show "#0 <= \\<parallel>g\\<parallel>E,norm" ..
     qed
   qed
 qed
+qed
+qed
 
-end
\ No newline at end of file
+end