forked from afp-mirror/Core_DOM
Merge branch 'master' into scope_components
This commit is contained in:
commit
a0c897e2db
|
@ -2785,6 +2785,28 @@ next
|
||||||
qed
|
qed
|
||||||
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
|
end
|
||||||
|
|
||||||
locale l_get_owner_document_wf = l_heap_is_wellformed_defs + l_type_wf + l_known_ptrs
|
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"
|
node_ptr \<in> set disc_nodes"
|
||||||
assumes get_owner_document_owner_document_in_heap:
|
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"
|
"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?:
|
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 get_owner_document_disconnected_nodes apply fast
|
||||||
using in_disconnected_nodes_no_parent apply fast
|
using in_disconnected_nodes_no_parent apply fast
|
||||||
using get_owner_document_owner_document_in_heap apply fast
|
using get_owner_document_owner_document_in_heap apply fast
|
||||||
|
using get_owner_document_ok apply fast
|
||||||
done
|
done
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -244,4 +244,15 @@ proof -
|
||||||
using object_ptr_kinds_preserved_small by blast
|
using object_ptr_kinds_preserved_small by blast
|
||||||
qed
|
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
|
end
|
||||||
|
|
Reference in New Issue