theory AutoCorres_C

lemma corres_to_ccorres_extra_globals:
  assumes rf_sr_def: "rf_sr \<equiv> {(s,s'). cstate_relation s (globals s')}"
  assumes acc: "ac_corres globals check_term \<Gamma> ret_xf G (liftE ac) c"
  assumes cac: "corres_underlying {(s,s'). cstate_relation s s'} True True
                                  R P Q a (do x \<leftarrow> ac; y \<leftarrow> gets g; return (x,y) od)"
  assumes pre: "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> P s \<and> Q (globals s')"
  assumes p_g: "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> G s'"
  assumes ret: "\<And>r s'. R r (ret_xf s', g (globals s')) \<longrightarrow> R' r (ret_xf' s')"
  shows "ccorresG rf_sr \<Gamma> R' ret_xf' P' Q' [] a c" unfolding rf_sr_def using ac_corres_ccorres_underlying[OF acc] apply (clarsimp intro!: ccorresI') apply (frule corres_underlyingD[OF cac, simplified], (simp add: pre)+) apply (clarsimp simp: bind_def return_def simpler_gets_def) apply (erule ccorresE, simp+, erule p_g, simp+) apply (simp add: liftE_def) apply assumption apply (fastforce simp: unif_rrel_def dest: mp[OF ret] split: xstate.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorresG rf_sr \<Gamma> R' ret_xf' P' Q' [] a c proof (prove)
goal (1 subgoal):
 1. ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> R' ret_xf' P' Q' [] a c proof (prove)
using this:
ccorres_underlying {(a, b). a = globals b} \<Gamma> ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = ret_xf s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = ret_xf s)) Inr (\<lambda>_. True) (Collect G) [] (liftE ac) c

goal (1 subgoal):
 1. ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> R' ret_xf' P' Q' [] a c proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>ccorres_underlying {(a, b). a = globals b} \<Gamma> ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = ret_xf s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = ret_xf s)) Inr (\<lambda>_. True) (Collect G) [] (liftE ac) c; P' s; s' \<in> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>[c],s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); cstate_relation s (globals s')\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> cstate_relation t (globals t') \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' r t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>ccorres_underlying {(a, b). a = globals b} \<Gamma> ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = ret_xf s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = ret_xf s)) Inr (\<lambda>_. True) (Collect G) [] (liftE ac) c; P' s; s' \<in> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>[c],s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); cstate_relation s (globals s'); (\<forall>x\<in>fst ((do x <- ac;
y <- gets g;
return (x, y)
od) (globals s')). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> cstate_relation t t' \<and> R r r') \<and> \<not> snd ((do x <- ac;
y <- gets g;
return (x, y)
od) (globals s'))\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> cstate_relation t (globals t') \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' r t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>ccorres_underlying {(a, b). a = globals b} \<Gamma> ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = ret_xf s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = ret_xf s)) Inr (\<lambda>_. True) (Collect G) [] (liftE ac) c; P' s; s' \<in> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>[c],s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); cstate_relation s (globals s'); \<forall>y\<in>fst (ac (globals s')). \<forall>x\<in>fst (case y of (x, s) \<Rightarrow> ({((x, g s), s)}, False)). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> cstate_relation t t' \<and> R r r'; \<forall>x\<in>fst (ac (globals s')). \<not> snd (case x of (x, s) \<Rightarrow> ({((x, g s), s)}, False)); \<not> snd (ac (globals s'))\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> cstate_relation t (globals t') \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' r t') proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z. \<lbrakk>P' s; s' \<in> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>[c],s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); cstate_relation s (globals s'); \<forall>y\<in>fst (ac (globals s')). \<forall>x\<in>fst (case y of (x, s) \<Rightarrow> ({((x, g s), s)}, False)). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> cstate_relation t t' \<and> R r r'; \<forall>x\<in>fst (ac (globals s')). \<not> snd (case x of (x, s) \<Rightarrow> ({((x, g s), s)}, False)); \<not> snd (ac (globals s'))\<rbrakk> \<Longrightarrow> \<not> snd (liftE ac (globals s'))
 2. \<And>s s' n z. \<lbrakk>P' s; s' \<in> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>[c],s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); cstate_relation s (globals s'); \<forall>y\<in>fst (ac (globals s')). \<forall>x\<in>fst (case y of (x, s) \<Rightarrow> ({((x, g s), s)}, False)). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> cstate_relation t t' \<and> R r r'; \<forall>x\<in>fst (ac (globals s')). \<not> snd (case x of (x, s) \<Rightarrow> ({((x, g s), s)}, False)); \<not> snd (ac (globals s'))\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>[c],s'\<rangle> \<Rightarrow> (?n29 s s' n z, ?x29 s s' n z)
 3. \<And>s s' n z t' r t. \<lbrakk>P' s; s' \<in> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>[c],s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); cstate_relation s (globals s'); \<forall>y\<in>fst (ac (globals s')). \<forall>x\<in>fst (case y of (x, s) \<Rightarrow> ({((x, g s), s)}, False)). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> cstate_relation t t' \<and> R r r'; \<forall>x\<in>fst (ac (globals s')). \<not> snd (case x of (x, s) \<Rightarrow> ({((x, g s), s)}, False)); \<not> snd (ac (globals s')); ?x29 s s' n z = Normal t'; (r, t) \<in> fst (liftE ac (globals s')); (t, t') \<in> {(a, b). a = globals b}; unif_rrel (?n29 s s' n z = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = ret_xf s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = ret_xf s)) Inr r t'; ?n29 s s' n z \<le> length []\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> cstate_relation t (globals t') \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' r t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z. \<lbrakk>P' s; s' \<in> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>[c],s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); cstate_relation s (globals s'); \<forall>y\<in>fst (ac (globals s')). \<forall>x\<in>fst (case y of (x, s) \<Rightarrow> ({((x, g s), s)}, False)). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> cstate_relation t t' \<and> R r r'; \<forall>x\<in>fst (ac (globals s')). \<not> snd (case x of (x, s) \<Rightarrow> ({((x, g s), s)}, False)); \<not> snd (ac (globals s'))\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>[c],s'\<rangle> \<Rightarrow> (?n29 s s' n z, ?x29 s s' n z)
 2. \<And>s s' n z t' r t. \<lbrakk>P' s; s' \<in> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>[c],s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); cstate_relation s (globals s'); \<forall>y\<in>fst (ac (globals s')). \<forall>x\<in>fst (case y of (x, s) \<Rightarrow> ({((x, g s), s)}, False)). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> cstate_relation t t' \<and> R r r'; \<forall>x\<in>fst (ac (globals s')). \<not> snd (case x of (x, s) \<Rightarrow> ({((x, g s), s)}, False)); \<not> snd (ac (globals s')); ?x29 s s' n z = Normal t'; (r, t) \<in> fst (liftE ac (globals s')); (t, t') \<in> {(a, b). a = globals b}; unif_rrel (?n29 s s' n z = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = ret_xf s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = ret_xf s)) Inr r t'; ?n29 s s' n z \<le> length []\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> cstate_relation t (globals t') \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' r t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t' r t. \<lbrakk>P' s; s' \<in> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>[c],s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); cstate_relation s (globals s'); \<forall>y\<in>fst (ac (globals s')). \<forall>x\<in>fst (case y of (x, s) \<Rightarrow> ({((x, g s), s)}, False)). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> cstate_relation t t' \<and> R r r'; \<forall>x\<in>fst (ac (globals s')). \<not> snd (case x of (x, s) \<Rightarrow> ({((x, g s), s)}, False)); \<not> snd (ac (globals s')); z = Normal t'; (r, t) \<in> fst (liftE ac (globals s')); (t, t') \<in> {(a, b). a = globals b}; unif_rrel (n = length []) ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = ret_xf s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = ret_xf s)) Inr r t'; n \<le> length []\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> cstate_relation t (globals t') \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' r t') proof (prove)
goal:
No subgoals!