theory Corres_UL_C

lemma ccorres_call_getter_setter:
  assumes cul: "ccorresG sr \<Gamma> r' xf' P (i ` P') [] getter (Call f)"
  and     gsr: "\<And>x x' s t rv rv'.
                  \<lbrakk> (x, t) \<in> sr; r' rv (xf' t); (rv', x') \<in> fst (setter rv x) \<rbrakk>
                  \<Longrightarrow> (x', g s t (clean s t)) \<in> sr"
  and     res: "\<And>s t rv. r' rv (xf' t) \<Longrightarrow> r rv (xf (g s t (clean s t)))"
  and     ist: "\<And>x s. (x, s) \<in> sr \<Longrightarrow> (x, i s) \<in> sr"
  and      ef: "\<And>val. empty_fail (setter val)"
  shows "ccorresG sr \<Gamma> r xf P P' hs
           (do val \<leftarrow> getter; setter val; return val od)
           (call i f clean (\<lambda>s t. Basic (g s t)))" apply (rule ccorresI') apply (rename_tac s s' n z) apply (prop_tac "\<not> snd (getter s)") apply (clarsimp simp: bind_def) apply (erule exec_handlers.cases; clarsimp) apply (erule exec_call_Normal_elim; simp?) apply (clarsimp elim!: exec_Normal_elim_cases) apply (fastforce intro: ccorresE[OF cul ist] EHAbrupt EHEmpty elim: exec.Call) apply (erule exec_call_Normal_elim; simp?) apply (rule ccorresE[OF cul ist], simp+) apply (fastforce intro: EHOther elim: exec.Call) using ef apply (fastforce intro: gsr res
                       simp: unif_rrel_simps bind_def empty_fail_def return_def
                       elim: exec_Normal_elim_cases) apply (fastforce intro: ccorresE[OF cul ist] EHOther elim: exec.Call) apply (fastforce intro: ccorresE[OF cul ist] EHOther elim: exec.Call) apply (fastforce intro: ccorresE[OF cul ist] EHOther elim: exec.CallUndefined) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorresG sr \<Gamma> r xf P P' hs (do val <- getter;
setter val;
return val
od) (call i f clean (\<lambda>s t. Basic (g s t))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>call i f clean (\<lambda>s t. Basic (g s t)) # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((do val <- getter;
setter val;
return val
od) s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((do val <- getter;
setter val;
return val
od) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>call i f clean (\<lambda>s t. Basic (g s t)) # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((do val <- getter;
setter val;
return val
od) s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((do val <- getter;
setter val;
return val
od) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>call i f clean (\<lambda>s t. Basic (g s t)) # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((do val <- getter;
setter val;
return val
od) s)\<rbrakk> \<Longrightarrow> \<not> snd (getter s)
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>call i f clean (\<lambda>s t. Basic (g s t)) # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((do val <- getter;
setter val;
return val
od) s); \<not> snd (getter s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((do val <- getter;
setter val;
return val
od) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>call i f clean (\<lambda>s t. Basic (g s t)) # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((do val <- getter;
setter val;
return val
od) s); \<not> snd (getter s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((do val <- getter;
setter val;
return val
od) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s sa za na t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma>\<turnstile> \<langle>call i f clean (\<lambda>s t. Basic (g s t)),Normal sa\<rangle> \<Rightarrow> Abrupt za; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,za\<rangle> \<Rightarrow> (na, t)\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst ((do val <- getter;
y <- setter val;
return val
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = length hs) r xf r xf ra t')
 2. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma>\<turnstile> \<langle>call i f clean (\<lambda>s t. Basic (g s t)),Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst ((do val <- getter;
y <- setter val;
return val
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel True r xf r xf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s sa za na t bdy t'. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,za\<rangle> \<Rightarrow> (na, t); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Normal t'; \<Gamma>\<turnstile> \<langle>Basic (g sa t'),Normal (clean sa t')\<rangle> \<Rightarrow> Abrupt za\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst ((do val <- getter;
y <- setter val;
return val
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = length hs) r xf r xf ra t')
 2. \<And>s sa za na t bdy t'. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,clean sa t'\<rangle> \<Rightarrow> (na, t); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Abrupt t'; za = clean sa t'\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst ((do val <- getter;
y <- setter val;
return val
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = length hs) r xf r xf ra t')
 3. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma>\<turnstile> \<langle>call i f clean (\<lambda>s t. Basic (g s t)),Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst ((do val <- getter;
y <- setter val;
return val
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel True r xf r xf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s sa za na t bdy t'. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,clean sa t'\<rangle> \<Rightarrow> (na, t); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Abrupt t'; za = clean sa t'\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst ((do val <- getter;
y <- setter val;
return val
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = length hs) r xf r xf ra t')
 2. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma>\<turnstile> \<langle>call i f clean (\<lambda>s t. Basic (g s t)),Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst ((do val <- getter;
y <- setter val;
return val
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel True r xf r xf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma>\<turnstile> \<langle>call i f clean (\<lambda>s t. Basic (g s t)),Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst ((do val <- getter;
y <- setter val;
return val
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel True r xf r xf ra t') proof (prove)
goal (4 subgoals):
 1. \<And>s sa t bdy t'. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<not> isAbr t; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Normal t'; \<Gamma>\<turnstile> \<langle>Basic (g sa t'),Normal (clean sa t')\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst ((do val <- getter;
y <- setter val;
return val
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel True r xf r xf ra t')
 2. \<And>s sa t bdy fa. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Fault fa; t = Fault fa\<rbrakk> \<Longrightarrow> False
 3. \<And>s sa t bdy. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Stuck; t = Stuck\<rbrakk> \<Longrightarrow> False
 4. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>s sa t bdy t'. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<not> isAbr t; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Normal t'; \<Gamma>\<turnstile> \<langle>Basic (g sa t'),Normal (clean sa t')\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f],i sa\<rangle> \<Rightarrow> (?n189 s sa t bdy t', ?x189 s sa t bdy t')
 2. \<And>s sa t bdy t' t'a ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<not> isAbr t; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Normal t'; \<Gamma>\<turnstile> \<langle>Basic (g sa t'),Normal (clean sa t')\<rangle> \<Rightarrow> t; ?x189 s sa t bdy t' = Normal t'a; (ra, ta) \<in> fst (getter s); (ta, t'a) \<in> sr; unif_rrel (?n189 s sa t bdy t' = length []) r' xf' r' xf' ra t'a; ?n189 s sa t bdy t' \<le> length []\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst ((do val <- getter;
y <- setter val;
return val
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel True r xf r xf ra t')
 3. \<And>s sa t bdy fa. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Fault fa; t = Fault fa\<rbrakk> \<Longrightarrow> False
 4. \<And>s sa t bdy. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Stuck; t = Stuck\<rbrakk> \<Longrightarrow> False
 5. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>s sa t bdy t' t'a ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<not> isAbr t; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Normal t'; \<Gamma>\<turnstile> \<langle>Basic (g sa t'),Normal (clean sa t')\<rangle> \<Rightarrow> t; Normal t' = Normal t'a; (ra, ta) \<in> fst (getter s); (ta, t'a) \<in> sr; unif_rrel (length [] = length []) r' xf' r' xf' ra t'a; length [] \<le> length []\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst ((do val <- getter;
y <- setter val;
return val
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel True r xf r xf ra t')
 2. \<And>s sa t bdy fa. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Fault fa; t = Fault fa\<rbrakk> \<Longrightarrow> False
 3. \<And>s sa t bdy. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Stuck; t = Stuck\<rbrakk> \<Longrightarrow> False
 4. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
using this:
empty_fail (setter ?val)

goal (4 subgoals):
 1. \<And>s sa t bdy t' t'a ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<not> isAbr t; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Normal t'; \<Gamma>\<turnstile> \<langle>Basic (g sa t'),Normal (clean sa t')\<rangle> \<Rightarrow> t; Normal t' = Normal t'a; (ra, ta) \<in> fst (getter s); (ta, t'a) \<in> sr; unif_rrel (length [] = length []) r' xf' r' xf' ra t'a; length [] \<le> length []\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst ((do val <- getter;
y <- setter val;
return val
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel True r xf r xf ra t')
 2. \<And>s sa t bdy fa. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Fault fa; t = Fault fa\<rbrakk> \<Longrightarrow> False
 3. \<And>s sa t bdy. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Stuck; t = Stuck\<rbrakk> \<Longrightarrow> False
 4. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s sa t bdy fa. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Fault fa; t = Fault fa\<rbrakk> \<Longrightarrow> False
 2. \<And>s sa t bdy. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Stuck; t = Stuck\<rbrakk> \<Longrightarrow> False
 3. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s sa t bdy. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i sa)\<rangle> \<Rightarrow> Stuck; t = Stuck\<rbrakk> \<Longrightarrow> False
 2. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd ((do val <- getter;
y <- setter val;
return val
od) s); \<not> snd (getter s); \<Gamma> f = None; t = Stuck\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!