More fixes to multiple-rebinds of theorems under same name

HOL-Theorem-Prover · Sep 14, 2023 · b404802 · b404802
1 parent 0f1309e
commit b404802
Show file tree

Hide file tree

Showing 11 changed files with 148 additions and 313 deletions.
diff --git a/examples/algebra/group/corresScript.sml b/examples/algebra/group/corresScript.sml
@@ -157,22 +157,13 @@ val _ = ParseExtras.tight_equality();
      <=>  x IN s iff x IN s                                                  FOL
      <=>  T                                                                  FOL
 *)
-val SURJ_IMAGE_PREIMAGE = store_thm(
-  "SURJ_IMAGE_PREIMAGE",
-  ``!f a b s. s SUBSET b /\ SURJ f a b ==> (IMAGE f (PREIMAGE f s INTER a) = s)``,
-  rpt strip_tac >>
-  simp[EXTENSION, PREIMAGE_def] >>
-  strip_tac >>
-  fs[SURJ_DEF] >>
-  eq_tac >-
-  metis_tac[] >>
-  metis_tac[SUBSET_DEF]);
-(* original *)
-val SURJ_IMAGE_PREIMAGE = store_thm(
-    "SURJ_IMAGE_PREIMAGE",
-    ``!f a b. s SUBSET b /\  SURJ f a b ==> (IMAGE f(PREIMAGE f s INTER a) = s)``,
-    rpt strip_tac >> simp[EXTENSION, PREIMAGE_def] >> strip_tac >> fs[SURJ_DEF] >>
-    eq_tac >> rpt strip_tac >> metis_tac[SUBSET_DEF]);
+
+Theorem SURJ_IMAGE_PREIMAGE:
+  !f a b. s SUBSET b /\  SURJ f a b ==> (IMAGE f(PREIMAGE f s INTER a) = s)
+Proof
+  rpt strip_tac >> simp[EXTENSION, PREIMAGE_def] >> strip_tac >> fs[SURJ_DEF] >>
+  eq_tac >> rpt strip_tac >> metis_tac[SUBSET_DEF]
+QED
 
 (* Add some facts about cardinal arithmetic of groups. *)
 
@@ -337,22 +328,15 @@ val preimage_group_group = store_thm(
         SUBSET g1.carrier, true                              by preimage_group_def
    (3) (preimage_group f g1 g2 h.carrier).op = g1.op, true   by preimage_group_def
 *)
-val preimage_subgroup_subgroup = store_thm(
-  "preimage_subgroup_subgroup",
-  ``!f g1:'a group g2:'b group h. Group g1 /\ Group g2 /\ GroupHomo f g1 g2 /\ h <= g2 ==>
-            preimage_group f g1 g2 h.carrier <= g1``,
-  rpt strip_tac >>
-  simp[Subgroup_def] >>
-  rpt strip_tac >-
-  metis_tac[preimage_group_group] >-
-  rw[preimage_group_def] >>
-  rw[preimage_group_def]);
-val preimage_subgroup_subgroup = store_thm(
-    "preimage_subgroup_subgroup",
-    ``!f g1:'a group g2:'b group h. Group g1 /\ Group g2 /\ GroupHomo f g1 g2 /\ h <= g2 ==>
-               preimage_group f g1 g2 h.carrier <= g1``,
-    rpt strip_tac >> simp[Subgroup_def] >> rpt strip_tac >- metis_tac[preimage_group_group] >>
-    rw[preimage_group_def]);
+Theorem preimage_subgroup_subgroup:
+  !f g1:'a group g2:'b group h.
+    Group g1 /\ Group g2 /\ GroupHomo f g1 g2 /\ h <= g2 ==>
+    preimage_group f g1 g2 h.carrier <= g1
+Proof
+  rpt strip_tac >> simp[Subgroup_def] >> rpt strip_tac
+  >- metis_tac[preimage_group_group] >>
+  rw[preimage_group_def]
+QED
 
 (* This is Lemma 2 *)
 
@@ -595,31 +579,19 @@ val preimage_image_subset = store_thm(
        (2) h1.carrier SUBSET PREIMAGE f (IMAGE f h1.carrier) INTER g1.carrier
            This is true                   by subset_preimage_image
 *)
-val bij_corres = store_thm(
-  "bij_corres",
-  ``!f g1:'a group g2 h1 h2.
-         Group g1 /\ Group g2 /\ h1 <= g1 /\ h2 <= g2 /\ GroupHomo f g1 g2 /\
-            SURJ f g1.carrier g2.carrier /\ kernel f g1 g2 SUBSET h1.carrier ==>
-            IMAGE f (PREIMAGE f h2.carrier INTER g1.carrier) = h2.carrier /\
-            PREIMAGE f (IMAGE f h1.carrier) INTER g1.carrier = h1.carrier``,
-  rpt strip_tac >-
-  metis_tac[image_preimage_group] >>
-  (irule SUBSET_ANTISYM >> rpt conj_tac) >-
-  metis_tac[preimage_image_subset] >>
-  metis_tac[subset_preimage_image]);
-(* original *)
-val bij_corres = store_thm(
-    "bij_corres",
-    ``!f g1:'a group g2 h1 h2. Group g1 /\ Group g2 /\ h1 <= g1 /\ h2 <= g2 /\
-         GroupHomo f g1 g2 /\ SURJ f g1.carrier g2.carrier /\ kernel f g1 g2 SUBSET h1.carrier ==>
-            IMAGE f (PREIMAGE f h2.carrier INTER g1.carrier) = h2.carrier /\
-            PREIMAGE f (IMAGE f h1.carrier) INTER g1.carrier = h1.carrier``,
-    rpt strip_tac >- metis_tac[image_preimage_group] >>
-    `PREIMAGE f (IMAGE f h1.carrier) INTER g1.carrier SUBSET h1.carrier /\
-     h1.carrier SUBSET PREIMAGE f (IMAGE f h1.carrier) INTER g1.carrier` suffices_by metis_tac[SET_EQ_SUBSET] >>
-    strip_tac >-
-    metis_tac[preimage_image_subset] >-
-    metis_tac[subset_preimage_image]);
+Theorem bij_corres:
+  !f g1:'a group g2 h1 h2.
+    Group g1 /\ Group g2 /\ h1 <= g1 /\ h2 <= g2 /\ GroupHomo f g1 g2 /\
+    SURJ f g1.carrier g2.carrier /\ kernel f g1 g2 SUBSET h1.carrier ==>
+    IMAGE f (PREIMAGE f h2.carrier INTER g1.carrier) = h2.carrier /\
+    PREIMAGE f (IMAGE f h1.carrier) INTER g1.carrier = h1.carrier
+Proof
+  rpt strip_tac
+  >- metis_tac[image_preimage_group] >>
+  irule SUBSET_ANTISYM >> rpt conj_tac
+  >- metis_tac[preimage_image_subset] >>
+  metis_tac[subset_preimage_image]
+QED
 
 (* This is Lemma 5 *)
 
@@ -710,26 +682,18 @@ val image_iso_preimage_quotient = store_thm(
     ==> FINITE (IMAGE f (preimage_group f g1 g2 h.carrier).carrier)          by IMAGE_FINITE
       = FINITE (homo_image f (preimage_group f g1 g2 h.carrier) g2).carrier  by homo_image_def
 *)
-val finite_homo_image = store_thm(
-  "finite_homo_image",
-  ``!f g1:'a group g2 h.FiniteGroup g1 /\ Group g2 /\ h <= g2 /\ GroupHomo f g1 g2 ==>
-          FINITE (homo_image f (preimage_group f g1 g2 h.carrier) g2).carrier``,
+Theorem finite_homo_image:
+  !f g1:'a group g2 h.
+    FiniteGroup g1 /\ Group g2 /\ h <= g2 /\ GroupHomo f g1 g2 ==>
+    FINITE (homo_image f (preimage_group f g1 g2 h.carrier) g2).carrier
+Proof
   rpt strip_tac >>
   fs[homo_image_def] >>
   irule IMAGE_FINITE >>
   fs[preimage_group_def] >>
   irule FINITE_INTER >>
-  metis_tac[FiniteGroup_def]);
-(* original *)
-val finite_homo_image = store_thm(
-    "finite_homo_image",
-    ``!f g1:'a group g2 h.FiniteGroup g1 /\ Group g2 /\ h <= g2 /\ GroupHomo f g1 g2 ==> FINITE (homo_image f (preimage_group f g1 g2 h.carrier) g2).carrier``,
-    rpt strip_tac >> fs[homo_image_def] >>
-    `FINITE (preimage_group f g1 g2 h.carrier).carrier` suffices_by fs[IMAGE_FINITE] >>
-    fs[preimage_group_def] >>
-    `(PREIMAGE f h.carrier ∩ g1.carrier) SUBSET g1.carrier` by fs[INTER_SUBSET] >>
-    `FINITE g1.carrier` by metis_tac[FiniteGroup_def] >>
-    metis_tac[SUBSET_FINITE]);
+  metis_tac[FiniteGroup_def]
+QED
 
 (* Theorem: FiniteGroup g1 /\ Group g2 /\ h <= g2 /\ GroupHomo f g1 g2 ==>
     CARD (homo_image f (preimage_group f g1 g2 h.carrier) g2).carrier =
@@ -744,32 +708,20 @@ val finite_homo_image = store_thm(
    Note FINITE t1.carrier                    by finite_homo_image, FiniteGroup g1
    Thus CARD t1.carrier = CARD t2.carrier    by iso_group_same_card
 *)
-val image_preimage_quotient_same_card = store_thm(
-  "image_preimage_quotient_same_card",
-  ``!f g1:'a group g2 h.FiniteGroup g1 /\ Group g2 /\ h <= g2 /\ GroupHomo f g1 g2 ==>
+Theorem image_preimage_quotient_same_card:
+  !f g1:'a group g2 h.
+    FiniteGroup g1 /\ Group g2 /\ h <= g2 /\ GroupHomo f g1 g2 ==>
     CARD (homo_image f (preimage_group f g1 g2 h.carrier) g2).carrier =
-    CARD (preimage_group f g1 g2 h.carrier / kernel_group f (preimage_group f g1 g2 h.carrier) g2).carrier``,
+    CARD
+      (preimage_group f g1 g2 h.carrier /
+       kernel_group f (preimage_group f g1 g2 h.carrier) g2).carrier
+Proof
   rpt strip_tac >>
   `Group g1` by metis_tac[finite_group_is_group] >>
   imp_res_tac image_iso_preimage_quotient >>
   `FINITE (homo_image f (preimage_group f g1 g2 h.carrier) g2).carrier` by metis_tac[finite_homo_image] >>
-  metis_tac[iso_group_same_card]);
-(* original *)
-val image_preimage_quotient_same_card = store_thm(
-    "image_preimage_quotient_same_card",
-    ``!f g1:'a group g2 h.FiniteGroup g1 /\ Group g2 /\ h <= g2 /\ GroupHomo f g1 g2 ==>
-    CARD (homo_image f (preimage_group f g1 g2 h.carrier) g2).carrier =
-    CARD (preimage_group f g1 g2 h.carrier / kernel_group f (preimage_group f g1 g2 h.carrier) g2).carrier``,
-    rpt strip_tac >> `Group g1` by metis_tac[finite_group_is_group] >>
-    ` GroupIso
-         (\z. coset (preimage_group f g1 g2 h.carrier)
-                    (CHOICE (preimage f (preimage_group f g1 g2 h.carrier).carrier z))
-                    (kernel f (preimage_group f g1 g2 h.carrier) g2))
-         (homo_image f (preimage_group f g1 g2 h.carrier) g2)
-         (preimage_group f g1 g2 h.carrier /
-          kernel_group f (preimage_group f g1 g2 h.carrier) g2)` by metis_tac[image_iso_preimage_quotient] >>
-    `FINITE (homo_image f (preimage_group f g1 g2 h.carrier) g2).carrier` by metis_tac[finite_homo_image] >>
-    metis_tac[iso_group_same_card]);
+  metis_tac[iso_group_same_card]
+QED
 
 (* Theorem: H SUBSET g1.carrier /\
             GroupHomo f g1 g2 /\ (kernel f g1 g2) SUBSET H ==> kernel f g1 g2 = kernel f h g2 *)

diff --git a/examples/algebra/group/finiteGroupScript.sml b/examples/algebra/group/finiteGroupScript.sml
@@ -943,11 +943,11 @@ val subgroup_cross_card_eqn = store_thm(
     = CARD (s1 o s2) * CARD (s1 INTER s2)              by MULT_COMM
     = CARD (h1 o h2).carrier * CARD (s1 INTER s2)      by subgroup_cross_property
 *)
-val subgroup_cross_card_eqn = store_thm(
-  "subgroup_cross_card_eqn",
-  ``!(g h1 h2):'a group. h1 <= g /\ h2 <= g /\ FINITE G ==>
+Theorem subgroup_cross_card_eqn[allow_rebind]:
+  !(g h1 h2):'a group. h1 <= g /\ h2 <= g /\ FINITE G ==>
    let (s1 = h1.carrier) in let (s2 = h2.carrier) in
-    (CARD (h1 o h2).carrier * CARD (s1 INTER s2) = (CARD s1) * (CARD s2))``,
+    (CARD (h1 o h2).carrier * CARD (s1 INTER s2) = (CARD s1) * (CARD s2))
+Proof
   rw_tac std_ss[] >>
   qabbrev_tac `s = s1 CROSS s2` >>
   `FINITE s1 /\ FINITE s2` by metis_tac[subgroup_carrier_subset, SUBSET_FINITE] >>
@@ -963,7 +963,8 @@ val subgroup_cross_card_eqn = store_thm(
   `_ = SIGMA (CARD o t) (s1 o s2)` by metis_tac[SUM_IMAGE_INJ_o, subset_cross_preimage_inj] >>
   `_ = SIGMA (\z. CARD (s1 INTER s2)) (s1 o s2)` by rw[SUM_IMAGE_CONG] >>
   `_ = CARD (s1 INTER s2) * CARD (s1 o s2)` by rw[SIGMA_CONSTANT] >>
-  rw[subgroup_cross_property]);
+  rw[subgroup_cross_property]
+QED
 
 (* Theorem: h1 <= g /\ h2 <= g /\ FINITE G ==>
             let (s1 = h1.carrier) in let (s2 = h2.carrier) in

diff --git a/examples/algebra/group/groupCyclicScript.sml b/examples/algebra/group/groupCyclicScript.sml
@@ -1622,17 +1622,20 @@ val finite_cyclic_group_add_mod_iso = store_thm(
                                                       by group_iso_sym
      or ?f. GroupIso f g1 g2                          by group_iso_trans
 *)
-val finite_cyclic_group_uniqueness = store_thm(
-  "finite_cyclic_group_uniqueness",
-  ``!g1:'a group g2:'b group. cyclic g1 /\ cyclic g2 /\ FINITE g1.carrier /\ FINITE g2.carrier /\
-        (CARD g1.carrier = CARD g2.carrier) ==> ?f. GroupIso f g1 g2``,
+Theorem finite_cyclic_group_uniqueness[allow_rebind]:
+  !g1:'a group g2:'b group.
+    cyclic g1 /\ cyclic g2 /\ FINITE g1.carrier /\ FINITE g2.carrier /\
+    (CARD g1.carrier = CARD g2.carrier) ==>
+    ?f. GroupIso f g1 g2
+Proof
   rpt strip_tac >>
-  `Group g1 /\ FiniteGroup g1` by rw[cyclic_group, FiniteGroup_def] >>
-  `0 < CARD g1.carrier` by rw[finite_group_card_pos] >>
-  `Group (add_mod (CARD g1.carrier))` by rw[add_mod_group] >>
-  `GroupIso (\n. g1.exp (cyclic_gen g1) n) (add_mod (CARD g1.carrier)) g1` by rw[finite_cyclic_group_add_mod_iso] >>
-  `GroupIso (\n. g2.exp (cyclic_gen g2) n) (add_mod (CARD g2.carrier)) g2` by rw[finite_cyclic_group_add_mod_iso] >>
-  metis_tac[group_iso_sym, group_iso_trans]);
+  ‘Group g1 /\ FiniteGroup g1’ by rw[cyclic_group, FiniteGroup_def] >>
+  ‘0 < CARD g1.carrier’ by rw[finite_group_card_pos] >>
+  ‘Group (add_mod (CARD g1.carrier))’ by rw[add_mod_group] >>
+  ‘GroupIso (\n. g1.exp (cyclic_gen g1) n) (add_mod (CARD g1.carrier)) g1’ by rw[finite_cyclic_group_add_mod_iso] >>
+  ‘GroupIso (\n. g2.exp (cyclic_gen g2) n) (add_mod (CARD g2.carrier)) g2’ by rw[finite_cyclic_group_add_mod_iso] >>
+  metis_tac[group_iso_sym, group_iso_trans]
+QED
 
 (* ------------------------------------------------------------------------- *)
 (* Isomorphism between Cyclic Groups                                         *)

diff --git a/examples/algebra/group/groupOrderScript.sml b/examples/algebra/group/groupOrderScript.sml
@@ -190,11 +190,6 @@ val finite_group_exp_not_distinct = store_thm(
   "finite_group_exp_not_distinct",
   ``!g:'a group. FiniteGroup g ==> !x. x IN G ==> ?h k. (x ** h = x ** k) /\ h <> k``,
   rw[finite_monoid_exp_not_distinct, finite_group_is_finite_monoid]);
-(* using theorem transform *)
-val finite_group_exp_not_distinct = save_thm("finite_group_exp_not_distinct",
-   finite_group_is_finite_monoid |> SPEC_ALL |> UNDISCH
-   |> MP (finite_monoid_exp_not_distinct |> SPEC_ALL) |> DISCH_ALL |> GEN_ALL);
-(* > val finite_group_exp_not_distinct = |- !g. FiniteGroup g ==> !x. x IN G ==> ?h k. (x ** h = x ** k) /\ h <> k : thm *)
 
 (* Theorem: For FINITE Group g and x IN G, there is k > 0 such that x ** k = #e. *)
 (* Proof:
@@ -1103,10 +1098,11 @@ val group_uroots_subgroup = store_thm(
 
 (* Theorem: AbelianGroup g ==> !n. Group (uroots n) *)
 (* Proof: by group_uroots_subgroup, Subgroup_def *)
-val group_uroots_group = store_thm(
-  "group_uroots_group",
-  ``!g:'a group. AbelianGroup g ==> !n. Group (uroots n)``,
-  metis_tac[group_uroots_subgroup, Subgroup_def]);
+Theorem group_uroots_group:
+  !g:'a group. AbelianGroup g ==> !n. Group (uroots n)
+Proof
+  metis_tac[group_uroots_subgroup, Subgroup_def]
+QED
 
 (* Is this true: Group g ==> !n. Group (uroots n) *)
 (* No? *)
@@ -1128,14 +1124,16 @@ val group_uroots_group = store_thm(
        Thus ( |/ x) ** n = #e   by group_order_divides_exp
        Take y = |/ x, then true by group_linv
 *)
-val group_uroots_group = store_thm(
-  "group_uroots_group",
-  ``!g:'a group. AbelianGroup g ==> !n. Group (uroots n)``,
+Theorem group_uroots_group[allow_rebind]:
+  !g:'a group. AbelianGroup g ==> !n. Group (uroots n)
+Proof
   rw[AbelianGroup_def] >>
-  rw[roots_of_unity_def, group_def_alt] >-
-  rw[group_comm_op_exp] >-
-  metis_tac[group_assoc] >>
-  metis_tac[group_order_divides_exp, group_inv_order, group_linv, group_inv_element]);
+  rw[roots_of_unity_def, group_def_alt]
+  >- rw[group_comm_op_exp]
+  >- metis_tac[group_assoc] >>
+  metis_tac[group_order_divides_exp, group_inv_order, group_linv,
+            group_inv_element]
+QED
 
 (* ------------------------------------------------------------------------- *)
 (* Subgroup generated by a subset of a Group.                                *)

diff --git a/examples/algebra/group/groupScript.sml b/examples/algebra/group/groupScript.sml
@@ -458,27 +458,21 @@ val group_exp_mult = lift_monoid_thm "exp_mult";
 
 (* Theorem: [Group inverse element] |/ x IN G *)
 (* Proof: by Group_def and monoid_inv_def. *)
-val group_inv_element = store_thm(
-  "group_inv_element",
-  ``!g:'a group. Group g ==> !x. x IN G ==> |/x IN G``,
-  rw[monoid_inv_def]);
+Theorem group_inv_element[simp]:
+  !g:'a group. Group g ==> !x. x IN G ==> |/x IN G
+Proof rw[monoid_inv_def]
+QED
 (* Below is too much effort for a simple theorem. *)
 
 
 val gim = Group_def |> SPEC_ALL |> #1 o EQ_IMP_RULE |> UNDISCH_ALL |> CONJUNCT1;
 val ginv = Group_def |> SPEC_ALL |> #1 o EQ_IMP_RULE |> UNDISCH_ALL |> CONJUNCT2;
 
-(* Theorem: Group inverse is an element. *)
-val group_inv_element = save_thm("group_inv_element",
-  monoid_inv_def |> SPEC_ALL |> REWRITE_RULE [gim, ginv] |> SPEC_ALL |> UNDISCH_ALL
-                 |> CONJUNCT1 |> DISCH ``x IN G`` |> GEN ``x`` |> DISCH ``Group g`` |> GEN_ALL);
-(* > val group_inv_element = |- !g. Group g ==> !x. x IN G ==> |/ x IN G : thm *)
-
 (* Theorem: [Group left inverse] |/ x * x = #e *)
 (* Proof: by Group_def and monoid_inv_def. *)
-val group_linv = save_thm("group_linv",
+Theorem group_linv[simp] =
   monoid_inv_def |> SPEC_ALL |> REWRITE_RULE [gim, ginv] |> SPEC_ALL |> UNDISCH_ALL
-                 |> CONJUNCT2 |> CONJUNCT2 |> DISCH ``x IN G`` |> GEN ``x`` |> DISCH ``Group g`` |> GEN_ALL);
+                 |> CONJUNCT2 |> CONJUNCT2 |> DISCH ``x IN G`` |> GEN ``x`` |> DISCH ``Group g`` |> GEN_ALL
 (* > val group_linv = |- !g. Group g ==> !x. x IN G ==> ( |/ x * x = #e) : thm *)
 
 (* Theorem: [Group right inverse] x * |/ x = #e *)
@@ -1116,16 +1110,17 @@ val group_including_excluding_eqn = store_thm(
     metis_tac[]
   ]);
 (* better -- Michael's solution *)
-val group_including_excluding_eqn = store_thm(
-  "group_including_excluding_eqn",
-  ``!g:'a group. !z:'a. g including z excluding z =
-      if z IN G then <| carrier := G DELETE z;
-                             op := g.op;
-                             id := g.id |>
-      else g``,
+Theorem group_including_excluding_eqn[allow_rebind]:
+  !g:'a group. !z:'a. g including z excluding z =
+                      if z IN G then <| carrier := G DELETE z;
+                                        op := g.op;
+                                        id := g.id |>
+                      else g
+Proof
   rw[including_def, excluding_def] >>
   rw[monoid_component_equality] >>
-  rw[EXTENSION] >> metis_tac[]);
+  rw[EXTENSION] >> metis_tac[]
+QED
 
 (* Theorem: (g excluding z).op = g.op *)
 (* Proof: by definition. *)