From c00a37373f09dd2dfde04fed2a6e76f74cf9012c Mon Sep 17 00:00:00 2001
From: ordinarymath <ordinarymath@yahoo.com>
Date: Sun, 26 Jan 2025 11:35:04 +0000
Subject: [PATCH] Remove list_max for #1122 in examples

---
 examples/lpr_checker/array/lpr_arrayProgScript.sml   | 10 ++++++----
 examples/lpr_checker/array/lpr_listScript.sml        |  3 ++-
 .../xlrup_checker/array/xlrup_arrayProgScript.sml    | 12 +++++++-----
 examples/xlrup_checker/array/xlrup_listScript.sml    |  3 ++-
 4 files changed, 17 insertions(+), 11 deletions(-)

diff --git a/examples/lpr_checker/array/lpr_arrayProgScript.sml b/examples/lpr_checker/array/lpr_arrayProgScript.sml
index 80d542b8f7..053f182624 100644
--- 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
index 464b5ecfe6..6b4e0239f2 100644
--- 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
index fa4847986e..5967cf876b 100644
--- 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
index 3745392061..aec0065cb7 100644
--- 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 *)