|
|
|
|
@ -145,7 +145,6 @@ defines heap_is_wellformed = "l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub
|
|
|
|
|
and owner_document_valid = a_owner_document_valid
|
|
|
|
|
.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
locale l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
|
|
|
|
|
l_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs
|
|
|
|
|
+ l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs get_child_nodes get_child_nodes_locs get_disconnected_nodes
|
|
|
|
|
@ -1813,9 +1812,6 @@ 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:
|
|
|
|
|
"ptr |\<in>| object_ptr_kinds h \<Longrightarrow> \<not>is_node_ptr_kind 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"
|
|
|
|
|
@ -1854,7 +1850,6 @@ 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_parent_same apply (blast, blast)
|
|
|
|
|
done
|
|
|
|
|
|
|
|
|
|
@ -3581,8 +3576,7 @@ have "type_wf h2"
|
|
|
|
|
apply(auto simp add: a_owner_document_valid_def object_ptr_kinds_eq3 document_ptr_kinds_eq3
|
|
|
|
|
node_ptr_kinds_eq3)[1]
|
|
|
|
|
proof -
|
|
|
|
|
|
|
|
|
|
fix node_ptr
|
|
|
|
|
fix node_ptr
|
|
|
|
|
assume 0: "\<forall>node_ptr\<in>fset (node_ptr_kinds h'). (\<exists>document_ptr. document_ptr |\<in>| document_ptr_kinds h' \<and> node_ptr \<in> set |h \<turnstile> get_disconnected_nodes document_ptr|\<^sub>r) \<or> (\<exists>parent_ptr. parent_ptr |\<in>| object_ptr_kinds h' \<and> node_ptr \<in> set |h \<turnstile> get_child_nodes parent_ptr|\<^sub>r)"
|
|
|
|
|
and 1: "node_ptr |\<in>| node_ptr_kinds h'"
|
|
|
|
|
and 2: "\<forall>parent_ptr. parent_ptr |\<in>| object_ptr_kinds h' \<longrightarrow> node_ptr \<notin> set |h' \<turnstile> get_child_nodes parent_ptr|\<^sub>r"
|
|
|
|
|
@ -4534,9 +4528,15 @@ proof -
|
|
|
|
|
using wellformed_h2 by (simp add: heap_is_wellformed_def)
|
|
|
|
|
then have "a_owner_document_valid h'"
|
|
|
|
|
apply(simp add: a_owner_document_valid_def node_ptr_kinds_eq_h2 node_ptr_kinds_eq3_h3
|
|
|
|
|
object_ptr_kinds_eq_h2 object_ptr_kinds_eq_h3 document_ptr_kinds_eq2_h2
|
|
|
|
|
object_ptr_kinds_eq_h2 object_ptr_kinds_eq_h3 document_ptr_kinds_eq2_h2
|
|
|
|
|
document_ptr_kinds_eq2_h3 children_eq2_h2 children_eq2_h3 )
|
|
|
|
|
by (smt disc_nodes_document_ptr_h' disc_nodes_document_ptr_h2 disc_nodes_old_document_h2 disc_nodes_old_document_h3 disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 document_ptr_in_heap document_ptr_kinds_eq3_h2 document_ptr_kinds_eq3_h3 in_set_remove1 list.set_intros(1) node_ptr_kinds_eq3_h2 node_ptr_kinds_eq3_h3 object_ptr_kinds_h2_eq3 object_ptr_kinds_h3_eq3 select_result_I2 set_subset_Cons subset_code(1))
|
|
|
|
|
by (smt disc_nodes_document_ptr_h' disc_nodes_document_ptr_h2
|
|
|
|
|
disc_nodes_old_document_h2 disc_nodes_old_document_h3
|
|
|
|
|
disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 document_ptr_in_heap
|
|
|
|
|
document_ptr_kinds_eq3_h2 document_ptr_kinds_eq3_h3 in_set_remove1
|
|
|
|
|
list.set_intros(1) list.set_intros(2) node_ptr_kinds_eq3_h2
|
|
|
|
|
node_ptr_kinds_eq3_h3 object_ptr_kinds_h2_eq3 object_ptr_kinds_h3_eq3
|
|
|
|
|
select_result_I2)
|
|
|
|
|
|
|
|
|
|
have a_distinct_lists_h2: "a_distinct_lists h2"
|
|
|
|
|
using wellformed_h2 by (simp add: heap_is_wellformed_def)
|
|
|
|
|
@ -5486,7 +5486,7 @@ proof -
|
|
|
|
|
have "a_all_ptrs_in_heap h3"
|
|
|
|
|
using \<open>a_all_ptrs_in_heap h2\<close>
|
|
|
|
|
apply(auto simp add: a_all_ptrs_in_heap_def object_ptr_kinds_M_eq2_h2 node_ptr_kinds_eq2_h2
|
|
|
|
|
children_eq_h2)[1]
|
|
|
|
|
children_eq_h2)[1]
|
|
|
|
|
using disconnected_nodes_eq2_h2 disconnected_nodes_h2 disconnected_nodes_h3
|
|
|
|
|
using node_ptr_kinds_eq2_h2 apply auto[1]
|
|
|
|
|
apply (metis \<open>known_ptrs h2\<close> \<open>type_wf h3\<close> children_eq_h2 local.get_child_nodes_ok local.heap_is_wellformed_children_in_heap local.known_ptrs_known_ptr object_ptr_kinds_M_eq3_h2 returns_result_select_result wellformed_h2)
|
|
|
|
|
@ -5501,15 +5501,13 @@ proof -
|
|
|
|
|
using node_in_heap
|
|
|
|
|
apply(auto simp add: node_ptr_kinds_eq2_h node_ptr_kinds_eq2_h2 node_ptr_kinds_eq2_h3)[1]
|
|
|
|
|
by (metis (no_types, hide_lams) contra_subsetD finite_set_in insert_before_list_in_set
|
|
|
|
|
node_ptr_kinds_commutes object_ptr_kinds_M_eq3_h object_ptr_kinds_M_eq3_h'
|
|
|
|
|
object_ptr_kinds_M_eq3_h2)
|
|
|
|
|
node_ptr_kinds_commutes object_ptr_kinds_M_eq3_h object_ptr_kinds_M_eq3_h'
|
|
|
|
|
object_ptr_kinds_M_eq3_h2)
|
|
|
|
|
then show ?thesis
|
|
|
|
|
using \<open>a_all_ptrs_in_heap h3\<close>
|
|
|
|
|
apply(auto simp add: object_ptr_kinds_M_eq3_h' a_all_ptrs_in_heap_def node_ptr_kinds_def
|
|
|
|
|
node_ptr_kinds_eq2_h3 disconnected_nodes_eq_h3)[1]
|
|
|
|
|
node_ptr_kinds_eq2_h3 disconnected_nodes_eq_h3)[1]
|
|
|
|
|
using children_eq_h3 children_h'
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
apply (metis (no_types, lifting) children_eq2_h3 finite_set_in select_result_I2 subsetD)
|
|
|
|
|
by (metis (no_types) \<open>type_wf h'\<close> disconnected_nodes_eq2_h3 disconnected_nodes_eq_h3 finite_set_in is_OK_returns_result_I local.get_disconnected_nodes_ok local.get_disconnected_nodes_ptr_in_heap returns_result_select_result subsetD)
|
|
|
|
|
qed
|
|
|
|
|
@ -5518,14 +5516,14 @@ proof -
|
|
|
|
|
using wellformed_h2 by (simp add: heap_is_wellformed_def)
|
|
|
|
|
then have "a_distinct_lists h3"
|
|
|
|
|
proof(auto simp add: a_distinct_lists_def object_ptr_kinds_M_eq2_h2 document_ptr_kinds_eq2_h2
|
|
|
|
|
children_eq2_h2 intro!: distinct_concat_map_I)[1]
|
|
|
|
|
children_eq2_h2 intro!: distinct_concat_map_I)[1]
|
|
|
|
|
fix x
|
|
|
|
|
assume 1: "x |\<in>| document_ptr_kinds h3"
|
|
|
|
|
and 2: "distinct (concat (map (\<lambda>document_ptr. |h2 \<turnstile> get_disconnected_nodes document_ptr|\<^sub>r)
|
|
|
|
|
(sorted_list_of_set (fset (document_ptr_kinds h3)))))"
|
|
|
|
|
show "distinct |h3 \<turnstile> get_disconnected_nodes x|\<^sub>r"
|
|
|
|
|
using distinct_concat_map_E(2)[OF 2] select_result_I2[OF disconnected_nodes_h3]
|
|
|
|
|
disconnected_nodes_eq2_h2 select_result_I2[OF disconnected_nodes_h2] 1
|
|
|
|
|
disconnected_nodes_eq2_h2 select_result_I2[OF disconnected_nodes_h2] 1
|
|
|
|
|
by (metis (full_types) distinct_remove1 finite_fset fmember.rep_eq set_sorted_list_of_set)
|
|
|
|
|
next
|
|
|
|
|
fix x y xa
|
|
|
|
|
@ -5552,17 +5550,17 @@ proof -
|
|
|
|
|
proof (cases "y = owner_document")
|
|
|
|
|
case True
|
|
|
|
|
then show ?thesis
|
|
|
|
|
using distinct_concat_map_E(1)[OF 1]
|
|
|
|
|
using 2 3 4 5 6 select_result_I2[OF disconnected_nodes_h3] select_result_I2[OF disconnected_nodes_h2]
|
|
|
|
|
apply(auto simp add: True disconnected_nodes_eq2_h2[OF \<open>x \<noteq> owner_document\<close>])[1]
|
|
|
|
|
by (metis (no_types, hide_lams) disconnected_nodes_eq2_h2 disjoint_iff_not_equal notin_set_remove1)
|
|
|
|
|
using distinct_concat_map_E(1)[OF 1]
|
|
|
|
|
using 2 3 4 5 6 select_result_I2[OF disconnected_nodes_h3] select_result_I2[OF disconnected_nodes_h2]
|
|
|
|
|
apply(auto simp add: True disconnected_nodes_eq2_h2[OF \<open>x \<noteq> owner_document\<close>])[1]
|
|
|
|
|
by (metis (no_types, hide_lams) disconnected_nodes_eq2_h2 disjoint_iff_not_equal notin_set_remove1)
|
|
|
|
|
next
|
|
|
|
|
case False
|
|
|
|
|
then show ?thesis
|
|
|
|
|
using distinct_concat_map_E(1)[OF 1, simplified, OF 2 3 4] 5 6
|
|
|
|
|
using disconnected_nodes_eq2_h2 disconnected_nodes_h2 disconnected_nodes_h3
|
|
|
|
|
disjoint_iff_not_equal finite_fset fmember.rep_eq notin_set_remove1 select_result_I2
|
|
|
|
|
set_sorted_list_of_set
|
|
|
|
|
disjoint_iff_not_equal finite_fset fmember.rep_eq notin_set_remove1 select_result_I2
|
|
|
|
|
set_sorted_list_of_set
|
|
|
|
|
by (metis (no_types, lifting))
|
|
|
|
|
qed
|
|
|
|
|
qed
|
|
|
|
|
@ -5577,10 +5575,10 @@ proof -
|
|
|
|
|
have 6: "set |h3 \<turnstile> get_child_nodes xa|\<^sub>r \<inter> set |h2 \<turnstile> get_disconnected_nodes xb|\<^sub>r = {}"
|
|
|
|
|
using 1 2 4
|
|
|
|
|
by (metis \<open>type_wf h2\<close> children_eq2_h2 document_ptr_kinds_commutes known_ptrs
|
|
|
|
|
local.get_child_nodes_ok local.get_disconnected_nodes_ok
|
|
|
|
|
local.heap_is_wellformed_children_disc_nodes_different local.known_ptrs_known_ptr
|
|
|
|
|
object_ptr_kinds_M_eq3_h object_ptr_kinds_M_eq3_h2 returns_result_select_result
|
|
|
|
|
wellformed_h2)
|
|
|
|
|
local.get_child_nodes_ok local.get_disconnected_nodes_ok
|
|
|
|
|
local.heap_is_wellformed_children_disc_nodes_different local.known_ptrs_known_ptr
|
|
|
|
|
object_ptr_kinds_M_eq3_h object_ptr_kinds_M_eq3_h2 returns_result_select_result
|
|
|
|
|
wellformed_h2)
|
|
|
|
|
show False
|
|
|
|
|
proof (cases "xb = owner_document")
|
|
|
|
|
case True
|
|
|
|
|
@ -5595,11 +5593,11 @@ proof -
|
|
|
|
|
qed
|
|
|
|
|
then have "a_distinct_lists h'"
|
|
|
|
|
proof(auto simp add: a_distinct_lists_def document_ptr_kinds_eq2_h3 object_ptr_kinds_M_eq2_h3
|
|
|
|
|
disconnected_nodes_eq2_h3 intro!: distinct_concat_map_I)[1]
|
|
|
|
|
disconnected_nodes_eq2_h3 intro!: distinct_concat_map_I)[1]
|
|
|
|
|
fix x
|
|
|
|
|
assume 1: "distinct (concat (map (\<lambda>ptr. |h3 \<turnstile> get_child_nodes ptr|\<^sub>r)
|
|
|
|
|
(sorted_list_of_set (fset (object_ptr_kinds h')))))" and
|
|
|
|
|
2: "x |\<in>| object_ptr_kinds h'"
|
|
|
|
|
2: "x |\<in>| object_ptr_kinds h'"
|
|
|
|
|
have 3: "\<And>p. p |\<in>| object_ptr_kinds h' \<Longrightarrow> distinct |h3 \<turnstile> get_child_nodes p|\<^sub>r"
|
|
|
|
|
using 1 by (auto elim: distinct_concat_map_E)
|
|
|
|
|
show "distinct |h' \<turnstile> get_child_nodes x|\<^sub>r"
|
|
|
|
|
@ -5608,7 +5606,7 @@ proof -
|
|
|
|
|
show ?thesis
|
|
|
|
|
using 3[OF 2] children_h3 children_h'
|
|
|
|
|
by(auto simp add: True insert_before_list_distinct
|
|
|
|
|
dest: child_not_in_any_children[unfolded children_eq_h2])
|
|
|
|
|
dest: child_not_in_any_children[unfolded children_eq_h2])
|
|
|
|
|
next
|
|
|
|
|
case False
|
|
|
|
|
show ?thesis
|
|
|
|
|
@ -5634,9 +5632,9 @@ proof -
|
|
|
|
|
using children_h3 children_h' child_not_in_any_children[unfolded children_eq_h2] 5 6
|
|
|
|
|
apply(auto simp add: True children_eq2_h3[OF \<open>ptr \<noteq> y\<close>])[1]
|
|
|
|
|
by (metis (no_types, hide_lams) "3" "7" \<open>type_wf h3\<close> children_eq2_h3 disjoint_iff_not_equal
|
|
|
|
|
get_child_nodes_ok insert_before_list_in_set known_ptrs local.known_ptrs_known_ptr
|
|
|
|
|
object_ptr_kinds_M_eq3_h object_ptr_kinds_M_eq3_h'
|
|
|
|
|
object_ptr_kinds_M_eq3_h2 returns_result_select_result select_result_I2)
|
|
|
|
|
get_child_nodes_ok insert_before_list_in_set known_ptrs local.known_ptrs_known_ptr
|
|
|
|
|
object_ptr_kinds_M_eq3_h object_ptr_kinds_M_eq3_h'
|
|
|
|
|
object_ptr_kinds_M_eq3_h2 returns_result_select_result select_result_I2)
|
|
|
|
|
next
|
|
|
|
|
case False
|
|
|
|
|
then show ?thesis
|
|
|
|
|
@ -5646,10 +5644,10 @@ proof -
|
|
|
|
|
using children_h3 children_h' child_not_in_any_children[unfolded children_eq_h2] 5 6
|
|
|
|
|
apply(auto simp add: True children_eq2_h3[OF \<open>ptr \<noteq> x\<close>])[1]
|
|
|
|
|
by (metis (no_types, hide_lams) "2" "4" "7" IntI \<open>known_ptrs h3\<close> \<open>type_wf h'\<close>
|
|
|
|
|
children_eq_h3 empty_iff insert_before_list_in_set local.get_child_nodes_ok
|
|
|
|
|
local.known_ptrs_known_ptr object_ptr_kinds_M_eq3_h'
|
|
|
|
|
returns_result_select_result select_result_I2)
|
|
|
|
|
next
|
|
|
|
|
children_eq_h3 empty_iff insert_before_list_in_set local.get_child_nodes_ok
|
|
|
|
|
local.known_ptrs_known_ptr object_ptr_kinds_M_eq3_h'
|
|
|
|
|
returns_result_select_result select_result_I2)
|
|
|
|
|
next
|
|
|
|
|
case False
|
|
|
|
|
then show ?thesis
|
|
|
|
|
using children_eq2_h3[OF \<open>ptr \<noteq> x\<close>] children_eq2_h3[OF \<open>ptr \<noteq> y\<close>] 5 6 7 by auto
|
|
|
|
|
@ -5682,13 +5680,13 @@ proof -
|
|
|
|
|
case True
|
|
|
|
|
show ?thesis
|
|
|
|
|
using 6 node_not_in_disconnected_nodes 3 4 5 select_result_I2[OF children_h']
|
|
|
|
|
select_result_I2[OF children_h3] True disconnected_nodes_eq2_h3
|
|
|
|
|
select_result_I2[OF children_h3] True disconnected_nodes_eq2_h3
|
|
|
|
|
by (metis (no_types, lifting) "2" DocumentMonad.ptr_kinds_ptr_kinds_M
|
|
|
|
|
\<open>a_distinct_lists h3\<close> \<open>type_wf h'\<close> disconnected_nodes_eq_h3
|
|
|
|
|
distinct_lists_no_parent document_ptr_kinds_eq2_h3 get_disconnected_nodes_ok
|
|
|
|
|
insert_before_list_in_set object_ptr_kinds_M_eq3_h' returns_result_select_result)
|
|
|
|
|
\<open>a_distinct_lists h3\<close> \<open>type_wf h'\<close> disconnected_nodes_eq_h3
|
|
|
|
|
distinct_lists_no_parent document_ptr_kinds_eq2_h3 get_disconnected_nodes_ok
|
|
|
|
|
insert_before_list_in_set object_ptr_kinds_M_eq3_h' returns_result_select_result)
|
|
|
|
|
|
|
|
|
|
next
|
|
|
|
|
next
|
|
|
|
|
case False
|
|
|
|
|
then show ?thesis
|
|
|
|
|
using 1 2 3 4 5 children_eq2_h3[OF False] by fastforce
|
|
|
|
|
@ -5699,11 +5697,11 @@ proof -
|
|
|
|
|
using wellformed_h2 by (simp add: heap_is_wellformed_def)
|
|
|
|
|
then have "a_owner_document_valid h'"
|
|
|
|
|
apply(auto simp add: a_owner_document_valid_def object_ptr_kinds_M_eq2_h2
|
|
|
|
|
object_ptr_kinds_M_eq2_h3 node_ptr_kinds_eq2_h2 node_ptr_kinds_eq2_h3
|
|
|
|
|
document_ptr_kinds_eq2_h2 document_ptr_kinds_eq2_h3 children_eq2_h2)[1]
|
|
|
|
|
object_ptr_kinds_M_eq2_h3 node_ptr_kinds_eq2_h2 node_ptr_kinds_eq2_h3
|
|
|
|
|
document_ptr_kinds_eq2_h2 document_ptr_kinds_eq2_h3 children_eq2_h2)[1]
|
|
|
|
|
apply(auto simp add: document_ptr_kinds_eq2_h2[simplified] document_ptr_kinds_eq2_h3[simplified]
|
|
|
|
|
object_ptr_kinds_M_eq2_h2[simplified] object_ptr_kinds_M_eq2_h3[simplified]
|
|
|
|
|
node_ptr_kinds_eq2_h2[simplified] node_ptr_kinds_eq2_h3[simplified])[1]
|
|
|
|
|
object_ptr_kinds_M_eq2_h2[simplified] object_ptr_kinds_M_eq2_h3[simplified]
|
|
|
|
|
node_ptr_kinds_eq2_h2[simplified] node_ptr_kinds_eq2_h3[simplified])[1]
|
|
|
|
|
apply(auto simp add: disconnected_nodes_eq2_h3[symmetric])[1]
|
|
|
|
|
by (smt children_eq2_h3 children_h' children_h3 disconnected_nodes_eq2_h2 disconnected_nodes_h2 disconnected_nodes_h3 finite_set_in in_set_remove1 insert_before_list_in_set object_ptr_kinds_M_eq3_h' ptr_in_heap select_result_I2)
|
|
|
|
|
|
|
|
|
|
@ -6182,7 +6180,9 @@ proof -
|
|
|
|
|
by auto
|
|
|
|
|
obtain parent_opt where
|
|
|
|
|
parent_opt: "h \<turnstile> get_parent child \<rightarrow>\<^sub>r parent_opt"
|
|
|
|
|
by (meson assms(2) assms(3) is_OK_returns_result_I l_get_owner_document.get_owner_document_ptr_in_heap local.get_parent_ok local.l_get_owner_document_axioms node_ptr_kinds_commutes old_document returns_result_select_result)
|
|
|
|
|
by (meson assms(2) assms(3) is_OK_returns_result_I l_get_owner_document.get_owner_document_ptr_in_heap
|
|
|
|
|
local.get_parent_ok local.l_get_owner_document_axioms node_ptr_kinds_commutes old_document
|
|
|
|
|
returns_result_select_result)
|
|
|
|
|
then have "h \<turnstile> ok (get_parent child)"
|
|
|
|
|
by auto
|
|
|
|
|
|
|
|
|
|
@ -6409,7 +6409,8 @@ proof -
|
|
|
|
|
|
|
|
|
|
obtain h2 where
|
|
|
|
|
h2: "h \<turnstile> adopt_node owner_document node \<rightarrow>\<^sub>h h2"
|
|
|
|
|
by (meson assms(1) assms(2) assms(3) assms(5) is_OK_returns_heap_E adopt_node_ok l_insert_before_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms local.get_owner_document_owner_document_in_heap owner_document)
|
|
|
|
|
by (meson assms(1) assms(2) assms(3) assms(5) is_OK_returns_heap_E adopt_node_ok l_insert_before_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms
|
|
|
|
|
local.get_owner_document_owner_document_in_heap owner_document)
|
|
|
|
|
then have "h \<turnstile> ok (adopt_node owner_document node)"
|
|
|
|
|
by auto
|
|
|
|
|
have "object_ptr_kinds h = object_ptr_kinds h2"
|
|
|
|
|
@ -6972,8 +6973,18 @@ proof -
|
|
|
|
|
ultimately show "False"
|
|
|
|
|
apply(-)
|
|
|
|
|
apply(cases "x = document_ptr")
|
|
|
|
|
apply (smt NodeMonad.ptr_kinds_ptr_kinds_M \<open>cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^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 new_element_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close> \<open>local.a_all_ptrs_in_heap h\<close> disc_nodes_h3 disconnected_nodes_eq2_h disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 disjoint_iff_not_equal document_ptr_kinds_eq_h document_ptr_kinds_eq_h2 finite_set_in h' l_set_disconnected_nodes_get_disconnected_nodes.set_disconnected_nodes_get_disconnected_nodes local.a_all_ptrs_in_heap_def local.l_set_disconnected_nodes_get_disconnected_nodes_axioms select_result_I2 set_ConsD subsetD)
|
|
|
|
|
by (smt NodeMonad.ptr_kinds_ptr_kinds_M \<open>cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^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 new_element_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close> \<open>local.a_all_ptrs_in_heap h\<close> disc_nodes_document_ptr_h2 disconnected_nodes_eq2_h disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 disjoint_iff_not_equal document_ptr_kinds_eq_h document_ptr_kinds_eq_h2 finite_set_in h' l_set_disconnected_nodes_get_disconnected_nodes.set_disconnected_nodes_get_disconnected_nodes local.a_all_ptrs_in_heap_def local.l_set_disconnected_nodes_get_disconnected_nodes_axioms select_result_I2 set_ConsD subsetD)
|
|
|
|
|
apply (smt NodeMonad.ptr_kinds_ptr_kinds_M \<open>cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^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 new_element_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close> \<open>local.a_all_ptrs_in_heap h\<close>
|
|
|
|
|
disc_nodes_h3 disconnected_nodes_eq2_h disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3
|
|
|
|
|
disjoint_iff_not_equal document_ptr_kinds_eq_h document_ptr_kinds_eq_h2 finite_set_in h'
|
|
|
|
|
l_set_disconnected_nodes_get_disconnected_nodes.set_disconnected_nodes_get_disconnected_nodes
|
|
|
|
|
local.a_all_ptrs_in_heap_def local.l_set_disconnected_nodes_get_disconnected_nodes_axioms
|
|
|
|
|
select_result_I2 set_ConsD subsetD)
|
|
|
|
|
by (smt NodeMonad.ptr_kinds_ptr_kinds_M \<open>cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^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 new_element_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close> \<open>local.a_all_ptrs_in_heap h\<close>
|
|
|
|
|
disc_nodes_document_ptr_h2 disconnected_nodes_eq2_h disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3
|
|
|
|
|
disjoint_iff_not_equal document_ptr_kinds_eq_h document_ptr_kinds_eq_h2 finite_set_in h'
|
|
|
|
|
l_set_disconnected_nodes_get_disconnected_nodes.set_disconnected_nodes_get_disconnected_nodes
|
|
|
|
|
local.a_all_ptrs_in_heap_def local.l_set_disconnected_nodes_get_disconnected_nodes_axioms
|
|
|
|
|
select_result_I2 set_ConsD subsetD)
|
|
|
|
|
next
|
|
|
|
|
fix x xa xb
|
|
|
|
|
assume 2: "(\<Union>x\<in>fset (object_ptr_kinds h3). set |h' \<turnstile> get_child_nodes x|\<^sub>r)
|
|
|
|
|
@ -7338,15 +7349,23 @@ proof -
|
|
|
|
|
apply(auto simp add: a_all_ptrs_in_heap_def)[1]
|
|
|
|
|
using node_ptr_kinds_eq_h \<open>cast new_character_data_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close>
|
|
|
|
|
\<open>h2 \<turnstile> get_child_nodes (cast new_character_data_ptr) \<rightarrow>\<^sub>r []\<close>
|
|
|
|
|
apply (metis (no_types, lifting) NodeMonad.ptr_kinds_ptr_kinds_M \<open>parent_child_rel h = parent_child_rel h2\<close> children_eq2_h finite_set_in finsert_iff funion_finsert_right local.parent_child_rel_child local.parent_child_rel_parent_in_heap node_ptr_kinds_commutes object_ptr_kinds_eq_h select_result_I2 subsetD sup_bot.right_neutral)
|
|
|
|
|
by (metis assms(1) assms(3) disconnected_nodes_eq2_h document_ptr_kinds_eq_h funionI1 local.get_disconnected_nodes_ok local.heap_is_wellformed_disc_nodes_in_heap node_ptr_kinds_eq_h returns_result_select_result)
|
|
|
|
|
|
|
|
|
|
apply (metis (no_types, lifting) NodeMonad.ptr_kinds_ptr_kinds_M \<open>parent_child_rel h = parent_child_rel h2\<close>
|
|
|
|
|
children_eq2_h finite_set_in finsert_iff funion_finsert_right local.parent_child_rel_child
|
|
|
|
|
local.parent_child_rel_parent_in_heap node_ptr_kinds_commutes object_ptr_kinds_eq_h
|
|
|
|
|
select_result_I2 subsetD sup_bot.right_neutral)
|
|
|
|
|
by (metis assms(1) assms(3) disconnected_nodes_eq2_h document_ptr_kinds_eq_h funionI1
|
|
|
|
|
local.get_disconnected_nodes_ok local.heap_is_wellformed_disc_nodes_in_heap
|
|
|
|
|
node_ptr_kinds_eq_h returns_result_select_result)
|
|
|
|
|
then have "a_all_ptrs_in_heap h3"
|
|
|
|
|
by (simp add: children_eq2_h2 disconnected_nodes_eq2_h2 document_ptr_kinds_eq_h2 local.a_all_ptrs_in_heap_def node_ptr_kinds_eq_h2 object_ptr_kinds_eq_h2)
|
|
|
|
|
by (simp add: children_eq2_h2 disconnected_nodes_eq2_h2 document_ptr_kinds_eq_h2
|
|
|
|
|
local.a_all_ptrs_in_heap_def node_ptr_kinds_eq_h2 object_ptr_kinds_eq_h2)
|
|
|
|
|
then have "a_all_ptrs_in_heap h'"
|
|
|
|
|
by (smt character_data_ptr_kinds_commutes children_eq2_h3 disc_nodes_document_ptr_h2 disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 document_ptr_kinds_eq_h3 finite_set_in h' h2 local.a_all_ptrs_in_heap_def local.set_disconnected_nodes_get_disconnected_nodes new_character_data_ptr new_character_data_ptr_in_heap node_ptr_kinds_eq_h2 node_ptr_kinds_eq_h3 object_ptr_kinds_eq_h3 select_result_I2 set_ConsD subset_code(1))
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
by (smt character_data_ptr_kinds_commutes children_eq2_h3 disc_nodes_document_ptr_h2
|
|
|
|
|
disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 document_ptr_kinds_eq_h3
|
|
|
|
|
finite_set_in h' h2 local.a_all_ptrs_in_heap_def
|
|
|
|
|
local.set_disconnected_nodes_get_disconnected_nodes new_character_data_ptr
|
|
|
|
|
new_character_data_ptr_in_heap node_ptr_kinds_eq_h2 node_ptr_kinds_eq_h3
|
|
|
|
|
object_ptr_kinds_eq_h3 select_result_I2 set_ConsD subset_code(1))
|
|
|
|
|
have "\<And>p. p |\<in>| object_ptr_kinds h \<Longrightarrow> cast new_character_data_ptr \<notin> set |h \<turnstile> get_child_nodes p|\<^sub>r"
|
|
|
|
|
using \<open>heap_is_wellformed h\<close> \<open>cast new_character_data_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close>
|
|
|
|
|
heap_is_wellformed_children_in_heap
|
|
|
|
|
@ -7409,7 +7428,13 @@ proof -
|
|
|
|
|
moreover have "set |h3 \<turnstile> get_disconnected_nodes x|\<^sub>r \<inter> set |h3 \<turnstile> get_disconnected_nodes y|\<^sub>r = {}"
|
|
|
|
|
using calculation by(auto dest: distinct_concat_map_E(1))
|
|
|
|
|
ultimately show "False"
|
|
|
|
|
by (smt NodeMonad.ptr_kinds_ptr_kinds_M \<open>cast\<^sub>c\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>_\<^sub>d\<^sub>a\<^sub>t\<^sub>a\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_character_data_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close> \<open>local.a_all_ptrs_in_heap h\<close> disc_nodes_document_ptr_h2 disconnected_nodes_eq2_h disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 disjoint_iff_not_equal document_ptr_kinds_eq_h document_ptr_kinds_eq_h2 finite_set_in h' l_set_disconnected_nodes_get_disconnected_nodes.set_disconnected_nodes_get_disconnected_nodes local.a_all_ptrs_in_heap_def local.l_set_disconnected_nodes_get_disconnected_nodes_axioms select_result_I2 set_ConsD subsetD)
|
|
|
|
|
by (smt NodeMonad.ptr_kinds_ptr_kinds_M \<open>cast\<^sub>c\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>_\<^sub>d\<^sub>a\<^sub>t\<^sub>a\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_character_data_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close>
|
|
|
|
|
\<open>local.a_all_ptrs_in_heap h\<close> disc_nodes_document_ptr_h2 disconnected_nodes_eq2_h
|
|
|
|
|
disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 disjoint_iff_not_equal
|
|
|
|
|
document_ptr_kinds_eq_h document_ptr_kinds_eq_h2 finite_set_in h'
|
|
|
|
|
l_set_disconnected_nodes_get_disconnected_nodes.set_disconnected_nodes_get_disconnected_nodes
|
|
|
|
|
local.a_all_ptrs_in_heap_def local.l_set_disconnected_nodes_get_disconnected_nodes_axioms
|
|
|
|
|
select_result_I2 set_ConsD subsetD)
|
|
|
|
|
next
|
|
|
|
|
fix x xa xb
|
|
|
|
|
assume 2: "(\<Union>x\<in>fset (object_ptr_kinds h3). set |h' \<turnstile> get_child_nodes x|\<^sub>r)
|
|
|
|
|
@ -7445,7 +7470,12 @@ proof -
|
|
|
|
|
apply (metis (no_types, lifting) document_ptr_kinds_eq_h h' list.set_intros(1)
|
|
|
|
|
local.set_disconnected_nodes_get_disconnected_nodes select_result_I2)
|
|
|
|
|
apply(simp add: object_ptr_kinds_eq_h)
|
|
|
|
|
by (metis (mono_tags, lifting) \<open>cast\<^sub>c\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>_\<^sub>d\<^sub>a\<^sub>t\<^sub>a\<^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 new_character_data_ptr \<notin> set |h \<turnstile> object_ptr_kinds_M|\<^sub>r\<close> children_eq2_h disconnected_nodes_eq2_h3 document_ptr_kinds_eq_h finite_set_in h' l_ptr_kinds_M.ptr_kinds_ptr_kinds_M l_set_disconnected_nodes_get_disconnected_nodes.set_disconnected_nodes_get_disconnected_nodes list.set_intros(2) local.l_set_disconnected_nodes_get_disconnected_nodes_axioms object_ptr_kinds_M_def select_result_I2)
|
|
|
|
|
by (metis (mono_tags, lifting) \<open>cast\<^sub>c\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>_\<^sub>d\<^sub>a\<^sub>t\<^sub>a\<^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 new_character_data_ptr \<notin> set |h \<turnstile> object_ptr_kinds_M|\<^sub>r\<close>
|
|
|
|
|
children_eq2_h disconnected_nodes_eq2_h3 document_ptr_kinds_eq_h finite_set_in h'
|
|
|
|
|
l_ptr_kinds_M.ptr_kinds_ptr_kinds_M
|
|
|
|
|
l_set_disconnected_nodes_get_disconnected_nodes.set_disconnected_nodes_get_disconnected_nodes
|
|
|
|
|
list.set_intros(2) local.l_set_disconnected_nodes_get_disconnected_nodes_axioms object_ptr_kinds_M_def
|
|
|
|
|
select_result_I2)
|
|
|
|
|
|
|
|
|
|
have "known_ptr (cast new_character_data_ptr)"
|
|
|
|
|
using \<open>h \<turnstile> create_character_data document_ptr text \<rightarrow>\<^sub>r new_character_data_ptr\<close> local.create_character_data_known_ptr by blast
|
|
|
|
|
@ -7568,7 +7598,7 @@ proof -
|
|
|
|
|
"\<And>doc_ptr disc_nodes. doc_ptr \<noteq> new_document_ptr
|
|
|
|
|
\<Longrightarrow> h \<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 h' get_disconnected_nodes_new_document_different_pointers new_document_ptr
|
|
|
|
|
apply(auto simp add: reads_def reflp_def transp_def preserved_def)[1]
|
|
|
|
|
apply(auto simp add: reads_def reflp_def transp_def preserved_def)[1]
|
|
|
|
|
by (metis(full_types) \<open>\<And>thesis. (\<And>new_document_ptr.
|
|
|
|
|
\<lbrakk>h \<turnstile> new_document \<rightarrow>\<^sub>r new_document_ptr; h \<turnstile> new_document \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close>
|
|
|
|
|
local.get_disconnected_nodes_new_document_different_pointers new_document_ptr)+
|
|
|
|
|
@ -7618,16 +7648,20 @@ proof -
|
|
|
|
|
|
|
|
|
|
have "a_all_ptrs_in_heap h"
|
|
|
|
|
using \<open>heap_is_wellformed h\<close> by (simp add: heap_is_wellformed_def)
|
|
|
|
|
then have "a_all_ptrs_in_heap h'"
|
|
|
|
|
then have "a_all_ptrs_in_heap h'"
|
|
|
|
|
apply(auto simp add: a_all_ptrs_in_heap_def)[1]
|
|
|
|
|
using ObjectMonad.ptr_kinds_ptr_kinds_M
|
|
|
|
|
\<open>cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^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 new_document_ptr \<notin> set |h \<turnstile> object_ptr_kinds_M|\<^sub>r\<close>
|
|
|
|
|
\<open>parent_child_rel h = parent_child_rel h'\<close> assms(1) children_eq fset_of_list_elem
|
|
|
|
|
local.heap_is_wellformed_children_in_heap local.parent_child_rel_child
|
|
|
|
|
local.parent_child_rel_parent_in_heap node_ptr_kinds_eq
|
|
|
|
|
apply (metis (no_types, lifting) \<open>h' \<turnstile> get_child_nodes (cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^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 new_document_ptr) \<rightarrow>\<^sub>r []\<close> children_eq2 finite_set_in finsert_iff funion_finsert_right object_ptr_kinds_eq select_result_I2 subsetD sup_bot.right_neutral)
|
|
|
|
|
by (metis (no_types, lifting) \<open>cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^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 new_document_ptr |\<notin>| object_ptr_kinds h\<close> \<open>h' \<turnstile> get_child_nodes (cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^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 new_document_ptr) \<rightarrow>\<^sub>r []\<close> \<open>h' \<turnstile> get_disconnected_nodes new_document_ptr \<rightarrow>\<^sub>r []\<close> \<open>parent_child_rel h = parent_child_rel h'\<close> \<open>type_wf h'\<close> assms(1) disconnected_nodes_eq_h local.get_disconnected_nodes_ok local.heap_is_wellformed_disc_nodes_in_heap local.parent_child_rel_child local.parent_child_rel_parent_in_heap node_ptr_kinds_eq returns_result_select_result select_result_I2)
|
|
|
|
|
|
|
|
|
|
using ObjectMonad.ptr_kinds_ptr_kinds_M
|
|
|
|
|
\<open>cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^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 new_document_ptr \<notin> set |h \<turnstile> object_ptr_kinds_M|\<^sub>r\<close>
|
|
|
|
|
\<open>parent_child_rel h = parent_child_rel h'\<close> assms(1) children_eq fset_of_list_elem
|
|
|
|
|
local.heap_is_wellformed_children_in_heap local.parent_child_rel_child
|
|
|
|
|
local.parent_child_rel_parent_in_heap node_ptr_kinds_eq
|
|
|
|
|
apply (metis (no_types, lifting) \<open>h' \<turnstile> get_child_nodes (cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^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 new_document_ptr) \<rightarrow>\<^sub>r []\<close>
|
|
|
|
|
children_eq2 finite_set_in finsert_iff funion_finsert_right object_ptr_kinds_eq select_result_I2 subsetD sup_bot.right_neutral)
|
|
|
|
|
by (metis (no_types, lifting) \<open>cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^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 new_document_ptr |\<notin>| object_ptr_kinds h\<close>
|
|
|
|
|
\<open>h' \<turnstile> get_child_nodes (cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^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 new_document_ptr) \<rightarrow>\<^sub>r []\<close>
|
|
|
|
|
\<open>h' \<turnstile> get_disconnected_nodes new_document_ptr \<rightarrow>\<^sub>r []\<close> \<open>parent_child_rel h = parent_child_rel h'\<close> \<open>type_wf h'\<close> assms(1) disconnected_nodes_eq_h local.get_disconnected_nodes_ok
|
|
|
|
|
local.heap_is_wellformed_disc_nodes_in_heap local.parent_child_rel_child local.parent_child_rel_parent_in_heap
|
|
|
|
|
node_ptr_kinds_eq returns_result_select_result select_result_I2)
|
|
|
|
|
have "a_distinct_lists h"
|
|
|
|
|
using \<open>heap_is_wellformed h\<close>
|
|
|
|
|
by (simp add: heap_is_wellformed_def)
|
|
|
|
|
@ -7695,8 +7729,8 @@ proof -
|
|
|
|
|
using \<open>heap_is_wellformed h\<close> by (simp add: heap_is_wellformed_def)
|
|
|
|
|
then have "a_owner_document_valid h'"
|
|
|
|
|
apply(auto simp add: a_owner_document_valid_def)[1]
|
|
|
|
|
by (metis \<open>cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^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 new_document_ptr |\<notin>| object_ptr_kinds h\<close> children_eq2 disconnected_nodes_eq2_h document_ptr_kinds_commutes finite_set_in funion_iff node_ptr_kinds_eq object_ptr_kinds_eq)
|
|
|
|
|
|
|
|
|
|
by (metis \<open>cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^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 new_document_ptr |\<notin>| object_ptr_kinds h\<close>
|
|
|
|
|
children_eq2 disconnected_nodes_eq2_h document_ptr_kinds_commutes finite_set_in funion_iff node_ptr_kinds_eq object_ptr_kinds_eq)
|
|
|
|
|
show "heap_is_wellformed h'"
|
|
|
|
|
using \<open>a_acyclic_heap h'\<close> \<open>a_all_ptrs_in_heap h'\<close> \<open>a_distinct_lists h'\<close> \<open>a_owner_document_valid h'\<close>
|
|
|
|
|
by(simp add: heap_is_wellformed_def)
|
|
|
|
|
|
Achim D. Brucker