Theory DefAssPreservation

(*  Title:      JinjaThreads/J/DefAssPreservation.thy
    Author:     Andreas Lochbihler, Tobias Nipkow
*)
header {* \isaheader{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 [iff]: "\<D> (extRet2J va) A"
by(cases va) simp_all

lemma blocks_defass [iff]: "!!A. [| length Vs = length Ts; length vs = length Ts|] ==>
 \<D> (blocks (Vs,Ts,vs,e)) A = \<D> e (A \<squnion> ⌊set Vs⌋)"
(*<*)
apply(induct Vs Ts vs e rule:blocks.induct)
apply(simp_all add:hyperset_defs)
done
(*>*)

lemma red_lA_incr: "extTA,P \<turnstile> ⟨e,s⟩ -ta-> ⟨e',s'⟩ ==> ⌊dom (lcl s)⌋ \<squnion> \<A> e \<sqsubseteq>  ⌊dom (lcl s')⌋ \<squnion> \<A> e'"
  and reds_lA_incr: "extTA,P \<turnstile> ⟨es,s⟩ [-ta->] ⟨es',s'⟩ ==> ⌊dom (lcl s)⌋ \<squnion> \<A>s es \<sqsubseteq>  ⌊dom (lcl s')⌋ \<squnion> \<A>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(force split: split_if_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+

text{* Now preservation of definite assignment. *}

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

lemma assumes wf: "wf_J_prog P"
  shows red_preserves_defass: "extTA,P \<turnstile> ⟨e,s⟩ -ta-> ⟨e',s'⟩ ==> \<D> e ⌊dom (lcl s)⌋ ==> \<D> e' ⌊dom (lcl s')⌋"
  and reds_preserves_defass: "extTA,P \<turnstile> ⟨es,s⟩ [-ta->] ⟨es',s'⟩ ==> \<D>s es ⌊dom (lcl s)⌋ ==> \<D>s es' ⌊dom (lcl s')⌋"
proof (induct 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 a s ta a' s' i e)
  have ss: "extTA,P \<turnstile> ⟨a,s⟩ -ta-> ⟨a',s'⟩"
    and IH: "\<D> a ⌊dom (lcl s)⌋ ==> \<D> a' ⌊dom (lcl s')⌋"
    and D: "\<D> (a⌊i⌉ := e) ⌊dom (lcl s)⌋" by fact+
  from D have "\<D> a ⌊dom (lcl s)⌋" by simp
  with IH have Da: "\<D> a' ⌊dom (lcl s')⌋" by simp
  from ss have domgrow: "⌊dom (lcl s)⌋ \<squnion> \<A> a \<sqsubseteq>  ⌊dom (lcl s')⌋ \<squnion> \<A> a'" by - (erule red_lA_incr)
  from D have "\<D> i (⌊dom (lcl s)⌋ \<squnion> \<A> a)" by simp
  with domgrow have Di: "\<D> i (⌊dom (lcl s')⌋ \<squnion> \<A> a')" by - (erule D_mono)
  from domgrow have domgrow2: "⌊dom (lcl s)⌋ \<squnion> \<A> a \<squnion> \<A> i \<sqsubseteq> ⌊dom (lcl s')⌋ \<squnion> \<A> a' \<squnion> \<A> i" by - (rule sqUn_lem)
  from D have "\<D> e (⌊dom (lcl s)⌋ \<squnion> \<A> a \<squnion> \<A> i)" by simp
  with domgrow2 have De: "\<D> e (⌊dom (lcl s')⌋ \<squnion> \<A> a' \<squnion> \<A> i)" by - (erule D_mono)
  from Da Di De show ?case by simp
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 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: split_if_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 (fastsimp 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