theory Prefix_Refinement

lemma list_all2_all_trace_steps:
  assumes P: "\<forall>x\<in>trace_steps (rev tr) s0. P x"
  and lR': "list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> R' as cs) tr' tr"
  and R': "R' s0' s0"
  and Q: "\<forall>idn as1 as2 cs1 cs2. R' as1 cs1 \<longrightarrow> R' as2 cs2
    \<longrightarrow> P (idn, cs1, cs2) \<longrightarrow> Q (idn, as1, as2)"
  shows "\<forall>x\<in>trace_steps (rev tr') s0'. Q x" proof - note lR'' = lR'[simplified trans[OF list_all2_rev[symmetric] list_all2_conv_all_nth],
    simplified split_def, THEN conjunct2, rule_format] note len[simp] = lR'[THEN list_all2_lengthD] show ?thesis using P R' apply (clarsimp simp: trace_steps_nth) apply (drule_tac x=x in bspec, simp) apply (frule lR''[simplified]) apply (cut_tac i="x - 1" in lR'', simp) apply (auto simp: Q) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>trace_steps (rev tr') s0'. Q x proof (state)
goal (1 subgoal):
 1. \<forall>x\<in>trace_steps (rev tr') s0'. Q x proof (state)
this:
?i < length (rev tr') \<Longrightarrow> fst (rev tr' ! ?i) = fst (rev tr ! ?i) \<and> R' (snd (rev tr' ! ?i)) (snd (rev tr ! ?i))

goal (1 subgoal):
 1. \<forall>x\<in>trace_steps (rev tr') s0'. Q x proof (state)
this:
length tr' = length tr

goal (1 subgoal):
 1. \<forall>x\<in>trace_steps (rev tr') s0'. Q x proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>trace_steps (rev tr') s0'. Q x proof (prove)
using this:
\<forall>x\<in>trace_steps (rev tr) s0. P x
R' s0' s0

goal (1 subgoal):
 1. \<forall>x\<in>trace_steps (rev tr') s0'. Q x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>{..<length tr}. P (fst (rev tr ! x), if x = 0 then s0 else snd (rev tr ! (x - 1)), snd (rev tr ! x)); R' s0' s0; x < length tr\<rbrakk> \<Longrightarrow> (x = 0 \<longrightarrow> Q (fst (rev tr' ! 0), s0', snd (rev tr' ! 0))) \<and> (0 < x \<longrightarrow> Q (fst (rev tr' ! x), snd (rev tr' ! (x - Suc 0)), snd (rev tr' ! x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>R' s0' s0; x < length tr; P (fst (rev tr ! x), if x = 0 then s0 else snd (rev tr ! (x - 1)), snd (rev tr ! x))\<rbrakk> \<Longrightarrow> (x = 0 \<longrightarrow> Q (fst (rev tr' ! 0), s0', snd (rev tr' ! 0))) \<and> (0 < x \<longrightarrow> Q (fst (rev tr' ! x), snd (rev tr' ! (x - Suc 0)), snd (rev tr' ! x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>R' s0' s0; x < length tr; P (fst (rev tr ! x), if x = 0 then s0 else snd (rev tr ! (x - 1)), snd (rev tr ! x)); fst (rev tr' ! x) = fst (rev tr ! x) \<and> R' (snd (rev tr' ! x)) (snd (rev tr ! x))\<rbrakk> \<Longrightarrow> (x = 0 \<longrightarrow> Q (fst (rev tr' ! 0), s0', snd (rev tr' ! 0))) \<and> (0 < x \<longrightarrow> Q (fst (rev tr' ! x), snd (rev tr' ! (x - Suc 0)), snd (rev tr' ! x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>R' s0' s0; x < length tr; P (fst (rev tr ! x), if x = 0 then s0 else snd (rev tr ! (x - 1)), snd (rev tr ! x)); fst (rev tr' ! x) = fst (rev tr ! x) \<and> R' (snd (rev tr' ! x)) (snd (rev tr ! x)); fst (rev tr' ! (x - 1)) = fst (rev tr ! (x - 1)) \<and> R' (snd (rev tr' ! (x - 1))) (snd (rev tr ! (x - 1)))\<rbrakk> \<Longrightarrow> (x = 0 \<longrightarrow> Q (fst (rev tr' ! 0), s0', snd (rev tr' ! 0))) \<and> (0 < x \<longrightarrow> Q (fst (rev tr' ! x), snd (rev tr' ! (x - Suc 0)), snd (rev tr' ! x))) proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>x\<in>trace_steps (rev tr') s0'. Q x

goal:
No subgoals!