forked from afp-mirror/Core_DOM
Added more lemmas.
This commit is contained in:
Michael Herzberg
parent
ae19cacb08
commit
b7fa25e301
|
|
@ -3167,19 +3167,51 @@ global_interpretation l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<
|
|||
|
||||
locale l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
|
||||
l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs +
|
||||
l_get_disconnected_nodes +
|
||||
l_set_tag_type +
|
||||
l_create_element_defs +
|
||||
assumes create_element_impl: "create_element = a_create_element"
|
||||
begin
|
||||
lemmas create_element_def = a_create_element_def[folded create_element_impl]
|
||||
|
||||
lemma create_element_document_in_heap:
|
||||
assumes "h \<turnstile> ok (create_element document_ptr tag)"
|
||||
shows "document_ptr |\<in>| document_ptr_kinds h"
|
||||
proof -
|
||||
obtain h' where "h \<turnstile> create_element document_ptr tag \<rightarrow>\<^sub>h h'"
|
||||
using assms(1)
|
||||
by auto
|
||||
then
|
||||
obtain new_element_ptr h2 h3 disc_nodes_h3 where
|
||||
new_element_ptr: "h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr" and
|
||||
h2: "h \<turnstile> new_element \<rightarrow>\<^sub>h h2" and
|
||||
h3: "h2 \<turnstile> set_tag_type new_element_ptr tag \<rightarrow>\<^sub>h h3" and
|
||||
disc_nodes_h3: "h3 \<turnstile> get_disconnected_nodes document_ptr \<rightarrow>\<^sub>r disc_nodes_h3" and
|
||||
h': "h3 \<turnstile> set_disconnected_nodes document_ptr (cast new_element_ptr # disc_nodes_h3) \<rightarrow>\<^sub>h h'"
|
||||
by(auto simp add: create_element_def
|
||||
elim!: bind_returns_heap_E
|
||||
bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated] )
|
||||
|
||||
have object_ptr_kinds_eq_h: "object_ptr_kinds h2 = object_ptr_kinds h |\<union>| {|cast new_element_ptr|}"
|
||||
using new_element_new_ptr h2 new_element_ptr by blast
|
||||
|
||||
moreover have object_ptr_kinds_eq_h2: "object_ptr_kinds h3 = object_ptr_kinds h2"
|
||||
apply(rule writes_small_big[where P="\<lambda>h h'. object_ptr_kinds h' = object_ptr_kinds h", OF set_tag_type_writes h3])
|
||||
using set_tag_type_pointers_preserved
|
||||
by (auto simp add: reflp_def transp_def)
|
||||
moreover have "document_ptr |\<in>| document_ptr_kinds h3"
|
||||
by (meson disc_nodes_h3 is_OK_returns_result_I local.get_disconnected_nodes_ptr_in_heap)
|
||||
|
||||
ultimately show ?thesis
|
||||
by (auto simp add: document_ptr_kinds_def)
|
||||
qed
|
||||
end
|
||||
|
||||
locale l_create_element = l_create_element_defs
|
||||
|
||||
interpretation
|
||||
i_create_element?: l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_disconnected_nodes get_disconnected_nodes_locs
|
||||
set_disconnected_nodes set_disconnected_nodes_locs set_tag_type
|
||||
set_tag_type_locs create_element
|
||||
by unfold_locales (simp add: create_element_def)
|
||||
i_create_element?: l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs set_tag_type set_tag_type_locs type_wf create_element
|
||||
by(auto simp add: l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms_def create_element_def instances)
|
||||
declare l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms[instances]
|
||||
|
||||
|
||||
|
|
@ -3218,19 +3250,51 @@ global_interpretation l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^
|
|||
|
||||
locale l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
|
||||
l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs +
|
||||
l_get_disconnected_nodes +
|
||||
l_set_val +
|
||||
l_create_character_data_defs +
|
||||
assumes create_character_data_impl: "create_character_data = a_create_character_data"
|
||||
begin
|
||||
lemmas create_character_data_def = a_create_character_data_def[folded create_character_data_impl]
|
||||
|
||||
lemma create_character_data_document_in_heap:
|
||||
assumes "h \<turnstile> ok (create_character_data document_ptr text)"
|
||||
shows "document_ptr |\<in>| document_ptr_kinds h"
|
||||
proof -
|
||||
obtain h' where "h \<turnstile> create_character_data document_ptr text \<rightarrow>\<^sub>h h'"
|
||||
using assms(1)
|
||||
by auto
|
||||
then
|
||||
obtain new_character_data_ptr h2 h3 disc_nodes_h3 where
|
||||
new_character_data_ptr: "h \<turnstile> new_character_data \<rightarrow>\<^sub>r new_character_data_ptr" and
|
||||
h2: "h \<turnstile> new_character_data \<rightarrow>\<^sub>h h2" and
|
||||
h3: "h2 \<turnstile> set_val new_character_data_ptr text \<rightarrow>\<^sub>h h3" and
|
||||
disc_nodes_h3: "h3 \<turnstile> get_disconnected_nodes document_ptr \<rightarrow>\<^sub>r disc_nodes_h3" and
|
||||
h': "h3 \<turnstile> set_disconnected_nodes document_ptr (cast new_character_data_ptr # disc_nodes_h3) \<rightarrow>\<^sub>h h'"
|
||||
by(auto simp add: create_character_data_def
|
||||
elim!: bind_returns_heap_E
|
||||
bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated] )
|
||||
|
||||
have object_ptr_kinds_eq_h: "object_ptr_kinds h2 = object_ptr_kinds h |\<union>| {|cast new_character_data_ptr|}"
|
||||
using new_character_data_new_ptr h2 new_character_data_ptr by blast
|
||||
|
||||
moreover have object_ptr_kinds_eq_h2: "object_ptr_kinds h3 = object_ptr_kinds h2"
|
||||
apply(rule writes_small_big[where P="\<lambda>h h'. object_ptr_kinds h' = object_ptr_kinds h", OF set_val_writes h3])
|
||||
using set_val_pointers_preserved
|
||||
by (auto simp add: reflp_def transp_def)
|
||||
moreover have "document_ptr |\<in>| document_ptr_kinds h3"
|
||||
by (meson disc_nodes_h3 is_OK_returns_result_I local.get_disconnected_nodes_ptr_in_heap)
|
||||
|
||||
ultimately show ?thesis
|
||||
by (auto simp add: document_ptr_kinds_def)
|
||||
qed
|
||||
end
|
||||
|
||||
locale l_create_character_data = l_create_character_data_defs
|
||||
|
||||
interpretation
|
||||
i_create_character_data?: l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M set_val set_val_locs get_disconnected_nodes
|
||||
get_disconnected_nodes_locs set_disconnected_nodes
|
||||
set_disconnected_nodes_locs create_character_data
|
||||
by unfold_locales (simp add: create_character_data_def)
|
||||
i_create_character_data?: l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M set_val set_val_locs get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs type_wf create_character_data
|
||||
by(auto simp add: l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms_def create_character_data_def instances)
|
||||
declare l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -517,8 +517,8 @@ proof -
|
|||
proof (induct rule: wf_induct_rule)
|
||||
case (less parent)
|
||||
then show ?case
|
||||
using assms child_parent_dual parent_child_rel_parent
|
||||
by (meson converse_iff parent_child_rel_child)
|
||||
using assms parent_child_rel_child
|
||||
by (meson converse_iff)
|
||||
qed
|
||||
qed
|
||||
|
||||
|
|
@ -1764,9 +1764,9 @@ locale l_get_root_node_wf = l_heap_is_wellformed_defs + l_get_root_node_defs + l
|
|||
assumes get_root_node_same_no_parent:
|
||||
"heap_is_wellformed h \<Longrightarrow> type_wf h \<Longrightarrow> known_ptrs h
|
||||
\<Longrightarrow> h \<turnstile> get_root_node ptr \<rightarrow>\<^sub>r cast child \<Longrightarrow> h \<turnstile> get_parent child \<rightarrow>\<^sub>r None"
|
||||
assumes get_root_node_not_node_same:
|
||||
(* assumes get_root_node_not_node_same:
|
||||
"ptr |\<in>| object_ptr_kinds h \<Longrightarrow> \<not>is_node_ptr_kind ptr
|
||||
\<Longrightarrow> h \<turnstile> get_root_node ptr \<rightarrow>\<^sub>r ptr"
|
||||
\<Longrightarrow> h \<turnstile> get_root_node ptr \<rightarrow>\<^sub>r ptr" *)
|
||||
assumes get_root_node_parent_same:
|
||||
"h \<turnstile> get_parent child \<rightarrow>\<^sub>r Some ptr
|
||||
\<Longrightarrow> h \<turnstile> get_root_node (cast child) \<rightarrow>\<^sub>r root \<longleftrightarrow> h \<turnstile> get_root_node ptr \<rightarrow>\<^sub>r root"
|
||||
|
|
@ -1805,7 +1805,7 @@ lemma get_root_node_wf_is_l_get_root_node_wf [instances]:
|
|||
using get_root_node_root_in_heap apply blast
|
||||
using get_ancestors_same_root_node apply(blast, blast)
|
||||
using get_root_node_same_no_parent apply blast
|
||||
using get_root_node_not_node_same apply blast
|
||||
(* using get_root_node_not_node_same apply blast *)
|
||||
using get_root_node_parent_same apply (blast, blast)
|
||||
done
|
||||
|
||||
|
|
@ -2374,13 +2374,8 @@ lemma to_tree_order_wf_is_l_to_tree_order_wf [instances]:
|
|||
subsubsection \<open>get\_root\_node\<close>
|
||||
|
||||
locale l_to_tree_order_wf_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
|
||||
l_get_ancestors
|
||||
+ l_get_ancestors_wf
|
||||
+ l_get_root_node
|
||||
+ l_get_root_node_wf
|
||||
l_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
|
||||
+ l_to_tree_order_wf
|
||||
+ l_get_parent
|
||||
+ l_get_parent_wf
|
||||
begin
|
||||
lemma to_tree_order_get_root_node:
|
||||
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
|
||||
|
|
@ -2467,9 +2462,7 @@ qed
|
|||
end
|
||||
|
||||
interpretation i_to_tree_order_wf_get_root_node_wf?: l_to_tree_order_wf_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
|
||||
get_ancestors get_ancestors_locs heap_is_wellformed parent_child_rel known_ptr
|
||||
known_ptrs type_wf get_child_nodes get_child_nodes_locs get_parent get_parent_locs
|
||||
get_root_node get_root_node_locs to_tree_order
|
||||
known_ptr type_wf known_ptrs 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 to_tree_order
|
||||
using instances
|
||||
by(simp add: l_to_tree_order_wf_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def)
|
||||
|
||||
|
|
@ -2506,6 +2499,7 @@ locale l_get_owner_document_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<
|
|||
+ l_get_ancestors_wf
|
||||
+ l_get_parent
|
||||
+ l_get_parent_wf
|
||||
+ l_get_root_node_wf
|
||||
+ l_get_owner_document\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
|
||||
begin
|
||||
|
||||
|
|
@ -2643,6 +2637,154 @@ proof -
|
|||
returns_result_select_result select_result_I2
|
||||
by (metis (no_types, hide_lams) )
|
||||
qed
|
||||
|
||||
lemma get_owner_document_owner_document_in_heap:
|
||||
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
|
||||
assumes "h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document"
|
||||
shows "owner_document |\<in>| document_ptr_kinds h"
|
||||
using assms
|
||||
apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def)
|
||||
apply(split invoke_split_asm)+
|
||||
proof -
|
||||
assume "h \<turnstile> invoke [] ptr () \<rightarrow>\<^sub>r owner_document"
|
||||
then show "owner_document |\<in>| document_ptr_kinds h"
|
||||
by (meson invoke_empty is_OK_returns_result_I)
|
||||
next
|
||||
assume "h \<turnstile> Heap_Error_Monad.bind (check_in_heap ptr)
|
||||
(\<lambda>_. (local.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 \<circ> the \<circ> cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r) ptr ())
|
||||
\<rightarrow>\<^sub>r owner_document"
|
||||
then show "owner_document |\<in>| document_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 elim!: bind_returns_result_E2 split: if_splits)
|
||||
next
|
||||
assume 0: "heap_is_wellformed h"
|
||||
and 1: "type_wf h"
|
||||
and 2: "known_ptrs h"
|
||||
and 3: "\<not> is_element_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr"
|
||||
and 4: "is_character_data_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr"
|
||||
and 5: "h \<turnstile> Heap_Error_Monad.bind (check_in_heap ptr) (\<lambda>_. (local.a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r \<circ> the \<circ> cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r) ptr ()) \<rightarrow>\<^sub>r owner_document"
|
||||
then obtain root where
|
||||
root: "h \<turnstile> get_root_node ptr \<rightarrow>\<^sub>r root"
|
||||
by(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 split: option.splits)
|
||||
|
||||
then show ?thesis
|
||||
proof (cases "is_document_ptr root")
|
||||
case True
|
||||
then show ?thesis
|
||||
using 4 5 root
|
||||
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!: filter_M_pure_I bind_pure_I split: option.splits)[1]
|
||||
apply(drule(1) returns_result_eq) apply(auto)[1]
|
||||
using "0" "1" "2" document_ptr_kinds_commutes local.get_root_node_root_in_heap by blast
|
||||
next
|
||||
case False
|
||||
have "known_ptr root"
|
||||
using "0" "1" "2" local.get_root_node_root_in_heap local.known_ptrs_known_ptr root by blast
|
||||
have "root |\<in>| object_ptr_kinds h"
|
||||
using root
|
||||
using "0" "1" "2" local.get_root_node_root_in_heap
|
||||
by blast
|
||||
then have "is_node_ptr_kind root"
|
||||
using False \<open>known_ptr root\<close>
|
||||
apply(simp add: known_ptr_impl known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs)
|
||||
using is_node_ptr_kind_none by force
|
||||
then
|
||||
have "(\<exists>document_ptr \<in> fset (document_ptr_kinds h). root \<in> cast ` set |h \<turnstile> get_disconnected_nodes document_ptr|\<^sub>r)"
|
||||
by (metis (no_types, lifting) "0" "1" "2" \<open>root |\<in>| object_ptr_kinds h\<close> local.child_parent_dual local.get_child_nodes_ok local.get_root_node_same_no_parent local.heap_is_wellformed_children_disc_nodes local.known_ptrs_known_ptr node_ptr_casts_commute3 node_ptr_inclusion node_ptr_kinds_commutes notin_fset option.distinct(1) returns_result_eq returns_result_select_result root)
|
||||
then obtain some_owner_document where
|
||||
"some_owner_document |\<in>| document_ptr_kinds h" and
|
||||
"root \<in> cast ` set |h \<turnstile> get_disconnected_nodes some_owner_document|\<^sub>r"
|
||||
by auto
|
||||
then
|
||||
obtain candidates where
|
||||
candidates: "h \<turnstile> filter_M
|
||||
(\<lambda>document_ptr.
|
||||
Heap_Error_Monad.bind (get_disconnected_nodes document_ptr)
|
||||
(\<lambda>disconnected_nodes. return (root \<in> 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 ` set disconnected_nodes)))
|
||||
(sorted_list_of_set (fset (document_ptr_kinds h)))
|
||||
\<rightarrow>\<^sub>r candidates"
|
||||
by (metis (no_types, lifting) "1" bind_is_OK_I2 bind_pure_I filter_M_is_OK_I finite_fset is_OK_returns_result_E local.get_disconnected_nodes_ok local.get_disconnected_nodes_pure notin_fset return_ok return_pure sorted_list_of_set(1))
|
||||
then have "some_owner_document \<in> set candidates"
|
||||
apply(rule filter_M_in_result_if_ok)
|
||||
using \<open>some_owner_document |\<in>| document_ptr_kinds h\<close> \<open>root \<in> cast ` set |h \<turnstile> get_disconnected_nodes some_owner_document|\<^sub>r\<close>
|
||||
apply(auto intro!: bind_pure_I bind_pure_returns_result_I)
|
||||
by (simp add: "1" local.get_disconnected_nodes_ok)
|
||||
|
||||
then have "candidates \<noteq> []"
|
||||
by auto
|
||||
then have "owner_document \<in> set candidates"
|
||||
using 5 root 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!: filter_M_pure_I bind_pure_I split: option.splits)[1]
|
||||
apply (metis candidates list.set_sel(1) returns_result_eq)
|
||||
by (metis \<open>is_node_ptr_kind root\<close> node_ptr_no_document_ptr_cast returns_result_eq)
|
||||
|
||||
then show ?thesis
|
||||
using candidates
|
||||
by (meson bind_pure_I bind_returns_result_E2 filter_M_holds_for_result is_OK_returns_result_I local.get_disconnected_nodes_ptr_in_heap local.get_disconnected_nodes_pure return_pure)
|
||||
qed
|
||||
next
|
||||
assume 0: "heap_is_wellformed h"
|
||||
and 1: "type_wf h"
|
||||
and 2: "known_ptrs h"
|
||||
and 3: "is_element_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr"
|
||||
and 4: "h \<turnstile> Heap_Error_Monad.bind (check_in_heap ptr) (\<lambda>_. (local.a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r \<circ> the \<circ> cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r) ptr ()) \<rightarrow>\<^sub>r owner_document"
|
||||
then obtain root where
|
||||
root: "h \<turnstile> get_root_node ptr \<rightarrow>\<^sub>r root"
|
||||
by(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 split: option.splits)
|
||||
|
||||
then show ?thesis
|
||||
proof (cases "is_document_ptr root")
|
||||
case True
|
||||
then show ?thesis
|
||||
using 3 4 root
|
||||
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!: filter_M_pure_I bind_pure_I split: option.splits)[1]
|
||||
apply(drule(1) returns_result_eq) apply(auto)[1]
|
||||
using "0" "1" "2" document_ptr_kinds_commutes local.get_root_node_root_in_heap by blast
|
||||
next
|
||||
case False
|
||||
have "known_ptr root"
|
||||
using "0" "1" "2" local.get_root_node_root_in_heap local.known_ptrs_known_ptr root by blast
|
||||
have "root |\<in>| object_ptr_kinds h"
|
||||
using root
|
||||
using "0" "1" "2" local.get_root_node_root_in_heap
|
||||
by blast
|
||||
then have "is_node_ptr_kind root"
|
||||
using False \<open>known_ptr root\<close>
|
||||
apply(simp add: known_ptr_impl known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs)
|
||||
using is_node_ptr_kind_none by force
|
||||
then
|
||||
have "(\<exists>document_ptr \<in> fset (document_ptr_kinds h). root \<in> cast ` set |h \<turnstile> get_disconnected_nodes document_ptr|\<^sub>r)"
|
||||
by (metis (no_types, lifting) "0" "1" "2" \<open>root |\<in>| object_ptr_kinds h\<close> local.child_parent_dual local.get_child_nodes_ok local.get_root_node_same_no_parent local.heap_is_wellformed_children_disc_nodes local.known_ptrs_known_ptr node_ptr_casts_commute3 node_ptr_inclusion node_ptr_kinds_commutes notin_fset option.distinct(1) returns_result_eq returns_result_select_result root)
|
||||
then obtain some_owner_document where
|
||||
"some_owner_document |\<in>| document_ptr_kinds h" and
|
||||
"root \<in> cast ` set |h \<turnstile> get_disconnected_nodes some_owner_document|\<^sub>r"
|
||||
by auto
|
||||
then
|
||||
obtain candidates where
|
||||
candidates: "h \<turnstile> filter_M
|
||||
(\<lambda>document_ptr.
|
||||
Heap_Error_Monad.bind (get_disconnected_nodes document_ptr)
|
||||
(\<lambda>disconnected_nodes. return (root \<in> 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 ` set disconnected_nodes)))
|
||||
(sorted_list_of_set (fset (document_ptr_kinds h)))
|
||||
\<rightarrow>\<^sub>r candidates"
|
||||
by (metis (no_types, lifting) "1" bind_is_OK_I2 bind_pure_I filter_M_is_OK_I finite_fset is_OK_returns_result_E local.get_disconnected_nodes_ok local.get_disconnected_nodes_pure notin_fset return_ok return_pure sorted_list_of_set(1))
|
||||
then have "some_owner_document \<in> set candidates"
|
||||
apply(rule filter_M_in_result_if_ok)
|
||||
using \<open>some_owner_document |\<in>| document_ptr_kinds h\<close> \<open>root \<in> cast ` set |h \<turnstile> get_disconnected_nodes some_owner_document|\<^sub>r\<close>
|
||||
apply(auto intro!: bind_pure_I bind_pure_returns_result_I)
|
||||
by (simp add: "1" local.get_disconnected_nodes_ok)
|
||||
|
||||
then have "candidates \<noteq> []"
|
||||
by auto
|
||||
then have "owner_document \<in> set candidates"
|
||||
using 4 root 3
|
||||
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!: filter_M_pure_I bind_pure_I split: option.splits)[1]
|
||||
apply (metis candidates list.set_sel(1) returns_result_eq)
|
||||
by (metis \<open>is_node_ptr_kind root\<close> node_ptr_no_document_ptr_cast returns_result_eq)
|
||||
|
||||
then show ?thesis
|
||||
using candidates
|
||||
by (meson bind_pure_I bind_returns_result_E2 filter_M_holds_for_result is_OK_returns_result_I local.get_disconnected_nodes_ptr_in_heap local.get_disconnected_nodes_pure return_pure)
|
||||
qed
|
||||
qed
|
||||
end
|
||||
|
||||
locale l_get_owner_document_wf = l_heap_is_wellformed_defs + l_type_wf + l_known_ptrs
|
||||
|
|
@ -2663,32 +2805,28 @@ locale l_get_owner_document_wf = l_heap_is_wellformed_defs + l_type_wf + l_known
|
|||
known_ptrs h \<Longrightarrow>
|
||||
type_wf h\<Longrightarrow>
|
||||
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"
|
||||
|
||||
|
||||
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
|
||||
using known_ptrs_is_l_known_ptrs
|
||||
using heap_is_wellformed_is_l_heap_is_wellformed
|
||||
using get_root_node_is_l_get_root_node
|
||||
using get_ancestors_is_l_get_ancestors
|
||||
using get_ancestors_wf_is_l_get_ancestors_wf
|
||||
using get_parent_is_l_get_parent
|
||||
using get_ancestors_wf_is_l_get_ancestors_wf
|
||||
using get_parent_wf_is_l_get_parent_wf
|
||||
using l_get_owner_document\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms
|
||||
by(simp add: l_get_owner_document_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def)
|
||||
|
||||
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)
|
||||
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"
|
||||
using known_ptrs_is_l_known_ptrs
|
||||
apply(simp add: l_get_owner_document_wf_def l_get_owner_document_wf_axioms_def)
|
||||
using get_owner_document_disconnected_nodes in_disconnected_nodes_no_parent
|
||||
by fast
|
||||
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
|
||||
done
|
||||
|
||||
|
||||
subsection \<open>Preserving heap-wellformedness\<close>
|
||||
|
|
@ -3631,6 +3769,7 @@ subsection \<open>adopt\_node\<close>
|
|||
locale l_adopt_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
|
||||
l_adopt_node\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
|
||||
l_get_parent_wf +
|
||||
l_get_owner_document_wf +
|
||||
l_remove_child_wf2 +
|
||||
l_heap_is_wellformed
|
||||
begin
|
||||
|
|
@ -3665,6 +3804,65 @@ proof -
|
|||
dest!: reads_writes_separate_forwards[OF get_child_nodes_reads set_disconnected_nodes_writes]
|
||||
split: if_splits)
|
||||
qed
|
||||
|
||||
|
||||
lemma adopt_node_document_in_heap:
|
||||
assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
|
||||
assumes "h \<turnstile> ok (adopt_node owner_document node)"
|
||||
shows "owner_document |\<in>| document_ptr_kinds h"
|
||||
proof -
|
||||
obtain old_document parent_opt h2 h' where
|
||||
old_document: "h \<turnstile> get_owner_document (cast node) \<rightarrow>\<^sub>r old_document" and
|
||||
parent_opt: "h \<turnstile> get_parent node \<rightarrow>\<^sub>r parent_opt" and
|
||||
h2: "h \<turnstile> (case parent_opt of Some parent \<Rightarrow> do { remove_child parent node } | None \<Rightarrow> do { return ()}) \<rightarrow>\<^sub>h h2"
|
||||
and
|
||||
h': "h2 \<turnstile> (if owner_document \<noteq> old_document then do {
|
||||
old_disc_nodes \<leftarrow> get_disconnected_nodes old_document;
|
||||
set_disconnected_nodes old_document (remove1 node old_disc_nodes);
|
||||
disc_nodes \<leftarrow> get_disconnected_nodes owner_document;
|
||||
set_disconnected_nodes owner_document (node # disc_nodes)
|
||||
} else do { return () }) \<rightarrow>\<^sub>h h'"
|
||||
using assms(4)
|
||||
by(auto simp add: adopt_node_def
|
||||
elim!: bind_returns_heap_E
|
||||
dest!: pure_returns_heap_eq[rotated, OF get_owner_document_pure]
|
||||
pure_returns_heap_eq[rotated, OF get_parent_pure])
|
||||
show ?thesis
|
||||
proof (cases "owner_document = old_document")
|
||||
case True
|
||||
then show ?thesis
|
||||
using old_document get_owner_document_owner_document_in_heap assms(1) assms(2) assms(3)
|
||||
by auto
|
||||
next
|
||||
case False
|
||||
|
||||
then obtain h3 old_disc_nodes disc_nodes where
|
||||
old_disc_nodes: "h2 \<turnstile> get_disconnected_nodes old_document \<rightarrow>\<^sub>r old_disc_nodes" and
|
||||
h3: "h2 \<turnstile> set_disconnected_nodes old_document (remove1 node old_disc_nodes) \<rightarrow>\<^sub>h h3" and
|
||||
old_disc_nodes: "h3 \<turnstile> get_disconnected_nodes owner_document \<rightarrow>\<^sub>r disc_nodes" and
|
||||
h': "h3 \<turnstile> set_disconnected_nodes owner_document (node # disc_nodes) \<rightarrow>\<^sub>h h'"
|
||||
using h'
|
||||
by(auto elim!: bind_returns_heap_E
|
||||
bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated] )
|
||||
then have "owner_document |\<in>| document_ptr_kinds h3"
|
||||
by (meson is_OK_returns_result_I local.get_disconnected_nodes_ptr_in_heap)
|
||||
|
||||
moreover have "object_ptr_kinds h = object_ptr_kinds h2"
|
||||
using h2 apply(simp split: option.splits)
|
||||
apply(rule writes_small_big[where P="\<lambda>h h'. object_ptr_kinds h = object_ptr_kinds h'",
|
||||
OF remove_child_writes])
|
||||
using remove_child_pointers_preserved
|
||||
by (auto simp add: reflp_def transp_def)
|
||||
moreover have "object_ptr_kinds h2 = object_ptr_kinds h3"
|
||||
apply(rule writes_small_big[where P="\<lambda>h h'. object_ptr_kinds h = object_ptr_kinds h'",
|
||||
OF set_disconnected_nodes_writes h3])
|
||||
using set_disconnected_nodes_pointers_preserved set_child_nodes_pointers_preserved
|
||||
by (auto simp add: reflp_def transp_def)
|
||||
|
||||
ultimately show ?thesis
|
||||
by(auto simp add: document_ptr_kinds_def)
|
||||
qed
|
||||
qed
|
||||
end
|
||||
|
||||
locale l_adopt_node_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
|
||||
|
|
@ -4343,6 +4541,9 @@ locale l_adopt_node_wf = l_heap_is_wellformed + l_known_ptrs + l_type_wf + l_ado
|
|||
\<Longrightarrow> h \<turnstile> adopt_node owner_document node \<rightarrow>\<^sub>h h'
|
||||
\<Longrightarrow> h \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r node # children
|
||||
\<Longrightarrow> h' \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children"
|
||||
assumes adopt_node_document_in_heap: "heap_is_wellformed h \<Longrightarrow> known_ptrs h \<Longrightarrow> type_wf h
|
||||
\<Longrightarrow> h \<turnstile> ok (adopt_node owner_document node)
|
||||
\<Longrightarrow> owner_document |\<in>| document_ptr_kinds h"
|
||||
|
||||
lemma adopt_node_wf_is_l_adopt_node_wf [instances]:
|
||||
"l_adopt_node_wf type_wf known_ptr heap_is_wellformed parent_child_rel get_child_nodes
|
||||
|
|
@ -4353,6 +4554,7 @@ lemma adopt_node_wf_is_l_adopt_node_wf [instances]:
|
|||
using adopt_node_removes_child apply blast
|
||||
using adopt_node_node_in_disconnected_nodes apply blast
|
||||
using adopt_node_removes_first_child apply blast
|
||||
using adopt_node_document_in_heap apply blast
|
||||
done
|
||||
|
||||
|
||||
|
|
@ -5110,7 +5312,7 @@ locale l_create_element_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub
|
|||
l_set_tag_type_get_disconnected_nodes type_wf set_tag_type set_tag_type_locs
|
||||
get_disconnected_nodes get_disconnected_nodes_locs +
|
||||
l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes
|
||||
set_disconnected_nodes_locs set_tag_type set_tag_type_locs create_element +
|
||||
set_disconnected_nodes_locs set_tag_type set_tag_type_locs type_wf create_element +
|
||||
l_new_element_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs +
|
||||
l_set_tag_type_get_child_nodes type_wf set_tag_type set_tag_type_locs known_ptr
|
||||
get_child_nodes get_child_nodes_locs +
|
||||
|
|
@ -5516,7 +5718,7 @@ locale l_create_character_data_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>
|
|||
type_wf set_val set_val_locs get_disconnected_nodes get_disconnected_nodes_locs
|
||||
+ l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
|
||||
set_val set_val_locs get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes
|
||||
set_disconnected_nodes_locs create_character_data
|
||||
set_disconnected_nodes_locs type_wf create_character_data
|
||||
+ l_new_character_data_get_child_nodes
|
||||
type_wf known_ptr get_child_nodes get_child_nodes_locs
|
||||
+ l_set_val_get_child_nodes
|
||||
|
|
|
|||
Reference in New Issue