theory DetSchedSchedule_AI

lemma choose_thread_cur_dom_or_idle:
  "\<lbrace> valid_queues \<rbrace>
   choose_thread
   \<lbrace>\<lambda>_ s. (in_cur_domain (cur_thread s) s \<or> cur_thread s = idle_thread s) \<rbrace>" apply (wpsimp simp: choose_thread_def
                wp: guarded_switch_to_lift) apply (rule hoare_disjI2)  (* idle thread *)
       apply wp apply (rule hoare_disjI1)  (* in current domain *)
      apply (wp guarded_switch_to_lift)+ apply clarsimp apply (fastforce dest!: next_thread_queued split: option.splits
                   simp: etcb_at_def next_thread_def valid_queues_def in_cur_domain_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues\<rbrace> choose_thread \<lbrace>\<lambda>_ s. in_cur_domain (cur_thread s) s \<or> cur_thread s = idle_thread s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>d queues. \<forall>prio. queues prio = [] \<Longrightarrow> \<lbrace>?Q4 d queues\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>_ s. in_cur_domain (cur_thread s) s \<or> cur_thread s = idle_thread s\<rbrace>
 2. \<And>d queues. \<not> (\<forall>prio. queues prio = []) \<Longrightarrow> \<lbrace>?R4 d queues\<rbrace> guarded_switch_to (hd (max_non_empty_queue queues)) \<lbrace>\<lambda>_ s. in_cur_domain (cur_thread s) s \<or> cur_thread s = idle_thread s\<rbrace>
 3. \<And>d. \<lbrace>?B2 d\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>\<lambda>queues s. ((\<forall>prio. queues prio = []) \<longrightarrow> ?Q4 d queues s) \<and> (\<not> (\<forall>prio. queues prio = []) \<longrightarrow> ?R4 d queues s)\<rbrace>
 4. \<lbrace>?Q1\<rbrace> gets cur_domain \<lbrace>?B2\<rbrace>
 5. \<And>s. valid_queues s \<Longrightarrow> ?Q1 s proof (prove)
goal (5 subgoals):
 1. \<And>d queues. \<forall>prio. queues prio = [] \<Longrightarrow> \<lbrace>?Q4 d queues\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>rv s. cur_thread s = idle_thread s\<rbrace>
 2. \<And>d queues. \<not> (\<forall>prio. queues prio = []) \<Longrightarrow> \<lbrace>?R4 d queues\<rbrace> guarded_switch_to (hd (max_non_empty_queue queues)) \<lbrace>\<lambda>_ s. in_cur_domain (cur_thread s) s \<or> cur_thread s = idle_thread s\<rbrace>
 3. \<And>d. \<lbrace>?B2 d\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>\<lambda>queues s. ((\<forall>prio. queues prio = []) \<longrightarrow> ?Q4 d queues s) \<and> (\<not> (\<forall>prio. queues prio = []) \<longrightarrow> ?R4 d queues s)\<rbrace>
 4. \<lbrace>?Q1\<rbrace> gets cur_domain \<lbrace>?B2\<rbrace>
 5. \<And>s. valid_queues s \<Longrightarrow> ?Q1 s proof (prove)
goal (5 subgoals):
 1. \<And>d queues. \<forall>prio. queues prio = [] \<Longrightarrow> \<lbrace>?Q4 d queues\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>rv s. cur_thread s = idle_thread s\<rbrace>
 2. \<And>d queues. \<not> (\<forall>prio. queues prio = []) \<Longrightarrow> \<lbrace>?R4 d queues\<rbrace> guarded_switch_to (hd (max_non_empty_queue queues)) \<lbrace>\<lambda>_ s. in_cur_domain (cur_thread s) s \<or> cur_thread s = idle_thread s\<rbrace>
 3. \<And>d. \<lbrace>?B2 d\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>\<lambda>queues s. ((\<forall>prio. queues prio = []) \<longrightarrow> ?Q4 d queues s) \<and> (\<not> (\<forall>prio. queues prio = []) \<longrightarrow> ?R4 d queues s)\<rbrace>
 4. \<lbrace>?Q1\<rbrace> gets cur_domain \<lbrace>?B2\<rbrace>
 5. \<And>s. valid_queues s \<Longrightarrow> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<And>d queues. \<not> (\<forall>prio. queues prio = []) \<Longrightarrow> \<lbrace>?R4 d queues\<rbrace> guarded_switch_to (hd (max_non_empty_queue queues)) \<lbrace>\<lambda>_ s. in_cur_domain (cur_thread s) s \<or> cur_thread s = idle_thread s\<rbrace>
 2. \<And>d. \<lbrace>?B2 d\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>\<lambda>queues s. ((\<forall>prio. queues prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. queues prio = []) \<longrightarrow> ?R4 d queues s)\<rbrace>
 3. \<lbrace>?Q1\<rbrace> gets cur_domain \<lbrace>?B2\<rbrace>
 4. \<And>s. valid_queues s \<Longrightarrow> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<And>d queues. \<not> (\<forall>prio. queues prio = []) \<Longrightarrow> \<lbrace>?R4 d queues\<rbrace> guarded_switch_to (hd (max_non_empty_queue queues)) \<lbrace>\<lambda>rv s. in_cur_domain (cur_thread s) s\<rbrace>
 2. \<And>d. \<lbrace>?B2 d\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>\<lambda>queues s. ((\<forall>prio. queues prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. queues prio = []) \<longrightarrow> ?R4 d queues s)\<rbrace>
 3. \<lbrace>?Q1\<rbrace> gets cur_domain \<lbrace>?B2\<rbrace>
 4. \<And>s. valid_queues s \<Longrightarrow> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<And>d queues. \<not> (\<forall>prio. queues prio = []) \<Longrightarrow> \<lbrace>?R4 d queues\<rbrace> guarded_switch_to (hd (max_non_empty_queue queues)) \<lbrace>\<lambda>rv s. in_cur_domain (cur_thread s) s\<rbrace>
 2. \<And>d. \<lbrace>?B2 d\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>\<lambda>queues s. ((\<forall>prio. queues prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. queues prio = []) \<longrightarrow> ?R4 d queues s)\<rbrace>
 3. \<lbrace>?Q1\<rbrace> gets cur_domain \<lbrace>?B2\<rbrace>
 4. \<And>s. valid_queues s \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_queues s \<Longrightarrow> ((\<forall>prio. ready_queues s (cur_domain s) prio = []) \<longrightarrow> True) \<and> (\<not> (\<forall>prio. ready_queues s (cur_domain s) prio = []) \<longrightarrow> in_cur_domain (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s prio. \<lbrakk>valid_queues s; ready_queues s (cur_domain s) prio \<noteq> []\<rbrakk> \<Longrightarrow> in_cur_domain (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s proof (prove)
goal:
No subgoals!