theory SR_lemmas_C

lemma tcb_at_h_t_valid:
  "\<lbrakk> tcb_at' thread s; (s, s') \<in> rf_sr \<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread" apply (drule cmap_relation_tcb) apply (drule map_to_tcbs_from_tcb_at) apply (clarsimp simp add: cmap_relation_def) apply (drule (1) bspec [OF _ domI]) apply (clarsimp simp add: dom_def tcb_ptr_to_ctcb_ptr_def image_def) apply (drule equalityD1) apply (drule subsetD) apply simp apply (rule exI [where x = thread]) apply simp apply (clarsimp simp: typ_heap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_at' thread s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_at' thread s; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; map_to_tcbs (ksPSpace s) thread \<noteq> None\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>map_to_tcbs (ksPSpace s) thread = Some y; tcb_ptr_to_ctcb_ptr ` dom (map_to_tcbs (ksPSpace s)) = dom (cslift s'); \<forall>x\<in>dom (map_to_tcbs (ksPSpace s)). ctcb_relation (the (map_to_tcbs (ksPSpace s) x)) (the (cslift s' (tcb_ptr_to_ctcb_ptr x)))\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>map_to_tcbs (ksPSpace s) thread = Some y; tcb_ptr_to_ctcb_ptr ` dom (map_to_tcbs (ksPSpace s)) = dom (cslift s'); ctcb_relation (the (map_to_tcbs (ksPSpace s) thread)) (the (cslift s' (tcb_ptr_to_ctcb_ptr thread)))\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>map_to_tcbs (ksPSpace s) thread = Some y; {y. \<exists>x. (\<exists>y. map_to_tcbs (ksPSpace s) x = Some y) \<and> y = tcb_Ptr (x + ctcb_offset)} = {a. \<exists>y. cslift s' a = Some y}; ctcb_relation y (the (cslift s' (tcb_Ptr (thread + ctcb_offset))))\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_Ptr (thread + ctcb_offset) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>map_to_tcbs (ksPSpace s) thread = Some y; ctcb_relation y (the (cslift s' (tcb_Ptr (thread + ctcb_offset)))); {y. \<exists>x. (\<exists>y. map_to_tcbs (ksPSpace s) x = Some y) \<and> y = tcb_Ptr (x + ctcb_offset)} \<subseteq> {a. \<exists>y. cslift s' a = Some y}\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_Ptr (thread + ctcb_offset) proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>map_to_tcbs (ksPSpace s) thread = Some y; ctcb_relation y (the (cslift s' (tcb_Ptr (thread + ctcb_offset))))\<rbrakk> \<Longrightarrow> ?c11 y \<in> {y. \<exists>x. (\<exists>y. map_to_tcbs (ksPSpace s) x = Some y) \<and> y = tcb_Ptr (x + ctcb_offset)}
 2. \<And>y. \<lbrakk>map_to_tcbs (ksPSpace s) thread = Some y; ctcb_relation y (the (cslift s' (tcb_Ptr (thread + ctcb_offset)))); ?c11 y \<in> {a. \<exists>y. cslift s' a = Some y}\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_Ptr (thread + ctcb_offset) proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>map_to_tcbs (ksPSpace s) thread = Some y; ctcb_relation y (the (cslift s' (tcb_Ptr (thread + ctcb_offset))))\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>y. map_to_tcbs (ksPSpace s) x = Some y) \<and> ?c11 y = tcb_Ptr (x + ctcb_offset)
 2. \<And>y. \<lbrakk>map_to_tcbs (ksPSpace s) thread = Some y; ctcb_relation y (the (cslift s' (tcb_Ptr (thread + ctcb_offset)))); ?c11 y \<in> {a. \<exists>y. cslift s' a = Some y}\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_Ptr (thread + ctcb_offset) proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>map_to_tcbs (ksPSpace s) thread = Some y; ctcb_relation y (the (cslift s' (tcb_Ptr (thread + ctcb_offset))))\<rbrakk> \<Longrightarrow> (\<exists>y. map_to_tcbs (ksPSpace s) thread = Some y) \<and> ?c11 y = tcb_Ptr (thread + ctcb_offset)
 2. \<And>y. \<lbrakk>map_to_tcbs (ksPSpace s) thread = Some y; ctcb_relation y (the (cslift s' (tcb_Ptr (thread + ctcb_offset)))); ?c11 y \<in> {a. \<exists>y. cslift s' a = Some y}\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_Ptr (thread + ctcb_offset) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>map_to_tcbs (ksPSpace s) thread = Some y; ctcb_relation y (the (cslift s' (tcb_Ptr (thread + ctcb_offset)))); tcb_Ptr (thread + ctcb_offset) \<in> {a. \<exists>y. cslift s' a = Some y}\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_Ptr (thread + ctcb_offset) proof (prove)
goal:
No subgoals!