Theory Core_DOM_SC_DOM_Components
section ‹Core SC DOM Components II›
theory Core_DOM_SC_DOM_Components
imports
Core_DOM_DOM_Components
begin
declare [[smt_timeout=2400]]
section ‹Scope Components›
subsection ‹Definition›
locale l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs =
l_get_disconnected_nodes_defs get_disconnected_nodes get_disconnected_nodes_locs +
l_get_owner_document_defs get_owner_document +
l_to_tree_order_defs to_tree_order
for get_owner_document :: "(_::linorder) object_ptr ⇒ ((_) heap, exception, (_) document_ptr) prog"
and get_disconnected_nodes :: "(_) document_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
and get_disconnected_nodes_locs :: "(_) document_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
and to_tree_order :: "(_) object_ptr ⇒ ((_) heap, exception, (_) object_ptr list) prog"
begin
definition a_get_scdom_component :: "(_) object_ptr ⇒ (_, (_) object_ptr list) dom_prog"
where
"a_get_scdom_component ptr = do {
document ← get_owner_document ptr;
disc_nodes ← get_disconnected_nodes document;
tree_order ← to_tree_order (cast document);
disconnected_tree_orders ← map_M (to_tree_order ∘ cast) disc_nodes;
return (tree_order @ (concat disconnected_tree_orders))
}"
definition a_is_strongly_scdom_component_safe ::
"(_) object_ptr set ⇒ (_) object_ptr set ⇒ (_) heap ⇒ (_) heap ⇒ bool"
where
"a_is_strongly_scdom_component_safe S⇩a⇩r⇩g S⇩r⇩e⇩s⇩u⇩l⇩t h h' = (
let removed_pointers = fset (object_ptr_kinds h) - fset (object_ptr_kinds h') in
let added_pointers = fset (object_ptr_kinds h') - fset (object_ptr_kinds h) in
let arg_components =
(⋃ptr ∈ (⋃ptr ∈ S⇩a⇩r⇩g. set |h ⊢ a_get_scdom_component ptr|⇩r) ∩
fset (object_ptr_kinds h). set |h ⊢ a_get_scdom_component ptr|⇩r) in
let arg_components' =
(⋃ptr ∈ (⋃ptr ∈ S⇩a⇩r⇩g. set |h ⊢ a_get_scdom_component ptr|⇩r) ∩
fset (object_ptr_kinds h'). set |h' ⊢ a_get_scdom_component ptr|⇩r) in
removed_pointers ⊆ arg_components ∧
added_pointers ⊆ arg_components' ∧
S⇩r⇩e⇩s⇩u⇩l⇩t ⊆ arg_components' ∧
(∀outside_ptr ∈ fset (object_ptr_kinds h) ∩ fset (object_ptr_kinds h') -
(⋃ptr ∈ S⇩a⇩r⇩g. set |h ⊢ a_get_scdom_component ptr|⇩r). preserved (get_M outside_ptr id) h h'))"
definition a_is_weakly_scdom_component_safe ::
"(_) object_ptr set ⇒ (_) object_ptr set ⇒ (_) heap ⇒ (_) heap ⇒ bool"
where
"a_is_weakly_scdom_component_safe S⇩a⇩r⇩g S⇩r⇩e⇩s⇩u⇩l⇩t h h' = (
let removed_pointers = fset (object_ptr_kinds h) - fset (object_ptr_kinds h') in
let added_pointers = fset (object_ptr_kinds h') - fset (object_ptr_kinds h) in
let arg_components =
(⋃ptr ∈ (⋃ptr ∈ S⇩a⇩r⇩g. set |h ⊢ a_get_scdom_component ptr|⇩r) ∩
fset (object_ptr_kinds h). set |h ⊢ a_get_scdom_component ptr|⇩r) in
let arg_components' =
(⋃ptr ∈ (⋃ptr ∈ S⇩a⇩r⇩g. set |h ⊢ a_get_scdom_component ptr|⇩r) ∩
fset (object_ptr_kinds h'). set |h' ⊢ a_get_scdom_component ptr|⇩r) in
removed_pointers ⊆ arg_components ∧
S⇩r⇩e⇩s⇩u⇩l⇩t ⊆ arg_components' ∪ added_pointers ∧
(∀outside_ptr ∈ fset (object_ptr_kinds h) ∩ fset (object_ptr_kinds h') -
(⋃ptr ∈ S⇩a⇩r⇩g. set |h ⊢ a_get_scdom_component ptr|⇩r). preserved (get_M outside_ptr id) h h'))"
end
global_interpretation l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs get_owner_document get_disconnected_nodes
get_disconnected_nodes_locs to_tree_order
defines get_scdom_component = "l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs.a_get_scdom_component
get_owner_document get_disconnected_nodes to_tree_order"
and is_strongly_scdom_component_safe = a_is_strongly_scdom_component_safe
and is_weakly_scdom_component_safe = a_is_weakly_scdom_component_safe
.
locale l_get_scdom_component_defs =
fixes get_scdom_component :: "(_) object_ptr ⇒ (_, (_) object_ptr list) dom_prog"
fixes is_strongly_scdom_component_safe ::
"(_) object_ptr set ⇒ (_) object_ptr set ⇒ (_) heap ⇒ (_) heap ⇒ bool"
fixes is_weakly_scdom_component_safe ::
"(_) object_ptr set ⇒ (_) object_ptr set ⇒ (_) heap ⇒ (_) heap ⇒ bool"
locale l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_scdom_component_defs +
l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs +
assumes get_scdom_component_impl: "get_scdom_component = a_get_scdom_component"
assumes is_strongly_scdom_component_safe_impl:
"is_strongly_scdom_component_safe = a_is_strongly_scdom_component_safe"
assumes is_weakly_scdom_component_safe_impl:
"is_weakly_scdom_component_safe = a_is_weakly_scdom_component_safe"
begin
lemmas get_scdom_component_def = a_get_scdom_component_def[folded get_scdom_component_impl]
lemmas is_strongly_scdom_component_safe_def =
a_is_strongly_scdom_component_safe_def[folded is_strongly_scdom_component_safe_impl]
lemmas is_weakly_scdom_component_safe_def =
a_is_weakly_scdom_component_safe_def[folded is_weakly_scdom_component_safe_impl]
end
interpretation i_get_scdom_component?: l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
get_scdom_component is_strongly_scdom_component_safe is_weakly_scdom_component_safe
get_owner_document get_disconnected_nodes get_disconnected_nodes_locs to_tree_order
by(auto simp add: l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def get_scdom_component_def
is_strongly_scdom_component_safe_def is_weakly_scdom_component_safe_def instances)
declare l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]
locale l_get_dom_component_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_heap_is_wellformed +
l_get_owner_document +
l_get_owner_document_wf +
l_get_disconnected_nodes +
l_to_tree_order +
l_known_ptr +
l_known_ptrs +
l_get_owner_document_wf_get_root_node_wf +
assumes known_ptr_impl: "known_ptr = DocumentClass.known_ptr"
begin
lemma known_ptr_node_or_document: "known_ptr ptr ⟹ is_node_ptr_kind ptr ∨ is_document_ptr_kind ptr"
by(auto simp add: known_ptr_impl known_ptr_defs DocumentClass.known_ptr_defs
CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs
split: option.splits)
lemma get_scdom_component_ptr_in_heap2:
assumes "h ⊢ ok (get_scdom_component ptr)"
shows "ptr |∈| object_ptr_kinds h"
using assms get_root_node_ptr_in_heap
apply(auto simp add: get_scdom_component_def elim!: bind_is_OK_E3 intro!: map_M_pure_I)[1]
by (simp add: is_OK_returns_result_I local.get_owner_document_ptr_in_heap)
lemma get_scdom_component_subset_get_dom_component:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ get_scdom_component ptr →⇩r sc"
assumes "h ⊢ get_dom_component ptr →⇩r c"
shows "set c ⊆ set sc"
proof -
obtain document disc_nodes tree_order disconnected_tree_orders where
document: "h ⊢ get_owner_document ptr →⇩r document"
and disc_nodes: "h ⊢ get_disconnected_nodes document →⇩r disc_nodes"
and tree_order: "h ⊢ to_tree_order (cast document) →⇩r tree_order"
and disconnected_tree_orders: "h ⊢ map_M (to_tree_order ∘ cast) disc_nodes →⇩r disconnected_tree_orders"
and sc: "sc = tree_order @ (concat disconnected_tree_orders)"
using assms(4)
by(auto simp add: get_scdom_component_def elim!: bind_returns_result_E
elim!: bind_returns_result_E2[rotated, OF get_owner_document_pure, rotated]
elim!: bind_returns_result_E2[rotated, OF get_disconnected_nodes_pure, rotated]
elim!: bind_returns_result_E2[rotated, OF to_tree_order_pure, rotated]
)
obtain root_ptr where root_ptr: "h ⊢ get_root_node ptr →⇩r root_ptr"
and c: "h ⊢ to_tree_order root_ptr →⇩r c"
using assms(5)
by(auto simp add: get_dom_component_def elim!: bind_returns_result_E2[rotated, OF get_root_node_pure, rotated])
show ?thesis
proof (cases "is_document_ptr_kind root_ptr")
case True
then have "cast document = root_ptr"
using get_root_node_document assms(1) assms(2) assms(3) root_ptr document
by (metis document_ptr_casts_commute3 returns_result_eq)
then have "c = tree_order"
using tree_order c
by auto
then show ?thesis
by(simp add: sc)
next
case False
moreover have "root_ptr |∈| object_ptr_kinds h"
using assms(1) assms(2) assms(3) local.get_root_node_root_in_heap root_ptr by blast
ultimately have "is_node_ptr_kind root_ptr"
using assms(3) known_ptrs_known_ptr known_ptr_node_or_document
by auto
then obtain root_node_ptr where root_node_ptr: "root_ptr = cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r root_node_ptr"
by (metis node_ptr_casts_commute3)
then have "h ⊢ get_owner_document root_ptr →⇩r document"
using get_root_node_same_owner_document
using assms(1) assms(2) assms(3) document root_ptr by blast
then have "root_node_ptr ∈ set disc_nodes"
using assms(1) assms(2) assms(3) disc_nodes in_disconnected_nodes_no_parent root_node_ptr
using local.get_root_node_same_no_parent root_ptr by blast
then have "c ∈ set disconnected_tree_orders"
using c root_node_ptr
using map_M_pure_E[OF disconnected_tree_orders]
by (metis (mono_tags, lifting) comp_apply local.to_tree_order_pure select_result_I2)
then show ?thesis
by(auto simp add: sc)
qed
qed
lemma get_scdom_component_ptrs_same_owner_document:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ get_scdom_component ptr →⇩r sc"
assumes "ptr' ∈ set sc"
assumes "h ⊢ get_owner_document ptr →⇩r owner_document"
shows "h ⊢ get_owner_document ptr' →⇩r owner_document"
proof -
obtain document disc_nodes tree_order disconnected_tree_orders where
document: "h ⊢ get_owner_document ptr →⇩r document"
and disc_nodes: "h ⊢ get_disconnected_nodes document →⇩r disc_nodes"
and tree_order: "h ⊢ to_tree_order (cast document) →⇩r tree_order"
and disconnected_tree_orders: "h ⊢ map_M (to_tree_order ∘ cast) disc_nodes →⇩r disconnected_tree_orders"
and sc: "sc = tree_order @ (concat disconnected_tree_orders)"
using assms(4)
by(auto simp add: get_scdom_component_def elim!: bind_returns_result_E
elim!: bind_returns_result_E2[rotated, OF get_owner_document_pure, rotated]
elim!: bind_returns_result_E2[rotated, OF get_disconnected_nodes_pure, rotated]
elim!: bind_returns_result_E2[rotated, OF to_tree_order_pure, rotated]
)
show ?thesis
proof (cases "ptr' ∈ set tree_order")
case True
have "owner_document = document"
using assms(6) document by fastforce
then show ?thesis
by (metis (no_types) True assms(1) assms(2) assms(3) cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r_inject document
document_ptr_casts_commute3 document_ptr_document_ptr_cast document_ptr_kinds_commutes
local.get_owner_document_owner_document_in_heap local.get_root_node_document
local.get_root_node_not_node_same local.to_tree_order_same_root node_ptr_no_document_ptr_cast tree_order)
next
case False
then obtain disconnected_tree_order where disconnected_tree_order:
"ptr' ∈ set disconnected_tree_order" and "disconnected_tree_order ∈ set disconnected_tree_orders"
using sc ‹ptr' ∈ set sc›
by auto
obtain root_ptr' where
root_ptr': "root_ptr' ∈ set disc_nodes" and
"h ⊢ to_tree_order (cast root_ptr') →⇩r disconnected_tree_order"
using map_M_pure_E2[OF disconnected_tree_orders ‹disconnected_tree_order ∈ set disconnected_tree_orders›]
by (metis comp_apply local.to_tree_order_pure)
have "¬(∃parent ∈ fset (object_ptr_kinds h). root_ptr' ∈ set |h ⊢ get_child_nodes parent|⇩r)"
using disc_nodes
by (meson assms(1) assms(2) assms(3) disjoint_iff_not_equal local.get_child_nodes_ok
local.heap_is_wellformed_children_disc_nodes_different local.known_ptrs_known_ptr
returns_result_select_result root_ptr')
then
have "h ⊢ get_parent root_ptr' →⇩r None"
using disc_nodes
by (metis (no_types, opaque_lifting) assms(1) assms(2) assms(3) local.get_parent_child_dual
local.get_parent_ok local.get_parent_parent_in_heap local.heap_is_wellformed_disc_nodes_in_heap
returns_result_select_result root_ptr' select_result_I2 split_option_ex)
then have "h ⊢ get_root_node ptr' →⇩r cast root_ptr'"
using ‹h ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r root_ptr') →⇩r disconnected_tree_order› assms(1)
assms(2) assms(3) disconnected_tree_order local.get_root_node_no_parent
local.to_tree_order_get_root_node local.to_tree_order_ptr_in_result
by blast
then have "h ⊢ get_owner_document (cast root_ptr') →⇩r document"
using assms(1) assms(2) assms(3) disc_nodes local.get_owner_document_disconnected_nodes root_ptr'
by blast
then have "h ⊢ get_owner_document ptr' →⇩r document"
using ‹h ⊢ get_root_node ptr' →⇩r cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r root_ptr'› assms(1) assms(2) assms(3)
local.get_root_node_same_owner_document
by blast
then show ?thesis
using assms(6) document returns_result_eq by force
qed
qed
lemma get_scdom_component_ptrs_same_scope_component:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ get_scdom_component ptr →⇩r sc"
assumes "ptr' ∈ set sc"
shows "h ⊢ get_scdom_component ptr' →⇩r sc"
proof -
obtain document disc_nodes tree_order disconnected_tree_orders where
document: "h ⊢ get_owner_document ptr →⇩r document"
and disc_nodes: "h ⊢ get_disconnected_nodes document →⇩r disc_nodes"
and tree_order: "h ⊢ to_tree_order (cast document) →⇩r tree_order"
and disconnected_tree_orders: "h ⊢ map_M (to_tree_order ∘ cast) disc_nodes →⇩r disconnected_tree_orders"
and sc: "sc = tree_order @ (concat disconnected_tree_orders)"
using assms(4)
by(auto simp add: get_scdom_component_def elim!: bind_returns_result_E
elim!: bind_returns_result_E2[rotated, OF get_owner_document_pure, rotated]
elim!: bind_returns_result_E2[rotated, OF get_disconnected_nodes_pure, rotated]
elim!: bind_returns_result_E2[rotated, OF to_tree_order_pure, rotated]
)
show ?thesis
proof (cases "ptr' ∈ set tree_order")
case True
then have "h ⊢ get_owner_document ptr' →⇩r document"
by (metis assms(1) assms(2) assms(3) cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r_inject document
document_ptr_casts_commute3 document_ptr_kinds_commutes known_ptr_node_or_document
local.get_owner_document_owner_document_in_heap local.get_root_node_document
local.get_root_node_not_node_same local.known_ptrs_known_ptr local.to_tree_order_get_root_node
local.to_tree_order_ptr_in_result node_ptr_no_document_ptr_cast tree_order)
then show ?thesis
using disc_nodes tree_order disconnected_tree_orders sc
by(auto simp add: get_scdom_component_def intro!: bind_pure_returns_result_I map_M_pure_I)
next
case False
then obtain disconnected_tree_order where disconnected_tree_order:
"ptr' ∈ set disconnected_tree_order" and "disconnected_tree_order ∈ set disconnected_tree_orders"
using sc ‹ptr' ∈ set sc›
by auto
obtain root_ptr' where
root_ptr': "root_ptr' ∈ set disc_nodes" and
"h ⊢ to_tree_order (cast root_ptr') →⇩r disconnected_tree_order"
using map_M_pure_E2[OF disconnected_tree_orders ‹disconnected_tree_order ∈ set disconnected_tree_orders›]
by (metis comp_apply local.to_tree_order_pure)
have "¬(∃parent ∈ fset (object_ptr_kinds h). root_ptr' ∈ set |h ⊢ get_child_nodes parent|⇩r)"
using disc_nodes
by (meson assms(1) assms(2) assms(3) disjoint_iff_not_equal local.get_child_nodes_ok
local.heap_is_wellformed_children_disc_nodes_different local.known_ptrs_known_ptr
returns_result_select_result root_ptr')
then
have "h ⊢ get_parent root_ptr' →⇩r None"
using disc_nodes
by (metis (no_types, opaque_lifting) assms(1) assms(2) assms(3)
local.get_parent_child_dual local.get_parent_ok local.get_parent_parent_in_heap
local.heap_is_wellformed_disc_nodes_in_heap returns_result_select_result root_ptr'
select_result_I2 split_option_ex)
then have "h ⊢ get_root_node ptr' →⇩r cast root_ptr'"
using ‹h ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r root_ptr') →⇩r disconnected_tree_order› assms(1)
assms(2) assms(3) disconnected_tree_order local.get_root_node_no_parent
local.to_tree_order_get_root_node local.to_tree_order_ptr_in_result
by blast
then have "h ⊢ get_owner_document (cast root_ptr') →⇩r document"
using assms(1) assms(2) assms(3) disc_nodes local.get_owner_document_disconnected_nodes root_ptr'
by blast
then have "h ⊢ get_owner_document ptr' →⇩r document"
using ‹h ⊢ get_root_node ptr' →⇩r cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r root_ptr'› assms(1) assms(2) assms(3)
local.get_root_node_same_owner_document
by blast
then show ?thesis
using disc_nodes tree_order disconnected_tree_orders sc
by(auto simp add: get_scdom_component_def intro!: bind_pure_returns_result_I map_M_pure_I)
qed
qed
lemma get_scdom_component_ok:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "ptr |∈| object_ptr_kinds h"
shows "h ⊢ ok (get_scdom_component ptr)"
using assms
apply(auto simp add: get_scdom_component_def intro!: bind_is_OK_pure_I map_M_pure_I map_M_ok_I)[1]
using get_owner_document_ok
apply blast
apply (simp add: local.get_disconnected_nodes_ok local.get_owner_document_owner_document_in_heap)
apply (simp add: local.get_owner_document_owner_document_in_heap local.to_tree_order_ok)
using local.heap_is_wellformed_disc_nodes_in_heap local.to_tree_order_ok node_ptr_kinds_commutes
by blast
lemma get_scdom_component_ptr_in_heap:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ get_scdom_component ptr →⇩r sc"
assumes "ptr' ∈ set sc"
shows "ptr' |∈| object_ptr_kinds h"
apply(insert assms )
apply(auto simp add: get_scdom_component_def elim!: bind_returns_result_E2 intro!: map_M_pure_I)[1]
using local.to_tree_order_ptrs_in_heap apply blast
by (metis (no_types, lifting) assms(4) assms(5) bind_returns_result_E
get_scdom_component_ptrs_same_scope_component is_OK_returns_result_I get_scdom_component_def
local.get_owner_document_ptr_in_heap)
lemma get_scdom_component_contains_get_dom_component:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ get_scdom_component ptr →⇩r sc"
assumes "ptr' ∈ set sc"
obtains c where "h ⊢ get_dom_component ptr' →⇩r c" and "set c ⊆ set sc"
proof -
have "h ⊢ get_scdom_component ptr' →⇩r sc"
using assms(1) assms(2) assms(3) assms(4) assms(5) get_scdom_component_ptrs_same_scope_component
by blast
then show ?thesis
by (meson assms(1) assms(2) assms(3) assms(5) get_scdom_component_ptr_in_heap
get_scdom_component_subset_get_dom_component is_OK_returns_result_E local.get_dom_component_ok that)
qed
lemma get_scdom_component_owner_document_same:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ get_scdom_component ptr →⇩r sc"
assumes "ptr' ∈ set sc"
obtains owner_document where "h ⊢ get_owner_document ptr' →⇩r owner_document" and "cast owner_document ∈ set sc"
using assms
apply(auto simp add: get_scdom_component_def elim!: bind_returns_result_E2 intro!: map_M_pure_I)[1]
apply (metis (no_types, lifting) assms(4) assms(5) document_ptr_casts_commute3
document_ptr_document_ptr_cast get_scdom_component_contains_get_dom_component
local.get_dom_component_ptr local.get_dom_component_root_node_same local.get_dom_component_to_tree_order
local.get_root_node_document local.get_root_node_not_node_same local.to_tree_order_ptr_in_result
local.to_tree_order_ptrs_in_heap node_ptr_no_document_ptr_cast)
apply(rule map_M_pure_E2)
apply(simp)
apply(simp)
apply(simp)
using assms(4) assms(5) get_scdom_component_ptrs_same_owner_document local.to_tree_order_ptr_in_result
by blast
lemma get_scdom_component_different_owner_documents:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ get_owner_document ptr →⇩r owner_document"
assumes "h ⊢ get_owner_document ptr' →⇩r owner_document'"
assumes "owner_document ≠ owner_document'"
shows "set |h ⊢ get_scdom_component ptr|⇩r ∩ set |h ⊢ get_scdom_component ptr'|⇩r = {}"
using assms get_scdom_component_ptrs_same_owner_document
by (smt (verit) disjoint_iff_not_equal get_scdom_component_ok is_OK_returns_result_I
local.get_owner_document_ptr_in_heap returns_result_eq returns_result_select_result)
lemma get_scdom_component_ptr:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ get_scdom_component ptr →⇩r c"
shows "ptr ∈ set c"
using assms
by (meson get_scdom_component_ptr_in_heap2 get_scdom_component_subset_get_dom_component
is_OK_returns_result_E is_OK_returns_result_I local.get_dom_component_ok local.get_dom_component_ptr
subsetD)
end
locale l_get_dom_component_get_scdom_component = l_get_owner_document_defs + l_heap_is_wellformed_defs +
l_type_wf + l_known_ptrs + l_get_scdom_component_defs + l_get_dom_component_defs +
assumes get_scdom_component_subset_get_dom_component:
"heap_is_wellformed h ⟹ type_wf h ⟹ known_ptrs h ⟹ h ⊢ get_scdom_component ptr →⇩r sc ⟹
h ⊢ get_dom_component ptr →⇩r c ⟹ set c ⊆ set sc"
assumes get_scdom_component_ptrs_same_scope_component:
"heap_is_wellformed h ⟹ type_wf h ⟹ known_ptrs h ⟹ h ⊢ get_scdom_component ptr →⇩r sc ⟹
ptr' ∈ set sc ⟹ h ⊢ get_scdom_component ptr' →⇩r sc"
assumes get_scdom_component_ptrs_same_owner_document:
"heap_is_wellformed h ⟹ type_wf h ⟹ known_ptrs h ⟹ h ⊢ get_scdom_component ptr →⇩r sc ⟹
ptr' ∈ set sc ⟹ h ⊢ get_owner_document ptr →⇩r owner_document ⟹ h ⊢ get_owner_document ptr' →⇩r owner_document"
assumes get_scdom_component_ok:
"heap_is_wellformed h ⟹ type_wf h ⟹ known_ptrs h ⟹ ptr |∈| object_ptr_kinds h ⟹
h ⊢ ok (get_scdom_component ptr)"
assumes get_scdom_component_ptr_in_heap:
"heap_is_wellformed h ⟹ type_wf h ⟹ known_ptrs h ⟹ h ⊢ get_scdom_component ptr →⇩r sc ⟹
ptr' ∈ set sc ⟹ ptr' |∈| object_ptr_kinds h"
assumes get_scdom_component_contains_get_dom_component:
"(⋀c. h ⊢ get_dom_component ptr' →⇩r c ⟹ set c ⊆ set sc ⟹ thesis) ⟹ heap_is_wellformed h ⟹
type_wf h ⟹ known_ptrs h ⟹ h ⊢ get_scdom_component ptr →⇩r sc ⟹ ptr' ∈ set sc ⟹ thesis"
assumes get_scdom_component_owner_document_same:
"(⋀owner_document. h ⊢ get_owner_document ptr' →⇩r owner_document ⟹ cast owner_document ∈ set sc ⟹ thesis) ⟹
heap_is_wellformed h ⟹ type_wf h ⟹ known_ptrs h ⟹ h ⊢ get_scdom_component ptr →⇩r sc ⟹
ptr' ∈ set sc ⟹ thesis"
assumes get_scdom_component_different_owner_documents:
"heap_is_wellformed h ⟹ type_wf h ⟹ known_ptrs h ⟹ h ⊢ get_owner_document ptr →⇩r owner_document ⟹
h ⊢ get_owner_document ptr' →⇩r owner_document' ⟹ owner_document ≠ owner_document' ⟹
set |h ⊢ get_scdom_component ptr|⇩r ∩ set |h ⊢ get_scdom_component ptr'|⇩r = {}"
interpretation i_get_dom_component_get_scdom_component?: l_get_dom_component_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
get_scdom_component is_strongly_scdom_component_safe is_weakly_scdom_component_safe get_owner_document
get_disconnected_nodes get_disconnected_nodes_locs to_tree_order heap_is_wellformed parent_child_rel
type_wf known_ptr known_ptrs get_parent get_parent_locs get_child_nodes get_child_nodes_locs get_dom_component
is_strongly_dom_component_safe is_weakly_dom_component_safe get_root_node get_root_node_locs get_ancestors
get_ancestors_locs get_element_by_id get_elements_by_class_name get_elements_by_tag_name
by(auto simp add: l_get_dom_component_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def l_get_dom_component_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms_def instances)
declare l_get_dom_component_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]
lemma get_dom_component_get_scdom_component_is_l_get_dom_component_get_scdom_component [instances]:
"l_get_dom_component_get_scdom_component get_owner_document heap_is_wellformed type_wf known_ptr
known_ptrs get_scdom_component get_dom_component"
apply(auto simp add: l_get_dom_component_get_scdom_component_def l_get_dom_component_get_scdom_component_axioms_def instances)[1]
using get_scdom_component_subset_get_dom_component apply fast
using get_scdom_component_ptrs_same_scope_component apply fast
using get_scdom_component_ptrs_same_owner_document apply fast
using get_scdom_component_ok apply fast
using get_scdom_component_ptr_in_heap apply fast
using get_scdom_component_contains_get_dom_component apply blast
using get_scdom_component_owner_document_same apply blast
using get_scdom_component_different_owner_documents apply fast
done
subsubsection ‹get\_child\_nodes›
locale l_get_scdom_component_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_dom_component_get_scdom_component +
l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_dom_component_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin
lemma get_child_nodes_is_strongly_scdom_component_safe_step:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ get_scdom_component ptr →⇩r sc"
assumes "h ⊢ get_child_nodes ptr' →⇩r children"
assumes "child ∈ set children"
shows "cast child ∈ set sc ⟷ ptr' ∈ set sc"
apply(auto)[1]
apply (meson assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) contra_subsetD
get_scdom_component_ptrs_same_scope_component get_scdom_component_subset_get_dom_component
is_OK_returns_result_E local.get_child_nodes_is_strongly_dom_component_safe local.get_dom_component_ok
local.get_dom_component_ptr local.heap_is_wellformed_children_in_heap node_ptr_kinds_commutes)
by (meson assms(1) assms(2) assms(3) assms(4) assms(5) assms(6)
get_scdom_component_contains_get_dom_component is_OK_returns_result_E is_OK_returns_result_I
get_child_nodes_is_strongly_dom_component_safe local.get_child_nodes_ptr_in_heap
local.get_dom_component_ok local.get_dom_component_ptr set_rev_mp)
lemma get_child_nodes_is_strongly_scdom_component_safe:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ get_child_nodes ptr →⇩r children"
assumes "h ⊢ get_child_nodes ptr →⇩h h'"
shows "is_strongly_scdom_component_safe {ptr} (cast ` set children) h h'"
proof -
have "h = h'"
using assms(5)
by (meson local.get_child_nodes_pure pure_returns_heap_eq)
then show ?thesis
using assms
apply(auto simp add: is_strongly_scdom_component_safe_def Let_def preserved_def)[1]
by (smt (verit, del_insts) IntI
get_child_nodes_is_strongly_scdom_component_safe_step is_OK_returns_result_I
local.get_child_nodes_ptr_in_heap local.get_dom_component_ok local.get_dom_component_ptr
local.get_scdom_component_impl local.get_scdom_component_ok
local.get_scdom_component_subset_get_dom_component returns_result_select_result subsetD)
qed
end
interpretation i_get_scdom_component_get_child_nodes?: l_get_scdom_component_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
get_owner_document heap_is_wellformed parent_child_rel type_wf known_ptr known_ptrs
get_scdom_component is_strongly_scdom_component_safe is_weakly_scdom_component_safe
get_dom_component is_strongly_dom_component_safe is_weakly_dom_component_safe get_disconnected_nodes
get_disconnected_nodes_locs to_tree_order get_parent get_parent_locs get_child_nodes
get_child_nodes_locs get_root_node get_root_node_locs get_ancestors get_ancestors_locs get_element_by_id
get_elements_by_class_name get_elements_by_tag_name first_in_tree_order get_attribute get_attribute_locs
by(auto simp add: l_get_scdom_component_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def instances)
declare l_get_scdom_component_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]
subsubsection ‹get\_parent›
locale l_get_scdom_component_get_parent⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_dom_component_get_scdom_component +
l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_dom_component_get_parent⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin
lemma get_parent_is_strongly_scdom_component_safe_step:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ get_scdom_component ptr →⇩r sc"
assumes "h ⊢ get_parent ptr' →⇩r Some parent"
shows "parent ∈ set sc ⟷ cast ptr' ∈ set sc"
by (meson assms(1) assms(2) assms(3) assms(4) assms(5) contra_subsetD
get_scdom_component_contains_get_dom_component local.get_dom_component_ptr
local.get_parent_is_strongly_dom_component_safe_step)
lemma get_parent_is_strongly_scdom_component_safe:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ get_parent node_ptr →⇩r Some parent"
assumes "h ⊢ get_parent node_ptr →⇩h h'"
shows "is_strongly_scdom_component_safe {cast node_ptr} {parent} h h'"
proof -
have "h = h'"
using assms(5)
by (meson local.get_parent_pure pure_returns_heap_eq)
then show ?thesis
using assms
apply(auto simp add: is_strongly_scdom_component_safe_def Let_def preserved_def)[1]
by (smt (verit) Int_iff get_parent_is_strongly_scdom_component_safe_step in_mono
get_dom_component_ptr local.get_dom_component_ok
local.get_parent_parent_in_heap local.get_scdom_component_impl local.get_scdom_component_ok
local.get_scdom_component_ptr_in_heap local.get_scdom_component_ptrs_same_scope_component
local.get_scdom_component_subset_get_dom_component
returns_result_eq returns_result_select_result)
qed
end
interpretation i_get_scdom_component_get_parent?: l_get_scdom_component_get_parent⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
get_owner_document heap_is_wellformed parent_child_rel type_wf known_ptr known_ptrs
get_scdom_component is_strongly_scdom_component_safe is_weakly_scdom_component_safe get_dom_component
is_strongly_dom_component_safe is_weakly_dom_component_safe get_disconnected_nodes
get_disconnected_nodes_locs to_tree_order get_parent get_parent_locs get_child_nodes get_child_nodes_locs
get_root_node get_root_node_locs get_ancestors get_ancestors_locs get_element_by_id
get_elements_by_class_name get_elements_by_tag_name first_in_tree_order get_attribute get_attribute_locs
by(auto simp add: l_get_scdom_component_get_parent⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def instances)
declare l_get_scdom_component_get_parent⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]
subsubsection ‹get\_root\_node›
locale l_get_scdom_component_get_root_node⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_dom_component_get_scdom_component +
l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_dom_component_get_root_node⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin
lemma get_root_node_is_strongly_scdom_component_safe_step:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ get_scdom_component ptr →⇩r sc"
assumes "h ⊢ get_root_node ptr' →⇩r root"
shows "root ∈ set sc ⟷ ptr' ∈ set sc"
by (meson assms(1) assms(2) assms(3) assms(4) assms(5) contra_subsetD
get_scdom_component_contains_get_dom_component local.get_dom_component_ptr
local.get_root_node_is_strongly_dom_component_safe_step)
lemma get_root_node_is_strongly_scdom_component_safe:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ get_root_node ptr →⇩r root"
assumes "h ⊢ get_root_node ptr →⇩h h'"
shows "is_strongly_scdom_component_safe {ptr} {root} h h'"
proof -
have "h = h'"
using assms(5)
by (meson local.get_root_node_pure pure_returns_heap_eq)
then show ?thesis
using assms
apply(auto simp add: is_strongly_scdom_component_safe_def Let_def preserved_def)[1]
by (smt (verit) Int_iff is_OK_returns_result_I local.get_dom_component_ok
local.get_dom_component_ptr local.get_root_node_is_strongly_dom_component_safe_step
local.get_root_node_ptr_in_heap local.get_scdom_component_impl local.get_scdom_component_ok
local.get_scdom_component_subset_get_dom_component returns_result_select_result subset_eq)
qed
end
interpretation i_get_scdom_component_get_root_node?: l_get_scdom_component_get_root_node⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
get_owner_document heap_is_wellformed parent_child_rel type_wf known_ptr known_ptrs
get_scdom_component is_strongly_scdom_component_safe is_weakly_scdom_component_safe get_dom_component
is_strongly_dom_component_safe is_weakly_dom_component_safe get_disconnected_nodes
get_disconnected_nodes_locs to_tree_order get_parent get_parent_locs get_child_nodes
get_child_nodes_locs get_root_node get_root_node_locs get_ancestors get_ancestors_locs
get_element_by_id get_elements_by_class_name get_elements_by_tag_name first_in_tree_order
get_attribute get_attribute_locs
by(auto simp add: l_get_scdom_component_get_root_node⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def instances)
declare l_get_scdom_component_get_root_node⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]
subsubsection ‹get\_element\_by\_id›
locale l_get_scdom_component_get_element_by_id⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_dom_component_get_scdom_component +
l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_dom_component_get_element_by_id⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin
lemma get_element_by_id_is_strongly_scdom_component_safe_step:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ get_scdom_component ptr →⇩r sc"
assumes "h ⊢ get_element_by_id ptr' idd →⇩r Some result"
shows "cast result ∈ set sc ⟷ ptr' ∈ set sc"
by (meson assms(1) assms(2) assms(3) assms(4) assms(5) contra_subsetD
get_element_by_id_is_strongly_dom_component_safe_step get_scdom_component_contains_get_dom_component
local.get_dom_component_ptr)
lemma get_element_by_id_is_strongly_scdom_component_safe:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ get_element_by_id ptr idd →⇩r Some result"
assumes "h ⊢ get_element_by_id ptr idd →⇩h h'"
shows "is_strongly_scdom_component_safe {ptr} {cast result} h h'"
proof -
have "h = h'"
using assms(5)
by(auto simp add: preserved_def get_element_by_id_def first_in_tree_order_def
elim!: bind_returns_heap_E2 intro!: map_filter_M_pure bind_pure_I
split: option.splits list.splits)
have "ptr |∈| object_ptr_kinds h"
using assms(4)
apply(auto simp add: get_element_by_id_def)[1]
by (metis (no_types, lifting) assms(1) assms(2) assms(3) bind_is_OK_E is_OK_returns_result_I
local.first_in_tree_order_def local.to_tree_order_ptr_in_result local.to_tree_order_ptrs_in_heap)
obtain to where to: "h ⊢ to_tree_order ptr →⇩r to"
by (meson ‹ptr |∈| object_ptr_kinds h› assms(1) assms(2) assms(3) is_OK_returns_result_E
local.to_tree_order_ok)
then have "cast result ∈ set to"
using assms(4) local.get_element_by_id_result_in_tree_order by auto
obtain c where c: "h ⊢ a_get_scdom_component ptr →⇩r c"
using ‹ptr |∈| object_ptr_kinds h› assms(1) assms(2) assms(3) local.get_scdom_component_impl
local.get_scdom_component_ok
by blast
then show ?thesis
using assms ‹h = h'›
apply(auto simp add: is_strongly_scdom_component_safe_def Let_def preserved_def
get_element_by_id_def first_in_tree_order_def elim!: bind_returns_result_E2
intro!: map_filter_M_pure bind_pure_I split: option.splits list.splits)[1]
by (smt (verit) IntI ‹ptr |∈| object_ptr_kinds h› assms(4)
get_element_by_id_is_strongly_scdom_component_safe_step local.get_dom_component_ok
local.get_dom_component_ptr local.get_scdom_component_impl
local.get_scdom_component_subset_get_dom_component returns_result_select_result select_result_I2
subsetD)
qed
end
interpretation i_get_scdom_component_get_element_by_id?: l_get_scdom_component_get_element_by_id⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
get_owner_document heap_is_wellformed parent_child_rel type_wf known_ptr known_ptrs
get_scdom_component is_strongly_scdom_component_safe is_weakly_scdom_component_safe get_dom_component
is_strongly_dom_component_safe is_weakly_dom_component_safe get_disconnected_nodes
get_disconnected_nodes_locs to_tree_order get_parent get_parent_locs get_child_nodes
get_child_nodes_locs get_root_node get_root_node_locs get_ancestors get_ancestors_locs
get_element_by_id get_elements_by_class_name get_elements_by_tag_name first_in_tree_order
get_attribute get_attribute_locs
by(auto simp add: l_get_scdom_component_get_element_by_id⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def instances)
declare l_get_scdom_component_get_element_by_id⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]
subsubsection ‹get\_elements\_by\_class\_name›
locale l_get_scdom_component_get_elements_by_class_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_dom_component_get_scdom_component +
l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_dom_component_get_elements_by_class_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin
lemma get_elements_by_class_name_is_strongly_scdom_component_safe_step:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ get_scdom_component ptr →⇩r sc"
assumes "h ⊢ get_elements_by_class_name ptr' idd →⇩r results"
assumes "result ∈ set results"
shows "cast result ∈ set sc ⟷ ptr' ∈ set sc"
by (meson assms local.get_dom_component_ptr
local.get_elements_by_class_name_is_strongly_dom_component_safe_step
local.get_scdom_component_contains_get_dom_component subsetD)
lemma get_elements_by_class_name_is_strongly_scdom_component_safe:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ get_elements_by_class_name ptr idd →⇩r results"
assumes "h ⊢ get_elements_by_class_name ptr idd →⇩h h'"
shows "is_strongly_scdom_component_safe {ptr} (cast ` set results) h h'"
proof -
have "h = h'"
using assms(5)
by (meson local.get_elements_by_class_name_pure pure_returns_heap_eq)
have "ptr |∈| object_ptr_kinds h"
using assms(4)
apply(auto simp add: get_elements_by_class_name_def)[1]
by (metis (no_types, lifting) assms(1) assms(2) assms(3) bind_is_OK_E is_OK_returns_result_I
local.first_in_tree_order_def local.to_tree_order_ptr_in_result local.to_tree_order_ptrs_in_heap)
obtain to where to: "h ⊢ to_tree_order ptr →⇩r to"
by (meson ‹ptr |∈| object_ptr_kinds h› assms(1) assms(2) assms(3) is_OK_returns_result_E
local.to_tree_order_ok)
then have "cast ` set results ⊆ set to"
using assms(4) local.get_elements_by_class_name_result_in_tree_order by auto
obtain c where c: "h ⊢ a_get_scdom_component ptr →⇩r c"
using ‹ptr |∈| object_ptr_kinds h› assms(1) assms(2) assms(3) local.get_scdom_component_impl
local.get_scdom_component_ok by blast
then show ?thesis
using assms ‹h = h'›
apply(auto simp add: is_strongly_scdom_component_safe_def Let_def preserved_def
get_element_by_id_def first_in_tree_order_def elim!: bind_returns_result_E2 intro!: map_filter_M_pure
bind_pure_I split: option.splits list.splits)[1]
by (smt (verit) IntI ‹ptr |∈| object_ptr_kinds h›
get_elements_by_class_name_is_strongly_scdom_component_safe_step local.get_dom_component_ok
local.get_dom_component_ptr local.get_scdom_component_impl
local.get_scdom_component_subset_get_dom_component returns_result_select_result select_result_I2 subsetD)
qed
end
interpretation i_get_scdom_component_get_elements_by_class_name?: l_get_scdom_component_get_elements_by_class_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
get_owner_document heap_is_wellformed parent_child_rel type_wf known_ptr known_ptrs
get_scdom_component is_strongly_scdom_component_safe is_weakly_scdom_component_safe get_dom_component
is_strongly_dom_component_safe is_weakly_dom_component_safe get_disconnected_nodes
get_disconnected_nodes_locs to_tree_order get_parent get_parent_locs get_child_nodes get_child_nodes_locs
get_root_node get_root_node_locs get_ancestors get_ancestors_locs get_element_by_id
get_elements_by_class_name get_elements_by_tag_name first_in_tree_order get_attribute get_attribute_locs
by(auto simp add: l_get_scdom_component_get_elements_by_class_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def instances)
declare l_get_scdom_component_get_element_by_id⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]
subsubsection ‹get\_elements\_by\_tag\_name›
locale l_get_scdom_component_get_elements_by_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_dom_component_get_scdom_component +
l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_dom_component_get_elements_by_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin
lemma get_elements_by_tag_name_is_strongly_scdom_component_safe_step:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ get_scdom_component ptr →⇩r sc"
assumes "h ⊢ get_elements_by_tag_name ptr' idd →⇩r results"
assumes "result ∈ set results"
shows "cast result ∈ set sc ⟷ ptr' ∈ set sc"
by (meson assms local.get_dom_component_ptr
local.get_elements_by_tag_name_is_strongly_dom_component_safe_step
local.get_scdom_component_contains_get_dom_component subsetD)
lemma get_elements_by_tag_name_is_strongly_scdom_component_safe:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ get_elements_by_tag_name ptr idd →⇩r results"
assumes "h ⊢ get_elements_by_tag_name ptr idd →⇩h h'"
shows "is_strongly_scdom_component_safe {ptr} (cast ` set results) h h'"
proof -
have "h = h'"
using assms(5)
by (meson local.get_elements_by_tag_name_pure pure_returns_heap_eq)
have "ptr |∈| object_ptr_kinds h"
using assms(4)
apply(auto simp add: get_elements_by_tag_name_def)[1]
by (metis (no_types, lifting) assms(1) assms(2) assms(3) bind_is_OK_E is_OK_returns_result_I
local.first_in_tree_order_def local.to_tree_order_ptr_in_result local.to_tree_order_ptrs_in_heap)
obtain to where to: "h ⊢ to_tree_order ptr →⇩r to"
by (meson ‹ptr |∈| object_ptr_kinds h› assms(1) assms(2) assms(3) is_OK_returns_result_E
local.to_tree_order_ok)
then have "cast ` set results ⊆ set to"
using assms(4) local.get_elements_by_tag_name_result_in_tree_order by auto
obtain c where c: "h ⊢ a_get_scdom_component ptr →⇩r c"
using ‹ptr |∈| object_ptr_kinds h› assms(1) assms(2) assms(3) local.get_scdom_component_impl
local.get_scdom_component_ok by blast
then show ?thesis
using assms ‹h = h'›
apply(auto simp add: is_strongly_scdom_component_safe_def Let_def preserved_def
get_element_by_id_def first_in_tree_order_def elim!: bind_returns_result_E2 intro!:
map_filter_M_pure bind_pure_I split: option.splits list.splits)[1]
by (smt (verit) IntI ‹ptr |∈| object_ptr_kinds h›
get_elements_by_tag_name_is_strongly_scdom_component_safe_step local.get_dom_component_ok
local.get_dom_component_ptr local.get_scdom_component_impl
local.get_scdom_component_subset_get_dom_component returns_result_select_result select_result_I2
subsetD)
qed
end
interpretation i_get_scdom_component_get_elements_by_tag_name?:
l_get_scdom_component_get_elements_by_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
get_owner_document heap_is_wellformed parent_child_rel type_wf known_ptr known_ptrs
get_scdom_component is_strongly_scdom_component_safe is_weakly_scdom_component_safe
get_dom_component is_strongly_dom_component_safe is_weakly_dom_component_safe
get_disconnected_nodes get_disconnected_nodes_locs to_tree_order get_parent get_parent_locs
get_child_nodes get_child_nodes_locs get_root_node get_root_node_locs get_ancestors
get_ancestors_locs get_element_by_id get_elements_by_class_name get_elements_by_tag_name
first_in_tree_order get_attribute get_attribute_locs
by(auto simp add: l_get_scdom_component_get_elements_by_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def instances)
declare l_get_scdom_component_get_element_by_id⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]
subsubsection ‹remove\_child›
locale l_get_scdom_component_remove_child⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_dom_component_get_scdom_component +
l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_remove_child⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_set_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_set_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_owner_document_wf +
l_remove_child_wf2⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M get_child_nodes get_child_nodes_locs set_child_nodes set_child_nodes_locs
get_parent get_parent_locs get_owner_document get_disconnected_nodes get_disconnected_nodes_locs
set_disconnected_nodes set_disconnected_nodes_locs remove_child remove_child_locs remove type_wf
known_ptr known_ptrs heap_is_wellformed parent_child_rel
begin
lemma remove_child_is_component_unsafe:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ remove_child ptr' child →⇩h h'"
assumes "ptr ∉ set |h ⊢ get_dom_component ptr'|⇩r"
assumes "ptr ∉ set |h ⊢ get_dom_component (cast |h ⊢ get_owner_document (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r child)|⇩r)|⇩r"
shows "preserved (get_M ptr getter) h h'"
proof -
have "ptr ≠ ptr'"
using assms(5)
by (metis (no_types, lifting) assms(1) assms(2) assms(3) assms(4) is_OK_returns_heap_I
is_OK_returns_result_E local.get_dom_component_ok local.get_dom_component_ptr
local.remove_child_ptr_in_heap select_result_I2)
obtain owner_document where owner_document: "h ⊢ get_owner_document (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r child) →⇩r owner_document"
by (meson assms(1) assms(2) assms(3) assms(4) is_OK_returns_result_E local.get_owner_document_ok
local.remove_child_child_in_heap node_ptr_kinds_commutes)
then
obtain c where "h ⊢ get_dom_component (cast owner_document) →⇩r c"
using get_dom_component_ok owner_document assms(1) assms(2) assms(3)
by (meson document_ptr_kinds_commutes get_owner_document_owner_document_in_heap select_result_I)
then
have "ptr ≠ cast owner_document"
using assms(6) assms(1) assms(2) assms(3) local.get_dom_component_ptr owner_document
by auto
show ?thesis
using remove_child_writes assms(4)
apply(rule reads_writes_preserved2)
apply(auto simp add: remove_child_locs_def set_child_nodes_locs_def
set_disconnected_nodes_locs_def all_args_def split: option.splits)[1]
apply (metis ‹ptr ≠ ptr'› document_ptr_casts_commute3 get_M_Mdocument_preserved3)
apply (metis (no_types, lifting) ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r owner_document›
get_M_Mdocument_preserved3 owner_document select_result_I2)
apply (metis (no_types, lifting) ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r owner_document›
get_M_Mdocument_preserved3 owner_document select_result_I2)
apply (metis ‹ptr ≠ ptr'› element_ptr_casts_commute3 get_M_Element_preserved8)
apply (metis (no_types, lifting) ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r owner_document›
get_M_Mdocument_preserved3 owner_document select_result_I2)
apply (metis (no_types, lifting) ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r owner_document›
get_M_Mdocument_preserved3 owner_document select_result_I2)
done
qed
lemma remove_child_is_strongly_dom_component_safe_step:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ remove_child ptr' child →⇩h h'"
assumes "ptr ∉ set |h ⊢ get_scdom_component ptr'|⇩r"
assumes "ptr ∉ set |h ⊢ get_scdom_component (cast child)|⇩r"
shows "preserved (get_M ptr getter) h h'"
proof -
obtain sc where sc: "h ⊢ get_scdom_component ptr' →⇩r sc"
using get_scdom_component_ok
by (meson assms(1) assms(2) assms(3) assms(4) is_OK_returns_heap_I local.remove_child_ptr_in_heap
returns_result_select_result)
have "child |∈| node_ptr_kinds h"
using assms(4) remove_child_child_in_heap by blast
then
obtain child_sc where child_sc: "h ⊢ get_scdom_component (cast child) →⇩r child_sc"
using get_scdom_component_ok
by (meson assms(1) assms(2) assms(3) node_ptr_kinds_commutes select_result_I)
then obtain owner_document where owner_document: "h ⊢ get_owner_document (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r child) →⇩r owner_document"
by (meson ‹child |∈| node_ptr_kinds h› assms(1) assms(2) assms(3) contra_subsetD
get_scdom_component_owner_document_same is_OK_returns_result_E
get_scdom_component_subset_get_dom_component local.get_dom_component_ok local.get_dom_component_ptr
node_ptr_kinds_commutes)
then have "h ⊢ get_scdom_component (cast owner_document) →⇩r child_sc"
using child_sc
by (smt (verit) ‹child |∈| node_ptr_kinds h› assms(1) assms(2) assms(3) contra_subsetD
get_scdom_component_subset_get_dom_component get_scdom_component_owner_document_same
get_scdom_component_ptrs_same_scope_component local.get_dom_component_ok local.get_dom_component_ptr
node_ptr_kinds_commutes returns_result_select_result select_result_I2)
have "ptr ∉ set |h ⊢ get_dom_component ptr'|⇩r"
by (metis (no_types, lifting) assms(1) assms(2) assms(3) assms(4) assms(5) contra_subsetD
get_scdom_component_subset_get_dom_component is_OK_returns_heap_I local.get_dom_component_ok
local.remove_child_ptr_in_heap returns_result_select_result sc select_result_I2)
moreover have "ptr ∉ set |h ⊢ get_scdom_component (cast |h ⊢ get_owner_document (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r child)|⇩r)|⇩r"
using get_scdom_component_owner_document_same get_scdom_component_ptrs_same_scope_component
by (metis (no_types, lifting)
‹h ⊢ get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r owner_document) →⇩r child_sc› assms(6) child_sc
owner_document select_result_I2)
have "ptr ∉ set |h ⊢ get_dom_component (cast |h ⊢ get_owner_document (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r child)|⇩r)|⇩r"
using get_scdom_component_owner_document_same
by (metis (no_types, lifting)
‹h ⊢ get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r owner_document) →⇩r child_sc›
‹ptr ∉ set |h ⊢ get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r |h ⊢ get_owner_document (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r child)|⇩r)|⇩r›
assms(1) assms(2) assms(3) contra_subsetD document_ptr_kinds_commutes get_scdom_component_subset_get_dom_component
is_OK_returns_result_E local.get_dom_component_ok local.get_owner_document_owner_document_in_heap owner_document
select_result_I2)
ultimately show ?thesis
using assms(1) assms(2) assms(3) assms(4) remove_child_is_component_unsafe by blast
qed
lemma remove_child_is_strongly_dom_component_safe:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ remove_child ptr child →⇩h h'"
shows "is_strongly_scdom_component_safe {ptr, cast child} {} h h'"
proof -
obtain owner_document children_h h2 disconnected_nodes_h where
owner_document: "h ⊢ get_owner_document (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r child) →⇩r owner_document" and
children_h: "h ⊢ get_child_nodes ptr →⇩r children_h" and
child_in_children_h: "child ∈ set children_h" and
disconnected_nodes_h: "h ⊢ get_disconnected_nodes owner_document →⇩r disconnected_nodes_h" and
h2: "h ⊢ set_disconnected_nodes owner_document (child # disconnected_nodes_h) →⇩h h2" and
h': "h2 ⊢ set_child_nodes ptr (remove1 child children_h) →⇩h h'"
using assms(4)
apply(auto simp add: remove_child_def elim!: bind_returns_heap_E
dest!: pure_returns_heap_eq[rotated, OF get_owner_document_pure]
pure_returns_heap_eq[rotated, OF get_child_nodes_pure] split: if_splits)[1]
using pure_returns_heap_eq by fastforce
have object_ptr_kinds_eq3: "object_ptr_kinds h = object_ptr_kinds h'"
apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h = object_ptr_kinds h'",
OF remove_child_writes assms(4)])
unfolding remove_child_locs_def
using set_disconnected_nodes_pointers_preserved set_child_nodes_pointers_preserved
by (auto simp add: reflp_def transp_def)
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'"
using node_ptr_kinds_M_eq 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'"
using document_ptr_kinds_M_eq by auto
have children_eq:
"⋀ptr' children. ptr ≠ ptr' ⟹ h ⊢ get_child_nodes ptr' →⇩r children = h' ⊢ get_child_nodes ptr' →⇩r children"
apply(rule reads_writes_preserved[OF get_child_nodes_reads remove_child_writes assms(4)])
unfolding remove_child_locs_def
using set_disconnected_nodes_get_child_nodes set_child_nodes_get_child_nodes_different_pointers
by fast
then have children_eq2:
"⋀ptr' children. ptr ≠ 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. document_ptr ≠ owner_document
⟹ 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 remove_child_writes assms(4)])
unfolding remove_child_locs_def
using set_child_nodes_get_disconnected_nodes set_disconnected_nodes_get_disconnected_nodes_different_pointers
by (metis (no_types, lifting) Un_iff owner_document select_result_I2)
then have disconnected_nodes_eq2:
"⋀document_ptr. document_ptr ≠ owner_document
⟹ |h ⊢ get_disconnected_nodes document_ptr|⇩r = |h' ⊢ get_disconnected_nodes document_ptr|⇩r"
using select_result_eq by force
have "h2 ⊢ get_child_nodes ptr →⇩r children_h"
apply(rule reads_writes_separate_forwards[OF get_child_nodes_reads set_disconnected_nodes_writes h2 children_h] )
by (simp add: set_disconnected_nodes_get_child_nodes)
have "known_ptrs h'"
using object_ptr_kinds_eq3 known_ptrs_preserved ‹known_ptrs h› by blast
have "known_ptr ptr"
using assms(3)
using children_h get_child_nodes_ptr_in_heap local.known_ptrs_known_ptr by blast
have "type_wf h2"
using writes_small_big[where P="λh h'. type_wf h ⟶ type_wf h'", OF set_disconnected_nodes_writes h2]
using set_disconnected_nodes_types_preserved assms(2)
by(auto simp add: reflp_def transp_def)
then have "type_wf h'"
using writes_small_big[where P="λh h'. type_wf h ⟶ type_wf h'", OF set_child_nodes_writes h']
using set_child_nodes_types_preserved
by(auto simp add: reflp_def transp_def)
have children_h': "h' ⊢ get_child_nodes ptr →⇩r remove1 child children_h"
using assms(4) owner_document h2 disconnected_nodes_h children_h
apply(auto simp add: remove_child_def split: if_splits)[1]
apply(drule bind_returns_heap_E3)
apply(auto split: if_splits)[1]
apply(simp)
apply(auto split: if_splits)[1]
apply(drule bind_returns_heap_E3)
apply(auto)[1]
apply(simp)
apply(drule bind_returns_heap_E3)
apply(auto)[1]
apply(simp)
apply(drule bind_returns_heap_E4)
apply(auto)[1]
apply simp
using ‹type_wf h2› set_child_nodes_get_child_nodes ‹known_ptr ptr› h'
by blast
have disconnected_nodes_h2: "h2 ⊢ get_disconnected_nodes owner_document →⇩r child # disconnected_nodes_h"
using owner_document assms(4) h2 disconnected_nodes_h
apply (auto simp add: remove_child_def split: if_splits)[1]
apply(drule bind_returns_heap_E2)
apply(auto split: if_splits)[1]
apply(simp)
by(auto simp add: local.set_disconnected_nodes_get_disconnected_nodes split: if_splits)
then have disconnected_nodes_h': "h' ⊢ get_disconnected_nodes owner_document →⇩r child # disconnected_nodes_h"
apply(rule reads_writes_separate_forwards[OF get_disconnected_nodes_reads set_child_nodes_writes h'])
by (simp add: set_child_nodes_get_disconnected_nodes)
moreover have "a_acyclic_heap h"
using assms(1) by (simp add: heap_is_wellformed_def)
have "parent_child_rel h' ⊆ parent_child_rel h"
proof (standard, safe)
fix parent child
assume a1: "(parent, child) ∈ parent_child_rel h'"
then show "(parent, child) ∈ parent_child_rel h"
proof (cases "parent = ptr")
case True
then show ?thesis
using a1 remove_child_removes_parent[OF assms(1) assms(4)] children_h children_h'
get_child_nodes_ptr_in_heap
apply(auto simp add: parent_child_rel_def object_ptr_kinds_eq )[1]
by (metis imageI notin_set_remove1)
next
case False
then show ?thesis
using a1
by(auto simp add: parent_child_rel_def object_ptr_kinds_eq3 children_eq2)
qed
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 assms(1) by (simp add: heap_is_wellformed_def)
then have "a_all_ptrs_in_heap h'"
apply(auto simp add: a_all_ptrs_in_heap_def node_ptr_kinds_eq3 disconnected_nodes_eq)[1]
apply (metis (no_types, lifting) ‹type_wf h'› assms local.get_child_nodes_ok local.known_ptrs_known_ptr
local.remove_child_children_subset object_ptr_kinds_eq3 returns_result_select_result subset_code(1))
apply (metis (no_types, lifting) assms(4) disconnected_nodes_eq2 disconnected_nodes_h disconnected_nodes_h'
document_ptr_kinds_eq3 local.remove_child_child_in_heap node_ptr_kinds_eq3 select_result_I2
set_ConsD subset_code(1))
done
moreover have "a_owner_document_valid h"
using assms(1) by (simp add: heap_is_wellformed_def)
then have "a_owner_document_valid h'"
apply(auto simp add: a_owner_document_valid_def object_ptr_kinds_eq3 document_ptr_kinds_eq3
node_ptr_kinds_eq3)[1]
proof -
fix node_ptr
assume 0: "∀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)"
and 1: "node_ptr |∈| node_ptr_kinds h'"
and 2: "∀parent_ptr. parent_ptr |∈| object_ptr_kinds h' ⟶ node_ptr ∉ set |h' ⊢ get_child_nodes parent_ptr|⇩r"
then show "∃document_ptr. document_ptr |∈| document_ptr_kinds h'
∧ node_ptr ∈ set |h' ⊢ get_disconnected_nodes document_ptr|⇩r"
proof (cases "node_ptr = child")
case True
show ?thesis
apply(rule exI[where x=owner_document])
using children_eq2 disconnected_nodes_eq2 children_h children_h' disconnected_nodes_h' True
by (metis (no_types, lifting) get_disconnected_nodes_ptr_in_heap is_OK_returns_result_I
list.set_intros(1) select_result_I2)
next
case False
then show ?thesis
using 0 1 2 children_eq2 children_h children_h' disconnected_nodes_eq2 disconnected_nodes_h
disconnected_nodes_h'
apply(auto simp add: children_eq2 disconnected_nodes_eq2 dest!: select_result_I2)[1]
by (metis children_eq2 disconnected_nodes_eq2 in_set_remove1 list.set_intros(2))
qed
qed
moreover
{
have h0: "a_distinct_lists h"
using assms(1) by (simp add: heap_is_wellformed_def)
moreover have ha1: "(⋃x∈set |h ⊢ object_ptr_kinds_M|⇩r. set |h ⊢ get_child_nodes x|⇩r)
∩ (⋃x∈set |h ⊢ document_ptr_kinds_M|⇩r. set |h ⊢ get_disconnected_nodes x|⇩r) = {}"
using ‹a_distinct_lists h›
unfolding a_distinct_lists_def
by(auto)
have ha2: "ptr |∈| object_ptr_kinds h"
using children_h get_child_nodes_ptr_in_heap by blast
have ha3: "child ∈ set |h ⊢ get_child_nodes ptr|⇩r"
using child_in_children_h children_h
by(simp)
have child_not_in: "⋀document_ptr. document_ptr |∈| document_ptr_kinds h
⟹ child ∉ set |h ⊢ get_disconnected_nodes document_ptr|⇩r"
using ha1 ha2 ha3
apply(simp)
using IntI by fastforce
moreover have "distinct |h ⊢ object_ptr_kinds_M|⇩r"
apply(rule select_result_I)
by(auto simp add: object_ptr_kinds_M_defs)
moreover have "distinct |h ⊢ document_ptr_kinds_M|⇩r"
apply(rule select_result_I)
by(auto simp add: document_ptr_kinds_M_defs)
ultimately have "a_distinct_lists h'"
proof(simp (no_asm) add: a_distinct_lists_def, safe)
assume 1: "a_distinct_lists h"
and 3: "distinct |h ⊢ object_ptr_kinds_M|⇩r"
assume 1: "a_distinct_lists h"
and 3: "distinct |h ⊢ object_ptr_kinds_M|⇩r"
have 4: "distinct (concat ((map (λptr. |h ⊢ get_child_nodes ptr|⇩r) |h ⊢ object_ptr_kinds_M|⇩r)))"
using 1 by(auto simp add: a_distinct_lists_def)
show "distinct (concat (map (λptr. |h' ⊢ get_child_nodes ptr|⇩r)
(sorted_list_of_set (fset (object_ptr_kinds h')))))"
proof(rule distinct_concat_map_I[OF 3[unfolded object_ptr_kinds_eq2], simplified])
fix x
assume 5: "x |∈| object_ptr_kinds h'"
then have 6: "distinct |h ⊢ get_child_nodes x|⇩r"
using 4 distinct_concat_map_E object_ptr_kinds_eq2 by fastforce
obtain children where children: "h ⊢ get_child_nodes x →⇩r children"
and distinct_children: "distinct children"
by (metis "5" "6" assms get_child_nodes_ok local.known_ptrs_known_ptr
object_ptr_kinds_eq3 select_result_I)
obtain children' where children': "h' ⊢ get_child_nodes x →⇩r children'"
using children children_eq children_h' by fastforce
then have "distinct children'"
proof (cases "ptr = x")
case True
then show ?thesis
using children distinct_children children_h children_h'
by (metis children' distinct_remove1 returns_result_eq)
next
case False
then show ?thesis
using children distinct_children children_eq[OF False]
using children' distinct_lists_children h0
using select_result_I2 by fastforce
qed
then show "distinct |h' ⊢ get_child_nodes x|⇩r"
using children' by(auto simp add: )
next
fix x y
assume 5: "x |∈| object_ptr_kinds h'" and 6: "y |∈| object_ptr_kinds h'" and 7: "x ≠ y"
obtain children_x where children_x: "h ⊢ get_child_nodes x →⇩r children_x"
by (metis "5" assms get_child_nodes_ok is_OK_returns_result_E
local.known_ptrs_known_ptr object_ptr_kinds_eq3)
obtain children_y where children_y: "h ⊢ get_child_nodes y →⇩r children_y"
by (metis "6" assms get_child_nodes_ok is_OK_returns_result_E
local.known_ptrs_known_ptr object_ptr_kinds_eq3)
obtain children_x' where children_x': "h' ⊢ get_child_nodes x →⇩r children_x'"
using children_eq children_h' children_x by fastforce
obtain children_y' where children_y': "h' ⊢ get_child_nodes y →⇩r children_y'"
using children_eq children_h' children_y by fastforce
have "distinct (concat (map (λptr. |h ⊢ get_child_nodes ptr|⇩r) |h ⊢ object_ptr_kinds_M|⇩r))"
using h0 by(auto simp add: a_distinct_lists_def)
then have 8: "set children_x ∩ set children_y = {}"
using "7" assms(1) children_x children_y local.heap_is_wellformed_one_parent by blast
have "set children_x' ∩ set children_y' = {}"
proof (cases "ptr = x")
case True
then have "ptr ≠ y"
by(simp add: 7)
have "children_x' = remove1 child children_x"
using children_h children_h' children_x children_x' True returns_result_eq by fastforce
moreover have "children_y' = children_y"
using children_y children_y' children_eq[OF ‹ptr ≠ y›] by auto
ultimately show ?thesis
using 8 set_remove1_subset by fastforce
next
case False
then show ?thesis
proof (cases "ptr = y")
case True
have "children_y' = remove1 child children_y"
using children_h children_h' children_y children_y' True returns_result_eq by fastforce
moreover have "children_x' = children_x"
using children_x children_x' children_eq[OF ‹ptr ≠ x›] by auto
ultimately show ?thesis
using 8 set_remove1_subset by fastforce
next
case False
have "children_x' = children_x"
using children_x children_x' children_eq[OF ‹ptr ≠ x›] by auto
moreover have "children_y' = children_y"
using children_y children_y' children_eq[OF ‹ptr ≠ y›] by auto
ultimately show ?thesis
using 8 by simp
qed
qed
then show "set |h' ⊢ get_child_nodes x|⇩r ∩ set |h' ⊢ get_child_nodes y|⇩r = {}"
using children_x' children_y'
by (metis (no_types, lifting) select_result_I2)
qed
next
assume 2: "distinct |h ⊢ document_ptr_kinds_M|⇩r"
then have 4: "distinct (sorted_list_of_set (fset (document_ptr_kinds h')))"
by simp
have 3: "distinct (concat (map (λdocument_ptr. |h ⊢ get_disconnected_nodes document_ptr|⇩r)
(sorted_list_of_set (fset (document_ptr_kinds h')))))"
using h0
by(simp add: a_distinct_lists_def document_ptr_kinds_eq3)
show "distinct (concat (map (λdocument_ptr. |h' ⊢ get_disconnected_nodes document_ptr|⇩r)
(sorted_list_of_set (fset (document_ptr_kinds h')))))"
proof(rule distinct_concat_map_I[OF 4[unfolded document_ptr_kinds_eq3]])
fix x
assume 4: "x ∈ set (sorted_list_of_set (fset (document_ptr_kinds h')))"
have 5: "distinct |h ⊢ get_disconnected_nodes x|⇩r"
using distinct_lists_disconnected_nodes[OF h0] 4 get_disconnected_nodes_ok
by (simp add: assms document_ptr_kinds_eq3 select_result_I)
show "distinct |h' ⊢ get_disconnected_nodes x|⇩r"
proof (cases "x = owner_document")
case True
have "child ∉ set |h ⊢ get_disconnected_nodes x|⇩r"
using child_not_in document_ptr_kinds_eq2 "4" by fastforce
moreover have "|h' ⊢ get_disconnected_nodes x|⇩r = child # |h ⊢ get_disconnected_nodes x|⇩r"
using disconnected_nodes_h' disconnected_nodes_h unfolding True
by(simp)
ultimately show ?thesis
using 5 unfolding True
by simp
next
case False
show ?thesis
using "5" False disconnected_nodes_eq2 by auto
qed
next
fix x y
assume 4: "x ∈ set (sorted_list_of_set (fset (document_ptr_kinds h')))"
and 5: "y ∈ set (sorted_list_of_set (fset (document_ptr_kinds h')))" and "x ≠ y"
obtain disc_nodes_x where disc_nodes_x: "h ⊢ get_disconnected_nodes x →⇩r disc_nodes_x"
using 4 get_disconnected_nodes_ok[OF ‹type_wf h›, of x] document_ptr_kinds_eq2
by auto
obtain disc_nodes_y where disc_nodes_y: "h ⊢ get_disconnected_nodes y →⇩r disc_nodes_y"
using 5 get_disconnected_nodes_ok[OF ‹type_wf h›, of y] document_ptr_kinds_eq2
by auto
obtain disc_nodes_x' where disc_nodes_x': "h' ⊢ get_disconnected_nodes x →⇩r disc_nodes_x'"
using 4 get_disconnected_nodes_ok[OF ‹type_wf h'›, of x] document_ptr_kinds_eq2
by auto
obtain disc_nodes_y' where disc_nodes_y': "h' ⊢ get_disconnected_nodes y →⇩r disc_nodes_y'"
using 5 get_disconnected_nodes_ok[OF ‹type_wf h'›, of y] document_ptr_kinds_eq2
by auto
have "distinct
(concat (map (λdocument_ptr. |h ⊢ get_disconnected_nodes document_ptr|⇩r) |h ⊢ document_ptr_kinds_M|⇩r))"
using h0 by (simp add: a_distinct_lists_def)
then have 6: "set disc_nodes_x ∩ set disc_nodes_y = {}"
using ‹x ≠ y› assms(1) disc_nodes_x disc_nodes_y local.heap_is_wellformed_one_disc_parent
by blast
have "set disc_nodes_x' ∩ set disc_nodes_y' = {}"
proof (cases "x = owner_document")
case True
then have "y ≠ owner_document"
using ‹x ≠ y› by simp
then have "disc_nodes_y' = disc_nodes_y"
using disconnected_nodes_eq[OF ‹y ≠ owner_document›] disc_nodes_y disc_nodes_y'
by auto
have "disc_nodes_x' = child # disc_nodes_x"
using disconnected_nodes_h' disc_nodes_x disc_nodes_x' True disconnected_nodes_h returns_result_eq
by fastforce
have "child ∉ set disc_nodes_y"
using child_not_in disc_nodes_y 5
using document_ptr_kinds_eq2 by fastforce
then show ?thesis
apply(unfold ‹disc_nodes_x' = child # disc_nodes_x› ‹disc_nodes_y' = disc_nodes_y›)
using 6 by auto
next
case False
then show ?thesis
proof (cases "y = owner_document")
case True
then have "disc_nodes_x' = disc_nodes_x"
using disconnected_nodes_eq[OF ‹x ≠ owner_document›] disc_nodes_x disc_nodes_x' by auto
have "disc_nodes_y' = child # disc_nodes_y"
using disconnected_nodes_h' disc_nodes_y disc_nodes_y' True disconnected_nodes_h returns_result_eq
by fastforce
have "child ∉ set disc_nodes_x"
using child_not_in disc_nodes_x 4
using document_ptr_kinds_eq2 by fastforce
then show ?thesis
apply(unfold ‹disc_nodes_y' = child # disc_nodes_y› ‹disc_nodes_x' = disc_nodes_x›)
using 6 by auto
next
case False
have "disc_nodes_x' = disc_nodes_x"
using disconnected_nodes_eq[OF ‹x ≠ owner_document›] disc_nodes_x disc_nodes_x' by auto
have "disc_nodes_y' = disc_nodes_y"
using disconnected_nodes_eq[OF ‹y ≠ owner_document›] disc_nodes_y disc_nodes_y' by auto
then show ?thesis
apply(unfold ‹disc_nodes_y' = disc_nodes_y› ‹disc_nodes_x' = disc_nodes_x›)
using 6 by auto
qed
qed
then show "set |h' ⊢ get_disconnected_nodes x|⇩r ∩ set |h' ⊢ get_disconnected_nodes y|⇩r = {}"
using disc_nodes_x' disc_nodes_y' by auto
qed
next
fix x xa xb
assume 1: "xa ∈ fset (object_ptr_kinds h')"
and 2: "x ∈ set |h' ⊢ get_child_nodes xa|⇩r"
and 3: "xb ∈ fset (document_ptr_kinds h')"
and 4: "x ∈ set |h' ⊢ get_disconnected_nodes xb|⇩r"
obtain disc_nodes where disc_nodes: "h ⊢ get_disconnected_nodes xb →⇩r disc_nodes"
using 3 get_disconnected_nodes_ok[OF ‹type_wf h›, of xb] document_ptr_kinds_eq2 by auto
obtain disc_nodes' where disc_nodes': "h' ⊢ get_disconnected_nodes xb →⇩r disc_nodes'"
using 3 get_disconnected_nodes_ok[OF ‹type_wf h'›, of xb] document_ptr_kinds_eq2 by auto
obtain children where children: "h ⊢ get_child_nodes xa →⇩r children"
by (metis "1" assms get_child_nodes_ok is_OK_returns_result_E
local.known_ptrs_known_ptr object_ptr_kinds_eq3)
obtain children' where children': "h' ⊢ get_child_nodes xa →⇩r children'"
using children children_eq children_h' by fastforce
have "⋀x. x ∈ set |h ⊢ get_child_nodes xa|⇩r ⟹ x ∈ set |h ⊢ get_disconnected_nodes xb|⇩r ⟹ False"
using 1 3
apply(fold ‹ object_ptr_kinds h = object_ptr_kinds h'›)
apply(fold ‹ document_ptr_kinds h = document_ptr_kinds h'›)
using children disc_nodes h0 apply(auto simp add: a_distinct_lists_def)[1]
by (metis (no_types, lifting) h0 local.distinct_lists_no_parent select_result_I2)
then have 5: "⋀x. x ∈ set children ⟹ x ∈ set disc_nodes ⟹ False"
using children disc_nodes by fastforce
have 6: "|h' ⊢ get_child_nodes xa|⇩r = children'"
using children' by simp
have 7: "|h' ⊢ get_disconnected_nodes xb|⇩r = disc_nodes'"
using disc_nodes' by simp
have "False"
proof (cases "xa = ptr")
case True
have "distinct children_h"
using children_h distinct_lists_children h0 ‹known_ptr ptr› by blast
have "|h' ⊢ get_child_nodes ptr|⇩r = remove1 child children_h"
using children_h'
by simp
have "children = children_h"
using True children children_h by auto
show ?thesis
using disc_nodes' children' 5 2 4 children_h ‹distinct children_h› disconnected_nodes_h'
apply(auto simp add: 6 7
‹xa = ptr› ‹|h' ⊢ get_child_nodes ptr|⇩r = remove1 child children_h› ‹children = children_h›)[1]
by (metis (no_types, lifting) disc_nodes disconnected_nodes_eq2 disconnected_nodes_h
select_result_I2 set_ConsD)
next
case False
have "children' = children"
using children' children children_eq[OF False[symmetric]]
by auto
then show ?thesis
proof (cases "xb = owner_document")
case True
then show ?thesis
using disc_nodes disconnected_nodes_h disconnected_nodes_h'
using "2" "4" "5" "6" "7" False ‹children' = children› assms(1) child_in_children_h
child_parent_dual children children_h disc_nodes' get_child_nodes_ptr_in_heap
list.set_cases list.simps(3) option.simps(1) returns_result_eq set_ConsD
by (metis (no_types, opaque_lifting) assms)
next
case False
then show ?thesis
using "2" "4" "5" "6" "7" ‹children' = children› disc_nodes disc_nodes'
disconnected_nodes_eq returns_result_eq
by metis
qed
qed
then show "x ∈ {}"
by simp
qed
}
ultimately have "heap_is_wellformed h'"
using heap_is_wellformed_def by blast
show ?thesis
apply(auto simp add: is_strongly_scdom_component_safe_def Let_def object_ptr_kinds_eq3)[1]
using assms(1) assms(2) assms(3) assms(4) local.get_scdom_component_impl
remove_child_is_strongly_dom_component_safe_step
by blast
qed
end
interpretation i_get_scdom_component_remove_child?: l_get_scdom_component_remove_child⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
get_owner_document heap_is_wellformed parent_child_rel type_wf known_ptr known_ptrs
get_scdom_component is_strongly_scdom_component_safe is_weakly_scdom_component_safe get_dom_component
is_strongly_dom_component_safe is_weakly_dom_component_safe to_tree_order get_parent
get_parent_locs get_child_nodes get_child_nodes_locs get_root_node get_root_node_locs get_ancestors
get_ancestors_locs get_disconnected_nodes get_disconnected_nodes_locs get_element_by_id
get_elements_by_class_name get_elements_by_tag_name set_child_nodes set_child_nodes_locs
set_disconnected_nodes set_disconnected_nodes_locs remove_child remove_child_locs remove
by(auto simp add: l_get_scdom_component_remove_child⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def instances)
declare l_get_scdom_component_remove_child⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]
subsubsection ‹adopt\_node›
locale l_get_scdom_component_adopt_node⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_dom_component_get_scdom_component +
l_adopt_node⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_remove_child⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_set_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_set_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_adopt_node_wf +
l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_owner_document_wf +
l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_adopt_node_wf⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_heap_is_wellformed⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin
lemma adopt_node_is_component_unsafe:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ adopt_node document_ptr node_ptr →⇩h h'"
assumes "ptr ∉ set |h ⊢ get_dom_component (cast document_ptr)|⇩r"
assumes "ptr ∉ set |h ⊢ get_dom_component (cast node_ptr)|⇩r"
assumes "ptr ∉ set |h ⊢ get_dom_component (cast |h ⊢ get_owner_document (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r node_ptr)|⇩r)|⇩r"
shows "preserved (get_M ptr getter) h h'"
proof -
obtain owner_document where owner_document: "h ⊢ get_owner_document (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r node_ptr) →⇩r owner_document"
using assms(4) local.adopt_node_def by auto
then
obtain c where "h ⊢ get_dom_component (cast owner_document) →⇩r c"
using get_dom_component_ok assms(1) assms(2) assms(3) get_owner_document_owner_document_in_heap
by (meson document_ptr_kinds_commutes select_result_I)
then
have "ptr ≠ cast owner_document"
using assms(6) assms(1) assms(2) assms(3) local.get_dom_component_ptr owner_document
by (metis (no_types, lifting) assms(7) select_result_I2)
have "document_ptr |∈| document_ptr_kinds h"
using adopt_node_document_in_heap assms(1) assms(2) assms(3) assms(4) by auto
then
have "ptr ≠ cast document_ptr"
using assms(5)
using assms(1) assms(2) assms(3) local.get_dom_component_ptr get_dom_component_ok
by (meson document_ptr_kinds_commutes returns_result_select_result)
have "⋀parent. |h ⊢ get_parent node_ptr|⇩r = Some parent ⟹ parent ≠ ptr"
by (metis assms(1) assms(2) assms(3) assms(6) is_OK_returns_result_I local.get_dom_component_ok
local.get_dom_component_parent_inside local.get_dom_component_ptr local.get_owner_document_ptr_in_heap
local.get_parent_ok node_ptr_kinds_commutes owner_document returns_result_select_result)
show ?thesis
using adopt_node_writes assms(4)
apply(rule reads_writes_preserved2)
apply(auto simp add: adopt_node_locs_def remove_child_locs_def set_child_nodes_locs_def set_disconnected_nodes_locs_def all_args_def)[1]
apply (metis ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr› get_M_Mdocument_preserved3)
apply (metis (no_types, lifting) ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r owner_document› get_M_Mdocument_preserved3 owner_document select_result_I2)
apply(drule ‹⋀parent. |h ⊢ get_parent node_ptr|⇩r = Some parent ⟹ parent ≠ ptr›)[1] apply (metis element_ptr_casts_commute3 get_M_Element_preserved8 is_node_ptr_kind_none node_ptr_casts_commute3 option.case_eq_if)
apply (metis (no_types, lifting) ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r owner_document› get_M_Mdocument_preserved3 owner_document select_result_I2)
apply (metis ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr› get_M_Mdocument_preserved3)
apply (metis (no_types, lifting) ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r owner_document› get_M_Mdocument_preserved3 owner_document select_result_I2)
apply (metis ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr› get_M_Mdocument_preserved3)
apply (metis (no_types, lifting) ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r owner_document› get_M_Mdocument_preserved3 owner_document select_result_I2)
apply(drule ‹⋀parent. |h ⊢ get_parent node_ptr|⇩r = Some parent ⟹ parent ≠ ptr›)[1] apply (metis document_ptr_casts_commute3 get_M_Mdocument_preserved3)
apply (metis (no_types, lifting) ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r owner_document› get_M_Mdocument_preserved3 owner_document select_result_I2)
apply (metis ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr› get_M_Mdocument_preserved3)
apply (metis (no_types, lifting) ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r owner_document› get_M_Mdocument_preserved3 owner_document select_result_I2)
apply (metis ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr› get_M_Mdocument_preserved3)
apply (metis (no_types, lifting) ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r owner_document› get_M_Mdocument_preserved3 owner_document select_result_I2)
apply(drule ‹⋀parent. |h ⊢ get_parent node_ptr|⇩r = Some parent ⟹ parent ≠ ptr›)[1]
apply (metis (no_types, lifting) ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r owner_document› get_M_Mdocument_preserved3 owner_document select_result_I2)
apply (metis ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr› get_M_Mdocument_preserved3)
apply (metis (no_types, lifting) ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r owner_document› get_M_Mdocument_preserved3 owner_document select_result_I2)
done
qed
lemma adopt_node_is_strongly_dom_component_safe_step:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ adopt_node document_ptr node_ptr →⇩h h'"
assumes "ptr ∉ set |h ⊢ get_scdom_component (cast document_ptr)|⇩r"
assumes "ptr ∉ set |h ⊢ get_scdom_component (cast node_ptr)|⇩r"
shows "preserved (get_M ptr getter) h h'"
proof -
have "document_ptr |∈| document_ptr_kinds h"
by (meson assms(1) assms(2) assms(3) assms(4) is_OK_returns_heap_I local.adopt_node_document_in_heap)
then
obtain sc where sc: "h ⊢ get_scdom_component (cast document_ptr) →⇩r sc"
using get_scdom_component_ok
by (meson assms(1) assms(2) assms(3) document_ptr_kinds_commutes returns_result_select_result)
have "node_ptr |∈| node_ptr_kinds h"
using assms(4)
by (meson is_OK_returns_heap_I local.adopt_node_child_in_heap)
then
obtain child_sc where child_sc: "h ⊢ get_scdom_component (cast node_ptr) →⇩r child_sc"
using get_scdom_component_ok
by (meson assms(1) assms(2) assms(3) is_OK_returns_result_E node_ptr_kinds_commutes)
then obtain owner_document where owner_document: "h ⊢ get_owner_document (cast node_ptr) →⇩r owner_document"
by (meson ‹node_ptr |∈| node_ptr_kinds h› assms(1) assms(2) assms(3) contra_subsetD
get_scdom_component_owner_document_same is_OK_returns_result_E
get_scdom_component_subset_get_dom_component local.get_dom_component_ok local.get_dom_component_ptr
node_ptr_kinds_commutes)
then have "h ⊢ get_scdom_component (cast owner_document) →⇩r child_sc"
using child_sc
by (metis (no_types, lifting) ‹node_ptr |∈| node_ptr_kinds h› assms(1) assms(2) assms(3)
get_scdom_component_owner_document_same get_scdom_component_ptrs_same_scope_component
get_scdom_component_subset_get_dom_component is_OK_returns_result_E local.get_dom_component_ok
local.get_dom_component_ptr node_ptr_kinds_commutes select_result_I2 subset_code(1))
have "ptr ∉ set |h ⊢ get_dom_component (cast document_ptr)|⇩r"
by (metis (no_types, lifting) ‹document_ptr |∈| document_ptr_kinds h› assms(1) assms(2) assms(3)
assms(5) contra_subsetD document_ptr_kinds_commutes get_scdom_component_subset_get_dom_component
local.get_dom_component_ok returns_result_select_result sc select_result_I2)
moreover have "ptr ∉ set |h ⊢ get_dom_component (cast node_ptr)|⇩r"
by (metis (no_types, lifting) ‹node_ptr |∈| node_ptr_kinds h› assms(1) assms(2) assms(3) assms(6)
child_sc contra_subsetD get_scdom_component_subset_get_dom_component local.get_dom_component_ok
node_ptr_kinds_commutes returns_result_select_result select_result_I2)
moreover have "ptr ∉ set |h ⊢ get_scdom_component (cast |h ⊢ get_owner_document (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r node_ptr)|⇩r)|⇩r"
using get_scdom_component_owner_document_same get_scdom_component_ptrs_same_scope_component
by (metis (no_types, lifting)
‹h ⊢ get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r owner_document) →⇩r child_sc› assms(6) child_sc
owner_document select_result_I2)
have "ptr ∉ set |h ⊢ get_dom_component (cast |h ⊢ get_owner_document (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r node_ptr)|⇩r)|⇩r"
using get_scdom_component_owner_document_same
by (metis (no_types, opaque_lifting)
‹⋀thesis. (⋀owner_document. h ⊢ get_owner_document (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r node_ptr) →⇩r owner_document ⟹ thesis) ⟹ thesis›
‹h ⊢ get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r owner_document) →⇩r child_sc›
‹ptr ∉ set |h ⊢ get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r |h ⊢ get_owner_document (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r node_ptr)|⇩r)|⇩r›
assms(1) assms(2) assms(3) contra_subsetD document_ptr_kinds_commutes get_scdom_component_subset_get_dom_component
is_OK_returns_result_E local.get_dom_component_ok local.get_owner_document_owner_document_in_heap owner_document
returns_result_eq select_result_I2)
ultimately show ?thesis
using assms(1) assms(2) assms(3) assms(4) adopt_node_is_component_unsafe
by blast
qed
lemma adopt_node_is_strongly_scdom_component_safe:
assumes "heap_is_wellformed h" and type_wf: "type_wf h" and known_ptrs: "known_ptrs h"
assumes "h ⊢ adopt_node document_ptr child →⇩h h'"
shows "is_strongly_scdom_component_safe {cast document_ptr, cast child} {} h h'"
proof -
obtain old_document parent_opt h2 where
old_document: "h ⊢ get_owner_document (cast child) →⇩r old_document"
and
parent_opt: "h ⊢ get_parent child →⇩r parent_opt"
and
h2: "h ⊢ (case parent_opt of Some parent ⇒ remove_child parent child | None ⇒ return ()) →⇩h h2"
and
h': "h2 ⊢ (if document_ptr ≠ old_document then do {
old_disc_nodes ← get_disconnected_nodes old_document;
set_disconnected_nodes old_document (remove1 child old_disc_nodes);
disc_nodes ← get_disconnected_nodes document_ptr;
set_disconnected_nodes document_ptr (child # disc_nodes)
} else do {
return ()
}) →⇩h h'"
using assms(4)
by(auto simp add: adopt_node_def elim!: bind_returns_heap_E
dest!: pure_returns_heap_eq[rotated, OF get_owner_document_pure]
pure_returns_heap_eq[rotated, OF get_parent_pure])
have object_ptr_kinds_h_eq3: "object_ptr_kinds h = object_ptr_kinds h2"
using h2 apply(simp split: option.splits)
apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h = object_ptr_kinds h'",
OF remove_child_writes])
using remove_child_pointers_preserved
by (auto simp add: reflp_def transp_def)
then have object_ptr_kinds_M_eq_h:
"⋀ptrs. h ⊢ object_ptr_kinds_M →⇩r ptrs = h2 ⊢ object_ptr_kinds_M →⇩r ptrs"
unfolding object_ptr_kinds_M_defs by simp
then have object_ptr_kinds_eq_h: "|h ⊢ object_ptr_kinds_M|⇩r = |h2 ⊢ object_ptr_kinds_M|⇩r"
by simp
then have node_ptr_kinds_eq_h: "|h ⊢ node_ptr_kinds_M|⇩r = |h2 ⊢ node_ptr_kinds_M|⇩r"
using node_ptr_kinds_M_eq by blast
have wellformed_h2: "heap_is_wellformed h2"
using h2 remove_child_heap_is_wellformed_preserved known_ptrs type_wf
by (metis (no_types, lifting) assms(1) option.case_eq_if pure_returns_heap_eq return_pure)
have "type_wf h2"
using h2 remove_child_preserves_type_wf known_ptrs type_wf
by (metis (no_types, lifting) assms(1) option.case_eq_if pure_returns_heap_eq return_pure)
have "known_ptrs h2"
using h2 remove_child_preserves_known_ptrs known_ptrs type_wf
by (metis (no_types, lifting) assms(1) option.case_eq_if pure_returns_heap_eq return_pure)
have "heap_is_wellformed h' ∧ known_ptrs h' ∧ type_wf h'"
proof(cases "document_ptr = old_document")
case True
then show ?thesis
using h' wellformed_h2 ‹type_wf h2› ‹known_ptrs h2› by auto
next
case False
then obtain h3 old_disc_nodes disc_nodes_document_ptr_h3 where
docs_neq: "document_ptr ≠ old_document" and
old_disc_nodes: "h2 ⊢ get_disconnected_nodes old_document →⇩r old_disc_nodes" and
h3: "h2 ⊢ set_disconnected_nodes old_document (remove1 child old_disc_nodes) →⇩h h3" and
disc_nodes_document_ptr_h3:
"h3 ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes_document_ptr_h3" and
h': "h3 ⊢ set_disconnected_nodes document_ptr (child # disc_nodes_document_ptr_h3) →⇩h h'"
using h'
by(auto elim!: bind_returns_heap_E
bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated] )
have object_ptr_kinds_h2_eq3: "object_ptr_kinds h2 = object_ptr_kinds h3"
apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h = object_ptr_kinds h'",
OF set_disconnected_nodes_writes h3])
using set_disconnected_nodes_pointers_preserved set_child_nodes_pointers_preserved
by (auto simp add: reflp_def transp_def)
then have object_ptr_kinds_M_eq_h2:
"⋀ptrs. h2 ⊢ object_ptr_kinds_M →⇩r ptrs = h3 ⊢ object_ptr_kinds_M →⇩r ptrs"
by(simp add: object_ptr_kinds_M_defs)
then have object_ptr_kinds_eq_h2: "|h2 ⊢ object_ptr_kinds_M|⇩r = |h3 ⊢ object_ptr_kinds_M|⇩r"
by(simp)
then have node_ptr_kinds_eq_h2: "|h2 ⊢ node_ptr_kinds_M|⇩r = |h3 ⊢ node_ptr_kinds_M|⇩r"
using node_ptr_kinds_M_eq by blast
then have node_ptr_kinds_eq3_h2: "node_ptr_kinds h2 = node_ptr_kinds h3"
by auto
have document_ptr_kinds_eq2_h2: "|h2 ⊢ document_ptr_kinds_M|⇩r = |h3 ⊢ document_ptr_kinds_M|⇩r"
using object_ptr_kinds_eq_h2 document_ptr_kinds_M_eq by auto
then have document_ptr_kinds_eq3_h2: "document_ptr_kinds h2 = document_ptr_kinds h3"
using object_ptr_kinds_eq_h2 document_ptr_kinds_M_eq by auto
have children_eq_h2:
"⋀ptr children. h2 ⊢ get_child_nodes ptr →⇩r children = h3 ⊢ get_child_nodes ptr →⇩r children"
using get_child_nodes_reads set_disconnected_nodes_writes h3
apply(rule reads_writes_preserved)
by (simp add: set_disconnected_nodes_get_child_nodes)
then have children_eq2_h2: "⋀ptr. |h2 ⊢ get_child_nodes ptr|⇩r = |h3 ⊢ get_child_nodes ptr|⇩r"
using select_result_eq by force
have object_ptr_kinds_h3_eq3: "object_ptr_kinds h3 = object_ptr_kinds h'"
apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h = object_ptr_kinds h'",
OF set_disconnected_nodes_writes h'])
using set_disconnected_nodes_pointers_preserved set_child_nodes_pointers_preserved
by (auto simp add: reflp_def transp_def)
then have object_ptr_kinds_M_eq_h3:
"⋀ptrs. h3 ⊢ 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_h3: "|h3 ⊢ object_ptr_kinds_M|⇩r = |h' ⊢ object_ptr_kinds_M|⇩r"
by(simp)
then have node_ptr_kinds_eq_h3: "|h3 ⊢ node_ptr_kinds_M|⇩r = |h' ⊢ node_ptr_kinds_M|⇩r"
using node_ptr_kinds_M_eq by blast
then have node_ptr_kinds_eq3_h3: "node_ptr_kinds h3 = node_ptr_kinds h'"
by auto
have document_ptr_kinds_eq2_h3: "|h3 ⊢ document_ptr_kinds_M|⇩r = |h' ⊢ document_ptr_kinds_M|⇩r"
using object_ptr_kinds_eq_h3 document_ptr_kinds_M_eq by auto
then have document_ptr_kinds_eq3_h3: "document_ptr_kinds h3 = document_ptr_kinds h'"
using object_ptr_kinds_eq_h3 document_ptr_kinds_M_eq by auto
have children_eq_h3:
"⋀ptr children. h3 ⊢ get_child_nodes ptr →⇩r children = h' ⊢ get_child_nodes ptr →⇩r children"
using get_child_nodes_reads set_disconnected_nodes_writes h'
apply(rule reads_writes_preserved)
by (simp add: set_disconnected_nodes_get_child_nodes)
then have children_eq2_h3: "⋀ptr. |h3 ⊢ get_child_nodes ptr|⇩r = |h' ⊢ get_child_nodes ptr|⇩r"
using select_result_eq by force
have disconnected_nodes_eq_h2:
"⋀doc_ptr disc_nodes. old_document ≠ doc_ptr
⟹ h2 ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes = h3 ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes"
using get_disconnected_nodes_reads set_disconnected_nodes_writes h3
apply(rule reads_writes_preserved)
by (simp add: set_disconnected_nodes_get_disconnected_nodes_different_pointers)
then have disconnected_nodes_eq2_h2:
"⋀doc_ptr. old_document ≠ doc_ptr
⟹ |h2 ⊢ get_disconnected_nodes doc_ptr|⇩r = |h3 ⊢ get_disconnected_nodes doc_ptr|⇩r"
using select_result_eq by force
obtain disc_nodes_old_document_h2 where disc_nodes_old_document_h2:
"h2 ⊢ get_disconnected_nodes old_document →⇩r disc_nodes_old_document_h2"
using old_disc_nodes by blast
then have disc_nodes_old_document_h3:
"h3 ⊢ get_disconnected_nodes old_document →⇩r remove1 child disc_nodes_old_document_h2"
using h3 old_disc_nodes returns_result_eq set_disconnected_nodes_get_disconnected_nodes
by fastforce
have "distinct disc_nodes_old_document_h2"
using disc_nodes_old_document_h2 local.heap_is_wellformed_disconnected_nodes_distinct wellformed_h2
by blast
have "type_wf h2"
proof (insert h2, induct parent_opt)
case None
then show ?case
using type_wf by simp
next
case (Some option)
then show ?case
using writes_small_big[where P="λh h'. type_wf h ⟶ type_wf h'", OF remove_child_writes]
type_wf remove_child_types_preserved
by (simp add: reflp_def transp_def)
qed
then have "type_wf h3"
using writes_small_big[where P="λh h'. type_wf h ⟶ type_wf h'", OF set_disconnected_nodes_writes h3]
using set_disconnected_nodes_types_preserved
by(auto simp add: reflp_def transp_def)
then have "type_wf h'"
using writes_small_big[where P="λh h'. type_wf h ⟶ type_wf h'", OF set_disconnected_nodes_writes h']
using set_disconnected_nodes_types_preserved
by(auto simp add: reflp_def transp_def)
have "known_ptrs h3"
using known_ptrs local.known_ptrs_preserved object_ptr_kinds_h2_eq3 object_ptr_kinds_h_eq3 by blast
then have "known_ptrs h'"
using local.known_ptrs_preserved object_ptr_kinds_h3_eq3 by blast
have disconnected_nodes_eq_h3:
"⋀doc_ptr disc_nodes. document_ptr ≠ doc_ptr
⟹ h3 ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes = h' ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes"
using get_disconnected_nodes_reads set_disconnected_nodes_writes h'
apply(rule reads_writes_preserved)
by (simp add: set_disconnected_nodes_get_disconnected_nodes_different_pointers)
then have disconnected_nodes_eq2_h3:
"⋀doc_ptr. document_ptr ≠ doc_ptr
⟹ |h3 ⊢ get_disconnected_nodes doc_ptr|⇩r = |h' ⊢ get_disconnected_nodes doc_ptr|⇩r"
using select_result_eq by force
have disc_nodes_document_ptr_h2:
"h2 ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes_document_ptr_h3"
using disconnected_nodes_eq_h2 docs_neq disc_nodes_document_ptr_h3 by auto
have disc_nodes_document_ptr_h': "
h' ⊢ get_disconnected_nodes document_ptr →⇩r child # disc_nodes_document_ptr_h3"
using h' disc_nodes_document_ptr_h3
using set_disconnected_nodes_get_disconnected_nodes by blast
have document_ptr_in_heap: "document_ptr |∈| document_ptr_kinds h2"
using disc_nodes_document_ptr_h3 document_ptr_kinds_eq2_h2 get_disconnected_nodes_ok assms(1)
unfolding heap_is_wellformed_def
using disc_nodes_document_ptr_h2 get_disconnected_nodes_ptr_in_heap by blast
have old_document_in_heap: "old_document |∈| document_ptr_kinds h2"
using disc_nodes_old_document_h3 document_ptr_kinds_eq2_h2 get_disconnected_nodes_ok assms(1)
unfolding heap_is_wellformed_def
using get_disconnected_nodes_ptr_in_heap old_disc_nodes by blast
have "child ∈ set disc_nodes_old_document_h2"
proof (insert parent_opt h2, induct parent_opt)
case None
then have "h = h2"
by(auto)
moreover have "a_owner_document_valid h"
using assms(1) heap_is_wellformed_def by(simp add: heap_is_wellformed_def)
ultimately show ?case
using old_document disc_nodes_old_document_h2 None(1) child_parent_dual[OF assms(1)]
in_disconnected_nodes_no_parent assms(1) known_ptrs type_wf by blast
next
case (Some option)
then show ?case
apply(simp split: option.splits)
using assms(1) disc_nodes_old_document_h2 old_document remove_child_in_disconnected_nodes known_ptrs
by blast
qed
have "child ∉ set (remove1 child disc_nodes_old_document_h2)"
using disc_nodes_old_document_h3 h3 known_ptrs wellformed_h2 ‹distinct disc_nodes_old_document_h2›
by auto
have "child ∉ set disc_nodes_document_ptr_h3"
proof -
have "a_distinct_lists h2"
using heap_is_wellformed_def wellformed_h2 by blast
then have 0: "distinct (concat (map (λdocument_ptr. |h2 ⊢ get_disconnected_nodes document_ptr|⇩r)
|h2 ⊢ document_ptr_kinds_M|⇩r))"
by(simp add: a_distinct_lists_def)
show ?thesis
using distinct_concat_map_E(1)[OF 0] ‹child ∈ set disc_nodes_old_document_h2›
disc_nodes_old_document_h2 disc_nodes_document_ptr_h2
by (meson ‹type_wf h2› docs_neq known_ptrs local.get_owner_document_disconnected_nodes
local.known_ptrs_preserved object_ptr_kinds_h_eq3 returns_result_eq wellformed_h2)
qed
have child_in_heap: "child |∈| node_ptr_kinds h"
using get_owner_document_ptr_in_heap[OF is_OK_returns_result_I[OF old_document]]
node_ptr_kinds_commutes by blast
have "a_acyclic_heap h2"
using wellformed_h2 by (simp add: heap_is_wellformed_def)
have "parent_child_rel h' ⊆ parent_child_rel h2"
proof
fix x
assume "x ∈ parent_child_rel h'"
then show "x ∈ parent_child_rel h2"
using object_ptr_kinds_h2_eq3 object_ptr_kinds_h3_eq3 children_eq2_h2 children_eq2_h3
mem_Collect_eq object_ptr_kinds_M_eq_h3 select_result_eq split_cong
unfolding parent_child_rel_def
by(simp)
qed
then have "a_acyclic_heap h'"
using ‹a_acyclic_heap h2› acyclic_heap_def acyclic_subset by blast
moreover have "a_all_ptrs_in_heap h2"
using wellformed_h2 by (simp add: heap_is_wellformed_def)
then have "a_all_ptrs_in_heap h3"
apply(auto simp add: a_all_ptrs_in_heap_def node_ptr_kinds_eq3_h2 children_eq_h2)[1]
apply (simp add: children_eq2_h2 object_ptr_kinds_h2_eq3 subset_code(1))
by (metis (no_types, lifting) ‹child ∈ set disc_nodes_old_document_h2› ‹type_wf h2›
disc_nodes_old_document_h2 disc_nodes_old_document_h3 disconnected_nodes_eq2_h2 document_ptr_kinds_eq3_h2
in_set_remove1 local.get_disconnected_nodes_ok local.heap_is_wellformed_disc_nodes_in_heap node_ptr_kinds_eq3_h2
returns_result_select_result select_result_I2 wellformed_h2)
then have "a_all_ptrs_in_heap h'"
apply(auto simp add: a_all_ptrs_in_heap_def node_ptr_kinds_eq3_h3 children_eq_h3)[1]
apply (simp add: children_eq2_h3 object_ptr_kinds_h3_eq3 subset_code(1))
by (metis (no_types, lifting) ‹child ∈ set disc_nodes_old_document_h2› disc_nodes_document_ptr_h'
disc_nodes_document_ptr_h2 disc_nodes_old_document_h2 disconnected_nodes_eq2_h3 document_ptr_kinds_eq3_h3
local.heap_is_wellformed_disc_nodes_in_heap node_ptr_kinds_eq3_h2 node_ptr_kinds_eq3_h3
select_result_I2 set_ConsD subset_code(1) wellformed_h2)
moreover have "a_owner_document_valid h2"
using wellformed_h2 by (simp add: heap_is_wellformed_def)
then have "a_owner_document_valid h'"
apply(simp add: a_owner_document_valid_def node_ptr_kinds_eq_h2 node_ptr_kinds_eq3_h3
object_ptr_kinds_eq_h2 object_ptr_kinds_eq_h3 document_ptr_kinds_eq2_h2
document_ptr_kinds_eq2_h3 children_eq2_h2 children_eq2_h3 )
by (smt (verit) disc_nodes_document_ptr_h' disc_nodes_document_ptr_h2
disc_nodes_old_document_h2 disc_nodes_old_document_h3
disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 document_ptr_in_heap
document_ptr_kinds_eq3_h2 document_ptr_kinds_eq3_h3 in_set_remove1
list.set_intros(1) node_ptr_kinds_eq3_h2 node_ptr_kinds_eq3_h3
object_ptr_kinds_h2_eq3 object_ptr_kinds_h3_eq3 select_result_I2
set_subset_Cons subset_code(1))
have a_distinct_lists_h2: "a_distinct_lists h2"
using wellformed_h2 by (simp add: heap_is_wellformed_def)
then have "a_distinct_lists h'"
apply(auto simp add: a_distinct_lists_def object_ptr_kinds_eq_h3 object_ptr_kinds_eq_h2
children_eq2_h2 children_eq2_h3)[1]
proof -
assume 1: "distinct (concat (map (λptr. |h' ⊢ get_child_nodes ptr|⇩r)
(sorted_list_of_set (fset (object_ptr_kinds h')))))"
and 2: "distinct (concat (map (λdocument_ptr. |h2 ⊢ get_disconnected_nodes document_ptr|⇩r)
(sorted_list_of_set (fset (document_ptr_kinds h2)))))"
and 3: "(⋃x∈fset (object_ptr_kinds h'). set |h' ⊢ get_child_nodes x|⇩r)
∩ (⋃x∈fset (document_ptr_kinds h2). set |h2 ⊢ get_disconnected_nodes x|⇩r) = {}"
show "distinct (concat (map (λdocument_ptr. |h' ⊢ get_disconnected_nodes document_ptr|⇩r)
(sorted_list_of_set (fset (document_ptr_kinds h')))))"
proof(rule distinct_concat_map_I)
show "distinct (sorted_list_of_set (fset (document_ptr_kinds h')))"
by(auto simp add: document_ptr_kinds_M_def )
next
fix x
assume a1: "x ∈ set (sorted_list_of_set (fset (document_ptr_kinds h')))"
have 4: "distinct |h2 ⊢ get_disconnected_nodes x|⇩r"
using a_distinct_lists_h2 "2" a1 concat_map_all_distinct document_ptr_kinds_eq2_h2
document_ptr_kinds_eq2_h3
by fastforce
then show "distinct |h' ⊢ get_disconnected_nodes x|⇩r"
proof (cases "old_document ≠ x")
case True
then show ?thesis
proof (cases "document_ptr ≠ x")
case True
then show ?thesis
using disconnected_nodes_eq2_h2[OF ‹old_document ≠ x›]
disconnected_nodes_eq2_h3[OF ‹document_ptr ≠ x›] 4
by(auto)
next
case False
then show ?thesis
using disc_nodes_document_ptr_h3 disc_nodes_document_ptr_h' 4
‹child ∉ set disc_nodes_document_ptr_h3›
by(auto simp add: disconnected_nodes_eq2_h2[OF ‹old_document ≠ x›] )
qed
next
case False
then show ?thesis
by (metis (no_types, opaque_lifting) ‹distinct disc_nodes_old_document_h2›
disc_nodes_old_document_h3 disconnected_nodes_eq2_h3
distinct_remove1 docs_neq select_result_I2)
qed
next
fix x y
assume a0: "x ∈ set (sorted_list_of_set (fset (document_ptr_kinds h')))"
and a1: "y ∈ set (sorted_list_of_set (fset (document_ptr_kinds h')))"
and a2: "x ≠ y"
moreover have 5: "set |h2 ⊢ get_disconnected_nodes x|⇩r ∩ set |h2 ⊢ get_disconnected_nodes y|⇩r = {}"
using 2 calculation
by (auto simp add: document_ptr_kinds_eq3_h2 document_ptr_kinds_eq3_h3 dest: distinct_concat_map_E(1))
ultimately show "set |h' ⊢ get_disconnected_nodes x|⇩r ∩ set |h' ⊢ get_disconnected_nodes y|⇩r = {}"
proof(cases "old_document = x")
case True
have "old_document ≠ y"
using ‹x ≠ y› ‹old_document = x› by simp
have "document_ptr ≠ x"
using docs_neq ‹old_document = x› by auto
show ?thesis
proof(cases "document_ptr = y")
case True
then show ?thesis
using 5 True select_result_I2[OF disc_nodes_document_ptr_h']
select_result_I2[OF disc_nodes_document_ptr_h2]
select_result_I2[OF disc_nodes_old_document_h2]
select_result_I2[OF disc_nodes_old_document_h3] ‹old_document = x›
by (metis (no_types, lifting) ‹child ∉ set (remove1 child disc_nodes_old_document_h2)›
‹document_ptr ≠ x› disconnected_nodes_eq2_h3 disjoint_iff_not_equal
notin_set_remove1 set_ConsD)
next
case False
then show ?thesis
using 5 select_result_I2[OF disc_nodes_document_ptr_h']
select_result_I2[OF disc_nodes_document_ptr_h2]
select_result_I2[OF disc_nodes_old_document_h2]
select_result_I2[OF disc_nodes_old_document_h3]
disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 ‹old_document = x›
docs_neq ‹old_document ≠ y›
by (metis (no_types, lifting) disjoint_iff_not_equal notin_set_remove1)
qed
next
case False
then show ?thesis
proof(cases "old_document = y")
case True
then show ?thesis
proof(cases "document_ptr = x")
case True
show ?thesis
using 5 select_result_I2[OF disc_nodes_document_ptr_h']
select_result_I2[OF disc_nodes_document_ptr_h2]
select_result_I2[OF disc_nodes_old_document_h2]
select_result_I2[OF disc_nodes_old_document_h3]
‹old_document ≠ x› ‹old_document = y› ‹document_ptr = x›
apply(simp)
by (metis (no_types, lifting) ‹child ∉ set (remove1 child disc_nodes_old_document_h2)›
disconnected_nodes_eq2_h3 disjoint_iff_not_equal notin_set_remove1)
next
case False
then show ?thesis
using 5 select_result_I2[OF disc_nodes_document_ptr_h']
select_result_I2[OF disc_nodes_document_ptr_h2]
select_result_I2[OF disc_nodes_old_document_h2]
select_result_I2[OF disc_nodes_old_document_h3]
‹old_document ≠ x› ‹old_document = y› ‹document_ptr ≠ x›
by (metis (no_types, lifting) disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3
disjoint_iff_not_equal docs_neq notin_set_remove1)
qed
next
case False
have "set |h2 ⊢ get_disconnected_nodes y|⇩r ∩ set disc_nodes_old_document_h2 = {}"
by (metis DocumentMonad.ptr_kinds_M_ok DocumentMonad.ptr_kinds_M_ptr_kinds False
‹type_wf h2› a1 disc_nodes_old_document_h2 document_ptr_kinds_M_def
document_ptr_kinds_eq2_h2 document_ptr_kinds_eq2_h3
l_ptr_kinds_M.ptr_kinds_ptr_kinds_M local.get_disconnected_nodes_ok
local.heap_is_wellformed_one_disc_parent returns_result_select_result
wellformed_h2)
then show ?thesis
proof(cases "document_ptr = x")
case True
then have "document_ptr ≠ y"
using ‹x ≠ y› by auto
have "set |h2 ⊢ get_disconnected_nodes y|⇩r ∩ set disc_nodes_old_document_h2 = {}"
using ‹set |h2 ⊢ get_disconnected_nodes y|⇩r ∩ set disc_nodes_old_document_h2 = {}›
by blast
then show ?thesis
using 5 select_result_I2[OF disc_nodes_document_ptr_h']
select_result_I2[OF disc_nodes_document_ptr_h2]
select_result_I2[OF disc_nodes_old_document_h2]
select_result_I2[OF disc_nodes_old_document_h3]
‹old_document ≠ x› ‹old_document ≠ y› ‹document_ptr = x› ‹document_ptr ≠ y›
‹child ∈ set disc_nodes_old_document_h2› disconnected_nodes_eq2_h2
disconnected_nodes_eq2_h3
‹set |h2 ⊢ get_disconnected_nodes y|⇩r ∩ set disc_nodes_old_document_h2 = {}›
by(auto)
next
case False
then show ?thesis
proof(cases "document_ptr = y")
case True
have f1: "set |h2 ⊢ get_disconnected_nodes x|⇩r ∩ set disc_nodes_document_ptr_h3 = {}"
using 2 a1 document_ptr_in_heap document_ptr_kinds_eq2_h2 document_ptr_kinds_eq2_h3
‹document_ptr ≠ x› select_result_I2[OF disc_nodes_document_ptr_h3, symmetric]
disconnected_nodes_eq2_h2[OF docs_neq[symmetric], symmetric]
by (simp add: "5" True)
moreover have f1:
"set |h2 ⊢ get_disconnected_nodes x|⇩r ∩ set |h2 ⊢ get_disconnected_nodes old_document|⇩r = {}"
using 2 a1 old_document_in_heap document_ptr_kinds_eq2_h2 document_ptr_kinds_eq2_h3
‹old_document ≠ x›
by (metis (no_types, lifting) a0 distinct_concat_map_E(1) document_ptr_kinds_eq3_h2
document_ptr_kinds_eq3_h3 finite_fset set_sorted_list_of_set)
ultimately show ?thesis
using 5 select_result_I2[OF disc_nodes_document_ptr_h']
select_result_I2[OF disc_nodes_old_document_h2] ‹old_document ≠ x›
‹document_ptr ≠ x› ‹document_ptr = y›
‹child ∈ set disc_nodes_old_document_h2› disconnected_nodes_eq2_h2
disconnected_nodes_eq2_h3
by auto
next
case False
then show ?thesis
using 5
select_result_I2[OF disc_nodes_old_document_h2] ‹old_document ≠ x›
‹document_ptr ≠ x› ‹document_ptr ≠ y›
‹child ∈ set disc_nodes_old_document_h2›
disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3
by (metis ‹set |h2 ⊢ get_disconnected_nodes y|⇩r ∩ set disc_nodes_old_document_h2 = {}›
empty_iff inf.idem)
qed
qed
qed
qed
qed
next
fix x xa xb
assume 0: "distinct (concat (map (λptr. |h' ⊢ get_child_nodes ptr|⇩r)
(sorted_list_of_set (fset (object_ptr_kinds h')))))"
and 1: "distinct (concat (map (λdocument_ptr. |h2 ⊢ get_disconnected_nodes document_ptr|⇩r)
(sorted_list_of_set (fset (document_ptr_kinds h2)))))"
and 2: "(⋃x∈fset (object_ptr_kinds h'). set |h' ⊢ get_child_nodes x|⇩r)
∩ (⋃x∈fset (document_ptr_kinds h2). set |h2 ⊢ get_disconnected_nodes x|⇩r) = {}"
and 3: "xa |∈| object_ptr_kinds h'"
and 4: "x ∈ set |h' ⊢ get_child_nodes xa|⇩r"
and 5: "xb |∈| document_ptr_kinds h'"
and 6: "x ∈ set |h' ⊢ get_disconnected_nodes xb|⇩r"
then show False
using ‹child ∈ set disc_nodes_old_document_h2› disc_nodes_document_ptr_h'
disc_nodes_document_ptr_h2 disc_nodes_old_document_h2 disc_nodes_old_document_h3
disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 document_ptr_kinds_eq2_h2
document_ptr_kinds_eq2_h3 old_document_in_heap
apply(auto)[1]
apply(cases "xb = old_document")
proof -
assume a1: "xb = old_document"
assume a2: "h2 ⊢ get_disconnected_nodes old_document →⇩r disc_nodes_old_document_h2"
assume a3: "h3 ⊢ get_disconnected_nodes old_document →⇩r remove1 child disc_nodes_old_document_h2"
assume a4: "x ∈ set |h' ⊢ get_child_nodes xa|⇩r"
assume "document_ptr_kinds h2 = document_ptr_kinds h'"
assume a5: "(⋃x∈fset (object_ptr_kinds h'). set |h' ⊢ get_child_nodes x|⇩r)
∩ (⋃x∈fset (document_ptr_kinds h'). set |h2 ⊢ get_disconnected_nodes x|⇩r) = {}"
have f6: "old_document |∈| document_ptr_kinds h'"
using a1 ‹xb |∈| document_ptr_kinds h'› by blast
have f7: "|h2 ⊢ get_disconnected_nodes old_document|⇩r = disc_nodes_old_document_h2"
using a2 by simp
have "x ∈ set disc_nodes_old_document_h2"
using f6 a3 a1 by (metis (no_types) ‹type_wf h'› ‹x ∈ set |h' ⊢ get_disconnected_nodes xb|⇩r›
disconnected_nodes_eq_h3 docs_neq get_disconnected_nodes_ok returns_result_eq
returns_result_select_result set_remove1_subset subsetCE)
then have "set |h' ⊢ get_child_nodes xa|⇩r ∩ set |h2 ⊢ get_disconnected_nodes xb|⇩r = {}"
using f7 f6 a5 a4 ‹xa |∈| object_ptr_kinds h'›
by fastforce
then show ?thesis
using ‹x ∈ set disc_nodes_old_document_h2› a1 a4 f7 by blast
next
assume a1: "xb ≠ old_document"
assume a2: "h2 ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes_document_ptr_h3"
assume a3: "h2 ⊢ get_disconnected_nodes old_document →⇩r disc_nodes_old_document_h2"
assume a4: "xa |∈| object_ptr_kinds h'"
assume a5: "h' ⊢ get_disconnected_nodes document_ptr →⇩r child # disc_nodes_document_ptr_h3"
assume a6: "old_document |∈| document_ptr_kinds h'"
assume a7: "x ∈ set |h' ⊢ get_disconnected_nodes xb|⇩r"
assume a8: "x ∈ set |h' ⊢ get_child_nodes xa|⇩r"
assume a9: "document_ptr_kinds h2 = document_ptr_kinds h'"
assume a10: "⋀doc_ptr. old_document ≠ doc_ptr
⟹ |h2 ⊢ get_disconnected_nodes doc_ptr|⇩r = |h3 ⊢ get_disconnected_nodes doc_ptr|⇩r"
assume a11: "⋀doc_ptr. document_ptr ≠ doc_ptr
⟹ |h3 ⊢ get_disconnected_nodes doc_ptr|⇩r = |h' ⊢ get_disconnected_nodes doc_ptr|⇩r"
assume a12: "(⋃x∈fset (object_ptr_kinds h'). set |h' ⊢ get_child_nodes x|⇩r)
∩ (⋃x∈fset (document_ptr_kinds h'). set |h2 ⊢ get_disconnected_nodes x|⇩r) = {}"
have f13: "⋀d. d ∉ set |h' ⊢ document_ptr_kinds_M|⇩r ∨ h2 ⊢ ok get_disconnected_nodes d"
using a9 ‹type_wf h2› get_disconnected_nodes_ok
by simp
then have f14: "|h2 ⊢ get_disconnected_nodes old_document|⇩r = disc_nodes_old_document_h2"
using a6 a3 by simp
have "x ∉ set |h2 ⊢ get_disconnected_nodes xb|⇩r"
using a12 a8 a4 ‹xb |∈| document_ptr_kinds h'›
by (meson UN_I disjoint_iff_not_equal)
then have "x = child"
using f13 a11 a10 a7 a5 a2 a1
by (metis (no_types, lifting) select_result_I2 set_ConsD)
then have "child ∉ set disc_nodes_old_document_h2"
using f14 a12 a8 a6 a4
by (metis ‹type_wf h'› adopt_node_removes_child assms type_wf
get_child_nodes_ok known_ptrs local.known_ptrs_known_ptr object_ptr_kinds_h2_eq3
object_ptr_kinds_h3_eq3 object_ptr_kinds_h_eq3 returns_result_select_result)
then show ?thesis
using ‹child ∈ set disc_nodes_old_document_h2› by fastforce
qed
qed
ultimately show ?thesis
using ‹type_wf h'› ‹known_ptrs h'› ‹a_owner_document_valid h'› heap_is_wellformed_def by blast
qed
then have "heap_is_wellformed h'" and "known_ptrs h'" and "type_wf h'"
by auto
have object_ptr_kinds_eq3: "object_ptr_kinds h = object_ptr_kinds h'"
apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h = object_ptr_kinds h'",
OF adopt_node_writes assms(4)])
unfolding adopt_node_locs_def
using set_disconnected_nodes_pointers_preserved set_child_nodes_pointers_preserved
remove_child_pointers_preserved
by (auto simp add: reflp_def transp_def split: if_splits)
show ?thesis
apply(auto simp add: is_strongly_scdom_component_safe_def Let_def object_ptr_kinds_eq3 )[1]
using adopt_node_is_strongly_dom_component_safe_step get_scdom_component_impl assms by blast
qed
end
interpretation i_get_scdom_component_adopt_node?: l_get_scdom_component_adopt_node⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
get_owner_document heap_is_wellformed parent_child_rel type_wf known_ptr known_ptrs
get_scdom_component is_strongly_scdom_component_safe is_weakly_scdom_component_safe get_dom_component
is_strongly_dom_component_safe is_weakly_dom_component_safe get_parent get_parent_locs remove_child
remove_child_locs get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes
set_disconnected_nodes_locs adopt_node adopt_node_locs get_child_nodes get_child_nodes_locs
set_child_nodes set_child_nodes_locs remove to_tree_order get_root_node get_root_node_locs
get_ancestors get_ancestors_locs get_element_by_id get_elements_by_class_name get_elements_by_tag_name
by(auto simp add: l_get_scdom_component_adopt_node⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def instances)
declare l_get_scdom_component_adopt_node⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]
subsubsection ‹create\_element›
locale l_get_scdom_component_create_element⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_dom_component_get_scdom_component +
l_get_dom_component_create_element⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_create_element_wf⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_to_tree_order⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_owner_document⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin
lemma create_element_is_strongly_scdom_component_safe_step:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ create_element document_ptr tag →⇩h h'"
assumes "ptr ∉ set |h ⊢ get_scdom_component (cast document_ptr)|⇩r"
assumes "ptr ≠ cast |h ⊢ create_element document_ptr tag|⇩r"
shows "preserved (get_M ptr getter) h h'"
proof -
obtain new_element_ptr h2 h3 disc_nodes where
new_element_ptr: "h ⊢ new_element →⇩r new_element_ptr" and
h2: "h ⊢ new_element →⇩h h2" and
h3: "h2 ⊢set_tag_name new_element_ptr tag →⇩h h3" and
disc_nodes: "h3 ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes" and
h': "h3 ⊢ set_disconnected_nodes document_ptr (cast new_element_ptr # disc_nodes) →⇩h h'"
using assms(4)
by(auto simp add: create_element_def elim!: bind_returns_heap_E bind_returns_heap_E2[rotated,
OF get_disconnected_nodes_pure, rotated])
have object_ptr_kinds_eq_h: "object_ptr_kinds h2 = object_ptr_kinds h |∪| {|cast new_element_ptr|}"
using new_element_new_ptr h2 new_element_ptr by blast
then have node_ptr_kinds_eq_h: "node_ptr_kinds h2 = node_ptr_kinds h |∪| {|cast new_element_ptr|}"
apply(simp add: node_ptr_kinds_def)
by force
then have element_ptr_kinds_eq_h: "element_ptr_kinds h2 = element_ptr_kinds h |∪| {|new_element_ptr|}"
apply(simp add: element_ptr_kinds_def)
by force
have character_data_ptr_kinds_eq_h: "character_data_ptr_kinds h2 = character_data_ptr_kinds h"
using object_ptr_kinds_eq_h
by(auto simp add: node_ptr_kinds_def character_data_ptr_kinds_def)
have document_ptr_kinds_eq_h: "document_ptr_kinds h2 = document_ptr_kinds h"
using object_ptr_kinds_eq_h
by(auto simp add: document_ptr_kinds_def)
have object_ptr_kinds_eq_h2: "object_ptr_kinds h3 = object_ptr_kinds h2"
apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h' = object_ptr_kinds h", OF set_tag_name_writes h3])
using set_tag_name_pointers_preserved
by (auto simp add: reflp_def transp_def)
then have document_ptr_kinds_eq_h2: "document_ptr_kinds h3 = document_ptr_kinds h2"
by (auto simp add: document_ptr_kinds_def)
have node_ptr_kinds_eq_h2: "node_ptr_kinds h3 = node_ptr_kinds h2"
using object_ptr_kinds_eq_h2
by(auto simp add: node_ptr_kinds_def)
have object_ptr_kinds_eq_h3: "object_ptr_kinds h' = object_ptr_kinds h3"
apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h' = object_ptr_kinds h",
OF set_disconnected_nodes_writes h'])
using set_disconnected_nodes_pointers_preserved
by (auto simp add: reflp_def transp_def)
then have document_ptr_kinds_eq_h3: "document_ptr_kinds h' = document_ptr_kinds h3"
by (auto simp add: document_ptr_kinds_def)
have node_ptr_kinds_eq_h3: "node_ptr_kinds h' = node_ptr_kinds h3"
using object_ptr_kinds_eq_h3
by(auto simp add: node_ptr_kinds_def)
have "heap_is_wellformed h'"
using assms(4)
using assms(1) assms(2) assms(3) local.create_element_preserves_wellformedness(1) by blast
have "type_wf h'"
using assms(1) assms(2) assms(3) assms(4) local.create_element_preserves_wellformedness(2) by blast
have "known_ptrs h'"
using assms(1) assms(2) assms(3) assms(4) local.create_element_preserves_wellformedness(3) by blast
have "document_ptr |∈| document_ptr_kinds h"
by (meson assms(4) is_OK_returns_heap_I local.create_element_document_in_heap)
then
obtain sc where sc: "h ⊢ get_scdom_component (cast document_ptr) →⇩r sc"
using get_scdom_component_ok
by (meson assms(1) assms(2) assms(3) document_ptr_kinds_commutes returns_result_select_result)
have "document_ptr |∈| document_ptr_kinds h'"
using ‹document_ptr |∈| document_ptr_kinds h› document_ptr_kinds_eq_h
using document_ptr_kinds_eq_h2 document_ptr_kinds_eq_h3 by blast
then
obtain sc' where sc': "h' ⊢ get_scdom_component (cast document_ptr) →⇩r sc'"
using get_scdom_component_ok
by (meson ‹heap_is_wellformed h'› ‹known_ptrs h'› ‹type_wf h'› document_ptr_kinds_commutes
returns_result_select_result)
obtain c where c: "h ⊢ get_dom_component (cast document_ptr) →⇩r c"
by (meson ‹document_ptr |∈| document_ptr_kinds h› assms(1) assms(2) assms(3)
document_ptr_kinds_commutes is_OK_returns_result_E local.get_dom_component_ok)
have "set c ⊆ set sc"
using assms(1) assms(2) assms(3) c get_scdom_component_subset_get_dom_component sc by blast
have "ptr ∉ set c"
using ‹set c ⊆ set sc› assms(5) sc
by auto
then
show ?thesis
using create_element_is_weakly_dom_component_safe
by (metis (no_types, lifting) assms(1) assms(2) assms(3) assms(4) assms(6) c
local.create_element_is_weakly_dom_component_safe_step select_result_I2)
qed
lemma create_element_is_strongly_scdom_component_safe:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ create_element document_ptr tag →⇩r result"
assumes "h ⊢ create_element document_ptr tag →⇩h h'"
shows "is_strongly_scdom_component_safe {cast document_ptr} {cast result} h h'"
proof -
obtain new_element_ptr h2 h3 disc_nodes_h3 where
new_element_ptr: "h ⊢ new_element →⇩r new_element_ptr" and
h2: "h ⊢ new_element →⇩h h2" and
h3: "h2 ⊢ set_tag_name new_element_ptr tag →⇩h h3" and
disc_nodes_h3: "h3 ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes_h3" and
h': "h3 ⊢ set_disconnected_nodes document_ptr (cast new_element_ptr # disc_nodes_h3) →⇩h h'"
using assms(5)
by(auto simp add: create_element_def returns_result_heap_def
elim!: bind_returns_heap_E
bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated] )
then have "h ⊢ create_element document_ptr tag →⇩r new_element_ptr"
apply(auto simp add: create_element_def intro!: bind_returns_result_I)[1]
apply (metis is_OK_returns_heap_I is_OK_returns_result_E old.unit.exhaust)
apply (metis is_OK_returns_heap_E is_OK_returns_result_I local.get_disconnected_nodes_pure pure_returns_heap_eq)
by (metis is_OK_returns_heap_I is_OK_returns_result_E old.unit.exhaust)
then have "result = new_element_ptr"
using assms(4) by auto
have "new_element_ptr ∉ set |h ⊢ element_ptr_kinds_M|⇩r"
using new_element_ptr ElementMonad.ptr_kinds_ptr_kinds_M h2
using new_element_ptr_not_in_heap by blast
then have "cast new_element_ptr ∉ set |h ⊢ node_ptr_kinds_M|⇩r"
by simp
then have "cast new_element_ptr ∉ set |h ⊢ object_ptr_kinds_M|⇩r"
by simp
have object_ptr_kinds_eq_h: "object_ptr_kinds h2 = object_ptr_kinds h |∪| {|cast new_element_ptr|}"
using new_element_new_ptr h2 new_element_ptr by blast
then have node_ptr_kinds_eq_h: "node_ptr_kinds h2 = node_ptr_kinds h |∪| {|cast new_element_ptr|}"
apply(simp add: node_ptr_kinds_def)
by force
then have element_ptr_kinds_eq_h: "element_ptr_kinds h2 = element_ptr_kinds h |∪| {|new_element_ptr|}"
apply(simp add: element_ptr_kinds_def)
by force
have character_data_ptr_kinds_eq_h: "character_data_ptr_kinds h2 = character_data_ptr_kinds h"
using object_ptr_kinds_eq_h
by(auto simp add: node_ptr_kinds_def character_data_ptr_kinds_def)
have document_ptr_kinds_eq_h: "document_ptr_kinds h2 = document_ptr_kinds h"
using object_ptr_kinds_eq_h
by(auto simp add: document_ptr_kinds_def)
have object_ptr_kinds_eq_h2: "object_ptr_kinds h3 = object_ptr_kinds h2"
apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h' = object_ptr_kinds h", OF set_tag_name_writes h3])
using set_tag_name_pointers_preserved
by (auto simp add: reflp_def transp_def)
then have document_ptr_kinds_eq_h2: "document_ptr_kinds h3 = document_ptr_kinds h2"
by (auto simp add: document_ptr_kinds_def)
have node_ptr_kinds_eq_h2: "node_ptr_kinds h3 = node_ptr_kinds h2"
using object_ptr_kinds_eq_h2
by(auto simp add: node_ptr_kinds_def)
have object_ptr_kinds_eq_h3: "object_ptr_kinds h' = object_ptr_kinds h3"
apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h' = object_ptr_kinds h",
OF set_disconnected_nodes_writes h'])
using set_disconnected_nodes_pointers_preserved
by (auto simp add: reflp_def transp_def)
then have document_ptr_kinds_eq_h3: "document_ptr_kinds h' = document_ptr_kinds h3"
by (auto simp add: document_ptr_kinds_def)
have node_ptr_kinds_eq_h3: "node_ptr_kinds h' = node_ptr_kinds h3"
using object_ptr_kinds_eq_h3
by(auto simp add: node_ptr_kinds_def)
have "known_ptr (cast new_element_ptr)"
using ‹h ⊢ create_element document_ptr tag →⇩r new_element_ptr› local.create_element_known_ptr by blast
then
have "known_ptrs h2"
using known_ptrs_new_ptr object_ptr_kinds_eq_h ‹known_ptrs h› h2
by blast
then
have "known_ptrs h3"
using known_ptrs_preserved object_ptr_kinds_eq_h2 by blast
then
have "known_ptrs h'"
using known_ptrs_preserved object_ptr_kinds_eq_h3 by blast
have "document_ptr |∈| document_ptr_kinds h"
using disc_nodes_h3 document_ptr_kinds_eq_h object_ptr_kinds_eq_h2
get_disconnected_nodes_ptr_in_heap ‹type_wf h› document_ptr_kinds_def
by (metis is_OK_returns_result_I)
have children_eq_h: "⋀ptr' children. ptr' ≠ cast new_element_ptr
⟹ h ⊢ get_child_nodes ptr' →⇩r children = h2 ⊢ get_child_nodes ptr' →⇩r children"
using get_child_nodes_reads h2 get_child_nodes_new_element[rotated, OF new_element_ptr h2]
apply(auto simp add: reads_def reflp_def transp_def preserved_def)[1]
by blast+
then have children_eq2_h: "⋀ptr'. ptr' ≠ cast new_element_ptr
⟹ |h ⊢ get_child_nodes ptr'|⇩r = |h2 ⊢ get_child_nodes ptr'|⇩r"
using select_result_eq by force
have "h2 ⊢ get_child_nodes (cast new_element_ptr) →⇩r []"
using new_element_ptr h2 new_element_ptr_in_heap[OF h2 new_element_ptr]
new_element_is_element_ptr[OF new_element_ptr] new_element_no_child_nodes
by blast
have disconnected_nodes_eq_h:
"⋀doc_ptr disc_nodes. h ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes
= h2 ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes"
using get_disconnected_nodes_reads h2 get_disconnected_nodes_new_element[OF new_element_ptr h2]
apply(auto simp add: reads_def reflp_def transp_def preserved_def)[1]
by blast+
then have disconnected_nodes_eq2_h:
"⋀doc_ptr. |h ⊢ get_disconnected_nodes doc_ptr|⇩r = |h2 ⊢ get_disconnected_nodes doc_ptr|⇩r"
using select_result_eq by force
have children_eq_h2:
"⋀ptr' children. h2 ⊢ get_child_nodes ptr' →⇩r children = h3 ⊢ get_child_nodes ptr' →⇩r children"
using get_child_nodes_reads set_tag_name_writes h3
apply(rule reads_writes_preserved)
by(auto simp add: set_tag_name_get_child_nodes)
then have children_eq2_h2: "⋀ptr'. |h2 ⊢ get_child_nodes ptr'|⇩r = |h3 ⊢ get_child_nodes ptr'|⇩r"
using select_result_eq by force
have disconnected_nodes_eq_h2:
"⋀doc_ptr disc_nodes. h2 ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes
= h3 ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes"
using get_disconnected_nodes_reads set_tag_name_writes h3
apply(rule reads_writes_preserved)
by(auto simp add: set_tag_name_get_disconnected_nodes)
then have disconnected_nodes_eq2_h2:
"⋀doc_ptr. |h2 ⊢ get_disconnected_nodes doc_ptr|⇩r = |h3 ⊢ get_disconnected_nodes doc_ptr|⇩r"
using select_result_eq by force
have "type_wf h2"
using ‹type_wf h› new_element_types_preserved h2 by blast
then have "type_wf h3"
using writes_small_big[where P="λh h'. type_wf h ⟶ type_wf h'", OF set_tag_name_writes h3]
using set_tag_name_types_preserved
by(auto simp add: reflp_def transp_def)
then have "type_wf h'"
using writes_small_big[where P="λh h'. type_wf h ⟶ type_wf h'", OF set_disconnected_nodes_writes h']
using set_disconnected_nodes_types_preserved
by(auto simp add: reflp_def transp_def)
have children_eq_h3:
"⋀ptr' children. h3 ⊢ get_child_nodes ptr' →⇩r children = h' ⊢ get_child_nodes ptr' →⇩r children"
using get_child_nodes_reads set_disconnected_nodes_writes h'
apply(rule reads_writes_preserved)
by(auto simp add: set_disconnected_nodes_get_child_nodes)
then have children_eq2_h3: "⋀ptr'. |h3 ⊢ get_child_nodes ptr'|⇩r = |h' ⊢ get_child_nodes ptr'|⇩r"
using select_result_eq by force
have disconnected_nodes_eq_h3:
"⋀doc_ptr disc_nodes. document_ptr ≠ doc_ptr
⟹ h3 ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes
= h' ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes"
using get_disconnected_nodes_reads set_disconnected_nodes_writes h'
apply(rule reads_writes_preserved)
by(auto simp add: set_disconnected_nodes_get_disconnected_nodes_different_pointers)
then have disconnected_nodes_eq2_h3:
"⋀doc_ptr. document_ptr ≠ doc_ptr
⟹ |h3 ⊢ get_disconnected_nodes doc_ptr|⇩r = |h' ⊢ get_disconnected_nodes doc_ptr|⇩r"
using select_result_eq by force
have disc_nodes_document_ptr_h2: "h2 ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes_h3"
using disconnected_nodes_eq_h2 disc_nodes_h3 by auto
then have disc_nodes_document_ptr_h: "h ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes_h3"
using disconnected_nodes_eq_h by auto
then have "cast new_element_ptr ∉ set disc_nodes_h3"
using ‹heap_is_wellformed h›
using ‹cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r new_element_ptr ∉ set |h ⊢ node_ptr_kinds_M|⇩r›
a_all_ptrs_in_heap_def heap_is_wellformed_def
using NodeMonad.ptr_kinds_ptr_kinds_M local.heap_is_wellformed_disc_nodes_in_heap by blast
have "parent_child_rel h = parent_child_rel h'"
proof -
have "parent_child_rel h = parent_child_rel h2"
proof(auto simp add: parent_child_rel_def)[1]
fix a x
assume 0: "a |∈| object_ptr_kinds h"
and 1: "x ∈ set |h ⊢ get_child_nodes a|⇩r"
then show "a |∈| object_ptr_kinds h2"
by (simp add: object_ptr_kinds_eq_h)
next
fix a x
assume 0: "a |∈| object_ptr_kinds h"
and 1: "x ∈ set |h ⊢ get_child_nodes a|⇩r"
then show "x ∈ set |h2 ⊢ get_child_nodes a|⇩r"
by (metis ObjectMonad.ptr_kinds_ptr_kinds_M
‹cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_element_ptr ∉ set |h ⊢ object_ptr_kinds_M|⇩r› children_eq2_h)
next
fix a x
assume 0: "a |∈| object_ptr_kinds h2"
and 1: "x ∈ set |h2 ⊢ get_child_nodes a|⇩r"
then show "a |∈| object_ptr_kinds h"
using object_ptr_kinds_eq_h ‹h2 ⊢ get_child_nodes (cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_element_ptr) →⇩r []›
by(auto)
next
fix a x
assume 0: "a |∈| object_ptr_kinds h2"
and 1: "x ∈ set |h2 ⊢ get_child_nodes a|⇩r"
then show "x ∈ set |h ⊢ get_child_nodes a|⇩r"
by (metis (no_types, lifting)
‹h2 ⊢ get_child_nodes (cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_element_ptr) →⇩r []›
children_eq2_h empty_iff empty_set image_eqI select_result_I2)
qed
also have "… = parent_child_rel h3"
by(auto simp add: parent_child_rel_def object_ptr_kinds_eq_h2 children_eq2_h2)
also have "… = parent_child_rel h'"
by(auto simp add: parent_child_rel_def object_ptr_kinds_eq_h3 children_eq2_h3)
finally show ?thesis
by simp
qed
have "document_ptr |∈| document_ptr_kinds h'"
by (simp add: ‹document_ptr |∈| document_ptr_kinds h› document_ptr_kinds_eq_h
document_ptr_kinds_eq_h2 document_ptr_kinds_eq_h3)
have "known_ptr (cast document_ptr)"
using ‹document_ptr |∈| document_ptr_kinds h› assms(3) document_ptr_kinds_commutes
local.known_ptrs_known_ptr by blast
have "h ⊢ get_owner_document (cast document_ptr) →⇩r document_ptr"
using ‹known_ptr (cast document_ptr)› ‹document_ptr |∈| document_ptr_kinds h›
apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def)[1]
apply(split invoke_splits, rule conjI)+
by(auto simp add: known_ptr_impl known_ptr_defs CharacterDataClass.known_ptr_defs
ElementClass.known_ptr_defs NodeClass.known_ptr_defs a_get_owner_document⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def intro!: bind_pure_returns_result_I split: option.splits)
have "h' ⊢ get_owner_document (cast document_ptr) →⇩r document_ptr"
using ‹known_ptr (cast document_ptr)› ‹document_ptr |∈| document_ptr_kinds h'›
apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def)[1]
apply(split invoke_splits, rule conjI)+
by(auto simp add: known_ptr_impl known_ptr_defs CharacterDataClass.known_ptr_defs
ElementClass.known_ptr_defs NodeClass.known_ptr_defs a_get_owner_document⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def intro!: bind_pure_returns_result_I split: option.splits)
obtain to where to: "h ⊢ to_tree_order (cast document_ptr) →⇩r to"
by (meson ‹h ⊢ get_owner_document (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr) →⇩r document_ptr› assms(1)
assms(2) assms(3) is_OK_returns_result_E is_OK_returns_result_I local.get_owner_document_ptr_in_heap
local.to_tree_order_ok)
obtain to' where to': "h' ⊢ to_tree_order (cast document_ptr) →⇩r to'"
by (metis ‹document_ptr |∈| document_ptr_kinds h› ‹known_ptrs h'› ‹type_wf h'› assms(1) assms(2)
assms(3) assms(5) document_ptr_kinds_commutes document_ptr_kinds_eq_h document_ptr_kinds_eq_h2
document_ptr_kinds_eq_h3 is_OK_returns_result_E local.create_element_preserves_wellformedness(1)
local.to_tree_order_ok)
have "set to = set to'"
proof safe
fix x
assume "x ∈ set to"
show "x ∈ set to'"
using to to'
using to_tree_order_parent_child_rel ‹parent_child_rel h = parent_child_rel h'›
by (metis ‹known_ptrs h'› ‹type_wf h'› ‹x ∈ set to› assms(1) assms(2) assms(3) assms(5)
local.create_element_preserves_wellformedness(1))
next
fix x
assume "x ∈ set to'"
show "x ∈ set to"
using to to'
using to_tree_order_parent_child_rel ‹parent_child_rel h = parent_child_rel h'›
by (metis ‹known_ptrs h'› ‹type_wf h'› ‹x ∈ set to'› assms(1) assms(2) assms(3) assms(5)
local.create_element_preserves_wellformedness(1))
qed
have "h' ⊢ get_disconnected_nodes document_ptr →⇩r cast new_element_ptr # disc_nodes_h3"
using h' local.set_disconnected_nodes_get_disconnected_nodes by auto
obtain disc_nodes_h' where disc_nodes_h': "h' ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes_h'"
and "cast new_element_ptr ∈ set disc_nodes_h'"
and "disc_nodes_h' = cast new_element_ptr # disc_nodes_h3"
by (simp add: ‹h' ⊢ get_disconnected_nodes document_ptr →⇩r cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r new_element_ptr # disc_nodes_h3›)
have "⋀disc_ptr to to'. disc_ptr ∈ set disc_nodes_h3 ⟹ h ⊢ to_tree_order (cast disc_ptr) →⇩r to ⟹
h' ⊢ to_tree_order (cast disc_ptr) →⇩r to' ⟹ set to = set to'"
proof safe
fix disc_ptr to to' x
assume "disc_ptr ∈ set disc_nodes_h3"
assume "h ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r to"
assume "h' ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r to'"
assume "x ∈ set to"
show "x ∈ set to'"
using to_tree_order_parent_child_rel ‹parent_child_rel h = parent_child_rel h'›
by (metis ‹h ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r to›
‹h' ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r to'› ‹known_ptrs h'› ‹type_wf h'› ‹x ∈ set to›
assms(1) assms(2) assms(3) assms(5) local.create_element_preserves_wellformedness(1))
next
fix disc_ptr to to' x
assume "disc_ptr ∈ set disc_nodes_h3"
assume "h ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r to"
assume "h' ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r to'"
assume "x ∈ set to'"
show "x ∈ set to"
using to_tree_order_parent_child_rel ‹parent_child_rel h = parent_child_rel h'›
by (metis ‹h ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r to›
‹h' ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r to'› ‹known_ptrs h'› ‹type_wf h'› ‹x ∈ set to'›
assms(1) assms(2) assms(3) assms(5) local.create_element_preserves_wellformedness(1))
qed
have "heap_is_wellformed h'"
using assms(1) assms(2) assms(3) assms(5) local.create_element_preserves_wellformedness(1)
by blast
have "cast new_element_ptr |∈| object_ptr_kinds h'"
using ‹cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r new_element_ptr ∈ set disc_nodes_h'› ‹heap_is_wellformed h'› disc_nodes_h'
local.heap_is_wellformed_disc_nodes_in_heap node_ptr_kinds_commutes by blast
then
have "new_element_ptr |∈| element_ptr_kinds h'"
by simp
have "⋀node_ptr. node_ptr ∈ set disc_nodes_h3 ⟹ node_ptr |∈| node_ptr_kinds h'"
by (meson ‹heap_is_wellformed h'› h' local.heap_is_wellformed_disc_nodes_in_heap
local.set_disconnected_nodes_get_disconnected_nodes set_subset_Cons subset_code(1))
have "h ⊢ ok (map_M (to_tree_order ∘ cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r) disc_nodes_h3)"
using assms(1) assms(2) assms(3) to_tree_order_ok
apply(auto intro!: map_M_ok_I)[1]
using disc_nodes_document_ptr_h local.heap_is_wellformed_disc_nodes_in_heap node_ptr_kinds_commutes
by blast
then
obtain disc_tree_orders where disc_tree_orders:
"h ⊢ map_M (to_tree_order ∘ cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r) disc_nodes_h3 →⇩r disc_tree_orders"
by auto
have "h' ⊢ ok (map_M (to_tree_order ∘ cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r) disc_nodes_h')"
apply(auto intro!: map_M_ok_I)[1]
apply(simp add: ‹disc_nodes_h' = cast new_element_ptr # disc_nodes_h3›)
using ‹⋀node_ptr. node_ptr ∈ set disc_nodes_h3 ⟹ node_ptr |∈| node_ptr_kinds h'›
‹cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r new_element_ptr ∈ set disc_nodes_h'› ‹heap_is_wellformed h'› ‹known_ptrs h'›
‹type_wf h'› disc_nodes_h' local.heap_is_wellformed_disc_nodes_in_heap local.to_tree_order_ok
node_ptr_kinds_commutes by blast
then
obtain disc_tree_orders' where disc_tree_orders':
"h' ⊢ map_M (to_tree_order ∘ cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r) disc_nodes_h' →⇩r disc_tree_orders'"
by auto
have "h' ⊢ get_child_nodes (cast new_element_ptr) →⇩r []"
using ‹h2 ⊢ get_child_nodes (cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_element_ptr) →⇩r []› children_eq_h2
children_eq_h3 by auto
obtain new_tree_order where new_tree_order:
"h' ⊢ to_tree_order (cast new_element_ptr) →⇩r new_tree_order" and
"new_tree_order ∈ set disc_tree_orders'"
using map_M_pure_E[OF disc_tree_orders' ‹cast new_element_ptr ∈ set disc_nodes_h'›]
by auto
then have "new_tree_order = [cast new_element_ptr]"
using ‹h' ⊢ get_child_nodes (cast new_element_ptr) →⇩r []›
by(auto simp add: to_tree_order_def
dest!: bind_returns_result_E3[rotated, OF ‹h' ⊢ get_child_nodes (cast new_element_ptr) →⇩r []›, rotated])
obtain foo where foo: "h' ⊢ map_M (to_tree_order ∘ cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r)
(cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r new_element_ptr # disc_nodes_h3) →⇩r [cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_element_ptr] # foo"
apply(auto intro!: bind_pure_returns_result_I map_M_pure_I)[1]
using ‹new_tree_order = [cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_element_ptr]› new_tree_order apply auto[1]
by (smt (verit) ‹disc_nodes_h' = cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r new_element_ptr # disc_nodes_h3›
bind_pure_returns_result_I bind_returns_result_E2 comp_apply disc_tree_orders'
local.to_tree_order_pure map_M.simps(2) map_M_pure_I return_returns_result returns_result_eq)
then have "set (concat foo) = set (concat disc_tree_orders)"
apply(auto elim!: bind_returns_result_E2 intro!: map_M_pure_I)[1]
apply (smt (verit) ‹⋀to' toa disc_ptr. ⟦disc_ptr ∈ set disc_nodes_h3; h ⊢ to_tree_order
(cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r toa; h' ⊢ to_tree_order
(cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r to'⟧ ⟹ set toa = set to'›
comp_eq_dest_lhs disc_tree_orders local.to_tree_order_pure map_M_pure_E map_M_pure_E2)
by (smt (verit) ‹⋀to' toa disc_ptr. ⟦disc_ptr ∈ set disc_nodes_h3; h ⊢ to_tree_order
(cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r toa; h' ⊢ to_tree_order
(cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r to'⟧ ⟹ set toa = set to'›
comp_eq_dest_lhs disc_tree_orders local.to_tree_order_pure map_M_pure_E map_M_pure_E2)
have "disc_tree_orders' = [cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_element_ptr] # foo"
using foo disc_tree_orders'
by (simp add: ‹disc_nodes_h' = cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r new_element_ptr # disc_nodes_h3› returns_result_eq)
have "set (concat disc_tree_orders') = {cast new_element_ptr} ∪ set (concat disc_tree_orders)"
apply(auto simp add: ‹disc_tree_orders' = [cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_element_ptr] # foo›)[1]
using ‹set (concat foo) = set (concat disc_tree_orders)› by auto
have "h' ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr) →⇩r to' @ concat disc_tree_orders'"
using ‹h' ⊢ get_owner_document (cast document_ptr) →⇩r document_ptr› disc_nodes_h' to' disc_tree_orders'
by(auto simp add: a_get_scdom_component_def intro!: bind_pure_returns_result_I map_M_pure_I)
then
have "set |h' ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r =
set to' ∪ set (concat disc_tree_orders')"
by auto
have "h ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr) →⇩r to @ concat disc_tree_orders"
using ‹h ⊢ get_owner_document (cast document_ptr) →⇩r document_ptr› disc_nodes_document_ptr_h
to disc_tree_orders
by(auto simp add: a_get_scdom_component_def intro!: bind_pure_returns_result_I map_M_pure_I)
then
have "set |h ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r = set to ∪ set (concat disc_tree_orders)"
by auto
have "{cast new_element_ptr} ∪ set |h ⊢ local.a_get_scdom_component (cast document_ptr)|⇩r =
set |h' ⊢ local.a_get_scdom_component (cast document_ptr)|⇩r"
proof(safe)
show "cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_element_ptr
∈ set |h' ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r"
using ‹h' ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr) →⇩r to' @ concat disc_tree_orders'›
apply(auto simp add: a_get_scdom_component_def)[1]
by (meson ‹⋀thesis. (⋀new_tree_order. ⟦h' ⊢ to_tree_order (cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_element_ptr) →⇩r new_tree_order;
new_tree_order ∈ set disc_tree_orders'⟧ ⟹ thesis) ⟹ thesis› local.to_tree_order_ptr_in_result)
next
fix x
assume " x ∈ set |h ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r"
then
show "x ∈ set |h' ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r"
using ‹set |h ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r =
set to ∪set (concat disc_tree_orders)›
using ‹set |h' ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r =
set to' ∪ set (concat disc_tree_orders')›
using ‹set to = set to'›
using ‹set (concat disc_tree_orders') = {cast new_element_ptr} ∪ set (concat disc_tree_orders)›
by(auto)
next
fix x
assume " x ∈ set |h' ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r"
assume "x ∉ set |h ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r"
show "x = cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_element_ptr"
using ‹set |h ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r =
set to ∪ set (concat disc_tree_orders)›
using ‹set |h' ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r =
set to' ∪ set (concat disc_tree_orders')›
using ‹set to = set to'›
using ‹set (concat disc_tree_orders') = {cast new_element_ptr} ∪ set (concat disc_tree_orders)›
using ‹x ∈ set |h' ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r›
‹x ∉ set |h ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r›
by auto
qed
have "object_ptr_kinds h' = object_ptr_kinds h |∪| {|cast new_element_ptr|}"
using object_ptr_kinds_eq_h object_ptr_kinds_eq_h2 object_ptr_kinds_eq_h3 by auto
then
show ?thesis
apply(auto simp add: is_strongly_scdom_component_safe_def Let_def)[1]
apply(rule bexI[where x="cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr"])
using ‹{cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_element_ptr} ∪
set |h ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r =
set |h' ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r›
apply auto[2]
using ‹set to = set to'› ‹set |h ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r =
set to ∪ set (concat disc_tree_orders)› local.to_tree_order_ptr_in_result to'
apply auto[1]
using ‹document_ptr |∈| document_ptr_kinds h›
apply blast
apply(rule bexI[where x="cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr"])
using ‹result = new_element_ptr›
‹{cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_element_ptr} ∪ set |h ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r =
set |h' ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r› apply auto[1]
apply(auto)[1]
using ‹set to = set to'› ‹set |h ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r =
set to ∪ set (concat disc_tree_orders)› local.to_tree_order_ptr_in_result to' apply auto[1]
apply (simp add: ‹document_ptr |∈| document_ptr_kinds h›)
using ‹⋀thesis. (⋀new_element_ptr h2 h3 disc_nodes_h3. ⟦h ⊢ new_element →⇩r new_element_ptr;
h ⊢ new_element →⇩h h2; h2 ⊢ set_tag_name new_element_ptr tag →⇩h h3;
h3 ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes_h3;
h3 ⊢ set_disconnected_nodes document_ptr (cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r new_element_ptr # disc_nodes_h3) →⇩h h'⟧ ⟹ thesis) ⟹ thesis›
new_element_ptr new_element_ptr_not_in_heap
apply auto[1]
using create_element_is_strongly_scdom_component_safe_step
by (smt (verit, best) ObjectMonad.ptr_kinds_ptr_kinds_M
‹cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_element_ptr ∉ set |h ⊢
object_ptr_kinds_M|⇩r› ‹h ⊢ create_element document_ptr tag →⇩r new_element_ptr› assms(1)
assms(2) assms(3) assms(5) local.get_scdom_component_impl select_result_I2)
qed
end
interpretation i_get_scdom_component_remove_child?: l_get_scdom_component_remove_child⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
get_owner_document heap_is_wellformed parent_child_rel type_wf known_ptr known_ptrs get_scdom_component
is_strongly_scdom_component_safe is_weakly_scdom_component_safe get_dom_component is_strongly_dom_component_safe
is_weakly_dom_component_safe to_tree_order get_parent get_parent_locs get_child_nodes get_child_nodes_locs
get_root_node get_root_node_locs get_ancestors get_ancestors_locs get_disconnected_nodes get_disconnected_nodes_locs
get_element_by_id get_elements_by_class_name get_elements_by_tag_name set_child_nodes set_child_nodes_locs
set_disconnected_nodes set_disconnected_nodes_locs remove_child remove_child_locs remove
by(auto simp add: l_get_scdom_component_remove_child⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def instances)
declare l_get_scdom_component_remove_child⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]
subsubsection ‹create\_character\_data›
locale l_get_scdom_component_create_character_data⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_dom_component_get_scdom_component +
l_get_dom_component_create_character_data⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_create_character_data_wf⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_to_tree_order⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_owner_document⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin
lemma create_character_data_is_strongly_dom_component_safe_step:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ create_character_data document_ptr text →⇩h h'"
assumes "ptr ∉ set |h ⊢ get_scdom_component (cast document_ptr)|⇩r"
assumes "ptr ≠ cast |h ⊢ create_character_data document_ptr text|⇩r"
shows "preserved (get_M ptr getter) h h'"
proof -
have "document_ptr |∈| document_ptr_kinds h"
by (meson assms(4) is_OK_returns_heap_I local.create_character_data_document_in_heap)
then
obtain sc where sc: "h ⊢ get_scdom_component (cast document_ptr) →⇩r sc"
using get_scdom_component_ok
by (meson assms(1) assms(2) assms(3) document_ptr_kinds_commutes returns_result_select_result)
obtain c where c: "h ⊢ get_dom_component (cast document_ptr) →⇩r c"
by (meson ‹document_ptr |∈| document_ptr_kinds h› assms(1) assms(2) assms(3)
document_ptr_kinds_commutes is_OK_returns_result_E local.get_dom_component_ok)
have "set c ⊆ set sc"
using assms(1) assms(2) assms(3) c get_scdom_component_subset_get_dom_component sc by blast
have "ptr ∉ set c"
using ‹set c ⊆ set sc› assms(5) sc
by auto
then
show ?thesis
by (metis (no_types, lifting) assms(1) assms(2) assms(3) assms(4) assms(6) c
local.create_character_data_is_weakly_dom_component_safe_step select_result_I2)
qed
lemma create_character_data_is_strongly_dom_component_safe:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ create_character_data document_ptr text →⇩r result"
assumes "h ⊢ create_character_data document_ptr text →⇩h h'"
shows "is_strongly_scdom_component_safe {cast document_ptr} {cast result} h h'"
proof -
obtain new_character_data_ptr h2 h3 disc_nodes_h3 where
new_character_data_ptr: "h ⊢ new_character_data →⇩r new_character_data_ptr" and
h2: "h ⊢ new_character_data →⇩h h2" and
h3: "h2 ⊢ set_val new_character_data_ptr text →⇩h h3" and
disc_nodes_h3: "h3 ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes_h3" and
h': "h3 ⊢ set_disconnected_nodes document_ptr (cast new_character_data_ptr # disc_nodes_h3) →⇩h h'"
using assms(5)
by(auto simp add: create_character_data_def
elim!: bind_returns_heap_E
bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated] )
then have "h ⊢ create_character_data document_ptr text →⇩r new_character_data_ptr"
apply(auto simp add: create_character_data_def intro!: bind_returns_result_I)[1]
apply (metis is_OK_returns_heap_I is_OK_returns_result_E old.unit.exhaust)
apply (metis is_OK_returns_heap_E is_OK_returns_result_I local.get_disconnected_nodes_pure
pure_returns_heap_eq)
by (metis is_OK_returns_heap_I is_OK_returns_result_E old.unit.exhaust)
then have "result = new_character_data_ptr"
using assms(4) by auto
have "new_character_data_ptr ∉ set |h ⊢ character_data_ptr_kinds_M|⇩r"
using new_character_data_ptr CharacterDataMonad.ptr_kinds_ptr_kinds_M h2
using new_character_data_ptr_not_in_heap by blast
then have "cast new_character_data_ptr ∉ set |h ⊢ node_ptr_kinds_M|⇩r"
by simp
then have "cast new_character_data_ptr ∉ set |h ⊢ object_ptr_kinds_M|⇩r"
by simp
have object_ptr_kinds_eq_h:
"object_ptr_kinds h2 = object_ptr_kinds h |∪| {|cast new_character_data_ptr|}"
using new_character_data_new_ptr h2 new_character_data_ptr by blast
then have node_ptr_kinds_eq_h:
"node_ptr_kinds h2 = node_ptr_kinds h |∪| {|cast new_character_data_ptr|}"
apply(simp add: node_ptr_kinds_def)
by force
then have character_data_ptr_kinds_eq_h:
"character_data_ptr_kinds h2 = character_data_ptr_kinds h |∪| {|new_character_data_ptr|}"
apply(simp add: character_data_ptr_kinds_def)
by force
have element_ptr_kinds_eq_h: "element_ptr_kinds h2 = element_ptr_kinds h"
using object_ptr_kinds_eq_h
by(auto simp add: node_ptr_kinds_def element_ptr_kinds_def)
have document_ptr_kinds_eq_h: "document_ptr_kinds h2 = document_ptr_kinds h"
using object_ptr_kinds_eq_h
by(auto simp add: document_ptr_kinds_def)
have object_ptr_kinds_eq_h2: "object_ptr_kinds h3 = object_ptr_kinds h2"
apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h' = object_ptr_kinds h",
OF set_val_writes h3])
using set_val_pointers_preserved
by (auto simp add: reflp_def transp_def)
then have document_ptr_kinds_eq_h2: "document_ptr_kinds h3 = document_ptr_kinds h2"
by (auto simp add: document_ptr_kinds_def)
have node_ptr_kinds_eq_h2: "node_ptr_kinds h3 = node_ptr_kinds h2"
using object_ptr_kinds_eq_h2
by(auto simp add: node_ptr_kinds_def)
have object_ptr_kinds_eq_h3: "object_ptr_kinds h' = object_ptr_kinds h3"
apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h' = object_ptr_kinds h",
OF set_disconnected_nodes_writes h'])
using set_disconnected_nodes_pointers_preserved
by (auto simp add: reflp_def transp_def)
then have document_ptr_kinds_eq_h3: "document_ptr_kinds h' = document_ptr_kinds h3"
by (auto simp add: document_ptr_kinds_def)
have node_ptr_kinds_eq_h3: "node_ptr_kinds h' = node_ptr_kinds h3"
using object_ptr_kinds_eq_h3
by(auto simp add: node_ptr_kinds_def)
have "document_ptr |∈| document_ptr_kinds h"
using disc_nodes_h3 document_ptr_kinds_eq_h object_ptr_kinds_eq_h2
get_disconnected_nodes_ptr_in_heap ‹type_wf h› document_ptr_kinds_def
by (metis is_OK_returns_result_I)
have children_eq_h: "⋀ptr' children. ptr' ≠ cast new_character_data_ptr
⟹ h ⊢ get_child_nodes ptr' →⇩r children = h2 ⊢ get_child_nodes ptr' →⇩r children"
using get_child_nodes_reads h2 get_child_nodes_new_character_data[rotated, OF new_character_data_ptr h2]
apply(auto simp add: reads_def reflp_def transp_def preserved_def)[1]
by blast+
then have children_eq2_h:
"⋀ptr'. ptr' ≠ cast new_character_data_ptr
⟹ |h ⊢ get_child_nodes ptr'|⇩r = |h2 ⊢ get_child_nodes ptr'|⇩r"
using select_result_eq by force
have object_ptr_kinds_eq_h:
"object_ptr_kinds h2 = object_ptr_kinds h |∪| {|cast new_character_data_ptr|}"
using new_character_data_new_ptr h2 new_character_data_ptr by blast
then have node_ptr_kinds_eq_h:
"node_ptr_kinds h2 = node_ptr_kinds h |∪| {|cast new_character_data_ptr|}"
apply(simp add: node_ptr_kinds_def)
by force
then have character_data_ptr_kinds_eq_h:
"character_data_ptr_kinds h2 = character_data_ptr_kinds h |∪| {|new_character_data_ptr|}"
apply(simp add: character_data_ptr_kinds_def)
by force
have element_ptr_kinds_eq_h: "element_ptr_kinds h2 = element_ptr_kinds h"
using object_ptr_kinds_eq_h
by(auto simp add: node_ptr_kinds_def element_ptr_kinds_def)
have document_ptr_kinds_eq_h: "document_ptr_kinds h2 = document_ptr_kinds h"
using object_ptr_kinds_eq_h
by(auto simp add: document_ptr_kinds_def)
have object_ptr_kinds_eq_h2: "object_ptr_kinds h3 = object_ptr_kinds h2"
apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h' = object_ptr_kinds h",
OF set_val_writes h3])
using set_val_pointers_preserved
by (auto simp add: reflp_def transp_def)
then have document_ptr_kinds_eq_h2: "document_ptr_kinds h3 = document_ptr_kinds h2"
by (auto simp add: document_ptr_kinds_def)
have node_ptr_kinds_eq_h2: "node_ptr_kinds h3 = node_ptr_kinds h2"
using object_ptr_kinds_eq_h2
by(auto simp add: node_ptr_kinds_def)
have object_ptr_kinds_eq_h3: "object_ptr_kinds h' = object_ptr_kinds h3"
apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h' = object_ptr_kinds h",
OF set_disconnected_nodes_writes h'])
using set_disconnected_nodes_pointers_preserved
by (auto simp add: reflp_def transp_def)
then have document_ptr_kinds_eq_h3: "document_ptr_kinds h' = document_ptr_kinds h3"
by (auto simp add: document_ptr_kinds_def)
have node_ptr_kinds_eq_h3: "node_ptr_kinds h' = node_ptr_kinds h3"
using object_ptr_kinds_eq_h3
by(auto simp add: node_ptr_kinds_def)
have "document_ptr |∈| document_ptr_kinds h"
using disc_nodes_h3 document_ptr_kinds_eq_h object_ptr_kinds_eq_h2
get_disconnected_nodes_ptr_in_heap ‹type_wf h› document_ptr_kinds_def
by (metis is_OK_returns_result_I)
have children_eq_h: "⋀ptr' children. ptr' ≠ cast new_character_data_ptr
⟹ h ⊢ get_child_nodes ptr' →⇩r children = h2 ⊢ get_child_nodes ptr' →⇩r children"
using get_child_nodes_reads h2 get_child_nodes_new_character_data[rotated, OF new_character_data_ptr h2]
apply(auto simp add: reads_def reflp_def transp_def preserved_def)[1]
by blast+
then have children_eq2_h: "⋀ptr'. ptr' ≠ cast new_character_data_ptr
⟹ |h ⊢ get_child_nodes ptr'|⇩r = |h2 ⊢ get_child_nodes ptr'|⇩r"
using select_result_eq by force
have "h2 ⊢ get_child_nodes (cast new_character_data_ptr) →⇩r []"
using new_character_data_ptr h2 new_character_data_ptr_in_heap[OF h2 new_character_data_ptr]
new_character_data_is_character_data_ptr[OF new_character_data_ptr]
new_character_data_no_child_nodes
by blast
have disconnected_nodes_eq_h:
"⋀doc_ptr disc_nodes. h ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes
= h2 ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes"
using get_disconnected_nodes_reads h2
get_disconnected_nodes_new_character_data[OF new_character_data_ptr h2]
apply(auto simp add: reads_def reflp_def transp_def preserved_def)[1]
by blast+
then have disconnected_nodes_eq2_h:
"⋀doc_ptr. |h ⊢ get_disconnected_nodes doc_ptr|⇩r = |h2 ⊢ get_disconnected_nodes doc_ptr|⇩r"
using select_result_eq by force
have children_eq_h2:
"⋀ptr' children. h2 ⊢ get_child_nodes ptr' →⇩r children = h3 ⊢ get_child_nodes ptr' →⇩r children"
using get_child_nodes_reads set_val_writes h3
apply(rule reads_writes_preserved)
by(auto simp add: set_val_get_child_nodes)
then have children_eq2_h2:
"⋀ptr'. |h2 ⊢ get_child_nodes ptr'|⇩r = |h3 ⊢ get_child_nodes ptr'|⇩r"
using select_result_eq by force
have disconnected_nodes_eq_h2:
"⋀doc_ptr disc_nodes. h2 ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes
= h3 ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes"
using get_disconnected_nodes_reads set_val_writes h3
apply(rule reads_writes_preserved)
by(auto simp add: set_val_get_disconnected_nodes)
then have disconnected_nodes_eq2_h2:
"⋀doc_ptr. |h2 ⊢ get_disconnected_nodes doc_ptr|⇩r = |h3 ⊢ get_disconnected_nodes doc_ptr|⇩r"
using select_result_eq by force
have "type_wf h2"
using ‹type_wf h› new_character_data_types_preserved h2 by blast
then have "type_wf h3"
using writes_small_big[where P="λh h'. type_wf h ⟶ type_wf h'", OF set_val_writes h3]
using set_val_types_preserved
by(auto simp add: reflp_def transp_def)
then have "type_wf h'"
using writes_small_big[where P="λh h'. type_wf h ⟶ type_wf h'", OF set_disconnected_nodes_writes h']
using set_disconnected_nodes_types_preserved
by(auto simp add: reflp_def transp_def)
have children_eq_h3:
"⋀ptr' children. h3 ⊢ get_child_nodes ptr' →⇩r children = h' ⊢ get_child_nodes ptr' →⇩r children"
using get_child_nodes_reads set_disconnected_nodes_writes h'
apply(rule reads_writes_preserved)
by(auto simp add: set_disconnected_nodes_get_child_nodes)
then have children_eq2_h3:
" ⋀ptr'. |h3 ⊢ get_child_nodes ptr'|⇩r = |h' ⊢ get_child_nodes ptr'|⇩r"
using select_result_eq by force
have disconnected_nodes_eq_h3: "⋀doc_ptr disc_nodes. document_ptr ≠ doc_ptr
⟹ h3 ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes
= h' ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes"
using get_disconnected_nodes_reads set_disconnected_nodes_writes h'
apply(rule reads_writes_preserved)
by(auto simp add: set_disconnected_nodes_get_disconnected_nodes_different_pointers)
then have disconnected_nodes_eq2_h3: "⋀doc_ptr. document_ptr ≠ doc_ptr
⟹ |h3 ⊢ get_disconnected_nodes doc_ptr|⇩r = |h' ⊢ get_disconnected_nodes doc_ptr|⇩r"
using select_result_eq by force
have disc_nodes_document_ptr_h2: "h2 ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes_h3"
using disconnected_nodes_eq_h2 disc_nodes_h3 by auto
then have disc_nodes_document_ptr_h: "h ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes_h3"
using disconnected_nodes_eq_h by auto
then have "cast new_character_data_ptr ∉ set disc_nodes_h3"
using ‹heap_is_wellformed h› using ‹cast new_character_data_ptr ∉ set |h ⊢ node_ptr_kinds_M|⇩r›
a_all_ptrs_in_heap_def heap_is_wellformed_def
using NodeMonad.ptr_kinds_ptr_kinds_M local.heap_is_wellformed_disc_nodes_in_heap by blast
have "parent_child_rel h = parent_child_rel h'"
proof -
have "parent_child_rel h = parent_child_rel h2"
proof(auto simp add: parent_child_rel_def)[1]
fix a x
assume 0: "a |∈| object_ptr_kinds h"
and 1: "x ∈ set |h ⊢ get_child_nodes a|⇩r"
then show "a |∈| object_ptr_kinds h2"
by (simp add: object_ptr_kinds_eq_h)
next
fix a x
assume 0: "a |∈| object_ptr_kinds h"
and 1: "x ∈ set |h ⊢ get_child_nodes a|⇩r"
then show "x ∈ set |h2 ⊢ get_child_nodes a|⇩r"
by (metis ObjectMonad.ptr_kinds_ptr_kinds_M
‹cast new_character_data_ptr ∉ set |h ⊢ object_ptr_kinds_M|⇩r› children_eq2_h)
next
fix a x
assume 0: "a |∈| object_ptr_kinds h2"
and 1: "x ∈ set |h2 ⊢ get_child_nodes a|⇩r"
then show "a |∈| object_ptr_kinds h"
using object_ptr_kinds_eq_h ‹h2 ⊢ get_child_nodes (cast new_character_data_ptr) →⇩r []›
by(auto)
next
fix a x
assume 0: "a |∈| object_ptr_kinds h2"
and 1: "x ∈ set |h2 ⊢ get_child_nodes a|⇩r"
then show "x ∈ set |h ⊢ get_child_nodes a|⇩r"
by (metis (no_types, lifting) ‹h2 ⊢ get_child_nodes (cast new_character_data_ptr) →⇩r []›
children_eq2_h empty_iff empty_set image_eqI select_result_I2)
qed
also have "… = parent_child_rel h3"
by(auto simp add: parent_child_rel_def object_ptr_kinds_eq_h2 children_eq2_h2)
also have "… = parent_child_rel h'"
by(auto simp add: parent_child_rel_def object_ptr_kinds_eq_h3 children_eq2_h3)
finally show ?thesis
by simp
qed
have "known_ptr (cast new_character_data_ptr)"
using ‹h ⊢ create_character_data document_ptr text →⇩r new_character_data_ptr›
create_character_data_known_ptr by blast
then
have "known_ptrs h2"
using known_ptrs_new_ptr object_ptr_kinds_eq_h ‹known_ptrs h› h2
by blast
then
have "known_ptrs h3"
using known_ptrs_preserved object_ptr_kinds_eq_h2 by blast
then
have "known_ptrs h'"
using known_ptrs_preserved object_ptr_kinds_eq_h3 by blast
have "document_ptr |∈| document_ptr_kinds h'"
by (simp add: ‹document_ptr |∈| document_ptr_kinds h› document_ptr_kinds_eq_h
document_ptr_kinds_eq_h2 document_ptr_kinds_eq_h3)
have "known_ptr (cast document_ptr)"
using ‹document_ptr |∈| document_ptr_kinds h› assms(3) document_ptr_kinds_commutes
local.known_ptrs_known_ptr by blast
have "h ⊢ get_owner_document (cast document_ptr) →⇩r document_ptr"
using ‹known_ptr (cast document_ptr)› ‹document_ptr |∈| document_ptr_kinds h›
apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def)[1]
apply(split invoke_splits, rule conjI)+
by(auto simp add: known_ptr_impl known_ptr_defs CharacterDataClass.known_ptr_defs
ElementClass.known_ptr_defs NodeClass.known_ptr_defs a_get_owner_document⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def
intro!: bind_pure_returns_result_I split: option.splits)
have "h' ⊢ get_owner_document (cast document_ptr) →⇩r document_ptr"
using ‹known_ptr (cast document_ptr)› ‹document_ptr |∈| document_ptr_kinds h'›
apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def)[1]
apply(split invoke_splits, rule conjI)+
by(auto simp add: known_ptr_impl known_ptr_defs CharacterDataClass.known_ptr_defs
ElementClass.known_ptr_defs NodeClass.known_ptr_defs a_get_owner_document⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def
intro!: bind_pure_returns_result_I split: option.splits)
obtain to where to: "h ⊢ to_tree_order (cast document_ptr) →⇩r to"
by (meson ‹h ⊢ get_owner_document (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr) →⇩r document_ptr›
assms(1) assms(2) assms(3) is_OK_returns_result_E is_OK_returns_result_I
local.get_owner_document_ptr_in_heap local.to_tree_order_ok)
obtain to' where to': "h' ⊢ to_tree_order (cast document_ptr) →⇩r to'"
by (metis ‹document_ptr |∈| document_ptr_kinds h› ‹known_ptrs h'› ‹type_wf h'› assms(1) assms(2)
assms(3) assms(5) document_ptr_kinds_commutes document_ptr_kinds_eq_h document_ptr_kinds_eq_h2
document_ptr_kinds_eq_h3 is_OK_returns_result_E local.create_character_data_preserves_wellformedness(1)
local.to_tree_order_ok)
have "set to = set to'"
proof safe
fix x
assume "x ∈ set to"
show "x ∈ set to'"
using to to'
using to_tree_order_parent_child_rel ‹parent_child_rel h = parent_child_rel h'›
by (metis ‹known_ptrs h'› ‹type_wf h'› ‹x ∈ set to› assms(1) assms(2) assms(3) assms(5)
local.create_character_data_preserves_wellformedness(1))
next
fix x
assume "x ∈ set to'"
show "x ∈ set to"
using to to'
using to_tree_order_parent_child_rel ‹parent_child_rel h = parent_child_rel h'›
by (metis ‹known_ptrs h'› ‹type_wf h'› ‹x ∈ set to'› assms(1) assms(2) assms(3) assms(5)
local.create_character_data_preserves_wellformedness(1))
qed
have "h' ⊢ get_disconnected_nodes document_ptr →⇩r cast new_character_data_ptr # disc_nodes_h3"
using h' local.set_disconnected_nodes_get_disconnected_nodes by auto
obtain disc_nodes_h' where disc_nodes_h': "h' ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes_h'"
and "cast new_character_data_ptr ∈ set disc_nodes_h'"
and "disc_nodes_h' = cast new_character_data_ptr # disc_nodes_h3"
by (simp add: ‹h' ⊢ get_disconnected_nodes document_ptr →⇩r cast new_character_data_ptr # disc_nodes_h3›)
have "⋀disc_ptr to to'. disc_ptr ∈ set disc_nodes_h3 ⟹ h ⊢ to_tree_order (cast disc_ptr) →⇩r to ⟹
h' ⊢ to_tree_order (cast disc_ptr) →⇩r to' ⟹ set to = set to'"
proof safe
fix disc_ptr to to' x
assume "disc_ptr ∈ set disc_nodes_h3"
assume "h ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r to"
assume "h' ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r to'"
assume "x ∈ set to"
show "x ∈ set to'"
using to_tree_order_parent_child_rel ‹parent_child_rel h = parent_child_rel h'›
by (metis ‹h ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r to›
‹h' ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r to'› ‹known_ptrs h'› ‹type_wf h'› ‹x ∈ set to›
assms(1) assms(2) assms(3) assms(5) local.create_character_data_preserves_wellformedness(1))
next
fix disc_ptr to to' x
assume "disc_ptr ∈ set disc_nodes_h3"
assume "h ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r to"
assume "h' ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r to'"
assume "x ∈ set to'"
show "x ∈ set to"
using to_tree_order_parent_child_rel ‹parent_child_rel h = parent_child_rel h'›
by (metis ‹h ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r to›
‹h' ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r to'› ‹known_ptrs h'› ‹type_wf h'› ‹x ∈ set to'›
assms(1) assms(2) assms(3) assms(5) local.create_character_data_preserves_wellformedness(1))
qed
have "heap_is_wellformed h'"
using assms(1) assms(2) assms(3) assms(5) local.create_character_data_preserves_wellformedness(1)
by blast
have "cast new_character_data_ptr |∈| object_ptr_kinds h'"
using ‹cast new_character_data_ptr ∈ set disc_nodes_h'› ‹heap_is_wellformed h'› disc_nodes_h'
local.heap_is_wellformed_disc_nodes_in_heap node_ptr_kinds_commutes by blast
then
have "new_character_data_ptr |∈| character_data_ptr_kinds h'"
by simp
have "⋀node_ptr. node_ptr ∈ set disc_nodes_h3 ⟹ node_ptr |∈| node_ptr_kinds h'"
by (meson ‹heap_is_wellformed h'› h' local.heap_is_wellformed_disc_nodes_in_heap
local.set_disconnected_nodes_get_disconnected_nodes set_subset_Cons subset_code(1))
have "h ⊢ ok (map_M (to_tree_order ∘ cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r) disc_nodes_h3)"
using assms(1) assms(2) assms(3) to_tree_order_ok
apply(auto intro!: map_M_ok_I)[1]
using disc_nodes_document_ptr_h local.heap_is_wellformed_disc_nodes_in_heap node_ptr_kinds_commutes
by blast
then
obtain disc_tree_orders where disc_tree_orders:
"h ⊢ map_M (to_tree_order ∘ cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r) disc_nodes_h3 →⇩r disc_tree_orders"
by auto
have "h' ⊢ ok (map_M (to_tree_order ∘ cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r) disc_nodes_h')"
apply(auto intro!: map_M_ok_I)[1]
apply(simp add: ‹disc_nodes_h' = cast new_character_data_ptr # disc_nodes_h3›)
using ‹⋀node_ptr. node_ptr ∈ set disc_nodes_h3 ⟹ node_ptr |∈| node_ptr_kinds h'›
‹cast new_character_data_ptr ∈ set disc_nodes_h'› ‹heap_is_wellformed h'› ‹known_ptrs h'›
‹type_wf h'› disc_nodes_h' local.heap_is_wellformed_disc_nodes_in_heap local.to_tree_order_ok
node_ptr_kinds_commutes by blast
then
obtain disc_tree_orders' where disc_tree_orders':
"h' ⊢ map_M (to_tree_order ∘ cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r) disc_nodes_h' →⇩r disc_tree_orders'"
by auto
have "h' ⊢ get_child_nodes (cast new_character_data_ptr) →⇩r []"
using ‹h2 ⊢ get_child_nodes (cast new_character_data_ptr) →⇩r []› children_eq_h2 children_eq_h3 by auto
obtain new_tree_order where new_tree_order:
"h' ⊢ to_tree_order (cast new_character_data_ptr) →⇩r new_tree_order" and
"new_tree_order ∈ set disc_tree_orders'"
using map_M_pure_E[OF disc_tree_orders' ‹cast new_character_data_ptr ∈ set disc_nodes_h'›]
by auto
then have "new_tree_order = [cast new_character_data_ptr]"
using ‹h' ⊢ get_child_nodes (cast new_character_data_ptr) →⇩r []›
by(auto simp add: to_tree_order_def
dest!: bind_returns_result_E3[rotated, OF ‹h' ⊢ get_child_nodes (cast new_character_data_ptr) →⇩r []›, rotated])
obtain foo where foo: "h' ⊢ map_M (to_tree_order ∘ cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r)
(cast new_character_data_ptr # disc_nodes_h3) →⇩r [cast new_character_data_ptr] # foo"
apply(auto intro!: bind_pure_returns_result_I map_M_pure_I)[1]
using ‹new_tree_order = [cast new_character_data_ptr]› new_tree_order apply auto[1]
using ‹disc_nodes_h' = cast new_character_data_ptr # disc_nodes_h3› bind_pure_returns_result_I
bind_returns_result_E2 comp_apply disc_tree_orders' local.to_tree_order_pure map_M.simps(2)
map_M_pure_I return_returns_result returns_result_eq
apply simp
by (smt (verit) ‹disc_nodes_h' = cast new_character_data_ptr # disc_nodes_h3› bind_pure_returns_result_I
bind_returns_result_E2 comp_apply disc_tree_orders' local.to_tree_order_pure map_M.simps(2) map_M_pure_I
return_returns_result returns_result_eq)
then have "set (concat foo) = set (concat disc_tree_orders)"
apply(auto elim!: bind_returns_result_E2 intro!: map_M_pure_I)[1]
apply (smt (verit) ‹⋀to' toa disc_ptr. ⟦disc_ptr ∈ set disc_nodes_h3;
h ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r toa; h' ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r to'⟧ ⟹
set toa = set to'› comp_apply disc_tree_orders local.to_tree_order_pure map_M_pure_E map_M_pure_E2)
by (smt (verit) ‹⋀to' toa disc_ptr. ⟦disc_ptr ∈ set disc_nodes_h3; h ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r toa;
h' ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r disc_ptr) →⇩r to'⟧ ⟹ set toa = set to'› comp_apply disc_tree_orders
local.to_tree_order_pure map_M_pure_E map_M_pure_E2)
have "disc_tree_orders' = [cast new_character_data_ptr] # foo"
using foo disc_tree_orders'
by (simp add: ‹disc_nodes_h' = cast new_character_data_ptr # disc_nodes_h3› returns_result_eq)
have "set (concat disc_tree_orders') = {cast new_character_data_ptr} ∪ set (concat disc_tree_orders)"
apply(auto simp add: ‹disc_tree_orders' = [cast new_character_data_ptr] # foo›)[1]
using ‹set (concat foo) = set (concat disc_tree_orders)› by auto
have "h' ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr) →⇩r to' @ concat disc_tree_orders'"
using ‹h' ⊢ get_owner_document (cast document_ptr) →⇩r document_ptr› disc_nodes_h' to' disc_tree_orders'
by(auto simp add: a_get_scdom_component_def intro!: bind_pure_returns_result_I map_M_pure_I)
then
have "set |h' ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r = set to' ∪ set (concat disc_tree_orders')"
by auto
have "h ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr) →⇩r to @ concat disc_tree_orders"
using ‹h ⊢ get_owner_document (cast document_ptr) →⇩r document_ptr› disc_nodes_document_ptr_h to disc_tree_orders
by(auto simp add: a_get_scdom_component_def intro!: bind_pure_returns_result_I map_M_pure_I)
then
have "set |h ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r = set to ∪ set (concat disc_tree_orders)"
by auto
have "{cast new_character_data_ptr} ∪ set |h ⊢ local.a_get_scdom_component (cast document_ptr)|⇩r =
set |h' ⊢ local.a_get_scdom_component (cast document_ptr)|⇩r"
proof(safe)
show "cast new_character_data_ptr
∈ set |h' ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r"
using ‹h' ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr) →⇩r to' @ concat disc_tree_orders'›
apply(auto simp add: a_get_scdom_component_def)[1]
by (meson ‹⋀thesis. (⋀new_tree_order. ⟦h' ⊢ to_tree_order (cast new_character_data_ptr) →⇩r new_tree_order;
new_tree_order ∈ set disc_tree_orders'⟧ ⟹ thesis) ⟹ thesis› local.to_tree_order_ptr_in_result)
next
fix x
assume " x ∈ set |h ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r"
then
show "x ∈ set |h' ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r"
using ‹set |h ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r =
set to ∪ set (concat disc_tree_orders)›
using ‹set |h' ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r =
set to' ∪ set (concat disc_tree_orders')›
using ‹set to = set to'›
using ‹set (concat disc_tree_orders') = {cast new_character_data_ptr} ∪ set (concat disc_tree_orders)›
by(auto)
next
fix x
assume " x ∈ set |h' ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r"
assume "x ∉ set |h ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r"
show "x = cast new_character_data_ptr"
using ‹set |h ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r =
set to ∪ set (concat disc_tree_orders)›
using ‹set |h' ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r =
set to' ∪ set (concat disc_tree_orders')›
using ‹set to = set to'›
using ‹set (concat disc_tree_orders') = {cast new_character_data_ptr} ∪ set (concat disc_tree_orders)›
using ‹x ∈ set |h' ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r›
‹x ∉ set |h ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r›
by auto
qed
have "object_ptr_kinds h' = object_ptr_kinds h |∪| {|cast new_character_data_ptr|}"
using object_ptr_kinds_eq_h object_ptr_kinds_eq_h2 object_ptr_kinds_eq_h3 by auto
then
show ?thesis
apply(auto simp add: is_strongly_scdom_component_safe_def Let_def)[1]
apply(rule bexI[where x="cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr"])
using ‹{cast⇩c⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩_⇩d⇩a⇩t⇩a⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_character_data_ptr} ∪ set |h ⊢ local.a_get_scdom_component
(cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r = set |h' ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r›
apply auto[2]
using ‹set to = set to'› ‹set |h ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r =
set to ∪ set (concat disc_tree_orders)› local.to_tree_order_ptr_in_result to'
apply auto[1]
using ‹document_ptr |∈| document_ptr_kinds h›
apply blast
apply(rule bexI[where x="cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr"])
using ‹result = new_character_data_ptr› ‹{cast⇩c⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩_⇩d⇩a⇩t⇩a⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_character_data_ptr} ∪
set |h ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r =
set |h' ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r›
apply auto[1]
apply(auto)[1]
using ‹set to = set to'› ‹set |h ⊢ local.a_get_scdom_component (cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr)|⇩r =
set to ∪ set (concat disc_tree_orders)› local.to_tree_order_ptr_in_result to' apply auto[1]
apply (simp add: ‹document_ptr |∈| document_ptr_kinds h›)
using ‹⋀thesis. (⋀new_character_data_ptr h2 h3 disc_nodes_h3. ⟦h ⊢ new_character_data →⇩r new_character_data_ptr;
h ⊢ new_character_data →⇩h h2; h2 ⊢ set_val new_character_data_ptr text →⇩h h3;
h3 ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes_h3;
h3 ⊢ set_disconnected_nodes document_ptr (cast⇩c⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩_⇩d⇩a⇩t⇩a⇩_⇩p⇩t⇩r⇩2⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r new_character_data_ptr # disc_nodes_h3) →⇩h h'⟧ ⟹ thesis) ⟹ thesis›
new_character_data_ptr new_character_data_ptr_not_in_heap
apply auto[1]
using create_character_data_is_strongly_dom_component_safe_step
by (smt (verit) ObjectMonad.ptr_kinds_ptr_kinds_M ‹cast⇩c⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩_⇩d⇩a⇩t⇩a⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_character_data_ptr ∉ set |h ⊢ object_ptr_kinds_M|⇩r›
‹result = new_character_data_ptr› assms(1) assms(2) assms(3) assms(4) assms(5) local.get_scdom_component_impl select_result_I2)
qed
end
interpretation i_get_scdom_component_create_character_data?: l_get_scdom_component_create_character_data⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
get_owner_document heap_is_wellformed parent_child_rel type_wf known_ptr known_ptrs get_scdom_component
is_strongly_scdom_component_safe is_weakly_scdom_component_safe get_dom_component is_strongly_dom_component_safe
is_weakly_dom_component_safe to_tree_order get_parent get_parent_locs get_child_nodes get_child_nodes_locs
get_root_node get_root_node_locs get_ancestors get_ancestors_locs get_element_by_id get_elements_by_class_name
get_elements_by_tag_name set_val set_val_locs get_disconnected_nodes get_disconnected_nodes_locs
set_disconnected_nodes set_disconnected_nodes_locs create_character_data
by(auto simp add: l_get_scdom_component_create_character_data⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def instances)
declare l_get_scdom_component_create_character_data⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]
subsubsection ‹create\_document›
lemma create_document_not_strongly_component_safe:
obtains
h :: "('object_ptr::{equal,linorder}, 'node_ptr::{equal,linorder}, 'element_ptr::{equal,linorder},
'character_data_ptr::{equal,linorder}, 'document_ptr::{equal,linorder}, 'shadow_root_ptr::{equal,linorder},
'Object::{equal,linorder}, 'Node::{equal,linorder}, 'Element::{equal,linorder},
'CharacterData::{equal,linorder}, 'Document::{equal,linorder}) heap" and
h' and new_document_ptr where
"heap_is_wellformed h" and "type_wf h" and "known_ptrs h" and
"h ⊢ create_document →⇩r new_document_ptr →⇩h h'" and
"¬ is_strongly_scdom_component_safe {} {cast new_document_ptr} h h'"
proof -
let ?h0 = "Heap fmempty ::('object_ptr::{equal,linorder}, 'node_ptr::{equal,linorder},
'element_ptr::{equal,linorder}, 'character_data_ptr::{equal,linorder}, 'document_ptr::{equal,linorder},
'shadow_root_ptr::{equal,linorder}, 'Object::{equal,linorder}, 'Node::{equal,linorder},
'Element::{equal,linorder}, 'CharacterData::{equal,linorder}, 'Document::{equal,linorder}) heap"
let ?P = "create_document"
let ?h1 = "|?h0 ⊢ ?P|⇩h"
let ?document_ptr = "|?h0 ⊢ ?P|⇩r"
show thesis
apply(rule that[where h="?h1"])
by code_simp+
qed
locale l_get_scdom_component_create_document⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_dom_component_get_scdom_component +
l_get_dom_component_create_document⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin
lemma create_document_is_weakly_scdom_component_safe:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ create_document →⇩r result"
assumes "h ⊢ create_document →⇩h h'"
shows "is_weakly_scdom_component_safe {} {cast result} h h'"
proof -
have "object_ptr_kinds h' = {|cast result|} |∪| object_ptr_kinds h"
using assms(4) assms(5) local.create_document_def new_document_new_ptr by blast
have "result |∉| document_ptr_kinds h"
using assms(4) assms(5) local.create_document_def new_document_ptr_not_in_heap by auto
show ?thesis
using assms
apply(auto simp add: is_weakly_scdom_component_safe_def Let_def)[1]
using ‹object_ptr_kinds h' = {|cast result|} |∪| object_ptr_kinds h› apply(auto)[1]
apply (simp add: local.create_document_def new_document_ptr_in_heap)
using ‹result |∉| document_ptr_kinds h› apply auto[1]
apply (metis (no_types, lifting) ‹result |∉| document_ptr_kinds h› document_ptr_kinds_commutes
local.create_document_is_weakly_dom_component_safe_step select_result_I2)
done
qed
end
interpretation i_get_scdom_component_create_document?: l_get_scdom_component_create_document⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
get_owner_document heap_is_wellformed parent_child_rel type_wf known_ptr known_ptrs
get_scdom_component is_strongly_scdom_component_safe is_weakly_scdom_component_safe get_dom_component
is_strongly_dom_component_safe is_weakly_dom_component_safe to_tree_order get_parent get_parent_locs
get_child_nodes get_child_nodes_locs get_root_node get_root_node_locs get_ancestors get_ancestors_locs
get_element_by_id get_elements_by_class_name get_elements_by_tag_name create_document
get_disconnected_nodes get_disconnected_nodes_locs
by(auto simp add: l_get_scdom_component_create_document⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def instances)
declare l_get_scdom_component_create_document⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]
subsubsection ‹insert\_before›
locale l_get_dom_component_insert_before⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_set_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_set_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_remove_child⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_adopt_node⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_insert_before⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_append_child⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_owner_document_wf +
l_get_dom_component_get_scdom_component +
l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_insert_before_wf⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_set_child_nodes_get_disconnected_nodes +
l_remove_child +
l_get_root_node_wf +
l_set_disconnected_nodes_get_disconnected_nodes_wf +
l_set_disconnected_nodes_get_ancestors +
l_get_ancestors_wf +
l_get_owner_document +
l_heap_is_wellformed⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin
lemma insert_before_is_component_unsafe:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ insert_before ptr' child ref →⇩h h'"
assumes "ptr ∉ set |h ⊢ get_dom_component ptr'|⇩r"
assumes "ptr ∉ set |h ⊢ get_dom_component (cast child)|⇩r"
assumes "ptr ∉ set |h ⊢ get_dom_component (cast |h ⊢ get_owner_document ptr'|⇩r)|⇩r"
assumes "ptr ∉ set |h ⊢ get_dom_component (cast |h ⊢ get_owner_document (cast child)|⇩r)|⇩r"
shows "preserved (get_M ptr getter) h h'"
proof -
obtain owner_document where owner_document: "h ⊢ get_owner_document (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r child) →⇩r owner_document"
using assms(4)
by(auto simp add: local.adopt_node_def insert_before_def elim!: bind_returns_heap_E
bind_returns_heap_E2[rotated, OF ensure_pre_insertion_validity_pure, rotated]
bind_returns_heap_E2[rotated, OF get_owner_document_pure, rotated] bind_returns_heap_E2[rotated, OF next_sibling_pure, rotated] split: if_splits)
then
obtain c where "h ⊢ get_dom_component (cast owner_document) →⇩r c"
using get_dom_component_ok assms(1) assms(2) assms(3) get_owner_document_owner_document_in_heap
by (meson document_ptr_kinds_commutes select_result_I)
then
have "ptr ≠ cast owner_document"
using assms(6) assms(1) assms(2) assms(3) local.get_dom_component_ptr owner_document
by (metis (no_types, lifting) assms(8) select_result_I2)
obtain owner_document' where owner_document': "h ⊢ get_owner_document ptr' →⇩r owner_document'"
using assms(4)
by(auto simp add: local.adopt_node_def insert_before_def elim!: bind_returns_heap_E
bind_returns_heap_E2[rotated, OF ensure_pre_insertion_validity_pure, rotated]
bind_returns_heap_E2[rotated, OF get_owner_document_pure, rotated]
bind_returns_heap_E2[rotated, OF next_sibling_pure, rotated] split: if_splits)
then
obtain c where "h ⊢ get_dom_component (cast owner_document') →⇩r c"
using get_dom_component_ok assms(1) assms(2) assms(3) get_owner_document_owner_document_in_heap
by (meson document_ptr_kinds_commutes select_result_I)
then
have "ptr ≠ cast owner_document'"
using assms(1) assms(2) assms(3) assms(7) local.get_dom_component_ptr owner_document' by auto
then
have "ptr ≠ cast |h ⊢ get_owner_document ptr'|⇩r"
using owner_document' by auto
have "ptr ≠ ptr'"
by (metis (mono_tags, opaque_lifting) assms(1) assms(2) assms(3) assms(5) assms(7) is_OK_returns_result_I
l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M.get_dom_component_ok l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M.get_dom_component_ptr
l_get_owner_document.get_owner_document_ptr_in_heap local.l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms
local.l_get_owner_document_axioms owner_document' return_returns_result returns_result_select_result)
have "⋀parent. h ⊢ get_parent child →⇩r Some parent ⟹ parent ≠ ptr"
by (meson assms(1) assms(2) assms(3) assms(6) l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M.get_dom_component_ptr
local.get_dom_component_ok local.get_dom_component_to_tree_order local.get_parent_parent_in_heap
local.l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms local.to_tree_order_ok local.to_tree_order_parent
local.to_tree_order_ptr_in_result local.to_tree_order_ptrs_in_heap returns_result_select_result)
then
have "⋀parent. |h ⊢ get_parent child|⇩r = Some parent ⟹ parent ≠ ptr"
by (metis assms(2) assms(3) assms(4) is_OK_returns_heap_I local.get_parent_ok
local.insert_before_child_in_heap select_result_I)
show ?thesis
using insert_before_writes assms(4)
apply(rule reads_writes_preserved2)
apply(auto simp add: insert_before_locs_def adopt_node_locs_def all_args_def)[1]
apply(auto simp add: remove_child_locs_def set_child_nodes_locs_def
set_disconnected_nodes_locs_def all_args_def split: if_splits)[1]
apply (metis ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r |h ⊢ get_owner_document ptr'|⇩r›
get_M_Mdocument_preserved3)
apply(auto simp add: remove_child_locs_def set_child_nodes_locs_def
set_disconnected_nodes_locs_def all_args_def split: if_splits)[1]
apply (metis (no_types, lifting) ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r owner_document›
get_M_Mdocument_preserved3 owner_document select_result_I2)
apply(auto simp add: remove_child_locs_def set_child_nodes_locs_def
set_disconnected_nodes_locs_def all_args_def split: if_splits)[1]
apply (metis ‹ptr ≠ ptr'› document_ptr_casts_commute3 get_M_Mdocument_preserved3)
apply(auto split: option.splits)[1]
apply (metis ‹ptr ≠ ptr'› element_ptr_casts_commute3 get_M_Element_preserved8)
apply(auto simp add: remove_child_locs_def set_child_nodes_locs_def set_disconnected_nodes_locs_def
all_args_def split: if_splits)[1]
apply (metis ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r |h ⊢ get_owner_document ptr'|⇩r› get_M_Mdocument_preserved3)
apply(auto simp add: remove_child_locs_def set_child_nodes_locs_def
set_disconnected_nodes_locs_def all_args_def split: if_splits)[1]
apply (metis (no_types, lifting) ‹⋀parent. |h ⊢ get_parent child|⇩r = Some parent ⟹ parent ≠ ptr›
element_ptr_casts_commute3 get_M_Element_preserved8 node_ptr_casts_commute option.case_eq_if option.collapse)
apply (metis (no_types, lifting) ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r owner_document›
get_M_Mdocument_preserved3 owner_document select_result_I2)
apply (metis ‹⋀parent. |h ⊢ get_parent child|⇩r = Some parent ⟹ parent ≠ ptr›
document_ptr_casts_commute3 get_M_Mdocument_preserved3)
apply (metis (no_types, lifting) ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r owner_document›
get_M_Mdocument_preserved3 owner_document select_result_I2)
apply (metis (no_types, lifting) ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r owner_document›
get_M_Mdocument_preserved3 owner_document select_result_I2)
apply(auto simp add: remove_child_locs_def set_child_nodes_locs_def
set_disconnected_nodes_locs_def all_args_def split: if_splits)[1]
apply (metis ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r |h ⊢ get_owner_document ptr'|⇩r›
get_M_Mdocument_preserved3)
apply(auto simp add: remove_child_locs_def set_child_nodes_locs_def
set_disconnected_nodes_locs_def all_args_def split: if_splits)[1]
apply (metis (no_types, lifting) ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r owner_document›
get_M_Mdocument_preserved3 owner_document select_result_I2)
apply(auto simp add: remove_child_locs_def set_child_nodes_locs_def
set_disconnected_nodes_locs_def all_args_def split: if_splits)[1]
apply (metis ‹ptr ≠ ptr'› document_ptr_casts_commute3 get_M_Mdocument_preserved3)
apply (metis (no_types, lifting) ‹ptr ≠ ptr'› element_ptr_casts_commute3
get_M_Element_preserved8 node_ptr_casts_commute option.case_eq_if option.collapse)
apply(auto simp add: remove_child_locs_def set_child_nodes_locs_def
set_disconnected_nodes_locs_def all_args_def split: if_splits)[1]
by (metis ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r |h ⊢ get_owner_document ptr'|⇩r› get_M_Mdocument_preserved3)
qed
lemma insert_before_is_strongly_dom_component_safe_step:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ insert_before ptr' child ref →⇩h h'"
assumes "ptr ∉ set |h ⊢ get_scdom_component ptr'|⇩r"
assumes "ptr ∉ set |h ⊢ get_scdom_component (cast child)|⇩r"
shows "preserved (get_M ptr getter) h h'"
proof -
have "ptr' |∈| object_ptr_kinds h"
by (meson assms(4) is_OK_returns_heap_I local.insert_before_ptr_in_heap)
then
obtain sc' where sc': "h ⊢ get_scdom_component ptr' →⇩r sc'"
by (meson assms(1) assms(2) assms(3) get_scdom_component_ok is_OK_returns_result_E)
moreover
obtain c' where c': "h ⊢ get_dom_component ptr' →⇩r c'"
by (meson ‹ptr' |∈| object_ptr_kinds h› assms(1) assms(2) assms(3) is_OK_returns_result_E
local.get_dom_component_ok)
ultimately have "set c' ⊆ set sc'"
using assms(1) assms(2) assms(3) get_scdom_component_subset_get_dom_component by blast
have "child |∈| node_ptr_kinds h"
by (meson assms(4) is_OK_returns_heap_I local.insert_before_child_in_heap)
then
obtain child_sc where child_sc: "h ⊢ get_scdom_component (cast child) →⇩r child_sc"
by (meson assms(1) assms(2) assms(3) get_scdom_component_ok is_OK_returns_result_E
node_ptr_kinds_commutes)
moreover
obtain child_c where child_c: "h ⊢ get_dom_component (cast child) →⇩r child_c"
by (meson ‹child |∈| node_ptr_kinds h› assms(1) assms(2) assms(3) is_OK_returns_result_E
local.get_dom_component_ok node_ptr_kinds_commutes)
ultimately have "set child_c ⊆ set child_sc"
using assms(1) assms(2) assms(3) get_scdom_component_subset_get_dom_component by blast
obtain ptr'_owner_document where ptr'_owner_document: "h ⊢ get_owner_document ptr' →⇩r ptr'_owner_document"
by (meson ‹set c' ⊆ set sc'› assms(1) assms(2) assms(3) c' get_scdom_component_owner_document_same
local.get_dom_component_ptr sc' subset_code(1))
then
have "h ⊢ get_scdom_component (cast ptr'_owner_document) →⇩r sc'"
by (metis (no_types, lifting) ‹set c' ⊆ set sc'› assms(1) assms(2) assms(3) c'
get_scdom_component_owner_document_same get_scdom_component_ptrs_same_scope_component
local.get_dom_component_ptr sc' select_result_I2 subset_code(1))
moreover
obtain ptr'_owner_document_c where ptr'_owner_document_c:
"h ⊢ get_dom_component (cast ptr'_owner_document) →⇩r ptr'_owner_document_c"
by (meson assms(1) assms(2) assms(3) document_ptr_kinds_commutes is_OK_returns_result_E
local.get_dom_component_ok local.get_owner_document_owner_document_in_heap ptr'_owner_document)
ultimately have "set ptr'_owner_document_c ⊆ set sc'"
using assms(1) assms(2) assms(3) get_scdom_component_subset_get_dom_component by blast
obtain child_owner_document where child_owner_document: "h ⊢ get_owner_document (cast child) →⇩r child_owner_document"
by (meson ‹set child_c ⊆ set child_sc› assms(1) assms(2) assms(3) child_c child_sc
get_scdom_component_owner_document_same local.get_dom_component_ptr subset_code(1))
have "child_owner_document |∈| document_ptr_kinds h"
using assms(1) assms(2) assms(3) child_owner_document local.get_owner_document_owner_document_in_heap
by blast
then
have "h ⊢ get_scdom_component (cast child_owner_document) →⇩r child_sc"
using get_scdom_component_ok assms(1) assms(2) assms(3) child_sc
by (metis (no_types, lifting) ‹set child_c ⊆ set child_sc› child_c child_owner_document
get_scdom_component_owner_document_same get_scdom_component_ptrs_same_scope_component
local.get_dom_component_ptr returns_result_eq set_mp)
moreover
obtain child_owner_document_c where child_owner_document_c:
"h ⊢ get_dom_component (cast child_owner_document) →⇩r child_owner_document_c"
by (meson assms(1) assms(2) assms(3) child_owner_document document_ptr_kinds_commutes
is_OK_returns_result_E local.get_dom_component_ok local.get_owner_document_owner_document_in_heap)
ultimately have "set child_owner_document_c ⊆ set child_sc"
using assms(1) assms(2) assms(3) get_scdom_component_subset_get_dom_component by blast
have "ptr ∉ set |h ⊢ get_dom_component ptr'|⇩r"
using ‹set c' ⊆ set sc'› assms(5) c' sc' by auto
moreover have "ptr ∉ set |h ⊢ get_dom_component (cast child)|⇩r"
using ‹set child_c ⊆ set child_sc› assms(6) child_c child_sc by auto
moreover have "ptr ∉ set |h ⊢ get_dom_component (cast |h ⊢ get_owner_document ptr'|⇩r)|⇩r"
using ‹set ptr'_owner_document_c ⊆ set sc'› assms(5) ptr'_owner_document ptr'_owner_document_c sc'
by auto
moreover have "ptr ∉ set |h ⊢ get_dom_component (cast |h ⊢ get_owner_document (cast child)|⇩r)|⇩r"
using ‹set child_owner_document_c ⊆ set child_sc› assms(6) child_owner_document child_owner_document_c
child_sc by auto
ultimately show ?thesis
using assms insert_before_is_component_unsafe
by blast
qed
lemma insert_before_is_strongly_dom_component_safe:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ insert_before ptr node child →⇩h h'"
shows "is_strongly_scdom_component_safe ({ptr, cast node} ∪ (case child of Some ref ⇒ {cast ref} | None ⇒ {} )) {} h h'"
proof -
obtain ancestors reference_child owner_document h2 h3 disconnected_nodes_h2 where
ancestors: "h ⊢ get_ancestors ptr →⇩r ancestors" and
node_not_in_ancestors: "cast node ∉ set ancestors" and
reference_child:
"h ⊢ (if Some node = child then a_next_sibling node else return child) →⇩r reference_child" and
owner_document: "h ⊢ get_owner_document ptr →⇩r owner_document" and
h2: "h ⊢ adopt_node owner_document node →⇩h h2" and
disconnected_nodes_h2: "h2 ⊢ get_disconnected_nodes owner_document →⇩r disconnected_nodes_h2" and
h3: "h2 ⊢ set_disconnected_nodes owner_document (remove1 node disconnected_nodes_h2) →⇩h h3" and
h': "h3 ⊢ a_insert_node ptr node reference_child →⇩h h'"
using assms(4)
by(auto simp add: insert_before_def a_ensure_pre_insertion_validity_def
elim!: bind_returns_heap_E bind_returns_result_E
bind_returns_heap_E2[rotated, OF get_parent_pure, rotated]
bind_returns_heap_E2[rotated, OF get_child_nodes_pure, rotated]
bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated]
bind_returns_heap_E2[rotated, OF get_ancestors_pure, rotated]
bind_returns_heap_E2[rotated, OF next_sibling_pure, rotated]
bind_returns_heap_E2[rotated, OF get_owner_document_pure, rotated]
split: if_splits option.splits)
have object_ptr_kinds_M_eq3_h: "object_ptr_kinds h = object_ptr_kinds h2"
apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h = object_ptr_kinds h'",
OF adopt_node_writes h2])
using adopt_node_pointers_preserved
apply blast
by (auto simp add: reflp_def transp_def)
then have object_ptr_kinds_M_eq_h: "⋀ptrs. h ⊢ object_ptr_kinds_M →⇩r ptrs = h2 ⊢ object_ptr_kinds_M →⇩r ptrs"
by(simp add: object_ptr_kinds_M_defs )
then have object_ptr_kinds_M_eq2_h: "|h ⊢ object_ptr_kinds_M|⇩r = |h2 ⊢ object_ptr_kinds_M|⇩r"
by simp
then have node_ptr_kinds_eq2_h: "|h ⊢ node_ptr_kinds_M|⇩r = |h2 ⊢ node_ptr_kinds_M|⇩r"
using node_ptr_kinds_M_eq by blast
have "known_ptrs h2"
using assms(3) object_ptr_kinds_M_eq3_h known_ptrs_preserved by blast
have wellformed_h2: "heap_is_wellformed h2"
using adopt_node_preserves_wellformedness[OF assms(1) h2] assms(3) assms(2) .
have object_ptr_kinds_M_eq3_h2: "object_ptr_kinds h2 = object_ptr_kinds h3"
apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h = object_ptr_kinds h'",
OF set_disconnected_nodes_writes h3])
unfolding a_remove_child_locs_def
using set_disconnected_nodes_pointers_preserved
by (auto simp add: reflp_def transp_def)
then have object_ptr_kinds_M_eq_h2: "⋀ptrs. h2 ⊢ object_ptr_kinds_M →⇩r ptrs = h3 ⊢ object_ptr_kinds_M →⇩r ptrs"
by(simp add: object_ptr_kinds_M_defs)
then have object_ptr_kinds_M_eq2_h2: "|h2 ⊢ object_ptr_kinds_M|⇩r = |h3 ⊢ object_ptr_kinds_M|⇩r"
by simp
then have node_ptr_kinds_eq2_h2: "|h2 ⊢ node_ptr_kinds_M|⇩r = |h3 ⊢ node_ptr_kinds_M|⇩r"
using node_ptr_kinds_M_eq by blast
have document_ptr_kinds_eq2_h2: "|h2 ⊢ document_ptr_kinds_M|⇩r = |h3 ⊢ document_ptr_kinds_M|⇩r"
using object_ptr_kinds_M_eq2_h2 document_ptr_kinds_M_eq by auto
have "known_ptrs h3"
using object_ptr_kinds_M_eq3_h2 known_ptrs_preserved ‹known_ptrs h2› by blast
have object_ptr_kinds_M_eq3_h': "object_ptr_kinds h3 = object_ptr_kinds h'"
apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h = object_ptr_kinds h'",
OF insert_node_writes h'])
unfolding a_remove_child_locs_def
using set_child_nodes_pointers_preserved
by (auto simp add: reflp_def transp_def)
then have object_ptr_kinds_M_eq_h3:
"⋀ptrs. h3 ⊢ 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_M_eq2_h3:
"|h3 ⊢ object_ptr_kinds_M|⇩r = |h' ⊢ object_ptr_kinds_M|⇩r"
by simp
then have node_ptr_kinds_eq2_h3: "|h3 ⊢ node_ptr_kinds_M|⇩r = |h' ⊢ node_ptr_kinds_M|⇩r"
using node_ptr_kinds_M_eq by blast
have document_ptr_kinds_eq2_h3: "|h3 ⊢ document_ptr_kinds_M|⇩r = |h' ⊢ document_ptr_kinds_M|⇩r"
using object_ptr_kinds_M_eq2_h3 document_ptr_kinds_M_eq by auto
have "object_ptr_kinds h = object_ptr_kinds h'"
by (simp add: object_ptr_kinds_M_eq3_h object_ptr_kinds_M_eq3_h' object_ptr_kinds_M_eq3_h2)
then
show ?thesis
using assms
apply(auto simp add: is_strongly_scdom_component_safe_def)[1]
using insert_before_is_strongly_dom_component_safe_step local.get_scdom_component_impl by blast
qed
lemma append_child_is_strongly_dom_component_safe_step:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ append_child ptr' child →⇩h h'"
assumes "ptr ∉ set |h ⊢ get_scdom_component ptr'|⇩r"
assumes "ptr ∉ set |h ⊢ get_scdom_component (cast child)|⇩r"
shows "preserved (get_M ptr getter) h h'"
by (metis assms(1) assms(2) assms(3) assms(4) assms(5) assms(6)
insert_before_is_strongly_dom_component_safe_step local.append_child_def)
lemma append_child_is_strongly_dom_component_safe:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ append_child ptr child →⇩h h'"
shows "is_strongly_scdom_component_safe {ptr, cast child} {} h h'"
using assms unfolding append_child_def
using insert_before_is_strongly_dom_component_safe
by fastforce
end
interpretation i_get_dom_component_insert_before?: l_get_dom_component_insert_before⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
heap_is_wellformed parent_child_rel type_wf known_ptr known_ptrs to_tree_order get_parent
get_parent_locs get_child_nodes get_child_nodes_locs get_dom_component is_strongly_dom_component_safe
is_weakly_dom_component_safe get_root_node get_root_node_locs get_ancestors get_ancestors_locs
get_disconnected_nodes get_disconnected_nodes_locs get_element_by_id get_elements_by_class_name
get_elements_by_tag_name set_child_nodes set_child_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs
get_owner_document remove_child remove_child_locs remove adopt_node adopt_node_locs insert_before
insert_before_locs append_child get_scdom_component is_strongly_scdom_component_safe
is_weakly_scdom_component_safe
by(auto simp add: l_get_dom_component_insert_before⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def instances)
declare l_get_dom_component_insert_before⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]
subsubsection ‹get\_owner\_document›
locale l_get_owner_document_scope_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_owner_document_wf⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_dom_component_get_scdom_component +
l_get_owner_document_wf_get_root_node_wf
begin
lemma get_owner_document_is_strongly_scdom_component_safe_step:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ get_scdom_component ptr →⇩r sc"
assumes "h ⊢ get_owner_document ptr' →⇩r owner_document"
shows "cast owner_document ∈ set sc ⟷ ptr' ∈ set sc"
proof -
have "h ⊢ get_owner_document (cast owner_document) →⇩r owner_document"
by (metis assms(1) assms(2) assms(3) assms(5) cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r_inject
document_ptr_casts_commute3 document_ptr_document_ptr_cast document_ptr_kinds_commutes
local.get_owner_document_owner_document_in_heap local.get_root_node_document
local.get_root_node_not_node_same node_ptr_no_document_ptr_cast)
then show ?thesis
using assms
using bind_returns_result_E contra_subsetD get_scdom_component_ok
get_scdom_component_ptrs_same_scope_component get_scdom_component_subset_get_dom_component
is_OK_returns_result_E is_OK_returns_result_I local.get_dom_component_ok local.get_dom_component_ptr
local.get_owner_document_ptr_in_heap local.get_owner_document_pure local.get_scdom_component_def
pure_returns_heap_eq returns_result_eq
by (smt (verit) local.get_scdom_component_ptrs_same_owner_document subsetD)
qed
lemma get_owner_document_is_strongly_scdom_component_safe:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h ⊢ get_owner_document ptr →⇩r owner_document"
assumes "h ⊢ get_owner_document ptr →⇩h h'"
shows "is_strongly_scdom_component_safe {ptr} {cast owner_document} h h'"
proof -
have "h = h'"
by (meson assms(5) local.get_owner_document_pure pure_returns_heap_eq)
then show ?thesis
using assms
apply(auto simp add: is_strongly_scdom_component_safe_def Let_def preserved_def)[1]
by (smt (verit) get_owner_document_is_strongly_scdom_component_safe_step inf.orderE is_OK_returns_result_I
local.get_dom_component_ok local.get_dom_component_to_tree_order_subset local.get_owner_document_ptr_in_heap
local.get_scdom_component_impl local.get_scdom_component_ok local.get_scdom_component_ptr_in_heap
local.get_scdom_component_subset_get_dom_component local.to_tree_order_ok
local.to_tree_order_ptr_in_result returns_result_select_result subset_eq)
qed
end
interpretation i_get_owner_document_scope_component?: l_get_owner_document_scope_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
get_scdom_component is_strongly_scdom_component_safe is_weakly_scdom_component_safe
get_owner_document get_disconnected_nodes get_disconnected_nodes_locs to_tree_order known_ptr
known_ptrs type_wf heap_is_wellformed parent_child_rel get_child_nodes get_child_nodes_locs
get_parent get_parent_locs get_ancestors get_ancestors_locs get_root_node get_root_node_locs
get_dom_component is_strongly_dom_component_safe is_weakly_dom_component_safe get_element_by_id
get_elements_by_class_name get_elements_by_tag_name
by(auto simp add: l_get_owner_document_scope_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def instances)
declare l_get_owner_document_scope_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]
end