theory Trace_Sat

lemma exs_valid_bind[wp_split]:
  "\<lbrakk> \<And>rv. \<lbrace>B rv\<rbrace> g rv \<exists>\<lbrace>C\<rbrace>; \<lbrace>A\<rbrace> f \<exists>\<lbrace>B\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>= (\<lambda>rv. g rv) \<exists>\<lbrace>C\<rbrace>" apply atomize apply (clarsimp simp: exs_valid_def bind_def' mres_def) apply (drule spec, drule(1) mp, clarsimp) apply (drule spec2, drule(1) mp, clarsimp) apply (simp add: image_def bex_Un) apply (strengthen subst[where P="\<lambda>x. x \<in> f s" for s, mk_strg I _ E], simp) apply (fastforce elim: rev_bexI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. \<lbrace>B rv\<rbrace> g rv \<exists>\<lbrace>C\<rbrace>; \<lbrace>A\<rbrace> f \<exists>\<lbrace>B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>= g \<exists>\<lbrace>C\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>rv. \<lbrace>B rv\<rbrace> g rv \<exists>\<lbrace>C\<rbrace>; \<lbrace>A\<rbrace> f \<exists>\<lbrace>B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>= g \<exists>\<lbrace>C\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>rv s. B rv s \<longrightarrow> (\<exists>x\<in>Result -` snd ` g rv s. case x of (rv, s') \<Rightarrow> C rv s'); \<forall>s. A s \<longrightarrow> (\<exists>x\<in>Result -` snd ` f s. case x of (rv, s') \<Rightarrow> B rv s'); A s\<rbrakk> \<Longrightarrow> \<exists>x\<in>Result -` snd ` ((\<lambda>xs. (xs, Failed)) ` {xs. (xs, Failed) \<in> f s} \<union> (\<lambda>xs. (xs, Incomplete)) ` {xs. (xs, Incomplete) \<in> f s} \<union> (\<Union>x\<in>{(xs, rv, s'). (xs, Result (rv, s')) \<in> f s}. case x of (xs, rv, s) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g rv s)). case x of (rv, s') \<Rightarrow> C rv s' proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa. \<lbrakk>\<forall>rv s. B rv s \<longrightarrow> (\<exists>x\<in>Result -` snd ` g rv s. case x of (x, xa) \<Rightarrow> C x xa); A s; B a b; (aa, Result (a, b)) \<in> f s\<rbrakk> \<Longrightarrow> \<exists>x\<in>Result -` snd ` ((\<lambda>xs. (xs, Failed)) ` {xs. (xs, Failed) \<in> f s} \<union> (\<lambda>xs. (xs, Incomplete)) ` {xs. (xs, Incomplete) \<in> f s} \<union> (\<Union>x\<in>{(xs, rv, s'). (xs, Result (rv, s')) \<in> f s}. case x of (xs, rv, s) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g rv s)). case x of (x, xa) \<Rightarrow> C x xa proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa ab ba ac. \<lbrakk>A s; B a b; (aa, Result (a, b)) \<in> f s; C ab ba; (ac, Result (ab, ba)) \<in> g a b\<rbrakk> \<Longrightarrow> \<exists>x\<in>Result -` snd ` ((\<lambda>xs. (xs, Failed)) ` {xs. (xs, Failed) \<in> f s} \<union> (\<lambda>xs. (xs, Incomplete)) ` {xs. (xs, Incomplete) \<in> f s} \<union> (\<Union>x\<in>{(xs, rv, s'). (xs, Result (rv, s')) \<in> f s}. case x of (xs, rv, s) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g rv s)). case x of (x, xa) \<Rightarrow> C x xa proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa ab ba ac. \<lbrakk>A s; B a b; (aa, Result (a, b)) \<in> f s; C ab ba; (ac, Result (ab, ba)) \<in> g a b\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>y. (\<exists>a aa b. (a, Result (aa, b)) \<in> f s \<and> y = {y. \<exists>x\<in>g aa b. y = (case x of (aa, x) \<Rightarrow> (aa @ a, x))}) \<and> (\<exists>x\<in>y. Result (a, b) = snd x)) \<and> C a b proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa ab ba ac. \<lbrakk>A s; B a b; (aa, Result (a, b)) \<in> f s; C ab ba; (ac, Result (ab, ba)) \<in> g a b\<rbrakk> \<Longrightarrow> \<exists>x xa. (\<exists>ab. \<exists>xb\<in>g a b. (ab, Result (x, xa)) = (case xb of (a, x) \<Rightarrow> (a @ aa, x))) \<and> C x xa proof (prove)
goal:
No subgoals!