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.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$