theory CSpace_AI

lemma free_index_update_ut_revocable[simp]:
  "ms src = Some src_cap \<Longrightarrow>
   ut_revocable P (ms (src \<mapsto> (src_cap\<lparr>free_index:=a\<rparr>))) = ut_revocable P ms" unfolding ut_revocable_def apply (rule iffI) apply clarify apply (drule_tac x = p in spec) apply (case_tac "p = src") apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ms src = Some src_cap \<Longrightarrow> ut_revocable P (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) = ut_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_untyped_cap cap \<longrightarrow> P p) = (\<forall>p cap. ms p = Some cap \<longrightarrow> is_untyped_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_untyped_cap cap \<longrightarrow> P p\<rbrakk> \<Longrightarrow> \<forall>p cap. ms p = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> P p
 2. \<lbrakk>ms src = Some src_cap; \<forall>p cap. ms p = Some cap \<longrightarrow> is_untyped_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_untyped_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_untyped_cap cap \<longrightarrow> P p; ms p = Some cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> P p
 2. \<lbrakk>ms src = Some src_cap; \<forall>p cap. ms p = Some cap \<longrightarrow> is_untyped_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_untyped_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_untyped_cap cap; \<forall>cap. (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) p = Some cap \<longrightarrow> is_untyped_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_untyped_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_untyped_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_untyped_cap cap; \<forall>cap. (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) p = Some cap \<longrightarrow> is_untyped_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_untyped_cap cap; \<forall>cap. (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) p = Some cap \<longrightarrow> is_untyped_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_untyped_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_untyped_cap cap \<longrightarrow> P p proof (prove)
goal:
No subgoals!