# Theory CWellForm

```(*  Title:       CoreC++

Author:      Tobias Nipkow, Daniel Wasserrab
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>
*)

section ‹Well-formedness Constraints›

theory CWellForm imports WellForm WWellForm WellTypeRT DefAss begin

definition wf_C_mdecl :: "prog ⇒ cname ⇒ mdecl ⇒ bool" where
"wf_C_mdecl P C ≡  λ(M,Ts,T,(pns,body)).
length Ts = length pns ∧
distinct pns ∧
this ∉ set pns ∧
P,[this↦Class C,pns[↦]Ts] ⊢ body :: T ∧
𝒟 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↦Class C,pns[↦]Ts] ⊢ body :: T ∧
𝒟 body ⌊{this} ∪ set pns⌋)"

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 (erule conjE)+
apply (drule bspec, assumption)
apply simp
apply (erule conjE)+
apply (drule bspec, assumption)
done

lemma wf_mdecl_wwf_mdecl: "wf_C_mdecl P C Md ⟹ wwf_mdecl P C Md"
by(fastforce simp:wwf_mdecl_def dest!:WT_fv)

lemma wf_prog_wwf_prog: "wf_C_prog P ⟹ wwf_prog P"