equal
deleted
inserted
replaced
225 |
225 |
226 lemma vs_sumD: |
226 lemma vs_sumD: |
227 "x \<in> U + V = (\<exists>u \<in> U. \<exists>v \<in> V. x = u + v)" |
227 "x \<in> U + V = (\<exists>u \<in> U. \<exists>v \<in> V. x = u + v)" |
228 by (unfold vs_sum_def) fast |
228 by (unfold vs_sum_def) fast |
229 |
229 |
230 lemmas vs_sumE = vs_sumD [THEN iffD1, elimify, standard] |
230 lemmas vs_sumE = vs_sumD [THEN iffD1, elimified, standard] |
231 |
231 |
232 lemma vs_sumI [intro?]: |
232 lemma vs_sumI [intro?]: |
233 "[| x \<in> U; y \<in> V; t= x + y |] ==> t \<in> U + V" |
233 "[| x \<in> U; y \<in> V; t= x + y |] ==> t \<in> U + V" |
234 by (unfold vs_sum_def) fast |
234 by (unfold vs_sum_def) fast |
235 |
235 |