kings-crown/FVELER_Isabelle huggingface dataset:
theory Corres_C

lemma ccorres_gen_asm_state:
  assumes rl: "\<And>s. P s \<Longrightarrow> ccorres_underlying srel Ga r xf arrel axf G G' hs a c"
  shows "ccorres_underlying srel Ga r xf arrel axf (G and P) G' hs a c" proof (rule ccorres_guard_imp2) show "ccorres_underlying srel Ga r xf arrel axf (G and (\<lambda>_. \<exists>s. P s)) G' hs a c" apply (rule ccorres_gen_asm) apply (erule exE) apply (erule rl) done next fix s s' assume "(s, s') \<in> srel" and "(G and P) s" and "s' \<in> G'" thus "(G and (\<lambda>_. \<exists>s. P s)) s \<and> s' \<in> G'" by fastforce qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying srel Ga r xf arrel axf (G and P) G' hs a c proof (state)
goal (2 subgoals):
 1. ccorres_underlying srel Ga r xf arrel axf ?Q ?Q' hs a c
 2. \<And>s s'. \<lbrakk>(s, s') \<in> srel; (G and P) s; s' \<in> G'\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (1 subgoal):
 1. ccorres_underlying srel Ga r xf arrel axf (G and (\<lambda>_. \<exists>s. P s)) G' hs a c proof (prove)
goal (1 subgoal):
 1. \<exists>s. P s \<Longrightarrow> ccorres_underlying srel Ga r xf arrel axf G G' hs a c proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> ccorres_underlying srel Ga r xf arrel axf G G' hs a c proof (prove)
goal:
No subgoals! proof (state)
this:
ccorres_underlying srel Ga r xf arrel axf (G and (\<lambda>_. \<exists>s. P s)) G' hs a c

goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> srel; (G and P) s; s' \<in> G'\<rbrakk> \<Longrightarrow> (G and (\<lambda>_. \<exists>s. P s)) s \<and> s' \<in> G' proof (state)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> srel; (G and P) s; s' \<in> G'\<rbrakk> \<Longrightarrow> (G and (\<lambda>_. \<exists>s. P s)) s \<and> s' \<in> G' proof (state)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> srel; (G and P) s; s' \<in> G'\<rbrakk> \<Longrightarrow> (G and (\<lambda>_. \<exists>s. P s)) s \<and> s' \<in> G' proof (state)
this:
(s, s') \<in> srel
(G and P) s
s' \<in> G'

goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> srel; (G and P) s; s' \<in> G'\<rbrakk> \<Longrightarrow> (G and (\<lambda>_. \<exists>s. P s)) s \<and> s' \<in> G' proof (prove)
using this:
(s, s') \<in> srel
(G and P) s
s' \<in> G'

goal (1 subgoal):
 1. (G and (\<lambda>_. \<exists>s. P s)) s \<and> s' \<in> G' proof (state)
this:
(G and (\<lambda>_. \<exists>s. P s)) s \<and> s' \<in> G'

goal:
No subgoals!
theory Corres_C

lemma wfhandlers_skip:
  "wfhandlers (SKIP # hs)" unfolding wfhandlers_def apply (intro allI impI) apply (erule conjE) apply (erule exec_handlers.cases) apply (auto elim: exec_Normal_elim_cases) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wfhandlers (SKIP # hs) proof (prove)
goal (1 subgoal):
 1. \<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s proof (prove)
goal (1 subgoal):
 1. \<And>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,s\<rangle> \<Rightarrow> (n, t) \<Longrightarrow> t = Normal s proof (prove)
goal (1 subgoal):
 1. \<And>\<Gamma> s t n. \<lbrakk>global_exn_var_' s = Return; \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,s\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> t = Normal s proof (prove)
goal (3 subgoals):
 1. \<And>\<Gamma> s t n h sa z hsa na ta. \<lbrakk>global_exn_var_' s = Return; s = sa; SKIP # hs = h # hsa; n = na; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (na, ta)\<rbrakk> \<Longrightarrow> t = Normal s
 2. \<And>\<Gamma> s t n h sa ta hsa. \<lbrakk>global_exn_var_' s = Return; s = sa; SKIP # hs = h # hsa; n = length hsa; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> t = Normal s
 3. \<And>\<Gamma> s t n sa. \<lbrakk>global_exn_var_' s = Return; s = sa; SKIP # hs = []; n = 0; t = Abrupt sa\<rbrakk> \<Longrightarrow> t = Normal s proof (prove)
goal:
No subgoals!
theory Corres_C

lemma wfhandlersD:
  "\<lbrakk>wfhandlers hs; \<Gamma> \<turnstile>\<^sub>h \<langle>hs, s\<rangle> \<Rightarrow> (n, t); global_exn_var_' s = Return\<rbrakk> \<Longrightarrow> t = Normal s" unfolding wfhandlers_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wfhandlers hs; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t); global_exn_var_' s = Return\<rbrakk> \<Longrightarrow> t = Normal s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t); global_exn_var_' s = Return\<rbrakk> \<Longrightarrow> t = Normal s
theory Corres_C

lemma exflag_liftxf [simp]:
  "exflag (liftxf es sf vf xf s) = sf (xf s)" unfolding liftxf_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. exflag (liftxf es sf vf xf s) = sf (xf s) proof (prove)
goal (1 subgoal):
 1. exflag \<lparr>exflag = sf (xf s), exstate = es s, exvalue = vf (xf s)\<rparr> = sf (xf s)
theory Corres_C

lemma exstate_liftxf [simp]:
  "exstate (liftxf es sf vf xf s) = es s" unfolding liftxf_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. exstate (liftxf es sf vf xf s) = es s proof (prove)
goal (1 subgoal):
 1. exstate \<lparr>exflag = sf (xf s), exstate = es s, exvalue = vf (xf s)\<rparr> = es s
theory Corres_C

lemma exvalue_liftxf [simp]:
  "exvalue (liftxf es sf vf xf s) = vf (xf s)" unfolding liftxf_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. exvalue (liftxf es sf vf xf s) = vf (xf s) proof (prove)
goal (1 subgoal):
 1. exvalue \<lparr>exflag = sf (xf s), exstate = es s, exvalue = vf (xf s)\<rparr> = vf (xf s)
theory Corres_C

lemma xfdc_equal[simp]:
  "xfdc t = xfdc s" unfolding xfdc_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xfdc t = xfdc s proof (prove)
goal (1 subgoal):
 1. 0 = 0
theory Corres_C

lemma ccorres_call_record:
  assumes  cul: "ccorres_underlying rf_sr \<Gamma> r xf'' r xf'' A C' [] a (Call f)"
  and      ggl: "\<And>f s. globals (xfu' f s) = globals s"
  and    xfxfu: "\<And>v s. xf' (xfu' (\<lambda>_. v) s) = v"
  and  xfrxfru: "\<And>v s. xfr (xfru (\<lambda>_. v) s) = v"
  and      igl: "\<And>s. globals (i s) = globals s"
  shows "ccorres_underlying rf_sr \<Gamma> r (xfr \<circ> xf') arrel axf
           A {s. i s \<in> C'} hs a (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>)
        (\<lambda>_ t. Basic (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv))))" apply (rule ccorres_call) apply (rule cul) apply (rule ggl) apply (simp add: xfrxfru xfxfu) apply (rule igl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r (xfr \<circ> xf') arrel axf A {s. i s \<in> C'} hs a (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>_ t. Basic (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv)))) proof (prove)
goal (4 subgoals):
 1. ccorres r ?xf'' A C' [] a (Call f)
 2. \<And>_ t s. globals (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) s) = globals s
 3. \<And>a s t. (xfr \<circ> xf') (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) (s\<lparr>globals := globals t\<rparr>)) = ?xf'' t
 4. \<And>s. globals (i s) = globals s proof (prove)
goal (3 subgoals):
 1. \<And>_ t s. globals (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) s) = globals s
 2. \<And>a s t. (xfr \<circ> xf') (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) (s\<lparr>globals := globals t\<rparr>)) = xf'' t
 3. \<And>s. globals (i s) = globals s proof (prove)
goal (2 subgoals):
 1. \<And>a s t. (xfr \<circ> xf') (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) (s\<lparr>globals := globals t\<rparr>)) = xf'' t
 2. \<And>s. globals (i s) = globals s proof (prove)
goal (1 subgoal):
 1. \<And>s. globals (i s) = globals s proof (prove)
goal:
No subgoals!
theory Corres_C

lemma errlookup_fault_errstate [simp]:
  "errlookup_fault (errstate s) = lookup_fault_lift (current_lookup_fault_' (globals s))" unfolding errstate_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. errlookup_fault (errstate s) = lookup_fault_lift (current_lookup_fault_' (globals s)) proof (prove)
goal (1 subgoal):
 1. errlookup_fault \<lparr>errfault = seL4_Fault_lift (current_fault_' (globals s)), errlookup_fault = lookup_fault_lift (current_lookup_fault_' (globals s)), errsyscall = current_syscall_error_' (globals s)\<rparr> = lookup_fault_lift (current_lookup_fault_' (globals s))
theory Corres_C

lemma errfault_errstate [simp]:
  "errfault (errstate s) = seL4_Fault_lift (current_fault_' (globals s))" unfolding errstate_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. errfault (errstate s) = seL4_Fault_lift (current_fault_' (globals s)) proof (prove)
goal (1 subgoal):
 1. errfault \<lparr>errfault = seL4_Fault_lift (current_fault_' (globals s)), errlookup_fault = lookup_fault_lift (current_lookup_fault_' (globals s)), errsyscall = current_syscall_error_' (globals s)\<rparr> = seL4_Fault_lift (current_fault_' (globals s))
theory Corres_C

lemma errsyscall_errstate [simp]:
  "errsyscall (errstate s) = (current_syscall_error_' (globals s))" unfolding errstate_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. errsyscall (errstate s) = current_syscall_error_' (globals s) proof (prove)
goal (1 subgoal):
 1. errsyscall \<lparr>errfault = seL4_Fault_lift (current_fault_' (globals s)), errlookup_fault = lookup_fault_lift (current_lookup_fault_' (globals s)), errsyscall = current_syscall_error_' (globals s)\<rparr> = current_syscall_error_' (globals s)
theory Corres_C

lemma ccorres_split_nothrow_call_record_novcg:
  assumes ac: "ccorres r' xf'' P P' [] a (Call f)"
  and   ceqv: "\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv')"
  and     bd: "\<And>rv rv'. r' rv rv' \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' (xfru (\<lambda>_. rv') oldv))"
  and      ggl: "\<And>f s. globals (xfu' f s) = globals s"
  and    xfxfu: "\<And>v s. xf' (xfu' (\<lambda>_. v) s) = v"
  and  xfrxfru: "\<And>v s. xfr (xfru (\<lambda>_. v) s) = v"
  and      igl: "\<And>s. globals (i s) = globals s"
  and  valid: "\<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>"
  and  novcg: "guard_is_UNIV r' (xfr \<circ> xf') Q'"
  \<comment> \<open>This might cause problems \<dots> has to be preserved across c in vcg case, but we can't do that\<close>
  and xfoldv: "\<And>s. xf' s = xfru (\<lambda>_. (xfr \<circ> xf') s) oldv"
  shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf (P and R) ({s. i s \<in> P'}) hs (a >>= (\<lambda>rv. b rv)) (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>)
                (\<lambda>_ t. Basic (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv))) ;; d)" using ac ggl xfxfu xfrxfru igl ceqv apply (rule  ccorres_split_nothrow_record_novcg [OF ccorres_call_record]) apply (erule bd) apply (rule valid) apply (rule novcg) apply (rule xfoldv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (P and R) {s. i s \<in> P'} hs (a >>= b) (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>_ t. Basic (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv)));;
d) proof (prove)
using this:
ccorres r' xf'' P P' [] a (Call f)
globals (xfu' ?f1 ?s1) = globals ?s1
xf' (xfu' (\<lambda>_. ?v1) ?s1) = ?v1
xfr (xfru (\<lambda>_. ?v1) ?s1) = ?v1
globals (i ?s1) = globals ?s1
ceqv \<Gamma> xf' ?rv'1 ?t1 ?t'1 d (d' ?rv'1)

goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (P and R) {s. i s \<in> P'} hs (a >>= b) (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>_ t. Basic (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv)));;
d) proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. r' rv rv' \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf (?Q rv) (?Q' rv rv') hs (b rv) (d' (?xfru (\<lambda>_. rv') ?oldv))
 2. \<lbrace>R\<rbrace> a \<lbrace>?Q\<rbrace>
 3. guard_is_UNIV r' (xfr \<circ> xf') ?Q'
 4. \<And>s. xf' s = ?xfru (\<lambda>_. (xfr \<circ> xf') s) ?oldv proof (prove)
goal (3 subgoals):
 1. \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>
 2. guard_is_UNIV r' (xfr \<circ> xf') Q'
 3. \<And>s. xf' s = xfru (\<lambda>_. (xfr \<circ> xf') s) oldv proof (prove)
goal (2 subgoals):
 1. guard_is_UNIV r' (xfr \<circ> xf') Q'
 2. \<And>s. xf' s = xfru (\<lambda>_. (xfr \<circ> xf') s) oldv proof (prove)
goal (1 subgoal):
 1. \<And>s. xf' s = xfru (\<lambda>_. (xfr \<circ> xf') s) oldv proof (prove)
goal:
No subgoals!
theory Corres_C

lemma ccorres_return_C:
  assumes xf1: "\<And>s f. xf (global_exn_var_'_update f (xfu (\<lambda>_. v s) s)) = v s"
  and     xfu: "\<And>s f. globals (xfu f s) = globals s"
  and     wfh: "wfhandlers hs"
  shows "ccorres_underlying rf_sr \<Gamma> r rvxf arrel xf \<top> {s. arrel rv (v s)}
               hs (return rv) (return_C xfu v)" apply (rule ccorres_guard_imp2, rule ccorres_return_C') apply (simp add: xf1) apply (rule wfh) apply (simp add: xfu rf_sr_def cong: cstate_relation_only_t_hrs) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r rvxf arrel xf (\<lambda>_. True) {s. arrel rv (v s)} hs (return rv) (return_C xfu v) proof (prove)
goal (4 subgoals):
 1. \<And>s. xf (xfu (\<lambda>_. v s) s\<lparr>global_exn_var_' := Return\<rparr>) = v s
 2. wfhandlers hs
 3. \<And>s s'. (s, s') \<in> rf_sr \<Longrightarrow> (s, xfu (\<lambda>_. v s') s'\<lparr>global_exn_var_' := Return\<rparr>) \<in> rf_sr
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. arrel rv (v s)}\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. arrel rv (v s)} proof (prove)
goal (3 subgoals):
 1. wfhandlers hs
 2. \<And>s s'. (s, s') \<in> rf_sr \<Longrightarrow> (s, xfu (\<lambda>_. v s') s'\<lparr>global_exn_var_' := Return\<rparr>) \<in> rf_sr
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. arrel rv (v s)}\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. arrel rv (v s)} proof (prove)
goal (2 subgoals):
 1. \<And>s s'. (s, s') \<in> rf_sr \<Longrightarrow> (s, xfu (\<lambda>_. v s') s'\<lparr>global_exn_var_' := Return\<rparr>) \<in> rf_sr
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. arrel rv (v s)}\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. arrel rv (v s)} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. arrel rv (v s)}\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. arrel rv (v s)} proof (prove)
goal:
No subgoals!
theory Corres_C

lemma ccorres_return_CE:
  assumes xf1: "\<And>s f. xf (global_exn_var_'_update f (xfu (\<lambda>_. v s) s)) = v s"
  and     xfu: "\<And>s f. globals (xfu f s) = globals s"
  and     wfh: "wfhandlers hs"
  shows "ccorres_underlying rf_sr \<Gamma> rvr rxf (f \<currency> r) (liftxf es sf vf xf)
  \<top> {s. sf (v s) = scast EXCEPTION_NONE \<and> r rv (vf (v s))} hs
  (returnOk rv) (return_C xfu v)" apply (rule ccorres_guard_imp2, rule ccorres_return_CE') apply (simp add: xf1) apply (rule wfh) apply (simp add: xfu rf_sr_def cong: cstate_relation_only_t_hrs) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> rvr rxf (f \<currency> r) (liftxf es sf vf xf) (\<lambda>_. True) {s. sf (v s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> r rv (vf (v s))} hs (returnOk rv) (return_C xfu v) proof (prove)
goal (4 subgoals):
 1. \<And>s. xf (xfu (\<lambda>_. v s) s\<lparr>global_exn_var_' := Return\<rparr>) = v s
 2. wfhandlers hs
 3. \<And>s s'. (s, s') \<in> rf_sr \<Longrightarrow> (s, xfu (\<lambda>_. v s') s'\<lparr>global_exn_var_' := Return\<rparr>) \<in> rf_sr
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. sf (v s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> r rv (vf (v s))}\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. sf (v s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> r rv (vf (v s))} proof (prove)
goal (3 subgoals):
 1. wfhandlers hs
 2. \<And>s s'. (s, s') \<in> rf_sr \<Longrightarrow> (s, xfu (\<lambda>_. v s') s'\<lparr>global_exn_var_' := Return\<rparr>) \<in> rf_sr
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. sf (v s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> r rv (vf (v s))}\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. sf (v s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> r rv (vf (v s))} proof (prove)
goal (2 subgoals):
 1. \<And>s s'. (s, s') \<in> rf_sr \<Longrightarrow> (s, xfu (\<lambda>_. v s') s'\<lparr>global_exn_var_' := Return\<rparr>) \<in> rf_sr
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. sf (v s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> r rv (vf (v s))}\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. sf (v s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> r rv (vf (v s))} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. sf (v s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> r rv (vf (v s))}\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. sf (v s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> r rv (vf (v s))} proof (prove)
goal:
No subgoals!
theory Corres_C

lemma ccorres_trim_redundant_throw:
  "\<lbrakk>ccorres_underlying rf_sr \<Gamma> arrel axf arrel axf G G' (SKIP # hs) a c;
          \<And>s f. axf (global_exn_var_'_update f s) = axf s \<rbrakk>
  \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' (SKIP # hs)
          a (c;; Basic (global_exn_var_'_update (\<lambda>_. Return));; THROW)" apply - apply (rule ccorres_trim_redundant_throw') apply simp apply simp apply (simp add: rf_sr_upd_safe) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres arrel axf G G' (SKIP # hs) a c; \<And>s f. axf (global_exn_var_'_update f s) = axf s\<rbrakk> \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' (SKIP # hs) a (c;;
\<acute>global_exn_var :== Return;;
THROW) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres arrel axf G G' (SKIP # hs) a c; \<And>s f. axf (global_exn_var_'_update f s) = axf s\<rbrakk> \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' (SKIP # hs) a (c;;
\<acute>global_exn_var :== Return;;
THROW) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ccorres arrel axf G G' (SKIP # hs) a c; \<And>s f. axf (global_exn_var_'_update f s) = axf s\<rbrakk> \<Longrightarrow> ccorres arrel axf G G' (SKIP # hs) a c
 2. \<And>s. \<lbrakk>ccorres arrel axf G G' (SKIP # hs) a c; \<And>s f. axf (global_exn_var_'_update f s) = axf s\<rbrakk> \<Longrightarrow> axf (s\<lparr>global_exn_var_' := Return\<rparr>) = axf s
 3. \<And>t t'. \<lbrakk>ccorres arrel axf G G' (SKIP # hs) a c; \<And>s f. axf (global_exn_var_'_update f s) = axf s; (t, t') \<in> rf_sr\<rbrakk> \<Longrightarrow> (t, t'\<lparr>global_exn_var_' := Return\<rparr>) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>ccorres arrel axf G G' (SKIP # hs) a c; \<And>s f. axf (global_exn_var_'_update f s) = axf s\<rbrakk> \<Longrightarrow> axf (s\<lparr>global_exn_var_' := Return\<rparr>) = axf s
 2. \<And>t t'. \<lbrakk>ccorres arrel axf G G' (SKIP # hs) a c; \<And>s f. axf (global_exn_var_'_update f s) = axf s; (t, t') \<in> rf_sr\<rbrakk> \<Longrightarrow> (t, t'\<lparr>global_exn_var_' := Return\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>t t'. \<lbrakk>ccorres arrel axf G G' (SKIP # hs) a c; \<And>s f. axf (global_exn_var_'_update f s) = axf s; (t, t') \<in> rf_sr\<rbrakk> \<Longrightarrow> (t, t'\<lparr>global_exn_var_' := Return\<rparr>) \<in> rf_sr proof (prove)
goal:
No subgoals!
theory Corres_C

lemma fd_cons_update_accessD:
  "\<lbrakk> fd_cons_update_access d n; length bs = n \<rbrakk> \<Longrightarrow> field_update d (field_access d v bs) v = v" unfolding fd_cons_update_access_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fd_cons_update_access d n; length bs = n\<rbrakk> \<Longrightarrow> field_update d (field_access d v bs) v = v proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>v bs. length bs = n \<longrightarrow> field_update d (field_access d v bs) v = v; length bs = n\<rbrakk> \<Longrightarrow> field_update d (field_access d v bs) v = v
theory Corres_C

lemma cte_C_cap_C_tcb_C':
  fixes val :: "cap_C" and ptr :: "cte_C ptr"
  assumes cl: "clift hp ptr = Some z"
  shows "(clift (hrs_mem_update (heap_update (Ptr &(ptr\<rightarrow>[''cap_C''])) val) hp)) =
  (clift hp :: tcb_C typ_heap)" using cl by (simp add: typ_heap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. clift (hrs_mem_update (heap_update (cap_Ptr &(ptr\<rightarrow>[''cap_C''])) val) hp) = clift hp proof (prove)
using this:
clift hp ptr = Some z

goal (1 subgoal):
 1. clift (hrs_mem_update (heap_update (cap_Ptr &(ptr\<rightarrow>[''cap_C''])) val) hp) = clift hp
theory Corres_C

lemma cte_C_cap_C_update:
  fixes val :: "cap_C" and ptr :: "cte_C ptr"
  assumes  cl: "clift hp ptr = Some z"
  shows "(clift (hrs_mem_update (heap_update (Ptr &(ptr\<rightarrow>[''cap_C''])) val) hp)) =
         (clift hp)(ptr \<mapsto> cte_C.cap_C_update (\<lambda>_. val) z)" using cl by (simp add: clift_field_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. clift (hrs_mem_update (heap_update (cap_Ptr &(ptr\<rightarrow>[''cap_C''])) val) hp) = (clift hp)(ptr \<mapsto> cte_C.cap_C_update (\<lambda>_. val) z) proof (prove)
using this:
clift hp ptr = Some z

goal (1 subgoal):
 1. clift (hrs_mem_update (heap_update (cap_Ptr &(ptr\<rightarrow>[''cap_C''])) val) hp) = (clift hp)(ptr \<mapsto> cte_C.cap_C_update (\<lambda>_. val) z)
theory Corres_C

lemma rf_sr_globals_exn_var:
  "((s, global_exn_var_'_update f s') \<in> rf_sr)
       = ((s, s') \<in> rf_sr)" by (rule rf_sr_upd, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((s, global_exn_var_'_update f s') \<in> rf_sr) = ((s, s') \<in> rf_sr)