theory Detype_C

lemma ccorres_stateAssert_fwd:
  "ccorres r xf (P and R) P' hs b c \<Longrightarrow> ccorres r xf P P' hs (stateAssert R vs >>= (\<lambda>_. b)) c" apply (rule ccorresI') apply (simp add: stateAssert_def bind_assoc) apply (drule not_snd_bindD) apply (fastforce simp add: in_monad) apply clarsimp apply (frule not_snd_bindI1) apply simp apply (erule (1) ccorresE) apply simp apply assumption apply assumption apply assumption apply (fastforce simp: in_monad') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf (P and R) P' hs b c \<Longrightarrow> ccorres r xf P P' hs (do _ <- stateAssert R vs;
b
od) c proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>ccorres r xf (P and R) P' hs b c; (s, s') \<in> rf_sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((do _ <- stateAssert R vs;
b
od) s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((do _ <- stateAssert R vs;
b
od) s). (t, t') \<in> rf_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>ccorres r xf (P and R) P' hs b c; (s, s') \<in> rf_sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((do x <- get;
_ <- assert (R x);
b
od) s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((do x <- get;
_ <- assert (R x);
b
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> rf_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>ccorres r xf (P and R) P' hs b c; (s, s') \<in> rf_sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<rbrakk> \<Longrightarrow> (?rv4 s s' n z, ?s'4 s s' n z) \<in> fst (get s)
 2. \<And>s s' n z. \<lbrakk>ccorres r xf (P and R) P' hs b c; (s, s') \<in> rf_sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (get s) \<and> \<not> snd ((do _ <- assert (R (?rv4 s s' n z));
b
od) (?s'4 s s' n z))\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((do x <- get;
_ <- assert (R x);
b
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> rf_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>ccorres r xf (P and R) P' hs b c; (s, s') \<in> rf_sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (get s) \<and> \<not> snd ((do _ <- assert (R s);
b
od) s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((do x <- get;
_ <- assert (R x);
b
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> rf_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>ccorres r xf (P and R) P' hs b c; (s, s') \<in> rf_sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (get s); \<not> snd ((do _ <- assert (R s);
b
od) s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((do x <- get;
_ <- assert (R x);
b
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> rf_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>ccorres r xf (P and R) P' hs b c; (s, s') \<in> rf_sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (get s); \<not> snd ((do _ <- assert (R s);
b
od) s); \<not> snd (assert (R s) s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((do x <- get;
_ <- assert (R x);
b
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> rf_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>ccorres r xf (P and R) P' hs b c; (s, s') \<in> rf_sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (get s); \<not> snd (b s); R s\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((do x <- get;
_ <- assert (R x);
b
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf ra t') proof (prove)
goal (5 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (get s); \<not> snd (b s); R s\<rbrakk> \<Longrightarrow> (P and R) s
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (get s); \<not> snd (b s); R s\<rbrakk> \<Longrightarrow> s' \<in> P'
 3. \<And>s s' n z. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (get s); \<not> snd (b s); R s\<rbrakk> \<Longrightarrow> \<not> snd (b s)
 4. \<And>s s' n z. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (get s); \<not> snd (b s); R s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n15 s s' n z, ?x15 s s' n z)
 5. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (get s); \<not> snd (b s); R s; ?x15 s s' n z = Normal t'; (ra, t) \<in> fst (b s); (t, t') \<in> rf_sr; unif_rrel (?n15 s s' n z = length hs) r xf r xf ra t'; ?n15 s s' n z \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((do x <- get;
_ <- assert (R x);
b
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf ra t') proof (prove)
goal (4 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (get s); \<not> snd (b s); R s\<rbrakk> \<Longrightarrow> s' \<in> P'
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (get s); \<not> snd (b s); R s\<rbrakk> \<Longrightarrow> \<not> snd (b s)
 3. \<And>s s' n z. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (get s); \<not> snd (b s); R s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n15 s s' n z, ?x15 s s' n z)
 4. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (get s); \<not> snd (b s); R s; ?x15 s s' n z = Normal t'; (ra, t) \<in> fst (b s); (t, t') \<in> rf_sr; unif_rrel (?n15 s s' n z = length hs) r xf r xf ra t'; ?n15 s s' n z \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((do x <- get;
_ <- assert (R x);
b
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (get s); \<not> snd (b s); R s\<rbrakk> \<Longrightarrow> \<not> snd (b s)
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (get s); \<not> snd (b s); R s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n15 s s' n z, ?x15 s s' n z)
 3. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (get s); \<not> snd (b s); R s; ?x15 s s' n z = Normal t'; (ra, t) \<in> fst (b s); (t, t') \<in> rf_sr; unif_rrel (?n15 s s' n z = length hs) r xf r xf ra t'; ?n15 s s' n z \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((do x <- get;
_ <- assert (R x);
b
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> rf_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> rf_sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (get s); \<not> snd (b s); R s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n15 s s' n z, ?x15 s s' n z)
 2. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (get s); \<not> snd (b s); R s; ?x15 s s' n z = Normal t'; (ra, t) \<in> fst (b s); (t, t') \<in> rf_sr; unif_rrel (?n15 s s' n z = length hs) r xf r xf ra t'; ?n15 s s' n z \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((do x <- get;
_ <- assert (R x);
b
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> rf_sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (get s); \<not> snd (b s); R s; z = Normal t'; (ra, t) \<in> fst (b s); (t, t') \<in> rf_sr; unif_rrel (n = length hs) r xf r xf ra t'; n \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((do x <- get;
_ <- assert (R x);
b
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf ra t') proof (prove)
goal:
No subgoals!