Theory J1WellForm

(*  Title:      JinjaThreads/Compiler/J1WellForm.thy
    Author:     Andreas Lochbihler, Tobias Nipkow
*)

section ‹Well-Formedness of Intermediate Language›

theory J1WellForm imports
  "../J/DefAss"
  J1WellType
begin

subsection‹Well-formedness›

definition wf_J1_mdecl :: "'addr J1_prog ⇒ cname ⇒ 'addr expr1 mdecl ⇒ bool"
where
  "wf_J1_mdecl P C  ≡  λ(M,Ts,T,body).
    (∃T'. P,Class C#Ts ⊢1 body :: T' ∧ P ⊢ T' ≤ T) ∧
    𝒟 body ⌊{..size Ts}⌋ ∧ ℬ body (size Ts + 1) ∧ syncvars body"

lemma wf_J1_mdecl[simp]:
  "wf_J1_mdecl P C (M,Ts,T,body) ≡
    ((∃T'. P,Class C#Ts ⊢1 body :: T' ∧ P ⊢ T' ≤ T) ∧
     𝒟 body ⌊{..size Ts}⌋ ∧ ℬ body (size Ts + 1)) ∧ syncvars body"
by (simp add:wf_J1_mdecl_def)

abbreviation wf_J1_prog :: "'addr J1_prog ⇒ bool"
where "wf_J1_prog == wf_prog wf_J1_mdecl"

end