From dd1d17df54c37be5e16ab7afadff60a4db697a80 Mon Sep 17 00:00:00 2001
From: Michael McInerney <michael.mcinerney@proofcraft.systems>
Date: Wed, 10 Jan 2024 11:15:36 +1030
Subject: [PATCH] lib: add Heap_List.thy, for reasoning about linked lists on
 heaps

From the rt branch

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
---
 lib/Heap_List.thy | 348 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 348 insertions(+)
 create mode 100644 lib/Heap_List.thy

diff --git a/lib/Heap_List.thy b/lib/Heap_List.thy
new file mode 100644
index 000000000..3b64851ea
--- /dev/null
+++ b/lib/Heap_List.thy
@@ -0,0 +1,348 @@
+(*
+ * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ *)
+
+(* Singly-linked lists on heaps or projections from heaps, as predicate and as recursive function.
+   Loosely after ~~/src/HOL/Hoare/Pointer_Examples.thy *)
+
+theory Heap_List
+imports Main "HOL-Library.Prefix_Order"
+begin
+
+(* Given a heap projection that returns the next-pointer for an object at address x,
+   given a start pointer x, and an end pointer y, determine if the given list
+   is the path of addresses visited when following the next-pointers from x to y *)
+primrec heap_path :: "('a \<rightharpoonup> 'a) \<Rightarrow> 'a option \<Rightarrow> 'a list \<Rightarrow> 'a option \<Rightarrow> bool" where
+  "heap_path hp x [] y     = (x = y)"
+| "heap_path hp x (a#as) y = (x = Some a \<and> heap_path hp (hp a) as y)"
+
+(* When a path ends in None, it is a singly-linked list *)
+abbreviation heap_ls :: "('a \<rightharpoonup> 'a) \<Rightarrow> 'a option \<Rightarrow> 'a list \<Rightarrow> bool" where
+  "heap_ls hp x xs \<equiv> heap_path hp x xs None"
+
+(* Walk a linked list of next pointers, recording which it visited.
+   Terminates artificially at loops, and otherwise because the address domain is finite *)
+function heap_walk :: "('a::finite \<rightharpoonup> 'a) \<Rightarrow> 'a option \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+  "heap_walk hp None xs = xs"
+| "heap_walk hp (Some x) xs = (if x \<in> set xs then xs else heap_walk hp (hp x) (xs@[x]))"
+  by pat_completeness auto
+
+lemma card_set_UNIV:
+  fixes xs :: "'a::finite list"
+  assumes "x \<notin> set xs"
+  shows "card (set xs) < card(UNIV::'a set)"
+proof -
+  have "finite (UNIV::'a set)" by simp
+  moreover
+  from assms have "set xs \<subset> UNIV" by blast
+  ultimately
+  show ?thesis by (rule psubset_card_mono)
+qed
+
+termination heap_walk
+  by (relation "measure (\<lambda>(_, _, xs). card(UNIV :: 'a set) - card (set xs))";
+      simp add: card_set_UNIV diff_less_mono2)
+
+lemma heap_path_append[simp]:
+  "heap_path hp start (xs @ ys) end = (\<exists>x. heap_path hp start xs x \<and> heap_path hp x ys end)"
+  by (induct xs arbitrary: start; simp)
+
+lemma heap_path_None[simp]:
+  "heap_path hp None xs end = (xs = [] \<and> end = None)"
+  by (cases xs, auto)
+
+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)
+
+lemma heap_ls_hd_not_in_tl:
+  "heap_ls hp (hp x) xs \<Longrightarrow> x \<notin> set xs"
+proof
+  assume "x \<in> set xs"
+  then obtain ys zs where xs: "xs = ys @ x # zs"  by (auto simp: in_set_conv_decomp)
+  moreover assume "heap_ls hp (hp x) xs"
+  moreover from this xs have "heap_ls hp (hp x) zs" by clarsimp
+  ultimately show False by (fastforce dest: heap_ls_unique)
+qed
+
+lemma heap_ls_distinct:
+  "heap_ls hp x xs \<Longrightarrow> distinct xs"
+  by (induct xs arbitrary: x; clarsimp simp: heap_ls_hd_not_in_tl)
+
+lemma heap_ls_is_walk':
+  "\<lbrakk> heap_ls hp x xs; set xs \<inter> set ys = {} \<rbrakk> \<Longrightarrow> heap_walk hp x ys = ys @ xs"
+  by (frule heap_ls_distinct) (induct xs arbitrary: x ys; clarsimp)
+
+lemma heap_ls_is_walk:
+  "heap_ls hp x xs \<Longrightarrow> heap_walk hp x [] = xs"
+  using heap_ls_is_walk' by fastforce
+
+lemma heap_path_end_unique:
+  "heap_path hp x xs y \<Longrightarrow> heap_path hp x xs y' \<Longrightarrow> y = y'"
+  by (induct xs arbitrary: x; clarsimp)
+
+lemma heap_path_head:
+  "heap_path hp x xs y \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> x = Some (hd xs)"
+  by (induct xs arbitrary: x; clarsimp)
+
+lemma heap_path_non_nil_lookup_next:
+  "heap_path hp x (xs@z#ys) y \<Longrightarrow> hp z = (case ys of [] \<Rightarrow> y | _ \<Rightarrow> Some (hd ys))"
+  by (cases ys; fastforce)
+
+lemma heap_path_prefix:
+  "heap_path hp st ls ed \<Longrightarrow> \<forall>xs\<le>ls. heap_path hp st xs (if xs = [] then st else hp (last xs))"
+  apply clarsimp
+  apply (erule Prefix_Order.prefixE)
+  by (metis append_butlast_last_id heap_path_append heap_path_non_nil_lookup_next list.case(1))
+
+lemma heap_path_butlast:
+  "heap_path hp st ls ed \<Longrightarrow> ls \<noteq> [] \<Longrightarrow> heap_path hp st (butlast ls) (Some (last ls))"
+  by (induct ls rule: rev_induct; simp)
+
+lemma in_list_decompose_takeWhile:
+  "x \<in> set xs \<Longrightarrow>
+   xs = (takeWhile ((\<noteq>) x) xs) @ x # (drop (length (takeWhile ((\<noteq>) x) xs) + 1) xs)"
+  by (induct xs arbitrary: x; clarsimp)
+
+lemma takeWhile_neq_hd_eq_Nil[simp]:
+  "takeWhile ((\<noteq>) (hd xs)) xs = Nil"
+  by (metis (full_types) hd_Cons_tl takeWhile.simps(1) takeWhile.simps(2))
+
+lemma heap_not_in_dom[simp]:
+  "ptr \<notin> dom hp \<Longrightarrow> hp(ptr := None) = hp"
+  by (auto simp: dom_def)
+
+lemma heap_path_takeWhile_lookup_next:
+  "\<lbrakk> heap_path hp st rs ed; r \<in> set rs \<rbrakk>
+   \<Longrightarrow> heap_path hp st (takeWhile ((\<noteq>) r) rs) (Some r)"
+  apply (drule heap_path_prefix)
+  apply (subgoal_tac "takeWhile ((\<noteq>) r) rs @ [r] \<le> rs", fastforce)
+  by (fastforce dest!: in_list_decompose_takeWhile intro: Prefix_Order.prefixI)
+
+lemma heap_path_heap_upd_not_in:
+  "\<lbrakk>heap_path hp st rs ed; r \<notin> set rs\<rbrakk> \<Longrightarrow> heap_path (hp(r:= x)) st rs ed"
+  by (induct rs arbitrary: st; clarsimp)
+
+lemma heap_walk_lb:
+  "heap_walk hp x xs \<ge> xs"
+  apply (induct xs rule: heap_walk.induct; clarsimp)
+  by (metis Prefix_Order.prefixE Prefix_Order.prefixI append_assoc)
+
+lemma heal_walk_Some_nonempty':
+  "heap_walk hp (Some x) [] > []"
+  by (fastforce intro: heap_walk_lb less_le_trans[where y="[x]"])
+
+lemma heal_walk_Some_nonempty:
+  "heap_walk hp (Some x) [] \<noteq> []"
+  by (metis less_list_def heal_walk_Some_nonempty')
+
+lemma heap_walk_Nil_None:
+  "heap_walk hp st [] = [] \<Longrightarrow> st = None"
+   by (case_tac st; simp only: heal_walk_Some_nonempty)
+
+lemma heap_ls_last_None:
+  "heap_ls hp st xs \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> hp (last xs) = None"
+  by (induct xs rule: rev_induct; clarsimp)
+
+(* sym_heap *)
+
+definition sym_heap where
+  "sym_heap hp hp' \<equiv> \<forall>p p'. hp p = Some p' \<longleftrightarrow> hp' p' = Some p"
+
+lemma sym_heapD1:
+  "sym_heap hp hp' \<Longrightarrow> hp p = Some p' \<Longrightarrow> hp' p' = Some p"
+  by (clarsimp simp: sym_heap_def)
+
+lemma sym_heapD2:
+  "sym_heap hp hp' \<Longrightarrow> hp' p' = Some p \<Longrightarrow> hp p = Some p'"
+  by (clarsimp simp: sym_heap_def)
+
+lemma sym_heap_symmetric:
+  "sym_heap hp hp' \<longleftrightarrow> sym_heap hp' hp"
+  unfolding sym_heap_def by blast
+
+lemma sym_heap_None:
+  "\<lbrakk>sym_heap hp hp'; hp p = None\<rbrakk> \<Longrightarrow> \<forall>p'. hp' p' \<noteq> Some p" unfolding sym_heap_def by force
+
+lemma sym_heap_path_reverse:
+  "sym_heap hp hp' \<Longrightarrow>
+      heap_path hp (Some p) (p#ps) (Some p')
+          \<longleftrightarrow> heap_path hp' (Some p') (p'#(rev ps)) (Some p)"
+  unfolding sym_heap_def by (induct ps arbitrary: p p' rule: rev_induct; force)
+
+lemma sym_heap_ls_rev_Cons:
+  "\<lbrakk>sym_heap hp hp'; heap_ls hp (Some p) (p#ps)\<rbrakk>
+  \<Longrightarrow> heap_path hp' (Some (last (p#ps))) (rev ps) (Some p)"
+  supply rev.simps[simp del]
+  apply (induct ps arbitrary: p rule: rev_induct; simp add: rev.simps)
+  by (auto dest!: sym_heap_path_reverse[THEN iffD1])
+
+lemma sym_heap_ls_rev:
+  "\<lbrakk>sym_heap hp hp'; heap_ls hp (Some p) ps\<rbrakk>
+  \<Longrightarrow> heap_path hp' (Some (last ps)) (butlast (rev ps)) (Some p)
+      \<and> hp (last ps) = None"
+  apply (induct ps arbitrary: p rule: rev_induct, simp)
+  apply (frule heap_path_head; clarsimp)
+  by (auto dest!: sym_heap_path_reverse[THEN iffD1])
+
+(* more on heap_path : next/prev in path *)
+
+lemma heap_path_extend:
+  "heap_path hp st (ls @ [p]) (hp p) \<longleftrightarrow> heap_path hp st ls (Some p)"
+  by (induct ls rule: rev_induct; simp)
+
+lemma heap_path_prefix_heap_ls:
+  "\<lbrakk>heap_ls hp st xs; heap_path hp st ys ed\<rbrakk> \<Longrightarrow> ys \<le> xs"
+  apply (induct xs arbitrary: ys st, simp)
+  apply (case_tac ys; clarsimp)
+  done
+
+lemma distinct_decompose2:
+  "\<lbrakk>distinct xs; xs = ys @ x # y # zs\<rbrakk>
+   \<Longrightarrow> x \<noteq> y \<and> x \<notin> set ys \<and> y \<notin> set ys \<and> x \<notin> set zs \<and> y \<notin> set zs"
+  by (simp add: in_set_conv_decomp)
+
+lemma heap_path_distinct_next_cases: (* the other direction needs sym_heap *)
+  "\<lbrakk>heap_path hp st xs ed; distinct xs; p \<in> set xs; hp p = Some np\<rbrakk>
+  \<Longrightarrow> ed = Some p \<or> ed = Some np \<or> np \<in> set xs"
+  apply (cases ed; simp)
+   apply (frule in_list_decompose_takeWhile)
+   apply (subgoal_tac "heap_ls hp st (takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs)")
+   apply (drule heap_path_non_nil_lookup_next)
+   apply (case_tac "drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs"; simp)
+   apply (metis in_set_dropD list.set_intros(1))
+  apply simp
+  apply (frule in_list_decompose_takeWhile)
+  apply (subgoal_tac "heap_path hp st (takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs) ed")
+  apply (frule heap_path_non_nil_lookup_next)
+  apply (case_tac "drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs", simp)
+  apply (simp split: if_split_asm)
+  apply (drule (1) distinct_decompose2)
+  apply clarsimp
+  by (metis in_set_dropD list.set_intros(1)) simp
+
+lemma heap_ls_next_in_list:
+  "\<lbrakk>heap_ls hp st xs; p \<in> set xs; hp p = Some np\<rbrakk>
+  \<Longrightarrow> np \<in> set xs"
+   apply (subgoal_tac "distinct xs")
+   by (fastforce dest!: heap_path_distinct_next_cases) (erule heap_ls_distinct)
+
+lemma heap_path_distinct_sym_prev_cases:
+  "\<lbrakk>heap_path hp st xs ed; distinct xs; np \<in> set xs; hp p = Some np; sym_heap hp hp'\<rbrakk>
+  \<Longrightarrow> st = Some np \<or> p \<in> set xs"
+  apply (cases st; simp)
+  apply (rename_tac stp)
+  apply (case_tac "stp = np"; simp)
+  apply (cases xs; simp del: heap_path.simps)
+  apply (frule heap_path_head, simp)
+  apply (cases ed, clarsimp)
+   apply (frule sym_heap_ls_rev_Cons, fastforce)
+   apply (drule heap_path_distinct_next_cases[where hp=hp']; simp add: sym_heap_def)
+   apply simp
+  apply (simp del: heap_path.simps)
+  apply (frule (1) sym_heap_path_reverse[where hp'=hp', THEN iffD1])
+  apply simp
+  apply (frule heap_path_distinct_next_cases[where hp=hp']; simp add: sym_heap_def)
+  apply fastforce
+  done
+
+lemma heap_ls_prev_cases:
+  "\<lbrakk>heap_ls hp st xs; np \<in> set xs; hp p = Some np; sym_heap hp hp'\<rbrakk>
+  \<Longrightarrow> st = Some np \<or> p \<in> set xs"
+   apply (subgoal_tac "distinct xs")
+   by (fastforce dest!: heap_path_distinct_sym_prev_cases) (erule heap_ls_distinct)
+
+lemma heap_ls_prev_not_in:
+  "\<lbrakk>heap_ls hp st xs; np \<notin> set xs; hp p = Some np\<rbrakk>
+  \<Longrightarrow> p \<notin> set xs"
+  by (meson heap_ls_next_in_list)
+
+lemma heap_path_distinct_prev_not_in:
+  "\<lbrakk>heap_path hp st xs ed; distinct xs; np \<notin> set xs; hp p = Some np; ed \<noteq> Some np; ed \<noteq> Some p\<rbrakk>
+  \<Longrightarrow> p \<notin> set xs"
+  using heap_path_distinct_next_cases
+  by fastforce
+
+lemma heap_path_distinct_next_not_in:
+  "\<lbrakk>heap_path hp st xs ed; distinct xs; p \<notin> set xs; hp p = Some np;
+    sym_heap hp hp'; st \<noteq> Some np\<rbrakk>
+  \<Longrightarrow> np \<notin> set xs"
+  by (fastforce dest!: heap_path_distinct_sym_prev_cases[simplified])
+
+lemma heap_ls_next_not_in:
+  "\<lbrakk>heap_ls hp st xs; p \<notin> set xs; hp p = Some np; sym_heap hp hp'; st \<noteq> Some np\<rbrakk>
+  \<Longrightarrow> np \<notin> set xs"
+  by (fastforce dest!: heap_ls_prev_cases[simplified])
+
+(* more on heap_path *)
+
+(* moved from ListLibLemmas *)
+lemma distinct_inj_middle: "distinct list \<Longrightarrow> list = (xa @ x # xb) \<Longrightarrow> list = (ya @ x # yb) \<Longrightarrow> xa = ya \<and> xb = yb"
+  apply (induct list arbitrary: xa ya)
+  apply simp
+  apply clarsimp
+  apply (case_tac "xa")
+   apply simp
+   apply (case_tac "ya")
+    apply simp
+   apply clarsimp
+  apply clarsimp
+  apply (case_tac "ya")
+   apply (simp (no_asm_simp))
+   apply simp
+  apply clarsimp
+  done
+
+lemma heap_ls_next_takeWhile_append:
+  "\<lbrakk>heap_ls hp st xs; p \<in> set xs; hp p = Some np\<rbrakk>
+  \<Longrightarrow> takeWhile ((\<noteq>) np) xs = (takeWhile ((\<noteq>) p) xs) @ [p]"
+  apply (frule heap_ls_distinct)
+  apply (frule in_list_decompose_takeWhile)
+  apply (subgoal_tac "heap_ls hp st (takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs)")
+   prefer 2 apply simp
+  apply (drule heap_path_non_nil_lookup_next)
+  apply (case_tac "drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs"; simp)
+  apply (subgoal_tac "np \<in> set xs")
+   prefer 2 apply (erule (2) heap_ls_next_in_list)
+  apply (frule in_list_decompose_takeWhile[where x=np])
+  apply (drule (1) distinct_inj_middle[where x=np and xa="takeWhile ((\<noteq>) np) xs" and ya="takeWhile ((\<noteq>) p) xs @ [p]"])
+   apply simp+
+  done
+
+(* RT FIXME: Move *)
+lemma takeWhile_neq_notin_same:
+  "x \<notin> set xs \<Longrightarrow> takeWhile ((\<noteq>) x) xs = xs"
+  using takeWhile_eq_all_conv by blast
+
+lemma heap_path_extend_takeWhile:
+  "\<lbrakk>heap_ls hp st xs; heap_path hp st (takeWhile ((\<noteq>) p) xs) (Some p); hp p = Some np\<rbrakk>
+  \<Longrightarrow> heap_path hp st (takeWhile ((\<noteq>) np) xs) (Some np)"
+  apply (case_tac "p \<in> set xs")
+  apply (subst heap_ls_next_takeWhile_append[where p=p and np=np and hp=hp]; simp)
+  apply (drule takeWhile_neq_notin_same, simp)
+  apply (drule (1) heap_path_end_unique, simp)
+  done
+
+lemma heap_ls_next_takeWhile_append_sym:
+  "\<lbrakk>heap_ls hp st xs; np \<in> set xs; st \<noteq> Some np; hp p = Some np; sym_heap hp hp'\<rbrakk>
+  \<Longrightarrow>takeWhile ((\<noteq>) np) xs = (takeWhile ((\<noteq>) p) xs) @ [p]"
+  apply (frule (3) heap_ls_prev_cases, simp)
+  apply (fastforce elim!: heap_ls_next_takeWhile_append)
+  done
+
+lemma heap_path_curtail_takeWhile:
+  "\<lbrakk>heap_ls hp st xs; heap_path hp st (takeWhile ((\<noteq>) np) xs) (Some np);
+    st \<noteq> Some np; hp p = Some np; sym_heap hp hp'\<rbrakk>
+  \<Longrightarrow> heap_path hp st (takeWhile ((\<noteq>) p) xs) (Some p)"
+  apply (case_tac "np \<in> set xs")
+   apply (drule (4) heap_ls_next_takeWhile_append_sym)
+   apply simp
+  apply (drule takeWhile_neq_notin_same, simp)
+  apply (drule (1) heap_path_end_unique, simp)
+  done
+
+(* more on heap_path : end *)
+
+end
\ No newline at end of file