[STATEMENT]
lemma set_shadow_root_ok: "type_wf h \<Longrightarrow> element_ptr |\<in>| element_ptr_kinds h \<Longrightarrow> h \<turnstile> ok (set_shadow_root element_ptr tag)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>type_wf h; element_ptr |\<in>| element_ptr_kinds h\<rbrakk> \<Longrightarrow> h \<turnstile> ok set_shadow_root element_ptr tag
[PROOF STEP]
apply(unfold type_wf_impl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ShadowRootClass.type_wf h; element_ptr |\<in>| element_ptr_kinds h\<rbrakk> \<Longrightarrow> h \<turnstile> ok set_shadow_root element_ptr tag
[PROOF STEP]
unfolding set_shadow_root_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ShadowRootClass.type_wf h; element_ptr |\<in>| element_ptr_kinds h\<rbrakk> \<Longrightarrow> h \<turnstile> ok put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr shadow_root_opt_update tag
[PROOF STEP]
using get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ok put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ok
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>ShadowRootClass.type_wf ?h; ?ptr |\<in>| element_ptr_kinds ?h\<rbrakk> \<Longrightarrow> ?h \<turnstile> ok get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t ?ptr ?getter
\<lbrakk>ShadowRootClass.type_wf ?h; ?ptr |\<in>| element_ptr_kinds ?h\<rbrakk> \<Longrightarrow> ?h \<turnstile> ok put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t ?ptr ?setter ?v

goal (1 subgoal):
 1. \<lbrakk>ShadowRootClass.type_wf h; element_ptr |\<in>| element_ptr_kinds h\<rbrakk> \<Longrightarrow> h \<turnstile> ok put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr shadow_root_opt_update tag
[PROOF STEP]
by (simp add: ShadowRootMonad.put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ok)