theory Prefix_Refinement

lemma par_tr_fin_fragment:
  "par_tr_fin_principle f
    \<Longrightarrow> (tr, res) \<in> f s
    \<Longrightarrow> is_matching_fragment sr osr rvr ctr cres s0 R s f
    \<Longrightarrow> res = (case (length ctr - length tr, cres)
          of (0, Failed) \<Rightarrow> Failed
           | (0, Result _) \<Rightarrow> Result ((), last_st_tr tr s)
           | _ \<Rightarrow> Incomplete)" apply (frule(1) is_matching_fragment_trD) apply (cases "length tr < length ctr") apply (clarsimp split: nat.split) apply (clarsimp simp: matching_tr_pfx_def) apply (erule tmres.rel_cases; clarsimp) apply (frule(1) par_tr_fin_principleD) apply (clarsimp simp: neq_Nil_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>par_tr_fin_principle f; (tr, res) \<in> f s; is_matching_fragment sr osr rvr ctr cres s0 R s f\<rbrakk> \<Longrightarrow> res = (case (length ctr - length tr, cres) of (0, Failed) \<Rightarrow> Failed | (0, Incomplete) \<Rightarrow> Incomplete | (0, Result x) \<Rightarrow> Result ((), last_st_tr tr s) | (Suc nat, b) \<Rightarrow> Incomplete) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>par_tr_fin_principle f; (tr, res) \<in> f s; is_matching_fragment sr osr rvr ctr cres s0 R s f; 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)\<rbrakk> \<Longrightarrow> res = (case (length ctr - length tr, cres) of (0, Failed) \<Rightarrow> Failed | (0, Incomplete) \<Rightarrow> Incomplete | (0, Result x) \<Rightarrow> Result ((), last_st_tr tr s) | (Suc nat, b) \<Rightarrow> Incomplete) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>par_tr_fin_principle f; (tr, res) \<in> f s; is_matching_fragment sr osr rvr ctr cres s0 R s f; 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); length tr < length ctr\<rbrakk> \<Longrightarrow> res = (case (length ctr - length tr, cres) of (0, Failed) \<Rightarrow> Failed | (0, Incomplete) \<Rightarrow> Incomplete | (0, Result x) \<Rightarrow> Result ((), last_st_tr tr s) | (Suc nat, b) \<Rightarrow> Incomplete)
 2. \<lbrakk>par_tr_fin_principle f; (tr, res) \<in> f s; is_matching_fragment sr osr rvr ctr cres s0 R s f; 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); \<not> length tr < length ctr\<rbrakk> \<Longrightarrow> res = (case (length ctr - length tr, cres) of (0, Failed) \<Rightarrow> Failed | (0, Incomplete) \<Rightarrow> Incomplete | (0, Result x) \<Rightarrow> Result ((), last_st_tr tr s) | (Suc nat, b) \<Rightarrow> Incomplete) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>par_tr_fin_principle f; (tr, res) \<in> f s; is_matching_fragment sr osr rvr ctr cres s0 R s f; 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); \<not> length tr < length ctr\<rbrakk> \<Longrightarrow> res = (case (length ctr - length tr, cres) of (0, Failed) \<Rightarrow> Failed | (0, Incomplete) \<Rightarrow> Incomplete | (0, Result x) \<Rightarrow> Result ((), last_st_tr tr s) | (Suc nat, b) \<Rightarrow> Incomplete) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>par_tr_fin_principle f; (tr, res) \<in> f s; is_matching_fragment sr osr rvr ctr cres s0 R s f; rely_cond R s0 tr; length tr = length ctr; matching_tr sr (rev tr) (rev ctr); rel_tmres osr rvr res cres\<rbrakk> \<Longrightarrow> res = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result x \<Rightarrow> Result ((), last_st_tr tr s)) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>par_tr_fin_principle f; (tr, Result ((), b)) \<in> f s; is_matching_fragment sr osr rvr ctr (Result (a, ba)) s0 R s f; rely_cond R s0 tr; length tr = length ctr; matching_tr sr (rev tr) (rev ctr); res = Result ((), b); cres = Result (a, ba); rvr () a; osr b ba\<rbrakk> \<Longrightarrow> b = last_st_tr tr s proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>par_tr_fin_principle f; (tr, Result ((), b)) \<in> f s; is_matching_fragment sr osr rvr ctr (Result (a, ba)) s0 R s f; rely_cond R s0 tr; length tr = length ctr; matching_tr sr (rev tr) (rev ctr); res = Result ((), b); cres = Result (a, ba); rvr () a; osr b ba; b = last_st_tr tr s \<and> tr \<noteq> []\<rbrakk> \<Longrightarrow> b = last_st_tr tr s proof (prove)
goal:
No subgoals!