From 633e5c76bbcf5fd2120454dd487fc2a7303f3627 Mon Sep 17 00:00:00 2001 From: Michael Herzberg Date: Mon, 9 Dec 2019 12:16:20 +0000 Subject: [PATCH] Added _thesis lemmas for thesis. --- Core_DOM/Core_DOM_Heap_WF.thy | 546 ++++++++++++++++++++++++++++++++++ 1 file changed, 546 insertions(+) diff --git a/Core_DOM/Core_DOM_Heap_WF.thy b/Core_DOM/Core_DOM_Heap_WF.thy index 11ce2a5..7a7c159 100644 --- a/Core_DOM/Core_DOM_Heap_WF.thy +++ b/Core_DOM/Core_DOM_Heap_WF.thy @@ -4270,6 +4270,13 @@ proof - qed qed +lemma adopt_node_removes_child_thesis: + assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h" + assumes "h \ adopt_node owner_document node_ptr \\<^sub>h h'" +shows "\ptr' children'. + h' \ get_child_nodes ptr' \\<^sub>r children' \ node_ptr \ set children'" + using adopt_node_removes_child assms by blast + lemma adopt_node_preserves_wellformedness: assumes "heap_is_wellformed h" and "h \ adopt_node document_ptr child \\<^sub>h h'" @@ -4982,6 +4989,245 @@ locale l_insert_before_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub 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_preserves_acyclitity_thesis: + assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h" + assumes "h \ insert_before ptr node child \\<^sub>h h'" +shows "acyclic (parent_child_rel 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 "known_ptr ptr" + by (meson get_owner_document_ptr_in_heap is_OK_returns_result_I assms + l_known_ptrs.known_ptrs_known_ptr l_known_ptrs_axioms owner_document) + + have "type_wf h2" + using writes_small_big[where P="\h h'. type_wf h \ type_wf h'", OF adopt_node_writes h2] + using assms adopt_node_types_preserved + by(auto simp add: a_remove_child_locs_def reflp_def transp_def) + 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 insert_node_writes h'] + using set_child_nodes_types_preserved + by(auto simp add: reflp_def transp_def) + + 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 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 by simp + + 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 "known_ptrs h'" + using object_ptr_kinds_M_eq3_h' known_ptrs_preserved \known_ptrs h3\ by blast + + have disconnected_nodes_eq_h2: + "\doc_ptr disc_nodes. owner_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 (auto simp add: set_disconnected_nodes_get_disconnected_nodes_different_pointers) + then have disconnected_nodes_eq2_h2: + "\doc_ptr. doc_ptr \ owner_document + \ |h2 \ get_disconnected_nodes doc_ptr|\<^sub>r = |h3 \ get_disconnected_nodes doc_ptr|\<^sub>r" + using select_result_eq by force + have disconnected_nodes_h3: + "h3 \ get_disconnected_nodes owner_document \\<^sub>r remove1 node disconnected_nodes_h2" + using h3 set_disconnected_nodes_get_disconnected_nodes + by blast + + have disconnected_nodes_eq_h3: + "\doc_ptr disc_nodes. 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 insert_node_writes h' + apply(rule reads_writes_preserved) + using set_child_nodes_get_disconnected_nodes by fast + then have disconnected_nodes_eq2_h3: + "\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 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 (auto 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 children_eq_h3: + "\ptr' children. ptr \ ptr' + \ h3 \ get_child_nodes ptr' \\<^sub>r children = h' \ get_child_nodes ptr' \\<^sub>r children" + using get_child_nodes_reads insert_node_writes h' + apply(rule reads_writes_preserved) + by (auto simp add: set_child_nodes_get_child_nodes_different_pointers) + then have children_eq2_h3: + "\ptr'. ptr \ ptr' \ |h3 \ get_child_nodes ptr'|\<^sub>r = |h' \ get_child_nodes ptr'|\<^sub>r" + using select_result_eq by force + obtain children_h3 where children_h3: "h3 \ get_child_nodes ptr \\<^sub>r children_h3" + using h' a_insert_node_def by auto + have children_h': "h' \ get_child_nodes ptr \\<^sub>r insert_before_list node reference_child children_h3" + using h' \type_wf h3\ \known_ptr ptr\ + by(auto simp add: a_insert_node_def elim!: bind_returns_heap_E2 + dest!: set_child_nodes_get_child_nodes returns_result_eq[OF children_h3]) + + have ptr_in_heap: "ptr |\| object_ptr_kinds h3" + using children_h3 get_child_nodes_ptr_in_heap by blast + have node_in_heap: "node |\| node_ptr_kinds h" + using h2 adopt_node_child_in_heap by fast + have child_not_in_any_children: + "\p children. h2 \ get_child_nodes p \\<^sub>r children \ node \ set children" + using assms h2 adopt_node_removes_child by auto + have "node \ set disconnected_nodes_h2" + using disconnected_nodes_h2 h2 adopt_node_node_in_disconnected_nodes assms(1) + \type_wf h\ \known_ptrs h\ by blast + have node_not_in_disconnected_nodes: + "\d. d |\| document_ptr_kinds h3 \ node \ set |h3 \ get_disconnected_nodes d|\<^sub>r" + proof - + fix d + assume "d |\| document_ptr_kinds h3" + show "node \ set |h3 \ get_disconnected_nodes d|\<^sub>r" + proof (cases "d = owner_document") + case True + then show ?thesis + using disconnected_nodes_h2 wellformed_h2 h3 remove_from_disconnected_nodes_removes + wellformed_h2 \d |\| document_ptr_kinds h3\ disconnected_nodes_h3 + by fastforce + next + case False + then have + "set |h2 \ get_disconnected_nodes d|\<^sub>r \ set |h2 \ get_disconnected_nodes owner_document|\<^sub>r = {}" + using distinct_concat_map_E(1) wellformed_h2 + by (metis (no_types, lifting) \d |\| document_ptr_kinds h3\ \type_wf h2\ + disconnected_nodes_h2 document_ptr_kinds_M_def document_ptr_kinds_eq2_h2 + 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 + select_result_I2) + then show ?thesis + using disconnected_nodes_eq2_h2[OF False] \node \ set disconnected_nodes_h2\ + disconnected_nodes_h2 by fastforce + qed + qed + + have "cast node \ ptr" + using ancestors node_not_in_ancestors get_ancestors_ptr + by fast + + obtain ancestors_h2 where ancestors_h2: "h2 \ get_ancestors ptr \\<^sub>r ancestors_h2" + using get_ancestors_ok object_ptr_kinds_M_eq2_h2 \known_ptrs h2\ \type_wf h2\ + by (metis is_OK_returns_result_E object_ptr_kinds_M_eq3_h2 ptr_in_heap wellformed_h2) + have ancestors_h3: "h3 \ get_ancestors ptr \\<^sub>r ancestors_h2" + using get_ancestors_reads set_disconnected_nodes_writes h3 + apply(rule reads_writes_separate_forwards) + using \heap_is_wellformed h2\ ancestors_h2 + by (auto simp add: set_disconnected_nodes_get_ancestors) + have node_not_in_ancestors_h2: "cast node \ set ancestors_h2" + apply(rule get_ancestors_remains_not_in_ancestors[OF assms(1) wellformed_h2 ancestors ancestors_h2]) + using adopt_node_children_subset using h2 \known_ptrs h\ \ type_wf h\ apply(blast) + using node_not_in_ancestors apply(blast) + using object_ptr_kinds_M_eq3_h apply(blast) + using \known_ptrs h\ apply(blast) + using \type_wf h\ apply(blast) + using \type_wf h2\ by blast + + have "acyclic (parent_child_rel h2)" + using wellformed_h2 by (simp add: heap_is_wellformed_def acyclic_heap_def) + then have "acyclic (parent_child_rel h3)" + by(auto simp add: parent_child_rel_def object_ptr_kinds_M_eq3_h2 children_eq2_h2) + moreover + + have "cast node \ {x. (x, ptr) \ (parent_child_rel h2)\<^sup>*}" + using adopt_node_removes_child + using ancestors node_not_in_ancestors + using \known_ptrs h2\ \type_wf h2\ ancestors_h2 local.get_ancestors_parent_child_rel node_not_in_ancestors_h2 wellformed_h2 + by blast + then have "cast node \ {x. (x, ptr) \ (parent_child_rel h3)\<^sup>*}" + by(auto simp add: parent_child_rel_def object_ptr_kinds_M_eq3_h2 children_eq2_h2) + moreover have "parent_child_rel h' + = insert (ptr, cast node) ((parent_child_rel h3))" + using children_h3 children_h' ptr_in_heap + apply(auto simp add: parent_child_rel_def object_ptr_kinds_M_eq3_h' children_eq2_h3 + insert_before_list_node_in_set)[1] + apply (metis (no_types, lifting) children_eq2_h3 insert_before_list_in_set select_result_I2) + by (metis (no_types, lifting) children_eq2_h3 imageI insert_before_list_in_set select_result_I2) + ultimately show "acyclic (parent_child_rel h')" + by (auto simp add: heap_is_wellformed_def) +qed + lemma insert_before_heap_is_wellformed_preserved: assumes wellformed: "heap_is_wellformed h" and insert_before: "h \ insert_before ptr node child \\<^sub>h h'" @@ -5446,6 +5692,306 @@ proof - ultimately show "heap_is_wellformed h'" by (simp add: heap_is_wellformed_def) qed + +lemma adopt_node_children_remain_distinct_thesis: + assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h" + assumes "h \ adopt_node owner_document node_ptr \\<^sub>h h'" +shows "\ptr' children'. + h' \ get_child_nodes ptr' \\<^sub>r children' \ distinct children'" + using assms(1) assms(2) assms(3) assms(4) local.adopt_node_preserves_wellformedness local.heap_is_wellformed_children_distinct + by blast + + +lemma insert_node_children_remain_distinct_thesis: + assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h" + assumes "h \ a_insert_node ptr new_child reference_child_opt \\<^sub>h h'" + assumes "h \ get_child_nodes ptr \\<^sub>r children" + assumes "new_child \ set children" +shows "\children'. + h' \ get_child_nodes ptr \\<^sub>r children' \ distinct children'" +proof - + fix children' + assume a1: "h' \ get_child_nodes ptr \\<^sub>r children'" + have "h' \ get_child_nodes ptr \\<^sub>r (insert_before_list new_child reference_child_opt children)" + using assms(4) assms(5) apply(auto simp add: a_insert_node_def elim!: bind_returns_heap_E)[1] + using returns_result_eq set_child_nodes_get_child_nodes assms(2) assms(3) + by (metis is_OK_returns_result_I local.get_child_nodes_ptr_in_heap local.get_child_nodes_pure local.known_ptrs_known_ptr pure_returns_heap_eq) + moreover have "a_distinct_lists h" + using assms local.heap_is_wellformed_def by blast + then have "\children. h \ get_child_nodes ptr \\<^sub>r children + \ distinct children" + using assms local.heap_is_wellformed_children_distinct by blast + ultimately show "h' \ get_child_nodes ptr \\<^sub>r children' \ distinct children'" + using assms(5) assms(6) insert_before_list_distinct returns_result_eq by fastforce +qed + +lemma insert_before_children_remain_distinct_thesis: + assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h" + assumes "h \ insert_before ptr new_child child_opt \\<^sub>h h'" +shows "\ptr' children'. + h' \ get_child_nodes ptr' \\<^sub>r children' \ distinct children'" +proof - + obtain reference_child owner_document h2 h3 disconnected_nodes_h2 where + reference_child: + "h \ (if Some new_child = child_opt then a_next_sibling new_child else return child_opt) \\<^sub>r reference_child" and + owner_document: "h \ get_owner_document ptr \\<^sub>r owner_document" and + h2: "h \ adopt_node owner_document new_child \\<^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 new_child disconnected_nodes_h2) \\<^sub>h h3" and + h': "h3 \ a_insert_node ptr new_child 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 "\ptr children. h2 \ get_child_nodes ptr \\<^sub>r children + \ distinct children" + using adopt_node_children_remain_distinct_thesis + using assms(1) assms(2) assms(3) h2 + by blast + moreover have "\ptr children. h2 \ get_child_nodes ptr \\<^sub>r children + \ new_child \ set children" + using adopt_node_removes_child + using assms(1) assms(2) assms(3) h2 + by blast + moreover have "\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 (auto simp add: set_disconnected_nodes_get_child_nodes) + ultimately show "\ptr children. h' \ get_child_nodes ptr \\<^sub>r children + \ distinct children" + using insert_node_children_remain_distinct + by (meson assms(1) assms(2) assms(3) assms(4) insert_before_heap_is_wellformed_preserved(1) local.heap_is_wellformed_children_distinct) +qed + + +lemma insert_before_removes_child_thesis: + assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h" + assumes "h \ insert_before ptr node child \\<^sub>h h'" + assumes "ptr \ ptr'" + shows "\children'. h' \ get_child_nodes ptr' \\<^sub>r children' \ node \ set children'" +proof - + fix children' + assume a1: "h' \ get_child_nodes ptr' \\<^sub>r children'" + 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 "known_ptr ptr" + by (meson get_owner_document_ptr_in_heap is_OK_returns_result_I assms(2) + l_known_ptrs.known_ptrs_known_ptr l_known_ptrs_axioms owner_document) + + have "type_wf h2" + using writes_small_big[where P="\h h'. type_wf h \ type_wf h'", OF adopt_node_writes h2] + using assms(3) adopt_node_types_preserved + by(auto simp add: a_remove_child_locs_def reflp_def transp_def) + 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 insert_node_writes h'] + using set_child_nodes_types_preserved + by(auto simp add: reflp_def transp_def) + + 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 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 by simp + + 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 "known_ptrs h'" + using object_ptr_kinds_M_eq3_h' known_ptrs_preserved \known_ptrs h3\ by blast + + have disconnected_nodes_eq_h2: + "\doc_ptr disc_nodes. owner_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 (auto simp add: set_disconnected_nodes_get_disconnected_nodes_different_pointers) + then have disconnected_nodes_eq2_h2: + "\doc_ptr. doc_ptr \ owner_document + \ |h2 \ get_disconnected_nodes doc_ptr|\<^sub>r = |h3 \ get_disconnected_nodes doc_ptr|\<^sub>r" + using select_result_eq by force + have disconnected_nodes_h3: + "h3 \ get_disconnected_nodes owner_document \\<^sub>r remove1 node disconnected_nodes_h2" + using h3 set_disconnected_nodes_get_disconnected_nodes + by blast + + have disconnected_nodes_eq_h3: + "\doc_ptr disc_nodes. 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 insert_node_writes h' + apply(rule reads_writes_preserved) + using set_child_nodes_get_disconnected_nodes by fast + then have disconnected_nodes_eq2_h3: + "\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 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 (auto 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 children_eq_h3: + "\ptr' children. ptr \ ptr' + \ h3 \ get_child_nodes ptr' \\<^sub>r children = h' \ get_child_nodes ptr' \\<^sub>r children" + using get_child_nodes_reads insert_node_writes h' + apply(rule reads_writes_preserved) + by (auto simp add: set_child_nodes_get_child_nodes_different_pointers) + then have children_eq2_h3: + "\ptr'. ptr \ ptr' \ |h3 \ get_child_nodes ptr'|\<^sub>r = |h' \ get_child_nodes ptr'|\<^sub>r" + using select_result_eq by force + obtain children_h3 where children_h3: "h3 \ get_child_nodes ptr \\<^sub>r children_h3" + using h' a_insert_node_def by auto + have children_h': "h' \ get_child_nodes ptr \\<^sub>r insert_before_list node reference_child children_h3" + using h' \type_wf h3\ \known_ptr ptr\ + by(auto simp add: a_insert_node_def elim!: bind_returns_heap_E2 + dest!: set_child_nodes_get_child_nodes returns_result_eq[OF children_h3]) + + have ptr_in_heap: "ptr |\| object_ptr_kinds h3" + using children_h3 get_child_nodes_ptr_in_heap by blast + have node_in_heap: "node |\| node_ptr_kinds h" + using h2 adopt_node_child_in_heap by fast + have child_not_in_any_children: + "\p children. h2 \ get_child_nodes p \\<^sub>r children \ node \ set children" + using assms(1) assms(2) assms(3) h2 local.adopt_node_removes_child by blast + show "node \ set children'" + using a1 assms(5) child_not_in_any_children children_eq_h2 children_eq_h3 by blast +qed + +lemma ensure_pre_insertion_validity_ok: + assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h" + assumes "ptr |\| object_ptr_kinds h" + assumes "\is_character_data_ptr_kind parent" + assumes "cast node \ set |h \ get_ancestors parent|\<^sub>r" + assumes "h \ get_parent ref \\<^sub>r Some parent" + assumes "is_document_ptr parent \ h \ get_child_nodes parent \\<^sub>r []" + assumes "is_document_ptr parent \ \is_character_data_ptr_kind node" + shows "h \ ok (a_ensure_pre_insertion_validity node parent (Some ref))" +proof - + have "h \ (if is_character_data_ptr_kind parent + then error HierarchyRequestError else return ()) \\<^sub>r ()" + using assms + by (simp add: assms(4)) + moreover have "h \ do { + ancestors \ get_ancestors parent; + (if cast node \ set ancestors then error HierarchyRequestError else return ()) + } \\<^sub>r ()" + using assms(6) + apply(auto intro!: bind_pure_returns_result_I) + using assms(1) assms(2) assms(3) assms(7) local.get_ancestors_ok local.get_parent_parent_in_heap by auto + + moreover have "h \ do { + (case Some ref of + Some child \ do { + child_parent \ get_parent child; + (if child_parent \ Some parent then error NotFoundError else return ())} + | None \ return ()) + } \\<^sub>r ()" + using assms(7) + by(auto split: option.splits) + moreover have "h \ do { + children \ get_child_nodes parent; + (if children \ [] \ is_document_ptr parent + then error HierarchyRequestError else return ()) + } \\<^sub>r ()" + using assms(8) + by (smt assms(5) assms(7) bind_pure_returns_result_I2 calculation(1) is_OK_returns_result_I local.get_child_nodes_pure local.get_parent_child_dual returns_result_eq) + + moreover have "h \ do { + (if is_character_data_ptr node \ is_document_ptr parent + then error HierarchyRequestError else return ()) + } \\<^sub>r ()" + using assms + using is_character_data_ptr_kind_none by force + ultimately show ?thesis + unfolding a_ensure_pre_insertion_validity_def + apply(intro bind_is_OK_pure_I) + apply(auto) + using assms(1) assms(2) assms(3) assms(7) local.get_ancestors_ok local.get_parent_parent_in_heap apply blast + + using assms(6) apply auto[1] + apply (smt assms(7) bind_returns_heap_E2 is_OK_returns_heap_E local.get_parent_pure pure_def pure_returns_heap_eq return_pure returns_result_eq) + apply (meson assms(7) is_OK_returns_result_I local.get_parent_child_dual) + by (simp add: assms(8) returns_result_eq) +qed + end locale l_insert_before_wf2 = l_type_wf + l_known_ptrs + l_insert_before_defs