# Theory Pointers0

theory Pointers0
imports Hoare_Logic
```(*  Title:      HOL/Hoare/Pointers0.thy
Author:     Tobias Nipkow

This is like Pointers.thy, but instead of a type constructor 'a ref
that adjoins Null to a type, Null is simply a distinguished element of
the address type. This avoids the Ref constructor and thus simplifies
specifications (a bit). However, the proofs don't seem to get simpler
- in fact in some case they appear to get (a bit) more complicated.
*)

theory Pointers0 imports Hoare_Logic begin

subsection "References"

class ref =
fixes Null :: 'a

subsection "Field access and update"

syntax
"_fassign"  :: "'a::ref => id => 'v => 's com"
("(2_^._ :=/ _)" [70,1000,65] 61)
"_faccess"  :: "'a::ref => ('a::ref ⇒ 'v) => 'v"
("_^._" [65,1000] 65)
translations
"p^.f := e"  =>  "f := CONST fun_upd f p e"
"p^.f"       =>  "f p"

text "An example due to Suzuki:"

lemma "VARS v n
{distinct[w,x,y,z]}
w^.v := (1::int); w^.n := x;
x^.v := 2; x^.n := y;
y^.v := 3; y^.n := z;
z^.v := 4; x^.n := z
{w^.n^.n^.v = 4}"
by vcg_simp

section "The heap"

subsection "Paths in the heap"

primrec Path :: "('a::ref ⇒ 'a) ⇒ 'a ⇒ 'a list ⇒ 'a ⇒ bool"
where
"Path h x [] y = (x = y)"
| "Path h x (a#as) y = (x ≠ Null ∧ x = a ∧ Path h (h a) as y)"

lemma [iff]: "Path h Null xs y = (xs = [] ∧ y = Null)"
apply(case_tac xs)
apply fastforce
apply fastforce
done

lemma [simp]: "a ≠ Null ⟹ Path h a as z =
(as = [] ∧ z = a  ∨  (∃bs. as = a#bs ∧ Path h (h a) bs z))"
apply(case_tac as)
apply fastforce
apply fastforce
done

lemma [simp]: "⋀x. Path f x (as@bs) z = (∃y. Path f x as y ∧ Path f y bs z)"
by(induct as, simp+)

lemma [simp]: "⋀x. u ∉ set as ⟹ Path (f(u := v)) x as y = Path f x as y"

subsection "Lists on the heap"

subsubsection "Relational abstraction"

definition List :: "('a::ref ⇒ 'a) ⇒ 'a ⇒ 'a list ⇒ bool"
where "List h x as = Path h x as Null"

lemma [simp]: "List h x [] = (x = Null)"

lemma [simp]: "List h x (a#as) = (x ≠ Null ∧ x = a ∧ List h (h a) as)"

lemma [simp]: "List h Null as = (as = [])"
by(case_tac as, simp_all)

lemma List_Ref[simp]:
"a ≠ Null ⟹ List h a as = (∃bs. as = a#bs ∧ List h (h a) bs)"
by(case_tac as, simp_all, fast)

theorem notin_List_update[simp]:
"⋀x. a ∉ set as ⟹ List (h(a := y)) x as = List h x as"
apply(induct as)
apply simp
done

declare fun_upd_apply[simp del]fun_upd_same[simp] fun_upd_other[simp]

lemma List_unique: "⋀x bs. List h x as ⟹ List h x bs ⟹ as = bs"
by(induct as, simp, clarsimp)

lemma List_unique1: "List h p as ⟹ ∃!as. List h p as"
by(blast intro:List_unique)

lemma List_app: "⋀x. List h x (as@bs) = (∃y. Path h x as y ∧ List h y bs)"
by(induct as, simp, clarsimp)

lemma List_hd_not_in_tl[simp]: "List h (h a) as ⟹ a ∉ set as"
apply(frule List_app[THEN iffD1])
apply(fastforce dest: List_unique)
done

lemma List_distinct[simp]: "⋀x. List h x as ⟹ distinct as"
apply(induct as, simp)
apply(fastforce dest:List_hd_not_in_tl)
done

subsection "Functional abstraction"

definition islist :: "('a::ref ⇒ 'a) ⇒ 'a ⇒ bool"
where "islist h p ⟷ (∃as. List h p as)"

definition list :: "('a::ref ⇒ 'a) ⇒ 'a ⇒ 'a list"
where "list h p = (SOME as. List h p as)"

lemma List_conv_islist_list: "List h p as = (islist h p ∧ as = list h p)"
apply(rule iffI)
apply(rule conjI)
apply blast
apply(subst some1_equality)
apply(erule List_unique1)
apply assumption
apply(rule refl)
apply simp
apply(rule someI_ex)
apply fast
done

lemma [simp]: "islist h Null"

lemma [simp]: "a ≠ Null ⟹ islist h a = islist h (h a)"

lemma [simp]: "list h Null = []"

lemma list_Ref_conv[simp]:
"⟦ a ≠ Null; islist h (h a) ⟧ ⟹ list h a = a # list h (h a)"
apply(insert List_Ref[of _ h])
apply(fastforce simp:List_conv_islist_list)
done

lemma [simp]: "islist h (h a) ⟹ a ∉ set(list h (h a))"
apply(insert List_hd_not_in_tl[of h])
done

lemma list_upd_conv[simp]:
"islist h p ⟹ y ∉ set(list h p) ⟹ list (h(y := q)) p = list h p"
apply(drule notin_List_update[of _ _ h q p])
done

lemma islist_upd[simp]:
"islist h p ⟹ y ∉ set(list h p) ⟹ islist (h(y := q)) p"
apply(frule notin_List_update[of _ _ h q p])
done

section "Verifications"

subsection "List reversal"

text "A short but unreadable proof:"

lemma "VARS tl p q r
{List tl p Ps ∧ List tl q Qs ∧ set Ps ∩ set Qs = {}}
WHILE p ≠ Null
INV {∃ps qs. List tl p ps ∧ List tl q qs ∧ set ps ∩ set qs = {} ∧
rev ps @ qs = rev Ps @ Qs}
DO r := p; p := p^.tl; r^.tl := q; q := r OD
{List tl q (rev Ps @ Qs)}"
apply vcg_simp
apply fastforce
apply(fastforce intro:notin_List_update[THEN iffD2])
― ‹explicit:›
⌦‹apply clarify›
⌦‹apply(rename_tac ps qs)›
⌦‹apply clarsimp›
⌦‹apply(rename_tac ps')›
⌦‹apply(rule_tac x = ps' in exI)›
⌦‹apply simp›
⌦‹apply(rule_tac x = "p#qs" in exI)›
⌦‹apply simp›
apply fastforce
done

lemma "VARS tl p q r
{List tl p Ps ∧ List tl q Qs ∧ set Ps ∩ set Qs = {}}
WHILE p ≠ Null
INV {∃ps qs. List tl p ps ∧ List tl q qs ∧ set ps ∩ set qs = {} ∧
rev ps @ qs = rev Ps @ Qs}
DO r := p; p := p^.tl; r^.tl := q; q := r OD
{List tl q (rev Ps @ Qs)}"
proof vcg
fix tl p q r
assume "List tl p Ps ∧ List tl q Qs ∧ set Ps ∩ set Qs = {}"
thus "∃ps qs. List tl p ps ∧ List tl q qs ∧ set ps ∩ set qs = {} ∧
rev ps @ qs = rev Ps @ Qs" by fastforce
next
fix tl p q r
assume "(∃ps qs. List tl p ps ∧ List tl q qs ∧ set ps ∩ set qs = {} ∧
rev ps @ qs = rev Ps @ Qs) ∧ p ≠ Null"
(is "(∃ps qs. ?I ps qs) ∧ _")
then obtain ps qs where I: "?I ps qs ∧ p ≠ Null" by fast
then obtain ps' where "ps = p # ps'" by fastforce
hence "List (tl(p := q)) (p^.tl) ps' ∧
List (tl(p := q)) p       (p#qs) ∧
set ps' ∩ set (p#qs) = {} ∧
rev ps' @ (p#qs) = rev Ps @ Qs"
using I by fastforce
thus "∃ps' qs'. List (tl(p := q)) (p^.tl) ps' ∧
List (tl(p := q)) p       qs' ∧
set ps' ∩ set qs' = {} ∧
rev ps' @ qs' = rev Ps @ Qs" by fast
next
fix tl p q r
assume "(∃ps qs. List tl p ps ∧ List tl q qs ∧ set ps ∩ set qs = {} ∧
rev ps @ qs = rev Ps @ Qs) ∧ ¬ p ≠ Null"
thus "List tl q (rev Ps @ Qs)" by fastforce
qed

text‹Finaly, the functional version. A bit more verbose, but automatic!›

lemma "VARS tl p q r
{islist tl p ∧ islist tl q ∧
Ps = list tl p ∧ Qs = list tl q ∧ set Ps ∩ set Qs = {}}
WHILE p ≠ Null
INV {islist tl p ∧ islist tl q ∧
set(list tl p) ∩ set(list tl q) = {} ∧
rev(list tl p) @ (list tl q) = rev Ps @ Qs}
DO r := p; p := p^.tl; r^.tl := q; q := r OD
{islist tl q ∧ list tl q = rev Ps @ Qs}"
apply vcg_simp
apply clarsimp
apply clarsimp
apply clarsimp
done

subsection "Searching in a list"

text‹What follows is a sequence of successively more intelligent proofs that
a simple loop finds an element in a linked list.

We start with a proof based on the @{term List} predicate. This means it only
works for acyclic lists.›

lemma "VARS tl p
{List tl p Ps ∧ X ∈ set Ps}
WHILE p ≠ Null ∧ p ≠ X
INV {p ≠ Null ∧ (∃ps. List tl p ps ∧ X ∈ set ps)}
DO p := p^.tl OD
{p = X}"
apply vcg_simp
apply(case_tac "p = Null")
apply clarsimp
apply fastforce
apply clarsimp
apply fastforce
apply clarsimp
done

text‹Using @{term Path} instead of @{term List} generalizes the correctness
statement to cyclic lists as well:›

lemma "VARS tl p
{Path tl p Ps X}
WHILE p ≠ Null ∧ p ≠ X
INV {∃ps. Path tl p ps X}
DO p := p^.tl OD
{p = X}"
apply vcg_simp
apply blast
apply fastforce
apply clarsimp
done

text‹Now it dawns on us that we do not need the list witness at all --- it
suffices to talk about reachability, i.e.\ we can use relations directly.›

lemma "VARS tl p
{(p,X) ∈ {(x,y). y = tl x & x ≠ Null}⇧*}
WHILE p ≠ Null ∧ p ≠ X
INV {(p,X) ∈ {(x,y). y = tl x & x ≠ Null}⇧*}
DO p := p^.tl OD
{p = X}"
apply vcg_simp
apply clarsimp
apply(erule converse_rtranclE)
apply simp
apply(simp)
apply(fastforce elim:converse_rtranclE)
done

subsection "Merging two lists"

text"This is still a bit rough, especially the proof."

fun merge :: "'a list * 'a list * ('a ⇒ 'a ⇒ bool) ⇒ 'a list" where
"merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
else y # merge(x#xs,ys,f))" |
"merge(x#xs,[],f) = x # merge(xs,[],f)" |
"merge([],y#ys,f) = y # merge([],ys,f)" |
"merge([],[],f) = []"

lemma imp_disjCL: "(P|Q ⟶ R) = ((P ⟶ R) ∧ (~P ⟶ Q ⟶ R))"
by blast

declare disj_not1[simp del] imp_disjL[simp del] imp_disjCL[simp]

lemma "VARS hd tl p q r s
{List tl p Ps ∧ List tl q Qs ∧ set Ps ∩ set Qs = {} ∧
(p ≠ Null ∨ q ≠ Null)}
IF if q = Null then True else p ~= Null & p^.hd ≤ q^.hd
THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI;
s := r;
WHILE p ≠ Null ∨ q ≠ Null
INV {∃rs ps qs. Path tl r rs s ∧ List tl p ps ∧ List tl q qs ∧
distinct(s # ps @ qs @ rs) ∧ s ≠ Null ∧
merge(Ps,Qs,λx y. hd x ≤ hd y) =
rs @ s # merge(ps,qs,λx y. hd x ≤ hd y) ∧
(tl s = p ∨ tl s = q)}
DO IF if q = Null then True else p ≠ Null ∧ p^.hd ≤ q^.hd
THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI;
s := s^.tl
OD
{List tl r (merge(Ps,Qs,λx y. hd x ≤ hd y))}"
apply vcg_simp

apply (fastforce)

apply clarsimp
apply(rule conjI)
apply clarsimp
apply(rule_tac x = "rs @ [s]" in exI)
apply simp
apply(rule_tac x = "bs" in exI)
apply (fastforce simp:eq_sym_conv)

apply clarsimp
apply(rule conjI)
apply clarsimp
apply(rule_tac x = "rs @ [s]" in exI)
apply simp
apply(rule_tac x = "bsa" in exI)
apply(rule conjI)
apply(rule exI)
apply(rule conjI)
apply(rule_tac x = bs in exI)
apply(rule conjI)
apply(rule refl)

apply(rule conjI)
apply clarsimp
apply(rule_tac x = "rs @ [s]" in exI)
apply simp
apply(rule_tac x = bs in exI)
apply clarsimp
apply(rule_tac x = "rs @ [s]" in exI)
apply(rule exI)
apply(rule conjI)
apply(rule_tac x = bsa in exI)
apply(rule conjI)
apply(rule refl)
apply(rule_tac x = bs in exI)

done

(* TODO: merging with islist/list instead of List: an improvement?
needs (is)path, which is not so easy to prove either. *)

subsection "Storage allocation"

definition new :: "'a set ⇒ 'a::ref"
where "new A = (SOME a. a ∉ A & a ≠ Null)"

lemma new_notin:
"⟦ ~finite(UNIV::('a::ref)set); finite(A::'a set); B ⊆ A ⟧ ⟹
new (A) ∉ B & new A ≠ Null"
apply(unfold new_def)
apply(rule someI2_ex)
apply (fast dest:ex_new_if_finite[of "insert Null A"])
apply (fast)
done

lemma "~finite(UNIV::('a::ref)set) ⟹
VARS xs elem next alloc p q
{Xs = xs ∧ p = (Null::'a)}
WHILE xs ≠ []
INV {islist next p ∧ set(list next p) ⊆ set alloc ∧
map elem (rev(list next p)) @ xs = Xs}
DO q := new(set alloc); alloc := q#alloc;
q^.next := p; q^.elem := hd xs; xs := tl xs; p := q
OD
{islist next p ∧ map elem (rev(list next p)) = Xs}"
apply vcg_simp
apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin)
apply fastforce
done

end
```