theory Syscall_AC

lemma valid_sched_action_switch_subject_thread:
   "\<lbrakk> scheduler_action s = switch_thread t; valid_sched_action s;
      valid_etcbs s; pas_refined aag s; pas_cur_domain aag s \<rbrakk>
      \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (tcb_domain (the (ekheap s t))) \<and>
          pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s t)))" apply (clarsimp simp: valid_sched_action_def weak_valid_sched_action_2_def
                        switch_in_cur_domain_2_def in_cur_domain_2_def valid_etcbs_def
                        etcb_at_def st_tcb_at_def obj_at_def is_etcb_at_def) apply (rule conjI) apply (force simp: pas_refined_def tcb_domain_map_wellformed_aux_def
                intro: domtcbs) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>scheduler_action s = switch_thread t; valid_sched_action s; valid_etcbs s; pas_refined aag s; pas_cur_domain aag s\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (tcb_domain (the (ekheap s t))) \<and> pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s t))) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>scheduler_action s = switch_thread t; \<forall>ptr. (\<exists>ko. kheap s ptr = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekheap s ptr = Some y); pas_refined aag s; pas_cur_domain aag s; case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_domain x = cur_domain s; kheap s t = Some (TCB tcb); runnable (tcb_state tcb)\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (tcb_domain (the (ekheap s t))) \<and> pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s t))) proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrakk>scheduler_action s = switch_thread t; \<forall>ptr. (\<exists>ko. kheap s ptr = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekheap s ptr = Some y); pas_refined aag s; pas_cur_domain aag s; case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_domain x = cur_domain s; kheap s t = Some (TCB tcb); runnable (tcb_state tcb)\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (tcb_domain (the (ekheap s t)))
 2. \<And>tcb. \<lbrakk>scheduler_action s = switch_thread t; \<forall>ptr. (\<exists>ko. kheap s ptr = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekheap s ptr = Some y); pas_refined aag s; pas_cur_domain aag s; case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_domain x = cur_domain s; kheap s t = Some (TCB tcb); runnable (tcb_state tcb)\<rbrakk> \<Longrightarrow> pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s t))) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>scheduler_action s = switch_thread t; \<forall>ptr. (\<exists>ko. kheap s ptr = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekheap s ptr = Some y); pas_refined aag s; pas_cur_domain aag s; case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_domain x = cur_domain s; kheap s t = Some (TCB tcb); runnable (tcb_state tcb)\<rbrakk> \<Longrightarrow> pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s t))) proof (prove)
goal:
No subgoals!