# HG changeset patch
# User wenzelm
# Date 964087487 -7200
# Node ID 1ff8a6234c6a7dd3d2b4b08ebe86f5b5c2296276
# Parent  c97111953a66a95087ef043658731a5bb422dabb
tuned;

diff -r c97111953a66 -r 1ff8a6234c6a src/HOL/Real/HahnBanach/Aux.thy
--- a/src/HOL/Real/HahnBanach/Aux.thy	Wed Jul 19 18:57:27 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy	Thu Jul 20 12:04:47 2000 +0200
@@ -38,19 +38,6 @@
 qed
 
 text_raw {* \medskip *}
-text {* Some lemmas about linear orders. *}
-
-theorem linorder_linear_split: 
-"[| x < a ==> Q; x = a ==> Q; a < (x::'a::linorder) ==> Q |] ==> Q"
-  by (rule linorder_less_linear [of x a, elimify]) 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])
-
-text_raw {* \medskip *}
 text{* Some lemmas for the reals. *}
 
 lemma real_add_minus_eq: "x - y = (#0::real) ==> x = y"
@@ -66,9 +53,9 @@
   hence "x < y | x = y" by (force simp add: order_le_less)
   thus ?thesis
   proof (elim disjE) 
-   assume "x < y" show ?thesis by  (rule real_mult_le_less_mono2) simp
+    assume "x < y" show ?thesis by  (rule real_mult_le_less_mono2) simp
   next 
-   assume "x = y" thus ?thesis by simp
+    assume "x = y" thus ?thesis by simp
   qed
 qed
 
@@ -79,9 +66,9 @@
   hence "x < y | x = y" by (force simp add: order_le_less)
   thus ?thesis
   proof (elim disjE) 
-   assume "x < y" show ?thesis by (rule real_mult_le_less_mono1) simp
+    assume "x < y" show ?thesis by (rule real_mult_le_less_mono1) simp
   next 
-   assume "x = y" thus ?thesis by simp
+    assume "x = y" thus ?thesis by simp
   qed
 qed
 
@@ -108,27 +95,27 @@
   thus ?thesis by (simp only: real_mult_commute)
 qed
 
-lemma real_rinv_gt_zero1: "#0 < x ==> #0 < rinv x";
-proof -; 
-  assume "#0 < x";
-  have "0 < x"; by simp;
-  hence "0 < rinv x"; by (rule real_rinv_gt_zero);
-  thus ?thesis; by simp;
-qed;
+lemma real_rinv_gt_zero1: "#0 < x ==> #0 < rinv x"
+proof - 
+  assume "#0 < x"
+  have "0 < x" by simp
+  hence "0 < rinv x" by (rule real_rinv_gt_zero)
+  thus ?thesis by simp
+qed
 
 lemma real_mult_inv_right1: "x \\<noteq> #0 ==> x*rinv(x) = #1"
-   by simp
+  by simp
 
 lemma real_mult_inv_left1: "x \\<noteq> #0 ==> rinv(x) * x = #1"
-   by simp
+  by simp
 
 lemma real_le_mult_order1a: 
-      "[| (#0::real) <= x; #0 <= y |] ==> #0 <= x * y"
+  "[| (#0::real) <= x; #0 <= y |] ==> #0 <= x * y"
 proof -
   assume "#0 <= x" "#0 <= y"
-    have "[|0 <= x; 0 <= y|] ==> 0 <= x * y"  
-      by (rule real_le_mult_order)
-    thus ?thesis by (simp!)
+  have "[|0 <= x; 0 <= y|] ==> 0 <= x * y"  
+    by (rule real_le_mult_order)
+  thus ?thesis by (simp!)
 qed
 
 lemma real_mult_diff_distrib: 
@@ -138,7 +125,7 @@
   also have "a * ... = a * - x + a * - y" 
     by (simp only: real_add_mult_distrib2)
   also have "... = - a * x - a * y" 
-    by simp;
+    by simp
   finally show ?thesis .
 qed
 
@@ -148,7 +135,7 @@
   also have "a * ... = a * x + a * - y" 
     by (simp only: real_add_mult_distrib2)
   also have "... = a * x - a * y"   
-    by simp;
+    by simp
   finally show ?thesis .
 qed
 
@@ -156,7 +143,7 @@
   by simp
 
 lemma real_diff_ineq_swap: 
-  "(d::real) - b <= c + a ==> - a - b <= c - d"
+    "(d::real) - b <= c + a ==> - a - b <= c - d"
   by simp
 
 end
\ No newline at end of file
diff -r c97111953a66 -r 1ff8a6234c6a src/HOL/Real/HahnBanach/FunctionNorm.thy
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Wed Jul 19 18:57:27 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Thu Jul 20 12:04:47 2000 +0200
@@ -136,7 +136,7 @@
         $y\in B$. If $y = 0$ then $y \leq \idt{max}\ap c\ap 0$: *}
 
 	fix y assume "y = (#0::real)"
-        show "y <= b" by (simp! add: le_max2)
+        show "y <= b" by (simp! add: le_maxI2)
 
         txt{* The second case is 
         $y = {|f\ap x|}/{\norm x}$ for some 
@@ -184,7 +184,7 @@
             by (rule not_sym, rule lt_imp_not_eq, 
               rule normed_vs_norm_gt_zero)
         qed
-        also have "c * ... <= b " by (simp! add: le_max1)
+        also have "c * ... <= b " by (simp! add: le_maxI1)
 	finally show "y <= b" .
       qed simp
     qed
diff -r c97111953a66 -r 1ff8a6234c6a src/HOL/Real/HahnBanach/HahnBanach.thy
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Wed Jul 19 18:57:27 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Jul 20 12:04:47 2000 +0200
@@ -78,23 +78,23 @@
   -- {* Define $M$ as the set of all norm-preserving extensions of $F$. \skp *}
   {
     fix c assume "c \\<in> chain M" "\\<exists>x. x \\<in> c"
-    have "\\<Union> c \\<in> M"
+    have "\\<Union>c \\<in> M"
     -- {* Show that every non-empty chain $c$ of $M$ has an upper bound in $M$: *}
     -- {* $\Union c$ is greater than any element of the chain $c$, so it suffices to show $\Union c \in M$. *}
     proof (unfold M_def, rule norm_pres_extensionI)
-      show "\\<exists>H h. graph H h = \\<Union> c
+      show "\\<exists>H h. graph H h = \\<Union>c
               \\<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)"
       proof (intro exI conjI)
-        let ?H = "domain (\\<Union> c)"
-        let ?h = "funct (\\<Union> c)"
+        let ?H = "domain (\\<Union>c)"
+        let ?h = "funct (\\<Union>c)"
 
-        show a: "graph ?H ?h = \\<Union> c" 
+        show a: "graph ?H ?h = \\<Union>c" 
         proof (rule graph_domain_funct)
-          fix x y z assume "(x, y) \\<in> \\<Union> c" "(x, z) \\<in> \\<Union> c"
+          fix x y z assume "(x, y) \\<in> \\<Union>c" "(x, z) \\<in> \\<Union>c"
           show "z = y" by (rule sup_definite)
         qed
         show "is_linearform ?H ?h" 
@@ -214,7 +214,7 @@
 		    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');
+		      by (rule decomp_H'_H) (assumption+, rule x')
 		    thus "h t = h' t" by (simp! add: Let_def)
 		  next
 		    show "H \\<subseteq> H'"
diff -r c97111953a66 -r 1ff8a6234c6a src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Wed Jul 19 18:57:27 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Jul 20 12:04:47 2000 +0200
@@ -270,10 +270,10 @@
 
     txt{* Now we show  
     $h\ap y + a \cdot \xi\leq  p\ap (y\plus a \mult x_0)$ 
-    by case analysis on $a$. \label{linorder_linear_split}*};
+    by case analysis on $a$. *};
 
     also; have "... <= p (y + a \\<cdot> x0)";
-    proof (rule linorder_linear_split); 
+    proof (rule linorder_less_split); 
 
       assume z: "a = #0"; 
       with vs y a; show ?thesis; by simp;
diff -r c97111953a66 -r 1ff8a6234c6a src/HOL/Real/HahnBanach/HahnBanachLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachLemmas.thy	Wed Jul 19 18:57:27 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachLemmas.thy	Thu Jul 20 12:04:47 2000 +0200
@@ -1,3 +1,3 @@
 
-theory HahnBanachLemmas = HahnBanachSupLemmas + HahnBanachExtLemmas:;
-end;
+theory HahnBanachLemmas = HahnBanachSupLemmas + HahnBanachExtLemmas:
+end
diff -r c97111953a66 -r 1ff8a6234c6a src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Wed Jul 19 18:57:27 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Thu Jul 20 12:04:47 2000 +0200
@@ -25,17 +25,17 @@
 
 lemma some_H'h't:
   "[| M = norm_pres_extensions E p F f; c \\<in> chain M; 
-  graph H h = \\<Union> c; x \\<in> H |]
+  graph H h = \\<Union>c; x \\<in> H |]
    ==> \\<exists>H' h'. graph H' h' \\<in> c \\<and> (x, h x) \\<in> graph H' h' 
        \\<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)"
 proof -
   assume m: "M = norm_pres_extensions E p F f" and "c \\<in> chain M"
-     and u: "graph H h = \\<Union> c" "x \\<in> H"
+     and u: "graph H h = \\<Union>c" "x \\<in> H"
 
   have h: "(x, h x) \\<in> graph H h" ..
-  with u have "(x, h x) \\<in> \\<Union> c" by simp
+  with u have "(x, h x) \\<in> \\<Union>c" by simp
   hence ex1: "\\<exists>g \\<in> c. (x, h x) \\<in> g" 
     by (simp only: Union_iff)
   thus ?thesis
@@ -75,13 +75,13 @@
 
 lemma some_H'h': 
   "[| M = norm_pres_extensions E p F f; c \\<in> chain M; 
-  graph H h = \\<Union> c; x \\<in> H |] 
+  graph H h = \\<Union>c; x \\<in> H |] 
   ==> \\<exists>H' h'. x \\<in> H' \\<and> graph H' h' \\<subseteq> graph H h 
       \\<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)" 
 proof -
   assume "M = norm_pres_extensions E p F f" and cM: "c \\<in> chain M"
-     and u: "graph H h = \\<Union> c" "x \\<in> H"  
+     and u: "graph H h = \\<Union>c" "x \\<in> H"  
 
   have "\\<exists>H' h'. graph H' h' \\<in> c \\<and> (x, h x) \\<in> graph H' h' 
        \\<and> is_linearform H' h' \\<and> is_subspace H' E 
@@ -109,13 +109,13 @@
 
 lemma some_H'h'2: 
   "[| M = norm_pres_extensions E p F f; c \\<in> chain M; 
-  graph H h = \\<Union> c;  x \\<in> H; y \\<in> H |] 
+  graph H h = \\<Union>c;  x \\<in> H; y \\<in> H |] 
   ==> \\<exists>H' h'. x \\<in> H' \\<and> y \\<in> H' \\<and> graph H' h' \\<subseteq> graph H h 
       \\<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)" 
 proof -
   assume "M = norm_pres_extensions E p F f" "c \\<in> chain M" 
-         "graph H h = \\<Union> c" "x \\<in> H" "y \\<in> H"
+         "graph H h = \\<Union>c" "x \\<in> H" "y \\<in> H"
 
   txt {* $x$ is in the domain $H'$ of some function $h'$, 
   such that $h$ extends $h'$. *} 
@@ -188,10 +188,10 @@
 
 lemma sup_definite: 
   "[| M == norm_pres_extensions E p F f; c \\<in> chain M; 
-  (x, y) \\<in> \\<Union> c; (x, z) \\<in> \\<Union> c |] ==> z = y"
+  (x, y) \\<in> \\<Union>c; (x, z) \\<in> \\<Union>c |] ==> z = y"
 proof - 
   assume "c \\<in> chain M" "M == norm_pres_extensions E p F f"
-    "(x, y) \\<in> \\<Union> c" "(x, z) \\<in> \\<Union> c"
+    "(x, y) \\<in> \\<Union>c" "(x, z) \\<in> \\<Union>c"
   thus ?thesis
   proof (elim UnionE chainE2)
 
@@ -245,10 +245,10 @@
 
 lemma sup_lf: 
   "[| M = norm_pres_extensions E p F f; c \\<in> chain M; 
-  graph H h = \\<Union> c |] ==> is_linearform H h"
+  graph H h = \\<Union>c |] ==> is_linearform H h"
 proof - 
   assume "M = norm_pres_extensions E p F f" "c \\<in> chain M"
-         "graph H h = \\<Union> c"
+         "graph H h = \\<Union>c"
  
   show "is_linearform H h"
   proof
@@ -306,11 +306,11 @@
 for every element of the chain.*}
 
 lemma sup_ext:
-  "[| graph H h = \\<Union> c; M = norm_pres_extensions E p F f; 
+  "[| graph H h = \\<Union>c; M = norm_pres_extensions E p F f; 
   c \\<in> chain M; \\<exists>x. x \\<in> c |] ==> graph F f \\<subseteq> graph H h"
 proof -
   assume "M = norm_pres_extensions E p F f" "c \\<in> chain M" 
-         "graph H h = \\<Union> c"
+         "graph H h = \\<Union>c"
   assume "\\<exists>x. x \\<in> c"
   thus ?thesis 
   proof
@@ -332,8 +332,8 @@
       fix G g assume "graph F f \\<subseteq> graph G g"
       also assume "graph G g = x"
       also have "... \\<in> c" .
-      hence "x \\<subseteq> \\<Union> c" by fast
-      also have [RS sym]: "graph H h = \\<Union> c" .
+      hence "x \\<subseteq> \\<Union>c" by fast
+      also have [RS sym]: "graph H h = \\<Union>c" .
       finally show ?thesis .
     qed
   qed
@@ -345,12 +345,12 @@
 vector space. *}
 
 lemma sup_supF: 
-  "[|  graph H h = \\<Union> c; M = norm_pres_extensions E p F f; 
+  "[|  graph H h = \\<Union>c; M = norm_pres_extensions E p F f; 
   c \\<in> chain M; \\<exists>x. x \\<in> c; is_subspace F E; is_vectorspace E |] 
   ==> is_subspace F H"
 proof - 
   assume "M = norm_pres_extensions E p F f" "c \\<in> chain M" "\\<exists>x. x \\<in> c"
-    "graph H h = \\<Union> c" "is_subspace F E" "is_vectorspace E"
+    "graph H h = \\<Union>c" "is_subspace F E" "is_vectorspace E"
 
   show ?thesis 
   proof
@@ -377,12 +377,12 @@
 of $E$. *}
 
 lemma sup_subE: 
-  "[| graph H h = \\<Union> c; M = norm_pres_extensions E p F f; 
+  "[| graph H h = \\<Union>c; M = norm_pres_extensions E p F f; 
   c \\<in> chain M; \\<exists>x. x \\<in> c; is_subspace F E; is_vectorspace E |] 
   ==> is_subspace H E"
 proof - 
   assume "M = norm_pres_extensions E p F f" "c \\<in> chain M" "\\<exists>x. x \\<in> c"
-    "graph H h = \\<Union> c" "is_subspace F E" "is_vectorspace E"
+    "graph H h = \\<Union>c" "is_subspace F E" "is_vectorspace E"
   show ?thesis 
   proof
  
@@ -461,11 +461,11 @@
 *}
 
 lemma sup_norm_pres:
-  "[| graph H h = \\<Union> c; M = norm_pres_extensions E p F f; 
+  "[| graph H h = \\<Union>c; M = norm_pres_extensions E p F f; 
   c \\<in> chain M |] ==> \\<forall>x \\<in> H. h x <= p x"
 proof
   assume "M = norm_pres_extensions E p F f" "c \\<in> chain M" 
-         "graph H h = \\<Union> c"
+         "graph H h = \\<Union>c"
   fix x assume "x \\<in> H"
   have "\\<exists>H' h'. x \\<in> H' \\<and> graph H' h' \\<subseteq> graph H h 
           \\<and> is_linearform H' h' \\<and> is_subspace H' E \\<and> is_subspace F H'
diff -r c97111953a66 -r 1ff8a6234c6a src/HOL/Real/HahnBanach/document/notation.tex
--- a/src/HOL/Real/HahnBanach/document/notation.tex	Wed Jul 19 18:57:27 2000 +0200
+++ b/src/HOL/Real/HahnBanach/document/notation.tex	Thu Jul 20 12:04:47 2000 +0200
@@ -24,7 +24,8 @@
 \newcommand{\Le}{\leq}
 \newcommand{\Lt}{\lt}
 \newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
-\newcommand{\ap}{\mathpalette{\mathbin{\!}}{\mathbin{\!}}{\mathbin{}}{\mathbin{}}}
+%\newcommand{\ap}{\mathpalette{\mathbin{\!}}{\mathbin{\!}}{\mathbin{}}{\mathbin{}}}
+\newcommand{\ap}{\mathpalette{\mathbin{}}{\mathbin{}}{\mathbin{}}{\mathbin{}}}
 \newcommand{\Union}{\bigcup}
 \newcommand{\Un}{\cup}
 \newcommand{\Int}{\cap}