theory Retype_R

lemma descendants_of_retype':
  assumes P: "\<And>p. P p \<Longrightarrow> m p = None"
  shows "descendants_of' p (\<lambda>p. if P p then Some makeObject else m p) =
         descendants_of' p m" apply (rule set_eqI) apply (simp add: descendants_of'_def) apply (rule iffI) apply (erule subtree.induct) apply (rule direct_parent) apply (clarsimp simp: mdb_next_unfold makeObject_cte split: if_split_asm) apply assumption apply (clarsimp simp: parentOf_def makeObject_cte split: if_split_asm) apply (erule trans_parent) apply (clarsimp simp: mdb_next_unfold makeObject_cte split: if_split_asm) apply assumption apply (clarsimp simp: parentOf_def makeObject_cte split: if_split_asm) apply (erule subtree.induct) apply (rule direct_parent) apply (clarsimp simp: mdb_next_unfold dest!: P) apply assumption apply (fastforce simp: parentOf_def dest!: P) apply (erule trans_parent) apply (clarsimp simp: mdb_next_unfold dest!: P) apply assumption apply (fastforce simp: parentOf_def dest!: P) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of' p (\<lambda>p. if P p then Some makeObject else m p) = descendants_of' p m proof (prove)
goal (1 subgoal):
 1. \<And>x. (x \<in> descendants_of' p (\<lambda>p. if P p then Some makeObject else m p)) = (x \<in> descendants_of' p m) proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (prove)
goal (2 subgoals):
 1. \<And>x. (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> x \<Longrightarrow> m \<turnstile> p \<rightarrow> x
 2. \<And>x. m \<turnstile> p \<rightarrow> x \<Longrightarrow> (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> x proof (prove)
goal (3 subgoals):
 1. \<And>x c'. \<lbrakk>(\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<leadsto> c'; c' \<noteq> 0; \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'
 2. \<And>x c' c''. \<lbrakk>(\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c'; (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c''
 3. \<And>x. m \<turnstile> p \<rightarrow> x \<Longrightarrow> (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> x proof (prove)
goal (5 subgoals):
 1. \<And>x c'. \<lbrakk>(\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<leadsto> c'; c' \<noteq> 0; \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> c'
 2. \<And>x c'. \<lbrakk>(\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<leadsto> c'; c' \<noteq> 0; \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<And>x c'. \<lbrakk>(\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<leadsto> c'; c' \<noteq> 0; \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c'
 4. \<And>x c' c''. \<lbrakk>(\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c'; (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c''
 5. \<And>x. m \<turnstile> p \<rightarrow> x \<Longrightarrow> (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> x proof (prove)
goal (4 subgoals):
 1. \<And>x c'. \<lbrakk>(\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<leadsto> c'; c' \<noteq> 0; \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 2. \<And>x c'. \<lbrakk>(\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<leadsto> c'; c' \<noteq> 0; \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c'
 3. \<And>x c' c''. \<lbrakk>(\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c'; (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c''
 4. \<And>x. m \<turnstile> p \<rightarrow> x \<Longrightarrow> (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> x proof (prove)
goal (3 subgoals):
 1. \<And>x c'. \<lbrakk>(\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<leadsto> c'; c' \<noteq> 0; \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c'
 2. \<And>x c' c''. \<lbrakk>(\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c'; (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c''
 3. \<And>x. m \<turnstile> p \<rightarrow> x \<Longrightarrow> (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> x proof (prove)
goal (2 subgoals):
 1. \<And>x c' c''. \<lbrakk>(\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c'; (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c''
 2. \<And>x. m \<turnstile> p \<rightarrow> x \<Longrightarrow> (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> x proof (prove)
goal (4 subgoals):
 1. \<And>x c' c''. \<lbrakk>(\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> c'; (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> c' \<leadsto> c''
 2. \<And>x c' c''. \<lbrakk>(\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> c'; (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 3. \<And>x c' c''. \<lbrakk>(\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> c'; (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c''
 4. \<And>x. m \<turnstile> p \<rightarrow> x \<Longrightarrow> (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> x proof (prove)
goal (3 subgoals):
 1. \<And>x c' c''. \<lbrakk>(\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> c'; (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 2. \<And>x c' c''. \<lbrakk>(\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> c'; (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c''
 3. \<And>x. m \<turnstile> p \<rightarrow> x \<Longrightarrow> (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> x proof (prove)
goal (2 subgoals):
 1. \<And>x c' c''. \<lbrakk>(\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> c'; (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c''
 2. \<And>x. m \<turnstile> p \<rightarrow> x \<Longrightarrow> (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> x proof (prove)
goal (1 subgoal):
 1. \<And>x. m \<turnstile> p \<rightarrow> x \<Longrightarrow> (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> x proof (prove)
goal (2 subgoals):
 1. \<And>x c'. \<lbrakk>m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> c'
 2. \<And>x c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> c'' proof (prove)
goal (4 subgoals):
 1. \<And>x c'. \<lbrakk>m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<leadsto> c'
 2. \<And>x c'. \<lbrakk>m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<And>x c'. \<lbrakk>m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c'
 4. \<And>x c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> c'' proof (prove)
goal (3 subgoals):
 1. \<And>x c'. \<lbrakk>m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 2. \<And>x c'. \<lbrakk>m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c'
 3. \<And>x c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> c'' proof (prove)
goal (2 subgoals):
 1. \<And>x c'. \<lbrakk>m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c'
 2. \<And>x c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> c'' proof (prove)
goal (1 subgoal):
 1. \<And>x c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> p \<rightarrow> c'' proof (prove)
goal (3 subgoals):
 1. \<And>x c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> (\<lambda>p. if P p then Some makeObject else m p) \<turnstile> c' \<leadsto> c''
 2. \<And>x c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 3. \<And>x c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c'' proof (prove)
goal (2 subgoals):
 1. \<And>x c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 2. \<And>x c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c'' proof (prove)
goal (1 subgoal):
 1. \<And>x c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> \<lambda>p. if P p then Some makeObject else m p \<turnstile> p parentOf c'' proof (prove)
goal:
No subgoals!