lib: add length_tail_nonempty

Signed-off-by: Michael McInerney <[email protected]>
seL4 · Feb 20, 2024 · 66b399a · 66b399a
1 parent dce36cc
commit 66b399a
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/lib/Lib.thy b/lib/Lib.thy
@@ -2617,6 +2617,10 @@ lemma list_not_last:
   "Suc 0 < length ls \<Longrightarrow> ls \<noteq> [last ls]"
   by (cases ls; clarsimp)
 
+lemma length_tail_nonempty:
+  "Suc 0 < length list \<Longrightarrow> tl list \<noteq> []"
+  by (cases list, simp, simp)
+
 text \<open>Prevent clarsimp and others from creating Some from not None by folding this and unfolding
   again when safe.\<close>