Remove list_max for #1122 in examples

CakeML · Jan 26, 2025 · c00a373 · c00a373
1 parent bbdadb9
commit c00a373
Show file tree

Hide file tree

Showing 4 changed files with 17 additions and 11 deletions.
diff --git a/examples/lpr_checker/array/lpr_arrayProgScript.sml b/examples/lpr_checker/array/lpr_arrayProgScript.sml
@@ -1120,7 +1120,7 @@ QED
 
 val _ = translate safe_hd_def;
 
-val _ = translate list_max_def;
+val _ = translate MAX_LIST_def;
 val _ = translate list_max_index_def;
 
 (* bump up the length to a large number *)
@@ -1406,7 +1406,9 @@ Theorem list_max_index_bounded_clause:
   EVERY ($> n o index) l ∧ EVERY ($> n o index o $~) l
 Proof
   simp[list_max_index_def]>>
-  Induct>>rw[list_max_def,index_def]>>
+  Induct>>rw[] >>
+  fs[MAX_LIST_def,MAX_DEF,index_def]>>
+  rw[] >>
   intLib.ARITH_TAC
 QED
 
@@ -1440,8 +1442,8 @@ Theorem EVERY_index_resize_Clist:
 Proof
   rw[]>>
   simp[resize_Clist_def,list_max_index_def]>>
-  qmatch_goalsub_abbrev_tac`list_max lss`>>
-  qspec_then `lss` assume_tac list_max_max>>
+  qmatch_goalsub_abbrev_tac`MAX_LIST lss`>>
+  qspec_then `lss` assume_tac MAX_LIST_PROPERTY>>
   fs[EVERY_MEM,Abbr`lss`,MEM_MAP,PULL_EXISTS]>>
   ntac 2 strip_tac>>first_x_assum drule>>
   rw[]>>simp[index_def]>>rw[]>>

diff --git a/examples/lpr_checker/array/lpr_listScript.sml b/examples/lpr_checker/array/lpr_listScript.sml
@@ -302,8 +302,9 @@ Definition safe_hd_def:
   safe_hd ls = case ls of [] => (0:int) | (x::xs) => x
 End
 
+(*Might want to rename to MAX_LIST_index*)
 Definition list_max_index_def:
-  list_max_index C = 2*list_max (MAP (λc. Num (ABS c)) C) + 1
+  list_max_index C = 2*MAX_LIST (MAP (λc. Num (ABS c)) C) + 1
 End
 
 (* bump up the length to a large number *)

diff --git a/examples/xlrup_checker/array/xlrup_arrayProgScript.sml b/examples/xlrup_checker/array/xlrup_arrayProgScript.sml
@@ -1263,7 +1263,7 @@ Proof
   simp[LIST_REL_REPLICATE_same,OPTION_TYPE_def]
 QED
 
-val _ = translate list_max_def;
+val _ = translate MAX_LIST_def;
 val _ = translate list_max_index_def;
 
 (* bump up the length to a large number *)
@@ -1738,8 +1738,10 @@ Theorem list_max_index_bounded_clause:
   EVERY ($> n o index) l ∧ EVERY ($> n o index o $~) l
 Proof
   simp[list_max_index_def]>>
-  Induct>>rw[list_max_def,index_def]>>
-  intLib.ARITH_TAC
+  Induct>>rw[] >>
+  fs[MAX_LIST_def,MAX_DEF,index_def]>>
+  rw[] >>
+  intLib.COOPER_TAC
 QED
 
 Theorem bounded_cfml_update_resize:
@@ -1772,8 +1774,8 @@ Theorem EVERY_index_resize_Clist:
 Proof
   rw[]>>
   simp[resize_Clist_def,list_max_index_def]>>
-  qmatch_goalsub_abbrev_tac`list_max lss`>>
-  qspec_then `lss` assume_tac list_max_max>>
+  qmatch_goalsub_abbrev_tac`MAX_LIST lss`>>
+  qspec_then `lss` assume_tac MAX_LIST_PROPERTY>>
   fs[EVERY_MEM,Abbr`lss`,MEM_MAP,PULL_EXISTS]>>
   ntac 2 strip_tac>>first_x_assum drule>>
   rw[]>>simp[index_def]>>rw[]>>

diff --git a/examples/xlrup_checker/array/xlrup_listScript.sml b/examples/xlrup_checker/array/xlrup_listScript.sml
@@ -162,8 +162,9 @@ Definition list_delete_list_def:
     else list_delete_list is (LUPDATE NONE i fml))
 End
 
+(*Might want to rename to MAX_LIST_index*)
 Definition list_max_index_def:
-  list_max_index C = 2*list_max (MAP (λc. Num (ABS c)) C) + 1
+  list_max_index C = 2* MAX_LIST (MAP (λc. Num (ABS c)) C) + 1
 End
 
 (* bump up the length to a large number *)