More fixes to multiple-rebinds of theorems under same name

HOL-Theorem-Prover · Sep 22, 2023 · cc08422 · cc08422
1 parent 900bf74
commit cc08422
Show file tree

Hide file tree

Showing 4 changed files with 70 additions and 67 deletions.
diff --git a/examples/algebra/field/fieldInstancesScript.sml b/examples/algebra/field/fieldInstancesScript.sml
@@ -633,17 +633,19 @@ val ZN_finite_field = store_thm(
           Note 0 < p /\ 0 * y = 0 ==> 0 MOD p = 0   by MULT, ZERO_MOD
            and 0 < p /\ x * 0 = 0 ==> 0 MOD p = 0   by MULT_0, ZERO_MOD
 *)
-val ZN_finite_field = store_thm(
-  "ZN_finite_field",
-  ``!p. prime p ==> FiniteField (ZN p)``,
+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[] >>
-  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
 
 (* Theorem: prime p <=> FiniteField (ZN p) *)
 (* Proof:

diff --git a/examples/algebra/polynomial/polyDivisionScript.sml b/examples/algebra/polynomial/polyDivisionScript.sml
@@ -986,11 +986,13 @@ val poly_mod_sub = 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,40 +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_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_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_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_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_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
@@ -935,31 +935,18 @@ val poly_deg_X = store_thm(
   ``!r:'a ring. Ring r /\ #1 <> #0 ==> (deg X = 1)``,
   rw[]);
 
-(* Theorem: lead X = #1 *)
-(* Proof: by poly_X_def. *)
-val poly_lead_X = store_thm(
-  "poly_lead_X",
-  ``!r:'a ring. Ring r /\ #1 <> #0 ==> (lead X = #1)``,
-  rw[]);
-
-(* better than: above poly_lead_X
-   |- !r. Ring r /\ #1 <> #0 ==> (lead X = #1)
-*)
-
 (* Theorem: lead X = #1 *)
 (* Proof:
     lead X
   = lead ( |1| >> 1)   by notation
   = 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: