theory CCorresLemmas

lemma ccorres_stateAssert:
  "ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c \<Longrightarrow>
   ccorres_underlying sr Gamm r xf arrel axf (\<lambda>s. Q s \<longrightarrow> P s) P' hs (stateAssert Q [] >>= a) c" apply (rule ccorres_guard_imp [OF ccorres_symb_exec_l]) apply simp apply (clarsimp simp: stateAssert_def) apply (wp, simp)[1] apply (clarsimp simp: stateAssert_def) apply wp[1] apply (simp add: empty_fail_stateAssert) apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf (\<lambda>s. Q s \<longrightarrow> P s) P' hs (stateAssert Q [] >>= a) c proof (prove)
goal (6 subgoals):
 1. \<And>rv. ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf (?Q1 rv) (?Q'1 rv) hs (a rv) c
 2. \<And>s. ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c \<Longrightarrow> \<lbrace>(=) s\<rbrace> stateAssert Q [] \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c \<Longrightarrow> \<lbrace>?Q\<rbrace> stateAssert Q [] \<lbrace>?Q1\<rbrace>
 4. ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c \<Longrightarrow> empty_fail (stateAssert Q [])
 5. \<And>s. \<lbrakk>ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c; Q s \<longrightarrow> P s\<rbrakk> \<Longrightarrow> ?Q s
 6. \<And>s. \<lbrakk>ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c; s \<in> P'\<rbrakk> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> sr \<and> ?Q1 rv s \<longrightarrow> s' \<in> ?Q'1 rv} proof (prove)
goal (5 subgoals):
 1. \<And>s. ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c \<Longrightarrow> \<lbrace>(=) s\<rbrace> stateAssert Q [] \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c \<Longrightarrow> \<lbrace>?Q\<rbrace> stateAssert Q [] \<lbrace>\<lambda>a. P\<rbrace>
 3. ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c \<Longrightarrow> empty_fail (stateAssert Q [])
 4. \<And>s. \<lbrakk>ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c; Q s \<longrightarrow> P s\<rbrakk> \<Longrightarrow> ?Q s
 5. \<And>s. \<lbrakk>ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c; s \<in> P'\<rbrakk> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> sr \<and> P s \<longrightarrow> s' \<in> P'} proof (prove)
goal (5 subgoals):
 1. \<And>s. ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c \<Longrightarrow> \<lbrace>(=) s\<rbrace> do s <- get;
assert (Q s)
od \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c \<Longrightarrow> \<lbrace>?Q\<rbrace> stateAssert Q [] \<lbrace>\<lambda>a. P\<rbrace>
 3. ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c \<Longrightarrow> empty_fail (stateAssert Q [])
 4. \<And>s. \<lbrakk>ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c; Q s \<longrightarrow> P s\<rbrakk> \<Longrightarrow> ?Q s
 5. \<And>s. \<lbrakk>ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c; s \<in> P'\<rbrakk> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> sr \<and> P s \<longrightarrow> s' \<in> P'} proof (prove)
goal (4 subgoals):
 1. ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c \<Longrightarrow> \<lbrace>?Q\<rbrace> stateAssert Q [] \<lbrace>\<lambda>a. P\<rbrace>
 2. ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c \<Longrightarrow> empty_fail (stateAssert Q [])
 3. \<And>s. \<lbrakk>ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c; Q s \<longrightarrow> P s\<rbrakk> \<Longrightarrow> ?Q s
 4. \<And>s. \<lbrakk>ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c; s \<in> P'\<rbrakk> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> sr \<and> P s \<longrightarrow> s' \<in> P'} proof (prove)
goal (4 subgoals):
 1. ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c \<Longrightarrow> \<lbrace>?Q\<rbrace> do s <- get;
assert (Q s)
od \<lbrace>\<lambda>a. P\<rbrace>
 2. ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c \<Longrightarrow> empty_fail (stateAssert Q [])
 3. \<And>s. \<lbrakk>ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c; Q s \<longrightarrow> P s\<rbrakk> \<Longrightarrow> ?Q s
 4. \<And>s. \<lbrakk>ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c; s \<in> P'\<rbrakk> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> sr \<and> P s \<longrightarrow> s' \<in> P'} proof (prove)
goal (3 subgoals):
 1. ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c \<Longrightarrow> empty_fail (stateAssert Q [])
 2. \<And>s. \<lbrakk>ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c; Q s \<longrightarrow> P s\<rbrakk> \<Longrightarrow> Q s \<longrightarrow> P s
 3. \<And>s. \<lbrakk>ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c; s \<in> P'\<rbrakk> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> sr \<and> P s \<longrightarrow> s' \<in> P'} proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c; Q s \<longrightarrow> P s\<rbrakk> \<Longrightarrow> Q s \<longrightarrow> P s
 2. \<And>s. \<lbrakk>ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c; s \<in> P'\<rbrakk> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> sr \<and> P s \<longrightarrow> s' \<in> P'} proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ccorres_underlying sr Gamm r xf arrel axf P P' hs (a ()) c; s \<in> P'\<rbrakk> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> sr \<and> P s \<longrightarrow> s' \<in> P'} proof (prove)
goal:
No subgoals!