author wenzelm Tue Feb 22 21:49:34 2000 +0100 (2000-02-22) changeset 8280 259073d16f84 parent 8279 3453f73fad71 child 8281 188e2924433e
"cases" method;
     1.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Feb 22 21:48:50 2000 +0100
1.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Feb 22 21:49:34 2000 +0100
1.3 @@ -253,7 +253,7 @@
1.4   txt{* The proof is by case analysis on $x$. *};
1.5
1.6    show ?thesis;
1.7 -  proof (rule case_split);
1.8 +  proof cases;
1.9
1.10      txt {* For the case $x = \zero$ the thesis follows
1.11      from the linearity of $f$: for every linear function

     2.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Tue Feb 22 21:48:50 2000 +0100
2.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Tue Feb 22 21:49:34 2000 +0100
2.3 @@ -378,7 +378,7 @@
2.4          proof (unfold lin_def, elim CollectE exE conjE);
2.5            fix a; assume "x = a <*> x0";
2.6            show ?thesis;
2.7 -          proof (rule case_split);
2.8 +          proof cases;
2.9              assume "a = 0r"; show ?thesis; by (simp!);
2.10            next;
2.11              assume "a ~= 0r";
2.12 @@ -435,27 +435,27 @@
2.13  $h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *};
2.14
2.15  lemma h0_definite:
2.16 -  "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
2.17 +  "[| h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
2.18                  in (h y) + a * xi);
2.19    x = y + a <*> x0; is_vectorspace E; is_subspace H E;
2.20    y:H; x0 ~: H; x0:E; x0 ~= <0> |]
2.21    ==> h0 x = h y + a * xi";
2.22  proof -;
2.23    assume
2.24 -    "h0 == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
2.25 +    "h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
2.26                 in (h y) + a * xi)"
2.27      "x = y + a <*> x0" "is_vectorspace E" "is_subspace H E"
2.28      "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
2.29    have "x : H + (lin x0)";
2.30      by (simp! add: vs_sum_def lin_def) force+;
2.31 -  have "EX! xa. ((\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)";
2.32 +  have "EX! xa. ((\\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)";
2.33    proof;
2.34 -    show "EX xa. ((\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)";
2.35 +    show "EX xa. ((\\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)";
2.36        by (force!);
2.37    next;
2.38      fix xa ya;
2.39 -    assume "(\<lambda>(y,a). x = y + a <*> x0 & y : H) xa"
2.40 -           "(\<lambda>(y,a). x = y + a <*> x0 & y : H) ya";
2.41 +    assume "(\\<lambda>(y,a). x = y + a <*> x0 & y : H) xa"
2.42 +           "(\\<lambda>(y,a). x = y + a <*> x0 & y : H) ya";
2.43      show "xa = ya"; ;
2.44      proof -;
2.45        show "fst xa = fst ya & snd xa = snd ya ==> xa = ya";

     3.1 --- a/src/HOL/Real/HahnBanach/ZornLemma.thy	Tue Feb 22 21:48:50 2000 +0100
3.2 +++ b/src/HOL/Real/HahnBanach/ZornLemma.thy	Tue Feb 22 21:49:34 2000 +0100
3.3 @@ -27,7 +27,7 @@
3.4    proof;
3.5      fix c; assume "c:chain S";
3.6      show "EX y:S. ALL z:c. z <= y";
3.7 -    proof (rule case_split);
3.8 +    proof cases;
3.9
3.10        txt{* If $c$ is an empty chain, then every element
3.11        in $S$ is an upper bound of $c$. *};