From 99a6566ed08f631ace23769373e7c2cd50aba2b6 Mon Sep 17 00:00:00 2001 From: Michael Herzberg Date: Thu, 16 Jul 2020 09:04:34 +0100 Subject: [PATCH] Restrict all autos to one subgoal. --- .../Core_DOM/common/Core_DOM_Functions.thy | 7 ++- .../common/monads/CharacterDataMonad.thy | 2 +- .../Core_DOM/common/monads/DocumentMonad.thy | 2 +- Core_DOM/Core_DOM/common/monads/NodeMonad.thy | 4 +- .../Core_DOM/standard/Core_DOM_Heap_WF.thy | 61 +++++++++++-------- .../safely_composable/Core_DOM_Heap_WF.thy | 31 +++++----- 6 files changed, 59 insertions(+), 48 deletions(-) diff --git a/Core_DOM/Core_DOM/common/Core_DOM_Functions.thy b/Core_DOM/Core_DOM/common/Core_DOM_Functions.thy index 48249f7..5bbe4f5 100644 --- a/Core_DOM/Core_DOM/common/Core_DOM_Functions.thy +++ b/Core_DOM/Core_DOM/common/Core_DOM_Functions.thy @@ -216,7 +216,7 @@ lemma get_child_nodes_reads: "reads (get_child_nodes_locs ptr) (get_child_nodes intro!: reads_bind_pure reads_subset[OF return_reads] )[1] apply(auto simp add: get_child_nodes\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def intro: reads_subset[OF reads_singleton] reads_subset[OF check_in_heap_reads] intro!: reads_bind_pure reads_subset[OF return_reads] - split: option.splits) + split: option.splits)[1] done end @@ -618,7 +618,8 @@ lemma set_child_nodes_get_child_nodes_different_pointers: apply(auto)[1] apply(auto)[1] apply(rule is_element_ptr_kind_obtains) - apply(auto) + apply(auto)[1] + apply(auto)[1] done lemma set_child_nodes_element_ok [simp]: @@ -668,7 +669,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) + 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)[1] 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)[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] diff --git a/Core_DOM/Core_DOM/common/monads/CharacterDataMonad.thy b/Core_DOM/Core_DOM/common/monads/CharacterDataMonad.thy index bc9b018..6eff901 100644 --- a/Core_DOM/Core_DOM/common/monads/CharacterDataMonad.thy +++ b/Core_DOM/Core_DOM/common/monads/CharacterDataMonad.thy @@ -308,7 +308,7 @@ lemma type_wf_put_ptr_not_in_heap_E: shows "type_wf h" using assms apply(auto simp add: type_wf_defs elim!: ElementMonad.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/monads/DocumentMonad.thy b/Core_DOM/Core_DOM/common/monads/DocumentMonad.thy index 1500c33..e0197ef 100644 --- a/Core_DOM/Core_DOM/common/monads/DocumentMonad.thy +++ b/Core_DOM/Core_DOM/common/monads/DocumentMonad.thy @@ -498,7 +498,7 @@ lemma put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_doct apply(auto simp add: is_document_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(auto simp add: get_M_defs) + apply(auto simp add: get_M_defs)[1] 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]: diff --git a/Core_DOM/Core_DOM/common/monads/NodeMonad.thy b/Core_DOM/Core_DOM/common/monads/NodeMonad.thy index b17a231..317a1e1 100644 --- a/Core_DOM/Core_DOM/common/monads/NodeMonad.thy +++ b/Core_DOM/Core_DOM/common/monads/NodeMonad.thy @@ -165,7 +165,7 @@ lemma type_wf_put_ptr_in_heap_E: assumes "is_node_ptr_kind ptr \ is_node_kind (the (get ptr h))" shows "type_wf h" using assms - apply(auto simp add: type_wf_defs split: option.splits if_splits) + apply(auto simp add: type_wf_defs split: option.splits if_splits)[1] 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) @@ -192,7 +192,7 @@ lemma type_wf_preserved_small: assumes "\node_ptr. preserved (get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr RNode.nothing) h h'" shows "type_wf h = type_wf h'" using type_wf_preserved allI[OF assms(2), of id, simplified] - apply(auto simp add: type_wf_defs) + apply(auto simp add: type_wf_defs)[1] apply(auto simp add: preserved_def get_M_defs node_ptr_kinds_small[OF assms(1)] split: option.splits)[1] apply (metis notin_fset option.simps(3)) 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 f2fb9c9..0bb8321 100644 --- a/Core_DOM/Core_DOM/standard/Core_DOM_Heap_WF.thy +++ b/Core_DOM/Core_DOM/standard/Core_DOM_Heap_WF.thy @@ -1492,7 +1492,7 @@ proof - apply(rule bind_cong_2) apply(auto intro!: filter_M_pure_I bind_pure_I)[1] apply(auto intro!: filter_M_pure_I bind_pure_I)[1] - apply(auto simp add: filter_eq (* dest!: returns_result_eq[OF ptrs] *)) + apply(auto simp add: filter_eq (* dest!: returns_result_eq[OF ptrs] *))[1] using filter_eq ptrs apply auto[1] using filter_eq ptrs by auto qed @@ -2808,7 +2808,11 @@ 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) + apply(auto intro!: bind_pure_I bind_pure_returns_result_I)[1] + 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)[1] + 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)[1] by (simp add: "1" local.get_disconnected_nodes_ok) then have "candidates \ []" @@ -2915,7 +2919,7 @@ proof - by (meson bind_pure_returns_result_I bind_returns_result_E3 local.get_root_node_pure) 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) @@ -3038,7 +3042,7 @@ proof - assume "is_node_ptr_kind ptr" then have ?thesis using \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) @@ -3104,7 +3108,7 @@ proof - using True by (smt \h \ get_owner_document ptr \\<^sub>r owner_document\ assms(1) assms(2) assms(3) assms(4) document_ptr_casts_commute3 get_root_node_document returns_result_eq) 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)+)+ using \is_document_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r root\ apply blast using \root |\| object_ptr_kinds h\ @@ -3119,14 +3123,15 @@ proof - by (metis node_ptr_casts_commute3) then have "h \ local.a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r root_node_ptr () \\<^sub>r owner_document" using \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\ assms(4) - apply(auto simp add: a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def elim!: bind_returns_result_E2 intro!: bind_pure_returns_result_I filter_M_pure_I bind_pure_I split: 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 elim!: bind_returns_result_E2 intro!: bind_pure_returns_result_I filter_M_pure_I bind_pure_I split: option.splits)[1] apply (metis assms(1) assms(2) assms(3) local.get_root_node_no_parent local.get_root_node_same_no_parent node_ptr returns_result_eq) using \is_node_ptr_kind root\ node_ptr returns_result_eq by fastforce 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)+)+ using \is_node_ptr_kind root\ \known_ptr root\ - apply(auto simp add: known_ptr_impl DocumentClass.known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)[2] + apply(auto simp add: known_ptr_impl DocumentClass.known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)[1] + apply(auto simp add: known_ptr_impl DocumentClass.known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)[1] using \root |\| object_ptr_kinds h\ by(auto simp add: root_node_ptr) qed @@ -3137,10 +3142,10 @@ proof - case True have "root = cast owner_document" using \h \ get_owner_document root \\<^sub>r owner_document\ - 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) - apply(auto simp add: True 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 split: if_splits) + apply(auto simp add: True 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 split: if_splits)[1] apply (metis True cast_document_ptr_not_node_ptr(2) is_document_ptr_kind_obtains is_node_ptr_kind_none node_ptr_casts_commute3 option.case_eq_if) by (metis True cast_document_ptr_not_node_ptr(1) document_ptr_casts_commute3 is_node_ptr_kind_none node_ptr_casts_commute3 option.case_eq_if) then show ?thesis @@ -3155,16 +3160,16 @@ proof - by (metis node_ptr_casts_commute3) then have "h \ local.a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r root_node_ptr () \\<^sub>r owner_document" using \h \ get_owner_document root \\<^sub>r owner_document\ - 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 simp add: is_document_ptr_kind_none elim!: bind_returns_result_E2) 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" - apply(auto simp add: a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def elim!: bind_returns_result_E2 intro!: bind_pure_returns_result_I filter_M_pure_I bind_pure_I split: 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 elim!: bind_returns_result_E2 intro!: bind_pure_returns_result_I filter_M_pure_I bind_pure_I split: option.splits)[1] using assms(1) assms(2) assms(3) assms(4) local.get_root_node_no_parent local.get_root_node_same_no_parent node_ptr returns_result_eq root_node_ptr by fastforce+ 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)+)+ using node_ptr \known_ptr ptr\ \ptr |\| object_ptr_kinds h\ @@ -3185,7 +3190,7 @@ locale l_get_owner_document_wf_get_root_node_wf = l_heap_is_wellformed_defs + l_ lemma get_owner_document_wf_get_root_node_wf_is_l_get_owner_document_wf_get_root_node_wf [instances]: "l_get_owner_document_wf_get_root_node_wf heap_is_wellformed type_wf known_ptr known_ptrs get_root_node get_owner_document" - apply(auto simp add: l_get_owner_document_wf_get_root_node_wf_def l_get_owner_document_wf_get_root_node_wf_axioms_def instances) + apply(auto simp add: l_get_owner_document_wf_get_root_node_wf_def l_get_owner_document_wf_get_root_node_wf_axioms_def instances)[1] using get_root_node_document apply blast using get_root_node_same_owner_document apply (blast, blast) done @@ -6097,7 +6102,7 @@ proof - using assms(2) assms(4) local.known_ptrs_known_ptr node_ptr_kinds_commutes by blast then show ?thesis using assms - apply(auto simp add: a_next_sibling_def intro!: bind_is_OK_pure_I split: option.splits list.splits) + apply(auto simp add: a_next_sibling_def intro!: bind_is_OK_pure_I split: option.splits list.splits)[1] using get_child_nodes_ok local.get_parent_parent_in_heap local.known_ptrs_known_ptr by blast qed @@ -6133,7 +6138,7 @@ proof - using \ptr |\| object_ptr_kinds h\ apply(simp add: get_child_nodes_def a_get_child_nodes_tups_def) apply(split invoke_splits)+ - apply(auto split: option.splits) + apply(auto split: option.splits)[1] apply (meson invoke_empty is_OK_returns_result_I) apply (meson invoke_empty is_OK_returns_result_I) by(auto simp add: get_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 elim!: bind_returns_result_E2 split: option.splits) @@ -6181,13 +6186,15 @@ 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) ultimately show ?thesis using assms(4) - apply(auto simp add: get_child_nodes_def a_get_child_nodes_tups_def) + apply(auto simp add: get_child_nodes_def a_get_child_nodes_tups_def)[1] apply(split invoke_splits)+ - apply(auto elim!: bind_returns_result_E2 split: option.splits) - apply(auto simp add: get_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 elim!: bind_returns_result_E2 split: option.splits) - using \ptr |\| object_ptr_kinds h\ \is_document_ptr_kind ptr\ \known_ptr ptr\ \object_ptr_kinds h = object_ptr_kinds h2\ \type_wf h2\ assms(4) local.set_child_nodes_document1_ok apply blast - using \ptr |\| object_ptr_kinds h\ \is_document_ptr_kind ptr\ \known_ptr ptr\ \object_ptr_kinds h = object_ptr_kinds h2\ \type_wf h2\ assms(4) local.set_child_nodes_document1_ok apply blast - using \ptr |\| object_ptr_kinds h\ \is_document_ptr_kind ptr\ \known_ptr ptr\ \object_ptr_kinds h = object_ptr_kinds h2\ \type_wf h2\ assms(4) is_element_ptr_kind_cast local.set_child_nodes_document2_ok by blast + apply(auto elim!: bind_returns_result_E2 split: option.splits)[1] + apply(auto simp add: get_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 elim!: bind_returns_result_E2 split: option.splits)[1] + using assms(5) apply auto[1] + using \is_document_ptr_kind ptr\ \known_ptr ptr\ \object_ptr_kinds h = object_ptr_kinds h2\ \ptr |\| object_ptr_kinds h\ \type_wf h2\ local.set_child_nodes_document1_ok apply blast + using \is_document_ptr_kind ptr\ \known_ptr ptr\ \object_ptr_kinds h = object_ptr_kinds h2\ \ptr |\| object_ptr_kinds h\ \type_wf h2\ is_element_ptr_kind_cast local.set_child_nodes_document2_ok apply blast + using \\ is_character_data_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr\ apply blast + by (metis False is_element_ptr_implies_kind option.case_eq_if) qed then obtain h' where @@ -6203,7 +6210,7 @@ proof - bind_is_OK_pure_I[OF get_disconnected_nodes_pure] bind_is_OK_I[rotated, OF h2] dest!: returns_result_eq[OF assms(4)] returns_result_eq[OF owner_document] returns_result_eq[OF disconnected_nodes_h] -) +)[1] using h2 returns_result_select_result by force qed @@ -6345,7 +6352,7 @@ proof - using \h2 \ ok get_disconnected_nodes old_document\ using \h3 \ ok get_disconnected_nodes document_ptr\ apply(auto dest!: returns_result_eq[OF old_disc_nodes] returns_result_eq[OF disc_nodes] - intro!: bind_is_OK_I[rotated, OF h3] bind_is_OK_pure_I[OF get_disconnected_nodes_pure] ) + intro!: bind_is_OK_I[rotated, OF h3] bind_is_OK_pure_I[OF get_disconnected_nodes_pure] )[1] using \h2 \ ok set_disconnected_nodes old_document (remove1 child old_disc_nodes)\ by auto qed then obtain h' where @@ -6368,7 +6375,7 @@ proof - intro!: bind_is_OK_pure_I[OF get_owner_document_pure] bind_is_OK_pure_I[OF get_parent_pure] bind_is_OK_I[rotated, OF h2] - dest!: returns_result_eq[OF parent_opt] returns_result_eq[OF old_document]) + dest!: returns_result_eq[OF parent_opt] returns_result_eq[OF old_document])[1] using \h \ ok (case parent_opt of None \ return () | Some parent \ remove_child parent child)\ by auto qed @@ -6514,7 +6521,7 @@ proof - bind_is_OK_pure_I[OF get_disconnected_nodes_pure] dest!: returns_result_eq[OF owner_document] returns_result_eq[OF disconnected_nodes_h2] returns_heap_eq[OF h2] returns_heap_eq[OF h3] dest!: sym[of node ref] - ) + )[1] using returns_result_eq by fastforce qed end @@ -7146,7 +7153,7 @@ proof - bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated] ) then have "h \ create_character_data document_ptr text \\<^sub>r new_character_data_ptr" - apply(auto simp add: create_character_data_def intro!: bind_returns_result_I) + apply(auto simp add: create_character_data_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_SC_DOM/safely_composable/Core_DOM_Heap_WF.thy b/Core_DOM/Core_SC_DOM/safely_composable/Core_DOM_Heap_WF.thy index 5158344..f5b0c25 100644 --- a/Core_DOM/Core_SC_DOM/safely_composable/Core_DOM_Heap_WF.thy +++ b/Core_DOM/Core_SC_DOM/safely_composable/Core_DOM_Heap_WF.thy @@ -1492,7 +1492,7 @@ proof - apply(rule bind_cong_2) apply(auto intro!: filter_M_pure_I bind_pure_I)[1] apply(auto intro!: filter_M_pure_I bind_pure_I)[1] - apply(auto simp add: filter_eq (* dest!: returns_result_eq[OF ptrs] *)) + apply(auto simp add: filter_eq (* dest!: returns_result_eq[OF ptrs] *))[1] using filter_eq ptrs apply auto[1] using filter_eq ptrs by auto qed @@ -2808,8 +2808,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 @@ -2915,7 +2917,7 @@ proof - by (meson bind_pure_returns_result_I bind_returns_result_E3 local.get_root_node_pure) 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) @@ -3107,7 +3109,7 @@ proof - using True by (smt \h \ get_owner_document ptr \\<^sub>r owner_document\ assms(1) assms(2) assms(3) assms(4) document_ptr_casts_commute3 get_root_node_document returns_result_eq) 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)+)+ using \is_document_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r root\ apply blast using \root |\| object_ptr_kinds h\ @@ -3122,14 +3124,15 @@ proof - by (metis node_ptr_casts_commute3) then have "h \ local.a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r root_node_ptr () \\<^sub>r owner_document" using \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\ assms(4) - apply(auto simp add: a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def elim!: bind_returns_result_E2 intro!: bind_pure_returns_result_I filter_M_pure_I bind_pure_I split: 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 elim!: bind_returns_result_E2 intro!: bind_pure_returns_result_I filter_M_pure_I bind_pure_I split: option.splits)[1] apply (metis assms(1) assms(2) assms(3) local.get_root_node_no_parent local.get_root_node_same_no_parent node_ptr returns_result_eq) using \is_node_ptr_kind root\ node_ptr returns_result_eq by fastforce 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)+)+ using \is_node_ptr_kind root\ \known_ptr root\ - apply(auto simp add: known_ptr_impl DocumentClass.known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)[2] + apply(auto simp add: known_ptr_impl DocumentClass.known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)[1] + apply(auto simp add: known_ptr_impl DocumentClass.known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)[1] using \root |\| object_ptr_kinds h\ by(auto simp add: root_node_ptr) qed @@ -3140,10 +3143,10 @@ proof - case True have "root = cast owner_document" using \h \ get_owner_document root \\<^sub>r owner_document\ - 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) - apply(auto simp add: True 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 split: if_splits) + apply(auto simp add: True 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 split: if_splits)[1] apply (metis True cast_document_ptr_not_node_ptr(2) is_document_ptr_kind_obtains is_node_ptr_kind_none node_ptr_casts_commute3 option.case_eq_if) by (metis True cast_document_ptr_not_node_ptr(1) document_ptr_casts_commute3 is_node_ptr_kind_none node_ptr_casts_commute3 option.case_eq_if) then show ?thesis @@ -3158,16 +3161,16 @@ proof - by (metis node_ptr_casts_commute3) then have "h \ local.a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r root_node_ptr () \\<^sub>r owner_document" using \h \ get_owner_document root \\<^sub>r owner_document\ - 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 simp add: is_document_ptr_kind_none elim!: bind_returns_result_E2) 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" - apply(auto simp add: a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def elim!: bind_returns_result_E2 intro!: bind_pure_returns_result_I filter_M_pure_I bind_pure_I split: 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 elim!: bind_returns_result_E2 intro!: bind_pure_returns_result_I filter_M_pure_I bind_pure_I split: option.splits)[1] using assms(1) assms(2) assms(3) assms(4) local.get_root_node_no_parent local.get_root_node_same_no_parent node_ptr returns_result_eq root_node_ptr by fastforce+ 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)+)+ using node_ptr \known_ptr ptr\ \ptr |\| object_ptr_kinds h\ @@ -3188,7 +3191,7 @@ locale l_get_owner_document_wf_get_root_node_wf = l_heap_is_wellformed_defs + l_ lemma get_owner_document_wf_get_root_node_wf_is_l_get_owner_document_wf_get_root_node_wf [instances]: "l_get_owner_document_wf_get_root_node_wf heap_is_wellformed type_wf known_ptr known_ptrs get_root_node get_owner_document" - apply(auto simp add: l_get_owner_document_wf_get_root_node_wf_def l_get_owner_document_wf_get_root_node_wf_axioms_def instances) + apply(auto simp add: l_get_owner_document_wf_get_root_node_wf_def l_get_owner_document_wf_get_root_node_wf_axioms_def instances)[1] using get_root_node_document apply blast using get_root_node_same_owner_document apply (blast, blast) done