diff --git a/Arithmetic/definability.ml b/Arithmetic/definability.ml index 150fe288..1691e24d 100644 --- a/Arithmetic/definability.ml +++ b/Arithmetic/definability.ml @@ -72,59 +72,11 @@ let primepow_DELTA = prove (`primepow p x <=> prime(p) /\ ~(x = 0) /\ !z. z <= x ==> z divides x ==> z = 1 \/ p divides z`, - REWRITE_TAC[primepow; TAUT `a ==> b \/ c <=> a /\ ~b ==> c`] THEN - ASM_CASES_TAC `prime(p)` THEN - ASM_REWRITE_TAC[] THEN EQ_TAC THENL - [DISCH_THEN(X_CHOOSE_THEN `n:num` SUBST1_TAC) THEN - ASM_REWRITE_TAC[EXP_EQ_0] THEN - ASM_CASES_TAC `p = 0` THEN ASM_REWRITE_TAC[] THENL - [ASM_MESON_TAC[PRIME_0]; ALL_TAC] THEN - REPEAT STRIP_TAC THEN - FIRST_ASSUM(MP_TAC o SPEC `z:num` o MATCH_MP PRIME_COPRIME) THEN - ASM_REWRITE_TAC[] THEN - ASM_CASES_TAC `p divides z` THEN ASM_REWRITE_TAC[] THEN - ONCE_REWRITE_TAC[COPRIME_SYM] THEN - DISCH_THEN(MP_TAC o SPEC `n:num` o MATCH_MP COPRIME_EXP) THEN - ASM_MESON_TAC[COPRIME; DIVIDES_REFL]; - SPEC_TAC(`x:num`,`x:num`) THEN MATCH_MP_TAC num_WF THEN - REPEAT STRIP_TAC THEN ASM_CASES_TAC `x = 1` THENL - [EXISTS_TAC `0` THEN ASM_REWRITE_TAC[EXP]; ALL_TAC] THEN - FIRST_ASSUM(X_CHOOSE_THEN `q:num` MP_TAC o MATCH_MP PRIME_FACTOR) THEN - STRIP_TAC THEN - UNDISCH_TAC `!z. z <= x ==> z divides x /\ ~(z = 1) ==> p divides z` THEN - DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN - DISCH_THEN(MP_TAC o SPEC `q:num`) THEN ASM_REWRITE_TAC[] THEN - ASM_CASES_TAC `q = 1` THENL [ASM_MESON_TAC[PRIME_1]; ALL_TAC] THEN - ASM_REWRITE_TAC[] THEN - SUBGOAL_THEN `q <= x` ASSUME_TAC THENL - [ASM_MESON_TAC[DIVIDES_LE]; ASM_REWRITE_TAC[]] THEN - SUBGOAL_THEN `p divides x` MP_TAC THENL - [ASM_MESON_TAC[DIVIDES_TRANS]; ALL_TAC] THEN - REWRITE_TAC[divides] THEN DISCH_THEN(X_CHOOSE_TAC `y:num`) THEN - SUBGOAL_THEN `y < x` (ANTE_RES_THEN MP_TAC) THENL - [MATCH_MP_TAC PRIME_FACTOR_LT THEN - EXISTS_TAC `p:num` THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN - ASM_CASES_TAC `y = 0` THENL - [UNDISCH_TAC `x = p * y` THEN ASM_REWRITE_TAC[MULT_CLAUSES]; ALL_TAC] THEN - ASM_REWRITE_TAC[] THEN - SUBGOAL_THEN `!z. z <= y ==> z divides y /\ ~(z = 1) ==> p divides z` - (fun th -> REWRITE_TAC[th]) THENL - [REPEAT STRIP_TAC THEN - FIRST_ASSUM(MATCH_MP_TAC o REWRITE_RULE - [IMP_IMP]) THEN - REPEAT CONJ_TAC THENL - [MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `y:num` THEN - ASM_REWRITE_TAC[] THEN - GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `y = 1 * y`] THEN - REWRITE_TAC[LE_MULT_RCANCEL] THEN - ASM_REWRITE_TAC[GSYM NOT_LT] THEN - REWRITE_TAC[num_CONV `1`; LT; DE_MORGAN_THM] THEN - ASM_MESON_TAC[PRIME_0; PRIME_1]; - ASM_REWRITE_TAC[] THEN MATCH_MP_TAC DIVIDES_LMUL THEN - ASM_REWRITE_TAC[]; - ASM_REWRITE_TAC[]]; - DISCH_THEN(X_CHOOSE_THEN `n:num` SUBST1_TAC) THEN - EXISTS_TAC `SUC n` THEN ASM_REWRITE_TAC[EXP]]]);; + REWRITE_TAC[primepow] THEN + ASM_CASES_TAC `prime(p)` THEN ASM_REWRITE_TAC[] THEN + ASM_CASES_TAC `x = 0` THEN ASM_REWRITE_TAC[] THENL + [ASM_MESON_TAC[EXP_EQ_0; PRIME_0]; + ASM_SIMP_TAC[PRIME_POWER_EXISTS_ALT] THEN ASM_MESON_TAC[DIVIDES_LE]]);; (* ------------------------------------------------------------------------- *) (* Sigma-representability of reflexive transitive closure. *) diff --git a/CHANGES b/CHANGES index 95154c8e..ee940c41 100644 --- a/CHANGES +++ b/CHANGES @@ -8,6 +8,178 @@ * page: https://github.com/jrh13/hol-light/commits/master * * ***************************************************************** +Wed 9th Oct 2024 Library/ringtheory.ml + +Added a number of miscellaneous and simple ring theory lemmas: + + FIELD_HOMOMORPHISM_DIV + FIELD_HOMOMORPHISM_INV + FINITE_MONOMIAL_VARS + FINITE_MONOMIAL_VARS_1 + IMAGE_POLY_EVAL + IMAGE_POLY_EXTEND_1 + IN_IDEAL_GENERATED_SELF + IN_IDEAL_GENERATED_SING + IN_IDEAL_GENERATED_SING_EQ + ISOMORPHIC_TRANSPORT_OF_RING + POLY_DEG_SUBRING_GENERATED + POLY_EXTEND_FROM_SUBRING_GENERATED + POLY_EXTEND_INTO_SUBRING_GENERATED + POLY_SUBRING_GENERATED_1 + POLY_SUBRING_GENERATED_CLAUSES + RING_0_IN_SUBRING_GENERATED + RING_1_IN_SUBRING_GENERATED + RING_ADD_IN_SUBRING_GENERATED + RING_HOMOMORPHISM_INV + RING_MONOMORPHISM_INTO_SUBRING + RING_MUL_IN_SUBRING_GENERATED + RING_NEG_IN_SUBRING_GENERATED + RING_POW_IN_SUBRING_GENERATED + RING_PRODUCT_SUBRING_GENERATED + RING_PRODUCT_SUBRING_GENERATED_GEN + RING_SUM_CASES + SUBRING_GENERATED_INC_GEN + +Wed 9th Oct 2024 EC/ccsm2.ml + +Added two more easy theorems by analogy with the earlier additions +for NIST curves: + + SM2_GROUP_ORDER = + |- CARD (group_carrier sm2_group) = n_sm2 + + SM2_GROUP_ELEMENT_ORDER = + |- !P. P IN group_carrier sm2_group + ==> group_element_order sm2_group P = + (if P = group_id sm2_group then 1 else n_sm2) + +Mon 7th Oct 2024 tactics.ml, pa_j/passim + +Merged an update from June Lee that provides an optional change in +the behaviour of THEN, requiring that first tactic should produce only +a single subgoal, rather than applying the second tactic to all the +subgoals regardless of number. This is controlled by an expansion +in the preprocessor switched by the special identifiers + + set_then_multiple_subgoals + unset_then_multiple_subgoals + +The default behavior is "set_then_multiple_subgoals", which as before +allows multiple subgoals. + +Tue 24th Sep 2024 bool.ml + +Added conveniently packaged interface mappings to set up more friendly +syntax for the quantifiers. New functions "set_verbose_symbols" and +"unset_verbose_symbols" enable and disable, respectively, these more +verbose and descriptive names for some logical symbols: + + F -> false + T -> true + ! -> forall + ? -> exists + ?! -> existsunique + +This is all done via interface maps. Not only is the underlying term +structure unchanged (the "actual" names are the symbolic ones) but +also the original syntax is accepted as an alternative: + + # `exists x. x = 1` = `?x. x = 1`;; + val it : bool = true + +The new syntax is enabled by default, but can, as explained above, +be switched off with "unset_verbose_symbols()". + +Thu 19th Sep 2024 .gitignore, Makefile, README, hol.ml, hol_4.14.sh, hol_4.sh, hol_lib.ml, hol_lib_use_module.ml [new file], inline_load.ml [new file] + +Merged an update from June Lee that enables compilation of HOL Light +(supported for OCaml >= 4.14). It is controlled by the environment +variable HOLLIGHT_USE_MODULE, such that doing: + + HOLLIGHT_USE_MODULE=1 make + +will build "hol.sh" so that it uses the compiled "hol_lib.cmo". + +Thu 19th Sep 2024 impconv.ml + +Fix IMP_REWRITE_TAC and related tactics in impconv.ml to raise the +preferred "Failure" exception rather than "Unchanged", making them +consistent with the rest of the codebase and in particular compatible +with tactic combinators like ORELSE. This change is from June Lee. + +Wed 18th Sep 2024 int.ml, Library/words.ml + +Made a small enhancement to div/rem elimination in INT_ARITH, making it +handle the common case where divisor and dividend are nonnegative, thus +being more comparable to ARITH_RULE. + +Made some improvements to WORD_ARITH/WORD_ARITH_TAC to further normalize +constants and as a last resort write away all word expressions using numeric +values, to widen the scope, e.g. + + WORD_ARITH + `!m n. m < 4096 /\ n <= 511 + ==> word_ule (word_add (word_mul (word n) (word 0x00001000)) (word m)) + (word 0x0000000001FFFFFF:int64)`;; + +Tue 17th Sep 2024 trivia.ml + +Added the special eta-conversion variant for the 1-element type: + + ETA_ONE = |- !f:1->A. (\x. f one) = f + +Tue 3rd Sep 2024 Library/words.ml + +Made a couple of small improvements to BITBLAST_RULE: do more systematic +reduction of word constant-expressions in the middle of prenormalization, and +handle val(x) DIV 2^k and val(x) MOD 2^k in the initial bitwise expansion. +(The recognition of powers of 2 in arbitrary numeric expressions is broken out +as a separate conversion EMPOWER_CONV.) For example, this didn't work before +but now does: + + BITBLAST_RULE + `word_and x (word 256):int64 = word 0 <=> val x MOD 512 < 256`;; + +Fri 23rd Aug 2024 hol_lib.ml, hol_loader.ml [new files], passim + +Merged a refactoring from June Lee that factors out file loading so that it +can be readily replaced with catenation and module compilation. + +Tue 6th Aug 2024 Makefile, bignum_num.ml, bignum_zarith.ml, hol.ml, system.ml, pa_j/passim + +Merged an update from June Lee that reorganizes the camlp5 preprocessing in +various ways so that camlp5r can be used with pa_j.cmo as a standaline +preprocessor, e.g. as follows: + + ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I . pa_j.cmo" test.ml + +This required several changes: + + * Printing "* HOL-Light syntax in effect *" is redirected to stderr, not + stdout, because ocamlc was consuming the log from from stdout too. + + * jrh_lexer is enabled by default. + + * quotexpander is moved to pa_j.ml + + * bignum files had to be separately compiled without using pa_j because + they were declaring modules which interfere with the preprocessor. + +Thu 1st Aug 2024 Library/prime.ml, Arithmetic/definability.ml + +Added a simple variant of an existing theorem PRIME_POWER_EXISTS, +characterizing prime powers via their divisors: + + PRIME_POWER_EXISTS_ALT = + |- !n p. + prime p + ==> ((?i. n = p EXP i) <=> + (!d. d divides n ==> d = 1 \/ p divides d)) + +Used this to simplify the proof of primepow_DELTA in the arithmetic +definability material, since it is only a minor elaboration of +this lemma. + Sat 6th Jul 2024 Makefile, README, pa_j [new directory], pa_j/pa_j_4.xx_8.03.ml Merged an update from June Lee adding camlp5 8.03 support and making it the diff --git a/EC/ccsm2.ml b/EC/ccsm2.ml index 3a656cb7..204ef22d 100644 --- a/EC/ccsm2.ml +++ b/EC/ccsm2.ml @@ -156,6 +156,16 @@ let SIZE_SM2_GROUP = prove REWRITE_TAC[GSYM num_coprime; ARITH; COPRIME_2] THEN DISCH_THEN(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN ASM_INT_ARITH_TAC]);; +let SM2_GROUP_ORDER = prove + (`CARD(group_carrier sm2_group) = n_sm2`, + REWRITE_TAC[REWRITE_RULE[HAS_SIZE] SIZE_SM2_GROUP]);; + +let SM2_GROUP_ELEMENT_ORDER = prove + (`!P. P IN group_carrier sm2_group + ==> group_element_order sm2_group P = + if P = group_id sm2_group then 1 else n_sm2`, + MESON_TAC[SIZE_SM2_GROUP; HAS_SIZE; GROUP_ELEMENT_ORDER_PRIME; PRIME_NSM2]);; + let GENERATED_SM2_GROUP = prove (`subgroup_generated sm2_group {g_sm2} = sm2_group`, SIMP_TAC[SUBGROUP_GENERATED_ELEMENT_ORDER; diff --git a/Library/prime.ml b/Library/prime.ml index 054273d4..ed40ac39 100755 --- a/Library/prime.ml +++ b/Library/prime.ml @@ -1729,6 +1729,14 @@ let PRIME_POWER_EXISTS = prove CONV_TAC(ONCE_DEPTH_CONV EXPAND_CASES_CONV) THEN REWRITE_TAC[LT] THEN ARITH_TAC]);; +let PRIME_POWER_EXISTS_ALT = prove + (`!n p. + prime p + ==> ((?i. n = p EXP i) <=> + (!d. d divides n ==> d = 1 \/ p divides d))`, + SIMP_TAC[PRIME_POWER_EXISTS] THEN + MESON_TAC[DIVIDES_TRANS; DIVIDES_PRIME_PRIME; PRIME_FACTOR; PRIME_1]);; + let PRIME_FACTORIZATION_ALT = prove (`!n. ~(n = 0) ==> nproduct {p | prime p} (\p. p EXP index p n) = n`, MATCH_MP_TAC COMPLETE_FACTOR_INDUCT THEN diff --git a/Library/ringtheory.ml b/Library/ringtheory.ml index 01950d13..823e9196 100644 --- a/Library/ringtheory.ml +++ b/Library/ringtheory.ml @@ -432,7 +432,7 @@ let RING_CARRIER_HAS_SIZE_1 = prove REWRITE_TAC[TRIVIAL_RING]);; let TRIVIAL_RING_HAS_SIZE_1 = prove - (`!G:A ring. trivial_ring G <=> ring_carrier(G) HAS_SIZE 1`, + (`!r:A ring. trivial_ring r <=> ring_carrier(r) HAS_SIZE 1`, REWRITE_TAC[RING_CARRIER_HAS_SIZE_1]);; let RING_CARRIER_HAS_SIZE_2 = prove @@ -746,9 +746,9 @@ let RING_POW_MUL = prove ASM_SIMP_TAC[RING_POW_ADD; CONJUNCT2 ring_pow]);; let RING_POW_POW = prove - (`!G (x:A) m n. - x IN ring_carrier G - ==> ring_pow G (ring_pow G x m) n = ring_pow G x (m * n)`, + (`!r (x:A) m n. + x IN ring_carrier r + ==> ring_pow r (ring_pow r x m) n = ring_pow r x (m * n)`, SIMP_TAC[RING_POW_MUL]);; let RING_MUL_POW = prove @@ -1238,6 +1238,21 @@ let RING_SUM_RESTRICT_SET = prove MATCH_MP_TAC RING_SUM_SUPERSET THEN SIMP_TAC[IN_ELIM_THM; SUBSET_RESTRICT] THEN MESON_TAC[]]);; +let RING_SUM_CASES = prove + (`!r s P (f:K->A) g. + FINITE s + ==> ring_sum r s (\x. if P x then f x else g x) = + ring_add r (ring_sum r {x | x IN s /\ P x} f) + (ring_sum r {x | x IN s /\ ~P x} g)`, + REPEAT STRIP_TAC THEN + MP_TAC(ISPECL [`r:A ring`; `\x. if P x then (f:K->A) x else g x`; + `{x:K | x IN s /\ P x}`; `{x:K | x IN s /\ ~P x}`] + RING_SUM_UNION) THEN + ANTS_TAC THENL [ASM_SIMP_TAC[FINITE_RESTRICT] THEN SET_TAC[]; ALL_TAC] THEN + MATCH_MP_TAC EQ_IMP THEN BINOP_TAC THENL + [AP_THM_TAC THEN AP_TERM_TAC THEN SET_TAC[]; + BINOP_TAC THEN MATCH_MP_TAC RING_SUM_EQ THEN SET_TAC[]]);; + let RING_SUM_IMAGE = prove (`!r (f:K->L) (g:L->A) s. (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) @@ -2679,9 +2694,9 @@ let SUBRING_GENERATED = prove ring_add; ring_mul]]);; let SUBRING_GENERATED_EQ = prove - (`!G s:A->bool. - subring_generated G s = G <=> - ring_carrier(subring_generated G s) = ring_carrier G`, + (`!r s:A->bool. + subring_generated r s = r <=> + ring_carrier(subring_generated r s) = ring_carrier r`, REPEAT GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [RINGS_EQ] THEN REWRITE_TAC[CONJUNCT2 SUBRING_GENERATED]);; @@ -2705,6 +2720,40 @@ let RING_OF_INT_SUBRING_GENERATED = prove REWRITE_TAC[ring_of_int; RING_OF_NUM_SUBRING_GENERATED] THEN REWRITE_TAC[SUBRING_GENERATED]);; +let RING_0_IN_SUBRING_GENERATED = prove + (`!r (s:A->bool). ring_0 r IN ring_carrier (subring_generated r s)`, + MESON_TAC[RING_0; SUBRING_GENERATED]);; + +let RING_1_IN_SUBRING_GENERATED = prove + (`!r (s:A->bool). ring_1 r IN ring_carrier (subring_generated r s)`, + MESON_TAC[RING_1; SUBRING_GENERATED]);; + +let RING_NEG_IN_SUBRING_GENERATED = prove + (`!r s x:A. + x IN ring_carrier (subring_generated r s) + ==> ring_neg r x IN ring_carrier (subring_generated r s)`, + MESON_TAC[RING_NEG; SUBRING_GENERATED]);; + +let RING_ADD_IN_SUBRING_GENERATED = prove + (`!r s x y:A. + x IN ring_carrier (subring_generated r s) /\ + y IN ring_carrier (subring_generated r s) + ==> ring_add r x y IN ring_carrier (subring_generated r s)`, + MESON_TAC[RING_ADD; SUBRING_GENERATED]);; + +let RING_MUL_IN_SUBRING_GENERATED = prove + (`!r s x y:A. + x IN ring_carrier (subring_generated r s) /\ + y IN ring_carrier (subring_generated r s) + ==> ring_mul r x y IN ring_carrier (subring_generated r s)`, + MESON_TAC[RING_MUL; SUBRING_GENERATED]);; + +let RING_POW_IN_SUBRING_GENERATED = prove + (`!r s (x:A) n. + x IN ring_carrier (subring_generated r s) + ==> ring_pow r x n IN ring_carrier (subring_generated r s)`, + MESON_TAC[RING_POW; RING_POW_SUBRING_GENERATED]);; + let SUBRING_GENERATED_RESTRICT = prove (`!r s:A->bool. subring_generated r s = @@ -2882,6 +2931,12 @@ let SUBRING_GENERATED_INC = prove REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; GSYM SUBSET] THEN REWRITE_TAC[SUBRING_GENERATED_SUBSET_CARRIER_SUBSET]);; +let SUBRING_GENERATED_INC_GEN = prove + (`!r s x:A. + x IN ring_carrier r /\ x IN s + ==> x IN ring_carrier(subring_generated r s)`, + MESON_TAC[SUBRING_GENERATED_SUBSET_CARRIER; IN_INTER; SUBSET]);; + let SUBRING_OF_SUBRING_GENERATED_REV = prove (`!r g h:A->bool. g subring_of (subring_generated r h) @@ -3935,6 +3990,20 @@ let IDEAL_GENERATED_SING_ALT = prove REWRITE_TAC[EXTENSION; IN_ELIM_THM; ring_divides] THEN ASM_MESON_TAC[RING_MUL]);; +let IN_IDEAL_GENERATED_SING_EQ = prove + (`!r x y:A. x IN ring_carrier r + ==> (y IN ideal_generated r {x} <=> ring_divides r x y)`, + SIMP_TAC[IDEAL_GENERATED_SING] THEN SET_TAC[]);; + +let IN_IDEAL_GENERATED_SING = prove + (`!r x y:A. ring_divides r x y ==> y IN ideal_generated r {x}`, + MESON_TAC[IN_IDEAL_GENERATED_SING_EQ; ring_divides]);; + +let IN_IDEAL_GENERATED_SELF = prove + (`!r x:A. x IN ideal_generated r {x} <=> x IN ring_carrier r`, + MESON_TAC[IN_IDEAL_GENERATED_SING; RING_DIVIDES_REFL; + IDEAL_GENERATED_SUBSET; SUBSET]);; + let IDEAL_GENERATED_SING_EQ_CARRIER = prove (`!r a:A. a IN ring_carrier r @@ -4925,6 +4994,37 @@ let RING_HOMOMORPHISM_POW = prove REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THEN ASM_SIMP_TAC[ring_pow; RING_POW]);; +let RING_HOMOMORPHISM_INV = prove + (`!r r' (f:A->B). + ring_homomorphism (r,r') f + ==> !x. ring_unit r x ==> f(ring_inv r x) = ring_inv r' (f x)`, + REPEAT STRIP_TAC THEN + SUBGOAL_THEN `(x:A) IN ring_carrier r` ASSUME_TAC THENL + [ASM_MESON_TAC[ring_unit]; ALL_TAC] THEN + CONV_TAC SYM_CONV THEN MATCH_MP_TAC RING_LINV_UNIQUE THEN + RULE_ASSUM_TAC(REWRITE_RULE[ring_homomorphism; SUBSET; FORALL_IN_IMAGE]) THEN + FIRST_X_ASSUM(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o GSYM)) THEN + ASM_SIMP_TAC[RING_INV] THEN DISCH_THEN(K ALL_TAC) THEN + AP_TERM_TAC THEN ASM_SIMP_TAC[RING_MUL_LINV]);; + +let FIELD_HOMOMORPHISM_INV = prove + (`!r r' (f:A->B). + field r /\ ring_homomorphism (r,r') f + ==> !x. x IN ring_carrier r ==> f(ring_inv r x) = ring_inv r' (f x)`, + REPEAT STRIP_TAC THEN ASM_CASES_TAC `x:A = ring_0 r` THENL + [ALL_TAC; ASM_MESON_TAC[RING_HOMOMORPHISM_INV; FIELD_UNIT]] THEN + RULE_ASSUM_TAC(REWRITE_RULE + [ring_homomorphism; SUBSET; FORALL_IN_IMAGE]) THEN + ASM_SIMP_TAC[RING_INV_0]);; + +let FIELD_HOMOMORPHISM_DIV = prove + (`!r r' (f:A->B). + field r /\ ring_homomorphism (r,r') f + ==> !x y. x IN ring_carrier r /\ y IN ring_carrier r + ==> f(ring_div r x y) = ring_div r' (f x) (f y)`, + REWRITE_TAC[ring_div] THEN + MESON_TAC[FIELD_HOMOMORPHISM_INV; RING_HOMOMORPHISM_MUL; RING_INV]);; + let RING_HOMOMORPHISM_RING_OF_NUM = prove (`!r r' (f:A->B). ring_homomorphism(r,r') f @@ -5246,6 +5346,13 @@ let RING_HOMOMORPHISM_BETWEEN_SUBRINGS_ALT = prove MESON_TAC[SUBRING_GENERATED_RESTRICT; RING_HOMOMORPHISM_BETWEEN_SUBRINGS]);; +let RING_MONOMORPHISM_INTO_SUBRING = prove + (`!r r' s (f:A->B). + ring_monomorphism (r,r') f /\ IMAGE f (ring_carrier r) SUBSET s + ==> ring_monomorphism (r,subring_generated r' s) f`, + REWRITE_TAC[ring_monomorphism] THEN + MESON_TAC[RING_HOMOMORPHISM_INTO_SUBRING]);; + let RING_MONOMORPHISM_BETWEEN_SUBRINGS = prove (`!r r' s t (f:A->B). ring_monomorphism(r,r') f /\ IMAGE f s SUBSET t @@ -5279,6 +5386,23 @@ let RING_SUM_SUBRING_GENERATED = prove REWRITE_TAC[RING_SUM_SUBRING_GENERATED_GEN] THEN SIMP_TAC[CARRIER_SUBRING_GENERATED_SUBRING]);; +let RING_PRODUCT_SUBRING_GENERATED_GEN = prove + (`!r s k (f:K->A). + ring_product (subring_generated r s) k f = + ring_product r + {x | x IN k /\ f x IN ring_carrier(subring_generated r s)} f`, + REPEAT GEN_TAC THEN MATCH_ACCEPT_TAC + (REWRITE_RULE[o_DEF; ETA_AX] (MATCH_MP RING_MONOMORPHISM_PRODUCT_GEN + (SPEC_ALL RING_MONOMORPHISM_INCLUSION))));; + +let RING_PRODUCT_SUBRING_GENERATED = prove + (`!r s k (f:K->A). + s subring_of r + ==> ring_product (subring_generated r s) k f = + ring_product r {x | x IN k /\ f x IN s} f`, + REWRITE_TAC[RING_PRODUCT_SUBRING_GENERATED_GEN] THEN + SIMP_TAC[CARRIER_SUBRING_GENERATED_SUBRING]);; + let SUBRING_GENERATED_BY_HOMOMORPHIC_IMAGE = prove (`!r r' (f:A->B) s. ring_homomorphism(r,r') f /\ s SUBSET ring_carrier r @@ -5478,32 +5602,32 @@ let RING_ISOMORPHISMS_ISOMORPHISM = prove MESON_TAC[RING_ISOMORPHISM_IMP_HOMOMORPHISM]]);; let RING_ISOMORPHISM_EQ_MONOMORPHISM_FINITE = prove - (`!G H (f:A->B). - FINITE(ring_carrier G) /\ FINITE(ring_carrier H) /\ - CARD(ring_carrier G) = CARD(ring_carrier H) - ==> (ring_isomorphism(G,H) f <=> ring_monomorphism(G,H) f)`, + (`!r r' (f:A->B). + FINITE(ring_carrier r) /\ FINITE(ring_carrier r') /\ + CARD(ring_carrier r) = CARD(ring_carrier r') + ==> (ring_isomorphism(r,r') f <=> ring_monomorphism(r,r') f)`, REPEAT STRIP_TAC THEN EQ_TAC THEN REWRITE_TAC[RING_ISOMORPHISM_IMP_MONOMORPHISM] THEN SIMP_TAC[GSYM RING_MONOMORPHISM_EPIMORPHISM] THEN SIMP_TAC[ring_monomorphism; ring_epimorphism] THEN REWRITE_TAC[ring_homomorphism] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN MP_TAC(ISPECL - [`ring_carrier G:A->bool`; `ring_carrier H:B->bool`; `f:A->B`] + [`ring_carrier r:A->bool`; `ring_carrier r':B->bool`; `f:A->B`] SURJECTIVE_IFF_INJECTIVE_GEN) THEN ASM_REWRITE_TAC[] THEN ASM SET_TAC[]);; let RING_ISOMORPHISM_EQ_EPIMORPHISM_FINITE = prove - (`!G H (f:A->B). - FINITE(ring_carrier G) /\ FINITE(ring_carrier H) /\ - CARD(ring_carrier G) = CARD(ring_carrier H) - ==> (ring_isomorphism(G,H) f <=> ring_epimorphism(G,H) f)`, + (`!r r' (f:A->B). + FINITE(ring_carrier r) /\ FINITE(ring_carrier r') /\ + CARD(ring_carrier r) = CARD(ring_carrier r') + ==> (ring_isomorphism(r,r') f <=> ring_epimorphism(r,r') f)`, REPEAT STRIP_TAC THEN EQ_TAC THEN REWRITE_TAC[RING_ISOMORPHISM_IMP_EPIMORPHISM] THEN SIMP_TAC[GSYM RING_MONOMORPHISM_EPIMORPHISM] THEN SIMP_TAC[ring_monomorphism; ring_epimorphism] THEN REWRITE_TAC[ring_homomorphism] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN MP_TAC(ISPECL - [`ring_carrier G:A->bool`; `ring_carrier H:B->bool`; `f:A->B`] + [`ring_carrier r:A->bool`; `ring_carrier r':B->bool`; `f:A->B`] SURJECTIVE_IFF_INJECTIVE_GEN) THEN ASM_REWRITE_TAC[] THEN ASM SET_TAC[]);; @@ -5779,9 +5903,9 @@ let ISOMORPHIC_TO_TRIVIAL_RING = prove REWRITE_TAC[lemma]);; let ISOMORPHIC_TRIVIAL_RINGS = prove - (`!(G:A ring) (H:B ring). - trivial_ring G /\ trivial_ring H - ==> G isomorphic_ring H`, + (`!(r:A ring) (r':B ring). + trivial_ring r /\ trivial_ring r' + ==> r isomorphic_ring r'`, MESON_TAC[ISOMORPHIC_TO_TRIVIAL_RING]);; let ISOMORPHIC_RING_SINGLETON_RING = prove @@ -5872,14 +5996,19 @@ let ISOMORPHIC_RING_CHAR = prove REWRITE_TAC[isomorphic_ring] THEN MESON_TAC[RING_ISOMORPHISM_IMP_MONOMORPHISM; RING_CHAR_MONOMORPHIC_IMAGE]);; -let ISOMORPHIC_COPY_OF_RING = prove - (`!(r:A ring) (s:B->bool). - (?r'. ring_carrier r' = s /\ r isomorphic_ring r') <=> - ring_carrier r =_c s`, - REPEAT GEN_TAC THEN EQ_TAC THENL - [MESON_TAC[ISOMORPHIC_RING_CARD_EQ; CARD_EQ_TRANS]; - REWRITE_TAC[EQ_C_BIJECTIONS; LEFT_IMP_EXISTS_THM]] THEN - MAP_EVERY X_GEN_TAC [`f:A->B`; `g:B->A`] THEN STRIP_TAC THEN +let ISOMORPHIC_TRANSPORT_OF_RING = prove + (`!(f:A->B) r. + (!x y. x IN ring_carrier r /\ y IN ring_carrier r /\ f x = f y + ==> x = y) + ==> ?r'. ring_isomorphism(r,r') f`, + REPEAT GEN_TAC THEN + REWRITE_TAC[INJECTIVE_ON_LEFT_INVERSE; LEFT_IMP_EXISTS_THM] THEN + X_GEN_TAC `g:B->A` THEN STRIP_TAC THEN + ABBREV_TAC `s = IMAGE (f:A->B) (ring_carrier r)` THEN + SUBGOAL_THEN + `(!x. x IN ring_carrier r ==> (f:A->B) x IN s) /\ + (!y. y IN s ==> g y IN ring_carrier r /\ f(g y) = y)` + STRIP_ASSUME_TAC THENL [ASM SET_TAC[]; FIRST_X_ASSUM(K ALL_TAC o SYM)] THEN ABBREV_TAC `r' = ring(s:B->bool, f (ring_0 r:A), @@ -5912,11 +6041,25 @@ let ISOMORPHIC_COPY_OF_RING = prove RING_ADD_LNEG; RING_MUL_SYM; RING_MUL_ASSOC; RING_MUL_LID; RING_ADD_LDISTRIB]; EXISTS_TAC `r':B ring` THEN ASM_REWRITE_TAC[isomorphic_ring] THEN - EXISTS_TAC `f:A->B` THEN REWRITE_TAC[ring_isomorphism] THEN + REWRITE_TAC[ring_isomorphism] THEN EXISTS_TAC `g:B->A` THEN REWRITE_TAC[ring_isomorphisms] THEN ASM_SIMP_TAC[ring_homomorphism; RING_0; RING_1; SUBSET; FORALL_IN_IMAGE; RING_NEG; RING_ADD; RING_MUL]]);; +let ISOMORPHIC_COPY_OF_RING = prove + (`!(r:A ring) (s:B->bool). + (?r'. ring_carrier r' = s /\ r isomorphic_ring r') <=> + ring_carrier r =_c s`, + REPEAT GEN_TAC THEN EQ_TAC THENL + [MESON_TAC[ISOMORPHIC_RING_CARD_EQ; CARD_EQ_TRANS]; + REWRITE_TAC[EQ_C_BIJECTIONS; LEFT_IMP_EXISTS_THM]] THEN + MAP_EVERY X_GEN_TAC [`f:A->B`; `g:B->A`] THEN STRIP_TAC THEN + MP_TAC(ISPECL [`f:A->B`; `r:A ring`] ISOMORPHIC_TRANSPORT_OF_RING) THEN + ANTS_TAC THENL [ASM_MESON_TAC[]; MATCH_MP_TAC MONO_EXISTS] THEN + REWRITE_TAC[isomorphic_ring] THEN REPEAT STRIP_TAC THENL + [ALL_TAC; ASM_MESON_TAC[]] THEN + RULE_ASSUM_TAC(REWRITE_RULE[RING_ISOMORPHISM]) THEN ASM SET_TAC[]);; + let ISOMORPHIC_SUBCOPY_OF_RING = prove (`!(r:A ring) (s:B->bool). ring_carrier r <=_c s @@ -15036,6 +15179,14 @@ let MONOMIAL_TAC = let MONOMIAL_RULE tm = prove(tm,MONOMIAL_TAC);; +let FINITE_MONOMIAL_VARS = prove + (`!m:V->num. FINITE(:V) ==> FINITE(monomial_vars m)`, + MESON_TAC[FINITE_SUBSET; SUBSET_UNIV]);; + +let FINITE_MONOMIAL_VARS_1 = prove + (`!m:1->num. FINITE(monomial_vars m)`, + MESON_TAC[FINITE_MONOMIAL_VARS; FINITE_1]);; + let MONOMIAL_DEG = prove (`!m:V->num. monomial_deg m = nsum UNIV m`, GEN_TAC THEN REWRITE_TAC[monomial_deg] THEN @@ -16008,6 +16159,36 @@ let POLY_CLAUSES = prove (!(r:A ring). poly_mul r = ring_mul (poly_ring r (:V)))`, REWRITE_TAC[POLY_RING_CLAUSES; SUBSET_UNIV]);; +let POLY_SUBRING_GENERATED_CLAUSES = prove + (`(forall (r:A ring) s (v:V->bool). + ring_0 (poly_ring (subring_generated r s) v) = + ring_0 (poly_ring r v)) /\ + (forall (r:A ring) s (v:V->bool). + ring_1 (poly_ring (subring_generated r s) v) = + ring_1 (poly_ring r v)) /\ + (forall (r:A ring) s (v:V->bool). + ring_neg (poly_ring (subring_generated r s) v) = + ring_neg (poly_ring r v)) /\ + (forall (r:A ring) s (v:V->bool). + ring_add (poly_ring (subring_generated r s) v) = + ring_add (poly_ring r v)) /\ + (forall (r:A ring) s (v:V->bool) p q. + (!m. p m IN ring_carrier(subring_generated r s)) /\ + (!m. q m IN ring_carrier(subring_generated r s)) + ==> ring_mul (poly_ring (subring_generated r s) v) p q = + ring_mul (poly_ring r v) p q) /\ + (forall (r:A ring) s (v:V->bool). + ring_sub (poly_ring (subring_generated r s) v) = + ring_sub (poly_ring r v))`, + REWRITE_TAC[POLY_RING_CLAUSES; poly_0; poly_1; poly_add; poly_neg; poly_mul; + poly_sub; poly_const; FUN_EQ_THM; CONJUNCT2 SUBRING_GENERATED; + RING_SUB_SUBRING_GENERATED; RING_SUM_SUBRING_GENERATED_GEN] THEN + REPEAT STRIP_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN + REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ; FORALL_IN_GSPEC; SUBSET; IMP_CONJ] THEN + REWRITE_TAC[IN_ELIM_PAIR_THM] THEN ONCE_REWRITE_TAC[IN_ELIM_THM] THEN + REWRITE_TAC[IN_ELIM_PAIR_THM] THEN + ASM_MESON_TAC[RING_MUL; CONJUNCT2 SUBRING_GENERATED]);; + let POWSER_MONOMIAL_IN_CARRIER = prove (`!r s (p:(V->num)->A) m. p IN ring_carrier (powser_ring r s) ==> p m IN ring_carrier r`, @@ -16489,6 +16670,12 @@ let poly_extend = new_definition (ring_product r' (monomial_vars m) (\i. ring_pow r' (x i) (m i))))`;; +let POLY_EXTEND_FROM_SUBRING_GENERATED = prove + (`!r s r'. + poly_extend(subring_generated r s,r'):(A->B)->(V->B)->((V->num)->A)->B = + poly_extend(r,r')`, + REWRITE_TAC[FUN_EQ_THM; poly_extend; CONJUNCT2 SUBRING_GENERATED]);; + let POLY_EXTEND = prove (`!r r' (h:A->B) p (x:V->B). poly_extend (r,r') h x p IN ring_carrier r'`, REWRITE_TAC[poly_extend; RING_SUM]);; @@ -16927,6 +17114,70 @@ let POLY_SUBRING_GENERATED = prove SIMP_TAC[SUBSET; FORALL_IN_GSPEC; POLY_VAR; POLY_CONST] THEN RULE_ASSUM_TAC(REWRITE_RULE[POLY_RING; poly_vars]) THEN ASM SET_TAC[]]);; +let POLY_SUBRING_GENERATED_1 = prove + (`!(r:A ring). + subring_generated (poly_ring r (:1)) + (poly_var r one INSERT IMAGE (poly_const r) (ring_carrier r)) = + poly_ring r (:1)`, + GEN_TAC THEN GEN_REWRITE_TAC RAND_CONV [GSYM POLY_SUBRING_GENERATED] THEN + AP_TERM_TAC THEN REWRITE_TAC[UNIV_1] THEN SET_TAC[]);; + +let IMAGE_POLY_EXTEND_1 = prove + (`!(f:A->B) k l a. + ring_homomorphism(k,l) f /\ a IN ring_carrier l + ==> IMAGE (poly_extend(k,l) f (\v. a)) + (ring_carrier(poly_ring k (:1))) = + ring_carrier + (subring_generated l (a INSERT IMAGE f (ring_carrier k)))`, + REPEAT STRIP_TAC THEN + MP_TAC(ISPECL [`poly_ring (k:A ring) (:1)`; `l:B ring`; + `poly_extend(k,l) (f:A->B) (\v:1. a)`; + `poly_var k one INSERT + IMAGE (poly_const k) (ring_carrier k:A->bool)`] + SUBRING_GENERATED_BY_HOMOMORPHIC_IMAGE) THEN + REWRITE_TAC[POLY_SUBRING_GENERATED_1] THEN + REWRITE_TAC[SUBSET; FORALL_IN_INSERT; FORALL_IN_IMAGE] THEN + ASM_SIMP_TAC[RING_HOMOMORPHISM_POLY_EXTEND; POLY_VAR_UNIV; POLY_CONST] THEN + DISCH_THEN(SUBST1_TAC o SYM) THEN AP_TERM_TAC THEN AP_TERM_TAC THEN + REWRITE_TAC[IMAGE_CLAUSES; GSYM IMAGE_o] THEN + ASM_SIMP_TAC[POLY_EXTEND_VAR] THEN AP_TERM_TAC THEN + MATCH_MP_TAC IMAGE_EQ THEN ASM_SIMP_TAC[o_THM; POLY_EXTEND_CONST]);; + +let POLY_EXTEND_INTO_SUBRING_GENERATED = prove + (`!r r' s (h:A->B) v (x:V->B) p. + p IN ring_carrier(poly_ring r v) /\ + ring_homomorphism(r,subring_generated r' s) h /\ + (!i. i IN v ==> x i IN ring_carrier(subring_generated r' s)) + ==> poly_extend (r,subring_generated r' s) h x p = + poly_extend (r,r') h x p`, + REPEAT STRIP_TAC THEN + SUBGOAL_THEN `!i. i IN v ==> (x:V->B) i IN ring_carrier r'` ASSUME_TAC THENL + [ASM_MESON_TAC[SUBSET; RING_CARRIER_SUBRING_GENERATED_SUBSET]; ALL_TAC] THEN + FIRST_ASSUM(ASSUME_TAC o GEN_REWRITE_RULE I + [RING_HOMOMORPHISM_INTO_SUBRING_EQ_GEN]) THEN + REWRITE_TAC[poly_extend; SUBRING_GENERATED; RING_POW_SUBRING_GENERATED] THEN + ONCE_REWRITE_TAC[GSYM SUBRING_GENERATED_BY_SUBRING_GENERATED] THEN + SIMP_TAC[RING_SUM_SUBRING_GENERATED; SUBRING_SUBRING_GENERATED] THEN + MATCH_MP_TAC(MESON[RING_SUM_EQ] + `s = t /\ (!x. x IN t ==> f x = g x) + ==> ring_sum r s f = ring_sum r t g`) THEN + REWRITE_TAC[IN_ELIM_THM] THEN CONJ_TAC THENL + [REWRITE_TAC[SET_RULE + `{x | P x /\ Q x} = {x | P x} <=> !x. P x ==> Q x`] THEN + X_GEN_TAC `m:V->num` THEN DISCH_TAC THEN + MATCH_MP_TAC RING_MUL_IN_SUBRING_GENERATED THEN + REWRITE_TAC[SUBRING_GENERATED_BY_SUBRING_GENERATED; RING_PRODUCT] THEN + FIRST_ASSUM(ASSUME_TAC o MATCH_MP POLY_MONOMIAL_IN_CARRIER) THEN + RULE_ASSUM_TAC(REWRITE_RULE[ring_homomorphism]) THEN ASM SET_TAC[]; + X_GEN_TAC `m:V->num` THEN DISCH_TAC THEN AP_TERM_TAC] THEN + SIMP_TAC[RING_PRODUCT_SUBRING_GENERATED; SUBRING_SUBRING_GENERATED] THEN + CONV_TAC SYM_CONV THEN MATCH_MP_TAC RING_PRODUCT_SUPERSET THEN + REWRITE_TAC[SUBSET_RESTRICT; IN_ELIM_THM] THEN X_GEN_TAC `i:V` THEN + MATCH_MP_TAC(TAUT `(p ==> r) ==> p /\ ~(p /\ r) ==> s`) THEN + DISCH_TAC THEN MATCH_MP_TAC RING_POW_IN_SUBRING_GENERATED THEN + RULE_ASSUM_TAC(REWRITE_RULE[POLY_RING; poly_vars; IN_ELIM_THM]) THEN + ASM SET_TAC[]);; + (* ------------------------------------------------------------------------- *) (* Some "natural" isomorphisms between polynomial / power series variants. *) (* ------------------------------------------------------------------------- *) @@ -18417,6 +18668,11 @@ let poly_deg = new_definition `poly_deg r (p:(V->num)->A) = minimal d. !m. ~(p m = ring_0 r) ==> monomial_deg m <= d`;; +let POLY_DEG_SUBRING_GENERATED = prove + (`!r s (p:(V->num)->A). + poly_deg (subring_generated r s) p = poly_deg r p`, + REWRITE_TAC[poly_deg; CONJUNCT2 SUBRING_GENERATED]);; + let POLY_DEG_CONST = prove (`!r c. poly_deg r (poly_const r c:(V->num)->A) = 0`, REPEAT GEN_TAC THEN REWRITE_TAC[poly_deg; poly_const] THEN @@ -19153,6 +19409,19 @@ let POLY_EVAL_AT_0 = prove REPEAT STRIP_TAC THEN REWRITE_TAC[poly_eval; GSYM monomial_1] THEN ASM_MESON_TAC[POLY_EVALUATE_AT_0]);; +let IMAGE_POLY_EVAL = prove + (`!l k a:A. + k subring_of l /\ a IN ring_carrier l + ==> IMAGE (\p. poly_eval l p a) + (ring_carrier(poly_ring (subring_generated l k) (:1))) = + ring_carrier (subring_generated l (a INSERT k))`, + REPEAT STRIP_TAC THEN REWRITE_TAC[poly_eval; poly_evaluate; ETA_AX] THEN + MP_TAC(ISPECL [`I:A->A`; `subring_generated l k:A ring`; `l:A ring`; `a:A`] + IMAGE_POLY_EXTEND_1) THEN + ASM_SIMP_TAC[CARRIER_SUBRING_GENERATED_SUBRING; IMAGE_I; + RING_HOMOMORPHISM_FROM_SUBRING_GENERATED; + RING_HOMOMORPHISM_I; POLY_EXTEND_FROM_SUBRING_GENERATED]);; + (* ------------------------------------------------------------------------- *) (* Composing polynomials and power series with homomorphisms. *) (* ------------------------------------------------------------------------- *) diff --git a/bignum_zarith.ml b/bignum_zarith.ml index 7f370680..a7df4e9a 100644 --- a/bignum_zarith.ml +++ b/bignum_zarith.ml @@ -106,7 +106,7 @@ module Num = struct let exp_i = int_of_num exponent in Q.of_bigint (Z.pow (Q.to_bigint base) exp_i) in if ge_num exponent (num_of_int 0) then f base exponent - else div_num (num_of_int 1) (f base (minus_num exponent));; + else div_num (num_of_int 1) (f base (minus_num exponent));; end;; diff --git a/int.ml b/int.ml index 1cbe561f..922de631 100755 --- a/int.ml +++ b/int.ml @@ -2207,7 +2207,7 @@ 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]]]) and BETA2_CONV = RATOR_CONV BETA_CONV THENC BETA_CONV and div_tm = `(div):int->int->int` and rem_tm = `(rem):int->int->int` diff --git a/realax.ml b/realax.ml index 2ec66972..ad27c84c 100644 --- a/realax.ml +++ b/realax.ml @@ -245,7 +245,9 @@ let BOUNDS_IGNORE = prove REWRITE_TAC[LE_ADD]]]]);; (* ------------------------------------------------------------------------- *) -(* Define type of nearly additive functions. *) +(* Define type of nearly-multiplicative functions. This is equivalent to *) +(* being nearly-additive, hence the name, but it is easier to work with this *) +(* formulation rather than actually derive it from nearly-additivity. *) (* ------------------------------------------------------------------------- *) let is_nadd = new_definition @@ -262,7 +264,7 @@ override_interface ("fn",`dest_nadd`);; override_interface ("afn",`mk_nadd`);; (* ------------------------------------------------------------------------- *) -(* Properties of nearly-additive functions. *) +(* Properties of nearly-multiplicative / nearly-additive functions. *) (* ------------------------------------------------------------------------- *) let NADD_CAUCHY = prove diff --git a/trivia.ml b/trivia.ml index 23d68ec4..4e9d06ea 100644 --- a/trivia.ml +++ b/trivia.ml @@ -92,6 +92,11 @@ let EXISTS_ONE_THM = prove GEN_REWRITE_TAC I [TAUT `(p <=> q) <=> (~p <=> ~q)`] THEN REWRITE_TAC[NOT_EXISTS_THM; FORALL_ONE_THM]);; +let ETA_ONE = prove + (`!f:1->A. (\x. f one) = f`, + REWRITE_TAC[FUN_EQ_THM] THEN REPEAT GEN_TAC THEN + ONCE_REWRITE_TAC[one] THEN REFL_TAC);; + (* ------------------------------------------------------------------------- *) (* Add the type "1" to the inductive type store. *) (* ------------------------------------------------------------------------- *)