(* 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(simp add: WTNew) apply(fastforce simp: WTDynCast) apply(fastforce simp: WTStaticCast) apply(fastforce simp: WTVal) apply(simp add: WTVar map_le_def dom_def) 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) apply(simp add: WTNil) apply(simp add: WTCons) 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