Theory PIMP

(* Copyright (C) 2007--2010 Norbert Schirmer
 * All rights reserved, DFKI GmbH 
 *)
(*
header {* Parallel - IMP *}
*)

subsection ‹PIMP›

theory PIMP
imports ReduceStoreBufferSimulation
begin

datatype expr = Const val | Mem bool addr | Tmp sop
              | Unop "val ⇒ val" expr 
              | Binop "val ⇒ val ⇒ val" expr expr
(* Hmm. addr's should be vals ? *)
datatype stmt = 
                Skip 
              | Assign bool expr expr "tmps ⇒ owns" "tmps ⇒ owns" "tmps ⇒ owns" "tmps ⇒ owns" 
              | CAS expr expr expr "tmps ⇒ owns" "tmps ⇒ owns" "tmps ⇒ owns" "tmps ⇒ owns" 
              | Seq "stmt" "stmt"
              | Cond expr "stmt" "stmt"
              | While  expr "stmt" 


              | SGhost "tmps ⇒ owns" "tmps ⇒ owns" "tmps ⇒ owns" "tmps ⇒ owns"
              | SFence

(*
FIXME:
Genralisation of Assignment and CAS (and SGhost) would be nice:
  * A L R W sets not just dependent on value of addr, but on tmps 
    (beware of domain: thm program_step_tmps_mono) or some ghost state
*)
primrec used_tmps:: "expr ⇒ nat" ― ‹number of temporaries used›
where
"used_tmps (Const v) = 0"
| "used_tmps (Mem volatile addr) = 1"
| "used_tmps (Tmp sop) = 0"
| "used_tmps (Unop f e) = used_tmps e"
| "used_tmps (Binop f e1 e2) = used_tmps e1 + used_tmps e2"

primrec issue_expr:: "tmp ⇒ expr ⇒ instr list" ― ‹load operations›
where
"issue_expr t (Const v) = []"
|"issue_expr t (Mem volatile a) = [Read volatile a t]"
|"issue_expr t (Tmp sop) = []"
|"issue_expr t (Unop f e) = issue_expr t e"
|"issue_expr t (Binop f e1 e2) = issue_expr t e1 @ issue_expr (t + (used_tmps e1)) e2" 

primrec eval_expr:: "tmp ⇒ expr ⇒ sop" ― ‹calculate result›
where
"eval_expr t (Const v) = ({},λθ. v)"
|"eval_expr t (Mem volatile a) = ({t},λθ. the (θ t))"
|"eval_expr t (Tmp sop) = sop"
(*
"eval_expr t (Tmp sop) = ({i. i ∈ fst sop ∧ i < t}, λθ. snd sop (θ |`{i. i ∈ fst sop ∧ i < t}))"*)
                         ― ‹trick to enforce sop to be sensible in the current context, without
                               having to include wellformedness constraints›
|"eval_expr t (Unop f e) = (let (D,fe) = eval_expr t e in (D,λθ. f (fe θ))) "
|"eval_expr t (Binop f e1 e2) = (let (D1,f1) = eval_expr t e1;
                                    (D2,f2) = eval_expr (t + (used_tmps e1)) e2  
                                in (D1 ∪ D2,λθ. f (f1 θ) (f2 θ)))" 

primrec valid_sops_expr:: "nat ⇒ expr ⇒ bool"
where
"valid_sops_expr t (Const v) = True"
|"valid_sops_expr t (Mem volatile a) = True"
|"valid_sops_expr t (Tmp sop) = ((∀t' ∈ fst sop. t' < t) ∧ valid_sop sop)"
|"valid_sops_expr t (Unop f e) = valid_sops_expr t e"
|"valid_sops_expr t (Binop f e1 e2) = (valid_sops_expr t e1 ∧ valid_sops_expr t e2)" 


primrec valid_sops_stmt:: "nat ⇒ stmt ⇒ bool"
where
"valid_sops_stmt t Skip = True"
|"valid_sops_stmt t (Assign volatile a e A L R W) = (valid_sops_expr t a ∧ valid_sops_expr t e)"
|"valid_sops_stmt t (CAS a ce se A L R W) = (valid_sops_expr t a ∧ valid_sops_expr t ce ∧ 
                                            valid_sops_expr t se)"
|"valid_sops_stmt t (Seq s1 s2) = (valid_sops_stmt t s1 ∧ valid_sops_stmt t s2)"
|"valid_sops_stmt t (Cond e s1 s2) = (valid_sops_expr t e ∧ valid_sops_stmt t s1 ∧ valid_sops_stmt t s2)"
|"valid_sops_stmt t (While e s) = (valid_sops_expr t e ∧ valid_sops_stmt t s)"
|"valid_sops_stmt t (SGhost A L R W) = True"
|"valid_sops_stmt t SFence = True"

  
type_synonym stmt_config = "stmt × nat"
consts isTrue:: "val ⇒ bool"

inductive stmt_step:: "tmps ⇒ stmt_config  ⇒ stmt_config × instrs  ⇒ bool" 
  ("_⊢ _ →s _" [60,60,60] 100)
for θ
where

  AssignAddr:
  "∀sop. a ≠ Tmp sop  ⟹
   θ⊢ (Assign volatile a e A L R W, t) →s 
         ((Assign volatile (Tmp (eval_expr t a)) e A L R W, t + used_tmps a), issue_expr t a)"

|  Assign:
  "D ⊆ dom θ ⟹ 
   θ⊢ (Assign volatile (Tmp (D,a)) e A L R W, t) →s 
         ((Skip, t + used_tmps e), 
           issue_expr t e@[Write volatile (a θ) (eval_expr t e) (A θ) (L θ) (R θ) (W θ)])"


| CASAddr:
  "∀sop. a ≠ Tmp sop  ⟹
   θ⊢ (CAS a ce se A L R W, t) →s 
         ((CAS (Tmp (eval_expr t a)) ce se A L R W, t + used_tmps a), issue_expr t a)"


| CASComp:
  "∀sop. ce ≠ Tmp sop  ⟹
   θ⊢ (CAS (Tmp (Da,a)) ce se A L R W, t) →s 
         ((CAS (Tmp (Da,a)) (Tmp (eval_expr t ce)) se A L R W, t + used_tmps ce), issue_expr t ce)"

| CAS:
  "⟦Da ⊆ dom θ; Dc ⊆ dom θ; eval_expr t se  = (D,f) ⟧  
   ⟹
   θ⊢ (CAS (Tmp (Da,a)) (Tmp (Dc,c)) se A L R W, t) →s 
         ((Skip, Suc (t + used_tmps se)), issue_expr t se@
           [RMW (a θ) (t + used_tmps se) (D,f) (λθ. the (θ (t + used_tmps se)) = c θ) (λv1 v2. v1) 
            (A θ) (L θ) (R θ) (W θ) ])"

| Seq:
  "θ⊢ (s1, t) →s ((s1', t'), is) 
   ⟹ 
   θ⊢ (Seq s1 s2, t) →s ((Seq s1' s2, t'),is)"

| SeqSkip:
  "θ⊢ (Seq Skip s2, t) →s ((s2, t), [])"


| Cond:
  "∀sop. e ≠ Tmp sop 
   ⟹
   θ⊢ (Cond e s1 s2, t) →s 
    ((Cond (Tmp (eval_expr t e)) s1 s2, t + used_tmps e), issue_expr t e)"

| CondTrue:
  "⟦D ⊆ dom θ; isTrue (e θ)⟧ 
   ⟹ 
   θ⊢ (Cond (Tmp (D,e)) s1 s2, t) →s ((s1, t),[])"

| CondFalse:
  "⟦D ⊆ dom θ; ¬ isTrue (e θ)⟧ 
   ⟹ 
   θ⊢ (Cond (Tmp (D,e)) s1 s2, t) →s ((s2, t),[])"

| While:
  "θ⊢ (While e s, t) →s 
   ((Cond e (Seq s (While e s)) Skip, t),[])"

| SGhost:
  "θ⊢ (SGhost A L R W, t) →s ((Skip, t),[Ghost (A θ) (L θ) (R θ) (W θ)])"

| SFence:
  "θ⊢ (SFence, t) →s ((Skip, t),[Fence])"

inductive_cases stmt_step_cases [cases set]:
"θ⊢ (Skip, t) →s c"
"θ⊢ (Assign volatile a e A L R W, t) →s c"
"θ⊢ (CAS a ce se A L R W, t) →s c"
"θ⊢ (Seq s1 s2, t) →s c"
"θ⊢ (Cond e s1 s2, t) →s c"
"θ⊢ (While e s, t) →s c"
"θ⊢ (SGhost A L R W, t) →s c"
"θ⊢ (SFence, t) →s c"

lemma valid_sops_expr_mono: "⋀t t'. valid_sops_expr t e ⟹ t ≤ t'  ⟹ valid_sops_expr t' e"
  by (induct e) auto

lemma valid_sops_stmt_mono: "⋀t t'.  valid_sops_stmt t s ⟹ t ≤ t'  ⟹ valid_sops_stmt t' s"
  by (induct s) (auto intro: valid_sops_expr_mono)

lemma valid_sops_expr_valid_sop: "⋀t. valid_sops_expr t e ⟹ valid_sop (eval_expr t e)"
proof (induct e)
  case (Unop f e)
  then obtain "valid_sops_expr t e"
    by simp
  from Unop.hyps [OF this]
  have vs: "valid_sop (eval_expr t e)"
    by simp
  obtain D g where eval_e: "eval_expr t e = (D,g)"
    by (cases "eval_expr t e")

  interpret valid_sop "(D,g)"
    using vs eval_e
    by simp

  show ?case
    apply (clarsimp simp add: Let_def valid_sop_def eval_e)
    apply (drule valid_sop [OF refl])
    apply simp
    done
next
  case (Binop f e1 e2)
  then obtain v1: "valid_sops_expr t e1" and v2: "valid_sops_expr t e2"
    by simp
  with Binop.hyps (1) [of t]  Binop.hyps (2) [of "(t + used_tmps e1)"]  
    valid_sops_expr_mono [OF v2, of "(t + used_tmps e1)"]
  obtain vs1: "valid_sop (eval_expr t e1)" and vs2: "valid_sop (eval_expr (t + used_tmps e1) e2)"
    by auto
  obtain D1 g1 where eval_e1: "eval_expr t e1 = (D1,g1)"
    by (cases "eval_expr t e1")
  obtain D2 g2 where eval_e2: "eval_expr (t + used_tmps e1) e2 = (D2,g2)"
    by (cases "eval_expr (t + used_tmps e1) e2")
  interpret vs1: valid_sop "(D1,g1)"
    using vs1 eval_e1 by auto
  interpret vs2: valid_sop "(D2,g2)"
    using vs2 eval_e2 by auto
  {
    fix θ:: "nat⇒val option" 
    assume D1: "D1 ⊆ dom θ" 
    assume D2: "D2 ⊆ dom θ"
    have "f (g1 θ) (g2 θ) = f (g1 (θ |` (D1 ∪ D2))) (g2 (θ |` (D1 ∪ D2)))"
    proof -
      from vs1.valid_sop [OF refl D1]
      have "g1 θ = g1 (θ |` D1)".
      also
      from D1 have D1': "D1 ⊆ dom (θ |` (D1 ∪ D2))"
	by auto
      have "θ |` (D1 ∪ D2) |` D1 = θ |` D1"
	apply (rule ext)
	apply (auto simp add: restrict_map_def)
	done
      with vs1.valid_sop [OF refl D1']
      have "g1 (θ |` D1) = g1 (θ |` (D1 ∪ D2))"
	by auto
      finally have g1: "g1 (θ |` (D1 ∪ D2)) = g1 θ"
	by simp

      from vs2.valid_sop [OF refl D2]
      have "g2 θ = g2 (θ |` D2)".
      also
      from D2 have D2': "D2 ⊆ dom (θ |` (D1 ∪ D2))"
	by auto
      have "θ |` (D1 ∪ D2) |` D2 = θ |` D2"
	apply (rule ext)
	apply (auto simp add: restrict_map_def)
	done
      with vs2.valid_sop [OF refl D2']
      have "g2 (θ |` D2) = g2 (θ |` (D1 ∪ D2))"
	by auto
      finally have g2: "g2 (θ |` (D1 ∪ D2)) = g2 θ"
	by simp

      from g1 g2 show ?thesis by simp
    qed
  }
      
  note lem=this
  show ?case
    apply (clarsimp simp add: Let_def valid_sop_def eval_e1 eval_e2)
    apply (rule lem)
    by auto
qed (auto simp add: valid_sop_def)

lemma valid_sops_expr_eval_expr_in_range: 
  "⋀t. valid_sops_expr t e ⟹ ∀t' ∈ fst (eval_expr t e). t' < t + used_tmps e"
proof (induct e)
  case (Unop f e)
  thus ?case
    apply (cases "eval_expr t e")
    apply auto
    done
next
  case (Binop f e1 e2)
  then obtain v1: "valid_sops_expr t e1" and v2: "valid_sops_expr t e2"
    by simp
  from valid_sops_expr_mono [OF v2]
  have v2': "valid_sops_expr (t + used_tmps e1) e2"
    by auto
  from Binop.hyps (1) [OF v1] Binop.hyps (2) [OF v2']
  show ?case
    apply (cases "eval_expr t e1")
    apply (cases "eval_expr (t + used_tmps e1) e2")
    apply auto
    done
qed auto



lemma stmt_step_tmps_count_mono:
  assumes step: "θ⊢ (s,t) →s ((s',t'),is)"
  shows "t ≤ t'"
using step
by (induct x=="(s,t)" y=="((s',t'),is)" arbitrary: s t s' t' "is" rule: stmt_step.induct) force+
  

lemma valid_sops_stmt_invariant:
  assumes step: "θ⊢ (s,t) →s ((s',t'),is)"
  shows "valid_sops_stmt t s ⟹ valid_sops_stmt t' s'"
using step
proof (induct x=="(s,t)" y=="((s',t'),is)" arbitrary: s t s' t' "is" rule: stmt_step.induct)
  case AssignAddr thus ?case by 
  (force simp add: valid_sops_expr_valid_sop intro: valid_sops_stmt_mono valid_sops_expr_mono  
     dest: valid_sops_expr_eval_expr_in_range)
next
  case Assign thus ?case by simp
next
  case CASAddr thus ?case by 
  (force simp add: valid_sops_expr_valid_sop intro: valid_sops_stmt_mono valid_sops_expr_mono  
     dest: valid_sops_expr_eval_expr_in_range)
next
  case CASComp thus ?case by 
  (force simp add: valid_sops_expr_valid_sop intro: valid_sops_stmt_mono valid_sops_expr_mono  
     dest: valid_sops_expr_eval_expr_in_range)
next
  case CAS thus ?case by simp
next
  case Seq thus ?case by (force intro: valid_sops_stmt_mono dest: stmt_step_tmps_count_mono)
next
  case SeqSkip thus ?case by auto
next
  case Cond thus ?case 
    by (fastforce simp add: valid_sops_expr_valid_sop intro: valid_sops_stmt_mono 
     dest: valid_sops_expr_eval_expr_in_range)
next
  case CondTrue thus ?case by force
next
  case CondFalse thus ?case by force
next
  case While thus ?case by auto
next
  case SGhost thus ?case by simp
next
  case SFence thus ?case by simp
qed


lemma map_le_restrict_map_eq: "m1 ⊆m m2 ⟹ D ⊆ dom m1 ⟹ m2 |` D = m1 |` D"
  apply (rule ext)
  apply (force simp add: restrict_map_def map_le_def)
  done


lemma sbh_step_preserves_load_tmps_bound: 
  assumes step: "(is,𝒪,𝒟,θ,sb,𝒮,m) →sbh (is',𝒪',𝒟',θ',sb',𝒮',m')"
  assumes less: "∀i ∈ load_tmps is. i < n" 
  shows "∀i ∈ load_tmps is'. i < n"
  using step less
  by cases auto

lemma sbh_step_preserves_read_tmps_bound:
  assumes step: "(is,θ,sb,m,𝒟,𝒪,𝒮) →sbh (is',θ',sb',m',𝒟',𝒪',𝒮')"
  assumes less_is: "∀i ∈ load_tmps is. i < n" 
  assumes less_sb: "∀i ∈ read_tmps sb. i < n" 
  shows "∀i ∈ read_tmps sb'. i < n"
  using step less_is less_sb
  by cases (auto simp add: read_tmps_append)

lemma sbh_step_preserves_tmps_bound:
  assumes step: "(is,θ,sb,m,𝒟,𝒪,𝒮) →sbh (is',θ',sb',m',𝒟',𝒪',𝒮')"
  assumes less_dom: "∀i ∈ dom θ. i < n" 
  assumes less_is: "∀i ∈ load_tmps is. i < n" 
  shows "∀i ∈ dom θ'. i < n"
  using step less_dom  less_is
  by cases (auto simp add: read_tmps_append)

lemma flush_step_preserves_read_tmps:
  assumes step: "(m,sb,𝒪) →f (m',sb',𝒪')"
  assumes less_sb: "∀i ∈ read_tmps sb. i < n" 
  shows "∀i ∈ read_tmps sb'. i < n"
  using step less_sb
  by cases (auto simp add: read_tmps_append)

lemma flush_step_preserves_write_sops:
  assumes step: "(m,sb,𝒪) →f (m',sb',𝒪')"
  assumes less_sb: "∀i∈⋃(fst ` write_sops sb). i < t" 
  shows "∀i∈⋃(fst ` write_sops sb'). i < t"
  using step less_sb
  by cases (auto simp add: read_tmps_append)

lemma issue_expr_load_tmps_range': 
  "⋀t. load_tmps (issue_expr t e) = {i. t ≤ i ∧ i < t + used_tmps e}"
apply (induct e)
apply (force simp add: load_tmps_append)+
done


lemma issue_expr_load_tmps_range: 
  "⋀t. ∀i ∈ load_tmps (issue_expr t e). t ≤ i ∧ i < t + (used_tmps e)"
by (auto simp add: issue_expr_load_tmps_range')


lemma stmt_step_load_tmps_range':
  assumes step: "θ⊢ (s, t) →s ((s', t'),is)"
  shows "load_tmps is = {i. t ≤ i ∧ i < t'}"
  using step 
  apply (induct x=="(s,t)" y=="((s',t'),is)" arbitrary: s t s' t' "is" rule: stmt_step.induct)
  apply (force simp add: load_tmps_append simp add: issue_expr_load_tmps_range')+
  done


lemma stmt_step_load_tmps_range:
  assumes step: "θ⊢ (s, t) →s ((s', t'),is)"
  shows "∀i ∈ load_tmps is. t ≤ i ∧ i < t'"
using stmt_step_load_tmps_range' [OF step]
by auto


lemma distinct_load_tmps_issue_expr: "⋀t. distinct_load_tmps (issue_expr t e)"
  apply (induct e)
  apply (auto simp add: distinct_load_tmps_append dest!: issue_expr_load_tmps_range [rule_format])
  done

lemma max_used_load_tmps: "t + used_tmps e ∉ load_tmps (issue_expr t e)"
proof -
  from issue_expr_load_tmps_range [rule_format, of "t+used_tmps e"]
  show ?thesis
    by auto
qed

lemma stmt_step_distinct_load_tmps:
  assumes step: "θ⊢ (s, t) →s ((s', t'),is)"
  shows "distinct_load_tmps is"
  using step 
  apply (induct x=="(s,t)" y=="((s',t'),is)" arbitrary: s t s' t' "is" rule: stmt_step.induct)
  apply (force simp add: distinct_load_tmps_append distinct_load_tmps_issue_expr max_used_load_tmps)+  
  done

lemma store_sops_issue_expr [simp]: "⋀t. store_sops (issue_expr t e) = {}"
  apply (induct e)
  apply (auto simp add: store_sops_append)
  done


lemma stmt_step_data_store_sops_range:
  assumes step: "θ⊢ (s, t) →s ((s', t'),is)"
  assumes valid: "valid_sops_stmt t s"
  shows "∀(D,f) ∈ store_sops is. ∀i ∈ D. i < t'"
using step valid
proof (induct x=="(s,t)" y=="((s',t'),is)" arbitrary: s t s' t' "is" rule: stmt_step.induct)
  case AssignAddr
  thus ?case
    by auto
next
  case (Assign D volatile a e)
  thus ?case
    apply (cases "eval_expr t e")
    apply (auto simp add: store_sops_append intro: valid_sops_expr_eval_expr_in_range [rule_format])
    done
next
  case CASAddr
  thus ?case
    by auto
next
  case CASComp
  thus ?case
    by auto
next
  case (CAS _ _ D f a A L R)
  thus ?case
    by (fastforce simp add: store_sops_append dest: valid_sops_expr_eval_expr_in_range [rule_format])
next
  case Seq
  thus ?case
    by (force intro: valid_sops_stmt_mono )
next
  case SeqSkip thus ?case by simp
next
  case Cond thus ?case
    by auto
next
  case CondTrue thus ?case by auto
next
  case CondFalse thus ?case by auto
next
  case While thus ?case by auto
next
  case SGhost thus ?case by auto
next
  case SFence thus ?case by auto
qed

lemma sbh_step_distinct_load_tmps_prog_step: 
      assumes step: "θ⊢(s,t) →s ((s',t'),is')"
  assumes load_tmps_le: "∀i ∈ load_tmps is. i < t"
  assumes read_tmps_le: "∀i ∈ read_tmps sb. i < t"
  shows "distinct_load_tmps is' ∧ (load_tmps is' ∩ load_tmps is = {}) ∧
         (load_tmps is' ∩ read_tmps sb) = {}"
proof - 
  from stmt_step_load_tmps_range [OF step] stmt_step_distinct_load_tmps [OF step] 
    load_tmps_le read_tmps_le
  show ?thesis
    by force
qed


lemma data_dependency_consistent_instrs_issue_expr: 
  "⋀t T. data_dependency_consistent_instrs T (issue_expr t e)"
  apply (induct e)
  apply (auto simp add: data_dependency_consistent_instrs_append 
    dest!: issue_expr_load_tmps_range [rule_format] 
    )
  done

lemma dom_eval_expr:
  "⋀t. ⟦valid_sops_expr t e; x ∈ fst (eval_expr t e)⟧ ⟹ x ∈ {i. i < t} ∪ load_tmps (issue_expr t e)"
proof (induct e)
  case Const thus ?case by simp
next
  case Mem thus ?case by simp
next
  case Tmp thus ?case by simp
next
  case (Unop f e)
  thus ?case
    by (cases "eval_expr t e") auto
next
  case (Binop f e1 e2)
  then obtain valid1: "valid_sops_expr t e1" and valid2: "valid_sops_expr t e2"
    by auto
  from valid_sops_expr_mono [OF valid2] have valid2': "valid_sops_expr (t+used_tmps e1) e2"
    by auto

  from Binop.hyps (1) [OF valid1] Binop.hyps (2) [OF valid2'] Binop.prems
  show ?case
    apply (case_tac "eval_expr t e1")
    apply (case_tac "eval_expr (t+used_tmps e1) e2")
    apply (auto simp add: load_tmps_append issue_expr_load_tmps_range')
    done
qed


lemma Cond_not_s1: "s1 ≠ Cond e s1 s2 " 
  by (induct s1) auto

lemma Cond_not_s2: "s2 ≠ Cond e s1 s2 " 
  by (induct s2) auto

lemma Seq_not_s1: "s1 ≠ Seq s1 s2"
  by (induct s1) auto

lemma Seq_not_s2: "s2 ≠ Seq s1 s2"
  by (induct s2) auto

lemma prog_step_progress:
  assumes step: "θ⊢(s,t) →s ((s',t'),is)"
  shows "(s',t') ≠ (s,t) ∨ is ≠ []"
using step 
proof (induct x=="(s,t)" y=="((s',t'),is)" arbitrary: s t s' t' "is" rule: stmt_step.induct)
  case (AssignAddr a _ _ _ _ _ _ t) thus ?case 
    by (cases "eval_expr t a") auto
next
  case Assign thus ?case by auto
next
  case (CASAddr a _ _ _ _ _ _ t) thus ?case by (cases "eval_expr t a") auto 
next
  case (CASComp ce _ _ _ _ _ _ _ t) thus ?case by (cases "eval_expr t ce") auto  
next
  case CAS thus ?case by auto
next
  case (Cond e _ _ t) thus ?case by (cases "eval_expr t e") auto  
next
  case CondTrue thus ?case using Cond_not_s1 by auto
next
  case CondFalse thus ?case using Cond_not_s2 by auto
next
  case Seq thus ?case by force
next
  case SeqSkip thus ?case using Seq_not_s2 by auto
next
  case While thus ?case by auto
next
  case SGhost thus ?case by auto
next
  case SFence thus ?case by auto
qed

lemma stmt_step_data_dependency_consistent_instrs:
  assumes step: "θ⊢ (s, t) →s ((s', t'),is)"
  assumes valid: "valid_sops_stmt t s"
  shows "data_dependency_consistent_instrs ({i. i < t}) is"
  using step valid 
proof (induct x=="(s,t)" y=="((s',t'),is)" arbitrary: s t s' t' "is" T rule: stmt_step.induct)
  case AssignAddr
  thus ?case
    by (fastforce simp add: simp add: data_dependency_consistent_instrs_append 
    data_dependency_consistent_instrs_issue_expr load_tmps_append
    dest: dom_eval_expr)
next
  case Assign
  thus ?case
    by (fastforce simp add: simp add: data_dependency_consistent_instrs_append 
    data_dependency_consistent_instrs_issue_expr load_tmps_append
    dest: dom_eval_expr)
next
  case CASAddr
  thus ?case
    by (fastforce simp add: simp add: data_dependency_consistent_instrs_append 
    data_dependency_consistent_instrs_issue_expr load_tmps_append
    dest: dom_eval_expr)
next
  case CASComp
  thus ?case
    by (fastforce simp add: simp add: data_dependency_consistent_instrs_append 
    data_dependency_consistent_instrs_issue_expr load_tmps_append
    dest: dom_eval_expr)
next
  case CAS
  thus ?case
    by (fastforce simp add: simp add: data_dependency_consistent_instrs_append 
      data_dependency_consistent_instrs_issue_expr load_tmps_append
      dest: dom_eval_expr)
next
  case Seq
  thus ?case
    by (fastforce simp add: simp add: data_dependency_consistent_instrs_append)
next
  case SeqSkip thus ?case by auto
next
  case Cond
  thus ?case
    by (fastforce simp add: simp add: data_dependency_consistent_instrs_append 
      data_dependency_consistent_instrs_issue_expr load_tmps_append
      dest: dom_eval_expr)
next
  case CondTrue thus ?case by auto
next
  case CondFalse thus ?case by auto
next
  case While
  thus ?case by auto
next
  case SGhost thus ?case by auto
next
  case SFence thus ?case by auto
qed



lemma sbh_valid_data_dependency_prog_step: 
  assumes step: "θ⊢(s,t) →s ((s',t'),is')"
  assumes store_sops_le: "∀i ∈ ⋃(fst ` store_sops is). i < t"
  assumes write_sops_le: "∀i ∈ ⋃(fst ` write_sops sb). i < t"
  assumes valid: "valid_sops_stmt t s"
  shows "data_dependency_consistent_instrs ({i. i < t}) is' ∧ 
         load_tmps is' ∩ ⋃(fst ` store_sops is)  = {} ∧
         load_tmps is' ∩ ⋃(fst ` write_sops sb)  = {}"
proof -
  from stmt_step_data_dependency_consistent_instrs [OF step valid] stmt_step_load_tmps_range [OF step]
  store_sops_le write_sops_le
  show ?thesis
    by fastforce
qed

lemma sbh_load_tmps_fresh_prog_step:
  assumes step: "θ⊢(s,t) →s ((s',t'),is')"
  assumes tmps_le: "∀i ∈ dom θ. i < t"
  shows "load_tmps is' ∩ dom θ = {}"
proof -
  from stmt_step_load_tmps_range [OF step] tmps_le
  show ?thesis
    apply auto
    subgoal for x
    apply (drule_tac x=x in bspec )
    apply  assumption
    apply (drule_tac x=x in bspec )
    apply  fastforce
    apply simp
    done
    done
qed

lemma sbh_valid_sops_prog_step:
  assumes step: "θ⊢(s,t) →s ((s',t'),is)"
  assumes valid: "valid_sops_stmt t s"
  shows "∀sop∈store_sops is. valid_sop sop"
using step valid
proof (induct x=="(s,t)" y=="((s',t'),is)" arbitrary: s t s' t' "is" rule: stmt_step.induct)
  case AssignAddr
  thus ?case by auto
next
  case Assign
  thus ?case
    by (auto simp add: store_sops_append valid_sops_expr_valid_sop)
next
  case CASAddr
  thus ?case by auto
next
  case CASComp
  thus ?case by auto
next
  case CAS
  thus ?case
    by (fastforce simp add: store_sops_append dest: valid_sops_expr_valid_sop)
next
  case Seq
  thus ?case
    by (force intro: valid_sops_stmt_mono )
next
  case SeqSkip thus ?case by simp
next
  case Cond thus ?case
    by auto
next
  case CondTrue thus ?case by auto
next
  case CondFalse thus ?case by auto
next
  case While thus ?case by auto
next
  case SGhost thus ?case by auto
next
  case SFence thus ?case by auto
qed

primrec prog_configs:: "'a memref list ⇒ 'a set"
where
"prog_configs [] = {}"
|"prog_configs (x#xs) = (case x of 
                         Progsb p p' is ⇒ {p,p'} ∪ prog_configs xs
                       | _ ⇒ prog_configs xs)"

lemma prog_configs_append: "⋀ys. prog_configs (xs@ys) = prog_configs xs ∪ prog_configs ys"
  by (induct xs) (auto split: memref.splits)

lemma prog_configs_in1: "Progsb p1 p2 is ∈ set xs ⟹ p1 ∈ prog_configs xs"
  by (induct xs) (auto split: memref.splits)

lemma prog_configs_in2: "Progsb p1 p2 is ∈ set xs ⟹ p2 ∈ prog_configs xs"
  by (induct xs) (auto split: memref.splits)

lemma prog_configs_mono: "⋀ys. set xs ⊆ set ys ⟹ prog_configs xs ⊆ prog_configs ys"
  by (induct xs) (auto split: memref.splits simp add: prog_configs_append
  prog_configs_in1 prog_configs_in2)

locale separated_tmps = 
fixes ts
assumes valid_sops_stmt: "⟦i < length ts; ts!i = ((s,t),is,θ,sb,𝒟,𝒪)⟧ 
  ⟹ valid_sops_stmt t s"
assumes valid_sops_stmt_sb: "⟦i < length ts; ts!i = ((s,t),is,θ,sb,𝒟,𝒪); (s',t') ∈ prog_configs sb⟧ 
  ⟹  valid_sops_stmt t' s'"
assumes load_tmps_le: "⟦i < length ts; ts!i = ((s,t),is,θ,sb,𝒟,𝒪)⟧ 
  ⟹ ∀i ∈ load_tmps is. i < t"
assumes read_tmps_le: "⟦i < length ts; ts!i = ((s,t),is,θ,sb,𝒟,𝒪)⟧ 
  ⟹ ∀i ∈ read_tmps sb. i < t"
assumes store_sops_le: "⟦i < length ts; ts!i = ((s,t),is,θ,sb,𝒟,𝒪)⟧ 
  ⟹ ∀i ∈ ⋃(fst ` store_sops is). i < t"
assumes write_sops_le: "⟦i < length ts; ts!i = ((s,t),is,θ,sb,𝒟,𝒪)⟧ 
  ⟹ ∀i ∈ ⋃(fst ` write_sops sb). i < t"
assumes tmps_le: "⟦i < length ts; ts!i = ((s,t),is,θ,sb,𝒟,𝒪)⟧ 
  ⟹ dom θ ∪ load_tmps is = {i. i < t}"

lemma (in separated_tmps)
  tmps_le': 
  assumes i_bound: "i < length ts" 
  assumes ts_i: "ts!i = ((s,t),is,θ,sb,𝒟,𝒪)"
  shows "∀i ∈ dom θ. i < t"
using tmps_le [OF i_bound ts_i] by auto



lemma (in separated_tmps) separated_tmps_nth_update: 
  "⟦i < length ts; valid_sops_stmt t s; ∀(s',t') ∈ prog_configs sb. valid_sops_stmt t' s'; 
   ∀i ∈ load_tmps is. i < t;∀i ∈ read_tmps sb. i < t;
    ∀i ∈ ⋃(fst ` store_sops is). i < t; ∀i ∈ ⋃(fst ` write_sops sb). i < t; dom θ ∪ load_tmps is = {i. i < t}⟧ 
   ⟹
   separated_tmps (ts[i:=((s,t),is,θ,sb,𝒟,𝒪)])"
  apply (unfold_locales)
  apply       (force intro: valid_sops_stmt  simp add: nth_list_update split: if_split_asm)
  apply      (fastforce intro: valid_sops_stmt_sb  simp add: nth_list_update split: if_split_asm)
  apply     (fastforce intro: load_tmps_le [rule_format] simp add: nth_list_update split: if_split_asm)
  apply    (fastforce intro: read_tmps_le [rule_format] simp add: nth_list_update split: if_split_asm)
  apply   (fastforce intro: store_sops_le [rule_format] simp add: nth_list_update split: if_split_asm)
  apply  (fastforce intro: write_sops_le [rule_format] simp add: nth_list_update split: if_split_asm)
  apply (fastforce dest: tmps_le [rule_format] simp add: nth_list_update split: if_split_asm)
  done

lemma hd_prog_app_in_first: "⋀ys. Progsb p p' is ∈ set xs ⟹ hd_prog q (xs @ ys) = hd_prog q xs"
  by (induct xs) (auto split: memref.splits)

lemma hd_prog_app_in_eq: "⋀ys. Progsb p p' is ∈ set xs ⟹ hd_prog q xs = hd_prog x xs"
  by (induct xs) (auto split: memref.splits)

lemma hd_prog_app_notin_first: "⋀ys. ∀p p' is. Progsb p p' is ∉ set xs ⟹ hd_prog q (xs @ ys) = hd_prog q ys"
  by (induct xs) (auto split: memref.splits)

lemma union_eq_subsetD: "A ∪ B = C ⟹ A ∪ B ⊆ C ∧  C ⊆ A ∪ B"
  by auto

lemma prog_step_preserves_separated_tmps:
  assumes i_bound: "i < length ts"  
  assumes ts_i: "ts!i = (p,is,θ,sb,𝒟,𝒪)" 
  assumes prog_step: "θ⊢ p →s (p', is')"
  assumes sep: "separated_tmps ts"
  shows "separated_tmps 
             (ts [i:=(p',is@is',θ,sb@[Progsb p p' is'],𝒟,𝒪)])"
proof -
  obtain s t where p: "p=(s,t)" by (cases p)
  obtain s' t' where p': "p'=(s',t')" by (cases p')
  note ts_i = ts_i [simplified p]
  note step = prog_step [simplified p p']
  interpret separated_tmps ts by fact
  have "separated_tmps (ts[i := ((s',t'), is @ is', θ, 
    sb @ [Progsb (s,t) (s',t') is'], 𝒟,𝒪)])"
  proof (rule separated_tmps_nth_update [OF i_bound])
    from stmt_step_load_tmps_range [OF step] load_tmps_le [OF i_bound ts_i]
    stmt_step_tmps_count_mono [OF step]
    show "∀i∈load_tmps (is @ is'). i < t'"
      by (auto simp add: load_tmps_append)
  next
    from read_tmps_le [OF i_bound ts_i] stmt_step_tmps_count_mono [OF step]
    show "∀i∈read_tmps (sb @ [Progsb (s, t) (s', t') is']). i < t'"
      by (auto simp add: read_tmps_append)
  next
    from stmt_step_data_store_sops_range [OF step] stmt_step_tmps_count_mono [OF step]
    store_sops_le [OF i_bound ts_i] valid_sops_stmt [OF i_bound ts_i]
    show "∀i∈⋃(fst ` store_sops (is @ is')). i < t'"
      by (fastforce simp add: store_sops_append)
  next
    from 
      stmt_step_tmps_count_mono [OF step] write_sops_le [OF i_bound ts_i]
    show "∀i∈⋃(fst ` write_sops (sb @ [Progsb (s, t) (s', t') is'])). i < t'"
      by (fastforce simp add: write_sops_append)
  next
    from tmps_le [OF i_bound ts_i] 
    have "dom θ ∪ load_tmps is = {i. i < t}" by simp
    with stmt_step_load_tmps_range' [OF step] stmt_step_tmps_count_mono [OF step]
    show "dom θ ∪ load_tmps (is @ is') = {i. i < t'}"
      apply (clarsimp simp add: load_tmps_append)
      apply rule
      apply  (drule union_eq_subsetD)
      apply  fastforce
      apply clarsimp
      subgoal for x
      apply (case_tac "t ≤ x")
      apply  simp
      apply (subgoal_tac "x < t")
      apply  fastforce
      apply fastforce
      done
      done
  next
    from valid_sops_stmt_invariant [OF prog_step [simplified p p'] valid_sops_stmt [OF i_bound ts_i]]
    show "valid_sops_stmt t' s'".
  next
    show "∀(s', t')∈prog_configs (sb @ [Progsb (s, t) (s', t') is']).
             valid_sops_stmt t' s'"
    proof -
      {
	fix s1 t1 
	assume cfgs: "(s1,t1) ∈ prog_configs (sb @ [Progsb (s, t) (s', t') is'])"
	have "valid_sops_stmt t1 s1"
	proof -
	  from valid_sops_stmt [OF i_bound ts_i]
	  have "valid_sops_stmt t s".
	  moreover
	  from valid_sops_stmt_invariant [OF prog_step [simplified p p'] valid_sops_stmt [OF i_bound ts_i]]
	  have "valid_sops_stmt t' s'".
	  moreover
	  note valid_sops_stmt_sb [OF i_bound ts_i]
	  ultimately
	  show ?thesis
	    using cfgs
	    by (auto simp add: prog_configs_append)
	qed
      }
      thus ?thesis
	by auto
    qed
  qed
  then
  show ?thesis
    by (simp add: p p')
qed

lemma flush_step_sb_subset:
  assumes step: "(m,sb,𝒪) →f (m', sb',𝒪')"
  shows "set sb' ⊆ set sb"
using step
apply (induct c1=="(m,sb,𝒪)" c2=="(m',sb',𝒪')" arbitrary: m sb 𝒪 acq m' sb' 𝒪' acq
  rule: flush_step.induct)
apply auto
done

lemma flush_step_preserves_separated_tmps:
  assumes i_bound: "i < length ts"  
  assumes ts_i: "ts!i = (p,is,θ,sb,𝒟,𝒪,ℛ)" 
  assumes flush_step: "(m,sb,𝒪,ℛ,𝒮) →f (m', sb',𝒪',ℛ',𝒮')"
  assumes sep: "separated_tmps ts"
  shows "separated_tmps (ts [i:=(p,is,θ,sb',𝒟,𝒪',ℛ')])"
proof -
  obtain s t where p: "p=(s,t)" by (cases p)
  note ts_i = ts_i [simplified p]
  interpret separated_tmps ts by fact
  have "separated_tmps (ts [i:=((s,t),is,θ,sb',𝒟,𝒪',ℛ')])"
  proof (rule separated_tmps_nth_update [OF i_bound])
    from load_tmps_le [OF i_bound ts_i]
    show "∀i∈load_tmps is. i < t".
  next
    from flush_step_preserves_read_tmps [OF flush_step read_tmps_le [OF i_bound ts_i] ]
    show "∀i∈read_tmps sb'. i < t".
  next
    from store_sops_le [OF i_bound ts_i]
    show "∀i∈⋃(fst ` store_sops is). i < t".
  next
    from flush_step_preserves_write_sops [OF flush_step write_sops_le [OF i_bound ts_i]]
    show "∀i∈⋃(fst ` write_sops sb'). i < t".
  next
    from tmps_le [OF i_bound ts_i] 
    show "dom θ ∪ load_tmps is = {i. i < t}"
      by auto
  next
    from valid_sops_stmt [OF i_bound ts_i]
    show "valid_sops_stmt t s".
  next
    from valid_sops_stmt_sb [OF i_bound ts_i] flush_step_sb_subset [OF flush_step]
    show "∀(s', t')∈prog_configs sb'. valid_sops_stmt t' s'"
      by (auto dest!: prog_configs_mono)
  qed
  then
  show ?thesis
    by (simp add: p)
qed

lemma sbh_step_preserves_store_sops_bound:
  assumes step: "(is,θ,sb,m,𝒟,𝒪,ℛ,𝒮) →sbh (is',θ',sb',m',𝒟',𝒪',ℛ',𝒮')"
  assumes store_sops_le: "∀i∈⋃(fst ` store_sops is). i < t"
  shows "∀i∈⋃(fst ` store_sops is'). i < t"
  using step store_sops_le
  by cases auto

lemma sbh_step_preserves_write_sops_bound:
  assumes step: "(is,θ,sb,m,𝒟,𝒪,ℛ,𝒮) →sbh (is',θ',sb',m',𝒟',𝒪',ℛ',𝒮')"
  assumes store_sops_le: "∀i∈⋃(fst ` store_sops is). i < t"
  assumes write_sops_le: "∀i∈⋃(fst ` write_sops sb). i < t"
  shows "∀i∈⋃(fst ` write_sops sb'). i < t"
  using step store_sops_le write_sops_le
  by cases (auto simp add: write_sops_append)

lemma sbh_step_prog_configs_eq:
  assumes step: "(is,θ,sb,m,𝒟,𝒪,ℛ,𝒮) →sbh (is',θ',sb',m',𝒟',𝒪',ℛ',𝒮')"
  shows "prog_configs sb' = prog_configs sb"
using step
apply (cases)
apply (auto simp add: prog_configs_append)
done

lemma sbh_step_preserves_tmps_bound':
  assumes step: "(is,θ,sb,m,𝒟,𝒪,ℛ,𝒮) →sbh (is',θ',sb',m',𝒟',𝒪',ℛ',𝒮')"
  shows "dom θ ∪ load_tmps is = dom θ' ∪ load_tmps is'"
  using step 
  apply cases 
  apply (auto simp add: read_tmps_append)
  done

lemma sbh_step_preserves_separated_tmps:
  assumes i_bound: "i < length ts" 
  assumes ts_i: "ts!i = (p,is,θ,sb,𝒟,𝒪,ℛ)" 
  assumes memop_step: "(is, θ, sb, m,𝒟, 𝒪, ℛ,𝒮) →sbh 
                        (is', θ', sb', m',𝒟', 𝒪', ℛ',𝒮')" 
  assumes instr: "separated_tmps ts"
  shows "separated_tmps (ts [i:=(p,is',θ',sb',𝒟',𝒪',ℛ')])"
proof -
  obtain s t where p: "p=(s,t)" by (cases p)
  note ts_i = ts_i [simplified p]
  interpret separated_tmps ts by fact
  have "separated_tmps (ts [i:=((s,t),is',θ',sb',𝒟',𝒪',ℛ')])"
  proof (rule separated_tmps_nth_update [OF i_bound])
    from sbh_step_preserves_load_tmps_bound [OF memop_step load_tmps_le [OF i_bound ts_i]]
    show "∀i∈load_tmps is'. i < t".
  next
    from sbh_step_preserves_read_tmps_bound [OF memop_step load_tmps_le [OF i_bound ts_i]
        read_tmps_le [OF i_bound ts_i]]
    show "∀i∈read_tmps sb'. i < t".
  next
    from sbh_step_preserves_store_sops_bound [OF memop_step store_sops_le [OF i_bound ts_i]]
    show "∀i∈⋃(fst ` store_sops is'). i < t".
  next
    from sbh_step_preserves_write_sops_bound [OF memop_step store_sops_le [OF i_bound ts_i] 
      write_sops_le [OF i_bound ts_i]]
    show "∀i∈⋃(fst ` write_sops sb'). i < t".
  next
    from sbh_step_preserves_tmps_bound' [OF memop_step] tmps_le [OF i_bound ts_i]
    show "dom θ' ∪ load_tmps is' = {i. i < t}"
      by auto
  next
    from valid_sops_stmt [OF i_bound ts_i]
    show "valid_sops_stmt t s".
  next
    from valid_sops_stmt_sb [OF i_bound ts_i] sbh_step_prog_configs_eq [OF memop_step]
    show "∀(s', t')∈prog_configs sb'. valid_sops_stmt t' s'"
      by auto
  qed
  then show ?thesis
    by (simp add: p)
qed

definition 
  "valid_pimp ts ≡ separated_tmps ts"

lemma prog_step_preserves_valid:
  assumes i_bound: "i < length ts"  
  assumes ts_i: "ts!i = (p,is,θ,sb::stmt_config store_buffer,𝒟,𝒪,ℛ)" 
  assumes prog_step: "θ⊢ p →s (p', is')"
  assumes valid: "valid_pimp ts"
  shows "valid_pimp (ts [i:=(p',is@is',θ,sb@[Progsb p p' is'],𝒟,𝒪,ℛ)])"
using prog_step_preserves_separated_tmps [OF i_bound ts_i prog_step] valid
by (auto simp add: valid_pimp_def)

lemma flush_step_preserves_valid:
  assumes i_bound: "i < length ts"  
  assumes ts_i: "ts!i = (p,is,θ,sb::stmt_config store_buffer,𝒟,𝒪,ℛ)" 
  assumes flush_step: "(m,sb,𝒪,ℛ,𝒮) →f (m', sb',𝒪',ℛ',𝒮')"
  assumes valid: "valid_pimp ts"
  shows "valid_pimp (ts [i:=(p,is,θ,sb',𝒟,𝒪',ℛ')])"
using flush_step_preserves_separated_tmps [OF i_bound ts_i flush_step] valid
by (auto simp add: valid_pimp_def)

lemma sbh_step_preserves_valid:
  assumes i_bound: "i < length ts" 
  assumes ts_i: "ts!i = (p,is,θ,sb::stmt_config store_buffer,𝒟,𝒪,ℛ)" 
  assumes memop_step: "(is, θ, sb, m,𝒟, 𝒪, ℛ,𝒮) →sbh 
                        (is', θ', sb', m',𝒟', 𝒪', ℛ', 𝒮')" 
  assumes valid: "valid_pimp ts"
  shows "valid_pimp (ts [i:=(p,is',θ',sb',𝒟',𝒪',ℛ')])"
using 
sbh_step_preserves_separated_tmps [OF i_bound ts_i memop_step] valid
by (auto simp add: valid_pimp_def)

lemma hd_prog_prog_configs: "hd_prog p sb = p ∨ hd_prog p sb ∈ prog_configs sb"
  by (induct sb) (auto split:memref.splits)


interpretation PIMP: xvalid_program_progress stmt_step "λ(s,t). valid_sops_stmt t s" valid_pimp
proof
  fix θ p p' is'
  assume step: "θ⊢ p →s (p', is')" 
  obtain s t where p: "p = (s,t)"
    by (cases p)
  obtain s' t' where p': "p' = (s',t')"
    by (cases p')
  from prog_step_progress [OF step [simplified p p']]
  show "p' ≠ p ∨ is' ≠ []"
    by (simp add: p p')
next
  fix θ p p' is'
  assume step: "θ⊢ p →s (p', is')" 
    and valid_stmt: "(λ(s, t). valid_sops_stmt t s) p"
  obtain s t where p: "p = (s,t)"
    by (cases p)
  obtain s' t' where p': "p' = (s',t')"
    by (cases p')
  from valid_sops_stmt_invariant [OF step [simplified p p'] valid_stmt [simplified p, simplified]]
  have "valid_sops_stmt t' s'".
  then show "(λ(s, t). valid_sops_stmt t s) p'" by (simp add: p')
next
  fix i ts p "is" 𝒪 ℛ 𝒟 θ sb
  assume i_bound: "i < length ts" 
    and ts_i: "ts ! i = (p, is, θ, sb::(stmt × nat) memref list, 𝒟, 𝒪,ℛ)" 
    and valid: "valid_pimp ts"
  from valid have "separated_tmps ts"
    by (simp add: valid_pimp_def)
  then interpret separated_tmps ts .
  obtain s t where p: "p = (s,t)"
    by (cases p)
  from valid_sops_stmt [OF i_bound ts_i [simplified p]]
  show "(λ(s, t). valid_sops_stmt t s) p"
    by (auto simp add: p)
next
  fix i ts p "is" 𝒪 ℛ 𝒟  θ sb
  assume i_bound: "i < length ts" 
    and ts_i: "ts ! i = (p, is, θ, sb::(stmt × nat) memref list, 𝒟, 𝒪,ℛ)" 
    and valid: "valid_pimp ts"
  from valid have "separated_tmps ts"
    by (simp add: valid_pimp_def)
  then interpret separated_tmps ts .
  obtain s t where p: "p = (s,t)"
    by (cases p)
  from hd_prog_prog_configs [of p sb] valid_sops_stmt [OF i_bound ts_i [simplified p]]
  valid_sops_stmt_sb [OF i_bound ts_i [simplified p]]
  show "(λ(s, t). valid_sops_stmt t s) (hd_prog p sb)"
    by (auto simp add: p)
next
  fix i ts p "is" 𝒪 ℛ 𝒟 θ sb p' is'
  assume i_bound: "i < length ts" 
    and ts_i: "ts ! i = (p, is, θ, sb, 𝒟, 𝒪,ℛ)" 
    and step: "θ⊢ p →s (p', is')"
    and valid: "valid_pimp ts"
  show "distinct_load_tmps is' ∧
          load_tmps is' ∩ load_tmps is = {} ∧
          load_tmps is' ∩ read_tmps sb = {}"
  proof -
    obtain s t where p: "p=(s,t)" by (cases p)
    obtain s' t' where p': "p'=(s',t')" by (cases p')
    note ts_i = ts_i [simplified p]
    note step = step [simplified p p']
    from valid 
    interpret separated_tmps ts
      by (simp add: valid_pimp_def)
     

    from sbh_step_distinct_load_tmps_prog_step [OF step load_tmps_le [OF i_bound ts_i]
      read_tmps_le [OF i_bound ts_i]]
    show ?thesis .
  qed
next
  fix i ts p "is" 𝒪 ℛ 𝒟 θ sb p' is'
  assume i_bound: "i < length ts" 
    and ts_i: "ts ! i = (p, is, θ, sb, 𝒟, 𝒪,ℛ)" 
    and step: "θ⊢ p →s (p', is')"
    and valid: "valid_pimp ts"
  show "data_dependency_consistent_instrs (dom θ ∪ load_tmps is) is' ∧
          load_tmps is' ∩ ⋃(fst ` store_sops is) = {} ∧
          load_tmps is' ∩ ⋃(fst ` write_sops sb) = {}"
  proof -
    obtain s t where p: "p=(s,t)" by (cases p)
    obtain s' t' where p': "p'=(s',t')" by (cases p')
    note ts_i = ts_i [simplified p]
    note step = step [simplified p p']
    from valid 
    interpret separated_tmps ts
      by (simp add: valid_pimp_def)

    from sbh_valid_data_dependency_prog_step [OF step store_sops_le [OF i_bound ts_i]
      write_sops_le [OF i_bound ts_i] valid_sops_stmt [OF i_bound ts_i]] tmps_le [OF i_bound ts_i]
    show ?thesis by auto
  qed
next
  fix i ts p "is" 𝒪 ℛ 𝒟 θ sb p' is'
  assume i_bound: "i < length ts" 
    and ts_i: "ts ! i = (p, is, θ, sb, 𝒟, 𝒪,ℛ)" 
    and step: "θ⊢ p →s (p', is')"
    and valid: "valid_pimp ts"
  show "load_tmps is' ∩ dom θ = {}"
  proof -
    obtain s t where p: "p=(s,t)" by (cases p)
    obtain s' t' where p': "p'=(s',t')" by (cases p')
    note ts_i = ts_i [simplified p]
    note step = step [simplified p p']
    from valid 
    interpret separated_tmps ts
      by (simp add: valid_pimp_def)  
    from sbh_load_tmps_fresh_prog_step [OF step tmps_le' [OF i_bound ts_i]]
    show ?thesis .
  qed
next
  fix θ p p' "is"
  assume  step: "θ⊢ p →s (p', is)"
    and valid: "(λ(s, t). valid_sops_stmt t s) p"
  show  "∀sop∈store_sops is. valid_sop sop"
  proof -
    obtain s t where p: "p=(s,t)" by (cases p)
    obtain s' t' where p': "p'=(s',t')" by (cases p')
    note step = step [simplified p p']
    from sbh_valid_sops_prog_step [OF step valid [simplified p,simplified]]
    show ?thesis .
  qed
next
  fix i ts p "is" 𝒪 ℛ 𝒟 θ sb p' is'
  assume i_bound: "i < length ts" 
    and ts_i: "ts ! i = (p, is, θ, sb::stmt_config store_buffer, 𝒟, 𝒪,ℛ)" 
    and step: "θ⊢ p →s (p', is')"
    and valid: "valid_pimp ts"
  from prog_step_preserves_valid [OF i_bound ts_i step valid]
  show "valid_pimp (ts[i := (p', is @ is', θ, sb @ [Progsb p p' is'], 𝒟, 𝒪,ℛ)])" .
next
  fix i ts p "is" 𝒪 ℛ 𝒟 θ sb  𝒮 m m' sb' 𝒪' ℛ' 𝒮'
  assume i_bound: "i < length ts" 
    and ts_i: "ts ! i = (p, is, θ, sb::stmt_config store_buffer, 𝒟, 𝒪,ℛ)" 
    and step: "(m, sb, 𝒪, ℛ,𝒮) →f (m', sb',𝒪',ℛ',𝒮')"
    and valid: "valid_pimp ts"
  thm flush_step_preserves_valid [OF ]
  from flush_step_preserves_valid [OF i_bound ts_i step valid]
  show "valid_pimp (ts[i := (p, is, θ, sb', 𝒟, 𝒪',ℛ')])" .
next
  fix i ts p "is" 𝒪 ℛ 𝒟 θ sb 𝒮 m is' 𝒪' ℛ' 𝒟' θ' sb' 𝒮' m'
  assume i_bound: "i < length ts" 
    and ts_i: "ts ! i = (p, is, θ, sb::stmt_config store_buffer, 𝒟, 𝒪,ℛ)"
    and step: "(is, θ, sb, m, 𝒟, 𝒪, ℛ, 𝒮) →sbh 
                  (is', θ', sb', m',𝒟', 𝒪', ℛ',𝒮')"
    and valid: "valid_pimp ts"
  from sbh_step_preserves_valid [OF i_bound ts_i step valid]
  show "valid_pimp (ts[i := (p, is', θ', sb', 𝒟', 𝒪',ℛ')])" .
qed

thm PIMP.concurrent_direct_steps_simulates_store_buffer_history_step
thm PIMP.concurrent_direct_steps_simulates_store_buffer_history_steps
thm PIMP.concurrent_direct_steps_simulates_store_buffer_step

text ‹We can instantiate PIMP with the various memory models.›

(* FIXME: note I used () instead of sb , because simplifier rewrites sb::unit to sb.
  Make this consistent with interpretations/theorems in ReduceStoreBuffer *)
interpretation direct: 
  computation direct_memop_step empty_storebuffer_step stmt_step "λp p' is sb. ()".
interpretation virtual: 
  computation virtual_memop_step empty_storebuffer_step stmt_step "λp p' is sb. ()".
interpretation store_buffer:
  computation sb_memop_step store_buffer_step stmt_step "λp p' is sb. sb" .
interpretation store_buffer_history:
  computation sbh_memop_step flush_step stmt_step "λp p' is sb. sb @ [Progsb p p' is]".

abbreviation direct_pimp_step:: 
  "(stmt_config,unit,bool,owns,rels,shared) global_config ⇒ (stmt_config,unit,bool,owns,rels,shared) global_config ⇒ bool" 
  ("_ ⇒dp _" [60,60] 100)
where
"c ⇒dp d ≡ direct.concurrent_step c d"

abbreviation direct_pimp_steps:: 
  "(stmt_config,unit,bool,owns,rels,shared) global_config ⇒ (stmt_config,unit,bool,owns,rels,shared) global_config ⇒ bool" 
  ("_ ⇒dp* _" [60,60] 100)
where
"direct_pimp_steps == direct_pimp_step^**"

text ‹Execution examples›



lemma Assign_Const_ex: 
"([((Assign True (Tmp ({},λθ. a)) (Const c) (λθ. A) (λθ. L) (λθ. R) (λθ. W),t),[],θ,(),𝒟,𝒪,ℛ)],m,𝒮) ⇒dp* 
 ([((Skip,t),[],θ,(),True,𝒪 ∪ A - R,Map.empty)],m(a := c),𝒮 ⊕⇘W⇙ R ⊖⇘A⇙ L)"
apply (rule converse_rtranclp_into_rtranclp)
apply  (rule direct.Program [where i=0])
apply    simp
apply   simp
apply  (rule Assign)
apply simp
apply (rule converse_rtranclp_into_rtranclp)
apply  (rule direct.Memop [where i=0])
apply    simp
apply   simp
apply  (rule direct_memop_step.WriteVolatile)
apply simp
done

lemma 
" ([((Assign True (Tmp ({},λθ. a)) (Binop (+) (Mem True x) (Mem True y)) (λθ. A) (λθ. L) (λθ. R) (λθ. W),t),[],θ,(),𝒟,𝒪,ℛ)],m,S) 
 ⇒dp* 
 ([((Skip,t + 2),[],θ(t↦m x, t + 1 ↦m y),(),True,𝒪 ∪ A - R,Map.empty)],m(a := m x + m y),S  ⊕⇘W⇙ R ⊖⇘A⇙ L)"
apply (rule converse_rtranclp_into_rtranclp)
apply  (rule direct.Program [where i=0])
apply    simp
apply   simp
apply  (rule Assign)
apply simp

apply (rule converse_rtranclp_into_rtranclp)
apply  (rule direct.Memop)
apply    simp
apply   simp
apply  (rule direct_memop_step.Read )
apply simp

apply (rule converse_rtranclp_into_rtranclp)
apply  (rule direct.Memop)
apply    simp
apply   simp
apply  (rule direct_memop_step.Read)
apply simp

apply (rule converse_rtranclp_into_rtranclp)
apply  (rule direct.Memop)
apply    simp
apply   simp
apply  (rule direct_memop_step.WriteVolatile )
apply simp
done


lemma  
assumes isTrue: "isTrue c"
shows  
"([((Cond (Const c) (Assign True (Tmp ({},λθ. a)) (Const c) (λθ. A) (λθ. L) (λθ. R) (λθ. W)) Skip,t) ,[],θ,(),𝒟,𝒪,ℛ)],m,𝒮) ⇒dp* 
 ([((Skip,t),[],θ,(),True,𝒪 ∪ A - R,Map.empty)],m(a := c),𝒮  ⊕⇘W⇙ R ⊖⇘A⇙ L)"
apply (rule converse_rtranclp_into_rtranclp)
apply  (rule direct.Program [where i=0])
apply    simp
apply   simp
apply  (rule Cond)
apply  simp
apply simp

apply (rule converse_rtranclp_into_rtranclp)
apply  (rule direct.Program [where i=0])
apply    simp
apply   simp
apply  (rule CondTrue)
apply   simp
apply  (simp add: isTrue)
apply simp

apply (rule Assign_Const_ex)
done


end