forked from afp-mirror/Core_DOM
Added lemma get_owner_document_child_same.
This commit is contained in:
Michael Herzberg
parent
a0c897e2db
commit
b210f725ca
|
|
@ -2494,7 +2494,7 @@ subsection \<open>get\_owner\_document\<close>
|
|||
locale l_get_owner_document_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
|
||||
l_known_ptrs
|
||||
+ l_heap_is_wellformed
|
||||
+ l_get_root_node
|
||||
+ l_get_root_node\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
|
||||
+ l_get_ancestors
|
||||
+ l_get_ancestors_wf
|
||||
+ l_get_parent
|
||||
|
|
@ -2807,11 +2807,93 @@ proof -
|
|||
apply (simp add: assms(1) assms(2) assms(3) local.get_root_node_ok)
|
||||
using assms(3) local.get_disconnected_nodes_ok by blast
|
||||
qed
|
||||
|
||||
lemma get_owner_document_child_same:
|
||||
assumes "heap_is_wellformed h" "known_ptrs h" "type_wf h"
|
||||
assumes "h \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children"
|
||||
assumes "child \<in> set children"
|
||||
shows "h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document \<longleftrightarrow> h \<turnstile> get_owner_document (cast child) \<rightarrow>\<^sub>r owner_document"
|
||||
proof -
|
||||
have "ptr |\<in>| object_ptr_kinds h"
|
||||
by (meson assms(4) is_OK_returns_result_I local.get_child_nodes_ptr_in_heap)
|
||||
then have "known_ptr ptr"
|
||||
using assms(2) local.known_ptrs_known_ptr by blast
|
||||
|
||||
have "cast child |\<in>| object_ptr_kinds h"
|
||||
using assms(1) assms(4) assms(5) local.heap_is_wellformed_children_in_heap node_ptr_kinds_commutes by blast
|
||||
then
|
||||
have "known_ptr (cast child)"
|
||||
using assms(2) local.known_ptrs_known_ptr by blast
|
||||
|
||||
obtain root where root: "h \<turnstile> get_root_node ptr \<rightarrow>\<^sub>r root"
|
||||
by (meson \<open>ptr |\<in>| object_ptr_kinds h\<close> assms(1) assms(2) assms(3) is_OK_returns_result_E local.get_root_node_ok)
|
||||
then have "h \<turnstile> get_root_node (cast child) \<rightarrow>\<^sub>r root"
|
||||
using assms(1) assms(2) assms(3) assms(4) assms(5) local.child_parent_dual local.get_root_node_parent_same by blast
|
||||
|
||||
have "h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document \<longleftrightarrow> h \<turnstile> a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r child () \<rightarrow>\<^sub>r owner_document"
|
||||
proof (cases "is_document_ptr ptr")
|
||||
case True
|
||||
then obtain document_ptr where document_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 = ptr"
|
||||
using case_optionE document_ptr_casts_commute by blast
|
||||
then have "root = cast document_ptr"
|
||||
using root
|
||||
by(auto simp add: get_root_node_def get_ancestors_def elim!: bind_returns_result_E2 split: option.splits)
|
||||
|
||||
then have "h \<turnstile> 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 document_ptr () \<rightarrow>\<^sub>r owner_document \<longleftrightarrow> h \<turnstile> a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r child () \<rightarrow>\<^sub>r owner_document"
|
||||
using document_ptr \<open>h \<turnstile> get_root_node (cast child) \<rightarrow>\<^sub>r root\<close>[simplified \<open>root = cast document_ptr\<close> document_ptr]
|
||||
apply(auto simp add: a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def 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 dest!: bind_returns_result_E3[rotated, OF \<open>h \<turnstile> get_root_node (cast child) \<rightarrow>\<^sub>r root\<close>[simplified \<open>root = cast document_ptr\<close> document_ptr], rotated] intro!: bind_pure_returns_result_I filter_M_pure_I bind_pure_I split: if_splits option.splits)
|
||||
using \<open>ptr |\<in>| object_ptr_kinds h\<close> document_ptr_kinds_commutes by blast
|
||||
then show ?thesis
|
||||
using \<open>known_ptr ptr\<close>
|
||||
apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def known_ptr_impl)
|
||||
apply(split invoke_splits, ((rule conjI | rule impI)+)?)+
|
||||
apply(drule(1) known_ptr_not_document_ptr[folded known_ptr_impl])
|
||||
apply(drule(1) known_ptr_not_character_data_ptr)
|
||||
apply(drule(1) known_ptr_not_element_ptr)
|
||||
apply(simp add: NodeClass.known_ptr_defs)
|
||||
using \<open>ptr |\<in>| object_ptr_kinds h\<close> True
|
||||
by(auto simp add: document_ptr[symmetric] intro!: bind_pure_returns_result_I split: option.splits)
|
||||
next
|
||||
case False
|
||||
then obtain node_ptr where node_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 = 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 have "h \<turnstile> 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 \<longleftrightarrow> h \<turnstile> a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r child () \<rightarrow>\<^sub>r owner_document"
|
||||
using root \<open>h \<turnstile> get_root_node (cast child) \<rightarrow>\<^sub>r root\<close>
|
||||
unfolding a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def
|
||||
by (meson bind_pure_returns_result_I bind_returns_result_E3 local.get_root_node_pure)
|
||||
then show ?thesis
|
||||
using \<open>known_ptr ptr\<close>
|
||||
apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def known_ptr_impl)
|
||||
apply(split invoke_splits, ((rule conjI | rule impI)+)?)+
|
||||
apply(drule(1) known_ptr_not_document_ptr[folded known_ptr_impl])
|
||||
apply(drule(1) known_ptr_not_character_data_ptr)
|
||||
apply(drule(1) known_ptr_not_element_ptr)
|
||||
apply(simp add: NodeClass.known_ptr_defs)
|
||||
using \<open>cast child |\<in>| object_ptr_kinds h\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close> False
|
||||
apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )
|
||||
apply(split invoke_splits, ((rule conjI | rule impI)+)?)+
|
||||
apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )
|
||||
by (meson invoke_empty is_OK_returns_result_I)
|
||||
qed
|
||||
then show ?thesis
|
||||
using \<open>known_ptr (cast child)\<close>
|
||||
apply(auto simp add: get_owner_document_def[of "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"] a_get_owner_document_tups_def known_ptr_impl)
|
||||
apply(split invoke_splits, ((rule conjI | rule impI)+)?)+
|
||||
apply(drule(1) known_ptr_not_document_ptr[folded known_ptr_impl])
|
||||
apply(drule(1) known_ptr_not_character_data_ptr)
|
||||
apply(drule(1) known_ptr_not_element_ptr)
|
||||
apply(simp add: NodeClass.known_ptr_defs)
|
||||
using \<open>cast child |\<in>| object_ptr_kinds h\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close>
|
||||
apply(auto intro!: bind_pure_returns_result_I split: option.splits)
|
||||
by (smt \<open>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 |\<in>| object_ptr_kinds h\<close> cast_document_ptr_not_node_ptr(1) comp_apply invoke_empty invoke_not invoke_returns_result is_OK_returns_result_I node_ptr_casts_commute2 option.sel)
|
||||
qed
|
||||
|
||||
end
|
||||
|
||||
locale l_get_owner_document_wf = l_heap_is_wellformed_defs + l_type_wf + l_known_ptrs
|
||||
+ l_get_disconnected_nodes_defs + l_get_owner_document_defs
|
||||
+ l_get_parent_defs +
|
||||
+ l_get_parent_defs + l_get_child_nodes_defs +
|
||||
assumes get_owner_document_disconnected_nodes:
|
||||
"heap_is_wellformed h \<Longrightarrow>
|
||||
known_ptrs h \<Longrightarrow>
|
||||
|
|
@ -2832,26 +2914,24 @@ locale l_get_owner_document_wf = l_heap_is_wellformed_defs + l_type_wf + l_known
|
|||
assumes get_owner_document_ok:
|
||||
"heap_is_wellformed h \<Longrightarrow> known_ptrs h \<Longrightarrow> type_wf h \<Longrightarrow> ptr |\<in>| object_ptr_kinds h
|
||||
\<Longrightarrow> h \<turnstile> ok (get_owner_document ptr)"
|
||||
assumes get_owner_document_child_same:
|
||||
"heap_is_wellformed h \<Longrightarrow> type_wf h \<Longrightarrow> known_ptrs h \<Longrightarrow> h \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children \<Longrightarrow> child \<in> set children \<Longrightarrow> h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document \<longleftrightarrow> h \<turnstile> get_owner_document (cast child) \<rightarrow>\<^sub>r owner_document"
|
||||
|
||||
|
||||
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
|
||||
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)
|
||||
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_parent get_parent_locs get_ancestors get_ancestors_locs get_root_node get_root_node_locs get_owner_document
|
||||
by(auto 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"
|
||||
get_owner_document get_parent get_child_nodes"
|
||||
using known_ptrs_is_l_known_ptrs
|
||||
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
|
||||
using get_owner_document_ok apply fast
|
||||
using get_owner_document_child_same apply (fast, fast)
|
||||
done
|
||||
|
||||
|
||||
|
|
|
|||
Reference in New Issue