1(* ------------------------------------------------------------------------- *) 2(* Linear Independence *) 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 "LinearIndep"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16 17(* val _ = load "jcLib"; *) 18open jcLib; 19 20(* Get dependent theories local *) 21(* val _ = load "SpanSpaceTheory"; *) 22open VectorSpaceTheory SpanSpaceTheory; 23open monoidTheory groupTheory 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(* Linear Independence Documentation *) 35(* ------------------------------------------------------------------------- *) 36(* Overload: 37*) 38(* Definitions and Theorems (# are exported): 39 40 Change of Basis: 41 stick_rotate_length |- !r n1 n. n1 IN sticks r n ==> !k. rotate k n1 IN sticks r n 42 basis_rotate_once_basis |- !g b. basis g b ==> basis g (rotate 1 b) 43 basis_rotate_basis |- !g b. basis g b ==> !k. k < LENGTH b ==> basis g (rotate k b) 44 vsum_stick_rotate_once |- !r g op. VSpace r g op ==> !b. basis g b ==> 45 !n. n IN sticks r (LENGTH b) ==> (n |o| b = rotate 1 n |o| rotate 1 b) 46 vsum_stick_rotate |- !r g op. VSpace r g op ==> !b. basis g b ==> 47 !n. n IN sticks r (LENGTH b) ==> 48 !k. k < LENGTH b ==> (n |o| b = rotate k n |o| rotate k b) 49 vspace_span_with_rotate |- !r g op. VSpace r g op ==> !b. basis g b ==> 50 !k. k < LENGTH b ==> (SpanSpace r g op (rotate k b) = SpanSpace r g op b) 51 vspace_span_basis_shrink|- !r g op. VSpace r g op ==> !b. basis g b ==> 52 !n. n IN sticks r (LENGTH b) /\ (n |o| b = |0|) ==> 53 !k. k < LENGTH b /\ EL k n <> #0 ==> 54 (SpanSpace r g op (DROP (SUC k) b ++ TAKE k b) = SpanSpace r g op b) 55 56 Linear Independence: 57 LinearIndepBasis_def |- !r g op b. LinearIndepBasis r g op b <=> basis g b /\ 58 !n. n IN sticks r (LENGTH b) ==> 59 ((n |o| b = |0|) <=> !k. k < LENGTH b ==> (EL k n = #0)) 60 indep_basis_is_basis |- !r g op b. LinearIndepBasis r g op b ==> basis g b 61 indep_basis_property |- !r g op b. LinearIndepBasis r g op b ==> 62 !n. n IN sticks r (LENGTH b) ==> 63 ((n |o| b = |0|) <=> !k. k < LENGTH b ==> (EL k n = #0)) 64 65 vspace_indep_basis_inj |- !r g op. VSpace r g op ==> !b. LinearIndepBasis r g op b ==> 66 INJ (\n. n |o| b) (sticks r (LENGTH b)) V 67 vspace_basis_indep_one_less |- !r g op. VSpace r g op ==> 68 !h t. LinearIndepBasis r g op (h::t) ==> LinearIndepBasis r g op t 69 vspace_basis_dep_one_more |- !r g op. VSpace r g op ==> 70 !h t. ~LinearIndepBasis r g op t ==> ~LinearIndepBasis r g op (h::t) 71*) 72 73(* Overloads for convenience *) 74val _ = temp_overload_on ("o", ``(op:'a -> 'b -> 'b)``); 75val _ = temp_overload_on ("V", ``(g:'b group).carrier``); 76val _ = temp_overload_on ("||", ``(g:'b group).op``); 77val _ = temp_overload_on ("|0|", ``(g:'b group).id``); 78val _ = set_fixity "||" (Infixl 500); (* same as + in arithmeticScript.sml *) 79 80val _ = temp_overload_on ("+", ``stick_add r``); 81val _ = temp_overload_on ("-", ``stick_neg r``); 82val _ = temp_overload_on ("*", ``stick_cmult r``); 83val _ = temp_overload_on ("-", ``stick_sub r``); 84 85(* ------------------------------------------------------------------------- *) 86(* Change of Basis *) 87(* ------------------------------------------------------------------------- *) 88 89(* Note: rotate is defined in helperList. 90> rotate_def; 91val it = |- !n l. rotate n l = DROP n l ++ TAKE n l: thm 92 93This is a simple form of a change of basis by permutation. 94*) 95 96(* Theorem: !n1. n1 IN sticks r n ==> !k. (rotate k nl) IN sticks r n *) 97(* Proof: 98 By sticks_def, rotate_same_length, rotate_same_set. 99*) 100val stick_rotate_length = store_thm( 101 "stick_rotate_length", 102 ``!r:'a field. !n1 n. n1 IN sticks r n ==> !k. (rotate k n1) IN sticks r n``, 103 rw[sticks_def, rotate_same_length, rotate_same_set]); 104 105(* Theorem: !b. basis g b ==> basis g (rotate 1 b) *) 106(* Proof: 107 If b = [], 108 basis g (rotate 1 []) 109 = basis g [] by rotate_nil 110 = T by basis_nil 111 If b = h::t, h IN V /\ basis g t by basis_cons 112 rotate 1 (h::t) 113 = DROP (SUC 0) (h::t) ++ TAKE (SUC 0) (h::t) by ONE 114 = DROP 0 t ++ h::TAKE 0 t by DROP_def, TAKE_def 115 = b ++ [h] by DROP_def, TAKE_def 116 Since basis g b, !x. MEM x b <=> x IN V. by basis_member 117 With h IN V, !x. MEM x (b ++ [h]) <=> x IN V. 118 Hence basis g (b ++ [h]) by basis_member 119*) 120val basis_rotate_once_basis = store_thm( 121 "basis_rotate_once_basis", 122 ``!(g:'b group) (b:'b list). basis g b ==> basis g (rotate 1 b)``, 123 strip_tac >> 124 Cases_on `b` >- 125 rw[basis_nil, rotate_nil] >> 126 rw[basis_cons, rotate_def] >> 127 pop_assum mp_tac >> 128 rw[basis_member] >> 129 rw[]); 130 131(* Theorem: basis g b ==> !k. k < LENGTH b ==> basis g (rotate k b) *) 132(* Proof: 133 By induction on k. 134 Base case: 0 < LENGTH b ==> basis g (rotate 0 b) 135 basis g (rotate 0 b) = basis g b by rotate_0 136 Hence true. 137 Step case: SUC k < LENGTH b ==> basis g (rotate (SUC k) b) 138 i.e. k < LENGTH b. 139 basis g (rotate (SUC k) b) 140 = basis g (rotate 1 (rotate k b)) by rotate_suc 141 = T by basis_rotate_once_basis 142 due to basis g (rotate k b) by induction hypothesis 143*) 144val basis_rotate_basis = store_thm( 145 "basis_rotate_basis", 146 ``!(g:'b group) (b:'b list). basis g b ==> !k. k < LENGTH b ==> basis g (rotate k b)``, 147 rpt strip_tac >> 148 Induct_on `k` >- 149 rw[rotate_0] >> 150 rw[] >> 151 `k < LENGTH b` by decide_tac >> 152 rw[rotate_suc, basis_rotate_once_basis]); 153 154(* Theorem: basis g b ==> !n. n IN sticks r (LENGTH b) ==> n |o| b = (rotate 1 n) |o| (rotate 1 b) *) 155(* Proof: 156 If b = [], n IN sticks r 0 ==> n = [] by sticks_0, IN_SING. 157 RHS = (rotate 1 []) |o| (rotate 1 []) 158 = [] |o| [] by rotate_nil 159 = LHS 160 If b = h::t, LENGTH (h::t) = SUC (LENGTH t) by LENGTH 161 ?k s. k IN R /\ s IN sticks r (LENGTH t) /\ (n = k::s) by stick_cons 162 After expanding by vsum_cons and rotate_def, SNOC, this is to show: 163 k o h || (s |o| t) = (s ++ [k]) |o| (t ++ [h]) 164 RHS = (s ++ [k]) |o| (t ++ [h]) 165 = (SNOC k s) |o| (SNOC h t) by SNOC_APPEND 166 = k o h || (s |o| t) by vsum_stick_snoc 167 = LHS 168*) 169val vsum_stick_rotate_once = store_thm( 170 "vsum_stick_rotate_once", 171 ``!(r:'a field) (g:'b group) op. VSpace r g op ==> !b. basis g b ==> 172 !n. n IN sticks r (LENGTH b) ==> (n |o| b = (rotate 1 n) |o| (rotate 1 b))``, 173 rpt strip_tac >> 174 Cases_on `b` >| [ 175 pop_assum mp_tac >> 176 rw[] >> 177 `n = []` by metis_tac[sticks_0, IN_SING] >> 178 rw[rotate_nil], 179 pop_assum mp_tac >> 180 pop_assum mp_tac >> 181 rw[basis_cons, stick_cons] >> 182 rw[vsum_cons, rotate_def] >> 183 metis_tac[vsum_stick_snoc, SNOC_APPEND] 184 ]); 185 186(* Theorem: basis g b ==> 187 !n. n IN sticks r (LENGTH b) ==> !k. k < LENGTH b ==> n |o| b = (rotate k n) |o| (rotate k b) *) 188(* Proof: 189 By induction on b. 190 Base case: 0 < LENGTH b ==> (n |o| b = rotate 0 n |o| rotate 0 b) 191 Since rotate 0 n = n and rotate 0 b = b by rotate_0 192 This is true. 193 Step case: SUC k < LENGTH b ==> (n |o| b = rotate (SUC k) n |o| rotate (SUC k) b) 194 Since SUC k < LENGTH b implies k < LENGTH b, 195 and LENGTH n = LENGTH b by stick_length 196 and basis g (rotate k b) by basis_rotate_basis 197 RHS = rotate (SUC k) n |o| rotate (SUC k) b 198 = (rotate 1 (rotate k n)) |o| (rotate 1 (rotate k b)) by rotate_suc 199 = (rotate k n) |o| (rotate k b) by vsum_stick_rotate_once 200 = n |o| b by induction hypothesis 201 = LHS 202*) 203val vsum_stick_rotate = store_thm( 204 "vsum_stick_rotate", 205 ``!(r:'a field) (g:'b group) op. VSpace r g op ==> !b. basis g b ==> 206 !n. n IN sticks r (LENGTH b) ==> !k. k < LENGTH b ==> (n |o| b = (rotate k n) |o| (rotate k b))``, 207 ntac 8 strip_tac >> 208 Induct >- 209 rw[rotate_0] >> 210 rw[] >> 211 `k < LENGTH b` by decide_tac >> 212 `LENGTH n = LENGTH b` by metis_tac[stick_length] >> 213 `basis g (rotate k b)` by rw[basis_rotate_basis] >> 214 `(rotate k n) IN sticks r (LENGTH b)` by metis_tac[stick_rotate_length] >> 215 `LENGTH (rotate k b) = LENGTH b` by rw[rotate_same_length] >> 216 metis_tac[rotate_suc, vsum_stick_rotate_once]); 217 218(* Theorem: !k. k < LENGTH b ==> SpanSpace r g op (rotate k b) = SpanSpace r g op b *) 219(* Proof: 220 Note that LENGTH (rotate k b) = LENGTH b by rotate_same_length 221 Expanding by SpanSpace_def, using monoid_component_equality, this is to show: 222 (1) n IN sticks r (LENGTH b) ==> ?n'. (n |o| rotate k b = n' |o| b) /\ n' IN sticks r (LENGTH b) 223 Let n' = rotate (LENGTH b - k) n IN sticks r (LENGTH b) by stick_rotate_length 224 Then n' |o| b 225 = (rotate (LENGTH b - k) n) |o| b by n' = rotate (LENGTH b - k) n 226 = (rotate k (rotate (LENGTH b - k) n)) |o| (rotate k b) by vsum_stick_rotate 227 = n |o| (rotate k b) by rotate_rcancel 228 (2) n IN sticks r (LENGTH b) ==> ?n'. (n |o| b = n' |o| rotate k b) /\ n' IN sticks r (LENGTH b) 229 Let n' = rotate k n IN sticks r (LENGTH b) by stick_rotate_length 230 Then n' |o| (rotate k b) 231 = (rotate k n) |o| (rotate k b) by n' = rotate k n 232 = n |o| b by vsum_stick_rotate 233*) 234val vspace_span_with_rotate = store_thm( 235 "vspace_span_with_rotate", 236 ``!(r:'a field) (g:'b group) op. VSpace r g op ==> !b. basis g b ==> 237 !k. k < LENGTH b ==> (SpanSpace r g op (rotate k b) = SpanSpace r g op b)``, 238 rpt strip_tac >> 239 rw[SpanSpace_def, monoid_component_equality, rotate_same_length, EXTENSION, EQ_IMP_THM] >- 240 metis_tac[stick_rotate_length, stick_length, vsum_stick_rotate, rotate_rcancel] >> 241 metis_tac[vsum_stick_rotate, stick_rotate_length]); 242 243(* Theorem: Let n IN sticks r (LENGTH b) /\ (n |o| b = |0|) 244 If n is nonzero at index k, the basis b at same index k, after deletion (from list), 245 will span the same subspace. 246 basis g b ==> !n. n IN sticks r (LENGTH b) /\ (n |o| b = |0|) ==> 247 !k. k < LENGTH b /\ EL k n <> #0 ==> 248 (SpanSpace r g op (DROP (SUC k) b ++ TAKE k b) = SpanSpace r g op b) *) 249(* Proof: 250 Let u = EL k b, a vector in the basis b. 251 Let b' = DROP (SUC k) b ++ TAKE k b, a kind of mutated basis of b. 252 Note rotate k b = u::b' by rotate_shift_element 253 and u IN V /\ basis g b' by basis_rotate_basis, basis_cons 254 SpanSpace r g op b 255 = SpanSpace r g op (rotate k b) by vspace_span_with_rotate 256 = SpanSpace r g op (u::b') by rotate_shift_element 257 = SpanSpace r g op (b') by vspace_span_with_member 258 if u IN (SpanSpace r g op b').carrier, which is proved as: 259 260 Let h = EL k n, the corresponding scalar in sticks n. 261 To show: u IN (SpanSpace r g op b').carrier, i.e. u is spanned by basis b', 262 Trick is to show: (h o u) IN (SpanSpace r g op b').carrier, 263 Then u = |/h o (h o u) IN (SpanSpace r g op b').carrier by vspace_span_cmult. 264 265 Why does the trick works? Due to rotation: 266 Let n' = (DROP (SUC k) n ++ TAKE k n), a kind of mutated n to match b'. 267 Note k < LENGTH b means k < LENGTH n by stick_length, n IN sticks r (LENGTH b) 268 Then rotate k n = h::n' by rotate_shift_element 269 Thus |0| = n |o| b by given 270 = (rotate k n) |o| (rotate k b) by vsum_stick_rotate 271 = (h::n') |o| (u::b') by rotations above 272 = (h o u) || (n' |o| b') by vsum_stick_cons 273 Since Group (SpanSpace r g op b') by vspace_span_group 274 It is obvious that (n' |o| b') IN (SpanSpace r g op b').carrier (recall it is a span space), 275 and it is almost simple to argue that its inverse should be in the same carrier. 276 The actual path is still not so straight-forward. 277 278 (1) Let's try to show: (n' |o| b') IN (SpanSpace r g op b').carrier 279 This is true by vspace_span_property if: n' IN sticks r (LENGTH b') 280 Note rotate k n IN sticks r (LENGTH b) by stick_rotate_length 281 or h :: n' IN sticks r (LENGTH b) by rotate k n = h::n' above 282 or IN sticks r (LENGTH (rotate k b)) by rotate_same_length 283 or IN sticks r (LENGTH (u::b')) by rotate k b = u::b' above 284 or IN sticks r (SUC (LENGTH b')) by LENGTH 285 Thus ?h1 n1. h1 IN R /\ n1 IN sticks r (LENGTH b') 286 and (h :: n' = h1 :: n1) by stick_cons 287 or (h1 = h) /\ (n1 = n') by list_11 288 Hence n' IN sticks r (LENGTH b'). 289 and h IN R as bonus, although this can be deduced by stick_components_stick 290 (2) Now to show: h o u IN (SpanSpace r g op b').carrier 291 Let vv = n' |o| b'. 292 Then vv IN (SpanSpace r g op b').carrier by n' IN sticks r (LENGTH b'), above 293 thus ?uu. uu IN (SpanSpace r g op s).carrier, and 294 (uu || vv = |0|) by vspace_span_negative 295 Now uu IN V /\ vv IN V by vspace_span_vector 296 and h o u IN V by vspace_cmult_vector, h IN R, u IN V 297 With Group g by vspace_has_group 298 so h o u = uu by group_linv_unique, Group g 299 Thus h o u IN (SpanSpace r g op b').carrier by uu IN (SpanSpace r g op s).carrier 300 (3) With Field r by vspace_has_field 301 and h IN R+ by field_nonzero_eq, given h <> #0 302 so |/h IN R by field_inv_element, h IN R+ 303 Now |/h o (h o u) 304 = ( |/h * h) o u by vspace_cmult_cmult 305 = #1 o u by field_mult_linv, h IN R+ 306 = u by vspace_cmult_lone 307 Hence u = |/h o (h o u) IN (SpanSpace r g op b').carrier by vspace_span_cmult 308*) 309val vspace_span_basis_shrink = store_thm( 310 "vspace_span_basis_shrink", 311 ``!(r:'a field) (g:'b group) op. VSpace r g op ==> !b. basis g b ==> 312 !n. n IN sticks r (LENGTH b) /\ (n |o| b = |0|) ==> 313 !k. k < LENGTH b /\ EL k n <> #0 ==> 314 (SpanSpace r g op ((DROP (SUC k) b) ++ (TAKE k b)) = SpanSpace r g op b)``, 315 rpt strip_tac >> 316 qabbrev_tac `u = EL k b` >> 317 qabbrev_tac `h = EL k n` >> 318 qabbrev_tac `b' = DROP (SUC k) b ++ TAKE k b` >> 319 qabbrev_tac `n' = DROP (SUC k) n ++ TAKE k n` >> 320 `rotate k b = u::b'` by rw[rotate_shift_element, Abbr`u`, Abbr`b'`] >> 321 `rotate k n = h :: n'` by metis_tac[rotate_shift_element, stick_length] >> 322 `u IN V /\ basis g b'` by metis_tac[basis_cons, basis_rotate_basis] >> 323 `u IN (SpanSpace r g op b').carrier` by 324 (`h IN R /\ h o u IN (SpanSpace r g op b').carrier` by 325 (`rotate k n IN sticks r (SUC (LENGTH b'))` by metis_tac[stick_rotate_length, rotate_same_length, LENGTH] >> 326 `h IN R /\ n' IN sticks r (LENGTH b')` by metis_tac[stick_cons, list_11] >> 327 `(h o u) || (n' |o| b') = |0|` by metis_tac[vsum_stick_cons, vsum_stick_rotate] >> 328 qabbrev_tac `vv = n' |o| b'` >> 329 `vv IN (SpanSpace r g op b').carrier` by rw[vspace_span_property, Abbr`vv`] >> 330 `?uu. uu IN (SpanSpace r g op b').carrier /\ (uu || vv = |0|)` by rw[vspace_span_negative] >> 331 `uu IN V /\ vv IN V` by metis_tac[vspace_span_vector] >> 332 `h o u IN V` by metis_tac[vspace_cmult_vector] >> 333 `h o u = uu` by metis_tac[group_linv_unique, vspace_has_group] >> 334 rw[]) >> 335 `Field r` by metis_tac[vspace_has_field] >> 336 `h IN R+ /\ |/h IN R` by rw[field_nonzero_eq] >> 337 `|/h o (h o u) = ( |/h * h) o u` by metis_tac[vspace_cmult_cmult] >> 338 `_ = #1 o u` by rw[] >> 339 `_ = u` by metis_tac[vspace_cmult_lone] >> 340 metis_tac[vspace_span_cmult]) >> 341 metis_tac[vspace_span_with_rotate, rotate_shift_element, vspace_span_with_member]); 342 343(* 344If SpanSpace r g op b = SpanSpace r g op b', what is the condition on an additional vector h such that: 345 SpanSpace r g op (h::b) = SpanSpace r g op (h::b') ? 346If h is already spanned by b (or b'), (h::b) spans the same space. 347If h is not spanned by b (or b'), (h::b) gives another dimension, same as (h::b'). 348*) 349 350(* ------------------------------------------------------------------------- *) 351(* Linear Independence. *) 352(* ------------------------------------------------------------------------- *) 353 354(* In general, vectors in basis b may or may not be linearly independent. 355 However, if a vector has two sticks representations: 356 e.g. 4 o (v) || 4 o (-v) = 3 o (v) || 3 o (-v) 357 then 1 o (v) || 1 o (-v) = |0| 358 i.e. there is another sticks of the same length giving a nonzero representation of zero vector. 359*) 360 361(* Better formulation: if vector zero has only zero-representation, 362 then any vector has a unique representation. *) 363 364(* Linearly Independent basis has only one representation of zero vector *) 365val LinearIndepBasis_def = Define` 366 LinearIndepBasis (r:'a field) (g:'b group) (op:'a -> 'b -> 'b) (b:'b list) <=> 367 (basis g b) /\ 368 !n. n IN sticks r (LENGTH b) ==> ((n |o| b = |0|) <=> !k. k < LENGTH b ==> (EL k n = #0)) 369`; 370 371(* Theorem: LinearIndepBasis r g op b ==> basis g b *) 372(* Proof: by LinearIndepBasis_def *) 373val indep_basis_is_basis = store_thm( 374 "indep_basis_is_basis", 375 ``!(r:'a field) (g:'b group) op b. LinearIndepBasis r g op b ==> basis g b``, 376 rw[LinearIndepBasis_def]); 377 378(* Theorem: LinearIndepBasis r g op b ==> 379 !n. n IN sticks r (LENGTH b) ==> ((n |o| b = |0|) <=> !k. k < LENGTH b ==> (EL k n = #0)) *) 380(* Proof: by LinearIndepBasis_def *) 381val indep_basis_property = store_thm( 382 "indep_basis_property", 383 ``!(r:'a field) (g:'b group) op b. LinearIndepBasis r g op b ==> 384 !n. n IN sticks r (LENGTH b) ==> ((n |o| b = |0|) <=> !k. k < LENGTH b ==> (EL k n = #0))``, 385 rw[LinearIndepBasis_def]); 386 387(* Theorem: LinearIndepBasis r g op b ==> INJ (\n. n |o| b) (sticks r (LENGTH b)) V *) 388(* Proof: 389 Note basis g b by indep_basis_is_basis 390 By INJ_DEF, this is to show: 391 (1) n IN sticks r (LENGTH b) ==> n |o| b IN V 392 True by vsum_basis_stick_vector. 393 (2) n IN sticks r (LENGTH b) /\ n' IN sticks r (LENGTH b) /\ (n |o| b = n' |o| b) ==> n = n' 394 Note (n |o| b) IN V /\ (n' |o| b) IN V by vsum_basis_stick_vector 395 Then (n - n') |o| b 396 = (n |o| b) || g.inv (n' |o| b) by vsum_stick_sub 397 = |0| by group_rinv, given n |o| b = n' |o| b 398 As n - n' IN sticks r (LENGTH b) by stick_sub_length 399 !k. k < LENGTH b ==> (EL k (n - n') = #0) by indep_basis_property 400 Hence n = n' by stick_eq_property. 401*) 402val vspace_indep_basis_inj = store_thm( 403 "vspace_indep_basis_inj", 404 ``!(r:'a field) (g:'b group) op. VSpace r g op ==> 405 !b. LinearIndepBasis r g op b ==> INJ (\n. n |o| b) (sticks r (LENGTH b)) V``, 406 rw[INJ_DEF, LinearIndepBasis_def] >- 407 metis_tac[vsum_basis_stick_vector] >> 408 `(n - n') |o| b = (n |o| b) || g.inv (n' |o| b)` by rw[vsum_stick_sub] >> 409 `n |o| b IN V /\ n' |o| b IN V` by metis_tac[vspace_span_vector, vspace_span_property] >> 410 `(n - n') |o| b = |0|` by metis_tac[group_rinv, vspace_has_group] >> 411 `Field r` by metis_tac[vspace_has_field] >> 412 `n - n' IN sticks r (LENGTH b)` by rw[stick_sub_length] >> 413 metis_tac[stick_eq_property]); 414 415(* Theorem: Reduce-by-1 of linear indepedent basis is still linear independent: 416 LinearIndepBasis r g op (h::t) ==> LinearIndepBasis r g op t *) 417(* Proof: 418 By LinearIndepBasis_def, this is to show: 419 !n. n IN sticks r (SUC (LENGTH t)) ==> 420 ((n |o| (h::t) = |0|) <=> !k. k < SUC (LENGTH t) ==> (EL k n = #0)) 421 422 By contradiction, need to find m IN sticks r (SUC (LENGTH t)) 423 such that ((m |o| (h::t) = |0|) <=/=> !k. k < SUC (LENGTH t) ==> (EL k m = #0)) 424 425 Note VSpace r g op ==> Field r by vspace_has_field 426 VSpace r g op ==> Group g by vspace_has_group 427 Let m = #0 :: n, that is, appending #0 to the sticks n. 428 Then m IN sticks r (SUC (LENGTH t)) by stick_cons, LENGTH 429 Note (n |o| t) IN V by vsum_stick_basis_vector 430 Also m |o| (h::t) 431 = (#0::n) |o| (h::t) 432 = #0 o h || (n |o| t) by vsum_cons, MAP2 433 = |0| || (n |o| t) by vspace_cmult_lzero 434 = (n |o| t) by group_lid, (n |o| t) IN V 435 436 Now !k . k < LENGTH t <=> SUC k < SUC (LENGTH t) by LESS_MONO 437 and !k. EL (SUC k) (#0::n) = EL k n by EL_restricted 438 also EL 0 (#0::n) = #0 by EL, HD 439 440 The assumed LinearIndepBasis r g op (h::t) gives: 441 !n'. n' IN sticks r (SUC (LENGTH t)) ==> 442 ((n' |o| (h::t) = |0|) <=> !k. k < SUC (LENGTH t) ==> (EL k n' = #0)) 443 444 To derive the contradiction, need to show: 445 (1) (n |o| t = |0|) /\ k < (LENGTH t) /\ EL k n <> #0 ==> F 446 Putting m as n', k as (SUC k) in the if implication, 447 EL (SUC k) m = #0, 448 or EL (SUC k) m = EL (SUC k) (#0::n) = EL k n = #0, contradicting EL k n <> #0. 449 (2) (!k. k < (LENGTH t) ==> (EL k n = #0)) /\ (n |o| t <> |0|) ==> F 450 Putting m as n', k as (SUC k) in the only-if implication, and consider cases on k, 451 m |o| (h::t) = |0| 452 or n |o| t = |0|. 453*) 454val vspace_basis_indep_one_less = store_thm( 455 "vspace_basis_indep_one_less", 456 ``!(r:'a field) (g:'b group) op. VSpace r g op ==> 457 !h t. LinearIndepBasis r g op (h::t) ==> LinearIndepBasis r g op t``, 458 rw[LinearIndepBasis_def, basis_cons] >> 459 `Field r` by metis_tac[vspace_has_field] >> 460 `Group g` by metis_tac[vspace_has_group] >> 461 qabbrev_tac `m = #0 :: n` >> 462 `m IN sticks r (SUC (LENGTH t))` by rw[stick_cons, Abbr`m`] >> 463 `n |o| t IN V` by metis_tac[vsum_basis_stick_vector] >> 464 `m |o| (h::t) = #0 o h || (n |o| t)` by rw[vsum_cons, Abbr`m`] >> 465 `_ = |0| || (n |o| t)` by metis_tac[vspace_cmult_lzero] >> 466 `_ = n |o| t` by rw[] >> 467 `!k . k < LENGTH t <=> SUC k < SUC (LENGTH t)` by decide_tac >> 468 `!k. EL (SUC k) (#0::n) = EL k n` by metis_tac[EL_restricted] >> 469 `EL 0 (#0::n) = #0` by rw[Abbr`m`] >> 470 rw_tac bool_ss[EQ_IMP_THM] >- 471 metis_tac[] >> 472 metis_tac[num_CASES]); 473 474(* Theorem: Add-by-1 of a linear dependent basis is still linear dependent: 475 ~LinearIndepBasis r g op t ==> ~LinearIndepBasis r g op (h::t) *) 476(* Proof: by contrapositive of vspace_basis_indep_one_less. *) 477val vspace_basis_dep_one_more = store_thm( 478 "vspace_basis_dep_one_more", 479 ``!(r:'a field) (g:'b group) op. VSpace r g op ==> 480 !h t. ~LinearIndepBasis r g op t ==> ~LinearIndepBasis r g op (h::t)``, 481 metis_tac[vspace_basis_indep_one_less]); 482 483 484(* ------------------------------------------------------------------------- *) 485 486(* export theory at end *) 487val _ = export_theory(); 488 489(*===========================================================================*) 490