theory Refine

lemma kernel_entry_invs:
  "\<lbrace>einvs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)
    and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle)
    and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace>
  kernel_entry e us
  \<lbrace>\<lambda>rv. einvs and (\<lambda>s. ct_running s \<or> ct_idle s)
    and (\<lambda>s. 0 < domain_time s) and valid_domain_list
    and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace>" apply (rule_tac Q="\<lambda>rv. invs and (\<lambda>s. ct_running s \<or> ct_idle s) and valid_sched and
                           (\<lambda>s. 0 < domain_time s) and valid_domain_list and
                           valid_list and (\<lambda>s. scheduler_action s = resume_cur_thread)"
            in hoare_post_imp) apply clarsimp apply (simp add: kernel_entry_def) apply (wp akernel_invs_det_ext call_kernel_valid_sched thread_set_invs_trivial
            thread_set_ct_running thread_set_not_state_valid_sched
            hoare_vcg_disj_lift ct_in_state_thread_state_lift thread_set_no_change_tcb_state
            call_kernel_domain_time_inv_det_ext call_kernel_domain_list_inv_det_ext
            hoare_weak_lift_imp
      | clarsimp simp add: tcb_cap_cases_def active_from_running)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>einvs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> kernel_entry e us \<lbrace>\<lambda>rv. einvs and (\<lambda>s. ct_running s \<or> ct_idle s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. (invs and (\<lambda>s. ct_running s \<or> ct_idle s) and valid_sched and (\<lambda>s. 0 < domain_time s) and valid_domain_list and valid_list and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. ct_running s \<or> ct_idle s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. scheduler_action s = resume_cur_thread)) s
 2. \<lbrace>einvs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> kernel_entry e us \<lbrace>\<lambda>rv. invs and (\<lambda>s. ct_running s \<or> ct_idle s) and valid_sched and (\<lambda>s. 0 < domain_time s) and valid_domain_list and valid_list and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>einvs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> kernel_entry e us \<lbrace>\<lambda>rv. invs and (\<lambda>s. ct_running s \<or> ct_idle s) and valid_sched and (\<lambda>s. 0 < domain_time s) and valid_domain_list and valid_list and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>einvs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> do t <- gets cur_thread;
y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set us (tcb_arch tcb)\<rparr>) t;
y <- call_kernel e;
gets cur_thread >>= thread_get (arch_tcb_context_get \<circ> tcb_arch)
od \<lbrace>\<lambda>rv. invs and (\<lambda>s. ct_running s \<or> ct_idle s) and valid_sched and (\<lambda>s. 0 < domain_time s) and valid_domain_list and valid_list and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> proof (prove)
goal:
No subgoals!