|
|
|
|
Quelle Shadow_DOM.thy
Sprache: Isabelle
|
|
(***********************************************************************************
* Copyright (c) 2016-2020 The University of Sheffield, UK
* 2019-2020 University of Exeter, UK
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are met:
*
* * Redistributions of source code must retain the above copyright notice, this
* list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above copyright notice,
* this list of conditions and the following disclaimer in the documentation
* and/or other materials provided with the distribution.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*
* SPDX-License-Identifier: BSD-2-Clause
***********************************************************************************)
section‹The Shadow DOM›
theory Shadow_DOM
imports
"monads/ShadowRootMonad"
Core_DOM.Core_DOM
begin
abbreviation "safe_shadow_root_element_types ≡ {''article'', ''aside'', ''blockquote'', ''body'',
''div'', ''footer'', ''h1'', ''h2'', ''h3'', ''h4'', ''h5'', ''h6'', ''header'', ''main'',
''nav'', ''p'', ''section'', ''span''}"
subsection ‹Function Definitions›
subsubsection ‹get\_child\_nodes›
locale l_get_child_nodesShadow_DOM_defs =
CD: l_get_child_nodesCore_DOM_defs
begin
definition get_child_nodesshadow_root_ptr :: "(_) shadow_root_ptr ==> unit
==> (_, (_) node_ptr list) dom_prog" where
"get_child_nodesshadow_root_ptr shadow_root_ptr _ = get_M shadow_root_ptr RShadowRoot.child_nodes"
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_shadow_root_ptrobject_ptr, get_child_nodesshadow_root_ptr ∘ the ∘ cast)]"
definition a_get_child_nodes :: "(_) object_ptr ==> (_, (_) node_ptr list) dom_prog" where
"a_get_child_nodes ptr = invoke (CD.a_get_child_nodes_tups @ 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_shadow_root_ptr_kind ptr
then {preserved (get_M (the (cast ptr)) RShadowRoot.child_nodes)} else {}) ∪
CD.a_get_child_nodes_locs ptr"
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
global_interpretation l_get_child_nodesShadow_DOM_defs defines
get_child_nodes = l_get_child_nodesShadow_DOM_defs.a_get_child_nodes and
get_child_nodes_locs = l_get_child_nodesShadow_DOM_defs.a_get_child_nodes_locs
.
locale l_get_child_nodesShadow_DOM =
l_type_wf type_wf +
l_known_ptr known_ptr +
l_get_child_nodesShadow_DOM_defs +
l_get_child_nodes_defs get_child_nodes get_child_nodes_locs +
CD: l_get_child_nodesCore_DOM type_wfCore_DOM known_ptrCore_DOM get_child_nodesCore_DOM
get_child_nodes_locsCore_DOM
for type_wf :: "(_) heap ==> bool"
and known_ptr :: "(_) object_ptr ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and known_ptrCore_DOM :: "(_) 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"
and get_child_nodesCore_DOM :: "(_) object_ptr ==> (_, (_) node_ptr list) dom_prog"
and get_child_nodes_locsCore_DOM :: "(_) object_ptr ==> ((_) heap ==> (_) heap ==> bool) set" +
assumes known_ptr_impl: "known_ptr = ShadowRootClass.known_ptr"
assumes type_wf_impl: "type_wf = ShadowRootClass.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 get_child_nodes_def]
lemmas get_child_nodes_locs_def = get_child_nodes_locs_impl[unfolded a_get_child_nodes_locs_def
get_child_nodes_locs_def, folded CD.get_child_nodes_locs_impl]
lemma get_child_nodes_ok:
assumes "known_ptr ptr"
assumes "type_wf h"
assumes "ptr |∈| object_ptr_kinds h"
shows "h ⊨ ok (get_child_nodes ptr)"
using assms[unfolded known_ptr_impl type_wf_impl]
apply(auto simp add: get_child_nodes_def)[1]
apply(split CD.get_child_nodes_splits, rule conjI)+
using ShadowRootClass.type_wfDocument CD.get_child_nodes_ok CD.known_ptr_impl CD.type_wf_impl
apply blast
apply(auto simp add: CD.known_ptr_impl a_get_child_nodes_tups_def get_child_nodesshadow_root_ptr_def
get_MShadowRoot_ok
dest!: known_ptr_new_shadow_root_ptr intro!: bind_is_OK_I2)[1]
by (metis is_shadow_root_ptr_kind_none l_get_MShadowRoot_lemmas.get_MShadowRoot_ok
l_get_MShadowRoot_lemmas_axioms option.case_eq_if shadow_root_ptr_casts_commute3
shadow_root_ptr_kinds_commutes)
lemma get_child_nodes_ptr_in_heap:
assumes "h ⊨ get_child_nodes ptr →r children"
shows "ptr |∈| object_ptr_kinds h"
using assms
by(auto simp add: 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"
unfolding get_child_nodes_def a_get_child_nodes_tups_def
proof(split CD.get_child_nodes_splits, rule conjI; clarify)
assume "known_ptrCore_DOM ptr"
then show "pure (get_child_nodesCore_DOM ptr) h"
by simp
next
assume "¬ known_ptrCore_DOM ptr"
then show "pure (invoke [(is_shadow_root_ptrobject_ptr,
get_child_nodesshadow_root_ptr ∘ the ∘ castobject_ptr2shadow_root_ptr)]
ptr ()) h"
by(auto simp add: get_child_nodesshadow_root_ptr_def intro: bind_pure_I split: invoke_splits)
qed
lemma get_child_nodes_reads: "reads (get_child_nodes_locs ptr) (get_child_nodes ptr) h h'"
apply (simp add: get_child_nodes_def a_get_child_nodes_tups_def get_child_nodes_locs_def
CD.get_child_nodes_locs_def)
apply(split CD.get_child_nodes_splits, rule conjI)+
apply(auto intro!: reads_subset[OF CD.get_child_nodes_reads[unfolded CD.get_child_nodes_locs_def]]
split: if_splits)[1]
apply(split invoke_splits, rule conjI)+
apply(auto)[1]
apply(auto simp add: get_child_nodesshadow_root_ptr_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
interpretation i_get_child_nodes?: l_get_child_nodesShadow_DOM type_wf known_ptr DocumentClass.type_wf
DocumentClass.known_ptr get_child_nodes get_child_nodes_locs Core_DOM_Functions.get_child_nodes
Core_DOM_Functions.get_child_nodes_locs
by(simp add: l_get_child_nodesShadow_DOM_def l_get_child_nodesShadow_DOM_axioms_def instances)
declare l_get_child_nodesShadow_DOM_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(auto simp add: l_get_child_nodes_def instances)[1]
using get_child_nodes_reads get_child_nodes_ok get_child_nodes_ptr_in_heap get_child_nodes_pure
by blast+
paragraph ‹new\_document›
locale l_new_document_get_child_nodesShadow_DOM =
CD: l_new_document_get_child_nodesCore_DOM type_wfCore_DOM known_ptrCore_DOM get_child_nodesCore_DOM
get_child_nodes_locsCore_DOM
+ l_get_child_nodesShadow_DOM type_wf known_ptr type_wfCore_DOM known_ptrCore_DOM get_child_nodes
get_child_nodes_locs get_child_nodesCore_DOM get_child_nodes_locsCore_DOM
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"
and type_wfCore_DOM :: "(_) heap ==> bool"
and known_ptrCore_DOM :: "(_) object_ptr ==> bool"
and get_child_nodesCore_DOM :: "(_) object_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locsCore_DOM :: "(_) 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'"
apply(auto simp add: get_child_nodes_locs_def)[1]
using CD.get_child_nodes_new_document
apply (metis document_ptr_casts_commute3 empty_iff is_document_ptr_kind_none
new_document_get_MShadowRoot option.case_eq_if shadow_root_ptr_casts_commute3
singletonD)
by (simp add: CD.get_child_nodes_new_document)
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)[1]
apply(split CD.get_child_nodes_splits, rule conjI)+
using CD.new_document_no_child_nodes apply auto[1]
by(auto simp add: DocumentClass.a_known_ptr_def CD.known_ptr_impl known_ptr_def
dest!: new_document_is_document_ptr)
end
interpretation i_new_document_get_child_nodes?:
l_new_document_get_child_nodesShadow_DOM type_wf known_ptr get_child_nodes get_child_nodes_locs
DocumentClass.type_wf DocumentClass.known_ptr Core_DOM_Functions.get_child_nodes
Core_DOM_Functions.get_child_nodes_locs
by(unfold_locales)
declare l_new_document_get_child_nodesCore_DOM_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
paragraph ‹new\_shadow\_root›
locale l_new_shadow_root_get_child_nodesShadow_DOM =
l_get_child_nodesShadow_DOM type_wf known_ptr type_wfCore_DOM known_ptrCore_DOM get_child_nodes
get_child_nodes_locs get_child_nodesCore_DOM get_child_nodes_locsCore_DOM
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"
and type_wfCore_DOM :: "(_) heap ==> bool"
and known_ptrCore_DOM :: "(_) object_ptr ==> bool"
and get_child_nodesCore_DOM :: "(_) object_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locsCore_DOM :: "(_) object_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
lemma get_child_nodes_new_shadow_root:
"ptr' ≠ cast new_shadow_root_ptr ==> h ⊨ newShadowRoot_M →r new_shadow_root_ptr
==> h ⊨ newShadowRoot_M →h h' ==> r ∈ get_child_nodes_locs ptr' ==> r h h'"
apply(auto simp add: get_child_nodes_locs_def)[1]
apply (metis document_ptr_casts_commute3 insert_absorb insert_not_empty is_document_ptr_kind_none
new_shadow_root_get_MShadowRoot option.case_eq_if shadow_root_ptr_casts_commute3 singletonD)
apply(auto simp add: CD.get_child_nodes_locs_def)[1]
using new_shadow_root_get_MObject apply blast
apply (metis empty_iff insertE new_shadow_root_get_MElement)
apply (metis empty_iff new_shadow_root_get_MDocument singletonD)
done
lemma new_shadow_root_no_child_nodes:
"h ⊨ newShadowRoot_M →r new_shadow_root_ptr ==> h ⊨ newShadowRoot_M →h h'
==> h' ⊨ get_child_nodes (cast new_shadow_root_ptr) →r []"
apply(auto simp add: get_child_nodes_def )[1]
apply(split CD.get_child_nodes_splits, rule conjI)+
apply(auto simp add: CD.get_child_nodes_def CD.a_get_child_nodes_tups_def)[1]
apply(split invoke_splits, rule conjI)+
using NodeClass.a_known_ptr_def known_ptr_not_character_data_ptr known_ptr_not_document_ptr
known_ptr_not_element_ptr local.CD.known_ptr_impl apply blast
apply(auto simp add: is_document_ptr_def split: option.splits document_ptr.splits)[1]
apply(auto simp add: is_character_data_ptr_def split: option.splits document_ptr.splits)[1]
apply(auto simp add: is_element_ptr_def split: option.splits document_ptr.splits)[1]
apply(auto simp add: a_get_child_nodes_tups_def)[1]
apply(split invoke_splits, rule conjI)+
apply(auto simp add: is_shadow_root_ptr_def split: shadow_root_ptr.splits
dest!: newShadowRoot_M_is_shadow_root_ptr)[1]
apply(auto intro!: bind_pure_returns_result_I)[1]
apply(drule(1) newShadowRoot_M_ptr_in_heap)
apply(auto simp add: shadow_root_ptr_kinds_def document_ptr_kinds_def)[1]
apply (metis check_in_heap_ptr_in_heap is_OK_returns_result_E old.unit.exhaust)
using new_shadow_root_children
by (simp add: new_shadow_root_children get_child_nodesshadow_root_ptr_def)
end
interpretation i_new_shadow_root_get_child_nodes?:
l_new_shadow_root_get_child_nodesShadow_DOM type_wf known_ptr get_child_nodes get_child_nodes_locs
DocumentClass.type_wf DocumentClass.known_ptr Core_DOM_Functions.get_child_nodes
Core_DOM_Functions.get_child_nodes_locs
by(unfold_locales)
declare l_new_shadow_root_get_child_nodesShadow_DOM_def[instances]
locale l_new_shadow_root_get_child_nodes = l_get_child_nodes +
assumes get_child_nodes_new_shadow_root:
"ptr' ≠ cast new_shadow_root_ptr ==> h ⊨ newShadowRoot_M →r new_shadow_root_ptr
==> h ⊨ newShadowRoot_M →h h' ==> r ∈ get_child_nodes_locs ptr' ==> r h h'"
assumes new_shadow_root_no_child_nodes:
"h ⊨ newShadowRoot_M →r new_shadow_root_ptr ==> h ⊨ newShadowRoot_M →h h'
==> h' ⊨ get_child_nodes (cast new_shadow_root_ptr) →r []"
lemma new_shadow_root_get_child_nodes_is_l_new_shadow_root_get_child_nodes [instances]:
"l_new_shadow_root_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs"
apply(simp add: l_new_shadow_root_get_child_nodes_def l_new_shadow_root_get_child_nodes_axioms_def
instances)
using get_child_nodes_new_shadow_root new_shadow_root_no_child_nodes
by fast
paragraph ‹new\_element›
locale l_new_element_get_child_nodesShadow_DOM =
l_get_child_nodesShadow_DOM +
l_new_element_get_child_nodesCore_DOM type_wfCore_DOM known_ptrCore_DOM get_child_nodesCore_DOM
get_child_nodes_locsCore_DOM
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 CD.get_child_nodes_locs_def new_element_get_MObject
new_element_get_MElement new_element_get_MDocument new_element_get_MShadowRoot
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 CD.get_child_nodes_splits, rule conjI)+
using local.new_element_no_child_nodes apply auto[1]
apply(auto simp add: invoke_def)[1]
apply(auto simp add: new_element_ptr_in_heap get_child_nodeselement_ptr_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)[1]
proof -
assume " h ⊨ new_element →r new_element_ptr"
assume "h ⊨ new_element →h h'"
assume "¬ known_ptrCore_DOM (castelement_ptr2object_ptr new_element_ptr)"
moreover
have "known_ptr (cast new_element_ptr)"
using new_element_is_element_ptr ‹h ⊨ new_element →r new_element_ptr›
by(auto simp add: known_ptr_impl ShadowRootClass.a_known_ptr_def DocumentClass.a_known_ptr_def
CharacterDataClass.a_known_ptr_def ElementClass.a_known_ptr_def)
ultimately show "False"
by(simp add: known_ptr_impl CD.known_ptr_impl ShadowRootClass.a_known_ptr_def
is_document_ptr_kind_none)
qed
end
interpretation i_new_element_get_child_nodes?:
l_new_element_get_child_nodesShadow_DOM type_wf known_ptr DocumentClass.type_wf
DocumentClass.known_ptr get_child_nodes get_child_nodes_locs Core_DOM_Functions.get_child_nodes
Core_DOM_Functions.get_child_nodes_locs
by(unfold_locales)
declare l_new_element_get_child_nodesShadow_DOM_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+
subsubsection ‹delete\_shadow\_root›
locale l_delete_shadow_root_get_child_nodesShadow_DOM =
l_get_child_nodesShadow_DOM
begin
lemma get_child_nodes_delete_shadow_root:
"ptr' ≠ cast shadow_root_ptr ==> h ⊨ deleteShadowRoot_M shadow_root_ptr →h h' ==>
r ∈ get_child_nodes_locs ptr' ==> r h h'"
by(auto simp add: get_child_nodes_locs_def CD.get_child_nodes_locs_def
delete_shadow_root_get_MObject delete_shadow_root_get_MShadowRoot
delete_shadow_root_get_MDocument delete_shadow_root_get_MElement
split: if_splits option.splits
intro: is_shadow_root_ptr_kind_obtains)
end
locale l_delete_shadow_root_get_child_nodes = l_get_child_nodes_defs +
assumes get_child_nodes_delete_shadow_root:
"ptr' ≠ cast shadow_root_ptr ==> h ⊨ deleteShadowRoot_M shadow_root_ptr →h h' ==>
r ∈ get_child_nodes_locs ptr' ==> r h h'"
interpretation l_delete_shadow_root_get_child_nodesShadow_DOM type_wf known_ptr DocumentClass.type_wf
DocumentClass.known_ptr get_child_nodes get_child_nodes_locs Core_DOM_Functions.get_child_nodes
Core_DOM_Functions.get_child_nodes_locs
by(auto simp add: l_delete_shadow_root_get_child_nodesShadow_DOM_def instances)
lemma l_delete_shadow_root_get_child_nodes_get_child_nodes_locs [instances]: "l_delete_shadow_root_get_child_nodes get_child_nodes_locs"
apply(auto simp add: l_delete_shadow_root_get_child_nodes_def)[1]
using get_child_nodes_delete_shadow_root apply fast
done
subsubsection ‹set\_child\_nodes›
locale l_set_child_nodesShadow_DOM_defs =
CD: l_set_child_nodesCore_DOM_defs
begin
definition set_child_nodesshadow_root_ptr :: "(_) shadow_root_ptr ==> (_) node_ptr list
==> (_, unit) dom_prog" where
"set_child_nodesshadow_root_ptr shadow_root_ptr = put_M shadow_root_ptr RShadowRoot.child_nodes_update"
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_shadow_root_ptrobject_ptr, set_child_nodesshadow_root_ptr ∘ the ∘ cast)]"
definition a_set_child_nodes :: "(_) object_ptr ==> (_) node_ptr list ==> (_, unit) dom_prog" where
"a_set_child_nodes ptr children = invoke (CD.a_set_child_nodes_tups @ a_set_child_nodes_tups)
ptr children"
definition a_set_child_nodes_locs :: "(_) object_ptr ==> (_, unit) dom_prog set"
where
"a_set_child_nodes_locs ptr ≡
(if is_shadow_root_ptr_kind ptr
then all_args (put_M (the (cast ptr)) RShadowRoot.child_nodes_update)
else {}) ∪ CD.a_set_child_nodes_locs ptr"
end
global_interpretation l_set_child_nodesShadow_DOM_defs defines
set_child_nodes = l_set_child_nodesShadow_DOM_defs.a_set_child_nodes and
set_child_nodes_locs = l_set_child_nodesShadow_DOM_defs.a_set_child_nodes_locs
.
locale l_set_child_nodesShadow_DOM =
l_type_wf type_wf +
l_known_ptr known_ptr +
l_set_child_nodesShadow_DOM_defs +
l_set_child_nodes_defs set_child_nodes set_child_nodes_locs +
CD: l_set_child_nodesCore_DOM type_wfCore_DOM known_ptrCore_DOM set_child_nodesCore_DOM
set_child_nodes_locsCore_DOM
for type_wf :: "(_) heap ==> bool"
and known_ptr :: "(_) object_ptr ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and known_ptrCore_DOM :: "(_) 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"
and set_child_nodesCore_DOM :: "(_) object_ptr ==> (_) node_ptr list ==> (_, unit) dom_prog"
and set_child_nodes_locsCore_DOM :: "(_) object_ptr ==> (_, unit) dom_prog set" +
assumes known_ptr_impl: "known_ptr = ShadowRootClass.known_ptr"
assumes type_wf_impl: "type_wf = ShadowRootClass.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 set_child_nodes_def]
lemmas set_child_nodes_locs_def = set_child_nodes_locs_impl[unfolded a_set_child_nodes_locs_def
set_child_nodes_locs_def, folded CD.set_child_nodes_locs_impl]
lemma set_child_nodes_writes: "writes (set_child_nodes_locs ptr) (set_child_nodes ptr children) h h'"
apply (simp add: set_child_nodes_def a_set_child_nodes_tups_def set_child_nodes_locs_def)
apply(split CD.set_child_nodes_splits, rule conjI)+
apply (simp add: CD.set_child_nodes_writes writes_union_right_I)
apply(split invoke_splits, rule conjI)+
apply(auto simp add: a_set_child_nodes_def)[1]
apply(auto simp add: set_child_nodesshadow_root_ptr_def
intro!: writes_bind_pure
intro: writes_union_right_I writes_union_left_I
split: list.splits)[1]
by (simp add: is_shadow_root_ptr_kind_none)
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: all_args_def set_child_nodes_locs_def CD.set_child_nodes_locs_def
split: if_splits)
lemma set_child_nodes_types_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: all_args_def type_wf_impl a_set_child_nodes_tups_def set_child_nodes_locs_def
CD.set_child_nodes_locs_def
split: if_splits option.splits)
end
interpretation
i_set_child_nodes?: l_set_child_nodesShadow_DOM type_wf known_ptr DocumentClass.type_wf
DocumentClass.known_ptr set_child_nodes set_child_nodes_locs Core_DOM_Functions.set_child_nodes
Core_DOM_Functions.set_child_nodes_locs
apply(unfold_locales)
by (auto simp add: set_child_nodes_def set_child_nodes_locs_def)
declare l_set_child_nodesShadow_DOM_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"
using instances Shadow_DOM.i_set_child_nodes.set_child_nodes_pointers_preserved Shadow_DOM.i_set_child_nodes.set_child_nodes_writes i_set_child_nodes.set_child_nodes_types_preserved
unfolding l_set_child_nodes_def
by blast
paragraph ‹get\_child\_nodes›
locale l_set_child_nodes_get_child_nodesShadow_DOM =
l_get_child_nodesShadow_DOM
type_wf known_ptr type_wfCore_DOM known_ptrCore_DOM get_child_nodes get_child_nodes_locs
get_child_nodesCore_DOM get_child_nodes_locsCore_DOM
+ l_set_child_nodesShadow_DOM
type_wf known_ptr type_wfCore_DOM known_ptrCore_DOM set_child_nodes set_child_nodes_locs
set_child_nodesCore_DOM set_child_nodes_locsCore_DOM
+ CD: l_set_child_nodes_get_child_nodesCore_DOM
type_wfCore_DOM known_ptrCore_DOM get_child_nodesCore_DOM get_child_nodes_locsCore_DOM
set_child_nodesCore_DOM set_child_nodes_locsCore_DOM
for type_wf :: "(_) heap ==> bool"
and known_ptr :: "(_) object_ptr ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and known_ptrCore_DOM :: "(_) 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"
and get_child_nodesCore_DOM :: "(_) object_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locsCore_DOM :: "(_) object_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and set_child_nodes :: "(_) object_ptr ==> (_) node_ptr list ==> ((_) heap, exception, unit) prog"
and set_child_nodes_locs :: "(_) object_ptr ==> ((_) heap, exception, unit) prog set"
and set_child_nodesCore_DOM :: "(_) object_ptr ==> (_) node_ptr list ==> ((_) heap, exception, unit) prog"
and set_child_nodes_locsCore_DOM :: "(_) object_ptr ==> ((_) heap, exception, unit) prog set"
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_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_def
CD.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)
apply(auto simp add: all_args_def set_child_nodes_locs_def CD.set_child_nodes_locs_def)[1]
done
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: type_wf_impl known_ptr_impl get_child_nodes_def a_get_child_nodes_tups_def
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 CD.get_child_nodes_splits, (rule conjI impI)+)+
apply(split CD.set_child_nodes_splits)+
apply(auto simp add: CD.set_child_nodes_get_child_nodes type_wf_impl CD.type_wf_impl
dest: ShadowRootClass.type_wfDocument)[1]
apply(auto simp add: CD.set_child_nodes_get_child_nodes type_wf_impl CD.type_wf_impl
dest: ShadowRootClass.type_wfDocument)[1]
apply(split CD.set_child_nodes_splits)+
by(auto simp add: known_ptr_impl CD.known_ptr_impl set_child_nodesshadow_root_ptr_def
get_child_nodesshadow_root_ptr_def CD.type_wf_impl ShadowRootClass.type_wfDocument
dest: known_ptr_new_shadow_root_ptr)[2]
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: set_child_nodes_locs_def CD.set_child_nodes_locs_def
get_child_nodes_locs_def CD.get_child_nodes_locs_def)[1]
by(auto simp add: all_args_def
elim!: is_document_ptr_kind_obtains is_shadow_root_ptr_kind_obtains
is_element_ptr_kind_obtains
split: if_splits option.splits)
end
interpretation
i_set_child_nodes_get_child_nodes?: l_set_child_nodes_get_child_nodesShadow_DOM type_wf known_ptr
DocumentClass.type_wf DocumentClass.known_ptr get_child_nodes get_child_nodes_locs
Core_DOM_Functions.get_child_nodes Core_DOM_Functions.get_child_nodes_locs set_child_nodes
set_child_nodes_locs Core_DOM_Functions.set_child_nodes Core_DOM_Functions.set_child_nodes_locs
using instances
by(auto simp add: l_set_child_nodes_get_child_nodesShadow_DOM_def )
declare l_set_child_nodes_get_child_nodesShadow_DOM_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"
apply(auto simp add: instances 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 fast
using set_child_nodes_get_child_nodes_different_pointers apply fast
done
subsubsection ‹set\_tag\_type›
locale l_set_tag_nameShadow_DOM =
CD: l_set_tag_nameCore_DOM type_wfCore_DOM set_tag_name set_tag_name_locs +
l_type_wf type_wf
for type_wf :: "(_) heap ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and set_tag_name :: "(_) element_ptr ==> tag_name ==> (_, unit) dom_prog"
and set_tag_name_locs :: "(_) element_ptr ==> (_, unit) dom_prog set" +
assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
begin
lemmas set_tag_name_def = CD.set_tag_name_impl[unfolded CD.a_set_tag_name_def set_tag_name_def]
lemmas set_tag_name_locs_def = CD.set_tag_name_locs_impl[unfolded CD.a_set_tag_name_locs_def
set_tag_name_locs_def]
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_MElement_ok put_MElement_ok
using CD.set_tag_name_ok CD.type_wf_impl ShadowRootClass.type_wfDocument by blast
lemma set_tag_name_writes:
"writes (set_tag_name_locs element_ptr) (set_tag_name element_ptr tag) h h'"
using CD.set_tag_name_writes .
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
by(simp add: CD.set_tag_name_pointers_preserved)
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)
apply(rule type_wf_preserved[OF writes_singleton2 assms(2)])
using assms(1) set_tag_name_locs_def
by(auto simp add: all_args_def set_tag_name_locs_def
split: if_splits)
end
interpretation i_set_tag_name?: l_set_tag_nameShadow_DOM type_wf DocumentClass.type_wf set_tag_name
set_tag_name_locs
by(auto simp add: l_set_tag_nameShadow_DOM_def l_set_tag_nameShadow_DOM_axioms_def instances)
declare l_set_tag_nameShadow_DOM_axioms [instances]
lemma set_tag_name_is_l_set_tag_name [instances]:
"l_set_tag_name type_wf set_tag_name set_tag_name_locs"
apply(auto simp add: l_set_tag_name_def)[1]
using set_tag_name_writes apply fast
using set_tag_name_ok apply fast
using set_tag_name_pointers_preserved apply (fast, fast)
using set_tag_name_typess_preserved apply (fast, fast)
done
paragraph ‹get\_child\_nodes›
locale l_set_tag_name_get_child_nodesShadow_DOM =
l_set_tag_nameShadow_DOM +
l_get_child_nodesShadow_DOM +
CD: l_set_tag_name_get_child_nodesCore_DOM type_wfCore_DOM set_tag_name set_tag_name_locs
known_ptrCore_DOM get_child_nodesCore_DOM get_child_nodes_locsCore_DOM
begin
lemma set_tag_name_get_child_nodes:
"∀w ∈ set_tag_name_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_child_nodes_locs ptr'. r h h'))"
apply(auto simp add: get_child_nodes_locs_def)[1]
apply(auto simp add: set_tag_name_locs_def all_args_def)[1]
using CD.set_tag_name_get_child_nodes apply(blast)
using CD.set_tag_name_get_child_nodes apply(blast)
done
end
interpretation
i_set_tag_name_get_child_nodes?: l_set_tag_name_get_child_nodesShadow_DOM type_wf
DocumentClass.type_wf set_tag_name set_tag_name_locs known_ptr DocumentClass.known_ptr
get_child_nodes get_child_nodes_locs Core_DOM_Functions.get_child_nodes
Core_DOM_Functions.get_child_nodes_locs
by unfold_locales
declare l_set_tag_name_get_child_nodesShadow_DOM_axioms[instances]
lemma set_tag_name_get_child_nodes_is_l_set_tag_name_get_child_nodes [instances]:
"l_set_tag_name_get_child_nodes type_wf set_tag_name set_tag_name_locs known_ptr get_child_nodes
get_child_nodes_locs"
using set_tag_name_is_l_set_tag_name get_child_nodes_is_l_get_child_nodes
apply(simp add: l_set_tag_name_get_child_nodes_def
l_set_tag_name_get_child_nodes_axioms_def)
using set_tag_name_get_child_nodes
by fast
subsubsection ‹get\_shadow\_root›
locale l_get_shadow_rootShadow_DOM_defs
begin
definition a_get_shadow_root :: "(_) element_ptr ==> (_, (_) shadow_root_ptr option) dom_prog"
where
"a_get_shadow_root element_ptr = get_M element_ptr shadow_root_opt"
definition a_get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
where
"a_get_shadow_root_locs element_ptr ≡ {preserved (get_M element_ptr shadow_root_opt)}"
end
global_interpretation l_get_shadow_rootShadow_DOM_defs
defines get_shadow_root = a_get_shadow_root
and get_shadow_root_locs = a_get_shadow_root_locs
.
locale l_get_shadow_root_defs =
fixes get_shadow_root :: "(_) element_ptr ==> (_, (_) shadow_root_ptr option) dom_prog"
fixes get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
locale l_get_shadow_rootShadow_DOM =
l_get_shadow_rootShadow_DOM_defs +
l_get_shadow_root_defs get_shadow_root get_shadow_root_locs +
l_type_wf type_wf
for type_wf :: "(_) heap ==> bool"
and get_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set" +
assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
assumes get_shadow_root_impl: "get_shadow_root = a_get_shadow_root"
assumes get_shadow_root_locs_impl: "get_shadow_root_locs = a_get_shadow_root_locs"
begin
lemmas get_shadow_root_def = get_shadow_root_impl[unfolded get_shadow_root_def a_get_shadow_root_def]
lemmas get_shadow_root_locs_def = get_shadow_root_locs_impl[unfolded get_shadow_root_locs_def
a_get_shadow_root_locs_def]
lemma get_shadow_root_ok:
"type_wf h ==> element_ptr |∈| element_ptr_kinds h ==> h ⊨ ok (get_shadow_root element_ptr)"
unfolding get_shadow_root_def type_wf_impl
using ShadowRootMonad.get_MElement_ok by blast
lemma get_shadow_root_pure [simp]: "pure (get_shadow_root element_ptr) h"
unfolding get_shadow_root_def by simp
lemma get_shadow_root_ptr_in_heap:
assumes "h ⊨ get_shadow_root element_ptr →r children"
shows "element_ptr |∈| element_ptr_kinds h"
using assms
by(auto simp add: get_shadow_root_def get_MElement_ptr_in_heap dest: is_OK_returns_result_I)
lemma get_shadow_root_reads:
"reads (get_shadow_root_locs element_ptr) (get_shadow_root element_ptr) h h'"
by(simp add: get_shadow_root_def get_shadow_root_locs_def reads_bind_pure
reads_insert_writes_set_right)
end
interpretation i_get_shadow_root?: l_get_shadow_rootShadow_DOM type_wf get_shadow_root
get_shadow_root_locs
using instances
by (auto simp add: l_get_shadow_rootShadow_DOM_def)
declare l_get_shadow_rootShadow_DOM_axioms [instances]
locale l_get_shadow_root = l_type_wf + l_get_shadow_root_defs +
assumes get_shadow_root_reads:
"reads (get_shadow_root_locs element_ptr) (get_shadow_root element_ptr) h h'"
assumes get_shadow_root_ok:
"type_wf h ==> element_ptr |∈| element_ptr_kinds h ==> h ⊨ ok (get_shadow_root element_ptr)"
assumes get_shadow_root_ptr_in_heap:
"h ⊨ ok (get_shadow_root element_ptr) ==> element_ptr |∈| element_ptr_kinds h"
assumes get_shadow_root_pure [simp]:
"pure (get_shadow_root element_ptr) h"
lemma get_shadow_root_is_l_get_shadow_root [instances]:
"l_get_shadow_root type_wf get_shadow_root get_shadow_root_locs"
using instances
unfolding l_get_shadow_root_def
by (metis (no_types, lifting) ElementClass.l_type_wfElement_axioms get_shadow_root_ok get_shadow_root_pure get_shadow_root_reads l_get_MElement_lemmas.get_MElement_ptr_in_heap l_get_MElement_lemmas.intro l_get_shadow_rootShadow_DOM.get_shadow_root_def)
paragraph ‹set\_disconnected\_nodes›
locale l_set_disconnected_nodes_get_shadow_rootShadow_DOM =
l_set_disconnected_nodesCore_DOM type_wfCore_DOM set_disconnected_nodes set_disconnected_nodes_locs +
l_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
for type_wf :: "(_) heap ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and set_disconnected_nodes
:: "(_) document_ptr ==> (_) node_ptr list ==> ((_) heap, exception, unit) prog"
and set_disconnected_nodes_locs :: "(_) document_ptr ==> ((_) heap, exception, unit) prog set"
and get_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
lemma set_disconnected_nodes_get_shadow_root:
"∀w ∈ set_disconnected_nodes_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_shadow_root_locs ptr'. r h h'))"
by(auto simp add: set_disconnected_nodes_locs_def get_shadow_root_locs_def all_args_def)
end
locale l_set_disconnected_nodes_get_shadow_root =
l_set_disconnected_nodes_defs +
l_get_shadow_root_defs +
assumes set_disconnected_nodes_get_shadow_root:
"∀w ∈ set_disconnected_nodes_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_shadow_root_locs ptr'. r h h'))"
interpretation
i_set_disconnected_nodes_get_shadow_root?: l_set_disconnected_nodes_get_shadow_rootShadow_DOM
type_wf DocumentClass.type_wf set_disconnected_nodes set_disconnected_nodes_locs get_shadow_root
get_shadow_root_locs
by(auto simp add: l_set_disconnected_nodes_get_shadow_rootShadow_DOM_def instances)
declare l_set_disconnected_nodes_get_shadow_rootShadow_DOM_axioms[instances]
lemma set_disconnected_nodes_get_shadow_root_is_l_set_disconnected_nodes_get_shadow_root [instances]:
"l_set_disconnected_nodes_get_shadow_root set_disconnected_nodes_locs get_shadow_root_locs"
apply(auto simp add: l_set_disconnected_nodes_get_shadow_root_def)[1]
using set_disconnected_nodes_get_shadow_root apply fast
done
paragraph ‹set\_tag\_type›
locale l_set_tag_name_get_shadow_rootCore_DOM =
l_set_tag_nameShadow_DOM +
l_get_shadow_rootShadow_DOM
begin
lemma set_tag_name_get_shadow_root:
"∀w ∈ set_tag_name_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_shadow_root_locs ptr'. r h h'))"
by(auto simp add: set_tag_name_locs_def
get_shadow_root_locs_def all_args_def
intro: element_put_get_preserved[where setter=tag_name_update and getter=shadow_root_opt])
end
locale l_set_tag_name_get_shadow_root = l_set_tag_name + l_get_shadow_root +
assumes set_tag_name_get_shadow_root:
"∀w ∈ set_tag_name_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_shadow_root_locs ptr'. r h h'))"
interpretation
i_set_tag_name_get_shadow_root?: l_set_tag_name_get_shadow_rootCore_DOM type_wf DocumentClass.type_wf
set_tag_name set_tag_name_locs
get_shadow_root get_shadow_root_locs
apply(auto simp add: l_set_tag_name_get_shadow_rootCore_DOM_def instances)[1]
using l_set_tag_nameShadow_DOM_axioms
by unfold_locales
declare l_set_tag_name_get_shadow_rootCore_DOM_axioms[instances]
lemma set_tag_name_get_shadow_root_is_l_set_tag_name_get_shadow_root [instances]:
"l_set_tag_name_get_shadow_root type_wf set_tag_name set_tag_name_locs get_shadow_root
get_shadow_root_locs"
using set_tag_name_is_l_set_tag_name get_shadow_root_is_l_get_shadow_root
apply(simp add: l_set_tag_name_get_shadow_root_def l_set_tag_name_get_shadow_root_axioms_def)
using set_tag_name_get_shadow_root
by fast
paragraph ‹set\_child\_nodes›
locale l_set_child_nodes_get_shadow_rootShadow_DOM =
l_set_child_nodesShadow_DOM type_wf known_ptr type_wfCore_DOM known_ptrCore_DOM set_child_nodes
set_child_nodes_locs set_child_nodesCore_DOM set_child_nodes_locsCore_DOM +
l_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
for type_wf :: "(_) heap ==> bool"
and known_ptr :: "(_) object_ptr ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and known_ptrCore_DOM :: "(_) object_ptr ==> bool"
and set_child_nodes :: "(_) object_ptr ==> (_) node_ptr list ==> ((_) heap, exception, unit) prog"
and set_child_nodes_locs :: "(_) object_ptr ==> ((_) heap, exception, unit) prog set"
and set_child_nodesCore_DOM :: "(_) object_ptr ==> (_) node_ptr list ==> ((_) heap, exception, unit) prog"
and set_child_nodes_locsCore_DOM :: "(_) object_ptr ==> ((_) heap, exception, unit) prog set"
and get_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
lemma set_child_nodes_get_shadow_root: "∀w ∈ set_child_nodes_locs ptr. (h ⊨ w →h h' ⟶
(∀r ∈ get_shadow_root_locs ptr'. r h h'))"
apply(auto simp add: set_child_nodes_locs_def get_shadow_root_locs_def CD.set_child_nodes_locs_def
all_args_def)[1]
by(auto intro!: element_put_get_preserved[where getter=shadow_root_opt and
setter=RElement.child_nodes_update])
end
locale l_set_child_nodes_get_shadow_root = l_set_child_nodes_defs + l_get_shadow_root_defs +
assumes set_child_nodes_get_shadow_root:
"∀w ∈ set_child_nodes_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_shadow_root_locs ptr'. r h h'))"
interpretation
i_set_child_nodes_get_shadow_root?: l_set_child_nodes_get_shadow_rootShadow_DOM type_wf known_ptr
DocumentClass.type_wf DocumentClass.known_ptr set_child_nodes set_child_nodes_locs
Core_DOM_Functions.set_child_nodes Core_DOM_Functions.set_child_nodes_locs get_shadow_root
get_shadow_root_locs
by(auto simp add: l_set_child_nodes_get_shadow_rootShadow_DOM_def instances)
declare l_set_child_nodes_get_shadow_rootShadow_DOM_axioms[instances]
lemma set_child_nodes_get_shadow_root_is_l_set_child_nodes_get_shadow_root [instances]:
"l_set_child_nodes_get_shadow_root set_child_nodes_locs get_shadow_root_locs"
apply(auto simp add: l_set_child_nodes_get_shadow_root_def)[1]
using set_child_nodes_get_shadow_root apply fast
done
paragraph ‹delete\_shadow\_root›
locale l_delete_shadow_root_get_shadow_rootShadow_DOM =
l_get_shadow_rootShadow_DOM
begin
lemma get_shadow_root_delete_shadow_root: "h ⊨ deleteShadowRoot_M shadow_root_ptr →h h'
==> r ∈ get_shadow_root_locs ptr' ==> r h h'"
by(auto simp add: get_shadow_root_locs_def delete_shadow_root_get_MElement)
end
locale l_delete_shadow_root_get_shadow_root = l_get_shadow_root_defs +
assumes get_shadow_root_delete_shadow_root: "h ⊨ deleteShadowRoot_M shadow_root_ptr →h h'
==> r ∈ get_shadow_root_locs ptr' ==> r h h'"
interpretation l_delete_shadow_root_get_shadow_rootShadow_DOM type_wf get_shadow_root
get_shadow_root_locs
by(auto simp add: l_delete_shadow_root_get_shadow_rootShadow_DOM_def instances)
lemma l_delete_shadow_root_get_shadow_root_get_shadow_root_locs [instances]: "l_delete_shadow_root_get_shadow_root get_shadow_root_locs"
apply(auto simp add: l_delete_shadow_root_get_shadow_root_def)[1]
using get_shadow_root_delete_shadow_root apply fast
done
paragraph ‹new\_character\_data›
locale l_new_character_data_get_shadow_rootShadow_DOM =
l_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
for type_wf :: "(_) heap ==> bool"
and get_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
lemma get_shadow_root_new_character_data:
"h ⊨ new_character_data →r new_character_data_ptr ==> h ⊨ new_character_data →h h'
==> r ∈ get_shadow_root_locs ptr' ==> r h h'"
by (auto simp add: get_shadow_root_locs_def new_character_data_get_MObject
new_character_data_get_MElement
split: prod.splits if_splits option.splits
elim!: bind_returns_result_E bind_returns_heap_E
intro: is_element_ptr_kind_obtains)
end
locale l_new_character_data_get_shadow_root = l_new_character_data + l_get_shadow_root +
assumes get_shadow_root_new_character_data:
"h ⊨ new_character_data →r new_character_data_ptr
==> h ⊨ new_character_data →h h' ==> r ∈ get_shadow_root_locs ptr' ==> r h h'"
interpretation i_new_character_data_get_shadow_root?:
l_new_character_data_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
by(unfold_locales)
declare l_new_character_data_get_shadow_rootShadow_DOM_axioms [instances]
lemma new_character_data_get_shadow_root_is_l_new_character_data_get_shadow_root [instances]:
"l_new_character_data_get_shadow_root type_wf get_shadow_root get_shadow_root_locs"
using new_character_data_is_l_new_character_data get_shadow_root_is_l_get_shadow_root
apply(auto simp add: l_new_character_data_get_shadow_root_def
l_new_character_data_get_shadow_root_axioms_def instances)[1]
using get_shadow_root_new_character_data
by fast
paragraph ‹new\_document›
locale l_new_document_get_shadow_rootShadow_DOM =
l_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
for type_wf :: "(_) heap ==> bool"
and get_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
lemma get_shadow_root_new_document:
"h ⊨ new_document →r new_document_ptr ==> h ⊨ new_document →h h'
==> r ∈ get_shadow_root_locs ptr' ==> r h h'"
by (auto simp add: get_shadow_root_locs_def new_document_get_MObject new_document_get_MElement
split: prod.splits if_splits option.splits
elim!: bind_returns_result_E bind_returns_heap_E intro: is_element_ptr_kind_obtains)
end
locale l_new_document_get_shadow_root = l_new_document + l_get_shadow_root +
assumes get_shadow_root_new_document:
"h ⊨ new_document →r new_document_ptr
==> h ⊨ new_document →h h' ==> r ∈ get_shadow_root_locs ptr' ==> r h h'"
interpretation i_new_document_get_shadow_root?:
l_new_document_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
by(unfold_locales)
declare l_new_document_get_shadow_rootShadow_DOM_axioms [instances]
lemma new_document_get_shadow_root_is_l_new_document_get_shadow_root [instances]:
"l_new_document_get_shadow_root type_wf get_shadow_root get_shadow_root_locs"
using new_document_is_l_new_document get_shadow_root_is_l_get_shadow_root
apply(auto simp add: l_new_document_get_shadow_root_def l_new_document_get_shadow_root_axioms_def
instances)[1]
using get_shadow_root_new_document
by fast
paragraph ‹new\_element›
locale l_new_element_get_shadow_rootShadow_DOM =
l_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
for type_wf :: "(_) heap ==> bool"
and get_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
lemma get_shadow_root_new_element:
"ptr' ≠ new_element_ptr ==> h ⊨ new_element →r new_element_ptr ==> h ⊨ new_element →h h'
==> r ∈ get_shadow_root_locs ptr' ==> r h h'"
by (auto simp add: get_shadow_root_locs_def new_element_get_MObject new_element_get_MElement
new_element_get_MDocument 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_shadow_root:
"h ⊨ new_element →r new_element_ptr ==> h ⊨ new_element →h h'
==> h' ⊨ get_shadow_root new_element_ptr →r None"
by(simp add: get_shadow_root_def new_element_shadow_root_opt)
end
locale l_new_element_get_shadow_root = l_new_element + l_get_shadow_root +
assumes get_shadow_root_new_element:
"ptr' ≠ new_element_ptr ==> h ⊨ new_element →r new_element_ptr
==> h ⊨ new_element →h h' ==> r ∈ get_shadow_root_locs ptr' ==> r h h'"
assumes new_element_no_shadow_root:
"h ⊨ new_element →r new_element_ptr ==> h ⊨ new_element →h h'
==> h' ⊨ get_shadow_root new_element_ptr →r None"
interpretation i_new_element_get_shadow_root?:
l_new_element_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
by(unfold_locales)
declare l_new_element_get_shadow_rootShadow_DOM_axioms [instances]
lemma new_element_get_shadow_root_is_l_new_element_get_shadow_root [instances]:
"l_new_element_get_shadow_root type_wf get_shadow_root get_shadow_root_locs"
using new_element_is_l_new_element get_shadow_root_is_l_get_shadow_root
apply(auto simp add: l_new_element_get_shadow_root_def l_new_element_get_shadow_root_axioms_def
instances)[1]
using get_shadow_root_new_element new_element_no_shadow_root
by fast+
paragraph ‹new\_shadow\_root›
locale l_new_shadow_root_get_shadow_rootShadow_DOM =
l_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
for type_wf :: "(_) heap ==> bool"
and get_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
lemma get_shadow_root_new_shadow_root:
"h ⊨ newShadowRoot_M →r new_shadow_root_ptr ==> h ⊨ newShadowRoot_M →h h'
==> r ∈ get_shadow_root_locs ptr' ==> r h h'"
by (auto simp add: get_shadow_root_locs_def new_shadow_root_get_MObject new_shadow_root_get_MElement
split: prod.splits if_splits option.splits
elim!: bind_returns_result_E bind_returns_heap_E intro: is_element_ptr_kind_obtains)
end
locale l_new_shadow_root_get_shadow_root = l_get_shadow_root +
assumes get_shadow_root_new_shadow_root:
"h ⊨ newShadowRoot_M →r new_shadow_root_ptr
==> h ⊨ newShadowRoot_M →h h' ==> r ∈ get_shadow_root_locs ptr' ==> r h h'"
interpretation i_new_shadow_root_get_shadow_root?:
l_new_shadow_root_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
by(unfold_locales)
declare l_new_shadow_root_get_shadow_rootShadow_DOM_axioms [instances]
lemma new_shadow_root_get_shadow_root_is_l_new_shadow_root_get_shadow_root [instances]:
"l_new_shadow_root_get_shadow_root type_wf get_shadow_root get_shadow_root_locs"
using get_shadow_root_is_l_get_shadow_root
apply(auto simp add: l_new_shadow_root_get_shadow_root_def
l_new_shadow_root_get_shadow_root_axioms_def instances)[1]
using get_shadow_root_new_shadow_root
by fast
subsubsection ‹set\_shadow\_root›
locale l_set_shadow_rootShadow_DOM_defs
begin
definition a_set_shadow_root :: "(_) element_ptr ==> (_) shadow_root_ptr option ==> (_, unit) dom_prog"
where
"a_set_shadow_root element_ptr = put_M element_ptr shadow_root_opt_update"
definition a_set_shadow_root_locs :: "(_) element_ptr ==> ((_, unit) dom_prog) set"
where
"a_set_shadow_root_locs element_ptr ≡ all_args (put_M element_ptr shadow_root_opt_update)"
end
global_interpretation l_set_shadow_rootShadow_DOM_defs
defines set_shadow_root = a_set_shadow_root
and set_shadow_root_locs = a_set_shadow_root_locs
.
locale l_set_shadow_root_defs =
fixes set_shadow_root :: "(_) element_ptr ==> (_) shadow_root_ptr option ==> (_, unit) dom_prog"
fixes set_shadow_root_locs :: "(_) element_ptr ==> (_, unit) dom_prog set"
locale l_set_shadow_rootShadow_DOM =
l_type_wf type_wf +
l_set_shadow_root_defs set_shadow_root set_shadow_root_locs +
l_set_shadow_rootShadow_DOM_defs
for type_wf :: "(_) heap ==> bool"
and set_shadow_root :: "(_) element_ptr ==> (_) shadow_root_ptr option ==> (_, unit) dom_prog"
and set_shadow_root_locs :: "(_) element_ptr ==> (_, unit) dom_prog set" +
assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
assumes set_shadow_root_impl: "set_shadow_root = a_set_shadow_root"
assumes set_shadow_root_locs_impl: "set_shadow_root_locs = a_set_shadow_root_locs"
begin
lemmas set_shadow_root_def = set_shadow_root_impl[unfolded set_shadow_root_def
a_set_shadow_root_def]
lemmas set_shadow_root_locs_def = set_shadow_root_locs_impl[unfolded set_shadow_root_locs_def
a_set_shadow_root_locs_def]
lemma set_shadow_root_ok: "type_wf h ==> element_ptr |∈| element_ptr_kinds h ==>
h ⊨ ok (set_shadow_root element_ptr tag)"
apply(unfold type_wf_impl)
unfolding set_shadow_root_def using get_MElement_ok put_MElement_ok
by (simp add: ShadowRootMonad.put_MElement_ok)
lemma set_shadow_root_ptr_in_heap:
"h ⊨ ok (set_shadow_root element_ptr shadow_root) ==> element_ptr |∈| element_ptr_kinds h"
by(simp add: set_shadow_root_def ElementMonad.put_M_ptr_in_heap)
lemma set_shadow_root_writes:
"writes (set_shadow_root_locs element_ptr) (set_shadow_root element_ptr tag) h h'"
by(auto simp add: set_shadow_root_def set_shadow_root_locs_def intro: writes_bind_pure)
lemma set_shadow_root_pointers_preserved:
assumes "w ∈ set_shadow_root_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_shadow_root_locs_def split: if_splits)
lemma set_shadow_root_types_preserved:
assumes "w ∈ set_shadow_root_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_shadow_root_locs_def split: if_splits)
end
interpretation i_set_shadow_root?: l_set_shadow_rootShadow_DOM type_wf set_shadow_root
set_shadow_root_locs
by (auto simp add: l_set_shadow_rootShadow_DOM_def instances)
declare l_set_shadow_rootShadow_DOM_axioms [instances]
locale l_set_shadow_root = l_type_wf +l_set_shadow_root_defs +
assumes set_shadow_root_writes:
"writes (set_shadow_root_locs element_ptr) (set_shadow_root element_ptr disc_nodes) h h'"
assumes set_shadow_root_ok:
"type_wf h ==> element_ptr |∈| element_ptr_kinds h ==>
h ⊨ ok (set_shadow_root element_ptr shadow_root)"
assumes set_shadow_root_ptr_in_heap:
"h ⊨ ok (set_shadow_root element_ptr shadow_root) ==> element_ptr |∈| element_ptr_kinds h"
assumes set_shadow_root_pointers_preserved:
"w ∈ set_shadow_root_locs element_ptr ==> h ⊨ w →h h' ==>
object_ptr_kinds h = object_ptr_kinds h'"
assumes set_shadow_root_types_preserved:
"w ∈ set_shadow_root_locs element_ptr ==> h ⊨ w →h h' ==> type_wf h = type_wf h'"
lemma set_shadow_root_is_l_set_shadow_root [instances]:
"l_set_shadow_root type_wf set_shadow_root set_shadow_root_locs"
apply(auto simp add: l_set_shadow_root_def instances)[1]
using set_shadow_root_writes apply blast
using set_shadow_root_ok apply (blast)
using set_shadow_root_ptr_in_heap apply blast
using set_shadow_root_pointers_preserved apply(blast, blast)
using set_shadow_root_types_preserved apply(blast, blast)
done
paragraph ‹get\_shadow\_root›
locale l_set_shadow_root_get_shadow_rootShadow_DOM =
l_set_shadow_rootShadow_DOM +
l_get_shadow_rootShadow_DOM
begin
lemma set_shadow_root_get_shadow_root:
"type_wf h ==> h ⊨ set_shadow_root ptr shadow_root_ptr_opt →h h' ==>
h' ⊨ get_shadow_root ptr →r shadow_root_ptr_opt"
by(auto simp add: set_shadow_root_def get_shadow_root_def)
lemma set_shadow_root_get_shadow_root_different_pointers: "ptr ≠ ptr' ==>
∀w ∈ set_shadow_root_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_shadow_root_locs ptr'. r h h'))"
by(auto simp add: set_shadow_root_locs_def get_shadow_root_locs_def all_args_def)
end
interpretation i_set_shadow_root_get_shadow_root?: l_set_shadow_root_get_shadow_rootShadow_DOM type_wf
set_shadow_root set_shadow_root_locs get_shadow_root get_shadow_root_locs
apply(auto simp add: l_set_shadow_root_get_shadow_rootShadow_DOM_def instances)[1]
by(unfold_locales)
declare l_set_shadow_root_get_shadow_rootShadow_DOM_axioms[instances]
locale l_set_shadow_root_get_shadow_root =
l_type_wf +
l_set_shadow_root_defs +
l_get_shadow_root_defs +
assumes set_shadow_root_get_shadow_root:
"type_wf h ==> h ⊨ set_shadow_root ptr shadow_root_ptr_opt →h h' ==>
h' ⊨ get_shadow_root ptr →r shadow_root_ptr_opt"
assumes set_shadow_root_get_shadow_root_different_pointers:
"ptr ≠ ptr' ==> w ∈ set_shadow_root_locs ptr ==> h ⊨ w →h h' ==>
r ∈ get_shadow_root_locs ptr' ==> r h h'"
lemma set_shadow_root_get_shadow_root_is_l_set_shadow_root_get_shadow_root [instances]:
"l_set_shadow_root_get_shadow_root type_wf set_shadow_root set_shadow_root_locs get_shadow_root
get_shadow_root_locs"
apply(auto simp add: l_set_shadow_root_get_shadow_root_def instances)[1]
using set_shadow_root_get_shadow_root apply fast
using set_shadow_root_get_shadow_root_different_pointers apply fast
done
subsubsection ‹set\_mode›
locale l_set_modeShadow_DOM_defs
begin
definition a_set_mode :: "(_) shadow_root_ptr ==> shadow_root_mode ==> (_, unit) dom_prog"
where
"a_set_mode shadow_root_ptr = put_M shadow_root_ptr mode_update"
definition a_set_mode_locs :: "(_) shadow_root_ptr ==> ((_, unit) dom_prog) set"
where
"a_set_mode_locs shadow_root_ptr ≡ all_args (put_M shadow_root_ptr mode_update)"
end
global_interpretation l_set_modeShadow_DOM_defs
defines set_mode = a_set_mode
and set_mode_locs = a_set_mode_locs
.
locale l_set_mode_defs =
fixes set_mode :: "(_) shadow_root_ptr ==> shadow_root_mode ==> (_, unit) dom_prog"
fixes set_mode_locs :: "(_) shadow_root_ptr ==> (_, unit) dom_prog set"
locale l_set_modeShadow_DOM =
l_type_wf type_wf +
l_set_mode_defs set_mode set_mode_locs +
l_set_modeShadow_DOM_defs
for type_wf :: "(_) heap ==> bool"
and set_mode :: "(_) shadow_root_ptr ==> shadow_root_mode ==> (_, unit) dom_prog"
and set_mode_locs :: "(_) shadow_root_ptr ==> (_, unit) dom_prog set" +
assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
assumes set_mode_impl: "set_mode = a_set_mode"
assumes set_mode_locs_impl: "set_mode_locs = a_set_mode_locs"
begin
lemmas set_mode_def = set_mode_impl[unfolded set_mode_def a_set_mode_def]
lemmas set_mode_locs_def = set_mode_locs_impl[unfolded set_mode_locs_def a_set_mode_locs_def]
lemma set_mode_ok:
"type_wf h ==> shadow_root_ptr |∈| shadow_root_ptr_kinds h ==>
h ⊨ ok (set_mode shadow_root_ptr shadow_root_mode)"
apply(unfold type_wf_impl)
unfolding set_mode_def using get_MShadowRoot_ok put_MShadowRoot_ok
by (simp add: ShadowRootMonad.put_MShadowRoot_ok)
lemma set_mode_ptr_in_heap:
"h ⊨ ok (set_mode shadow_root_ptr shadow_root_mode) ==>
shadow_root_ptr |∈| shadow_root_ptr_kinds h"
by(simp add: set_mode_def put_M_ptr_in_heap)
lemma set_mode_writes:
"writes (set_mode_locs shadow_root_ptr) (set_mode shadow_root_ptr shadow_root_mode) h h'"
by(auto simp add: set_mode_def set_mode_locs_def intro: writes_bind_pure)
lemma set_mode_pointers_preserved:
assumes "w ∈ set_mode_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_mode_locs_def split: if_splits)
lemma set_mode_types_preserved:
assumes "w ∈ set_mode_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_mode_locs_def split: if_splits)
end
interpretation i_set_mode?: l_set_modeShadow_DOM type_wf set_mode set_mode_locs
by (auto simp add: l_set_modeShadow_DOM_def instances)
declare l_set_modeShadow_DOM_axioms [instances]
locale l_set_mode = l_type_wf +l_set_mode_defs +
assumes set_mode_writes:
"writes (set_mode_locs shadow_root_ptr) (set_mode shadow_root_ptr shadow_root_mode) h h'"
assumes set_mode_ok:
"type_wf h ==> shadow_root_ptr |∈| shadow_root_ptr_kinds h ==>
h ⊨ ok (set_mode shadow_root_ptr shadow_root_mode)"
assumes set_mode_ptr_in_heap:
"h ⊨ ok (set_mode shadow_root_ptr shadow_root_mode) ==>
shadow_root_ptr |∈| shadow_root_ptr_kinds h"
assumes set_mode_pointers_preserved:
"w ∈ set_mode_locs shadow_root_ptr ==>
h ⊨ w →h h' ==> object_ptr_kinds h = object_ptr_kinds h'"
assumes set_mode_types_preserved:
"w ∈ set_mode_locs shadow_root_ptr ==> h ⊨ w →h h' ==> type_wf h = type_wf h'"
lemma set_mode_is_l_set_mode [instances]: "l_set_mode type_wf set_mode set_mode_locs"
apply(auto simp add: l_set_mode_def instances)[1]
using set_mode_writes apply blast
using set_mode_ok apply (blast)
using set_mode_ptr_in_heap apply blast
using set_mode_pointers_preserved apply(blast, blast)
using set_mode_types_preserved apply(blast, blast)
done
paragraph ‹get\_child\_nodes›
locale l_set_shadow_root_get_child_nodesShadow_DOM =
l_get_child_nodesShadow_DOM +
l_set_shadow_rootShadow_DOM
begin
lemma set_shadow_root_get_child_nodes:
"∀w ∈ set_shadow_root_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_child_nodes_locs ptr'. r h h'))"
by(auto simp add: get_child_nodes_locs_def set_shadow_root_locs_def CD.get_child_nodes_locs_def
all_args_def
intro: element_put_get_preserved[where setter=shadow_root_opt_update])
end
interpretation i_set_shadow_root_get_child_nodes?: l_set_shadow_root_get_child_nodesShadow_DOM type_wf
known_ptr DocumentClass.type_wf DocumentClass.known_ptr get_child_nodes get_child_nodes_locs
Core_DOM_Functions.get_child_nodes Core_DOM_Functions.get_child_nodes_locs set_shadow_root
set_shadow_root_locs
by(unfold_locales)
declare l_set_shadow_root_get_child_nodesShadow_DOM_axioms[instances]
locale l_set_shadow_root_get_child_nodes = l_set_shadow_root + l_get_child_nodes +
assumes set_shadow_root_get_child_nodes:
"∀w ∈ set_shadow_root_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_child_nodes_locs ptr'. r h h'))"
lemma set_shadow_root_get_child_nodes_is_l_set_shadow_root_get_child_nodes [instances]:
"l_set_shadow_root_get_child_nodes type_wf set_shadow_root set_shadow_root_locs known_ptr
get_child_nodes get_child_nodes_locs"
apply(auto simp add: l_set_shadow_root_get_child_nodes_def
l_set_shadow_root_get_child_nodes_axioms_def instances)[1]
using set_shadow_root_get_child_nodes apply blast
done
paragraph ‹get\_shadow\_root›
locale l_set_mode_get_shadow_rootShadow_DOM =
l_set_modeShadow_DOM +
l_get_shadow_rootShadow_DOM
begin
lemma set_mode_get_shadow_root:
"∀w ∈ set_mode_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_shadow_root_locs ptr'. r h h'))"
by(auto simp add: set_mode_locs_def get_shadow_root_locs_def all_args_def)
end
interpretation
i_set_mode_get_shadow_root?: l_set_mode_get_shadow_rootShadow_DOM type_wf
set_mode set_mode_locs get_shadow_root
get_shadow_root_locs
by unfold_locales
declare l_set_mode_get_shadow_rootShadow_DOM_axioms[instances]
locale l_set_mode_get_shadow_root = l_set_mode + l_get_shadow_root +
assumes set_mode_get_shadow_root:
"∀w ∈ set_mode_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_shadow_root_locs ptr'. r h h'))"
lemma set_mode_get_shadow_root_is_l_set_mode_get_shadow_root [instances]:
"l_set_mode_get_shadow_root type_wf set_mode set_mode_locs get_shadow_root
get_shadow_root_locs"
using set_mode_is_l_set_mode get_shadow_root_is_l_get_shadow_root
apply(simp add: l_set_mode_get_shadow_root_def
l_set_mode_get_shadow_root_axioms_def)
using set_mode_get_shadow_root
by fast
paragraph ‹get\_child\_nodes›
locale l_set_mode_get_child_nodesShadow_DOM =
l_set_modeShadow_DOM +
l_get_child_nodesShadow_DOM
begin
lemma set_mode_get_child_nodes:
"∀w ∈ set_mode_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_child_nodes_locs ptr'. r h h'))"
by(auto simp add: get_child_nodes_locs_def CD.get_child_nodes_locs_def set_mode_locs_def
all_args_def)[1]
end
interpretation i_set_mode_get_child_nodes?: l_set_mode_get_child_nodesShadow_DOM type_wf set_mode
set_mode_locs known_ptr DocumentClass.type_wf DocumentClass.known_ptr get_child_nodes
get_child_nodes_locs Core_DOM_Functions.get_child_nodes Core_DOM_Functions.get_child_nodes_locs
by unfold_locales
declare l_set_mode_get_child_nodesShadow_DOM_axioms[instances]
locale l_set_mode_get_child_nodes = l_set_mode + l_get_child_nodes +
assumes set_mode_get_child_nodes:
"∀w ∈ set_mode_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_child_nodes_locs ptr'. r h h'))"
lemma set_mode_get_child_nodes_is_l_set_mode_get_child_nodes [instances]:
"l_set_mode_get_child_nodes type_wf set_mode set_mode_locs known_ptr get_child_nodes
get_child_nodes_locs"
using set_mode_is_l_set_mode get_child_nodes_is_l_get_child_nodes
apply(simp add: l_set_mode_get_child_nodes_def
l_set_mode_get_child_nodes_axioms_def)
using set_mode_get_child_nodes
by fast
subsubsection ‹get\_host›
locale l_get_hostShadow_DOM_defs =
l_get_shadow_root_defs get_shadow_root get_shadow_root_locs
for get_shadow_root
:: "(_::linorder) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
definition a_get_host :: "(_) shadow_root_ptr ==> (_, (_) element_ptr) dom_prog" where
"a_get_host shadow_root_ptr = do {
host_ptrs ← element_ptr_kinds_M 🍋 filter_M (λelement_ptr. do {
shadow_root_opt ← get_shadow_root element_ptr;
return (shadow_root_opt = Some shadow_root_ptr)
});
(case host_ptrs of host_ptr#[] ==> return host_ptr | _ ==> error HierarchyRequestError)
}"
definition "a_get_host_locs ≡ (∪element_ptr. (get_shadow_root_locs element_ptr)) ∪
(∪ptr. {preserved (get_MObject ptr RObject.nothing)})"
end
global_interpretation l_get_hostShadow_DOM_defs get_shadow_root get_shadow_root_locs
defines get_host = "a_get_host"
and get_host_locs = "a_get_host_locs"
.
locale l_get_host_defs =
fixes get_host :: "(_) shadow_root_ptr ==> (_, (_) element_ptr) dom_prog"
fixes get_host_locs :: "((_) heap ==> (_) heap ==> bool) set"
locale l_get_hostShadow_DOM =
l_get_hostShadow_DOM_defs +
l_get_host_defs +
l_get_shadow_root +
assumes get_host_impl: "get_host = a_get_host"
assumes get_host_locs_impl: "get_host_locs = a_get_host_locs"
begin
lemmas get_host_def = get_host_impl[unfolded a_get_host_def]
lemmas get_host_locs_def = get_host_locs_impl[unfolded a_get_host_locs_def]
lemma get_host_pure [simp]: "pure (get_host element_ptr) h"
by(auto simp add: get_host_def intro!: bind_pure_I filter_M_pure_I split: list.splits)
lemma get_host_reads: "reads get_host_locs (get_host element_ptr) h h'"
using get_shadow_root_reads[unfolded reads_def]
by(auto simp add: get_host_def get_host_locs_def
intro!: reads_bind_pure reads_subset[OF check_in_heap_reads] reads_subset[OF error_reads]
reads_subset[OF get_shadow_root_reads] reads_subset[OF return_reads]
reads_subset[OF element_ptr_kinds_M_reads] filter_M_reads filter_M_pure_I
bind_pure_I
split: list.splits)
end
locale l_get_host = l_get_host_defs +
assumes get_host_pure [simp]: "pure (get_host element_ptr) h"
assumes get_host_reads: "reads get_host_locs (get_host node_ptr) h h'"
interpretation i_get_host?: l_get_hostShadow_DOM get_shadow_root get_shadow_root_locs get_host
get_host_locs type_wf
using instances
by (simp add: l_get_hostShadow_DOM_def l_get_hostShadow_DOM_axioms_def get_host_def get_host_locs_def)
declare l_get_hostShadow_DOM_axioms [instances]
lemma get_host_is_l_get_host [instances]: "l_get_host get_host get_host_locs"
apply(auto simp add: l_get_host_def)[1]
using get_host_reads apply fast
done
subsubsection ‹get\_mode›
locale l_get_modeShadow_DOM_defs
begin
definition a_get_mode :: "(_) shadow_root_ptr ==> (_, shadow_root_mode) dom_prog"
where
"a_get_mode shadow_root_ptr = get_M shadow_root_ptr mode"
definition a_get_mode_locs :: "(_) shadow_root_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
where
"a_get_mode_locs shadow_root_ptr ≡ {preserved (get_M shadow_root_ptr mode)}"
end
global_interpretation l_get_modeShadow_DOM_defs
defines get_mode = a_get_mode
and get_mode_locs = a_get_mode_locs
.
locale l_get_mode_defs =
fixes get_mode :: "(_) shadow_root_ptr ==> (_, shadow_root_mode) dom_prog"
fixes get_mode_locs :: "(_) shadow_root_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
locale l_get_modeShadow_DOM =
l_get_modeShadow_DOM_defs +
l_get_mode_defs get_mode get_mode_locs +
l_type_wf type_wf
for get_mode :: "(_) shadow_root_ptr ==> ((_) heap, exception, shadow_root_mode) prog"
and get_mode_locs :: "(_) shadow_root_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and type_wf :: "(_) heap ==> bool" +
assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
assumes get_mode_impl: "get_mode = a_get_mode"
assumes get_mode_locs_impl: "get_mode_locs = a_get_mode_locs"
begin
lemmas get_mode_def = get_mode_impl[unfolded get_mode_def a_get_mode_def]
lemmas get_mode_locs_def = get_mode_locs_impl[unfolded get_mode_locs_def a_get_mode_locs_def]
lemma get_mode_ok: "type_wf h ==> shadow_root_ptr |∈| shadow_root_ptr_kinds h ==>
h ⊨ ok (get_mode shadow_root_ptr)"
unfolding get_mode_def type_wf_impl
using ShadowRootMonad.get_MShadowRoot_ok by blast
lemma get_mode_pure [simp]: "pure (get_mode element_ptr) h"
unfolding get_mode_def by simp
lemma get_mode_ptr_in_heap:
assumes "h ⊨ get_mode shadow_root_ptr →r children"
shows "shadow_root_ptr |∈| shadow_root_ptr_kinds h"
using assms
by(auto simp add: get_mode_def get_MShadowRoot_ptr_in_heap dest: is_OK_returns_result_I)
lemma get_mode_reads: "reads (get_mode_locs element_ptr) (get_mode element_ptr) h h'"
by(simp add: get_mode_def get_mode_locs_def reads_bind_pure reads_insert_writes_set_right)
end
interpretation i_get_mode?: l_get_modeShadow_DOM get_mode get_mode_locs type_wf
using instances
by (auto simp add: l_get_modeShadow_DOM_def)
declare l_get_modeShadow_DOM_axioms [instances]
locale l_get_mode = l_type_wf + l_get_mode_defs +
assumes get_mode_reads: "reads (get_mode_locs shadow_root_ptr) (get_mode shadow_root_ptr) h h'"
assumes get_mode_ok:
"type_wf h ==> shadow_root_ptr |∈| shadow_root_ptr_kinds h ==> h ⊨ ok (get_mode shadow_root_ptr)"
assumes get_mode_ptr_in_heap:
"h ⊨ ok (get_mode shadow_root_ptr) ==> shadow_root_ptr |∈| shadow_root_ptr_kinds h"
assumes get_mode_pure [simp]: "pure (get_mode shadow_root_ptr) h"
lemma get_mode_is_l_get_mode [instances]: "l_get_mode type_wf get_mode get_mode_locs"
apply(auto simp add: l_get_mode_def instances)[1]
using get_mode_reads apply blast
using get_mode_ok apply blast
using get_mode_ptr_in_heap apply blast
done
subsubsection ‹get\_shadow\_root\_safe›
locale l_get_shadow_root_safeShadow_DOM_defs =
l_get_shadow_root_defs get_shadow_root get_shadow_root_locs +
l_get_mode_defs get_mode get_mode_locs
for get_shadow_root :: "(_) element_ptr ==> (_, (_) shadow_root_ptr option) dom_prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_mode :: "(_) shadow_root_ptr ==> (_, shadow_root_mode) dom_prog"
and get_mode_locs :: "(_) shadow_root_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
definition a_get_shadow_root_safe :: "(_) element_ptr ==> (_, (_) shadow_root_ptr option) dom_prog"
where
"a_get_shadow_root_safe element_ptr = do {
shadow_root_ptr_opt ← get_shadow_root element_ptr;
(case shadow_root_ptr_opt of
Some shadow_root_ptr ==> do {
mode ← get_mode shadow_root_ptr;
(if mode = Open then
return (Some shadow_root_ptr)
else
return None
)
} | None ==> return None)
}"
definition a_get_shadow_root_safe_locs
:: "(_) element_ptr ==> (_) shadow_root_ptr ==> ((_) heap ==> (_) heap ==> bool) set" where
"a_get_shadow_root_safe_locs element_ptr shadow_root_ptr ≡
(get_shadow_root_locs element_ptr) ∪ (get_mode_locs shadow_root_ptr)"
end
global_interpretation l_get_shadow_root_safeShadow_DOM_defs get_shadow_root get_shadow_root_locs
get_mode get_mode_locs
defines get_shadow_root_safe = a_get_shadow_root_safe
and get_shadow_root_safe_locs = a_get_shadow_root_safe_locs
.
locale l_get_shadow_root_safe_defs =
fixes get_shadow_root_safe :: "(_) element_ptr ==> (_, (_) shadow_root_ptr option) dom_prog"
fixes get_shadow_root_safe_locs ::
"(_) element_ptr ==> (_) shadow_root_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
locale l_get_shadow_root_safeShadow_DOM =
l_get_shadow_root_safeShadow_DOM_defs get_shadow_root get_shadow_root_locs get_mode get_mode_locs +
l_get_shadow_root_safe_defs get_shadow_root_safe get_shadow_root_safe_locs +
l_get_shadow_root type_wf get_shadow_root get_shadow_root_locs +
l_get_mode type_wf get_mode get_mode_locs +
l_type_wf type_wf
for type_wf :: "(_) heap ==> bool"
and get_shadow_root_safe ::
"(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_safe_locs ::
"(_) element_ptr ==> (_) shadow_root_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_shadow_root :: "(_) element_ptr ==> (_, (_) shadow_root_ptr option) dom_prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_mode :: "(_) shadow_root_ptr ==> (_, shadow_root_mode) dom_prog"
and get_mode_locs :: "(_) shadow_root_ptr ==> ((_) heap ==> (_) heap ==> bool) set" +
assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
assumes get_shadow_root_safe_impl: "get_shadow_root_safe = a_get_shadow_root_safe"
assumes get_shadow_root_safe_locs_impl: "get_shadow_root_safe_locs = a_get_shadow_root_safe_locs"
begin
lemmas get_shadow_root_safe_def =
get_shadow_root_safe_impl[unfolded get_shadow_root_safe_def a_get_shadow_root_safe_def]
lemmas get_shadow_root_safe_locs_def =
get_shadow_root_safe_locs_impl[unfolded get_shadow_root_safe_locs_def a_get_shadow_root_safe_locs_def]
lemma get_shadow_root_safe_pure [simp]: "pure (get_shadow_root_safe element_ptr) h"
by (auto simp add: get_shadow_root_safe_def bind_pure_I option.case_eq_if)
end
interpretation i_get_shadow_root_safe?: l_get_shadow_root_safeShadow_DOM type_wf get_shadow_root_safe
get_shadow_root_safe_locs get_shadow_root get_shadow_root_locs get_mode get_mode_locs
using instances
by (auto simp add: l_get_shadow_root_safeShadow_DOM_def l_get_shadow_root_safeShadow_DOM_axioms_def
get_shadow_root_safe_def get_shadow_root_safe_locs_def)
declare l_get_shadow_root_safeShadow_DOM_axioms [instances]
locale l_get_shadow_root_safe = l_get_shadow_root_safe_defs +
assumes get_shadow_root_safe_pure [simp]: "pure (get_shadow_root_safe element_ptr) h"
lemma get_shadow_root_safe_is_l_get_shadow_root_safe [instances]:
"l_get_shadow_root_safe get_shadow_root_safe"
using instances
apply(auto simp add: l_get_shadow_root_safe_def)[1]
done
subsubsection ‹set\_disconnected\_nodes›
locale l_set_disconnected_nodesShadow_DOM =
CD: l_set_disconnected_nodesCore_DOM type_wfCore_DOM set_disconnected_nodes set_disconnected_nodes_locs +
l_type_wf type_wf
for type_wf :: "(_) heap ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and set_disconnected_nodes ::
"(_) document_ptr ==> (_) node_ptr list ==> ((_) heap, exception, unit) prog"
and set_disconnected_nodes_locs :: "(_) document_ptr ==> ((_) heap, exception, unit) prog set" +
assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
begin
lemma set_disconnected_nodes_ok:
"type_wf h ==> document_ptr |∈| document_ptr_kinds h ==>
h ⊨ ok (set_disconnected_nodes document_ptr node_ptrs)"
using CD.set_disconnected_nodes_ok CD.type_wf_impl ShadowRootClass.type_wf_defs local.type_wf_impl
by blast
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 CD.set_disconnected_nodes_locs_def split: if_splits)
end
interpretation i_set_disconnected_nodes?: l_set_disconnected_nodesShadow_DOM type_wf
DocumentClass.type_wf set_disconnected_nodes set_disconnected_nodes_locs
by(auto simp add: l_set_disconnected_nodesShadow_DOM_def
l_set_disconnected_nodesShadow_DOM_axioms_def instances)
declare l_set_disconnected_nodesShadow_DOM_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(auto simp add: l_set_disconnected_nodes_def)[1]
apply (simp add: i_set_disconnected_nodes.set_disconnected_nodes_writes)
using set_disconnected_nodes_ok apply blast
apply (simp add: i_set_disconnected_nodes.set_disconnected_nodes_ptr_in_heap)
using i_set_disconnected_nodes.set_disconnected_nodes_pointers_preserved apply (blast, blast)
using set_disconnected_nodes_typess_preserved apply(blast, blast)
done
paragraph ‹get\_child\_nodes›
locale l_set_disconnected_nodes_get_child_nodesShadow_DOM =
l_set_disconnected_nodesCore_DOM type_wfCore_DOM set_disconnected_nodes set_disconnected_nodes_locs +
l_get_child_nodesShadow_DOM type_wf known_ptr type_wfCore_DOM known_ptrCore_DOM get_child_nodes
get_child_nodes_locs get_child_nodesCore_DOM get_child_nodes_locsCore_DOM
for type_wf :: "(_) heap ==> bool"
and set_disconnected_nodes :: "(_) document_ptr ==> (_) node_ptr list ==> ((_) heap, exception, unit)
prog"
and set_disconnected_nodes_locs :: "(_) document_ptr ==> ((_) heap, exception, unit) prog set"
and known_ptr :: "(_) object_ptr ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and known_ptrCore_DOM :: "(_) 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"
and get_child_nodesCore_DOM :: "(_) object_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locsCore_DOM :: "(_) object_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
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_def get_child_nodes_locs_def
CD.get_child_nodes_locs_def all_args_def)
end
interpretation i_set_disconnected_nodes_get_child_nodes?:
l_set_disconnected_nodes_get_child_nodesShadow_DOM type_wf set_disconnected_nodes
set_disconnected_nodes_locs known_ptr DocumentClass.type_wf DocumentClass.known_ptr get_child_nodes
get_child_nodes_locs Core_DOM_Functions.get_child_nodes Core_DOM_Functions.get_child_nodes_locs
by(auto simp add: l_set_disconnected_nodes_get_child_nodesShadow_DOM_def instances)
declare l_set_disconnected_nodes_get_child_nodesShadow_DOM_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"
apply(auto simp add: l_set_disconnected_nodes_get_child_nodes_def)[1]
using set_disconnected_nodes_get_child_nodes apply fast
done
paragraph ‹get\_host›
locale l_set_disconnected_nodes_get_hostShadow_DOM =
l_set_disconnected_nodesShadow_DOM +
l_get_shadow_rootShadow_DOM +
l_get_hostShadow_DOM
begin
lemma set_disconnected_nodes_get_host:
"∀w ∈ set_disconnected_nodes_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_host_locs. r h h'))"
by(auto simp add: CD.set_disconnected_nodes_locs_def get_shadow_root_locs_def get_host_locs_def all_args_def)
end
interpretation i_set_disconnected_nodes_get_host?: l_set_disconnected_nodes_get_hostShadow_DOM type_wf
DocumentClass.type_wf set_disconnected_nodes set_disconnected_nodes_locs get_shadow_root
get_shadow_root_locs get_host get_host_locs
by(auto simp add: l_set_disconnected_nodes_get_hostShadow_DOM_def instances)
declare l_set_disconnected_nodes_get_hostShadow_DOM_axioms [instances]
locale l_set_disconnected_nodes_get_host = l_set_disconnected_nodes_defs + l_get_host_defs +
assumes set_disconnected_nodes_get_host:
"∀w ∈ set_disconnected_nodes_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_host_locs. r h h'))"
lemma set_disconnected_nodes_get_host_is_l_set_disconnected_nodes_get_host [instances]:
"l_set_disconnected_nodes_get_host set_disconnected_nodes_locs get_host_locs"
apply(auto simp add: l_set_disconnected_nodes_get_host_def instances)[1]
using set_disconnected_nodes_get_host
by fast
subsubsection ‹get\_tag\_name›
locale l_get_tag_nameShadow_DOM =
CD: l_get_tag_nameCore_DOM type_wfCore_DOM get_tag_name get_tag_name_locs +
l_type_wf type_wf
for type_wf :: "(_) heap ==> bool"
and type_wfCore_DOM :: "(_) 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 = ShadowRootClass.type_wf"
begin
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 CD.get_tag_name_ok CD.type_wf_impl ShadowRootClass.type_wfDocument
by blast
end
interpretation i_get_tag_name?: l_get_tag_nameShadow_DOM type_wf DocumentClass.type_wf get_tag_name
get_tag_name_locs
by(auto simp add: l_get_tag_nameShadow_DOM_def l_get_tag_nameShadow_DOM_axioms_def instances)
declare l_get_tag_nameShadow_DOM_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(auto simp add: l_get_tag_name_def)[1]
using get_tag_name_reads apply fast
using get_tag_name_ok apply fast
done
paragraph ‹set\_disconnected\_nodes›
locale l_set_disconnected_nodes_get_tag_nameShadow_DOM =
l_set_disconnected_nodesShadow_DOM +
l_get_tag_nameShadow_DOM
begin
lemma 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'))"
by(auto simp add: CD.set_disconnected_nodes_locs_def CD.get_tag_name_locs_def all_args_def)
end
interpretation i_set_disconnected_nodes_get_tag_name?: l_set_disconnected_nodes_get_tag_nameShadow_DOM
type_wf DocumentClass.type_wf set_disconnected_nodes set_disconnected_nodes_locs get_tag_name
get_tag_name_locs
by(auto simp add: l_set_disconnected_nodes_get_tag_nameShadow_DOM_def instances)
declare l_set_disconnected_nodes_get_tag_nameShadow_DOM_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"
apply(auto simp add: l_set_disconnected_nodes_get_tag_name_def
l_set_disconnected_nodes_get_tag_name_axioms_def instances)[1]
using set_disconnected_nodes_get_tag_name
by fast
paragraph ‹set\_child\_nodes›
locale l_set_child_nodes_get_tag_nameShadow_DOM =
l_set_child_nodesShadow_DOM +
l_get_tag_nameShadow_DOM
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: CD.set_child_nodes_locs_def set_child_nodes_locs_def CD.get_tag_name_locs_def
all_args_def
intro: element_put_get_preserved[where getter=tag_name and
setter=RElement.child_nodes_update])
end
interpretation i_set_child_nodes_get_tag_name?: l_set_child_nodes_get_tag_nameShadow_DOM type_wf
known_ptr DocumentClass.type_wf DocumentClass.known_ptr set_child_nodes set_child_nodes_locs
Core_DOM_Functions.set_child_nodes Core_DOM_Functions.set_child_nodes_locs get_tag_name
get_tag_name_locs
by(auto simp add: l_set_child_nodes_get_tag_nameShadow_DOM_def instances)
declare l_set_child_nodes_get_tag_nameShadow_DOM_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"
apply(auto simp add: l_set_child_nodes_get_tag_name_def l_set_child_nodes_get_tag_name_axioms_def
instances)[1]
using set_child_nodes_get_tag_name
by fast
paragraph ‹delete\_shadow\_root›
locale l_delete_shadow_root_get_tag_nameShadow_DOM =
l_get_tag_nameShadow_DOM
begin
lemma get_tag_name_delete_shadow_root: "h ⊨ deleteShadowRoot_M shadow_root_ptr →h h'
==> r ∈ get_tag_name_locs ptr' ==> r h h'"
by(auto simp add: CD.get_tag_name_locs_def delete_shadow_root_get_MElement)
end
locale l_delete_shadow_root_get_tag_name = l_get_tag_name_defs +
assumes get_tag_name_delete_shadow_root: "h ⊨ deleteShadowRoot_M shadow_root_ptr →h h'
==> r ∈ get_tag_name_locs ptr' ==> r h h'"
interpretation l_delete_shadow_root_get_tag_nameShadow_DOM type_wf DocumentClass.type_wf get_tag_name
get_tag_name_locs
by(auto simp add: l_delete_shadow_root_get_tag_nameShadow_DOM_def instances)
lemma l_delete_shadow_root_get_tag_name_get_tag_name_locs [instances]: "l_delete_shadow_root_get_tag_name get_tag_name_locs"
apply(auto simp add: l_delete_shadow_root_get_tag_name_def)[1]
using get_tag_name_delete_shadow_root apply fast
done
paragraph ‹set\_shadow\_root›
locale l_set_shadow_root_get_tag_nameShadow_DOM =
l_set_shadow_rootShadow_DOM +
l_get_tag_nameShadow_DOM
begin
lemma set_shadow_root_get_tag_name:
"∀w ∈ set_shadow_root_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_tag_name_locs ptr'. r h h'))"
by(auto simp add: set_shadow_root_locs_def CD.get_tag_name_locs_def all_args_def
element_put_get_preserved[where setter=shadow_root_opt_update])
end
interpretation i_set_shadow_root_get_tag_name?: l_set_shadow_root_get_tag_nameShadow_DOM type_wf
set_shadow_root set_shadow_root_locs DocumentClass.type_wf get_tag_name get_tag_name_locs
apply(auto simp add: l_set_shadow_root_get_tag_nameShadow_DOM_def instances)[1]
by(unfold_locales)
declare l_set_shadow_root_get_tag_nameShadow_DOM_axioms[instances]
locale l_set_shadow_root_get_tag_name = l_set_shadow_root_defs + l_get_tag_name_defs +
assumes set_shadow_root_get_tag_name:
"∀w ∈ set_shadow_root_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_tag_name_locs ptr'. r h h'))"
lemma set_shadow_root_get_tag_name_is_l_set_shadow_root_get_tag_name [instances]:
"l_set_shadow_root_get_tag_name set_shadow_root_locs get_tag_name_locs"
using set_shadow_root_is_l_set_shadow_root get_tag_name_is_l_get_tag_name
apply(simp add: l_set_shadow_root_get_tag_name_def )
using set_shadow_root_get_tag_name
by fast
paragraph ‹new\_element›
locale l_new_element_get_tag_nameShadow_DOM =
l_get_tag_nameShadow_DOM type_wf type_wfCore_DOM get_tag_name get_tag_name_locs
for type_wf :: "(_) heap ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and get_tag_name :: "(_) element_ptr ==> (_, tag_name) dom_prog"
and get_tag_name_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
lemma get_tag_name_new_element:
"ptr' ≠ new_element_ptr ==> h ⊨ new_element →r new_element_ptr ==> h ⊨ new_element →h h'
==> r ∈ get_tag_name_locs ptr' ==> r h h'"
by (auto simp add: CD.get_tag_name_locs_def new_element_get_MObject new_element_get_MElement
new_element_get_MDocument 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_empty_tag_name:
"h ⊨ new_element →r new_element_ptr ==> h ⊨ new_element →h h'
==> h' ⊨ get_tag_name new_element_ptr →r ''''"
by(simp add: CD.get_tag_name_def new_element_tag_name)
end
locale l_new_element_get_tag_name = l_new_element + l_get_tag_name +
assumes get_tag_name_new_element:
"ptr' ≠ new_element_ptr ==> h ⊨ new_element →r new_element_ptr
==> h ⊨ new_element →h h' ==> r ∈ get_tag_name_locs ptr' ==> r h h'"
assumes new_element_empty_tag_name:
"h ⊨ new_element →r new_element_ptr ==> h ⊨ new_element →h h'
==> h' ⊨ get_tag_name new_element_ptr →r ''''"
interpretation i_new_element_get_tag_name?:
l_new_element_get_tag_nameShadow_DOM type_wf DocumentClass.type_wf get_tag_name get_tag_name_locs
by(auto simp add: l_new_element_get_tag_nameShadow_DOM_def instances)
declare l_new_element_get_tag_nameShadow_DOM_axioms [instances]
lemma new_element_get_tag_name_is_l_new_element_get_tag_name [instances]:
"l_new_element_get_tag_name type_wf get_tag_name get_tag_name_locs"
using new_element_is_l_new_element get_tag_name_is_l_get_tag_name
apply(auto simp add: l_new_element_get_tag_name_def l_new_element_get_tag_name_axioms_def
instances)[1]
using get_tag_name_new_element new_element_empty_tag_name
by fast+
paragraph ‹get\_shadow\_root›
locale l_set_mode_get_tag_nameShadow_DOM =
l_set_modeShadow_DOM +
l_get_tag_nameShadow_DOM
begin
lemma set_mode_get_tag_name:
"∀w ∈ set_mode_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_tag_name_locs ptr'. r h h'))"
by(auto simp add: set_mode_locs_def CD.get_tag_name_locs_def all_args_def)
end
interpretation
i_set_mode_get_tag_name?: l_set_mode_get_tag_nameShadow_DOM type_wf
set_mode set_mode_locs DocumentClass.type_wf get_tag_name
get_tag_name_locs
by unfold_locales
declare l_set_mode_get_tag_nameShadow_DOM_axioms[instances]
locale l_set_mode_get_tag_name = l_set_mode + l_get_tag_name +
assumes set_mode_get_tag_name:
"∀w ∈ set_mode_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_tag_name_locs ptr'. r h h'))"
lemma set_mode_get_tag_name_is_l_set_mode_get_tag_name [instances]:
"l_set_mode_get_tag_name type_wf set_mode set_mode_locs get_tag_name
get_tag_name_locs"
using set_mode_is_l_set_mode get_tag_name_is_l_get_tag_name
apply(simp add: l_set_mode_get_tag_name_def
l_set_mode_get_tag_name_axioms_def)
using set_mode_get_tag_name
by fast
paragraph ‹new\_document›
locale l_new_document_get_tag_nameShadow_DOM =
l_get_tag_nameShadow_DOM type_wf type_wfCore_DOM get_tag_name get_tag_name_locs
for type_wf :: "(_) heap ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and get_tag_name :: "(_) element_ptr ==> ((_) heap, exception, tag_name) prog"
and get_tag_name_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
lemma get_tag_name_new_document:
"h ⊨ new_document →r new_document_ptr ==> h ⊨ new_document →h h'
==> r ∈ get_tag_name_locs ptr' ==> r h h'"
by(auto simp add: CD.get_tag_name_locs_def new_document_get_MElement)
end
locale l_new_document_get_tag_name = l_get_tag_name_defs +
assumes get_tag_name_new_document:
"h ⊨ new_document →r new_document_ptr ==> h ⊨ new_document →h h'
==> r ∈ get_tag_name_locs ptr' ==> r h h'"
interpretation i_new_document_get_tag_name?:
l_new_document_get_tag_nameShadow_DOM type_wf DocumentClass.type_wf get_tag_name
get_tag_name_locs
by unfold_locales
declare l_new_document_get_tag_nameShadow_DOM_def[instances]
lemma new_document_get_tag_name_is_l_new_document_get_tag_name [instances]:
"l_new_document_get_tag_name get_tag_name_locs"
unfolding l_new_document_get_tag_name_def
unfolding get_tag_name_locs_def
using new_document_get_MElement by blast
paragraph ‹new\_shadow\_root›
locale l_new_shadow_root_get_tag_nameShadow_DOM =
l_get_tag_nameShadow_DOM
begin
lemma get_tag_name_new_shadow_root:
"h ⊨ newShadowRoot_M →r new_shadow_root_ptr ==> h ⊨ newShadowRoot_M →h h'
==> r ∈ get_tag_name_locs ptr' ==> r h h'"
by (auto simp add: CD.get_tag_name_locs_def new_shadow_root_get_MObject new_shadow_root_get_MElement
split: prod.splits if_splits option.splits
elim!: bind_returns_result_E bind_returns_heap_E intro: is_element_ptr_kind_obtains)
end
locale l_new_shadow_root_get_tag_name = l_get_tag_name +
assumes get_tag_name_new_shadow_root:
"h ⊨ newShadowRoot_M →r new_shadow_root_ptr
==> h ⊨ newShadowRoot_M →h h' ==> r ∈ get_tag_name_locs ptr' ==> r h h'"
interpretation i_new_shadow_root_get_tag_name?:
l_new_shadow_root_get_tag_nameShadow_DOM type_wf DocumentClass.type_wf get_tag_name get_tag_name_locs
by(unfold_locales)
declare l_new_shadow_root_get_tag_nameShadow_DOM_axioms [instances]
lemma new_shadow_root_get_tag_name_is_l_new_shadow_root_get_tag_name [instances]:
"l_new_shadow_root_get_tag_name type_wf get_tag_name get_tag_name_locs"
using get_tag_name_is_l_get_tag_name
apply(auto simp add: l_new_shadow_root_get_tag_name_def l_new_shadow_root_get_tag_name_axioms_def
instances)[1]
using get_tag_name_new_shadow_root
by fast
paragraph ‹new\_character\_data›
locale l_new_character_data_get_tag_nameShadow_DOM =
l_get_tag_nameShadow_DOM type_wf type_wfCore_DOM get_tag_name get_tag_name_locs
for type_wf :: "(_) heap ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and get_tag_name :: "(_) element_ptr ==> ((_) heap, exception, tag_name) prog"
and get_tag_name_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
lemma get_tag_name_new_character_data:
"h ⊨ new_character_data →r new_character_data_ptr ==> h ⊨ new_character_data →h h'
==> r ∈ get_tag_name_locs ptr' ==> r h h'"
by(auto simp add: CD.get_tag_name_locs_def new_character_data_get_MElement)
end
locale l_new_character_data_get_tag_name = l_get_tag_name_defs +
assumes get_tag_name_new_character_data:
"h ⊨ new_character_data →r new_character_data_ptr ==> h ⊨ new_character_data →h h'
==> r ∈ get_tag_name_locs ptr' ==> r h h'"
interpretation i_new_character_data_get_tag_name?:
l_new_character_data_get_tag_nameShadow_DOM type_wf DocumentClass.type_wf get_tag_name
get_tag_name_locs
by unfold_locales
declare l_new_character_data_get_tag_nameShadow_DOM_def[instances]
lemma new_character_data_get_tag_name_is_l_new_character_data_get_tag_name [instances]:
"l_new_character_data_get_tag_name get_tag_name_locs"
unfolding l_new_character_data_get_tag_name_def
unfolding get_tag_name_locs_def
using new_character_data_get_MElement by blast
paragraph ‹get\_tag\_type›
locale l_set_tag_name_get_tag_nameShadow_DOM = l_get_tag_nameShadow_DOM
+ l_set_tag_nameShadow_DOM
begin
lemma set_tag_name_get_tag_name:
assumes "h ⊨ CD.a_set_tag_name element_ptr tag →h h'"
shows "h' ⊨ CD.a_get_tag_name element_ptr →r tag"
using assms
by(auto simp add: CD.a_get_tag_name_def CD.a_set_tag_name_def)
lemma set_tag_name_get_tag_name_different_pointers:
assumes "ptr ≠ ptr'"
assumes "w ∈ CD.a_set_tag_name_locs ptr"
assumes "h ⊨ w →h h'"
assumes "r ∈ CD.a_get_tag_name_locs ptr'"
shows "r h h'"
using assms
by(auto simp add: all_args_def CD.a_set_tag_name_locs_def CD.a_get_tag_name_locs_def
split: if_splits option.splits )
end
interpretation i_set_tag_name_get_tag_name?:
l_set_tag_name_get_tag_nameShadow_DOM type_wf DocumentClass.type_wf get_tag_name
get_tag_name_locs set_tag_name set_tag_name_locs
by unfold_locales
declare l_set_tag_name_get_tag_nameShadow_DOM_axioms[instances]
lemma set_tag_name_get_tag_name_is_l_set_tag_name_get_tag_name [instances]:
"l_set_tag_name_get_tag_name type_wf get_tag_name get_tag_name_locs
set_tag_name set_tag_name_locs"
using set_tag_name_is_l_set_tag_name get_tag_name_is_l_get_tag_name
apply(simp add: l_set_tag_name_get_tag_name_def
l_set_tag_name_get_tag_name_axioms_def)
using set_tag_name_get_tag_name
set_tag_name_get_tag_name_different_pointers
by fast+
subsubsection ‹attach\_shadow\_root›
locale l_attach_shadow_rootShadow_DOM_defs =
l_set_shadow_root_defs set_shadow_root set_shadow_root_locs +
l_set_mode_defs set_mode set_mode_locs +
l_get_tag_name_defs get_tag_name get_tag_name_locs +
l_get_shadow_root_defs get_shadow_root get_shadow_root_locs
for set_shadow_root ::
"(_) element_ptr ==> (_) shadow_root_ptr option ==> ((_) heap, exception, unit) prog"
and set_shadow_root_locs :: "(_) element_ptr ==> ((_) heap, exception, unit) prog set"
and set_mode :: "(_) shadow_root_ptr ==> shadow_root_mode ==> ((_) heap, exception, unit) prog"
and set_mode_locs :: "(_) shadow_root_ptr ==> ((_) heap, exception, unit) prog set"
and get_tag_name :: "(_) element_ptr ==> (_, char list) dom_prog"
and get_tag_name_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
definition a_attach_shadow_root ::
"(_) element_ptr ==> shadow_root_mode ==> (_, (_) shadow_root_ptr) dom_prog"
where
"a_attach_shadow_root element_ptr shadow_root_mode = do {
tag ← get_tag_name element_ptr;
(if tag ∉ safe_shadow_root_element_types then error NotSupportedError else return ());
prev_shadow_root ← get_shadow_root element_ptr;
(if prev_shadow_root ≠ None then error NotSupportedError else return ());
new_shadow_root_ptr ← newShadowRoot_M;
set_mode new_shadow_root_ptr shadow_root_mode;
set_shadow_root element_ptr (Some new_shadow_root_ptr);
return new_shadow_root_ptr
}"
end
locale l_attach_shadow_root_defs =
fixes attach_shadow_root ::
"(_) element_ptr ==> shadow_root_mode ==> (_, (_) shadow_root_ptr) dom_prog"
global_interpretation l_attach_shadow_rootShadow_DOM_defs set_shadow_root set_shadow_root_locs
set_mode set_mode_locs get_tag_name get_tag_name_locs get_shadow_root get_shadow_root_locs
defines attach_shadow_root = a_attach_shadow_root
.
locale l_attach_shadow_rootShadow_DOM =
l_attach_shadow_rootShadow_DOM_defs set_shadow_root set_shadow_root_locs set_mode set_mode_locs
get_tag_name get_tag_name_locs get_shadow_root get_shadow_root_locs +
l_attach_shadow_root_defs attach_shadow_root +
l_set_shadow_rootShadow_DOM type_wf set_shadow_root set_shadow_root_locs +
l_set_mode type_wf set_mode set_mode_locs +
l_get_tag_name type_wf get_tag_name get_tag_name_locs +
l_get_shadow_root type_wf get_shadow_root get_shadow_root_locs +
l_known_ptr known_ptr
for known_ptr :: "(_) object_ptr ==> bool"
and set_shadow_root ::
"(_) element_ptr ==> (_) shadow_root_ptr option ==> ((_) heap, exception, unit) prog"
and set_shadow_root_locs :: "(_) element_ptr ==> ((_) heap, exception, unit) prog set"
and set_mode :: "(_) shadow_root_ptr ==> shadow_root_mode ==> ((_) heap, exception, unit) prog"
and set_mode_locs :: "(_) shadow_root_ptr ==> ((_) heap, exception, unit) prog set"
and attach_shadow_root ::
"(_) element_ptr ==> shadow_root_mode ==> ((_) heap, exception, (_) shadow_root_ptr) prog"
and type_wf :: "(_) heap ==> bool"
and get_tag_name :: "(_) element_ptr ==> (_, char list) dom_prog"
and get_tag_name_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set" +
assumes known_ptr_impl: "known_ptr = a_known_ptr"
assumes attach_shadow_root_impl: "attach_shadow_root = a_attach_shadow_root"
begin
lemmas attach_shadow_root_def = a_attach_shadow_root_def[folded attach_shadow_root_impl]
lemma attach_shadow_root_element_ptr_in_heap:
assumes "h ⊨ ok (attach_shadow_root element_ptr shadow_root_mode)"
shows "element_ptr |∈| element_ptr_kinds h"
proof -
obtain h' where "h ⊨ attach_shadow_root element_ptr shadow_root_mode →h h'"
using assms by auto
then
obtain h2 h3 new_shadow_root_ptr where
h2: "h ⊨ newShadowRoot_M →h h2" and
new_shadow_root_ptr: "h ⊨ newShadowRoot_M →r new_shadow_root_ptr" and
h3: "h2 ⊨ set_mode new_shadow_root_ptr shadow_root_mode →h h3" and
"h3 ⊨ set_shadow_root element_ptr (Some new_shadow_root_ptr) →h h'"
by(auto simp add: attach_shadow_root_def
elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_tag_name_pure, rotated]
bind_returns_heap_E2[rotated, OF get_shadow_root_pure, rotated] split: if_splits)
then have "element_ptr |∈| element_ptr_kinds h3"
using set_shadow_root_ptr_in_heap by blast
moreover
have "object_ptr_kinds h2 = object_ptr_kinds h |∪| {|cast new_shadow_root_ptr|}"
using h2 newShadowRoot_M_new_ptr new_shadow_root_ptr by auto
moreover
have "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_mode_writes h3])
using set_mode_pointers_preserved
apply blast
by (auto simp add: reflp_def transp_def)
ultimately
show ?thesis
by(auto simp add: element_ptr_kinds_def node_ptr_kinds_def)
qed
lemma create_shadow_root_known_ptr:
assumes "h ⊨ attach_shadow_root element_ptr shadow_root_mode →r new_shadow_root_ptr"
shows "known_ptr (castshadow_root_ptr2object_ptr new_shadow_root_ptr)"
using assms
by(auto simp add: attach_shadow_root_def known_ptr_impl ShadowRootClass.a_known_ptr_def
newShadowRoot_M_def newShadowRoot_def Let_def
elim!: bind_returns_result_E)
end
locale l_attach_shadow_root = l_attach_shadow_root_defs
interpretation
i_attach_shadow_root?: l_attach_shadow_rootShadow_DOM known_ptr set_shadow_root set_shadow_root_locs
set_mode set_mode_locs attach_shadow_root type_wf get_tag_name get_tag_name_locs get_shadow_root
get_shadow_root_locs
by(auto simp add: l_attach_shadow_rootShadow_DOM_def l_attach_shadow_rootShadow_DOM_axioms_def
attach_shadow_root_def instances)
declare l_attach_shadow_rootShadow_DOM_axioms [instances]
subsubsection ‹get\_parent›
global_interpretation l_get_parentCore_DOM_defs get_child_nodes get_child_nodes_locs
defines get_parent = "l_get_parentCore_DOM_defs.a_get_parent get_child_nodes"
and get_parent_locs = "l_get_parentCore_DOM_defs.a_get_parent_locs get_child_nodes_locs"
.
interpretation i_get_parent?: l_get_parentCore_DOM known_ptr type_wf get_child_nodes
get_child_nodes_locs known_ptrs get_parent get_parent_locs
by(simp add: l_get_parentCore_DOM_def l_get_parentCore_DOM_axioms_def get_parent_def
get_parent_locs_def instances)
declare l_get_parentCore_DOM_axioms [instances]
lemma get_parent_is_l_get_parent [instances]: "l_get_parent type_wf known_ptr known_ptrs get_parent
get_parent_locs get_child_nodes get_child_nodes_locs"
apply(simp add: l_get_parent_def l_get_parent_axioms_def instances)
using get_parent_reads get_parent_ok get_parent_ptr_in_heap get_parent_pure
get_parent_parent_in_heap get_parent_child_dual get_parent_reads_pointers
by blast
paragraph ‹set\_disconnected\_nodes›
locale l_set_disconnected_nodes_get_parentShadow_DOM =
l_set_disconnected_nodes_get_child_nodes
+ l_set_disconnected_nodesShadow_DOM
+ l_get_parentCore_DOM
begin
lemma set_disconnected_nodes_get_parent [simp]:
"∀w ∈ set_disconnected_nodes_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_parent_locs. r h h'))"
by(auto simp add: get_parent_locs_def CD.set_disconnected_nodes_locs_def all_args_def)
end
interpretation i_set_disconnected_nodes_get_parent?: l_set_disconnected_nodes_get_parentShadow_DOM
set_disconnected_nodes set_disconnected_nodes_locs get_child_nodes get_child_nodes_locs type_wf
DocumentClass.type_wf known_ptr known_ptrs get_parent get_parent_locs
by (simp add: l_set_disconnected_nodes_get_parentShadow_DOM_def instances)
declare l_set_disconnected_nodes_get_parentCore_DOM_axioms[instances]
lemma set_disconnected_nodes_get_parent_is_l_set_disconnected_nodes_get_parent [instances]:
"l_set_disconnected_nodes_get_parent set_disconnected_nodes_locs get_parent_locs"
by(simp add: l_set_disconnected_nodes_get_parent_def)
subsubsection ‹get\_root\_node›
global_interpretation l_get_root_nodeCore_DOM_defs get_parent get_parent_locs
defines get_root_node = "l_get_root_nodeCore_DOM_defs.a_get_root_node get_parent"
and get_root_node_locs = "l_get_root_nodeCore_DOM_defs.a_get_root_node_locs get_parent_locs"
and get_ancestors = "l_get_root_nodeCore_DOM_defs.a_get_ancestors get_parent"
and get_ancestors_locs = "l_get_root_nodeCore_DOM_defs.a_get_ancestors_locs get_parent_locs"
.
declare a_get_ancestors.simps [code]
interpretation i_get_root_node?: l_get_root_nodeCore_DOM type_wf known_ptr known_ptrs get_parent
get_parent_locs get_child_nodes get_child_nodes_locs get_ancestors get_ancestors_locs
get_root_node get_root_node_locs
by(simp add: l_get_root_nodeCore_DOM_def l_get_root_nodeCore_DOM_axioms_def get_root_node_def
get_root_node_locs_def get_ancestors_def get_ancestors_locs_def instances)
declare l_get_root_nodeCore_DOM_axioms [instances]
lemma get_ancestors_is_l_get_ancestors [instances]: "l_get_ancestors get_ancestors"
apply(auto simp add: l_get_ancestors_def)[1]
using get_ancestors_ptr_in_heap apply fast
using get_ancestors_ptr apply fast
done
lemma get_root_node_is_l_get_root_node [instances]: "l_get_root_node get_root_node get_parent"
by (simp add: l_get_root_node_def Shadow_DOM.i_get_root_node.get_root_node_no_parent)
subsubsection ‹get\_root\_node\_si›
locale l_get_root_node_siShadow_DOM_defs =
l_get_parent_defs get_parent get_parent_locs +
l_get_host_defs get_host get_host_locs
for get_parent :: "(_) node_ptr ==> ((_) heap, exception, (_::linorder) object_ptr option) prog"
and get_parent_locs :: "((_) heap ==> (_) heap ==> bool) set"
and get_host :: "(_) shadow_root_ptr ==> ((_) heap, exception, (_) element_ptr) prog"
and get_host_locs :: "((_) heap ==> (_) heap ==> bool) set"
begin
partial_function (dom_prog) a_get_ancestors_si ::
"(_::linorder) object_ptr ==> (_, (_) object_ptr list) dom_prog"
where
"a_get_ancestors_si ptr = do {
check_in_heap ptr;
ancestors ← (case castobject_ptr2node_ptr ptr of
Some node_ptr ==> do {
parent_ptr_opt ← get_parent node_ptr;
(case parent_ptr_opt of
Some parent_ptr ==> a_get_ancestors_si parent_ptr
| None ==> return [])
}
| None ==> (case cast ptr of
Some shadow_root_ptr ==> do {
host ← get_host shadow_root_ptr;
a_get_ancestors_si (cast host)
} |
None ==> return []));
return (ptr # ancestors)
}"
definition "a_get_ancestors_si_locs = get_parent_locs ∪ get_host_locs"
definition a_get_root_node_si :: "(_) object_ptr ==> (_, (_) object_ptr) dom_prog"
where
"a_get_root_node_si ptr = do {
ancestors ← a_get_ancestors_si ptr;
return (last ancestors)
}"
definition "a_get_root_node_si_locs = a_get_ancestors_si_locs"
end
locale l_get_ancestors_si_defs =
fixes get_ancestors_si :: "(_::linorder) object_ptr ==> (_, (_) object_ptr list) dom_prog"
fixes get_ancestors_si_locs :: "((_) heap ==> (_) heap ==> bool) set"
locale l_get_root_node_si_defs =
fixes get_root_node_si :: "(_) object_ptr ==> (_, (_) object_ptr) dom_prog"
fixes get_root_node_si_locs :: "((_) heap ==> (_) heap ==> bool) set"
locale l_get_root_node_siShadow_DOM =
l_get_parent +
l_get_host +
l_get_root_node_siShadow_DOM_defs +
l_get_ancestors_si_defs +
l_get_root_node_si_defs +
assumes get_ancestors_si_impl: "get_ancestors_si = a_get_ancestors_si"
assumes get_ancestors_si_locs_impl: "get_ancestors_si_locs = a_get_ancestors_si_locs"
assumes get_root_node_si_impl: "get_root_node_si = a_get_root_node_si"
assumes get_root_node_si_locs_impl: "get_root_node_si_locs = a_get_root_node_si_locs"
begin
lemmas get_ancestors_si_def = a_get_ancestors_si.simps[folded get_ancestors_si_impl]
lemmas get_ancestors_si_locs_def = a_get_ancestors_si_locs_def[folded get_ancestors_si_locs_impl]
lemmas get_root_node_si_def =
a_get_root_node_si_def[folded get_root_node_si_impl get_ancestors_si_impl]
lemmas get_root_node_si_locs_def =
a_get_root_node_si_locs_def[folded get_root_node_si_locs_impl get_ancestors_si_locs_impl]
lemma get_ancestors_si_pure [simp]:
"pure (get_ancestors_si ptr) h"
proof -
have "∀ptr h h' x. h ⊨ get_ancestors_si ptr →r x ⟶ h ⊨ get_ancestors_si ptr →h h' ⟶ h = h'"
proof (induct rule: a_get_ancestors_si.fixp_induct[folded get_ancestors_si_impl])
case 1
then show ?case
by(rule admissible_dom_prog)
next
case 2
then show ?case
by simp
next
case (3 f)
then show ?case
using get_parent_pure get_host_pure
apply(auto simp add: pure_returns_heap_eq pure_def
split: option.splits
elim!: bind_returns_heap_E bind_returns_result_E
dest!: pure_returns_heap_eq[rotated, OF check_in_heap_pure])[1]
apply (meson option.simps(3) returns_result_eq)
apply(metis get_parent_pure pure_returns_heap_eq)
apply(metis get_host_pure pure_returns_heap_eq)
done
qed
then show ?thesis
by (meson pure_eq_iff)
qed
lemma get_root_node_si_pure [simp]: "pure (get_root_node_si ptr) h"
by(auto simp add: get_root_node_si_def bind_pure_I)
lemma get_ancestors_si_ptr_in_heap:
assumes "h ⊨ ok (get_ancestors_si ptr)"
shows "ptr |∈| object_ptr_kinds h"
using assms
by(auto simp add: get_ancestors_si_def check_in_heap_ptr_in_heap elim!: bind_is_OK_E
dest: is_OK_returns_result_I)
lemma get_ancestors_si_ptr:
assumes "h ⊨ get_ancestors_si ptr →r ancestors"
shows "ptr ∈ set ancestors"
using assms
by(simp add: get_ancestors_si_def)
(auto elim!: bind_returns_result_E2
split: option.splits
intro!: bind_pure_I)
lemma get_ancestors_si_never_empty:
assumes "h ⊨ get_ancestors_si child →r ancestors"
shows "ancestors ≠ []"
using assms
apply(simp add: get_ancestors_si_def)
by(auto elim!: bind_returns_result_E2 split: option.splits)
lemma get_root_node_si_no_parent:
"h ⊨ get_parent node_ptr →r None ==> h ⊨ get_root_node_si (cast node_ptr) →r cast node_ptr"
apply(auto simp add: check_in_heap_def get_root_node_si_def get_ancestors_si_def
intro!: bind_pure_returns_result_I )[1]
using get_parent_ptr_in_heap by blast
lemma get_root_node_si_root_not_shadow_root:
assumes "h ⊨ get_root_node_si ptr →r root"
shows "¬ is_shadow_root_ptrobject_ptr root"
using assms
proof(auto simp add: get_root_node_si_def elim!: bind_returns_result_E2)
fix y
assume "h ⊨ get_ancestors_si ptr →r y"
and "is_shadow_root_ptrobject_ptr (last y)"
and "root = last y"
then
show False
proof(induct y arbitrary: ptr)
case Nil
then show ?case
using assms(1) get_ancestors_si_never_empty by blast
next
case (Cons a x)
then show ?case
apply(auto simp add: get_ancestors_si_def[of ptr]
elim!: bind_returns_result_E2
split: option.splits if_splits)[1]
using get_ancestors_si_never_empty apply blast
using Cons.prems(2) apply auto[1]
using ‹is_shadow_root_ptrobject_ptr (last y)› ‹root = last y› by auto
qed
qed
end
global_interpretation l_get_root_node_siShadow_DOM_defs get_parent get_parent_locs get_host get_host_locs
defines get_root_node_si = a_get_root_node_si
and get_root_node_si_locs = a_get_root_node_si_locs
and get_ancestors_si = a_get_ancestors_si
and get_ancestors_si_locs = a_get_ancestors_si_locs
.
declare a_get_ancestors_si.simps [code]
interpretation i_get_root_node_si?: l_get_root_node_siShadow_DOM type_wf known_ptr known_ptrs
get_parent get_parent_locs get_child_nodes get_child_nodes_locs get_host get_host_locs
get_ancestors_si get_ancestors_si_locs get_root_node_si get_root_node_si_locs
apply(auto simp add: l_get_root_node_siShadow_DOM_def l_get_root_node_siShadow_DOM_axioms_def
instances)[1]
by(auto simp add: get_root_node_si_def get_root_node_si_locs_def get_ancestors_si_def
get_ancestors_si_locs_def)
declare l_get_root_node_siShadow_DOM_axioms[instances]
lemma get_ancestors_si_is_l_get_ancestors [instances]: "l_get_ancestors get_ancestors_si"
unfolding l_get_ancestors_def
using get_ancestors_si_pure get_ancestors_si_ptr get_ancestors_si_ptr_in_heap
by blast
lemma get_root_node_si_is_l_get_root_node [instances]: "l_get_root_node get_root_node_si get_parent"
apply(simp add: l_get_root_node_def)
using get_root_node_si_no_parent
by fast
paragraph ‹set\_disconnected\_nodes›
locale l_set_disconnected_nodes_get_ancestors_siCore_DOM =
l_set_disconnected_nodes_get_parent
+ l_get_root_node_siShadow_DOM
+ l_set_disconnected_nodesShadow_DOM
+ l_set_disconnected_nodes_get_host
begin
lemma set_disconnected_nodes_get_ancestors_si:
"∀w ∈ set_disconnected_nodes_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_ancestors_si_locs. r h h'))"
by(auto simp add: get_parent_locs_def set_disconnected_nodes_locs_def
set_disconnected_nodes_get_host get_ancestors_si_locs_def all_args_def)
end
locale l_set_disconnected_nodes_get_ancestors_si =
l_set_disconnected_nodes_defs +
l_get_ancestors_si_defs +
assumes set_disconnected_nodes_get_ancestors_si:
"∀w ∈ set_disconnected_nodes_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_ancestors_si_locs. r h h'))"
interpretation i_set_disconnected_nodes_get_ancestors_si?:
l_set_disconnected_nodes_get_ancestors_siCore_DOM set_disconnected_nodes set_disconnected_nodes_locs
get_parent get_parent_locs type_wf known_ptr known_ptrs get_child_nodes get_child_nodes_locs
get_host get_host_locs get_ancestors_si get_ancestors_si_locs get_root_node_si
get_root_node_si_locs DocumentClass.type_wf
by (auto simp add: l_set_disconnected_nodes_get_ancestors_siCore_DOM_def instances)
declare l_set_disconnected_nodes_get_ancestors_siCore_DOM_axioms[instances]
lemma set_disconnected_nodes_get_ancestors_si_is_l_set_disconnected_nodes_get_ancestors_si [instances]:
"l_set_disconnected_nodes_get_ancestors_si set_disconnected_nodes_locs get_ancestors_si_locs"
using instances
apply(simp add: l_set_disconnected_nodes_get_ancestors_si_def)
using set_disconnected_nodes_get_ancestors_si
by fast
subsubsection ‹get\_attribute›
lemma get_attribute_is_l_get_attribute [instances]:
"l_get_attribute type_wf get_attribute get_attribute_locs"
apply(auto simp add: l_get_attribute_def)[1]
using i_get_attribute.get_attribute_reads apply fast
using type_wfDocument i_get_attribute.get_attribute_ok apply blast
using i_get_attribute.get_attribute_ptr_in_heap apply fast
done
subsubsection ‹to\_tree\_order›
global_interpretation l_to_tree_orderCore_DOM_defs get_child_nodes get_child_nodes_locs defines
to_tree_order = "l_to_tree_orderCore_DOM_defs.a_to_tree_order get_child_nodes" .
declare a_to_tree_order.simps [code]
interpretation i_to_tree_order?: l_to_tree_orderCore_DOM ShadowRootClass.known_ptr
ShadowRootClass.type_wf Shadow_DOM.get_child_nodes Shadow_DOM.get_child_nodes_locs to_tree_order
by(auto simp add: l_to_tree_orderCore_DOM_def l_to_tree_orderCore_DOM_axioms_def to_tree_order_def
instances)
declare l_to_tree_orderCore_DOM_axioms [instances]
subsubsection ‹to\_tree\_order\_si›
locale l_to_tree_order_siCore_DOM_defs =
l_get_child_nodes_defs get_child_nodes get_child_nodes_locs +
l_get_shadow_root_defs get_shadow_root get_shadow_root_locs
for get_child_nodes :: "(_::linorder) object_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locs :: "(_) object_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
partial_function (dom_prog) a_to_tree_order_si :: "(_) object_ptr ==> (_, (_) object_ptr list) dom_prog"
where
"a_to_tree_order_si ptr = (do {
children ← get_child_nodes ptr;
shadow_root_part ← (case cast ptr of
Some element_ptr ==> do {
shadow_root_opt ← get_shadow_root element_ptr;
(case shadow_root_opt of
Some shadow_root_ptr ==> return [cast shadow_root_ptr]
| None ==> return [])
} |
None ==> return []);
treeorders ← map_M a_to_tree_order_si ((map (cast) children) @ shadow_root_part);
return (ptr # concat treeorders)
})"
end
locale l_to_tree_order_si_defs =
fixes to_tree_order_si :: "(_) object_ptr ==> (_, (_) object_ptr list) dom_prog"
global_interpretation l_to_tree_order_siCore_DOM_defs get_child_nodes get_child_nodes_locs
get_shadow_root get_shadow_root_locs
defines to_tree_order_si = "a_to_tree_order_si" .
declare a_to_tree_order_si.simps [code]
locale l_to_tree_order_siShadow_DOM =
l_to_tree_order_si_defs +
l_to_tree_order_siCore_DOM_defs +
l_get_child_nodes +
l_get_shadow_root +
assumes to_tree_order_si_impl: "to_tree_order_si = a_to_tree_order_si"
begin
lemmas to_tree_order_si_def = a_to_tree_order_si.simps[folded to_tree_order_si_impl]
lemma to_tree_order_si_pure [simp]: "pure (to_tree_order_si ptr) h"
proof -
have "\<forall>ptr h h' x. h \<turnstile> to_tree_order_si ptr \<rightarrow>\<^sub>r x \<longrightarrow> h \<turnstile> to_tree_order_si ptr \<rightarrow>\<^sub>h h' \<longrightarrow> h = h'"
proof (induct rule: a_to_tree_order_si.fixp_induct[folded to_tree_order_si_impl])
case 1
then show ?case
by (rule admissible_dom_prog)
next
case 2
then show ?case
by simp
next
case (3 f)
then have "\<And>x h. pure (f x) h"
by (metis is_OK_returns_heap_E is_OK_returns_result_E pure_def)
then have "\<And>xs h. pure (map_M f xs) h"
by(rule map_M_pure_I)
then show ?case
by(auto elim!: bind_returns_heap_E2 split: option.splits)
qed
then show ?thesis
unfolding pure_def
by (metis is_OK_returns_heap_E is_OK_returns_result_E)
qed
end
interpretation i_to_tree_order_si?: l_to_tree_order_si\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M to_tree_order_si get_child_nodes
get_child_nodes_locs get_shadow_root get_shadow_root_locs type_wf known_ptr
by(auto simp add: l_to_tree_order_si\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def l_to_tree_order_si\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms_def
to_tree_order_si_def instances)
declare l_to_tree_order_si\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]
subsubsection \<open>first\_in\_tree\_order\<close>
global_interpretation l_first_in_tree_order\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs to_tree_order defines
first_in_tree_order = "l_first_in_tree_order\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.a_first_in_tree_order to_tree_order" .
interpretation i_first_in_tree_order?: l_first_in_tree_order\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M to_tree_order first_in_tree_order
by(auto simp add: l_first_in_tree_order\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def first_in_tree_order_def)
declare l_first_in_tree_order\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]
lemma to_tree_order_is_l_to_tree_order [instances]: "l_to_tree_order to_tree_order"
by(auto simp add: l_to_tree_order_def)
subsubsection \<open>first\_in\_tree\_order\<close>
global_interpretation l_dummy defines
first_in_tree_order_si = "l_first_in_tree_order\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.a_first_in_tree_order to_tree_order_si"
.
subsubsection \<open>get\_element\_by\<close>
global_interpretation l_get_element_by\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs to_tree_order first_in_tree_order get_attribute
get_attribute_locs
defines
get_element_by_id =
"l_get_element_by\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.a_get_element_by_id first_in_tree_order get_attribute" and
get_elements_by_class_name =
"l_get_element_by\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.a_get_elements_by_class_name to_tree_order get_attribute" and
get_elements_by_tag_name =
"l_get_element_by\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.a_get_elements_by_tag_name to_tree_order" .
interpretation i_get_element_by?: l_get_element_by\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M to_tree_order first_in_tree_order
get_attribute get_attribute_locs get_element_by_id get_elements_by_class_name
get_elements_by_tag_name type_wf
by(auto simp add: l_get_element_by\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def l_get_element_by\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms_def
get_element_by_id_def get_elements_by_class_name_def get_elements_by_tag_name_def
instances)
declare l_get_element_by\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms[instances]
lemma get_element_by_is_l_get_element_by [instances]:
"l_get_element_by get_element_by_id get_elements_by_tag_name to_tree_order"
apply(auto simp add: l_get_element_by_def)[1]
using get_element_by_id_result_in_tree_order apply fast
done
subsubsection \<open>get\_element\_by\_si\<close>
global_interpretation l_dummy defines
get_element_by_id_si =
"l_get_element_by\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.a_get_element_by_id first_in_tree_order_si get_attribute" and
get_elements_by_class_name_si =
"l_get_element_by\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.a_get_elements_by_class_name to_tree_order_si get_attribute" and
get_elements_by_tag_name_si =
"l_get_element_by\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.a_get_elements_by_tag_name to_tree_order_si"
.
subsubsection \<open>find\_slot\<close>
locale l_find_slot\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs =
l_get_parent_defs get_parent get_parent_locs +
l_get_shadow_root_defs get_shadow_root get_shadow_root_locs +
l_get_mode_defs get_mode get_mode_locs +
l_get_attribute_defs get_attribute get_attribute_locs +
l_get_tag_name_defs get_tag_name get_tag_name_locs +
l_first_in_tree_order_defs first_in_tree_order
for get_parent :: "(_) node_ptr \<Rightarrow> ((_) heap, exception, (_::linorder) object_ptr option) prog"
and get_parent_locs :: "((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
and get_shadow_root :: "(_) element_ptr \<Rightarrow> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr \<Rightarrow> ((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
and get_mode :: "(_) shadow_root_ptr \<Rightarrow> ((_) heap, exception, shadow_root_mode) prog"
and get_mode_locs :: "(_) shadow_root_ptr \<Rightarrow> ((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
and get_attribute :: "(_) element_ptr \<Rightarrow> char list \<Rightarrow> ((_) heap, exception, char list option) prog"
and get_attribute_locs :: "(_) element_ptr \<Rightarrow> ((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
and get_tag_name :: "(_) element_ptr \<Rightarrow> ((_) heap, exception, char list) prog"
and get_tag_name_locs :: "(_) element_ptr \<Rightarrow> ((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
and first_in_tree_order ::
"(_) object_ptr \<Rightarrow> ((_) object_ptr \<Rightarrow> ((_) heap, exception, (_) element_ptr option) prog) \<Rightarrow>
((_) heap, exception, (_) element_ptr option) prog"
begin
definition a_find_slot :: "bool \<Rightarrow> (_) node_ptr \<Rightarrow> (_, (_) element_ptr option) dom_prog"
where
"a_find_slot open_flag slotable = do {
parent_opt \<leftarrow> get_parent slotable;
(case parent_opt of
Some parent \<Rightarrow>
if is_element_ptr_kind parent
then do {
shadow_root_ptr_opt \<leftarrow> get_shadow_root (the (cast parent));
(case shadow_root_ptr_opt of
Some shadow_root_ptr \<Rightarrow> do {
shadow_root_mode \<leftarrow> get_mode shadow_root_ptr;
if open_flag \<and> shadow_root_mode \<noteq> Open
then return None
else first_in_tree_order (cast shadow_root_ptr) (\<lambda>ptr. if is_element_ptr_kind ptr
then do {
tag \<leftarrow> get_tag_name (the (cast ptr));
name_attr \<leftarrow> get_attribute (the (cast ptr)) ''name'';
slotable_name_attr \<leftarrow> (if is_element_ptr_kind slotable
then get_attribute (the (cast slotable)) ''slot''
else return None);
(if (tag = ''slot'' \<and> (name_attr = slotable_name_attr \<or>
(name_attr = None \<and> slotable_name_attr = Some '''') \<or>
(name_attr = Some '''' \<and> slotable_name_attr = None)))
then return (Some (the (cast ptr)))
else return None)}
else return None)}
| None \<Rightarrow> return None)}
else return None
| _ \<Rightarrow> return None)}"
definition a_assigned_slot :: "(_) node_ptr \<Rightarrow> (_, (_) element_ptr option) dom_prog"
where
"a_assigned_slot = a_find_slot True"
end
global_interpretation l_find_slot\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs get_parent get_parent_locs get_shadow_root
get_shadow_root_locs get_mode get_mode_locs get_attribute get_attribute_locs get_tag_name
get_tag_name_locs first_in_tree_order
defines find_slot = a_find_slot
and assigned_slot = a_assigned_slot
.
locale l_find_slot_defs =
fixes find_slot :: "bool \<Rightarrow> (_) node_ptr \<Rightarrow> (_, (_) element_ptr option) dom_prog"
and assigned_slot :: "(_) node_ptr \<Rightarrow> (_, (_) element_ptr option) dom_prog"
locale l_find_slot\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
l_find_slot\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs +
l_find_slot_defs +
l_get_parent +
l_get_shadow_root +
l_get_mode +
l_get_attribute +
l_get_tag_name +
l_to_tree_order +
l_first_in_tree_order\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
assumes find_slot_impl: "find_slot = a_find_slot"
assumes assigned_slot_impl: "assigned_slot = a_assigned_slot"
begin
lemmas find_slot_def = find_slot_impl[unfolded a_find_slot_def]
lemmas assigned_slot_def = assigned_slot_impl[unfolded a_assigned_slot_def]
lemma find_slot_ptr_in_heap:
assumes "h \<turnstile> find_slot open_flag slotable \<rightarrow>\<^sub>r slot_opt"
shows "slotable |\<in>| node_ptr_kinds h"
using assms
apply(auto simp add: find_slot_def elim!: bind_returns_result_E2)[1]
using get_parent_ptr_in_heap by blast
lemma find_slot_slot_in_heap:
assumes "h \<turnstile> find_slot open_flag slotable \<rightarrow>\<^sub>r Some slot"
shows "slot |\<in>| element_ptr_kinds h"
using assms
apply(auto simp add: find_slot_def first_in_tree_order_def
elim!: bind_returns_result_E2 map_filter_M_pure_E[where y=slot]
split: option.splits if_splits list.splits
intro!: map_filter_M_pure bind_pure_I)[1]
using get_tag_name_ptr_in_heap by blast+
lemma find_slot_pure [simp]: "pure (find_slot open_flag slotable) h"
by(auto simp add: find_slot_def first_in_tree_order_def
intro!: bind_pure_I map_filter_M_pure
split: option.splits list.splits)
end
interpretation i_find_slot?: l_find_slot\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_parent get_parent_locs get_shadow_root
get_shadow_root_locs get_mode get_mode_locs get_attribute get_attribute_locs get_tag_name
get_tag_name_locs first_in_tree_order find_slot assigned_slot type_wf known_ptr known_ptrs
get_child_nodes get_child_nodes_locs to_tree_order
by (auto simp add: find_slot_def assigned_slot_def l_find_slot\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def
l_find_slot\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms_def instances)
declare l_find_slot\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]
locale l_find_slot = l_find_slot_defs +
assumes find_slot_ptr_in_heap:
"h \<turnstile> find_slot open_flag slotable \<rightarrow>\<^sub>r slot_opt \<Longrightarrow> slotable |\<in>| node_ptr_kinds h"
assumes find_slot_slot_in_heap:
"h \<turnstile> find_slot open_flag slotable \<rightarrow>\<^sub>r Some slot \<Longrightarrow> slot |\<in>| element_ptr_kinds h"
assumes find_slot_pure [simp]:
"pure (find_slot open_flag slotable) h"
lemma find_slot_is_l_find_slot [instances]: "l_find_slot find_slot"
apply(auto simp add: l_find_slot_def)[1]
using find_slot_ptr_in_heap apply fast
using find_slot_slot_in_heap apply fast
done
subsubsection \<open>get\_disconnected\_nodes\<close>
locale l_get_disconnected_nodes\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
CD: l_get_disconnected_nodes\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M type_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_disconnected_nodes
get_disconnected_nodes_locs +
l_type_wf type_wf
for type_wf :: "(_) heap \<Rightarrow> bool"
and type_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M :: "(_) heap \<Rightarrow> bool"
and get_disconnected_nodes :: "(_) document_ptr \<Rightarrow> (_, (_) node_ptr list) dom_prog"
and get_disconnected_nodes_locs :: "(_) document_ptr \<Rightarrow> ((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set" +
assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
begin
lemma get_disconnected_nodes_ok:
"type_wf h \<Longrightarrow> document_ptr |\<in>| document_ptr_kinds h \<Longrightarrow>
h \<turnstile> ok (get_disconnected_nodes document_ptr)"
apply(unfold type_wf_impl get_disconnected_nodes_impl[unfolded a_get_disconnected_nodes_def])
using CD.get_disconnected_nodes_ok CD.type_wf_impl ShadowRootClass.type_wf\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t
by blast
end
interpretation i_get_disconnected_nodes?: l_get_disconnected_nodes\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M type_wf
DocumentClass.type_wf get_disconnected_nodes get_disconnected_nodes_locs
by(auto simp add: l_get_disconnected_nodes\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def l_get_disconnected_nodes\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms_def
instances)
declare l_get_disconnected_nodes\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>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(auto simp add: l_get_disconnected_nodes_def)[1]
using i_get_disconnected_nodes.get_disconnected_nodes_reads apply fast
using get_disconnected_nodes_ok apply fast
using i_get_disconnected_nodes.get_disconnected_nodes_ptr_in_heap apply fast
done
paragraph \<open>set\_child\_nodes\<close>
locale l_set_child_nodes_get_disconnected_nodes\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
l_set_child_nodes\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
l_get_disconnected_nodes\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M
begin
lemma set_child_nodes_get_disconnected_nodes:
"\<forall>w \<in> set_child_nodes_locs ptr. (h \<turnstile> w \<rightarrow>\<^sub>h h' \<longrightarrow> (\<forall>r \<in> get_disconnected_nodes_locs ptr'. r h h'))"
by(auto simp add: set_child_nodes_locs_def CD.set_child_nodes_locs_def
CD.get_disconnected_nodes_locs_def all_args_def)
end
interpretation
i_set_child_nodes_get_disconnected_nodes?: l_set_child_nodes_get_disconnected_nodes\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M type_wf
known_ptr DocumentClass.type_wf DocumentClass.known_ptr set_child_nodes set_child_nodes_locs
Core_DOM_Functions.set_child_nodes Core_DOM_Functions.set_child_nodes_locs
get_disconnected_nodes get_disconnected_nodes_locs
apply(auto simp add: l_set_child_nodes_get_disconnected_nodes\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)[ | | |