forked from afp-mirror/Core_DOM
Limit auto to first sub-goal ...
This commit is contained in:
parent
9a96718e9f
commit
989597fc9d
|
|
@ -633,7 +633,7 @@ proof -
|
|||
by(auto simp add: known_ptr_impl known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)
|
||||
then show ?thesis
|
||||
using assms
|
||||
apply(auto simp add: set_child_nodes_def a_set_child_nodes_tups_def set_child_nodes\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def split: option.splits)
|
||||
apply(auto simp add: set_child_nodes_def a_set_child_nodes_tups_def set_child_nodes\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def split: option.splits)[1]
|
||||
by (simp add: DocumentMonad.put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ok local.type_wf_impl)
|
||||
qed
|
||||
|
||||
|
|
@ -650,7 +650,7 @@ proof -
|
|||
by(auto simp add: known_ptr_impl known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)
|
||||
then show ?thesis
|
||||
using assms
|
||||
apply(auto simp add: set_child_nodes_def a_set_child_nodes_tups_def set_child_nodes\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def split: option.splits)
|
||||
apply(auto simp add: set_child_nodes_def a_set_child_nodes_tups_def set_child_nodes\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def split: option.splits)[1]
|
||||
by (simp add: DocumentMonad.put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ok local.type_wf_impl)
|
||||
qed
|
||||
|
||||
|
|
@ -670,9 +670,11 @@ proof -
|
|||
using assms
|
||||
apply(auto simp add: set_child_nodes_def a_set_child_nodes_tups_def set_child_nodes\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def)
|
||||
apply(split invoke_splits, rule conjI)+
|
||||
apply(auto simp add: is_element_ptr_kind\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def set_child_nodes\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def split: option.splits)
|
||||
using assms(3) l_put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_lemmas.put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ok l_put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_lemmas_axioms local.type_wf_impl
|
||||
by fastforce
|
||||
apply(auto simp add: is_element_ptr_kind\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def set_child_nodes\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def split: option.splits)[1]
|
||||
apply(auto simp add: is_element_ptr_kind\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def set_child_nodes\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def split: option.splits)[1]
|
||||
apply (simp add: local.type_wf_impl put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ok)
|
||||
apply(auto simp add: is_element_ptr_kind\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def set_child_nodes\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def split: option.splits)[1]
|
||||
by(auto simp add: is_element_ptr_kind\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def set_child_nodes\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def split: option.splits)[1]
|
||||
qed
|
||||
end
|
||||
|
||||
|
|
@ -2417,7 +2419,7 @@ lemma remove_child_child_in_heap:
|
|||
assumes "h \<turnstile> remove_child ptr' child \<rightarrow>\<^sub>h h'"
|
||||
shows "child |\<in>| node_ptr_kinds h"
|
||||
using assms
|
||||
apply(auto simp add: remove_child_def elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_child_nodes_pure, rotated] split: if_splits)
|
||||
apply(auto simp add: remove_child_def elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_child_nodes_pure, rotated] split: if_splits)[1]
|
||||
by (meson is_OK_returns_result_I local.get_owner_document_ptr_in_heap node_ptr_kinds_commutes)
|
||||
|
||||
|
||||
|
|
@ -3040,8 +3042,8 @@ lemma insert_before_list_in_set: "x \<in> set (insert_before_list v ref xs) \<lo
|
|||
by(auto)
|
||||
|
||||
lemma insert_before_list_distinct: "x \<notin> set xs \<Longrightarrow> distinct xs \<Longrightarrow> distinct (insert_before_list x ref xs)"
|
||||
by (induct x ref xs rule: insert_before_list.induct)
|
||||
(auto simp add: insert_before_list_in_set)
|
||||
apply(induct x ref xs rule: insert_before_list.induct)
|
||||
by(auto simp add: insert_before_list_in_set)
|
||||
|
||||
lemma insert_before_list_subset: "set xs \<subseteq> set (insert_before_list x ref xs)"
|
||||
apply(induct x ref xs rule: insert_before_list.induct)
|
||||
|
|
@ -3081,7 +3083,7 @@ lemma insert_before_ptr_in_heap:
|
|||
assumes "h \<turnstile> ok (insert_before ptr node reference_child)"
|
||||
shows "ptr |\<in>| object_ptr_kinds h"
|
||||
using assms
|
||||
apply(auto simp add: insert_before_def elim!: bind_is_OK_E)
|
||||
apply(auto simp add: insert_before_def elim!: bind_is_OK_E)[1]
|
||||
by (metis (mono_tags, lifting) ensure_pre_insertion_validity_pure is_OK_returns_result_I local.get_owner_document_ptr_in_heap next_sibling_pure pure_returns_heap_eq return_returns_heap)
|
||||
|
||||
lemma insert_before_child_in_heap:
|
||||
|
|
@ -3295,7 +3297,7 @@ lemma create_element_known_ptr:
|
|||
proof -
|
||||
have "is_element_ptr new_element_ptr"
|
||||
using assms
|
||||
apply(auto simp add: create_element_def elim!: bind_returns_result_E)
|
||||
apply(auto simp add: create_element_def elim!: bind_returns_result_E)[1]
|
||||
using new_element_is_element_ptr
|
||||
by blast
|
||||
then show ?thesis
|
||||
|
|
@ -3402,7 +3404,7 @@ lemma create_character_data_known_ptr:
|
|||
proof -
|
||||
have "is_character_data_ptr new_character_data_ptr"
|
||||
using assms
|
||||
apply(auto simp add: create_character_data_def elim!: bind_returns_result_E)
|
||||
apply(auto simp add: create_character_data_def elim!: bind_returns_result_E)[1]
|
||||
using new_character_data_is_character_data_ptr
|
||||
by blast
|
||||
then show ?thesis
|
||||
|
|
|
|||
|
|
@ -300,7 +300,7 @@ lemma type_wf_put_ptr_not_in_heap_E:
|
|||
shows "type_wf h"
|
||||
using assms
|
||||
apply(auto simp add: type_wf_defs elim!: NodeMonad.type_wf_put_ptr_not_in_heap_E
|
||||
split: option.splits if_splits)
|
||||
split: option.splits if_splits)[1]
|
||||
using assms(2) node_ptr_kinds_commutes by blast
|
||||
|
||||
lemma type_wf_put_ptr_in_heap_E:
|
||||
|
|
|
|||
|
|
@ -93,7 +93,7 @@ definition
|
|||
where
|
||||
"returns_result_heap h p r h' \<longleftrightarrow> h \<turnstile> p \<rightarrow>\<^sub>r r \<and> h \<turnstile> p \<rightarrow>\<^sub>h h'"
|
||||
|
||||
lemma [code]: "returns_result_heap h p r h' \<longleftrightarrow> (case h \<turnstile> p of Inr (r', h'') \<Rightarrow> r = r' \<and> h' = h'' | Inl _ \<Rightarrow> False)"
|
||||
lemma return_result_heap_code [code]: "returns_result_heap h p r h' \<longleftrightarrow> (case h \<turnstile> p of Inr (r', h'') \<Rightarrow> r = r' \<and> h' = h'' | Inl _ \<Rightarrow> False)"
|
||||
by(auto simp add: returns_result_heap_def returns_result_def returns_heap_def split: sum.splits)
|
||||
|
||||
fun select_result_heap ("|(_)|\<^sub>r\<^sub>h")
|
||||
|
|
@ -731,7 +731,7 @@ definition preserved :: "('heap, 'e, 'result) prog \<Rightarrow> 'heap \<Rightar
|
|||
"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(auto simp add: preserved_def)[1]
|
||||
apply (meson is_OK_returns_result_E is_OK_returns_result_I)+
|
||||
done
|
||||
|
||||
|
|
|
|||
|
|
@ -56,7 +56,7 @@ definition a_owner_document_valid :: "(_) heap \<Rightarrow> bool"
|
|||
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)
|
||||
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)[1]
|
||||
proof -
|
||||
fix x
|
||||
assume 1: " \<forall>node_ptr\<in>fset (node_ptr_kinds h).
|
||||
|
|
@ -2681,7 +2681,7 @@ lemma get_owner_document_owner_document_in_heap:
|
|||
assumes "h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document"
|
||||
shows "owner_document |\<in>| document_ptr_kinds h"
|
||||
using assms
|
||||
apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def)
|
||||
apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def)[1]
|
||||
apply(split invoke_split_asm)+
|
||||
proof -
|
||||
assume "h \<turnstile> invoke [] ptr () \<rightarrow>\<^sub>r owner_document"
|
||||
|
|
@ -2743,9 +2743,10 @@ next
|
|||
then have "some_owner_document \<in> set candidates"
|
||||
apply(rule filter_M_in_result_if_ok)
|
||||
using \<open>some_owner_document |\<in>| document_ptr_kinds h\<close> \<open>root \<in> cast ` set |h \<turnstile> get_disconnected_nodes some_owner_document|\<^sub>r\<close>
|
||||
apply(auto intro!: bind_pure_I bind_pure_returns_result_I)
|
||||
by (simp add: "1" local.get_disconnected_nodes_ok)
|
||||
|
||||
apply(auto intro!: bind_pure_I bind_pure_returns_result_I)[1]
|
||||
apply (simp add: \<open>some_owner_document |\<in>| document_ptr_kinds h\<close>)
|
||||
using "1" \<open>root \<in> 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 ` set |h \<turnstile> get_disconnected_nodes some_owner_document|\<^sub>r\<close> \<open>some_owner_document |\<in>| document_ptr_kinds h\<close>
|
||||
local.get_disconnected_nodes_ok by auto
|
||||
then have "candidates \<noteq> []"
|
||||
by auto
|
||||
then have "owner_document \<in> set candidates"
|
||||
|
|
@ -2833,17 +2834,28 @@ proof -
|
|||
using assms(2) assms(4) local.known_ptrs_known_ptr
|
||||
by blast
|
||||
then show ?thesis
|
||||
apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def)
|
||||
apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def)[1]
|
||||
apply(split invoke_splits, (rule conjI | rule impI)+)+
|
||||
apply(auto simp add: known_ptr_impl)[1]
|
||||
using NodeClass.a_known_ptr_def known_ptr_not_character_data_ptr known_ptr_not_document_ptr known_ptr_not_element_ptr apply blast
|
||||
using NodeClass.a_known_ptr_def known_ptr_not_character_data_ptr known_ptr_not_document_ptr known_ptr_not_element_ptr
|
||||
apply blast
|
||||
using assms(4)
|
||||
apply(auto simp add: a_get_owner_document\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def intro!: bind_is_OK_pure_I)
|
||||
apply(auto simp add: a_get_owner_document\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def intro!: bind_is_OK_pure_I)[1]
|
||||
apply (metis (no_types, lifting) document_ptr_casts_commute3 document_ptr_kinds_commutes is_document_ptr_kind_none option.case_eq_if)
|
||||
using assms(4)
|
||||
apply(auto simp add: a_get_owner_document\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def intro!: bind_is_OK_pure_I)[1]
|
||||
apply (metis (no_types, lifting) assms(1) assms(2) assms(3) is_node_ptr_kind_none local.get_root_node_ok node_ptr_casts_commute3 option.case_eq_if)
|
||||
apply(auto split: option.splits intro!: bind_is_OK_pure_I filter_M_pure_I bind_pure_I filter_M_is_OK_I)
|
||||
using assms(3) local.get_disconnected_nodes_ok apply blast
|
||||
using assms(4)
|
||||
apply(auto simp add: a_get_owner_document\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def intro!: bind_is_OK_pure_I)[1]
|
||||
apply(auto split: option.splits intro!: bind_is_OK_pure_I filter_M_pure_I bind_pure_I filter_M_is_OK_I)[1]
|
||||
using assms(3) local.get_disconnected_nodes_ok
|
||||
apply blast
|
||||
apply (simp add: assms(1) assms(2) assms(3) local.get_root_node_ok)
|
||||
using assms(4)
|
||||
apply(auto simp add: a_get_owner_document\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def intro!: bind_is_OK_pure_I)[1]
|
||||
apply(auto split: option.splits intro!: bind_is_OK_pure_I filter_M_pure_I bind_pure_I filter_M_is_OK_I)[1]
|
||||
apply (simp add: assms(1) assms(2) assms(3) local.get_root_node_ok)[1]
|
||||
apply(auto split: option.splits intro!: bind_is_OK_pure_I filter_M_pure_I bind_pure_I filter_M_is_OK_I)[1]
|
||||
using assms(3) local.get_disconnected_nodes_ok by blast
|
||||
qed
|
||||
|
||||
|
|
@ -2880,11 +2892,11 @@ proof -
|
|||
|
||||
then have "h \<turnstile> a_get_owner_document\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r document_ptr () \<rightarrow>\<^sub>r owner_document \<longleftrightarrow> h \<turnstile> a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r child () \<rightarrow>\<^sub>r owner_document"
|
||||
using document_ptr \<open>h \<turnstile> get_root_node (cast child) \<rightarrow>\<^sub>r root\<close>[simplified \<open>root = cast document_ptr\<close> document_ptr]
|
||||
apply(auto simp add: a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def a_get_owner_document\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def elim!: bind_returns_result_E2 dest!: bind_returns_result_E3[rotated, OF \<open>h \<turnstile> get_root_node (cast child) \<rightarrow>\<^sub>r root\<close>[simplified \<open>root = cast document_ptr\<close> document_ptr], rotated] intro!: bind_pure_returns_result_I filter_M_pure_I bind_pure_I split: if_splits option.splits)
|
||||
apply(auto simp add: a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def a_get_owner_document\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def elim!: bind_returns_result_E2 dest!: bind_returns_result_E3[rotated, OF \<open>h \<turnstile> get_root_node (cast child) \<rightarrow>\<^sub>r root\<close>[simplified \<open>root = cast document_ptr\<close> document_ptr], rotated] intro!: bind_pure_returns_result_I filter_M_pure_I bind_pure_I split: if_splits option.splits)[1]
|
||||
using \<open>ptr |\<in>| object_ptr_kinds h\<close> document_ptr_kinds_commutes by blast
|
||||
then show ?thesis
|
||||
using \<open>known_ptr ptr\<close>
|
||||
apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def known_ptr_impl)
|
||||
apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def known_ptr_impl)[1]
|
||||
apply(split invoke_splits, ((rule conjI | rule impI)+)?)+
|
||||
apply(drule(1) known_ptr_not_document_ptr[folded known_ptr_impl])
|
||||
apply(drule(1) known_ptr_not_character_data_ptr)
|
||||
|
|
@ -2910,21 +2922,36 @@ proof -
|
|||
apply(drule(1) known_ptr_not_element_ptr)
|
||||
apply(simp add: NodeClass.known_ptr_defs)
|
||||
using \<open>cast child |\<in>| object_ptr_kinds h\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close> False
|
||||
apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )
|
||||
apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )[1]
|
||||
using \<open>cast child |\<in>| object_ptr_kinds h\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close> False
|
||||
apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )[1]
|
||||
using \<open>cast child |\<in>| object_ptr_kinds h\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close> False
|
||||
apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )[1]
|
||||
using \<open>cast child |\<in>| object_ptr_kinds h\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close> False
|
||||
apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )[1]
|
||||
apply(split invoke_splits, ((rule conjI | rule impI)+)?)+
|
||||
apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )
|
||||
by (meson invoke_empty is_OK_returns_result_I)
|
||||
apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )[1]
|
||||
apply (meson invoke_empty is_OK_returns_result_I)
|
||||
apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )[1]
|
||||
apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )[1]
|
||||
by(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )[1]
|
||||
qed
|
||||
then show ?thesis
|
||||
using \<open>known_ptr (cast child)\<close>
|
||||
apply(auto simp add: get_owner_document_def[of "cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r child"] a_get_owner_document_tups_def known_ptr_impl)
|
||||
apply(auto simp add: get_owner_document_def[of "cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r child"] a_get_owner_document_tups_def known_ptr_impl)[1]
|
||||
apply(split invoke_splits, ((rule conjI | rule impI)+)?)+
|
||||
apply(drule(1) known_ptr_not_document_ptr[folded known_ptr_impl])
|
||||
apply(drule(1) known_ptr_not_character_data_ptr)
|
||||
apply(drule(1) known_ptr_not_element_ptr)
|
||||
apply(simp add: NodeClass.known_ptr_defs)
|
||||
using \<open>cast child |\<in>| object_ptr_kinds h\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close>
|
||||
apply(auto intro!: bind_pure_returns_result_I split: option.splits)
|
||||
apply(auto intro!: bind_pure_returns_result_I split: option.splits)[1]
|
||||
using \<open>cast child |\<in>| object_ptr_kinds h\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close>
|
||||
apply(auto intro!: bind_pure_returns_result_I split: option.splits)[1]
|
||||
using \<open>cast child |\<in>| object_ptr_kinds h\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close>
|
||||
apply(auto intro!: bind_pure_returns_result_I split: option.splits)[1]
|
||||
using \<open>cast child |\<in>| object_ptr_kinds h\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close>
|
||||
apply(auto intro!: bind_pure_returns_result_I split: option.splits)[1]
|
||||
by (smt \<open>cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r child |\<in>| object_ptr_kinds h\<close> cast_document_ptr_not_node_ptr(1) comp_apply invoke_empty invoke_not invoke_returns_result is_OK_returns_result_I node_ptr_casts_commute2 option.sel)
|
||||
qed
|
||||
|
||||
|
|
@ -2963,7 +2990,7 @@ lemma get_owner_document_wf_is_l_get_owner_document_wf [instances]:
|
|||
"l_get_owner_document_wf heap_is_wellformed type_wf known_ptr known_ptrs get_disconnected_nodes
|
||||
get_owner_document get_parent"
|
||||
using known_ptrs_is_l_known_ptrs
|
||||
apply(auto simp add: l_get_owner_document_wf_def l_get_owner_document_wf_axioms_def)
|
||||
apply(auto simp add: l_get_owner_document_wf_def l_get_owner_document_wf_axioms_def)[1]
|
||||
using get_owner_document_disconnected_nodes apply fast
|
||||
using in_disconnected_nodes_no_parent apply fast
|
||||
using get_owner_document_owner_document_in_heap apply fast
|
||||
|
|
@ -2998,7 +3025,7 @@ proof -
|
|||
by(auto simp add: get_root_node_def get_ancestors_def elim!: bind_returns_result_E2 split: option.splits)
|
||||
then have ?thesis
|
||||
using \<open>is_document_ptr_kind ptr\<close> \<open>known_ptr ptr\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close>
|
||||
apply(auto simp add: known_ptr_impl get_owner_document_def a_get_owner_document_tups_def)
|
||||
apply(auto simp add: known_ptr_impl get_owner_document_def a_get_owner_document_tups_def)[1]
|
||||
apply(split invoke_splits, (rule conjI | rule impI)+)+
|
||||
apply(drule(1) known_ptr_not_document_ptr[folded known_ptr_impl])
|
||||
apply(drule(1) known_ptr_not_character_data_ptr)
|
||||
|
|
@ -3046,7 +3073,7 @@ proof -
|
|||
then
|
||||
have "ptr = root"
|
||||
using assms(4)
|
||||
apply(auto simp add: get_root_node_def elim!: bind_returns_result_E2)
|
||||
apply(auto simp add: get_root_node_def elim!: bind_returns_result_E2)[1]
|
||||
by (metis document_ptr_casts_commute3 last_ConsL local.get_ancestors_not_node node_ptr_no_document_ptr_cast)
|
||||
then show ?thesis
|
||||
by auto
|
||||
|
|
@ -3062,7 +3089,7 @@ proof -
|
|||
assume "h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document"
|
||||
then have "h \<turnstile> local.a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r node_ptr () \<rightarrow>\<^sub>r owner_document"
|
||||
using node_ptr
|
||||
apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def)
|
||||
apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def)[1]
|
||||
apply(split invoke_splits)+
|
||||
apply (meson invoke_empty is_OK_returns_result_I)
|
||||
by(auto elim!: bind_returns_result_E2 split: option.splits)
|
||||
|
|
@ -3934,7 +3961,7 @@ proof -
|
|||
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF remove_child_writes assms(2)]
|
||||
using set_child_nodes_types_preserved set_disconnected_nodes_types_preserved type_wf
|
||||
unfolding remove_child_locs_def
|
||||
apply(auto simp add: reflp_def transp_def)
|
||||
apply(auto simp add: reflp_def transp_def)[1]
|
||||
by blast
|
||||
ultimately show ?thesis
|
||||
using remove_child_removes_parent remove_child_heap_is_wellformed_preserved child_parent_dual
|
||||
|
|
@ -5970,7 +5997,7 @@ proof -
|
|||
(if cast node \<in> set ancestors then error HierarchyRequestError else return ())
|
||||
} \<rightarrow>\<^sub>r ()"
|
||||
using assms(6)
|
||||
apply(auto intro!: bind_pure_returns_result_I)
|
||||
apply(auto intro!: bind_pure_returns_result_I)[1]
|
||||
using assms(1) assms(2) assms(3) assms(7) local.get_ancestors_ok local.get_parent_parent_in_heap by auto
|
||||
|
||||
moreover have "h \<turnstile> do {
|
||||
|
|
@ -5999,13 +6026,26 @@ proof -
|
|||
ultimately show ?thesis
|
||||
unfolding a_ensure_pre_insertion_validity_def
|
||||
apply(intro bind_is_OK_pure_I)
|
||||
apply(auto)
|
||||
using assms(1) assms(2) assms(3) assms(7) local.get_ancestors_ok local.get_parent_parent_in_heap apply blast
|
||||
|
||||
using assms(6) apply auto[1]
|
||||
apply (smt assms(7) bind_returns_heap_E2 is_OK_returns_heap_E local.get_parent_pure pure_def pure_returns_heap_eq return_pure returns_result_eq)
|
||||
apply auto[1]
|
||||
apply auto[1]
|
||||
apply auto[1]
|
||||
using assms(1) assms(2) assms(3) assms(7) local.get_ancestors_ok local.get_parent_parent_in_heap
|
||||
apply blast
|
||||
apply auto[1]
|
||||
apply auto[1]
|
||||
using assms(6)
|
||||
apply auto[1]
|
||||
using assms(1) assms(2) assms(3) assms(7) local.get_ancestors_ok local.get_parent_parent_in_heap
|
||||
apply auto[1]
|
||||
apply (smt bind_returns_heap_E is_OK_returns_heap_E local.get_parent_pure pure_def
|
||||
pure_returns_heap_eq return_returns_heap returns_result_eq)
|
||||
apply(blast)
|
||||
using local.get_child_nodes_pure
|
||||
apply blast
|
||||
apply (meson assms(7) is_OK_returns_result_I local.get_parent_child_dual)
|
||||
by (simp add: assms(8) returns_result_eq)
|
||||
apply (simp)
|
||||
apply (smt assms(5) assms(8) is_OK_returns_result_I returns_result_eq)
|
||||
by(auto)
|
||||
qed
|
||||
end
|
||||
|
||||
|
|
@ -6187,7 +6227,7 @@ proof -
|
|||
by auto
|
||||
|
||||
have "h \<turnstile> ok (case parent_opt of Some parent \<Rightarrow> remove_child parent child | None \<Rightarrow> return ())"
|
||||
apply(auto split: option.splits)
|
||||
apply(auto split: option.splits)[1]
|
||||
using remove_child_ok
|
||||
by (metis assms(1) assms(2) assms(3) local.get_parent_child_dual parent_opt)
|
||||
then
|
||||
|
|
@ -6391,7 +6431,7 @@ proof -
|
|||
have "h \<turnstile> ok (if Some node = Some ref
|
||||
then a_next_sibling node
|
||||
else return (Some ref))" (is "h \<turnstile> ok ?P")
|
||||
apply(auto split: if_splits)
|
||||
apply(auto split: if_splits)[1]
|
||||
using assms(1) assms(2) assms(3) assms(5) next_sibling_ok by blast
|
||||
|
||||
then obtain reference_child where
|
||||
|
|
@ -6649,7 +6689,7 @@ interpretation i_append_child_wf?: l_append_child_wf\<^sub>C\<^sub>o\<^sub>r\<^s
|
|||
by(auto simp add: l_append_child_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
|
||||
|
||||
lemma append_child_wf_is_l_append_child_wf [instances]: "l_append_child_wf type_wf known_ptr known_ptrs append_child heap_is_wellformed"
|
||||
apply(auto simp add: l_append_child_wf_def l_append_child_wf_axioms_def instances)
|
||||
apply(auto simp add: l_append_child_wf_def l_append_child_wf_axioms_def instances)[1]
|
||||
using append_child_heap_is_wellformed_preserved by fast+
|
||||
|
||||
|
||||
|
|
@ -6707,7 +6747,7 @@ proof -
|
|||
elim!: bind_returns_heap_E
|
||||
bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated] )
|
||||
then have "h \<turnstile> create_element document_ptr tag \<rightarrow>\<^sub>r new_element_ptr"
|
||||
apply(auto simp add: create_element_def intro!: bind_returns_result_I)
|
||||
apply(auto simp add: create_element_def intro!: bind_returns_result_I)[1]
|
||||
apply (metis is_OK_returns_heap_I is_OK_returns_result_E old.unit.exhaust)
|
||||
apply (metis is_OK_returns_heap_E is_OK_returns_result_I local.get_disconnected_nodes_pure pure_returns_heap_eq)
|
||||
by (metis is_OK_returns_heap_I is_OK_returns_result_E old.unit.exhaust)
|
||||
|
|
|
|||
|
|
@ -633,7 +633,7 @@ proof -
|
|||
by(auto simp add: known_ptr_impl known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)
|
||||
then show ?thesis
|
||||
using assms
|
||||
apply(auto simp add: set_child_nodes_def a_set_child_nodes_tups_def set_child_nodes\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def split: option.splits)
|
||||
apply(auto simp add: set_child_nodes_def a_set_child_nodes_tups_def set_child_nodes\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def split: option.splits)[1]
|
||||
by (simp add: DocumentMonad.put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ok local.type_wf_impl)
|
||||
qed
|
||||
|
||||
|
|
@ -650,7 +650,7 @@ proof -
|
|||
by(auto simp add: known_ptr_impl known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)
|
||||
then show ?thesis
|
||||
using assms
|
||||
apply(auto simp add: set_child_nodes_def a_set_child_nodes_tups_def set_child_nodes\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def split: option.splits)
|
||||
apply(auto simp add: set_child_nodes_def a_set_child_nodes_tups_def set_child_nodes\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def split: option.splits)[1]
|
||||
by (simp add: DocumentMonad.put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ok local.type_wf_impl)
|
||||
qed
|
||||
|
||||
|
|
@ -670,9 +670,11 @@ proof -
|
|||
using assms
|
||||
apply(auto simp add: set_child_nodes_def a_set_child_nodes_tups_def set_child_nodes\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def)
|
||||
apply(split invoke_splits, rule conjI)+
|
||||
apply(auto simp add: is_element_ptr_kind\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def set_child_nodes\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def split: option.splits)
|
||||
using assms(3) l_put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_lemmas.put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ok l_put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_lemmas_axioms local.type_wf_impl
|
||||
by fastforce
|
||||
apply(auto simp add: is_element_ptr_kind\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def set_child_nodes\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def split: option.splits)[1]
|
||||
apply(auto simp add: is_element_ptr_kind\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def set_child_nodes\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def split: option.splits)[1]
|
||||
apply (simp add: local.type_wf_impl put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ok)
|
||||
apply(auto simp add: is_element_ptr_kind\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def set_child_nodes\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def split: option.splits)[1]
|
||||
by(auto simp add: is_element_ptr_kind\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def set_child_nodes\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def split: option.splits)[1]
|
||||
qed
|
||||
end
|
||||
|
||||
|
|
@ -2417,7 +2419,7 @@ lemma remove_child_child_in_heap:
|
|||
assumes "h \<turnstile> remove_child ptr' child \<rightarrow>\<^sub>h h'"
|
||||
shows "child |\<in>| node_ptr_kinds h"
|
||||
using assms
|
||||
apply(auto simp add: remove_child_def elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_child_nodes_pure, rotated] split: if_splits)
|
||||
apply(auto simp add: remove_child_def elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_child_nodes_pure, rotated] split: if_splits)[1]
|
||||
by (meson is_OK_returns_result_I local.get_owner_document_ptr_in_heap node_ptr_kinds_commutes)
|
||||
|
||||
|
||||
|
|
@ -3040,8 +3042,8 @@ lemma insert_before_list_in_set: "x \<in> set (insert_before_list v ref xs) \<lo
|
|||
by(auto)
|
||||
|
||||
lemma insert_before_list_distinct: "x \<notin> set xs \<Longrightarrow> distinct xs \<Longrightarrow> distinct (insert_before_list x ref xs)"
|
||||
by (induct x ref xs rule: insert_before_list.induct)
|
||||
(auto simp add: insert_before_list_in_set)
|
||||
apply(induct x ref xs rule: insert_before_list.induct)
|
||||
by(auto simp add: insert_before_list_in_set)
|
||||
|
||||
lemma insert_before_list_subset: "set xs \<subseteq> set (insert_before_list x ref xs)"
|
||||
apply(induct x ref xs rule: insert_before_list.induct)
|
||||
|
|
@ -3081,7 +3083,7 @@ lemma insert_before_ptr_in_heap:
|
|||
assumes "h \<turnstile> ok (insert_before ptr node reference_child)"
|
||||
shows "ptr |\<in>| object_ptr_kinds h"
|
||||
using assms
|
||||
apply(auto simp add: insert_before_def elim!: bind_is_OK_E)
|
||||
apply(auto simp add: insert_before_def elim!: bind_is_OK_E)[1]
|
||||
by (metis (mono_tags, lifting) ensure_pre_insertion_validity_pure is_OK_returns_result_I local.get_owner_document_ptr_in_heap next_sibling_pure pure_returns_heap_eq return_returns_heap)
|
||||
|
||||
lemma insert_before_child_in_heap:
|
||||
|
|
@ -3295,7 +3297,7 @@ lemma create_element_known_ptr:
|
|||
proof -
|
||||
have "is_element_ptr new_element_ptr"
|
||||
using assms
|
||||
apply(auto simp add: create_element_def elim!: bind_returns_result_E)
|
||||
apply(auto simp add: create_element_def elim!: bind_returns_result_E)[1]
|
||||
using new_element_is_element_ptr
|
||||
by blast
|
||||
then show ?thesis
|
||||
|
|
@ -3402,7 +3404,7 @@ lemma create_character_data_known_ptr:
|
|||
proof -
|
||||
have "is_character_data_ptr new_character_data_ptr"
|
||||
using assms
|
||||
apply(auto simp add: create_character_data_def elim!: bind_returns_result_E)
|
||||
apply(auto simp add: create_character_data_def elim!: bind_returns_result_E)[1]
|
||||
using new_character_data_is_character_data_ptr
|
||||
by blast
|
||||
then show ?thesis
|
||||
|
|
|
|||
|
|
@ -300,7 +300,7 @@ lemma type_wf_put_ptr_not_in_heap_E:
|
|||
shows "type_wf h"
|
||||
using assms
|
||||
apply(auto simp add: type_wf_defs elim!: NodeMonad.type_wf_put_ptr_not_in_heap_E
|
||||
split: option.splits if_splits)
|
||||
split: option.splits if_splits)[1]
|
||||
using assms(2) node_ptr_kinds_commutes by blast
|
||||
|
||||
lemma type_wf_put_ptr_in_heap_E:
|
||||
|
|
|
|||
|
|
@ -93,7 +93,7 @@ definition
|
|||
where
|
||||
"returns_result_heap h p r h' \<longleftrightarrow> h \<turnstile> p \<rightarrow>\<^sub>r r \<and> h \<turnstile> p \<rightarrow>\<^sub>h h'"
|
||||
|
||||
lemma [code]: "returns_result_heap h p r h' \<longleftrightarrow> (case h \<turnstile> p of Inr (r', h'') \<Rightarrow> r = r' \<and> h' = h'' | Inl _ \<Rightarrow> False)"
|
||||
lemma return_result_heap_code [code]: "returns_result_heap h p r h' \<longleftrightarrow> (case h \<turnstile> p of Inr (r', h'') \<Rightarrow> r = r' \<and> h' = h'' | Inl _ \<Rightarrow> False)"
|
||||
by(auto simp add: returns_result_heap_def returns_result_def returns_heap_def split: sum.splits)
|
||||
|
||||
fun select_result_heap ("|(_)|\<^sub>r\<^sub>h")
|
||||
|
|
@ -731,7 +731,7 @@ definition preserved :: "('heap, 'e, 'result) prog \<Rightarrow> 'heap \<Rightar
|
|||
"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(auto simp add: preserved_def)[1]
|
||||
apply (meson is_OK_returns_result_E is_OK_returns_result_I)+
|
||||
done
|
||||
|
||||
|
|
|
|||
Reference in New Issue