diff --git a/Core_DOM/Core_DOM_Heap_WF.thy b/Core_DOM/Core_DOM_Heap_WF.thy index c9a9f93..6937ad9 100644 --- a/Core_DOM/Core_DOM_Heap_WF.thy +++ b/Core_DOM/Core_DOM_Heap_WF.thy @@ -5882,7 +5882,6 @@ 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(-) 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\ @@ -5912,7 +5911,6 @@ proof - and 6: "x \ set |h' \ get_disconnected_nodes xb|\<^sub>r" show "False" using disc_nodes_document_ptr_h disconnected_nodes_eq2_h3 - apply - apply(cases "xb = document_ptr") apply (metis (no_types, hide_lams) "3" "4" "6" \\p. p |\| object_ptr_kinds h3 \ cast new_character_data_ptr \ set |h3 \ get_child_nodes p|\<^sub>r\ @@ -5927,11 +5925,11 @@ proof - then have "a_owner_document_valid h'" using disc_nodes_h3 \document_ptr |\| document_ptr_kinds h\ apply(simp add: a_owner_document_valid_def) - apply(simp add: object_ptr_kinds_eq_h object_ptr_kinds_eq_h3 ) + apply(simp add: object_ptr_kinds_eq_h object_ptr_kinds_eq_h3 ) apply(simp add: object_ptr_kinds_eq_h2) - apply(simp add: document_ptr_kinds_eq_h document_ptr_kinds_eq_h3 ) + apply(simp add: document_ptr_kinds_eq_h document_ptr_kinds_eq_h3 ) apply(simp add: document_ptr_kinds_eq_h2) - apply(simp add: node_ptr_kinds_eq_h node_ptr_kinds_eq_h3 ) + apply(simp add: node_ptr_kinds_eq_h node_ptr_kinds_eq_h3 ) apply(simp add: node_ptr_kinds_eq_h2 node_ptr_kinds_eq_h ) apply(auto simp add: children_eq2_h2[symmetric] children_eq2_h3[symmetric] disconnected_nodes_eq2_h disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3)[1] diff --git a/Core_DOM/ROOT b/Core_DOM/ROOT index f4591ac..798cf8e 100644 --- a/Core_DOM/ROOT +++ b/Core_DOM/ROOT @@ -1,7 +1,7 @@ chapter AFP session "Core_DOM-devel" (AFP) = "HOL-Library" + - options [timeout = 4800, document = pdf, document_variants="document:outline=/proof,/ML"] + options [timeout = 600] theories Core_DOM Core_DOM_Tests diff --git a/Core_DOM/classes/BaseClass.thy b/Core_DOM/classes/BaseClass.thy index 02b4fa6..011bb9b 100644 --- a/Core_DOM/classes/BaseClass.thy +++ b/Core_DOM/classes/BaseClass.thy @@ -32,7 +32,7 @@ text\In this theory, we introduce the basic infrastructure for our encodin of classes.\ theory BaseClass imports - "~~/src/HOL/Library/Finite_Map" + "HOL-Library.Finite_Map" "../pointers/Ref" "../Core_DOM_Basic_Datatypes" begin diff --git a/Core_DOM/monads/CharacterDataMonad.thy b/Core_DOM/monads/CharacterDataMonad.thy index e34b42e..4506a2a 100644 --- a/Core_DOM/monads/CharacterDataMonad.thy +++ b/Core_DOM/monads/CharacterDataMonad.thy @@ -364,10 +364,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 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) ElementMonad.a_get_M_def error_returns_result - get_heap_returns_result option.exhaust_sel option.simps(4)) + 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 ) lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_child_nodes_type_wf_preserved [simp]: @@ -394,8 +392,7 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_child_nodes_ 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) ElementMonad.a_get_M_def error_returns_result get_heap_returns_result - option.exhaust_sel option.simps(4)) + by (metis (no_types, lifting) option.exhaust_sel) 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'" @@ -416,7 +413,7 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_attrs_type_w 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) ElementMonad.a_get_M_def error_returns_result get_heap_returns_result option.exhaust_sel option.simps(4)) + by (metis (no_types, lifting) option.exhaust_sel) 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'" @@ -437,8 +434,7 @@ lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_shadow_root_ 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) ElementMonad.a_get_M_def error_returns_result get_heap_returns_result - option.exhaust_sel option.simps(4)) + by (metis (no_types, lifting) option.exhaust_sel) lemma new_character_data_type_wf_preserved [simp]: @@ -536,4 +532,4 @@ lemma type_wf_drop: "type_wf h \ type_wf (Heap (fmdrop ptr (the_ 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) -end +end \ No newline at end of file diff --git a/Core_DOM/monads/NodeMonad.thy b/Core_DOM/monads/NodeMonad.thy index 42c764b..91a9791 100644 --- a/Core_DOM/monads/NodeMonad.thy +++ b/Core_DOM/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_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 (metis (mono_tags, hide_lams) object_ptr_kinds_preserved_small old.unit.exhaust preserved_def) diff --git a/Core_DOM/preliminaries/Heap_Error_Monad.thy b/Core_DOM/preliminaries/Heap_Error_Monad.thy index 2f8f1d7..f713b04 100644 --- a/Core_DOM/preliminaries/Heap_Error_Monad.thy +++ b/Core_DOM/preliminaries/Heap_Error_Monad.thy @@ -591,7 +591,7 @@ lemma filter_M_ex1: and "h \ P x \\<^sub>r True" shows "ys = [x]" proof - - have "\!x \ set xs. |h \ P x|\<^sub>r" + have *: "\!x \ set xs. |h \ P x|\<^sub>r" apply(insert assms(1) assms(3) assms(4)) apply(drule filter_M_filter) apply(simp) @@ -601,7 +601,7 @@ proof - apply(insert assms(1) assms(4)) apply(drule filter_M_filter) apply(auto)[1] - by (metis \\!x. x \ set xs \ |h \ P x|\<^sub>r\ assms(2) assms(5) assms(6) distinct_filter + by (metis * assms(2) assms(5) assms(6) distinct_filter distinct_length_2_or_more filter_empty_conv filter_set list.exhaust list.set_intros(1) list.set_intros(2) member_filter select_result_I2) qed