Theory CWellForm

(*  Title:       CoreC++
    ID:          $Id: CWellForm.thy,v 1.7 2008-06-23 21:24:36 makarius Exp $
    Author:      Tobias Nipkow, Daniel Wasserrab
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>
*)

header {* \isaheader{Well-formedness Constraints} *}

theory CWellForm imports WellForm WWellForm WellTypeRT DefAss begin


constdefs
  wf_C_mdecl :: "prog => cname => mdecl => bool"
  "wf_C_mdecl P C ≡  λ(M,Ts,T,(pns,body)).
  length Ts = length pns ∧
  distinct pns ∧
  this ∉ set pns ∧
  P,[this\<mapsto>Class C,pns[\<mapsto>]Ts] \<turnstile> body :: T ∧
  \<D> body ⌊{this} ∪ set pns⌋"

lemma wf_C_mdecl[simp]:
  "wf_C_mdecl P C (M,Ts,T,pns,body) ≡
  (length Ts = length pns ∧
  distinct pns ∧
  this ∉ set pns ∧
  P,[this\<mapsto>Class C,pns[\<mapsto>]Ts] \<turnstile> body :: T ∧
  \<D> body ⌊{this} ∪ set pns⌋)"
by(simp add:wf_C_mdecl_def)



abbreviation
  wf_C_prog :: "prog => bool" where
  "wf_C_prog ==  wf_prog wf_C_mdecl"

lemma wf_C_prog_wf_C_mdecl:
  "[| wf_C_prog P; (C,Bs,fs,ms) ∈ set P; m ∈ set ms |]
  ==> wf_C_mdecl P C m"

apply (simp add: wf_prog_def)
apply (simp add: wf_cdecl_def)
apply (erule conjE)+
apply (drule bspec, assumption)
apply simp
apply (erule conjE)+
apply (drule bspec, assumption)
apply (simp add: wf_mdecl_def split_beta)
done



lemma wf_mdecl_wwf_mdecl: "wf_C_mdecl P C Md ==> wwf_mdecl P C Md"
by(fastsimp simp:wwf_mdecl_def dest!:WT_fv)


lemma wf_prog_wwf_prog: "wf_C_prog P ==> wwf_prog P"

apply(simp add:wf_prog_def wf_cdecl_def wf_mdecl_def)
apply(fast intro:wf_mdecl_wwf_mdecl)
done



end