theory Prefix_Refinement

lemma par_tr_fin_add_env_n_steps:
  "par_tr_fin_principle f
    \<Longrightarrow> par_tr_fin_principle (do x \<leftarrow> f; env_n_steps n od)" proof (induct n) case 0 then show ?case by simp next case (Suc n) define f' where "f' \<equiv> (do x \<leftarrow> f; env_n_steps n od)" from Suc have f': "par_tr_fin_principle f'" by (simp add: f'_def) hence "par_tr_fin_principle (do x \<leftarrow> f'; env_n_steps 1 od)" by (clarsimp simp: par_tr_fin_principle_def env_step_def
                       bind_def select_def get_def put_def length_Suc_conv
                       return_def put_trace_elem_def
                split: tmres.split_asm) then show ?case by (simp add: repeat_n_plus[where m="Suc 0", simplified, symmetric]
                     f'_def bind_assoc) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. par_tr_fin_principle f \<Longrightarrow> par_tr_fin_principle (do x <- f;
env_n_steps n
od) proof (state)
goal (2 subgoals):
 1. par_tr_fin_principle f \<Longrightarrow> par_tr_fin_principle (do x <- f;
env_n_steps 0
od)
 2. \<And>n. \<lbrakk>par_tr_fin_principle f \<Longrightarrow> par_tr_fin_principle (do x <- f;
env_n_steps n
od); par_tr_fin_principle f\<rbrakk> \<Longrightarrow> par_tr_fin_principle (do x <- f;
env_n_steps (Suc n)
od) proof (state)
this:
par_tr_fin_principle f

goal (2 subgoals):
 1. par_tr_fin_principle f \<Longrightarrow> par_tr_fin_principle (do x <- f;
env_n_steps 0
od)
 2. \<And>n. \<lbrakk>par_tr_fin_principle f \<Longrightarrow> par_tr_fin_principle (do x <- f;
env_n_steps n
od); par_tr_fin_principle f\<rbrakk> \<Longrightarrow> par_tr_fin_principle (do x <- f;
env_n_steps (Suc n)
od) proof (chain)
picking this:
par_tr_fin_principle f proof (prove)
using this:
par_tr_fin_principle f

goal (1 subgoal):
 1. par_tr_fin_principle (do x <- f;
env_n_steps 0
od) proof (state)
this:
par_tr_fin_principle (do x <- f;
env_n_steps 0
od)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>par_tr_fin_principle f \<Longrightarrow> par_tr_fin_principle (do x <- f;
env_n_steps n
od); par_tr_fin_principle f\<rbrakk> \<Longrightarrow> par_tr_fin_principle (do x <- f;
env_n_steps (Suc n)
od) proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>par_tr_fin_principle f \<Longrightarrow> par_tr_fin_principle (do x <- f;
env_n_steps n
od); par_tr_fin_principle f\<rbrakk> \<Longrightarrow> par_tr_fin_principle (do x <- f;
env_n_steps (Suc n)
od) proof (state)
this:
par_tr_fin_principle f \<Longrightarrow> par_tr_fin_principle (do x <- f;
env_n_steps n
od)
par_tr_fin_principle f

goal (1 subgoal):
 1. \<And>n. \<lbrakk>par_tr_fin_principle f \<Longrightarrow> par_tr_fin_principle (do x <- f;
env_n_steps n
od); par_tr_fin_principle f\<rbrakk> \<Longrightarrow> par_tr_fin_principle (do x <- f;
env_n_steps (Suc n)
od) proof (state)
this:
f' \<equiv> do x <- f;
env_n_steps n
od

goal (1 subgoal):
 1. \<And>n. \<lbrakk>par_tr_fin_principle f \<Longrightarrow> par_tr_fin_principle (do x <- f;
env_n_steps n
od); par_tr_fin_principle f\<rbrakk> \<Longrightarrow> par_tr_fin_principle (do x <- f;
env_n_steps (Suc n)
od) proof (chain)
picking this:
par_tr_fin_principle f \<Longrightarrow> par_tr_fin_principle (do x <- f;
env_n_steps n
od)
par_tr_fin_principle f proof (prove)
using this:
par_tr_fin_principle f \<Longrightarrow> par_tr_fin_principle (do x <- f;
env_n_steps n
od)
par_tr_fin_principle f

goal (1 subgoal):
 1. par_tr_fin_principle f' proof (state)
this:
par_tr_fin_principle f'

goal (1 subgoal):
 1. \<And>n. \<lbrakk>par_tr_fin_principle f \<Longrightarrow> par_tr_fin_principle (do x <- f;
env_n_steps n
od); par_tr_fin_principle f\<rbrakk> \<Longrightarrow> par_tr_fin_principle (do x <- f;
env_n_steps (Suc n)
od) proof (prove)
using this:
par_tr_fin_principle f'

goal (1 subgoal):
 1. par_tr_fin_principle (do x <- f';
env_n_steps 1
od) proof (state)
this:
par_tr_fin_principle (do x <- f';
env_n_steps 1
od)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>par_tr_fin_principle f \<Longrightarrow> par_tr_fin_principle (do x <- f;
env_n_steps n
od); par_tr_fin_principle f\<rbrakk> \<Longrightarrow> par_tr_fin_principle (do x <- f;
env_n_steps (Suc n)
od) proof (chain)
picking this:
par_tr_fin_principle (do x <- f';
env_n_steps 1
od) proof (prove)
using this:
par_tr_fin_principle (do x <- f';
env_n_steps 1
od)

goal (1 subgoal):
 1. par_tr_fin_principle (do x <- f;
env_n_steps (Suc n)
od) proof (state)
this:
par_tr_fin_principle (do x <- f;
env_n_steps (Suc n)
od)

goal:
No subgoals!