theory Ipc_DR

lemma not_idle_thread_resolve_address_bits:
  "\<lbrace>valid_global_refs and valid_objs and valid_idle and valid_irq_node and ko_at (TCB obj) thread\<rbrace>
    CSpace_A.resolve_address_bits (tcb_ctable obj, blist)
            \<lbrace>\<lambda>rv. not_idle_thread (fst (fst rv))\<rbrace>, \<lbrace>\<lambda>_. \<top>\<rbrace>" apply (rule validE_R_validE) apply (rule_tac hoare_vcg_precond_impE_R) apply (rule validE_validE_R) apply (rule_tac Q="\<lambda>r. valid_global_refs and valid_objs and valid_idle and valid_irq_node and ex_cte_cap_to (fst r)"
    in hoare_post_impErr[where E="\<lambda>x y. True"]) apply (wp rab_cte_cap_to) apply clarsimp apply (drule ex_cte_cap_to_not_idle, auto simp: not_idle_thread_def)[1] apply (rule TrueI) apply (clarsimp simp:ex_cte_cap_to_def) apply (rule_tac x = thread in exI,rule_tac x = "tcb_cnode_index 0" in exI) apply (clarsimp simp:cte_wp_at_cases obj_at_def is_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs and valid_objs and valid_idle and valid_irq_node and ko_at (TCB obj) thread\<rbrace> CSpace_A.resolve_address_bits (tcb_ctable obj, blist) \<lbrace>\<lambda>rv. not_idle_thread (fst (fst rv))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs and valid_objs and valid_idle and valid_irq_node and ko_at (TCB obj) thread\<rbrace> CSpace_A.resolve_address_bits (tcb_ctable obj, blist) \<lbrace>\<lambda>rv. not_idle_thread (fst (fst rv))\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'2\<rbrace> CSpace_A.resolve_address_bits (tcb_ctable obj, blist) \<lbrace>\<lambda>rv. not_idle_thread (fst (fst rv))\<rbrace>, -
 2. \<And>s. (valid_global_refs and valid_objs and valid_idle and valid_irq_node and ko_at (TCB obj) thread) s \<Longrightarrow> ?P'2 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'2\<rbrace> CSpace_A.resolve_address_bits (tcb_ctable obj, blist) \<lbrace>\<lambda>rv. not_idle_thread (fst (fst rv))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s. (valid_global_refs and valid_objs and valid_idle and valid_irq_node and ko_at (TCB obj) thread) s \<Longrightarrow> ?P'2 s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'2\<rbrace> CSpace_A.resolve_address_bits (tcb_ctable obj, blist) \<lbrace>\<lambda>r. valid_global_refs and valid_objs and valid_idle and valid_irq_node and ex_cte_cap_wp_to (\<lambda>_. True) (fst r)\<rbrace>, \<lbrace>\<lambda>x y. True\<rbrace>
 2. \<And>rv s. (valid_global_refs and valid_objs and valid_idle and valid_irq_node and ex_cte_cap_wp_to (\<lambda>_. True) (fst rv)) s \<Longrightarrow> not_idle_thread (fst (fst rv)) s
 3. \<And>e s. True \<Longrightarrow> True
 4. \<And>s. (valid_global_refs and valid_objs and valid_idle and valid_irq_node and ko_at (TCB obj) thread) s \<Longrightarrow> ?P'2 s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. (valid_global_refs and valid_objs and valid_idle and valid_irq_node and ex_cte_cap_wp_to (\<lambda>_. True) (fst rv)) s \<Longrightarrow> not_idle_thread (fst (fst rv)) s
 2. \<And>e s. True \<Longrightarrow> True
 3. \<And>s. (valid_global_refs and valid_objs and valid_idle and valid_irq_node and ko_at (TCB obj) thread) s \<Longrightarrow> True \<and> (valid_global_refs and valid_objs and valid_idle and valid_irq_node) s \<and> (Structures_A.is_cnode_cap (fst (tcb_ctable obj, blist)) \<longrightarrow> (\<forall>r\<in>cte_refs (fst (tcb_ctable obj, blist)) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>cap. True) r s)) \<and> (\<forall>cap. Structures_A.is_cnode_cap cap \<longrightarrow> True) proof (prove)
goal (3 subgoals):
 1. \<And>a b s. \<lbrakk>valid_global_refs s; valid_objs s; valid_idle s; valid_irq_node s; ex_cte_cap_wp_to (\<lambda>_. True) (a, b) s\<rbrakk> \<Longrightarrow> not_idle_thread a s
 2. \<And>e s. True \<Longrightarrow> True
 3. \<And>s. (valid_global_refs and valid_objs and valid_idle and valid_irq_node and ko_at (TCB obj) thread) s \<Longrightarrow> True \<and> (valid_global_refs and valid_objs and valid_idle and valid_irq_node) s \<and> (Structures_A.is_cnode_cap (fst (tcb_ctable obj, blist)) \<longrightarrow> (\<forall>r\<in>cte_refs (fst (tcb_ctable obj, blist)) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>cap. True) r s)) \<and> (\<forall>cap. Structures_A.is_cnode_cap cap \<longrightarrow> True) proof (prove)
goal (2 subgoals):
 1. \<And>e s. True \<Longrightarrow> True
 2. \<And>s. (valid_global_refs and valid_objs and valid_idle and valid_irq_node and ko_at (TCB obj) thread) s \<Longrightarrow> True \<and> (valid_global_refs and valid_objs and valid_idle and valid_irq_node) s \<and> (Structures_A.is_cnode_cap (fst (tcb_ctable obj, blist)) \<longrightarrow> (\<forall>r\<in>cte_refs (fst (tcb_ctable obj, blist)) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>cap. True) r s)) \<and> (\<forall>cap. Structures_A.is_cnode_cap cap \<longrightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_global_refs and valid_objs and valid_idle and valid_irq_node and ko_at (TCB obj) thread) s \<Longrightarrow> True \<and> (valid_global_refs and valid_objs and valid_idle and valid_irq_node) s \<and> (Structures_A.is_cnode_cap (fst (tcb_ctable obj, blist)) \<longrightarrow> (\<forall>r\<in>cte_refs (fst (tcb_ctable obj, blist)) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>cap. True) r s)) \<and> (\<forall>cap. Structures_A.is_cnode_cap cap \<longrightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>valid_global_refs s; valid_objs s; valid_idle s; valid_irq_node s; ko_at (TCB obj) thread s; Structures_A.is_cnode_cap (tcb_ctable obj); (a, b) \<in> cte_refs (tcb_ctable obj) (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> \<exists>aa ba. cte_wp_at (\<lambda>c. (a, b) \<in> cte_refs c (interrupt_irq_node s)) (aa, ba) s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>valid_global_refs s; valid_objs s; valid_idle s; valid_irq_node s; ko_at (TCB obj) thread s; Structures_A.is_cnode_cap (tcb_ctable obj); (a, b) \<in> cte_refs (tcb_ctable obj) (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. (a, b) \<in> cte_refs c (interrupt_irq_node s)) (thread, tcb_cnode_index 0) s proof (prove)
goal:
No subgoals!