Theory Variants

(*<*)
theory Variants
imports Abbrevs 
begin


lemma restrict_map_inverse: "m |` (dom m - X) = m |`(-X)"
  apply (rule ext)
  apply (auto simp add: restrict_map_def)
  done

lemma conj_assoc: "((P ∧ Q) ∧ X) = (P ∧ Q ∧ X)"
  by simp

(* Constructor markup for some datatypes *)
(* instr *)
notation (latex output)
Read (‹\<^latex>‹\constructor{Read}››)
notation (latex output)
Write (‹\<^latex>‹\constructor{Write}››)
notation (latex output)
RMW (‹\<^latex>‹\constructor{RMW}››)
notation (latex output)
Fence (‹\<^latex>‹\constructor{Fence}››)
notation (latex output)
Ghost (‹\<^latex>‹\constructor{Ghost}››)

(* memref *)
notation (latex output)
Write⇩s⇩b (‹\<^latex>‹\constructor{Write}›⇩s⇩b›)
notation (latex output)
Read⇩s⇩b (‹\<^latex>‹\constructor{Read}›⇩s⇩b›)
notation (latex output)
Prog⇩s⇩b (‹\<^latex>‹\constructor{Prog}›⇩s⇩b›)
notation (latex output)
Ghost⇩s⇩b (‹\<^latex>‹\constructor{Ghost}›⇩s⇩b›)



(* expr *)
notation (latex output)
Const (‹\<^latex>‹\constructor{Const}››)
notation (latex output)
Mem (‹\<^latex>‹\constructor{Mem}››)
notation (latex output)
Tmp (‹\<^latex>‹\constructor{Tmp}››)
notation (latex output)
Unop (‹\<^latex>‹\constructor{Unop}››)
notation (latex output)
Binop (‹\<^latex>‹\constructor{Binop}››)

(* stmt *)
notation (latex output)
Skip (‹\<^latex>‹\constructor{Skip}››)
notation (latex output)
Assign (‹\<^latex>‹\constructor{Assign}››)
notation (latex output)
CAS (‹\<^latex>‹\constructor{CAS}››)
notation (latex output)
Seq (‹\<^latex>‹\constructor{Seq}››)
notation (latex output)
Cond (‹\<^latex>‹\constructor{Cond}››)
notation (latex output)
While (‹\<^latex>‹\constructor{While}››)
notation (latex output)
SGhost (‹\<^latex>‹\constructor{SGhost}››)
notation (latex output)
SFence (‹\<^latex>‹\constructor{SFence}››)

lemma sim_direct_config_def': "ts⇩s⇩b ∼⇩d ts ≡
(ts⇩s⇩b = (map (λ(p,is, θ,sb::unit,𝒟, 𝒪,ℛ). (p,is,θ,[],(),(),())) ts))"
apply (rule HOL.eq_reflection)
apply rule
apply  (erule sim_direct_config.cases)
apply  (clarsimp)
apply  (rule nth_equalityI)
apply   simp
apply  clarsimp
apply  (case_tac "ts!i")
apply  fastforce
apply (rule sim_direct_config.intros)
apply auto
done

ML ‹@{term "(λ(p,is, θ,sb::unit,𝒟, 𝒪,ℛ). (p,is,θ,[],(),(),()))"}›

lemma DRead: "(Read volatile a t # is,θ, x, m,ghst) →
               (is, θ (t↦m a), x, m, ghst)"
apply (cases ghst) 
apply (simp add: direct_memop_step.Read)
done

lemma DWriteNonVolatile:"
  (Write False a (D,f) A L R W#is, θ, x, m, ghst) → (is, θ, x, m(a := f θ), ghst)"
apply (cases ghst) 
apply (simp add: direct_memop_step.WriteNonVolatile)
done

lemma DWriteVolatile:
  "ghst = (𝒟, 𝒪, ℛ, 𝒮) ⟹ ghst' = (True, 𝒪 ∪ A - R, Map.empty, 𝒮 ⊕⇘W⇙ R ⊖⇘A⇙ L) 
   ⟹ (Write True a (D,f) A L R W# is, θ, x, m, ghst) → (is, θ,  x, m(a:=f θ), ghst')"
by (simp add: direct_memop_step.WriteVolatile)

lemma DGhost:
  "ghst = (𝒟, 𝒪, ℛ, 𝒮) ⟹ ghst' = (𝒟, 𝒪 ∪ A - R, augment_rels (dom 𝒮) R ℛ, 𝒮 ⊕⇘W⇙ R ⊖⇘A⇙ L) 
   ⟹ (Ghost A L R W# is, θ, x, m, ghst) → (is, θ,  x, m, ghst')"
by (simp add: direct_memop_step.Ghost)

lemma DRMWReadOnly:
  "⟦¬ cond (θ(t↦m a)); ghst = (𝒟, 𝒪, ℛ, 𝒮); ghst'=(False, 𝒪, Map.empty,𝒮)⟧ ⟹ 
   (RMW a t (D,f) cond ret A L R W # is, θ, x, m, ghst) → (is, θ(t↦m a),x,m, ghst')"
apply (simp add: direct_memop_step.RMWReadOnly)
done

lemma DRMWWrite:
  "⟦cond (θ(t↦m a)); 
    θ' = θ(t↦ret (m a) (f(θ(t↦m a))));
    m' = m(a:= f(θ(t↦m a)));
    ghst = (𝒟, 𝒪, ℛ, 𝒮); 
   ghst' = (False,𝒪 ∪ A - R, Map.empty, 𝒮 ⊕⇘W⇙ R ⊖⇘A⇙ L)⟧ 
   ⟹ 
   (RMW a t (D,f) cond ret A L R W# is, θ, x, m, ghst) → (is, θ',x, m' , ghst')"
apply (simp add: direct_memop_step.RMWWrite)
done

lemma VRead: "(Read volatile a t # is,θ, x, m,ghst) →⇩v
               (is, θ (t↦m a), x, m, ghst)"
apply (cases ghst) 
apply (simp add: virtual_memop_step.Read)
done

lemma VWriteNonVolatile:"
  (Write False a (D,f) A L R W#is, θ, x, m, ghst) →⇩v (is, θ, x, m(a := f θ), ghst)"
apply (cases ghst) 
apply (simp add: virtual_memop_step.WriteNonVolatile)
done

lemma VWriteVolatile:
  "ghst = (𝒟, 𝒪, ℛ, 𝒮) ⟹ ghst' = (True, 𝒪 ∪ A - R, ℛ, 𝒮 ⊕⇘W⇙ R ⊖⇘A⇙ L) 
   ⟹ (Write True a (D,f) A L R W# is, θ, x, m, ghst) →⇩v (is, θ,  x, m(a:=f θ), ghst')"
by (simp add: virtual_memop_step.WriteVolatile)

lemma VRMWReadOnly:
  "⟦¬ cond (θ(t↦m a)); ghst = (𝒟, 𝒪, ℛ, 𝒮); ghst'=(False, 𝒪,ℛ,𝒮)⟧ ⟹ 
   (RMW a t (D,f) cond ret A L R W # is, θ, x, m, ghst) →⇩v (is, θ(t↦m a),x,m, ghst')"
apply (simp add: virtual_memop_step.RMWReadOnly)
done

lemma VFence:
  "ghst = (𝒟, 𝒪, ℛ, 𝒮) ⟹ ghst' = (False, 𝒪, ℛ, 𝒮) 
   ⟹ (Fence# is, θ, x, m, ghst) →⇩v (is, θ,  x, m, ghst')"
by (simp add: virtual_memop_step.Fence)

lemma VGhost:
  "ghst = (𝒟, 𝒪, ℛ, 𝒮) ⟹ ghst' = (𝒟, 𝒪 ∪ A - R, ℛ, 𝒮 ⊕⇘W⇙ R ⊖⇘A⇙ L)  
   ⟹ (Ghost A L R W# is, θ, x, m, ghst) →⇩v (is, θ,  x, m, ghst')"
by (simp add: virtual_memop_step.Ghost)

lemma VRMWWrite:
  "⟦cond (θ(t↦m a)); 
    θ' = θ(t↦ret (m a) (f(θ(t↦m a))));
    m' = m(a:= f(θ(t↦m a)));
    ghst = (𝒟, 𝒪, ℛ, 𝒮); 
   ghst' = (False,𝒪 ∪ A - R, ℛ, 𝒮 ⊕⇘W⇙ R ⊖⇘A⇙ L)⟧ 
   ⟹ 
   (RMW a t (D,f) cond ret A L R W# is, θ, x, m, ghst) →⇩v (is, θ',x, m' , ghst')"
apply (simp add: virtual_memop_step.RMWWrite)
done


lemma SafeWriteVolatile:
  "⟦∀j < length 𝒪s. i≠j ⟶ a ∉ 𝒪s!j; a ∉ read_only 𝒮;    
    ∀j < length 𝒪s. i≠j ⟶  A ∩  𝒪s!j = {};
    A ⊆ 𝒪 ∪ dom 𝒮; L ⊆ A; R ⊆ 𝒪; A ∩ R = {}
   ⟧
   ⟹ 
   𝒪s,i⊢(Write True a (D,f) A L R W# is, θ, m, 𝒟, 𝒪, 𝒮)√"
apply (rule safe_direct_memop_state.WriteVolatile)
apply auto
done

lemma SafeDelayedWriteVolatile:
  "⟦∀j < length 𝒪s. i≠j ⟶ a ∉ (𝒪s!j ∪ dom (ℛs!j)); a ∉ read_only 𝒮;
  ∀j < length 𝒪s. i≠j ⟶  A ∩  (𝒪s!j ∪ dom (ℛs!j)) = {};
    A ⊆ dom 𝒮 ∪ 𝒪; L ⊆ A; R ⊆ 𝒪; A ∩ R = {}
   ⟧
   ⟹ 
   𝒪s,ℛs,i⊢(Write True a (D,f) A L R W# is, θ, m, 𝒟, 𝒪, 𝒮)√"
apply (rule safe_delayed_direct_memop_state.WriteVolatile)
apply auto
done


lemma SafeRMWReadOnly:
  "⟦¬ cond (θ(t↦m a)); a ∈ dom 𝒮 ∪ 𝒪⟧ ⟹ 
   𝒪s,i⊢ (RMW a t (D,f) cond ret A L R W# is, θ, m, 𝒟, 𝒪, 𝒮)√"
apply (rule safe_direct_memop_state.RMWReadOnly)
apply auto
done

lemma SafeDelayedRMWReadOnly:
  "⟦¬ cond (θ(t↦m a)); a ∈ dom 𝒮 ∪ 𝒪; 
   ∀j < length 𝒪s. i≠j ⟶ (ℛs!j) a ≠ Some False ― ‹no release of unshared address›⟧
   ⟹ 
   𝒪s,ℛs,i⊢(RMW a t (D,f) cond ret A L R W# is, θ, m, 𝒟, 𝒪, 𝒮)√"
apply (rule safe_delayed_direct_memop_state.RMWReadOnly)
apply auto
done

lemma SafeRMWWrite:
  "⟦cond (θ(t↦m a));  
    ∀j < length 𝒪s. i≠j ⟶ a ∉ 𝒪s!j; a ∉ read_only 𝒮;
    ∀j < length 𝒪s. i≠j ⟶ A ∩ 𝒪s!j  = {};    
    A ⊆  𝒪 ∪ dom 𝒮; L ⊆ A; R ⊆ 𝒪; A ∩ R = {}
    ⟧ 
   ⟹ 
   𝒪s,i⊢ (RMW a t (D,f) cond ret A L R W# is, θ, m, 𝒟, 𝒪, 𝒮)√"
apply (rule safe_direct_memop_state.RMWWrite)
apply auto
done

lemma SafeDelayedRMWWrite:
  "⟦cond (θ(t↦m a)); a ∈ dom 𝒮 ∪ 𝒪;  
    ∀j < length 𝒪s. i≠j ⟶ a ∉ (𝒪s!j ∪ dom (ℛs!j));a ∉ read_only 𝒮;
    ∀j < length 𝒪s. i≠j ⟶ A ∩ (𝒪s!j ∪ dom (ℛs!j))  = {};
    A ⊆ dom 𝒮 ∪ 𝒪; L ⊆ A; R ⊆ 𝒪; A ∩ R = {}
    ⟧ 
   ⟹ 
   𝒪s,ℛs,i⊢(RMW a t (D,f) cond ret A L R W# is, θ, m, 𝒟, 𝒪, 𝒮)√"
apply (rule safe_delayed_direct_memop_state.RMWWrite)
apply auto
done

lemma  Write⇩s⇩bNonVolatile: 
  "(m, Write⇩s⇩b False a sop v A L R W# rs,𝒪,ℛ,𝒮) →⇩f (m(a := v), rs,𝒪,ℛ,𝒮)"
  apply (rule flush_step.Write⇩s⇩b)
  apply auto
  done

lemma Write⇩s⇩bVolatile: 
"⟦𝒪'= 𝒪 ∪ A - R;  𝒮'=(𝒮 ⊕⇘W⇙ R ⊖⇘A⇙ L)⟧ ⟹
  (m, Write⇩s⇩b True a sop v A L R W# rs,𝒪,ℛ,𝒮) →⇩f (m(a := v), rs,𝒪',Map.empty,𝒮')"
  apply (rule flush_step.Write⇩s⇩b)
  apply auto
  done

lemma Ghost⇩s⇩b: "⟦𝒪'= 𝒪 ∪ A - R; ℛ'= augment_rels (dom 𝒮) R ℛ; 𝒮'=𝒮 ⊕⇘W⇙ R ⊖⇘A⇙ L⟧ ⟹ 
             (m, Ghost⇩s⇩b A L R W# rs,𝒪,ℛ,𝒮) →⇩f (m, rs,𝒪',ℛ',𝒮')"
by (simp add: flush_step.Ghost)

lemma  SBHRead: 
  "⟦v = (case (buffered_val sb a) of Some v' ⇒ v' | None ⇒ m a);
   sb' = sb@[Read⇩s⇩b volatile a t v] ⟧
   ⟹
   (Read volatile a t # is, θ, sb, m,ghst) →⇩s⇩b⇩h
          (is, θ (t↦v), sb', m,ghst)"
  apply (cases ghst)
  apply (cases "buffered_val sb a")
  apply (auto simp add: SBHReadBuffered SBHReadUnbuffered)
  done

lemma  SBRead: 
  "⟦v = (case (buffered_val sb a) of Some v' ⇒ v' | None ⇒ m a)⟧
   ⟹
   (Read volatile a t # is, θ, sb, m,ghst) →⇩s⇩b
          (is, θ (t↦v), sb, m,ghst)"
  apply (cases ghst)
  apply (cases "buffered_val sb a")
  apply (auto simp add: SBReadBuffered SBReadUnbuffered)
  done

lemma  SBHReadBuffered': 
  "⟦buffered_val sb a = Some v;
   sb' = sb@[Read⇩s⇩b volatile a t v] ⟧
   ⟹
   (Read volatile a t # is, θ, sb, m, 𝒟, 𝒪,ℛ, 𝒮) →⇩s⇩b⇩h
          (is, θ (t↦v), sb', m, 𝒟, 𝒪,ℛ, 𝒮)"
  by (simp add: SBHReadBuffered)

lemma SBHReadUnbuffered': 
  "⟦buffered_val sb a = None;
    sb' = sb@[Read⇩s⇩b volatile a t (m a)]⟧ 
   ⟹
   (Read volatile a t # is,θ, sb, m, 𝒟, 𝒪,ℛ, 𝒮) →⇩s⇩b⇩h
          (is,θ (t↦m a), sb', m, 𝒟, 𝒪,ℛ, 𝒮)"
by (simp add: SBHReadUnbuffered)

lemma SBHWriteNonVolatile':
  "⟦ sb'= sb@ [Write⇩s⇩b False a (D,f) (f θ) A L R W]⟧ 
   ⟹
   (Write False a (D,f) A L R W#is,θ, sb, m, ghst) →⇩s⇩b⇩h
          (is, θ, sb', m, ghst)"
by (cases ghst) (simp add: SBHWriteNonVolatile)

lemma SBWriteNonVolatile':
  "⟦ sb'= sb@ [Write⇩s⇩b False a (D,f) (f θ) A L R W]⟧ 
   ⟹
   (Write False a (D,f) A L R W#is,θ, sb, m, ghst) →⇩s⇩b
          (is, θ, sb', m, ghst)"
by (cases ghst) (simp add: SBWriteNonVolatile)

lemma SBHWriteVolatile':
  "⟦sb'= sb@[Write⇩s⇩b True a (D,f) (f θ) A L R W]; ghst = (𝒟, 𝒪, ℛ, 𝒮); ghst' = (True, 𝒪,ℛ, 𝒮)⟧
   ⟹ 
   (Write True a (D,f) A L R W# is,θ, sb, m,ghst) →⇩s⇩b⇩h
         (is,θ, sb', m,ghst')"
by (simp add: SBHWriteVolatile)

lemma SBHGhost':
  "(Ghost A L R W# is, θ, sb, m, G) →⇩s⇩b⇩h
         (is, θ, sb@[Ghost⇩s⇩b A L R W], m, G)"
  by (cases G) (simp add: SBHGhost)


lemma SBWriteVolatile':
  "⟦sb'= sb@[Write⇩s⇩b True a (D,f) (f θ) A L R W]⟧
   ⟹ 
   (Write True a (D,f) A L R W# is,θ, sb, m,ghst) →⇩s⇩b
         (is,θ, sb', m,ghst)"
by (cases ghst) (simp add: SBWriteVolatile)

lemma SBWrite':
  "⟦sb'= sb@[Write⇩s⇩b volatile a (D,f) (f θ) A L R W]⟧
   ⟹ 
   (Write volatile a (D,f) A L R W# is,θ, sb, m,ghst) →⇩s⇩b
         (is,θ, sb', m,ghst)"
apply (cases volatile)
apply (auto intro: SBWriteVolatile' SBWriteNonVolatile')
done


lemma SBHRMWReadOnly':
  "⟦¬ cond (θ(t↦m a)); ghst = (𝒟, 𝒪, ℛ, 𝒮); ghst' = (False, 𝒪, Map.empty,𝒮)⟧ ⟹ 
   (RMW a t (D,f) cond ret A L R W# is, θ, [], m, ghst) →⇩s⇩b⇩h (is, θ(t↦m a),[], m, ghst')"
by (simp add: SBHRMWReadOnly)

lemma SBHRMWWrite':
  "⟦cond (θ(t↦m a)); θ'=θ(t↦ret (m a) (f(θ(t↦m a))));m'=m(a:= f(θ(t↦m a)));
   ghst = (𝒟, 𝒪,ℛ, 𝒮); ghst'=(False, 𝒪 ∪ A - R, Map.empty,𝒮 ⊕⇘W⇙ R ⊖⇘A⇙ L)⟧ ⟹ 
   (RMW a t (D,f) cond ret A L R W# is, θ, [], m, ghst) →⇩s⇩b⇩h
         (is, θ',[], m', ghst')"
  by (simp add: SBHRMWWrite)

lemma SBRMWReadOnly':
  "⟦¬ cond (θ(t↦m a)); θ'=θ(t↦m a)⟧ ⟹ 
   (RMW a t (D,f) cond ret A L R W# is, θ, [], m, ghst) →⇩s⇩b (is, θ',[], m, ghst)"
by (cases ghst) (simp add: SBRMWReadOnly)

lemma SBRMWWrite':
  "⟦cond (θ(t↦m a)); θ'=θ(t↦ret (m a) (f(θ(t↦m a))));m'=m(a:= f(θ(t↦m a)))⟧ 
   ⟹ 
   (RMW a t (D,f) cond ret A L R W# is, θ, [], m, ghst) →⇩s⇩b
         (is, θ',[], m', ghst)"
  by (cases ghst) (simp add: SBRMWWrite)

lemma sim_config':
  "⟦m = flush_all_until_volatile_write ts⇩s⇩b⇩h m⇩s⇩b⇩h;
    𝒮 = share_all_until_volatile_write ts⇩s⇩b⇩h 𝒮⇩s⇩b⇩h;
    length ts⇩s⇩b⇩h = length ts; 
    ∀i < length ts⇩s⇩b⇩h. 
           let (p⇩s⇩b⇩h, is⇩s⇩b⇩h, θ⇩s⇩b⇩h, sb, 𝒟⇩s⇩b⇩h, 𝒪⇩s⇩b⇩h,ℛ⇩s⇩b⇩h) = ts⇩s⇩b⇩h!i;
               execs = takeWhile (Not ∘ is_volatile_Write⇩s⇩b) sb;
               suspends = dropWhile (Not ∘ is_volatile_Write⇩s⇩b) sb
            in  ∃is 𝒟. instrs suspends @ is⇩s⇩b⇩h = is @ prog_instrs suspends ∧
                    𝒟⇩s⇩b⇩h = (𝒟 ∨ outstanding_refs is_volatile_Write⇩s⇩b sb ≠ {}) ∧
                ts!i = (hd_prog p⇩s⇩b⇩h suspends, 
                        is,
                        θ⇩s⇩b⇩h |` (dom θ⇩s⇩b⇩h - read_tmps suspends),(),
                        𝒟,  
                        acquired True execs 𝒪⇩s⇩b⇩h,
                        release execs (dom 𝒮⇩s⇩b⇩h) ℛ⇩s⇩b⇩h)
   ⟧ 
    ⟹ 
     (ts⇩s⇩b⇩h,m⇩s⇩b⇩h,𝒮⇩s⇩b⇩h) ∼ (ts,m,𝒮)"
apply (rule sim_config.intros)
apply (simp_all add: Let_def)
done

lemma  AssignAddr':
  "⟦∀sop. a ≠ Tmp sop; a'=Tmp (eval_expr t a); t'= t + used_tmps a; is=issue_expr t a ⟧ ⟹
   θ⊢ (Assign volatile a e A L R W, t) →⇩s 
         ((Assign volatile a' e A L R W, t'),is)"
  by (simp add: AssignAddr)


lemma  Assign':
  "⟦D ⊆ dom θ; is= issue_expr t e@[Write volatile (a θ) (eval_expr t e) (A θ) (L θ) (R θ) (W θ)]⟧ ⟹ 
   θ⊢ (Assign volatile (Tmp (D,a)) e A L R W, t) →⇩s 
         ((Skip, t + used_tmps e), is)"
  by (simp add: Assign)


lemma CASAddr':
  "⟦∀sop. a ≠ Tmp sop; a'=(Tmp (eval_expr t a));t'=t + used_tmps a; is=issue_expr t a ⟧ ⟹
   θ⊢ (CAS a c⇩e s⇩e A L R W, t) →⇩s 
         ((CAS a' c⇩e s⇩e A L R W, t'), is)"
  by (simp add: CASAddr)

lemma CASComp':
  "⟦∀sop. c⇩e ≠ Tmp sop;c⇩e'=(Tmp (eval_expr t c⇩e));t'=t + used_tmps c⇩e; is= issue_expr t c⇩e ⟧ ⟹
   θ⊢ (CAS (Tmp a) c⇩e s⇩e A L R W, t) →⇩s 
         ((CAS (Tmp a) c⇩e' s⇩e A L R W, t'), is)"
  by (cases a) (simp add: CASComp)
  
lemma CAS':
  "⟦D⇩a ⊆ dom θ; D⇩c ⊆ dom θ; eval_expr t s⇩e  = (D,f);t'=(t + used_tmps s⇩e); 
   cond = (λθ. the (θ t') = c θ);
   ret = (λv⇩1 v⇩2. v⇩1);
   is = issue_expr t s⇩e@
           [RMW (a θ) t' (D,f) cond ret 
            (A θ) (L θ) (R θ) (W θ) ]⟧  
   ⟹
   θ⊢ (CAS (Tmp (D⇩a,a)) (Tmp (D⇩c,c)) s⇩e A L R W, t) →⇩s 
         ((Skip, Suc t'),is )"
  by (simp add: CAS)


lemma SCond':
  "∀sop. e ≠ Tmp sop ⟹ e'= (Tmp (eval_expr t e)) ⟹ t'=t + used_tmps e ⟹ is=issue_expr t e
   ⟹
   θ⊢ (Cond e s⇩1 s⇩2, t) →⇩s 
    ((Cond e' s⇩1 s⇩2, t'), is)"
  by (simp add: Cond)

lemma SWhile':
  "s'= (Cond e (Seq s (While e s)) Skip) ⟹
   θ⊢ (While e s, t) →⇩s ((s', t),[])"
  by (simp add: stmt_step.While)


theorem (in xvalid_program) simulation_hol:
  "(ts⇩s⇩b⇩h,m⇩s⇩b⇩h,𝒮⇩s⇩b⇩h) ⇒⇩s⇩b⇩h (ts⇩s⇩b⇩h',m⇩s⇩b⇩h',𝒮⇩s⇩b⇩h') ∧
   (ts⇩s⇩b⇩h,m⇩s⇩b⇩h,𝒮⇩s⇩b⇩h) ∼ (ts,m,𝒮) ∧ safe_reach_direct safe_delayed (ts, m, 𝒮) ∧
   invariant ts⇩s⇩b⇩h 𝒮⇩s⇩b⇩h m⇩s⇩b⇩h ⟶
  invariant ts⇩s⇩b⇩h' 𝒮⇩s⇩b⇩h' m⇩s⇩b⇩h' ∧
           (∃ts' 𝒮' m'. (ts,m,𝒮) ⇒⇩d⇧* (ts',m',𝒮') ∧ (ts⇩s⇩b⇩h',m⇩s⇩b⇩h',𝒮⇩s⇩b⇩h') ∼ (ts',m',𝒮'))"
  apply clarify
  apply (drule simulation')
  by auto

theorem (in xvalid_program_progress) store_buffer_execution_result_sequential_consistent'_hol:
"(ts⇩s⇩b,m,x) ⇒⇩s⇩b⇧* (ts⇩s⇩b',m',x') ∧
empty_store_buffers ts⇩s⇩b' ∧
ts⇩s⇩b ∼⇩d ts ∧
initial⇩v ts 𝒮 valid ∧
safe_reach_virtual safe_free_flowing (ts,m,𝒮) 
⟶
(∃ts' 𝒮'. 
          (ts,m,𝒮) ⇒⇩v⇧* (ts',m',𝒮') ∧ ts⇩s⇩b' ∼⇩d ts')"
  apply clarify
  apply (drule store_buffer_execution_result_sequential_consistent')
  apply auto
  done

end
(*>*)