theory DetSchedAux_AI

lemma invoke_untyped_valid_sched:
  "\<lbrace>invs and valid_untyped_inv ui and ct_active and valid_sched and valid_idle \<rbrace>
     invoke_untyped ui
   \<lbrace> \<lambda>_ . valid_sched \<rbrace>" including no_pre apply (rule hoare_pre) apply (rule_tac I="invs and valid_untyped_inv ui and ct_active"
     in valid_sched_tcb_state_preservation) apply (wp invoke_untyped_st_tcb_at) apply simp apply (wp invoke_untyped_etcb_at)+ apply (rule hoare_post_impErr, rule hoare_pre, rule invoke_untyp_invs,
        simp_all add: invs_valid_idle)[1] apply (rule_tac f="\<lambda>s. P (scheduler_action s)" in hoare_lift_Pf) apply (rule_tac f="\<lambda>s. x (ready_queues s)" in hoare_lift_Pf) apply wp+ apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_untyped_inv ui and ct_active and valid_sched and valid_idle\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_untyped_inv ui and ct_active and valid_sched and valid_idle\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. valid_sched\<rbrace>
 2. \<And>s. (invs and valid_untyped_inv ui and ct_active and valid_sched and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>P t. \<lbrace>invs and valid_untyped_inv ui and ct_active and ct_active and st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. st_tcb_at P t\<rbrace>
 2. \<And>P t. \<lbrace>etcb_at P t and valid_etcbs\<rbrace> invoke_untyped ui \<lbrace>\<lambda>r s. st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> invoke_untyped ui \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>
 4. \<And>P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> invoke_untyped ui \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>
 5. \<lbrace>valid_etcbs\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. valid_etcbs\<rbrace>
 6. \<lbrace>valid_blocked\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. valid_blocked\<rbrace>
 7. \<lbrace>invs and valid_untyped_inv ui and ct_active\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. valid_idle\<rbrace>
 8. \<And>P. \<lbrace>\<lambda>s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace> invoke_untyped ui \<lbrace>\<lambda>r s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace>
 9. \<And>s. (invs and valid_untyped_inv ui and ct_active and valid_sched and valid_idle) s \<Longrightarrow> (invs and valid_untyped_inv ui and ct_active and ct_active and valid_sched and valid_idle) s proof (prove)
goal (9 subgoals):
 1. \<And>P t s. (invs and valid_untyped_inv ui and ct_active and ct_active and st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t) s \<Longrightarrow> (invs and st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t and ct_active and valid_untyped_inv ui) s
 2. \<And>P t. \<lbrace>etcb_at P t and valid_etcbs\<rbrace> invoke_untyped ui \<lbrace>\<lambda>r s. st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> invoke_untyped ui \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>
 4. \<And>P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> invoke_untyped ui \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>
 5. \<lbrace>valid_etcbs\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. valid_etcbs\<rbrace>
 6. \<lbrace>valid_blocked\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. valid_blocked\<rbrace>
 7. \<lbrace>invs and valid_untyped_inv ui and ct_active\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. valid_idle\<rbrace>
 8. \<And>P. \<lbrace>\<lambda>s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace> invoke_untyped ui \<lbrace>\<lambda>r s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace>
 9. \<And>s. (invs and valid_untyped_inv ui and ct_active and valid_sched and valid_idle) s \<Longrightarrow> (invs and valid_untyped_inv ui and ct_active and ct_active and valid_sched and valid_idle) s proof (prove)
goal (8 subgoals):
 1. \<And>P t. \<lbrace>etcb_at P t and valid_etcbs\<rbrace> invoke_untyped ui \<lbrace>\<lambda>r s. st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> invoke_untyped ui \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> invoke_untyped ui \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>
 4. \<lbrace>valid_etcbs\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. valid_etcbs\<rbrace>
 5. \<lbrace>valid_blocked\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. valid_blocked\<rbrace>
 6. \<lbrace>invs and valid_untyped_inv ui and ct_active\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. valid_idle\<rbrace>
 7. \<And>P. \<lbrace>\<lambda>s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace> invoke_untyped ui \<lbrace>\<lambda>r s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace>
 8. \<And>s. (invs and valid_untyped_inv ui and ct_active and valid_sched and valid_idle) s \<Longrightarrow> (invs and valid_untyped_inv ui and ct_active and ct_active and valid_sched and valid_idle) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>invs and valid_untyped_inv ui and ct_active\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. valid_idle\<rbrace>, \<lbrace>\<lambda>_. valid_idle\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace> invoke_untyped ui \<lbrace>\<lambda>r s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace>
 3. \<And>s. (invs and valid_untyped_inv ui and ct_active and valid_sched and valid_idle) s \<Longrightarrow> (invs and valid_untyped_inv ui and ct_active and ct_active and valid_sched and valid_idle) s proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace> invoke_untyped ui \<lbrace>\<lambda>r s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace>
 2. \<And>s. (invs and valid_untyped_inv ui and ct_active and valid_sched and valid_idle) s \<Longrightarrow> (invs and valid_untyped_inv ui and ct_active and ct_active and valid_sched and valid_idle) s proof (prove)
goal (3 subgoals):
 1. \<And>P x. \<lbrace>\<lambda>s. x (ready_queues s) (cur_domain s)\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_ a. x (ready_queues a) (cur_domain a)\<rbrace>
 2. \<And>P Pa. \<lbrace>\<lambda>s. Pa (P (scheduler_action s))\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_ s. Pa (P (scheduler_action s))\<rbrace>
 3. \<And>s. (invs and valid_untyped_inv ui and ct_active and valid_sched and valid_idle) s \<Longrightarrow> (invs and valid_untyped_inv ui and ct_active and ct_active and valid_sched and valid_idle) s proof (prove)
goal (4 subgoals):
 1. \<And>P x xa. \<lbrace>\<lambda>s. xa (cur_domain s)\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_ a. xa (cur_domain a)\<rbrace>
 2. \<And>P x Pa. \<lbrace>\<lambda>s. Pa (x (ready_queues s))\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_ s. Pa (x (ready_queues s))\<rbrace>
 3. \<And>P Pa. \<lbrace>\<lambda>s. Pa (P (scheduler_action s))\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_ s. Pa (P (scheduler_action s))\<rbrace>
 4. \<And>s. (invs and valid_untyped_inv ui and ct_active and valid_sched and valid_idle) s \<Longrightarrow> (invs and valid_untyped_inv ui and ct_active and ct_active and valid_sched and valid_idle) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and valid_untyped_inv ui and ct_active and valid_sched and valid_idle) s \<Longrightarrow> (invs and valid_untyped_inv ui and ct_active and ct_active and valid_sched and valid_idle) s proof (prove)
goal:
No subgoals!