theory Bisim_UL

lemma bisim_symb_exec_r:
  assumes  z: "\<And>rv. bisim_underlying sr r P (Q' rv) x (y rv)"
  assumes  y: "\<lbrace>P'\<rbrace> m \<lbrace>Q'\<rbrace>"
  assumes  x: "\<And>s. \<lbrace>Pe and (=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>"
  assumes ne: "not_empty Pd m"
  shows      "bisim_underlying sr r P (P' and Pe and Pd) x (m >>= (\<lambda>rv. y rv))" apply (rule bisim_guard_imp) apply (subst gets_bind_ign [symmetric], rule bisim_split) apply (rule bisim_noop [OF _ x not_empty_gets]) apply (rule hoare_pre, wp) apply fastforce apply (rule ne) apply (rule z) apply (wp y)+ apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim_underlying sr r P (P' and Pe and Pd) x (m >>= y) proof (prove)
goal (3 subgoals):
 1. bisim_underlying sr r ?Q ?Q' x (m >>= y)
 2. \<And>s. P s \<Longrightarrow> ?Q s
 3. \<And>s. (P' and Pe and Pd) s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. bisim_underlying sr ?R'7 ?P7 ?P'7 (gets ?f5) m
 2. \<And>ra r'. ?R'7 ra r' \<Longrightarrow> bisim_underlying sr r (?Q7 ra) (?Q'7 r') x (y r')
 3. \<lbrace>?S7\<rbrace> gets ?f5 \<lbrace>?Q7\<rbrace>
 4. \<lbrace>?S'7\<rbrace> m \<lbrace>?Q'7\<rbrace>
 5. \<And>s. P s \<Longrightarrow> (?P7 and ?S7) s
 6. \<And>s. (P' and Pe and Pd) s \<Longrightarrow> (?P'7 and ?S'7) s proof (prove)
goal (7 subgoals):
 1. \<And>s. \<lbrace>?Pa12 and (=) s\<rbrace> gets ?f5 \<lbrace>\<lambda>_. (=) s\<rbrace>
 2. not_empty ?P'12 m
 3. \<And>ra r'. dc ra r' \<Longrightarrow> bisim_underlying sr r (?Q7 ra) (?Q'7 r') x (y r')
 4. \<lbrace>?S7\<rbrace> gets ?f5 \<lbrace>?Q7\<rbrace>
 5. \<lbrace>?S'7\<rbrace> m \<lbrace>?Q'7\<rbrace>
 6. \<And>s. P s \<Longrightarrow> (?Pa12 and (\<lambda>_. True) and ?S7) s
 7. \<And>s. (P' and Pe and Pd) s \<Longrightarrow> (Pe and ?P'12 and ?S'7) s proof (prove)
goal (7 subgoals):
 1. \<And>s sa. (?Pa12 and (=) s) sa \<Longrightarrow> s = sa
 2. not_empty ?P'12 m
 3. \<And>ra r'. dc ra r' \<Longrightarrow> bisim_underlying sr r (?Q7 ra) (?Q'7 r') x (y r')
 4. \<lbrace>?S7\<rbrace> gets ?f5 \<lbrace>?Q7\<rbrace>
 5. \<lbrace>?S'7\<rbrace> m \<lbrace>?Q'7\<rbrace>
 6. \<And>s. P s \<Longrightarrow> (?Pa12 and (\<lambda>_. True) and ?S7) s
 7. \<And>s. (P' and Pe and Pd) s \<Longrightarrow> (Pe and ?P'12 and ?S'7) s proof (prove)
goal (6 subgoals):
 1. not_empty ?P'12 m
 2. \<And>ra r'. dc ra r' \<Longrightarrow> bisim_underlying sr r (?Q7 ra) (?Q'7 r') x (y r')
 3. \<lbrace>?S7\<rbrace> gets ?f5 \<lbrace>?Q7\<rbrace>
 4. \<lbrace>?S'7\<rbrace> m \<lbrace>?Q'7\<rbrace>
 5. \<And>s. P s \<Longrightarrow> (?Pa12 and (\<lambda>_. True) and ?S7) s
 6. \<And>s. (P' and Pe and Pd) s \<Longrightarrow> (Pe and ?P'12 and ?S'7) s proof (prove)
goal (5 subgoals):
 1. \<And>ra r'. dc ra r' \<Longrightarrow> bisim_underlying sr r (?Q7 ra) (?Q'7 r') x (y r')
 2. \<lbrace>?S7\<rbrace> gets ?f5 \<lbrace>?Q7\<rbrace>
 3. \<lbrace>?S'7\<rbrace> m \<lbrace>?Q'7\<rbrace>
 4. \<And>s. P s \<Longrightarrow> (?Pa12 and (\<lambda>_. True) and ?S7) s
 5. \<And>s. (P' and Pe and Pd) s \<Longrightarrow> (Pe and Pd and ?S'7) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?S7\<rbrace> gets ?f5 \<lbrace>\<lambda>r. P\<rbrace>
 2. \<lbrace>?S'7\<rbrace> m \<lbrace>Q'\<rbrace>
 3. \<And>s. P s \<Longrightarrow> (?Pa12 and (\<lambda>_. True) and ?S7) s
 4. \<And>s. (P' and Pe and Pd) s \<Longrightarrow> (Pe and Pd and ?S'7) s proof (prove)
goal (2 subgoals):
 1. \<And>s. P s \<Longrightarrow> (?Pa12 and (\<lambda>_. True) and P) s
 2. \<And>s. (P' and Pe and Pd) s \<Longrightarrow> (Pe and Pd and P') s proof (prove)
goal:
No subgoals!