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