Theory WWellForm

(*  Title:      Jinja/J/WWellForm.thy
    ID:         $Id: WWellForm.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

header {* \isaheader{Weak well-formedness of Jinja programs} *}

theory WWellForm = WellForm + Expr:

constdefs
  wwf_J_mdecl :: "J_prog => cname => J_mb mdecl => bool"
  "wwf_J_mdecl P C  ≡  λ(M,Ts,T,(pns,body)).
  length Ts = length pns ∧ distinct pns ∧ this ∉ set pns ∧ fv body ⊆ {this} ∪ set pns"

lemma wwf_J_mdecl[simp]:
  "wwf_J_mdecl P C (M,Ts,T,pns,body) =
  (length Ts = length pns ∧ distinct pns ∧ this ∉ set pns ∧ fv body ⊆ {this} ∪ set pns)"
(*<*)by(simp add:wwf_J_mdecl_def)(*>*)


syntax
  wwf_J_prog :: "J_prog => bool"
translations
  "wwf_J_prog"  ==  "wf_prog wwf_J_mdecl"

end