theory CSpace_AI

lemma free_index_update_reply_master_revocable[simp]:
  "ms src = Some src_cap \<Longrightarrow>
   reply_master_revocable P (ms(src \<mapsto> src_cap\<lparr>free_index:=a\<rparr>)) =
   reply_master_revocable P ms" unfolding reply_master_revocable_def apply (rule iffI) apply clarify apply (drule_tac x = p in spec) apply (case_tac "p = src") apply (clarsimp simp:free_index_update_def is_master_reply_cap_def
         split:cap.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ms src = Some src_cap \<Longrightarrow> reply_master_revocable P (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) = reply_master_revocable P ms proof (prove)
goal (1 subgoal):
 1. ms src = Some src_cap \<Longrightarrow> (\<forall>p cap. (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) p = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> P p) = (\<forall>p cap. ms p = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> P p) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ms src = Some src_cap; \<forall>p cap. (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) p = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> P p\<rbrakk> \<Longrightarrow> \<forall>p cap. ms p = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> P p
 2. \<lbrakk>ms src = Some src_cap; \<forall>p cap. ms p = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> P p\<rbrakk> \<Longrightarrow> \<forall>p cap. (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) p = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> P p proof (prove)
goal (2 subgoals):
 1. \<And>p cap. \<lbrakk>ms src = Some src_cap; \<forall>p cap. (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) p = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> P p; ms p = Some cap; is_master_reply_cap cap\<rbrakk> \<Longrightarrow> P p
 2. \<lbrakk>ms src = Some src_cap; \<forall>p cap. ms p = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> P p\<rbrakk> \<Longrightarrow> \<forall>p cap. (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) p = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> P p proof (prove)
goal (2 subgoals):
 1. \<And>p cap. \<lbrakk>ms src = Some src_cap; ms p = Some cap; is_master_reply_cap cap; \<forall>cap. (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) p = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> P p\<rbrakk> \<Longrightarrow> P p
 2. \<lbrakk>ms src = Some src_cap; \<forall>p cap. ms p = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> P p\<rbrakk> \<Longrightarrow> \<forall>p cap. (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) p = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> P p proof (prove)
goal (3 subgoals):
 1. \<And>p cap. \<lbrakk>ms src = Some src_cap; ms p = Some cap; is_master_reply_cap cap; \<forall>cap. (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) p = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> P p; p = src\<rbrakk> \<Longrightarrow> P p
 2. \<And>p cap. \<lbrakk>ms src = Some src_cap; ms p = Some cap; is_master_reply_cap cap; \<forall>cap. (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) p = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> P p; p \<noteq> src\<rbrakk> \<Longrightarrow> P p
 3. \<lbrakk>ms src = Some src_cap; \<forall>p cap. ms p = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> P p\<rbrakk> \<Longrightarrow> \<forall>p cap. (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) p = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> P p proof (prove)
goal:
No subgoals!