theory Trace_RG

lemma validI_invariant_imp:
  assumes v: "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
    and P: "\<forall>s0 s. P s0 s \<longrightarrow> I s0"
    and R: "\<forall>s0 s. I s0 \<longrightarrow> R s0 s \<longrightarrow> I s"
    and G: "\<forall>s0 s. I s0 \<longrightarrow> G s0 s \<longrightarrow> I s"
  shows "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>\<lambda>s0 s. I s0 \<and> I s \<and> G s0 s\<rbrace>,\<lbrace>\<lambda>rv s0 s. I s0 \<and> Q rv s0 s\<rbrace>" proof - { fix tr s0 i assume r: "rely_cond R s0 tr" and g: "guar_cond G s0 tr"
      and I: "I s0" hence imp: "\<forall>(_, s, s') \<in> trace_steps (rev tr) s0. I s \<longrightarrow> I s'" apply (clarsimp simp: guar_cond_def rely_cond_def) apply (drule(1) bspec)+ apply (clarsimp simp: eq_Me_neq_Env) apply (metis R G) done hence "i < length tr \<longrightarrow> I (snd (rev tr ! i))" using I apply (induct i) apply (clarsimp simp: neq_Nil_conv[where xs="rev tr" for tr, simplified]) apply clarsimp apply (drule bspec, fastforce simp add: trace_steps_nth) apply simp done } note I = this show ?thesis using v apply (clarsimp simp: validI_def rely_def imp_conjL) apply (drule spec2, drule(1) mp)+ apply clarsimp apply (frule P[rule_format]) apply (clarsimp simp: guar_cond_def trace_steps_nth I last_st_tr_def
                          hd_append last_rev[symmetric]
                          last_conv_nth rev_map) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>\<lambda>s0 s. I s0 \<and> I s \<and> G s0 s\<rbrace>, \<lbrace>\<lambda>rv s0 s. I s0 \<and> Q rv s0 s\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>\<lambda>s0 s. I s0 \<and> I s \<and> G s0 s\<rbrace>, \<lbrace>\<lambda>rv s0 s. I s0 \<and> Q rv s0 s\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>\<lambda>s0 s. I s0 \<and> I s \<and> G s0 s\<rbrace>, \<lbrace>\<lambda>rv s0 s. I s0 \<and> Q rv s0 s\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>\<lambda>s0 s. I s0 \<and> I s \<and> G s0 s\<rbrace>, \<lbrace>\<lambda>rv s0 s. I s0 \<and> Q rv s0 s\<rbrace> proof (state)
this:
rely_cond R s0 tr
guar_cond G s0 tr
I s0

goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>\<lambda>s0 s. I s0 \<and> I s \<and> G s0 s\<rbrace>, \<lbrace>\<lambda>rv s0 s. I s0 \<and> Q rv s0 s\<rbrace> proof (prove)
using this:
rely_cond R s0 tr
guar_cond G s0 tr
I s0

goal (1 subgoal):
 1. \<forall>(uu_, s, s')\<in>trace_steps (rev tr) s0. I s \<longrightarrow> I s' proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>\<forall>x\<in>trace_steps (rev tr) s0. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> R s0 s; \<forall>x\<in>trace_steps (rev tr) s0. case x of (ident, s0, s) \<Rightarrow> ident = Me \<longrightarrow> G s0 s; I s0; (a, aa, b) \<in> trace_steps (rev tr) s0; I aa\<rbrakk> \<Longrightarrow> I b proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>I s0; (a, aa, b) \<in> trace_steps (rev tr) s0; I aa; case (a, aa, b) of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> R s0 s; case (a, aa, b) of (ident, s0, s) \<Rightarrow> ident = Me \<longrightarrow> G s0 s\<rbrakk> \<Longrightarrow> I b proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>I s0; (a, aa, b) \<in> trace_steps (rev tr) s0; I aa; a = Env \<longrightarrow> R aa b; a \<noteq> Env \<longrightarrow> G aa b\<rbrakk> \<Longrightarrow> I b proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>(uu_, s, s')\<in>trace_steps (rev tr) s0. I s \<longrightarrow> I s'

goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>\<lambda>s0 s. I s0 \<and> I s \<and> G s0 s\<rbrace>, \<lbrace>\<lambda>rv s0 s. I s0 \<and> Q rv s0 s\<rbrace> proof (prove)
using this:
\<forall>(uu_, s, s')\<in>trace_steps (rev tr) s0. I s \<longrightarrow> I s'

goal (1 subgoal):
 1. i < length tr \<longrightarrow> I (snd (rev tr ! i)) proof (prove)
using this:
\<forall>(uu_, s, s')\<in>trace_steps (rev tr) s0. I s \<longrightarrow> I s'
I s0

goal (1 subgoal):
 1. i < length tr \<longrightarrow> I (snd (rev tr ! i)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>(uu_, s, s')\<in>trace_steps (rev tr) s0. I s \<longrightarrow> I s'; I s0\<rbrakk> \<Longrightarrow> 0 < length tr \<longrightarrow> I (snd (rev tr ! 0))
 2. \<And>i. \<lbrakk>\<lbrakk>\<forall>(uu_, s, s')\<in>trace_steps (rev tr) s0. I s \<longrightarrow> I s'; I s0\<rbrakk> \<Longrightarrow> i < length tr \<longrightarrow> I (snd (rev tr ! i)); \<forall>(uu_, s, s')\<in>trace_steps (rev tr) s0. I s \<longrightarrow> I s'; I s0\<rbrakk> \<Longrightarrow> Suc i < length tr \<longrightarrow> I (snd (rev tr ! Suc i)) proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<lbrakk>\<forall>(uu_, s, s')\<in>trace_steps (rev tr) s0. I s \<longrightarrow> I s'; I s0\<rbrakk> \<Longrightarrow> i < length tr \<longrightarrow> I (snd (rev tr ! i)); \<forall>(uu_, s, s')\<in>trace_steps (rev tr) s0. I s \<longrightarrow> I s'; I s0\<rbrakk> \<Longrightarrow> Suc i < length tr \<longrightarrow> I (snd (rev tr ! Suc i)) proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>I (snd (rev tr ! i)); \<forall>x\<in>trace_steps (rev tr) s0. case x of (uu_, s, s') \<Rightarrow> I s \<longrightarrow> I s'; I s0; Suc i < length tr\<rbrakk> \<Longrightarrow> I (snd (rev tr ! Suc i)) proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>I (snd (rev tr ! i)); I s0; Suc i < length tr; case (fst (rev tr ! Suc i), if Suc i = 0 then s0 else snd (rev tr ! (Suc i - 1)), snd (rev tr ! Suc i)) of (uu_, s, s') \<Rightarrow> I s \<longrightarrow> I s'\<rbrakk> \<Longrightarrow> I (snd (rev tr ! Suc i)) proof (prove)
goal:
No subgoals! proof (state)
this:
i < length tr \<longrightarrow> I (snd (rev tr ! i))

goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>\<lambda>s0 s. I s0 \<and> I s \<and> G s0 s\<rbrace>, \<lbrace>\<lambda>rv s0 s. I s0 \<and> Q rv s0 s\<rbrace> proof (state)
this:
\<lbrakk>rely_cond R ?s0.2 ?tr2; guar_cond G ?s0.2 ?tr2; I ?s0.2\<rbrakk> \<Longrightarrow> ?i2 < length ?tr2 \<longrightarrow> I (snd (rev ?tr2 ! ?i2))

goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>\<lambda>s0 s. I s0 \<and> I s \<and> G s0 s\<rbrace>, \<lbrace>\<lambda>rv s0 s. I s0 \<and> Q rv s0 s\<rbrace> proof (state)
this:
\<lbrakk>rely_cond R ?s0.2 ?tr2; guar_cond G ?s0.2 ?tr2; I ?s0.2\<rbrakk> \<Longrightarrow> ?i2 < length ?tr2 \<longrightarrow> I (snd (rev ?tr2 ! ?i2))

goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>\<lambda>s0 s. I s0 \<and> I s \<and> G s0 s\<rbrace>, \<lbrace>\<lambda>rv s0 s. I s0 \<and> Q rv s0 s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>\<lambda>s0 s. I s0 \<and> I s \<and> G s0 s\<rbrace>, \<lbrace>\<lambda>rv s0 s. I s0 \<and> Q rv s0 s\<rbrace> proof (prove)
using this:
\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>

goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>\<lambda>s0 s. I s0 \<and> I s \<and> G s0 s\<rbrace>, \<lbrace>\<lambda>rv s0 s. I s0 \<and> Q rv s0 s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr res. \<lbrakk>prefix_closed f; \<forall>s0 s. P s0 s \<longrightarrow> (\<forall>tr res. (tr, res) \<in> f s \<longrightarrow> rely_cond R s0 tr \<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; (tr, res) \<in> f s; rely_cond R s0 tr\<rbrakk> \<Longrightarrow> guar_cond (\<lambda>s0 s. I s0 \<and> I s \<and> G s0 s) s0 tr \<and> ((\<exists>rv s'. res = Result (rv, s')) \<longrightarrow> I (last_st_tr tr s0)) proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr res. \<lbrakk>prefix_closed f; P s0 s; (tr, res) \<in> f s; rely_cond R s0 tr; rely_cond R s0 tr \<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> guar_cond (\<lambda>s0 s. I s0 \<and> I s \<and> G s0 s) s0 tr \<and> ((\<exists>rv s'. res = Result (rv, s')) \<longrightarrow> I (last_st_tr tr s0)) proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr res. \<lbrakk>prefix_closed f; P s0 s; (tr, res) \<in> f s; rely_cond R s0 tr; guar_cond G s0 tr; \<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s'\<rbrakk> \<Longrightarrow> guar_cond (\<lambda>s0 s. I s0 \<and> I s \<and> G s0 s) s0 tr \<and> ((\<exists>rv s'. res = Result (rv, s')) \<longrightarrow> I (last_st_tr tr s0)) proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr res. \<lbrakk>prefix_closed f; P s0 s; (tr, res) \<in> f s; rely_cond R s0 tr; guar_cond G s0 tr; \<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s'; I s0\<rbrakk> \<Longrightarrow> guar_cond (\<lambda>s0 s. I s0 \<and> I s \<and> G s0 s) s0 tr \<and> ((\<exists>rv s'. res = Result (rv, s')) \<longrightarrow> I (last_st_tr tr s0)) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>\<lambda>s0 s. I s0 \<and> I s \<and> G s0 s\<rbrace>, \<lbrace>\<lambda>rv s0 s. I s0 \<and> Q rv s0 s\<rbrace>

goal:
No subgoals!