| b27a524 | Jacques Carette | 24 August 2020, 14:18:07 UTC | Merge pull request #35 from sjjs7/final-changes Final changes | 24 August 2020, 14:18:07 UTC |
| 04b98db | Johanna | 21 August 2020, 21:31:47 UTC | Add files via upload | 21 August 2020, 21:31:47 UTC |
| a69b53a | Johanna | 21 August 2020, 21:29:17 UTC | Create hol-light-qe-overview-aug-2020.tex Summary of changes made during the summer of 2020. | 21 August 2020, 21:29:17 UTC |
| 9267d0d | Johanna | 21 August 2020, 16:29:23 UTC | Update gen_tactics.ml | 21 August 2020, 16:29:23 UTC |
| 7255431 | Johanna | 21 August 2020, 16:28:49 UTC | Create eps_multi.ml | 21 August 2020, 16:28:49 UTC |
| de7fcc3 | Johanna | 21 August 2020, 16:26:56 UTC | Update eps_additon.ml Fixed the documentation. | 21 August 2020, 16:26:56 UTC |
| 15d4e16 | Johanna | 21 August 2020, 16:25:55 UTC | Update QuotationTactics.ml | 21 August 2020, 16:25:55 UTC |
| 0ef7dda | Johanna | 21 August 2020, 16:25:20 UTC | Update tactics.ml "Lower-down" change in error messages, to make them more explicit. | 21 August 2020, 16:25:20 UTC |
| 1a49610 | Johanna | 21 August 2020, 16:24:17 UTC | Update drule.ml Case added to make error messages better when a NEI theorem must be proved. | 21 August 2020, 16:24:17 UTC |
| cf92be4 | Johanna | 21 August 2020, 16:23:16 UTC | Update fusion.ml A few minor changes | 21 August 2020, 16:23:16 UTC |
| c2a69e5 | Jacques Carette | 16 August 2020, 15:58:52 UTC | Merge pull request #34 from sjjs7/eps_addition Eps addition | 16 August 2020, 15:58:52 UTC |
| 70549d8 | Johanna | 13 August 2020, 00:25:14 UTC | Create holQE.ml File to load HOL Light QE. | 13 August 2020, 00:25:14 UTC |
| 84450bf | Johanna | 13 August 2020, 00:23:58 UTC | Create nat_arithmetic.ml | 13 August 2020, 00:23:58 UTC |
| 31b59c7 | Johanna | 13 August 2020, 00:22:44 UTC | Update fusion.ml | 13 August 2020, 00:22:44 UTC |
| be837a8 | Johanna | 13 August 2020, 00:21:52 UTC | Update epsilon.ml | 13 August 2020, 00:21:52 UTC |
| 25500cd | Johanna | 13 August 2020, 00:21:28 UTC | Create gen_tactics.ml | 13 August 2020, 00:21:28 UTC |
| 93589c3 | Johanna | 13 August 2020, 00:21:01 UTC | Update QuotationTactics.ml | 13 August 2020, 00:21:01 UTC |
| 3db88b6 | Johanna | 13 August 2020, 00:20:28 UTC | Update eps_additon.ml | 13 August 2020, 00:20:28 UTC |
| 904f19e | Johanna | 30 July 2020, 16:41:47 UTC | Create eps_additon.ml | 30 July 2020, 16:41:47 UTC |
| ce2dc49 | Jacques Carette | 24 July 2020, 14:40:39 UTC | Merge pull request #31 from sjjs7/PR_fix Hole LEM PR | 24 July 2020, 14:40:39 UTC |
| d2737de | Johanna | 24 July 2020, 14:35:03 UTC | Update fusion.ml | 24 July 2020, 14:35:03 UTC |
| 32dc788 | Johanna | 20 July 2020, 19:16:25 UTC | Update fusion.ml | 20 July 2020, 19:16:25 UTC |
| 1fd6a40 | Johanna | 20 July 2020, 16:20:59 UTC | Update LEM_hole.ml | 20 July 2020, 16:20:59 UTC |
| 1d8c19c | Johanna | 20 July 2020, 16:18:46 UTC | Update QuotationOperatorTests.ml | 20 July 2020, 16:18:46 UTC |
| d5acdde | Johanna | 20 July 2020, 16:03:04 UTC | Create LEM_hole.ml | 20 July 2020, 16:03:04 UTC |
| f8c6de7 | Johanna | 20 July 2020, 16:02:14 UTC | Create QE_tests.ml | 20 July 2020, 16:02:14 UTC |
| 605697c | Johanna | 20 July 2020, 15:58:39 UTC | Update LEM_Example.ml | 20 July 2020, 15:58:39 UTC |
| c6f7621 | Johanna | 20 July 2020, 15:50:30 UTC | Update QuotationOperatorTests.ml | 20 July 2020, 15:50:30 UTC |
| 4f56227 | Johanna | 20 July 2020, 15:48:47 UTC | Update epsilon.ml | 20 July 2020, 15:48:47 UTC |
| ebd0c10 | Johanna | 20 July 2020, 15:47:10 UTC | Update fusion.ml | 20 July 2020, 15:47:10 UTC |
| 239dad8 | Johanna | 20 July 2020, 15:37:53 UTC | Update QuotationTactics.ml | 20 July 2020, 15:37:53 UTC |
| 664adba | Johanna | 20 July 2020, 15:20:03 UTC | Update QuotationOperatorTests.ml | 20 July 2020, 15:20:03 UTC |
| c7661b7 | Johanna | 20 July 2020, 15:19:29 UTC | Update epsilon.ml | 20 July 2020, 15:19:29 UTC |
| 2497a80 | Johanna | 20 July 2020, 15:18:32 UTC | Update fusion.ml | 20 July 2020, 15:18:32 UTC |
| fb68d2b | Johanna | 20 July 2020, 15:02:08 UTC | Merge pull request #11 from JacquesCarette/master PR-fix | 20 July 2020, 15:02:08 UTC |
| 21631c4 | Jacques Carette | 07 July 2020, 21:34:10 UTC | Merge pull request #26 from sjjs7/holeFix A few more fusion changes | 07 July 2020, 21:34:10 UTC |
| 5dac5e7 | Johanna | 07 July 2020, 20:35:14 UTC | Update pseudoquotation.ml | 07 July 2020, 20:35:14 UTC |
| ebe8578 | Johanna | 07 July 2020, 20:34:42 UTC | Update ConstructionTactics.ml | 07 July 2020, 20:34:42 UTC |
| 1b7df5a | Johanna | 07 July 2020, 20:31:52 UTC | Update fusion.ml Final minor changes to fusion | 07 July 2020, 20:31:52 UTC |
| f1021f9 | Jacques Carette | 07 July 2020, 17:58:54 UTC | Merge pull request #27 from jrh13/master Added a few miscellaneous group theory and word lemmas: | 07 July 2020, 17:58:54 UTC |
| 6c17e00 | Johanna | 06 July 2020, 14:54:13 UTC | Update holtest So I can stop c&p every time!! | 06 July 2020, 14:54:13 UTC |
| b63563d | Johanna | 06 July 2020, 14:53:07 UTC | Update QuotationTactics.ml | 06 July 2020, 14:53:07 UTC |
| 8ee2fe5 | Johanna | 06 July 2020, 14:52:19 UTC | Update fusion.ml Minor changes | 06 July 2020, 14:52:19 UTC |
| fe63c31 | Jacques Carette | 03 July 2020, 19:06:21 UTC | Merge pull request #25 from sjjs7/holeFix Hole fix | 03 July 2020, 19:06:21 UTC |
| 8ca7bb0 | Johanna | 03 July 2020, 15:00:06 UTC | Update QuotationTactics.ml | 03 July 2020, 15:00:06 UTC |
| 6b26396 | Johanna | 02 July 2020, 20:18:34 UTC | Update drule.ml | 02 July 2020, 20:18:34 UTC |
| b0c981a | Johanna | 02 July 2020, 20:18:08 UTC | Update equal.ml | 02 July 2020, 20:18:08 UTC |
| 70b1ea8 | Johanna | 02 July 2020, 20:17:37 UTC | Update basics.ml | 02 July 2020, 20:17:37 UTC |
| 97277aa | Johanna | 02 July 2020, 20:17:14 UTC | Update impconv.ml | 02 July 2020, 20:17:14 UTC |
| dab5c7a | Johanna | 02 July 2020, 20:16:26 UTC | Update preterm.ml | 02 July 2020, 20:16:26 UTC |
| 5810f1b | Johanna | 02 July 2020, 20:15:38 UTC | Update parser.ml | 02 July 2020, 20:15:38 UTC |
| aae90d9 | Johanna | 02 July 2020, 20:15:07 UTC | Update printer.ml A hole's intended type now gets printed. | 02 July 2020, 20:15:07 UTC |
| 291313c | Johanna | 02 July 2020, 20:13:50 UTC | Update fusion.ml Mostly fixed some hole implementation and removed type argument from quote. | 02 July 2020, 20:13:50 UTC |
| 857d6fc | Jacques Carette | 01 July 2020, 15:34:10 UTC | Merge pull request #24 from sjjs7/fusionFix Fusion & Construction file changes (to reflect the fusion changes) | 01 July 2020, 15:34:10 UTC |
| f4d9f23 | Johanna | 01 July 2020, 01:07:22 UTC | Update fusion.ml Fix error!! | 01 July 2020, 01:07:22 UTC |
| 1d90bfc | Johanna | 30 June 2020, 20:35:12 UTC | Update fusion.ml Changes to fusion as requested by Bill. Remove old code, fix comments & layout of inference rules. | 30 June 2020, 20:35:12 UTC |
| d3b300b | John Harrison | 29 June 2020, 00:30:52 UTC | Added a few miscellaneous group theory and word lemmas: ABELIAN_GROUP_PRODUCT_ITERATE ABELIAN_GROUP_SUM_ITERATE GROUP_HOMOMORPHISM_PRODUCT GROUP_HOMOMORPHISM_PRODUCT_INJECTION GROUP_HOMOMORPHISM_SUM GROUP_HOMOMORPHISM_SUM_INJECTION GROUP_HOMOMORPHISM_SUM_PROJECTION INT_VAL_WORD_MASK REAL_VAL_WORD_MASK REAL_VAL_WORD_NEG_CASES SUM_GROUP_ALT VAL_WORD_MASK Also made a couple of changes in the existing group theory material to emphasize the newer "group_sum G" in place of "iterate (group_add G)", renaming ABELIAN_GROUP_SUM to ABELIAN_GROUP_ITERATE while also removing its finiteness assumption: ABELIAN_GROUP_ITERATE = |- !G x k. abelian_group G /\ (!i. i IN k ==> x i IN group_carrier G) ==> iterate (group_add G) k x IN group_carrier G and changing ABELIAN_GROUP_HOMOMORPHISM_GROUP_SUM to use "group_sum" explicitly: ABELIAN_GROUP_HOMOMORPHISM_GROUP_SUM = |- !f k A B. abelian_group B /\ (!i. i IN k ==> group_homomorphism (A i,B) (f i)) ==> group_homomorphism (sum_group k A,B) (\x. group_sum B k (\i. f i (x i))) Also dded a simple tactic (naive backchaining plus optional initial polynomial normalization) to "Library/floor.ml" that tries to prove a real expression is an integer # g `integer(&22 / &7 * (x - x * &1) + &n pow 7)`;; ... # e REAL_INTEGER_TAC;; val it : goalstack = No subgoals | 29 June 2020, 00:30:52 UTC |
| 9b45ac7 | Johanna | 26 June 2020, 17:01:40 UTC | Update simp.ml Change is_eval_free to eval_free to reflect change in fusion | 26 June 2020, 17:01:40 UTC |
| 6e6f0ef | Johanna | 26 June 2020, 16:58:16 UTC | Update fusion.ml Biggest change was the addition of an exception (Problem) and new type (check) which is to help throw exceptions. | 26 June 2020, 16:58:16 UTC |
| 3295902 | Johanna | 25 June 2020, 20:25:04 UTC | Update Induction_Schema_Example.ml | 25 June 2020, 20:25:04 UTC |
| 73e3a5b | Johanna | 25 June 2020, 15:32:10 UTC | Update QuotationOperatorTests.ml | 25 June 2020, 15:32:10 UTC |
| 45ba75a | Johanna | 24 June 2020, 22:30:37 UTC | Update QuotationTactics.ml | 24 June 2020, 22:30:37 UTC |
| 339a9e9 | Johanna | 24 June 2020, 22:30:01 UTC | Update QuotationOperatorTests.ml | 24 June 2020, 22:30:01 UTC |
| 9cdb2ae | Johanna | 24 June 2020, 22:29:14 UTC | Update LEM_Example.ml | 24 June 2020, 22:29:14 UTC |
| 4899e82 | Johanna | 24 June 2020, 22:28:25 UTC | Update Induction_Schema_Example.ml | 24 June 2020, 22:28:25 UTC |
| 6e36919 | Johanna | 24 June 2020, 22:25:09 UTC | Update ConstructionTactics.ml | 24 June 2020, 22:25:09 UTC |
| d37b807 | Johanna | 24 June 2020, 22:14:55 UTC | Update fusion | 24 June 2020, 22:14:55 UTC |
| 7b6fce3 | Jacques Carette | 24 June 2020, 19:21:42 UTC | Merge pull request #23 from sjjs7/sixth Sixth | 24 June 2020, 19:21:42 UTC |
| 567c998 | sjjs7 | 23 June 2020, 14:46:23 UTC | fix LAST error | 23 June 2020, 14:46:23 UTC |
| f7c3d50 | sjjs7 | 23 June 2020, 14:39:40 UTC | Merge branch '070' into sixth | 23 June 2020, 14:39:40 UTC |
| b5b500c | sjjs7 | 23 June 2020, 14:37:24 UTC | Merge branch '068' into sixth | 23 June 2020, 14:37:24 UTC |
| f0a140a | sjjs7 | 23 June 2020, 14:35:30 UTC | Merge branch '067' into sixth | 23 June 2020, 14:35:30 UTC |
| f5f0d14 | sjjs7 | 23 June 2020, 14:33:52 UTC | Merge branch '066' into sixth | 23 June 2020, 14:33:52 UTC |
| e3471f4 | sjjs7 | 23 June 2020, 14:32:53 UTC | Merge branch '065' into sixth | 23 June 2020, 14:32:53 UTC |
| a580a68 | sjjs7 | 23 June 2020, 14:31:17 UTC | fix error | 23 June 2020, 14:31:17 UTC |
| 794b5c5 | Jacques Carette | 23 June 2020, 14:27:54 UTC | Merge pull request #22 from sjjs7/fifth Fifth batch | 23 June 2020, 14:27:54 UTC |
| 25a5cc6 | sjjs7 | 23 June 2020, 14:26:58 UTC | Merge branch '063' into sixth | 23 June 2020, 14:26:58 UTC |
| 6eb5098 | sjjs7 | 23 June 2020, 14:24:15 UTC | Merge branch '061' into sixth | 23 June 2020, 14:24:15 UTC |
| 4b19bac | sjjs7 | 23 June 2020, 14:21:37 UTC | Merge branch '060' into sixth | 23 June 2020, 14:21:37 UTC |
| 06bdf8c | Jacques Carette | 23 June 2020, 02:10:19 UTC | Merge pull request #21 from sjjs7/fourth big batch | 23 June 2020, 02:10:19 UTC |
| c5e58ff | sjjs7 | 22 June 2020, 14:37:05 UTC | error with CHANGES | 22 June 2020, 14:37:05 UTC |
| 5829d73 | sjjs7 | 22 June 2020, 14:31:17 UTC | Merge branch '025' | 22 June 2020, 14:31:17 UTC |
| 94b6b31 | sjjs7 | 22 June 2020, 14:29:19 UTC | Merge branch '023' | 22 June 2020, 14:29:19 UTC |
| c0f9e50 | sjjs7 | 22 June 2020, 14:27:28 UTC | Merge branch '022' | 22 June 2020, 14:27:28 UTC |
| 38715e8 | sjjs7 | 22 June 2020, 14:26:00 UTC | Merge branch '021' | 22 June 2020, 14:26:00 UTC |
| 9c85d55 | sjjs7 | 22 June 2020, 14:24:49 UTC | Merge branch '020' | 22 June 2020, 14:24:49 UTC |
| 835d8c2 | sjjs7 | 22 June 2020, 14:23:30 UTC | Merge branch '019' | 22 June 2020, 14:23:30 UTC |
| b533c68 | sjjs7 | 22 June 2020, 14:21:44 UTC | Merge branch '018' | 22 June 2020, 14:21:44 UTC |
| b01f7d0 | sjjs7 | 22 June 2020, 14:20:47 UTC | Merge branch '017' | 22 June 2020, 14:20:47 UTC |
| 4d5213f | sjjs7 | 22 June 2020, 14:18:02 UTC | Merge branch '016' | 22 June 2020, 14:18:02 UTC |
| b7fa9d3 | sjjs7 | 22 June 2020, 14:15:16 UTC | Merge branch '015' | 22 June 2020, 14:15:16 UTC |
| 710d0bb | sjjs7 | 22 June 2020, 13:55:54 UTC | Merge branch '012' | 22 June 2020, 13:55:54 UTC |
| 1a29c64 | sjjs7 | 22 June 2020, 13:47:17 UTC | Merge branch '011' | 22 June 2020, 13:47:17 UTC |
| 6d3e58e | sjjs7 | 22 June 2020, 13:45:17 UTC | Merge branch '010' | 22 June 2020, 13:45:17 UTC |
| d64054a | sjjs7 | 22 June 2020, 13:43:21 UTC | Merge branch '09' | 22 June 2020, 13:43:21 UTC |
| 62f986e | John Harrison | 22 June 2020, 00:07:06 UTC | Added a number of lemmas, mainly technical group theory results related to the correspondence between internal and external direct sums over an arbitrary indexing set, e.g. ISOMORPHIC_NORMAL_SUM_GROUP = |- !k G h. (!i. i IN k ==> h i normal_subgroup_of G) /\ subgroup_generated G (UNIONS {h i | i IN k}) = G /\ (!i. i IN k ==> h i INTER group_carrier (subgroup_generated G (UNIONS {h j | j IN k DELETE i})) = {group_id G}) ==> sum_group k (\i. subgroup_generated G (h i)) isomorphic_group G Renamed SUBGROUP_GENERATED_SETOP -> SUBGROUP_GENERATED_SETMUL, which is a more natural name (this was a survival from more general "op" terminology which tried to be neutral between additive and multiplicative forms of group properties). Added "group_sum", "group_product", "ring_sum" and "ring_product" to the basic congruence rules for the simplifier so that their bodies can be simplified using the context. Switched around all the theorems RING_SUM_RESTRICT, RING_SUM_SUPPORT, RING_PRODUCT_RESTRICT and RING_PRODUCT_SUPPORT, to be more consistent with similar clauses for "group_sum" and "group_product" and other iterated operations. Added a shallow "tactic" wrapper GROUP_TAC around GROUP_RULE, which is marginally more convenient to use in interactive tactic proofs. It does include the preprocessing step of trying to solve "one-relator" problems by reducing "s = t ==> u = v" to "s = t <=> u = v" and trying to prove that via the complete procedure for equivalences, an incomplete but on occasional useful process for implications. (This is a decidable problem so a complete procedcure is possible, but it requires quite a bit more work than the equivalence case for not too many applications.) New theorems: GROUP_EPIMORPHISM_ABELIAN_GROUP_SUM GROUP_EPIMORPHISM_GROUP_SUM GROUP_EPIMORPHISM_GROUP_SUM_EQ GROUP_EPIMORPHISM_GROUP_SUM_GEN GROUP_EPIMORPHISM_INTO_SUBGROUP_EQ GROUP_EPIMORPHISM_INTO_SUBGROUP_EQ_GEN GROUP_HOMOMORPHISM_GROUP_SUM GROUP_HOMOMORPHISM_GROUP_SUM_EQ GROUP_HOMOMORPHISM_GROUP_SUM_GEN GROUP_ISOMORPHISM_ABELIAN_GROUP_SUM GROUP_ISOMORPHISM_GROUP_SUM GROUP_ISOMORPHISM_GROUP_SUM_EQ GROUP_ISOMORPHISM_GROUP_SUM_GEN GROUP_MONOMORPHISM_ABELIAN_GROUP_SUM GROUP_MONOMORPHISM_GROUP_SUM GROUP_MONOMORPHISM_GROUP_SUM_EQ GROUP_MONOMORPHISM_GROUP_SUM_GEN GROUP_MONOMORPHISM_INTO_SUPERGROUP IN_SUBGROUP_PRODUCT IN_SUBGROUP_SUM ISOMORPHIC_ABELIAN_SUM_GROUP ISOMORPHIC_NORMAL_SUM_GROUP ISOMORPHIC_SUM_GROUP ISOMORPHIC_SUM_GROUP_GEN RESTRICTION_THM SUBGROUP_EPIMORPHISM_ABELIAN_GROUP_SUM SUBGROUP_EPIMORPHISM_GROUP_SUM SUBGROUP_EPIMORPHISM_GROUP_SUM_EQ SUBGROUP_EPIMORPHISM_GROUP_SUM_GEN SUBGROUP_GENERATED_SUPERSET SUBGROUP_ISOMORPHISM_ABELIAN_GROUP_SUM SUBGROUP_ISOMORPHISM_GROUP_SUM SUBGROUP_ISOMORPHISM_GROUP_SUM_EQ SUBGROUP_ISOMORPHISM_GROUP_SUM_GEN SUBGROUP_MONOMORPHISM_EPIMORPHISM WORD_NEG_SUB WORD_NOT_NOT WORD_XOR_NOT | 22 June 2020, 00:07:06 UTC |
| ed91bdd | sjjs7 | 21 June 2020, 20:35:01 UTC | Merge branch '08' | 21 June 2020, 20:35:01 UTC |
| 7b0807d | sjjs7 | 21 June 2020, 20:33:58 UTC | Merge branch '07' | 21 June 2020, 20:33:58 UTC |
| 76a47ed | sjjs7 | 21 June 2020, 20:32:10 UTC | Merge branch '06' | 21 June 2020, 20:32:10 UTC |
| 729addc | sjjs7 | 21 June 2020, 20:31:04 UTC | Merge branch '05' | 21 June 2020, 20:31:04 UTC |
