Theory FWLiftingSem

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

section ‹Semantic properties of lifted predicates›

theory FWLiftingSem
imports
  FWSemantics
  FWLifting
begin

context multithreaded_base begin

lemma redT_preserves_ts_inv_ok:
  "⟦ s -t▹ta→ s'; ts_inv_ok (thr s) I ⟧
  ⟹ ts_inv_ok (thr s') (upd_invs I P ⦃ta⦄⇘t⇙)"
by(erule redT.cases)(fastforce intro: ts_inv_ok_upd_invs ts_inv_ok_upd_ts redT_updTs_Some)+

lemma RedT_preserves_ts_inv_ok:
  "⟦ s -▹ttas→* s'; ts_inv_ok (thr s) I ⟧
  ⟹ ts_inv_ok (thr s') (upd_invs I Q (concat (map (thr_a ∘ snd) ttas)))"
by(induct rule: RedT_induct)(auto intro: redT_preserves_ts_inv_ok)

lemma redT_upd_inv_ext:
  fixes I :: "'t ⇀ 'i"
  shows "⟦ s -t▹ta→ s'; ts_inv_ok (thr s) I ⟧ ⟹ I ⊆⇩m upd_invs I P ⦃ta⦄⇘t⇙"
by(erule redT.cases, auto intro: ts_inv_ok_inv_ext_upd_invs)

lemma RedT_upd_inv_ext:
  fixes I :: "'t ⇀ 'i"
  shows "⟦ s -▹ttas→* s'; ts_inv_ok (thr s) I ⟧
         ⟹ I ⊆⇩m upd_invs I P (concat (map (thr_a ∘ snd) ttas))"
proof(induct rule: RedT_induct)
  case refl thus ?case by simp
next
  case (step S TTAS S' T TA S'')
  hence "ts_inv_ok (thr S') (upd_invs I P (concat (map (thr_a ∘ snd) TTAS)))"
    by -(rule RedT_preserves_ts_inv_ok)
  hence "upd_invs I P (concat (map (thr_a ∘ snd) TTAS)) ⊆⇩m upd_invs (upd_invs I P (concat (map (thr_a ∘ snd) TTAS))) P ⦃TA⦄⇘t⇙" 
    using step by -(rule redT_upd_inv_ext)
  with step show ?case by(auto elim!: map_le_trans simp add: comp_def)
qed

end

locale lifting_inv = multithreaded final r convert_RA
  for final :: "'x ⇒ bool" 
  and r :: "('l,'t,'x,'m,'w,'o) semantics" (‹_ ⊢ _ -_→ _› [50,0,0,50] 80) 
  and convert_RA :: "'l released_locks ⇒ 'o list"
  +
  fixes P :: "'i ⇒ 't ⇒ 'x ⇒ 'm ⇒ bool"
  assumes invariant_red: "⟦ t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩; P i t x m ⟧ ⟹ P i t x' m'"
  and invariant_NewThread: "⟦ t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩; P i t x m; NewThread t'' x'' m' ∈ set ⦃ta⦄⇘t⇙ ⟧ 
                            ⟹ ∃i''. P i'' t'' x'' m'"
  and invariant_other: "⟦ t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩; P i t x m; P i'' t'' x'' m ⟧ ⟹ P i'' t'' x'' m'"
begin

lemma redT_updTs_invariant:
  fixes ln
  assumes tsiP: "ts_inv P I ts m"
  and red: "t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩"
  and tao: "thread_oks ts ⦃ta⦄⇘t⇙"
  and tst: "ts t = ⌊(x, ln)⌋"
  shows "ts_inv P (upd_invs I P ⦃ta⦄⇘t⇙) ((redT_updTs ts ⦃ta⦄⇘t⇙)(t ↦ (x', ln'))) m'"
proof(rule ts_invI)
  fix T X LN
  assume XLN: "((redT_updTs ts ⦃ta⦄⇘t⇙)(t ↦ (x', ln'))) T = ⌊(X, LN)⌋"
  from tsiP ‹ts t = ⌊(x, ln)⌋› obtain i where "I t = ⌊i⌋" "P i t x m" 
    by(auto dest: ts_invD)
  show "∃i. upd_invs I P ⦃ta⦄⇘t⇙ T = ⌊i⌋ ∧ P i T X m'"
  proof(cases "T = t")
    case True
    from red ‹P i t x m› have "P i t x' m'" by(rule invariant_red)
    moreover from ‹I t = ⌊i⌋› ‹ts t = ⌊(x, ln)⌋› tao 
    have "upd_invs I P ⦃ta⦄⇘t⇙ t = ⌊i⌋"
      by(simp add: upd_invs_Some)
    ultimately show ?thesis using True XLN by simp
  next
    case False
    show ?thesis
    proof(cases "ts T")
      case None
      with XLN tao False have "∃m'. NewThread T X m' ∈ set ⦃ta⦄⇘t⇙"
        by(auto dest: redT_updTs_new_thread)
      with red have nt: "NewThread T X m' ∈ set ⦃ta⦄⇘t⇙" by(auto dest: new_thread_memory)
      with red ‹P i t x m› have "∃i''. P i'' T X m'" by(rule invariant_NewThread)
      hence "P (SOME i. P i T X m') T X m'" by(rule someI_ex)
      with nt tao show ?thesis by(auto intro: SOME_new_thread_upd_invs) 
    next
      case (Some a)
      obtain X' LN' where [simp]: "a = (X', LN')" by(cases a)
      with ‹ts T = ⌊a⌋› have esT: "ts T = ⌊(X', LN')⌋" by simp
      hence "redT_updTs ts ⦃ta⦄⇘t⇙ T = ⌊(X', LN')⌋"
        using ‹thread_oks ts ⦃ta⦄⇘t⇙› by(auto intro: redT_updTs_Some)
      moreover from esT tsiP obtain i' where "I T = ⌊i'⌋" "P i' T X' m"
        by(auto dest: ts_invD)
      from red ‹P i t x m› ‹P i' T X' m›
      have "P i' T X' m'" by(rule invariant_other)
      moreover from ‹I T = ⌊i'⌋› esT tao have "upd_invs I P ⦃ta⦄⇘t⇙ T = ⌊i'⌋"
        by(simp add: upd_invs_Some)
      ultimately show ?thesis using XLN False by simp
    qed
  qed
qed

theorem redT_invariant:
  assumes redT: "s -t▹ta→ s'"
  and esinvP: "ts_inv P I (thr s) (shr s)"
  shows "ts_inv P (upd_invs I P ⦃ta⦄⇘t⇙) (thr s') (shr s')"
using redT
proof(cases rule: redT_elims)
  case acquire thus ?thesis using esinvP 
    by(auto intro!: ts_invI split: if_split_asm dest: ts_invD)
next
  case (normal x x' m')
  with esinvP
  have "ts_inv P (upd_invs I P ⦃ta⦄⇘t⇙) ((redT_updTs (thr s) ⦃ta⦄⇘t⇙)(t ↦ (x', redT_updLns (locks s) t no_wait_locks ⦃ta⦄⇘l⇙))) m'"
    by(auto intro: redT_updTs_invariant)
  thus ?thesis using normal by simp
qed

theorem RedT_invariant:
  assumes RedT: "s -▹ttas→* s'"
  and esinvQ: "ts_inv P I (thr s) (shr s)"
  shows "ts_inv P (upd_invs I P (concat (map (thr_a ∘ snd) ttas))) (thr s') (shr s')"
using RedT esinvQ
proof(induct rule: RedT_induct)
  case refl thus ?case by(simp (no_asm))
next
  case (step S TTAS S' T TA S'')
  note IH = ‹ts_inv P I (thr S) (shr S) ⟹ ts_inv P (upd_invs I P (concat (map (thr_a ∘ snd) TTAS))) (thr S') (shr S')›
  with ‹ts_inv P I (thr S) (shr S)›
  have "ts_inv P (upd_invs I P (concat (map (thr_a ∘ snd) TTAS))) (thr S') (shr S')" by blast
  with ‹S' -T▹TA→ S''› 
  have "ts_inv P (upd_invs (upd_invs I P (concat (map (thr_a ∘ snd) TTAS))) P ⦃TA⦄⇘t⇙) (thr S'') (shr S'')"
    by(rule redT_invariant)
  thus ?case by(simp add: comp_def)
qed

lemma invariant3p_ts_inv: "invariant3p redT {s. ∃I. ts_inv P I (thr s) (shr s)}"
by(auto intro!: invariant3pI dest: redT_invariant)

end

locale lifting_wf = multithreaded final r convert_RA
  for final :: "'x ⇒ bool" 
  and r :: "('l,'t,'x,'m,'w,'o) semantics" (‹_ ⊢ _ -_→ _› [50,0,0,50] 80) 
  and convert_RA :: "'l released_locks ⇒ 'o list"
  +
  fixes P :: "'t ⇒ 'x ⇒ 'm ⇒ bool"
  assumes preserves_red: "⟦ t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩; P t x m ⟧ ⟹ P t x' m'"
  and preserves_NewThread: "⟦ t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩; P t x m; NewThread t'' x'' m' ∈ set ⦃ta⦄⇘t⇙ ⟧ 
                            ⟹ P t'' x'' m'"
  and preserves_other: "⟦ t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩; P t x m; P t'' x'' m ⟧ ⟹ P t'' x'' m'"
begin

lemma lifting_inv: "lifting_inv final r (λ_ :: unit. P)"
by(unfold_locales)(blast intro: preserves_red preserves_NewThread preserves_other)+

lemma redT_updTs_preserves:
  fixes ln
  assumes esokQ: "ts_ok P ts m"
  and red: "t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩"
  and "ts t = ⌊(x, ln)⌋"
  and "thread_oks ts ⦃ta⦄⇘t⇙"
  shows "ts_ok P ((redT_updTs ts ⦃ta⦄⇘t⇙)(t ↦ (x', ln'))) m'"
proof -
  interpret lifting_inv final r convert_RA "λ_ :: unit. P" by(rule lifting_inv)
  from esokQ obtain I :: "'t ⇀ unit" where "ts_inv (λ_. P) I ts m" by(rule ts_ok_into_ts_inv_const)
  hence "ts_inv (λ_. P) (upd_invs I (λ_. P) ⦃ta⦄⇘t⇙) ((redT_updTs ts ⦃ta⦄⇘t⇙)(t ↦ (x', ln'))) m'"
    using red ‹thread_oks ts ⦃ta⦄⇘t⇙› ‹ts t = ⌊(x, ln)⌋› by(rule redT_updTs_invariant)
  thus ?thesis by(rule ts_inv_const_into_ts_ok)
qed

theorem redT_preserves:
  assumes redT: "s -t▹ta→ s'"
  and esokQ: "ts_ok P (thr s) (shr s)"
  shows "ts_ok P (thr s') (shr s')"
proof -
  interpret lifting_inv final r convert_RA "λ_ :: unit. P" by(rule lifting_inv)
  from esokQ obtain I :: "'t ⇀ unit" where "ts_inv (λ_. P) I (thr s) (shr s)" by(rule ts_ok_into_ts_inv_const)
  with redT have "ts_inv (λ_. P) (upd_invs I (λ_. P) ⦃ta⦄⇘t⇙) (thr s') (shr s')" by(rule redT_invariant)
  thus ?thesis by(rule ts_inv_const_into_ts_ok)
qed

theorem RedT_preserves:
  "⟦ s -▹ttas→* s'; ts_ok P (thr s) (shr s) ⟧ ⟹ ts_ok P (thr s') (shr s')"
by(erule (1) RedT_lift_preserveD)(fastforce elim: redT_preserves)

lemma invariant3p_ts_ok: "invariant3p redT {s. ts_ok P (thr s) (shr s)}"
by(auto intro!: invariant3pI intro: redT_preserves)

end

lemma lifting_wf_Const [intro!]: 
  assumes "multithreaded final r"
  shows "lifting_wf final r (λt x m. k)"
proof -
  interpret multithreaded final r using assms .
  show ?thesis by unfold_locales blast+
qed

end