theory Retype_R

lemma createObjects_corres':
  "\<lbrakk>corres r P P' f (createObjects a b ko d); ko = injectKO val\<rbrakk>
   \<Longrightarrow> corres dc P P' f (createObjects' a b ko d)" apply (clarsimp simp:corres_underlying_def createObjects_def return_def) apply (rule conjI) apply (clarsimp simp:bind_def split_def) apply (drule(1) bspec) apply (clarsimp simp:image_def) apply (drule(1) bspec) apply clarsimp apply (erule bexI[rotated]) apply simp apply (clarsimp simp:bind_def split_def image_def) apply (drule(1) bspec|clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres r P P' f (createObjects a b ko d); ko = injectKO val\<rbrakk> \<Longrightarrow> corres dc P P' f (createObjects' a b ko d) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>\<forall>x\<in>state_relation. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst ((do oBits <- \<lambda>s. ({(objBitsKO (injectKO val), s)}, False);
gBits <- \<lambda>s. ({(oBits + d, s)}, False);
y <- createObjects' a b (injectKO val) d;
\<lambda>s. ({(map (\<lambda>n. a + (n << gBits)) [0 .e. word_of_nat b - 1], s)}, False)
od) s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> state_relation \<and> r ra r') \<and> \<not> snd ((do oBits <- \<lambda>s. ({(objBitsKO (injectKO val), s)}, False);
gBits <- \<lambda>s. ({(oBits + d, s)}, False);
y <- createObjects' a b (injectKO val) d;
\<lambda>s. ({(map (\<lambda>n. a + (n << gBits)) [0 .e. word_of_nat b - 1], s)}, False)
od) s'); ko = injectKO val; (aa, ba) \<in> state_relation; P aa; P' ba\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (createObjects' a b (injectKO val) d ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f aa). case x of (r, t) \<Rightarrow> (t, t') \<in> state_relation) \<and> \<not> snd (createObjects' a b (injectKO val) d ba) proof (prove)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>\<forall>x\<in>state_relation. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst ((do oBits <- \<lambda>s. ({(objBitsKO (injectKO val), s)}, False);
gBits <- \<lambda>s. ({(oBits + d, s)}, False);
y <- createObjects' a b (injectKO val) d;
\<lambda>s. ({(map (\<lambda>n. a + (n << gBits)) [0 .e. word_of_nat b - 1], s)}, False)
od) s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> state_relation \<and> r ra r') \<and> \<not> snd ((do oBits <- \<lambda>s. ({(objBitsKO (injectKO val), s)}, False);
gBits <- \<lambda>s. ({(oBits + d, s)}, False);
y <- createObjects' a b (injectKO val) d;
\<lambda>s. ({(map (\<lambda>n. a + (n << gBits)) [0 .e. word_of_nat b - 1], s)}, False)
od) s'); ko = injectKO val; (aa, ba) \<in> state_relation; P aa; P' ba\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (createObjects' a b (injectKO val) d ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f aa). case x of (r, t) \<Rightarrow> (t, t') \<in> state_relation
 2. \<And>aa ba. \<lbrakk>\<forall>x\<in>state_relation. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst ((do oBits <- \<lambda>s. ({(objBitsKO (injectKO val), s)}, False);
gBits <- \<lambda>s. ({(oBits + d, s)}, False);
y <- createObjects' a b (injectKO val) d;
\<lambda>s. ({(map (\<lambda>n. a + (n << gBits)) [0 .e. word_of_nat b - 1], s)}, False)
od) s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> state_relation \<and> r ra r') \<and> \<not> snd ((do oBits <- \<lambda>s. ({(objBitsKO (injectKO val), s)}, False);
gBits <- \<lambda>s. ({(oBits + d, s)}, False);
y <- createObjects' a b (injectKO val) d;
\<lambda>s. ({(map (\<lambda>n. a + (n << gBits)) [0 .e. word_of_nat b - 1], s)}, False)
od) s'); ko = injectKO val; (aa, ba) \<in> state_relation; P aa; P' ba\<rbrakk> \<Longrightarrow> \<not> snd (createObjects' a b (injectKO val) d ba) proof (prove)
goal (2 subgoals):
 1. \<And>aa ba bb. \<lbrakk>\<forall>x\<in>state_relation. P (fst x) \<and> P' (snd x) \<longrightarrow> (\<forall>y\<in>fst (createObjects' a b (injectKO val) d (snd x)). \<exists>x\<in>fst (f (fst x)). (snd x, snd y) \<in> state_relation \<and> r (fst x) (map (\<lambda>n. a + (n << objBitsKO (injectKO val) + d)) [0 .e. word_of_nat b - 1])) \<and> \<not> snd (createObjects' a b (injectKO val) d (snd x)); ko = injectKO val; (aa, ba) \<in> state_relation; P aa; P' ba; ((), bb) \<in> fst (createObjects' a b (injectKO val) d ba)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f aa). (snd x, bb) \<in> state_relation
 2. \<And>aa ba. \<lbrakk>\<forall>x\<in>state_relation. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst ((do oBits <- \<lambda>s. ({(objBitsKO (injectKO val), s)}, False);
gBits <- \<lambda>s. ({(oBits + d, s)}, False);
y <- createObjects' a b (injectKO val) d;
\<lambda>s. ({(map (\<lambda>n. a + (n << gBits)) [0 .e. word_of_nat b - 1], s)}, False)
od) s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> state_relation \<and> r ra r') \<and> \<not> snd ((do oBits <- \<lambda>s. ({(objBitsKO (injectKO val), s)}, False);
gBits <- \<lambda>s. ({(oBits + d, s)}, False);
y <- createObjects' a b (injectKO val) d;
\<lambda>s. ({(map (\<lambda>n. a + (n << gBits)) [0 .e. word_of_nat b - 1], s)}, False)
od) s'); ko = injectKO val; (aa, ba) \<in> state_relation; P aa; P' ba\<rbrakk> \<Longrightarrow> \<not> snd (createObjects' a b (injectKO val) d ba) proof (prove)
goal (2 subgoals):
 1. \<And>aa ba baa. \<lbrakk>ko = injectKO val; (aa, ba) \<in> state_relation; P aa; P' ba; ((), baa) \<in> fst (createObjects' a b (injectKO val) d ba); P (fst (aa, ba)) \<and> P' (snd (aa, ba)) \<longrightarrow> (\<forall>y\<in>fst (createObjects' a b (injectKO val) d (snd (aa, ba))). \<exists>x\<in>fst (f (fst (aa, ba))). (snd x, snd y) \<in> state_relation \<and> r (fst x) (map (\<lambda>n. a + (n << objBitsKO (injectKO val) + d)) [0 .e. word_of_nat b - 1])) \<and> \<not> snd (createObjects' a b (injectKO val) d (snd (aa, ba)))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f aa). (snd x, baa) \<in> state_relation
 2. \<And>aa ba. \<lbrakk>\<forall>x\<in>state_relation. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst ((do oBits <- \<lambda>s. ({(objBitsKO (injectKO val), s)}, False);
gBits <- \<lambda>s. ({(oBits + d, s)}, False);
y <- createObjects' a b (injectKO val) d;
\<lambda>s. ({(map (\<lambda>n. a + (n << gBits)) [0 .e. word_of_nat b - 1], s)}, False)
od) s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> state_relation \<and> r ra r') \<and> \<not> snd ((do oBits <- \<lambda>s. ({(objBitsKO (injectKO val), s)}, False);
gBits <- \<lambda>s. ({(oBits + d, s)}, False);
y <- createObjects' a b (injectKO val) d;
\<lambda>s. ({(map (\<lambda>n. a + (n << gBits)) [0 .e. word_of_nat b - 1], s)}, False)
od) s'); ko = injectKO val; (aa, ba) \<in> state_relation; P aa; P' ba\<rbrakk> \<Longrightarrow> \<not> snd (createObjects' a b (injectKO val) d ba) proof (prove)
goal (2 subgoals):
 1. \<And>aa ba baa. \<lbrakk>ko = injectKO val; (aa, ba) \<in> state_relation; P aa; P' ba; ((), baa) \<in> fst (createObjects' a b (injectKO val) d ba); \<forall>y\<in>fst (createObjects' a b (injectKO val) d ba). \<exists>x\<in>fst (f aa). (snd x, snd y) \<in> state_relation \<and> r (fst x) (map (\<lambda>n. a + (n << objBitsKO (injectKO val) + d)) [0 .e. word_of_nat b - 1]); \<not> snd (createObjects' a b (injectKO val) d ba)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f aa). (snd x, baa) \<in> state_relation
 2. \<And>aa ba. \<lbrakk>\<forall>x\<in>state_relation. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst ((do oBits <- \<lambda>s. ({(objBitsKO (injectKO val), s)}, False);
gBits <- \<lambda>s. ({(oBits + d, s)}, False);
y <- createObjects' a b (injectKO val) d;
\<lambda>s. ({(map (\<lambda>n. a + (n << gBits)) [0 .e. word_of_nat b - 1], s)}, False)
od) s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> state_relation \<and> r ra r') \<and> \<not> snd ((do oBits <- \<lambda>s. ({(objBitsKO (injectKO val), s)}, False);
gBits <- \<lambda>s. ({(oBits + d, s)}, False);
y <- createObjects' a b (injectKO val) d;
\<lambda>s. ({(map (\<lambda>n. a + (n << gBits)) [0 .e. word_of_nat b - 1], s)}, False)
od) s'); ko = injectKO val; (aa, ba) \<in> state_relation; P aa; P' ba\<rbrakk> \<Longrightarrow> \<not> snd (createObjects' a b (injectKO val) d ba) proof (prove)
goal (2 subgoals):
 1. \<And>aa ba baa. \<lbrakk>ko = injectKO val; (aa, ba) \<in> state_relation; P aa; P' ba; ((), baa) \<in> fst (createObjects' a b (injectKO val) d ba); \<not> snd (createObjects' a b (injectKO val) d ba); \<exists>x\<in>fst (f aa). (snd x, snd ((), baa)) \<in> state_relation \<and> r (fst x) (map (\<lambda>n. a + (n << objBitsKO (injectKO val) + d)) [0 .e. word_of_nat b - 1])\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f aa). (snd x, baa) \<in> state_relation
 2. \<And>aa ba. \<lbrakk>\<forall>x\<in>state_relation. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst ((do oBits <- \<lambda>s. ({(objBitsKO (injectKO val), s)}, False);
gBits <- \<lambda>s. ({(oBits + d, s)}, False);
y <- createObjects' a b (injectKO val) d;
\<lambda>s. ({(map (\<lambda>n. a + (n << gBits)) [0 .e. word_of_nat b - 1], s)}, False)
od) s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> state_relation \<and> r ra r') \<and> \<not> snd ((do oBits <- \<lambda>s. ({(objBitsKO (injectKO val), s)}, False);
gBits <- \<lambda>s. ({(oBits + d, s)}, False);
y <- createObjects' a b (injectKO val) d;
\<lambda>s. ({(map (\<lambda>n. a + (n << gBits)) [0 .e. word_of_nat b - 1], s)}, False)
od) s'); ko = injectKO val; (aa, ba) \<in> state_relation; P aa; P' ba\<rbrakk> \<Longrightarrow> \<not> snd (createObjects' a b (injectKO val) d ba) proof (prove)
goal (2 subgoals):
 1. \<And>aa ba baa aaa bb. \<lbrakk>ko = injectKO val; (aa, ba) \<in> state_relation; P aa; P' ba; ((), baa) \<in> fst (createObjects' a b (injectKO val) d ba); \<not> snd (createObjects' a b (injectKO val) d ba); (aaa, bb) \<in> fst (f aa); (bb, baa) \<in> state_relation; r aaa (map (\<lambda>n. a + (n << objBitsKO (injectKO val) + d)) [0 .e. word_of_nat b - 1])\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f aa). (snd x, baa) \<in> state_relation
 2. \<And>aa ba. \<lbrakk>\<forall>x\<in>state_relation. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst ((do oBits <- \<lambda>s. ({(objBitsKO (injectKO val), s)}, False);
gBits <- \<lambda>s. ({(oBits + d, s)}, False);
y <- createObjects' a b (injectKO val) d;
\<lambda>s. ({(map (\<lambda>n. a + (n << gBits)) [0 .e. word_of_nat b - 1], s)}, False)
od) s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> state_relation \<and> r ra r') \<and> \<not> snd ((do oBits <- \<lambda>s. ({(objBitsKO (injectKO val), s)}, False);
gBits <- \<lambda>s. ({(oBits + d, s)}, False);
y <- createObjects' a b (injectKO val) d;
\<lambda>s. ({(map (\<lambda>n. a + (n << gBits)) [0 .e. word_of_nat b - 1], s)}, False)
od) s'); ko = injectKO val; (aa, ba) \<in> state_relation; P aa; P' ba\<rbrakk> \<Longrightarrow> \<not> snd (createObjects' a b (injectKO val) d ba) proof (prove)
goal (2 subgoals):
 1. \<And>aa ba baa aaa bb. \<lbrakk>ko = injectKO val; (aa, ba) \<in> state_relation; P aa; P' ba; ((), baa) \<in> fst (createObjects' a b (injectKO val) d ba); \<not> snd (createObjects' a b (injectKO val) d ba); (bb, baa) \<in> state_relation; r aaa (map (\<lambda>n. a + (n << objBitsKO (injectKO val) + d)) [0 .e. word_of_nat b - 1])\<rbrakk> \<Longrightarrow> (snd (aaa, bb), baa) \<in> state_relation
 2. \<And>aa ba. \<lbrakk>\<forall>x\<in>state_relation. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst ((do oBits <- \<lambda>s. ({(objBitsKO (injectKO val), s)}, False);
gBits <- \<lambda>s. ({(oBits + d, s)}, False);
y <- createObjects' a b (injectKO val) d;
\<lambda>s. ({(map (\<lambda>n. a + (n << gBits)) [0 .e. word_of_nat b - 1], s)}, False)
od) s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> state_relation \<and> r ra r') \<and> \<not> snd ((do oBits <- \<lambda>s. ({(objBitsKO (injectKO val), s)}, False);
gBits <- \<lambda>s. ({(oBits + d, s)}, False);
y <- createObjects' a b (injectKO val) d;
\<lambda>s. ({(map (\<lambda>n. a + (n << gBits)) [0 .e. word_of_nat b - 1], s)}, False)
od) s'); ko = injectKO val; (aa, ba) \<in> state_relation; P aa; P' ba\<rbrakk> \<Longrightarrow> \<not> snd (createObjects' a b (injectKO val) d ba) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>\<forall>x\<in>state_relation. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst ((do oBits <- \<lambda>s. ({(objBitsKO (injectKO val), s)}, False);
gBits <- \<lambda>s. ({(oBits + d, s)}, False);
y <- createObjects' a b (injectKO val) d;
\<lambda>s. ({(map (\<lambda>n. a + (n << gBits)) [0 .e. word_of_nat b - 1], s)}, False)
od) s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> state_relation \<and> r ra r') \<and> \<not> snd ((do oBits <- \<lambda>s. ({(objBitsKO (injectKO val), s)}, False);
gBits <- \<lambda>s. ({(oBits + d, s)}, False);
y <- createObjects' a b (injectKO val) d;
\<lambda>s. ({(map (\<lambda>n. a + (n << gBits)) [0 .e. word_of_nat b - 1], s)}, False)
od) s'); ko = injectKO val; (aa, ba) \<in> state_relation; P aa; P' ba\<rbrakk> \<Longrightarrow> \<not> snd (createObjects' a b (injectKO val) d ba) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>\<forall>x\<in>state_relation. P (fst x) \<and> P' (snd x) \<longrightarrow> (\<forall>y. (\<exists>x\<in>fst (createObjects' a b (injectKO val) d (snd x)). y = {(map (\<lambda>n. a + (n << objBitsKO (injectKO val) + d)) [0 .e. word_of_nat b - 1], snd x)}) \<longrightarrow> (\<forall>xa\<in>y. \<exists>x\<in>fst (f (fst x)). (snd x, snd xa) \<in> state_relation \<and> r (fst x) (fst xa))) \<and> \<not> snd (createObjects' a b (injectKO val) d (snd x)); ko = injectKO val; (aa, ba) \<in> state_relation; P aa; P' ba; snd (createObjects' a b (injectKO val) d ba)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!