theory IpcCancel_C

lemma threadGet_vcg_corres_P:
  assumes c: "\<And>x. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr
                       \<and> tcb_at' thread \<sigma> \<and> P \<sigma>
                       \<and> (\<forall>tcb. ko_at' tcb thread \<sigma> \<longrightarrow> (\<exists>tcb'.
                       x = f tcb \<and> cslift s (tcb_ptr_to_ctcb_ptr thread) = Some tcb'
                       \<and> ctcb_relation tcb tcb'))} c {s. (\<sigma>, s) \<in> rf_sr \<and> r x (xf s)}"
  shows "ccorres r xf P UNIV hs (threadGet f thread) c" apply (rule ccorres_add_return2) apply (rule ccorres_guard_imp2) apply (rule ccorres_pre_threadGet) apply (rule_tac P = "\<lambda>\<sigma>. \<exists>tcb. ko_at' tcb thread \<sigma> \<and> x = f tcb \<and> P \<sigma>"
    and P' = UNIV in ccorres_from_vcg) apply (simp add: return_def) apply (rule allI, rule conseqPre) apply (rule spec [OF c]) apply clarsimp apply (frule cmap_relation_tcb) apply (frule (1) cmap_relation_ko_atD) apply clarsimp apply (rule conjI) apply (erule obj_at'_weakenE) apply simp apply clarsimp apply (drule (1) ko_at_obj_congD') apply simp apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf P UNIV hs (threadGet f thread) c proof (prove)
goal (1 subgoal):
 1. ccorres r xf P UNIV hs (threadGet f thread >>= return) c proof (prove)
goal (2 subgoals):
 1. ccorres r xf ?Q2 ?Q'2 hs (threadGet f thread >>= return) c
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q2 s \<and> s' \<in> ?Q'2 proof (prove)
goal (2 subgoals):
 1. \<And>x. ccorres r xf (?P5 x) (?P'5 x) hs (return x) c
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> ?P5 (f tcb) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> ?P'5 (f tcb)} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (\<exists>tcb. ko_at' tcb thread \<sigma> \<and> x = f tcb \<and> P \<sigma>) \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} c {s. \<exists>(rv, \<sigma>')\<in>fst (return x \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> r rv (xf s)}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (\<exists>tcba. ko_at' tcba thread s \<and> f tcb = f tcba \<and> P s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (\<exists>tcb. ko_at' tcb thread \<sigma> \<and> x = f tcb \<and> P \<sigma>) \<and> (\<sigma>, s) \<in> rf_sr} c {s. (\<sigma>, s) \<in> rf_sr \<and> r x (xf s)}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (\<exists>tcba. ko_at' tcba thread s \<and> f tcb = f tcba \<and> P s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>x \<sigma>. \<Gamma>\<turnstile> (?P'11 x \<sigma>) c {s. (\<sigma>, s) \<in> rf_sr \<and> r x (xf s)}
 2. \<And>x \<sigma>. {s. (\<exists>tcb. ko_at' tcb thread \<sigma> \<and> x = f tcb \<and> P \<sigma>) \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> ?P'11 x \<sigma>
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (\<exists>tcba. ko_at' tcba thread s \<and> f tcb = f tcba \<and> P s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>x \<sigma>. {s. (\<exists>tcb. ko_at' tcb thread \<sigma> \<and> x = f tcb \<and> P \<sigma>) \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. (\<sigma>, s) \<in> rf_sr \<and> tcb_at' thread \<sigma> \<and> P \<sigma> \<and> (\<forall>tcb. ko_at' tcb thread \<sigma> \<longrightarrow> (\<exists>tcb'. x = f tcb \<and> cslift s (tcb_ptr_to_ctcb_ptr thread) = Some tcb' \<and> ctcb_relation tcb tcb'))}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (\<exists>tcba. ko_at' tcba thread s \<and> f tcb = f tcba \<and> P s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> xa tcb. \<lbrakk>(\<sigma>, xa) \<in> rf_sr; ko_at' tcb thread \<sigma>; P \<sigma>\<rbrakk> \<Longrightarrow> tcb_at' thread \<sigma> \<and> (\<forall>tcba. ko_at' tcba thread \<sigma> \<longrightarrow> f tcb = f tcba \<and> (\<exists>tcb'. cslift xa (tcb_ptr_to_ctcb_ptr thread) = Some tcb' \<and> ctcb_relation tcba tcb'))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (\<exists>tcba. ko_at' tcba thread s \<and> f tcb = f tcba \<and> P s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> xa tcb. \<lbrakk>(\<sigma>, xa) \<in> rf_sr; ko_at' tcb thread \<sigma>; P \<sigma>; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift xa) tcb_ptr_to_ctcb_ptr ctcb_relation\<rbrakk> \<Longrightarrow> tcb_at' thread \<sigma> \<and> (\<forall>tcba. ko_at' tcba thread \<sigma> \<longrightarrow> f tcb = f tcba \<and> (\<exists>tcb'. cslift xa (tcb_ptr_to_ctcb_ptr thread) = Some tcb' \<and> ctcb_relation tcba tcb'))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (\<exists>tcba. ko_at' tcba thread s \<and> f tcb = f tcba \<and> P s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> xa tcb. \<lbrakk>(\<sigma>, xa) \<in> rf_sr; ko_at' tcb thread \<sigma>; P \<sigma>; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift xa) tcb_ptr_to_ctcb_ptr ctcb_relation; \<exists>ko'. cslift xa (tcb_ptr_to_ctcb_ptr thread) = Some ko' \<and> ctcb_relation tcb ko'\<rbrakk> \<Longrightarrow> tcb_at' thread \<sigma> \<and> (\<forall>tcba. ko_at' tcba thread \<sigma> \<longrightarrow> f tcb = f tcba \<and> (\<exists>tcb'. cslift xa (tcb_ptr_to_ctcb_ptr thread) = Some tcb' \<and> ctcb_relation tcba tcb'))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (\<exists>tcba. ko_at' tcba thread s \<and> f tcb = f tcba \<and> P s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> xa tcb ko'. \<lbrakk>(\<sigma>, xa) \<in> rf_sr; ko_at' tcb thread \<sigma>; P \<sigma>; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift xa) tcb_ptr_to_ctcb_ptr ctcb_relation; cslift xa (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation tcb ko'\<rbrakk> \<Longrightarrow> tcb_at' thread \<sigma> \<and> (\<forall>tcba. ko_at' tcba thread \<sigma> \<longrightarrow> f tcb = f tcba \<and> ctcb_relation tcba ko')
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (\<exists>tcba. ko_at' tcba thread s \<and> f tcb = f tcba \<and> P s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> xa tcb ko'. \<lbrakk>(\<sigma>, xa) \<in> rf_sr; ko_at' tcb thread \<sigma>; P \<sigma>; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift xa) tcb_ptr_to_ctcb_ptr ctcb_relation; cslift xa (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation tcb ko'\<rbrakk> \<Longrightarrow> tcb_at' thread \<sigma>
 2. \<And>\<sigma> xa tcb ko'. \<lbrakk>(\<sigma>, xa) \<in> rf_sr; ko_at' tcb thread \<sigma>; P \<sigma>; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift xa) tcb_ptr_to_ctcb_ptr ctcb_relation; cslift xa (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation tcb ko'\<rbrakk> \<Longrightarrow> \<forall>tcba. ko_at' tcba thread \<sigma> \<longrightarrow> f tcb = f tcba \<and> ctcb_relation tcba ko'
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (\<exists>tcba. ko_at' tcba thread s \<and> f tcb = f tcba \<and> P s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> xa tcb ko' k. \<lbrakk>(\<sigma>, xa) \<in> rf_sr; P \<sigma>; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift xa) tcb_ptr_to_ctcb_ptr ctcb_relation; cslift xa (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation tcb ko'; k = tcb\<rbrakk> \<Longrightarrow> True
 2. \<And>\<sigma> xa tcb ko'. \<lbrakk>(\<sigma>, xa) \<in> rf_sr; ko_at' tcb thread \<sigma>; P \<sigma>; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift xa) tcb_ptr_to_ctcb_ptr ctcb_relation; cslift xa (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation tcb ko'\<rbrakk> \<Longrightarrow> \<forall>tcba. ko_at' tcba thread \<sigma> \<longrightarrow> f tcb = f tcba \<and> ctcb_relation tcba ko'
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (\<exists>tcba. ko_at' tcba thread s \<and> f tcb = f tcba \<and> P s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> xa tcb ko'. \<lbrakk>(\<sigma>, xa) \<in> rf_sr; ko_at' tcb thread \<sigma>; P \<sigma>; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift xa) tcb_ptr_to_ctcb_ptr ctcb_relation; cslift xa (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation tcb ko'\<rbrakk> \<Longrightarrow> \<forall>tcba. ko_at' tcba thread \<sigma> \<longrightarrow> f tcb = f tcba \<and> ctcb_relation tcba ko'
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (\<exists>tcba. ko_at' tcba thread s \<and> f tcb = f tcba \<and> P s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> xa tcb ko' tcba. \<lbrakk>(\<sigma>, xa) \<in> rf_sr; ko_at' tcb thread \<sigma>; P \<sigma>; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift xa) tcb_ptr_to_ctcb_ptr ctcb_relation; cslift xa (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation tcb ko'; ko_at' tcba thread \<sigma>\<rbrakk> \<Longrightarrow> f tcb = f tcba \<and> ctcb_relation tcba ko'
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (\<exists>tcba. ko_at' tcba thread s \<and> f tcb = f tcba \<and> P s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> xa tcb ko' tcba. \<lbrakk>(\<sigma>, xa) \<in> rf_sr; P \<sigma>; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift xa) tcb_ptr_to_ctcb_ptr ctcb_relation; cslift xa (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation tcb ko'; ko_at' tcba thread \<sigma>; tcb = tcba\<rbrakk> \<Longrightarrow> f tcb = f tcba \<and> ctcb_relation tcba ko'
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (\<exists>tcba. ko_at' tcba thread s \<and> f tcb = f tcba \<and> P s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (\<exists>tcba. ko_at' tcba thread s \<and> f tcb = f tcba \<and> P s)) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV} proof (prove)
goal:
No subgoals!