# Theory JWellForm

```(*  Title:      JinjaDCI/J/JWellForm.thy

Author:     Tobias Nipkow, Susannah Mansky
Copyright   2003 Technische Universitaet Muenchen, 2019-20 UIUC

Based on the Jinja theory J/JWellForm.thy by Tobias Nipkow
*)

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,b,Ts,T,(pns,body)).
length Ts = length pns ∧
distinct pns ∧
¬sub_RI body ∧
(case b of
NonStatic ⇒ this ∉ set pns ∧
(∃T'. P,[this↦Class C,pns[↦]Ts] ⊢ body :: T' ∧ P ⊢ T' ≤ T) ∧
𝒟 body ⌊{this} ∪ set pns⌋
| Static ⇒ (∃T'. P,[pns[↦]Ts] ⊢ body :: T' ∧ P ⊢ T' ≤ T) ∧
𝒟 body ⌊set pns⌋)"

lemma wf_J_mdecl_NonStatic[simp]:
"wf_J_mdecl P C (M,NonStatic,Ts,T,pns,body) ≡
(length Ts = length pns ∧
distinct pns ∧
¬sub_RI body ∧
this ∉ set pns ∧
(∃T'. P,[this↦Class C,pns[↦]Ts] ⊢ body :: T' ∧ P ⊢ T' ≤ T) ∧
𝒟 body ⌊{this} ∪ set pns⌋)"

lemma wf_J_mdecl_Static[simp]:
"wf_J_mdecl P C (M,Static,Ts,T,pns,body) ≡
(length Ts = length pns ∧
distinct pns ∧
¬sub_RI body ∧
(∃T'. P,[pns[↦]Ts] ⊢ body :: T' ∧ P ⊢ T' ≤ T) ∧
𝒟 body ⌊set pns⌋)"

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"
(*<*)
proof -
obtain M b Ts T pns body where "Md = (M, b, Ts, T, pns, body)" by(cases Md) simp
then show "wf_J_mdecl P C Md ⟹ wwf_J_mdecl P C Md"
by(case_tac b) (fastforce simp:wwf_J_mdecl_def dest!:WT_fv)+
qed
(*>*)

lemma wf_prog_wwf_prog: "wf_J_prog P ⟹ wwf_J_prog P"
(*<*)