# Theory Separation_Logic_Imperative_HOL.List_Seg

```section ‹Singly Linked List Segments›
theory List_Seg
imports "../Sep_Main"
begin

subsection ‹Nodes›
text ‹
We define a node of a list to contain a data value and a next pointer.
As Imperative HOL does not support null-pointers, we make the next-pointer
an optional value, ‹None› representing a null pointer.

Unfortunately, Imperative HOL requires some boilerplate code to define
a datatype.
›
(@{const_name Ref}, SOME @{typ "nat ⇒ 'a::type ref"})›

datatype 'a node = Node "'a" "'a node ref option"

(@{const_name Ref}, SOME @{typ "nat ⇒ 'a::heap ref"})›

SOME @{typ "'a::heap ⇒ 'a node ref option ⇒ 'a node"})›

text ‹Selector Functions›
primrec val :: "'a::heap node ⇒ 'a" where
[sep_dflt_simps]: "val (Node x _) = x"

primrec "next" :: "'a::heap node ⇒ 'a node ref option" where
[sep_dflt_simps]: "next (Node _ r) = r"

text ‹Encoding to natural numbers, as required by Imperative/HOL›
fun
node_encode :: "'a::heap node ⇒ nat"
where
"node_encode (Node x r) = to_nat (x, r)"

instance node :: (heap) heap
apply (rule heap_class.intro)
apply (rule countable_classI [of "node_encode"])
apply (case_tac x, simp_all, case_tac y, simp_all)
..

subsection ‹List Segment Assertion›
text ‹
Intuitively, ‹lseg l p s› describes a list starting at ‹p› and
ending with a pointer ‹s›. The content of the list are ‹l›.
Note that the pointer ‹s› may also occur earlier in the list, in which
case it is handled as a usual next-pointer.
›
fun lseg
:: "'a::heap list ⇒ 'a node ref option ⇒ 'a node ref option ⇒ assn"
where
"lseg [] p s = ↑(p=s)"
| "lseg (x#l) (Some p) s = (∃⇩Aq. p ↦⇩r Node x q * lseg l q s)"
| "lseg (_#_) None _ = false"

lemma lseg_if_splitf1[simp, sep_dflt_simps]:
"lseg l None None = ↑(l=[])"
apply (cases l, simp_all)
done

lemma lseg_if_splitf2[simp, sep_dflt_simps]:
"lseg (x#xs) p q
= (∃⇩App n. pp ↦⇩r (Node x n) * lseg xs n q * ↑(p=Some pp))"
apply (cases p, simp_all)
(* TODO: One-point simproc for assertions! *)
apply (rule ent_iffI)
apply solve_entails
apply solve_entails
done

subsection ‹Lemmas›

subsubsection ‹Concatenation›
lemma lseg_prepend:
"p↦⇩rNode x q * lseg l q s ⟹⇩A lseg (x#l) (Some p) s"
by sep_auto

lemma lseg_append:
"lseg l p (Some s) * s↦⇩rNode x q ⟹⇩A lseg (l@[x]) p q"
proof (induction l arbitrary: p)
case Nil thus ?case by sep_auto
next
case (Cons y l)
show ?case
apply (cases p)
apply simp
apply (sep_auto)
apply (rule ent_frame_fwd[OF Cons.IH])
apply frame_inference
apply solve_entails
done
qed

lemma lseg_conc: "lseg l1 p q * lseg l2 q r ⟹⇩A lseg (l1@l2) p r"
proof (induct l1 arbitrary: p)
case Nil thus ?case by simp
next
case (Cons x l1)
show ?case
apply simp
apply sep_auto
apply (rule ent_frame_fwd[OF Cons.hyps])
apply frame_inference
apply solve_entails
done
qed

subsubsection ‹Splitting›
lemma lseg_split:
"lseg (l1@l2) p r ⟹⇩A ∃⇩Aq. lseg l1 p q * lseg l2 q r"
proof (induct l1 arbitrary: p)
case Nil thus ?case by sep_auto
next
case (Cons x l1)

have "lseg ((x # l1) @ l2) p r
⟹⇩A ∃⇩App n. pp ↦⇩r Node x n * lseg (l1 @ l2) n r * ↑ (p = Some pp)"
by simp
also have "… ⟹⇩A
∃⇩App n q. pp ↦⇩r Node x n
* lseg l1 n q
* lseg l2 q r
* ↑(p = Some pp)"
apply (intro ent_ex_preI)
apply clarsimp
apply (rule ent_frame_fwd[OF Cons.hyps])
apply frame_inference
apply sep_auto
done
also have "… ⟹⇩A ∃⇩Aq. lseg (x#l1) p q * lseg l2 q r"
by sep_auto
finally show ?case .
qed

subsubsection ‹Precision›
lemma lseg_prec1:
"∀l l'. (h⊨
(lseg l p (Some q) * q ↦⇩r x * F1)
∧⇩A (lseg l' p (Some q) * q ↦⇩r x * F2))
⟶ l=l'"
apply (intro allI)
subgoal for l l'
proof (induct l arbitrary: p l' F1 F2)
case Nil thus ?case
apply simp_all
apply (cases l')
apply simp
apply auto
done
next
case (Cons y l)
from Cons.prems show ?case
apply (cases l')
apply auto []
apply (cases p)
apply simp

apply (clarsimp)

apply (subgoal_tac "y=a ∧ na=n", simp)

using Cons.hyps apply (erule prec_frame')
apply frame_inference
apply frame_inference

apply (drule_tac p=aa in prec_frame[OF sngr_prec])
apply frame_inference
apply frame_inference
apply simp
done
qed
done

lemma lseg_prec2:
"∀l l'. (h⊨
(lseg l p None * F1) ∧⇩A (lseg l' p None * F2))
⟶ l=l'"
apply (intro allI)
subgoal for l l'
proof (induct l arbitrary: p l' F1 F2)
case Nil thus ?case
apply simp_all
apply (cases l')
apply simp
apply (cases p)
apply auto
done
next
case (Cons y l)
from Cons.prems show ?case
apply (cases p)
apply simp
apply (cases l')
apply (auto) []

apply (clarsimp)

apply (subgoal_tac "y=aa ∧ na=n", simp)

using Cons.hyps apply (erule prec_frame')
apply frame_inference
apply frame_inference

apply (drule_tac p=a in prec_frame[OF sngr_prec])
apply frame_inference
apply frame_inference
apply simp
done
qed
done

lemma lseg_prec3:
"∀q q'. h ⊨ (lseg l p q * F1) ∧⇩A (lseg l p q' * F2) ⟶ q=q'"
apply (intro allI)
proof (induct l arbitrary: p F1 F2)
case Nil thus ?case by auto
next
case (Cons x l)
show ?case
apply auto

apply (subgoal_tac "na=n")
using Cons.hyps apply (erule prec_frame')
apply frame_inference
apply frame_inference

apply (drule prec_frame[OF sngr_prec])
apply frame_inference
apply frame_inference
apply simp
done
qed

end
```