forked from afp-mirror/Core_DOM
Added _thesis lemmas for thesis.
This commit is contained in:
Michael Herzberg
parent
6aa9154363
commit
633e5c76bb
|
|
@ -4270,6 +4270,13 @@ proof -
|
|||
qed
|
||||
qed
|
||||
|
||||
lemma adopt_node_removes_child_thesis:
|
||||
assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
|
||||
assumes "h \<turnstile> adopt_node owner_document node_ptr \<rightarrow>\<^sub>h h'"
|
||||
shows "\<And>ptr' children'.
|
||||
h' \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children' \<Longrightarrow> node_ptr \<notin> set children'"
|
||||
using adopt_node_removes_child assms by blast
|
||||
|
||||
lemma adopt_node_preserves_wellformedness:
|
||||
assumes "heap_is_wellformed h"
|
||||
and "h \<turnstile> adopt_node document_ptr child \<rightarrow>\<^sub>h h'"
|
||||
|
|
@ -4982,6 +4989,245 @@ locale l_insert_before_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub
|
|||
l_get_owner_document +
|
||||
l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
|
||||
begin
|
||||
|
||||
lemma insert_before_preserves_acyclitity_thesis:
|
||||
assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
|
||||
assumes "h \<turnstile> insert_before ptr node child \<rightarrow>\<^sub>h h'"
|
||||
shows "acyclic (parent_child_rel h')"
|
||||
proof -
|
||||
obtain ancestors reference_child owner_document h2 h3
|
||||
disconnected_nodes_h2
|
||||
where
|
||||
ancestors: "h \<turnstile> get_ancestors ptr \<rightarrow>\<^sub>r ancestors" and
|
||||
node_not_in_ancestors: "cast node \<notin> set ancestors" and
|
||||
reference_child:
|
||||
"h \<turnstile> (if Some node = child then a_next_sibling node
|
||||
else return child) \<rightarrow>\<^sub>r reference_child" and
|
||||
owner_document: "h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document" and
|
||||
h2: "h \<turnstile> adopt_node owner_document node \<rightarrow>\<^sub>h h2" and
|
||||
disconnected_nodes_h2: "h2 \<turnstile> get_disconnected_nodes owner_document
|
||||
\<rightarrow>\<^sub>r disconnected_nodes_h2" and
|
||||
h3: "h2 \<turnstile> set_disconnected_nodes owner_document
|
||||
(remove1 node disconnected_nodes_h2) \<rightarrow>\<^sub>h h3" and
|
||||
h': "h3 \<turnstile> a_insert_node ptr node reference_child \<rightarrow>\<^sub>h h'"
|
||||
using assms(4)
|
||||
by(auto simp add: insert_before_def a_ensure_pre_insertion_validity_def
|
||||
elim!: bind_returns_heap_E bind_returns_result_E
|
||||
bind_returns_heap_E2[rotated, OF get_parent_pure, rotated]
|
||||
bind_returns_heap_E2[rotated, OF get_child_nodes_pure, rotated]
|
||||
bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated]
|
||||
bind_returns_heap_E2[rotated, OF get_ancestors_pure, rotated]
|
||||
bind_returns_heap_E2[rotated, OF next_sibling_pure, rotated]
|
||||
bind_returns_heap_E2[rotated, OF get_owner_document_pure, rotated]
|
||||
split: if_splits option.splits)
|
||||
|
||||
have "known_ptr ptr"
|
||||
by (meson get_owner_document_ptr_in_heap is_OK_returns_result_I assms
|
||||
l_known_ptrs.known_ptrs_known_ptr l_known_ptrs_axioms owner_document)
|
||||
|
||||
have "type_wf h2"
|
||||
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF adopt_node_writes h2]
|
||||
using assms adopt_node_types_preserved
|
||||
by(auto simp add: a_remove_child_locs_def reflp_def transp_def)
|
||||
then have "type_wf h3"
|
||||
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF set_disconnected_nodes_writes h3]
|
||||
using set_disconnected_nodes_types_preserved
|
||||
by(auto simp add: reflp_def transp_def)
|
||||
then have "type_wf h'"
|
||||
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF insert_node_writes h']
|
||||
using set_child_nodes_types_preserved
|
||||
by(auto simp add: reflp_def transp_def)
|
||||
|
||||
have object_ptr_kinds_M_eq3_h: "object_ptr_kinds h = object_ptr_kinds h2"
|
||||
apply(rule writes_small_big[where P="\<lambda>h h'. object_ptr_kinds h = object_ptr_kinds h'",
|
||||
OF adopt_node_writes h2])
|
||||
using adopt_node_pointers_preserved
|
||||
apply blast
|
||||
by (auto simp add: reflp_def transp_def)
|
||||
then have object_ptr_kinds_M_eq_h: "\<And>ptrs. h \<turnstile> object_ptr_kinds_M \<rightarrow>\<^sub>r ptrs = h2 \<turnstile> object_ptr_kinds_M \<rightarrow>\<^sub>r ptrs"
|
||||
by(simp add: object_ptr_kinds_M_defs )
|
||||
then have object_ptr_kinds_M_eq2_h: "|h \<turnstile> object_ptr_kinds_M|\<^sub>r = |h2 \<turnstile> object_ptr_kinds_M|\<^sub>r"
|
||||
by simp
|
||||
then have node_ptr_kinds_eq2_h: "|h \<turnstile> node_ptr_kinds_M|\<^sub>r = |h2 \<turnstile> node_ptr_kinds_M|\<^sub>r"
|
||||
using node_ptr_kinds_M_eq by blast
|
||||
|
||||
have "known_ptrs h2"
|
||||
using assms object_ptr_kinds_M_eq3_h known_ptrs_preserved by blast
|
||||
|
||||
have wellformed_h2: "heap_is_wellformed h2"
|
||||
using adopt_node_preserves_wellformedness[OF assms(1) h2] assms by simp
|
||||
|
||||
have object_ptr_kinds_M_eq3_h2: "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])
|
||||
unfolding a_remove_child_locs_def
|
||||
using set_disconnected_nodes_pointers_preserved
|
||||
by (auto simp add: reflp_def transp_def)
|
||||
then have object_ptr_kinds_M_eq_h2: "\<And>ptrs. h2 \<turnstile> object_ptr_kinds_M \<rightarrow>\<^sub>r ptrs = h3 \<turnstile> object_ptr_kinds_M \<rightarrow>\<^sub>r ptrs"
|
||||
by(simp add: object_ptr_kinds_M_defs)
|
||||
then have object_ptr_kinds_M_eq2_h2: "|h2 \<turnstile> object_ptr_kinds_M|\<^sub>r = |h3 \<turnstile> object_ptr_kinds_M|\<^sub>r"
|
||||
by simp
|
||||
then have node_ptr_kinds_eq2_h2: "|h2 \<turnstile> node_ptr_kinds_M|\<^sub>r = |h3 \<turnstile> node_ptr_kinds_M|\<^sub>r"
|
||||
using node_ptr_kinds_M_eq by blast
|
||||
have document_ptr_kinds_eq2_h2: "|h2 \<turnstile> document_ptr_kinds_M|\<^sub>r = |h3 \<turnstile> document_ptr_kinds_M|\<^sub>r"
|
||||
using object_ptr_kinds_M_eq2_h2 document_ptr_kinds_M_eq by auto
|
||||
|
||||
have "known_ptrs h3"
|
||||
using object_ptr_kinds_M_eq3_h2 known_ptrs_preserved \<open>known_ptrs h2\<close> by blast
|
||||
|
||||
have object_ptr_kinds_M_eq3_h': "object_ptr_kinds h3 = object_ptr_kinds h'"
|
||||
apply(rule writes_small_big[where P="\<lambda>h h'. object_ptr_kinds h = object_ptr_kinds h'",
|
||||
OF insert_node_writes h'])
|
||||
unfolding a_remove_child_locs_def
|
||||
using set_child_nodes_pointers_preserved
|
||||
by (auto simp add: reflp_def transp_def)
|
||||
then have object_ptr_kinds_M_eq_h3:
|
||||
"\<And>ptrs. h3 \<turnstile> object_ptr_kinds_M \<rightarrow>\<^sub>r ptrs = h' \<turnstile> object_ptr_kinds_M \<rightarrow>\<^sub>r ptrs"
|
||||
by(simp add: object_ptr_kinds_M_defs)
|
||||
then have object_ptr_kinds_M_eq2_h3:
|
||||
"|h3 \<turnstile> object_ptr_kinds_M|\<^sub>r = |h' \<turnstile> object_ptr_kinds_M|\<^sub>r"
|
||||
by simp
|
||||
then have node_ptr_kinds_eq2_h3: "|h3 \<turnstile> node_ptr_kinds_M|\<^sub>r = |h' \<turnstile> node_ptr_kinds_M|\<^sub>r"
|
||||
using node_ptr_kinds_M_eq by blast
|
||||
have document_ptr_kinds_eq2_h3: "|h3 \<turnstile> document_ptr_kinds_M|\<^sub>r = |h' \<turnstile> document_ptr_kinds_M|\<^sub>r"
|
||||
using object_ptr_kinds_M_eq2_h3 document_ptr_kinds_M_eq by auto
|
||||
|
||||
have "known_ptrs h'"
|
||||
using object_ptr_kinds_M_eq3_h' known_ptrs_preserved \<open>known_ptrs h3\<close> by blast
|
||||
|
||||
have disconnected_nodes_eq_h2:
|
||||
"\<And>doc_ptr disc_nodes. owner_document \<noteq> doc_ptr
|
||||
\<Longrightarrow> h2 \<turnstile> get_disconnected_nodes doc_ptr \<rightarrow>\<^sub>r disc_nodes = h3 \<turnstile> get_disconnected_nodes doc_ptr \<rightarrow>\<^sub>r disc_nodes"
|
||||
using get_disconnected_nodes_reads set_disconnected_nodes_writes h3
|
||||
apply(rule reads_writes_preserved)
|
||||
by (auto simp add: set_disconnected_nodes_get_disconnected_nodes_different_pointers)
|
||||
then have disconnected_nodes_eq2_h2:
|
||||
"\<And>doc_ptr. doc_ptr \<noteq> owner_document
|
||||
\<Longrightarrow> |h2 \<turnstile> get_disconnected_nodes doc_ptr|\<^sub>r = |h3 \<turnstile> get_disconnected_nodes doc_ptr|\<^sub>r"
|
||||
using select_result_eq by force
|
||||
have disconnected_nodes_h3:
|
||||
"h3 \<turnstile> get_disconnected_nodes owner_document \<rightarrow>\<^sub>r remove1 node disconnected_nodes_h2"
|
||||
using h3 set_disconnected_nodes_get_disconnected_nodes
|
||||
by blast
|
||||
|
||||
have disconnected_nodes_eq_h3:
|
||||
"\<And>doc_ptr disc_nodes. h3 \<turnstile> get_disconnected_nodes doc_ptr \<rightarrow>\<^sub>r disc_nodes
|
||||
= h' \<turnstile> get_disconnected_nodes doc_ptr \<rightarrow>\<^sub>r disc_nodes"
|
||||
using get_disconnected_nodes_reads insert_node_writes h'
|
||||
apply(rule reads_writes_preserved)
|
||||
using set_child_nodes_get_disconnected_nodes by fast
|
||||
then have disconnected_nodes_eq2_h3:
|
||||
"\<And>doc_ptr. |h3 \<turnstile> get_disconnected_nodes doc_ptr|\<^sub>r = |h' \<turnstile> get_disconnected_nodes doc_ptr|\<^sub>r"
|
||||
using select_result_eq by force
|
||||
|
||||
have children_eq_h2:
|
||||
"\<And>ptr' children. h2 \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children = h3 \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children"
|
||||
using get_child_nodes_reads set_disconnected_nodes_writes h3
|
||||
apply(rule reads_writes_preserved)
|
||||
by (auto simp add: set_disconnected_nodes_get_child_nodes)
|
||||
then have children_eq2_h2:
|
||||
"\<And>ptr'. |h2 \<turnstile> get_child_nodes ptr'|\<^sub>r = |h3 \<turnstile> get_child_nodes ptr'|\<^sub>r"
|
||||
using select_result_eq by force
|
||||
|
||||
have children_eq_h3:
|
||||
"\<And>ptr' children. ptr \<noteq> ptr'
|
||||
\<Longrightarrow> h3 \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children = h' \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children"
|
||||
using get_child_nodes_reads insert_node_writes h'
|
||||
apply(rule reads_writes_preserved)
|
||||
by (auto simp add: set_child_nodes_get_child_nodes_different_pointers)
|
||||
then have children_eq2_h3:
|
||||
"\<And>ptr'. ptr \<noteq> ptr' \<Longrightarrow> |h3 \<turnstile> get_child_nodes ptr'|\<^sub>r = |h' \<turnstile> get_child_nodes ptr'|\<^sub>r"
|
||||
using select_result_eq by force
|
||||
obtain children_h3 where children_h3: "h3 \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children_h3"
|
||||
using h' a_insert_node_def by auto
|
||||
have children_h': "h' \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r insert_before_list node reference_child children_h3"
|
||||
using h' \<open>type_wf h3\<close> \<open>known_ptr ptr\<close>
|
||||
by(auto simp add: a_insert_node_def elim!: bind_returns_heap_E2
|
||||
dest!: set_child_nodes_get_child_nodes returns_result_eq[OF children_h3])
|
||||
|
||||
have ptr_in_heap: "ptr |\<in>| object_ptr_kinds h3"
|
||||
using children_h3 get_child_nodes_ptr_in_heap by blast
|
||||
have node_in_heap: "node |\<in>| node_ptr_kinds h"
|
||||
using h2 adopt_node_child_in_heap by fast
|
||||
have child_not_in_any_children:
|
||||
"\<And>p children. h2 \<turnstile> get_child_nodes p \<rightarrow>\<^sub>r children \<Longrightarrow> node \<notin> set children"
|
||||
using assms h2 adopt_node_removes_child by auto
|
||||
have "node \<in> set disconnected_nodes_h2"
|
||||
using disconnected_nodes_h2 h2 adopt_node_node_in_disconnected_nodes assms(1)
|
||||
\<open>type_wf h\<close> \<open>known_ptrs h\<close> by blast
|
||||
have node_not_in_disconnected_nodes:
|
||||
"\<And>d. d |\<in>| document_ptr_kinds h3 \<Longrightarrow> node \<notin> set |h3 \<turnstile> get_disconnected_nodes d|\<^sub>r"
|
||||
proof -
|
||||
fix d
|
||||
assume "d |\<in>| document_ptr_kinds h3"
|
||||
show "node \<notin> set |h3 \<turnstile> get_disconnected_nodes d|\<^sub>r"
|
||||
proof (cases "d = owner_document")
|
||||
case True
|
||||
then show ?thesis
|
||||
using disconnected_nodes_h2 wellformed_h2 h3 remove_from_disconnected_nodes_removes
|
||||
wellformed_h2 \<open>d |\<in>| document_ptr_kinds h3\<close> disconnected_nodes_h3
|
||||
by fastforce
|
||||
next
|
||||
case False
|
||||
then have
|
||||
"set |h2 \<turnstile> get_disconnected_nodes d|\<^sub>r \<inter> set |h2 \<turnstile> get_disconnected_nodes owner_document|\<^sub>r = {}"
|
||||
using distinct_concat_map_E(1) wellformed_h2
|
||||
by (metis (no_types, lifting) \<open>d |\<in>| document_ptr_kinds h3\<close> \<open>type_wf h2\<close>
|
||||
disconnected_nodes_h2 document_ptr_kinds_M_def document_ptr_kinds_eq2_h2
|
||||
l_ptr_kinds_M.ptr_kinds_ptr_kinds_M local.get_disconnected_nodes_ok
|
||||
local.heap_is_wellformed_one_disc_parent returns_result_select_result
|
||||
select_result_I2)
|
||||
then show ?thesis
|
||||
using disconnected_nodes_eq2_h2[OF False] \<open>node \<in> set disconnected_nodes_h2\<close>
|
||||
disconnected_nodes_h2 by fastforce
|
||||
qed
|
||||
qed
|
||||
|
||||
have "cast node \<noteq> ptr"
|
||||
using ancestors node_not_in_ancestors get_ancestors_ptr
|
||||
by fast
|
||||
|
||||
obtain ancestors_h2 where ancestors_h2: "h2 \<turnstile> get_ancestors ptr \<rightarrow>\<^sub>r ancestors_h2"
|
||||
using get_ancestors_ok object_ptr_kinds_M_eq2_h2 \<open>known_ptrs h2\<close> \<open>type_wf h2\<close>
|
||||
by (metis is_OK_returns_result_E object_ptr_kinds_M_eq3_h2 ptr_in_heap wellformed_h2)
|
||||
have ancestors_h3: "h3 \<turnstile> get_ancestors ptr \<rightarrow>\<^sub>r ancestors_h2"
|
||||
using get_ancestors_reads set_disconnected_nodes_writes h3
|
||||
apply(rule reads_writes_separate_forwards)
|
||||
using \<open>heap_is_wellformed h2\<close> ancestors_h2
|
||||
by (auto simp add: set_disconnected_nodes_get_ancestors)
|
||||
have node_not_in_ancestors_h2: "cast node \<notin> set ancestors_h2"
|
||||
apply(rule get_ancestors_remains_not_in_ancestors[OF assms(1) wellformed_h2 ancestors ancestors_h2])
|
||||
using adopt_node_children_subset using h2 \<open>known_ptrs h\<close> \<open> type_wf h\<close> apply(blast)
|
||||
using node_not_in_ancestors apply(blast)
|
||||
using object_ptr_kinds_M_eq3_h apply(blast)
|
||||
using \<open>known_ptrs h\<close> apply(blast)
|
||||
using \<open>type_wf h\<close> apply(blast)
|
||||
using \<open>type_wf h2\<close> by blast
|
||||
|
||||
have "acyclic (parent_child_rel h2)"
|
||||
using wellformed_h2 by (simp add: heap_is_wellformed_def acyclic_heap_def)
|
||||
then have "acyclic (parent_child_rel h3)"
|
||||
by(auto simp add: parent_child_rel_def object_ptr_kinds_M_eq3_h2 children_eq2_h2)
|
||||
moreover
|
||||
|
||||
have "cast node \<notin> {x. (x, ptr) \<in> (parent_child_rel h2)\<^sup>*}"
|
||||
using adopt_node_removes_child
|
||||
using ancestors node_not_in_ancestors
|
||||
using \<open>known_ptrs h2\<close> \<open>type_wf h2\<close> ancestors_h2 local.get_ancestors_parent_child_rel node_not_in_ancestors_h2 wellformed_h2
|
||||
by blast
|
||||
then have "cast node \<notin> {x. (x, ptr) \<in> (parent_child_rel h3)\<^sup>*}"
|
||||
by(auto simp add: parent_child_rel_def object_ptr_kinds_M_eq3_h2 children_eq2_h2)
|
||||
moreover have "parent_child_rel h'
|
||||
= insert (ptr, cast node) ((parent_child_rel h3))"
|
||||
using children_h3 children_h' ptr_in_heap
|
||||
apply(auto simp add: parent_child_rel_def object_ptr_kinds_M_eq3_h' children_eq2_h3
|
||||
insert_before_list_node_in_set)[1]
|
||||
apply (metis (no_types, lifting) children_eq2_h3 insert_before_list_in_set select_result_I2)
|
||||
by (metis (no_types, lifting) children_eq2_h3 imageI insert_before_list_in_set select_result_I2)
|
||||
ultimately show "acyclic (parent_child_rel h')"
|
||||
by (auto simp add: heap_is_wellformed_def)
|
||||
qed
|
||||
|
||||
lemma insert_before_heap_is_wellformed_preserved:
|
||||
assumes wellformed: "heap_is_wellformed h"
|
||||
and insert_before: "h \<turnstile> insert_before ptr node child \<rightarrow>\<^sub>h h'"
|
||||
|
|
@ -5446,6 +5692,306 @@ proof -
|
|||
ultimately show "heap_is_wellformed h'"
|
||||
by (simp add: heap_is_wellformed_def)
|
||||
qed
|
||||
|
||||
lemma adopt_node_children_remain_distinct_thesis:
|
||||
assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
|
||||
assumes "h \<turnstile> adopt_node owner_document node_ptr \<rightarrow>\<^sub>h h'"
|
||||
shows "\<And>ptr' children'.
|
||||
h' \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children' \<Longrightarrow> distinct children'"
|
||||
using assms(1) assms(2) assms(3) assms(4) local.adopt_node_preserves_wellformedness local.heap_is_wellformed_children_distinct
|
||||
by blast
|
||||
|
||||
|
||||
lemma insert_node_children_remain_distinct_thesis:
|
||||
assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
|
||||
assumes "h \<turnstile> a_insert_node ptr new_child reference_child_opt \<rightarrow>\<^sub>h h'"
|
||||
assumes "h \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children"
|
||||
assumes "new_child \<notin> set children"
|
||||
shows "\<And>children'.
|
||||
h' \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children' \<Longrightarrow> distinct children'"
|
||||
proof -
|
||||
fix children'
|
||||
assume a1: "h' \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children'"
|
||||
have "h' \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r (insert_before_list new_child reference_child_opt children)"
|
||||
using assms(4) assms(5) apply(auto simp add: a_insert_node_def elim!: bind_returns_heap_E)[1]
|
||||
using returns_result_eq set_child_nodes_get_child_nodes assms(2) assms(3)
|
||||
by (metis is_OK_returns_result_I local.get_child_nodes_ptr_in_heap local.get_child_nodes_pure local.known_ptrs_known_ptr pure_returns_heap_eq)
|
||||
moreover have "a_distinct_lists h"
|
||||
using assms local.heap_is_wellformed_def by blast
|
||||
then have "\<And>children. h \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children
|
||||
\<Longrightarrow> distinct children"
|
||||
using assms local.heap_is_wellformed_children_distinct by blast
|
||||
ultimately show "h' \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children' \<Longrightarrow> distinct children'"
|
||||
using assms(5) assms(6) insert_before_list_distinct returns_result_eq by fastforce
|
||||
qed
|
||||
|
||||
lemma insert_before_children_remain_distinct_thesis:
|
||||
assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
|
||||
assumes "h \<turnstile> insert_before ptr new_child child_opt \<rightarrow>\<^sub>h h'"
|
||||
shows "\<And>ptr' children'.
|
||||
h' \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children' \<Longrightarrow> distinct children'"
|
||||
proof -
|
||||
obtain reference_child owner_document h2 h3 disconnected_nodes_h2 where
|
||||
reference_child:
|
||||
"h \<turnstile> (if Some new_child = child_opt then a_next_sibling new_child else return child_opt) \<rightarrow>\<^sub>r reference_child" and
|
||||
owner_document: "h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document" and
|
||||
h2: "h \<turnstile> adopt_node owner_document new_child \<rightarrow>\<^sub>h h2" and
|
||||
disconnected_nodes_h2: "h2 \<turnstile> get_disconnected_nodes owner_document \<rightarrow>\<^sub>r disconnected_nodes_h2" and
|
||||
h3: "h2 \<turnstile> set_disconnected_nodes owner_document (remove1 new_child disconnected_nodes_h2) \<rightarrow>\<^sub>h h3" and
|
||||
h': "h3 \<turnstile> a_insert_node ptr new_child reference_child \<rightarrow>\<^sub>h h'"
|
||||
using assms(4)
|
||||
by(auto simp add: insert_before_def a_ensure_pre_insertion_validity_def
|
||||
elim!: bind_returns_heap_E bind_returns_result_E
|
||||
bind_returns_heap_E2[rotated, OF get_parent_pure, rotated]
|
||||
bind_returns_heap_E2[rotated, OF get_child_nodes_pure, rotated]
|
||||
bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated]
|
||||
bind_returns_heap_E2[rotated, OF get_ancestors_pure, rotated]
|
||||
bind_returns_heap_E2[rotated, OF next_sibling_pure, rotated]
|
||||
bind_returns_heap_E2[rotated, OF get_owner_document_pure, rotated]
|
||||
split: if_splits option.splits)
|
||||
|
||||
have "\<And>ptr children. h2 \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children
|
||||
\<Longrightarrow> distinct children"
|
||||
using adopt_node_children_remain_distinct_thesis
|
||||
using assms(1) assms(2) assms(3) h2
|
||||
by blast
|
||||
moreover have "\<And>ptr children. h2 \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children
|
||||
\<Longrightarrow> new_child \<notin> set children"
|
||||
using adopt_node_removes_child
|
||||
using assms(1) assms(2) assms(3) h2
|
||||
by blast
|
||||
moreover have "\<And>ptr children. h2 \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children = h3 \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children"
|
||||
using get_child_nodes_reads set_disconnected_nodes_writes h3
|
||||
apply(rule reads_writes_preserved)
|
||||
by (auto simp add: set_disconnected_nodes_get_child_nodes)
|
||||
ultimately show "\<And>ptr children. h' \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children
|
||||
\<Longrightarrow> distinct children"
|
||||
using insert_node_children_remain_distinct
|
||||
by (meson assms(1) assms(2) assms(3) assms(4) insert_before_heap_is_wellformed_preserved(1) local.heap_is_wellformed_children_distinct)
|
||||
qed
|
||||
|
||||
|
||||
lemma insert_before_removes_child_thesis:
|
||||
assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
|
||||
assumes "h \<turnstile> insert_before ptr node child \<rightarrow>\<^sub>h h'"
|
||||
assumes "ptr \<noteq> ptr'"
|
||||
shows "\<And>children'. h' \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children' \<Longrightarrow> node \<notin> set children'"
|
||||
proof -
|
||||
fix children'
|
||||
assume a1: "h' \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children'"
|
||||
obtain ancestors reference_child owner_document h2 h3 disconnected_nodes_h2 where
|
||||
ancestors: "h \<turnstile> get_ancestors ptr \<rightarrow>\<^sub>r ancestors" and
|
||||
node_not_in_ancestors: "cast node \<notin> set ancestors" and
|
||||
reference_child:
|
||||
"h \<turnstile> (if Some node = child then a_next_sibling node else return child) \<rightarrow>\<^sub>r reference_child" and
|
||||
owner_document: "h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document" and
|
||||
h2: "h \<turnstile> adopt_node owner_document node \<rightarrow>\<^sub>h h2" and
|
||||
disconnected_nodes_h2: "h2 \<turnstile> get_disconnected_nodes owner_document \<rightarrow>\<^sub>r disconnected_nodes_h2" and
|
||||
h3: "h2 \<turnstile> set_disconnected_nodes owner_document (remove1 node disconnected_nodes_h2) \<rightarrow>\<^sub>h h3" and
|
||||
h': "h3 \<turnstile> a_insert_node ptr node reference_child \<rightarrow>\<^sub>h h'"
|
||||
using assms(4)
|
||||
by(auto simp add: insert_before_def a_ensure_pre_insertion_validity_def
|
||||
elim!: bind_returns_heap_E bind_returns_result_E
|
||||
bind_returns_heap_E2[rotated, OF get_parent_pure, rotated]
|
||||
bind_returns_heap_E2[rotated, OF get_child_nodes_pure, rotated]
|
||||
bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated]
|
||||
bind_returns_heap_E2[rotated, OF get_ancestors_pure, rotated]
|
||||
bind_returns_heap_E2[rotated, OF next_sibling_pure, rotated]
|
||||
bind_returns_heap_E2[rotated, OF get_owner_document_pure, rotated]
|
||||
split: if_splits option.splits)
|
||||
|
||||
have "known_ptr ptr"
|
||||
by (meson get_owner_document_ptr_in_heap is_OK_returns_result_I assms(2)
|
||||
l_known_ptrs.known_ptrs_known_ptr l_known_ptrs_axioms owner_document)
|
||||
|
||||
have "type_wf h2"
|
||||
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF adopt_node_writes h2]
|
||||
using assms(3) adopt_node_types_preserved
|
||||
by(auto simp add: a_remove_child_locs_def reflp_def transp_def)
|
||||
then have "type_wf h3"
|
||||
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF set_disconnected_nodes_writes h3]
|
||||
using set_disconnected_nodes_types_preserved
|
||||
by(auto simp add: reflp_def transp_def)
|
||||
then have "type_wf h'"
|
||||
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF insert_node_writes h']
|
||||
using set_child_nodes_types_preserved
|
||||
by(auto simp add: reflp_def transp_def)
|
||||
|
||||
have object_ptr_kinds_M_eq3_h: "object_ptr_kinds h = object_ptr_kinds h2"
|
||||
apply(rule writes_small_big[where P="\<lambda>h h'. object_ptr_kinds h = object_ptr_kinds h'",
|
||||
OF adopt_node_writes h2])
|
||||
using adopt_node_pointers_preserved
|
||||
apply blast
|
||||
by (auto simp add: reflp_def transp_def)
|
||||
then have object_ptr_kinds_M_eq_h: "\<And>ptrs. h \<turnstile> object_ptr_kinds_M \<rightarrow>\<^sub>r ptrs = h2 \<turnstile> object_ptr_kinds_M \<rightarrow>\<^sub>r ptrs"
|
||||
by(simp add: object_ptr_kinds_M_defs )
|
||||
then have object_ptr_kinds_M_eq2_h: "|h \<turnstile> object_ptr_kinds_M|\<^sub>r = |h2 \<turnstile> object_ptr_kinds_M|\<^sub>r"
|
||||
by simp
|
||||
then have node_ptr_kinds_eq2_h: "|h \<turnstile> node_ptr_kinds_M|\<^sub>r = |h2 \<turnstile> node_ptr_kinds_M|\<^sub>r"
|
||||
using node_ptr_kinds_M_eq by blast
|
||||
|
||||
have "known_ptrs h2"
|
||||
using assms object_ptr_kinds_M_eq3_h known_ptrs_preserved by blast
|
||||
|
||||
have wellformed_h2: "heap_is_wellformed h2"
|
||||
using adopt_node_preserves_wellformedness[OF assms(1) h2] assms by simp
|
||||
|
||||
have object_ptr_kinds_M_eq3_h2: "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])
|
||||
unfolding a_remove_child_locs_def
|
||||
using set_disconnected_nodes_pointers_preserved
|
||||
by (auto simp add: reflp_def transp_def)
|
||||
then have object_ptr_kinds_M_eq_h2: "\<And>ptrs. h2 \<turnstile> object_ptr_kinds_M \<rightarrow>\<^sub>r ptrs = h3 \<turnstile> object_ptr_kinds_M \<rightarrow>\<^sub>r ptrs"
|
||||
by(simp add: object_ptr_kinds_M_defs)
|
||||
then have object_ptr_kinds_M_eq2_h2: "|h2 \<turnstile> object_ptr_kinds_M|\<^sub>r = |h3 \<turnstile> object_ptr_kinds_M|\<^sub>r"
|
||||
by simp
|
||||
then have node_ptr_kinds_eq2_h2: "|h2 \<turnstile> node_ptr_kinds_M|\<^sub>r = |h3 \<turnstile> node_ptr_kinds_M|\<^sub>r"
|
||||
using node_ptr_kinds_M_eq by blast
|
||||
have document_ptr_kinds_eq2_h2: "|h2 \<turnstile> document_ptr_kinds_M|\<^sub>r = |h3 \<turnstile> document_ptr_kinds_M|\<^sub>r"
|
||||
using object_ptr_kinds_M_eq2_h2 document_ptr_kinds_M_eq by auto
|
||||
|
||||
have "known_ptrs h3"
|
||||
using object_ptr_kinds_M_eq3_h2 known_ptrs_preserved \<open>known_ptrs h2\<close> by blast
|
||||
|
||||
have object_ptr_kinds_M_eq3_h': "object_ptr_kinds h3 = object_ptr_kinds h'"
|
||||
apply(rule writes_small_big[where P="\<lambda>h h'. object_ptr_kinds h = object_ptr_kinds h'",
|
||||
OF insert_node_writes h'])
|
||||
unfolding a_remove_child_locs_def
|
||||
using set_child_nodes_pointers_preserved
|
||||
by (auto simp add: reflp_def transp_def)
|
||||
then have object_ptr_kinds_M_eq_h3:
|
||||
"\<And>ptrs. h3 \<turnstile> object_ptr_kinds_M \<rightarrow>\<^sub>r ptrs = h' \<turnstile> object_ptr_kinds_M \<rightarrow>\<^sub>r ptrs"
|
||||
by(simp add: object_ptr_kinds_M_defs)
|
||||
then have object_ptr_kinds_M_eq2_h3:
|
||||
"|h3 \<turnstile> object_ptr_kinds_M|\<^sub>r = |h' \<turnstile> object_ptr_kinds_M|\<^sub>r"
|
||||
by simp
|
||||
then have node_ptr_kinds_eq2_h3: "|h3 \<turnstile> node_ptr_kinds_M|\<^sub>r = |h' \<turnstile> node_ptr_kinds_M|\<^sub>r"
|
||||
using node_ptr_kinds_M_eq by blast
|
||||
have document_ptr_kinds_eq2_h3: "|h3 \<turnstile> document_ptr_kinds_M|\<^sub>r = |h' \<turnstile> document_ptr_kinds_M|\<^sub>r"
|
||||
using object_ptr_kinds_M_eq2_h3 document_ptr_kinds_M_eq by auto
|
||||
|
||||
have "known_ptrs h'"
|
||||
using object_ptr_kinds_M_eq3_h' known_ptrs_preserved \<open>known_ptrs h3\<close> by blast
|
||||
|
||||
have disconnected_nodes_eq_h2:
|
||||
"\<And>doc_ptr disc_nodes. owner_document \<noteq> doc_ptr
|
||||
\<Longrightarrow> h2 \<turnstile> get_disconnected_nodes doc_ptr \<rightarrow>\<^sub>r disc_nodes = h3 \<turnstile> get_disconnected_nodes doc_ptr \<rightarrow>\<^sub>r disc_nodes"
|
||||
using get_disconnected_nodes_reads set_disconnected_nodes_writes h3
|
||||
apply(rule reads_writes_preserved)
|
||||
by (auto simp add: set_disconnected_nodes_get_disconnected_nodes_different_pointers)
|
||||
then have disconnected_nodes_eq2_h2:
|
||||
"\<And>doc_ptr. doc_ptr \<noteq> owner_document
|
||||
\<Longrightarrow> |h2 \<turnstile> get_disconnected_nodes doc_ptr|\<^sub>r = |h3 \<turnstile> get_disconnected_nodes doc_ptr|\<^sub>r"
|
||||
using select_result_eq by force
|
||||
have disconnected_nodes_h3:
|
||||
"h3 \<turnstile> get_disconnected_nodes owner_document \<rightarrow>\<^sub>r remove1 node disconnected_nodes_h2"
|
||||
using h3 set_disconnected_nodes_get_disconnected_nodes
|
||||
by blast
|
||||
|
||||
have disconnected_nodes_eq_h3:
|
||||
"\<And>doc_ptr disc_nodes. h3 \<turnstile> get_disconnected_nodes doc_ptr \<rightarrow>\<^sub>r disc_nodes
|
||||
= h' \<turnstile> get_disconnected_nodes doc_ptr \<rightarrow>\<^sub>r disc_nodes"
|
||||
using get_disconnected_nodes_reads insert_node_writes h'
|
||||
apply(rule reads_writes_preserved)
|
||||
using set_child_nodes_get_disconnected_nodes by fast
|
||||
then have disconnected_nodes_eq2_h3:
|
||||
"\<And>doc_ptr. |h3 \<turnstile> get_disconnected_nodes doc_ptr|\<^sub>r = |h' \<turnstile> get_disconnected_nodes doc_ptr|\<^sub>r"
|
||||
using select_result_eq by force
|
||||
|
||||
have children_eq_h2:
|
||||
"\<And>ptr' children. h2 \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children = h3 \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children"
|
||||
using get_child_nodes_reads set_disconnected_nodes_writes h3
|
||||
apply(rule reads_writes_preserved)
|
||||
by (auto simp add: set_disconnected_nodes_get_child_nodes)
|
||||
then have children_eq2_h2:
|
||||
"\<And>ptr'. |h2 \<turnstile> get_child_nodes ptr'|\<^sub>r = |h3 \<turnstile> get_child_nodes ptr'|\<^sub>r"
|
||||
using select_result_eq by force
|
||||
|
||||
have children_eq_h3:
|
||||
"\<And>ptr' children. ptr \<noteq> ptr'
|
||||
\<Longrightarrow> h3 \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children = h' \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children"
|
||||
using get_child_nodes_reads insert_node_writes h'
|
||||
apply(rule reads_writes_preserved)
|
||||
by (auto simp add: set_child_nodes_get_child_nodes_different_pointers)
|
||||
then have children_eq2_h3:
|
||||
"\<And>ptr'. ptr \<noteq> ptr' \<Longrightarrow> |h3 \<turnstile> get_child_nodes ptr'|\<^sub>r = |h' \<turnstile> get_child_nodes ptr'|\<^sub>r"
|
||||
using select_result_eq by force
|
||||
obtain children_h3 where children_h3: "h3 \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children_h3"
|
||||
using h' a_insert_node_def by auto
|
||||
have children_h': "h' \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r insert_before_list node reference_child children_h3"
|
||||
using h' \<open>type_wf h3\<close> \<open>known_ptr ptr\<close>
|
||||
by(auto simp add: a_insert_node_def elim!: bind_returns_heap_E2
|
||||
dest!: set_child_nodes_get_child_nodes returns_result_eq[OF children_h3])
|
||||
|
||||
have ptr_in_heap: "ptr |\<in>| object_ptr_kinds h3"
|
||||
using children_h3 get_child_nodes_ptr_in_heap by blast
|
||||
have node_in_heap: "node |\<in>| node_ptr_kinds h"
|
||||
using h2 adopt_node_child_in_heap by fast
|
||||
have child_not_in_any_children:
|
||||
"\<And>p children. h2 \<turnstile> get_child_nodes p \<rightarrow>\<^sub>r children \<Longrightarrow> node \<notin> set children"
|
||||
using assms(1) assms(2) assms(3) h2 local.adopt_node_removes_child by blast
|
||||
show "node \<notin> set children'"
|
||||
using a1 assms(5) child_not_in_any_children children_eq_h2 children_eq_h3 by blast
|
||||
qed
|
||||
|
||||
lemma ensure_pre_insertion_validity_ok:
|
||||
assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
|
||||
assumes "ptr |\<in>| object_ptr_kinds h"
|
||||
assumes "\<not>is_character_data_ptr_kind parent"
|
||||
assumes "cast node \<notin> set |h \<turnstile> get_ancestors parent|\<^sub>r"
|
||||
assumes "h \<turnstile> get_parent ref \<rightarrow>\<^sub>r Some parent"
|
||||
assumes "is_document_ptr parent \<Longrightarrow> h \<turnstile> get_child_nodes parent \<rightarrow>\<^sub>r []"
|
||||
assumes "is_document_ptr parent \<Longrightarrow> \<not>is_character_data_ptr_kind node"
|
||||
shows "h \<turnstile> ok (a_ensure_pre_insertion_validity node parent (Some ref))"
|
||||
proof -
|
||||
have "h \<turnstile> (if is_character_data_ptr_kind parent
|
||||
then error HierarchyRequestError else return ()) \<rightarrow>\<^sub>r ()"
|
||||
using assms
|
||||
by (simp add: assms(4))
|
||||
moreover have "h \<turnstile> do {
|
||||
ancestors \<leftarrow> get_ancestors parent;
|
||||
(if cast node \<in> set ancestors then error HierarchyRequestError else return ())
|
||||
} \<rightarrow>\<^sub>r ()"
|
||||
using assms(6)
|
||||
apply(auto intro!: bind_pure_returns_result_I)
|
||||
using assms(1) assms(2) assms(3) assms(7) local.get_ancestors_ok local.get_parent_parent_in_heap by auto
|
||||
|
||||
moreover have "h \<turnstile> do {
|
||||
(case Some ref of
|
||||
Some child \<Rightarrow> do {
|
||||
child_parent \<leftarrow> get_parent child;
|
||||
(if child_parent \<noteq> Some parent then error NotFoundError else return ())}
|
||||
| None \<Rightarrow> return ())
|
||||
} \<rightarrow>\<^sub>r ()"
|
||||
using assms(7)
|
||||
by(auto split: option.splits)
|
||||
moreover have "h \<turnstile> do {
|
||||
children \<leftarrow> get_child_nodes parent;
|
||||
(if children \<noteq> [] \<and> is_document_ptr parent
|
||||
then error HierarchyRequestError else return ())
|
||||
} \<rightarrow>\<^sub>r ()"
|
||||
using assms(8)
|
||||
by (smt assms(5) assms(7) bind_pure_returns_result_I2 calculation(1) is_OK_returns_result_I local.get_child_nodes_pure local.get_parent_child_dual returns_result_eq)
|
||||
|
||||
moreover have "h \<turnstile> do {
|
||||
(if is_character_data_ptr node \<and> is_document_ptr parent
|
||||
then error HierarchyRequestError else return ())
|
||||
} \<rightarrow>\<^sub>r ()"
|
||||
using assms
|
||||
using is_character_data_ptr_kind_none by force
|
||||
ultimately show ?thesis
|
||||
unfolding a_ensure_pre_insertion_validity_def
|
||||
apply(intro bind_is_OK_pure_I)
|
||||
apply(auto)
|
||||
using assms(1) assms(2) assms(3) assms(7) local.get_ancestors_ok local.get_parent_parent_in_heap apply blast
|
||||
|
||||
using assms(6) apply auto[1]
|
||||
apply (smt assms(7) bind_returns_heap_E2 is_OK_returns_heap_E local.get_parent_pure pure_def pure_returns_heap_eq return_pure returns_result_eq)
|
||||
apply (meson assms(7) is_OK_returns_result_I local.get_parent_child_dual)
|
||||
by (simp add: assms(8) returns_result_eq)
|
||||
qed
|
||||
|
||||
end
|
||||
|
||||
locale l_insert_before_wf2 = l_type_wf + l_known_ptrs + l_insert_before_defs
|
||||
|
|
|
|||
Reference in New Issue