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