diff --git a/Core_DOM/Core_DOM_Functions.thy b/Core_DOM/Core_DOM_Functions.thy index 7a4a48e..b221870 100644 --- a/Core_DOM/Core_DOM_Functions.thy +++ b/Core_DOM/Core_DOM_Functions.thy @@ -3291,10 +3291,21 @@ global_interpretation l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^ . locale l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M = - l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs + - l_get_disconnected_nodes + - l_set_val + - l_create_character_data_defs + + l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs set_val set_val_locs get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs + + l_get_disconnected_nodes type_wf get_disconnected_nodes get_disconnected_nodes_locs + + l_set_val type_wf set_val set_val_locs + + l_create_character_data_defs create_character_data + + l_known_ptr known_ptr + for get_disconnected_nodes :: "(_) document_ptr \ ((_) heap, exception, (_) node_ptr list) prog" + and get_disconnected_nodes_locs :: "(_) document_ptr \ ((_) heap \ (_) heap \ bool) set" + and set_disconnected_nodes :: "(_) document_ptr \ (_) node_ptr list \ ((_) heap, exception, unit) prog" + and set_disconnected_nodes_locs :: "(_) document_ptr \ ((_) heap, exception, unit) prog set" + and set_val :: "(_) character_data_ptr \ char list \ ((_) heap, exception, unit) prog" + and set_val_locs :: "(_) character_data_ptr \ ((_) heap, exception, unit) prog set" + and type_wf :: "(_) heap \ bool" + and create_character_data :: "(_) document_ptr \ char list \ ((_) heap, exception, (_) character_data_ptr) prog" + and known_ptr :: "(_) object_ptr \ bool" + + assumes known_ptr_impl: "known_ptr = a_known_ptr" assumes create_character_data_impl: "create_character_data = a_create_character_data" begin lemmas create_character_data_def = a_create_character_data_def[folded create_character_data_impl] @@ -3330,12 +3341,25 @@ proof - ultimately show ?thesis by (auto simp add: document_ptr_kinds_def) qed + +lemma create_character_data_known_ptr: + assumes "h \ create_character_data document_ptr tag \\<^sub>r new_character_data_ptr" + shows "known_ptr (cast new_character_data_ptr)" +proof - + have "is_character_data_ptr new_character_data_ptr" + using assms + apply(auto simp add: create_character_data_def elim!: bind_returns_result_E) + using new_character_data_is_character_data_ptr + by blast + then show ?thesis + by(auto simp add: known_ptr_impl DocumentClass.known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs) +qed end locale l_create_character_data = l_create_character_data_defs interpretation - i_create_character_data?: l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M set_val set_val_locs get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs type_wf create_character_data + i_create_character_data?: l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs set_val set_val_locs type_wf create_character_data known_ptr by(auto simp add: l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms_def create_character_data_def instances) declare l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances] @@ -3592,6 +3616,30 @@ lemma get_element_by_id_result_in_tree_order: intro!: map_filter_M_pure map_M_pure_I bind_pure_I split: option.splits list.splits if_splits) +lemma get_elements_by_class_name_result_in_tree_order: + assumes "h \ get_elements_by_class_name ptr name \\<^sub>r results" + assumes "h \ to_tree_order ptr \\<^sub>r to" + assumes "element_ptr \ set results" + shows "cast element_ptr \ set to" + using assms + by(auto simp add: get_elements_by_class_name_def first_in_tree_order_def + elim!: map_filter_M_pure_E[where y=element_ptr] bind_returns_result_E2 + dest!: bind_returns_result_E3[rotated, OF assms(2), rotated] + intro!: map_filter_M_pure map_M_pure_I bind_pure_I + split: option.splits list.splits if_splits) + +lemma get_elements_by_tag_name_result_in_tree_order: + assumes "h \ get_elements_by_tag_name ptr name \\<^sub>r results" + assumes "h \ to_tree_order ptr \\<^sub>r to" + assumes "element_ptr \ set results" + shows "cast element_ptr \ set to" + using assms + by(auto simp add: get_elements_by_tag_name_def first_in_tree_order_def + elim!: map_filter_M_pure_E[where y=element_ptr] bind_returns_result_E2 + dest!: bind_returns_result_E3[rotated, OF assms(2), rotated] + intro!: map_filter_M_pure map_M_pure_I bind_pure_I + split: option.splits list.splits if_splits) + lemma get_elements_by_tag_name_pure [simp]: "pure (get_elements_by_tag_name ptr tag_name) h" by(auto simp add: get_elements_by_tag_name_def intro!: bind_pure_I map_filter_M_pure diff --git a/Core_DOM/Core_DOM_Heap_WF.thy b/Core_DOM/Core_DOM_Heap_WF.thy index f312a29..df5c085 100644 --- a/Core_DOM/Core_DOM_Heap_WF.thy +++ b/Core_DOM/Core_DOM_Heap_WF.thy @@ -6038,8 +6038,8 @@ locale l_create_character_data_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub> + l_set_val_get_disconnected_nodes type_wf set_val set_val_locs get_disconnected_nodes get_disconnected_nodes_locs + l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M - set_val set_val_locs get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes - set_disconnected_nodes_locs type_wf create_character_data + get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes + set_disconnected_nodes_locs set_val set_val_locs type_wf create_character_data known_ptr + l_new_character_data_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs + l_set_val_get_child_nodes @@ -6451,6 +6451,7 @@ interpretation i_create_character_data_wf?: l_create_character_data_wf\<^sub>C\< set_disconnected_nodes_locs create_character_data known_ptrs using instances by (auto simp add: l_create_character_data_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def) +declare l_create_character_data_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances] subsection \create\_document\