Theory Concrete

(*<*)
(*
 * Copyright 2015, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(NICTA_BSD)
 *)

theory Concrete
imports
  Concrete_heap
begin

(*>*)
text‹›

context gc_system
begin

abbreviation sys_init_state :: concrete_local_state where
  "sys_init_state ≡
     undefined⦇ fA := initial_mark
              , fM := initial_mark
              , heap := sys_init_heap
              , hs_pending := ⟨False⟩
              , hs_type := ht_GetRoots
              , mem_lock := None
              , mem_store_buffers := ⟨[]⟩
              , phase := ph_Idle
              , W := {}
              , ghost_honorary_grey := {}
              , ghost_hs_in_sync := ⟨True⟩
              , ghost_hs_phase := hp_IdleMarkSweep ⦈"

abbreviation gc_init_state :: concrete_local_state where
  "gc_init_state ≡
     undefined⦇ fM := initial_mark
              , fA := initial_mark
              , phase := ph_Idle
              , W := {}
              , ghost_honorary_grey := {} ⦈"

primrec lookup :: "('k × 'v) list ⇒ 'v ⇒ 'k ⇒ 'v" where
  "lookup [] v0 k = v0"
| "lookup (kv # kvs) v0 k = (if fst kv = k then snd kv else lookup kvs v0 k)"

abbreviation muts_init_states :: "(mut × concrete_local_state) list" where
  "muts_init_states ≡ [ (0, mut_init_state0), (1, mut_init_state1), (2, mut_init_state2) ]"

abbreviation init_state :: clsts where
  "init_state ≡ λp. case p of
              gc ⇒ gc_init_state
            | sys ⇒ sys_init_state
            | mutator m ⇒ lookup muts_init_states mut_common_init_state m"

lemma
  "gc_system_init init_state"
(*<*)
unfolding gc_system_init_def gc_initial_state_def mut_initial_state_def sys_initial_state_def
apply (clarsimp; intro conjI)
 apply (auto simp: ran_def; fail)
unfolding valid_refs_def reaches_def
apply auto
apply (erule rtranclp.cases; auto simp: ran_def split: if_splits obj_at_splits)+
done
(*>*)
text‹›

end
(*<*)

end
(*>*)