theory Heap imports Main begin
subsection "References"
datatype 'a ref = Null | Ref 'a
lemma not_Null_eq [iff]: "(x ~= Null) = (EX y. x = Ref y)"
by (induct x) auto
lemma not_Ref_eq [iff]: "(ALL y. x ~= Ref y) = (x = Null)"
by (induct x) auto
primrec addr :: "'a ref ⇒ 'a" where
"addr (Ref a) = a"
section "The heap"
subsection "Paths in the heap"
primrec Path :: "('a ⇒ 'a ref) ⇒ 'a ref ⇒ 'a list ⇒ 'a ref ⇒ bool" where
"Path h x [] y ⟷ x = y"
| "Path h x (a#as) y ⟷ x = Ref 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]: "Path h (Ref a) as z =
(as = [] ∧ z = Ref 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 Path_upd[simp]:
"⋀x. u ∉ set as ⟹ Path (f(u := v)) x as y = Path f x as y"
by(induct as, simp, simp add:eq_sym_conv)
lemma Path_snoc:
"Path (f(a := q)) p as (Ref a) ⟹ Path (f(a := q)) p (as @ [a]) q"
by simp
subsection "Non-repeating paths"
definition distPath :: "('a ⇒ 'a ref) ⇒ 'a ref ⇒ 'a list ⇒ 'a ref ⇒ bool"
where "distPath h x as y ⟷ Path h x as y ∧ distinct as"
text‹The term @{term"distPath h x as y"} expresses the fact that a
non-repeating path @{term as} connects location @{term x} to location
@{term y} by means of the @{term h} field. In the case where ‹x
= y›, and there is a cycle from @{term x} to itself, @{term as} can
be both @{term "[]"} and the non-repeating list of nodes in the
cycle.›
lemma neq_dP: "p ≠ q ⟹ Path h p Ps q ⟹ distinct Ps ⟹
EX a Qs. p = Ref a & Ps = a#Qs & a ∉ set Qs"
by (case_tac Ps, auto)
lemma neq_dP_disp: "⟦ p ≠ q; distPath h p Ps q ⟧ ⟹
EX a Qs. p = Ref a ∧ Ps = a#Qs ∧ a ∉ set Qs"
apply (simp only:distPath_def)
by (case_tac Ps, auto)
subsection "Lists on the heap"
subsubsection "Relational abstraction"
definition List :: "('a ⇒ 'a ref) ⇒ 'a ref ⇒ 'a list ⇒ bool"
where "List h x as = Path h x as Null"
lemma [simp]: "List h x [] = (x = Null)"
by(simp add:List_def)
lemma [simp]: "List h x (a#as) = (x = Ref a ∧ List h (h a) as)"
by(simp add:List_def)
lemma [simp]: "List h Null as = (as = [])"
by(case_tac as, simp_all)
lemma List_Ref[simp]: "List h (Ref 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
apply(clarsimp simp add:fun_upd_apply)
done
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 (clarsimp simp add:in_set_conv_decomp)
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
lemma Path_is_List:
"⟦Path h b Ps (Ref a); a ∉ set Ps⟧ ⟹ List (h(a := Null)) b (Ps @ [a])"
apply (induct Ps arbitrary: b)
apply (auto simp add:fun_upd_apply)
done
subsection "Functional abstraction"
definition islist :: "('a ⇒ 'a ref) ⇒ 'a ref ⇒ bool"
where "islist h p ⟷ (∃as. List h p as)"
definition list :: "('a ⇒ 'a ref) ⇒ 'a ref ⇒ '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(simp add:islist_def list_def)
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"
by(simp add:islist_def)
lemma [simp]: "islist h (Ref a) = islist h (h a)"
by(simp add:islist_def)
lemma [simp]: "list h Null = []"
by(simp add:list_def)
lemma list_Ref_conv[simp]:
"islist h (h a) ⟹ list h (Ref 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])
apply(simp add:List_conv_islist_list)
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])
apply(simp add:List_conv_islist_list)
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])
apply(simp add:List_conv_islist_list)
done
end