Added missing character data stuff.

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 \<Rightarrow> ((_) heap, exception, (_) node_ptr list) prog"
+  and get_disconnected_nodes_locs :: "(_) document_ptr \<Rightarrow> ((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
+  and set_disconnected_nodes :: "(_) document_ptr \<Rightarrow> (_) node_ptr list \<Rightarrow> ((_) heap, exception, unit) prog"
+  and set_disconnected_nodes_locs :: "(_) document_ptr \<Rightarrow> ((_) heap, exception, unit) prog set"
+  and set_val :: "(_) character_data_ptr \<Rightarrow> char list \<Rightarrow> ((_) heap, exception, unit) prog"
+  and set_val_locs :: "(_) character_data_ptr \<Rightarrow> ((_) heap, exception, unit) prog set"
+  and type_wf :: "(_) heap \<Rightarrow> bool"
+  and create_character_data :: "(_) document_ptr \<Rightarrow> char list \<Rightarrow> ((_) heap, exception, (_) character_data_ptr) prog"
+  and known_ptr :: "(_) object_ptr \<Rightarrow> 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 \<turnstile> create_character_data document_ptr tag \<rightarrow>\<^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 \<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 

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 \<open>create\_document\<close>