Fix rebinds

candle/prover/candle_kernel_valsScript.sml

@@ -223,7 +223,7 @@ Definition THM_TYPE_HEAD_def:
            s ∈ thm_ctors_set
 End
 
-Theorem THM_TYPE_HEAD_def = SIMP_RULE list_ss [] THM_TYPE_HEAD_def;
+Theorem THM_TYPE_HEAD_def[allow_rebind] = SIMP_RULE list_ss [] THM_TYPE_HEAD_def;
 
 Definition LIST_TYPE_HEAD_def:
   LIST_TYPE_HEAD h v = ∃l:unit list. LIST_TYPE (K h) l v
@@ -1144,15 +1144,6 @@ Proof
   prove_head_tac
 QED
 
-Theorem is_type_v_head:
-  do_opapp [is_type_v; v] = SOME (env, exp) ∧
-  evaluate ^s env [exp] = (s', res) ⇒
-    ^safe_error_goal ∨
-    TYPE_TYPE_HEAD v
-Proof
-  prove_head_tac
-QED
-
 Theorem is_vartype_v_head:
   do_opapp [is_vartype_v; v] = SOME (env, exp) ∧
   evaluate ^s env [exp] = (s', res) ⇒
@@ -1261,15 +1252,6 @@ Proof
   prove_head_tac
 QED
 
-Theorem dest_type_v_head:
-  do_opapp [dest_type_v; v] = SOME (env, exp) ∧
-  evaluate ^s env [exp] = (s', res) ⇒
-    ^safe_error_goal ∨
-    TYPE_TYPE_HEAD v
-Proof
-  prove_head_tac
-QED
-
 Theorem dest_eq_v_head:
   do_opapp [dest_eq_v; v] = SOME (env, exp) ∧
   evaluate ^s env [exp] = (s', res) ⇒
@@ -1297,15 +1279,6 @@ Proof
   prove_head_tac
 QED
 
-Theorem call_type_vars_in_term_v_head:
-  do_opapp [call_type_vars_in_term_v; v] = SOME (env, exp) ∧
-  evaluate ^s env [exp] = (s', res) ⇒
-    ^safe_error_goal ∨
-    TERM_TYPE_HEAD v
-Proof
-  prove_head_tac
-QED
-
 Theorem new_basic_definition_v_head:
   do_opapp [new_basic_definition_v; v] = SOME (env, exp) ∧
   evaluate ^s env [exp] = (s', res) ⇒
@@ -1464,17 +1437,6 @@ Proof
   prove_head_tac
 QED
 
-Theorem vsubst_v_head:
-  do_partial_app vsubst_v v = SOME g ∧
-  do_opapp [g; w] = SOME (env, exp) ∧
-  evaluate ^s env [exp] = (s', res) ⇒
-    ^safe_error_goal ∨
-    LIST_TYPE_HEAD (PAIR_TYPE_HEAD TERM_TYPE_HEAD TERM_TYPE_HEAD) v ∧
-    TERM_TYPE_HEAD w
-Proof
-  prove_head_tac
-QED
-
 Theorem inst_v_head:
   do_partial_app inst_v v = SOME g ∧
   do_opapp [g; w] = SOME (env, exp) ∧
@@ -1599,17 +1561,6 @@ Proof
   prove_head_tac
 QED
 
-Theorem inst_v_head:
-  do_partial_app inst_v v = SOME g ∧
-  do_opapp [g; w] = SOME (env, exp) ∧
-  evaluate ^s env [exp] = (s', res) ⇒
-    ^safe_error_goal ∨
-    LIST_TYPE_HEAD (PAIR_TYPE_HEAD TYPE_TYPE_HEAD TYPE_TYPE_HEAD) v ∧
-    TERM_TYPE_HEAD w
-Proof
-  prove_head_tac
-QED
-
 Theorem Kernel_print_thm_v_head:
   do_opapp [Kernel_print_thm_v; v] = SOME (env, exp) ∧
   evaluate ^s env [exp] = (s', res) ⇒

candle/prover/candle_prover_invScript.sml

@@ -383,20 +383,6 @@ Proof
   \\ gvs [nsLookup_Bind_v_some, CaseEqs ["bool", "option"], kernel_types_def]
 QED
 
-Theorem v_ok_bind_exn_v[simp]:
-  v_ok ctxt bind_exn_v
-Proof
-  fs [bind_exn_v_def]
-  \\ fs [Once v_ok_cases,bind_stamp_def]
-QED
-
-Theorem v_ok_sub_exn_v[simp]:
-  v_ok ctxt sub_exn_v
-Proof
-  rw [v_ok_def, sub_exn_v_def]
-  \\ rw [Once v_ok_cases, subscript_stamp_def, kernel_types_def]
-QED
-
 Theorem v_ok_Cons:
   v_ok ctxt (Conv (SOME (TypeStamp "::" 1)) [x; y]) ⇔ v_ok ctxt x ∧ v_ok ctxt y
 Proof

compiler/repl/repl_moduleProgScript.sml

@@ -142,10 +142,10 @@ val eval_thm = let
   in v_thm |> REWRITE_RULE [GSYM v_def] end
 val _ = ml_prog_update (add_Dlet eval_thm "exn");
 
-Theorem exn_def          = fetch "-" "exn_def"                        |> tidy_up;
-Theorem isEOF_def        = declare_new_ref "isEOF"        “F”         |> tidy_up;
-Theorem nextString_def   = declare_new_ref "nextString"   “strlit ""” |> tidy_up;
-Theorem errorMessage_def = declare_new_ref "errorMessage" “strlit ""” |> tidy_up;
+Theorem exn_def[allow_rebind]          = fetch "-" "exn_def"                        |> tidy_up;
+Theorem isEOF_def[allow_rebind]        = declare_new_ref "isEOF"        “F”         |> tidy_up;
+Theorem nextString_def[allow_rebind]   = declare_new_ref "nextString"   “strlit ""” |> tidy_up;
+Theorem errorMessage_def[allow_rebind] = declare_new_ref "errorMessage" “strlit ""” |> tidy_up;
 
 val _ = ml_prog_update open_local_block;
 

examples/divScript.sml

@@ -485,7 +485,7 @@ val io_events_def = Define `
 
 Overload yes = ``yes_v``
 
-Theorem yes_spec:
+Theorem yes_spec_lemma:
   !uv.
     limited_parts names p ==>
     app (p:'ffi ffi_proj) ^(fetch_v "yes" st) [arg]
@@ -515,7 +515,7 @@ Proof
   \\ irule REPLICATE_LIST_LREPEAT \\ fs []
 QED
 
-val yes_spec = save_thm("yes_spec",yes_spec |> SPEC_ALL |> UNDISCH_ALL);
+val yes_spec = save_thm("yes_spec", yes_spec_lemma |> SPEC_ALL |> UNDISCH_ALL);
 
 (* An IO-conditional loop with side effects *)
 

examples/lcsScript.sml

@@ -243,12 +243,6 @@ Proof
   fs[common_subsequence_def,is_subsequence_append]
 QED
 
-Theorem common_subsequence_sym:
-   common_subsequence u u u
-Proof
-  fs[common_subsequence_def,is_subsequence_refl]
-QED
-
 Theorem common_subsequence_sym:
    common_subsequence s u t = common_subsequence s t u
 Proof
@@ -895,7 +889,7 @@ Proof
           >> rfs[] >> metis_tac[sub_le_suc])
 QED
 
-Theorem dynamic_lcs_row_invariant_pres2:
+Theorem dynamic_lcs_row_invariant_pres2[allow_rebind]:
     !h r previous_col previous_row diagonal prevh fullr l n.
   (dynamic_lcs_row_invariant h r previous_col previous_row diagonal prevh fullr
     /\ (dynamic_lcs_row h r previous_col previous_row diagonal = l)

examples/lpr_checker/lprScript.sml

@@ -993,7 +993,7 @@ Proof
 QED
 
 (* Theorems about mindel *)
-Theorem lookup_FOLDL_delete:
+Theorem lookup_FOLDL_delete':
   ∀l fml.
   lookup n fml = SOME c ∧
   EVERY ($< mindel) l ∧ n ≤ mindel ⇒
@@ -1013,7 +1013,7 @@ Theorem check_lpr_step_mindel:
 Proof
   rw[check_lpr_step_def]>>
   every_case_tac>>fs[]>>rw[lookup_insert]>>
-  match_mp_tac lookup_FOLDL_delete>>
+  match_mp_tac lookup_FOLDL_delete'>>
   fs[EVERY_MEM]
 QED
 

examples/lpr_checker/ramseyScript.sml

@@ -801,17 +801,17 @@ val sol = rconc (EVAL ``
       250; 251; 252; 253; 254; 255; 256; 257; 258; 259; 260; 261; 262; 263;
       264; 265; 266; 267; 268; 269; 270]``);
 
-val solf_def = Define`
-  solf n = case lookup n ^sol of NONE => F | _ => T`
+val solf'_def = Define`
+  solf' n = case lookup n ^sol of NONE => F | _ => T`
 
-val thm = EVAL ``check_sat solf (fast_ramsey_lpr 4 17)``;
+val thm = EVAL ``check_sat solf' (fast_ramsey_lpr 4 17)``;
 
 Theorem not_is_ramsey_4_17:
   ¬(is_ramsey 4 17)
 Proof
   match_mp_tac fast_ramsey_lpr_correct>>
   simp[satisfiable_def]>>
-  qexists_tac`solf`>>match_mp_tac check_sat_satisfies>>
+  qexists_tac`solf'`>>match_mp_tac check_sat_satisfies>>
   simp[thm]
 QED
 

examples/md5ProgScript.sml

@@ -101,7 +101,7 @@ val _ = (append_prog o process_topdecs) `
       Some s => md5_final s
     | None => None`;
 
-Theorem md5_of_v_def = fetch "-" "md5_of_v_def";
+val md5_of_v_def = fetch "-" "md5_of_v_def";
 
 Theorem md5_of_SOME:
   OPTION_TYPE FILENAME (SOME s) fnv ∧

examples/stackProgScript.sml

@@ -57,7 +57,7 @@ val xs_auto_tac = rpt (FIRST [xcon, (CHANGED_TAC xsimpl), xif, xmatch, xapp, xle
 
 val st = get_ml_prog_state ();
 
-Theorem empty_stack_spec:
+Theorem empty_stack_spec':
      !uv. app (p:'ffi ffi_proj) ^(fetch_v "empty_stack" st) [uv]
           emp (POSTv qv. STACK A [] qv)
 Proof
@@ -77,7 +77,7 @@ Proof
     xcf "empty_stack" st >> simp[STACK_def] >> xs_auto_tac
 QED
 
-Theorem push_spec:
+Theorem push_spec':
      !qv xv vs x. app (p:'ffi ffi_proj) ^(fetch_v "push" st) [qv; xv]
           (STACK A vs qv * & A x xv)
           (POSTv uv. STACK A (vs ++ [x]) qv)

icing/pull_wordsScript.sml

@@ -130,14 +130,6 @@ Termination
   \\ imp_res_tac exp_size_lemma \\ gvs []
 End
 
-Definition gather_constants_decl_def:
-  gather_constants_decl [Dlet loc p e] =
-    gather_constants_exp e ∧
-  gather_constants_decl (d1::d2::ds) =
-    gather_constants_decl [d1] ++ gather_constants_decl (d2::ds) ∧
-  gather_constants_decl _ = []
-End
-
 (**
   Walk over an AST and replace constants by variables that globally allocate
   their value
@@ -1883,19 +1875,6 @@ Proof
   >> gs[]
 QED
 
-Theorem build_cnst_list_unique:
-  DISJOINT (set (FLAT (MAP gather_used_identifiers_exp es)))
-    (set (MAP SND (build_cnst_list ws (FLAT (MAP gather_used_identifiers_exp es)) 0)))
-Proof
-  gs[pred_setTheory.DISJOINT_DEF, INTER_DEF]
-  >> rewrite_tac [FUN_EQ_THM] >> rpt strip_tac >> reverse EQ_TAC
-  >- gs[]
-  >> gs[]
-  >> Cases_on ‘MEM x (MAP SND (build_cnst_list ws (FLAT (MAP gather_used_identifiers_exp es)) 0))’
-  >> gs[]
-  >> imp_res_tac MEM_used_ids_not_mem_vars
-QED
-
 Theorem build_cnst_list_disjoint_res:
   ∀ cnsts vars n.
     DISJOINT (set (MAP SND (build_cnst_list cnsts vars n))) (set vars)

icing/source_to_source2ProofsScript.sml

@@ -3179,7 +3179,7 @@ Proof
   \\ simple_case_tac
 QED
 
-Theorem stos_pass_with_plans_sing_exists:
+Theorem stos_pass_with_plans_sing_exists':
   ∃ e_opt res. stos_pass_with_plans cfg [h][e] = [(e_opt, res)]
 Proof
   measureInduct_on ‘exp_size e’\\ Cases_on ‘e’ \\ fs[stos_pass_with_plans_def]
@@ -3193,7 +3193,7 @@ Theorem MAP_FST_Fun:
   MAP FST ((λ (e_opt, res). [(Fun s e_opt, res)])(HD (stos_pass_with_plans cfg [h][e]))) =
   [Fun s (FST (HD (stos_pass_with_plans cfg [h][e])))]
 Proof
-  qspec_then ‘e’ assume_tac (GEN “e:ast$exp”stos_pass_with_plans_sing_exists)
+  qspec_then ‘e’ assume_tac (GEN “e:ast$exp”stos_pass_with_plans_sing_exists')
   \\ fs[]
 QED
 

translator/monadic/ml_monad_translatorLib.sml

@@ -460,7 +460,7 @@ fun abbrev_nsLookup_code th = let
     List.filter (not o is_const o snd)
 
   fun find_abbrev (name, code) = let
-    val n = Theory.temp_binding ("[[ " ^ name ^ "_code ]]")
+    val n = Theory.temp_binding ("____" ^ name ^ "_code____")
     val code_def = Definition.new_definition(n,mk_eq(mk_var(n,type_of code),code))
   in code_def end
   val abbrevs = List.map find_abbrev name_code_pairs
@@ -2915,7 +2915,7 @@ handle HOL_ERR _ => failwith "extract_precondition_rec failed";
 fun abbrev_code (fname,ml_fname,def,th,v) = let
   val th = th |> UNDISCH_ALL
   val exp = th |> concl |> rator |> rator |> rand
-  val n = Theory.temp_binding ("[[ " ^ fname ^ "_code ]]")
+  val n = Theory.temp_binding ("____" ^ fname ^ "_code____")
   val code_def = Definition.new_definition(n,mk_eq(mk_var(n,type_of exp),exp))
   val th =
     CONV_RULE ((RATOR_CONV o RATOR_CONV o RAND_CONV) (K (GSYM code_def))) th