# Theory POPLmarkRecordCtxt

(*  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