From 989597fc9dc56e3b4f8baa0271a18d98fec2950b Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Thu, 16 Apr 2020 12:18:57 +0100 Subject: [PATCH] Limit auto to first sub-goal ... --- .../Core_DOM/common/Core_DOM_Functions.thy | 24 ++-- .../Core_DOM/common/monads/ElementMonad.thy | 2 +- .../common/preliminaries/Heap_Error_Monad.thy | 4 +- .../Core_DOM/standard/Core_DOM_Heap_WF.thy | 106 ++++++++++++------ .../common/Core_DOM_Functions.thy | 24 ++-- .../common/monads/ElementMonad.thy | 2 +- .../common/preliminaries/Heap_Error_Monad.thy | 4 +- 7 files changed, 105 insertions(+), 61 deletions(-) diff --git a/Core_DOM/Core_DOM/common/Core_DOM_Functions.thy b/Core_DOM/Core_DOM/common/Core_DOM_Functions.thy index f279d89..deae67a 100644 --- a/Core_DOM/Core_DOM/common/Core_DOM_Functions.thy +++ b/Core_DOM/Core_DOM/common/Core_DOM_Functions.thy @@ -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 \ remove_child ptr' child \\<^sub>h h'" shows "child |\| 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 \ set (insert_before_list v ref xs) \ set xs \ distinct xs \ 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 \ 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 \ ok (insert_before ptr node reference_child)" shows "ptr |\| 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 diff --git a/Core_DOM/Core_DOM/common/monads/ElementMonad.thy b/Core_DOM/Core_DOM/common/monads/ElementMonad.thy index f4ba05c..2103139 100644 --- a/Core_DOM/Core_DOM/common/monads/ElementMonad.thy +++ b/Core_DOM/Core_DOM/common/monads/ElementMonad.thy @@ -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: diff --git a/Core_DOM/Core_DOM/common/preliminaries/Heap_Error_Monad.thy b/Core_DOM/Core_DOM/common/preliminaries/Heap_Error_Monad.thy index f483031..5a4a0b4 100644 --- a/Core_DOM/Core_DOM/common/preliminaries/Heap_Error_Monad.thy +++ b/Core_DOM/Core_DOM/common/preliminaries/Heap_Error_Monad.thy @@ -93,7 +93,7 @@ definition where "returns_result_heap h p r h' \ h \ p \\<^sub>r r \ h \ p \\<^sub>h h'" -lemma [code]: "returns_result_heap h p r h' \ (case h \ p of Inr (r', h'') \ r = r' \ h' = h'' | Inl _ \ False)" +lemma return_result_heap_code [code]: "returns_result_heap h p r h' \ (case h \ p of Inr (r', h'') \ r = r' \ h' = h'' | Inl _ \ 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 \ 'heap \ (\x. h \ f \\<^sub>r x \ h' \ f \\<^sub>r x)" lemma preserved_code [code]: "preserved f h h' = (((h \ ok f) \ (h' \ ok f) \ |h \ f|\<^sub>r = |h' \ f|\<^sub>r) \ ((\h \ ok f) \ (\h' \ 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 diff --git a/Core_DOM/Core_DOM/standard/Core_DOM_Heap_WF.thy b/Core_DOM/Core_DOM/standard/Core_DOM_Heap_WF.thy index 0535ce9..55e2271 100644 --- a/Core_DOM/Core_DOM/standard/Core_DOM_Heap_WF.thy +++ b/Core_DOM/Core_DOM/standard/Core_DOM_Heap_WF.thy @@ -56,7 +56,7 @@ definition a_owner_document_valid :: "(_) heap \ bool" lemma a_owner_document_valid_code [code]: "a_owner_document_valid h \ node_ptr_kinds h |\| fset_of_list (concat (map (\parent. |h \ get_child_nodes parent|\<^sub>r) (sorted_list_of_fset (object_ptr_kinds h)) @ map (\parent. |h \ 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: " \node_ptr\fset (node_ptr_kinds h). @@ -2681,7 +2681,7 @@ lemma get_owner_document_owner_document_in_heap: assumes "h \ get_owner_document ptr \\<^sub>r owner_document" shows "owner_document |\| 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 \ invoke [] ptr () \\<^sub>r owner_document" @@ -2743,9 +2743,10 @@ next then have "some_owner_document \ set candidates" apply(rule filter_M_in_result_if_ok) using \some_owner_document |\| document_ptr_kinds h\ \root \ cast ` set |h \ get_disconnected_nodes some_owner_document|\<^sub>r\ - 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: \some_owner_document |\| document_ptr_kinds h\) + using "1" \root \ 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 \ get_disconnected_nodes some_owner_document|\<^sub>r\ \some_owner_document |\| document_ptr_kinds h\ + local.get_disconnected_nodes_ok by auto then have "candidates \ []" by auto then have "owner_document \ 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 \ 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 () \\<^sub>r owner_document \ h \ a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r child () \\<^sub>r owner_document" using document_ptr \h \ get_root_node (cast child) \\<^sub>r root\[simplified \root = cast document_ptr\ 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 \h \ get_root_node (cast child) \\<^sub>r root\[simplified \root = cast document_ptr\ 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 \h \ get_root_node (cast child) \\<^sub>r root\[simplified \root = cast document_ptr\ document_ptr], rotated] intro!: bind_pure_returns_result_I filter_M_pure_I bind_pure_I split: if_splits option.splits)[1] using \ptr |\| object_ptr_kinds h\ document_ptr_kinds_commutes by blast then show ?thesis using \known_ptr ptr\ - 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 \cast child |\| object_ptr_kinds h\ \ptr |\| object_ptr_kinds h\ 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 \cast child |\| object_ptr_kinds h\ \ptr |\| object_ptr_kinds h\ False + apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )[1] + using \cast child |\| object_ptr_kinds h\ \ptr |\| object_ptr_kinds h\ False + apply(auto simp add: node_ptr[symmetric] intro!: bind_pure_returns_result_I split: )[1] + using \cast child |\| object_ptr_kinds h\ \ptr |\| object_ptr_kinds h\ 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 \known_ptr (cast child)\ - 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 \cast child |\| object_ptr_kinds h\ \ptr |\| object_ptr_kinds h\ - apply(auto intro!: bind_pure_returns_result_I split: option.splits) + apply(auto intro!: bind_pure_returns_result_I split: option.splits)[1] + using \cast child |\| object_ptr_kinds h\ \ptr |\| object_ptr_kinds h\ + apply(auto intro!: bind_pure_returns_result_I split: option.splits)[1] + using \cast child |\| object_ptr_kinds h\ \ptr |\| object_ptr_kinds h\ + apply(auto intro!: bind_pure_returns_result_I split: option.splits)[1] + using \cast child |\| object_ptr_kinds h\ \ptr |\| object_ptr_kinds h\ + apply(auto intro!: bind_pure_returns_result_I split: option.splits)[1] by (smt \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 |\| object_ptr_kinds h\ 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 \is_document_ptr_kind ptr\ \known_ptr ptr\ \ptr |\| object_ptr_kinds h\ - 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 \ get_owner_document ptr \\<^sub>r owner_document" then have "h \ local.a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r node_ptr () \\<^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="\h h'. type_wf h \ 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 \ set ancestors then error HierarchyRequestError else return ()) } \\<^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 \ 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 \ ok (case parent_opt of Some parent \ remove_child parent child | None \ 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 \ ok (if Some node = Some ref then a_next_sibling node else return (Some ref))" (is "h \ 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 \ create_element document_ptr tag \\<^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) diff --git a/Core_DOM/Core_DOM_Scope_Components/common/Core_DOM_Functions.thy b/Core_DOM/Core_DOM_Scope_Components/common/Core_DOM_Functions.thy index f279d89..deae67a 100644 --- a/Core_DOM/Core_DOM_Scope_Components/common/Core_DOM_Functions.thy +++ b/Core_DOM/Core_DOM_Scope_Components/common/Core_DOM_Functions.thy @@ -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 \ remove_child ptr' child \\<^sub>h h'" shows "child |\| 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 \ set (insert_before_list v ref xs) \ set xs \ distinct xs \ 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 \ 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 \ ok (insert_before ptr node reference_child)" shows "ptr |\| 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 diff --git a/Core_DOM/Core_DOM_Scope_Components/common/monads/ElementMonad.thy b/Core_DOM/Core_DOM_Scope_Components/common/monads/ElementMonad.thy index 8b00146..44ddd85 100644 --- a/Core_DOM/Core_DOM_Scope_Components/common/monads/ElementMonad.thy +++ b/Core_DOM/Core_DOM_Scope_Components/common/monads/ElementMonad.thy @@ -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: diff --git a/Core_DOM/Core_DOM_Scope_Components/common/preliminaries/Heap_Error_Monad.thy b/Core_DOM/Core_DOM_Scope_Components/common/preliminaries/Heap_Error_Monad.thy index f483031..5a4a0b4 100644 --- a/Core_DOM/Core_DOM_Scope_Components/common/preliminaries/Heap_Error_Monad.thy +++ b/Core_DOM/Core_DOM_Scope_Components/common/preliminaries/Heap_Error_Monad.thy @@ -93,7 +93,7 @@ definition where "returns_result_heap h p r h' \ h \ p \\<^sub>r r \ h \ p \\<^sub>h h'" -lemma [code]: "returns_result_heap h p r h' \ (case h \ p of Inr (r', h'') \ r = r' \ h' = h'' | Inl _ \ False)" +lemma return_result_heap_code [code]: "returns_result_heap h p r h' \ (case h \ p of Inr (r', h'') \ r = r' \ h' = h'' | Inl _ \ 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 \ 'heap \ (\x. h \ f \\<^sub>r x \ h' \ f \\<^sub>r x)" lemma preserved_code [code]: "preserved f h h' = (((h \ ok f) \ (h' \ ok f) \ |h \ f|\<^sub>r = |h' \ f|\<^sub>r) \ ((\h \ ok f) \ (\h' \ 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