theory ADT_IF

lemma kernel_entry_if_irq_measure:
  "\<lbrakk> event \<noteq> Interrupt; invs i_s; domain_sep_inv False (st :: det_state) i_s;
     irq_is_recurring irq i_s; ((Inr (), a), b) \<in> fst (kernel_entry_if event uc i_s) \<rbrakk>
     \<Longrightarrow> irq_measure_if b \<le> irq_measure_if i_s" apply (fold irq_measure_if_inv_def) apply (rule mp) apply (erule_tac P="(=) i_s" and Q="\<lambda>rv s. (isRight (fst rv)) \<longrightarrow> Q s" for Q in use_valid) apply (simp_all add: isRight_def) apply (simp add: kernel_entry_if_def) apply (rule hoare_pre, wp) apply (rule validE_cases_valid, simp) apply (wp irq_measure_if_inv handle_event_irq_state_inv[THEN validE_validE_R'])+ apply (wpsimp wp: irq_measure_if_inv' irq_state_inv_triv
                      thread_set_invs_trivial irq_is_recurring_triv
                simp: ran_tcb_cap_cases arch_tcb_update_aux2 irq_state_inv_refl)+ apply (simp add: irq_measure_if_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; ((Inr (), a), b) \<in> fst (kernel_entry_if event uc i_s)\<rbrakk> \<Longrightarrow> irq_measure_if b \<le> irq_measure_if 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; ((Inr (), a), b) \<in> fst (kernel_entry_if event uc i_s)\<rbrakk> \<Longrightarrow> irq_measure_if_inv i_s b proof (prove)
goal (2 subgoals):
 1. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; ((Inr (), a), b) \<in> fst (kernel_entry_if event uc i_s)\<rbrakk> \<Longrightarrow> ?P \<longrightarrow> irq_measure_if_inv i_s b
 2. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; ((Inr (), a), b) \<in> fst (kernel_entry_if event uc i_s)\<rbrakk> \<Longrightarrow> ?P proof (prove)
goal (3 subgoals):
 1. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s\<rbrakk> \<Longrightarrow> \<lbrace>(=) i_s\<rbrace> kernel_entry_if event uc \<lbrace>\<lambda>rv s. isRight (fst rv) \<longrightarrow> irq_measure_if_inv i_s s\<rbrace>
 2. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s\<rbrakk> \<Longrightarrow> i_s = i_s
 3. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; ((Inr (), a), b) \<in> fst (kernel_entry_if event uc i_s)\<rbrakk> \<Longrightarrow> isRight (fst (Inr (), a)) 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\<rbrakk> \<Longrightarrow> \<lbrace>(=) i_s\<rbrace> kernel_entry_if event uc \<lbrace>\<lambda>rv s. fst rv = Inr () \<longrightarrow> irq_measure_if_inv i_s s\<rbrace> 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\<rbrakk> \<Longrightarrow> \<lbrace>(=) i_s\<rbrace> do t <- gets cur_thread;
y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) t;
r <- handle_event event;
return (r, uc)
od \<lbrace>\<lambda>rv s. fst rv = Inr () \<longrightarrow> irq_measure_if_inv i_s s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s\<rbrakk> \<Longrightarrow> \<lbrace>?B13 x y\<rbrace> handle_event event \<lbrace>\<lambda>r a. fst (r, uc) = Inr () \<longrightarrow> irq_measure_if_inv i_s a\<rbrace>
 2. \<And>x. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s\<rbrakk> \<Longrightarrow> \<lbrace>?B12 x\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) x \<lbrace>?B13 x\<rbrace>
 3. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s\<rbrakk> \<Longrightarrow> \<lbrace>?Q8\<rbrace> gets cur_thread \<lbrace>?B12\<rbrace>
 4. \<And>s. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; i_s = s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s\<rbrakk> \<Longrightarrow> \<lbrace>?B13 x ()\<rbrace> handle_event event \<lbrace>\<lambda>rv. irq_measure_if_inv i_s\<rbrace>, \<lbrace>\<lambda>rv s. True\<rbrace>
 2. \<And>x. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s\<rbrakk> \<Longrightarrow> \<lbrace>?B12 x\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) x \<lbrace>?B13 x\<rbrace>
 3. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s\<rbrakk> \<Longrightarrow> \<lbrace>?Q8\<rbrace> gets cur_thread \<lbrace>?B12\<rbrace>
 4. \<And>s. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; i_s = s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s\<rbrakk> \<Longrightarrow> \<lbrace>?P'35 x\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set uc (tcb_arch tcb)\<rparr>) x \<lbrace>\<lambda>rv s. irq_measure_if_inv i_s s \<and> (irq_state_inv s s \<longrightarrow> (irq_state_inv s and invs and domain_sep_inv False (?sta32 x rv s) and K (irq_is_recurring (?irq31 x rv s) s)) s)\<rbrace>
 2. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s\<rbrakk> \<Longrightarrow> \<lbrace>?Q8\<rbrace> gets cur_thread \<lbrace>\<lambda>x s. True \<and> ?P'35 x s\<rbrace>
 3. \<And>s. \<lbrakk>event \<noteq> Interrupt; invs i_s; domain_sep_inv False st i_s; irq_is_recurring irq i_s; i_s = s\<rbrakk> \<Longrightarrow> ?Q8 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\<rbrakk> \<Longrightarrow> irq_measure_if_inv i_s i_s \<and> domain_sep_inv False (?sta50 (cur_thread i_s) ()) i_s \<and> irq_is_recurring (?irq52 (cur_thread i_s) ()) i_s proof (prove)
goal:
No subgoals!