From 9a96718e9f36bfd9f70be2ad69c3b35672808db6 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Thu, 16 Apr 2020 07:46:14 +0100 Subject: [PATCH] Preparing AFP update. --- Core_DOM/Core_DOM/ROOT | 2 +- .../common/classes/CharacterDataClass.thy | 2 +- .../Core_DOM/common/classes/DocumentClass.thy | 2 +- .../Core_DOM/common/classes/ObjectClass.thy | 2 +- .../common/monads/CharacterDataMonad.thy | 2 +- .../Core_DOM/common/monads/DocumentMonad.thy | 6 +- .../Core_DOM/common/monads/ElementMonad.thy | 4 +- Core_DOM/Core_DOM/common/monads/NodeMonad.thy | 2 +- .../preliminaries/Hiding_Type_Variables.thy | 4 +- .../Core_DOM/standard/Core_DOM_Heap_WF.thy | 226 +++++++++--------- .../standard/classes/ElementClass.thy | 2 +- 11 files changed, 125 insertions(+), 129 deletions(-) diff --git a/Core_DOM/Core_DOM/ROOT b/Core_DOM/Core_DOM/ROOT index 8d18124..7cceaab 100644 --- a/Core_DOM/Core_DOM/ROOT +++ b/Core_DOM/Core_DOM/ROOT @@ -2,7 +2,7 @@ chapter AFP session "Core_DOM" (AFP) = "HOL-Library" + options [timeout = 1200] - directories + directories "common" "common/classes" "common/monads" diff --git a/Core_DOM/Core_DOM/common/classes/CharacterDataClass.thy b/Core_DOM/Core_DOM/common/classes/CharacterDataClass.thy index cf9786f..f434a93 100644 --- a/Core_DOM/Core_DOM/common/classes/CharacterDataClass.thy +++ b/Core_DOM/Core_DOM/common/classes/CharacterDataClass.thy @@ -64,7 +64,7 @@ type_synonym ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'docume = "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr, 'shadow_root_ptr, 'Object, 'CharacterData option RCharacterData_ext + 'Node, 'Element) heap" register_default_tvars "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr, - 'shadow_root_ptr, 'Object, 'Node, 'Element, 'CharacterData) heap" + 'shadow_root_ptr, 'Object, 'Node, 'Element, 'CharacterData) heap" type_synonym heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l = "(unit, unit, unit, unit, unit, unit, unit, unit, unit, unit) heap" diff --git a/Core_DOM/Core_DOM/common/classes/DocumentClass.thy b/Core_DOM/Core_DOM/common/classes/DocumentClass.thy index 0cc7880..094e216 100644 --- a/Core_DOM/Core_DOM/common/classes/DocumentClass.thy +++ b/Core_DOM/Core_DOM/common/classes/DocumentClass.thy @@ -64,7 +64,7 @@ type_synonym ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'docume 'Element, 'CharacterData) heap" register_default_tvars "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr, - 'shadow_root_ptr, 'Object, 'Node, 'Element, 'CharacterData, 'Document) heap" + 'shadow_root_ptr, 'Object, 'Node, 'Element, 'CharacterData, 'Document) heap" type_synonym heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l = "(unit, unit, unit, unit, unit, unit, unit, unit, unit, unit, unit) heap" diff --git a/Core_DOM/Core_DOM/common/classes/ObjectClass.thy b/Core_DOM/Core_DOM/common/classes/ObjectClass.thy index b3091ef..7461138 100644 --- a/Core_DOM/Core_DOM/common/classes/ObjectClass.thy +++ b/Core_DOM/Core_DOM/common/classes/ObjectClass.thy @@ -44,7 +44,7 @@ type_synonym 'Object Object = "'Object RObject_scheme" register_default_tvars "'Object Object" datatype ('object_ptr, 'Object) heap = Heap (the_heap: "((_) object_ptr, (_) Object) fmap") -register_default_tvars "('object_ptr, 'Object) heap" +register_default_tvars "('object_ptr, 'Object) heap" type_synonym heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l = "(unit, unit) heap" definition object_ptr_kinds :: "(_) heap \ (_) object_ptr fset" diff --git a/Core_DOM/Core_DOM/common/monads/CharacterDataMonad.thy b/Core_DOM/Core_DOM/common/monads/CharacterDataMonad.thy index 209d410..b86e4c3 100644 --- a/Core_DOM/Core_DOM/common/monads/CharacterDataMonad.thy +++ b/Core_DOM/Core_DOM/common/monads/CharacterDataMonad.thy @@ -57,7 +57,7 @@ lemma character_data_ptr_kinds_M_eq: lemma character_data_ptr_kinds_M_reads: "reads (\node_ptr. {preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t node_ptr RObject.nothing)}) character_data_ptr_kinds_M h h'" using node_ptr_kinds_M_reads - apply(simp add: reads_def node_ptr_kinds_M_defs character_data_ptr_kinds_M_defs + apply (simp add: reads_def node_ptr_kinds_M_defs character_data_ptr_kinds_M_defs character_data_ptr_kinds_def preserved_def) by (smt node_ptr_kinds_small preserved_def unit_all_impI) diff --git a/Core_DOM/Core_DOM/common/monads/DocumentMonad.thy b/Core_DOM/Core_DOM/common/monads/DocumentMonad.thy index 2ff02bc..9b9958c 100644 --- a/Core_DOM/Core_DOM/common/monads/DocumentMonad.thy +++ b/Core_DOM/Core_DOM/common/monads/DocumentMonad.thy @@ -55,7 +55,7 @@ lemma document_ptr_kinds_M_eq: lemma document_ptr_kinds_M_reads: "reads (\object_ptr. {preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing)}) document_ptr_kinds_M h h'" using object_ptr_kinds_M_reads - apply(simp add: reads_def object_ptr_kinds_M_defs document_ptr_kinds_M_defs + apply (simp add: reads_def object_ptr_kinds_M_defs document_ptr_kinds_M_defs document_ptr_kinds_def preserved_def cong del: image_cong_simp) apply (metis (mono_tags, hide_lams) object_ptr_kinds_preserved_small old.unit.exhaust preserved_def) done @@ -453,7 +453,7 @@ 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_docu split: option.splits)[1] 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 diff --git a/Core_DOM/Core_DOM/common/monads/ElementMonad.thy b/Core_DOM/Core_DOM/common/monads/ElementMonad.thy index 8b00146..f4ba05c 100644 --- a/Core_DOM/Core_DOM/common/monads/ElementMonad.thy +++ b/Core_DOM/Core_DOM/common/monads/ElementMonad.thy @@ -54,7 +54,7 @@ lemma element_ptr_kinds_M_eq: lemma element_ptr_kinds_M_reads: "reads (\element_ptr. {preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t element_ptr RObject.nothing)}) element_ptr_kinds_M h h'" - apply(simp add: reads_def node_ptr_kinds_M_defs element_ptr_kinds_M_defs element_ptr_kinds_def + apply (simp add: reads_def node_ptr_kinds_M_defs element_ptr_kinds_M_defs element_ptr_kinds_def node_ptr_kinds_M_reads preserved_def cong del: image_cong_simp) apply (metis (mono_tags, hide_lams) node_ptr_kinds_small old.unit.exhaust preserved_def) done @@ -323,7 +323,7 @@ lemma new_element_type_wf_preserved [simp]: "h \ new_element \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 finite_set_in - is_element_ptr_ref) + 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) diff --git a/Core_DOM/Core_DOM/common/monads/NodeMonad.thy b/Core_DOM/Core_DOM/common/monads/NodeMonad.thy index b5616b0..b17a231 100644 --- a/Core_DOM/Core_DOM/common/monads/NodeMonad.thy +++ b/Core_DOM/Core_DOM/common/monads/NodeMonad.thy @@ -75,7 +75,7 @@ global_interpretation l_get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e_lemmas type_wf by lemma node_ptr_kinds_M_reads: "reads (\object_ptr. {preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing)}) node_ptr_kinds_M h h'" using object_ptr_kinds_M_reads - apply(simp add: reads_def node_ptr_kinds_M_defs node_ptr_kinds_def + apply (simp add: reads_def node_ptr_kinds_M_defs node_ptr_kinds_def object_ptr_kinds_M_reads preserved_def) by (smt object_ptr_kinds_preserved_small preserved_def unit_all_impI) diff --git a/Core_DOM/Core_DOM/common/preliminaries/Hiding_Type_Variables.thy b/Core_DOM/Core_DOM/common/preliminaries/Hiding_Type_Variables.thy index 9c6c783..3c593ef 100644 --- a/Core_DOM/Core_DOM/common/preliminaries/Hiding_Type_Variables.thy +++ b/Core_DOM/Core_DOM/common/preliminaries/Hiding_Type_Variables.thy @@ -278,7 +278,7 @@ structure Hide_Tvar : HIDE_TVAR = struct fun parse_ast ((Ast.Constant const)::[]) = (const,NONE) | parse_ast ((Ast.Constant sort)::(Ast.Constant const)::[]) = (const,SOME sort) - | parse_ast _ = error("AST type not supported.") + | parse_ast _ = error("AST type not supported.") val (decorated_name, decorated_sort) = parse_ast ast @@ -295,7 +295,7 @@ structure Hide_Tvar : HIDE_TVAR = struct let fun mk_tvar n = case decorated_sort of NONE => Ast.Variable(name_of_tvar n) - | SOME sort => Ast.Appl([Ast.Constant("_ofsort"), + | SOME sort => Ast.Appl([Ast.Constant("_ofsort"), Ast.Variable(name_of_tvar n), Ast.Constant(sort)]) in diff --git a/Core_DOM/Core_DOM/standard/Core_DOM_Heap_WF.thy b/Core_DOM/Core_DOM/standard/Core_DOM_Heap_WF.thy index 6d31b9b..0535ce9 100644 --- a/Core_DOM/Core_DOM/standard/Core_DOM_Heap_WF.thy +++ b/Core_DOM/Core_DOM/standard/Core_DOM_Heap_WF.thy @@ -3576,7 +3576,7 @@ have "type_wf h2" 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 + 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" @@ -4528,9 +4528,9 @@ proof - 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 + 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 @@ -5486,7 +5486,7 @@ 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] 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) @@ -5501,12 +5501,12 @@ proof - 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' 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) @@ -5516,14 +5516,14 @@ proof - 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 @@ -5550,17 +5550,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 @@ -5575,10 +5575,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 @@ -5593,11 +5593,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" @@ -5606,7 +5606,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 @@ -5632,9 +5632,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 @@ -5644,10 +5644,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 @@ -5680,13 +5680,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 @@ -5697,11 +5697,11 @@ 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] 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) @@ -6180,7 +6180,9 @@ proof - by auto obtain parent_opt where parent_opt: "h \ get_parent child \\<^sub>r parent_opt" - by (meson assms(2) assms(3) is_OK_returns_result_I l_get_owner_document.get_owner_document_ptr_in_heap local.get_parent_ok local.l_get_owner_document_axioms node_ptr_kinds_commutes old_document returns_result_select_result) + by (meson assms(2) assms(3) is_OK_returns_result_I l_get_owner_document.get_owner_document_ptr_in_heap + local.get_parent_ok local.l_get_owner_document_axioms node_ptr_kinds_commutes old_document + returns_result_select_result) then have "h \ ok (get_parent child)" by auto @@ -6407,7 +6409,8 @@ proof - obtain h2 where h2: "h \ adopt_node owner_document node \\<^sub>h h2" - by (meson assms(1) assms(2) assms(3) assms(5) is_OK_returns_heap_E adopt_node_ok l_insert_before_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms local.get_owner_document_owner_document_in_heap owner_document) + by (meson assms(1) assms(2) assms(3) assms(5) is_OK_returns_heap_E adopt_node_ok l_insert_before_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms + local.get_owner_document_owner_document_in_heap owner_document) then have "h \ ok (adopt_node owner_document node)" by auto have "object_ptr_kinds h = object_ptr_kinds h2" @@ -6970,24 +6973,18 @@ 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) @@ -7352,20 +7349,23 @@ 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\ heap_is_wellformed_children_in_heap @@ -7428,25 +7428,13 @@ 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) @@ -7482,10 +7470,25 @@ 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) + + have "known_ptr (cast new_character_data_ptr)" + using \h \ create_character_data document_ptr text \\<^sub>r new_character_data_ptr\ local.create_character_data_known_ptr by blast + then + have "known_ptrs h2" + using known_ptrs_new_ptr object_ptr_kinds_eq_h \known_ptrs h\ h2 + by blast + then + have "known_ptrs h3" + using known_ptrs_preserved object_ptr_kinds_eq_h2 by blast + then + show "known_ptrs h'" + using known_ptrs_preserved object_ptr_kinds_eq_h3 by blast 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'\ @@ -7595,7 +7598,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)+ @@ -7645,22 +7648,20 @@ proof - have "a_all_ptrs_in_heap h" using \heap_is_wellformed h\ by (simp add: heap_is_wellformed_def) - then have "a_all_ptrs_in_heap h'" + 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\ by (simp add: heap_is_wellformed_def) @@ -7729,12 +7730,7 @@ proof - 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) - + 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'\ by(simp add: heap_is_wellformed_def) diff --git a/Core_DOM/Core_DOM/standard/classes/ElementClass.thy b/Core_DOM/Core_DOM/standard/classes/ElementClass.thy index 1746aaa..8128245 100644 --- a/Core_DOM/Core_DOM/standard/classes/ElementClass.thy +++ b/Core_DOM/Core_DOM/standard/classes/ElementClass.thy @@ -156,7 +156,7 @@ lemma get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_type_wf: 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 notin_fset - option.distinct(1)) + 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