theory FinalCaps

lemma finalise_cap_ret_intra_label_cap:
  "\<lbrace>\<lambda>s. cap_points_to_label aag cap l\<rbrace>
   finalise_cap cap blah
   \<lbrace>\<lambda>rv s :: det_state. cap_points_to_label aag (fst rv) l\<rbrace>" apply (clarsimp simp: cap_points_to_label_def valid_def) apply (rule conjI) apply (erule ball_subset) apply (drule use_valid[OF _ finalise_cap_ret_subset_obj_refs]) apply (rule refl) apply simp apply (erule ball_subset) apply (drule use_valid[OF _ finalise_cap_ret_subset_cap_irqs]) apply (rule refl) by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cap_points_to_label aag cap l\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. cap_points_to_label aag (fst rv) l\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b ba. \<lbrakk>((a, b), ba) \<in> fst (finalise_cap cap blah s); \<forall>x\<in>obj_refs cap. pasObjectAbs aag x = l; \<forall>x\<in>cap_irqs cap. pasIRQAbs aag x = l\<rbrakk> \<Longrightarrow> (\<forall>x\<in>obj_refs a. pasObjectAbs aag x = l) \<and> (\<forall>x\<in>cap_irqs a. pasIRQAbs aag x = l) proof (prove)
goal (2 subgoals):
 1. \<And>s a b ba. \<lbrakk>((a, b), ba) \<in> fst (finalise_cap cap blah s); \<forall>x\<in>obj_refs cap. pasObjectAbs aag x = l; \<forall>x\<in>cap_irqs cap. pasIRQAbs aag x = l\<rbrakk> \<Longrightarrow> \<forall>x\<in>obj_refs a. pasObjectAbs aag x = l
 2. \<And>s a b ba. \<lbrakk>((a, b), ba) \<in> fst (finalise_cap cap blah s); \<forall>x\<in>obj_refs cap. pasObjectAbs aag x = l; \<forall>x\<in>cap_irqs cap. pasIRQAbs aag x = l\<rbrakk> \<Longrightarrow> \<forall>x\<in>cap_irqs a. pasIRQAbs aag x = l proof (prove)
goal (2 subgoals):
 1. \<And>s a b ba. \<lbrakk>((a, b), ba) \<in> fst (finalise_cap cap blah s); \<forall>x\<in>cap_irqs cap. pasIRQAbs aag x = l\<rbrakk> \<Longrightarrow> obj_refs a \<subseteq> obj_refs cap
 2. \<And>s a b ba. \<lbrakk>((a, b), ba) \<in> fst (finalise_cap cap blah s); \<forall>x\<in>obj_refs cap. pasObjectAbs aag x = l; \<forall>x\<in>cap_irqs cap. pasIRQAbs aag x = l\<rbrakk> \<Longrightarrow> \<forall>x\<in>cap_irqs a. pasIRQAbs aag x = l proof (prove)
goal (3 subgoals):
 1. \<And>s a b ba. \<forall>x\<in>cap_irqs cap. pasIRQAbs aag x = l \<Longrightarrow> obj_refs cap = ?X17 s a b ba
 2. \<And>s a b ba. \<lbrakk>\<forall>x\<in>cap_irqs cap. pasIRQAbs aag x = l; obj_refs (fst (a, b)) \<subseteq> ?X17 s a b ba\<rbrakk> \<Longrightarrow> obj_refs a \<subseteq> obj_refs cap
 3. \<And>s a b ba. \<lbrakk>((a, b), ba) \<in> fst (finalise_cap cap blah s); \<forall>x\<in>obj_refs cap. pasObjectAbs aag x = l; \<forall>x\<in>cap_irqs cap. pasIRQAbs aag x = l\<rbrakk> \<Longrightarrow> \<forall>x\<in>cap_irqs a. pasIRQAbs aag x = l proof (prove)
goal (2 subgoals):
 1. \<And>s a b ba. \<lbrakk>\<forall>x\<in>cap_irqs cap. pasIRQAbs aag x = l; obj_refs (fst (a, b)) \<subseteq> obj_refs cap\<rbrakk> \<Longrightarrow> obj_refs a \<subseteq> obj_refs cap
 2. \<And>s a b ba. \<lbrakk>((a, b), ba) \<in> fst (finalise_cap cap blah s); \<forall>x\<in>obj_refs cap. pasObjectAbs aag x = l; \<forall>x\<in>cap_irqs cap. pasIRQAbs aag x = l\<rbrakk> \<Longrightarrow> \<forall>x\<in>cap_irqs a. pasIRQAbs aag x = l proof (prove)
goal (1 subgoal):
 1. \<And>s a b ba. \<lbrakk>((a, b), ba) \<in> fst (finalise_cap cap blah s); \<forall>x\<in>obj_refs cap. pasObjectAbs aag x = l; \<forall>x\<in>cap_irqs cap. pasIRQAbs aag x = l\<rbrakk> \<Longrightarrow> \<forall>x\<in>cap_irqs a. pasIRQAbs aag x = l proof (prove)
goal (1 subgoal):
 1. \<And>s a b ba. \<lbrakk>((a, b), ba) \<in> fst (finalise_cap cap blah s); \<forall>x\<in>obj_refs cap. pasObjectAbs aag x = l\<rbrakk> \<Longrightarrow> cap_irqs a \<subseteq> cap_irqs cap proof (prove)
goal (2 subgoals):
 1. \<And>s a b ba. \<forall>x\<in>obj_refs cap. pasObjectAbs aag x = l \<Longrightarrow> cap_irqs cap = ?X23 s a b ba
 2. \<And>s a b ba. \<lbrakk>\<forall>x\<in>obj_refs cap. pasObjectAbs aag x = l; cap_irqs (fst (a, b)) \<subseteq> ?X23 s a b ba\<rbrakk> \<Longrightarrow> cap_irqs a \<subseteq> cap_irqs cap proof (prove)
goal (1 subgoal):
 1. \<And>s a b ba. \<lbrakk>\<forall>x\<in>obj_refs cap. pasObjectAbs aag x = l; cap_irqs (fst (a, b)) \<subseteq> cap_irqs cap\<rbrakk> \<Longrightarrow> cap_irqs a \<subseteq> cap_irqs cap