theory Prefix_Refinement

lemma is_matching_fragment_UNION:
  "(\<forall>x. x \<in> S s \<longrightarrow> is_matching_fragment sr osr rvr ctr cres s0 R s (f x))
    \<Longrightarrow> (\<forall>s' x. x \<in> S s' \<longrightarrow> prefix_closed (f x))
    \<Longrightarrow> S s \<noteq> {}
    \<Longrightarrow> is_matching_fragment sr osr rvr ctr cres s0 R s (\<lambda>s. \<Union>x \<in> S s. f x s)" apply (clarsimp simp: is_matching_fragment_def prefix_closed_UNION) apply (intro conjI impI) apply (clarsimp simp: self_closed_def split_def in_fst_snd_image_eq) apply blast apply (clarsimp simp: env_closed_def split_def in_fst_snd_image_eq) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. x \<in> S s \<longrightarrow> is_matching_fragment sr osr rvr ctr cres s0 R s (f x); \<forall>s' x. x \<in> S s' \<longrightarrow> prefix_closed (f x); S s \<noteq> {}\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr rvr ctr cres s0 R s (\<lambda>s. \<Union>x\<in>S s. f x s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. x \<in> S s \<longrightarrow> self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s (f x) \<and> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)) s (f x) \<and> f x s \<noteq> {} \<and> (\<forall>x\<in>f x s. case x of (tr, res) \<Rightarrow> rely_cond R s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr rvr res cres)); \<forall>s' x. x \<in> S s' \<longrightarrow> prefix_closed (f x); S s \<noteq> {}\<rbrakk> \<Longrightarrow> self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s (\<lambda>s. \<Union>x\<in>S s. f x s) \<and> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)) s (\<lambda>s. \<Union>x\<in>S s. f x s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x. x \<in> S s \<longrightarrow> self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s (f x) \<and> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)) s (f x) \<and> f x s \<noteq> {} \<and> (\<forall>x\<in>f x s. case x of (tr, res) \<Rightarrow> rely_cond R s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr rvr res cres)); \<forall>s' x. x \<in> S s' \<longrightarrow> prefix_closed (f x); S s \<noteq> {}\<rbrakk> \<Longrightarrow> self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s (\<lambda>s. \<Union>x\<in>S s. f x s)
 2. \<lbrakk>\<forall>x. x \<in> S s \<longrightarrow> self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s (f x) \<and> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)) s (f x) \<and> f x s \<noteq> {} \<and> (\<forall>x\<in>f x s. case x of (tr, res) \<Rightarrow> rely_cond R s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr rvr res cres)); \<forall>s' x. x \<in> S s' \<longrightarrow> prefix_closed (f x); S s \<noteq> {}\<rbrakk> \<Longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)) s (\<lambda>s. \<Union>x\<in>S s. f x s) proof (prove)
goal (2 subgoals):
 1. \<And>xs x. \<lbrakk>\<forall>x. x \<in> S s \<longrightarrow> (\<forall>xs. (xs, Incomplete) \<in> f x s \<longrightarrow> length xs < length ctr \<and> fst (rev ctr ! length xs) = Me \<longrightarrow> (\<exists>s' y. ((Me, s') # xs, y) \<in> f x s)) \<and> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)) s (f x) \<and> f x s \<noteq> {} \<and> (\<forall>x\<in>f x s. rely_cond R s0 (fst x) \<and> matching_tr_pfx sr (fst x) ctr \<and> (length (fst x) < length ctr \<longrightarrow> snd x = Incomplete) \<and> (length (fst x) = length ctr \<longrightarrow> rel_tmres osr rvr (snd x) cres)); \<forall>s' x. x \<in> S s' \<longrightarrow> prefix_closed (f x); S s \<noteq> {}; x \<in> S s; (xs, Incomplete) \<in> f x s; length xs < length ctr; fst (rev ctr ! length xs) = Me\<rbrakk> \<Longrightarrow> \<exists>s' y. \<exists>x\<in>S s. ((Me, s') # xs, y) \<in> f x s
 2. \<lbrakk>\<forall>x. x \<in> S s \<longrightarrow> self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s (f x) \<and> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)) s (f x) \<and> f x s \<noteq> {} \<and> (\<forall>x\<in>f x s. case x of (tr, res) \<Rightarrow> rely_cond R s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr rvr res cres)); \<forall>s' x. x \<in> S s' \<longrightarrow> prefix_closed (f x); S s \<noteq> {}\<rbrakk> \<Longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)) s (\<lambda>s. \<Union>x\<in>S s. f x s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. x \<in> S s \<longrightarrow> self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s (f x) \<and> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)) s (f x) \<and> f x s \<noteq> {} \<and> (\<forall>x\<in>f x s. case x of (tr, res) \<Rightarrow> rely_cond R s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr rvr res cres)); \<forall>s' x. x \<in> S s' \<longrightarrow> prefix_closed (f x); S s \<noteq> {}\<rbrakk> \<Longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond R s0 ((Env, s) # xs)) s (\<lambda>s. \<Union>x\<in>S s. f x s) proof (prove)
goal (1 subgoal):
 1. \<And>xs x s'. \<lbrakk>\<forall>x. x \<in> S s \<longrightarrow> self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s (f x) \<and> (\<forall>xs. (xs, Incomplete) \<in> f x s \<longrightarrow> (\<forall>s'. matching_tr_pfx sr ((Env, s') # xs) ctr \<and> rely_cond R s0 ((Env, s') # xs) \<longrightarrow> (\<exists>y. ((Env, s') # xs, y) \<in> f x s))) \<and> f x s \<noteq> {} \<and> (\<forall>x\<in>f x s. rely_cond R s0 (fst x) \<and> matching_tr_pfx sr (fst x) ctr \<and> (length (fst x) < length ctr \<longrightarrow> snd x = Incomplete) \<and> (length (fst x) = length ctr \<longrightarrow> rel_tmres osr rvr (snd x) cres)); \<forall>s' x. x \<in> S s' \<longrightarrow> prefix_closed (f x); S s \<noteq> {}; x \<in> S s; (xs, Incomplete) \<in> f x s; matching_tr_pfx sr ((Env, s') # xs) ctr; rely_cond R s0 ((Env, s') # xs)\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>x\<in>S s. ((Env, s') # xs, y) \<in> f x s proof (prove)
goal:
No subgoals!