theory EmptyFail_H

theorem call_kernel_serial:
  "\<lbrakk> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and
              (\<lambda>s. scheduler_action s = resume_cur_thread) and
              (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s;
       \<exists>s'. (s, s') \<in> state_relation \<and>
            (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and
              (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and
              (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s' \<rbrakk>
    \<Longrightarrow> fst (call_kernel event s) \<noteq> {}" apply (cut_tac m = "call_kernel event" in corres_underlying_serial) apply (rule kernel_corres) apply (rule callKernel_empty_fail) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s; \<exists>s'. (s, s') \<in> state_relation \<and> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s'\<rbrakk> \<Longrightarrow> fst (call_kernel event s) \<noteq> {} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s; \<exists>s'. (s, s') \<in> state_relation \<and> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s'\<rbrakk> \<Longrightarrow> corres_underlying ?S False True ?rrel ?G ?G' (call_kernel event) ?m'
 2. \<lbrakk>(einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s; \<exists>s'. (s, s') \<in> state_relation \<and> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s'\<rbrakk> \<Longrightarrow> empty_fail ?m'
 3. \<lbrakk>(einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s; \<exists>s'. (s, s') \<in> state_relation \<and> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s'; \<forall>s. (\<exists>s'. (s, s') \<in> ?S \<and> ?G s \<and> ?G' s') \<longrightarrow> fst (call_kernel event s) \<noteq> {}\<rbrakk> \<Longrightarrow> fst (call_kernel event s) \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s; \<exists>s'. (s, s') \<in> state_relation \<and> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s'\<rbrakk> \<Longrightarrow> empty_fail (callKernel event)
 2. \<lbrakk>(einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s; \<exists>s'. (s, s') \<in> state_relation \<and> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s'; \<forall>s. (\<exists>s'. (s, s') \<in> state_relation \<and> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s \<and> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s') \<longrightarrow> fst (call_kernel event s) \<noteq> {}\<rbrakk> \<Longrightarrow> fst (call_kernel event s) \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s; \<exists>s'. (s, s') \<in> state_relation \<and> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s'; \<forall>s. (\<exists>s'. (s, s') \<in> state_relation \<and> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s \<and> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s') \<longrightarrow> fst (call_kernel event s) \<noteq> {}\<rbrakk> \<Longrightarrow> fst (call_kernel event s) \<noteq> {} proof (prove)
goal:
No subgoals!