theory Prefix_Refinement

lemma prefix_refinement_modify:
  "\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t)
    \<Longrightarrow> prefix_refinement sr isr osr (\<lambda>_ _. True) (\<lambda>_. P) (\<lambda>_. Q) AR R (modify f) (modify g)" apply (simp add: modify_def) apply (rule prefix_refinement_weaken_pre) apply (rule prefix_refinement_bind[where intsr=isr, OF prefix_refinement_get]) apply (rule_tac P="P x" in prefix_refinement_assume_pre(1)) apply (rule_tac P="Q y" in prefix_refinement_assume_pre(2)) apply (rule prefix_refinement_put, simp) apply wp+ apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> prefix_refinement sr isr osr (\<lambda>_ _. True) (\<lambda>_. P) (\<lambda>_. Q) AR R (modify f) (modify g) proof (prove)
goal (1 subgoal):
 1. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> prefix_refinement sr isr osr (\<lambda>_ _. True) (\<lambda>_. P) (\<lambda>_. Q) AR R (do s <- get;
put (f s)
od) (do s <- get;
put (g s)
od) proof (prove)
goal (3 subgoals):
 1. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> prefix_refinement sr isr osr (\<lambda>_ _. True) ?P' ?Q' AR R (do s <- get;
put (f s)
od) (do s <- get;
put (g s)
od)
 2. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> \<forall>s s0. P s \<longrightarrow> ?P' s0 s
 3. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> \<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> ?Q' t0 t proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t); isr x y\<rbrakk> \<Longrightarrow> prefix_refinement sr isr osr (\<lambda>_ _. True) (?P''4 x) (?Q''4 y) AR R (put (f x)) (put (g y))
 2. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> \<lbrace>?P'4\<rbrace>, \<lbrace>AR\<rbrace> get -, \<lbrace>?P''4\<rbrace>
 3. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> \<lbrace>?Q'4\<rbrace>, \<lbrace>R\<rbrace> get -, \<lbrace>?Q''4\<rbrace>
 4. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> \<forall>s s0. P s \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 5. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> \<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> ((\<lambda>_ _. True) and ?Q'4) t0 t proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t); isr x y; P x\<rbrakk> \<Longrightarrow> prefix_refinement sr isr osr (\<lambda>_ _. True) (?P'10 x) (?Q''4 y) AR R (put (f x)) (put (g y))
 2. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> \<lbrace>?P'4\<rbrace>, \<lbrace>AR\<rbrace> get -, \<lbrace>\<lambda>x. ?P'10 x and (\<lambda>_ _. P x)\<rbrace>
 3. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> \<lbrace>?Q'4\<rbrace>, \<lbrace>R\<rbrace> get -, \<lbrace>?Q''4\<rbrace>
 4. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> \<forall>s s0. P s \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 5. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> \<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> ((\<lambda>_ _. True) and ?Q'4) t0 t proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t); isr x y; P x; Q y\<rbrakk> \<Longrightarrow> prefix_refinement sr isr osr (\<lambda>_ _. True) (?P'10 x) (?Q'12 y) AR R (put (f x)) (put (g y))
 2. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> \<lbrace>?P'4\<rbrace>, \<lbrace>AR\<rbrace> get -, \<lbrace>\<lambda>x. ?P'10 x and (\<lambda>_ _. P x)\<rbrace>
 3. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> \<lbrace>?Q'4\<rbrace>, \<lbrace>R\<rbrace> get -, \<lbrace>\<lambda>y. ?Q'12 y and (\<lambda>_ _. Q y)\<rbrace>
 4. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> \<forall>s s0. P s \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 5. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> \<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> ((\<lambda>_ _. True) and ?Q'4) t0 t proof (prove)
goal (4 subgoals):
 1. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> \<lbrace>?P'4\<rbrace>, \<lbrace>AR\<rbrace> get -, \<lbrace>\<lambda>x. (\<lambda>_ _. True) and (\<lambda>_ _. P x)\<rbrace>
 2. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> \<lbrace>?Q'4\<rbrace>, \<lbrace>R\<rbrace> get -, \<lbrace>\<lambda>y. (\<lambda>_ _. True) and (\<lambda>_ _. Q y)\<rbrace>
 3. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> \<forall>s s0. P s \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 4. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> \<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> ((\<lambda>_ _. True) and ?Q'4) t0 t proof (prove)
goal (2 subgoals):
 1. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> \<forall>s s0. P s \<longrightarrow> ((\<lambda>_ _. True) and (\<lambda>s0 s. ((\<lambda>_ _. True) and (\<lambda>_ _. P s)) s0 s)) s0 s
 2. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> \<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> ((\<lambda>_ _. True) and (\<lambda>s0 s. ((\<lambda>_ _. True) and (\<lambda>_ _. Q s)) s0 s)) t0 t proof (prove)
goal (1 subgoal):
 1. \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> osr (f s) (g t) \<Longrightarrow> \<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> ((\<lambda>_ _. True) and (\<lambda>s0 s. ((\<lambda>_ _. True) and (\<lambda>_ _. Q s)) s0 s)) t0 t proof (prove)
goal:
No subgoals!