[STATEMENT]
lemma valid_refs_inv_dequeue_Mutate:
  fixes s :: "('field, 'mut, 'payload, 'ref) lsts"
  assumes vri: "valid_refs_inv s"
  assumes sb: "sys_mem_store_buffers (mutator m') s = mw_Mutate r f opt_r' # ws"
  shows "valid_refs_inv (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)),
                                        mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))" (is "valid_refs_inv ?s'")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_refs_inv (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))
[PROOF STEP]
proof(rule valid_refs_invI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m x y. \<lbrakk>(x reaches y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)); x \<in> roots ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> ghost_honorary_root ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> mut_m.tso_store_refs m (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) \<or> grey x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))\<rbrakk> \<Longrightarrow> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m x y. \<lbrakk>(x reaches y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)); x \<in> roots ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> ghost_honorary_root ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> mut_m.tso_store_refs m (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) \<or> grey x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))\<rbrakk> \<Longrightarrow> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))
[PROOF STEP]
let ?root = "\<lambda>m x. mut_m.root m x \<^bold>\<or> grey x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m x y. \<lbrakk>(x reaches y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)); x \<in> roots ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> ghost_honorary_root ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> mut_m.tso_store_refs m (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) \<or> grey x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))\<rbrakk> \<Longrightarrow> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m x y. \<lbrakk>(x reaches y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)); x \<in> roots ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> ghost_honorary_root ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> mut_m.tso_store_refs m (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) \<or> grey x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))\<rbrakk> \<Longrightarrow> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))
[PROOF STEP]
assume xy: "(x reaches y) ?s'" and x: "?root m x ?s'"
[PROOF STATE]
proof (state)
this:
(x reaches y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))
x \<in> roots ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> ghost_honorary_root ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> mut_m.tso_store_refs m (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) \<or> grey x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))

goal (1 subgoal):
 1. \<And>m x y. \<lbrakk>(x reaches y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)); x \<in> roots ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> ghost_honorary_root ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> mut_m.tso_store_refs m (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) \<or> grey x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))\<rbrakk> \<Longrightarrow> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))
[PROOF STEP]
from xy
[PROOF STATE]
proof (chain)
picking this:
(x reaches y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))
[PROOF STEP]
have "(\<exists>m x. ?root m x s \<and> (x reaches y) s) \<and> valid_ref y ?s'"
[PROOF STATE]
proof (prove)
using this:
(x reaches y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))

goal (1 subgoal):
 1. (\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (x reaches y) s) \<and> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))
[PROOF STEP]
unfolding reaches_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x y. (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)))\<^sup>*\<^sup>* x y

goal (1 subgoal):
 1. (\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y) \<and> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<exists>m xa. (xa \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey xa s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x) \<and> obj_at (\<lambda>s. True) x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))
 2. \<And>y z. \<lbrakk>(\<lambda>x y. (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)))\<^sup>*\<^sup>* x y; (y points_to z) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)); (\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y) \<and> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))\<rbrakk> \<Longrightarrow> (\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x z) \<and> obj_at (\<lambda>s. True) z (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))
[PROOF STEP]
case base
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (\<exists>m xa. (xa \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey xa s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x) \<and> obj_at (\<lambda>s. True) x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))
 2. \<And>y z. \<lbrakk>(\<lambda>x y. (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)))\<^sup>*\<^sup>* x y; (y points_to z) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)); (\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y) \<and> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))\<rbrakk> \<Longrightarrow> (\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x z) \<and> obj_at (\<lambda>s. True) z (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))
[PROOF STEP]
with x sb vri
[PROOF STATE]
proof (chain)
picking this:
x \<in> roots ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> ghost_honorary_root ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> mut_m.tso_store_refs m (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) \<or> grey x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))
sys_mem_store_buffers (mutator m') s = mw_Mutate r f opt_r' # ws
valid_refs_inv s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> roots ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> ghost_honorary_root ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> mut_m.tso_store_refs m (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) \<or> grey x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))
sys_mem_store_buffers (mutator m') s = mw_Mutate r f opt_r' # ws
valid_refs_inv s

goal (1 subgoal):
 1. (\<exists>m xa. (xa \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey xa s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x) \<and> obj_at (\<lambda>s. True) x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> roots ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> ghost_honorary_root ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> mut_m.tso_store_refs m (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) \<or> grey x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)); sys_mem_store_buffers (mutator m') s = mw_Mutate r f opt_r' # ws; valid_refs_inv s\<rbrakk> \<Longrightarrow> (\<exists>m xa. (xa \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey xa s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x) \<and> obj_at (\<lambda>s. True) x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))
[PROOF STEP]
apply (subst obj_at_fun_upd)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> roots ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> ghost_honorary_root ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> mut_m.tso_store_refs m (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) \<or> grey x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)); sys_mem_store_buffers (mutator m') s = mw_Mutate r f opt_r' # ws; valid_refs_inv s\<rbrakk> \<Longrightarrow> map_option (\<lambda>s. True) (sys_heap (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) x) = map_option (\<lambda>s. True) (sys_heap s x)
 2. \<lbrakk>x \<in> roots ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> ghost_honorary_root ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> mut_m.tso_store_refs m (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) \<or> grey x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)); sys_mem_store_buffers (mutator m') s = mw_Mutate r f opt_r' # ws; valid_refs_inv s\<rbrakk> \<Longrightarrow> (\<exists>m xa. (xa \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey xa s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x) \<and> obj_at (\<lambda>s. True) x s
[PROOF STEP]
apply (auto simp: mut_m.tso_store_refs_def reaches_def fun_upd_apply split: if_splits intro: valid_refs_invD(5)[where m=m])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>sys_mem_store_buffers (mutator m') s = mw_Mutate r f opt_r' # ws; valid_refs_inv s; m = m'; xa \<in> set ws; x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> \<exists>m xa. (xa \<in> roots (s (mutator m)) \<or> xa \<in> ghost_honorary_root (s (mutator m)) \<or> (\<exists>xaa\<in>set (sys_mem_store_buffers (mutator m) s). xa \<in> (case xaa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})) \<or> grey xa s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x
[PROOF STEP]
apply (metis list.set_intros(2) rtranclp.rtrancl_refl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<exists>m xa. (xa \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey xa s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x) \<and> obj_at (\<lambda>s. True) x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(\<lambda>x y. (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)))\<^sup>*\<^sup>* x y; (y points_to z) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)); (\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y) \<and> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))\<rbrakk> \<Longrightarrow> (\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x z) \<and> obj_at (\<lambda>s. True) z (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))
[PROOF STEP]
(* FIXME rules *)
[PROOF STATE]
proof (state)
this:
(\<exists>m xa. (xa \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey xa s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x) \<and> obj_at (\<lambda>s. True) x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(\<lambda>x y. (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)))\<^sup>*\<^sup>* x y; (y points_to z) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)); (\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y) \<and> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))\<rbrakk> \<Longrightarrow> (\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x z) \<and> obj_at (\<lambda>s. True) z (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(\<lambda>x y. (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)))\<^sup>*\<^sup>* x y; (y points_to z) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)); (\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y) \<and> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))\<rbrakk> \<Longrightarrow> (\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x z) \<and> obj_at (\<lambda>s. True) z (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))
[PROOF STEP]
case (step y z)
[PROOF STATE]
proof (state)
this:
(\<lambda>x y. (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)))\<^sup>*\<^sup>* x y
(y points_to z) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))
(\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y) \<and> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(\<lambda>x y. (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)))\<^sup>*\<^sup>* x y; (y points_to z) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)); (\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y) \<and> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))\<rbrakk> \<Longrightarrow> (\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x z) \<and> obj_at (\<lambda>s. True) z (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))
[PROOF STEP]
with sb vri
[PROOF STATE]
proof (chain)
picking this:
sys_mem_store_buffers (mutator m') s = mw_Mutate r f opt_r' # ws
valid_refs_inv s
(\<lambda>x y. (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)))\<^sup>*\<^sup>* x y
(y points_to z) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))
(\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y) \<and> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sys_mem_store_buffers (mutator m') s = mw_Mutate r f opt_r' # ws
valid_refs_inv s
(\<lambda>x y. (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)))\<^sup>*\<^sup>* x y
(y points_to z) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))
(\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y) \<and> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))

goal (1 subgoal):
 1. (\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x z) \<and> obj_at (\<lambda>s. True) z (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_mem_store_buffers (mutator m') s = mw_Mutate r f opt_r' # ws; valid_refs_inv s; (\<lambda>x y. (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)))\<^sup>*\<^sup>* x y; (y points_to z) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)); (\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y) \<and> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))\<rbrakk> \<Longrightarrow> (\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x z) \<and> obj_at (\<lambda>s. True) z (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))
[PROOF STEP]
apply (subst obj_at_fun_upd, clarsimp simp: fun_upd_apply)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_mem_store_buffers (mutator m') s = mw_Mutate r f opt_r' # ws; valid_refs_inv s; (\<lambda>x y. (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)))\<^sup>*\<^sup>* x y; (y points_to z) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)); (\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y) \<and> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))\<rbrakk> \<Longrightarrow> (\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x z) \<and> obj_at (\<lambda>s. True) z s
[PROOF STEP]
apply (subst (asm) obj_at_fun_upd, fastforce simp: fun_upd_apply)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_mem_store_buffers (mutator m') s = mw_Mutate r f opt_r' # ws; valid_refs_inv s; (\<lambda>x y. (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)))\<^sup>*\<^sup>* x y; (y points_to z) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)); (\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y) \<and> obj_at (\<lambda>s. True) y s\<rbrakk> \<Longrightarrow> (\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x z) \<and> obj_at (\<lambda>s. True) z s
[PROOF STEP]
apply (clarsimp simp: points_to_Mutate fun_upd_apply)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m xa. \<lbrakk>sys_mem_store_buffers (mutator m') s = mw_Mutate r f opt_r' # ws; valid_refs_inv s; (\<lambda>x y. r \<noteq> x \<and> (x points_to y) s \<or> r = x \<and> obj_at (\<lambda>s. True) r s \<and> (opt_r' = Some y \<or> (x points_to y) s \<and> obj_at (\<lambda>obj. \<exists>f'. obj_fields obj f' = Some y \<and> f \<noteq> f') r s))\<^sup>*\<^sup>* x y; r \<noteq> y \<and> (y points_to z) s \<or> r = y \<and> obj_at (\<lambda>s. True) r s \<and> (opt_r' = Some z \<or> (y points_to z) s \<and> obj_at (\<lambda>obj. \<exists>f'. obj_fields obj f' = Some z \<and> f \<noteq> f') r s); obj_at (\<lambda>s. True) y s; xa \<in> roots (s (mutator m)) \<or> xa \<in> ghost_honorary_root (s (mutator m)) \<or> xa \<in> mut_m.tso_store_refs m s \<or> grey xa s; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa y\<rbrakk> \<Longrightarrow> (\<exists>m x. (x \<in> roots (s (mutator m)) \<or> x \<in> ghost_honorary_root (s (mutator m)) \<or> x \<in> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x z) \<and> obj_at (\<lambda>s. True) z s
[PROOF STEP]
apply (fastforce elim: rtranclp.intros(2) simp: mut_m.tso_store_refs_def reaches_def fun_upd_apply intro: exI[where x=m'] valid_refs_invD(5)[where m=m'])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x z) \<and> obj_at (\<lambda>s. True) z (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (\<lambda>a. sys_mem_store_buffers a s)(mutator m' := ws)\<rparr>))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (x reaches y) s) \<and> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))

goal (1 subgoal):
 1. \<And>m x y. \<lbrakk>(x reaches y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)); x \<in> roots ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> ghost_honorary_root ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) (mutator m)) \<union> mut_m.tso_store_refs m (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>)) \<or> grey x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))\<rbrakk> \<Longrightarrow> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (x reaches y) s) \<and> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))
[PROOF STEP]
show "valid_ref y ?s'"
[PROOF STATE]
proof (prove)
using this:
(\<exists>m x. (x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s) \<and> (x reaches y) s) \<and> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))

goal (1 subgoal):
 1. obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := ws)\<rparr>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_refs_inv_dequeue_Mutate_Payload:
  notes if_split_asm[split del]
  fixes s :: "('field, 'mut, 'payload, 'ref) lsts"
  assumes vri: "valid_refs_inv s"
  assumes sb: "sys_mem_store_buffers (mutator m') s = mw_Mutate_Payload r f pl # ws"
  shows "valid_refs_inv (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_payload := (obj_payload obj)(f := pl)\<rparr>) (sys_heap s r)),
                                        mem_store_buffers := (mem_store_buffers (s sys))(mutator m := ws)\<rparr>))" (is "valid_refs_inv ?s'")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_refs_inv (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_payload := (obj_payload obj)(f := pl)\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m := ws)\<rparr>))
[PROOF STEP]
apply (rule valid_refs_invI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ma x y. \<lbrakk>(x reaches y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_payload := (obj_payload obj)(f := pl)\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m := ws)\<rparr>)); x \<in> roots ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_payload := (obj_payload obj)(f := pl)\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m := ws)\<rparr>)) (mutator ma)) \<union> ghost_honorary_root ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_payload := (obj_payload obj)(f := pl)\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m := ws)\<rparr>)) (mutator ma)) \<union> mut_m.tso_store_refs ma (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_payload := (obj_payload obj)(f := pl)\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m := ws)\<rparr>)) \<or> grey x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_payload := (obj_payload obj)(f := pl)\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m := ws)\<rparr>))\<rbrakk> \<Longrightarrow> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_payload := (obj_payload obj)(f := pl)\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m := ws)\<rparr>))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
valid_refs_inv s
sys_mem_store_buffers (mutator m') s = mw_Mutate_Payload r f pl # ws

goal (1 subgoal):
 1. \<And>ma x y. \<lbrakk>(x reaches y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_payload := (obj_payload obj)(f := pl)\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m := ws)\<rparr>)); x \<in> roots ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_payload := (obj_payload obj)(f := pl)\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m := ws)\<rparr>)) (mutator ma)) \<union> ghost_honorary_root ((s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_payload := (obj_payload obj)(f := pl)\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m := ws)\<rparr>)) (mutator ma)) \<union> mut_m.tso_store_refs ma (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_payload := (obj_payload obj)(f := pl)\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m := ws)\<rparr>)) \<or> grey x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_payload := (obj_payload obj)(f := pl)\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m := ws)\<rparr>))\<rbrakk> \<Longrightarrow> obj_at (\<lambda>s. True) y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_payload := (obj_payload obj)(f := pl)\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(mutator m := ws)\<rparr>))
[PROOF STEP]
apply (clarsimp simp: valid_refs_invD fun_upd_apply split: obj_at_splits mem_store_action.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ma x y. \<lbrakk>(x reaches y) s; x \<in> roots (s (mutator ma)) \<or> x \<in> ghost_honorary_root (s (mutator ma)) \<or> x \<in> (if m = ma then \<Union> (store_refs ` set ws) else mut_m.tso_store_refs ma s) \<or> grey x s; valid_refs_inv s; sys_mem_store_buffers (mutator m') s = mw_Mutate_Payload r f pl # ws\<rbrakk> \<Longrightarrow> \<exists>ya. sys_heap s y = Some ya
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ma x y. \<lbrakk>(x reaches y) s; valid_refs_inv s; sys_mem_store_buffers (mutator m') s = mw_Mutate_Payload r f pl # ws; x \<in> (if m = ma then \<Union> (store_refs ` set ws) else mut_m.tso_store_refs ma s)\<rbrakk> \<Longrightarrow> \<exists>ya. sys_heap s y = Some ya
 2. \<And>x y. \<lbrakk>(x reaches y) s; valid_refs_inv s; sys_mem_store_buffers (mutator m') s = mw_Mutate_Payload r f pl # ws; grey x s\<rbrakk> \<Longrightarrow> \<exists>ya. sys_heap s y = Some ya
[PROOF STEP]
apply (metis (mono_tags, lifting) UN_insert Un_iff list.simps(15) mut_m.tso_store_refs_def valid_refs_invD(4))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>(x reaches y) s; valid_refs_inv s; sys_mem_store_buffers (mutator m') s = mw_Mutate_Payload r f pl # ws; grey x s\<rbrakk> \<Longrightarrow> \<exists>ya. sys_heap s y = Some ya
[PROOF STEP]
apply (metis case_optionE obj_at_def valid_refs_invD(7))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma unfoldE:
  fixes P :: pi
  and   Q :: pi
  and   s :: "(name \<times> name) list"

  assumes "P \<simeq>\<^sup>s Q"

  shows "P[<s>] \<leadsto><weakBisim> Q[<s>]"
  and   "Q[<s>] \<leadsto><weakBisim> P[<s>]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P[<s>] \<leadsto><weakBisim> Q[<s>] &&& Q[<s>] \<leadsto><weakBisim> P[<s>]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P[<s>] \<leadsto><weakBisim> Q[<s>]
 2. Q[<s>] \<leadsto><weakBisim> P[<s>]
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
P \<simeq>\<^sup>s Q
[PROOF STEP]
show "P[<s>] \<leadsto><weakBisim> Q[<s>]"
[PROOF STATE]
proof (prove)
using this:
P \<simeq>\<^sup>s Q

goal (1 subgoal):
 1. P[<s>] \<leadsto><weakBisim> Q[<s>]
[PROOF STEP]
by(force simp add: congruenceSubstDef)
[PROOF STATE]
proof (state)
this:
P[<s>] \<leadsto><weakBisim> Q[<s>]

goal (1 subgoal):
 1. Q[<s>] \<leadsto><weakBisim> P[<s>]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Q[<s>] \<leadsto><weakBisim> P[<s>]
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
P \<simeq>\<^sup>s Q
[PROOF STEP]
show "Q[<s>] \<leadsto><weakBisim> P[<s>]"
[PROOF STATE]
proof (prove)
using this:
P \<simeq>\<^sup>s Q

goal (1 subgoal):
 1. Q[<s>] \<leadsto><weakBisim> P[<s>]
[PROOF STEP]
by(force simp add: congruenceSubstDef)
[PROOF STATE]
proof (state)
this:
Q[<s>] \<leadsto><weakBisim> P[<s>]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unfoldI:
  fixes P :: pi
  and   Q :: pi

  assumes "\<forall>s. P[<s>] \<leadsto><weakBisim> Q[<s>] \<and> Q[<s>] \<leadsto><weakBisim> P[<s>]"

  shows "P \<simeq>\<^sup>s Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<simeq>\<^sup>s Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<simeq>\<^sup>s Q
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<forall>s. P[<s>] \<leadsto><weakBisim> Q[<s>] \<and> Q[<s>] \<leadsto><weakBisim> P[<s>]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>s. P[<s>] \<leadsto><weakBisim> Q[<s>] \<and> Q[<s>] \<leadsto><weakBisim> P[<s>]

goal (1 subgoal):
 1. P \<simeq>\<^sup>s Q
[PROOF STEP]
by(force simp add: congruenceSubstDef)
[PROOF STATE]
proof (state)
this:
P \<simeq>\<^sup>s Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakEqSubset:
  shows "substClosed congruence \<subseteq> weakBisim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. substClosed congruence \<subseteq> weakBisim
[PROOF STEP]
proof(auto simp add: substClosed_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<forall>\<sigma>. a[<\<sigma>>] \<simeq> b[<\<sigma>>] \<Longrightarrow> a \<approx> b
[PROOF STEP]
fix P Q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<forall>\<sigma>. a[<\<sigma>>] \<simeq> b[<\<sigma>>] \<Longrightarrow> a \<approx> b
[PROOF STEP]
assume "\<forall>s. P[<s>] \<simeq> Q[<s>]"
[PROOF STATE]
proof (state)
this:
\<forall>s. P[<s>] \<simeq> Q[<s>]

goal (1 subgoal):
 1. \<And>a b. \<forall>\<sigma>. a[<\<sigma>>] \<simeq> b[<\<sigma>>] \<Longrightarrow> a \<approx> b
[PROOF STEP]
hence "P[<[]>] \<simeq> Q[<[]>]"
[PROOF STATE]
proof (prove)
using this:
\<forall>s. P[<s>] \<simeq> Q[<s>]

goal (1 subgoal):
 1. P[<[]>] \<simeq> Q[<[]>]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P[<[]>] \<simeq> Q[<[]>]

goal (1 subgoal):
 1. \<And>a b. \<forall>\<sigma>. a[<\<sigma>>] \<simeq> b[<\<sigma>>] \<Longrightarrow> a \<approx> b
[PROOF STEP]
thus "P \<approx> Q"
[PROOF STATE]
proof (prove)
using this:
P[<[]>] \<simeq> Q[<[]>]

goal (1 subgoal):
 1. P \<approx> Q
[PROOF STEP]
by(force dest: congruenceWeakBisim intro: Weak_Late_Bisim.unfoldI)
[PROOF STATE]
proof (state)
this:
P \<approx> Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakCongWeakEq:
  fixes P :: pi
  and   Q :: pi

  assumes "P \<simeq>\<^sup>s Q"

  shows "P \<simeq> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<simeq> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<simeq>\<^sup>s Q

goal (1 subgoal):
 1. P \<simeq> Q
[PROOF STEP]
apply(auto simp add: substClosed_def congruenceSubst_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. P[<\<sigma>>] \<simeq> Q[<\<sigma>>] \<Longrightarrow> P \<simeq> Q
[PROOF STEP]
apply(erule_tac x="[]" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P[<[]>] \<simeq> Q[<[]>] \<Longrightarrow> P \<simeq> Q
[PROOF STEP]
by auto


[STATEMENT]
lemma eqvt:
  shows "eqvt (substClosed congruence)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt (substClosed congruence)
[PROOF STEP]
by(rule eqvtSubstClosed[OF Weak_Late_Cong.eqvt])


[STATEMENT]
lemma eqvtI:
  fixes P :: pi
  and   Q :: pi
  and   perm :: "name prm"

  assumes "P \<simeq>\<^sup>s Q"

  shows "(perm \<bullet> P) \<simeq>\<^sup>s (perm \<bullet> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. perm \<bullet> P \<simeq>\<^sup>s perm \<bullet> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<simeq>\<^sup>s Q

goal (1 subgoal):
 1. perm \<bullet> P \<simeq>\<^sup>s perm \<bullet> Q
[PROOF STEP]
by(simp add: congruenceSubst_def) (rule eqvtRelI[OF eqvt])


[STATEMENT]
lemma strongEqWeakCong:
  fixes P :: pi
  and   Q :: pi

  assumes "P \<sim>\<^sup>s Q"

  shows "P \<simeq>\<^sup>s Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<simeq>\<^sup>s Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<sim>\<^sup>s Q

goal (1 subgoal):
 1. P \<simeq>\<^sup>s Q
[PROOF STEP]
by(force intro: strongBisimWeakEq simp add: substClosed_def congruenceSubst_def)


[STATEMENT]
lemma congSubstBisimSubst:
  fixes P :: pi
  and   Q :: pi

  assumes "P \<simeq>\<^sup>s Q"

  shows "P \<approx>\<^sup>s Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<approx>\<^sup>s Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<simeq>\<^sup>s Q

goal (1 subgoal):
 1. P \<approx>\<^sup>s Q
[PROOF STEP]
by(force simp add: congruenceSubst_def substClosed_def intro: congruenceWeakBisim)


[STATEMENT]
lemma reflexive:
  fixes P :: pi

  shows "P \<simeq>\<^sup>s P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<simeq>\<^sup>s P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<simeq>\<^sup>s P
[PROOF STEP]
from Weak_Late_Bisim.reflexive
[PROOF STATE]
proof (chain)
picking this:
?P \<approx> ?P
[PROOF STEP]
have "\<And>P. P \<leadsto><weakBisim> P"
[PROOF STATE]
proof (prove)
using this:
?P \<approx> ?P

goal (1 subgoal):
 1. \<And>P. P \<leadsto><weakBisim> P
[PROOF STEP]
by(blast intro: Weak_Late_Step_Sim.reflexive)
[PROOF STATE]
proof (state)
this:
?P \<leadsto><weakBisim> ?P

goal (1 subgoal):
 1. P \<simeq>\<^sup>s P
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?P \<leadsto><weakBisim> ?P

goal (1 subgoal):
 1. P \<simeq>\<^sup>s P
[PROOF STEP]
by(force simp add: congruenceSubstDef)
[PROOF STATE]
proof (state)
this:
P \<simeq>\<^sup>s P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma symetric:
  fixes P :: pi
  and   Q :: pi

  assumes "P \<simeq>\<^sup>s Q"

  shows "Q \<simeq>\<^sup>s P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<simeq>\<^sup>s P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<simeq>\<^sup>s Q

goal (1 subgoal):
 1. Q \<simeq>\<^sup>s P
[PROOF STEP]
by(force simp add: congruenceSubstDef)


[STATEMENT]
lemma transitive:
  fixes P :: pi
  and   Q :: pi
  and   R :: pi

  assumes "P \<simeq>\<^sup>s Q"
  and     "Q \<simeq>\<^sup>s R"

  shows "P \<simeq>\<^sup>s R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<simeq>\<^sup>s R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<simeq>\<^sup>s Q
Q \<simeq>\<^sup>s R

goal (1 subgoal):
 1. P \<simeq>\<^sup>s R
[PROOF STEP]
by(force simp add: congruenceSubst_def substClosed_def intro: Weak_Late_Cong.transitive)


[STATEMENT]
lemma partUnfold:
  fixes P :: pi
  and   Q :: pi
  and   s :: "(name \<times> name) list"

  assumes "P \<simeq>\<^sup>s Q"

  shows "P[<s>] \<simeq>\<^sup>s Q[<s>]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P[<s>] \<simeq>\<^sup>s Q[<s>]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<simeq>\<^sup>s Q

goal (1 subgoal):
 1. P[<s>] \<simeq>\<^sup>s Q[<s>]
[PROOF STEP]
proof(auto simp add: congruenceSubst_def substClosed_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma>. \<forall>\<sigma>. P[<\<sigma>>] \<simeq> Q[<\<sigma>>] \<Longrightarrow> P[<s>][<\<sigma>>] \<simeq> Q[<s>][<\<sigma>>]
[PROOF STEP]
fix s'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma>. \<forall>\<sigma>. P[<\<sigma>>] \<simeq> Q[<\<sigma>>] \<Longrightarrow> P[<s>][<\<sigma>>] \<simeq> Q[<s>][<\<sigma>>]
[PROOF STEP]
assume "\<forall>s. (P[<s>], Q[<s>]) \<in> congruence"
[PROOF STATE]
proof (state)
this:
\<forall>s. P[<s>] \<simeq> Q[<s>]

goal (1 subgoal):
 1. \<And>\<sigma>. \<forall>\<sigma>. P[<\<sigma>>] \<simeq> Q[<\<sigma>>] \<Longrightarrow> P[<s>][<\<sigma>>] \<simeq> Q[<s>][<\<sigma>>]
[PROOF STEP]
hence "(P[<(s@s')>], Q[<(s@s')>]) \<in> congruence"
[PROOF STATE]
proof (prove)
using this:
\<forall>s. P[<s>] \<simeq> Q[<s>]

goal (1 subgoal):
 1. P[<(s @ s')>] \<simeq> Q[<(s @ s')>]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P[<(s @ s')>] \<simeq> Q[<(s @ s')>]

goal (1 subgoal):
 1. \<And>\<sigma>. \<forall>\<sigma>. P[<\<sigma>>] \<simeq> Q[<\<sigma>>] \<Longrightarrow> P[<s>][<\<sigma>>] \<simeq> Q[<s>][<\<sigma>>]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P[<(s @ s')>] \<simeq> Q[<(s @ s')>]

goal (1 subgoal):
 1. \<And>\<sigma>. \<forall>\<sigma>. P[<\<sigma>>] \<simeq> Q[<\<sigma>>] \<Longrightarrow> P[<s>][<\<sigma>>] \<simeq> Q[<s>][<\<sigma>>]
[PROOF STEP]
have "P[<(s@s')>] = (P[<s>])[<s'>]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P[<(s @ s')>] = P[<s>][<s'>]
[PROOF STEP]
by(induct s', auto)
[PROOF STATE]
proof (state)
this:
P[<(s @ s')>] = P[<s>][<s'>]

goal (1 subgoal):
 1. \<And>\<sigma>. \<forall>\<sigma>. P[<\<sigma>>] \<simeq> Q[<\<sigma>>] \<Longrightarrow> P[<s>][<\<sigma>>] \<simeq> Q[<s>][<\<sigma>>]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P[<(s @ s')>] = P[<s>][<s'>]

goal (1 subgoal):
 1. \<And>\<sigma>. \<forall>\<sigma>. P[<\<sigma>>] \<simeq> Q[<\<sigma>>] \<Longrightarrow> P[<s>][<\<sigma>>] \<simeq> Q[<s>][<\<sigma>>]
[PROOF STEP]
have "Q[<(s@s')>] = (Q[<s>])[<s'>]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q[<(s @ s')>] = Q[<s>][<s'>]
[PROOF STEP]
by(induct s', auto)
[PROOF STATE]
proof (state)
this:
Q[<(s @ s')>] = Q[<s>][<s'>]

goal (1 subgoal):
 1. \<And>\<sigma>. \<forall>\<sigma>. P[<\<sigma>>] \<simeq> Q[<\<sigma>>] \<Longrightarrow> P[<s>][<\<sigma>>] \<simeq> Q[<s>][<\<sigma>>]
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P[<(s @ s')>] \<simeq> Q[<(s @ s')>]
P[<(s @ s')>] = P[<s>][<s'>]
Q[<(s @ s')>] = Q[<s>][<s'>]
[PROOF STEP]
show "((P[<s>])[<s'>], (Q[<s>])[<s'>]) \<in> congruence"
[PROOF STATE]
proof (prove)
using this:
P[<(s @ s')>] \<simeq> Q[<(s @ s')>]
P[<(s @ s')>] = P[<s>][<s'>]
Q[<(s @ s')>] = Q[<s>][<s'>]

goal (1 subgoal):
 1. P[<s>][<s'>] \<simeq> Q[<s>][<s'>]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P[<s>][<s'>] \<simeq> Q[<s>][<s'>]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma initial_abs': "s\<in>wa_initial WAC \<Longrightarrow> \<alpha> s \<in> wa_initial WAA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> wa_initial WAC \<Longrightarrow> \<alpha> s \<in> wa_initial WAA
[PROOF STEP]
using initial_abs
[PROOF STATE]
proof (prove)
using this:
\<alpha> ` wa_initial WAC \<subseteq> wa_initial WAA

goal (1 subgoal):
 1. s \<in> wa_initial WAC \<Longrightarrow> \<alpha> s \<in> wa_initial WAA
[PROOF STEP]
by auto


[STATEMENT]
lemma invar_abs': "s\<in>wa_invar WAC \<Longrightarrow> \<alpha> s \<in> wa_invar WAA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> wa_invar WAC \<Longrightarrow> \<alpha> s \<in> wa_invar WAA
[PROOF STEP]
using invar_abs
[PROOF STATE]
proof (prove)
using this:
\<alpha> ` wa_invar WAC \<subseteq> wa_invar WAA

goal (1 subgoal):
 1. s \<in> wa_invar WAC \<Longrightarrow> \<alpha> s \<in> wa_invar WAA
[PROOF STEP]
by auto


[STATEMENT]
lemma wa_refine_intro:
  fixes condc :: "'C set" and
        stepc :: "('C\<times>'C) set" and
        initialc :: "'C set" and
        invar_addc :: "'C set"
  fixes WAA :: "'A while_algo"
  fixes \<alpha> :: "'C \<Rightarrow> 'A"
  assumes "while_algo WAA"

  \<comment> \<open>The concrete step preserves the concrete part of the invariant\<close>
  assumes step_invarc:
    "!!s s'. \<lbrakk> s\<in>invar_addc; s\<in>condc; \<alpha> s \<in> wa_invar WAA; (s,s')\<in>stepc \<rbrakk>
              \<Longrightarrow> s'\<in>invar_addc"
  \<comment> \<open>The concrete initial states satisfy the concrete part of the invariant\<close>
  assumes initial_invarc: "initialc \<subseteq> invar_addc"

  \<comment> \<open>Condition implemented correctly\<close>
  assumes cond_abs:
    "!!s. \<lbrakk> s\<in>invar_addc; \<alpha> s \<in> wa_invar WAA; s\<in>condc \<rbrakk> \<Longrightarrow> \<alpha> s \<in> wa_cond WAA"
  \<comment> \<open>Step implemented correctly\<close>
  assumes step_abs:
    "!!s s'. \<lbrakk> s\<in>invar_addc; s\<in>condc; \<alpha> s \<in> wa_invar WAA; (s,s')\<in>stepc \<rbrakk>
             \<Longrightarrow> (\<alpha> s, \<alpha> s')\<in>wa_step WAA"
  \<comment> \<open>Initial states implemented correctly\<close>
  assumes initial_abs: "\<alpha> ` initialc \<subseteq> wa_initial WAA"

  \<comment> \<open>Concrete while-algorithm: The invariant is separated into a concrete and
      an abstract part\<close>
  defines "WAC == \<lparr>
   wa_cond=condc,
   wa_step=stepc,
   wa_initial=initialc,
   wa_invar=(invar_addc \<inter> {s. \<alpha> s\<in> wa_invar WAA}) \<rparr>"

  shows
    "while_algo WAC \<and>
     wa_refine WAC WAA \<alpha>" (is "?T1 \<and> ?T2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. while_algo WAC \<and> wa_refine WAC WAA \<alpha>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. while_algo WAC
 2. wa_refine WAC WAA \<alpha>
[PROOF STEP]
interpret waa: while_algo WAA
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. while_algo WAA
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. while_algo WAC
 2. wa_refine WAC WAA \<alpha>
[PROOF STEP]
show G1: "?T1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. while_algo WAC
[PROOF STEP]
apply (unfold_locales)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>s \<in> wa_invar WAC; s \<in> wa_cond WAC; (s, s') \<in> wa_step WAC\<rbrakk> \<Longrightarrow> s' \<in> wa_invar WAC
 2. wa_initial WAC \<subseteq> wa_invar WAC
 3. wf {(s', s). s \<in> wa_invar WAC \<and> s \<in> wa_cond WAC \<and> (s, s') \<in> wa_step WAC}
[PROOF STEP]
apply (simp_all add: WAC_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>s \<in> invar_addc \<and> \<alpha> s \<in> wa_invar WAA; s \<in> condc; (s, s') \<in> stepc\<rbrakk> \<Longrightarrow> s' \<in> invar_addc \<and> \<alpha> s' \<in> wa_invar WAA
 2. initialc \<subseteq> invar_addc \<and> initialc \<subseteq> {s. \<alpha> s \<in> wa_invar WAA}
 3. wf {(s', s). s \<in> invar_addc \<and> \<alpha> s \<in> wa_invar WAA \<and> s \<in> condc \<and> (s, s') \<in> stepc}
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>s s'. \<lbrakk>s \<in> condc; (s, s') \<in> stepc; s \<in> invar_addc; \<alpha> s \<in> wa_invar WAA\<rbrakk> \<Longrightarrow> s' \<in> invar_addc
 2. \<And>s s'. \<lbrakk>s \<in> condc; (s, s') \<in> stepc; s \<in> invar_addc; \<alpha> s \<in> wa_invar WAA\<rbrakk> \<Longrightarrow> \<alpha> s' \<in> wa_invar WAA
 3. \<And>x. x \<in> initialc \<Longrightarrow> x \<in> invar_addc
 4. \<And>x. x \<in> initialc \<Longrightarrow> \<alpha> x \<in> wa_invar WAA
 5. wf {(s', s). s \<in> invar_addc \<and> \<alpha> s \<in> wa_invar WAA \<and> s \<in> condc \<and> (s, s') \<in> stepc}
[PROOF STEP]
apply (blast intro!: step_invarc)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>s \<in> condc; (s, s') \<in> stepc; s \<in> invar_addc; \<alpha> s \<in> wa_invar WAA\<rbrakk> \<Longrightarrow> \<alpha> s' \<in> wa_invar WAA
 2. \<And>x. x \<in> initialc \<Longrightarrow> x \<in> invar_addc
 3. \<And>x. x \<in> initialc \<Longrightarrow> \<alpha> x \<in> wa_invar WAA
 4. wf {(s', s). s \<in> invar_addc \<and> \<alpha> s \<in> wa_invar WAA \<and> s \<in> condc \<and> (s, s') \<in> stepc}
[PROOF STEP]
apply (frule (3) step_abs)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>s \<in> condc; (s, s') \<in> stepc; s \<in> invar_addc; \<alpha> s \<in> wa_invar WAA; (\<alpha> s, \<alpha> s') \<in> wa_step WAA\<rbrakk> \<Longrightarrow> \<alpha> s' \<in> wa_invar WAA
 2. \<And>x. x \<in> initialc \<Longrightarrow> x \<in> invar_addc
 3. \<And>x. x \<in> initialc \<Longrightarrow> \<alpha> x \<in> wa_invar WAA
 4. wf {(s', s). s \<in> invar_addc \<and> \<alpha> s \<in> wa_invar WAA \<and> s \<in> condc \<and> (s, s') \<in> stepc}
[PROOF STEP]
apply (frule (2) cond_abs)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>s \<in> condc; (s, s') \<in> stepc; s \<in> invar_addc; \<alpha> s \<in> wa_invar WAA; (\<alpha> s, \<alpha> s') \<in> wa_step WAA; \<alpha> s \<in> wa_cond WAA\<rbrakk> \<Longrightarrow> \<alpha> s' \<in> wa_invar WAA
 2. \<And>x. x \<in> initialc \<Longrightarrow> x \<in> invar_addc
 3. \<And>x. x \<in> initialc \<Longrightarrow> \<alpha> x \<in> wa_invar WAA
 4. wf {(s', s). s \<in> invar_addc \<and> \<alpha> s \<in> wa_invar WAA \<and> s \<in> condc \<and> (s, s') \<in> stepc}
[PROOF STEP]
apply (erule (2) waa.step_invar)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> initialc \<Longrightarrow> x \<in> invar_addc
 2. \<And>x. x \<in> initialc \<Longrightarrow> \<alpha> x \<in> wa_invar WAA
 3. wf {(s', s). s \<in> invar_addc \<and> \<alpha> s \<in> wa_invar WAA \<and> s \<in> condc \<and> (s, s') \<in> stepc}
[PROOF STEP]
apply (erule rev_subsetD[OF _ initial_invarc])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> initialc \<Longrightarrow> \<alpha> x \<in> wa_invar WAA
 2. wf {(s', s). s \<in> invar_addc \<and> \<alpha> s \<in> wa_invar WAA \<and> s \<in> condc \<and> (s, s') \<in> stepc}
[PROOF STEP]
apply (insert initial_abs waa.initial_invar) [1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> initialc; \<alpha> ` initialc \<subseteq> wa_initial WAA; wa_initial WAA \<subseteq> wa_invar WAA\<rbrakk> \<Longrightarrow> \<alpha> x \<in> wa_invar WAA
 2. wf {(s', s). s \<in> invar_addc \<and> \<alpha> s \<in> wa_invar WAA \<and> s \<in> condc \<and> (s, s') \<in> stepc}
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(s', s). s \<in> invar_addc \<and> \<alpha> s \<in> wa_invar WAA \<and> s \<in> condc \<and> (s, s') \<in> stepc}
[PROOF STEP]
apply (rule_tac
      r="inv_image { (s',s). s\<in>wa_invar WAA
                     \<and> s\<in>wa_cond WAA
                     \<and> (s,s')\<in>wa_step WAA } \<alpha>"
      in wf_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wf (inv_image {(s', s). s \<in> wa_invar WAA \<and> s \<in> wa_cond WAA \<and> (s, s') \<in> wa_step WAA} \<alpha>)
 2. {(s', s). s \<in> invar_addc \<and> \<alpha> s \<in> wa_invar WAA \<and> s \<in> condc \<and> (s, s') \<in> stepc} \<subseteq> inv_image {(s', s). s \<in> wa_invar WAA \<and> s \<in> wa_cond WAA \<and> (s, s') \<in> wa_step WAA} \<alpha>
[PROOF STEP]
apply (simp add: waa.step_wf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(s', s). s \<in> invar_addc \<and> \<alpha> s \<in> wa_invar WAA \<and> s \<in> condc \<and> (s, s') \<in> stepc} \<subseteq> inv_image {(s', s). s \<in> wa_invar WAA \<and> s \<in> wa_cond WAA \<and> (s, s') \<in> wa_step WAA} \<alpha>
[PROOF STEP]
apply (auto simp add: cond_abs step_abs) [1]
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
while_algo WAC

goal (1 subgoal):
 1. wa_refine WAC WAA \<alpha>
[PROOF STEP]
show ?T2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wa_refine WAC WAA \<alpha>
[PROOF STEP]
apply (unfold_locales)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>s \<in> wa_invar WAC; s \<in> wa_cond WAC\<rbrakk> \<Longrightarrow> \<alpha> s \<in> wa_cond WAA
 2. \<And>s s'. \<lbrakk>s \<in> wa_invar WAC; s \<in> wa_cond WAC; (s, s') \<in> wa_step WAC\<rbrakk> \<Longrightarrow> (\<alpha> s, \<alpha> s') \<in> wa_step WAA
 3. \<alpha> ` wa_initial WAC \<subseteq> wa_initial WAA
 4. \<alpha> ` wa_invar WAC \<subseteq> wa_invar WAA
[PROOF STEP]
apply (auto simp add: cond_abs step_abs initial_abs WAC_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
wa_refine WAC WAA \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed

  \<comment> \<open>After refinement has been shown, this lemma transfers
        the well-definedness property up the refinement chain.
        Like in @{thm [source] wa_refine_intro}, some proof-obligations can
        be discharged by assuming refinement and well-definedness of the
        abstract algorithm.\<close>


[STATEMENT]
lemma (in wa_refine) wa_intro:
  \<comment> \<open>Concrete part of the invariant\<close>
  fixes addi :: "'C set"
  \<comment> \<open>The abstract algorithm is well-defined\<close>
  assumes "while_algo WAA"
  \<comment> \<open>The invariant can be split into concrete and abstract part\<close>
  assumes icf: "wa_invar WAC = addi \<inter> {s. \<alpha> s \<in> wa_invar WAA}"

  \<comment> \<open>The step-relation preserves the concrete part of the invariant\<close>
  assumes step_addi:
    "!!s s'. \<lbrakk> s\<in>addi; s\<in>wa_cond WAC; \<alpha> s \<in> wa_invar WAA;
               (s,s')\<in>wa_step WAC
             \<rbrakk> \<Longrightarrow> s'\<in>addi"

  \<comment> \<open>The initial states satisfy the concrete part of the invariant\<close>
  assumes initial_addi: "wa_initial WAC \<subseteq> addi"

  shows
    "while_algo WAC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. while_algo WAC
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. while_algo WAC
[PROOF STEP]
interpret waa: while_algo WAA
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. while_algo WAA
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. while_algo WAC
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. while_algo WAC
[PROOF STEP]
apply (unfold_locales)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>s \<in> wa_invar WAC; s \<in> wa_cond WAC; (s, s') \<in> wa_step WAC\<rbrakk> \<Longrightarrow> s' \<in> wa_invar WAC
 2. wa_initial WAC \<subseteq> wa_invar WAC
 3. wf {(s', s). s \<in> wa_invar WAC \<and> s \<in> wa_cond WAC \<and> (s, s') \<in> wa_step WAC}
[PROOF STEP]
apply (subst icf)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>s \<in> wa_invar WAC; s \<in> wa_cond WAC; (s, s') \<in> wa_step WAC\<rbrakk> \<Longrightarrow> s' \<in> addi \<inter> {s. \<alpha> s \<in> wa_invar WAA}
 2. wa_initial WAC \<subseteq> wa_invar WAC
 3. wf {(s', s). s \<in> wa_invar WAC \<and> s \<in> wa_cond WAC \<and> (s, s') \<in> wa_step WAC}
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>s \<in> wa_invar WAC; s \<in> wa_cond WAC; (s, s') \<in> wa_step WAC\<rbrakk> \<Longrightarrow> s' \<in> addi
 2. \<And>s s'. \<lbrakk>s \<in> wa_invar WAC; s \<in> wa_cond WAC; (s, s') \<in> wa_step WAC\<rbrakk> \<Longrightarrow> \<alpha> s' \<in> wa_invar WAA
 3. \<And>x. x \<in> wa_initial WAC \<Longrightarrow> x \<in> wa_invar WAC
 4. wf {(s', s). s \<in> wa_invar WAC \<and> s \<in> wa_cond WAC \<and> (s, s') \<in> wa_step WAC}
[PROOF STEP]
apply (simp only: icf)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>s \<in> addi \<inter> {s. \<alpha> s \<in> wa_invar WAA}; s \<in> wa_cond WAC; (s, s') \<in> wa_step WAC\<rbrakk> \<Longrightarrow> s' \<in> addi
 2. \<And>s s'. \<lbrakk>s \<in> wa_invar WAC; s \<in> wa_cond WAC; (s, s') \<in> wa_step WAC\<rbrakk> \<Longrightarrow> \<alpha> s' \<in> wa_invar WAA
 3. \<And>x. x \<in> wa_initial WAC \<Longrightarrow> x \<in> wa_invar WAC
 4. wf {(s', s). s \<in> wa_invar WAC \<and> s \<in> wa_cond WAC \<and> (s, s') \<in> wa_step WAC}
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>s \<in> wa_cond WAC; (s, s') \<in> wa_step WAC; s \<in> addi; \<alpha> s \<in> wa_invar WAA\<rbrakk> \<Longrightarrow> s' \<in> addi
 2. \<And>s s'. \<lbrakk>s \<in> wa_invar WAC; s \<in> wa_cond WAC; (s, s') \<in> wa_step WAC\<rbrakk> \<Longrightarrow> \<alpha> s' \<in> wa_invar WAA
 3. \<And>x. x \<in> wa_initial WAC \<Longrightarrow> x \<in> wa_invar WAC
 4. wf {(s', s). s \<in> wa_invar WAC \<and> s \<in> wa_cond WAC \<and> (s, s') \<in> wa_step WAC}
[PROOF STEP]
apply (blast intro!: step_addi)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>s \<in> wa_invar WAC; s \<in> wa_cond WAC; (s, s') \<in> wa_step WAC\<rbrakk> \<Longrightarrow> \<alpha> s' \<in> wa_invar WAA
 2. \<And>x. x \<in> wa_initial WAC \<Longrightarrow> x \<in> wa_invar WAC
 3. wf {(s', s). s \<in> wa_invar WAC \<and> s \<in> wa_cond WAC \<and> (s, s') \<in> wa_step WAC}
[PROOF STEP]
apply (frule (2) step_abs)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>s \<in> wa_invar WAC; s \<in> wa_cond WAC; (s, s') \<in> wa_step WAC; (\<alpha> s, \<alpha> s') \<in> wa_step WAA\<rbrakk> \<Longrightarrow> \<alpha> s' \<in> wa_invar WAA
 2. \<And>x. x \<in> wa_initial WAC \<Longrightarrow> x \<in> wa_invar WAC
 3. wf {(s', s). s \<in> wa_invar WAC \<and> s \<in> wa_cond WAC \<and> (s, s') \<in> wa_step WAC}
[PROOF STEP]
apply (frule (1) cond_abs)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>s \<in> wa_invar WAC; s \<in> wa_cond WAC; (s, s') \<in> wa_step WAC; (\<alpha> s, \<alpha> s') \<in> wa_step WAA; \<alpha> s \<in> wa_cond WAA\<rbrakk> \<Longrightarrow> \<alpha> s' \<in> wa_invar WAA
 2. \<And>x. x \<in> wa_initial WAC \<Longrightarrow> x \<in> wa_invar WAC
 3. wf {(s', s). s \<in> wa_invar WAC \<and> s \<in> wa_cond WAC \<and> (s, s') \<in> wa_step WAC}
[PROOF STEP]
apply (simp only: icf)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>s \<in> addi \<inter> {s. \<alpha> s \<in> wa_invar WAA}; s \<in> wa_cond WAC; (s, s') \<in> wa_step WAC; (\<alpha> s, \<alpha> s') \<in> wa_step WAA; \<alpha> s \<in> wa_cond WAA\<rbrakk> \<Longrightarrow> \<alpha> s' \<in> wa_invar WAA
 2. \<And>x. x \<in> wa_initial WAC \<Longrightarrow> x \<in> wa_invar WAC
 3. wf {(s', s). s \<in> wa_invar WAC \<and> s \<in> wa_cond WAC \<and> (s, s') \<in> wa_step WAC}
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>s \<in> wa_cond WAC; (s, s') \<in> wa_step WAC; (\<alpha> s, \<alpha> s') \<in> wa_step WAA; \<alpha> s \<in> wa_cond WAA; s \<in> addi; \<alpha> s \<in> wa_invar WAA\<rbrakk> \<Longrightarrow> \<alpha> s' \<in> wa_invar WAA
 2. \<And>x. x \<in> wa_initial WAC \<Longrightarrow> x \<in> wa_invar WAC
 3. wf {(s', s). s \<in> wa_invar WAC \<and> s \<in> wa_cond WAC \<and> (s, s') \<in> wa_step WAC}
[PROOF STEP]
apply (erule (2) waa.step_invar)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> wa_initial WAC \<Longrightarrow> x \<in> wa_invar WAC
 2. wf {(s', s). s \<in> wa_invar WAC \<and> s \<in> wa_cond WAC \<and> (s, s') \<in> wa_step WAC}
[PROOF STEP]
apply (simp add: icf)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> wa_initial WAC \<Longrightarrow> x \<in> addi \<and> \<alpha> x \<in> wa_invar WAA
 2. wf {(s', s). s \<in> wa_invar WAC \<and> s \<in> wa_cond WAC \<and> (s, s') \<in> wa_step WAC}
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> wa_initial WAC \<Longrightarrow> x \<in> addi
 2. \<And>x. x \<in> wa_initial WAC \<Longrightarrow> \<alpha> x \<in> wa_invar WAA
 3. wf {(s', s). s \<in> wa_invar WAC \<and> s \<in> wa_cond WAC \<and> (s, s') \<in> wa_step WAC}
[PROOF STEP]
apply (erule rev_subsetD[OF _ initial_addi])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> wa_initial WAC \<Longrightarrow> \<alpha> x \<in> wa_invar WAA
 2. wf {(s', s). s \<in> wa_invar WAC \<and> s \<in> wa_cond WAC \<and> (s, s') \<in> wa_step WAC}
[PROOF STEP]
apply (insert initial_abs waa.initial_invar) [1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> wa_initial WAC; \<alpha> ` wa_initial WAC \<subseteq> wa_initial WAA; wa_initial WAA \<subseteq> wa_invar WAA\<rbrakk> \<Longrightarrow> \<alpha> x \<in> wa_invar WAA
 2. wf {(s', s). s \<in> wa_invar WAC \<and> s \<in> wa_cond WAC \<and> (s, s') \<in> wa_step WAC}
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(s', s). s \<in> wa_invar WAC \<and> s \<in> wa_cond WAC \<and> (s, s') \<in> wa_step WAC}
[PROOF STEP]
apply (rule_tac
      r="inv_image { (s',s). s\<in>wa_invar WAA
                    \<and> s\<in>wa_cond WAA
                    \<and> (s,s')\<in>wa_step WAA } \<alpha>"
      in wf_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wf (inv_image {(s', s). s \<in> wa_invar WAA \<and> s \<in> wa_cond WAA \<and> (s, s') \<in> wa_step WAA} \<alpha>)
 2. {(s', s). s \<in> wa_invar WAC \<and> s \<in> wa_cond WAC \<and> (s, s') \<in> wa_step WAC} \<subseteq> inv_image {(s', s). s \<in> wa_invar WAA \<and> s \<in> wa_cond WAA \<and> (s, s') \<in> wa_step WAA} \<alpha>
[PROOF STEP]
apply (simp add: waa.step_wf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(s', s). s \<in> wa_invar WAC \<and> s \<in> wa_cond WAC \<and> (s, s') \<in> wa_step WAC} \<subseteq> inv_image {(s', s). s \<in> wa_invar WAA \<and> s \<in> wa_cond WAA \<and> (s, s') \<in> wa_step WAA} \<alpha>
[PROOF STEP]
apply (auto simp add: cond_abs step_abs icf) [1]
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
while_algo WAC

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma transfer_correctness:
    assumes A: "\<forall>s. s\<in>wa_invar WAA \<and> s\<notin>wa_cond WAA \<longrightarrow> P s"
    shows "\<forall>sc. sc\<in>wa_invar WAC \<and> sc\<notin>wa_cond WAC \<longrightarrow> P (\<alpha> sc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>sc. sc \<in> wa_invar WAC \<and> sc \<notin> wa_cond WAC \<longrightarrow> P (\<alpha> sc)
[PROOF STEP]
using A cond_abs invar_abs cond_precise
[PROOF STATE]
proof (prove)
using this:
\<forall>s. s \<in> wa_invar WAA \<and> s \<notin> wa_cond WAA \<longrightarrow> P s
\<lbrakk>?s \<in> wa_invar WAC; ?s \<in> wa_cond WAC\<rbrakk> \<Longrightarrow> \<alpha> ?s \<in> wa_cond WAA
\<alpha> ` wa_invar WAC \<subseteq> wa_invar WAA
\<forall>s. s \<in> wa_invar WAC \<and> \<alpha> s \<in> wa_cond WAA \<longrightarrow> s \<in> wa_cond WAC

goal (1 subgoal):
 1. \<forall>sc. sc \<in> wa_invar WAC \<and> sc \<notin> wa_cond WAC \<longrightarrow> P (\<alpha> sc)
[PROOF STEP]
by blast


[STATEMENT]
lemma wa_ref_refl: "wa_refine WA WA id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wa_refine WA WA id
[PROOF STEP]
by (unfold_locales) auto


[STATEMENT]
lemma wa_pref_refl: "wa_precise_refine WA WA id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wa_precise_refine WA WA id
[PROOF STEP]
by (unfold_locales) auto


[STATEMENT]
lemma wa_ref_trans:
  assumes "wa_refine WC WB \<alpha>1"
  assumes "wa_refine WB WA \<alpha>2"
  shows "wa_refine WC WA (\<alpha>2\<circ>\<alpha>1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wa_refine WC WA (\<alpha>2 \<circ> \<alpha>1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wa_refine WC WA (\<alpha>2 \<circ> \<alpha>1)
[PROOF STEP]
interpret r1: wa_refine WC WB \<alpha>1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wa_refine WC WB \<alpha>1
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wa_refine WC WA (\<alpha>2 \<circ> \<alpha>1)
[PROOF STEP]
interpret r2: wa_refine WB WA \<alpha>2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wa_refine WB WA \<alpha>2
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wa_refine WC WA (\<alpha>2 \<circ> \<alpha>1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wa_refine WC WA (\<alpha>2 \<circ> \<alpha>1)
[PROOF STEP]
(* Cool, everything by auto! *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wa_refine WC WA (\<alpha>2 \<circ> \<alpha>1)
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>s \<in> wa_invar WC; s \<in> wa_cond WC\<rbrakk> \<Longrightarrow> (\<alpha>2 \<circ> \<alpha>1) s \<in> wa_cond WA
 2. \<And>s s'. \<lbrakk>s \<in> wa_invar WC; s \<in> wa_cond WC; (s, s') \<in> wa_step WC\<rbrakk> \<Longrightarrow> ((\<alpha>2 \<circ> \<alpha>1) s, (\<alpha>2 \<circ> \<alpha>1) s') \<in> wa_step WA
 3. (\<alpha>2 \<circ> \<alpha>1) ` wa_initial WC \<subseteq> wa_initial WA
 4. (\<alpha>2 \<circ> \<alpha>1) ` wa_invar WC \<subseteq> wa_invar WA
[PROOF STEP]
apply (auto simp add:
      r1.invar_abs' r2.invar_abs'
      r1.cond_abs r2.cond_abs
      r1.step_abs r2.step_abs
      r1.initial_abs' r2.initial_abs')
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
wa_refine WC WA (\<alpha>2 \<circ> \<alpha>1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wa_pref_trans:
  assumes "wa_precise_refine WC WB \<alpha>1"
  assumes "wa_precise_refine WB WA \<alpha>2"
  shows "wa_precise_refine WC WA (\<alpha>2\<circ>\<alpha>1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wa_precise_refine WC WA (\<alpha>2 \<circ> \<alpha>1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wa_precise_refine WC WA (\<alpha>2 \<circ> \<alpha>1)
[PROOF STEP]
interpret r1: wa_precise_refine WC WB \<alpha>1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wa_precise_refine WC WB \<alpha>1
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wa_precise_refine WC WA (\<alpha>2 \<circ> \<alpha>1)
[PROOF STEP]
interpret r2: wa_precise_refine WB WA \<alpha>2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wa_precise_refine WB WA \<alpha>2
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wa_precise_refine WC WA (\<alpha>2 \<circ> \<alpha>1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wa_precise_refine WC WA (\<alpha>2 \<circ> \<alpha>1)
[PROOF STEP]
apply intro_locales
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wa_refine WC WA (\<alpha>2 \<circ> \<alpha>1)
 2. wa_precise_refine_axioms WC WA (\<alpha>2 \<circ> \<alpha>1)
[PROOF STEP]
apply (rule wa_ref_trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. wa_refine WC ?WB1 \<alpha>1
 2. wa_refine ?WB1 WA \<alpha>2
 3. wa_precise_refine_axioms WC WA (\<alpha>2 \<circ> \<alpha>1)
[PROOF STEP]
apply (unfold_locales)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s. s \<in> wa_invar WC \<and> (\<alpha>2 \<circ> \<alpha>1) s \<in> wa_cond WA \<longrightarrow> s \<in> wa_cond WC
[PROOF STEP]
apply (auto simp add: r1.invar_abs' r2.invar_abs'
                          r1.cond_precise r2.cond_precise)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
wa_precise_refine WC WA (\<alpha>2 \<circ> \<alpha>1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_while_algo: "while_algo (det_wa_wa WA)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. while_algo (det_wa_wa WA)
[PROOF STEP]
apply (unfold_locales)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>s \<in> wa_invar (det_wa_wa WA); s \<in> wa_cond (det_wa_wa WA); (s, s') \<in> wa_step (det_wa_wa WA)\<rbrakk> \<Longrightarrow> s' \<in> wa_invar (det_wa_wa WA)
 2. wa_initial (det_wa_wa WA) \<subseteq> wa_invar (det_wa_wa WA)
 3. wf {(s', s). s \<in> wa_invar (det_wa_wa WA) \<and> s \<in> wa_cond (det_wa_wa WA) \<and> (s, s') \<in> wa_step (det_wa_wa WA)}
[PROOF STEP]
apply (auto simp add: det_wa_wa_def step_invar initial_invar)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(s', s). s \<in> dwa_invar WA \<and> dwa_cond WA s \<and> s' = dwa_step WA s}
[PROOF STEP]
apply (insert step_wf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(dwa_step WA s, s) |s. s \<in> dwa_invar WA \<and> dwa_cond WA s} \<Longrightarrow> wf {(s', s). s \<in> dwa_invar WA \<and> dwa_cond WA s \<and> s' = dwa_step WA s}
[PROOF STEP]
apply (erule_tac P=wf in back_subst)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(dwa_step WA s, s) |s. s \<in> dwa_invar WA \<and> dwa_cond WA s} = {(s', s). s \<in> dwa_invar WA \<and> dwa_cond WA s \<and> s' = dwa_step WA s}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma det_while_algo_intro:
  assumes "while_algo (det_wa_wa DWA)"
  shows "det_while_algo DWA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det_while_algo DWA
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. det_while_algo DWA
[PROOF STEP]
interpret while_algo "(det_wa_wa DWA)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. while_algo (det_wa_wa DWA)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. det_while_algo DWA
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det_while_algo DWA
[PROOF STEP]
using step_invar initial_invar step_wf
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?s \<in> wa_invar (det_wa_wa DWA); ?s \<in> wa_cond (det_wa_wa DWA); (?s, ?s') \<in> wa_step (det_wa_wa DWA)\<rbrakk> \<Longrightarrow> ?s' \<in> wa_invar (det_wa_wa DWA)
wa_initial (det_wa_wa DWA) \<subseteq> wa_invar (det_wa_wa DWA)
wf {(s', s). s \<in> wa_invar (det_wa_wa DWA) \<and> s \<in> wa_cond (det_wa_wa DWA) \<and> (s, s') \<in> wa_step (det_wa_wa DWA)}

goal (1 subgoal):
 1. det_while_algo DWA
[PROOF STEP]
apply (unfold_locales)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<And>s s'. \<lbrakk>s \<in> wa_invar (det_wa_wa DWA); s \<in> wa_cond (det_wa_wa DWA); (s, s') \<in> wa_step (det_wa_wa DWA)\<rbrakk> \<Longrightarrow> s' \<in> wa_invar (det_wa_wa DWA); wa_initial (det_wa_wa DWA) \<subseteq> wa_invar (det_wa_wa DWA); wf {(s', s). s \<in> wa_invar (det_wa_wa DWA) \<and> s \<in> wa_cond (det_wa_wa DWA) \<and> (s, s') \<in> wa_step (det_wa_wa DWA)}; s \<in> dwa_invar DWA; dwa_cond DWA s\<rbrakk> \<Longrightarrow> dwa_step DWA s \<in> dwa_invar DWA
 2. \<lbrakk>\<And>s s'. \<lbrakk>s \<in> wa_invar (det_wa_wa DWA); s \<in> wa_cond (det_wa_wa DWA); (s, s') \<in> wa_step (det_wa_wa DWA)\<rbrakk> \<Longrightarrow> s' \<in> wa_invar (det_wa_wa DWA); wa_initial (det_wa_wa DWA) \<subseteq> wa_invar (det_wa_wa DWA); wf {(s', s). s \<in> wa_invar (det_wa_wa DWA) \<and> s \<in> wa_cond (det_wa_wa DWA) \<and> (s, s') \<in> wa_step (det_wa_wa DWA)}\<rbrakk> \<Longrightarrow> dwa_initial DWA \<in> dwa_invar DWA
 3. \<lbrakk>\<And>s s'. \<lbrakk>s \<in> wa_invar (det_wa_wa DWA); s \<in> wa_cond (det_wa_wa DWA); (s, s') \<in> wa_step (det_wa_wa DWA)\<rbrakk> \<Longrightarrow> s' \<in> wa_invar (det_wa_wa DWA); wa_initial (det_wa_wa DWA) \<subseteq> wa_invar (det_wa_wa DWA); wf {(s', s). s \<in> wa_invar (det_wa_wa DWA) \<and> s \<in> wa_cond (det_wa_wa DWA) \<and> (s, s') \<in> wa_step (det_wa_wa DWA)}\<rbrakk> \<Longrightarrow> wf {(dwa_step DWA s, s) |s. s \<in> dwa_invar DWA \<and> dwa_cond DWA s}
[PROOF STEP]
apply (unfold det_wa_wa_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<And>s s'. \<lbrakk>s \<in> wa_invar \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr>; s \<in> wa_cond \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr>; (s, s') \<in> wa_step \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr>\<rbrakk> \<Longrightarrow> s' \<in> wa_invar \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr>; wa_initial \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr> \<subseteq> wa_invar \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr>; wf {(s', s). s \<in> wa_invar \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr> \<and> s \<in> wa_cond \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr> \<and> (s, s') \<in> wa_step \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr>}; s \<in> dwa_invar DWA; dwa_cond DWA s\<rbrakk> \<Longrightarrow> dwa_step DWA s \<in> dwa_invar DWA
 2. \<lbrakk>\<And>s s'. \<lbrakk>s \<in> wa_invar \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr>; s \<in> wa_cond \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr>; (s, s') \<in> wa_step \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr>\<rbrakk> \<Longrightarrow> s' \<in> wa_invar \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr>; wa_initial \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr> \<subseteq> wa_invar \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr>; wf {(s', s). s \<in> wa_invar \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr> \<and> s \<in> wa_cond \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr> \<and> (s, s') \<in> wa_step \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr>}\<rbrakk> \<Longrightarrow> dwa_initial DWA \<in> dwa_invar DWA
 3. \<lbrakk>\<And>s s'. \<lbrakk>s \<in> wa_invar \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr>; s \<in> wa_cond \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr>; (s, s') \<in> wa_step \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr>\<rbrakk> \<Longrightarrow> s' \<in> wa_invar \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr>; wa_initial \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr> \<subseteq> wa_invar \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr>; wf {(s', s). s \<in> wa_invar \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr> \<and> s \<in> wa_cond \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr> \<and> (s, s') \<in> wa_step \<lparr>wa_cond = {s. dwa_cond DWA s}, wa_step = {(s, dwa_step DWA s) |s. True}, wa_initial = {dwa_initial DWA}, wa_invar = dwa_invar DWA\<rparr>}\<rbrakk> \<Longrightarrow> wf {(dwa_step DWA s, s) |s. s \<in> dwa_invar DWA \<and> dwa_cond DWA s}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s s'. \<lbrakk>s \<in> dwa_invar DWA; dwa_cond DWA s; s' = dwa_step DWA s\<rbrakk> \<Longrightarrow> dwa_step DWA s \<in> dwa_invar DWA; dwa_initial DWA \<in> dwa_invar DWA; wf {(s', s). s \<in> dwa_invar DWA \<and> dwa_cond DWA s \<and> s' = dwa_step DWA s}\<rbrakk> \<Longrightarrow> wf {(dwa_step DWA s, s) |s. s \<in> dwa_invar DWA \<and> dwa_cond DWA s}
[PROOF STEP]
apply (erule_tac P=wf in back_subst)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s s'. \<lbrakk>s \<in> dwa_invar DWA; dwa_cond DWA s; s' = dwa_step DWA s\<rbrakk> \<Longrightarrow> dwa_step DWA s \<in> dwa_invar DWA; dwa_initial DWA \<in> dwa_invar DWA\<rbrakk> \<Longrightarrow> {(s', s). s \<in> dwa_invar DWA \<and> dwa_cond DWA s \<and> s' = dwa_step DWA s} = {(dwa_step DWA s, s) |s. s \<in> dwa_invar DWA \<and> dwa_cond DWA s}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
det_while_algo DWA

goal:
No subgoals!
[PROOF STEP]
qed

\<comment> \<open>A deterministic while-algorithm is well-defined, if and only if the
    corresponding non-deterministic while-algorithm is well-defined\<close>


[STATEMENT]
theorem dwa_is_wa:
  "while_algo (det_wa_wa DWA) \<longleftrightarrow> det_while_algo DWA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. while_algo (det_wa_wa DWA) = det_while_algo DWA
[PROOF STEP]
using det_while_algo_intro det_while_algo.is_while_algo
[PROOF STATE]
proof (prove)
using this:
while_algo (det_wa_wa ?DWA) \<Longrightarrow> det_while_algo ?DWA
det_while_algo ?WA \<Longrightarrow> while_algo (det_wa_wa ?WA)

goal (1 subgoal):
 1. while_algo (det_wa_wa DWA) = det_while_algo DWA
[PROOF STEP]
by auto