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

section ‹Linked Lists by ML references›

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

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'
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'
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 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
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]
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"
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]
from p_not_in_refs p_is_Node refs_def have refs_of2: "refs_of' (Ref.set p (Node x q) h) ref refs"
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"
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
```