Merge pull request #14 from CakeML/update

Update to latest HOL Light commit

Author: dnezam

100/transcendence.ml

@@ -8,6 +8,230 @@
   * page: https://github.com/jrh13/hol-light/commits/master         *
   * *****************************************************************
 
+Mon 27th Apr 2026       Probability/*
+
+Substantially extended the probability theory library with new results,
+generalized definitions, and systematic naming cleanup, also adding
+standard discrete distributions. This work was entirely done by Claude
+Opus 4.6.
+
+The most significant structural change is the systematic generalization
+from simple random variables to integrable random variables. The original
+library developed much of the theory using simple_rv (finite-valued
+random variables) with simple_expectation. This update adds parallel
+general definitions using integrable/expectation (Lebesgue integration)
+and reproves key results at this level of generality. The naming
+convention is: unprefixed names (e.g. martingale, char_fn_re) now refer
+to the general versions, while the original simple-RV versions are
+preserved under SIMPLE_ prefixes (e.g. simple_martingale,
+simple_char_fn_re).
+
+IMPORTANT: Several definitions and theorem names that existed in the
+previous version now refer to different (strictly more general) objects.
+
+The following definitions changed meaning (old simple-RV-based
+definitions are preserved under the names shown):
+
+  martingale         now uses adapted/integrable/expectation
+                     (was: simple_adapted/simple_rv/simple_expectation;
+                      old version now called simple_martingale)
+
+  submartingale      same generalization pattern
+                     (old version now called simple_submartingale)
+
+  supermartingale    same generalization pattern
+                     (old version now called simple_supermartingale)
+
+  char_fn_re         now defined via expectation p (\x. cos(t * X x))
+                     (was: simple_expectation p (\x. cos(t * X x));
+                      old version now called simple_char_fn_re)
+
+  char_fn_im         now defined via expectation p (\x. sin(t * X x))
+                     (was: simple_expectation p (\x. sin(t * X x));
+                      old version now called simple_char_fn_im)
+
+  converges_L2       now defined via expectation
+                     (was: simple_expectation;
+                      old version now called simple_converges_L2)
+
+The following 20 theorem names that existed in the previous version now
+prove strictly stronger results (weaker hypotheses, same conclusions).
+In each case, the hypothesis "simple_rv" was replaced by
+"random_variable" or "integrable", and "simple_expectation" by
+"expectation". The old simple-RV versions are preserved with a SIMPLE_
+prefix:
+
+  CDF_LE_EXPECTATION                    CLT_CHAR_FN_CONVERGENCE
+  CHAR_FN_ADD_INDEP_IM                  CLT_CHAR_FN_IM_CONVERGENCE
+  CHAR_FN_ADD_INDEP_RE                  CLT_IM_ERROR_VANISHES
+  CHAR_FN_DETERMINES_NORMAL_CDF_LIMIT   EXPECTATION_LE_CDF
+  CHAR_FN_IM_BOUND                      MCT_NN_EXPECTATION
+  CHAR_FN_MODULUS_LE                    STEP_C_BOUND
+  CHAR_FN_RE_BOUND                      TRIG_POLY_WEAK_CONVERGENCE
+  CHAR_FN_RE_POW_CONV_EXP               WEAK_CONVERGENCE_FROM_CHAR_FN
+  CHAR_FN_SUM_IID_IM_SQ_BOUND           MEASURABLE_WRT_ADD
+  CHAR_FN_SUM_IID_RE_BOUND              MEASURABLE_WRT_SUB
+
+Major new results include:
+
+  KOLMOGOROV_SLLN: Kolmogorov's Strong Law of Large Numbers via the
+    maximal inequality for independent summands
+
+  IID_SLLN: for i.i.d. integrable random variables, the sample mean
+    converges almost surely to the common expectation
+
+  LINDEBERG_FELLER_CLT: the CLT under the Lindeberg condition for
+    triangular arrays of independent random variables
+
+  LEVY_CONTINUITY_GENERAL: pointwise convergence of characteristic
+    functions implies convergence in distribution
+
+  HELLY_SELECTION_THEOREM: every uniformly bounded sequence of
+    distribution functions has a convergent subsequence
+
+  PROHOROV_FORWARD: tightness implies relative sequential compactness
+    in the topology of convergence in distribution
+
+  RADON_NIKODYM: for an absolutely continuous signed measure, there
+    exists an integrable density
+
+  HAHN_DECOMPOSITION / JORDAN_DECOMPOSITION: every signed measure
+    admits a Hahn decomposition and a Jordan decomposition into
+    nonneg measures concentrated on complementary sets
+
+  GEN_COND_EXP_EXISTS / GEN_COND_EXP_TOWER / GEN_COND_EXP_ITERATED:
+    general conditional expectation via Radon-Nikodym with tower
+    property, iterated conditioning, monotonicity, and linearity
+
+  GEN_DOOB_DECOMPOSITION: general Doob decomposition of a
+    submartingale into a martingale plus a predictable increasing
+    process
+
+  BACKWARD_MARTINGALE_CONVERGENCE_L1_BOUNDED: L1-bounded backward
+    martingales converge almost surely
+
+  UI_SUBMARTINGALE_CONVERGENCE_AS / OPTIONAL_STOPPING_UI: uniformly
+    integrable submartingale convergence and optional stopping
+
+  AZUMA_HOEFFDING_TWO_SIDED / MCDIARMID_INEQUALITY: concentration
+    inequalities for martingales and bounded-differences functions
+
+  THREE_SERIES_SUFFICIENCY / THREE_SERIES_NECESSITY /
+  THREE_SERIES_NECESSITY_INDEP: Kolmogorov three-series theorem (both
+    directions; two independent proofs of necessity)
+
+  PALEY_ZYGMUND: reverse Markov-type inequality for lower bounds on
+    the probability that a nonneg RV exceeds a fraction of its mean
+
+  UI_BACKWARD_MARTINGALE_CONVERGENCE_AS: UI backward martingales
+    converge almost surely
+
+  WALD_EQUATION: for a martingale stopped at a bounded stopping time
+
+  FATOU_LEMMA / REVERSE_FATOU_LEMMA / DOMINATED_CONVERGENCE_AE:
+    convergence theorems for expectations
+
+  POISSON_LIMIT: the Poisson limit theorem (binomial -> Poisson)
+
+Thu 23rd Apr 2026       Library/ringtheory.ml, Library/fieldtheory.ml, 100/transcendence.ml
+
+Adopted the "coeff" function from 100/transcendence.ml in the main ring theory
+file, with an equivalent but more direct definition. Added 28 new theorems
+about coefficient extraction for basic operations, the Cauchy product, degree
+interaction, polynomial characterization, and evaluation:
+
+        COEFF
+        COEFF_IN_CARRIER
+        COEFF_IN_CARRIER_ALT
+        COEFF_NONZERO_LE
+        COEFF_NONZERO_LE_DEG
+        COEFF_POLY_0
+        COEFF_POLY_1
+        COEFF_POLY_ADD
+        COEFF_POLY_CONST
+        COEFF_POLY_CONST_MUL
+        COEFF_POLY_MUL
+        COEFF_POLY_MUL_CONST
+        COEFF_POLY_NEG
+        COEFF_POLY_SUB
+        COEFF_POLY_SUM
+        FINITE_COEFF_SUPPORT
+        FUN_EQ_COEFF
+        POLY_DEG_EQ_COEFF
+        POLY_DEG_EQ_COEFF_FROM_LE
+        POLY_DEG_LE_COEFF
+        POLY_EVAL_COEFF
+        POLY_MUL_UNIVARIATE
+        POLY_TOP_EQ_0
+        RING_POLYNOMIAL_COEFF
+        RING_POLYNOMIAL_COEFF_BOUND
+        RING_POLYNOMIAL_COEFF_ZERO_FROM
+        RING_POLYNOMIAL_SUBRING_COEFF
+        RING_POWERSERIES_COEFF
+
+Also added helper lemmas LAMBDA_1_EQ, FINITE_FUN_FROM_1, MONOMIAL_DEG_ONE
+and moved EXISTS_FUN_FROM_1, FORALL_FUN_FROM_1 earlier in the file. Seven
+existing theorems are restated to use coeff in their statements:
+
+        POLY_DIVISION_GEN
+        POLY_EVAL_AT_0
+        POLY_EVAL_EXPAND
+        POLY_EXPAND
+        POLY_EXTEND_UNIVARIATE
+        POLY_TOP_NONZERO
+        POLY_TOP_TAIL
+
+Three proofs in Library/fieldtheory.ml are adjusted for the restated
+POLY_EXTEND_UNIVARIATE, and in 100/transcendence.ml the local coeff
+definition is replaced by a bridge lemma "coeff_x_monomial" connecting the
+ringtheory definition with the local x_monomial construct, and about 20
+proofs are simplified to one-line derivations from the new ringtheory
+theorems.
+
+Mon 20th Apr 2026       passim
+
+Fixed another case identified by Daniel Nezamabadi where polymorphic
+comparison was mistakenly being used on the bignum type, this one in
+Multivariate/vectors.ml; then assisted by Claude found and fixed many
+other instances of the same issue
+
+     - iterate.ml: EXPAND_NSUM_CONV, EXPAND_SUM_CONV
+     - printer.ml: DECIMAL printer
+     - calc_rat.ml: RAW_REAL_RAT_MUL_CONV
+     - calc_int.ml: is_realintconst, term_of_rat
+     - int.ml: is_intconst
+     - Library/calc_real.ml: REAL_FLOAT_MUL_CONV helper
+     - Library/bitmatch.ml: bitpat_matches, inst_bitpat_numeral, unword
+     - Library/isum.ml: EXPAND_ISUM_CONV
+
+Tue 14th Apr 2026       Library/tactician_light.ml [new file]
+
+Added "Tactician Light", a proof format translator for HOL Light, converting
+between interactive (g/e) and structured (prove) proof styles. It is inspired
+by Mark Adams' Tactician tool for HOL Light:
+
+  http://www.proof-technologies.com/tactician/
+
+which provided similar functionality via a "hiproof" representation and
+refactoring pipeline. This is a from-scratch reimplementation by Claude Code
+using string-based tactic recording rather than the original promotion/demotion
+mechanism. Although this simpler version requires some additional user work
+(e.g. saving a log of the tactic invocations to a file for processing by
+"i2s"), it is considerably simpler and less sensitive to OCaml internals.
+
+Mon 13th Apr 2026       mcp/*
+
+Merged an update from Ceren Kocaogullar adding proof recording tools
+"start_recording" and "stop_recording" to the MCP setup. This helps when
+the LLM is developing large proofs interactively in cases where the
+context window is exhausted or the session crashes. By retaining this
+record, the proof can resume where it left off.
+
+Sun 12th Apr 2026       mcp/SKILL.md
+
+Merged an update from Nevine Ebeid to the mcp/SKILL.md file that refines or
+corrects the explanations of several constructs and adds new pitfall warnings.
+
 Wed  8th Apr 2026       100/green.ml [new file], 100/isoperimetric.ml, Library/words.ml, Multivariate/measure.ml, Multivariate/transcendentals.ml, Multivariate/realanalysis.ml, Multivariate/cauchy.ml
 
 Added a proof of Green's theorem in a fairly general form, autoformalized by
@@ -200,6 +424,117 @@ Numbers (weak and strong), Fair Games Theorem (Doob optional stopping),
 Borel-Cantelli lemmas, martingale convergence and the Azuma-Hoeffding
 inequality.
 
+Mon  9th Mar 2026       Library/ringtheory.ml
+
+Added more elementary results in ring theory: the preservation of the UFD
+property in localization and in polynomial rings (the latter via Gauss's lemma,
+some forms of which are broken out, e.g. as POLY_PRIMITIVE_CONST_CANCEL), and
+the Eisenstein irreducibility criterion:
+
+        EISENSTEIN_IRREDUCIBILITY
+        EISENSTEIN_IRREDUCIBILITY_FRACTION_RING
+        EISENSTEIN_IRREDUCIBILITY_GEN
+        INTEGRAL_DOMAIN_LOCALIZATION
+        IRREDUCIBLE_PRIMITIVE_POLY_FRACTION_RING
+        LOCALEQUIV_MUL_CANCEL
+        MAKE_PRIMITIVE_IN_IDEAL
+        MONOMIAL_MUL_VAR_ONE
+        POLY_CLEAR_DENOMINATORS
+        POLY_CONST_DIVIDES_COEFFS
+        POLY_CONST_DIVIDES_COEFFS_EQ
+        POLY_CONST_DIVIDES_COEFFS_REV
+        POLY_MAKE_PRIMITIVE
+        POLY_MONOMIALS_ALT
+        POLY_MUL_VAR_COEFF_UNIVARIATE
+        POLY_PRIMITIVE_CONST_CANCEL
+        POLY_RING_HOMOMORPHISM_I
+        POLY_VAR_DIVIDES_UNIVARIATE
+        POLY_VAR_MONOMIAL_1
+        RING_DIVIDES_LOCALEQUIV
+        RING_PRIME_POLY_CONST
+        RING_PRIME_POLY_RING_MONO
+        RING_PRIME_POLY_VAR_UNIVARIATE
+        UFD_LOCALIZATION
+        UFD_POLY_RING
+
+Fri  6th Mar 2026       sets.ml, Library/grouptheory.ml, Library/permutations.ml, Library/symmetric_group.ml [new file]
+
+Added a definition of "solvable_group" to the group theory library with some
+of its basic properties, as well as additional material about permutations.
+Combining these, the new file Library/symmetric_group.ml gives a basic
+development of the symmetric group (the group of permutations on set) including
+its unsolvability for a set of size >= 5. New definitions:
+
+        solvable_group
+        symmetric_group
+        three_cycle
+
+and theorems:
+
+        ABELIAN_IMP_SOLVABLE_GROUP
+        ABELIAN_QUOTIENT_COMMUTATOR
+        ABELIAN_QUOTIENT_EPIMORPHIC_IMAGE
+        ALL_TRANSPOSITIONS_GENERATE_SYMMETRIC
+        CARD_SYMMETRIC_GROUP
+        CAYLEY_THEOREM
+        CAYLEY_THEOREM_EXPLICIT
+        CHAIN_STEP_THREE_CYCLES_GEN
+        COMMUTATOR_IMP_ABELIAN_QUOTIENT
+        FINITE_SYMMETRIC_GROUP
+        INVERSE_UNIQUE_ALT
+        INVOLUTION_MOVES_2_IS_SWAP
+        INVOLUTION_SIZE_2_IS_SWAP
+        ISOMORPHIC_GROUP_SOLVABILITY
+        NOT_SOLVABLE_SYMMETRIC_GROUP
+        PERMUTES_THREE_CYCLE
+        POINT_TRANSPOSITIONS_GENERATE_ALL
+        PRIME_ORDER_PERM_NO_FIXPOINT
+        PRIME_ORDER_PERM_ORBIT
+        PRIME_ORDER_POW_PERM
+        RESTRICT_COMPOSE
+        RESTRICT_I
+        RESTRICT_INVERSE
+        RESTRICT_PERMUTES_SUBSET
+        RESTRICT_SWAP
+        RESTRICT_SYMMETRIC_GROUP_HOMOMORPHISM
+        SOLVABLE_GROUP_ALT
+        SOLVABLE_GROUP_EPIMORPHIC_IMAGE
+        SOLVABLE_GROUP_NORMAL_EXTENSION
+        SOLVABLE_GROUP_QUOTIENT
+        SOLVABLE_GROUP_SOLVABLE_QUOTIENT
+        SOLVABLE_GROUP_SUBGROUP
+        SUBGROUP_RESTRICT_PERMUTES
+        SWAP_CONJUGATE
+        SWAP_CONJUGATE_IN_SUBGROUP
+        SWAP_IN_SYMMETRIC_GROUP
+        SWAP_LEFT
+        SWAP_OTHER
+        SWAP_RIGHT
+        SWAP_TRIPLE
+        SWAP_TRIPLE_ALT
+        SYMMETRIC_GROUP
+        SYMMETRIC_GROUP_ACTION
+        SYMMETRIC_GROUP_ID
+        SYMMETRIC_GROUP_INV
+        SYMMETRIC_GROUP_MUL
+        SYMMETRIC_GROUP_POW
+        SYMMETRIC_GROUP_POW_IN
+        THREE_CYCLE_AS_COMMUTATOR
+        THREE_CYCLE_COMMUTATOR
+        THREE_CYCLE_COMPOSE_REVERSE
+        THREE_CYCLE_INVERSE
+        THREE_CYCLE_IN_SYMMETRIC
+        THREE_CYCLE_NOT_I
+        TRANSITIVE_TRANSPOSITION_GENERATES_SYMMETRIC
+        TRANSPOSITION_PCYCLE_GENERATES
+        TRIVIAL_IMP_SOLVABLE_GROUP
+
+Also added a few simple but natural lemmas to the sets.ml file in support:
+
+        CARD_LE_2 = |- CARD {a,b} <= 2
+        CARD_LE_3 = |- CARD {a,b,c} <= 3
+        CARD_LE_4 = |- CARD {a,b,c,d} <= 4
+
 Thu  5th Mar 2026       Help/mapi.hlp
 
 Added a documentation file for the new "mapi" function introduced as