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 tl? =   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: "fsl? = 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 "fsl? = 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. fsl? = 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. fsl? = u  []  u : U"
      by (rule Rcd_type1')
    with T_Proj obtain u where u: "fsl? = 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