theory Schedule_C

lemma get_tsType_ccorres2:
  "ccorres (\<lambda>r r'. r' = thread_state_to_tsType r) ret__unsigned_' (tcb_at' thread)
           (UNIV \<inter> {s. f s = tcb_ptr_to_ctcb_ptr thread} \<inter>
            {s. cslift s (Ptr &(f s\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}) []
  (getThreadState thread) (Call thread_state_get_tsType_'proc)" unfolding getThreadState_def apply (rule ccorres_from_spec_modifies [where P=\<top>, simplified]) apply (rule thread_state_get_tsType_spec) apply (rule thread_state_get_tsType_modifies) apply simp apply (frule (1) obj_at_cslift_tcb) apply (clarsimp simp: typ_heap_simps) apply (rule bexI [rotated, OF threadGet_eq], assumption) apply simp apply (drule ctcb_relation_thread_state_to_tsType) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>r r'. r' = thread_state_to_tsType r) ret__unsigned_' (tcb_at' thread) (UNIV \<inter> {s. f s = tcb_ptr_to_ctcb_ptr thread} \<inter> {s. cslift s (PTR(thread_state_C) &(f s\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}) [] (getThreadState thread) (Call thread_state_get_tsType_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>r r'. r' = thread_state_to_tsType r) ret__unsigned_' (tcb_at' thread) (UNIV \<inter> {s. f s = tcb_ptr_to_ctcb_ptr thread} \<inter> {s. cslift s (PTR(thread_state_C) &(f s\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}) [] (threadGet tcbState thread) (Call thread_state_get_tsType_'proc) proof (prove)
goal (4 subgoals):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call thread_state_get_tsType_'proc {t. ?Q s t}
 2. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call thread_state_get_tsType_'proc {t. t may_not_modify_globals s}
 3. \<And>f s. ret__unsigned_' (globals_update f s) = ret__unsigned_' s
 4. \<And>s s' t'. \<lbrakk>tcb_at' thread s; s' \<in> UNIV \<inter> {s. f s = tcb_ptr_to_ctcb_ptr thread} \<inter> {s. cslift s (PTR(thread_state_C) &(f s\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}; (s, s') \<in> rf_sr; ?Q s' t'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (threadGet tcbState thread s). case x of (rv, t) \<Rightarrow> (t, s') \<in> rf_sr \<and> ret__unsigned_' t' = thread_state_to_tsType rv proof (prove)
goal (3 subgoals):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call thread_state_get_tsType_'proc {t. t may_not_modify_globals s}
 2. \<And>f s. ret__unsigned_' (globals_update f s) = ret__unsigned_' s
 3. \<And>s s' t'. \<lbrakk>tcb_at' thread s; s' \<in> UNIV \<inter> {s. f s = tcb_ptr_to_ctcb_ptr thread} \<inter> {s. cslift s (PTR(thread_state_C) &(f s\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}; (s, s') \<in> rf_sr; ret__unsigned_' t' = tsType_CL (thread_state_lift (thread_state_' s'))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (threadGet tcbState thread s). case x of (rv, t) \<Rightarrow> (t, s') \<in> rf_sr \<and> ret__unsigned_' t' = thread_state_to_tsType rv proof (prove)
goal (2 subgoals):
 1. \<And>f s. ret__unsigned_' (globals_update f s) = ret__unsigned_' s
 2. \<And>s s' t'. \<lbrakk>tcb_at' thread s; s' \<in> UNIV \<inter> {s. f s = tcb_ptr_to_ctcb_ptr thread} \<inter> {s. cslift s (PTR(thread_state_C) &(f s\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}; (s, s') \<in> rf_sr; ret__unsigned_' t' = tsType_CL (thread_state_lift (thread_state_' s'))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (threadGet tcbState thread s). case x of (rv, t) \<Rightarrow> (t, s') \<in> rf_sr \<and> ret__unsigned_' t' = thread_state_to_tsType rv proof (prove)
goal (1 subgoal):
 1. \<And>s s' t'. \<lbrakk>tcb_at' thread s; s' \<in> UNIV \<inter> {s. f s = tcb_ptr_to_ctcb_ptr thread} \<inter> {s. cslift s (PTR(thread_state_C) &(f s\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}; (s, s') \<in> rf_sr; ret__unsigned_' t' = tsType_CL (thread_state_lift (thread_state_' s'))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (threadGet tcbState thread s). case x of (rv, t) \<Rightarrow> (t, s') \<in> rf_sr \<and> ret__unsigned_' t' = thread_state_to_tsType rv proof (prove)
goal (1 subgoal):
 1. \<And>s s' t'. \<lbrakk>tcb_at' thread s; s' \<in> UNIV \<inter> {s. f s = tcb_ptr_to_ctcb_ptr thread} \<inter> {s. cslift s (PTR(thread_state_C) &(f s\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}; (s, s') \<in> rf_sr; ret__unsigned_' t' = tsType_CL (thread_state_lift (thread_state_' s')); \<exists>ko ko'. ko_at' ko thread s \<and> True \<and> cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ko' \<and> ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (threadGet tcbState thread s). case x of (rv, t) \<Rightarrow> (t, s') \<in> rf_sr \<and> ret__unsigned_' t' = thread_state_to_tsType rv proof (prove)
goal (1 subgoal):
 1. \<And>s s' t' ko ko'. \<lbrakk>tcb_at' thread s; (s, s') \<in> rf_sr; ret__unsigned_' t' = tsType_CL (thread_state_lift (thread_state_' s')); f s' = tcb_ptr_to_ctcb_ptr thread; tcbState_C ko' = thread_state_' s'; ko_at' ko thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (threadGet tcbState thread s). case x of (rv, t) \<Rightarrow> (t, s') \<in> rf_sr \<and> tsType_CL (thread_state_lift (thread_state_' s')) = thread_state_to_tsType rv proof (prove)
goal (1 subgoal):
 1. \<And>s s' t' ko ko'. \<lbrakk>tcb_at' thread s; (s, s') \<in> rf_sr; ret__unsigned_' t' = tsType_CL (thread_state_lift (thread_state_' s')); f s' = tcb_ptr_to_ctcb_ptr thread; tcbState_C ko' = thread_state_' s'; ko_at' ko thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> case (tcbState ko, s) of (rv, t) \<Rightarrow> (t, s') \<in> rf_sr \<and> tsType_CL (thread_state_lift (thread_state_' s')) = thread_state_to_tsType rv proof (prove)
goal (1 subgoal):
 1. \<And>s s' t' ko ko'. \<lbrakk>tcb_at' thread s; (s, s') \<in> rf_sr; ret__unsigned_' t' = tsType_CL (thread_state_lift (thread_state_' s')); f s' = tcb_ptr_to_ctcb_ptr thread; tcbState_C ko' = thread_state_' s'; ko_at' ko thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> tsType_CL (thread_state_lift (thread_state_' s')) = thread_state_to_tsType (tcbState ko) proof (prove)
goal (1 subgoal):
 1. \<And>s s' t' ko ko'. \<lbrakk>tcb_at' thread s; (s, s') \<in> rf_sr; ret__unsigned_' t' = tsType_CL (thread_state_lift (thread_state_' s')); f s' = tcb_ptr_to_ctcb_ptr thread; tcbState_C ko' = thread_state_' s'; ko_at' ko thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ko'; tsType_CL (thread_state_lift (tcbState_C ko')) = thread_state_to_tsType (tcbState ko)\<rbrakk> \<Longrightarrow> tsType_CL (thread_state_lift (thread_state_' s')) = thread_state_to_tsType (tcbState ko) proof (prove)
goal:
No subgoals!