(* Title: POPLmark/POPLmarkRecordCtxt.thy Author: Stefan Berghofer, TU Muenchen, 2005 *) theory POPLmarkRecordCtxt imports POPLmarkRecord begin section ‹Evaluation contexts› text ‹ \label{sec:evaluation-ctxt} In this section, we present a different way of formalizing the evaluation relation. Rather than using additional congruence rules, we first formalize a set ‹ctxt› of evaluation contexts, describing the locations in a term where reductions can occur. We have chosen a higher-order formalization of evaluation contexts as functions from terms to terms. We define simultaneously a set ‹rctxt› of evaluation contexts for records represented as functions from terms to lists of fields. › inductive_set ctxt :: "(trm ⇒ trm) set" and rctxt :: "(trm ⇒ rcd) set" where C_Hole: "(λt. t) ∈ ctxt" | C_App1: "E ∈ ctxt ⟹ (λt. E t ∙ u) ∈ ctxt" | C_App2: "v ∈ value ⟹ E ∈ ctxt ⟹ (λt. v ∙ E t) ∈ ctxt" | C_TApp: "E ∈ ctxt ⟹ (λt. E t ∙⇩_{τ}T) ∈ ctxt" | C_Proj: "E ∈ ctxt ⟹ (λt. E t..l) ∈ ctxt" | C_Rcd: "E ∈ rctxt ⟹ (λt. Rcd (E t)) ∈ ctxt" | C_Let: "E ∈ ctxt ⟹ (λt. LET p = E t IN u) ∈ ctxt" | C_hd: "E ∈ ctxt ⟹ (λt. (l, E t) ∷ fs) ∈ rctxt" | C_tl: "v ∈ value ⟹ E ∈ rctxt ⟹ (λt. (l, v) ∷ E t) ∈ rctxt" lemmas rctxt_induct = ctxt_rctxt.inducts(2) [of _ "λx. True", simplified True_simps, consumes 1, case_names C_hd C_tl] lemma rctxt_labels: assumes H: "E ∈ rctxt" shows "E t⟨l⟩⇩_{?}= ⊥ ⟹ E t'⟨l⟩⇩_{?}= ⊥" using H by (induct rule: rctxt_induct) auto text ‹ The evaluation relation ‹t ⟼⇩_{c}t'› is now characterized by the rule ‹E_Ctxt›, which allows reductions in arbitrary contexts, as well as the rules ‹E_Abs›, ‹E_TAbs›, ‹E_LetV›, and ‹E_ProjRcd› describing the ``immediate'' reductions, which have already been presented in \secref{sec:evaluation} and \secref{sec:evaluation-rcd}. › inductive eval :: "trm ⇒ trm ⇒ bool" (infixl "⟼⇩_{c}" 50) where E_Ctxt: "t ⟼⇩_{c}t' ⟹ E ∈ ctxt ⟹ E t ⟼⇩_{c}E t'" | E_Abs: "v⇩_{2}∈ value ⟹ (λ:T⇩_{1}⇩_{1}. t⇩_{1}⇩_{2}) ∙ v⇩_{2}⟼⇩_{c}t⇩_{1}⇩_{2}[0 ↦ v⇩_{2}]" | E_TAbs: "(λ<:T⇩_{1}⇩_{1}. t⇩_{1}⇩_{2}) ∙⇩_{τ}T⇩_{2}⟼⇩_{c}t⇩_{1}⇩_{2}[0 ↦⇩_{τ}T⇩_{2}]" | E_LetV: "v ∈ value ⟹ ⊢ p ⊳ v ⇒ ts ⟹ (LET p = v IN t) ⟼⇩_{c}t[0 ↦⇩_{s}ts]" | E_ProjRcd: "fs⟨l⟩⇩_{?}= ⌊v⌋ ⟹ v ∈ value ⟹ Rcd fs..l ⟼⇩_{c}v" text ‹ In the proof of the preservation theorem, the case corresponding to the rule ‹E_Ctxt› requires a lemma stating that replacing a term @{term t} in a well-typed term of the form @{term "E t"}, where @{term E} is a context, by a term @{term t'} of the same type does not change the type of the resulting term @{term "E t'"}. The proof is by mutual induction on the typing derivations for terms and records. › lemma context_typing: ― ‹A.18› "Γ ⊢ u : T ⟹ E ∈ ctxt ⟹ u = E t ⟹ (⋀T⇩_{0}. Γ ⊢ t : T⇩_{0}⟹ Γ ⊢ t' : T⇩_{0}) ⟹ Γ ⊢ E t' : T" "Γ ⊢ fs [:] fTs ⟹ E⇩_{r}∈ rctxt ⟹ fs = E⇩_{r}t ⟹ (⋀T⇩_{0}. Γ ⊢ t : T⇩_{0}⟹ Γ ⊢ t' : T⇩_{0}) ⟹ Γ ⊢ E⇩_{r}t' [:] fTs" proof (induct arbitrary: E t t' and E⇩_{r}t t' set: typing typings) case (T_Var Γ i U T E t t') from ‹E ∈ ctxt› have "E = (λt. t)" using T_Var by cases simp_all with T_Var show ?case by (blast intro: typing_typings.intros) next case (T_Abs T⇩_{1}T⇩_{2}Γ t⇩_{2}E t t') from ‹E ∈ ctxt› have "E = (λt. t)" using T_Abs by cases simp_all with T_Abs show ?case by (blast intro: typing_typings.intros) next case (T_App Γ t⇩_{1}T⇩_{1}⇩_{1}T⇩_{1}⇩_{2}t⇩_{2}E t t') from ‹E ∈ ctxt› show ?case using T_App by cases (simp_all, (blast intro: typing_typings.intros)+) next case (T_TAbs T⇩_{1}Γ t⇩_{2}T⇩_{2}E t t') from ‹E ∈ ctxt› have "E = (λt. t)" using T_TAbs by cases simp_all with T_TAbs show ?case by (blast intro: typing_typings.intros) next case (T_TApp Γ t⇩_{1}T⇩_{1}⇩_{1}T⇩_{1}⇩_{2}T⇩_{2}E t t') from ‹E ∈ ctxt› show ?case using T_TApp by cases (simp_all, (blast intro: typing_typings.intros)+) next case (T_Sub Γ t S T E ta t') thus ?case by (blast intro: typing_typings.intros) next case (T_Let Γ t⇩_{1}T⇩_{1}p Δ t⇩_{2}T⇩_{2}E t t') from ‹E ∈ ctxt› show ?case using T_Let by cases (simp_all, (blast intro: typing_typings.intros)+) next case (T_Rcd Γ fs fTs E t t') from ‹E ∈ ctxt› show ?case using T_Rcd by cases (simp_all, (blast intro: typing_typings.intros)+) next case (T_Proj Γ t fTs l T E ta t') from ‹E ∈ ctxt› show ?case using T_Proj by cases (simp_all, (blast intro: typing_typings.intros)+) next case (T_Nil Γ E t t') from ‹E ∈ rctxt› show ?case using T_Nil by cases simp_all next case (T_Cons Γ t T fs fTs l E ta t') from ‹E ∈ rctxt› show ?case using T_Cons by cases (blast intro: typing_typings.intros rctxt_labels)+ qed text ‹ The fact that immediate reduction preserves the types of terms is proved in several parts. The proof of each statement is by induction on the typing derivation. › theorem Abs_preservation: ― ‹A.19(1)› assumes H: "Γ ⊢ (λ:T⇩_{1}⇩_{1}. t⇩_{1}⇩_{2}) ∙ t⇩_{2}: T" shows "Γ ⊢ t⇩_{1}⇩_{2}[0 ↦ t⇩_{2}] : T" using H proof (induct Γ "(λ:T⇩_{1}⇩_{1}. t⇩_{1}⇩_{2}) ∙ t⇩_{2}" T arbitrary: T⇩_{1}⇩_{1}t⇩_{1}⇩_{2}t⇩_{2}rule: typing_induct) case (T_App Γ T⇩_{1}⇩_{1}T⇩_{1}⇩_{2}t⇩_{2}T⇩_{1}⇩_{1}' t⇩_{1}⇩_{2}) from ‹Γ ⊢ (λ:T⇩_{1}⇩_{1}'. t⇩_{1}⇩_{2}) : T⇩_{1}⇩_{1}→ T⇩_{1}⇩_{2}› obtain S' where T⇩_{1}⇩_{1}: "Γ ⊢ T⇩_{1}⇩_{1}<: T⇩_{1}⇩_{1}'" and t⇩_{1}⇩_{2}: "VarB T⇩_{1}⇩_{1}' ∷ Γ ⊢ t⇩_{1}⇩_{2}: S'" and S': "Γ ⊢ S'[0 ↦⇩_{τ}Top]⇩_{τ}<: T⇩_{1}⇩_{2}" by (rule Abs_type' [simplified]) blast from ‹Γ ⊢ t⇩_{2}: T⇩_{1}⇩_{1}› have "Γ ⊢ t⇩_{2}: T⇩_{1}⇩_{1}'" using T⇩_{1}⇩_{1}by (rule T_Sub) with t⇩_{1}⇩_{2}have "Γ ⊢ t⇩_{1}⇩_{2}[0 ↦ t⇩_{2}] : S'[0 ↦⇩_{τ}Top]⇩_{τ}" by (rule subst_type [where Δ="[]", simplified]) then show ?case using S' by (rule T_Sub) next case T_Sub thus ?case by (blast intro: typing_typings.intros) qed theorem TAbs_preservation: ― ‹A.19(2)› assumes H: "Γ ⊢ (λ<:T⇩_{1}⇩_{1}. t⇩_{1}⇩_{2}) ∙⇩_{τ}T⇩_{2}: T" shows "Γ ⊢ t⇩_{1}⇩_{2}[0 ↦⇩_{τ}T⇩_{2}] : T" using H proof (induct Γ "(λ<:T⇩_{1}⇩_{1}. t⇩_{1}⇩_{2}) ∙⇩_{τ}T⇩_{2}" T arbitrary: T⇩_{1}⇩_{1}t⇩_{1}⇩_{2}T⇩_{2}rule: typing_induct) case (T_TApp Γ T⇩_{1}⇩_{1}T⇩_{1}⇩_{2}T⇩_{2}T⇩_{1}⇩_{1}' t⇩_{1}⇩_{2}) from ‹Γ ⊢ (λ<:T⇩_{1}⇩_{1}'. t⇩_{1}⇩_{2}) : (∀<:T⇩_{1}⇩_{1}. T⇩_{1}⇩_{2})› obtain S' where "TVarB T⇩_{1}⇩_{1}∷ Γ ⊢ t⇩_{1}⇩_{2}: S'" and "TVarB T⇩_{1}⇩_{1}∷ Γ ⊢ S' <: T⇩_{1}⇩_{2}" by (rule TAbs_type') blast hence "TVarB T⇩_{1}⇩_{1}∷ Γ ⊢ t⇩_{1}⇩_{2}: T⇩_{1}⇩_{2}" by (rule T_Sub) then show ?case using ‹Γ ⊢ T⇩_{2}<: T⇩_{1}⇩_{1}› by (rule substT_type [where Δ="[]", simplified]) next case T_Sub thus ?case by (blast intro: typing_typings.intros) qed theorem Let_preservation: ― ‹A.19(3)› assumes H: "Γ ⊢ (LET p = t⇩_{1}IN t⇩_{2}) : T" shows "⊢ p ⊳ t⇩_{1}⇒ ts ⟹ Γ ⊢ t⇩_{2}[0 ↦⇩_{s}ts] : T" using H proof (induct Γ "LET p = t⇩_{1}IN t⇩_{2}" T arbitrary: p t⇩_{1}t⇩_{2}ts rule: typing_induct) case (T_Let Γ t⇩_{1}T⇩_{1}p Δ t⇩_{2}T⇩_{2}ts) from ‹⊢ p : T⇩_{1}⇒ Δ› ‹Γ ⊢ t⇩_{1}: T⇩_{1}› ‹Δ @ Γ ⊢ t⇩_{2}: T⇩_{2}› ‹⊢ p ⊳ t⇩_{1}⇒ ts› show ?case by (rule match_type(1) [of _ _ _ _ _ "[]", simplified]) next case T_Sub thus ?case by (blast intro: typing_typings.intros) qed theorem Proj_preservation: ― ‹A.19(4)› assumes H: "Γ ⊢ Rcd fs..l : T" shows "fs⟨l⟩⇩_{?}= ⌊v⌋ ⟹ Γ ⊢ v : T" using H proof (induct Γ "Rcd fs..l" T arbitrary: fs l v rule: typing_induct) case (T_Proj Γ fTs l T fs v) from ‹Γ ⊢ Rcd fs : RcdT fTs› have "∀(l, U)∈set fTs. ∃u. fs⟨l⟩⇩_{?}= ⌊u⌋ ∧ Γ ⊢ u : U" by (rule Rcd_type1') with T_Proj show ?case by (fastforce dest: assoc_set) next case T_Sub thus ?case by (blast intro: typing_typings.intros) qed theorem preservation: ― ‹A.20› assumes H: "t ⟼⇩_{c}t'" shows "Γ ⊢ t : T ⟹ Γ ⊢ t' : T" using H proof (induct arbitrary: Γ T) case (E_Ctxt t t' E Γ T) from E_Ctxt(4,3) refl E_Ctxt(2) show ?case by (rule context_typing) next case (E_Abs v⇩_{2}T⇩_{1}⇩_{1}t⇩_{1}⇩_{2}Γ T) from E_Abs(2) show ?case by (rule Abs_preservation) next case (E_TAbs T⇩_{1}⇩_{1}t⇩_{1}⇩_{2}T⇩_{2}Γ T) thus ?case by (rule TAbs_preservation) next case (E_LetV v p ts t Γ T) from E_LetV(3,2) show ?case by (rule Let_preservation) next case (E_ProjRcd fs l v Γ T) from E_ProjRcd(3,1) show ?case by (rule Proj_preservation) qed text ‹ For the proof of the progress theorem, we need a lemma stating that each well-typed, closed term @{term t} is either a canonical value, or can be decomposed into an evaluation context @{term E} and a term @{term "t⇩_{0}"} such that @{term "t⇩_{0}"} is a redex. The proof of this result, which is called the {\it decomposition lemma}, is again by induction on the typing derivation. A similar property is also needed for records. › theorem context_decomp: ― ‹A.15› "[] ⊢ t : T ⟹ t ∈ value ∨ (∃E t⇩_{0}t⇩_{0}'. E ∈ ctxt ∧ t = E t⇩_{0}∧ t⇩_{0}⟼⇩_{c}t⇩_{0}')" "[] ⊢ fs [:] fTs ⟹ (∀(l, t) ∈ set fs. t ∈ value) ∨ (∃E t⇩_{0}t⇩_{0}'. E ∈ rctxt ∧ fs = E t⇩_{0}∧ t⇩_{0}⟼⇩_{c}t⇩_{0}')" proof (induct "[]::env" t T and "[]::env" fs fTs set: typing typings) case T_Var thus ?case by simp next case T_Abs from value.Abs show ?case .. next case (T_App t⇩_{1}T⇩_{1}⇩_{1}T⇩_{1}⇩_{2}t⇩_{2}) from ‹t⇩_{1}∈ value ∨ (∃E t⇩_{0}t⇩_{0}'. E ∈ ctxt ∧ t⇩_{1}= E t⇩_{0}∧ t⇩_{0}⟼⇩_{c}t⇩_{0}')› show ?case proof assume t⇩_{1}_val: "t⇩_{1}∈ value" with T_App obtain t S where t⇩_{1}: "t⇩_{1}= (λ:S. t)" by (auto dest!: Fun_canonical) from ‹t⇩_{2}∈ value ∨ (∃E t⇩_{0}t⇩_{0}'. E ∈ ctxt ∧ t⇩_{2}= E t⇩_{0}∧ t⇩_{0}⟼⇩_{c}t⇩_{0}')› show ?thesis proof assume "t⇩_{2}∈ value" with t⇩_{1}have "t⇩_{1}∙ t⇩_{2}⟼⇩_{c}t[0 ↦ t⇩_{2}]" by simp (rule eval.intros) thus ?thesis by (iprover intro: C_Hole) next assume "∃E t⇩_{0}t⇩_{0}'. E ∈ ctxt ∧ t⇩_{2}= E t⇩_{0}∧ t⇩_{0}⟼⇩_{c}t⇩_{0}'" with t⇩_{1}_val show ?thesis by (iprover intro: ctxt_rctxt.intros) qed next assume "∃E t⇩_{0}t⇩_{0}'. E ∈ ctxt ∧ t⇩_{1}= E t⇩_{0}∧ t⇩_{0}⟼⇩_{c}t⇩_{0}'" thus ?thesis by (iprover intro: ctxt_rctxt.intros) qed next case T_TAbs from value.TAbs show ?case .. next case (T_TApp t⇩_{1}T⇩_{1}⇩_{1}T⇩_{1}⇩_{2}T⇩_{2}) from ‹t⇩_{1}∈ value ∨ (∃E t⇩_{0}t⇩_{0}'. E ∈ ctxt ∧ t⇩_{1}= E t⇩_{0}∧ t⇩_{0}⟼⇩_{c}t⇩_{0}')› show ?case proof assume "t⇩_{1}∈ value" with T_TApp obtain t S where "t⇩_{1}= (λ<:S. t)" by (auto dest!: TyAll_canonical) hence "t⇩_{1}∙⇩_{τ}T⇩_{2}⟼⇩_{c}t[0 ↦⇩_{τ}T⇩_{2}]" by simp (rule eval.intros) thus ?thesis by (iprover intro: C_Hole) next assume "∃E t⇩_{0}t⇩_{0}'. E ∈ ctxt ∧ t⇩_{1}= E t⇩_{0}∧ t⇩_{0}⟼⇩_{c}t⇩_{0}'" thus ?thesis by (iprover intro: ctxt_rctxt.intros) qed next case (T_Sub t S T) show ?case by (rule T_Sub) next case (T_Let t⇩_{1}T⇩_{1}p Δ t⇩_{2}T⇩_{2}) from ‹t⇩_{1}∈ value ∨ (∃E t⇩_{0}t⇩_{0}'. E ∈ ctxt ∧ t⇩_{1}= E t⇩_{0}∧ t⇩_{0}⟼⇩_{c}t⇩_{0}')› show ?case proof assume t⇩_{1}: "t⇩_{1}∈ value" with T_Let have "∃ts. ⊢ p ⊳ t⇩_{1}⇒ ts" by (auto intro: ptyping_match) with t⇩_{1}show ?thesis by (iprover intro: eval.intros C_Hole) next assume "∃E t⇩_{0}t⇩_{0}'. E ∈ ctxt ∧ t⇩_{1}= E t⇩_{0}∧ t⇩_{0}⟼⇩_{c}t⇩_{0}'" thus ?thesis by (iprover intro: ctxt_rctxt.intros) qed next case (T_Rcd fs fTs) thus ?case by (blast intro: value.intros eval.intros ctxt_rctxt.intros) next case (T_Proj t fTs l T) from ‹t ∈ value ∨ (∃E t⇩_{0}t⇩_{0}'. E ∈ ctxt ∧ t = E t⇩_{0}∧ t⇩_{0}⟼⇩_{c}t⇩_{0}')› show ?case proof assume tv: "t ∈ value" with T_Proj obtain fs where t: "t = Rcd fs" and fs: "∀(l, t) ∈ set fs. t ∈ value" by (auto dest: RcdT_canonical) with T_Proj have "[] ⊢ Rcd fs : RcdT fTs" by simp hence "∀(l, U)∈set fTs. ∃u. fs⟨l⟩⇩_{?}= ⌊u⌋ ∧ [] ⊢ u : U" by (rule Rcd_type1') with T_Proj obtain u where u: "fs⟨l⟩⇩_{?}= ⌊u⌋" by (blast dest: assoc_set) with fs have "u ∈ value" by (blast dest: assoc_set) with u t show ?thesis by (iprover intro: eval.intros C_Hole) next assume "∃E t⇩_{0}t⇩_{0}'. E ∈ ctxt ∧ t = E t⇩_{0}∧ t⇩_{0}⟼⇩_{c}t⇩_{0}'" thus ?case by (iprover intro: ctxt_rctxt.intros) qed next case T_Nil show ?case by simp next case (T_Cons t T fs fTs l) thus ?case by (auto intro: ctxt_rctxt.intros) qed theorem progress: ― ‹A.16› assumes H: "[] ⊢ t : T" shows "t ∈ value ∨ (∃t'. t ⟼⇩_{c}t')" proof - from H have "t ∈ value ∨ (∃E t⇩_{0}t⇩_{0}'. E ∈ ctxt ∧ t = E t⇩_{0}∧ t⇩_{0}⟼⇩_{c}t⇩_{0}')" by (rule context_decomp) thus ?thesis by (iprover intro: eval.intros) qed text ‹ Finally, we prove that the two definitions of the evaluation relation are equivalent. The proof that @{term "t ⟼⇩_{c}t'"} implies @{term "t ⟼ t'"} requires a lemma stating that ‹⟼› is compatible with evaluation contexts. › lemma ctxt_imp_eval: "E ∈ ctxt ⟹ t ⟼ t' ⟹ E t ⟼ E t'" "E⇩_{r}∈ rctxt ⟹ t ⟼ t' ⟹ E⇩_{r}t [⟼] E⇩_{r}t'" by (induct rule: ctxt_rctxt.inducts) (auto intro: eval_evals.intros) lemma eval_evalc_eq: "(t ⟼ t') = (t ⟼⇩_{c}t')" proof fix ts ts' have r: "t ⟼ t' ⟹ t ⟼⇩_{c}t'" and "ts [⟼] ts' ⟹ ∃E t t'. E ∈ rctxt ∧ ts = E t ∧ ts' = E t' ∧ t ⟼⇩_{c}t'" by (induct rule: eval_evals.inducts) (iprover intro: ctxt_rctxt.intros eval.intros)+ assume "t ⟼ t'" thus "t ⟼⇩_{c}t'" by (rule r) next assume "t ⟼⇩_{c}t'" thus "t ⟼ t'" by induct (auto intro: eval_evals.intros ctxt_imp_eval) qed end