Various fixes for theorem-rebind errors

Now think that -t3 build goes through entirely.

examples/machine-code/graph/func_decompileLib.sml

@@ -10,6 +10,8 @@ open writerLib cond_cleanLib;
 val _ = max_print_depth := ~1;
 val _ = set_trace "Unicode" 0;
 
+val new_definition = Feedback.trace ("Theory.allow_rebinds", 1) new_definition
+
 local
   val export_fails = ref ([]:string list)
 in

examples/machine-code/lisp/lisp_proofScript.sml

@@ -35,12 +35,16 @@ val x2sexp_def = tDefine "x2sexp" `
 
 val x2sexp = x2sexp_def |> CONJUNCTS |> map SPEC_ALL |> LIST_CONJ
 
-val term2sexp_def = save_thm("func2sexp_def",save_thm("term2sexp_def",let
-  val term2sexp_deff = Define `term2sexp x = x2sexp (T,x,FunVar "nil")`;
-  val func2sexp_deff = Define `func2sexp y = x2sexp (F,Var "nil",y)`;
-  val th = Q.INST [`xx`|->`Var "nil"`,`yy`|->`FunVar "nil"`] x2sexp
-  val th = REWRITE_RULE [GSYM term2sexp_deff,GSYM func2sexp_deff] th
-  in th end));
+val term2sexp_def = save_thm(
+  "func2sexp_def[allow_rebind]",
+  save_thm(
+    "term2sexp_def[allow_rebind]",
+    let
+      val term2sexp_deff = Define `term2sexp x = x2sexp (T,x,FunVar "nil")`;
+      val func2sexp_deff = Define `func2sexp y = x2sexp (F,Var "nil",y)`;
+      val th = Q.INST [`xx`|->`Var "nil"`,`yy`|->`FunVar "nil"`] x2sexp
+      val th = REWRITE_RULE [GSYM term2sexp_deff,GSYM func2sexp_deff] th
+    in th end));
 
 val zip_yz_lemma = prove(
   ``!xs ys zs x (stack:SExp) alist (l:num).

examples/theorem-prover/lisp-runtime/extract/lisp_extractLib.sml

@@ -13,6 +13,7 @@ val op \\ = op THEN;
 val RW = REWRITE_RULE;
 val RW1 = ONCE_REWRITE_RULE;
 
+fun allowing_rebinds f x = Feedback.trace ("Theory.allow_rebinds", 1) f x
 
 (* definitions *)
 
@@ -41,6 +42,7 @@ fun new_def def_tm term_tac = let
             handle HOL_ERR _ => NONE)
   in (def,ind) end
 
+val new_def = allowing_rebinds new_def
 
 (* ML equivalent of term datatype defined in lisp_semanticsTheory *)
 
@@ -444,6 +446,8 @@ fun pure_extract name term_tac = let
   val _ = save_thm("R_ev_" ^ good_name,result)
   in def end;
 
+val pure_extract = fn n => fn tac => allowing_rebinds (pure_extract n) tac
+
 fun pure_extract_mutual_rec names term_tac = let
   val _ = print "extracting:"
   val _ = map (fn name => print (" " ^ name)) names
@@ -858,6 +862,9 @@ fun impure_extract_aux name term_tac use_short_cut = let
   val _ = save_thm("R_ev_" ^ good_name,result)
   in def end;
 
+val impure_extract_aux =
+    fn n => fn tac => fn b => allowing_rebinds (impure_extract_aux n tac) b
+
 fun impure_extract name term_tac =
   impure_extract_aux name term_tac false
 

examples/theorem-prover/lisp-runtime/garbage-collector/stop_and_copyScript.sml

@@ -416,27 +416,25 @@ val rel_gc_def = Define `
 
 (* invariant *)
 
-val (full_heap_rules,full_heap_ind,full_heap_cases) =
-  Hol_reln
-  `(!b m. full_heap b b m) /\
-   (!b e m n xs d.
-      (m b = H_BLOCK (xs,n,d)) /\ EMP_RANGE (b+1,b+n+1) m /\
-      full_heap (b+n+1) e m ==> full_heap b e m)`;
-
-val full_heap_ind = IndDefLib.derive_strong_induction(full_heap_rules,full_heap_ind);
-val _ = save_thm("full_heap_ind",full_heap_ind);
-
-val (part_heap_rules,part_heap_ind,part_heap_cases) =
-  Hol_reln
-  `(!b m. part_heap b b m 0) /\
-   (!b e m k.
-      ~(isBLOCK (m b)) /\ part_heap (b+1) e m k ==> part_heap b e m k) /\
-   (!b e m n xs d k.
-      (m b = H_BLOCK (xs,n,d)) /\ EMP_RANGE (b+1,b+n+1) m /\
-      part_heap (b+n+1) e m k ==> part_heap b e m (k+n+1))`;
-
-val part_heap_ind = IndDefLib.derive_strong_induction(part_heap_rules,part_heap_ind);
-val _ = save_thm("part_heap_ind",part_heap_ind);
+Inductive full_heap:
+  (!b m. full_heap b b m) /\
+  (!b e m n xs d.
+     (m b = H_BLOCK (xs,n,d)) /\ EMP_RANGE (b+1,b+n+1) m /\
+     full_heap (b+n+1) e m ==> full_heap b e m)
+End
+
+val full_heap_ind = save_thm("full_heap_ind[allow_rebind]",full_heap_strongind);
+
+Inductive part_heap:
+  (!b m. part_heap b b m 0) /\
+  (!b e m k.
+     ~(isBLOCK (m b)) /\ part_heap (b+1) e m k ==> part_heap b e m k) /\
+  (!b e m n xs d k.
+     (m b = H_BLOCK (xs,n,d)) /\ EMP_RANGE (b+1,b+n+1) m /\
+     part_heap (b+n+1) e m k ==> part_heap b e m (k+n+1))
+End
+
+val part_heap_ind = save_thm("part_heap_ind[allow_rebind]",part_heap_strongind);
 
 val ref_heap_mem_def = Define `
   ref_heap_mem (h,f) m =

examples/theorem-prover/lisp-runtime/implementation/lisp_codegenScript.sml

@@ -374,14 +374,6 @@ val (mc_xbp_load_spec,mc_xbp_load_def) = basic_decompile_strings x64_tools "mc_x
 
 val BLAST_LEMMA = prove(``w << 2 !! 1w = w << 2 + 1w:word32``,blastLib.BBLAST_TAC);
 
-val EL_UPDATE_NTH = store_thm("EL_UPDATE_NTH",
-  ``!xs n k x. EL n (UPDATE_NTH k x xs) =
-               if (k = n) /\ k < LENGTH xs then x else EL n xs``,
-  Induct \\ Cases_on `k` \\ SIMP_TAC std_ss [LENGTH,UPDATE_NTH_def]
-  THEN1 (Cases_on `n` \\ FULL_SIMP_TAC std_ss [EL,HD,TL] \\ FULL_SIMP_TAC std_ss [ADD1])
-  \\ Cases_on `n'` \\ FULL_SIMP_TAC std_ss [EL,HD,TL]
-  \\ FULL_SIMP_TAC std_ss [ADD1]);
-
 val UPDATE_NTH_1 = prove(``UPDATE_NTH 1 x (y1::y2::ys) = y1::x::ys``, EVAL_TAC);
 
 val mc_xbp_load_blast = blastLib.BBLAST_PROVE

examples/theorem-prover/lisp-runtime/implementation/lisp_opsScript.sml

@@ -13,6 +13,7 @@ open progTheory set_sepTheory helperLib;
 open prog_x64Theory prog_x64Lib x64_encodeLib;
 open stop_and_copyTheory;
 
+fun allowing_rebinds f x = Feedback.trace ("Theory.allow_rebinds", 1) f x
 infix \\
 val op \\ = op THEN;
 val RW = REWRITE_RULE;
@@ -83,7 +84,8 @@ val zLISP_INIT_def = Define `
        zCODE_UNCHANGED cu dd d *
         cond (lisp_init (a1,a2,sl,sl1,e,ex,cs) io (df,f,dg,g,dd,d,sp,sa1,sa_len,ds))`;
 
-val zLISP_raw = Define `zLISP = zLISP_ALT (\wsp wi we ds tw2. T)`;
+Definition zLISP_raw: zLISP = zLISP_ALT (\wsp wi we ds tw2. T)
+End
 val zLISP_def = SIMP_CONV std_ss [zLISP_ALT_def,zLISP_raw]
   ``zLISP (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok)``
 val _ = save_thm("zLISP_def",zLISP_def);
@@ -644,9 +646,12 @@ fun X64_LISP_EQ_VAL n i = let
   val result = prove_spec th imp def pre_tm post_tm
   in save_lisp_thm("X64_LISP_EQ_VAL_" ^ int_to_string n ^ "_" ^ int_to_string i,result) end;
 
+val X64_LISP_EQ_VAL = fn n => fn i => allowing_rebinds (X64_LISP_EQ_VAL n) i
+
 val _ = map (X64_LISP_EQ_VAL 1) all_regs;
 val _ = map (X64_LISP_EQ_VAL 2) all_regs;
 val _ = map (X64_LISP_EQ_VAL 3) all_regs;
+(* does 3 0 a second time *)
 val _ = map (fn n => X64_LISP_EQ_VAL n 0) [3,4,5,6,7,8,9,10,11,12,13,14,15];
 
 (* eq *)
@@ -864,7 +869,7 @@ val all_syms = ilist 0 lisp_inv_sym_tests;
 val _ = map (X64_LISP_SYM 0) all_regs; (* NIL *)
 val _ = map (X64_LISP_SYM 1) all_regs; (* T *)
 val _ = map (X64_LISP_SYM 2) all_regs; (* QUOTE *)
-val _ = map (fn x => X64_LISP_SYM x 0) all_syms;
+val _ = map (fn x => allowing_rebinds (X64_LISP_SYM x) 0) all_syms;
 
 
 (* error *)
@@ -3015,8 +3020,8 @@ val X64_LISP_TEST_CF = let
 
 (* prove a few theorems which imply that the bytecode does the right thing *)
 
-val X64_POP0 = SPEC_COMPOSE_RULE [X64_LISP_TOP 0,X64_LISP_POP]
-val X64_POP1 = SPEC_COMPOSE_RULE [X64_LISP_TOP 1,X64_LISP_POP]
+val X64_POP0 = SPEC_COMPOSE_RULE [allowing_rebinds X64_LISP_TOP 0,X64_LISP_POP]
+val X64_POP1 = SPEC_COMPOSE_RULE [allowing_rebinds X64_LISP_TOP 1,X64_LISP_POP]
 
 val X64_LISP_SWAP1 = let
   val ((th,_,_),_) = x64_spec (x64_encode "xchg r8,r9")

examples/theorem-prover/lisp-runtime/implementation/lisp_symbolsScript.sml

@@ -406,12 +406,6 @@ val IO_WRITE_APPEND = store_thm("IO_WRITE_APPEND",
   ``!io x1 x2. IO_WRITE (IO_WRITE io x1) x2 = IO_WRITE io (x1 ++ x2)``,
   Cases \\ ASM_SIMP_TAC std_ss [IO_WRITE_def,APPEND_ASSOC,MAP_APPEND]);
 
-val zIO_def = Define `
-  zIO (iow:word64,ior:word64,iod:word64,ioi:word64) (io:io_streams) = zR 2w 3w`;
-
-val zIO_R_def = Define `
-  zIO_R (iow,ior,iod) io = SEP_EXISTS ioi. zR 1w ioi * zIO (iow,ior,iod,ioi) io`;
-
 val null_term_str_def = Define `
   null_term_str a df f str =
     ?p. (one_string a (str ++ [CHR 0]) * p) (fun2set (f,df)) /\