theory Retype_R

lemma across_null_filter_eq':
  assumes eq: "null_filter' xs = null_filter' ys"
  shows "\<lbrakk> xs x = Some v; ys x = Some v \<Longrightarrow> R;
           \<lbrakk> v = CTE NullCap nullMDBNode; ys x = None \<rbrakk> \<Longrightarrow> R \<rbrakk>
            \<Longrightarrow> R" apply (cases "null_filter' xs x") apply (subgoal_tac "null_filter' ys x = None") apply (simp add: null_filter'_def split: if_split_asm) apply (simp add: eq) apply (subgoal_tac "null_filter' ys x = Some a") apply (simp add: null_filter'_def split: if_split_asm) apply (simp add: eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs x = Some v; ys x = Some v \<Longrightarrow> R; \<lbrakk>v = CTE capability.NullCap nullMDBNode; ys x = None\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xs x = Some v; ys x = Some v \<Longrightarrow> R; \<lbrakk>v = CTE capability.NullCap nullMDBNode; ys x = None\<rbrakk> \<Longrightarrow> R; null_filter' xs x = None\<rbrakk> \<Longrightarrow> R
 2. \<And>a. \<lbrakk>xs x = Some v; ys x = Some v \<Longrightarrow> R; \<lbrakk>v = CTE capability.NullCap nullMDBNode; ys x = None\<rbrakk> \<Longrightarrow> R; null_filter' xs x = Some a\<rbrakk> \<Longrightarrow> R proof (prove)
goal (3 subgoals):
 1. \<lbrakk>xs x = Some v; ys x = Some v \<Longrightarrow> R; \<lbrakk>v = CTE capability.NullCap nullMDBNode; ys x = None\<rbrakk> \<Longrightarrow> R; null_filter' xs x = None; null_filter' ys x = None\<rbrakk> \<Longrightarrow> R
 2. \<lbrakk>xs x = Some v; ys x = Some v \<Longrightarrow> R; \<lbrakk>v = CTE capability.NullCap nullMDBNode; ys x = None\<rbrakk> \<Longrightarrow> R; null_filter' xs x = None\<rbrakk> \<Longrightarrow> null_filter' ys x = None
 3. \<And>a. \<lbrakk>xs x = Some v; ys x = Some v \<Longrightarrow> R; \<lbrakk>v = CTE capability.NullCap nullMDBNode; ys x = None\<rbrakk> \<Longrightarrow> R; null_filter' xs x = Some a\<rbrakk> \<Longrightarrow> R proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xs x = Some v; ys x = Some v \<Longrightarrow> R; \<lbrakk>v = CTE capability.NullCap nullMDBNode; ys x = None\<rbrakk> \<Longrightarrow> R; null_filter' xs x = None\<rbrakk> \<Longrightarrow> null_filter' ys x = None
 2. \<And>a. \<lbrakk>xs x = Some v; ys x = Some v \<Longrightarrow> R; \<lbrakk>v = CTE capability.NullCap nullMDBNode; ys x = None\<rbrakk> \<Longrightarrow> R; null_filter' xs x = Some a\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>xs x = Some v; ys x = Some v \<Longrightarrow> R; \<lbrakk>v = CTE capability.NullCap nullMDBNode; ys x = None\<rbrakk> \<Longrightarrow> R; null_filter' xs x = Some a\<rbrakk> \<Longrightarrow> R proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>xs x = Some v; ys x = Some v \<Longrightarrow> R; \<lbrakk>v = CTE capability.NullCap nullMDBNode; ys x = None\<rbrakk> \<Longrightarrow> R; null_filter' xs x = Some a; null_filter' ys x = Some a\<rbrakk> \<Longrightarrow> R
 2. \<And>a. \<lbrakk>xs x = Some v; ys x = Some v \<Longrightarrow> R; \<lbrakk>v = CTE capability.NullCap nullMDBNode; ys x = None\<rbrakk> \<Longrightarrow> R; null_filter' xs x = Some a\<rbrakk> \<Longrightarrow> null_filter' ys x = Some a proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>xs x = Some v; ys x = Some v \<Longrightarrow> R; \<lbrakk>v = CTE capability.NullCap nullMDBNode; ys x = None\<rbrakk> \<Longrightarrow> R; null_filter' xs x = Some a\<rbrakk> \<Longrightarrow> null_filter' ys x = Some a proof (prove)
goal:
No subgoals!