diff --git a/CHANGES b/CHANGES index 59ae1e40..95154c8e 100644 --- a/CHANGES +++ b/CHANGES @@ -8,6 +8,180 @@ * page: https://github.com/jrh13/hol-light/commits/master * * ***************************************************************** +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 +target version for "make switch", as well as reorganizing this and previous +pa_j files into a subdirectory with a README to explain how they are put +together. + +Sat 6th Jul 2024 holtest, holtest.ml, holtest_parallel + +Merged an update from June Lee making the various HOL test files use the +"hol.sh" script to invoke HOL Light. + +Fri 5th Jul 2024 EC/passim + +Added a couple more theorems (easy consequences of existing ones) for +each one of the various Weierstrass curves, all analogs of the +following for P-256: + + P256_GROUP_ELEMENT_ORDER = + |- !P. P IN group_carrier p256_group + ==> group_element_order p256_group P = + if P = group_id p256_group then 1 else n_256 + + P256_GROUP_ORDER = + |- CARD(group_carrier p256_group) = n_256 + +with the complete list of new theorems being + + P192K1_GROUP_ELEMENT_ORDER + P192K1_GROUP_ORDER + P192_GROUP_ELEMENT_ORDER + P192_GROUP_ORDER + P224K1_GROUP_ELEMENT_ORDER + P224K1_GROUP_ORDER + P224_GROUP_ELEMENT_ORDER + P256K1_GROUP_ELEMENT_ORDER + P256K1_GROUP_ORDER + P256_GROUP_ELEMENT_ORDER + P256_GROUP_ORDER + P256_GROUP_ORDER + P384_GROUP_ELEMENT_ORDER + P384_GROUP_ORDER + P521_GROUP_ELEMENT_ORDER + P521_GROUP_ORDER + +Also consistently renamed all the following existing theorems: + + FINITE_GROUP_CARRIER_192 -> FINITE_GROUP_CARRIER_P192 + FINITE_GROUP_CARRIER_192K1 -> FINITE_GROUP_CARRIER_P192K1 + FINITE_GROUP_CARRIER_224 -> FINITE_GROUP_CARRIER_P224 + FINITE_GROUP_CARRIER_224K1 -> FINITE_GROUP_CARRIER_P224K1 + FINITE_GROUP_CARRIER_256 -> FINITE_GROUP_CARRIER_P256 + FINITE_GROUP_CARRIER_256K1 -> FINITE_GROUP_CARRIER_P256K1 + FINITE_GROUP_CARRIER_384 -> FINITE_GROUP_CARRIER_P384 + FINITE_GROUP_CARRIER_521 -> FINITE_GROUP_CARRIER_P521 + +Wed 3rd Jul 2024 Library/prime.ml + +Added a little lemma that is trivial to construct but handy sometimes: + + DIVIDES_EQ_ZERO = |- !p n. n < p ==> (p divides n <=> n = 0) + +Wed 3rd Jul 2024 Library/grouptheory.ml + +Added a few elementary group lemmas: + + GROUP_ELEMENT_ORDER_PRIME = + |- !G a. + prime p /\ group_carrier G HAS_SIZE p /\ a IN group_carrier G + ==> group_element_order G a = + (if a = group_id G then 1 else CARD (group_carrier G)) + + GROUP_POW_MOD_ELEMENT_ORDER = + |- !G x n. + x IN group_carrier G + ==> group_pow G x (n MOD group_element_order G x) = group_pow G x n + + GROUP_POW_MOD_ORDER = + |- !G x n. + FINITE (group_carrier G) /\ x IN group_carrier G + ==> group_pow G x (n MOD CARD (group_carrier G)) = group_pow G x n + + GROUP_ZPOW_INV = + |- !G x n. + x IN group_carrier G + ==> group_zpow G (group_inv G x) n = group_zpow G x (--n) + + GROUP_ZPOW_REM_ELEMENT_ORDER = + |- !G x n. + x IN group_carrier G + ==> group_zpow G x (n rem &(group_element_order G x)) = + group_zpow G x n + + GROUP_ZPOW_REM_ORDER = + |- !G x n. + FINITE (group_carrier G) /\ x IN group_carrier G + ==> group_zpow G x (n rem &(CARD (group_carrier G))) = + group_zpow G x n + +Fri 28th Jun 2024 Library/ringtheory.ml + +Added more elementary ring lemmas including characterizations of units and +nilpotents in polynomial rings: + + IN_SUBRING_PRODUCT = + |- !r h f s. + h subring_of r /\ (!a. a IN s ==> f a IN h) + ==> ring_product r s f IN h + + IN_SUBRING_SUM = + |- !r h f s. + h subring_of r /\ (!a. a IN s ==> f a IN h) ==> ring_sum r s f IN h + + MONOMIAL_VAR_1 = + |- (!v. ~(monomial_var v = monomial_1)) /\ + (!v. ~(monomial_1 = monomial_var v)) + + POLY_EVALUATE_AT_0 = + |- !r p. + p IN ring_carrier (poly_ring r v) + ==> poly_evaluate r p (\x. ring_0 r) = p monomial_1 + + POLY_EVAL_AT_0 = + |- !r p. + p IN ring_carrier (poly_ring r (:1)) + ==> poly_eval r p (ring_0 r) = p (\v. 0) + + POLY_EXTEND_AT_0 = + |- !r s v h p. + ring_homomorphism (r,s) h /\ p IN ring_carrier (poly_ring r v) + ==> poly_extend (r,s) h (\x. ring_0 s) p = h (p monomial_1) + + POLY_MUL_MONOMIAL_1 = + |- !r p q. + ring_polynomial r p /\ ring_polynomial r q + ==> poly_mul r p q monomial_1 = + ring_mul r (p monomial_1) (q monomial_1) + + POLY_SUBRING_GENERATED = + |- !r s. + subring_generated (poly_ring r s) + ({poly_const r c | c | c IN ring_carrier r} UNION + {poly_var r x | x IN s}) = + poly_ring r s + + RING_HOMOMORPHISM_MONOMIAL_1 = + |- !r v. ring_homomorphism (poly_ring r v,r) (\p. p monomial_1) + + RING_NILPOTENT_POLY_RING = + |- !r s p. + ring_nilpotent (poly_ring r s) p <=> + p IN ring_carrier (poly_ring r s) /\ (!m. ring_nilpotent r (p m)) + + RING_NILPOTENT_SUM = + |- !r f s. + FINITE s /\ (!i. i IN s ==> ring_nilpotent r (f i)) + ==> ring_nilpotent r (ring_sum r s f) + + RING_UNIT_POLY_CONST = + |- !r s c. ring_unit (poly_ring r s) (poly_const r c) <=> ring_unit r c + + RING_UNIT_POLY_DOMAIN = + |- !r s p. + integral_domain r + ==> (ring_unit (poly_ring r s) p <=> + (?c. ring_unit r c /\ p = poly_const r c)) + + RING_UNIT_POLY_RING = + |- !r s p. + ring_unit (poly_ring r s) p <=> + p IN ring_carrier (poly_ring r s) /\ + ring_unit r (p monomial_1) /\ + (!m. ~(m = monomial_1) ==> ring_nilpotent r (p m)) + Sun 9th Jun 2024 Library/ringtheory.ml Added a slew of further elementary definitions and theorems about rings, in @@ -18,130 +192,130 @@ is now used for a slightly different theorem. New definitions: local_ring = |- !r. local_ring r <=> (?!j. maximal_ideal r j) - + poly_deg = |- !p r. poly_deg r p = (minimal d. !m. ~(p m = ring_0 r) ==> monomial_deg m <= d) - + poly_eval = |- !r p x. poly_eval r p x = poly_evaluate r p (\v. x) - + poly_evaluate = |- !r x p. poly_evaluate r p x = poly_extend (r,r) I x p - + poly_sub = |- !r p1 p2. poly_sub r p1 p2 = (\m. ring_sub r (p1 m) (p2 m)) and theorems: - + EUCLIDEAN_POLY_RING = |- !f. field f ==> euclidean_ring (poly_ring f (:1)) - + EXISTS_FUN_FROM_1 = |- !P. (?f. P (f one) f) <=> (?z. P z (\v. z)) - + FIELD_IMP_LOCAL_RING = |- !r. field r ==> local_ring r - + FORALL_FUN_FROM_1 = |- !P. (!f. P (f one) f) <=> (!z. P z (\v. z)) - + INTEGER_QUOTIENT_RING_ISOMORPHIC_MOD = |- quotient_ring integer_ring (ideal_generated integer_ring {&n}) isomorphic_ring integer_mod_ring n - + INTEGER_RING_COSET_IDEAL_GENERATED_SING = |- !n. ring_coset integer_ring (ideal_generated integer_ring {n}) = mod n - + INTEGER_RING_IDEAL_GENERATED_SING = |- !n. ideal_generated integer_ring {n} = {x | n divides x} - + IN_POLY_RING_CARRIER = |- !r s. p IN ring_carrier (poly_ring r s) <=> ring_polynomial r p /\ poly_vars r p SUBSET s - + IN_RING_COSET = |- !r j x y. (ring_ideal r j \/ j subring_of r) /\ x IN ring_carrier r /\ y IN ring_carrier r ==> (x IN ring_coset r j y <=> ring_coset r j x = ring_coset r j y) - + IN_RING_POLYNOMIAL_CARRIER_COMPOSE = |- !r s f v p. ring_homomorphism (r,s) f /\ p IN ring_carrier (poly_ring r v) ==> f o p IN ring_carrier (poly_ring s v) - + IN_RING_POWERSERIES_CARRIER_COMPOSE = |- !r s v f p. ring_homomorphism (r,s) f /\ p IN ring_carrier (powser_ring r v) ==> f o p IN ring_carrier (powser_ring s v) - + ISOMORPHIC_RING_LOCALITY = |- !r r'. r isomorphic_ring r' ==> (local_ring r <=> local_ring r') - + ISOMORPHIC_SUBCOPY_OF_RING = |- !r s. ring_carrier r <=_c s ==> (?r'. ring_carrier r' SUBSET s /\ r isomorphic_ring r') - + LOCAL_IMP_NONTRIVIAL_RING = |- !r. local_ring r ==> ~trivial_ring r - + LOCAL_POWSER_RING = |- !r s. local_ring r ==> local_ring (powser_ring r s) - + LOCAL_QUOTIENT_RING = |- !r j. local_ring r /\ proper_ideal r j ==> local_ring (quotient_ring r j) - + LOCAL_RING_EPIMORPHIC_IMAGE = |- !r r' f. ring_epimorphism (r,r') f /\ local_ring r /\ ~trivial_ring r' ==> local_ring r' - + LOCAL_RING_IDEAL_NONUNITS = |- !r. local_ring r <=> ring_ideal r {x | x IN ring_carrier r /\ ~ring_unit r x} - + LOCAL_RING_LOCALIZATION = |- !r j. prime_ideal r j ==> local_ring (ring_localization r (ring_carrier r DIFF j)) - + MAXIMAL_CONTAINING_IDEAL_EXISTS = |- !r a. a IN ring_carrier r /\ ~ring_unit r a ==> (?j. maximal_ideal r j /\ a IN j) - + MAXIMAL_IDEAL_NONUNITS = |- !r. maximal_ideal r {x | x IN ring_carrier r /\ ~ring_unit r x} <=> ring_ideal r {x | x IN ring_carrier r /\ ~ring_unit r x} - + MONOMIAL_DEG = |- !m. monomial_deg m = nsum (:V) m - + MONOMIAL_DEG_LE_POLY_DEG = |- !r p m. ring_polynomial r p /\ ~(p m = ring_0 r) ==> monomial_deg m <= poly_deg r p - + MONOMIAL_DEG_UNIVARIATE = |- !i. monomial_deg (\v. i) = i - + MONOMIAL_VARS_UNIVARIATE = |- !i. monomial_vars (\v. i) = (if i = 0 then {} else {one}) - + PID_POLY_RING = |- !f. field f ==> PID (poly_ring f (:1)) - + POLY_0 = |- !r. poly_0 r = (\m. ring_0 r) - + POLY_CLAUSES = |- (!r. {p | ring_polynomial r p} = ring_carrier (poly_ring r (:V))) /\ (!r. poly_0 r = ring_0 (poly_ring r (:V))) /\ @@ -150,87 +324,87 @@ and theorems: (!r. poly_add r = ring_add (poly_ring r (:V))) /\ (!r. poly_sub r = ring_sub (poly_ring r (:V))) /\ (!r. poly_mul r = ring_mul (poly_ring r (:V))) - + POLY_CONST_1 = |- !r. poly_const r (ring_1 r) = poly_1 r - + POLY_DEG_0 = |- !r. poly_deg r (poly_0 r) = 0 - + POLY_DEG_1 = |- !r. poly_deg r (poly_1 r) = 0 - + POLY_DEG_ADD = |- !r p q. ring_polynomial r p /\ ring_polynomial r q /\ ~(poly_deg r p = poly_deg r q) ==> poly_deg r (poly_add r p q) = MAX (poly_deg r p) (poly_deg r q) - + POLY_DEG_ADD_LE = |- !r p q. ring_polynomial r p /\ ring_polynomial r q ==> poly_deg r (poly_add r p q) <= MAX (poly_deg r p) (poly_deg r q) - + POLY_DEG_CONST = |- !r c. poly_deg r (poly_const r c) = 0 - + POLY_DEG_EQ = |- !r p n. ring_polynomial r p ==> (poly_deg r p = n <=> (!m. ~(p m = ring_0 r) ==> monomial_deg m <= n) /\ (n = 0 \/ (?m. ~(p m = ring_0 r) /\ monomial_deg m = n))) - + POLY_DEG_EQ_0 = |- !r p. ring_polynomial r p ==> (poly_deg r p = 0 <=> (?c. c IN ring_carrier r /\ p = poly_const r c)) - + POLY_DEG_EQ_0_ALT = |- !r p. ring_polynomial r p ==> (poly_deg r p = 0 <=> p = poly_const r (p monomial_1)) - + POLY_DEG_GE = |- !r p m n. ring_polynomial r p /\ ~(p m = ring_0 r) /\ n <= monomial_deg m ==> n <= poly_deg r p - + POLY_DEG_GE_EQ = |- !r p n. ring_polynomial r p ==> (n <= poly_deg r p <=> n = 0 \/ (?m. ~(p m = ring_0 r) /\ n <= monomial_deg m)) - + POLY_DEG_HOMOMORPHIC_IMAGE = |- !r s f p. ring_homomorphism (r,s) f /\ ring_polynomial r p ==> poly_deg s (f o p) <= poly_deg r p - + POLY_DEG_LE = |- !r p n. ring_polynomial r p /\ (!m. ~(p m = ring_0 r) ==> monomial_deg m <= n) ==> poly_deg r p <= n - + POLY_DEG_LE_EQ = |- !r p n. ring_polynomial r p ==> (poly_deg r p <= n <=> (!m. ~(p m = ring_0 r) ==> monomial_deg m <= n)) - + POLY_DEG_MONOMIAL_EXISTS = |- !r p. ring_polynomial r p /\ ~(p = poly_0 r) ==> (?m. ~(p m = ring_0 r) /\ monomial_deg m = poly_deg r p) - + POLY_DEG_MONOMORPHIC_IMAGE = |- !r s f p. ring_monomorphism (r,s) f /\ ring_polynomial r p ==> poly_deg s (f o p) = poly_deg r p - + POLY_DEG_MUL = |- !r p q. integral_domain r /\ @@ -238,15 +412,15 @@ and theorems: ring_polynomial r q /\ (p = poly_0 r <=> q = poly_0 r) ==> poly_deg r (poly_mul r p q) = poly_deg r p + poly_deg r q - + POLY_DEG_MUL_LE = |- !r p q. ring_polynomial r p /\ ring_polynomial r q ==> poly_deg r (poly_mul r p q) <= poly_deg r p + poly_deg r q - + POLY_DEG_NEG = |- !r p. ring_polynomial r p ==> poly_deg r (poly_neg r p) = poly_deg r p - + POLY_DEG_RING_ADD_LE = |- !r s p q n. p IN ring_carrier (poly_ring r s) /\ @@ -254,7 +428,7 @@ and theorems: poly_deg r p <= n /\ poly_deg r q <= n ==> poly_deg r (ring_add (poly_ring r s) p q) <= n - + POLY_DEG_RING_SUB_LE = |- !r s p q n. p IN ring_carrier (poly_ring r s) /\ @@ -262,7 +436,7 @@ and theorems: poly_deg r p <= n /\ poly_deg r q <= n ==> poly_deg r (ring_sub (poly_ring r s) p q) <= n - + POLY_DEG_RING_SUM_LE = |- !r s f k n. FINITE k /\ @@ -271,41 +445,41 @@ and theorems: ==> f i IN ring_carrier (poly_ring r s) /\ poly_deg r (f i) <= n) ==> poly_deg r (ring_sum (poly_ring r s) k f) <= n - + POLY_DEG_SUB = |- !r p q. ring_polynomial r p /\ ring_polynomial r q /\ ~(poly_deg r p = poly_deg r q) ==> poly_deg r (poly_sub r p q) = MAX (poly_deg r p) (poly_deg r q) - + POLY_DEG_SUB_LE = |- !r p q. ring_polynomial r p /\ ring_polynomial r q ==> poly_deg r (poly_sub r p q) <= MAX (poly_deg r p) (poly_deg r q) - + POLY_DEG_UNIQUE = |- !r p n. ring_polynomial r p /\ (!m. ~(p m = ring_0 r) ==> monomial_deg m <= n) /\ (n = 0 \/ (?m. ~(p m = ring_0 r) /\ monomial_deg m = n)) ==> poly_deg r p = n - + POLY_DEG_VAR = |- !r. poly_deg r (poly_var r v) = (if ring_1 r = ring_0 r then 0 else 1) - + POLY_DEG_VAR_POW = |- !r s i k. poly_deg r (ring_pow (poly_ring r s) (poly_var r i) k) = (if ring_1 r = ring_0 r then 0 else k) - + POLY_DIVIDES_X_MINUS_A = |- !r a p. a IN ring_carrier r /\ p IN ring_carrier (poly_ring r (:1)) ==> ring_divides (poly_ring r (:1)) (poly_sub r (poly_var r one) (poly_const r a)) (poly_sub r p (poly_const r (poly_eval r p a))) - + POLY_DIVIDES_X_MINUS_ROOT = |- !r a p. a IN ring_carrier r /\ @@ -314,7 +488,7 @@ and theorems: ==> ring_divides (poly_ring r (:1)) (poly_sub r (poly_var r one) (poly_const r a)) p - + POLY_DIVIDES_X_MINUS_ROOT_EQ = |- !r a p. a IN ring_carrier r /\ p IN ring_carrier (poly_ring r (:1)) @@ -322,7 +496,7 @@ and theorems: (poly_sub r (poly_var r one) (poly_const r a)) p <=> poly_eval r p a = ring_0 r) - + POLY_DIVISION = |- !f p d. field f /\ @@ -338,7 +512,7 @@ and theorems: (ring_mul (poly_ring f (:1)) q d) t = p) - + POLY_DIVISION_GEN = |- !r p d. p IN ring_carrier (poly_ring r (:1)) /\ @@ -353,47 +527,47 @@ and theorems: (ring_mul (poly_ring r (:1)) q d) t = p) - + POLY_EQ_0_MONOMORPHIC_IMAGE = |- !r s f p. ring_monomorphism (r,s) f /\ ring_polynomial r p ==> (f o p = poly_0 s <=> p = poly_0 r) - + POLY_EVAL = |- !r p x. poly_eval r p x IN ring_carrier r - + POLY_EVALUATE = |- !r p x. poly_evaluate r p x IN ring_carrier r - + POLY_EVALUATE_0 = |- !r x. poly_evaluate r (poly_0 r) x = ring_0 r - + POLY_EVALUATE_1 = |- !r x. poly_evaluate r (poly_1 r) x = ring_1 r - + POLY_EVALUATE_ADD = |- !r p q x. ring_polynomial r p /\ ring_polynomial r q ==> poly_evaluate r (poly_add r p q) x = ring_add r (poly_evaluate r p x) (poly_evaluate r q x) - + POLY_EVALUATE_CONST = |- !r a x. a IN ring_carrier r ==> poly_evaluate r (poly_const r a) x = a - + POLY_EVALUATE_EQ = |- !r s p x y. (!i. i IN s ==> x i IN ring_carrier r) /\ (!i. i IN s ==> x i = y i) /\ p IN ring_carrier (poly_ring r s) ==> poly_evaluate r p x = poly_evaluate r p y - + POLY_EVALUATE_HOMOMORPHIC_IMAGE = |- !r s x f v p. ring_homomorphism (r,s) f /\ IMAGE x v SUBSET ring_carrier r /\ p IN ring_carrier (poly_ring r v) ==> f (poly_evaluate r p x) = poly_evaluate s (f o p) (f o x) - + POLY_EVALUATE_MUL = |- !r p q x. ring_polynomial r p /\ @@ -403,60 +577,60 @@ and theorems: ==> x i IN ring_carrier r) ==> poly_evaluate r (poly_mul r p q) x = ring_mul r (poly_evaluate r p x) (poly_evaluate r q x) - + POLY_EVALUATE_SUB = |- !r p q x. ring_polynomial r p /\ ring_polynomial r q ==> poly_evaluate r (poly_sub r p q) x = ring_sub r (poly_evaluate r p x) (poly_evaluate r q x) - + POLY_EVALUATE_VAR = |- !r i x. x i IN ring_carrier r ==> poly_evaluate r (poly_var r i) x = x i - + POLY_EVAL_0 = |- !r x. poly_eval r (poly_0 r) x = ring_0 r - + POLY_EVAL_1 = |- !r x. poly_eval r (poly_1 r) x = ring_1 r - + POLY_EVAL_ADD = |- !r p q x. ring_polynomial r p /\ ring_polynomial r q ==> poly_eval r (poly_add r p q) x = ring_add r (poly_eval r p x) (poly_eval r q x) - + POLY_EVAL_CONST = |- !r a x. a IN ring_carrier r ==> poly_eval r (poly_const r a) x = a - + POLY_EVAL_EXPAND = |- !r x p. x IN ring_carrier r /\ p IN ring_carrier (poly_ring r (:1)) ==> poly_eval r p x = ring_sum r (0..poly_deg r p) (\i. ring_mul r (p (\v. i)) (ring_pow r x i)) - + POLY_EVAL_HOMOMORPHIC_IMAGE = |- !r s x f p. ring_homomorphism (r,s) f /\ x IN ring_carrier r /\ p IN ring_carrier (poly_ring r (:1)) ==> f (poly_eval r p x) = poly_eval s (f o p) (f x) - + POLY_EVAL_MUL = |- !r p q x. ring_polynomial r p /\ ring_polynomial r q /\ x IN ring_carrier r ==> poly_eval r (poly_mul r p q) x = ring_mul r (poly_eval r p x) (poly_eval r q x) - + POLY_EVAL_SUB = |- !r p q x. ring_polynomial r p /\ ring_polynomial r q ==> poly_eval r (poly_sub r p q) x = ring_sub r (poly_eval r p x) (poly_eval r q x) - + POLY_EVAL_VAR = |- !r x. x IN ring_carrier r ==> poly_eval r (poly_var r one) x = x - + POLY_EXPAND = |- !r p. p IN ring_carrier (poly_ring r (:1)) @@ -465,7 +639,7 @@ and theorems: (\i. ring_mul (poly_ring r (:1)) (poly_const r (p (\v. i))) (ring_pow (poly_ring r (:1)) (poly_var r one) i)) - + POLY_EXTEND_EQ = |- !r r' s h k x y p. ring_homomorphism (r,r') h /\ @@ -474,12 +648,12 @@ and theorems: (!i. i IN s ==> x i = y i) /\ p IN ring_carrier (poly_ring r s) ==> poly_extend (r,r') h x p = poly_extend (r,r') k y p - + POLY_EXTEND_EVALUATE = |- !r s f x p. ring_homomorphism (r,s) f ==> poly_extend (r,s) f x p = poly_evaluate s (f o p) x - + POLY_EXTEND_HOMOMORPHIC_IMAGE = |- !r s t h v x f p. ring_homomorphism (r,s) h /\ @@ -488,7 +662,7 @@ and theorems: p IN ring_carrier (poly_ring r v) ==> f (poly_extend (r,s) h x p) = poly_extend (r,t) (f o h) (f o x) p - + POLY_EXTEND_SUB = |- !r r' h x p1 p2. ring_homomorphism (r,r') h /\ @@ -497,7 +671,7 @@ and theorems: ==> poly_extend (r,r') h x (poly_sub r p1 p2) = ring_sub r' (poly_extend (r,r') h x p1) (poly_extend (r,r') h x p2) - + POLY_EXTEND_UNIVARIATE = |- !r r' h x p. ring_homomorphism (r,r') h /\ @@ -506,23 +680,23 @@ and theorems: ==> poly_extend (r,r') h x p = ring_sum r' (0..poly_deg r p) (\i. ring_mul r' (h (p (\v. i))) (ring_pow r' (x one) i)) - + POLY_MONOMIALS = |- !r s m. p IN ring_carrier (poly_ring r s) /\ ~(p m = ring_0 r) ==> monomial s m - + POLY_MONOMIALS_FINITE = |- !r s. p IN ring_carrier (poly_ring r s) ==> FINITE {m | ~(p m = ring_0 r)} - + POLY_MONOMIAL_IN_CARRIER = |- !r s p m. p IN ring_carrier (poly_ring r s) ==> p m IN ring_carrier r - + POLY_MUL_0 = |- (!r p. ring_polynomial r p ==> poly_mul r p (poly_0 r) = poly_0 r) /\ (!r q. ring_polynomial r q ==> poly_mul r (poly_0 r) q = poly_0 r) - + POLY_RING_CLAUSES = |- (!r s. ring_carrier (poly_ring r s) = @@ -533,7 +707,7 @@ and theorems: (!r s. ring_add (poly_ring r s) = poly_add r) /\ (!r s. ring_sub (poly_ring r s) = poly_sub r) /\ (!r s. ring_mul (poly_ring r s) = poly_mul r) - + POLY_ROOT_BOUND = |- !r p. integral_domain r /\ @@ -542,10 +716,10 @@ and theorems: ==> FINITE {x | x IN ring_carrier r /\ poly_eval r p x = ring_0 r} /\ CARD {x | x IN ring_carrier r /\ poly_eval r p x = ring_0 r} <= poly_deg r p - + POLY_SUB = |- !r p q. poly_sub r p q = poly_add r p (poly_neg r q) - + POLY_TOP_MONOMIAL_LE = |- !(<<=) r p. toset (<<=) /\ @@ -558,7 +732,7 @@ and theorems: (!m'. ~(p m' = ring_0 r) /\ monomial_deg m' = poly_deg r p ==> monomial_le (<<=) m' m)) - + POLY_TOP_MONOMIAL_LT = |- !(<<=) r p. toset (<<=) /\ @@ -573,13 +747,13 @@ and theorems: monomial_deg m' = poly_deg r p /\ ~(m' = m) ==> monomial_lt (<<=) m' m)) - + POLY_TOP_NONZERO = |- !r p. p IN ring_carrier (poly_ring r (:1)) /\ ~(p = ring_0 (poly_ring r (:1))) ==> ~(p (\v. poly_deg r p) = ring_0 r) - + POLY_TOP_TAIL = |- !r p. p IN ring_carrier (poly_ring r (:1)) /\ @@ -595,118 +769,118 @@ and theorems: (poly_deg r p))) q = p) - + POLY_VAR_UNIV = |- !r i. poly_var r i IN ring_carrier (poly_ring r (:V)) - + POWSER_MONOMIALS = |- !r s m. p IN ring_carrier (powser_ring r s) /\ ~(p m = ring_0 r) ==> monomial s m - + POWSER_MONOMIAL_IN_CARRIER = |- !r s p m. p IN ring_carrier (powser_ring r s) ==> p m IN ring_carrier r - + POWSER_VAR_UNIV = |- !r i. poly_var r i IN ring_carrier (powser_ring r (:V)) - + PRIME_IDEAL_CONTAINS_NILPOTENTS = |- !r j. prime_ideal r j ==> {x | ring_nilpotent r x} SUBSET j - + PRIME_IDEAL_NONUNITS = |- !r. prime_ideal r {x | x IN ring_carrier r /\ ~ring_unit r x} <=> ring_ideal r {x | x IN ring_carrier r /\ ~ring_unit r x} - + PROPER_IDEAL_NONUNITS = |- !r. proper_ideal r {x | x IN ring_carrier r /\ ~ring_unit r x} <=> ring_ideal r {x | x IN ring_carrier r /\ ~ring_unit r x} - + PROPER_IDEAL_SUBSET_NONUNITS = |- !r j. proper_ideal r j ==> j SUBSET {x | x IN ring_carrier r /\ ~ring_unit r x} - + RING_COSET_IDEAL_GENERATED_SING = |- !r a x. a IN ring_carrier r /\ x IN ring_carrier r ==> ring_coset r (ideal_generated r {a}) x = {y | y IN ring_carrier r /\ ring_divides r a (ring_sub r x y)} - + RING_COSET_IDEAL_GENERATED_SING_EQ = |- !r a x y. a IN ring_carrier r /\ x IN ring_carrier r /\ y IN ring_carrier r ==> (ring_coset r (ideal_generated r {a}) x = ring_coset r (ideal_generated r {a}) y <=> ring_divides r a (ring_sub r x y)) - + RING_COSET_RELATIONAL = |- !r j x y. (ring_ideal r j \/ j subring_of r) /\ x IN ring_carrier r /\ y IN ring_carrier r ==> (ring_coset r j x y <=> ring_coset r j x = ring_coset r j y) - + RING_EPIMORPHISM_I = |- !r. ring_epimorphism (r,r) I - + RING_EPIMORPHISM_POLY_EVAL = |- !r s x. x IN ring_carrier r ==> ring_epimorphism (poly_ring r s,r) (\p. poly_eval r p x) - + RING_EPIMORPHISM_POLY_EVALUATE = |- !r s x. IMAGE x s SUBSET ring_carrier r ==> ring_epimorphism (poly_ring r s,r) (\p. poly_evaluate r p x) - + RING_EPIMORPHISM_POLY_RINGS = |- !r s f v. ring_epimorphism (r,s) f ==> ring_epimorphism (poly_ring r v,poly_ring s v) (\p. f o p) - + RING_EPIMORPHISM_POWSER_RINGS = |- !r s f v. ring_epimorphism (r,s) f ==> ring_epimorphism (powser_ring r v,powser_ring s v) (\p. f o p) - + RING_HOMOMORPHISM_I = |- !r. ring_homomorphism (r,r) I - + RING_HOMOMORPHISM_INTEGER_MOD_RINGS = |- !p m n. ring_homomorphism (integer_mod_ring m,integer_mod_ring n) (\x. x rem &n) <=> n divides m - + RING_HOMOMORPHISM_INTEGER_MOD_RINGS_POW = |- !p i j. i <= j ==> ring_homomorphism (integer_mod_ring (p EXP j),integer_mod_ring (p EXP i)) (\x. x rem &p pow i) - + RING_HOMOMORPHISM_POLY_EVAL = |- !r s x. x IN ring_carrier r ==> ring_homomorphism (poly_ring r s,r) (\p. poly_eval r p x) - + RING_HOMOMORPHISM_POLY_EVALUATE = |- !r s x. IMAGE x s SUBSET ring_carrier r ==> ring_homomorphism (poly_ring r s,r) (\p. poly_evaluate r p x) - + RING_HOMOMORPHISM_POLY_RINGS = |- !r s f v. ring_homomorphism (r,s) f ==> ring_homomorphism (poly_ring r v,poly_ring s v) (\p. f o p) - + RING_HOMOMORPHISM_POWSER_RINGS = |- !r s f v. ring_homomorphism (r,s) f ==> ring_homomorphism (powser_ring r v,powser_ring s v) (\p. f o p) - + RING_IDEAL_NONUNITS = |- !r. ring_ideal r {x | x IN ring_carrier r /\ ~ring_unit r x} <=> @@ -717,85 +891,85 @@ and theorems: y IN ring_carrier r /\ ~ring_unit r y ==> ~ring_unit r (ring_add r x y)) - + RING_ISOMORPHISMS_I = |- !r. ring_isomorphisms (r,r) (I,I) - + RING_ISOMORPHISM_I = |- !r. ring_isomorphism (r,r) I - + RING_ISOMORPHISM_POLY_RINGS = |- !r s f v. ring_isomorphism (r,s) f ==> ring_isomorphism (poly_ring r v,poly_ring s v) (\p. f o p) - + RING_ISOMORPHISM_POWSER_RINGS = |- !r s f v. ring_isomorphism (r,s) f ==> ring_isomorphism (powser_ring r v,powser_ring s v) (\p. f o p) - + RING_MONOMORPHISM_I = |- !r. ring_monomorphism (r,r) I - + RING_MONOMORPHISM_POLY_RINGS = |- !r s f v. ring_monomorphism (r,s) f ==> ring_monomorphism (poly_ring r v,poly_ring s v) (\p. f o p) - + RING_MONOMORPHISM_POWSER_RINGS = |- !r s f v. ring_monomorphism (r,s) f ==> ring_monomorphism (powser_ring r v,powser_ring s v) (\p. f o p) - + RING_MULTSYS = |- (!r s x. ring_multsys r s /\ x IN s ==> x IN ring_carrier r) /\ (!r s. ring_multsys r s ==> ring_1 r IN s) /\ (!r s x y. ring_multsys r s /\ x IN s /\ y IN s ==> ring_mul r x y IN s) - + RING_NILPOTENT_UNIT = |- !r x. ring_unit r x /\ ring_nilpotent r x <=> trivial_ring r /\ x = ring_0 r - + RING_POLYNOMIAL = |- !r p. ring_polynomial r p <=> p IN ring_carrier (poly_ring r (:V)) - + RING_POLYNOMIAL_CARRIER = |- !r p. ring_polynomial r p <=> p IN ring_carrier (poly_ring r (poly_vars r p)) - + RING_POLYNOMIAL_CARRIER_GEN = |- !r s p. poly_vars r p SUBSET s ==> (ring_polynomial r p <=> p IN ring_carrier (poly_ring r s)) - + RING_POLYNOMIAL_COMPOSE = |- !r s f p. ring_homomorphism (r,s) f /\ ring_polynomial r p ==> ring_polynomial s (f o p) - + RING_POLYNOMIAL_MONOMIAL = |- !r p m. ring_polynomial r p /\ ~(p m = ring_0 r) ==> monomial (:V) m - + RING_POLYNOMIAL_SUB = |- !r p1 p2. ring_polynomial r p1 /\ ring_polynomial r p2 ==> ring_polynomial r (poly_sub r p1 p2) - + RING_POWERSERIES_COMPOSE = |- !r s f p. ring_homomorphism (r,s) f /\ ring_powerseries r p ==> ring_powerseries s (f o p) - + RING_POWERSERIES_MONOMIAL = |- !r p m. ring_powerseries r p /\ ~(p m = ring_0 r) ==> monomial (:V) m - + RING_POWERSERIES_SUB = |- !r p1 p2. ring_powerseries r p1 /\ ring_powerseries r p2 ==> ring_powerseries r (poly_sub r p1 p2) - + RING_SATURATED_MULTSYS_NONPRIME = |- !r j. prime_ideal r j @@ -806,7 +980,7 @@ and theorems: ring_mul r x y IN ring_carrier r DIFF j ==> x IN ring_carrier r DIFF j /\ y IN ring_carrier r DIFF j) - + RING_SUM_CLAUSES_RIGHT = |- !r f m n. 0 < n /\ m <= n @@ -814,7 +988,7 @@ and theorems: (if f n IN ring_carrier r then ring_add r (ring_sum r (m..n - 1) f) (f n) else ring_sum r (m..n - 1) f) - + RING_UNIT_LOCALEQUIV_EQ = |- !r s a b. ring_multsys r s /\ @@ -827,7 +1001,7 @@ and theorems: b IN s ==> (ring_unit (ring_localization r s) (ring_localequiv r s (a,b)) <=> a IN s) - + RING_UNIT_LOCALIZATION = |- !r s c. ring_multsys r s /\ @@ -838,23 +1012,23 @@ and theorems: ==> x IN s /\ y IN s) ==> (ring_unit (ring_localization r s) c <=> (?a b. a IN s /\ b IN s /\ c = ring_localequiv r s (a,b))) - + UNIONS_PRIME_IDEALS = |- !r. UNIONS {j | prime_ideal r j} = {x | x IN ring_carrier r /\ ~ring_unit r x} - + UNIONS_PROPER_IDEALS = |- !r. UNIONS {j | proper_ideal r j} = {x | x IN ring_carrier r /\ ~ring_unit r x} - + UNIQUE_PRIME_IDEAL = |- !r. (?!j. prime_ideal r j) <=> ~trivial_ring r /\ (!x. x IN ring_carrier r ==> ring_unit r x \/ ring_nilpotent r x) - + UNIQUE_PRIME_IDEAL_IMP_LOCAL_RING = |- !r. (?!j. prime_ideal r j) ==> local_ring r diff --git a/EC/nistp192.ml b/EC/nistp192.ml index c6d5734c..071fb9b8 100644 --- a/EC/nistp192.ml +++ b/EC/nistp192.ml @@ -109,7 +109,7 @@ let GROUP_ELEMENT_ORDER_G192 = prove REWRITE_TAC[n_192] THEN CONV_TAC(LAND_CONV ECGROUP_POW_CONV) THEN REFL_TAC);; -let FINITE_GROUP_CARRIER_192 = prove +let FINITE_GROUP_CARRIER_P192 = prove (`FINITE(group_carrier p192_group)`, REWRITE_TAC[P192_GROUP] THEN MATCH_MP_TAC FINITE_WEIERSTRASS_CURVE THEN REWRITE_TAC[FINITE_INTEGER_MOD_RING; FIELD_INTEGER_MOD_RING; PRIME_P192] THEN @@ -120,7 +120,7 @@ let SIZE_P192_GROUP = prove MATCH_MP_TAC GROUP_ADHOC_ORDER_UNIQUE_LEMMA THEN EXISTS_TAC `G_192:(int#int)option` THEN REWRITE_TAC[GENERATOR_IN_GROUP_CARRIER_192; GROUP_ELEMENT_ORDER_G192; - FINITE_GROUP_CARRIER_192] THEN + FINITE_GROUP_CARRIER_P192] THEN REWRITE_TAC[P192_GROUP] THEN CONJ_TAC THENL [W(MP_TAC o PART_MATCH (lhand o rand) CARD_BOUND_WEIERSTRASS_CURVE o lhand o snd) THEN @@ -152,11 +152,21 @@ let SIZE_P192_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 P192_GROUP_ORDER = prove + (`CARD(group_carrier p192_group) = n_192`, + REWRITE_TAC[REWRITE_RULE[HAS_SIZE] SIZE_P192_GROUP]);; + +let P192_GROUP_ELEMENT_ORDER = prove + (`!P. P IN group_carrier p192_group + ==> group_element_order p192_group P = + if P = group_id p192_group then 1 else n_192`, + MESON_TAC[SIZE_P192_GROUP; HAS_SIZE; GROUP_ELEMENT_ORDER_PRIME; PRIME_N192]);; + let GENERATED_P192_GROUP = prove (`subgroup_generated p192_group {G_192} = p192_group`, SIMP_TAC[SUBGROUP_GENERATED_ELEMENT_ORDER; GENERATOR_IN_GROUP_CARRIER_192; - FINITE_GROUP_CARRIER_192] THEN + FINITE_GROUP_CARRIER_P192] THEN REWRITE_TAC[GROUP_ELEMENT_ORDER_G192; REWRITE_RULE[HAS_SIZE] SIZE_P192_GROUP]);; diff --git a/EC/nistp224.ml b/EC/nistp224.ml index d6babd31..9ce74a9b 100644 --- a/EC/nistp224.ml +++ b/EC/nistp224.ml @@ -108,7 +108,7 @@ let GROUP_ELEMENT_ORDER_G224 = prove REWRITE_TAC[n_224] THEN CONV_TAC(LAND_CONV ECGROUP_POW_CONV) THEN REFL_TAC);; -let FINITE_GROUP_CARRIER_224 = prove +let FINITE_GROUP_CARRIER_P224 = prove (`FINITE(group_carrier p224_group)`, REWRITE_TAC[P224_GROUP] THEN MATCH_MP_TAC FINITE_WEIERSTRASS_CURVE THEN REWRITE_TAC[FINITE_INTEGER_MOD_RING; FIELD_INTEGER_MOD_RING; PRIME_P224] THEN @@ -119,7 +119,7 @@ let SIZE_P224_GROUP = prove MATCH_MP_TAC GROUP_ADHOC_ORDER_UNIQUE_LEMMA THEN EXISTS_TAC `G_224:(int#int)option` THEN REWRITE_TAC[GENERATOR_IN_GROUP_CARRIER_224; GROUP_ELEMENT_ORDER_G224; - FINITE_GROUP_CARRIER_224] THEN + FINITE_GROUP_CARRIER_P224] THEN REWRITE_TAC[P224_GROUP] THEN CONJ_TAC THENL [W(MP_TAC o PART_MATCH (lhand o rand) CARD_BOUND_WEIERSTRASS_CURVE o lhand o snd) THEN @@ -151,11 +151,21 @@ let SIZE_P224_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 P256_GROUP_ORDER = prove + (`CARD(group_carrier p224_group) = n_224`, + REWRITE_TAC[REWRITE_RULE[HAS_SIZE] SIZE_P224_GROUP]);; + +let P224_GROUP_ELEMENT_ORDER = prove + (`!P. P IN group_carrier p224_group + ==> group_element_order p224_group P = + if P = group_id p224_group then 1 else n_224`, + MESON_TAC[SIZE_P224_GROUP; HAS_SIZE; GROUP_ELEMENT_ORDER_PRIME; PRIME_N224]);; + let GENERATED_P224_GROUP = prove (`subgroup_generated p224_group {G_224} = p224_group`, SIMP_TAC[SUBGROUP_GENERATED_ELEMENT_ORDER; GENERATOR_IN_GROUP_CARRIER_224; - FINITE_GROUP_CARRIER_224] THEN + FINITE_GROUP_CARRIER_P224] THEN REWRITE_TAC[GROUP_ELEMENT_ORDER_G224; REWRITE_RULE[HAS_SIZE] SIZE_P224_GROUP]);; diff --git a/EC/nistp256.ml b/EC/nistp256.ml index 10d5cec2..2a7354e8 100644 --- a/EC/nistp256.ml +++ b/EC/nistp256.ml @@ -116,7 +116,7 @@ let GROUP_ELEMENT_ORDER_G256 = prove REWRITE_TAC[n_256] THEN CONV_TAC(LAND_CONV ECGROUP_POW_CONV) THEN REFL_TAC);; -let FINITE_GROUP_CARRIER_256 = prove +let FINITE_GROUP_CARRIER_P256 = prove (`FINITE(group_carrier p256_group)`, REWRITE_TAC[P256_GROUP] THEN MATCH_MP_TAC FINITE_WEIERSTRASS_CURVE THEN REWRITE_TAC[FINITE_INTEGER_MOD_RING; FIELD_INTEGER_MOD_RING; PRIME_P256] THEN @@ -127,7 +127,7 @@ let SIZE_P256_GROUP = prove MATCH_MP_TAC GROUP_ADHOC_ORDER_UNIQUE_LEMMA THEN EXISTS_TAC `G_256:(int#int)option` THEN REWRITE_TAC[GENERATOR_IN_GROUP_CARRIER_256; GROUP_ELEMENT_ORDER_G256; - FINITE_GROUP_CARRIER_256] THEN + FINITE_GROUP_CARRIER_P256] THEN REWRITE_TAC[P256_GROUP] THEN CONJ_TAC THENL [W(MP_TAC o PART_MATCH (lhand o rand) CARD_BOUND_WEIERSTRASS_CURVE o lhand o snd) THEN @@ -159,11 +159,21 @@ let SIZE_P256_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 P256_GROUP_ORDER = prove + (`CARD(group_carrier p256_group) = n_256`, + REWRITE_TAC[REWRITE_RULE[HAS_SIZE] SIZE_P256_GROUP]);; + +let P256_GROUP_ELEMENT_ORDER = prove + (`!P. P IN group_carrier p256_group + ==> group_element_order p256_group P = + if P = group_id p256_group then 1 else n_256`, + MESON_TAC[SIZE_P256_GROUP; HAS_SIZE; GROUP_ELEMENT_ORDER_PRIME; PRIME_N256]);; + let GENERATED_P256_GROUP = prove (`subgroup_generated p256_group {G_256} = p256_group`, SIMP_TAC[SUBGROUP_GENERATED_ELEMENT_ORDER; GENERATOR_IN_GROUP_CARRIER_256; - FINITE_GROUP_CARRIER_256] THEN + FINITE_GROUP_CARRIER_P256] THEN REWRITE_TAC[GROUP_ELEMENT_ORDER_G256; REWRITE_RULE[HAS_SIZE] SIZE_P256_GROUP]);; diff --git a/EC/nistp384.ml b/EC/nistp384.ml index 470cd8de..8c6beb07 100644 --- a/EC/nistp384.ml +++ b/EC/nistp384.ml @@ -129,7 +129,7 @@ let GROUP_ELEMENT_ORDER_G384 = prove REWRITE_TAC[n_384] THEN CONV_TAC(LAND_CONV ECGROUP_POW_CONV) THEN REFL_TAC);; -let FINITE_GROUP_CARRIER_384 = prove +let FINITE_GROUP_CARRIER_P384 = prove (`FINITE(group_carrier p384_group)`, REWRITE_TAC[P384_GROUP] THEN MATCH_MP_TAC FINITE_WEIERSTRASS_CURVE THEN REWRITE_TAC[FINITE_INTEGER_MOD_RING; FIELD_INTEGER_MOD_RING; PRIME_P384] THEN @@ -140,7 +140,7 @@ let SIZE_P384_GROUP = prove MATCH_MP_TAC GROUP_ADHOC_ORDER_UNIQUE_LEMMA THEN EXISTS_TAC `G_384:(int#int)option` THEN REWRITE_TAC[GENERATOR_IN_GROUP_CARRIER_384; GROUP_ELEMENT_ORDER_G384; - FINITE_GROUP_CARRIER_384] THEN + FINITE_GROUP_CARRIER_P384] THEN REWRITE_TAC[P384_GROUP] THEN CONJ_TAC THENL [W(MP_TAC o PART_MATCH (lhand o rand) CARD_BOUND_WEIERSTRASS_CURVE o lhand o snd) THEN @@ -172,11 +172,21 @@ let SIZE_P384_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 P384_GROUP_ORDER = prove + (`CARD(group_carrier p384_group) = n_384`, + REWRITE_TAC[REWRITE_RULE[HAS_SIZE] SIZE_P384_GROUP]);; + +let P384_GROUP_ELEMENT_ORDER = prove + (`!P. P IN group_carrier p384_group + ==> group_element_order p384_group P = + if P = group_id p384_group then 1 else n_384`, + MESON_TAC[SIZE_P384_GROUP; HAS_SIZE; GROUP_ELEMENT_ORDER_PRIME; PRIME_N384]);; + let GENERATED_P384_GROUP = prove (`subgroup_generated p384_group {G_384} = p384_group`, SIMP_TAC[SUBGROUP_GENERATED_ELEMENT_ORDER; GENERATOR_IN_GROUP_CARRIER_384; - FINITE_GROUP_CARRIER_384] THEN + FINITE_GROUP_CARRIER_P384] THEN REWRITE_TAC[GROUP_ELEMENT_ORDER_G384; REWRITE_RULE[HAS_SIZE] SIZE_P384_GROUP]);; diff --git a/EC/nistp521.ml b/EC/nistp521.ml index a668e882..a64e4195 100644 --- a/EC/nistp521.ml +++ b/EC/nistp521.ml @@ -127,7 +127,7 @@ let GROUP_ELEMENT_ORDER_G521 = prove REWRITE_TAC[n_521] THEN CONV_TAC(LAND_CONV ECGROUP_POW_CONV) THEN REFL_TAC);; -let FINITE_GROUP_CARRIER_521 = prove +let FINITE_GROUP_CARRIER_P521 = prove (`FINITE(group_carrier p521_group)`, REWRITE_TAC[P521_GROUP] THEN MATCH_MP_TAC FINITE_WEIERSTRASS_CURVE THEN REWRITE_TAC[FINITE_INTEGER_MOD_RING; FIELD_INTEGER_MOD_RING; PRIME_P521] THEN @@ -138,7 +138,7 @@ let SIZE_P521_GROUP = prove MATCH_MP_TAC GROUP_ADHOC_ORDER_UNIQUE_LEMMA THEN EXISTS_TAC `G_521:(int#int)option` THEN REWRITE_TAC[GENERATOR_IN_GROUP_CARRIER_521; GROUP_ELEMENT_ORDER_G521; - FINITE_GROUP_CARRIER_521] THEN + FINITE_GROUP_CARRIER_P521] THEN REWRITE_TAC[P521_GROUP] THEN CONJ_TAC THENL [W(MP_TAC o PART_MATCH (lhand o rand) CARD_BOUND_WEIERSTRASS_CURVE o lhand o snd) THEN @@ -170,11 +170,21 @@ let SIZE_P521_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 P521_GROUP_ORDER = prove + (`CARD(group_carrier p521_group) = n_521`, + REWRITE_TAC[REWRITE_RULE[HAS_SIZE] SIZE_P521_GROUP]);; + +let P521_GROUP_ELEMENT_ORDER = prove + (`!P. P IN group_carrier p521_group + ==> group_element_order p521_group P = + if P = group_id p521_group then 1 else n_521`, + MESON_TAC[SIZE_P521_GROUP; HAS_SIZE; GROUP_ELEMENT_ORDER_PRIME; PRIME_N521]);; + let GENERATED_P521_GROUP = prove (`subgroup_generated p521_group {G_521} = p521_group`, SIMP_TAC[SUBGROUP_GENERATED_ELEMENT_ORDER; GENERATOR_IN_GROUP_CARRIER_521; - FINITE_GROUP_CARRIER_521] THEN + FINITE_GROUP_CARRIER_P521] THEN REWRITE_TAC[GROUP_ELEMENT_ORDER_G521; REWRITE_RULE[HAS_SIZE] SIZE_P521_GROUP]);; diff --git a/EC/secp192k1.ml b/EC/secp192k1.ml index 92784fd4..fb03c3fe 100644 --- a/EC/secp192k1.ml +++ b/EC/secp192k1.ml @@ -95,7 +95,7 @@ let GROUP_ELEMENT_ORDER_G192K1 = prove REWRITE_TAC[n_192k1] THEN CONV_TAC(LAND_CONV ECGROUP_POW_CONV) THEN REFL_TAC);; -let FINITE_GROUP_CARRIER_192K1 = prove +let FINITE_GROUP_CARRIER_P192K1 = prove (`FINITE(group_carrier p192k1_group)`, REWRITE_TAC[P192K1_GROUP] THEN MATCH_MP_TAC FINITE_WEIERSTRASS_CURVE THEN REWRITE_TAC[FINITE_INTEGER_MOD_RING; @@ -108,7 +108,7 @@ let SIZE_P192K1_GROUP = prove EXISTS_TAC `G_192K1:(int#int)option` THEN REWRITE_TAC[GENERATOR_IN_GROUP_CARRIER_192K1; GROUP_ELEMENT_ORDER_G192K1; - FINITE_GROUP_CARRIER_192K1] THEN + FINITE_GROUP_CARRIER_P192K1] THEN REWRITE_TAC[P192K1_GROUP] THEN CONJ_TAC THENL [W(MP_TAC o PART_MATCH (lhand o rand) CARD_BOUND_WEIERSTRASS_CURVE o lhand o snd) THEN @@ -140,11 +140,22 @@ let SIZE_P192K1_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 P192K1_GROUP_ORDER = prove + (`CARD(group_carrier p192k1_group) = n_192k1`, + REWRITE_TAC[REWRITE_RULE[HAS_SIZE] SIZE_P192K1_GROUP]);; + +let P192K1_GROUP_ELEMENT_ORDER = prove + (`!P. P IN group_carrier p192k1_group + ==> group_element_order p192k1_group P = + if P = group_id p192k1_group then 1 else n_192k1`, + MESON_TAC[SIZE_P192K1_GROUP; HAS_SIZE; GROUP_ELEMENT_ORDER_PRIME; + PRIME_N192K1]);; + let GENERATED_P192K1_GROUP = prove (`subgroup_generated p192k1_group {G_192K1} = p192k1_group`, SIMP_TAC[SUBGROUP_GENERATED_ELEMENT_ORDER; GENERATOR_IN_GROUP_CARRIER_192K1; - FINITE_GROUP_CARRIER_192K1] THEN + FINITE_GROUP_CARRIER_P192K1] THEN REWRITE_TAC[GROUP_ELEMENT_ORDER_G192K1; REWRITE_RULE[HAS_SIZE] SIZE_P192K1_GROUP]);; diff --git a/EC/secp224k1.ml b/EC/secp224k1.ml index 4869d9b6..d1e4f89d 100644 --- a/EC/secp224k1.ml +++ b/EC/secp224k1.ml @@ -100,7 +100,7 @@ let GROUP_ELEMENT_ORDER_G224K1 = prove REWRITE_TAC[n_224k1] THEN CONV_TAC(LAND_CONV ECGROUP_POW_CONV) THEN REFL_TAC);; -let FINITE_GROUP_CARRIER_224K1 = prove +let FINITE_GROUP_CARRIER_P224K1 = prove (`FINITE(group_carrier p224k1_group)`, REWRITE_TAC[P224K1_GROUP] THEN MATCH_MP_TAC FINITE_WEIERSTRASS_CURVE THEN REWRITE_TAC[FINITE_INTEGER_MOD_RING; @@ -113,7 +113,7 @@ let SIZE_P224K1_GROUP = prove EXISTS_TAC `G_224K1:(int#int)option` THEN REWRITE_TAC[GENERATOR_IN_GROUP_CARRIER_224K1; GROUP_ELEMENT_ORDER_G224K1; - FINITE_GROUP_CARRIER_224K1] THEN + FINITE_GROUP_CARRIER_P224K1] THEN REWRITE_TAC[P224K1_GROUP] THEN CONJ_TAC THENL [W(MP_TAC o PART_MATCH (lhand o rand) CARD_BOUND_WEIERSTRASS_CURVE o lhand o snd) THEN @@ -145,11 +145,22 @@ let SIZE_P224K1_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 P224K1_GROUP_ORDER = prove + (`CARD(group_carrier p224k1_group) = n_224k1`, + REWRITE_TAC[REWRITE_RULE[HAS_SIZE] SIZE_P224K1_GROUP]);; + +let P224K1_GROUP_ELEMENT_ORDER = prove + (`!P. P IN group_carrier p224k1_group + ==> group_element_order p224k1_group P = + if P = group_id p224k1_group then 1 else n_224k1`, + MESON_TAC[SIZE_P224K1_GROUP; HAS_SIZE; GROUP_ELEMENT_ORDER_PRIME; + PRIME_N224K1]);; + let GENERATED_P224K1_GROUP = prove (`subgroup_generated p224k1_group {G_224K1} = p224k1_group`, SIMP_TAC[SUBGROUP_GENERATED_ELEMENT_ORDER; GENERATOR_IN_GROUP_CARRIER_224K1; - FINITE_GROUP_CARRIER_224K1] THEN + FINITE_GROUP_CARRIER_P224K1] THEN REWRITE_TAC[GROUP_ELEMENT_ORDER_G224K1; REWRITE_RULE[HAS_SIZE] SIZE_P224K1_GROUP]);; diff --git a/EC/secp256k1.ml b/EC/secp256k1.ml index 8131dc2d..8c69c7d3 100644 --- a/EC/secp256k1.ml +++ b/EC/secp256k1.ml @@ -108,7 +108,7 @@ let GROUP_ELEMENT_ORDER_G256K1 = prove REWRITE_TAC[n_256k1] THEN CONV_TAC(LAND_CONV ECGROUP_POW_CONV) THEN REFL_TAC);; -let FINITE_GROUP_CARRIER_256K1 = prove +let FINITE_GROUP_CARRIER_P256K1 = prove (`FINITE(group_carrier p256k1_group)`, REWRITE_TAC[P256K1_GROUP] THEN MATCH_MP_TAC FINITE_WEIERSTRASS_CURVE THEN REWRITE_TAC[FINITE_INTEGER_MOD_RING; @@ -121,7 +121,7 @@ let SIZE_P256K1_GROUP = prove EXISTS_TAC `G_256K1:(int#int)option` THEN REWRITE_TAC[GENERATOR_IN_GROUP_CARRIER_256K1; GROUP_ELEMENT_ORDER_G256K1; - FINITE_GROUP_CARRIER_256K1] THEN + FINITE_GROUP_CARRIER_P256K1] THEN REWRITE_TAC[P256K1_GROUP] THEN CONJ_TAC THENL [W(MP_TAC o PART_MATCH (lhand o rand) CARD_BOUND_WEIERSTRASS_CURVE o lhand o snd) THEN @@ -153,11 +153,22 @@ let SIZE_P256K1_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 P256K1_GROUP_ORDER = prove + (`CARD(group_carrier p256k1_group) = n_256k1`, + REWRITE_TAC[REWRITE_RULE[HAS_SIZE] SIZE_P256K1_GROUP]);; + +let P256K1_GROUP_ELEMENT_ORDER = prove + (`!P. P IN group_carrier p256k1_group + ==> group_element_order p256k1_group P = + if P = group_id p256k1_group then 1 else n_256k1`, + MESON_TAC[SIZE_P256K1_GROUP; HAS_SIZE; GROUP_ELEMENT_ORDER_PRIME; + PRIME_N256K1]);; + let GENERATED_P256K1_GROUP = prove (`subgroup_generated p256k1_group {G_256K1} = p256k1_group`, SIMP_TAC[SUBGROUP_GENERATED_ELEMENT_ORDER; GENERATOR_IN_GROUP_CARRIER_256K1; - FINITE_GROUP_CARRIER_256K1] THEN + FINITE_GROUP_CARRIER_P256K1] THEN REWRITE_TAC[GROUP_ELEMENT_ORDER_G256K1; REWRITE_RULE[HAS_SIZE] SIZE_P256K1_GROUP]);; diff --git a/Library/grouptheory.ml b/Library/grouptheory.ml index fb3b8368..c4647f03 100644 --- a/Library/grouptheory.ml +++ b/Library/grouptheory.ml @@ -596,6 +596,12 @@ let GROUP_INV_ZPOW = prove REPEAT STRIP_TAC THEN REWRITE_TAC[group_zpow] THEN COND_CASES_TAC THEN ASM_SIMP_TAC[GROUP_INV_POW]);; +let GROUP_ZPOW_INV = prove + (`!G (x:A) n. + x IN group_carrier G + ==> group_zpow G (group_inv G x) n = group_zpow G x (--n)`, + SIMP_TAC[GSYM GROUP_INV_ZPOW; GSYM GROUP_ZPOW_NEG]);; + let GROUP_ZPOW_MUL = prove (`!G (x:A) m n. x IN group_carrier G @@ -8897,6 +8903,22 @@ let GROUP_POW_EQ = prove (m == n) (mod (group_element_order G x)))`, SIMP_TAC[GSYM GROUP_NPOW; GROUP_ZPOW_EQ; num_congruent]);; +let GROUP_ZPOW_REM_ELEMENT_ORDER = prove + (`!G (x:A) n. + x IN group_carrier G + ==> group_zpow G x (n rem &(group_element_order G x)) = + group_zpow G x n`, + SIMP_TAC[GROUP_ZPOW_EQ; INT_CONG_LREM] THEN + REPEAT STRIP_TAC THEN CONV_TAC INTEGER_RULE);; + +let GROUP_POW_MOD_ELEMENT_ORDER = prove + (`!G (x:A) n. + x IN group_carrier G + ==> group_pow G x (n MOD group_element_order G x) = + group_pow G x n`, + REWRITE_TAC[GSYM GROUP_NPOW; GSYM INT_OF_NUM_REM; + GROUP_ZPOW_REM_ELEMENT_ORDER]);; + let GROUP_ELEMENT_ORDER_EQ_0 = prove (`!G (x:A). x IN group_carrier G @@ -10179,6 +10201,27 @@ let GROUP_POW_GROUP_ORDER = prove ==> group_pow G x (CARD(group_carrier G)) = group_id G`, SIMP_TAC[GROUP_POW_EQ_ID; GROUP_ELEMENT_ORDER_DIVIDES_GROUP_ORDER]);; +let GROUP_ZPOW_REM_ORDER = prove + (`!G (x:A) n. + FINITE(group_carrier G) /\ x IN group_carrier G + ==> group_zpow G x (n rem &(CARD(group_carrier G))) = + group_zpow G x n`, + REPEAT STRIP_TAC THEN ASM_SIMP_TAC[GROUP_ZPOW_EQ] THEN + MATCH_MP_TAC(INTEGER_RULE + `!d:int. (x == y) (mod d) /\ e divides d ==> (x == y) (mod e)`) THEN + EXISTS_TAC `&(CARD(group_carrier G:A->bool)):int` THEN + ASM_SIMP_TAC[GROUP_ELEMENT_ORDER_DIVIDES_GROUP_ORDER; INT_CONG_LREM; + GSYM num_divides] THEN + CONV_TAC INTEGER_RULE);; + +let GROUP_POW_MOD_ORDER = prove + (`!G (x:A) n. FINITE(group_carrier G) /\ x IN group_carrier G + ==> group_pow G x (n MOD CARD(group_carrier G)) = + group_pow G x n`, + REWRITE_TAC[GSYM GROUP_NPOW; GSYM INT_OF_NUM_REM; + GROUP_ZPOW_REM_ORDER]);; + + let SUBGROUP_OF_FINITE_CYCLIC_GROUP = prove (`!G h a:A. FINITE(group_carrier G) /\ @@ -11817,6 +11860,14 @@ let CYCLIC_PRIME_ORDER_GROUP = prove ASM_SIMP_TAC[GROUP_ELEMENT_ORDER_DIVIDES_GROUP_ORDER] THEN ASM_SIMP_TAC[GROUP_ELEMENT_ORDER_EQ_1]);; +let GROUP_ELEMENT_ORDER_PRIME = prove + (`!G a:A. prime p /\ (group_carrier G) HAS_SIZE p /\ a IN group_carrier G + ==> group_element_order G a = + if a = group_id G then 1 else CARD(group_carrier G)`, + REWRITE_TAC[HAS_SIZE] THEN + MESON_TAC[GROUP_ELEMENT_ORDER_ID; SUBGROUP_GENERATED_ELEMENT_ORDER; + CYCLIC_PRIME_ORDER_GROUP]);; + let GENERATOR_INTEGER_MOD_GROUP = prove (`!n a. subgroup_generated (integer_mod_group n) {a} = integer_mod_group n <=> (n <= 1 \/ &0 <= a /\ a < &n) /\ coprime(&n,a)`, diff --git a/Library/prime.ml b/Library/prime.ml index 75e057ff..054273d4 100755 --- a/Library/prime.ml +++ b/Library/prime.ml @@ -92,6 +92,10 @@ let DIVIDES_RMUL2_EQ = prove (`!a b c. ~(c = 0) ==> ((a * c) divides (b * c) <=> a divides b)`, NUMBER_TAC);; +let DIVIDES_EQ_ZERO = prove + (`!p n. n < p ==> (p divides n <=> n = 0)`, + MESON_TAC[DIVIDES_0; DIVIDES_LE_STRONG; NOT_LE; LT]);; + let DIVIDES_CASES = prove (`!m n. n divides m ==> m = 0 \/ m = n \/ 2 * n <= m`, SIMP_TAC[ARITH_RULE `m = n \/ 2 * n <= m <=> m = n * 1 \/ n * 2 <= m`] THEN diff --git a/Library/ringtheory.ml b/Library/ringtheory.ml index 044a0186..01950d13 100644 --- a/Library/ringtheory.ml +++ b/Library/ringtheory.ml @@ -2605,6 +2605,20 @@ let IN_SUBRING_POW = prove REPEAT GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THEN ASM_SIMP_TAC[ring_pow; IN_SUBRING_1; IN_SUBRING_MUL]);; +let IN_SUBRING_SUM = prove + (`!r h (f:K->A) s. + h subring_of r /\ (!a. a IN s ==> f a IN h) ==> ring_sum r s f IN h`, + REPEAT STRIP_TAC THEN MATCH_MP_TAC(REWRITE_RULE[] + (ISPECL [`r:A ring`; `\x:A. x IN h`] RING_SUM_CLOSED)) THEN + ASM_MESON_TAC[subring_of]);; + +let IN_SUBRING_PRODUCT = prove + (`!r h (f:K->A) s. + h subring_of r /\ (!a. a IN s ==> f a IN h) ==> ring_product r s f IN h`, + REPEAT STRIP_TAC THEN MATCH_MP_TAC(REWRITE_RULE[] + (ISPECL [`r:A ring`; `\x:A. x IN h`] RING_PRODUCT_CLOSED)) THEN + ASM_MESON_TAC[subring_of]);; + let SUBRING_OF_INTERS = prove (`!r (gs:(A->bool)->bool). (!g. g IN gs ==> g subring_of r) /\ ~(gs = {}) @@ -11378,6 +11392,15 @@ let RING_NILPOTENT_SUB = prove ==> ring_nilpotent r (ring_sub r x y)`, SIMP_TAC[ring_sub; RING_NILPOTENT_ADD; RING_NILPOTENT_NEG]);; +let RING_NILPOTENT_SUM = prove + (`!(r:A ring) (f:K->A) s. + FINITE s /\ (!i. i IN s ==> ring_nilpotent r (f i)) + ==> ring_nilpotent r (ring_sum r s f)`, + GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN + MATCH_MP_TAC FINITE_INDUCT_STRONG THEN + SIMP_TAC[RING_SUM_CLAUSES; FORALL_IN_INSERT; RING_NILPOTENT_0] THEN + MESON_TAC[RING_NILPOTENT_ADD; ring_nilpotent]);; + let RING_ZERODIVISOR_NILPOTENT_CLAUSES = prove (`(!r w z:A. ring_zerodivisor r w /\ ring_nilpotent r z @@ -15019,6 +15042,12 @@ let MONOMIAL_DEG = prove CONV_TAC SYM_CONV THEN MATCH_MP_TAC NSUM_SUPERSET THEN REWRITE_TAC[IN_UNIV; SUBSET_UNIV; monomial_vars; IN_ELIM_THM]);; +let MONOMIAL_VAR_1 = prove + (`(!v:V. ~(monomial_var v = monomial_1)) /\ + (!v:V. ~(monomial_1 = monomial_var v))`, + REWRITE_TAC[monomial_var; monomial_1; FUN_EQ_THM] THEN + MESON_TAC[ARITH_RULE `~(1 = 0)`]);; + let MONOMIAL_VARS_1 = prove (`monomial_vars (monomial_1:V->num) = {}`, REWRITE_TAC[monomial_vars; monomial_1; EMPTY_GSPEC]);; @@ -15755,6 +15784,16 @@ let POLY_MUL_0 = prove MATCH_MP_TAC RING_SUM_EQ_0 THEN ASM_SIMP_TAC[FORALL_PAIR_THM; RING_MUL_LZERO; RING_MUL_RZERO]);; +let POLY_MUL_MONOMIAL_1 = prove + (`!r (p:(V->num)->A) q. + ring_polynomial r p /\ ring_polynomial r q + ==> poly_mul r p q monomial_1 = + ring_mul r (p monomial_1) (q monomial_1)`, + REWRITE_TAC[ring_polynomial; ring_powerseries] THEN + REPEAT STRIP_TAC THEN REWRITE_TAC[poly_mul; MONOMIAL_MUL_EQ_1] THEN + REWRITE_TAC[SET_RULE `{x,y | x = a /\ y = b} = {(a,b)}`] THEN + ASM_SIMP_TAC[RING_SUM_SING; RING_MUL]);; + let POLY_VARS_CONST = prove (`!(r:A ring) c. poly_vars r (poly_const r c) = {}`, REPEAT GEN_TAC THEN REWRITE_TAC[poly_vars; poly_const] THEN @@ -16119,6 +16158,15 @@ let RING_MONOMORPHISM_POWSER_CONST = prove REWRITE_TAC[ring_monomorphism; RING_HOMOMORPHISM_POWSER_CONST] THEN SIMP_TAC[POLY_CONST_EQ]);; +let RING_HOMOMORPHISM_MONOMIAL_1 = prove + (`!(r:A ring) (v:V->bool). + ring_homomorphism (poly_ring r v,r) (\p. p monomial_1)`, + REWRITE_TAC[RING_HOMOMORPHISM; CONJUNCT2 POLY_RING] THEN + REWRITE_TAC[poly_0; poly_1; poly_const; poly_add] THEN + REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; CONJUNCT1 POLY_RING; IN_ELIM_THM] THEN + SIMP_TAC[POLY_MUL_MONOMIAL_1] THEN + SIMP_TAC[ring_polynomial; ring_powerseries]);; + let POWSER_SUM = prove (`!(r:A ring) (s:V->bool) f (k:K->bool). FINITE k /\ @@ -16840,6 +16888,45 @@ let POLY_EXTEND_HOMOMORPHIC_IMAGE = prove RULE_ASSUM_TAC(REWRITE_RULE[poly_vars; UNIONS_SUBSET; IN_ELIM_THM]) THEN ASM SET_TAC[]);; +let POLY_EXTEND_AT_0 = prove + (`!r s (v:V->bool) (h:A->B) p. + ring_homomorphism (r,s) h /\ + p IN ring_carrier (poly_ring r v) + ==> poly_extend (r,s) h (\x. ring_0 s) p = h(p monomial_1)`, + REPEAT STRIP_TAC THEN MATCH_MP_TAC POLY_EXTEND_UNIQUE THEN + EXISTS_TAC `v:V->bool` THEN + ASM_REWRITE_TAC[poly_var; poly_const; MONOMIAL_VAR_1] THEN + CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[RING_HOMOMORPHISM_0]] THEN + GEN_REWRITE_TAC RAND_CONV [GSYM o_DEF] THEN + MATCH_MP_TAC RING_HOMOMORPHISM_COMPOSE THEN + EXISTS_TAC `r:A ring` THEN + ASM_REWRITE_TAC[RING_HOMOMORPHISM_MONOMIAL_1]);; + +let POLY_SUBRING_GENERATED = prove + (`!(r:A ring) (s:V->bool). + subring_generated (poly_ring r s) + ({poly_const r c |c| c IN ring_carrier r} UNION + {poly_var r x | x IN s}) = + poly_ring r s`, + REPEAT GEN_TAC THEN REWRITE_TAC[SUBRING_GENERATED_EQ] THEN + SIMP_TAC[GSYM SUBSET_ANTISYM_EQ; RING_CARRIER_SUBRING_GENERATED_SUBSET] THEN + REWRITE_TAC[SUBSET] THEN X_GEN_TAC `p:(V->num)->A` THEN DISCH_TAC THEN + FIRST_ASSUM(SUBST1_TAC o SYM o MATCH_MP POLY_EXTEND_ID) THEN + REWRITE_TAC[poly_extend] THEN MATCH_MP_TAC IN_SUBRING_SUM THEN + REWRITE_TAC[SUBRING_SUBRING_GENERATED] THEN X_GEN_TAC `m:V->num` THEN + REWRITE_TAC[IN_ELIM_THM] THEN DISCH_TAC THEN MATCH_MP_TAC IN_SUBRING_MUL THEN + REWRITE_TAC[SUBRING_SUBRING_GENERATED] THEN CONJ_TAC THENL + [MATCH_MP_TAC SUBRING_GENERATED_INC THEN REWRITE_TAC[UNION_SUBSET] THEN + SIMP_TAC[SUBSET; FORALL_IN_GSPEC; POLY_VAR; POLY_CONST] THEN + FIRST_ASSUM(MP_TAC o MATCH_MP POLY_MONOMIAL_IN_CARRIER) THEN SET_TAC[]; + MATCH_MP_TAC IN_SUBRING_PRODUCT THEN + REWRITE_TAC[SUBRING_SUBRING_GENERATED] THEN + X_GEN_TAC `x:V` THEN DISCH_TAC THEN MATCH_MP_TAC IN_SUBRING_POW THEN + REWRITE_TAC[SUBRING_SUBRING_GENERATED] THEN + MATCH_MP_TAC SUBRING_GENERATED_INC THEN REWRITE_TAC[UNION_SUBSET] THEN + SIMP_TAC[SUBSET; FORALL_IN_GSPEC; POLY_VAR; POLY_CONST] THEN + RULE_ASSUM_TAC(REWRITE_RULE[POLY_RING; poly_vars]) THEN ASM SET_TAC[]]);; + (* ------------------------------------------------------------------------- *) (* Some "natural" isomorphisms between polynomial / power series variants. *) (* ------------------------------------------------------------------------- *) @@ -18799,178 +18886,6 @@ let CARD_EQ_POLY_RING_INFINITE = prove MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] CARD_EQ_TRANS) THEN ASM_SIMP_TAC[CARD_MUL_CONG; CARD_EQ_REFL; CARD_EQ_MONOMIALS_INFINITE]]);; -(* ------------------------------------------------------------------------- *) -(* Zerodivisors and units in polynomial and power series rings. *) -(* ------------------------------------------------------------------------- *) - -let INTEGRAL_DOMAIN_POWSER_RING = prove - (`!(r:A ring) (s:V->bool). - integral_domain(powser_ring r s) <=> integral_domain r`, - REPEAT GEN_TAC THEN EQ_TAC THENL - [MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] - INTEGRAL_DOMAIN_MONOMORPHIC_PREIMAGE) THEN - MESON_TAC[RING_MONOMORPHISM_POWSER_CONST]; - REWRITE_TAC[integral_domain; GSYM TRIVIAL_RING_10]] THEN - MATCH_MP_TAC MONO_AND THEN REWRITE_TAC[TRIVIAL_POWSER_RING] THEN - REWRITE_TAC[RING_CARRIER_POWSER_RING] THEN REWRITE_TAC[POWSER_RING] THEN - DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`p:(V->num)->A`; `q:(V->num)->A`] THEN - REWRITE_TAC[IN_ELIM_THM] THEN - REPEAT(DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC)) THEN - GEN_REWRITE_TAC I [GSYM CONTRAPOS_THM] THEN - REWRITE_TAC[DE_MORGAN_THM; FUN_EQ_THM; NOT_FORALL_THM; poly_0] THEN - REWRITE_TAC[POLY_CONST_0; POLY_0; poly_mul] THEN DISCH_TAC THEN - MP_TAC(ISPEC `(:V)` WO) THEN DISCH_THEN(X_CHOOSE_TAC `l:V->V->bool`) THEN - FIRST_ASSUM(ASSUME_TAC o MATCH_MP WOSET_MONOMIAL_LE) THEN - FIRST_ASSUM(MP_TAC o CONJUNCT2 o GEN_REWRITE_RULE I [WOSET]) THEN - REWRITE_TAC[FLD_MONOMIAL_LE] THEN DISCH_THEN(fun th -> - MP_TAC(SPEC `{m | ~((q:(V->num)->A) m = ring_0 r)}` th) THEN - MP_TAC(SPEC `{m | ~((p:(V->num)->A) m = ring_0 r)}` th)) THEN - ASM_REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; MONOMIAL; IN_ELIM_THM; SUBSET] THEN - ANTS_TAC THENL [ASM_MESON_TAC[monomial]; ALL_TAC] THEN - DISCH_THEN(X_CHOOSE_THEN `mp:V->num` STRIP_ASSUME_TAC) THEN - ANTS_TAC THENL [ASM_MESON_TAC[monomial]; ALL_TAC] THEN - DISCH_THEN(X_CHOOSE_THEN `mq:V->num` STRIP_ASSUME_TAC) THEN - EXISTS_TAC `monomial_mul mp mq:V->num` THEN MATCH_MP_TAC(MESON[] - `!m. ~(ring_sum r {m} f = z) /\ ring_sum r s f = ring_sum r {m} f - ==> ~(ring_sum r s f = z)`) THEN - EXISTS_TAC `(mp:V->num),(mq:V->num)` THEN CONJ_TAC THENL - [ASM_SIMP_TAC[RING_SUM_SING; RING_MUL] THEN ASM_MESON_TAC[]; ALL_TAC] THEN - MATCH_MP_TAC RING_SUM_SUPERSET THEN - REWRITE_TAC[SING_SUBSET; FORALL_IN_GSPEC; IMP_CONJ] THEN - REWRITE_TAC[IN_ELIM_PAIR_THM; IN_SING] THEN - MAP_EVERY X_GEN_TAC [`np:V->num`; `nq:V->num`] THEN - DISCH_TAC THEN REWRITE_TAC[PAIR_EQ; DE_MORGAN_THM] THEN - ASM_CASES_TAC `(p:(V->num)->A) np = ring_0 r` THENL - [ASM_SIMP_TAC[RING_MUL_LZERO]; ALL_TAC] THEN - ASM_CASES_TAC `(q:(V->num)->A) nq = ring_0 r` THENL - [ASM_SIMP_TAC[RING_MUL_RZERO]; ALL_TAC] THEN - MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN STRIP_TAC THEN - FIRST_ASSUM(MP_TAC o MATCH_MP (MESON[MONOMIAL_LT_REFL] - `m' = m ==> !l. ~monomial_lt l m m'`)) THEN - DISCH_THEN(MP_TAC o SPEC `l:V->V->bool`) THEN REWRITE_TAC[] THENL - [MATCH_MP_TAC MONOMIAL_LTE_MUL2; - MATCH_MP_TAC MONOMIAL_LET_MUL2] THEN - ASM_SIMP_TAC[monomial_lt; WOSET_IMP_POSET]);; - -let INTEGRAL_DOMAIN_POLY_RING = prove - (`!(r:A ring) (s:V->bool). - integral_domain(poly_ring r s) <=> integral_domain r`, - REPEAT GEN_TAC THEN EQ_TAC THENL - [ALL_TAC; GEN_REWRITE_TAC LAND_CONV [GSYM INTEGRAL_DOMAIN_POWSER_RING]] THEN - MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] - INTEGRAL_DOMAIN_MONOMORPHIC_PREIMAGE) THEN - MESON_TAC[RING_MONOMORPHISM_POLY_CONST; RING_MONOMORPHISM_POLY_POWSER]);; - -let RING_UNIT_POWSER_RING = prove - (`!(r:A ring) (s:V->bool) p. - ring_unit (powser_ring r s) p <=> - p IN ring_carrier(powser_ring r s) /\ - ring_unit r (p monomial_1)`, - REPEAT GEN_TAC THEN REWRITE_TAC[ring_unit] THEN - EQ_TAC THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN - ASM_REWRITE_TAC[] THENL - [CONJ_TAC THENL - [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV - [RING_CARRIER_POWSER_RING]) THEN - SIMP_TAC[IN_ELIM_THM]; - FIRST_X_ASSUM(X_CHOOSE_THEN `q:(V->num)->A` MP_TAC) THEN - DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN - REWRITE_TAC[POWSER_RING] THEN DISCH_TAC THEN - EXISTS_TAC `(q:(V->num)->A) monomial_1` THEN - RULE_ASSUM_TAC(REWRITE_RULE[RING_CARRIER_POWSER_RING; IN_ELIM_THM]) THEN - FIRST_X_ASSUM(MP_TAC o C AP_THM `monomial_1:V->num`) THEN - ASM_REWRITE_TAC[poly_mul; poly_1; MONOMIAL_MUL_EQ_1; poly_const] THEN - REWRITE_TAC[SET_RULE `{f x y | x = a /\ y = b} = {f a b}`] THEN - ASM_SIMP_TAC[RING_SUM_SING; RING_MUL]]; - ONCE_REWRITE_TAC[TAUT `p /\ q <=> ~(p ==> ~q)`] THEN - MP_TAC(ISPECL [`r:A ring`; `s:V->bool`] POWSER_RING_EQ) THEN - ASM_SIMP_TAC[POWSER_RING_EQ; RING_MUL; RING_1] THEN - DISCH_THEN(K ALL_TAC) THEN - REWRITE_TAC[RING_CARRIER_POWSER_RING; CONJUNCT2 POWSER_RING] THEN - FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV - [RING_CARRIER_POWSER_RING]) THEN - REWRITE_TAC[IN_ELIM_THM; poly_mul; poly_1; poly_const]] THEN - SUBGOAL_THEN - `!(q:(V->num)->A) m. - monomial s m /\ - (!m. p m IN ring_carrier r) /\ - (!m. q m IN ring_carrier r) - ==> ring_sum r {m1,m2 | monomial_mul m1 m2 = m} - (\(m1,m2). ring_mul r (p m1) (q m2)) = - ring_add r (ring_mul r (p monomial_1) (q m)) - (ring_sum r ({m1,m2 | monomial_mul m1 m2 = m} DELETE - (monomial_1,m)) - (\(m1,m2). ring_mul r (p m1) (q m2)))` - MP_TAC THENL - [SIMP_TAC[RING_SUM_DELETE; RING_MUL; MONOMIAL_MUL_LID; - MONOMIAL_FINITE_DIVISORPAIRS; monomial; IN_ELIM_PAIR_THM] THEN - REPEAT STRIP_TAC THEN MATCH_MP_TAC(RING_RULE - `x IN ring_carrier r /\ y IN ring_carrier r - ==> x = ring_add r y (ring_sub r x y)`) THEN - ASM_SIMP_TAC[RING_SUM; RING_MUL]; - SIMP_TAC[] THEN DISCH_THEN(K ALL_TAC) THEN STRIP_TAC] THEN - REWRITE_TAC[NOT_IMP; AND_FORALL_THM] THEN - MP_TAC(ISPEC `(:V)` WO) THEN DISCH_THEN(X_CHOOSE_TAC `l:V->V->bool`) THEN - FIRST_ASSUM(ASSUME_TAC o MATCH_MP WOSET_MONOMIAL_LE) THEN - FIRST_ASSUM(MP_TAC o CONJUNCT2 o GEN_REWRITE_RULE I [WOSET_WF]) THEN - REWRITE_TAC[PROPERLY_MONOMIAL_LE] THEN - DISCH_THEN(MATCH_MP_TAC o MATCH_MP WF_REC_EXISTS) THEN CONJ_TAC THENL - [REPEAT STRIP_TAC THEN AP_TERM_TAC THEN - MATCH_MP_TAC(TAUT `(p ==> (q <=> r)) ==> (p ==> q <=> p ==> r)`) THEN - REWRITE_TAC[monomial] THEN STRIP_TAC THEN - AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN - MATCH_MP_TAC RING_SUM_EQ THEN - REWRITE_TAC[IN_DELETE; IMP_CONJ; FORALL_IN_GSPEC] THEN - MAP_EVERY X_GEN_TAC [`m1:V->num`; `m2:V->num`] THEN - ASM_CASES_TAC `m1:V->num = monomial_1` THEN - ASM_SIMP_TAC[PAIR_EQ; MONOMIAL_MUL_LID] THEN DISCH_TAC THEN - AP_TERM_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN - FIRST_ASSUM(SUBST1_TAC o SYM) THEN - GEN_REWRITE_TAC LAND_CONV [GSYM MONOMIAL_MUL_LID] THEN - REWRITE_TAC[MONOMIAL_LT_RMUL] THEN - ASM_REWRITE_TAC[monomial_lt; MONOMIAL_GE_1] THEN - ASM_MESON_TAC[MONOMIAL_MUL; MONOMIAL]; - ALL_TAC] THEN - MAP_EVERY X_GEN_TAC [`q:(V->num)->A`; `m:V->num`] THEN - REWRITE_TAC[TAUT `p ==> q /\ r <=> (p ==> q) /\ (p ==> r)`] THEN - REWRITE_TAC[FORALL_AND_THM] THEN - DISCH_THEN(CONJUNCTS_THEN STRIP_ASSUME_TAC o CONJUNCT1) THEN - ASM_CASES_TAC `monomial s (m:V->num)` THEN ASM_REWRITE_TAC[] THENL - [ALL_TAC; MESON_TAC[RING_0]] THEN - SUBGOAL_THEN - `!w x z:A. - w IN ring_carrier r /\ x IN ring_carrier r /\ z IN ring_carrier r /\ - (!z. z IN ring_carrier r - ==> ?y. y IN ring_carrier r /\ - ring_mul r x y = z) - ==> ?y. y IN ring_carrier r /\ - ring_add r (ring_mul r x y) z = w` - MATCH_MP_TAC THENL - [MAP_EVERY X_GEN_TAC [`a:A`; `b:A`; `c:A`] THEN - REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN - DISCH_THEN(MP_TAC o SPEC `ring_sub r a c:A`) THEN - ASM_SIMP_TAC[RING_SUB] THEN - MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d:A` THEN - DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN - ASM_REWRITE_TAC[] THEN RING_TAC; - ASM_REWRITE_TAC[RING_SUM]] THEN - CONJ_TAC THENL [MESON_TAC[RING_0; RING_1]; ALL_TAC] THEN - X_GEN_TAC `a:A` THEN DISCH_TAC THEN - FIRST_X_ASSUM(X_CHOOSE_THEN `b:A` STRIP_ASSUME_TAC) THEN - EXISTS_TAC `ring_mul r b a:A` THEN - ASM_SIMP_TAC[RING_MUL; RING_MUL_ASSOC; RING_MUL_LID]);; - -let LOCAL_POWSER_RING = prove - (`!(r:A ring) (s:V->bool). - local_ring r ==> local_ring(powser_ring r s)`, - REPEAT GEN_TAC THEN - REWRITE_TAC[LOCAL_RING_IDEAL_NONUNITS; RING_IDEAL_NONUNITS] THEN - STRIP_TAC THEN ASM_REWRITE_TAC[TRIVIAL_POWSER_RING] THEN - ASM_SIMP_TAC[RING_UNIT_POWSER_RING; RING_ADD] THEN - REWRITE_TAC[CONJUNCT2 POWSER_RING; poly_add] THEN - REPEAT GEN_TAC THEN STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN - ASM SET_TAC[RING_CARRIER_POWSER_RING]);; - (* ------------------------------------------------------------------------- *) (* Polynomial evaluation. *) (* ------------------------------------------------------------------------- *) @@ -19080,6 +18995,13 @@ let POLY_EVALUATE_EQ = prove MATCH_MP_TAC POLY_EXTEND_EQ THEN EXISTS_TAC `s:V->bool` THEN ASM_REWRITE_TAC[RING_HOMOMORPHISM_I]);; +let POLY_EVALUATE_AT_0 = prove + (`!r (p:(V->num)->A). + p IN ring_carrier (poly_ring r v) + ==> poly_evaluate r p (\x. ring_0 r) = p monomial_1`, + REPEAT STRIP_TAC THEN REWRITE_TAC[poly_evaluate] THEN + ASM_MESON_TAC[POLY_EXTEND_AT_0; RING_HOMOMORPHISM_I; I_THM]);; + (* ------------------------------------------------------------------------- *) (* Same for univariate polynomials with simpler interface *) (* ------------------------------------------------------------------------- *) @@ -19224,6 +19146,13 @@ let POLY_EXPAND = prove MATCH_MP_TAC POLY_EXTEND_UNIVARIATE THEN ASM_REWRITE_TAC[RING_HOMOMORPHISM_POLY_CONST; POLY_VAR_UNIV]);; +let POLY_EVAL_AT_0 = prove + (`!(r:A ring) p. + p IN ring_carrier (poly_ring r (:1)) + ==> poly_eval r p (ring_0 r) = p (\v. 0)`, + REPEAT STRIP_TAC THEN REWRITE_TAC[poly_eval; GSYM monomial_1] THEN + ASM_MESON_TAC[POLY_EVALUATE_AT_0]);; + (* ------------------------------------------------------------------------- *) (* Composing polynomials and power series with homomorphisms. *) (* ------------------------------------------------------------------------- *) @@ -19400,6 +19329,330 @@ let RING_ISOMORPHISM_POLY_RINGS = prove REWRITE_TAC[GSYM RING_MONOMORPHISM_EPIMORPHISM] THEN SIMP_TAC[RING_MONOMORPHISM_POLY_RINGS; RING_EPIMORPHISM_POLY_RINGS]);; +(* ------------------------------------------------------------------------- *) +(* Zerodivisors, nilpotents and units in polynomial and power series rings. *) +(* ------------------------------------------------------------------------- *) + +let INTEGRAL_DOMAIN_POWSER_RING = prove + (`!(r:A ring) (s:V->bool). + integral_domain(powser_ring r s) <=> integral_domain r`, + REPEAT GEN_TAC THEN EQ_TAC THENL + [MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] + INTEGRAL_DOMAIN_MONOMORPHIC_PREIMAGE) THEN + MESON_TAC[RING_MONOMORPHISM_POWSER_CONST]; + REWRITE_TAC[integral_domain; GSYM TRIVIAL_RING_10]] THEN + MATCH_MP_TAC MONO_AND THEN REWRITE_TAC[TRIVIAL_POWSER_RING] THEN + REWRITE_TAC[RING_CARRIER_POWSER_RING] THEN REWRITE_TAC[POWSER_RING] THEN + DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`p:(V->num)->A`; `q:(V->num)->A`] THEN + REWRITE_TAC[IN_ELIM_THM] THEN + REPEAT(DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC)) THEN + GEN_REWRITE_TAC I [GSYM CONTRAPOS_THM] THEN + REWRITE_TAC[DE_MORGAN_THM; FUN_EQ_THM; NOT_FORALL_THM; poly_0] THEN + REWRITE_TAC[POLY_CONST_0; POLY_0; poly_mul] THEN DISCH_TAC THEN + MP_TAC(ISPEC `(:V)` WO) THEN DISCH_THEN(X_CHOOSE_TAC `l:V->V->bool`) THEN + FIRST_ASSUM(ASSUME_TAC o MATCH_MP WOSET_MONOMIAL_LE) THEN + FIRST_ASSUM(MP_TAC o CONJUNCT2 o GEN_REWRITE_RULE I [WOSET]) THEN + REWRITE_TAC[FLD_MONOMIAL_LE] THEN DISCH_THEN(fun th -> + MP_TAC(SPEC `{m | ~((q:(V->num)->A) m = ring_0 r)}` th) THEN + MP_TAC(SPEC `{m | ~((p:(V->num)->A) m = ring_0 r)}` th)) THEN + ASM_REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; MONOMIAL; IN_ELIM_THM; SUBSET] THEN + ANTS_TAC THENL [ASM_MESON_TAC[monomial]; ALL_TAC] THEN + DISCH_THEN(X_CHOOSE_THEN `mp:V->num` STRIP_ASSUME_TAC) THEN + ANTS_TAC THENL [ASM_MESON_TAC[monomial]; ALL_TAC] THEN + DISCH_THEN(X_CHOOSE_THEN `mq:V->num` STRIP_ASSUME_TAC) THEN + EXISTS_TAC `monomial_mul mp mq:V->num` THEN MATCH_MP_TAC(MESON[] + `!m. ~(ring_sum r {m} f = z) /\ ring_sum r s f = ring_sum r {m} f + ==> ~(ring_sum r s f = z)`) THEN + EXISTS_TAC `(mp:V->num),(mq:V->num)` THEN CONJ_TAC THENL + [ASM_SIMP_TAC[RING_SUM_SING; RING_MUL] THEN ASM_MESON_TAC[]; ALL_TAC] THEN + MATCH_MP_TAC RING_SUM_SUPERSET THEN + REWRITE_TAC[SING_SUBSET; FORALL_IN_GSPEC; IMP_CONJ] THEN + REWRITE_TAC[IN_ELIM_PAIR_THM; IN_SING] THEN + MAP_EVERY X_GEN_TAC [`np:V->num`; `nq:V->num`] THEN + DISCH_TAC THEN REWRITE_TAC[PAIR_EQ; DE_MORGAN_THM] THEN + ASM_CASES_TAC `(p:(V->num)->A) np = ring_0 r` THENL + [ASM_SIMP_TAC[RING_MUL_LZERO]; ALL_TAC] THEN + ASM_CASES_TAC `(q:(V->num)->A) nq = ring_0 r` THENL + [ASM_SIMP_TAC[RING_MUL_RZERO]; ALL_TAC] THEN + MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN STRIP_TAC THEN + FIRST_ASSUM(MP_TAC o MATCH_MP (MESON[MONOMIAL_LT_REFL] + `m' = m ==> !l. ~monomial_lt l m m'`)) THEN + DISCH_THEN(MP_TAC o SPEC `l:V->V->bool`) THEN REWRITE_TAC[] THENL + [MATCH_MP_TAC MONOMIAL_LTE_MUL2; + MATCH_MP_TAC MONOMIAL_LET_MUL2] THEN + ASM_SIMP_TAC[monomial_lt; WOSET_IMP_POSET]);; + +let INTEGRAL_DOMAIN_POLY_RING = prove + (`!(r:A ring) (s:V->bool). + integral_domain(poly_ring r s) <=> integral_domain r`, + REPEAT GEN_TAC THEN EQ_TAC THENL + [ALL_TAC; GEN_REWRITE_TAC LAND_CONV [GSYM INTEGRAL_DOMAIN_POWSER_RING]] THEN + MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] + INTEGRAL_DOMAIN_MONOMORPHIC_PREIMAGE) THEN + MESON_TAC[RING_MONOMORPHISM_POLY_CONST; RING_MONOMORPHISM_POLY_POWSER]);; + +let RING_UNIT_POLY_CONST = prove + (`!r s c. ring_unit (poly_ring r s) (poly_const r c:(V->num)->A) <=> + ring_unit r c`, + REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL + [MP_TAC(ISPECL [`r:A ring`; `s:V->bool`] RING_HOMOMORPHISM_MONOMIAL_1) THEN + DISCH_THEN(MP_TAC o SPEC `poly_const r c:(V->num)->A` o + MATCH_MP(REWRITE_RULE[IMP_CONJ] RING_UNIT_HOMOMORPHIC_IMAGE)) THEN + ASM_REWRITE_TAC[] THEN REWRITE_TAC[poly_const]; + MATCH_MP_TAC RING_UNIT_HOMOMORPHIC_IMAGE THEN + EXISTS_TAC `r:A ring` THEN + ASM_REWRITE_TAC[RING_HOMOMORPHISM_POLY_CONST]]);; + +let RING_UNIT_POLY_DOMAIN = prove + (`!r s (p:(V->num)->A). + integral_domain r + ==> (ring_unit (poly_ring r s) p <=> + ?c. ring_unit r c /\ p = poly_const r c)`, + REPEAT STRIP_TAC THEN + MATCH_MP_TAC(MESON[] + `(!x. Q(f x) <=> P x) /\ (!y. Q y ==> ?x. y = f x) + ==> (Q y <=> ?x. P x /\ y = f x)`) THEN + REWRITE_TAC[RING_UNIT_POLY_CONST] THEN + X_GEN_TAC `p:(V->num)->A` THEN REWRITE_TAC[ring_unit] THEN + REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN + X_GEN_TAC `q:(V->num)->A` THEN + REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN + MAP_EVERY ASM_CASES_TAC + [`p:(V->num)->A = ring_0(poly_ring r s)`; + `q:(V->num)->A = ring_0(poly_ring r s)`] THEN + ASM_SIMP_TAC[RING_MUL_LZERO; INTEGRAL_DOMAIN_NONTRIVIAL; RING_0; + INTEGRAL_DOMAIN_POLY_RING; RING_MUL_RZERO] THEN + DISCH_THEN(MP_TAC o AP_TERM `poly_deg r:((V->num)->A)->num`) THEN + REWRITE_TAC[POLY_RING; POLY_DEG_1] THEN + RULE_ASSUM_TAC(REWRITE_RULE[POLY_RING; IN_ELIM_THM]) THEN + ASM_SIMP_TAC[POLY_DEG_MUL; ADD_EQ_0] THEN ASM_MESON_TAC[POLY_DEG_EQ_0]);; + +let RING_NILPOTENT_POLY_RING = prove + (`!r s (p:(V->num)->A). + ring_nilpotent (poly_ring r s) p <=> + p IN ring_carrier(poly_ring r s) /\ (!m. ring_nilpotent r (p m))`, + REPEAT GEN_TAC THEN + ASM_CASES_TAC `(p:(V->num)->A) IN ring_carrier(poly_ring r s)` THENL + [ASM_REWRITE_TAC[]; ASM_MESON_TAC[ring_nilpotent]] THEN + EQ_TAC THEN DISCH_TAC THENL + [X_GEN_TAC `m:V->num` THEN + MP_TAC(ISPEC `r:A ring` RING_NILRADICAL) THEN + GEN_REWRITE_TAC LAND_CONV [EXTENSION] THEN + DISCH_THEN(MP_TAC o SPEC `(p:(V->num)->A) m`) THEN + REWRITE_TAC[RADICAL_0; IN_ELIM_THM] THEN + DISCH_THEN SUBST1_TAC THEN COND_CASES_TAC THENL + [FIRST_X_ASSUM(SUBST1_TAC o SYM o GEN_REWRITE_RULE I [trivial_ring]) THEN + ASM_MESON_TAC[POLY_MONOMIAL_IN_CARRIER]; + REWRITE_TAC[IN_INTERS; FORALL_IN_GSPEC]] THEN + X_GEN_TAC `j:A->bool` THEN DISCH_TAC THEN + FIRST_ASSUM(ASSUME_TAC o MATCH_MP PRIME_IMP_RING_IDEAL) THEN + SUBGOAL_THEN + `ring_nilpotent + (poly_ring (quotient_ring r j) s) + (ring_coset r (j:A->bool) o (p:(V->num)->A))` + MP_TAC THENL + [MATCH_MP_TAC RING_NILPOTENT_HOMOMORPHIC_IMAGE THEN + EXISTS_TAC `poly_ring (r:A ring) (s:V->bool)` THEN + ASM_REWRITE_TAC[] THEN + MATCH_MP_TAC(REWRITE_RULE[ETA_AX] RING_HOMOMORPHISM_POLY_RINGS) THEN + ASM_SIMP_TAC[RING_HOMOMORPHISM_RING_COSET; PRIME_IMP_RING_IDEAL]; + ASM_SIMP_TAC[INTEGRAL_DOMAIN_NILPOTENT; INTEGRAL_DOMAIN_POLY_RING; + INTEGRAL_DOMAIN_QUOTIENT_RING]] THEN + GEN_REWRITE_TAC LAND_CONV [FUN_EQ_THM] THEN + DISCH_THEN(MP_TAC o SPEC `m:V->num`) THEN + ASM_SIMP_TAC[POLY_RING; POLY_0; o_THM; QUOTIENT_RING; RING_COSET_0; + RING_IDEAL_IMP_SUBSET] THEN + ASM_MESON_TAC[POLY_MONOMIAL_IN_CARRIER; RING_COSET_EQ_IDEAL]; + FIRST_ASSUM(ASSUME_TAC o MATCH_MP POLY_MONOMIALS_FINITE) THEN + FIRST_ASSUM(SUBST1_TAC o SYM o MATCH_MP POLY_EXTEND_ID) THEN + REWRITE_TAC[poly_extend] THEN MATCH_MP_TAC RING_NILPOTENT_SUM THEN + ASM_REWRITE_TAC[FORALL_IN_GSPEC] THEN X_GEN_TAC `m:V->num` THEN + DISCH_TAC THEN MATCH_MP_TAC RING_NILPOTENT_RMUL THEN + REWRITE_TAC[RING_PRODUCT] THEN + MATCH_MP_TAC RING_NILPOTENT_HOMOMORPHIC_IMAGE THEN + EXISTS_TAC `r:A ring` THEN + ASM_REWRITE_TAC[RING_HOMOMORPHISM_POLY_CONST]]);; + +let RING_UNIT_POLY_RING = prove + (`!r s (p:(V->num)->A). + ring_unit (poly_ring r s) p <=> + p IN ring_carrier(poly_ring r s) /\ + ring_unit r (p monomial_1) /\ + (!m. ~(m = monomial_1) ==> ring_nilpotent r (p m))`, + REPEAT GEN_TAC THEN + ASM_CASES_TAC `(p:(V->num)->A) IN ring_carrier(poly_ring r s)` THENL + [ASM_REWRITE_TAC[]; ASM_MESON_TAC[ring_unit]] THEN + EQ_TAC THEN DISCH_TAC THEN TRY CONJ_TAC THENL + [MP_TAC(MATCH_MP (REWRITE_RULE[IMP_CONJ] RING_UNIT_HOMOMORPHIC_IMAGE) + (ISPECL [`r:A ring`; `s:V->bool`] RING_HOMOMORPHISM_MONOMIAL_1)) THEN + ASM_SIMP_TAC[]; + X_GEN_TAC `m:V->num` THEN DISCH_TAC THEN + MP_TAC(ISPEC `r:A ring` RING_NILRADICAL) THEN + GEN_REWRITE_TAC LAND_CONV [EXTENSION] THEN + DISCH_THEN(MP_TAC o SPEC `(p:(V->num)->A) m`) THEN + REWRITE_TAC[RADICAL_0; IN_ELIM_THM] THEN + DISCH_THEN SUBST1_TAC THEN COND_CASES_TAC THENL + [FIRST_X_ASSUM(SUBST1_TAC o SYM o GEN_REWRITE_RULE I [trivial_ring]) THEN + ASM_MESON_TAC[POLY_MONOMIAL_IN_CARRIER]; + REWRITE_TAC[IN_INTERS; FORALL_IN_GSPEC]] THEN + X_GEN_TAC `j:A->bool` THEN DISCH_TAC THEN + FIRST_ASSUM(ASSUME_TAC o MATCH_MP PRIME_IMP_RING_IDEAL) THEN + MP_TAC(ISPECL + [`quotient_ring r (j:A->bool)`; `s:V->bool`; + `ring_coset r (j:A->bool) o (p:(V->num)->A)`] + RING_UNIT_POLY_DOMAIN) THEN + ASM_SIMP_TAC[INTEGRAL_DOMAIN_POLY_RING; INTEGRAL_DOMAIN_QUOTIENT_RING] THEN + DISCH_THEN(MP_TAC o fst o EQ_IMP_RULE) THEN ANTS_TAC THENL + [MATCH_MP_TAC RING_UNIT_HOMOMORPHIC_IMAGE THEN + EXISTS_TAC `poly_ring (r:A ring) (s:V->bool)` THEN + ASM_REWRITE_TAC[] THEN + MATCH_MP_TAC(REWRITE_RULE[ETA_AX] RING_HOMOMORPHISM_POLY_RINGS) THEN + ASM_SIMP_TAC[RING_HOMOMORPHISM_RING_COSET; PRIME_IMP_RING_IDEAL]; + DISCH_THEN(X_CHOOSE_THEN `c:A->bool` STRIP_ASSUME_TAC)] THEN + FIRST_X_ASSUM(MP_TAC o SPEC `m:V->num` o + GEN_REWRITE_RULE I [FUN_EQ_THM]) THEN + ASM_SIMP_TAC[poly_const; o_THM; QUOTIENT_RING; RING_COSET_0; + RING_IDEAL_IMP_SUBSET] THEN + ASM_MESON_TAC[POLY_MONOMIAL_IN_CARRIER; RING_COSET_EQ_IDEAL]; + ASM_CASES_TAC `trivial_ring (r:A ring)` THENL + [ASM_MESON_TAC[TRIVIAL_POLY_RING; trivial_ring; RING_UNIT_0; IN_SING]; + ALL_TAC] THEN + FIRST_ASSUM(ASSUME_TAC o MATCH_MP POLY_MONOMIALS_FINITE) THEN + FIRST_ASSUM(ASSUME_TAC o MATCH_MP POLY_MONOMIAL_IN_CARRIER) THEN + FIRST_ASSUM(SUBST1_TAC o SYM o MATCH_MP POLY_EXTEND_ID) THEN + REWRITE_TAC[poly_extend] THEN + SUBGOAL_THEN + `{m | ~((p:(V->num)->A) m = ring_0 r)} = + monomial_1 INSERT ({m | ~(p m = ring_0 r)} DELETE monomial_1)` + SUBST1_TAC THENL + [REWRITE_TAC[SET_RULE + `{x | P x} = a INSERT ({x | P x} DELETE a) <=> P a`] THEN + ASM_MESON_TAC[RING_UNIT_0]; + + ASM_SIMP_TAC[RING_SUM_CLAUSES; FINITE_DELETE; RING_MUL; POLY_CONST; + RING_PRODUCT; IN_DELETE]] THEN + MATCH_MP_TAC(CONJUNCT1 RING_UNIT_NILPOTENT_CLAUSES) THEN CONJ_TAC THENL + [REWRITE_TAC[MONOMIAL_VARS_1; RING_PRODUCT_CLAUSES] THEN + ASM_SIMP_TAC[RING_MUL_RID; POLY_CONST; RING_UNIT_POLY_CONST]; + MATCH_MP_TAC RING_NILPOTENT_SUM THEN + ASM_REWRITE_TAC[FINITE_DELETE; IN_ELIM_THM; IN_DELETE] THEN + X_GEN_TAC `m:V->num` THEN + DISCH_TAC THEN MATCH_MP_TAC RING_NILPOTENT_RMUL THEN + REWRITE_TAC[RING_PRODUCT] THEN + MATCH_MP_TAC RING_NILPOTENT_HOMOMORPHIC_IMAGE THEN + EXISTS_TAC `r:A ring` THEN + ASM_SIMP_TAC[RING_HOMOMORPHISM_POLY_CONST]]]);; + +let RING_UNIT_POWSER_RING = prove + (`!(r:A ring) (s:V->bool) p. + ring_unit (powser_ring r s) p <=> + p IN ring_carrier(powser_ring r s) /\ + ring_unit r (p monomial_1)`, + REPEAT GEN_TAC THEN REWRITE_TAC[ring_unit] THEN + EQ_TAC THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN + ASM_REWRITE_TAC[] THENL + [CONJ_TAC THENL + [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV + [RING_CARRIER_POWSER_RING]) THEN + SIMP_TAC[IN_ELIM_THM]; + FIRST_X_ASSUM(X_CHOOSE_THEN `q:(V->num)->A` MP_TAC) THEN + DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN + REWRITE_TAC[POWSER_RING] THEN DISCH_TAC THEN + EXISTS_TAC `(q:(V->num)->A) monomial_1` THEN + RULE_ASSUM_TAC(REWRITE_RULE[RING_CARRIER_POWSER_RING; IN_ELIM_THM]) THEN + FIRST_X_ASSUM(MP_TAC o C AP_THM `monomial_1:V->num`) THEN + ASM_REWRITE_TAC[poly_mul; poly_1; MONOMIAL_MUL_EQ_1; poly_const] THEN + REWRITE_TAC[SET_RULE `{f x y | x = a /\ y = b} = {f a b}`] THEN + ASM_SIMP_TAC[RING_SUM_SING; RING_MUL]]; + ONCE_REWRITE_TAC[TAUT `p /\ q <=> ~(p ==> ~q)`] THEN + MP_TAC(ISPECL [`r:A ring`; `s:V->bool`] POWSER_RING_EQ) THEN + ASM_SIMP_TAC[POWSER_RING_EQ; RING_MUL; RING_1] THEN + DISCH_THEN(K ALL_TAC) THEN + REWRITE_TAC[RING_CARRIER_POWSER_RING; CONJUNCT2 POWSER_RING] THEN + FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV + [RING_CARRIER_POWSER_RING]) THEN + REWRITE_TAC[IN_ELIM_THM; poly_mul; poly_1; poly_const]] THEN + SUBGOAL_THEN + `!(q:(V->num)->A) m. + monomial s m /\ + (!m. p m IN ring_carrier r) /\ + (!m. q m IN ring_carrier r) + ==> ring_sum r {m1,m2 | monomial_mul m1 m2 = m} + (\(m1,m2). ring_mul r (p m1) (q m2)) = + ring_add r (ring_mul r (p monomial_1) (q m)) + (ring_sum r ({m1,m2 | monomial_mul m1 m2 = m} DELETE + (monomial_1,m)) + (\(m1,m2). ring_mul r (p m1) (q m2)))` + MP_TAC THENL + [SIMP_TAC[RING_SUM_DELETE; RING_MUL; MONOMIAL_MUL_LID; + MONOMIAL_FINITE_DIVISORPAIRS; monomial; IN_ELIM_PAIR_THM] THEN + REPEAT STRIP_TAC THEN MATCH_MP_TAC(RING_RULE + `x IN ring_carrier r /\ y IN ring_carrier r + ==> x = ring_add r y (ring_sub r x y)`) THEN + ASM_SIMP_TAC[RING_SUM; RING_MUL]; + SIMP_TAC[] THEN DISCH_THEN(K ALL_TAC) THEN STRIP_TAC] THEN + REWRITE_TAC[NOT_IMP; AND_FORALL_THM] THEN + MP_TAC(ISPEC `(:V)` WO) THEN DISCH_THEN(X_CHOOSE_TAC `l:V->V->bool`) THEN + FIRST_ASSUM(ASSUME_TAC o MATCH_MP WOSET_MONOMIAL_LE) THEN + FIRST_ASSUM(MP_TAC o CONJUNCT2 o GEN_REWRITE_RULE I [WOSET_WF]) THEN + REWRITE_TAC[PROPERLY_MONOMIAL_LE] THEN + DISCH_THEN(MATCH_MP_TAC o MATCH_MP WF_REC_EXISTS) THEN CONJ_TAC THENL + [REPEAT STRIP_TAC THEN AP_TERM_TAC THEN + MATCH_MP_TAC(TAUT `(p ==> (q <=> r)) ==> (p ==> q <=> p ==> r)`) THEN + REWRITE_TAC[monomial] THEN STRIP_TAC THEN + AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN + MATCH_MP_TAC RING_SUM_EQ THEN + REWRITE_TAC[IN_DELETE; IMP_CONJ; FORALL_IN_GSPEC] THEN + MAP_EVERY X_GEN_TAC [`m1:V->num`; `m2:V->num`] THEN + ASM_CASES_TAC `m1:V->num = monomial_1` THEN + ASM_SIMP_TAC[PAIR_EQ; MONOMIAL_MUL_LID] THEN DISCH_TAC THEN + AP_TERM_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN + FIRST_ASSUM(SUBST1_TAC o SYM) THEN + GEN_REWRITE_TAC LAND_CONV [GSYM MONOMIAL_MUL_LID] THEN + REWRITE_TAC[MONOMIAL_LT_RMUL] THEN + ASM_REWRITE_TAC[monomial_lt; MONOMIAL_GE_1] THEN + ASM_MESON_TAC[MONOMIAL_MUL; MONOMIAL]; + ALL_TAC] THEN + MAP_EVERY X_GEN_TAC [`q:(V->num)->A`; `m:V->num`] THEN + REWRITE_TAC[TAUT `p ==> q /\ r <=> (p ==> q) /\ (p ==> r)`] THEN + REWRITE_TAC[FORALL_AND_THM] THEN + DISCH_THEN(CONJUNCTS_THEN STRIP_ASSUME_TAC o CONJUNCT1) THEN + ASM_CASES_TAC `monomial s (m:V->num)` THEN ASM_REWRITE_TAC[] THENL + [ALL_TAC; MESON_TAC[RING_0]] THEN + SUBGOAL_THEN + `!w x z:A. + w IN ring_carrier r /\ x IN ring_carrier r /\ z IN ring_carrier r /\ + (!z. z IN ring_carrier r + ==> ?y. y IN ring_carrier r /\ + ring_mul r x y = z) + ==> ?y. y IN ring_carrier r /\ + ring_add r (ring_mul r x y) z = w` + MATCH_MP_TAC THENL + [MAP_EVERY X_GEN_TAC [`a:A`; `b:A`; `c:A`] THEN + REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN + DISCH_THEN(MP_TAC o SPEC `ring_sub r a c:A`) THEN + ASM_SIMP_TAC[RING_SUB] THEN + MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d:A` THEN + DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN + ASM_REWRITE_TAC[] THEN RING_TAC; + ASM_REWRITE_TAC[RING_SUM]] THEN + CONJ_TAC THENL [MESON_TAC[RING_0; RING_1]; ALL_TAC] THEN + X_GEN_TAC `a:A` THEN DISCH_TAC THEN + FIRST_X_ASSUM(X_CHOOSE_THEN `b:A` STRIP_ASSUME_TAC) THEN + EXISTS_TAC `ring_mul r b a:A` THEN + ASM_SIMP_TAC[RING_MUL; RING_MUL_ASSOC; RING_MUL_LID]);; + +let LOCAL_POWSER_RING = prove + (`!(r:A ring) (s:V->bool). + local_ring r ==> local_ring(powser_ring r s)`, + REPEAT GEN_TAC THEN + REWRITE_TAC[LOCAL_RING_IDEAL_NONUNITS; RING_IDEAL_NONUNITS] THEN + STRIP_TAC THEN ASM_REWRITE_TAC[TRIVIAL_POWSER_RING] THEN + ASM_SIMP_TAC[RING_UNIT_POWSER_RING; RING_ADD] THEN + REWRITE_TAC[CONJUNCT2 POWSER_RING; poly_add] THEN + REPEAT GEN_TAC THEN STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN + ASM SET_TAC[RING_CARRIER_POWSER_RING]);; + (* ------------------------------------------------------------------------- *) (* X - a divides p(X) - p(a) and consequences like finiteness of roots. *) (* ------------------------------------------------------------------------- *) diff --git a/Library/words.ml b/Library/words.ml index 27131eb1..d38b516c 100644 --- a/Library/words.ml +++ b/Library/words.ml @@ -1278,7 +1278,7 @@ let TWOS_COMPLEMENT_GEN = prove ==> n DIV 2 EXP p = (2 EXP k - 1) * bitval(x < &0) /\ &n - &2 pow (p + k) * &(bitval(x < &0)) = x`, REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[bitval] THEN - COND_CASES_TAC THEN + COND_CASES_TAC THEN ASM_REWRITE_TAC[INT_MUL_RZERO; INT_MUL_RID; INT_EQ_SUB_RADD; GSYM INT_OF_NUM_CLAUSES; GSYM INT_OF_NUM_DIV] THEN SIMP_TAC[GSYM INT_OF_NUM_SUB; LE_1; EXP_EQ_0; ARITH_EQ; @@ -1286,7 +1286,7 @@ let TWOS_COMPLEMENT_GEN = prove MATCH_MP_TAC(TAUT `q /\ (q ==> p) ==> p /\ q`) THEN (CONJ_TAC THENL [MATCH_MP_TAC INT_CONG_IMP_EQ THEN EXISTS_TAC `(&2:int) pow (p + k)` THEN - ASM_REWRITE_TAC[INTEGER_RULE + ASM_REWRITE_TAC[INTEGER_RULE `(n:int == x + p) (mod p) <=> (n == x) (mod p)`] THEN MATCH_MP_TAC(INT_ARITH `&0 <= x /\ x < p /\ &0 <= y /\ y < p @@ -1301,7 +1301,7 @@ let TWOS_COMPLEMENT_GEN = prove SIMP_TAC[INT_POW_ADD; INT_DIV_MUL_ADD; INT_POW_EQ_0; INT_OF_NUM_EQ; ARITH_EQ; INT_ARITH `x + k:int = k - &1 <=> x + &1 = &0`] THEN TRANS_TAC EQ_TRANS `(x + &1 * &2 pow p) div &2 pow p` THEN CONJ_TAC THENL - [SIMP_TAC[INT_POW_ADD; INT_DIV_MUL_ADD; INT_POW_EQ_0; INT_OF_NUM_EQ; + [SIMP_TAC[INT_POW_ADD; INT_DIV_MUL_ADD; INT_POW_EQ_0; INT_OF_NUM_EQ; ARITH_EQ]; REWRITE_TAC[INT_DIV_EQ_0] THEN ASM_INT_ARITH_TAC]);; @@ -8246,9 +8246,3 @@ let SIMD2 = prove ADD_SUB2; ARITH_RULE `i < n ==> i < 2 * n`; ARITH_RULE `n + i < 2 * n <=> i < n`; ARITH_RULE `~(n + i:num < n)`]);; - -(* ------------------------------------------------------------------------- *) -(* Some explicit formulas for comparisons in terms of top bit. *) -(* ------------------------------------------------------------------------- *) - -