Theory FWLifting

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

header {* \isaheader{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 :: "('x => 'm => bool) => ('l, 't,'x) thread_info => 'm => bool"
where
  "ts_ok P ts m ≡ ∀t. case (ts t) of None => True | ⌊(x, ln)⌋ => P x m"

lemma ts_okI:
  "[| !!t x ln. ts t = ⌊(x, ln)⌋ ==> P 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 x m |] ==> Q |] ==> Q"
by(auto simp add: ts_ok_def)

lemma ts_okD:
  "[| ts_ok P ts m; ts t = ⌊(x, ln)⌋ |] ==> P x m"
by(auto simp add: ts_ok_def)

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

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

text{* Lifting for properites, that also require additional data that does not change during execution *}

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

lemma ts_invI:
  "[| !!t x ln. ts t = ⌊(x, ln)⌋ ==> ∃i. I t = ⌊i⌋ ∧ P i 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 x m) ==> R |] ==> R"
by(auto simp add: ts_inv_def)

lemma ts_invD:
  "[| ts_inv P I ts m; ts t = ⌊(x, ln)⌋ |] ==> ∃i. I t = ⌊i⌋ ∧ P i x m"
by(auto simp add: ts_inv_def)

definition
  inv_ext :: "('t \<rightharpoonup> 'i) => ('t \<rightharpoonup> 'i) => bool" ("_ \<unlhd> _" [51,51] 50)
where
  "I \<unlhd> I'  ≡ (∀t. case I t of None => True | ⌊i⌋ => I' t = ⌊i⌋)"

lemma inv_extI:
  "(!!t i. I t = ⌊i⌋ ==> I' t = ⌊i⌋) ==> I \<unlhd> I'"
by(simp add: inv_ext_def)

lemma inv_extE:
  "[| I \<unlhd> I'; ∀t i. I t = ⌊i⌋ --> I' t = ⌊i⌋ ==> P |] ==> P"
by(simp add: inv_ext_def)

lemma inv_extD:
  "[| I \<unlhd> I'; I t = ⌊i⌋ |] ==> I' t = ⌊i⌋"
by(simp add: inv_ext_def)

lemma inv_ext_refl [iff]:
  fixes I:: "'t \<rightharpoonup> 'i"
  shows "I \<unlhd> I"
by(auto intro: inv_extI)

lemma inv_ext_trans [trans]:
  fixes I :: "'t \<rightharpoonup> 'i"
  shows "[| I \<unlhd> I'; I' \<unlhd> I'' |] ==> I \<unlhd> I''" 
by(auto intro: inv_extI dest: inv_extD)

lemma inv_ext_upd: "I t = None ==> I \<unlhd> I(t := v)"
by(auto intro!: inv_extI)

text {* Wellformedness properties for lifting *}

definition
  ts_inv_ok :: "('l,'t,'x) thread_info => ('t \<rightharpoonup> '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"
apply(clarsimp simp add: ts_inv_ok_def)
done

lemma ts_inv_okI2:
  "(!!t. (∃v. ts t = ⌊v⌋) <-> (∃v. I t = ⌊v⌋)) ==> ts_inv_ok ts I"
apply(force simp add: ts_inv_ok_def)
done

lemma ts_inv_okE:
  "[| ts_inv_ok ts I; ∀t. ts t = None <-> I t = None ==> P |] ==> P"
apply(force simp add: ts_inv_ok_def)
done

lemma ts_inv_okE2:
  "[| ts_inv_ok ts I; ∀t. (∃v. ts t = ⌊v⌋) <-> (∃v. I t = ⌊v⌋) ==> P |] ==> P"
apply(force simp add: ts_inv_ok_def)
done

lemma ts_inv_okD:
  "ts_inv_ok ts I ==> (ts t = None) <-> (I t = None)"
apply(erule ts_inv_okE, blast)
done

lemma ts_inv_okD2:
  "ts_inv_ok ts I ==> (∃v. ts t = ⌊v⌋) <-> (∃v. I t = ⌊v⌋)"
apply(erule ts_inv_okE2, blast)
done

lemma ts_inv_ok_upd_ts:
  "[| ts t = ⌊x⌋; ts_inv_ok ts I |] ==> ts_inv_ok (ts(t \<mapsto> x')) I"
by(auto dest!: ts_inv_okD intro!: ts_inv_okI split: if_splits)


fun upd_inv :: "('t \<rightharpoonup> 'i) => ('i => 'x => 'm => bool) => ('t,'x,'m) new_thread_action => ('t \<rightharpoonup> 'i)"
where
  "upd_inv I P (NewThread t x m) = I(t \<mapsto> SOME i. P i x m)"
| "upd_inv I P _ = I"

fun upd_invs :: "('t \<rightharpoonup> 'i) => ('i => 'x => 'm => bool) => ('t,'x,'m) new_thread_action list => ('t \<rightharpoonup> '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"
apply(induct xs arbitrary: I)
apply(auto)
done

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_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 \<unlhd> upd_inv I P ta"
apply(cases ta, auto intro!: inv_ext_upd dest: ts_inv_okD)
done

lemma ts_inv_ok_inv_ext_upd_invs:
  "[| ts_inv_ok ts I; thread_oks ts tas|]
  ==> I \<unlhd> 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 \<unlhd> upd_invs I P TAS`
  note esinv = `ts_inv_ok TS I`
  note cct = `thread_oks TS (TA # TAS)`
  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 \<unlhd> upd_invs (upd_inv I P TA) P TAS"
    by(auto intro: IH)
  moreover from esinv cct have "I \<unlhd> upd_inv I P TA"
    by(auto intro: ts_inv_ok_inv_ext_upd_inv)
  ultimately show ?case by(auto elim: inv_ext_trans)
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 x m) 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 x m"
proof(rule exI[where x="SOME i. Q i x m"])
  from nt cct have "upd_invs I Q tas t = ⌊SOME i. Q i 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 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 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 x m⌋ ∧ Q (SOME i. Q i x m) x m"
    by(simp)
qed

end