forked from afp-mirror/Core_DOM
Merged scope_components into master.
This commit is contained in:
Michael Herzberg
commit
2c86c19a42
|
|
@ -47,30 +47,75 @@ locale l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^su
|
|||
begin
|
||||
definition a_owner_document_valid :: "(_) heap \<Rightarrow> bool"
|
||||
where
|
||||
"a_owner_document_valid h = (\<forall>node_ptr. node_ptr |\<in>| node_ptr_kinds h \<longrightarrow>
|
||||
"a_owner_document_valid h \<longleftrightarrow> (\<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)))"
|
||||
|
||||
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)
|
||||
proof -
|
||||
fix x
|
||||
assume 1: " \<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)"
|
||||
assume 2: "x |\<in>| node_ptr_kinds h"
|
||||
assume 3: "x |\<notin>| fset_of_list (concat (map (\<lambda>parent. |h \<turnstile> get_disconnected_nodes parent|\<^sub>r) (sorted_list_of_fset (document_ptr_kinds h))))"
|
||||
have "\<not>(\<exists>document_ptr. document_ptr |\<in>| document_ptr_kinds h \<and> x \<in> set |h \<turnstile> get_disconnected_nodes document_ptr|\<^sub>r)"
|
||||
using 1 2 3
|
||||
by (smt UN_I fset_of_list_elem image_eqI notin_fset set_concat set_map sorted_list_of_fset_simps(1))
|
||||
then
|
||||
have "(\<exists>parent_ptr. parent_ptr |\<in>| object_ptr_kinds h \<and> x \<in> set |h \<turnstile> get_child_nodes parent_ptr|\<^sub>r)"
|
||||
using 1 2
|
||||
by auto
|
||||
then obtain parent_ptr where parent_ptr: "parent_ptr |\<in>| object_ptr_kinds h \<and> x \<in> set |h \<turnstile> get_child_nodes parent_ptr|\<^sub>r"
|
||||
by auto
|
||||
moreover have "parent_ptr \<in> set (sorted_list_of_fset (object_ptr_kinds h))"
|
||||
using parent_ptr by auto
|
||||
moreover have "|h \<turnstile> get_child_nodes parent_ptr|\<^sub>r \<in> set (map (\<lambda>parent. |h \<turnstile> get_child_nodes parent|\<^sub>r) (sorted_list_of_fset (object_ptr_kinds h)))"
|
||||
using calculation(2) by auto
|
||||
ultimately
|
||||
show "x |\<in>| fset_of_list (concat (map (\<lambda>parent. |h \<turnstile> get_child_nodes parent|\<^sub>r) (sorted_list_of_fset (object_ptr_kinds h))))"
|
||||
using fset_of_list_elem by fastforce
|
||||
next
|
||||
fix node_ptr
|
||||
assume 1: "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)))) |\<union>| fset_of_list (concat (map (\<lambda>parent. |h \<turnstile> get_disconnected_nodes parent|\<^sub>r) (sorted_list_of_fset (document_ptr_kinds h))))"
|
||||
assume 2: "node_ptr |\<in>| node_ptr_kinds h"
|
||||
assume 3: "\<forall>parent_ptr. parent_ptr |\<in>| object_ptr_kinds h \<longrightarrow> node_ptr \<notin> set |h \<turnstile> get_child_nodes parent_ptr|\<^sub>r"
|
||||
have "node_ptr \<in> set (concat (map (\<lambda>parent. |h \<turnstile> get_child_nodes parent|\<^sub>r) (sorted_list_of_fset (object_ptr_kinds h)))) \<or> node_ptr \<in> set (concat (map (\<lambda>parent. |h \<turnstile> get_disconnected_nodes parent|\<^sub>r) (sorted_list_of_fset (document_ptr_kinds h))))"
|
||||
using 1 2
|
||||
by (meson fin_mono fset_of_list_elem funion_iff)
|
||||
then
|
||||
show "\<exists>document_ptr. document_ptr |\<in>| document_ptr_kinds h \<and> node_ptr \<in> set |h \<turnstile> get_disconnected_nodes document_ptr|\<^sub>r"
|
||||
using 3
|
||||
by auto
|
||||
qed
|
||||
|
||||
definition a_parent_child_rel :: "(_) heap \<Rightarrow> ((_) object_ptr \<times> (_) object_ptr) set"
|
||||
where
|
||||
"a_parent_child_rel h = {(parent, child). parent |\<in>| object_ptr_kinds h
|
||||
\<and> child \<in> cast ` set |h \<turnstile> get_child_nodes parent|\<^sub>r}"
|
||||
|
||||
lemma a_parent_child_rel_code [code]: "a_parent_child_rel h = set (concat (map
|
||||
(\<lambda>parent. map
|
||||
(\<lambda>child. (parent, 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))
|
||||
|h \<turnstile> get_child_nodes parent|\<^sub>r)
|
||||
(sorted_list_of_fset (object_ptr_kinds h)))
|
||||
)"
|
||||
by(auto simp add: a_parent_child_rel_def)
|
||||
|
||||
definition a_acyclic_heap :: "(_) heap \<Rightarrow> bool"
|
||||
where
|
||||
"a_acyclic_heap h = acyclic (a_parent_child_rel h)"
|
||||
|
||||
|
||||
definition a_all_ptrs_in_heap :: "(_) heap \<Rightarrow> bool"
|
||||
where
|
||||
"a_all_ptrs_in_heap h = ((\<forall>ptr children. (h \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children)
|
||||
\<longrightarrow> fset_of_list children |\<subseteq>| node_ptr_kinds h)
|
||||
\<and> (\<forall>document_ptr disc_node_ptrs. (h \<turnstile> get_disconnected_nodes document_ptr \<rightarrow>\<^sub>r disc_node_ptrs)
|
||||
\<longrightarrow> fset_of_list disc_node_ptrs |\<subseteq>| node_ptr_kinds h))"
|
||||
|
||||
"a_all_ptrs_in_heap h \<longleftrightarrow>
|
||||
(\<forall>ptr \<in> fset (object_ptr_kinds h). set |h \<turnstile> get_child_nodes ptr|\<^sub>r \<subseteq> fset (node_ptr_kinds h)) \<and>
|
||||
(\<forall>document_ptr \<in> fset (document_ptr_kinds h). set |h \<turnstile> get_disconnected_nodes document_ptr|\<^sub>r \<subseteq> fset (node_ptr_kinds h))"
|
||||
|
||||
definition a_distinct_lists :: "(_) heap \<Rightarrow> bool"
|
||||
where
|
||||
|
|
@ -94,8 +139,13 @@ global_interpretation l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub
|
|||
defines heap_is_wellformed = "l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.a_heap_is_wellformed get_child_nodes
|
||||
get_disconnected_nodes"
|
||||
and parent_child_rel = "l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.a_parent_child_rel get_child_nodes"
|
||||
and acyclic_heap = a_acyclic_heap
|
||||
and all_ptrs_in_heap = a_all_ptrs_in_heap
|
||||
and distinct_lists = a_distinct_lists
|
||||
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
|
||||
|
|
@ -218,7 +268,7 @@ lemma heap_is_wellformed_children_in_heap:
|
|||
shows "child |\<in>| node_ptr_kinds h"
|
||||
using assms
|
||||
apply(auto simp add: heap_is_wellformed_def a_all_ptrs_in_heap_def)[1]
|
||||
by (meson fset_of_list_elem fset_rev_mp)
|
||||
by (metis (no_types, lifting) finite_set_in is_OK_returns_result_I local.get_child_nodes_ptr_in_heap select_result_I2 subsetD)
|
||||
|
||||
lemma heap_is_wellformed_one_parent:
|
||||
assumes "heap_is_wellformed h"
|
||||
|
|
@ -267,12 +317,12 @@ lemma parent_child_rel_child_in_heap:
|
|||
\<Longrightarrow> (parent, child_ptr) \<in> parent_child_rel h \<Longrightarrow> child_ptr |\<in>| object_ptr_kinds h"
|
||||
apply(auto simp add: heap_is_wellformed_def parent_child_rel_def a_all_ptrs_in_heap_def)[1]
|
||||
using get_child_nodes_ok
|
||||
by (meson fin_mono fset_of_list_elem returns_result_select_result)
|
||||
by (meson finite_set_in subsetD)
|
||||
|
||||
lemma heap_is_wellformed_disc_nodes_in_heap:
|
||||
"heap_is_wellformed h \<Longrightarrow> h \<turnstile> get_disconnected_nodes document_ptr \<rightarrow>\<^sub>r disc_nodes
|
||||
\<Longrightarrow> node \<in> set disc_nodes \<Longrightarrow> node |\<in>| node_ptr_kinds h"
|
||||
by (meson fset_mp fset_of_list_elem local.a_all_ptrs_in_heap_def local.heap_is_wellformed_def)
|
||||
by (metis (no_types, lifting) finite_set_in is_OK_returns_result_I local.a_all_ptrs_in_heap_def local.get_disconnected_nodes_ptr_in_heap local.heap_is_wellformed_def select_result_I2 subsetD)
|
||||
|
||||
lemma heap_is_wellformed_one_disc_parent:
|
||||
"heap_is_wellformed h \<Longrightarrow> h \<turnstile> get_disconnected_nodes document_ptr \<rightarrow>\<^sub>r disc_nodes
|
||||
|
|
@ -667,8 +717,7 @@ proof -
|
|||
moreover have "a_all_ptrs_in_heap h"
|
||||
using heap_is_wellformed by (simp add: heap_is_wellformed_def)
|
||||
then have "a_all_ptrs_in_heap h'"
|
||||
by(auto simp add: a_all_ptrs_in_heap_def node_ptr_kinds_def node_ptr_kinds_eq2
|
||||
object_ptr_kinds_eq3 children_eq disconnected_nodes_eq)
|
||||
by (simp add: children_eq2 disconnected_nodes_eq2 document_ptr_kinds_eq3 l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.a_all_ptrs_in_heap_def node_ptr_kinds_eq3 object_ptr_kinds_eq3)
|
||||
|
||||
moreover have h0: "a_distinct_lists h"
|
||||
using heap_is_wellformed by (simp add: heap_is_wellformed_def)
|
||||
|
|
@ -2494,7 +2543,7 @@ subsection \<open>get\_owner\_document\<close>
|
|||
locale l_get_owner_document_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
|
||||
l_known_ptrs
|
||||
+ l_heap_is_wellformed
|
||||
+ l_get_root_node
|
||||
+ l_get_root_node\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
|
||||
+ l_get_ancestors
|
||||
+ l_get_ancestors_wf
|
||||
+ l_get_parent
|
||||
|
|
@ -2807,6 +2856,88 @@ proof -
|
|||
apply (simp add: assms(1) assms(2) assms(3) local.get_root_node_ok)
|
||||
using assms(3) local.get_disconnected_nodes_ok by blast
|
||||
qed
|
||||
|
||||
lemma get_owner_document_child_same:
|
||||
assumes "heap_is_wellformed h" "known_ptrs h" "type_wf h"
|
||||
assumes "h \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children"
|
||||
assumes "child \<in> set children"
|
||||
shows "h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document \<longleftrightarrow> h \<turnstile> get_owner_document (cast child) \<rightarrow>\<^sub>r owner_document"
|
||||
proof -
|
||||
have "ptr |\<in>| object_ptr_kinds h"
|
||||
by (meson assms(4) is_OK_returns_result_I local.get_child_nodes_ptr_in_heap)
|
||||
then have "known_ptr ptr"
|
||||
using assms(2) local.known_ptrs_known_ptr by blast
|
||||
|
||||
have "cast child |\<in>| object_ptr_kinds h"
|
||||
using assms(1) assms(4) assms(5) local.heap_is_wellformed_children_in_heap node_ptr_kinds_commutes by blast
|
||||
then
|
||||
have "known_ptr (cast child)"
|
||||
using assms(2) local.known_ptrs_known_ptr by blast
|
||||
|
||||
obtain root where root: "h \<turnstile> get_root_node ptr \<rightarrow>\<^sub>r root"
|
||||
by (meson \<open>ptr |\<in>| object_ptr_kinds h\<close> assms(1) assms(2) assms(3) is_OK_returns_result_E local.get_root_node_ok)
|
||||
then have "h \<turnstile> get_root_node (cast child) \<rightarrow>\<^sub>r root"
|
||||
using assms(1) assms(2) assms(3) assms(4) assms(5) local.child_parent_dual local.get_root_node_parent_same by blast
|
||||
|
||||
have "h \<turnstile> get_owner_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"
|
||||
proof (cases "is_document_ptr ptr")
|
||||
case True
|
||||
then obtain document_ptr where document_ptr: "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 document_ptr = ptr"
|
||||
using case_optionE document_ptr_casts_commute by blast
|
||||
then have "root = cast document_ptr"
|
||||
using root
|
||||
by(auto simp add: get_root_node_def get_ancestors_def elim!: bind_returns_result_E2 split: option.splits)
|
||||
|
||||
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)
|
||||
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(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>ptr |\<in>| object_ptr_kinds h\<close> True
|
||||
by(auto simp add: document_ptr[symmetric] intro!: bind_pure_returns_result_I split: option.splits)
|
||||
next
|
||||
case False
|
||||
then obtain node_ptr where node_ptr: "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 node_ptr = ptr"
|
||||
using \<open>known_ptr ptr\<close>
|
||||
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 "h \<turnstile> 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 \<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 root \<open>h \<turnstile> get_root_node (cast child) \<rightarrow>\<^sub>r root\<close>
|
||||
unfolding a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def
|
||||
by (meson bind_pure_returns_result_I bind_returns_result_E3 local.get_root_node_pure)
|
||||
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(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> False
|
||||
apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )
|
||||
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)
|
||||
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(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)
|
||||
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
|
||||
|
||||
end
|
||||
|
||||
locale l_get_owner_document_wf = l_heap_is_wellformed_defs + l_type_wf + l_known_ptrs
|
||||
|
|
@ -2833,16 +2964,11 @@ locale l_get_owner_document_wf = l_heap_is_wellformed_defs + l_type_wf + l_known
|
|||
"heap_is_wellformed h \<Longrightarrow> known_ptrs h \<Longrightarrow> type_wf h \<Longrightarrow> ptr |\<in>| object_ptr_kinds h
|
||||
\<Longrightarrow> h \<turnstile> ok (get_owner_document ptr)"
|
||||
|
||||
|
||||
interpretation i_get_owner_document_wf?:
|
||||
l_get_owner_document_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M known_ptr known_ptrs type_wf heap_is_wellformed parent_child_rel
|
||||
get_child_nodes get_child_nodes_locs get_disconnected_nodes get_disconnected_nodes_locs
|
||||
get_root_node get_root_node_locs get_parent get_parent_locs get_ancestors get_ancestors_locs
|
||||
get_owner_document
|
||||
by(simp add: l_get_owner_document_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
|
||||
interpretation i_get_owner_document_wf?: l_get_owner_document_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
|
||||
known_ptr known_ptrs type_wf heap_is_wellformed parent_child_rel get_child_nodes get_child_nodes_locs get_disconnected_nodes get_disconnected_nodes_locs get_parent get_parent_locs get_ancestors get_ancestors_locs get_root_node get_root_node_locs get_owner_document
|
||||
by(auto simp add: l_get_owner_document_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
|
||||
declare l_get_owner_document_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]
|
||||
|
||||
|
||||
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"
|
||||
|
|
@ -3451,35 +3577,20 @@ have "type_wf h2"
|
|||
using assms(1) by (simp add: heap_is_wellformed_def)
|
||||
then have "a_all_ptrs_in_heap h'"
|
||||
apply(auto simp add: a_all_ptrs_in_heap_def node_ptr_kinds_eq3 disconnected_nodes_eq)[1]
|
||||
apply (metis (no_types, lifting) type_wf assms(3) children_eq2 children_h children_h'
|
||||
fset_of_list_subset fsubsetD get_child_nodes_ok get_child_nodes_ptr_in_heap
|
||||
is_OK_returns_result_E is_OK_returns_result_I local.known_ptrs_known_ptr
|
||||
object_ptr_kinds_eq3 select_result_I2 set_remove1_subset)
|
||||
by (metis (no_types, lifting)
|
||||
\<open>\<And>thesis. (\<And>owner_document children_h h2 disconnected_nodes_h.
|
||||
\<lbrakk>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;
|
||||
h \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children_h; child \<in> set children_h;
|
||||
h \<turnstile> get_disconnected_nodes owner_document \<rightarrow>\<^sub>r disconnected_nodes_h;
|
||||
h \<turnstile> set_disconnected_nodes owner_document (child # disconnected_nodes_h) \<rightarrow>\<^sub>h h2;
|
||||
h2 \<turnstile> set_child_nodes ptr (remove1 child children_h) \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close>
|
||||
disconnected_nodes_h disconnected_nodes_eq disconnected_nodes_h' fset_mp fset_of_list_elem
|
||||
returns_result_eq set_ConsD)
|
||||
|
||||
apply (metis (no_types, lifting) \<open>type_wf h'\<close> assms(2) assms(3) local.get_child_nodes_ok local.known_ptrs_known_ptr local.remove_child_children_subset notin_fset object_ptr_kinds_eq3 returns_result_select_result subset_code(1) type_wf)
|
||||
apply (metis (no_types, lifting) assms(2) disconnected_nodes_eq2 disconnected_nodes_h disconnected_nodes_h' document_ptr_kinds_eq3 finite_set_in local.remove_child_child_in_heap node_ptr_kinds_eq3 select_result_I2 set_ConsD subset_code(1))
|
||||
done
|
||||
moreover have "a_owner_document_valid h"
|
||||
using assms(1) 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_eq3 document_ptr_kinds_eq3
|
||||
node_ptr_kinds_eq3)[1]
|
||||
proof -
|
||||
fix node_ptr
|
||||
assume 0: "\<forall>node_ptr. node_ptr |\<in>| node_ptr_kinds h'
|
||||
\<longrightarrow> (\<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"
|
||||
|
||||
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"
|
||||
then show "\<exists>document_ptr. document_ptr |\<in>| document_ptr_kinds h'
|
||||
\<and> node_ptr \<in> set |h' \<turnstile> get_disconnected_nodes document_ptr|\<^sub>r"
|
||||
proof (cases "node_ptr = child")
|
||||
|
|
@ -3495,7 +3606,7 @@ have "type_wf h2"
|
|||
using 0 1 2 children_eq2 children_h children_h' disconnected_nodes_eq2 disconnected_nodes_h
|
||||
disconnected_nodes_h'
|
||||
apply(auto simp add: children_eq2 disconnected_nodes_eq2 dest!: select_result_I2)[1]
|
||||
by (metis children_eq2 disconnected_nodes_eq2 in_set_remove1 list.set_intros(2))
|
||||
by (metis children_eq2 disconnected_nodes_eq2 finite_set_in in_set_remove1 list.set_intros(2))
|
||||
qed
|
||||
qed
|
||||
|
||||
|
|
@ -4399,29 +4510,20 @@ proof -
|
|||
using wellformed_h2 by (simp add: heap_is_wellformed_def)
|
||||
then have "a_all_ptrs_in_heap h3"
|
||||
apply(auto simp add: a_all_ptrs_in_heap_def node_ptr_kinds_eq3_h2 children_eq_h2)[1]
|
||||
by (metis (mono_tags, lifting) disc_nodes_old_document_h2 disc_nodes_old_document_h3
|
||||
disconnected_nodes_eq_h2 fset_of_list_elem fset_rev_mp returns_result_eq
|
||||
set_remove1_subset subsetCE)
|
||||
apply (simp add: children_eq2_h2 object_ptr_kinds_h2_eq3 subset_code(1))
|
||||
by (metis (no_types, lifting) \<open>child \<in> set disc_nodes_old_document_h2\<close> \<open>type_wf h2\<close> disc_nodes_old_document_h2 disc_nodes_old_document_h3 disconnected_nodes_eq2_h2 document_ptr_kinds_eq3_h2 in_set_remove1 local.get_disconnected_nodes_ok local.heap_is_wellformed_disc_nodes_in_heap node_ptr_kinds_eq3_h2 returns_result_select_result select_result_I2 wellformed_h2)
|
||||
then have "a_all_ptrs_in_heap h'"
|
||||
apply(auto simp add: a_all_ptrs_in_heap_def node_ptr_kinds_eq3_h3 children_eq_h3)[1]
|
||||
by (metis (no_types) NodeMonad.ptr_kinds_ptr_kinds_M child_in_heap disc_nodes_document_ptr_h'
|
||||
disc_nodes_document_ptr_h3 disconnected_nodes_eq_h3 fset_mp fset_of_list_elem
|
||||
node_ptr_kinds_eq_h node_ptr_kinds_eq_h2 node_ptr_kinds_eq_h3 select_result_I2
|
||||
set_ConsD)
|
||||
apply (simp add: children_eq2_h3 object_ptr_kinds_h3_eq3 subset_code(1))
|
||||
by (metis (no_types, lifting) \<open>child \<in> set disc_nodes_old_document_h2\<close> disc_nodes_document_ptr_h' disc_nodes_document_ptr_h2 disc_nodes_old_document_h2 disconnected_nodes_eq2_h3 document_ptr_kinds_eq3_h3 finite_set_in local.heap_is_wellformed_disc_nodes_in_heap node_ptr_kinds_eq3_h2 node_ptr_kinds_eq3_h3 select_result_I2 set_ConsD subset_code(1) wellformed_h2)
|
||||
|
||||
moreover have "a_owner_document_valid h2"
|
||||
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 (metis (no_types) 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)
|
||||
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)
|
||||
|
|
@ -5120,46 +5222,46 @@ 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]
|
||||
by (metis (no_types, lifting) NodeMonad.ptr_kinds_ptr_kinds_M disconnected_nodes_eq_h2
|
||||
disconnected_nodes_h2 disconnected_nodes_h3 fset_mp fset_of_list_subset
|
||||
node_ptr_kinds_eq2_h2 select_result_I2 set_remove1_subset)
|
||||
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)
|
||||
by (metis (no_types, lifting) disconnected_nodes_eq2_h2 disconnected_nodes_h2 disconnected_nodes_h3 document_ptr_kinds_commutes finite_set_in node_ptr_kinds_commutes object_ptr_kinds_M_eq3_h2 select_result_I2 set_remove1_subset subsetD)
|
||||
|
||||
have "set children_h3 \<subseteq> set |h' \<turnstile> node_ptr_kinds_M|\<^sub>r"
|
||||
using children_h3 \<open>a_all_ptrs_in_heap h3\<close>
|
||||
apply(auto simp add: a_all_ptrs_in_heap_def node_ptr_kinds_eq2_h3)[1]
|
||||
by (metis (no_types, hide_lams) fset_mp fset_of_list_elem node_ptr_kinds_commutes object_ptr_kinds_M_eq3_h')
|
||||
by (metis children_eq_h2 l_heap_is_wellformed.heap_is_wellformed_children_in_heap local.l_heap_is_wellformed_axioms node_ptr_kinds_commutes object_ptr_kinds_M_eq3_h' object_ptr_kinds_M_eq3_h2 wellformed_h2)
|
||||
|
||||
then have "set (insert_before_list node reference_child children_h3) \<subseteq> set |h' \<turnstile> node_ptr_kinds_M|\<^sub>r"
|
||||
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'
|
||||
by (metis (no_types, hide_lams) NodeMonad.ptr_kinds_ptr_kinds_M
|
||||
\<open>set (insert_before_list node reference_child children_h3) \<subseteq> set |h' \<turnstile> node_ptr_kinds_M|\<^sub>r\<close>
|
||||
fset.map_comp fset_mp fset_of_list_elem node_ptr_kinds_def node_ptr_kinds_eq2_h3
|
||||
returns_result_eq subsetCE)
|
||||
qed
|
||||
|
||||
|
||||
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
|
||||
|
||||
moreover have "a_distinct_lists h2"
|
||||
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
|
||||
|
|
@ -5186,17 +5288,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
|
||||
|
|
@ -5211,10 +5313,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
|
||||
|
|
@ -5229,11 +5331,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"
|
||||
|
|
@ -5242,7 +5344,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
|
||||
|
|
@ -5268,9 +5370,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
|
||||
|
|
@ -5280,10 +5382,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
|
||||
|
|
@ -5316,13 +5418,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
|
||||
|
|
@ -5333,33 +5435,13 @@ 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]
|
||||
proof -
|
||||
fix node_ptr
|
||||
assume 0: "\<forall>node_ptr. node_ptr |\<in>| node_ptr_kinds h'
|
||||
\<longrightarrow> (\<exists>document_ptr. document_ptr |\<in>| document_ptr_kinds h'
|
||||
\<and> node_ptr \<in> set |h2 \<turnstile> get_disconnected_nodes document_ptr|\<^sub>r)
|
||||
\<or> (\<exists>parent_ptr. parent_ptr |\<in>| object_ptr_kinds h'
|
||||
\<and> node_ptr \<in> set |h3 \<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"
|
||||
then have "(\<exists>document_ptr. document_ptr |\<in>| document_ptr_kinds h'
|
||||
\<and> node_ptr \<in> set |h2 \<turnstile> get_disconnected_nodes document_ptr|\<^sub>r)"
|
||||
by (metis (no_types, lifting) children_eq2_h3 children_h' children_h3
|
||||
insert_before_list_in_set select_result_I2)
|
||||
then show "\<exists>document_ptr. document_ptr |\<in>| document_ptr_kinds h'
|
||||
\<and> node_ptr \<in> set |h3 \<turnstile> get_disconnected_nodes document_ptr|\<^sub>r"
|
||||
by (metis (no_types, hide_lams) "2" children_h' disconnected_nodes_eq2_h2
|
||||
disconnected_nodes_h2 disconnected_nodes_h3 in_set_remove1
|
||||
insert_before_list_in_set object_ptr_kinds_M_eq3_h'
|
||||
ptr_in_heap select_result_I2)
|
||||
qed
|
||||
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)
|
||||
|
||||
ultimately show "heap_is_wellformed h'"
|
||||
by (simp add: heap_is_wellformed_def)
|
||||
|
|
@ -5764,7 +5846,7 @@ proof -
|
|||
using \<open>heap_is_wellformed h\<close>
|
||||
using \<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>
|
||||
a_all_ptrs_in_heap_def heap_is_wellformed_def
|
||||
by (meson NodeMonad.ptr_kinds_ptr_kinds_M fset_mp fset_of_list_elem )
|
||||
using NodeMonad.ptr_kinds_ptr_kinds_M local.heap_is_wellformed_disc_nodes_in_heap by blast
|
||||
|
||||
have "acyclic (parent_child_rel h)"
|
||||
using \<open>heap_is_wellformed h\<close>
|
||||
|
|
@ -5810,21 +5892,12 @@ proof -
|
|||
using \<open>heap_is_wellformed h\<close> by (simp add: heap_is_wellformed_def)
|
||||
then have "a_all_ptrs_in_heap h2"
|
||||
apply(auto simp add: a_all_ptrs_in_heap_def)[1]
|
||||
using node_ptr_kinds_eq_h
|
||||
\<open>cast new_element_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close>
|
||||
\<open>h2 \<turnstile> get_child_nodes (cast new_element_ptr) \<rightarrow>\<^sub>r []\<close>
|
||||
apply (metis (no_types, hide_lams) children_eq_h fempty_iff fset_mp fset_of_list_simps(1)
|
||||
funionCI select_result_I2)
|
||||
by (simp add: disconnected_nodes_eq_h fset_rev_mp node_ptr_kinds_eq_h)
|
||||
apply (metis \<open>known_ptrs h2\<close> \<open>parent_child_rel h = parent_child_rel h2\<close> \<open>type_wf h2\<close> assms(1) assms(3) funion_iff local.get_child_nodes_ok local.known_ptrs_known_ptr local.parent_child_rel_child_in_heap local.parent_child_rel_child_nodes2 node_ptr_kinds_commutes node_ptr_kinds_eq_h returns_result_select_result)
|
||||
by (metis assms(1) assms(3) disconnected_nodes_eq2_h document_ptr_kinds_eq_h funion_iff 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(auto simp add: a_all_ptrs_in_heap_def object_ptr_kinds_eq_h2 node_ptr_kinds_def
|
||||
children_eq_h2 disconnected_nodes_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'"
|
||||
apply(auto simp add: a_all_ptrs_in_heap_def object_ptr_kinds_eq_h3 node_ptr_kinds_def children_eq_h3 )[1]
|
||||
using disconnected_nodes_eq_h3 object_ptr_kinds_eq_h object_ptr_kinds_eq_h2
|
||||
by (metis (no_types, lifting) disc_nodes_h3 finsertCI fset.map_comp fset_mp fset_of_list_elem
|
||||
funion_finsert_right h' local.set_disconnected_nodes_get_disconnected_nodes
|
||||
node_ptr_kinds_def node_ptr_kinds_eq_h select_result_I2 set_ConsD)
|
||||
by (smt \<open>h2 \<turnstile> get_child_nodes (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>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_element_ptr) \<rightarrow>\<^sub>r []\<close> 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' is_OK_returns_result_I l_set_disconnected_nodes_get_disconnected_nodes.set_disconnected_nodes_get_disconnected_nodes local.a_all_ptrs_in_heap_def local.get_child_nodes_ptr_in_heap local.l_set_disconnected_nodes_get_disconnected_nodes_axioms node_ptr_kinds_commutes object_ptr_kinds_eq_h2 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_element_ptr \<notin> set |h \<turnstile> get_child_nodes p|\<^sub>r"
|
||||
using \<open>heap_is_wellformed h\<close> \<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>
|
||||
|
|
@ -5893,24 +5966,8 @@ proof -
|
|||
ultimately show "False"
|
||||
apply(-)
|
||||
apply(cases "x = document_ptr")
|
||||
apply (metis (no_types) NodeMonad.ptr_kinds_ptr_kinds_M
|
||||
\<open>a_all_ptrs_in_heap h\<close>
|
||||
\<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>
|
||||
a_all_ptrs_in_heap_def assms(3) 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 fset_mp fset_of_list_elem
|
||||
get_disconnected_nodes_ok h' returns_result_select_result select_result_I2
|
||||
set_ConsD set_disconnected_nodes_get_disconnected_nodes)
|
||||
apply(cases "y = document_ptr" )
|
||||
apply (metis (no_types) NodeMonad.ptr_kinds_ptr_kinds_M
|
||||
\<open>a_all_ptrs_in_heap h\<close>
|
||||
\<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>
|
||||
a_all_ptrs_in_heap_def assms(3) 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 fset_mp fset_of_list_elem
|
||||
get_disconnected_nodes_ok h' returns_result_select_result select_result_I2
|
||||
set_ConsD set_disconnected_nodes_get_disconnected_nodes)
|
||||
using disconnected_nodes_eq2_h3 by auto
|
||||
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)
|
||||
|
|
@ -5949,27 +6006,8 @@ 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)
|
||||
proof -
|
||||
fix node_ptr :: "(_) node_ptr"
|
||||
assume a1: "\<forall>node_ptr. node_ptr |\<in>| node_ptr_kinds h \<longrightarrow> (\<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)"
|
||||
assume a2: "node_ptr |\<in>| node_ptr_kinds h"
|
||||
assume a3: "\<forall>parent_ptr. (parent_ptr = 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>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_element_ptr \<longrightarrow> node_ptr \<notin> set |h' \<turnstile> get_child_nodes (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>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_element_ptr)|\<^sub>r) \<and> (parent_ptr |\<in>| object_ptr_kinds h \<longrightarrow> node_ptr \<notin> set |h' \<turnstile> get_child_nodes parent_ptr|\<^sub>r)"
|
||||
assume a4: "document_ptr |\<in>| document_ptr_kinds h"
|
||||
assume a5: "h3 \<turnstile> get_disconnected_nodes document_ptr \<rightarrow>\<^sub>r disc_nodes_h3"
|
||||
obtain dd :: "(_) node_ptr \<Rightarrow> (_) document_ptr" where
|
||||
"\<forall>x0. (\<exists>v1. v1 |\<in>| document_ptr_kinds h \<and> x0 \<in> set |h \<turnstile> get_disconnected_nodes v1|\<^sub>r) = (dd x0 |\<in>| document_ptr_kinds h \<and> x0 \<in> set |h \<turnstile> get_disconnected_nodes (dd x0)|\<^sub>r)"
|
||||
by moura
|
||||
then have f6: "dd node_ptr |\<in>| document_ptr_kinds h \<and> node_ptr \<in> set |h \<turnstile> get_disconnected_nodes (dd node_ptr)|\<^sub>r"
|
||||
using a3 a2 a1 by (metis (no_types) \<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>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_element_ptr \<notin> set |h \<turnstile> object_ptr_kinds_M|\<^sub>r\<close> children_eq2_h children_eq2_h2 children_eq2_h3 l_ptr_kinds_M.ptr_kinds_ptr_kinds_M object_ptr_kinds_M_def)
|
||||
moreover
|
||||
{ assume "|h \<turnstile> get_disconnected_nodes (dd node_ptr)|\<^sub>r \<noteq> disc_nodes_h3"
|
||||
then have "document_ptr \<noteq> dd node_ptr"
|
||||
using a5 disconnected_nodes_eq2_h disconnected_nodes_eq2_h2 by force
|
||||
then have "\<exists>d. d |\<in>| document_ptr_kinds h2 \<and> node_ptr \<in> set |h' \<turnstile> get_disconnected_nodes d|\<^sub>r"
|
||||
using f6 disconnected_nodes_eq2_h disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 document_ptr_kinds_eq_h by auto }
|
||||
ultimately show "\<exists>d. d |\<in>| document_ptr_kinds h2 \<and> node_ptr \<in> set |h' \<turnstile> get_disconnected_nodes d|\<^sub>r"
|
||||
using a4 by (metis (no_types) document_ptr_kinds_eq_h h' insert_iff list.set(2) local.set_disconnected_nodes_get_disconnected_nodes select_result_I2)
|
||||
qed
|
||||
by(metis (no_types, lifting) 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> children_eq2_h children_eq2_h2 children_eq2_h3 disconnected_nodes_eq2_h disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 document_ptr_kinds_eq_h finite_set_in h' 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 node_ptr_kinds_commutes select_result_I2)
|
||||
|
||||
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)
|
||||
|
|
@ -6241,7 +6279,7 @@ proof -
|
|||
then have "cast new_character_data_ptr \<notin> set disc_nodes_h3"
|
||||
using \<open>heap_is_wellformed h\<close> using \<open>cast new_character_data_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close>
|
||||
a_all_ptrs_in_heap_def heap_is_wellformed_def
|
||||
by (meson NodeMonad.ptr_kinds_ptr_kinds_M fset_mp fset_of_list_elem )
|
||||
using NodeMonad.ptr_kinds_ptr_kinds_M local.heap_is_wellformed_disc_nodes_in_heap by blast
|
||||
|
||||
have "acyclic (parent_child_rel h)"
|
||||
using \<open>heap_is_wellformed h\<close>
|
||||
|
|
@ -6288,19 +6326,14 @@ 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, hide_lams) children_eq_h fempty_iff fset_mp fset_of_list_simps(1)
|
||||
funionCI select_result_I2)
|
||||
by (simp add: disconnected_nodes_eq_h fset_rev_mp node_ptr_kinds_eq_h)
|
||||
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(auto simp add: a_all_ptrs_in_heap_def object_ptr_kinds_eq_h2 node_ptr_kinds_def
|
||||
children_eq_h2 disconnected_nodes_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'"
|
||||
apply(auto simp add: a_all_ptrs_in_heap_def object_ptr_kinds_eq_h3 node_ptr_kinds_def
|
||||
children_eq_h3 )[1]
|
||||
using disconnected_nodes_eq_h3 object_ptr_kinds_eq_h object_ptr_kinds_eq_h2
|
||||
by (metis (no_types, lifting) disc_nodes_h3 finsertCI fset.map_comp fset_mp fset_of_list_elem
|
||||
funion_finsert_right h' local.set_disconnected_nodes_get_disconnected_nodes
|
||||
node_ptr_kinds_def node_ptr_kinds_eq_h select_result_I2 set_ConsD)
|
||||
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>
|
||||
|
|
@ -6364,25 +6397,7 @@ 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"
|
||||
apply(cases "x = document_ptr")
|
||||
apply (metis (no_types) NodeMonad.ptr_kinds_ptr_kinds_M \<open>a_all_ptrs_in_heap h\<close>
|
||||
\<open>cast new_character_data_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close>
|
||||
a_all_ptrs_in_heap_def assms(3) 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 fset_mp
|
||||
fset_of_list_elem get_disconnected_nodes_ok h'
|
||||
returns_result_select_result select_result_I2 set_ConsD
|
||||
set_disconnected_nodes_get_disconnected_nodes)
|
||||
apply(cases "y = document_ptr" )
|
||||
apply (metis (no_types) NodeMonad.ptr_kinds_ptr_kinds_M
|
||||
\<open>a_all_ptrs_in_heap h\<close> \<open>cast new_character_data_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close>
|
||||
a_all_ptrs_in_heap_def assms(3) 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 fset_mp fset_of_list_elem
|
||||
get_disconnected_nodes_ok h' returns_result_select_result select_result_I2 set_ConsD
|
||||
set_disconnected_nodes_get_disconnected_nodes)
|
||||
using disconnected_nodes_eq2_h3 by auto
|
||||
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)
|
||||
|
|
@ -6418,10 +6433,8 @@ 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 (no_types, lifting) ObjectMonad.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>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 h' list.set_intros(2)
|
||||
local.set_disconnected_nodes_get_disconnected_nodes 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'"
|
||||
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>
|
||||
|
|
@ -6530,7 +6543,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)+
|
||||
|
|
@ -6582,19 +6595,13 @@ proof -
|
|||
using \<open>heap_is_wellformed h\<close> by (simp add: heap_is_wellformed_def)
|
||||
then have "a_all_ptrs_in_heap h'"
|
||||
apply(auto simp add: a_all_ptrs_in_heap_def)[1]
|
||||
apply (metis 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)
|
||||
by (metis (no_types, lifting) 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>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>parent_child_rel h = parent_child_rel h'\<close> assms(1) disconnected_nodes_eq_h
|
||||
fset_of_list_elem h' local.heap_is_wellformed_disc_nodes_in_heap
|
||||
local.new_document_no_disconnected_nodes local.parent_child_rel_child
|
||||
local.parent_child_rel_parent_in_heap new_document_ptr node_ptr_kinds_eq
|
||||
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>
|
||||
|
|
@ -6663,12 +6670,7 @@ 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>
|
||||
\<open>new_document_ptr |\<notin>| document_ptr_kinds h\<close> assms(3) assms(4) children_eq
|
||||
children_eq2 disconnected_nodes_eq2_h disconnected_nodes_eq_h
|
||||
is_OK_returns_result_E is_OK_returns_result_I local.get_child_nodes_ok
|
||||
local.get_child_nodes_ptr_in_heap local.get_disconnected_nodes_ok
|
||||
local.get_disconnected_nodes_ptr_in_heap local.known_ptrs_known_ptr node_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>
|
||||
|
|
|
|||
|
|
@ -64,7 +64,8 @@ type_synonym ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'docume
|
|||
= "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr, 'shadow_root_ptr,
|
||||
'Object, 'CharacterData option RCharacterData_ext + 'Node, 'Element) heap"
|
||||
register_default_tvars "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr,
|
||||
'shadow_root_ptr, 'Object, 'Node, 'Element, 'CharacterData) heap"
|
||||
'shadow_root_ptr, 'Object, 'Node, 'Element, 'CharacterData) heap"
|
||||
type_synonym heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l = "(unit, unit, unit, unit, unit, unit, unit, unit, unit, unit) heap"
|
||||
|
||||
|
||||
definition character_data_ptr_kinds :: "(_) heap \<Rightarrow> (_) character_data_ptr fset"
|
||||
|
|
@ -139,8 +140,8 @@ begin
|
|||
definition a_type_wf :: "(_) heap \<Rightarrow> bool"
|
||||
where
|
||||
"a_type_wf h = (ElementClass.type_wf h
|
||||
\<and> (\<forall>character_data_ptr. character_data_ptr |\<in>| character_data_ptr_kinds h
|
||||
\<longrightarrow> get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a character_data_ptr h \<noteq> None))"
|
||||
\<and> (\<forall>character_data_ptr \<in> fset (character_data_ptr_kinds h).
|
||||
get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a character_data_ptr h \<noteq> None))"
|
||||
end
|
||||
global_interpretation l_type_wf_def\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a defines type_wf = a_type_wf .
|
||||
lemmas type_wf_defs = a_type_wf_def
|
||||
|
|
@ -163,8 +164,7 @@ lemma get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>
|
|||
\<longleftrightarrow> get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a character_data_ptr h \<noteq> None"
|
||||
using l_type_wf\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_axioms assms
|
||||
apply(simp add: type_wf_defs get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def l_type_wf\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def)
|
||||
by (metis NodeClass.get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_type_wf bind_eq_None_conv character_data_ptr_kinds_commutes
|
||||
l_type_wf\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def local.l_type_wf\<^sub>N\<^sub>o\<^sub>d\<^sub>e_axioms option.distinct(1))
|
||||
by (metis assms bind.bind_lzero character_data_ptr_kinds_commutes fmember.rep_eq local.get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_type_wf option.exhaust option.simps(3))
|
||||
end
|
||||
|
||||
global_interpretation l_get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_lemmas type_wf
|
||||
|
|
@ -325,17 +325,18 @@ locale l_known_ptrs\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^su
|
|||
begin
|
||||
definition a_known_ptrs :: "(_) heap \<Rightarrow> bool"
|
||||
where
|
||||
"a_known_ptrs h = (\<forall>ptr. ptr |\<in>| object_ptr_kinds h \<longrightarrow> known_ptr ptr)"
|
||||
"a_known_ptrs h = (\<forall>ptr \<in> fset (object_ptr_kinds h). known_ptr ptr)"
|
||||
|
||||
lemma known_ptrs_known_ptr: "a_known_ptrs h \<Longrightarrow> ptr |\<in>| object_ptr_kinds h \<Longrightarrow> known_ptr ptr"
|
||||
by(simp add: a_known_ptrs_def)
|
||||
apply(simp add: a_known_ptrs_def)
|
||||
using notin_fset by fastforce
|
||||
|
||||
lemma known_ptrs_preserved:
|
||||
"object_ptr_kinds h = object_ptr_kinds h' \<Longrightarrow> a_known_ptrs h = a_known_ptrs h'"
|
||||
by(auto simp add: a_known_ptrs_def)
|
||||
lemma known_ptrs_subset:
|
||||
"object_ptr_kinds h' |\<subseteq>| object_ptr_kinds h \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
||||
by(auto simp add: a_known_ptrs_def)
|
||||
by(simp add: a_known_ptrs_def less_eq_fset.rep_eq subsetD)
|
||||
lemma known_ptrs_new_ptr: "object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|new_ptr|} \<Longrightarrow> known_ptr new_ptr \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
||||
by(simp add: a_known_ptrs_def)
|
||||
end
|
||||
|
|
|
|||
|
|
@ -64,7 +64,8 @@ type_synonym ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'docume
|
|||
'Element, 'CharacterData) heap"
|
||||
register_default_tvars
|
||||
"('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr,
|
||||
'shadow_root_ptr, 'Object, 'Node, 'Element, 'CharacterData, 'Document) heap"
|
||||
'shadow_root_ptr, 'Object, 'Node, 'Element, 'CharacterData, 'Document) heap"
|
||||
type_synonym heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l = "(unit, unit, unit, unit, unit, unit, unit, unit, unit, unit, unit) heap"
|
||||
|
||||
|
||||
definition document_ptr_kinds :: "(_) heap \<Rightarrow> (_) document_ptr fset"
|
||||
|
|
@ -115,7 +116,7 @@ begin
|
|||
definition a_type_wf :: "(_) heap \<Rightarrow> bool"
|
||||
where
|
||||
"a_type_wf h = (CharacterDataClass.type_wf h \<and>
|
||||
(\<forall>document_ptr. document_ptr |\<in>| document_ptr_kinds h \<longrightarrow> get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr h \<noteq> None))"
|
||||
(\<forall>document_ptr \<in> fset (document_ptr_kinds h). get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr h \<noteq> None))"
|
||||
end
|
||||
global_interpretation l_type_wf_def\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t defines type_wf = a_type_wf .
|
||||
lemmas type_wf_defs = a_type_wf_def
|
||||
|
|
@ -135,8 +136,7 @@ lemma get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_type_w
|
|||
shows "document_ptr |\<in>| document_ptr_kinds h \<longleftrightarrow> get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr h \<noteq> None"
|
||||
using l_type_wf\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_axioms assms
|
||||
apply(simp add: type_wf_defs get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def l_type_wf\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)
|
||||
by (metis bind_eq_None_conv document_ptr_kinds_commutes local.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf
|
||||
option.distinct(1))
|
||||
by (metis document_ptr_kinds_commutes fmember.rep_eq is_none_bind is_none_simps(1) is_none_simps(2) local.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf)
|
||||
end
|
||||
|
||||
global_interpretation l_get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_lemmas type_wf by unfold_locales
|
||||
|
|
@ -228,7 +228,7 @@ abbreviation
|
|||
definition new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t :: "(_)heap \<Rightarrow> ((_) document_ptr \<times> (_) heap)"
|
||||
where
|
||||
"new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t h =
|
||||
(let new_document_ptr = document_ptr.Ref (Suc (fMax (document_ptr.the_ref |`| (document_ptrs h))))
|
||||
(let new_document_ptr = document_ptr.Ref (Suc (fMax (finsert 0 (document_ptr.the_ref |`| (document_ptrs h)))))
|
||||
in
|
||||
(new_document_ptr, put new_document_ptr (create_document_obj '''' None []) h))"
|
||||
|
||||
|
|
@ -315,17 +315,18 @@ locale l_known_ptrs\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^su
|
|||
begin
|
||||
definition a_known_ptrs :: "(_) heap \<Rightarrow> bool"
|
||||
where
|
||||
"a_known_ptrs h = (\<forall>ptr. ptr |\<in>| object_ptr_kinds h \<longrightarrow> known_ptr ptr)"
|
||||
"a_known_ptrs h = (\<forall>ptr \<in> fset (object_ptr_kinds h). known_ptr ptr)"
|
||||
|
||||
lemma known_ptrs_known_ptr: "a_known_ptrs h \<Longrightarrow> ptr |\<in>| object_ptr_kinds h \<Longrightarrow> known_ptr ptr"
|
||||
by(simp add: a_known_ptrs_def)
|
||||
apply(simp add: a_known_ptrs_def)
|
||||
using notin_fset by fastforce
|
||||
|
||||
lemma known_ptrs_preserved:
|
||||
"object_ptr_kinds h = object_ptr_kinds h' \<Longrightarrow> a_known_ptrs h = a_known_ptrs h'"
|
||||
by(auto simp add: a_known_ptrs_def)
|
||||
lemma known_ptrs_subset:
|
||||
"object_ptr_kinds h' |\<subseteq>| object_ptr_kinds h \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
||||
by(auto simp add: a_known_ptrs_def)
|
||||
by(simp add: a_known_ptrs_def less_eq_fset.rep_eq subsetD)
|
||||
lemma known_ptrs_new_ptr: "object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|new_ptr|} \<Longrightarrow> known_ptr new_ptr \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
||||
by(simp add: a_known_ptrs_def)
|
||||
end
|
||||
|
|
|
|||
|
|
@ -68,6 +68,7 @@ type_synonym
|
|||
('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Element option) RElement_ext + 'Node) heap"
|
||||
register_default_tvars
|
||||
"('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr, 'shadow_root_ptr, 'Object, 'Node, 'Element) heap"
|
||||
type_synonym heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l = "(unit, unit, unit, unit, unit, unit, unit, unit, unit) heap"
|
||||
|
||||
definition element_ptr_kinds :: "(_) heap \<Rightarrow> (_) element_ptr fset"
|
||||
where
|
||||
|
|
@ -131,8 +132,8 @@ locale l_type_wf_def\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t
|
|||
begin
|
||||
definition a_type_wf :: "(_) heap \<Rightarrow> bool"
|
||||
where
|
||||
"a_type_wf h = (NodeClass.type_wf h \<and> (\<forall>element_ptr. element_ptr |\<in>| element_ptr_kinds h
|
||||
\<longrightarrow> get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr h \<noteq> None))"
|
||||
"a_type_wf h = (NodeClass.type_wf h \<and> (\<forall>element_ptr \<in> fset (element_ptr_kinds h).
|
||||
get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr h \<noteq> None))"
|
||||
end
|
||||
global_interpretation l_type_wf_def\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t defines type_wf = a_type_wf .
|
||||
lemmas type_wf_defs = a_type_wf_def
|
||||
|
|
@ -154,8 +155,8 @@ lemma get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_type_wf:
|
|||
shows "element_ptr |\<in>| element_ptr_kinds h \<longleftrightarrow> get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr h \<noteq> None"
|
||||
using l_type_wf\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_axioms assms
|
||||
apply(simp add: type_wf_defs get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def l_type_wf\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)
|
||||
by (metis NodeClass.get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_type_wf bind_eq_None_conv element_ptr_kinds_commutes
|
||||
option.distinct(1))
|
||||
by (metis NodeClass.get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_type_wf bind_eq_None_conv element_ptr_kinds_commutes notin_fset
|
||||
option.distinct(1))
|
||||
end
|
||||
|
||||
global_interpretation l_get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_lemmas type_wf
|
||||
|
|
@ -290,16 +291,17 @@ locale l_known_ptrs\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t = l_
|
|||
begin
|
||||
definition a_known_ptrs :: "(_) heap \<Rightarrow> bool"
|
||||
where
|
||||
"a_known_ptrs h = (\<forall>ptr. ptr |\<in>| object_ptr_kinds h \<longrightarrow> known_ptr ptr)"
|
||||
"a_known_ptrs h = (\<forall>ptr \<in> fset (object_ptr_kinds h). known_ptr ptr)"
|
||||
|
||||
lemma known_ptrs_known_ptr:
|
||||
"ptr |\<in>| object_ptr_kinds h \<Longrightarrow> a_known_ptrs h \<Longrightarrow> known_ptr ptr"
|
||||
by(simp add: a_known_ptrs_def)
|
||||
apply(simp add: a_known_ptrs_def)
|
||||
using notin_fset by fastforce
|
||||
|
||||
lemma known_ptrs_preserved: "object_ptr_kinds h = object_ptr_kinds h' \<Longrightarrow> a_known_ptrs h = a_known_ptrs h'"
|
||||
by(auto simp add: a_known_ptrs_def)
|
||||
lemma known_ptrs_subset: "object_ptr_kinds h' |\<subseteq>| object_ptr_kinds h \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
||||
by(auto simp add: a_known_ptrs_def)
|
||||
by(simp add: a_known_ptrs_def less_eq_fset.rep_eq subsetD)
|
||||
lemma known_ptrs_new_ptr: "object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|new_ptr|} \<Longrightarrow> known_ptr new_ptr \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
||||
by(simp add: a_known_ptrs_def)
|
||||
end
|
||||
|
|
|
|||
|
|
@ -51,6 +51,7 @@ type_synonym ('object_ptr, 'node_ptr, 'Object, 'Node) heap
|
|||
= "('node_ptr node_ptr + 'object_ptr, 'Node RNode_ext + 'Object) heap"
|
||||
register_default_tvars
|
||||
"('object_ptr, 'node_ptr, 'Object, 'Node) heap"
|
||||
type_synonym heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l = "(unit, unit, unit, unit) heap"
|
||||
|
||||
|
||||
definition node_ptr_kinds :: "(_) heap \<Rightarrow> (_) node_ptr fset"
|
||||
|
|
@ -89,8 +90,7 @@ begin
|
|||
definition a_type_wf :: "(_) heap \<Rightarrow> bool"
|
||||
where
|
||||
"a_type_wf h = (ObjectClass.type_wf h
|
||||
\<and> (\<forall>node_ptr. node_ptr |\<in>| node_ptr_kinds h
|
||||
\<longrightarrow> get\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr h \<noteq> None))"
|
||||
\<and> (\<forall>node_ptr \<in> fset( node_ptr_kinds h). get\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr h \<noteq> None))"
|
||||
end
|
||||
global_interpretation l_type_wf_def\<^sub>N\<^sub>o\<^sub>d\<^sub>e defines type_wf = a_type_wf .
|
||||
lemmas type_wf_defs = a_type_wf_def
|
||||
|
|
@ -110,9 +110,8 @@ lemma get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_type_wf:
|
|||
shows "node_ptr |\<in>| node_ptr_kinds h \<longleftrightarrow> get\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr h \<noteq> None"
|
||||
using l_type_wf\<^sub>N\<^sub>o\<^sub>d\<^sub>e_axioms assms
|
||||
apply(simp add: type_wf_defs get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def l_type_wf\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def)
|
||||
by (metis (mono_tags, lifting) bind_eq_None_conv ffmember_filter fimage_eqI
|
||||
is_node_ptr_kind_cast get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf local.l_type_wf\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_axioms
|
||||
node_ptr_casts_commute2 node_ptr_kinds_def option.sel option.simps(3))
|
||||
by (metis bind_eq_None_conv ffmember_filter fimage_eqI fmember.rep_eq is_node_ptr_kind_cast
|
||||
get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf node_ptr_casts_commute2 node_ptr_kinds_def option.sel option.simps(3))
|
||||
end
|
||||
|
||||
global_interpretation l_get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_lemmas type_wf
|
||||
|
|
@ -177,15 +176,15 @@ locale l_known_ptrs\<^sub>N\<^sub>o\<^sub>d\<^sub>e = l_known_ptr known_ptr for
|
|||
begin
|
||||
definition a_known_ptrs :: "(_) heap \<Rightarrow> bool"
|
||||
where
|
||||
"a_known_ptrs h = (\<forall>ptr. ptr |\<in>| object_ptr_kinds h \<longrightarrow> known_ptr ptr)"
|
||||
"a_known_ptrs h = (\<forall>ptr \<in> fset (object_ptr_kinds h). known_ptr ptr)"
|
||||
|
||||
lemma known_ptrs_known_ptr: "a_known_ptrs h \<Longrightarrow> ptr |\<in>| object_ptr_kinds h \<Longrightarrow> known_ptr ptr"
|
||||
by(simp add: a_known_ptrs_def)
|
||||
|
||||
apply(simp add: a_known_ptrs_def)
|
||||
using notin_fset by fastforce
|
||||
lemma known_ptrs_preserved: "object_ptr_kinds h = object_ptr_kinds h' \<Longrightarrow> a_known_ptrs h = a_known_ptrs h'"
|
||||
by(auto simp add: a_known_ptrs_def)
|
||||
lemma known_ptrs_subset: "object_ptr_kinds h' |\<subseteq>| object_ptr_kinds h \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
||||
by(auto simp add: a_known_ptrs_def)
|
||||
by(simp add: a_known_ptrs_def less_eq_fset.rep_eq subsetD)
|
||||
lemma known_ptrs_new_ptr: "object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|new_ptr|} \<Longrightarrow> known_ptr new_ptr \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
||||
by(simp add: a_known_ptrs_def)
|
||||
end
|
||||
|
|
|
|||
|
|
@ -44,7 +44,8 @@ type_synonym 'Object Object = "'Object RObject_scheme"
|
|||
register_default_tvars "'Object Object"
|
||||
|
||||
datatype ('object_ptr, 'Object) heap = Heap (the_heap: "((_) object_ptr, (_) Object) fmap")
|
||||
register_default_tvars "('object_ptr, 'Object) heap"
|
||||
register_default_tvars "('object_ptr, 'Object) heap"
|
||||
type_synonym heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l = "(unit, unit) heap"
|
||||
|
||||
definition object_ptr_kinds :: "(_) heap \<Rightarrow> (_) object_ptr fset"
|
||||
where
|
||||
|
|
@ -134,16 +135,17 @@ locale l_known_ptrs\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t = l_known_pt
|
|||
begin
|
||||
definition a_known_ptrs :: "(_) heap \<Rightarrow> bool"
|
||||
where
|
||||
"a_known_ptrs h = (\<forall>ptr. ptr |\<in>| object_ptr_kinds h \<longrightarrow> known_ptr ptr)"
|
||||
"a_known_ptrs h = (\<forall>ptr \<in> fset (object_ptr_kinds h). known_ptr ptr)"
|
||||
|
||||
lemma known_ptrs_known_ptr:
|
||||
"a_known_ptrs h \<Longrightarrow> ptr |\<in>| object_ptr_kinds h \<Longrightarrow> known_ptr ptr"
|
||||
by(simp add: a_known_ptrs_def)
|
||||
apply(simp add: a_known_ptrs_def)
|
||||
using notin_fset by fastforce
|
||||
|
||||
lemma known_ptrs_preserved: "object_ptr_kinds h = object_ptr_kinds h' \<Longrightarrow> a_known_ptrs h = a_known_ptrs h'"
|
||||
by(auto simp add: a_known_ptrs_def)
|
||||
lemma known_ptrs_subset: "object_ptr_kinds h' |\<subseteq>| object_ptr_kinds h \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
||||
by(auto simp add: a_known_ptrs_def)
|
||||
by(simp add: a_known_ptrs_def less_eq_fset.rep_eq subsetD)
|
||||
lemma known_ptrs_new_ptr: "object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|new_ptr|} \<Longrightarrow> known_ptr new_ptr \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
|
||||
by(simp add: a_known_ptrs_def)
|
||||
end
|
||||
|
|
@ -192,4 +194,24 @@ lemma delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_ok:
|
|||
using assms
|
||||
by(auto simp add: delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def object_ptr_kinds_def split: if_splits)
|
||||
|
||||
|
||||
subsection \<open>Code Generator Setup\<close>
|
||||
|
||||
definition "create_heap xs = Heap (fmap_of_list xs)"
|
||||
|
||||
code_datatype ObjectClass.heap.Heap create_heap
|
||||
|
||||
lemma object_ptr_kinds_code3 [code]:
|
||||
"fmlookup (the_heap (create_heap xs)) x = map_of xs x"
|
||||
by(auto simp add: create_heap_def fmlookup_of_list)
|
||||
|
||||
lemma object_ptr_kinds_code4 [code]:
|
||||
"the_heap (create_heap xs) = fmap_of_list xs"
|
||||
by(simp add: create_heap_def)
|
||||
|
||||
lemma object_ptr_kinds_code5 [code]:
|
||||
"the_heap (Heap x) = x"
|
||||
by simp
|
||||
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -59,7 +59,7 @@ lemma character_data_ptr_kinds_M_reads:
|
|||
using node_ptr_kinds_M_reads
|
||||
apply(simp add: reads_def node_ptr_kinds_M_defs character_data_ptr_kinds_M_defs
|
||||
character_data_ptr_kinds_def preserved_def)
|
||||
by (metis (mono_tags, hide_lams) node_ptr_kinds_small old.unit.exhaust preserved_def)
|
||||
by (smt node_ptr_kinds_small preserved_def unit_all_impI)
|
||||
|
||||
global_interpretation l_dummy defines get_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a = "l_get_M.a_get_M get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a" .
|
||||
lemma get_M_is_l_get_M: "l_get_M get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a type_wf character_data_ptr_kinds"
|
||||
|
|
@ -307,8 +307,9 @@ lemma type_wf_put_ptr_not_in_heap_E:
|
|||
assumes "ptr |\<notin>| object_ptr_kinds h"
|
||||
shows "type_wf h"
|
||||
using assms
|
||||
by(auto simp add: type_wf_defs elim!: ElementMonad.type_wf_put_ptr_not_in_heap_E
|
||||
apply(auto simp add: type_wf_defs elim!: ElementMonad.type_wf_put_ptr_not_in_heap_E
|
||||
split: option.splits if_splits)
|
||||
using assms(2) node_ptr_kinds_commutes by blast
|
||||
|
||||
lemma type_wf_put_ptr_in_heap_E:
|
||||
assumes "type_wf (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)"
|
||||
|
|
@ -318,14 +319,7 @@ lemma type_wf_put_ptr_in_heap_E:
|
|||
shows "type_wf h"
|
||||
using assms
|
||||
apply(auto simp add: type_wf_defs split: option.splits if_splits)[1]
|
||||
apply(case_tac "x2 = cast character_data_ptr")
|
||||
apply(auto)[1]
|
||||
apply(drule_tac x=character_data_ptr in allE)
|
||||
apply(simp)
|
||||
apply (metis (no_types, lifting) ElementClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf assms(2) bind.bind_lunit
|
||||
cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_inv cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def
|
||||
get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def option.exhaust_sel)
|
||||
by(blast)
|
||||
by (metis (no_types, lifting) ElementClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf assms(2) bind.bind_lunit cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_inv cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def notin_fset option.collapse)
|
||||
|
||||
subsection\<open>Preserving Types\<close>
|
||||
|
||||
|
|
@ -364,8 +358,9 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_tag_type_typ
|
|||
apply(auto simp add: is_node_kind_def type_wf_defs ElementClass.type_wf_defs
|
||||
NodeClass.type_wf_defs ElementMonad.get_M_defs split: option.splits)[1]
|
||||
using ObjectMonad.type_wf_put_ptr_in_heap_E ObjectMonad.type_wf_put_ptr_not_in_heap_E apply blast
|
||||
apply (metis (mono_tags, lifting) bind_eq_Some_conv get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def option.exhaust_sel)
|
||||
by (metis (no_types, lifting) option.exhaust_sel )
|
||||
apply (metis (no_types, lifting) bind_eq_Some_conv finite_set_in get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)
|
||||
apply (metis finite_set_in)
|
||||
done
|
||||
|
||||
|
||||
lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_child_nodes_type_wf_preserved [simp]:
|
||||
|
|
@ -390,9 +385,9 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_child_nodes_
|
|||
NodeClass.type_wf_defs ElementMonad.get_M_defs
|
||||
split: option.splits)[1]
|
||||
using ObjectMonad.type_wf_put_ptr_in_heap_E ObjectMonad.type_wf_put_ptr_not_in_heap_E apply blast
|
||||
apply (metis (mono_tags, lifting) ElementMonad.a_get_M_def bind_eq_Some_conv error_returns_result
|
||||
get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get_heap_returns_result option.exhaust_sel option.simps(4))
|
||||
by (metis (no_types, lifting) option.exhaust_sel)
|
||||
apply (metis (no_types, lifting) bind_eq_Some_conv finite_set_in get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)
|
||||
apply (metis finite_set_in)
|
||||
done
|
||||
|
||||
lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_attrs_type_wf_preserved [simp]:
|
||||
"h \<turnstile> put_M element_ptr attrs_update v \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
|
||||
|
|
@ -412,8 +407,9 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_attrs_type_w
|
|||
apply(auto simp add: is_node_kind_def type_wf_defs ElementClass.type_wf_defs NodeClass.type_wf_defs
|
||||
ElementMonad.get_M_defs split: option.splits)[1]
|
||||
using ObjectMonad.type_wf_put_ptr_in_heap_E ObjectMonad.type_wf_put_ptr_not_in_heap_E apply blast
|
||||
apply (metis (mono_tags, lifting) ElementMonad.a_get_M_def bind_eq_Some_conv error_returns_result get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get_heap_returns_result option.exhaust_sel option.simps(4))
|
||||
by (metis (no_types, lifting) option.exhaust_sel)
|
||||
apply (metis (no_types, lifting) bind_eq_Some_conv finite_set_in get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)
|
||||
apply (metis finite_set_in)
|
||||
done
|
||||
|
||||
lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_shadow_root_opt_type_wf_preserved [simp]:
|
||||
"h \<turnstile> put_M element_ptr shadow_root_opt_update v \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
|
||||
|
|
@ -433,8 +429,9 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_shadow_root_
|
|||
apply(auto simp add: is_node_kind_def type_wf_defs ElementClass.type_wf_defs NodeClass.type_wf_defs
|
||||
ElementMonad.get_M_defs split: option.splits)[1]
|
||||
using ObjectMonad.type_wf_put_ptr_in_heap_E ObjectMonad.type_wf_put_ptr_not_in_heap_E apply blast
|
||||
apply (metis (mono_tags, lifting) bind_eq_Some_conv get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)
|
||||
by (metis (no_types, lifting) option.exhaust_sel)
|
||||
apply (metis (no_types, lifting) bind_eq_Some_conv finite_set_in get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)
|
||||
apply (metis finite_set_in)
|
||||
done
|
||||
|
||||
|
||||
lemma new_character_data_type_wf_preserved [simp]:
|
||||
|
|
@ -469,8 +466,9 @@ lemma put_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^su
|
|||
NodeClass.type_wf_defs CharacterDataMonad.get_M_defs
|
||||
ObjectClass.a_type_wf_def
|
||||
split: option.splits)[1]
|
||||
apply (metis (no_types, lifting) bind_eq_Some_conv get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def)
|
||||
by metis
|
||||
apply (metis (no_types, lifting) bind_eq_Some_conv finite_set_in get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def)
|
||||
apply (metis finite_set_in)
|
||||
done
|
||||
|
||||
lemma character_data_ptr_kinds_small:
|
||||
assumes "\<And>object_ptr. preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h'"
|
||||
|
|
@ -528,8 +526,6 @@ lemma type_wf_drop: "type_wf h \<Longrightarrow> type_wf (Heap (fmdrop ptr (the_
|
|||
apply(auto simp add: type_wf_def ElementMonad.type_wf_drop
|
||||
l_type_wf_def\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a.a_type_wf_def)[1]
|
||||
using type_wf_drop
|
||||
by (metis (no_types, lifting) ElementClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf character_data_ptr_kinds_commutes
|
||||
fmlookup_drop get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def heap.sel
|
||||
node_ptr_kinds_commutes)
|
||||
by (metis (no_types, lifting) ElementClass.type_wf\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ObjectClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf character_data_ptr_kinds_commutes finite_set_in fmlookup_drop get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def node_ptr_kinds_commutes object_ptr_kinds_code5)
|
||||
|
||||
end
|
||||
end
|
||||
|
|
|
|||
|
|
@ -58,7 +58,7 @@ lemma document_ptr_kinds_M_reads:
|
|||
|
||||
apply(simp add: reads_def object_ptr_kinds_M_defs document_ptr_kinds_M_defs
|
||||
document_ptr_kinds_def preserved_def)
|
||||
by (metis (mono_tags, hide_lams) object_ptr_kinds_preserved_small old.unit.exhaust preserved_def)
|
||||
by (smt object_ptr_kinds_preserved_small preserved_def unit_all_impI)
|
||||
|
||||
global_interpretation l_dummy defines get_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t = "l_get_M.a_get_M get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t" .
|
||||
lemma get_M_is_l_get_M: "l_get_M get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t type_wf document_ptr_kinds"
|
||||
|
|
@ -322,8 +322,7 @@ lemma type_wf_put_ptr_in_heap_E:
|
|||
using assms
|
||||
apply(auto simp add: type_wf_defs elim!: CharacterDataMonad.type_wf_put_ptr_in_heap_E
|
||||
split: option.splits if_splits)[1]
|
||||
by (metis (no_types, lifting) CharacterDataClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf bind.bind_lunit get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def
|
||||
is_document_kind_def option.collapse)
|
||||
by (metis (no_types, lifting) CharacterDataClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf bind.bind_lunit get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def is_document_kind_def notin_fset option.exhaust_sel)
|
||||
|
||||
|
||||
|
||||
|
|
@ -361,9 +360,8 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_tag_type_typ
|
|||
apply(auto simp add: is_node_kind_def type_wf_defs ElementClass.type_wf_defs NodeClass.type_wf_defs
|
||||
ElementMonad.get_M_defs ObjectClass.type_wf_defs
|
||||
CharacterDataClass.type_wf_defs split: option.splits)[1]
|
||||
apply (metis (no_types, lifting) Option.bind_cong bind_rzero
|
||||
get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def option.distinct(1))
|
||||
by metis
|
||||
apply (metis NodeClass.a_type_wf_def NodeClass.get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_type_wf ObjectClass.a_type_wf_def bind.bind_lzero finite_set_in get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def l_type_wf_def\<^sub>N\<^sub>o\<^sub>d\<^sub>e.a_type_wf_def option.collapse option.distinct(1) option.simps(3))
|
||||
by (metis fmember.rep_eq)
|
||||
|
||||
lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_child_nodes_type_wf_preserved [simp]:
|
||||
"h \<turnstile> put_M element_ptr child_nodes_update v \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
|
||||
|
|
@ -378,8 +376,8 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_child_nodes_
|
|||
apply(auto simp add: is_node_kind_def type_wf_defs ElementClass.type_wf_defs
|
||||
NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs
|
||||
CharacterDataClass.type_wf_defs split: option.splits)[1]
|
||||
apply (metis (no_types, lifting) Option.bind_cong bind_rzero get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def option.distinct(1))
|
||||
by metis
|
||||
apply (metis NodeClass.a_type_wf_def NodeClass.get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_type_wf ObjectClass.a_type_wf_def bind.bind_lzero finite_set_in get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def l_type_wf_def\<^sub>N\<^sub>o\<^sub>d\<^sub>e.a_type_wf_def option.collapse option.distinct(1) option.simps(3))
|
||||
by (metis fmember.rep_eq)
|
||||
|
||||
lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_attrs_type_wf_preserved [simp]:
|
||||
"h \<turnstile> put_M element_ptr attrs_update v \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
|
||||
|
|
@ -394,8 +392,8 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_attrs_type_w
|
|||
apply(auto simp add: is_node_kind_def type_wf_defs ElementClass.type_wf_defs
|
||||
NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs
|
||||
CharacterDataClass.type_wf_defs split: option.splits)[1]
|
||||
apply (metis (no_types, lifting) Option.bind_cong bind_rzero get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def option.distinct(1))
|
||||
by metis
|
||||
apply (metis NodeClass.a_type_wf_def NodeClass.get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_type_wf ObjectClass.a_type_wf_def bind.bind_lzero finite_set_in get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def l_type_wf_def\<^sub>N\<^sub>o\<^sub>d\<^sub>e.a_type_wf_def option.collapse option.distinct(1) option.simps(3))
|
||||
by (metis fmember.rep_eq)
|
||||
|
||||
lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_shadow_root_opt_type_wf_preserved [simp]:
|
||||
"h \<turnstile> put_M element_ptr shadow_root_opt_update v \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
|
||||
|
|
@ -410,8 +408,8 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_shadow_root_
|
|||
apply(auto simp add: is_node_kind_def type_wf_defs ElementClass.type_wf_defs
|
||||
NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs
|
||||
CharacterDataClass.type_wf_defs split: option.splits)[1]
|
||||
apply (metis (no_types, lifting) Option.bind_cong bind_rzero get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def option.distinct(1))
|
||||
by metis
|
||||
apply (metis NodeClass.a_type_wf_def NodeClass.get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_type_wf ObjectClass.a_type_wf_def bind.bind_lzero finite_set_in get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def l_type_wf_def\<^sub>N\<^sub>o\<^sub>d\<^sub>e.a_type_wf_def option.collapse option.distinct(1) option.simps(3))
|
||||
by (metis fmember.rep_eq)
|
||||
|
||||
lemma new_character_data_type_wf_preserved [simp]:
|
||||
"h \<turnstile> new_character_data \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
|
||||
|
|
@ -440,13 +438,11 @@ lemma put_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^su
|
|||
intro!: type_wf_put_I CharacterDataMonad.type_wf_put_I ElementMonad.type_wf_put_I
|
||||
NodeMonad.type_wf_put_I ObjectMonad.type_wf_put_I)[1]
|
||||
apply(auto simp add: is_node_kind_def type_wf_defs ElementClass.type_wf_defs
|
||||
NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs
|
||||
NodeClass.type_wf_defs CharacterDataMonad.get_M_defs ObjectClass.type_wf_defs
|
||||
CharacterDataClass.type_wf_defs split: option.splits)[1]
|
||||
apply (metis (no_types, lifting) CharacterDataMonad.a_get_M_def bind_eq_None_conv
|
||||
error_returns_result get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def get_heap_returns_result option.exhaust_sel
|
||||
option.simps(4))
|
||||
by (metis (no_types, lifting) CharacterDataMonad.a_get_M_def error_returns_result
|
||||
get_heap_returns_result option.exhaust_sel option.simps(4))
|
||||
apply (metis bind.bind_lzero finite_set_in get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def option.distinct(1) option.exhaust_sel)
|
||||
by (metis finite_set_in)
|
||||
|
||||
|
||||
lemma new_document_type_wf_preserved [simp]: "h \<turnstile> new_document \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
|
||||
apply(auto simp add: new_document_def new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def
|
||||
|
|
@ -457,10 +453,13 @@ lemma new_document_type_wf_preserved [simp]: "h \<turnstile> new_document \<righ
|
|||
intro!: type_wf_put_I ElementMonad.type_wf_put_I CharacterDataMonad.type_wf_put_I
|
||||
NodeMonad.type_wf_put_I ObjectMonad.type_wf_put_I
|
||||
split: if_splits)[1]
|
||||
apply(auto simp add: type_wf_defs ElementClass.type_wf_defs CharacterDataClass.type_wf_defs
|
||||
apply(auto simp add: type_wf_defs ElementClass.type_wf_defs CharacterDataClass.type_wf_defs
|
||||
NodeClass.type_wf_defs ObjectClass.type_wf_defs is_document_kind_def
|
||||
split: option.splits)[1]
|
||||
by (meson new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ptr_not_in_heap)
|
||||
using document_ptrs_def apply fastforce
|
||||
apply (simp add: is_document_kind_def)
|
||||
apply (metis Suc_n_not_le_n document_ptr.sel(1) document_ptrs_def fMax_ge ffmember_filter fimage_eqI is_document_ptr_ref)
|
||||
done
|
||||
|
||||
locale l_new_document = l_type_wf +
|
||||
assumes new_document_types_preserved: "h \<turnstile> new_document \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
|
||||
|
|
@ -500,7 +499,7 @@ lemma put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_doct
|
|||
NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs
|
||||
CharacterDataClass.type_wf_defs split: option.splits)[1]
|
||||
apply(auto simp add: get_M_defs)
|
||||
by (metis (no_types, lifting) error_returns_result option.exhaust_sel option.simps(4))
|
||||
by (metis (mono_tags) error_returns_result finite_set_in option.exhaust_sel option.simps(4))
|
||||
|
||||
lemma put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_document_element_type_wf_preserved [simp]:
|
||||
"h \<turnstile> put_M document_ptr document_element_update v \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
|
||||
|
|
@ -519,9 +518,9 @@ lemma put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_docu
|
|||
NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs
|
||||
CharacterDataClass.type_wf_defs
|
||||
split: option.splits)[1]
|
||||
by (metis)
|
||||
by (metis finite_set_in)
|
||||
|
||||
lemma put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_disconnected_nodes_type_wf_preserved [simp]:
|
||||
lemma put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_disconnected_nodes_type_wf_preserved [simp]:
|
||||
"h \<turnstile> put_M document_ptr disconnected_nodes_update v \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
|
||||
apply(auto simp add: put_M_defs put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def
|
||||
DocumentClass.type_wf\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a
|
||||
|
|
@ -538,7 +537,7 @@ lemma put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_disc
|
|||
apply(auto simp add: is_document_kind_def get_M_defs type_wf_defs ElementClass.type_wf_defs
|
||||
NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs
|
||||
CharacterDataClass.type_wf_defs split: option.splits)[1]
|
||||
by (metis)
|
||||
by (metis finite_set_in)
|
||||
|
||||
lemma document_ptr_kinds_small:
|
||||
assumes "\<And>object_ptr. preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h'"
|
||||
|
|
@ -600,6 +599,5 @@ lemma type_wf_drop: "type_wf h \<Longrightarrow> type_wf (Heap (fmdrop ptr (the_
|
|||
apply(auto simp add: type_wf_defs)[1]
|
||||
using type_wf_drop
|
||||
apply blast
|
||||
by (metis (mono_tags, lifting) comp_apply document_ptr_kinds_commutes ffmember_filter fmdom_filter
|
||||
fmfilter_alt_defs(1) fmlookup_drop get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def heap.sel object_ptr_kinds_def)
|
||||
by (metis (no_types, lifting) CharacterDataClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf CharacterDataMonad.type_wf_drop document_ptr_kinds_commutes finite_set_in fmlookup_drop get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def heap.sel)
|
||||
end
|
||||
|
|
|
|||
|
|
@ -56,7 +56,7 @@ lemma element_ptr_kinds_M_reads:
|
|||
"reads (\<Union>element_ptr. {preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t element_ptr RObject.nothing)}) element_ptr_kinds_M h h'"
|
||||
apply(simp add: reads_def node_ptr_kinds_M_defs element_ptr_kinds_M_defs element_ptr_kinds_def
|
||||
node_ptr_kinds_M_reads preserved_def)
|
||||
by (metis (mono_tags, hide_lams) node_ptr_kinds_small old.unit.exhaust preserved_def)
|
||||
by (smt filter_fset node_ptr_kinds_small preserved_def unit_all_impI)
|
||||
|
||||
global_interpretation l_dummy defines get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t = "l_get_M.a_get_M get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t" .
|
||||
lemma get_M_is_l_get_M: "l_get_M get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t type_wf element_ptr_kinds"
|
||||
|
|
@ -298,8 +298,9 @@ lemma type_wf_put_ptr_not_in_heap_E:
|
|||
assumes "ptr |\<notin>| object_ptr_kinds h"
|
||||
shows "type_wf h"
|
||||
using assms
|
||||
by(auto simp add: type_wf_defs elim!: NodeMonad.type_wf_put_ptr_not_in_heap_E
|
||||
apply(auto simp add: type_wf_defs elim!: NodeMonad.type_wf_put_ptr_not_in_heap_E
|
||||
split: option.splits if_splits)
|
||||
using assms(2) node_ptr_kinds_commutes by blast
|
||||
|
||||
lemma type_wf_put_ptr_in_heap_E:
|
||||
assumes "type_wf (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)"
|
||||
|
|
@ -309,12 +310,9 @@ lemma type_wf_put_ptr_in_heap_E:
|
|||
shows "type_wf h"
|
||||
using assms
|
||||
apply(auto simp add: type_wf_defs split: option.splits if_splits)[1]
|
||||
apply(case_tac "x2 = cast element_ptr")
|
||||
apply(drule_tac x=element_ptr in allE)
|
||||
apply(auto)[1]
|
||||
apply(metis (no_types, lifting) NodeClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf assms(2) bind.bind_lunit
|
||||
cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_inv cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def option.exhaust_sel)
|
||||
by(auto)
|
||||
by (metis (no_types, lifting) NodeClass.l_get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_lemmas_axioms assms(2) bind.bind_lunit
|
||||
cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_inv cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv finite_set_in get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def
|
||||
l_get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_lemmas.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf option.collapse)
|
||||
|
||||
subsection\<open>Preserving Types\<close>
|
||||
|
||||
|
|
@ -323,13 +321,14 @@ lemma new_element_type_wf_preserved [simp]: "h \<turnstile> new_element \<righta
|
|||
new_element_def Let_def put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def
|
||||
get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def
|
||||
split: prod.splits if_splits elim!: bind_returns_heap_E)[1]
|
||||
apply (metis element_ptr_kinds_commutes element_ptrs_def fempty_iff ffmember_filter
|
||||
is_element_ptr_ref)
|
||||
using element_ptrs_def apply fastforce
|
||||
apply (metis (mono_tags, hide_lams) Suc_n_not_le_n element_ptr.sel(1) element_ptr_kinds_commutes
|
||||
element_ptrs_def fMax_ge ffmember_filter fimageI is_element_ptr_ref)
|
||||
by (metis (no_types, lifting) fMax_finsert fempty_iff fimage_is_fempty max_0L new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def
|
||||
new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ptr_not_in_heap)
|
||||
apply (metis element_ptr_kinds_commutes element_ptrs_def fempty_iff ffmember_filter finite_set_in
|
||||
is_element_ptr_ref)
|
||||
apply (metis element_ptrs_def fempty_iff ffmember_filter finite_set_in is_element_ptr_ref)
|
||||
apply (metis (no_types, lifting) Suc_n_not_le_n element_ptr.sel(1) element_ptr_kinds_commutes
|
||||
element_ptrs_def fMax_ge ffmember_filter fimage_eqI is_element_ptr_ref notin_fset)
|
||||
apply (metis (no_types, lifting) Suc_n_not_le_n element_ptr.sel(1) element_ptrs_def
|
||||
fMax_ge ffmember_filter fimage_eqI finite_set_in is_element_ptr_ref)
|
||||
done
|
||||
|
||||
locale l_new_element = l_type_wf +
|
||||
assumes new_element_types_preserved: "h \<turnstile> new_element \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
|
||||
|
|
@ -344,12 +343,9 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_tag_type_typ
|
|||
Let_def put_M_defs get_M_defs put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def
|
||||
get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def
|
||||
split: prod.splits option.splits Option.bind_splits elim!: bind_returns_heap_E)[1]
|
||||
apply (metis option.distinct(1))
|
||||
apply (metis bind.bind_lunit cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none)
|
||||
apply (metis option.distinct(1))
|
||||
apply (metis bind.bind_lunit cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none)
|
||||
by (metis bind.bind_lunit cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_none cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv)
|
||||
|
||||
apply (metis finite_set_in option.inject)
|
||||
apply (metis cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv finite_set_in option.sel)
|
||||
done
|
||||
|
||||
lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_child_nodes_type_wf_preserved [simp]:
|
||||
"h \<turnstile> put_M element_ptr child_nodes_update v \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
|
||||
|
|
@ -357,11 +353,9 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_child_nodes_
|
|||
Let_def put_M_defs get_M_defs put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def
|
||||
get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def
|
||||
split: prod.splits option.splits Option.bind_splits elim!: bind_returns_heap_E)[1]
|
||||
apply (metis option.distinct(1))
|
||||
apply (metis bind.bind_lunit cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none)
|
||||
apply (metis option.distinct(1))
|
||||
apply (metis bind.bind_lunit cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none)
|
||||
by (metis bind.bind_lunit cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_none cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv)
|
||||
apply (metis finite_set_in option.inject)
|
||||
apply (metis cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv finite_set_in option.sel)
|
||||
done
|
||||
|
||||
lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_attrs_type_wf_preserved [simp]:
|
||||
"h \<turnstile> put_M element_ptr attrs_update v \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
|
||||
|
|
@ -369,11 +363,9 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_attrs_type_w
|
|||
put_M_defs get_M_defs put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def
|
||||
get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def
|
||||
split: prod.splits option.splits Option.bind_splits elim!: bind_returns_heap_E)[1]
|
||||
apply (metis option.distinct(1))
|
||||
apply (metis bind.bind_lunit cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none)
|
||||
apply (metis option.distinct(1))
|
||||
apply (metis bind.bind_lunit cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none)
|
||||
by (metis bind.bind_lunit cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_none cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv)
|
||||
apply (metis finite_set_in option.inject)
|
||||
apply (metis cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv finite_set_in option.sel)
|
||||
done
|
||||
|
||||
lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_shadow_root_opt_type_wf_preserved [simp]:
|
||||
"h \<turnstile> put_M element_ptr shadow_root_opt_update v \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
|
||||
|
|
@ -381,11 +373,9 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_shadow_root_
|
|||
Let_def put_M_defs get_M_defs put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def
|
||||
get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def
|
||||
split: prod.splits option.splits Option.bind_splits elim!: bind_returns_heap_E)[1]
|
||||
apply (metis option.distinct(1))
|
||||
apply (metis bind.bind_lunit cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none)
|
||||
apply (metis option.distinct(1))
|
||||
apply (metis bind.bind_lunit cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none)
|
||||
by (metis bind.bind_lunit cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_none cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv)
|
||||
apply (metis finite_set_in option.inject)
|
||||
apply (metis cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv finite_set_in option.sel)
|
||||
done
|
||||
|
||||
lemma put_M_pointers_preserved:
|
||||
assumes "h \<turnstile> put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr setter v \<rightarrow>\<^sub>h h'"
|
||||
|
|
@ -446,11 +436,9 @@ lemma type_wf_drop: "type_wf h \<Longrightarrow> type_wf (Heap (fmdrop ptr (the_
|
|||
apply(auto simp add: type_wf_defs NodeClass.type_wf_defs ObjectClass.type_wf_defs
|
||||
node_ptr_kinds_def object_ptr_kinds_def is_node_ptr_kind_def
|
||||
get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def)[1]
|
||||
apply (metis (mono_tags, lifting) comp_apply ffmember_filter fimage_eqI
|
||||
is_node_ptr_kind_cast node_ptr_casts_commute2 option.sel)
|
||||
apply (metis (no_types, lifting) comp_apply element_ptr_kinds_commutes ffmember_filter
|
||||
fmdom_filter fmfilter_alt_defs(1) heap.sel node_ptr_kinds_commutes object_ptr_kinds_def)
|
||||
by (metis comp_eq_dest_lhs element_ptr_kinds_commutes fmdom_notI fmdrop_lookup heap.sel
|
||||
node_ptr_kinds_commutes object_ptr_kinds_def)
|
||||
apply (metis (no_types, lifting) element_ptr_kinds_commutes finite_set_in fmdom_notD fmdom_notI
|
||||
fmlookup_drop heap.sel node_ptr_kinds_commutes o_apply object_ptr_kinds_def)
|
||||
by (metis element_ptr_kinds_commutes fmdom_notI fmdrop_lookup heap.sel node_ptr_kinds_commutes
|
||||
o_apply object_ptr_kinds_def)
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -77,7 +77,7 @@ lemma node_ptr_kinds_M_reads:
|
|||
using object_ptr_kinds_M_reads
|
||||
apply(simp add: reads_def node_ptr_kinds_M_defs node_ptr_kinds_def
|
||||
object_ptr_kinds_M_reads preserved_def)
|
||||
by (metis (mono_tags, hide_lams) object_ptr_kinds_preserved_small old.unit.exhaust preserved_def)
|
||||
by (smt object_ptr_kinds_preserved_small preserved_def unit_all_impI)
|
||||
|
||||
global_interpretation l_put_M type_wf node_ptr_kinds get\<^sub>N\<^sub>o\<^sub>d\<^sub>e put\<^sub>N\<^sub>o\<^sub>d\<^sub>e
|
||||
rewrites "a_get_M = get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e"
|
||||
|
|
@ -166,7 +166,7 @@ lemma type_wf_put_ptr_in_heap_E:
|
|||
shows "type_wf h"
|
||||
using assms
|
||||
apply(auto simp add: type_wf_defs split: option.splits if_splits)
|
||||
by (metis ObjectClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf bind.bind_lunit get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def is_node_kind_def option.collapse)
|
||||
by (metis ObjectClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf bind.bind_lunit finite_set_in get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def is_node_kind_def option.exhaust_sel)
|
||||
|
||||
|
||||
subsection\<open>Preserving Types\<close>
|
||||
|
|
@ -194,7 +194,8 @@ lemma type_wf_preserved_small:
|
|||
using type_wf_preserved allI[OF assms(2), of id, simplified]
|
||||
apply(auto simp add: type_wf_defs)
|
||||
apply(auto simp add: preserved_def get_M_defs node_ptr_kinds_small[OF assms(1)]
|
||||
split: option.splits, force)[1]
|
||||
split: option.splits)[1]
|
||||
apply (metis notin_fset option.simps(3))
|
||||
by(auto simp add: preserved_def get_M_defs node_ptr_kinds_small[OF assms(1)]
|
||||
split: option.splits, force)[1]
|
||||
|
||||
|
|
|
|||
|
|
@ -46,6 +46,10 @@ type_synonym ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr,
|
|||
register_default_tvars "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr,
|
||||
'document_ptr, 'shadow_root_ptr) object_ptr"
|
||||
|
||||
definition cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r :: "(_) shadow_root_ptr \<Rightarrow> (_) shadow_root_ptr"
|
||||
where
|
||||
"cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r = id"
|
||||
|
||||
definition cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^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 :: "(_)shadow_root_ptr \<Rightarrow> (_) object_ptr"
|
||||
where
|
||||
"cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^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 ptr = object_ptr.Ext (Inr (Inr (Inl ptr)))"
|
||||
|
|
@ -56,7 +60,7 @@ definition cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\
|
|||
object_ptr.Ext (Inr (Inr (Inl shadow_root_ptr))) \<Rightarrow> Some shadow_root_ptr
|
||||
| _ \<Rightarrow> None)"
|
||||
|
||||
adhoc_overloading cast cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^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 cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r
|
||||
adhoc_overloading cast cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^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 cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r
|
||||
|
||||
|
||||
definition is_shadow_root_ptr_kind :: "(_) object_ptr \<Rightarrow> bool"
|
||||
|
|
|
|||
|
|
@ -79,9 +79,28 @@ definition
|
|||
where
|
||||
"returns_heap h p h' \<longleftrightarrow> (case h \<turnstile> p of Inr (_ , h'') \<Rightarrow> h' = h'' | Inl _ \<Rightarrow> False)"
|
||||
|
||||
fun select_heap ("|(_)|\<^sub>h")
|
||||
where
|
||||
"select_heap (Inr ( _, h)) = h"
|
||||
| "select_heap (Inl _) = undefined"
|
||||
|
||||
lemma returns_heap_eq [elim]: "h \<turnstile> f \<rightarrow>\<^sub>h h' \<Longrightarrow> h \<turnstile> f \<rightarrow>\<^sub>h h'' \<Longrightarrow> h' = h''"
|
||||
by(auto simp add: returns_heap_def split: sum.splits)
|
||||
|
||||
definition
|
||||
returns_result_heap :: "'heap \<Rightarrow> ('heap, 'e, 'result) prog \<Rightarrow> 'result \<Rightarrow> 'heap \<Rightarrow> bool"
|
||||
("((_)/ \<turnstile> (_)/ \<rightarrow>\<^sub>r (_) \<rightarrow>\<^sub>h (_))" [60, 35, 61, 62] 65)
|
||||
where
|
||||
"returns_result_heap h p r h' \<longleftrightarrow> h \<turnstile> p \<rightarrow>\<^sub>r r \<and> h \<turnstile> p \<rightarrow>\<^sub>h h'"
|
||||
|
||||
lemma [code]: "returns_result_heap h p r h' \<longleftrightarrow> (case h \<turnstile> p of Inr (r', h'') \<Rightarrow> r = r' \<and> h' = h'' | Inl _ \<Rightarrow> False)"
|
||||
by(auto simp add: returns_result_heap_def returns_result_def returns_heap_def split: sum.splits)
|
||||
|
||||
fun select_result_heap ("|(_)|\<^sub>r\<^sub>h")
|
||||
where
|
||||
"select_result_heap (Inr (r, h)) = (r, h)"
|
||||
| "select_result_heap (Inl _) = undefined"
|
||||
|
||||
definition
|
||||
returns_error :: "'heap \<Rightarrow> ('heap, 'e, 'result) prog \<Rightarrow> 'e \<Rightarrow> bool"
|
||||
("((_)/ \<turnstile> (_)/ \<rightarrow>\<^sub>e (_))" [60, 35, 61] 65)
|
||||
|
|
@ -711,6 +730,11 @@ definition preserved :: "('heap, 'e, 'result) prog \<Rightarrow> 'heap \<Rightar
|
|||
where
|
||||
"preserved f h h' \<longleftrightarrow> (\<forall>x. h \<turnstile> f \<rightarrow>\<^sub>r x \<longleftrightarrow> h' \<turnstile> f \<rightarrow>\<^sub>r x)"
|
||||
|
||||
lemma preserved_code [code]: "preserved f h h' = (((h \<turnstile> ok f) \<and> (h' \<turnstile> ok f) \<and> |h \<turnstile> f|\<^sub>r = |h' \<turnstile> f|\<^sub>r) \<or> ((\<not>h \<turnstile> ok f) \<and> (\<not>h' \<turnstile> ok f)))"
|
||||
apply(auto simp add: preserved_def)
|
||||
apply (meson is_OK_returns_result_E is_OK_returns_result_I)+
|
||||
done
|
||||
|
||||
lemma reflp_preserved_f [simp]: "reflp (preserved f)"
|
||||
by(auto simp add: preserved_def reflp_def)
|
||||
lemma transp_preserved_f [simp]: "transp (preserved f)"
|
||||
|
|
|
|||
|
|
@ -276,9 +276,8 @@ structure Hide_Tvar : HIDE_TVAR = struct
|
|||
val thy = Proof_Context.theory_of ctx
|
||||
|
||||
fun parse_ast ((Ast.Constant const)::[]) = (const,NONE)
|
||||
| parse_ast ((Ast.Constant sort)::(Ast.Constant const)::[])
|
||||
= (const,SOME sort)
|
||||
| parse_ast _ = error("AST type not supported.")
|
||||
| parse_ast (sort::(Ast.Constant const)::[]) = (const,SOME sort)
|
||||
| parse_ast _ = error("AST type not supported.")
|
||||
|
||||
val (decorated_name, decorated_sort) = parse_ast ast
|
||||
|
||||
|
|
@ -295,9 +294,9 @@ structure Hide_Tvar : HIDE_TVAR = struct
|
|||
let fun mk_tvar n =
|
||||
case decorated_sort of
|
||||
NONE => Ast.Variable(name_of_tvar n)
|
||||
| SOME sort => Ast.Appl([Ast.Constant("_ofsort"),
|
||||
| SOME sort => Ast.Appl([Ast.Constant("_ofsort"),
|
||||
Ast.Variable(name_of_tvar n),
|
||||
Ast.Constant(sort)])
|
||||
sort])
|
||||
in
|
||||
map mk_tvar (#tvars default_info)
|
||||
end
|
||||
|
|
|
|||
|
|
@ -79,39 +79,6 @@ definition removeWhiteSpaceOnlyTextNodes :: "((_) object_ptr option) \<Rightarro
|
|||
"removeWhiteSpaceOnlyTextNodes _ = return ()"
|
||||
|
||||
|
||||
subsection \<open>create\_heap\<close>
|
||||
|
||||
(* We use this construction because partially applied functions such as "map_of xs" don't play
|
||||
well together with the code generator. *)
|
||||
definition "create_heap xs = Heap (fmap_of_list xs)"
|
||||
|
||||
code_datatype ObjectClass.heap.Heap create_heap
|
||||
|
||||
lemma object_ptr_kinds_code1 [code]:
|
||||
"object_ptr_kinds (Heap (fmap_of_list xs)) = object_ptr_kinds (create_heap xs)"
|
||||
by(simp add: create_heap_def)
|
||||
|
||||
lemma object_ptr_kinds_code2 [code]:
|
||||
"object_ptr_kinds (create_heap xs) = fset_of_list (map fst xs)"
|
||||
by (simp add: object_ptr_kinds_def create_heap_def dom_map_of_conv_image_fst)
|
||||
|
||||
lemma object_ptr_kinds_code3 [code]:
|
||||
"fmlookup (the_heap (create_heap xs)) x = map_of xs x"
|
||||
by(auto simp add: create_heap_def fmlookup_of_list)
|
||||
|
||||
lemma object_ptr_kinds_code4 [code]:
|
||||
"the_heap (create_heap xs) = fmap_of_list xs"
|
||||
by(simp add: create_heap_def)
|
||||
|
||||
lemma object_ptr_kinds_code5 [code]:
|
||||
"the_heap (Heap x) = x"
|
||||
by simp
|
||||
|
||||
lemma object_ptr_kinds_code6 [code]:
|
||||
"noop = return ()"
|
||||
by(simp add: noop_def)
|
||||
|
||||
|
||||
subsection \<open>Making the functions under test compatible with untyped languages such as JavaScript\<close>
|
||||
|
||||
fun set_attribute_with_null :: "((_) object_ptr option) \<Rightarrow> attr_key \<Rightarrow> attr_value \<Rightarrow> (_, unit) dom_prog"
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
(***********************************************************************************
|
||||
* Copyright (c) 2016-2018 The University of Sheffield, UK
|
||||
* Copyright (c) 2016-2019 The University of Sheffield, UK
|
||||
*
|
||||
* All rights reserved.
|
||||
*
|
||||
|
|
@ -27,15 +27,17 @@
|
|||
* SPDX-License-Identifier: BSD-2-Clause
|
||||
***********************************************************************************)
|
||||
|
||||
section\<open>Testing adoptNode\<close>
|
||||
text\<open>This theory contains the test cases for adoptNode.\<close>
|
||||
(* This file is automatically generated, please do not modify! *)
|
||||
|
||||
section\<open>Testing Document_adoptNode\<close>
|
||||
text\<open>This theory contains the test cases for Document_adoptNode.\<close>
|
||||
|
||||
theory Document_adoptNode
|
||||
imports
|
||||
"Core_DOM_BaseTest"
|
||||
begin
|
||||
|
||||
definition Document_adoptNode_heap :: "(unit, unit, unit, unit, unit, unit, unit, unit, unit, unit, unit) heap" where
|
||||
definition Document_adoptNode_heap :: heap⇩f⇩i⇩n⇩a⇩l where
|
||||
"Document_adoptNode_heap = create_heap [(cast (document_ptr.Ref 1), cast (create_document_obj html (Some (cast (element_ptr.Ref 1))) [])),
|
||||
(cast (element_ptr.Ref 1), cast (create_element_obj ''html'' [cast (element_ptr.Ref 2), cast (element_ptr.Ref 8)] fmempty None)),
|
||||
(cast (element_ptr.Ref 2), cast (create_element_obj ''head'' [cast (element_ptr.Ref 3), cast (element_ptr.Ref 4), cast (element_ptr.Ref 5), cast (element_ptr.Ref 6), cast (element_ptr.Ref 7)] fmempty None)),
|
||||
|
|
@ -52,30 +54,30 @@ definition Document_adoptNode_heap :: "(unit, unit, unit, unit, unit, unit, unit
|
|||
(cast (element_ptr.Ref 11), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 3)] fmempty None)),
|
||||
(cast (character_data_ptr.Ref 3), cast (create_character_data_obj ''%3C%3Cscript%3E%3E''))]"
|
||||
|
||||
definition document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "document = Some (cast (document_ptr.Ref 1))"
|
||||
definition Document_adoptNode_document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "Document_adoptNode_document = Some (cast (document_ptr.Ref 1))"
|
||||
|
||||
|
||||
text \<open>"Adopting an Element called 'x<' should work."\<close>
|
||||
|
||||
lemma "test (do {
|
||||
tmp0 \<leftarrow> document . getElementsByTagName(''x<'');
|
||||
tmp0 \<leftarrow> Document_adoptNode_document . getElementsByTagName(''x<'');
|
||||
y \<leftarrow> return (tmp0 ! 0);
|
||||
child \<leftarrow> y . firstChild;
|
||||
tmp1 \<leftarrow> y . parentNode;
|
||||
tmp2 \<leftarrow> document . body;
|
||||
tmp2 \<leftarrow> Document_adoptNode_document . body;
|
||||
assert_equals(tmp1, tmp2);
|
||||
tmp3 \<leftarrow> y . ownerDocument;
|
||||
assert_equals(tmp3, document);
|
||||
tmp4 \<leftarrow> document . adoptNode(y);
|
||||
assert_equals(tmp3, Document_adoptNode_document);
|
||||
tmp4 \<leftarrow> Document_adoptNode_document . adoptNode(y);
|
||||
assert_equals(tmp4, y);
|
||||
tmp5 \<leftarrow> y . parentNode;
|
||||
assert_equals(tmp5, None);
|
||||
tmp6 \<leftarrow> y . firstChild;
|
||||
assert_equals(tmp6, child);
|
||||
tmp7 \<leftarrow> y . ownerDocument;
|
||||
assert_equals(tmp7, document);
|
||||
assert_equals(tmp7, Document_adoptNode_document);
|
||||
tmp8 \<leftarrow> child . ownerDocument;
|
||||
assert_equals(tmp8, document);
|
||||
assert_equals(tmp8, Document_adoptNode_document);
|
||||
doc \<leftarrow> createDocument(None, None, None);
|
||||
tmp9 \<leftarrow> doc . adoptNode(y);
|
||||
assert_equals(tmp9, y);
|
||||
|
|
@ -94,8 +96,8 @@ lemma "test (do {
|
|||
text \<open>"Adopting an Element called ':good:times:' should work."\<close>
|
||||
|
||||
lemma "test (do {
|
||||
x \<leftarrow> document . createElement('':good:times:'');
|
||||
tmp0 \<leftarrow> document . adoptNode(x);
|
||||
x \<leftarrow> Document_adoptNode_document . createElement('':good:times:'');
|
||||
tmp0 \<leftarrow> Document_adoptNode_document . adoptNode(x);
|
||||
assert_equals(tmp0, x);
|
||||
doc \<leftarrow> createDocument(None, None, None);
|
||||
tmp1 \<leftarrow> doc . adoptNode(x);
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
(***********************************************************************************
|
||||
* Copyright (c) 2016-2018 The University of Sheffield, UK
|
||||
* Copyright (c) 2016-2019 The University of Sheffield, UK
|
||||
*
|
||||
* All rights reserved.
|
||||
*
|
||||
|
|
@ -27,15 +27,17 @@
|
|||
* SPDX-License-Identifier: BSD-2-Clause
|
||||
***********************************************************************************)
|
||||
|
||||
section\<open>Testing getElementById\<close>
|
||||
text\<open>This theory contains the test cases for getElementById.\<close>
|
||||
(* This file is automatically generated, please do not modify! *)
|
||||
|
||||
section\<open>Testing Document_getElementById\<close>
|
||||
text\<open>This theory contains the test cases for Document_getElementById.\<close>
|
||||
|
||||
theory Document_getElementById
|
||||
imports
|
||||
"Core_DOM_BaseTest"
|
||||
begin
|
||||
|
||||
definition Document_getElementById_heap :: "(unit, unit, unit, unit, unit, unit, unit, unit, unit, unit, unit) heap" where
|
||||
definition Document_getElementById_heap :: heap⇩f⇩i⇩n⇩a⇩l where
|
||||
"Document_getElementById_heap = create_heap [(cast (document_ptr.Ref 1), cast (create_document_obj html (Some (cast (element_ptr.Ref 1))) [])),
|
||||
(cast (element_ptr.Ref 1), cast (create_element_obj ''html'' [cast (element_ptr.Ref 2), cast (element_ptr.Ref 9)] fmempty None)),
|
||||
(cast (element_ptr.Ref 2), cast (create_element_obj ''head'' [cast (element_ptr.Ref 3), cast (element_ptr.Ref 4), cast (element_ptr.Ref 5), cast (element_ptr.Ref 6), cast (element_ptr.Ref 7), cast (element_ptr.Ref 8)] fmempty None)),
|
||||
|
|
@ -60,23 +62,23 @@ definition Document_getElementById_heap :: "(unit, unit, unit, unit, unit, unit,
|
|||
(cast (element_ptr.Ref 19), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 3)] fmempty None)),
|
||||
(cast (character_data_ptr.Ref 3), cast (create_character_data_obj ''%3C%3Cscript%3E%3E''))]"
|
||||
|
||||
definition document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "document = Some (cast (document_ptr.Ref 1))"
|
||||
definition Document_getElementById_document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "Document_getElementById_document = Some (cast (document_ptr.Ref 1))"
|
||||
|
||||
|
||||
text \<open>"Document.getElementById with a script-inserted element"\<close>
|
||||
|
||||
lemma "test (do {
|
||||
gBody \<leftarrow> document . body;
|
||||
gBody \<leftarrow> Document_getElementById_document . body;
|
||||
TEST_ID \<leftarrow> return ''test2'';
|
||||
test \<leftarrow> document . createElement(''div'');
|
||||
test \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
test . setAttribute(''id'', TEST_ID);
|
||||
gBody . appendChild(test);
|
||||
result \<leftarrow> document . getElementById(TEST_ID);
|
||||
result \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_not_equals(result, None, ''should not be null.'');
|
||||
tmp0 \<leftarrow> result . tagName;
|
||||
assert_equals(tmp0, ''div'', ''should have appended element's tag name'');
|
||||
gBody . removeChild(test);
|
||||
removed \<leftarrow> document . getElementById(TEST_ID);
|
||||
removed \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(removed, None, ''should not get removed element.'')
|
||||
}) Document_getElementById_heap"
|
||||
by eval
|
||||
|
|
@ -85,19 +87,19 @@ lemma "test (do {
|
|||
text \<open>"update `id` attribute via setAttribute/removeAttribute"\<close>
|
||||
|
||||
lemma "test (do {
|
||||
gBody \<leftarrow> document . body;
|
||||
gBody \<leftarrow> Document_getElementById_document . body;
|
||||
TEST_ID \<leftarrow> return ''test3'';
|
||||
test \<leftarrow> document . createElement(''div'');
|
||||
test \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
test . setAttribute(''id'', TEST_ID);
|
||||
gBody . appendChild(test);
|
||||
UPDATED_ID \<leftarrow> return ''test3-updated'';
|
||||
test . setAttribute(''id'', UPDATED_ID);
|
||||
e \<leftarrow> document . getElementById(UPDATED_ID);
|
||||
e \<leftarrow> Document_getElementById_document . getElementById(UPDATED_ID);
|
||||
assert_equals(e, test, ''should get the element with id.'');
|
||||
old \<leftarrow> document . getElementById(TEST_ID);
|
||||
old \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(old, None, ''shouldn't get the element by the old id.'');
|
||||
test . removeAttribute(''id'');
|
||||
e2 \<leftarrow> document . getElementById(UPDATED_ID);
|
||||
e2 \<leftarrow> Document_getElementById_document . getElementById(UPDATED_ID);
|
||||
assert_equals(e2, None, ''should return null when the passed id is none in document.'')
|
||||
}) Document_getElementById_heap"
|
||||
by eval
|
||||
|
|
@ -107,13 +109,13 @@ text \<open>"Ensure that the id attribute only affects elements present in a doc
|
|||
|
||||
lemma "test (do {
|
||||
TEST_ID \<leftarrow> return ''test4-should-not-exist'';
|
||||
e \<leftarrow> document . createElement(''div'');
|
||||
e \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
e . setAttribute(''id'', TEST_ID);
|
||||
tmp0 \<leftarrow> document . getElementById(TEST_ID);
|
||||
tmp0 \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(tmp0, None, ''should be null'');
|
||||
tmp1 \<leftarrow> document . body;
|
||||
tmp1 \<leftarrow> Document_getElementById_document . body;
|
||||
tmp1 . appendChild(e);
|
||||
tmp2 \<leftarrow> document . getElementById(TEST_ID);
|
||||
tmp2 \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(tmp2, e, ''should be the appended element'')
|
||||
}) Document_getElementById_heap"
|
||||
by eval
|
||||
|
|
@ -122,23 +124,23 @@ lemma "test (do {
|
|||
text \<open>"in tree order, within the context object's tree"\<close>
|
||||
|
||||
lemma "test (do {
|
||||
gBody \<leftarrow> document . body;
|
||||
gBody \<leftarrow> Document_getElementById_document . body;
|
||||
TEST_ID \<leftarrow> return ''test5'';
|
||||
target \<leftarrow> document . getElementById(TEST_ID);
|
||||
target \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_not_equals(target, None, ''should not be null'');
|
||||
tmp0 \<leftarrow> target . getAttribute(''data-name'');
|
||||
assert_equals(tmp0, ''1st'', ''should return the 1st'');
|
||||
element4 \<leftarrow> document . createElement(''div'');
|
||||
element4 \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
element4 . setAttribute(''id'', TEST_ID);
|
||||
element4 . setAttribute(''data-name'', ''4th'');
|
||||
gBody . appendChild(element4);
|
||||
target2 \<leftarrow> document . getElementById(TEST_ID);
|
||||
target2 \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_not_equals(target2, None, ''should not be null'');
|
||||
tmp1 \<leftarrow> target2 . getAttribute(''data-name'');
|
||||
assert_equals(tmp1, ''1st'', ''should be the 1st'');
|
||||
tmp2 \<leftarrow> target2 . parentNode;
|
||||
tmp2 . removeChild(target2);
|
||||
target3 \<leftarrow> document . getElementById(TEST_ID);
|
||||
target3 \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_not_equals(target3, None, ''should not be null'');
|
||||
tmp3 \<leftarrow> target3 . getAttribute(''data-name'');
|
||||
assert_equals(tmp3, ''4th'', ''should be the 4th'')
|
||||
|
|
@ -146,17 +148,15 @@ lemma "test (do {
|
|||
by eval
|
||||
|
||||
|
||||
text \<open>"Modern browsers optimize this method with using internal id cache.
|
||||
This test checks that their optimization should effect only append to
|
||||
`Document`, not append to `Node`."\<close>
|
||||
text \<open>"Modern browsers optimize this method with using internal id cache. This test checks that their optimization should effect only append to `Document`, not append to `Node`."\<close>
|
||||
|
||||
lemma "test (do {
|
||||
TEST_ID \<leftarrow> return ''test6'';
|
||||
s \<leftarrow> document . createElement(''div'');
|
||||
s \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
s . setAttribute(''id'', TEST_ID);
|
||||
tmp0 \<leftarrow> document . createElement(''div'');
|
||||
tmp0 \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
tmp0 . appendChild(s);
|
||||
tmp1 \<leftarrow> document . getElementById(TEST_ID);
|
||||
tmp1 \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(tmp1, None, ''should be null'')
|
||||
}) Document_getElementById_heap"
|
||||
by eval
|
||||
|
|
@ -165,17 +165,17 @@ lemma "test (do {
|
|||
text \<open>"changing attribute's value via `Attr` gotten from `Element.attribute`."\<close>
|
||||
|
||||
lemma "test (do {
|
||||
gBody \<leftarrow> document . body;
|
||||
gBody \<leftarrow> Document_getElementById_document . body;
|
||||
TEST_ID \<leftarrow> return ''test7'';
|
||||
element \<leftarrow> document . createElement(''div'');
|
||||
element \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
element . setAttribute(''id'', TEST_ID);
|
||||
gBody . appendChild(element);
|
||||
target \<leftarrow> document . getElementById(TEST_ID);
|
||||
target \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(target, element, ''should return the element before changing the value'');
|
||||
element . setAttribute(''id'', (TEST_ID @ ''-updated''));
|
||||
target2 \<leftarrow> document . getElementById(TEST_ID);
|
||||
target2 \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(target2, None, ''should return null after updated id via Attr.value'');
|
||||
target3 \<leftarrow> document . getElementById((TEST_ID @ ''-updated''));
|
||||
target3 \<leftarrow> Document_getElementById_document . getElementById((TEST_ID @ ''-updated''));
|
||||
assert_equals(target3, element, ''should be equal to the updated element.'')
|
||||
}) Document_getElementById_heap"
|
||||
by eval
|
||||
|
|
@ -184,19 +184,19 @@ lemma "test (do {
|
|||
text \<open>"update `id` attribute via element.id"\<close>
|
||||
|
||||
lemma "test (do {
|
||||
gBody \<leftarrow> document . body;
|
||||
gBody \<leftarrow> Document_getElementById_document . body;
|
||||
TEST_ID \<leftarrow> return ''test12'';
|
||||
test \<leftarrow> document . createElement(''div'');
|
||||
test \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
test . setAttribute(''id'', TEST_ID);
|
||||
gBody . appendChild(test);
|
||||
UPDATED_ID \<leftarrow> return (TEST_ID @ ''-updated'');
|
||||
test . setAttribute(''id'', UPDATED_ID);
|
||||
e \<leftarrow> document . getElementById(UPDATED_ID);
|
||||
e \<leftarrow> Document_getElementById_document . getElementById(UPDATED_ID);
|
||||
assert_equals(e, test, ''should get the element with id.'');
|
||||
old \<leftarrow> document . getElementById(TEST_ID);
|
||||
old \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(old, None, ''shouldn't get the element by the old id.'');
|
||||
test . setAttribute(''id'', '''');
|
||||
e2 \<leftarrow> document . getElementById(UPDATED_ID);
|
||||
e2 \<leftarrow> Document_getElementById_document . getElementById(UPDATED_ID);
|
||||
assert_equals(e2, None, ''should return null when the passed id is none in document.'')
|
||||
}) Document_getElementById_heap"
|
||||
by eval
|
||||
|
|
@ -205,33 +205,33 @@ lemma "test (do {
|
|||
text \<open>"where insertion order and tree order don't match"\<close>
|
||||
|
||||
lemma "test (do {
|
||||
gBody \<leftarrow> document . body;
|
||||
gBody \<leftarrow> Document_getElementById_document . body;
|
||||
TEST_ID \<leftarrow> return ''test13'';
|
||||
container \<leftarrow> document . createElement(''div'');
|
||||
container \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
container . setAttribute(''id'', (TEST_ID @ ''-fixture''));
|
||||
gBody . appendChild(container);
|
||||
element1 \<leftarrow> document . createElement(''div'');
|
||||
element1 \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
element1 . setAttribute(''id'', TEST_ID);
|
||||
element2 \<leftarrow> document . createElement(''div'');
|
||||
element2 \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
element2 . setAttribute(''id'', TEST_ID);
|
||||
element3 \<leftarrow> document . createElement(''div'');
|
||||
element3 \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
element3 . setAttribute(''id'', TEST_ID);
|
||||
element4 \<leftarrow> document . createElement(''div'');
|
||||
element4 \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
element4 . setAttribute(''id'', TEST_ID);
|
||||
container . appendChild(element2);
|
||||
container . appendChild(element4);
|
||||
container . insertBefore(element3, element4);
|
||||
container . insertBefore(element1, element2);
|
||||
test \<leftarrow> document . getElementById(TEST_ID);
|
||||
test \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(test, element1, ''should return 1st element'');
|
||||
container . removeChild(element1);
|
||||
test \<leftarrow> document . getElementById(TEST_ID);
|
||||
test \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(test, element2, ''should return 2nd element'');
|
||||
container . removeChild(element2);
|
||||
test \<leftarrow> document . getElementById(TEST_ID);
|
||||
test \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(test, element3, ''should return 3rd element'');
|
||||
container . removeChild(element3);
|
||||
test \<leftarrow> document . getElementById(TEST_ID);
|
||||
test \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(test, element4, ''should return 4th element'');
|
||||
container . removeChild(element4)
|
||||
}) Document_getElementById_heap"
|
||||
|
|
@ -241,16 +241,16 @@ lemma "test (do {
|
|||
text \<open>"Inserting an id by inserting its parent node"\<close>
|
||||
|
||||
lemma "test (do {
|
||||
gBody \<leftarrow> document . body;
|
||||
gBody \<leftarrow> Document_getElementById_document . body;
|
||||
TEST_ID \<leftarrow> return ''test14'';
|
||||
a \<leftarrow> document . createElement(''a'');
|
||||
b \<leftarrow> document . createElement(''b'');
|
||||
a \<leftarrow> Document_getElementById_document . createElement(''a'');
|
||||
b \<leftarrow> Document_getElementById_document . createElement(''b'');
|
||||
a . appendChild(b);
|
||||
b . setAttribute(''id'', TEST_ID);
|
||||
tmp0 \<leftarrow> document . getElementById(TEST_ID);
|
||||
tmp0 \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(tmp0, None);
|
||||
gBody . appendChild(a);
|
||||
tmp1 \<leftarrow> document . getElementById(TEST_ID);
|
||||
tmp1 \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(tmp1, b)
|
||||
}) Document_getElementById_heap"
|
||||
by eval
|
||||
|
|
@ -260,15 +260,15 @@ text \<open>"Document.getElementById must not return nodes not present in docume
|
|||
|
||||
lemma "test (do {
|
||||
TEST_ID \<leftarrow> return ''test15'';
|
||||
outer \<leftarrow> document . getElementById(''outer'');
|
||||
middle \<leftarrow> document . getElementById(''middle'');
|
||||
inner \<leftarrow> document . getElementById(''inner'');
|
||||
tmp0 \<leftarrow> document . getElementById(''middle'');
|
||||
outer \<leftarrow> Document_getElementById_document . getElementById(''outer'');
|
||||
middle \<leftarrow> Document_getElementById_document . getElementById(''middle'');
|
||||
inner \<leftarrow> Document_getElementById_document . getElementById(''inner'');
|
||||
tmp0 \<leftarrow> Document_getElementById_document . getElementById(''middle'');
|
||||
outer . removeChild(tmp0);
|
||||
new_el \<leftarrow> document . createElement(''h1'');
|
||||
new_el \<leftarrow> Document_getElementById_document . createElement(''h1'');
|
||||
new_el . setAttribute(''id'', ''heading'');
|
||||
inner . appendChild(new_el);
|
||||
tmp1 \<leftarrow> document . getElementById(''heading'');
|
||||
tmp1 \<leftarrow> Document_getElementById_document . getElementById(''heading'');
|
||||
assert_equals(tmp1, None)
|
||||
}) Document_getElementById_heap"
|
||||
by eval
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
(***********************************************************************************
|
||||
* Copyright (c) 2016-2018 The University of Sheffield, UK
|
||||
* Copyright (c) 2016-2019 The University of Sheffield, UK
|
||||
*
|
||||
* All rights reserved.
|
||||
*
|
||||
|
|
@ -27,15 +27,17 @@
|
|||
* SPDX-License-Identifier: BSD-2-Clause
|
||||
***********************************************************************************)
|
||||
|
||||
section\<open>Testing insertBefore\<close>
|
||||
text\<open>This theory contains the test cases for insertBefore.\<close>
|
||||
(* This file is automatically generated, please do not modify! *)
|
||||
|
||||
section\<open>Testing Node_insertBefore\<close>
|
||||
text\<open>This theory contains the test cases for Node_insertBefore.\<close>
|
||||
|
||||
theory Node_insertBefore
|
||||
imports
|
||||
"Core_DOM_BaseTest"
|
||||
begin
|
||||
|
||||
definition Node_insertBefore_heap :: "(unit, unit, unit, unit, unit, unit, unit, unit, unit, unit, unit) heap" where
|
||||
definition Node_insertBefore_heap :: heap⇩f⇩i⇩n⇩a⇩l where
|
||||
"Node_insertBefore_heap = create_heap [(cast (document_ptr.Ref 1), cast (create_document_obj html (Some (cast (element_ptr.Ref 1))) [])),
|
||||
(cast (element_ptr.Ref 1), cast (create_element_obj ''html'' [cast (element_ptr.Ref 2), cast (element_ptr.Ref 6)] fmempty None)),
|
||||
(cast (element_ptr.Ref 2), cast (create_element_obj ''head'' [cast (element_ptr.Ref 3), cast (element_ptr.Ref 4), cast (element_ptr.Ref 5)] fmempty None)),
|
||||
|
|
@ -48,14 +50,14 @@ definition Node_insertBefore_heap :: "(unit, unit, unit, unit, unit, unit, unit,
|
|||
(cast (element_ptr.Ref 8), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 2)] fmempty None)),
|
||||
(cast (character_data_ptr.Ref 2), cast (create_character_data_obj ''%3C%3Cscript%3E%3E''))]"
|
||||
|
||||
definition document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "document = Some (cast (document_ptr.Ref 1))"
|
||||
definition Node_insertBefore_document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "Node_insertBefore_document = Some (cast (document_ptr.Ref 1))"
|
||||
|
||||
|
||||
text \<open>"Calling insertBefore an a leaf node Text must throw HIERARCHY\_REQUEST\_ERR."\<close>
|
||||
|
||||
lemma "test (do {
|
||||
node \<leftarrow> document . createTextNode(''Foo'');
|
||||
tmp0 \<leftarrow> document . createTextNode(''fail'');
|
||||
node \<leftarrow> Node_insertBefore_document . createTextNode(''Foo'');
|
||||
tmp0 \<leftarrow> Node_insertBefore_document . createTextNode(''fail'');
|
||||
assert_throws(HierarchyRequestError, node . insertBefore(tmp0, None))
|
||||
}) Node_insertBefore_heap"
|
||||
by eval
|
||||
|
|
@ -64,13 +66,13 @@ lemma "test (do {
|
|||
text \<open>"Calling insertBefore with an inclusive ancestor of the context object must throw HIERARCHY\_REQUEST\_ERR."\<close>
|
||||
|
||||
lemma "test (do {
|
||||
tmp1 \<leftarrow> document . body;
|
||||
tmp2 \<leftarrow> document . getElementById(''log'');
|
||||
tmp0 \<leftarrow> document . body;
|
||||
tmp1 \<leftarrow> Node_insertBefore_document . body;
|
||||
tmp2 \<leftarrow> Node_insertBefore_document . getElementById(''log'');
|
||||
tmp0 \<leftarrow> Node_insertBefore_document . body;
|
||||
assert_throws(HierarchyRequestError, tmp0 . insertBefore(tmp1, tmp2));
|
||||
tmp4 \<leftarrow> document . documentElement;
|
||||
tmp5 \<leftarrow> document . getElementById(''log'');
|
||||
tmp3 \<leftarrow> document . body;
|
||||
tmp4 \<leftarrow> Node_insertBefore_document . documentElement;
|
||||
tmp5 \<leftarrow> Node_insertBefore_document . getElementById(''log'');
|
||||
tmp3 \<leftarrow> Node_insertBefore_document . body;
|
||||
assert_throws(HierarchyRequestError, tmp3 . insertBefore(tmp4, tmp5))
|
||||
}) Node_insertBefore_heap"
|
||||
by eval
|
||||
|
|
@ -79,9 +81,9 @@ lemma "test (do {
|
|||
text \<open>"Calling insertBefore with a reference child whose parent is not the context node must throw a NotFoundError."\<close>
|
||||
|
||||
lemma "test (do {
|
||||
a \<leftarrow> document . createElement(''div'');
|
||||
b \<leftarrow> document . createElement(''div'');
|
||||
c \<leftarrow> document . createElement(''div'');
|
||||
a \<leftarrow> Node_insertBefore_document . createElement(''div'');
|
||||
b \<leftarrow> Node_insertBefore_document . createElement(''div'');
|
||||
c \<leftarrow> Node_insertBefore_document . createElement(''div'');
|
||||
assert_throws(NotFoundError, a . insertBefore(b, c))
|
||||
}) Node_insertBefore_heap"
|
||||
by eval
|
||||
|
|
@ -104,9 +106,9 @@ lemma "test (do {
|
|||
text \<open>"Inserting a node before itself should not move the node"\<close>
|
||||
|
||||
lemma "test (do {
|
||||
a \<leftarrow> document . createElement(''div'');
|
||||
b \<leftarrow> document . createElement(''div'');
|
||||
c \<leftarrow> document . createElement(''div'');
|
||||
a \<leftarrow> Node_insertBefore_document . createElement(''div'');
|
||||
b \<leftarrow> Node_insertBefore_document . createElement(''div'');
|
||||
c \<leftarrow> Node_insertBefore_document . createElement(''div'');
|
||||
a . appendChild(b);
|
||||
a . appendChild(c);
|
||||
tmp0 \<leftarrow> a . childNodes;
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
(***********************************************************************************
|
||||
* Copyright (c) 2016-2018 The University of Sheffield, UK
|
||||
* Copyright (c) 2016-2019 The University of Sheffield, UK
|
||||
*
|
||||
* All rights reserved.
|
||||
*
|
||||
|
|
@ -27,15 +27,17 @@
|
|||
* SPDX-License-Identifier: BSD-2-Clause
|
||||
***********************************************************************************)
|
||||
|
||||
section\<open>Testing removeChild\<close>
|
||||
text\<open>This theory contains the test cases for removeChild.\<close>
|
||||
(* This file is automatically generated, please do not modify! *)
|
||||
|
||||
section\<open>Testing Node_removeChild\<close>
|
||||
text\<open>This theory contains the test cases for Node_removeChild.\<close>
|
||||
|
||||
theory Node_removeChild
|
||||
imports
|
||||
"Core_DOM_BaseTest"
|
||||
begin
|
||||
|
||||
definition Node_removeChild_heap :: "(unit, unit, unit, unit, unit, unit, unit, unit, unit, unit, unit) heap" where
|
||||
definition Node_removeChild_heap :: heap⇩f⇩i⇩n⇩a⇩l where
|
||||
"Node_removeChild_heap = create_heap [(cast (document_ptr.Ref 1), cast (create_document_obj html (Some (cast (element_ptr.Ref 1))) [])),
|
||||
(cast (element_ptr.Ref 1), cast (create_element_obj ''html'' [cast (element_ptr.Ref 2), cast (element_ptr.Ref 7)] fmempty None)),
|
||||
(cast (element_ptr.Ref 2), cast (create_element_obj ''head'' [cast (element_ptr.Ref 3), cast (element_ptr.Ref 4), cast (element_ptr.Ref 5), cast (element_ptr.Ref 6)] fmempty None)),
|
||||
|
|
@ -50,17 +52,17 @@ definition Node_removeChild_heap :: "(unit, unit, unit, unit, unit, unit, unit,
|
|||
(cast (element_ptr.Ref 10), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 2)] fmempty None)),
|
||||
(cast (character_data_ptr.Ref 2), cast (create_character_data_obj ''%3C%3Cscript%3E%3E''))]"
|
||||
|
||||
definition document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "document = Some (cast (document_ptr.Ref 1))"
|
||||
definition Node_removeChild_document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "Node_removeChild_document = Some (cast (document_ptr.Ref 1))"
|
||||
|
||||
|
||||
text \<open>"Passing a detached Element to removeChild should not affect it."\<close>
|
||||
|
||||
lemma "test (do {
|
||||
doc \<leftarrow> return document;
|
||||
doc \<leftarrow> return Node_removeChild_document;
|
||||
s \<leftarrow> doc . createElement(''div'');
|
||||
tmp0 \<leftarrow> s . ownerDocument;
|
||||
assert_equals(tmp0, doc);
|
||||
tmp1 \<leftarrow> document . body;
|
||||
tmp1 \<leftarrow> Node_removeChild_document . body;
|
||||
assert_throws(NotFoundError, tmp1 . removeChild(s));
|
||||
tmp2 \<leftarrow> s . ownerDocument;
|
||||
assert_equals(tmp2, doc)
|
||||
|
|
@ -71,13 +73,13 @@ lemma "test (do {
|
|||
text \<open>"Passing a non-detached Element to removeChild should not affect it."\<close>
|
||||
|
||||
lemma "test (do {
|
||||
doc \<leftarrow> return document;
|
||||
doc \<leftarrow> return Node_removeChild_document;
|
||||
s \<leftarrow> doc . createElement(''div'');
|
||||
tmp0 \<leftarrow> doc . documentElement;
|
||||
tmp0 . appendChild(s);
|
||||
tmp1 \<leftarrow> s . ownerDocument;
|
||||
assert_equals(tmp1, doc);
|
||||
tmp2 \<leftarrow> document . body;
|
||||
tmp2 \<leftarrow> Node_removeChild_document . body;
|
||||
assert_throws(NotFoundError, tmp2 . removeChild(s));
|
||||
tmp3 \<leftarrow> s . ownerDocument;
|
||||
assert_equals(tmp3, doc)
|
||||
|
|
@ -88,7 +90,7 @@ lemma "test (do {
|
|||
text \<open>"Calling removeChild on an Element with no children should throw NOT\_FOUND\_ERR."\<close>
|
||||
|
||||
lemma "test (do {
|
||||
doc \<leftarrow> return document;
|
||||
doc \<leftarrow> return Node_removeChild_document;
|
||||
s \<leftarrow> doc . createElement(''div'');
|
||||
tmp0 \<leftarrow> doc . body;
|
||||
tmp0 . appendChild(s);
|
||||
|
|
@ -106,7 +108,7 @@ lemma "test (do {
|
|||
s \<leftarrow> doc . createElement(''div'');
|
||||
tmp0 \<leftarrow> s . ownerDocument;
|
||||
assert_equals(tmp0, doc);
|
||||
tmp1 \<leftarrow> document . body;
|
||||
tmp1 \<leftarrow> Node_removeChild_document . body;
|
||||
assert_throws(NotFoundError, tmp1 . removeChild(s));
|
||||
tmp2 \<leftarrow> s . ownerDocument;
|
||||
assert_equals(tmp2, doc)
|
||||
|
|
@ -123,7 +125,7 @@ lemma "test (do {
|
|||
tmp0 . appendChild(s);
|
||||
tmp1 \<leftarrow> s . ownerDocument;
|
||||
assert_equals(tmp1, doc);
|
||||
tmp2 \<leftarrow> document . body;
|
||||
tmp2 \<leftarrow> Node_removeChild_document . body;
|
||||
assert_throws(NotFoundError, tmp2 . removeChild(s));
|
||||
tmp3 \<leftarrow> s . ownerDocument;
|
||||
assert_equals(tmp3, doc)
|
||||
|
|
@ -148,7 +150,7 @@ lemma "test (do {
|
|||
text \<open>"Passing a value that is not a Node reference to removeChild should throw TypeError."\<close>
|
||||
|
||||
lemma "test (do {
|
||||
tmp0 \<leftarrow> document . body;
|
||||
tmp0 \<leftarrow> Node_removeChild_document . body;
|
||||
assert_throws(TypeError, tmp0 . removeChild(None))
|
||||
}) Node_removeChild_heap"
|
||||
by eval
|
||||
|
|
|
|||
Reference in New Issue