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.
›
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, 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: 
  "prNode x q * lseg l q s A lseg (x#l) (Some p) s"
  by sep_auto

lemma lseg_append: 
  "lseg l p (Some s) * srNode 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