Theory FWState

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

chapter ‹The generic multithreaded semantics›

section ‹State of the multithreaded semantics›

theory FWState
imports 
  "../Basic/Auxiliary"
begin

datatype lock_action =
    Lock
  | 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"

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

type_synonym
  ('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')]
  end
›
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"
where
  "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"
where
  "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"
where
  "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"
where
  "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
syntax
  "_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" (‹_→_›)

translations
  "_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)"


adhoc_overloading
  inject_thread_action ⇌ NewThreadAction ConditionalAction WaitSetAction InterruptAction ObsAction LockAction

lemma ta_upd_proj_simps [simp]:
  shows ta_obs_proj_simps:
  "⦃ta_update_obs ta obs⦄⇘l⇙ = ⦃ta⦄⇘l⇙" "⦃ta_update_obs ta obs⦄⇘t⇙ = ⦃ta⦄⇘t⇙" "⦃ta_update_obs ta obs⦄⇘w⇙ = ⦃ta⦄⇘w⇙" 
  "⦃ta_update_obs ta obs⦄⇘c⇙ = ⦃ta⦄⇘c⇙" "⦃ta_update_obs ta obs⦄⇘i⇙ = ⦃ta⦄⇘i⇙" "⦃ta_update_obs ta obs⦄⇘o⇙ = ⦃ta⦄⇘o⇙ @ [obs]"
  and ta_lock_proj_simps:
  "⦃ta_update_locks ta x l⦄⇘l⇙ = (let ls = ⦃ta⦄⇘l⇙ in ls(l $:= ls $ l @ [x]))"
  "⦃ta_update_locks ta x l⦄⇘t⇙ = ⦃ta⦄⇘t⇙" "⦃ta_update_locks ta x l⦄⇘w⇙ = ⦃ta⦄⇘w⇙" "⦃ta_update_locks ta x l⦄⇘c⇙ = ⦃ta⦄⇘c⇙" 
  "⦃ta_update_locks ta x l⦄⇘i⇙ = ⦃ta⦄⇘i⇙" "⦃ta_update_locks ta x l⦄⇘o⇙ = ⦃ta⦄⇘o⇙"
  and ta_thread_proj_simps:
  "⦃ta_update_NewThread ta t⦄⇘l⇙ = ⦃ta⦄⇘l⇙" "⦃ta_update_NewThread ta t⦄⇘t⇙ = ⦃ta⦄⇘t⇙ @ [t]" "⦃ta_update_NewThread ta t⦄⇘w⇙ = ⦃ta⦄⇘w⇙" 
  "⦃ta_update_NewThread ta t⦄⇘c⇙ = ⦃ta⦄⇘c⇙" "⦃ta_update_NewThread ta t⦄⇘i⇙ = ⦃ta⦄⇘i⇙" "⦃ta_update_NewThread ta t⦄⇘o⇙ = ⦃ta⦄⇘o⇙"
  and ta_wset_proj_simps:
  "⦃ta_update_wait_set ta w⦄⇘l⇙ = ⦃ta⦄⇘l⇙" "⦃ta_update_wait_set ta w⦄⇘t⇙ = ⦃ta⦄⇘t⇙" "⦃ta_update_wait_set ta w⦄⇘w⇙ = ⦃ta⦄⇘w⇙ @ [w]"
  "⦃ta_update_wait_set ta w⦄⇘c⇙ = ⦃ta⦄⇘c⇙" "⦃ta_update_wait_set ta w⦄⇘i⇙ = ⦃ta⦄⇘i⇙" "⦃ta_update_wait_set ta w⦄⇘o⇙ = ⦃ta⦄⇘o⇙"
  and ta_cond_proj_simps:
  "⦃ta_update_Conditional ta c⦄⇘l⇙ = ⦃ta⦄⇘l⇙" "⦃ta_update_Conditional ta c⦄⇘t⇙ = ⦃ta⦄⇘t⇙" "⦃ta_update_Conditional ta c⦄⇘w⇙ = ⦃ta⦄⇘w⇙"
  "⦃ta_update_Conditional ta c⦄⇘c⇙ = ⦃ta⦄⇘c⇙ @ [c]" "⦃ta_update_Conditional ta c⦄⇘i⇙ = ⦃ta⦄⇘i⇙" "⦃ta_update_Conditional ta c⦄⇘o⇙ = ⦃ta⦄⇘o⇙"
  and ta_interrupt_proj_simps:
  "⦃ta_update_interrupt ta i⦄⇘l⇙ = ⦃ta⦄⇘l⇙" "⦃ta_update_interrupt ta i⦄⇘t⇙ = ⦃ta⦄⇘t⇙" "⦃ta_update_interrupt ta i⦄⇘c⇙ = ⦃ta⦄⇘c⇙"
  "⦃ta_update_interrupt ta i⦄⇘w⇙ = ⦃ta⦄⇘w⇙" "⦃ta_update_interrupt ta i⦄⇘i⇙ = ⦃ta⦄⇘i⇙ @ [i]" "⦃ta_update_interrupt ta i⦄⇘o⇙ = ⦃ta⦄⇘o⇙"
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)) ta⦄⇘l⇙ = ⦃ta_update_locks ta la l⦄⇘l⇙"
  "⦃thread_action'_to_thread_action (NewThreadAction nt) ta⦄⇘l⇙ = ⦃ta_update_NewThread ta nt⦄⇘l⇙"
  "⦃thread_action'_to_thread_action (ConditionalAction ca) ta⦄⇘l⇙ = ⦃ta_update_Conditional ta ca⦄⇘l⇙"
  "⦃thread_action'_to_thread_action (WaitSetAction wa) ta⦄⇘l⇙ = ⦃ta_update_wait_set ta wa⦄⇘l⇙"
  "⦃thread_action'_to_thread_action (InterruptAction ia) ta⦄⇘l⇙ = ⦃ta_update_interrupt ta ia⦄⇘l⇙"
  "⦃thread_action'_to_thread_action (ObsAction ob) ta⦄⇘l⇙ = ⦃ta_update_obs ta ob⦄⇘l⇙"
  and thread_action'_to_thread_action_proj_nt_simps:
  "⦃thread_action'_to_thread_action (LockAction (la, l)) ta⦄⇘t⇙ = ⦃ta_update_locks ta la l⦄⇘t⇙"
  "⦃thread_action'_to_thread_action (NewThreadAction nt) ta⦄⇘t⇙ = ⦃ta_update_NewThread ta nt⦄⇘t⇙"
  "⦃thread_action'_to_thread_action (ConditionalAction ca) ta⦄⇘t⇙ = ⦃ta_update_Conditional ta ca⦄⇘t⇙"
  "⦃thread_action'_to_thread_action (WaitSetAction wa) ta⦄⇘t⇙ = ⦃ta_update_wait_set ta wa⦄⇘t⇙"
  "⦃thread_action'_to_thread_action (InterruptAction ia) ta⦄⇘t⇙ = ⦃ta_update_interrupt ta ia⦄⇘t⇙"
  "⦃thread_action'_to_thread_action (ObsAction ob) ta⦄⇘t⇙ = ⦃ta_update_obs ta ob⦄⇘t⇙"
  and thread_action'_to_thread_action_proj_cond_simps:
  "⦃thread_action'_to_thread_action (LockAction (la, l)) ta⦄⇘c⇙ = ⦃ta_update_locks ta la l⦄⇘c⇙"
  "⦃thread_action'_to_thread_action (NewThreadAction nt) ta⦄⇘c⇙ = ⦃ta_update_NewThread ta nt⦄⇘c⇙"
  "⦃thread_action'_to_thread_action (ConditionalAction ca) ta⦄⇘c⇙ = ⦃ta_update_Conditional ta ca⦄⇘c⇙"
  "⦃thread_action'_to_thread_action (WaitSetAction wa) ta⦄⇘c⇙ = ⦃ta_update_wait_set ta wa⦄⇘c⇙"
  "⦃thread_action'_to_thread_action (InterruptAction ia) ta⦄⇘c⇙ = ⦃ta_update_interrupt ta ia⦄⇘c⇙"
  "⦃thread_action'_to_thread_action (ObsAction ob) ta⦄⇘c⇙ = ⦃ta_update_obs ta ob⦄⇘c⇙"
  and thread_action'_to_thread_action_proj_wset_simps:
  "⦃thread_action'_to_thread_action (LockAction (la, l)) ta⦄⇘w⇙ = ⦃ta_update_locks ta la l⦄⇘w⇙"
  "⦃thread_action'_to_thread_action (NewThreadAction nt) ta⦄⇘w⇙ = ⦃ta_update_NewThread ta nt⦄⇘w⇙"
  "⦃thread_action'_to_thread_action (ConditionalAction ca) ta⦄⇘w⇙ = ⦃ta_update_Conditional ta ca⦄⇘w⇙"
  "⦃thread_action'_to_thread_action (WaitSetAction wa) ta⦄⇘w⇙ = ⦃ta_update_wait_set ta wa⦄⇘w⇙"
  "⦃thread_action'_to_thread_action (InterruptAction ia) ta⦄⇘w⇙ = ⦃ta_update_interrupt ta ia⦄⇘w⇙"
  "⦃thread_action'_to_thread_action (ObsAction ob) ta⦄⇘w⇙ = ⦃ta_update_obs ta ob⦄⇘w⇙"
  and thread_action'_to_thread_action_proj_interrupt_simps:
  "⦃thread_action'_to_thread_action (LockAction (la, l)) ta⦄⇘i⇙ = ⦃ta_update_locks ta la l⦄⇘i⇙"
  "⦃thread_action'_to_thread_action (NewThreadAction nt) ta⦄⇘i⇙ = ⦃ta_update_NewThread ta nt⦄⇘i⇙"
  "⦃thread_action'_to_thread_action (ConditionalAction ca) ta⦄⇘i⇙ = ⦃ta_update_Conditional ta ca⦄⇘i⇙"
  "⦃thread_action'_to_thread_action (WaitSetAction wa) ta⦄⇘i⇙ = ⦃ta_update_wait_set ta wa⦄⇘i⇙"
  "⦃thread_action'_to_thread_action (InterruptAction ia) ta⦄⇘i⇙ = ⦃ta_update_interrupt ta ia⦄⇘i⇙"
  "⦃thread_action'_to_thread_action (ObsAction ob) ta⦄⇘i⇙ = ⦃ta_update_obs ta ob⦄⇘i⇙"
  and thread_action'_to_thread_action_proj_obs_simps:
  "⦃thread_action'_to_thread_action (LockAction (la, l)) ta⦄⇘o⇙ = ⦃ta_update_locks ta la l⦄⇘o⇙"
  "⦃thread_action'_to_thread_action (NewThreadAction nt) ta⦄⇘o⇙ = ⦃ta_update_NewThread ta nt⦄⇘o⇙"
  "⦃thread_action'_to_thread_action (ConditionalAction ca) ta⦄⇘o⇙ = ⦃ta_update_Conditional ta ca⦄⇘o⇙"
  "⦃thread_action'_to_thread_action (WaitSetAction wa) ta⦄⇘o⇙ = ⦃ta_update_wait_set ta wa⦄⇘o⇙"
  "⦃thread_action'_to_thread_action (InterruptAction ia) ta⦄⇘o⇙ = ⦃ta_update_interrupt ta ia⦄⇘o⇙"
  "⦃thread_action'_to_thread_action (ObsAction ob) ta⦄⇘o⇙ = ⦃ta_update_obs ta ob⦄⇘o⇙"
by(simp_all)

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
  thread_action'_to_thread_action.simps

declare ta_upd_simps [simp del]

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

datatype wake_up_status =
  WSNotified
| 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"

translations
  (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')]
  end
›
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"
where
  "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+
done

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)
done

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)
done

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)
qed

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 = (⦃ta⦄⇘l⇙, map (convert_new_thread_action f) ⦃ta⦄⇘t⇙, snd (snd ta))"

lemma convert_extTA_simps [simp]:
  "convert_extTA f ε = ε"
  "⦃convert_extTA f ta⦄⇘l⇙ = ⦃ta⦄⇘l⇙"
  "⦃convert_extTA f ta⦄⇘t⇙ = map (convert_new_thread_action f) ⦃ta⦄⇘t⇙"
  "⦃convert_extTA f ta⦄⇘c⇙ = ⦃ta⦄⇘c⇙"
  "⦃convert_extTA f ta⦄⇘w⇙ = ⦃ta⦄⇘w⇙"
  "⦃convert_extTA f ta⦄⇘i⇙ = ⦃ta⦄⇘i⇙"
  "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)+
done

lemma convert_extTA_eq_conv:
  "convert_extTA f ta = ta' ⟷
   ⦃ta⦄⇘l⇙ = ⦃ta'⦄⇘l⇙ ∧ ⦃ta⦄⇘c⇙ = ⦃ta'⦄⇘c⇙ ∧ ⦃ta⦄⇘w⇙ = ⦃ta'⦄⇘w⇙ ∧ ⦃ta⦄⇘o⇙ = ⦃ta'⦄⇘o⇙ ∧ ⦃ta⦄⇘i⇙ = ⦃ta'⦄⇘i⇙ ∧ length ⦃ta⦄⇘t⇙ = length ⦃ta'⦄⇘t⇙ ∧ 
   (∀n < length ⦃ta⦄⇘t⇙. convert_new_thread_action f (⦃ta⦄⇘t⇙ ! n) = ⦃ta'⦄⇘t⇙ ! n)"
apply(cases ta, cases ta')
apply(auto simp add: convert_extTA_def map_eq_all_nth_conv)
done

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"
where 
  "convert_obs_initial ta = (⦃ta⦄⇘l⇙, ⦃ta⦄⇘t⇙, ⦃ta⦄⇘c⇙, ⦃ta⦄⇘w⇙, ⦃ta⦄⇘i⇙, map NormalAction ⦃ta⦄⇘o⇙)"

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 ta⦄⇘o⇙ = map NormalAction ⦃ta⦄⇘o⇙"
  "⦃convert_obs_initial ta⦄⇘l⇙ = ⦃ta⦄⇘l⇙"
  "⦃convert_obs_initial ta⦄⇘t⇙ = ⦃ta⦄⇘t⇙"
  "⦃convert_obs_initial ta⦄⇘c⇙ = ⦃ta⦄⇘c⇙"
  "⦃convert_obs_initial ta⦄⇘w⇙ = ⦃ta⦄⇘w⇙"
  "⦃convert_obs_initial ta⦄⇘i⇙ = ⦃ta⦄⇘i⇙"
by(simp_all add: convert_obs_initial_def)

type_synonym
  ('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'
       [t4,
        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')]
  end
›
typ "('l,'t,'x,'m,'w,'o) semantics"

end