theory Dpolicy

lemma state_irqs_transform:
  "\<lbrakk> einvs s; (x, a, y) \<in> state_irqs_to_policy aag s \<rbrakk> \<Longrightarrow>
   (x, a, y) \<in> cdl_state_irqs_to_policy aag (transform s)" apply (erule state_irqs_to_policy_aux.induct) apply (simp add: fst_transform_cslot_ptr) apply (rule_tac cap="transform_cap cap" in csita_controlled) apply (rule caps_of_state_transform_opt_cap) apply simp apply fastforce apply (clarsimp simp:idle_thread_no_irqs) apply (simp add: cap_irqs_controlled_transform) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; (x, a, y) \<in> state_irqs_to_policy aag s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_irqs_to_policy aag (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>ptr cap irq. \<lbrakk>einvs s; caps_of_state s ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ptr), Control, pasIRQAbs aag irq) \<in> cdl_state_irqs_to_policy aag (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>ptr cap irq. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst (transform_cslot_ptr ptr)), Control, pasIRQAbs aag irq) \<in> cdl_state_irqs_to_policy aag (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>ptr cap irq. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr ptr) (transform s) = Some (transform_cap cap)
 2. \<And>ptr cap irq. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> irq \<in> cdl_cap_irqs_controlled (transform_cap cap) proof (prove)
goal (4 subgoals):
 1. \<And>ptr cap irq. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> caps_of_state s ptr = Some cap
 2. \<And>ptr cap irq. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> valid_etcbs s
 3. \<And>ptr cap irq. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s
 4. \<And>ptr cap irq. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> irq \<in> cdl_cap_irqs_controlled (transform_cap cap) proof (prove)
goal (3 subgoals):
 1. \<And>ptr cap irq. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> valid_etcbs s
 2. \<And>ptr cap irq. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s
 3. \<And>ptr cap irq. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> irq \<in> cdl_cap_irqs_controlled (transform_cap cap) proof (prove)
goal (2 subgoals):
 1. \<And>ptr cap irq. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s
 2. \<And>ptr cap irq. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> irq \<in> cdl_cap_irqs_controlled (transform_cap cap) proof (prove)
goal (1 subgoal):
 1. \<And>ptr cap irq. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; caps_of_state s ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> irq \<in> cdl_cap_irqs_controlled (transform_cap cap) proof (prove)
goal:
No subgoals!