# Theory JWellForm

```(*  Title:      JinjaThreads/J/JWellForm.thy
Author:     Tobias Nipkow, Andreas Lochbihler
*)

section ‹Well-formedness Constraints›

theory JWellForm
imports
WWellForm
WellType
DefAss
begin

definition wf_J_mdecl :: "'addr J_prog ⇒ cname ⇒ 'addr 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⌋)"

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

lemma wf_mdecl_wwf_mdecl: "wf_J_mdecl P C Md ⟹ wwf_J_mdecl P C Md"
(*<*)
apply(frule WT_fv)
apply(auto)
done

lemma wf_prog_wwf_prog: "wf_J_prog P ⟹ wwf_J_prog P"
by(erule wf_prog_lift)(erule wf_mdecl_wwf_mdecl)

subsection ‹Code generation›

definition typeable_with :: "'addr J_prog ⇒ env ⇒ 'addr expr ⇒ ty ⇒ bool"
where [simp]: "typeable_with P E e T ⟷ (∃T'. P,E ⊢ e ::' T' ∧ P ⊢ T' ≤ T)"

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

definition wf_J_prog' :: "'addr J_prog ⇒ bool"
where "wf_J_prog' = wf_prog wf_J_mdecl'"

lemma wf_J_prog_wf_J_prog':
"wf_J_prog P ⟹ wf_J_prog' P"
unfolding wf_J_prog'_def
apply(erule wf_prog_lift)
apply(drule (1) WT_into_WT_code)
apply(auto simp add: ran_def map_upds_def dest!: map_of_SomeD set_zip_rightD)
done

lemma wf_J_prog'_wf_J_prog:
"wf_J_prog' P ⟹ wf_J_prog P"
unfolding wf_J_prog'_def
apply(erule wf_prog_lift)
apply(drule (1) WT_code_into_WT)
apply(auto simp add: ran_def map_upds_def dest!: map_of_SomeD set_zip_rightD)
done

lemma wf_J_prog_eq_wf_J_prog' [code_unfold]:
"wf_J_prog = wf_J_prog'"
by(blast intro: ext wf_J_prog'_wf_J_prog wf_J_prog_wf_J_prog' del: equalityI)

code_pred
(modes: i ⇒ i ⇒ i ⇒ i ⇒ bool)
[inductify]
typeable_with
.

text ‹Formal code generation test›
ML_val ‹@{code wf_J_prog'}›

end
```