theory L4VerifiedLinks

lemma ccorresE_ccorres_underlying':
  "\<lbrakk> ccorresE st check_termination \<Gamma> G G' A B; no_throw G A \<rbrakk> \<Longrightarrow>
  ccorres_underlying {(s', s). s' = st s} \<Gamma> dc (\<lambda>_. ()) dc (\<lambda>_. ()) G G' [] A B" apply (clarsimp simp: ccorres_underlying_def dc_def) apply (clarsimp simp: ccorresE_def) apply (erule allE, erule impE, force) apply (erule exec_handlers.cases, simp_all) apply clarsimp apply (erule_tac allE, erule (1) impE) apply clarsimp apply (drule (1) no_throw_Inr) apply fastforce apply fastforce apply (clarsimp split: xstate.splits) apply (erule allE, erule conjE, erule impE, assumption) apply (clarsimp simp: unif_rrel_def isAbr_def split: xstate.splits) apply (case_tac ta, simp_all) apply (rule bexI [rotated], assumption) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorresE st check_termination \<Gamma> G G' A B; no_throw G A\<rbrakk> \<Longrightarrow> ccorresG {(s', s). s' = st s} \<Gamma> dc (\<lambda>_. ()) G G' [] A B proof (prove)
goal (1 subgoal):
 1. \<And>b n t. \<lbrakk>ccorresE st check_termination \<Gamma> G G' A B; no_throw G A; G (st b); b \<in> G'; \<not> snd (A (st b)); \<Gamma>\<turnstile>\<^sub>h \<langle>[B],b\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(s', s). s' = st s} \<and> unif_rrel (n = length []) dc (\<lambda>_. ()) dc (\<lambda>_. ()) r s'' | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b n t. \<lbrakk>\<forall>s. G (st s) \<and> s \<in> G' \<and> \<not> snd (A (st s)) \<longrightarrow> (\<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> (case t of Normal s' \<Rightarrow> (Inr (), st s') \<in> fst (A (st s)) | Abrupt s' \<Rightarrow> (Inl (), st s') \<in> fst (A (st s)) | _ \<Rightarrow> False)) \<and> (check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal s); no_throw G A; G (st b); b \<in> G'; \<not> snd (A (st b)); \<Gamma>\<turnstile>\<^sub>h \<langle>[B],b\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(s', s). s' = st s} \<and> unif_rrel (n = length []) dc (\<lambda>_. ()) dc (\<lambda>_. ()) r s'' | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b n t. \<lbrakk>no_throw G A; G (st b); b \<in> G'; \<not> snd (A (st b)); \<Gamma>\<turnstile>\<^sub>h \<langle>[B],b\<rangle> \<Rightarrow> (n, t); (\<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal b\<rangle> \<Rightarrow> t \<longrightarrow> (case t of Normal s' \<Rightarrow> (Inr (), st s') \<in> fst (A (st b)) | Abrupt s' \<Rightarrow> (Inl (), st s') \<in> fst (A (st b)) | _ \<Rightarrow> False)) \<and> (check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal b)\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(s', s). s' = st s} \<and> unif_rrel (n = length []) dc (\<lambda>_. ()) dc (\<lambda>_. ()) r s'' | _ \<Rightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>b n t h s z na ta. \<lbrakk>no_throw G A; G (st s); s \<in> G'; \<not> snd (A (st s)); (\<forall>t. \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> (case t of Normal s' \<Rightarrow> (Inr (), st s') \<in> fst (A (st b)) | Abrupt s' \<Rightarrow> (Inl (), st s') \<in> fst (A (st b)) | _ \<Rightarrow> False)) \<and> (check_termination \<longrightarrow> \<Gamma>\<turnstile>h \<down> Normal s); b = s; B = h; n = na; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>[],z\<rangle> \<Rightarrow> (na, ta)\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(s', s). s' = st s} \<and> unif_rrel (n = length []) dc (\<lambda>_. ()) dc (\<lambda>_. ()) r s'' | _ \<Rightarrow> False
 2. \<And>b n t h s ta. \<lbrakk>no_throw G A; G (st s); s \<in> G'; \<not> snd (A (st s)); (\<forall>t. \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> (case t of Normal s' \<Rightarrow> (Inr (), st s') \<in> fst (A (st b)) | Abrupt s' \<Rightarrow> (Inl (), st s') \<in> fst (A (st b)) | _ \<Rightarrow> False)) \<and> (check_termination \<longrightarrow> \<Gamma>\<turnstile>h \<down> Normal s); b = s; B = h; n = 0; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(s', s). s' = st s} \<and> unif_rrel (n = length []) dc (\<lambda>_. ()) dc (\<lambda>_. ()) r s'' | _ \<Rightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s z na ta. \<lbrakk>no_throw G A; G (st s); s \<in> G'; \<not> snd (A (st s)); \<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>[],z\<rangle> \<Rightarrow> (na, ta); \<forall>t. \<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> (case t of Normal s' \<Rightarrow> (Inr (), st s') \<in> fst (A (st s)) | Abrupt s' \<Rightarrow> (Inl (), st s') \<in> fst (A (st s)) | _ \<Rightarrow> False); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal s\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st s)). (t, s'') \<in> {(s', s). s' = st s} \<and> unif_rrel (na = length []) dc (\<lambda>_. ()) dc (\<lambda>_. ()) r s'' | _ \<Rightarrow> False
 2. \<And>b n t h s ta. \<lbrakk>no_throw G A; G (st s); s \<in> G'; \<not> snd (A (st s)); (\<forall>t. \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> (case t of Normal s' \<Rightarrow> (Inr (), st s') \<in> fst (A (st b)) | Abrupt s' \<Rightarrow> (Inl (), st s') \<in> fst (A (st b)) | _ \<Rightarrow> False)) \<and> (check_termination \<longrightarrow> \<Gamma>\<turnstile>h \<down> Normal s); b = s; B = h; n = 0; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(s', s). s' = st s} \<and> unif_rrel (n = length []) dc (\<lambda>_. ()) dc (\<lambda>_. ()) r s'' | _ \<Rightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s z na ta. \<lbrakk>no_throw G A; G (st s); s \<in> G'; \<not> snd (A (st s)); \<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>[],z\<rangle> \<Rightarrow> (na, ta); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal s; case Abrupt z of Normal s' \<Rightarrow> (Inr (), st s') \<in> fst (A (st s)) | Abrupt s' \<Rightarrow> (Inl (), st s') \<in> fst (A (st s)) | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st s)). (t, s'') \<in> {(s', s). s' = st s} \<and> unif_rrel (na = length []) dc (\<lambda>_. ()) dc (\<lambda>_. ()) r s'' | _ \<Rightarrow> False
 2. \<And>b n t h s ta. \<lbrakk>no_throw G A; G (st s); s \<in> G'; \<not> snd (A (st s)); (\<forall>t. \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> (case t of Normal s' \<Rightarrow> (Inr (), st s') \<in> fst (A (st b)) | Abrupt s' \<Rightarrow> (Inl (), st s') \<in> fst (A (st b)) | _ \<Rightarrow> False)) \<and> (check_termination \<longrightarrow> \<Gamma>\<turnstile>h \<down> Normal s); b = s; B = h; n = 0; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(s', s). s' = st s} \<and> unif_rrel (n = length []) dc (\<lambda>_. ()) dc (\<lambda>_. ()) r s'' | _ \<Rightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s z na ta. \<lbrakk>no_throw G A; G (st s); s \<in> G'; \<not> snd (A (st s)); \<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>[],z\<rangle> \<Rightarrow> (na, ta); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal s; (Inl (), st z) \<in> fst (A (st s))\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st s)). (t, s'') \<in> {(s', s). s' = st s} \<and> unif_rrel (na = length []) dc (\<lambda>_. ()) dc (\<lambda>_. ()) r s'' | _ \<Rightarrow> False
 2. \<And>b n t h s ta. \<lbrakk>no_throw G A; G (st s); s \<in> G'; \<not> snd (A (st s)); (\<forall>t. \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> (case t of Normal s' \<Rightarrow> (Inr (), st s') \<in> fst (A (st b)) | Abrupt s' \<Rightarrow> (Inl (), st s') \<in> fst (A (st b)) | _ \<Rightarrow> False)) \<and> (check_termination \<longrightarrow> \<Gamma>\<turnstile>h \<down> Normal s); b = s; B = h; n = 0; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(s', s). s' = st s} \<and> unif_rrel (n = length []) dc (\<lambda>_. ()) dc (\<lambda>_. ()) r s'' | _ \<Rightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s z na ta. \<lbrakk>no_throw G A; G (st s); s \<in> G'; \<not> snd (A (st s)); \<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>[],z\<rangle> \<Rightarrow> (na, ta); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal s\<rbrakk> \<Longrightarrow> G (st s)
 2. \<And>s z na ta. \<lbrakk>no_throw G A; G (st s); s \<in> G'; \<not> snd (A (st s)); \<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>[],z\<rangle> \<Rightarrow> (na, ta); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal s; \<exists>y. fst (Inl (), st z) = Inr y\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st s)). (t, s'') \<in> {(s', s). s' = st s} \<and> unif_rrel (na = length []) dc (\<lambda>_. ()) dc (\<lambda>_. ()) r s'' | _ \<Rightarrow> False
 3. \<And>b n t h s ta. \<lbrakk>no_throw G A; G (st s); s \<in> G'; \<not> snd (A (st s)); (\<forall>t. \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> (case t of Normal s' \<Rightarrow> (Inr (), st s') \<in> fst (A (st b)) | Abrupt s' \<Rightarrow> (Inl (), st s') \<in> fst (A (st b)) | _ \<Rightarrow> False)) \<and> (check_termination \<longrightarrow> \<Gamma>\<turnstile>h \<down> Normal s); b = s; B = h; n = 0; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(s', s). s' = st s} \<and> unif_rrel (n = length []) dc (\<lambda>_. ()) dc (\<lambda>_. ()) r s'' | _ \<Rightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s z na ta. \<lbrakk>no_throw G A; G (st s); s \<in> G'; \<not> snd (A (st s)); \<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>[],z\<rangle> \<Rightarrow> (na, ta); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal s; \<exists>y. fst (Inl (), st z) = Inr y\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st s)). (t, s'') \<in> {(s', s). s' = st s} \<and> unif_rrel (na = length []) dc (\<lambda>_. ()) dc (\<lambda>_. ()) r s'' | _ \<Rightarrow> False
 2. \<And>b n t h s ta. \<lbrakk>no_throw G A; G (st s); s \<in> G'; \<not> snd (A (st s)); (\<forall>t. \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> (case t of Normal s' \<Rightarrow> (Inr (), st s') \<in> fst (A (st b)) | Abrupt s' \<Rightarrow> (Inl (), st s') \<in> fst (A (st b)) | _ \<Rightarrow> False)) \<and> (check_termination \<longrightarrow> \<Gamma>\<turnstile>h \<down> Normal s); b = s; B = h; n = 0; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(s', s). s' = st s} \<and> unif_rrel (n = length []) dc (\<lambda>_. ()) dc (\<lambda>_. ()) r s'' | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b n t h s ta. \<lbrakk>no_throw G A; G (st s); s \<in> G'; \<not> snd (A (st s)); (\<forall>t. \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> (case t of Normal s' \<Rightarrow> (Inr (), st s') \<in> fst (A (st b)) | Abrupt s' \<Rightarrow> (Inl (), st s') \<in> fst (A (st b)) | _ \<Rightarrow> False)) \<and> (check_termination \<longrightarrow> \<Gamma>\<turnstile>h \<down> Normal s); b = s; B = h; n = 0; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> case ta of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (A (st b)). (t, s'') \<in> {(s', s). s' = st s} \<and> unif_rrel (n = length []) dc (\<lambda>_. ()) dc (\<lambda>_. ()) r s'' | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta; no_throw G A; G (st s); s \<in> G'; \<not> snd (A (st s)); \<forall>t. (\<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (Inr (), st x1) \<in> fst (A (st s)))) \<and> (\<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (Inl (), st x2) \<in> fst (A (st s)))) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> \<not> \<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> t) \<and> (t = Stuck \<longrightarrow> \<not> \<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> Stuck); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal s\<rbrakk> \<Longrightarrow> (\<forall>x1. ta = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (A (st s)). case x of (r, t) \<Rightarrow> t = st x1 \<and> unif_rrel True dc (\<lambda>_. ()) dc (\<lambda>_. ()) r x1)) \<and> (\<forall>x2. ta \<noteq> Abrupt x2) \<and> (\<forall>x3. ta \<noteq> Fault x3) \<and> ta \<noteq> Stuck proof (prove)
goal (1 subgoal):
 1. \<And>s ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta; no_throw G A; G (st s); s \<in> G'; \<not> snd (A (st s)); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal s; (\<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> ta \<longrightarrow> (\<forall>x2. ta = Abrupt x2 \<longrightarrow> (Inl (), st x2) \<in> fst (A (st s)))) \<and> ((\<forall>x3. ta \<noteq> Fault x3) \<or> \<not> \<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> ta) \<and> (ta = Stuck \<longrightarrow> \<not> \<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> Stuck); \<forall>x1. ta = Normal x1 \<longrightarrow> (Inr (), st x1) \<in> fst (A (st s))\<rbrakk> \<Longrightarrow> (\<forall>x1. ta = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (A (st s)). case x of (r, t) \<Rightarrow> t = st x1 \<and> unif_rrel True dc (\<lambda>_. ()) dc (\<lambda>_. ()) r x1)) \<and> (\<forall>x2. ta \<noteq> Abrupt x2) \<and> (\<forall>x3. ta \<noteq> Fault x3) \<and> ta \<noteq> Stuck proof (prove)
goal (1 subgoal):
 1. \<And>s ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> ta; \<forall>s. ta \<noteq> Abrupt s; no_throw G A; G (st s); s \<in> G'; \<not> snd (A (st s)); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal s; \<forall>x1. ta = Normal x1 \<longrightarrow> (Inr (), st x1) \<in> fst (A (st s)); \<forall>x3. ta \<noteq> Fault x3; ta = Stuck \<longrightarrow> \<not> \<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> Stuck\<rbrakk> \<Longrightarrow> (\<forall>x1. ta = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (A (st s)). case x of (r, t) \<Rightarrow> t = st x1)) \<and> ta \<noteq> Stuck proof (prove)
goal (1 subgoal):
 1. \<And>s ta x1. \<lbrakk>\<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> Normal x1; no_throw G A; G (st s); s \<in> G'; \<not> snd (A (st s)); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal s; (Inr (), st x1) \<in> fst (A (st s)); ta = Normal x1\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (A (st s)). case x of (r, t) \<Rightarrow> t = st x1 proof (prove)
goal (1 subgoal):
 1. \<And>s ta x1. \<lbrakk>\<Gamma>\<turnstile> \<langle>B,Normal s\<rangle> \<Rightarrow> Normal x1; no_throw G A; G (st s); s \<in> G'; \<not> snd (A (st s)); check_termination \<longrightarrow> \<Gamma>\<turnstile>B \<down> Normal s; (Inr (), st x1) \<in> fst (A (st s)); ta = Normal x1\<rbrakk> \<Longrightarrow> case (Inr (), st x1) of (r, t) \<Rightarrow> t = st x1 proof (prove)
goal:
No subgoals!