Theory Linked_Lists

(*  Title:      HOL/Imperative_HOL/ex/Linked_Lists.thy
    Author:     Lukas Bulwahn, TU Muenchen
*)

section ‹Linked Lists by ML references›

theory Linked_Lists
imports "../Imperative_HOL" "HOL-Library.Code_Target_Int"
begin

section ‹Definition of Linked Lists›

setup ‹Sign.add_const_constraint (\<^const_name>‹Ref›, SOME \<^typ>‹nat ⇒ 'a::type ref›)›
datatype 'a node = Empty | Node 'a "'a node ref"

primrec
  node_encode :: "'a::countable node ⇒ nat"
where
  "node_encode Empty = 0"
  | "node_encode (Node x r) = Suc (to_nat (x, r))"

instance node :: (countable) countable
proof (rule countable_classI [of "node_encode"])
  fix x y :: "'a::countable node"
  show "node_encode x = node_encode y ⟹ x = y"
  by (induct x, auto, induct y, auto, induct y, auto)
qed

instance node :: (heap) heap ..

primrec make_llist :: "'a::heap list ⇒ 'a node Heap"
where 
  [simp del]: "make_llist []     = return Empty"
            | "make_llist (x#xs) = do { tl ← make_llist xs;
                                        next ← ref tl;
                                        return (Node x next)
                                   }"


partial_function (heap) traverse :: "'a::heap node ⇒ 'a list Heap"
where
  [code del]: "traverse l =
    (case l of Empty ⇒ return []
     | Node x r ⇒ do { tl ← Ref.lookup r;
                              xs ← traverse tl;
                              return (x#xs)
                         })"

lemma traverse_simps[code, simp]:
  "traverse Empty      = return []"
  "traverse (Node x r) = do { tl ← Ref.lookup r;
                              xs ← traverse tl;
                              return (x#xs)
                         }"
by (simp_all add: traverse.simps[of "Empty"] traverse.simps[of "Node x r"])


section ‹Proving correctness with relational abstraction›

subsection ‹Definition of list_of, list_of', refs_of and refs_of'›

primrec list_of :: "heap ⇒ ('a::heap) node ⇒ 'a list ⇒ bool"
where
  "list_of h r [] = (r = Empty)"
| "list_of h r (a#as) = (case r of Empty ⇒ False | Node b bs ⇒ (a = b ∧ list_of h (Ref.get h bs) as))"
 
definition list_of' :: "heap ⇒ ('a::heap) node ref ⇒ 'a list ⇒ bool"
where
  "list_of' h r xs = list_of h (Ref.get h r) xs"

primrec refs_of :: "heap ⇒ ('a::heap) node ⇒ 'a node ref list ⇒ bool"
where
  "refs_of h r [] = (r = Empty)"
| "refs_of h r (x#xs) = (case r of Empty ⇒ False | Node b bs ⇒ (x = bs) ∧ refs_of h (Ref.get h bs) xs)"

primrec refs_of' :: "heap ⇒ ('a::heap) node ref ⇒ 'a node ref list ⇒ bool"
where
  "refs_of' h r [] = False"
| "refs_of' h r (x#xs) = ((x = r) ∧ refs_of h (Ref.get h x) xs)"


subsection ‹Properties of these definitions›

lemma list_of_Empty[simp]: "list_of h Empty xs = (xs = [])"
by (cases xs, auto)

lemma list_of_Node[simp]: "list_of h (Node x ps) xs = (∃xs'. (xs = x # xs') ∧ list_of h (Ref.get h ps) xs')"
by (cases xs, auto)

lemma list_of'_Empty[simp]: "Ref.get h q = Empty ⟹ list_of' h q xs = (xs = [])"
unfolding list_of'_def by simp

lemma list_of'_Node[simp]: "Ref.get h q = Node x ps ⟹ list_of' h q xs = (∃xs'. (xs = x # xs') ∧ list_of' h ps xs')"
unfolding list_of'_def by simp

lemma list_of'_Nil: "list_of' h q [] ⟹ Ref.get h q = Empty"
unfolding list_of'_def by simp

lemma list_of'_Cons: 
assumes "list_of' h q (x#xs)"
obtains n where "Ref.get h q = Node x n" and "list_of' h n xs"
using assms unfolding list_of'_def by (auto split: node.split_asm)

lemma refs_of_Empty[simp] : "refs_of h Empty xs = (xs = [])"
  by (cases xs, auto)

lemma refs_of_Node[simp]: "refs_of h (Node x ps) xs = (∃prs. xs = ps # prs ∧ refs_of h (Ref.get h ps) prs)"
  by (cases xs, auto)

lemma refs_of'_def': "refs_of' h p ps = (∃prs. (ps = (p # prs)) ∧ refs_of h (Ref.get h p) prs)"
by (cases ps, auto)

lemma refs_of'_Node:
  assumes "refs_of' h p xs"
  assumes "Ref.get h p = Node x pn"
  obtains pnrs
  where "xs = p # pnrs" and "refs_of' h pn pnrs"
using assms
unfolding refs_of'_def' by auto

lemma list_of_is_fun: "⟦ list_of h n xs; list_of h n ys⟧ ⟹ xs = ys"
proof (induct xs arbitrary: ys n)
  case Nil thus ?case by auto
next
  case (Cons x xs')
  thus ?case
    by (cases ys,  auto split: node.split_asm)
qed

lemma refs_of_is_fun: "⟦ refs_of h n xs; refs_of h n ys⟧ ⟹ xs = ys"
proof (induct xs arbitrary: ys n)
  case Nil thus ?case by auto
next
  case (Cons x xs')
  thus ?case
    by (cases ys,  auto split: node.split_asm)
qed

lemma refs_of'_is_fun: "⟦ refs_of' h p as; refs_of' h p bs ⟧ ⟹ as = bs"
unfolding refs_of'_def' by (auto dest: refs_of_is_fun)


lemma list_of_refs_of_HOL:
  assumes "list_of h r xs"
  shows "∃rs. refs_of h r rs"
using assms
proof (induct xs arbitrary: r)
  case Nil thus ?case by auto
next
  case (Cons x xs')
  thus ?case
    by (cases r, auto)
qed
    
lemma list_of_refs_of:
  assumes "list_of h r xs"
  obtains rs where "refs_of h r rs"
using list_of_refs_of_HOL[OF assms]
by auto

lemma list_of'_refs_of'_HOL:
  assumes "list_of' h r xs"
  shows "∃rs. refs_of' h r rs"
proof -
  from assms obtain rs' where "refs_of h (Ref.get h r) rs'"
    unfolding list_of'_def by (rule list_of_refs_of)
  thus ?thesis unfolding refs_of'_def' by auto
qed

lemma list_of'_refs_of':
  assumes "list_of' h r xs"
  obtains rs where "refs_of' h r rs"
using list_of'_refs_of'_HOL[OF assms]
by auto

lemma refs_of_list_of_HOL:
  assumes "refs_of h r rs"
  shows "∃xs. list_of h r xs"
using assms
proof (induct rs arbitrary: r)
  case Nil thus ?case by auto
next
  case (Cons r rs')
  thus ?case
    by (cases r, auto)
qed

lemma refs_of_list_of:
  assumes "refs_of h r rs"
  obtains xs where "list_of h r xs"
using refs_of_list_of_HOL[OF assms]
by auto

lemma refs_of'_list_of'_HOL:
  assumes "refs_of' h r rs"
  shows "∃xs. list_of' h r xs"
using assms
unfolding list_of'_def refs_of'_def'
by (auto intro: refs_of_list_of)


lemma refs_of'_list_of':
  assumes "refs_of' h r rs"
  obtains xs where "list_of' h r xs"
using refs_of'_list_of'_HOL[OF assms]
by auto

lemma refs_of'E: "refs_of' h q rs ⟹ q ∈ set rs"
unfolding refs_of'_def' by auto

lemma list_of'_refs_of'2:
  assumes "list_of' h r xs"
  shows "∃rs'. refs_of' h r (r#rs')"
proof -
  from assms obtain rs where "refs_of' h r rs" by (rule list_of'_refs_of')
  thus ?thesis by (auto simp add: refs_of'_def')
qed

subsection ‹More complicated properties of these predicates›

lemma list_of_append:
  "list_of h n (as @ bs) ⟹ ∃m. list_of h m bs"
apply (induct as arbitrary: n)
apply auto
apply (case_tac n)
apply auto
done

lemma refs_of_append: "refs_of h n (as @ bs) ⟹ ∃m. refs_of h m bs"
apply (induct as arbitrary: n)
apply auto
apply (case_tac n)
apply auto
done

lemma refs_of_next:
assumes "refs_of h (Ref.get h p) rs"
  shows "p ∉ set rs"
proof (rule ccontr)
  assume a: "¬ (p ∉ set rs)"
  from this obtain as bs where split:"rs = as @ p # bs" by (fastforce dest: split_list)
  with assms obtain q where "refs_of h q (p # bs)" by (fast dest: refs_of_append)
  with assms split show "False"
    by (cases q,auto dest: refs_of_is_fun)
qed

lemma refs_of_distinct: "refs_of h p rs ⟹ distinct rs"
proof (induct rs arbitrary: p)
  case Nil thus ?case by simp
next
  case (Cons r rs')
  thus ?case
    by (cases p, auto simp add: refs_of_next)
qed

lemma refs_of'_distinct: "refs_of' h p rs ⟹ distinct rs"
  unfolding refs_of'_def'
  by (fastforce simp add: refs_of_distinct refs_of_next)


subsection ‹Interaction of these predicates with our heap transitions›

lemma list_of_set_ref: "refs_of h q rs ⟹ p ∉ set rs ⟹ list_of (Ref.set p v h) q as = list_of h q as"
proof (induct as arbitrary: q rs)
  case Nil thus ?case by simp
next
  case (Cons x xs)
  thus ?case
  proof (cases q)
    case Empty thus ?thesis by auto
  next
    case (Node a ref)
    from Cons(2) Node obtain rs' where 1: "refs_of h (Ref.get h ref) rs'" and rs_rs': "rs = ref # rs'" by auto
    from Cons(3) rs_rs' have "ref ≠ p" by fastforce
    hence ref_eq: "Ref.get (Ref.set p v h) ref = (Ref.get h ref)" by (auto simp add: Ref.get_set_neq)
    from rs_rs' Cons(3) have 2: "p ∉ set rs'" by simp
    from Cons.hyps[OF 1 2] Node ref_eq show ?thesis by simp
  qed
qed

lemma refs_of_set_ref: "refs_of h q rs ⟹ p ∉ set rs ⟹ refs_of (Ref.set p v h) q as = refs_of h q as"
proof (induct as arbitrary: q rs)
  case Nil thus ?case by simp
next
  case (Cons x xs)
  thus ?case
  proof (cases q)
    case Empty thus ?thesis by auto
  next
    case (Node a ref)
    from Cons(2) Node obtain rs' where 1: "refs_of h (Ref.get h ref) rs'" and rs_rs': "rs = ref # rs'" by auto
    from Cons(3) rs_rs' have "ref ≠ p" by fastforce
    hence ref_eq: "Ref.get (Ref.set p v h) ref = (Ref.get h ref)" by (auto simp add: Ref.get_set_neq)
    from rs_rs' Cons(3) have 2: "p ∉ set rs'" by simp
    from Cons.hyps[OF 1 2] Node ref_eq show ?thesis by auto
  qed
qed

lemma refs_of_set_ref2: "refs_of (Ref.set p v h) q rs ⟹ p ∉ set rs ⟹ refs_of (Ref.set p v h) q rs = refs_of h q rs"
proof (induct rs arbitrary: q)
  case Nil thus ?case by simp
next
  case (Cons x xs)
  thus ?case
  proof (cases q)
    case Empty thus ?thesis by auto
  next
    case (Node a ref)
    from Cons(2) Node have 1:"refs_of (Ref.set p v h) (Ref.get (Ref.set p v h) ref) xs" and x_ref: "x = ref" by auto
    from Cons(3) this have "ref ≠ p" by fastforce
    hence ref_eq: "Ref.get (Ref.set p v h) ref = (Ref.get h ref)" by (auto simp add: Ref.get_set_neq)
    from Cons(3) have 2: "p ∉ set xs" by simp
    with Cons.hyps 1 2 Node ref_eq show ?thesis
      by simp
  qed
qed

lemma list_of'_set_ref:
  assumes "refs_of' h q rs"
  assumes "p ∉ set rs"
  shows "list_of' (Ref.set p v h) q as = list_of' h q as"
proof -
  from assms have "q ≠ p" by (auto simp only: dest!: refs_of'E)
  with assms show ?thesis
    unfolding list_of'_def refs_of'_def'
    by (auto simp add: list_of_set_ref)
qed

lemma list_of'_set_next_ref_Node[simp]:
  assumes "list_of' h r xs"
  assumes "Ref.get h p = Node x r'"
  assumes "refs_of' h r rs"
  assumes "p ∉ set rs"
  shows "list_of' (Ref.set p (Node x r) h) p (x#xs) = list_of' h r xs"
using assms
unfolding list_of'_def refs_of'_def'
by (auto simp add: list_of_set_ref Ref.noteq_sym)

lemma refs_of'_set_ref:
  assumes "refs_of' h q rs"
  assumes "p ∉ set rs"
  shows "refs_of' (Ref.set p v h) q as = refs_of' h q as"
using assms
proof -
  from assms have "q ≠ p" by (auto simp only: dest!: refs_of'E)
  with assms show ?thesis
    unfolding refs_of'_def'
    by (auto simp add: refs_of_set_ref)
qed

lemma refs_of'_set_ref2:
  assumes "refs_of' (Ref.set p v h) q rs"
  assumes "p ∉ set rs"
  shows "refs_of' (Ref.set p v h) q as = refs_of' h q as"
using assms
proof -
  from assms have "q ≠ p" by (auto simp only: dest!: refs_of'E)
  with assms show ?thesis
    unfolding refs_of'_def'
    apply auto
    apply (subgoal_tac "prs = prsa")
    apply (insert refs_of_set_ref2[of p v h "Ref.get h q"])
    apply (erule_tac x="prs" in meta_allE)
    apply auto
    apply (auto dest: refs_of_is_fun)
    done
qed

lemma refs_of'_set_next_ref:
assumes "Ref.get h1 p = Node x pn"
assumes "refs_of' (Ref.set p (Node x r1) h1) p rs"
obtains r1s where "rs = (p#r1s)" and "refs_of' h1 r1 r1s"
proof -
  from assms refs_of'_distinct[OF assms(2)] have "∃ r1s. rs = (p # r1s) ∧ refs_of' h1 r1 r1s"
    apply -
    unfolding refs_of'_def'[of _ p]
    apply (auto, frule refs_of_set_ref2) by (auto dest: Ref.noteq_sym)
  with assms that show thesis by auto
qed

section ‹Proving make_llist and traverse correct›

lemma refs_of_invariant:
  assumes "refs_of h (r::('a::heap) node) xs"
  assumes "∀refs. refs_of h r refs ⟶ (∀ref ∈ set refs. Ref.present h ref ∧ Ref.present h' ref ∧ Ref.get h ref = Ref.get h' ref)"
  shows "refs_of h' r xs"
using assms
proof (induct xs arbitrary: r)
  case Nil thus ?case by simp
next
  case (Cons x xs')
  from Cons(2) obtain v where Node: "r = Node v x" by (cases r, auto)
  from Cons(2) Node have refs_of_next: "refs_of h (Ref.get h x) xs'" by simp
  from Cons(2-3) Node have ref_eq: "Ref.get h x = Ref.get h' x" by auto
  from ref_eq refs_of_next have 1: "refs_of h (Ref.get h' x) xs'" by simp
  from Cons(2) Cons(3) have "∀ref ∈ set xs'. Ref.present h ref ∧ Ref.present h' ref ∧ Ref.get h ref = Ref.get h' ref"
    by fastforce
  with Cons(3) 1 have 2: "∀refs. refs_of h (Ref.get h' x) refs ⟶ (∀ref ∈ set refs. Ref.present h ref ∧ Ref.present h' ref ∧ Ref.get h ref = Ref.get h' ref)"
    by (fastforce dest: refs_of_is_fun)
  from Cons.hyps[OF 1 2] have "refs_of h' (Ref.get h' x) xs'" .
  with Node show ?case by simp
qed

lemma refs_of'_invariant:
  assumes "refs_of' h r xs"
  assumes "∀refs. refs_of' h r refs ⟶ (∀ref ∈ set refs. Ref.present h ref ∧ Ref.present h' ref ∧ Ref.get h ref = Ref.get h' ref)"
  shows "refs_of' h' r xs"
using assms
proof -
  from assms obtain prs where refs:"refs_of h (Ref.get h r) prs" and xs_def: "xs = r # prs"
    unfolding refs_of'_def' by auto
  from xs_def assms have x_eq: "Ref.get h r = Ref.get h' r" by fastforce
  from refs assms xs_def have 2: "∀refs. refs_of h (Ref.get h r) refs ⟶
     (∀ref∈set refs. Ref.present h ref ∧ Ref.present h' ref ∧ Ref.get h ref = Ref.get h' ref)" 
    by (fastforce dest: refs_of_is_fun)
  from refs_of_invariant [OF refs 2] xs_def x_eq show ?thesis
    unfolding refs_of'_def' by auto
qed

lemma list_of_invariant:
  assumes "list_of h (r::('a::heap) node) xs"
  assumes "∀refs. refs_of h r refs ⟶ (∀ref ∈ set refs. Ref.present h ref ∧ Ref.present h' ref ∧ Ref.get h ref = Ref.get h' ref)"
  shows "list_of h' r xs"
using assms
proof (induct xs arbitrary: r)
  case Nil thus ?case by simp
next
  case (Cons x xs')

  from Cons(2) obtain ref where Node: "r = Node x ref"
    by (cases r, auto)
  from Cons(2) obtain rs where rs_def: "refs_of h r rs" by (rule list_of_refs_of)
  from Node rs_def obtain rss where refs_of: "refs_of h r (ref#rss)" and rss_def: "rs = ref#rss" by auto
  from Cons(3) Node refs_of have ref_eq: "Ref.get h ref = Ref.get h' ref"
    by auto
  from Cons(2) ref_eq Node have 1: "list_of h (Ref.get h' ref) xs'" by simp
  from refs_of Node ref_eq have refs_of_ref: "refs_of h (Ref.get h' ref) rss" by simp
  from Cons(3) rs_def have rs_heap_eq: "∀ref∈set rs. Ref.present h ref ∧ Ref.present h' ref ∧ Ref.get h ref = Ref.get h' ref" by simp
  from refs_of_ref rs_heap_eq rss_def have 2: "∀refs. refs_of h (Ref.get h' ref) refs ⟶
          (∀ref∈set refs. Ref.present h ref ∧ Ref.present h' ref ∧ Ref.get h ref = Ref.get h' ref)"
    by (auto dest: refs_of_is_fun)
  from Cons(1)[OF 1 2]
  have "list_of h' (Ref.get h' ref) xs'" .
  with Node show ?case
    unfolding list_of'_def
    by simp
qed

lemma effect_ref:
  assumes "effect (ref v) h h' x"
  obtains "Ref.get h' x = v"
  and "¬ Ref.present h x"
  and "Ref.present h' x"
  and "∀y. Ref.present h y ⟶ Ref.get h y = Ref.get h' y"
 (* and "lim h' = Suc (lim h)" *)
  and "∀y. Ref.present h y ⟶ Ref.present h' y"
  using assms
  unfolding Ref.ref_def
  apply (elim effect_heapE)
  unfolding Ref.alloc_def
  apply (simp add: Let_def)
  unfolding Ref.present_def
  apply auto
  unfolding Ref.get_def Ref.set_def
  apply auto
  done

lemma make_llist:
assumes "effect (make_llist xs) h h' r"
shows "list_of h' r xs ∧ (∀rs. refs_of h' r rs ⟶ (∀ref ∈ (set rs). Ref.present h' ref))"
using assms 
proof (induct xs arbitrary: h h' r)
  case Nil thus ?case by (auto elim: effect_returnE simp add: make_llist.simps)
next
  case (Cons x xs')
  from Cons.prems obtain h1 r1 r' where make_llist: "effect (make_llist xs') h h1 r1"
    and effect_refnew:"effect (ref r1) h1 h' r'" and Node: "r = Node x r'"
    unfolding make_llist.simps
    by (auto elim!: effect_bindE effect_returnE)
  from Cons.hyps[OF make_llist] have list_of_h1: "list_of h1 r1 xs'" ..
  from Cons.hyps[OF make_llist] obtain rs' where rs'_def: "refs_of h1 r1 rs'" by (auto intro: list_of_refs_of)
  from Cons.hyps[OF make_llist] rs'_def have refs_present: "∀ref∈set rs'. Ref.present h1 ref" by simp
  from effect_refnew rs'_def refs_present have refs_unchanged: "∀refs. refs_of h1 r1 refs ⟶
         (∀ref∈set refs. Ref.present h1 ref ∧ Ref.present h' ref ∧ Ref.get h1 ref = Ref.get h' ref)"
    by (auto elim!: effect_ref dest: refs_of_is_fun)
  with list_of_invariant[OF list_of_h1 refs_unchanged] Node effect_refnew have fstgoal: "list_of h' r (x # xs')"
    unfolding list_of.simps
    by (auto elim!: effect_refE)
  from refs_unchanged rs'_def have refs_still_present: "∀ref∈set rs'. Ref.present h' ref" by auto
  from refs_of_invariant[OF rs'_def refs_unchanged] refs_unchanged Node effect_refnew refs_still_present
  have sndgoal: "∀rs. refs_of h' r rs ⟶ (∀ref∈set rs. Ref.present h' ref)"
    by (fastforce elim!: effect_refE dest: refs_of_is_fun)
  from fstgoal sndgoal show ?case ..
qed

lemma traverse: "list_of h n r ⟹ effect (traverse n) h h r"
proof (induct r arbitrary: n)
  case Nil
  thus ?case
    by (auto intro: effect_returnI)
next
  case (Cons x xs)
  thus ?case
  apply (cases n, auto)
  by (auto intro!: effect_bindI effect_returnI effect_lookupI)
qed

lemma traverse_make_llist':
  assumes effect: "effect (make_llist xs ⤜ traverse) h h' r"
  shows "r = xs"
proof -
  from effect obtain h1 r1
    where makell: "effect (make_llist xs) h h1 r1"
    and trav: "effect (traverse r1) h1 h' r"
    by (auto elim!: effect_bindE)
  from make_llist[OF makell] have "list_of h1 r1 xs" ..
  from traverse [OF this] trav show ?thesis
    using effect_deterministic by fastforce
qed

section ‹Proving correctness of in-place reversal›

subsection ‹Definition of in-place reversal›

partial_function (heap) rev' :: "('a::heap) node ref ⇒ 'a node ref ⇒ 'a node ref Heap"
where
  [code]: "rev' q p =
   do {
     v ← !p;
     (case v of
        Empty ⇒ return q
      | Node x next ⇒
        do {
          p := Node x q;
          rev' p next
        })
    }"
  
primrec rev :: "('a:: heap) node ⇒ 'a node Heap" 
where
  "rev Empty = return Empty"
| "rev (Node x n) = do { q ← ref Empty; p ← ref (Node x n); v ← rev' q p; !v }"

subsection ‹Correctness Proof›

lemma rev'_invariant:
  assumes "effect (rev' q p) h h' v"
  assumes "list_of' h q qs"
  assumes "list_of' h p ps"
  assumes "∀qrs prs. refs_of' h q qrs ∧ refs_of' h p prs ⟶ set prs ∩ set qrs = {}"
  shows "∃vs. list_of' h' v vs ∧ vs = (List.rev ps) @ qs"
using assms
proof (induct ps arbitrary: qs p q h)
  case Nil
  thus ?case
    unfolding rev'.simps[of q p] list_of'_def
    by (auto elim!: effect_bindE effect_lookupE effect_returnE)
next
  case (Cons x xs)
  (*"LinkedList.list_of h' (get_ref v h') (List.rev xs @ x # qsa)"*)
  from Cons(4) obtain ref where 
    p_is_Node: "Ref.get h p = Node x ref"
    (*and "ref_present ref h"*)
    and list_of'_ref: "list_of' h ref xs"
    unfolding list_of'_def by (cases "Ref.get h p", auto)
  from p_is_Node Cons(2) have effect_rev': "effect (rev' p ref) (Ref.set p (Node x q) h) h' v"
    by (auto simp add: rev'.simps [of q p] elim!: effect_bindE effect_lookupE effect_updateE)
  from Cons(3) obtain qrs where qrs_def: "refs_of' h q qrs" by (elim list_of'_refs_of')
  from Cons(4) obtain prs where prs_def: "refs_of' h p prs" by (elim list_of'_refs_of')
  from qrs_def prs_def Cons(5) have distinct_pointers: "set qrs ∩ set prs = {}" by fastforce
  from qrs_def prs_def distinct_pointers refs_of'E have p_notin_qrs: "p ∉ set qrs" by fastforce
  from Cons(3) qrs_def this have 1: "list_of' (Ref.set p (Node x q) h) p (x#qs)"
    unfolding list_of'_def  
    apply (simp)
    unfolding list_of'_def[symmetric]
    by (simp add: list_of'_set_ref)
  from list_of'_refs_of'2[OF Cons(4)] p_is_Node prs_def obtain refs where refs_def: "refs_of' h ref refs" and prs_refs: "prs = p # refs"
    unfolding refs_of'_def' by auto
  from prs_refs prs_def have p_not_in_refs: "p ∉ set refs"
    by (fastforce dest!: refs_of'_distinct)
  with refs_def p_is_Node list_of'_ref have 2: "list_of' (Ref.set p (Node x q) h) ref xs"
    by (auto simp add: list_of'_set_ref)
  from p_notin_qrs qrs_def have refs_of1: "refs_of' (Ref.set p (Node x q) h) p (p#qrs)"
    unfolding refs_of'_def'
    apply (simp)
    unfolding refs_of'_def'[symmetric]
    by (simp add: refs_of'_set_ref)
  from p_not_in_refs p_is_Node refs_def have refs_of2: "refs_of' (Ref.set p (Node x q) h) ref refs"
    by (simp add: refs_of'_set_ref)
  from p_not_in_refs refs_of1 refs_of2 distinct_pointers prs_refs have 3: "∀qrs prs. refs_of' (Ref.set p (Node x q) h) p qrs ∧ refs_of' (Ref.set p (Node x q) h) ref prs ⟶ set prs ∩ set qrs = {}"
    apply - apply (rule allI)+ apply (rule impI) apply (erule conjE)
    apply (drule refs_of'_is_fun) back back apply assumption
    apply (drule refs_of'_is_fun) back back apply assumption
    apply auto done
  from Cons.hyps [OF effect_rev' 1 2 3] show ?case by simp
qed


lemma rev_correctness:
  assumes list_of_h: "list_of h r xs"
  assumes validHeap: "∀refs. refs_of h r refs ⟶ (∀r ∈ set refs. Ref.present h r)"
  assumes effect_rev: "effect (rev r) h h' r'"
  shows "list_of h' r' (List.rev xs)"
using assms
proof (cases r)
  case Empty
  with list_of_h effect_rev show ?thesis
    by (auto simp add: list_of_Empty elim!: effect_returnE)
next
  case (Node x ps)
  with effect_rev obtain p q h1 h2 h3 v where
    init: "effect (ref Empty) h h1 q"
    "effect (ref (Node x ps)) h1 h2 p"
    and effect_rev':"effect (rev' q p) h2 h3 v"
    and lookup: "effect (!v) h3 h' r'"
    using rev.simps
    by (auto elim!: effect_bindE)
  from init have a1:"list_of' h2 q []"
    unfolding list_of'_def
    by (auto elim!: effect_ref)
  from list_of_h obtain refs where refs_def: "refs_of h r refs" by (rule list_of_refs_of)
  from validHeap init refs_def have heap_eq: "∀refs. refs_of h r refs ⟶ (∀ref∈set refs. Ref.present h ref ∧ Ref.present h2 ref ∧ Ref.get h ref = Ref.get h2 ref)"
    by (fastforce elim!: effect_ref dest: refs_of_is_fun)
  from list_of_invariant[OF list_of_h heap_eq] have "list_of h2 r xs" .
  from init this Node have a2: "list_of' h2 p xs"
    apply -
    unfolding list_of'_def
    apply (auto elim!: effect_refE)
    done
  from init have refs_of_q: "refs_of' h2 q [q]"
    by (auto elim!: effect_ref)
  from refs_def Node have refs_of'_ps: "refs_of' h ps refs"
    by (auto simp add: refs_of'_def'[symmetric])
  from validHeap refs_def have all_ref_present: "∀r∈set refs. Ref.present h r" by simp
  from init refs_of'_ps this
    have heap_eq: "∀refs. refs_of' h ps refs ⟶ (∀ref∈set refs. Ref.present h ref ∧ Ref.present h2 ref ∧ Ref.get h ref = Ref.get h2 ref)"
    by (auto elim!: effect_ref [where ?'a="'a node", where ?'b="'a node", where ?'c="'a node"] dest: refs_of'_is_fun)
  from refs_of'_invariant[OF refs_of'_ps this] have "refs_of' h2 ps refs" .
  with init have refs_of_p: "refs_of' h2 p (p#refs)"
    by (auto elim!: effect_refE simp add: refs_of'_def')
  with init all_ref_present have q_is_new: "q ∉ set (p#refs)"
    by (auto elim!: effect_refE intro!: Ref.noteq_I)
  from refs_of_p refs_of_q q_is_new have a3: "∀qrs prs. refs_of' h2 q qrs ∧ refs_of' h2 p prs ⟶ set prs ∩ set qrs = {}"
    by (fastforce simp only: list.set dest: refs_of'_is_fun)
  from rev'_invariant [OF effect_rev' a1 a2 a3] have "list_of h3 (Ref.get h3 v) (List.rev xs)" 
    unfolding list_of'_def by auto
  with lookup show ?thesis
    by (auto elim: effect_lookupE)
qed


section ‹The merge function on Linked Lists›
text ‹We also prove merge correct›

text‹First, we define merge on lists in a natural way.›

fun Lmerge :: "('a::ord) list ⇒ 'a list ⇒ 'a list"
where
  "Lmerge (x#xs) (y#ys) =
     (if x ≤ y then x # Lmerge xs (y#ys) else y # Lmerge (x#xs) ys)"
| "Lmerge [] ys = ys"
| "Lmerge xs [] = xs"

subsection ‹Definition of merge function›

partial_function (heap) merge :: "('a::{heap, ord}) node ref ⇒ 'a node ref ⇒ 'a node ref Heap"
where
[code]: "merge p q = (do { v ← !p; w ← !q;
  (case v of Empty ⇒ return q
          | Node valp np ⇒
            (case w of Empty ⇒ return p
                     | Node valq nq ⇒
                       if (valp ≤ valq) then do {
                         npq ← merge np q;
                         p := Node valp npq;
                         return p }
                       else do {
                         pnq ← merge p nq;
                         q := Node valq pnq;
                         return q }))})"


lemma if_return: "(if P then return x else return y) = return (if P then x else y)"
by auto

lemma if_distrib_App: "(if P then f else g) x = (if P then f x else g x)"
by auto
lemma redundant_if: "(if P then (if P then x else z) else y) = (if P then x else y)"
  "(if P then x else (if P then z else y)) = (if P then x else y)"
by auto



lemma sum_distrib: "case_sum fl fr (case x of Empty ⇒ y | Node v n ⇒ (z v n)) = (case x of Empty ⇒ case_sum fl fr y | Node v n ⇒ case_sum fl fr (z v n))"
by (cases x) auto

subsection ‹Induction refinement by applying the abstraction function to our induct rule›

text ‹From our original induction rule Lmerge.induct, we derive a new rule with our list_of' predicate›

lemma merge_induct2:
  assumes "list_of' h (p::'a::{heap, ord} node ref) xs"
  assumes "list_of' h q ys"
  assumes "⋀ ys p q. ⟦ list_of' h p []; list_of' h q ys; Ref.get h p = Empty ⟧ ⟹ P p q [] ys"
  assumes "⋀ x xs' p q pn. ⟦ list_of' h p (x#xs'); list_of' h q []; Ref.get h p = Node x pn; Ref.get h q = Empty ⟧ ⟹ P p q (x#xs') []"
  assumes "⋀ x xs' y ys' p q pn qn.
  ⟦ list_of' h p (x#xs'); list_of' h q (y#ys'); Ref.get h p = Node x pn; Ref.get h q = Node y qn;
  x ≤ y; P pn q xs' (y#ys') ⟧
  ⟹ P p q (x#xs') (y#ys')"
  assumes "⋀ x xs' y ys' p q pn qn.
  ⟦ list_of' h p (x#xs'); list_of' h q (y#ys'); Ref.get h p = Node x pn; Ref.get h q = Node y qn;
  ¬ x ≤ y; P p qn (x#xs') ys'⟧
  ⟹ P p q (x#xs') (y#ys')"
  shows "P p q xs ys"
using assms(1-2)
proof (induct xs ys arbitrary: p q rule: Lmerge.induct)
  case (2 ys)
  from 2(1) have "Ref.get h p = Empty" unfolding list_of'_def by simp
  with 2(1-2) assms(3) show ?case by blast
next
  case (3 x xs')
  from 3(1) obtain pn where Node: "Ref.get h p = Node x pn" by (rule list_of'_Cons)
  from 3(2) have "Ref.get h q = Empty" unfolding list_of'_def by simp
  with Node 3(1-2) assms(4) show ?case by blast
next
  case (1 x xs' y ys')
  from 1(3) obtain pn where pNode:"Ref.get h p = Node x pn"
    and list_of'_pn: "list_of' h pn xs'" by (rule list_of'_Cons)
  from 1(4) obtain qn where qNode:"Ref.get h q = Node y qn"
    and  list_of'_qn: "list_of' h qn ys'" by (rule list_of'_Cons)
  show ?case
  proof (cases "x ≤ y")
    case True
    from 1(1)[OF True list_of'_pn 1(4)] assms(5) 1(3-4) pNode qNode True
    show ?thesis by blast
  next
    case False
    from 1(2)[OF False 1(3) list_of'_qn] assms(6) 1(3-4) pNode qNode False
    show ?thesis by blast
  qed
qed


text ‹secondly, we add the effect statement in the premise, and derive the effect statements for the single cases which we then eliminate with our effect elim rules.›
  
lemma merge_induct3: 
assumes  "list_of' h p xs"
assumes  "list_of' h q ys"
assumes  "effect (merge p q) h h' r"
assumes  "⋀ ys p q. ⟦ list_of' h p []; list_of' h q ys; Ref.get h p = Empty ⟧ ⟹ P p q h h q [] ys"
assumes  "⋀ x xs' p q pn. ⟦ list_of' h p (x#xs'); list_of' h q []; Ref.get h p = Node x pn; Ref.get h q = Empty ⟧ ⟹ P p q h h p (x#xs') []"
assumes  "⋀ x xs' y ys' p q pn qn h1 r1 h'.
  ⟦ list_of' h p (x#xs'); list_of' h q (y#ys');Ref.get h p = Node x pn; Ref.get h q = Node y qn;
  x ≤ y; effect (merge pn q) h h1 r1 ; P pn q h h1 r1 xs' (y#ys'); h' = Ref.set p (Node x r1) h1 ⟧
  ⟹ P p q h h' p (x#xs') (y#ys')"
assumes "⋀ x xs' y ys' p q pn qn h1 r1 h'.
  ⟦ list_of' h p (x#xs'); list_of' h q (y#ys'); Ref.get h p = Node x pn; Ref.get h q = Node y qn;
  ¬ x ≤ y; effect (merge p qn) h h1 r1; P p qn h h1 r1 (x#xs') ys'; h' = Ref.set q (Node y r1) h1 ⟧
  ⟹ P p q h h' q (x#xs') (y#ys')"
shows "P p q h h' r xs ys"
using assms(3)
proof (induct arbitrary: h' r rule: merge_induct2[OF assms(1) assms(2)])
  case (1 ys p q)
  from 1(3-4) have "h = h' ∧ r = q"
    unfolding merge.simps[of p q]
    by (auto elim!: effect_lookupE effect_bindE effect_returnE)
  with assms(4)[OF 1(1) 1(2) 1(3)] show ?case by simp
next
  case (2 x xs' p q pn)
  from 2(3-5) have "h = h' ∧ r = p"
    unfolding merge.simps[of p q]
    by (auto elim!: effect_lookupE effect_bindE effect_returnE)
  with assms(5)[OF 2(1-4)] show ?case by simp
next
  case (3 x xs' y ys' p q pn qn)
  from 3(3-5) 3(7) obtain h1 r1 where
    1: "effect (merge pn q) h h1 r1" 
    and 2: "h' = Ref.set p (Node x r1) h1 ∧ r = p"
    unfolding merge.simps[of p q]
    by (auto elim!: effect_lookupE effect_bindE effect_returnE effect_ifE effect_updateE)
  from 3(6)[OF 1] assms(6) [OF 3(1-5)] 1 2 show ?case by simp
next
  case (4 x xs' y ys' p q pn qn)
  from 4(3-5) 4(7) obtain h1 r1 where
    1: "effect (merge p qn) h h1 r1" 
    and 2: "h' = Ref.set q (Node y r1) h1 ∧ r = q"
    unfolding merge.simps[of p q]
    by (auto elim!: effect_lookupE effect_bindE effect_returnE effect_ifE effect_updateE)
  from 4(6)[OF 1] assms(7) [OF 4(1-5)] 1 2 show ?case by simp
qed


subsection ‹Proving merge correct›

text ‹As many parts of the following three proofs are identical, we could actually move the
same reasoning into an extended induction rule›
 
lemma merge_unchanged:
  assumes "refs_of' h p xs"
  assumes "refs_of' h q ys"  
  assumes "effect (merge p q) h h' r'"
  assumes "set xs ∩ set ys = {}"
  assumes "r ∉ set xs ∪ set ys"
  shows "Ref.get h r = Ref.get h' r"
proof -
  from assms(1) obtain ps where ps_def: "list_of' h p ps" by (rule refs_of'_list_of')
  from assms(2) obtain qs where qs_def: "list_of' h q qs" by (rule refs_of'_list_of')
  show ?thesis using assms(1) assms(2) assms(4) assms(5)
  proof (induct arbitrary: xs ys r rule: merge_induct3[OF ps_def qs_def assms(3)])
    case 1 thus ?case by simp
  next
    case 2 thus ?case by simp
  next
    case (3 x xs' y ys' p q pn qn h1 r1 h' xs ys r)
    from 3(9) 3(3) obtain pnrs
      where pnrs_def: "xs = p#pnrs"
      and refs_of'_pn: "refs_of' h pn pnrs"
      by (rule refs_of'_Node)
    with 3(12) have r_in: "r ∉ set pnrs ∪ set ys" by auto
    from pnrs_def 3(12) have "r ≠ p" by auto
    with 3(11) 3(12) pnrs_def refs_of'_distinct[OF 3(9)] have p_in: "p ∉ set pnrs ∪ set ys" by auto
    from 3(11) pnrs_def have no_inter: "set pnrs ∩ set ys = {}" by auto
    from 3(7)[OF refs_of'_pn 3(10) this p_in] 3(3) have p_is_Node: "Ref.get h1 p = Node x pn"
      by simp
    from 3(7)[OF refs_of'_pn 3(10) no_inter r_in] 3(8) ‹r ≠ p› show ?case
      by simp
  next
    case (4 x xs' y ys' p q pn qn h1 r1 h' xs ys r)
    from 4(10) 4(4) obtain qnrs
      where qnrs_def: "ys = q#qnrs"
      and refs_of'_qn: "refs_of' h qn qnrs"
      by (rule refs_of'_Node)
    with 4(12) have r_in: "r ∉ set xs ∪ set qnrs" by auto
    from qnrs_def 4(12) have "r ≠ q" by auto
    with 4(11) 4(12) qnrs_def refs_of'_distinct[OF 4(10)] have q_in: "q ∉ set xs ∪ set qnrs" by auto
    from 4(11) qnrs_def have no_inter: "set xs ∩ set qnrs = {}" by auto
    from 4(7)[OF 4(9) refs_of'_qn this q_in] 4(4) have q_is_Node: "Ref.get h1 q = Node y qn" by simp
    from 4(7)[OF 4(9) refs_of'_qn no_inter r_in] 4(8) ‹r ≠ q› show ?case
      by simp
  qed
qed

lemma refs_of'_merge:
  assumes "refs_of' h p xs"
  assumes "refs_of' h q ys"
  assumes "effect (merge p q) h h' r"
  assumes "set xs ∩ set ys = {}"
  assumes "refs_of' h' r rs"
  shows "set rs ⊆ set xs ∪ set ys"
proof -
  from assms(1) obtain ps where ps_def: "list_of' h p ps" by (rule refs_of'_list_of')
  from assms(2) obtain qs where qs_def: "list_of' h q qs" by (rule refs_of'_list_of')
  show ?thesis using assms(1) assms(2) assms(4) assms(5)
  proof (induct arbitrary: xs ys rs rule: merge_induct3[OF ps_def qs_def assms(3)])
    case 1
    from 1(5) 1(7) have "rs = ys" by (fastforce simp add: refs_of'_is_fun)
    thus ?case by auto
  next
    case 2
    from 2(5) 2(8) have "rs = xs" by (auto simp add: refs_of'_is_fun)
    thus ?case by auto
  next
    case (3 x xs' y ys' p q pn qn h1 r1 h' xs ys rs)
    from 3(9) 3(3) obtain pnrs
      where pnrs_def: "xs = p#pnrs"
      and refs_of'_pn: "refs_of' h pn pnrs"
      by (rule refs_of'_Node)
    from 3(10) 3(9) 3(11) pnrs_def refs_of'_distinct[OF 3(9)] have p_in: "p ∉ set pnrs ∪ set ys" by auto
    from 3(11) pnrs_def have no_inter: "set pnrs ∩ set ys = {}" by auto
    from merge_unchanged[OF refs_of'_pn 3(10) 3(6) no_inter p_in] have p_stays: "Ref.get h1 p = Ref.get h p" ..
    from 3 p_stays obtain r1s
      where rs_def: "rs = p#r1s" and refs_of'_r1:"refs_of' h1 r1 r1s"
      by (auto elim: refs_of'_set_next_ref)
    from 3(7)[OF refs_of'_pn 3(10) no_inter refs_of'_r1] rs_def pnrs_def show ?case by auto
  next
    case (4 x xs' y ys' p q pn qn h1 r1 h' xs ys rs)
    from 4(10) 4(4) obtain qnrs
      where qnrs_def: "ys = q#qnrs"
      and refs_of'_qn: "refs_of' h qn qnrs"
      by (rule refs_of'_Node)
    from 4(10) 4(9) 4(11) qnrs_def refs_of'_distinct[OF 4(10)] have q_in: "q ∉ set xs ∪ set qnrs" by auto
    from 4(11) qnrs_def have no_inter: "set xs ∩ set qnrs = {}" by auto
    from merge_unchanged[OF 4(9) refs_of'_qn 4(6) no_inter q_in] have q_stays: "Ref.get h1 q = Ref.get h q" ..
    from 4 q_stays obtain r1s
      where rs_def: "rs = q#r1s" and refs_of'_r1:"refs_of' h1 r1 r1s"
      by (auto elim: refs_of'_set_next_ref)
    from 4(7)[OF 4(9) refs_of'_qn no_inter refs_of'_r1] rs_def qnrs_def show ?case by auto
  qed
qed

lemma
  assumes "list_of' h p xs"
  assumes "list_of' h q ys"
  assumes "effect (merge p q) h h' r"
  assumes "∀qrs prs. refs_of' h q qrs ∧ refs_of' h p prs ⟶ set prs ∩ set qrs = {}"
  shows "list_of' h' r (Lmerge xs ys)"
using assms(4)
proof (induct rule: merge_induct3[OF assms(1-3)])
  case 1
  thus ?case by simp
next
  case 2
  thus ?case by simp
next
  case (3 x xs' y ys' p q pn qn h1 r1 h')
  from 3(1) obtain prs where prs_def: "refs_of' h p prs" by (rule list_of'_refs_of')
  from 3(2) obtain qrs where qrs_def: "refs_of' h q qrs" by (rule list_of'_refs_of')
  from prs_def 3(3) obtain pnrs
    where pnrs_def: "prs = p#pnrs"
    and refs_of'_pn: "refs_of' h pn pnrs"
    by (rule refs_of'_Node)
  from prs_def qrs_def 3(9) pnrs_def refs_of'_distinct[OF prs_def] have p_in: "p ∉ set pnrs ∪ set qrs" by fastforce
  from prs_def qrs_def 3(9) pnrs_def have no_inter: "set pnrs ∩ set qrs = {}" by fastforce
  from no_inter refs_of'_pn qrs_def have no_inter2: "∀qrs prs. refs_of' h q qrs ∧ refs_of' h pn prs ⟶ set prs ∩ set qrs = {}"
    by (fastforce dest: refs_of'_is_fun)
  from merge_unchanged[OF refs_of'_pn qrs_def 3(6) no_inter p_in] have p_stays: "Ref.get h1 p = Ref.get h p" ..
  from 3(7)[OF no_inter2] obtain rs where rs_def: "refs_of' h1 r1 rs" by (rule list_of'_refs_of')
  from refs_of'_merge[OF refs_of'_pn qrs_def 3(6) no_inter this] p_in have p_rs: "p ∉ set rs" by auto
  with 3(7)[OF no_inter2] 3(1-5) 3(8) p_rs rs_def p_stays
  show ?case by (auto simp: list_of'_set_ref)
next
  case (4 x xs' y ys' p q pn qn h1 r1 h')
  from 4(1) obtain prs where prs_def: "refs_of' h p prs" by (rule list_of'_refs_of')
  from 4(2) obtain qrs where qrs_def: "refs_of' h q qrs" by (rule list_of'_refs_of')
  from qrs_def 4(4) obtain qnrs
    where qnrs_def: "qrs = q#qnrs"
    and refs_of'_qn: "refs_of' h qn qnrs"
    by (rule refs_of'_Node)
  from prs_def qrs_def 4(9) qnrs_def refs_of'_distinct[OF qrs_def] have q_in: "q ∉ set prs ∪ set qnrs" by fastforce
  from prs_def qrs_def 4(9) qnrs_def have no_inter: "set prs ∩ set qnrs = {}" by fastforce
  from no_inter refs_of'_qn prs_def have no_inter2: "∀qrs prs. refs_of' h qn qrs ∧ refs_of' h p prs ⟶ set prs ∩ set qrs = {}"
    by (fastforce dest: refs_of'_is_fun)
  from merge_unchanged[OF prs_def refs_of'_qn 4(6) no_inter q_in] have q_stays: "Ref.get h1 q = Ref.get h q" ..
  from 4(7)[OF no_inter2] obtain rs where rs_def: "refs_of' h1 r1 rs" by (rule list_of'_refs_of')
  from refs_of'_merge[OF prs_def refs_of'_qn 4(6) no_inter this] q_in have q_rs: "q ∉ set rs" by auto
  with 4(7)[OF no_inter2] 4(1-5) 4(8) q_rs rs_def q_stays
  show ?case by (auto simp: list_of'_set_ref)
qed

section ‹Code generation›

text ‹A simple example program›

definition test_1 where "test_1 = (do { ll_xs ← make_llist [1..(15::int)]; xs ← traverse ll_xs; return xs })" 
definition test_2 where "test_2 = (do { ll_xs ← make_llist [1..(15::int)]; ll_ys ← rev ll_xs; ys ← traverse ll_ys; return ys })"

definition test_3 where "test_3 =
  (do {
    ll_xs ← make_llist (filter (%n. n mod 2 = 0) [2..8]);
    ll_ys ← make_llist (filter (%n. n mod 2 = 1) [5..11]);
    r ← ref ll_xs;
    q ← ref ll_ys;
    p ← merge r q;
    ll_zs ← !p;
    zs ← traverse ll_zs;
    return zs
  })"

code_reserved SML upto

ML_val ‹@{code test_1} ()›
ML_val ‹@{code test_2} ()›
ML_val ‹@{code test_3} ()›

export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp

end