theory CSpace_AI

lemma free_index_update_irq_revocable[simp]:
  "ms src = Some src_cap \<Longrightarrow>
   irq_revocable P (ms(src \<mapsto> src_cap\<lparr>free_index:=a\<rparr>)) = irq_revocable P ms" unfolding irq_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)+ apply (simp add: free_index_update_def split:cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ms src = Some src_cap \<Longrightarrow> irq_revocable P (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) = irq_revocable P ms proof (prove)
goal (1 subgoal):
 1. ms src = Some src_cap \<Longrightarrow> (\<forall>p. (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) p = Some IRQControlCap \<longrightarrow> P p) = (\<forall>p. ms p = Some IRQControlCap \<longrightarrow> P p) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ms src = Some src_cap; \<forall>p. (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) p = Some IRQControlCap \<longrightarrow> P p\<rbrakk> \<Longrightarrow> \<forall>p. ms p = Some IRQControlCap \<longrightarrow> P p
 2. \<lbrakk>ms src = Some src_cap; \<forall>p. ms p = Some IRQControlCap \<longrightarrow> P p\<rbrakk> \<Longrightarrow> \<forall>p. (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) p = Some IRQControlCap \<longrightarrow> P p proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>ms src = Some src_cap; \<forall>p. (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) p = Some IRQControlCap \<longrightarrow> P p; ms p = Some IRQControlCap\<rbrakk> \<Longrightarrow> P p
 2. \<lbrakk>ms src = Some src_cap; \<forall>p. ms p = Some IRQControlCap \<longrightarrow> P p\<rbrakk> \<Longrightarrow> \<forall>p. (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) p = Some IRQControlCap \<longrightarrow> P p proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>ms src = Some src_cap; ms p = Some IRQControlCap; (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) p = Some IRQControlCap \<longrightarrow> P p\<rbrakk> \<Longrightarrow> P p
 2. \<lbrakk>ms src = Some src_cap; \<forall>p. ms p = Some IRQControlCap \<longrightarrow> P p\<rbrakk> \<Longrightarrow> \<forall>p. (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) p = Some IRQControlCap \<longrightarrow> P p proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrakk>ms src = Some src_cap; ms p = Some IRQControlCap; (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) p = Some IRQControlCap \<longrightarrow> P p; p = src\<rbrakk> \<Longrightarrow> P p
 2. \<And>p. \<lbrakk>ms src = Some src_cap; ms p = Some IRQControlCap; (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) p = Some IRQControlCap \<longrightarrow> P p; p \<noteq> src\<rbrakk> \<Longrightarrow> P p
 3. \<lbrakk>ms src = Some src_cap; \<forall>p. ms p = Some IRQControlCap \<longrightarrow> P p\<rbrakk> \<Longrightarrow> \<forall>p. (ms(src \<mapsto> free_index_update (\<lambda>_. a) src_cap)) p = Some IRQControlCap \<longrightarrow> P p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ms src = Some src_cap; \<forall>p. ms p = Some IRQControlCap \<longrightarrow> P p; (case src_cap of UntypedCap dev ref sz f \<Rightarrow> UntypedCap dev ref sz a | _ \<Rightarrow> src_cap) = IRQControlCap\<rbrakk> \<Longrightarrow> P src proof (prove)
goal:
No subgoals!