forked from afp-mirror/Core_DOM
Added get_owner_document_ok and reads_writes_preserved2.
This commit is contained in:
parent
9f48ee249e
commit
2a97e8efe2
|
@ -2785,6 +2785,28 @@ next
|
|||
qed
|
||||
qed
|
||||
|
||||
lemma get_owner_document_ok:
|
||||
assumes "heap_is_wellformed h" "known_ptrs h" "type_wf h"
|
||||
assumes "ptr |\<in>| object_ptr_kinds h"
|
||||
shows "h \<turnstile> ok (get_owner_document ptr)"
|
||||
proof -
|
||||
have "known_ptr ptr"
|
||||
using assms(2) assms(4) local.known_ptrs_known_ptr
|
||||
by blast
|
||||
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)+)+
|
||||
apply(auto simp add: known_ptr_impl)[1]
|
||||
using NodeClass.a_known_ptr_def known_ptr_not_character_data_ptr known_ptr_not_document_ptr known_ptr_not_element_ptr apply blast
|
||||
using assms(4)
|
||||
apply(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 a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def intro!: bind_is_OK_pure_I)
|
||||
apply (metis (no_types, lifting) document_ptr_casts_commute3 document_ptr_kinds_commutes is_document_ptr_kind_none option.case_eq_if)
|
||||
apply (metis (no_types, lifting) assms(1) assms(2) assms(3) is_node_ptr_kind_none local.get_root_node_ok node_ptr_casts_commute3 option.case_eq_if)
|
||||
apply(auto split: option.splits intro!: bind_is_OK_pure_I filter_M_pure_I bind_pure_I filter_M_is_OK_I)
|
||||
using assms(3) local.get_disconnected_nodes_ok apply blast
|
||||
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
|
||||
end
|
||||
|
||||
locale l_get_owner_document_wf = l_heap_is_wellformed_defs + l_type_wf + l_known_ptrs
|
||||
|
@ -2807,6 +2829,9 @@ locale l_get_owner_document_wf = l_heap_is_wellformed_defs + l_type_wf + l_known
|
|||
node_ptr \<in> set disc_nodes"
|
||||
assumes get_owner_document_owner_document_in_heap:
|
||||
"heap_is_wellformed h \<Longrightarrow> type_wf h \<Longrightarrow> known_ptrs h \<Longrightarrow> h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document \<Longrightarrow> owner_document |\<in>| document_ptr_kinds h"
|
||||
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)"
|
||||
|
||||
|
||||
interpretation i_get_owner_document_wf?:
|
||||
|
@ -2826,6 +2851,7 @@ lemma get_owner_document_wf_is_l_get_owner_document_wf [instances]:
|
|||
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
|
||||
done
|
||||
|
||||
|
||||
|
|
|
@ -244,4 +244,15 @@ proof -
|
|||
using object_ptr_kinds_preserved_small by blast
|
||||
qed
|
||||
|
||||
|
||||
lemma reads_writes_preserved2:
|
||||
assumes "writes SW setter h h'"
|
||||
assumes "h \<turnstile> setter \<rightarrow>\<^sub>h h'"
|
||||
assumes "\<And>h h' x. \<forall>w \<in> SW. h \<turnstile> w \<rightarrow>\<^sub>h h' \<longrightarrow> preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr getter) h h'"
|
||||
shows "preserved (get_M ptr getter) h h'"
|
||||
apply(clarsimp simp add: preserved_def)
|
||||
using reads_singleton assms(1) assms(2)
|
||||
apply(rule reads_writes_preserved)
|
||||
using assms(3)
|
||||
by(auto simp add: preserved_def)
|
||||
end
|
||||
|
|
Reference in New Issue