theory Corres_C

lemma ccorres_symb_exec_r2:
  assumes cul: "ccorres_underlying rf_sr \<Gamma> r xf arrel axf R Q' hs a d"
  and     ex:  "\<Gamma> \<turnstile> R' c Q'"
  and   pres:  "\<forall>s. \<Gamma> \<turnstile>\<^bsub>/F\<^esub> {s} c {t. t may_not_modify_globals s}"
  shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf R R' hs a (c ;; d)" apply (rule ccorres_add_return) apply (rule ccorres_guard_imp2) apply (rule ccorres_split_nothrow') apply (rule ccorres_noop_spec) apply (rule allI) apply (rule ex) apply (rule pres) apply simp apply (rule cul) apply wp apply (rule HoarePartialProps.augment_Faults [OF ex]) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf R R' hs a (c;;
d) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf R R' hs (do _ <- return ();
a
od) (c;;
d) proof (prove)
goal (2 subgoals):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf ?Q2 ?Q'2 hs (do _ <- return ();
a
od) (c;;
d)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; R s; s' \<in> R'\<rbrakk> \<Longrightarrow> ?Q2 s \<and> s' \<in> ?Q'2 proof (prove)
goal (5 subgoals):
 1. ccorres_underlying rf_sr \<Gamma> ?r'5 ?xf'5 dc axf ?P5 ?P'5 hs (return ()) c
 2. \<And>uu_. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (?Q5 uu_) (?Q'5 \<inter> {s. ?r'5 uu_ (?xf'5 s)}) hs a d
 3. \<lbrace>?R5\<rbrace> return () \<lbrace>?Q5\<rbrace>
 4. \<Gamma>\<turnstile>\<^bsub>/?F5\<^esub> ?R'5 c ?Q'5
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; R s; s' \<in> R'\<rbrakk> \<Longrightarrow> (?P5 and ?R5) s \<and> s' \<in> ?P'5 \<inter> ?R'5 proof (prove)
goal (6 subgoals):
 1. \<forall>s. \<Gamma>\<turnstile> (?P10 s) c (?R10 s),(?A10 s)
 2. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/?F10\<^esub> {s} c {t. t may_not_modify_globals s}
 3. \<And>uu_. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (?Q5 uu_) (?Q'5 \<inter> {s. dc uu_ (?xf'5 s)}) hs a d
 4. \<lbrace>?R5\<rbrace> return () \<lbrace>?Q5\<rbrace>
 5. \<Gamma>\<turnstile>\<^bsub>/?F5\<^esub> ?R'5 c ?Q'5
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; R s; s' \<in> R'\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R5) s \<and> s' \<in> {s. s \<in> ?P10 s} \<inter> ?R'5 proof (prove)
goal (6 subgoals):
 1. \<And>s. \<Gamma>\<turnstile> (?P10 s) c (?R10 s),(?A10 s)
 2. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/?F10\<^esub> {s} c {t. t may_not_modify_globals s}
 3. \<And>uu_. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (?Q5 uu_) (?Q'5 \<inter> {s. dc uu_ (?xf'5 s)}) hs a d
 4. \<lbrace>?R5\<rbrace> return () \<lbrace>?Q5\<rbrace>
 5. \<Gamma>\<turnstile>\<^bsub>/?F5\<^esub> ?R'5 c ?Q'5
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; R s; s' \<in> R'\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R5) s \<and> s' \<in> {s. s \<in> ?P10 s} \<inter> ?R'5 proof (prove)
goal (5 subgoals):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/?F10\<^esub> {s} c {t. t may_not_modify_globals s}
 2. \<And>uu_. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (?Q5 uu_) (?Q'5 \<inter> {s. dc uu_ (?xf'5 s)}) hs a d
 3. \<lbrace>?R5\<rbrace> return () \<lbrace>?Q5\<rbrace>
 4. \<Gamma>\<turnstile>\<^bsub>/?F5\<^esub> ?R'5 c ?Q'5
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; R s; s' \<in> R'\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R5) s \<and> s' \<in> {s. s \<in> R'} \<inter> ?R'5 proof (prove)
goal (4 subgoals):
 1. \<And>uu_. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (?Q5 uu_) (?Q'5 \<inter> {s. dc uu_ (?xf'5 s)}) hs a d
 2. \<lbrace>?R5\<rbrace> return () \<lbrace>?Q5\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/?F5\<^esub> ?R'5 c ?Q'5
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; R s; s' \<in> R'\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R5) s \<and> s' \<in> {s. s \<in> R'} \<inter> ?R'5 proof (prove)
goal (4 subgoals):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (?Q5 ()) ?Q'5 hs a d
 2. \<lbrace>?R5\<rbrace> return () \<lbrace>?Q5\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/?F5\<^esub> ?R'5 c ?Q'5
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; R s; s' \<in> R'\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R5) s \<and> s' \<in> {s. s \<in> R'} \<inter> ?R'5 proof (prove)
goal (3 subgoals):
 1. \<lbrace>?R5\<rbrace> return () \<lbrace>\<lambda>a. R\<rbrace>
 2. \<Gamma>\<turnstile>\<^bsub>/?F5\<^esub> ?R'5 c Q'
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; R s; s' \<in> R'\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R5) s \<and> s' \<in> {s. s \<in> R'} \<inter> ?R'5 proof (prove)
goal (2 subgoals):
 1. \<Gamma>\<turnstile>\<^bsub>/?F5\<^esub> ?R'5 c Q'
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; R s; s' \<in> R'\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and R) s \<and> s' \<in> {s. s \<in> R'} \<inter> ?R'5 proof (prove)
goal (2 subgoals):
 1. {} \<subseteq> ?F5
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; R s; s' \<in> R'\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and R) s \<and> s' \<in> {s. s \<in> R'} \<inter> R' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; R s; s' \<in> R'\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and R) s \<and> s' \<in> {s. s \<in> R'} \<inter> R' proof (prove)
goal:
No subgoals!