{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":44509152,"defaultBranch":"master","name":"hol-light","ownerLogin":"jrh13","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2015-10-19T03:27:43.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/15177806?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1445225715.0","currentOid":""},"activityList":{"items":[{"before":"5af59fc27f53b97efa1c4afdfacae89de99e7722","after":"2c04223793f00dd0221d87ceed7e7612592b007d","ref":"refs/heads/master","pushedAt":"2024-09-24T17:16:17.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Merge pull request #111 from jargh/master\n\nEnable more descriptive names for quantifiers and logical constants","shortMessageHtmlLink":"Merge pull request #111 from jargh/master"}},{"before":"bf1651f0aa3f52a25fb0f7e910dfb6c52505050d","after":"5af59fc27f53b97efa1c4afdfacae89de99e7722","ref":"refs/heads/master","pushedAt":"2024-09-19T16:51:45.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Merge pull request #110 from jargh/master\n\nEnhance word automation procedures WORD_ARITH and BITBLAST_RULE","shortMessageHtmlLink":"Merge pull request #110 from jargh/master"}},{"before":"413e41a997c2a84ea72b1a5725c2e44dda08b2e9","after":"bf1651f0aa3f52a25fb0f7e910dfb6c52505050d","ref":"refs/heads/master","pushedAt":"2024-09-19T15:45:45.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Merge pull request #108 from aqjune-aws/module3\n\nSupport compilation of HOL Light","shortMessageHtmlLink":"Merge pull request #108 from aqjune-aws/module3"}},{"before":"282fc370a33c3e5900dd2789bd53dd2a3bf138ad","after":"413e41a997c2a84ea72b1a5725c2e44dda08b2e9","ref":"refs/heads/master","pushedAt":"2024-09-19T13:37:03.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Merge pull request #109 from aqjune-aws/imp_rewrite\n\nFix tactics in impconv.ml to raise Failure rather than Unchanged","shortMessageHtmlLink":"Merge pull request #109 from aqjune-aws/imp_rewrite"}},{"before":"016d22698294583153a0d9ff625d0b0cf44ee9d1","after":"282fc370a33c3e5900dd2789bd53dd2a3bf138ad","ref":"refs/heads/master","pushedAt":"2024-08-23T22:53:56.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Merge pull request #107 from aqjune-aws/module2\n\nFactor out loader functions and core loads as hol_loader.ml and hol_lib.ml","shortMessageHtmlLink":"Merge pull request #107 from aqjune-aws/module2"}},{"before":"7f7808d6df09801ea84a7a7ade278b1d20dcb2b7","after":"016d22698294583153a0d9ff625d0b0cf44ee9d1","ref":"refs/heads/master","pushedAt":"2024-08-08T17:37:11.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Merge pull request #106 from aqjune-aws/bugfix\n\nFix include Bignum failure when hol.sh is loaded outside hol-light","shortMessageHtmlLink":"Merge pull request #106 from aqjune-aws/bugfix"}},{"before":"321103aa0630b04c2215af47fed85861c55ffbfc","after":"7f7808d6df09801ea84a7a7ade278b1d20dcb2b7","ref":"refs/heads/master","pushedAt":"2024-08-06T18:23:16.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Merge pull request #105 from aqjune-aws/module1\n\nEnable using pa_j as a standalone camlp5r preprocessor","shortMessageHtmlLink":"Merge pull request #105 from aqjune-aws/module1"}},{"before":"16b184e30e7e3fe9add7d1ee93242323ed2e1726","after":"321103aa0630b04c2215af47fed85861c55ffbfc","ref":"refs/heads/master","pushedAt":"2024-08-06T18:00:36.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Merge pull request #103 from aqjune/url\n\nUpdate README to refer to the new homepage","shortMessageHtmlLink":"Merge pull request #103 from aqjune/url"}},{"before":"c94729fede821f12f00b785bc6fb515e363b77ff","after":"16b184e30e7e3fe9add7d1ee93242323ed2e1726","ref":"refs/heads/master","pushedAt":"2024-07-07T01:50:43.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Added various elementary group and ring theorems (e.g. characterizations\nof units and nilpotents in polynomial rings), as well as a suite of\nanalogous extras for the various NIST/SECG Weierstrass form elliptic\ncurves giving the group order and order of each element.\n\n DIVIDES_EQ_ZERO\n GROUP_ELEMENT_ORDER_PRIME\n GROUP_POW_MOD_ELEMENT_ORDER\n GROUP_POW_MOD_ORDER\n GROUP_ZPOW_INV\n GROUP_ZPOW_REM_ELEMENT_ORDER\n GROUP_ZPOW_REM_ORDER\n IN_SUBRING_PRODUCT\n IN_SUBRING_SUM\n MONOMIAL_VAR_1\n P192K1_GROUP_ELEMENT_ORDER\n P192K1_GROUP_ORDER\n P192_GROUP_ELEMENT_ORDER\n P192_GROUP_ORDER\n P224K1_GROUP_ELEMENT_ORDER\n P224K1_GROUP_ORDER\n P224_GROUP_ELEMENT_ORDER\n P256K1_GROUP_ELEMENT_ORDER\n P256K1_GROUP_ORDER\n P256_GROUP_ELEMENT_ORDER\n P256_GROUP_ORDER\n P256_GROUP_ORDER\n P384_GROUP_ELEMENT_ORDER\n P384_GROUP_ORDER\n P521_GROUP_ELEMENT_ORDER\n P521_GROUP_ORDER\n POLY_EVALUATE_AT_0\n POLY_EVAL_AT_0\n POLY_EXTEND_AT_0\n POLY_MUL_MONOMIAL_1\n POLY_SUBRING_GENERATED\n RING_HOMOMORPHISM_MONOMIAL_1\n RING_NILPOTENT_POLY_RING\n RING_NILPOTENT_SUM\n RING_UNIT_POLY_CONST\n RING_UNIT_POLY_DOMAIN\n RING_UNIT_POLY_RING\n\nAlso consistently renamed all the following existing theorems:\n\n FINITE_GROUP_CARRIER_192 -> FINITE_GROUP_CARRIER_P192\n FINITE_GROUP_CARRIER_192K1 -> FINITE_GROUP_CARRIER_P192K1\n FINITE_GROUP_CARRIER_224 -> FINITE_GROUP_CARRIER_P224\n FINITE_GROUP_CARRIER_224K1 -> FINITE_GROUP_CARRIER_P224K1\n FINITE_GROUP_CARRIER_256 -> FINITE_GROUP_CARRIER_P256\n FINITE_GROUP_CARRIER_256K1 -> FINITE_GROUP_CARRIER_P256K1\n FINITE_GROUP_CARRIER_384 -> FINITE_GROUP_CARRIER_P384\n FINITE_GROUP_CARRIER_521 -> FINITE_GROUP_CARRIER_P521","shortMessageHtmlLink":"Added various elementary group and ring theorems (e.g. characterizations"}},{"before":"27f8d1c9b4ee2ed68d4777b784a95fb0366b2d10","after":"c94729fede821f12f00b785bc6fb515e363b77ff","ref":"refs/heads/master","pushedAt":"2024-07-06T20:12:09.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Merge pull request #102 from aqjune/camlp5-update\n\nAdd camlp5 8.03 support, update make switch to use it","shortMessageHtmlLink":"Merge pull request #102 from aqjune/camlp5-update"}},{"before":"168189671bb7cad63b7e13d2d66ef712527478ca","after":"27f8d1c9b4ee2ed68d4777b784a95fb0366b2d10","ref":"refs/heads/master","pushedAt":"2024-06-27T01:05:11.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Added missing test file for Cadical interface","shortMessageHtmlLink":"Added missing test file for Cadical interface"}},{"before":"ae6f82198f85860f2fb648882bdc90f307e5f821","after":"168189671bb7cad63b7e13d2d66ef712527478ca","ref":"refs/heads/master","pushedAt":"2024-06-13T00:30:43.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Added a slew of further elementary definitions and theorems about\nrings, in particular defining \"local_ring\" (local ring), \"poly_deg\"\n(degree of a polynomial), \"poly_evaluate\"/\"poly_eval\" (evaluation in\nthe multivariate and univariate settings). In incompatible changes,\nthe original name POLY_CONST_0 is now used for a slightly different\ntheorem.\n\nAdded basic existence of direct limits (for a simple nested union of\nsets) for both groups and rings, as well as some more pure set theory,\nincluding a general version of Zorn's lemma for a quasi-order\n(preorder). In incompatible changes, the existing HP (Hausdorff\nmaximal principle) is now generalized to preorders, and the existing\nQOSET_REFL is renamed to QOSET_REFL_EQ to maintain terminological\nconsistency with POSET_REFL.\n\nAdded a few more machine word theorems including TWOS_COMPLEMENT_GEN\n(a more general variant of the existing theorem TWOS_COMPLEMENT) and\nsome little lemmas giving characterizations of various orderings in\nterms of the top bit (cf. Hacker's Delight 2-11).\n\nAdopted a small refinement from Joe Hurd that eliminates the catching\nof completely arbitrary exception patterns (\"with _ -> ...\") in the\nMETIS code. In principle, such patterns could hide or be confused by\nasynchronous interrupts.\n\nMade a very tiny tweak to the printer to allow/encourage linebreak\nafter the varstruct of an abstraction, even if it consists of just a\nsingle variable.\n\nNew definitions:\n\n local_ring\n poly_deg\n poly_eval\n poly_evaluate\n poly_sub\n\nand theorems:\n\n EUCLIDEAN_POLY_RING\n EXISTS_FUN_FROM_1\n EXISTS_UNIQUE_UNIONS_INTERS\n FIELD_IMP_LOCAL_RING\n FINITE_SUBSET_UNIONS_CHAIN_EQ\n FINITE_SUBSET_UNIONS_DIRECTED_EQ\n FORALL_FUN_FROM_1\n GROUP_DIRECT_LIMIT\n INTEGER_QUOTIENT_RING_ISOMORPHIC_MOD\n INTEGER_RING_COSET_IDEAL_GENERATED_SING\n INTEGER_RING_IDEAL_GENERATED_SING\n IN_POLY_RING_CARRIER\n IN_RING_COSET\n IN_RING_POLYNOMIAL_CARRIER_COMPOSE\n IN_RING_POWERSERIES_CARRIER_COMPOSE\n ISOMORPHIC_RING_LOCALITY\n ISOMORPHIC_SUBCOPY_OF_RING\n LOCAL_IMP_NONTRIVIAL_RING\n LOCAL_POWSER_RING\n LOCAL_QUOTIENT_RING\n LOCAL_RING_EPIMORPHIC_IMAGE\n LOCAL_RING_IDEAL_NONUNITS\n LOCAL_RING_LOCALIZATION\n MAXIMAL_CONTAINING_IDEAL_EXISTS\n MAXIMAL_IDEAL_NONUNITS\n MONOMIAL_DEG\n MONOMIAL_DEG_LE_POLY_DEG\n MONOMIAL_DEG_UNIVARIATE\n MONOMIAL_VARS_UNIVARIATE\n PID_POLY_RING\n POLY_0\n POLY_CLAUSES\n POLY_CONST_1\n POLY_DEG_0\n POLY_DEG_1\n POLY_DEG_ADD\n POLY_DEG_ADD_LE\n POLY_DEG_CONST\n POLY_DEG_EQ\n POLY_DEG_EQ_0\n POLY_DEG_EQ_0_ALT\n POLY_DEG_GE\n POLY_DEG_GE_EQ\n POLY_DEG_HOMOMORPHIC_IMAGE\n POLY_DEG_LE\n POLY_DEG_LE_EQ\n POLY_DEG_MONOMIAL_EXISTS\n POLY_DEG_MONOMORPHIC_IMAGE\n POLY_DEG_MUL\n POLY_DEG_MUL_LE\n POLY_DEG_NEG\n POLY_DEG_RING_ADD_LE\n POLY_DEG_RING_SUB_LE\n POLY_DEG_RING_SUM_LE\n POLY_DEG_SUB\n POLY_DEG_SUB_LE\n POLY_DEG_UNIQUE\n POLY_DEG_VAR\n POLY_DEG_VAR_POW\n POLY_DIVIDES_X_MINUS_A\n POLY_DIVIDES_X_MINUS_ROOT\n POLY_DIVIDES_X_MINUS_ROOT_EQ\n POLY_DIVISION\n POLY_DIVISION_GEN\n POLY_EQ_0_MONOMORPHIC_IMAGE\n POLY_EVAL\n POLY_EVALUATE\n POLY_EVALUATE_0\n POLY_EVALUATE_1\n POLY_EVALUATE_ADD\n POLY_EVALUATE_CONST\n POLY_EVALUATE_EQ\n POLY_EVALUATE_HOMOMORPHIC_IMAGE\n POLY_EVALUATE_MUL\n POLY_EVALUATE_SUB\n POLY_EVALUATE_VAR\n POLY_EVAL_0\n POLY_EVAL_1\n POLY_EVAL_ADD\n POLY_EVAL_CONST\n POLY_EVAL_EXPAND\n POLY_EVAL_HOMOMORPHIC_IMAGE\n POLY_EVAL_MUL\n POLY_EVAL_SUB\n POLY_EVAL_VAR\n POLY_EXPAND\n POLY_EXTEND_EQ\n POLY_EXTEND_EVALUATE\n POLY_EXTEND_HOMOMORPHIC_IMAGE\n POLY_EXTEND_SUB\n POLY_EXTEND_UNIVARIATE\n POLY_MONOMIALS\n POLY_MONOMIALS_FINITE\n POLY_MONOMIAL_IN_CARRIER\n POLY_MUL_0\n POLY_RING_CLAUSES\n POLY_ROOT_BOUND\n POLY_SUB\n POLY_TOP_MONOMIAL_LE\n POLY_TOP_MONOMIAL_LT\n POLY_TOP_NONZERO\n POLY_TOP_TAIL\n POLY_VAR_UNIV\n POWSER_MONOMIALS\n POWSER_MONOMIAL_IN_CARRIER\n POWSER_VAR_UNIV\n PRIME_IDEAL_CONTAINS_NILPOTENTS\n PRIME_IDEAL_NONUNITS\n PROPER_IDEAL_NONUNITS\n PROPER_IDEAL_SUBSET_NONUNITS\n QOSET_FLDEQ\n QOSET_REFL_EQ\n QOSET_TRANS\n RESTRICTION_UNIV\n RING_COSET_IDEAL_GENERATED_SING\n RING_COSET_IDEAL_GENERATED_SING_EQ\n RING_COSET_RELATIONAL\n RING_DIRECT_LIMIT\n RING_EPIMORPHISM_I\n RING_EPIMORPHISM_POLY_EVAL\n RING_EPIMORPHISM_POLY_EVALUATE\n RING_EPIMORPHISM_POLY_RINGS\n RING_EPIMORPHISM_POWSER_RINGS\n RING_HOMOMORPHISM_I\n RING_HOMOMORPHISM_INTEGER_MOD_RINGS\n RING_HOMOMORPHISM_INTEGER_MOD_RINGS_POW\n RING_HOMOMORPHISM_POLY_EVAL\n RING_HOMOMORPHISM_POLY_EVALUATE\n RING_HOMOMORPHISM_POLY_RINGS\n RING_HOMOMORPHISM_POWSER_RINGS\n RING_IDEAL_NONUNITS\n RING_ISOMORPHISMS_I\n RING_ISOMORPHISM_I\n RING_ISOMORPHISM_POLY_RINGS\n RING_ISOMORPHISM_POWSER_RINGS\n RING_MONOMORPHISM_I\n RING_MONOMORPHISM_POLY_RINGS\n RING_MONOMORPHISM_POWSER_RINGS\n RING_MULTSYS\n RING_NILPOTENT_UNIT\n RING_POLYNOMIAL\n RING_POLYNOMIAL_CARRIER\n RING_POLYNOMIAL_CARRIER_GEN\n RING_POLYNOMIAL_COMPOSE\n RING_POLYNOMIAL_MONOMIAL\n RING_POLYNOMIAL_SUB\n RING_POWERSERIES_COMPOSE\n RING_POWERSERIES_MONOMIAL\n RING_POWERSERIES_SUB\n RING_SATURATED_MULTSYS_NONPRIME\n RING_SUM_CLAUSES_RIGHT\n RING_UNIT_LOCALEQUIV_EQ\n RING_UNIT_LOCALIZATION\n SING_ALT\n TWOS_COMPLEMENT_GEN\n UNIONS_EQ_INTERS\n UNIONS_PRIME_IDEALS\n UNIONS_PROPER_IDEALS\n UNIQUE_PRIME_IDEAL\n UNIQUE_PRIME_IDEAL_IMP_LOCAL_RING\n UNIV_1\n WORD_COMPARISON_EQ\n WORD_COMPARISON_ILE\n WORD_COMPARISON_ILT\n WORD_COMPARISON_NE\n WORD_COMPARISON_ULE\n WORD_COMPARISON_ULT\n ZL_STRONG","shortMessageHtmlLink":"Added a slew of further elementary definitions and theorems about"}},{"before":"d8366986e22555c4e4c8ff49667d646d15c35f14","after":"ae6f82198f85860f2fb648882bdc90f307e5f821","ref":"refs/heads/master","pushedAt":"2024-06-01T00:39:18.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Merge pull request #99 from aqjune/fixes\n\nPin camlp5 version of `make switch` to 8.02.01, fix typos in `NAME_ASSUMS_TAC` help","shortMessageHtmlLink":"Merge pull request #99 from aqjune/fixes"}},{"before":"4832374d7f49e3036667e73b172889ddbb31e49e","after":"d8366986e22555c4e4c8ff49667d646d15c35f14","ref":"refs/heads/master","pushedAt":"2024-05-10T18:31:30.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Merge pull request #98 from aqjune/switch\n\nAdd `make switch` fore easy installation of dependencies","shortMessageHtmlLink":"Merge pull request #98 from aqjune/switch"}},{"before":"db271ab4ff04d3c47a70298b8f66c9dd50f288f5","after":"4832374d7f49e3036667e73b172889ddbb31e49e","ref":"refs/heads/master","pushedAt":"2024-05-10T18:01:50.000Z","pushType":"pr_merge","commitsCount":6,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Merge pull request #97 from monadius/nonlinear\n\nFormal_ineqs updates","shortMessageHtmlLink":"Merge pull request #97 from monadius/nonlinear"}},{"before":"4460d849589b19c8b58962f0f67b68f21b56b285","after":"db271ab4ff04d3c47a70298b8f66c9dd50f288f5","ref":"refs/heads/master","pushedAt":"2024-04-13T06:04:12.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Added a proof-checking interface to the Cadical SAT solver\n(https://github.com/arminbiere/cadical). This is highly analogous to\nthe existing interfaces to Minisat and zchaff in \"Minisat/*\" and uses\nsome very similar code for CNF transformation. Among other facilities,\nthis makes available a Cadical-powered tautology checker, with the\nLRAT proof produced by Cadical (it is tidied up with lrat-trim in the\nstandard flow) checked in the HOL Light kernel. For example:\n\n # CADICAL_PROVE `(p ==> q) <=> (p <=> p /\\ q)`;;\n val it : thm = |- p ==> q <=> p <=> p /\\ q\n\nAdded a proof that a polygon with all its vertices on the unit circle\nis closed under complex multiplication iff the vertices are the n'th\ncomplex roots of unity for some n. This is based on the discussion\nhere, in particular the observation from Dario extending Carl\nSchildkraut's proof of the original problem to an equivalence:\n\n https://math.stackexchange.com/questions/4892153\n\nFixed a printer bug where interface maps were not reversed on printing\nfor binders. Also made a few minor name changes in the embedded logics\nto avoid using \"true\" and \"false\", to make room for using those as\nalternative names for T and F.\n\nMade a few useful improvements to SET_TAC and SET_RULE. First of all,\nthey now deal with conditionals at least to some extent (the previous\nfailure to do so was a basic bug). They also use streamlined versions\nof certain \"write away set concepts\" rules such as UNIONS_GSPEC, which\ncan be helpful preprocessing to make the eventual MESON problem\neasier, or even provable at all. Here are a couple of trivial examples\nthat now work but didn't previously:\n\n SET_RULE `IMAGE (f:A->B) s = UNIONS {{f x} | x IN s}`;;\n\n SET_RULE `{a,b} DELETE (a:A) = if a = b then {} else {b}`;;\n\nMade a few tiny optimizations to basic rules like CONJUNCT1 by\nswitching the implementation from PROVE_HYP to the underlying\nprimitive rules DEDUCT_ANTISYM_RULE and EQ_MP. This has the advantage\nof skipping a check that in context we know is redundant (whether the\nPROVE_HYP is non-trivial in the sense that the assumption is not there\nto start with).\n\nAdded a few new theorems (mainly in support of the polygon example\nabove):\n\n BILINEAR_IN_AFFINE_HULL\n BILINEAR_IN_CONVEX_HULL\n FINITE_SUBGROUP_OF_SETWISE\n SIMPLEX_FURTHEST_LT_EXISTS\n\nas well as generalizing these two existing theorems by removing the\nfiniteness assumption (hence perhaps making the \"SIMPLEX\" in the name\na bit misleading):\n\n SIMPLEX_FURTHEST_LT\n SIMPLEX_FURTHEST_LE_EXISTS","shortMessageHtmlLink":"Added a proof-checking interface to the Cadical SAT solver"}},{"before":"85987b12f9b9a9635b407eb76fcdfbd944bcad62","after":"4460d849589b19c8b58962f0f67b68f21b56b285","ref":"refs/heads/master","pushedAt":"2024-04-06T00:34:44.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Update ocamlgraph setup for the QBF subdirectory\n\nThis solution using \"topfind\" seems to be a lot simpler and appears\nto work reliably on recent OCamls.","shortMessageHtmlLink":"Update ocamlgraph setup for the QBF subdirectory"}},{"before":"b388ce4eeb258bbf3fc74215992872a29f7db96f","after":"85987b12f9b9a9635b407eb76fcdfbd944bcad62","ref":"refs/heads/master","pushedAt":"2024-04-05T20:31:07.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Fixed a few things that break after the removal of explicit module\nidentifiers, adding a \"float_fabs\" binding for the absolute\nvalue function on floating-point numbers.\n\nFixed a long-standing problem in the Mizarlight Makefile by using\nocamlfind to find camlp5 - this in turn can be installed in an Opam\nsetting by \"opam install ocamlfind\", and is anyway already used in\nthe main \"hol.ml\" root file for recent OCamls.","shortMessageHtmlLink":"Fixed a few things that break after the removal of explicit module"}},{"before":"bfb2ea95cf4b20f40136d5f08102875400c8cba7","after":"b388ce4eeb258bbf3fc74215992872a29f7db96f","ref":"refs/heads/master","pushedAt":"2024-04-05T15:17:40.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Made some initial changes to support OCaml version 5. This is mainly\nsimply removing the module names for some fully-qualified identifiers.\nThese are exposed at the top level anyway and are in different places\nin newer versions of OCaml, e.g.\n\n Pervasives.compare -> Stdlib.compare\n Pervasives.sqrt -> Float.sqrt\n\nThe latter one is also captured as \"float_sqrt\" to avoid getting\noverwritten by theorem names later.\n\nCurrently dynamic database updating is not supported in\nversion 5, and the current version of \"update_database.ml\"\nis a dummy that reports that fact.\n\nAlso slightly tweaked some functions in the new bignum_zarith\nwrapper to improve compatibility with the Num library, e.g\naccepting negative exponents in the power function.","shortMessageHtmlLink":"Made some initial changes to support OCaml version 5. This is mainly"}},{"before":"c153f40da8deb3bcc7aaef39126ad15e4713e68c","after":"bfb2ea95cf4b20f40136d5f08102875400c8cba7","ref":"refs/heads/master","pushedAt":"2024-04-04T14:52:42.000Z","pushType":"pr_merge","commitsCount":4,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Merge pull request #94 from aqjune/zarith\n\nUse Zarith in OCaml 4.14 instead of Num","shortMessageHtmlLink":"Merge pull request #94 from aqjune/zarith"}},{"before":"7e9faf7bcfbbc55084543bc2cb79d954a2f6f9e4","after":"c153f40da8deb3bcc7aaef39126ad15e4713e68c","ref":"refs/heads/master","pushedAt":"2024-03-20T00:59:28.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Added a basic bit-blasting tactic and rule to the word library, using\nBDDs as the backend by default (BITBLAST_TAC and BITBLAST_RULE) but\nproviding a more general BITBLAST_THEN that does the reduction followed\nby another tactic (e.g. SAT). The new file \"Examples/bitblast.ml\" gives\na number of examples, mainly typical \"Hacker's Delight\" fare.\n\nAdded a proof of Bondy's theorem, following the first of the two proofs\ngiven in Bollobas's \"Combinatorics\" for Theorem 1 (p4).\n\nMade \"strings_of_file\" and \"string_of_file\" more robust so they can\nhandle bigger input files without problems. Previously, the core loop of\n\"strings_of_file\" was not tail recursive because the body was enclosed\nin a \"try...with\" block; this is now changed. The \"string_of_file\"\nfunction now just uses more basic library functions directly instead of\ncalling \"strings_of_file\" and concatenating the results.","shortMessageHtmlLink":"Added a basic bit-blasting tactic and rule to the word library, using"}},{"before":"2120695645f56e57ba33b2598e20b5b1116bdff6","after":"7e9faf7bcfbbc55084543bc2cb79d954a2f6f9e4","ref":"refs/heads/master","pushedAt":"2024-03-17T07:17:08.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Added a basic implementation of BDDs as a HOL derived rule, in the new\nfile Library/bdd.ml, together with some examples of usage in the other\nnew file Examples/bdd_examples.ml The style of implementation follows\nBrace, Rudell and Bryant's paper \"Efficient implementation of a BDD\npackage\" (DAC 1990). This implementation is distantly descended from\nthe hol90 implementation in \"Binary Decision Diagrams as a HOL Derived\nRule\", but greatly simplified since HOL Light handles pointer-eq\nsubterms more efficiently and so we can avoid introducing any\nadditional variables. Also added an extra utility function \"atoms\" for\nreturning the set of propositional atomic formulas in a Boolean term.\n\nMade a number of explicit type variable choices in theorems (and\noccasionally fixed up or added quantifiers), just so things look\ntidier with the new default print_types_of_subterms=1.\n\nAdded miscelleneous theorems, in particular quite a few connected\nwith the concept of \"square-free\":\n\n CARD_IMAGE_LE2\n CARD_IMAGE_LT2\n FORALL_PRIME_INDEX\n IMAGE_EQ\n ISOMORPHIC_PROD_INTEGER_MOD_RING\n RING_CARRIER_INTEGER_MOD_RING\n RING_HOMOMORPHISM_PROD_INTEGER_MOD_RING\n RING_ISOMORPHISM_PROD_INTEGER_MOD_RING\n RING_OF_INT_PROD_RING\n RING_OF_NUM_PROD_RING\n SQUAREFREE,SQUAREFREE_ALT\n SQUAREFREE_DIVEXP\n SQUAREFREE_DIVEXP_EQ\n SQUAREFREE_DIVIDES\n SQUAREFREE_GCD\n SQUAREFREE_GCD_SQUARE\n VNREGULAR_INTEGER_MOD_RING","shortMessageHtmlLink":"Added a basic implementation of BDDs as a HOL derived rule, in the new"}},{"before":"44c12e043043ca52bfe02d513e6ea5019575ffed","after":"2120695645f56e57ba33b2598e20b5b1116bdff6","ref":"refs/heads/master","pushedAt":"2024-03-14T18:03:09.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Merge pull request #93 from aqjune/makehol\n\nAdd `make hol.sh` that creates `hol.sh` running `ocaml` initialized with `hol.ml`","shortMessageHtmlLink":"Merge pull request #93 from aqjune/makehol"}},{"before":"c518278d36d267500ef6c3b71f3533f60d5c3a58","after":"44c12e043043ca52bfe02d513e6ea5019575ffed","ref":"refs/heads/master","pushedAt":"2024-03-02T01:33:12.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Added more word lemmas\n\n BIT_REVERSEFIELDS_1\n WORD_CLZ_REVERSEFIELDS\n WORD_CTZ_EMULATION_POPCOUNT\n WORD_CTZ_REVERSEFIELDS\n WORD_EVENPARITY_POPCOUNT\n WORD_MUL_EXPAND\n WORD_MUL_EXPAND_ALT\n WORD_ODDPARITY_POPCOUNT\n WORD_POPCOUNT_MUL\n\nas well as defining a couple more utility functions for the word type\n\n dest_word_ty\n mk_word_ty\n\nand augmenting BIT_WORD_CONV to handle the two special cases of\ncondition and mask words based on \"bitval b\":\n\n BIT_WORD_CONV `bit 0 (word(bitval b):byte)`;;\n\n BIT_WORD_CONV `bit 42 (word_neg(word(bitval b)):int64)`;;\n\nAs for the SAT interface, made the overall GEN_SAT_PROVE, SAT_PROVE and\nZSAT_PROVE initially convert any non-variable atomic formulas into\nvariables before calling the core procedure. This makes things work on\nmore general tautologies where the atomic formulas are arbitrary. Also\nmade a few modernizations to the two README files to better reflect\nthe current experience with MiniSat and zchaff.","shortMessageHtmlLink":"Added more word lemmas"}},{"before":"3d231f3a12fef6ae014ad0a03d3e8e5680f27e26","after":"c518278d36d267500ef6c3b71f3533f60d5c3a58","ref":"refs/heads/master","pushedAt":"2024-03-01T17:00:41.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Merge pull request #92 from aqjune/typevar-print\n\nAdd a new flag `print_types_of_subterms`","shortMessageHtmlLink":"Merge pull request #92 from aqjune/typevar-print"}},{"before":"575f952a9ed3408444fd34c989af7f7db68cc271","after":"3d231f3a12fef6ae014ad0a03d3e8e5680f27e26","ref":"refs/heads/master","pushedAt":"2024-02-22T21:38:08.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Added some alternative definitions of Jacobian-coordinate elliptic\ncurve operations with fewer special case distinctions,\n\"jacobian_add_unexceptional\" and \"jacobian_double_unexceptional\". The\nkey theorems still work for these, with the exception of using the\naddition formula for doubling, which still needs to be handled\nseparately. Also added a few miscelleneous arithmetical and machine\nword theorems. New definitions:\n\n jacobian_add_unexceptional\n jacobian_double_unexceptional\n\nand theorems:\n\n DIGITSUM_UNIQUE\n DIV_ADD_EQ\n DIV_ADD_EQ_EQ\n MOD_ADD_EQ\n MOD_ADD_EQ_EQ\n VAL_EXPAND_SUBWORDS\n VAL_SUBWORDS_EQ\n WEIERSTRASS_OF_JACOBIAN_ADD_UNEXCEPTIONAL\n WEIERSTRASS_OF_JACOBIAN_DOUBLE_UNEXCEPTIONAL\n WORD_SUBWORDS_EQ\n WORD_SUBWORD_ADD","shortMessageHtmlLink":"Added some alternative definitions of Jacobian-coordinate elliptic"}},{"before":"ec54c6b846ce189974f517999ec8a4ab2031eed2","after":"575f952a9ed3408444fd34c989af7f7db68cc271","ref":"refs/heads/master","pushedAt":"2024-02-22T00:35:48.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Merge pull request #91 from aqjune/define-errmsg\n\nPrint \"'name' is already defined\" message","shortMessageHtmlLink":"Merge pull request #91 from aqjune/define-errmsg"}},{"before":"4393d5021a88b3e5e5b34f34bfa6b7087742a0fc","after":"ec54c6b846ce189974f517999ec8a4ab2031eed2","ref":"refs/heads/master","pushedAt":"2024-02-22T00:32:50.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Merge pull request #90 from aqjune/errmsg\n\nAdd NAME_ASSUMS_TAC and PRINT_GOAL_TAC, improve error messages of a few decision procedures","shortMessageHtmlLink":"Merge pull request #90 from aqjune/errmsg"}},{"before":"ea45176c4b775051c3a3c980d6c88e871e082873","after":"4393d5021a88b3e5e5b34f34bfa6b7087742a0fc","ref":"refs/heads/master","pushedAt":"2024-02-22T00:29:46.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Merge pull request #89 from yiyuan-cao/patch-1\n\nUpdate README of Proofrecording","shortMessageHtmlLink":"Merge pull request #89 from yiyuan-cao/patch-1"}},{"before":"b2b6304bbbfc183854a053e259c6591877d1472d","after":"ea45176c4b775051c3a3c980d6c88e871e082873","ref":"refs/heads/master","pushedAt":"2024-02-07T04:31:29.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jrh13","name":null,"path":"/jrh13","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15177806?s=80&v=4"},"commit":{"message":"Added just a few small lemmas, a couple abut machine words, and\nsome divstep-related ones noting that once g = 0 the update\nmatrix remains diagonal thereafter. New theorems:\n\n DIVSTEP_MAT_DIAGONAL\n DIVSTEP_MAT_DIAGONAL_1\n DIVSTEP_MAT_DIAGONAL_2\n IDIVSTEP_STAYS_ZERO\n INT_VAL_WORD_SUB\n IVAL_EQ_VAL","shortMessageHtmlLink":"Added just a few small lemmas, a couple abut machine words, and"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0yNFQxNzoxNjoxNy4wMDAwMDBazwAAAAS_bz_x","endCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wMi0wN1QwNDozMToyOS4wMDAwMDBazwAAAAP0CpxF"}},"title":"Activity ยท jrh13/hol-light"}