"cases" method;
authorwenzelm
Tue Feb 22 21:49:34 2000 +0100 (2000-02-22)
changeset 8280259073d16f84
parent 8279 3453f73fad71
child 8281 188e2924433e
"cases" method;
src/HOL/Real/HahnBanach/FunctionNorm.thy
src/HOL/Real/HahnBanach/Subspace.thy
src/HOL/Real/HahnBanach/ZornLemma.thy
     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$. *};