# Theory State_Refinement

Author:     Andreas Lochbihler
*)

chapter ‹Schedulers›

theory State_Refinement
imports

begin

type_synonym
('l,'t,'m,'m_t,'m_w,'s_i) state_refine = "('l,'t) locks × ('m_t × 'm) × 'm_w × 's_i"

locale state_refine_base =
fixes final :: "'x  bool"
and r :: "'t  ('x × 'm)  (('l,'t,'x,'m,'w,'o) thread_action × 'x × 'm) Predicate.pred"
and convert_RA :: "'l released_locks  'o list"
and thr_α :: "'m_t  ('l,'t,'x) thread_info"
and thr_invar :: "'m_t  bool"
and ws_α :: "'m_w  ('w,'t) wait_sets"
and ws_invar :: "'m_w  bool"
and is_α :: "'s_i  't interrupts"
and is_invar :: "'s_i  bool"
begin

fun state_α :: "('l,'t,'m,'m_t,'m_w, 's_i) state_refine  ('l,'t,'x,'m,'w) state"
where "state_α (ls, (ts, m), ws, is) = (ls, (thr_α ts, m), ws_α ws, is_α is)"

lemma state_α_conv [simp]:
"locks (state_α s) = locks s"
"thr (state_α s) = thr_α (thr s)"
"shr (state_α s) = shr s"
"wset (state_α s) = ws_α (wset s)"
"interrupts (state_α s) = is_α (interrupts s)"
by(case_tac [!] s) auto

inductive state_invar :: "('l,'t,'m,'m_t,'m_w,'s_i) state_refine  bool"
where " thr_invar ts; ws_invar ws; is_invar is   state_invar (ls, (ts, m), ws, is)"

inductive_simps state_invar_simps [simp]:
"state_invar (ls, (ts, m), ws, is)"

lemma state_invarD [simp]:
assumes "state_invar s"
shows "thr_invar (thr s)" "ws_invar (wset s)" "is_invar (interrupts s)"
using assms by(case_tac [!] s) auto

end

sublocale state_refine_base < α: final_thread final .
sublocale state_refine_base < α:
final
"λt xm ta x'm'. Predicate.eval (r t xm) (ta, x'm')"
.

definition (in heap_base) start_state_refine ::
(cname  mname  ty list  ty  'md  'addr val list  'x)  'md prog  cname  mname  'addr val list
where
"is_empty.
start_state_refine thr_empty thr_update ws_empty is_empty f P C M vs =
(let (D, Ts, T, m) = method P C M
in (K\$ None, (thr_update start_tid (f D M Ts T (the m) vs, no_wait_locks) thr_empty, start_heap), ws_empty, is_empty))"

definition Jinja_output ::