HOL-Hahn_Banach: use Set_Algebras library
authorhuffman
Sat Aug 13 07:56:55 2011 -0700 (2011-08-13)
changeset 44190fe5504984937
parent 44189 4a80017c733f
child 44191 be78e13a80d6
HOL-Hahn_Banach: use Set_Algebras library
src/HOL/Hahn_Banach/Hahn_Banach.thy
src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
src/HOL/Hahn_Banach/Subspace.thy
     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.6  
     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.16  
    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.5  
     3.6  theory Subspace
     3.7 -imports Vector_Space
     3.8 +imports Vector_Space "~~/src/HOL/Library/Set_Algebras"
     3.9  begin
    3.10  
    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.15  
    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.27  
    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.32  
    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.37  
    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.42  
    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.45  
    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.69  
    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.116  
   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.121  
   3.122  
   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