theory Prefix_Refinement

lemma prefix_closed_mbind:
  "prefix_closed f
    \<Longrightarrow> \<forall>tr x s' s. (tr, Result (x, s')) \<in> f s \<longrightarrow> prefix_closed (g (last_st_tr tr s0) x)
   \<Longrightarrow> prefix_closed (mbind f g s0)" apply (subst prefix_closed_def, clarsimp simp: mbind_def) apply (split tmres.split_asm; clarsimp;
        (drule(1) prefix_closedD, fastforce elim: rev_bexI)?) apply (simp add: Cons_eq_append_conv, safe) apply (drule(1) prefix_closedD) apply (fastforce elim: rev_bexI) apply (drule spec2, drule mp, blast) apply (erule rev_bexI, clarsimp) apply (drule(1) prefix_closedD) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed f; \<forall>tr x s' s. (tr, Result (x, s')) \<in> f s \<longrightarrow> prefix_closed (g (last_st_tr tr s0) x)\<rbrakk> \<Longrightarrow> prefix_closed (mbind f g s0) proof (prove)
goal (1 subgoal):
 1. \<And>s a b xs ba ab bb. \<lbrakk>prefix_closed f; \<forall>tr x. (\<exists>s' s. (tr, Result (x, s')) \<in> f s) \<longrightarrow> prefix_closed (g (last_st_tr tr s0) x); (ab, bb) \<in> f s; ((a, b) # xs, ba) \<in> (case bb of Failed \<Rightarrow> {(ab, Failed)} | Incomplete \<Rightarrow> {(ab, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ ab, y)) ` g (last_st_tr ab s0) rv s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>f s. (xs, Incomplete) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (1 subgoal):
 1. \<And>s a b xs ab aa bc ac bd. \<lbrakk>prefix_closed f; \<forall>tr x. (\<exists>s' s. (tr, Result (x, s')) \<in> f s) \<longrightarrow> prefix_closed (g (last_st_tr tr s0) x); (ab, Result (aa, bc)) \<in> f s; (ac, bd) \<in> g (last_st_tr ab s0) aa bc; (a, b) # xs = ac @ ab\<rbrakk> \<Longrightarrow> \<exists>x\<in>f s. (xs, Incomplete) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (2 subgoals):
 1. \<And>s a b xs ab aa bc ac bd. \<lbrakk>prefix_closed f; \<forall>tr x. (\<exists>s' s. (tr, Result (x, s')) \<in> f s) \<longrightarrow> prefix_closed (g (last_st_tr tr s0) x); ((a, b) # xs, Result (aa, bc)) \<in> f s; ([], bd) \<in> g (last_st_tr ((a, b) # xs) s0) aa bc\<rbrakk> \<Longrightarrow> \<exists>x\<in>f s. (xs, Incomplete) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s)
 2. \<And>s a b xs ab aa bc ac bd ys'. \<lbrakk>prefix_closed f; \<forall>tr x. (\<exists>s' s. (tr, Result (x, s')) \<in> f s) \<longrightarrow> prefix_closed (g (last_st_tr tr s0) x); (ab, Result (aa, bc)) \<in> f s; ((a, b) # ys', bd) \<in> g (last_st_tr ab s0) aa bc\<rbrakk> \<Longrightarrow> \<exists>x\<in>f s. (ys' @ ab, Incomplete) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (2 subgoals):
 1. \<And>s a b xs ab aa bc ac bd. \<lbrakk>\<forall>tr x. (\<exists>s' s. (tr, Result (x, s')) \<in> f s) \<longrightarrow> prefix_closed (g (last_st_tr tr s0) x); ((a, b) # xs, Result (aa, bc)) \<in> f s; ([], bd) \<in> g (last_st_tr ((a, b) # xs) s0) aa bc; (xs, Incomplete) \<in> f s\<rbrakk> \<Longrightarrow> \<exists>x\<in>f s. (xs, Incomplete) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s)
 2. \<And>s a b xs ab aa bc ac bd ys'. \<lbrakk>prefix_closed f; \<forall>tr x. (\<exists>s' s. (tr, Result (x, s')) \<in> f s) \<longrightarrow> prefix_closed (g (last_st_tr tr s0) x); (ab, Result (aa, bc)) \<in> f s; ((a, b) # ys', bd) \<in> g (last_st_tr ab s0) aa bc\<rbrakk> \<Longrightarrow> \<exists>x\<in>f s. (ys' @ ab, Incomplete) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (1 subgoal):
 1. \<And>s a b xs ab aa bc ac bd ys'. \<lbrakk>prefix_closed f; \<forall>tr x. (\<exists>s' s. (tr, Result (x, s')) \<in> f s) \<longrightarrow> prefix_closed (g (last_st_tr tr s0) x); (ab, Result (aa, bc)) \<in> f s; ((a, b) # ys', bd) \<in> g (last_st_tr ab s0) aa bc\<rbrakk> \<Longrightarrow> \<exists>x\<in>f s. (ys' @ ab, Incomplete) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (1 subgoal):
 1. \<And>s a b xs ab aa bc ac bd ys'. \<lbrakk>prefix_closed f; (ab, Result (aa, bc)) \<in> f s; ((a, b) # ys', bd) \<in> g (last_st_tr ab s0) aa bc; prefix_closed (g (last_st_tr ab s0) aa)\<rbrakk> \<Longrightarrow> \<exists>x\<in>f s. (ys' @ ab, Incomplete) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g (last_st_tr xs s0) rv s) proof (prove)
goal (1 subgoal):
 1. \<And>a b ab aa bc bd ys'. \<lbrakk>prefix_closed f; ((a, b) # ys', bd) \<in> g (last_st_tr ab s0) aa bc; prefix_closed (g (last_st_tr ab s0) aa)\<rbrakk> \<Longrightarrow> (ys' @ ab, Incomplete) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ ab, x)) ` g (last_st_tr ab s0) aa bc proof (prove)
goal (1 subgoal):
 1. \<And>a b ab aa bc bd ys'. \<lbrakk>prefix_closed f; ((a, b) # ys', bd) \<in> g (last_st_tr ab s0) aa bc; (ys', Incomplete) \<in> g (last_st_tr ab s0) aa bc\<rbrakk> \<Longrightarrow> (ys' @ ab, Incomplete) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ ab, x)) ` g (last_st_tr ab s0) aa bc proof (prove)
goal:
No subgoals!