Theory Core_DOM_Heap_WF
section‹Wellformedness›
text‹In this theory, we discuss the wellformedness of the DOM. First, we define
wellformedness and, second, we show for all functions for querying and modifying the
DOM to what extend they preserve wellformendess.›
theory Core_DOM_Heap_WF
imports
"Core_DOM_Functions"
begin
locale l_heap_is_wellformed⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs =
l_get_child_nodes_defs get_child_nodes get_child_nodes_locs +
l_get_disconnected_nodes_defs get_disconnected_nodes get_disconnected_nodes_locs
for get_child_nodes :: "(_::linorder) object_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locs :: "(_) object_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
and get_disconnected_nodes :: "(_) document_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
and get_disconnected_nodes_locs :: "(_) document_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
begin
definition a_owner_document_valid :: "(_) heap ⇒ bool"
where
"a_owner_document_valid h ⟷ (∀node_ptr ∈ fset (node_ptr_kinds h).
((∃document_ptr. document_ptr |∈| document_ptr_kinds h
∧ node_ptr ∈ set |h ⊢ get_disconnected_nodes document_ptr|⇩r)
∨ (∃parent_ptr. parent_ptr |∈| object_ptr_kinds h
∧ node_ptr ∈ set |h ⊢ get_child_nodes parent_ptr|⇩r)))"
lemma a_owner_document_valid_code [code]: "a_owner_document_valid h ⟷ node_ptr_kinds h |⊆|
fset_of_list (concat (map (λparent. |h ⊢ get_child_nodes parent|⇩r)
(sorted_list_of_fset (object_ptr_kinds h)) @ map (λparent. |h ⊢ get_disconnected_nodes parent|⇩r)
(sorted_list_of_fset (document_ptr_kinds h))))
"
apply(auto simp add: a_owner_document_valid_def
l_heap_is_wellformed⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs.a_owner_document_valid_def)[1]
proof -
fix x
assume 1: " ∀node_ptr∈fset (node_ptr_kinds h).
(∃document_ptr. document_ptr |∈| document_ptr_kinds h ∧
node_ptr ∈ set |h ⊢ get_disconnected_nodes document_ptr|⇩r) ∨
(∃parent_ptr. parent_ptr |∈| object_ptr_kinds h ∧
node_ptr ∈ set |h ⊢ get_child_nodes parent_ptr|⇩r)"
assume 2: "x |∈| node_ptr_kinds h"
assume 3: "x |∉| fset_of_list (concat (map (λparent. |h ⊢ get_disconnected_nodes parent|⇩r)
(sorted_list_of_fset (document_ptr_kinds h))))"
have "¬(∃document_ptr. document_ptr |∈| document_ptr_kinds h ∧
x ∈ set |h ⊢ get_disconnected_nodes document_ptr|⇩r)"
using 1 2 3
by (smt (verit) UN_I fset_of_list_elem image_eqI set_concat set_map sorted_list_of_fset_simps(1))
then
have "(∃parent_ptr. parent_ptr |∈| object_ptr_kinds h ∧ x ∈ set |h ⊢ get_child_nodes parent_ptr|⇩r)"
using 1 2
by auto
then obtain parent_ptr where parent_ptr:
"parent_ptr |∈| object_ptr_kinds h ∧ x ∈ set |h ⊢ get_child_nodes parent_ptr|⇩r"
by auto
moreover have "parent_ptr ∈ set (sorted_list_of_fset (object_ptr_kinds h))"
using parent_ptr by auto
moreover have "|h ⊢ get_child_nodes parent_ptr|⇩r ∈ set (map (λparent. |h ⊢ get_child_nodes parent|⇩r)
(sorted_list_of_fset (object_ptr_kinds h)))"
using calculation(2) by auto
ultimately
show "x |∈| fset_of_list (concat (map (λparent. |h ⊢ get_child_nodes parent|⇩r)
(sorted_list_of_fset (object_ptr_kinds h))))"
using fset_of_list_elem by fastforce
next
fix node_ptr
assume 1: "node_ptr_kinds h |⊆| fset_of_list (concat (map (λparent. |h ⊢ get_child_nodes parent|⇩r)
(sorted_list_of_fset (object_ptr_kinds h)))) |∪|
fset_of_list (concat (map (λparent. |h ⊢ get_disconnected_nodes parent|⇩r)
(sorted_list_of_fset (document_ptr_kinds h))))"
assume 2: "node_ptr |∈| node_ptr_kinds h"
assume 3: "∀parent_ptr. parent_ptr |∈| object_ptr_kinds h ⟶
node_ptr ∉ set |h ⊢ get_child_nodes parent_ptr|⇩r"
have "node_ptr ∈ set (concat (map (λparent. |h ⊢ get_child_nodes parent|⇩r)
(sorted_list_of_fset (object_ptr_kinds h)))) ∨
node_ptr ∈ set (concat (map (λparent. |h ⊢ get_disconnected_nodes parent|⇩r)
(sorted_list_of_fset (document_ptr_kinds h))))"
using 1 2
by (meson fin_mono fset_of_list_elem funion_iff)
then
show "∃document_ptr. document_ptr |∈| document_ptr_kinds h ∧
node_ptr ∈ set |h ⊢ get_disconnected_nodes document_ptr|⇩r"
using 3
by auto
qed
definition a_parent_child_rel :: "(_) heap ⇒ ((_) object_ptr × (_) object_ptr) set"
where
"a_parent_child_rel h = {(parent, child). parent |∈| object_ptr_kinds h
∧ child ∈ cast ` set |h ⊢ get_child_nodes parent|⇩r}"
lemma a_parent_child_rel_code [code]: "a_parent_child_rel h = set (concat (map
(λparent. map
(λchild. (parent, cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r child))
|h ⊢ get_child_nodes parent|⇩r)
(sorted_list_of_fset (object_ptr_kinds h)))
)"
by(auto simp add: a_parent_child_rel_def)
definition a_acyclic_heap :: "(_) heap ⇒ bool"
where
"a_acyclic_heap h = acyclic (a_parent_child_rel h)"
definition a_all_ptrs_in_heap :: "(_) heap ⇒ bool"
where
"a_all_ptrs_in_heap h ⟷
(∀ptr ∈ fset (object_ptr_kinds h). set |h ⊢ get_child_nodes ptr|⇩r ⊆ fset (node_ptr_kinds h)) ∧
(∀document_ptr ∈ fset (document_ptr_kinds h).
set |h ⊢ get_disconnected_nodes document_ptr|⇩r ⊆ fset (node_ptr_kinds h))"
definition a_distinct_lists :: "(_) heap ⇒ bool"
where
"a_distinct_lists h = distinct (concat (
(map (λptr. |h ⊢ get_child_nodes ptr|⇩r) |h ⊢ object_ptr_kinds_M|⇩r)
@ (map (λdocument_ptr. |h ⊢ get_disconnected_nodes document_ptr|⇩r) |h ⊢ document_ptr_kinds_M|⇩r)
))"
definition a_heap_is_wellformed :: "(_) heap ⇒ bool"
where
"a_heap_is_wellformed h ⟷
a_acyclic_heap h ∧ a_all_ptrs_in_heap h ∧ a_distinct_lists h ∧ a_owner_document_valid h"
end
locale l_heap_is_wellformed_defs =
fixes heap_is_wellformed :: "(_) heap ⇒ bool"
fixes parent_child_rel :: "(_) heap ⇒ ((_) object_ptr × (_) object_ptr) set"
global_interpretation l_heap_is_wellformed⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs get_child_nodes get_child_nodes_locs
get_disconnected_nodes get_disconnected_nodes_locs
defines heap_is_wellformed = "l_heap_is_wellformed⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs.a_heap_is_wellformed get_child_nodes
get_disconnected_nodes"
and parent_child_rel = "l_heap_is_wellformed⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs.a_parent_child_rel get_child_nodes"
and acyclic_heap = a_acyclic_heap
and all_ptrs_in_heap = a_all_ptrs_in_heap
and distinct_lists = a_distinct_lists
and owner_document_valid = a_owner_document_valid
.
locale l_heap_is_wellformed⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs
+ l_heap_is_wellformed⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs get_child_nodes get_child_nodes_locs get_disconnected_nodes
get_disconnected_nodes_locs
+ l_heap_is_wellformed_defs heap_is_wellformed parent_child_rel
+ l_get_disconnected_nodes type_wf get_disconnected_nodes get_disconnected_nodes_locs
for known_ptr :: "(_::linorder) object_ptr ⇒ bool"
and type_wf :: "(_) heap ⇒ bool"
and get_child_nodes :: "(_) object_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locs :: "(_) object_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
and get_disconnected_nodes :: "(_) document_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
and get_disconnected_nodes_locs :: "(_) document_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
and heap_is_wellformed :: "(_) heap ⇒ bool"
and parent_child_rel :: "(_) heap ⇒ ((_) object_ptr × (_) object_ptr) set" +
assumes heap_is_wellformed_impl: "heap_is_wellformed = a_heap_is_wellformed"
assumes parent_child_rel_impl: "parent_child_rel = a_parent_child_rel"
begin
lemmas heap_is_wellformed_def = heap_is_wellformed_impl[unfolded a_heap_is_wellformed_def]
lemmas parent_child_rel_def = parent_child_rel_impl[unfolded a_parent_child_rel_def]
lemmas acyclic_heap_def = a_acyclic_heap_def[folded parent_child_rel_impl]
lemma parent_child_rel_node_ptr:
"(parent, child) ∈ parent_child_rel h ⟹ is_node_ptr_kind child"
by(auto simp add: parent_child_rel_def)
lemma parent_child_rel_child_nodes:
assumes "known_ptr parent"
and "h ⊢ get_child_nodes parent →⇩r children"
and "child ∈ set children"
shows "(parent, cast child) ∈ parent_child_rel h"
using assms
apply(auto simp add: parent_child_rel_def is_OK_returns_result_I )[1]
using get_child_nodes_ptr_in_heap by blast
lemma parent_child_rel_child_nodes2:
assumes "known_ptr parent"
and "h ⊢ get_child_nodes parent →⇩r children"
and "child ∈ set children"
and "cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r child = child_obj"
shows "(parent, child_obj) ∈ parent_child_rel h"
using assms parent_child_rel_child_nodes by blast
lemma parent_child_rel_finite: "finite (parent_child_rel h)"
proof -
have "parent_child_rel h = (⋃ptr ∈ set |h ⊢ object_ptr_kinds_M|⇩r.
(⋃child ∈ set |h ⊢ get_child_nodes ptr|⇩r. {(ptr, cast child)}))"
by(auto simp add: parent_child_rel_def)
moreover have "finite (⋃ptr ∈ set |h ⊢ object_ptr_kinds_M|⇩r.
(⋃child ∈ set |h ⊢ get_child_nodes ptr|⇩r. {(ptr, cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r child)}))"
by simp
ultimately show ?thesis
by simp
qed
lemma distinct_lists_no_parent:
assumes "a_distinct_lists h"
assumes "h ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes"
assumes "node_ptr ∈ set disc_nodes"
shows "¬(∃parent_ptr. parent_ptr |∈| object_ptr_kinds h
∧ node_ptr ∈ set |h ⊢ get_child_nodes parent_ptr|⇩r)"
using assms
apply(auto simp add: a_distinct_lists_def)[1]
proof -
fix parent_ptr :: "(_) object_ptr"
assume a1: "parent_ptr |∈| object_ptr_kinds h"
assume a2: "(⋃x∈fset (object_ptr_kinds h).
set |h ⊢ get_child_nodes x|⇩r) ∩ (⋃x∈fset (document_ptr_kinds h).
set |h ⊢ get_disconnected_nodes x|⇩r) = {}"
assume a3: "h ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes"
assume a4: "node_ptr ∈ set disc_nodes"
assume a5: "node_ptr ∈ set |h ⊢ get_child_nodes parent_ptr|⇩r"
have f6: "parent_ptr ∈ fset (object_ptr_kinds h)"
using a1 by auto
have f7: "document_ptr ∈ fset (document_ptr_kinds h)"
using a3 by (meson get_disconnected_nodes_ptr_in_heap is_OK_returns_result_I)
have "|h ⊢ get_disconnected_nodes document_ptr|⇩r = disc_nodes"
using a3 by simp
then show False
using f7 f6 a5 a4 a2 by blast
qed
lemma distinct_lists_disconnected_nodes:
assumes "a_distinct_lists h"
and "h ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes"
shows "distinct disc_nodes"
proof -
have h1: "distinct (concat (map (λdocument_ptr. |h ⊢ get_disconnected_nodes document_ptr|⇩r)
|h ⊢ document_ptr_kinds_M|⇩r))"
using assms(1)
by(simp add: a_distinct_lists_def)
then show ?thesis
using concat_map_all_distinct[OF h1] assms(2) is_OK_returns_result_I get_disconnected_nodes_ok
by (metis (no_types, lifting) DocumentMonad.ptr_kinds_ptr_kinds_M
l_get_disconnected_nodes.get_disconnected_nodes_ptr_in_heap
l_get_disconnected_nodes_axioms select_result_I2)
qed
lemma distinct_lists_children:
assumes "a_distinct_lists h"
and "known_ptr ptr"
and "h ⊢ get_child_nodes ptr →⇩r children"
shows "distinct children"
proof (cases "children = []", simp)
assume "children ≠ []"
have h1: "distinct (concat ((map (λptr. |h ⊢ get_child_nodes ptr|⇩r) |h ⊢ object_ptr_kinds_M|⇩r)))"
using assms(1)
by(simp add: a_distinct_lists_def)
show ?thesis
using concat_map_all_distinct[OF h1] assms(2) assms(3)
by (metis (no_types, lifting) ObjectMonad.ptr_kinds_ptr_kinds_M get_child_nodes_ptr_in_heap
is_OK_returns_result_I select_result_I2)
qed
lemma heap_is_wellformed_children_in_heap:
assumes "heap_is_wellformed h"
assumes "h ⊢ get_child_nodes ptr →⇩r children"
assumes "child ∈ set children"
shows "child |∈| node_ptr_kinds h"
using assms
apply(auto simp add: heap_is_wellformed_def a_all_ptrs_in_heap_def)[1]
by (metis (no_types, opaque_lifting) is_OK_returns_result_I
local.get_child_nodes_ptr_in_heap select_result_I2 subsetD)
lemma heap_is_wellformed_one_parent:
assumes "heap_is_wellformed h"
assumes "h ⊢ get_child_nodes ptr →⇩r children"
assumes "h ⊢ get_child_nodes ptr' →⇩r children'"
assumes "set children ∩ set children' ≠ {}"
shows "ptr = ptr'"
using assms
proof (auto simp add: heap_is_wellformed_def a_distinct_lists_def)[1]
fix x :: "(_) node_ptr"
assume a1: "ptr ≠ ptr'"
assume a2: "h ⊢ get_child_nodes ptr →⇩r children"
assume a3: "h ⊢ get_child_nodes ptr' →⇩r children'"
assume a4: "distinct (concat (map (λptr. |h ⊢ get_child_nodes ptr|⇩r)
(sorted_list_of_set (fset (object_ptr_kinds h)))))"
have f5: "|h ⊢ get_child_nodes ptr|⇩r = children"
using a2 by simp
have "|h ⊢ get_child_nodes ptr'|⇩r = children'"
using a3 by (meson select_result_I2)
then have "ptr ∉ set (sorted_list_of_set (fset (object_ptr_kinds h)))
∨ ptr' ∉ set (sorted_list_of_set (fset (object_ptr_kinds h)))
∨ set children ∩ set children' = {}"
using f5 a4 a1 by (meson distinct_concat_map_E(1))
then show False
using a3 a2 by (metis (no_types) assms(4) finite_fset is_OK_returns_result_I
local.get_child_nodes_ptr_in_heap set_sorted_list_of_set)
qed
lemma parent_child_rel_child:
"h ⊢ get_child_nodes ptr →⇩r children ⟹
child ∈ set children ⟷ (ptr, cast child) ∈ parent_child_rel h"
by (simp add: is_OK_returns_result_I get_child_nodes_ptr_in_heap parent_child_rel_def)
lemma parent_child_rel_acyclic: "heap_is_wellformed h ⟹ acyclic (parent_child_rel h)"
by (simp add: acyclic_heap_def local.heap_is_wellformed_def)
lemma heap_is_wellformed_disconnected_nodes_distinct:
"heap_is_wellformed h ⟹ h ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes ⟹
distinct disc_nodes"
using distinct_lists_disconnected_nodes local.heap_is_wellformed_def by blast
lemma parent_child_rel_parent_in_heap:
"(parent, child_ptr) ∈ parent_child_rel h ⟹ parent |∈| object_ptr_kinds h"
using local.parent_child_rel_def by blast
lemma parent_child_rel_child_in_heap:
"heap_is_wellformed h ⟹ type_wf h ⟹ known_ptr parent
⟹ (parent, child_ptr) ∈ parent_child_rel h ⟹ child_ptr |∈| object_ptr_kinds h"
apply(auto simp add: heap_is_wellformed_def parent_child_rel_def a_all_ptrs_in_heap_def)[1]
using get_child_nodes_ok
by (meson subsetD)
lemma heap_is_wellformed_disc_nodes_in_heap:
"heap_is_wellformed h ⟹ h ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes
⟹ node ∈ set disc_nodes ⟹ node |∈| node_ptr_kinds h"
by (metis (no_types, opaque_lifting) is_OK_returns_result_I local.a_all_ptrs_in_heap_def
local.get_disconnected_nodes_ptr_in_heap local.heap_is_wellformed_def select_result_I2 subsetD)
lemma heap_is_wellformed_one_disc_parent:
"heap_is_wellformed h ⟹ h ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes
⟹ h ⊢ get_disconnected_nodes document_ptr' →⇩r disc_nodes'
⟹ set disc_nodes ∩ set disc_nodes' ≠ {} ⟹ document_ptr = document_ptr'"
using DocumentMonad.ptr_kinds_ptr_kinds_M concat_append distinct_append distinct_concat_map_E(1)
is_OK_returns_result_I local.a_distinct_lists_def local.get_disconnected_nodes_ptr_in_heap
local.heap_is_wellformed_def select_result_I2
proof -
assume a1: "heap_is_wellformed h"
assume a2: "h ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes"
assume a3: "h ⊢ get_disconnected_nodes document_ptr' →⇩r disc_nodes'"
assume a4: "set disc_nodes ∩ set disc_nodes' ≠ {}"
have f5: "|h ⊢ get_disconnected_nodes document_ptr|⇩r = disc_nodes"
using a2 by (meson select_result_I2)
have f6: "|h ⊢ get_disconnected_nodes document_ptr'|⇩r = disc_nodes'"
using a3 by (meson select_result_I2)
have "⋀nss nssa. ¬ distinct (concat (nss @ nssa)) ∨ distinct (concat nssa::(_) node_ptr list)"
by (metis (no_types) concat_append distinct_append)
then have "distinct (concat (map (λd. |h ⊢ get_disconnected_nodes d|⇩r) |h ⊢ document_ptr_kinds_M|⇩r))"
using a1 local.a_distinct_lists_def local.heap_is_wellformed_def by blast
then show ?thesis
using f6 f5 a4 a3 a2 by (meson DocumentMonad.ptr_kinds_ptr_kinds_M distinct_concat_map_E(1)
is_OK_returns_result_I local.get_disconnected_nodes_ptr_in_heap)
qed
lemma heap_is_wellformed_children_disc_nodes_different:
"heap_is_wellformed h ⟹ h ⊢ get_child_nodes ptr →⇩r children
⟹ h ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes
⟹ set children ∩ set disc_nodes = {}"
by (metis (no_types, opaque_lifting) disjoint_iff_not_equal distinct_lists_no_parent
is_OK_returns_result_I local.get_child_nodes_ptr_in_heap
local.heap_is_wellformed_def select_result_I2)
lemma heap_is_wellformed_children_disc_nodes:
"heap_is_wellformed h ⟹ node_ptr |∈| node_ptr_kinds h
⟹ ¬(∃parent ∈ fset (object_ptr_kinds h). node_ptr ∈ set |h ⊢ get_child_nodes parent|⇩r)
⟹ (∃document_ptr ∈ fset (document_ptr_kinds h). node_ptr ∈ set |h ⊢ get_disconnected_nodes document_ptr|⇩r)"
by (auto simp add: heap_is_wellformed_def a_distinct_lists_def a_owner_document_valid_def)
lemma heap_is_wellformed_children_distinct:
"heap_is_wellformed h ⟹ h ⊢ get_child_nodes ptr →⇩r children ⟹ distinct children"
by (metis (no_types, lifting) ObjectMonad.ptr_kinds_ptr_kinds_M concat_append distinct_append
distinct_concat_map_E(2) is_OK_returns_result_I local.a_distinct_lists_def
local.get_child_nodes_ptr_in_heap local.heap_is_wellformed_def
select_result_I2)
end
locale l_heap_is_wellformed = l_type_wf + l_known_ptr + l_heap_is_wellformed_defs
+ l_get_child_nodes_defs + l_get_disconnected_nodes_defs +
assumes heap_is_wellformed_children_in_heap:
"heap_is_wellformed h ⟹ h ⊢ get_child_nodes ptr →⇩r children ⟹ child ∈ set children
⟹ child |∈| node_ptr_kinds h"
assumes heap_is_wellformed_disc_nodes_in_heap:
"heap_is_wellformed h ⟹ h ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes
⟹ node ∈ set disc_nodes ⟹ node |∈| node_ptr_kinds h"
assumes heap_is_wellformed_one_parent:
"heap_is_wellformed h ⟹ h ⊢ get_child_nodes ptr →⇩r children
⟹ h ⊢ get_child_nodes ptr' →⇩r children'
⟹ set children ∩ set children' ≠ {} ⟹ ptr = ptr'"
assumes heap_is_wellformed_one_disc_parent:
"heap_is_wellformed h ⟹ h ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes
⟹ h ⊢ get_disconnected_nodes document_ptr' →⇩r disc_nodes'
⟹ set disc_nodes ∩ set disc_nodes' ≠ {} ⟹ document_ptr = document_ptr'"
assumes heap_is_wellformed_children_disc_nodes_different:
"heap_is_wellformed h ⟹ h ⊢ get_child_nodes ptr →⇩r children
⟹ h ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes
⟹ set children ∩ set disc_nodes = {}"
assumes heap_is_wellformed_disconnected_nodes_distinct:
"heap_is_wellformed h ⟹ h ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes
⟹ distinct disc_nodes"
assumes heap_is_wellformed_children_distinct:
"heap_is_wellformed h ⟹ h ⊢ get_child_nodes ptr →⇩r children ⟹ distinct children"
assumes heap_is_wellformed_children_disc_nodes:
"heap_is_wellformed h ⟹ node_ptr |∈| node_ptr_kinds h
⟹ ¬(∃parent ∈ fset (object_ptr_kinds h). node_ptr ∈ set |h ⊢ get_child_nodes parent|⇩r)
⟹ (∃document_ptr ∈ fset (document_ptr_kinds h). node_ptr ∈ set |h ⊢ get_disconnected_nodes document_ptr|⇩r)"
assumes parent_child_rel_child:
"h ⊢ get_child_nodes ptr →⇩r children
⟹ child ∈ set children ⟷ (ptr, cast child) ∈ parent_child_rel h"
assumes parent_child_rel_finite:
"heap_is_wellformed h ⟹ finite (parent_child_rel h)"
assumes parent_child_rel_acyclic:
"heap_is_wellformed h ⟹ acyclic (parent_child_rel h)"
assumes parent_child_rel_node_ptr:
"(parent, child_ptr) ∈ parent_child_rel h ⟹ is_node_ptr_kind child_ptr"
assumes parent_child_rel_parent_in_heap:
"(parent, child_ptr) ∈ parent_child_rel h ⟹ parent |∈| object_ptr_kinds h"
assumes parent_child_rel_child_in_heap:
"heap_is_wellformed h ⟹ type_wf h ⟹ known_ptr parent
⟹ (parent, child_ptr) ∈ parent_child_rel h ⟹ child_ptr |∈| object_ptr_kinds h"
interpretation i_heap_is_wellformed?: l_heap_is_wellformed⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M known_ptr type_wf get_child_nodes
get_child_nodes_locs get_disconnected_nodes get_disconnected_nodes_locs
heap_is_wellformed parent_child_rel
apply(unfold_locales)
by(auto simp add: heap_is_wellformed_def parent_child_rel_def)
declare l_heap_is_wellformed⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
lemma heap_is_wellformed_is_l_heap_is_wellformed [instances]:
"l_heap_is_wellformed type_wf known_ptr heap_is_wellformed parent_child_rel get_child_nodes
get_disconnected_nodes"
apply(auto simp add: l_heap_is_wellformed_def)[1]
using heap_is_wellformed_children_in_heap
apply blast
using heap_is_wellformed_disc_nodes_in_heap
apply blast
using heap_is_wellformed_one_parent
apply blast
using heap_is_wellformed_one_disc_parent
apply blast
using heap_is_wellformed_children_disc_nodes_different
apply blast
using heap_is_wellformed_disconnected_nodes_distinct
apply blast
using heap_is_wellformed_children_distinct
apply blast
using heap_is_wellformed_children_disc_nodes
apply blast
using parent_child_rel_child
apply (blast)
using parent_child_rel_child
apply(blast)
using parent_child_rel_finite
apply blast
using parent_child_rel_acyclic
apply blast
using parent_child_rel_node_ptr
apply blast
using parent_child_rel_parent_in_heap
apply blast
using parent_child_rel_child_in_heap
apply blast
done
subsection ‹get\_parent›
locale l_get_parent_wf⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_parent⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
known_ptr type_wf get_child_nodes get_child_nodes_locs known_ptrs get_parent get_parent_locs
+ l_heap_is_wellformed
type_wf known_ptr heap_is_wellformed parent_child_rel get_child_nodes get_child_nodes_locs
get_disconnected_nodes get_disconnected_nodes_locs
for known_ptr :: "(_::linorder) object_ptr ⇒ bool"
and type_wf :: "(_) heap ⇒ bool"
and get_child_nodes :: "(_) object_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locs :: "(_) object_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
and known_ptrs :: "(_) heap ⇒ bool"
and get_parent :: "(_) node_ptr ⇒ ((_) heap, exception, (_) object_ptr option) prog"
and get_parent_locs :: "((_) heap ⇒ (_) heap ⇒ bool) set"
and heap_is_wellformed :: "(_) heap ⇒ bool"
and parent_child_rel :: "(_) heap ⇒ ((_) object_ptr × (_) object_ptr) set"
and get_disconnected_nodes :: "(_) document_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
and get_disconnected_nodes_locs :: "(_) document_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
begin
lemma child_parent_dual:
assumes heap_is_wellformed: "heap_is_wellformed h"
assumes "h ⊢ get_child_nodes ptr →⇩r children"
assumes "child ∈ set children"
assumes "known_ptrs h"
assumes type_wf: "type_wf h"
shows "h ⊢ get_parent child →⇩r Some ptr"
proof -
obtain ptrs where ptrs: "h ⊢ object_ptr_kinds_M →⇩r ptrs"
by(simp add: object_ptr_kinds_M_defs)
then have h1: "ptr ∈ set ptrs"
using get_child_nodes_ok assms(2) is_OK_returns_result_I
by (metis (no_types, opaque_lifting) ObjectMonad.ptr_kinds_ptr_kinds_M
‹⋀thesis. (⋀ptrs. h ⊢ object_ptr_kinds_M →⇩r ptrs ⟹ thesis) ⟹ thesis›
get_child_nodes_ptr_in_heap returns_result_eq select_result_I2)
let ?P = "(λptr. get_child_nodes ptr ⤜ (λchildren. return (child ∈ set children)))"
let ?filter = "filter_M ?P ptrs"
have "h ⊢ ok ?filter"
using ptrs type_wf
using get_child_nodes_ok
apply(auto intro!: filter_M_is_OK_I bind_is_OK_pure_I get_child_nodes_ok simp add: bind_pure_I)[1]
using assms(4) local.known_ptrs_known_ptr by blast
then obtain parent_ptrs where parent_ptrs: "h ⊢ ?filter →⇩r parent_ptrs"
by auto
have h5: "∃!x. x ∈ set ptrs ∧ h ⊢ Heap_Error_Monad.bind (get_child_nodes x)
(λchildren. return (child ∈ set children)) →⇩r True"
apply(auto intro!: bind_pure_returns_result_I)[1]
using heap_is_wellformed_one_parent
proof -
have "h ⊢ (return (child ∈ set children)::((_) heap, exception, bool) prog) →⇩r True"
by (simp add: assms(3))
then show
"∃z. z ∈ set ptrs ∧ h ⊢ Heap_Error_Monad.bind (get_child_nodes z)
(λns. return (child ∈ set ns)) →⇩r True"
by (metis (no_types) assms(2) bind_pure_returns_result_I2 h1 is_OK_returns_result_I
local.get_child_nodes_pure select_result_I2)
next
fix x y
assume 0: "x ∈ set ptrs"
and 1: "h ⊢ Heap_Error_Monad.bind (get_child_nodes x)
(λchildren. return (child ∈ set children)) →⇩r True"
and 2: "y ∈ set ptrs"
and 3: "h ⊢ Heap_Error_Monad.bind (get_child_nodes y)
(λchildren. return (child ∈ set children)) →⇩r True"
and 4: "(⋀h ptr children ptr' children'. heap_is_wellformed h
⟹ h ⊢ get_child_nodes ptr →⇩r children ⟹ h ⊢ get_child_nodes ptr' →⇩r children'
⟹ set children ∩ set children' ≠ {} ⟹ ptr = ptr')"
then show "x = y"
by (metis (no_types, lifting) bind_returns_result_E disjoint_iff_not_equal heap_is_wellformed
return_returns_result)
qed
have "child |∈| node_ptr_kinds h"
using heap_is_wellformed_children_in_heap heap_is_wellformed assms(2) assms(3)
by fast
moreover have "parent_ptrs = [ptr]"
apply(rule filter_M_ex1[OF parent_ptrs h1 h5])
using ptrs assms(2) assms(3)
by(auto simp add: object_ptr_kinds_M_defs bind_pure_I intro!: bind_pure_returns_result_I)
ultimately show ?thesis
using ptrs parent_ptrs
by(auto simp add: bind_pure_I get_parent_def
elim!: bind_returns_result_E2
intro!: bind_pure_returns_result_I filter_M_pure_I)
qed
lemma parent_child_rel_parent:
assumes "heap_is_wellformed h"
and "h ⊢ get_parent child_node →⇩r Some parent"
shows "(parent, cast child_node) ∈ parent_child_rel h"
using assms parent_child_rel_child get_parent_child_dual by auto
lemma heap_wellformed_induct [consumes 1, case_names step]:
assumes "heap_is_wellformed h"
and step: "⋀parent. (⋀children child. h ⊢ get_child_nodes parent →⇩r children
⟹ child ∈ set children ⟹ P (cast child)) ⟹ P parent"
shows "P ptr"
proof -
fix ptr
have "wf ((parent_child_rel h)¯)"
by (simp add: assms(1) finite_acyclic_wf_converse parent_child_rel_acyclic parent_child_rel_finite)
then show "?thesis"
proof (induct rule: wf_induct_rule)
case (less parent)
then show ?case
using assms parent_child_rel_child
by (meson converse_iff)
qed
qed
lemma heap_wellformed_induct2 [consumes 3, case_names not_in_heap empty_children step]:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
and not_in_heap: "⋀parent. parent |∉| object_ptr_kinds h ⟹ P parent"
and empty_children: "⋀parent. h ⊢ get_child_nodes parent →⇩r [] ⟹ P parent"
and step: "⋀parent children child. h ⊢ get_child_nodes parent →⇩r children
⟹ child ∈ set children ⟹ P (cast child) ⟹ P parent"
shows "P ptr"
proof(insert assms(1), induct rule: heap_wellformed_induct)
case (step parent)
then show ?case
proof(cases "parent |∈| object_ptr_kinds h")
case True
then obtain children where children: "h ⊢ get_child_nodes parent →⇩r children"
using get_child_nodes_ok assms(2) assms(3)
by (meson is_OK_returns_result_E local.known_ptrs_known_ptr)
then show ?thesis
proof (cases "children = []")
case True
then show ?thesis
using children empty_children
by simp
next
case False
then show ?thesis
using assms(6) children last_in_set step.hyps by blast
qed
next
case False
then show ?thesis
by (simp add: not_in_heap)
qed
qed
lemma heap_wellformed_induct_rev [consumes 1, case_names step]:
assumes "heap_is_wellformed h"
and step: "⋀child. (⋀parent child_node. cast child_node = child
⟹ h ⊢ get_parent child_node →⇩r Some parent ⟹ P parent) ⟹ P child"
shows "P ptr"
proof -
fix ptr
have "wf ((parent_child_rel h))"
by (simp add: assms(1) local.parent_child_rel_acyclic local.parent_child_rel_finite
wf_iff_acyclic_if_finite)
then show "?thesis"
proof (induct rule: wf_induct_rule)
case (less child)
show ?case
using assms get_parent_child_dual
by (metis less.hyps parent_child_rel_parent)
qed
qed
end
interpretation i_get_parent_wf?: l_get_parent_wf⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M known_ptr type_wf get_child_nodes
get_child_nodes_locs known_ptrs get_parent get_parent_locs heap_is_wellformed
parent_child_rel get_disconnected_nodes
using instances
by(simp add: l_get_parent_wf⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def)
declare l_get_parent_wf⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
locale l_get_parent_wf2⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_parent_wf⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
known_ptr type_wf get_child_nodes get_child_nodes_locs known_ptrs get_parent get_parent_locs
heap_is_wellformed parent_child_rel get_disconnected_nodes get_disconnected_nodes_locs
+ l_heap_is_wellformed⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
known_ptr type_wf get_child_nodes get_child_nodes_locs get_disconnected_nodes
get_disconnected_nodes_locs heap_is_wellformed parent_child_rel
for known_ptr :: "(_::linorder) object_ptr ⇒ bool"
and type_wf :: "(_) heap ⇒ bool"
and get_child_nodes :: "(_) object_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locs :: "(_) object_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
and known_ptrs :: "(_) heap ⇒ bool"
and get_parent :: "(_) node_ptr ⇒ ((_) heap, exception, (_) object_ptr option) prog"
and get_parent_locs :: "((_) heap ⇒ (_) heap ⇒ bool) set"
and heap_is_wellformed :: "(_) heap ⇒ bool"
and parent_child_rel :: "(_) heap ⇒ ((_) object_ptr × (_) object_ptr) set"
and get_disconnected_nodes :: "(_) document_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
and get_disconnected_nodes_locs :: "(_) document_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
begin
lemma preserves_wellformedness_writes_needed:
assumes heap_is_wellformed: "heap_is_wellformed h"
and "h ⊢ f →⇩h h'"
and "writes SW f h h'"
and preserved_get_child_nodes:
"⋀h h' w. w ∈ SW ⟹ h ⊢ w →⇩h h'
⟹ ∀object_ptr. ∀r ∈ get_child_nodes_locs object_ptr. r h h'"
and preserved_get_disconnected_nodes:
"⋀h h' w. w ∈ SW ⟹ h ⊢ w →⇩h h'
⟹ ∀document_ptr. ∀r ∈ get_disconnected_nodes_locs document_ptr. r h h'"
and preserved_object_pointers:
"⋀h h' w. w ∈ SW ⟹ h ⊢ w →⇩h h'
⟹ ∀object_ptr. preserved (get_M⇩O⇩b⇩j⇩e⇩c⇩t object_ptr RObject.nothing) h h'"
shows "heap_is_wellformed h'"
proof -
have object_ptr_kinds_eq3: "object_ptr_kinds h = object_ptr_kinds h'"
using assms(2) assms(3) object_ptr_kinds_preserved preserved_object_pointers by blast
then have object_ptr_kinds_eq:
"⋀ptrs. h ⊢ object_ptr_kinds_M →⇩r ptrs = h' ⊢ object_ptr_kinds_M →⇩r ptrs"
unfolding object_ptr_kinds_M_defs by simp
then have object_ptr_kinds_eq2: "|h ⊢ object_ptr_kinds_M|⇩r = |h' ⊢ object_ptr_kinds_M|⇩r"
using select_result_eq by force
then have node_ptr_kinds_eq2: "|h ⊢ node_ptr_kinds_M|⇩r = |h' ⊢ node_ptr_kinds_M|⇩r"
using node_ptr_kinds_M_eq by auto
then have node_ptr_kinds_eq3: "node_ptr_kinds h = node_ptr_kinds h'"
by auto
have document_ptr_kinds_eq2: "|h ⊢ document_ptr_kinds_M|⇩r = |h' ⊢ document_ptr_kinds_M|⇩r"
using object_ptr_kinds_eq2 document_ptr_kinds_M_eq by auto
then have document_ptr_kinds_eq3: "document_ptr_kinds h = document_ptr_kinds h'"
by auto
have children_eq:
"⋀ptr children. h ⊢ get_child_nodes ptr →⇩r children = h' ⊢ get_child_nodes ptr →⇩r children"
apply(rule reads_writes_preserved[OF get_child_nodes_reads assms(3) assms(2)])
using preserved_get_child_nodes by fast
then have children_eq2: "⋀ptr. |h ⊢ get_child_nodes ptr|⇩r = |h' ⊢ get_child_nodes ptr|⇩r"
using select_result_eq by force
have disconnected_nodes_eq:
"⋀document_ptr disconnected_nodes.
h ⊢ get_disconnected_nodes document_ptr →⇩r disconnected_nodes
= h' ⊢ get_disconnected_nodes document_ptr →⇩r disconnected_nodes"
apply(rule reads_writes_preserved[OF get_disconnected_nodes_reads assms(3) assms(2)])
using preserved_get_disconnected_nodes by fast
then have disconnected_nodes_eq2:
"⋀document_ptr. |h ⊢ get_disconnected_nodes document_ptr|⇩r
= |h' ⊢ get_disconnected_nodes document_ptr|⇩r"
using select_result_eq by force
have get_parent_eq: "⋀ptr parent. h ⊢ get_parent ptr →⇩r parent = h' ⊢ get_parent ptr →⇩r parent"
apply(rule reads_writes_preserved[OF get_parent_reads assms(3) assms(2)])
using preserved_get_child_nodes preserved_object_pointers unfolding get_parent_locs_def by fast
have "a_acyclic_heap h"
using heap_is_wellformed by (simp add: heap_is_wellformed_def)
have "parent_child_rel h' ⊆ parent_child_rel h"
proof
fix x
assume "x ∈ parent_child_rel h'"
then show "x ∈ parent_child_rel h"
by(simp add: parent_child_rel_def children_eq2 object_ptr_kinds_eq3)
qed
then have "a_acyclic_heap h'"
using ‹a_acyclic_heap h› acyclic_heap_def acyclic_subset by blast
moreover have "a_all_ptrs_in_heap h"
using heap_is_wellformed by (simp add: heap_is_wellformed_def)
then have "a_all_ptrs_in_heap h'"
by (simp add: children_eq2 disconnected_nodes_eq2 document_ptr_kinds_eq3
l_heap_is_wellformed⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs.a_all_ptrs_in_heap_def node_ptr_kinds_eq3 object_ptr_kinds_eq3)
moreover have h0: "a_distinct_lists h"
using heap_is_wellformed by (simp add: heap_is_wellformed_def)
have h1: "map (λptr. |h ⊢ get_child_nodes ptr|⇩r) (sorted_list_of_set (fset (object_ptr_kinds h)))
= map (λptr. |h' ⊢ get_child_nodes ptr|⇩r) (sorted_list_of_set (fset (object_ptr_kinds h')))"
by (simp add: children_eq2 object_ptr_kinds_eq3)
have h2: "map (λdocument_ptr. |h ⊢ get_disconnected_nodes document_ptr|⇩r)
(sorted_list_of_set (fset (document_ptr_kinds h)))
= map (λdocument_ptr. |h' ⊢ get_disconnected_nodes document_ptr|⇩r)
(sorted_list_of_set (fset (document_ptr_kinds h')))"
using disconnected_nodes_eq document_ptr_kinds_eq2 select_result_eq by force
have "a_distinct_lists h'"
using h0
by(simp add: a_distinct_lists_def h1 h2)
moreover have "a_owner_document_valid h"
using heap_is_wellformed by (simp add: heap_is_wellformed_def)
then have "a_owner_document_valid h'"
by(auto simp add: a_owner_document_valid_def children_eq2 disconnected_nodes_eq2
object_ptr_kinds_eq3 node_ptr_kinds_eq3 document_ptr_kinds_eq3)
ultimately show ?thesis
by (simp add: heap_is_wellformed_def)
qed
end
interpretation i_get_parent_wf2?: l_get_parent_wf2⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M known_ptr type_wf get_child_nodes
get_child_nodes_locs known_ptrs get_parent get_parent_locs
heap_is_wellformed parent_child_rel get_disconnected_nodes
get_disconnected_nodes_locs
using l_get_parent_wf⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms l_heap_is_wellformed⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms
by (simp add: l_get_parent_wf2⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def)
declare l_get_parent_wf2⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
locale l_get_parent_wf = l_type_wf + l_known_ptrs + l_heap_is_wellformed_defs
+ l_get_child_nodes_defs + l_get_parent_defs +
assumes child_parent_dual:
"heap_is_wellformed h
⟹ type_wf h
⟹ known_ptrs h
⟹ h ⊢ get_child_nodes ptr →⇩r children
⟹ child ∈ set children
⟹ h ⊢ get_parent child →⇩r Some ptr"
assumes heap_wellformed_induct [consumes 1, case_names step]:
"heap_is_wellformed h
⟹ (⋀parent. (⋀children child. h ⊢ get_child_nodes parent →⇩r children
⟹ child ∈ set children ⟹ P (cast child)) ⟹ P parent)
⟹ P ptr"
assumes heap_wellformed_induct_rev [consumes 1, case_names step]:
"heap_is_wellformed h
⟹ (⋀child. (⋀parent child_node. cast child_node = child
⟹ h ⊢ get_parent child_node →⇩r Some parent ⟹ P parent) ⟹ P child)
⟹ P ptr"
assumes parent_child_rel_parent: "heap_is_wellformed h
⟹ h ⊢ get_parent child_node →⇩r Some parent
⟹ (parent, cast child_node) ∈ parent_child_rel h"
lemma get_parent_wf_is_l_get_parent_wf [instances]:
"l_get_parent_wf type_wf known_ptr known_ptrs heap_is_wellformed parent_child_rel
get_child_nodes get_parent"
using known_ptrs_is_l_known_ptrs
apply(auto simp add: l_get_parent_wf_def l_get_parent_wf_axioms_def)[1]
using child_parent_dual heap_wellformed_induct heap_wellformed_induct_rev parent_child_rel_parent
by metis+
subsection ‹get\_disconnected\_nodes›
subsection ‹set\_disconnected\_nodes›
subsubsection ‹get\_disconnected\_nodes›
locale l_set_disconnected_nodes_get_disconnected_nodes_wf⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_set_disconnected_nodes_get_disconnected_nodes
type_wf get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes
set_disconnected_nodes_locs
+ l_heap_is_wellformed
type_wf known_ptr heap_is_wellformed parent_child_rel get_child_nodes get_child_nodes_locs
get_disconnected_nodes get_disconnected_nodes_locs
for known_ptr :: "(_) object_ptr ⇒ bool"
and type_wf :: "(_) heap ⇒ bool"
and get_disconnected_nodes :: "(_) document_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
and get_disconnected_nodes_locs :: "(_) document_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
and set_disconnected_nodes :: "(_) document_ptr ⇒ (_) node_ptr list ⇒ ((_) heap, exception, unit) prog"
and set_disconnected_nodes_locs :: "(_) document_ptr ⇒ ((_) heap, exception, unit) prog set"
and heap_is_wellformed :: "(_) heap ⇒ bool"
and parent_child_rel :: "(_) heap ⇒ ((_) object_ptr × (_) object_ptr) set"
and get_child_nodes :: "(_) object_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locs :: "(_) object_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
begin
lemma remove_from_disconnected_nodes_removes:
assumes "heap_is_wellformed h"
assumes "h ⊢ get_disconnected_nodes ptr →⇩r disc_nodes"
assumes "h ⊢ set_disconnected_nodes ptr (remove1 node_ptr disc_nodes) →⇩h h'"
assumes "h' ⊢ get_disconnected_nodes ptr →⇩r disc_nodes'"
shows "node_ptr ∉ set disc_nodes'"
using assms
by (metis distinct_remove1_removeAll heap_is_wellformed_disconnected_nodes_distinct
set_disconnected_nodes_get_disconnected_nodes member_remove remove_code(1)
returns_result_eq)
end
locale l_set_disconnected_nodes_get_disconnected_nodes_wf = l_heap_is_wellformed
+ l_set_disconnected_nodes_get_disconnected_nodes +
assumes remove_from_disconnected_nodes_removes:
"heap_is_wellformed h ⟹ h ⊢ get_disconnected_nodes ptr →⇩r disc_nodes
⟹ h ⊢ set_disconnected_nodes ptr (remove1 node_ptr disc_nodes) →⇩h h'
⟹ h' ⊢ get_disconnected_nodes ptr →⇩r disc_nodes'
⟹ node_ptr ∉ set disc_nodes'"
interpretation i_set_disconnected_nodes_get_disconnected_nodes_wf⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M?:
l_set_disconnected_nodes_get_disconnected_nodes_wf⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M known_ptr type_wf get_disconnected_nodes
get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs heap_is_wellformed
parent_child_rel get_child_nodes
using instances
by (simp add: l_set_disconnected_nodes_get_disconnected_nodes_wf⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def)
declare l_set_disconnected_nodes_get_disconnected_nodes_wf⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
lemma set_disconnected_nodes_get_disconnected_nodes_wf_is_l_set_disconnected_nodes_get_disconnected_nodes_wf [instances]:
"l_set_disconnected_nodes_get_disconnected_nodes_wf type_wf known_ptr heap_is_wellformed parent_child_rel
get_child_nodes get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes
set_disconnected_nodes_locs"
apply(auto simp add: l_set_disconnected_nodes_get_disconnected_nodes_wf_def
l_set_disconnected_nodes_get_disconnected_nodes_wf_axioms_def instances)[1]
using remove_from_disconnected_nodes_removes apply fast
done
subsection ‹get\_root\_node›
locale l_get_root_node_wf⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_heap_is_wellformed
type_wf known_ptr heap_is_wellformed parent_child_rel get_child_nodes get_child_nodes_locs
get_disconnected_nodes get_disconnected_nodes_locs
+ l_get_parent⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
known_ptr type_wf get_child_nodes get_child_nodes_locs known_ptrs get_parent get_parent_locs
+ l_get_parent_wf
type_wf known_ptr known_ptrs heap_is_wellformed parent_child_rel get_child_nodes
get_child_nodes_locs get_parent get_parent_locs
+ l_get_root_node⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
type_wf known_ptr known_ptrs get_parent get_parent_locs get_child_nodes get_child_nodes_locs
get_ancestors get_ancestors_locs get_root_node get_root_node_locs
for known_ptr :: "(_::linorder) object_ptr ⇒ bool"
and type_wf :: "(_) heap ⇒ bool"
and known_ptrs :: "(_) heap ⇒ bool"
and heap_is_wellformed :: "(_) heap ⇒ bool"
and parent_child_rel :: "(_) heap ⇒ ((_) object_ptr × (_) object_ptr) set"
and get_child_nodes :: "(_) object_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locs :: "(_) object_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
and get_disconnected_nodes :: "(_) document_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
and get_disconnected_nodes_locs :: "(_) document_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
and get_parent :: "(_) node_ptr ⇒ ((_) heap, exception, (_) object_ptr option) prog"
and get_parent_locs :: "((_) heap ⇒ (_) heap ⇒ bool) set"
and get_ancestors :: "(_) object_ptr ⇒ ((_) heap, exception, (_) object_ptr list) prog"
and get_ancestors_locs :: "((_) heap ⇒ (_) heap ⇒ bool) set"
and get_root_node :: "(_) object_ptr ⇒ ((_) heap, exception, (_) object_ptr) prog"
and get_root_node_locs :: "((_) heap ⇒ (_) heap ⇒ bool) set"
begin
lemma get_ancestors_reads:
assumes "heap_is_wellformed h"
shows "reads get_ancestors_locs (get_ancestors node_ptr) h h'"
proof (insert assms(1), induct rule: heap_wellformed_induct_rev)
case (step child)
then show ?case
using [[simproc del: Product_Type.unit_eq]] get_parent_reads[unfolded reads_def]
apply(simp (no_asm) add: get_ancestors_def)
by(auto simp add: get_ancestors_locs_def reads_subset[OF return_reads] get_parent_reads_pointers
intro!: reads_bind_pure reads_subset[OF check_in_heap_reads]
reads_subset[OF get_parent_reads] reads_subset[OF get_child_nodes_reads]
split: option.splits)
qed
lemma get_ancestors_ok:
assumes "heap_is_wellformed h"
and "ptr |∈| object_ptr_kinds h"
and "known_ptrs h"
and type_wf: "type_wf h"
shows "h ⊢ ok (get_ancestors ptr)"
proof (insert assms(1) assms(2), induct rule: heap_wellformed_induct_rev)
case (step child)
then show ?case
using assms(3) assms(4)
apply(simp (no_asm) add: get_ancestors_def)
apply(simp add: assms(1) get_parent_parent_in_heap)
by(auto intro!: bind_is_OK_pure_I bind_pure_I get_parent_ok split: option.splits)
qed
lemma get_root_node_ptr_in_heap:
assumes "h ⊢ ok (get_root_node ptr)"
shows "ptr |∈| object_ptr_kinds h"
using assms
unfolding get_root_node_def
using get_ancestors_ptr_in_heap
by auto
lemma get_root_node_ok:
assumes "heap_is_wellformed h" "known_ptrs h" "type_wf h"
and "ptr |∈| object_ptr_kinds h"
shows "h ⊢ ok (get_root_node ptr)"
unfolding get_root_node_def
using assms get_ancestors_ok
by auto
lemma get_ancestors_parent:
assumes "heap_is_wellformed h"
and "h ⊢ get_parent child →⇩r Some parent"
shows "h ⊢ get_ancestors (cast child) →⇩r (cast child) # parent # ancestors
⟷ h ⊢ get_ancestors parent →⇩r parent # ancestors"
proof
assume a1: "h ⊢ get_ancestors (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r child) →⇩r
cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r child # parent # ancestors"
then have "h ⊢ Heap_Error_Monad.bind (check_in_heap (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r child))
(λ_. Heap_Error_Monad.bind (get_parent child)
(λx. Heap_Error_Monad.bind (case x of None ⇒ return [] | Some x ⇒ get_ancestors x)
(λancestors. return (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r child # ancestors))))
→⇩r cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r child # parent # ancestors"
by(simp add: get_ancestors_def)
then show "h ⊢ get_ancestors parent →⇩r parent # ancestors"
using assms(2) apply(auto elim!: bind_returns_result_E2 split: option.splits)[1]
using returns_result_eq by fastforce
next
assume "h ⊢ get_ancestors parent →⇩r parent # ancestors"
then show "h ⊢ get_ancestors (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r child) →⇩r cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r child # parent # ancestors"
using assms(2)
apply(simp (no_asm) add: get_ancestors_def)
apply(auto intro!: bind_pure_returns_result_I split: option.splits)[1]
by (metis (full_types) assms(2) check_in_heap_ptr_in_heap is_OK_returns_result_I
local.get_parent_ptr_in_heap node_ptr_kinds_commutes old.unit.exhaust
select_result_I)
qed
lemma get_ancestors_never_empty:
assumes "heap_is_wellformed h"
and "h ⊢ get_ancestors child →⇩r ancestors"
shows "ancestors ≠ []"
proof(insert assms(2), induct arbitrary: ancestors rule: heap_wellformed_induct_rev[OF assms(1)])
case (1 child)
then show ?case
proof (induct "cast⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r⇩2⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r child")
case None
then show ?case
apply(simp add: get_ancestors_def)
by(auto elim!: bind_returns_result_E2 split: option.splits)
next
case (Some child_node)
then obtain parent_opt where parent_opt: "h ⊢ get_parent child_node →⇩r parent_opt"
apply(simp add: get_ancestors_def)
by(auto elim!: bind_returns_result_E2 split: option.splits)
with Some show ?case
proof(induct parent_opt)
case None
then show ?case
apply(simp add: get_ancestors_def)
by(auto elim!: bind_returns_result_E2 split: option.splits)
next
case (Some option)
then show ?case
apply(simp add: get_ancestors_def)
by(auto elim!: bind_returns_result_E2 split: option.splits)
qed
qed
qed
lemma get_ancestors_subset:
assumes "heap_is_wellformed h"
and "h ⊢ get_ancestors ptr →⇩r ancestors"
and "ancestor ∈ set ancestors"
and "h ⊢ get_ancestors ancestor →⇩r ancestor_ancestors"
and type_wf: "type_wf h"
and known_ptrs: "known_ptrs h"
shows "set ancestor_ancestors ⊆ set ancestors"
proof (insert assms(1) assms(2) assms(3), induct ptr arbitrary: ancestors
rule: heap_wellformed_induct_rev)
case (step child)
have "child |∈| object_ptr_kinds h"
using get_ancestors_ptr_in_heap step(2) by auto
show ?case
proof (induct "cast⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r⇩2⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r child")
case None
then have "ancestors = [child]"
using step(2) step(3)
by(auto simp add: get_ancestors_def elim!: bind_returns_result_E2)
show ?case
using step(2) step(3)
apply(auto simp add: ‹ancestors = [child]›)[1]
using assms(4) returns_result_eq by fastforce
next
case (Some child_node)
note s1 = Some
obtain parent_opt where parent_opt: "h ⊢ get_parent child_node →⇩r parent_opt"
using ‹child |∈| object_ptr_kinds h› assms(1) Some[symmetric]
get_parent_ok[OF type_wf known_ptrs]
by (metis (no_types, lifting) is_OK_returns_result_E known_ptrs get_parent_ok
l_get_parent⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms node_ptr_casts_commute node_ptr_kinds_commutes)
then show ?case
proof (induct parent_opt)
case None
then have "ancestors = [child]"
using step(2) step(3) s1
apply(simp add: get_ancestors_def)
by(auto elim!: bind_returns_result_E2 split: option.splits dest: returns_result_eq)
show ?case
using step(2) step(3)
apply(auto simp add: ‹ancestors = [child]›)[1]
using assms(4) returns_result_eq by fastforce
next
case (Some parent)
have "h ⊢ Heap_Error_Monad.bind (check_in_heap child)
(λ_. Heap_Error_Monad.bind
(case cast⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r⇩2⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r child of None ⇒ return []
| Some node_ptr ⇒ Heap_Error_Monad.bind (get_parent node_ptr)
(λparent_ptr_opt. case parent_ptr_opt of None ⇒ return []
| Some x ⇒ get_ancestors x))
(λancestors. return (child # ancestors)))
→⇩r ancestors"
using step(2)
by(simp add: get_ancestors_def)
moreover obtain tl_ancestors where tl_ancestors: "ancestors = child # tl_ancestors"
using calculation
by(auto elim!: bind_returns_result_E2 split: option.splits)
ultimately have "h ⊢ get_ancestors parent →⇩r tl_ancestors"
using s1 Some
by(auto elim!: bind_returns_result_E2 split: option.splits dest: returns_result_eq)
show ?case
using step(1)[OF s1[symmetric, simplified] Some ‹h ⊢ get_ancestors parent →⇩r tl_ancestors›]
step(3)
apply(auto simp add: tl_ancestors)[1]
by (metis assms(4) insert_iff list.simps(15) local.step(2) returns_result_eq tl_ancestors)
qed
qed
qed
lemma get_ancestors_also_parent:
assumes "heap_is_wellformed h"
and "h ⊢ get_ancestors some_ptr →⇩r ancestors"
and "cast child ∈ set ancestors"
and "h ⊢ get_parent child →⇩r Some parent"
and type_wf: "type_wf h"
and known_ptrs: "known_ptrs h"
shows "parent ∈ set ancestors"
proof -
obtain child_ancestors where child_ancestors: "h ⊢ get_ancestors (cast child) →⇩r child_ancestors"
by (meson assms(1) assms(4) get_ancestors_ok is_OK_returns_result_I known_ptrs
local.get_parent_ptr_in_heap node_ptr_kinds_commutes returns_result_select_result
type_wf)
then have "parent ∈ set child_ancestors"
apply(simp add: get_ancestors_def)
by(auto elim!: bind_returns_result_E2 split: option.splits dest!: returns_result_eq[OF assms(4)]
get_ancestors_ptr)
then show ?thesis
using assms child_ancestors get_ancestors_subset by blast
qed
lemma get_ancestors_obtains_children:
assumes "heap_is_wellformed h"
and "ancestor ≠ ptr"
and "ancestor ∈ set ancestors"
and "h ⊢ get_ancestors ptr →⇩r ancestors"
and type_wf: "type_wf h"
and known_ptrs: "known_ptrs h"
obtains children ancestor_child where "h ⊢ get_child_nodes ancestor →⇩r children"
and "ancestor_child ∈ set children" and "cast ancestor_child ∈ set ancestors"
proof -
assume 0: "(⋀children ancestor_child.
h ⊢ get_child_nodes ancestor →⇩r children ⟹
ancestor_child ∈ set children ⟹ cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r ancestor_child ∈ set ancestors
⟹ thesis)"
have "∃child. h ⊢ get_parent child →⇩r Some ancestor ∧ cast child ∈ set ancestors"
proof (insert assms(1) assms(2) assms(3) assms(4), induct ptr arbitrary: ancestors
rule: heap_wellformed_induct_rev)
case (step child)
have "child |∈| object_ptr_kinds h"
using get_ancestors_ptr_in_heap step(4) by auto
show ?case
proof (induct "cast⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r⇩2⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r child")
case None
then have "ancestors = [child]"
using step(3) step(4)
by(auto simp add: get_ancestors_def elim!: bind_returns_result_E2)
show ?case
using step(2) step(3) step(4)
by(auto simp add: ‹ancestors = [child]›)
next
case (Some child_node)
note s1 = Some
obtain parent_opt where parent_opt: "h ⊢ get_parent child_node →⇩r parent_opt"
using ‹child |∈| object_ptr_kinds h› assms(1) Some[symmetric]
using get_parent_ok known_ptrs type_wf
by (metis (no_types, lifting) is_OK_returns_result_E node_ptr_casts_commute
node_ptr_kinds_commutes)
then show ?case
proof (induct parent_opt)
case None
then have "ancestors = [child]"
using step(2) step(3) step(4) s1
apply(simp add: get_ancestors_def)
by(auto elim!: bind_returns_result_E2 split: option.splits dest: returns_result_eq)
show ?case
using step(2) step(3) step(4)
by(auto simp add: ‹ancestors = [child]›)
next
case (Some parent)
have "h ⊢ Heap_Error_Monad.bind (check_in_heap child)
(λ_. Heap_Error_Monad.bind
(case cast⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r⇩2⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r child of None ⇒ return []
| Some node_ptr ⇒ Heap_Error_Monad.bind (get_parent node_ptr)
(λparent_ptr_opt. case parent_ptr_opt of None ⇒ return []
| Some x ⇒ get_ancestors x))
(λancestors. return (child # ancestors)))
→⇩r ancestors"
using step(4)
by(simp add: get_ancestors_def)
moreover obtain tl_ancestors where tl_ancestors: "ancestors = child # tl_ancestors"
using calculation
by(auto elim!: bind_returns_result_E2 split: option.splits)
ultimately have "h ⊢ get_ancestors parent →⇩r tl_ancestors"
using s1 Some
by(auto elim!: bind_returns_result_E2 split: option.splits dest: returns_result_eq)
have "ancestor ∈ set tl_ancestors"
using tl_ancestors step(2) step(3) by auto
show ?case
proof (cases "ancestor ≠ parent")
case True
show ?thesis
using step(1)[OF s1[symmetric, simplified] Some True
‹ancestor ∈ set tl_ancestors› ‹h ⊢ get_ancestors parent →⇩r tl_ancestors›]
using tl_ancestors by auto
next
case False
have "child ∈ set ancestors"
using step(4) get_ancestors_ptr by simp
then show ?thesis
using Some False s1[symmetric] by(auto)
qed
qed
qed
qed
then obtain child where child: "h ⊢ get_parent child →⇩r Some ancestor"
and in_ancestors: "cast child ∈ set ancestors"
by auto
then obtain children where
children: "h ⊢ get_child_nodes ancestor →⇩r children" and
child_in_children: "child ∈ set children"
using get_parent_child_dual by blast
show thesis
using 0[OF children child_in_children] child assms(3) in_ancestors by blast
qed
lemma get_ancestors_parent_child_rel:
assumes "heap_is_wellformed h"
and "h ⊢ get_ancestors child →⇩r ancestors"
and known_ptrs: "known_ptrs h"
and type_wf: "type_wf h"
shows "(ptr, child) ∈ (parent_child_rel h)⇧* ⟷ ptr ∈ set ancestors"
proof (safe)
assume 3: "(ptr, child) ∈ (parent_child_rel h)⇧*"
show "ptr ∈ set ancestors"
proof (insert 3, induct ptr rule: heap_wellformed_induct[OF assms(1)])
case (1 ptr)
then show ?case
proof (cases "ptr = child")
case True
then show ?thesis
by (metis (no_types, lifting) assms(2) bind_returns_result_E get_ancestors_def
in_set_member member_rec(1) return_returns_result)
next
case False
obtain ptr_child where
ptr_child: "(ptr, ptr_child) ∈ (parent_child_rel h) ∧ (ptr_child, child) ∈ (parent_child_rel h)⇧*"
using converse_rtranclE[OF 1(2)] ‹ptr ≠ child›
by metis
then obtain ptr_child_node
where ptr_child_ptr_child_node: "ptr_child = cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r ptr_child_node"
using ptr_child node_ptr_casts_commute3 parent_child_rel_node_ptr
by (metis )
then obtain children where
children: "h ⊢ get_child_nodes ptr →⇩r children" and
ptr_child_node: "ptr_child_node ∈ set children"
proof -
assume a1: "⋀children. ⟦h ⊢ get_child_nodes ptr →⇩r children; ptr_child_node ∈ set children⟧
⟹ thesis"
have "ptr |∈| object_ptr_kinds h"
using local.parent_child_rel_parent_in_heap ptr_child by blast
moreover have "ptr_child_node ∈ set |h ⊢ get_child_nodes ptr|⇩r"
by (metis calculation known_ptrs local.get_child_nodes_ok local.known_ptrs_known_ptr
local.parent_child_rel_child ptr_child ptr_child_ptr_child_node
returns_result_select_result type_wf)
ultimately show ?thesis
using a1 get_child_nodes_ok type_wf known_ptrs
by (meson local.known_ptrs_known_ptr returns_result_select_result)
qed
moreover have "(cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r ptr_child_node, child) ∈ (parent_child_rel h)⇧*"
using ptr_child ptr_child_ptr_child_node by auto
ultimately have "cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r ptr_child_node ∈ set ancestors"
using 1 by auto
moreover have "h ⊢ get_parent ptr_child_node →⇩r Some ptr"
using assms(1) children ptr_child_node child_parent_dual
using known_ptrs type_wf by blast
ultimately show ?thesis
using get_ancestors_also_parent assms type_wf by blast
qed
qed
next
assume 3: "ptr ∈ set ancestors"
show "(ptr, child) ∈ (parent_child_rel h)⇧*"
proof (insert 3, induct ptr rule: heap_wellformed_induct[OF assms(1)])
case (1 ptr)
then show ?case
proof (cases "ptr = child")
case True
then show ?thesis
by simp
next
case False
then obtain children ptr_child_node where
children: "h ⊢ get_child_nodes ptr →⇩r children" and
ptr_child_node: "ptr_child_node ∈ set children" and
ptr_child_node_in_ancestors: "cast ptr_child_node ∈ set ancestors"
using 1(2) assms(2) get_ancestors_obtains_children assms(1)
using known_ptrs type_wf by blast
then have "(cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r ptr_child_node, child) ∈ (parent_child_rel h)⇧*"
using 1(1) by blast
moreover have "(ptr, cast ptr_child_node) ∈ parent_child_rel h"
using children ptr_child_node assms(1) parent_child_rel_child_nodes2
using child_parent_dual known_ptrs parent_child_rel_parent type_wf
by blast
ultimately show ?thesis
by auto
qed
qed
qed
lemma get_root_node_parent_child_rel:
assumes "heap_is_wellformed h"
and "h ⊢ get_root_node child →⇩r root"
and known_ptrs: "known_ptrs h"
and type_wf: "type_wf h"
shows "(root, child) ∈ (parent_child_rel h)⇧*"
using assms get_ancestors_parent_child_rel
apply(auto simp add: get_root_node_def elim!: bind_returns_result_E2)[1]
using get_ancestors_never_empty last_in_set by blast
lemma get_ancestors_eq:
assumes "heap_is_wellformed h"
and "heap_is_wellformed h'"
and "⋀object_ptr w. object_ptr ≠ ptr ⟹ w ∈ get_child_nodes_locs object_ptr ⟹ w h h'"
and pointers_preserved: "⋀object_ptr. preserved (get_M⇩O⇩b⇩j⇩e⇩c⇩t object_ptr RObject.nothing) h h'"
and known_ptrs: "known_ptrs h"
and known_ptrs': "known_ptrs h'"
and "h ⊢ get_ancestors ptr →⇩r ancestors"
and type_wf: "type_wf h"
and type_wf': "type_wf h'"
shows "h' ⊢ get_ancestors ptr →⇩r ancestors"
proof -
have object_ptr_kinds_eq3: "object_ptr_kinds h = object_ptr_kinds h'"
using pointers_preserved object_ptr_kinds_preserved_small by blast
then have object_ptr_kinds_M_eq:
"⋀ptrs. h ⊢ object_ptr_kinds_M →⇩r ptrs = h' ⊢ object_ptr_kinds_M →⇩r ptrs"
by(simp add: object_ptr_kinds_M_defs)
then have object_ptr_kinds_eq: "|h ⊢ object_ptr_kinds_M|⇩r = |h' ⊢ object_ptr_kinds_M|⇩r"
by(simp)
have "h' ⊢ ok (get_ancestors ptr)"
using get_ancestors_ok get_ancestors_ptr_in_heap object_ptr_kinds_eq3 assms(1) known_ptrs
known_ptrs' assms(2) assms(7) type_wf'
by blast
then obtain ancestors' where ancestors': "h' ⊢ get_ancestors ptr →⇩r ancestors'"
by auto
obtain root where root: "h ⊢ get_root_node ptr →⇩r root"
proof -
assume 0: "(⋀root. h ⊢ get_root_node ptr →⇩r root ⟹ thesis)"
show thesis
apply(rule 0)
using assms(7)
by(auto simp add: get_root_node_def elim!: bind_returns_result_E2 split: option.splits)
qed
have children_eq:
"⋀p children. p ≠ ptr ⟹ h ⊢ get_child_nodes p →⇩r children = h' ⊢ get_child_nodes p →⇩r children"
using get_child_nodes_reads assms(3)
apply(simp add: reads_def reflp_def transp_def preserved_def)
by blast
have "acyclic (parent_child_rel h)"
using assms(1) local.parent_child_rel_acyclic by auto
have "acyclic (parent_child_rel h')"
using assms(2) local.parent_child_rel_acyclic by blast
have 2: "⋀c parent_opt. cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r c ∈ set ancestors ∩ set ancestors'
⟹ h ⊢ get_parent c →⇩r parent_opt = h' ⊢ get_parent c →⇩r parent_opt"
proof -
fix c parent_opt
assume 1: " cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r c ∈ set ancestors ∩ set ancestors'"
obtain ptrs where ptrs: "h ⊢ object_ptr_kinds_M →⇩r ptrs"
by simp
let ?P = "(λptr. Heap_Error_Monad.bind (get_child_nodes ptr) (λchildren. return (c ∈ set children)))"
have children_eq_True: "⋀p. p ∈ set ptrs ⟹ h ⊢ ?P p →⇩r True ⟷ h' ⊢ ?P p →⇩r True"
proof -
fix p
assume "p ∈ set ptrs"
then show "h ⊢ ?P p →⇩r True ⟷ h' ⊢ ?P p →⇩r True"
proof (cases "p = ptr")
case True
have "(cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r c, ptr) ∈ (parent_child_rel h)⇧*"
using get_ancestors_parent_child_rel 1 assms by blast
then have "(ptr, cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r c) ∉ (parent_child_rel h)"
proof (cases "cast c = ptr")
case True
then show ?thesis
using ‹acyclic (parent_child_rel h)› by(auto simp add: acyclic_def)
next
case False
then have "(ptr, cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r c) ∉ (parent_child_rel h)⇧*"
using ‹acyclic (parent_child_rel h)› False rtrancl_eq_or_trancl rtrancl_trancl_trancl
‹(cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r c, ptr) ∈ (parent_child_rel h)⇧*›
by (metis acyclic_def)
then show ?thesis
using r_into_rtrancl by auto
qed
obtain children where children: "h ⊢ get_child_nodes ptr →⇩r children"
using type_wf
by (metis ‹h' ⊢ ok get_ancestors ptr› assms(1) get_ancestors_ptr_in_heap get_child_nodes_ok
heap_is_wellformed_def is_OK_returns_result_E known_ptrs local.known_ptrs_known_ptr
object_ptr_kinds_eq3)
then have "c ∉ set children"
using ‹(ptr, cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r c) ∉ (parent_child_rel h)› assms(1)
using parent_child_rel_child_nodes2
using child_parent_dual known_ptrs parent_child_rel_parent
type_wf by blast
with children have "h ⊢ ?P p →⇩r False"
by(auto simp add: True)
moreover have "(cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r c, ptr) ∈ (parent_child_rel h')⇧*"
using get_ancestors_parent_child_rel assms(2) ancestors' 1 known_ptrs' type_wf
type_wf' by blast
then have "(ptr, cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r c) ∉ (parent_child_rel h')"
proof (cases "cast c = ptr")
case True
then show ?thesis
using ‹acyclic (parent_child_rel h')› by(auto simp add: acyclic_def)
next
case False
then have "(ptr, cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r c) ∉ (parent_child_rel h')⇧*"
using ‹acyclic (parent_child_rel h')› False rtrancl_eq_or_trancl rtrancl_trancl_trancl
‹(cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r c, ptr) ∈ (parent_child_rel h')⇧*›
by (metis acyclic_def)
then show ?thesis
using r_into_rtrancl by auto
qed
then have "(ptr, cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r c) ∉ (parent_child_rel h')"
using r_into_rtrancl by auto
obtain children' where children': "h' ⊢ get_child_nodes ptr →⇩r children'"
using type_wf type_wf'
by (meson ‹h' ⊢ ok (get_ancestors ptr)› assms(2) get_ancestors_ptr_in_heap
get_child_nodes_ok is_OK_returns_result_E known_ptrs'
local.known_ptrs_known_ptr)
then have "c ∉ set children'"
using ‹(ptr, cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r c) ∉ (parent_child_rel h')› assms(2) type_wf type_wf'
using parent_child_rel_child_nodes2 child_parent_dual known_ptrs' parent_child_rel_parent
by auto
with children' have "h' ⊢ ?P p →⇩r False"
by(auto simp add: True)
ultimately show ?thesis
by (metis returns_result_eq)
next
case False
then show ?thesis
using children_eq ptrs
by (metis (no_types, lifting) bind_pure_returns_result_I bind_returns_result_E
get_child_nodes_pure return_returns_result)
qed
qed
have "⋀pa. pa ∈ set ptrs ⟹ h ⊢ ok (get_child_nodes pa
⤜ (λchildren. return (c ∈ set children))) = h' ⊢ ok ( get_child_nodes pa
⤜ (λchildren. return (c ∈ set children)))"
using assms(1) assms(2) object_ptr_kinds_eq ptrs type_wf type_wf'
by (metis (no_types, lifting) ObjectMonad.ptr_kinds_ptr_kinds_M bind_is_OK_pure_I
get_child_nodes_ok get_child_nodes_pure known_ptrs'
local.known_ptrs_known_ptr return_ok select_result_I2)
have children_eq_False:
"⋀pa. pa ∈ set ptrs ⟹ h ⊢ get_child_nodes pa
⤜ (λchildren. return (c ∈ set children)) →⇩r False = h' ⊢ get_child_nodes pa
⤜ (λchildren. return (c ∈ set children)) →⇩r False"
proof
fix pa
assume "pa ∈ set ptrs"
and "h ⊢ get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)) →⇩r False"
have "h ⊢ ok (get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)))
⟹ h' ⊢ ok ( get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)))"
using ‹pa ∈ set ptrs› ‹⋀pa. pa ∈ set ptrs ⟹ h ⊢ ok (get_child_nodes pa
⤜ (λchildren. return (c ∈ set children))) = h' ⊢ ok ( get_child_nodes pa
⤜ (λchildren. return (c ∈ set children)))›
by auto
moreover have "h ⊢ get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)) →⇩r False
⟹ h' ⊢ get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)) →⇩r False"
by (metis (mono_tags, lifting) ‹⋀pa. pa ∈ set ptrs
⟹ h ⊢ get_child_nodes pa
⤜ (λchildren. return (c ∈ set children)) →⇩r True = h' ⊢ get_child_nodes pa
⤜ (λchildren. return (c ∈ set children)) →⇩r True› ‹pa ∈ set ptrs›
calculation is_OK_returns_result_I returns_result_eq returns_result_select_result)
ultimately show "h' ⊢ get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)) →⇩r False"
using ‹h ⊢ get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)) →⇩r False›
by auto
next
fix pa
assume "pa ∈ set ptrs"
and "h' ⊢ get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)) →⇩r False"
have "h' ⊢ ok (get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)))
⟹ h ⊢ ok ( get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)))"
using ‹pa ∈ set ptrs› ‹⋀pa. pa ∈ set ptrs
⟹ h ⊢ ok (get_child_nodes pa
⤜ (λchildren. return (c ∈ set children))) = h' ⊢ ok ( get_child_nodes pa
⤜ (λchildren. return (c ∈ set children)))›
by auto
moreover have "h' ⊢ get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)) →⇩r False
⟹ h ⊢ get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)) →⇩r False"
by (metis (mono_tags, lifting)
‹⋀pa. pa ∈ set ptrs ⟹ h ⊢ get_child_nodes pa
⤜ (λchildren. return (c ∈ set children)) →⇩r True = h' ⊢ get_child_nodes pa
⤜ (λchildren. return (c ∈ set children)) →⇩r True› ‹pa ∈ set ptrs›
calculation is_OK_returns_result_I returns_result_eq returns_result_select_result)
ultimately show "h ⊢ get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)) →⇩r False"
using ‹h' ⊢ get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)) →⇩r False› by blast
qed
have filter_eq: "⋀xs. h ⊢ filter_M ?P ptrs →⇩r xs = h' ⊢ filter_M ?P ptrs →⇩r xs"
proof (rule filter_M_eq)
show
"⋀xs x. pure (Heap_Error_Monad.bind (get_child_nodes x) (λchildren. return (c ∈ set children))) h"
by(auto intro!: bind_pure_I)
next
show
"⋀xs x. pure (Heap_Error_Monad.bind (get_child_nodes x) (λchildren. return (c ∈ set children))) h'"
by(auto intro!: bind_pure_I)
next
fix xs b x
assume 0: "x ∈ set ptrs"
then show "h ⊢ Heap_Error_Monad.bind (get_child_nodes x) (λchildren. return (c ∈ set children)) →⇩r b
= h' ⊢ Heap_Error_Monad.bind (get_child_nodes x) (λchildren. return (c ∈ set children)) →⇩r b"
apply(induct b)
using children_eq_True apply blast
using children_eq_False apply blast
done
qed
show "h ⊢ get_parent c →⇩r parent_opt = h' ⊢ get_parent c →⇩r parent_opt"
apply(simp add: get_parent_def)
apply(rule bind_cong_2)
apply(simp)
apply(simp)
apply(simp add: check_in_heap_def node_ptr_kinds_def object_ptr_kinds_eq3)
apply(rule bind_cong_2)
apply(auto simp add: object_ptr_kinds_M_eq object_ptr_kinds_eq3)[1]
apply(auto simp add: object_ptr_kinds_M_eq object_ptr_kinds_eq3)[1]
apply(auto simp add: object_ptr_kinds_M_eq object_ptr_kinds_eq3)[1]
apply(rule bind_cong_2)
apply(auto intro!: filter_M_pure_I bind_pure_I)[1]
apply(auto intro!: filter_M_pure_I bind_pure_I)[1]
apply(auto simp add: filter_eq )[1]
using filter_eq ptrs apply auto[1]
using filter_eq ptrs by auto
qed
have "ancestors = ancestors'"
proof(insert assms(1) assms(7) ancestors' 2, induct ptr arbitrary: ancestors ancestors'
rule: heap_wellformed_induct_rev)
case (step child)
show ?case
using step(2) step(3) step(4)
apply(simp add: get_ancestors_def)
apply(auto intro!: elim!: bind_returns_result_E2 split: option.splits)[1]
using returns_result_eq apply fastforce
apply (meson option.simps(3) returns_result_eq)
by (metis IntD1 IntD2 option.inject returns_result_eq step.hyps)
qed
then show ?thesis
using assms(5) ancestors'
by simp
qed
lemma get_ancestors_remains_not_in_ancestors:
assumes "heap_is_wellformed h"
and "heap_is_wellformed h'"
and "h ⊢ get_ancestors ptr →⇩r ancestors"
and "h' ⊢ get_ancestors ptr →⇩r ancestors'"
and "⋀p children children'. h ⊢ get_child_nodes p →⇩r children
⟹ h' ⊢ get_child_nodes p →⇩r children' ⟹ set children' ⊆ set children"
and "node ∉ set ancestors"
and object_ptr_kinds_eq3: "object_ptr_kinds h = object_ptr_kinds h'"
and known_ptrs: "known_ptrs h"
and type_wf: "type_wf h"
and type_wf': "type_wf h'"
shows "node ∉ set ancestors'"
proof -
have object_ptr_kinds_M_eq:
"⋀ptrs. h ⊢ object_ptr_kinds_M →⇩r ptrs = h' ⊢ object_ptr_kinds_M →⇩r ptrs"
using object_ptr_kinds_eq3
by(simp add: object_ptr_kinds_M_defs)
then have object_ptr_kinds_eq: "|h ⊢ object_ptr_kinds_M|⇩r = |h' ⊢ object_ptr_kinds_M|⇩r"
by(simp)
show ?thesis
proof (insert assms(1) assms(3) assms(4) assms(6), induct ptr arbitrary: ancestors ancestors'
rule: heap_wellformed_induct_rev)
case (step child)
have 1: "⋀p parent. h' ⊢ get_parent p →⇩r Some parent ⟹ h ⊢ get_parent p →⇩r Some parent"
proof -
fix p parent
assume "h' ⊢ get_parent p →⇩r Some parent"
then obtain children' where
children': "h' ⊢ get_child_nodes parent →⇩r children'" and
p_in_children': "p ∈ set children'"
using get_parent_child_dual by blast
obtain children where children: "h ⊢ get_child_nodes parent →⇩r children"
using get_child_nodes_ok assms(1) get_child_nodes_ptr_in_heap object_ptr_kinds_eq children'
known_ptrs
using type_wf type_wf'
by (metis ‹h' ⊢ get_parent p →⇩r Some parent› get_parent_parent_in_heap is_OK_returns_result_E
local.known_ptrs_known_ptr object_ptr_kinds_eq3)
have "p ∈ set children"
using assms(5) children children' p_in_children'
by blast
then show "h ⊢ get_parent p →⇩r Some parent"
using child_parent_dual assms(1) children known_ptrs type_wf by blast
qed
have "node ≠ child"
using assms(1) get_ancestors_parent_child_rel step.prems(1) step.prems(3) known_ptrs
using type_wf type_wf'
by blast
then show ?case
using step(2) step(3)
apply(simp add: get_ancestors_def)
using step(4)
apply(auto elim!: bind_returns_result_E2 split: option.splits)[1]
using 1
apply (meson option.distinct(1) returns_result_eq)
by (metis "1" option.inject returns_result_eq step.hyps)
qed
qed
lemma get_ancestors_ptrs_in_heap:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ get_ancestors ptr →⇩r ancestors"
assumes "ptr' ∈ set ancestors"
shows "ptr' |∈| object_ptr_kinds h"
proof (insert