From 9f48ee249e2ff178582bceb63c96efd4d07fd0fb Mon Sep 17 00:00:00 2001 From: Michael Herzberg Date: Mon, 1 Apr 2019 17:43:00 +0100 Subject: [PATCH] Proved get_root_node_same_owner_document. --- Core_DOM/Core_DOM_Heap_WF.thy | 116 +++++++++++++++++++++++++++++++++- 1 file changed, 115 insertions(+), 1 deletion(-) diff --git a/Core_DOM/Core_DOM_Heap_WF.thy b/Core_DOM/Core_DOM_Heap_WF.thy index 46d6bda..d87cc7a 100644 --- a/Core_DOM/Core_DOM_Heap_WF.thy +++ b/Core_DOM/Core_DOM_Heap_WF.thy @@ -2889,7 +2889,121 @@ lemma get_root_node_same_owner_document: assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h" assumes "h \ get_root_node ptr \\<^sub>r root" shows "h \ get_owner_document ptr \\<^sub>r owner_document \ h \ get_owner_document root \\<^sub>r owner_document" - sorry +proof - + have "ptr |\| object_ptr_kinds h" + by (meson assms(4) is_OK_returns_result_I local.get_root_node_ptr_in_heap) + have "root |\| object_ptr_kinds h" + using assms(1) assms(2) assms(3) assms(4) local.get_root_node_root_in_heap by blast + have "known_ptr ptr" + using \ptr |\| object_ptr_kinds h\ assms(3) local.known_ptrs_known_ptr by blast + have "known_ptr root" + using \root |\| object_ptr_kinds h\ assms(3) local.known_ptrs_known_ptr by blast + show ?thesis + proof (cases "is_document_ptr_kind ptr") + case True + then + have "ptr = root" + using assms(4) + apply(auto simp add: get_root_node_def elim!: bind_returns_result_E2) + by (metis document_ptr_casts_commute3 last_ConsL local.get_ancestors_not_node node_ptr_no_document_ptr_cast) + then show ?thesis + by auto + next + case False + then have "is_node_ptr_kind ptr" + using \known_ptr ptr\ + by(auto simp add: known_ptr_impl DocumentClass.known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits) + then obtain node_ptr where node_ptr: "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 node_ptr" + by (metis node_ptr_casts_commute3) + show ?thesis + proof + assume "h \ get_owner_document ptr \\<^sub>r owner_document" + then have "h \ local.a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r node_ptr () \\<^sub>r owner_document" + using node_ptr + apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def) + apply(split invoke_splits)+ + apply (meson invoke_empty is_OK_returns_result_I) + by(auto elim!: bind_returns_result_E2 split: option.splits) + + show "h \ get_owner_document root \\<^sub>r owner_document" + proof (cases "is_document_ptr_kind root") + case True + have "is_document_ptr root" + using True \known_ptr root\ + by(auto simp add: known_ptr_impl DocumentClass.known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits) + have "root = cast owner_document" + using True + by (smt \h \ get_owner_document ptr \\<^sub>r owner_document\ assms(1) assms(2) assms(3) assms(4) document_ptr_casts_commute3 get_root_node_document returns_result_eq) + then show ?thesis + apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def) + apply(split invoke_splits, (rule conjI | rule impI)+)+ + using \is_document_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r root\ apply blast + using \root |\| object_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 is_node_ptr_kind_none) + + next + case False + then have "is_node_ptr_kind root" + using \known_ptr root\ + by(auto simp add: known_ptr_impl DocumentClass.known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits) + then obtain root_node_ptr where root_node_ptr: "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 root_node_ptr" + by (metis node_ptr_casts_commute3) + then have "h \ local.a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r root_node_ptr () \\<^sub>r owner_document" + using \h \ local.a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r node_ptr () \\<^sub>r owner_document\ assms(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!: bind_pure_returns_result_I filter_M_pure_I bind_pure_I split: option.splits) + apply (metis assms(1) assms(2) assms(3) local.get_root_node_no_parent local.get_root_node_same_no_parent node_ptr returns_result_eq) + using \is_node_ptr_kind root\ node_ptr returns_result_eq by fastforce + then show ?thesis + apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def) + apply(split invoke_splits, (rule conjI | rule impI)+)+ + using \is_node_ptr_kind root\ \known_ptr root\ + apply(auto simp add: known_ptr_impl DocumentClass.known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)[2] + using \root |\| object_ptr_kinds h\ + by(auto simp add: root_node_ptr) + qed + next + assume "h \ get_owner_document root \\<^sub>r owner_document" + show "h \ get_owner_document ptr \\<^sub>r owner_document" + proof (cases "is_document_ptr_kind root") + case True + have "root = cast owner_document" + using \h \ get_owner_document root \\<^sub>r owner_document\ + apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def) + apply(split invoke_splits)+ + apply (meson invoke_empty is_OK_returns_result_I) + apply(auto simp add: True 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) + apply (metis True cast_document_ptr_not_node_ptr(2) is_document_ptr_kind_obtains is_node_ptr_kind_none node_ptr_casts_commute3 option.case_eq_if) + by (metis True cast_document_ptr_not_node_ptr(1) document_ptr_casts_commute3 is_node_ptr_kind_none node_ptr_casts_commute3 option.case_eq_if) + then show ?thesis + using assms(1) assms(2) assms(3) assms(4) get_root_node_document + by fastforce + next + case False + then have "is_node_ptr_kind root" + using \known_ptr root\ + by(auto simp add: known_ptr_impl DocumentClass.known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits) + then obtain root_node_ptr where root_node_ptr: "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 root_node_ptr" + by (metis node_ptr_casts_commute3) + then have "h \ local.a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r root_node_ptr () \\<^sub>r owner_document" + using \h \ get_owner_document root \\<^sub>r owner_document\ + apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def) + apply(split invoke_splits)+ + apply (meson invoke_empty is_OK_returns_result_I) + by(auto simp add: is_document_ptr_kind_none elim!: bind_returns_result_E2) + then have "h \ local.a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r node_ptr () \\<^sub>r owner_document" + 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!: bind_pure_returns_result_I filter_M_pure_I bind_pure_I split: option.splits) + using assms(1) assms(2) assms(3) assms(4) local.get_root_node_no_parent local.get_root_node_same_no_parent node_ptr returns_result_eq root_node_ptr + by fastforce+ + then show ?thesis + apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def) + apply(split invoke_splits, (rule conjI | rule impI)+)+ + using node_ptr \known_ptr ptr\ \ptr |\| object_ptr_kinds h\ + + by(auto simp add: known_ptr_impl DocumentClass.known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs intro!: bind_pure_returns_result_I split: option.splits) + qed + qed + qed +qed end interpretation get_owner_document_wf_get_root_node_wf?: l_get_owner_document_wf_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M type_wf known_ptr known_ptrs get_parent get_parent_locs get_child_nodes get_child_nodes_locs get_ancestors get_ancestors_locs get_root_node get_root_node_locs heap_is_wellformed parent_child_rel get_disconnected_nodes get_disconnected_nodes_locs get_owner_document