forked from afp-mirror/Core_DOM
Made various parts work better with the code generator.
This commit is contained in:
parent
834d6a8077
commit
bdd16a015f
|
@ -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)
|
||||
|
@ -3531,35 +3580,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")
|
||||
|
@ -3575,7 +3609,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
|
||||
|
||||
|
@ -4479,29 +4513,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)
|
||||
|
@ -5200,46 +5225,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
|
||||
|
@ -5266,17 +5291,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
|
||||
|
@ -5291,10 +5316,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
|
||||
|
@ -5309,11 +5334,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"
|
||||
|
@ -5322,7 +5347,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
|
||||
|
@ -5348,9 +5373,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
|
||||
|
@ -5360,10 +5385,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
|
||||
|
@ -5396,13 +5421,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
|
||||
|
@ -5413,33 +5438,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)
|
||||
|
@ -5844,7 +5849,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>
|
||||
|
@ -5890,21 +5895,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>
|
||||
|
@ -5973,24 +5969,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)
|
||||
|
@ -6029,27 +6009,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)
|
||||
|
@ -6321,7 +6282,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>
|
||||
|
@ -6368,19 +6329,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>
|
||||
|
@ -6444,25 +6400,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)
|
||||
|
@ -6498,10 +6436,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>
|
||||
|
@ -6610,7 +6546,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)+
|
||||
|
@ -6662,19 +6598,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>
|
||||
|
@ -6743,12 +6673,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>
|
||||
|
|
|
@ -139,8 +139,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 +163,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 +324,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
|
||||
|
|
|
@ -115,7 +115,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 +135,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 +227,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 +314,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
|
||||
|
|
|
@ -131,8 +131,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 +154,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 +290,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
|
||||
|
|
|
@ -89,8 +89,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 +109,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 +175,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
|
||||
|
|
|
@ -134,16 +134,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 +193,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
|
||||
|
|
|
@ -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
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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]
|
||||
|
||||
|
|
|
@ -711,6 +711,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)"
|
||||
|
|
|
@ -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"
|
||||
|
|
Reference in New Issue