From 25e85825bd68891c68478cc0aec67e7fc3a2abab Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Wed, 15 Apr 2020 23:59:20 +0100 Subject: [PATCH] Preparing AFP update. --- Core_DOM/Core_DOM/common/Core_DOM.thy | 5 - .../Core_DOM/common/monads/DocumentMonad.thy | 6 +- .../Core_DOM/common/monads/ElementMonad.thy | 5 +- .../preliminaries/Hiding_Type_Variables.thy | 5 +- .../common/preliminaries/Testing_Utils.thy | 3 +- .../Core_DOM/standard/Core_DOM_Heap_WF.thy | 112 ++++++++++++------ Core_DOM/Core_DOM_Scope_Components/CITATION | 37 ++++++ Core_DOM/Core_DOM_Scope_Components/ROOT | 2 +- .../common/Core_DOM.thy | 5 - .../common/monads/DocumentMonad.thy | 6 +- .../common/monads/ElementMonad.thy | 5 +- .../preliminaries/Hiding_Type_Variables.thy | 5 +- .../common/preliminaries/Testing_Utils.thy | 3 +- 13 files changed, 133 insertions(+), 66 deletions(-) create mode 100644 Core_DOM/Core_DOM_Scope_Components/CITATION diff --git a/Core_DOM/Core_DOM/common/Core_DOM.thy b/Core_DOM/Core_DOM/common/Core_DOM.thy index de33929..6b48724 100644 --- a/Core_DOM/Core_DOM/common/Core_DOM.thy +++ b/Core_DOM/Core_DOM/common/Core_DOM.thy @@ -35,10 +35,5 @@ imports "Core_DOM_Heap_WF" begin -ML - {* - map warning (Posix.ProcEnv.environ()) -*} - end diff --git a/Core_DOM/Core_DOM/common/monads/DocumentMonad.thy b/Core_DOM/Core_DOM/common/monads/DocumentMonad.thy index 72f8538..2ff02bc 100644 --- a/Core_DOM/Core_DOM/common/monads/DocumentMonad.thy +++ b/Core_DOM/Core_DOM/common/monads/DocumentMonad.thy @@ -55,10 +55,10 @@ 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 - document_ptr_kinds_def preserved_def) - by (smt object_ptr_kinds_preserved_small preserved_def unit_all_impI) + 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 global_interpretation l_dummy defines get_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t = "l_get_M.a_get_M get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t" . lemma get_M_is_l_get_M: "l_get_M get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t type_wf document_ptr_kinds" diff --git a/Core_DOM/Core_DOM/common/monads/ElementMonad.thy b/Core_DOM/Core_DOM/common/monads/ElementMonad.thy index de137cc..8b00146 100644 --- a/Core_DOM/Core_DOM/common/monads/ElementMonad.thy +++ b/Core_DOM/Core_DOM/common/monads/ElementMonad.thy @@ -55,8 +55,9 @@ 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 - node_ptr_kinds_M_reads preserved_def) - by (smt filter_fset node_ptr_kinds_small preserved_def unit_all_impI) + 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 global_interpretation l_dummy defines get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t = "l_get_M.a_get_M get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t" . lemma get_M_is_l_get_M: "l_get_M get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t type_wf element_ptr_kinds" 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 e31e560..9c6c783 100644 --- a/Core_DOM/Core_DOM/common/preliminaries/Hiding_Type_Variables.thy +++ b/Core_DOM/Core_DOM/common/preliminaries/Hiding_Type_Variables.thy @@ -276,7 +276,8 @@ structure Hide_Tvar : HIDE_TVAR = struct val thy = Proof_Context.theory_of ctx fun parse_ast ((Ast.Constant const)::[]) = (const,NONE) - | parse_ast (sort::(Ast.Constant const)::[]) = (const,SOME sort) + | parse_ast ((Ast.Constant sort)::(Ast.Constant const)::[]) + = (const,SOME sort) | parse_ast _ = error("AST type not supported.") val (decorated_name, decorated_sort) = parse_ast ast @@ -296,7 +297,7 @@ structure Hide_Tvar : HIDE_TVAR = struct NONE => Ast.Variable(name_of_tvar n) | SOME sort => Ast.Appl([Ast.Constant("_ofsort"), Ast.Variable(name_of_tvar n), - sort]) + Ast.Constant(sort)]) in map mk_tvar (#tvars default_info) end diff --git a/Core_DOM/Core_DOM/common/preliminaries/Testing_Utils.thy b/Core_DOM/Core_DOM/common/preliminaries/Testing_Utils.thy index c5bd990..a8811e7 100644 --- a/Core_DOM/Core_DOM/common/preliminaries/Testing_Utils.thy +++ b/Core_DOM/Core_DOM/common/preliminaries/Testing_Utils.thy @@ -30,7 +30,6 @@ theory Testing_Utils imports Main begin - ML \ val _ = Theory.setup (Method.setup @{binding timed_code_simp} @@ -90,4 +89,4 @@ val _ = Theory.setup (* of "eval" with either "timed_code_simp", "timed_eval", or, to run both and write the results *) (* to /tmp/isabellebench, "timed_eval_and_code_simp". *) -end \ No newline at end of file +end 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 7b72a6f..6d31b9b 100644 --- a/Core_DOM/Core_DOM/standard/Core_DOM_Heap_WF.thy +++ b/Core_DOM/Core_DOM/standard/Core_DOM_Heap_WF.thy @@ -145,7 +145,6 @@ defines heap_is_wellformed = "l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub 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 @@ -1813,9 +1812,6 @@ locale l_get_root_node_wf = l_heap_is_wellformed_defs + l_get_root_node_defs + l assumes get_root_node_same_no_parent: "heap_is_wellformed h \ type_wf h \ known_ptrs h \ h \ get_root_node ptr \\<^sub>r cast child \ h \ get_parent child \\<^sub>r None" - (* assumes get_root_node_not_node_same: - "ptr |\| object_ptr_kinds h \ \is_node_ptr_kind ptr - \ h \ get_root_node ptr \\<^sub>r ptr" *) assumes get_root_node_parent_same: "h \ get_parent child \\<^sub>r Some ptr \ h \ get_root_node (cast child) \\<^sub>r root \ h \ get_root_node ptr \\<^sub>r root" @@ -1854,7 +1850,6 @@ lemma get_root_node_wf_is_l_get_root_node_wf [instances]: using get_root_node_root_in_heap apply blast using get_ancestors_same_root_node apply(blast, blast) using get_root_node_same_no_parent apply blast - (* using get_root_node_not_node_same apply blast *) using get_root_node_parent_same apply (blast, blast) done @@ -3581,7 +3576,6 @@ 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 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'" @@ -4536,7 +4530,13 @@ proof - 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 document_ptr_kinds_eq2_h3 children_eq2_h2 children_eq2_h3 ) - 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)) + 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) have a_distinct_lists_h2: "a_distinct_lists h2" using wellformed_h2 by (simp add: heap_is_wellformed_def) @@ -5508,8 +5508,6 @@ proof - 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] 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) qed @@ -6972,8 +6970,24 @@ proof - ultimately show "False" apply(-) apply(cases "x = document_ptr") - 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) + 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 next fix x xa xb assume 2: "(\x\fset (object_ptr_kinds h3). set |h' \ get_child_nodes x|\<^sub>r) @@ -7338,14 +7352,19 @@ 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, 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) - + 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) then have "a_all_ptrs_in_heap h3" - 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) + 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) then have "a_all_ptrs_in_heap h'" - 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)) - + 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) 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\ @@ -7409,7 +7428,25 @@ 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" - 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) + 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 next fix x xa xb assume 2: "(\x\fset (object_ptr_kinds h3). set |h' \ get_child_nodes x|\<^sub>r) @@ -7445,20 +7482,10 @@ 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 (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 + 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) 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'\ @@ -7620,13 +7647,19 @@ 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] - using ObjectMonad.ptr_kinds_ptr_kinds_M + 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 - 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) + 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) have "a_distinct_lists h" using \heap_is_wellformed h\ @@ -7695,7 +7728,12 @@ 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\ children_eq2 disconnected_nodes_eq2_h document_ptr_kinds_commutes finite_set_in funion_iff node_ptr_kinds_eq object_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\ + \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) 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/Core_DOM_Scope_Components/CITATION b/Core_DOM/Core_DOM_Scope_Components/CITATION new file mode 100644 index 0000000..5246cbd --- /dev/null +++ b/Core_DOM/Core_DOM_Scope_Components/CITATION @@ -0,0 +1,37 @@ +An overview of the formalization is given in: + + Achim D. Brucker and Michael Herzberg. A Formal Semantics of the Core DOM + in Isabelle/HOL. In The 2018 Web Conference Companion (WWW). Pages 741-749, + ACM Press, 2018. doi:10.1145/3184558.3185980 + +A BibTeX entry for LaTeX users is +@InProceedings{ brucker.ea:core-dom:2018, + abstract = {At its core, the Document Object Model (DOM) defines a tree-like + data structure for representing documents in general and HTML + documents in particular. It forms the heart of any rendering engine + of modern web browsers. Formalizing the key concepts of the DOM is + a pre-requisite for the formal reasoning over client-side JavaScript + programs as well as for the analysis of security concepts in modern + web browsers. In this paper, we present a formalization of the core DOM, + with focus on the node-tree and the operations defined on node-trees, + in Isabelle/HOL. We use the formalization to verify the functional + correctness of the most important functions defined in the DOM standard. + Moreover, our formalization is (1) extensible, i.e., can be extended without + the need of re-proving already proven properties and (2) executable, i.e., + we can generate executable code from our specification.}, + address = {New York, NY, USA}, + author = {Achim D. Brucker and Michael Herzberg}, + booktitle= {The 2018 Web Conference Companion (WWW)}, + conf_date= {April 23-27, 2018}, + doi = {10.1145/3184558.3185980}, + editor = {Pierre{-}Antoine Champin and Fabien L. Gandon and Mounia Lalmas and Panagiotis G. Ipeirotis}, + isbn = {978-1-4503-5640-4/18/04}, + keywords = {Document Object Model, DOM, Formal Semantics, Isabelle/HOL}, + location = {Lyon, France}, + pages = {741--749}, + pdf = {https://www.brucker.ch/bibliography/download/2018/brucker.ea-core-dom-2018.pdf}, + publisher= {ACM Press}, + title = {A Formal Semantics of the Core {DOM} in {Isabelle/HOL}}, + url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-core-dom-2018}, + year = {2018}, +} diff --git a/Core_DOM/Core_DOM_Scope_Components/ROOT b/Core_DOM/Core_DOM_Scope_Components/ROOT index 31b8f76..5481852 100644 --- a/Core_DOM/Core_DOM_Scope_Components/ROOT +++ b/Core_DOM/Core_DOM_Scope_Components/ROOT @@ -1,7 +1,7 @@ chapter AFP session "Core_DOM_Scope_Components" (AFP) = "HOL-Library" + - options [timeout = 600] + options [timeout = 1200] directories "common" "common/classes" diff --git a/Core_DOM/Core_DOM_Scope_Components/common/Core_DOM.thy b/Core_DOM/Core_DOM_Scope_Components/common/Core_DOM.thy index de33929..6b48724 100644 --- a/Core_DOM/Core_DOM_Scope_Components/common/Core_DOM.thy +++ b/Core_DOM/Core_DOM_Scope_Components/common/Core_DOM.thy @@ -35,10 +35,5 @@ imports "Core_DOM_Heap_WF" begin -ML - {* - map warning (Posix.ProcEnv.environ()) -*} - end diff --git a/Core_DOM/Core_DOM_Scope_Components/common/monads/DocumentMonad.thy b/Core_DOM/Core_DOM_Scope_Components/common/monads/DocumentMonad.thy index 72f8538..2ff02bc 100644 --- a/Core_DOM/Core_DOM_Scope_Components/common/monads/DocumentMonad.thy +++ b/Core_DOM/Core_DOM_Scope_Components/common/monads/DocumentMonad.thy @@ -55,10 +55,10 @@ 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 - document_ptr_kinds_def preserved_def) - by (smt object_ptr_kinds_preserved_small preserved_def unit_all_impI) + 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 global_interpretation l_dummy defines get_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t = "l_get_M.a_get_M get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t" . lemma get_M_is_l_get_M: "l_get_M get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t type_wf document_ptr_kinds" diff --git a/Core_DOM/Core_DOM_Scope_Components/common/monads/ElementMonad.thy b/Core_DOM/Core_DOM_Scope_Components/common/monads/ElementMonad.thy index de137cc..8b00146 100644 --- a/Core_DOM/Core_DOM_Scope_Components/common/monads/ElementMonad.thy +++ b/Core_DOM/Core_DOM_Scope_Components/common/monads/ElementMonad.thy @@ -55,8 +55,9 @@ 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 - node_ptr_kinds_M_reads preserved_def) - by (smt filter_fset node_ptr_kinds_small preserved_def unit_all_impI) + 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 global_interpretation l_dummy defines get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t = "l_get_M.a_get_M get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t" . lemma get_M_is_l_get_M: "l_get_M get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t type_wf element_ptr_kinds" diff --git a/Core_DOM/Core_DOM_Scope_Components/common/preliminaries/Hiding_Type_Variables.thy b/Core_DOM/Core_DOM_Scope_Components/common/preliminaries/Hiding_Type_Variables.thy index e31e560..9c6c783 100644 --- a/Core_DOM/Core_DOM_Scope_Components/common/preliminaries/Hiding_Type_Variables.thy +++ b/Core_DOM/Core_DOM_Scope_Components/common/preliminaries/Hiding_Type_Variables.thy @@ -276,7 +276,8 @@ structure Hide_Tvar : HIDE_TVAR = struct val thy = Proof_Context.theory_of ctx fun parse_ast ((Ast.Constant const)::[]) = (const,NONE) - | parse_ast (sort::(Ast.Constant const)::[]) = (const,SOME sort) + | parse_ast ((Ast.Constant sort)::(Ast.Constant const)::[]) + = (const,SOME sort) | parse_ast _ = error("AST type not supported.") val (decorated_name, decorated_sort) = parse_ast ast @@ -296,7 +297,7 @@ structure Hide_Tvar : HIDE_TVAR = struct NONE => Ast.Variable(name_of_tvar n) | SOME sort => Ast.Appl([Ast.Constant("_ofsort"), Ast.Variable(name_of_tvar n), - sort]) + Ast.Constant(sort)]) in map mk_tvar (#tvars default_info) end diff --git a/Core_DOM/Core_DOM_Scope_Components/common/preliminaries/Testing_Utils.thy b/Core_DOM/Core_DOM_Scope_Components/common/preliminaries/Testing_Utils.thy index c5bd990..a8811e7 100644 --- a/Core_DOM/Core_DOM_Scope_Components/common/preliminaries/Testing_Utils.thy +++ b/Core_DOM/Core_DOM_Scope_Components/common/preliminaries/Testing_Utils.thy @@ -30,7 +30,6 @@ theory Testing_Utils imports Main begin - ML \ val _ = Theory.setup (Method.setup @{binding timed_code_simp} @@ -90,4 +89,4 @@ val _ = Theory.setup (* of "eval" with either "timed_code_simp", "timed_eval", or, to run both and write the results *) (* to /tmp/isabellebench, "timed_eval_and_code_simp". *) -end \ No newline at end of file +end