Replace cv_sum_depth by cv_size (and delete cv_size_alt)

examples/bootstrap/compiler_funs_cvScript.sml

@@ -1,7 +1,7 @@
 
 open HolKernel Parse boolLib bossLib term_tactic cv_transLib cv_stdTheory;
 open arithmeticTheory listTheory pairTheory finite_mapTheory stringTheory;
-open wordsTheory wordsLib automationLib printingTheory;
+open wordsTheory wordsLib printingTheory codegenTheory;
 
 val _ = new_theory "compiler_funs_cv";
 
@@ -12,8 +12,8 @@ val res = cv_auto_trans codegenTheory.c_pops_def;
 
 val res = cv_auto_trans_pre_rec codegenTheory.c_exp_def
  (WF_REL_TAC ‘inv_image (measure I LEX measure I)
-    (λx. case x of INL (t,l,vs,fs,x) => (cv_sum_depth x, cv$c2n t)
-                 | INR (l,vs,fs,xs) => (cv_sum_depth xs, 0))’
+    (λx. case x of INL (t,l,vs,fs,x) => (cv_size x, cv$c2n t)
+                 | INR (l,vs,fs,xs) => (cv_size xs, 0))’
   \\ rpt strip_tac
   \\ (Cases_on ‘cv_z’ ORELSE Cases_on ‘cv_zs’) \\ gvs []
   \\ gvs [cvTheory.c2b_def]
@@ -34,7 +34,7 @@ Proof
 QED
 
 val pre = cv_trans_pre_rec printingTheory.num2str_def
-  (WF_REL_TAC ‘measure cv_sum_depth’ \\ Cases \\ gvs [] \\ rw [] \\ gvs []);
+  (WF_REL_TAC ‘measure cv_size’ \\ Cases \\ gvs [] \\ rw [] \\ gvs []);
 
 Theorem num2str_pre[cv_pre]:
   ∀n. num2str_pre n
@@ -82,8 +82,8 @@ val _ = cv_trans printingTheory.dest_list_def;
 Theorem cv_dest_list_size:
   ∀v x y.
     cv_dest_list v = Pair x y ⇒
-    cv_sum_depth x <= cv_sum_depth v ∧
-    cv_sum_depth y <= cv_sum_depth v
+    cv_size x <= cv_size v ∧
+    cv_size y <= cv_size v
 Proof
   recInduct (fetch "-" "cv_dest_list_ind") \\ rw []
   \\ cv_termination_tac \\ gvs [ADD1]
@@ -97,8 +97,8 @@ val v2pretty_eq =
   CONJ (printingTheory.v2pretty_def |> SRULE [GSYM vs2pretty_def]) vs2pretty_thm;
 
 val pre = cv_auto_trans_pre_rec v2pretty_eq
-  (WF_REL_TAC ‘measure $ λx. case x of INL v => cv_sum_depth v
-                                     | INR v => cv_sum_depth v’
+  (WF_REL_TAC ‘measure $ λx. case x of INL v => cv_size v
+                                     | INR v => cv_size v’
    \\ rw [] \\ cv_termination_tac
    \\ qpat_x_assum ‘cv_dest_list _ = _’ mp_tac
    \\ simp [Once $ fetch "-" "cv_dest_list_def"] \\ rw [] \\ gvs []
@@ -147,9 +147,9 @@ QED
 
 val pre = cv_auto_trans_pre_rec exp2v_def
   (WF_REL_TAC ‘measure $ λx. case x of
-                             | INL v => cv_sum_depth v + 1
-                             | INR (INL v) => cv_sum_depth v + 1
-                             | INR (INR v) => cv_sum_depth v’
+                             | INL v => cv_size v + 1
+                             | INR (INL v) => cv_size v + 1
+                             | INR (INR v) => cv_size v’
    \\ cv_termination_tac \\ cheat);
 
 Theorem exp2v_pre[cv_pre]:

examples/cv_compute/examplesScript.sml

@@ -60,8 +60,8 @@ Definition factc_def:
           (Num 1)
           (cv_mul n (factc (cv_sub n (Num 1))))
 Termination
-  WF_REL_TAC `measure cv_size_alt`
-  \\ Cases \\ simp [cv_size_alt_def, CaseEq "bool", c2b_def]
+  WF_REL_TAC `measure cv_size`
+  \\ Cases \\ simp [CaseEq "bool", c2b_def]
 End
 
 Theorem factc_is_fact:
@@ -109,9 +109,9 @@ Definition isprimec_aux_def:
                  (Num 0))
           (Num 1)
 Termination
-  WF_REL_TAC `measure (\(dvs,n). cv_size_alt (cv_sub n dvs))`
+  WF_REL_TAC `measure (\(dvs,n). cv_size (cv_sub n dvs))`
   \\ Induct \\ simp [PULL_EXISTS, c2b_def]
-  \\ Cases_on `dvs` \\ gs [cv_size_alt_def] \\ rw [] \\ gs []
+  \\ Cases_on `dvs` \\ gs [] \\ rw [] \\ gs []
 End
 
 Definition isprimec_def:
@@ -135,8 +135,8 @@ Definition primes_uptoc_def:
                         (primes_uptoc (cv_sub upto (Num 1))))
                  (Num 0))
 Termination
-  WF_REL_TAC `measure cv_size_alt`
-  \\ conj_tac \\ Cases \\ simp [cv_size_alt_def, c2b_def]
+  WF_REL_TAC `measure cv_size`
+  \\ conj_tac \\ Cases \\ simp [cv_size_def, c2b_def]
 End
 
 (* Here are the corresponding HOL functions, and a proof they compute values

src/num/theories/cvScript.sml

@@ -198,7 +198,7 @@ Overload case = “cv_CASE”
 val cv_size_def = Prim_rec.new_recursive_definition {
   name = "cv_size_def",
   rec_axiom = cv_Axiom,
-  def = “cv_size (Num n) = 1 + n /\
+  def = “cv_size (Num n) = n /\
          cv_size (Pair c d) = 1 + (cv_size c + cv_size d)”};
 
 val _ = TypeBase.export (
@@ -217,7 +217,7 @@ val cv_snd_def = recdef("cv_snd_def",
 val cv_ispair_def = recdef("cv_ispair_def",
                            “cv_ispair (Pair p q) = Num (SUC 0) /\
                             cv_ispair (Num m) = Num 0”);
-val _ = export_rewrites ["cv_fst_def", "cv_snd_def", "cv_ispair_def"];
+val _ = export_rewrites ["cv_fst_def", "cv_snd_def", "cv_ispair_def", "cv_size_def"];
 
 val b2c_def = Prim_rec.new_recursive_definition{
   def = “b2c T = Num (SUC 0) /\ b2c F = Num 0”,
@@ -332,11 +332,6 @@ Proof
   simp [cv_eq_def0]
 QED
 
-
-val cv_size_alt_def = recdef("cv_size_alt_def",
-  “(cv_size_alt (Num n) = n) /\
-   (cv_size_alt (Pair p q) = 1 + cv_size_alt p + cv_size_alt q)”);
-
 (* -------------------------------------------------------------------------
  * Extra characteristic theorems
  * ------------------------------------------------------------------------- *)

src/num/theories/cv_compute/automation/cv_miscLib.sig

@@ -15,8 +15,8 @@ sig
   val is_cv_rep : term -> bool
   val is_cv_proj : term -> bool
   val dest_cv_proj : term -> term * term
-  val cv_sum_depth_tm : term
-  val mk_cv_sum_depth : term -> term
+  val cv_size_tm : term
+  val mk_cv_size : term -> term
 
   val contains_fun_ty : hol_type -> bool
 

src/num/theories/cv_compute/automation/cv_miscLib.sml

@@ -35,9 +35,9 @@ fun is_cv_proj tm = let
 fun dest_cv_proj tm =
   if is_cv_proj tm then (rand (rator tm), rand tm) else failwith "dest_cv_proj";
 
-val cv_sum_depth_tm = cv_sum_depth_def |> CONJUNCT1 |> SPEC_ALL
+val cv_size_tm = cv_size_def |> CONJUNCT1 |> SPEC_ALL
                         |> concl |> dest_eq |> fst |> repeat rator;
-fun mk_cv_sum_depth tm = mk_comb(cv_sum_depth_tm, tm);
+fun mk_cv_size tm = mk_comb(cv_size_tm, tm);
 
 val remove_fupd_conv = let
   fun rpt_ABS_CONV c tm =

src/num/theories/cv_compute/automation/cv_repScript.sml

@@ -86,25 +86,20 @@ Proof
   strip_tac \\ fs [FUN_EQ_THM] \\ Cases \\ fs []
 QED
 
-Definition cv_sum_depth_def[simp]:
-  cv_sum_depth (Num n) = n /\
-  cv_sum_depth (Pair x y) = 1 + cv_sum_depth x + cv_sum_depth y
-End
-
 Definition cv_proj_def:
   cv_proj [] v = v /\
   cv_proj (T::xs) v = cv_fst (cv_proj xs v) /\
   cv_proj (F::xs) v = cv_snd (cv_proj xs v)
 End
 
 Theorem cv_proj_less_eq:
-  !v xs. cv_sum_depth (cv_proj xs v) <= cv_sum_depth v
+  !v xs. cv_size (cv_proj xs v) <= cv_size v
 Proof
   gen_tac \\ Induct \\ gvs [cv_proj_def]
   \\ Cases \\ gvs [cv_proj_def] \\ rw []
   \\ irule arithmeticTheory.LESS_EQ_TRANS
   \\ pop_assum $ irule_at (Pos last)
-  \\ Cases_on ‘cv_proj xs v’ \\ gvs [cv_sum_depth_def]
+  \\ Cases_on ‘cv_proj xs v’ \\ gvs []
 QED
 
 Theorem to_cv_proj:

src/num/theories/cv_compute/automation/cv_stdScript.sml

@@ -288,7 +288,7 @@ Definition cv_map_fst_def:
       (Pair (cv_fst (cv_fst cv)) (cv_map_fst (cv_snd cv)))
       (Num 0)
 Termination
-  WF_REL_TAC `measure cv_sum_depth` >> cv_termination_tac
+  WF_REL_TAC ‘measure cv_size’ >> cv_termination_tac
 End
 
 Theorem cv_MAP_FST[cv_rep]:
@@ -305,7 +305,7 @@ Definition cv_map_snd_def:
       (Pair (cv_snd (cv_fst cv)) (cv_map_snd (cv_snd cv)))
       (Num 0)
 Termination
-  WF_REL_TAC `measure cv_sum_depth` >> cv_termination_tac
+  WF_REL_TAC ‘measure cv_size’ >> cv_termination_tac
 End
 
 Theorem cv_MAP_SND[cv_rep]:

src/num/theories/cv_compute/automation/cv_transLib.sml

@@ -42,7 +42,7 @@ fun make_measures alts = let
   fun process (combs,nargs) = let
     val input = mk_var("input",cvs_ty nargs)
     fun each combs = let
-      val ys = map (fn i => mk_cv_sum_depth (access i nargs input)) combs
+      val ys = map (fn i => mk_cv_size (access i nargs input)) combs
       in mk_abs(input,mk_sum_term ys) end
     in map each combs end
   fun combine x y = let