[STATEMENT]
lemma get_M_Mshadow_root_preserved4  [simp]:
  "h \<turnstile> put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr setter v \<rightarrow>\<^sub>h h'
   \<Longrightarrow> (\<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x))
   \<Longrightarrow> preserved (get_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr getter) h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h \<turnstile> put_M shadow_root_ptr setter v \<rightarrow>\<^sub>h h'; \<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x)\<rbrakk> \<Longrightarrow> preserved (get_M document_ptr getter) h h'
[PROOF STEP]
apply(cases "cast shadow_root_ptr \<noteq> document_ptr")[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h \<turnstile> put_M shadow_root_ptr setter v \<rightarrow>\<^sub>h h'; \<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x); cast shadow_root_ptr \<noteq> document_ptr\<rbrakk> \<Longrightarrow> preserved (get_M document_ptr getter) h h'
 2. \<lbrakk>h \<turnstile> put_M shadow_root_ptr setter v \<rightarrow>\<^sub>h h'; \<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x); \<not> cast shadow_root_ptr \<noteq> document_ptr\<rbrakk> \<Longrightarrow> preserved (get_M document_ptr getter) h h'
[PROOF STEP]
by(auto simp add: put_M_defs get_M_defs get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def
      DocumentMonad.get_M_defs preserved_def
      split: option.splits bind_splits dest: get_heap_E)