forked from afp-mirror/Core_DOM
Added more lemmas and locales.
This commit is contained in:
parent
b7fa25e301
commit
4ef60408e5
|
@ -3575,6 +3575,15 @@ assume 1: "xa \<in> fset (object_ptr_kinds h')"
|
||||||
using heap_is_wellformed_def by blast
|
using heap_is_wellformed_def by blast
|
||||||
qed
|
qed
|
||||||
|
|
||||||
|
lemma remove_heap_is_wellformed_preserved:
|
||||||
|
assumes "heap_is_wellformed h"
|
||||||
|
and "h \<turnstile> remove child \<rightarrow>\<^sub>h h'"
|
||||||
|
and "known_ptrs h"
|
||||||
|
and type_wf: "type_wf h"
|
||||||
|
shows "type_wf h'" and "known_ptrs h'" and "heap_is_wellformed h'"
|
||||||
|
using assms
|
||||||
|
by(auto simp add: remove_def intro: remove_child_heap_is_wellformed_preserved elim!: bind_returns_heap_E2 split: option.splits)
|
||||||
|
|
||||||
lemma remove_child_removes_child:
|
lemma remove_child_removes_child:
|
||||||
assumes wellformed: "heap_is_wellformed h"
|
assumes wellformed: "heap_is_wellformed h"
|
||||||
and remove_child: "h \<turnstile> remove_child ptr' child \<rightarrow>\<^sub>h h'"
|
and remove_child: "h \<turnstile> remove_child ptr' child \<rightarrow>\<^sub>h h'"
|
||||||
|
@ -3728,6 +3737,15 @@ locale l_remove_child_wf2 = l_type_wf + l_known_ptrs + l_remove_child_defs + l_h
|
||||||
assumes remove_child_heap_is_wellformed_preserved:
|
assumes remove_child_heap_is_wellformed_preserved:
|
||||||
"type_wf h \<Longrightarrow> known_ptrs h \<Longrightarrow> heap_is_wellformed h \<Longrightarrow> h \<turnstile> remove_child ptr child \<rightarrow>\<^sub>h h'
|
"type_wf h \<Longrightarrow> known_ptrs h \<Longrightarrow> heap_is_wellformed h \<Longrightarrow> h \<turnstile> remove_child ptr child \<rightarrow>\<^sub>h h'
|
||||||
\<Longrightarrow> heap_is_wellformed h'"
|
\<Longrightarrow> heap_is_wellformed h'"
|
||||||
|
assumes remove_preserves_type_wf:
|
||||||
|
"heap_is_wellformed h \<Longrightarrow> type_wf h \<Longrightarrow> known_ptrs h \<Longrightarrow> h \<turnstile> remove child \<rightarrow>\<^sub>h h'
|
||||||
|
\<Longrightarrow> type_wf h'"
|
||||||
|
assumes remove_preserves_known_ptrs:
|
||||||
|
"heap_is_wellformed h \<Longrightarrow> type_wf h \<Longrightarrow> known_ptrs h \<Longrightarrow> h \<turnstile> remove child \<rightarrow>\<^sub>h h'
|
||||||
|
\<Longrightarrow> known_ptrs h'"
|
||||||
|
assumes remove_heap_is_wellformed_preserved:
|
||||||
|
"type_wf h \<Longrightarrow> known_ptrs h \<Longrightarrow> heap_is_wellformed h \<Longrightarrow> h \<turnstile> remove child \<rightarrow>\<^sub>h h'
|
||||||
|
\<Longrightarrow> heap_is_wellformed h'"
|
||||||
assumes remove_child_removes_child:
|
assumes remove_child_removes_child:
|
||||||
"heap_is_wellformed h \<Longrightarrow> h \<turnstile> remove_child ptr' child \<rightarrow>\<^sub>h h' \<Longrightarrow> h' \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children
|
"heap_is_wellformed h \<Longrightarrow> h \<turnstile> remove_child ptr' child \<rightarrow>\<^sub>h h' \<Longrightarrow> h' \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children
|
||||||
\<Longrightarrow> known_ptrs h \<Longrightarrow> type_wf h
|
\<Longrightarrow> known_ptrs h \<Longrightarrow> type_wf h
|
||||||
|
@ -3756,6 +3774,7 @@ lemma remove_child_wf2_is_l_remove_child_wf2 [instances]:
|
||||||
"l_remove_child_wf2 type_wf known_ptr known_ptrs remove_child heap_is_wellformed get_child_nodes remove"
|
"l_remove_child_wf2 type_wf known_ptr known_ptrs remove_child heap_is_wellformed get_child_nodes remove"
|
||||||
apply(auto simp add: l_remove_child_wf2_def l_remove_child_wf2_axioms_def instances)[1]
|
apply(auto simp add: l_remove_child_wf2_def l_remove_child_wf2_axioms_def instances)[1]
|
||||||
using remove_child_heap_is_wellformed_preserved apply(fast, fast, fast)
|
using remove_child_heap_is_wellformed_preserved apply(fast, fast, fast)
|
||||||
|
using remove_heap_is_wellformed_preserved apply(fast, fast, fast)
|
||||||
using remove_child_removes_child apply fast
|
using remove_child_removes_child apply fast
|
||||||
using remove_child_removes_first_child apply fast
|
using remove_child_removes_first_child apply fast
|
||||||
using remove_removes_child apply fast
|
using remove_removes_child apply fast
|
||||||
|
@ -5161,12 +5180,23 @@ lemma insert_before_wf2_is_l_insert_before_wf2 [instances]:
|
||||||
|
|
||||||
locale l_append_child_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
|
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_adopt_node\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
|
||||||
l_insert_before_wf\<^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 +
|
||||||
l_insert_before_wf2 +
|
|
||||||
l_append_child\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
|
l_append_child\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
|
||||||
|
l_insert_before_wf +
|
||||||
|
l_insert_before_wf2 +
|
||||||
l_get_child_nodes
|
l_get_child_nodes
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
|
||||||
|
lemma append_child_heap_is_wellformed_preserved:
|
||||||
|
assumes wellformed: "heap_is_wellformed h"
|
||||||
|
and append_child: "h \<turnstile> append_child ptr node \<rightarrow>\<^sub>h h'"
|
||||||
|
and known_ptrs: "known_ptrs h"
|
||||||
|
and type_wf: "type_wf h"
|
||||||
|
shows "heap_is_wellformed h'" and "type_wf h'" and "known_ptrs h'"
|
||||||
|
using assms
|
||||||
|
by(auto simp add: append_child_def intro: insert_before_preserves_type_wf insert_before_preserves_known_ptrs insert_before_heap_is_wellformed_preserved)
|
||||||
|
|
||||||
lemma append_child_children:
|
lemma append_child_children:
|
||||||
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
|
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
|
||||||
assumes "h \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r xs"
|
assumes "h \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r xs"
|
||||||
|
@ -5289,6 +5319,17 @@ lemma append_child_for_all_on_no_children:
|
||||||
by force
|
by force
|
||||||
end
|
end
|
||||||
|
|
||||||
|
locale l_append_child_wf = l_type_wf + l_known_ptrs + l_append_child_defs + l_heap_is_wellformed_defs +
|
||||||
|
assumes append_child_preserves_type_wf:
|
||||||
|
"heap_is_wellformed h \<Longrightarrow> type_wf h \<Longrightarrow> known_ptrs h \<Longrightarrow> h \<turnstile> append_child ptr child \<rightarrow>\<^sub>h h'
|
||||||
|
\<Longrightarrow> type_wf h'"
|
||||||
|
assumes append_child_preserves_known_ptrs:
|
||||||
|
"heap_is_wellformed h \<Longrightarrow> type_wf h \<Longrightarrow> known_ptrs h \<Longrightarrow> h \<turnstile> append_child ptr child \<rightarrow>\<^sub>h h'
|
||||||
|
\<Longrightarrow> known_ptrs h'"
|
||||||
|
assumes append_child_heap_is_wellformed_preserved:
|
||||||
|
"type_wf h \<Longrightarrow> known_ptrs h \<Longrightarrow> heap_is_wellformed h \<Longrightarrow> h \<turnstile> append_child ptr child \<rightarrow>\<^sub>h h'
|
||||||
|
\<Longrightarrow> heap_is_wellformed h'"
|
||||||
|
|
||||||
interpretation i_append_child_wf?: l_append_child_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_owner_document get_parent
|
interpretation i_append_child_wf?: l_append_child_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_owner_document get_parent
|
||||||
get_parent_locs remove_child remove_child_locs
|
get_parent_locs remove_child remove_child_locs
|
||||||
get_disconnected_nodes get_disconnected_nodes_locs
|
get_disconnected_nodes get_disconnected_nodes_locs
|
||||||
|
@ -5300,6 +5341,9 @@ interpretation i_append_child_wf?: l_append_child_wf\<^sub>C\<^sub>o\<^sub>r\<^s
|
||||||
parent_child_rel
|
parent_child_rel
|
||||||
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)
|
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)
|
||||||
|
using append_child_heap_is_wellformed_preserved by fast+
|
||||||
|
|
||||||
|
|
||||||
subsection \<open>create\_element\<close>
|
subsection \<open>create\_element\<close>
|
||||||
|
|
Reference in New Issue