theory Schedule_R

lemma corres_split_sched_act:
  "\<lbrakk>sched_act_relation act act';
    corres r P P' f1 g1;
    \<And>t. corres r (Q t) (Q' t) (f2 t) (g2 t);
    corres r R R' f3 g3\<rbrakk>
    \<Longrightarrow> corres r (case act of resume_cur_thread \<Rightarrow> P
                           | switch_thread t \<Rightarrow> Q t
                           | choose_new_thread \<Rightarrow> R)
               (case act' of ResumeCurrentThread \<Rightarrow> P'
                           | SwitchToThread t \<Rightarrow> Q' t
                           | ChooseThread \<Rightarrow> R')
       (case act of resume_cur_thread \<Rightarrow> f1
                  | switch_thread t \<Rightarrow> f2 t
                  | choose_new_thread \<Rightarrow> f3)
       (case act' of ResumeCurrentThread \<Rightarrow> g1
                   | ChooseNewThread \<Rightarrow> g3
                   | SwitchToThread t \<Rightarrow> g2 t)" apply (cases act) apply (rule corres_guard_imp, force+)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sched_act_relation act act'; corres r P P' f1 g1; \<And>t. corres r (Q t) (Q' t) (f2 t) (g2 t); corres r R R' f3 g3\<rbrakk> \<Longrightarrow> corres r (case act of resume_cur_thread \<Rightarrow> P | switch_thread t \<Rightarrow> Q t | choose_new_thread \<Rightarrow> R) (case act' of ResumeCurrentThread \<Rightarrow> P' | ChooseNewThread \<Rightarrow> R' | SwitchToThread t \<Rightarrow> Q' t) (case act of resume_cur_thread \<Rightarrow> f1 | switch_thread t \<Rightarrow> f2 t | choose_new_thread \<Rightarrow> f3) (case act' of ResumeCurrentThread \<Rightarrow> g1 | ChooseNewThread \<Rightarrow> g3 | SwitchToThread t \<Rightarrow> g2 t) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>sched_act_relation act act'; corres r P P' f1 g1; \<And>t. corres r (Q t) (Q' t) (f2 t) (g2 t); corres r R R' f3 g3; act = resume_cur_thread\<rbrakk> \<Longrightarrow> corres r (case act of resume_cur_thread \<Rightarrow> P | switch_thread t \<Rightarrow> Q t | choose_new_thread \<Rightarrow> R) (case act' of ResumeCurrentThread \<Rightarrow> P' | ChooseNewThread \<Rightarrow> R' | SwitchToThread t \<Rightarrow> Q' t) (case act of resume_cur_thread \<Rightarrow> f1 | switch_thread t \<Rightarrow> f2 t | choose_new_thread \<Rightarrow> f3) (case act' of ResumeCurrentThread \<Rightarrow> g1 | ChooseNewThread \<Rightarrow> g3 | SwitchToThread t \<Rightarrow> g2 t)
 2. \<And>x2. \<lbrakk>sched_act_relation act act'; corres r P P' f1 g1; \<And>t. corres r (Q t) (Q' t) (f2 t) (g2 t); corres r R R' f3 g3; act = switch_thread x2\<rbrakk> \<Longrightarrow> corres r (case act of resume_cur_thread \<Rightarrow> P | switch_thread t \<Rightarrow> Q t | choose_new_thread \<Rightarrow> R) (case act' of ResumeCurrentThread \<Rightarrow> P' | ChooseNewThread \<Rightarrow> R' | SwitchToThread t \<Rightarrow> Q' t) (case act of resume_cur_thread \<Rightarrow> f1 | switch_thread t \<Rightarrow> f2 t | choose_new_thread \<Rightarrow> f3) (case act' of ResumeCurrentThread \<Rightarrow> g1 | ChooseNewThread \<Rightarrow> g3 | SwitchToThread t \<Rightarrow> g2 t)
 3. \<lbrakk>sched_act_relation act act'; corres r P P' f1 g1; \<And>t. corres r (Q t) (Q' t) (f2 t) (g2 t); corres r R R' f3 g3; act = choose_new_thread\<rbrakk> \<Longrightarrow> corres r (case act of resume_cur_thread \<Rightarrow> P | switch_thread t \<Rightarrow> Q t | choose_new_thread \<Rightarrow> R) (case act' of ResumeCurrentThread \<Rightarrow> P' | ChooseNewThread \<Rightarrow> R' | SwitchToThread t \<Rightarrow> Q' t) (case act of resume_cur_thread \<Rightarrow> f1 | switch_thread t \<Rightarrow> f2 t | choose_new_thread \<Rightarrow> f3) (case act' of ResumeCurrentThread \<Rightarrow> g1 | ChooseNewThread \<Rightarrow> g3 | SwitchToThread t \<Rightarrow> g2 t) proof (prove)
goal:
No subgoals!