kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_RG

lemma rg_conj:
  "\<lbrakk>\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q and Q'\<rbrace>" unfolding validI_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q and Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s')); prefix_closed f \<and> (\<forall>s0 s tr res. P' s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q' rv (last_st_tr tr s0) s'))\<rbrakk> \<Longrightarrow> prefix_closed f \<and> (\<forall>s0 s tr res. (P and P') s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> (Q and Q') rv (last_st_tr tr s0) s'))
theory Trace_RG

lemma rg_pre_cont[simp]:
  "\<lbrace>\<bottom>\<bottom>\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> = prefix_closed f" by (simp add: validI_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_ _. False\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> = prefix_closed f
theory Trace_RG

lemma rg_FalseE[simp]:
  "\<lbrace>\<bottom>\<bottom>\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> = prefix_closed f" by (simp add: validI_def validIE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_ _. False\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> = prefix_closed f
theory Trace_RG

lemma rg_post_imp:
  "\<lbrakk>\<And>v s0 s. Q' v s0 s \<Longrightarrow> Q v s0 s; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" by (simp add: validI_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>v s0 s. Q' v s0 s \<Longrightarrow> Q v s0 s; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
theory Trace_RG

lemma rg_post_impE:
  "\<lbrakk>\<And>v s0 s. Q' v s0 s \<Longrightarrow> Q v s0 s; \<And>v s0 s. E' v s0 s \<Longrightarrow> E v s0 s; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>,\<lbrace>E'\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by (clarsimp simp: validIE_def2 split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>v s0 s. Q' v s0 s \<Longrightarrow> Q v s0 s; \<And>v s0 s. E' v s0 s \<Longrightarrow> E v s0 s; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace>, \<lbrace>E'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_RG

lemma rg_post_imp_dc:
  "\<lbrakk>\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q'\<rbrace>; \<And>s0 s. Q' s0 s \<Longrightarrow> Q s0 s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>" by (fastforce simp: validIE_def validI_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. Q'\<rbrace>; \<And>s0 s. Q' s0 s \<Longrightarrow> Q s0 s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace>
theory Trace_RG

lemma rg_post_imp_dc2:
  "\<lbrakk>\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q'\<rbrace>; \<And>s0 s. Q' s0 s \<Longrightarrow> Q s0 s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>,-" by (fastforce simp: validIE_def validI_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. Q'\<rbrace>; \<And>s0 s. Q' s0 s \<Longrightarrow> Q s0 s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace>, -
theory Trace_RG

lemma rg_post_imp_dc2E:
  "\<lbrakk>\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q'\<rbrace>; \<And>s0 s. Q' s0 s \<Longrightarrow> Q s0 s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>,-,\<lbrace>\<lambda>_. Q\<rbrace>" by (fastforce simp: validIE_def validI_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. Q'\<rbrace>; \<And>s0 s. Q' s0 s \<Longrightarrow> Q s0 s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>, -, \<lbrace>\<lambda>_. Q\<rbrace>
theory Trace_RG

lemma rg_guar_impE:
  "\<lbrakk>\<And>s0 s. G' s0 s \<Longrightarrow> G s0 s; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G'\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by (clarsimp simp: validIE_def elim!: rg_guar_imp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s0 s. G' s0 s \<Longrightarrow> G s0 s; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G'\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_RG

lemma rg_conjD1:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0. Q rv s0 and Q' rv s0\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. Q rv\<rbrace>" unfolding validI_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0. Q rv s0 and Q' rv s0\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> (Q rv (last_st_tr tr s0) and Q' rv (last_st_tr tr s0)) s')) \<Longrightarrow> prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s'))
theory Trace_RG

lemma rg_conjD2:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0. Q rv s0 and Q' rv s0\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. Q' rv\<rbrace>" unfolding validI_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0. Q rv s0 and Q' rv s0\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> (Q rv (last_st_tr tr s0) and Q' rv (last_st_tr tr s0)) s')) \<Longrightarrow> prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q' rv (last_st_tr tr s0) s'))
theory Trace_RG

lemma rg_post_disjI1:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. Q rv\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0. Q rv s0 or Q' rv s0\<rbrace>" unfolding validI_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0. Q rv s0 or Q' rv s0\<rbrace> proof (prove)
goal (1 subgoal):
 1. prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s')) \<Longrightarrow> prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> (Q rv (last_st_tr tr s0) or Q' rv (last_st_tr tr s0)) s'))
theory Trace_RG

lemma rg_post_disjI2:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. Q' rv\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0. Q rv s0 or Q' rv s0\<rbrace>" unfolding validI_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0. Q rv s0 or Q' rv s0\<rbrace> proof (prove)
goal (1 subgoal):
 1. prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q' rv (last_st_tr tr s0) s')) \<Longrightarrow> prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> (Q rv (last_st_tr tr s0) or Q' rv (last_st_tr tr s0)) s'))
theory Trace_RG

lemma use_validI':
  "\<lbrakk>(tr, Result (rv, s')) \<in> rely f R s0 s; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; P s0 s; s0' = last_st_tr tr s0\<rbrakk>
   \<Longrightarrow> Q rv s0' s'" unfolding validI_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(tr, Result (rv, s')) \<in> rely f R s0 s; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; P s0 s; s0' = last_st_tr tr s0\<rbrakk> \<Longrightarrow> Q rv s0' s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(tr, Result (rv, s')) \<in> rely f R s0 s; prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s')); P s0 s; s0' = last_st_tr tr s0\<rbrakk> \<Longrightarrow> Q rv s0' s'
theory Trace_RG

lemma use_validI_guar:
  "\<lbrakk>(tr, res) \<in> rely f R s0 s; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; P s0 s\<rbrakk>
   \<Longrightarrow> guar_cond G s0 tr" unfolding validI_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(tr, res) \<in> rely f R s0 s; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; P s0 s\<rbrakk> \<Longrightarrow> guar_cond G s0 tr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(tr, res) \<in> rely f R s0 s; prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s')); P s0 s\<rbrakk> \<Longrightarrow> guar_cond G s0 tr
theory Trace_RG

lemma in_inv_by_rgD:
  "\<lbrakk>\<And>P. f \<lbrace>R\<rbrace>,-,\<lbrace>P\<rbrace>; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> s' = s" unfolding validI_def apply (drule meta_spec[where x="\<lambda>_. (=) s"]) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>P. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> s' = s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>P. prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond (\<lambda>_ _. True) s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> P (last_st_tr tr s0) s')); (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> s' = s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(tr, Result (rv, s')) \<in> rely f R s0 s; prefix_closed f \<and> (\<forall>s0 sa tr res. s = sa \<and> (tr, res) \<in> rely f R s0 sa \<longrightarrow> guar_cond (\<lambda>_ _. True) s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> s = s'))\<rbrakk> \<Longrightarrow> s' = s proof (prove)
goal:
No subgoals!
theory Trace_RG

lemma last_st_in_inv_by_rgD:
  "\<lbrakk>\<And>P. f \<lbrace>R\<rbrace>,-,\<lbrace>P\<rbrace>; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> last_st_tr tr s0 = s0" unfolding validI_def apply (drule meta_spec[where x="\<lambda>s0' _. s0' = s0"]) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>P. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> last_st_tr tr s0 = s0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>P. prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond (\<lambda>_ _. True) s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> P (last_st_tr tr s0) s')); (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> last_st_tr tr s0 = s0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(tr, Result (rv, s')) \<in> rely f R s0 s; prefix_closed f \<and> (\<forall>s0a s tr res. s0a = s0 \<and> (tr, res) \<in> rely f R s0a s \<longrightarrow> guar_cond (\<lambda>_ _. True) s0a tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> last_st_tr tr s0a = s0))\<rbrakk> \<Longrightarrow> last_st_tr tr s0 = s0 proof (prove)
goal:
No subgoals!
theory Trace_RG

lemma validI_GD_drop:
  "\<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; P s0 s; (tr, res) \<in> f s;
     rely_cond R s0 (drop n tr)\<rbrakk>
   \<Longrightarrow> guar_cond G s0 (drop n tr)" apply (drule prefix_closed_drop[where n=n], erule validI_prefix_closed) apply (auto dest: validI_GD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; P s0 s; (tr, res) \<in> f s; rely_cond R s0 (drop n tr)\<rbrakk> \<Longrightarrow> guar_cond G s0 (drop n tr) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; P s0 s; rely_cond R s0 (drop n tr); \<exists>res'. (drop n tr, res') \<in> f s\<rbrakk> \<Longrightarrow> guar_cond G s0 (drop n tr) proof (prove)
goal:
No subgoals!
theory Trace_RG

lemma rely_cond_drop:
  "rely_cond R s0 xs \<Longrightarrow> rely_cond R s0 (drop n xs)" using rely_cond_append[where xs="take n xs" and ys="drop n xs"] by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rely_cond R s0 xs \<Longrightarrow> rely_cond R s0 (drop n xs) proof (prove)
using this:
rely_cond ?R ?s (take n xs @ drop n xs) = (rely_cond ?R ?s (drop n xs) \<and> rely_cond ?R (last_st_tr (drop n xs) ?s) (take n xs))

goal (1 subgoal):
 1. rely_cond R s0 xs \<Longrightarrow> rely_cond R s0 (drop n xs)
theory Trace_RG

lemma rely_cond_is_drop:
  "\<lbrakk>rely_cond R s0 xs; (ys = drop (length xs - length ys) xs)\<rbrakk>
   \<Longrightarrow> rely_cond R s0 ys" by (metis rely_cond_drop)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rely_cond R s0 xs; ys = drop (length xs - length ys) xs\<rbrakk> \<Longrightarrow> rely_cond R s0 ys
theory Trace_RG

lemma bounded_rev_nat_induct:
  "\<lbrakk>(\<And>n. N \<le> n \<Longrightarrow> P n); \<And>n. \<lbrakk>n < N; P (Suc n)\<rbrakk> \<Longrightarrow> P n\<rbrakk>
   \<Longrightarrow> P n" by (induct diff\<equiv>"N - n" arbitrary: n; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>n. N \<le> n \<Longrightarrow> P n; \<And>n. \<lbrakk>n < N; P (Suc n)\<rbrakk> \<Longrightarrow> P n\<rbrakk> \<Longrightarrow> P n
theory Trace_RG

lemma drop_n_induct:
  "\<lbrakk>P []; \<And>n. \<lbrakk>n < length xs; P (drop (Suc n) xs)\<rbrakk> \<Longrightarrow> P (drop n xs)\<rbrakk>
   \<Longrightarrow> P (drop n xs)" by (induct len\<equiv>"length (drop n xs)" arbitrary: n xs; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P []; \<And>n. \<lbrakk>n < length xs; P (drop (Suc n) xs)\<rbrakk> \<Longrightarrow> P (drop n xs)\<rbrakk> \<Longrightarrow> P (drop n xs)
theory Trace_RG

lemma guar_cond_Cons:
  "\<lbrakk>guar_cond R s0 xs; fst x \<noteq> Env \<longrightarrow> R (last_st_tr xs s0) (snd x)\<rbrakk>
   \<Longrightarrow> guar_cond R s0 (x # xs)" by (simp add: guar_cond_Cons_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>guar_cond R s0 xs; fst x \<noteq> Env \<longrightarrow> R (last_st_tr xs s0) (snd x)\<rbrakk> \<Longrightarrow> guar_cond R s0 (x # xs)
theory Trace_RG

lemma guar_cond_drop_Suc_eq:
  "n < length xs
   \<Longrightarrow> guar_cond R s0 (drop n xs) = (guar_cond R s0 (drop (Suc n) xs)
       \<and> (fst (xs ! n) \<noteq> Env \<longrightarrow> R (last_st_tr (drop (Suc n) xs) s0) (snd (xs ! n))))" apply (rule trans[OF _ guar_cond_Cons_eq]) apply (simp add: Cons_nth_drop_Suc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < length xs \<Longrightarrow> guar_cond R s0 (drop n xs) = (guar_cond R s0 (drop (Suc n) xs) \<and> (fst (xs ! n) \<noteq> Env \<longrightarrow> R (last_st_tr (drop (Suc n) xs) s0) (snd (xs ! n)))) proof (prove)
goal (1 subgoal):
 1. n < length xs \<Longrightarrow> guar_cond R s0 (drop n xs) = guar_cond R s0 (xs ! n # drop (Suc n) xs) proof (prove)
goal:
No subgoals!
theory Trace_RG

lemma guar_cond_drop_Suc:
  "\<lbrakk>guar_cond R s0 (drop (Suc n) xs);
    fst (xs ! n) \<noteq> Env \<longrightarrow> R (last_st_tr (drop (Suc n) xs) s0) (snd (xs ! n))\<rbrakk>
   \<Longrightarrow> guar_cond R s0 (drop n xs)" by (cases "n < length xs"; simp add: guar_cond_drop_Suc_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>guar_cond R s0 (drop (Suc n) xs); fst (xs ! n) \<noteq> Env \<longrightarrow> R (last_st_tr (drop (Suc n) xs) s0) (snd (xs ! n))\<rbrakk> \<Longrightarrow> guar_cond R s0 (drop n xs)
theory Trace_RG

lemma rely_cond_Cons_eq:
  "rely_cond R s0 (x # xs)
   = (rely_cond R s0 xs \<and> (fst x = Env \<longrightarrow> R (last_st_tr xs s0) (snd x)))" by (simp add: rely_cond_def trace_steps_append conj_comms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rely_cond R s0 (x # xs) = (rely_cond R s0 xs \<and> (fst x = Env \<longrightarrow> R (last_st_tr xs s0) (snd x)))
theory Trace_RG

lemma rely_cond_Cons:
  "\<lbrakk>rely_cond R s0 xs; fst x = Env \<longrightarrow> R (last_st_tr xs s0) (snd x)\<rbrakk>
   \<Longrightarrow> rely_cond R s0 (x # xs)" by (simp add: rely_cond_Cons_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rely_cond R s0 xs; fst x = Env \<longrightarrow> R (last_st_tr xs s0) (snd x)\<rbrakk> \<Longrightarrow> rely_cond R s0 (x # xs)
theory Trace_RG

lemma rely_cond_drop_Suc_eq:
  "n < length xs
   \<Longrightarrow> rely_cond R s0 (drop n xs) = (rely_cond R s0 (drop (Suc n) xs)
       \<and> (fst (xs ! n) = Env \<longrightarrow> R (last_st_tr (drop (Suc n) xs) s0) (snd (xs ! n))))" apply (rule trans[OF _ rely_cond_Cons_eq]) apply (simp add: Cons_nth_drop_Suc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < length xs \<Longrightarrow> rely_cond R s0 (drop n xs) = (rely_cond R s0 (drop (Suc n) xs) \<and> (fst (xs ! n) = Env \<longrightarrow> R (last_st_tr (drop (Suc n) xs) s0) (snd (xs ! n)))) proof (prove)
goal (1 subgoal):
 1. n < length xs \<Longrightarrow> rely_cond R s0 (drop n xs) = rely_cond R s0 (xs ! n # drop (Suc n) xs) proof (prove)
goal:
No subgoals!
theory Trace_RG

lemma rely_cond_drop_Suc:
  "\<lbrakk>rely_cond R s0 (drop (Suc n) xs);
    fst (xs ! n) = Env \<longrightarrow> R (last_st_tr (drop (Suc n) xs) s0) (snd (xs ! n))\<rbrakk>
   \<Longrightarrow> rely_cond R s0 (drop n xs)" by (cases "n < length xs"; simp add: rely_cond_drop_Suc_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rely_cond R s0 (drop (Suc n) xs); fst (xs ! n) = Env \<longrightarrow> R (last_st_tr (drop (Suc n) xs) s0) (snd (xs ! n))\<rbrakk> \<Longrightarrow> rely_cond R s0 (drop n xs)
theory Trace_RG

lemma last_st_tr_map_zip_hd:
  "\<lbrakk>length flags = length tr; tr \<noteq> [] \<longrightarrow> snd (f (hd flags, hd tr)) = snd (hd tr)\<rbrakk>
   \<Longrightarrow> last_st_tr (map f (zip flags tr)) = last_st_tr tr" apply (cases tr; simp) apply (cases flags; simp) apply (simp add: fun_eq_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length flags = length tr; tr \<noteq> [] \<longrightarrow> snd (f (hd flags, hd tr)) = snd (hd tr)\<rbrakk> \<Longrightarrow> last_st_tr (map f (zip flags tr)) = last_st_tr tr proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>length flags = Suc (length list); snd (f (hd flags, a)) = snd a; tr = a # list\<rbrakk> \<Longrightarrow> last_st_tr (map f (zip flags (a # list))) = last_st_tr (a # list) proof (prove)
goal (1 subgoal):
 1. \<And>a list aa lista. \<lbrakk>length lista = length list; snd (f (aa, a)) = snd a; tr = a # list; flags = aa # lista\<rbrakk> \<Longrightarrow> last_st_tr (f (aa, a) # map f (zip lista list)) = last_st_tr (a # list) proof (prove)
goal:
No subgoals!
theory Trace_RG

lemma last_st_tr_drop_map_zip_hd:
  "\<lbrakk>length flags = length tr;
    n < length tr \<longrightarrow> snd (f (flags ! n, tr ! n)) = snd (tr ! n)\<rbrakk>
   \<Longrightarrow> last_st_tr (drop n (map f (zip flags tr))) = last_st_tr (drop n tr)" apply (simp add: drop_map drop_zip) apply (rule last_st_tr_map_zip_hd; clarsimp) apply (simp add: hd_drop_conv_nth) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length flags = length tr; n < length tr \<longrightarrow> snd (f (flags ! n, tr ! n)) = snd (tr ! n)\<rbrakk> \<Longrightarrow> last_st_tr (drop n (map f (zip flags tr))) = last_st_tr (drop n tr) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length flags = length tr; n < length tr \<longrightarrow> snd (f (flags ! n, tr ! n)) = snd (tr ! n)\<rbrakk> \<Longrightarrow> last_st_tr (map f (zip (drop n flags) (drop n tr))) = last_st_tr (drop n tr) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length flags = length tr; snd (f (flags ! n, tr ! n)) = snd (tr ! n); \<not> length tr \<le> n\<rbrakk> \<Longrightarrow> snd (f (hd (drop n flags), hd (drop n tr))) = snd (hd (drop n tr)) proof (prove)
goal:
No subgoals!