From 9eccc5e457c56b94a3223821e98f5ec559023c67 Mon Sep 17 00:00:00 2001 From: John Harrison Date: Thu, 7 Nov 2024 16:53:36 +0000 Subject: [PATCH] Factored the material about linear dependence, span and dimension out of the specific setting of vectors in R^n and set it up as a general theory of "matroids". These don't have all the finiteness assumptions common in matroid theory, but could be considered as "finitary" (matroid span is assumed to have finite character). The setup roughly follows Pete Clark's "Field Theory" notes, 11.4: http://alpha.math.uga.edu/~pete/FieldTheory.pdf Added one more theorem WORD_SUBWORD_DUPLICATE_DUPLICATE relating subwords and duplication, which is also now exploited inside WORD_SIMPLE_SUBWORD_CONV. Slightly refined the improvements to div/rem elimination made recently, to avoid exponential blowups while preserving the ability to deduce nonnegativity of the quotient in "easy" cases. List of new definitions (all connected with matroids) matroid_basis matroid_dim matroid_dimension matroid_finite_dim matroid_finite_dimensional matroid_independent matroid_set matroid_span matroid_spanning matroid_subspace matroid_tybij submatroid and theorems (all about matroids except the last one) FINITE_IMP_MATROID_FINITE_DIM FINITE_IMP_MATROID_FINITE_DIM_SPAN MATROID_BASES_CARD_EQ MATROID_BASES_FINITE MATROID_BASES_SIZE MATROID_BASIS_EQ_MAXIMAL_INDEPENDENT MATROID_BASIS_EQ_MINIMAL_SPANNING MATROID_BASIS_EXISTS MATROID_BASIS_EXISTS_DIM MATROID_BASIS_EXISTS_DIMENSION MATROID_BASIS_IMP_SUBSET MATROID_BASIS_SUBMATROID MATROID_CHOOSE_SUBSET MATROID_CHOOSE_SUBSPACE MATROID_CONTAINS_BASIS_DIM MATROID_DIMENSION_ALT MATROID_DIMENSION_EQ_CARD MATROID_DIMENSION_FINITE_LE MATROID_DIMENSION_GE MATROID_DIMENSION_GE_CARD MATROID_DIMENSION_GE_FINITE_CARD MATROID_DIMENSION_LE MATROID_DIMENSION_UNIQUE MATROID_DIM_ALT MATROID_DIM_BASIS MATROID_DIM_EMPTY MATROID_DIM_EQ_CARD MATROID_DIM_EQ_CARD_GEN MATROID_DIM_EQ_FINITE_CARD_EQ,MATROID_DIM_GE_FINITE_CARD_EQ MATROID_DIM_EQ_SPAN MATROID_DIM_FINITE_LE MATROID_DIM_GE MATROID_DIM_GE_CARD MATROID_DIM_GE_CARD_GEN MATROID_DIM_GE_FINITE_CARD MATROID_DIM_INSERT MATROID_DIM_LE MATROID_DIM_LE_CARD MATROID_DIM_LE_CARD_GEN MATROID_DIM_SET MATROID_DIM_SPAN MATROID_DIM_SPAN_EQ MATROID_DIM_SPAN_EQ_GEN MATROID_DIM_SPAN_PSUBSET MATROID_DIM_SPAN_SUBSET MATROID_DIM_SUBSET MATROID_DIM_SUBSET_ALT MATROID_DIM_UNIQUE MATROID_DIM_UNIQUE_ALT MATROID_EQ_SPANS_CARD_EQ MATROID_EQ_SPANS_FINITE MATROID_EQ_SPANS_SIZE MATROID_FINITE_DIM MATROID_FINITE_DIMENSIONAL MATROID_FINITE_DIMENSIONAL_ANY MATROID_FINITE_DIMENSIONAL_BASIS MATROID_FINITE_DIMENSIONAL_CONTAINS_BASIS MATROID_FINITE_DIMENSIONAL_DIM MATROID_FINITE_DIM_BASIS MATROID_FINITE_DIM_EMPTY MATROID_FINITE_DIM_FINITE MATROID_FINITE_DIM_IMP_SUBSET MATROID_FINITE_DIM_INSERT MATROID_FINITE_DIM_MONO MATROID_FINITE_DIM_SET MATROID_FINITE_DIM_SPAN MATROID_FINITE_DIM_SPAN_EQ MATROID_FINITE_DIM_SUBSET MATROID_FINITE_DIM_UNION MATROID_INDEPENDENT_CARD_LE_SPAN MATROID_INDEPENDENT_CARD_LE_SPANNING MATROID_INDEPENDENT_CARD_LE_SPAN_FINITE MATROID_INDEPENDENT_CHAIN MATROID_INDEPENDENT_EMPTY MATROID_INDEPENDENT_EXTENDS_TO_BASIS MATROID_INDEPENDENT_FINITARY MATROID_INDEPENDENT_IMP_FINITE MATROID_INDEPENDENT_IMP_SUBSET MATROID_INDEPENDENT_INSERT MATROID_INDEPENDENT_MONO MATROID_INDEPENDENT_SPANNING_FINITE MATROID_INDEPENDENT_SUBMATROID MATROID_INTERMEDIATE_BASIS MATROID_INTERMEDIATE_SPAN MATROID_LOWDIM_EXPAND_BASIS MATROID_LOWDIM_EXPAND_DIMENSION MATROID_MAXIMAL_INDEPENDENT_SUBSET_SPAN MATROID_SPANNING_ALT MATROID_SPANNING_CONTAINS_BASIS MATROID_SPANNING_IMP_SUBSET MATROID_SPANNING_PSUBSET_INDEPENDENT MATROID_SPANNING_SET MATROID_SPANNING_SUBMATROID MATROID_SPANNING_SUBMATROID_SELF MATROID_SPANNING_SUBSET_INDEPENDENT MATROID_SPAN_CHAIN MATROID_SPAN_DELETE_EQ MATROID_SPAN_DIM_EQ MATROID_SPAN_EQ MATROID_SPAN_EQ_SELF MATROID_SPAN_EQ_SET MATROID_SPAN_EXCHANGE_DELETE MATROID_SPAN_FINITARY_GEN MATROID_SPAN_FINITARY_MINIMAL MATROID_SPAN_INC MATROID_SPAN_INSERT_EQ MATROID_SPAN_INSERT_REFL MATROID_SPAN_INTER_SPANS MATROID_SPAN_INTER_SUBSET MATROID_SPAN_MINIMAL MATROID_SPAN_MONO MATROID_SPAN_OF_SUBSPACE MATROID_SPAN_PSUBSET_INDEPENDENT MATROID_SPAN_SET MATROID_SPAN_SUBSET MATROID_SPAN_SUBSET_EQ MATROID_SPAN_SUBSET_SUBSPACE MATROID_SPAN_SUBSPACE MATROID_SPAN_SUPERSET MATROID_SPAN_TRANS MATROID_SPAN_UNION_EQ MATROID_SPAN_UNION_SUBSET MATROID_STEINITZ_EXCHANGE MATROID_STEINITZ_EXCHANGE_ALT MATROID_STEINITZ_EXCHANGE_FINITE MATROID_SUBSET_CONTAINS_BASIS MATROID_SUBSPACE MATROID_SUBSPACE_CHAIN MATROID_SUBSPACE_IMP_SUBSET MATROID_SUBSPACE_INTER MATROID_SUBSPACE_INTERS MATROID_SUBSPACE_SET MATROID_SUBSPACE_SPAN SUBMATROID SUBMATROID_GEN SUBMATROID_SET SUBMATROID_SPAN SUBMATROID_SUBSET SUBSET_MATROID_SPAN WORD_SUBWORD_DUPLICATE_DUPLICATE --- CHANGES | 132 +++ Library/matroids.ml | 1529 +++++++++++++++++++++++++ Library/words.ml | 27 +- Multivariate/complex_database.ml | 190 +++ Multivariate/make.ml | 1 + Multivariate/make_complex.ml | 1 + Multivariate/multivariate_database.ml | 190 +++ Multivariate/vectors.ml | 702 +++++------- holtest | 1 + holtest.mk | 1 + int.ml | 61 +- 11 files changed, 2410 insertions(+), 425 deletions(-) create mode 100644 Library/matroids.ml diff --git a/CHANGES b/CHANGES index e0280f01..a71c87c5 100644 --- a/CHANGES +++ b/CHANGES @@ -8,6 +8,138 @@ * page: https://github.com/jrh13/hol-light/commits/master * * ***************************************************************** +Thu 7th Nov 2024 Multivariate/vectors.ml, Library/matroids.ml [new file] + +Factored the material about linear dependence, span and dimension +out of the specific setting of vectors in R^n and set it up as a +general theory of "matroids". These don't have all the finiteness +assumptions common in matroid theory, but could be considered as +"finitary" (matroid span is assumed to have finite character). +The setup roughly follows Pete Clark's "Field Theory" notes, 11.4: + + http://alpha.math.uga.edu/~pete/FieldTheory.pdf + +Wed 6th Nov 2024 Library/words.ml + +Added one more theorem relating subwords and duplication, which is also +now exploited inside WORD_SIMPLE_SUBWORD_CONV: + + WORD_SUBWORD_DUPLICATE_DUPLICATE = + |- !x pos len. + pos MOD dimindex (:M) = 0 /\ + dimindex (:P) <= len /\ + pos + len <= dimindex (:N) + ==> word_subword (word_duplicate x) (pos,len) = word_duplicate x + +Wed 6th Nov 2024 int.ml + +Slightly refined the improvements to div/rem elimination made recently, +to avoid exponential blowups while preserving the ability to deduce +nonnegativity of the quotient in "easy" cases. + +Fri 1st Nov 2024 Library/words.ml + +Added both unsigned and signed *saturating* conversions from N and Z to +machine words, which rather than wrapping modulo 2^wordsize as the main +"word" and "iword" do, saturate at the extremal values of that size: + + word_saturate = + |- word_saturate n = + if n > val word_UINT_MAX then word_UINT_MAX else word n + + iword_saturate = + |- iword_saturate x = + if x < ival word_INT_MIN then word_INT_MIN + else if x > ival word_INT_MAX then word_INT_MAX + else iword x + +Also added a natural "word_duplicate" operation, a kind of iterated +word_join inferring relative sizes and hence number of duplicates from +the types. + + word_duplicate = + |- (word_duplicate:M word->N word) x = + word_of_bits {i | bit (i MOD dimindex (:M)) x + +There are also a few elementary lemmas about it: + + BIT_WORD_DUPLICATE = + |- !x i. + bit i (word_duplicate x) <=> + i < dimindex(:N) /\ bit (i MOD dimindex(:M)) x + + VAL_WORD_DUPLICATE = + |- !x k. + dimindex(:N) <= k * dimindex(:M) + ==> val (word_duplicate x) = + ((2 EXP (k * dimindex(:M)) - 1) DIV (2 EXP dimindex(:M) - 1) * + val x) MOD + 2 EXP dimindex(:N) + + WORD_DUPLICATE = + |- !m k. + dimindex(:N) <= k * dimindex(:M) + ==> word_duplicate (word m) = + word + ((2 EXP (k * dimindex(:M)) - 1) DIV (2 EXP dimindex(:M) - 1) * + m MOD 2 EXP dimindex(:M)) + + WORD_DUPLICATE_DOUBLE = + |- !x. word_duplicate (word_join x x) = word_duplicate x + + WORD_DUPLICATE_REFL = + |- !x. word_duplicate x = x + + WORD_SUBWORD_DUPLICATE = + |- !x pos len. + pos MOD dimindex(:M) + len <= dimindex(:M) /\ + pos + len <= dimindex(:N) + ==> word_subword (word_duplicate x) (pos,len) = + word_subword x (pos MOD dimindex(:M),len) + +The relevant conversions like BIT_WORD_CONV, SIMPLE_WORD_SUBWORD_CONV +and WORD_RED_CONV have all been updated to take these three new operations +into account. + +Tue 22nd Oct 2024 Library/words.ml + +Added several new lemmas for "simple subwords of composite word +expressions": + + WORD_SUBWORD_INSERT_INNER + WORD_SUBWORD_INSERT_OUTER + WORD_SUBWORD_JOIN_LOWER + WORD_SUBWORD_JOIN_UPPER + WORD_SUBWORD_SUBWORD + WORD_SUBWORD_TRIVIAL + +as well as a new conversion WORD_SIMPLE_SUBWORD_CONV that packages +them up into a simplifying function, e.g. + + # WORD_SIMPLE_SUBWORD_CONV `word_subword (x:int16) (0,16):int16`;; + val it : thm = |- word_subword x (0,16) = x + + # WORD_SIMPLE_SUBWORD_CONV + `word_subword (word_join (x:int16) (y:int16):int32) (0,16):int16`;; + val it : thm = |- word_subword (word_join x y) (0,16) = word_subword y (0,16) + + # WORD_SIMPLE_SUBWORD_CONV + `word_subword (word_subword (x:int64) (32,32):int32) (0,16):int16`;; + val it : thm = + |- word_subword (word_subword x (32,32)) (0,16) = word_subword x (32,16) + +Tue 22nd Oct 2024 README, hol.ml, hol_4.sh, hol_4.14.sh, opam [new file], META [new file] + +Added updates from June Lee with new files containing metadata for +opam, as well as appropriately updated instructions in README to +reflect that fact that now HOL Light can indeed now be installed via +opam. + +This update also increases the version string to "3.0.0+" to reflect +the freezing of a release of that name on the github page and adds a +new option "-dir" to the hol.sh script that will print the HOL Light +directory. + Wed 16th Oct 2024 Library/ringtheory.ml Fixed identical degenerate-case bugs in the decision procedures diff --git a/Library/matroids.ml b/Library/matroids.ml new file mode 100644 index 00000000..4426f8ae --- /dev/null +++ b/Library/matroids.ml @@ -0,0 +1,1529 @@ +(* ========================================================================= *) +(* Axiomatic approach to independence. This is matroid-like but without *) +(* any finiteness assumptions, closely following Pete Clark's "Field Theory" *) +(* notes (http://alpha.math.uga.edu/~pete/FieldTheory.pdf), section 11.4. *) +(* ========================================================================= *) + +needs "Library/card.ml";; + +(* ------------------------------------------------------------------------- *) +(* Basic finitary matroid type definition. *) +(* ------------------------------------------------------------------------- *) + +let matroid_tybij = + let eth = prove + (`?m. (!s:A->bool. s SUBSET FST m ==> SND m s SUBSET FST m) /\ + (!s:A->bool. s SUBSET FST m ==> s SUBSET SND m s) /\ + (!s t. s SUBSET t /\ t SUBSET FST m ==> SND m s SUBSET SND m t) /\ + (!s. s SUBSET FST m ==> SND m (SND m s) = SND m s) /\ + (!s x. s SUBSET FST m /\ x IN SND m s + ==> ?s'. FINITE s' /\ s' SUBSET s /\ x IN SND m (s')) /\ + (!s x y. s SUBSET FST m /\ x IN FST m /\ + y IN SND m (x INSERT s) /\ ~(y IN SND m s) + ==> x IN SND m (y INSERT s))`, + EXISTS_TAC `({}:A->bool,(\x:A->bool. x))` THEN SET_TAC[]) in + new_type_definition "matroid" ("matroid","dest_matroid") eth;; + +let matroid_set = new_definition + `matroid_set:A matroid->A->bool = \m. FST(dest_matroid m)`;; + +let matroid_span = new_definition + `matroid_span = \m:A matroid. SND(dest_matroid m)`;; + +let [MATROID_SPAN_SUBSET; MATROID_SPAN_SUPERSET; MATROID_SPAN_MONO; + MATROID_SPAN_SPAN; MATROID_SPAN_FINITARY; MATROID_SPAN_EXCHANGE] = + (map (GEN `m:A matroid`) o CONJUNCTS) + (REWRITE_RULE(CONJUNCT1 matroid_tybij:: + map (REWRITE_RULE[] o ONCE_REWRITE_RULE[FUN_EQ_THM] o SYM) + [matroid_set; matroid_span]) + (SPEC `dest_matroid(m:A matroid)` (CONJUNCT2 matroid_tybij)));; + +let MATROID_SPAN_INC = prove + (`!(m:A matroid) s x. + s SUBSET matroid_set m /\ x IN s ==> x IN matroid_span m s`, + MESON_TAC[MATROID_SPAN_SUPERSET; SUBSET]);; + +let SUBSET_MATROID_SPAN = prove + (`!(m:A matroid) s t. + s SUBSET matroid_set m /\ t SUBSET matroid_set m + ==> (matroid_span m s SUBSET matroid_span m t <=> + s SUBSET matroid_span m t)`, + MESON_TAC[MATROID_SPAN_MONO; MATROID_SPAN_SPAN; MATROID_SPAN_SUBSET; + MATROID_SPAN_SUPERSET; SUBSET_TRANS]);; + +let MATROID_SPAN_MINIMAL = prove + (`!(m:A matroid) s t. + t SUBSET matroid_set m /\ + s SUBSET matroid_span m t + ==> matroid_span m s SUBSET matroid_span m t`, + MESON_TAC[SUBSET_MATROID_SPAN; MATROID_SPAN_SUBSET; SUBSET_TRANS]);; + +let MATROID_SPAN_SET = prove + (`!(m:A matroid). matroid_span m (matroid_set m) = matroid_set m`, + REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ] THEN + MESON_TAC[MATROID_SPAN_SUPERSET; SUBSET_REFL; MATROID_SPAN_SUBSET]);; + +let MATROID_SPAN_EQ = prove + (`!(m:A matroid) s t. + s SUBSET matroid_set m /\ t SUBSET matroid_set m + ==> (matroid_span m s = matroid_span m t <=> + s SUBSET matroid_span m t /\ t SUBSET matroid_span m s)`, + SIMP_TAC[GSYM SUBSET_ANTISYM_EQ; SUBSET_MATROID_SPAN]);; + +let MATROID_SPAN_EQ_SET = prove + (`!(m:A matroid) s. + s SUBSET matroid_set m + ==> (matroid_span m s = matroid_set m <=> + matroid_set m SUBSET matroid_span m s)`, + MESON_TAC[MATROID_SPAN_EQ; SUBSET_REFL; MATROID_SPAN_SET]);; + +let MATROID_SPAN_SUBSET_EQ = prove + (`!(m:A matroid) s t. + s SUBSET t /\ t SUBSET matroid_set m + ==> (matroid_span m s = matroid_span m t <=> + t SUBSET matroid_span m s)`, + MESON_TAC[MATROID_SPAN_EQ; SUBSET_TRANS; MATROID_SPAN_SUPERSET]);; + +let MATROID_SPAN_INTER_SUBSET = prove + (`!(m:A matroid) s t. + s SUBSET matroid_set m /\ t SUBSET matroid_set m + ==> matroid_span m (s INTER t) SUBSET + matroid_span m s INTER matroid_span m t`, + REWRITE_TAC[SUBSET_INTER] THEN REPEAT STRIP_TAC THEN + MATCH_MP_TAC MATROID_SPAN_MONO THEN ASM SET_TAC[]);; + +let MATROID_SPAN_UNION_SUBSET = prove + (`!(m:A matroid) s t. + s SUBSET matroid_set m /\ t SUBSET matroid_set m + ==> matroid_span m s UNION matroid_span m t SUBSET + matroid_span m (s UNION t)`, + REWRITE_TAC[UNION_SUBSET] THEN REPEAT STRIP_TAC THEN + MATCH_MP_TAC MATROID_SPAN_MONO THEN ASM SET_TAC[]);; + +let MATROID_SPAN_EXCHANGE_DELETE = prove + (`!(m:A matroid) a b s. + s SUBSET matroid_set m /\ + b IN matroid_set m /\ + a IN matroid_span m s /\ + ~(a IN matroid_span m (s DELETE b)) + ==> b IN matroid_span m (a INSERT (s DELETE b))`, + REPEAT STRIP_TAC THEN MATCH_MP_TAC MATROID_SPAN_EXCHANGE THEN + ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN + FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE + `x IN s ==> s SUBSET t ==> x IN t`)) THEN + MATCH_MP_TAC MATROID_SPAN_MONO THEN ASM SET_TAC[]);; + +let MATROID_SPAN_UNION_EQ = prove + (`!m s t:A->bool. + s SUBSET matroid_set m /\ t SUBSET matroid_set m + ==> (matroid_span m (s UNION t) = matroid_span m t <=> + s SUBSET matroid_span m t)`, + REPEAT STRIP_TAC THEN + MP_TAC(ISPECL [`m:A matroid`; `t:A->bool`; `s UNION t:A->bool`] + MATROID_SPAN_SUBSET_EQ) THEN + ASM_REWRITE_TAC[UNION_SUBSET; SUBSET_UNION] THEN + ASM_MESON_TAC[MATROID_SPAN_SUPERSET]);; + +let MATROID_SPAN_INSERT_EQ = prove + (`!(m:A matroid) s x. + s SUBSET matroid_set m /\ x IN matroid_set m + ==> (matroid_span m (x INSERT s) = matroid_span m s <=> + x IN matroid_span m s)`, + ONCE_REWRITE_TAC[SET_RULE `x INSERT s = {x} UNION s`] THEN + MESON_TAC[GSYM SING_SUBSET; MATROID_SPAN_UNION_EQ]);; + +let MATROID_SPAN_DELETE_EQ = prove + (`!(m:A matroid) s x. + x IN s /\ s SUBSET matroid_set m + ==> (matroid_span m (s DELETE x) = matroid_span m s <=> + x IN matroid_span m (s DELETE x))`, + SIMP_TAC[MATROID_SPAN_SUBSET_EQ; DELETE_SUBSET] THEN + ASM_MESON_TAC[MATROID_SPAN_SUPERSET; SET_RULE + `x IN s ==> (s SUBSET t <=> x IN t /\ s DELETE x SUBSET t)`]);; + +let MATROID_SPAN_TRANS = prove + (`!(m:A matroid) x y s. + s SUBSET matroid_set m /\ + x IN matroid_span m s /\ + y IN matroid_span m (x INSERT s) + ==> y IN matroid_span m s`, + MESON_TAC[SUBSET; MATROID_SPAN_SUBSET; MATROID_SPAN_INSERT_EQ]);; + +let MATROID_SPAN_FINITARY_GEN = prove + (`!(m:A matroid) s k. + s SUBSET matroid_set m /\ + FINITE k /\ k SUBSET matroid_span m s + ==> exists s'. FINITE s' /\ s' SUBSET s /\ k SUBSET matroid_span m s'`, + GEN_TAC THEN GEN_TAC THEN + REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN + MATCH_MP_TAC FINITE_INDUCT_STRONG THEN + REWRITE_TAC[EMPTY_SUBSET; INSERT_SUBSET; IMP_IMP; GSYM CONJ_ASSOC] THEN + CONJ_TAC THENL [MESON_TAC[FINITE_EMPTY; EMPTY_SUBSET]; ALL_TAC] THEN + MAP_EVERY X_GEN_TAC [`x:A`; `k:A->bool`] THEN + DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN + ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN + X_GEN_TAC `t:A->bool` THEN STRIP_TAC THEN + MP_TAC(ISPECL [`m:A matroid`; `s:A->bool`; `x:A`] MATROID_SPAN_FINITARY) THEN + ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN + X_GEN_TAC `u:A->bool` THEN STRIP_TAC THEN + EXISTS_TAC `t UNION u:A->bool` THEN + ASM_REWRITE_TAC[FINITE_UNION; UNION_SUBSET] THEN CONJ_TAC THENL + [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE + `x IN s ==> s SUBSET t ==> x IN t`)); + FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP + (REWRITE_RULE[IMP_CONJ] SUBSET_TRANS))] THEN + MATCH_MP_TAC MATROID_SPAN_MONO THEN ASM SET_TAC[]);; + +let MATROID_SPAN_FINITARY_MINIMAL = prove + (`!(m:A matroid) s x. + s SUBSET matroid_set m /\ + x IN matroid_span m s + ==> ?t. FINITE t /\ t SUBSET s /\ x IN matroid_span m t /\ + !t'. t' PSUBSET t ==> ~(x IN matroid_span m t')`, + REPEAT STRIP_TAC THEN + MP_TAC(ISPECL [`m:A matroid`; `s:A->bool`; `x:A`] MATROID_SPAN_FINITARY) THEN + ASM_REWRITE_TAC[] THEN + DISCH_THEN(X_CHOOSE_THEN `u:A->bool` STRIP_ASSUME_TAC) THEN + FIRST_ASSUM(MP_TAC o MATCH_MP WF_PSUBSET) THEN REWRITE_TAC[WF] THEN + DISCH_THEN(MP_TAC o SPEC + `\s. s SUBSET u /\ (x:A) IN matroid_span m s`) THEN + REWRITE_TAC[] THEN + ANTS_TAC THENL [ASM_MESON_TAC[SUBSET_REFL]; MATCH_MP_TAC MONO_EXISTS] THEN + GEN_TAC THEN STRIP_TAC THEN CONJ_TAC THENL + [ASM_MESON_TAC[FINITE_SUBSET]; ASM SET_TAC[]]);; + +(* ------------------------------------------------------------------------- *) +(* Definitions of linear algebra notions in terms of span. *) +(* We build in the assumption that they are subsets of the overall set. *) +(* ------------------------------------------------------------------------- *) + +let matroid_spanning = new_definition + `matroid_spanning (m:A matroid) s <=> + s SUBSET matroid_set m /\ matroid_span m s = matroid_set m`;; + +let matroid_independent = new_definition + `matroid_independent (m:A matroid) s <=> + s SUBSET matroid_set m /\ + !x. x IN s ==> ~(x IN matroid_span m (s DELETE x))`;; + +let matroid_basis = new_definition + `matroid_basis (m:A matroid) s <=> + matroid_spanning m s /\ matroid_independent m s`;; + +let MATROID_SPANNING_IMP_SUBSET = prove + (`!(m:A matroid) s. matroid_spanning m s ==> s SUBSET matroid_set m`, + SIMP_TAC[matroid_spanning]);; + +let MATROID_INDEPENDENT_IMP_SUBSET = prove + (`!(m:A matroid) s. matroid_independent m s ==> s SUBSET matroid_set m`, + SIMP_TAC[matroid_independent]);; + +let MATROID_BASIS_IMP_SUBSET = prove + (`!(m:A matroid) s. matroid_basis m s ==> s SUBSET matroid_set m`, + SIMP_TAC[matroid_basis; matroid_spanning]);; + +let MATROID_SPANNING_ALT = prove + (`!(m:A matroid) s. + matroid_spanning m s <=> + s SUBSET matroid_set m /\ + matroid_set m SUBSET matroid_span m s`, + REWRITE_TAC[matroid_spanning] THEN MESON_TAC[MATROID_SPAN_EQ_SET]);; + +let MATROID_SPANNING_SET = prove + (`!(m:A matroid). + matroid_spanning m (matroid_set m)`, + SIMP_TAC[matroid_spanning; SUBSET_REFL; MATROID_SPAN_SET]);; + +(* ------------------------------------------------------------------------- *) +(* Properties of independent sets (which in other formulations could *) +(* be the matroid axioms). *) +(* ------------------------------------------------------------------------- *) + +let MATROID_INDEPENDENT_EMPTY = prove + (`!m:A matroid. matroid_independent m {}`, + REWRITE_TAC[matroid_independent; NOT_IN_EMPTY; EMPTY_SUBSET]);; + +let MATROID_INDEPENDENT_MONO = prove + (`!(m:A matroid) s t. + matroid_independent m t /\ s SUBSET t ==> matroid_independent m s`, + REPEAT GEN_TAC THEN REWRITE_TAC[matroid_independent] THEN STRIP_TAC THEN + CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN + X_GEN_TAC `x:A` THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `x:A`) THEN + MP_TAC(ISPECL + [`m:A matroid`; `s DELETE (x:A)`; `t DELETE (x:A)`] MATROID_SPAN_MONO) THEN + ASM SET_TAC[]);; + +let MATROID_INDEPENDENT_FINITARY = prove + (`!(m:A matroid) s. + matroid_independent m s <=> + s SUBSET matroid_set m /\ + !t. FINITE t /\ t SUBSET s ==> matroid_independent m t`, + REPEAT GEN_TAC THEN EQ_TAC THENL + [ASM_MESON_TAC[MATROID_INDEPENDENT_MONO; MATROID_INDEPENDENT_IMP_SUBSET]; + ASM_REWRITE_TAC[matroid_independent] THEN STRIP_TAC] THEN + ASM_REWRITE_TAC[] THEN X_GEN_TAC `x:A` THEN REPEAT STRIP_TAC THEN + MP_TAC(ISPECL + [`m:A matroid`; `s DELETE (x:A)`; `x:A`] MATROID_SPAN_FINITARY) THEN + ANTS_TAC THENL [ASM SET_TAC[]; REWRITE_TAC[LEFT_IMP_EXISTS_THM]] THEN + X_GEN_TAC `t:A->bool` THEN + REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN + FIRST_X_ASSUM(MP_TAC o SPEC `(x:A) INSERT t`) THEN ANTS_TAC THENL + [ASM_REWRITE_TAC[FINITE_INSERT] THEN ASM SET_TAC[]; + DISCH_THEN(MP_TAC o SPEC `x:A` o CONJUNCT2)] THEN + ASM_REWRITE_TAC[IN_INSERT; CONTRAPOS_THM] THEN + MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN AP_TERM_TAC THEN ASM SET_TAC[]);; + +let MATROID_INDEPENDENT_INSERT = prove + (`!(m:A matroid) s a. + matroid_independent m (a INSERT s) <=> + if a IN s then matroid_independent m s + else a IN matroid_set m /\ + matroid_independent m s /\ + ~(a IN matroid_span m s)`, + REPEAT STRIP_TAC THEN COND_CASES_TAC THEN + ASM_SIMP_TAC[SET_RULE `a IN s ==> a INSERT s = s`] THEN + REWRITE_TAC[matroid_independent; INSERT_SUBSET; FORALL_IN_INSERT] THEN + ASM_CASES_TAC `(a:A) IN matroid_set m` THEN ASM_REWRITE_TAC[] THEN + ASM_CASES_TAC `(s:A->bool) SUBSET matroid_set m` THEN ASM_REWRITE_TAC[] THEN + ASM_SIMP_TAC[SET_RULE `~(a IN s) ==> (a INSERT s) DELETE a = s`] THEN + REWRITE_TAC[TAUT `(~p /\ q <=> q' /\ ~p) <=> ~p ==> (q <=> q')`] THEN + DISCH_TAC THEN MATCH_MP_TAC(SET_RULE + `(!x. p x ==> (q x <=> r x)) + ==> ((!x. p x ==> ~q x) <=> (!x. p x ==> ~r x))`) THEN + X_GEN_TAC `b:A` THEN DISCH_TAC THEN EQ_TAC THENL + [ALL_TAC; + MATCH_MP_TAC(SET_RULE `s SUBSET t ==> a IN s ==> a IN t`) THEN + MATCH_MP_TAC MATROID_SPAN_MONO THEN ASM SET_TAC[]] THEN + ASM_CASES_TAC `b:A = a` THEN + ASM_SIMP_TAC[SET_RULE `~(a IN s) ==> (a INSERT s) DELETE a = s`] THEN + ASM_SIMP_TAC[SET_RULE + `~(a IN s) /\ ~(b = a) + ==> ((a INSERT s) DELETE b = a INSERT (s DELETE b))`] THEN + MP_TAC(ISPECL [`m:A matroid`; `s DELETE (b:A)`; `a:A`; `b:A`] + MATROID_SPAN_EXCHANGE) THEN + ASM_SIMP_TAC[SET_RULE `b IN s ==> b INSERT (s DELETE b) = s`] THEN + ASM SET_TAC[]);; + +let MATROID_SPAN_PSUBSET_INDEPENDENT = prove + (`!(m:A matroid) s t. + s PSUBSET t /\ matroid_independent m t + ==> matroid_span m s PSUBSET matroid_span m t`, + REPEAT STRIP_TAC THEN + FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [PSUBSET_ALT]) THEN + DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC + (X_CHOOSE_THEN `x:A` STRIP_ASSUME_TAC)) THEN + FIRST_ASSUM(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `x:A`) o + GEN_REWRITE_RULE I [matroid_independent]) THEN + ASM_SIMP_TAC[PSUBSET_ALT; MATROID_SPAN_MONO] THEN + DISCH_TAC THEN EXISTS_TAC `(x:A)` THEN + MP_TAC(SPECL [`m:A matroid`; `s:A->bool`; `t DELETE (x:A)`] + MATROID_SPAN_MONO) THEN + ASM SET_TAC[MATROID_SPAN_INC]);; + +let MATROID_SPANNING_SUBSET_INDEPENDENT = prove + (`!(m:A matroid) s t. + t SUBSET s /\ matroid_independent m s /\ s SUBSET matroid_span m t + ==> s = t`, + SIMP_TAC[GSYM SUBSET_ANTISYM_EQ] THEN REPEAT STRIP_TAC THEN + REWRITE_TAC[SUBSET] THEN X_GEN_TAC `a:A` THEN DISCH_TAC THEN + FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [matroid_independent]) THEN + DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `a:A`)) THEN + MP_TAC(ISPECL [`m:A matroid`; `t:A->bool`; `s DELETE (a:A)`] + MATROID_SPAN_MONO) THEN + ASM SET_TAC[]);; + +let MATROID_SPANNING_PSUBSET_INDEPENDENT = prove + (`!(m:A matroid) s t. + ~(s PSUBSET t /\ matroid_spanning m s /\ matroid_independent m t)`, + REPEAT STRIP_TAC THEN + MP_TAC(ISPECL [`m:A matroid`; `s:A->bool`; `t:A->bool`] + MATROID_SPAN_PSUBSET_INDEPENDENT) THEN + ASM_REWRITE_TAC[] THEN + MATCH_MP_TAC(SET_RULE `s SUBSET t ==> ~(t PSUBSET s)`) THEN + ASM_MESON_TAC[MATROID_SPAN_SUBSET; matroid_spanning; matroid_independent]);; + +let MATROID_MAXIMAL_INDEPENDENT_SUBSET_SPAN = prove + (`!(m:A matroid) s t. + s SUBSET t /\ t SUBSET matroid_set m /\ + matroid_independent m s /\ + (!s'. s PSUBSET s' /\ s' SUBSET t ==> ~matroid_independent m s') + ==> matroid_span m s = matroid_span m t`, + REPEAT STRIP_TAC THEN + FIRST_ASSUM(ASSUME_TAC o MATCH_MP MATROID_INDEPENDENT_IMP_SUBSET) THEN + MATCH_MP_TAC SUBSET_ANTISYM THEN ASM_SIMP_TAC[MATROID_SPAN_MONO] THEN + ASM_SIMP_TAC[SUBSET_MATROID_SPAN] THEN + REWRITE_TAC[SUBSET] THEN X_GEN_TAC `x:A` THEN DISCH_TAC THEN + FIRST_X_ASSUM(MP_TAC o SPEC `(x:A) INSERT s`) THEN + ASM_REWRITE_TAC[MATROID_INDEPENDENT_INSERT] THEN COND_CASES_TAC THEN + ASM_REWRITE_TAC[SET_RULE `s PSUBSET x INSERT s <=> ~(x IN s)`] THEN + ASM_MESON_TAC[SUBSET; INSERT_SUBSET; MATROID_SPAN_SUPERSET]);; + +let MATROID_BASIS_EQ_MAXIMAL_INDEPENDENT = prove + (`!(m:A matroid) s. + matroid_basis m s <=> + matroid_independent m s /\ + !s'. s PSUBSET s' ==> ~matroid_independent m s'`, + REPEAT GEN_TAC THEN EQ_TAC THENL + [ASM_MESON_TAC[MATROID_SPANNING_PSUBSET_INDEPENDENT; matroid_basis]; + STRIP_TAC THEN ASM_REWRITE_TAC[matroid_basis]] THEN + FIRST_ASSUM(ASSUME_TAC o MATCH_MP MATROID_INDEPENDENT_IMP_SUBSET) THEN + ASM_REWRITE_TAC[matroid_spanning] THEN + ONCE_REWRITE_TAC[GSYM MATROID_SPAN_SET] THEN + MATCH_MP_TAC MATROID_MAXIMAL_INDEPENDENT_SUBSET_SPAN THEN + ASM_SIMP_TAC[SUBSET_REFL]);; + +let MATROID_BASIS_EQ_MINIMAL_SPANNING = prove + (`!(m:A matroid) s. + matroid_basis m s <=> + matroid_spanning m s /\ + !s'. s' PSUBSET s ==> ~matroid_spanning m s'`, + REPEAT GEN_TAC THEN EQ_TAC THENL + [ASM_MESON_TAC[MATROID_SPANNING_PSUBSET_INDEPENDENT; matroid_basis]; + STRIP_TAC THEN ASM_REWRITE_TAC[matroid_basis]] THEN + FIRST_ASSUM(ASSUME_TAC o MATCH_MP MATROID_SPANNING_IMP_SUBSET) THEN + ASM_REWRITE_TAC[matroid_independent] THEN + X_GEN_TAC `x:A` THEN REPEAT STRIP_TAC THEN + FIRST_X_ASSUM(MP_TAC o SPEC `s DELETE (x:A)`) THEN + REWRITE_TAC[matroid_spanning; NOT_IMP] THEN + REPEAT(CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC]) THEN + ASM_MESON_TAC[MATROID_SPAN_DELETE_EQ; matroid_spanning]);; + +let MATROID_INDEPENDENT_CHAIN = prove + (`!(m:A matroid) c. + (!s. s IN c ==> matroid_independent m s) /\ + (!s t. s IN c /\ t IN c ==> s SUBSET t \/ t SUBSET s) + ==> matroid_independent m (UNIONS c)`, + REPEAT STRIP_TAC THEN + ASM_CASES_TAC `c:(A->bool)->bool = {}` THEN + ASM_REWRITE_TAC[UNIONS_0; MATROID_INDEPENDENT_EMPTY] THEN + ONCE_REWRITE_TAC[MATROID_INDEPENDENT_FINITARY] THEN CONJ_TAC THENL + [RULE_ASSUM_TAC(REWRITE_RULE[matroid_independent]) THEN ASM SET_TAC[]; + X_GEN_TAC `s:A->bool` THEN STRIP_TAC] THEN + MP_TAC(ISPECL [`c:(A->bool)->bool`; `s:A->bool`] + FINITE_SUBSET_UNIONS_CHAIN) THEN + ASM_MESON_TAC[MATROID_INDEPENDENT_MONO]);; + +let MATROID_SPAN_CHAIN = prove + (`!(m:A matroid) c. + ~(c = {}) /\ + (!s. s IN c ==> s SUBSET matroid_set m) /\ + (!s t. s IN c /\ t IN c ==> s SUBSET t \/ t SUBSET s) + ==> matroid_span m (UNIONS c) = UNIONS {matroid_span m s | s IN c}`, + REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL + [REWRITE_TAC[SUBSET] THEN X_GEN_TAC `a:A` THEN DISCH_TAC; + REWRITE_TAC[UNIONS_SUBSET; FORALL_IN_GSPEC] THEN + REPEAT STRIP_TAC THEN MATCH_MP_TAC MATROID_SPAN_MONO THEN + ASM SET_TAC[]] THEN + FIRST_X_ASSUM(MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ_ALT] + MATROID_SPAN_FINITARY)) THEN + ASM_REWRITE_TAC[UNIONS_SUBSET] THEN + DISCH_THEN(X_CHOOSE_THEN `t:A->bool` STRIP_ASSUME_TAC) THEN + MP_TAC(ISPECL [`c:(A->bool)->bool`; `t:A->bool`] + FINITE_SUBSET_UNIONS_CHAIN) THEN + ASM SET_TAC[MATROID_SPAN_MONO]);; + +let MATROID_INTERMEDIATE_SPAN = prove + (`!(m:A matroid) s t. + matroid_independent m s /\ + t SUBSET matroid_set m /\ + s SUBSET matroid_span m t + ==> ?b. s SUBSET b /\ b SUBSET (s UNION t) /\ + matroid_independent m b /\ + matroid_span m b = matroid_span m t`, + REPEAT STRIP_TAC THEN + MP_TAC(ISPEC `\u:A->bool. s SUBSET u /\ u SUBSET (s UNION t) /\ + matroid_independent m u` + ZL_SUBSETS_UNIONS_NONEMPTY) THEN + ASM_REWRITE_TAC[] THEN ANTS_TAC THENL + [CONJ_TAC THENL [EXISTS_TAC `s:A->bool` THEN ASM SET_TAC[]; ALL_TAC] THEN + X_GEN_TAC `c:(A->bool)->bool` THEN STRIP_TAC THEN + ASM_SIMP_TAC[MATROID_INDEPENDENT_CHAIN; UNION_SUBSET] THEN ASM SET_TAC[]; + MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `b:A->bool`] THEN + STRIP_TAC THEN ASM_REWRITE_TAC[] THEN + FIRST_ASSUM(ASSUME_TAC o MATCH_MP MATROID_INDEPENDENT_IMP_SUBSET) THEN + MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THEN + MATCH_MP_TAC MATROID_SPAN_MINIMAL THEN + (CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC]) THENL + [TRANS_TAC SUBSET_TRANS `s UNION t:A->bool` THEN + ASM_REWRITE_TAC[UNION_SUBSET] THEN ASM_SIMP_TAC[MATROID_SPAN_SUPERSET]; + REWRITE_TAC[SUBSET] THEN X_GEN_TAC `x:A` THEN DISCH_TAC THEN + FIRST_X_ASSUM(MP_TAC o SPEC `(x:A) INSERT b`) THEN + ASM_REWRITE_TAC[MATROID_INDEPENDENT_INSERT] THEN + COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL + [ASM_MESON_TAC[MATROID_SPAN_INC]; ASM SET_TAC[]]]);; + +let MATROID_INTERMEDIATE_BASIS = prove + (`!(m:A matroid) s t. + matroid_independent m s /\ matroid_spanning m t + ==> ?b. s SUBSET b /\ b SUBSET (s UNION t) /\ matroid_basis m b`, + REWRITE_TAC[matroid_spanning; matroid_basis] THEN REPEAT STRIP_TAC THEN + MP_TAC(ISPECL [`m:A matroid`; `s:A->bool`; `t:A->bool`] + MATROID_INTERMEDIATE_SPAN) THEN + ASM_MESON_TAC[matroid_independent]);; + +let MATROID_INDEPENDENT_EXTENDS_TO_BASIS = prove + (`!(m:A matroid) s. + matroid_independent m s ==> ?b. s SUBSET b /\ matroid_basis m b`, + REPEAT STRIP_TAC THEN + MP_TAC(ISPECL [`m:A matroid`; `s:A->bool`; `matroid_set m:A->bool`] + MATROID_INTERMEDIATE_BASIS) THEN + ASM_REWRITE_TAC[MATROID_SPANNING_SET] THEN MESON_TAC[]);; + +let MATROID_BASIS_EXISTS = prove + (`!(m:A matroid). ?b. matroid_basis m b`, + MESON_TAC[MATROID_INDEPENDENT_EXTENDS_TO_BASIS; MATROID_INDEPENDENT_EMPTY]);; + +let MATROID_SPANNING_CONTAINS_BASIS = prove + (`!(m:A matroid) s. + matroid_spanning m s ==> ?b. b SUBSET s /\ matroid_basis m b`, + REPEAT STRIP_TAC THEN + MP_TAC(ISPECL [`m:A matroid`; `{}:A->bool`; `s:A->bool`] + MATROID_INTERMEDIATE_BASIS) THEN + ASM_REWRITE_TAC[MATROID_INDEPENDENT_EMPTY; UNION_EMPTY] THEN MESON_TAC[]);; + +let MATROID_STEINITZ_EXCHANGE = prove + (`!(m:A matroid) s t. + t SUBSET matroid_set m /\ + FINITE s /\ matroid_independent m s /\ s SUBSET matroid_span m t + ==> ?t'. t' SUBSET t /\ t' HAS_SIZE (CARD s) /\ + matroid_span m ((t DIFF t') UNION s) = matroid_span m t`, + GEN_TAC THEN + GEN_REWRITE_TAC I [SWAP_FORALL_THM] THEN GEN_TAC THEN + REWRITE_TAC[RIGHT_FORALL_IMP_THM; IMP_CONJ] THEN DISCH_TAC THEN + MATCH_MP_TAC FINITE_INDUCT_STRONG THEN CONJ_TAC THENL + [REPEAT STRIP_TAC THEN EXISTS_TAC `{}:A->bool` THEN + REWRITE_TAC[HAS_SIZE; FINITE_EMPTY; EMPTY_SUBSET] THEN + AP_TERM_TAC THEN SET_TAC[]; + MAP_EVERY X_GEN_TAC [`x:A`; `s:A->bool`] THEN REWRITE_TAC[IMP_IMP]] THEN + REWRITE_TAC[INSERT_SUBSET] THEN STRIP_TAC THEN + FIRST_X_ASSUM(MP_TAC o check (is_imp o concl)) THEN ANTS_TAC THENL + [ASM_MESON_TAC[MATROID_INDEPENDENT_MONO; SET_RULE `s SUBSET x INSERT s`]; + DISCH_THEN(X_CHOOSE_THEN `u:A->bool` STRIP_ASSUME_TAC)] THEN + MP_TAC(ISPECL [`m:A matroid`; `t DIFF u UNION s:A->bool`; `x:A`] + MATROID_SPAN_FINITARY_MINIMAL) THEN + ASM_REWRITE_TAC[] THEN ANTS_TAC THENL + [ASM SET_TAC[MATROID_SPAN_SUBSET]; + ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM]] THEN + X_GEN_TAC `v:A->bool` THEN STRIP_TAC THEN + FIRST_ASSUM(DISJ_CASES_THEN MP_TAC o MATCH_MP (SET_RULE + `v SUBSET t UNION s ==> v SUBSET s \/ ?a. a IN v /\ a IN t`)) + THENL + [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [matroid_independent]) THEN + REWRITE_TAC[FORALL_IN_INSERT; INSERT_SUBSET] THEN + ASM_SIMP_TAC[SET_RULE `~(x IN s) ==> (x INSERT s) DELETE x = s`] THEN + ASM_MESON_TAC[MATROID_SPAN_MONO; SUBSET]; + REWRITE_TAC[IN_DIFF; LEFT_IMP_EXISTS_THM]] THEN + X_GEN_TAC `y:A` THEN STRIP_TAC THEN EXISTS_TAC `(y:A) INSERT u` THEN + FIRST_X_ASSUM(STRIP_ASSUME_TAC o GEN_REWRITE_RULE I [HAS_SIZE]) THEN + ABBREV_TAC `n = CARD(s:A->bool)` THEN + ASM_SIMP_TAC[INSERT_SUBSET; HAS_SIZE; CARD_CLAUSES; FINITE_INSERT] THEN + MATCH_MP_TAC SUBSET_ANTISYM THEN + CONJ_TAC THEN MATCH_MP_TAC MATROID_SPAN_MINIMAL THENL + [ASM SET_TAC[MATROID_SPAN_SUPERSET]; ALL_TAC] THEN + CONJ_TAC THENL [ASM SET_TAC[MATROID_SPAN_SUBSET]; ALL_TAC] THEN + TRANS_TAC SUBSET_TRANS `matroid_span (m:A matroid) (t DIFF u UNION s)` THEN + CONJ_TAC THENL [ASM_SIMP_TAC[MATROID_SPAN_SUPERSET]; ALL_TAC] THEN + MATCH_MP_TAC MATROID_SPAN_MINIMAL THEN + CONJ_TAC THENL [ASM SET_TAC[MATROID_SPAN_SUBSET]; ALL_TAC] THEN + TRANS_TAC SUBSET_TRANS + `{y:A} UNION (t DIFF (y INSERT u) UNION (x INSERT s))` THEN CONJ_TAC + THENL [SET_TAC[]; ONCE_REWRITE_TAC[UNION_SUBSET]] THEN CONJ_TAC THENL + [ALL_TAC; + MATCH_MP_TAC MATROID_SPAN_SUPERSET THEN + ASM SET_TAC[MATROID_SPAN_SUBSET]] THEN + TRANS_TAC SUBSET_TRANS `matroid_span m ((x:A) INSERT (v DELETE y))` THEN + CONJ_TAC THENL + [REWRITE_TAC[SING_SUBSET]; + MATCH_MP_TAC MATROID_SPAN_MONO THEN ASM SET_TAC[MATROID_SPAN_SUBSET]] THEN + MATCH_MP_TAC MATROID_SPAN_EXCHANGE THEN + ASM_SIMP_TAC[SET_RULE `y IN v ==> y INSERT (v DELETE y) = v`] THEN + REPEAT(CONJ_TAC THENL [ASM SET_TAC[MATROID_SPAN_SUBSET]; ALL_TAC]) THEN + FIRST_X_ASSUM MATCH_MP_TAC THEN ASM SET_TAC[]);; + +let MATROID_INDEPENDENT_CARD_LE_SPAN_FINITE = prove + (`!(m:A matroid) s t. + FINITE t /\ t SUBSET matroid_set m /\ + matroid_independent m s /\ s SUBSET matroid_span m t + ==> FINITE s /\ CARD s <= CARD t`, + REPEAT GEN_TAC THEN STRIP_TAC THEN + REWRITE_TAC[TAUT `p /\ q <=> ~(p ==> ~q)`] THEN + REWRITE_TAC[ARITH_RULE `~(a <= b) <=> b + 1 <= a`] THEN DISCH_TAC THEN + FIRST_ASSUM(X_CHOOSE_THEN `u:A->bool` STRIP_ASSUME_TAC o + REWRITE_RULE[HAS_SIZE] o MATCH_MP CHOOSE_SUBSET_STRONG) THEN + MP_TAC(ISPECL [`m:A matroid`; `u:A->bool`; `t:A->bool`] + MATROID_STEINITZ_EXCHANGE) THEN + ASM_REWRITE_TAC[NOT_IMP; HAS_SIZE] THEN REPEAT CONJ_TAC THENL + [ASM_MESON_TAC[MATROID_INDEPENDENT_MONO]; + ASM SET_TAC[]; + ASM_MESON_TAC[FINITE_SUBSET; CARD_SUBSET; + ARITH_RULE `m <= n ==> ~(n + 1 = m)`]]);; + +let MATROID_EQ_SPANS_FINITE = prove + (`!(m:A matroid) s t. + matroid_independent m s /\ matroid_independent m t /\ + matroid_span m s = matroid_span m t + ==> (FINITE s <=> FINITE t)`, + MESON_TAC[SUBSET_MATROID_SPAN; SUBSET_REFL; matroid_independent; + MATROID_INDEPENDENT_CARD_LE_SPAN_FINITE]);; + +let MATROID_EQ_SPANS_SIZE = prove + (`!(m:A matroid) s t n. + matroid_independent m s /\ matroid_independent m t /\ + matroid_span m s = matroid_span m t + ==> (s HAS_SIZE n <=> t HAS_SIZE n)`, + REWRITE_TAC[HAS_SIZE] THEN + MESON_TAC[SUBSET_MATROID_SPAN; SUBSET_REFL; matroid_independent; + MATROID_INDEPENDENT_CARD_LE_SPAN_FINITE; LE_ANTISYM]);; + +let MATROID_BASES_FINITE = prove + (`!(m:A matroid) s t. + matroid_basis m s /\ matroid_basis m t ==> (FINITE s <=> FINITE t)`, + REWRITE_TAC[matroid_basis; matroid_spanning] THEN + MESON_TAC[MATROID_EQ_SPANS_FINITE]);; + +let MATROID_BASES_SIZE = prove + (`!(m:A matroid) s t n. + matroid_basis m s /\ matroid_basis m t + ==> (s HAS_SIZE n <=> t HAS_SIZE n)`, + REWRITE_TAC[matroid_basis; matroid_spanning] THEN + MESON_TAC[MATROID_EQ_SPANS_SIZE]);; + +let MATROID_INDEPENDENT_CARD_LE_SPAN = prove + (`!(m:A matroid) s t. + t SUBSET matroid_set m /\ + matroid_independent m s /\ s SUBSET matroid_span m t + ==> s <=_c t`, + let lemma = prove + (`!(m:A matroid) s t. + matroid_independent m s /\ + INFINITE t /\ t SUBSET matroid_set m /\ + matroid_span m t = matroid_span m s + ==> s <=_c t`, + REPEAT STRIP_TAC THEN + SUBGOAL_THEN + `!x:A. x IN t + ==> ?k. FINITE k /\ k SUBSET s /\ x IN matroid_span m k` + MP_TAC THENL + [REPEAT STRIP_TAC THEN MATCH_MP_TAC MATROID_SPAN_FINITARY THEN + ASM_MESON_TAC[MATROID_SPAN_SUPERSET; matroid_independent; SUBSET]; + REWRITE_TAC[RIGHT_IMP_EXISTS_THM; SKOLEM_THM]] THEN + DISCH_THEN(X_CHOOSE_TAC `k:A->A->bool`) THEN + MP_TAC(ISPECL + [`m:A matroid`; `UNIONS {(k:A->A->bool) x | x IN t}`; `s:A->bool`] + MATROID_SPAN_PSUBSET_INDEPENDENT) THEN + ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(SET_RULE + `t SUBSET s /\ (t SUBSET s ==> s' SUBSET t' /\ (s SUBSET t ==> P)) + ==> (t PSUBSET s ==> t' PSUBSET s') ==> P`) THEN + CONJ_TAC THENL + [REWRITE_TAC[UNIONS_SUBSET; FORALL_IN_GSPEC] THEN + ASM_MESON_TAC[MATROID_SPAN_SUPERSET; SUBSET]; + STRIP_TAC] THEN + CONJ_TAC THENL + [FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN + MATCH_MP_TAC MATROID_SPAN_MINIMAL THEN + CONJ_TAC THENL [ASM SET_TAC[matroid_independent]; ALL_TAC] THEN + REWRITE_TAC[SUBSET] THEN X_GEN_TAC `x:A` THEN DISCH_TAC THEN + FIRST_X_ASSUM(MP_TAC o SPEC `x:A`) THEN + ASM_REWRITE_TAC[] THEN STRIP_TAC THEN + FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE + `x IN t ==> t SUBSET s ==> x IN s`)) THEN + MATCH_MP_TAC MATROID_SPAN_MONO THEN + RULE_ASSUM_TAC(REWRITE_RULE[matroid_independent]) THEN ASM SET_TAC[]; + DISCH_THEN(MP_TAC o MATCH_MP CARD_LE_SUBSET) THEN + MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] CARD_LE_TRANS) THEN + MATCH_MP_TAC CARD_LE_UNIONS THEN + ASM_SIMP_TAC[SIMPLE_IMAGE; CARD_LE_IMAGE; FORALL_IN_IMAGE] THEN + ASM_SIMP_TAC[CARD_LE_FINITE_INFINITE]]) in + REPEAT STRIP_TAC THEN ASM_CASES_TAC `FINITE(t:A->bool)` THENL + [ASM_MESON_TAC[MATROID_INDEPENDENT_CARD_LE_SPAN_FINITE; + CARD_LE_CARD]; + RULE_ASSUM_TAC(REWRITE_RULE[GSYM INFINITE])] THEN + MP_TAC(ISPECL [`m:A matroid`; `s:A->bool`; `t:A->bool`] + MATROID_INTERMEDIATE_SPAN) THEN + ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN + X_GEN_TAC `b:A->bool` THEN STRIP_TAC THEN + TRANS_TAC CARD_LE_TRANS `b:A->bool` THEN + ASM_SIMP_TAC[CARD_LE_SUBSET] THEN MATCH_MP_TAC lemma THEN ASM_MESON_TAC[]);; + +let MATROID_INDEPENDENT_CARD_LE_SPANNING = prove + (`!(m:A matroid) s t. + matroid_independent m s /\ matroid_spanning m t + ==> s <=_c t`, + REWRITE_TAC[matroid_spanning] THEN + REPEAT STRIP_TAC THEN MATCH_MP_TAC MATROID_INDEPENDENT_CARD_LE_SPAN THEN + ASM_MESON_TAC[matroid_independent]);; + +let MATROID_EQ_SPANS_CARD_EQ = prove + (`!(m:A matroid) s t. + matroid_independent m s /\ matroid_independent m t /\ + matroid_span m s = matroid_span m t + ==> s =_c t`, + GEN_TAC THEN REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN + MESON_TAC[MATROID_INDEPENDENT_CARD_LE_SPAN; matroid_independent; + MATROID_SPAN_SUPERSET]);; + +let MATROID_BASES_CARD_EQ = prove + (`!(m:A matroid) s t. + matroid_basis m s /\ matroid_basis m t ==> s =_c t`, + REWRITE_TAC[matroid_basis; matroid_spanning] THEN + MESON_TAC[MATROID_EQ_SPANS_CARD_EQ]);; + +let MATROID_INDEPENDENT_SPANNING_FINITE = prove + (`!(m:A matroid) s t. + matroid_independent m s /\ matroid_spanning m t /\ FINITE t + ==> FINITE s`, + MESON_TAC[CARD_LE_FINITE; MATROID_INDEPENDENT_CARD_LE_SPANNING]);; + +(* ------------------------------------------------------------------------- *) +(* Subspaces, i.e. sets closed under the matroid span operation. *) +(* ------------------------------------------------------------------------- *) + +let matroid_subspace = new_definition + `matroid_subspace (m:A matroid) s <=> + s SUBSET matroid_set m /\ matroid_span m s = s`;; + +let MATROID_SUBSPACE_IMP_SUBSET = prove + (`!(m:A matroid) s. matroid_subspace m s ==> s SUBSET matroid_set m`, + SIMP_TAC[matroid_subspace]);; + +let MATROID_SUBSPACE_SET = prove + (`!m:A matroid. matroid_subspace m (matroid_set m)`, + REWRITE_TAC[matroid_subspace; SUBSET_REFL; MATROID_SPAN_SET]);; + +let MATROID_SUBSPACE_SPAN = prove + (`!(m:A matroid) s. + s SUBSET matroid_set m + ==> matroid_subspace m (matroid_span m s)`, + SIMP_TAC[matroid_subspace; MATROID_SPAN_SUBSET; MATROID_SPAN_SPAN]);; + +let MATROID_SUBSPACE = prove + (`!(m:A matroid) s. + matroid_subspace m s <=> + s SUBSET matroid_set m /\ matroid_span m s SUBSET s`, + REWRITE_TAC[matroid_subspace; GSYM SUBSET_ANTISYM_EQ] THEN + MESON_TAC[MATROID_SPAN_SUPERSET]);; + +let MATROID_SUBSPACE_INTERS = prove + (`!(m:A matroid) f. + ~(f = {}) /\ (!s. s IN f ==> matroid_subspace m s) + ==> matroid_subspace m (INTERS f)`, + REPEAT STRIP_TAC THEN REWRITE_TAC[MATROID_SUBSPACE; SUBSET_INTERS] THEN + RULE_ASSUM_TAC(REWRITE_RULE[matroid_subspace]) THEN + CONJ_TAC THENL [ASM SET_TAC[]; X_GEN_TAC `s:A->bool` THEN STRIP_TAC] THEN + FIRST_X_ASSUM(MP_TAC o SPEC `s:A->bool`) THEN ASM_REWRITE_TAC[] THEN + DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (SUBST1_TAC o SYM)) THEN + MATCH_MP_TAC MATROID_SPAN_MONO THEN ASM SET_TAC[]);; + +let MATROID_SUBSPACE_INTER = prove + (`!(m:A matroid) s t. + matroid_subspace m s /\ matroid_subspace m t + ==> matroid_subspace m (s INTER t)`, + REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM INTERS_2] THEN + MATCH_MP_TAC MATROID_SUBSPACE_INTERS THEN ASM SET_TAC[]);; + +let MATROID_SPAN_INTER_SPANS = prove + (`!(m:A matroid) s t. + s SUBSET matroid_set m /\ t SUBSET matroid_set m + ==> matroid_span m (matroid_span m s INTER matroid_span m t) = + matroid_span m s INTER matroid_span m t`, + MESON_TAC[matroid_subspace; MATROID_SPAN_SPAN; MATROID_SPAN_SUBSET; + MATROID_SUBSPACE_INTER]);; + +let MATROID_SUBSPACE_CHAIN = prove + (`!(m:A matroid) c. + ~(c = {}) /\ + (!s. s IN c ==> matroid_subspace m s) /\ + (!s t. s IN c /\ t IN c ==> s SUBSET t \/ t SUBSET s) + ==> matroid_subspace m (UNIONS c)`, + REWRITE_TAC[matroid_subspace] THEN + ASM_SIMP_TAC[MATROID_SPAN_CHAIN] THEN SET_TAC[]);; + +let MATROID_SPAN_SUBSPACE = prove + (`!(m:A matroid) s b. + b SUBSET s /\ s SUBSET matroid_span m b /\ matroid_subspace m s + ==> matroid_span m b = s`, + SIMP_TAC[GSYM SUBSET_ANTISYM_EQ] THEN + MESON_TAC[MATROID_SPAN_MINIMAL; matroid_subspace]);; + +let MATROID_SPAN_EQ_SELF = prove + (`!(m:A matroid) s. + s SUBSET matroid_set m + ==> (matroid_span m s = s <=> matroid_subspace m s)`, + SIMP_TAC[matroid_subspace]);; + +let MATROID_SPAN_OF_SUBSPACE = prove + (`!(m:A matroid) s. + matroid_subspace m s ==> matroid_span m s = s`, + SIMP_TAC[matroid_subspace]);; + +let MATROID_SPAN_SUBSET_SUBSPACE = prove + (`!(m:A matroid) s t. + s SUBSET t /\ matroid_subspace m t ==> matroid_span m s SUBSET t`, + MESON_TAC[matroid_subspace; MATROID_SPAN_MONO]);; + +(* ------------------------------------------------------------------------- *) +(* Sub-matroids *) +(* ------------------------------------------------------------------------- *) + +let submatroid = new_definition + `submatroid (m:A matroid) s = + matroid(matroid_span m (matroid_set m INTER s),matroid_span m)`;; + +let SUBMATROID_GEN = prove + (`(!m s:A->bool. matroid_set (submatroid m s) = + matroid_span m (matroid_set m INTER s)) /\ + (!m s:A->bool. matroid_span (submatroid m s) = matroid_span m)`, + REWRITE_TAC[AND_FORALL_THM] THEN REPEAT GEN_TAC THEN + GEN_REWRITE_TAC (BINOP_CONV o LAND_CONV o ONCE_DEPTH_CONV) + [matroid_set; matroid_span] THEN + REWRITE_TAC[GSYM PAIR_EQ; submatroid] THEN + REWRITE_TAC[GSYM(CONJUNCT2 matroid_tybij)] THEN + MP_TAC(ISPECL [`m:A matroid`; `matroid_set m INTER s:A->bool`] + MATROID_SPAN_SUBSET) THEN + REWRITE_TAC[INTER_SUBSET] THEN REPEAT STRIP_TAC THENL + [MATCH_MP_TAC MATROID_SPAN_MINIMAL; + MATCH_MP_TAC MATROID_SPAN_SUPERSET; + MATCH_MP_TAC MATROID_SPAN_MONO; + MATCH_MP_TAC MATROID_SPAN_SPAN; + MATCH_MP_TAC MATROID_SPAN_FINITARY; + MATCH_MP_TAC MATROID_SPAN_EXCHANGE] THEN + ASM SET_TAC[]);; + +let SUBMATROID = prove + (`(!m s:A->bool. + matroid_subspace m s ==> matroid_set (submatroid m s) = s) /\ + (!m s:A->bool. matroid_span (submatroid m s) = matroid_span m)`, + REWRITE_TAC[SUBMATROID_GEN] THEN + SIMP_TAC[matroid_subspace; SET_RULE `s SUBSET u ==> u INTER s = s`]);; + +let SUBMATROID_SPAN = prove + (`!m s:A->bool. + s SUBSET matroid_set m + ==> submatroid m (matroid_span m s) = submatroid m s`, + SIMP_TAC[submatroid; MATROID_SPAN_SPAN; MATROID_SPAN_SUBSET; + SET_RULE `t SUBSET s ==> s INTER t = t`]);; + +let SUBMATROID_SUBSET = prove + (`(!m s:A->bool. + s SUBSET matroid_set m + ==> matroid_set (submatroid m s) = matroid_span m s) /\ + (!m s:A->bool. matroid_span (submatroid m s) = matroid_span m)`, + MESON_TAC[SUBMATROID_SPAN; SUBMATROID; MATROID_SUBSPACE_SPAN]);; + +let SUBMATROID_SET = prove + (`!m:A matroid. submatroid m (matroid_set m) = m`, + REWRITE_TAC[submatroid; INTER_IDEMPOT; MATROID_SPAN_SET] THEN + REWRITE_TAC[matroid_set; matroid_span; PAIR; CONJUNCT1 matroid_tybij]);; + +let MATROID_INDEPENDENT_SUBMATROID = prove + (`!(m:A matroid) s b. + s SUBSET matroid_set m + ==> (matroid_independent (submatroid m s) b <=> + b SUBSET matroid_span m s /\ matroid_independent m b)`, + SIMP_TAC[matroid_independent; SUBMATROID_SUBSET] THEN + MESON_TAC[MATROID_SPAN_SUBSET; SUBSET_TRANS]);; + +let MATROID_SPANNING_SUBMATROID = prove + (`!(m:A matroid) s b. + s SUBSET matroid_set m + ==> (matroid_spanning (submatroid m s) b <=> + b SUBSET matroid_span m s /\ matroid_span m b = matroid_span m s)`, + SIMP_TAC[matroid_spanning; SUBMATROID_SUBSET]);; + +let MATROID_SPANNING_SUBMATROID_SELF = prove + (`!(m:A matroid) s. + s SUBSET matroid_set m ==> matroid_spanning (submatroid m s) s`, + SIMP_TAC[MATROID_SPANNING_SUBMATROID; MATROID_SPAN_SUPERSET]);; + +let MATROID_BASIS_SUBMATROID = prove + (`!(m:A matroid) s b. + s SUBSET matroid_set m + ==> (matroid_basis (submatroid m s) b <=> + b SUBSET matroid_span m s /\ + matroid_independent m b /\ + matroid_span m b = matroid_span m s)`, + REWRITE_TAC[matroid_basis] THEN + SIMP_TAC[MATROID_INDEPENDENT_SUBMATROID; MATROID_SPANNING_SUBMATROID] THEN + MESON_TAC[]);; + +let MATROID_SUBSET_CONTAINS_BASIS = prove + (`!(m:A matroid) s. + s SUBSET matroid_set m + ==> ?b. b SUBSET s /\ + matroid_independent m b /\ + matroid_span m b = matroid_span m s`, + REPEAT STRIP_TAC THEN + FIRST_ASSUM(MP_TAC o MATCH_MP MATROID_SPANNING_SUBMATROID_SELF) THEN + DISCH_THEN(MP_TAC o MATCH_MP MATROID_SPANNING_CONTAINS_BASIS) THEN + ASM_SIMP_TAC[MATROID_BASIS_SUBMATROID] THEN MESON_TAC[]);; + +let MATROID_STEINITZ_EXCHANGE_FINITE = prove + (`!(m:A matroid) s t. + FINITE t /\ t SUBSET matroid_set m /\ + matroid_independent m s /\ s SUBSET matroid_span m t + ==> ?t'. t' HAS_SIZE (CARD t) /\ + s SUBSET t' /\ + t' SUBSET (s UNION t) /\ + matroid_span m t' = matroid_span m t`, + REPEAT STRIP_TAC THEN + MP_TAC(ISPECL [`submatroid m (t:A->bool)`; `s:A->bool`; `t:A->bool`] + MATROID_INTERMEDIATE_BASIS) THEN + ASM_SIMP_TAC[MATROID_INDEPENDENT_SUBMATROID; SUBMATROID; matroid_basis; + MATROID_SPANNING_SUBMATROID; MATROID_SPAN_SUPERSET] THEN + DISCH_THEN(X_CHOOSE_THEN `b:A->bool` STRIP_ASSUME_TAC) THEN + MP_TAC(SPECL [`CARD(t:A->bool)`; `b:A->bool`; `s UNION t:A->bool`] + CHOOSE_SUBSET_BETWEEN) THEN + ASM_SIMP_TAC[CARD_SUBSET; SUBSET_UNION] THEN ANTS_TAC THENL + [ASM_MESON_TAC[MATROID_INDEPENDENT_CARD_LE_SPAN_FINITE]; + MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `u:A->bool` THEN STRIP_TAC] THEN + ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN + MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL + [MP_TAC(ISPECL [`m:A matroid`; `s:A->bool`; `t:A->bool`] + MATROID_SPAN_UNION_EQ) THEN + ASM_SIMP_TAC[MATROID_INDEPENDENT_IMP_SUBSET] THEN + DISCH_THEN(SUBST1_TAC o SYM); + FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [SYM th])] THEN + MATCH_MP_TAC MATROID_SPAN_MONO THEN ASM SET_TAC[MATROID_SPAN_SUBSET]);; + +let MATROID_STEINITZ_EXCHANGE_ALT = prove + (`!(m:A matroid) s t. + FINITE t /\ t SUBSET matroid_set m /\ + matroid_independent m s /\ s SUBSET matroid_span m t + ==> ?t'. t' SUBSET t /\ CARD(t') + CARD s = CARD t /\ + matroid_span m (s UNION t') = matroid_span m t`, + REPEAT STRIP_TAC THEN + MP_TAC(ISPECL [`m:(A)matroid`; `s:A->bool`;`t:A->bool`] + MATROID_STEINITZ_EXCHANGE) THEN + ANTS_TAC THENL + [ASM_MESON_TAC[MATROID_INDEPENDENT_CARD_LE_SPAN_FINITE]; + DISCH_THEN(X_CHOOSE_THEN `u:A->bool` STRIP_ASSUME_TAC)] THEN + EXISTS_TAC `t DIFF u:A->bool` THEN ONCE_REWRITE_TAC[UNION_COMM] THEN + RULE_ASSUM_TAC(REWRITE_RULE[HAS_SIZE]) THEN + ASM_SIMP_TAC[SUBSET_DIFF; CARD_DIFF; FINITE_DIFF] THEN + MATCH_MP_TAC SUB_ADD THEN ASM_MESON_TAC[CARD_SUBSET]);; + +(* ------------------------------------------------------------------------- *) +(* Finite-dimensionality and dimension, both of whole matroid and a subset. *) +(* ------------------------------------------------------------------------- *) + +let matroid_finite_dimensional = define + `matroid_finite_dimensional (m:A matroid) <=> + ?b. FINITE b /\ matroid_spanning m b`;; + +let matroid_dimension = define + `matroid_dimension (m:A matroid) = + @n. !b. matroid_basis m b ==> b HAS_SIZE n`;; + +let matroid_finite_dim = define + `matroid_finite_dim (m:A matroid) s <=> + s SUBSET matroid_set m /\ + matroid_finite_dimensional(submatroid m s)`;; + +let matroid_dim = define + `matroid_dim (m:A matroid) s = matroid_dimension(submatroid m s)`;; + +let MATROID_FINITE_DIM_IMP_SUBSET = prove + (`!(m:A matroid) s. matroid_finite_dim m s ==> s SUBSET matroid_set m`, + SIMP_TAC[matroid_finite_dim]);; + +let MATROID_FINITE_DIM_SET = prove + (`!(m:A matroid). + matroid_finite_dim m (matroid_set m) = matroid_finite_dimensional m`, + REWRITE_TAC[matroid_finite_dim; SUBMATROID_SET; SUBSET_REFL]);; + +let MATROID_DIM_SET = prove + (`!(m:A matroid). + matroid_dim m (matroid_set m) = matroid_dimension m`, + REWRITE_TAC[matroid_dim; SUBMATROID_SET]);; + +let MATROID_FINITE_DIM_SPAN_EQ = prove + (`!(m:A matroid) s. + matroid_finite_dim m s <=> + s SUBSET matroid_set m /\ matroid_finite_dim m (matroid_span m s)`, + REWRITE_TAC[matroid_finite_dim] THEN + MESON_TAC[SUBMATROID_SPAN; MATROID_SPAN_SUBSET]);; + +let MATROID_FINITE_DIM_SPAN = prove + (`!(m:A matroid) s. + s SUBSET matroid_set m + ==> (matroid_finite_dim m (matroid_span m s) <=> + matroid_finite_dim m s)`, + MESON_TAC[MATROID_FINITE_DIM_SPAN_EQ]);; + +let MATROID_DIM_SPAN = prove + (`!(m:A matroid) s. + s SUBSET matroid_set m + ==> matroid_dim m (matroid_span m s) = matroid_dim m s`, + SIMP_TAC[matroid_dim; SUBMATROID_SPAN]);; + +let MATROID_FINITE_DIMENSIONAL = prove + (`!(m:A matroid). + matroid_finite_dimensional m <=> + ?b. FINITE b /\ + b SUBSET matroid_set m /\ + matroid_set m SUBSET matroid_span m b`, + REWRITE_TAC[matroid_finite_dimensional; matroid_spanning] THEN + MESON_TAC[MATROID_SPAN_EQ_SET]);; + +let MATROID_FINITE_DIMENSIONAL_BASIS = prove + (`!(m:A matroid). + matroid_finite_dimensional m <=> + ?b. FINITE b /\ matroid_basis m b`, + REWRITE_TAC[matroid_finite_dimensional] THEN + MESON_TAC[MATROID_SPANNING_CONTAINS_BASIS; FINITE_SUBSET; + matroid_basis]);; + +let MATROID_FINITE_DIMENSIONAL_CONTAINS_BASIS = prove + (`!(m:A matroid) s. + matroid_finite_dimensional m /\ matroid_spanning m s + ==> ?b. FINITE b /\ b SUBSET s /\ matroid_basis m b`, + REPEAT STRIP_TAC THEN + FIRST_ASSUM(MP_TAC o MATCH_MP MATROID_SPANNING_CONTAINS_BASIS) THEN + RULE_ASSUM_TAC(REWRITE_RULE[MATROID_FINITE_DIMENSIONAL_BASIS]) THEN + ASM_MESON_TAC[MATROID_BASES_FINITE]);; + +let MATROID_FINITE_DIMENSIONAL_ANY = prove + (`!(m:A matroid) b. + matroid_basis m b + ==> (matroid_finite_dimensional (m:A matroid) <=> FINITE b)`, + MESON_TAC[MATROID_FINITE_DIMENSIONAL_BASIS; MATROID_BASES_FINITE; + MATROID_BASIS_EXISTS]);; + +let [MATROID_FINITE_DIM; MATROID_FINITE_DIM_SUBSET; MATROID_FINITE_DIM_BASIS] = + (CONJUNCTS o prove) + (`(!(m:A matroid) s. + matroid_finite_dim m s <=> + ?b. FINITE b /\ b SUBSET matroid_set m /\ s SUBSET matroid_span m b) /\ + (!(m:A matroid) s. + matroid_finite_dim m s <=> + s SUBSET matroid_set m /\ + ?b. FINITE b /\ b SUBSET s /\ s SUBSET matroid_span m b) /\ + (!(m:A matroid) s. + matroid_finite_dim m s <=> + s SUBSET matroid_set m /\ + ?b. FINITE b /\ + b SUBSET s /\ + matroid_independent m b /\ + matroid_span m b = matroid_span m s)`, + REWRITE_TAC[AND_FORALL_THM] THEN REPEAT GEN_TAC THEN + MATCH_MP_TAC(TAUT + `(s ==> r) /\ (r ==> p) /\ (p ==> q) /\ (q ==> s) + ==> (p <=> q) /\ (p <=> r) /\ (p <=> s)`) THEN + CONJ_TAC THENL [ASM SET_TAC[MATROID_SPAN_SUPERSET]; ALL_TAC] THEN + REWRITE_TAC[ONCE_REWRITE_RULE[TAUT `p /\ q <=> ~(p ==> ~q)`] + matroid_finite_dim] THEN + SIMP_TAC[matroid_finite_dimensional; SUBMATROID_SUBSET; + MATROID_SPANNING_SUBMATROID] THEN + REWRITE_TAC[NOT_IMP] THEN REPEAT CONJ_TAC THENL + [REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ] THEN + MESON_TAC[MATROID_SPAN_MINIMAL; MATROID_SPAN_SUPERSET; SUBSET_TRANS]; + MESON_TAC[SUBSET_MATROID_SPAN; MATROID_SPAN_SUBSET; SUBSET]; + DISCH_THEN(X_CHOOSE_THEN `c:A->bool` STRIP_ASSUME_TAC)] THEN + MATCH_MP_TAC(TAUT `p /\ (p ==> q) ==> p /\ q`) THEN CONJ_TAC THENL + [ASM SET_TAC[MATROID_SPAN_SUBSET]; DISCH_TAC] THEN + FIRST_ASSUM(MP_TAC o MATCH_MP MATROID_SUBSET_CONTAINS_BASIS) THEN + MATCH_MP_TAC MONO_EXISTS THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN + MP_TAC(ISPECL [`m:A matroid`; `b:A->bool`; `c:A->bool`] + MATROID_INDEPENDENT_CARD_LE_SPAN_FINITE) THEN + ASM SET_TAC[MATROID_SPAN_SUBSET; MATROID_SPAN_SUPERSET]);; + +let MATROID_FINITE_DIMENSIONAL_DIM = prove + (`!(m:A matroid) s. + matroid_finite_dimensional m /\ s SUBSET matroid_set m + ==> matroid_finite_dim m s`, + REWRITE_TAC[matroid_finite_dimensional; matroid_spanning; + MATROID_FINITE_DIM] THEN + SET_TAC[]);; + +let FINITE_IMP_MATROID_FINITE_DIM = prove + (`!(m:A matroid) s. + FINITE s /\ s SUBSET matroid_set m ==> matroid_finite_dim m s`, + REWRITE_TAC[MATROID_FINITE_DIM] THEN MESON_TAC[MATROID_SPAN_SUPERSET]);; + +let MATROID_FINITE_DIM_FINITE = prove + (`!m s:A->bool. + FINITE s ==> (matroid_finite_dim m s <=> s SUBSET matroid_set m)`, + MESON_TAC[matroid_finite_dim; FINITE_IMP_MATROID_FINITE_DIM]);; + +let MATROID_FINITE_DIM_EMPTY = prove + (`!m:A matroid. matroid_finite_dim m {}`, + SIMP_TAC[FINITE_IMP_MATROID_FINITE_DIM; EMPTY_SUBSET; FINITE_EMPTY]);; + +let MATROID_FINITE_DIM_MONO = prove + (`!(m:A matroid) s t. + matroid_finite_dim m t /\ s SUBSET t ==> matroid_finite_dim m s`, + REWRITE_TAC[MATROID_FINITE_DIM] THEN SET_TAC[]);; + +let MATROID_FINITE_DIM_UNION = prove + (`!m s t:A->bool. + matroid_finite_dim m (s UNION t) <=> + matroid_finite_dim m s /\ matroid_finite_dim m t`, + REPEAT GEN_TAC THEN EQ_TAC THENL + [MESON_TAC[MATROID_FINITE_DIM_MONO; SUBSET_UNION]; + REWRITE_TAC[MATROID_FINITE_DIM]] THEN + DISCH_THEN(CONJUNCTS_THEN2 + (X_CHOOSE_THEN `b:A->bool` STRIP_ASSUME_TAC) + (X_CHOOSE_THEN `c:A->bool` STRIP_ASSUME_TAC)) THEN + EXISTS_TAC `b UNION c:A->bool` THEN + ASM_REWRITE_TAC[UNION_SUBSET; FINITE_UNION] THEN CONJ_TAC THEN + ASM_MESON_TAC[MATROID_SPAN_MONO; UNION_SUBSET; SUBSET_TRANS; SUBSET_UNION]);; + +let MATROID_FINITE_DIM_INSERT = prove + (`!m s x:A. + matroid_finite_dim m (x INSERT s) <=> + x IN matroid_set m /\ matroid_finite_dim m s`, + REPEAT GEN_TAC THEN + ONCE_REWRITE_TAC[SET_RULE`a INSERT s = {a} UNION s`] THEN + SIMP_TAC[MATROID_FINITE_DIM_UNION; MATROID_FINITE_DIM_FINITE; FINITE_SING; + SING_SUBSET]);; + +let MATROID_DIMENSION_ALT = prove + (`!m:A matroid. + matroid_dimension m = @n. ?b. matroid_basis m b /\ b HAS_SIZE n`, + GEN_TAC THEN REWRITE_TAC[matroid_dimension] THEN + AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN + MESON_TAC[MATROID_BASES_SIZE; MATROID_BASIS_EXISTS]);; + +let MATROID_DIM_BASIS = prove + (`!(m:A matroid) s. + s SUBSET matroid_set m + ==> (matroid_dim m s = + @n. ?b. b SUBSET s /\ + matroid_independent m b /\ + matroid_span m b = matroid_span m s /\ + b HAS_SIZE n)`, + REWRITE_TAC[matroid_dim; MATROID_DIMENSION_ALT] THEN + SIMP_TAC[MATROID_BASIS_SUBMATROID] THEN + REPEAT STRIP_TAC THEN AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN + FIRST_ASSUM(MP_TAC o MATCH_MP MATROID_SUBSET_CONTAINS_BASIS) THEN + ASM_MESON_TAC[MATROID_EQ_SPANS_SIZE; MATROID_SPAN_SUPERSET; SUBSET_TRANS]);; + +let MATROID_DIM_ALT = prove + (`!(m:A matroid) s. + s SUBSET matroid_set m + ==> (matroid_dim m s = + @n. ?b. b SUBSET s /\ + matroid_independent m b /\ + s SUBSET matroid_span m b /\ + b HAS_SIZE n)`, + REPEAT STRIP_TAC THEN ASM_SIMP_TAC[MATROID_DIM_BASIS] THEN + REPLICATE_TAC 2 (AP_TERM_TAC THEN ABS_TAC) THEN + ASM_MESON_TAC[MATROID_SPAN_EQ; MATROID_SPAN_MINIMAL; SUBSET_TRANS]);; + +let MATROID_DIMENSION_UNIQUE = prove + (`!(m:A matroid) b n. + matroid_basis m b /\ b HAS_SIZE n ==> matroid_dimension m = n`, + REWRITE_TAC[matroid_dimension] THEN + MESON_TAC[MATROID_BASES_SIZE; HAS_SIZE]);; + +let MATROID_DIMENSION_EQ_CARD = prove + (`!(m:A matroid) b. + matroid_basis m b /\ FINITE b ==> matroid_dimension m = CARD b`, + MESON_TAC[MATROID_DIMENSION_UNIQUE; HAS_SIZE]);; + +let MATROID_DIM_UNIQUE_ALT = prove + (`!(m:A matroid) s b n. + s SUBSET matroid_set m /\ b SUBSET matroid_set m /\ b HAS_SIZE n /\ + matroid_independent m b /\ matroid_span m b = matroid_span m s + ==> matroid_dim m s = n`, + REPEAT STRIP_TAC THEN REWRITE_TAC[matroid_dim] THEN + MATCH_MP_TAC MATROID_DIMENSION_UNIQUE THEN EXISTS_TAC `b:A->bool` THEN + SUBGOAL_THEN `(s:A->bool) SUBSET matroid_set m` ASSUME_TAC THENL + [ASM_MESON_TAC[MATROID_SPAN_SUBSET; SUBSET_TRANS]; + ASM_SIMP_TAC[MATROID_BASIS_SUBMATROID]] THEN + ASM_MESON_TAC[MATROID_SPAN_SUPERSET]);; + +let MATROID_DIM_UNIQUE = prove + (`!(m:A matroid) s b n. + b SUBSET s /\ b HAS_SIZE n /\ + matroid_independent m b /\ s SUBSET matroid_span m b + ==> matroid_dim m s = n`, + REPEAT STRIP_TAC THEN MATCH_MP_TAC MATROID_DIM_UNIQUE_ALT THEN + EXISTS_TAC `b:A->bool` THEN ASM_REWRITE_TAC[] THEN + FIRST_ASSUM(ASSUME_TAC o MATCH_MP MATROID_INDEPENDENT_IMP_SUBSET) THEN + ASM_MESON_TAC[MATROID_SPAN_EQ; MATROID_SPAN_SUBSET; SUBSET_TRANS]);; + +let MATROID_SPAN_DIM_EQ = prove + (`!m s t:A->bool. + s SUBSET matroid_set m /\ + t SUBSET matroid_set m /\ + matroid_span m s = matroid_span m t + ==> matroid_dim m s = matroid_dim m t`, + MESON_TAC[MATROID_DIM_SPAN]);; + +let MATROID_SPAN_INSERT_REFL = prove + (`!m s x:A. + s SUBSET matroid_set m /\ x IN matroid_span m s + ==> matroid_span m (x INSERT s) = matroid_span m s`, + MESON_TAC[MATROID_SPAN_INSERT_EQ; MATROID_SPAN_SUBSET; SUBSET]);; + +let MATROID_BASIS_EXISTS_DIMENSION = prove + (`!m:A matroid. + matroid_finite_dimensional m <=> + ?b. b HAS_SIZE matroid_dimension m /\ matroid_basis m b`, + REWRITE_TAC[MATROID_FINITE_DIMENSIONAL_BASIS; HAS_SIZE] THEN + MESON_TAC[MATROID_DIMENSION_UNIQUE; HAS_SIZE]);; + +let MATROID_BASIS_EXISTS_DIM = prove + (`!m s:A->bool. + matroid_finite_dim m s <=> + s SUBSET matroid_set m /\ + ?b. b HAS_SIZE matroid_dim m s /\ + b SUBSET matroid_span m s /\ + matroid_independent m b /\ + matroid_span m b = matroid_span m s`, + REPEAT GEN_TAC THEN REWRITE_TAC[matroid_finite_dim] THEN + ASM_CASES_TAC `(s:A->bool) SUBSET matroid_set m` THEN ASM_REWRITE_TAC[] THEN + ASM_SIMP_TAC[MATROID_BASIS_EXISTS_DIMENSION; MATROID_BASIS_SUBMATROID] THEN + MESON_TAC[matroid_dim]);; + +let MATROID_CONTAINS_BASIS_DIM = prove + (`!m s:A->bool. + matroid_finite_dim m s <=> + s SUBSET matroid_set m /\ + ?b. b HAS_SIZE matroid_dim m s /\ + b SUBSET s /\ + matroid_independent m b /\ + matroid_span m b = matroid_span m s`, + REPEAT GEN_TAC THEN REWRITE_TAC[MATROID_FINITE_DIM_BASIS; HAS_SIZE] THEN + ASM_CASES_TAC `(s:A->bool) SUBSET matroid_set m` THEN ASM_REWRITE_TAC[] THEN + ASM_MESON_TAC[MATROID_DIM_UNIQUE_ALT; HAS_SIZE; SUBSET]);; + +let MATROID_DIM_EQ_CARD_GEN = prove + (`!(m:A matroid) s b. + b SUBSET s /\ FINITE b /\ + matroid_independent m b /\ s SUBSET matroid_span m b + ==> matroid_dim m s = CARD b`, + MESON_TAC[MATROID_DIM_UNIQUE; HAS_SIZE]);; + +let MATROID_DIM_EQ_CARD = prove + (`!(m:A matroid) b. + FINITE b /\ matroid_independent m b + ==> matroid_dim m b = CARD b`, + MESON_TAC[MATROID_DIM_EQ_CARD_GEN; MATROID_INDEPENDENT_IMP_SUBSET; + SUBSET_REFL; MATROID_SPAN_SUPERSET]);; + +let MATROID_DIMENSION_LE = prove + (`!(m:A matroid) b n. + b SUBSET matroid_set m /\ matroid_set m SUBSET matroid_span m b /\ + FINITE b /\ CARD b <= n + ==> matroid_dimension m <= n`, + REPEAT STRIP_TAC THEN + FIRST_ASSUM(MP_TAC o MATCH_MP MATROID_SUBSET_CONTAINS_BASIS) THEN + DISCH_THEN(X_CHOOSE_THEN `c:A->bool` STRIP_ASSUME_TAC) THEN + TRANS_TAC LE_TRANS `CARD(c:A->bool)` THEN CONJ_TAC THENL + [MATCH_MP_TAC EQ_IMP_LE; ASM_MESON_TAC[CARD_SUBSET; LE_TRANS]] THEN + MATCH_MP_TAC MATROID_DIMENSION_UNIQUE THEN + EXISTS_TAC `c:A->bool` THEN ASM_REWRITE_TAC[matroid_basis; HAS_SIZE] THEN + ASM_REWRITE_TAC[MATROID_SPANNING_ALT] THEN + ASM_MESON_TAC[FINITE_SUBSET; SUBSET_TRANS]);; + +let MATROID_DIMENSION_FINITE_LE = prove + (`!(m:A matroid) b n. + b SUBSET matroid_set m /\ matroid_set m SUBSET matroid_span m b /\ + FINITE b /\ CARD b <= n + ==> matroid_finite_dimensional m /\ matroid_dimension m <= n`, + MESON_TAC[MATROID_DIMENSION_LE; MATROID_FINITE_DIMENSIONAL]);; + +let MATROID_DIM_LE = prove + (`!(m:A matroid) s b n. + FINITE b /\ CARD b <= n /\ + b SUBSET matroid_set m /\ s SUBSET matroid_span m b + ==> matroid_dim m s <= n`, + REPEAT STRIP_TAC THEN + SUBGOAL_THEN `(s:A->bool) SUBSET matroid_set m` ASSUME_TAC THENL + [ASM_MESON_TAC[MATROID_SPAN_SUBSET; SUBSET_TRANS]; + FIRST_ASSUM(MP_TAC o MATCH_MP MATROID_SUBSET_CONTAINS_BASIS)] THEN + DISCH_THEN(X_CHOOSE_THEN `c:A->bool` STRIP_ASSUME_TAC) THEN + MP_TAC(ISPECL [`m:A matroid`; `c:A->bool`; `b:A->bool`] + MATROID_INDEPENDENT_CARD_LE_SPAN_FINITE) THEN + ANTS_TAC THENL [ASM SET_TAC[]; STRIP_TAC] THEN + MP_TAC(ISPECL [`m:A matroid`; `s:A->bool`; `c:A->bool`] + MATROID_DIM_EQ_CARD_GEN) THEN + ASM_SIMP_TAC[MATROID_SPAN_SUPERSET] THEN ASM_ARITH_TAC);; + +let MATROID_DIM_FINITE_LE = prove + (`!(m:A matroid) s b n. + FINITE b /\ CARD b <= n /\ + b SUBSET matroid_set m /\ s SUBSET matroid_span m b + ==> matroid_finite_dim m s /\ matroid_dim m s <= n`, + MESON_TAC[MATROID_DIM_LE; MATROID_FINITE_DIM]);; + +let MATROID_DIM_LE_CARD_GEN = prove + (`!(m:A matroid) s b. + FINITE b /\ + b SUBSET matroid_set m /\ s SUBSET matroid_span m b + ==> matroid_dim m s <= CARD b`, + MESON_TAC[MATROID_DIM_LE; LE_REFL; HAS_SIZE]);; + +let MATROID_DIM_LE_CARD = prove + (`!(m:A matroid) s. + FINITE s /\ s SUBSET matroid_set m ==> matroid_dim m s <= CARD s`, + MESON_TAC[MATROID_DIM_LE_CARD_GEN; MATROID_SPAN_SUPERSET]);; + +let MATROID_DIMENSION_GE_FINITE_CARD = prove + (`!(m:A matroid) b. + matroid_finite_dimensional m /\ + matroid_independent m b + ==> FINITE b /\ CARD b <= matroid_dimension m`, + ASM_MESON_TAC[MATROID_INDEPENDENT_CARD_LE_SPAN_FINITE; matroid_basis; + MATROID_FINITE_DIMENSIONAL_BASIS; matroid_spanning; + MATROID_INDEPENDENT_IMP_SUBSET; MATROID_DIMENSION_EQ_CARD]);; + +let MATROID_DIMENSION_GE = prove + (`!(m:A matroid) b n. + matroid_finite_dimensional m /\ + matroid_independent m b /\ + n <= CARD b + ==> n <= matroid_dimension m`, + MESON_TAC[MATROID_DIMENSION_GE_FINITE_CARD; LE_TRANS]);; + +let MATROID_DIMENSION_GE_CARD = prove + (`!(m:A matroid) b. + matroid_finite_dimensional m /\ matroid_independent m b + ==> CARD b <= matroid_dimension m`, + MESON_TAC[MATROID_DIMENSION_GE_FINITE_CARD]);; + +let MATROID_DIM_GE_FINITE_CARD = prove + (`!(m:A matroid) s b. + matroid_finite_dim m s /\ matroid_independent m b /\ b SUBSET s + ==> FINITE b /\ CARD b <= matroid_dim m s`, + REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[matroid_dim] THEN + MATCH_MP_TAC MATROID_DIMENSION_GE_FINITE_CARD THEN + ASM_MESON_TAC[matroid_finite_dim; MATROID_INDEPENDENT_SUBMATROID; + MATROID_SPAN_SUPERSET; SUBSET_TRANS]);; + +let MATROID_DIM_GE = prove + (`!(m:A matroid) s b n. + matroid_finite_dim m s /\ matroid_independent m b /\ + b SUBSET s /\ n <= CARD b + ==> n <= matroid_dim m s`, + MESON_TAC[MATROID_DIM_GE_FINITE_CARD; LE_TRANS]);; + +let MATROID_DIM_GE_CARD_GEN = prove + (`!(m:A matroid) s b. + matroid_finite_dim m s /\ matroid_independent m b /\ b SUBSET s + ==> CARD b <= matroid_dim m s`, + MESON_TAC[MATROID_DIM_GE_FINITE_CARD; LE_TRANS]);; + +let MATROID_DIM_GE_CARD = prove + (`!(m:A matroid) s. + matroid_finite_dim m s /\ matroid_independent m s + ==> CARD s <= matroid_dim m s`, + MESON_TAC[MATROID_DIM_GE_CARD_GEN; SUBSET_REFL]);; + +let FINITE_IMP_MATROID_FINITE_DIM_SPAN = prove + (`!(m:A matroid) s. + FINITE s /\ s SUBSET matroid_set m + ==> matroid_finite_dim m (matroid_span m s)`, + MESON_TAC[MATROID_FINITE_DIM_SPAN; FINITE_IMP_MATROID_FINITE_DIM]);; + +let MATROID_INDEPENDENT_IMP_FINITE = prove + (`!(m:A matroid) s. + matroid_finite_dim m s /\ matroid_independent m s + ==> FINITE s`, + MESON_TAC[MATROID_DIM_GE_FINITE_CARD; SUBSET_REFL]);; + +let MATROID_DIM_EQ_FINITE_CARD_EQ,MATROID_DIM_GE_FINITE_CARD_EQ = + (CONJ_PAIR o prove) + (`(!m s:A->bool. + s SUBSET matroid_set m /\ FINITE s /\ matroid_dim m s = CARD s <=> + matroid_finite_dim m s /\ matroid_independent m s) /\ + (!m s:A->bool. + s SUBSET matroid_set m /\ FINITE s /\ CARD s <= matroid_dim m s <=> + matroid_finite_dim m s /\ matroid_independent m s)`, + REWRITE_TAC[AND_FORALL_THM] THEN REPEAT GEN_TAC THEN + MATCH_MP_TAC(TAUT + `(p ==> q) /\ (r ==> p) /\ (q ==> r) ==> (p <=> r) /\ (q <=> r)`) THEN + SIMP_TAC[LE_REFL] THEN CONJ_TAC THENL + [MESON_TAC[MATROID_FINITE_DIM_IMP_SUBSET; MATROID_INDEPENDENT_IMP_FINITE; + SUBSET_REFL; MATROID_DIM_EQ_CARD]; + STRIP_TAC THEN ASM_SIMP_TAC[FINITE_IMP_MATROID_FINITE_DIM]] THEN + MP_TAC(ISPECL [`submatroid m (s:A->bool)`; `s:A->bool`] + MATROID_BASIS_EQ_MINIMAL_SPANNING) THEN + ASM_SIMP_TAC[MATROID_BASIS_SUBMATROID; MATROID_SPANNING_SUBMATROID; + MATROID_SPAN_SUPERSET] THEN + DISCH_THEN(K ALL_TAC) THEN X_GEN_TAC `t:A->bool` THEN REPEAT STRIP_TAC THEN + MP_TAC(ISPECL [`m:A matroid`; `s:A->bool`; `t:A->bool`] + MATROID_DIM_LE_CARD_GEN) THEN + ASM_MESON_TAC[MATROID_SPAN_SUPERSET; SUBSET; PSUBSET; FINITE_SUBSET; + CARD_PSUBSET; NOT_LT; LE_TRANS]);; + +let MATROID_DIM_EMPTY = prove + (`!m:A matroid. matroid_dim m {} = 0`, + GEN_TAC THEN MATCH_MP_TAC MATROID_DIM_UNIQUE THEN + EXISTS_TAC `{}:A->bool` THEN + REWRITE_TAC[MATROID_INDEPENDENT_EMPTY; HAS_SIZE; FINITE_RULES; CARD_CLAUSES; + EMPTY_SUBSET]);; + +let MATROID_DIM_INSERT = prove + (`!m s x:A. + matroid_finite_dim m s /\ x IN matroid_set m + ==> matroid_dim m (x INSERT s) = + if x IN matroid_span m s then matroid_dim m s + else matroid_dim m s + 1`, + REPEAT STRIP_TAC THEN + FIRST_ASSUM(ASSUME_TAC o MATCH_MP MATROID_FINITE_DIM_IMP_SUBSET) THEN + COND_CASES_TAC THENL + [ASM_MESON_TAC[MATROID_SPAN_INSERT_REFL; MATROID_SPAN_DIM_EQ; + INSERT_SUBSET; MATROID_SPAN_SUBSET; SUBSET]; + FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [MATROID_CONTAINS_BASIS_DIM])] THEN + ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM; HAS_SIZE] THEN + X_GEN_TAC `b:A->bool` THEN STRIP_TAC THEN + MATCH_MP_TAC MATROID_DIM_UNIQUE THEN EXISTS_TAC `(x:A) INSERT b` THEN + ASM_REWRITE_TAC[HAS_SIZE; FINITE_INSERT; MATROID_INDEPENDENT_INSERT] THEN + CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN + ASM_SIMP_TAC[CARD_CLAUSES; INSERT_SUBSET] THEN + COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL + [ASM_MESON_TAC[MATROID_SPAN_SUPERSET; SUBSET]; REWRITE_TAC[ADD1]] THEN + CONJ_TAC THENL + [MATCH_MP_TAC MATROID_SPAN_INC THEN ASM SET_TAC[]; ALL_TAC] THEN + TRANS_TAC SUBSET_TRANS `matroid_span m b:A->bool` THEN + CONJ_TAC THENL + [ASM_SIMP_TAC[MATROID_SPAN_SUPERSET]; + MATCH_MP_TAC MATROID_SPAN_MONO THEN ASM SET_TAC[]]);; + +let MATROID_DIM_SUBSET = prove + (`!m s t:A->bool. + s SUBSET t /\ matroid_finite_dim m t + ==> matroid_dim m s <= matroid_dim m t`, + REPEAT STRIP_TAC THEN + FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [MATROID_FINITE_DIM_BASIS]) THEN + DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC + (X_CHOOSE_THEN `b:A->bool` (STRIP_ASSUME_TAC o GSYM))) THEN + MP_TAC(ISPECL [`m:A matroid`; `s:A->bool`; `b:A->bool`; `CARD(b:A->bool)`] + MATROID_DIM_FINITE_LE) THEN + MP_TAC(ISPECL [`m:A matroid`; `b:A->bool`] MATROID_DIM_EQ_CARD) THEN + MP_TAC(ISPECL [`m:A matroid`; `t:A->bool`] MATROID_DIM_SPAN) THEN + ASM_REWRITE_TAC[LE_REFL] THEN + ASM SET_TAC[MATROID_DIM_SPAN; MATROID_SPAN_SUPERSET]);; + +let MATROID_DIM_SUBSET_ALT = prove + (`!m s t:A->bool. + s SUBSET matroid_span m t /\ matroid_finite_dim m t + ==> matroid_dim m s <= matroid_dim m t`, + MESON_TAC[MATROID_DIM_SUBSET; MATROID_FINITE_DIM_SPAN; MATROID_DIM_SPAN; + MATROID_FINITE_DIM_IMP_SUBSET]);; + +let MATROID_DIM_SPAN_SUBSET = prove + (`!m s t:A->bool. + s SUBSET matroid_set m /\ + matroid_span m s SUBSET matroid_span m t /\ + matroid_finite_dim m t + ==> matroid_dim m s <= matroid_dim m t`, + MESON_TAC[MATROID_SPAN_MINIMAL; MATROID_DIM_SPAN; MATROID_DIM_SUBSET_ALT; + MATROID_FINITE_DIM_IMP_SUBSET]);; + +let MATROID_DIM_SPAN_PSUBSET = prove + (`!m s t:A->bool. + s SUBSET matroid_set m /\ + matroid_span m s PSUBSET matroid_span m t /\ + matroid_finite_dim m t + ==> matroid_dim m s < matroid_dim m t`, + REPEAT STRIP_TAC THEN + FIRST_ASSUM(ASSUME_TAC o MATCH_MP MATROID_FINITE_DIM_IMP_SUBSET) THEN + FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [PSUBSET_ALT]) THEN + DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC + (X_CHOOSE_THEN `a:A` STRIP_ASSUME_TAC)) THEN + SUBGOAL_THEN `matroid_finite_dim m (s:A->bool)` ASSUME_TAC THENL + [ASM_MESON_TAC[MATROID_FINITE_DIM_SPAN; MATROID_FINITE_DIM_MONO]; + ALL_TAC] THEN + ASM_CASES_TAC `(a:A) IN matroid_set m` THENL + [ALL_TAC; ASM_MESON_TAC[MATROID_SPAN_SUBSET; SUBSET]] THEN + TRANS_TAC LTE_TRANS `matroid_dim m ((a:A) INSERT s)` THEN CONJ_TAC THENL + [ASM_SIMP_TAC[MATROID_DIM_INSERT; ARITH_RULE `n < n + 1`]; ALL_TAC] THEN + TRANS_TAC LE_TRANS `matroid_dim m (matroid_span m t:A->bool)` THEN + CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[MATROID_DIM_SPAN; LE_REFL]] THEN + MATCH_MP_TAC MATROID_DIM_SUBSET THEN + ASM_SIMP_TAC[MATROID_FINITE_DIM_SPAN; INSERT_SUBSET] THEN + ASM_MESON_TAC[MATROID_SPAN_SUPERSET; SUBSET_TRANS]);; + +let MATROID_DIM_SPAN_EQ_GEN = prove + (`!m s t:A->bool. + s SUBSET matroid_set m /\ matroid_finite_dim m t /\ + matroid_span m s SUBSET matroid_span m t /\ + matroid_dim m t <= matroid_dim m s + ==> matroid_span m s = matroid_span m t`, + MESON_TAC[MATROID_DIM_SPAN_PSUBSET; PSUBSET; NOT_LT]);; + +let MATROID_DIM_SPAN_EQ = prove + (`!m s t:A->bool. + s SUBSET matroid_set m /\ matroid_finite_dim m t /\ + matroid_span m s SUBSET matroid_span m t /\ + matroid_dim m s = matroid_dim m t + ==> matroid_span m s = matroid_span m t`, + MESON_TAC[MATROID_DIM_SPAN_PSUBSET; PSUBSET; LT_REFL]);; + +let MATROID_DIM_EQ_SPAN = prove + (`!m s t:A->bool. + matroid_finite_dim m t /\ s SUBSET t /\ matroid_dim m t <= matroid_dim m s + ==> matroid_span m s = matroid_span m t`, + REPEAT STRIP_TAC THEN MATCH_MP_TAC MATROID_DIM_SPAN_EQ_GEN THEN + ASM_MESON_TAC[MATROID_SPAN_MONO; MATROID_FINITE_DIM_IMP_SUBSET; SUBSET]);; + +let MATROID_CHOOSE_SUBSET = prove + (`!(m:A matroid) s n. + s SUBSET matroid_set m /\ + (matroid_finite_dim m s ==> n <= matroid_dim m s) + ==> ?t. t SUBSET s /\ matroid_independent m t /\ t HAS_SIZE n`, + REPEAT STRIP_TAC THEN + FIRST_ASSUM(X_CHOOSE_THEN `b:A->bool` STRIP_ASSUME_TAC o MATCH_MP + MATROID_SUBSET_CONTAINS_BASIS) THEN + MP_TAC(ISPECL [`n:num`; `b:A->bool`] CHOOSE_SUBSET_STRONG) THEN ANTS_TAC + THENL [DISCH_TAC; ASM_MESON_TAC[MATROID_INDEPENDENT_MONO; SUBSET]] THEN + ASM_SIMP_TAC[GSYM MATROID_DIM_EQ_CARD] THEN + ASM_MESON_TAC[MATROID_FINITE_DIM_BASIS; MATROID_SPAN_DIM_EQ; SUBSET]);; + +let MATROID_CHOOSE_SUBSPACE = prove + (`!(m:A matroid) s n. + s SUBSET matroid_set m /\ + (matroid_finite_dim m s ==> n <= matroid_dim m s) + ==> ?t. matroid_subspace m t /\ t SUBSET matroid_span m s /\ + matroid_finite_dim m t /\ matroid_dim m t = n`, + REPEAT GEN_TAC THEN DISCH_TAC THEN + FIRST_ASSUM(X_CHOOSE_THEN `b:A->bool` STRIP_ASSUME_TAC o + REWRITE_RULE[HAS_SIZE] o MATCH_MP MATROID_CHOOSE_SUBSET) THEN + EXISTS_TAC `matroid_span m b:A->bool` THEN + SUBGOAL_THEN `(b:A->bool) SUBSET matroid_set m` ASSUME_TAC THENL + [ASM SET_TAC[]; ALL_TAC] THEN + ASM_SIMP_TAC[MATROID_SUBSPACE_SPAN; MATROID_SPAN_MONO; MATROID_DIM_EQ_CARD; + MATROID_FINITE_DIM_SPAN; MATROID_DIM_SPAN; FINITE_IMP_MATROID_FINITE_DIM]);; + +let MATROID_LOWDIM_EXPAND_BASIS = prove + (`!m (s:A->bool) n. + matroid_finite_dim m s /\ matroid_dim m s <= n /\ + (matroid_finite_dimensional m ==> n <= matroid_dimension m) + ==> ?b. b HAS_SIZE n /\ matroid_independent m b /\ + matroid_span m s SUBSET matroid_span m b`, + REPEAT STRIP_TAC THEN + FIRST_ASSUM(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC o + GEN_REWRITE_RULE I [MATROID_FINITE_DIM_BASIS]) THEN + DISCH_THEN(X_CHOOSE_THEN `b:A->bool` STRIP_ASSUME_TAC) THEN + FIRST_ASSUM(X_CHOOSE_THEN `d:A->bool` STRIP_ASSUME_TAC o + MATCH_MP MATROID_INDEPENDENT_EXTENDS_TO_BASIS) THEN + MP_TAC(ISPECL [`n:num`; `b:A->bool`; `d:A->bool`] + CHOOSE_SUBSET_BETWEEN) THEN + ASM_REWRITE_TAC[] THEN ANTS_TAC THENL + [CONJ_TAC THENL + [ASM_MESON_TAC[MATROID_DIM_EQ_CARD; MATROID_SPAN_DIM_EQ; SUBSET]; + DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o check (is_imp o concl))] THEN + ANTS_TAC THENL + [ASM_MESON_TAC[matroid_finite_dimensional; matroid_basis]; + ASM_MESON_TAC[MATROID_DIMENSION_UNIQUE; HAS_SIZE]]; + MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `c:A->bool` THEN + STRIP_TAC THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL + [ASM_MESON_TAC[matroid_basis; MATROID_INDEPENDENT_MONO]; + ASM_MESON_TAC[MATROID_SPAN_MONO; SUBSET; MATROID_BASIS_IMP_SUBSET]]]);; + +let MATROID_LOWDIM_EXPAND_DIMENSION = prove + (`!m (s:A->bool) n. + matroid_finite_dim m s /\ matroid_dim m s <= n /\ + (matroid_finite_dimensional m ==> n <= matroid_dimension m) + ==> ?t. matroid_finite_dim m t /\ matroid_dim m t = n /\ + matroid_span m s SUBSET matroid_span m t`, + REPEAT GEN_TAC THEN DISCH_TAC THEN + FIRST_ASSUM(MP_TAC o MATCH_MP MATROID_LOWDIM_EXPAND_BASIS) THEN + MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `t:A->bool` THEN + REWRITE_TAC[HAS_SIZE] THEN STRIP_TAC THEN + ASM_SIMP_TAC[MATROID_DIM_EQ_CARD; FINITE_IMP_MATROID_FINITE_DIM; + MATROID_INDEPENDENT_IMP_SUBSET]);; diff --git a/Library/words.ml b/Library/words.ml index 58d8c6a3..95b2b9db 100644 --- a/Library/words.ml +++ b/Library/words.ml @@ -4431,6 +4431,22 @@ let WORD_SUBWORD_DUPLICATE = prove MATCH_MP_TAC MOD_UNIQ THEN EXISTS_TAC `pos DIV dimindex(:M)` THEN ASM_ARITH_TAC);; +let WORD_SUBWORD_DUPLICATE_DUPLICATE = prove + (`!x pos len. + pos MOD dimindex(:M) = 0 /\ dimindex(:P) <= len /\ + pos + len <= dimindex(:N) + ==> word_subword ((word_duplicate:M word->N word) x) (pos,len):P word = + word_duplicate x`, + REPEAT STRIP_TAC THEN + REWRITE_TAC[WORD_EQ_BITS_ALT; BIT_WORD_SUBWORD; BIT_WORD_DUPLICATE] THEN + X_GEN_TAC `i:num` THEN DISCH_TAC THEN + ASM_REWRITE_TAC[ARITH_RULE `i < MIN m n <=> i < m /\ i < n`] THEN + REWRITE_TAC[CONJ_ASSOC] THEN + MATCH_MP_TAC(TAUT `p /\ (q <=> r) ==> (p /\ q <=> r)`) THEN + CONJ_TAC THENL [ASM_ARITH_TAC; AP_THM_TAC THEN AP_TERM_TAC] THEN + ONCE_REWRITE_TAC[GSYM MOD_ADD_MOD] THEN + ASM_REWRITE_TAC[ADD_CLAUSES; MOD_MOD_REFL]);; + let VAL_WORD_DUPLICATE = prove (`!x k. dimindex(:N) <= k * dimindex(:M) ==> val((word_duplicate:M word->N word) x) = @@ -4500,13 +4516,16 @@ let WORD_SIMPLE_SUBWORD_CONV = let dimarith_rule th = MP th (EQT_ELIM(dimarith_conv(lhand(concl th)))) and post_rule = - CONV_RULE(RAND_CONV(RAND_CONV(BINOP_CONV dimarith_conv))) in + CONV_RULE(RAND_CONV(RAND_CONV(BINOP_CONV dimarith_conv))) + and triv_rule = + GEN_REWRITE_RULE (RAND_CONV o TRY_CONV) [WORD_DUPLICATE_REFL] in let [rules_join; rules_insert; rules_subword; rules_duplicate; - [rule_trivial]] = + [rule_duplicate]; [rule_trivial]] = map (map (PART_MATCH (lhand o rand))) [[WORD_SUBWORD_JOIN_LOWER; WORD_SUBWORD_JOIN_UPPER]; [WORD_SUBWORD_INSERT_OUTER; WORD_SUBWORD_INSERT_INNER]; [WORD_SUBWORD_SUBWORD]; [WORD_SUBWORD_DUPLICATE]; + [WORD_SUBWORD_DUPLICATE_DUPLICATE]; [WORD_SUBWORD_TRIVIAL]] in fun tm -> match tm with @@ -4521,7 +4540,9 @@ let WORD_SIMPLE_SUBWORD_CONV = | Comb(Comb(Const("word_subword",_),_),_) -> post_rule(tryfind (fun f -> dimarith_rule(f tm)) rules_subword) | Comb(Const("word_duplicate",_),_) -> - post_rule(tryfind (fun f -> dimarith_rule(f tm)) rules_duplicate) + (try triv_rule(dimarith_rule(rule_duplicate tm)) + with Failure _ -> + post_rule(tryfind (fun f -> dimarith_rule(f tm)) rules_duplicate)) | _ -> dimarith_rule(rule_trivial tm)) | _ -> failwith "WORD_SIMPLE_SUBWORD_CONV";; diff --git a/Multivariate/complex_database.ml b/Multivariate/complex_database.ml index 9d1f9582..77a0ad79 100644 --- a/Multivariate/complex_database.ml +++ b/Multivariate/complex_database.ml @@ -1091,6 +1091,8 @@ theorems := "BILINEAR_EQ_STDBASIS",BILINEAR_EQ_STDBASIS; "BILINEAR_GEOM",BILINEAR_GEOM; "BILINEAR_INNER",BILINEAR_INNER; +"BILINEAR_IN_AFFINE_HULL",BILINEAR_IN_AFFINE_HULL; +"BILINEAR_IN_CONVEX_HULL",BILINEAR_IN_CONVEX_HULL; "BILINEAR_LADD",BILINEAR_LADD; "BILINEAR_LIFT_MUL",BILINEAR_LIFT_MUL; "BILINEAR_LMUL",BILINEAR_LMUL; @@ -5440,6 +5442,7 @@ theorems := "DIVIDES_DIV_MULT",DIVIDES_DIV_MULT; "DIVIDES_DIV_NOT",DIVIDES_DIV_NOT; "DIVIDES_DIV_SELF",DIVIDES_DIV_SELF; +"DIVIDES_EQ_ZERO",DIVIDES_EQ_ZERO; "DIVIDES_EXP",DIVIDES_EXP; "DIVIDES_EXP2",DIVIDES_EXP2; "DIVIDES_EXP2_EQ",DIVIDES_EXP2_EQ; @@ -5831,6 +5834,7 @@ theorems := "EQ_TRANS",EQ_TRANS; "EQ_UNIV",EQ_UNIV; "ETA_AX",ETA_AX; +"ETA_ONE",ETA_ONE; "EUCLID",EUCLID; "EUCLIDEANREAL_CLOSURE_OF_HALFSPACE_GE",EUCLIDEANREAL_CLOSURE_OF_HALFSPACE_GE; "EUCLIDEANREAL_CLOSURE_OF_HALFSPACE_GT",EUCLIDEANREAL_CLOSURE_OF_HALFSPACE_GT; @@ -5851,8 +5855,17 @@ theorems := "EUCLIDEAN_DERIVED_SET_OF_IFF_LIMIT_POINT_OF",EUCLIDEAN_DERIVED_SET_OF_IFF_LIMIT_POINT_OF; "EUCLIDEAN_FRONTIER_OF",EUCLIDEAN_FRONTIER_OF; "EUCLIDEAN_INTERIOR_OF",EUCLIDEAN_INTERIOR_OF; +"EUCLIDEAN_MATROID",EUCLIDEAN_MATROID; +"EUCLIDEAN_MATROID_DIM",EUCLIDEAN_MATROID_DIM; +"EUCLIDEAN_MATROID_DIMENSION",EUCLIDEAN_MATROID_DIMENSION; +"EUCLIDEAN_MATROID_FINITE_DIM",EUCLIDEAN_MATROID_FINITE_DIM; +"EUCLIDEAN_MATROID_FINITE_DIMENSIONAL",EUCLIDEAN_MATROID_FINITE_DIMENSIONAL; +"EUCLIDEAN_MATROID_INDEPENDENT",EUCLIDEAN_MATROID_INDEPENDENT; +"EUCLIDEAN_MATROID_SPANNING",EUCLIDEAN_MATROID_SPANNING; +"EUCLIDEAN_MATROID_SUBSPACE",EUCLIDEAN_MATROID_SUBSPACE; "EUCLIDEAN_METRIC",EUCLIDEAN_METRIC; "EUCLIDEAN_SPACE_INFINITE",EUCLIDEAN_SPACE_INFINITE; +"EUCLIDEAN_SUBMATROID",EUCLIDEAN_SUBMATROID; "EUCLID_BOUND",EUCLID_BOUND; "EULER",EULER; "EULER_ROTATION_THEOREM",EULER_ROTATION_THEOREM; @@ -6032,6 +6045,7 @@ theorems := "EXISTS_UNIQUE_DEF",EXISTS_UNIQUE_DEF; "EXISTS_UNIQUE_REFL",EXISTS_UNIQUE_REFL; "EXISTS_UNIQUE_THM",EXISTS_UNIQUE_THM; +"EXISTS_UNIQUE_UNIONS_INTERS",EXISTS_UNIQUE_UNIONS_INTERS; "EXISTS_UNPAIR_FUN_THM",EXISTS_UNPAIR_FUN_THM; "EXISTS_UNPAIR_THM",EXISTS_UNPAIR_THM; "EXISTS_VECTORIZE",EXISTS_VECTORIZE; @@ -6385,6 +6399,8 @@ theorems := "FINITE_IMP_ENR",FINITE_IMP_ENR; "FINITE_IMP_FINITELY_GENERATED_GROUP",FINITE_IMP_FINITELY_GENERATED_GROUP; "FINITE_IMP_LOCALLY_FINITE_IN",FINITE_IMP_LOCALLY_FINITE_IN; +"FINITE_IMP_MATROID_FINITE_DIM",FINITE_IMP_MATROID_FINITE_DIM; +"FINITE_IMP_MATROID_FINITE_DIM_SPAN",FINITE_IMP_MATROID_FINITE_DIM_SPAN; "FINITE_IMP_NOT_OPEN",FINITE_IMP_NOT_OPEN; "FINITE_IMP_TOTALLY_BOUNDED_IN",FINITE_IMP_TOTALLY_BOUNDED_IN; "FINITE_IMP_TOTALLY_DISCONNECTED",FINITE_IMP_TOTALLY_DISCONNECTED; @@ -6468,12 +6484,15 @@ theorems := "FINITE_SUBGROUPS",FINITE_SUBGROUPS; "FINITE_SUBGROUPS_EQ",FINITE_SUBGROUPS_EQ; "FINITE_SUBGROUP_GENERATED",FINITE_SUBGROUP_GENERATED; +"FINITE_SUBGROUP_OF_SETWISE",FINITE_SUBGROUP_OF_SETWISE; "FINITE_SUBSET",FINITE_SUBSET; "FINITE_SUBSET_IMAGE",FINITE_SUBSET_IMAGE; "FINITE_SUBSET_IMAGE_IMP",FINITE_SUBSET_IMAGE_IMP; "FINITE_SUBSET_NUMSEG",FINITE_SUBSET_NUMSEG; "FINITE_SUBSET_UNIONS",FINITE_SUBSET_UNIONS; "FINITE_SUBSET_UNIONS_CHAIN",FINITE_SUBSET_UNIONS_CHAIN; +"FINITE_SUBSET_UNIONS_CHAIN_EQ",FINITE_SUBSET_UNIONS_CHAIN_EQ; +"FINITE_SUBSET_UNIONS_DIRECTED_EQ",FINITE_SUBSET_UNIONS_DIRECTED_EQ; "FINITE_SUM_IMAGE",FINITE_SUM_IMAGE; "FINITE_SUPPORT",FINITE_SUPPORT; "FINITE_SUPPORT_DELTA",FINITE_SUPPORT_DELTA; @@ -7165,6 +7184,7 @@ theorems := "GROUP_CONJUGATION_RIGHT_COSET",GROUP_CONJUGATION_RIGHT_COSET; "GROUP_CONJUGATION_RINV",GROUP_CONJUGATION_RINV; "GROUP_CONJUGATION_SUBGROUP_GENERATED",GROUP_CONJUGATION_SUBGROUP_GENERATED; +"GROUP_DIRECT_LIMIT",GROUP_DIRECT_LIMIT; "GROUP_DISJOINT_SUM_ALT",GROUP_DISJOINT_SUM_ALT; "GROUP_DISJOINT_SUM_CANCEL",GROUP_DISJOINT_SUM_CANCEL; "GROUP_DISJOINT_SUM_ID",GROUP_DISJOINT_SUM_ID; @@ -7201,6 +7221,7 @@ theorems := "GROUP_ELEMENT_ORDER_POW",GROUP_ELEMENT_ORDER_POW; "GROUP_ELEMENT_ORDER_POW_DIVIDES",GROUP_ELEMENT_ORDER_POW_DIVIDES; "GROUP_ELEMENT_ORDER_POW_GEN",GROUP_ELEMENT_ORDER_POW_GEN; +"GROUP_ELEMENT_ORDER_PRIME",GROUP_ELEMENT_ORDER_PRIME; "GROUP_ELEMENT_ORDER_PRIMEPOW_DECOMP",GROUP_ELEMENT_ORDER_PRIMEPOW_DECOMP; "GROUP_ELEMENT_ORDER_PROD_GROUP",GROUP_ELEMENT_ORDER_PROD_GROUP; "GROUP_ELEMENT_ORDER_PROD_GROUP_ALT",GROUP_ELEMENT_ORDER_PROD_GROUP_ALT; @@ -7538,6 +7559,8 @@ theorems := "GROUP_POW_ID",GROUP_POW_ID; "GROUP_POW_INTEGER_GROUP",GROUP_POW_INTEGER_GROUP; "GROUP_POW_INTEGER_MOD_GROUP",GROUP_POW_INTEGER_MOD_GROUP; +"GROUP_POW_MOD_ELEMENT_ORDER",GROUP_POW_MOD_ELEMENT_ORDER; +"GROUP_POW_MOD_ORDER",GROUP_POW_MOD_ORDER; "GROUP_POW_MUL",GROUP_POW_MUL; "GROUP_POW_MUL_EQ_ID_SYM",GROUP_POW_MUL_EQ_ID_SYM; "GROUP_POW_POW",GROUP_POW_POW; @@ -7662,12 +7685,15 @@ theorems := "GROUP_ZPOW_ID",GROUP_ZPOW_ID; "GROUP_ZPOW_INTEGER_GROUP",GROUP_ZPOW_INTEGER_GROUP; "GROUP_ZPOW_INTEGER_MOD_GROUP",GROUP_ZPOW_INTEGER_MOD_GROUP; +"GROUP_ZPOW_INV",GROUP_ZPOW_INV; "GROUP_ZPOW_MINUS1",GROUP_ZPOW_MINUS1; "GROUP_ZPOW_MUL",GROUP_ZPOW_MUL; "GROUP_ZPOW_NEG",GROUP_ZPOW_NEG; "GROUP_ZPOW_POW",GROUP_ZPOW_POW; "GROUP_ZPOW_PRODUCT_GROUP",GROUP_ZPOW_PRODUCT_GROUP; "GROUP_ZPOW_PROD_GROUP",GROUP_ZPOW_PROD_GROUP; +"GROUP_ZPOW_REM_ELEMENT_ORDER",GROUP_ZPOW_REM_ELEMENT_ORDER; +"GROUP_ZPOW_REM_ORDER",GROUP_ZPOW_REM_ORDER; "GROUP_ZPOW_SUB",GROUP_ZPOW_SUB; "GROUP_ZPOW_SUBGROUP_GENERATED",GROUP_ZPOW_SUBGROUP_GENERATED; "GROUP_ZPOW_SUB_ALT",GROUP_ZPOW_SUB_ALT; @@ -12327,6 +12353,141 @@ theorems := "MATRIX_VECTOR_MUL_TRANSP",MATRIX_VECTOR_MUL_TRANSP; "MATRIX_WLOG_INVERTIBLE",MATRIX_WLOG_INVERTIBLE; "MATRIX_WORKS",MATRIX_WORKS; +"MATROID_BASES_CARD_EQ",MATROID_BASES_CARD_EQ; +"MATROID_BASES_FINITE",MATROID_BASES_FINITE; +"MATROID_BASES_SIZE",MATROID_BASES_SIZE; +"MATROID_BASIS_EQ_MAXIMAL_INDEPENDENT",MATROID_BASIS_EQ_MAXIMAL_INDEPENDENT; +"MATROID_BASIS_EQ_MINIMAL_SPANNING",MATROID_BASIS_EQ_MINIMAL_SPANNING; +"MATROID_BASIS_EXISTS",MATROID_BASIS_EXISTS; +"MATROID_BASIS_EXISTS_DIM",MATROID_BASIS_EXISTS_DIM; +"MATROID_BASIS_EXISTS_DIMENSION",MATROID_BASIS_EXISTS_DIMENSION; +"MATROID_BASIS_IMP_SUBSET",MATROID_BASIS_IMP_SUBSET; +"MATROID_BASIS_SUBMATROID",MATROID_BASIS_SUBMATROID; +"MATROID_CHOOSE_SUBSET",MATROID_CHOOSE_SUBSET; +"MATROID_CHOOSE_SUBSPACE",MATROID_CHOOSE_SUBSPACE; +"MATROID_CONTAINS_BASIS_DIM",MATROID_CONTAINS_BASIS_DIM; +"MATROID_DIMENSION_ALT",MATROID_DIMENSION_ALT; +"MATROID_DIMENSION_EQ_CARD",MATROID_DIMENSION_EQ_CARD; +"MATROID_DIMENSION_FINITE_LE",MATROID_DIMENSION_FINITE_LE; +"MATROID_DIMENSION_GE",MATROID_DIMENSION_GE; +"MATROID_DIMENSION_GE_CARD",MATROID_DIMENSION_GE_CARD; +"MATROID_DIMENSION_GE_FINITE_CARD",MATROID_DIMENSION_GE_FINITE_CARD; +"MATROID_DIMENSION_LE",MATROID_DIMENSION_LE; +"MATROID_DIMENSION_UNIQUE",MATROID_DIMENSION_UNIQUE; +"MATROID_DIM_ALT",MATROID_DIM_ALT; +"MATROID_DIM_BASIS",MATROID_DIM_BASIS; +"MATROID_DIM_EMPTY",MATROID_DIM_EMPTY; +"MATROID_DIM_EQ_CARD",MATROID_DIM_EQ_CARD; +"MATROID_DIM_EQ_CARD_GEN",MATROID_DIM_EQ_CARD_GEN; +"MATROID_DIM_EQ_FINITE_CARD_EQ",MATROID_DIM_EQ_FINITE_CARD_EQ; +"MATROID_DIM_EQ_SPAN",MATROID_DIM_EQ_SPAN; +"MATROID_DIM_FINITE_LE",MATROID_DIM_FINITE_LE; +"MATROID_DIM_GE",MATROID_DIM_GE; +"MATROID_DIM_GE_CARD",MATROID_DIM_GE_CARD; +"MATROID_DIM_GE_CARD_GEN",MATROID_DIM_GE_CARD_GEN; +"MATROID_DIM_GE_FINITE_CARD",MATROID_DIM_GE_FINITE_CARD; +"MATROID_DIM_GE_FINITE_CARD_EQ",MATROID_DIM_GE_FINITE_CARD_EQ; +"MATROID_DIM_INSERT",MATROID_DIM_INSERT; +"MATROID_DIM_LE",MATROID_DIM_LE; +"MATROID_DIM_LE_CARD",MATROID_DIM_LE_CARD; +"MATROID_DIM_LE_CARD_GEN",MATROID_DIM_LE_CARD_GEN; +"MATROID_DIM_SET",MATROID_DIM_SET; +"MATROID_DIM_SPAN",MATROID_DIM_SPAN; +"MATROID_DIM_SPAN_EQ",MATROID_DIM_SPAN_EQ; +"MATROID_DIM_SPAN_EQ_GEN",MATROID_DIM_SPAN_EQ_GEN; +"MATROID_DIM_SPAN_PSUBSET",MATROID_DIM_SPAN_PSUBSET; +"MATROID_DIM_SPAN_SUBSET",MATROID_DIM_SPAN_SUBSET; +"MATROID_DIM_SUBSET",MATROID_DIM_SUBSET; +"MATROID_DIM_SUBSET_ALT",MATROID_DIM_SUBSET_ALT; +"MATROID_DIM_UNIQUE",MATROID_DIM_UNIQUE; +"MATROID_DIM_UNIQUE_ALT",MATROID_DIM_UNIQUE_ALT; +"MATROID_EQ_SPANS_CARD_EQ",MATROID_EQ_SPANS_CARD_EQ; +"MATROID_EQ_SPANS_FINITE",MATROID_EQ_SPANS_FINITE; +"MATROID_EQ_SPANS_SIZE",MATROID_EQ_SPANS_SIZE; +"MATROID_FINITE_DIM",MATROID_FINITE_DIM; +"MATROID_FINITE_DIMENSIONAL",MATROID_FINITE_DIMENSIONAL; +"MATROID_FINITE_DIMENSIONAL_ANY",MATROID_FINITE_DIMENSIONAL_ANY; +"MATROID_FINITE_DIMENSIONAL_BASIS",MATROID_FINITE_DIMENSIONAL_BASIS; +"MATROID_FINITE_DIMENSIONAL_CONTAINS_BASIS",MATROID_FINITE_DIMENSIONAL_CONTAINS_BASIS; +"MATROID_FINITE_DIMENSIONAL_DIM",MATROID_FINITE_DIMENSIONAL_DIM; +"MATROID_FINITE_DIM_BASIS",MATROID_FINITE_DIM_BASIS; +"MATROID_FINITE_DIM_EMPTY",MATROID_FINITE_DIM_EMPTY; +"MATROID_FINITE_DIM_FINITE",MATROID_FINITE_DIM_FINITE; +"MATROID_FINITE_DIM_IMP_SUBSET",MATROID_FINITE_DIM_IMP_SUBSET; +"MATROID_FINITE_DIM_INSERT",MATROID_FINITE_DIM_INSERT; +"MATROID_FINITE_DIM_MONO",MATROID_FINITE_DIM_MONO; +"MATROID_FINITE_DIM_SET",MATROID_FINITE_DIM_SET; +"MATROID_FINITE_DIM_SPAN",MATROID_FINITE_DIM_SPAN; +"MATROID_FINITE_DIM_SPAN_EQ",MATROID_FINITE_DIM_SPAN_EQ; +"MATROID_FINITE_DIM_SUBSET",MATROID_FINITE_DIM_SUBSET; +"MATROID_FINITE_DIM_UNION",MATROID_FINITE_DIM_UNION; +"MATROID_INDEPENDENT_CARD_LE_SPAN",MATROID_INDEPENDENT_CARD_LE_SPAN; +"MATROID_INDEPENDENT_CARD_LE_SPANNING",MATROID_INDEPENDENT_CARD_LE_SPANNING; +"MATROID_INDEPENDENT_CARD_LE_SPAN_FINITE",MATROID_INDEPENDENT_CARD_LE_SPAN_FINITE; +"MATROID_INDEPENDENT_CHAIN",MATROID_INDEPENDENT_CHAIN; +"MATROID_INDEPENDENT_EMPTY",MATROID_INDEPENDENT_EMPTY; +"MATROID_INDEPENDENT_EXTENDS_TO_BASIS",MATROID_INDEPENDENT_EXTENDS_TO_BASIS; +"MATROID_INDEPENDENT_FINITARY",MATROID_INDEPENDENT_FINITARY; +"MATROID_INDEPENDENT_IMP_FINITE",MATROID_INDEPENDENT_IMP_FINITE; +"MATROID_INDEPENDENT_IMP_SUBSET",MATROID_INDEPENDENT_IMP_SUBSET; +"MATROID_INDEPENDENT_INSERT",MATROID_INDEPENDENT_INSERT; +"MATROID_INDEPENDENT_MONO",MATROID_INDEPENDENT_MONO; +"MATROID_INDEPENDENT_SPANNING_FINITE",MATROID_INDEPENDENT_SPANNING_FINITE; +"MATROID_INDEPENDENT_SUBMATROID",MATROID_INDEPENDENT_SUBMATROID; +"MATROID_INTERMEDIATE_BASIS",MATROID_INTERMEDIATE_BASIS; +"MATROID_INTERMEDIATE_SPAN",MATROID_INTERMEDIATE_SPAN; +"MATROID_LOWDIM_EXPAND_BASIS",MATROID_LOWDIM_EXPAND_BASIS; +"MATROID_LOWDIM_EXPAND_DIMENSION",MATROID_LOWDIM_EXPAND_DIMENSION; +"MATROID_MAXIMAL_INDEPENDENT_SUBSET_SPAN",MATROID_MAXIMAL_INDEPENDENT_SUBSET_SPAN; +"MATROID_SPANNING_ALT",MATROID_SPANNING_ALT; +"MATROID_SPANNING_CONTAINS_BASIS",MATROID_SPANNING_CONTAINS_BASIS; +"MATROID_SPANNING_IMP_SUBSET",MATROID_SPANNING_IMP_SUBSET; +"MATROID_SPANNING_PSUBSET_INDEPENDENT",MATROID_SPANNING_PSUBSET_INDEPENDENT; +"MATROID_SPANNING_SET",MATROID_SPANNING_SET; +"MATROID_SPANNING_SUBMATROID",MATROID_SPANNING_SUBMATROID; +"MATROID_SPANNING_SUBMATROID_SELF",MATROID_SPANNING_SUBMATROID_SELF; +"MATROID_SPANNING_SUBSET_INDEPENDENT",MATROID_SPANNING_SUBSET_INDEPENDENT; +"MATROID_SPAN_CHAIN",MATROID_SPAN_CHAIN; +"MATROID_SPAN_DELETE_EQ",MATROID_SPAN_DELETE_EQ; +"MATROID_SPAN_DIM_EQ",MATROID_SPAN_DIM_EQ; +"MATROID_SPAN_EQ",MATROID_SPAN_EQ; +"MATROID_SPAN_EQ_SELF",MATROID_SPAN_EQ_SELF; +"MATROID_SPAN_EQ_SET",MATROID_SPAN_EQ_SET; +"MATROID_SPAN_EXCHANGE",MATROID_SPAN_EXCHANGE; +"MATROID_SPAN_EXCHANGE_DELETE",MATROID_SPAN_EXCHANGE_DELETE; +"MATROID_SPAN_FINITARY",MATROID_SPAN_FINITARY; +"MATROID_SPAN_FINITARY_GEN",MATROID_SPAN_FINITARY_GEN; +"MATROID_SPAN_FINITARY_MINIMAL",MATROID_SPAN_FINITARY_MINIMAL; +"MATROID_SPAN_INC",MATROID_SPAN_INC; +"MATROID_SPAN_INSERT_EQ",MATROID_SPAN_INSERT_EQ; +"MATROID_SPAN_INSERT_REFL",MATROID_SPAN_INSERT_REFL; +"MATROID_SPAN_INTER_SPANS",MATROID_SPAN_INTER_SPANS; +"MATROID_SPAN_INTER_SUBSET",MATROID_SPAN_INTER_SUBSET; +"MATROID_SPAN_MINIMAL",MATROID_SPAN_MINIMAL; +"MATROID_SPAN_MONO",MATROID_SPAN_MONO; +"MATROID_SPAN_OF_SUBSPACE",MATROID_SPAN_OF_SUBSPACE; +"MATROID_SPAN_PSUBSET_INDEPENDENT",MATROID_SPAN_PSUBSET_INDEPENDENT; +"MATROID_SPAN_SET",MATROID_SPAN_SET; +"MATROID_SPAN_SPAN",MATROID_SPAN_SPAN; +"MATROID_SPAN_SUBSET",MATROID_SPAN_SUBSET; +"MATROID_SPAN_SUBSET_EQ",MATROID_SPAN_SUBSET_EQ; +"MATROID_SPAN_SUBSET_SUBSPACE",MATROID_SPAN_SUBSET_SUBSPACE; +"MATROID_SPAN_SUBSPACE",MATROID_SPAN_SUBSPACE; +"MATROID_SPAN_SUPERSET",MATROID_SPAN_SUPERSET; +"MATROID_SPAN_TRANS",MATROID_SPAN_TRANS; +"MATROID_SPAN_UNION_EQ",MATROID_SPAN_UNION_EQ; +"MATROID_SPAN_UNION_SUBSET",MATROID_SPAN_UNION_SUBSET; +"MATROID_STEINITZ_EXCHANGE",MATROID_STEINITZ_EXCHANGE; +"MATROID_STEINITZ_EXCHANGE_ALT",MATROID_STEINITZ_EXCHANGE_ALT; +"MATROID_STEINITZ_EXCHANGE_FINITE",MATROID_STEINITZ_EXCHANGE_FINITE; +"MATROID_SUBSET_CONTAINS_BASIS",MATROID_SUBSET_CONTAINS_BASIS; +"MATROID_SUBSPACE",MATROID_SUBSPACE; +"MATROID_SUBSPACE_CHAIN",MATROID_SUBSPACE_CHAIN; +"MATROID_SUBSPACE_IMP_SUBSET",MATROID_SUBSPACE_IMP_SUBSET; +"MATROID_SUBSPACE_INTER",MATROID_SUBSPACE_INTER; +"MATROID_SUBSPACE_INTERS",MATROID_SUBSPACE_INTERS; +"MATROID_SUBSPACE_SET",MATROID_SUBSPACE_SET; +"MATROID_SUBSPACE_SPAN",MATROID_SUBSPACE_SPAN; "MAT_0_COMPONENT",MAT_0_COMPONENT; "MAT_0_ROW",MAT_0_ROW; "MAT_CMUL",MAT_CMUL; @@ -14931,6 +15092,7 @@ theorems := "PRIME_ORDER_IMP_CYCLIC_GROUP",PRIME_ORDER_IMP_CYCLIC_GROUP; "PRIME_ORDER_IMP_NO_PROPER_SUBGROUPS",PRIME_ORDER_IMP_NO_PROPER_SUBGROUPS; "PRIME_POWER_EXISTS",PRIME_POWER_EXISTS; +"PRIME_POWER_EXISTS_ALT",PRIME_POWER_EXISTS_ALT; "PRIME_POWER_EXP",PRIME_POWER_EXP; "PRIME_POWER_MULT",PRIME_POWER_MULT; "PRIME_PRIME_FACTOR",PRIME_PRIME_FACTOR; @@ -15098,11 +15260,14 @@ theorems := "P_HULL",P_HULL; "Product_DEF",Product_DEF; "QOSET_FLD",QOSET_FLD; +"QOSET_FLDEQ",QOSET_FLDEQ; "QOSET_MAX",QOSET_MAX; "QOSET_MIN",QOSET_MIN; "QOSET_POINTWISE",QOSET_POINTWISE; "QOSET_REFL",QOSET_REFL; +"QOSET_REFL_EQ",QOSET_REFL_EQ; "QOSET_RESTRICT",QOSET_RESTRICT; +"QOSET_TRANS",QOSET_TRANS; "QOSET_TRIVIAL",QOSET_TRIVIAL; "QOSET_num",QOSET_num; "QUANTIFY_SURJECTION_HIGHER_THM",QUANTIFY_SURJECTION_HIGHER_THM; @@ -16977,6 +17142,7 @@ theorems := "RESTRICTION_UNDEFINED",RESTRICTION_UNDEFINED; "RESTRICTION_UNIQUE",RESTRICTION_UNIQUE; "RESTRICTION_UNIQUE_ALT",RESTRICTION_UNIQUE_ALT; +"RESTRICTION_UNIV",RESTRICTION_UNIV; "RETRACTION",RETRACTION; "RETRACTION_ARC",RETRACTION_ARC; "RETRACTION_CLOSEST_POINT",RETRACTION_CLOSEST_POINT; @@ -17625,6 +17791,7 @@ theorems := "SIMPLEX_FURTHEST_LE",SIMPLEX_FURTHEST_LE; "SIMPLEX_FURTHEST_LE_EXISTS",SIMPLEX_FURTHEST_LE_EXISTS; "SIMPLEX_FURTHEST_LT",SIMPLEX_FURTHEST_LT; +"SIMPLEX_FURTHEST_LT_EXISTS",SIMPLEX_FURTHEST_LT_EXISTS; "SIMPLEX_IMP_CLOSED",SIMPLEX_IMP_CLOSED; "SIMPLEX_IMP_COMPACT",SIMPLEX_IMP_COMPACT; "SIMPLEX_IMP_CONVEX",SIMPLEX_IMP_CONVEX; @@ -17821,6 +17988,7 @@ theorems := "SINGULAR_SUBDIVISION_SIMPLICIAL_SIMPLEX",SINGULAR_SUBDIVISION_SIMPLICIAL_SIMPLEX; "SINGULAR_SUBDIVISION_SUB",SINGULAR_SUBDIVISION_SUB; "SINGULAR_SUBDIVISION_ZERO",SINGULAR_SUBDIVISION_ZERO; +"SING_ALT",SING_ALT; "SING_GSPEC",SING_GSPEC; "SING_STRONG_DEFORMATION_RETRACT_OF_AR",SING_STRONG_DEFORMATION_RETRACT_OF_AR; "SING_SUBSET",SING_SUBSET; @@ -18148,6 +18316,11 @@ theorems := "SUBINTERVAL_MEAN_VALUE_THEOREM",SUBINTERVAL_MEAN_VALUE_THEOREM; "SUBINTERVAL_MEAN_VALUE_THEOREM_ALT",SUBINTERVAL_MEAN_VALUE_THEOREM_ALT; "SUBINTERVAL_MEAN_VALUE_THEOREM_SEQ",SUBINTERVAL_MEAN_VALUE_THEOREM_SEQ; +"SUBMATROID",SUBMATROID; +"SUBMATROID_GEN",SUBMATROID_GEN; +"SUBMATROID_SET",SUBMATROID_SET; +"SUBMATROID_SPAN",SUBMATROID_SPAN; +"SUBMATROID_SUBSET",SUBMATROID_SUBSET; "SUBMETRIC",SUBMETRIC; "SUBMETRIC_MSPACE",SUBMETRIC_MSPACE; "SUBMETRIC_PROD_METRIC",SUBMETRIC_PROD_METRIC; @@ -18210,6 +18383,7 @@ theorems := "SUBSET_INTER_ABSORPTION",SUBSET_INTER_ABSORPTION; "SUBSET_LE_DIM",SUBSET_LE_DIM; "SUBSET_LIFT_IMAGE",SUBSET_LIFT_IMAGE; +"SUBSET_MATROID_SPAN",SUBSET_MATROID_SPAN; "SUBSET_NUMSEG",SUBSET_NUMSEG; "SUBSET_OF_FACE_OF",SUBSET_OF_FACE_OF; "SUBSET_OF_FACE_OF_AFFINE_HULL",SUBSET_OF_FACE_OF_AFFINE_HULL; @@ -19117,6 +19291,7 @@ theorems := "UNIONS_CONNECTED_COMPONENTS_OF",UNIONS_CONNECTED_COMPONENTS_OF; "UNIONS_DELETE_EMPTY",UNIONS_DELETE_EMPTY; "UNIONS_DIFF",UNIONS_DIFF; +"UNIONS_EQ_INTERS",UNIONS_EQ_INTERS; "UNIONS_GROUP_ORBITS",UNIONS_GROUP_ORBITS; "UNIONS_GROUP_ORBITS_CLOSED",UNIONS_GROUP_ORBITS_CLOSED; "UNIONS_GROUP_ORBITS_INVARIANT",UNIONS_GROUP_ORBITS_INVARIANT; @@ -19172,6 +19347,7 @@ theorems := "UNIT_INTERVAL_NONEMPTY",UNIT_INTERVAL_NONEMPTY; "UNIV",UNIV; "UNIVERSAL_COVERING_SPACE",UNIVERSAL_COVERING_SPACE; +"UNIV_1",UNIV_1; "UNIV_GSPEC",UNIV_GSPEC; "UNIV_HAS_SIZE_DIMINDEX",UNIV_HAS_SIZE_DIMINDEX; "UNIV_NOT_EMPTY",UNIV_NOT_EMPTY; @@ -19645,6 +19821,7 @@ theorems := "ZIP",ZIP; "ZIP_DEF",ZIP_DEF; "ZL",ZL; +"ZL_STRONG",ZL_STRONG; "ZL_SUBSETS",ZL_SUBSETS; "ZL_SUBSETS_UNIONS",ZL_SUBSETS_UNIONS; "ZL_SUBSETS_UNIONS_NONEMPTY",ZL_SUBSETS_UNIONS_NONEMPTY; @@ -19825,6 +20002,7 @@ theorems := "eq_c",eq_c; "equiintegrable_on",equiintegrable_on; "euclidean",euclidean; +"euclidean_matroid",euclidean_matroid; "euclidean_metric",euclidean_metric; "euclidean_space",euclidean_space; "euclideanreal",euclideanreal; @@ -20076,6 +20254,17 @@ theorems := "matrix_neg",matrix_neg; "matrix_sub",matrix_sub; "matrix_vector_mul",matrix_vector_mul; +"matroid_basis",matroid_basis; +"matroid_dim",matroid_dim; +"matroid_dimension",matroid_dimension; +"matroid_finite_dim",matroid_finite_dim; +"matroid_finite_dimensional",matroid_finite_dimensional; +"matroid_independent",matroid_independent; +"matroid_set",matroid_set; +"matroid_span",matroid_span; +"matroid_spanning",matroid_spanning; +"matroid_subspace",matroid_subspace; +"matroid_tybij",matroid_tybij; "mball",mball; "mbasis",mbasis; "mbounded",mbounded; @@ -20364,6 +20553,7 @@ theorems := "string_INFINITE",string_INFINITE; "subgroup_generated",subgroup_generated; "subgroup_of",subgroup_of; +"submatroid",submatroid; "submetric",submetric; "subpath",subpath; "subspace",subspace; diff --git a/Multivariate/make.ml b/Multivariate/make.ml index 181b331b..7cd6695e 100644 --- a/Multivariate/make.ml +++ b/Multivariate/make.ml @@ -9,6 +9,7 @@ loadt "Library/floor.ml";; (* Useful here and there *) loadt "Multivariate/misc.ml";; (* Background stuff *) loadt "Library/iter.ml";; (* n-fold iteration of function *) loadt "Library/grouptheory.ml";; (* Groups, to support homology *) +loadt "Library/matroids.ml";; (* Generalized linear dependence *) (* ------------------------------------------------------------------------- *) (* The main core theory. *) diff --git a/Multivariate/make_complex.ml b/Multivariate/make_complex.ml index 3048e561..7b85f164 100644 --- a/Multivariate/make_complex.ml +++ b/Multivariate/make_complex.ml @@ -9,6 +9,7 @@ loadt "Library/floor.ml";; (* Useful here and there *) loadt "Multivariate/misc.ml";; (* Background stuff *) loadt "Library/iter.ml";; (* n-fold iteration of function *) loadt "Library/grouptheory.ml";; (* Groups, to support homology *) +loadt "Library/matroids.ml";; (* Generalized linear dependence *) loadt "Library/binomial.ml";; (* For Leibniz deriv formula etc. *) (* ------------------------------------------------------------------------- *) diff --git a/Multivariate/multivariate_database.ml b/Multivariate/multivariate_database.ml index 94779a45..d74683d6 100644 --- a/Multivariate/multivariate_database.ml +++ b/Multivariate/multivariate_database.ml @@ -898,6 +898,8 @@ theorems := "BILINEAR_EQ_STDBASIS",BILINEAR_EQ_STDBASIS; "BILINEAR_GEOM",BILINEAR_GEOM; "BILINEAR_INNER",BILINEAR_INNER; +"BILINEAR_IN_AFFINE_HULL",BILINEAR_IN_AFFINE_HULL; +"BILINEAR_IN_CONVEX_HULL",BILINEAR_IN_CONVEX_HULL; "BILINEAR_LADD",BILINEAR_LADD; "BILINEAR_LIFT_MUL",BILINEAR_LIFT_MUL; "BILINEAR_LMUL",BILINEAR_LMUL; @@ -4467,6 +4469,7 @@ theorems := "DIVIDES_DIV_MULT",DIVIDES_DIV_MULT; "DIVIDES_DIV_NOT",DIVIDES_DIV_NOT; "DIVIDES_DIV_SELF",DIVIDES_DIV_SELF; +"DIVIDES_EQ_ZERO",DIVIDES_EQ_ZERO; "DIVIDES_EXP",DIVIDES_EXP; "DIVIDES_EXP2",DIVIDES_EXP2; "DIVIDES_EXP2_EQ",DIVIDES_EXP2_EQ; @@ -4854,6 +4857,7 @@ theorems := "EQ_TRANS",EQ_TRANS; "EQ_UNIV",EQ_UNIV; "ETA_AX",ETA_AX; +"ETA_ONE",ETA_ONE; "EUCLID",EUCLID; "EUCLIDEANREAL_CLOSURE_OF_HALFSPACE_GE",EUCLIDEANREAL_CLOSURE_OF_HALFSPACE_GE; "EUCLIDEANREAL_CLOSURE_OF_HALFSPACE_GT",EUCLIDEANREAL_CLOSURE_OF_HALFSPACE_GT; @@ -4874,8 +4878,17 @@ theorems := "EUCLIDEAN_DERIVED_SET_OF_IFF_LIMIT_POINT_OF",EUCLIDEAN_DERIVED_SET_OF_IFF_LIMIT_POINT_OF; "EUCLIDEAN_FRONTIER_OF",EUCLIDEAN_FRONTIER_OF; "EUCLIDEAN_INTERIOR_OF",EUCLIDEAN_INTERIOR_OF; +"EUCLIDEAN_MATROID",EUCLIDEAN_MATROID; +"EUCLIDEAN_MATROID_DIM",EUCLIDEAN_MATROID_DIM; +"EUCLIDEAN_MATROID_DIMENSION",EUCLIDEAN_MATROID_DIMENSION; +"EUCLIDEAN_MATROID_FINITE_DIM",EUCLIDEAN_MATROID_FINITE_DIM; +"EUCLIDEAN_MATROID_FINITE_DIMENSIONAL",EUCLIDEAN_MATROID_FINITE_DIMENSIONAL; +"EUCLIDEAN_MATROID_INDEPENDENT",EUCLIDEAN_MATROID_INDEPENDENT; +"EUCLIDEAN_MATROID_SPANNING",EUCLIDEAN_MATROID_SPANNING; +"EUCLIDEAN_MATROID_SUBSPACE",EUCLIDEAN_MATROID_SUBSPACE; "EUCLIDEAN_METRIC",EUCLIDEAN_METRIC; "EUCLIDEAN_SPACE_INFINITE",EUCLIDEAN_SPACE_INFINITE; +"EUCLIDEAN_SUBMATROID",EUCLIDEAN_SUBMATROID; "EUCLID_BOUND",EUCLID_BOUND; "EULER_ROTATION_THEOREM",EULER_ROTATION_THEOREM; "EULER_ROTATION_THEOREM_GEN",EULER_ROTATION_THEOREM_GEN; @@ -5046,6 +5059,7 @@ theorems := "EXISTS_UNIQUE_DEF",EXISTS_UNIQUE_DEF; "EXISTS_UNIQUE_REFL",EXISTS_UNIQUE_REFL; "EXISTS_UNIQUE_THM",EXISTS_UNIQUE_THM; +"EXISTS_UNIQUE_UNIONS_INTERS",EXISTS_UNIQUE_UNIONS_INTERS; "EXISTS_UNPAIR_FUN_THM",EXISTS_UNPAIR_FUN_THM; "EXISTS_UNPAIR_THM",EXISTS_UNPAIR_THM; "EXISTS_VECTORIZE",EXISTS_VECTORIZE; @@ -5381,6 +5395,8 @@ theorems := "FINITE_IMP_ENR",FINITE_IMP_ENR; "FINITE_IMP_FINITELY_GENERATED_GROUP",FINITE_IMP_FINITELY_GENERATED_GROUP; "FINITE_IMP_LOCALLY_FINITE_IN",FINITE_IMP_LOCALLY_FINITE_IN; +"FINITE_IMP_MATROID_FINITE_DIM",FINITE_IMP_MATROID_FINITE_DIM; +"FINITE_IMP_MATROID_FINITE_DIM_SPAN",FINITE_IMP_MATROID_FINITE_DIM_SPAN; "FINITE_IMP_NOT_OPEN",FINITE_IMP_NOT_OPEN; "FINITE_IMP_TOTALLY_BOUNDED_IN",FINITE_IMP_TOTALLY_BOUNDED_IN; "FINITE_IMP_TOTALLY_DISCONNECTED",FINITE_IMP_TOTALLY_DISCONNECTED; @@ -5463,12 +5479,15 @@ theorems := "FINITE_SUBGROUPS",FINITE_SUBGROUPS; "FINITE_SUBGROUPS_EQ",FINITE_SUBGROUPS_EQ; "FINITE_SUBGROUP_GENERATED",FINITE_SUBGROUP_GENERATED; +"FINITE_SUBGROUP_OF_SETWISE",FINITE_SUBGROUP_OF_SETWISE; "FINITE_SUBSET",FINITE_SUBSET; "FINITE_SUBSET_IMAGE",FINITE_SUBSET_IMAGE; "FINITE_SUBSET_IMAGE_IMP",FINITE_SUBSET_IMAGE_IMP; "FINITE_SUBSET_NUMSEG",FINITE_SUBSET_NUMSEG; "FINITE_SUBSET_UNIONS",FINITE_SUBSET_UNIONS; "FINITE_SUBSET_UNIONS_CHAIN",FINITE_SUBSET_UNIONS_CHAIN; +"FINITE_SUBSET_UNIONS_CHAIN_EQ",FINITE_SUBSET_UNIONS_CHAIN_EQ; +"FINITE_SUBSET_UNIONS_DIRECTED_EQ",FINITE_SUBSET_UNIONS_DIRECTED_EQ; "FINITE_SUM_IMAGE",FINITE_SUM_IMAGE; "FINITE_SUPPORT",FINITE_SUPPORT; "FINITE_SUPPORT_DELTA",FINITE_SUPPORT_DELTA; @@ -6138,6 +6157,7 @@ theorems := "GROUP_CONJUGATION_RIGHT_COSET",GROUP_CONJUGATION_RIGHT_COSET; "GROUP_CONJUGATION_RINV",GROUP_CONJUGATION_RINV; "GROUP_CONJUGATION_SUBGROUP_GENERATED",GROUP_CONJUGATION_SUBGROUP_GENERATED; +"GROUP_DIRECT_LIMIT",GROUP_DIRECT_LIMIT; "GROUP_DISJOINT_SUM_ALT",GROUP_DISJOINT_SUM_ALT; "GROUP_DISJOINT_SUM_CANCEL",GROUP_DISJOINT_SUM_CANCEL; "GROUP_DISJOINT_SUM_ID",GROUP_DISJOINT_SUM_ID; @@ -6174,6 +6194,7 @@ theorems := "GROUP_ELEMENT_ORDER_POW",GROUP_ELEMENT_ORDER_POW; "GROUP_ELEMENT_ORDER_POW_DIVIDES",GROUP_ELEMENT_ORDER_POW_DIVIDES; "GROUP_ELEMENT_ORDER_POW_GEN",GROUP_ELEMENT_ORDER_POW_GEN; +"GROUP_ELEMENT_ORDER_PRIME",GROUP_ELEMENT_ORDER_PRIME; "GROUP_ELEMENT_ORDER_PRIMEPOW_DECOMP",GROUP_ELEMENT_ORDER_PRIMEPOW_DECOMP; "GROUP_ELEMENT_ORDER_PROD_GROUP",GROUP_ELEMENT_ORDER_PROD_GROUP; "GROUP_ELEMENT_ORDER_PROD_GROUP_ALT",GROUP_ELEMENT_ORDER_PROD_GROUP_ALT; @@ -6511,6 +6532,8 @@ theorems := "GROUP_POW_ID",GROUP_POW_ID; "GROUP_POW_INTEGER_GROUP",GROUP_POW_INTEGER_GROUP; "GROUP_POW_INTEGER_MOD_GROUP",GROUP_POW_INTEGER_MOD_GROUP; +"GROUP_POW_MOD_ELEMENT_ORDER",GROUP_POW_MOD_ELEMENT_ORDER; +"GROUP_POW_MOD_ORDER",GROUP_POW_MOD_ORDER; "GROUP_POW_MUL",GROUP_POW_MUL; "GROUP_POW_MUL_EQ_ID_SYM",GROUP_POW_MUL_EQ_ID_SYM; "GROUP_POW_POW",GROUP_POW_POW; @@ -6635,12 +6658,15 @@ theorems := "GROUP_ZPOW_ID",GROUP_ZPOW_ID; "GROUP_ZPOW_INTEGER_GROUP",GROUP_ZPOW_INTEGER_GROUP; "GROUP_ZPOW_INTEGER_MOD_GROUP",GROUP_ZPOW_INTEGER_MOD_GROUP; +"GROUP_ZPOW_INV",GROUP_ZPOW_INV; "GROUP_ZPOW_MINUS1",GROUP_ZPOW_MINUS1; "GROUP_ZPOW_MUL",GROUP_ZPOW_MUL; "GROUP_ZPOW_NEG",GROUP_ZPOW_NEG; "GROUP_ZPOW_POW",GROUP_ZPOW_POW; "GROUP_ZPOW_PRODUCT_GROUP",GROUP_ZPOW_PRODUCT_GROUP; "GROUP_ZPOW_PROD_GROUP",GROUP_ZPOW_PROD_GROUP; +"GROUP_ZPOW_REM_ELEMENT_ORDER",GROUP_ZPOW_REM_ELEMENT_ORDER; +"GROUP_ZPOW_REM_ORDER",GROUP_ZPOW_REM_ORDER; "GROUP_ZPOW_SUB",GROUP_ZPOW_SUB; "GROUP_ZPOW_SUBGROUP_GENERATED",GROUP_ZPOW_SUBGROUP_GENERATED; "GROUP_ZPOW_SUB_ALT",GROUP_ZPOW_SUB_ALT; @@ -10572,6 +10598,141 @@ theorems := "MATRIX_VECTOR_MUL_TRANSP",MATRIX_VECTOR_MUL_TRANSP; "MATRIX_WLOG_INVERTIBLE",MATRIX_WLOG_INVERTIBLE; "MATRIX_WORKS",MATRIX_WORKS; +"MATROID_BASES_CARD_EQ",MATROID_BASES_CARD_EQ; +"MATROID_BASES_FINITE",MATROID_BASES_FINITE; +"MATROID_BASES_SIZE",MATROID_BASES_SIZE; +"MATROID_BASIS_EQ_MAXIMAL_INDEPENDENT",MATROID_BASIS_EQ_MAXIMAL_INDEPENDENT; +"MATROID_BASIS_EQ_MINIMAL_SPANNING",MATROID_BASIS_EQ_MINIMAL_SPANNING; +"MATROID_BASIS_EXISTS",MATROID_BASIS_EXISTS; +"MATROID_BASIS_EXISTS_DIM",MATROID_BASIS_EXISTS_DIM; +"MATROID_BASIS_EXISTS_DIMENSION",MATROID_BASIS_EXISTS_DIMENSION; +"MATROID_BASIS_IMP_SUBSET",MATROID_BASIS_IMP_SUBSET; +"MATROID_BASIS_SUBMATROID",MATROID_BASIS_SUBMATROID; +"MATROID_CHOOSE_SUBSET",MATROID_CHOOSE_SUBSET; +"MATROID_CHOOSE_SUBSPACE",MATROID_CHOOSE_SUBSPACE; +"MATROID_CONTAINS_BASIS_DIM",MATROID_CONTAINS_BASIS_DIM; +"MATROID_DIMENSION_ALT",MATROID_DIMENSION_ALT; +"MATROID_DIMENSION_EQ_CARD",MATROID_DIMENSION_EQ_CARD; +"MATROID_DIMENSION_FINITE_LE",MATROID_DIMENSION_FINITE_LE; +"MATROID_DIMENSION_GE",MATROID_DIMENSION_GE; +"MATROID_DIMENSION_GE_CARD",MATROID_DIMENSION_GE_CARD; +"MATROID_DIMENSION_GE_FINITE_CARD",MATROID_DIMENSION_GE_FINITE_CARD; +"MATROID_DIMENSION_LE",MATROID_DIMENSION_LE; +"MATROID_DIMENSION_UNIQUE",MATROID_DIMENSION_UNIQUE; +"MATROID_DIM_ALT",MATROID_DIM_ALT; +"MATROID_DIM_BASIS",MATROID_DIM_BASIS; +"MATROID_DIM_EMPTY",MATROID_DIM_EMPTY; +"MATROID_DIM_EQ_CARD",MATROID_DIM_EQ_CARD; +"MATROID_DIM_EQ_CARD_GEN",MATROID_DIM_EQ_CARD_GEN; +"MATROID_DIM_EQ_FINITE_CARD_EQ",MATROID_DIM_EQ_FINITE_CARD_EQ; +"MATROID_DIM_EQ_SPAN",MATROID_DIM_EQ_SPAN; +"MATROID_DIM_FINITE_LE",MATROID_DIM_FINITE_LE; +"MATROID_DIM_GE",MATROID_DIM_GE; +"MATROID_DIM_GE_CARD",MATROID_DIM_GE_CARD; +"MATROID_DIM_GE_CARD_GEN",MATROID_DIM_GE_CARD_GEN; +"MATROID_DIM_GE_FINITE_CARD",MATROID_DIM_GE_FINITE_CARD; +"MATROID_DIM_GE_FINITE_CARD_EQ",MATROID_DIM_GE_FINITE_CARD_EQ; +"MATROID_DIM_INSERT",MATROID_DIM_INSERT; +"MATROID_DIM_LE",MATROID_DIM_LE; +"MATROID_DIM_LE_CARD",MATROID_DIM_LE_CARD; +"MATROID_DIM_LE_CARD_GEN",MATROID_DIM_LE_CARD_GEN; +"MATROID_DIM_SET",MATROID_DIM_SET; +"MATROID_DIM_SPAN",MATROID_DIM_SPAN; +"MATROID_DIM_SPAN_EQ",MATROID_DIM_SPAN_EQ; +"MATROID_DIM_SPAN_EQ_GEN",MATROID_DIM_SPAN_EQ_GEN; +"MATROID_DIM_SPAN_PSUBSET",MATROID_DIM_SPAN_PSUBSET; +"MATROID_DIM_SPAN_SUBSET",MATROID_DIM_SPAN_SUBSET; +"MATROID_DIM_SUBSET",MATROID_DIM_SUBSET; +"MATROID_DIM_SUBSET_ALT",MATROID_DIM_SUBSET_ALT; +"MATROID_DIM_UNIQUE",MATROID_DIM_UNIQUE; +"MATROID_DIM_UNIQUE_ALT",MATROID_DIM_UNIQUE_ALT; +"MATROID_EQ_SPANS_CARD_EQ",MATROID_EQ_SPANS_CARD_EQ; +"MATROID_EQ_SPANS_FINITE",MATROID_EQ_SPANS_FINITE; +"MATROID_EQ_SPANS_SIZE",MATROID_EQ_SPANS_SIZE; +"MATROID_FINITE_DIM",MATROID_FINITE_DIM; +"MATROID_FINITE_DIMENSIONAL",MATROID_FINITE_DIMENSIONAL; +"MATROID_FINITE_DIMENSIONAL_ANY",MATROID_FINITE_DIMENSIONAL_ANY; +"MATROID_FINITE_DIMENSIONAL_BASIS",MATROID_FINITE_DIMENSIONAL_BASIS; +"MATROID_FINITE_DIMENSIONAL_CONTAINS_BASIS",MATROID_FINITE_DIMENSIONAL_CONTAINS_BASIS; +"MATROID_FINITE_DIMENSIONAL_DIM",MATROID_FINITE_DIMENSIONAL_DIM; +"MATROID_FINITE_DIM_BASIS",MATROID_FINITE_DIM_BASIS; +"MATROID_FINITE_DIM_EMPTY",MATROID_FINITE_DIM_EMPTY; +"MATROID_FINITE_DIM_FINITE",MATROID_FINITE_DIM_FINITE; +"MATROID_FINITE_DIM_IMP_SUBSET",MATROID_FINITE_DIM_IMP_SUBSET; +"MATROID_FINITE_DIM_INSERT",MATROID_FINITE_DIM_INSERT; +"MATROID_FINITE_DIM_MONO",MATROID_FINITE_DIM_MONO; +"MATROID_FINITE_DIM_SET",MATROID_FINITE_DIM_SET; +"MATROID_FINITE_DIM_SPAN",MATROID_FINITE_DIM_SPAN; +"MATROID_FINITE_DIM_SPAN_EQ",MATROID_FINITE_DIM_SPAN_EQ; +"MATROID_FINITE_DIM_SUBSET",MATROID_FINITE_DIM_SUBSET; +"MATROID_FINITE_DIM_UNION",MATROID_FINITE_DIM_UNION; +"MATROID_INDEPENDENT_CARD_LE_SPAN",MATROID_INDEPENDENT_CARD_LE_SPAN; +"MATROID_INDEPENDENT_CARD_LE_SPANNING",MATROID_INDEPENDENT_CARD_LE_SPANNING; +"MATROID_INDEPENDENT_CARD_LE_SPAN_FINITE",MATROID_INDEPENDENT_CARD_LE_SPAN_FINITE; +"MATROID_INDEPENDENT_CHAIN",MATROID_INDEPENDENT_CHAIN; +"MATROID_INDEPENDENT_EMPTY",MATROID_INDEPENDENT_EMPTY; +"MATROID_INDEPENDENT_EXTENDS_TO_BASIS",MATROID_INDEPENDENT_EXTENDS_TO_BASIS; +"MATROID_INDEPENDENT_FINITARY",MATROID_INDEPENDENT_FINITARY; +"MATROID_INDEPENDENT_IMP_FINITE",MATROID_INDEPENDENT_IMP_FINITE; +"MATROID_INDEPENDENT_IMP_SUBSET",MATROID_INDEPENDENT_IMP_SUBSET; +"MATROID_INDEPENDENT_INSERT",MATROID_INDEPENDENT_INSERT; +"MATROID_INDEPENDENT_MONO",MATROID_INDEPENDENT_MONO; +"MATROID_INDEPENDENT_SPANNING_FINITE",MATROID_INDEPENDENT_SPANNING_FINITE; +"MATROID_INDEPENDENT_SUBMATROID",MATROID_INDEPENDENT_SUBMATROID; +"MATROID_INTERMEDIATE_BASIS",MATROID_INTERMEDIATE_BASIS; +"MATROID_INTERMEDIATE_SPAN",MATROID_INTERMEDIATE_SPAN; +"MATROID_LOWDIM_EXPAND_BASIS",MATROID_LOWDIM_EXPAND_BASIS; +"MATROID_LOWDIM_EXPAND_DIMENSION",MATROID_LOWDIM_EXPAND_DIMENSION; +"MATROID_MAXIMAL_INDEPENDENT_SUBSET_SPAN",MATROID_MAXIMAL_INDEPENDENT_SUBSET_SPAN; +"MATROID_SPANNING_ALT",MATROID_SPANNING_ALT; +"MATROID_SPANNING_CONTAINS_BASIS",MATROID_SPANNING_CONTAINS_BASIS; +"MATROID_SPANNING_IMP_SUBSET",MATROID_SPANNING_IMP_SUBSET; +"MATROID_SPANNING_PSUBSET_INDEPENDENT",MATROID_SPANNING_PSUBSET_INDEPENDENT; +"MATROID_SPANNING_SET",MATROID_SPANNING_SET; +"MATROID_SPANNING_SUBMATROID",MATROID_SPANNING_SUBMATROID; +"MATROID_SPANNING_SUBMATROID_SELF",MATROID_SPANNING_SUBMATROID_SELF; +"MATROID_SPANNING_SUBSET_INDEPENDENT",MATROID_SPANNING_SUBSET_INDEPENDENT; +"MATROID_SPAN_CHAIN",MATROID_SPAN_CHAIN; +"MATROID_SPAN_DELETE_EQ",MATROID_SPAN_DELETE_EQ; +"MATROID_SPAN_DIM_EQ",MATROID_SPAN_DIM_EQ; +"MATROID_SPAN_EQ",MATROID_SPAN_EQ; +"MATROID_SPAN_EQ_SELF",MATROID_SPAN_EQ_SELF; +"MATROID_SPAN_EQ_SET",MATROID_SPAN_EQ_SET; +"MATROID_SPAN_EXCHANGE",MATROID_SPAN_EXCHANGE; +"MATROID_SPAN_EXCHANGE_DELETE",MATROID_SPAN_EXCHANGE_DELETE; +"MATROID_SPAN_FINITARY",MATROID_SPAN_FINITARY; +"MATROID_SPAN_FINITARY_GEN",MATROID_SPAN_FINITARY_GEN; +"MATROID_SPAN_FINITARY_MINIMAL",MATROID_SPAN_FINITARY_MINIMAL; +"MATROID_SPAN_INC",MATROID_SPAN_INC; +"MATROID_SPAN_INSERT_EQ",MATROID_SPAN_INSERT_EQ; +"MATROID_SPAN_INSERT_REFL",MATROID_SPAN_INSERT_REFL; +"MATROID_SPAN_INTER_SPANS",MATROID_SPAN_INTER_SPANS; +"MATROID_SPAN_INTER_SUBSET",MATROID_SPAN_INTER_SUBSET; +"MATROID_SPAN_MINIMAL",MATROID_SPAN_MINIMAL; +"MATROID_SPAN_MONO",MATROID_SPAN_MONO; +"MATROID_SPAN_OF_SUBSPACE",MATROID_SPAN_OF_SUBSPACE; +"MATROID_SPAN_PSUBSET_INDEPENDENT",MATROID_SPAN_PSUBSET_INDEPENDENT; +"MATROID_SPAN_SET",MATROID_SPAN_SET; +"MATROID_SPAN_SPAN",MATROID_SPAN_SPAN; +"MATROID_SPAN_SUBSET",MATROID_SPAN_SUBSET; +"MATROID_SPAN_SUBSET_EQ",MATROID_SPAN_SUBSET_EQ; +"MATROID_SPAN_SUBSET_SUBSPACE",MATROID_SPAN_SUBSET_SUBSPACE; +"MATROID_SPAN_SUBSPACE",MATROID_SPAN_SUBSPACE; +"MATROID_SPAN_SUPERSET",MATROID_SPAN_SUPERSET; +"MATROID_SPAN_TRANS",MATROID_SPAN_TRANS; +"MATROID_SPAN_UNION_EQ",MATROID_SPAN_UNION_EQ; +"MATROID_SPAN_UNION_SUBSET",MATROID_SPAN_UNION_SUBSET; +"MATROID_STEINITZ_EXCHANGE",MATROID_STEINITZ_EXCHANGE; +"MATROID_STEINITZ_EXCHANGE_ALT",MATROID_STEINITZ_EXCHANGE_ALT; +"MATROID_STEINITZ_EXCHANGE_FINITE",MATROID_STEINITZ_EXCHANGE_FINITE; +"MATROID_SUBSET_CONTAINS_BASIS",MATROID_SUBSET_CONTAINS_BASIS; +"MATROID_SUBSPACE",MATROID_SUBSPACE; +"MATROID_SUBSPACE_CHAIN",MATROID_SUBSPACE_CHAIN; +"MATROID_SUBSPACE_IMP_SUBSET",MATROID_SUBSPACE_IMP_SUBSET; +"MATROID_SUBSPACE_INTER",MATROID_SUBSPACE_INTER; +"MATROID_SUBSPACE_INTERS",MATROID_SUBSPACE_INTERS; +"MATROID_SUBSPACE_SET",MATROID_SUBSPACE_SET; +"MATROID_SUBSPACE_SPAN",MATROID_SUBSPACE_SPAN; "MAT_0_COMPONENT",MAT_0_COMPONENT; "MAT_0_ROW",MAT_0_ROW; "MAT_CMUL",MAT_CMUL; @@ -12988,6 +13149,7 @@ theorems := "PRIME_ORDER_IMP_CYCLIC_GROUP",PRIME_ORDER_IMP_CYCLIC_GROUP; "PRIME_ORDER_IMP_NO_PROPER_SUBGROUPS",PRIME_ORDER_IMP_NO_PROPER_SUBGROUPS; "PRIME_POWER_EXISTS",PRIME_POWER_EXISTS; +"PRIME_POWER_EXISTS_ALT",PRIME_POWER_EXISTS_ALT; "PRIME_POWER_EXP",PRIME_POWER_EXP; "PRIME_POWER_MULT",PRIME_POWER_MULT; "PRIME_PRIME_FACTOR",PRIME_PRIME_FACTOR; @@ -13152,11 +13314,14 @@ theorems := "P_HULL",P_HULL; "Product_DEF",Product_DEF; "QOSET_FLD",QOSET_FLD; +"QOSET_FLDEQ",QOSET_FLDEQ; "QOSET_MAX",QOSET_MAX; "QOSET_MIN",QOSET_MIN; "QOSET_POINTWISE",QOSET_POINTWISE; "QOSET_REFL",QOSET_REFL; +"QOSET_REFL_EQ",QOSET_REFL_EQ; "QOSET_RESTRICT",QOSET_RESTRICT; +"QOSET_TRANS",QOSET_TRANS; "QOSET_TRIVIAL",QOSET_TRIVIAL; "QOSET_num",QOSET_num; "QUANTIFY_SURJECTION_HIGHER_THM",QUANTIFY_SURJECTION_HIGHER_THM; @@ -14089,6 +14254,7 @@ theorems := "RESTRICTION_UNDEFINED",RESTRICTION_UNDEFINED; "RESTRICTION_UNIQUE",RESTRICTION_UNIQUE; "RESTRICTION_UNIQUE_ALT",RESTRICTION_UNIQUE_ALT; +"RESTRICTION_UNIV",RESTRICTION_UNIV; "RETRACTION",RETRACTION; "RETRACTION_ARC",RETRACTION_ARC; "RETRACTION_CLOSEST_POINT",RETRACTION_CLOSEST_POINT; @@ -14590,6 +14756,7 @@ theorems := "SIMPLEX_FURTHEST_LE",SIMPLEX_FURTHEST_LE; "SIMPLEX_FURTHEST_LE_EXISTS",SIMPLEX_FURTHEST_LE_EXISTS; "SIMPLEX_FURTHEST_LT",SIMPLEX_FURTHEST_LT; +"SIMPLEX_FURTHEST_LT_EXISTS",SIMPLEX_FURTHEST_LT_EXISTS; "SIMPLEX_IMP_CLOSED",SIMPLEX_IMP_CLOSED; "SIMPLEX_IMP_COMPACT",SIMPLEX_IMP_COMPACT; "SIMPLEX_IMP_CONVEX",SIMPLEX_IMP_CONVEX; @@ -14744,6 +14911,7 @@ theorems := "SINGULAR_SUBDIVISION_SIMPLICIAL_SIMPLEX",SINGULAR_SUBDIVISION_SIMPLICIAL_SIMPLEX; "SINGULAR_SUBDIVISION_SUB",SINGULAR_SUBDIVISION_SUB; "SINGULAR_SUBDIVISION_ZERO",SINGULAR_SUBDIVISION_ZERO; +"SING_ALT",SING_ALT; "SING_GSPEC",SING_GSPEC; "SING_STRONG_DEFORMATION_RETRACT_OF_AR",SING_STRONG_DEFORMATION_RETRACT_OF_AR; "SING_SUBSET",SING_SUBSET; @@ -15001,6 +15169,11 @@ theorems := "SUBINTERVAL_MEAN_VALUE_THEOREM",SUBINTERVAL_MEAN_VALUE_THEOREM; "SUBINTERVAL_MEAN_VALUE_THEOREM_ALT",SUBINTERVAL_MEAN_VALUE_THEOREM_ALT; "SUBINTERVAL_MEAN_VALUE_THEOREM_SEQ",SUBINTERVAL_MEAN_VALUE_THEOREM_SEQ; +"SUBMATROID",SUBMATROID; +"SUBMATROID_GEN",SUBMATROID_GEN; +"SUBMATROID_SET",SUBMATROID_SET; +"SUBMATROID_SPAN",SUBMATROID_SPAN; +"SUBMATROID_SUBSET",SUBMATROID_SUBSET; "SUBMETRIC",SUBMETRIC; "SUBMETRIC_MSPACE",SUBMETRIC_MSPACE; "SUBMETRIC_PROD_METRIC",SUBMETRIC_PROD_METRIC; @@ -15063,6 +15236,7 @@ theorems := "SUBSET_INTER_ABSORPTION",SUBSET_INTER_ABSORPTION; "SUBSET_LE_DIM",SUBSET_LE_DIM; "SUBSET_LIFT_IMAGE",SUBSET_LIFT_IMAGE; +"SUBSET_MATROID_SPAN",SUBSET_MATROID_SPAN; "SUBSET_NUMSEG",SUBSET_NUMSEG; "SUBSET_OF_FACE_OF",SUBSET_OF_FACE_OF; "SUBSET_OF_FACE_OF_AFFINE_HULL",SUBSET_OF_FACE_OF_AFFINE_HULL; @@ -15893,6 +16067,7 @@ theorems := "UNIONS_CONNECTED_COMPONENTS_OF",UNIONS_CONNECTED_COMPONENTS_OF; "UNIONS_DELETE_EMPTY",UNIONS_DELETE_EMPTY; "UNIONS_DIFF",UNIONS_DIFF; +"UNIONS_EQ_INTERS",UNIONS_EQ_INTERS; "UNIONS_GROUP_ORBITS",UNIONS_GROUP_ORBITS; "UNIONS_GROUP_ORBITS_CLOSED",UNIONS_GROUP_ORBITS_CLOSED; "UNIONS_GROUP_ORBITS_INVARIANT",UNIONS_GROUP_ORBITS_INVARIANT; @@ -15948,6 +16123,7 @@ theorems := "UNIT_INTERVAL_NONEMPTY",UNIT_INTERVAL_NONEMPTY; "UNIV",UNIV; "UNIVERSAL_COVERING_SPACE",UNIVERSAL_COVERING_SPACE; +"UNIV_1",UNIV_1; "UNIV_GSPEC",UNIV_GSPEC; "UNIV_HAS_SIZE_DIMINDEX",UNIV_HAS_SIZE_DIMINDEX; "UNIV_NOT_EMPTY",UNIV_NOT_EMPTY; @@ -16319,6 +16495,7 @@ theorems := "ZIP",ZIP; "ZIP_DEF",ZIP_DEF; "ZL",ZL; +"ZL_STRONG",ZL_STRONG; "ZL_SUBSETS",ZL_SUBSETS; "ZL_SUBSETS_UNIONS",ZL_SUBSETS_UNIONS; "ZL_SUBSETS_UNIONS_NONEMPTY",ZL_SUBSETS_UNIONS_NONEMPTY; @@ -16458,6 +16635,7 @@ theorems := "eq_c",eq_c; "equiintegrable_on",equiintegrable_on; "euclidean",euclidean; +"euclidean_matroid",euclidean_matroid; "euclidean_metric",euclidean_metric; "euclidean_space",euclidean_space; "euclideanreal",euclideanreal; @@ -16693,6 +16871,17 @@ theorems := "matrix_neg",matrix_neg; "matrix_sub",matrix_sub; "matrix_vector_mul",matrix_vector_mul; +"matroid_basis",matroid_basis; +"matroid_dim",matroid_dim; +"matroid_dimension",matroid_dimension; +"matroid_finite_dim",matroid_finite_dim; +"matroid_finite_dimensional",matroid_finite_dimensional; +"matroid_independent",matroid_independent; +"matroid_set",matroid_set; +"matroid_span",matroid_span; +"matroid_spanning",matroid_spanning; +"matroid_subspace",matroid_subspace; +"matroid_tybij",matroid_tybij; "mball",mball; "mbasis",mbasis; "mbounded",mbounded; @@ -16939,6 +17128,7 @@ theorems := "string_INFINITE",string_INFINITE; "subgroup_generated",subgroup_generated; "subgroup_of",subgroup_of; +"submatroid",submatroid; "submetric",submetric; "subpath",subpath; "subspace",subspace; diff --git a/Multivariate/vectors.ml b/Multivariate/vectors.ml index 93672985..b54a81bc 100644 --- a/Multivariate/vectors.ml +++ b/Multivariate/vectors.ml @@ -6,6 +6,7 @@ (* (c) Copyright, Andrea Gabrielli, Marco Maggesi 2016-2017 *) (* ========================================================================= *) +needs "Library/matroids.ml";; needs "Multivariate/misc.ml";; (* ------------------------------------------------------------------------- *) @@ -5072,21 +5073,6 @@ let EQ_SPAN_INSERT_EQ = prove VECTOR_ARITH `(z - k % y) - k % (x - y) = z - k % x`; VECTOR_ARITH `(z - k % x) + k % (x - y) = z - k % y`]);; -(* ------------------------------------------------------------------------- *) -(* Transitivity property. *) -(* ------------------------------------------------------------------------- *) - -let SPAN_TRANS = prove - (`!x y:real^N s. x IN span(s) /\ y IN span(x INSERT s) ==> y IN span(s)`, - REPEAT STRIP_TAC THEN - MP_TAC(SPECL [`x:real^N`; `(x:real^N) INSERT s`; `y:real^N`] - SPAN_BREAKDOWN) THEN - ASM_REWRITE_TAC[IN_INSERT] THEN - DISCH_THEN(X_CHOOSE_THEN `k:real` STRIP_ASSUME_TAC) THEN - SUBST1_TAC(VECTOR_ARITH `y:real^N = (y - k % x) + k % x`) THEN - MATCH_MP_TAC SPAN_ADD THEN ASM_SIMP_TAC[SPAN_MUL] THEN - ASM_MESON_TAC[SPAN_MONO; SUBSET; IN_INSERT; IN_DELETE]);; - (* ------------------------------------------------------------------------- *) (* An explicit expansion is sometimes needed. *) (* ------------------------------------------------------------------------- *) @@ -5280,123 +5266,123 @@ let INDEPENDENT_BASIS_IMAGE = prove ASM_REWRITE_TAC[GSYM numseg]]);; (* ------------------------------------------------------------------------- *) -(* This is useful for building a basis step-by-step. *) +(* Definition of dimension, and setup of matroid for Euclidean span. *) (* ------------------------------------------------------------------------- *) +let dim = new_definition + `dim (v:real^N->bool) = + @n. ?b. b SUBSET v /\ independent b /\ v SUBSET (span b) /\ b HAS_SIZE n`;; + +let euclidean_matroid = new_definition + `euclidean_matroid = matroid((:real^N),span)`;; + +let EUCLIDEAN_MATROID = prove + (`matroid_set euclidean_matroid = (:real^N) /\ + matroid_span euclidean_matroid = (span:(real^N->bool)->(real^N->bool))`, + ONCE_REWRITE_TAC[matroid_set; matroid_span] THEN + REWRITE_TAC[GSYM PAIR_EQ; euclidean_matroid] THEN + REWRITE_TAC[GSYM(CONJUNCT2 matroid_tybij)] THEN + REWRITE_TAC[SUBSET_UNIV; IN_UNIV] THEN + REWRITE_TAC[SPAN_INC; SPAN_MONO; SPAN_SPAN; IN_SPAN_INSERT] THEN + REPEAT GEN_TAC THEN + GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [SPAN_EXPLICIT] THEN + REWRITE_TAC[IN_ELIM_THM] THEN MATCH_MP_TAC MONO_EXISTS THEN + SIMP_TAC[SPAN_FINITE; LEFT_IMP_EXISTS_THM; IN_ELIM_THM] THEN + MESON_TAC[]);; + +let EUCLIDEAN_MATROID_INDEPENDENT = prove + (`matroid_independent (euclidean_matroid:(real^N)matroid) = independent`, + SIMP_TAC[independent; dependent; matroid_independent; FUN_EQ_THM] THEN + REWRITE_TAC[EUCLIDEAN_MATROID; SUBSET_UNIV] THEN MESON_TAC[]);; + +let EUCLIDEAN_MATROID_SPANNING = prove + (`!s. matroid_spanning euclidean_matroid s <=> span s = (:real^N)`, + REWRITE_TAC[matroid_spanning; EUCLIDEAN_MATROID; SUBSET_UNIV]);; + +let EUCLIDEAN_MATROID_SUBSPACE = prove + (`matroid_subspace (euclidean_matroid:(real^N)matroid) = subspace`, + GEN_REWRITE_TAC I [FUN_EQ_THM] THEN + REWRITE_TAC[matroid_subspace; EUCLIDEAN_MATROID; SUBSET_UNIV] THEN + REWRITE_TAC[SPAN_EQ_SELF]);; + +let EUCLIDEAN_MATROID_FINITE_DIMENSIONAL = prove + (`matroid_finite_dimensional (euclidean_matroid:(real^N)matroid)`, + REWRITE_TAC[MATROID_FINITE_DIMENSIONAL; EUCLIDEAN_MATROID] THEN + EXISTS_TAC `{basis i :real^N | 1 <= i /\ i <= dimindex(:N)}` THEN + REWRITE_TAC[SPAN_STDBASIS; SUBSET_UNIV; FINITE_STDBASIS]);; + +let EUCLIDEAN_MATROID_DIMENSION = prove + (`matroid_dimension (euclidean_matroid:(real^N)matroid) = dimindex(:N)`, + MATCH_MP_TAC MATROID_DIMENSION_UNIQUE THEN + EXISTS_TAC `{basis i :real^N | 1 <= i /\ i <= dimindex(:N)}` THEN + REWRITE_TAC[matroid_basis; EUCLIDEAN_MATROID_INDEPENDENT; SPAN_STDBASIS; + EUCLIDEAN_MATROID_SPANNING; INDEPENDENT_STDBASIS; HAS_SIZE_STDBASIS]);; + +let EUCLIDEAN_MATROID_FINITE_DIM = prove + (`!s:real^N->bool. matroid_finite_dim euclidean_matroid s`, + GEN_TAC THEN MATCH_MP_TAC MATROID_FINITE_DIMENSIONAL_DIM THEN + REWRITE_TAC[EUCLIDEAN_MATROID_FINITE_DIMENSIONAL] THEN + REWRITE_TAC[EUCLIDEAN_MATROID; SUBSET_UNIV]);; + +let EUCLIDEAN_SUBMATROID = prove + (`(!s:real^N->bool. matroid_set (submatroid euclidean_matroid s) = span s) /\ + (!s:real^N->bool. matroid_span (submatroid euclidean_matroid s) = span)`, + SIMP_TAC[SUBMATROID_SUBSET; EUCLIDEAN_MATROID; SUBSET_UNIV]);; + +let EUCLIDEAN_MATROID_DIM = prove + (`matroid_dim (euclidean_matroid:(real^N)matroid) = dim`, + REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `s:real^N->bool` THEN + REWRITE_TAC[dim] THEN + SIMP_TAC[MATROID_DIM_ALT; EUCLIDEAN_MATROID; SUBSET_UNIV] THEN + REWRITE_TAC[EUCLIDEAN_MATROID_INDEPENDENT]);; + +(* ------------------------------------------------------------------------- *) +(* Some linear algebra basics, leaning on matroids in many cases *) +(* ------------------------------------------------------------------------- *) + +let SPAN_EQ = prove + (`!s t:real^N->bool. span s = span t <=> s SUBSET span t /\ t SUBSET span s`, + REPEAT GEN_TAC THEN MP_TAC(ISPECL + [`euclidean_matroid:(real^N)matroid`; `s:real^N->bool`; `t:real^N->bool`] + MATROID_SPAN_EQ) THEN + REWRITE_TAC[EUCLIDEAN_MATROID; IN_UNIV; SUBSET_UNIV]);; + +let SPAN_EQ_INSERT = prove + (`!s x:real^N. span(x INSERT s) = span s <=> x IN span s`, + REPEAT GEN_TAC THEN MP_TAC(ISPECL + [`euclidean_matroid:(real^N)matroid`; `s:real^N->bool`; `x:real^N`] + MATROID_SPAN_INSERT_EQ) THEN + REWRITE_TAC[EUCLIDEAN_MATROID; IN_UNIV; SUBSET_UNIV]);; + let INDEPENDENT_INSERT = prove (`!a:real^N s. independent(a INSERT s) <=> if a IN s then independent s else independent s /\ ~(a IN span s)`, - REPEAT GEN_TAC THEN ASM_CASES_TAC `(a:real^N) IN s` THEN - ASM_SIMP_TAC[SET_RULE `x IN s ==> (x INSERT s = s)`] THEN - EQ_TAC THENL - [DISCH_TAC THEN CONJ_TAC THENL - [ASM_MESON_TAC[INDEPENDENT_MONO; SUBSET; IN_INSERT]; - POP_ASSUM MP_TAC THEN REWRITE_TAC[independent; dependent] THEN - ASM_MESON_TAC[IN_INSERT; SET_RULE - `~(a IN s) ==> ((a INSERT s) DELETE a = s)`]]; - ALL_TAC] THEN - REWRITE_TAC[independent; dependent; NOT_EXISTS_THM] THEN - STRIP_TAC THEN X_GEN_TAC `b:real^N` THEN - REWRITE_TAC[IN_INSERT] THEN ASM_CASES_TAC `b:real^N = a` THEN - ASM_SIMP_TAC[SET_RULE `~(a IN s) ==> ((a INSERT s) DELETE a = s)`] THEN - ASM_SIMP_TAC[SET_RULE - `~(a IN s) /\ ~(b = a) - ==> ((a INSERT s) DELETE b = a INSERT (s DELETE b))`] THEN - ASM_MESON_TAC[IN_SPAN_INSERT; SET_RULE - `b IN s ==> (b INSERT (s DELETE b) = s)`]);; + MESON_TAC[EUCLIDEAN_MATROID; EUCLIDEAN_MATROID_INDEPENDENT; + MATROID_INDEPENDENT_INSERT; IN_UNIV]);; -(* ------------------------------------------------------------------------- *) -(* The degenerate case of the Exchange Lemma. *) -(* ------------------------------------------------------------------------- *) +let SPAN_TRANS = prove + (`!x y:real^N s. x IN span(s) /\ y IN span(x INSERT s) ==> y IN span(s)`, + REWRITE_TAC[GSYM EUCLIDEAN_MATROID] THEN + MESON_TAC[MATROID_SPAN_INSERT_EQ; EUCLIDEAN_MATROID; IN_UNIV; SUBSET_UNIV]);; let SPANNING_SUBSET_INDEPENDENT = prove (`!s t:real^N->bool. - t SUBSET s /\ independent s /\ s SUBSET span(t) ==> (s = t)`, - REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN - ASM_REWRITE_TAC[] THEN REWRITE_TAC[SUBSET] THEN - X_GEN_TAC `a:real^N` THEN DISCH_TAC THEN - FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [independent]) THEN - REWRITE_TAC[dependent; NOT_EXISTS_THM] THEN - DISCH_THEN(MP_TAC o SPEC `a:real^N`) THEN ASM_REWRITE_TAC[] THEN - ASM_MESON_TAC[SPAN_MONO; SUBSET; IN_DELETE]);; - -(* ------------------------------------------------------------------------- *) -(* The general case of the Exchange Lemma, the key to what follows. *) -(* ------------------------------------------------------------------------- *) + t SUBSET s /\ independent s /\ s SUBSET span(t) ==> s = t`, + MP_TAC(ISPEC `euclidean_matroid:(real^N)matroid` + MATROID_SPANNING_SUBSET_INDEPENDENT) THEN + REWRITE_TAC[EUCLIDEAN_MATROID; EUCLIDEAN_MATROID_INDEPENDENT]);; let EXCHANGE_LEMMA = prove (`!s t:real^N->bool. FINITE t /\ independent s /\ s SUBSET span t ==> ?t'. t' HAS_SIZE (CARD t) /\ s SUBSET t' /\ t' SUBSET (s UNION t) /\ s SUBSET (span t')`, - REPEAT GEN_TAC THEN - WF_INDUCT_TAC `CARD(t DIFF s :real^N->bool)` THEN - ASM_CASES_TAC `(s:real^N->bool) SUBSET t` THENL - [ASM_MESON_TAC[HAS_SIZE; SUBSET_UNION]; ALL_TAC] THEN - ASM_CASES_TAC `t SUBSET (s:real^N->bool)` THENL - [ASM_MESON_TAC[SPANNING_SUBSET_INDEPENDENT; HAS_SIZE]; ALL_TAC] THEN - STRIP_TAC THEN - FIRST_X_ASSUM(MP_TAC o REWRITE_RULE[SUBSET] o check(is_neg o concl)) THEN - REWRITE_TAC[NOT_FORALL_THM; NOT_IMP] THEN - DISCH_THEN(X_CHOOSE_THEN `b:real^N` STRIP_ASSUME_TAC) THEN - ASM_CASES_TAC `s SUBSET span(t DELETE (b:real^N))` THENL - [FIRST_X_ASSUM(MP_TAC o - SPECL [`t DELETE (b:real^N)`; `s:real^N->bool`]) THEN - ASM_REWRITE_TAC[SET_RULE `s DELETE a DIFF t = (s DIFF t) DELETE a`] THEN - ASM_SIMP_TAC[CARD_DELETE; FINITE_DIFF; IN_DIFF; FINITE_DELETE; - CARD_EQ_0; ARITH_RULE `n - 1 < n <=> ~(n = 0)`] THEN - ANTS_TAC THENL - [UNDISCH_TAC `~((s:real^N->bool) SUBSET t)` THEN ASM SET_TAC[]; - ALL_TAC] THEN - DISCH_THEN(X_CHOOSE_THEN `u:real^N->bool` STRIP_ASSUME_TAC) THEN - EXISTS_TAC `(b:real^N) INSERT u` THEN - ASM_SIMP_TAC[SUBSET_INSERT; INSERT_SUBSET; IN_UNION] THEN CONJ_TAC THENL - [UNDISCH_TAC `(u:real^N->bool) HAS_SIZE CARD(t:real^N->bool) - 1` THEN - SIMP_TAC[HAS_SIZE; FINITE_RULES; CARD_CLAUSES] THEN STRIP_TAC THEN - COND_CASES_TAC THENL - [ASM_MESON_TAC[SUBSET; IN_UNION; IN_DELETE]; ALL_TAC] THEN - ASM_MESON_TAC[ARITH_RULE `~(n = 0) ==> (SUC(n - 1) = n)`; - CARD_EQ_0; MEMBER_NOT_EMPTY]; - ALL_TAC] THEN - CONJ_TAC THENL - [UNDISCH_TAC `u SUBSET s UNION t DELETE (b:real^N)` THEN SET_TAC[]; - ASM_MESON_TAC[SUBSET; SPAN_MONO; IN_INSERT]]; - ALL_TAC] THEN - UNDISCH_TAC `~(s SUBSET span (t DELETE (b:real^N)))` THEN - GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [SUBSET] THEN - REWRITE_TAC[NOT_FORALL_THM; NOT_IMP] THEN - DISCH_THEN(X_CHOOSE_THEN `a:real^N` STRIP_ASSUME_TAC) THEN - SUBGOAL_THEN `~(a:real^N = b)` ASSUME_TAC THENL - [ASM_MESON_TAC[]; ALL_TAC] THEN - SUBGOAL_THEN `~((a:real^N) IN t)` ASSUME_TAC THENL - [ASM_MESON_TAC[IN_DELETE; SPAN_CLAUSES]; ALL_TAC] THEN - FIRST_X_ASSUM(MP_TAC o SPECL - [`(a:real^N) INSERT (t DELETE b)`; `s:real^N->bool`]) THEN - ANTS_TAC THENL - [ASM_SIMP_TAC[SET_RULE - `a IN s ==> ((a INSERT (t DELETE b) DIFF s) = (t DIFF s) DELETE b)`] THEN - ASM_SIMP_TAC[CARD_DELETE; FINITE_DELETE; FINITE_DIFF; IN_DIFF] THEN - ASM_SIMP_TAC[ARITH_RULE `n - 1 < n <=> ~(n = 0)`; CARD_EQ_0; - FINITE_DIFF] THEN - UNDISCH_TAC `~((s:real^N->bool) SUBSET t)` THEN ASM SET_TAC[]; - ALL_TAC] THEN - ANTS_TAC THENL - [ASM_SIMP_TAC[FINITE_RULES; FINITE_DELETE] THEN - REWRITE_TAC[SUBSET] THEN X_GEN_TAC `x:real^N` THEN - DISCH_TAC THEN MATCH_MP_TAC SPAN_TRANS THEN EXISTS_TAC `b:real^N` THEN - ASM_MESON_TAC[IN_SPAN_DELETE; SUBSET; SPAN_MONO; - SET_RULE `t SUBSET (b INSERT (a INSERT (t DELETE b)))`]; - ALL_TAC] THEN - MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `u:real^N->bool` THEN - ASM_SIMP_TAC[HAS_SIZE; CARD_CLAUSES; CARD_DELETE; FINITE_DELETE; IN_DELETE; - ARITH_RULE `(SUC(n - 1) = n) <=> ~(n = 0)`; - CARD_EQ_0] THEN - UNDISCH_TAC `(b:real^N) IN t` THEN ASM SET_TAC[]);; - -(* ------------------------------------------------------------------------- *) -(* This implies corresponding size bounds. *) -(* ------------------------------------------------------------------------- *) + REPEAT STRIP_TAC THEN MP_TAC(ISPECL + [`euclidean_matroid:(real^N)matroid`; `s:real^N->bool`; `t:real^N->bool`] + MATROID_STEINITZ_EXCHANGE_FINITE) THEN + ASM_REWRITE_TAC[EUCLIDEAN_MATROID; EUCLIDEAN_MATROID_INDEPENDENT] THEN + REWRITE_TAC[SUBSET_UNIV] THEN MATCH_MP_TAC MONO_EXISTS THEN ASM_MESON_TAC[]);; let INDEPENDENT_SPAN_BOUND = prove (`!s t. FINITE t /\ independent s /\ s SUBSET span(t) @@ -5422,130 +5408,25 @@ let INDEPENDENT_IMP_FINITE = prove (`!s:real^N->bool. independent s ==> FINITE s`, SIMP_TAC[INDEPENDENT_BOUND]);; -(* ------------------------------------------------------------------------- *) -(* Explicit formulation of independence. *) -(* ------------------------------------------------------------------------- *) - -let INDEPENDENT_EXPLICIT = prove - (`!b:real^N->bool. - independent b <=> - FINITE b /\ - !c. vsum b (\v. c(v) % v) = vec 0 ==> !v. v IN b ==> c(v) = &0`, - GEN_TAC THEN - ASM_CASES_TAC `FINITE(b:real^N->bool)` THENL - [ALL_TAC; ASM_MESON_TAC[INDEPENDENT_BOUND]] THEN - ASM_SIMP_TAC[independent; DEPENDENT_FINITE] THEN MESON_TAC[]);; - -let INDEPENDENT_SING = prove - (`!x. independent {x} <=> ~(x = vec 0)`, - REWRITE_TAC[INDEPENDENT_INSERT; NOT_IN_EMPTY; SPAN_EMPTY] THEN - REWRITE_TAC[INDEPENDENT_EMPTY] THEN SET_TAC[]);; - -let DEPENDENT_SING = prove - (`!x. dependent {x} <=> x = vec 0`, - MESON_TAC[independent; INDEPENDENT_SING]);; - -let DEPENDENT_2 = prove - (`!a b:real^N. - dependent {a,b} <=> - if a = b then a = vec 0 - else ?x y. x % a + y % b = vec 0 /\ ~(x = &0 /\ y = &0)`, - REPEAT STRIP_TAC THEN COND_CASES_TAC THEN - ASM_REWRITE_TAC[DEPENDENT_SING; SET_RULE `{x,x} = {x}`] THEN - SIMP_TAC[DEPENDENT_FINITE; VSUM_CLAUSES; FINITE_INSERT; FINITE_EMPTY] THEN - ASM_REWRITE_TAC[IN_SING; NOT_IN_EMPTY; VECTOR_ADD_RID; EXISTS_IN_INSERT] THEN - EQ_TAC THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THENL - [X_GEN_TAC `u:real^N->real` THEN STRIP_TAC THEN - MAP_EVERY EXISTS_TAC [`(u:real^N->real) a`; `(u:real^N->real) b`] THEN - ASM_REWRITE_TAC[]; - MAP_EVERY X_GEN_TAC [`x:real`; `y:real`] THEN DISCH_TAC THEN EXISTS_TAC - `\v:real^N. if v = a then x else if v = b then y else z:real` THEN - ASM_MESON_TAC[]]);; - -let DEPENDENT_3 = prove - (`!a b c:real^N. - ~(a = b) /\ ~(a = c) /\ ~(b = c) - ==> (dependent {a,b,c} <=> - ?x y z. x % a + y % b + z % c = vec 0 /\ - ~(x = &0 /\ y = &0 /\ z = &0))`, - REPEAT STRIP_TAC THEN - SIMP_TAC[DEPENDENT_FINITE; VSUM_CLAUSES; FINITE_INSERT; FINITE_EMPTY] THEN - ASM_REWRITE_TAC[IN_SING; NOT_IN_EMPTY; VECTOR_ADD_RID; IN_INSERT] THEN - EQ_TAC THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THENL - [X_GEN_TAC `u:real^N->real` THEN STRIP_TAC THEN MAP_EVERY EXISTS_TAC - [`(u:real^N->real) a`; `(u:real^N->real) b`; `(u:real^N->real) c`]; - MAP_EVERY X_GEN_TAC [`x:real`; `y:real`; `z:real`] THEN DISCH_TAC THEN - EXISTS_TAC - `\v:real^N. if v = a then x else if v = b then y else z:real`] THEN - ASM_MESON_TAC[]);; - -let INDEPENDENT_2 = prove - (`!a b:real^N x y. - independent{a,b} /\ ~(a = b) - ==> (x % a + y % b = vec 0 <=> x = &0 /\ y = &0)`, - SIMP_TAC[IMP_CONJ_ALT; independent; DEPENDENT_2] THEN - MESON_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID]);; - -let INDEPENDENT_3 = prove - (`!a b c:real^N x y z. - independent{a,b,c} /\ ~(a = b) /\ ~(a = c) /\ ~(b = c) - ==> (x % a + y % b + z % c = vec 0 <=> x = &0 /\ y = &0 /\ z = &0)`, - SIMP_TAC[IMP_CONJ_ALT; independent; DEPENDENT_3] THEN - MESON_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID]);; - -(* ------------------------------------------------------------------------- *) -(* Hence we can create a maximal independent subset. *) -(* ------------------------------------------------------------------------- *) - let MAXIMAL_INDEPENDENT_SUBSET_EXTEND = prove (`!s v:real^N->bool. s SUBSET v /\ independent s ==> ?b. s SUBSET b /\ b SUBSET v /\ independent b /\ v SUBSET (span b)`, - REPEAT GEN_TAC THEN - WF_INDUCT_TAC `dimindex(:N) - CARD(s:real^N->bool)` THEN - REPEAT STRIP_TAC THEN - ASM_CASES_TAC `v SUBSET (span(s:real^N->bool))` THENL - [ASM_MESON_TAC[SUBSET_REFL]; ALL_TAC] THEN - FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [SUBSET]) THEN - REWRITE_TAC[NOT_FORALL_THM; NOT_IMP] THEN - DISCH_THEN(X_CHOOSE_THEN `a:real^N` STRIP_ASSUME_TAC) THEN - FIRST_X_ASSUM(MP_TAC o SPEC `(a:real^N) INSERT s`) THEN - REWRITE_TAC[IMP_IMP] THEN ANTS_TAC THENL - [ALL_TAC; MESON_TAC[INSERT_SUBSET]] THEN - SUBGOAL_THEN `independent ((a:real^N) INSERT s)` ASSUME_TAC THENL - [ASM_REWRITE_TAC[INDEPENDENT_INSERT; COND_ID]; ALL_TAC] THEN - ASM_REWRITE_TAC[INSERT_SUBSET] THEN - MATCH_MP_TAC(ARITH_RULE `(b = a + 1) /\ b <= n ==> n - b < n - a`) THEN - ASM_SIMP_TAC[CARD_CLAUSES; INDEPENDENT_BOUND] THEN - ASM_MESON_TAC[SPAN_SUPERSET; ADD1]);; + REPEAT STRIP_TAC THEN MP_TAC(ISPECL + [`submatroid euclidean_matroid (v:real^N->bool)`; + `s:real^N->bool`; `v:real^N->bool`] MATROID_INTERMEDIATE_BASIS) THEN + ASM_SIMP_TAC[MATROID_INDEPENDENT_SUBMATROID; EUCLIDEAN_MATROID; SUBSET_UNIV; + MATROID_SPANNING_SUBMATROID; EUCLIDEAN_MATROID_INDEPENDENT; + MATROID_BASIS_SUBMATROID; + SET_RULE `s SUBSET v ==> s UNION v = v`] THEN + ASM_MESON_TAC[SPAN_INC; SUBSET_TRANS]);; let MAXIMAL_INDEPENDENT_SUBSET = prove (`!v:real^N->bool. ?b. b SUBSET v /\ independent b /\ v SUBSET (span b)`, MP_TAC(SPEC `EMPTY:real^N->bool` MAXIMAL_INDEPENDENT_SUBSET_EXTEND) THEN REWRITE_TAC[EMPTY_SUBSET; INDEPENDENT_EMPTY]);; -(* ------------------------------------------------------------------------- *) -(* A kind of closed graph property for linearity. *) -(* ------------------------------------------------------------------------- *) - -let LINEAR_SUBSPACE_GRAPH = prove - (`!f:real^M->real^N. - linear f <=> subspace {pastecart x (f x) | x IN (:real^M)}`, - REWRITE_TAC[linear; subspace; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN - REWRITE_TAC[FORALL_IN_GSPEC; GSYM(SPEC `0` PASTECART_VEC); IN_UNIV] THEN - REWRITE_TAC[IN_ELIM_THM; PASTECART_INJ; UNWIND_THM1; PASTECART_ADD; - GSYM PASTECART_CMUL] THEN - MESON_TAC[VECTOR_MUL_LZERO]);; - -(* ------------------------------------------------------------------------- *) -(* Notion of dimension. *) -(* ------------------------------------------------------------------------- *) - -let dim = new_definition - `dim v = @n. ?b. b SUBSET v /\ independent b /\ v SUBSET (span b) /\ - b HAS_SIZE n`;; - let BASIS_EXISTS = prove (`!v. ?b. b SUBSET v /\ independent b /\ v SUBSET (span b) /\ b HAS_SIZE (dim v)`, @@ -5574,10 +5455,6 @@ let BASIS_SUBSPACE_EXISTS = prove ASM_REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ] THEN ASM_MESON_TAC[SPAN_EQ_SELF; SPAN_MONO; INDEPENDENT_IMP_FINITE]);; -(* ------------------------------------------------------------------------- *) -(* Consequences of independence or spanning for cardinality. *) -(* ------------------------------------------------------------------------- *) - let INDEPENDENT_CARD_LE_DIM = prove (`!v b:real^N->bool. b SUBSET v /\ independent b ==> FINITE b /\ CARD(b) <= dim v`, @@ -5599,9 +5476,16 @@ let BASIS_HAS_SIZE_DIM = prove MATCH_MP_TAC BASIS_CARD_EQ_DIM THEN ASM_REWRITE_TAC[SUBSET_REFL] THEN FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[SPAN_INC]);; +let DIM_SPAN = prove + (`!s:real^N->bool. dim(span s) = dim s`, + GEN_TAC THEN MP_TAC(ISPECL + [`euclidean_matroid:(real^N)matroid`; `s:real^N->bool`] + MATROID_DIM_SPAN) THEN + SIMP_TAC[EUCLIDEAN_MATROID_DIM; EUCLIDEAN_MATROID; SUBSET_UNIV]);; + let DIM_UNIQUE = prove (`!v b. b SUBSET v /\ v SUBSET (span b) /\ independent b /\ b HAS_SIZE n - ==> (dim v = n)`, + ==> dim v = n`, MESON_TAC[BASIS_CARD_EQ_DIM; HAS_SIZE]);; let DIM_LE_CARD = prove @@ -5609,10 +5493,6 @@ let DIM_LE_CARD = prove GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC SPAN_CARD_GE_DIM THEN ASM_REWRITE_TAC[SPAN_INC; SUBSET_REFL]);; -(* ------------------------------------------------------------------------- *) -(* More lemmas about dimension. *) -(* ------------------------------------------------------------------------- *) - let DIM_UNIV = prove (`dim(:real^N) = dimindex(:N)`, MATCH_MP_TAC DIM_UNIQUE THEN @@ -5633,42 +5513,29 @@ let BASIS_HAS_SIZE_UNIV = prove (`!b. independent b /\ span b = (:real^N) ==> b HAS_SIZE (dimindex(:N))`, REWRITE_TAC[GSYM DIM_UNIV; BASIS_HAS_SIZE_DIM]);; -(* ------------------------------------------------------------------------- *) -(* Converses to those. *) -(* ------------------------------------------------------------------------- *) - let CARD_GE_DIM_INDEPENDENT = prove (`!v b:real^N->bool. b SUBSET v /\ independent b /\ dim v <= CARD(b) - ==> v SUBSET (span b)`, - REPEAT STRIP_TAC THEN - SUBGOAL_THEN `!a:real^N. ~(a IN v /\ ~(a IN span b))` MP_TAC THENL - [ALL_TAC; SET_TAC[]] THEN - X_GEN_TAC `a:real^N` THEN STRIP_TAC THEN - SUBGOAL_THEN `independent((a:real^N) INSERT b)` ASSUME_TAC THENL - [ASM_MESON_TAC[INDEPENDENT_INSERT]; ALL_TAC] THEN - MP_TAC(ISPECL [`v:real^N->bool`; `(a:real^N) INSERT b`] - INDEPENDENT_CARD_LE_DIM) THEN - ASM_SIMP_TAC[INSERT_SUBSET; CARD_CLAUSES; INDEPENDENT_BOUND] THEN - ASM_MESON_TAC[SPAN_SUPERSET; SUBSET; ARITH_RULE - `x <= y ==> ~(SUC y <= x)`]);; + ==> v SUBSET span b`, + REPEAT STRIP_TAC THEN MP_TAC(ISPECL + [`euclidean_matroid:(real^N)matroid`; `b:real^N->bool`; `v:real^N->bool`] + MATROID_DIM_SPAN_EQ_GEN) THEN + MP_TAC(ISPECL [`euclidean_matroid:(real^N)matroid`; `b:real^N->bool`] + MATROID_DIM_GE_FINITE_CARD_EQ) THEN + ASM_REWRITE_TAC[EUCLIDEAN_MATROID; EUCLIDEAN_MATROID_DIM; SUBSET_UNIV; + EUCLIDEAN_MATROID_FINITE_DIM; EUCLIDEAN_MATROID_INDEPENDENT] THEN + ASM_MESON_TAC[SPAN_INC; LE_TRANS; SPAN_MONO]);; let CARD_LE_DIM_SPANNING = prove (`!v b:real^N->bool. - v SUBSET (span b) /\ FINITE b /\ CARD(b) <= dim v - ==> independent b`, - REPEAT STRIP_TAC THEN REWRITE_TAC[independent; dependent] THEN - DISCH_THEN(X_CHOOSE_THEN `a:real^N` STRIP_ASSUME_TAC) THEN - SUBGOAL_THEN `dim(v:real^N->bool) <= CARD(b DELETE (a:real^N))` MP_TAC THENL - [ALL_TAC; - ASM_SIMP_TAC[CARD_DELETE] THEN MATCH_MP_TAC - (ARITH_RULE `b <= n /\ ~(b = 0) ==> ~(n <= b - 1)`) THEN - ASM_SIMP_TAC[CARD_EQ_0] THEN ASM_MESON_TAC[MEMBER_NOT_EMPTY]] THEN - MATCH_MP_TAC SPAN_CARD_GE_DIM THEN ASM_SIMP_TAC[FINITE_DELETE] THEN - REWRITE_TAC[SUBSET] THEN REPEAT STRIP_TAC THEN - MATCH_MP_TAC SPAN_TRANS THEN EXISTS_TAC `a:real^N` THEN - ASM_SIMP_TAC[SET_RULE `a IN b ==> (a INSERT (b DELETE a) = b)`] THEN - ASM_MESON_TAC[SUBSET]);; + v SUBSET span b /\ FINITE b /\ CARD(b) <= dim v ==> independent b`, + REPEAT STRIP_TAC THEN + MP_TAC(ISPECL [`euclidean_matroid:(real^N)matroid`; `b:real^N->bool`] + MATROID_DIM_GE_FINITE_CARD_EQ) THEN + REWRITE_TAC[EUCLIDEAN_MATROID; EUCLIDEAN_MATROID_DIM; SUBSET_UNIV; + EUCLIDEAN_MATROID_INDEPENDENT; EUCLIDEAN_MATROID_FINITE_DIM] THEN + DISCH_THEN(SUBST1_TAC o SYM) THEN + ASM_MESON_TAC[DIM_SPAN; SPAN_SPAN; DIM_SUBSET; LE_TRANS]);; let CARD_EQ_DIM = prove (`!v b. b SUBSET v /\ b HAS_SIZE (dim v) @@ -5676,10 +5543,6 @@ let CARD_EQ_DIM = prove REWRITE_TAC[HAS_SIZE; GSYM LE_ANTISYM] THEN MESON_TAC[CARD_LE_DIM_SPANNING; CARD_GE_DIM_INDEPENDENT]);; -(* ------------------------------------------------------------------------- *) -(* More general size bound lemmas. *) -(* ------------------------------------------------------------------------- *) - let INDEPENDENT_BOUND_GENERAL = prove (`!s:real^N->bool. independent s ==> FINITE s /\ CARD(s) <= dim(s)`, MESON_TAC[INDEPENDENT_CARD_LE_DIM; INDEPENDENT_BOUND; SUBSET_REFL]);; @@ -5689,18 +5552,6 @@ let DEPENDENT_BIGGERSET_GENERAL = prove MP_TAC INDEPENDENT_BOUND_GENERAL THEN MATCH_MP_TAC MONO_FORALL THEN REWRITE_TAC[GT; GSYM NOT_LE; independent] THEN MESON_TAC[]);; -let DIM_SPAN = prove - (`!s:real^N->bool. dim(span s) = dim s`, - GEN_TAC THEN REWRITE_TAC[GSYM LE_ANTISYM] THEN CONJ_TAC THENL - [ALL_TAC; - MATCH_MP_TAC DIM_SUBSET THEN MESON_TAC[SUBSET; SPAN_SUPERSET]] THEN - MP_TAC(ISPEC `s:real^N->bool` BASIS_EXISTS) THEN - REWRITE_TAC[HAS_SIZE] THEN STRIP_TAC THEN - FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN - MATCH_MP_TAC SPAN_CARD_GE_DIM THEN ASM_REWRITE_TAC[] THEN - GEN_REWRITE_TAC RAND_CONV [GSYM SPAN_SPAN] THEN - MATCH_MP_TAC SPAN_MONO THEN ASM_REWRITE_TAC[]);; - let DIM_INSERT_0 = prove (`!s:real^N->bool. dim(vec 0 INSERT s) = dim s`, ONCE_REWRITE_TAC[GSYM DIM_SPAN] THEN @@ -5736,6 +5587,160 @@ let SPAN_EQ_DIM = prove (`!s t. span s = span t ==> dim s = dim t`, MESON_TAC[DIM_SPAN]);; +let DIM_EMPTY = prove + (`dim({}:real^N->bool) = 0`, + REWRITE_TAC[GSYM EUCLIDEAN_MATROID_DIM; MATROID_DIM_EMPTY]);; + +let DIM_INSERT = prove + (`!x:real^N s. dim(x INSERT s) = if x IN span s then dim s else dim s + 1`, + REWRITE_TAC[GSYM EUCLIDEAN_MATROID_DIM] THEN + SIMP_TAC[MATROID_DIM_INSERT; EUCLIDEAN_MATROID_FINITE_DIM; EUCLIDEAN_MATROID; + IN_UNIV]);; + +let CHOOSE_SUBSPACE_OF_SUBSPACE = prove + (`!s:real^N->bool n. + n <= dim s ==> ?t. subspace t /\ t SUBSET span s /\ dim t = n`, + REPEAT STRIP_TAC THEN MP_TAC(ISPECL + [`euclidean_matroid:(real^N)matroid`; `s:real^N->bool`; `n:num`] + MATROID_CHOOSE_SUBSPACE) THEN + ASM_REWRITE_TAC[EUCLIDEAN_MATROID; SUBSET_UNIV; EUCLIDEAN_MATROID_DIM; + EUCLIDEAN_MATROID_SUBSPACE] THEN + MESON_TAC[]);; + +let SUBSPACE_EXISTS = prove + (`!n. n <= dimindex(:N) ==> ?s:real^N->bool. subspace s /\ dim s = n`, + REPEAT GEN_TAC THEN REWRITE_TAC[GSYM DIM_UNIV] THEN + DISCH_THEN(MP_TAC o MATCH_MP CHOOSE_SUBSPACE_OF_SUBSPACE) THEN + MESON_TAC[]);; + +let DIM_EQ_SPAN = prove + (`!s t:real^N->bool. s SUBSET t /\ dim t <= dim s ==> span s = span t`, + REPEAT STRIP_TAC THEN + MP_TAC(ISPECL + [`euclidean_matroid:(real^N)matroid`; `s:real^N->bool`; `t:real^N->bool`] + MATROID_DIM_EQ_SPAN) THEN + ASM_REWRITE_TAC[EUCLIDEAN_MATROID; EUCLIDEAN_MATROID_FINITE_DIM; + EUCLIDEAN_MATROID_DIM; SUBSET_UNIV]);; + +let DIM_EQ_FULL = prove + (`!s:real^N->bool. dim s = dimindex(:N) <=> span s = (:real^N)`, + GEN_TAC THEN ONCE_REWRITE_TAC[GSYM DIM_SPAN] THEN EQ_TAC THEN + SIMP_TAC[DIM_UNIV] THEN DISCH_TAC THEN + GEN_REWRITE_TAC RAND_CONV [GSYM SPAN_UNIV] THEN MATCH_MP_TAC DIM_EQ_SPAN THEN + ASM_REWRITE_TAC[SUBSET_UNIV; DIM_UNIV] THEN + ASM_MESON_TAC[LE_REFL; DIM_SPAN]);; + +let DIM_PSUBSET = prove + (`!s t:real^N->bool. span s PSUBSET span t ==> dim s < dim t`, + ONCE_REWRITE_TAC[GSYM DIM_SPAN] THEN + SIMP_TAC[PSUBSET; DIM_SUBSET; LT_LE] THEN + MESON_TAC[EQ_IMP_LE; DIM_EQ_SPAN; SPAN_SPAN]);; + +let LOWDIM_EXPAND_DIMENSION = prove + (`!s:real^N->bool n. + dim s <= n /\ n <= dimindex(:N) + ==> ?t. dim(t) = n /\ span s SUBSET span t`, + REPEAT STRIP_TAC THEN MP_TAC(ISPECL + [`euclidean_matroid:(real^N)matroid`; `s:real^N->bool`; `n:num`] + MATROID_LOWDIM_EXPAND_DIMENSION) THEN + ASM_SIMP_TAC[EUCLIDEAN_MATROID; EUCLIDEAN_MATROID_DIMENSION; + EUCLIDEAN_MATROID_FINITE_DIM; EUCLIDEAN_MATROID_DIM]);; + +let LOWDIM_EXPAND_BASIS = prove + (`!s:real^N->bool n. + dim s <= n /\ n <= dimindex(:N) + ==> ?b. b HAS_SIZE n /\ independent b /\ span s SUBSET span b`, + REPEAT STRIP_TAC THEN MP_TAC(ISPECL + [`euclidean_matroid:(real^N)matroid`; `s:real^N->bool`; `n:num`] + MATROID_LOWDIM_EXPAND_BASIS) THEN + ASM_SIMP_TAC[EUCLIDEAN_MATROID; EUCLIDEAN_MATROID_INDEPENDENT; + EUCLIDEAN_MATROID_DIMENSION; EUCLIDEAN_MATROID_FINITE_DIM; + EUCLIDEAN_MATROID_DIM]);; + +(* ------------------------------------------------------------------------- *) +(* Explicit formulation of independence. *) +(* ------------------------------------------------------------------------- *) + +let INDEPENDENT_EXPLICIT = prove + (`!b:real^N->bool. + independent b <=> + FINITE b /\ + !c. vsum b (\v. c(v) % v) = vec 0 ==> !v. v IN b ==> c(v) = &0`, + GEN_TAC THEN + ASM_CASES_TAC `FINITE(b:real^N->bool)` THENL + [ALL_TAC; ASM_MESON_TAC[INDEPENDENT_BOUND]] THEN + ASM_SIMP_TAC[independent; DEPENDENT_FINITE] THEN MESON_TAC[]);; + +let INDEPENDENT_SING = prove + (`!x. independent {x} <=> ~(x = vec 0)`, + REWRITE_TAC[INDEPENDENT_INSERT; NOT_IN_EMPTY; SPAN_EMPTY] THEN + REWRITE_TAC[INDEPENDENT_EMPTY] THEN SET_TAC[]);; + +let DEPENDENT_SING = prove + (`!x. dependent {x} <=> x = vec 0`, + MESON_TAC[independent; INDEPENDENT_SING]);; + +let DEPENDENT_2 = prove + (`!a b:real^N. + dependent {a,b} <=> + if a = b then a = vec 0 + else ?x y. x % a + y % b = vec 0 /\ ~(x = &0 /\ y = &0)`, + REPEAT STRIP_TAC THEN COND_CASES_TAC THEN + ASM_REWRITE_TAC[DEPENDENT_SING; SET_RULE `{x,x} = {x}`] THEN + SIMP_TAC[DEPENDENT_FINITE; VSUM_CLAUSES; FINITE_INSERT; FINITE_EMPTY] THEN + ASM_REWRITE_TAC[IN_SING; NOT_IN_EMPTY; VECTOR_ADD_RID; EXISTS_IN_INSERT] THEN + EQ_TAC THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THENL + [X_GEN_TAC `u:real^N->real` THEN STRIP_TAC THEN + MAP_EVERY EXISTS_TAC [`(u:real^N->real) a`; `(u:real^N->real) b`] THEN + ASM_REWRITE_TAC[]; + MAP_EVERY X_GEN_TAC [`x:real`; `y:real`] THEN DISCH_TAC THEN EXISTS_TAC + `\v:real^N. if v = a then x else if v = b then y else z:real` THEN + ASM_MESON_TAC[]]);; + +let DEPENDENT_3 = prove + (`!a b c:real^N. + ~(a = b) /\ ~(a = c) /\ ~(b = c) + ==> (dependent {a,b,c} <=> + ?x y z. x % a + y % b + z % c = vec 0 /\ + ~(x = &0 /\ y = &0 /\ z = &0))`, + REPEAT STRIP_TAC THEN + SIMP_TAC[DEPENDENT_FINITE; VSUM_CLAUSES; FINITE_INSERT; FINITE_EMPTY] THEN + ASM_REWRITE_TAC[IN_SING; NOT_IN_EMPTY; VECTOR_ADD_RID; IN_INSERT] THEN + EQ_TAC THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THENL + [X_GEN_TAC `u:real^N->real` THEN STRIP_TAC THEN MAP_EVERY EXISTS_TAC + [`(u:real^N->real) a`; `(u:real^N->real) b`; `(u:real^N->real) c`]; + MAP_EVERY X_GEN_TAC [`x:real`; `y:real`; `z:real`] THEN DISCH_TAC THEN + EXISTS_TAC + `\v:real^N. if v = a then x else if v = b then y else z:real`] THEN + ASM_MESON_TAC[]);; + +let INDEPENDENT_2 = prove + (`!a b:real^N x y. + independent{a,b} /\ ~(a = b) + ==> (x % a + y % b = vec 0 <=> x = &0 /\ y = &0)`, + SIMP_TAC[IMP_CONJ_ALT; independent; DEPENDENT_2] THEN + MESON_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID]);; + +let INDEPENDENT_3 = prove + (`!a b c:real^N x y z. + independent{a,b,c} /\ ~(a = b) /\ ~(a = c) /\ ~(b = c) + ==> (x % a + y % b + z % c = vec 0 <=> x = &0 /\ y = &0 /\ z = &0)`, + SIMP_TAC[IMP_CONJ_ALT; independent; DEPENDENT_3] THEN + MESON_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID]);; + +(* ------------------------------------------------------------------------- *) +(* A kind of closed graph property for linearity. *) +(* ------------------------------------------------------------------------- *) + +let LINEAR_SUBSPACE_GRAPH = prove + (`!f:real^M->real^N. + linear f <=> subspace {pastecart x (f x) | x IN (:real^M)}`, + REWRITE_TAC[linear; subspace; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN + REWRITE_TAC[FORALL_IN_GSPEC; GSYM(SPEC `0` PASTECART_VEC); IN_UNIV] THEN + REWRITE_TAC[IN_ELIM_THM; PASTECART_INJ; UNWIND_THM1; PASTECART_ADD; + GSYM PASTECART_CMUL] THEN + MESON_TAC[VECTOR_MUL_LZERO]);; + let SPANS_IMAGE = prove (`!f b v. linear f /\ v SUBSET (span b) ==> (IMAGE f v) SUBSET span(IMAGE f b)`, @@ -5753,33 +5758,6 @@ let DIM_LINEAR_IMAGE_LE = prove (* Some stepping theorems. *) (* ------------------------------------------------------------------------- *) -let DIM_EMPTY = prove - (`dim({}:real^N->bool) = 0`, - MATCH_MP_TAC DIM_UNIQUE THEN EXISTS_TAC `{}:real^N->bool` THEN - REWRITE_TAC[SUBSET_REFL; SPAN_EMPTY; INDEPENDENT_EMPTY; HAS_SIZE_0; - EMPTY_SUBSET]);; - -let DIM_INSERT = prove - (`!x:real^N s. dim(x INSERT s) = if x IN span s then dim s else dim s + 1`, - REPEAT GEN_TAC THEN COND_CASES_TAC THENL - [MATCH_MP_TAC SPAN_EQ_DIM THEN MATCH_MP_TAC SUBSET_ANTISYM THEN - ASM_MESON_TAC[SPAN_TRANS; SUBSET; SPAN_MONO; IN_INSERT]; - ALL_TAC] THEN - X_CHOOSE_THEN `b:real^N->bool` STRIP_ASSUME_TAC - (ISPEC `span s:real^N->bool` BASIS_EXISTS) THEN - ONCE_REWRITE_TAC[GSYM DIM_SPAN] THEN - MATCH_MP_TAC DIM_UNIQUE THEN - EXISTS_TAC `(x:real^N) INSERT b` THEN REPEAT CONJ_TAC THENL - [REWRITE_TAC[INSERT_SUBSET] THEN - ASM_MESON_TAC[SUBSET; SPAN_MONO; IN_INSERT; SPAN_SUPERSET]; - REWRITE_TAC[SUBSET; SPAN_BREAKDOWN_EQ] THEN - ASM_MESON_TAC[SUBSET]; - REWRITE_TAC[INDEPENDENT_INSERT] THEN - ASM_MESON_TAC[SUBSET; SPAN_SUPERSET; SPAN_MONO; SPAN_SPAN]; - RULE_ASSUM_TAC(REWRITE_RULE[HAS_SIZE]) THEN - ASM_SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; ADD1] THEN - ASM_MESON_TAC[SUBSET; SPAN_SUPERSET; SPAN_MONO; SPAN_SPAN]]);; - let DIM_SING = prove (`!x. dim{x} = if x = vec 0 then 0 else 1`, REWRITE_TAC[DIM_INSERT; DIM_EMPTY; SPAN_EMPTY; IN_SING; ARITH]);; @@ -5794,38 +5772,6 @@ let DIM_EQ_0 = prove EXISTS_TAC `dim{vec 0:real^N}` THEN ASM_SIMP_TAC[DIM_SUBSET]] THEN ASM_REWRITE_TAC[DIM_SING; ARITH]);; -(* ------------------------------------------------------------------------- *) -(* Choosing a subspace of a given dimension. *) -(* ------------------------------------------------------------------------- *) - -let CHOOSE_SUBSPACE_OF_SUBSPACE = prove - (`!s:real^N->bool n. - n <= dim s ==> ?t. subspace t /\ t SUBSET span s /\ dim t = n`, - GEN_TAC THEN INDUCT_TAC THENL - [DISCH_TAC THEN EXISTS_TAC `{vec 0:real^N}` THEN - REWRITE_TAC[SUBSPACE_TRIVIAL; DIM_SING; SING_SUBSET; SPAN_0]; - DISCH_THEN(fun th -> POP_ASSUM MP_TAC THEN ASSUME_TAC th) THEN - ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN - DISCH_THEN(X_CHOOSE_THEN `t:real^N->bool` STRIP_ASSUME_TAC) THEN - ASM_CASES_TAC `span (s:real^N->bool) SUBSET span t` THENL - [SUBGOAL_THEN `dim(s:real^N->bool) = dim(t:real^N->bool)` MP_TAC THENL - [ALL_TAC; ASM_ARITH_TAC] THEN MATCH_MP_TAC SPAN_EQ_DIM THEN - MATCH_MP_TAC SUBSET_ANTISYM THEN ASM_REWRITE_TAC[] THEN - MATCH_MP_TAC SPAN_SUBSET_SUBSPACE THEN ASM_REWRITE_TAC[SUBSPACE_SPAN]; - FIRST_ASSUM(X_CHOOSE_THEN `y:real^N` STRIP_ASSUME_TAC o MATCH_MP(SET_RULE - `~(s SUBSET t) ==> ?a. a IN s /\ ~(a IN t)`)) THEN - EXISTS_TAC `span((y:real^N) INSERT t)` THEN - REWRITE_TAC[SUBSPACE_SPAN] THEN CONJ_TAC THENL - [MATCH_MP_TAC SPAN_SUBSET_SUBSPACE THEN - ASM_REWRITE_TAC[SUBSPACE_SPAN] THEN ASM SET_TAC[]; - ASM_REWRITE_TAC[DIM_SPAN; DIM_INSERT; ADD1]]]]);; - -let SUBSPACE_EXISTS = prove - (`!n. n <= dimindex(:N) ==> ?s:real^N->bool. subspace s /\ dim s = n`, - REPEAT GEN_TAC THEN REWRITE_TAC[GSYM DIM_UNIV] THEN - DISCH_THEN(MP_TAC o MATCH_MP CHOOSE_SUBSPACE_OF_SUBSPACE) THEN - MESON_TAC[]);; - (* ------------------------------------------------------------------------- *) (* Relation between bases and injectivity/surjectivity of map. *) (* ------------------------------------------------------------------------- *) @@ -5960,16 +5906,6 @@ let ORTHOGONAL_BASIS_EXISTS = prove ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[SPAN_SPAN; SPAN_MONO; SUBSET_TRANS; SPAN_INC]]);; -let SPAN_EQ = prove - (`!s t. span s = span t <=> s SUBSET span t /\ t SUBSET span s`, - REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ] THEN - MESON_TAC[SUBSET_TRANS; SPAN_SPAN; SPAN_MONO; SPAN_INC]);; - -let SPAN_EQ_INSERT = prove - (`!s x. span(x INSERT s) = span s <=> x IN span s`, - REWRITE_TAC[SPAN_EQ; INSERT_SUBSET] THEN - MESON_TAC[SPAN_INC; SUBSET; SET_RULE `s SUBSET (x INSERT s)`]);; - let SPAN_SPECIAL_SCALE = prove (`!s a x:real^N. span((a % x) INSERT s) = if a = &0 then span s else span(x INSERT s)`, @@ -6928,31 +6864,6 @@ let RANK_DIM_IM = prove AP_TERM_TAC THEN GEN_REWRITE_TAC LAND_CONV [GSYM SPAN_SPAN] THEN REWRITE_TAC[SPAN_STDBASIS]);; -let DIM_EQ_SPAN = prove - (`!s t:real^N->bool. s SUBSET t /\ dim t <= dim s ==> span s = span t`, - REPEAT STRIP_TAC THEN - X_CHOOSE_THEN `b:real^N->bool` STRIP_ASSUME_TAC - (ISPEC `span s:real^N->bool` BASIS_EXISTS) THEN - MP_TAC(ISPECL [`span t:real^N->bool`; `b:real^N->bool`] - CARD_GE_DIM_INDEPENDENT) THEN - RULE_ASSUM_TAC(REWRITE_RULE[HAS_SIZE]) THEN - ASM_REWRITE_TAC[DIM_SPAN] THEN - ASM_MESON_TAC[SPAN_MONO; SPAN_SPAN; SUBSET_TRANS; SUBSET_ANTISYM]);; - -let DIM_EQ_FULL = prove - (`!s:real^N->bool. dim s = dimindex(:N) <=> span s = (:real^N)`, - GEN_TAC THEN ONCE_REWRITE_TAC[GSYM DIM_SPAN] THEN EQ_TAC THEN - SIMP_TAC[DIM_UNIV] THEN DISCH_TAC THEN - GEN_REWRITE_TAC RAND_CONV [GSYM SPAN_UNIV] THEN MATCH_MP_TAC DIM_EQ_SPAN THEN - ASM_REWRITE_TAC[SUBSET_UNIV; DIM_UNIV] THEN - ASM_MESON_TAC[LE_REFL; DIM_SPAN]);; - -let DIM_PSUBSET = prove - (`!s t. (span s) PSUBSET (span t) ==> dim s < dim t`, - ONCE_REWRITE_TAC[GSYM DIM_SPAN] THEN - SIMP_TAC[PSUBSET; DIM_SUBSET; LT_LE] THEN - MESON_TAC[EQ_IMP_LE; DIM_EQ_SPAN; SPAN_SPAN]);; - let RANK_BOUND = prove (`!A:real^M^N. rank(A) <= MIN (dimindex(:M)) (dimindex(:N))`, GEN_TAC THEN REWRITE_TAC[ARITH_RULE `x <= MIN a b <=> x <= a /\ x <= b`] THEN @@ -7325,41 +7236,6 @@ let LINEAR_SINGULAR_IMAGE_HYPERPLANE = prove ASM_SIMP_TAC[LINEAR_SINGULAR_INTO_HYPERPLANE] THEN SIMP_TAC[SUBSET; FORALL_IN_IMAGE; IN_ELIM_THM] THEN MESON_TAC[]);; -let LOWDIM_EXPAND_DIMENSION = prove - (`!s:real^N->bool n. - dim s <= n /\ n <= dimindex(:N) - ==> ?t. dim(t) = n /\ span s SUBSET span t`, - GEN_TAC THEN - GEN_REWRITE_TAC (BINDER_CONV o LAND_CONV o LAND_CONV) [LE_EXISTS] THEN - SIMP_TAC[LEFT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM; IMP_CONJ] THEN - ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN - REWRITE_TAC[RIGHT_FORALL_IMP_THM; LEFT_FORALL_IMP_THM; EXISTS_REFL] THEN - INDUCT_TAC THENL [MESON_TAC[ADD_CLAUSES; SUBSET_REFL]; ALL_TAC] THEN - REWRITE_TAC[ARITH_RULE `s + SUC d <= n <=> s + d < n`] THEN - DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o check (is_imp o concl)) THEN - ASM_SIMP_TAC[LT_IMP_LE; LEFT_IMP_EXISTS_THM] THEN - X_GEN_TAC `t:real^N->bool` THEN STRIP_TAC THEN - REWRITE_TAC[ADD_CLAUSES] THEN FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN - SUBGOAL_THEN `~(span t = (:real^N))` MP_TAC THENL - [REWRITE_TAC[GSYM DIM_EQ_FULL] THEN ASM_ARITH_TAC; ALL_TAC] THEN - REWRITE_TAC[EXTENSION; IN_UNIV; NOT_FORALL_THM; LEFT_IMP_EXISTS_THM] THEN - X_GEN_TAC `a:real^N` THEN DISCH_TAC THEN - EXISTS_TAC `(a:real^N) INSERT t` THEN ASM_REWRITE_TAC[DIM_INSERT; ADD1] THEN - MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC `span(t:real^N->bool)` THEN - ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SPAN_MONO THEN SET_TAC[]);; - -let LOWDIM_EXPAND_BASIS = prove - (`!s:real^N->bool n. - dim s <= n /\ n <= dimindex(:N) - ==> ?b. b HAS_SIZE n /\ independent b /\ span s SUBSET span b`, - REPEAT GEN_TAC THEN DISCH_TAC THEN - FIRST_ASSUM(X_CHOOSE_THEN `t:real^N->bool` STRIP_ASSUME_TAC o - MATCH_MP LOWDIM_EXPAND_DIMENSION) THEN - MP_TAC(ISPEC `t:real^N->bool` BASIS_EXISTS) THEN - MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `b:real^N->bool` THEN - ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN - ASM_MESON_TAC[SPAN_SPAN; SUBSET_TRANS; SPAN_MONO]);; - (* ------------------------------------------------------------------------- *) (* Orthogonal bases, Gram-Schmidt process, and related theorems. *) (* ------------------------------------------------------------------------- *) diff --git a/holtest b/holtest index 9c116a4d..7024266a 100755 --- a/holtest +++ b/holtest @@ -67,6 +67,7 @@ echo '### Loading Examples/kb.ml'; echo 'loadt "Examples/kb.ml";;' | (time $holl echo '### Loading Examples/lagrange_lemma.ml'; echo 'loadt "Examples/lagrange_lemma.ml";;' | (time $hollight) echo '### Loading Examples/lucas_lehmer.ml'; echo 'loadt "Examples/lucas_lehmer.ml";;' | (time $hollight) echo '### Loading Examples/mangoldt.ml'; echo 'loadt "Examples/mangoldt.ml";;' | (time $hollight) +echo '### Loading Library/matroids.ml'; echo 'loadt "Library/matroids.ml";;' | (time $hollight) echo '### Loading Examples/mccarthy.ml'; echo 'loadt "Examples/mccarthy.ml";;' | (time $hollight) echo '### Loading Examples/miller_rabin.ml'; echo 'loadt "Examples/miller_rabin.ml";;' | (time $hollight) echo '### Loading Examples/misiurewicz.ml'; echo 'loadt "Examples/misiurewicz.ml";;' | (time $hollight) diff --git a/holtest.mk b/holtest.mk index 6538d36a..94b9a63a 100644 --- a/holtest.mk +++ b/holtest.mk @@ -38,6 +38,7 @@ STANDALONE_EXAMPLES:=\ Examples/lagrange_lemma \ Examples/lucas_lehmer \ Examples/mangoldt \ + Library/matroids \ Examples/mccarthy \ Examples/miller_rabin \ Examples/misiurewicz \ diff --git a/int.ml b/int.ml index caf1d596..08368ef8 100755 --- a/int.ml +++ b/int.ml @@ -2191,14 +2191,28 @@ let INT_ARITH = let base_CONV = TRY_CONV atom_CONV THENC bub_CONV in let NNF_NORM_CONV = GEN_NNF_CONV false (base_CONV,fun t -> base_CONV t,base_CONV(mk_neg t)) in + let INT_POS_RULE = + let x_tm = `x:int` and y_tm = `y:int` and n_tm = `n:num` in + let pth_pos = SPEC n_tm INT_POS + and pth_add = SPECL [x_tm;y_tm] INT_LE_ADD + and pth_mul = SPECL [x_tm;y_tm] INT_LE_MUL + and pth_pow = SPECL [x_tm;n_tm] INT_POW_LE in + let rec rule tm = + match tm with + Comb(Const("int_of_num",_),rtm) -> INST[rtm,n_tm] pth_pos + | Comb(Comb(Const("int_add",_),ltm),rtm) -> + let lth = rule ltm and rth = rule rtm in + MP (INST [ltm,x_tm; rtm,y_tm] pth_add) (CONJ lth rth) + | Comb(Comb(Const("int_mul",_),ltm),rtm) -> + let lth = rule ltm and rth = rule rtm in + MP (INST [ltm,x_tm; rtm,y_tm] pth_mul) (CONJ lth rth) + | Comb(Comb(Const("int_pow",_),ltm),rtm) -> + let lth = rule ltm in + MP (INST [ltm,x_tm; rtm,n_tm] pth_pow) lth + | _ -> failwith "INT_POS_RULE" in + rule in let INT_DIVREM_ELIM_CONV = - let DIVREM_ELIM_THM = prove - (`P (m div n) (m rem n) <=> - ?q r. (n = &0 /\ q = &0 /\ r = m \/ - m = q * n + r /\ - (&0 <= m /\ &0 <= n ==> &0 <= q) /\ - &0 <= r /\ r + &1 <= abs n) /\ - P q r`, + let tac = REWRITE_TAC[GSYM INT_LT_DISCRETE] THEN ASM_CASES_TAC `n:int = &0` THEN ASM_REWRITE_TAC[] THENL [ASM_REWRITE_TAC[INT_ABS_NUM; INT_LET_ANTISYM] THEN @@ -2207,7 +2221,31 @@ let INT_ARITH = EQ_TAC THEN STRIP_TAC THENL [MAP_EVERY EXISTS_TAC [`m div n`; `m rem n`] THEN ASM_SIMP_TAC[INT_DIVISION; INT_LE_DIV]; - ASM_METIS_TAC[INT_DIVMOD_UNIQ]]]) + ASM_METIS_TAC[INT_DIVMOD_UNIQ]]] in + let DIVREM_ELIM_THM = prove + (`P (m div n) (m rem n) <=> + ?q r. (n = &0 /\ q = &0 /\ r = m \/ + m = q * n + r /\ + &0 <= r /\ r + &1 <= abs n) /\ + P q r`, + tac) + and DIVREM_ELIM_THM' = prove + (`P (m div n) (m rem n) <=> + ?q r. (n = &0 /\ q = &0 /\ r = m \/ + m = q * n + r /\ + (&0 <= m /\ &0 <= n ==> &0 <= q) /\ + &0 <= r /\ r + &1 <= abs n) /\ + P q r`, + tac) in + let DIVREM_ELIM_THM_POS = prove + (`&0 <= m /\ &0 <= n + ==> (P (m div n) (m rem n) <=> + ?q r. (n = &0 /\ q = &0 /\ r = m \/ + m = q * n + r /\ + &0 <= q /\ + &0 <= r /\ r + &1 <= n) /\ + P q r)`, + SIMP_TAC[DIVREM_ELIM_THM'; INT_ABS]) and BETA2_CONV = RATOR_CONV BETA_CONV THENC BETA_CONV and div_tm = `(div):int->int->int` and rem_tm = `(rem):int->int->int` @@ -2226,7 +2264,12 @@ let INT_ARITH = let vd = genvar(type_of dtm) and vr = genvar(type_of rtm) in let p = list_mk_abs([vd;vr],subst[vd,dtm; vr,rtm] tm) in - let th1 = INST [p,p_tm; x,m_tm; y,n_tm] DIVREM_ELIM_THM in + let th0 = INST [p,p_tm; x,m_tm; y,n_tm] DIVREM_ELIM_THM_POS in + let th1 = + try let ltm,rtm = dest_conj(lhand(concl th0)) in + MP th0 + (CONJ (INT_POS_RULE(rand ltm)) (INT_POS_RULE(rand rtm))) + with Failure _ -> INST [p,p_tm; x,m_tm; y,n_tm] DIVREM_ELIM_THM in let th2 = CONV_RULE(COMB2_CONV(RAND_CONV BETA2_CONV) (funpow 2 BINDER_CONV(RAND_CONV BETA2_CONV))) th1 in let th3 = CONV_RULE(RAND_CONV