# Theory FWInitFinLift

```(*  Title:      JinjaThreads/MM/FWInitFinLift.thy
Author:     Andreas Lochbihler
*)

section ‹Synthetic first and last actions for each thread›

theory FWInitFinLift
imports
FWLTS
FWLiftingSem
begin

datatype status =
PreStart
| Running
| Finished

where "convert_TA_initial == convert_extTA (Pair PreStart)"

lemma convert_obs_initial_convert_TA_initial:
"convert_obs_initial (convert_TA_initial ta) = convert_TA_initial (convert_obs_initial ta)"

lemma convert_TA_initial_inject [simp]:
"convert_TA_initial ta = convert_TA_initial ta' ⟷ ta = ta'"
by(cases ta)(cases ta', auto)

primrec init_fin_final :: "status × 'x ⇒ bool"
where "init_fin_final (status, x) ⟷ status = Finished ∧ final x"

end

inductive init_fin :: "('l,'t,status × 'x,'m,'w,'o action) semantics" ("_ ⊢ _ -_→i _" [50,0,0,51] 51)
where
NormalAction:
"t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩
⟹ t ⊢ ((Running, x), m) -convert_TA_initial (convert_obs_initial ta)→i ((Running, x'), m')"

"t ⊢ ((PreStart, x), m) -⦃InitialThreadAction⦄→i ((Running, x), m)"

"final x ⟹ t ⊢ ((Running, x), m) -⦃ThreadFinishAction⦄→i ((Finished, x), m)"

end

declare split_paired_Ex [simp del]

"t ⊢ ((Finished, x), m) -ta→i xm'"
"t ⊢ ((PreStart, x), m) -ta→i xm'"
"t ⊢ ((Running, x), m) -ta→i xm'"
"t ⊢ xm -ta→i ((Finished, x'), m')"
"t ⊢ xm -ta→i ((Running, x'), m')"
"t ⊢ xm -ta→i ((PreStart, x'), m')"

declare split_paired_Ex [simp]

end

constrains final :: "'x ⇒ bool"
and r :: "('l,'t,'x,'m,'w,'o) semantics"
and convert_RA :: "'l released_locks ⇒ 'o list"

"init_fin_final"
"init_fin"
"map NormalAction ∘ convert_RA"
.

constrains final :: "'x ⇒ bool"
and r :: "('l,'t,'x,'m,'w,'o) semantics"
and convert_RA :: "'l released_locks ⇒ 'o list"

"init_fin_final"
"init_fin"
"map NormalAction ∘ convert_RA"

inductive init_fin_τmove :: "('l,'t,status × 'x,'m,'w,'o action) τmoves"
where
"τmove (x, m) ta (x', m')
⟹ init_fin_τmove ((Running, x), m) (convert_TA_initial (convert_obs_initial ta)) ((Running, x'), m')"

lemma init_fin_τmove_simps [simp]:
"init_fin_τmove ((PreStart, x), m) ta x'm' = False"
"init_fin_τmove xm ta ((PreStart, x'), m') = False"
"init_fin_τmove ((Running, x), m) ta ((s, x'), m') ⟷
(∃ta'. ta = convert_TA_initial (convert_obs_initial ta') ∧ s = Running ∧ τmove (x, m) ta' (x', m'))"
"init_fin_τmove ((s, x), m) ta ((Running, x'), m') ⟷
s = Running ∧ (∃ta'. ta = convert_TA_initial (convert_obs_initial ta') ∧ τmove (x, m) ta' (x', m'))"
"init_fin_τmove ((Finished, x), m) ta x'm' = False"
"init_fin_τmove xm ta ((Finished, x'), m') = False"

lemma init_fin_silent_move_RunningI:
assumes "silent_move t (x, m) (x', m')"
shows "τtrsys.silent_move (init_fin t) init_fin_τmove ((Running, x), m) ((Running, x'), m')"
using assms by(cases)(auto intro: τtrsys.silent_move.intros init_fin.NormalAction)

lemma init_fin_silent_moves_RunningI:
assumes "silent_moves t (x, m) (x', m')"
shows "τtrsys.silent_moves (init_fin t) init_fin_τmove ((Running, x), m) ((Running, x'), m')"
using assms
by(induct rule: rtranclp_induct2)(auto elim: rtranclp.rtrancl_into_rtrancl intro: init_fin_silent_move_RunningI)

lemma init_fin_silent_moveD:
assumes "τtrsys.silent_move (init_fin t) init_fin_τmove ((s, x), m) ((s', x'), m')"
shows "silent_move t (x, m) (x', m') ∧ s = s' ∧ s' = Running"
using assms by(auto elim!: τtrsys.silent_move.cases init_fin.cases)

lemma init_fin_silent_movesD:
assumes "τtrsys.silent_moves (init_fin t) init_fin_τmove ((s, x), m) ((s', x'), m')"
shows "silent_moves t (x, m) (x', m') ∧ s = s'"
using assms
by(induct "((s, x), m)" "((s', x'), m')" arbitrary: s' x' m')
(auto 7 2 simp only: dest!: init_fin_silent_moveD intro: rtranclp.rtrancl_into_rtrancl)

lemma init_fin_τdivergeD:
assumes "τtrsys.τdiverge (init_fin t) init_fin_τmove ((status, x), m)"
shows "τdiverge t (x, m) ∧ status = Running"
proof
from assms show "status = Running"
by(cases rule: τtrsys.τdiverge.cases[consumes 1])(auto dest: init_fin_silent_moveD)
moreover define xm where "xm = (x, m)"
ultimately have "∃x m. xm = (x, m) ∧ τtrsys.τdiverge (init_fin t) init_fin_τmove ((Running, x), m)"
using assms by blast
thus "τdiverge t xm"
proof(coinduct)
case (τdiverge xm)
then obtain x m
where diverge: "τtrsys.τdiverge (init_fin t) init_fin_τmove ((Running, x), m)"
and xm: "xm = (x, m)" by blast
thus ?case
by(cases rule:τtrsys.τdiverge.cases[consumes 1])(auto dest!: init_fin_silent_moveD)
qed
qed

lemma init_fin_τdiverge_RunningI:
assumes "τdiverge t (x, m)"
shows "τtrsys.τdiverge (init_fin t) init_fin_τmove ((Running, x), m)"
proof -
define sxm where "sxm = ((Running, x), m)"
with assms have "∃x m. τdiverge t (x, m) ∧ sxm = ((Running, x), m)" by blast
thus "τtrsys.τdiverge (init_fin t) init_fin_τmove sxm"
proof(coinduct rule: τtrsys.τdiverge.coinduct[consumes 1, case_names τdiverge])
case (τdiverge sxm)
then obtain x m where "τdiverge t (x, m)" and "sxm = ((Running, x), m)" by blast
thus ?case by(cases)(auto intro: init_fin_silent_move_RunningI)
qed
qed

lemma init_fin_τdiverge_conv:
"τtrsys.τdiverge (init_fin t) init_fin_τmove ((status, x), m) ⟷
τdiverge t (x, m) ∧ status = Running"
by(blast intro: init_fin_τdiverge_RunningI dest: init_fin_τdivergeD)

end

lemma init_fin_τmoves_False:
"τmultithreaded.init_fin_τmove (λ_ _ _. False) = (λ_ _ _. False)"

constrains final :: "'x ⇒ bool"
and r :: "('l,'t,'x,'m,'w,'o) semantics"
and convert_RA :: "'l released_locks ⇒ 'o list"
and τmove :: "('l,'t,'x,'m,'w,'o) τmoves"

"init_fin_final"
"init_fin"
"map NormalAction ∘ convert_RA"
"init_fin_τmove"
.

constrains final :: "'x ⇒ bool"
and r :: "('l,'t,'x,'m,'w,'o) semantics"
and convert_RA :: "'l released_locks ⇒ 'o list"
and τmove :: "('l,'t,'x,'m,'w,'o) τmoves"

by unfold_locales

proof -
interpret "if": multithreaded init_fin_final init_fin "map NormalAction ∘ convert_RA"
show ?thesis
proof(unfold_locales)
fix t x m ta x' m'
assume "init_fin_τmove (x, m) ta (x', m')" "t ⊢ (x, m) -ta→i (x', m')"
thus "m = m'" by(cases)(auto dest: τmove_heap)
next
fix s ta s'
assume "init_fin_τmove s ta s'"
thus "ta = ε" by(cases)(auto dest: silent_tl)
qed
qed

end

"init_fin_final"
"init_fin"
"map NormalAction ∘ convert_RA"
"init_fin_τmove"

primrec init_fin_lift_inv :: "('i ⇒ 't ⇒ 'x ⇒ 'm ⇒ bool) ⇒ 'i ⇒ 't ⇒ status × 'x ⇒ 'm ⇒ bool"
where "init_fin_lift_inv P I t (s, x) = P I t x"

context lifting_inv begin

lemma lifting_inv_init_fin_lift_inv:
"lifting_inv init_fin_final init_fin (init_fin_lift_inv P)"
proof -
interpret "if": multithreaded init_fin_final init_fin "map NormalAction ∘ convert_RA"
show ?thesis
by(unfold_locales)(fastforce elim!: init_fin.cases dest: invariant_red invariant_NewThread invariant_other)+
qed

end

locale if_lifting_inv =
lifting_inv +
constrains final :: "'x ⇒ bool"
and r :: "('l,'t,'x,'m,'w,'o) semantics"
and convert_RA :: "'l released_locks ⇒ 'o list"
and P :: "'i ⇒ 't ⇒ 'x ⇒ 'm ⇒ bool"

sublocale if_lifting_inv < "if": lifting_inv
init_fin_final
init_fin
"map NormalAction ∘ convert_RA"
"init_fin_lift_inv P"
by(rule lifting_inv_init_fin_lift_inv)

primrec init_fin_lift :: "('t ⇒ 'x ⇒ 'm ⇒ bool) ⇒ 't ⇒ status × 'x ⇒ 'm ⇒ bool"
where "init_fin_lift P t (s, x) = P t x"

context lifting_wf begin

lemma lifting_wf_init_fin_lift:
"lifting_wf init_fin_final init_fin (init_fin_lift P)"
proof -
interpret "if": multithreaded init_fin_final init_fin "map NormalAction ∘ convert_RA"
show ?thesis
by(unfold_locales)(fastforce elim!: init_fin.cases dest: dest: preserves_red preserves_other preserves_NewThread)+
qed

end

locale if_lifting_wf =
lifting_wf +
constrains final :: "'x ⇒ bool"
and r :: "('l,'t,'x,'m,'w,'o) semantics"
and convert_RA :: "'l released_locks ⇒ 'o list"
and P :: "'t ⇒ 'x ⇒ 'm ⇒ bool"

sublocale if_lifting_wf < "if": lifting_wf
init_fin_final
init_fin
"map NormalAction ∘ convert_RA"
"init_fin_lift P"
by(rule lifting_wf_init_fin_lift)

lemma (in if_lifting_wf) if_lifting_inv:
"if_lifting_inv final r (λ_::unit. P)"
proof -
interpret lifting_inv final r convert_RA  "λ_ :: unit. P" by(rule lifting_inv)
show ?thesis by unfold_locales
qed

lifting_inv +
constrains final :: "'x ⇒ bool"
and r :: "('l,'t,'x,'m,'w,'o) semantics"
and convert_RA :: "'l released_locks ⇒ 'o list"
and τmove :: "('l,'t,'x,'m,'w,'o) τmoves"
and P :: "'i ⇒ 't ⇒ 'x ⇒ 'm ⇒ bool"
begin

lemma redT_silent_move_invariant:
"⟦ τmredT s s'; ts_inv P Is (thr s) (shr s) ⟧ ⟹ ts_inv P Is (thr s') (shr s')"
by(auto dest!: redT_invariant mτmove_silentD)

lemma redT_silent_moves_invariant:
"⟦ mthr.silent_moves s s'; ts_inv P Is (thr s) (shr s) ⟧ ⟹ ts_inv P Is (thr s') (shr s')"
by(induct rule: rtranclp_induct)(auto dest: redT_silent_move_invariant)

lemma redT_τrtrancl3p_invariant:
"⟦ mthr.τrtrancl3p s ttas s'; ts_inv P Is (thr s) (shr s) ⟧
⟹ ts_inv P (upd_invs Is P (concat (map (thr_a ∘ snd) ttas))) (thr s') (shr s')"
proof(induct arbitrary: Is rule: mthr.τrtrancl3p.induct)
case τrtrancl3p_refl thus ?case by simp
next
case (τrtrancl3p_step s s' tls s'' tl)
thus ?case by(cases tl)(force dest: redT_invariant)
next
case (τrtrancl3p_τstep s s' tls s'' tl)
thus ?case by(cases tl)(force dest: redT_invariant mτmove_silentD)
qed

end

lifting_wf +
constrains final :: "'x ⇒ bool"
and r :: "('l,'t,'x,'m,'w,'o) semantics"
and convert_RA :: "'l released_locks ⇒ 'o list"
and τmove :: "('l,'t,'x,'m,'w,'o) τmoves"
and P :: "'t ⇒ 'x ⇒ 'm ⇒ bool"
begin

lemma redT_silent_move_preserves:
"⟦ τmredT s s'; ts_ok P (thr s) (shr s) ⟧ ⟹ ts_ok P (thr s') (shr s')"
by(auto dest: redT_preserves)

lemma redT_silent_moves_preserves:
"⟦ mthr.silent_moves s s'; ts_ok P (thr s) (shr s) ⟧ ⟹ ts_ok P (thr s') (shr s')"
by(induct rule: rtranclp.induct)(auto dest: redT_silent_move_preserves)

lemma redT_τrtrancl3p_preserves:
"⟦ mthr.τrtrancl3p s ttas s'; ts_ok P (thr s) (shr s) ⟧ ⟹ ts_ok P (thr s') (shr s')"
by(induct rule: mthr.τrtrancl3p.induct)(auto dest: redT_silent_moves_preserves redT_preserves)

end

definition init_fin_lift_state :: "status ⇒ ('l,'t,'x,'m,'w) state ⇒ ('l,'t,status × 'x,'m,'w) state"
where "init_fin_lift_state s σ = (locks σ, (λt. map_option (λ(x, ln). ((s, x), ln)) (thr σ t), shr σ), wset σ, interrupts σ)"

where "init_fin_descend_thr ts = map_option (λ((s, x), ln). (x, ln)) ∘ ts"

definition init_fin_descend_state :: "('l,'t,'status × 'x,'m,'w) state ⇒ ('l,'t,'x,'m,'w) state"
where "init_fin_descend_state σ = (locks σ, (init_fin_descend_thr (thr σ), shr σ), wset σ, interrupts σ)"

lemma ts_ok_init_fin_lift_init_fin_lift_state [simp]:
"ts_ok (init_fin_lift P) (thr (init_fin_lift_state s σ)) (shr (init_fin_lift_state s σ)) ⟷ ts_ok P (thr σ) (shr σ)"
by(auto simp add: init_fin_lift_state_def intro!: ts_okI dest: ts_okD)

lemma ts_inv_init_fin_lift_inv_init_fin_lift_state [simp]:
"ts_inv (init_fin_lift_inv P) I (thr (init_fin_lift_state s σ)) (shr (init_fin_lift_state s σ)) ⟷
ts_inv P I (thr σ) (shr σ)"
by(auto simp add: init_fin_lift_state_def intro!: ts_invI dest: ts_invD)

lemma init_fin_lift_state_conv_simps:
shows shr_init_fin_lift_state: "shr (init_fin_lift_state s σ) = shr σ"
and locks_init_fin_lift_state: "locks (init_fin_lift_state s σ) = locks σ"
and wset_init_fin_lift_state: "wset (init_fin_lift_state s σ) = wset σ"
and interrupts_init_fin_lift_stae: "interrupts (init_fin_lift_state s σ) = interrupts σ"
and thr_init_fin_list_state:
"thr (init_fin_lift_state s σ) t = map_option (λ(x, ln). ((s, x), ln)) (thr σ t)"

lemma thr_init_fin_list_state':
"thr (init_fin_lift_state s σ) = map_option (λ(x, ln). ((s, x), ln)) ∘ thr σ"

lemma init_fin_descend_thr_Some_conv [simp]:
"⋀ln. ts t = ⌊((status, x), ln)⌋ ⟹ init_fin_descend_thr ts t = ⌊(x, ln)⌋"

lemma init_fin_descend_thr_None_conv [simp]:
"ts t = None ⟹ init_fin_descend_thr ts t = None"

lemma init_fin_descend_thr_eq_None [simp]:
"init_fin_descend_thr ts t = None ⟷ ts t = None"

lemma init_fin_descend_state_simps [simp]:
"init_fin_descend_state (ls, (ts, m), ws, is) = (ls, (init_fin_descend_thr ts, m), ws, is)"
"locks (init_fin_descend_state s) = locks s"
"thr (init_fin_descend_state s) = init_fin_descend_thr (thr s)"
"shr (init_fin_descend_state s) = shr s"
"wset (init_fin_descend_state s) = wset s"
"interrupts (init_fin_descend_state s) = interrupts s"

lemma init_fin_descend_thr_update [simp]:
"init_fin_descend_thr (ts(t := v)) = (init_fin_descend_thr ts)(t := map_option (λ((status, x), ln). (x, ln)) v)"

lemma ts_ok_init_fin_descend_state:
"ts_ok P (init_fin_descend_thr ts) = ts_ok (init_fin_lift P) ts"
by(rule ext)(auto 4 3 intro!: ts_okI dest: ts_okD simp add: init_fin_descend_thr_def)

lemma redT_updT'_init_fin_descend_thr_eq_None [simp]:
"redT_updT' (init_fin_descend_thr ts) nt t = None ⟷ redT_updT' ts nt t = None"
by(cases nt) simp_all

by(cases nta) simp_all

by(induct ntas arbitrary: ts)(auto elim!: thread_oks_ts_change[THEN iffD1, rotated 1])

lemma init_fin_descend_thr_redT_updT [simp]:
"init_fin_descend_thr (redT_updT ts (convert_new_thread_action (Pair status) nt)) =
redT_updT (init_fin_descend_thr ts) nt"
by(cases nt) simp_all

lemma init_fin_descend_thr_redT_updTs [simp]:
"init_fin_descend_thr (redT_updTs ts (map (convert_new_thread_action (Pair status)) nts)) =
redT_updTs (init_fin_descend_thr ts) nts"
by(induct nts arbitrary: ts) simp_all

lemma cond_action_ok_init_fin_descend_stateI [simp]:
"final_thread.cond_action_ok init_fin_final s t ct ⟹ cond_action_ok (init_fin_descend_state s) t ct"

lemma cond_action_oks_init_fin_descend_stateI [simp]:
"final_thread.cond_action_oks init_fin_final s t cts ⟹ cond_action_oks (init_fin_descend_state s) t cts"

end

definition lift_start_obs :: "'t ⇒ 'o list ⇒ ('t × 'o action) list"
where "lift_start_obs t obs = (t, InitialThreadAction) # map (λob. (t, NormalAction ob)) obs"

lemma length_lift_start_obs [simp]: "length (lift_start_obs t obs) = Suc (length obs)"