Theory FWWellform

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

header {* \isaheader{Wellformedness conditions for the multithreaded state } *}

theory FWWellform imports FWLocking FWThread begin

text{* Well-formedness property: Locks are held by real threads *}

definition
  lock_thread_ok :: "('l, 't) locks => ('l, 't,'x) thread_info => bool"
where [code del]:
  "lock_thread_ok ls ts ≡ ∀l t. has_lock (lsf l) t --> (∃xw. ts t = ⌊xw⌋)"

lemma lock_thread_ok_code [code]: 
  "lock_thread_ok ls ts = finfun_All ((λl. case l of None => True | ⌊(t, n)⌋ => (ts t ≠ None)) of ls)"
by(simp add: lock_thread_ok_def finfun_All_All has_lock_has_locks_conv has_locks_iff o_def)

lemma lock_thread_okI:
  "(!!l t. has_lock (lsf l) t ==> ∃xw. ts t = ⌊xw⌋) ==> lock_thread_ok ls ts"
by(auto simp add: lock_thread_ok_def)

lemma lock_thread_okD:
  "[| lock_thread_ok ls ts; has_lock (lsf l) t |] ==> ∃xw. ts t = ⌊xw⌋"
by(fastsimp simp add: lock_thread_ok_def)

lemma lock_thread_okD':
  "[| lock_thread_ok ls ts; has_locks (lsf l) t = Suc n |] ==> ∃xw. ts t = ⌊xw⌋"
by(auto elim: lock_thread_okD[where l=l] simp del: split_paired_Ex)

lemma lock_thread_okE:
  "[| lock_thread_ok ls ts; ∀l t. has_lock (lsf l) t --> (∃xw. ts t = ⌊xw⌋) ==> P |] ==> P"
by(auto simp add: lock_thread_ok_def simp del: split_paired_Ex)

lemma lock_thread_ok_upd:
  "lock_thread_ok ls ts ==> lock_thread_ok ls (ts(t \<mapsto> xw))"
by(auto intro!: lock_thread_okI dest: lock_thread_okD)

lemma lock_thread_ok_has_lockE:
  assumes "lock_thread_ok ls ts"
  and "has_lock (lsf l) t"
  obtains x ln where "ts t = ⌊(x, ln)⌋"
using assms
by(auto dest!: lock_thread_okD)

lemma redT_updLs_preserves_lock_thread_ok:
  assumes lto: "lock_thread_ok ls ts"
  and tst: "ts t = ⌊xw⌋"
  shows "lock_thread_ok (redT_updLs ls t las) ts"
proof(rule lock_thread_okI)
  fix L T
  assume ru: "has_lock ((redT_updLs ls t las)f L) T"
  show "∃xw. ts T = ⌊xw⌋"
  proof(cases "t = T")
    case True
    thus ?thesis using tst lto
      by(auto elim: lock_thread_okE)
  next
    case False
    with ru have "has_lock (lsf L) T"
      by(rule redT_updLs_Some_thread_idD) 
    thus ?thesis using lto
      by(auto elim!: lock_thread_okE simp del: split_paired_Ex)
  qed
qed

lemma redT_updTs_preserves_lock_thread_ok:
  assumes lto: "lock_thread_ok ls ts"
  shows "lock_thread_ok ls (redT_updTs ts nts)"
proof(rule lock_thread_okI)
  fix l t
  assume "has_lock (lsf l) t"
  with lto have "∃xw. ts t = ⌊xw⌋"
    by(auto elim!: lock_thread_okE simp del: split_paired_Ex)
  thus "∃xw. redT_updTs ts nts t = ⌊xw⌋"
    by(auto intro: redT_updTs_Some1 simp del: split_paired_Ex)
qed

lemma lock_thread_ok_has_lock:
  assumes "lock_thread_ok ls ts"
  and "has_lock (lsf l) t"
  obtains xw where "ts t = ⌊xw⌋"
using assms
by(auto dest!: lock_thread_okD)

lemma lock_thread_ok_None_has_locks_0:
  "[| lock_thread_ok ls ts; ts t = None |] ==> has_locks (lsf l) t = 0"
by(rule ccontr)(auto dest: lock_thread_okD)

lemma redT_upds_preserves_lock_thread_ok:
  "[|lock_thread_ok ls ts; ts t = ⌊xw⌋; thread_oks ts tas|]
  ==> lock_thread_ok (redT_updLs ls t las) (redT_updTs ts tas(t \<mapsto> xw'))"
apply(rule lock_thread_okI)
apply(clarsimp simp del: split_paired_Ex)
apply(drule has_lock_upd_locks_implies_has_lock, simp)
apply(drule lock_thread_okD, assumption)
apply(erule exE)
by(rule redT_updTs_Some1)

lemma acquire_all_preserves_lock_thread_ok:
  "[| lock_thread_ok ls ts; ts t = ⌊(x, ln)⌋ |] ==> lock_thread_ok (acquire_all ls t ln) (ts(t \<mapsto> xw))"
by(rule lock_thread_okI, auto dest!: has_lock_acquire_locks_implies_has_lock dest: lock_thread_okD)


end