src/HOL/Hahn_Banach/Vector_Space.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46867 0883804b67bb
child 54230 b1d955791529
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31795
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 29252
diff changeset
     1
(*  Title:      HOL/Hahn_Banach/Vector_Space.thy
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
     2
    Author:     Gertrud Bauer, TU Munich
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
     3
*)
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
     4
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
     5
header {* Vector spaces *}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
     6
31795
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 29252
diff changeset
     7
theory Vector_Space
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
     8
imports Complex_Main Bounds "~~/src/HOL/Library/Zorn"
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
     9
begin
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    10
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    11
subsection {* Signature *}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    12
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10683
diff changeset
    13
text {*
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10683
diff changeset
    14
  For the definition of real vector spaces a type @{typ 'a} of the
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10683
diff changeset
    15
  sort @{text "{plus, minus, zero}"} is considered, on which a real
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10683
diff changeset
    16
  scalar multiplication @{text \<cdot>} is declared.
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10683
diff changeset
    17
*}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    18
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    19
consts
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10683
diff changeset
    20
  prod  :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a"     (infixr "'(*')" 70)
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    21
21210
c17fd2df4e9e renamed 'const_syntax' to 'notation';
wenzelm
parents: 19736
diff changeset
    22
notation (xsymbols)
19736
wenzelm
parents: 16417
diff changeset
    23
  prod  (infixr "\<cdot>" 70)
21210
c17fd2df4e9e renamed 'const_syntax' to 'notation';
wenzelm
parents: 19736
diff changeset
    24
notation (HTML output)
19736
wenzelm
parents: 16417
diff changeset
    25
  prod  (infixr "\<cdot>" 70)
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    26
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    27
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    28
subsection {* Vector space laws *}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    29
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10683
diff changeset
    30
text {*
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10683
diff changeset
    31
  A \emph{vector space} is a non-empty set @{text V} of elements from
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10683
diff changeset
    32
  @{typ 'a} with the following vector space laws: The set @{text V} is
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10683
diff changeset
    33
  closed under addition and scalar multiplication, addition is
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10683
diff changeset
    34
  associative and commutative; @{text "- x"} is the inverse of @{text
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10683
diff changeset
    35
  x} w.~r.~t.~addition and @{text 0} is the neutral element of
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10683
diff changeset
    36
  addition.  Addition and multiplication are distributive; scalar
12018
ec054019c910 Numerals and simprocs for types real and hypreal. The abstract
paulson
parents: 11704
diff changeset
    37
  multiplication is associative and the real number @{text "1"} is
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10683
diff changeset
    38
  the neutral element of scalar multiplication.
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    39
*}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    40
46867
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
    41
locale vectorspace =
0883804b67bb modernized locale expression, with some fluctuation of arguments;
wenzelm
parents: 44887
diff changeset
    42
  fixes V
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
    43
  assumes non_empty [iff, intro?]: "V \<noteq> {}"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
    44
    and add_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y \<in> V"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
    45
    and mult_closed [iff]: "x \<in> V \<Longrightarrow> a \<cdot> x \<in> V"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
    46
    and add_assoc: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (x + y) + z = x + (y + z)"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
    47
    and add_commute: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y = y + x"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
    48
    and diff_self [simp]: "x \<in> V \<Longrightarrow> x - x = 0"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
    49
    and add_zero_left [simp]: "x \<in> V \<Longrightarrow> 0 + x = x"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
    50
    and add_mult_distrib1: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
    51
    and add_mult_distrib2: "x \<in> V \<Longrightarrow> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
    52
    and mult_assoc: "x \<in> V \<Longrightarrow> (a * b) \<cdot> x = a \<cdot> (b \<cdot> x)"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
    53
    and mult_1 [simp]: "x \<in> V \<Longrightarrow> 1 \<cdot> x = x"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
    54
    and negate_eq1: "x \<in> V \<Longrightarrow> - x = (- 1) \<cdot> x"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
    55
    and diff_eq1: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y = x + - y"
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
    56
begin
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    57
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
    58
lemma negate_eq2: "x \<in> V \<Longrightarrow> (- 1) \<cdot> x = - x"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
    59
  by (rule negate_eq1 [symmetric])
9013
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents: 8703
diff changeset
    60
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
    61
lemma negate_eq2a: "x \<in> V \<Longrightarrow> -1 \<cdot> x = - x"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
    62
  by (simp add: negate_eq1)
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    63
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
    64
lemma diff_eq2: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + - y = x - y"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
    65
  by (rule diff_eq1 [symmetric])
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    66
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
    67
lemma diff_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y \<in> V"
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    68
  by (simp add: diff_eq1 negate_eq1)
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    69
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
    70
lemma neg_closed [iff]: "x \<in> V \<Longrightarrow> - x \<in> V"
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    71
  by (simp add: negate_eq1)
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    72
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
    73
lemma add_left_commute: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)"
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    74
proof -
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
    75
  assume xyz: "x \<in> V"  "y \<in> V"  "z \<in> V"
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
    76
  then have "x + (y + z) = (x + y) + z"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
    77
    by (simp only: add_assoc)
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
    78
  also from xyz have "\<dots> = (y + x) + z" by (simp only: add_commute)
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
    79
  also from xyz have "\<dots> = y + (x + z)" by (simp only: add_assoc)
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    80
  finally show ?thesis .
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    81
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    82
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
    83
theorems add_ac = add_assoc add_commute add_left_commute
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    84
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    85
7978
1b99ee57d131 final update by Gertrud Bauer;
wenzelm
parents: 7927
diff changeset
    86
text {* The existence of the zero element of a vector space
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
    87
  follows from the non-emptiness of carrier set. *}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    88
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
    89
lemma zero [iff]: "0 \<in> V"
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10683
diff changeset
    90
proof -
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
    91
  from non_empty obtain x where x: "x \<in> V" by blast
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
    92
  then have "0 = x - x" by (rule diff_self [symmetric])
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
    93
  also from x x have "\<dots> \<in> V" by (rule diff_closed)
11472
wenzelm
parents: 10687
diff changeset
    94
  finally show ?thesis .
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    95
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    96
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
    97
lemma add_zero_right [simp]: "x \<in> V \<Longrightarrow>  x + 0 = x"
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    98
proof -
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
    99
  assume x: "x \<in> V"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   100
  from this and zero have "x + 0 = 0 + x" by (rule add_commute)
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   101
  also from x have "\<dots> = x" by (rule add_zero_left)
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   102
  finally show ?thesis .
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   103
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   104
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   105
lemma mult_assoc2: "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = (a * b) \<cdot> x"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   106
  by (simp only: mult_assoc)
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   107
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   108
lemma diff_mult_distrib1: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<cdot> (x - y) = a \<cdot> x - a \<cdot> y"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   109
  by (simp add: diff_eq1 negate_eq1 add_mult_distrib1 mult_assoc2)
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   110
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   111
lemma diff_mult_distrib2: "x \<in> V \<Longrightarrow> (a - b) \<cdot> x = a \<cdot> x - (b \<cdot> x)"
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   112
proof -
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   113
  assume x: "x \<in> V"
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10683
diff changeset
   114
  have " (a - b) \<cdot> x = (a + - b) \<cdot> x"
37887
2ae085b07f2f diff_minus subsumes diff_def
haftmann
parents: 36778
diff changeset
   115
    by (simp add: diff_minus)
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   116
  also from x have "\<dots> = a \<cdot> x + (- b) \<cdot> x"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   117
    by (rule add_mult_distrib2)
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   118
  also from x have "\<dots> = a \<cdot> x + - (b \<cdot> x)"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   119
    by (simp add: negate_eq1 mult_assoc2)
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   120
  also from x have "\<dots> = a \<cdot> x - (b \<cdot> x)"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   121
    by (simp add: diff_eq1)
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   122
  finally show ?thesis .
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   123
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   124
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   125
lemmas distrib =
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   126
  add_mult_distrib1 add_mult_distrib2
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   127
  diff_mult_distrib1 diff_mult_distrib2
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   128
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10683
diff changeset
   129
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10683
diff changeset
   130
text {* \medskip Further derived laws: *}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   131
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   132
lemma mult_zero_left [simp]: "x \<in> V \<Longrightarrow> 0 \<cdot> x = 0"
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   133
proof -
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   134
  assume x: "x \<in> V"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   135
  have "0 \<cdot> x = (1 - 1) \<cdot> x" by simp
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   136
  also have "\<dots> = (1 + - 1) \<cdot> x" by simp
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   137
  also from x have "\<dots> =  1 \<cdot> x + (- 1) \<cdot> x"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   138
    by (rule add_mult_distrib2)
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   139
  also from x have "\<dots> = x + (- 1) \<cdot> x" by simp
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   140
  also from x have "\<dots> = x + - x" by (simp add: negate_eq2a)
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   141
  also from x have "\<dots> = x - x" by (simp add: diff_eq2)
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   142
  also from x have "\<dots> = 0" by simp
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   143
  finally show ?thesis .
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   144
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   145
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   146
lemma mult_zero_right [simp]: "a \<cdot> 0 = (0::'a)"
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   147
proof -
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   148
  have "a \<cdot> 0 = a \<cdot> (0 - (0::'a))" by simp
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   149
  also have "\<dots> =  a \<cdot> 0 - a \<cdot> 0"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   150
    by (rule diff_mult_distrib1) simp_all
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   151
  also have "\<dots> = 0" by simp
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   152
  finally show ?thesis .
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   153
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   154
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   155
lemma minus_mult_cancel [simp]: "x \<in> V \<Longrightarrow> (- a) \<cdot> - x = a \<cdot> x"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   156
  by (simp add: negate_eq1 mult_assoc2)
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   157
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   158
lemma add_minus_left_eq_diff: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + y = y - x"
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10683
diff changeset
   159
proof -
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   160
  assume xy: "x \<in> V"  "y \<in> V"
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   161
  then have "- x + y = y + - x" by (simp add: add_commute)
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   162
  also from xy have "\<dots> = y - x" by (simp add: diff_eq1)
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   163
  finally show ?thesis .
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   164
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   165
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   166
lemma add_minus [simp]: "x \<in> V \<Longrightarrow> x + - x = 0"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   167
  by (simp add: diff_eq2)
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   168
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   169
lemma add_minus_left [simp]: "x \<in> V \<Longrightarrow> - x + x = 0"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   170
  by (simp add: diff_eq2 add_commute)
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   171
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   172
lemma minus_minus [simp]: "x \<in> V \<Longrightarrow> - (- x) = x"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   173
  by (simp add: negate_eq1 mult_assoc2)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   174
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   175
lemma minus_zero [simp]: "- (0::'a) = 0"
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   176
  by (simp add: negate_eq1)
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   177
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   178
lemma minus_zero_iff [simp]:
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   179
  assumes x: "x \<in> V"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   180
  shows "(- x = 0) = (x = 0)"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   181
proof
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   182
  from x have "x = - (- x)" by simp
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   183
  also assume "- x = 0"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   184
  also have "- \<dots> = 0" by (rule minus_zero)
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   185
  finally show "x = 0" .
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   186
next
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   187
  assume "x = 0"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   188
  then show "- x = 0" by simp
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   189
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   190
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   191
lemma add_minus_cancel [simp]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + (- x + y) = y"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   192
  by (simp add: add_assoc [symmetric])
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   193
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   194
lemma minus_add_cancel [simp]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + (x + y) = y"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   195
  by (simp add: add_assoc [symmetric])
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   196
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   197
lemma minus_add_distrib [simp]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - (x + y) = - x + - y"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   198
  by (simp add: negate_eq1 add_mult_distrib1)
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   199
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   200
lemma diff_zero [simp]: "x \<in> V \<Longrightarrow> x - 0 = x"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   201
  by (simp add: diff_eq1)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   202
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   203
lemma diff_zero_right [simp]: "x \<in> V \<Longrightarrow> 0 - x = - x"
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10683
diff changeset
   204
  by (simp add: diff_eq1)
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   205
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   206
lemma add_left_cancel:
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   207
  assumes x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   208
  shows "(x + y = x + z) = (y = z)"
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   209
proof
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   210
  from y have "y = 0 + y" by simp
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   211
  also from x y have "\<dots> = (- x + x) + y" by simp
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   212
  also from x y have "\<dots> = - x + (x + y)" by (simp add: add_assoc)
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   213
  also assume "x + y = x + z"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   214
  also from x z have "- x + (x + z) = - x + x + z" by (simp add: add_assoc)
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   215
  also from x z have "\<dots> = z" by simp
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   216
  finally show "y = z" .
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   217
next
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   218
  assume "y = z"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   219
  then show "x + y = x + z" by (simp only:)
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   220
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   221
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   222
lemma add_right_cancel: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   223
  by (simp only: add_commute add_left_cancel)
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   224
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   225
lemma add_assoc_cong:
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   226
  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x' \<in> V \<Longrightarrow> y' \<in> V \<Longrightarrow> z \<in> V
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   227
    \<Longrightarrow> x + y = x' + y' \<Longrightarrow> x + (y + z) = x' + (y' + z)"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   228
  by (simp only: add_assoc [symmetric])
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   229
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   230
lemma mult_left_commute: "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = b \<cdot> a \<cdot> x"
36778
739a9379e29b avoid using real-specific versions of generic lemmas
huffman
parents: 31795
diff changeset
   231
  by (simp add: mult_commute mult_assoc2)
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   232
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   233
lemma mult_zero_uniq:
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   234
  assumes x: "x \<in> V"  "x \<noteq> 0" and ax: "a \<cdot> x = 0"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   235
  shows "a = 0"
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   236
proof (rule classical)
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   237
  assume a: "a \<noteq> 0"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   238
  from x a have "x = (inverse a * a) \<cdot> x" by simp
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   239
  also from `x \<in> V` have "\<dots> = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc)
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   240
  also from ax have "\<dots> = inverse a \<cdot> 0" by simp
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   241
  also have "\<dots> = 0" by simp
9374
153853af318b - xsymbols for
bauerg
parents: 9035
diff changeset
   242
  finally have "x = 0" .
23378
1d138d6bb461 tuned proofs: avoid implicit prems;
wenzelm
parents: 21210
diff changeset
   243
  with `x \<noteq> 0` show "a = 0" by contradiction
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   244
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   245
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   246
lemma mult_left_cancel:
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   247
  assumes x: "x \<in> V" and y: "y \<in> V" and a: "a \<noteq> 0"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   248
  shows "(a \<cdot> x = a \<cdot> y) = (x = y)"
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   249
proof
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   250
  from x have "x = 1 \<cdot> x" by simp
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   251
  also from a have "\<dots> = (inverse a * a) \<cdot> x" by simp
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   252
  also from x have "\<dots> = inverse a \<cdot> (a \<cdot> x)"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   253
    by (simp only: mult_assoc)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   254
  also assume "a \<cdot> x = a \<cdot> y"
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   255
  also from a y have "inverse a \<cdot> \<dots> = y"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   256
    by (simp add: mult_assoc2)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   257
  finally show "x = y" .
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   258
next
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   259
  assume "x = y"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   260
  then show "a \<cdot> x = a \<cdot> y" by (simp only:)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   261
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   262
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   263
lemma mult_right_cancel:
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   264
  assumes x: "x \<in> V" and neq: "x \<noteq> 0"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   265
  shows "(a \<cdot> x = b \<cdot> x) = (a = b)"
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   266
proof
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   267
  from x have "(a - b) \<cdot> x = a \<cdot> x - b \<cdot> x"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   268
    by (simp add: diff_mult_distrib2)
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   269
  also assume "a \<cdot> x = b \<cdot> x"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   270
  with x have "a \<cdot> x - b \<cdot> x = 0" by simp
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   271
  finally have "(a - b) \<cdot> x = 0" .
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   272
  with x neq have "a - b = 0" by (rule mult_zero_uniq)
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   273
  then show "a = b" by simp
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   274
next
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   275
  assume "a = b"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   276
  then show "a \<cdot> x = b \<cdot> x" by (simp only:)
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   277
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   278
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   279
lemma eq_diff_eq:
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   280
  assumes x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   281
  shows "(x = z - y) = (x + y = z)"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   282
proof
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   283
  assume "x = z - y"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   284
  then have "x + y = z - y + y" by simp
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   285
  also from y z have "\<dots> = z + - y + y"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   286
    by (simp add: diff_eq1)
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   287
  also have "\<dots> = z + (- y + y)"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   288
    by (rule add_assoc) (simp_all add: y z)
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   289
  also from y z have "\<dots> = z + 0"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   290
    by (simp only: add_minus_left)
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   291
  also from z have "\<dots> = z"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   292
    by (simp only: add_zero_right)
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   293
  finally show "x + y = z" .
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   294
next
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   295
  assume "x + y = z"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   296
  then have "z - y = (x + y) - y" by simp
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   297
  also from x y have "\<dots> = x + y + - y"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   298
    by (simp add: diff_eq1)
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   299
  also have "\<dots> = x + (y + - y)"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   300
    by (rule add_assoc) (simp_all add: x y)
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   301
  also from x y have "\<dots> = x" by simp
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   302
  finally show "x = z - y" ..
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   303
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   304
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   305
lemma add_minus_eq_minus:
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   306
  assumes x: "x \<in> V" and y: "y \<in> V" and xy: "x + y = 0"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   307
  shows "x = - y"
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   308
proof -
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   309
  from x y have "x = (- y + y) + x" by simp
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   310
  also from x y have "\<dots> = - y + (x + y)" by (simp add: add_ac)
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   311
  also note xy
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   312
  also from y have "- y + 0 = - y" by simp
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   313
  finally show "x = - y" .
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   314
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   315
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   316
lemma add_minus_eq:
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   317
  assumes x: "x \<in> V" and y: "y \<in> V" and xy: "x - y = 0"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   318
  shows "x = y"
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   319
proof -
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   320
  from x y xy have eq: "x + - y = 0" by (simp add: diff_eq1)
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   321
  with _ _ have "x = - (- y)"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   322
    by (rule add_minus_eq_minus) (simp_all add: x y)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   323
  with x y show "x = y" by simp
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   324
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   325
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   326
lemma add_diff_swap:
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   327
  assumes vs: "a \<in> V"  "b \<in> V"  "c \<in> V"  "d \<in> V"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   328
    and eq: "a + b = c + d"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   329
  shows "a - c = d - b"
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10683
diff changeset
   330
proof -
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   331
  from assms have "- c + (a + b) = - c + (c + d)"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   332
    by (simp add: add_left_cancel)
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   333
  also have "\<dots> = d" using `c \<in> V` `d \<in> V` by (rule minus_add_cancel)
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   334
  finally have eq: "- c + (a + b) = d" .
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10683
diff changeset
   335
  from vs have "a - c = (- c + (a + b)) + - b"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   336
    by (simp add: add_ac diff_eq1)
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   337
  also from vs eq have "\<dots>  = d + - b"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   338
    by (simp add: add_right_cancel)
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 23378
diff changeset
   339
  also from vs have "\<dots> = d - b" by (simp add: diff_eq2)
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   340
  finally show "a - c = d - b" .
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   341
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   342
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   343
lemma vs_add_cancel_21:
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   344
  assumes vs: "x \<in> V"  "y \<in> V"  "z \<in> V"  "u \<in> V"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   345
  shows "(x + (y + z) = y + u) = (x + z = u)"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   346
proof
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   347
  from vs have "x + z = - y + y + (x + z)" by simp
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   348
  also have "\<dots> = - y + (y + (x + z))"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   349
    by (rule add_assoc) (simp_all add: vs)
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   350
  also from vs have "y + (x + z) = x + (y + z)"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   351
    by (simp add: add_ac)
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   352
  also assume "x + (y + z) = y + u"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   353
  also from vs have "- y + (y + u) = u" by simp
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   354
  finally show "x + z = u" .
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   355
next
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   356
  assume "x + z = u"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   357
  with vs show "x + (y + z) = y + u"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   358
    by (simp only: add_left_commute [of x])
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   359
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   360
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   361
lemma add_cancel_end:
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   362
  assumes vs: "x \<in> V"  "y \<in> V"  "z \<in> V"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   363
  shows "(x + (y + z) = y) = (x = - z)"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12114
diff changeset
   364
proof
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   365
  assume "x + (y + z) = y"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   366
  with vs have "(x + z) + y = 0 + y" by (simp add: add_ac)
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   367
  with vs have "x + z = 0" by (simp only: add_right_cancel add_closed zero)
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   368
  with vs show "x = - z" by (simp add: add_minus_eq_minus)
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   369
next
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   370
  assume eq: "x = - z"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   371
  then have "x + (y + z) = - z + (y + z)" by simp
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   372
  also have "\<dots> = y + (- z + z)" by (rule add_left_commute) (simp_all add: vs)
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   373
  also from vs have "\<dots> = y"  by simp
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   374
  finally show "x + (y + z) = y" .
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
   375
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   376
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 10683
diff changeset
   377
end
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   378
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   379
end
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
   380