From bdd16a015f2a4582af084c38d49964bd41c412e7 Mon Sep 17 00:00:00 2001 From: Michael Herzberg Date: Tue, 16 Jul 2019 00:20:30 +0100 Subject: [PATCH] Made various parts work better with the code generator. --- Core_DOM/Core_DOM_Heap_WF.thy | 373 ++++++++------------ Core_DOM/classes/CharacterDataClass.thy | 14 +- Core_DOM/classes/DocumentClass.thy | 14 +- Core_DOM/classes/ElementClass.thy | 15 +- Core_DOM/classes/NodeClass.thy | 16 +- Core_DOM/classes/ObjectClass.thy | 27 +- Core_DOM/monads/CharacterDataMonad.thy | 42 +-- Core_DOM/monads/DocumentMonad.thy | 48 ++- Core_DOM/monads/ElementMonad.thy | 70 ++-- Core_DOM/monads/NodeMonad.thy | 5 +- Core_DOM/preliminaries/Heap_Error_Monad.thy | 5 + Core_DOM/tests/Core_DOM_BaseTest.thy | 33 -- 12 files changed, 281 insertions(+), 381 deletions(-) diff --git a/Core_DOM/Core_DOM_Heap_WF.thy b/Core_DOM/Core_DOM_Heap_WF.thy index eebd0f2..f312a29 100644 --- a/Core_DOM/Core_DOM_Heap_WF.thy +++ b/Core_DOM/Core_DOM_Heap_WF.thy @@ -47,30 +47,75 @@ locale l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^su begin definition a_owner_document_valid :: "(_) heap \ bool" where - "a_owner_document_valid h = (\node_ptr. node_ptr |\| node_ptr_kinds h \ + "a_owner_document_valid h \ (\node_ptr \ fset (node_ptr_kinds h). ((\document_ptr. document_ptr |\| document_ptr_kinds h \ node_ptr \ set |h \ get_disconnected_nodes document_ptr|\<^sub>r) \ (\parent_ptr. parent_ptr |\| object_ptr_kinds h \ node_ptr \ set |h \ get_child_nodes parent_ptr|\<^sub>r)))" +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) +proof - + fix x + assume 1: " \node_ptr\fset (node_ptr_kinds h). + (\document_ptr. document_ptr |\| document_ptr_kinds h \ node_ptr \ set |h \ get_disconnected_nodes document_ptr|\<^sub>r) \ + (\parent_ptr. parent_ptr |\| object_ptr_kinds h \ node_ptr \ set |h \ get_child_nodes parent_ptr|\<^sub>r)" + assume 2: "x |\| node_ptr_kinds h" + assume 3: "x |\| fset_of_list (concat (map (\parent. |h \ get_disconnected_nodes parent|\<^sub>r) (sorted_list_of_fset (document_ptr_kinds h))))" + have "\(\document_ptr. document_ptr |\| document_ptr_kinds h \ x \ set |h \ get_disconnected_nodes document_ptr|\<^sub>r)" + using 1 2 3 + by (smt UN_I fset_of_list_elem image_eqI notin_fset set_concat set_map sorted_list_of_fset_simps(1)) + then + have "(\parent_ptr. parent_ptr |\| object_ptr_kinds h \ x \ set |h \ get_child_nodes parent_ptr|\<^sub>r)" + using 1 2 + by auto + then obtain parent_ptr where parent_ptr: "parent_ptr |\| object_ptr_kinds h \ x \ set |h \ get_child_nodes parent_ptr|\<^sub>r" + by auto + moreover have "parent_ptr \ set (sorted_list_of_fset (object_ptr_kinds h))" + using parent_ptr by auto + moreover have "|h \ get_child_nodes parent_ptr|\<^sub>r \ set (map (\parent. |h \ get_child_nodes parent|\<^sub>r) (sorted_list_of_fset (object_ptr_kinds h)))" + using calculation(2) by auto + ultimately + show "x |\| fset_of_list (concat (map (\parent. |h \ get_child_nodes parent|\<^sub>r) (sorted_list_of_fset (object_ptr_kinds h))))" + using fset_of_list_elem by fastforce +next + fix node_ptr + assume 1: "node_ptr_kinds h |\| fset_of_list (concat (map (\parent. |h \ get_child_nodes parent|\<^sub>r) (sorted_list_of_fset (object_ptr_kinds h)))) |\| fset_of_list (concat (map (\parent. |h \ get_disconnected_nodes parent|\<^sub>r) (sorted_list_of_fset (document_ptr_kinds h))))" + assume 2: "node_ptr |\| node_ptr_kinds h" + assume 3: "\parent_ptr. parent_ptr |\| object_ptr_kinds h \ node_ptr \ set |h \ get_child_nodes parent_ptr|\<^sub>r" + have "node_ptr \ set (concat (map (\parent. |h \ get_child_nodes parent|\<^sub>r) (sorted_list_of_fset (object_ptr_kinds h)))) \ node_ptr \ set (concat (map (\parent. |h \ get_disconnected_nodes parent|\<^sub>r) (sorted_list_of_fset (document_ptr_kinds h))))" + using 1 2 + by (meson fin_mono fset_of_list_elem funion_iff) + then + show "\document_ptr. document_ptr |\| document_ptr_kinds h \ node_ptr \ set |h \ get_disconnected_nodes document_ptr|\<^sub>r" + using 3 + by auto +qed definition a_parent_child_rel :: "(_) heap \ ((_) object_ptr \ (_) object_ptr) set" where "a_parent_child_rel h = {(parent, child). parent |\| object_ptr_kinds h \ child \ cast ` set |h \ get_child_nodes parent|\<^sub>r}" +lemma a_parent_child_rel_code [code]: "a_parent_child_rel h = set (concat (map + (\parent. map + (\child. (parent, cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r child)) + |h \ get_child_nodes parent|\<^sub>r) + (sorted_list_of_fset (object_ptr_kinds h))) +)" + by(auto simp add: a_parent_child_rel_def) + definition a_acyclic_heap :: "(_) heap \ bool" where "a_acyclic_heap h = acyclic (a_parent_child_rel h)" - definition a_all_ptrs_in_heap :: "(_) heap \ bool" where - "a_all_ptrs_in_heap h = ((\ptr children. (h \ get_child_nodes ptr \\<^sub>r children) - \ fset_of_list children |\| node_ptr_kinds h) - \ (\document_ptr disc_node_ptrs. (h \ get_disconnected_nodes document_ptr \\<^sub>r disc_node_ptrs) - \ fset_of_list disc_node_ptrs |\| node_ptr_kinds h))" - + "a_all_ptrs_in_heap h \ + (\ptr \ fset (object_ptr_kinds h). set |h \ get_child_nodes ptr|\<^sub>r \ fset (node_ptr_kinds h)) \ + (\document_ptr \ fset (document_ptr_kinds h). set |h \ get_disconnected_nodes document_ptr|\<^sub>r \ fset (node_ptr_kinds h))" definition a_distinct_lists :: "(_) heap \ bool" where @@ -94,8 +139,13 @@ global_interpretation l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub defines heap_is_wellformed = "l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.a_heap_is_wellformed get_child_nodes get_disconnected_nodes" and parent_child_rel = "l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.a_parent_child_rel get_child_nodes" + and acyclic_heap = a_acyclic_heap + and all_ptrs_in_heap = a_all_ptrs_in_heap + and distinct_lists = a_distinct_lists + and owner_document_valid = a_owner_document_valid . + locale l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M = l_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs + l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs get_child_nodes get_child_nodes_locs get_disconnected_nodes @@ -218,7 +268,7 @@ lemma heap_is_wellformed_children_in_heap: shows "child |\| node_ptr_kinds h" using assms apply(auto simp add: heap_is_wellformed_def a_all_ptrs_in_heap_def)[1] - by (meson fset_of_list_elem fset_rev_mp) + by (metis (no_types, lifting) finite_set_in is_OK_returns_result_I local.get_child_nodes_ptr_in_heap select_result_I2 subsetD) lemma heap_is_wellformed_one_parent: assumes "heap_is_wellformed h" @@ -267,12 +317,12 @@ lemma parent_child_rel_child_in_heap: \ (parent, child_ptr) \ parent_child_rel h \ child_ptr |\| object_ptr_kinds h" apply(auto simp add: heap_is_wellformed_def parent_child_rel_def a_all_ptrs_in_heap_def)[1] using get_child_nodes_ok - by (meson fin_mono fset_of_list_elem returns_result_select_result) + by (meson finite_set_in subsetD) lemma heap_is_wellformed_disc_nodes_in_heap: "heap_is_wellformed h \ h \ get_disconnected_nodes document_ptr \\<^sub>r disc_nodes \ node \ set disc_nodes \ node |\| node_ptr_kinds h" - by (meson fset_mp fset_of_list_elem local.a_all_ptrs_in_heap_def local.heap_is_wellformed_def) + by (metis (no_types, lifting) finite_set_in is_OK_returns_result_I local.a_all_ptrs_in_heap_def local.get_disconnected_nodes_ptr_in_heap local.heap_is_wellformed_def select_result_I2 subsetD) lemma heap_is_wellformed_one_disc_parent: "heap_is_wellformed h \ h \ get_disconnected_nodes document_ptr \\<^sub>r disc_nodes @@ -667,8 +717,7 @@ proof - moreover have "a_all_ptrs_in_heap h" using heap_is_wellformed by (simp add: heap_is_wellformed_def) then have "a_all_ptrs_in_heap h'" - by(auto simp add: a_all_ptrs_in_heap_def node_ptr_kinds_def node_ptr_kinds_eq2 - object_ptr_kinds_eq3 children_eq disconnected_nodes_eq) + by (simp add: children_eq2 disconnected_nodes_eq2 document_ptr_kinds_eq3 l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.a_all_ptrs_in_heap_def node_ptr_kinds_eq3 object_ptr_kinds_eq3) moreover have h0: "a_distinct_lists h" using heap_is_wellformed by (simp add: heap_is_wellformed_def) @@ -3531,35 +3580,20 @@ have "type_wf h2" using assms(1) by (simp add: heap_is_wellformed_def) then have "a_all_ptrs_in_heap h'" apply(auto simp add: a_all_ptrs_in_heap_def node_ptr_kinds_eq3 disconnected_nodes_eq)[1] - apply (metis (no_types, lifting) type_wf assms(3) children_eq2 children_h children_h' - fset_of_list_subset fsubsetD get_child_nodes_ok get_child_nodes_ptr_in_heap - is_OK_returns_result_E is_OK_returns_result_I local.known_ptrs_known_ptr - object_ptr_kinds_eq3 select_result_I2 set_remove1_subset) - by (metis (no_types, lifting) - \\thesis. (\owner_document children_h h2 disconnected_nodes_h. - \h \ get_owner_document (cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r child) \\<^sub>r owner_document; - h \ get_child_nodes ptr \\<^sub>r children_h; child \ set children_h; - h \ get_disconnected_nodes owner_document \\<^sub>r disconnected_nodes_h; - h \ set_disconnected_nodes owner_document (child # disconnected_nodes_h) \\<^sub>h h2; - h2 \ set_child_nodes ptr (remove1 child children_h) \\<^sub>h h'\ \ thesis) \ thesis\ - disconnected_nodes_h disconnected_nodes_eq disconnected_nodes_h' fset_mp fset_of_list_elem - returns_result_eq set_ConsD) - + apply (metis (no_types, lifting) \type_wf h'\ assms(2) assms(3) local.get_child_nodes_ok local.known_ptrs_known_ptr local.remove_child_children_subset notin_fset object_ptr_kinds_eq3 returns_result_select_result subset_code(1) type_wf) + apply (metis (no_types, lifting) assms(2) disconnected_nodes_eq2 disconnected_nodes_h disconnected_nodes_h' document_ptr_kinds_eq3 finite_set_in local.remove_child_child_in_heap node_ptr_kinds_eq3 select_result_I2 set_ConsD subset_code(1)) + done moreover have "a_owner_document_valid h" using assms(1) by (simp add: heap_is_wellformed_def) then have "a_owner_document_valid h'" apply(auto simp add: a_owner_document_valid_def object_ptr_kinds_eq3 document_ptr_kinds_eq3 node_ptr_kinds_eq3)[1] proof - - fix node_ptr - assume 0: "\node_ptr. node_ptr |\| node_ptr_kinds h' - \ (\document_ptr. document_ptr |\| document_ptr_kinds h' - \ node_ptr \ set |h \ get_disconnected_nodes document_ptr|\<^sub>r) - \ (\parent_ptr. parent_ptr |\| object_ptr_kinds h' - \ node_ptr \ set |h \ get_child_nodes parent_ptr|\<^sub>r)" - and 1: "node_ptr |\| node_ptr_kinds h'" - and 2: "\parent_ptr. parent_ptr |\| object_ptr_kinds h' - \ node_ptr \ set |h' \ get_child_nodes parent_ptr|\<^sub>r" + +fix node_ptr +assume 0: "\node_ptr\fset (node_ptr_kinds h'). (\document_ptr. document_ptr |\| document_ptr_kinds h' \ node_ptr \ set |h \ get_disconnected_nodes document_ptr|\<^sub>r) \ (\parent_ptr. parent_ptr |\| object_ptr_kinds h' \ node_ptr \ set |h \ get_child_nodes parent_ptr|\<^sub>r)" + and 1: "node_ptr |\| node_ptr_kinds h'" + and 2: "\parent_ptr. parent_ptr |\| object_ptr_kinds h' \ node_ptr \ set |h' \ get_child_nodes parent_ptr|\<^sub>r" then show "\document_ptr. document_ptr |\| document_ptr_kinds h' \ node_ptr \ set |h' \ get_disconnected_nodes document_ptr|\<^sub>r" proof (cases "node_ptr = child") @@ -3575,7 +3609,7 @@ have "type_wf h2" using 0 1 2 children_eq2 children_h children_h' disconnected_nodes_eq2 disconnected_nodes_h disconnected_nodes_h' apply(auto simp add: children_eq2 disconnected_nodes_eq2 dest!: select_result_I2)[1] - by (metis children_eq2 disconnected_nodes_eq2 in_set_remove1 list.set_intros(2)) + by (metis children_eq2 disconnected_nodes_eq2 finite_set_in in_set_remove1 list.set_intros(2)) qed qed @@ -4479,29 +4513,20 @@ proof - using wellformed_h2 by (simp add: heap_is_wellformed_def) then have "a_all_ptrs_in_heap h3" apply(auto simp add: a_all_ptrs_in_heap_def node_ptr_kinds_eq3_h2 children_eq_h2)[1] - by (metis (mono_tags, lifting) disc_nodes_old_document_h2 disc_nodes_old_document_h3 - disconnected_nodes_eq_h2 fset_of_list_elem fset_rev_mp returns_result_eq - set_remove1_subset subsetCE) + apply (simp add: children_eq2_h2 object_ptr_kinds_h2_eq3 subset_code(1)) + by (metis (no_types, lifting) \child \ set disc_nodes_old_document_h2\ \type_wf h2\ disc_nodes_old_document_h2 disc_nodes_old_document_h3 disconnected_nodes_eq2_h2 document_ptr_kinds_eq3_h2 in_set_remove1 local.get_disconnected_nodes_ok local.heap_is_wellformed_disc_nodes_in_heap node_ptr_kinds_eq3_h2 returns_result_select_result select_result_I2 wellformed_h2) then have "a_all_ptrs_in_heap h'" apply(auto simp add: a_all_ptrs_in_heap_def node_ptr_kinds_eq3_h3 children_eq_h3)[1] - by (metis (no_types) NodeMonad.ptr_kinds_ptr_kinds_M child_in_heap disc_nodes_document_ptr_h' - disc_nodes_document_ptr_h3 disconnected_nodes_eq_h3 fset_mp fset_of_list_elem - node_ptr_kinds_eq_h node_ptr_kinds_eq_h2 node_ptr_kinds_eq_h3 select_result_I2 - set_ConsD) + apply (simp add: children_eq2_h3 object_ptr_kinds_h3_eq3 subset_code(1)) + by (metis (no_types, lifting) \child \ set disc_nodes_old_document_h2\ disc_nodes_document_ptr_h' disc_nodes_document_ptr_h2 disc_nodes_old_document_h2 disconnected_nodes_eq2_h3 document_ptr_kinds_eq3_h3 finite_set_in local.heap_is_wellformed_disc_nodes_in_heap node_ptr_kinds_eq3_h2 node_ptr_kinds_eq3_h3 select_result_I2 set_ConsD subset_code(1) wellformed_h2) moreover have "a_owner_document_valid h2" using wellformed_h2 by (simp add: heap_is_wellformed_def) then have "a_owner_document_valid h'" apply(simp add: a_owner_document_valid_def node_ptr_kinds_eq_h2 node_ptr_kinds_eq3_h3 - object_ptr_kinds_eq_h2 object_ptr_kinds_eq_h3 document_ptr_kinds_eq2_h2 + object_ptr_kinds_eq_h2 object_ptr_kinds_eq_h3 document_ptr_kinds_eq2_h2 document_ptr_kinds_eq2_h3 children_eq2_h2 children_eq2_h3 ) - by (metis (no_types) disc_nodes_document_ptr_h' disc_nodes_document_ptr_h2 - disc_nodes_old_document_h2 disc_nodes_old_document_h3 - disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 document_ptr_in_heap - document_ptr_kinds_eq3_h2 document_ptr_kinds_eq3_h3 in_set_remove1 - list.set_intros(1) list.set_intros(2) node_ptr_kinds_eq3_h2 - node_ptr_kinds_eq3_h3 object_ptr_kinds_h2_eq3 object_ptr_kinds_h3_eq3 - select_result_I2) + by (smt disc_nodes_document_ptr_h' disc_nodes_document_ptr_h2 disc_nodes_old_document_h2 disc_nodes_old_document_h3 disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 document_ptr_in_heap document_ptr_kinds_eq3_h2 document_ptr_kinds_eq3_h3 in_set_remove1 list.set_intros(1) node_ptr_kinds_eq3_h2 node_ptr_kinds_eq3_h3 object_ptr_kinds_h2_eq3 object_ptr_kinds_h3_eq3 select_result_I2 set_subset_Cons subset_code(1)) have a_distinct_lists_h2: "a_distinct_lists h2" using wellformed_h2 by (simp add: heap_is_wellformed_def) @@ -5200,46 +5225,46 @@ proof - have "a_all_ptrs_in_heap h3" using \a_all_ptrs_in_heap h2\ apply(auto simp add: a_all_ptrs_in_heap_def object_ptr_kinds_M_eq2_h2 node_ptr_kinds_eq2_h2 - children_eq_h2)[1] + children_eq_h2)[1] using disconnected_nodes_eq2_h2 disconnected_nodes_h2 disconnected_nodes_h3 using node_ptr_kinds_eq2_h2 apply auto[1] - by (metis (no_types, lifting) NodeMonad.ptr_kinds_ptr_kinds_M disconnected_nodes_eq_h2 - disconnected_nodes_h2 disconnected_nodes_h3 fset_mp fset_of_list_subset - node_ptr_kinds_eq2_h2 select_result_I2 set_remove1_subset) + apply (metis \known_ptrs h2\ \type_wf h3\ children_eq_h2 local.get_child_nodes_ok local.heap_is_wellformed_children_in_heap local.known_ptrs_known_ptr object_ptr_kinds_M_eq3_h2 returns_result_select_result wellformed_h2) + by (metis (no_types, lifting) disconnected_nodes_eq2_h2 disconnected_nodes_h2 disconnected_nodes_h3 document_ptr_kinds_commutes finite_set_in node_ptr_kinds_commutes object_ptr_kinds_M_eq3_h2 select_result_I2 set_remove1_subset subsetD) + have "set children_h3 \ set |h' \ node_ptr_kinds_M|\<^sub>r" using children_h3 \a_all_ptrs_in_heap h3\ apply(auto simp add: a_all_ptrs_in_heap_def node_ptr_kinds_eq2_h3)[1] - by (metis (no_types, hide_lams) fset_mp fset_of_list_elem node_ptr_kinds_commutes object_ptr_kinds_M_eq3_h') + by (metis children_eq_h2 l_heap_is_wellformed.heap_is_wellformed_children_in_heap local.l_heap_is_wellformed_axioms node_ptr_kinds_commutes object_ptr_kinds_M_eq3_h' object_ptr_kinds_M_eq3_h2 wellformed_h2) + then have "set (insert_before_list node reference_child children_h3) \ set |h' \ node_ptr_kinds_M|\<^sub>r" using node_in_heap apply(auto simp add: node_ptr_kinds_eq2_h node_ptr_kinds_eq2_h2 node_ptr_kinds_eq2_h3)[1] by (metis (no_types, hide_lams) contra_subsetD finite_set_in insert_before_list_in_set - node_ptr_kinds_commutes object_ptr_kinds_M_eq3_h object_ptr_kinds_M_eq3_h' - object_ptr_kinds_M_eq3_h2) + node_ptr_kinds_commutes object_ptr_kinds_M_eq3_h object_ptr_kinds_M_eq3_h' + object_ptr_kinds_M_eq3_h2) then show ?thesis using \a_all_ptrs_in_heap h3\ apply(auto simp add: object_ptr_kinds_M_eq3_h' a_all_ptrs_in_heap_def node_ptr_kinds_def - node_ptr_kinds_eq2_h3 disconnected_nodes_eq_h3)[1] + node_ptr_kinds_eq2_h3 disconnected_nodes_eq_h3)[1] using children_eq_h3 children_h' - by (metis (no_types, hide_lams) NodeMonad.ptr_kinds_ptr_kinds_M - \set (insert_before_list node reference_child children_h3) \ set |h' \ node_ptr_kinds_M|\<^sub>r\ - fset.map_comp fset_mp fset_of_list_elem node_ptr_kinds_def node_ptr_kinds_eq2_h3 - returns_result_eq subsetCE) - qed + apply (metis (no_types, lifting) children_eq2_h3 finite_set_in select_result_I2 subsetD) + by (metis (no_types) \type_wf h'\ disconnected_nodes_eq2_h3 disconnected_nodes_eq_h3 finite_set_in is_OK_returns_result_I local.get_disconnected_nodes_ok local.get_disconnected_nodes_ptr_in_heap returns_result_select_result subsetD) + qed + moreover have "a_distinct_lists h2" using wellformed_h2 by (simp add: heap_is_wellformed_def) then have "a_distinct_lists h3" proof(auto simp add: a_distinct_lists_def object_ptr_kinds_M_eq2_h2 document_ptr_kinds_eq2_h2 - children_eq2_h2 intro!: distinct_concat_map_I)[1] + children_eq2_h2 intro!: distinct_concat_map_I)[1] fix x assume 1: "x |\| document_ptr_kinds h3" and 2: "distinct (concat (map (\document_ptr. |h2 \ get_disconnected_nodes document_ptr|\<^sub>r) (sorted_list_of_set (fset (document_ptr_kinds h3)))))" show "distinct |h3 \ get_disconnected_nodes x|\<^sub>r" using distinct_concat_map_E(2)[OF 2] select_result_I2[OF disconnected_nodes_h3] - disconnected_nodes_eq2_h2 select_result_I2[OF disconnected_nodes_h2] 1 + disconnected_nodes_eq2_h2 select_result_I2[OF disconnected_nodes_h2] 1 by (metis (full_types) distinct_remove1 finite_fset fmember.rep_eq set_sorted_list_of_set) next fix x y xa @@ -5266,17 +5291,17 @@ proof - proof (cases "y = owner_document") case True then show ?thesis - using distinct_concat_map_E(1)[OF 1] - using 2 3 4 5 6 select_result_I2[OF disconnected_nodes_h3] select_result_I2[OF disconnected_nodes_h2] - apply(auto simp add: True disconnected_nodes_eq2_h2[OF \x \ owner_document\])[1] - by (metis (no_types, hide_lams) disconnected_nodes_eq2_h2 disjoint_iff_not_equal notin_set_remove1) + using distinct_concat_map_E(1)[OF 1] + using 2 3 4 5 6 select_result_I2[OF disconnected_nodes_h3] select_result_I2[OF disconnected_nodes_h2] + apply(auto simp add: True disconnected_nodes_eq2_h2[OF \x \ owner_document\])[1] + by (metis (no_types, hide_lams) disconnected_nodes_eq2_h2 disjoint_iff_not_equal notin_set_remove1) next case False then show ?thesis using distinct_concat_map_E(1)[OF 1, simplified, OF 2 3 4] 5 6 using disconnected_nodes_eq2_h2 disconnected_nodes_h2 disconnected_nodes_h3 - disjoint_iff_not_equal finite_fset fmember.rep_eq notin_set_remove1 select_result_I2 - set_sorted_list_of_set + disjoint_iff_not_equal finite_fset fmember.rep_eq notin_set_remove1 select_result_I2 + set_sorted_list_of_set by (metis (no_types, lifting)) qed qed @@ -5291,10 +5316,10 @@ proof - have 6: "set |h3 \ get_child_nodes xa|\<^sub>r \ set |h2 \ get_disconnected_nodes xb|\<^sub>r = {}" using 1 2 4 by (metis \type_wf h2\ children_eq2_h2 document_ptr_kinds_commutes known_ptrs - local.get_child_nodes_ok local.get_disconnected_nodes_ok - local.heap_is_wellformed_children_disc_nodes_different local.known_ptrs_known_ptr - object_ptr_kinds_M_eq3_h object_ptr_kinds_M_eq3_h2 returns_result_select_result - wellformed_h2) + local.get_child_nodes_ok local.get_disconnected_nodes_ok + local.heap_is_wellformed_children_disc_nodes_different local.known_ptrs_known_ptr + object_ptr_kinds_M_eq3_h object_ptr_kinds_M_eq3_h2 returns_result_select_result + wellformed_h2) show False proof (cases "xb = owner_document") case True @@ -5309,11 +5334,11 @@ proof - qed then have "a_distinct_lists h'" proof(auto simp add: a_distinct_lists_def document_ptr_kinds_eq2_h3 object_ptr_kinds_M_eq2_h3 - disconnected_nodes_eq2_h3 intro!: distinct_concat_map_I)[1] + disconnected_nodes_eq2_h3 intro!: distinct_concat_map_I)[1] fix x assume 1: "distinct (concat (map (\ptr. |h3 \ get_child_nodes ptr|\<^sub>r) (sorted_list_of_set (fset (object_ptr_kinds h')))))" and - 2: "x |\| object_ptr_kinds h'" + 2: "x |\| object_ptr_kinds h'" have 3: "\p. p |\| object_ptr_kinds h' \ distinct |h3 \ get_child_nodes p|\<^sub>r" using 1 by (auto elim: distinct_concat_map_E) show "distinct |h' \ get_child_nodes x|\<^sub>r" @@ -5322,7 +5347,7 @@ proof - show ?thesis using 3[OF 2] children_h3 children_h' by(auto simp add: True insert_before_list_distinct - dest: child_not_in_any_children[unfolded children_eq_h2]) + dest: child_not_in_any_children[unfolded children_eq_h2]) next case False show ?thesis @@ -5348,9 +5373,9 @@ proof - using children_h3 children_h' child_not_in_any_children[unfolded children_eq_h2] 5 6 apply(auto simp add: True children_eq2_h3[OF \ptr \ y\])[1] by (metis (no_types, hide_lams) "3" "7" \type_wf h3\ children_eq2_h3 disjoint_iff_not_equal - get_child_nodes_ok insert_before_list_in_set known_ptrs local.known_ptrs_known_ptr - object_ptr_kinds_M_eq3_h object_ptr_kinds_M_eq3_h' - object_ptr_kinds_M_eq3_h2 returns_result_select_result select_result_I2) + get_child_nodes_ok insert_before_list_in_set known_ptrs local.known_ptrs_known_ptr + object_ptr_kinds_M_eq3_h object_ptr_kinds_M_eq3_h' + object_ptr_kinds_M_eq3_h2 returns_result_select_result select_result_I2) next case False then show ?thesis @@ -5360,10 +5385,10 @@ proof - using children_h3 children_h' child_not_in_any_children[unfolded children_eq_h2] 5 6 apply(auto simp add: True children_eq2_h3[OF \ptr \ x\])[1] by (metis (no_types, hide_lams) "2" "4" "7" IntI \known_ptrs h3\ \type_wf h'\ - children_eq_h3 empty_iff insert_before_list_in_set local.get_child_nodes_ok - local.known_ptrs_known_ptr object_ptr_kinds_M_eq3_h' - returns_result_select_result select_result_I2) - next + children_eq_h3 empty_iff insert_before_list_in_set local.get_child_nodes_ok + local.known_ptrs_known_ptr object_ptr_kinds_M_eq3_h' + returns_result_select_result select_result_I2) + next case False then show ?thesis using children_eq2_h3[OF \ptr \ x\] children_eq2_h3[OF \ptr \ y\] 5 6 7 by auto @@ -5396,13 +5421,13 @@ proof - case True show ?thesis using 6 node_not_in_disconnected_nodes 3 4 5 select_result_I2[OF children_h'] - select_result_I2[OF children_h3] True disconnected_nodes_eq2_h3 + select_result_I2[OF children_h3] True disconnected_nodes_eq2_h3 by (metis (no_types, lifting) "2" DocumentMonad.ptr_kinds_ptr_kinds_M - \a_distinct_lists h3\ \type_wf h'\ disconnected_nodes_eq_h3 - distinct_lists_no_parent document_ptr_kinds_eq2_h3 get_disconnected_nodes_ok - insert_before_list_in_set object_ptr_kinds_M_eq3_h' returns_result_select_result) + \a_distinct_lists h3\ \type_wf h'\ disconnected_nodes_eq_h3 + distinct_lists_no_parent document_ptr_kinds_eq2_h3 get_disconnected_nodes_ok + insert_before_list_in_set object_ptr_kinds_M_eq3_h' returns_result_select_result) - next + next case False then show ?thesis using 1 2 3 4 5 children_eq2_h3[OF False] by fastforce @@ -5413,33 +5438,13 @@ proof - using wellformed_h2 by (simp add: heap_is_wellformed_def) then have "a_owner_document_valid h'" apply(auto simp add: a_owner_document_valid_def object_ptr_kinds_M_eq2_h2 - object_ptr_kinds_M_eq2_h3 node_ptr_kinds_eq2_h2 node_ptr_kinds_eq2_h3 - document_ptr_kinds_eq2_h2 document_ptr_kinds_eq2_h3 children_eq2_h2)[1] + object_ptr_kinds_M_eq2_h3 node_ptr_kinds_eq2_h2 node_ptr_kinds_eq2_h3 + document_ptr_kinds_eq2_h2 document_ptr_kinds_eq2_h3 children_eq2_h2)[1] apply(auto simp add: document_ptr_kinds_eq2_h2[simplified] document_ptr_kinds_eq2_h3[simplified] - object_ptr_kinds_M_eq2_h2[simplified] object_ptr_kinds_M_eq2_h3[simplified] - node_ptr_kinds_eq2_h2[simplified] node_ptr_kinds_eq2_h3[simplified])[1] + object_ptr_kinds_M_eq2_h2[simplified] object_ptr_kinds_M_eq2_h3[simplified] + node_ptr_kinds_eq2_h2[simplified] node_ptr_kinds_eq2_h3[simplified])[1] apply(auto simp add: disconnected_nodes_eq2_h3[symmetric])[1] - proof - - fix node_ptr - assume 0: "\node_ptr. node_ptr |\| node_ptr_kinds h' - \ (\document_ptr. document_ptr |\| document_ptr_kinds h' - \ node_ptr \ set |h2 \ get_disconnected_nodes document_ptr|\<^sub>r) - \ (\parent_ptr. parent_ptr |\| object_ptr_kinds h' - \ node_ptr \ set |h3 \ get_child_nodes parent_ptr|\<^sub>r)" - and 1: "node_ptr |\| node_ptr_kinds h'" - and 2: "\parent_ptr. parent_ptr |\| object_ptr_kinds h' - \ node_ptr \ set |h' \ get_child_nodes parent_ptr|\<^sub>r" - then have "(\document_ptr. document_ptr |\| document_ptr_kinds h' - \ node_ptr \ set |h2 \ get_disconnected_nodes document_ptr|\<^sub>r)" - by (metis (no_types, lifting) children_eq2_h3 children_h' children_h3 - insert_before_list_in_set select_result_I2) - then show "\document_ptr. document_ptr |\| document_ptr_kinds h' - \ node_ptr \ set |h3 \ get_disconnected_nodes document_ptr|\<^sub>r" - by (metis (no_types, hide_lams) "2" children_h' disconnected_nodes_eq2_h2 - disconnected_nodes_h2 disconnected_nodes_h3 in_set_remove1 - insert_before_list_in_set object_ptr_kinds_M_eq3_h' - ptr_in_heap select_result_I2) - qed + by (smt children_eq2_h3 children_h' children_h3 disconnected_nodes_eq2_h2 disconnected_nodes_h2 disconnected_nodes_h3 finite_set_in in_set_remove1 insert_before_list_in_set object_ptr_kinds_M_eq3_h' ptr_in_heap select_result_I2) ultimately show "heap_is_wellformed h'" by (simp add: heap_is_wellformed_def) @@ -5844,7 +5849,7 @@ proof - using \heap_is_wellformed h\ using \cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_element_ptr \ set |h \ node_ptr_kinds_M|\<^sub>r\ a_all_ptrs_in_heap_def heap_is_wellformed_def - by (meson NodeMonad.ptr_kinds_ptr_kinds_M fset_mp fset_of_list_elem ) + using NodeMonad.ptr_kinds_ptr_kinds_M local.heap_is_wellformed_disc_nodes_in_heap by blast have "acyclic (parent_child_rel h)" using \heap_is_wellformed h\ @@ -5890,21 +5895,12 @@ proof - using \heap_is_wellformed h\ by (simp add: heap_is_wellformed_def) then have "a_all_ptrs_in_heap h2" apply(auto simp add: a_all_ptrs_in_heap_def)[1] - using node_ptr_kinds_eq_h - \cast new_element_ptr \ set |h \ node_ptr_kinds_M|\<^sub>r\ - \h2 \ get_child_nodes (cast new_element_ptr) \\<^sub>r []\ - apply (metis (no_types, hide_lams) children_eq_h fempty_iff fset_mp fset_of_list_simps(1) - funionCI select_result_I2) - by (simp add: disconnected_nodes_eq_h fset_rev_mp node_ptr_kinds_eq_h) + apply (metis \known_ptrs h2\ \parent_child_rel h = parent_child_rel h2\ \type_wf h2\ assms(1) assms(3) funion_iff local.get_child_nodes_ok local.known_ptrs_known_ptr local.parent_child_rel_child_in_heap local.parent_child_rel_child_nodes2 node_ptr_kinds_commutes node_ptr_kinds_eq_h returns_result_select_result) + by (metis assms(1) assms(3) disconnected_nodes_eq2_h document_ptr_kinds_eq_h funion_iff local.get_disconnected_nodes_ok local.heap_is_wellformed_disc_nodes_in_heap node_ptr_kinds_eq_h returns_result_select_result) then have "a_all_ptrs_in_heap h3" - by(auto simp add: a_all_ptrs_in_heap_def object_ptr_kinds_eq_h2 node_ptr_kinds_def - children_eq_h2 disconnected_nodes_eq_h2) + by (simp add: children_eq2_h2 disconnected_nodes_eq2_h2 document_ptr_kinds_eq_h2 local.a_all_ptrs_in_heap_def node_ptr_kinds_eq_h2 object_ptr_kinds_eq_h2) then have "a_all_ptrs_in_heap h'" - apply(auto simp add: a_all_ptrs_in_heap_def object_ptr_kinds_eq_h3 node_ptr_kinds_def children_eq_h3 )[1] - using disconnected_nodes_eq_h3 object_ptr_kinds_eq_h object_ptr_kinds_eq_h2 - by (metis (no_types, lifting) disc_nodes_h3 finsertCI fset.map_comp fset_mp fset_of_list_elem - funion_finsert_right h' local.set_disconnected_nodes_get_disconnected_nodes - node_ptr_kinds_def node_ptr_kinds_eq_h select_result_I2 set_ConsD) + by (smt \h2 \ get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_element_ptr) \\<^sub>r []\ children_eq2_h3 disc_nodes_document_ptr_h2 disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 document_ptr_kinds_eq_h3 finite_set_in h' is_OK_returns_result_I l_set_disconnected_nodes_get_disconnected_nodes.set_disconnected_nodes_get_disconnected_nodes local.a_all_ptrs_in_heap_def local.get_child_nodes_ptr_in_heap local.l_set_disconnected_nodes_get_disconnected_nodes_axioms node_ptr_kinds_commutes object_ptr_kinds_eq_h2 object_ptr_kinds_eq_h3 select_result_I2 set_ConsD subset_code(1)) have "\p. p |\| object_ptr_kinds h \ cast new_element_ptr \ set |h \ get_child_nodes p|\<^sub>r" using \heap_is_wellformed h\ \cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_element_ptr \ set |h \ node_ptr_kinds_M|\<^sub>r\ @@ -5973,24 +5969,8 @@ proof - ultimately show "False" apply(-) apply(cases "x = document_ptr") - apply (metis (no_types) NodeMonad.ptr_kinds_ptr_kinds_M - \a_all_ptrs_in_heap h\ - \cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_element_ptr \ set |h \ node_ptr_kinds_M|\<^sub>r\ - a_all_ptrs_in_heap_def assms(3) disc_nodes_h3 disconnected_nodes_eq2_h - disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 disjoint_iff_not_equal - document_ptr_kinds_eq_h document_ptr_kinds_eq_h2 fset_mp fset_of_list_elem - get_disconnected_nodes_ok h' returns_result_select_result select_result_I2 - set_ConsD set_disconnected_nodes_get_disconnected_nodes) - apply(cases "y = document_ptr" ) - apply (metis (no_types) NodeMonad.ptr_kinds_ptr_kinds_M - \a_all_ptrs_in_heap h\ - \cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_element_ptr \ set |h \ node_ptr_kinds_M|\<^sub>r\ - a_all_ptrs_in_heap_def assms(3) disc_nodes_h3 disconnected_nodes_eq2_h - disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 disjoint_iff_not_equal - document_ptr_kinds_eq_h document_ptr_kinds_eq_h2 fset_mp fset_of_list_elem - get_disconnected_nodes_ok h' returns_result_select_result select_result_I2 - set_ConsD set_disconnected_nodes_get_disconnected_nodes) - using disconnected_nodes_eq2_h3 by auto + apply (smt NodeMonad.ptr_kinds_ptr_kinds_M \cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_element_ptr \ set |h \ node_ptr_kinds_M|\<^sub>r\ \local.a_all_ptrs_in_heap h\ disc_nodes_h3 disconnected_nodes_eq2_h disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 disjoint_iff_not_equal document_ptr_kinds_eq_h document_ptr_kinds_eq_h2 finite_set_in h' l_set_disconnected_nodes_get_disconnected_nodes.set_disconnected_nodes_get_disconnected_nodes local.a_all_ptrs_in_heap_def local.l_set_disconnected_nodes_get_disconnected_nodes_axioms select_result_I2 set_ConsD subsetD) + by (smt NodeMonad.ptr_kinds_ptr_kinds_M \cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_element_ptr \ set |h \ node_ptr_kinds_M|\<^sub>r\ \local.a_all_ptrs_in_heap h\ disc_nodes_document_ptr_h2 disconnected_nodes_eq2_h disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 disjoint_iff_not_equal document_ptr_kinds_eq_h document_ptr_kinds_eq_h2 finite_set_in h' l_set_disconnected_nodes_get_disconnected_nodes.set_disconnected_nodes_get_disconnected_nodes local.a_all_ptrs_in_heap_def local.l_set_disconnected_nodes_get_disconnected_nodes_axioms select_result_I2 set_ConsD subsetD) next fix x xa xb assume 2: "(\x\fset (object_ptr_kinds h3). set |h' \ get_child_nodes x|\<^sub>r) @@ -6029,27 +6009,8 @@ proof - apply (metis (no_types, lifting) document_ptr_kinds_eq_h h' list.set_intros(1) local.set_disconnected_nodes_get_disconnected_nodes select_result_I2) apply(simp add: object_ptr_kinds_eq_h) - proof - - fix node_ptr :: "(_) node_ptr" - assume a1: "\node_ptr. node_ptr |\| node_ptr_kinds h \ (\document_ptr. document_ptr |\| document_ptr_kinds h \ node_ptr \ set |h \ get_disconnected_nodes document_ptr|\<^sub>r) \ (\parent_ptr. parent_ptr |\| object_ptr_kinds h \ node_ptr \ set |h \ get_child_nodes parent_ptr|\<^sub>r)" - assume a2: "node_ptr |\| node_ptr_kinds h" - assume a3: "\parent_ptr. (parent_ptr = cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_element_ptr \ node_ptr \ set |h' \ get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_element_ptr)|\<^sub>r) \ (parent_ptr |\| object_ptr_kinds h \ node_ptr \ set |h' \ get_child_nodes parent_ptr|\<^sub>r)" - assume a4: "document_ptr |\| document_ptr_kinds h" - assume a5: "h3 \ get_disconnected_nodes document_ptr \\<^sub>r disc_nodes_h3" - obtain dd :: "(_) node_ptr \ (_) document_ptr" where - "\x0. (\v1. v1 |\| document_ptr_kinds h \ x0 \ set |h \ get_disconnected_nodes v1|\<^sub>r) = (dd x0 |\| document_ptr_kinds h \ x0 \ set |h \ get_disconnected_nodes (dd x0)|\<^sub>r)" - by moura - then have f6: "dd node_ptr |\| document_ptr_kinds h \ node_ptr \ set |h \ get_disconnected_nodes (dd node_ptr)|\<^sub>r" - using a3 a2 a1 by (metis (no_types) \cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_element_ptr \ set |h \ object_ptr_kinds_M|\<^sub>r\ children_eq2_h children_eq2_h2 children_eq2_h3 l_ptr_kinds_M.ptr_kinds_ptr_kinds_M object_ptr_kinds_M_def) - moreover - { assume "|h \ get_disconnected_nodes (dd node_ptr)|\<^sub>r \ disc_nodes_h3" - then have "document_ptr \ dd node_ptr" - using a5 disconnected_nodes_eq2_h disconnected_nodes_eq2_h2 by force - then have "\d. d |\| document_ptr_kinds h2 \ node_ptr \ set |h' \ get_disconnected_nodes d|\<^sub>r" - using f6 disconnected_nodes_eq2_h disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 document_ptr_kinds_eq_h by auto } - ultimately show "\d. d |\| document_ptr_kinds h2 \ node_ptr \ set |h' \ get_disconnected_nodes d|\<^sub>r" - using a4 by (metis (no_types) document_ptr_kinds_eq_h h' insert_iff list.set(2) local.set_disconnected_nodes_get_disconnected_nodes select_result_I2) - qed + by(metis (no_types, lifting) NodeMonad.ptr_kinds_ptr_kinds_M \cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_element_ptr \ set |h \ node_ptr_kinds_M|\<^sub>r\ children_eq2_h children_eq2_h2 children_eq2_h3 disconnected_nodes_eq2_h disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 document_ptr_kinds_eq_h finite_set_in h' l_set_disconnected_nodes_get_disconnected_nodes.set_disconnected_nodes_get_disconnected_nodes list.set_intros(2) local.l_set_disconnected_nodes_get_disconnected_nodes_axioms node_ptr_kinds_commutes select_result_I2) + show "heap_is_wellformed h'" using \a_acyclic_heap h'\ \a_all_ptrs_in_heap h'\ \a_distinct_lists h'\ \a_owner_document_valid h'\ by(simp add: heap_is_wellformed_def) @@ -6321,7 +6282,7 @@ proof - then have "cast new_character_data_ptr \ set disc_nodes_h3" using \heap_is_wellformed h\ using \cast new_character_data_ptr \ set |h \ node_ptr_kinds_M|\<^sub>r\ a_all_ptrs_in_heap_def heap_is_wellformed_def - by (meson NodeMonad.ptr_kinds_ptr_kinds_M fset_mp fset_of_list_elem ) + using NodeMonad.ptr_kinds_ptr_kinds_M local.heap_is_wellformed_disc_nodes_in_heap by blast have "acyclic (parent_child_rel h)" using \heap_is_wellformed h\ @@ -6368,19 +6329,14 @@ proof - apply(auto simp add: a_all_ptrs_in_heap_def)[1] using node_ptr_kinds_eq_h \cast new_character_data_ptr \ set |h \ node_ptr_kinds_M|\<^sub>r\ \h2 \ get_child_nodes (cast new_character_data_ptr) \\<^sub>r []\ - apply (metis (no_types, hide_lams) children_eq_h fempty_iff fset_mp fset_of_list_simps(1) - funionCI select_result_I2) - by (simp add: disconnected_nodes_eq_h fset_rev_mp node_ptr_kinds_eq_h) + apply (metis (no_types, lifting) NodeMonad.ptr_kinds_ptr_kinds_M \parent_child_rel h = parent_child_rel h2\ children_eq2_h finite_set_in finsert_iff funion_finsert_right local.parent_child_rel_child local.parent_child_rel_parent_in_heap node_ptr_kinds_commutes object_ptr_kinds_eq_h select_result_I2 subsetD sup_bot.right_neutral) + by (metis assms(1) assms(3) disconnected_nodes_eq2_h document_ptr_kinds_eq_h funionI1 local.get_disconnected_nodes_ok local.heap_is_wellformed_disc_nodes_in_heap node_ptr_kinds_eq_h returns_result_select_result) + then have "a_all_ptrs_in_heap h3" - by(auto simp add: a_all_ptrs_in_heap_def object_ptr_kinds_eq_h2 node_ptr_kinds_def - children_eq_h2 disconnected_nodes_eq_h2) + by (simp add: children_eq2_h2 disconnected_nodes_eq2_h2 document_ptr_kinds_eq_h2 local.a_all_ptrs_in_heap_def node_ptr_kinds_eq_h2 object_ptr_kinds_eq_h2) then have "a_all_ptrs_in_heap h'" - apply(auto simp add: a_all_ptrs_in_heap_def object_ptr_kinds_eq_h3 node_ptr_kinds_def - children_eq_h3 )[1] - using disconnected_nodes_eq_h3 object_ptr_kinds_eq_h object_ptr_kinds_eq_h2 - by (metis (no_types, lifting) disc_nodes_h3 finsertCI fset.map_comp fset_mp fset_of_list_elem - funion_finsert_right h' local.set_disconnected_nodes_get_disconnected_nodes - node_ptr_kinds_def node_ptr_kinds_eq_h select_result_I2 set_ConsD) + by (smt character_data_ptr_kinds_commutes children_eq2_h3 disc_nodes_document_ptr_h2 disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 document_ptr_kinds_eq_h3 finite_set_in h' h2 local.a_all_ptrs_in_heap_def local.set_disconnected_nodes_get_disconnected_nodes new_character_data_ptr new_character_data_ptr_in_heap node_ptr_kinds_eq_h2 node_ptr_kinds_eq_h3 object_ptr_kinds_eq_h3 select_result_I2 set_ConsD subset_code(1)) + have "\p. p |\| object_ptr_kinds h \ cast new_character_data_ptr \ set |h \ get_child_nodes p|\<^sub>r" using \heap_is_wellformed h\ \cast new_character_data_ptr \ set |h \ node_ptr_kinds_M|\<^sub>r\ @@ -6444,25 +6400,7 @@ proof - moreover have "set |h3 \ get_disconnected_nodes x|\<^sub>r \ set |h3 \ get_disconnected_nodes y|\<^sub>r = {}" using calculation by(auto dest: distinct_concat_map_E(1)) ultimately show "False" - apply(cases "x = document_ptr") - apply (metis (no_types) NodeMonad.ptr_kinds_ptr_kinds_M \a_all_ptrs_in_heap h\ - \cast new_character_data_ptr \ set |h \ node_ptr_kinds_M|\<^sub>r\ - a_all_ptrs_in_heap_def assms(3) disc_nodes_h3 - disconnected_nodes_eq2_h disconnected_nodes_eq2_h2 - disconnected_nodes_eq2_h3 disjoint_iff_not_equal - document_ptr_kinds_eq_h document_ptr_kinds_eq_h2 fset_mp - fset_of_list_elem get_disconnected_nodes_ok h' - returns_result_select_result select_result_I2 set_ConsD - set_disconnected_nodes_get_disconnected_nodes) - apply(cases "y = document_ptr" ) - apply (metis (no_types) NodeMonad.ptr_kinds_ptr_kinds_M - \a_all_ptrs_in_heap h\ \cast new_character_data_ptr \ set |h \ node_ptr_kinds_M|\<^sub>r\ - a_all_ptrs_in_heap_def assms(3) disc_nodes_h3 disconnected_nodes_eq2_h - disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 disjoint_iff_not_equal - document_ptr_kinds_eq_h document_ptr_kinds_eq_h2 fset_mp fset_of_list_elem - get_disconnected_nodes_ok h' returns_result_select_result select_result_I2 set_ConsD - set_disconnected_nodes_get_disconnected_nodes) - using disconnected_nodes_eq2_h3 by auto + by (smt NodeMonad.ptr_kinds_ptr_kinds_M \cast\<^sub>c\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>_\<^sub>d\<^sub>a\<^sub>t\<^sub>a\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_character_data_ptr \ set |h \ node_ptr_kinds_M|\<^sub>r\ \local.a_all_ptrs_in_heap h\ disc_nodes_document_ptr_h2 disconnected_nodes_eq2_h disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 disjoint_iff_not_equal document_ptr_kinds_eq_h document_ptr_kinds_eq_h2 finite_set_in h' l_set_disconnected_nodes_get_disconnected_nodes.set_disconnected_nodes_get_disconnected_nodes local.a_all_ptrs_in_heap_def local.l_set_disconnected_nodes_get_disconnected_nodes_axioms select_result_I2 set_ConsD subsetD) next fix x xa xb assume 2: "(\x\fset (object_ptr_kinds h3). set |h' \ get_child_nodes x|\<^sub>r) @@ -6498,10 +6436,8 @@ proof - apply (metis (no_types, lifting) document_ptr_kinds_eq_h h' list.set_intros(1) local.set_disconnected_nodes_get_disconnected_nodes select_result_I2) apply(simp add: object_ptr_kinds_eq_h) - by (metis (no_types, lifting) ObjectMonad.ptr_kinds_ptr_kinds_M - \cast\<^sub>c\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>_\<^sub>d\<^sub>a\<^sub>t\<^sub>a\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_character_data_ptr \ set |h \ object_ptr_kinds_M|\<^sub>r\ - children_eq2_h disconnected_nodes_eq2_h3 document_ptr_kinds_eq_h h' list.set_intros(2) - local.set_disconnected_nodes_get_disconnected_nodes select_result_I2) + by (metis (mono_tags, lifting) \cast\<^sub>c\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>_\<^sub>d\<^sub>a\<^sub>t\<^sub>a\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_character_data_ptr \ set |h \ object_ptr_kinds_M|\<^sub>r\ children_eq2_h disconnected_nodes_eq2_h3 document_ptr_kinds_eq_h finite_set_in h' l_ptr_kinds_M.ptr_kinds_ptr_kinds_M l_set_disconnected_nodes_get_disconnected_nodes.set_disconnected_nodes_get_disconnected_nodes list.set_intros(2) local.l_set_disconnected_nodes_get_disconnected_nodes_axioms object_ptr_kinds_M_def select_result_I2) + show "heap_is_wellformed h'" using \a_acyclic_heap h'\ \a_all_ptrs_in_heap h'\ \a_distinct_lists h'\ \a_owner_document_valid h'\ @@ -6610,7 +6546,7 @@ proof - "\doc_ptr disc_nodes. doc_ptr \ new_document_ptr \ h \ get_disconnected_nodes doc_ptr \\<^sub>r disc_nodes = h' \ get_disconnected_nodes doc_ptr \\<^sub>r disc_nodes" using get_disconnected_nodes_reads h' get_disconnected_nodes_new_document_different_pointers new_document_ptr - apply(auto simp add: reads_def reflp_def transp_def preserved_def)[1] + apply(auto simp add: reads_def reflp_def transp_def preserved_def)[1] by (metis(full_types) \\thesis. (\new_document_ptr. \h \ new_document \\<^sub>r new_document_ptr; h \ new_document \\<^sub>h h'\ \ thesis) \ thesis\ local.get_disconnected_nodes_new_document_different_pointers new_document_ptr)+ @@ -6662,19 +6598,13 @@ proof - using \heap_is_wellformed h\ by (simp add: heap_is_wellformed_def) then have "a_all_ptrs_in_heap h'" apply(auto simp add: a_all_ptrs_in_heap_def)[1] - apply (metis ObjectMonad.ptr_kinds_ptr_kinds_M - \cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_document_ptr \ set |h \ object_ptr_kinds_M|\<^sub>r\ - \parent_child_rel h = parent_child_rel h'\ assms(1) children_eq fset_of_list_elem - local.heap_is_wellformed_children_in_heap local.parent_child_rel_child - local.parent_child_rel_parent_in_heap node_ptr_kinds_eq) - by (metis (no_types, lifting) ObjectMonad.ptr_kinds_ptr_kinds_M - \cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_document_ptr \ set |h \ object_ptr_kinds_M|\<^sub>r\ - \h' \ get_child_nodes (cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_document_ptr) \\<^sub>r []\ - \parent_child_rel h = parent_child_rel h'\ assms(1) disconnected_nodes_eq_h - fset_of_list_elem h' local.heap_is_wellformed_disc_nodes_in_heap - local.new_document_no_disconnected_nodes local.parent_child_rel_child - local.parent_child_rel_parent_in_heap new_document_ptr node_ptr_kinds_eq - select_result_I2) + using ObjectMonad.ptr_kinds_ptr_kinds_M + \cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_document_ptr \ set |h \ object_ptr_kinds_M|\<^sub>r\ + \parent_child_rel h = parent_child_rel h'\ assms(1) children_eq fset_of_list_elem + local.heap_is_wellformed_children_in_heap local.parent_child_rel_child + local.parent_child_rel_parent_in_heap node_ptr_kinds_eq + apply (metis (no_types, lifting) \h' \ get_child_nodes (cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_document_ptr) \\<^sub>r []\ children_eq2 finite_set_in finsert_iff funion_finsert_right object_ptr_kinds_eq select_result_I2 subsetD sup_bot.right_neutral) + by (metis (no_types, lifting) \cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_document_ptr |\| object_ptr_kinds h\ \h' \ get_child_nodes (cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_document_ptr) \\<^sub>r []\ \h' \ get_disconnected_nodes new_document_ptr \\<^sub>r []\ \parent_child_rel h = parent_child_rel h'\ \type_wf h'\ assms(1) disconnected_nodes_eq_h local.get_disconnected_nodes_ok local.heap_is_wellformed_disc_nodes_in_heap local.parent_child_rel_child local.parent_child_rel_parent_in_heap node_ptr_kinds_eq returns_result_select_result select_result_I2) have "a_distinct_lists h" using \heap_is_wellformed h\ @@ -6743,12 +6673,7 @@ proof - using \heap_is_wellformed h\ by (simp add: heap_is_wellformed_def) then have "a_owner_document_valid h'" apply(auto simp add: a_owner_document_valid_def)[1] - by (metis \cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_document_ptr |\| object_ptr_kinds h\ - \new_document_ptr |\| document_ptr_kinds h\ assms(3) assms(4) children_eq - children_eq2 disconnected_nodes_eq2_h disconnected_nodes_eq_h - is_OK_returns_result_E is_OK_returns_result_I local.get_child_nodes_ok - local.get_child_nodes_ptr_in_heap local.get_disconnected_nodes_ok - local.get_disconnected_nodes_ptr_in_heap local.known_ptrs_known_ptr node_ptr_kinds_eq) + by (metis \cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_document_ptr |\| object_ptr_kinds h\ children_eq2 disconnected_nodes_eq2_h document_ptr_kinds_commutes finite_set_in funion_iff node_ptr_kinds_eq object_ptr_kinds_eq) show "heap_is_wellformed h'" using \a_acyclic_heap h'\ \a_all_ptrs_in_heap h'\ \a_distinct_lists h'\ \a_owner_document_valid h'\ diff --git a/Core_DOM/classes/CharacterDataClass.thy b/Core_DOM/classes/CharacterDataClass.thy index 47b34a0..cf0ee61 100644 --- a/Core_DOM/classes/CharacterDataClass.thy +++ b/Core_DOM/classes/CharacterDataClass.thy @@ -139,8 +139,8 @@ begin definition a_type_wf :: "(_) heap \ bool" where "a_type_wf h = (ElementClass.type_wf h - \ (\character_data_ptr. character_data_ptr |\| character_data_ptr_kinds h - \ get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a character_data_ptr h \ None))" + \ (\character_data_ptr \ fset (character_data_ptr_kinds h). + get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a character_data_ptr h \ None))" end global_interpretation l_type_wf_def\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a defines type_wf = a_type_wf . lemmas type_wf_defs = a_type_wf_def @@ -163,8 +163,7 @@ lemma get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub> \ get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a character_data_ptr h \ None" using l_type_wf\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_axioms assms apply(simp add: type_wf_defs get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def l_type_wf\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def) - by (metis NodeClass.get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_type_wf bind_eq_None_conv character_data_ptr_kinds_commutes - l_type_wf\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def local.l_type_wf\<^sub>N\<^sub>o\<^sub>d\<^sub>e_axioms option.distinct(1)) + by (metis assms bind.bind_lzero character_data_ptr_kinds_commutes fmember.rep_eq local.get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_type_wf option.exhaust option.simps(3)) end global_interpretation l_get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_lemmas type_wf @@ -325,17 +324,18 @@ locale l_known_ptrs\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^su begin definition a_known_ptrs :: "(_) heap \ bool" where - "a_known_ptrs h = (\ptr. ptr |\| object_ptr_kinds h \ known_ptr ptr)" + "a_known_ptrs h = (\ptr \ fset (object_ptr_kinds h). known_ptr ptr)" lemma known_ptrs_known_ptr: "a_known_ptrs h \ ptr |\| object_ptr_kinds h \ known_ptr ptr" - by(simp add: a_known_ptrs_def) + apply(simp add: a_known_ptrs_def) + using notin_fset by fastforce lemma known_ptrs_preserved: "object_ptr_kinds h = object_ptr_kinds h' \ a_known_ptrs h = a_known_ptrs h'" by(auto simp add: a_known_ptrs_def) lemma known_ptrs_subset: "object_ptr_kinds h' |\| object_ptr_kinds h \ a_known_ptrs h \ a_known_ptrs h'" - by(auto simp add: a_known_ptrs_def) + by(simp add: a_known_ptrs_def less_eq_fset.rep_eq subsetD) lemma known_ptrs_new_ptr: "object_ptr_kinds h' = object_ptr_kinds h |\| {|new_ptr|} \ known_ptr new_ptr \ a_known_ptrs h \ a_known_ptrs h'" by(simp add: a_known_ptrs_def) end diff --git a/Core_DOM/classes/DocumentClass.thy b/Core_DOM/classes/DocumentClass.thy index 64cbc1f..84a1990 100644 --- a/Core_DOM/classes/DocumentClass.thy +++ b/Core_DOM/classes/DocumentClass.thy @@ -115,7 +115,7 @@ begin definition a_type_wf :: "(_) heap \ bool" where "a_type_wf h = (CharacterDataClass.type_wf h \ - (\document_ptr. document_ptr |\| document_ptr_kinds h \ get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr h \ None))" + (\document_ptr \ fset (document_ptr_kinds h). get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr h \ None))" end global_interpretation l_type_wf_def\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t defines type_wf = a_type_wf . lemmas type_wf_defs = a_type_wf_def @@ -135,8 +135,7 @@ lemma get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_type_w shows "document_ptr |\| document_ptr_kinds h \ get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr h \ None" using l_type_wf\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_axioms assms apply(simp add: type_wf_defs get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def l_type_wf\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def) - by (metis bind_eq_None_conv document_ptr_kinds_commutes local.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf - option.distinct(1)) + by (metis document_ptr_kinds_commutes fmember.rep_eq is_none_bind is_none_simps(1) is_none_simps(2) local.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf) end global_interpretation l_get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_lemmas type_wf by unfold_locales @@ -228,7 +227,7 @@ abbreviation definition new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t :: "(_)heap \ ((_) document_ptr \ (_) heap)" where "new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = - (let new_document_ptr = document_ptr.Ref (Suc (fMax (document_ptr.the_ref |`| (document_ptrs h)))) + (let new_document_ptr = document_ptr.Ref (Suc (fMax (finsert 0 (document_ptr.the_ref |`| (document_ptrs h))))) in (new_document_ptr, put new_document_ptr (create_document_obj '''' None []) h))" @@ -315,17 +314,18 @@ locale l_known_ptrs\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^su begin definition a_known_ptrs :: "(_) heap \ bool" where - "a_known_ptrs h = (\ptr. ptr |\| object_ptr_kinds h \ known_ptr ptr)" + "a_known_ptrs h = (\ptr \ fset (object_ptr_kinds h). known_ptr ptr)" lemma known_ptrs_known_ptr: "a_known_ptrs h \ ptr |\| object_ptr_kinds h \ known_ptr ptr" - by(simp add: a_known_ptrs_def) + apply(simp add: a_known_ptrs_def) + using notin_fset by fastforce lemma known_ptrs_preserved: "object_ptr_kinds h = object_ptr_kinds h' \ a_known_ptrs h = a_known_ptrs h'" by(auto simp add: a_known_ptrs_def) lemma known_ptrs_subset: "object_ptr_kinds h' |\| object_ptr_kinds h \ a_known_ptrs h \ a_known_ptrs h'" - by(auto simp add: a_known_ptrs_def) + by(simp add: a_known_ptrs_def less_eq_fset.rep_eq subsetD) lemma known_ptrs_new_ptr: "object_ptr_kinds h' = object_ptr_kinds h |\| {|new_ptr|} \ known_ptr new_ptr \ a_known_ptrs h \ a_known_ptrs h'" by(simp add: a_known_ptrs_def) end diff --git a/Core_DOM/classes/ElementClass.thy b/Core_DOM/classes/ElementClass.thy index 1d45ac8..d7f624d 100644 --- a/Core_DOM/classes/ElementClass.thy +++ b/Core_DOM/classes/ElementClass.thy @@ -131,8 +131,8 @@ locale l_type_wf_def\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t begin definition a_type_wf :: "(_) heap \ bool" where - "a_type_wf h = (NodeClass.type_wf h \ (\element_ptr. element_ptr |\| element_ptr_kinds h - \ get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr h \ None))" + "a_type_wf h = (NodeClass.type_wf h \ (\element_ptr \ fset (element_ptr_kinds h). + get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr h \ None))" end global_interpretation l_type_wf_def\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t defines type_wf = a_type_wf . lemmas type_wf_defs = a_type_wf_def @@ -154,8 +154,8 @@ lemma get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_type_wf: shows "element_ptr |\| element_ptr_kinds h \ get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr h \ None" using l_type_wf\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_axioms assms apply(simp add: type_wf_defs get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def l_type_wf\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def) - by (metis NodeClass.get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_type_wf bind_eq_None_conv element_ptr_kinds_commutes - option.distinct(1)) + by (metis NodeClass.get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_type_wf bind_eq_None_conv element_ptr_kinds_commutes notin_fset + option.distinct(1)) end global_interpretation l_get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_lemmas type_wf @@ -290,16 +290,17 @@ locale l_known_ptrs\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t = l_ begin definition a_known_ptrs :: "(_) heap \ bool" where - "a_known_ptrs h = (\ptr. ptr |\| object_ptr_kinds h \ known_ptr ptr)" + "a_known_ptrs h = (\ptr \ fset (object_ptr_kinds h). known_ptr ptr)" lemma known_ptrs_known_ptr: "ptr |\| object_ptr_kinds h \ a_known_ptrs h \ known_ptr ptr" - by(simp add: a_known_ptrs_def) + apply(simp add: a_known_ptrs_def) + using notin_fset by fastforce lemma known_ptrs_preserved: "object_ptr_kinds h = object_ptr_kinds h' \ a_known_ptrs h = a_known_ptrs h'" by(auto simp add: a_known_ptrs_def) lemma known_ptrs_subset: "object_ptr_kinds h' |\| object_ptr_kinds h \ a_known_ptrs h \ a_known_ptrs h'" - by(auto simp add: a_known_ptrs_def) + by(simp add: a_known_ptrs_def less_eq_fset.rep_eq subsetD) lemma known_ptrs_new_ptr: "object_ptr_kinds h' = object_ptr_kinds h |\| {|new_ptr|} \ known_ptr new_ptr \ a_known_ptrs h \ a_known_ptrs h'" by(simp add: a_known_ptrs_def) end diff --git a/Core_DOM/classes/NodeClass.thy b/Core_DOM/classes/NodeClass.thy index e132a30..5670183 100644 --- a/Core_DOM/classes/NodeClass.thy +++ b/Core_DOM/classes/NodeClass.thy @@ -89,8 +89,7 @@ begin definition a_type_wf :: "(_) heap \ bool" where "a_type_wf h = (ObjectClass.type_wf h - \ (\node_ptr. node_ptr |\| node_ptr_kinds h - \ get\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr h \ None))" + \ (\node_ptr \ fset( node_ptr_kinds h). get\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr h \ None))" end global_interpretation l_type_wf_def\<^sub>N\<^sub>o\<^sub>d\<^sub>e defines type_wf = a_type_wf . lemmas type_wf_defs = a_type_wf_def @@ -110,9 +109,8 @@ lemma get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_type_wf: shows "node_ptr |\| node_ptr_kinds h \ get\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr h \ None" using l_type_wf\<^sub>N\<^sub>o\<^sub>d\<^sub>e_axioms assms apply(simp add: type_wf_defs get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def l_type_wf\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def) - by (metis (mono_tags, lifting) bind_eq_None_conv ffmember_filter fimage_eqI - is_node_ptr_kind_cast get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf local.l_type_wf\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_axioms - node_ptr_casts_commute2 node_ptr_kinds_def option.sel option.simps(3)) + by (metis bind_eq_None_conv ffmember_filter fimage_eqI fmember.rep_eq is_node_ptr_kind_cast + get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf node_ptr_casts_commute2 node_ptr_kinds_def option.sel option.simps(3)) end global_interpretation l_get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_lemmas type_wf @@ -177,15 +175,15 @@ locale l_known_ptrs\<^sub>N\<^sub>o\<^sub>d\<^sub>e = l_known_ptr known_ptr for begin definition a_known_ptrs :: "(_) heap \ bool" where - "a_known_ptrs h = (\ptr. ptr |\| object_ptr_kinds h \ known_ptr ptr)" + "a_known_ptrs h = (\ptr \ fset (object_ptr_kinds h). known_ptr ptr)" lemma known_ptrs_known_ptr: "a_known_ptrs h \ ptr |\| object_ptr_kinds h \ known_ptr ptr" - by(simp add: a_known_ptrs_def) - + apply(simp add: a_known_ptrs_def) + using notin_fset by fastforce lemma known_ptrs_preserved: "object_ptr_kinds h = object_ptr_kinds h' \ a_known_ptrs h = a_known_ptrs h'" by(auto simp add: a_known_ptrs_def) lemma known_ptrs_subset: "object_ptr_kinds h' |\| object_ptr_kinds h \ a_known_ptrs h \ a_known_ptrs h'" - by(auto simp add: a_known_ptrs_def) + by(simp add: a_known_ptrs_def less_eq_fset.rep_eq subsetD) lemma known_ptrs_new_ptr: "object_ptr_kinds h' = object_ptr_kinds h |\| {|new_ptr|} \ known_ptr new_ptr \ a_known_ptrs h \ a_known_ptrs h'" by(simp add: a_known_ptrs_def) end diff --git a/Core_DOM/classes/ObjectClass.thy b/Core_DOM/classes/ObjectClass.thy index e080277..d7cbeb9 100644 --- a/Core_DOM/classes/ObjectClass.thy +++ b/Core_DOM/classes/ObjectClass.thy @@ -134,16 +134,17 @@ locale l_known_ptrs\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t = l_known_pt begin definition a_known_ptrs :: "(_) heap \ bool" where - "a_known_ptrs h = (\ptr. ptr |\| object_ptr_kinds h \ known_ptr ptr)" + "a_known_ptrs h = (\ptr \ fset (object_ptr_kinds h). known_ptr ptr)" lemma known_ptrs_known_ptr: "a_known_ptrs h \ ptr |\| object_ptr_kinds h \ known_ptr ptr" - by(simp add: a_known_ptrs_def) + apply(simp add: a_known_ptrs_def) + using notin_fset by fastforce lemma known_ptrs_preserved: "object_ptr_kinds h = object_ptr_kinds h' \ a_known_ptrs h = a_known_ptrs h'" by(auto simp add: a_known_ptrs_def) lemma known_ptrs_subset: "object_ptr_kinds h' |\| object_ptr_kinds h \ a_known_ptrs h \ a_known_ptrs h'" - by(auto simp add: a_known_ptrs_def) + by(simp add: a_known_ptrs_def less_eq_fset.rep_eq subsetD) lemma known_ptrs_new_ptr: "object_ptr_kinds h' = object_ptr_kinds h |\| {|new_ptr|} \ known_ptr new_ptr \ a_known_ptrs h \ a_known_ptrs h'" by(simp add: a_known_ptrs_def) end @@ -192,4 +193,24 @@ lemma delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_ok: using assms by(auto simp add: delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def object_ptr_kinds_def split: if_splits) + +subsection \Code Generator Setup\ + +definition "create_heap xs = Heap (fmap_of_list xs)" + +code_datatype ObjectClass.heap.Heap create_heap + +lemma object_ptr_kinds_code3 [code]: + "fmlookup (the_heap (create_heap xs)) x = map_of xs x" + by(auto simp add: create_heap_def fmlookup_of_list) + +lemma object_ptr_kinds_code4 [code]: + "the_heap (create_heap xs) = fmap_of_list xs" + by(simp add: create_heap_def) + +lemma object_ptr_kinds_code5 [code]: + "the_heap (Heap x) = x" + by simp + + end diff --git a/Core_DOM/monads/CharacterDataMonad.thy b/Core_DOM/monads/CharacterDataMonad.thy index 4e84b4f..1cf3130 100644 --- a/Core_DOM/monads/CharacterDataMonad.thy +++ b/Core_DOM/monads/CharacterDataMonad.thy @@ -307,8 +307,9 @@ lemma type_wf_put_ptr_not_in_heap_E: assumes "ptr |\| object_ptr_kinds h" shows "type_wf h" using assms - by(auto simp add: type_wf_defs elim!: ElementMonad.type_wf_put_ptr_not_in_heap_E + apply(auto simp add: type_wf_defs elim!: ElementMonad.type_wf_put_ptr_not_in_heap_E split: option.splits if_splits) + using assms(2) node_ptr_kinds_commutes by blast lemma type_wf_put_ptr_in_heap_E: assumes "type_wf (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)" @@ -318,14 +319,7 @@ lemma type_wf_put_ptr_in_heap_E: shows "type_wf h" using assms apply(auto simp add: type_wf_defs split: option.splits if_splits)[1] - apply(case_tac "x2 = cast character_data_ptr") - apply(auto)[1] - apply(drule_tac x=character_data_ptr in allE) - apply(simp) - apply (metis (no_types, lifting) ElementClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf assms(2) bind.bind_lunit - cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_inv cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def - get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def option.exhaust_sel) - by(blast) + by (metis (no_types, lifting) ElementClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf assms(2) bind.bind_lunit cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_inv cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def notin_fset option.collapse) subsection\Preserving Types\ @@ -364,8 +358,9 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_tag_type_typ apply(auto simp add: is_node_kind_def type_wf_defs ElementClass.type_wf_defs NodeClass.type_wf_defs ElementMonad.get_M_defs split: option.splits)[1] using ObjectMonad.type_wf_put_ptr_in_heap_E ObjectMonad.type_wf_put_ptr_not_in_heap_E apply blast - apply (metis (mono_tags, lifting) bind_eq_Some_conv get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def option.exhaust_sel) - by (metis (no_types, lifting) option.exhaust_sel ) + apply (metis (no_types, lifting) bind_eq_Some_conv finite_set_in get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def) + apply (metis finite_set_in) + done lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_child_nodes_type_wf_preserved [simp]: @@ -390,9 +385,9 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_child_nodes_ NodeClass.type_wf_defs ElementMonad.get_M_defs split: option.splits)[1] using ObjectMonad.type_wf_put_ptr_in_heap_E ObjectMonad.type_wf_put_ptr_not_in_heap_E apply blast - apply (metis (mono_tags, lifting) ElementMonad.a_get_M_def bind_eq_Some_conv error_returns_result - get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get_heap_returns_result option.exhaust_sel option.simps(4)) - by (metis (no_types, lifting) option.exhaust_sel) + apply (metis (no_types, lifting) bind_eq_Some_conv finite_set_in get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def) + apply (metis finite_set_in) + done lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_attrs_type_wf_preserved [simp]: "h \ put_M element_ptr attrs_update v \\<^sub>h h' \ type_wf h = type_wf h'" @@ -412,8 +407,9 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_attrs_type_w apply(auto simp add: is_node_kind_def type_wf_defs ElementClass.type_wf_defs NodeClass.type_wf_defs ElementMonad.get_M_defs split: option.splits)[1] using ObjectMonad.type_wf_put_ptr_in_heap_E ObjectMonad.type_wf_put_ptr_not_in_heap_E apply blast - apply (metis (mono_tags, lifting) ElementMonad.a_get_M_def bind_eq_Some_conv error_returns_result get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get_heap_returns_result option.exhaust_sel option.simps(4)) - by (metis (no_types, lifting) option.exhaust_sel) + apply (metis (no_types, lifting) bind_eq_Some_conv finite_set_in get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def) + apply (metis finite_set_in) + done lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_shadow_root_opt_type_wf_preserved [simp]: "h \ put_M element_ptr shadow_root_opt_update v \\<^sub>h h' \ type_wf h = type_wf h'" @@ -433,8 +429,9 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_shadow_root_ apply(auto simp add: is_node_kind_def type_wf_defs ElementClass.type_wf_defs NodeClass.type_wf_defs ElementMonad.get_M_defs split: option.splits)[1] using ObjectMonad.type_wf_put_ptr_in_heap_E ObjectMonad.type_wf_put_ptr_not_in_heap_E apply blast - apply (metis (mono_tags, lifting) bind_eq_Some_conv get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def) - by (metis (no_types, lifting) option.exhaust_sel) + apply (metis (no_types, lifting) bind_eq_Some_conv finite_set_in get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def) + apply (metis finite_set_in) + done lemma new_character_data_type_wf_preserved [simp]: @@ -469,8 +466,9 @@ lemma put_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^su NodeClass.type_wf_defs CharacterDataMonad.get_M_defs ObjectClass.a_type_wf_def split: option.splits)[1] - apply (metis (no_types, lifting) bind_eq_Some_conv get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def) - by metis + apply (metis (no_types, lifting) bind_eq_Some_conv finite_set_in get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def) + apply (metis finite_set_in) + done lemma character_data_ptr_kinds_small: assumes "\object_ptr. preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h'" @@ -528,8 +526,6 @@ lemma type_wf_drop: "type_wf h \ type_wf (Heap (fmdrop ptr (the_ apply(auto simp add: type_wf_def ElementMonad.type_wf_drop l_type_wf_def\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a.a_type_wf_def)[1] using type_wf_drop - by (metis (no_types, lifting) ElementClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf character_data_ptr_kinds_commutes - fmlookup_drop get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def heap.sel - node_ptr_kinds_commutes) + by (metis (no_types, lifting) ElementClass.type_wf\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ObjectClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf character_data_ptr_kinds_commutes finite_set_in fmlookup_drop get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def node_ptr_kinds_commutes object_ptr_kinds_code5) end \ No newline at end of file diff --git a/Core_DOM/monads/DocumentMonad.thy b/Core_DOM/monads/DocumentMonad.thy index 695f39d..72f8538 100644 --- a/Core_DOM/monads/DocumentMonad.thy +++ b/Core_DOM/monads/DocumentMonad.thy @@ -322,8 +322,7 @@ lemma type_wf_put_ptr_in_heap_E: using assms apply(auto simp add: type_wf_defs elim!: CharacterDataMonad.type_wf_put_ptr_in_heap_E split: option.splits if_splits)[1] - by (metis (no_types, lifting) CharacterDataClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf bind.bind_lunit get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def - is_document_kind_def option.collapse) + by (metis (no_types, lifting) CharacterDataClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf bind.bind_lunit get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def is_document_kind_def notin_fset option.exhaust_sel) @@ -361,9 +360,8 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_tag_type_typ apply(auto simp add: is_node_kind_def type_wf_defs ElementClass.type_wf_defs NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs CharacterDataClass.type_wf_defs split: option.splits)[1] - apply (metis (no_types, lifting) Option.bind_cong bind_rzero - get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def option.distinct(1)) - by metis + apply (metis NodeClass.a_type_wf_def NodeClass.get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_type_wf ObjectClass.a_type_wf_def bind.bind_lzero finite_set_in get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def l_type_wf_def\<^sub>N\<^sub>o\<^sub>d\<^sub>e.a_type_wf_def option.collapse option.distinct(1) option.simps(3)) + by (metis fmember.rep_eq) lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_child_nodes_type_wf_preserved [simp]: "h \ put_M element_ptr child_nodes_update v \\<^sub>h h' \ type_wf h = type_wf h'" @@ -378,8 +376,8 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_child_nodes_ apply(auto simp add: is_node_kind_def type_wf_defs ElementClass.type_wf_defs NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs CharacterDataClass.type_wf_defs split: option.splits)[1] - apply (metis (no_types, lifting) Option.bind_cong bind_rzero get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def option.distinct(1)) - by metis + apply (metis NodeClass.a_type_wf_def NodeClass.get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_type_wf ObjectClass.a_type_wf_def bind.bind_lzero finite_set_in get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def l_type_wf_def\<^sub>N\<^sub>o\<^sub>d\<^sub>e.a_type_wf_def option.collapse option.distinct(1) option.simps(3)) + by (metis fmember.rep_eq) lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_attrs_type_wf_preserved [simp]: "h \ put_M element_ptr attrs_update v \\<^sub>h h' \ type_wf h = type_wf h'" @@ -394,8 +392,8 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_attrs_type_w apply(auto simp add: is_node_kind_def type_wf_defs ElementClass.type_wf_defs NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs CharacterDataClass.type_wf_defs split: option.splits)[1] - apply (metis (no_types, lifting) Option.bind_cong bind_rzero get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def option.distinct(1)) - by metis + apply (metis NodeClass.a_type_wf_def NodeClass.get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_type_wf ObjectClass.a_type_wf_def bind.bind_lzero finite_set_in get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def l_type_wf_def\<^sub>N\<^sub>o\<^sub>d\<^sub>e.a_type_wf_def option.collapse option.distinct(1) option.simps(3)) + by (metis fmember.rep_eq) lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_shadow_root_opt_type_wf_preserved [simp]: "h \ put_M element_ptr shadow_root_opt_update v \\<^sub>h h' \ type_wf h = type_wf h'" @@ -410,8 +408,8 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_shadow_root_ apply(auto simp add: is_node_kind_def type_wf_defs ElementClass.type_wf_defs NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs CharacterDataClass.type_wf_defs split: option.splits)[1] - apply (metis (no_types, lifting) Option.bind_cong bind_rzero get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def option.distinct(1)) - by metis + apply (metis NodeClass.a_type_wf_def NodeClass.get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_type_wf ObjectClass.a_type_wf_def bind.bind_lzero finite_set_in get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def l_type_wf_def\<^sub>N\<^sub>o\<^sub>d\<^sub>e.a_type_wf_def option.collapse option.distinct(1) option.simps(3)) + by (metis fmember.rep_eq) lemma new_character_data_type_wf_preserved [simp]: "h \ new_character_data \\<^sub>h h' \ type_wf h = type_wf h'" @@ -440,13 +438,11 @@ lemma put_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^su intro!: type_wf_put_I CharacterDataMonad.type_wf_put_I ElementMonad.type_wf_put_I NodeMonad.type_wf_put_I ObjectMonad.type_wf_put_I)[1] apply(auto simp add: is_node_kind_def type_wf_defs ElementClass.type_wf_defs - NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs + NodeClass.type_wf_defs CharacterDataMonad.get_M_defs ObjectClass.type_wf_defs CharacterDataClass.type_wf_defs split: option.splits)[1] - apply (metis (no_types, lifting) CharacterDataMonad.a_get_M_def bind_eq_None_conv - error_returns_result get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def get_heap_returns_result option.exhaust_sel - option.simps(4)) - by (metis (no_types, lifting) CharacterDataMonad.a_get_M_def error_returns_result - get_heap_returns_result option.exhaust_sel option.simps(4)) + apply (metis bind.bind_lzero finite_set_in get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def option.distinct(1) option.exhaust_sel) + by (metis finite_set_in) + lemma new_document_type_wf_preserved [simp]: "h \ new_document \\<^sub>h h' \ type_wf h = type_wf h'" apply(auto simp add: new_document_def new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def @@ -457,10 +453,13 @@ lemma new_document_type_wf_preserved [simp]: "h \ new_document \D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ptr_not_in_heap) + using document_ptrs_def apply fastforce + apply (simp add: is_document_kind_def) + apply (metis Suc_n_not_le_n document_ptr.sel(1) document_ptrs_def fMax_ge ffmember_filter fimage_eqI is_document_ptr_ref) + done locale l_new_document = l_type_wf + assumes new_document_types_preserved: "h \ new_document \\<^sub>h h' \ type_wf h = type_wf h'" @@ -500,7 +499,7 @@ lemma put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_doct NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs CharacterDataClass.type_wf_defs split: option.splits)[1] apply(auto simp add: get_M_defs) - by (metis (no_types, lifting) error_returns_result option.exhaust_sel option.simps(4)) + by (metis (mono_tags) error_returns_result finite_set_in option.exhaust_sel option.simps(4)) lemma put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_document_element_type_wf_preserved [simp]: "h \ put_M document_ptr document_element_update v \\<^sub>h h' \ type_wf h = type_wf h'" @@ -519,9 +518,9 @@ lemma put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_docu NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs CharacterDataClass.type_wf_defs split: option.splits)[1] - by (metis) + by (metis finite_set_in) -lemma put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_disconnected_nodes_type_wf_preserved [simp]: +lemma put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_disconnected_nodes_type_wf_preserved [simp]: "h \ put_M document_ptr disconnected_nodes_update v \\<^sub>h h' \ type_wf h = type_wf h'" apply(auto simp add: put_M_defs put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def DocumentClass.type_wf\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a @@ -538,7 +537,7 @@ lemma put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_disc apply(auto simp add: is_document_kind_def get_M_defs type_wf_defs ElementClass.type_wf_defs NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs CharacterDataClass.type_wf_defs split: option.splits)[1] - by (metis) + by (metis finite_set_in) lemma document_ptr_kinds_small: assumes "\object_ptr. preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h'" @@ -600,6 +599,5 @@ lemma type_wf_drop: "type_wf h \ type_wf (Heap (fmdrop ptr (the_ apply(auto simp add: type_wf_defs)[1] using type_wf_drop apply blast - by (metis (mono_tags, lifting) comp_apply document_ptr_kinds_commutes ffmember_filter fmdom_filter - fmfilter_alt_defs(1) fmlookup_drop get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def heap.sel object_ptr_kinds_def) + by (metis (no_types, lifting) CharacterDataClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf CharacterDataMonad.type_wf_drop document_ptr_kinds_commutes finite_set_in fmlookup_drop get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def heap.sel) end diff --git a/Core_DOM/monads/ElementMonad.thy b/Core_DOM/monads/ElementMonad.thy index 72870f7..7646666 100644 --- a/Core_DOM/monads/ElementMonad.thy +++ b/Core_DOM/monads/ElementMonad.thy @@ -298,8 +298,9 @@ lemma type_wf_put_ptr_not_in_heap_E: assumes "ptr |\| object_ptr_kinds h" shows "type_wf h" using assms - by(auto simp add: type_wf_defs elim!: NodeMonad.type_wf_put_ptr_not_in_heap_E + apply(auto simp add: type_wf_defs elim!: NodeMonad.type_wf_put_ptr_not_in_heap_E split: option.splits if_splits) + using assms(2) node_ptr_kinds_commutes by blast lemma type_wf_put_ptr_in_heap_E: assumes "type_wf (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)" @@ -309,12 +310,9 @@ lemma type_wf_put_ptr_in_heap_E: shows "type_wf h" using assms apply(auto simp add: type_wf_defs split: option.splits if_splits)[1] - apply(case_tac "x2 = cast element_ptr") - apply(drule_tac x=element_ptr in allE) - apply(auto)[1] - apply(metis (no_types, lifting) NodeClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf assms(2) bind.bind_lunit - cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_inv cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def option.exhaust_sel) - by(auto) + by (metis (no_types, lifting) NodeClass.l_get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_lemmas_axioms assms(2) bind.bind_lunit + cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_inv cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv finite_set_in get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def + l_get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_lemmas.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf option.collapse) subsection\Preserving Types\ @@ -323,13 +321,14 @@ lemma new_element_type_wf_preserved [simp]: "h \ new_element \E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def split: prod.splits if_splits elim!: bind_returns_heap_E)[1] - apply (metis element_ptr_kinds_commutes element_ptrs_def fempty_iff ffmember_filter - is_element_ptr_ref) - using element_ptrs_def apply fastforce - apply (metis (mono_tags, hide_lams) Suc_n_not_le_n element_ptr.sel(1) element_ptr_kinds_commutes - element_ptrs_def fMax_ge ffmember_filter fimageI is_element_ptr_ref) - by (metis (no_types, lifting) fMax_finsert fempty_iff fimage_is_fempty max_0L new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def - new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ptr_not_in_heap) + apply (metis element_ptr_kinds_commutes element_ptrs_def fempty_iff ffmember_filter finite_set_in + is_element_ptr_ref) + apply (metis element_ptrs_def fempty_iff ffmember_filter finite_set_in is_element_ptr_ref) + apply (metis (no_types, lifting) Suc_n_not_le_n element_ptr.sel(1) element_ptr_kinds_commutes + element_ptrs_def fMax_ge ffmember_filter fimage_eqI is_element_ptr_ref notin_fset) + apply (metis (no_types, lifting) Suc_n_not_le_n element_ptr.sel(1) element_ptrs_def + fMax_ge ffmember_filter fimage_eqI finite_set_in is_element_ptr_ref) + done locale l_new_element = l_type_wf + assumes new_element_types_preserved: "h \ new_element \\<^sub>h h' \ type_wf h = type_wf h'" @@ -344,12 +343,9 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_tag_type_typ Let_def put_M_defs get_M_defs put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def split: prod.splits option.splits Option.bind_splits elim!: bind_returns_heap_E)[1] - apply (metis option.distinct(1)) - apply (metis bind.bind_lunit cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none) - apply (metis option.distinct(1)) - apply (metis bind.bind_lunit cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none) - by (metis bind.bind_lunit cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_none cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv) - + apply (metis finite_set_in option.inject) + apply (metis cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv finite_set_in option.sel) + done lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_child_nodes_type_wf_preserved [simp]: "h \ put_M element_ptr child_nodes_update v \\<^sub>h h' \ type_wf h = type_wf h'" @@ -357,11 +353,9 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_child_nodes_ Let_def put_M_defs get_M_defs put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def split: prod.splits option.splits Option.bind_splits elim!: bind_returns_heap_E)[1] - apply (metis option.distinct(1)) - apply (metis bind.bind_lunit cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none) - apply (metis option.distinct(1)) - apply (metis bind.bind_lunit cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none) - by (metis bind.bind_lunit cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_none cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv) + apply (metis finite_set_in option.inject) + apply (metis cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv finite_set_in option.sel) + done lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_attrs_type_wf_preserved [simp]: "h \ put_M element_ptr attrs_update v \\<^sub>h h' \ type_wf h = type_wf h'" @@ -369,11 +363,9 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_attrs_type_w put_M_defs get_M_defs put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def split: prod.splits option.splits Option.bind_splits elim!: bind_returns_heap_E)[1] - apply (metis option.distinct(1)) - apply (metis bind.bind_lunit cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none) - apply (metis option.distinct(1)) - apply (metis bind.bind_lunit cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none) - by (metis bind.bind_lunit cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_none cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv) + apply (metis finite_set_in option.inject) + apply (metis cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv finite_set_in option.sel) + done lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_shadow_root_opt_type_wf_preserved [simp]: "h \ put_M element_ptr shadow_root_opt_update v \\<^sub>h h' \ type_wf h = type_wf h'" @@ -381,11 +373,9 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_shadow_root_ Let_def put_M_defs get_M_defs put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def split: prod.splits option.splits Option.bind_splits elim!: bind_returns_heap_E)[1] - apply (metis option.distinct(1)) - apply (metis bind.bind_lunit cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none) - apply (metis option.distinct(1)) - apply (metis bind.bind_lunit cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none) - by (metis bind.bind_lunit cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_none cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv) + apply (metis finite_set_in option.inject) + apply (metis cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv finite_set_in option.sel) + done lemma put_M_pointers_preserved: assumes "h \ put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr setter v \\<^sub>h h'" @@ -446,11 +436,9 @@ lemma type_wf_drop: "type_wf h \ type_wf (Heap (fmdrop ptr (the_ apply(auto simp add: type_wf_defs NodeClass.type_wf_defs ObjectClass.type_wf_defs node_ptr_kinds_def object_ptr_kinds_def is_node_ptr_kind_def get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def)[1] - apply (metis (mono_tags, lifting) comp_apply ffmember_filter fimage_eqI - is_node_ptr_kind_cast node_ptr_casts_commute2 option.sel) - apply (metis (no_types, lifting) comp_apply element_ptr_kinds_commutes ffmember_filter - fmdom_filter fmfilter_alt_defs(1) heap.sel node_ptr_kinds_commutes object_ptr_kinds_def) - by (metis comp_eq_dest_lhs element_ptr_kinds_commutes fmdom_notI fmdrop_lookup heap.sel - node_ptr_kinds_commutes object_ptr_kinds_def) + apply (metis (no_types, lifting) element_ptr_kinds_commutes finite_set_in fmdom_notD fmdom_notI + fmlookup_drop heap.sel node_ptr_kinds_commutes o_apply object_ptr_kinds_def) + by (metis element_ptr_kinds_commutes fmdom_notI fmdrop_lookup heap.sel node_ptr_kinds_commutes + o_apply object_ptr_kinds_def) end diff --git a/Core_DOM/monads/NodeMonad.thy b/Core_DOM/monads/NodeMonad.thy index f915f54..b5616b0 100644 --- a/Core_DOM/monads/NodeMonad.thy +++ b/Core_DOM/monads/NodeMonad.thy @@ -166,7 +166,7 @@ lemma type_wf_put_ptr_in_heap_E: shows "type_wf h" using assms apply(auto simp add: type_wf_defs split: option.splits if_splits) - by (metis ObjectClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf bind.bind_lunit get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def is_node_kind_def option.collapse) + by (metis ObjectClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf bind.bind_lunit finite_set_in get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def is_node_kind_def option.exhaust_sel) subsection\Preserving Types\ @@ -194,7 +194,8 @@ lemma type_wf_preserved_small: using type_wf_preserved allI[OF assms(2), of id, simplified] apply(auto simp add: type_wf_defs) apply(auto simp add: preserved_def get_M_defs node_ptr_kinds_small[OF assms(1)] - split: option.splits, force)[1] + split: option.splits)[1] + apply (metis notin_fset option.simps(3)) by(auto simp add: preserved_def get_M_defs node_ptr_kinds_small[OF assms(1)] split: option.splits, force)[1] diff --git a/Core_DOM/preliminaries/Heap_Error_Monad.thy b/Core_DOM/preliminaries/Heap_Error_Monad.thy index f713b04..e035a64 100644 --- a/Core_DOM/preliminaries/Heap_Error_Monad.thy +++ b/Core_DOM/preliminaries/Heap_Error_Monad.thy @@ -711,6 +711,11 @@ 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 (meson is_OK_returns_result_E is_OK_returns_result_I)+ + done + lemma reflp_preserved_f [simp]: "reflp (preserved f)" by(auto simp add: preserved_def reflp_def) lemma transp_preserved_f [simp]: "transp (preserved f)" diff --git a/Core_DOM/tests/Core_DOM_BaseTest.thy b/Core_DOM/tests/Core_DOM_BaseTest.thy index 19839f4..62f5703 100644 --- a/Core_DOM/tests/Core_DOM_BaseTest.thy +++ b/Core_DOM/tests/Core_DOM_BaseTest.thy @@ -79,39 +79,6 @@ definition removeWhiteSpaceOnlyTextNodes :: "((_) object_ptr option) \create\_heap\ - -(* We use this construction because partially applied functions such as "map_of xs" don't play - well together with the code generator. *) -definition "create_heap xs = Heap (fmap_of_list xs)" - -code_datatype ObjectClass.heap.Heap create_heap - -lemma object_ptr_kinds_code1 [code]: - "object_ptr_kinds (Heap (fmap_of_list xs)) = object_ptr_kinds (create_heap xs)" - by(simp add: create_heap_def) - -lemma object_ptr_kinds_code2 [code]: - "object_ptr_kinds (create_heap xs) = fset_of_list (map fst xs)" - by (simp add: object_ptr_kinds_def create_heap_def dom_map_of_conv_image_fst) - -lemma object_ptr_kinds_code3 [code]: - "fmlookup (the_heap (create_heap xs)) x = map_of xs x" - by(auto simp add: create_heap_def fmlookup_of_list) - -lemma object_ptr_kinds_code4 [code]: - "the_heap (create_heap xs) = fmap_of_list xs" - by(simp add: create_heap_def) - -lemma object_ptr_kinds_code5 [code]: - "the_heap (Heap x) = x" - by simp - -lemma object_ptr_kinds_code6 [code]: - "noop = return ()" - by(simp add: noop_def) - - subsection \Making the functions under test compatible with untyped languages such as JavaScript\ fun set_attribute_with_null :: "((_) object_ptr option) \ attr_key \ attr_value \ (_, unit) dom_prog"