forked from afp-mirror/Core_DOM
Added a few new lemmas.
This commit is contained in:
parent
874251f8c1
commit
d90812beed
|
@ -2358,6 +2358,15 @@ proof -
|
||||||
using assms(1) get_child_nodes_ptr_in_heap by blast
|
using assms(1) get_child_nodes_ptr_in_heap by blast
|
||||||
qed
|
qed
|
||||||
|
|
||||||
|
|
||||||
|
lemma remove_child_child_in_heap:
|
||||||
|
assumes "h \<turnstile> remove_child ptr' child \<rightarrow>\<^sub>h h'"
|
||||||
|
shows "child |\<in>| node_ptr_kinds h"
|
||||||
|
using assms
|
||||||
|
apply(auto simp add: remove_child_def elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_child_nodes_pure, rotated] split: if_splits)
|
||||||
|
by (meson is_OK_returns_result_I local.get_owner_document_ptr_in_heap node_ptr_kinds_commutes)
|
||||||
|
|
||||||
|
|
||||||
lemma remove_child_in_disconnected_nodes:
|
lemma remove_child_in_disconnected_nodes:
|
||||||
(* assumes "known_ptrs h" *)
|
(* assumes "known_ptrs h" *)
|
||||||
assumes "h \<turnstile> remove_child ptr child \<rightarrow>\<^sub>h h'"
|
assumes "h \<turnstile> remove_child ptr child \<rightarrow>\<^sub>h h'"
|
||||||
|
@ -2490,6 +2499,7 @@ locale l_remove_child = l_type_wf + l_known_ptrs + l_remove_child_defs + l_get_o
|
||||||
\<Longrightarrow> h' \<turnstile> get_disconnected_nodes owner_document \<rightarrow>\<^sub>r disc_nodes
|
\<Longrightarrow> h' \<turnstile> get_disconnected_nodes owner_document \<rightarrow>\<^sub>r disc_nodes
|
||||||
\<Longrightarrow> child \<in> set disc_nodes"
|
\<Longrightarrow> child \<in> set disc_nodes"
|
||||||
assumes remove_child_ptr_in_heap: "h \<turnstile> ok (remove_child ptr child) \<Longrightarrow> ptr |\<in>| object_ptr_kinds h"
|
assumes remove_child_ptr_in_heap: "h \<turnstile> ok (remove_child ptr child) \<Longrightarrow> ptr |\<in>| object_ptr_kinds h"
|
||||||
|
assumes remove_child_child_in_heap: "h \<turnstile> remove_child ptr' child \<rightarrow>\<^sub>h h' \<Longrightarrow> child |\<in>| node_ptr_kinds h"
|
||||||
assumes remove_child_children_subset:
|
assumes remove_child_children_subset:
|
||||||
"known_ptrs h \<Longrightarrow> type_wf h \<Longrightarrow> h \<turnstile> remove_child parent child \<rightarrow>\<^sub>h h'
|
"known_ptrs h \<Longrightarrow> type_wf h \<Longrightarrow> h \<turnstile> remove_child parent child \<rightarrow>\<^sub>h h'
|
||||||
\<Longrightarrow> h \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children
|
\<Longrightarrow> h \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children
|
||||||
|
@ -2535,6 +2545,7 @@ lemma remove_child_is_l_remove_child [instances]:
|
||||||
using remove_child_types_preserved apply(blast)
|
using remove_child_types_preserved apply(blast)
|
||||||
using remove_child_in_disconnected_nodes apply(blast)
|
using remove_child_in_disconnected_nodes apply(blast)
|
||||||
using remove_child_ptr_in_heap apply(blast)
|
using remove_child_ptr_in_heap apply(blast)
|
||||||
|
using remove_child_child_in_heap apply(blast)
|
||||||
using remove_child_children_subset apply(blast)
|
using remove_child_children_subset apply(blast)
|
||||||
done
|
done
|
||||||
|
|
||||||
|
@ -3012,6 +3023,13 @@ proof -
|
||||||
unfolding insert_before_def by auto
|
unfolding insert_before_def by auto
|
||||||
qed
|
qed
|
||||||
|
|
||||||
|
lemma insert_before_ptr_in_heap:
|
||||||
|
assumes "h \<turnstile> ok (insert_before ptr node reference_child)"
|
||||||
|
shows "ptr |\<in>| object_ptr_kinds h"
|
||||||
|
using assms
|
||||||
|
apply(auto simp add: insert_before_def elim!: bind_is_OK_E)
|
||||||
|
by (metis (mono_tags, lifting) ensure_pre_insertion_validity_pure is_OK_returns_result_I local.get_owner_document_ptr_in_heap next_sibling_pure pure_returns_heap_eq return_returns_heap)
|
||||||
|
|
||||||
lemma insert_before_child_in_heap:
|
lemma insert_before_child_in_heap:
|
||||||
assumes "h \<turnstile> ok (insert_before ptr node reference_child)"
|
assumes "h \<turnstile> ok (insert_before ptr node reference_child)"
|
||||||
shows "node |\<in>| node_ptr_kinds h"
|
shows "node |\<in>| node_ptr_kinds h"
|
||||||
|
@ -3166,10 +3184,21 @@ 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 =
|
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_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs set_tag_type set_tag_type_locs +
|
||||||
l_get_disconnected_nodes +
|
l_get_disconnected_nodes type_wf get_disconnected_nodes get_disconnected_nodes_locs +
|
||||||
l_set_tag_type +
|
l_set_tag_type type_wf set_tag_type set_tag_type_locs +
|
||||||
l_create_element_defs +
|
l_create_element_defs create_element +
|
||||||
|
l_known_ptr known_ptr
|
||||||
|
for get_disconnected_nodes :: "(_) document_ptr \<Rightarrow> ((_) heap, exception, (_) node_ptr list) prog"
|
||||||
|
and get_disconnected_nodes_locs :: "(_) document_ptr \<Rightarrow> ((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
|
||||||
|
and set_disconnected_nodes :: "(_) document_ptr \<Rightarrow> (_) node_ptr list \<Rightarrow> ((_) heap, exception, unit) prog"
|
||||||
|
and set_disconnected_nodes_locs :: "(_) document_ptr \<Rightarrow> ((_) heap, exception, unit) prog set"
|
||||||
|
and set_tag_type :: "(_) element_ptr \<Rightarrow> char list \<Rightarrow> ((_) heap, exception, unit) prog"
|
||||||
|
and set_tag_type_locs :: "(_) element_ptr \<Rightarrow> ((_) heap, exception, unit) prog set"
|
||||||
|
and type_wf :: "(_) heap \<Rightarrow> bool"
|
||||||
|
and create_element :: "(_) document_ptr \<Rightarrow> char list \<Rightarrow> ((_) heap, exception, (_) element_ptr) prog"
|
||||||
|
and known_ptr :: "(_) object_ptr \<Rightarrow> bool" +
|
||||||
|
assumes known_ptr_impl: "known_ptr = a_known_ptr"
|
||||||
assumes create_element_impl: "create_element = a_create_element"
|
assumes create_element_impl: "create_element = a_create_element"
|
||||||
begin
|
begin
|
||||||
lemmas create_element_def = a_create_element_def[folded create_element_impl]
|
lemmas create_element_def = a_create_element_def[folded create_element_impl]
|
||||||
|
@ -3205,12 +3234,25 @@ proof -
|
||||||
ultimately show ?thesis
|
ultimately show ?thesis
|
||||||
by (auto simp add: document_ptr_kinds_def)
|
by (auto simp add: document_ptr_kinds_def)
|
||||||
qed
|
qed
|
||||||
|
|
||||||
|
lemma create_element_known_ptr:
|
||||||
|
assumes "h \<turnstile> create_element document_ptr tag \<rightarrow>\<^sub>r new_element_ptr"
|
||||||
|
shows "known_ptr (cast new_element_ptr)"
|
||||||
|
proof -
|
||||||
|
have "is_element_ptr new_element_ptr"
|
||||||
|
using assms
|
||||||
|
apply(auto simp add: create_element_def elim!: bind_returns_result_E)
|
||||||
|
using new_element_is_element_ptr
|
||||||
|
by blast
|
||||||
|
then show ?thesis
|
||||||
|
by(auto simp add: known_ptr_impl DocumentClass.known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs)
|
||||||
|
qed
|
||||||
end
|
end
|
||||||
|
|
||||||
locale l_create_element = l_create_element_defs
|
locale l_create_element = l_create_element_defs
|
||||||
|
|
||||||
interpretation
|
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 type_wf create_element
|
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 known_ptr
|
||||||
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)
|
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]
|
declare l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms[instances]
|
||||||
|
|
||||||
|
|
|
@ -2623,7 +2623,6 @@ proof -
|
||||||
by (metis (no_types, hide_lams))
|
by (metis (no_types, hide_lams))
|
||||||
moreover have "node_ptr |\<in>| node_ptr_kinds h"
|
moreover have "node_ptr |\<in>| node_ptr_kinds h"
|
||||||
using assms(2) get_parent_ptr_in_heap by blast
|
using assms(2) get_parent_ptr_in_heap by blast
|
||||||
thm heap_is_wellformed_children_disc_nodes_different
|
|
||||||
ultimately
|
ultimately
|
||||||
have 0: "\<exists>document_ptr\<in>set |h \<turnstile> document_ptr_kinds_M|\<^sub>r. node_ptr \<in> set |h \<turnstile> get_disconnected_nodes document_ptr|\<^sub>r"
|
have 0: "\<exists>document_ptr\<in>set |h \<turnstile> document_ptr_kinds_M|\<^sub>r. node_ptr \<in> set |h \<turnstile> get_disconnected_nodes document_ptr|\<^sub>r"
|
||||||
by (metis DocumentMonad.ptr_kinds_ptr_kinds_M assms(1) finite_set_in heap_is_wellformed_children_disc_nodes)
|
by (metis DocumentMonad.ptr_kinds_ptr_kinds_M assms(1) finite_set_in heap_is_wellformed_children_disc_nodes)
|
||||||
|
@ -2785,6 +2784,7 @@ next
|
||||||
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)
|
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
|
||||||
qed
|
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
|
||||||
|
@ -2829,8 +2829,86 @@ lemma get_owner_document_wf_is_l_get_owner_document_wf [instances]:
|
||||||
done
|
done
|
||||||
|
|
||||||
|
|
||||||
subsection \<open>Preserving heap-wellformedness\<close>
|
subsubsection \<open>get\_root\_node\<close>
|
||||||
|
|
||||||
|
locale l_get_owner_document_wf_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
|
||||||
|
l_get_root_node\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
|
||||||
|
l_get_root_node_wf +
|
||||||
|
l_get_owner_document\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
|
||||||
|
l_get_owner_document_wf
|
||||||
|
begin
|
||||||
|
|
||||||
|
lemma get_root_node_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"
|
||||||
|
assumes "is_document_ptr_kind root"
|
||||||
|
shows "h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r the (cast root)"
|
||||||
|
proof -
|
||||||
|
have "ptr |\<in>| object_ptr_kinds h"
|
||||||
|
using assms(4)
|
||||||
|
by (meson is_OK_returns_result_I local.get_root_node_ptr_in_heap)
|
||||||
|
then have "known_ptr ptr"
|
||||||
|
using assms(3) local.known_ptrs_known_ptr by blast
|
||||||
|
{
|
||||||
|
assume "is_document_ptr_kind ptr"
|
||||||
|
then have "ptr = root"
|
||||||
|
using assms(4)
|
||||||
|
by(auto simp add: get_root_node_def get_ancestors_def elim!: bind_returns_result_E2 split: option.splits)
|
||||||
|
then have ?thesis
|
||||||
|
using \<open>is_document_ptr_kind ptr\<close> \<open>known_ptr ptr\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close>
|
||||||
|
apply(auto simp add: known_ptr_impl get_owner_document_def a_get_owner_document_tups_def)
|
||||||
|
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)
|
||||||
|
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 intro!: bind_pure_returns_result_I split: option.splits)
|
||||||
|
}
|
||||||
|
moreover
|
||||||
|
{
|
||||||
|
assume "is_node_ptr_kind ptr"
|
||||||
|
then have ?thesis
|
||||||
|
using \<open>known_ptr ptr\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close>
|
||||||
|
apply(auto simp add: known_ptr_impl get_owner_document_def a_get_owner_document_tups_def)
|
||||||
|
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)
|
||||||
|
apply(auto split: option.splits)[1]
|
||||||
|
using \<open>h \<turnstile> get_root_node ptr \<rightarrow>\<^sub>r root\<close> assms(5)
|
||||||
|
by(auto simp add: a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def is_document_ptr_kind_def intro!: bind_pure_returns_result_I split: option.splits)[2]
|
||||||
|
}
|
||||||
|
ultimately
|
||||||
|
show ?thesis
|
||||||
|
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)
|
||||||
|
qed
|
||||||
|
|
||||||
|
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
|
||||||
|
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
|
||||||
|
by(auto simp add: l_get_owner_document_wf_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
|
||||||
|
declare l_get_owner_document_wf_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]
|
||||||
|
|
||||||
|
locale l_get_owner_document_wf_get_root_node_wf = l_heap_is_wellformed_defs + l_type_wf + l_known_ptrs + l_get_root_node_defs + l_get_owner_document_defs +
|
||||||
|
assumes get_root_node_document: "heap_is_wellformed h \<Longrightarrow> type_wf h \<Longrightarrow> known_ptrs h \<Longrightarrow> h \<turnstile> get_root_node ptr \<rightarrow>\<^sub>r root \<Longrightarrow> is_document_ptr_kind root \<Longrightarrow> h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r the (cast root)"
|
||||||
|
assumes get_root_node_same_owner_document: "heap_is_wellformed h \<Longrightarrow> type_wf h \<Longrightarrow> known_ptrs h \<Longrightarrow> h \<turnstile> get_root_node ptr \<rightarrow>\<^sub>r root \<Longrightarrow> h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document \<longleftrightarrow> h \<turnstile> get_owner_document root \<rightarrow>\<^sub>r owner_document"
|
||||||
|
|
||||||
|
lemma get_owner_document_wf_get_root_node_wf_is_l_get_owner_document_wf_get_root_node_wf [instances]:
|
||||||
|
"l_get_owner_document_wf_get_root_node_wf heap_is_wellformed type_wf known_ptr known_ptrs get_root_node get_owner_document"
|
||||||
|
apply(auto simp add: l_get_owner_document_wf_get_root_node_wf_def l_get_owner_document_wf_get_root_node_wf_axioms_def instances)
|
||||||
|
using get_root_node_document apply blast
|
||||||
|
using get_root_node_same_owner_document apply (blast, blast)
|
||||||
|
done
|
||||||
|
|
||||||
|
|
||||||
|
subsection \<open>Preserving heap-wellformedness\<close>
|
||||||
|
|
||||||
subsection \<open>set\_attribute\<close>
|
subsection \<open>set\_attribute\<close>
|
||||||
|
|
||||||
|
@ -5356,7 +5434,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
|
l_set_tag_type_get_disconnected_nodes type_wf set_tag_type set_tag_type_locs
|
||||||
get_disconnected_nodes get_disconnected_nodes_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
|
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 +
|
set_disconnected_nodes_locs set_tag_type set_tag_type_locs type_wf create_element known_ptr +
|
||||||
l_new_element_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs +
|
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
|
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 +
|
get_child_nodes get_child_nodes_locs +
|
||||||
|
@ -5387,7 +5465,7 @@ lemma create_element_preserves_wellformedness:
|
||||||
and "h \<turnstile> create_element document_ptr tag \<rightarrow>\<^sub>h h'"
|
and "h \<turnstile> create_element document_ptr tag \<rightarrow>\<^sub>h h'"
|
||||||
and "type_wf h"
|
and "type_wf h"
|
||||||
and "known_ptrs h"
|
and "known_ptrs h"
|
||||||
shows "heap_is_wellformed h'"
|
shows "heap_is_wellformed h'" and "type_wf h'" and "known_ptrs h'"
|
||||||
proof -
|
proof -
|
||||||
obtain new_element_ptr h2 h3 disc_nodes_h3 where
|
obtain new_element_ptr h2 h3 disc_nodes_h3 where
|
||||||
new_element_ptr: "h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr" and
|
new_element_ptr: "h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr" and
|
||||||
|
@ -5399,6 +5477,11 @@ proof -
|
||||||
by(auto simp add: create_element_def
|
by(auto simp add: create_element_def
|
||||||
elim!: bind_returns_heap_E
|
elim!: bind_returns_heap_E
|
||||||
bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated] )
|
bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated] )
|
||||||
|
then have "h \<turnstile> create_element document_ptr tag \<rightarrow>\<^sub>r new_element_ptr"
|
||||||
|
apply(auto simp add: create_element_def intro!: bind_returns_result_I)
|
||||||
|
apply (metis is_OK_returns_heap_I is_OK_returns_result_E old.unit.exhaust)
|
||||||
|
apply (metis is_OK_returns_heap_E is_OK_returns_result_I local.get_disconnected_nodes_pure pure_returns_heap_eq)
|
||||||
|
by (metis is_OK_returns_heap_I is_OK_returns_result_E old.unit.exhaust)
|
||||||
|
|
||||||
have "new_element_ptr \<notin> set |h \<turnstile> element_ptr_kinds_M|\<^sub>r"
|
have "new_element_ptr \<notin> set |h \<turnstile> element_ptr_kinds_M|\<^sub>r"
|
||||||
using new_element_ptr ElementMonad.ptr_kinds_ptr_kinds_M h2
|
using new_element_ptr ElementMonad.ptr_kinds_ptr_kinds_M h2
|
||||||
|
@ -5444,6 +5527,19 @@ proof -
|
||||||
using object_ptr_kinds_eq_h3
|
using object_ptr_kinds_eq_h3
|
||||||
by(auto simp add: node_ptr_kinds_def)
|
by(auto simp add: node_ptr_kinds_def)
|
||||||
|
|
||||||
|
have "known_ptr (cast new_element_ptr)"
|
||||||
|
using \<open>h \<turnstile> create_element document_ptr tag \<rightarrow>\<^sub>r new_element_ptr\<close> local.create_element_known_ptr by blast
|
||||||
|
then
|
||||||
|
have "known_ptrs h2"
|
||||||
|
using known_ptrs_new_ptr object_ptr_kinds_eq_h \<open>known_ptrs h\<close> h2
|
||||||
|
by blast
|
||||||
|
then
|
||||||
|
have "known_ptrs h3"
|
||||||
|
using known_ptrs_preserved object_ptr_kinds_eq_h2 by blast
|
||||||
|
then
|
||||||
|
show "known_ptrs h'"
|
||||||
|
using known_ptrs_preserved object_ptr_kinds_eq_h3 by blast
|
||||||
|
|
||||||
|
|
||||||
have "document_ptr |\<in>| document_ptr_kinds h"
|
have "document_ptr |\<in>| document_ptr_kinds h"
|
||||||
using disc_nodes_h3 document_ptr_kinds_eq_h object_ptr_kinds_eq_h2
|
using disc_nodes_h3 document_ptr_kinds_eq_h object_ptr_kinds_eq_h2
|
||||||
|
@ -5496,7 +5592,7 @@ proof -
|
||||||
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF set_tag_type_writes h3]
|
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF set_tag_type_writes h3]
|
||||||
using set_tag_type_types_preserved
|
using set_tag_type_types_preserved
|
||||||
by(auto simp add: reflp_def transp_def)
|
by(auto simp add: reflp_def transp_def)
|
||||||
then have "type_wf h'"
|
then show "type_wf h'"
|
||||||
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF set_disconnected_nodes_writes h']
|
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF set_disconnected_nodes_writes h']
|
||||||
using set_disconnected_nodes_types_preserved
|
using set_disconnected_nodes_types_preserved
|
||||||
by(auto simp add: reflp_def transp_def)
|
by(auto simp add: reflp_def transp_def)
|
||||||
|
|
|
@ -336,12 +336,14 @@ lemma known_ptrs_preserved:
|
||||||
lemma known_ptrs_subset:
|
lemma known_ptrs_subset:
|
||||||
"object_ptr_kinds h' |\<subseteq>| object_ptr_kinds h \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
"object_ptr_kinds h' |\<subseteq>| object_ptr_kinds h \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
||||||
by(auto simp add: a_known_ptrs_def)
|
by(auto simp add: a_known_ptrs_def)
|
||||||
|
lemma known_ptrs_new_ptr: "object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|new_ptr|} \<Longrightarrow> known_ptr new_ptr \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
||||||
|
by(simp add: a_known_ptrs_def)
|
||||||
end
|
end
|
||||||
global_interpretation l_known_ptrs\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a known_ptr defines known_ptrs = a_known_ptrs .
|
global_interpretation l_known_ptrs\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a known_ptr defines known_ptrs = a_known_ptrs .
|
||||||
lemmas known_ptrs_defs = a_known_ptrs_def
|
lemmas known_ptrs_defs = a_known_ptrs_def
|
||||||
|
|
||||||
lemma known_ptrs_is_l_known_ptrs: "l_known_ptrs known_ptr known_ptrs"
|
lemma known_ptrs_is_l_known_ptrs: "l_known_ptrs known_ptr known_ptrs"
|
||||||
using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset
|
using known_ptrs_known_ptr known_ptrs_preserved known_ptrs_subset known_ptrs_new_ptr l_known_ptrs_def
|
||||||
by blast
|
by blast
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
|
@ -326,11 +326,14 @@ lemma known_ptrs_preserved:
|
||||||
lemma known_ptrs_subset:
|
lemma known_ptrs_subset:
|
||||||
"object_ptr_kinds h' |\<subseteq>| object_ptr_kinds h \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
"object_ptr_kinds h' |\<subseteq>| object_ptr_kinds h \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
||||||
by(auto simp add: a_known_ptrs_def)
|
by(auto simp add: a_known_ptrs_def)
|
||||||
|
lemma known_ptrs_new_ptr: "object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|new_ptr|} \<Longrightarrow> known_ptr new_ptr \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
||||||
|
by(simp add: a_known_ptrs_def)
|
||||||
end
|
end
|
||||||
global_interpretation l_known_ptrs\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t known_ptr defines known_ptrs = a_known_ptrs .
|
global_interpretation l_known_ptrs\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t known_ptr defines known_ptrs = a_known_ptrs .
|
||||||
lemmas known_ptrs_defs = a_known_ptrs_def
|
lemmas known_ptrs_defs = a_known_ptrs_def
|
||||||
|
|
||||||
lemma known_ptrs_is_l_known_ptrs [instances]: "l_known_ptrs known_ptr known_ptrs"
|
lemma known_ptrs_is_l_known_ptrs [instances]: "l_known_ptrs known_ptr known_ptrs"
|
||||||
using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset by blast
|
using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset known_ptrs_new_ptr
|
||||||
|
by blast
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
|
@ -273,7 +273,6 @@ lemma new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_get\<^sub>E\<^
|
||||||
using assms
|
using assms
|
||||||
by(auto simp add: new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def)
|
by(auto simp add: new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def)
|
||||||
|
|
||||||
|
|
||||||
locale l_known_ptr\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t
|
locale l_known_ptr\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t
|
||||||
begin
|
begin
|
||||||
definition a_known_ptr :: "(_) object_ptr \<Rightarrow> bool"
|
definition a_known_ptr :: "(_) object_ptr \<Rightarrow> bool"
|
||||||
|
@ -301,11 +300,13 @@ lemma known_ptrs_preserved: "object_ptr_kinds h = object_ptr_kinds h' \<Longrigh
|
||||||
by(auto simp add: a_known_ptrs_def)
|
by(auto simp add: a_known_ptrs_def)
|
||||||
lemma known_ptrs_subset: "object_ptr_kinds h' |\<subseteq>| object_ptr_kinds h \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
lemma known_ptrs_subset: "object_ptr_kinds h' |\<subseteq>| object_ptr_kinds h \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
||||||
by(auto simp add: a_known_ptrs_def)
|
by(auto simp add: a_known_ptrs_def)
|
||||||
|
lemma known_ptrs_new_ptr: "object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|new_ptr|} \<Longrightarrow> known_ptr new_ptr \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
||||||
|
by(simp add: a_known_ptrs_def)
|
||||||
end
|
end
|
||||||
global_interpretation l_known_ptrs\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t known_ptr defines known_ptrs = a_known_ptrs .
|
global_interpretation l_known_ptrs\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t known_ptr defines known_ptrs = a_known_ptrs .
|
||||||
lemmas known_ptrs_defs = a_known_ptrs_def
|
lemmas known_ptrs_defs = a_known_ptrs_def
|
||||||
|
|
||||||
lemma known_ptrs_is_l_known_ptrs: "l_known_ptrs known_ptr known_ptrs"
|
lemma known_ptrs_is_l_known_ptrs: "l_known_ptrs known_ptr known_ptrs"
|
||||||
using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset by blast
|
using known_ptrs_known_ptr known_ptrs_preserved known_ptrs_subset known_ptrs_new_ptr l_known_ptrs_def by blast
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
|
@ -186,12 +186,15 @@ lemma known_ptrs_preserved: "object_ptr_kinds h = object_ptr_kinds h' \<Longrigh
|
||||||
by(auto simp add: a_known_ptrs_def)
|
by(auto simp add: a_known_ptrs_def)
|
||||||
lemma known_ptrs_subset: "object_ptr_kinds h' |\<subseteq>| object_ptr_kinds h \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
lemma known_ptrs_subset: "object_ptr_kinds h' |\<subseteq>| object_ptr_kinds h \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
||||||
by(auto simp add: a_known_ptrs_def)
|
by(auto simp add: a_known_ptrs_def)
|
||||||
|
lemma known_ptrs_new_ptr: "object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|new_ptr|} \<Longrightarrow> known_ptr new_ptr \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
||||||
|
by(simp add: a_known_ptrs_def)
|
||||||
end
|
end
|
||||||
global_interpretation l_known_ptrs\<^sub>N\<^sub>o\<^sub>d\<^sub>e known_ptr defines known_ptrs = a_known_ptrs .
|
global_interpretation l_known_ptrs\<^sub>N\<^sub>o\<^sub>d\<^sub>e known_ptr defines known_ptrs = a_known_ptrs .
|
||||||
lemmas known_ptrs_defs = a_known_ptrs_def
|
lemmas known_ptrs_defs = a_known_ptrs_def
|
||||||
|
|
||||||
lemma known_ptrs_is_l_known_ptrs: "l_known_ptrs known_ptr known_ptrs"
|
lemma known_ptrs_is_l_known_ptrs: "l_known_ptrs known_ptr known_ptrs"
|
||||||
using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset by blast
|
using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset known_ptrs_new_ptr
|
||||||
|
by blast
|
||||||
|
|
||||||
lemma get_node_ptr_simp1 [simp]: "get\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr (put\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr node h) = Some node"
|
lemma get_node_ptr_simp1 [simp]: "get\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr (put\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr node h) = Some node"
|
||||||
by(auto simp add: get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def)
|
by(auto simp add: get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def)
|
||||||
|
|
|
@ -128,6 +128,7 @@ locale l_known_ptrs = l_known_ptr known_ptr for known_ptr :: "(_) object_ptr \<R
|
||||||
assumes known_ptrs_known_ptr: "known_ptrs h \<Longrightarrow> ptr |\<in>| object_ptr_kinds h \<Longrightarrow> known_ptr ptr"
|
assumes known_ptrs_known_ptr: "known_ptrs h \<Longrightarrow> ptr |\<in>| object_ptr_kinds h \<Longrightarrow> known_ptr ptr"
|
||||||
assumes known_ptrs_preserved: "object_ptr_kinds h = object_ptr_kinds h' \<Longrightarrow> known_ptrs h = known_ptrs h'"
|
assumes known_ptrs_preserved: "object_ptr_kinds h = object_ptr_kinds h' \<Longrightarrow> known_ptrs h = known_ptrs h'"
|
||||||
assumes known_ptrs_subset: "object_ptr_kinds h' |\<subseteq>| object_ptr_kinds h \<Longrightarrow> known_ptrs h \<Longrightarrow> known_ptrs h'"
|
assumes known_ptrs_subset: "object_ptr_kinds h' |\<subseteq>| object_ptr_kinds h \<Longrightarrow> known_ptrs h \<Longrightarrow> known_ptrs h'"
|
||||||
|
assumes known_ptrs_new_ptr: "object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|new_ptr|} \<Longrightarrow> known_ptr new_ptr \<Longrightarrow> known_ptrs h \<Longrightarrow> known_ptrs h'"
|
||||||
|
|
||||||
locale l_known_ptrs\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t = l_known_ptr known_ptr for known_ptr :: "(_) object_ptr \<Rightarrow> bool"
|
locale l_known_ptrs\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t = l_known_ptr known_ptr for known_ptr :: "(_) object_ptr \<Rightarrow> bool"
|
||||||
begin
|
begin
|
||||||
|
@ -143,12 +144,15 @@ lemma known_ptrs_preserved: "object_ptr_kinds h = object_ptr_kinds h' \<Longrigh
|
||||||
by(auto simp add: a_known_ptrs_def)
|
by(auto simp add: a_known_ptrs_def)
|
||||||
lemma known_ptrs_subset: "object_ptr_kinds h' |\<subseteq>| object_ptr_kinds h \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
lemma known_ptrs_subset: "object_ptr_kinds h' |\<subseteq>| object_ptr_kinds h \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
||||||
by(auto simp add: a_known_ptrs_def)
|
by(auto simp add: a_known_ptrs_def)
|
||||||
|
lemma known_ptrs_new_ptr: "object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|new_ptr|} \<Longrightarrow> known_ptr new_ptr \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
||||||
|
by(simp add: a_known_ptrs_def)
|
||||||
end
|
end
|
||||||
global_interpretation l_known_ptrs\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t known_ptr defines known_ptrs = a_known_ptrs .
|
global_interpretation l_known_ptrs\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t known_ptr defines known_ptrs = a_known_ptrs .
|
||||||
lemmas known_ptrs_defs = a_known_ptrs_def
|
lemmas known_ptrs_defs = a_known_ptrs_def
|
||||||
|
|
||||||
lemma known_ptrs_is_l_known_ptrs: "l_known_ptrs known_ptr known_ptrs"
|
lemma known_ptrs_is_l_known_ptrs: "l_known_ptrs known_ptr known_ptrs"
|
||||||
using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset by blast
|
using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset known_ptrs_new_ptr
|
||||||
|
by blast
|
||||||
|
|
||||||
|
|
||||||
lemma get_object_ptr_simp1 [simp]: "get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr object h) = Some object"
|
lemma get_object_ptr_simp1 [simp]: "get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr object h) = Some object"
|
||||||
|
|
Reference in New Issue