68 \\<forall>x \\<in> V. \\<forall>y \\<in> V. x - y = x + - y |] ==> is_vectorspace V" |
68 \\<forall>x \\<in> V. \\<forall>y \\<in> V. x - y = x + - y |] ==> is_vectorspace V" |
69 proof (unfold is_vectorspace_def, intro conjI ballI allI) |
69 proof (unfold is_vectorspace_def, intro conjI ballI allI) |
70 fix x y z |
70 fix x y z |
71 assume "x \\<in> V" "y \\<in> V" "z \\<in> V" |
71 assume "x \\<in> V" "y \\<in> V" "z \\<in> V" |
72 "\\<forall>x \\<in> V. \\<forall>y \\<in> V. \\<forall>z \\<in> V. x + y + z = x + (y + z)" |
72 "\\<forall>x \\<in> V. \\<forall>y \\<in> V. \\<forall>z \\<in> V. x + y + z = x + (y + z)" |
73 thus "x + y + z = x + (y + z)" by (elim bspec[elimify]) |
73 thus "x + y + z = x + (y + z)" by blast |
74 qed force+ |
74 qed force+ |
75 |
75 |
76 text_raw {* \medskip *} |
76 text_raw {* \medskip *} |
77 text {* The corresponding destruction rules are: *} |
77 text {* The corresponding destruction rules are: *} |
78 |
78 |
94 |
94 |
95 lemma diff_eq2: |
95 lemma diff_eq2: |
96 "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> x + - y = x - y" |
96 "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> x + - y = x - y" |
97 by (unfold is_vectorspace_def) simp |
97 by (unfold is_vectorspace_def) simp |
98 |
98 |
99 lemma vs_not_empty [intro??]: "is_vectorspace V ==> (V \\<noteq> {})" |
99 lemma vs_not_empty [intro?]: "is_vectorspace V ==> (V \\<noteq> {})" |
100 by (unfold is_vectorspace_def) simp |
100 by (unfold is_vectorspace_def) simp |
101 |
101 |
102 lemma vs_add_closed [simp, intro??]: |
102 lemma vs_add_closed [simp, intro?]: |
103 "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> x + y \\<in> V" |
103 "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> x + y \\<in> V" |
104 by (unfold is_vectorspace_def) simp |
104 by (unfold is_vectorspace_def) simp |
105 |
105 |
106 lemma vs_mult_closed [simp, intro??]: |
106 lemma vs_mult_closed [simp, intro?]: |
107 "[| is_vectorspace V; x \\<in> V |] ==> a \\<cdot> x \\<in> V" |
107 "[| is_vectorspace V; x \\<in> V |] ==> a \\<cdot> x \\<in> V" |
108 by (unfold is_vectorspace_def) simp |
108 by (unfold is_vectorspace_def) simp |
109 |
109 |
110 lemma vs_diff_closed [simp, intro??]: |
110 lemma vs_diff_closed [simp, intro?]: |
111 "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> x - y \\<in> V" |
111 "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> x - y \\<in> V" |
112 by (simp add: diff_eq1 negate_eq1) |
112 by (simp add: diff_eq1 negate_eq1) |
113 |
113 |
114 lemma vs_neg_closed [simp, intro??]: |
114 lemma vs_neg_closed [simp, intro?]: |
115 "[| is_vectorspace V; x \\<in> V |] ==> - x \\<in> V" |
115 "[| is_vectorspace V; x \\<in> V |] ==> - x \\<in> V" |
116 by (simp add: negate_eq1) |
116 by (simp add: negate_eq1) |
117 |
117 |
118 lemma vs_add_assoc [simp]: |
118 lemma vs_add_assoc [simp]: |
119 "[| is_vectorspace V; x \\<in> V; y \\<in> V; z \\<in> V |] |
119 "[| is_vectorspace V; x \\<in> V; y \\<in> V; z \\<in> V |] |
321 also have "... = - x + x + y" by (simp!) |
321 also have "... = - x + x + y" by (simp!) |
322 also have "... = - x + (x + y)" |
322 also have "... = - x + (x + y)" |
323 by (simp! only: vs_add_assoc vs_neg_closed) |
323 by (simp! only: vs_add_assoc vs_neg_closed) |
324 also assume "x + y = x + z" |
324 also assume "x + y = x + z" |
325 also have "- x + (x + z) = - x + x + z" |
325 also have "- x + (x + z) = - x + x + z" |
326 by (simp! only: vs_add_assoc[RS sym] vs_neg_closed) |
326 by (simp! only: vs_add_assoc [RS sym] vs_neg_closed) |
327 also have "... = z" by (simp!) |
327 also have "... = z" by (simp!) |
328 finally show ?R . |
328 finally show ?R . |
329 qed force |
329 qed force |
330 |
330 |
331 lemma vs_add_right_cancel: |
331 lemma vs_add_right_cancel: |