theory Prefix_Refinement

lemma is_matching_fragment_mbind_union:
  "is_matching_fragment sr intsr rvr ctr cres s0 R s f_a
    \<Longrightarrow> ctr'' = ctr' @ ctr
    \<Longrightarrow> cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | _ \<Rightarrow> cres')
    \<Longrightarrow> cres = Incomplete \<or> cres = Failed \<longrightarrow> ctr' = []
    \<Longrightarrow> \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s
        \<longrightarrow> (\<exists>f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f
                \<and> triv_refinement (aprog x) f)
    \<Longrightarrow> is_matching_fragment sr osr rvr' ctr'' cres'' s0 R s
        (mbind f_a (\<lambda>s0' rv s. \<Union>f \<in> {f. is_matching_fragment sr osr rvr' ctr' cres' s0' R s f
                    \<and> triv_refinement (aprog rv) f}. f s) s0)" apply (rule is_matching_fragment_mbind; assumption?) apply clarsimp apply (rule is_matching_fragment_UNION) apply clarsimp apply (clarsimp simp: is_matching_fragment_prefix_closed) apply clarsimp apply clarsimp apply (rule prefix_closed_UNION) apply (clarsimp simp: is_matching_fragment_prefix_closed) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<or> cres = Failed \<longrightarrow> ctr' = []; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> (\<exists>f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f \<and> triv_refinement (aprog x) f)\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr rvr' ctr'' cres'' s0 R s (mbind f_a (\<lambda>s0' rv s. \<Union>f\<in>{f. is_matching_fragment sr osr rvr' ctr' cres' s0' R s f \<and> triv_refinement (aprog rv) f}. f s) s0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<or> cres = Failed \<longrightarrow> ctr' = []; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> (\<exists>f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f \<and> triv_refinement (aprog x) f)\<rbrakk> \<Longrightarrow> \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (\<lambda>s. \<Union>f\<in>{f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s f \<and> triv_refinement (aprog x) f}. f s)
 2. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<or> cres = Failed \<longrightarrow> ctr' = []; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> (\<exists>f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f \<and> triv_refinement (aprog x) f)\<rbrakk> \<Longrightarrow> \<forall>s0' x. prefix_closed (\<lambda>s. \<Union>f\<in>{f. is_matching_fragment sr osr rvr' ctr' cres' s0' R s f \<and> triv_refinement (aprog x) f}. f s) proof (prove)
goal (2 subgoals):
 1. \<And>tr x s'. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> (\<exists>f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f \<and> triv_refinement (aprog x) f); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; (tr, Result (x, s')) \<in> f_a s\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (\<lambda>s. \<Union>f\<in>{f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s f \<and> triv_refinement (aprog x) f}. f s)
 2. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<or> cres = Failed \<longrightarrow> ctr' = []; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> (\<exists>f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f \<and> triv_refinement (aprog x) f)\<rbrakk> \<Longrightarrow> \<forall>s0' x. prefix_closed (\<lambda>s. \<Union>f\<in>{f. is_matching_fragment sr osr rvr' ctr' cres' s0' R s f \<and> triv_refinement (aprog x) f}. f s) proof (prove)
goal (4 subgoals):
 1. \<And>tr x s'. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> (\<exists>f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f \<and> triv_refinement (aprog x) f); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; (tr, Result (x, s')) \<in> f_a s\<rbrakk> \<Longrightarrow> \<forall>f. f \<in> {f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f \<and> triv_refinement (aprog x) f} \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f
 2. \<And>tr x s'. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> (\<exists>f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f \<and> triv_refinement (aprog x) f); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; (tr, Result (x, s')) \<in> f_a s\<rbrakk> \<Longrightarrow> \<forall>s' f. f \<in> {f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f \<and> triv_refinement (aprog x) f} \<longrightarrow> prefix_closed f
 3. \<And>tr x s'. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> (\<exists>f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f \<and> triv_refinement (aprog x) f); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; (tr, Result (x, s')) \<in> f_a s\<rbrakk> \<Longrightarrow> {f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f \<and> triv_refinement (aprog x) f} \<noteq> {}
 4. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<or> cres = Failed \<longrightarrow> ctr' = []; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> (\<exists>f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f \<and> triv_refinement (aprog x) f)\<rbrakk> \<Longrightarrow> \<forall>s0' x. prefix_closed (\<lambda>s. \<Union>f\<in>{f. is_matching_fragment sr osr rvr' ctr' cres' s0' R s f \<and> triv_refinement (aprog x) f}. f s) proof (prove)
goal (3 subgoals):
 1. \<And>tr x s'. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> (\<exists>f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f \<and> triv_refinement (aprog x) f); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; (tr, Result (x, s')) \<in> f_a s\<rbrakk> \<Longrightarrow> \<forall>s' f. f \<in> {f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f \<and> triv_refinement (aprog x) f} \<longrightarrow> prefix_closed f
 2. \<And>tr x s'. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> (\<exists>f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f \<and> triv_refinement (aprog x) f); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; (tr, Result (x, s')) \<in> f_a s\<rbrakk> \<Longrightarrow> {f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f \<and> triv_refinement (aprog x) f} \<noteq> {}
 3. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<or> cres = Failed \<longrightarrow> ctr' = []; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> (\<exists>f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f \<and> triv_refinement (aprog x) f)\<rbrakk> \<Longrightarrow> \<forall>s0' x. prefix_closed (\<lambda>s. \<Union>f\<in>{f. is_matching_fragment sr osr rvr' ctr' cres' s0' R s f \<and> triv_refinement (aprog x) f}. f s) proof (prove)
goal (2 subgoals):
 1. \<And>tr x s'. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> (\<exists>f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f \<and> triv_refinement (aprog x) f); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; (tr, Result (x, s')) \<in> f_a s\<rbrakk> \<Longrightarrow> {f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f \<and> triv_refinement (aprog x) f} \<noteq> {}
 2. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<or> cres = Failed \<longrightarrow> ctr' = []; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> (\<exists>f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f \<and> triv_refinement (aprog x) f)\<rbrakk> \<Longrightarrow> \<forall>s0' x. prefix_closed (\<lambda>s. \<Union>f\<in>{f. is_matching_fragment sr osr rvr' ctr' cres' s0' R s f \<and> triv_refinement (aprog x) f}. f s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<or> cres = Failed \<longrightarrow> ctr' = []; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> (\<exists>f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f \<and> triv_refinement (aprog x) f)\<rbrakk> \<Longrightarrow> \<forall>s0' x. prefix_closed (\<lambda>s. \<Union>f\<in>{f. is_matching_fragment sr osr rvr' ctr' cres' s0' R s f \<and> triv_refinement (aprog x) f}. f s) proof (prove)
goal (1 subgoal):
 1. \<And>s0' x. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> (\<exists>f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f \<and> triv_refinement (aprog x) f); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []\<rbrakk> \<Longrightarrow> prefix_closed (\<lambda>s. \<Union>f\<in>{f. is_matching_fragment sr osr rvr' ctr' cres' s0' R s f \<and> triv_refinement (aprog x) f}. f s) proof (prove)
goal (1 subgoal):
 1. \<And>s0' x. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> (\<exists>f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f \<and> triv_refinement (aprog x) f); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []\<rbrakk> \<Longrightarrow> \<forall>s' f. f \<in> {f. is_matching_fragment sr osr rvr' ctr' cres' s0' R s' f \<and> triv_refinement (aprog x) f} \<longrightarrow> prefix_closed f proof (prove)
goal:
No subgoals!