From b7fa25e301022bbd41c6072b669cc94beac51dd6 Mon Sep 17 00:00:00 2001 From: Michael Herzberg Date: Wed, 6 Feb 2019 14:05:15 +0000 Subject: [PATCH] Added more lemmas. --- Core_DOM/Core_DOM_Functions.thy | 80 +++++++++- Core_DOM/Core_DOM_Heap_WF.thy | 262 ++++++++++++++++++++++++++++---- 2 files changed, 304 insertions(+), 38 deletions(-) diff --git a/Core_DOM/Core_DOM_Functions.thy b/Core_DOM/Core_DOM_Functions.thy index 851d76c..dc1e185 100644 --- a/Core_DOM/Core_DOM_Functions.thy +++ b/Core_DOM/Core_DOM_Functions.thy @@ -3167,19 +3167,51 @@ global_interpretation l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\< locale l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M = l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs + + l_get_disconnected_nodes + + l_set_tag_type + l_create_element_defs + assumes create_element_impl: "create_element = a_create_element" begin lemmas create_element_def = a_create_element_def[folded create_element_impl] + +lemma create_element_document_in_heap: + assumes "h \ ok (create_element document_ptr tag)" + shows "document_ptr |\| document_ptr_kinds h" +proof - + obtain h' where "h \ create_element document_ptr tag \\<^sub>h h'" + using assms(1) + by auto + then + 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_type 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'" + 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 + + moreover 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_type_writes h3]) + using set_tag_type_pointers_preserved + by (auto simp add: reflp_def transp_def) + moreover have "document_ptr |\| document_ptr_kinds h3" + by (meson disc_nodes_h3 is_OK_returns_result_I local.get_disconnected_nodes_ptr_in_heap) + + ultimately show ?thesis + by (auto simp add: document_ptr_kinds_def) +qed end locale l_create_element = l_create_element_defs interpretation - i_create_element?: l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_disconnected_nodes get_disconnected_nodes_locs - set_disconnected_nodes set_disconnected_nodes_locs set_tag_type - set_tag_type_locs create_element - by unfold_locales (simp add: create_element_def) + i_create_element?: l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs set_tag_type set_tag_type_locs type_wf create_element + by(auto simp add: l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms_def create_element_def instances) declare l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms[instances] @@ -3218,19 +3250,51 @@ global_interpretation l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^ locale l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M = l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs + + l_get_disconnected_nodes + + l_set_val + l_create_character_data_defs + assumes create_character_data_impl: "create_character_data = a_create_character_data" begin lemmas create_character_data_def = a_create_character_data_def[folded create_character_data_impl] + +lemma create_character_data_document_in_heap: + assumes "h \ ok (create_character_data document_ptr text)" + shows "document_ptr |\| document_ptr_kinds h" +proof - + obtain h' where "h \ create_character_data document_ptr text \\<^sub>h h'" + using assms(1) + by auto + then + 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'" + by(auto simp add: create_character_data_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_character_data_ptr|}" + using new_character_data_new_ptr h2 new_character_data_ptr by blast + + moreover 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) + moreover have "document_ptr |\| document_ptr_kinds h3" + by (meson disc_nodes_h3 is_OK_returns_result_I local.get_disconnected_nodes_ptr_in_heap) + + ultimately show ?thesis + by (auto simp add: document_ptr_kinds_def) +qed end locale l_create_character_data = l_create_character_data_defs interpretation - i_create_character_data?: l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M set_val set_val_locs get_disconnected_nodes - get_disconnected_nodes_locs set_disconnected_nodes - set_disconnected_nodes_locs create_character_data - by unfold_locales (simp add: create_character_data_def) + i_create_character_data?: l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M set_val set_val_locs get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs type_wf create_character_data + by(auto simp add: l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms_def create_character_data_def instances) declare l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances] diff --git a/Core_DOM/Core_DOM_Heap_WF.thy b/Core_DOM/Core_DOM_Heap_WF.thy index 6937ad9..4de73f1 100644 --- a/Core_DOM/Core_DOM_Heap_WF.thy +++ b/Core_DOM/Core_DOM_Heap_WF.thy @@ -517,8 +517,8 @@ proof - proof (induct rule: wf_induct_rule) case (less parent) then show ?case - using assms child_parent_dual parent_child_rel_parent - by (meson converse_iff parent_child_rel_child) + using assms parent_child_rel_child + by (meson converse_iff) qed qed @@ -1764,9 +1764,9 @@ locale l_get_root_node_wf = l_heap_is_wellformed_defs + l_get_root_node_defs + l assumes get_root_node_same_no_parent: "heap_is_wellformed h \ type_wf h \ known_ptrs h \ h \ get_root_node ptr \\<^sub>r cast child \ h \ get_parent child \\<^sub>r None" - assumes get_root_node_not_node_same: + (* assumes get_root_node_not_node_same: "ptr |\| object_ptr_kinds h \ \is_node_ptr_kind ptr - \ h \ get_root_node ptr \\<^sub>r ptr" + \ h \ get_root_node ptr \\<^sub>r ptr" *) assumes get_root_node_parent_same: "h \ get_parent child \\<^sub>r Some ptr \ h \ get_root_node (cast child) \\<^sub>r root \ h \ get_root_node ptr \\<^sub>r root" @@ -1805,7 +1805,7 @@ lemma get_root_node_wf_is_l_get_root_node_wf [instances]: using get_root_node_root_in_heap apply blast using get_ancestors_same_root_node apply(blast, blast) using get_root_node_same_no_parent apply blast - using get_root_node_not_node_same apply blast + (* using get_root_node_not_node_same apply blast *) using get_root_node_parent_same apply (blast, blast) done @@ -2374,13 +2374,8 @@ lemma to_tree_order_wf_is_l_to_tree_order_wf [instances]: subsubsection \get\_root\_node\ locale l_to_tree_order_wf_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M = - l_get_ancestors - + l_get_ancestors_wf - + l_get_root_node - + l_get_root_node_wf + l_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M + l_to_tree_order_wf - + l_get_parent - + l_get_parent_wf begin lemma to_tree_order_get_root_node: assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h" @@ -2467,9 +2462,7 @@ qed end interpretation i_to_tree_order_wf_get_root_node_wf?: l_to_tree_order_wf_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M - get_ancestors get_ancestors_locs heap_is_wellformed parent_child_rel known_ptr - known_ptrs type_wf get_child_nodes get_child_nodes_locs get_parent get_parent_locs - get_root_node get_root_node_locs to_tree_order + known_ptr type_wf known_ptrs heap_is_wellformed parent_child_rel get_child_nodes get_child_nodes_locs get_disconnected_nodes get_disconnected_nodes_locs get_parent get_parent_locs get_ancestors get_ancestors_locs get_root_node get_root_node_locs to_tree_order using instances by(simp add: l_to_tree_order_wf_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def) @@ -2506,6 +2499,7 @@ locale l_get_owner_document_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\< + l_get_ancestors_wf + l_get_parent + l_get_parent_wf + + l_get_root_node_wf + l_get_owner_document\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M begin @@ -2643,6 +2637,154 @@ proof - returns_result_select_result select_result_I2 by (metis (no_types, hide_lams) ) qed + +lemma get_owner_document_owner_document_in_heap: + assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h" + assumes "h \ get_owner_document ptr \\<^sub>r owner_document" + shows "owner_document |\| document_ptr_kinds h" + using assms + apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def) + apply(split invoke_split_asm)+ +proof - + assume "h \ invoke [] ptr () \\<^sub>r owner_document" + then show "owner_document |\| document_ptr_kinds h" + by (meson invoke_empty is_OK_returns_result_I) +next + assume "h \ Heap_Error_Monad.bind (check_in_heap ptr) + (\_. (local.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 \ the \ cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r) ptr ()) + \\<^sub>r owner_document" + then show "owner_document |\| document_ptr_kinds h" + by(auto simp add: 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 elim!: bind_returns_result_E2 split: if_splits) +next + assume 0: "heap_is_wellformed h" + and 1: "type_wf h" + and 2: "known_ptrs h" + and 3: "\ is_element_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr" + and 4: "is_character_data_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr" + and 5: "h \ Heap_Error_Monad.bind (check_in_heap ptr) (\_. (local.a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r \ the \ cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^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) ptr ()) \\<^sub>r owner_document" + then obtain root where + root: "h \ get_root_node ptr \\<^sub>r root" + by(auto simp add: a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def elim!: bind_returns_result_E2 split: option.splits) + + then show ?thesis + proof (cases "is_document_ptr root") + case True + then show ?thesis + using 4 5 root + apply(auto simp add: a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def elim!: bind_returns_result_E2 intro!: filter_M_pure_I bind_pure_I split: option.splits)[1] + apply(drule(1) returns_result_eq) apply(auto)[1] + using "0" "1" "2" document_ptr_kinds_commutes local.get_root_node_root_in_heap by blast + next + case False + have "known_ptr root" + using "0" "1" "2" local.get_root_node_root_in_heap local.known_ptrs_known_ptr root by blast + have "root |\| object_ptr_kinds h" + using root + using "0" "1" "2" local.get_root_node_root_in_heap + by blast + then have "is_node_ptr_kind root" + using False \known_ptr root\ + apply(simp add: known_ptr_impl known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs) + using is_node_ptr_kind_none by force + then + have "(\document_ptr \ fset (document_ptr_kinds h). root \ cast ` set |h \ get_disconnected_nodes document_ptr|\<^sub>r)" + by (metis (no_types, lifting) "0" "1" "2" \root |\| object_ptr_kinds h\ local.child_parent_dual local.get_child_nodes_ok local.get_root_node_same_no_parent local.heap_is_wellformed_children_disc_nodes local.known_ptrs_known_ptr node_ptr_casts_commute3 node_ptr_inclusion node_ptr_kinds_commutes notin_fset option.distinct(1) returns_result_eq returns_result_select_result root) + then obtain some_owner_document where + "some_owner_document |\| document_ptr_kinds h" and + "root \ cast ` set |h \ get_disconnected_nodes some_owner_document|\<^sub>r" + by auto + then + obtain candidates where + candidates: "h \ filter_M + (\document_ptr. + Heap_Error_Monad.bind (get_disconnected_nodes document_ptr) + (\disconnected_nodes. return (root \ 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 ` set disconnected_nodes))) + (sorted_list_of_set (fset (document_ptr_kinds h))) + \\<^sub>r candidates" + by (metis (no_types, lifting) "1" bind_is_OK_I2 bind_pure_I filter_M_is_OK_I finite_fset is_OK_returns_result_E local.get_disconnected_nodes_ok local.get_disconnected_nodes_pure notin_fset return_ok return_pure sorted_list_of_set(1)) + then have "some_owner_document \ set candidates" + apply(rule filter_M_in_result_if_ok) + using \some_owner_document |\| document_ptr_kinds h\ \root \ cast ` set |h \ get_disconnected_nodes some_owner_document|\<^sub>r\ + apply(auto intro!: bind_pure_I bind_pure_returns_result_I) + by (simp add: "1" local.get_disconnected_nodes_ok) + + then have "candidates \ []" + by auto + then have "owner_document \ set candidates" + using 5 root 4 + apply(auto simp add: a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def elim!: bind_returns_result_E2 intro!: filter_M_pure_I bind_pure_I split: option.splits)[1] + apply (metis candidates list.set_sel(1) returns_result_eq) + by (metis \is_node_ptr_kind root\ node_ptr_no_document_ptr_cast returns_result_eq) + + then show ?thesis + using candidates + by (meson bind_pure_I bind_returns_result_E2 filter_M_holds_for_result is_OK_returns_result_I local.get_disconnected_nodes_ptr_in_heap local.get_disconnected_nodes_pure return_pure) + qed +next + assume 0: "heap_is_wellformed h" + and 1: "type_wf h" + and 2: "known_ptrs h" + and 3: "is_element_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr" + and 4: "h \ Heap_Error_Monad.bind (check_in_heap ptr) (\_. (local.a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r \ the \ cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^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) ptr ()) \\<^sub>r owner_document" + then obtain root where + root: "h \ get_root_node ptr \\<^sub>r root" + by(auto simp add: a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def elim!: bind_returns_result_E2 split: option.splits) + + then show ?thesis + proof (cases "is_document_ptr root") + case True + then show ?thesis + using 3 4 root + apply(auto simp add: a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def elim!: bind_returns_result_E2 intro!: filter_M_pure_I bind_pure_I split: option.splits)[1] + apply(drule(1) returns_result_eq) apply(auto)[1] + using "0" "1" "2" document_ptr_kinds_commutes local.get_root_node_root_in_heap by blast + next + case False + have "known_ptr root" + using "0" "1" "2" local.get_root_node_root_in_heap local.known_ptrs_known_ptr root by blast + have "root |\| object_ptr_kinds h" + using root + using "0" "1" "2" local.get_root_node_root_in_heap + by blast + then have "is_node_ptr_kind root" + using False \known_ptr root\ + apply(simp add: known_ptr_impl known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs) + using is_node_ptr_kind_none by force + then + have "(\document_ptr \ fset (document_ptr_kinds h). root \ cast ` set |h \ get_disconnected_nodes document_ptr|\<^sub>r)" + by (metis (no_types, lifting) "0" "1" "2" \root |\| object_ptr_kinds h\ local.child_parent_dual local.get_child_nodes_ok local.get_root_node_same_no_parent local.heap_is_wellformed_children_disc_nodes local.known_ptrs_known_ptr node_ptr_casts_commute3 node_ptr_inclusion node_ptr_kinds_commutes notin_fset option.distinct(1) returns_result_eq returns_result_select_result root) + then obtain some_owner_document where + "some_owner_document |\| document_ptr_kinds h" and + "root \ cast ` set |h \ get_disconnected_nodes some_owner_document|\<^sub>r" + by auto + then + obtain candidates where + candidates: "h \ filter_M + (\document_ptr. + Heap_Error_Monad.bind (get_disconnected_nodes document_ptr) + (\disconnected_nodes. return (root \ 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 ` set disconnected_nodes))) + (sorted_list_of_set (fset (document_ptr_kinds h))) + \\<^sub>r candidates" + by (metis (no_types, lifting) "1" bind_is_OK_I2 bind_pure_I filter_M_is_OK_I finite_fset is_OK_returns_result_E local.get_disconnected_nodes_ok local.get_disconnected_nodes_pure notin_fset return_ok return_pure sorted_list_of_set(1)) + then have "some_owner_document \ set candidates" + apply(rule filter_M_in_result_if_ok) + using \some_owner_document |\| document_ptr_kinds h\ \root \ cast ` set |h \ get_disconnected_nodes some_owner_document|\<^sub>r\ + apply(auto intro!: bind_pure_I bind_pure_returns_result_I) + by (simp add: "1" local.get_disconnected_nodes_ok) + + then have "candidates \ []" + by auto + then have "owner_document \ set candidates" + using 4 root 3 + apply(auto simp add: a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def elim!: bind_returns_result_E2 intro!: filter_M_pure_I bind_pure_I split: option.splits)[1] + apply (metis candidates list.set_sel(1) returns_result_eq) + by (metis \is_node_ptr_kind root\ node_ptr_no_document_ptr_cast returns_result_eq) + + then show ?thesis + using candidates + by (meson bind_pure_I bind_returns_result_E2 filter_M_holds_for_result is_OK_returns_result_I local.get_disconnected_nodes_ptr_in_heap local.get_disconnected_nodes_pure return_pure) + qed +qed end locale l_get_owner_document_wf = l_heap_is_wellformed_defs + l_type_wf + l_known_ptrs @@ -2663,32 +2805,28 @@ locale l_get_owner_document_wf = l_heap_is_wellformed_defs + l_type_wf + l_known known_ptrs h \ type_wf h\ node_ptr \ set disc_nodes" + assumes get_owner_document_owner_document_in_heap: + "heap_is_wellformed h \ type_wf h \ known_ptrs h \ h \ get_owner_document ptr \\<^sub>r owner_document \ owner_document |\| document_ptr_kinds h" + interpretation i_get_owner_document_wf?: l_get_owner_document_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M known_ptr known_ptrs type_wf heap_is_wellformed parent_child_rel get_child_nodes get_child_nodes_locs get_disconnected_nodes get_disconnected_nodes_locs get_root_node get_root_node_locs get_parent get_parent_locs get_ancestors get_ancestors_locs get_owner_document - using known_ptrs_is_l_known_ptrs - using heap_is_wellformed_is_l_heap_is_wellformed - using get_root_node_is_l_get_root_node - using get_ancestors_is_l_get_ancestors - using get_ancestors_wf_is_l_get_ancestors_wf - using get_parent_is_l_get_parent - using get_ancestors_wf_is_l_get_ancestors_wf - using get_parent_wf_is_l_get_parent_wf - using l_get_owner_document\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms - by(simp add: l_get_owner_document_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def) - + by(simp add: l_get_owner_document_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances) +declare l_get_owner_document_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances] lemma get_owner_document_wf_is_l_get_owner_document_wf [instances]: "l_get_owner_document_wf heap_is_wellformed type_wf known_ptr known_ptrs get_disconnected_nodes get_owner_document get_parent" using known_ptrs_is_l_known_ptrs - apply(simp add: l_get_owner_document_wf_def l_get_owner_document_wf_axioms_def) - using get_owner_document_disconnected_nodes in_disconnected_nodes_no_parent - by fast + apply(auto simp add: l_get_owner_document_wf_def l_get_owner_document_wf_axioms_def) + using get_owner_document_disconnected_nodes apply fast + using in_disconnected_nodes_no_parent apply fast + using get_owner_document_owner_document_in_heap apply fast + done subsection \Preserving heap-wellformedness\ @@ -3631,6 +3769,7 @@ subsection \adopt\_node\ locale l_adopt_node_wf\<^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_get_parent_wf + + l_get_owner_document_wf + l_remove_child_wf2 + l_heap_is_wellformed begin @@ -3665,6 +3804,65 @@ proof - dest!: reads_writes_separate_forwards[OF get_child_nodes_reads set_disconnected_nodes_writes] split: if_splits) qed + + +lemma adopt_node_document_in_heap: + assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h" + assumes "h \ ok (adopt_node owner_document node)" + shows "owner_document |\| document_ptr_kinds h" +proof - + obtain old_document parent_opt h2 h' where + old_document: "h \ get_owner_document (cast node) \\<^sub>r old_document" and + parent_opt: "h \ get_parent node \\<^sub>r parent_opt" and + h2: "h \ (case parent_opt of Some parent \ do { remove_child parent node } | None \ do { return ()}) \\<^sub>h h2" + and + h': "h2 \ (if owner_document \ old_document then do { + old_disc_nodes \ get_disconnected_nodes old_document; + set_disconnected_nodes old_document (remove1 node old_disc_nodes); + disc_nodes \ get_disconnected_nodes owner_document; + set_disconnected_nodes owner_document (node # 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]) + show ?thesis + proof (cases "owner_document = old_document") + case True + then show ?thesis + using old_document get_owner_document_owner_document_in_heap assms(1) assms(2) assms(3) + by auto + next + case False + + then obtain h3 old_disc_nodes disc_nodes where + old_disc_nodes: "h2 \ get_disconnected_nodes old_document \\<^sub>r old_disc_nodes" and + h3: "h2 \ set_disconnected_nodes old_document (remove1 node old_disc_nodes) \\<^sub>h h3" and + old_disc_nodes: "h3 \ get_disconnected_nodes owner_document \\<^sub>r disc_nodes" and + h': "h3 \ set_disconnected_nodes owner_document (node # disc_nodes) \\<^sub>h h'" + using h' + by(auto elim!: bind_returns_heap_E + bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated] ) + then have "owner_document |\| document_ptr_kinds h3" + by (meson is_OK_returns_result_I local.get_disconnected_nodes_ptr_in_heap) + + moreover have "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) + moreover have "object_ptr_kinds h2 = object_ptr_kinds h3" + apply(rule writes_small_big[where P="\h h'. object_ptr_kinds h = object_ptr_kinds h'", + OF set_disconnected_nodes_writes h3]) + using set_disconnected_nodes_pointers_preserved set_child_nodes_pointers_preserved + by (auto simp add: reflp_def transp_def) + + ultimately show ?thesis + by(auto simp add: document_ptr_kinds_def) + qed +qed end locale l_adopt_node_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M = @@ -4343,6 +4541,9 @@ locale l_adopt_node_wf = l_heap_is_wellformed + l_known_ptrs + l_type_wf + l_ado \ h \ adopt_node owner_document node \\<^sub>h h' \ h \ get_child_nodes ptr' \\<^sub>r node # children \ h' \ get_child_nodes ptr' \\<^sub>r children" + assumes adopt_node_document_in_heap: "heap_is_wellformed h \ known_ptrs h \ type_wf h + \ h \ ok (adopt_node owner_document node) + \ owner_document |\| document_ptr_kinds h" lemma adopt_node_wf_is_l_adopt_node_wf [instances]: "l_adopt_node_wf type_wf known_ptr heap_is_wellformed parent_child_rel get_child_nodes @@ -4353,6 +4554,7 @@ lemma adopt_node_wf_is_l_adopt_node_wf [instances]: using adopt_node_removes_child apply blast using adopt_node_node_in_disconnected_nodes apply blast using adopt_node_removes_first_child apply blast + using adopt_node_document_in_heap apply blast done @@ -5110,7 +5312,7 @@ locale l_create_element_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub l_set_tag_type_get_disconnected_nodes type_wf set_tag_type set_tag_type_locs get_disconnected_nodes get_disconnected_nodes_locs + l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes - set_disconnected_nodes_locs set_tag_type set_tag_type_locs create_element + + set_disconnected_nodes_locs set_tag_type set_tag_type_locs type_wf create_element + l_new_element_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs + l_set_tag_type_get_child_nodes type_wf set_tag_type set_tag_type_locs known_ptr get_child_nodes get_child_nodes_locs + @@ -5516,7 +5718,7 @@ locale l_create_character_data_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub> type_wf set_val set_val_locs get_disconnected_nodes get_disconnected_nodes_locs + l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M set_val set_val_locs get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes - set_disconnected_nodes_locs create_character_data + set_disconnected_nodes_locs type_wf create_character_data + l_new_character_data_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs + l_set_val_get_child_nodes