theory Tcb_AC

lemma set_priority_pas_refined[wp]:
  "\<lbrace>pas_refined aag\<rbrace>
   set_priority tptr prio
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: set_priority_def thread_set_priority_def
                   ethread_set_def set_eobject_def get_etcb_def
         | wp hoare_vcg_imp_lift')+ apply (simp add: tcb_sched_action_def | wp)+ apply (clarsimp simp: etcb_at_def pas_refined_def tcb_domain_map_wellformed_aux_def
                 split: option.splits) apply (erule_tac x="(a, b)" in ballE) apply simp apply (erule domains_of_state_aux.cases) apply (force intro: domtcbs split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> set_priority tptr prio \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q'29\<rbrace> tcb_sched_action tcb_sched_dequeue tptr \<lbrace>\<lambda>rv s. pas_refined aag (ekheap_update (\<lambda>_ a. if a = tptr then Some (the (ekheap s tptr)\<lparr>tcb_priority := prio\<rparr>) else ekheap s a) s)\<rbrace>
 2. \<And>s. pas_refined aag s \<Longrightarrow> \<not> (\<nexists>y. ekheap s tptr = Some y) \<longrightarrow> ?Q'29 s proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<Longrightarrow> (\<exists>y. ekheap s tptr = Some y) \<longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. pas_refined aag (trans_state (\<lambda>e. e\<lparr>ready_queues_internal := \<lambda>t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_dequeue tptr (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p, ekheap_internal := \<lambda>a. if a = tptr then Some (the (ekheap s tptr)\<lparr>tcb_priority := prio\<rparr>) else ekheap s a\<rparr>) s)) tptr s) tptr s proof (prove)
goal (1 subgoal):
 1. \<And>s x2 a b. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; \<forall>x\<in>domains_of_state s. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ekheap s tptr = Some x2; (a, b) \<in> domains_of_state_aux (\<lambda>a. if a = tptr then Some (x2\<lparr>tcb_priority := prio\<rparr>) else ekheap s a)\<rbrakk> \<Longrightarrow> pasObjectAbs aag a \<in> pasDomainAbs aag b proof (prove)
goal (2 subgoals):
 1. \<And>s x2 a b. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ekheap s tptr = Some x2; (a, b) \<in> domains_of_state_aux (\<lambda>a. if a = tptr then Some (x2\<lparr>tcb_priority := prio\<rparr>) else ekheap s a); case (a, b) of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> pasObjectAbs aag a \<in> pasDomainAbs aag b
 2. \<And>s x2 a b. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ekheap s tptr = Some x2; (a, b) \<in> domains_of_state_aux (\<lambda>a. if a = tptr then Some (x2\<lparr>tcb_priority := prio\<rparr>) else ekheap s a); (a, b) \<notin> domains_of_state s\<rbrakk> \<Longrightarrow> pasObjectAbs aag a \<in> pasDomainAbs aag b proof (prove)
goal (1 subgoal):
 1. \<And>s x2 a b. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ekheap s tptr = Some x2; (a, b) \<in> domains_of_state_aux (\<lambda>a. if a = tptr then Some (x2\<lparr>tcb_priority := prio\<rparr>) else ekheap s a); (a, b) \<notin> domains_of_state s\<rbrakk> \<Longrightarrow> pasObjectAbs aag a \<in> pasDomainAbs aag b proof (prove)
goal (1 subgoal):
 1. \<And>s x2 a b ptr etcb d. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ekheap s tptr = Some x2; (a, b) \<notin> domains_of_state s; a = ptr; b = d; (if ptr = tptr then Some (x2\<lparr>tcb_priority := prio\<rparr>) else ekheap s ptr) = Some etcb; d = tcb_domain etcb\<rbrakk> \<Longrightarrow> pasObjectAbs aag a \<in> pasDomainAbs aag b proof (prove)
goal:
No subgoals!