Update "val foo_def = Define ..." to use Definition syntax

basis/ArrayProofScript.sml

@@ -474,8 +474,9 @@ val drop_pre_length_thm = Q.prove(
 );
 
 (*
-val ARRAY_TYPE_def = Define`
-  ARRAY_TYPE A a av = SEP_EXISTS vs. ARRAY av vs * & LIST_REL A a vs`;
+Definition ARRAY_TYPE_def:
+  ARRAY_TYPE A a av = SEP_EXISTS vs. ARRAY av vs * & LIST_REL A a vs
+End
 *)
 
 Theorem array_modify_aux_spec:

basis/CommandLineProofScript.sml

@@ -8,12 +8,14 @@ val _ = new_theory"CommandLineProof";
 
 val _ = translation_extends"CommandLineProg";
 
-val wfcl_def = Define`
-  wfcl cl <=> EVERY validArg cl ∧ LENGTH cl < 256 * 256 /\ cl <> []`;
+Definition wfcl_def:
+  wfcl cl <=> EVERY validArg cl ∧ LENGTH cl < 256 * 256 /\ cl <> []
+End
 
-val COMMANDLINE_def = Define `
+Definition COMMANDLINE_def:
   COMMANDLINE cl =
-    IOx cl_ffi_part cl * &wfcl cl`
+    IOx cl_ffi_part cl * &wfcl cl
+End
 
 val set_thm =
   COMMANDLINE_def
@@ -276,8 +278,9 @@ QED
 val tl_v_thm = fetch "ListProg" "tl_v_thm";
 val mlstring_tl_v_thm = tl_v_thm |> INST_TYPE [alpha |-> mlstringSyntax.mlstring_ty]
 
-val name_def = Define `
-  name () = (\cl. (M_success (HD cl), cl))`;
+Definition name_def:
+  name () = (\cl. (M_success (HD cl), cl))
+End
 
 Theorem EvalM_name:
    Eval env exp (UNIT_TYPE u) /\
@@ -307,8 +310,9 @@ Proof
   \\ Cases_on `cl` \\ rw[TL_DEF]
 QED
 
-val arguments_def = Define `
-  arguments () = (\cl. (M_success (TL cl), cl))`
+Definition arguments_def:
+  arguments () = (\cl. (M_success (TL cl), cl))
+End
 
 Theorem EvalM_arguments:
    Eval env exp (UNIT_TYPE u) /\

basis/HashtableProofScript.sml

@@ -19,58 +19,68 @@ val hashtable_st = get_ml_prog_state();
 (* the vlv list contains the buckets *)
 (* each bucket only contains keys that hash there *)
 
-val hash_key_set_def = Define`
-  hash_key_set hf length idx  = { k' | hf k' MOD length = idx }`;
+Definition hash_key_set_def:
+  hash_key_set hf length idx  = { k' | hf k' MOD length = idx }
+End
 
-val bucket_ok_def = Define `
+Definition bucket_ok_def:
 bucket_ok b hf idx length  = !k v.
-      (mlmap$lookup b k = SOME v ==> k ∈ (hash_key_set hf length idx))`;
+      (mlmap$lookup b k = SOME v ==> k ∈ (hash_key_set hf length idx))
+End
 
-val buckets_empty_def = Define `
-  buckets_empty bs = (MAP mlmap$to_fmap bs = (REPLICATE (LENGTH bs) FEMPTY))`;
+Definition buckets_empty_def:
+  buckets_empty bs = (MAP mlmap$to_fmap bs = (REPLICATE (LENGTH bs) FEMPTY))
+End
 
 
-val buckets_to_fmap_def = Define `
-  buckets_to_fmap xs = alist_to_fmap (FLAT (MAP mlmap$toAscList xs))`;
+Definition buckets_to_fmap_def:
+  buckets_to_fmap xs = alist_to_fmap (FLAT (MAP mlmap$toAscList xs))
+End
 
-val list_union_def = Define `
+Definition list_union_def:
   list_union [x] = x /\
-  list_union (x::xs) = mlmap$union x (list_union xs)`;
+  list_union (x::xs) = mlmap$union x (list_union xs)
+End
 
-val buckets_ok_def = Define `
+Definition buckets_ok_def:
    buckets_ok bs hf =
      !i. i < LENGTH bs ==>
-       bucket_ok (EL i bs) hf i (LENGTH bs)`;
+       bucket_ok (EL i bs) hf i (LENGTH bs)
+End
 
-val hashtable_inv_def = Define `
+Definition hashtable_inv_def:
   hashtable_inv a b hf cmp (h:('a|->'b)) vlv =
     ?buckets.
       h = to_fmap (list_union buckets) /\
       buckets_ok buckets hf /\
       0 <> (LENGTH vlv)  /\
       LIST_REL (MAP_TYPE a b) buckets vlv /\
       EVERY mlmap$map_ok buckets /\
-      EVERY (\t. mlmap$cmp_of t = cmp) buckets`;
+      EVERY (\t. mlmap$cmp_of t = cmp) buckets
+End
 
 
 
-val REF_NUM_def = Define `
+Definition REF_NUM_def:
   REF_NUM loc n =
-    SEP_EXISTS v. REF loc v * & (NUM n v)`;
+    SEP_EXISTS v. REF loc v * & (NUM n v)
+End
 
-val REF_ARRAY_def = Define `
-  REF_ARRAY loc arr content = REF loc arr * ARRAY arr content`;
+Definition REF_ARRAY_def:
+  REF_ARRAY loc arr content = REF loc arr * ARRAY arr content
+End
 
-val HASHTABLE_def = Define
- `HASHTABLE a b hf cmp h v =
+Definition HASHTABLE_def:
+  HASHTABLE a b hf cmp h v =
     SEP_EXISTS ur ar hfv vlv arr cmpv heuristic_size.
       &(v = (Conv hashtable_con_stamp [ur; ar; hfv; cmpv]) /\
         (a --> NUM) hf hfv /\
         (a --> a --> ORDERING_TYPE) cmp cmpv /\
         TotOrd cmp /\
         hashtable_inv a b hf cmp h vlv) *
       REF_NUM ur heuristic_size *
-      REF_ARRAY ar arr vlv`;
+      REF_ARRAY ar arr vlv
+End
 
 Theorem hashtable_initBuckets_spec:
   !a b n nv cmp cmpv.

basis/ListProgScript.sml

@@ -399,12 +399,14 @@ val _ =  ml_prog_update (close_module NONE);
 
 val _ = ml_prog_update (open_module "Alist");
 
-val FMAP_EQ_ALIST_def = Define `
-  FMAP_EQ_ALIST f l <=> (ALOOKUP l = FLOOKUP f)`;
+Definition FMAP_EQ_ALIST_def:
+  FMAP_EQ_ALIST f l <=> (ALOOKUP l = FLOOKUP f)
+End
 
-val FMAP_TYPE_def = Define `
+Definition FMAP_TYPE_def:
   FMAP_TYPE (a:'a -> v -> bool) (b:'b -> v -> bool) (f:'a|->'b) =
-    \v. ?l. LIST_TYPE (PAIR_TYPE a b) l v /\ FMAP_EQ_ALIST f l`;
+    \v. ?l. LIST_TYPE (PAIR_TYPE a b) l v /\ FMAP_EQ_ALIST f l
+End
 
 val _ = add_type_inv ``FMAP_TYPE (a:'a -> v -> bool) (b:'b -> v -> bool)``
                      ``:('a # 'b) list``;
@@ -422,7 +424,9 @@ val Eval_FLOOKUP = Q.prove(
   |> add_user_proved_v_thm;
 
 val _ = next_ml_names := ["update"];
-val AUPDATE_def = Define `AUPDATE l (x:'a,y:'b) = (x,y)::l`;
+Definition AUPDATE_def:
+  AUPDATE l (x:'a,y:'b) = (x,y)::l
+End
 val AUPDATE_eval = translate AUPDATE_def;
 
 val FMAP_EQ_ALIST_UPDATE = Q.prove(
@@ -454,12 +458,15 @@ val Eval_FEMPTY = Q.prove(
   |> MATCH_MP (MATCH_MP Eval_WEAKEN NIL_eval)
   |> add_eval_thm;
 
-val AEVERY_AUX_def = Define `
+Definition AEVERY_AUX_def:
   (AEVERY_AUX aux P [] = T) /\
   (AEVERY_AUX aux P ((x:'a,y:'b)::xs) =
      if MEMBER x aux then AEVERY_AUX aux P xs else
-       P (x,y) /\ AEVERY_AUX (x::aux) P xs)`;
-val AEVERY_def = Define `AEVERY = AEVERY_AUX []`;
+       P (x,y) /\ AEVERY_AUX (x::aux) P xs)
+End
+Definition AEVERY_def:
+  AEVERY = AEVERY_AUX []
+End
 val _ = next_ml_names := ["every","every"];
 val _ = translate AEVERY_AUX_def;
 val AEVERY_eval = translate AEVERY_def;
@@ -494,9 +501,10 @@ val Eval_FEVERY = Q.prove(
   |> add_user_proved_v_thm;
 
 val _ = next_ml_names := ["map"];
-val AMAP_def = Define `
+Definition AMAP_def:
   (AMAP f [] = []) /\
-  (AMAP f ((x:'a,y:'b)::xs) = (x,(f y):'c) :: AMAP f xs)`;
+  (AMAP f ((x:'a,y:'b)::xs) = (x,(f y):'c) :: AMAP f xs)
+End
 val AMAP_eval = translate AMAP_def;
 
 val ALOOKUP_AMAP = Q.prove(
@@ -551,9 +559,10 @@ val Eval_FUNION = Q.prove(
   |> add_user_proved_v_thm;
 
 val _ = next_ml_names := ["delete"];
-val ADEL_def = Define `
+Definition ADEL_def:
   (ADEL [] z = []) /\
-  (ADEL ((x:'a,y:'b)::xs) z = if x = z then ADEL xs z else (x,y)::ADEL xs z)`
+  (ADEL ((x:'a,y:'b)::xs) z = if x = z then ADEL xs z else (x,y)::ADEL xs z)
+End
 val ADEL_eval = translate ADEL_def;
 
 val ALOOKUP_ADEL = Q.prove(

basis/MarshallingScript.sml

@@ -8,23 +8,27 @@ val _ = new_theory "Marshalling";
 
 (* encode/decode nums as 2 or 8 bytes *)
 (* similar to n2l & l2n but with padding *)
-val n2w2_def = Define`
-  n2w2 (i : num) : word8 list = [n2w (i DIV 256); n2w i]`
+Definition n2w2_def:
+  n2w2 (i : num) : word8 list = [n2w (i DIV 256); n2w i]
+End
 
-val n2w8_def = Define`
+Definition n2w8_def:
   n2w8 (i : num) : word8 list =
    [n2w (i DIV 256**7); n2w (i DIV 256**6);
     n2w (i DIV 256**5); n2w (i DIV 256**4);
     n2w (i DIV 256**3); n2w (i DIV 256**2);
-    n2w (i DIV 256); n2w i]`
+    n2w (i DIV 256); n2w i]
+End
 
-val w22n_def = Define`
-  w22n ([b1; b0] : word8 list) = w2n b1 * 256 + w2n b0`
+Definition w22n_def:
+  w22n ([b1; b0] : word8 list) = w2n b1 * 256 + w2n b0
+End
 
-val w82n_def = Define`
+Definition w82n_def:
   w82n ([b7; b6; b5; b4; b3; b2; b1; b0] : word8 list) =
   256 * ( 256 * ( 256 * ( 256 * ( 256 * ( 256 * ( 256 *
-  w2n b7 + w2n b6) + w2n b5) + w2n b4) + w2n b3) + w2n b2) + w2n b1) + w2n b0`
+  w2n b7 + w2n b6) + w2n b5) + w2n b4) + w2n b3) + w2n b2) + w2n b1) + w2n b0
+End
 
 Theorem w22n_n2w2:
    !i. i < 2**(2*8) ==> w22n (n2w2 i) = i

basis/RatProgScript.sml

@@ -34,17 +34,19 @@ val _ = ml_prog_update (add_dec
 
 (* refinement invariants *)
 
-val RAT_TYPE_def = Define `
+Definition RAT_TYPE_def:
   RAT_TYPE (r:rat) =
     \v. ?(n:int) (d:num). (r = (rat_of_int n) / &d) /\
                           gcd (Num (ABS n)) d = 1 /\ d <> 0 /\
-                          RATIONAL_TYPE (RatPair n d) v`;
+                          RATIONAL_TYPE (RatPair n d) v
+End
 
 val _ = add_type_inv ``RAT_TYPE`` ``:rational``;
 
-val REAL_TYPE_def = Define `
+Definition REAL_TYPE_def:
   REAL_TYPE (r:real) =
-    \v. ?x:rat. RAT_TYPE x v /\ (real_of_rat x = r)`;
+    \v. ?x:rat. RAT_TYPE x v /\ (real_of_rat x = r)
+End
 
 val _ = add_type_inv ``REAL_TYPE`` ``:rational``;
 
@@ -160,8 +162,9 @@ val Eval_REAL_NUM = Q.prove(
   \\ pop_assum $ qspec_then ‘&x’ mp_tac \\ fs [])
   |> add_user_proved_v_thm;
 
-val pair_le_def = Define `
-  pair_le (RatPair n1 d1) (RatPair n2 d2) = (n1 * & d2 <= n2 * (& d1):int)`;
+Definition pair_le_def:
+  pair_le (RatPair n1 d1) (RatPair n2 d2) = (n1 * & d2 <= n2 * (& d1):int)
+End
 
 val _ = next_ml_names := ["<="];
 val pair_le_v_thm = translate pair_le_def;
@@ -209,8 +212,9 @@ val Eval_REAL_GE = Q.prove(
   |> (fn th => MATCH_MP th Eval_RAT_GE)
   |> add_user_proved_v_thm;
 
-val pair_lt_def = Define `
-  pair_lt (RatPair n1 d1) (RatPair n2 d2) = (n1 * & d2 < n2 * (& d1):int)`;
+Definition pair_lt_def:
+  pair_lt (RatPair n1 d1) (RatPair n2 d2) = (n1 * & d2 < n2 * (& d1):int)
+End
 
 val _ = next_ml_names := ["<"];
 val pair_lt_v_thm = translate pair_lt_def;
@@ -256,16 +260,18 @@ val Eval_REAL_GT = Q.prove(
   |> (fn th => MATCH_MP th Eval_RAT_GT)
   |> add_user_proved_v_thm;
 
-val pair_compare_def = Define `
+Definition pair_compare_def:
   pair_compare (RatPair n1 d1) (RatPair n2 d2) =
     let x1 = n1 * & d2 in
     let x2 = n2 * & d1 in
       if x1 < x2 then Less else
-      if x2 < x1 then Greater else Equal`
+      if x2 < x1 then Greater else Equal
+End
 
-val rat_compare_def = Define `
+Definition rat_compare_def:
   rat_compare (r1:rat) r2 =
-    if r1 < r2 then Less else if r2 < r1 then Greater else Equal`
+    if r1 < r2 then Less else if r2 < r1 then Greater else Equal
+End
 
 val _ = next_ml_names := ["compare"];
 val pair_compare_v_thm = translate pair_compare_def;
@@ -410,9 +416,10 @@ val PAIR_TYPE_IMP_RAT_TYPE = prove(
        integerTheory.INT_ABS_NUM, rat_of_int_ainv] >>
   simp[RAT_MUL_NUM_CALCULATE]);
 
-val pair_add_def = Define `
+Definition pair_add_def:
   pair_add (RatPair n1 d1) (RatPair n2 d2) =
-    div_gcd ((n1 * &d2) + (n2 * &d1)) (d1 * d2)`;
+    div_gcd ((n1 * &d2) + (n2 * &d1)) (d1 * d2)
+End
 
 val _ = next_ml_names := ["+"];
 val pair_add_v_thm = translate pair_add_def;
@@ -454,9 +461,10 @@ val Eval_REAL_ADD = Q.prove(
   |> (fn th => MATCH_MP th Eval_RAT_ADD)
   |> add_user_proved_v_thm;
 
-val pair_sub_def = Define `
+Definition pair_sub_def:
   pair_sub (RatPair n1 d1) (RatPair n2 d2) =
-    div_gcd ((n1 * &d2) - (n2 * &d1)) (d1 * d2)`;
+    div_gcd ((n1 * &d2) - (n2 * &d1)) (d1 * d2)
+End
 
 val _ = next_ml_names := ["-"];
 val pair_sub_v_thm = translate pair_sub_def;
@@ -509,8 +517,9 @@ val Eval_REAL_NEG = Q.prove(
   |> (fn th => MATCH_MP th Eval_RAT_NEG)
   |> add_user_proved_v_thm;
 
-val pair_mul_def = Define `
-  pair_mul (RatPair n1 d1) (RatPair n2 d2) = div_gcd (n1 * n2:int) (d1 * d2:num)`;
+Definition pair_mul_def:
+  pair_mul (RatPair n1 d1) (RatPair n2 d2) = div_gcd (n1 * n2:int) (d1 * d2:num)
+End
 
 val _ = next_ml_names := ["*"];
 val pair_mul_v_thm = translate pair_mul_def;
@@ -546,9 +555,10 @@ val Eval_REAL_MUL = Q.prove(
   |> (fn th => MATCH_MP th Eval_RAT_MUL)
   |> add_user_proved_v_thm;
 
-val pair_inv_def = Define `
+Definition pair_inv_def:
   pair_inv (RatPair n1 d1) =
-    (RatPair (if n1 < 0 then - & d1 else (& d1):int) (num_of_int n1))`;
+    (RatPair (if n1 < 0 then - & d1 else (& d1):int) (num_of_int n1))
+End
 
 val _ = next_ml_names := ["inv"];
 val pair_inv_v_thm = translate pair_inv_def;