theory Scheduler_IF

lemma next_domain_snippit:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects_scheduler aag l (invs and pas_refined aag and valid_queues)
           (do dom_time \<leftarrow> gets domain_time;
               y \<leftarrow> when (dom_time = 0) next_domain;
               y \<leftarrow> choose_thread;
               set_scheduler_action resume_cur_thread
            od)" apply (simp add: when_def) apply (rule bind_ev_pre) apply (rule bind_ev_general) apply (simp add: when_def) apply (rule choose_thread_reads_respects_scheduler[OF domains_distinct]) apply (wp next_domain_midstrength_equiv_scheduler) apply (rule ev_weaken_pre_relation) apply (rule next_domain_midstrength_equiv_scheduler) apply fastforce apply (rule ev_weaken_pre_relation) apply wp apply fastforce apply (wp next_domain_valid_queues)+ apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and pas_refined aag and valid_queues) (do dom_time <- gets domain_time;
y <- when (dom_time = 0) next_domain;
y <- choose_thread;
set_scheduler_action resume_cur_thread
od) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and pas_refined aag and valid_queues) (do dom_time <- gets domain_time;
y <- if dom_time = 0 then next_domain else return ();
y <- choose_thread;
set_scheduler_action resume_cur_thread
od) proof (prove)
goal (4 subgoals):
 1. \<And>rv. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?Q rv) (do y <- if rv = 0 then next_domain else return ();
y <- choose_thread;
set_scheduler_action resume_cur_thread
od)
 2. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P' (gets domain_time)
 3. \<lbrace>?P''\<rbrace> gets domain_time \<lbrace>?Q\<rbrace>
 4. \<And>s. (invs and pas_refined aag and valid_queues) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (6 subgoals):
 1. \<And>rv rva. equiv_valid (scheduler_equiv aag) (?B5 rv) (scheduler_affects_equiv aag l) (?Q5 rv rva) (do y <- choose_thread;
set_scheduler_action resume_cur_thread
od)
 2. \<And>rv. equiv_valid (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?B5 rv) (?P'5 rv) (if rv = 0 then next_domain else return ())
 3. \<And>rv. \<lbrace>?P''5 rv\<rbrace> if rv = 0 then next_domain else return () \<lbrace>?Q5 rv\<rbrace>
 4. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P' (gets domain_time)
 5. \<lbrace>?P''\<rbrace> gets domain_time \<lbrace>\<lambda>rv s. ?P'5 rv s \<and> ?P''5 rv s\<rbrace>
 6. \<And>s. (invs and pas_refined aag and valid_queues) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (6 subgoals):
 1. \<And>rv. equiv_valid (scheduler_equiv aag) (?B5 rv) (scheduler_affects_equiv aag l) (?Q5 rv ()) (do y <- choose_thread;
set_scheduler_action resume_cur_thread
od)
 2. \<And>rv. equiv_valid (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?B5 rv) (?P'5 rv) (if rv = 0 then next_domain else return ())
 3. \<And>rv. \<lbrace>?P''5 rv\<rbrace> if rv = 0 then next_domain else return () \<lbrace>?Q5 rv\<rbrace>
 4. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P' (gets domain_time)
 5. \<lbrace>?P''\<rbrace> gets domain_time \<lbrace>\<lambda>rv s. ?P'5 rv s \<and> ?P''5 rv s\<rbrace>
 6. \<And>s. (invs and pas_refined aag and valid_queues) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (5 subgoals):
 1. \<And>rv. equiv_valid (scheduler_equiv aag) (scheduler_affects_equiv aag l) (midstrength_scheduler_affects_equiv aag l) (?P'5 rv) (if rv = 0 then next_domain else return ())
 2. \<And>rv. \<lbrace>?P''5 rv\<rbrace> if rv = 0 then next_domain else return () \<lbrace>\<lambda>a. invs and pas_refined aag and valid_queues\<rbrace>
 3. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P' (gets domain_time)
 4. \<lbrace>?P''\<rbrace> gets domain_time \<lbrace>\<lambda>rv s. ?P'5 rv s \<and> ?P''5 rv s\<rbrace>
 5. \<And>s. (invs and pas_refined aag and valid_queues) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (6 subgoals):
 1. \<And>rv. rv = 0 \<Longrightarrow> equiv_valid (scheduler_equiv aag) (scheduler_affects_equiv aag l) (midstrength_scheduler_affects_equiv aag l) (?P11 rv) next_domain
 2. \<And>rv. rv \<noteq> 0 \<Longrightarrow> equiv_valid (scheduler_equiv aag) (scheduler_affects_equiv aag l) (midstrength_scheduler_affects_equiv aag l) (?Q11 rv) (return ())
 3. \<And>rv. \<lbrace>?P''5 rv\<rbrace> if rv = 0 then next_domain else return () \<lbrace>\<lambda>a. invs and pas_refined aag and valid_queues\<rbrace>
 4. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P' (gets domain_time)
 5. \<lbrace>?P''\<rbrace> gets domain_time \<lbrace>\<lambda>rv s. ((rv = 0 \<longrightarrow> ?P11 rv s) \<and> (rv \<noteq> 0 \<longrightarrow> ?Q11 rv s)) \<and> ?P''5 rv s\<rbrace>
 6. \<And>s. (invs and pas_refined aag and valid_queues) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (7 subgoals):
 1. \<And>rv. rv = 0 \<Longrightarrow> equiv_valid (scheduler_equiv aag) (?A13 rv) (midstrength_scheduler_affects_equiv aag l) (?P11 rv) next_domain
 2. \<And>rv s t. \<lbrakk>rv = 0; scheduler_affects_equiv aag l s t\<rbrakk> \<Longrightarrow> ?A13 rv s t
 3. \<And>rv. rv \<noteq> 0 \<Longrightarrow> equiv_valid (scheduler_equiv aag) (scheduler_affects_equiv aag l) (midstrength_scheduler_affects_equiv aag l) (?Q11 rv) (return ())
 4. \<And>rv. \<lbrace>?P''5 rv\<rbrace> if rv = 0 then next_domain else return () \<lbrace>\<lambda>a. invs and pas_refined aag and valid_queues\<rbrace>
 5. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P' (gets domain_time)
 6. \<lbrace>?P''\<rbrace> gets domain_time \<lbrace>\<lambda>rv s. ((rv = 0 \<longrightarrow> ?P11 rv s) \<and> (rv \<noteq> 0 \<longrightarrow> ?Q11 rv s)) \<and> ?P''5 rv s\<rbrace>
 7. \<And>s. (invs and pas_refined aag and valid_queues) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (6 subgoals):
 1. \<And>rv s t. \<lbrakk>rv = 0; scheduler_affects_equiv aag l s t\<rbrakk> \<Longrightarrow> weak_scheduler_affects_equiv aag l s t
 2. \<And>rv. rv \<noteq> 0 \<Longrightarrow> equiv_valid (scheduler_equiv aag) (scheduler_affects_equiv aag l) (midstrength_scheduler_affects_equiv aag l) (?Q11 rv) (return ())
 3. \<And>rv. \<lbrace>?P''5 rv\<rbrace> if rv = 0 then next_domain else return () \<lbrace>\<lambda>a. invs and pas_refined aag and valid_queues\<rbrace>
 4. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P' (gets domain_time)
 5. \<lbrace>?P''\<rbrace> gets domain_time \<lbrace>\<lambda>rv s. ((rv = 0 \<longrightarrow> True) \<and> (rv \<noteq> 0 \<longrightarrow> ?Q11 rv s)) \<and> ?P''5 rv s\<rbrace>
 6. \<And>s. (invs and pas_refined aag and valid_queues) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (5 subgoals):
 1. \<And>rv. rv \<noteq> 0 \<Longrightarrow> equiv_valid (scheduler_equiv aag) (scheduler_affects_equiv aag l) (midstrength_scheduler_affects_equiv aag l) (?Q11 rv) (return ())
 2. \<And>rv. \<lbrace>?P''5 rv\<rbrace> if rv = 0 then next_domain else return () \<lbrace>\<lambda>a. invs and pas_refined aag and valid_queues\<rbrace>
 3. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P' (gets domain_time)
 4. \<lbrace>?P''\<rbrace> gets domain_time \<lbrace>\<lambda>rv s. ((rv = 0 \<longrightarrow> True) \<and> (rv \<noteq> 0 \<longrightarrow> ?Q11 rv s)) \<and> ?P''5 rv s\<rbrace>
 5. \<And>s. (invs and pas_refined aag and valid_queues) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (6 subgoals):
 1. \<And>rv. rv \<noteq> 0 \<Longrightarrow> equiv_valid (scheduler_equiv aag) (?A21 rv) (midstrength_scheduler_affects_equiv aag l) (?Q11 rv) (return ())
 2. \<And>rv s t. \<lbrakk>rv \<noteq> 0; scheduler_affects_equiv aag l s t\<rbrakk> \<Longrightarrow> ?A21 rv s t
 3. \<And>rv. \<lbrace>?P''5 rv\<rbrace> if rv = 0 then next_domain else return () \<lbrace>\<lambda>a. invs and pas_refined aag and valid_queues\<rbrace>
 4. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P' (gets domain_time)
 5. \<lbrace>?P''\<rbrace> gets domain_time \<lbrace>\<lambda>rv s. ((rv = 0 \<longrightarrow> True) \<and> (rv \<noteq> 0 \<longrightarrow> ?Q11 rv s)) \<and> ?P''5 rv s\<rbrace>
 6. \<And>s. (invs and pas_refined aag and valid_queues) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (5 subgoals):
 1. \<And>rv s t. \<lbrakk>rv \<noteq> 0; scheduler_affects_equiv aag l s t\<rbrakk> \<Longrightarrow> midstrength_scheduler_affects_equiv aag l s t
 2. \<And>rv. \<lbrace>?P''5 rv\<rbrace> if rv = 0 then next_domain else return () \<lbrace>\<lambda>a. invs and pas_refined aag and valid_queues\<rbrace>
 3. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P' (gets domain_time)
 4. \<lbrace>?P''\<rbrace> gets domain_time \<lbrace>\<lambda>rv s. ((rv = 0 \<longrightarrow> True) \<and> (rv \<noteq> 0 \<longrightarrow> True)) \<and> ?P''5 rv s\<rbrace>
 5. \<And>s. (invs and pas_refined aag and valid_queues) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (4 subgoals):
 1. \<And>rv. \<lbrace>?P''5 rv\<rbrace> if rv = 0 then next_domain else return () \<lbrace>\<lambda>a. invs and pas_refined aag and valid_queues\<rbrace>
 2. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P' (gets domain_time)
 3. \<lbrace>?P''\<rbrace> gets domain_time \<lbrace>\<lambda>rv s. ((rv = 0 \<longrightarrow> True) \<and> (rv \<noteq> 0 \<longrightarrow> True)) \<and> ?P''5 rv s\<rbrace>
 4. \<And>s. (invs and pas_refined aag and valid_queues) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and pas_refined aag and valid_queues) s \<Longrightarrow> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> domain_time s = domain_time t) \<and> ((domain_time s = 0 \<longrightarrow> True) \<and> (domain_time s \<noteq> 0 \<longrightarrow> True)) \<and> (domain_time s = 0 \<longrightarrow> invs s \<and> pas_refined aag s \<and> valid_queues s) \<and> (domain_time s \<noteq> 0 \<longrightarrow> invs s \<and> pas_refined aag s \<and> valid_queues s) proof (prove)
goal:
No subgoals!