src/HOL/Hahn_Banach/Vector_Space.thy
 author paulson Mon May 23 15:33:24 2016 +0100 (2016-05-23) changeset 63114 27afe7af7379 parent 61879 e4f9d8f094fe child 69597 ff784d5a5bfb permissions -rw-r--r--
Lots of new material for multivariate analysis
```     1 (*  Title:      HOL/Hahn_Banach/Vector_Space.thy
```
```     2     Author:     Gertrud Bauer, TU Munich
```
```     3 *)
```
```     4
```
```     5 section \<open>Vector spaces\<close>
```
```     6
```
```     7 theory Vector_Space
```
```     8 imports Complex_Main Bounds
```
```     9 begin
```
```    10
```
```    11 subsection \<open>Signature\<close>
```
```    12
```
```    13 text \<open>
```
```    14   For the definition of real vector spaces a type @{typ 'a} of the sort
```
```    15   \<open>{plus, minus, zero}\<close> is considered, on which a real scalar multiplication
```
```    16   \<open>\<cdot>\<close> is declared.
```
```    17 \<close>
```
```    18
```
```    19 consts
```
```    20   prod :: "real \<Rightarrow> 'a::{plus,minus,zero} \<Rightarrow> 'a"  (infixr "\<cdot>" 70)
```
```    21
```
```    22
```
```    23 subsection \<open>Vector space laws\<close>
```
```    24
```
```    25 text \<open>
```
```    26   A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from @{typ 'a} with the
```
```    27   following vector space laws: The set \<open>V\<close> is closed under addition and scalar
```
```    28   multiplication, addition is associative and commutative; \<open>- x\<close> is the
```
```    29   inverse of \<open>x\<close> wrt.\ addition and \<open>0\<close> is the neutral element of addition.
```
```    30   Addition and multiplication are distributive; scalar multiplication is
```
```    31   associative and the real number \<open>1\<close> is the neutral element of scalar
```
```    32   multiplication.
```
```    33 \<close>
```
```    34
```
```    35 locale vectorspace =
```
```    36   fixes V
```
```    37   assumes non_empty [iff, intro?]: "V \<noteq> {}"
```
```    38     and add_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y \<in> V"
```
```    39     and mult_closed [iff]: "x \<in> V \<Longrightarrow> a \<cdot> x \<in> V"
```
```    40     and add_assoc: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (x + y) + z = x + (y + z)"
```
```    41     and add_commute: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y = y + x"
```
```    42     and diff_self [simp]: "x \<in> V \<Longrightarrow> x - x = 0"
```
```    43     and add_zero_left [simp]: "x \<in> V \<Longrightarrow> 0 + x = x"
```
```    44     and add_mult_distrib1: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y"
```
```    45     and add_mult_distrib2: "x \<in> V \<Longrightarrow> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x"
```
```    46     and mult_assoc: "x \<in> V \<Longrightarrow> (a * b) \<cdot> x = a \<cdot> (b \<cdot> x)"
```
```    47     and mult_1 [simp]: "x \<in> V \<Longrightarrow> 1 \<cdot> x = x"
```
```    48     and negate_eq1: "x \<in> V \<Longrightarrow> - x = (- 1) \<cdot> x"
```
```    49     and diff_eq1: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y = x + - y"
```
```    50 begin
```
```    51
```
```    52 lemma negate_eq2: "x \<in> V \<Longrightarrow> (- 1) \<cdot> x = - x"
```
```    53   by (rule negate_eq1 [symmetric])
```
```    54
```
```    55 lemma negate_eq2a: "x \<in> V \<Longrightarrow> -1 \<cdot> x = - x"
```
```    56   by (simp add: negate_eq1)
```
```    57
```
```    58 lemma diff_eq2: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + - y = x - y"
```
```    59   by (rule diff_eq1 [symmetric])
```
```    60
```
```    61 lemma diff_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y \<in> V"
```
```    62   by (simp add: diff_eq1 negate_eq1)
```
```    63
```
```    64 lemma neg_closed [iff]: "x \<in> V \<Longrightarrow> - x \<in> V"
```
```    65   by (simp add: negate_eq1)
```
```    66
```
```    67 lemma add_left_commute:
```
```    68   "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)"
```
```    69 proof -
```
```    70   assume xyz: "x \<in> V"  "y \<in> V"  "z \<in> V"
```
```    71   then have "x + (y + z) = (x + y) + z"
```
```    72     by (simp only: add_assoc)
```
```    73   also from xyz have "\<dots> = (y + x) + z" by (simp only: add_commute)
```
```    74   also from xyz have "\<dots> = y + (x + z)" by (simp only: add_assoc)
```
```    75   finally show ?thesis .
```
```    76 qed
```
```    77
```
```    78 lemmas add_ac = add_assoc add_commute add_left_commute
```
```    79
```
```    80
```
```    81 text \<open>
```
```    82   The existence of the zero element of a vector space follows from the
```
```    83   non-emptiness of carrier set.
```
```    84 \<close>
```
```    85
```
```    86 lemma zero [iff]: "0 \<in> V"
```
```    87 proof -
```
```    88   from non_empty obtain x where x: "x \<in> V" by blast
```
```    89   then have "0 = x - x" by (rule diff_self [symmetric])
```
```    90   also from x x have "\<dots> \<in> V" by (rule diff_closed)
```
```    91   finally show ?thesis .
```
```    92 qed
```
```    93
```
```    94 lemma add_zero_right [simp]: "x \<in> V \<Longrightarrow>  x + 0 = x"
```
```    95 proof -
```
```    96   assume x: "x \<in> V"
```
```    97   from this and zero have "x + 0 = 0 + x" by (rule add_commute)
```
```    98   also from x have "\<dots> = x" by (rule add_zero_left)
```
```    99   finally show ?thesis .
```
```   100 qed
```
```   101
```
```   102 lemma mult_assoc2: "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = (a * b) \<cdot> x"
```
```   103   by (simp only: mult_assoc)
```
```   104
```
```   105 lemma diff_mult_distrib1: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<cdot> (x - y) = a \<cdot> x - a \<cdot> y"
```
```   106   by (simp add: diff_eq1 negate_eq1 add_mult_distrib1 mult_assoc2)
```
```   107
```
```   108 lemma diff_mult_distrib2: "x \<in> V \<Longrightarrow> (a - b) \<cdot> x = a \<cdot> x - (b \<cdot> x)"
```
```   109 proof -
```
```   110   assume x: "x \<in> V"
```
```   111   have " (a - b) \<cdot> x = (a + - b) \<cdot> x"
```
```   112     by simp
```
```   113   also from x have "\<dots> = a \<cdot> x + (- b) \<cdot> x"
```
```   114     by (rule add_mult_distrib2)
```
```   115   also from x have "\<dots> = a \<cdot> x + - (b \<cdot> x)"
```
```   116     by (simp add: negate_eq1 mult_assoc2)
```
```   117   also from x have "\<dots> = a \<cdot> x - (b \<cdot> x)"
```
```   118     by (simp add: diff_eq1)
```
```   119   finally show ?thesis .
```
```   120 qed
```
```   121
```
```   122 lemmas distrib =
```
```   123   add_mult_distrib1 add_mult_distrib2
```
```   124   diff_mult_distrib1 diff_mult_distrib2
```
```   125
```
```   126
```
```   127 text \<open>\<^medskip> Further derived laws:\<close>
```
```   128
```
```   129 lemma mult_zero_left [simp]: "x \<in> V \<Longrightarrow> 0 \<cdot> x = 0"
```
```   130 proof -
```
```   131   assume x: "x \<in> V"
```
```   132   have "0 \<cdot> x = (1 - 1) \<cdot> x" by simp
```
```   133   also have "\<dots> = (1 + - 1) \<cdot> x" by simp
```
```   134   also from x have "\<dots> =  1 \<cdot> x + (- 1) \<cdot> x"
```
```   135     by (rule add_mult_distrib2)
```
```   136   also from x have "\<dots> = x + (- 1) \<cdot> x" by simp
```
```   137   also from x have "\<dots> = x + - x" by (simp add: negate_eq2a)
```
```   138   also from x have "\<dots> = x - x" by (simp add: diff_eq2)
```
```   139   also from x have "\<dots> = 0" by simp
```
```   140   finally show ?thesis .
```
```   141 qed
```
```   142
```
```   143 lemma mult_zero_right [simp]: "a \<cdot> 0 = (0::'a)"
```
```   144 proof -
```
```   145   have "a \<cdot> 0 = a \<cdot> (0 - (0::'a))" by simp
```
```   146   also have "\<dots> =  a \<cdot> 0 - a \<cdot> 0"
```
```   147     by (rule diff_mult_distrib1) simp_all
```
```   148   also have "\<dots> = 0" by simp
```
```   149   finally show ?thesis .
```
```   150 qed
```
```   151
```
```   152 lemma minus_mult_cancel [simp]: "x \<in> V \<Longrightarrow> (- a) \<cdot> - x = a \<cdot> x"
```
```   153   by (simp add: negate_eq1 mult_assoc2)
```
```   154
```
```   155 lemma add_minus_left_eq_diff: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + y = y - x"
```
```   156 proof -
```
```   157   assume xy: "x \<in> V"  "y \<in> V"
```
```   158   then have "- x + y = y + - x" by (simp add: add_commute)
```
```   159   also from xy have "\<dots> = y - x" by (simp add: diff_eq1)
```
```   160   finally show ?thesis .
```
```   161 qed
```
```   162
```
```   163 lemma add_minus [simp]: "x \<in> V \<Longrightarrow> x + - x = 0"
```
```   164   by (simp add: diff_eq2)
```
```   165
```
```   166 lemma add_minus_left [simp]: "x \<in> V \<Longrightarrow> - x + x = 0"
```
```   167   by (simp add: diff_eq2 add_commute)
```
```   168
```
```   169 lemma minus_minus [simp]: "x \<in> V \<Longrightarrow> - (- x) = x"
```
```   170   by (simp add: negate_eq1 mult_assoc2)
```
```   171
```
```   172 lemma minus_zero [simp]: "- (0::'a) = 0"
```
```   173   by (simp add: negate_eq1)
```
```   174
```
```   175 lemma minus_zero_iff [simp]:
```
```   176   assumes x: "x \<in> V"
```
```   177   shows "(- x = 0) = (x = 0)"
```
```   178 proof
```
```   179   from x have "x = - (- x)" by simp
```
```   180   also assume "- x = 0"
```
```   181   also have "- \<dots> = 0" by (rule minus_zero)
```
```   182   finally show "x = 0" .
```
```   183 next
```
```   184   assume "x = 0"
```
```   185   then show "- x = 0" by simp
```
```   186 qed
```
```   187
```
```   188 lemma add_minus_cancel [simp]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + (- x + y) = y"
```
```   189   by (simp add: add_assoc [symmetric])
```
```   190
```
```   191 lemma minus_add_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_distrib [simp]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - (x + y) = - x + - y"
```
```   195   by (simp add: negate_eq1 add_mult_distrib1)
```
```   196
```
```   197 lemma diff_zero [simp]: "x \<in> V \<Longrightarrow> x - 0 = x"
```
```   198   by (simp add: diff_eq1)
```
```   199
```
```   200 lemma diff_zero_right [simp]: "x \<in> V \<Longrightarrow> 0 - x = - x"
```
```   201   by (simp add: diff_eq1)
```
```   202
```
```   203 lemma add_left_cancel:
```
```   204   assumes x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V"
```
```   205   shows "(x + y = x + z) = (y = z)"
```
```   206 proof
```
```   207   from y have "y = 0 + y" by simp
```
```   208   also from x y have "\<dots> = (- x + x) + y" by simp
```
```   209   also from x y have "\<dots> = - x + (x + y)" by (simp add: add.assoc)
```
```   210   also assume "x + y = x + z"
```
```   211   also from x z have "- x + (x + z) = - x + x + z" by (simp add: add.assoc)
```
```   212   also from x z have "\<dots> = z" by simp
```
```   213   finally show "y = z" .
```
```   214 next
```
```   215   assume "y = z"
```
```   216   then show "x + y = x + z" by (simp only:)
```
```   217 qed
```
```   218
```
```   219 lemma add_right_cancel:
```
```   220     "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)"
```
```   221   by (simp only: add_commute add_left_cancel)
```
```   222
```
```   223 lemma add_assoc_cong:
```
```   224   "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x' \<in> V \<Longrightarrow> y' \<in> V \<Longrightarrow> z \<in> V
```
```   225     \<Longrightarrow> x + y = x' + y' \<Longrightarrow> x + (y + z) = x' + (y' + z)"
```
```   226   by (simp only: add_assoc [symmetric])
```
```   227
```
```   228 lemma mult_left_commute: "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = b \<cdot> a \<cdot> x"
```
```   229   by (simp add: mult.commute mult_assoc2)
```
```   230
```
```   231 lemma mult_zero_uniq:
```
```   232   assumes x: "x \<in> V"  "x \<noteq> 0" and ax: "a \<cdot> x = 0"
```
```   233   shows "a = 0"
```
```   234 proof (rule classical)
```
```   235   assume a: "a \<noteq> 0"
```
```   236   from x a have "x = (inverse a * a) \<cdot> x" by simp
```
```   237   also from \<open>x \<in> V\<close> have "\<dots> = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc)
```
```   238   also from ax have "\<dots> = inverse a \<cdot> 0" by simp
```
```   239   also have "\<dots> = 0" by simp
```
```   240   finally have "x = 0" .
```
```   241   with \<open>x \<noteq> 0\<close> show "a = 0" by contradiction
```
```   242 qed
```
```   243
```
```   244 lemma mult_left_cancel:
```
```   245   assumes x: "x \<in> V" and y: "y \<in> V" and a: "a \<noteq> 0"
```
```   246   shows "(a \<cdot> x = a \<cdot> y) = (x = y)"
```
```   247 proof
```
```   248   from x have "x = 1 \<cdot> x" by simp
```
```   249   also from a have "\<dots> = (inverse a * a) \<cdot> x" by simp
```
```   250   also from x have "\<dots> = inverse a \<cdot> (a \<cdot> x)"
```
```   251     by (simp only: mult_assoc)
```
```   252   also assume "a \<cdot> x = a \<cdot> y"
```
```   253   also from a y have "inverse a \<cdot> \<dots> = y"
```
```   254     by (simp add: mult_assoc2)
```
```   255   finally show "x = y" .
```
```   256 next
```
```   257   assume "x = y"
```
```   258   then show "a \<cdot> x = a \<cdot> y" by (simp only:)
```
```   259 qed
```
```   260
```
```   261 lemma mult_right_cancel:
```
```   262   assumes x: "x \<in> V" and neq: "x \<noteq> 0"
```
```   263   shows "(a \<cdot> x = b \<cdot> x) = (a = b)"
```
```   264 proof
```
```   265   from x have "(a - b) \<cdot> x = a \<cdot> x - b \<cdot> x"
```
```   266     by (simp add: diff_mult_distrib2)
```
```   267   also assume "a \<cdot> x = b \<cdot> x"
```
```   268   with x have "a \<cdot> x - b \<cdot> x = 0" by simp
```
```   269   finally have "(a - b) \<cdot> x = 0" .
```
```   270   with x neq have "a - b = 0" by (rule mult_zero_uniq)
```
```   271   then show "a = b" by simp
```
```   272 next
```
```   273   assume "a = b"
```
```   274   then show "a \<cdot> x = b \<cdot> x" by (simp only:)
```
```   275 qed
```
```   276
```
```   277 lemma eq_diff_eq:
```
```   278   assumes x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V"
```
```   279   shows "(x = z - y) = (x + y = z)"
```
```   280 proof
```
```   281   assume "x = z - y"
```
```   282   then have "x + y = z - y + y" by simp
```
```   283   also from y z have "\<dots> = z + - y + y"
```
```   284     by (simp add: diff_eq1)
```
```   285   also have "\<dots> = z + (- y + y)"
```
```   286     by (rule add_assoc) (simp_all add: y z)
```
```   287   also from y z have "\<dots> = z + 0"
```
```   288     by (simp only: add_minus_left)
```
```   289   also from z have "\<dots> = z"
```
```   290     by (simp only: add_zero_right)
```
```   291   finally show "x + y = z" .
```
```   292 next
```
```   293   assume "x + y = z"
```
```   294   then have "z - y = (x + y) - y" by simp
```
```   295   also from x y have "\<dots> = x + y + - y"
```
```   296     by (simp add: diff_eq1)
```
```   297   also have "\<dots> = x + (y + - y)"
```
```   298     by (rule add_assoc) (simp_all add: x y)
```
```   299   also from x y have "\<dots> = x" by simp
```
```   300   finally show "x = z - y" ..
```
```   301 qed
```
```   302
```
```   303 lemma add_minus_eq_minus:
```
```   304   assumes x: "x \<in> V" and y: "y \<in> V" and xy: "x + y = 0"
```
```   305   shows "x = - y"
```
```   306 proof -
```
```   307   from x y have "x = (- y + y) + x" by simp
```
```   308   also from x y have "\<dots> = - y + (x + y)" by (simp add: add_ac)
```
```   309   also note xy
```
```   310   also from y have "- y + 0 = - y" by simp
```
```   311   finally show "x = - y" .
```
```   312 qed
```
```   313
```
```   314 lemma add_minus_eq:
```
```   315   assumes x: "x \<in> V" and y: "y \<in> V" and xy: "x - y = 0"
```
```   316   shows "x = y"
```
```   317 proof -
```
```   318   from x y xy have eq: "x + - y = 0" by (simp add: diff_eq1)
```
```   319   with _ _ have "x = - (- y)"
```
```   320     by (rule add_minus_eq_minus) (simp_all add: x y)
```
```   321   with x y show "x = y" by simp
```
```   322 qed
```
```   323
```
```   324 lemma add_diff_swap:
```
```   325   assumes vs: "a \<in> V"  "b \<in> V"  "c \<in> V"  "d \<in> V"
```
```   326     and eq: "a + b = c + d"
```
```   327   shows "a - c = d - b"
```
```   328 proof -
```
```   329   from assms have "- c + (a + b) = - c + (c + d)"
```
```   330     by (simp add: add_left_cancel)
```
```   331   also have "\<dots> = d" using \<open>c \<in> V\<close> \<open>d \<in> V\<close> by (rule minus_add_cancel)
```
```   332   finally have eq: "- c + (a + b) = d" .
```
```   333   from vs have "a - c = (- c + (a + b)) + - b"
```
```   334     by (simp add: add_ac diff_eq1)
```
```   335   also from vs eq have "\<dots>  = d + - b"
```
```   336     by (simp add: add_right_cancel)
```
```   337   also from vs have "\<dots> = d - b" by (simp add: diff_eq2)
```
```   338   finally show "a - c = d - b" .
```
```   339 qed
```
```   340
```
```   341 lemma vs_add_cancel_21:
```
```   342   assumes vs: "x \<in> V"  "y \<in> V"  "z \<in> V"  "u \<in> V"
```
```   343   shows "(x + (y + z) = y + u) = (x + z = u)"
```
```   344 proof
```
```   345   from vs have "x + z = - y + y + (x + z)" by simp
```
```   346   also have "\<dots> = - y + (y + (x + z))"
```
```   347     by (rule add_assoc) (simp_all add: vs)
```
```   348   also from vs have "y + (x + z) = x + (y + z)"
```
```   349     by (simp add: add_ac)
```
```   350   also assume "x + (y + z) = y + u"
```
```   351   also from vs have "- y + (y + u) = u" by simp
```
```   352   finally show "x + z = u" .
```
```   353 next
```
```   354   assume "x + z = u"
```
```   355   with vs show "x + (y + z) = y + u"
```
```   356     by (simp only: add_left_commute [of x])
```
```   357 qed
```
```   358
```
```   359 lemma add_cancel_end:
```
```   360   assumes vs: "x \<in> V"  "y \<in> V"  "z \<in> V"
```
```   361   shows "(x + (y + z) = y) = (x = - z)"
```
```   362 proof
```
```   363   assume "x + (y + z) = y"
```
```   364   with vs have "(x + z) + y = 0 + y" by (simp add: add_ac)
```
```   365   with vs have "x + z = 0" by (simp only: add_right_cancel add_closed zero)
```
```   366   with vs show "x = - z" by (simp add: add_minus_eq_minus)
```
```   367 next
```
```   368   assume eq: "x = - z"
```
```   369   then have "x + (y + z) = - z + (y + z)" by simp
```
```   370   also have "\<dots> = y + (- z + z)" by (rule add_left_commute) (simp_all add: vs)
```
```   371   also from vs have "\<dots> = y"  by simp
```
```   372   finally show "x + (y + z) = y" .
```
```   373 qed
```
```   374
```
```   375 end
```
```   376
```
```   377 end
```