Proved get_root_node_same_owner_document.

This commit is contained in:
Michael Herzberg 2019-04-01 17:43:00 +01:00
parent d90812beed
commit 9f48ee249e
1 changed files with 115 additions and 1 deletions

View File

@ -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 \<turnstile> get_root_node ptr \<rightarrow>\<^sub>r root"
shows "h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document \<longleftrightarrow> h \<turnstile> get_owner_document root \<rightarrow>\<^sub>r owner_document"
sorry
proof -
have "ptr |\<in>| object_ptr_kinds h"
by (meson assms(4) is_OK_returns_result_I local.get_root_node_ptr_in_heap)
have "root |\<in>| 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 \<open>ptr |\<in>| object_ptr_kinds h\<close> assms(3) local.known_ptrs_known_ptr by blast
have "known_ptr root"
using \<open>root |\<in>| object_ptr_kinds h\<close> 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 \<open>known_ptr ptr\<close>
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 \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document"
then have "h \<turnstile> local.a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r node_ptr () \<rightarrow>\<^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 \<turnstile> get_owner_document root \<rightarrow>\<^sub>r owner_document"
proof (cases "is_document_ptr_kind root")
case True
have "is_document_ptr root"
using True \<open>known_ptr root\<close>
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 \<open>h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document\<close> 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 \<open>is_document_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r root\<close> apply blast
using \<open>root |\<in>| object_ptr_kinds h\<close>
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 \<open>known_ptr root\<close>
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 \<turnstile> local.a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r root_node_ptr () \<rightarrow>\<^sub>r owner_document"
using \<open>h \<turnstile> local.a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r node_ptr () \<rightarrow>\<^sub>r owner_document\<close> 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 \<open>is_node_ptr_kind root\<close> 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 \<open>is_node_ptr_kind root\<close> \<open>known_ptr root\<close>
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 \<open>root |\<in>| object_ptr_kinds h\<close>
by(auto simp add: root_node_ptr)
qed
next
assume "h \<turnstile> get_owner_document root \<rightarrow>\<^sub>r owner_document"
show "h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document"
proof (cases "is_document_ptr_kind root")
case True
have "root = cast owner_document"
using \<open>h \<turnstile> get_owner_document root \<rightarrow>\<^sub>r owner_document\<close>
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 \<open>known_ptr root\<close>
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 \<turnstile> local.a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r root_node_ptr () \<rightarrow>\<^sub>r owner_document"
using \<open>h \<turnstile> get_owner_document root \<rightarrow>\<^sub>r owner_document\<close>
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 \<turnstile> local.a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r node_ptr () \<rightarrow>\<^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 \<open>known_ptr ptr\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close>
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