BrowserSecurity
/
Core_DOM-dev
Archived
forked from afp-mirror/Core_DOM
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

First step towards joining standard compliant and scope_component setup.

This commit is contained in:
Achim D. Brucker 2020-04-03 23:14:51 +01:00
parent 857db5127e
commit 781edd622a
1 changed files with 24 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
Core_DOM/Core_DOM_Functions.thy
View File

@ -3670,6 +3670,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 \<turnstile> get_elements_by_class_name ptr name \<rightarrow>\<^sub>r results"
assumes "h \<turnstile> to_tree_order ptr \<rightarrow>\<^sub>r to"
assumes "element_ptr \<in> set results"
shows "cast element_ptr \<in> 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 \<turnstile> get_elements_by_tag_name ptr name \<rightarrow>\<^sub>r results"
assumes "h \<turnstile> to_tree_order ptr \<rightarrow>\<^sub>r to"
assumes "element_ptr \<in> set results"
shows "cast element_ptr \<in> 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