Theory FWLiftingSem

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

header {* \isaheader{Semantic properties of lifted predicates} *}

theory FWLiftingSem imports FWSemantics FWLifting begin

context multithreaded begin

lemma redT_preserves_ts_inv_ok:
  "[| s -t\<triangleright>ta-> s'; ts_inv_ok (thr s) I |]
  ==> ts_inv_ok (thr s') (upd_invs I P \<lbrace>ta\<rbrace>t)"
apply(erule redT.cases)
apply(auto intro: ts_inv_ok_upd_invs ts_inv_ok_upd_ts redT_updTs_Some)
done

lemma RedT_preserves_ts_inv_ok:
  "[| s -\<triangleright>ttas->* s'; ts_inv_ok (thr s) I |]
  ==> ts_inv_ok (thr s') (upd_invs I Q (\<down>map (thr_a o snd) ttas\<down>))"
by(induct rule: RedT_induct)(auto intro: redT_preserves_ts_inv_ok)

lemma redT_upd_inv_ext:
  fixes I :: "'t \<rightharpoonup> 'i"
  shows "[| s -t\<triangleright>ta-> s'; ts_inv_ok (thr s) I |] ==> I \<unlhd> upd_invs I P \<lbrace>ta\<rbrace>t"
by(erule redT.cases, auto intro: ts_inv_ok_inv_ext_upd_invs)

lemma RedT_upd_inv_ext:
  fixes I :: "'t \<rightharpoonup> 'i"
  shows "[| s -\<triangleright>ttas->* s'; ts_inv_ok (thr s) I |]
         ==> I \<unlhd> upd_invs I P (\<down>map (thr_a o snd) ttas\<down>)"
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 (\<down>map (thr_a o snd) TTAS\<down>))"
    by -(erule RedT_preserves_ts_inv_ok, assumption)
  hence "upd_invs I P (\<down>map (thr_a o snd) TTAS\<down>) \<unlhd> upd_invs (upd_invs I P (\<down>map (thr_a o snd) TTAS\<down>)) P \<lbrace>TA\<rbrace>t" using step
    by -(erule redT_upd_inv_ext)
  with step show ?case
    apply(simp)
    apply(erule inv_ext_trans)
    by(simp add: comp_def)
qed

end

locale lifting_wf = multithreaded _ r
  for r :: "('l,'t,'x,'m,'w,'o) semantics" +
  fixes P :: "'x => 'm => bool"
  assumes preserves_red: "[| r (x, m) ta (x', m'); P x m |] ==> P x' m'"
  assumes preserves_NewThread: "[| r (x, m) ta (x', m'); P x m; NewThread t'' x'' m' ∈ set \<lbrace>ta\<rbrace>t |] ==> P x'' m'"
  assumes preserves_other: "[| r (x, m) ta (x', m'); P x m; P x'' m |] ==> P x'' m'"
begin


lemma redT_preserves:
  assumes redT: "s -t\<triangleright>ta-> s'"
  and esokQ: "ts_ok P (thr s) (shr s)"
  shows "ts_ok P (thr s') (shr s')"
proof(rule ts_okI)
  fix T X LN
  assume "thr s' T = ⌊(X, LN)⌋"
  moreover obtain ls ts m ws where s [simp]: "s = (ls, (ts, m), ws)" by(cases s, auto)
  moreover obtain ls' ts' m' ws' where s' [simp]: "s' = (ls', (ts', m'), ws')" by(cases s', auto)
  ultimately have es't': "ts' T = ⌊(X, LN)⌋" by auto
  obtain las tas cas was obs where ta: "ta = (las, tas, cas, was, obs)" by(cases ta)
  from redT show "P X (shr s')"
  proof(induct rule: redT_elims)
    case (normal x x' ta')
    with ta have red: "⟨x, m⟩ -ta'-> ⟨x', m'⟩"
      and est: "ts t = ⌊(x, no_wait_locks)⌋"
      and lota: "lock_ok_las ls t las"
      and cctta: "thread_oks ts tas"
      and cdta: "cond_action_oks (ls, (ts, m), ws) t cas"
      and wst: "ws t = None"
      and ls': "ls' = redT_updLs ls t las"
      and es': "ts' = redT_updTs ts tas(t \<mapsto> (x', redT_updLns ls t no_wait_locks las))"
      and ws': "ws' = redT_updWs ws t was"
      and [simp]: "ta = observable_ta_of ta'"
      by(auto)
    from est esokQ have qex: "P x m" by(auto dest: ts_okD)
    show "P X (shr s')"
    proof(cases "t = T")
      assume tt': "t = T"
      from red qex have "P x' m'" by(rule preserves_red)
      moreover from es't' es' tt' have "X = x'" by(simp)
      ultimately show ?thesis by simp
    next
      assume tt': "t ≠ T"
      show ?thesis
      proof(cases "ts T")
        assume esT: "ts T = None"
        with es't' est redT ta have "NewThread T X m' ∈ set tas"
          by(auto dest!: redT_new_thread)
        thus ?thesis using red qex ta
          by(auto intro: preserves_NewThread simp add: observable_ta_of_def)
      next
        fix a
        assume "ts T = ⌊a⌋"
        obtain x ln where [simp]: "a = (x, ln)" by (cases a, auto)
        from `ts T = ⌊a⌋` have esT: "ts T = ⌊(x, ln)⌋" by simp
        with redT tt' esT have "ts' T = ⌊(x, ln)⌋"
          by(auto elim: redT_ts_Some_inv)
        with es't' have "X = x" by auto
        moreover
        from esT esokQ have "P x m" by(auto dest: ts_okD)
        with qex have "P x m'" by -(rule preserves_other[OF red])
        ultimately show ?thesis by simp
      qed
    qed
  next
    fix x ln
    assume "shr s' = shr s" "thr s' = thr s(t \<mapsto> (x, no_wait_locks))" 
      and "thr s t = ⌊(x, ln)⌋"
    hence [simp]: "m = m'" "ts' = ts(t \<mapsto> (x, no_wait_locks))" by(auto)
    show ?thesis
    proof(cases "T = t")
      case True 
      note [simp] = this
      with es't' have "X = x" by(simp)
      with esokQ `thr s t = ⌊(x, ln)⌋` 
      show ?thesis by(auto dest!: ts_okD)
    next
      case False
      with es't' have "ts T = ⌊(X, LN)⌋" by(simp)
      with esokQ show ?thesis by(auto dest: ts_okD)
    qed
  qed
qed

lemma RedT_preserves:
  "[| s -\<triangleright>ttas->* s'; ts_ok P (thr s) (shr s) |] ==> ts_ok P (thr s') (shr s')"
apply(erule RedT_lift_preserveD, assumption)
by(fastsimp elim: redT_preserves)

end

lemma lifting_wf_Const [intro!]: "multithreaded r ==> lifting_wf r (λx m. k)"
by(unfold_locales)(rule multithreaded.new_thread_memory)

locale lifting_inv = lifting_wf final r Q 
  for final :: "'x => bool" and
      r :: "('l,'t,'x,'m,'w,'o) semantics" and
      Q :: "'x => 'm => bool" +
  fixes P :: "'i => 'x => 'm => bool"
  assumes invariant_red: "[| r (x, m) ta (x', m'); P i x m; Q x m |] ==> P i x' m'"
  assumes invariant_NewThread: "[| r (x, m) ta (x', m'); P i x m; Q x m; NewThread t'' x'' m' ∈ set \<lbrace>ta\<rbrace>t |] ==> ∃i''. P i'' x'' m'"
  assumes invariant_other: "[| r (x, m) ta (x', m'); P i x m; Q x m; P i'' x'' m; Q x'' m |] ==> P i'' x'' m'"
begin

lemma redT_invariant:
  assumes redT: "s -t\<triangleright>ta-> s'"
  and esinvP: "ts_inv P I (thr s) (shr s)"
  and esokQ: "ts_ok Q (thr s) (shr s)"
  shows "ts_inv P (upd_invs I P \<lbrace>ta\<rbrace>t) (thr s') (shr s')"
proof(rule ts_invI)
  fix T X LN
  assume "thr s' T = ⌊(X, LN)⌋"
  moreover obtain ls ts m ws where s [simp]: "s = (ls, (ts, m), ws)" by(cases s, auto)
  moreover obtain ls' ts' m' ws' where s' [simp]: "s' = (ls', (ts', m'), ws')" by(cases s', auto)
  ultimately have es't': "ts' T = ⌊(X, LN)⌋" by auto
  obtain las tas cas was obs where ta: "ta = (las, tas, cas, was, obs)" by (cases ta)
  from redT show "∃i. upd_invs I P \<lbrace>ta\<rbrace>t T = ⌊i⌋ ∧ P i X (shr s')"
  proof(induct rule: redT_elims)
    case (normal x x' ta')
    with ta have red: "⟨x, m⟩ -ta'-> ⟨x', m'⟩"
      and est: "ts t = ⌊(x, no_wait_locks)⌋"
      and lota: "lock_ok_las ls t las"
      and cctta: "thread_oks ts tas"
      and cdta: "cond_action_oks (ls, (ts, m), ws) t cas"
      and wst: "ws t = None"
      and ls': "ls' = redT_updLs ls t las"
      and es': "ts' = redT_updTs ts tas(t \<mapsto> (x', redT_updLns ls t no_wait_locks las))"
      and ws': "ws' = redT_updWs ws t was"
      and [simp]: "ta = observable_ta_of ta'"
      by(auto)
    from est esinvP obtain i where Iti: "I t = ⌊i⌋" and qiex: "P i x m"
      by(auto dest: ts_invD)
    from est esokQ Iti have rex: "Q x m" by(auto dest!: ts_okD)
    show ?thesis
    proof(cases "t = T")
      assume tT: "t = T"
      from qiex red rex have "P i x' m'"
        by -(rule invariant_red)
      moreover
      from tT est cctta Iti have "upd_invs I P tas t = ⌊i⌋"
        by(auto intro: upd_invs_Some) 
      moreover
      from es't' es' tT have "X = x'" by simp
      ultimately show ?thesis using tT ta by clarsimp
    next
      assume tT: "t ≠ T"
      show ?thesis
      proof(cases "ts T")
        assume esT: "ts T = None" 
        with es't' est redT ta have nt: "NewThread T X m' ∈ set \<lbrace>ta\<rbrace>t"
          by -(auto dest: redT_new_thread)
        with red qiex rex have i: "∃i''. P i'' X m'"
          by(auto intro!: invariant_NewThread)
        hence "P (SOME i. P i X m') X m'"
          by-(rule someI_ex)
        with nt cctta ta show ?thesis
          by (auto intro: SOME_new_thread_upd_invs simp add: observable_ta_of_def) 
      next
        fix a
        assume "ts T = ⌊a⌋"
        obtain x ln where [simp]: "a = (x, ln)" by(cases a, auto)
        with `ts T = ⌊a⌋` have esT: "ts T = ⌊(x, ln)⌋" by simp
        with redT tT have "ts' T = ⌊(x, ln)⌋" by(auto dest: redT_ts_Some_inv)
        with es't' have "X = x" by auto
        moreover
        from esT esinvP obtain i' where i': "I T = ⌊i'⌋" and qi'ex: "P i' x m"
          by(auto dest: ts_invD)
        from esT esokQ have "Q x m" by (auto dest: ts_okD)
        hence "P i' x m'" using red qiex rex qi'ex
          by(auto intro: invariant_other)
        moreover
        have "upd_invs I P tas T = ⌊i'⌋" using i'
          by(simp add: upd_invs_Some_eq[OF cctta, OF esT])
        ultimately show ?thesis using ta by auto
      qed
    qed
  next
    case (acquire x ln)
    hence [simp]: "m' = m" "ta = (λf [], [], [], [], ReacquireLocks ln)"
      "ts' = ts(t \<mapsto> (x, no_wait_locks))" by auto
    show ?thesis
    proof(cases "T = t")
      case True
      with `thr s t = ⌊(x, ln)⌋` es't'
      have [simp]: "X = x" by(simp)
      from True `thr s t = ⌊(x, ln)⌋` `ts_inv P I (thr s) (shr s)`
      obtain i where "I t = ⌊i⌋" and "P i x m" by(auto dest: ts_invD)
      with True show ?thesis by(simp)
    next
      case False
      with es't' `ts_inv P I (thr s) (shr s)`
      obtain i where "I T = ⌊i⌋" and "P i X (shr s)" by(auto dest: ts_invD)
      thus ?thesis by simp
    qed
  qed
qed


lemma RedT_invariant:
  assumes RedT: "s -\<triangleright>ttas->* s'"
  and esinvQ: "ts_inv P I (thr s) (shr s)"
  and esokR: "ts_ok Q (thr s) (shr s)"
  shows "ts_inv P (upd_invs I P (\<down>map (thr_a o snd) ttas\<down>)) (thr s') (shr s')"
using RedT esinvQ esokR
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_ok Q (thr S) (shr S)|] 
             ==> ts_inv P (upd_invs I P (\<down>map (thr_a o snd) TTAS\<down>)) (thr S') (shr S')`
  with `ts_inv P I (thr S) (shr S)` `ts_ok Q (thr S) (shr S)`
  have "ts_inv P (upd_invs I P (\<down>map (thr_a o snd) TTAS\<down>)) (thr S') (shr S')" by blast
  moreover from `S -\<triangleright>TTAS->* S'` `ts_ok Q (thr S) (shr S)`
  have "ts_ok Q (thr S') (shr S')" by(rule RedT_preserves)
  ultimately have "ts_inv P (upd_invs (upd_invs I P (\<down>map (thr_a o snd) TTAS\<down>)) P \<lbrace>TA\<rbrace>t) (thr S'') (shr S'')"
    using `S' -T\<triangleright>TA-> S''`
    by -(rule redT_invariant)
  thus ?case by(simp add: comp_def)
qed

end


end