src/HOL/Hahn_Banach/Vector_Space.thy
author haftmann
Fri Jul 04 20:18:47 2014 +0200 (2014-07-04)
changeset 57512 cc97b347b301
parent 55018 2a526bd279ed
child 58744 c434e37f290e
permissions -rw-r--r--
reduced name variants for assoc and commute on plus and mult
     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