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: "v2 ∈ value ⟹ (λ:T11. t12) ∙ v2 ⟼c t12[0 ↦ v2]"
| E_TAbs: "(λ<:T11. t12) ∙τ T2 ⟼c t12[0 ↦τ T2]"
| 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 ⟹
     (⋀T0. Γ ⊢ t : T0 ⟹ Γ ⊢ t' : T0) ⟹ Γ ⊢ E t' : T"
  "Γ ⊢ fs [:] fTs ⟹ Er ∈ rctxt ⟹ fs = Er t ⟹
     (⋀T0. Γ ⊢ t : T0 ⟹ Γ ⊢ t' : T0) ⟹ Γ ⊢ Er t' [:] fTs"
proof (induct arbitrary: E t t' and Er 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 T1 T2 Γ t2 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 Γ t1 T11 T12 t2 E t t')
  from ‹E ∈ ctxt›
  show ?case using T_App
    by cases (simp_all, (blast intro: typing_typings.intros)+)
next
  case (T_TAbs T1 Γ t2 T2 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 Γ t1 T11 T12 T2 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 Γ t1 T1 p Δ t2 T2 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: "Γ ⊢ (λ:T11. t12) ∙ t2 : T"
  shows "Γ ⊢ t12[0 ↦ t2] : T"
  using H
proof (induct Γ "(λ:T11. t12) ∙ t2" T arbitrary: T11 t12 t2 rule: typing_induct)
  case (T_App Γ T11 T12 t2 T11' t12)
  from ‹Γ ⊢ (λ:T11'. t12) : T11 → T12›
  obtain S'
    where T11: "Γ ⊢ T11 <: T11'"
    and t12: "VarB T11' ∷ Γ ⊢ t12 : S'"
    and S': "Γ ⊢ S'[0 ↦τ Top]τ <: T12" by (rule Abs_type' [simplified]) blast
  from ‹Γ ⊢ t2 : T11›
  have "Γ ⊢ t2 : T11'" using T11 by (rule T_Sub)
  with t12 have "Γ ⊢ t12[0 ↦ t2] : 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: "Γ ⊢ (λ<:T11. t12) ∙τ T2 : T"
  shows "Γ ⊢ t12[0 ↦τ T2] : T"
  using H
proof (induct Γ "(λ<:T11. t12) ∙τ T2" T arbitrary: T11 t12 T2 rule: typing_induct)
  case (T_TApp Γ T11 T12 T2 T11' t12)
  from ‹Γ ⊢ (λ<:T11'. t12) : (∀<:T11. T12)›
  obtain S'
    where "TVarB T11 ∷ Γ ⊢ t12 : S'"
    and "TVarB T11 ∷ Γ ⊢ S' <: T12" by (rule TAbs_type') blast
  hence "TVarB T11 ∷ Γ ⊢ t12 : T12" by (rule T_Sub)
  then show ?case using ‹Γ ⊢ T2 <: T11›
    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 = t1 IN t2) : T"
  shows "⊢ p ⊳ t1 ⇒ ts ⟹ Γ ⊢ t2[0 ↦s ts] : T"
  using H
proof (induct Γ "LET p = t1 IN t2" T arbitrary: p t1 t2 ts rule: typing_induct)
  case (T_Let Γ t1 T1 p Δ t2 T2 ts)
  from ‹⊢ p : T1 ⇒ Δ› ‹Γ ⊢ t1 : T1› ‹Δ @ Γ ⊢ t2 : T2› ‹⊢ p ⊳ t1 ⇒ 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 v2 T11 t12 Γ T)
  from E_Abs(2)
  show ?case by (rule Abs_preservation)
next
  case (E_TAbs T11 t12 T2 Γ 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 "t0"} such that @{term "t0"} 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 t0 t0'. E ∈ ctxt ∧ t = E t0 ∧ t0 ⟼c t0')"
  "[] ⊢ fs [:] fTs ⟹
     (∀(l, t) ∈ set fs. t ∈ value) ∨ (∃E t0 t0'. E ∈ rctxt ∧ fs = E t0 ∧ t0 ⟼c t0')"
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 t1 T11 T12 t2)
  from ‹t1 ∈ value ∨ (∃E t0 t0'. E ∈ ctxt ∧ t1 = E t0 ∧ t0 ⟼c t0')›
  show ?case
  proof
    assume t1_val: "t1 ∈ value"
    with T_App obtain t S where t1: "t1 = (λ:S. t)"
      by (auto dest!: Fun_canonical)
    from ‹t2 ∈ value ∨ (∃E t0 t0'. E ∈ ctxt ∧ t2 = E t0 ∧ t0 ⟼c t0')›
    show ?thesis
    proof
      assume "t2 ∈ value"
      with t1 have "t1 ∙ t2 ⟼c t[0 ↦ t2]"
        by simp (rule eval.intros)
      thus ?thesis by (iprover intro: C_Hole)
    next
      assume "∃E t0 t0'. E ∈ ctxt ∧ t2 = E t0 ∧ t0 ⟼c t0'"
      with t1_val show ?thesis by (iprover intro: ctxt_rctxt.intros)
    qed
  next
    assume "∃E t0 t0'. E ∈ ctxt ∧ t1 = E t0 ∧ t0 ⟼c t0'"
    thus ?thesis by (iprover intro: ctxt_rctxt.intros)
  qed
next
  case T_TAbs
  from value.TAbs show ?case ..
next
  case (T_TApp t1 T11 T12 T2)
  from ‹t1 ∈ value ∨ (∃E t0 t0'. E ∈ ctxt ∧ t1 = E t0 ∧ t0 ⟼c t0')›
  show ?case
  proof
    assume "t1 ∈ value"
    with T_TApp obtain t S where "t1 = (λ<:S. t)"
      by (auto dest!: TyAll_canonical)
    hence "t1 ∙τ T2 ⟼c t[0 ↦τ T2]" by simp (rule eval.intros)
    thus ?thesis by (iprover intro: C_Hole)
  next
    assume "∃E t0 t0'. E ∈ ctxt ∧ t1 = E t0 ∧ t0 ⟼c t0'"
    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 t1 T1 p Δ t2 T2)
  from ‹t1 ∈ value ∨ (∃E t0 t0'. E ∈ ctxt ∧ t1 = E t0 ∧ t0 ⟼c t0')›
  show ?case
  proof
    assume t1: "t1 ∈ value"
    with T_Let have "∃ts. ⊢ p ⊳ t1 ⇒ ts"
      by (auto intro: ptyping_match)
    with t1 show ?thesis by (iprover intro: eval.intros C_Hole)
  next
    assume "∃E t0 t0'. E ∈ ctxt ∧ t1 = E t0 ∧ t0 ⟼c t0'"
    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 t0 t0'. E ∈ ctxt ∧ t = E t0 ∧ t0 ⟼c t0')›
  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 t0 t0'. E ∈ ctxt ∧ t = E t0 ∧ t0 ⟼c t0'"
    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 t0 t0'. E ∈ ctxt ∧ t = E t0 ∧ t0 ⟼c t0')"
    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'"
  "Er ∈ rctxt ⟹ t ⟼ t' ⟹ Er t [⟼] Er 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