lib: add heap_path_not_Nil to Heap_List

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
seL4 · Feb 11, 2025 · 2cc6de9 · 2cc6de9
1 parent 0cba8a6
commit 2cc6de9
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/lib/Heap_List.thy b/lib/Heap_List.thy
@@ -53,6 +53,10 @@ lemma heap_path_None[simp]:
   "heap_path hp None xs end = (xs = [] \<and> end = None)"
   by (cases xs, auto)
 
+lemma heap_path_not_Nil:
+  "heap_ls hp (Some st) ls \<Longrightarrow> ls \<noteq> []"
+  by fastforce
+
 lemma heap_ls_unique:
   "\<lbrakk> heap_ls hp x xs; heap_ls hp x ys \<rbrakk> \<Longrightarrow> xs = ys"
   by (induct xs arbitrary: ys x; simp) (case_tac ys; clarsimp)