forked from afp-mirror/Core_DOM
Restrict auto.
This commit is contained in:
parent
0d7ed5df29
commit
7563d9696e
|
|
@ -56,7 +56,7 @@ definition a_owner_document_valid :: "(_) heap \<Rightarrow> bool"
|
|||
lemma a_owner_document_valid_code [code]: "a_owner_document_valid h \<longleftrightarrow> node_ptr_kinds h |\<subseteq>|
|
||||
fset_of_list (concat (map (\<lambda>parent. |h \<turnstile> get_child_nodes parent|\<^sub>r) (sorted_list_of_fset (object_ptr_kinds h)) @ map (\<lambda>parent. |h \<turnstile> get_disconnected_nodes parent|\<^sub>r) (sorted_list_of_fset (document_ptr_kinds h))))
|
||||
"
|
||||
apply(auto simp add: a_owner_document_valid_def l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.a_owner_document_valid_def)
|
||||
apply(auto simp add: a_owner_document_valid_def l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.a_owner_document_valid_def)[1]
|
||||
proof -
|
||||
fix x
|
||||
assume 1: " \<forall>node_ptr\<in>fset (node_ptr_kinds h).
|
||||
|
|
@ -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
|
||||
|
||||
|
|
@ -2686,7 +2681,7 @@ lemma get_owner_document_owner_document_in_heap:
|
|||
assumes "h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document"
|
||||
shows "owner_document |\<in>| document_ptr_kinds h"
|
||||
using assms
|
||||
apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def)
|
||||
apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def)[1]
|
||||
apply(split invoke_split_asm)+
|
||||
proof -
|
||||
assume "h \<turnstile> invoke [] ptr () \<rightarrow>\<^sub>r owner_document"
|
||||
|
|
@ -2748,9 +2743,10 @@ next
|
|||
then have "some_owner_document \<in> set candidates"
|
||||
apply(rule filter_M_in_result_if_ok)
|
||||
using \<open>some_owner_document |\<in>| document_ptr_kinds h\<close> \<open>root \<in> cast ` set |h \<turnstile> get_disconnected_nodes some_owner_document|\<^sub>r\<close>
|
||||
apply(auto intro!: bind_pure_I bind_pure_returns_result_I)
|
||||
by (simp add: "1" local.get_disconnected_nodes_ok)
|
||||
|
||||
apply(auto intro!: bind_pure_I bind_pure_returns_result_I)[1]
|
||||
apply (simp add: \<open>some_owner_document |\<in>| document_ptr_kinds h\<close>)
|
||||
using "1" \<open>root \<in> cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ` set |h \<turnstile> get_disconnected_nodes some_owner_document|\<^sub>r\<close> \<open>some_owner_document |\<in>| document_ptr_kinds h\<close>
|
||||
local.get_disconnected_nodes_ok by auto
|
||||
then have "candidates \<noteq> []"
|
||||
by auto
|
||||
then have "owner_document \<in> set candidates"
|
||||
|
|
@ -2838,17 +2834,28 @@ proof -
|
|||
using assms(2) assms(4) local.known_ptrs_known_ptr
|
||||
by blast
|
||||
then show ?thesis
|
||||
apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def)
|
||||
apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def)[1]
|
||||
apply(split invoke_splits, (rule conjI | rule impI)+)+
|
||||
apply(auto simp add: known_ptr_impl)[1]
|
||||
using NodeClass.a_known_ptr_def known_ptr_not_character_data_ptr known_ptr_not_document_ptr known_ptr_not_element_ptr apply blast
|
||||
using NodeClass.a_known_ptr_def known_ptr_not_character_data_ptr known_ptr_not_document_ptr known_ptr_not_element_ptr
|
||||
apply blast
|
||||
using assms(4)
|
||||
apply(auto simp add: a_get_owner_document\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def intro!: bind_is_OK_pure_I)
|
||||
apply(auto simp add: a_get_owner_document\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def intro!: bind_is_OK_pure_I)[1]
|
||||
apply (metis (no_types, lifting) document_ptr_casts_commute3 document_ptr_kinds_commutes is_document_ptr_kind_none option.case_eq_if)
|
||||
using assms(4)
|
||||
apply(auto simp add: a_get_owner_document\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def intro!: bind_is_OK_pure_I)[1]
|
||||
apply (metis (no_types, lifting) assms(1) assms(2) assms(3) is_node_ptr_kind_none local.get_root_node_ok node_ptr_casts_commute3 option.case_eq_if)
|
||||
apply(auto split: option.splits intro!: bind_is_OK_pure_I filter_M_pure_I bind_pure_I filter_M_is_OK_I)
|
||||
using assms(3) local.get_disconnected_nodes_ok apply blast
|
||||
using assms(4)
|
||||
apply(auto simp add: a_get_owner_document\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def intro!: bind_is_OK_pure_I)[1]
|
||||
apply(auto split: option.splits intro!: bind_is_OK_pure_I filter_M_pure_I bind_pure_I filter_M_is_OK_I)[1]
|
||||
using assms(3) local.get_disconnected_nodes_ok
|
||||
apply blast
|
||||
apply (simp add: assms(1) assms(2) assms(3) local.get_root_node_ok)
|
||||
using assms(4)
|
||||
apply(auto simp add: a_get_owner_document\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def intro!: bind_is_OK_pure_I)[1]
|
||||
apply(auto split: option.splits intro!: bind_is_OK_pure_I filter_M_pure_I bind_pure_I filter_M_is_OK_I)[1]
|
||||
apply (simp add: assms(1) assms(2) assms(3) local.get_root_node_ok)[1]
|
||||
apply(auto split: option.splits intro!: bind_is_OK_pure_I filter_M_pure_I bind_pure_I filter_M_is_OK_I)[1]
|
||||
using assms(3) local.get_disconnected_nodes_ok by blast
|
||||
qed
|
||||
|
||||
|
|
@ -2885,11 +2892,11 @@ proof -
|
|||
|
||||
then have "h \<turnstile> 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 document_ptr () \<rightarrow>\<^sub>r owner_document \<longleftrightarrow> h \<turnstile> a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r child () \<rightarrow>\<^sub>r owner_document"
|
||||
using document_ptr \<open>h \<turnstile> get_root_node (cast child) \<rightarrow>\<^sub>r root\<close>[simplified \<open>root = cast document_ptr\<close> document_ptr]
|
||||
apply(auto simp add: a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def a_get_owner_document\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def elim!: bind_returns_result_E2 dest!: bind_returns_result_E3[rotated, OF \<open>h \<turnstile> get_root_node (cast child) \<rightarrow>\<^sub>r root\<close>[simplified \<open>root = cast document_ptr\<close> document_ptr], rotated] intro!: bind_pure_returns_result_I filter_M_pure_I bind_pure_I split: if_splits option.splits)
|
||||
apply(auto simp add: a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def a_get_owner_document\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def elim!: bind_returns_result_E2 dest!: bind_returns_result_E3[rotated, OF \<open>h \<turnstile> get_root_node (cast child) \<rightarrow>\<^sub>r root\<close>[simplified \<open>root = cast document_ptr\<close> document_ptr], rotated] intro!: bind_pure_returns_result_I filter_M_pure_I bind_pure_I split: if_splits option.splits)[1]
|
||||
using \<open>ptr |\<in>| object_ptr_kinds h\<close> document_ptr_kinds_commutes by blast
|
||||
then show ?thesis
|
||||
using \<open>known_ptr ptr\<close>
|
||||
apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def known_ptr_impl)
|
||||
apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def known_ptr_impl)[1]
|
||||
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)
|
||||
|
|
@ -2915,21 +2922,36 @@ proof -
|
|||
apply(drule(1) known_ptr_not_element_ptr)
|
||||
apply(simp add: NodeClass.known_ptr_defs)
|
||||
using \<open>cast child |\<in>| object_ptr_kinds h\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close> False
|
||||
apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )
|
||||
apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )[1]
|
||||
using \<open>cast child |\<in>| object_ptr_kinds h\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close> False
|
||||
apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )[1]
|
||||
using \<open>cast child |\<in>| object_ptr_kinds h\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close> False
|
||||
apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )[1]
|
||||
using \<open>cast child |\<in>| object_ptr_kinds h\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close> False
|
||||
apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )[1]
|
||||
apply(split invoke_splits, ((rule conjI | rule impI)+)?)+
|
||||
apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )
|
||||
by (meson invoke_empty is_OK_returns_result_I)
|
||||
apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )[1]
|
||||
apply (meson invoke_empty is_OK_returns_result_I)
|
||||
apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )[1]
|
||||
apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )[1]
|
||||
by(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )[1]
|
||||
qed
|
||||
then show ?thesis
|
||||
using \<open>known_ptr (cast child)\<close>
|
||||
apply(auto simp add: get_owner_document_def[of "cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r child"] a_get_owner_document_tups_def known_ptr_impl)
|
||||
apply(auto simp add: get_owner_document_def[of "cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r child"] a_get_owner_document_tups_def known_ptr_impl)[1]
|
||||
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)
|
||||
using \<open>cast child |\<in>| object_ptr_kinds h\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close>
|
||||
apply(auto intro!: bind_pure_returns_result_I split: option.splits)
|
||||
apply(auto intro!: bind_pure_returns_result_I split: option.splits)[1]
|
||||
using \<open>cast child |\<in>| object_ptr_kinds h\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close>
|
||||
apply(auto intro!: bind_pure_returns_result_I split: option.splits)[1]
|
||||
using \<open>cast child |\<in>| object_ptr_kinds h\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close>
|
||||
apply(auto intro!: bind_pure_returns_result_I split: option.splits)[1]
|
||||
using \<open>cast child |\<in>| object_ptr_kinds h\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close>
|
||||
apply(auto intro!: bind_pure_returns_result_I split: option.splits)[1]
|
||||
by (smt \<open>cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r child |\<in>| object_ptr_kinds h\<close> cast_document_ptr_not_node_ptr(1) comp_apply invoke_empty invoke_not invoke_returns_result is_OK_returns_result_I node_ptr_casts_commute2 option.sel)
|
||||
qed
|
||||
|
||||
|
|
@ -2970,7 +2992,7 @@ lemma get_owner_document_wf_is_l_get_owner_document_wf [instances]:
|
|||
"l_get_owner_document_wf heap_is_wellformed type_wf known_ptr known_ptrs get_disconnected_nodes
|
||||
get_owner_document get_parent get_child_nodes"
|
||||
using known_ptrs_is_l_known_ptrs
|
||||
apply(auto simp add: l_get_owner_document_wf_def l_get_owner_document_wf_axioms_def)
|
||||
apply(auto simp add: l_get_owner_document_wf_def l_get_owner_document_wf_axioms_def)[1]
|
||||
using get_owner_document_disconnected_nodes apply fast
|
||||
using in_disconnected_nodes_no_parent apply fast
|
||||
using get_owner_document_owner_document_in_heap apply fast
|
||||
|
|
@ -3006,7 +3028,7 @@ proof -
|
|||
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(auto simp add: known_ptr_impl get_owner_document_def a_get_owner_document_tups_def)[1]
|
||||
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)
|
||||
|
|
@ -3054,7 +3076,7 @@ proof -
|
|||
then
|
||||
have "ptr = root"
|
||||
using assms(4)
|
||||
apply(auto simp add: get_root_node_def elim!: bind_returns_result_E2)
|
||||
apply(auto simp add: get_root_node_def elim!: bind_returns_result_E2)[1]
|
||||
by (metis document_ptr_casts_commute3 last_ConsL local.get_ancestors_not_node node_ptr_no_document_ptr_cast)
|
||||
then show ?thesis
|
||||
by auto
|
||||
|
|
@ -3070,7 +3092,7 @@ proof -
|
|||
assume "h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document"
|
||||
then have "h \<turnstile> local.a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r node_ptr () \<rightarrow>\<^sub>r owner_document"
|
||||
using node_ptr
|
||||
apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def)
|
||||
apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def)[1]
|
||||
apply(split invoke_splits)+
|
||||
apply (meson invoke_empty is_OK_returns_result_I)
|
||||
by(auto elim!: bind_returns_result_E2 split: option.splits)
|
||||
|
|
@ -3584,7 +3606,6 @@ 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
|
||||
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'"
|
||||
|
|
@ -3943,7 +3964,7 @@ proof -
|
|||
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF remove_child_writes assms(2)]
|
||||
using set_child_nodes_types_preserved set_disconnected_nodes_types_preserved type_wf
|
||||
unfolding remove_child_locs_def
|
||||
apply(auto simp add: reflp_def transp_def)
|
||||
apply(auto simp add: reflp_def transp_def)[1]
|
||||
by blast
|
||||
ultimately show ?thesis
|
||||
using remove_child_removes_parent remove_child_heap_is_wellformed_preserved child_parent_dual
|
||||
|
|
@ -4539,7 +4560,13 @@ proof -
|
|||
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
|
||||
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) 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))
|
||||
|
||||
have a_distinct_lists_h2: "a_distinct_lists h2"
|
||||
using wellformed_h2 by (simp add: heap_is_wellformed_def)
|
||||
|
|
@ -5262,8 +5289,6 @@ proof -
|
|||
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]
|
||||
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
|
||||
|
|
@ -5660,7 +5685,7 @@ interpretation i_append_child_wf?: l_append_child_wf\<^sub>C\<^sub>o\<^sub>r\<^s
|
|||
by(auto simp add: l_append_child_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
|
||||
|
||||
lemma append_child_wf_is_l_append_child_wf [instances]: "l_append_child_wf type_wf known_ptr known_ptrs append_child heap_is_wellformed"
|
||||
apply(auto simp add: l_append_child_wf_def l_append_child_wf_axioms_def instances)
|
||||
apply(auto simp add: l_append_child_wf_def l_append_child_wf_axioms_def instances)[1]
|
||||
using append_child_heap_is_wellformed_preserved by fast+
|
||||
|
||||
|
||||
|
|
@ -5718,7 +5743,7 @@ proof -
|
|||
elim!: bind_returns_heap_E
|
||||
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(auto simp add: create_element_def intro!: bind_returns_result_I)[1]
|
||||
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)
|
||||
|
|
@ -5984,8 +6009,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)
|
||||
|
|
@ -6344,15 +6379,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
|
||||
|
|
@ -6415,7 +6458,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)
|
||||
|
|
@ -6451,7 +6500,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)
|
||||
|
||||
|
||||
show "heap_is_wellformed h'"
|
||||
|
|
@ -6619,9 +6673,13 @@ proof -
|
|||
\<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)
|
||||
|
||||
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)
|
||||
|
|
@ -6689,8 +6747,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)
|
||||
|
|
|
|||
Reference in New Issue