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"
                         (‹_ , _ ⊨_ctxt _ : _ ← _› [50, 50, 50, 50, 50] 50)
where
  type_ctxtEmpty [intro!]: "Γ, Δ ⊨_ctxt ♢ : T ← T" |
  type_ctxtApp   [intro!]: "[ Γ, Δ ⊨_ctxt E : (T1→T2) ← U; Γ, Δ ⊨_T t : T1 ] ==> Γ, Δ ⊨_ctxt (E ^\<bullet> t) : T2 ← U"

inductive_cases typing_ctxt_elims [elim!]:
  "Γ, Δ ⊨_ctxt ♢ : T ← T"
  "Γ, Δ ⊨_ctxt (E ^\<bullet> t) : T ← U"

lemma typing_ctxt_correct1:
  shows "Γ, Δ ⊨_T (ctxt_subst E r) : T ==> ∃U. (Γ, Δ ⊨_T r : U ∧ Γ, Δ ⊨_ctxt E : T ← U)"
  by(induction E arbitrary: Γ Δ T r; force)

lemma typing_ctxt_correct2:
  shows "Γ, Δ ⊨_ctxt 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 (♢ ^\<bullet> (liftM_trm s n))]^C = c[n=n ((liftM_ctxt E n) ^\<bullet> (liftM_trm s n))]^C"
  "∀n E s. (t[n=n (liftM_ctxt E n)]^T)[n=n (♢ ^\<bullet> (liftM_trm s n))]^T = t[n=n ((liftM_ctxt E n) ^\<bullet> (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 "Γ, Δ ⊨_ctxt 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: "Γ, Δ ⊨_ctxt ♢ : 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