theory ADT_IF_Refine

lemma schedule_if_corres:
 "corres (=) (invs and valid_sched and valid_list and valid_domain_list
                   and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread))
             (invs') (schedule_if tc) (schedule'_if tc)" apply (simp add: schedule_if_def schedule'_if_def) apply (rule corres_guard_imp) apply (rule corres_split[where r'="dc"]) apply (rule schedule_corres) apply (rule corres_split[where r'="dc"]) apply (rule activateThread_corres) apply (rule corres_stateAssert_assume_stronger
                      [where Q=\<top> and P="\<lambda>s. valid_domain_list s \<and> 0 < domain_time s"]) apply simp apply (clarsimp simp: state_relation_def) apply wp+ apply (wp schedule_invs' schedule_domain_time_left)+ apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (invs and valid_sched and valid_list and valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)) invs' (schedule_if tc) (schedule'_if tc) proof (prove)
goal (1 subgoal):
 1. corres (=) (invs and valid_sched and valid_list and valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)) invs' (do y <- state_ext_sched_class.schedule;
y <- activate_thread;
return tc
od) (do y <- ThreadDecls_H.schedule;
y <- activateThread;
y <- stateAssert (\<lambda>s. 0 < ksDomainTime s \<and> valid_domain_list' s) [];
return tc
od) proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q ?Q' (do y <- state_ext_sched_class.schedule;
y <- activate_thread;
return tc
od) (do y <- ThreadDecls_H.schedule;
y <- activateThread;
y <- stateAssert (\<lambda>s. 0 < ksDomainTime s \<and> valid_domain_list' s) [];
return tc
od)
 2. \<And>s. (invs and valid_sched and valid_list and valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)) s \<Longrightarrow> ?Q s
 3. \<And>s. invs' s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. corres dc ?P4 ?P'4 state_ext_sched_class.schedule ThreadDecls_H.schedule
 2. \<And>y ya. dc y ya \<Longrightarrow> corres (=) (?R4 y) (?R'4 ya) (do y <- activate_thread;
return tc
od) (do y <- activateThread;
y <- stateAssert (\<lambda>s. 0 < ksDomainTime s \<and> valid_domain_list' s) [];
return tc
od)
 3. \<lbrace>?Q4\<rbrace> state_ext_sched_class.schedule \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> ThreadDecls_H.schedule \<lbrace>?R'4\<rbrace>
 5. \<And>s. (invs and valid_sched and valid_list and valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)) s \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s. invs' s \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>y ya. dc y ya \<Longrightarrow> corres (=) (?R4 y) (?R'4 ya) (do y <- activate_thread;
return tc
od) (do y <- activateThread;
y <- stateAssert (\<lambda>s. 0 < ksDomainTime s \<and> valid_domain_list' s) [];
return tc
od)
 2. \<lbrace>?Q4\<rbrace> state_ext_sched_class.schedule \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> ThreadDecls_H.schedule \<lbrace>?R'4\<rbrace>
 4. \<And>s. (invs and valid_sched and valid_list and valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)) s \<Longrightarrow> (invs and valid_sched and valid_list and ?Q4) s
 5. \<And>s. invs' s \<Longrightarrow> (invs' and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>y ya. dc y ya \<Longrightarrow> corres dc (?P10 y) (?P'12 ya) activate_thread activateThread
 2. \<And>y ya yb yc. \<lbrakk>dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> corres (=) (?R9 y ya yb) (?R'9 y ya yc) (return tc) (do y <- stateAssert (\<lambda>s. 0 < ksDomainTime s \<and> valid_domain_list' s) [];
return tc
od)
 3. \<And>y ya. dc y ya \<Longrightarrow> \<lbrace>?Q11 y\<rbrace> activate_thread \<lbrace>?R9 y ya\<rbrace>
 4. \<And>y ya. dc y ya \<Longrightarrow> \<lbrace>?Q'13 ya\<rbrace> activateThread \<lbrace>?R'9 y ya\<rbrace>
 5. \<lbrace>?Q4\<rbrace> state_ext_sched_class.schedule \<lbrace>\<lambda>y. ?P10 y and ?Q11 y\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>ya. ?P'12 ya and ?Q'13 ya\<rbrace>
 7. \<And>s. (invs and valid_sched and valid_list and valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)) s \<Longrightarrow> (invs and valid_sched and valid_list and ?Q4) s
 8. \<And>s. invs' s \<Longrightarrow> (invs' and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>y ya yb yc. \<lbrakk>dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> corres (=) (?R9 y ya yb) (?R'9 y ya yc) (return tc) (do y <- stateAssert (\<lambda>s. 0 < ksDomainTime s \<and> valid_domain_list' s) [];
return tc
od)
 2. \<And>y ya. dc y ya \<Longrightarrow> \<lbrace>?Q11 y\<rbrace> activate_thread \<lbrace>?R9 y ya\<rbrace>
 3. \<And>y ya. dc y ya \<Longrightarrow> \<lbrace>?Q'13 ya\<rbrace> activateThread \<lbrace>?R'9 y ya\<rbrace>
 4. \<lbrace>?Q4\<rbrace> state_ext_sched_class.schedule \<lbrace>\<lambda>y. invs and ct_in_state activatable and ?Q11 y\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>ya. invs' and ct_in_state' activatable' and ?Q'13 ya\<rbrace>
 6. \<And>s. (invs and valid_sched and valid_list and valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)) s \<Longrightarrow> (invs and valid_sched and valid_list and ?Q4) s
 7. \<And>s. invs' s \<Longrightarrow> (invs' and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>y ya yb yc. \<lbrakk>dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>s. valid_domain_list s \<and> 0 < domain_time s) (\<lambda>_. True) (return tc) (return tc)
 2. \<And>y ya yb yc s s'. \<lbrakk>dc y ya; dc yb yc; (s, s') \<in> state_relation; valid_domain_list s \<and> 0 < domain_time s; True\<rbrakk> \<Longrightarrow> 0 < ksDomainTime s' \<and> valid_domain_list' s'
 3. \<And>y ya. dc y ya \<Longrightarrow> \<lbrace>?Q11 y\<rbrace> activate_thread \<lbrace>\<lambda>yb s. valid_domain_list s \<and> 0 < domain_time s\<rbrace>
 4. \<And>y ya. dc y ya \<Longrightarrow> \<lbrace>?Q'13 ya\<rbrace> activateThread \<lbrace>\<lambda>yc _. True\<rbrace>
 5. \<lbrace>?Q4\<rbrace> state_ext_sched_class.schedule \<lbrace>\<lambda>y. invs and ct_in_state activatable and ?Q11 y\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>ya. invs' and ct_in_state' activatable' and ?Q'13 ya\<rbrace>
 7. \<And>s. (invs and valid_sched and valid_list and valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)) s \<Longrightarrow> (invs and valid_sched and valid_list and ?Q4) s
 8. \<And>s. invs' s \<Longrightarrow> (invs' and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>y ya yb yc s s'. \<lbrakk>dc y ya; dc yb yc; (s, s') \<in> state_relation; valid_domain_list s \<and> 0 < domain_time s; True\<rbrakk> \<Longrightarrow> 0 < ksDomainTime s' \<and> valid_domain_list' s'
 2. \<And>y ya. dc y ya \<Longrightarrow> \<lbrace>?Q11 y\<rbrace> activate_thread \<lbrace>\<lambda>yb s. valid_domain_list s \<and> 0 < domain_time s\<rbrace>
 3. \<And>y ya. dc y ya \<Longrightarrow> \<lbrace>?Q'13 ya\<rbrace> activateThread \<lbrace>\<lambda>yc _. True\<rbrace>
 4. \<lbrace>?Q4\<rbrace> state_ext_sched_class.schedule \<lbrace>\<lambda>y. invs and ct_in_state activatable and ?Q11 y\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>ya. invs' and ct_in_state' activatable' and ?Q'13 ya\<rbrace>
 6. \<And>s. (invs and valid_sched and valid_list and valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)) s \<Longrightarrow> (invs and valid_sched and valid_list and ?Q4) s
 7. \<And>s. invs' s \<Longrightarrow> (invs' and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>y ya. dc y ya \<Longrightarrow> \<lbrace>?Q11 y\<rbrace> activate_thread \<lbrace>\<lambda>yb s. valid_domain_list s \<and> 0 < domain_time s\<rbrace>
 2. \<And>y ya. dc y ya \<Longrightarrow> \<lbrace>?Q'13 ya\<rbrace> activateThread \<lbrace>\<lambda>yc _. True\<rbrace>
 3. \<lbrace>?Q4\<rbrace> state_ext_sched_class.schedule \<lbrace>\<lambda>y. invs and ct_in_state activatable and ?Q11 y\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>ya. invs' and ct_in_state' activatable' and ?Q'13 ya\<rbrace>
 5. \<And>s. (invs and valid_sched and valid_list and valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)) s \<Longrightarrow> (invs and valid_sched and valid_list and ?Q4) s
 6. \<And>s. invs' s \<Longrightarrow> (invs' and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'32\<rbrace> state_ext_sched_class.schedule \<lbrace>\<lambda>rv s. 0 < domain_time s\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>ya. invs' and ct_in_state' activatable' and (\<lambda>_. True)\<rbrace>
 3. \<And>s. (invs and valid_sched and valid_list and valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)) s \<Longrightarrow> (invs and valid_sched and valid_list and (\<lambda>s. invs s \<and> invs s \<and> valid_domain_list s \<and> ?P'32 s)) s
 4. \<And>s. invs' s \<Longrightarrow> (invs' and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs and valid_sched and valid_list and valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)) s \<Longrightarrow> (invs and valid_sched and valid_list and (\<lambda>s. invs s \<and> invs s \<and> valid_domain_list s \<and> (valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)) s)) s
 2. \<And>s. invs' s \<Longrightarrow> (invs' and (\<lambda>s. invs' s \<and> invs' s \<and> True)) s proof (prove)
goal:
No subgoals!