theory Invariants_AI

lemma unique_reply_capsD:
  "\<lbrakk> unique_reply_caps cs; reply_masters_mdb m cs;
     cs master = Some (ReplyCap t True rights);
     sl\<in>descendants_of master m; sl'\<in>descendants_of master m \<rbrakk>
   \<Longrightarrow> sl = sl'" apply (simp add: reply_masters_mdb_def
           del: split_paired_All) apply (drule_tac x=master in spec) apply (drule_tac x=t in spec) apply (clarsimp simp del: split_paired_All) apply (frule_tac x=sl in bspec,assumption) apply (drule_tac x=sl' in bspec,assumption) by (clarsimp simp add: unique_reply_caps_def is_cap_simps
           simp del: split_paired_All)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unique_reply_caps cs; reply_masters_mdb m cs; cs master = Some (ReplyCap t True rights); sl \<in> descendants_of master m; sl' \<in> descendants_of master m\<rbrakk> \<Longrightarrow> sl = sl' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unique_reply_caps cs; \<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t True rights)) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); cs master = Some (ReplyCap t True rights); sl \<in> descendants_of master m; sl' \<in> descendants_of master m\<rbrakk> \<Longrightarrow> sl = sl' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unique_reply_caps cs; cs master = Some (ReplyCap t True rights); sl \<in> descendants_of master m; sl' \<in> descendants_of master m; \<forall>t. (\<exists>rights. cs master = Some (ReplyCap t True rights)) \<longrightarrow> m master = None \<and> (\<forall>ptr'\<in>descendants_of master m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))\<rbrakk> \<Longrightarrow> sl = sl' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unique_reply_caps cs; cs master = Some (ReplyCap t True rights); sl \<in> descendants_of master m; sl' \<in> descendants_of master m; (\<exists>rights. cs master = Some (ReplyCap t True rights)) \<longrightarrow> m master = None \<and> (\<forall>ptr'\<in>descendants_of master m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))\<rbrakk> \<Longrightarrow> sl = sl' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unique_reply_caps cs; cs master = Some (ReplyCap t True rights); sl \<in> descendants_of master m; sl' \<in> descendants_of master m; m master = None; \<forall>ptr'\<in>descendants_of master m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> sl = sl' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unique_reply_caps cs; cs master = Some (ReplyCap t True rights); sl \<in> descendants_of master m; sl' \<in> descendants_of master m; m master = None; \<forall>ptr'\<in>descendants_of master m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'); \<exists>rights'. cs sl = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> sl = sl' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unique_reply_caps cs; cs master = Some (ReplyCap t True rights); sl \<in> descendants_of master m; sl' \<in> descendants_of master m; m master = None; \<exists>rights'. cs sl = Some (ReplyCap t False rights'); \<exists>rights'. cs sl' = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> sl = sl'