From 74d8f98e85798e92520f234b6a688e27f7d8d128 Mon Sep 17 00:00:00 2001
From: Michael McInerney <michael.mcinerney@proofcraft.systems>
Date: Wed, 10 Jan 2024 10:54:38 +1030
Subject: [PATCH] lib: add defn of list_insert_before, and some lemmas

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
---
 lib/ListLibLemmas.thy | 26 ++++++++++++++++++++++++++
 lib/List_Lib.thy      |  6 ++++++
 2 files changed, 32 insertions(+)

diff --git a/lib/ListLibLemmas.thy b/lib/ListLibLemmas.thy
index bdb72d61f..fdb3ba42c 100644
--- a/lib/ListLibLemmas.thy
+++ b/lib/ListLibLemmas.thy
@@ -371,6 +371,32 @@ lemma list_insert_after_after:
   apply fastforce
   done
 
+lemma list_insert_before_not_found:
+  "a \<notin> set ls \<Longrightarrow> list_insert_before ls a new = ls"
+  by (induct ls; fastforce)
+
+lemma list_insert_before_nonempty:
+  "ls \<noteq> [] \<Longrightarrow> list_insert_before ls a new \<noteq> []"
+  by (induct ls; clarsimp)
+
+lemma list_insert_before_head:
+  "xs \<noteq> [] \<Longrightarrow> list_insert_before xs (hd xs) new = new # xs"
+   by (induct xs; fastforce)
+
+lemma last_of_list_insert_before:
+  "xs \<noteq> [] \<Longrightarrow> last (list_insert_before xs a new) = last xs"
+  by (induct xs; clarsimp simp: list_insert_before_nonempty)
+
+lemma list_insert_before_distinct:
+  "\<lbrakk>distinct (xs @ ys); ys \<noteq> []\<rbrakk> \<Longrightarrow> list_insert_before (xs @ ys) (hd ys) new = xs @ new # ys"
+  by (induct xs; fastforce simp add: list_insert_before_head)
+
+lemma set_list_insert_before:
+  "\<lbrakk>new \<notin> set ls; before \<in> set ls\<rbrakk> \<Longrightarrow> set (list_insert_before ls before new) = set ls \<union> {new}"
+  apply (induct ls; clarsimp)
+  apply fastforce
+  done
+
 lemma list_remove_removed:
   "set (list_remove list x) = (set list) - {x}"
   apply (induct list,simp+)
diff --git a/lib/List_Lib.thy b/lib/List_Lib.thy
index 936f86e6e..e6471707c 100644
--- a/lib/List_Lib.thy
+++ b/lib/List_Lib.thy
@@ -26,6 +26,12 @@ primrec list_insert_after :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Righta
   "list_insert_after (x # xs) a b = (if x = a then x # b # xs
                                      else x # list_insert_after xs a b)"
 
+\<comment> \<open>Inserts the value new immediately before the first occurence of a (if any) in the list\<close>
+primrec list_insert_before :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a list" where
+  "list_insert_before [] a new = []" |
+  "list_insert_before (x # xs) a new = (if x = a then new # x # xs
+                                        else x # list_insert_before xs a new)"
+
 primrec list_remove :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list" where
   "list_remove [] a = []" |
   "list_remove (x # xs) a = (if x = a then (list_remove xs a)