(* Title: JinjaDCI/J/WellType.thy Author: Tobias Nipkow, Susannah Mansky Copyright 2003 Technische Universitaet Muenchen, 2019-20 UIUC Based on the Jinja theory J/WellType.thy by Tobias Nipkow *) section ‹ Well-typedness of Jinja expressions › theory WellType imports "../Common/Objects" Expr begin type_synonym env = "vname ⇀ ty" inductive WT :: "[J_prog,env, expr , ty ] ⇒ bool" ("_,_ ⊢ _ :: _" [51,51,51]50) and WTs :: "[J_prog,env, expr list, ty list] ⇒ bool" ("_,_ ⊢ _ [::] _" [51,51,51]50) for P :: J_prog where WTNew: "is_class P C ⟹ P,E ⊢ new C :: Class C" | WTCast: "⟦ P,E ⊢ e :: Class D; is_class P C; P ⊢ C ≼⇧^{*}D ∨ P ⊢ D ≼⇧^{*}C ⟧ ⟹ P,E ⊢ Cast C e :: Class C" | WTVal: "typeof v = Some T ⟹ P,E ⊢ Val v :: T" | WTVar: "E V = Some T ⟹ P,E ⊢ Var V :: T" | WTBinOpEq: "⟦ P,E ⊢ e⇩_{1}:: T⇩_{1}; P,E ⊢ e⇩_{2}:: T⇩_{2}; P ⊢ T⇩_{1}≤ T⇩_{2}∨ P ⊢ T⇩_{2}≤ T⇩_{1}⟧ ⟹ P,E ⊢ e⇩_{1}«Eq» e⇩_{2}:: Boolean" | WTBinOpAdd: "⟦ P,E ⊢ e⇩_{1}:: Integer; P,E ⊢ e⇩_{2}:: Integer ⟧ ⟹ P,E ⊢ e⇩_{1}«Add» e⇩_{2}:: Integer" | WTLAss: "⟦ E V = Some T; P,E ⊢ e :: T'; P ⊢ T' ≤ T; V ≠ this ⟧ ⟹ P,E ⊢ V:=e :: Void" | WTFAcc: "⟦ P,E ⊢ e :: Class C; P ⊢ C sees F,NonStatic:T in D ⟧ ⟹ P,E ⊢ e∙F{D} :: T" | WTSFAcc: "⟦ P ⊢ C sees F,Static:T in D ⟧ ⟹ P,E ⊢ C∙⇩_{s}F{D} :: T" | WTFAss: "⟦ P,E ⊢ e⇩_{1}:: Class C; P ⊢ C sees F,NonStatic:T in D; P,E ⊢ e⇩_{2}:: T'; P ⊢ T' ≤ T ⟧ ⟹ P,E ⊢ e⇩_{1}∙F{D}:=e⇩_{2}:: Void" | WTSFAss: "⟦ P ⊢ C sees F,Static:T in D; P,E ⊢ e⇩_{2}:: T'; P ⊢ T' ≤ T ⟧ ⟹ P,E ⊢ C∙⇩_{s}F{D}:=e⇩_{2}:: Void" | WTCall: "⟦ P,E ⊢ e :: Class C; P ⊢ C sees M,NonStatic:Ts → T = (pns,body) in D; P,E ⊢ es [::] Ts'; P ⊢ Ts' [≤] Ts ⟧ ⟹ P,E ⊢ e∙M(es) :: T" | WTSCall: "⟦ P ⊢ C sees M,Static:Ts → T = (pns,body) in D; P,E ⊢ es [::] Ts'; P ⊢ Ts' [≤] Ts; M ≠ clinit ⟧ ⟹ P,E ⊢ C∙⇩_{s}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⇩_{1}; P,E ⊢ e⇩_{2}::T⇩_{2}; P ⊢ T⇩_{1}≤ T⇩_{2}∨ P ⊢ T⇩_{2}≤ T⇩_{1}; P ⊢ T⇩_{1}≤ T⇩_{2}⟶ T = T⇩_{2}; P ⊢ T⇩_{2}≤ T⇩_{1}⟶ T = T⇩_{1}⟧ ⟹ 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" | WTTry: "⟦ P,E ⊢ e⇩_{1}:: T; P,E(V ↦ Class C) ⊢ e⇩_{2}:: T; is_class P C ⟧ ⟹ P,E ⊢ try e⇩_{1}catch(C V) e⇩_{2}:: T" ― ‹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)] (*>*) lemma init_nwt [simp]:"¬P,E ⊢ INIT C (Cs,b) ← e :: T" by(auto elim:WT.cases) lemma ri_nwt [simp]:"¬P,E ⊢ RI(C,e);Cs ← e' :: T" by(auto elim:WT.cases) lemma [iff]: "(P,E ⊢ [] [::] Ts) = (Ts = [])" (*<*)by (rule iffI) (auto elim: WTs.cases)(*>*) lemma [iff]: "(P,E ⊢ e#es [::] T#Ts) = (P,E ⊢ e :: T ∧ P,E ⊢ es [::] Ts)" (*<*)by (rule iffI) (auto elim: WTs.cases)(*>*) lemma [iff]: "(P,E ⊢ (e#es) [::] Ts) = (∃U Us. Ts = U#Us ∧ P,E ⊢ e :: U ∧ P,E ⊢ es [::] Us)" (*<*)by (rule iffI) (auto elim: WTs.cases)(*>*) 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})" (*<*) proof(induct es⇩_{1}type:list) case (Cons a list) let ?lhs = "(∃U Us. Ts = U # Us ∧ P,E ⊢ a :: U ∧ (∃Ts⇩_{1}Ts⇩_{2}. Us = Ts⇩_{1}@ Ts⇩_{2}∧ P,E ⊢ list [::] Ts⇩_{1}∧ P,E ⊢ es⇩_{2}[::] Ts⇩_{2}))" let ?rhs = "(∃Ts⇩_{1}Ts⇩_{2}. Ts = Ts⇩_{1}@ Ts⇩_{2}∧ (∃U Us. Ts⇩_{1}= U # Us ∧ P,E ⊢ a :: U ∧ P,E ⊢ list [::] Us) ∧ P,E ⊢ es⇩_{2}[::] Ts⇩_{2})" { assume ?lhs then have ?rhs by (auto intro: Cons_eq_appendI) } moreover { assume ?rhs then have ?lhs by fastforce } ultimately have "?lhs = ?rhs" by(rule iffI) then show ?case by (clarsimp simp: Cons) qed simp (*>*) lemma [iff]: "P,E ⊢ Val v :: T = (typeof v = Some T)" (*<*)proof(rule iffI) qed (auto elim: WT.cases)(*>*) lemma [iff]: "P,E ⊢ Var V :: T = (E V = Some T)" (*<*)proof(rule iffI) qed (auto elim: WT.cases)(*>*) lemma [iff]: "P,E ⊢ e⇩_{1};;e⇩_{2}:: T⇩_{2}= (∃T⇩_{1}. P,E ⊢ e⇩_{1}::T⇩_{1}∧ P,E ⊢ e⇩_{2}::T⇩_{2})" (*<*)proof(rule iffI) qed (auto elim: WT.cases)(*>*) lemma [iff]: "(P,E ⊢ {V:T; e} :: T') = (is_type P T ∧ P,E(V↦T) ⊢ e :: T')" (*<*)proof(rule iffI) qed (auto elim: WT.cases)(*>*) (*<*) inductive_cases WT_elim_cases[elim!]: "P,E ⊢ V :=e :: T" "P,E ⊢ if (e) e⇩_{1}else e⇩_{2}:: T" "P,E ⊢ while (e) c :: T" "P,E ⊢ throw e :: T" "P,E ⊢ try e⇩_{1}catch(C V) e⇩_{2}:: T" "P,E ⊢ Cast D e :: T" "P,E ⊢ a∙F{D} :: T" "P,E ⊢ C∙⇩_{s}F{D} :: T" "P,E ⊢ a∙F{D} := v :: T" "P,E ⊢ C∙⇩_{s}F{D} := v :: T" "P,E ⊢ e⇩_{1}«bop» e⇩_{2}:: T" "P,E ⊢ new C :: T" "P,E ⊢ e∙M(ps) :: T" "P,E ⊢ C∙⇩_{s}M(ps) :: 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)" (*<*) proof(induct rule: WT_WTs_inducts) case WTVar then show ?case by(simp add: map_le_def dom_def) next case WTLAss then show ?case by(force simp:map_le_def) qed fastforce+ (*>*) lemma WT_fv: "P,E ⊢ e :: T ⟹ fv e ⊆ dom E" and "P,E ⊢ es [::] Ts ⟹ fvs es ⊆ dom E" (*<*) proof(induct rule:WT_WTs.inducts) case WTVar then show ?case by fastforce next case WTLAss then show ?case by fastforce next case WTBlock then show ?case by fastforce next case WTTry then show ?case by fastforce qed simp_all (*>*) lemma WT_nsub_RI: "P,E ⊢ e :: T ⟹ ¬sub_RI e" and WTs_nsub_RIs: "P,E ⊢ es [::] Ts ⟹ ¬sub_RIs es" (*<*)proof(induct rule: WT_WTs.inducts) qed(simp_all) end (*>*)