theory Separation

lemma bisim_separate_cap_cases:
  assumes nc: "cap = NullCap \<Longrightarrow> bisim R Pn Pn' m m'"
  and     ac: "\<And>ptr badge rights. \<lbrakk> cap = NotificationCap ptr badge rights \<rbrakk>
               \<Longrightarrow> bisim R (Pa ptr badge rights) (Pa' ptr badge rights) m m'"
  shows   "bisim R (\<lambda>s. (cap = NullCap \<longrightarrow> Pn s)
                    \<and> (\<forall>ptr badge rights. cap = NotificationCap ptr badge rights \<longrightarrow> Pa ptr badge rights s))
                   ((\<lambda>s. (cap = NullCap \<longrightarrow> Pn' s)
                    \<and> (\<forall>ptr badge rights. cap = NotificationCap ptr badge rights \<longrightarrow> Pa' ptr badge rights s))
                       and K (separate_cap cap)) m m'" using assms apply - apply (rule bisim_gen_asm_r) apply (erule separate_capE, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim R (\<lambda>s. (cap = NullCap \<longrightarrow> Pn s) \<and> (\<forall>ptr badge rights. cap = NotificationCap ptr badge rights \<longrightarrow> Pa ptr badge rights s)) ((\<lambda>s. (cap = NullCap \<longrightarrow> Pn' s) \<and> (\<forall>ptr badge rights. cap = NotificationCap ptr badge rights \<longrightarrow> Pa' ptr badge rights s)) and K (separate_cap cap)) m m' proof (prove)
using this:
cap = NullCap \<Longrightarrow> bisim R Pn Pn' m m'
cap = NotificationCap ?ptr ?badge ?rights \<Longrightarrow> bisim R (Pa ?ptr ?badge ?rights) (Pa' ?ptr ?badge ?rights) m m'

goal (1 subgoal):
 1. bisim R (\<lambda>s. (cap = NullCap \<longrightarrow> Pn s) \<and> (\<forall>ptr badge rights. cap = NotificationCap ptr badge rights \<longrightarrow> Pa ptr badge rights s)) ((\<lambda>s. (cap = NullCap \<longrightarrow> Pn' s) \<and> (\<forall>ptr badge rights. cap = NotificationCap ptr badge rights \<longrightarrow> Pa' ptr badge rights s)) and K (separate_cap cap)) m m' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap = NullCap \<Longrightarrow> bisim R Pn Pn' m m'; \<And>ptr badge rights. cap = NotificationCap ptr badge rights \<Longrightarrow> bisim R (Pa ptr badge rights) (Pa' ptr badge rights) m m'\<rbrakk> \<Longrightarrow> bisim R (\<lambda>s. (cap = NullCap \<longrightarrow> Pn s) \<and> (\<forall>ptr badge rights. cap = NotificationCap ptr badge rights \<longrightarrow> Pa ptr badge rights s)) ((\<lambda>s. (cap = NullCap \<longrightarrow> Pn' s) \<and> (\<forall>ptr badge rights. cap = NotificationCap ptr badge rights \<longrightarrow> Pa' ptr badge rights s)) and K (separate_cap cap)) m m' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap = NullCap \<Longrightarrow> bisim R Pn Pn' m m'; \<And>ptr badge rights. cap = NotificationCap ptr badge rights \<Longrightarrow> bisim R (Pa ptr badge rights) (Pa' ptr badge rights) m m'; separate_cap cap\<rbrakk> \<Longrightarrow> bisim R (\<lambda>s. (cap = NullCap \<longrightarrow> Pn s) \<and> (\<forall>ptr badge rights. cap = NotificationCap ptr badge rights \<longrightarrow> Pa ptr badge rights s)) (\<lambda>s. (cap = NullCap \<longrightarrow> Pn' s) \<and> (\<forall>ptr badge rights. cap = NotificationCap ptr badge rights \<longrightarrow> Pa' ptr badge rights s)) m m' proof (prove)
goal:
No subgoals!