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⌋)"
(*<*)by(simp add:wf_J_mdecl_def)(*>*)


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(clarsimp simp add: wwf_J_mdecl_def)
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(clarsimp simp add: wf_J_mdecl'_def)
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(clarsimp simp add: wf_J_mdecl'_def)
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