BrowserSecurity
/
Core_DOM-dev
Archived
forked from afp-mirror/Core_DOM
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Renamed tag_type to tag_name and added some tag_name lemmas.

This commit is contained in:
Michael Herzberg 2020-06-08 23:46:58 +01:00
parent 9322d9753d
commit 6008a6c2be
10 changed files with 209 additions and 161 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

269
Core_DOM/Core_DOM/common/Core_DOM_Functions.thy
View File

@ -1346,17 +1346,17 @@ subsubsection \<open>get\_tag\_name\<close>
locale l_get_tag_name\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs
begin
definition a_get_tag_name :: "(_) element_ptr \<Rightarrow> (_, tag_type) dom_prog"
definition a_get_tag_name :: "(_) element_ptr \<Rightarrow> (_, tag_name) dom_prog"
where
"a_get_tag_name element_ptr = get_M element_ptr tag_type"
"a_get_tag_name element_ptr = get_M element_ptr tag_name"
definition a_get_tag_name_locs :: "(_) element_ptr \<Rightarrow> ((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
where
"a_get_tag_name_locs element_ptr \<equiv> {preserved (get_M element_ptr tag_type)}"
"a_get_tag_name_locs element_ptr \<equiv> {preserved (get_M element_ptr tag_name)}"
end
locale l_get_tag_name_defs =
fixes get_tag_name :: "(_) element_ptr \<Rightarrow> (_, tag_type) dom_prog"
fixes get_tag_name :: "(_) element_ptr \<Rightarrow> (_, tag_name) dom_prog"
fixes get_tag_name_locs :: "(_) element_ptr \<Rightarrow> ((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
locale l_get_tag_name\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
@ -1364,7 +1364,7 @@ locale l_get_tag_name\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^
l_get_tag_name_defs get_tag_name get_tag_name_locs +
l_get_tag_name\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs
for type_wf :: "(_) heap \<Rightarrow> bool"
and get_tag_name :: "(_) element_ptr \<Rightarrow> (_, tag_type) dom_prog"
and get_tag_name :: "(_) element_ptr \<Rightarrow> (_, tag_name) dom_prog"
and get_tag_name_locs :: "(_) element_ptr \<Rightarrow> ((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set" +
assumes type_wf_impl: "type_wf = DocumentClass.type_wf"
assumes get_tag_name_impl: "get_tag_name = a_get_tag_name"
@ -1466,7 +1466,7 @@ begin
lemma set_child_nodes_get_tag_name:
"\<forall>w \<in> set_child_nodes_locs ptr. (h \<turnstile> w \<rightarrow>\<^sub>h h' \<longrightarrow> (\<forall>r \<in> get_tag_name_locs ptr'. r h h'))"
by(auto simp add: set_child_nodes_locs_def get_tag_name_locs_def all_args_def
intro: element_put_get_preserved[where getter=tag_type and setter=child_nodes_update])
intro: element_put_get_preserved[where getter=tag_name and setter=child_nodes_update])
end
locale l_set_child_nodes_get_tag_name = l_set_child_nodes + l_get_tag_name +
@ -1489,162 +1489,209 @@ lemma set_child_nodes_get_tag_name_is_l_set_child_nodes_get_tag_name [instances]
subsubsection \<open>set\_tag\_type\<close>
locale l_set_tag_type\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs
locale l_set_tag_name\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs
begin
definition a_set_tag_type :: "(_) element_ptr \<Rightarrow> tag_type \<Rightarrow> (_, unit) dom_prog"
definition a_set_tag_name :: "(_) element_ptr \<Rightarrow> tag_name \<Rightarrow> (_, unit) dom_prog"
where
"a_set_tag_type ptr tag = do {
"a_set_tag_name ptr tag = do {
m \<leftarrow> get_M ptr attrs;
put_M ptr tag_type_update tag
put_M ptr tag_name_update tag
}"
lemmas set_tag_type_defs = a_set_tag_type_def
lemmas set_tag_name_defs = a_set_tag_name_def
definition a_set_tag_type_locs :: "(_) element_ptr \<Rightarrow> (_, unit) dom_prog set"
definition a_set_tag_name_locs :: "(_) element_ptr \<Rightarrow> (_, unit) dom_prog set"
where
"a_set_tag_type_locs element_ptr \<equiv> all_args (put_M element_ptr tag_type_update)"
"a_set_tag_name_locs element_ptr \<equiv> all_args (put_M element_ptr tag_name_update)"
end
locale l_set_tag_type_defs =
fixes set_tag_type :: "(_) element_ptr \<Rightarrow> tag_type \<Rightarrow> (_, unit) dom_prog"
fixes set_tag_type_locs :: "(_) element_ptr \<Rightarrow> (_, unit) dom_prog set"
locale l_set_tag_name_defs =
fixes set_tag_name :: "(_) element_ptr \<Rightarrow> tag_name \<Rightarrow> (_, unit) dom_prog"
fixes set_tag_name_locs :: "(_) element_ptr \<Rightarrow> (_, unit) dom_prog set"
locale l_set_tag_type\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
locale l_set_tag_name\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
l_type_wf type_wf +
l_set_tag_type_defs set_tag_type set_tag_type_locs +
l_set_tag_type\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs
l_set_tag_name_defs set_tag_name set_tag_name_locs +
l_set_tag_name\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs
for type_wf :: "(_) heap \<Rightarrow> bool"
and set_tag_type :: "(_) element_ptr \<Rightarrow> char list \<Rightarrow> (_, unit) dom_prog"
and set_tag_type_locs :: "(_) element_ptr \<Rightarrow> (_, unit) dom_prog set" +
and set_tag_name :: "(_) element_ptr \<Rightarrow> char list \<Rightarrow> (_, unit) dom_prog"
and set_tag_name_locs :: "(_) element_ptr \<Rightarrow> (_, unit) dom_prog set" +
assumes type_wf_impl: "type_wf = DocumentClass.type_wf"
assumes set_tag_type_impl: "set_tag_type = a_set_tag_type"
assumes set_tag_type_locs_impl: "set_tag_type_locs = a_set_tag_type_locs"
assumes set_tag_name_impl: "set_tag_name = a_set_tag_name"
assumes set_tag_name_locs_impl: "set_tag_name_locs = a_set_tag_name_locs"
begin
lemma set_tag_type_ok:
"type_wf h \<Longrightarrow> element_ptr |\<in>| element_ptr_kinds h \<Longrightarrow> h \<turnstile> ok (set_tag_type element_ptr tag)"
lemma set_tag_name_ok:
"type_wf h \<Longrightarrow> element_ptr |\<in>| element_ptr_kinds h \<Longrightarrow> h \<turnstile> ok (set_tag_name element_ptr tag)"
apply(unfold type_wf_impl)
unfolding set_tag_type_impl[unfolded a_set_tag_type_def] using get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ok put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ok
unfolding set_tag_name_impl[unfolded a_set_tag_name_def] using get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ok put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ok
by (metis (no_types, lifting) DocumentClass.type_wf\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t ElementMonad.get_M_pure bind_is_OK_E
bind_is_OK_pure_I is_OK_returns_result_I)
lemma set_tag_type_writes:
"writes (set_tag_type_locs element_ptr) (set_tag_type element_ptr tag) h h'"
by(auto simp add: set_tag_type_impl[unfolded a_set_tag_type_def]
set_tag_type_locs_impl[unfolded a_set_tag_type_locs_def] intro: writes_bind_pure)
lemma set_tag_name_writes:
"writes (set_tag_name_locs element_ptr) (set_tag_name element_ptr tag) h h'"
by(auto simp add: set_tag_name_impl[unfolded a_set_tag_name_def]
set_tag_name_locs_impl[unfolded a_set_tag_name_locs_def] intro: writes_bind_pure)
lemma set_tag_type_pointers_preserved:
assumes "w \<in> set_tag_type_locs element_ptr"
lemma set_tag_name_pointers_preserved:
assumes "w \<in> set_tag_name_locs element_ptr"
assumes "h \<turnstile> w \<rightarrow>\<^sub>h h'"
shows "object_ptr_kinds h = object_ptr_kinds h'"
using assms(1) object_ptr_kinds_preserved[OF writes_singleton2 assms(2)]
by(auto simp add: all_args_def set_tag_type_locs_impl[unfolded a_set_tag_type_locs_def]
by(auto simp add: all_args_def set_tag_name_locs_impl[unfolded a_set_tag_name_locs_def]
split: if_splits)
lemma set_tag_type_typess_preserved:
assumes "w \<in> set_tag_type_locs element_ptr"
lemma set_tag_name_typess_preserved:
assumes "w \<in> set_tag_name_locs element_ptr"
assumes "h \<turnstile> w \<rightarrow>\<^sub>h h'"
shows "type_wf h = type_wf h'"
apply(unfold type_wf_impl)
using assms(1) type_wf_preserved[OF writes_singleton2 assms(2)]
by(auto simp add: all_args_def set_tag_type_locs_impl[unfolded a_set_tag_type_locs_def]
by(auto simp add: all_args_def set_tag_name_locs_impl[unfolded a_set_tag_name_locs_def]
split: if_splits)
end
locale l_set_tag_type = l_type_wf + l_set_tag_type_defs +
assumes set_tag_type_writes:
"writes (set_tag_type_locs element_ptr) (set_tag_type element_ptr tag) h h'"
assumes set_tag_type_ok:
"type_wf h \<Longrightarrow> element_ptr |\<in>| element_ptr_kinds h \<Longrightarrow> h \<turnstile> ok (set_tag_type element_ptr tag)"
assumes set_tag_type_pointers_preserved:
"w \<in> set_tag_type_locs element_ptr \<Longrightarrow> h \<turnstile> w \<rightarrow>\<^sub>h h' \<Longrightarrow> object_ptr_kinds h = object_ptr_kinds h'"
assumes set_tag_type_types_preserved:
"w \<in> set_tag_type_locs element_ptr \<Longrightarrow> h \<turnstile> w \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
locale l_set_tag_name = l_type_wf + l_set_tag_name_defs +
assumes set_tag_name_writes:
"writes (set_tag_name_locs element_ptr) (set_tag_name element_ptr tag) h h'"
assumes set_tag_name_ok:
"type_wf h \<Longrightarrow> element_ptr |\<in>| element_ptr_kinds h \<Longrightarrow> h \<turnstile> ok (set_tag_name element_ptr tag)"
assumes set_tag_name_pointers_preserved:
"w \<in> set_tag_name_locs element_ptr \<Longrightarrow> h \<turnstile> w \<rightarrow>\<^sub>h h' \<Longrightarrow> object_ptr_kinds h = object_ptr_kinds h'"
assumes set_tag_name_types_preserved:
"w \<in> set_tag_name_locs element_ptr \<Longrightarrow> h \<turnstile> w \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
global_interpretation l_set_tag_type\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs defines
set_tag_type = l_set_tag_type\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.a_set_tag_type and
set_tag_type_locs = l_set_tag_type\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.a_set_tag_type_locs .
global_interpretation l_set_tag_name\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs defines
set_tag_name = l_set_tag_name\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.a_set_tag_name and
set_tag_name_locs = l_set_tag_name\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.a_set_tag_name_locs .
interpretation
i_set_tag_type?: l_set_tag_type\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M type_wf set_tag_type set_tag_type_locs
i_set_tag_name?: l_set_tag_name\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M type_wf set_tag_name set_tag_name_locs
apply(unfold_locales)
by (auto simp add: set_tag_type_def set_tag_type_locs_def)
declare l_set_tag_type\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms[instances]
by (auto simp add: set_tag_name_def set_tag_name_locs_def)
declare l_set_tag_name\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms[instances]
lemma set_tag_type_is_l_set_tag_type [instances]:
"l_set_tag_type type_wf set_tag_type set_tag_type_locs"
apply(simp add: l_set_tag_type_def)
using set_tag_type_ok set_tag_type_writes set_tag_type_pointers_preserved
set_tag_type_typess_preserved
lemma set_tag_name_is_l_set_tag_name [instances]:
"l_set_tag_name type_wf set_tag_name set_tag_name_locs"
apply(simp add: l_set_tag_name_def)
using set_tag_name_ok set_tag_name_writes set_tag_name_pointers_preserved
set_tag_name_typess_preserved
by blast
paragraph \<open>get\_child\_nodes\<close>
locale l_set_tag_type_get_child_nodes\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
l_set_tag_type\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
locale l_set_tag_name_get_child_nodes\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
l_set_tag_name\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
l_get_child_nodes\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
begin
lemma set_tag_type_get_child_nodes:
"\<forall>w \<in> set_tag_type_locs ptr. (h \<turnstile> w \<rightarrow>\<^sub>h h' \<longrightarrow> (\<forall>r \<in> get_child_nodes_locs ptr'. r h h'))"
by(auto simp add: set_tag_type_locs_impl[unfolded a_set_tag_type_locs_def]
lemma set_tag_name_get_child_nodes:
"\<forall>w \<in> set_tag_name_locs ptr. (h \<turnstile> w \<rightarrow>\<^sub>h h' \<longrightarrow> (\<forall>r \<in> get_child_nodes_locs ptr'. r h h'))"
by(auto simp add: set_tag_name_locs_impl[unfolded a_set_tag_name_locs_def]
get_child_nodes_locs_impl[unfolded a_get_child_nodes_locs_def] all_args_def
intro: element_put_get_preserved[where setter=tag_type_update and getter=child_nodes])
intro: element_put_get_preserved[where setter=tag_name_update and getter=child_nodes])
end
locale l_set_tag_type_get_child_nodes = l_set_tag_type + l_get_child_nodes +
assumes set_tag_type_get_child_nodes:
"\<forall>w \<in> set_tag_type_locs ptr. (h \<turnstile> w \<rightarrow>\<^sub>h h' \<longrightarrow> (\<forall>r \<in> get_child_nodes_locs ptr'. r h h'))"
locale l_set_tag_name_get_child_nodes = l_set_tag_name + l_get_child_nodes +
assumes set_tag_name_get_child_nodes:
"\<forall>w \<in> set_tag_name_locs ptr. (h \<turnstile> w \<rightarrow>\<^sub>h h' \<longrightarrow> (\<forall>r \<in> get_child_nodes_locs ptr'. r h h'))"
interpretation
i_set_tag_type_get_child_nodes?: l_set_tag_type_get_child_nodes\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M type_wf
set_tag_type set_tag_type_locs known_ptr
i_set_tag_name_get_child_nodes?: l_set_tag_name_get_child_nodes\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M type_wf
set_tag_name set_tag_name_locs known_ptr
get_child_nodes get_child_nodes_locs
by unfold_locales
declare l_set_tag_type_get_child_nodes\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms[instances]
declare l_set_tag_name_get_child_nodes\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms[instances]
lemma set_tag_type_get_child_nodes_is_l_set_tag_type_get_child_nodes [instances]:
"l_set_tag_type_get_child_nodes type_wf set_tag_type set_tag_type_locs known_ptr get_child_nodes
lemma set_tag_name_get_child_nodes_is_l_set_tag_name_get_child_nodes [instances]:
"l_set_tag_name_get_child_nodes type_wf set_tag_name set_tag_name_locs known_ptr get_child_nodes
get_child_nodes_locs"
using set_tag_type_is_l_set_tag_type get_child_nodes_is_l_get_child_nodes
apply(simp add: l_set_tag_type_get_child_nodes_def l_set_tag_type_get_child_nodes_axioms_def)
using set_tag_type_get_child_nodes
using set_tag_name_is_l_set_tag_name get_child_nodes_is_l_get_child_nodes
apply(simp add: l_set_tag_name_get_child_nodes_def l_set_tag_name_get_child_nodes_axioms_def)
using set_tag_name_get_child_nodes
by fast
paragraph \<open>get\_disconnected\_nodes\<close>
locale l_set_tag_type_get_disconnected_nodes\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
l_set_tag_type\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
locale l_set_tag_name_get_disconnected_nodes\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
l_set_tag_name\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
l_get_disconnected_nodes\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
begin
lemma set_tag_type_get_disconnected_nodes:
"\<forall>w \<in> set_tag_type_locs ptr. (h \<turnstile> w \<rightarrow>\<^sub>h h' \<longrightarrow> (\<forall>r \<in> get_disconnected_nodes_locs ptr'. r h h'))"
by(auto simp add: set_tag_type_locs_impl[unfolded a_set_tag_type_locs_def]
lemma set_tag_name_get_disconnected_nodes:
"\<forall>w \<in> set_tag_name_locs ptr. (h \<turnstile> w \<rightarrow>\<^sub>h h' \<longrightarrow> (\<forall>r \<in> get_disconnected_nodes_locs ptr'. r h h'))"
by(auto simp add: set_tag_name_locs_impl[unfolded a_set_tag_name_locs_def]
get_disconnected_nodes_locs_impl[unfolded a_get_disconnected_nodes_locs_def]
all_args_def)
end
locale l_set_tag_type_get_disconnected_nodes = l_set_tag_type + l_get_disconnected_nodes +
assumes set_tag_type_get_disconnected_nodes:
"\<forall>w \<in> set_tag_type_locs ptr. (h \<turnstile> w \<rightarrow>\<^sub>h h' \<longrightarrow> (\<forall>r \<in> get_disconnected_nodes_locs ptr'. r h h'))"
locale l_set_tag_name_get_disconnected_nodes = l_set_tag_name + l_get_disconnected_nodes +
assumes set_tag_name_get_disconnected_nodes:
"\<forall>w \<in> set_tag_name_locs ptr. (h \<turnstile> w \<rightarrow>\<^sub>h h' \<longrightarrow> (\<forall>r \<in> get_disconnected_nodes_locs ptr'. r h h'))"
interpretation
i_set_tag_type_get_disconnected_nodes?: l_set_tag_type_get_disconnected_nodes\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M type_wf
set_tag_type set_tag_type_locs get_disconnected_nodes
i_set_tag_name_get_disconnected_nodes?: l_set_tag_name_get_disconnected_nodes\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M type_wf
set_tag_name set_tag_name_locs get_disconnected_nodes
get_disconnected_nodes_locs
by unfold_locales
declare l_set_tag_type_get_disconnected_nodes\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms[instances]
declare l_set_tag_name_get_disconnected_nodes\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms[instances]
lemma set_tag_type_get_disconnected_nodes_is_l_set_tag_type_get_disconnected_nodes [instances]:
"l_set_tag_type_get_disconnected_nodes type_wf set_tag_type set_tag_type_locs get_disconnected_nodes
lemma set_tag_name_get_disconnected_nodes_is_l_set_tag_name_get_disconnected_nodes [instances]:
"l_set_tag_name_get_disconnected_nodes type_wf set_tag_name set_tag_name_locs get_disconnected_nodes
get_disconnected_nodes_locs"
using set_tag_type_is_l_set_tag_type get_disconnected_nodes_is_l_get_disconnected_nodes
apply(simp add: l_set_tag_type_get_disconnected_nodes_def
l_set_tag_type_get_disconnected_nodes_axioms_def)
using set_tag_type_get_disconnected_nodes
using set_tag_name_is_l_set_tag_name get_disconnected_nodes_is_l_get_disconnected_nodes
apply(simp add: l_set_tag_name_get_disconnected_nodes_def
l_set_tag_name_get_disconnected_nodes_axioms_def)
using set_tag_name_get_disconnected_nodes
by fast
paragraph \<open>get\_tag\_type\<close>
locale l_set_tag_name_get_tag_name\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M = l_get_tag_name\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
+ l_set_tag_name\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
begin
lemma set_tag_name_get_tag_name:
assumes "h \<turnstile> a_set_tag_name element_ptr tag \<rightarrow>\<^sub>h h'"
shows "h' \<turnstile> a_get_tag_name element_ptr \<rightarrow>\<^sub>r tag"
using assms
by(auto simp add: a_get_tag_name_def a_set_tag_name_def)
lemma set_tag_name_get_tag_name_different_pointers:
assumes "ptr \<noteq> ptr'"
assumes "w \<in> a_set_tag_name_locs ptr"
assumes "h \<turnstile> w \<rightarrow>\<^sub>h h'"
assumes "r \<in> a_get_tag_name_locs ptr'"
shows "r h h'"
using assms
by(auto simp add: all_args_def a_set_tag_name_locs_def a_get_tag_name_locs_def
split: if_splits option.splits )
end
locale l_set_tag_name_get_tag_name = l_get_tag_name + l_set_tag_name +
assumes set_tag_name_get_tag_name:
"h \<turnstile> set_tag_name element_ptr tag \<rightarrow>\<^sub>h h'
\<Longrightarrow> h' \<turnstile> get_tag_name element_ptr \<rightarrow>\<^sub>r tag"
assumes set_tag_name_get_tag_name_different_pointers:
"ptr \<noteq> ptr' \<Longrightarrow> w \<in> set_tag_name_locs ptr \<Longrightarrow> h \<turnstile> w \<rightarrow>\<^sub>h h'
\<Longrightarrow> r \<in> get_tag_name_locs ptr' \<Longrightarrow> r h h'"
interpretation i_set_tag_name_get_tag_name?:
l_set_tag_name_get_tag_name\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M type_wf get_tag_name
get_tag_name_locs set_tag_name set_tag_name_locs
by unfold_locales
declare l_set_tag_name_get_tag_name\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms[instances]
lemma set_tag_name_get_tag_name_is_l_set_tag_name_get_tag_name [instances]:
"l_set_tag_name_get_tag_name type_wf get_tag_name get_tag_name_locs
set_tag_name set_tag_name_locs"
using set_tag_name_is_l_set_tag_name get_tag_name_is_l_get_tag_name
apply(simp add: l_set_tag_name_get_tag_name_def
l_set_tag_name_get_tag_name_axioms_def)
using set_tag_name_get_tag_name
set_tag_name_get_tag_name_different_pointers
by fast+
subsubsection \<open>set\_val\<close>
locale l_set_val\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs
@ -3203,7 +3250,7 @@ subsubsection \<open>create\_element\<close>
locale l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs =
l_get_disconnected_nodes_defs get_disconnected_nodes get_disconnected_nodes_locs +
l_set_disconnected_nodes_defs set_disconnected_nodes set_disconnected_nodes_locs +
l_set_tag_type_defs set_tag_type set_tag_type_locs
l_set_tag_name_defs set_tag_name set_tag_name_locs
for get_disconnected_nodes ::
"(_) document_ptr \<Rightarrow> ((_) heap, exception, (_) node_ptr list) prog"
and get_disconnected_nodes_locs ::
@ -3212,16 +3259,16 @@ locale l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\
"(_) document_ptr \<Rightarrow> (_) node_ptr list \<Rightarrow> ((_) heap, exception, unit) prog"
and set_disconnected_nodes_locs ::
"(_) document_ptr \<Rightarrow> ((_) heap, exception, unit) prog set"
and set_tag_type ::
and set_tag_name ::
"(_) element_ptr \<Rightarrow> char list \<Rightarrow> ((_) heap, exception, unit) prog"
and set_tag_type_locs ::
and set_tag_name_locs ::
"(_) element_ptr \<Rightarrow> ((_) heap, exception, unit) prog set"
begin
definition a_create_element :: "(_) document_ptr \<Rightarrow> tag_type \<Rightarrow> (_, (_) element_ptr) dom_prog"
definition a_create_element :: "(_) document_ptr \<Rightarrow> tag_name \<Rightarrow> (_, (_) element_ptr) dom_prog"
where
"a_create_element document_ptr tag = do {
new_element_ptr \<leftarrow> new_element;
set_tag_type new_element_ptr tag;
set_tag_name new_element_ptr tag;
disc_nodes \<leftarrow> get_disconnected_nodes document_ptr;
set_disconnected_nodes document_ptr (cast new_element_ptr # disc_nodes);
return new_element_ptr
@ -3229,28 +3276,28 @@ definition a_create_element :: "(_) document_ptr \<Rightarrow> tag_type \<Righta
end
locale l_create_element_defs =
fixes create_element :: "(_) document_ptr \<Rightarrow> tag_type \<Rightarrow> (_, (_) element_ptr) dom_prog"
fixes create_element :: "(_) document_ptr \<Rightarrow> tag_name \<Rightarrow> (_, (_) element_ptr) dom_prog"
global_interpretation l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs get_disconnected_nodes get_disconnected_nodes_locs
set_disconnected_nodes set_disconnected_nodes_locs
set_tag_type set_tag_type_locs
set_tag_name set_tag_name_locs
defines
create_element = "l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.a_create_element get_disconnected_nodes
set_disconnected_nodes set_tag_type"
set_disconnected_nodes set_tag_name"
.
locale l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs set_tag_type set_tag_type_locs +
l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs set_tag_name set_tag_name_locs +
l_get_disconnected_nodes type_wf get_disconnected_nodes get_disconnected_nodes_locs +
l_set_tag_type type_wf set_tag_type set_tag_type_locs +
l_set_tag_name type_wf set_tag_name set_tag_name_locs +
l_create_element_defs create_element +
l_known_ptr known_ptr
for get_disconnected_nodes :: "(_) document_ptr \<Rightarrow> ((_) heap, exception, (_) node_ptr list) prog"
and get_disconnected_nodes_locs :: "(_) document_ptr \<Rightarrow> ((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
and set_disconnected_nodes :: "(_) document_ptr \<Rightarrow> (_) node_ptr list \<Rightarrow> ((_) heap, exception, unit) prog"
and set_disconnected_nodes_locs :: "(_) document_ptr \<Rightarrow> ((_) heap, exception, unit) prog set"
and set_tag_type :: "(_) element_ptr \<Rightarrow> char list \<Rightarrow> ((_) heap, exception, unit) prog"
and set_tag_type_locs :: "(_) element_ptr \<Rightarrow> ((_) heap, exception, unit) prog set"
and set_tag_name :: "(_) element_ptr \<Rightarrow> char list \<Rightarrow> ((_) heap, exception, unit) prog"
and set_tag_name_locs :: "(_) element_ptr \<Rightarrow> ((_) heap, exception, unit) prog set"
and type_wf :: "(_) heap \<Rightarrow> bool"
and create_element :: "(_) document_ptr \<Rightarrow> char list \<Rightarrow> ((_) heap, exception, (_) element_ptr) prog"
and known_ptr :: "(_) object_ptr \<Rightarrow> bool" +
@ -3270,7 +3317,7 @@ proof -
obtain new_element_ptr h2 h3 disc_nodes_h3 where
new_element_ptr: "h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr" and
h2: "h \<turnstile> new_element \<rightarrow>\<^sub>h h2" and
h3: "h2 \<turnstile> set_tag_type new_element_ptr tag \<rightarrow>\<^sub>h h3" and
h3: "h2 \<turnstile> set_tag_name new_element_ptr tag \<rightarrow>\<^sub>h h3" and
disc_nodes_h3: "h3 \<turnstile> get_disconnected_nodes document_ptr \<rightarrow>\<^sub>r disc_nodes_h3" and
h': "h3 \<turnstile> set_disconnected_nodes document_ptr (cast new_element_ptr # disc_nodes_h3) \<rightarrow>\<^sub>h h'"
by(auto simp add: create_element_def
@ -3281,8 +3328,8 @@ proof -
using new_element_new_ptr h2 new_element_ptr by blast
moreover have object_ptr_kinds_eq_h2: "object_ptr_kinds h3 = object_ptr_kinds h2"
apply(rule writes_small_big[where P="\<lambda>h h'. object_ptr_kinds h' = object_ptr_kinds h", OF set_tag_type_writes h3])
using set_tag_type_pointers_preserved
apply(rule writes_small_big[where P="\<lambda>h h'. object_ptr_kinds h' = object_ptr_kinds h", OF set_tag_name_writes h3])
using set_tag_name_pointers_preserved
by (auto simp add: reflp_def transp_def)
moreover have "document_ptr |\<in>| document_ptr_kinds h3"
by (meson disc_nodes_h3 is_OK_returns_result_I local.get_disconnected_nodes_ptr_in_heap)
@ -3308,7 +3355,7 @@ end
locale l_create_element = l_create_element_defs
interpretation
i_create_element?: l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs set_tag_type set_tag_type_locs type_wf create_element known_ptr
i_create_element?: l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs set_tag_name set_tag_name_locs type_wf create_element known_ptr
by(auto simp add: l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms_def create_element_def instances)
declare l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms[instances]
@ -3612,11 +3659,11 @@ definition a_get_elements_by_class_name :: "(_) object_ptr \<Rightarrow> attr_va
definition a_get_elements_by_tag_name :: "(_) object_ptr \<Rightarrow> attr_value \<Rightarrow> (_, (_) element_ptr list) dom_prog"
where
"a_get_elements_by_tag_name ptr tag_name = to_tree_order ptr \<bind>
"a_get_elements_by_tag_name ptr tag = to_tree_order ptr \<bind>
map_filter_M (\<lambda>ptr. (case cast ptr of
Some element_ptr \<Rightarrow> do {
this_tag_name \<leftarrow> get_M element_ptr tag_type;
(if this_tag_name = tag_name then return (Some element_ptr) else return None)
this_tag_name \<leftarrow> get_M element_ptr tag_name;
(if this_tag_name = tag then return (Some element_ptr) else return None)
}
| _ \<Rightarrow> return None))"
end
@ -3696,7 +3743,7 @@ lemma get_elements_by_tag_name_result_in_tree_order:
intro!: map_filter_M_pure map_M_pure_I bind_pure_I
split: option.splits list.splits if_splits)
lemma get_elements_by_tag_name_pure [simp]: "pure (get_elements_by_tag_name ptr tag_name) h"
lemma get_elements_by_tag_name_pure [simp]: "pure (get_elements_by_tag_name ptr tag) h"
by(auto simp add: get_elements_by_tag_name_def
intro!: bind_pure_I map_filter_M_pure
split: option.splits)
@ -3706,7 +3753,7 @@ locale l_get_element_by = l_get_element_by_defs + l_to_tree_order_defs +
assumes get_element_by_id_result_in_tree_order:
"h \<turnstile> get_element_by_id ptr iden \<rightarrow>\<^sub>r Some element_ptr \<Longrightarrow> h \<turnstile> to_tree_order ptr \<rightarrow>\<^sub>r to
\<Longrightarrow> cast element_ptr \<in> set to"
assumes get_elements_by_tag_name_pure [simp]: "pure (get_elements_by_tag_name ptr tag_name) h"
assumes get_elements_by_tag_name_pure [simp]: "pure (get_elements_by_tag_name ptr tag) h"
interpretation
i_get_element_by?: l_get_element_by\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M to_tree_order first_in_tree_order get_attribute

3
Core_DOM/Core_DOM/common/monads/BaseMonad.thy
View File

@ -37,7 +37,8 @@ begin
subsection\<open>Datatypes\<close>
datatype exception = NotFoundError | SegmentationFault | HierarchyRequestError | AssertException
| NonTerminationException | InvokeError | TypeError | DebugException nat
| NonTerminationException | InvokeError | TypeError | DebugException nat | NotSupportedError
| InvalidStateError
lemma finite_set_in [simp]: "x \<in> fset FS \<longleftrightarrow> x |\<in>| FS"
by (meson notin_fset)

4
Core_DOM/Core_DOM/common/monads/CharacterDataMonad.thy
View File

@ -340,8 +340,8 @@ lemma new_element_is_l_new_element: "l_new_element type_wf"
using l_new_element.intro new_element_type_wf_preserved
by blast
lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_tag_type_type_wf_preserved [simp]:
"h \<turnstile> put_M element_ptr tag_type_update v \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_tag_name_type_wf_preserved [simp]:
"h \<turnstile> put_M element_ptr tag_name_update v \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
apply(auto simp add: ElementMonad.put_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
dest!: get_heap_E
elim!: bind_returns_heap_E2

4
Core_DOM/Core_DOM/common/monads/DocumentMonad.thy
View File

@ -347,8 +347,8 @@ lemma new_element_is_l_new_element [instances]:
using l_new_element.intro new_element_type_wf_preserved
by blast
lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_tag_type_type_wf_preserved [simp]:
"h \<turnstile> put_M element_ptr tag_type_update v \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_tag_name_type_wf_preserved [simp]:
"h \<turnstile> put_M element_ptr tag_name_update v \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
apply(auto simp add: ElementMonad.put_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
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 DocumentClass.type_wf\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t
DocumentClass.type_wf\<^sub>N\<^sub>o\<^sub>d\<^sub>e DocumentClass.type_wf\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t

8
Core_DOM/Core_DOM/common/monads/ElementMonad.thy
View File

@ -233,10 +233,10 @@ lemma new_element_child_nodes:
by(auto simp add: get_M_defs new_element_def new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def
split: option.splits prod.splits elim!: bind_returns_result_E bind_returns_heap_E)
lemma new_element_tag_type:
lemma new_element_tag_name:
assumes "h \<turnstile> new_element \<rightarrow>\<^sub>h h'"
assumes "h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr"
shows "h' \<turnstile> get_M new_element_ptr tag_type \<rightarrow>\<^sub>r ''''"
shows "h' \<turnstile> get_M new_element_ptr tag_name \<rightarrow>\<^sub>r ''''"
using assms
by(auto simp add: get_M_defs new_element_def new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def
split: option.splits prod.splits elim!: bind_returns_result_E bind_returns_heap_E)
@ -338,8 +338,8 @@ lemma new_element_is_l_new_element: "l_new_element type_wf"
using l_new_element.intro new_element_type_wf_preserved
by blast
lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_tag_type_type_wf_preserved [simp]:
"h \<turnstile> put_M element_ptr tag_type_update v \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_tag_name_type_wf_preserved [simp]:
"h \<turnstile> put_M element_ptr tag_name_update v \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
apply(auto simp add: type_wf_defs NodeClass.type_wf_defs ObjectClass.type_wf_defs
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

6
Core_DOM/Core_DOM/common/tests/Core_DOM_BaseTest.thy
View File

@ -150,8 +150,8 @@ notation get_elements_by_class_name_with_null ("_ . getElementsByClassName'(_')"
fun get_elements_by_tag_name_with_null :: "((_::linorder) object_ptr option) \<Rightarrow> string \<Rightarrow> (_, ((_) object_ptr option) list) dom_prog"
where
"get_elements_by_tag_name_with_null (Some ptr) tag_name =
get_elements_by_tag_name ptr tag_name \<bind> map_M (return \<circ> Some \<circ> 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)"
"get_elements_by_tag_name_with_null (Some ptr) tag =
get_elements_by_tag_name ptr tag \<bind> map_M (return \<circ> Some \<circ> 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)"
notation get_elements_by_tag_name_with_null ("_ . getElementsByTagName'(_')")
fun insert_before_with_null :: "((_::linorder) object_ptr option) \<Rightarrow> ((_) object_ptr option) \<Rightarrow> ((_) object_ptr option) \<Rightarrow> (_, ((_) object_ptr option)) dom_prog"
@ -222,7 +222,7 @@ notation remove_child_with_null ("_ . removeChild")
fun get_tag_name_with_null :: "((_) object_ptr option) \<Rightarrow> (_, attr_value) dom_prog"
where
"get_tag_name_with_null (Some ptr) = (case cast ptr of
Some element_ptr \<Rightarrow> get_M element_ptr tag_type)"
Some element_ptr \<Rightarrow> get_M element_ptr tag_name)"
notation get_tag_name_with_null ("_ . tagName")
abbreviation "remove_attribute_with_null ptr k \<equiv> set_attribute_with_null2 ptr k None"

30
Core_DOM/Core_DOM/standard/Core_DOM_Heap_WF.thy
View File

@ -6700,12 +6700,12 @@ locale l_create_element_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub
get_disconnected_nodes get_disconnected_nodes_locs
heap_is_wellformed parent_child_rel +
l_new_element_get_disconnected_nodes get_disconnected_nodes get_disconnected_nodes_locs +
l_set_tag_type_get_disconnected_nodes type_wf set_tag_type set_tag_type_locs
l_set_tag_name_get_disconnected_nodes type_wf set_tag_name set_tag_name_locs
get_disconnected_nodes get_disconnected_nodes_locs +
l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes
set_disconnected_nodes_locs set_tag_type set_tag_type_locs type_wf create_element known_ptr +
set_disconnected_nodes_locs set_tag_name set_tag_name_locs type_wf create_element known_ptr +
l_new_element_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs +
l_set_tag_type_get_child_nodes type_wf set_tag_type set_tag_type_locs known_ptr
l_set_tag_name_get_child_nodes type_wf set_tag_name set_tag_name_locs known_ptr
get_child_nodes get_child_nodes_locs +
l_set_disconnected_nodes_get_child_nodes set_disconnected_nodes set_disconnected_nodes_locs
get_child_nodes get_child_nodes_locs +
@ -6723,8 +6723,8 @@ locale l_create_element_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub
and get_disconnected_nodes_locs :: "(_) document_ptr \<Rightarrow> ((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
and heap_is_wellformed :: "(_) heap \<Rightarrow> bool"
and parent_child_rel :: "(_) heap \<Rightarrow> ((_) object_ptr \<times> (_) object_ptr) set"
and set_tag_type :: "(_) element_ptr \<Rightarrow> char list \<Rightarrow> ((_) heap, exception, unit) prog"
and set_tag_type_locs :: "(_) element_ptr \<Rightarrow> ((_) heap, exception, unit) prog set"
and set_tag_name :: "(_) element_ptr \<Rightarrow> char list \<Rightarrow> ((_) heap, exception, unit) prog"
and set_tag_name_locs :: "(_) element_ptr \<Rightarrow> ((_) heap, exception, unit) prog set"
and set_disconnected_nodes :: "(_) document_ptr \<Rightarrow> (_) node_ptr list \<Rightarrow> ((_) heap, exception, unit) prog"
and set_disconnected_nodes_locs :: "(_) document_ptr \<Rightarrow> ((_) heap, exception, unit) prog set"
and create_element :: "(_) document_ptr \<Rightarrow> char list \<Rightarrow> ((_) heap, exception, (_) element_ptr) prog"
@ -6739,7 +6739,7 @@ proof -
obtain new_element_ptr h2 h3 disc_nodes_h3 where
new_element_ptr: "h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr" and
h2: "h \<turnstile> new_element \<rightarrow>\<^sub>h h2" and
h3: "h2 \<turnstile> set_tag_type new_element_ptr tag \<rightarrow>\<^sub>h h3" and
h3: "h2 \<turnstile> set_tag_name new_element_ptr tag \<rightarrow>\<^sub>h h3" and
disc_nodes_h3: "h3 \<turnstile> get_disconnected_nodes document_ptr \<rightarrow>\<^sub>r disc_nodes_h3" and
h': "h3 \<turnstile> set_disconnected_nodes document_ptr (cast new_element_ptr # disc_nodes_h3) \<rightarrow>\<^sub>h h'"
using assms(2)
@ -6776,8 +6776,8 @@ proof -
by(auto simp add: document_ptr_kinds_def)
have object_ptr_kinds_eq_h2: "object_ptr_kinds h3 = object_ptr_kinds h2"
apply(rule writes_small_big[where P="\<lambda>h h'. object_ptr_kinds h' = object_ptr_kinds h", OF set_tag_type_writes h3])
using set_tag_type_pointers_preserved
apply(rule writes_small_big[where P="\<lambda>h h'. object_ptr_kinds h' = object_ptr_kinds h", OF set_tag_name_writes h3])
using set_tag_name_pointers_preserved
by (auto simp add: reflp_def transp_def)
then have document_ptr_kinds_eq_h2: "document_ptr_kinds h3 = document_ptr_kinds h2"
by (auto simp add: document_ptr_kinds_def)
@ -6840,17 +6840,17 @@ proof -
have children_eq_h2:
"\<And>ptr' children. h2 \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children = h3 \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children"
using get_child_nodes_reads set_tag_type_writes h3
using get_child_nodes_reads set_tag_name_writes h3
apply(rule reads_writes_preserved)
by(auto simp add: set_tag_type_get_child_nodes)
by(auto simp add: set_tag_name_get_child_nodes)
then have children_eq2_h2: "\<And>ptr'. |h2 \<turnstile> get_child_nodes ptr'|\<^sub>r = |h3 \<turnstile> get_child_nodes ptr'|\<^sub>r"
using select_result_eq by force
have disconnected_nodes_eq_h2:
"\<And>doc_ptr disc_nodes. h2 \<turnstile> get_disconnected_nodes doc_ptr \<rightarrow>\<^sub>r disc_nodes
= h3 \<turnstile> get_disconnected_nodes doc_ptr \<rightarrow>\<^sub>r disc_nodes"
using get_disconnected_nodes_reads set_tag_type_writes h3
using get_disconnected_nodes_reads set_tag_name_writes h3
apply(rule reads_writes_preserved)
by(auto simp add: set_tag_type_get_disconnected_nodes)
by(auto simp add: set_tag_name_get_disconnected_nodes)
then have disconnected_nodes_eq2_h2:
"\<And>doc_ptr. |h2 \<turnstile> get_disconnected_nodes doc_ptr|\<^sub>r = |h3 \<turnstile> get_disconnected_nodes doc_ptr|\<^sub>r"
using select_result_eq by force
@ -6858,8 +6858,8 @@ proof -
have "type_wf h2"
using \<open>type_wf h\<close> new_element_types_preserved h2 by blast
then have "type_wf h3"
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF set_tag_type_writes h3]
using set_tag_type_types_preserved
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF set_tag_name_writes h3]
using set_tag_name_types_preserved
by(auto simp add: reflp_def transp_def)
then show "type_wf h'"
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF set_disconnected_nodes_writes h']
@ -7074,7 +7074,7 @@ end
interpretation i_create_element_wf?: l_create_element_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M known_ptr known_ptrs type_wf
get_child_nodes get_child_nodes_locs get_disconnected_nodes
get_disconnected_nodes_locs heap_is_wellformed parent_child_rel
set_tag_type set_tag_type_locs
set_tag_name set_tag_name_locs
set_disconnected_nodes set_disconnected_nodes_locs create_element
using instances
by(auto simp add: l_create_element_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def)

8
Core_DOM/Core_DOM/standard/classes/ElementClass.thy
View File

@ -39,10 +39,10 @@ text\<open>The type @{type "DOMString"} is a type synonym for @{type "string"},
type_synonym attr_key = DOMString
type_synonym attr_value = DOMString
type_synonym attrs = "(attr_key, attr_value) fmap"
type_synonym tag_type = DOMString
type_synonym tag_name = DOMString
record ('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr) RElement = RNode +
nothing :: unit
tag_type :: tag_type
tag_name :: tag_name
child_nodes :: "('node_ptr, 'element_ptr, 'character_data_ptr) node_ptr list"
attrs :: attrs
shadow_root_opt :: "'shadow_root_ptr shadow_root_ptr option"
@ -210,9 +210,9 @@ lemma get_elment_ptr_simp2 [simp]:
by(auto simp add: get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)
abbreviation "create_element_obj tag_type_arg child_nodes_arg attrs_arg shadow_root_opt_arg
abbreviation "create_element_obj tag_name_arg child_nodes_arg attrs_arg shadow_root_opt_arg
\<equiv> \<lparr> RObject.nothing = (), RNode.nothing = (), RElement.nothing = (),
tag_type = tag_type_arg, Element.child_nodes = child_nodes_arg, attrs = attrs_arg,
tag_name = tag_name_arg, Element.child_nodes = child_nodes_arg, attrs = attrs_arg,
shadow_root_opt = shadow_root_opt_arg, \<dots> = None \<rparr>"
definition new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t :: "(_) heap \<Rightarrow> ((_) element_ptr \<times> (_) heap)"

30
Core_DOM/Core_SC_DOM/safely_composable/Core_DOM_Heap_WF.thy
View File

@ -5698,12 +5698,12 @@ locale l_create_element_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub
get_disconnected_nodes get_disconnected_nodes_locs
heap_is_wellformed parent_child_rel +
l_new_element_get_disconnected_nodes get_disconnected_nodes get_disconnected_nodes_locs +
l_set_tag_type_get_disconnected_nodes type_wf set_tag_type set_tag_type_locs
l_set_tag_name_get_disconnected_nodes type_wf set_tag_name set_tag_name_locs
get_disconnected_nodes get_disconnected_nodes_locs +
l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes
set_disconnected_nodes_locs set_tag_type set_tag_type_locs type_wf create_element known_ptr +
set_disconnected_nodes_locs set_tag_name set_tag_name_locs type_wf create_element known_ptr +
l_new_element_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs +
l_set_tag_type_get_child_nodes type_wf set_tag_type set_tag_type_locs known_ptr
l_set_tag_name_get_child_nodes type_wf set_tag_name set_tag_name_locs known_ptr
get_child_nodes get_child_nodes_locs +
l_set_disconnected_nodes_get_child_nodes set_disconnected_nodes set_disconnected_nodes_locs
get_child_nodes get_child_nodes_locs +
@ -5721,8 +5721,8 @@ locale l_create_element_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub
and get_disconnected_nodes_locs :: "(_) document_ptr \<Rightarrow> ((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
and heap_is_wellformed :: "(_) heap \<Rightarrow> bool"
and parent_child_rel :: "(_) heap \<Rightarrow> ((_) object_ptr \<times> (_) object_ptr) set"
and set_tag_type :: "(_) element_ptr \<Rightarrow> char list \<Rightarrow> ((_) heap, exception, unit) prog"
and set_tag_type_locs :: "(_) element_ptr \<Rightarrow> ((_) heap, exception, unit) prog set"
and set_tag_name :: "(_) element_ptr \<Rightarrow> char list \<Rightarrow> ((_) heap, exception, unit) prog"
and set_tag_name_locs :: "(_) element_ptr \<Rightarrow> ((_) heap, exception, unit) prog set"
and set_disconnected_nodes :: "(_) document_ptr \<Rightarrow> (_) node_ptr list \<Rightarrow> ((_) heap, exception, unit) prog"
and set_disconnected_nodes_locs :: "(_) document_ptr \<Rightarrow> ((_) heap, exception, unit) prog set"
and create_element :: "(_) document_ptr \<Rightarrow> char list \<Rightarrow> ((_) heap, exception, (_) element_ptr) prog"
@ -5737,7 +5737,7 @@ proof -
obtain new_element_ptr h2 h3 disc_nodes_h3 where
new_element_ptr: "h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr" and
h2: "h \<turnstile> new_element \<rightarrow>\<^sub>h h2" and
h3: "h2 \<turnstile> set_tag_type new_element_ptr tag \<rightarrow>\<^sub>h h3" and
h3: "h2 \<turnstile> set_tag_name new_element_ptr tag \<rightarrow>\<^sub>h h3" and
disc_nodes_h3: "h3 \<turnstile> get_disconnected_nodes document_ptr \<rightarrow>\<^sub>r disc_nodes_h3" and
h': "h3 \<turnstile> set_disconnected_nodes document_ptr (cast new_element_ptr # disc_nodes_h3) \<rightarrow>\<^sub>h h'"
using assms(2)
@ -5774,8 +5774,8 @@ proof -
by(auto simp add: document_ptr_kinds_def)
have object_ptr_kinds_eq_h2: "object_ptr_kinds h3 = object_ptr_kinds h2"
apply(rule writes_small_big[where P="\<lambda>h h'. object_ptr_kinds h' = object_ptr_kinds h", OF set_tag_type_writes h3])
using set_tag_type_pointers_preserved
apply(rule writes_small_big[where P="\<lambda>h h'. object_ptr_kinds h' = object_ptr_kinds h", OF set_tag_name_writes h3])
using set_tag_name_pointers_preserved
by (auto simp add: reflp_def transp_def)
then have document_ptr_kinds_eq_h2: "document_ptr_kinds h3 = document_ptr_kinds h2"
by (auto simp add: document_ptr_kinds_def)
@ -5838,17 +5838,17 @@ proof -
have children_eq_h2:
"\<And>ptr' children. h2 \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children = h3 \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children"
using get_child_nodes_reads set_tag_type_writes h3
using get_child_nodes_reads set_tag_name_writes h3
apply(rule reads_writes_preserved)
by(auto simp add: set_tag_type_get_child_nodes)
by(auto simp add: set_tag_name_get_child_nodes)
then have children_eq2_h2: "\<And>ptr'. |h2 \<turnstile> get_child_nodes ptr'|\<^sub>r = |h3 \<turnstile> get_child_nodes ptr'|\<^sub>r"
using select_result_eq by force
have disconnected_nodes_eq_h2:
"\<And>doc_ptr disc_nodes. h2 \<turnstile> get_disconnected_nodes doc_ptr \<rightarrow>\<^sub>r disc_nodes
= h3 \<turnstile> get_disconnected_nodes doc_ptr \<rightarrow>\<^sub>r disc_nodes"
using get_disconnected_nodes_reads set_tag_type_writes h3
using get_disconnected_nodes_reads set_tag_name_writes h3
apply(rule reads_writes_preserved)
by(auto simp add: set_tag_type_get_disconnected_nodes)
by(auto simp add: set_tag_name_get_disconnected_nodes)
then have disconnected_nodes_eq2_h2:
"\<And>doc_ptr. |h2 \<turnstile> get_disconnected_nodes doc_ptr|\<^sub>r = |h3 \<turnstile> get_disconnected_nodes doc_ptr|\<^sub>r"
using select_result_eq by force
@ -5856,8 +5856,8 @@ proof -
have "type_wf h2"
using \<open>type_wf h\<close> new_element_types_preserved h2 by blast
then have "type_wf h3"
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF set_tag_type_writes h3]
using set_tag_type_types_preserved
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF set_tag_name_writes h3]
using set_tag_name_types_preserved
by(auto simp add: reflp_def transp_def)
then show "type_wf h'"
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF set_disconnected_nodes_writes h']
@ -6072,7 +6072,7 @@ end
interpretation i_create_element_wf?: l_create_element_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M known_ptr known_ptrs type_wf
get_child_nodes get_child_nodes_locs get_disconnected_nodes
get_disconnected_nodes_locs heap_is_wellformed parent_child_rel
set_tag_type set_tag_type_locs
set_tag_name set_tag_name_locs
set_disconnected_nodes set_disconnected_nodes_locs create_element
using instances
by(auto simp add: l_create_element_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def)

8
Core_DOM/Core_SC_DOM/safely_composable/classes/ElementClass.thy
View File

@ -39,10 +39,10 @@ text\<open>The type @{type "DOMString"} is a type synonym for @{type "string"},
type_synonym attr_key = DOMString
type_synonym attr_value = DOMString
type_synonym attrs = "(attr_key, attr_value) fmap"
type_synonym tag_type = DOMString
type_synonym tag_name = DOMString
record ('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr) RElement = RNode +
nothing :: unit
tag_type :: tag_type
tag_name :: tag_name
child_nodes :: "('node_ptr, 'element_ptr, 'character_data_ptr) node_ptr list"
attrs :: attrs
shadow_root_opt :: "'shadow_root_ptr shadow_root_ptr option"
@ -210,9 +210,9 @@ lemma get_elment_ptr_simp2 [simp]:
by(auto simp add: get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)
abbreviation "create_element_obj tag_type_arg child_nodes_arg attrs_arg shadow_root_opt_arg
abbreviation "create_element_obj tag_name_arg child_nodes_arg attrs_arg shadow_root_opt_arg
\<equiv> \<lparr> RObject.nothing = (), RNode.nothing = (), RElement.nothing = (),
tag_type = tag_type_arg, Element.child_nodes = child_nodes_arg, attrs = attrs_arg,
tag_name = tag_name_arg, Element.child_nodes = child_nodes_arg, attrs = attrs_arg,
shadow_root_opt = shadow_root_opt_arg, \<dots> = None \<rparr>"
definition new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t :: "(_) heap \<Rightarrow> ((_) element_ptr \<times> (_) heap)"