Theory ConformThreaded

(*  Title:      JinjaThreads/Common/ConformThreaded.thy
    Author:     Andreas Lochbihler
*)

header{* \isaheader{Conformance for threads} *}

theory ConformThreaded imports "../Framework/FWState" Exceptions  begin

text {* Every thread must be represented as an object whose address is its thread ID *}

definition thread_conf :: "'m prog => (addr,thread_id,'x) thread_info => heap => bool"
where "thread_conf P ts h ≡ ∀t xln. ts t = ⌊xln⌋ --> (∃T. typeofh (Addr t) = Some T ∧ P \<turnstile> T ≤ Class Thread)"

lemma thread_confI:
  "(!!t xln. ts t = ⌊xln⌋ ==> ∃T. typeofh (Addr t) = Some T ∧ P \<turnstile> T ≤ Class Thread) ==> thread_conf P ts h"
unfolding thread_conf_def by blast

lemma thread_confDE:
  assumes "thread_conf P ts h" "ts t = ⌊xln⌋"
  obtains T where "typeofh (Addr t) = Some T" "P \<turnstile> T ≤ Class Thread"
using assms unfolding thread_conf_def by blast

lemma thread_conf_hext:
  "[| thread_conf P ts h; h \<unlhd> h' |] ==> thread_conf P ts h'"
apply(rule thread_confI)
apply(erule thread_confDE, assumption)
apply(clarsimp split: heapobj.split_asm)
 apply(drule hext_objD, assumption)
 apply(fastsimp)
apply(drule hext_arrD, assumption)
apply(fastsimp)
done

lemma thread_conf_ts_upd_eq [simp]:
  assumes tst: "ts t = ⌊xln⌋"
  shows "thread_conf P (ts(t \<mapsto> xln')) h <-> thread_conf P ts h"
proof
  assume tc: "thread_conf P (ts(t \<mapsto> xln')) h"
  show "thread_conf P ts h"
  proof(rule thread_confI)
    fix T XLN
    assume "ts T = ⌊XLN⌋"
    with tc show "∃T'. typeofh (Addr T) = ⌊T'⌋ ∧ P \<turnstile> T' ≤ Class Thread"
      by(cases "T = t")(auto elim: thread_confDE)
  qed
next
  assume tc: "thread_conf P ts h"
  show "thread_conf P (ts(t \<mapsto> xln')) h"
  proof(rule thread_confI)
    fix T XLN
    assume "(ts(t \<mapsto> xln')) T = ⌊XLN⌋"
    with tst obtain XLN' where "ts T = ⌊XLN'⌋"
      by(cases "T = t")(auto)
    with tc show "∃T'. typeofh (Addr T) = ⌊T'⌋ ∧ P \<turnstile> T' ≤ Class Thread"
      by(auto elim: thread_confDE)
  qed
qed

end