Skip to content

Commit

Permalink
Merge branch 'develop' into fermat
Browse files Browse the repository at this point in the history
  • Loading branch information
@jhlchan
jhlchan authored Sep 21, 2023
2 parents 2bffa77 + 900bf74 commit 2f21ab8
Show file tree
Hide file tree
Showing 2 changed files with 39 additions and 51 deletions.
32 changes: 15 additions & 17 deletions examples/algebra/field/fieldScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1908,26 +1908,24 @@ val _ = export_rewrites ["field_inv_mult"];

(* 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
58 changes: 24 additions & 34 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,22 +1121,22 @@ 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]);
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

val _ = export_rewrites ["poly_mult_lone", "poly_mult_rone"];
(* 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 *)

(* Theorem: |1| * p = p and p * |1| = p *)
(* Proof: combine poly_mult_lone and poly_mult_rone. *)

(* 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[]);
Theorem poly_mult_one:
!r:'a ring. Ring r ==> !p. poly p ==> ( |1| * p = p) /\ (p * |1| = p)
Proof rw[]
QED

(* To show closure for Monoid (PolyRing r).prod. *)

Expand Down Expand Up @@ -2569,9 +2571,6 @@ val poly_mult_cmult = store_thm(
(* better 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:
Expand All @@ -2583,9 +2582,6 @@ val poly_mult_lneg = lift_ring_thm_with_goal "mult_lneg" "mult_lneg"
(* better 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"];

Expand All @@ -2599,18 +2595,12 @@ val _ = export_rewrites ["poly_mult_lneg", "poly_mult_rneg"];
(* better 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 *)
(* better 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 @@ -3741,7 +3731,6 @@ val poly_exp_add = store_thm(
(* Theorem: Ring r /\ poly p ==> !m n. (p ** (n * m) = (p ** n) ** m) *)
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 @@ -3752,7 +3741,6 @@ val poly_exp_mult = lift_ring_thm_with_goal "exp_mult" "exp_mult"
*)
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 @@ -4961,16 +4949,18 @@ val poly_cmult_unit = 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 2f21ab8

Please sign in to comment.