Preparing AFP update.

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

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 (\<Union>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)
+    document_ptr_kinds_def preserved_def cong del: image_cong_simp)
-  by (smt object_ptr_kinds_preserved_small preserved_def unit_all_impI)
+  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"

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 (\<Union>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)
+    node_ptr_kinds_M_reads preserved_def cong del: image_cong_simp)
-  by (smt filter_fset node_ptr_kinds_small preserved_def unit_all_impI)
+  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"

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

Core_DOM/Core_DOM/common/preliminaries/Testing_Utils.thy

@@ -30,7 +30,6 @@
 theory Testing_Utils
   imports Main
 begin
-
 ML \<open>
 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
+end

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 \<Longrightarrow> type_wf h \<Longrightarrow> known_ptrs h 
                           \<Longrightarrow> h \<turnstile> get_root_node ptr \<rightarrow>\<^sub>r cast child \<Longrightarrow> h \<turnstile> get_parent child \<rightarrow>\<^sub>r None"
-  (* assumes get_root_node_not_node_same: 
-    "ptr |\<in>| object_ptr_kinds h \<Longrightarrow> \<not>is_node_ptr_kind ptr 
-                                \<Longrightarrow> h \<turnstile> get_root_node ptr \<rightarrow>\<^sub>r ptr" *)
   assumes get_root_node_parent_same: 
     "h \<turnstile> get_parent child \<rightarrow>\<^sub>r Some ptr 
         \<Longrightarrow> h \<turnstile> get_root_node (cast child) \<rightarrow>\<^sub>r root \<longleftrightarrow> h \<turnstile> get_root_node ptr \<rightarrow>\<^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: "\<forall>node_ptr\<in>fset (node_ptr_kinds h'). (\<exists>document_ptr. document_ptr |\<in>| document_ptr_kinds h' \<and> node_ptr \<in> set |h \<turnstile> get_disconnected_nodes document_ptr|\<^sub>r) \<or> (\<exists>parent_ptr. parent_ptr |\<in>| object_ptr_kinds h' \<and> node_ptr \<in> set |h \<turnstile> get_child_nodes parent_ptr|\<^sub>r)"
     and 1: "node_ptr |\<in>| 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) \<open>type_wf h'\<close> 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 \<open>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 \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close> \<open>local.a_all_ptrs_in_heap h\<close> 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)
+       apply (metis (no_types) NodeMonad.ptr_kinds_ptr_kinds_M 
-      by (smt NodeMonad.ptr_kinds_ptr_kinds_M \<open>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 \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close> \<open>local.a_all_ptrs_in_heap h\<close> 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)
+                    \<open>a_all_ptrs_in_heap h\<close> 
+                    \<open>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 \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close> 
+                    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 
+                   \<open>a_all_ptrs_in_heap h\<close> 
+                   \<open>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 \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close> 
+                   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: "(\<Union>x\<in>fset (object_ptr_kinds h3). set |h' \<turnstile> 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 \<open>cast new_character_data_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close> 
           \<open>h2 \<turnstile> get_child_nodes (cast new_character_data_ptr) \<rightarrow>\<^sub>r []\<close>
-    apply (metis (no_types, lifting) NodeMonad.ptr_kinds_ptr_kinds_M \<open>parent_child_rel h = parent_child_rel h2\<close> 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)
+     apply (metis (no_types, hide_lams) children_eq_h fempty_iff fset_mp fset_of_list_simps(1) 
-    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)
+                  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 "\<And>p. p |\<in>| object_ptr_kinds h \<Longrightarrow> cast new_character_data_ptr \<notin> set |h \<turnstile> get_child_nodes p|\<^sub>r"
     using \<open>heap_is_wellformed h\<close> \<open>cast new_character_data_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close>
@@ -7409,7 +7428,25 @@ proof -
     moreover have "set |h3 \<turnstile> get_disconnected_nodes x|\<^sub>r \<inter> set |h3 \<turnstile> 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 \<open>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 \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close> \<open>local.a_all_ptrs_in_heap h\<close> 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 \<open>a_all_ptrs_in_heap h\<close> 
+                                \<open>cast new_character_data_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close> 
+                                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 
+                   \<open>a_all_ptrs_in_heap h\<close> \<open>cast new_character_data_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close> 
+                   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: "(\<Union>x\<in>fset (object_ptr_kinds h3). set |h' \<turnstile> 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) \<open>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 \<notin> set |h \<turnstile> object_ptr_kinds_M|\<^sub>r\<close> 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)
+    by (metis (no_types, lifting) ObjectMonad.ptr_kinds_ptr_kinds_M
-
+                \<open>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 \<notin> set |h \<turnstile> object_ptr_kinds_M|\<^sub>r\<close> 
-  have "known_ptr (cast new_character_data_ptr)"
+                children_eq2_h disconnected_nodes_eq2_h3 document_ptr_kinds_eq_h h' list.set_intros(2) 
-    using \<open>h \<turnstile> create_character_data document_ptr text \<rightarrow>\<^sub>r new_character_data_ptr\<close> local.create_character_data_known_ptr by blast
+                local.set_disconnected_nodes_get_disconnected_nodes select_result_I2)
-  then
-  have "known_ptrs h2"
-    using known_ptrs_new_ptr object_ptr_kinds_eq_h \<open>known_ptrs h\<close> 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
 
   show "heap_is_wellformed h'"
     using \<open>a_acyclic_heap h'\<close> \<open>a_all_ptrs_in_heap h'\<close> \<open>a_distinct_lists h'\<close> \<open>a_owner_document_valid h'\<close>
@@ -7620,13 +7647,19 @@ proof -
     using \<open>heap_is_wellformed h\<close>  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 
       \<open>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 \<notin> set |h \<turnstile> object_ptr_kinds_M|\<^sub>r\<close> 
       \<open>parent_child_rel h = parent_child_rel h'\<close> 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
+                  local.parent_child_rel_parent_in_heap node_ptr_kinds_eq)
-     apply (metis (no_types, lifting) \<open>h' \<turnstile> 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) \<rightarrow>\<^sub>r []\<close> 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) ObjectMonad.ptr_kinds_ptr_kinds_M 
-    by (metis (no_types, lifting) \<open>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 |\<notin>| object_ptr_kinds h\<close> \<open>h' \<turnstile> 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) \<rightarrow>\<^sub>r []\<close> \<open>h' \<turnstile> get_disconnected_nodes new_document_ptr \<rightarrow>\<^sub>r []\<close> \<open>parent_child_rel h = parent_child_rel h'\<close> \<open>type_wf h'\<close> 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) 
+                  \<open>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 \<notin> set |h \<turnstile> object_ptr_kinds_M|\<^sub>r\<close> 
+                  \<open>h' \<turnstile> 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) \<rightarrow>\<^sub>r []\<close> 
+                  \<open>parent_child_rel h = parent_child_rel h'\<close> 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 \<open>heap_is_wellformed h\<close> 
@@ -7695,7 +7728,12 @@ proof -
     using \<open>heap_is_wellformed h\<close>  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 \<open>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 |\<notin>| object_ptr_kinds h\<close> 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 \<open>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 |\<notin>| object_ptr_kinds h\<close> 
+              \<open>new_document_ptr |\<notin>| document_ptr_kinds h\<close> 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 \<open>a_acyclic_heap h'\<close> \<open>a_all_ptrs_in_heap h'\<close> \<open>a_distinct_lists h'\<close> \<open>a_owner_document_valid h'\<close>

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},
+} 

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"

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

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 (\<Union>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)
+    document_ptr_kinds_def preserved_def cong del: image_cong_simp)
-  by (smt object_ptr_kinds_preserved_small preserved_def unit_all_impI)
+  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"

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 (\<Union>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)
+    node_ptr_kinds_M_reads preserved_def cong del: image_cong_simp)
-  by (smt filter_fset node_ptr_kinds_small preserved_def unit_all_impI)
+  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"

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

Core_DOM/Core_DOM_Scope_Components/common/preliminaries/Testing_Utils.thy

@@ -30,7 +30,6 @@
 theory Testing_Utils
   imports Main
 begin
-
 ML \<open>
 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
+end