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, @{text "None"} representing a null pointer.
Unfortunately, Imperative HOL requires some boilerplate code to define
a datatype.
*}
setup {* Sign.add_const_constraint
(@{const_name Ref}, SOME @{typ "nat ⇒ 'a::type ref"}) *}
datatype 'a node = Node "'a" "'a node ref option"
setup {* Sign.add_const_constraint
(@{const_name Ref}, SOME @{typ "nat ⇒ 'a::heap ref"}) *}
setup {* Sign.add_const_constraint (@{const_name Node},
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, @{text "lseg l p s"} describes a list starting at @{text "p"} and
ending with a pointer @{text "s"}. The content of the list are @{text "l"}.
Note that the pointer @{text "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)
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