theory PasUpdates

lemma state_irqs_to_policy_pasSubject_update:
  "state_irqs_to_policy_aux (aag\<lparr>pasSubject := x\<rparr>) caps =
   state_irqs_to_policy_aux aag caps" apply (rule equalityI; clarify) apply (erule state_irqs_to_policy_aux.cases, simp, blast intro: state_irqs_to_policy_aux.intros) apply (erule state_irqs_to_policy_aux.cases) apply simp apply (subst pasObjectAbs_pasSubject_update[symmetric]) apply (subst pasIRQAbs_pasSubject_update[symmetric]) apply (rule state_irqs_to_policy_aux.intros) apply assumption+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_irqs_to_policy_aux (aag\<lparr>pasSubject := x\<rparr>) caps = state_irqs_to_policy_aux aag caps proof (prove)
goal (2 subgoals):
 1. \<And>a aa b. (a, aa, b) \<in> state_irqs_to_policy_aux (aag\<lparr>pasSubject := x\<rparr>) caps \<Longrightarrow> (a, aa, b) \<in> state_irqs_to_policy_aux aag caps
 2. \<And>a aa b. (a, aa, b) \<in> state_irqs_to_policy_aux aag caps \<Longrightarrow> (a, aa, b) \<in> state_irqs_to_policy_aux (aag\<lparr>pasSubject := x\<rparr>) caps proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. (a, aa, b) \<in> state_irqs_to_policy_aux aag caps \<Longrightarrow> (a, aa, b) \<in> state_irqs_to_policy_aux (aag\<lparr>pasSubject := x\<rparr>) caps proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ptr cap irq. \<lbrakk>a = pasObjectAbs aag (fst ptr); aa = Control; b = pasIRQAbs aag irq; caps ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> state_irqs_to_policy_aux (aag\<lparr>pasSubject := x\<rparr>) caps proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ptr cap irq. \<lbrakk>a = pasObjectAbs aag (fst ptr); aa = Control; b = pasIRQAbs aag irq; caps ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ptr), Control, pasIRQAbs aag irq) \<in> state_irqs_to_policy_aux (aag\<lparr>pasSubject := x\<rparr>) caps proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ptr cap irq. \<lbrakk>a = pasObjectAbs aag (fst ptr); aa = Control; b = pasIRQAbs aag irq; caps ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> (pasObjectAbs (aag\<lparr>pasSubject := ?x45 a aa b ptr cap irq\<rparr>) (fst ptr), Control, pasIRQAbs aag irq) \<in> state_irqs_to_policy_aux (aag\<lparr>pasSubject := x\<rparr>) caps proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ptr cap irq. \<lbrakk>a = pasObjectAbs aag (fst ptr); aa = Control; b = pasIRQAbs aag irq; caps ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> (pasObjectAbs (aag\<lparr>pasSubject := ?xa46 a aa b ptr cap irq (?a46 a aa b ptr cap irq) (?aa46 a aa b ptr cap irq) (?b46 a aa b ptr cap irq) ptr (?cap46 a aa b ptr cap irq) irq\<rparr>) (fst ptr), Control, pasIRQAbs (aag\<lparr>pasSubject := ?x46 a aa b ptr cap irq\<rparr>) irq) \<in> state_irqs_to_policy_aux (aag\<lparr>pasSubject := x\<rparr>) caps proof (prove)
goal (2 subgoals):
 1. \<And>a aa b ptr cap irq. \<lbrakk>a = pasObjectAbs aag (fst ptr); aa = Control; b = pasIRQAbs aag irq; caps ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> caps ptr = Some (?cap47 a aa b ptr cap irq)
 2. \<And>a aa b ptr cap irq. \<lbrakk>a = pasObjectAbs aag (fst ptr); aa = Control; b = pasIRQAbs aag irq; caps ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> irq \<in> cap_irqs_controlled (?cap47 a aa b ptr cap irq) proof (prove)
goal:
No subgoals!