# Theory WellType

```(*  Title:       CoreC++

Author:      Daniel Wasserrab
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

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

section ‹Well-typedness of CoreC++ expressions›

theory WellType imports Syntax TypeRel begin

subsection ‹The rules›

inductive
WT :: "[prog,env,expr     ,ty     ] ⇒ bool"
("_,_ ⊢ _ :: _"   [51,51,51]50)
and WTs :: "[prog,env,expr list,ty list] ⇒ bool"
("_,_ ⊢ _ [::] _" [51,51,51]50)
for P :: prog
where

WTNew:
"is_class P C ⟹
P,E ⊢ new C :: Class C"

| WTDynCast: (* not more than one path between classes *)
"⟦P,E ⊢ e :: Class D; is_class P C;
P ⊢ Path D to C unique ∨ (∀Cs. ¬ P ⊢ Path D to C via Cs)⟧
⟹ P,E ⊢ Cast C e :: Class C"

| WTStaticCast:
"⟦P,E ⊢ e :: Class D; is_class P C;
P ⊢ Path D to C unique ∨
(P ⊢ C ≼⇧* D ∧ (∀Cs. P ⊢ Path C to D via Cs ⟶ Subobjs⇩R P C Cs)) ⟧
⟹ P,E ⊢ ⦇C⦈e :: Class C"

| WTVal:
"typeof v = Some T ⟹
P,E ⊢ Val v :: T"

| WTVar:
"E V = Some T ⟹
P,E ⊢ Var V :: T"

| WTBinOp:
"⟦ P,E ⊢ e⇩1 :: T⇩1;  P,E ⊢ e⇩2 :: T⇩2;
case bop of Eq ⇒ T⇩1 = T⇩2 ∧ T = Boolean
| Add ⇒ T⇩1 = Integer ∧ T⇩2 = Integer ∧ T = Integer ⟧
⟹ P,E ⊢ e⇩1 «bop» e⇩2 :: T"

| WTLAss:
"⟦ E V = Some T;  P,E ⊢ e :: T'; P ⊢ T' ≤ T⟧
⟹ P,E ⊢ V:=e :: T"

| WTFAcc:
"⟦ P,E ⊢ e :: Class C;  P ⊢ C has least F:T via Cs⟧
⟹ P,E ⊢ e∙F{Cs} :: T"

| WTFAss:
"⟦ P,E ⊢ e⇩1 :: Class C;  P ⊢ C has least F:T via Cs;
P,E ⊢ e⇩2 :: T'; P ⊢ T' ≤ T⟧
⟹ P,E ⊢ e⇩1∙F{Cs}:=e⇩2 :: T"

| WTStaticCall:
"⟦ P,E ⊢ e :: Class C'; P ⊢ Path C' to C unique;
P ⊢ C has least M = (Ts,T,m) via Cs; P,E ⊢ es [::] Ts'; P ⊢ Ts' [≤] Ts ⟧
⟹ P,E ⊢ e∙(C::)M(es) :: T"

| WTCall:
"⟦ P,E ⊢ e :: Class C;  P ⊢ C has least M = (Ts,T,m) via Cs;
P,E ⊢ es [::] Ts'; P ⊢ Ts' [≤] Ts ⟧
⟹ P,E ⊢ e∙M(es) :: T"

| WTBlock:
"⟦ is_type P T;  P,E(V ↦ T) ⊢ e :: T' ⟧
⟹  P,E ⊢ {V:T; e} :: T'"

| WTSeq:
"⟦ P,E ⊢ e⇩1::T⇩1;  P,E ⊢ e⇩2::T⇩2 ⟧
⟹  P,E ⊢ e⇩1;;e⇩2 :: T⇩2"

| WTCond:
"⟦ P,E ⊢ e :: Boolean;  P,E ⊢ e⇩1::T;  P,E ⊢ e⇩2::T ⟧
⟹ P,E ⊢ if (e) e⇩1 else e⇩2 :: T"

| WTWhile:
"⟦ P,E ⊢ e :: Boolean;  P,E ⊢ c::T ⟧
⟹ P,E ⊢ while (e) c :: Void"

| WTThrow:
"P,E ⊢ e :: Class C  ⟹
P,E ⊢ throw e :: Void"

― ‹well-typed expression lists›

| WTNil:
"P,E ⊢ [] [::] []"

| WTCons:
"⟦ P,E ⊢ e :: T;  P,E ⊢ es [::] Ts ⟧
⟹  P,E ⊢ e#es [::] T#Ts"

declare WT_WTs.intros[intro!] WTNil[iff]

lemmas WT_WTs_induct = WT_WTs.induct [split_format (complete)]
and WT_WTs_inducts = WT_WTs.inducts [split_format (complete)]

subsection‹Easy consequences›

lemma [iff]: "(P,E ⊢ [] [::] Ts) = (Ts = [])"

apply(rule iffI)
apply (auto elim: WTs.cases)
done

lemma [iff]: "(P,E ⊢ e#es [::] T#Ts) = (P,E ⊢ e :: T ∧ P,E ⊢ es [::] Ts)"

apply(rule iffI)
apply (auto elim: WTs.cases)
done

lemma [iff]: "(P,E ⊢ (e#es) [::] Ts) =
(∃U Us. Ts = U#Us ∧ P,E ⊢ e :: U ∧ P,E ⊢ es [::] Us)"

apply(rule iffI)
apply (auto elim: WTs.cases)
done

lemma [iff]: "⋀Ts. (P,E ⊢ es⇩1 @ es⇩2 [::] Ts) =
(∃Ts⇩1 Ts⇩2. Ts = Ts⇩1 @ Ts⇩2 ∧ P,E ⊢ es⇩1 [::] Ts⇩1 ∧ P,E ⊢ es⇩2[::]Ts⇩2)"

apply(induct es⇩1 type:list)
apply simp
apply clarsimp
apply(erule thin_rl)
apply (rule iffI)
apply clarsimp
apply(rule exI)+
apply(rule conjI)
prefer 2 apply blast
apply simp
apply fastforce
done

lemma [iff]: "P,E ⊢ Val v :: T = (typeof v = Some T)"

apply(rule iffI)
apply (auto elim: WT.cases)
done

lemma [iff]: "P,E ⊢ Var V :: T = (E V = Some T)"

apply(rule iffI)
apply (auto elim: WT.cases)
done

lemma [iff]: "P,E ⊢ e⇩1;;e⇩2 :: T⇩2 = (∃T⇩1. P,E ⊢ e⇩1::T⇩1 ∧ P,E ⊢ e⇩2::T⇩2)"

apply(rule iffI)
apply (auto elim: WT.cases)
done

lemma [iff]: "(P,E ⊢ {V:T; e} :: T') = (is_type P T ∧ P,E(V↦T) ⊢ e :: T')"

apply(rule iffI)
apply (auto elim: WT.cases)
done

inductive_cases WT_elim_cases[elim!]:
"P,E ⊢ new C :: T"
"P,E ⊢ Cast C e :: T"
"P,E ⊢ ⦇C⦈e :: T"
"P,E ⊢ e⇩1 «bop» e⇩2 :: T"
"P,E ⊢ V:= e :: T"
"P,E ⊢ e∙F{Cs} :: T"
"P,E ⊢ e∙F{Cs} := v :: T"
"P,E ⊢ e∙M(ps) :: T"
"P,E ⊢ e∙(C::)M(ps) :: T"
"P,E ⊢ if (e) e⇩1 else e⇩2 :: T"
"P,E ⊢ while (e) c :: T"
"P,E ⊢ throw e :: T"

lemma wt_env_mono:
"P,E ⊢ e :: T ⟹ (⋀E'. E ⊆⇩m E' ⟹ P,E' ⊢ e :: T)" and
"P,E ⊢ es [::] Ts ⟹ (⋀E'. E ⊆⇩m E' ⟹ P,E' ⊢ es [::] Ts)"

apply(induct rule: WT_WTs_inducts)
apply(fastforce simp: WTDynCast)
apply(fastforce simp: WTStaticCast)
apply(fastforce simp: WTVal)
apply(fastforce simp: WTBinOp)
apply(force simp:map_le_def)
apply(fastforce simp: WTFAcc)
apply(fastforce simp: WTFAss)
apply(fastforce simp: WTCall)
apply(fastforce simp: WTStaticCall)
apply(fastforce simp: map_le_def WTBlock)
apply(fastforce simp: WTSeq)
apply(fastforce simp: WTCond)
apply(fastforce simp: WTWhile)
apply(fastforce simp: WTThrow)
done

lemma WT_fv: "P,E ⊢ e :: T ⟹ fv e ⊆ dom E"
and "P,E ⊢ es [::] Ts ⟹ fvs es ⊆ dom E"

apply(induct rule:WT_WTs.inducts)
apply(simp_all del: fun_upd_apply)
apply fast+
done

end
```