theory ADT_IF_Refine

lemma st_tcb_at_coerce_haskell:
  "\<lbrakk> st_tcb_at P t a; (a, c) \<in> state_relation; tcb_at' t c \<rbrakk>
     \<Longrightarrow> st_tcb_at' (\<lambda>st'. \<exists>st. thread_state_relation st st' \<and> P st) t c" apply (clarsimp simp: state_relation_def pspace_relation_def
                        obj_at_def st_tcb_at'_def st_tcb_at_def) apply (drule_tac x=t in bspec) apply fastforce apply clarsimp apply (simp add: other_obj_relation_def) apply clarsimp apply (clarsimp simp: obj_at'_def projectKO_eq projectKO_tcb split: kernel_object.splits) apply (rule_tac x="tcb_state tcb" in exI) apply simp apply (simp add: tcb_relation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at P t a; (a, c) \<in> state_relation; tcb_at' t c\<rbrakk> \<Longrightarrow> st_tcb_at' (\<lambda>st'. \<exists>st. thread_state_relation st st' \<and> P st) t c proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>tcb_at' t c; pspace_dom (kheap a) = dom (ksPSpace c); kheap a t = Some (TCB tcb); \<forall>x\<in>dom (kheap a). \<forall>xa\<in>obj_relation_cuts (the (kheap a x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap a x)) (the (ksPSpace c y)); P (tcb_state tcb); ekheap_relation (ekheap a) (ksPSpace c); sched_act_relation (scheduler_action a) (ksSchedulerAction c); ready_queues_relation (ready_queues a) (ksReadyQueues c); ghost_relation (kheap a) (gsUserPages c) (gsCNodes c); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of c); cdt_list_relation (cdt_list a) (cdt a) (ctes_of c); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of c); (arch_state a, ksArchState c) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState c); cur_thread a = ksCurThread c; idle_thread a = ksIdleThread c; machine_state a = ksMachineState c; work_units_completed a = ksWorkUnitsCompleted c; domain_index a = ksDomScheduleIdx c; domain_list a = ksDomSchedule c; cur_domain a = ksCurDomain c; domain_time a = ksDomainTime c\<rbrakk> \<Longrightarrow> obj_at' ((\<lambda>st'. \<exists>st. thread_state_relation st st' \<and> P st) \<circ> tcbState) t c proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrakk>tcb_at' t c; pspace_dom (kheap a) = dom (ksPSpace c); kheap a t = Some (TCB tcb); P (tcb_state tcb); ekheap_relation (ekheap a) (ksPSpace c); sched_act_relation (scheduler_action a) (ksSchedulerAction c); ready_queues_relation (ready_queues a) (ksReadyQueues c); ghost_relation (kheap a) (gsUserPages c) (gsCNodes c); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of c); cdt_list_relation (cdt_list a) (cdt a) (ctes_of c); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of c); (arch_state a, ksArchState c) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState c); cur_thread a = ksCurThread c; idle_thread a = ksIdleThread c; machine_state a = ksMachineState c; work_units_completed a = ksWorkUnitsCompleted c; domain_index a = ksDomScheduleIdx c; domain_list a = ksDomSchedule c; cur_domain a = ksCurDomain c; domain_time a = ksDomainTime c\<rbrakk> \<Longrightarrow> t \<in> dom (kheap a)
 2. \<And>tcb. \<lbrakk>tcb_at' t c; pspace_dom (kheap a) = dom (ksPSpace c); kheap a t = Some (TCB tcb); P (tcb_state tcb); ekheap_relation (ekheap a) (ksPSpace c); sched_act_relation (scheduler_action a) (ksSchedulerAction c); ready_queues_relation (ready_queues a) (ksReadyQueues c); ghost_relation (kheap a) (gsUserPages c) (gsCNodes c); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of c); cdt_list_relation (cdt_list a) (cdt a) (ctes_of c); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of c); (arch_state a, ksArchState c) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState c); cur_thread a = ksCurThread c; idle_thread a = ksIdleThread c; machine_state a = ksMachineState c; work_units_completed a = ksWorkUnitsCompleted c; domain_index a = ksDomScheduleIdx c; domain_list a = ksDomSchedule c; cur_domain a = ksCurDomain c; domain_time a = ksDomainTime c; \<forall>x\<in>obj_relation_cuts (the (kheap a t)) t. case x of (y, P) \<Rightarrow> P (the (kheap a t)) (the (ksPSpace c y))\<rbrakk> \<Longrightarrow> obj_at' ((\<lambda>st'. \<exists>st. thread_state_relation st st' \<and> P st) \<circ> tcbState) t c proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>tcb_at' t c; pspace_dom (kheap a) = dom (ksPSpace c); kheap a t = Some (TCB tcb); P (tcb_state tcb); ekheap_relation (ekheap a) (ksPSpace c); sched_act_relation (scheduler_action a) (ksSchedulerAction c); ready_queues_relation (ready_queues a) (ksReadyQueues c); ghost_relation (kheap a) (gsUserPages c) (gsCNodes c); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of c); cdt_list_relation (cdt_list a) (cdt a) (ctes_of c); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of c); (arch_state a, ksArchState c) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState c); cur_thread a = ksCurThread c; idle_thread a = ksIdleThread c; machine_state a = ksMachineState c; work_units_completed a = ksWorkUnitsCompleted c; domain_index a = ksDomScheduleIdx c; domain_list a = ksDomSchedule c; cur_domain a = ksCurDomain c; domain_time a = ksDomainTime c; \<forall>x\<in>obj_relation_cuts (the (kheap a t)) t. case x of (y, P) \<Rightarrow> P (the (kheap a t)) (the (ksPSpace c y))\<rbrakk> \<Longrightarrow> obj_at' ((\<lambda>st'. \<exists>st. thread_state_relation st st' \<and> P st) \<circ> tcbState) t c proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>tcb_at' t c; pspace_dom (kheap a) = dom (ksPSpace c); kheap a t = Some (TCB tcb); P (tcb_state tcb); ekheap_relation (ekheap a) (ksPSpace c); sched_act_relation (scheduler_action a) (ksSchedulerAction c); ready_queues_relation (ready_queues a) (ksReadyQueues c); ghost_relation (kheap a) (gsUserPages c) (gsCNodes c); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of c); cdt_list_relation (cdt_list a) (cdt a) (ctes_of c); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of c); (arch_state a, ksArchState c) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState c); cur_thread a = ksCurThread c; idle_thread a = ksIdleThread c; machine_state a = ksMachineState c; work_units_completed a = ksWorkUnitsCompleted c; domain_index a = ksDomScheduleIdx c; domain_list a = ksDomSchedule c; cur_domain a = ksCurDomain c; domain_time a = ksDomainTime c; other_obj_relation (TCB tcb) (the (ksPSpace c t))\<rbrakk> \<Longrightarrow> obj_at' ((\<lambda>st'. \<exists>st. thread_state_relation st st' \<and> P st) \<circ> tcbState) t c proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>tcb_at' t c; pspace_dom (kheap a) = dom (ksPSpace c); kheap a t = Some (TCB tcb); P (tcb_state tcb); ekheap_relation (ekheap a) (ksPSpace c); sched_act_relation (scheduler_action a) (ksSchedulerAction c); ready_queues_relation (ready_queues a) (ksReadyQueues c); ghost_relation (kheap a) (gsUserPages c) (gsCNodes c); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of c); cdt_list_relation (cdt_list a) (cdt a) (ctes_of c); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of c); (arch_state a, ksArchState c) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState c); cur_thread a = ksCurThread c; idle_thread a = ksIdleThread c; machine_state a = ksMachineState c; work_units_completed a = ksWorkUnitsCompleted c; domain_index a = ksDomScheduleIdx c; domain_list a = ksDomSchedule c; cur_domain a = ksCurDomain c; domain_time a = ksDomainTime c; case the (ksPSpace c t) of KOTCB x \<Rightarrow> tcb_relation tcb x | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> obj_at' ((\<lambda>st'. \<exists>st. thread_state_relation st st' \<and> P st) \<circ> tcbState) t c proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>tcb_at' t c; pspace_dom (kheap a) = dom (ksPSpace c); kheap a t = Some (TCB tcb); P (tcb_state tcb); ekheap_relation (ekheap a) (ksPSpace c); sched_act_relation (scheduler_action a) (ksSchedulerAction c); ready_queues_relation (ready_queues a) (ksReadyQueues c); ghost_relation (kheap a) (gsUserPages c) (gsCNodes c); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of c); cdt_list_relation (cdt_list a) (cdt a) (ctes_of c); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of c); (arch_state a, ksArchState c) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState c); cur_thread a = ksCurThread c; idle_thread a = ksIdleThread c; machine_state a = ksMachineState c; work_units_completed a = ksWorkUnitsCompleted c; domain_index a = ksDomScheduleIdx c; domain_list a = ksDomSchedule c; cur_domain a = ksCurDomain c; domain_time a = ksDomainTime c; case the (ksPSpace c t) of KOTCB x \<Rightarrow> tcb_relation tcb x | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> obj_at' ((\<lambda>st'. \<exists>st. thread_state_relation st st' \<and> P st) \<circ> tcbState) t c proof (prove)
goal (1 subgoal):
 1. \<And>tcb x6. \<lbrakk>pspace_dom (kheap a) = dom (ksPSpace c); kheap a t = Some (TCB tcb); P (tcb_state tcb); ekheap_relation (ekheap a) (ksPSpace c); sched_act_relation (scheduler_action a) (ksSchedulerAction c); ready_queues_relation (ready_queues a) (ksReadyQueues c); ghost_relation (kheap a) (gsUserPages c) (gsCNodes c); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of c); cdt_list_relation (cdt_list a) (cdt a) (ctes_of c); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of c); (arch_state a, ksArchState c) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState c); cur_thread a = ksCurThread c; idle_thread a = ksIdleThread c; machine_state a = ksMachineState c; work_units_completed a = ksWorkUnitsCompleted c; domain_index a = ksDomScheduleIdx c; domain_list a = ksDomSchedule c; cur_domain a = ksCurDomain c; domain_time a = ksDomainTime c; ksPSpace c t = Some (KOTCB x6); is_aligned t (objBitsKO (KOTCB x6)); ps_clear t (objBitsKO (KOTCB x6)) c; tcb_relation tcb x6\<rbrakk> \<Longrightarrow> \<exists>st. thread_state_relation st (tcbState x6) \<and> P st proof (prove)
goal (1 subgoal):
 1. \<And>tcb x6. \<lbrakk>pspace_dom (kheap a) = dom (ksPSpace c); kheap a t = Some (TCB tcb); P (tcb_state tcb); ekheap_relation (ekheap a) (ksPSpace c); sched_act_relation (scheduler_action a) (ksSchedulerAction c); ready_queues_relation (ready_queues a) (ksReadyQueues c); ghost_relation (kheap a) (gsUserPages c) (gsCNodes c); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of c); cdt_list_relation (cdt_list a) (cdt a) (ctes_of c); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of c); (arch_state a, ksArchState c) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState c); cur_thread a = ksCurThread c; idle_thread a = ksIdleThread c; machine_state a = ksMachineState c; work_units_completed a = ksWorkUnitsCompleted c; domain_index a = ksDomScheduleIdx c; domain_list a = ksDomSchedule c; cur_domain a = ksCurDomain c; domain_time a = ksDomainTime c; ksPSpace c t = Some (KOTCB x6); is_aligned t (objBitsKO (KOTCB x6)); ps_clear t (objBitsKO (KOTCB x6)) c; tcb_relation tcb x6\<rbrakk> \<Longrightarrow> thread_state_relation (tcb_state tcb) (tcbState x6) \<and> P (tcb_state tcb) proof (prove)
goal (1 subgoal):
 1. \<And>tcb x6. \<lbrakk>pspace_dom (kheap a) = dom (ksPSpace c); kheap a t = Some (TCB tcb); P (tcb_state tcb); ekheap_relation (ekheap a) (ksPSpace c); sched_act_relation (scheduler_action a) (ksSchedulerAction c); ready_queues_relation (ready_queues a) (ksReadyQueues c); ghost_relation (kheap a) (gsUserPages c) (gsCNodes c); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of c); cdt_list_relation (cdt_list a) (cdt a) (ctes_of c); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of c); (arch_state a, ksArchState c) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState c); cur_thread a = ksCurThread c; idle_thread a = ksIdleThread c; machine_state a = ksMachineState c; work_units_completed a = ksWorkUnitsCompleted c; domain_index a = ksDomScheduleIdx c; domain_list a = ksDomSchedule c; cur_domain a = ksCurDomain c; domain_time a = ksDomainTime c; ksPSpace c t = Some (KOTCB x6); is_aligned t (objBitsKO (KOTCB x6)); ps_clear t (objBitsKO (KOTCB x6)) c; tcb_relation tcb x6\<rbrakk> \<Longrightarrow> thread_state_relation (tcb_state tcb) (tcbState x6) proof (prove)
goal:
No subgoals!