Merge branch 'develop' into fermat

HOL-Theorem-Prover · Sep 22, 2023 · 083a881 · 083a881
2 parents 2f21ab8 + cc08422
commit 083a881
Show file tree

Hide file tree

Showing 4 changed files with 65 additions and 45 deletions.
diff --git a/examples/algebra/field/fieldInstancesScript.sml b/examples/algebra/field/fieldInstancesScript.sml
@@ -637,12 +637,13 @@ Theorem ZN_finite_field[allow_rebind]:
   !p. prime p ==> FiniteField (ZN p)
 Proof
   rpt strip_tac >>
-  (REVERSE (irule finite_field_from_finite_ring >> rpt conj_tac) >> simp[ZN_property]) >-
-  metis_tac[NOT_PRIME_1, ONE_NOT_ZERO] >-
-  rw[ZN_finite_ring, PRIME_POS] >>
-  rw[EQ_IMP_THM] >-
-  metis_tac[EUCLID_LEMMA, LESS_MOD] >-
-  rw[] >>
+  (REVERSE (irule finite_field_from_finite_ring >> rpt conj_tac) >>
+   simp[ZN_property])
+  >- metis_tac[NOT_PRIME_1, ONE_NOT_ZERO]
+  >- rw[ZN_finite_ring, PRIME_POS] >>
+  rw[EQ_IMP_THM]
+  >- metis_tac[EUCLID_LEMMA, LESS_MOD]
+  >- rw[] >>
   rw[]
 QED
 

diff --git a/examples/algebra/polynomial/polyDivisionScript.sml b/examples/algebra/polynomial/polyDivisionScript.sml
@@ -969,11 +969,13 @@ val poly_mod_add_assoc = store_thm(
    = (p % z + -(q % z)) % z   by poly_mod_neg
    = (p % z - q % z) % z      by poly_sub_def
 *)
-val poly_mod_sub = store_thm(
-  "poly_mod_sub",
-  ``!r:'a ring. Ring r ==> !p q z. poly p /\ poly q /\ ulead z ==>
-         ((p - q) % z = (p % z - q % z) % z)``,
-  rw[poly_sub_def, poly_mod_add, poly_mod_neg]);
+Theorem poly_mod_sub[allow_rebind]:
+  !r:'a ring. Ring r ==>
+              !p q z. poly p /\ poly q /\ ulead z ==>
+                      ((p - q) % z = (p % z - q % z) % z)
+Proof
+  rw[poly_sub_def, poly_mod_add, poly_mod_neg]
+QED
 
 (* Theorem: (p * q) % z = (p % z * q % z) % z *)
 (* Proof:

diff --git a/examples/algebra/polynomial/polyModuloRingScript.sml b/examples/algebra/polynomial/polyModuloRingScript.sml
@@ -1276,33 +1276,52 @@ val poly_field_ideal_cogen_property = store_thm("poly_field_ideal_cogen_property
                (coset (PolyRing r).sum p (principal_ideal (PolyRing r) z).carrier)) ==> (p == q) (pm z))``,
   rw[poly_ideal_cogen_property]);
 
-val poly_field_mod_sum_group_homo_quotient_ring = store_thm("poly_field_mod_sum_group_homo_quotient_ring",
-  ``!r:'a field. Field r ==> !z. poly z /\ z <> |0| ==>
-    GroupHomo (\x. coset (PolyRing r).sum x (principal_ideal (PolyRing r) z).carrier)
-              (PolyModRing r z).sum
-              (PolyRing r / principal_ideal (PolyRing r) z).sum``,
-  rw[poly_mod_sum_group_homo_quotient_ring]);
-
-val poly_field_mod_prod_monoid_homo_quotient_ring = store_thm("poly_field_mod_prod_monoid_homo_quotient_ring",
-  ``!r:'a field. Field r ==> !z. poly z /\ z <> |0| ==>
-    MonoidHomo (\x. coset (PolyRing r).sum x (principal_ideal (PolyRing r) z).carrier)
-               (PolyModRing r z).prod
-               (PolyRing r / principal_ideal (PolyRing r) z).prod``,
-  rw[poly_mod_prod_monoid_homo_quotient_ring]);
-
-val poly_field_mod_ring_homo_quotient_ring = store_thm("poly_field_mod_ring_homo_quotient_ring",
-  ``!r:'a field. Field r ==> !z. poly z /\ z <> |0| ==>
-    RingHomo (\x. coset (PolyRing r).sum x (principal_ideal (PolyRing r) z).carrier)
-               (PolyModRing r z)
-               (quotient_ring (PolyRing r) (principal_ideal (PolyRing r) z))``,
-  rw[poly_mod_ring_homo_quotient_ring]);
-
-val poly_field_mod_ring_iso_quotient_ring = store_thm("poly_field_mod_ring_iso_quotient_ring",
-  ``!r:'a field. Field r ==> !z. poly z /\ z <> |0| ==>
-    RingIso (\x. coset (PolyRing r).sum x (principal_ideal (PolyRing r) z).carrier)
-               (PolyModRing r z)
-               (quotient_ring (PolyRing r) (principal_ideal (PolyRing r) z))``,
-  rw[poly_mod_ring_iso_quotient_ring]);
+Theorem poly_field_mod_sum_group_homo_quotient_ring:
+  !r:'a field.
+    Field r ==> !z. poly z /\ z <> |0| ==>
+    GroupHomo
+      (\x. coset (PolyRing r).sum x (principal_ideal (PolyRing r) z).carrier)
+      (PolyModRing r z).sum
+      (PolyRing r / principal_ideal (PolyRing r) z).sum
+Proof
+  rw[poly_mod_sum_group_homo_quotient_ring]
+QED
+
+Theorem poly_field_mod_prod_monoid_homo_quotient_ring:
+  !r:'a field.
+    Field r ==>
+    !z. poly z /\ z <> |0| ==>
+        MonoidHomo
+         (\x. coset (PolyRing r).sum x (principal_ideal (PolyRing r) z).carrier)
+         (PolyModRing r z).prod
+         (PolyRing r / principal_ideal (PolyRing r) z).prod
+Proof
+  rw[poly_mod_prod_monoid_homo_quotient_ring]
+QED
+
+Theorem poly_field_mod_ring_homo_quotient_ring:
+  !r:'a field.
+    Field r ==>
+    !z. poly z /\ z <> |0| ==>
+        RingHomo
+         (\x. coset (PolyRing r).sum x (principal_ideal (PolyRing r) z).carrier)
+         (PolyModRing r z)
+         (quotient_ring (PolyRing r) (principal_ideal (PolyRing r) z))
+Proof
+  rw[poly_mod_ring_homo_quotient_ring]
+QED
+
+Theorem poly_field_mod_ring_iso_quotient_ring:
+  !r:'a field.
+    Field r ==>
+    !z. poly z /\ z <> |0| ==>
+        RingIso
+         (\x. coset (PolyRing r).sum x (principal_ideal (PolyRing r) z).carrier)
+         (PolyModRing r z)
+         (quotient_ring (PolyRing r) (principal_ideal (PolyRing r) z))
+Proof
+  rw[poly_mod_ring_iso_quotient_ring]
+QED
 
 val poly_field_mod_exp_alt = store_thm("poly_field_mod_exp_alt",
   ``!r:'a field. Field r ==> !p z. poly p /\ poly z /\ z <> |0| ==>

diff --git a/examples/algebra/polynomial/polyMonicScript.sml b/examples/algebra/polynomial/polyMonicScript.sml
@@ -942,13 +942,11 @@ val poly_deg_X = store_thm(
   = lead |1|          by poly_lead_shift
   = #1                by poly_lead_one
 *)
-val poly_lead_X = store_thm(
-  "poly_lead_X",
-  ``!r:'a ring. Ring r ==> (lead X = #1)``,
-  rw_tac std_ss[poly_lead_shift, poly_lead_one]);
-
-(* export simple result *)
-val _ = export_rewrites ["poly_lead_X"];
+Theorem poly_lead_X[simp]:
+  !r:'a ring. Ring r ==> (lead X = #1)
+Proof
+  rw_tac std_ss[poly_lead_shift, poly_lead_one]
+QED
 
 (* Theorem: monic X *)
 (* Proof: