theory Prefix_Refinement

lemma prefix_refinement_commit_step:
  "\<forall>s t. isr s t \<longrightarrow> sr s t \<and> osr s t
    \<Longrightarrow> prefix_refinement sr isr osr (\<lambda>_ _. True) (\<top>\<top>) (\<top>\<top>) AR R commit_step commit_step" apply (clarsimp simp: prefix_refinement_def) apply (rule default_prefix_refinement_ex) apply (simp add: commit_step_def bind_def get_def return_def put_trace_elem_def) apply (erule disjE) apply (simp add: is_matching_fragment_no_trace) apply (clarsimp simp: is_matching_fragment_def) apply (simp add: prefix_closed_def self_closed_def env_closed_def) apply (simp add: matching_tr_pfx_def matching_tr_def rely_cond_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s t. isr s t \<longrightarrow> sr s t \<and> osr s t \<Longrightarrow> prefix_refinement sr isr osr (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>_ _. True) AR R commit_step commit_step proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t a b. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> sr s t \<and> osr s t; isr s t; sr s0 t0; (a, b) \<in> commit_step t; rely_cond R t0 a\<rbrakk> \<Longrightarrow> \<exists>f. is_matching_fragment sr osr (\<lambda>_ _. True) a b s0 AR s f \<and> triv_refinement commit_step f proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t a b. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> sr s t \<and> osr s t; isr s t; sr s0 t0; (a, b) \<in> commit_step t; rely_cond R t0 a\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr (\<lambda>_ _. True) a b s0 AR s (\<lambda>s. commit_step s \<inter> {tr'. length tr' \<le> length a} \<times> UNIV) proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t a b. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> sr s t \<and> osr s t; isr s t; sr s0 t0; a = [] \<and> b = Incomplete \<or> a = [(Me, t)] \<and> b = Result ((), t); rely_cond R t0 a\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr (\<lambda>_ _. True) a b s0 AR s (\<lambda>s. insert ([], Incomplete) ({([(Me, s)], Result ((), s))} \<inter> {tr'. length tr' \<le> length a} \<times> UNIV)) proof (prove)
goal (2 subgoals):
 1. \<And>s s0 t0 t a b. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> sr s t \<and> osr s t; isr s t; sr s0 t0; rely_cond R t0 a; a = [] \<and> b = Incomplete\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr (\<lambda>_ _. True) a b s0 AR s (\<lambda>s. insert ([], Incomplete) ({([(Me, s)], Result ((), s))} \<inter> {tr'. length tr' \<le> length a} \<times> UNIV))
 2. \<And>s s0 t0 t a b. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> sr s t \<and> osr s t; isr s t; sr s0 t0; rely_cond R t0 a; a = [(Me, t)] \<and> b = Result ((), t)\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr (\<lambda>_ _. True) a b s0 AR s (\<lambda>s. insert ([], Incomplete) ({([(Me, s)], Result ((), s))} \<inter> {tr'. length tr' \<le> length a} \<times> UNIV)) proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t a b. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> sr s t \<and> osr s t; isr s t; sr s0 t0; rely_cond R t0 a; a = [(Me, t)] \<and> b = Result ((), t)\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr (\<lambda>_ _. True) a b s0 AR s (\<lambda>s. insert ([], Incomplete) ({([(Me, s)], Result ((), s))} \<inter> {tr'. length tr' \<le> length a} \<times> UNIV)) proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> sr s t \<and> osr s t; isr s t; sr s0 t0; rely_cond R t0 [(Me, t)]\<rbrakk> \<Longrightarrow> prefix_closed (\<lambda>s. {([], Incomplete), ([(Me, s)], Result ((), s))}) \<and> self_closed (\<lambda>xs. xs = [] \<and> fst ([(Me, t)] ! length xs) = Me) s (\<lambda>s. {([], Incomplete), ([(Me, s)], Result ((), s))}) \<and> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) [(Me, t)] \<and> rely_cond AR s0 ((Env, s) # xs)) s (\<lambda>s. {([], Incomplete), ([(Me, s)], Result ((), s))}) \<and> matching_tr_pfx sr [] [(Me, t)] \<and> rely_cond AR s0 [(Me, s)] \<and> matching_tr_pfx sr [(Me, s)] [(Me, t)] proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> sr s t \<and> osr s t; isr s t; sr s0 t0; rely_cond R t0 [(Me, t)]\<rbrakk> \<Longrightarrow> (\<forall>s'. matching_tr_pfx sr [(Env, s')] [(Me, t)] \<longrightarrow> \<not> rely_cond AR s0 [(Env, s')]) \<and> matching_tr_pfx sr [] [(Me, t)] \<and> rely_cond AR s0 [(Me, s)] \<and> matching_tr_pfx sr [(Me, s)] [(Me, t)] proof (prove)
goal:
No subgoals!