1(* ------------------------------------------------------------------------- *) 2(* Finite Vector Space *) 3(* ------------------------------------------------------------------------- *) 4 5(*===========================================================================*) 6 7(* add all dependent libraries for script *) 8open HolKernel boolLib bossLib Parse; 9 10(* declare new theory at start *) 11val _ = new_theory "FiniteVSpace"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16 17(* val _ = load "jcLib"; *) 18open jcLib; 19 20(* Get dependent theories local *) 21(* val _ = load "LinearIndepTheory"; *) 22open VectorSpaceTheory SpanSpaceTheory LinearIndepTheory; 23open monoidTheory fieldTheory; 24 25(* Get dependent theories in lib *) 26(* val _ = load "helperListTheory"; *) 27open helperNumTheory helperSetTheory helperListTheory; 28 29(* open dependent theories *) 30open pred_setTheory arithmeticTheory listTheory; 31 32 33(* ------------------------------------------------------------------------- *) 34(* Finite Vector Space Documentation *) 35(* ------------------------------------------------------------------------- *) 36(* Overload: 37*) 38(* Definitions and Theorems (# are exported): 39 40 Finite Vector Space: 41 FiniteVSpace_def |- !r g op. FiniteVSpace r g op <=> VSpace r g op /\ FINITE R /\ FINITE V 42 finite_vspace_is_vspace |- !r g op. FiniteVSpace r g op ==> VSpace r g op 43 finite_vspace_is_finite |- !r g op. FiniteVSpace r g op ==> FINITE R /\ FINITE V 44 finite_vspace_all_basis |- !r g op. FiniteVSpace r g op ==> basis g (SET_TO_LIST V) 45 finite_vspace_span_itself |- !r g op. FiniteVSpace r g op ==> (SpanSpace r g op (SET_TO_LIST V) = g) 46 47 Finite Vector Space Dimension: 48 dim_def |- !r g op. dim r g op = 49 MIN_SET (IMAGE LENGTH {b | basis g b /\ (SpanSpace r g op b = g)}) 50 finite_vspace_dim_basis |- !r g op. FiniteVSpace r g op ==> 51 ?b. basis g b /\ (LENGTH b = dim r g op) /\ (SpanSpace r g op b = g) 52 finite_vspace_dim_eq_0 |- !r g op. FiniteVSpace r g op /\ (dim r g op = 0) ==> (g.carrier = {g.id}) 53 54 finite_vspace_dim_basis_indep |- !r g op. FiniteVSpace r g op ==> 55 !b. basis g b /\ (LENGTH b = dim r g op) /\ 56 (SpanSpace r g op b = g) ==> LinearIndepBasis r g op b 57 finite_vspace_dim_map_inj |- !r g op. FiniteVSpace r g op ==> 58 !b. basis g b /\ (LENGTH b = dim r g op) /\ (SpanSpace r g op b = g) ==> 59 INJ (\n. n |o| b) (sticks r (LENGTH b)) V 60 61 Finite Vector Space Cardinality and Linear Independence: 62 finite_vspace_card |- !r g op. FiniteVSpace r g op ==> (CARD V = CARD R ** dim r g op) 63 finite_vspace_indep_span_card |- !r g op. FiniteVSpace r g op ==> !b. LinearIndepBasis r g op b ==> 64 (CARD (SpanSpace r g op b).carrier = CARD R ** LENGTH b) 65 finite_vspace_dim_basis_span |- !r g op. FiniteVSpace r g op ==> 66 !b. basis g b /\ (LENGTH b = dim r g op) /\ 67 LinearIndepBasis r g op b ==> (SpanSpace r g op b = g) 68 finite_vspace_dim_basis_property |- !r g op. FiniteVSpace r g op ==> 69 !b. basis g b /\ (LENGTH b = dim r g op) ==> 70 (LinearIndepBasis r g op b <=> (SpanSpace r g op b = g)) 71 finite_vspace_basis_dep_special |- !r g op. FiniteVSpace r g op ==> 72 !b. basis g b /\ (LENGTH b = SUC (dim r g op)) ==> ~LinearIndepBasis r g op b 73 finite_vspace_basis_dep |- !r g op. FiniteVSpace r g op ==> 74 !b. basis g b /\ dim r g op < LENGTH b ==> ~LinearIndepBasis r g op b 75 76*) 77 78(* Overloads for convenience *) 79val _ = temp_overload_on ("o", ``(op:'a -> 'b -> 'b)``); 80val _ = temp_overload_on ("V", ``(g:'b group).carrier``); 81val _ = temp_overload_on ("||", ``(g:'b group).op``); 82val _ = temp_overload_on ("|0|", ``(g:'b group).id``); 83val _ = set_fixity "||" (Infixl 500); (* same as + in arithmeticScript.sml *) 84 85val _ = temp_overload_on ("+", ``stick_add r``); 86val _ = temp_overload_on ("-", ``stick_neg r``); 87val _ = temp_overload_on ("*", ``stick_cmult r``); 88val _ = temp_overload_on ("-", ``stick_sub r``); 89 90(* ------------------------------------------------------------------------- *) 91(* Finite Vector Space. *) 92(* ------------------------------------------------------------------------- *) 93 94(* Define Finite Vector Space *) 95val FiniteVSpace_def = Define` 96 FiniteVSpace (r:'a field) (g:'b group) op <=> VSpace r g op /\ FINITE R /\ FINITE V 97`; 98 99(* Theorem: FiniteVSpace r g op ==> VSpace r g op *) 100(* Proof: by FiniteVSpace_def. *) 101(* 102val finite_vspace_is_vspace = store_thm( 103 "finite_vspace_is_vspace", 104 ``!(r:'a field) (g:'b group) op. FiniteVSpace r g op ==> VSpace r g op``, 105 rw[FiniteVSpace_def]); 106*) 107val finite_vspace_is_vspace = save_thm("finite_vspace_is_vspace", 108 FiniteVSpace_def |> SPEC_ALL |> (#1 o EQ_IMP_RULE) |> 109 UNDISCH |> CONJUNCTS |> el 1 |> DISCH_ALL |> GEN_ALL); 110(* val finite_vspace_is_vspace = |- !r op g. FiniteVSpace r g op ==> VSpace r g op: thm *) 111 112(* Theorem: FiniteVSpace r g op ==> FINITE R /\ FINITE V *) 113(* Proof: by FiniteVSpace_def. *) 114val finite_vspace_is_finite = store_thm( 115 "finite_vspace_is_finite", 116 ``!(r:'a field) (g:'b group) op. FiniteVSpace r g op ==> FINITE R /\ FINITE V``, 117 rw[FiniteVSpace_def]); 118 119(* Theorem: For FiniteVSpace, list of all vectors is a basis: basis g (SET_TO_LIST V) *) 120(* Proof: 121 Since FINITE V, !x. MEM x (SET_TO_LIST V) <=> x IN V by MEM_SET_TO_LIST 122 Thus true by basis_member. 123*) 124val finite_vspace_all_basis = store_thm( 125 "finite_vspace_all_basis", 126 ``!(r:'a field) (g:'b group) op. FiniteVSpace r g op ==> basis g (SET_TO_LIST V)``, 127 metis_tac[FiniteVSpace_def, basis_member, MEM_SET_TO_LIST]); 128 129(* Theorem: The whole Group g can span itself. 130 SpanSpace r g op (SET_TO_LIST V) = g *) 131(* Proof: 132 Note FiniteSpace r g op ==> basis g (SET_TO_LIST V) by finite_vspace_all_basis 133 By SpanSpace_def and monoid_component_equality, this is to show: 134 SpanSpace r g op (SET_TO_LIST V).carrier = V 135 or IMAGE (\n. n |o| (SET_TO_LIST V)) (sticks r (LENGTH (SET_TO_LIST V))) = V 136 which is to show: 137 (1) n IN sticks r (LENGTH (SET_TO_LIST V)) ==> n |o| (SET_TO_LIST V) IN V 138 n |o| (SET_TO_LIST V) IN V by vsum_basis_stick_vector 139 (2) x IN V ==> ?n. (x = n |o| (SET_TO_LIST V)) /\ n IN sticks r (LENGTH (SET_TO_LIST V)) 140 x IN V ==> MEM x (SET_TO_LIST V) by MEM_SET_TO_LIST 141 Let n = the sticks of LENGTH (SET_TO_LIST V), with all #0, but #1 at x. 142 Then n |o| (SET_TO_LIST V) = x by vspace_basis_stick 143*) 144val finite_vspace_span_itself = store_thm( 145 "finite_vspace_span_itself", 146 ``!(r:'a field) (g:'b group) op. FiniteVSpace r g op ==> (SpanSpace r g op (SET_TO_LIST V) = g)``, 147 rpt (stripDup[FiniteVSpace_def]) >> 148 `basis g (SET_TO_LIST V)` by metis_tac[finite_vspace_all_basis] >> 149 rw[monoid_component_equality, SpanSpace_def, EXTENSION, EQ_IMP_THM] >- 150 metis_tac[vsum_basis_stick_vector] >> 151 metis_tac[vspace_basis_stick, MEM_SET_TO_LIST]); 152 153(* ------------------------------------------------------------------------- *) 154(* Finite Vector Space Dimension. *) 155(* ------------------------------------------------------------------------- *) 156 157(* Dimension = LENGTH of shortest basis spanning the whole vector space) *) 158val dim_def = Define` 159 dim (r:'a field) (g:'b group) op = 160 MIN_SET (IMAGE LENGTH { b | basis g b /\ (SpanSpace r g op b = g) }) 161`; 162 163(* Theorem: Existence of Spanning basis with dimension. 164 FiniteVSpace r g op ==> ?b. basis g b /\ (LENGTH b = dim r g op) *) 165(* Proof: 166 Given FiniteVSpace r g op, 167 ==> basis g (SET_TO_LIST V) by finite_vspace_all_basis 168 (SpanSpace r g op (SET_TO_LIST V) = g) by finite_vspace_span_itself 169 hence SET_TO_LIST V IN { b | basis g b /\ (SpanSpace r g op b = g) } 170 or s = { b | basis g b /\ (SpanSpace r g op b = g) } <> {} by MEMBER_NOT_EMPTY 171 Thus IMAGE LENGTH s <> {} by IMAGE_EQ_EMPTY 172 so dim r g op exists, and 173 dim r g op = MIN_SET (IMAGE LENGTH s) IN (IMAGE LENGTH s) by MIN_SET_LEM 174 or ?b. basis g b /\ (LENGTH b = dim r g op) /\ (SpanSpace r g op b = g) by IN_IMAGE 175*) 176val finite_vspace_dim_basis = store_thm( 177 "finite_vspace_dim_basis", 178 ``!(r:'a field) (g:'b group) op. FiniteVSpace r g op ==> 179 ?b. basis g b /\ (LENGTH b = dim r g op) /\ (SpanSpace r g op b = g)``, 180 rw[dim_def] >> 181 qabbrev_tac `s = { b | basis g b /\ (SpanSpace r g op b = g) }` >> 182 `!b. b IN s ==> basis g b /\ (SpanSpace r g op b = g)` by rw[Abbr`s`] >> 183 `basis g (SET_TO_LIST V)` by metis_tac[finite_vspace_all_basis] >> 184 `(SpanSpace r g op (SET_TO_LIST V) = g)` by rw[finite_vspace_span_itself] >> 185 `SET_TO_LIST V IN s` by rw[Abbr`s`] >> 186 `IMAGE LENGTH s <> {}` by metis_tac[MEMBER_NOT_EMPTY, IMAGE_EQ_EMPTY] >> 187 `MIN_SET (IMAGE LENGTH s) IN (IMAGE LENGTH s)` by rw[MIN_SET_LEM] >> 188 metis_tac[IN_IMAGE]); 189 190(* Theorem: FiniteVSpace r g op /\ (dim r g op = 0) ==> (g.carrier = {g.id}) *) 191(* Proof: 192 Since FiniteVSpace r g op 193 ==> ?b. basis g b /\ (LENGTH b = dim r g op) /\ 194 (SpanSpace r g op b = g) by finite_vspace_dim_basis 195 Given dim r g op = 0, 196 so LENGTH b = 0, or b = [] by LENGTH_NIL 197 and sticks r 0 = {[]} by sticks_0 198 Hence g.carrier 199 = (SpanSpace r g op b).carrier by above 200 = IMAGE (\n. n |o| b) (sticks r (LENGTH b)) by vspace_span_property 201 = IMAGE (\n. n |o| []) {[]} by above 202 = {[] |o| []} by application 203 = {g.id} by vsum_nil 204*) 205val finite_vspace_dim_eq_0 = store_thm( 206 "finite_vspace_dim_eq_0", 207 ``!(r:'a ring) (g:'b group) op. FiniteVSpace r g op /\ (dim r g op = 0) ==> (g.carrier = {g.id})``, 208 rpt (stripDup[FiniteVSpace_def]) >> 209 `?b. basis g b /\ (LENGTH b = dim r g op) /\ (SpanSpace r g op b = g)` by rw[finite_vspace_dim_basis] >> 210 `b = []` by metis_tac[LENGTH_NIL] >> 211 `sticks r 0 = {[]}` by rw[sticks_0] >> 212 `g.carrier = IMAGE (\n. n |o| b) (sticks r (LENGTH b))` by rw[GSYM vspace_span_property] >> 213 rw[vsum_nil]); 214 215(* Theorem: In a Finite Vector Space, 216 A spanning basis of dimension size is linearly independent: 217 basis g b /\ (LENGTH b = dim r g op) /\ (SpanSpace r g op b = g) ==> LinearIndepBasis r g op b *) 218(* Proof: 219 By LinearIndepBasis_def, this is to show: 220 (1) k < dim r g op ==> EL k n = #0 221 Let u = EL k b` 222 b' = DROP (SUC k) b ++ TAKE k b 223 By contradiction, suppose EL k n = u <> #0. 224 (1) Show: LENGTH b' < LENGTH b 225 Note rotate k b = u::b' by rotate_shift_element 226 so LENGTH b = SUC(LENGTH b') by rotate_same_length, LENGTH 227 or LENGTH b' < LENGTH b 228 (2) Show: LENGTH b <= LENGTH b' 229 Let s = { b | basis g b /\ (SpanSpace r g op b = g) } 230 Then dim r g op = MIN_SET (IMAGE LENGTH s) 231 by dim_def 232 Since basis g (rotate k b) by basis_rotate_basis 233 = basis g (u::b') by above, rotate k b = u::b' 234 Hence basis g b' by basis_cons 235 and SpanSpace r g op b' = SpanSpace r g op b by vspace_span_basis_shrink 236 Thus b' IN s by definition of s 237 so s <> {} by MEMBER_NOT_EMPTY 238 and IMAGE LENGTH s <> {} by IMAGE_EQ_EMPTY 239 Also LENGTH b' IN IMAGE LENGTH s by IN_IMAGE 240 so LENGTH b <= LENGTH b' by MIN_SET_LEM 241 However, (1) and (2) lead to a contradiction. 242 (2) n IN sticks r (dim r g op) /\ !k. k < dim r g op ==> (EL k n = #0) ==> n |o| b = |0| 243 True by vspace_stick_zero. 244*) 245val finite_vspace_dim_basis_indep = store_thm( 246 "finite_vspace_dim_basis_indep", 247 ``!(r:'a field) (g:'b group) op. FiniteVSpace r g op ==> 248 !b. basis g b /\ (LENGTH b = dim r g op) /\ (SpanSpace r g op b = g) ==> 249 LinearIndepBasis r g op b``, 250 rpt (stripDup[FiniteVSpace_def]) >> 251 rw[LinearIndepBasis_def, EQ_IMP_THM] >| [ 252 spose_not_then strip_assume_tac >> 253 qabbrev_tac `u = EL k b` >> 254 qabbrev_tac `b' = DROP (SUC k) b ++ TAKE k b` >> 255 `rotate k b = u::b'` by rw[rotate_shift_element] >> 256 `LENGTH b = SUC(LENGTH b')` by metis_tac[rotate_same_length, LENGTH] >> 257 `LENGTH b' < LENGTH b` by decide_tac >> 258 qabbrev_tac `s = { b | basis g b /\ (SpanSpace r g op b = g) }` >> 259 `dim r g op = MIN_SET (IMAGE LENGTH s)` by rw[GSYM dim_def, Abbr`s`] >> 260 `basis g b'` by metis_tac[basis_rotate_basis, basis_cons] >> 261 `SpanSpace r g op b' = SpanSpace r g op b` by metis_tac[vspace_span_basis_shrink] >> 262 `b' IN s` by rw[Abbr`b'`, Abbr`s`] >> 263 `IMAGE LENGTH s <> {}` by metis_tac[MEMBER_NOT_EMPTY, IMAGE_EQ_EMPTY] >> 264 `LENGTH b <= LENGTH b'` by metis_tac[MIN_SET_LEM, IN_IMAGE] >> 265 decide_tac, 266 metis_tac[vspace_stick_zero] 267 ]); 268 269(* Theorem: In a Finite Vector Space, 270 A spanning basis of dimension size gives an injective map: 271 basis g b /\ (LENGTH b = dim r g op) /\ (SpanSpace r g op b = g) ==> 272 INJ (\n. n |o| b) (sticks r (LENGTH b)) V *) 273(* Proof: 274 Since FiniteVSpace r g op ==> VSpace r g op by finite_vspace_is_vspace 275 and LinearIndepBasis r g op b by finite_vspace_dim_basis_indep 276 so INJ (\n. n |o| b) (sticks r (LENGTH b)) V by vspace_indep_basis_inj 277*) 278val finite_vspace_dim_map_inj = store_thm( 279 "finite_vspace_dim_map_inj", 280 ``!(r:'a field) (g:'b group) op. FiniteVSpace r g op ==> 281 !b. basis g b /\ (LENGTH b = dim r g op) /\ (SpanSpace r g op b = g) ==> 282 INJ (\n. n |o| b) (sticks r (LENGTH b)) V``, 283 rw[FiniteVSpace_def, finite_vspace_dim_basis_indep, vspace_indep_basis_inj]); 284 285(* ------------------------------------------------------------------------- *) 286(* Finite Vector Space Cardinality and Linear Independence. *) 287(* ------------------------------------------------------------------------- *) 288 289(* Then show: CARD V = (CARD R) ** DIM (VSpace r g op) 290 Possibly, this involves showing n IN (sticks r (LENGTH b)) ==> (\n. n |o| p) is INJ. 291*) 292 293(* Theorem: FiniteVSpace r g op ==> CARD V = (CARD R) ** dim r g op *) 294(* Proof: 295 Since FiniteVSpace r g op, 296 ?b. basis g b /\ (LENGTH b = dim r g op) /\ 297 (SpanSpace r g op b = g) by finite_vspace_dim_basis 298 so V = (SpanSpace r g op b).carrier by monoid_component_equality 299 = IMAGE (\n. n |o| b) (sticks r (LENGTH b)) by vspace_span_property 300 Now INJ (\n. VSUM (MAP2 op n b)) (sticks r (LENGTH b)) V` by rw[finite_vspace_dim_map_inj]); 301 and SURJ (\n. VSUM (MAP2 op n b)) (sticks r (LENGTH b)) V` by rw[IMAGE_SURJ]); 302 and FINITE (sticks r (LENGTH b)), 303 Hence CARD V 304 = CARD (sticks r (LENGTH b)) by FINITE_BIJ_CARD_EQ, BIJ_DEF 305 = CARD R ** (LENGTH b) by sticks_card 306 = CARD R ** (dim r g op) by given LENGTH b = dim r g op 307*) 308val finite_vspace_card = store_thm( 309 "finite_vspace_card", 310 ``!(r:'a field) (g:'b group) op. FiniteVSpace r g op ==> (CARD V = (CARD R) ** dim r g op)``, 311 rpt (stripDup[FiniteVSpace_def]) >> 312 `?b. basis g b /\ (LENGTH b = dim r g op) /\ (SpanSpace r g op b = g)` by rw[finite_vspace_dim_basis] >> 313 `V = IMAGE (\n. n |o| b) (sticks r (LENGTH b))` by metis_tac[vspace_span_property, monoid_component_equality] >> 314 `INJ (\n. VSUM (MAP2 op n b)) (sticks r (LENGTH b)) V` by rw[finite_vspace_dim_map_inj] >> 315 `SURJ (\n. VSUM (MAP2 op n b)) (sticks r (LENGTH b)) V` by rw[IMAGE_SURJ] >> 316 `FINITE (sticks r (LENGTH b))` by rw[sticks_finite] >> 317 metis_tac[FINITE_BIJ_CARD_EQ, BIJ_DEF, sticks_card]); 318 319(* 320 321Vector Space: 322(1) a set of scalars (e.g. the basis field) 323(2) a set of vectors (e.g. the extended field), forming a group (an Abelian group) 324(3) an operation: (scalar, vector) -> vector, that preserves the group structure of vectors. 325 326First goal: establish a dimension for vector space. 327Since I define: dim = size of smallest basis that can span the whole space. 328The route is quite complicated: 329(a) Define a basis (or basis) = a list of vectors 330(b) Define what is meant by spanning by a basis: the set of all linear combinations. 331(b1) Linear combinations of basis with what? with sticks = a list of scalars. 332(b2) How to get a linear combination? VSUM (MAP (\(se, ve). se o ve) (ZIP (sticks, basis))) 333(c) Define a SpanSpace by basis. 334(d) Show that SpanSpace with basis = all vectors spans the whole space (of course). 335(e) Show that a basis can shrink if it includes a dependent element. 336(f) Since the possible basis is not empty, and empty basis cannot span the whole, there must be a minimum. 337(g) Define dim = cardinality (smallest spanning basis) 338Since this is the smallest spanning basis, all vectors are linear combinations of these vectors. 339By counting how many such linear combinations, 340finally giving the first important result: CARD (vector space) = CARD (scalar) ** (dimension) 341 342Next goal: any set of vectors with cardinality more than dim is linearly dependent. 343 344Can the first goal be done directly with the concept of linearly dependency and linear independency? 345(a) Define a vlist = list of vectors 346(b) Define a slist = list of scalars 347(c) Define linear combination = VSUM (MAP f (ZIP (slist, vlist))) of same length 348(d) Define a linear independent vlist <=> (linear_comb (slist, vlist) = ||0|| ==> (slist = all #0)) 349 can call a linear independent basis. 350(e) Show that a singleton basis is linearly independent. 351 Show that the whole basis is linearly dependent (because ???) 352 So there is a maximum linearly independent basis. 353 Define dim = size of maximum linearly independent basis 354(f) Then, all basis of cardinality exceeding dim will be linearly dependent. 355 356*) 357 358(* Theorem: FiniteVSpace r g op ==> !b. LinearIndepBasis r g op b ==> 359 (CARD ((SpanSpace r g op b).carrier) = CARD R ** LENGTH b) *) 360(* Proof: 361 Note VSpace r g op /\ FINITE R /\ FINITE V by FiniteVSpace_def 362 and basis g b by indep_basis_is_basis 363 Now INJ (\n. n |o| b) (sticks r (LENGTH b)) V by vspace_indep_basis_inj 364 and FINITE (sticks r (LENGTH b) by sticks_finite, FINITE R 365 CARD ((SpanSpace r g op b).carrier) 366 = CARD (IMAGE (\n. n |o| b) (sticks r (LENGTH b))) by vspace_span_property 367 = CARD (sticks r (LENGTH b)) by INJ_CARD_IMAGE_EQ 368 = CARD R ** LENGTH b by sticks_card 369*) 370val finite_vspace_indep_span_card = store_thm( 371 "finite_vspace_indep_span_card", 372 ``!(r:'a field) (g:'b group) op. FiniteVSpace r g op ==> 373 !b. LinearIndepBasis r g op b ==> (CARD ((SpanSpace r g op b).carrier) = CARD R ** LENGTH b)``, 374 rpt (stripDup[FiniteVSpace_def]) >> 375 `basis g b` by metis_tac[indep_basis_is_basis] >> 376 `INJ (\n. n |o| b) (sticks r (LENGTH b)) V` by rw[vspace_indep_basis_inj] >> 377 `FINITE (sticks r (LENGTH b))` by rw[sticks_finite] >> 378 metis_tac[vspace_span_property, INJ_CARD_IMAGE_EQ, sticks_card]); 379 380(* Theorem: basis g b /\ (LENGTH b = dim r g op) /\ LinearIndepBasis r g op b ==> (SpanSpace r g op b = g) *) 381(* Proof: 382 Note FiniteVSpace r g op 383 ==> VSpace r g op /\ FINITE R /\ FINITE V by FiniteVSpace_def 384 Since CARD V 385 = CARD R ** dim r g op by finite_vspace_card, FiniteVSpace r g op 386 = CARD R ** LENGTH b by given 387 = CARD ((SpanSpace r g op b).carrier) by finite_vspace_indep_span_card 388 Also (SpanSpace r g op b).carrier SUBSET V by vspace_span_vector, SUBSET_DEF 389 thus FINITE (SpanSpace r g op b).carrier by SUBSET_FINITE 390 so (SpanSpace r g op b).carrier = V by SUBSET_EQ_CARD 391 Hence SpanSpace r g op b = g by SpanSpace_def, monoid_component_equality 392*) 393val finite_vspace_dim_basis_span = store_thm( 394 "finite_vspace_dim_basis_span", 395 ``!(r:'a field) (g:'b group) op. FiniteVSpace r g op ==> 396 !b. basis g b /\ (LENGTH b = dim r g op) /\ LinearIndepBasis r g op b ==> (SpanSpace r g op b = g)``, 397 rpt (stripDup[FiniteVSpace_def]) >> 398 `CARD V = CARD R ** dim r g op` by rw[finite_vspace_card] >> 399 `CARD ((SpanSpace r g op b).carrier) = CARD R ** LENGTH b` by rw[finite_vspace_indep_span_card] >> 400 `(SpanSpace r g op b).carrier SUBSET V` by metis_tac[vspace_span_vector, SUBSET_DEF] >> 401 `FINITE (SpanSpace r g op b).carrier` by metis_tac[SUBSET_FINITE] >> 402 `(SpanSpace r g op b).carrier = V` by rw[SUBSET_EQ_CARD] >> 403 rw[SpanSpace_def, monoid_component_equality]); 404 405(* Theorem: basis g b /\ (LENGTH b = dim r g op) ==> 406 (LinearIndepBasis r g op b <=> (SpanSpace r g op b = g)) *) 407(* Proof: 408 If part: LinearIndepBasis r g op b ==> SpanSpace r g op b = g 409 True by finite_vspace_dim_basis_span. 410 Only-if part: SpanSpace r g op b = g ==> LinearIndepBasis r g op b 411 True by finite_vspace_dim_basis_indep 412*) 413val finite_vspace_dim_basis_property = store_thm( 414 "finite_vspace_dim_basis_property", 415 ``!(r:'a field) (g:'b group) op. FiniteVSpace r g op ==> 416 !b. basis g b /\ (LENGTH b = dim r g op) ==> 417 (LinearIndepBasis r g op b <=> (SpanSpace r g op b = g))``, 418 metis_tac[finite_vspace_dim_basis_span, finite_vspace_dim_basis_indep]); 419 420(* Theorem: A basis with a size one more of dimension is linear dependent: 421 basis g b /\ (LENGTH b = SUC (dim r g op)) ==> ~LinearIndepBasis r g op b *) 422(* Proof: 423 By contradiction, assume LinearIndepBasis r g op b. 424 Since LENGTH b = SUC (dim r g op) 425 ==> 0 < LENGTH b and LENGTH b <> 0 426 Hence ?v u. b = v::u by LENGTH_NIL, list_CASES 427 and basis g b ==> v IN V /\ basis g u by basis_cons 428 Also LENGHT b = SUC (LENGTH u) by LENGTH 429 = SUC (dim r g op) by given 430 so LENGTH u = dim r g op by prim_recTheory.INV_SUC_EQ 431 By shrinking a linear independent basis, 432 LinearIndepBasis r g op u by vspace_basis_indep_one_less 433 Hence SpanSpace r g op u = g by finite_vspace_dim_basis_property 434 Thus v IN V ==> 435 v IN (SpanSpace r g op u).carrier by monoid_component_equality 436 or ?n. n IN sticks r (LENGTH u) and 437 (v = n |o| u) by vspace_span_property 438 or |0| = (- #1) o v || (n |o| u) by vspace_vsub_eq_zero_alt 439 = ((- #1)::n) |o| b by vsum_cons, MAP2 440 Let m = (- #1) :: n. 441 Then m IN sticks r (LENGTH b) by stick_cons, LENGTH 442 and EL 0 m = -#1 by EL, HD 443 But !k. k < LENGTH b ==> (EL k m = #0) by implication, 444 so EL 0 m = #0 by 0 < LENGTH b 445 which is a contradiction with EL 0 m = #1. 446*) 447val finite_vspace_basis_dep_special = store_thm( 448 "finite_vspace_basis_dep_special", 449 ``!(r:'a field) (g:'b group) op. FiniteVSpace r g op ==> 450 !b. basis g b /\ (LENGTH b = SUC (dim r g op)) ==> ~LinearIndepBasis r g op b``, 451 rpt (stripDup[FiniteVSpace_def, LinearIndepBasis_def]) >> 452 `0 < LENGTH b /\ LENGTH b <> 0` by decide_tac >> 453 `?v u. b = v::u` by metis_tac[LENGTH_NIL, list_CASES] >> 454 `v IN V /\ basis g u` by metis_tac[basis_cons] >> 455 `SUC (LENGTH u) = SUC (dim r g op)` by metis_tac[LENGTH] >> 456 `LENGTH u = dim r g op` by decide_tac >> 457 `LinearIndepBasis r g op u` by metis_tac[vspace_basis_indep_one_less] >> 458 `SpanSpace r g op u = g` by rw[GSYM finite_vspace_dim_basis_property] >> 459 `v IN (SpanSpace r g op u).carrier` by rw[monoid_component_equality] >> 460 `?n. n IN sticks r (LENGTH u) /\ (v = n |o| u)` by rw[vspace_span_property] >> 461 `|0| = (- #1) o v || (n |o| u)` by metis_tac[vspace_vsub_eq_zero_alt] >> 462 `_ = ((- #1)::n) |o| b` by rw[vsum_cons] >> 463 `Field r` by metis_tac[vspace_has_field] >> 464 `Group g` by metis_tac[vspace_has_group] >> 465 `- #1 IN R /\ - #1 <> #0` by rw[] >> 466 qabbrev_tac `m = (- #1) :: n` >> 467 `m IN sticks r (LENGTH b)` by metis_tac[stick_cons, LENGTH] >> 468 `EL 0 m = -#1` by rw[Abbr`m`] >> 469 metis_tac[]); 470 471(* Theorem: FiniteVSpace r g op ==> 472 !b. basis g b /\ (dim r g op < LENGTH b) ==> ~LinearIndepBasis r g op b *) 473(* Proof: 474 Idea: 475 By contradiction, assume LinearIndepBasis r g op b. 476 Now remove elements from basis b to become b', with LENGTH b' = dim r g op. 477 Then LinearIndepBasis r g op b ==> LinearIndepBasis r g op b' by vspace_basis_indep_one_less 478 and SpanSpace r g op b' = g by finite_vspace_dim_basis_property 479 Since the removed elements are in V, 480 this means they can be expressed as linear combinations of b', 481 contradicting LinearIndepBasis r g op b. 482 Proof: 483 Note: dim r g op < LENGTH b means SUC (dim r g op) <= LENGTH b. 484 First, prove the case for LENGTH b = SUC (dim r g op) in finite_vspace_basis_dep_special 485 Then, by induction on (LENGTH b - SUC (dim r g op)). 486 Base case: LENGTH b - SUC (dim r g op) = 0 ==> ~LinearIndepBasis r g op b 487 Since LENGTH b - SUC (dim r g op) = 0 488 ==> LENGTH b <= SUC (dim r g op) by SUB_EQ_0 489 ==> LENGTH b = SUC (dim r g op) by given SUC (dim r g op) <= LENGTH b. 490 Hence ~LinearIndepBasis r g op b by finite_vspace_basis_dep_special 491 492 Step case: !b r g op. (v = LENGTH b - SUC (dim r g op)) /\ 493 basis g b /\ dim r g op < LENGTH b ==> ~LinearIndepBasis r g op b ==> 494 SUC v = LENGTH b - SUC (dim r g op) ==> ~LinearIndepBasis r g op b 495 Aim is to have b = h::t, then replace b by t in induction hypothesis. 496 Since dim r g op < LENGTH b, LENGTH b <> 0. 497 thus ?h t. b = h::t by LENGTH_NIL, list_CASES 498 From SUC v = LENGTH b - SUC (dim r g op) 499 = SUC (LENGTH t) - SUC (dim r g op) by LENGTH 500 so v = LENGTH t - SUC (dim r g op) by arithmetic 501 or SUC (dim r g op) <= LENGTH t by 0 <= v 502 or dim r g op < LENGTH t by arithmetic 503 Now h IN V /\ basis g t by basis_cons 504 and LinearIndepBasis r g op t by vspace_basis_indep_one_less 505 but ~LinearIndepBasis r g op t by induction hypothesis 506 which is a contradiction. 507*) 508val finite_vspace_basis_dep = store_thm( 509 "finite_vspace_basis_dep", 510 ``!(r:'a field) (g:'b group) op. FiniteVSpace r g op ==> 511 !b. basis g b /\ (dim r g op < LENGTH b) ==> ~LinearIndepBasis r g op b``, 512 rpt strip_tac >> 513 Induct_on `LENGTH b - SUC (dim r g op)` >| [ 514 rpt strip_tac >> 515 `LENGTH b = SUC (dim r g op)` by decide_tac >> 516 metis_tac[finite_vspace_basis_dep_special], 517 rpt strip_tac >> 518 `LENGTH b <> 0` by decide_tac >> 519 `?h t. b = h::t` by metis_tac[LENGTH_NIL, list_CASES] >> 520 `SUC v = SUC (LENGTH t) - SUC (dim r g op)` by rw[] >> 521 `v = LENGTH t - SUC (dim r g op)` by decide_tac >> 522 `dim r g op < LENGTH t` by decide_tac >> 523 metis_tac[basis_cons, vspace_basis_indep_one_less, finite_vspace_is_vspace] 524 ]); 525 526 527(* ------------------------------------------------------------------------- *) 528 529(* export theory at end *) 530val _ = export_theory(); 531 532(*===========================================================================*) 533