Adjust statements of TAKE_FRONT; make subterm_tpm[simp]

HOL-Theorem-Prover · Feb 22, 2024 · 49e3a90 · 49e3a90
1 parent f5e5217
commit 49e3a90
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/examples/lambda/barendregt/solvableScript.sml b/examples/lambda/barendregt/solvableScript.sml
@@ -633,7 +633,7 @@ Proof
  >> Q.EXISTS_TAC ‘tpm pi N’ >> rw []
 QED
 
-Theorem solvable_tpm :
+Theorem solvable_tpm[simp] :
     !pi M. solvable (tpm pi M) <=> solvable M
 Proof
     METIS_TAC [pmact_inverse, solvable_tpm_I]

diff --git a/src/list/src/rich_listScript.sml b/src/list/src/rich_listScript.sml
@@ -1179,14 +1179,14 @@ val TAKE_SNOC = Q.store_thm ("TAKE_SNOC",
    THEN ASM_REWRITE_TAC []);
 
 Theorem TAKE_FRONT :
-    !l n. l <> [] /\ n <= PRE (LENGTH l) ==> TAKE n (FRONT l) = TAKE n l
+    !l n. l <> [] /\ n < LENGTH l ==> TAKE n (FRONT l) = TAKE n l
 Proof
     HO_MATCH_MP_TAC SNOC_INDUCT
  >> CONJ_TAC >- SRW_TAC [][]
  >> RW_TAC arith_ss [FRONT_SNOC, LENGTH_SNOC]
  >> ONCE_REWRITE_TAC [EQ_SYM_EQ]
  >> MATCH_MP_TAC TAKE_SNOC
- >> ASM_REWRITE_TAC []
+ >> RW_TAC arith_ss []
 QED
 
 val SNOC_EL_TAKE = Q.store_thm ("SNOC_EL_TAKE",