theory ADT_IF_Refine

lemma step_corres_lift'''':
  "\<lbrakk> \<And>tc. corres_underlying srel False nf (=) (\<lambda>s. ((tc,s),mode) \<in> P)
                             (\<lambda>s'. ((tc,s'),mode) \<in> P') (f tc) (f' tc);
     \<And>tc. nf \<Longrightarrow> empty_fail (f' tc);
     \<And>tc s s'. (s,s') \<in> srel \<Longrightarrow> S' s' \<Longrightarrow> S s \<Longrightarrow> y s = y' s';
     \<And>tc. \<lbrace>\<lambda>s'. ((tc,s'),mode) \<in> P'\<rbrace> (f' tc) \<lbrace>\<lambda>_. S'\<rbrace>;
     \<And>tc. \<lbrace>\<lambda>s'. ((tc,s'),mode) \<in> P\<rbrace> (f tc) \<lbrace>\<lambda>_. S\<rbrace> \<rbrakk>
     \<Longrightarrow> step_corres nf (lift_snd_rel srel) mode P P'
           {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> f x xa) \<and> m = (y (snd s'))}
           {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> f' x xa) \<and> m = (y' (snd s'))}" apply (clarsimp simp: corres_underlying_def step_corres_def lift_snd_rel_def empty_fail_def) apply (clarsimp simp: valid_def) apply (drule_tac x=a in meta_spec)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>tc. corres_underlying srel False nf (=) (\<lambda>s. ((tc, s), mode) \<in> P) (\<lambda>s'. ((tc, s'), mode) \<in> P') (f tc) (f' tc); \<And>tc. nf \<Longrightarrow> empty_fail (f' tc); \<And>tc s s'. \<lbrakk>(s, s') \<in> srel; S' s'; S s\<rbrakk> \<Longrightarrow> y s = y' s'; \<And>tc. \<lbrace>\<lambda>s'. ((tc, s'), mode) \<in> P'\<rbrace> f' tc \<lbrace>\<lambda>_. S'\<rbrace>; \<And>tc. \<lbrace>\<lambda>s'. ((tc, s'), mode) \<in> P\<rbrace> f tc \<lbrace>\<lambda>_. S\<rbrace>\<rbrakk> \<Longrightarrow> step_corres nf (lift_snd_rel srel) mode P P' {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> f x xa) \<and> m = y (snd s')} {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> f' x xa) \<and> m = y' (snd s')} proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. \<lbrakk>\<And>tc. \<forall>x\<in>srel. case x of (s, s') \<Rightarrow> ((tc, s), mode) \<in> P \<and> ((tc, s'), mode) \<in> P' \<longrightarrow> (\<forall>x\<in>fst (f' tc s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f tc s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> r = r') \<and> (nf \<longrightarrow> \<not> snd (f' tc s')); \<And>tc. nf \<Longrightarrow> \<forall>s. fst (f' tc s) = {} \<longrightarrow> snd (f' tc s); \<And>s s'. \<lbrakk>(s, s') \<in> srel; S' s'; S s\<rbrakk> \<Longrightarrow> y s = y' s'; \<And>tc. \<lbrace>\<lambda>s'. ((tc, s'), mode) \<in> P'\<rbrace> f' tc \<lbrace>\<lambda>_. S'\<rbrace>; \<And>tc. \<lbrace>\<lambda>s'. ((tc, s'), mode) \<in> P\<rbrace> f tc \<lbrace>\<lambda>_. S\<rbrace>; (b, ba) \<in> srel; ((a, ba), mode) \<in> P'; ((a, b), mode) \<in> P\<rbrakk> \<Longrightarrow> (nf \<longrightarrow> (\<exists>aa b. (aa, b) \<in> fst (f' a ba))) \<and> (\<forall>aa bb. (aa, bb) \<in> fst (f' a ba) \<longrightarrow> (\<exists>ba. (aa, ba) \<in> fst (f a b) \<and> y' bb = y ba \<and> (ba, bb) \<in> srel)) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. \<lbrakk>\<And>tc. \<forall>x\<in>srel. case x of (s, s') \<Rightarrow> ((tc, s), mode) \<in> P \<and> ((tc, s'), mode) \<in> P' \<longrightarrow> (\<forall>x\<in>fst (f' tc s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f tc s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> r = r') \<and> (nf \<longrightarrow> \<not> snd (f' tc s')); \<And>tc. nf \<Longrightarrow> \<forall>s. fst (f' tc s) = {} \<longrightarrow> snd (f' tc s); \<And>s s'. \<lbrakk>(s, s') \<in> srel; S' s'; S s\<rbrakk> \<Longrightarrow> y s = y' s'; \<And>tc. \<forall>s. ((tc, s), mode) \<in> P' \<longrightarrow> (\<forall>x\<in>fst (f' tc s). case x of (r, s') \<Rightarrow> S' s'); \<And>tc. \<forall>s. ((tc, s), mode) \<in> P \<longrightarrow> (\<forall>x\<in>fst (f tc s). case x of (r, s') \<Rightarrow> S s'); (b, ba) \<in> srel; ((a, ba), mode) \<in> P'; ((a, b), mode) \<in> P\<rbrakk> \<Longrightarrow> (nf \<longrightarrow> (\<exists>aa b. (aa, b) \<in> fst (f' a ba))) \<and> (\<forall>aa bb. (aa, bb) \<in> fst (f' a ba) \<longrightarrow> (\<exists>ba. (aa, ba) \<in> fst (f a b) \<and> y' bb = y ba \<and> (ba, bb) \<in> srel)) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. \<lbrakk>\<And>s s'. \<lbrakk>(s, s') \<in> srel; S' s'; S s\<rbrakk> \<Longrightarrow> y s = y' s'; (b, ba) \<in> srel; ((a, ba), mode) \<in> P'; ((a, b), mode) \<in> P; \<forall>x\<in>srel. case x of (s, s') \<Rightarrow> ((a, s), mode) \<in> P \<and> ((a, s'), mode) \<in> P' \<longrightarrow> (\<forall>x\<in>fst (f' a s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> r = r') \<and> (nf \<longrightarrow> \<not> snd (f' a s')); nf \<Longrightarrow> \<forall>s. fst (f' a s) = {} \<longrightarrow> snd (f' a s); \<forall>s. ((a, s), mode) \<in> P' \<longrightarrow> (\<forall>x\<in>fst (f' a s). case x of (r, s') \<Rightarrow> S' s'); \<forall>s. ((a, s), mode) \<in> P \<longrightarrow> (\<forall>x\<in>fst (f a s). case x of (r, s') \<Rightarrow> S s')\<rbrakk> \<Longrightarrow> (nf \<longrightarrow> (\<exists>aa b. (aa, b) \<in> fst (f' a ba))) \<and> (\<forall>aa bb. (aa, bb) \<in> fst (f' a ba) \<longrightarrow> (\<exists>ba. (aa, ba) \<in> fst (f a b) \<and> y' bb = y ba \<and> (ba, bb) \<in> srel)) proof (prove)
goal:
No subgoals!