Forbid "rebinds" of exported theorems

This is not enforced interactively of course, when users will be
replaying definitions and proofs constantly. The [allow_rebind]
annotation can be used when the rebind is actually wanted, but as all
the fixups in this commit demonstrate, this change catches a great
number of errors.

Resolving all the errors is still ongoing.

examples/algebra/lib/helperNumScript.sml

@@ -1955,7 +1955,7 @@ val EXP_ODD = store_thm(
   rw[]);
 
 (* An exponentiation identity *)
-val EXP_THM = save_thm("EXP_THM", CONJ EXP_EVEN EXP_ODD);
+(* val EXP_THM = save_thm("EXP_THM", CONJ EXP_EVEN EXP_ODD); *)
 (*
 val EXP_THM = |- (!n. EVEN n ==> !m. m ** n = SQ m ** HALF n) /\
                   !n. ODD n ==> !m. m ** n = m * SQ m ** HALF n: thm
@@ -1965,11 +1965,13 @@ val EXP_THM = |- (!n. EVEN n ==> !m. m ** n = SQ m ** HALF n) /\
 (* Theorem: m ** n = if n = 0 then 1 else if n = 1 then m else
             if EVEN n then (m * m) ** HALF n else m * ((m * m) ** (HALF n)) *)
 (* Proof: mainly by EXP_EVEN, EXP_ODD. *)
-val EXP_THM = store_thm(
-  "EXP_THM",
-  ``!m n. m ** n = if n = 0 then 1 else if n = 1 then m else
-      if EVEN n then (m * m) ** HALF n else m * ((m * m) ** (HALF n))``,
-  metis_tac[EXP_0, EXP_1, EXP_EVEN, EXP_ODD, EVEN_ODD]);
+Theorem EXP_THM:
+  !m n. m ** n = if n = 0 then 1 else if n = 1 then m
+                 else if EVEN n then (m * m) ** HALF n
+                 else m * ((m * m) ** (HALF n))
+Proof
+  metis_tac[EXP_0, EXP_1, EXP_EVEN, EXP_ODD, EVEN_ODD]
+QED
 
 (* Theorem: m ** n =
             if n = 0 then 1
@@ -3662,15 +3664,15 @@ val power_parity = store_thm(
    <=> 0 = 0                       by ZERO_MOD
    <=> T
 *)
-val EXP_2_EVEN = store_thm(
-  "EXP_2_EVEN",
-  ``!n. 0 < n ==> EVEN (2 ** n)``,
-  rw[EVEN_MOD2, ZERO_EXP]);
-(* Michael's proof by induction *)
+Theorem EXP_2_EVEN:  !n. 0 < n ==> EVEN (2 ** n)
+Proof rw[EVEN_MOD2, ZERO_EXP]
+QED
+(* Michael's proof by induction
 val EXP_2_EVEN = store_thm(
   "EXP_2_EVEN",
   ``!n. 0 < n ==> EVEN (2 ** n)``,
   Induct >> rw[EXP, EVEN_DOUBLE]);
+ *)
 
 (* Theorem: 0 < n ==> ODD (2 ** n - 1) *)
 (* Proof:
@@ -4618,40 +4620,11 @@ val ONE_LT_HALF_SQ = store_thm(
   `(2 ** 2) DIV 2 = 2` by EVAL_TAC >>
   decide_tac);
 
-(* Theorem: 0 < n ==> (HALF (2 ** n) = 2 ** (n - 1)) *)
-(* Proof:
-   Since 2 ** n = (2 ** n) DIV 2 * 2 + (2 ** n) MOD 2   by DIVISION
-   But  (2 ** n) MOD 2
-      = ((2 MOD 2) ** n) MOD 2     by EXP_MOD
-      = (0 ** n) MOD 2             by DIVMOD_ID
-      = 0 MOD 2                    by ZERO_EXP, n <> 0
-      = 0                          by ZERO_MOD, 0 < n
-   Now  2 ** n
-      = 2 ** SUC (n - 1)
-      = 2 * 2 ** (n - 1)                by EXP
-      = 2 * (2 ** n DIV 2)              by MULT_COMM, above
-   Hence 2 ** (n - 1) = (2 ** n) DIV 2  by MULT_LEFT_CANCEL
-*)
-val EXP_2_HALF = store_thm(
-  "EXP_2_HALF",
-  ``!n. 0 < n ==> (HALF (2 ** n) = 2 ** (n - 1))``,
-  rpt strip_tac >>
-  `2 ** n = (2 ** n) DIV 2 * 2 + (2 ** n) MOD 2` by rw[DIVISION] >>
-  `(2 ** n) MOD 2 = ((2 MOD 2) ** n) MOD 2` by rw[] >>
-  `2 MOD 2 = 0` by rw[] >>
-  `n <> 0` by decide_tac >>
-  `0 ** n = 0` by rw[] >>
-  `(2 ** n) MOD 2 = 0` by rw[] >>
-  `2 ** n = 2 ** n DIV 2 * 2` by decide_tac >>
-  `n = SUC (n - 1)` by decide_tac >>
-  `2 * 2 ** (n - 1) = 2 * (2 ** n DIV 2)` by metis_tac[EXP, MULT_COMM] >>
-  decide_tac);
-(* Michael's proof by induction *)
-val EXP_2_HALF = store_thm(
-  "EXP_2_HALF",
-  ``!n. 0 < n ==> (HALF (2 ** n) = 2 ** (n - 1))``,
-  Induct >>
-  simp[EXP, MULT_TO_DIV]);
+Theorem EXP_2_HALF:
+  !n. 0 < n ==> (HALF (2 ** n) = 2 ** (n - 1))
+Proof
+  Induct >> simp[EXP, MULT_TO_DIV]
+QED
 
 (*
 There is EVEN_MULT    |- !m n. EVEN (m * n) <=> EVEN m \/ EVEN n

examples/formal-languages/context-free/grammarScript.sml

@@ -68,7 +68,7 @@ Termination
    WF_REL_TAC `measure ptree_size`
 End
 
-Theorem ptree_fringe_def[simp,compute] =
+Theorem ptree_fringe_def[simp,compute,allow_rebind] =
   CONV_RULE (DEPTH_CONV ETA_CONV) ptree_fringe_def
 
 Definition complete_ptree_def:

examples/formal-languages/context-free/pegScript.sml

@@ -571,7 +571,8 @@ Theorem peg_eval_tok_SOME:
 Proof simp[Once peg_eval_cases, pairTheory.EXISTS_PROD] >> metis_tac[]
 QED
 
-Theorem peg_eval_empty[simp]: peg_eval G (i, empty r) x ⇔ x = Success i r NONE
+Theorem peg_eval_empty[simp,allow_rebind]:
+  peg_eval G (i, empty r) x ⇔ x = Success i r NONE
 Proof simp[Once peg_eval_cases]
 QED
 
@@ -625,7 +626,7 @@ Proof
   metis_tac[]
 QED
 
-Theorem peg_eval_rpt:
+Theorem peg_eval_rpt[allow_rebind]:
   peg_eval G (i0, rpt s f) x ⇔
     ∃i l err. peg_eval_list G (i0,s) (i,l,err) ∧ x = Success i (f l) (SOME err)
 Proof simp[Once peg_eval_cases, SimpLHS] >> metis_tac[]

examples/formal-languages/context-free/simpleSexpScript.sml

@@ -99,7 +99,7 @@ val sxMEM_def = Define`
   sxMEM e s ⇔ ∃l. strip_sxcons s = SOME l ∧ MEM e l
 `;
 
-Theorem sexp_size_def[simp] = definition"sexp_size_def";
+Theorem sexp_size_def[simp,allow_rebind] = definition"sexp_size_def";
 
 Theorem sxMEM_sizelt:
   ∀s1 s2. sxMEM s1 s2 ⇒ sexp_size s1 < sexp_size s2

examples/lambda/basics/generic_termsScript.sml

@@ -577,9 +577,7 @@ val gtpm_raw = store_thm(
   ``gtpm = raw_gtpm``,
   srw_tac [][GSYM pmact_bijections,is_pmact_def,is_pmact_raw_gtpm]);
 
-val gtpm_thm = save_thm(
-"gtpm_thm",
-raw_gtpm_thm |> SUBS [GSYM gtpm_raw]);
+Theorem gtpm_thm = raw_gtpm_thm |> SUBS [GSYM gtpm_raw]
 
 val GFV_support = prove(
   ``support gt_pmact t (GFV t)``,
@@ -632,7 +630,7 @@ val gtmsize_gtpm = CONJ (SUBS [GSYM gtpm_raw] gtmsize_raw_gtpm) (GEN_ALL gtmsize
    working with this type *)
 val GFV_thm = save_thm("GFV_thm", rmGFV GFV_thm0)
 val GFV_gtpm = save_thm("GFV_gtpm", rmGFV (SUBS [GSYM gtpm_raw] GFV_raw_gtpm))
-val gtpm_thm = save_thm("gtpm_thm", REWRITE_RULE [MAP_gtpm] gtpm_thm)
+Theorem gtpm_thm[allow_rebind] = REWRITE_RULE [MAP_gtpm] gtpm_thm
 val gterm_distinct = save_thm("gterm_distinct", gterm_distinct)
 val gterm_11 = save_thm("gterm_11", gterm_11)
 val GLAM_eq_thm = save_thm("GLAM_eq_thm", rmGFV GLAM_eq_thm1)

examples/miller/formalize/extra_boolScript.sml

@@ -43,15 +43,13 @@ val xor_assoc = store_thm
    ``!x y z. (x xor y) xor z <=> x xor (y xor z)``,
    RW_TAC bool_ss [xor_def] THEN DECIDE_TAC);
 
-val xor_F = store_thm
-  ("xor_F",
-   ``!x. x xor F <=> x``,
-   RW_TAC bool_ss [xor_def]);
+Theorem xor_F: !x. x xor F <=> x
+Proof RW_TAC bool_ss [xor_def]
+QED
 
-val xor_F = store_thm
-  ("xor_F",
-   ``!x. F xor x <=> x``,
-   RW_TAC bool_ss [xor_def]);
+Theorem F_xor: !x. F xor x <=> x
+Proof RW_TAC bool_ss [xor_def]
+QED
 
 val xor_T = store_thm
   ("xor_T",

src/1/ThmAttribute.sml

@@ -9,7 +9,7 @@ struct
   val funstore = ref (Map.empty : attrfuns Map.table)
 
   val reserved_attrnames = ["local", "unlisted", "nocompute", "schematic",
-                            "notuserdef"]
+                            "notuserdef", "allow_rebind"]
 
   fun okchar c = Char.isAlphaNum c orelse c = #"_" orelse c = #"'"
   fun illegal_attrname s = Lib.mem s reserved_attrnames orelse

src/1/boolLib.sml

@@ -117,23 +117,27 @@ fun prove_local privp (n,th) =
     else ();
     DB.store_local {private=privp} n th;
     th)
-fun extract_localpriv (loc,priv,acc) attrs =
+fun extract_localpriv (loc,priv,rebindok,acc) attrs =
     case attrs of
-        [] => (loc,priv,List.rev acc)
-      | "unlisted" :: rest => extract_localpriv (loc,true,acc) rest
-      | "local" :: rest => extract_localpriv (true,priv,acc) rest
-      | a :: rest => extract_localpriv (loc,priv,a::acc) rest
+        [] => (loc,priv,rebindok,List.rev acc)
+      | "unlisted" :: rest => extract_localpriv (loc,true,rebindok,acc) rest
+      | "local" :: rest => extract_localpriv (true,priv,rebindok,acc) rest
+      | "allow_rebind" :: rest => extract_localpriv (loc,priv,true,acc) rest
+      | a :: rest => extract_localpriv (loc,priv,rebindok,a::acc) rest
 in
 fun save_thm_attrs fname (n, attrs, th) = let
-  val (localp,privp,attrs) = extract_localpriv (false,false,[]) attrs
+  val (localp,privp,rebindok,attrs) =
+      extract_localpriv (false,false,false,[]) attrs
   val save = if localp then prove_local privp
              else if privp then Theory.save_private_thm
              else Theory.save_thm
   val attrf = if localp then ThmAttribute.local_attribute
               else ThmAttribute.store_at_attribute
+  val storemod = if rebindok then trace("Theory.allow_rebinds", 1)
+                 else (fn f => f)
   fun do_attr a = attrf {thm = th, name = n, attrname = a}
 in
-  save(n,th) before app do_attr attrs
+  storemod save(n,th) before app do_attr attrs
 end
 fun store_thm(n0,t,tac) = let
   val (n, attrs) = ThmAttribute.extract_attributes n0

src/1/theory_tests/addDBScript.sml

@@ -2,6 +2,8 @@ open HolKernel Parse boolLib
 
 val _ = new_theory "addDB";
 
+val _ = set_trace "Theory.allow_rebinds" 1
+
 val foo_def = new_definition("foo_def", “foo x <=> ~x”);
 
 val th1 = DB.fetch "-" "foo_def"

src/IndDef/selftest.sml

@@ -2,6 +2,8 @@ open HolKernel Parse boolLib IndDefLib
 
 open testutils
 
+val _ = Feedback.set_trace "Theory.allow_rebinds" 1
+
 fun checkhyps th = if null (hyp th) then ()
                    else die "FAILED - Hyps in theorem!"
 fun f $ x = f x

src/boss/theory_tests/comp_delbinding1Script.sml

@@ -20,7 +20,7 @@ val _ =
 (* now replace "foo_def" binding with something else; the old binding
    should drop out of the compset
 *)
-Theorem foo_def = REFL ``x:num``
+Theorem foo_def[allow_rebind] = REFL ``x:num``
 
 val _ = null (ThmSetData.current_data{settype="compute"}) orelse
         raise Fail "compute data not empty!"

src/boss/theory_tests/quotient_testScript.sml

@@ -21,6 +21,7 @@ in
   {def_name = s ^ "_def", fixity = NONE, fname = s, func = t}
 end
 
+val _ = set_trace "Theory.allow_rebinds" 1
 val thms = define_equivalence_type {
              defs = map mk_def [``C1``, ``C2``],
              equiv = identity_equiv ``:foo``,

src/boss/theory_tests/register_indnAScript.sml

@@ -8,7 +8,7 @@ Definition foo_def:
   foo (h::t) = (h + 1) :: foo t
 End
 
-Definition foo_def:
+Definition foo_def[allow_rebind]:
   foo x 0 = x /\
   foo x (SUC n) = SUC (foo x n)
 End

src/boss/theory_tests/theory1Script.sml

@@ -2,6 +2,8 @@ open HolKernel Parse boolLib bossLib
 
 val _ = new_theory "theory1"
 
+val _ = set_trace "Theory.allow_rebinds" 1
+
 val _ = register_hook("magnus_bug",
                       (fn TheoryDelta.ExportTheory _ => delete_const "h"
                         | _ => ()))

src/coalgebras/itreeScript.sml

@@ -288,7 +288,7 @@ Definition itree_CASE[nocompute]:
     | Event e  => vis e (\a. (itree_abs (\path. itree_rep t (a::path))))
 End
 
-Theorem itree_CASE[compute]:
+Theorem itree_CASE[compute,allow_rebind]:
   itree_CASE (Ret r)   ret div vis = ret r /\
   itree_CASE Div       ret div vis = div /\
   itree_CASE (Vis a g) ret div vis = vis a g
@@ -362,7 +362,7 @@ Proof
   \\ fs [itree_unfold_path_def] \\ metis_tac []
 QED
 
-Theorem itree_unfold:
+Theorem itree_unfold[allow_rebind]:
   itree_unfold f seed =
     case f seed of
     | Ret' r   => Ret r
@@ -428,7 +428,7 @@ Proof
   metis_tac []
 QED
 
-Theorem itree_unfold_err:
+Theorem itree_unfold_err[allow_rebind]:
   itree_unfold_err f (rel, err_f, err) seed =
     case f seed of
     | Ret' r   => Ret r
@@ -464,7 +464,7 @@ Definition itree_el_def:
     itree_CASE t (\r. Return ARB) (Return ARB) (\e g. itree_el (g a) ns)
 End
 
-Theorem itree_el_def:
+Theorem itree_el_def[allow_rebind]:
   itree_el (Ret r) []   = Return r /\
   itree_el Div []       = Stuck /\
   itree_el (Vis e g) [] = Event e /\

src/coalgebras/itreeTauScript.sml

@@ -327,7 +327,7 @@ Definition itree_CASE[nocompute]:
     | Event e => vis e (\a. (itree_abs (\path. itree_rep t (SOME a::path))))
 End
 
-Theorem itree_CASE[compute]:
+Theorem itree_CASE[compute,allow_rebind]:
   itree_CASE (Ret r) ret tau vis = ret r /\
   itree_CASE (Tau t) ret tau vis = tau t /\
   itree_CASE (Vis a g) ret tau vis = vis a g
@@ -416,7 +416,7 @@ Proof
   \\ fs [itree_unfold_path_def] \\ metis_tac []
 QED
 
-Theorem itree_unfold:
+Theorem itree_unfold[allow_rebind]:
   itree_unfold f seed =
     case f seed of
     | Ret' r   => Ret r
@@ -904,7 +904,7 @@ Definition spin:
   spin = itree_unfold (K (Tau' ())) ()
 End
 
-Theorem spin:
+Theorem spin[allow_rebind]:
   spin = Tau spin  (* an infinite sequence of silent actions *)
 Proof
   fs [spin] \\ simp [Once itree_unfold]

src/coalgebras/llistScript.sml

@@ -1906,7 +1906,7 @@ val LFLATTEN_SINGLETON = store_thm(
   STRUCT_CASES_TAC (Q.SPEC `ll4` llist_CASES) THEN
   SIMP_TAC (srw_ss()) [LFLATTEN_THM, LHD_THM, LTL_THM]);
 
-Theorem LFINITE_LFLATTEN:
+Theorem LFINITE_LFLATTEN_EQN:
   !lll:'a llist llist.
     every (\ll. LFINITE ll /\ ll <> LNIL) lll ==>
     LFINITE (LFLATTEN lll) = LFINITE lll
@@ -2783,12 +2783,6 @@ val LNTH_LMAP = Q.store_thm(
   Induct >> simp[LNTH] >> rpt gen_tac >>
   Q.SPEC_THEN `l` STRUCT_CASES_TAC llist_CASES >> simp[])
 
-Theorem LNTH_fromList:
-  !n xs. LNTH n (fromList xs) = if n < LENGTH xs then SOME (EL n xs) else NONE
-Proof
-  Induct \\ Cases_on ‘xs’ \\ fs [LNTH]
-QED
-
 val LLENGTH_LGENLIST = Q.store_thm(
   "LLENGTH_LGENLIST[simp,compute]",
   `!f. LLENGTH (LGENLIST f limopt) = limopt`,
@@ -3609,7 +3603,7 @@ Proof
   simp[FUN_EQ_THM]
 QED
 
-Theorem LFLATTEN_fromList:
+Theorem LFLATTEN_fromList_of_NILs:
   EVERY ($= LNIL) l ==> LFLATTEN (fromList l) = LNIL
 Proof
   Induct_on ‘l’ >> simp[]
@@ -3628,7 +3622,7 @@ Proof
       rpt strip_tac >> gs[LFILTER_EQ_NIL, not_compose, iffRL LFLATTEN_EQ_NIL]>>
       drule_then strip_assume_tac LFILTER_EQ_CONS >>
       gvs[LFLATTEN_APPEND_FINITE1, LFINITE_fromList,
-          not_compose, LFLATTEN_fromList] >>
+          not_compose, LFLATTEN_fromList_of_NILs] >>
       drule_at (Pos last) every_LAPPEND2_LFINITE >>
       simp[LFINITE_fromList]) >>
   rpt $ pop_assum mp_tac >> qid_spec_tac ‘ll’ >> Induct_on ‘LFINITE’ >>
@@ -3643,7 +3637,7 @@ Proof
            h:::ll1’] >>
   ‘FILTER ($~ o $= LNIL) l = []’
     by simp[listTheory.FILTER_EQ_NIL, SF ETA_ss] >>
-  gs[LFLATTEN_fromList] >>
+  gs[LFLATTEN_fromList_of_NILs] >>
   Cases_on ‘hl’ >> gvs[] >> rename [‘LFLATTEN _ = LAPPEND t _’] >>
   first_x_assum $ qspec_then ‘t:::ll2’ mp_tac >> simp[LFLATTEN_APPEND] >>
   rw[] >> rw[]