theory Prefix_Refinement

lemma prefix_refinement_repeat_n:
  "prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g
    \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>AR\<rbrace> f \<lbrace>\<top>\<top>\<rbrace>,\<lbrace>\<lambda>_. P\<rbrace>
    \<Longrightarrow> \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>\<top>\<top>\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>
    \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R (repeat_n n f) (repeat_n n g)" apply (induct n) apply (simp add: prefix_refinement_return_imp) apply (rule prefix_refinement_weaken_pre) apply simp apply (rule prefix_refinement_bind, assumption+) apply simp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R (repeat_n n f) (repeat_n n g) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R (repeat_n 0 f) (repeat_n 0 g)
 2. \<And>n. \<lbrakk>\<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R (repeat_n n f) (repeat_n n g); prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R (repeat_n (Suc n) f) (repeat_n (Suc n) g) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R (repeat_n n f) (repeat_n n g); prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R (repeat_n (Suc n) f) (repeat_n (Suc n) g) proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>\<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R (repeat_n n f) (repeat_n n g); prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) (?P'4 n) (?Q'4 n) AR R (repeat_n (Suc n) f) (repeat_n (Suc n) g)
 2. \<And>n. \<lbrakk>\<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R (repeat_n n f) (repeat_n n g); prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s s0. P s0 s \<longrightarrow> ?P'4 n s0 s
 3. \<And>n. \<lbrakk>\<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R (repeat_n n f) (repeat_n n g); prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s0 s \<longrightarrow> Q t0 t \<longrightarrow> ?Q'4 n t0 t proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R (repeat_n n f) (repeat_n n g); prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) (?P'4 n) (?Q'4 n) AR R (do y <- f;
repeat_n n f
od) (do y <- g;
repeat_n n g
od)
 2. \<And>n. \<lbrakk>\<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R (repeat_n n f) (repeat_n n g); prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s s0. P s0 s \<longrightarrow> ?P'4 n s0 s
 3. \<And>n. \<lbrakk>\<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R (repeat_n n f) (repeat_n n g); prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s0 s \<longrightarrow> Q t0 t \<longrightarrow> ?Q'4 n t0 t proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R (repeat_n n f) (repeat_n n g); prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s s0. P s0 s \<longrightarrow> (P and P) s0 s
 2. \<And>n. \<lbrakk>\<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R (repeat_n n f) (repeat_n n g); prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s0 s \<longrightarrow> Q t0 t \<longrightarrow> (Q and (\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t))) t0 t proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R (repeat_n n f) (repeat_n n g); prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s0 s \<longrightarrow> Q t0 t \<longrightarrow> (Q and (\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t))) t0 t proof (prove)
goal:
No subgoals!