forked from afp-mirror/Core_DOM
Added insert_before_ok and related lemmas.
This commit is contained in:
Michael Herzberg
parent
9197e60e25
commit
342cac360e
|
|
@ -620,6 +620,60 @@ lemma set_child_nodes_get_child_nodes_different_pointers:
|
|||
apply(rule is_element_ptr_kind_obtains)
|
||||
apply(auto)
|
||||
done
|
||||
|
||||
lemma set_child_nodes_element_ok [simp]:
|
||||
assumes "known_ptr ptr"
|
||||
assumes "type_wf h"
|
||||
assumes "ptr |\<in>| object_ptr_kinds h"
|
||||
assumes "is_element_ptr_kind ptr"
|
||||
shows "h \<turnstile> ok (set_child_nodes ptr children)"
|
||||
proof -
|
||||
have "is_element_ptr ptr"
|
||||
using \<open>known_ptr ptr\<close> assms(4)
|
||||
by(auto simp add: known_ptr_impl known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)
|
||||
then show ?thesis
|
||||
using assms
|
||||
apply(auto simp add: set_child_nodes_def a_set_child_nodes_tups_def set_child_nodes\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def split: option.splits)
|
||||
by (simp add: DocumentMonad.put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ok local.type_wf_impl)
|
||||
qed
|
||||
|
||||
lemma set_child_nodes_document1_ok [simp]:
|
||||
assumes "known_ptr ptr"
|
||||
assumes "type_wf h"
|
||||
assumes "ptr |\<in>| object_ptr_kinds h"
|
||||
assumes "is_document_ptr_kind ptr"
|
||||
assumes "children = []"
|
||||
shows "h \<turnstile> ok (set_child_nodes ptr children)"
|
||||
proof -
|
||||
have "is_document_ptr ptr"
|
||||
using \<open>known_ptr ptr\<close> assms(4)
|
||||
by(auto simp add: known_ptr_impl known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)
|
||||
then show ?thesis
|
||||
using assms
|
||||
apply(auto simp add: set_child_nodes_def a_set_child_nodes_tups_def set_child_nodes\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def split: option.splits)
|
||||
by (simp add: DocumentMonad.put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ok local.type_wf_impl)
|
||||
qed
|
||||
|
||||
lemma set_child_nodes_document2_ok [simp]:
|
||||
assumes "known_ptr ptr"
|
||||
assumes "type_wf h"
|
||||
assumes "ptr |\<in>| object_ptr_kinds h"
|
||||
assumes "is_document_ptr_kind ptr"
|
||||
assumes "children = [child]"
|
||||
assumes "is_element_ptr_kind child"
|
||||
shows "h \<turnstile> ok (set_child_nodes ptr children)"
|
||||
proof -
|
||||
have "is_document_ptr ptr"
|
||||
using \<open>known_ptr ptr\<close> assms(4)
|
||||
by(auto simp add: known_ptr_impl known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)
|
||||
then show ?thesis
|
||||
using assms
|
||||
apply(auto simp add: set_child_nodes_def a_set_child_nodes_tups_def set_child_nodes\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def)
|
||||
apply(split invoke_splits, rule conjI)+
|
||||
apply(auto simp add: is_element_ptr_kind\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def set_child_nodes\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def split: option.splits)
|
||||
using assms(3) l_put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_lemmas.put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ok l_put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_lemmas_axioms local.type_wf_impl
|
||||
by fastforce
|
||||
qed
|
||||
end
|
||||
|
||||
locale l_set_child_nodes_get_child_nodes = l_get_child_nodes + l_set_child_nodes +
|
||||
|
|
|
|||
|
|
@ -1860,11 +1860,6 @@ lemma get_root_node_wf_is_l_get_root_node_wf [instances]:
|
|||
|
||||
|
||||
subsection \<open>to\_tree\_order\<close>
|
||||
(* lemma to_tree_order_reads:
|
||||
assumes "a_heap_is_wellformed h"
|
||||
shows "reads (all_ptrs (getter_preserved_set_ext \<union> {get_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_preserved document_element}
|
||||
\<union> {get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_preserved Element.child_nodes})) (to_tree_order ptr) h h'"
|
||||
oops *)
|
||||
|
||||
locale l_to_tree_order_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
|
||||
l_to_tree_order\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
|
||||
|
|
@ -4282,7 +4277,7 @@ lemma adopt_node_preserves_wellformedness:
|
|||
and "h \<turnstile> adopt_node document_ptr child \<rightarrow>\<^sub>h h'"
|
||||
and known_ptrs: "known_ptrs h"
|
||||
and type_wf: "type_wf h"
|
||||
shows "heap_is_wellformed h'"
|
||||
shows "heap_is_wellformed h'" and "known_ptrs h'" and "type_wf h'"
|
||||
proof -
|
||||
obtain old_document parent_opt h2 where
|
||||
old_document: "h \<turnstile> get_owner_document (cast child) \<rightarrow>\<^sub>r old_document"
|
||||
|
|
@ -4321,11 +4316,17 @@ proof -
|
|||
have wellformed_h2: "heap_is_wellformed h2"
|
||||
using h2 remove_child_heap_is_wellformed_preserved known_ptrs type_wf
|
||||
by (metis (no_types, lifting) assms(1) option.case_eq_if pure_returns_heap_eq return_pure)
|
||||
then show ?thesis
|
||||
have "type_wf h2"
|
||||
using h2 remove_child_preserves_type_wf known_ptrs type_wf
|
||||
by (metis (no_types, lifting) assms(1) option.case_eq_if pure_returns_heap_eq return_pure)
|
||||
have "known_ptrs h2"
|
||||
using h2 remove_child_preserves_known_ptrs known_ptrs type_wf
|
||||
by (metis (no_types, lifting) assms(1) option.case_eq_if pure_returns_heap_eq return_pure)
|
||||
have "heap_is_wellformed h' \<and> known_ptrs h' \<and> type_wf h'"
|
||||
proof(cases "document_ptr = old_document")
|
||||
case True
|
||||
then show ?thesis
|
||||
using h' wellformed_h2 by auto
|
||||
using h' wellformed_h2 \<open>type_wf h2\<close> \<open>known_ptrs h2\<close> by auto
|
||||
next
|
||||
case False
|
||||
then obtain h3 old_disc_nodes disc_nodes_document_ptr_h3 where
|
||||
|
|
@ -4434,6 +4435,11 @@ proof -
|
|||
using set_disconnected_nodes_types_preserved
|
||||
by(auto simp add: reflp_def transp_def)
|
||||
|
||||
have "known_ptrs h3"
|
||||
using known_ptrs local.known_ptrs_preserved object_ptr_kinds_h2_eq3 object_ptr_kinds_h_eq3 by blast
|
||||
then have "known_ptrs h'"
|
||||
using local.known_ptrs_preserved object_ptr_kinds_h3_eq3 by blast
|
||||
|
||||
have disconnected_nodes_eq_h3:
|
||||
"\<And>doc_ptr disc_nodes. document_ptr \<noteq> doc_ptr
|
||||
\<Longrightarrow> h3 \<turnstile> get_disconnected_nodes doc_ptr \<rightarrow>\<^sub>r disc_nodes = h' \<turnstile> get_disconnected_nodes doc_ptr \<rightarrow>\<^sub>r disc_nodes"
|
||||
|
|
@ -4788,8 +4794,10 @@ proof -
|
|||
qed
|
||||
qed
|
||||
ultimately show ?thesis
|
||||
using \<open>type_wf h'\<close> \<open>a_owner_document_valid h'\<close> heap_is_wellformed_def by blast
|
||||
using \<open>type_wf h'\<close> \<open>known_ptrs h'\<close> \<open>a_owner_document_valid h'\<close> heap_is_wellformed_def by blast
|
||||
qed
|
||||
then show "heap_is_wellformed h'" and "known_ptrs h'" and "type_wf h'"
|
||||
by auto
|
||||
qed
|
||||
|
||||
lemma adopt_node_node_in_disconnected_nodes:
|
||||
|
|
@ -4890,6 +4898,13 @@ locale l_adopt_node_wf = l_heap_is_wellformed + l_known_ptrs + l_type_wf + l_ado
|
|||
assumes adopt_node_document_in_heap: "heap_is_wellformed h \<Longrightarrow> known_ptrs h \<Longrightarrow> type_wf h
|
||||
\<Longrightarrow> h \<turnstile> ok (adopt_node owner_document node)
|
||||
\<Longrightarrow> owner_document |\<in>| document_ptr_kinds h"
|
||||
assumes adopt_node_preserves_type_wf:
|
||||
"heap_is_wellformed h \<Longrightarrow> h \<turnstile> adopt_node document_ptr child \<rightarrow>\<^sub>h h' \<Longrightarrow> known_ptrs h
|
||||
\<Longrightarrow> type_wf h \<Longrightarrow> type_wf h'"
|
||||
assumes adopt_node_preserves_known_ptrs:
|
||||
"heap_is_wellformed h \<Longrightarrow> h \<turnstile> adopt_node document_ptr child \<rightarrow>\<^sub>h h' \<Longrightarrow> known_ptrs h
|
||||
\<Longrightarrow> type_wf h \<Longrightarrow> known_ptrs h'"
|
||||
|
||||
|
||||
lemma adopt_node_wf_is_l_adopt_node_wf [instances]:
|
||||
"l_adopt_node_wf type_wf known_ptr heap_is_wellformed parent_child_rel get_child_nodes
|
||||
|
|
@ -4901,6 +4916,8 @@ lemma adopt_node_wf_is_l_adopt_node_wf [instances]:
|
|||
using adopt_node_node_in_disconnected_nodes apply blast
|
||||
using adopt_node_removes_first_child apply blast
|
||||
using adopt_node_document_in_heap apply blast
|
||||
using adopt_node_preserves_wellformedness apply blast
|
||||
using adopt_node_preserves_wellformedness apply blast
|
||||
done
|
||||
|
||||
|
||||
|
|
@ -4987,7 +5004,8 @@ locale l_insert_before_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub
|
|||
l_set_disconnected_nodes_get_ancestors +
|
||||
l_get_ancestors_wf +
|
||||
l_get_owner_document +
|
||||
l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
|
||||
l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
|
||||
l_get_owner_document_wf
|
||||
begin
|
||||
|
||||
lemma insert_before_preserves_acyclitity_thesis:
|
||||
|
|
@ -5991,7 +6009,6 @@ proof -
|
|||
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
|
||||
|
|
@ -6024,6 +6041,449 @@ lemma insert_before_wf2_is_l_insert_before_wf2 [instances]:
|
|||
using insert_before_heap_is_wellformed_preserved apply(fast, fast, fast)
|
||||
done
|
||||
|
||||
|
||||
|
||||
locale l_insert_before_wf3\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
|
||||
l_insert_before_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
|
||||
l_adopt_node\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
|
||||
l_set_child_nodes_get_child_nodes\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
|
||||
l_remove_child_wf2
|
||||
begin
|
||||
|
||||
lemma next_sibling_ok:
|
||||
assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
|
||||
assumes "node_ptr |\<in>| node_ptr_kinds h"
|
||||
shows "h \<turnstile> ok (a_next_sibling node_ptr)"
|
||||
proof -
|
||||
have "known_ptr (cast node_ptr)"
|
||||
using assms(2) assms(4) local.known_ptrs_known_ptr node_ptr_kinds_commutes by blast
|
||||
then show ?thesis
|
||||
using assms
|
||||
apply(auto simp add: a_next_sibling_def intro!: bind_is_OK_pure_I split: option.splits list.splits)
|
||||
using get_child_nodes_ok local.get_parent_parent_in_heap local.known_ptrs_known_ptr by blast
|
||||
qed
|
||||
|
||||
lemma remove_child_ok:
|
||||
assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
|
||||
assumes "h \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children"
|
||||
assumes "child \<in> set children"
|
||||
shows "h \<turnstile> ok (remove_child ptr child)"
|
||||
proof -
|
||||
|
||||
have "ptr |\<in>| object_ptr_kinds h"
|
||||
using assms(4) local.get_child_nodes_ptr_in_heap by blast
|
||||
have "child |\<in>| node_ptr_kinds h"
|
||||
using assms(1) assms(4) assms(5) local.heap_is_wellformed_children_in_heap by blast
|
||||
have "\<not>is_character_data_ptr ptr"
|
||||
proof (rule ccontr, simp)
|
||||
assume "is_character_data_ptr ptr"
|
||||
then have "h \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r []"
|
||||
using \<open>ptr |\<in>| object_ptr_kinds h\<close>
|
||||
apply(simp add: get_child_nodes_def a_get_child_nodes_tups_def)
|
||||
apply(split invoke_splits)+
|
||||
by(auto simp add: get_child_nodes\<^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_def intro!: bind_pure_returns_result_I split: option.splits)
|
||||
then
|
||||
show False
|
||||
using assms returns_result_eq by fastforce
|
||||
qed
|
||||
have "is_character_data_ptr child \<Longrightarrow> \<not>is_document_ptr_kind ptr"
|
||||
proof (rule ccontr, simp)
|
||||
assume "is_character_data_ptr\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r child"
|
||||
and "is_document_ptr_kind ptr"
|
||||
then show False
|
||||
using assms
|
||||
using \<open>ptr |\<in>| object_ptr_kinds h\<close>
|
||||
apply(simp add: get_child_nodes_def a_get_child_nodes_tups_def)
|
||||
apply(split invoke_splits)+
|
||||
apply(auto split: option.splits)
|
||||
apply (meson invoke_empty is_OK_returns_result_I)
|
||||
apply (meson invoke_empty is_OK_returns_result_I)
|
||||
by(auto simp add: get_child_nodes\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def elim!: bind_returns_result_E2 split: option.splits)
|
||||
qed
|
||||
|
||||
obtain owner_document where
|
||||
owner_document: "h \<turnstile> get_owner_document (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) \<rightarrow>\<^sub>r owner_document"
|
||||
by (meson \<open>child |\<in>| node_ptr_kinds h\<close> assms(1) assms(2) assms(3) is_OK_returns_result_E local.get_owner_document_ok node_ptr_kinds_commutes)
|
||||
obtain disconnected_nodes_h where
|
||||
disconnected_nodes_h: "h \<turnstile> get_disconnected_nodes owner_document \<rightarrow>\<^sub>r disconnected_nodes_h"
|
||||
by (meson assms(1) assms(2) assms(3) is_OK_returns_result_E local.get_disconnected_nodes_ok local.get_owner_document_owner_document_in_heap owner_document)
|
||||
obtain h2 where
|
||||
h2: "h \<turnstile> set_disconnected_nodes owner_document (child # disconnected_nodes_h) \<rightarrow>\<^sub>h h2"
|
||||
by (meson assms(1) assms(2) assms(3) is_OK_returns_heap_E l_set_disconnected_nodes.set_disconnected_nodes_ok local.get_owner_document_owner_document_in_heap local.l_set_disconnected_nodes_axioms owner_document)
|
||||
|
||||
have "known_ptr ptr"
|
||||
using assms(2) assms(4) local.known_ptrs_known_ptr
|
||||
using \<open>ptr |\<in>| object_ptr_kinds h\<close> by blast
|
||||
|
||||
have "type_wf h2"
|
||||
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF set_disconnected_nodes_writes h2]
|
||||
using set_disconnected_nodes_types_preserved assms(3)
|
||||
by(auto simp add: reflp_def transp_def)
|
||||
|
||||
have "object_ptr_kinds h = object_ptr_kinds h2"
|
||||
using h2
|
||||
apply(rule writes_small_big[where P="\<lambda>h h'. object_ptr_kinds h = object_ptr_kinds h'",
|
||||
OF set_disconnected_nodes_writes])
|
||||
using set_disconnected_nodes_pointers_preserved
|
||||
by (auto simp add: reflp_def transp_def)
|
||||
|
||||
have "h2 \<turnstile> ok (set_child_nodes ptr (remove1 child children))"
|
||||
proof (cases "is_element_ptr_kind ptr")
|
||||
case True
|
||||
then show ?thesis
|
||||
using set_child_nodes_element_ok \<open>known_ptr ptr\<close> \<open>object_ptr_kinds h = object_ptr_kinds h2\<close> \<open>type_wf h2\<close> assms(4)
|
||||
using \<open>ptr |\<in>| object_ptr_kinds h\<close> by blast
|
||||
next
|
||||
case False
|
||||
then have "is_document_ptr_kind ptr"
|
||||
using \<open>known_ptr ptr\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close> \<open>\<not>is_character_data_ptr ptr\<close>
|
||||
by(auto simp add:known_ptr_impl known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)
|
||||
moreover have "is_document_ptr ptr"
|
||||
using \<open>known_ptr ptr\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close> False \<open>\<not>is_character_data_ptr ptr\<close>
|
||||
by(auto simp add: known_ptr_impl known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)
|
||||
ultimately show ?thesis
|
||||
using assms(4)
|
||||
apply(auto simp add: get_child_nodes_def a_get_child_nodes_tups_def)
|
||||
apply(split invoke_splits)+
|
||||
apply(auto elim!: bind_returns_result_E2 split: option.splits)
|
||||
apply(auto simp add: get_child_nodes\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def elim!: bind_returns_result_E2 split: option.splits)
|
||||
using \<open>ptr |\<in>| object_ptr_kinds h\<close> \<open>is_document_ptr_kind ptr\<close> \<open>known_ptr ptr\<close> \<open>object_ptr_kinds h = object_ptr_kinds h2\<close> \<open>type_wf h2\<close> assms(4) local.set_child_nodes_document1_ok apply blast
|
||||
using \<open>ptr |\<in>| object_ptr_kinds h\<close> \<open>is_document_ptr_kind ptr\<close> \<open>known_ptr ptr\<close> \<open>object_ptr_kinds h = object_ptr_kinds h2\<close> \<open>type_wf h2\<close> assms(4) local.set_child_nodes_document1_ok apply blast
|
||||
using \<open>ptr |\<in>| object_ptr_kinds h\<close> \<open>is_document_ptr_kind ptr\<close> \<open>known_ptr ptr\<close> \<open>object_ptr_kinds h = object_ptr_kinds h2\<close> \<open>type_wf h2\<close> assms(4) is_element_ptr_kind_cast local.set_child_nodes_document2_ok by blast
|
||||
qed
|
||||
then
|
||||
obtain h' where
|
||||
h': "h2 \<turnstile> set_child_nodes ptr (remove1 child children) \<rightarrow>\<^sub>h h'"
|
||||
by auto
|
||||
|
||||
show ?thesis
|
||||
using assms
|
||||
apply(auto simp add: remove_child_def
|
||||
simp add: is_OK_returns_heap_I[OF h2] is_OK_returns_heap_I[OF h'] is_OK_returns_result_I[OF assms(4)] is_OK_returns_result_I[OF owner_document] is_OK_returns_result_I[OF disconnected_nodes_h]
|
||||
intro!: bind_is_OK_pure_I[OF get_owner_document_pure]
|
||||
bind_is_OK_pure_I[OF get_child_nodes_pure]
|
||||
bind_is_OK_pure_I[OF get_disconnected_nodes_pure]
|
||||
bind_is_OK_I[rotated, OF h2]
|
||||
dest!: returns_result_eq[OF assms(4)] returns_result_eq[OF owner_document] returns_result_eq[OF disconnected_nodes_h]
|
||||
)
|
||||
using h2 returns_result_select_result by force
|
||||
qed
|
||||
|
||||
lemma adopt_node_ok:
|
||||
assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
|
||||
assumes "document_ptr |\<in>| document_ptr_kinds h"
|
||||
assumes "child |\<in>| node_ptr_kinds h"
|
||||
shows "h \<turnstile> ok (adopt_node document_ptr child)"
|
||||
proof -
|
||||
obtain old_document where
|
||||
old_document: "h \<turnstile> get_owner_document (cast child) \<rightarrow>\<^sub>r old_document"
|
||||
by (meson assms(1) assms(2) assms(3) assms(5) is_OK_returns_result_E local.get_owner_document_ok node_ptr_kinds_commutes)
|
||||
then have "h \<turnstile> ok (get_owner_document (cast child))"
|
||||
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)
|
||||
then have "h \<turnstile> ok (get_parent child)"
|
||||
by auto
|
||||
|
||||
have "h \<turnstile> ok (case parent_opt of Some parent \<Rightarrow> remove_child parent child | None \<Rightarrow> return ())"
|
||||
apply(auto split: option.splits)
|
||||
using remove_child_ok
|
||||
by (metis assms(1) assms(2) assms(3) local.get_parent_child_dual parent_opt)
|
||||
then
|
||||
obtain h2 where
|
||||
h2: "h \<turnstile> (case parent_opt of Some parent \<Rightarrow> remove_child parent child | None \<Rightarrow> return ()) \<rightarrow>\<^sub>h h2"
|
||||
by auto
|
||||
|
||||
have "object_ptr_kinds h = object_ptr_kinds h2"
|
||||
using h2 apply(simp split: option.splits)
|
||||
apply(rule writes_small_big[where P="\<lambda>h h'. object_ptr_kinds h = object_ptr_kinds h'",
|
||||
OF remove_child_writes])
|
||||
using remove_child_pointers_preserved
|
||||
by (auto simp add: reflp_def transp_def)
|
||||
then
|
||||
have "old_document |\<in>| document_ptr_kinds h2"
|
||||
using assms(1) assms(2) assms(3) document_ptr_kinds_commutes local.get_owner_document_owner_document_in_heap old_document by blast
|
||||
|
||||
|
||||
have wellformed_h2: "heap_is_wellformed h2"
|
||||
using h2 remove_child_heap_is_wellformed_preserved assms
|
||||
by(auto split: option.splits)
|
||||
have "type_wf h2"
|
||||
using h2 remove_child_preserves_type_wf assms
|
||||
by(auto split: option.splits)
|
||||
have "known_ptrs h2"
|
||||
using h2 remove_child_preserves_known_ptrs assms
|
||||
by(auto split: option.splits)
|
||||
|
||||
|
||||
have "object_ptr_kinds h = object_ptr_kinds h2"
|
||||
using h2 apply(simp split: option.splits)
|
||||
apply(rule writes_small_big[where P="\<lambda>h h'. object_ptr_kinds h = object_ptr_kinds h'",
|
||||
OF remove_child_writes])
|
||||
using remove_child_pointers_preserved
|
||||
by (auto simp add: reflp_def transp_def)
|
||||
then have "document_ptr_kinds h = document_ptr_kinds h2"
|
||||
by(auto simp add: document_ptr_kinds_def)
|
||||
|
||||
have "h2 \<turnstile> ok (if document_ptr \<noteq> old_document then do {
|
||||
old_disc_nodes \<leftarrow> get_disconnected_nodes old_document;
|
||||
set_disconnected_nodes old_document (remove1 child old_disc_nodes);
|
||||
disc_nodes \<leftarrow> get_disconnected_nodes document_ptr;
|
||||
set_disconnected_nodes document_ptr (child # disc_nodes)
|
||||
} else do {
|
||||
return ()
|
||||
})"
|
||||
proof(cases "document_ptr = old_document")
|
||||
case True
|
||||
then show ?thesis
|
||||
by simp
|
||||
next
|
||||
case False
|
||||
then have "h2 \<turnstile> ok (get_disconnected_nodes old_document)"
|
||||
by (simp add: \<open>old_document |\<in>| document_ptr_kinds h2\<close> \<open>type_wf h2\<close> local.get_disconnected_nodes_ok)
|
||||
then obtain old_disc_nodes where
|
||||
old_disc_nodes: "h2 \<turnstile> get_disconnected_nodes old_document \<rightarrow>\<^sub>r old_disc_nodes"
|
||||
by auto
|
||||
|
||||
have "h2 \<turnstile> ok (set_disconnected_nodes old_document (remove1 child old_disc_nodes))"
|
||||
by (simp add: \<open>old_document |\<in>| document_ptr_kinds h2\<close> \<open>type_wf h2\<close> local.set_disconnected_nodes_ok)
|
||||
then obtain h3 where
|
||||
h3: "h2 \<turnstile> set_disconnected_nodes old_document (remove1 child old_disc_nodes) \<rightarrow>\<^sub>h h3"
|
||||
by auto
|
||||
|
||||
|
||||
have object_ptr_kinds_h2_eq3: "object_ptr_kinds h2 = object_ptr_kinds h3"
|
||||
apply(rule writes_small_big[where P="\<lambda>h h'. object_ptr_kinds h = object_ptr_kinds h'",
|
||||
OF set_disconnected_nodes_writes h3])
|
||||
using set_disconnected_nodes_pointers_preserved set_child_nodes_pointers_preserved
|
||||
by (auto simp add: reflp_def transp_def)
|
||||
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_eq_h2: "|h2 \<turnstile> object_ptr_kinds_M|\<^sub>r = |h3 \<turnstile> object_ptr_kinds_M|\<^sub>r"
|
||||
by(simp)
|
||||
then have node_ptr_kinds_eq_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
|
||||
then have node_ptr_kinds_eq3_h2: "node_ptr_kinds h2 = node_ptr_kinds h3"
|
||||
by auto
|
||||
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_eq_h2 document_ptr_kinds_M_eq by auto
|
||||
then have document_ptr_kinds_eq3_h2: "document_ptr_kinds h2 = document_ptr_kinds h3"
|
||||
using object_ptr_kinds_eq_h2 document_ptr_kinds_M_eq by auto
|
||||
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 (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 "type_wf h3"
|
||||
using \<open>type_wf h2\<close>
|
||||
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)
|
||||
moreover have "document_ptr |\<in>| document_ptr_kinds h3"
|
||||
using \<open>document_ptr_kinds h = document_ptr_kinds h2\<close> assms(4) document_ptr_kinds_eq3_h2 by auto
|
||||
ultimately have "h3 \<turnstile> ok (get_disconnected_nodes document_ptr)"
|
||||
by (simp add: local.get_disconnected_nodes_ok)
|
||||
|
||||
then obtain disc_nodes where
|
||||
disc_nodes: "h3 \<turnstile> get_disconnected_nodes document_ptr \<rightarrow>\<^sub>r disc_nodes"
|
||||
by auto
|
||||
|
||||
|
||||
have "h3 \<turnstile> ok (set_disconnected_nodes document_ptr (child # disc_nodes))"
|
||||
using \<open>document_ptr |\<in>| document_ptr_kinds h3\<close> \<open>type_wf h3\<close> local.set_disconnected_nodes_ok by auto
|
||||
then obtain h' where
|
||||
h': "h3 \<turnstile> set_disconnected_nodes document_ptr (child # disc_nodes) \<rightarrow>\<^sub>h h'"
|
||||
by auto
|
||||
|
||||
then show ?thesis
|
||||
using False
|
||||
using \<open>h2 \<turnstile> ok get_disconnected_nodes old_document\<close>
|
||||
using \<open>h3 \<turnstile> ok get_disconnected_nodes document_ptr\<close>
|
||||
apply(auto dest!: returns_result_eq[OF old_disc_nodes] returns_result_eq[OF disc_nodes]
|
||||
intro!: bind_is_OK_I[rotated, OF h3] bind_is_OK_pure_I[OF get_disconnected_nodes_pure] )
|
||||
using \<open>h2 \<turnstile> ok set_disconnected_nodes old_document (remove1 child old_disc_nodes)\<close> by auto
|
||||
qed
|
||||
then obtain h' where
|
||||
h': "h2 \<turnstile> (if document_ptr \<noteq> old_document then do {
|
||||
old_disc_nodes \<leftarrow> get_disconnected_nodes old_document;
|
||||
set_disconnected_nodes old_document (remove1 child old_disc_nodes);
|
||||
disc_nodes \<leftarrow> get_disconnected_nodes document_ptr;
|
||||
set_disconnected_nodes document_ptr (child # disc_nodes)
|
||||
} else do {
|
||||
return ()
|
||||
}) \<rightarrow>\<^sub>h h'"
|
||||
by auto
|
||||
|
||||
show ?thesis
|
||||
using \<open>h \<turnstile> ok (get_owner_document (cast child))\<close>
|
||||
using \<open>h \<turnstile> ok (get_parent child)\<close>
|
||||
using h2 h'
|
||||
apply(auto simp add: adopt_node_def
|
||||
simp add: is_OK_returns_heap_I[OF h2]
|
||||
intro!: bind_is_OK_pure_I[OF get_owner_document_pure]
|
||||
bind_is_OK_pure_I[OF get_parent_pure]
|
||||
bind_is_OK_I[rotated, OF h2]
|
||||
dest!: returns_result_eq[OF parent_opt] returns_result_eq[OF old_document])
|
||||
using \<open>h \<turnstile> ok (case parent_opt of None \<Rightarrow> return () | Some parent \<Rightarrow> remove_child parent child)\<close>
|
||||
by auto
|
||||
qed
|
||||
|
||||
lemma insert_node_ok:
|
||||
assumes "known_ptr parent" and "type_wf h"
|
||||
assumes "parent |\<in>| object_ptr_kinds h"
|
||||
assumes "\<not>is_character_data_ptr_kind 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"
|
||||
assumes "known_ptr (cast node)"
|
||||
shows "h \<turnstile> ok (a_insert_node parent node ref)"
|
||||
proof(auto simp add: a_insert_node_def get_child_nodes_ok[OF assms(1) assms(2) assms(3)] intro!: bind_is_OK_pure_I)
|
||||
fix children'
|
||||
assume "h \<turnstile> get_child_nodes parent \<rightarrow>\<^sub>r children'"
|
||||
|
||||
show "h \<turnstile> ok set_child_nodes parent (insert_before_list node ref children')"
|
||||
proof (cases "is_element_ptr_kind parent")
|
||||
case True
|
||||
then show ?thesis
|
||||
using set_child_nodes_element_ok
|
||||
using assms(1) assms(2) assms(3) by blast
|
||||
next
|
||||
case False
|
||||
then have "is_document_ptr_kind parent"
|
||||
using assms(4) assms(1)
|
||||
by(auto simp add: known_ptr_impl DocumentClass.known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)
|
||||
then have "is_document_ptr parent"
|
||||
using assms(1)
|
||||
by(auto simp add: known_ptr_impl DocumentClass.known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)
|
||||
then obtain children where children: "h \<turnstile> get_child_nodes parent \<rightarrow>\<^sub>r children" and "children = []"
|
||||
using assms(5) by blast
|
||||
|
||||
have "insert_before_list node ref children' = [node]"
|
||||
by (metis \<open>children = []\<close> \<open>h \<turnstile> get_child_nodes parent \<rightarrow>\<^sub>r children'\<close> append.left_neutral children insert_Nil l_insert_before\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.insert_before_list.elims l_insert_before\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.insert_before_list.simps(3) neq_Nil_conv returns_result_eq)
|
||||
moreover have "\<not>is_character_data_ptr_kind node"
|
||||
using \<open>is_document_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r parent\<close> assms(6) by blast
|
||||
then have "is_element_ptr_kind node"
|
||||
by (metis (no_types, lifting) CharacterDataClass.a_known_ptr_def DocumentClass.a_known_ptr_def ElementClass.a_known_ptr_def NodeClass.a_known_ptr_def assms(7) 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_inject document_ptr_no_node_ptr_cast is_character_data_ptr_kind_none is_document_ptr_kind_none is_element_ptr_implies_kind is_node_ptr_kind_cast local.known_ptr_impl node_ptr_casts_commute3 option.case_eq_if)
|
||||
ultimately
|
||||
show ?thesis
|
||||
using set_child_nodes_document2_ok
|
||||
by (metis \<open>is_document_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r parent\<close> assms(1) assms(2) assms(3) assms(5) is_document_ptr_kind_none option.case_eq_if)
|
||||
qed
|
||||
qed
|
||||
|
||||
lemma insert_before_ok:
|
||||
assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
|
||||
assumes "parent |\<in>| object_ptr_kinds h"
|
||||
assumes "node |\<in>| node_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 (insert_before parent node (Some ref))"
|
||||
proof -
|
||||
have "h \<turnstile> ok (a_ensure_pre_insertion_validity node parent (Some ref))"
|
||||
using assms ensure_pre_insertion_validity_ok by blast
|
||||
have "h \<turnstile> ok (if Some node = Some ref
|
||||
then a_next_sibling node
|
||||
else return (Some ref))" (is "h \<turnstile> ok ?P")
|
||||
apply(auto split: if_splits)
|
||||
using assms(1) assms(2) assms(3) assms(5) next_sibling_ok by blast
|
||||
|
||||
then obtain reference_child where
|
||||
reference_child: "h \<turnstile> ?P \<rightarrow>\<^sub>r reference_child"
|
||||
by auto
|
||||
|
||||
obtain owner_document where
|
||||
owner_document: "h \<turnstile> get_owner_document parent \<rightarrow>\<^sub>r owner_document"
|
||||
using assms get_owner_document_ok
|
||||
by (meson returns_result_select_result)
|
||||
then have "h \<turnstile> ok (get_owner_document parent)"
|
||||
by auto
|
||||
have "owner_document |\<in>| document_ptr_kinds h"
|
||||
using assms(1) assms(2) assms(3) local.get_owner_document_owner_document_in_heap owner_document by blast
|
||||
|
||||
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)
|
||||
then have "h \<turnstile> ok (adopt_node owner_document node)"
|
||||
by auto
|
||||
have "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 "document_ptr_kinds h = document_ptr_kinds h2"
|
||||
by(auto simp add: document_ptr_kinds_def)
|
||||
have "heap_is_wellformed h2"
|
||||
using h2 adopt_node_preserves_wellformedness assms by blast
|
||||
have "known_ptrs h2"
|
||||
using h2 adopt_node_preserves_known_ptrs assms by blast
|
||||
have "type_wf h2"
|
||||
using h2 adopt_node_preserves_type_wf assms by blast
|
||||
|
||||
obtain disconnected_nodes_h2 where
|
||||
disconnected_nodes_h2: "h2 \<turnstile> get_disconnected_nodes owner_document \<rightarrow>\<^sub>r disconnected_nodes_h2"
|
||||
by (metis \<open>document_ptr_kinds h = document_ptr_kinds h2\<close> \<open>type_wf h2\<close> assms(1) assms(2) assms(3) is_OK_returns_result_E local.get_disconnected_nodes_ok local.get_owner_document_owner_document_in_heap owner_document)
|
||||
|
||||
obtain h3 where
|
||||
h3: "h2 \<turnstile> set_disconnected_nodes owner_document (remove1 node disconnected_nodes_h2) \<rightarrow>\<^sub>h h3"
|
||||
by (metis \<open>document_ptr_kinds h = document_ptr_kinds h2\<close> \<open>owner_document |\<in>| document_ptr_kinds h\<close> \<open>type_wf h2\<close> document_ptr_kinds_def is_OK_returns_heap_E l_set_disconnected_nodes.set_disconnected_nodes_ok local.l_set_disconnected_nodes_axioms)
|
||||
|
||||
have "type_wf h3"
|
||||
using \<open>type_wf h2\<close>
|
||||
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)
|
||||
|
||||
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)
|
||||
|
||||
have "parent |\<in>| object_ptr_kinds h3"
|
||||
using \<open>object_ptr_kinds h = object_ptr_kinds h2\<close> assms(4) object_ptr_kinds_M_eq3_h2 by blast
|
||||
moreover have "known_ptr parent"
|
||||
using assms(2) assms(4) local.known_ptrs_known_ptr by blast
|
||||
moreover have "known_ptr (cast node)"
|
||||
using assms(2) assms(5) local.known_ptrs_known_ptr node_ptr_kinds_commutes by blast
|
||||
moreover have "is_document_ptr parent \<Longrightarrow> h3 \<turnstile> get_child_nodes parent \<rightarrow>\<^sub>r []"
|
||||
by (metis assms(8) assms(9) distinct.simps(2) distinct_singleton local.get_parent_child_dual returns_result_eq)
|
||||
ultimately obtain h' where
|
||||
h': "h3 \<turnstile> a_insert_node parent node reference_child \<rightarrow>\<^sub>h h'"
|
||||
using insert_node_ok \<open>type_wf h3\<close> assms by blast
|
||||
|
||||
show ?thesis
|
||||
using \<open>h \<turnstile> ok (a_ensure_pre_insertion_validity node parent (Some ref))\<close>
|
||||
using reference_child \<open>h \<turnstile> ok (get_owner_document parent)\<close> \<open>h \<turnstile> ok (adopt_node owner_document node)\<close> h3 h'
|
||||
apply(auto simp add: insert_before_def
|
||||
simp add: is_OK_returns_result_I[OF disconnected_nodes_h2]
|
||||
simp add: is_OK_returns_heap_I[OF h3] is_OK_returns_heap_I[OF h']
|
||||
intro!: bind_is_OK_I2
|
||||
bind_is_OK_pure_I[OF ensure_pre_insertion_validity_pure]
|
||||
bind_is_OK_pure_I[OF next_sibling_pure]
|
||||
bind_is_OK_pure_I[OF get_owner_document_pure]
|
||||
bind_is_OK_pure_I[OF get_disconnected_nodes_pure]
|
||||
dest!: returns_result_eq[OF owner_document] returns_result_eq[OF disconnected_nodes_h2] returns_heap_eq[OF h2] returns_heap_eq[OF h3]
|
||||
dest!: sym[of node ref]
|
||||
)
|
||||
using returns_result_eq by fastforce
|
||||
qed
|
||||
end
|
||||
|
||||
interpretation i_insert_before_wf3?: l_insert_before_wf3\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
|
||||
get_parent get_parent_locs get_child_nodes get_child_nodes_locs set_child_nodes set_child_nodes_locs get_ancestors get_ancestors_locs adopt_node adopt_node_locs set_disconnected_nodes set_disconnected_nodes_locs get_disconnected_nodes get_disconnected_nodes_locs get_owner_document insert_before insert_before_locs append_child type_wf known_ptr known_ptrs heap_is_wellformed parent_child_rel remove_child remove_child_locs get_root_node get_root_node_locs remove
|
||||
by(auto simp add: l_insert_before_wf3\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
|
||||
declare l_insert_before_wf3\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]
|
||||
|
||||
|
||||
locale l_append_child_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
|
||||
l_adopt_node\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
|
||||
l_insert_before\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
|
||||
|
|
|
|||
Reference in New Issue