Theory ContextFacts

subsection‹Contextual typing›

theory ContextFacts
imports
    Reduction
    Types
begin

text‹Naturally, we may wonder when instantiating the hole in a context is type-preserving.
    To assess this, we define a typing judgement for contexts.›

inductive typing_ctxt :: "(nat ⇒ type) ⇒ (nat ⇒ type) ⇒ ctxt ⇒ type ⇒ type ⇒ bool"
                         (‹_ , _ ⊢⇩c⇩t⇩x⇩t _ : _ ⇐ _› [50, 50, 50, 50, 50] 50)
where
  type_ctxtEmpty [intro!]: "Γ, Δ ⊢⇩c⇩t⇩x⇩t ◇ : T ⇐ T" |
  type_ctxtApp   [intro!]: "⟦ Γ, Δ ⊢⇩c⇩t⇩x⇩t E : (T1→T2) ⇐ U; Γ, Δ ⊢⇩T t : T1 ⟧ ⟹ Γ, Δ ⊢⇩c⇩t⇩x⇩t (E ⇧∙ t) : T2 ⇐ U"

inductive_cases typing_ctxt_elims [elim!]:
  "Γ, Δ ⊢⇩c⇩t⇩x⇩t ◇ : T ⇐ T"
  "Γ, Δ ⊢⇩c⇩t⇩x⇩t (E ⇧∙ t) : T ⇐ U"

lemma typing_ctxt_correct1:
  shows "Γ, Δ ⊢⇩T (ctxt_subst E r) : T  ⟹ ∃U. (Γ, Δ ⊢⇩T r : U ∧ Γ, Δ ⊢⇩c⇩t⇩x⇩t E : T ⇐ U)"
  by(induction E arbitrary: Γ Δ T r; force)

lemma typing_ctxt_correct2:
  shows "Γ, Δ ⊢⇩c⇩t⇩x⇩t E : T ⇐ U ⟹ Γ, Δ ⊢⇩T r : U  ⟹ Γ, Δ ⊢⇩T (ctxt_subst E r) : T"
  by(induction arbitrary: r rule: typing_ctxt.induct) auto

lemma ctxt_subst_basecase: 
  "∀n. c[n = n ◇]⇧C =  c"
  "∀n. t[n = n ◇]⇧T =  t"
  by(induct c and t) (auto) 

lemma ctxt_subst_caseApp:
  "∀n E s. (c[n=n (liftM_ctxt E n)]⇧C)[n=n (◇ ⇧∙ (liftM_trm s n))]⇧C = c[n=n ((liftM_ctxt E n) ⇧∙ (liftM_trm s n))]⇧C"
  "∀n E s. (t[n=n (liftM_ctxt E n)]⇧T)[n=n (◇ ⇧∙ (liftM_trm s n))]⇧T = t[n=n ((liftM_ctxt E n) ⇧∙ (liftM_trm s n))]⇧T"
  by (induction c and t) (auto simp add: liftLM_comm_ctxt liftLM_comm liftMM_comm_ctxt  liftMM_comm liftM_ctxt_struct_subst)

lemma ctxt_subst:
  assumes "Γ, Δ ⊢⇩c⇩t⇩x⇩t E : U ⇐ T"
  shows   "(ctxt_subst E (μ T : c)) ⇢⇧* μ U : (c[0 = 0 (liftM_ctxt E 0)]⇧C)"
using assms proof(induct E arbitrary: U T Γ Δ c)
  case ContextEmpty
  have ctxtEmpty_inv: "Γ, Δ ⊢⇩c⇩t⇩x⇩t ◇ : U ⇐ T ⟹ U = T"
    by(cases Γ Δ "◇" rule: typing_ctxt.cases, fastforce, simp)
  show ?case
    using ContextEmpty by (clarsimp dest!: ctxtEmpty_inv simp: ctxt_subst_basecase)
next
  case (ContextApp E x)
  then show ?case
    by clarsimp (rule rtc_term_trans, rule rtc_appL, assumption, rule step_term, force, clarsimp simp add: ctxt_subst_caseApp(1))
qed
  
end