theory Retype_AI

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 = cap.NullCap; 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 = NullCap; 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 = NullCap; 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 = NullCap; 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 = NullCap; 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 = NullCap; 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 = NullCap; 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 = NullCap; 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 = NullCap; 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 = NullCap; 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 = NullCap; 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 = NullCap; 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 = NullCap; 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!