theory Scheduler_IF

lemma timer_tick_snippit:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects_scheduler aag l (pas_refined aag and valid_queues and valid_etcbs
                                                         and valid_sched_action)
                                 (when (Suc 0 < numDomains)
                                    (do x \<leftarrow> dec_domain_time;
                                        dom_time \<leftarrow> gets domain_time;
                                        when (dom_time = 0) reschedule_required
                                     od))" apply (rule equiv_valid_guard_imp) apply (wp when_ev | wp (once) hoare_drop_imps)+ apply (clarsimp simp: scheduler_equiv_def) apply (wp reschedule_required_reads_respects_scheduler | wp (once) hoare_drop_imps)+ 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) (pas_refined aag and valid_queues and valid_etcbs and valid_sched_action) (when (Suc 0 < numDomains) (do x <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) proof (prove)
goal (2 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?Q (when (Suc 0 < numDomains) (do x <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od))
 2. \<And>s. (pas_refined aag and valid_queues and valid_etcbs and valid_sched_action) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>rv rva. \<lbrakk>Suc 0 < numDomains; rva = 0\<rbrakk> \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P7 rv rva) reschedule_required
 2. \<And>rv. Suc 0 < numDomains \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'6 rv) (gets domain_time)
 3. \<And>rv. Suc 0 < numDomains \<Longrightarrow> \<lbrace>?P''6 rv\<rbrace> gets domain_time \<lbrace>\<lambda>rva s. rva = 0 \<longrightarrow> ?P7 rv rva s\<rbrace>
 4. Suc 0 < numDomains \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'5 dec_domain_time
 5. Suc 0 < numDomains \<Longrightarrow> \<lbrace>?P''5\<rbrace> dec_domain_time \<lbrace>\<lambda>rv s. ?P'6 rv s \<and> ?P''6 rv s\<rbrace>
 6. \<And>s. (pas_refined aag and valid_queues and valid_etcbs and valid_sched_action) s \<Longrightarrow> Suc 0 < numDomains \<longrightarrow> ?P'5 s \<and> ?P''5 s proof (prove)
goal (6 subgoals):
 1. Suc 0 < numDomains \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P7 () 0) reschedule_required
 2. \<And>rv. Suc 0 < numDomains \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'6 rv) (gets domain_time)
 3. \<And>rv. Suc 0 < numDomains \<Longrightarrow> \<lbrace>?P''6 rv\<rbrace> gets domain_time \<lbrace>\<lambda>rva s. rva = 0 \<longrightarrow> ?P7 rv rva s\<rbrace>
 4. Suc 0 < numDomains \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'5 dec_domain_time
 5. Suc 0 < numDomains \<Longrightarrow> \<lbrace>?P''5\<rbrace> dec_domain_time \<lbrace>\<lambda>rv s. ?P'6 rv s \<and> ?P''6 rv s\<rbrace>
 6. \<And>s. (pas_refined aag and valid_queues and valid_etcbs and valid_sched_action) s \<Longrightarrow> Suc 0 < numDomains \<longrightarrow> ?P'5 s \<and> ?P''5 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and valid_queues and valid_etcbs and valid_sched_action) s \<Longrightarrow> Suc 0 < numDomains \<longrightarrow> True \<and> (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> domain_time s = domain_time t) \<and> pas_refined aag s \<and> valid_queues s \<and> valid_etcbs s \<and> valid_sched_action s proof (prove)
goal:
No subgoals!