theory ADT_IF

lemma kernel_entry_if_domain_time_sched_action:
  "\<lbrace>\<lambda>s. domain_time s > 0\<rbrace>
   kernel_entry_if e tc
   \<lbrace>\<lambda>_ s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>" apply (case_tac "e = Interrupt") apply (simp add: kernel_entry_if_def) apply (wp handle_interrupt_valid_domain_time| wpc | simp)+ apply (rule_tac Q="\<lambda>r s. domain_time s > 0" in hoare_strengthen_post) apply (wp | simp)+ apply (wp hoare_false_imp kernel_entry_if_domain_fields | fastforce)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 0 < domain_time s\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_ s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace> proof (prove)
goal (2 subgoals):
 1. e = Interrupt \<Longrightarrow> \<lbrace>\<lambda>s. 0 < domain_time s\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_ s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>
 2. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>\<lambda>s. 0 < domain_time s\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_ s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace> proof (prove)
goal (2 subgoals):
 1. e = Interrupt \<Longrightarrow> \<lbrace>\<lambda>s. 0 < domain_time s\<rbrace> do t <- gets cur_thread;
y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t;
r <- liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt);
return (r, tc)
od \<lbrace>\<lambda>_ s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>
 2. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>\<lambda>s. 0 < domain_time s\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_ s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>t. e = Interrupt \<Longrightarrow> \<lbrace>?B4 t ()\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>x s. (x = None \<longrightarrow> domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread) \<and> ((\<exists>xa. x = Some xa) \<longrightarrow> 0 < domain_time s)\<rbrace>
 2. \<And>t. e = Interrupt \<Longrightarrow> \<lbrace>?B3 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>?B4 t\<rbrace>
 3. e = Interrupt \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets cur_thread \<lbrace>?B3\<rbrace>
 4. \<And>s. \<lbrakk>e = Interrupt; 0 < domain_time s\<rbrakk> \<Longrightarrow> ?Q2 s
 5. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>\<lambda>s. 0 < domain_time s\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_ s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>t. e = Interrupt \<Longrightarrow> \<lbrace>?B4 t ()\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>r s. 0 < domain_time s\<rbrace>
 2. \<And>t rv s. \<lbrakk>e = Interrupt; 0 < domain_time s\<rbrakk> \<Longrightarrow> (rv = None \<longrightarrow> domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread) \<and> ((\<exists>x. rv = Some x) \<longrightarrow> 0 < domain_time s)
 3. \<And>t. e = Interrupt \<Longrightarrow> \<lbrace>?B3 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>?B4 t\<rbrace>
 4. e = Interrupt \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets cur_thread \<lbrace>?B3\<rbrace>
 5. \<And>s. \<lbrakk>e = Interrupt; 0 < domain_time s\<rbrakk> \<Longrightarrow> ?Q2 s
 6. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>\<lambda>s. 0 < domain_time s\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_ s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv s. \<lbrakk>e = Interrupt; 0 < domain_time s\<rbrakk> \<Longrightarrow> rv = None \<longrightarrow> domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread
 2. \<And>t. e = Interrupt \<Longrightarrow> \<lbrace>?B3 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>\<lambda>a b. 0 < domain_time b\<rbrace>
 3. e = Interrupt \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets cur_thread \<lbrace>?B3\<rbrace>
 4. \<And>s. \<lbrakk>e = Interrupt; 0 < domain_time s\<rbrakk> \<Longrightarrow> ?Q2 s
 5. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>\<lambda>s. 0 < domain_time s\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_ s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace> proof (prove)
goal:
No subgoals!