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:Ts→T = ⌊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