1(* ------------------------------------------------------------------------- *) 2(* Vector Space *) 3(* ------------------------------------------------------------------------- *) 4 5(* 6 7Overall Idea: 8* Have a list of vectors, called basis. 9* Have a list of scalars, called stick. Let sticks r m = set of sticks of length m. 10* Given a basis b, with m = LENGTH b, get the (sticks r m). 11* Combine stick n IN (sticks r m) and basis into pairs: ZIP (n, b) 12* Turn the list of pairs into a list of vectors by scalar multiplication: MAP op (ZIP (n, b)) 13* Sum up this list of vectors to give a final vector: VSUM (MAP op (ZIP (n, b))) 14 where VSUM [] = |0| 15 and VSUM (h::t) = h || VSUM t 16* The set of vectors given by this process is the SpanSpace of the basis. 17 SpanSpace r g op b = <| carrier := { VSUM (MAP2 op n, b) | n | n IN (sticks r (LENGTH b)) }; 18 op := g.op 19 id := g.id 20 |> 21* Then show: !b. VSpace r (SpanSpace r g op b) op 22* And show: VSpace r g op = SpanSpace r g op (SET_TO_LIST V), i.e. all vectors can be a basis. 23* Thus the set: s = { b | VSpace r g op = SpanSpace r g op b } is non-empty. 24 And IMAGE CARD s is a bunch of numbers, none of them zero. 25 Let DIM (VSpace r g op) = MIN_SET (IMAGE CARD { b | VSpace r g op = SpanSpace r g op b }) 26* By IN_IMAGE, there is a basis b such that CARD b = DIM (VSpace r g op). 27* Then show: CARD V = (CARD R) ** DIM (VSpace r g op) 28 Possibly, this involves showing n IN (sticks r (LENGTH b)) --> VSUM (MAP op (ZIP (n, b))) is INJ. 29 30*) 31 32(*===========================================================================*) 33 34(* add all dependent libraries for script *) 35open HolKernel boolLib bossLib Parse; 36 37(* declare new theory at start *) 38val _ = new_theory "VectorSpace"; 39 40(* ------------------------------------------------------------------------- *) 41 42 43 44(* val _ = load "jcLib"; *) 45open jcLib; 46 47(* Get dependent theories local *) 48(* val _ = load "fieldTheory"; *) 49open groupTheory fieldTheory; 50 51(* Get dependent theories in lib *) 52(* val _ = load "helperListTheory"; *) 53open helperNumTheory helperSetTheory helperListTheory; 54 55(* open dependent theories *) 56open pred_setTheory listTheory arithmeticTheory; 57 58 59(* ------------------------------------------------------------------------- *) 60(* Vector Space Documentation *) 61(* ------------------------------------------------------------------------- *) 62(* Overload: 63 o = op 64 V = g.carrier 65 |0| = g.id 66 u || v = g.op u v 67 n + m = stick_add r n m 68 n - m = stick_sub r n m 69 $- n = stick_neg r n 70 c * n = stick_cmult r c n 71*) 72(* Definitions and Theorems (# are exported): 73 74 Vector Space: 75 VSpace_def |- !r g op. VSpace r g op <=> 76 Field r /\ AbelianGroup g /\ 77 (!a v. a IN R /\ v IN V ==> a o v IN V) /\ 78 (!a b v. a IN R /\ b IN R /\ v IN V ==> (a o b o v = (a * b) o v)) /\ 79 (!v. v IN V ==> (#1 o v = v)) /\ 80 (!a u v. a IN R /\ u IN V /\ v IN V ==> (a o (u || v) = a o u || a o v)) /\ 81 !a b v. a IN R /\ b IN R /\ v IN V ==> ((a + b) o v = a o v || b o v) 82 Basic Properties: 83 vspace_has_field |- !r op g. VSpace r g op ==> Field r 84 vspace_has_abelian_group |- !r op g. VSpace r g op ==> AbelianGroup g 85 vspace_cmult_vector |- !r op g. VSpace r g op ==> !a v. a IN R /\ v IN V ==> a o v IN V 86 vspace_cmult_cmult |- !r op g. VSpace r g op ==> !a b v. a IN R /\ b IN R /\ v IN V ==> 87 (a o b o v = (a * b) o v) 88 vspace_cmult_lone |- !r op g. VSpace r g op ==> !v. v IN V ==> (#1 o v = v) 89 vspace_cmult_radd |- !r op g. VSpace r g op ==> !a u v. a IN R /\ u IN V /\ v IN V ==> 90 (a o (u || v) = a o u || a o v) 91 vspace_cmult_ladd |- !r op g. VSpace r g op ==> !a b v. a IN R /\ b IN R /\ v IN V ==> 92 ((a + b) o v = a o v || b o v) 93 vspace_has_group |- !r g op. VSpace r g op ==> Group g 94 vspace_has_zero |- !r g op. VSpace r g op ==> |0| IN V 95 vspace_vadd_vector |- !r g op. VSpace r g op ==> !u v. u IN V /\ v IN V ==> u || v IN V 96 vspace_vadd_lzero |- !r g op. VSpace r g op ==> !v. v IN V ==> ( |0| || v = v) 97 vspace_vadd_rzero |- !r g op. VSpace r g op ==> !v. v IN V ==> (v || |0| = v) 98 vspace_vadd_comm |- !r g op. VSpace r g op ==> !u v. u IN V /\ v IN V ==> (u || v = v || u 99 vspace_vadd_assoc |- !r g op. VSpace r g op ==> !u v w. u IN V /\ v IN V /\ w IN V ==> 100 (u || v || w = u || (v || w)) 101 vspace_cmult_lzero |- !r g op. VSpace r g op ==> !v. v IN V ==> (#0 o v = |0|) 102 vspace_cmult_rzero |- !r g op. VSpace r g op ==> !a. a IN R ==> (a o |0| = |0|) 103 vspace_cmult_eq_zero |- !r g op. VSpace r g op ==> !a v. a IN R /\ v IN V ==> 104 ((a o v = |0|) <=> (a = #0) \/ (v = |0|)) 105 vspace_vsub_eq_zero |- !r g op. VSpace r g op ==> 106 !u v. u IN V /\ v IN V ==> ((u = v) <=> (u || -#1 o v = |0|)) 107 vspace_vsub_eq_zero_alt |- !r g op. VSpace r g op ==> 108 !u v. u IN V /\ v IN V ==> ((u = v) <=> (-#1 o u || v = |0|)) 109 vspace_vadd_eq_zero |- !r g op. VSpace r g op ==> 110 !u v. u IN V /\ v IN V ==> ((u || v = |0|) <=> (u = -#1 o v)) 111 vspace_vadd_eq_zero_alt |- !r g op. VSpace r g op ==> 112 !u v. u IN V /\ v IN V ==> ((u || v = |0|) <=> (v = -#1 o u)) 113 114 Sticks: 115 sticks_def |- !r m. sticks r m = {l | set l SUBSET R /\ (LENGTH l = m)} 116 sticks_0 |- !r. sticks r 0 = {[]} 117 sticks_suc |- !r. sticks r (SUC n) = IMAGE (\(e,l). e::l) (R CROSS sticks r n) 118 sticks_finite |- !r. FINITE R ==> !n. FINITE (sticks r n) 119 sticks_card |- !r. FINITE R ==> !n. CARD (sticks r n) = CARD R ** n 120 sticks_1 |- !r. sticks r 1 = IMAGE (\c. [c]) R 121 sticks_1_member |- !r p. p IN sticks r 1 <=> ?c. c IN R /\ (p = [c]) 122 sticks_0_member |- !r p. p IN sticks r 0 <=> (p = []) 123 124 Stick Properties: 125 stick_length |- !r l n. l IN sticks r n ==> (LENGTH l = n) 126 stick_cons |- !r l n. l IN sticks r (SUC n) <=> ?h t. h IN R /\ t IN sticks r n /\ (l = h::t) 127 stick_all_zero |- !r g op. VSpace r g op ==> !n. GENLIST (\j. #0) n IN sticks r n 128 stick_insert_element 129 |- !r h t n. h IN R /\ t IN sticks r (n - 1) ==> 130 !k. k < n ==> TAKE k t ++ [h] ++ DROP k t IN sticks r n 131 stick_components_stick 132 |- !r t n. t IN sticks r n ==> !k. k < n ==> 133 EL k t IN R /\ TAKE k t IN sticks r k /\ DROP (SUC k) t IN sticks r (n - SUC k) 134 stick_snoc |- !r l n. l IN sticks r (SUC n) <=> 135 ?h t. h IN R /\ t IN sticks r n /\ (l = SNOC h t) 136 137 Stick Addition: 138 stick_add_def |- (!r. [] + [] = []) /\ !t' t r h' h. (h::t) + (h'::t') = h + h'::t + t' 139 stick_add_nil_nil |- !r. [] + [] = [] 140 stick_add_cons_cons |- !t' t r h' h. (h::t) + (h'::t') = h + h'::t + t' 141 stick_add_length |- !r. Field r ==> !n n1 n2. n1 IN sticks r n /\ n2 IN sticks r n ==> 142 n1 + n2 IN sticks r n 143 144 Stick Negation: 145 stick_neg_def |- (!r. $- [] = []) /\ !r h t. $- (h::t) = -h:: $- t 146 stick_neg_zero |- !r. $- [] = [] 147 stick_neg_cons |- !r h t. $- (h::t) = -h:: $- t 148 stick_neg_length |- !r. Field r ==> !n n1. n1 IN sticks r n ==> $- n1 IN sticks r n 149 150 Stick Scalar Multiplication: 151 stick_cmult_def |- (!r c. c * [] = []) /\ !r c h t. c * (h::t) = c * h::c * t 152 stick_cmult_zero |- !r c. c * [] = [] 153 stick_cmult_cons |- !r c h t. c * (h::t) = c * h::c * t 154 stick_cmult_length |- !r. Field r ==> !n c n1. c IN R /\ n1 IN sticks r n ==> c * n1 IN sticks r n 155 156 Stick Subtraction: 157 stick_sub_def |- (!r. [] - [] = []) /\ !t' t r h' h. (h::t) - (h'::t') = h - h'::t - t' 158 stick_sub_nil_nil |- !r. [] - [] = [] 159 stick_sub_cons_cons|- !t' t r h' h. (h::t) - (h'::t') = h - h'::t - t' 160 stick_sub_alt |- !r. Field r ==> !n n1 n2. n1 IN sticks r n /\ n2 IN sticks r n ==> 161 (n1 - n2 = n1 + $- n2) 162 stick_sub_length |- !r. Field r ==> !n n1 n2. n1 IN sticks r n /\ n2 IN sticks r n ==> 163 n1 - n2 IN sticks r n 164 stick_eq_property |- !r. Field r ==> !n n1 n2. n1 IN sticks r n /\ n2 IN sticks r n ==> 165 ((n1 = n2) <=> !k. k < n ==> (EL k (n1 - n2) = #0)) 166 167*) 168 169(* ------------------------------------------------------------------------- *) 170(* Vector Space *) 171(* ------------------------------------------------------------------------- *) 172 173(* Vector Space over a Field: 174 - a set of scalars (field elements), a set of vectors. 175 - vectors have addition, form an abelian group. 176 - scalars can multiply into vectors to give vectors. 177 - scalars and vectors can distrbute over each other. 178*) 179 180(* Axioms of Vector Space *) 181val VSpace_def = Define` 182 VSpace (r:'a field) (g:'b group) (op:'a -> 'b -> 'b) <=> 183 Field r /\ (* scalars from a field *) 184 AbelianGroup g /\ (* vectors form a commutative additive group *) 185 (!a v. a IN R /\ v IN g.carrier ==> (op a v) IN g.carrier) /\ (* scalar multiplication with vector gives vector *) 186 (!a b v. a IN R /\ b IN R /\ v IN g.carrier ==> (op a (op b v) = op (a * b) v)) /\ (* compatibility of scalar multiplication *) 187 (!v. v IN g.carrier ==> (op #1 v = v)) /\ (* identity of scalar multiplication *) 188 (!a u v. a IN R /\ u IN g.carrier /\ v IN g.carrier ==> 189 (op a (g.op u v) = g.op (op a u) (op a v))) /\ (* distribution of scalar over vector *) 190 (!a b v. a IN R /\ b IN R /\ v IN g.carrier ==> 191 (op (a + b) v = g.op (op a v) (op b v))) (* distribution of vector over scalar *) 192`; 193 194(* Overloads for convenience *) 195val _ = temp_overload_on ("o", ``(op:'a -> 'b -> 'b)``); 196val _ = temp_overload_on ("V", ``(g:'b group).carrier``); 197val _ = temp_overload_on ("||", ``(g:'b group).op``); 198val _ = temp_overload_on ("|0|", ``(g:'b group).id``); 199val _ = set_fixity "||" (Infixl 500); (* same as + in arithmeticScript.sml *) 200 201(* 202> VSpace_def; 203val it = |- !r g op. VSpace r g op <=> 204 Field r /\ AbelianGroup g /\ 205 (!a v. a IN R /\ v IN V ==> a o v IN V) /\ 206 (!a b v. a IN R /\ b IN R /\ v IN V ==> (a o b o v = (a * b) o v)) /\ 207 (!v. v IN V ==> (#1 o v = v)) /\ 208 (!a u v. a IN R /\ u IN V /\ v IN V ==> (a o (u || v) = a o u || a o v)) /\ 209 !a b v. a IN R /\ b IN R /\ v IN V ==> ((a + b) o v = a o v || b o v): thm 210*) 211 212(* ------------------------------------------------------------------------- *) 213(* Basic Properties. *) 214(* ------------------------------------------------------------------------- *) 215 216(* Theorem: VSpace r g op ==> Field r *) 217val vspace_has_field = save_thm("vspace_has_field", 218 VSpace_def |> SPEC_ALL |> (#1 o EQ_IMP_RULE) |> UNDISCH |> CONJUNCTS |> el 1 |> DISCH_ALL |> GEN_ALL); 219(* > val vspace_has_field = |- !r op g. VSpace r g op ==> Field r : thm *) 220 221(* Theorem: VSpace r g op ==> AbelianGroup g *) 222val vspace_has_abelian_group = save_thm("vspace_has_abelian_group", 223 VSpace_def |> SPEC_ALL |> (#1 o EQ_IMP_RULE) |> UNDISCH |> CONJUNCTS |> el 2 |> DISCH_ALL |> GEN_ALL); 224(* > val vspace_has_abelian_group = |- !r op g. VSpace r g op ==> AbelianGroup g : thm *) 225 226(* Theorem: VSpace r g op ==> !a v. a IN R /\ v IN V ==> a o v IN V *) 227val vspace_cmult_vector = save_thm("vspace_cmult_vector", 228 VSpace_def |> SPEC_ALL |> (#1 o EQ_IMP_RULE) |> UNDISCH |> CONJUNCTS |> el 3 |> DISCH_ALL |> GEN_ALL); 229(* > val vspace_cmult_vector = |- !r op g. VSpace r g op ==> !a v. a IN R /\ v IN V ==> a o v IN V : thm *) 230 231(* Theorem: VSpace r g op ==> !a b v. a IN R /\ b IN R /\ v IN V ==> (a o b o v = (a * b) o v) *) 232val vspace_cmult_cmult = save_thm("vspace_cmult_cmult", 233 VSpace_def |> SPEC_ALL |> (#1 o EQ_IMP_RULE) |> UNDISCH |> CONJUNCTS |> el 4 |> DISCH_ALL |> GEN_ALL); 234(* > val vspace_cmult_cmult = |- !r op g. VSpace r g op ==> 235 !a b v. a IN R /\ b IN R /\ v IN V ==> (a o b o v = (a * b) o v) : thm *) 236 237(* Theorem: VSpace r g op ==> !v. v IN V ==> (#1 o v = v) *) 238val vspace_cmult_lone = save_thm("vspace_cmult_lone", 239 VSpace_def |> SPEC_ALL |> (#1 o EQ_IMP_RULE) |> UNDISCH |> CONJUNCTS |> el 5 |> DISCH_ALL |> GEN_ALL); 240(* > val vspace_cmult_lone = |- !r op g. VSpace r g op ==> !v. v IN V ==> (#1 o v = v) : thm *) 241 242(* Theorem: VSpace r g op ==> !a u v. a IN R /\ u IN V /\ v IN V ==> (a o (u || v) = a o u || a o v) *) 243val vspace_cmult_radd = save_thm("vspace_cmult_radd", 244 VSpace_def |> SPEC_ALL |> (#1 o EQ_IMP_RULE) |> UNDISCH |> CONJUNCTS |> el 6 |> DISCH_ALL |> GEN_ALL); 245(* > val vspace_cmult_radd = |- !r op g. VSpace r g op ==> !a u v. a IN R /\ u IN V /\ v IN V ==> 246 (a o (u || v) = a o u || a o v) : thm *) 247 248(* Theorem: VSpace r g op ==> !a b v. a IN R /\ b IN R /\ v IN V ==> ((a + b) o v = a o v || b o v) *) 249val vspace_cmult_ladd = save_thm("vspace_cmult_ladd", 250 VSpace_def |> SPEC_ALL |> (#1 o EQ_IMP_RULE) |> UNDISCH |> CONJUNCTS |> el 7 |> DISCH_ALL |> GEN_ALL); 251(* > val vspace_cmult_ladd = |- !r op g. VSpace r g op ==> !a b v. a IN R /\ b IN R /\ v IN V ==> 252 ((a + b) o v = a o v || b o v) : thm *) 253 254(* Theorem: VSpace r g op ==> Group g *) 255(* Proof: by vspace_has_abelian_group, AbelianGroup_def. *) 256val vspace_has_group = store_thm( 257 "vspace_has_group", 258 ``!(r:'a field) (g:'b group) op. VSpace r g op ==> Group g``, 259 metis_tac[vspace_has_abelian_group, AbelianGroup_def]); 260 261(* Theorem: VSpace r g op ==> |0| IN V *) 262(* Proof: by vspace_has_group, group_id_element. *) 263val vspace_has_zero = store_thm( 264 "vspace_has_zero", 265 ``!(r:'a field) (g:'b group) op. VSpace r g op ==> |0| IN V``, 266 metis_tac[vspace_has_group, group_id_element]); 267 268(* Theorem: VSpace r g op ==> !u v. u IN V /\ v IN V ==> u || v IN V *) 269(* Proof: by vspace_has_group, group_op_element. *) 270val vspace_vadd_vector = store_thm( 271 "vspace_vadd_vector", 272 ``!(r:'a field) (g:'b group) op. VSpace r g op ==> !u v. u IN V /\ v IN V ==> u || v IN V``, 273 metis_tac[vspace_has_group, group_op_element]); 274 275(* Theorem: VSpace r g op ==> !v. v IN V ==> ( |0| || v = v) *) 276(* Proof: by vspace_has_group, group_lid. *) 277val vspace_vadd_lzero = store_thm( 278 "vspace_vadd_lzero", 279 ``!(r:'a field) (g:'b group) op. VSpace r g op ==> !v. v IN V ==> ( |0| || v = v)``, 280 metis_tac[vspace_has_group, group_lid]); 281 282(* Theorem: VSpace r g op ==> !v. v IN V ==> (v || |0| = v) *) 283(* Proof: by vspace_has_group, group_rid. *) 284val vspace_vadd_rzero = store_thm( 285 "vspace_vadd_rzero", 286 ``!(r:'a field) (g:'b group) op. VSpace r g op ==> !v. v IN V ==> (v || |0| = v)``, 287 metis_tac[vspace_has_group, group_rid]); 288 289(* Theorem: VSpace r g op ==> !u v. u IN V /\ v IN V ==> (u || v = v || u) *) 290(* Proof: by vspace_has_abelian_group, AbelianGroup_def. *) 291val vspace_vadd_comm = store_thm( 292 "vspace_vadd_comm", 293 ``!(r:'a field) (g:'b group) op. VSpace r g op ==> 294 !u v. u IN V /\ v IN V ==> (u || v = v || u)``, 295 metis_tac[vspace_has_abelian_group, AbelianGroup_def]); 296 297(* Theorem: VSpace r g op ==> !u v w. u IN V /\ v IN V /\ w IN V ==> (u || v || w = u || (v || w)) *) 298(* Proof: by vspace_has_group, group_assoc. *) 299val vspace_vadd_assoc = store_thm( 300 "vspace_vadd_assoc", 301 ``!(r:'a field) (g:'b group) op. VSpace r g op ==> 302 !u v w. u IN V /\ v IN V /\ w IN V ==> (u || v || w = u || (v || w))``, 303 metis_tac[vspace_has_group, group_assoc]); 304 305(* Theorem: #0 o v = |0| *) 306(* Proof: 307 v = #1 o v by vspace_cmult_lone 308 = (#0 + #1) o v by field_add_lzero 309 = #0 o v || #1 o v by vspace_cmult_ladd 310 = #0 o v || v by vspace_cmult_lone 311 hence #0 o v = |0| by group_rid_unique 312*) 313val vspace_cmult_lzero = store_thm( 314 "vspace_cmult_lzero", 315 ``!(r:'a field) (g:'b group) op. VSpace r g op ==> !v. v IN V ==> (#0 o v = |0|)``, 316 rpt strip_tac >> 317 `Field r /\ Group g` by metis_tac[VSpace_def, AbelianGroup_def] >> 318 `#0 IN R /\ #1 IN R` by rw[] >> 319 `#0 o v IN V` by metis_tac[vspace_cmult_vector] >> 320 `v = #1 o v` by metis_tac[vspace_cmult_lone] >> 321 `_ = (#0 + #1) o v` by rw[] >> 322 `_ = (#0 o v) || (#1 o v)` by rw[vspace_cmult_ladd] >> 323 `_ = #0 o v || v` by metis_tac[vspace_cmult_lone] >> 324 metis_tac[group_lid_unique]); 325 326(* Theorem: a IN R ==> a o |0| = |0| *) 327(* Proof: 328 a o |0| 329 = a o ( |0| || |0|) by group_id_id 330 = a o |0| || a o |0| by vspace_cmult_radd 331 hence a o |0}= |0| by group_id_fix 332*) 333val vspace_cmult_rzero = store_thm( 334 "vspace_cmult_rzero", 335 ``!(r:'a field) (g:'b group) op. VSpace r g op ==> !a. a IN R ==> (a o |0| = |0|)``, 336 rpt strip_tac >> 337 `Group g` by metis_tac[vspace_has_group] >> 338 `|0| IN V` by rw[] >> 339 `a o |0| IN V` by metis_tac[vspace_cmult_vector] >> 340 `a o |0| = a o ( |0| || |0|)` by rw[group_id_id] >> 341 `_ = a o |0| || a o |0|` by metis_tac[vspace_cmult_radd] >> 342 metis_tac[group_id_fix]); 343 344(* Theorem: a IN R /\ v IN V ==> a o v = |0| <=> a = #0 or v = |0| *) 345(* Proof: 346 If part: a IN R /\ v IN V /\ a o v = |0| ==> a = #0 or v = |0| 347 If a = #0, this is trivially true. 348 If a <> #0, |/a exists, and |/a * a = #1 349 v = #1 o v by vspace_cmult_lone 350 = ( |/a * a) o v by field_mult_linv 351 = |/a * (a o v) by vspace_cmult_cmult 352 = |/a * |0| by given 353 = |0| by vspace_cmult_rzero 354 Only-if part: a IN R /\ v IN V /\ a = #0 or v = |0| ==> a o v = |0| 355 If a = #0, #0 o v = |0| by vspace_cmult_lzero 356 If v = |0|, a o |0| = |0| by vspace_cmult_rzero 357*) 358val vspace_cmult_eq_zero = store_thm( 359 "vspace_cmult_eq_zero", 360 ``!(r:'a field) (g:'b group) op. VSpace r g op ==> 361 !a v. a IN R /\ v IN V ==> ((a o v = |0|) <=> (a = #0) \/ (v = |0|))``, 362 rw[EQ_IMP_THM] >| [ 363 `Field r` by metis_tac[vspace_has_field] >> 364 spose_not_then strip_assume_tac >> 365 `a IN R+` by rw[field_nonzero_eq] >> 366 `|/a IN R` by rw[] >> 367 `v = #1 o v` by metis_tac[vspace_cmult_lone] >> 368 metis_tac[field_mult_linv, vspace_cmult_cmult, vspace_cmult_rzero], 369 metis_tac[vspace_cmult_lzero], 370 metis_tac[vspace_cmult_rzero] 371 ]); 372 373(* Theorem: u IN V /\ v IN V ==> ((u = v) <=> (u || (- #1) o v = |0|)) *) 374(* Proof: 375 If part: u = v ==> u || -#1 o v = |0| 376 u || -#1 o v 377 = u || -#1 o u by given 378 = #1 o u || -#1 o u by vspace_cmult_lone 379 = (#1 + -#1) o u by vspace_cmult_ladd 380 = #0 o u by field_add_rneg 381 = |0| by vspace_cmult_lzero 382 Only-if part: u || -#1 o v = |0| ==> u = v 383 u 384 = u || |0| by vspace_vadd_rzero 385 = u || #0 o v by vspace_cmult_lzero 386 = u || (-#1 + #1) o v by field_add_lneg 387 = u || (-#1 o v || #1 o v) by vspace_cmult_ladd 388 = u || (-#1 o v || v) by vspace_cmult_lone 389 = (u || -#1 o v) || v by vspace_vadd_assoc 390 = |0| || v by given 391 = v by vspace_vadd_lzero 392*) 393val vspace_vsub_eq_zero = store_thm( 394 "vspace_vsub_eq_zero", 395 ``!(r:'a field) (g:'b group) op. VSpace r g op ==> 396 !u v. u IN V /\ v IN V ==> ((u = v) <=> (u || (- #1) o v = |0|))``, 397 rpt strip_tac >> 398 `Field r` by metis_tac[vspace_has_field] >> 399 rw[EQ_IMP_THM] >| [ 400 `u || -#1 o u = (#1 o u) || -#1 o u` by metis_tac[vspace_cmult_lone] >> 401 `_ = (#1 + -#1) o u ` by rw[vspace_cmult_ladd] >> 402 rw[vspace_cmult_lzero], 403 `#1 IN R /\ -#1 IN R` by rw[] >> 404 `-#1 o v IN V` by metis_tac[vspace_cmult_vector] >> 405 `u = u || #0 o v` by metis_tac[vspace_vadd_rzero, vspace_cmult_lzero] >> 406 `_ = u || (-#1 + #1) o v` by rw[] >> 407 metis_tac[vspace_cmult_ladd, vspace_cmult_lone, vspace_vadd_assoc, vspace_vadd_lzero] 408 ]); 409 410(* Theorem: u IN V /\ v IN V ==> ((u = v) <=> ((- #1) o u || v = |0|)) *) 411(* Proof: 412 Since -#1 o u IN V by vspace_cmult_vector 413 and (- #1) o u || v = v || (- #1) o u by vspace_vadd_comm 414 Hence the result follows by exchange of u, v in vspace_vsub_eq_zero. 415*) 416val vspace_vsub_eq_zero_alt = store_thm( 417 "vspace_vsub_eq_zero_alt", 418 ``!(r:'a field) (g:'b group) op. VSpace r g op ==> 419 !u v. u IN V /\ v IN V ==> ((u = v) <=> ((- #1) o u || v = |0|))``, 420 rpt strip_tac >> 421 `Field r` by metis_tac[vspace_has_field] >> 422 `-#1 IN R` by rw[] >> 423 `-#1 o u IN V` by metis_tac[vspace_cmult_vector] >> 424 metis_tac[vspace_vsub_eq_zero, vspace_vadd_comm]); 425 426(* Theorem: u IN V /\ v IN V ==> ((u || v = |0|) <=> (u = (- #1) o v)) *) 427(* Proof: 428 If part: u || v = |0| ==> u = -#1 o v 429 u 430 = u || |0| by vspace_vadd_rzero 431 = u || (v || (-#1) o v) by vspace_vsub_eq_zero 432 = (u || v) || (-#1) o v by vspace_vadd_assoc 433 = |0| || (-#1) o v by given 434 = -#1 o v by vspace_vadd_lzero 435 Only-if part: u = -#1 o v ==> u || v = |0| 436 u || v 437 = -#1 o v || v by given 438 = |0| by vspace_vsub_eq_zero_alt 439*) 440val vspace_vadd_eq_zero = store_thm( 441 "vspace_vadd_eq_zero", 442 ``!(r:'a field) (g:'b group) op. VSpace r g op ==> 443 !u v. u IN V /\ v IN V ==> ((u || v = |0|) <=> (u = (- #1) o v))``, 444 rpt strip_tac >> 445 `Field r` by metis_tac[vspace_has_field] >> 446 rw[EQ_IMP_THM] >| [ 447 `-#1 IN R` by rw[] >> 448 `-#1 o v IN V` by metis_tac[vspace_cmult_vector] >> 449 metis_tac[vspace_vadd_rzero, vspace_vsub_eq_zero, vspace_vadd_assoc, vspace_vadd_lzero], 450 rw[GSYM vspace_vsub_eq_zero_alt] 451 ]); 452 453(* Theorem: u IN V /\ v IN V ==> ((u || v = |0|) <=> (v = (- #1) o u)) *) 454(* Proof: 455 Since u || v = v || u by vspace_vadd_comm 456 Hence the result follows by exchange of u, v in vspace_vadd_eq_zero. 457*) 458val vspace_vadd_eq_zero_alt = store_thm( 459 "vspace_vadd_eq_zero_alt", 460 ``!(r:'a field) (g:'b group) op. VSpace r g op ==> 461 !u v. u IN V /\ v IN V ==> ((u || v = |0|) <=> (v = (- #1) o u))``, 462 metis_tac[vspace_vadd_eq_zero, vspace_vadd_comm]); 463 464(* ------------------------------------------------------------------------- *) 465(* Sticks -- a stick is a list of scalars of fixed width. *) 466(* ------------------------------------------------------------------------- *) 467 468(* Sticks is a set of vectors of length m *) 469val sticks_def = Define` 470 sticks (r:'a field) (m:num) = { (l:'a list) | (set l) SUBSET R /\ (LENGTH l = m) } 471`; 472 473(* Theorem: sticks r 0 = {[]} *) 474(* Proof: 475 This is to show: set x SUBSET R /\ (LENGTH x = 0) <=> (x = []) 476 If part: set x SUBSET R /\ (LENGTH x = 0) ==> (x = []) 477 Since LENGHT = 0, x = [] by LENGTH_NIL. 478 Only-if part: x = [] ==> set x SUBSET R /\ (LENGTH x = 0) 479 set [] = {} by LIST_TO_SET 480 and {} SUBSET R by EMPTY_SUBSET 481 also LENGTH [] = 0 by LENGTH 482*) 483val sticks_0 = store_thm( 484 "sticks_0", 485 ``!r:'a field. sticks r 0 = {[]}``, 486 rw[sticks_def, EXTENSION, EQ_IMP_THM, LENGTH_NIL]); 487 488(* Theorem: sticks r (SUC n) = IMAGE (\(e,l). e :: l) (R CROSS sticks r n) *) 489(* Proof: 490 After expanding by definitions, this is to show: 491 (1) set (h::l') SUBSET R ==> h IN R /\ set l' SUBSET R 492 set (h::l') = h INSERT set l' by LIST_TO_SET_THM 493 h INSERT set l' SUBSET R 494 <=> h IN R /\ set l' SUBSET R by INSERT_SUBSET 495 (2) p_1 IN R /\ set p_2 SUBSET R ==> set (p_1::p_2) SUBSET R 496 p_1 IN R /\ set p_2 SUBSET R 497 <=> p_1 INSERT set p_2 SUBSET R by INSERT_SUBSET 498 <=> set (p_1 :: p_2) SUBSET R by LIST_TO_SET_THM 499*) 500val sticks_suc = store_thm( 501 "sticks_suc", 502 ``!r:'a field. sticks r (SUC n) = IMAGE (\(e,l). e :: l) (R CROSS sticks r n)``, 503 rw[sticks_def, EXTENSION, pairTheory.EXISTS_PROD, LENGTH_CONS] >> 504 metis_tac[LIST_TO_SET_THM, INSERT_SUBSET]); 505 506(* Theorem: FINITE R ==> !n. FINITE (sticks r n). *) 507(* Proof: by induction on n. 508 Base case: FINITE (sticks r 0) 509 Since sticks r 0 = {[]} by sticks_0 510 Hence true by FINITE_SING 511 Step case: FINITE R /\ FINITE (sticks r n) ==> FINITE (sticks r (SUC n)) 512 sticks r (SUC n) 513 = IMAGE (\(e,l). e::l) (R CROSS sticks r n) by sticks_suc 514 Given FINITE R, and FINITE (sticks r n) by induction hypothesis 515 so FINITE (R CROSS (sticks r n)) by FINITE_CROSS 516 Hence true by IMAGE_FINITE. 517*) 518val sticks_finite = store_thm( 519 "sticks_finite", 520 ``!r:'a field. FINITE R ==> !n. FINITE (sticks r n)``, 521 rpt strip_tac >> 522 Induct_on `n` >- 523 rw[sticks_0] >> 524 rw[sticks_suc]); 525 526(* Theorem: FINITE R ==> CARD (sticks r n) = (CARD R) ** n. *) 527(* Proof: by induction on n. 528 Base case: CARD (sticks r 0) = CARD R ** 0 529 Since sticks r 0 = {[]} by sticks_0 530 CARD {[]} = 1 = CARD R ** 0 by CARD_SING, EXP 531 Step case: FINITE R /\ CARD (sticks r n) = CARD R ** n ==> 532 CARD (sticks r (SUC n)) = CARD R ** SUC n 533 Note that (\(e,l). e::l) x = (\(e,l). e::l) y <=> x = y by LIST_EQ, an injective property. 534 CARD (sticks r (SUC n)) 535 = CARD (IMAGE (\(e,l). e::l) (R CROSS sticks r n)) by sticks_suc 536 = CARD (R CROSS sticks r n) by CARD_INJ_IMAGE, by injective property above. 537 = CARD R * CARD (sticks r n) by CARD_CROSS, FINITE R, FINITE (sticks r n) 538 = CARD R * (CARD R ** n) by induction hypothesis 539 = CARD R ** (SUC n) by EXP 540*) 541val sticks_card = store_thm( 542 "sticks_card", 543 ``!r:'a field. FINITE R ==> !n. CARD (sticks r n) = (CARD R) ** n``, 544 rpt strip_tac >> 545 Induct_on `n` >- 546 rw[sticks_0] >> 547 rw[sticks_suc, sticks_finite, CARD_INJ_IMAGE, FINITE_COUNT, CARD_CROSS, pairTheory.FORALL_PROD, EXP]); 548 549(* Theorem: sticks r 1 = IMAGE (\c. [c]) R *) 550(* Proof: 551 By sticks_def, this is to show: 552 (1) set x SUBSET R /\ LENGTH x = 1 ==> ?c. (x = [c]) /\ c IN R 553 LENGTH x = 1 ==> ?c. x = [c] by LENGTH_EQ_1 554 Also set [c] = c INSERT set [] by LIST_TO_SET_THM 555 = c INSERT {} by LIST_TO_SET_THM 556 = {c} by notation 557 That is c IN set [c] by EXTENSION 558 Given set x SUBSET R, c IN R by SUBSET_DEF 559 (2) c IN R ==> set [c] SUBSET R 560 Since set [c] = {c} by above 561 so !x. x IN set [c] ==> x = c by IN_SING 562 Hence set [c] SUBSER R by SUBSET_DEF 563 (3) LENGTH [c] = 1 564 LENGTH [c] 565 = LENGTH (c::[]) by notation 566 = SUC (LENGTH []) by LENGTH 567 = SUC 0 by LENGTH 568 = 1 by ONE 569*) 570val sticks_1 = store_thm( 571 "sticks_1", 572 ``!r:'a field. sticks r 1 = IMAGE (\(c:'a). [c]) R``, 573 rw[sticks_def, EXTENSION, EQ_IMP_THM] >| [ 574 `?c. x = [c]` by rw[GSYM LENGTH_EQ_1] >> 575 `c IN set [c]` by rw[LIST_TO_SET_THM] >> 576 metis_tac[SUBSET_DEF], 577 rw[LIST_TO_SET_THM], 578 rw[] 579 ]); 580 581(* Theorem: !p. p IN sticks r 1 <=> ?c. c IN R /\ (p = [c]) *) 582(* Proof: by sticks_1, IN_IMAGE *) 583val sticks_1_member = store_thm( 584 "sticks_1_member", 585 ``!r:'a field. !p. p IN sticks r 1 <=> ?c. c IN R /\ (p = [c])``, 586 rw[sticks_1] >> 587 metis_tac[]); 588 589(* Theorem: !p. p IN sticks r 0 <=> (p = []) *) 590(* Proof: 591 p IN sticks r 0 592 <=> p IN {[]} by sticks_0 593 <=> p = [] by IN_SING 594*) 595val sticks_0_member = store_thm( 596 "sticks_0_member", 597 ``!r:'a field. !p. p IN sticks r 0 <=> (p = [])``, 598 rw[sticks_0]); 599 600(* ------------------------------------------------------------------------- *) 601(* Stick Properties. *) 602(* ------------------------------------------------------------------------- *) 603 604(* Theorem: l IN sticks r n ==> LENGTH l = n *) 605(* Proof: by sticks_def. *) 606val stick_length = store_thm( 607 "stick_length", 608 ``!r l n. l IN sticks r n ==> (LENGTH l = n)``, 609 rw[sticks_def]); 610 611(* Theorem: l IN sticks r (SUC n) <=> (?h t. h IN R /\ t IN sticks r n /\ (l = h::t)) *) 612(* Proof: by sticks_suc. *) 613val stick_cons = store_thm( 614 "stick_cons", 615 ``!r:'a field. !(l:'a list) n. l IN sticks r (SUC n) <=> 616 (?h t. h IN R /\ t IN sticks r n /\ (l = h::t))``, 617 rw[sticks_suc, pairTheory.EXISTS_PROD] >> 618 metis_tac[]); 619 620(* Define a sticks of length n with all zero *) 621(* 622val stick_all_zero_def = Define` 623 stick_all_zero (r:'a field) n = GENLIST (\j. #0) n 624`; 625*) 626 627(* Theorem: VSpace r g op ==> !n. (GENLIST (\j. #0) n) IN (sticks r n) *) 628(* Proof: 629 By induction on n. 630 Base case: GENLIST (\j. #0) 0 IN sticks r 0 631 GENLIST (\j. #0) 0 = [] by GENLIST 632 sticks r 0 = {[]} by sticks_0 633 and [] IN {[]} by IN_SING 634 Step case: GENLIST (\j. #0) n IN sticks r n ==> 635 GENLIST (\j. #0) (SUC n) IN sticks r (SUC n) 636\ GENLIST (\j. #0) (SUC n) 637 = #0 :: GENLIST ((\j. #0) o SUC) n by GENLIST_CONS 638 = #0 :: GENLIST (\j. #0) n since (\j. #0) o SUC = (\j. #0) by FUN_EQ_THM 639 Since #0 IN R by field_zero_element 640 and GENLIST (\j. #0) n IN sticks r n by induction hypothesis 641 so result IN sticks r (SUC n) by stick_cons 642*) 643val stick_all_zero = store_thm( 644 "stick_all_zero", 645 ``!(r:'a field) (g:'b group) op. VSpace r g op ==> !n. (GENLIST (\j. #0) n) IN (sticks r n)``, 646 rpt strip_tac >> 647 Induct_on `n` >| [ 648 rw[] >> 649 metis_tac[sticks_0, IN_SING], 650 rw[stick_cons] >> 651 qexists_tac `#0` >> 652 qexists_tac `GENLIST (\j. #0) n` >> 653 `Field r` by metis_tac[vspace_has_field] >> 654 rw_tac std_ss[GENLIST_CONS, field_zero_element] >> 655 `(\j. #0) o SUC = (\j. #0)` by rw[FUN_EQ_THM] >> 656 rw[] 657 ]); 658 659(* Theorem: h IN R /\ t IN sticks r (n - 1) ==> 660 !k. k < n ==> TAKE k t ++ [h] ++ DROP k t IN sticks r n *) 661(* Proof: by induction on n. 662 Base case: !k. k < 0 ==> ... 663 Since k < 0 is F, this is true. 664 Step case: k < SUC n ==> TAKE k t ++ [h] ++ DROP k t IN sticks r (SUC n) 665 If k = 0, TAKE 0 t ++ [h] ++ DROP 0 t 666 = [] ++ [h] ++ t 667 = h::t IN sticks r (SUC n) by stick_cons 668 If k = SUC n' < SUC n, n' < n 669 to show: TAKE (SUC n') t ++ [h] ++ DROP (SUC n') t IN sticks r (SUC n) 670 Since n' < n, n <> 0, 671 or n = SUC j, so t IN sticks r n means 672 ?k s. k IN R /\ s IN sticks r j /\ t = k::s by stick_cons 673 and (TAKE n' s ++ [h] ++ DROP n' s) IN sticks r (SUC j) 674 by induction hypothesis 675 TAKE (SUC n') t ++ [h] ++ DROP (SUC n') t 676 = TAKE (SUC n') (k::s) ++ [h] ++ DROP (SUC n') (k::s) 677 = (k:: TAKE n' s) ++ [h] ++ DROP n' s by TAKE_def, DROP_def 678 = k:: (TAKE n' s ++ [h] ++ DROP n' s) by APPEND 679 IN sticks r (SUC n) by stick_cons, k IN R, induction hypothesis. 680*) 681val stick_insert_element = store_thm( 682 "stick_insert_element", 683 ``!r:'a field. !h t n. h IN R /\ t IN sticks r (n - 1) ==> 684 !k. k < n ==> TAKE k t ++ [h] ++ DROP k t IN sticks r n``, 685 ntac 2 strip_tac >> 686 Induct_on `n` >- 687 rw[] >> 688 rw[] >> 689 Cases_on `k` >- 690 rw[stick_cons] >> 691 rw[] >> 692 `n' < n` by decide_tac >> 693 `n <> 0` by decide_tac >> 694 `?j. n = SUC j` by metis_tac[num_CASES] >> 695 `?k s. k IN R /\ s IN sticks r j /\ (t = k::s)` by metis_tac[stick_cons] >> 696 `SUC j - 1 = j` by decide_tac >> 697 rw[] >> 698 `(TAKE n' s ++ [h] ++ DROP n' s) IN sticks r (SUC j)` by rw[] >> 699 metis_tac[stick_cons]); 700 701(* Theorem: t IN sticks r n ==> !k. k < n ==> 702 EL k t IN R /\ TAKE k t IN sticks r k /\ DROP (SUC k) t IN sticks r (n - (SUC k)) *) 703(* Proof: 704 By induction on n. 705 Base case: !k. k < 0 ==> 706 TAKE k t IN sticks r k /\ EL k t IN R /\ DROP (SUC k) t IN sticks r (0 - (SUC k)) 707 Since k < 0 is F, this is true. 708 Step case: t IN sticks r (SUC n) ==> !k. k < SUC n ==> 709 EL k t IN R /\ TAKE k t IN sticks r k /\ DROP (SUC k) t IN sticks r (SUC n - SUC k) 710 Expanding by stick_cons, this is to show: 711 (1) k < SUC n ==> EL k (h::t') IN R 712 If k = 0, EL 0 (h::t') = h IN R by h IN R from stick_cons 713 If k = SUC j < SUC n, EL (SUC j) (h::t') = EL j t' IN R by induction hypothesis. 714 (2) k < SUC n ==> TAKE k (h::t') IN sticks r k 715 If k = 0, TAKE 0 (h::t') = [] IN sticks r 0 by sticks_0 716 If k = SUC j < SUC n, TAKE (SUC j) (h::t') = TAKE j t' IN sticks r j 717 by stick_cons, induction hypothesis. 718 (3) k < SUC n ==> DROP (SUC k) (h::t') IN sticks r (n - k) 719 If k = 0, DROP 1 (h::t') = t' IN sticks r n by stick_cons 720 If k = SUC j < SUC n, DROP (SUC j) (h::t') = DROP j t' IN sticks r (n - SUC j) 721 by induction hypothesis 722*) 723val stick_components_stick = store_thm( 724 "stick_components_stick", 725 ``!(r:'a field) (t:'a list) n. t IN sticks r n ==> 726 !k. k < n ==> EL k t IN R /\ TAKE k t IN sticks r k /\ DROP (SUC k) t IN sticks r (n - (SUC k))``, 727 strip_tac >> 728 Induct_on `n` >- 729 rw[] >> 730 `!j k. SUC j < SUC k ==> j < k` by decide_tac >> 731 rw[stick_cons] >| [ 732 Cases_on `k` >> rw[], 733 Cases_on `k` >> rw[sticks_0, stick_cons], 734 Cases_on `k` >> rw[] 735 ]); 736 737(* Theorem: l IN sticks r (SUC n) <=> (?h t. h IN R /\ t IN sticks r n /\ (l = SNOC h t)) *) 738(* Proof: 739 If part: l IN sticks r (SUC n) ==> ?h t. h IN R /\ t IN sticks r n /\ (l = t ++ [h]) 740 Since n < SUC n by LESS_SUC 741 and SUC n - SUC n by arithmetic 742 so EL n l IN R /\ TAKE n l IN sticks r n /\ 743 DROP (SUC n) l IN sticks r 0 by stick_components_stick 744 Let h = EL n l, t = TAKE n l, s = DROP (SUC n) l. 745 Then s IN sticks r 0 ==> s = [] by sticks_0, IN_SING 746 Also LENGTH l = SUC n by stick_length 747 so l = t ++ DROP n l by TAKE_DROP 748 = t ++ ([h] ++ s) by DROP_CONS_EL 749 = t ++ ([h] ++ []) by s = [] 750 = t ++ [h] by APPEND_NIL 751 Only-if part: h IN R /\ t IN sticks r n ==> t ++ [h] IN sticks r (SUC n) 752 h IN R /\ t IN sticks r n 753 ==> h IN R /\ set t SUBSET R /\ (LENGTH t = n) by sticks_def 754 ==> set (t ++ [h]) SUBSET R /\ (LENGTH t = n) by LIST_TO_SET_APPEND, UNION_SUBSET 755 ==> set (t ++ [h]) SUBSET R /\ (LENGTH (t ++ [h]) = 1 + n) by LENGTH_APPEND 756 ==> set (t ++ [h]) SUBSET R /\ (LENGTH (t ++ [h]) = SUC n) by SUC_ONE_ADD 757 ==> t ++ [h] IN sticks r (SUC n) by sticks_def 758*) 759val stick_snoc = store_thm( 760 "stick_snoc", 761 ``!r:'a field. !(l:'a list) n. l IN sticks r (SUC n) <=> 762 (?h t. h IN R /\ t IN sticks r n /\ (l = SNOC h t))``, 763 rw[EQ_IMP_THM] >| [ 764 `n < SUC n /\ (SUC n - SUC n = 0)` by decide_tac >> 765 `EL n l IN R /\ TAKE n l IN sticks r n /\ DROP (SUC n) l IN sticks r 0` by metis_tac[stick_components_stick] >> 766 qabbrev_tac `h = EL n l` >> 767 qabbrev_tac `t = TAKE n l` >> 768 qabbrev_tac `s = DROP (SUC n) l` >> 769 `s = []` by metis_tac[sticks_0, IN_SING] >> 770 `LENGTH l = SUC n` by metis_tac[stick_length] >> 771 `l = t ++ DROP n l` by rw[TAKE_DROP, Abbr`t`] >> 772 `_ = t ++ ([h] ++ s)` by rw[rich_listTheory.DROP_CONS_EL, Abbr`h`, Abbr`s`] >> 773 `_ = t ++ [h]` by rw[] >> 774 metis_tac[], 775 pop_assum mp_tac >> 776 rw[sticks_def] 777 ]); 778 779(* ------------------------------------------------------------------------- *) 780(* Stick Addition. *) 781(* ------------------------------------------------------------------------- *) 782 783(* Define stick addition by components. *) 784val stick_add_def = Define` 785 (stick_add (r:'a field) [][] = []) /\ 786 (stick_add (r:'a field) ((h:'a)::(t:'a list)) ((h':'a)::(t':'a list)) = 787 (h + h')::(stick_add r t t')) 788`; 789 790val _ = temp_overload_on ("+", ``stick_add r``); 791(* - stick_add_def; 792> val it = |- (!r. [] + [] = []) /\ !t' t r h' h. (h::t) + (h'::t') = h + h'::t + t' : thm *) 793 794val stick_add_nil_nil = save_thm("stick_add_nil_nil", stick_add_def |> CONJUNCTS |> el 1); 795(* val stick_add_nil_nil = |- !r. [] + [] = []: thm *) 796 797val stick_add_cons_cons = save_thm("stick_add_cons_cons", stick_add_def |> CONJUNCTS |> el 2); 798(* val stick_add_cons_cons = |- !t' t r h' h. (h::t) + (h'::t') = h + h'::t + t': thm *) 799 800(* Adding same-length sticks give another stick of the same length *) 801 802(* Theorem: !n. n1 IN sticks r n /\ n2 IN sticks r n ==> (n1 + n2) IN sticks r n *) 803(* Proof: by induction on n. 804 Base case: n1 IN sticks r 0 /\ n2 IN sticks r 0 ==> n1 + n2 IN sticks r 0 805 Since n1 = [] and n2 = [] by sticks_0, IN_SING 806 n1 + n2 = [] + [] = [] IN sticks r 0 by sticks_0, IN_SING. 807 Step case: !n1 n2. n1 IN sticks r (SUC n) /\ n2 IN sticks r (SUC n) ==> n1 + n2 IN sticks r (SUC n) 808 By stick_cons, this is to show: 809 ?h'' t''. h'' IN R /\ t'' IN sticks r n /\ ((h::t) + (h'::t') = h''::t'') 810 Let h'' = h + h', t'' = t + t'. 811 Then h + h' IN R by field_add_element 812 and t + t' IN sticks r n by induction hypothesis 813 and (h::t) + (h'::t') = h''::t'' by stick_add_def 814*) 815val stick_add_length = store_thm( 816 "stick_add_length", 817 ``!(r:'a field). Field r ==> 818 !n n1 n2. n1 IN sticks r n /\ n2 IN sticks r n ==> (n1 + n2) IN sticks r n``, 819 ntac 2 strip_tac >> 820 Induct >- 821 metis_tac[sticks_0, IN_SING, stick_add_def] >> 822 rw[stick_cons] >> 823 qexists_tac `h + h'` >> 824 qexists_tac `t + t'` >> 825 rw[stick_add_def]); 826 827(* ------------------------------------------------------------------------- *) 828(* Stick Negation. *) 829(* ------------------------------------------------------------------------- *) 830 831(* Define stick addition by components. *) 832val stick_neg_def = Define` 833 (stick_neg (r:'a field) [] = []) /\ 834 (stick_neg (r:'a field) ((h:'a)::(t:'a list)) = (-h)::(stick_neg r t)) 835`; 836 837val _ = temp_overload_on ("-", ``stick_neg r``); 838(* - stick_neg_def; 839> val it = |- (!r. $- [] = []) /\ !r h t. $- (h::t) = -h:: $- t : thm *) 840 841(* Theorem: $- [] = [] *) 842val stick_neg_zero = save_thm("stick_neg_zero", stick_neg_def |> SPEC_ALL |> CONJUNCTS |> el 1 |> DISCH_ALL |> GEN_ALL); 843(* val stick_neg_zero = |- !r. $- [] = []: thm *) 844 845(* Theorem: $- (h::t) = -h:: $- t *) 846val stick_neg_cons = save_thm("stick_neg_cons", stick_neg_def |> SPEC_ALL |> CONJUNCTS |> el 2 |> DISCH_ALL |> GEN_ALL); 847(* val stick_neg_cons = |- !r h t. $- (h::t) = -h:: $- t: thm *) 848 849(* Negating a stick gives another stick of the same length *) 850 851(* Theorem: !n. n1 IN sticks r n ==> ($- n1) IN sticks r n *) 852(* Proof: by induction on n. 853 Base case: n1 IN sticks r 0 ==> $- n1 IN sticks r 0 854 Since n1 = [] by sticks_0, IN_SING 855 $- n1 = $- [] = [] IN sticks r 0 by sticks_0, IN_SING. 856 Step case: !n1. n1 IN sticks r (SUC n) ==> $- n1 IN sticks r (SUC n) 857 By stick_cons, this is to show: 858 ?h' t'. h' IN R /\ t' IN sticks r n /\ ($- (h::t) = h'::t') 859 Let h' = -h, t' = $- t. 860 Then -h IN R by field_neg_element 861 and $- t IN sticks r n by induction hypothesis 862 and $- (h::t) = h'::t' by stick_neg_def 863*) 864val stick_neg_length = store_thm( 865 "stick_neg_length", 866 ``!(r:'a field). Field r ==> !n n1. n1 IN sticks r n ==> ($- n1) IN sticks r n``, 867 ntac 2 strip_tac >> 868 Induct >- 869 metis_tac[sticks_0, IN_SING, stick_neg_def] >> 870 rw[stick_cons] >> 871 qexists_tac `-h` >> 872 qexists_tac `$- t` >> 873 rw[stick_neg_def]); 874 875(* ------------------------------------------------------------------------- *) 876(* Stick Scalar Multiplication. *) 877(* ------------------------------------------------------------------------- *) 878 879(* Define stick scalar multiplication by components. *) 880val stick_cmult_def = Define` 881 (stick_cmult (r:'a field) (c:'a) [] = []) /\ 882 (stick_cmult (r:'a field) (c:'a) ((h:'a)::(t:'a list)) = (c * h)::(stick_cmult r c t)) 883`; 884 885val _ = temp_overload_on ("*", ``stick_cmult r``); 886(* - stick_cmult_def; 887> val it = |- (!r c. c * [] = []) /\ !r c h t. c * (h::t) = c * h::c * t : thm *) 888 889(* Theorem: c * [] = [] *) 890val stick_cmult_zero = save_thm("stick_cmult_zero", stick_cmult_def |> SPEC_ALL |> CONJUNCTS |> el 1 |> DISCH_ALL |> GEN_ALL); 891(* val stick_cmult_zero = |- !r c. c * [] = []: thm *) 892 893(* Theorem: c * (h::t) = c * h::c * t *) 894val stick_cmult_cons = save_thm("stick_cmult_cons", stick_cmult_def |> SPEC_ALL |> CONJUNCTS |> el 2 |> DISCH_ALL |> GEN_ALL); 895(* val stick_cmult_cons = |- !r c h t. c * (h::t) = c * h::c * t: thm *) 896 897(* Multiply a stick by a scalar gives another stick of the same length *) 898 899(* Theorem: !n. c IN R /\ n1 IN sticks r n ==> c * n1 IN sticks r n *) 900(* Proof: by induction on n. 901 Base case: !c n1. c IN R /\ n1 IN sticks r 0 ==> c * n1 IN sticks r 0 902 Since n1 = [] by sticks_0, IN_SING 903 c * n1 = c * [] = [] IN sticks r 0 by sticks_0, IN_SING 904 Step case: !c n1. c IN R /\ n1 IN sticks r (SUC n) ==> c * n1 IN sticks r (SUC n) 905 By stick_cons, this is to show: 906 ?h' t'. h' IN R /\ t' IN sticks r n /\ (c * (h::t) = h'::t') 907 Let h'' = c * h, t'' = c * t. 908 Then c * h IN R by field_mult_element 909 and c * t IN sticks r n by induction hypothesis 910 and c * (h::t) = h'::t' by stick_cmult_def 911*) 912val stick_cmult_length = store_thm( 913 "stick_cmult_length", 914 ``!(r:'a field). Field r ==> !n c n1. c IN R /\ n1 IN sticks r n ==> (c * n1) IN sticks r n``, 915 ntac 2 strip_tac >> 916 Induct >- 917 metis_tac[sticks_0, IN_SING, stick_cmult_def] >> 918 rw[stick_cons] >> 919 qexists_tac `c * h` >> 920 qexists_tac `c * t` >> 921 rw[stick_cmult_def]); 922 923(* ------------------------------------------------------------------------- *) 924(* Stick Subtraction. *) 925(* ------------------------------------------------------------------------- *) 926 927(* Define stick subtraction by components. *) 928val stick_sub_def = Define` 929 (stick_sub (r:'a field) [][] = []) /\ 930 (stick_sub (r:'a field) ((h:'a)::(t:'a list)) ((h':'a)::(t':'a list)) = 931 (h - h')::(stick_sub r t t')) 932`; 933 934val _ = temp_overload_on ("-", ``stick_sub r``); 935(* - stick_sub_def; 936> val it = |- (!r. [] - [] = []) /\ !t' t r h' h. (h::t) - (h'::t') = h - h'::t - t' : thm *) 937 938(* Theorem: [] - [] = [] *) 939val stick_sub_nil_nil = save_thm("stick_sub_nil_nil", stick_sub_def |> SPEC_ALL |> CONJUNCTS |> el 1 |> DISCH_ALL |> GEN_ALL); 940(* val val stick_sub_nil_nil = |- !r. [] - [] = []: thm *) 941 942(* Theorem: (h::t) - (h'::t') = h - h'::t - t' *) 943val stick_sub_cons_cons = save_thm("stick_sub_cons_cons", stick_sub_def |> SPEC_ALL |> CONJUNCTS |> el 2 |> DISCH_ALL |> GEN_ALL); 944(* val stick_sub_cons_cons = |- !t' t r h' h. (h::t) - (h'::t') = h - h'::t - t': thm *) 945 946(* Theorem: !n. n2. n1 IN sticks r n /\ n2 IN sticks r n ==> n1 - n2 = n1 + $- n2 *) 947(* Proof: by induction on n. 948 Base case: n1 IN sticks r 0 /\ n2 IN sticks r 0 ==> n1 - n2 = n1 + $- n2 949 Since n1 = [] and n2 = [] by sticks_0, IN_SING 950 n1 - n2 951 = [] by stick_sub_def 952 = [] + [] by stick_add_def 953 = [] + $- [] by stick_neg_def 954 Step case: n1 IN sticks r (SUC n) /\ n2 IN sticks r (SUC n) ==> n1 - n2 = n1 + $- n2 955 By expanding with stick_cons, this is to show: 956 (h::t) - (h'::t') = (h::t) + $- (h'::t') 957 (h::t) - (h'::t') 958 = h - h' :: t - t' by stick_sub_def 959 = h + -h':: t - t' by field_sub_def 960 = h + -h':: t + $-t' by induction hypothesis 961 = (h::t) + (-h'::-t') by stick_add_def 962 = (h::t) + -(h'::t') by stick_neg_def 963*) 964val stick_sub_alt = store_thm( 965 "stick_sub_alt", 966 ``!(r:'a field). Field r ==> 967 !n n1 n2. n1 IN sticks r n /\ n2 IN sticks r n ==> (n1 - n2 = n1 + $- n2)``, 968 ntac 2 strip_tac >> 969 Induct >| [ 970 rw[] >> 971 `(n1 = []) /\ (n2 = [])` by metis_tac[sticks_0, IN_SING] >> 972 rw[stick_sub_def, stick_add_def, stick_neg_def], 973 rw[stick_cons] >> 974 rw[stick_sub_def, stick_add_def, stick_neg_def] 975 ]); 976 977(* Subtracting same-length sticks give another stick of the same length *) 978 979(* Theorem: !n. n2. n1 IN sticks r n /\ n2 IN sticks r n ==> (n1 - n2) IN sticks r n *) 980(* Proof: by induction on n. 981 Base case: n1 IN sticks r 0 /\ n2 IN sticks r 0 ==> n1 - n2 IN sticks r 0 982 Since n1 = [] and n2 = [] by sticks_0, IN_SING 983 n1 - n2 = [] - [] = [] IN sticks r 0 by sticks_0, IN_SING 984 Step case: !n1 n2. n1 IN sticks r (SUC n) /\ n2 IN sticks r (SUC n) ==> n1 - n2 IN sticks r (SUC n) 985 By stick_cons, this is to show: 986 ?h'' t''. h'' IN R /\ t'' IN sticks r n /\ ((h::t) - (h'::t') = h''::t'') 987 Let h'' = h - h', t'' = t - t'. 988 Then h - h' IN R by field_sub_element 989 and t - t' IN sticks r n by induction hypothesis 990 and (h::t) - (h'::t') = h''::t'' by stick_sub_def 991 Or: 992 n1 - n2 = n1 + $- n2 by stick_sub_alt 993 Hence true by stick_add_length, stick_neg_length. 994*) 995val stick_sub_length = store_thm( 996 "stick_sub_length", 997 ``!(r:'a field). Field r ==> 998 !n n1 n2. n1 IN sticks r n /\ n2 IN sticks r n ==> (n1 - n2) IN sticks r n``, 999 rpt strip_tac >> 1000 `n1 - n2 = n1 + $- n2` by metis_tac[stick_sub_alt] >> 1001 rw[stick_add_length, stick_neg_length]); 1002 1003(* Theorem: !n. n1 IN sticks r n /\ n2 IN sticks r n ==> 1004 n1 = n2 <=> !k. k < n ==> (EL k (n1 - n2) = #0) *) 1005(* Proof: by induction on n. 1006 Base case: !n1 n2. n1 IN sticks r 0 /\ n2 IN sticks r 0 ==> 1007 ((n1 = n2) <=> !k. k < 0 ==> (EL k (n1 - n2) = #0)) 1008 Since n1 = [] and n2 = [] by sticks_0 1009 and LENGTH [] = 0 by LENGTH_NIL 1010 This is trivially true, as no k < 0. 1011 Step case: !n1 n2. n1 IN sticks r (SUC n) /\ n2 IN sticks r (SUC n) ==> 1012 ((n1 = n2) <=> !k. k < SUC n ==> (EL k (n1 - n2) = #0)) 1013 By stick_cons, this is to show: 1014 (h = h') /\ (!k. k < n ==> (EL k (t - t') = #0)) <=> !k. k < SUC n ==> (EL k ((h::t) - (h'::t')) = #0) 1015 1016 If part: k < SUC n ==> EL k ((h::t) - (h::t)) = #0 1017 EL k ((h::t) - (h::t)) 1018 = EL k ((h - h) :: (t - t)) by stick_sub_def 1019 = EL k (#0 :: (t - t)) by field_sub_eq_zero 1020 If k = 0, EL 0 (#0::(t - t)) is true by EL, HD. 1021 If k = SUC n', n' < n, EL (SUC n') (#0::(t - t)) = EL n' (t - t) = #0 by induction hypothesis. 1022 1023 Only-if part: !k. k < SUC n ==> (EL k ((h::t) - (h'::t')) = #0) ==> 1024 (h = h') /\ !k. k < n ==> (EL k (t - t') = #0) 1025 (h::t) - (h'::t') = (h - h')::(t - t') by stick_sub_def 1026 If k = 0, EL 0 ((h::t) - (h'::t')) = #0 => h - h' = #0, or h = h' by field_sub_eq_zero. 1027 If k = SUC n', 1028 !n'. n' < n and EL (SUC n') ((h::t) - (h'::t')) = EL n' (t - t') = #0 by induction hypothesis 1029*) 1030val stick_eq_property = store_thm( 1031 "stick_eq_property", 1032 ``!(r:'a field). Field r ==> !n n1 n2. n1 IN sticks r n /\ n2 IN sticks r n ==> 1033 ((n1 = n2) <=> (!k. k < n ==> (EL k (n1 - n2) = #0)))``, 1034 ntac 2 strip_tac >> 1035 Induct >- 1036 rw[sticks_0] >> 1037 rw[stick_cons, EQ_IMP_THM] >| [ 1038 `(h::t) - (h::t) = #0::(t - t)` by rw[stick_sub_def] >> 1039 rw[] >> 1040 Cases_on `k` >- 1041 rw[] >> 1042 `n' < n` by decide_tac >> 1043 rw[] >> 1044 metis_tac[], 1045 `(h::t) - (h'::t') = h - h'::(t - t')` by rw[stick_sub_def] >> 1046 `(!k. k < SUC n ==> (EL k ((h::t) - (h'::t')) = #0)) ==> 1047 (0 < SUC n ==> (EL 0 ((h::t) - (h'::t')) = #0)) /\ 1048 (!k. SUC k < SUC n ==> (EL (SUC k) ((h::t) - (h'::t')) = #0))` by metis_tac[num_CASES] >> 1049 `EL 0 ((h::t) - (h'::t')) = #0` by rw[] >> 1050 `h - h' = #0` by metis_tac[EL, HD] >> 1051 `h = h'` by metis_tac[field_sub_eq_zero] >> 1052 `!k. k < n ==> (EL (SUC k) ((h::t) - (h::t')) = #0)` by rw[] >> 1053 `!k. k < n ==> (EL k (t - t') = #0)` by metis_tac[EL, TL] >> 1054 rw[] 1055 ]); 1056 1057 1058(* ------------------------------------------------------------------------- *) 1059 1060(* export theory at end *) 1061val _ = export_theory(); 1062 1063(*===========================================================================*) 1064