Theory ConformThreaded

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

section ‹Conformance for threads›

theory ConformThreaded
imports
  "../Framework/FWLifting"
  "../Framework/FWWellform"
  Conform
begin

text ‹Every thread must be represented as an object whose address is its thread ID›

context heap_base begin

abbreviation thread_conf :: "'m prog ⇒ ('addr,'thread_id,'x) thread_info ⇒ 'heap ⇒ bool"
where "thread_conf P ≡ ts_ok (λt x m. P,m ⊢ t √t)"

lemma thread_confI:
  "(⋀t xln. ts t = ⌊xln⌋ ⟹ P,h ⊢ t √t) ⟹ thread_conf P ts h"
by(blast intro: ts_okI)

lemma thread_confD:
  assumes "thread_conf P ts h" "ts t = ⌊xln⌋"
  shows "P,h ⊢ t √t"
using assms by(cases xln)(auto dest: ts_okD)

lemma thread_conf_ts_upd_eq [simp]:
  assumes tst: "ts t = ⌊xln⌋"
  shows "thread_conf P (ts(t ↦ xln')) h ⟷ thread_conf P ts h"
proof
  assume tc: "thread_conf P (ts(t ↦ xln')) h"
  show "thread_conf P ts h"
  proof(rule thread_confI)
    fix T XLN
    assume "ts T = ⌊XLN⌋"
    with tc show "P,h ⊢ T √t"
      by(cases "T = t")(auto dest: thread_confD)
  qed
next
  assume tc: "thread_conf P ts h"
  show "thread_conf P (ts(t ↦ xln')) h"
  proof(rule thread_confI)
    fix T XLN
    assume "(ts(t ↦ xln')) T = ⌊XLN⌋"
    with tst obtain XLN' where "ts T = ⌊XLN'⌋"
      by(cases "T = t")(auto)
    with tc show "P,h ⊢ T √t"
      by(auto dest: thread_confD)
  qed
qed

end

context heap begin

lemma thread_conf_hext:
  "⟦ thread_conf P ts h; h ⊴ h' ⟧ ⟹ thread_conf P ts h'"
by(blast intro: thread_confI tconf_hext_mono dest: thread_confD)

lemma thread_conf_start_state:
  "⟦ start_heap_ok; wf_syscls P ⟧ ⟹ thread_conf P (thr (start_state f P C M vs)) (shr (start_state f P C M vs))"
by(auto intro!: thread_confI simp add: start_state_def split_beta split: if_split_asm intro: tconf_start_heap_start_tid)

end

context heap_base begin 

lemma lock_thread_ok_start_state:
  "lock_thread_ok (locks (start_state f P C M vs)) (thr (start_state f P C M vs))"
by(rule lock_thread_okI)(simp add: start_state_def split_beta)

lemma wset_thread_ok_start_state:
  "wset_thread_ok (wset (start_state f P C M vs)) (thr (start_state f P C M vs))"
by(auto simp add: wset_thread_ok_def start_state_def split_beta)

lemma wset_final_ok_start_state:
  "final_thread.wset_final_ok final (wset (start_state f P C M vs)) (thr (start_state f P C M vs))"
by(rule final_thread.wset_final_okI)(simp add: start_state_def split_beta)

end

end