src/HOL/Hahn_Banach/Vector_Space.thy
 author blanchet Thu Jan 16 16:33:19 2014 +0100 (2014-01-16) changeset 55018 2a526bd279ed parent 54230 b1d955791529 child 57512 cc97b347b301 permissions -rw-r--r--
moved 'Zorn' into 'Main', since it's a BNF dependency
     1 (*  Title:      HOL/Hahn_Banach/Vector_Space.thy

     2     Author:     Gertrud Bauer, TU Munich

     3 *)

     4

     5 header {* Vector spaces *}

     6

     7 theory Vector_Space

     8 imports Complex_Main Bounds

     9 begin

    10

    11 subsection {* Signature *}

    12

    13 text {*

    14   For the definition of real vector spaces a type @{typ 'a} of the

    15   sort @{text "{plus, minus, zero}"} is considered, on which a real

    16   scalar multiplication @{text \<cdot>} is declared.

    17 *}

    18

    19 consts

    20   prod  :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a"     (infixr "'(*')" 70)

    21

    22 notation (xsymbols)

    23   prod  (infixr "\<cdot>" 70)

    24 notation (HTML output)

    25   prod  (infixr "\<cdot>" 70)

    26

    27

    28 subsection {* Vector space laws *}

    29

    30 text {*

    31   A \emph{vector space} is a non-empty set @{text V} of elements from

    32   @{typ 'a} with the following vector space laws: The set @{text V} is

    33   closed under addition and scalar multiplication, addition is

    34   associative and commutative; @{text "- x"} is the inverse of @{text

    35   x} w.~r.~t.~addition and @{text 0} is the neutral element of

    36   addition.  Addition and multiplication are distributive; scalar

    37   multiplication is associative and the real number @{text "1"} is

    38   the neutral element of scalar multiplication.

    39 *}

    40

    41 locale vectorspace =

    42   fixes V

    43   assumes non_empty [iff, intro?]: "V \<noteq> {}"

    44     and add_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y \<in> V"

    45     and mult_closed [iff]: "x \<in> V \<Longrightarrow> a \<cdot> x \<in> V"

    46     and add_assoc: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (x + y) + z = x + (y + z)"

    47     and add_commute: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y = y + x"

    48     and diff_self [simp]: "x \<in> V \<Longrightarrow> x - x = 0"

    49     and add_zero_left [simp]: "x \<in> V \<Longrightarrow> 0 + x = x"

    50     and add_mult_distrib1: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y"

    51     and add_mult_distrib2: "x \<in> V \<Longrightarrow> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x"

    52     and mult_assoc: "x \<in> V \<Longrightarrow> (a * b) \<cdot> x = a \<cdot> (b \<cdot> x)"

    53     and mult_1 [simp]: "x \<in> V \<Longrightarrow> 1 \<cdot> x = x"

    54     and negate_eq1: "x \<in> V \<Longrightarrow> - x = (- 1) \<cdot> x"

    55     and diff_eq1: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y = x + - y"

    56 begin

    57

    58 lemma negate_eq2: "x \<in> V \<Longrightarrow> (- 1) \<cdot> x = - x"

    59   by (rule negate_eq1 [symmetric])

    60

    61 lemma negate_eq2a: "x \<in> V \<Longrightarrow> -1 \<cdot> x = - x"

    62   by (simp add: negate_eq1)

    63

    64 lemma diff_eq2: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + - y = x - y"

    65   by (rule diff_eq1 [symmetric])

    66

    67 lemma diff_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y \<in> V"

    68   by (simp add: diff_eq1 negate_eq1)

    69

    70 lemma neg_closed [iff]: "x \<in> V \<Longrightarrow> - x \<in> V"

    71   by (simp add: negate_eq1)

    72

    73 lemma add_left_commute: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)"

    74 proof -

    75   assume xyz: "x \<in> V"  "y \<in> V"  "z \<in> V"

    76   then have "x + (y + z) = (x + y) + z"

    77     by (simp only: add_assoc)

    78   also from xyz have "\<dots> = (y + x) + z" by (simp only: add_commute)

    79   also from xyz have "\<dots> = y + (x + z)" by (simp only: add_assoc)

    80   finally show ?thesis .

    81 qed

    82

    83 theorems add_ac = add_assoc add_commute add_left_commute

    84

    85

    86 text {* The existence of the zero element of a vector space

    87   follows from the non-emptiness of carrier set. *}

    88

    89 lemma zero [iff]: "0 \<in> V"

    90 proof -

    91   from non_empty obtain x where x: "x \<in> V" by blast

    92   then have "0 = x - x" by (rule diff_self [symmetric])

    93   also from x x have "\<dots> \<in> V" by (rule diff_closed)

    94   finally show ?thesis .

    95 qed

    96

    97 lemma add_zero_right [simp]: "x \<in> V \<Longrightarrow>  x + 0 = x"

    98 proof -

    99   assume x: "x \<in> V"

   100   from this and zero have "x + 0 = 0 + x" by (rule add_commute)

   101   also from x have "\<dots> = x" by (rule add_zero_left)

   102   finally show ?thesis .

   103 qed

   104

   105 lemma mult_assoc2: "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = (a * b) \<cdot> x"

   106   by (simp only: mult_assoc)

   107

   108 lemma diff_mult_distrib1: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<cdot> (x - y) = a \<cdot> x - a \<cdot> y"

   109   by (simp add: diff_eq1 negate_eq1 add_mult_distrib1 mult_assoc2)

   110

   111 lemma diff_mult_distrib2: "x \<in> V \<Longrightarrow> (a - b) \<cdot> x = a \<cdot> x - (b \<cdot> x)"

   112 proof -

   113   assume x: "x \<in> V"

   114   have " (a - b) \<cdot> x = (a + - b) \<cdot> x"

   115     by simp

   116   also from x have "\<dots> = a \<cdot> x + (- b) \<cdot> x"

   117     by (rule add_mult_distrib2)

   118   also from x have "\<dots> = a \<cdot> x + - (b \<cdot> x)"

   119     by (simp add: negate_eq1 mult_assoc2)

   120   also from x have "\<dots> = a \<cdot> x - (b \<cdot> x)"

   121     by (simp add: diff_eq1)

   122   finally show ?thesis .

   123 qed

   124

   125 lemmas distrib =

   126   add_mult_distrib1 add_mult_distrib2

   127   diff_mult_distrib1 diff_mult_distrib2

   128

   129

   130 text {* \medskip Further derived laws: *}

   131

   132 lemma mult_zero_left [simp]: "x \<in> V \<Longrightarrow> 0 \<cdot> x = 0"

   133 proof -

   134   assume x: "x \<in> V"

   135   have "0 \<cdot> x = (1 - 1) \<cdot> x" by simp

   136   also have "\<dots> = (1 + - 1) \<cdot> x" by simp

   137   also from x have "\<dots> =  1 \<cdot> x + (- 1) \<cdot> x"

   138     by (rule add_mult_distrib2)

   139   also from x have "\<dots> = x + (- 1) \<cdot> x" by simp

   140   also from x have "\<dots> = x + - x" by (simp add: negate_eq2a)

   141   also from x have "\<dots> = x - x" by (simp add: diff_eq2)

   142   also from x have "\<dots> = 0" by simp

   143   finally show ?thesis .

   144 qed

   145

   146 lemma mult_zero_right [simp]: "a \<cdot> 0 = (0::'a)"

   147 proof -

   148   have "a \<cdot> 0 = a \<cdot> (0 - (0::'a))" by simp

   149   also have "\<dots> =  a \<cdot> 0 - a \<cdot> 0"

   150     by (rule diff_mult_distrib1) simp_all

   151   also have "\<dots> = 0" by simp

   152   finally show ?thesis .

   153 qed

   154

   155 lemma minus_mult_cancel [simp]: "x \<in> V \<Longrightarrow> (- a) \<cdot> - x = a \<cdot> x"

   156   by (simp add: negate_eq1 mult_assoc2)

   157

   158 lemma add_minus_left_eq_diff: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + y = y - x"

   159 proof -

   160   assume xy: "x \<in> V"  "y \<in> V"

   161   then have "- x + y = y + - x" by (simp add: add_commute)

   162   also from xy have "\<dots> = y - x" by (simp add: diff_eq1)

   163   finally show ?thesis .

   164 qed

   165

   166 lemma add_minus [simp]: "x \<in> V \<Longrightarrow> x + - x = 0"

   167   by (simp add: diff_eq2)

   168

   169 lemma add_minus_left [simp]: "x \<in> V \<Longrightarrow> - x + x = 0"

   170   by (simp add: diff_eq2 add_commute)

   171

   172 lemma minus_minus [simp]: "x \<in> V \<Longrightarrow> - (- x) = x"

   173   by (simp add: negate_eq1 mult_assoc2)

   174

   175 lemma minus_zero [simp]: "- (0::'a) = 0"

   176   by (simp add: negate_eq1)

   177

   178 lemma minus_zero_iff [simp]:

   179   assumes x: "x \<in> V"

   180   shows "(- x = 0) = (x = 0)"

   181 proof

   182   from x have "x = - (- x)" by simp

   183   also assume "- x = 0"

   184   also have "- \<dots> = 0" by (rule minus_zero)

   185   finally show "x = 0" .

   186 next

   187   assume "x = 0"

   188   then show "- x = 0" by simp

   189 qed

   190

   191 lemma add_minus_cancel [simp]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + (- x + y) = y"

   192   by (simp add: add_assoc [symmetric])

   193

   194 lemma minus_add_cancel [simp]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + (x + y) = y"

   195   by (simp add: add_assoc [symmetric])

   196

   197 lemma minus_add_distrib [simp]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - (x + y) = - x + - y"

   198   by (simp add: negate_eq1 add_mult_distrib1)

   199

   200 lemma diff_zero [simp]: "x \<in> V \<Longrightarrow> x - 0 = x"

   201   by (simp add: diff_eq1)

   202

   203 lemma diff_zero_right [simp]: "x \<in> V \<Longrightarrow> 0 - x = - x"

   204   by (simp add: diff_eq1)

   205

   206 lemma add_left_cancel:

   207   assumes x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V"

   208   shows "(x + y = x + z) = (y = z)"

   209 proof

   210   from y have "y = 0 + y" by simp

   211   also from x y have "\<dots> = (- x + x) + y" by simp

   212   also from x y have "\<dots> = - x + (x + y)" by (simp add: add_assoc)

   213   also assume "x + y = x + z"

   214   also from x z have "- x + (x + z) = - x + x + z" by (simp add: add_assoc)

   215   also from x z have "\<dots> = z" by simp

   216   finally show "y = z" .

   217 next

   218   assume "y = z"

   219   then show "x + y = x + z" by (simp only:)

   220 qed

   221

   222 lemma add_right_cancel: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)"

   223   by (simp only: add_commute add_left_cancel)

   224

   225 lemma add_assoc_cong:

   226   "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x' \<in> V \<Longrightarrow> y' \<in> V \<Longrightarrow> z \<in> V

   227     \<Longrightarrow> x + y = x' + y' \<Longrightarrow> x + (y + z) = x' + (y' + z)"

   228   by (simp only: add_assoc [symmetric])

   229

   230 lemma mult_left_commute: "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = b \<cdot> a \<cdot> x"

   231   by (simp add: mult_commute mult_assoc2)

   232

   233 lemma mult_zero_uniq:

   234   assumes x: "x \<in> V"  "x \<noteq> 0" and ax: "a \<cdot> x = 0"

   235   shows "a = 0"

   236 proof (rule classical)

   237   assume a: "a \<noteq> 0"

   238   from x a have "x = (inverse a * a) \<cdot> x" by simp

   239   also from x \<in> V have "\<dots> = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc)

   240   also from ax have "\<dots> = inverse a \<cdot> 0" by simp

   241   also have "\<dots> = 0" by simp

   242   finally have "x = 0" .

   243   with x \<noteq> 0 show "a = 0" by contradiction

   244 qed

   245

   246 lemma mult_left_cancel:

   247   assumes x: "x \<in> V" and y: "y \<in> V" and a: "a \<noteq> 0"

   248   shows "(a \<cdot> x = a \<cdot> y) = (x = y)"

   249 proof

   250   from x have "x = 1 \<cdot> x" by simp

   251   also from a have "\<dots> = (inverse a * a) \<cdot> x" by simp

   252   also from x have "\<dots> = inverse a \<cdot> (a \<cdot> x)"

   253     by (simp only: mult_assoc)

   254   also assume "a \<cdot> x = a \<cdot> y"

   255   also from a y have "inverse a \<cdot> \<dots> = y"

   256     by (simp add: mult_assoc2)

   257   finally show "x = y" .

   258 next

   259   assume "x = y"

   260   then show "a \<cdot> x = a \<cdot> y" by (simp only:)

   261 qed

   262

   263 lemma mult_right_cancel:

   264   assumes x: "x \<in> V" and neq: "x \<noteq> 0"

   265   shows "(a \<cdot> x = b \<cdot> x) = (a = b)"

   266 proof

   267   from x have "(a - b) \<cdot> x = a \<cdot> x - b \<cdot> x"

   268     by (simp add: diff_mult_distrib2)

   269   also assume "a \<cdot> x = b \<cdot> x"

   270   with x have "a \<cdot> x - b \<cdot> x = 0" by simp

   271   finally have "(a - b) \<cdot> x = 0" .

   272   with x neq have "a - b = 0" by (rule mult_zero_uniq)

   273   then show "a = b" by simp

   274 next

   275   assume "a = b"

   276   then show "a \<cdot> x = b \<cdot> x" by (simp only:)

   277 qed

   278

   279 lemma eq_diff_eq:

   280   assumes x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V"

   281   shows "(x = z - y) = (x + y = z)"

   282 proof

   283   assume "x = z - y"

   284   then have "x + y = z - y + y" by simp

   285   also from y z have "\<dots> = z + - y + y"

   286     by (simp add: diff_eq1)

   287   also have "\<dots> = z + (- y + y)"

   288     by (rule add_assoc) (simp_all add: y z)

   289   also from y z have "\<dots> = z + 0"

   290     by (simp only: add_minus_left)

   291   also from z have "\<dots> = z"

   292     by (simp only: add_zero_right)

   293   finally show "x + y = z" .

   294 next

   295   assume "x + y = z"

   296   then have "z - y = (x + y) - y" by simp

   297   also from x y have "\<dots> = x + y + - y"

   298     by (simp add: diff_eq1)

   299   also have "\<dots> = x + (y + - y)"

   300     by (rule add_assoc) (simp_all add: x y)

   301   also from x y have "\<dots> = x" by simp

   302   finally show "x = z - y" ..

   303 qed

   304

   305 lemma add_minus_eq_minus:

   306   assumes x: "x \<in> V" and y: "y \<in> V" and xy: "x + y = 0"

   307   shows "x = - y"

   308 proof -

   309   from x y have "x = (- y + y) + x" by simp

   310   also from x y have "\<dots> = - y + (x + y)" by (simp add: add_ac)

   311   also note xy

   312   also from y have "- y + 0 = - y" by simp

   313   finally show "x = - y" .

   314 qed

   315

   316 lemma add_minus_eq:

   317   assumes x: "x \<in> V" and y: "y \<in> V" and xy: "x - y = 0"

   318   shows "x = y"

   319 proof -

   320   from x y xy have eq: "x + - y = 0" by (simp add: diff_eq1)

   321   with _ _ have "x = - (- y)"

   322     by (rule add_minus_eq_minus) (simp_all add: x y)

   323   with x y show "x = y" by simp

   324 qed

   325

   326 lemma add_diff_swap:

   327   assumes vs: "a \<in> V"  "b \<in> V"  "c \<in> V"  "d \<in> V"

   328     and eq: "a + b = c + d"

   329   shows "a - c = d - b"

   330 proof -

   331   from assms have "- c + (a + b) = - c + (c + d)"

   332     by (simp add: add_left_cancel)

   333   also have "\<dots> = d" using c \<in> V d \<in> V by (rule minus_add_cancel)

   334   finally have eq: "- c + (a + b) = d" .

   335   from vs have "a - c = (- c + (a + b)) + - b"

   336     by (simp add: add_ac diff_eq1)

   337   also from vs eq have "\<dots>  = d + - b"

   338     by (simp add: add_right_cancel)

   339   also from vs have "\<dots> = d - b" by (simp add: diff_eq2)

   340   finally show "a - c = d - b" .

   341 qed

   342

   343 lemma vs_add_cancel_21:

   344   assumes vs: "x \<in> V"  "y \<in> V"  "z \<in> V"  "u \<in> V"

   345   shows "(x + (y + z) = y + u) = (x + z = u)"

   346 proof

   347   from vs have "x + z = - y + y + (x + z)" by simp

   348   also have "\<dots> = - y + (y + (x + z))"

   349     by (rule add_assoc) (simp_all add: vs)

   350   also from vs have "y + (x + z) = x + (y + z)"

   351     by (simp add: add_ac)

   352   also assume "x + (y + z) = y + u"

   353   also from vs have "- y + (y + u) = u" by simp

   354   finally show "x + z = u" .

   355 next

   356   assume "x + z = u"

   357   with vs show "x + (y + z) = y + u"

   358     by (simp only: add_left_commute [of x])

   359 qed

   360

   361 lemma add_cancel_end:

   362   assumes vs: "x \<in> V"  "y \<in> V"  "z \<in> V"

   363   shows "(x + (y + z) = y) = (x = - z)"

   364 proof

   365   assume "x + (y + z) = y"

   366   with vs have "(x + z) + y = 0 + y" by (simp add: add_ac)

   367   with vs have "x + z = 0" by (simp only: add_right_cancel add_closed zero)

   368   with vs show "x = - z" by (simp add: add_minus_eq_minus)

   369 next

   370   assume eq: "x = - z"

   371   then have "x + (y + z) = - z + (y + z)" by simp

   372   also have "\<dots> = y + (- z + z)" by (rule add_left_commute) (simp_all add: vs)

   373   also from vs have "\<dots> = y"  by simp

   374   finally show "x + (y + z) = y" .

   375 qed

   376

   377 end

   378

   379 end

   380