Theory LinkedList

(*
  File: LinkedList.thy
  Author: Bohua Zhan
*)

section ‹Implementation of linked list›

theory LinkedList
  imports SepAuto
begin

text ‹
  Examples in linked lists. Definitions and some of the examples are
  based on List\_Seg and Open\_List theories in \<^cite>‹"Separation_Logic_Imperative_HOL-AFP"›
  by Lammich and Meis.
›

subsection ‹List Assertion›

datatype 'a node = Node (val: "'a") (nxt: "'a node ref option")
setup ‹fold add_rewrite_rule @{thms node.sel}›

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)
  ..

fun os_list :: "'a::heap list ⇒ 'a node ref option ⇒ assn" where
  "os_list [] p = ↑(p = None)"
| "os_list (x # l) (Some p) = (∃⇩Aq. p ↦⇩r Node x q * os_list l q)"
| "os_list (x # l) None = false"
setup ‹fold add_rewrite_ent_rule @{thms os_list.simps}›

lemma os_list_empty [forward_ent]:
  "os_list [] p ⟹⇩A ↑(p = None)" by auto2

lemma os_list_Cons [forward_ent]:
  "os_list (x # l) p ⟹⇩A (∃⇩Aq. the p ↦⇩r Node x q * os_list l q * ↑(p ≠ None))"
@proof @case "p = None" @qed

lemma os_list_none: "emp ⟹⇩A os_list [] None" by auto2

lemma os_list_constr_ent:
  "p ↦⇩r Node x q * os_list l q ⟹⇩A os_list (x # l) (Some p)" by auto2

setup ‹fold add_entail_matcher [@{thm os_list_none}, @{thm os_list_constr_ent}]›
setup ‹fold del_prfstep_thm @{thms os_list.simps}›

ML_file "list_matcher_test.ML"

type_synonym 'a os_list = "'a node ref option"

subsection ‹Basic operations›

definition os_empty :: "'a::heap os_list Heap" where
  "os_empty = return None"

lemma os_empty_rule [hoare_triple]:
  "<emp> os_empty <os_list []>" by auto2

definition os_is_empty :: "'a::heap os_list ⇒ bool Heap" where
  "os_is_empty b = return (b = None)"

lemma os_is_empty_rule [hoare_triple]:
  "<os_list xs b> os_is_empty b <λr. os_list xs b * ↑(r ⟷ xs = [])>"
@proof @case "xs = []" @have "xs = hd xs # tl xs" @qed

definition os_prepend :: "'a ⇒ 'a::heap os_list ⇒ 'a os_list Heap" where
  "os_prepend a n = do { p ← ref (Node a n); return (Some p) }"

lemma os_prepend_rule [hoare_triple]:
  "<os_list xs n> os_prepend x n <os_list (x # xs)>" by auto2

definition os_pop :: "'a::heap os_list ⇒ ('a × 'a os_list) Heap" where
  "os_pop r = (case r of
    None ⇒ raise STR ''Empty Os_list'' |
    Some p ⇒ do {m ← !p; return (val m, nxt m)})"

lemma os_pop_rule [hoare_triple]:
  "<os_list xs (Some p)>
   os_pop (Some p)
   <λ(x,r'). os_list (tl xs) r' * p ↦⇩r (Node x r') * ↑(x = hd xs)>"
@proof @case "xs = []" @have "xs = hd xs # tl xs" @qed

subsection ‹Reverse›

partial_function (heap) os_reverse_aux :: "'a::heap os_list ⇒ 'a os_list ⇒ 'a os_list Heap" where
  "os_reverse_aux q p = (case p of
    None ⇒ return q |
    Some r ⇒ do {
      v ← !r;
      r := Node (val v) q;
      os_reverse_aux p (nxt v) })"

lemma os_reverse_aux_rule [hoare_triple]:
  "<os_list xs p * os_list ys q> 
    os_reverse_aux q p 
   <os_list ((rev xs) @ ys)>"
@proof @induct xs arbitrary p q ys @qed

definition os_reverse :: "'a::heap os_list ⇒ 'a os_list Heap" where
  "os_reverse p = os_reverse_aux None p"

lemma os_reverse_rule:
  "<os_list xs p> os_reverse p <os_list (rev xs)>" by auto2

subsection ‹Remove›

setup ‹fold add_rewrite_rule @{thms removeAll.simps}›

partial_function (heap) os_rem :: "'a::heap ⇒ 'a node ref option ⇒ 'a node ref option Heap" where
  "os_rem x b = (case b of 
     None ⇒ return None |
     Some p ⇒ do { 
       n ← !p;
       q ← os_rem x (nxt n);
       (if (val n = x) 
         then return q
         else do {
           p := Node (val n) q; 
           return (Some p) }) })"

lemma os_rem_rule [hoare_triple]:
  "<os_list xs b> os_rem x b <λr. os_list (removeAll x xs) r>⇩t"
@proof @induct xs arbitrary b @qed

subsection ‹Extract list›

partial_function (heap) extract_list :: "'a::heap os_list ⇒ 'a list Heap" where
  "extract_list p = (case p of
    None ⇒ return []
  | Some pp ⇒ do {
      v ← !pp;
      ls ← extract_list (nxt v);
      return (val v # ls)
    })"

lemma extract_list_rule [hoare_triple]:
  "<os_list l p> extract_list p <λr. os_list l p * ↑(r = l)>"
@proof @induct l arbitrary p @qed

subsection ‹Ordered insert›

fun list_insert :: "'a::ord ⇒ 'a list ⇒ 'a list" where
  "list_insert x [] = [x]"
| "list_insert x (y # ys) = (
    if x ≤ y then x # (y # ys) else y # list_insert x ys)"
setup ‹fold add_rewrite_rule @{thms list_insert.simps}›

lemma list_insert_length:
  "length (list_insert x xs) = length xs + 1"
@proof @induct xs @qed
setup ‹add_forward_prfstep_cond @{thm list_insert_length} [with_term "list_insert ?x ?xs"]›

lemma list_insert_mset [rewrite]:
  "mset (list_insert x xs) = {#x#} + mset xs"
@proof @induct xs @qed

lemma list_insert_set [rewrite]:
  "set (list_insert x xs) = {x} ∪ set xs"
@proof @induct xs @qed

lemma list_insert_sorted [forward]:
  "sorted xs ⟹ sorted (list_insert x xs)"
@proof @induct xs @qed

partial_function (heap) os_insert :: "'a::{ord,heap} ⇒ 'a os_list ⇒ 'a os_list Heap" where
  "os_insert x b = (case b of
      None ⇒ os_prepend x None
    | Some p ⇒ do {
        v ← !p;
        (if x ≤ val v then os_prepend x b
         else do {
           q ← os_insert x (nxt v);
           p := Node (val v) q;
           return (Some p) }) })"

lemma os_insert_to_fun [hoare_triple]:
  "<os_list xs b> os_insert x b <os_list (list_insert x xs)>"
@proof @induct xs arbitrary b @qed

subsection ‹Insertion sort›

fun insert_sort :: "'a::ord list ⇒ 'a list" where
  "insert_sort [] = []"
| "insert_sort (x # xs) = list_insert x (insert_sort xs)"
setup ‹fold add_rewrite_rule @{thms insert_sort.simps}›

lemma insert_sort_mset [rewrite]:
  "mset (insert_sort xs) = mset xs"
@proof @induct xs @qed

lemma insert_sort_sorted [forward]:
  "sorted (insert_sort xs)"
@proof @induct xs @qed

lemma insert_sort_is_sort [rewrite]:
  "insert_sort xs = sort xs" by auto2

fun os_insert_sort_aux :: "'a::{ord,heap} list ⇒ 'a os_list Heap" where
  "os_insert_sort_aux [] = (return None)"
| "os_insert_sort_aux (x # xs) = do {
     b ← os_insert_sort_aux xs;
     b' ← os_insert x b;
     return b'
   }"

lemma os_insert_sort_aux_correct [hoare_triple]:
  "<emp> os_insert_sort_aux xs <os_list (insert_sort xs)>"
@proof @induct xs @qed

definition os_insert_sort :: "'a::{ord,heap} list ⇒ 'a list Heap" where
  "os_insert_sort xs = do {
    p ← os_insert_sort_aux xs;
    l ← extract_list p;
    return l
  }"

lemma insertion_sort_rule [hoare_triple]:
  "<emp> os_insert_sort xs <λys. ↑(ys = sort xs)>⇩t" by auto2

subsection ‹Merging two lists›

fun merge_list :: "('a::ord) list ⇒ 'a list ⇒ 'a list" where
  "merge_list xs [] = xs"
| "merge_list [] ys = ys"
| "merge_list (x # xs) (y # ys) = (
    if x ≤ y then x # (merge_list xs (y # ys))
    else y # (merge_list (x # xs) ys))"
setup ‹fold add_rewrite_rule @{thms merge_list.simps}›

lemma merge_list_correct [rewrite]:
  "set (merge_list xs ys) = set xs ∪ set ys"
@proof @fun_induct "merge_list xs ys" @qed

lemma merge_list_sorted [forward]:
  "sorted xs ⟹ sorted ys ⟹ sorted (merge_list xs ys)"
@proof @fun_induct "merge_list xs ys" @qed

partial_function (heap) merge_os_list :: "('a::{heap, ord}) os_list ⇒ 'a os_list ⇒ 'a os_list Heap" where
  "merge_os_list p q = (
    if p = None then return q
    else if q = None then return p
    else do {
      np ← !(the p); nq ← !(the q);
      if val np ≤ val nq then
        do { npq ← merge_os_list (nxt np) q;
             (the p) := Node (val np) npq;
             return p }
      else
        do { pnq ← merge_os_list p (nxt nq);
             (the q) := Node (val nq) pnq;
             return q } })"

lemma merge_os_list_to_fun [hoare_triple]:
  "<os_list xs p * os_list ys q>
  merge_os_list p q
  <λr. os_list (merge_list xs ys) r>"
@proof @fun_induct "merge_list xs ys" arbitrary p q @qed

subsection ‹List copy›

partial_function (heap) copy_os_list :: "'a::heap os_list ⇒ 'a os_list Heap" where
  "copy_os_list b = (case b of
      None ⇒ return None
    | Some p ⇒ do {
        v ← !p;
        q ← copy_os_list (nxt v);
        os_prepend (val v) q })"

lemma copy_os_list_rule [hoare_triple]:
  "<os_list xs b> copy_os_list b <λr. os_list xs b * os_list xs r>"
@proof @induct xs arbitrary b @qed

subsection ‹Higher-order functions›

partial_function (heap) map_os_list :: "('a::heap ⇒ 'a) ⇒ 'a os_list ⇒ 'a os_list Heap" where
  "map_os_list f b = (case b of
      None ⇒ return None
    | Some p ⇒ do {
        v ← !p;
        q ← map_os_list f (nxt v);
        p := Node (f (val v)) q;
        return (Some p) })"

lemma map_os_list_rule [hoare_triple]:
  "<os_list xs b> map_os_list f b <os_list (map f xs)>"
@proof @induct xs arbitrary b @qed

partial_function (heap) filter_os_list :: "('a::heap ⇒ bool) ⇒ 'a os_list ⇒ 'a os_list Heap" where
  "filter_os_list f b = (case b of
      None ⇒ return None
    | Some p ⇒ do {
        v ← !p;
        q ← filter_os_list f (nxt v);
        (if (f (val v)) then do {
           p := Node (val v) q;
           return (Some p) }
         else return q) })"

lemma filter_os_list_rule [hoare_triple]:
  "<os_list xs b> filter_os_list f b <λr. os_list (filter f xs) r * true>"
@proof @induct xs arbitrary b @qed

partial_function (heap) filter_os_list2 :: "('a::heap ⇒ bool) ⇒ 'a os_list ⇒ 'a os_list Heap" where
  "filter_os_list2 f b = (case b of
      None ⇒ return None
    | Some p ⇒ do {
        v ← !p;
        q ← filter_os_list2 f (nxt v);
        (if (f (val v)) then os_prepend (val v) q
         else return q) })"

lemma filter_os_list2_rule [hoare_triple]:
  "<os_list xs b> filter_os_list2 f b <λr. os_list xs b * os_list (filter f xs) r>"
@proof @induct xs arbitrary b @qed

setup ‹fold add_rewrite_rule @{thms List.fold_simps}›

partial_function (heap) fold_os_list :: "('a::heap ⇒ 'b ⇒ 'b) ⇒ 'a os_list ⇒ 'b ⇒ 'b Heap" where
  "fold_os_list f b x = (case b of
      None ⇒ return x
    | Some p ⇒ do {
       v ← !p;
       r ← fold_os_list f (nxt v) (f (val v) x);
       return r})"

lemma fold_os_list_rule [hoare_triple]:
  "<os_list xs b> fold_os_list f b x <λr. os_list xs b * ↑(r = fold f xs x)>"
@proof @induct xs arbitrary b x @qed

end