Theory FWState

(*  Title:      JinjaThreads/Framework/FWState.thy
    Author:     Andreas Lochbihler

chapter ‹The generic multithreaded semantics›

section ‹State of the multithreaded semantics›

theory FWState

datatype lock_action =
  | Unlock
  | UnlockFail
  | ReleaseAcquire

datatype ('t,'x,'m) new_thread_action =
    NewThread 't 'x 'm
  | ThreadExists 't bool

datatype 't conditional_action = 
    Join 't
  | Yield

datatype ('t, 'w) wait_set_action =
    Suspend 'w
  | Notify 'w
  | NotifyAll 'w
  | WakeUp 't
  | Notified
  | WokenUp

datatype 't interrupt_action 
  = IsInterrupted 't bool
  | Interrupt 't
  | ClearInterrupt 't

type_synonym 'l lock_actions = "'l ⇒f lock_action list"

  (type) "'l lock_actions" <= (type) "'l ⇒f lock_action list"

  ('l,'t,'x,'m,'w,'o) thread_action =
  "'l lock_actions × ('t,'x,'m) new_thread_action list ×
   't conditional_action list × ('t, 'w) wait_set_action list × 
   't interrupt_action list × 'o list"
(* pretty printing for thread_action type *)
print_translation let
    fun tr'
       [Const (@{type_syntax finfun}, _) $ l $
          (Const (@{type_syntax list}, _) $ Const (@{type_syntax lock_action}, _)),
        Const (@{type_syntax "prod"}, _) $
          (Const (@{type_syntax list}, _) $ (Const (@{type_syntax new_thread_action}, _) $ t1 $ x $ m)) $
          (Const (@{type_syntax "prod"}, _) $
            (Const (@{type_syntax list}, _) $ (Const (@{type_syntax conditional_action}, _) $ t2)) $
            (Const (@{type_syntax "prod"}, _) $
              (Const (@{type_syntax list}, _) $ (Const (@{type_syntax wait_set_action}, _) $ t3 $ w)) $ 
              (Const (@{type_syntax "prod"}, _) $
                 (Const (@{type_syntax "list"}, _) $ (Const (@{type_syntax "interrupt_action"}, _) $ t4)) $
                 (Const (@{type_syntax "list"}, _) $ o1))))] =
      if t1 = t2 andalso t2 = t3 andalso t3 = t4 then Syntax.const @{type_syntax thread_action} $ l $ t1 $ x $ m $ w $ o1
      else raise Match;
  in [(@{type_syntax "prod"}, K tr')]
typ "('l,'t,'x,'m,'w,'o) thread_action"
definition locks_a :: "('l,'t,'x,'m,'w,'o) thread_action  'l lock_actions" ("_l" [0] 1000) where
  "locks_a  fst"

definition thr_a :: "('l,'t,'x,'m,'w,'o) thread_action  ('t,'x,'m) new_thread_action list" ("_t" [0] 1000) where
  "thr_a  fst o snd"

definition cond_a :: "('l,'t,'x,'m,'w,'o) thread_action  't conditional_action list" ("_c" [0] 1000) where
  "cond_a = fst o snd o snd"

definition wset_a :: "('l,'t,'x,'m,'w,'o) thread_action  ('t, 'w) wait_set_action list" ("_w" [0] 1000) where
  "wset_a = fst o snd o snd o snd" 

definition interrupt_a :: "('l,'t,'x,'m,'w,'o) thread_action  't interrupt_action list" ("_i" [0] 1000) where
  "interrupt_a = fst o snd o snd o snd o snd"

definition obs_a :: "('l,'t,'x,'m,'w,'o) thread_action  'o list" ("_o" [0] 1000) where
  "obs_a  snd o snd o snd o snd o snd"

lemma locks_a_conv [simp]: "locks_a (ls, ntsjswss) = ls"
by(simp add:locks_a_def)

lemma thr_a_conv [simp]: "thr_a (ls, nts, jswss) = nts"
by(simp add: thr_a_def)

lemma cond_a_conv [simp]: "cond_a (ls, nts, js, wws) = js"
by(simp add: cond_a_def)

lemma wset_a_conv [simp]: "wset_a (ls, nts, js, wss, isobs) = wss"
by(simp add: wset_a_def)

lemma interrupt_a_conv [simp]: "interrupt_a (ls, nts, js, ws, is, obs) = is"
by(simp add: interrupt_a_def)

lemma obs_a_conv [simp]: "obs_a (ls, nts, js, wss, is, obs) = obs"
by(simp add: obs_a_def)

fun ta_update_locks :: "('l,'t,'x,'m,'w,'o) thread_action  lock_action  'l  ('l,'t,'x,'m,'w,'o) thread_action" where
  "ta_update_locks (ls, nts, js, wss, obs) lta l = (ls(l $:= ls $ l @ [lta]), nts, js, wss, obs)"

fun ta_update_NewThread :: "('l,'t,'x,'m,'w,'o) thread_action  ('t,'x,'m) new_thread_action  ('l,'t,'x,'m,'w,'o) thread_action" where
  "ta_update_NewThread (ls, nts, js, wss, is, obs) nt = (ls, nts @ [nt], js, wss, is, obs)"

fun ta_update_Conditional :: "('l,'t,'x,'m,'w,'o) thread_action  't conditional_action  ('l,'t,'x,'m,'w,'o) thread_action"
  "ta_update_Conditional (ls, nts, js, wss, is, obs) j = (ls, nts, js @ [j], wss, is, obs)"

fun ta_update_wait_set :: "('l,'t,'x,'m,'w,'o) thread_action  ('t, 'w) wait_set_action  ('l,'t,'x,'m,'w,'o) thread_action" where
  "ta_update_wait_set (ls, nts, js, wss, is, obs) ws = (ls, nts, js, wss @ [ws], is, obs)"

fun ta_update_interrupt :: "('l,'t,'x,'m,'w,'o) thread_action  't interrupt_action  ('l,'t,'x,'m,'w,'o) thread_action"
  "ta_update_interrupt (ls, nts, js, wss, is, obs) i = (ls, nts, js, wss, is @ [i], obs)"

fun ta_update_obs :: "('l,'t,'x,'m,'w,'o) thread_action  'o  ('l,'t,'x,'m,'w,'o) thread_action"
  "ta_update_obs (ls, nts, js, wss, is, obs) ob = (ls, nts, js, wss, is, obs @ [ob])"

abbreviation empty_ta :: "('l,'t,'x,'m,'w,'o) thread_action" where
  "empty_ta  (K$ [], [], [], [], [], [])"

notation (input) empty_ta ("ε")

text ‹
  Pretty syntax for specifying thread actions:
  Write ⦃ Lock→l, Unlock→l, Suspend w, Interrupt t⦄› instead of
  @{term "((K$ [])(l $:= [Lock, Unlock]), [], [Suspend w], [Interrupt t], [])"}.

  thread_action'› is a type that contains of all basic thread actions.
  Automatically coerce basic thread actions into that type and then dispatch to the right
  update function by pattern matching.
  For coercion, adhoc overloading replaces the generic injection inject_thread_action›
  by the specific ones, i.e. constructors.
  To avoid ambiguities with observable actions, the observable actions must be of sort obs_action›,
  which the basic thread action types are not.

class obs_action

datatype ('l,'t,'x,'m,'w,'o) thread_action' 
  = LockAction "lock_action × 'l"
  | NewThreadAction "('t,'x,'m) new_thread_action"
  | ConditionalAction "'t conditional_action"
  | WaitSetAction "('t, 'w) wait_set_action"
  | InterruptAction "'t interrupt_action"
  | ObsAction 'o

setup Sign.add_const_constraint (@{const_name ObsAction}, SOME @{typ "'o :: obs_action  ('l,'t,'x,'m,'w,'o) thread_action'"})

fun thread_action'_to_thread_action :: 
  "('l,'t,'x,'m,'w,'o :: obs_action) thread_action'  ('l,'t,'x,'m,'w,'o) thread_action  ('l,'t,'x,'m,'w,'o) thread_action"
  "thread_action'_to_thread_action (LockAction (la, l)) ta = ta_update_locks ta la l"
| "thread_action'_to_thread_action (NewThreadAction nt) ta = ta_update_NewThread ta nt"
| "thread_action'_to_thread_action (ConditionalAction ca) ta = ta_update_Conditional ta ca"
| "thread_action'_to_thread_action (WaitSetAction wa) ta = ta_update_wait_set ta wa"
| "thread_action'_to_thread_action (InterruptAction ia) ta = ta_update_interrupt ta ia"
| "thread_action'_to_thread_action (ObsAction ob) ta = ta_update_obs ta ob"

consts inject_thread_action :: "'a  ('l,'t,'x,'m,'w,'o) thread_action'"

nonterminal ta_let and ta_lets
  "_ta_snoc" :: "ta_lets  ta_let  ta_lets" ("_,/ _")
  "_ta_block" :: "ta_lets  'a" ("_" [0] 1000)
  "_ta_empty" :: "ta_lets" ("") 
  "_ta_single" :: "ta_let  ta_lets" ("_")
  "_ta_inject" :: "logic  ta_let" ("(_)")
  "_ta_lock" :: "logic  logic  ta_let" ("__")

  "_ta_block _ta_empty" == "CONST empty_ta"
  "_ta_block (_ta_single bta)" == "_ta_block (_ta_snoc _ta_empty bta)"
  "_ta_inject bta" == "CONST inject_thread_action bta"
  "_ta_lock la l" == "CONST inject_thread_action (CONST Pair la l)"
  "_ta_block (_ta_snoc btas bta)" == "CONST thread_action'_to_thread_action bta (_ta_block btas)"

  inject_thread_action NewThreadAction ConditionalAction WaitSetAction InterruptAction ObsAction LockAction

lemma ta_upd_proj_simps [simp]:
  shows ta_obs_proj_simps:
  "ta_update_obs ta obsl = tal" "ta_update_obs ta obst = tat" "ta_update_obs ta obsw = taw" 
  "ta_update_obs ta obsc = tac" "ta_update_obs ta obsi = tai" "ta_update_obs ta obso = tao @ [obs]"
  and ta_lock_proj_simps:
  "ta_update_locks ta x ll = (let ls = tal in ls(l $:= ls $ l @ [x]))"
  "ta_update_locks ta x lt = tat" "ta_update_locks ta x lw = taw" "ta_update_locks ta x lc = tac" 
  "ta_update_locks ta x li = tai" "ta_update_locks ta x lo = tao"
  and ta_thread_proj_simps:
  "ta_update_NewThread ta tl = tal" "ta_update_NewThread ta tt = tat @ [t]" "ta_update_NewThread ta tw = taw" 
  "ta_update_NewThread ta tc = tac" "ta_update_NewThread ta ti = tai" "ta_update_NewThread ta to = tao"
  and ta_wset_proj_simps:
  "ta_update_wait_set ta wl = tal" "ta_update_wait_set ta wt = tat" "ta_update_wait_set ta ww = taw @ [w]"
  "ta_update_wait_set ta wc = tac" "ta_update_wait_set ta wi = tai" "ta_update_wait_set ta wo = tao"
  and ta_cond_proj_simps:
  "ta_update_Conditional ta cl = tal" "ta_update_Conditional ta ct = tat" "ta_update_Conditional ta cw = taw"
  "ta_update_Conditional ta cc = tac @ [c]" "ta_update_Conditional ta ci = tai" "ta_update_Conditional ta co = tao"
  and ta_interrupt_proj_simps:
  "ta_update_interrupt ta il = tal" "ta_update_interrupt ta it = tat" "ta_update_interrupt ta ic = tac"
  "ta_update_interrupt ta iw = taw" "ta_update_interrupt ta ii = tai @ [i]" "ta_update_interrupt ta io = tao"
by(cases ta, simp)+

lemma thread_action'_to_thread_action_proj_simps [simp]:
  shows thread_action'_to_thread_action_proj_locks_simps:
  "thread_action'_to_thread_action (LockAction (la, l)) tal = ta_update_locks ta la ll"
  "thread_action'_to_thread_action (NewThreadAction nt) tal = ta_update_NewThread ta ntl"
  "thread_action'_to_thread_action (ConditionalAction ca) tal = ta_update_Conditional ta cal"
  "thread_action'_to_thread_action (WaitSetAction wa) tal = ta_update_wait_set ta wal"
  "thread_action'_to_thread_action (InterruptAction ia) tal = ta_update_interrupt ta ial"
  "thread_action'_to_thread_action (ObsAction ob) tal = ta_update_obs ta obl"
  and thread_action'_to_thread_action_proj_nt_simps:
  "thread_action'_to_thread_action (LockAction (la, l)) tat = ta_update_locks ta la lt"
  "thread_action'_to_thread_action (NewThreadAction nt) tat = ta_update_NewThread ta ntt"
  "thread_action'_to_thread_action (ConditionalAction ca) tat = ta_update_Conditional ta cat"
  "thread_action'_to_thread_action (WaitSetAction wa) tat = ta_update_wait_set ta wat"
  "thread_action'_to_thread_action (InterruptAction ia) tat = ta_update_interrupt ta iat"
  "thread_action'_to_thread_action (ObsAction ob) tat = ta_update_obs ta obt"
  and thread_action'_to_thread_action_proj_cond_simps:
  "thread_action'_to_thread_action (LockAction (la, l)) tac = ta_update_locks ta la lc"
  "thread_action'_to_thread_action (NewThreadAction nt) tac = ta_update_NewThread ta ntc"
  "thread_action'_to_thread_action (ConditionalAction ca) tac = ta_update_Conditional ta cac"
  "thread_action'_to_thread_action (WaitSetAction wa) tac = ta_update_wait_set ta wac"
  "thread_action'_to_thread_action (InterruptAction ia) tac = ta_update_interrupt ta iac"
  "thread_action'_to_thread_action (ObsAction ob) tac = ta_update_obs ta obc"
  and thread_action'_to_thread_action_proj_wset_simps:
  "thread_action'_to_thread_action (LockAction (la, l)) taw = ta_update_locks ta la lw"
  "thread_action'_to_thread_action (NewThreadAction nt) taw = ta_update_NewThread ta ntw"
  "thread_action'_to_thread_action (ConditionalAction ca) taw = ta_update_Conditional ta caw"
  "thread_action'_to_thread_action (WaitSetAction wa) taw = ta_update_wait_set ta waw"
  "thread_action'_to_thread_action (InterruptAction ia) taw = ta_update_interrupt ta iaw"
  "thread_action'_to_thread_action (ObsAction ob) taw = ta_update_obs ta obw"
  and thread_action'_to_thread_action_proj_interrupt_simps:
  "thread_action'_to_thread_action (LockAction (la, l)) tai = ta_update_locks ta la li"
  "thread_action'_to_thread_action (NewThreadAction nt) tai = ta_update_NewThread ta nti"
  "thread_action'_to_thread_action (ConditionalAction ca) tai = ta_update_Conditional ta cai"
  "thread_action'_to_thread_action (WaitSetAction wa) tai = ta_update_wait_set ta wai"
  "thread_action'_to_thread_action (InterruptAction ia) tai = ta_update_interrupt ta iai"
  "thread_action'_to_thread_action (ObsAction ob) tai = ta_update_obs ta obi"
  and thread_action'_to_thread_action_proj_obs_simps:
  "thread_action'_to_thread_action (LockAction (la, l)) tao = ta_update_locks ta la lo"
  "thread_action'_to_thread_action (NewThreadAction nt) tao = ta_update_NewThread ta nto"
  "thread_action'_to_thread_action (ConditionalAction ca) tao = ta_update_Conditional ta cao"
  "thread_action'_to_thread_action (WaitSetAction wa) tao = ta_update_wait_set ta wao"
  "thread_action'_to_thread_action (InterruptAction ia) tao = ta_update_interrupt ta iao"
  "thread_action'_to_thread_action (ObsAction ob) tao = ta_update_obs ta obo"

lemmas ta_upd_simps =
  ta_update_locks.simps ta_update_NewThread.simps ta_update_Conditional.simps
  ta_update_wait_set.simps ta_update_interrupt.simps ta_update_obs.simps

declare ta_upd_simps [simp del]

hide_const (open)
  LockAction NewThreadAction ConditionalAction WaitSetAction InterruptAction ObsAction
hide_type (open) thread_action'

datatype wake_up_status =
| WSWokenUp

datatype 'w wait_set_status =
  InWS 'w
| PostWS wake_up_status

type_synonym 't lock = "('t × nat) option"
type_synonym ('l,'t) locks = "'l ⇒f 't lock"
type_synonym 'l released_locks = "'l ⇒f nat"
type_synonym ('l,'t,'x) thread_info = "'t  ('x × 'l released_locks)"
type_synonym ('w,'t) wait_sets = "'t  'w wait_set_status"
type_synonym 't interrupts = "'t set"
type_synonym ('l,'t,'x,'m,'w) state = "('l,'t) locks × (('l,'t,'x) thread_info × 'm) × ('w,'t) wait_sets × 't interrupts"

  (type) "('l, 't) locks" <= (type) "'l ⇒f ('t × nat) option"
  (type) "('l, 't, 'x) thread_info" <= (type) "'t  ('x × ('l ⇒f nat))"

(* pretty printing for state type *)
print_translation let
    fun tr'
       [Const (@{type_syntax finfun}, _) $ l1 $
        (Const (@{type_syntax option}, _) $
          (Const (@{type_syntax "prod"}, _) $ t1 $ Const (@{type_syntax nat}, _))),
        Const (@{type_syntax "prod"}, _) $
          (Const (@{type_syntax "prod"}, _) $
            (Const (@{type_syntax fun}, _) $ t2 $
              (Const (@{type_syntax option}, _) $
                (Const (@{type_syntax "prod"}, _) $ x $
                  (Const (@{type_syntax finfun}, _) $ l2 $ Const (@{type_syntax nat}, _))))) $
            m) $
          (Const (@{type_syntax prod}, _) $
            (Const (@{type_syntax fun}, _) $ t3 $ 
              (Const (@{type_syntax option}, _) $ (Const (@{type_syntax wait_set_status}, _) $ w))) $
            (Const (@{type_syntax fun}, _) $ t4 $ (Const (@{type_syntax bool}, _))))] =
      if t1 = t2 andalso t1 = t3 andalso t1 = t4 andalso l1 = l2
      then Syntax.const @{type_syntax state} $ l1 $ t1 $ x $ m $ w
      else raise Match;
  in [(@{type_syntax "prod"}, K tr')]
typ "('l,'t,'x,'m,'w) state"

abbreviation no_wait_locks :: "'l ⇒f nat"
where "no_wait_locks  (K$ 0)"

lemma neq_no_wait_locks_conv:
  "ln. ln  no_wait_locks  (l. ln $ l > 0)"
by(auto simp add: expand_finfun_eq fun_eq_iff)

lemma neq_no_wait_locksE:
  fixes ln assumes "ln  no_wait_locks" obtains l where "ln $ l > 0"
using assms
by(auto simp add: neq_no_wait_locks_conv)

text ‹
  Use type variables for components instead of @{typ "('l,'t,'x,'m,'w) state"} in types for state projections
  to allow to reuse them for refined state implementations for code generation.

definition locks :: "('locks × ('thread_info × 'm) × 'wsets × 'interrupts)  'locks" where
  "locks lstsmws  fst lstsmws"

definition thr :: "('locks × ('thread_info × 'm) × 'wsets × 'interrupts)  'thread_info" where
  "thr lstsmws  fst (fst (snd lstsmws))"

definition shr :: "('locks × ('thread_info × 'm) × 'wsets × 'interrupts)  'm" where
  "shr lstsmws  snd (fst (snd lstsmws))"

definition wset :: "('locks × ('thread_info × 'm) × 'wsets × 'interrupts)  'wsets" where
  "wset lstsmws  fst (snd (snd lstsmws))"

definition interrupts :: "('locks × ('thread_info × 'm) × 'wsets × 'interrupts)  'interrupts" where
  "interrupts lstsmws  snd (snd (snd lstsmws))"

lemma locks_conv [simp]: "locks (ls, tsmws) = ls"
by(simp add: locks_def)

lemma thr_conv [simp]: "thr (ls, (ts, m), ws) = ts"
by(simp add: thr_def)

lemma shr_conv [simp]: "shr (ls, (ts, m), ws, is) = m"
by(simp add: shr_def)

lemma wset_conv [simp]: "wset (ls, (ts, m), ws, is) = ws"
by(simp add: wset_def)

lemma interrupts_conv [simp]: "interrupts (ls, (ts, m), ws, is) = is"
by(simp add: interrupts_def)

primrec convert_new_thread_action :: "('x  'x')  ('t,'x,'m) new_thread_action  ('t,'x','m) new_thread_action"
  "convert_new_thread_action f (NewThread t x m) = NewThread t (f x) m"
| "convert_new_thread_action f (ThreadExists t b) = ThreadExists t b"

lemma convert_new_thread_action_inv [simp]:
  "NewThread t x h = convert_new_thread_action f nta  (x'. nta = NewThread t x' h  x = f x')"
  "ThreadExists t b = convert_new_thread_action f nta  nta = ThreadExists t b"
  "convert_new_thread_action f nta = NewThread t x h  (x'. nta = NewThread t x' h  x = f x')"
  "convert_new_thread_action f nta = ThreadExists t b  nta = ThreadExists t b"
by(cases nta, auto)+

lemma convert_new_thread_action_eqI: 
  " t x m. nta = NewThread t x m  nta' = NewThread t (f x) m;
     t b. nta = ThreadExists t b  nta' = ThreadExists t b 
   convert_new_thread_action f nta = nta'"
apply(cases nta)
apply fastforce+

lemma convert_new_thread_action_compose [simp]:
  "convert_new_thread_action f (convert_new_thread_action g ta) = convert_new_thread_action (f o g) ta"
apply(cases ta)
apply(simp_all add: convert_new_thread_action_def)

lemma inj_convert_new_thread_action [simp]: 
  "inj (convert_new_thread_action f) = inj f"
apply(rule iffI)
 apply(rule injI)
 apply(drule_tac x="NewThread undefined x undefined" in injD)
 apply auto[2]
apply(rule injI)
apply(case_tac x)
apply(auto dest: injD)

lemma convert_new_thread_action_id:
  "convert_new_thread_action id = (id :: ('t, 'x, 'm) new_thread_action  ('t, 'x, 'm) new_thread_action)" (is ?thesis1)
  "convert_new_thread_action (λx. x) = (id :: ('t, 'x, 'm) new_thread_action  ('t, 'x, 'm) new_thread_action)" (is ?thesis2)
proof -
  show ?thesis1 by(rule ext)(case_tac x, simp_all)
  thus ?thesis2 by(simp add: id_def)

definition convert_extTA :: "('x  'x')  ('l,'t,'x,'m,'w,'o) thread_action  ('l,'t,'x','m,'w,'o) thread_action"
where "convert_extTA f ta = (tal, map (convert_new_thread_action f) tat, snd (snd ta))"

lemma convert_extTA_simps [simp]:
  "convert_extTA f ε = ε"
  "convert_extTA f tal = tal"
  "convert_extTA f tat = map (convert_new_thread_action f) tat"
  "convert_extTA f tac = tac"
  "convert_extTA f taw = taw"
  "convert_extTA f tai = tai"
  "convert_extTA f (las, tas, was, cas, is, obs) = (las, map (convert_new_thread_action f) tas, was, cas, is, obs)"
apply(simp_all add: convert_extTA_def)
apply(cases ta, simp)+

lemma convert_extTA_eq_conv:
  "convert_extTA f ta = ta' 
   tal = ta'l  tac = ta'c  taw = ta'w  tao = ta'o  tai = ta'i  length tat = length ta't  
   (n < length tat. convert_new_thread_action f (tat ! n) = ta't ! n)"
apply(cases ta, cases ta')
apply(auto simp add: convert_extTA_def map_eq_all_nth_conv)

lemma convert_extTA_compose [simp]:
  "convert_extTA f (convert_extTA g ta) = convert_extTA (f o g) ta"
by(simp add: convert_extTA_def)

lemma obs_a_convert_extTA [simp]: "obs_a (convert_extTA f ta) = obs_a ta"
by(cases ta) simp

text ‹Actions for thread start/finish›

datatype 'o action =
    NormalAction 'o
  | InitialThreadAction
  | ThreadFinishAction

instance action :: (type) obs_action
proof qed

definition convert_obs_initial :: "('l,'t,'x,'m,'w,'o) thread_action  ('l,'t,'x,'m,'w,'o action) thread_action"
  "convert_obs_initial ta = (tal, tat, tac, taw, tai, map NormalAction tao)"

lemma inj_NormalAction [simp]: "inj NormalAction"
by(rule injI) auto

lemma convert_obs_initial_inject [simp]:
  "convert_obs_initial ta = convert_obs_initial ta'  ta = ta'"
by(cases ta)(cases ta', auto simp add: convert_obs_initial_def)

lemma convert_obs_initial_empty_TA [simp]:
  "convert_obs_initial ε = ε"
by(simp add: convert_obs_initial_def)

lemma convert_obs_initial_eq_empty_TA [simp]:
  "convert_obs_initial ta = ε  ta = ε"
  "ε = convert_obs_initial ta  ta = ε"
by(case_tac [!] ta)(auto simp add: convert_obs_initial_def)

lemma convert_obs_initial_simps [simp]:
  "convert_obs_initial tao = map NormalAction tao"
  "convert_obs_initial tal = tal"
  "convert_obs_initial tat = tat"
  "convert_obs_initial tac = tac"
  "convert_obs_initial taw = taw"
  "convert_obs_initial tai = tai"
by(simp_all add: convert_obs_initial_def)

  ('l,'t,'x,'m,'w,'o) semantics =
    "'t  'x × 'm  ('l,'t,'x,'m,'w,'o) thread_action  'x × 'm  bool"

(* pretty printing for semantics *)
print_translation let
    fun tr'
        Const (@{type_syntax fun}, _) $
          (Const (@{type_syntax "prod"}, _) $ x1 $ m1) $
          (Const (@{type_syntax fun}, _) $
            (Const (@{type_syntax "prod"}, _) $
              (Const (@{type_syntax finfun}, _) $ l $
                (Const (@{type_syntax list}, _) $ Const (@{type_syntax lock_action}, _))) $
              (Const (@{type_syntax "prod"}, _) $
                (Const (@{type_syntax list}, _) $ (Const (@{type_syntax new_thread_action}, _) $ t1 $ x2 $ m2)) $
                (Const (@{type_syntax "prod"}, _) $
                  (Const (@{type_syntax list}, _) $ (Const (@{type_syntax conditional_action}, _) $ t2)) $
                  (Const (@{type_syntax "prod"}, _) $
                    (Const (@{type_syntax list}, _) $ (Const (@{type_syntax wait_set_action}, _) $ t3 $ w)) $ 
                    (Const (@{type_syntax prod}, _) $
                       (Const (@{type_syntax list}, _) $ (Const (@{type_syntax interrupt_action}, _) $ t5)) $
                       (Const (@{type_syntax list}, _) $ o1)))))) $
            (Const (@{type_syntax fun}, _) $ (Const (@{type_syntax "prod"}, _) $ x3 $ m3) $
              Const (@{type_syntax bool}, _)))] =
      if x1 = x2 andalso x1 = x3 andalso m1 = m2 andalso m1 = m3 
        andalso t1 = t2 andalso t2 = t3 andalso t3 = t4 andalso t4 = t5
      then Syntax.const @{type_syntax semantics} $ l $ t1 $ x1 $ m1 $ w $ o1
      else raise Match;
  in [(@{type_syntax fun}, K tr')]
typ "('l,'t,'x,'m,'w,'o) semantics"