theory Prefix_Refinement

lemma prefix_refinement_bind_v[rule_format]:
  "prefix_refinement sr isr intsr rvr P Q AR R a c
    \<Longrightarrow> (\<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y))
    \<Longrightarrow> \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace> \<Longrightarrow> \<lbrace>Q'\<rbrace>,\<lbrace>R\<rbrace> c \<lbrace>\<top>\<top>\<rbrace>,\<lbrace>Q''\<rbrace>
    \<Longrightarrow> prefix_refinement sr isr osr rvr' (\<lambda>s0. P s0 and P') (Q and Q') AR R (a >>= b) (c >>= d)" apply (rule prefix_refinement_weaken_pre,
    rule prefix_refinement_bind_general[where P'="\<lambda>_. P'"]) apply assumption apply (elim allE, erule(1) mp) apply (rule disjI2) apply simp apply assumption apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr isr osr rvr' (\<lambda>s0. P s0 and P') (Q and Q') AR R (a >>= b) (c >>= d) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr isr ?intsr4 ?rvr4 ?P4 ?Q4 AR R a c
 2. \<And>x y. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>; ?rvr4 x y\<rbrakk> \<Longrightarrow> prefix_refinement sr ?intsr4 osr rvr' (?P''4 x) (?Q''4 y) AR R (b x) (d y)
 3. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. P'\<rbrace>, \<lbrace>AR\<rbrace> a -, \<lbrace>?P''4\<rbrace> \<or> \<lbrace>\<lambda>s. \<exists>s0. P' s\<rbrace> a \<lbrace>\<lambda>rv s. \<forall>s0. ?P''4 rv s0 s\<rbrace>
 4. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>?Q''4\<rbrace>
 5. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s s0. (P s0 and P') s \<longrightarrow> (?P4 and (\<lambda>_. P')) s0 s
 6. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> (P s0 and P') s \<longrightarrow> (Q and Q') t0 t \<longrightarrow> (?Q4 and ?Q'4) t0 t proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>; rvr x y\<rbrakk> \<Longrightarrow> prefix_refinement sr intsr osr rvr' (?P''4 x) (?Q''4 y) AR R (b x) (d y)
 2. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. P'\<rbrace>, \<lbrace>AR\<rbrace> a -, \<lbrace>?P''4\<rbrace> \<or> \<lbrace>\<lambda>s. \<exists>s0. P' s\<rbrace> a \<lbrace>\<lambda>rv s. \<forall>s0. ?P''4 rv s0 s\<rbrace>
 3. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>?Q''4\<rbrace>
 4. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s s0. (P s0 and P') s \<longrightarrow> (P and (\<lambda>_. P')) s0 s
 5. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> (P s0 and P') s \<longrightarrow> (Q and Q') t0 t \<longrightarrow> (Q and ?Q'4) t0 t proof (prove)
goal (4 subgoals):
 1. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. P'\<rbrace>, \<lbrace>AR\<rbrace> a -, \<lbrace>\<lambda>x s0. P'' x\<rbrace> \<or> \<lbrace>\<lambda>s. \<exists>s0. P' s\<rbrace> a \<lbrace>\<lambda>rv s. \<forall>s0. P'' rv s\<rbrace>
 2. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>
 3. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s s0. (P s0 and P') s \<longrightarrow> (P and (\<lambda>_. P')) s0 s
 4. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> (P s0 and P') s \<longrightarrow> (Q and Q') t0 t \<longrightarrow> (Q and ?Q'4) t0 t proof (prove)
goal (4 subgoals):
 1. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>s0. P' s\<rbrace> a \<lbrace>\<lambda>rv s. \<forall>s0. P'' rv s\<rbrace>
 2. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>
 3. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s s0. (P s0 and P') s \<longrightarrow> (P and (\<lambda>_. P')) s0 s
 4. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> (P s0 and P') s \<longrightarrow> (Q and Q') t0 t \<longrightarrow> (Q and ?Q'4) t0 t proof (prove)
goal (3 subgoals):
 1. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>
 2. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s s0. (P s0 and P') s \<longrightarrow> (P and (\<lambda>_. P')) s0 s
 3. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> (P s0 and P') s \<longrightarrow> (Q and Q') t0 t \<longrightarrow> (Q and ?Q'4) t0 t proof (prove)
goal (2 subgoals):
 1. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s s0. (P s0 and P') s \<longrightarrow> (P and (\<lambda>_. P')) s0 s
 2. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> (P s0 and P') s \<longrightarrow> (Q and Q') t0 t \<longrightarrow> (Q and Q') t0 t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_refinement sr isr intsr rvr P Q AR R a c; \<forall>x y. rvr x y \<longrightarrow> prefix_refinement sr intsr osr rvr' (\<lambda>s0. P'' x) (Q'' y) AR R (b x) (d y); \<lbrace>P'\<rbrace> a \<lbrace>P''\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> c -, \<lbrace>Q''\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> (P s0 and P') s \<longrightarrow> (Q and Q') t0 t \<longrightarrow> (Q and Q') t0 t proof (prove)
goal:
No subgoals!