theory Corres_D

lemma dcorres_gets_the:
  assumes A: "\<And>s s' obj obj'. \<lbrakk>s = transform s';P s; P' s';  g' s' = Some obj' ;g s = Some obj\<rbrakk>
          \<Longrightarrow> dcorres r ((=) s) ((=) s') (f obj) (f' obj')"
  assumes B: "\<And>s s'. \<lbrakk>s = transform s'; P s; P' s' ; g' s' \<noteq> None\<rbrakk> \<Longrightarrow> g s \<noteq> None"
  shows "dcorres r P P' (do a\<leftarrow>gets_the (g);f a od) (do a\<leftarrow> gets_the (g'); f' a od)" apply (simp add:gets_the_def) apply (simp add: gets_def) apply (subst bind_assoc)+ apply (rule corres_split_keep_pfx[where r'="\<lambda>s s'. s = transform s'\<and> P s \<and> P' s'"
                                      and Q="\<lambda>x s. x = s" and Q'="\<lambda>x s. x = s "]) apply (clarsimp simp: corres_underlying_def get_def) apply (simp add: assert_opt_def) apply (rename_tac x) apply (case_tac "g' x = None") apply (clarsimp split:option.splits simp:corres_free_fail) apply (subgoal_tac "\<exists>obj. g (transform x) \<noteq> None") apply (clarsimp split:option.splits) apply (rule_tac Q="(=) (transform x)" and Q'="(=) x" in corres_guard_imp) apply (simp add: A)+ using B apply (wp|clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres r P P' (gets_the g >>= f) (gets_the g' >>= f') proof (prove)
goal (1 subgoal):
 1. dcorres r P P' (gets g >>= assert_opt >>= f) (gets g' >>= assert_opt >>= f') proof (prove)
goal (1 subgoal):
 1. dcorres r P P' (do s <- get;
assert_opt (g s)
od >>= f) (do s <- get;
assert_opt (g' s)
od >>= f') proof (prove)
goal (1 subgoal):
 1. dcorres r P P' (do x <- get;
assert_opt (g x) >>= f
od) (do x <- get;
assert_opt (g' x) >>= f'
od) proof (prove)
goal (4 subgoals):
 1. dcorres (\<lambda>s s'. s = transform s' \<and> P s \<and> P' s') P P' get get
 2. \<And>x xa. x = transform xa \<and> P x \<and> P' xa \<Longrightarrow> dcorres r (P and (=) x) (P' and (=) xa) (assert_opt (g x) >>= f) (assert_opt (g' xa) >>= f')
 3. \<lbrace>P\<rbrace> get \<lbrace>\<lambda>x. P and (=) x\<rbrace>
 4. \<lbrace>P'\<rbrace> get \<lbrace>\<lambda>x. P' and (=) x\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x xa. x = transform xa \<and> P x \<and> P' xa \<Longrightarrow> dcorres r (P and (=) x) (P' and (=) xa) (assert_opt (g x) >>= f) (assert_opt (g' xa) >>= f')
 2. \<lbrace>P\<rbrace> get \<lbrace>\<lambda>x. P and (=) x\<rbrace>
 3. \<lbrace>P'\<rbrace> get \<lbrace>\<lambda>x. P' and (=) x\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>xa. P (transform xa) \<and> P' xa \<Longrightarrow> dcorres r (P and (=) (transform xa)) (P' and (=) xa) ((case g (transform xa) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) >>= f) ((case g' xa of None \<Rightarrow> fail | Some x \<Rightarrow> return x) >>= f')
 2. \<lbrace>P\<rbrace> get \<lbrace>\<lambda>x. P and (=) x\<rbrace>
 3. \<lbrace>P'\<rbrace> get \<lbrace>\<lambda>x. P' and (=) x\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. P (transform x) \<and> P' x \<Longrightarrow> dcorres r (P and (=) (transform x)) (P' and (=) x) ((case g (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) >>= f) ((case g' x of None \<Rightarrow> fail | Some x \<Rightarrow> return x) >>= f')
 2. \<lbrace>P\<rbrace> get \<lbrace>\<lambda>x. P and (=) x\<rbrace>
 3. \<lbrace>P'\<rbrace> get \<lbrace>\<lambda>x. P' and (=) x\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>P (transform x) \<and> P' x; g' x = None\<rbrakk> \<Longrightarrow> dcorres r (P and (=) (transform x)) (P' and (=) x) ((case g (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) >>= f) ((case g' x of None \<Rightarrow> fail | Some x \<Rightarrow> return x) >>= f')
 2. \<And>x. \<lbrakk>P (transform x) \<and> P' x; g' x \<noteq> None\<rbrakk> \<Longrightarrow> dcorres r (P and (=) (transform x)) (P' and (=) x) ((case g (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) >>= f) ((case g' x of None \<Rightarrow> fail | Some x \<Rightarrow> return x) >>= f')
 3. \<lbrace>P\<rbrace> get \<lbrace>\<lambda>x. P and (=) x\<rbrace>
 4. \<lbrace>P'\<rbrace> get \<lbrace>\<lambda>x. P' and (=) x\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>P (transform x) \<and> P' x; g' x \<noteq> None\<rbrakk> \<Longrightarrow> dcorres r (P and (=) (transform x)) (P' and (=) x) ((case g (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) >>= f) ((case g' x of None \<Rightarrow> fail | Some x \<Rightarrow> return x) >>= f')
 2. \<lbrace>P\<rbrace> get \<lbrace>\<lambda>x. P and (=) x\<rbrace>
 3. \<lbrace>P'\<rbrace> get \<lbrace>\<lambda>x. P' and (=) x\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>P (transform x) \<and> P' x; g' x \<noteq> None; \<exists>obj. g (transform x) \<noteq> None\<rbrakk> \<Longrightarrow> dcorres r (P and (=) (transform x)) (P' and (=) x) ((case g (transform x) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) >>= f) ((case g' x of None \<Rightarrow> fail | Some x \<Rightarrow> return x) >>= f')
 2. \<And>x. \<lbrakk>P (transform x) \<and> P' x; g' x \<noteq> None\<rbrakk> \<Longrightarrow> \<exists>obj. g (transform x) \<noteq> None
 3. \<lbrace>P\<rbrace> get \<lbrace>\<lambda>x. P and (=) x\<rbrace>
 4. \<lbrace>P'\<rbrace> get \<lbrace>\<lambda>x. P' and (=) x\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x y ya. \<lbrakk>g' x = Some y; g (transform x) = Some ya; P (transform x); P' x\<rbrakk> \<Longrightarrow> dcorres r (P and (=) (transform x)) (P' and (=) x) (f ya) (f' y)
 2. \<And>x. \<lbrakk>P (transform x) \<and> P' x; g' x \<noteq> None\<rbrakk> \<Longrightarrow> \<exists>obj. g (transform x) \<noteq> None
 3. \<lbrace>P\<rbrace> get \<lbrace>\<lambda>x. P and (=) x\<rbrace>
 4. \<lbrace>P'\<rbrace> get \<lbrace>\<lambda>x. P' and (=) x\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x y ya. \<lbrakk>g' x = Some y; g (transform x) = Some ya; P (transform x); P' x\<rbrakk> \<Longrightarrow> dcorres r ((=) (transform x)) ((=) x) (f ya) (f' y)
 2. \<And>x y ya s. \<lbrakk>g' x = Some y; g (transform x) = Some ya; P (transform x); P' x; (P and (=) (transform x)) s\<rbrakk> \<Longrightarrow> transform x = s
 3. \<And>x y ya s. \<lbrakk>g' x = Some y; g (transform x) = Some ya; P (transform x); P' x; (P' and (=) x) s\<rbrakk> \<Longrightarrow> x = s
 4. \<And>x. \<lbrakk>P (transform x) \<and> P' x; g' x \<noteq> None\<rbrakk> \<Longrightarrow> \<exists>obj. g (transform x) \<noteq> None
 5. \<lbrace>P\<rbrace> get \<lbrace>\<lambda>x. P and (=) x\<rbrace>
 6. \<lbrace>P'\<rbrace> get \<lbrace>\<lambda>x. P' and (=) x\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>P (transform x) \<and> P' x; \<exists>y. g' x = Some y\<rbrakk> \<Longrightarrow> \<exists>y. g (transform x) = Some y
 2. \<lbrace>P\<rbrace> get \<lbrace>\<lambda>x. P and (=) x\<rbrace>
 3. \<lbrace>P'\<rbrace> get \<lbrace>\<lambda>x. P' and (=) x\<rbrace> proof (prove)
using this:
\<lbrakk>?s = transform ?s'; P ?s; P' ?s'; g' ?s' \<noteq> None\<rbrakk> \<Longrightarrow> g ?s \<noteq> None

goal (3 subgoals):
 1. \<And>x. \<lbrakk>P (transform x) \<and> P' x; \<exists>y. g' x = Some y\<rbrakk> \<Longrightarrow> \<exists>y. g (transform x) = Some y
 2. \<lbrace>P\<rbrace> get \<lbrace>\<lambda>x. P and (=) x\<rbrace>
 3. \<lbrace>P'\<rbrace> get \<lbrace>\<lambda>x. P' and (=) x\<rbrace> proof (prove)
goal:
No subgoals!