Theory DefAssPreservation

(*  Title:      JinjaThreads/J/DefAssPreservation.thy
    Author:     Andreas Lochbihler, Tobias Nipkow
*)

section ‹Preservation of definite assignment›

theory DefAssPreservation
imports
  DefAss
  JWellForm
  SmallStep
begin

text‹Preservation of definite assignment more complex and requires a
few lemmas first.›

lemma D_extRetJ [intro!]: "𝒟 e A ⟹ 𝒟 (extRet2J e va) A"
by(cases va) simp_all

lemma blocks_defass [iff]: "⋀A. ⟦ length Vs = length Ts; length vs = length Ts⟧ ⟹
 𝒟 (blocks Vs Ts vs e) A = 𝒟 e (A ⊔ ⌊set Vs⌋)"
(*<*)
apply(induct Vs Ts vs e rule:blocks.induct)
apply(simp_all add:hyperset_defs)
done
(*>*)

context J_heap_base begin

lemma red_lA_incr: "extTA,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩ ⟹ ⌊dom (lcl s)⌋ ⊔ 𝒜 e ⊑  ⌊dom (lcl s')⌋ ⊔ 𝒜 e'"
  and reds_lA_incr: "extTA,P,t ⊢ ⟨es,s⟩ [-ta→] ⟨es',s'⟩ ⟹ ⌊dom (lcl s)⌋ ⊔ 𝒜s es ⊑  ⌊dom (lcl s')⌋ ⊔ 𝒜s es'"
apply(induct rule:red_reds.inducts)
apply(simp_all del:fun_upd_apply add:hyperset_defs)
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply(force split: if_split_asm)
apply blast
apply blast
apply blast
apply blast
apply blast
apply(blast dest: red_lcl_incr)
apply(blast dest: red_lcl_incr)
by blast+

end

text‹Now preservation of definite assignment.›

declare hyperUn_comm [simp del]
declare hyperUn_leftComm [simp del]

context J_heap_base begin

lemma assumes wf: "wf_J_prog P"
  shows red_preserves_defass: "extTA,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩ ⟹ 𝒟 e ⌊dom (lcl s)⌋ ⟹ 𝒟 e' ⌊dom (lcl s')⌋"
  and reds_preserves_defass: "extTA,P,t ⊢ ⟨es,s⟩ [-ta→] ⟨es',s'⟩ ⟹ 𝒟s es ⌊dom (lcl s)⌋ ⟹ 𝒟s es' ⌊dom (lcl s')⌋"
proof (induction rule:red_reds.inducts)
  case BinOpRed1 thus ?case by (auto elim!: D_mono[OF red_lA_incr])
next
  case AAccRed1 thus ?case by (auto elim!: D_mono[OF red_lA_incr])
next
  case AAssRed1 thus ?case by(auto intro: red_lA_incr sqUn_lem D_mono)
next
  case AAssRed2 thus ?case by (auto elim!: D_mono[OF red_lA_incr])
next
  case FAssRed1 thus ?case by (auto elim!: D_mono[OF red_lA_incr])
next
  case CASRed1 thus ?case by(auto intro: red_lA_incr sqUn_lem D_mono)
next
  case CASRed2 thus ?case by (auto elim!: D_mono[OF red_lA_incr])
next
  case CallObj thus ?case by (auto elim!: Ds_mono[OF red_lA_incr])
next
  case CallParams thus ?case by(auto elim!: Ds_mono[OF red_lA_incr])
next
  case RedCall thus ?case by(auto dest!:sees_wf_mdecl[OF wf] simp:wf_mdecl_def elim!:D_mono')
next
  case BlockRed thus ?case
    by(auto simp:hyperset_defs elim!:D_mono' simp del:fun_upd_apply split: if_split_asm)
next
  case SynchronizedRed1 thus ?case by(auto elim!: D_mono[OF red_lA_incr])
next
  case SeqRed thus ?case by (auto elim!: D_mono[OF red_lA_incr])
next
  case CondRed thus ?case by (auto elim!: D_mono[OF red_lA_incr])
next
  case TryRed thus ?case
    by (fastforce dest:red_lcl_incr intro:D_mono' simp:hyperset_defs)
next
  case RedWhile thus ?case by(auto simp:hyperset_defs elim!:D_mono')
next
  case ListRed1 thus ?case by (auto elim!: Ds_mono[OF red_lA_incr])
qed (auto simp:hyperset_defs)

end

end