Add some theorems about dropWhile

src/list/src/listScript.sml

@@ -4734,6 +4734,16 @@ val EL_LENGTH_dropWhile_REVERSE = Q.store_thm("EL_LENGTH_dropWhile_REVERSE",
    >> fs [NOT_EVERY, dropWhile_APPEND_EXISTS, arithmeticTheory.ADD1])
 end
 
+Theorem dropWhile_id:
+ (dropWhile P ls = ls) <=> NULL ls \/ ~P(HD ls)
+Proof
+  Cases_on`ls` \\ rw[dropWhile_def, NULL]
+  \\ disch_then(mp_tac o Q.AP_TERM`LENGTH`)
+  \\ Q.MATCH_GOALSUB_RENAME_TAC`dropWhile P l`
+  \\ Q.SPECL_THEN[`P`,`l`]mp_tac LENGTH_dropWhile_LESS_EQ
+  \\ simp[]
+QED
+
 val IMP_EVERY_LUPDATE = store_thm("IMP_EVERY_LUPDATE",
   “!xs h i. P h /\ EVERY P xs ==> EVERY P (LUPDATE h i xs)”,
   Induct THEN fs [LUPDATE_def] THEN REPEAT STRIP_TAC

src/list/src/rich_listScript.sml

@@ -8,7 +8,7 @@ open HolKernel Parse boolLib BasicProvers;
 open numLib metisLib simpLib combinTheory arithmeticTheory prim_recTheory
      pred_setTheory listTheory pairTheory markerLib TotalDefn;
 
-local open listSimps pred_setSimps in end;
+local open listSimps pred_setSimps dep_rewrite in end;
 
 val FILTER_APPEND = FILTER_APPEND_DISTRIB
 val REVERSE = REVERSE_SNOC_DEF
@@ -3783,6 +3783,26 @@ Proof
 QED
 (* END more lemmas of IS_SUFFIX *)
 
+Theorem IS_SUFFIX_dropWhile:
+  IS_SUFFIX ls (dropWhile P ls)
+Proof
+  Induct_on`ls`
+  \\ rw[IS_SUFFIX_CONS]
+QED
+
+Theorem LENGTH_dropWhile_id:
+  (LENGTH (dropWhile P ls) = LENGTH ls) <=> (dropWhile P ls = ls)
+Proof
+  rw[EQ_IMP_THM]
+  \\ rw[dropWhile_id]
+  \\ Cases_on`ls` \\ fs[]
+  \\ strip_tac \\ fs[]
+  \\ `IS_SUFFIX t (dropWhile P t)` by simp[IS_SUFFIX_dropWhile]
+  \\ fs[IS_SUFFIX_APPEND]
+  \\ `LENGTH t = LENGTH l + LENGTH (dropWhile P t)` by metis_tac[LENGTH_APPEND]
+  \\ fs[]
+QED
+
 Theorem nub_GENLIST:
   nub (GENLIST f n) =
     MAP f (FILTER (\i. !j. (i < j) /\ (j < n) ==> f i <> f j) (COUNT_LIST n))