Theory JWellForm

(*  Title:      Jinja/J/JWellForm.thy

    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

section ‹Well-formedness Constraints›

theory JWellForm
imports "../Common/WellForm" WWellForm WellType DefAss
begin

definition wf_J_mdecl :: "J_prog ⇒ cname ⇒ J_mb mdecl ⇒ bool"
where
  "wf_J_mdecl P C  ≡  λ(M,Ts,T,(pns,body)).
  length Ts = length pns ∧
  distinct pns ∧
  this ∉ set pns ∧
  (∃T'. P,[this↦Class C,pns[↦]Ts] ⊢ body :: T' ∧ P ⊢ T' ≤ T) ∧
  𝒟 body ⌊{this} ∪ set pns⌋"

lemma wf_J_mdecl[simp]:
  "wf_J_mdecl P C (M,Ts,T,pns,body) ≡
  (length Ts = length pns ∧
  distinct pns ∧
  this ∉ set pns ∧
  (∃T'. P,[this↦Class C,pns[↦]Ts] ⊢ body :: T' ∧ P ⊢ T' ≤ T) ∧
  𝒟 body ⌊{this} ∪ set pns⌋)"
(*<*)by(simp add:wf_J_mdecl_def)(*>*)


abbreviation
  wf_J_prog :: "J_prog ⇒ bool" where
  "wf_J_prog == wf_prog wf_J_mdecl"

lemma wf_J_prog_wf_J_mdecl:
  "⟦ wf_J_prog P; (C, D, fds, mths) ∈ set P; jmdcl ∈ set mths ⟧
  ⟹ wf_J_mdecl P C jmdcl"
(*<*)by(fastforce simp: wf_prog_def wf_cdecl_def wf_mdecl_def)(*>*)


lemma wf_mdecl_wwf_mdecl: "wf_J_mdecl P C Md ⟹ wwf_J_mdecl P C Md"
(*<*)by(fastforce simp:wwf_J_mdecl_def dest!:WT_fv)(*>*)


lemma wf_prog_wwf_prog: "wf_J_prog P ⟹ wwf_J_prog P"
(*<*)
by (simp add:wf_prog_def wf_cdecl_def wf_mdecl_def)
   (fast intro:wf_mdecl_wwf_mdecl)
(*>*)


end