Adjust list theorems to return to previous quantification order

Keep existing definitions, using _def suffix, and make APPEND and EL be theorems with old variable order. The introduction of EL_def seems to confuse cv_trans_pre when applied to EL, so I changed that to just work over EL_def instead. Fixes regression in holfoot example, and other code that may be assuming that these rather fundamental theorems aren't going to change in their expression.
HOL-Theorem-Prover · Nov 26, 2024 · c9c025c · c9c025c
1 parent d2da44b
commit c9c025c
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 4 deletions.
diff --git a/src/list/src/ListConv1.sml b/src/list/src/ListConv1.sml
@@ -286,7 +286,7 @@ local
   val l2v = mk_var("l2", listSyntax.mk_list_type alpha)
   val hv = mk_var("h", alpha)
   val (th1,th2) = CONJ_PAIR (listTheory.APPEND)
-  val th3 = SPECL [hv,l1v,l2v] th2
+  val th3 = SPECL [l1v,l2v,hv] th2
   val th4 = GENL  [l2v,l1v,hv] th3
       fun itfn (cns,ath) v th =
         let val th1 = AP_TERM (mk_comb(cns,v)) th

diff --git a/src/list/src/listScript.sml b/src/list/src/listScript.sml
@@ -146,7 +146,7 @@ Definition SUM:
   SUM (h::t) = h + SUM t
 End
 
-Definition APPEND[simp]:
+Definition APPEND_def:
   APPEND [] l = l /\
   APPEND (h::l1) l2 = h::APPEND l1 l2
 End
@@ -157,6 +157,14 @@ val _ = Unicode.unicode_version {u = UnicodeChars.doubleplus, tmnm = "++"}
 val _ = TeX_notation { hol = UnicodeChars.doubleplus,
                        TeX = ("\\HOLTokenDoublePlus", 1) }
 
+(* preserving old choice of quantification order *)
+Theorem APPEND[simp]:
+  (!l:'a list.  APPEND [] l = l) /\
+  (!l1 l2 h:'a. APPEND (h::l1) l2 = h::(APPEND l1 l2))
+Proof
+  REWRITE_TAC[APPEND_def]
+QED
+
 Definition FLAT[simp]:
   FLAT []     = [] /\
   FLAT (h::t) = APPEND h (FLAT t)
@@ -219,11 +227,19 @@ Definition EXISTS_DEF[simp]:
   (EXISTS P (h::t) <=> P h \/ EXISTS P t)
 End
 
-Definition EL:
+Definition EL_def:
   EL 0 l = (HD l:'a) /\
   EL (SUC n) l = EL n (TL l)
 End
 
+(* preserving particular variable quantification order *)
+Theorem EL:
+  (!l.    EL 0 l = HD l:'a) /\
+  (!l n.  EL (SUC n) l = EL n (TL l))
+Proof
+  REWRITE_TAC[EL_def]
+QED
+
 (* ---------------------------------------------------------------------*)
 (* Definition of a function                                             *)
 (*                                                                      *)

diff --git a/src/num/theories/cv_compute/automation/cv_stdScript.sml b/src/num/theories/cv_compute/automation/cv_stdScript.sml
@@ -103,7 +103,7 @@ val res = cv_trans TAKE_def;
 
 val res = cv_trans DROP_def;
 
-val res = cv_trans_pre EL;
+val res = cv_trans_pre EL_def;
 
 Theorem EL_pre[cv_pre]:
   !n xs. EL_pre n xs <=> n < LENGTH xs