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
jrh13 · Nov 7, 2024 · 9eccc5e · 9eccc5e
1 parent c39dbfd
commit 9eccc5e
Show file tree

Hide file tree

Showing 11 changed files with 2,410 additions and 425 deletions.
diff --git 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