Theory FWLifting

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

section ‹Lifting of thread-local properties to the multithreaded case›

theory FWLifting
imports
  FWWellform
begin

text‹Lifting for properties that only involve thread-local state information and the shared memory.›

definition
  ts_ok :: "('t ⇒ 'x ⇒ 'm ⇒ bool) ⇒ ('l, 't,'x) thread_info ⇒ 'm ⇒ bool"
where
  "⋀ln. ts_ok P ts m ≡ ∀t. case (ts t) of None ⇒ True | ⌊(x, ln)⌋ ⇒ P t x m"

lemma ts_okI:
  "⟦ ⋀t x ln. ts t = ⌊(x, ln)⌋ ⟹ P t x m ⟧ ⟹ ts_ok P ts m"
by(auto simp add: ts_ok_def)

lemma ts_okE:
  "⟦ ts_ok P ts m; ⟦ ⋀t x ln. ts t = ⌊(x, ln)⌋ ⟹ P t x m ⟧ ⟹ Q ⟧ ⟹ Q"
by(auto simp add: ts_ok_def)

lemma ts_okD:
  "⋀ln. ⟦ ts_ok P ts m; ts t = ⌊(x, ln)⌋ ⟧ ⟹ P t x m"
by(auto simp add: ts_ok_def)

lemma ts_ok_True [simp]:
  "ts_ok (λt m x. True) ts m"
by(auto intro: ts_okI)

lemma ts_ok_conj:
  "ts_ok (λt x m. P t x m ∧ Q t x m) = (λts m. ts_ok P ts m ∧ ts_ok Q ts m)"
by(auto intro: ts_okI intro!: ext dest: ts_okD)

lemma ts_ok_mono:
  "⟦ ts_ok P ts m; ⋀t x. P t x m ⟹ Q t x m ⟧ ⟹ ts_ok Q ts m"
by(auto intro!: ts_okI dest: ts_okD)

text‹Lifting for properites, that also require additional data that does not change during execution›

definition
  ts_inv :: "('i ⇒ 't ⇒ 'x ⇒ 'm ⇒ bool) ⇒ ('t ⇀ 'i) ⇒ ('l,'t,'x) thread_info ⇒ 'm ⇒ bool"
where
  "⋀ln. ts_inv P I ts m ≡ ∀t. case (ts t) of None ⇒ True | ⌊(x, ln)⌋ ⇒ ∃i. I t = ⌊i⌋ ∧ P i t x m" 

lemma ts_invI:
  "⟦ ⋀t x ln. ts t = ⌊(x, ln)⌋ ⟹ ∃i. I t = ⌊i⌋ ∧ P i t x m ⟧ ⟹ ts_inv P I ts m"
by(simp add: ts_inv_def)

lemma ts_invE:
  "⟦ ts_inv P I ts m; ∀t x ln. ts t = ⌊(x, ln)⌋ ⟶ (∃i. I t = ⌊i⌋ ∧ P i t x m) ⟹ R ⟧ ⟹ R"
by(auto simp add: ts_inv_def)

lemma ts_invD:
  "⋀ln. ⟦ ts_inv P I ts m; ts t = ⌊(x, ln)⌋ ⟧ ⟹ ∃i. I t = ⌊i⌋ ∧ P i t x m"
by(auto simp add: ts_inv_def)

text ‹Wellformedness properties for lifting›

definition
  ts_inv_ok :: "('l,'t,'x) thread_info ⇒ ('t ⇀ 'i) ⇒ bool"
where
  "ts_inv_ok ts I ≡ ∀t. ts t = None ⟷ I t = None"

lemma ts_inv_okI:
  "(⋀t. ts t = None ⟷ I t = None) ⟹ ts_inv_ok ts I"
by(clarsimp simp add: ts_inv_ok_def)

lemma ts_inv_okI2:
  "(⋀t. (∃v. ts t = ⌊v⌋) ⟷ (∃v. I t = ⌊v⌋)) ⟹ ts_inv_ok ts I"
by(force simp add: ts_inv_ok_def)

lemma ts_inv_okE:
  "⟦ ts_inv_ok ts I; ∀t. ts t = None ⟷ I t = None ⟹ P ⟧ ⟹ P"
by(force simp add: ts_inv_ok_def)

lemma ts_inv_okE2:
  "⟦ ts_inv_ok ts I; ∀t. (∃v. ts t = ⌊v⌋) ⟷ (∃v. I t = ⌊v⌋) ⟹ P ⟧ ⟹ P"
by(force simp add: ts_inv_ok_def)

lemma ts_inv_okD:
  "ts_inv_ok ts I ⟹ (ts t = None) ⟷ (I t = None)"
by(erule ts_inv_okE, blast)

lemma ts_inv_okD2:
  "ts_inv_ok ts I ⟹ (∃v. ts t = ⌊v⌋) ⟷ (∃v. I t = ⌊v⌋)"
by(erule ts_inv_okE2, blast)

lemma ts_inv_ok_conv_dom_eq:
  "ts_inv_ok ts I ⟷ (dom ts = dom I)"
proof -
  have "ts_inv_ok ts I ⟷ (∀t. ts t = None ⟷ I t = None)"
    unfolding ts_inv_ok_def by blast
  also have "… ⟷ (∀t. t ∈ - dom ts ⟷ t ∈ - dom I)" by(force)
  also have "… ⟷ dom ts = dom I" by auto
  finally show ?thesis .
qed

lemma ts_inv_ok_upd_ts:
  "⟦ ts t = ⌊x⌋; ts_inv_ok ts I ⟧ ⟹ ts_inv_ok (ts(t ↦ x')) I"
by(auto dest!: ts_inv_okD intro!: ts_inv_okI split: if_splits)

lemma ts_inv_upd_map_option:
  assumes "ts_inv P I ts m"
  and "⋀x ln. ts t = ⌊(x, ln)⌋ ⟹ P (the (I t)) t (fst (f (x, ln))) m"
  shows "ts_inv P I (ts(t := (map_option f (ts t)))) m"
using assms
by(fastforce intro!: ts_invI split: if_split_asm dest: ts_invD)

fun upd_inv :: "('t ⇀ 'i) ⇒ ('i ⇒ 't ⇒ 'x ⇒ 'm ⇒ bool) ⇒ ('t,'x,'m) new_thread_action ⇒ ('t ⇀ 'i)"
where
  "upd_inv I P (NewThread t x m) = I(t ↦ SOME i. P i t x m)"
| "upd_inv I P _ = I"

fun upd_invs :: "('t ⇀ 'i) ⇒ ('i ⇒ 't ⇒ 'x ⇒ 'm ⇒ bool) ⇒ ('t,'x,'m) new_thread_action list ⇒ ('t ⇀ 'i)"
where
  "upd_invs I P [] = I"
| "upd_invs I P (ta#tas) = upd_invs (upd_inv I P ta) P tas"

lemma upd_invs_append [simp]:
  "upd_invs I P (xs @ ys) = upd_invs (upd_invs I P xs) P ys"
by(induct xs arbitrary: I)(auto)

lemma ts_inv_ok_upd_inv':
 "ts_inv_ok ts I ⟹ ts_inv_ok (redT_updT' ts ta) (upd_inv I P ta)"
by(cases ta)(auto intro!: ts_inv_okI elim: ts_inv_okD del: iffI)

lemma ts_inv_ok_upd_invs':
  "ts_inv_ok ts I ⟹ ts_inv_ok (redT_updTs' ts tas) (upd_invs I P tas)"
proof(induct tas arbitrary: ts I)
  case Nil thus ?case by simp
next
  case (Cons TA TAS TS I)
  note IH = ‹⋀ts I. ts_inv_ok ts I ⟹ ts_inv_ok (redT_updTs' ts TAS) (upd_invs I P TAS)›
  note esok = ‹ts_inv_ok TS I›
  from esok have "ts_inv_ok (redT_updT' TS TA) (upd_inv I P TA)"
    by -(rule ts_inv_ok_upd_inv')
  hence "ts_inv_ok (redT_updTs' (redT_updT' TS TA) TAS) (upd_invs (upd_inv I P TA) P TAS)"
    by (rule IH)
  thus ?case by simp
qed

lemma ts_inv_ok_upd_inv:
 "ts_inv_ok ts I ⟹ ts_inv_ok (redT_updT ts ta) (upd_inv I P ta)"
apply(cases ta)
apply(auto intro!: ts_inv_okI elim: ts_inv_okD del: iffI)
done

lemma ts_inv_ok_upd_invs:
  "ts_inv_ok ts I ⟹ ts_inv_ok (redT_updTs ts tas) (upd_invs I P tas)"
proof(induct tas arbitrary: ts I)
  case Nil thus ?case by simp
next
  case (Cons TA TAS TS I)
  note IH = ‹⋀ts I. ts_inv_ok ts I ⟹ ts_inv_ok (redT_updTs ts TAS) (upd_invs I P TAS)›
  note esok = ‹ts_inv_ok TS I›
  from esok have "ts_inv_ok (redT_updT TS TA) (upd_inv I P TA)"
    by -(rule ts_inv_ok_upd_inv)
  hence "ts_inv_ok (redT_updTs (redT_updT TS TA) TAS) (upd_invs (upd_inv I P TA) P TAS)"
    by (rule IH)
  thus ?case by simp
qed

lemma ts_inv_ok_inv_ext_upd_inv:
  "⟦ ts_inv_ok ts I; thread_ok ts ta ⟧ ⟹ I ⊆⇩m upd_inv I P ta"
by(cases ta)(auto intro!: map_le_same_upd dest: ts_inv_okD)

lemma ts_inv_ok_inv_ext_upd_invs:
  "⟦ ts_inv_ok ts I; thread_oks ts tas⟧
  ⟹ I ⊆⇩m upd_invs I P tas"
proof(induct tas arbitrary: ts I)
  case Nil thus ?case by simp
next
  case (Cons TA TAS TS I)
  note IH = ‹⋀ts I. ⟦ ts_inv_ok ts I; thread_oks ts TAS⟧ ⟹ I ⊆⇩m upd_invs I P TAS›
  note esinv = ‹ts_inv_ok TS I›
  note cct = ‹thread_oks TS (TA # TAS)›
  from esinv cct have "I ⊆⇩m upd_inv I P TA"
    by(auto intro: ts_inv_ok_inv_ext_upd_inv)
  also from esinv cct have "ts_inv_ok (redT_updT' TS TA) (upd_inv I P TA)"
    by(auto intro: ts_inv_ok_upd_inv')
  with cct have "upd_inv I P TA ⊆⇩m upd_invs (upd_inv I P TA) P TAS"
    by(auto intro: IH)
  finally show ?case by simp
qed

lemma upd_invs_Some:
  "⟦ thread_oks ts tas; I t = ⌊i⌋; ts t = ⌊x⌋ ⟧ ⟹ upd_invs I Q tas t = ⌊i⌋"
proof(induct tas arbitrary: ts I)
  case Nil thus ?case by simp
next
  case (Cons TA TAS TS I)
  note IH = ‹⋀ts I. ⟦thread_oks ts TAS; I t = ⌊i⌋; ts t = ⌊x⌋⟧ ⟹ upd_invs I Q TAS t = ⌊i⌋›
  note cct = ‹thread_oks TS (TA # TAS)›
  note it = ‹I t = ⌊i⌋›
  note est = ‹TS t = ⌊x⌋›
  from cct have cctta: "thread_ok TS TA"
    and ccttas: "thread_oks (redT_updT' TS TA) TAS" by auto
  from cctta it est have "upd_inv I Q TA t = ⌊i⌋"
    by(cases TA, auto)
  moreover
  have "redT_updT' TS TA t = ⌊x⌋" using cctta est
    by - (rule redT_updT'_Some) 
  ultimately have "upd_invs (upd_inv I Q TA) Q TAS t = ⌊i⌋" using ccttas
    by -(erule IH)
  thus ?case by simp
qed

lemma upd_inv_Some_eq:
  "⟦ thread_ok ts ta; ts t = ⌊x⌋ ⟧ ⟹ upd_inv I Q ta t = I t"
by(cases ta, auto)

lemma upd_invs_Some_eq: "⟦ thread_oks ts tas; ts t = ⌊x⌋ ⟧ ⟹ upd_invs I Q tas t = I t"
proof(induct tas arbitrary: ts I)
  case Nil thus ?case by simp
next
  case (Cons TA TAS TS I)
  note IH = ‹⋀ts I. ⟦thread_oks ts TAS; ts t = ⌊x⌋⟧ ⟹ upd_invs I Q TAS t = I t›
  note cct = ‹thread_oks TS (TA # TAS)›
  note est = ‹TS t = ⌊x⌋›
  from cct est have "upd_invs (upd_inv I Q TA) Q TAS t = upd_inv I Q TA t"
    apply(clarsimp)
    apply(erule IH)
    by(rule redT_updT'_Some)
  also from cct est have "… = I t" 
    by(auto elim: upd_inv_Some_eq)
  finally show ?case by simp
qed

lemma SOME_new_thread_upd_invs:
  assumes Qsome: "Q (SOME i. Q i t x m) t x m"
  and nt: "NewThread t x m ∈ set tas"
  and cct: "thread_oks ts tas"
  shows "∃i. upd_invs I Q tas t = ⌊i⌋ ∧ Q i t x m"
proof(rule exI[where x="SOME i. Q i t x m"])
  from nt cct have "upd_invs I Q tas t = ⌊SOME i. Q i t x m⌋"
  proof(induct tas arbitrary: ts I)
    case Nil thus ?case by simp
  next
    case (Cons TA TAS TS I)
    note IH = ‹⋀ts I. ⟦ NewThread t x m ∈ set TAS; thread_oks ts TAS ⟧ ⟹ upd_invs I Q TAS t = ⌊SOME i. Q i t x m⌋›
    note nt = ‹NewThread t x m ∈ set (TA # TAS)›
    note cct = ‹thread_oks TS (TA # TAS)›
    { assume nt': "NewThread t x m ∈ set TAS"
      from cct have ?case
        apply(clarsimp)
        by(rule IH[OF nt']) }
    moreover
    { assume ta: "TA = NewThread t x m"
      with cct have rup: "redT_updT' TS TA t = ⌊(undefined, no_wait_locks)⌋"
        by(simp)
      from cct have cctta: "thread_oks (redT_updT' TS TA) TAS" by simp
      from ta have "upd_inv I Q TA t = ⌊SOME i. Q i t x m⌋"
        by(simp)
      hence ?case 
        by(clarsimp simp add: upd_invs_Some_eq[OF cctta, OF rup]) }
    ultimately show ?case using nt by auto
  qed
  with Qsome show "upd_invs I Q tas t = ⌊SOME i. Q i t x m⌋ ∧ Q (SOME i. Q i t x m) t x m"
    by(simp)
qed

lemma ts_ok_into_ts_inv_const:
  assumes "ts_ok P ts m"
  obtains I where "ts_inv (λ_. P) I ts m"
proof -
  from assms have "ts_inv (λ_. P) (λt. if t ∈ dom ts then Some undefined else None) ts m"
    by(auto intro!: ts_invI dest: ts_okD)
  thus thesis by(rule that)
qed

lemma ts_inv_const_into_ts_ok:
  "ts_inv (λ_. P) I ts m ⟹ ts_ok P ts m"
by(auto intro!: ts_okI dest: ts_invD)

lemma ts_inv_into_ts_ok_Ex:
  "ts_inv Q I ts m ⟹ ts_ok (λt x m. ∃i. Q i t x m) ts m"
by(rule ts_okI)(blast dest: ts_invD)

lemma ts_ok_Ex_into_ts_inv:
  "ts_ok (λt x m. ∃i. Q i t x m) ts m ⟹ ∃I. ts_inv Q I ts m"
by(rule exI[where x="λt. ⌊SOME i. Q i t (fst (the (ts t))) m⌋"])(auto 4 4 dest: ts_okD intro: someI intro: ts_invI)

lemma Ex_ts_inv_conv_ts_ok:
  "(∃I. ts_inv Q I ts m) ⟷ (ts_ok (λt x m. ∃i. Q i t x m) ts m)"
by(auto dest: ts_inv_into_ts_ok_Ex ts_ok_Ex_into_ts_inv)

end