src/HOL/Real/HahnBanach/Subspace.thy
changeset 8280 259073d16f84
parent 8203 2fcc6017cb72
child 8703 816d8f6513be
     1.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Tue Feb 22 21:48:50 2000 +0100
     1.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Tue Feb 22 21:49:34 2000 +0100
     1.3 @@ -378,7 +378,7 @@
     1.4          proof (unfold lin_def, elim CollectE exE conjE);
     1.5            fix a; assume "x = a <*> x0";
     1.6            show ?thesis;
     1.7 -          proof (rule case_split);
     1.8 +          proof cases;
     1.9              assume "a = 0r"; show ?thesis; by (simp!);
    1.10            next;
    1.11              assume "a ~= 0r"; 
    1.12 @@ -435,27 +435,27 @@
    1.13  $h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *};
    1.14  
    1.15  lemma h0_definite:
    1.16 -  "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
    1.17 +  "[| h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
    1.18                  in (h y) + a * xi);
    1.19    x = y + a <*> x0; is_vectorspace E; is_subspace H E;
    1.20    y:H; x0 ~: H; x0:E; x0 ~= <0> |]
    1.21    ==> h0 x = h y + a * xi";
    1.22  proof -;  
    1.23    assume 
    1.24 -    "h0 == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
    1.25 +    "h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
    1.26                 in (h y) + a * xi)"
    1.27      "x = y + a <*> x0" "is_vectorspace E" "is_subspace H E"
    1.28      "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
    1.29    have "x : H + (lin x0)"; 
    1.30      by (simp! add: vs_sum_def lin_def) force+;
    1.31 -  have "EX! xa. ((\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)"; 
    1.32 +  have "EX! xa. ((\\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)"; 
    1.33    proof;
    1.34 -    show "EX xa. ((\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)";
    1.35 +    show "EX xa. ((\\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)";
    1.36        by (force!);
    1.37    next;
    1.38      fix xa ya;
    1.39 -    assume "(\<lambda>(y,a). x = y + a <*> x0 & y : H) xa"
    1.40 -           "(\<lambda>(y,a). x = y + a <*> x0 & y : H) ya";
    1.41 +    assume "(\\<lambda>(y,a). x = y + a <*> x0 & y : H) xa"
    1.42 +           "(\\<lambda>(y,a). x = y + a <*> x0 & y : H) ya";
    1.43      show "xa = ya"; ;
    1.44      proof -;
    1.45        show "fst xa = fst ya & snd xa = snd ya ==> xa = ya";