[STATEMENT]
lemma adopt_node_types_preserved:
  assumes "w \<in> adopt_node_locs parent owner_document document_ptr"
  assumes "h \<turnstile> w \<rightarrow>\<^sub>h h'"
  shows "type_wf h = type_wf h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. type_wf h = type_wf h'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
w \<in> adopt_node_locs parent owner_document document_ptr
h \<turnstile> w \<rightarrow>\<^sub>h h'

goal (1 subgoal):
 1. type_wf h = type_wf h'
[PROOF STEP]
using remove_child_types_preserved
[PROOF STATE]
proof (prove)
using this:
w \<in> adopt_node_locs parent owner_document document_ptr
h \<turnstile> w \<rightarrow>\<^sub>h h'
\<lbrakk>?w \<in> remove_child_locs ?ptr ?owner_document; ?h \<turnstile> ?w \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> type_wf ?h = type_wf ?h'

goal (1 subgoal):
 1. type_wf h = type_wf h'
[PROOF STEP]
using set_disconnected_nodes_types_preserved
[PROOF STATE]
proof (prove)
using this:
w \<in> adopt_node_locs parent owner_document document_ptr
h \<turnstile> w \<rightarrow>\<^sub>h h'
\<lbrakk>?w \<in> remove_child_locs ?ptr ?owner_document; ?h \<turnstile> ?w \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> type_wf ?h = type_wf ?h'
\<lbrakk>?w \<in> set_disconnected_nodes_locs ?document_ptr; ?h \<turnstile> ?w \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> type_wf ?h = type_wf ?h'

goal (1 subgoal):
 1. type_wf h = type_wf h'
[PROOF STEP]
unfolding adopt_node_locs_def
[PROOF STATE]
proof (prove)
using this:
w \<in> (if parent = None then {} else remove_child_locs (the parent) owner_document) \<union> set_disconnected_nodes_locs document_ptr \<union> set_disconnected_nodes_locs owner_document
h \<turnstile> w \<rightarrow>\<^sub>h h'
\<lbrakk>?w \<in> remove_child_locs ?ptr ?owner_document; ?h \<turnstile> ?w \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> type_wf ?h = type_wf ?h'
\<lbrakk>?w \<in> set_disconnected_nodes_locs ?document_ptr; ?h \<turnstile> ?w \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> type_wf ?h = type_wf ?h'

goal (1 subgoal):
 1. type_wf h = type_wf h'
[PROOF STEP]
by (auto split: if_splits)