Remove some Define usages manually

Author: dnezam

basis/TextIOProgScript.sml

@@ -16,9 +16,11 @@ val _ = ml_prog_update (open_module "TextIO");
 
 val _ = ml_prog_update open_local_block;
 
-
-(* val get_buffered_in_def = Define `get_out (InstreamBuffered)` *)
-
+(*
+Definition get_buffered_in_def:
+  get_out (InstreamBuffered)
+End
+*)
 
 Datatype:
   instream = Instream mlstring

basis/fsFFIScript.sml

@@ -281,7 +281,8 @@ Definition ffi_close_def:
 End
 
 (* given a file descriptor and an offset, returns 0 and update fs or returns 1
-* if an error is met val ffi_seek = Define`
+ * if an error is met
+Definition ffi_seek_def:
   ffi_seek bytes fs =
     do
       assert(LENGTH bytes = 2);
@@ -290,7 +291,9 @@ End
         return(LUPDATE 0w 0 bytes, fs')
       od ++
       return (LUPDATE 1w 0 bytes, fs)
-    od`; *)
+    od
+End
+ *)
 (* -- *)
 
 (* Packaging up the model as an ffi_part *)

characteristic/cfLetAutoScript.sml

@@ -91,8 +91,10 @@ Definition HPROP_INJ_def:
 End
 
 (* TODO: use that *)
-(* val HPROP_FRAME_IMP_def = Define `HPROP_FRAME_IMP H1 H2 Frame <=>
-?s. VALID_HEAP s /\ H1 s /\ (H2 * Frame) s`;
+(*
+Definition HPROP_FRAME_IMP_def:
+  HPROP_FRAME_IMP H1 H2 Frame <=> ?s. VALID_HEAP s /\ H1 s /\ (H2 * Frame) s
+End
 
 Theorem HPROP_FRAME_HCOND:
  HPROP_FRAME_IMP H1 (&PF * H2) Frame <=> PF /\ HPROP_FRAME_IMP H1 H2 Frame

compiler/backend/ag32/proofs/ag32_ffi_codeProofScript.sml

@@ -2923,10 +2923,10 @@ Proof
   qexists_tac `0` >> simp[]
 QED
 
-val ag32_ffi_get_arg_length_loop1_code_def = Define‘
+Definition ag32_ffi_get_arg_length_loop1_code_def:
   ag32_ffi_get_arg_length_loop1_code =
     GENLIST (λi. EL (i + 2) ag32_ffi_get_arg_length_loop_code) 4
-’;
+End
 
 val instn = instn0
               (CONV_RULE (RAND_CONV EVAL)
@@ -2976,13 +2976,13 @@ val loop_code_def' = Q.prove(
 val instn = instn0 loop_code_def'
 val combined = combined0 instn gmw
 
-val has_n_args_def = Define‘
+Definition has_n_args_def:
   (has_n_args mem a 0 ⇔ T) ∧
   (has_n_args (mem : word32 -> word8) a (SUC n) ⇔
      ∃off. mem (a + n2w off) = 0w ∧
            (∀i. i < off ⇒ mem (a + n2w i) ≠ 0w) ∧
            has_n_args mem (a + n2w off + 1w) n)
-’;
+End
 
 Theorem ag32_ffi_get_arg_length_loop_code_thm:
    has_n_args s.MEM (s.R 5w) argc ∧ w2n (s.R 6w) ≤ argc ∧

compiler/backend/word_allocScript.sml

@@ -835,7 +835,7 @@ Proof
 QED
 
 (* Old representation *)
-(* val get_clash_sets_def = Define`
+(* Definition get_clash_sets_def:
   (get_clash_sets (Seq s1 s2) live =
     let (hd,ls) = get_clash_sets s2 live in
     let (hd',ls') = get_clash_sets s1 hd in
@@ -867,7 +867,8 @@ QED
   (*Catchall for cases where we dont have in sub programs live sets*)
   (get_clash_sets prog live =
     let i_set = union (get_writes prog) live in
-      (get_live prog live,[i_set]))`
+      (get_live prog live,[i_set]))
+  End
 *)
 
 (* Potentially more efficient liveset representation for checking / allocation*)

compiler/inference/proofs/envRelScript.sml

@@ -26,11 +26,13 @@ Definition convert_env_def:
 convert_env s env = MAP (\(x,t). (x, convert_t (t_walkstar s t))) env
 End
 
-(* val convert_decls_def = Define `
-convert_decls idecls =
+(*
+Definition convert_decls_def:
+  convert_decls idecls =
   <| defined_mods := set idecls.inf_defined_mods;
      defined_types :=  set idecls.inf_defined_types;
-     defined_exns := set idecls.inf_defined_exns|>`;
+     defined_exns := set idecls.inf_defined_exns|>
+End
 
 Theorem convert_append_decls:
  !decls1 decls2. convert_decls (append_decls decls1 decls2) = union_decls (convert_decls decls1) (convert_decls decls2)

compiler/repl/repl_init_typesScript.sml

@@ -33,8 +33,11 @@ val print_types = let
   val _ = print "\n"
   in () end
 val result_tm = eval_res_thm |> concl |> rand |> rand
-val def = Define ‘repl_prog_types = ^result_tm’
-val result = eval_res_thm |> CONV_RULE (PATH_CONV "rr" (REWR_CONV (GSYM def)))
+Definition repl_prog_types_def:
+  repl_prog_types = ^result_tm
+End
+val result = eval_res_thm
+               |> CONV_RULE (PATH_CONV "rr" (REWR_CONV (GSYM repl_prog_types_def)));
 
 Theorem repl_prog_types_thm = result;
 

examples/queueProgScript.sml

@@ -45,14 +45,15 @@ End
 
 val EmptyQueue_exn_def = EVAL ``EmptyQueue_exn v``;
 
-val lqueue_def = Define‘
+Definition lqueue_def:
   lqueue qels f r els ⇔
     f < LENGTH qels ∧ r < LENGTH qels ∧
     (f ≤ r ∧
      (∃pj rj. qels = pj ++ els ++ rj ∧ LENGTH pj = f ∧
               r + LENGTH rj = LENGTH qels) ∨
      r ≤ f ∧ (∃p s mj. qels = s ++ mj ++ p ∧ els = p ++ s ∧
-                       r = LENGTH s ∧ f = r + LENGTH mj))’;
+                       r = LENGTH s ∧ f = r + LENGTH mj))
+End
 
 Theorem lqueue_empty:
    i < LENGTH xs ⇒ lqueue xs i i []
@@ -112,14 +113,15 @@ QED
    operations can be expressed in terms of the abstract value
 *)
 
-val QUEUE_def = Define‘
+Definition QUEUE_def:
   QUEUE A sz els qv ⇔
     SEP_EXISTS av fv rv cv qelvs.
       REF qv (Conv NONE [av;fv;rv;cv]) *
       ARRAY av qelvs *
       & (0 < sz ∧ NUM (LENGTH els) cv ∧
          ∃qels f r. LIST_REL A qels qelvs ∧ NUM f fv ∧ NUM r rv ∧
-                    lqueue qels f r els ∧ LENGTH qels = sz)’;
+                    lqueue qels f r els ∧ LENGTH qels = sz)
+End
 (*
    type_of “QUEUE”;
 *)

semantics/cmlPtreeConversionScript.sml

@@ -831,8 +831,7 @@ Definition letFromPat_def:
     | _ => Mat rhs [(p,body)]
 End
 
-local
-  val ptree_Expr_quotation = `
+Definition ptree_Expr_def:
   ptree_Expr ent (Lf _) = NONE ∧
   ptree_Expr ent (Nd (nt,loc) subs) =
   do
@@ -1217,11 +1216,8 @@ local
             seq <- ptree_Eseq seq_pt;
             SOME(e::seq)
           od
-        | _ => NONE)`
-in
-
-val ptree_Expr_def = Define ptree_Expr_quotation
-end
+        | _ => NONE)
+End
 
 Definition ptree_StructName_def:
   ptree_StructName (Lf _) = NONE ∧

semantics/proofs/cmlPtreeConversionPropsScript.sml

@@ -16,21 +16,21 @@ val _ = option_monadsyntax.temp_add_option_monadsyntax()
 
 (* first, capture those types that we expect to be in the range of the
    conversion *)
-val user_expressible_tyname_def = Define‘
+Definition user_expressible_tyname_def:
   (user_expressible_tyname (Short s) ⇔ T) ∧
   (user_expressible_tyname (Long m (Short s)) ⇔ T) ∧
   (user_expressible_tyname _ ⇔ F)
-’;
+End
 val _ = augment_srw_ss [rewrites [user_expressible_tyname_def]]
 
 Overload ND[local] = “λn. Nd (mkNT n, ARB)”
 Overload LF[local] = “λt. Lf (TOK t, ARB)”
 
-val tyname_to_AST_def = Define‘
+Definition tyname_to_AST_def:
   tyname_to_AST (Short n) = ND nTyOp [ND nUQTyOp [LF (AlphaT n)]] ∧
   tyname_to_AST (Long md (Short n)) = ND nTyOp [LF (LongidT md n)] ∧
   tyname_to_AST _ = ARB
-’;
+End
 
 Theorem tyname_inverted:
    ∀id. user_expressible_tyname id ⇒

translator/ml_progScript.sml

@@ -624,8 +624,10 @@ in
 Definition init_env_def[nocompute]:
   init_env = ^init_env_tm
 End
-  val init_state_def = Define `
-    init_state ffi = ^init_state_tm`;
+
+Definition init_state_def:
+  init_state ffi = ^init_state_tm
+End
 end
 
 Theorem init_state_env_thm: