theory Finalise_R

lemma corres_gets_lift:
  assumes inv: "\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>"
  assumes res: "\<lbrace>Q'\<rbrace> g \<lbrace>\<lambda>r s. r = g' s\<rbrace>"
  assumes Q: "\<And>s. Q s \<Longrightarrow> Q' s"
  assumes nf: "no_fail Q g"
  shows "corres r P Q f (gets g') \<Longrightarrow> corres r P Q f g" apply (clarsimp simp add: corres_underlying_def simpler_gets_def) apply (drule (1) bspec) apply (rule conjI) apply clarsimp apply (rule bexI) prefer 2 apply assumption apply simp apply (frule in_inv_by_hoareD [OF inv]) apply simp apply (drule use_valid, rule res) apply (erule Q) apply simp apply (insert nf) apply (clarsimp simp: no_fail_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres r P Q f (gets g') \<Longrightarrow> corres r P Q f g proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>state_relation. case x of (s, s') \<Rightarrow> P s \<and> Q s' \<longrightarrow> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, s') \<in> state_relation \<and> r ra (g' s')); (a, b) \<in> state_relation; P a; Q b\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, t') \<in> state_relation \<and> r ra r') \<and> \<not> snd (g b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; case (a, b) of (s, s') \<Rightarrow> P s \<and> Q s' \<longrightarrow> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, s') \<in> state_relation \<and> r ra (g' s'))\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, t') \<in> state_relation \<and> r ra r') \<and> \<not> snd (g b) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; case (a, b) of (s, s') \<Rightarrow> P s \<and> Q s' \<longrightarrow> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, s') \<in> state_relation \<and> r ra (g' s'))\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, t') \<in> state_relation \<and> r ra r'
 2. \<And>a b. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; case (a, b) of (s, s') \<Rightarrow> P s \<and> Q s' \<longrightarrow> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, s') \<in> state_relation \<and> r ra (g' s'))\<rbrakk> \<Longrightarrow> \<not> snd (g b) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; (aa, ba) \<in> fst (f a); (ab, bb) \<in> fst (g b); (ba, b) \<in> state_relation; r aa (g' b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, bb) \<in> state_relation \<and> r ra ab
 2. \<And>a b. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; case (a, b) of (s, s') \<Rightarrow> P s \<and> Q s' \<longrightarrow> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, s') \<in> state_relation \<and> r ra (g' s'))\<rbrakk> \<Longrightarrow> \<not> snd (g b) proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; (aa, ba) \<in> fst (f a); (ab, bb) \<in> fst (g b); (ba, b) \<in> state_relation; r aa (g' b)\<rbrakk> \<Longrightarrow> case ?x38 a b aa ba ab bb of (ra, t) \<Rightarrow> (t, bb) \<in> state_relation \<and> r ra ab
 2. \<And>a b aa ba ab bb. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; (aa, ba) \<in> fst (f a); (ab, bb) \<in> fst (g b); (ba, b) \<in> state_relation; r aa (g' b)\<rbrakk> \<Longrightarrow> ?x38 a b aa ba ab bb \<in> fst (f a)
 3. \<And>a b. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; case (a, b) of (s, s') \<Rightarrow> P s \<and> Q s' \<longrightarrow> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, s') \<in> state_relation \<and> r ra (g' s'))\<rbrakk> \<Longrightarrow> \<not> snd (g b) proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; (aa, ba) \<in> fst (f a); (ab, bb) \<in> fst (g b); (ba, b) \<in> state_relation; r aa (g' b)\<rbrakk> \<Longrightarrow> ?x38 a b aa ba ab bb \<in> fst (f a)
 2. \<And>a b aa ba ab bb. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; (aa, ba) \<in> fst (f a); (ab, bb) \<in> fst (g b); (ba, b) \<in> state_relation; r aa (g' b)\<rbrakk> \<Longrightarrow> case ?x38 a b aa ba ab bb of (ra, t) \<Rightarrow> (t, bb) \<in> state_relation \<and> r ra ab
 3. \<And>a b. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; case (a, b) of (s, s') \<Rightarrow> P s \<and> Q s' \<longrightarrow> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, s') \<in> state_relation \<and> r ra (g' s'))\<rbrakk> \<Longrightarrow> \<not> snd (g b) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; (aa, ba) \<in> fst (f a); (ab, bb) \<in> fst (g b); (ba, b) \<in> state_relation; r aa (g' b)\<rbrakk> \<Longrightarrow> case (aa, ba) of (ra, t) \<Rightarrow> (t, bb) \<in> state_relation \<and> r ra ab
 2. \<And>a b. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; case (a, b) of (s, s') \<Rightarrow> P s \<and> Q s' \<longrightarrow> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, s') \<in> state_relation \<and> r ra (g' s'))\<rbrakk> \<Longrightarrow> \<not> snd (g b) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; (aa, ba) \<in> fst (f a); (ab, bb) \<in> fst (g b); (ba, b) \<in> state_relation; r aa (g' b)\<rbrakk> \<Longrightarrow> (ba, bb) \<in> state_relation \<and> r aa ab
 2. \<And>a b. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; case (a, b) of (s, s') \<Rightarrow> P s \<and> Q s' \<longrightarrow> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, s') \<in> state_relation \<and> r ra (g' s'))\<rbrakk> \<Longrightarrow> \<not> snd (g b) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; (aa, ba) \<in> fst (f a); (ab, bb) \<in> fst (g b); (ba, b) \<in> state_relation; r aa (g' b); bb = b\<rbrakk> \<Longrightarrow> (ba, bb) \<in> state_relation \<and> r aa ab
 2. \<And>a b. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; case (a, b) of (s, s') \<Rightarrow> P s \<and> Q s' \<longrightarrow> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, s') \<in> state_relation \<and> r ra (g' s'))\<rbrakk> \<Longrightarrow> \<not> snd (g b) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; (aa, ba) \<in> fst (f a); (ab, b) \<in> fst (g b); (ba, b) \<in> state_relation; r aa (g' b); bb = b\<rbrakk> \<Longrightarrow> r aa ab
 2. \<And>a b. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; case (a, b) of (s, s') \<Rightarrow> P s \<and> Q s' \<longrightarrow> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, s') \<in> state_relation \<and> r ra (g' s'))\<rbrakk> \<Longrightarrow> \<not> snd (g b) proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; (aa, ba) \<in> fst (f a); (ba, b) \<in> state_relation; r aa (g' b); bb = b\<rbrakk> \<Longrightarrow> Q' b
 2. \<And>a b aa ba ab bb. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; (aa, ba) \<in> fst (f a); (ba, b) \<in> state_relation; r aa (g' b); bb = b; ab = g' b\<rbrakk> \<Longrightarrow> r aa ab
 3. \<And>a b. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; case (a, b) of (s, s') \<Rightarrow> P s \<and> Q s' \<longrightarrow> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, s') \<in> state_relation \<and> r ra (g' s'))\<rbrakk> \<Longrightarrow> \<not> snd (g b) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; (aa, ba) \<in> fst (f a); (ba, b) \<in> state_relation; r aa (g' b); bb = b; ab = g' b\<rbrakk> \<Longrightarrow> r aa ab
 2. \<And>a b. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; case (a, b) of (s, s') \<Rightarrow> P s \<and> Q s' \<longrightarrow> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, s') \<in> state_relation \<and> r ra (g' s'))\<rbrakk> \<Longrightarrow> \<not> snd (g b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; case (a, b) of (s, s') \<Rightarrow> P s \<and> Q s' \<longrightarrow> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, s') \<in> state_relation \<and> r ra (g' s'))\<rbrakk> \<Longrightarrow> \<not> snd (g b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> state_relation; P a; Q b; case (a, b) of (s, s') \<Rightarrow> P s \<and> Q s' \<longrightarrow> (\<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, s') \<in> state_relation \<and> r ra (g' s')); no_fail Q g\<rbrakk> \<Longrightarrow> \<not> snd (g b) proof (prove)
goal:
No subgoals!