theory ADT_IF

lemma kernel_entry_if_next_irq_state_of_state_next:
  "\<lbrakk> event \<noteq> Interrupt; invs i_s; domain_sep_inv False (st :: det_state) i_s;
     irq_is_recurring irq i_s; ((Inl r, a), b) \<in> fst (kernel_entry_if event uc i_s) \<rbrakk>
     \<Longrightarrow> irq_state_of_state b = next_irq_state_of_state i_s" apply (simp add: kernel_entry_if_def in_bind in_return | elim conjE exE)+ apply (erule use_validE_E) apply (rule validE_validE_E) apply (rule hoare_post_impErr) apply (rule handle_event_irq_state_inv[where sta=st and irq=irq and st=i_s]) apply simp+ apply (simp add: irq_state_next_def) apply (simp add: arch_tcb_update_aux2) apply (erule_tac f="thread_set (tcb_arch_update (arch_tcb_context_set uc)) t" in use_valid) apply (wpsimp wp: irq_measure_if_inv' irq_state_inv_triv
                     thread_set_invs_trivial irq_is_recurring_triv
               simp: ran_tcb_cap_cases)+ apply (erule use_valid) apply (wp | simp )+ apply (simp add: irq_state_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; ((Inl r, a), b) \<in> fst (kernel_entry_if event uc i_s)\<rbrakk> \<Longrightarrow> irq_state_of_state b = next_irq_state_of_state i_s proof (prove)
goal (1 subgoal):
 1. \<And>s'' t s''a. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; (t, s'') \<in> fst (gets cur_thread i_s); ((), s''a) \<in> fst (thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) t s''); (Inl (), b) \<in> fst (handle_event event s''a); a = uc\<rbrakk> \<Longrightarrow> irq_state_of_state b = next_irq_state_of_state i_s proof (prove)
goal (2 subgoals):
 1. \<And>s'' t s''a. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; (t, s'') \<in> fst (gets cur_thread i_s); ((), s''a) \<in> fst (thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) t s''); a = uc\<rbrakk> \<Longrightarrow> \<lbrace>?P6 s'' t s''a\<rbrace> handle_event event -, \<lbrace>\<lambda>a b. irq_state_of_state b = next_irq_state_of_state i_s\<rbrace>
 2. \<And>s'' t s''a. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; (t, s'') \<in> fst (gets cur_thread i_s); ((), s''a) \<in> fst (thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) t s''); a = uc\<rbrakk> \<Longrightarrow> ?P6 s'' t s''a s''a proof (prove)
goal (2 subgoals):
 1. \<And>s'' t s''a. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; (t, s'') \<in> fst (gets cur_thread i_s); ((), s''a) \<in> fst (thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) t s''); a = uc\<rbrakk> \<Longrightarrow> \<lbrace>?P6 s'' t s''a\<rbrace> handle_event event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a b. irq_state_of_state b = next_irq_state_of_state i_s\<rbrace>
 2. \<And>s'' t s''a. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; (t, s'') \<in> fst (gets cur_thread i_s); ((), s''a) \<in> fst (thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) t s''); a = uc\<rbrakk> \<Longrightarrow> ?P6 s'' t s''a s''a proof (prove)
goal (4 subgoals):
 1. \<And>s'' t s''a. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; (t, s'') \<in> fst (gets cur_thread i_s); ((), s''a) \<in> fst (thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) t s''); a = uc\<rbrakk> \<Longrightarrow> \<lbrace>?P6 s'' t s''a\<rbrace> handle_event event \<lbrace>?Q11 s'' t s''a\<rbrace>, \<lbrace>?E11 s'' t s''a\<rbrace>
 2. \<And>s'' t s''a rv s. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; (t, s'') \<in> fst (gets cur_thread i_s); ((), s''a) \<in> fst (thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) t s''); a = uc; ?Q11 s'' t s''a rv s\<rbrakk> \<Longrightarrow> True
 3. \<And>s'' t s''a e s. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; (t, s'') \<in> fst (gets cur_thread i_s); ((), s''a) \<in> fst (thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) t s''); a = uc; ?E11 s'' t s''a e s\<rbrakk> \<Longrightarrow> irq_state_of_state s = next_irq_state_of_state i_s
 4. \<And>s'' t s''a. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; (t, s'') \<in> fst (gets cur_thread i_s); ((), s''a) \<in> fst (thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) t s''); a = uc\<rbrakk> \<Longrightarrow> ?P6 s'' t s''a s''a proof (prove)
goal (4 subgoals):
 1. \<And>s'' t s''a. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; (t, s'') \<in> fst (gets cur_thread i_s); ((), s''a) \<in> fst (thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) t s''); a = uc\<rbrakk> \<Longrightarrow> event \<noteq> Interrupt
 2. \<And>s'' t s''a rv s. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; (t, s'') \<in> fst (gets cur_thread i_s); ((), s''a) \<in> fst (thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) t s''); a = uc; irq_state_inv i_s s\<rbrakk> \<Longrightarrow> True
 3. \<And>s'' t s''a e s. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; (t, s'') \<in> fst (gets cur_thread i_s); ((), s''a) \<in> fst (thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) t s''); a = uc; irq_state_next i_s s\<rbrakk> \<Longrightarrow> irq_state_of_state s = next_irq_state_of_state i_s
 4. \<And>s'' t s''a. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; (t, s'') \<in> fst (gets cur_thread i_s); ((), s''a) \<in> fst (thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) t s''); a = uc\<rbrakk> \<Longrightarrow> (irq_state_inv i_s and invs and domain_sep_inv False st and K (irq_is_recurring irq i_s)) s''a proof (prove)
goal (2 subgoals):
 1. \<And>s'' t s''a s. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; (t, s'') \<in> fst (gets cur_thread i_s); ((), s''a) \<in> fst (thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) t s''); a = uc; irq_state_next i_s s\<rbrakk> \<Longrightarrow> irq_state_of_state s = next_irq_state_of_state i_s
 2. \<And>s'' t s''a. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; (t, s'') \<in> fst (gets cur_thread i_s); ((), s''a) \<in> fst (thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) t s''); a = uc\<rbrakk> \<Longrightarrow> (irq_state_inv i_s and invs and domain_sep_inv False st and K (irq_is_recurring irq i_s)) s''a proof (prove)
goal (1 subgoal):
 1. \<And>s'' t s''a. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; (t, s'') \<in> fst (gets cur_thread i_s); ((), s''a) \<in> fst (thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) t s''); a = uc\<rbrakk> \<Longrightarrow> (irq_state_inv i_s and invs and domain_sep_inv False st and K (irq_is_recurring irq i_s)) s''a proof (prove)
goal (1 subgoal):
 1. \<And>s'' t s''a. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; (t, s'') \<in> fst (gets cur_thread i_s); ((), s''a) \<in> fst (thread_set (tcb_arch_update (arch_tcb_context_set uc)) t s''); a = uc\<rbrakk> \<Longrightarrow> irq_state_inv i_s s''a \<and> invs s''a \<and> domain_sep_inv False st s''a proof (prove)
goal (2 subgoals):
 1. \<And>s'' t s''a. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; (t, s'') \<in> fst (gets cur_thread i_s); a = uc\<rbrakk> \<Longrightarrow> \<lbrace>?P17 s'' t s''a\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set uc)) t \<lbrace>\<lambda>a b. irq_state_inv i_s b \<and> invs b \<and> domain_sep_inv False st b\<rbrace>
 2. \<And>s'' t s''a. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; (t, s'') \<in> fst (gets cur_thread i_s); a = uc\<rbrakk> \<Longrightarrow> ?P17 s'' t s''a s'' proof (prove)
goal (1 subgoal):
 1. \<And>s'' t. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; (t, s'') \<in> fst (gets cur_thread i_s); a = uc\<rbrakk> \<Longrightarrow> irq_state_inv i_s s'' \<and> invs s'' \<and> domain_sep_inv False st s'' proof (prove)
goal (2 subgoals):
 1. \<And>s'' t. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; a = uc\<rbrakk> \<Longrightarrow> \<lbrace>?P32 s'' t\<rbrace> gets cur_thread \<lbrace>\<lambda>a b. irq_state_inv i_s b \<and> invs b \<and> domain_sep_inv False st b\<rbrace>
 2. \<And>s'' t. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; a = uc\<rbrakk> \<Longrightarrow> ?P32 s'' t i_s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; a = uc\<rbrakk> \<Longrightarrow> irq_state_inv i_s i_s proof (prove)
goal:
No subgoals!