theory ADT_IF_Refine_C

lemma handle_preemption_corres_C:
  "corres_underlying rf_sr False False (=)
     (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) \<top>
     (handlePreemption_if tc) (handlePreemption_C_if tc)" apply (simp add: handlePreemption_if_def2 handlePreemption_C_if_def) apply (rule corres_stateAssert_no_fail) using corres_nofail[OF handle_preemption_if_corres[of tc], simplified] apply (simp add: handlePreemption_if_def2) apply (erule no_fail_pre) apply (clarsimp simp: ex_abs_underlying_def ex_abs_def) apply (rule exI, rule conjI, assumption) apply (clarsimp simp: domain_time_rel_eq domain_list_rel_eq) apply (rule corres_guard_imp) apply (rule_tac r'="dc" in corres_split) apply (rule ccorres_corres_u) apply (rule ccorres_guard_imp) apply (rule ccorres_rel_imp) apply (rule handleInterrupt_if_ccorres) apply simp prefer 3 apply (rule handleEvent_Interrupt_no_fail) apply clarsimp apply simp apply simp apply (rule hoare_post_taut[where P=\<top>])+ apply (fastforce simp: ex_abs_def schedaction_related)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr False False (=) (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) (\<lambda>_. True) (handlePreemption_if tc) (handlePreemption_C_if tc) proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr False False (=) (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) (\<lambda>_. True) (do r <- handleEvent Interrupt;
y <- stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od) (do y <- exec_C \<Gamma> handleInterruptEntry_C_body_if;
return tc
od) proof (prove)
goal (2 subgoals):
 1. no_fail (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) (do r <- handleEvent Interrupt;
y <- stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od)
 2. corres_underlying rf_sr False False (=) (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) (\<lambda>_. True) (do r <- handleEvent Interrupt;
return tc
od) (do y <- exec_C \<Gamma> handleInterruptEntry_C_body_if;
return tc
od) proof (prove)
using this:
no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> valid_domain_list s \<and> 0 < domain_time s \<and> invs' s') (handlePreemption_if tc)

goal (2 subgoals):
 1. no_fail (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) (do r <- handleEvent Interrupt;
y <- stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od)
 2. corres_underlying rf_sr False False (=) (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) (\<lambda>_. True) (do r <- handleEvent Interrupt;
return tc
od) (do y <- exec_C \<Gamma> handleInterruptEntry_C_body_if;
return tc
od) proof (prove)
goal (2 subgoals):
 1. no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> valid_domain_list s \<and> 0 < domain_time s \<and> invs' s') (do r <- handleEvent Interrupt;
y <- stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od) \<Longrightarrow> no_fail (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) (do r <- handleEvent Interrupt;
y <- stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od)
 2. corres_underlying rf_sr False False (=) (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) (\<lambda>_. True) (do r <- handleEvent Interrupt;
return tc
od) (do y <- exec_C \<Gamma> handleInterruptEntry_C_body_if;
return tc
od) proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) s \<Longrightarrow> \<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_list sa \<and> valid_sched sa \<and> valid_domain_list sa \<and> 0 < domain_time sa \<and> invs' s
 2. corres_underlying rf_sr False False (=) (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) (\<lambda>_. True) (do r <- handleEvent Interrupt;
return tc
od) (do y <- exec_C \<Gamma> handleInterruptEntry_C_body_if;
return tc
od) proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>invs' s; valid_domain_list' s; 0 < ksDomainTime s; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched sa\<rbrakk> \<Longrightarrow> \<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_list sa \<and> valid_sched sa \<and> valid_domain_list sa \<and> 0 < domain_time sa
 2. corres_underlying rf_sr False False (=) (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) (\<lambda>_. True) (do r <- handleEvent Interrupt;
return tc
od) (do y <- exec_C \<Gamma> handleInterruptEntry_C_body_if;
return tc
od) proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>invs' s; valid_domain_list' s; 0 < ksDomainTime s; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched sa\<rbrakk> \<Longrightarrow> invs sa \<and> valid_list sa \<and> valid_sched sa \<and> valid_domain_list sa \<and> 0 < domain_time sa
 2. corres_underlying rf_sr False False (=) (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) (\<lambda>_. True) (do r <- handleEvent Interrupt;
return tc
od) (do y <- exec_C \<Gamma> handleInterruptEntry_C_body_if;
return tc
od) proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr False False (=) (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) (\<lambda>_. True) (do r <- handleEvent Interrupt;
return tc
od) (do y <- exec_C \<Gamma> handleInterruptEntry_C_body_if;
return tc
od) proof (prove)
goal (3 subgoals):
 1. corres_underlying rf_sr False False (=) ?Q21 ?Q'21 (do r <- handleEvent Interrupt;
return tc
od) (do y <- exec_C \<Gamma> handleInterruptEntry_C_body_if;
return tc
od)
 2. \<And>s. (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) s \<Longrightarrow> ?Q21 s
 3. \<And>s. True \<Longrightarrow> ?Q'21 s proof (prove)
goal (6 subgoals):
 1. corres_underlying rf_sr False False dc ?P25 ?P'25 (handleEvent Interrupt) (exec_C \<Gamma> handleInterruptEntry_C_body_if)
 2. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R25 rv) (?R'25 rv') (return tc) (return tc)
 3. \<lbrace>?Q25\<rbrace> handleEvent Interrupt \<lbrace>?R25\<rbrace>
 4. \<lbrace>?Q'25\<rbrace> exec_C \<Gamma> handleInterruptEntry_C_body_if \<lbrace>?R'25\<rbrace>
 5. \<And>s. (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) s \<Longrightarrow> (?P25 and ?Q25) s
 6. \<And>s. True \<Longrightarrow> (?P'25 and ?Q'25) s proof (prove)
goal (7 subgoals):
 1. ccorres dc xfdc ?P25 (Collect ?P'25) [] (handleEvent Interrupt) handleInterruptEntry_C_body_if
 2. no_fail ?P25 (handleEvent Interrupt)
 3. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R25 rv) (?R'25 rv') (return tc) (return tc)
 4. \<lbrace>?Q25\<rbrace> handleEvent Interrupt \<lbrace>?R25\<rbrace>
 5. \<lbrace>?Q'25\<rbrace> exec_C \<Gamma> handleInterruptEntry_C_body_if \<lbrace>?R'25\<rbrace>
 6. \<And>s. (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) s \<Longrightarrow> (?P25 and ?Q25) s
 7. \<And>s. True \<Longrightarrow> (?P'25 and ?Q'25) s proof (prove)
goal (9 subgoals):
 1. ccorres dc xfdc ?Q31 ?Q'31 [] (handleEvent Interrupt) handleInterruptEntry_C_body_if
 2. \<And>s. ?P25 s \<Longrightarrow> ?Q31 s
 3. \<And>s. s \<in> Collect ?P'25 \<Longrightarrow> s \<in> ?Q'31
 4. no_fail ?P25 (handleEvent Interrupt)
 5. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R25 rv) (?R'25 rv') (return tc) (return tc)
 6. \<lbrace>?Q25\<rbrace> handleEvent Interrupt \<lbrace>?R25\<rbrace>
 7. \<lbrace>?Q'25\<rbrace> exec_C \<Gamma> handleInterruptEntry_C_body_if \<lbrace>?R'25\<rbrace>
 8. \<And>s. (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) s \<Longrightarrow> (?P25 and ?Q25) s
 9. \<And>s. True \<Longrightarrow> (?P'25 and ?Q'25) s proof (prove)
goal (10 subgoals):
 1. ccorres ?r'35 ?xf'35 ?Q31 ?Q'31 [] (handleEvent Interrupt) handleInterruptEntry_C_body_if
 2. \<And>x y. ?r'35 x (?xf'35 y) \<Longrightarrow> dc x (xfdc y)
 3. \<And>s. ?P25 s \<Longrightarrow> ?Q31 s
 4. \<And>s. s \<in> Collect ?P'25 \<Longrightarrow> s \<in> ?Q'31
 5. no_fail ?P25 (handleEvent Interrupt)
 6. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R25 rv) (?R'25 rv') (return tc) (return tc)
 7. \<lbrace>?Q25\<rbrace> handleEvent Interrupt \<lbrace>?R25\<rbrace>
 8. \<lbrace>?Q'25\<rbrace> exec_C \<Gamma> handleInterruptEntry_C_body_if \<lbrace>?R'25\<rbrace>
 9. \<And>s. (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) s \<Longrightarrow> (?P25 and ?Q25) s
 10. \<And>s. True \<Longrightarrow> (?P'25 and ?Q'25) s proof (prove)
goal (9 subgoals):
 1. \<And>x y. (K dc \<currency> dc) x (liftxf errstate id (K ()) ret__unsigned_long_' y) \<Longrightarrow> dc x (xfdc y)
 2. \<And>s. ?P25 s \<Longrightarrow> invs' s
 3. \<And>s. s \<in> Collect ?P'25 \<Longrightarrow> s \<in> UNIV
 4. no_fail ?P25 (handleEvent Interrupt)
 5. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R25 rv) (?R'25 rv') (return tc) (return tc)
 6. \<lbrace>?Q25\<rbrace> handleEvent Interrupt \<lbrace>?R25\<rbrace>
 7. \<lbrace>?Q'25\<rbrace> exec_C \<Gamma> handleInterruptEntry_C_body_if \<lbrace>?R'25\<rbrace>
 8. \<And>s. (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) s \<Longrightarrow> (?P25 and ?Q25) s
 9. \<And>s. True \<Longrightarrow> (?P'25 and ?Q'25) s proof (prove)
goal (8 subgoals):
 1. \<And>s. ?P25 s \<Longrightarrow> invs' s
 2. \<And>s. s \<in> Collect ?P'25 \<Longrightarrow> s \<in> UNIV
 3. no_fail ?P25 (handleEvent Interrupt)
 4. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R25 rv) (?R'25 rv') (return tc) (return tc)
 5. \<lbrace>?Q25\<rbrace> handleEvent Interrupt \<lbrace>?R25\<rbrace>
 6. \<lbrace>?Q'25\<rbrace> exec_C \<Gamma> handleInterruptEntry_C_body_if \<lbrace>?R'25\<rbrace>
 7. \<And>s. (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) s \<Longrightarrow> (?P25 and ?Q25) s
 8. \<And>s. True \<Longrightarrow> (?P'25 and ?Q'25) s proof (prove)
goal (8 subgoals):
 1. no_fail ?P25 (handleEvent Interrupt)
 2. \<And>s. ?P25 s \<Longrightarrow> invs' s
 3. \<And>s. s \<in> Collect ?P'25 \<Longrightarrow> s \<in> UNIV
 4. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R25 rv) (?R'25 rv') (return tc) (return tc)
 5. \<lbrace>?Q25\<rbrace> handleEvent Interrupt \<lbrace>?R25\<rbrace>
 6. \<lbrace>?Q'25\<rbrace> exec_C \<Gamma> handleInterruptEntry_C_body_if \<lbrace>?R'25\<rbrace>
 7. \<And>s. (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) s \<Longrightarrow> (?P25 and ?Q25) s
 8. \<And>s. True \<Longrightarrow> (?P'25 and ?Q'25) s proof (prove)
goal (7 subgoals):
 1. \<And>s. (invs' and ex_abs einvs) s \<Longrightarrow> invs' s
 2. \<And>s. s \<in> Collect ?P'25 \<Longrightarrow> s \<in> UNIV
 3. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R25 rv) (?R'25 rv') (return tc) (return tc)
 4. \<lbrace>?Q25\<rbrace> handleEvent Interrupt \<lbrace>?R25\<rbrace>
 5. \<lbrace>?Q'25\<rbrace> exec_C \<Gamma> handleInterruptEntry_C_body_if \<lbrace>?R'25\<rbrace>
 6. \<And>s. (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) s \<Longrightarrow> (invs' and ex_abs einvs and ?Q25) s
 7. \<And>s. True \<Longrightarrow> (?P'25 and ?Q'25) s proof (prove)
goal (6 subgoals):
 1. \<And>s. s \<in> Collect ?P'25 \<Longrightarrow> s \<in> UNIV
 2. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R25 rv) (?R'25 rv') (return tc) (return tc)
 3. \<lbrace>?Q25\<rbrace> handleEvent Interrupt \<lbrace>?R25\<rbrace>
 4. \<lbrace>?Q'25\<rbrace> exec_C \<Gamma> handleInterruptEntry_C_body_if \<lbrace>?R'25\<rbrace>
 5. \<And>s. (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) s \<Longrightarrow> (invs' and ex_abs einvs and ?Q25) s
 6. \<And>s. True \<Longrightarrow> (?P'25 and ?Q'25) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R25 rv) (?R'25 rv') (return tc) (return tc)
 2. \<lbrace>?Q25\<rbrace> handleEvent Interrupt \<lbrace>?R25\<rbrace>
 3. \<lbrace>?Q'25\<rbrace> exec_C \<Gamma> handleInterruptEntry_C_body_if \<lbrace>?R'25\<rbrace>
 4. \<And>s. (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) s \<Longrightarrow> (invs' and ex_abs einvs and ?Q25) s
 5. \<And>s. True \<Longrightarrow> (?P'25 and ?Q'25) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q25\<rbrace> handleEvent Interrupt \<lbrace>?R25\<rbrace>
 2. \<lbrace>?Q'25\<rbrace> exec_C \<Gamma> handleInterruptEntry_C_body_if \<lbrace>?R'25\<rbrace>
 3. \<And>s. (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) s \<Longrightarrow> (invs' and ex_abs einvs and ?Q25) s
 4. \<And>s. True \<Longrightarrow> (?P'25 and ?Q'25) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs' and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s) and ex_abs einvs) s \<Longrightarrow> (invs' and ex_abs einvs and (\<lambda>_. True)) s
 2. \<And>s. True \<Longrightarrow> (?P'25 and (\<lambda>_. True)) s proof (prove)
goal:
No subgoals!