author huffman Sat Aug 13 07:56:55 2011 -0700 (2011-08-13) changeset 44190 fe5504984937 parent 44189 4a80017c733f child 44191 be78e13a80d6
HOL-Hahn_Banach: use Set_Algebras library
1.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sat Aug 13 07:39:35 2011 -0700
1.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sat Aug 13 07:56:55 2011 -0700
1.3 @@ -151,12 +151,12 @@
1.4          qed
1.5        qed
1.7 -      def H' \<equiv> "H + lin x'"
1.8 +      def H' \<equiv> "H \<oplus> lin x'"
1.9          -- {* Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \skp *}
1.10        have HH': "H \<unlhd> H'"
1.11        proof (unfold H'_def)
1.12          from x'E have "vectorspace (lin x')" ..
1.13 -        with H show "H \<unlhd> H + lin x'" ..
1.14 +        with H show "H \<unlhd> H \<oplus> lin x'" ..
1.15        qed
1.17        obtain xi where
2.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Sat Aug 13 07:39:35 2011 -0700
2.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Sat Aug 13 07:56:55 2011 -0700
2.3 @@ -90,7 +90,7 @@
2.4  lemma h'_lf:
2.5    assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
2.6        SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
2.7 -    and H'_def: "H' \<equiv> H + lin x0"
2.8 +    and H'_def: "H' \<equiv> H \<oplus> lin x0"
2.9      and HE: "H \<unlhd> E"
2.10    assumes "linearform H h"
2.11    assumes x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"
2.12 @@ -106,7 +106,7 @@
2.13      proof (unfold H'_def)
2.14        from `x0 \<in> E`
2.15        have "lin x0 \<unlhd> E" ..
2.16 -      with HE show "vectorspace (H + lin x0)" using E ..
2.17 +      with HE show "vectorspace (H \<oplus> lin x0)" using E ..
2.18      qed
2.19      {
2.20        fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"
2.21 @@ -194,7 +194,7 @@
2.22  lemma h'_norm_pres:
2.23    assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
2.24        SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
2.25 -    and H'_def: "H' \<equiv> H + lin x0"
2.26 +    and H'_def: "H' \<equiv> H \<oplus> lin x0"
2.27      and x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"
2.28    assumes E: "vectorspace E" and HE: "subspace H E"
2.29      and "seminorm E p" and "linearform H h"
3.1 --- a/src/HOL/Hahn_Banach/Subspace.thy	Sat Aug 13 07:39:35 2011 -0700
3.2 +++ b/src/HOL/Hahn_Banach/Subspace.thy	Sat Aug 13 07:56:55 2011 -0700
3.3 @@ -5,7 +5,7 @@
3.4  header {* Subspaces *}
3.6  theory Subspace
3.7 -imports Vector_Space
3.8 +imports Vector_Space "~~/src/HOL/Library/Set_Algebras"
3.9  begin
3.11  subsection {* Definition *}
3.12 @@ -226,45 +226,38 @@
3.13    set of all sums of elements from @{text U} and @{text V}.
3.14  *}
3.16 -instantiation "fun" :: (type, type) plus
3.17 -begin
3.18 -
3.19 -definition
3.20 -  sum_def: "plus_fun U V = {u + v | u v. u \<in> U \<and> v \<in> V}"  (* FIXME not fully general!? *)
3.21 -
3.22 -instance ..
3.23 -
3.24 -end
3.25 +lemma sum_def: "U \<oplus> V = {u + v | u v. u \<in> U \<and> v \<in> V}"
3.26 +  unfolding set_plus_def by auto
3.28  lemma sumE [elim]:
3.29 -    "x \<in> U + V \<Longrightarrow> (\<And>u v. x = u + v \<Longrightarrow> u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> C) \<Longrightarrow> C"
3.30 +    "x \<in> U \<oplus> V \<Longrightarrow> (\<And>u v. x = u + v \<Longrightarrow> u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> C) \<Longrightarrow> C"
3.31    unfolding sum_def by blast
3.33  lemma sumI [intro]:
3.34 -    "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> x = u + v \<Longrightarrow> x \<in> U + V"
3.35 +    "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> x = u + v \<Longrightarrow> x \<in> U \<oplus> V"
3.36    unfolding sum_def by blast
3.38  lemma sumI' [intro]:
3.39 -    "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> u + v \<in> U + V"
3.40 +    "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> u + v \<in> U \<oplus> V"
3.41    unfolding sum_def by blast
3.43 -text {* @{text U} is a subspace of @{text "U + V"}. *}
3.44 +text {* @{text U} is a subspace of @{text "U \<oplus> V"}. *}
3.46  lemma subspace_sum1 [iff]:
3.47    assumes "vectorspace U" "vectorspace V"
3.48 -  shows "U \<unlhd> U + V"
3.49 +  shows "U \<unlhd> U \<oplus> V"
3.50  proof -
3.51    interpret vectorspace U by fact
3.52    interpret vectorspace V by fact
3.53    show ?thesis
3.54    proof
3.55      show "U \<noteq> {}" ..
3.56 -    show "U \<subseteq> U + V"
3.57 +    show "U \<subseteq> U \<oplus> V"
3.58      proof
3.59        fix x assume x: "x \<in> U"
3.60        moreover have "0 \<in> V" ..
3.61 -      ultimately have "x + 0 \<in> U + V" ..
3.62 -      with x show "x \<in> U + V" by simp
3.63 +      ultimately have "x + 0 \<in> U \<oplus> V" ..
3.64 +      with x show "x \<in> U \<oplus> V" by simp
3.65      qed
3.66      fix x y assume x: "x \<in> U" and "y \<in> U"
3.67      then show "x + y \<in> U" by simp
3.68 @@ -276,29 +269,29 @@
3.70  lemma sum_subspace [intro?]:
3.71    assumes "subspace U E" "vectorspace E" "subspace V E"
3.72 -  shows "U + V \<unlhd> E"
3.73 +  shows "U \<oplus> V \<unlhd> E"
3.74  proof -
3.75    interpret subspace U E by fact
3.76    interpret vectorspace E by fact
3.77    interpret subspace V E by fact
3.78    show ?thesis
3.79    proof
3.80 -    have "0 \<in> U + V"
3.81 +    have "0 \<in> U \<oplus> V"
3.82      proof
3.83        show "0 \<in> U" using `vectorspace E` ..
3.84        show "0 \<in> V" using `vectorspace E` ..
3.85        show "(0::'a) = 0 + 0" by simp
3.86      qed
3.87 -    then show "U + V \<noteq> {}" by blast
3.88 -    show "U + V \<subseteq> E"
3.89 +    then show "U \<oplus> V \<noteq> {}" by blast
3.90 +    show "U \<oplus> V \<subseteq> E"
3.91      proof
3.92 -      fix x assume "x \<in> U + V"
3.93 +      fix x assume "x \<in> U \<oplus> V"
3.94        then obtain u v where "x = u + v" and
3.95          "u \<in> U" and "v \<in> V" ..
3.96        then show "x \<in> E" by simp
3.97      qed
3.98 -    fix x y assume x: "x \<in> U + V" and y: "y \<in> U + V"
3.99 -    show "x + y \<in> U + V"
3.100 +    fix x y assume x: "x \<in> U \<oplus> V" and y: "y \<in> U \<oplus> V"
3.101 +    show "x + y \<in> U \<oplus> V"
3.102      proof -
3.103        from x obtain ux vx where "x = ux + vx" and "ux \<in> U" and "vx \<in> V" ..
3.104        moreover
3.105 @@ -310,7 +303,7 @@
3.106          using x y by (simp_all add: add_ac)
3.107        then show ?thesis ..
3.108      qed
3.109 -    fix a show "a \<cdot> x \<in> U + V"
3.110 +    fix a show "a \<cdot> x \<in> U \<oplus> V"
3.111      proof -
3.112        from x obtain u v where "x = u + v" and "u \<in> U" and "v \<in> V" ..
3.113        then have "a \<cdot> u \<in> U" and "a \<cdot> v \<in> V"
3.114 @@ -323,7 +316,7 @@
3.115  text{* The sum of two subspaces is a vectorspace. *}
3.117  lemma sum_vs [intro?]:
3.118 -    "U \<unlhd> E \<Longrightarrow> V \<unlhd> E \<Longrightarrow> vectorspace E \<Longrightarrow> vectorspace (U + V)"
3.119 +    "U \<unlhd> E \<Longrightarrow> V \<unlhd> E \<Longrightarrow> vectorspace E \<Longrightarrow> vectorspace (U \<oplus> V)"
3.120    by (rule subspace.vectorspace) (rule sum_subspace)
3.123 @@ -484,7 +477,7 @@
3.124  proof -
3.125    interpret vectorspace E by fact
3.126    interpret subspace H E by fact
3.127 -  from x y x' have "x \<in> H + lin x'" by auto
3.128 +  from x y x' have "x \<in> H \<oplus> lin x'" by auto
3.129    have "\<exists>!p. (\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) p" (is "\<exists>!p. ?P p")
3.130    proof (rule ex_ex1I)
3.131      from x y show "\<exists>p. ?P p" by blast