theory Retype_R

lemma null_filter_parentOf:
  "\<lbrakk> null_filter' xs = null_filter' ys; xs \<turnstile> x parentOf y \<rbrakk>
      \<Longrightarrow> ys \<turnstile> x parentOf y" apply (clarsimp simp add: parentOf_def) apply (rule across_null_filter_eq'[where x=x], assumption+) apply (erule(1) across_null_filter_eq') apply clarsimp apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>null_filter' xs = null_filter' ys; xs \<turnstile> x parentOf y\<rbrakk> \<Longrightarrow> ys \<turnstile> x parentOf y proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte. \<lbrakk>null_filter' xs = null_filter' ys; xs y = Some cte; xs x = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> \<exists>cte' cte. ys y = Some cte \<and> ys x = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (2 subgoals):
 1. \<And>cte' cte. \<lbrakk>null_filter' xs = null_filter' ys; xs y = Some cte; xs x = Some cte'; isMDBParentOf cte' cte; ys x = Some cte'\<rbrakk> \<Longrightarrow> \<exists>cte' cte. ys y = Some cte \<and> ys x = Some cte' \<and> isMDBParentOf cte' cte
 2. \<And>cte' cte. \<lbrakk>null_filter' xs = null_filter' ys; xs y = Some cte; xs x = Some cte'; isMDBParentOf cte' cte; cte' = CTE capability.NullCap nullMDBNode; ys x = None\<rbrakk> \<Longrightarrow> \<exists>cte' cte. ys y = Some cte \<and> ys x = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (3 subgoals):
 1. \<And>cte' cte. \<lbrakk>xs y = Some cte; xs x = Some cte'; isMDBParentOf cte' cte; ys x = Some cte'; ys y = Some cte\<rbrakk> \<Longrightarrow> \<exists>cte' cte. ys y = Some cte \<and> ys x = Some cte' \<and> isMDBParentOf cte' cte
 2. \<And>cte' cte. \<lbrakk>xs y = Some cte; xs x = Some cte'; isMDBParentOf cte' cte; ys x = Some cte'; cte = CTE capability.NullCap nullMDBNode; ys y = None\<rbrakk> \<Longrightarrow> \<exists>cte' cte. ys y = Some cte \<and> ys x = Some cte' \<and> isMDBParentOf cte' cte
 3. \<And>cte' cte. \<lbrakk>null_filter' xs = null_filter' ys; xs y = Some cte; xs x = Some cte'; isMDBParentOf cte' cte; cte' = CTE capability.NullCap nullMDBNode; ys x = None\<rbrakk> \<Longrightarrow> \<exists>cte' cte. ys y = Some cte \<and> ys x = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (2 subgoals):
 1. \<And>cte' cte. \<lbrakk>xs y = Some cte; xs x = Some cte'; isMDBParentOf cte' cte; ys x = Some cte'; cte = CTE capability.NullCap nullMDBNode; ys y = None\<rbrakk> \<Longrightarrow> \<exists>cte' cte. ys y = Some cte \<and> ys x = Some cte' \<and> isMDBParentOf cte' cte
 2. \<And>cte' cte. \<lbrakk>null_filter' xs = null_filter' ys; xs y = Some cte; xs x = Some cte'; isMDBParentOf cte' cte; cte' = CTE capability.NullCap nullMDBNode; ys x = None\<rbrakk> \<Longrightarrow> \<exists>cte' cte. ys y = Some cte \<and> ys x = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte. \<lbrakk>null_filter' xs = null_filter' ys; xs y = Some cte; xs x = Some cte'; isMDBParentOf cte' cte; cte' = CTE capability.NullCap nullMDBNode; ys x = None\<rbrakk> \<Longrightarrow> \<exists>cte' cte. ys y = Some cte \<and> ys x = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal:
No subgoals!