Theory SC_Collections

(*  Title:      JinjaThreads/MM/SC_Collections.thy
    Author:     Andreas Lochbihler
*)

section ‹Sequential consistency with efficient data structures›

theory SC_Collections
imports
  "../Common/Conform"
  (*"../../Collections/impl/RBTMapImpl"
  "../../Collections/impl/TrieMapImpl"
  "../../Collections/impl/ListMapImpl"*)
  "../Basic/JT_ICF"
  MM
begin

hide_const (open) new_Addr
hide_fact (open) new_Addr_SomeD new_Addr_SomeI

subsection‹Objects and Arrays›

type_synonym fields = "(char, (cname, addr val) lm) tm"
type_synonym array_cells = "(nat, addr val) rbt"
type_synonym array_fields = "(vname, addr val) lm"

datatype heapobj
  = Obj cname fields                    ― ‹class instance with class name and fields›
  | Arr ty nat array_fields array_cells                 ― ‹element type, size, fields and cell contents›

lemma rec_heapobj [simp]: "rec_heapobj = case_heapobj"
by(auto intro!: ext split: heapobj.split)

primrec obj_ty  :: "heapobj  htype"
where
  "obj_ty (Obj c f)   = Class_type c"
| "obj_ty (Arr t si f e) = Array_type t si"

fun is_Arr :: "heapobj  bool" where
  "is_Arr (Obj C fs)      = False"
| "is_Arr (Arr T f si el) = True"

lemma is_Arr_conv:
  "is_Arr arrobj = (T si f el. arrobj = Arr T si f el)"
by(cases arrobj, auto)

lemma is_ArrE:
  " is_Arr arrobj; T si f el. arrobj = Arr T si f el  thesis   thesis"
  " ¬ is_Arr arrobj; C fs. arrobj = Obj C fs  thesis   thesis"
by(cases arrobj, auto)+

definition init_fields :: "((vname × cname) × ty) list  fields"
where
  "init_fields FDTs 
  foldr (λ((F, D), T) fields. 
           let F' = String.explode F
           in tm_update F' (lm_update D (default_val T)
                                      (case tm_lookup F' fields of None  lm_empty () | Some lm  lm)) fields)
        FDTs (tm_empty ())"

definition init_fields_array :: "(vname × ty) list  array_fields"
where
  "init_fields_array  lm.to_map  map (λ(F, T). (F, default_val T))"

definition init_cells :: "ty  nat  array_cells"
where "init_cells T n = foldl (λcells i. rm_update i (default_val T) cells) (rm_empty ()) [0..<n]"

primrec ― ‹a new, blank object with default values in all fields:›
  blank :: "'m prog  htype  heapobj"
where
  "blank P (Class_type C) = Obj C (init_fields (map (λ(FD, (T, fm)). (FD, T)) (TypeRel.fields P C)))"
| "blank P (Array_type T n) =
   Arr T n (init_fields_array (map (λ((F, D), (T, fm)). (F, T)) (TypeRel.fields P Object))) (init_cells T n)"

lemma obj_ty_blank [iff]: "obj_ty (blank P hT) = hT"
by(cases hT) simp_all

subsection‹Heap›

type_synonym heap = "(addr, heapobj) rbt"

translations
  (type) "heap" <= (type) "(nat, heapobj) rbt"

abbreviation sc_empty :: heap
where "sc_empty  rm_empty ()"

fun the_obj :: "heapobj  cname × fields" where
  "the_obj (Obj C fs) = (C, fs)"

fun the_arr :: "heapobj  ty × nat × array_fields × array_cells" where
  "the_arr (Arr T si f el) = (T, si, f, el)"

abbreviation
  cname_of :: "heap  addr  cname" where
  "cname_of hp a == fst (the_obj (the (rm_lookup a hp)))"

definition new_Addr :: "heap  addr option"
where "new_Addr h = Some (case rm_max h (λ_. True) of None  0 | Some (a, _)  a + 1)"

definition sc_allocate :: "'m prog  heap  htype  (heap × addr) set"
where
  "sc_allocate P h hT = 
   (case new_Addr h of None  {}
                   | Some a  {(rm_update a (blank P hT) h, a)})"

definition sc_typeof_addr :: "heap  addr  htype option"
where "sc_typeof_addr h a = map_option obj_ty (rm_lookup a h)"

inductive sc_heap_read :: "heap  addr  addr_loc  addr val  bool"
for h :: heap and a :: addr
where
  Obj: " rm_lookup a h = Obj C fs; tm_lookup (String.explode F) fs = fs'; lm_lookup D fs' = v   sc_heap_read h a (CField D F) v"
| Arr: " rm_lookup a h = Arr T si f el; n < si   sc_heap_read h a (ACell n) (the (rm_lookup n el))"
| ArrObj: " rm_lookup a h = Arr T si f el; lm_lookup F f = v   sc_heap_read h a (CField Object F) v"

hide_fact (open) Obj Arr ArrObj

inductive_cases sc_heap_read_cases [elim!]:
  "sc_heap_read h a (CField C F) v"
  "sc_heap_read h a (ACell n) v"

inductive sc_heap_write :: "heap  addr  addr_loc  addr val  heap  bool"
for h :: heap and a :: addr
where
  Obj:
  " rm_lookup a h = Obj C fs; F' = String.explode F;
     h' = rm_update a (Obj C (tm_update F' (lm_update D v (case tm_lookup (String.explode F) fs of None  lm_empty () | Some fs'  fs')) fs)) h 
   sc_heap_write h a (CField D F) v h'"

| Arr:
  " rm_lookup a h = Arr T si f el; h' = rm_update a (Arr T si f (rm_update n v el)) h 
   sc_heap_write h a (ACell n) v h'"

| ArrObj:
  " rm_lookup a h = Arr T si f el; h' = rm_update a (Arr T si (lm_update F v f) el) h 
   sc_heap_write h a (CField Object F) v h'"

hide_fact (open) Obj Arr ArrObj

inductive_cases sc_heap_write_cases [elim!]:
  "sc_heap_write h a (CField C F) v h'"
  "sc_heap_write h a (ACell n) v h'"

consts sc_spurious_wakeups :: bool

lemma new_Addr_SomeD: "new_Addr h = a  rm_lookup a h = None"
apply(simp add: new_Addr_def)
apply(drule rm.max_None[OF rm.invar])
apply(simp add: rm.lookup_correct rel_of_def)
apply(clarsimp simp add: rm.lookup_correct)
apply(frule rm.max_Some[OF rm.invar])
apply(clarsimp simp add: rel_of_def)
apply(hypsubst_thin)
apply(rule ccontr)
apply(clarsimp)
apply(drule_tac k'="Suc a" in rm.max_Some(2)[OF rm.invar])
apply(auto simp add: rel_of_def)
done

interpretation sc: 
  heap_base
    "addr2thread_id"
    "thread_id2addr"
    "sc_spurious_wakeups"
    "sc_empty"
    "sc_allocate P"
    "sc_typeof_addr"
    "sc_heap_read"
    "sc_heap_write"
  for P . 

text ‹Translate notation from heap_base›

abbreviation sc_preallocated :: "'m prog  heap  bool"
where "sc_preallocated == sc.preallocated TYPE('m)"

abbreviation sc_start_tid :: "'md prog  thread_id"
where "sc_start_tid  sc.start_tid TYPE('md)"

abbreviation sc_start_heap_ok :: "'m prog  bool"
where "sc_start_heap_ok  sc.start_heap_ok TYPE('m)"

abbreviation sc_start_heap :: "'m prog  heap"
where "sc_start_heap  sc.start_heap TYPE('m)"

abbreviation sc_start_state :: 
  "(cname  mname  ty list  ty  'm  addr val list  'x)
   'm prog  cname  mname  addr val list  (addr, thread_id, 'x, heap, addr) state"
where
  "sc_start_state f P  sc.start_state TYPE('m) P f P"

abbreviation sc_wf_start_state :: "'m prog  cname  mname  addr val list  bool"
where "sc_wf_start_state P  sc.wf_start_state TYPE('m) P P"

notation sc.conf ("_,_ ⊢sc _ :≤ _"  [51,51,51,51] 50)
notation sc.confs ("_,_ ⊢sc _ [:≤] _" [51,51,51,51] 50)
notation sc.hext ("_ ⊴sc _" [51,51] 50)

lemma new_Addr_SomeI: "a. new_Addr h = Some a"
by(simp add: new_Addr_def)

lemma sc_start_heap_ok: "sc_start_heap_ok P"
by(simp add: sc.start_heap_ok_def sc.start_heap_data_def initialization_list_def sc.create_initial_object_simps sc_allocate_def case_option_conv_if new_Addr_SomeI sys_xcpts_list_def del: blank.simps split del: option.split if_split)

lemma sc_wf_start_state_iff:
  "sc_wf_start_state P C M vs  (Ts T meth D. P  C sees M:TsT = meth in D  P,sc_start_heap P ⊢sc vs [:≤] Ts)"
by(simp add: sc.wf_start_state.simps sc_start_heap_ok)

lemma sc_heap:
  "heap addr2thread_id thread_id2addr (sc_allocate P) sc_typeof_addr sc_heap_write P"
proof
  fix h' a h hT
  assume "(h', a)  sc_allocate P h hT"
  thus "sc_typeof_addr h' a = hT"
    by(auto simp add: sc_allocate_def sc_typeof_addr_def rm.lookup_correct rm.update_correct dest: new_Addr_SomeD split: if_split_asm)
next
  fix h h' hT a
  assume "(h', a)  sc_allocate P h hT"
  from this[symmetric] show "h ⊴sc h'"
    by(fastforce simp add: sc_allocate_def sc_typeof_addr_def sc.hext_def rm.lookup_correct rm.update_correct intro!: map_leI dest: new_Addr_SomeD)
next
  fix h a al v h'
  assume "sc_heap_write h a al v h'"
  thus "h ⊴sc h'"
    by(cases al)(auto intro!: sc.hextI simp add: sc_typeof_addr_def rm.lookup_correct rm.update_correct)
qed simp

interpretation sc: 
  heap 
    "addr2thread_id"
    "thread_id2addr"
    "sc_spurious_wakeups"
    "sc_empty"
    "sc_allocate P"
    "sc_typeof_addr"
    "sc_heap_read"
    "sc_heap_write"
    P
  for P by(rule sc_heap)

declare sc.typeof_addr_thread_id2_addr_addr2thread_id [simp del]

lemma sc_hext_new:
  "rm_lookup a h = None  h ⊴sc rm_update a arrobj h"
by(rule sc.hextI)(auto simp add: sc_typeof_addr_def rm.lookup_correct rm.update_correct dest!: new_Addr_SomeD)

lemma sc_hext_upd_obj: "rm_lookup a h = Some (Obj C fs)  h ⊴sc rm_update a (Obj C fs') h"
by(rule sc.hextI)(auto simp:fun_upd_apply sc_typeof_addr_def rm.lookup_correct rm.update_correct)

lemma sc_hext_upd_arr: " rm_lookup a h = Some (Arr T si f e)   h ⊴sc rm_update a (Arr T si f' e') h"
by(rule sc.hextI)(auto simp:fun_upd_apply sc_typeof_addr_def rm.lookup_correct rm.update_correct)

subsection ‹Conformance›

definition sc_oconf :: "'m prog  heap  heapobj  bool"   ("_,_ ⊢sc _ " [51,51,51] 50)
where
  "P,h ⊢sc obj   
   (case obj of 
     Obj C fs  
        is_class P C  
        (F D T fm. P  C has F:T (fm) in D  
           (fs' v. tm_α fs (String.explode F) = Some fs'  lm_α fs' D = Some v  P,h ⊢sc v :≤ T))
   | Arr T si f el  
      is_type P (T⌊⌉)  (n. n < si  (v. rm_α el n = Some v  P,h ⊢sc v :≤ T)) 
      (F T fm. P  Object has F:T (fm) in Object  (v. lm_lookup F f = Some v  P,h ⊢sc v :≤ T)))"

definition sc_hconf :: "'m prog  heap  bool"  ("_ ⊢sc _ " [51,51] 50)
where "P ⊢sc h   (a obj. rm_α h a = Some obj  P,h ⊢sc obj )"

interpretation sc: 
  heap_conf_base  
    "addr2thread_id"
    "thread_id2addr"
    "sc_spurious_wakeups"
    "sc_empty"
    "sc_allocate P"
    "sc_typeof_addr"
    "sc_heap_read"
    "sc_heap_write"
    "sc_hconf P"
    "P"
  for P 
.

lemma sc_conf_upd_obj: "rm_lookup a h = Some(Obj C fs)  (P,rm_update a (Obj C fs') h ⊢sc x :≤ T) = (P,h ⊢sc x :≤ T)"
apply (unfold sc.conf_def)
apply (rule val.induct)
apply (auto simp:fun_upd_apply)
apply (auto simp add: sc_typeof_addr_def rm.lookup_correct rm.update_correct split: if_split_asm)
done

lemma sc_conf_upd_arr:
  "rm_lookup a h = Some(Arr T si f el)  (P,rm_update a (Arr T si f' el') h ⊢sc x :≤ T') = (P,h ⊢sc x :≤ T')"
apply(unfold sc.conf_def)
apply (rule val.induct)
apply (auto simp:fun_upd_apply)
apply(auto simp add: sc_typeof_addr_def rm.lookup_correct rm.update_correct split: if_split_asm)
done

lemma sc_oconf_hext: "P,h ⊢sc obj   h ⊴sc h'  P,h' ⊢sc obj "
unfolding sc_oconf_def
by(fastforce split: heapobj.split elim: sc.conf_hext)

lemma map_of_fields_init_fields:
  assumes "map_of FDTs (F, D) = (T, fm)"
  shows "fs' v. tm_α (init_fields (map (λ(FD, (T, fm)). (FD, T)) FDTs)) (String.explode F) = fs'  lm_α fs' D = v  sc.conf P h v T"
using assms
  by(induct FDTs)(auto simp add: tm.lookup_correct tm.update_correct lm.update_correct init_fields_def String.explode_inject)

lemma sc_oconf_init_fields:
  assumes "P  C has_fields FDTs"
  shows "P,h ⊢sc (Obj C (init_fields (map (λ(FD, (T, fm)). (FD, T)) FDTs))) "
using assms has_fields_is_class[OF assms] map_of_fields_init_fields[of FDTs]
by(fastforce simp add: has_field_def sc_oconf_def dest: has_fields_fun)

lemma sc_oconf_init_arr:
  assumes type: "is_type P (T⌊⌉)"
  shows "P,h ⊢sc Arr T n (init_fields_array (map (λ((F, D), (T, fm)). (F, T)) (TypeRel.fields P Object))) (init_cells T n) "
proof -
  { fix n'
    assume "n' < n"
    { fix rm and k :: nat
      assume "i<k. v. rm_α rm i = v  sc.conf P h v T"
      with n' < n have "v. rm_α (foldl (λcells i. rm_update i (default_val T) cells) rm [k..<n]) n' = v  sc.conf P h v T"
        by(induct m"n-k" arbitrary: n k rm)(auto simp add: rm.update_correct upt_conv_Cons type)
    }
    from this[of 0 "rm_empty ()"]
    have "v. rm_α (foldl (λcells i. rm_update i (default_val T) cells) (rm_empty ()) [0..<n]) n' = v  sc.conf P h v T" by simp
  }
  moreover
  { fix F T fm
    assume "P  Object has F:T (fm) in Object"
    then obtain FDTs where has: "P  Object has_fields FDTs"
      and FDTs: "map_of FDTs (F, Object) = (T, fm)"
      by(auto simp add: has_field_def)
    from has have "snd ` fst ` set FDTs  {Object}" by(rule Object_has_fields_Object)
    with FDTs have "map_of (map ((λ(F, T). (F, default_val T))  (λ((F, D), T, fm). (F, T))) FDTs) F = default_val T"
      by(induct FDTs) auto
    with has FDTs
    have "v. lm_lookup F (init_fields_array (map (λ((F, D), T, fm). (F, T)) (TypeRel.fields P Object))) = v 
              sc.conf P h v T"
      by(auto simp add: init_fields_array_def lm_correct has_field_def)
  }
  ultimately show ?thesis using type by(auto simp add: sc_oconf_def init_cells_def)
qed

lemma sc_oconf_fupd [intro?]:
  " P  C has F:T (fm) in D; P,h ⊢sc v :≤ T; P,h ⊢sc (Obj C fs) ;
    fs' = (case tm_lookup (String.explode F) fs of None  lm_empty () | Some fs'  fs') 
   P,h ⊢sc (Obj C (tm_update (String.explode F) (lm_update D v fs') fs)) "
unfolding sc_oconf_def has_field_def
apply(auto dest: has_fields_fun simp add: lm.update_correct tm.update_correct tm.lookup_correct String.explode_inject)
apply(drule (1) has_fields_fun, fastforce)
apply(drule (1) has_fields_fun, fastforce)
done

lemma sc_oconf_fupd_arr [intro?]:
  " P,h ⊢sc v :≤ T; P,h ⊢sc (Arr T si f el)  
   P,h ⊢sc (Arr T si f (rm_update i v el)) "
unfolding sc_oconf_def
by(auto simp add: rm.update_correct)

lemma sc_oconf_fupd_arr_fields:
  " P  Object has F:T (fm) in Object; P,h ⊢sc v :≤ T; P,h ⊢sc (Arr T' si f el)  
   P,h ⊢sc (Arr T' si (lm_update F v f) el) "
unfolding sc_oconf_def by(auto dest: has_field_fun simp add: lm_correct)

lemma sc_oconf_new: " P,h ⊢sc obj ; rm_lookup a h = None   P,rm_update a arrobj h ⊢sc obj "
by(erule sc_oconf_hext)(rule sc_hext_new)

lemmas sc_oconf_upd_obj = sc_oconf_hext [OF _ sc_hext_upd_obj]

lemma sc_oconf_upd_arr:
  assumes "P,h ⊢sc obj "
  and ha: "rm_lookup a h = Arr T si f el"
  shows "P,rm_update a (Arr T si f' el') h ⊢sc obj "
using assms
by(fastforce simp add: sc_oconf_def sc_conf_upd_arr[OF ha] split: heapobj.split)

lemma sc_oconf_blank: "is_htype P hT  P,h ⊢sc blank P hT "
apply(cases hT)
 apply(fastforce dest: map_of_fields_init_fields simp add: has_field_def sc_oconf_def)
by(auto intro: sc_oconf_init_arr)

lemma sc_hconfD: " P ⊢sc h ; rm_lookup a h = Some obj   P,h ⊢sc obj "
unfolding sc_hconf_def by(auto simp add: rm.lookup_correct)

lemmas sc_preallocated_new = sc.preallocated_hext[OF _ sc_hext_new]
lemmas sc_preallocated_upd_obj = sc.preallocated_hext [OF _ sc_hext_upd_obj]
lemmas sc_preallocated_upd_arr = sc.preallocated_hext [OF _ sc_hext_upd_arr]

lemma sc_hconf_new: " P ⊢sc h ; rm_lookup a h = None; P,h ⊢sc obj    P ⊢sc rm_update a obj h "
unfolding sc_hconf_def
by(auto intro: sc_oconf_new simp add: rm.lookup_correct rm.update_correct)

lemma sc_hconf_upd_obj: " P ⊢sc h ; rm_lookup a h = Some (Obj C fs); P,h ⊢sc (Obj C fs')    P ⊢sc rm_update a (Obj C fs') h "
unfolding sc_hconf_def
by(auto intro: sc_oconf_upd_obj simp add: rm.lookup_correct rm.update_correct)

lemma sc_hconf_upd_arr: " P ⊢sc h ; rm_lookup a h = Some(Arr T si f el); P,h ⊢sc (Arr T si f' el')    P ⊢sc rm_update a (Arr T si f' el') h "
unfolding sc_hconf_def
by(auto intro: sc_oconf_upd_arr simp add: rm.lookup_correct rm.update_correct)

lemma sc_heap_conf: 
  "heap_conf addr2thread_id thread_id2addr sc_empty (sc_allocate P) sc_typeof_addr sc_heap_write (sc_hconf P) P"
proof
  show "P ⊢sc sc_empty " by(simp add: sc_hconf_def rm.empty_correct)
next
  fix h a hT
  assume "sc_typeof_addr h a = hT" "P ⊢sc h "
  thus "is_htype P hT"
    by(auto simp add: sc_typeof_addr_def sc_oconf_def dest!: sc_hconfD split: heapobj.split_asm)
next
  fix h' hT h a
  assume "P ⊢sc h " "(h', a)  sc_allocate P h hT" "is_htype P hT"
  thus "P ⊢sc h' "
    by(auto simp add: sc_allocate_def dest!: new_Addr_SomeD intro: sc_hconf_new sc_oconf_blank split: if_split_asm)
next
  fix h a al T v h'
  assume "P ⊢sc h "
    and "sc.addr_loc_type P h a al T"
    and "P,h ⊢sc v :≤ T"
    and "sc_heap_write h a al v h'"
  thus "P ⊢sc h' "
    by(cases al)(fastforce elim!: sc.addr_loc_type.cases simp add: sc_typeof_addr_def intro: sc_hconf_upd_obj sc_oconf_fupd sc_hconfD sc_hconf_upd_arr sc_oconf_fupd_arr sc_oconf_fupd_arr_fields)+
qed

interpretation sc: 
  heap_conf
    "addr2thread_id"
    "thread_id2addr"
    "sc_spurious_wakeups"
    "sc_empty"
    "sc_allocate P"
    "sc_typeof_addr"
    "sc_heap_read"
    "sc_heap_write"
    "sc_hconf P"
    "P"
  for P 
by(rule sc_heap_conf)

lemma sc_heap_progress:
  "heap_progress addr2thread_id thread_id2addr sc_empty (sc_allocate P) sc_typeof_addr sc_heap_read sc_heap_write (sc_hconf P) P"
proof
  fix h a al T
  assume hconf: "P ⊢sc h "
    and alt: "sc.addr_loc_type P h a al T"
  from alt obtain arrobj where arrobj: "rm_lookup a h = arrobj"
    by(auto elim!: sc.addr_loc_type.cases simp add: sc_typeof_addr_def)
  from alt show "v. sc_heap_read h a al v  P,h ⊢sc v :≤ T"
  proof(cases)
    case (addr_loc_type_field U F fm D) 
    note [simp] = al = CField D F
    show ?thesis
    proof(cases "arrobj")
      case (Obj C' fs)
      with sc_typeof_addr h a = U arrobj
      have [simp]: "C' = class_type_of U" by(auto simp add: sc_typeof_addr_def)
      from hconf arrobj Obj have "P,h ⊢sc Obj (class_type_of U) fs " by(auto dest: sc_hconfD)
      with P  class_type_of U has F:T (fm) in D obtain fs' v 
      where "tm_lookup (String.explode F) fs = fs'" "lm_lookup D fs' = v" "P,h ⊢sc v :≤ T"
      by(fastforce simp add: sc_oconf_def tm.lookup_correct lm.lookup_correct)
      thus ?thesis using Obj arrobj by(auto intro: sc_heap_read.intros)
    next
      case (Arr T' si f el)
      with sc_typeof_addr h a = U arrobj
      have [simp]: "U = Array_type T' si" by(auto simp add: sc_typeof_addr_def)
      from hconf arrobj Arr have "P,h ⊢sc Arr T' si f el " by(auto dest: sc_hconfD)
      from P  class_type_of U has F:T (fm) in D have [simp]: "D = Object"
        by(auto dest: has_field_decl_above)
      with P,h ⊢sc Arr T' si f el  P  class_type_of U has F:T (fm) in D
      obtain v where "lm_lookup F f = v" "P,h ⊢sc v :≤ T"
        by(fastforce simp add: sc_oconf_def)
      thus ?thesis using Arr arrobj by(auto intro: sc_heap_read.intros)
    qed
  next
    case (addr_loc_type_cell n' n)
    with arrobj obtain si f el
      where [simp]: "arrobj = Arr T si f el"
      by(cases arrobj)(auto simp add: sc_typeof_addr_def)
    from addr_loc_type_cell arrobj
    have [simp]: "al = ACell n" and n: "n < si" by(auto simp add: sc_typeof_addr_def)
    from hconf arrobj have "P,h ⊢sc Arr T si f el " by(auto dest: sc_hconfD)
    with n obtain v where "rm_lookup n el = v" "P,h ⊢sc v :≤ T"
      by(fastforce simp add: sc_oconf_def rm.lookup_correct)
    thus ?thesis using arrobj n by(fastforce intro: sc_heap_read.intros)
  qed
next
  fix h a al T v
  assume alt: "sc.addr_loc_type P h a al T"
  from alt obtain arrobj where arrobj: "rm_lookup a h = arrobj"
    by(auto elim!: sc.addr_loc_type.cases simp add: sc_typeof_addr_def)
  thus "h'. sc_heap_write h a al v h'" using alt
    by(cases arrobj)(fastforce intro: sc_heap_write.intros elim!: sc.addr_loc_type.cases simp add: sc_typeof_addr_def dest: has_field_decl_above)+
qed

interpretation sc: 
  heap_progress
    "addr2thread_id"
    "thread_id2addr"
    "sc_spurious_wakeups"
    "sc_empty"
    "sc_allocate P"
    "sc_typeof_addr"
    "sc_heap_read"
    "sc_heap_write"
    "sc_hconf P"
    "P"
  for P
by(rule sc_heap_progress)

lemma sc_heap_conf_read:
  "heap_conf_read addr2thread_id thread_id2addr sc_empty (sc_allocate P) sc_typeof_addr sc_heap_read sc_heap_write (sc_hconf P) P"
proof
  fix h a al v T
  assume read: "sc_heap_read h a al v"
    and alt: "sc.addr_loc_type P h a al T"
    and hconf: "P ⊢sc h "
  thus "P,h ⊢sc v :≤ T"
    apply(auto elim!: sc_heap_read.cases sc.addr_loc_type.cases simp add: sc_typeof_addr_def)
    apply(fastforce dest!: sc_hconfD simp add: sc_oconf_def tm.lookup_correct lm.lookup_correct rm.lookup_correct)+
    done
qed

interpretation sc: 
  heap_conf_read
    "addr2thread_id"
    "thread_id2addr"
    "sc_spurious_wakeups"
    "sc_empty"
    "sc_allocate P"
    "sc_typeof_addr"
    "sc_heap_read"
    "sc_heap_write"
    "sc_hconf P"
    "P"
  for P
by(rule sc_heap_conf_read)

abbreviation sc_deterministic_heap_ops :: "'m prog  bool"
where "sc_deterministic_heap_ops  sc.deterministic_heap_ops TYPE('m)"

lemma sc_deterministic_heap_ops: "¬ sc_spurious_wakeups  sc_deterministic_heap_ops P"
by(rule sc.deterministic_heap_opsI)(auto elim: sc_heap_read.cases sc_heap_write.cases simp add: sc_allocate_def)

subsection ‹Code generation›

code_pred 
  (modes: i  i  i  i  bool, i  i  i  o  bool)
  sc_heap_read .

code_pred 
  (modes: i  i  i  i  i  bool, i  i  i  i  o  bool)
  sc_heap_write .

lemma eval_sc_heap_read_i_i_i_o:
  "Predicate.eval (sc_heap_read_i_i_i_o h ad al) = sc_heap_read h ad al"
by(auto elim: sc_heap_read_i_i_i_oE intro: sc_heap_read_i_i_i_oI intro!: ext)

lemma eval_sc_heap_write_i_i_i_i_o:
  "Predicate.eval (sc_heap_write_i_i_i_i_o h ad al v) = sc_heap_write h ad al v"
by(auto elim: sc_heap_write_i_i_i_i_oE intro: sc_heap_write_i_i_i_i_oI intro!: ext)

end