src/HOL/Real/HahnBanach/Subspace.thy
changeset 9013 9dd0274f76af
parent 8703 816d8f6513be
child 9035 371f023d3dbd
     1.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Wed May 31 18:06:02 2000 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Thu Jun 01 11:22:27 2000 +0200
     1.3 @@ -87,7 +87,7 @@
     1.4      show "00 : U"; ..;
     1.5      show "ALL x:U. ALL a. a (*) x : U"; by (simp!);
     1.6      show "ALL x:U. ALL y:U. x + y : U"; by (simp!);
     1.7 -    show "ALL x:U. - x = -1r (*) x"; by (simp! add: negate_eq1);
     1.8 +    show "ALL x:U. - x = -#1 (*) x"; by (simp! add: negate_eq1);
     1.9      show "ALL x:U. ALL y:U. x - y =  x + - y"; 
    1.10        by (simp! add: diff_eq1);
    1.11    qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+;
    1.12 @@ -152,7 +152,7 @@
    1.13  lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x : lin x";
    1.14  proof (unfold lin_def, intro CollectI exI conjI);
    1.15    assume "is_vectorspace V" "x:V";
    1.16 -  show "x = 1r (*) x"; by (simp!);
    1.17 +  show "x = #1 (*) x"; by (simp!);
    1.18  qed simp;
    1.19  
    1.20  text {* Any linear closure is a subspace. *};
    1.21 @@ -163,7 +163,7 @@
    1.22    assume "is_vectorspace V" "x:V";
    1.23    show "00 : lin x"; 
    1.24    proof (unfold lin_def, intro CollectI exI conjI);
    1.25 -    show "00 = 0r (*) x"; by (simp!);
    1.26 +    show "00 = (#0::real) (*) x"; by (simp!);
    1.27    qed simp;
    1.28  
    1.29    show "lin x <= V";
    1.30 @@ -379,9 +379,9 @@
    1.31            fix a; assume "x = a (*) x0";
    1.32            show ?thesis;
    1.33            proof cases;
    1.34 -            assume "a = 0r"; show ?thesis; by (simp!);
    1.35 +            assume "a = (#0::real)"; show ?thesis; by (simp!);
    1.36            next;
    1.37 -            assume "a ~= 0r"; 
    1.38 +            assume "a ~= (#0::real)"; 
    1.39              from h; have "rinv a (*) a (*) x0 : H"; 
    1.40                by (rule subspace_mult_closed) (simp!);
    1.41              also; have "rinv a (*) a (*) x0 = x0"; by (simp!);
    1.42 @@ -419,15 +419,15 @@
    1.43  lemma decomp_H0_H: 
    1.44    "[| is_vectorspace E; is_subspace H E; t:H; x0 ~: H; x0:E;
    1.45    x0 ~= 00 |] 
    1.46 -  ==> (SOME (y, a). t = y + a (*) x0 & y : H) = (t, 0r)";
    1.47 +  ==> (SOME (y, a). t = y + a (*) x0 & y : H) = (t, (#0::real))";
    1.48  proof (rule, unfold split_paired_all);
    1.49    assume "is_vectorspace E" "is_subspace H E" "t:H" "x0 ~: H" "x0:E"
    1.50      "x0 ~= 00";
    1.51    have h: "is_vectorspace H"; ..;
    1.52    fix y a; presume t1: "t = y + a (*) x0" and "y:H";
    1.53 -  have "y = t & a = 0r"; 
    1.54 +  have "y = t & a = (#0::real)"; 
    1.55      by (rule decomp_H0) (assumption | (simp!))+;
    1.56 -  thus "(y, a) = (t, 0r)"; by (simp!);
    1.57 +  thus "(y, a) = (t, (#0::real))"; by (simp!);
    1.58  qed (simp!)+;
    1.59  
    1.60  text {* The components $y\in H$ and $a$ in $y \plus a \mult x_0$