From 900bf74c734e3c6829760a9bee9d68fe4e6b2935 Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Thu, 21 Sep 2023 12:07:43 +1200 Subject: [PATCH] More fixes to multiple-rebinds of theorems under same name --- examples/algebra/field/fieldMapScript.sml | 2 +- examples/algebra/field/fieldScript.sml | 50 ++---- .../algebra/polynomial/polyRingScript.sml | 144 +++++------------- 3 files changed, 51 insertions(+), 145 deletions(-) diff --git a/examples/algebra/field/fieldMapScript.sml b/examples/algebra/field/fieldMapScript.sml index 60e7aaa33f..3be9e3daa7 100644 --- a/examples/algebra/field/fieldMapScript.sml +++ b/examples/algebra/field/fieldMapScript.sml @@ -2273,7 +2273,7 @@ QED Since (ring_inj_image r f).sum.id = f #0 by ring_inj_image_def The result follows by field_inj_image_prod_nonzero_group *) -Theorem field_inj_image_field: +Theorem field_inj_image_field[allow_rebind]: !(r:'a field) f. Field r /\ INJ f R univ(:'b) ==> Field (ring_inj_image r f) Proof rpt strip_tac >> diff --git a/examples/algebra/field/fieldScript.sml b/examples/algebra/field/fieldScript.sml index 12e557f082..397fe5fca0 100644 --- a/examples/algebra/field/fieldScript.sml +++ b/examples/algebra/field/fieldScript.sml @@ -1906,40 +1906,26 @@ val field_inv_mult = store_thm( (* export simple theorem *) val _ = export_rewrites ["field_inv_mult"]; -(* Theorem: Field r ==> |/ #1 = #1 *) -(* Proof: by group_inv_id and r.prod group. *) -val field_inv_one = store_thm( - "field_inv_one", - ``!r:'a field. Field r ==> ( |/ #1 = #1)``, - metis_tac[group_inv_id |> SPEC ``f*`` |> UNDISCH_ALL - |> PROVE_HYP (field_mult_group |> SPEC_ALL |> UNDISCH_ALL |> CONJUNCT1) |> DISCH_ALL, - field_mult_group, field_nonzero_mult_property, group_id_element, field_mult_inv]); -(* > val field_inv_one = |- !r:'a field. Field r ==> ( |/ #1 = #1) : thm *) - -(* Same theorem, simple proof. *) - (* Theorem: Field r ==> |/ #1 = #1 *) (* Proof: by ring_inv_one, field_is_ring. *) -val field_inv_one = store_thm( - "field_inv_one", - ``!r:'a field. Field r ==> ( |/ #1 = #1)``, - metis_tac[ring_inv_one, field_is_ring]); - -(* export simple theorem *) -val _ = export_rewrites ["field_inv_one"]; +Theorem field_inv_one[simp]: + !r:'a field. Field r ==> ( |/ #1 = #1) +Proof metis_tac[ring_inv_one, field_is_ring] +QED (* Theorem: |/ ( |/ x) = x *) (* Proof: by group_inv_inv and r.prod group. *) -val field_inv_inv = store_thm( - "field_inv_inv", - ``!r:'a field. Field r ==> !x. x IN R+ ==> ( |/ ( |/ x) = x)``, - metis_tac[group_inv_inv |> SPEC ``f*`` |> UNDISCH_ALL - |> PROVE_HYP (field_mult_group |> SPEC_ALL |> UNDISCH_ALL |> CONJUNCT1) |> DISCH_ALL, - field_mult_group, field_nonzero_mult_property, group_inv_element, field_mult_inv]); -(* > val field_inv_inv = |- !r:'a field. Field r ==> !x. x IN R+ ==> ( |/ ( |/ x) = x) : thm *) - -(* export simple theorem *) -val _ = export_rewrites ["field_inv_inv"]; +Theorem field_inv_inv[simp]: + !r:'a field. Field r ==> !x. x IN R+ ==> ( |/ ( |/ x) = x) +Proof + metis_tac[group_inv_inv + |> SPEC ``f*`` |> UNDISCH_ALL + |> PROVE_HYP + (field_mult_group |> SPEC_ALL |> UNDISCH_ALL |> CONJUNCT1) + |> DISCH_ALL, + field_mult_group, field_nonzero_mult_property, group_inv_element, + field_mult_inv] +QED (* Theorem: x IN R+ ==> - x IN R+ *) (* Proof: by contradiction. @@ -3269,12 +3255,6 @@ val finite_field_fermat_all = store_thm( Induct_on `n` >- rw[EXP] >> rw[EXP, field_exp_mult, finite_field_fermat_thm, Abbr`m`]); -val finite_field_fermat_all = store_thm( - "finite_field_fermat_all", - ``!r:'a field. FiniteField r ==> !x. x IN R ==> !n. x ** (CARD R ** n) = x``, - rpt (stripDup[FiniteField_def]) >> - Induct_on `n` >> - rw[EXP, field_exp_mult, finite_field_fermat_thm]); (* Theorem: FiniteField r ==> !x. x IN R ==> !n. x ** n = x ** (n MOD (CARD R)) *) (* Proof: diff --git a/examples/algebra/polynomial/polyRingScript.sml b/examples/algebra/polynomial/polyRingScript.sml index 065be0a0df..9b7c1c1182 100644 --- a/examples/algebra/polynomial/polyRingScript.sml +++ b/examples/algebra/polynomial/polyRingScript.sml @@ -1103,10 +1103,12 @@ val poly_mult_const_const = store_thm( = chop p by weak_mult_lone = p by poly_chop_poly *) -val poly_mult_lone = store_thm( - "poly_mult_lone", - ``!r:'a ring. Ring r ==> !p. poly p ==> ( |1| * p = p)``, - metis_tac[weak_one, poly_is_weak, poly_mult_def, poly_ring_ids, poly_chop_mult, weak_mult_lone, poly_chop_poly]); +Theorem poly_mult_lone[simp]: + !r:'a ring. Ring r ==> !p. poly p ==> ( |1| * p = p) +Proof + metis_tac[weak_one, poly_is_weak, poly_mult_def, poly_ring_ids, + poly_chop_mult, weak_mult_lone, poly_chop_poly] +QED (* Here, we don't have poly_mult_comm. *) @@ -1119,39 +1121,20 @@ val poly_mult_lone = store_thm( = chop p by weak_mult_rone = p by poly_chop_poly *) -val poly_mult_rone = store_thm( - "poly_mult_rone", - ``!r:'a ring. Ring r ==> !p. poly p ==> (p * |1| = p)``, - metis_tac[weak_one, poly_is_weak, poly_mult_def, poly_ring_ids, poly_chop_mult_comm, weak_mult_rone, poly_chop_poly]); - -val _ = export_rewrites ["poly_mult_lone", "poly_mult_rone"]; +Theorem poly_mult_rone[simp]: + !r:'a ring. Ring r ==> !p. poly p ==> (p * |1| = p) +Proof + metis_tac[weak_one, poly_is_weak, poly_mult_def, poly_ring_ids, + poly_chop_mult_comm, weak_mult_rone, poly_chop_poly] +QED (* Theorem: |1| * p = p and p * |1| = p *) (* Proof: combine poly_mult_lone and poly_mult_rone. *) +Theorem poly_mult_one: + !r:'a ring. Ring r ==> !p. poly p ==> ( |1| * p = p) /\ (p * |1| = p) +Proof rw[] +QED -(* val poly_mult_one = save_thm("poly_mult_one", CONJ poly_mult_lone poly_mult_rone); *) -(* > val poly_mult_one = |- (!r. Ring r ==> !p. poly p ==> ( |1| * p = p)) /\ !r. Ring r ==> !p. poly p ==> (p * |1| = p) : thm *) -val poly_mult_one = store_thm( - "poly_mult_one", - ``!r:'a ring. Ring r ==> !p. poly p ==> ( |1| * p = p) /\ (p * |1| = p)``, - rw[]); - -(* first try: *) -val poly_mult_one = save_thm("poly_mult_one", CONJ poly_mult_lone poly_mult_rone); -(* > val poly_mult_one = |- (!r. Ring r ==> !p. poly p ==> ( |1| * p = p)) /\ !r. Ring r ==> !p. poly p ==> (p * |1| = p) : thm *) - -(* better, but not the best: *) -val poly_mult_one = save_thm("poly_mult_one", - CONJ (poly_mult_lone |> SPEC_ALL |> UNDISCH |> SPEC_ALL) - (poly_mult_rone |> SPEC_ALL |> UNDISCH |> SPEC_ALL) |> GEN ``p:'a poly`` |> DISCH_ALL |> GEN_ALL); -(* > val poly_mult_one = |- !r. Ring r ==> !p. (poly p ==> ( |1| * p = p)) /\ (poly p ==> (p * |1| = p)) : thm *) - -(* the best: *) -val poly_mult_one = save_thm("poly_mult_one", - CONJ (poly_mult_lone |> SPEC_ALL |> UNDISCH |> SPEC_ALL |> UNDISCH) - (poly_mult_rone |> SPEC_ALL |> UNDISCH |> SPEC_ALL |> UNDISCH) - |> DISCH ``poly p`` |> GEN ``p:'a poly`` |> DISCH_ALL |> GEN_ALL); -(* > val poly_mult_one = |- !r. Ring r ==> !p. poly p ==> ( |1| * p = p) /\ (p * |1| = p) : thm *) (* To show closure for Monoid (PolyRing r).prod. *) @@ -1380,15 +1363,18 @@ val poly_one_eq_zero = lift_ring_thm "one_eq_zero" "one_eq_zero"; (* Proof: by above poly_one_eq_zero, and improve by ONE_ELEMENT_SING and IN_SING. *) -val poly_one_eq_zero = store_thm( - "poly_one_eq_zero", - ``!r:'a ring. Ring r ==> (( |1| = |0|) <=> !p. poly p ==> (p = |0|))``, +Theorem poly_one_eq_zero[allow_rebind]: + !r:'a ring. Ring r ==> (( |1| = |0|) <=> !p. poly p ==> (p = |0|)) +Proof rw_tac std_ss[EQ_IMP_THM] >| [ - `(PolyRing r).carrier = { |0| }` by rw_tac std_ss[GSYM poly_one_eq_zero] >> + ‘(PolyRing r).carrier = { |0| }’ by rw_tac std_ss[GSYM poly_one_eq_zero] >> metis_tac [poly_ring_property, IN_SING], - `(PolyRing r).carrier = { |0| }` by metis_tac [poly_ring_property, poly_zero_poly, MEMBER_NOT_EMPTY, ONE_ELEMENT_SING] >> + ‘(PolyRing r).carrier = { |0| }’ + by metis_tac [poly_ring_property, poly_zero_poly, MEMBER_NOT_EMPTY, + ONE_ELEMENT_SING] >> metis_tac [poly_one_eq_zero] - ]); + ] +QED (* Theorem: Ring r ==> ( |0| = |1|) <=> (#0 = #1) *) (* Proof: @@ -2567,81 +2553,26 @@ val poly_mult_cmult = store_thm( (* Theorems on polynomial multiplication with negation. *) (* ------------------------------------------------------------------------- *) -(* Theorem: (- p) * q = - (p * q) *) -(* Proof: - Since - (-p) * q + (p * q) - = (- p + p) * q by poly_mult_ladd - = |0| * p by poly_add_lneg - = |0| by poly_mult_lzero - Hence - (- p) * q = - (p * q) by poly_add_eq_zero -*) -val poly_mult_lneg = store_thm( - "poly_mult_lneg", - ``!r:'a ring. Ring r ==> !p q. poly p /\ poly q ==> ((- p) * q = - (p * q))``, - rpt strip_tac >> - `poly (-p)` by rw[] >> - `poly (-p * q) /\ poly (p * q)` by rw[] >> - `(-p) * q + (p * q) = (- p + p) * q` by rw_tac std_ss[poly_mult_ladd] >> - rw_tac std_ss[GSYM poly_add_eq_zero, poly_add_lneg, poly_mult_lzero]); -(* better by lifting *) +(* by lifting *) val poly_mult_lneg = lift_ring_thm_with_goal "mult_lneg" "mult_lneg" ``!r:'a ring. Ring r ==> !p q. poly p /\ poly q ==> ((- p) * q = - (p * q))``; -(* > val poly_mult_lneg = -|- !r. Ring r ==> !p q. poly p /\ poly q ==> (-p * q = -(p * q)): thm -*) (* Theorem: p * (- q) = - (p * q) *) -(* Proof: - p * (-q) - = (-q) * p by poly_mult_comm - = - (q * p) by poly_mult_lneg - = - (p * q) by poly_mult_comm -*) -val poly_mult_rneg = store_thm( - "poly_mult_rneg", - ``!r:'a ring. Ring r ==> !p q. poly p /\ poly q ==> (p * (- q) = - (p * q))``, - metis_tac[poly_mult_lneg, poly_mult_comm, poly_neg_poly]); -(* better by lifting *) +(* by lifting *) val poly_mult_rneg = lift_ring_thm_with_goal "mult_rneg" "mult_rneg" ``!r:'a ring. Ring r ==> !p q. poly p /\ poly q ==> (p * (- q) = - (p * q))``; -(* > val poly_mult_rneg = -|- !r. Ring r ==> !p q. poly p /\ poly q ==> (p * -q = -(p * q)): thm -*) val _ = export_rewrites ["poly_mult_lneg", "poly_mult_rneg"]; (* Theorem: poly p /\ poly q ==> (-(p * q) = -p * q) /\ (-(p * q) = p * -q) *) -(* Proof: - Since Ring r ==> Ring (PolyRing r) by poly_add_mult_ring - and poly p <=> p IN (PolyRing r).carrier by poly_ring_element - Hence -(p * q) = -p * q by ring_neg_mult - and -(p * q) = p * -q by ring_neg_mult -*) -val poly_neg_mult = store_thm( - "poly_neg_mult", - ``!r:'a ring. Ring r ==> !p q. poly p /\ poly q ==> (-(p * q) = -p * q) /\ (-(p * q) = p * -q)``, - metis_tac[poly_add_mult_ring, poly_ring_element, ring_neg_mult]); -(* better by lifting *) +(* by lifting *) val poly_neg_mult = lift_ring_thm_with_goal "neg_mult" "neg_mult" ``!r:'a ring. Ring r ==> !p q. poly p /\ poly q ==> (-(p * q) = -p * q) /\ (-(p * q) = p * -q)``; -(* > val poly_neg_mult = -|- !r. Ring r ==> !p q. poly p /\ poly q ==> (-(p * q) = -p * q) /\ (-(p * q) = p * -q): thm -*) (* Theorem: Ring r ==> !p q. poly p /\ poly q ==> (-p * -q = p * q) *) -(* Proof: by poly_ring_ring, ring_mult_neg_neg *) -val poly_mult_neg_neg = store_thm( - "poly_mult_neg_neg", - ``!r:'a ring. Ring r ==> !p q. poly p /\ poly q ==> (-p * -q = p * q)``, - metis_tac[poly_ring_ring, ring_mult_neg_neg, poly_ring_element]); -(* better by lifting *) +(* by lifting *) val poly_mult_neg_neg = lift_ring_thm_with_goal "mult_neg_neg" "mult_neg_neg" ``!r:'a ring. Ring r ==> !p q. poly p /\ poly q ==> (-p * -q = p * q)``; -(* > val poly_mult_neg_neg = -|- !r. Ring r ==> !p q. poly p /\ poly q ==> (-p * -q = p * q): thm -*) (* ------------------------------------------------------------------------- *) (* Theorems on polynomial distribution with subtraction. *) @@ -3769,12 +3700,8 @@ val poly_exp_add = store_thm( ``!r:'a ring. Ring r ==> !p. poly p ==> !n m. p ** (n + m) = p ** n * p ** m``, metis_tac[poly_add_mult_ring, ring_exp_add, poly_ring_property]); -(* Theorem: Ring r /\ poly p ==> !m n. (p ** (n * m) = (p ** n) ** m) *) -val poly_exp_mult = lift_ring_thm "exp_mult" "exp_mult" |> REWRITE_RULE[poly_ring_element]; -(* > val poly_exp_mult = |- !r. Ring r ==> !x. poly x ==> !n k. x ** (n * k) = (x ** n) ** k: thm *) val poly_exp_mult = lift_ring_thm_with_goal "exp_mult" "exp_mult" ``!r:'a ring. Ring r ==> !p. poly p ==> !m n. p ** (n * m) = (p ** n) ** m``; -(* > val poly_exp_mult = |- !r. Ring r ==> !p. poly p ==> !m n. p ** (n * m) = (p ** n) ** m : thm *) (* Theorem: Ring r ==> !p. poly p ==> !m n. (p ** m) ** n = (p ** n) ** m *) (* Proof: @@ -3783,11 +3710,8 @@ val poly_exp_mult = lift_ring_thm_with_goal "exp_mult" "exp_mult" = p ** (n * m) by MULT_COMM = (p ** n) ** m by poly_exp_mult *) -val poly_exp_mult_comm = lift_ring_thm "exp_mult_comm" "exp_mult_comm" |> REWRITE_RULE[poly_ring_element]; -(* > val poly_exp_mult_comm = |- !r. Ring r ==> !x. poly x ==> !m n. (x ** m) ** n = (x ** n) ** m: thm *) val poly_exp_mult_comm = lift_ring_thm_with_goal "exp_mult_comm" "exp_mult_comm" ``!r:'a ring. Ring r ==> !p. poly p ==> !m n. (p ** m) ** n = (p ** n) ** m``; -(* > val poly_exp_mult_comm = |- !r. Ring r ==> !p. poly p ==> !m n. (p ** m) ** n = (p ** n) ** m: thm *) (* Theorem: Ring r /\ poly p /\ poly q ==> !n. (p ** n) * (q ** n) = (p * q) ** n *) val poly_mult_exp = lift_ring_thm_with_goal "mult_exp" "mult_exp" @@ -5026,16 +4950,18 @@ val poly_cmult_unit_comm = store_thm( = #1 * p by ring_unit_rinv = p by poly_cmult_lone *) -val poly_cmult_unit_comm = store_thm( - "poly_cmult_unit_comm", - ``!r:'a ring p c. Ring r /\ poly p /\ c IN R /\ unit c ==> (p = (( |/c) * p) * [c])``, +Theorem poly_cmult_unit_comm[allow_rebind]: + !r:'a ring p c. Ring r /\ poly p /\ c IN R /\ unit c ==> + (p = (( |/c) * p) * [c]) +Proof rpt strip_tac >> `|/c IN R` by rw[ring_unit_inv_element] >> `(( |/c) * p) * [c] = c * (( |/c) * p)` by rw[poly_mult_rconst] >> `_ = (c * |/c) * p` by rw[poly_cmult_cmult] >> `_ = #1 * p` by rw[ring_unit_rinv] >> `_ = p` by rw[] >> - simp[]); + simp[] +QED (* Theorem: Ring r /\ poly p /\ c IN R /\ unit c ==> (p = (( |/c) * p) * [c] + |0|) *)