theory Syscall_AC

lemma ethread_set_time_slice_pas_refined[wp]:
  "ethread_set (tcb_time_slice_update f) thread \<lbrace>pas_refined aag\<rbrace>" apply (simp add: ethread_set_def set_eobject_def | wp)+ apply (clarsimp simp: pas_refined_def tcb_domain_map_wellformed_aux_def) apply (erule_tac x="(a, b)" in ballE) apply force apply (erule notE) apply (erule domains_of_state_aux.cases, simp add: get_etcb_def split: if_split_asm) apply (force intro: domtcbs)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> ethread_set (tcb_time_slice_update f) thread \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<Longrightarrow> (\<exists>y. get_etcb thread s = Some y) \<longrightarrow> pas_refined aag (ekheap_update (\<lambda>_ a. if a = thread then Some (tcb_time_slice_update f (the (get_etcb thread s))) else ekheap s a) s) proof (prove)
goal (1 subgoal):
 1. \<And>s a b y. \<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; (a, b) \<in> domains_of_state_aux (\<lambda>a. if a = thread then Some (tcb_time_slice_update f y) else ekheap s a); get_etcb thread s = Some y\<rbrakk> \<Longrightarrow> pasObjectAbs aag a \<in> pasDomainAbs aag b proof (prove)
goal (2 subgoals):
 1. \<And>s a b y. \<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; (a, b) \<in> domains_of_state_aux (\<lambda>a. if a = thread then Some (tcb_time_slice_update f y) else ekheap s a); get_etcb thread s = Some y; 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 a b y. \<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; (a, b) \<in> domains_of_state_aux (\<lambda>a. if a = thread then Some (tcb_time_slice_update f y) else ekheap s a); get_etcb thread s = Some y; (a, b) \<notin> domains_of_state s\<rbrakk> \<Longrightarrow> pasObjectAbs aag a \<in> pasDomainAbs aag b proof (prove)
goal (1 subgoal):
 1. \<And>s a b y. \<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; (a, b) \<in> domains_of_state_aux (\<lambda>a. if a = thread then Some (tcb_time_slice_update f y) else ekheap s a); get_etcb thread s = Some y; (a, b) \<notin> domains_of_state s\<rbrakk> \<Longrightarrow> pasObjectAbs aag a \<in> pasDomainAbs aag b proof (prove)
goal (1 subgoal):
 1. \<And>s a b y. \<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; (a, b) \<in> domains_of_state_aux (\<lambda>a. if a = thread then Some (tcb_time_slice_update f y) else ekheap s a); get_etcb thread s = Some y\<rbrakk> \<Longrightarrow> (a, b) \<in> domains_of_state s proof (prove)
goal (2 subgoals):
 1. \<And>s a b y ptr etcb. \<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 thread = Some y; a = thread; b = tcb_domain etcb; ptr = thread; tcb_time_slice_update f y = etcb\<rbrakk> \<Longrightarrow> (thread, tcb_domain etcb) \<in> domains_of_state s
 2. \<And>s a b y ptr etcb. \<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 thread = Some y; a = ptr; b = tcb_domain etcb; ptr \<noteq> thread; ekheap s ptr = Some etcb\<rbrakk> \<Longrightarrow> (ptr, tcb_domain etcb) \<in> domains_of_state s proof (prove)
goal:
No subgoals!