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⇩₁ v⇩₂. v⇩₁);
   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⇩₁ s⇩₂, t) →⇩_s 
    ((Cond e' s⇩₁ s⇩₂, 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
(*>*)