Theory Core_DOM_Functions
section‹Querying and Modifying the DOM›
text‹In this theory, we are formalizing the functions for querying and modifying
the DOM.›
theory Core_DOM_Functions
imports
"monads/DocumentMonad"
begin
text ‹If we do not declare show\_variants, then all abbreviations that contain
constants that are overloaded by using adhoc\_overloading get immediately unfolded.›
declare [[show_variants]]
subsection ‹Various Functions›
lemma insort_split: "x ∈ set (insort y xs) ⟷ (x = y ∨ x ∈ set xs)"
apply(induct xs)
by(auto)
lemma concat_map_distinct:
"distinct (concat (map f xs)) ⟹ y ∈ set (concat (map f xs)) ⟹ ∃!x ∈ set xs. y ∈ set (f x)"
apply(induct xs)
by(auto)
lemma concat_map_all_distinct: "distinct (concat (map f xs)) ⟹ x ∈ set xs ⟹ distinct (f x)"
apply(induct xs)
by(auto)
lemma distinct_concat_map_I:
assumes "distinct xs"
and "⋀x. x ∈ set xs ⟹ distinct (f x)"
and "⋀x y. x ∈ set xs ⟹ y ∈ set xs ⟹ x ≠ y ⟹ (set (f x)) ∩ (set (f y)) = {}"
shows "distinct (concat ((map f xs)))"
using assms
apply(induct xs)
by(auto)
lemma distinct_concat_map_E:
assumes "distinct (concat ((map f xs)))"
shows "⋀x y. x ∈ set xs ⟹ y ∈ set xs ⟹ x ≠ y ⟹ (set (f x)) ∩ (set (f y)) = {}"
and "⋀x. x ∈ set xs ⟹ distinct (f x)"
using assms
apply(induct xs)
by(auto)
lemma bind_is_OK_E3 [elim]:
assumes "h ⊢ ok (f ⤜ g)" and "pure f h"
obtains x where "h ⊢ f →⇩r x" and "h ⊢ ok (g x)"
using assms
by(auto simp add: bind_def returns_result_def returns_heap_def is_OK_def execute_def pure_def
split: sum.splits)
subsection ‹Basic Functions›
subsubsection ‹get\_child\_nodes›
locale l_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs
begin
definition get_child_nodes⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r :: "(_) element_ptr ⇒ unit ⇒ (_, (_) node_ptr list) dom_prog"
where
"get_child_nodes⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r element_ptr _ = get_M element_ptr RElement.child_nodes"
definition get_child_nodes⇩c⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩_⇩d⇩a⇩t⇩a⇩_⇩p⇩t⇩r :: "(_) character_data_ptr ⇒ unit ⇒ (_, (_) node_ptr list) dom_prog"
where
"get_child_nodes⇩c⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩_⇩d⇩a⇩t⇩a⇩_⇩p⇩t⇩r _ _ = return []"
definition get_child_nodes⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r :: "(_) document_ptr ⇒ unit ⇒ (_, (_) node_ptr list) dom_prog"
where
"get_child_nodes⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r document_ptr _ = do {
doc_elem ← get_M document_ptr document_element;
(case doc_elem of
Some element_ptr ⇒ return [cast element_ptr]
| None ⇒ return [])
}"
definition a_get_child_nodes_tups :: "(((_) object_ptr ⇒ bool) × ((_) object_ptr ⇒ unit
⇒ (_, (_) node_ptr list) dom_prog)) list"
where
"a_get_child_nodes_tups = [
(is_element_ptr, get_child_nodes⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r ∘ the ∘ cast),
(is_character_data_ptr, get_child_nodes⇩c⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩_⇩d⇩a⇩t⇩a⇩_⇩p⇩t⇩r ∘ the ∘ cast),
(is_document_ptr, get_child_nodes⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r ∘ the ∘ cast)
]"
definition a_get_child_nodes :: "(_) object_ptr ⇒ (_, (_) node_ptr list) dom_prog"
where
"a_get_child_nodes ptr = invoke a_get_child_nodes_tups ptr ()"
definition a_get_child_nodes_locs :: "(_) object_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
where
"a_get_child_nodes_locs ptr ≡
(if is_element_ptr_kind ptr then {preserved (get_M (the (cast ptr)) RElement.child_nodes)} else {}) ∪
(if is_document_ptr_kind ptr then {preserved (get_M (the (cast ptr)) RDocument.document_element)} else {}) ∪
{preserved (get_M ptr RObject.nothing)}"
definition first_child :: "(_) object_ptr ⇒ (_, (_) node_ptr option) dom_prog"
where
"first_child ptr = do {
children ← a_get_child_nodes ptr;
return (case children of [] ⇒ None | child#_ ⇒ Some child)}"
end
locale l_get_child_nodes_defs =
fixes get_child_nodes :: "(_) object_ptr ⇒ (_, (_) node_ptr list) dom_prog"
fixes get_child_nodes_locs :: "(_) object_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
locale l_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_type_wf type_wf +
l_known_ptr known_ptr +
l_get_child_nodes_defs get_child_nodes get_child_nodes_locs +
l_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs
for type_wf :: "(_) heap ⇒ bool"
and known_ptr :: "(_) object_ptr ⇒ bool"
and get_child_nodes :: "(_) object_ptr ⇒ (_, (_) node_ptr list) dom_prog"
and get_child_nodes_locs :: "(_) object_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set" +
assumes known_ptr_impl: "known_ptr = DocumentClass.known_ptr"
assumes type_wf_impl: "type_wf = DocumentClass.type_wf"
assumes get_child_nodes_impl: "get_child_nodes = a_get_child_nodes"
assumes get_child_nodes_locs_impl: "get_child_nodes_locs = a_get_child_nodes_locs"
begin
lemmas get_child_nodes_def = get_child_nodes_impl[unfolded a_get_child_nodes_def]
lemmas get_child_nodes_locs_def = get_child_nodes_locs_impl[unfolded a_get_child_nodes_locs_def]
lemma get_child_nodes_split:
"P (invoke (a_get_child_nodes_tups @ xs) ptr ()) =
((known_ptr ptr ⟶ P (get_child_nodes ptr))
∧ (¬(known_ptr ptr) ⟶ P (invoke xs ptr ())))"
by(auto simp add: known_ptr_impl get_child_nodes_impl a_get_child_nodes_def a_get_child_nodes_tups_def
known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs
NodeClass.known_ptr_defs
split: invoke_splits)
lemma get_child_nodes_split_asm:
"P (invoke (a_get_child_nodes_tups @ xs) ptr ()) =
(¬((known_ptr ptr ∧ ¬P (get_child_nodes ptr))
∨ (¬(known_ptr ptr) ∧ ¬P (invoke xs ptr ()))))"
by(auto simp add: known_ptr_impl get_child_nodes_impl a_get_child_nodes_def
a_get_child_nodes_tups_def known_ptr_defs CharacterDataClass.known_ptr_defs
ElementClass.known_ptr_defs NodeClass.known_ptr_defs
split: invoke_splits)
lemmas get_child_nodes_splits = get_child_nodes_split get_child_nodes_split_asm
lemma get_child_nodes_ok [simp]:
assumes "known_ptr ptr"
assumes "type_wf h"
assumes "ptr |∈| object_ptr_kinds h"
shows "h ⊢ ok (get_child_nodes ptr)"
using assms(1) assms(2) assms(3)
apply(auto simp add: known_ptr_impl type_wf_impl get_child_nodes_def a_get_child_nodes_tups_def)[1]
apply(split invoke_splits, rule conjI)+
apply((rule impI)+, drule(1) known_ptr_not_document_ptr, drule(1) known_ptr_not_character_data_ptr,
drule(1) known_ptr_not_element_ptr)
apply(auto simp add: NodeClass.known_ptr_defs)[1]
apply(auto simp add: get_child_nodes⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def dest: get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_ok
split: list.splits option.splits intro!: bind_is_OK_I2)[1]
apply(auto simp add: get_child_nodes⇩c⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩_⇩d⇩a⇩t⇩a⇩_⇩p⇩t⇩r_def)[1]
apply (auto simp add: get_child_nodes⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def CharacterDataClass.type_wf_defs
DocumentClass.type_wf_defs intro!: bind_is_OK_I2 split: option.splits)[1]
using get_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t_ok ‹type_wf h›[unfolded type_wf_impl] by blast
lemma get_child_nodes_ptr_in_heap [simp]:
assumes "h ⊢ get_child_nodes ptr →⇩r children"
shows "ptr |∈| object_ptr_kinds h"
using assms
by(auto simp add: get_child_nodes_impl a_get_child_nodes_def invoke_ptr_in_heap
dest: is_OK_returns_result_I)
lemma get_child_nodes_pure [simp]:
"pure (get_child_nodes ptr) h"
apply (auto simp add: get_child_nodes_impl a_get_child_nodes_def a_get_child_nodes_tups_def)[1]
apply(split invoke_splits, rule conjI)+
by(auto simp add: get_child_nodes⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def get_child_nodes⇩c⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩_⇩d⇩a⇩t⇩a⇩_⇩p⇩t⇩r_def
get_child_nodes⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def intro!: bind_pure_I split: option.splits)
lemma get_child_nodes_reads: "reads (get_child_nodes_locs ptr) (get_child_nodes ptr) h h'"
apply(simp add: get_child_nodes_locs_impl get_child_nodes_impl a_get_child_nodes_def
a_get_child_nodes_tups_def a_get_child_nodes_locs_def)
apply(split invoke_splits, rule conjI)+
apply(auto)[1]
apply(auto simp add: get_child_nodes⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def intro: reads_subset[OF reads_singleton]
reads_subset[OF check_in_heap_reads]
intro!: reads_bind_pure reads_subset[OF return_reads] split: option.splits)[1]
apply(auto simp add: get_child_nodes⇩c⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩_⇩d⇩a⇩t⇩a⇩_⇩p⇩t⇩r_def intro: reads_subset[OF check_in_heap_reads]
intro!: reads_bind_pure reads_subset[OF return_reads] )[1]
apply(auto simp add: get_child_nodes⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def intro: reads_subset[OF reads_singleton]
reads_subset[OF check_in_heap_reads] intro!: reads_bind_pure reads_subset[OF return_reads]
split: option.splits)[1]
done
end
locale l_get_child_nodes = l_type_wf + l_known_ptr + l_get_child_nodes_defs +
assumes get_child_nodes_reads: "reads (get_child_nodes_locs ptr) (get_child_nodes ptr) h h'"
assumes get_child_nodes_ok: "type_wf h ⟹ known_ptr ptr ⟹ ptr |∈| object_ptr_kinds h
⟹ h ⊢ ok (get_child_nodes ptr)"
assumes get_child_nodes_ptr_in_heap: "h ⊢ ok (get_child_nodes ptr) ⟹ ptr |∈| object_ptr_kinds h"
assumes get_child_nodes_pure [simp]: "pure (get_child_nodes ptr) h"
global_interpretation l_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs defines
get_child_nodes = l_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs.a_get_child_nodes and
get_child_nodes_locs = l_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs.a_get_child_nodes_locs
.
interpretation
i_get_child_nodes?: l_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf known_ptr get_child_nodes get_child_nodes_locs
by(auto simp add: l_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def get_child_nodes_def get_child_nodes_locs_def)
declare l_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
lemma get_child_nodes_is_l_get_child_nodes [instances]:
"l_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs"
apply(unfold_locales)
using get_child_nodes_reads get_child_nodes_ok get_child_nodes_ptr_in_heap get_child_nodes_pure
by blast+
paragraph ‹new\_element›
locale l_new_element_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf known_ptr get_child_nodes get_child_nodes_locs
for type_wf :: "(_) heap ⇒ bool"
and known_ptr :: "(_) object_ptr ⇒ bool"
and get_child_nodes :: "(_) object_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locs :: "(_) object_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
begin
lemma get_child_nodes_new_element:
"ptr' ≠ cast new_element_ptr ⟹ h ⊢ new_element →⇩r new_element_ptr ⟹ h ⊢ new_element →⇩h h'
⟹ r ∈ get_child_nodes_locs ptr' ⟹ r h h'"
by (auto simp add: get_child_nodes_locs_def new_element_get_M⇩O⇩b⇩j⇩e⇩c⇩t new_element_get_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t
new_element_get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t split: prod.splits if_splits option.splits
elim!: bind_returns_result_E bind_returns_heap_E intro: is_element_ptr_kind_obtains)
lemma new_element_no_child_nodes:
"h ⊢ new_element →⇩r new_element_ptr ⟹ h ⊢ new_element →⇩h h'
⟹ h' ⊢ get_child_nodes (cast new_element_ptr) →⇩r []"
apply(auto simp add: get_child_nodes_def a_get_child_nodes_tups_def
split: prod.splits elim!: bind_returns_result_E bind_returns_heap_E)[1]
apply(split invoke_splits, rule conjI)+
apply(auto intro: new_element_is_element_ptr)[1]
by(auto simp add: new_element_ptr_in_heap get_child_nodes⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def check_in_heap_def
new_element_child_nodes intro!: bind_pure_returns_result_I
intro: new_element_is_element_ptr elim!: new_element_ptr_in_heap)
end
locale l_new_element_get_child_nodes = l_new_element + l_get_child_nodes +
assumes get_child_nodes_new_element:
"ptr' ≠ cast new_element_ptr ⟹ h ⊢ new_element →⇩r new_element_ptr
⟹ h ⊢ new_element →⇩h h' ⟹ r ∈ get_child_nodes_locs ptr' ⟹ r h h'"
assumes new_element_no_child_nodes:
"h ⊢ new_element →⇩r new_element_ptr ⟹ h ⊢ new_element →⇩h h'
⟹ h' ⊢ get_child_nodes (cast new_element_ptr) →⇩r []"
interpretation i_new_element_get_child_nodes?:
l_new_element_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf known_ptr get_child_nodes get_child_nodes_locs
by(unfold_locales)
declare l_new_element_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
lemma new_element_get_child_nodes_is_l_new_element_get_child_nodes [instances]:
"l_new_element_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs"
using new_element_is_l_new_element get_child_nodes_is_l_get_child_nodes
apply(auto simp add: l_new_element_get_child_nodes_def l_new_element_get_child_nodes_axioms_def)[1]
using get_child_nodes_new_element new_element_no_child_nodes
by fast+
paragraph ‹new\_character\_data›
locale l_new_character_data_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf known_ptr get_child_nodes get_child_nodes_locs
for type_wf :: "(_) heap ⇒ bool"
and known_ptr :: "(_) object_ptr ⇒ bool"
and get_child_nodes :: "(_) object_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locs :: "(_) object_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
begin
lemma get_child_nodes_new_character_data:
"ptr' ≠ cast new_character_data_ptr ⟹ h ⊢ new_character_data →⇩r new_character_data_ptr
⟹ h ⊢ new_character_data →⇩h h' ⟹ r ∈ get_child_nodes_locs ptr' ⟹ r h h'"
by (auto simp add: get_child_nodes_locs_def new_character_data_get_M⇩O⇩b⇩j⇩e⇩c⇩t
new_character_data_get_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t new_character_data_get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t
split: prod.splits if_splits option.splits
elim!: bind_returns_result_E bind_returns_heap_E
intro: is_character_data_ptr_kind_obtains)
lemma new_character_data_no_child_nodes:
"h ⊢ new_character_data →⇩r new_character_data_ptr ⟹ h ⊢ new_character_data →⇩h h'
⟹ h' ⊢ get_child_nodes (cast new_character_data_ptr) →⇩r []"
apply(auto simp add: get_child_nodes_def a_get_child_nodes_tups_def
split: prod.splits elim!: bind_returns_result_E bind_returns_heap_E)[1]
apply(split invoke_splits, rule conjI)+
apply(auto intro: new_character_data_is_character_data_ptr)[1]
by(auto simp add: new_character_data_ptr_in_heap get_child_nodes⇩c⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩_⇩d⇩a⇩t⇩a⇩_⇩p⇩t⇩r_def
check_in_heap_def new_character_data_child_nodes
intro!: bind_pure_returns_result_I
intro: new_character_data_is_character_data_ptr elim!: new_character_data_ptr_in_heap)
end
locale l_new_character_data_get_child_nodes = l_new_character_data + l_get_child_nodes +
assumes get_child_nodes_new_character_data:
"ptr' ≠ cast new_character_data_ptr ⟹ h ⊢ new_character_data →⇩r new_character_data_ptr
⟹ h ⊢ new_character_data →⇩h h' ⟹ r ∈ get_child_nodes_locs ptr' ⟹ r h h'"
assumes new_character_data_no_child_nodes:
"h ⊢ new_character_data →⇩r new_character_data_ptr ⟹ h ⊢ new_character_data →⇩h h'
⟹ h' ⊢ get_child_nodes (cast new_character_data_ptr) →⇩r []"
interpretation i_new_character_data_get_child_nodes?:
l_new_character_data_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf known_ptr get_child_nodes get_child_nodes_locs
by(unfold_locales)
declare l_new_character_data_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
lemma new_character_data_get_child_nodes_is_l_new_character_data_get_child_nodes [instances]:
"l_new_character_data_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs"
using new_character_data_is_l_new_character_data get_child_nodes_is_l_get_child_nodes
apply(simp add: l_new_character_data_get_child_nodes_def l_new_character_data_get_child_nodes_axioms_def)
using get_child_nodes_new_character_data new_character_data_no_child_nodes
by fast
paragraph ‹new\_document›
locale l_new_document_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf known_ptr get_child_nodes get_child_nodes_locs
for type_wf :: "(_) heap ⇒ bool"
and known_ptr :: "(_) object_ptr ⇒ bool"
and get_child_nodes :: "(_) object_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locs :: "(_) object_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
begin
lemma get_child_nodes_new_document:
"ptr' ≠ cast new_document_ptr ⟹ h ⊢ new_document →⇩r new_document_ptr
⟹ h ⊢ new_document →⇩h h' ⟹ r ∈ get_child_nodes_locs ptr' ⟹ r h h'"
by (auto simp add: get_child_nodes_locs_def new_document_get_M⇩O⇩b⇩j⇩e⇩c⇩t new_document_get_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t
new_document_get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t split: prod.splits if_splits option.splits
elim!: bind_returns_result_E bind_returns_heap_E
intro: is_document_ptr_kind_obtains)
lemma new_document_no_child_nodes:
"h ⊢ new_document →⇩r new_document_ptr ⟹ h ⊢ new_document →⇩h h'
⟹ h' ⊢ get_child_nodes (cast new_document_ptr) →⇩r []"
apply(auto simp add: get_child_nodes_def a_get_child_nodes_tups_def
split: prod.splits
elim!: bind_returns_result_E bind_returns_heap_E)[1]
apply(split invoke_splits, rule conjI)+
apply(auto intro: new_document_is_document_ptr)[1]
by(auto simp add: new_document_ptr_in_heap get_child_nodes⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def check_in_heap_def
new_document_document_element
intro!: bind_pure_returns_result_I
intro: new_document_is_document_ptr elim!: new_document_ptr_in_heap split: option.splits)
end
locale l_new_document_get_child_nodes = l_new_document + l_get_child_nodes +
assumes get_child_nodes_new_document:
"ptr' ≠ cast new_document_ptr ⟹ h ⊢ new_document →⇩r new_document_ptr
⟹ h ⊢ new_document →⇩h h' ⟹ r ∈ get_child_nodes_locs ptr' ⟹ r h h'"
assumes new_document_no_child_nodes:
"h ⊢ new_document →⇩r new_document_ptr ⟹ h ⊢ new_document →⇩h h'
⟹ h' ⊢ get_child_nodes (cast new_document_ptr) →⇩r []"
interpretation i_new_document_get_child_nodes?:
l_new_document_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf known_ptr get_child_nodes get_child_nodes_locs
by(unfold_locales)
declare l_new_document_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
lemma new_document_get_child_nodes_is_l_new_document_get_child_nodes [instances]:
"l_new_document_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs"
using new_document_is_l_new_document get_child_nodes_is_l_get_child_nodes
apply(simp add: l_new_document_get_child_nodes_def l_new_document_get_child_nodes_axioms_def)
using get_child_nodes_new_document new_document_no_child_nodes
by fast
subsubsection ‹set\_child\_nodes›
locale l_set_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs
begin
definition set_child_nodes⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r ::
"(_) element_ptr ⇒ (_) node_ptr list ⇒ (_, unit) dom_prog"
where
"set_child_nodes⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r element_ptr children = put_M element_ptr RElement.child_nodes_update children"
definition set_child_nodes⇩c⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩_⇩d⇩a⇩t⇩a⇩_⇩p⇩t⇩r ::
"(_) character_data_ptr ⇒ (_) node_ptr list ⇒ (_, unit) dom_prog"
where
"set_child_nodes⇩c⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩_⇩d⇩a⇩t⇩a⇩_⇩p⇩t⇩r _ _ = error HierarchyRequestError"
definition set_child_nodes⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r :: "(_) document_ptr ⇒ (_) node_ptr list ⇒ (_, unit) dom_prog"
where
"set_child_nodes⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r document_ptr children = do {
(case children of
[] ⇒ put_M document_ptr document_element_update None
| child # [] ⇒ (case cast child of
Some element_ptr ⇒ put_M document_ptr document_element_update (Some element_ptr)
| None ⇒ error HierarchyRequestError)
| _ ⇒ error HierarchyRequestError)
}"
definition a_set_child_nodes_tups ::
"(((_) object_ptr ⇒ bool) × ((_) object_ptr ⇒ (_) node_ptr list ⇒ (_, unit) dom_prog)) list"
where
"a_set_child_nodes_tups ≡ [
(is_element_ptr, set_child_nodes⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r ∘ the ∘ cast),
(is_character_data_ptr, set_child_nodes⇩c⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩_⇩d⇩a⇩t⇩a⇩_⇩p⇩t⇩r ∘ the ∘ cast),
(is_document_ptr, set_child_nodes⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r ∘ the ∘ cast)
]"
definition a_set_child_nodes :: "(_) object_ptr ⇒ (_) node_ptr list ⇒ (_, unit) dom_prog"
where
"a_set_child_nodes ptr children = invoke a_set_child_nodes_tups ptr (children)"
lemmas set_child_nodes_defs = a_set_child_nodes_def
definition a_set_child_nodes_locs :: "(_) object_ptr ⇒ (_, unit) dom_prog set"
where
"a_set_child_nodes_locs ptr ≡
(if is_element_ptr_kind ptr
then all_args (put_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t (the (cast ptr)) RElement.child_nodes_update) else {}) ∪
(if is_document_ptr_kind ptr
then all_args (put_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t (the (cast ptr)) document_element_update) else {})"
end
locale l_set_child_nodes_defs =
fixes set_child_nodes :: "(_) object_ptr ⇒ (_) node_ptr list ⇒ (_, unit) dom_prog"
fixes set_child_nodes_locs :: "(_) object_ptr ⇒ (_, unit) dom_prog set"
locale l_set_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_type_wf type_wf +
l_known_ptr known_ptr +
l_set_child_nodes_defs set_child_nodes set_child_nodes_locs +
l_set_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs
for type_wf :: "(_) heap ⇒ bool"
and known_ptr :: "(_) object_ptr ⇒ bool"
and set_child_nodes :: "(_) object_ptr ⇒ (_) node_ptr list ⇒ (_, unit) dom_prog"
and set_child_nodes_locs :: "(_) object_ptr ⇒ (_, unit) dom_prog set" +
assumes known_ptr_impl: "known_ptr = DocumentClass.known_ptr"
assumes type_wf_impl: "type_wf = DocumentClass.type_wf"
assumes set_child_nodes_impl: "set_child_nodes = a_set_child_nodes"
assumes set_child_nodes_locs_impl: "set_child_nodes_locs = a_set_child_nodes_locs"
begin
lemmas set_child_nodes_def = set_child_nodes_impl[unfolded a_set_child_nodes_def]
lemmas set_child_nodes_locs_def = set_child_nodes_locs_impl[unfolded a_set_child_nodes_locs_def]
lemma set_child_nodes_split:
"P (invoke (a_set_child_nodes_tups @ xs) ptr (children)) =
((known_ptr ptr ⟶ P (set_child_nodes ptr children))
∧ (¬(known_ptr ptr) ⟶ P (invoke xs ptr (children))))"
by(auto simp add: known_ptr_impl set_child_nodes_impl a_set_child_nodes_def
a_set_child_nodes_tups_def known_ptr_defs CharacterDataClass.known_ptr_defs
ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: invoke_splits)
lemma set_child_nodes_split_asm:
"P (invoke (a_set_child_nodes_tups @ xs) ptr (children)) =
(¬((known_ptr ptr ∧ ¬P (set_child_nodes ptr children))
∨ (¬(known_ptr ptr) ∧ ¬P (invoke xs ptr (children)))))"
by(auto simp add: known_ptr_impl set_child_nodes_impl a_set_child_nodes_def
a_set_child_nodes_tups_def known_ptr_defs CharacterDataClass.known_ptr_defs
ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: invoke_splits)[1]
lemmas set_child_nodes_splits = set_child_nodes_split set_child_nodes_split_asm
lemma set_child_nodes_writes: "writes (set_child_nodes_locs ptr) (set_child_nodes ptr children) h h'"
apply(simp add: set_child_nodes_locs_impl set_child_nodes_impl a_set_child_nodes_def
a_set_child_nodes_tups_def a_set_child_nodes_locs_def)
apply(split invoke_splits, rule conjI)+
apply(auto)[1]
apply(auto simp add: set_child_nodes⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def intro!: writes_bind_pure
intro: writes_union_right_I split: list.splits)[1]
apply(auto intro: writes_union_right_I split: option.splits)[1]
apply(auto intro: writes_union_right_I split: option.splits)[1]
apply(auto intro: writes_union_right_I split: option.splits)[1]
apply(auto intro: writes_union_right_I split: option.splits)[1]
apply(auto intro: writes_union_right_I split: option.splits)[1]
apply(auto intro: writes_union_right_I split: option.splits)[1]
apply(auto simp add: set_child_nodes⇩c⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩_⇩d⇩a⇩t⇩a⇩_⇩p⇩t⇩r_def intro!: writes_bind_pure)[1]
apply(auto simp add: set_child_nodes⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def intro: writes_union_left_I
intro!: writes_bind_pure split: list.splits option.splits)[1]
done
lemma set_child_nodes_pointers_preserved:
assumes "w ∈ set_child_nodes_locs object_ptr"
assumes "h ⊢ w →⇩h h'"
shows "object_ptr_kinds h = object_ptr_kinds h'"
using assms(1) object_ptr_kinds_preserved[OF writes_singleton2 assms(2)]
by(auto simp add: set_child_nodes_locs_impl all_args_def a_set_child_nodes_locs_def
split: if_splits)
lemma set_child_nodes_typess_preserved:
assumes "w ∈ set_child_nodes_locs object_ptr"
assumes "h ⊢ w →⇩h h'"
shows "type_wf h = type_wf h'"
using assms(1) type_wf_preserved[OF writes_singleton2 assms(2)]
by(auto simp add: set_child_nodes_locs_impl type_wf_impl all_args_def a_set_child_nodes_locs_def
split: if_splits)
end
locale l_set_child_nodes = l_type_wf + l_set_child_nodes_defs +
assumes set_child_nodes_writes:
"writes (set_child_nodes_locs ptr) (set_child_nodes ptr children) h h'"
assumes set_child_nodes_pointers_preserved:
"w ∈ set_child_nodes_locs object_ptr ⟹ h ⊢ w →⇩h h' ⟹ object_ptr_kinds h = object_ptr_kinds h'"
assumes set_child_nodes_types_preserved:
"w ∈ set_child_nodes_locs object_ptr ⟹ h ⊢ w →⇩h h' ⟹ type_wf h = type_wf h'"
global_interpretation l_set_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs defines
set_child_nodes = l_set_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs.a_set_child_nodes and
set_child_nodes_locs = l_set_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs.a_set_child_nodes_locs .
interpretation
i_set_child_nodes?: l_set_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf known_ptr set_child_nodes set_child_nodes_locs
apply(unfold_locales)
by (auto simp add: set_child_nodes_def set_child_nodes_locs_def)
declare l_set_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
lemma set_child_nodes_is_l_set_child_nodes [instances]:
"l_set_child_nodes type_wf set_child_nodes set_child_nodes_locs"
apply(unfold_locales)
using set_child_nodes_pointers_preserved set_child_nodes_typess_preserved set_child_nodes_writes
by blast+
paragraph ‹get\_child\_nodes›
locale l_set_child_nodes_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M = l_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M + l_set_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin
lemma set_child_nodes_get_child_nodes:
assumes "known_ptr ptr"
assumes "type_wf h"
assumes "h ⊢ set_child_nodes ptr children →⇩h h'"
shows "h' ⊢ get_child_nodes ptr →⇩r children"
proof -
have "h ⊢ check_in_heap ptr →⇩r ()"
using assms set_child_nodes_impl[unfolded a_set_child_nodes_def] invoke_ptr_in_heap
by (metis (full_types) check_in_heap_ptr_in_heap is_OK_returns_heap_I is_OK_returns_result_E
old.unit.exhaust)
then have ptr_in_h: "ptr |∈| object_ptr_kinds h"
by (simp add: check_in_heap_ptr_in_heap is_OK_returns_result_I)
have "type_wf h'"
apply(unfold type_wf_impl)
apply(rule subst[where P=id, OF type_wf_preserved[OF set_child_nodes_writes assms(3),
unfolded all_args_def], simplified])
by(auto simp add: all_args_def assms(2)[unfolded type_wf_impl]
set_child_nodes_locs_impl[unfolded a_set_child_nodes_locs_def]
split: if_splits)
have "h' ⊢ check_in_heap ptr →⇩r ()"
using check_in_heap_reads set_child_nodes_writes assms(3) ‹h ⊢ check_in_heap ptr →⇩r ()›
apply(rule reads_writes_separate_forwards)
by(auto simp add: all_args_def set_child_nodes_locs_impl[unfolded a_set_child_nodes_locs_def])
then have "ptr |∈| object_ptr_kinds h'"
using check_in_heap_ptr_in_heap by blast
with assms ptr_in_h ‹type_wf h'› show ?thesis
apply(auto simp add: get_child_nodes_impl set_child_nodes_impl type_wf_impl known_ptr_impl
a_get_child_nodes_def a_get_child_nodes_tups_def a_set_child_nodes_def
a_set_child_nodes_tups_def
del: bind_pure_returns_result_I2
intro!: bind_pure_returns_result_I2)[1]
apply(split invoke_splits, rule conjI)
apply(split invoke_splits, rule conjI)
apply(split invoke_splits, rule conjI)
apply(auto simp add: NodeClass.known_ptr_defs
dest!: known_ptr_not_document_ptr known_ptr_not_character_data_ptr
known_ptr_not_element_ptr)[1]
apply(auto simp add: NodeClass.known_ptr_defs
dest!: known_ptr_not_document_ptr known_ptr_not_character_data_ptr
known_ptr_not_element_ptr)[1]
apply(auto simp add: get_child_nodes⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def set_child_nodes⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_ok
split: list.splits option.splits
intro!: bind_pure_returns_result_I2
dest: get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_ok; auto dest: returns_result_eq
dest!: document_put_get[where getter = document_element])[1]
apply(auto simp add: get_child_nodes⇩c⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩_⇩d⇩a⇩t⇩a⇩_⇩p⇩t⇩r_def set_child_nodes⇩c⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩_⇩d⇩a⇩t⇩a⇩_⇩p⇩t⇩r_def)[1]
by(auto simp add: get_child_nodes⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def set_child_nodes⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def dest: element_put_get)
qed
lemma set_child_nodes_get_child_nodes_different_pointers:
assumes "ptr ≠ ptr'"
assumes "w ∈ set_child_nodes_locs ptr"
assumes "h ⊢ w →⇩h h'"
assumes "r ∈ get_child_nodes_locs ptr'"
shows "r h h'"
using assms
apply(auto simp add: get_child_nodes_locs_impl set_child_nodes_locs_impl all_args_def
a_set_child_nodes_locs_def a_get_child_nodes_locs_def
split: if_splits option.splits )[1]
apply(rule is_document_ptr_kind_obtains)
apply(simp)
apply(rule is_document_ptr_kind_obtains)
apply(auto)[1]
apply(auto)[1]
apply(rule is_element_ptr_kind_obtains)
apply(auto)[1]
apply(auto)[1]
apply(rule is_element_ptr_kind_obtains)
apply(auto)[1]
apply(auto)[1]
done
lemma set_child_nodes_element_ok [simp]:
assumes "known_ptr ptr"
assumes "type_wf h"
assumes "ptr |∈| object_ptr_kinds h"
assumes "is_element_ptr_kind ptr"
shows "h ⊢ ok (set_child_nodes ptr children)"
proof -
have "is_element_ptr ptr"
using ‹known_ptr ptr› assms(4)
by(auto simp add: known_ptr_impl known_ptr_defs CharacterDataClass.known_ptr_defs
ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)
then show ?thesis
using assms
apply(auto simp add: set_child_nodes_def a_set_child_nodes_tups_def set_child_nodes⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def
split: option.splits)[1]
by (simp add: DocumentMonad.put_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t_ok local.type_wf_impl)
qed
lemma set_child_nodes_document1_ok [simp]:
assumes "known_ptr ptr"
assumes "type_wf h"
assumes "ptr |∈| object_ptr_kinds h"
assumes "is_document_ptr_kind ptr"
assumes "children = []"
shows "h ⊢ ok (set_child_nodes ptr children)"
proof -
have "is_document_ptr ptr"
using ‹known_ptr ptr› assms(4)
by(auto simp add: known_ptr_impl known_ptr_defs CharacterDataClass.known_ptr_defs
ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)
then show ?thesis
using assms
apply(auto simp add: set_child_nodes_def a_set_child_nodes_tups_def set_child_nodes⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def
split: option.splits)[1]
by (simp add: DocumentMonad.put_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_ok local.type_wf_impl)
qed
lemma set_child_nodes_document2_ok [simp]:
assumes "known_ptr ptr"
assumes "type_wf h"
assumes "ptr |∈| object_ptr_kinds h"
assumes "is_document_ptr_kind ptr"
assumes "children = [child]"
assumes "is_element_ptr_kind child"
shows "h ⊢ ok (set_child_nodes ptr children)"
proof -
have "is_document_ptr ptr"
using ‹known_ptr ptr› assms(4)
by(auto simp add: known_ptr_impl known_ptr_defs CharacterDataClass.known_ptr_defs
ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)
then show ?thesis
using assms
apply(auto simp add: set_child_nodes_def a_set_child_nodes_tups_def set_child_nodes⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def)[1]
apply(split invoke_splits, rule conjI)+
apply(auto simp add: is_element_ptr_kind⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r_def set_child_nodes⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def split: option.splits)[1]
apply(auto simp add: is_element_ptr_kind⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r_def set_child_nodes⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def split: option.splits)[1]
apply (simp add: local.type_wf_impl put_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_ok)
apply(auto simp add: is_element_ptr_kind⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r_def set_child_nodes⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def split: option.splits)[1]
by(auto simp add: is_element_ptr_kind⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r_def set_child_nodes⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def split: option.splits)[1]
qed
end
locale l_set_child_nodes_get_child_nodes = l_get_child_nodes + l_set_child_nodes +
assumes set_child_nodes_get_child_nodes:
"type_wf h ⟹ known_ptr ptr
⟹ h ⊢ set_child_nodes ptr children →⇩h h' ⟹ h' ⊢ get_child_nodes ptr →⇩r children"
assumes set_child_nodes_get_child_nodes_different_pointers:
"ptr ≠ ptr' ⟹ w ∈ set_child_nodes_locs ptr ⟹ h ⊢ w →⇩h h'
⟹ r ∈ get_child_nodes_locs ptr' ⟹ r h h'"
interpretation
i_set_child_nodes_get_child_nodes?: l_set_child_nodes_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf
known_ptr get_child_nodes get_child_nodes_locs set_child_nodes set_child_nodes_locs
by unfold_locales
declare l_set_child_nodes_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
lemma set_child_nodes_get_child_nodes_is_l_set_child_nodes_get_child_nodes [instances]:
"l_set_child_nodes_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs
set_child_nodes set_child_nodes_locs"
using get_child_nodes_is_l_get_child_nodes set_child_nodes_is_l_set_child_nodes
apply(auto simp add: l_set_child_nodes_get_child_nodes_def l_set_child_nodes_get_child_nodes_axioms_def)[1]
using set_child_nodes_get_child_nodes apply blast
using set_child_nodes_get_child_nodes_different_pointers apply metis
done
subsubsection ‹get\_attribute›
locale l_get_attribute⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs
begin
definition a_get_attribute :: "(_) element_ptr ⇒ attr_key ⇒ (_, attr_value option) dom_prog"
where
"a_get_attribute ptr k = do {m ← get_M ptr attrs; return (fmlookup m k)}"
lemmas get_attribute_defs = a_get_attribute_def
definition a_get_attribute_locs :: "(_) element_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
where
"a_get_attribute_locs element_ptr = {preserved (get_M element_ptr attrs)}"
end
locale l_get_attribute_defs =
fixes get_attribute :: "(_) element_ptr ⇒ attr_key ⇒ (_, attr_value option) dom_prog"
fixes get_attribute_locs :: "(_) element_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
locale l_get_attribute⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_type_wf type_wf +
l_get_attribute_defs get_attribute get_attribute_locs +
l_get_attribute⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs
for type_wf :: "(_) heap ⇒ bool"
and get_attribute :: "(_) element_ptr ⇒ attr_key ⇒ (_, attr_value option) dom_prog"
and get_attribute_locs :: "(_) element_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set" +
assumes type_wf_impl: "type_wf = DocumentClass.type_wf"
assumes get_attribute_impl: "get_attribute = a_get_attribute"
assumes get_attribute_locs_impl: "get_attribute_locs = a_get_attribute_locs"
begin
lemma get_attribute_pure [simp]: "pure (get_attribute ptr k) h"
by (auto simp add: bind_pure_I get_attribute_impl[unfolded a_get_attribute_def])
lemma get_attribute_ok:
"type_wf h ⟹ element_ptr |∈| element_ptr_kinds h ⟹ h ⊢ ok (get_attribute element_ptr k)"
apply(unfold type_wf_impl)
unfolding get_attribute_impl[unfolded a_get_attribute_def] using get_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t_ok
by (metis bind_is_OK_pure_I return_ok ElementMonad.get_M_pure)
lemma get_attribute_ptr_in_heap:
"h ⊢ ok (get_attribute element_ptr k) ⟹ element_ptr |∈| element_ptr_kinds h"
unfolding get_attribute_impl[unfolded a_get_attribute_def]
by (meson DocumentMonad.get_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t_ptr_in_heap bind_is_OK_E is_OK_returns_result_I)
lemma get_attribute_reads:
"reads (get_attribute_locs element_ptr) (get_attribute element_ptr k) h h'"
by(auto simp add: get_attribute_impl[unfolded a_get_attribute_def]
get_attribute_locs_impl[unfolded a_get_attribute_locs_def]
reads_insert_writes_set_right
intro!: reads_bind_pure)
end
locale l_get_attribute = l_type_wf + l_get_attribute_defs +
assumes get_attribute_reads:
"reads (get_attribute_locs element_ptr) (get_attribute element_ptr k) h h'"
assumes get_attribute_ok:
"type_wf h ⟹ element_ptr |∈| element_ptr_kinds h ⟹ h ⊢ ok (get_attribute element_ptr k)"
assumes get_attribute_ptr_in_heap:
"h ⊢ ok (get_attribute element_ptr k) ⟹ element_ptr |∈| element_ptr_kinds h"
assumes get_attribute_pure [simp]: "pure (get_attribute element_ptr k) h"
global_interpretation l_get_attribute⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs defines
get_attribute = l_get_attribute⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs.a_get_attribute and
get_attribute_locs = l_get_attribute⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs.a_get_attribute_locs .
interpretation
i_get_attribute?: l_get_attribute⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf get_attribute get_attribute_locs
apply(unfold_locales)
by (auto simp add: get_attribute_def get_attribute_locs_def)
declare l_get_attribute⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
lemma get_attribute_is_l_get_attribute [instances]:
"l_get_attribute type_wf get_attribute get_attribute_locs"
apply(unfold_locales)
using get_attribute_reads get_attribute_ok get_attribute_ptr_in_heap get_attribute_pure
by blast+
subsubsection ‹set\_attribute›
locale l_set_attribute⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs
begin
definition
a_set_attribute :: "(_) element_ptr ⇒ attr_key ⇒ attr_value option ⇒ (_, unit) dom_prog"
where
"a_set_attribute ptr k v = do {
m ← get_M ptr attrs;
put_M ptr attrs_update (if v = None then fmdrop k m else fmupd k (the v) m)
}"
definition a_set_attribute_locs :: "(_) element_ptr ⇒ (_, unit) dom_prog set"
where
"a_set_attribute_locs element_ptr ≡ all_args (put_M element_ptr attrs_update)"
end
locale l_set_attribute_defs =
fixes set_attribute :: "(_) element_ptr ⇒ attr_key ⇒ attr_value option ⇒ (_, unit) dom_prog"
fixes set_attribute_locs :: "(_) element_ptr ⇒ (_, unit) dom_prog set"
locale l_set_attribute⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_type_wf type_wf +
l_set_attribute_defs set_attribute set_attribute_locs +
l_set_attribute⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs
for type_wf :: "(_) heap ⇒ bool"
and set_attribute :: "(_) element_ptr ⇒ attr_key ⇒ attr_value option ⇒ (_, unit) dom_prog"
and set_attribute_locs :: "(_) element_ptr ⇒ (_, unit) dom_prog set" +
assumes type_wf_impl: "type_wf = DocumentClass.type_wf"
assumes set_attribute_impl: "set_attribute = a_set_attribute"
assumes set_attribute_locs_impl: "set_attribute_locs = a_set_attribute_locs"
begin
lemmas set_attribute_def = set_attribute_impl[folded a_set_attribute_def]
lemmas set_attribute_locs_def = set_attribute_locs_impl[unfolded a_set_attribute_locs_def]
lemma set_attribute_ok: "type_wf h ⟹ element_ptr |∈| element_ptr_kinds h ⟹ h ⊢ ok (set_attribute element_ptr k v)"
apply(unfold type_wf_impl)
unfolding set_attribute_impl[unfolded a_set_attribute_def] using get_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t_ok put_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t_ok
by(metis (no_types, lifting) DocumentClass.type_wf⇩E⇩l⇩e⇩m⇩e⇩n⇩t ElementMonad.get_M_pure bind_is_OK_E
bind_is_OK_pure_I is_OK_returns_result_I)
lemma set_attribute_writes:
"writes (set_attribute_locs element_ptr) (set_attribute element_ptr k v) h h'"
by(auto simp add: set_attribute_impl[unfolded a_set_attribute_def]
set_attribute_locs_impl[unfolded a_set_attribute_locs_def]
intro: writes_bind_pure)
end
locale l_set_attribute = l_type_wf + l_set_attribute_defs +
assumes set_attribute_writes:
"writes (set_attribute_locs element_ptr) (set_attribute element_ptr k v) h h'"
assumes set_attribute_ok:
"type_wf h ⟹ element_ptr |∈| element_ptr_kinds h ⟹ h ⊢ ok (set_attribute element_ptr k v)"
global_interpretation l_set_attribute⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs defines
set_attribute = l_set_attribute⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs.a_set_attribute and
set_attribute_locs = l_set_attribute⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs.a_set_attribute_locs .
interpretation
i_set_attribute?: l_set_attribute⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf set_attribute set_attribute_locs
apply(unfold_locales)
by (auto simp add: set_attribute_def set_attribute_locs_def)
declare l_set_attribute⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
lemma set_attribute_is_l_set_attribute [instances]:
"l_set_attribute type_wf set_attribute set_attribute_locs"
apply(unfold_locales)
using set_attribute_ok set_attribute_writes
by blast+
paragraph ‹get\_attribute›
locale l_set_attribute_get_attribute⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_attribute⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_set_attribute⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin
lemma set_attribute_get_attribute:
"h ⊢ set_attribute ptr k v →⇩h h' ⟹ h' ⊢ get_attribute ptr k →⇩r v"
by(auto simp add: set_attribute_impl[unfolded a_set_attribute_def]
get_attribute_impl[unfolded a_get_attribute_def]
elim!: bind_returns_heap_E2
intro!: bind_pure_returns_result_I
elim: element_put_get)
end
locale l_set_attribute_get_attribute = l_get_attribute + l_set_attribute +
assumes set_attribute_get_attribute:
"h ⊢ set_attribute ptr k v →⇩h h' ⟹ h' ⊢ get_attribute ptr k →⇩r v"
interpretation
i_set_attribute_get_attribute?: l_set_attribute_get_attribute⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf
get_attribute get_attribute_locs set_attribute set_attribute_locs
by(unfold_locales)
declare l_set_attribute_get_attribute⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
lemma set_attribute_get_attribute_is_l_set_attribute_get_attribute [instances]:
"l_set_attribute_get_attribute type_wf get_attribute get_attribute_locs set_attribute set_attribute_locs"
using get_attribute_is_l_get_attribute set_attribute_is_l_set_attribute
apply(simp add: l_set_attribute_get_attribute_def l_set_attribute_get_attribute_axioms_def)
using set_attribute_get_attribute
by blast
paragraph ‹get\_child\_nodes›
locale l_set_attribute_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_set_attribute⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin
lemma set_attribute_get_child_nodes:
"∀w ∈ set_attribute_locs ptr. (h ⊢ w →⇩h h' ⟶ (∀r ∈ get_child_nodes_locs ptr'. r h h'))"
by(auto simp add: set_attribute_locs_def get_child_nodes_locs_def all_args_def
intro: element_put_get_preserved[where setter=attrs_update])
end
locale l_set_attribute_get_child_nodes =
l_set_attribute +
l_get_child_nodes +
assumes set_attribute_get_child_nodes:
"∀w ∈ set_attribute_locs ptr. (h ⊢ w →⇩h h' ⟶ (∀r ∈ get_child_nodes_locs ptr'. r h h'))"
interpretation
i_set_attribute_get_child_nodes?: l_set_attribute_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf
set_attribute set_attribute_locs known_ptr get_child_nodes get_child_nodes_locs
by unfold_locales
declare l_set_attribute_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
lemma set_attribute_get_child_nodes_is_l_set_attribute_get_child_nodes [instances]:
"l_set_attribute_get_child_nodes type_wf set_attribute set_attribute_locs known_ptr
get_child_nodes get_child_nodes_locs"
using set_attribute_is_l_set_attribute get_child_nodes_is_l_get_child_nodes
apply(simp add: l_set_attribute_get_child_nodes_def l_set_attribute_get_child_nodes_axioms_def)
using set_attribute_get_child_nodes
by blast
subsubsection ‹get\_disconnected\_nodes›
locale l_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs
begin
definition a_get_disconnected_nodes :: "(_) document_ptr
⇒ (_, (_) node_ptr list) dom_prog"
where
"a_get_disconnected_nodes document_ptr = get_M document_ptr disconnected_nodes"
lemmas get_disconnected_nodes_defs = a_get_disconnected_nodes_def
definition a_get_disconnected_nodes_locs :: "(_) document_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
where
"a_get_disconnected_nodes_locs document_ptr = {preserved (get_M document_ptr disconnected_nodes)}"
end
locale l_get_disconnected_nodes_defs =
fixes get_disconnected_nodes :: "(_) document_ptr ⇒ (_, (_) node_ptr list) dom_prog"
fixes get_disconnected_nodes_locs :: "(_) document_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
locale l_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_type_wf type_wf +
l_get_disconnected_nodes_defs get_disconnected_nodes get_disconnected_nodes_locs +
l_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs
for type_wf :: "(_) heap ⇒ bool"
and get_disconnected_nodes :: "(_) document_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
and get_disconnected_nodes_locs :: "(_) document_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set" +
assumes type_wf_impl: "type_wf = DocumentClass.type_wf"
assumes get_disconnected_nodes_impl: "get_disconnected_nodes = a_get_disconnected_nodes"
assumes get_disconnected_nodes_locs_impl: "get_disconnected_nodes_locs = a_get_disconnected_nodes_locs"
begin
lemmas
get_disconnected_nodes_def = get_disconnected_nodes_impl[unfolded a_get_disconnected_nodes_def]
lemmas
get_disconnected_nodes_locs_def = get_disconnected_nodes_locs_impl[unfolded a_get_disconnected_nodes_locs_def]
lemma get_disconnected_nodes_ok:
"type_wf h ⟹ document_ptr |∈| document_ptr_kinds h ⟹ h ⊢ ok (get_disconnected_nodes document_ptr)"
apply(unfold type_wf_impl)
unfolding get_disconnected_nodes_impl[unfolded a_get_disconnected_nodes_def] using get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_ok
by fast
lemma get_disconnected_nodes_ptr_in_heap:
"h ⊢ ok (get_disconnected_nodes document_ptr) ⟹ document_ptr |∈| document_ptr_kinds h"
unfolding get_disconnected_nodes_impl[unfolded a_get_disconnected_nodes_def]
by (simp add: DocumentMonad.get_M_ptr_in_heap)
lemma get_disconnected_nodes_pure [simp]: "pure (get_disconnected_nodes document_ptr) h"
unfolding get_disconnected_nodes_impl[unfolded a_get_disconnected_nodes_def] by simp
lemma get_disconnected_nodes_reads:
"reads (get_disconnected_nodes_locs document_ptr) (get_disconnected_nodes document_ptr) h h'"
by(simp add: get_disconnected_nodes_impl[unfolded a_get_disconnected_nodes_def]
get_disconnected_nodes_locs_impl[unfolded a_get_disconnected_nodes_locs_def]
reads_bind_pure reads_insert_writes_set_right)
end
locale l_get_disconnected_nodes = l_type_wf + l_get_disconnected_nodes_defs +
assumes get_disconnected_nodes_reads:
"reads (get_disconnected_nodes_locs document_ptr) (get_disconnected_nodes document_ptr) h h'"
assumes get_disconnected_nodes_ok:
"type_wf h ⟹ document_ptr |∈| document_ptr_kinds h ⟹ h ⊢ ok (get_disconnected_nodes document_ptr)"
assumes get_disconnected_nodes_ptr_in_heap:
"h ⊢ ok (get_disconnected_nodes document_ptr) ⟹ document_ptr |∈| document_ptr_kinds h"
assumes get_disconnected_nodes_pure [simp]:
"pure (get_disconnected_nodes document_ptr) h"
global_interpretation l_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs defines
get_disconnected_nodes = l_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs.a_get_disconnected_nodes and
get_disconnected_nodes_locs = l_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs.a_get_disconnected_nodes_locs .
interpretation
i_get_disconnected_nodes?: l_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf get_disconnected_nodes
get_disconnected_nodes_locs
apply(unfold_locales)
by (auto simp add: get_disconnected_nodes_def get_disconnected_nodes_locs_def)
declare l_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
lemma get_disconnected_nodes_is_l_get_disconnected_nodes [instances]:
"l_get_disconnected_nodes type_wf get_disconnected_nodes get_disconnected_nodes_locs"
apply(simp add: l_get_disconnected_nodes_def)
using get_disconnected_nodes_reads get_disconnected_nodes_ok get_disconnected_nodes_ptr_in_heap
get_disconnected_nodes_pure
by blast+
paragraph ‹set\_child\_nodes›
locale l_set_child_nodes_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_set_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
CD: l_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin
lemma set_child_nodes_get_disconnected_nodes:
"∀w ∈ a_set_child_nodes_locs ptr. (h ⊢ w →⇩h h' ⟶ (∀r ∈ a_get_disconnected_nodes_locs ptr'. r h h'))"
by(auto simp add: a_set_child_nodes_locs_def a_get_disconnected_nodes_locs_def all_args_def)
end
locale l_set_child_nodes_get_disconnected_nodes = l_set_child_nodes + l_get_disconnected_nodes +
assumes set_child_nodes_get_disconnected_nodes:
"∀w ∈ set_child_nodes_locs ptr. (h ⊢ w →⇩h h' ⟶ (∀r ∈ get_disconnected_nodes_locs ptr'. r h h'))"
interpretation
i_set_child_nodes_get_disconnected_nodes?: l_set_child_nodes_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf
known_ptr set_child_nodes set_child_nodes_locs
get_disconnected_nodes get_disconnected_nodes_locs
by(unfold_locales)
declare l_set_child_nodes_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
lemma set_child_nodes_get_disconnected_nodes_is_l_set_child_nodes_get_disconnected_nodes [instances]:
"l_set_child_nodes_get_disconnected_nodes type_wf set_child_nodes set_child_nodes_locs
get_disconnected_nodes get_disconnected_nodes_locs"
using set_child_nodes_is_l_set_child_nodes get_disconnected_nodes_is_l_get_disconnected_nodes
apply(simp add: l_set_child_nodes_get_disconnected_nodes_def
l_set_child_nodes_get_disconnected_nodes_axioms_def)
using set_child_nodes_get_disconnected_nodes
by fast
paragraph ‹set\_attribute›
locale l_set_attribute_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_set_attribute⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin
lemma set_attribute_get_disconnected_nodes:
"∀w ∈ a_set_attribute_locs ptr. (h ⊢ w →⇩h h' ⟶ (∀r ∈ a_get_disconnected_nodes_locs ptr'. r h h'))"
by(auto simp add: a_set_attribute_locs_def a_get_disconnected_nodes_locs_def all_args_def)
end
locale l_set_attribute_get_disconnected_nodes = l_set_attribute + l_get_disconnected_nodes +
assumes set_attribute_get_disconnected_nodes:
"∀w ∈ set_attribute_locs ptr. (h ⊢ w →⇩h h' ⟶ (∀r ∈ get_disconnected_nodes_locs ptr'. r h h'))"
interpretation
i_set_attribute_get_disconnected_nodes?: l_set_attribute_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf
set_attribute set_attribute_locs get_disconnected_nodes get_disconnected_nodes_locs
by(unfold_locales)
declare l_set_attribute_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
lemma set_attribute_get_disconnected_nodes_is_l_set_attribute_get_disconnected_nodes [instances]:
"l_set_attribute_get_disconnected_nodes type_wf set_attribute set_attribute_locs
get_disconnected_nodes get_disconnected_nodes_locs"
using set_attribute_is_l_set_attribute get_disconnected_nodes_is_l_get_disconnected_nodes
apply(simp add: l_set_attribute_get_disconnected_nodes_def
l_set_attribute_get_disconnected_nodes_axioms_def)
using set_attribute_get_disconnected_nodes
by fast
paragraph ‹new\_element›
locale l_new_element_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf get_disconnected_nodes get_disconnected_nodes_locs
for type_wf :: "(_) heap ⇒ bool"
and get_disconnected_nodes :: "(_) document_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
and get_disconnected_nodes_locs :: "(_) document_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
begin
lemma get_disconnected_nodes_new_element:
"h ⊢ new_element →⇩r new_element_ptr ⟹ h ⊢ new_element →⇩h h'
⟹ r ∈ get_disconnected_nodes_locs ptr' ⟹ r h h'"
by(auto simp add: get_disconnected_nodes_locs_def new_element_get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t)
end
locale l_new_element_get_disconnected_nodes = l_get_disconnected_nodes_defs +
assumes get_disconnected_nodes_new_element:
"h ⊢ new_element →⇩r new_element_ptr ⟹ h ⊢ new_element →⇩h h'
⟹ r ∈ get_disconnected_nodes_locs ptr' ⟹ r h h'"
interpretation i_new_element_get_disconnected_nodes?:
l_new_element_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf get_disconnected_nodes
get_disconnected_nodes_locs
by unfold_locales
declare l_new_element_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
lemma new_element_get_disconnected_nodes_is_l_new_element_get_disconnected_nodes [instances]:
"l_new_element_get_disconnected_nodes get_disconnected_nodes_locs"
by (simp add: get_disconnected_nodes_new_element l_new_element_get_disconnected_nodes_def)
paragraph ‹new\_character\_data›
locale l_new_character_data_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf get_disconnected_nodes get_disconnected_nodes_locs
for type_wf :: "(_) heap ⇒ bool"
and get_disconnected_nodes :: "(_) document_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
and get_disconnected_nodes_locs :: "(_) document_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
begin
lemma get_disconnected_nodes_new_character_data:
"h ⊢ new_character_data →⇩r new_character_data_ptr ⟹ h ⊢ new_character_data →⇩h h'
⟹ r ∈ get_disconnected_nodes_locs ptr' ⟹ r h h'"
by(auto simp add: get_disconnected_nodes_locs_def new_character_data_get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t)
end
locale l_new_character_data_get_disconnected_nodes = l_get_disconnected_nodes_defs +
assumes get_disconnected_nodes_new_character_data:
"h ⊢ new_character_data →⇩r new_character_data_ptr ⟹ h ⊢ new_character_data →⇩h h'
⟹ r ∈ get_disconnected_nodes_locs ptr' ⟹ r h h'"
interpretation i_new_character_data_get_disconnected_nodes?:
l_new_character_data_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf get_disconnected_nodes
get_disconnected_nodes_locs
by unfold_locales
declare l_new_character_data_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
lemma new_character_data_get_disconnected_nodes_is_l_new_character_data_get_disconnected_nodes [instances]:
"l_new_character_data_get_disconnected_nodes get_disconnected_nodes_locs"
by (simp add: get_disconnected_nodes_new_character_data l_new_character_data_get_disconnected_nodes_def)
paragraph ‹new\_document›
locale l_new_document_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf get_disconnected_nodes get_disconnected_nodes_locs
for type_wf :: "(_) heap ⇒ bool"
and get_disconnected_nodes :: "(_) document_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
and get_disconnected_nodes_locs :: "(_) document_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
begin
lemma get_disconnected_nodes_new_document_different_pointers:
"new_document_ptr ≠ ptr' ⟹ h ⊢ new_document →⇩r new_document_ptr ⟹ h ⊢ new_document →⇩h h'
⟹ r ∈ get_disconnected_nodes_locs ptr' ⟹ r h h'"
by(auto simp add: get_disconnected_nodes_locs_def new_document_get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t)
lemma new_document_no_disconnected_nodes:
"h ⊢ new_document →⇩r new_document_ptr ⟹ h ⊢ new_document →⇩h h'
⟹ h' ⊢ get_disconnected_nodes new_document_ptr →⇩r []"
by(simp add: get_disconnected_nodes_def new_document_disconnected_nodes)
end
interpretation i_new_document_get_disconnected_nodes?:
l_new_document_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf get_disconnected_nodes get_disconnected_nodes_locs
by unfold_locales
declare l_new_document_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
locale l_new_document_get_disconnected_nodes = l_get_disconnected_nodes_defs +
assumes get_disconnected_nodes_new_document_different_pointers:
"new_document_ptr ≠ ptr' ⟹ h ⊢ new_document →⇩r new_document_ptr ⟹ h ⊢ new_document →⇩h h'
⟹ r ∈ get_disconnected_nodes_locs ptr' ⟹ r h h'"
assumes new_document_no_disconnected_nodes:
"h ⊢ new_document →⇩r new_document_ptr ⟹ h ⊢ new_document →⇩h h'
⟹ h' ⊢ get_disconnected_nodes new_document_ptr →⇩r []"
lemma new_document_get_disconnected_nodes_is_l_new_document_get_disconnected_nodes [instances]:
"l_new_document_get_disconnected_nodes get_disconnected_nodes get_disconnected_nodes_locs"
apply (auto simp add: l_new_document_get_disconnected_nodes_def)[1]
using get_disconnected_nodes_new_document_different_pointers apply fast
using new_document_no_disconnected_nodes apply blast
done
subsubsection ‹set\_disconnected\_nodes›
locale l_set_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs
begin
definition a_set_disconnected_nodes :: "(_) document_ptr ⇒ (_) node_ptr list ⇒ (_, unit) dom_prog"
where
"a_set_disconnected_nodes document_ptr disc_nodes =
put_M document_ptr disconnected_nodes_update disc_nodes"
lemmas set_disconnected_nodes_defs = a_set_disconnected_nodes_def
definition a_set_disconnected_nodes_locs :: "(_) document_ptr ⇒ (_, unit) dom_prog set"
where
"a_set_disconnected_nodes_locs document_ptr ≡ all_args (put_M document_ptr disconnected_nodes_update)"
end
locale l_set_disconnected_nodes_defs =
fixes set_disconnected_nodes :: "(_) document_ptr ⇒ (_) node_ptr list ⇒ (_, unit) dom_prog"
fixes set_disconnected_nodes_locs :: "(_) document_ptr ⇒ (_, unit) dom_prog set"
locale l_set_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_type_wf type_wf +
l_set_disconnected_nodes_defs set_disconnected_nodes set_disconnected_nodes_locs +
l_set_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs
for type_wf :: "(_) heap ⇒ bool"
and set_disconnected_nodes :: "(_) document_ptr ⇒ (_) node_ptr list ⇒ (_, unit) dom_prog"
and set_disconnected_nodes_locs :: "(_) document_ptr ⇒ (_, unit) dom_prog set" +
assumes type_wf_impl: "type_wf = DocumentClass.type_wf"
assumes set_disconnected_nodes_impl: "set_disconnected_nodes = a_set_disconnected_nodes"
assumes set_disconnected_nodes_locs_impl: "set_disconnected_nodes_locs = a_set_disconnected_nodes_locs"
begin
lemmas set_disconnected_nodes_def = set_disconnected_nodes_impl[unfolded a_set_disconnected_nodes_def]
lemmas set_disconnected_nodes_locs_def =
set_disconnected_nodes_locs_impl[unfolded a_set_disconnected_nodes_locs_def]
lemma set_disconnected_nodes_ok:
"type_wf h ⟹ document_ptr |∈| document_ptr_kinds h ⟹
h ⊢ ok (set_disconnected_nodes document_ptr node_ptrs)"
by (simp add: type_wf_impl put_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_ok
set_disconnected_nodes_impl[unfolded a_set_disconnected_nodes_def])
lemma set_disconnected_nodes_ptr_in_heap:
"h ⊢ ok (set_disconnected_nodes document_ptr disc_nodes) ⟹ document_ptr |∈| document_ptr_kinds h"
by (simp add: set_disconnected_nodes_impl[unfolded a_set_disconnected_nodes_def]
DocumentMonad.put_M_ptr_in_heap)
lemma set_disconnected_nodes_writes:
"writes (set_disconnected_nodes_locs document_ptr) (set_disconnected_nodes document_ptr disc_nodes) h h'"
by(auto simp add: set_disconnected_nodes_impl[unfolded a_set_disconnected_nodes_def]
set_disconnected_nodes_locs_impl[unfolded a_set_disconnected_nodes_locs_def]
intro: writes_bind_pure)
lemma set_disconnected_nodes_pointers_preserved:
assumes "w ∈ set_disconnected_nodes_locs object_ptr"
assumes "h ⊢ w →⇩h h'"
shows "object_ptr_kinds h = object_ptr_kinds h'"
using assms(1) object_ptr_kinds_preserved[OF writes_singleton2 assms(2)]
by(auto simp add: all_args_def set_disconnected_nodes_locs_impl[unfolded
a_set_disconnected_nodes_locs_def]
split: if_splits)
lemma set_disconnected_nodes_typess_preserved:
assumes "w ∈ set_disconnected_nodes_locs object_ptr"
assumes "h ⊢ w →⇩h h'"
shows "type_wf h = type_wf h'"
using assms(1) type_wf_preserved[OF writes_singleton2 assms(2)]
apply(unfold type_wf_impl)
by(auto simp add: all_args_def
set_disconnected_nodes_locs_impl[unfolded a_set_disconnected_nodes_locs_def]
split: if_splits)
end
locale l_set_disconnected_nodes = l_type_wf + l_set_disconnected_nodes_defs +
assumes set_disconnected_nodes_writes:
"writes (set_disconnected_nodes_locs document_ptr)
(set_disconnected_nodes document_ptr disc_nodes) h h'"
assumes set_disconnected_nodes_ok:
"type_wf h ⟹ document_ptr |∈| document_ptr_kinds h ⟹
h ⊢ ok (set_disconnected_nodes document_ptr disc_noded)"
assumes set_disconnected_nodes_ptr_in_heap:
"h ⊢ ok (set_disconnected_nodes document_ptr disc_noded) ⟹
document_ptr |∈| document_ptr_kinds h"
assumes set_disconnected_nodes_pointers_preserved:
"w ∈ set_disconnected_nodes_locs document_ptr ⟹ h ⊢ w →⇩h h' ⟹
object_ptr_kinds h = object_ptr_kinds h'"
assumes set_disconnected_nodes_types_preserved:
"w ∈ set_disconnected_nodes_locs document_ptr ⟹ h ⊢ w →⇩h h' ⟹ type_wf h = type_wf h'"
global_interpretation l_set_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs defines
set_disconnected_nodes = l_set_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs.a_set_disconnected_nodes and
set_disconnected_nodes_locs = l_set_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs.a_set_disconnected_nodes_locs .
interpretation
i_set_disconnected_nodes?: l_set_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf set_disconnected_nodes
set_disconnected_nodes_locs
apply unfold_locales
by (auto simp add: set_disconnected_nodes_def set_disconnected_nodes_locs_def)
declare l_set_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
lemma set_disconnected_nodes_is_l_set_disconnected_nodes [instances]:
"l_set_disconnected_nodes type_wf set_disconnected_nodes set_disconnected_nodes_locs"
apply(simp add: l_set_disconnected_nodes_def)
using set_disconnected_nodes_ok set_disconnected_nodes_writes
set_disconnected_nodes_pointers_preserved
set_disconnected_nodes_ptr_in_heap set_disconnected_nodes_typess_preserved
by blast+
paragraph ‹get\_disconnected\_nodes›
locale l_set_disconnected_nodes_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M = l_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
+ l_set_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin
lemma set_disconnected_nodes_get_disconnected_nodes:
assumes "h ⊢ a_set_disconnected_nodes document_ptr disc_nodes →⇩h h'"
shows "h' ⊢ a_get_disconnected_nodes document_ptr →⇩r disc_nodes"
using assms
by(auto simp add: a_get_disconnected_nodes_def a_set_disconnected_nodes_def)
lemma set_disconnected_nodes_get_disconnected_nodes_different_pointers:
assumes "ptr ≠ ptr'"
assumes "w ∈ a_set_disconnected_nodes_locs ptr"
assumes "h ⊢ w →⇩h h'"
assumes "r ∈ a_get_disconnected_nodes_locs ptr'"
shows "r h h'"
using assms
by(auto simp add: all_args_def a_set_disconnected_nodes_locs_def a_get_disconnected_nodes_locs_def
split: if_splits option.splits )
end
locale l_set_disconnected_nodes_get_disconnected_nodes = l_get_disconnected_nodes
+ l_set_disconnected_nodes +
assumes set_disconnected_nodes_get_disconnected_nodes:
"h ⊢ set_disconnected_nodes document_ptr disc_nodes →⇩h h'
⟹ h' ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes"
assumes set_disconnected_nodes_get_disconnected_nodes_different_pointers:
"ptr ≠ ptr' ⟹ w ∈ set_disconnected_nodes_locs ptr ⟹ h ⊢ w →⇩h h'
⟹ r ∈ get_disconnected_nodes_locs ptr' ⟹ r h h'"
interpretation i_set_disconnected_nodes_get_disconnected_nodes?:
l_set_disconnected_nodes_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf get_disconnected_nodes
get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs
by unfold_locales
declare l_set_disconnected_nodes_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
lemma set_disconnected_nodes_get_disconnected_nodes_is_l_set_disconnected_nodes_get_disconnected_nodes
[instances]:
"l_set_disconnected_nodes_get_disconnected_nodes type_wf get_disconnected_nodes get_disconnected_nodes_locs
set_disconnected_nodes set_disconnected_nodes_locs"
using set_disconnected_nodes_is_l_set_disconnected_nodes get_disconnected_nodes_is_l_get_disconnected_nodes
apply(simp add: l_set_disconnected_nodes_get_disconnected_nodes_def
l_set_disconnected_nodes_get_disconnected_nodes_axioms_def)
using set_disconnected_nodes_get_disconnected_nodes
set_disconnected_nodes_get_disconnected_nodes_different_pointers
by fast+
paragraph ‹get\_child\_nodes›
locale l_set_disconnected_nodes_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_set_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin
lemma set_disconnected_nodes_get_child_nodes:
"∀w ∈ set_disconnected_nodes_locs ptr. (h ⊢ w →⇩h h' ⟶ (∀r ∈ get_child_nodes_locs ptr'. r h h'))"
by(auto simp add: set_disconnected_nodes_locs_impl[unfolded a_set_disconnected_nodes_locs_def]
get_child_nodes_locs_impl[unfolded a_get_child_nodes_locs_def] all_args_def)
end
locale l_set_disconnected_nodes_get_child_nodes = l_set_disconnected_nodes_defs + l_get_child_nodes_defs +
assumes set_disconnected_nodes_get_child_nodes [simp]:
"∀w ∈ set_disconnected_nodes_locs ptr. (h ⊢ w →⇩h h' ⟶ (∀r ∈ get_child_nodes_locs ptr'. r h h'))"
interpretation
i_set_disconnected_nodes_get_child_nodes?: l_set_disconnected_nodes_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
type_wf
set_disconnected_nodes set_disconnected_nodes_locs
known_ptr get_child_nodes get_child_nodes_locs
by unfold_locales
declare l_set_disconnected_nodes_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
lemma set_disconnected_nodes_get_child_nodes_is_l_set_disconnected_nodes_get_child_nodes [instances]:
"l_set_disconnected_nodes_get_child_nodes set_disconnected_nodes_locs get_child_nodes_locs"
using set_disconnected_nodes_is_l_set_disconnected_nodes get_child_nodes_is_l_get_child_nodes
apply(simp add: l_set_disconnected_nodes_get_child_nodes_def)
using set_disconnected_nodes_get_child_nodes
by fast
subsubsection ‹get\_tag\_name›
locale l_get_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs
begin
definition a_get_tag_name :: "(_) element_ptr ⇒ (_, tag_name) dom_prog"
where
"a_get_tag_name element_ptr = get_M element_ptr tag_name"
definition a_get_tag_name_locs :: "(_) element_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
where
"a_get_tag_name_locs element_ptr ≡ {preserved (get_M element_ptr tag_name)}"
end
locale l_get_tag_name_defs =
fixes get_tag_name :: "(_) element_ptr ⇒ (_, tag_name) dom_prog"
fixes get_tag_name_locs :: "(_) element_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
locale l_get_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_type_wf type_wf +
l_get_tag_name_defs get_tag_name get_tag_name_locs +
l_get_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs
for type_wf :: "(_) heap ⇒ bool"
and get_tag_name :: "(_) element_ptr ⇒ (_, tag_name) dom_prog"
and get_tag_name_locs :: "(_) element_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set" +
assumes type_wf_impl: "type_wf = DocumentClass.type_wf"
assumes get_tag_name_impl: "get_tag_name = a_get_tag_name"
assumes get_tag_name_locs_impl: "get_tag_name_locs = a_get_tag_name_locs"
begin
lemmas get_tag_name_def = get_tag_name_impl[unfolded a_get_tag_name_def]
lemmas get_tag_name_locs_def = get_tag_name_locs_impl[unfolded a_get_tag_name_locs_def]
lemma get_tag_name_ok:
"type_wf h ⟹ element_ptr |∈| element_ptr_kinds h ⟹ h ⊢ ok (get_tag_name element_ptr)"
apply(unfold type_wf_impl get_tag_name_impl[unfolded a_get_tag_name_def])
using get_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t_ok
by blast
lemma get_tag_name_pure [simp]: "pure (get_tag_name element_ptr) h"
unfolding get_tag_name_impl[unfolded a_get_tag_name_def]
by simp
lemma get_tag_name_ptr_in_heap [simp]:
assumes "h ⊢ get_tag_name element_ptr →⇩r children"
shows "element_ptr |∈| element_ptr_kinds h"
using assms
by(auto simp add: get_tag_name_impl[unfolded a_get_tag_name_def] get_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t_ptr_in_heap
dest: is_OK_returns_result_I)
lemma get_tag_name_reads: "reads (get_tag_name_locs element_ptr) (get_tag_name element_ptr) h h'"
by(simp add: get_tag_name_impl[unfolded a_get_tag_name_def]
get_tag_name_locs_impl[unfolded a_get_tag_name_locs_def] reads_bind_pure
reads_insert_writes_set_right)
end
locale l_get_tag_name = l_type_wf + l_get_tag_name_defs +
assumes get_tag_name_reads:
"reads (get_tag_name_locs element_ptr) (get_tag_name element_ptr) h h'"
assumes get_tag_name_ok:
"type_wf h ⟹ element_ptr |∈| element_ptr_kinds h ⟹ h ⊢ ok (get_tag_name element_ptr)"
assumes get_tag_name_ptr_in_heap:
"h ⊢ ok (get_tag_name element_ptr) ⟹ element_ptr |∈| element_ptr_kinds h"
assumes get_tag_name_pure [simp]:
"pure (get_tag_name element_ptr) h"
global_interpretation l_get_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs defines
get_tag_name = l_get_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs.a_get_tag_name and
get_tag_name_locs = l_get_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs.a_get_tag_name_locs .
interpretation
i_get_tag_name?: l_get_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf get_tag_name get_tag_name_locs
apply(unfold_locales)
by (auto simp add: get_tag_name_def get_tag_name_locs_def)
declare l_get_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
lemma get_tag_name_is_l_get_tag_name [instances]:
"l_get_tag_name type_wf get_tag_name get_tag_name_locs"
apply(unfold_locales)
using get_tag_name_reads get_tag_name_ok get_tag_name_ptr_in_heap get_tag_name_pure
by blast+
paragraph ‹set\_disconnected\_nodes›
locale l_set_disconnected_nodes_get_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_set_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin
lemma set_disconnected_nodes_get_tag_name:
"∀w ∈ a_set_disconnected_nodes_locs ptr. (h ⊢ w →⇩h h' ⟶ (∀r ∈ a_get_tag_name_locs ptr'. r h h'))"
by(auto simp add: a_set_disconnected_nodes_locs_def a_get_tag_name_locs_def all_args_def)
end
locale l_set_disconnected_nodes_get_tag_name = l_set_disconnected_nodes + l_get_tag_name +
assumes set_disconnected_nodes_get_tag_name:
"∀w ∈ set_disconnected_nodes_locs ptr. (h ⊢ w →⇩h h' ⟶ (∀r ∈ get_tag_name_locs ptr'. r h h'))"
interpretation
i_set_disconnected_nodes_get_tag_name?: l_set_disconnected_nodes_get_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf
set_disconnected_nodes set_disconnected_nodes_locs
get_tag_name get_tag_name_locs
by unfold_locales
declare l_set_disconnected_nodes_get_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
lemma set_disconnected_nodes_get_tag_name_is_l_set_disconnected_nodes_get_tag_name [instances]:
"l_set_disconnected_nodes_get_tag_name type_wf set_disconnected_nodes set_disconnected_nodes_locs
get_tag_name get_tag_name_locs"
using set_disconnected_nodes_is_l_set_disconnected_nodes get_tag_name_is_l_get_tag_name
apply(simp add: l_set_disconnected_nodes_get_tag_name_def l_set_disconnected_nodes_get_tag_name_axioms_def)
using set_disconnected_nodes_get_tag_name
by fast
paragraph ‹set\_child\_nodes›
locale l_set_child_nodes_get_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_set_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
l_get_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin
lemma set_child_nodes_get_tag_name:
"∀w ∈ set_child_nodes_locs ptr. (h ⊢ w →⇩h h' ⟶ (∀r ∈ get_tag_name_locs ptr'. r h h'))"
by(auto simp add: set_child_nodes_locs_def get_tag_name_locs_def all_args_def
intro: element_put_get_preserved[where getter=tag_name and setter=child_nodes_update])
end
locale l_set_child_nodes_get_tag_name = l_set_child_nodes + l_get_tag_name +
assumes set_child_nodes_get_tag_name:
"∀w ∈ set_child_nodes_locs ptr. (h ⊢ w →⇩h h' ⟶ (∀r ∈ get_tag_name_locs ptr'. r h h'))"
interpretation
i_set_child_nodes_get_tag_name?: l_set_child_nodes_get_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf known_ptr
set_child_nodes set_child_nodes_locs get_tag_name get_tag_name_locs
by unfold_locales
declare l_set_child_nodes_get_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms[instances]
lemma set_child_nodes_get_tag_name_is_l_set_child_nodes_get_tag_name [instances]:
"l_set_child_nodes_get_tag_name type_wf set_child_nodes set_child_nodes_locs get_tag_name get_tag_name_locs"
using set_child_nodes_is_l_set_child_nodes get_tag_name_is_l_get_tag_name
apply(simp add: l_set_child_nodes_get_tag_name_def l_set_child_nodes_get_tag_name_axioms_def)
using set_child_nodes_get_tag_name
by fast
subsubsection ‹set\_tag\_type›
locale l_set_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs
begin
definition a_set_tag_name :: "(_) element_ptr ⇒ tag_name ⇒ (_, unit) dom_prog"
where
"a_set_tag_name ptr tag = do {
m ← get_M ptr attrs;
put_M ptr tag_name_update tag
}"
lemmas set_tag_name_defs = a_set_tag_name_def
definition a_set_tag_name_locs :: "(_) element_ptr ⇒ (_, unit) dom_prog set"
where
"a_set_tag_name_locs element_ptr ≡ all_args (put_M element_ptr tag_name_update)"
end
locale l_set_tag_name_defs =
fixes set_tag_name :: "(_) element_ptr ⇒ tag_name ⇒ (_, unit) dom_prog"
fixes set_tag_name_locs :: "(_) element_ptr ⇒ (_, unit) dom_prog set"
locale l_set_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
l_type_wf type_wf +
l_set_tag_name_defs set_tag_name set_tag_name_locs +
l_set_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs
for type_wf :: "(_) heap ⇒ bool"
and set_tag_name :: "(_) element_ptr ⇒ char list ⇒ (_, unit) dom_prog"
and set_tag_name_locs :: "(_) element_ptr ⇒ (_, unit) dom_prog set" +
assumes type_wf_impl: "type_wf = DocumentClass.type_wf"
assumes set_tag_name_impl: "set_tag_name = a_set_tag_name"
assumes set_tag_name_locs_impl: "set_tag_name_locs = a_set_tag_name_locs"
begin
lemma set_tag_name_ok:
"type_wf h ⟹ element_ptr |∈| element_ptr_kinds h ⟹ h ⊢ ok (set_tag_name element_ptr tag)"
apply(unfold type_wf_impl)
unfolding set_tag_name_impl[unfolded a_set_tag_name_def] using get_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t_ok put_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t_ok
by (metis (no_types, lifting) DocumentClass.type_wf⇩E⇩l⇩e⇩m⇩e⇩n⇩t ElementMonad.get_M_pure bind_is_OK_E
bind_is_OK_pure_I is_OK_returns_result_I)
lemma set_tag_name_writes:
"writes (set_tag_name_locs element_ptr) (set_tag_name element_ptr tag) h h'"
by(auto simp add: set_tag_name_impl[unfolded a_set_tag_name_def]
set_tag_name_locs_impl[unfolded a_set_tag_name_locs_def] intro: writes_bind_pure)
lemma set_tag_name_pointers_preserved:
assumes "w ∈ set_tag_name_locs element_ptr"
assumes "h ⊢ w →⇩h h'"
shows "object_ptr_kinds h = object_ptr_kinds h'"
using assms(1) object_ptr_kinds_preserved[OF writes_singleton2 assms(2)]
by(auto simp add: all_args_def set_tag_name_locs_impl[unfolded a_set_tag_name_locs_def]
split: if_splits)
lemma set_tag_name_typess_preserved:
assumes "w ∈ set_tag_name_locs element_ptr"
assumes "h ⊢ w →⇩h h'"
shows "type_wf h = type_wf h'"
apply(unfold type_wf_impl)
using assms(1) type_wf_preserved[OF writes_singleton2 assms(2)]
by(auto simp add: all_args_def set_tag_name_locs_impl[unfolded a_set_tag_name_locs_def]
split: if_splits)
end
locale