Skip to content

Commit

Permalink
More fixes to multiple-rebinds of theorems under same name
Browse files Browse the repository at this point in the history
  • Loading branch information
@mn200
mn200 committed Sep 21, 2023
1 parent 58d0603 commit 900bf74
Show file tree
Hide file tree
Showing 3 changed files with 51 additions and 145 deletions.
2 changes: 1 addition & 1 deletion examples/algebra/field/fieldMapScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 >>
Expand Down
50 changes: 15 additions & 35 deletions examples/algebra/field/fieldScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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:
Expand Down
144 changes: 35 additions & 109 deletions examples/algebra/polynomial/polyRingScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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. *)

Expand All @@ -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. *)

Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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. *)
Expand Down Expand Up @@ -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:
Expand All @@ -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"
Expand Down Expand Up @@ -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|) *)
Expand Down

0 comments on commit 900bf74

Please sign in to comment.