Theory Sorted_Contexts

section ‹Sorted Contexts›

theory Sorted_Contexts
  imports
    First_Order_Terms.Subterm_and_Context
    Sorted_Terms
begin

text ‹We introduce the sort signature for abstract contexts:›

fun aContext where
  "aContext F A (Hole,σ) = Some σ"
| "aContext F A (More f ls C rs, σ) = do {
    ρs ← those (map A ls);
    μ ← aContext F A (C,σ);
    νs ← those (map A rs);
    F (f, ρs @ μ # νs)}"

text ‹Term contexts are abstract contexts in the term algebra.›

abbreviation Context (‹(2𝒞'(_,/_'))› [1,1]1000) where
  "𝒞(F,V) ≡ aContext F 𝒯(F,V)"

lemma Hole_hastype[simp]: "Hole : σ → τ in aContext F A ⟷ σ = τ"
  and More_hastype: "More f ls C rs : σ → τ in aContext F A ⟷ (∃ρs μ νs.
    f : ρs @ μ # νs → τ in F ∧
    ls :⇩l ρs in A ∧
    C : σ → μ in aContext F A ∧
    rs :⇩l νs in A)"
   by (auto simp: hastype_list_iff_those bind_eq_Some_conv fun_hastype_def
       intro!: hastypeI)

lemma More_hastypeI:
  assumes "f : ρs @ μ # νs → τ in F"
    and "ls :⇩l ρs in A"
    and "C : σ → μ in aContext F A"
    and "rs :⇩l νs in A"
  shows "More f ls C rs : σ → τ in aContext F A"
  using assms by (auto simp: More_hastype)

lemma hastype_aContext_induct[consumes 1, case_names Hole More]:
  assumes C: "C : σ → τ in aContext F A"
    and hole: "P □ σ"
    and more: "⋀f μs ρ νs τ ls C rs.
      f : μs @ ρ # νs → τ in F ⟹
      ls :⇩l μs in A ⟹
      C : σ → ρ in aContext F A ⟹
      P C ρ ⟹
      rs :⇩l νs in A ⟹
      P (More f ls C rs) τ"
  shows "P C τ"
  using C
proof (induct C arbitrary: τ)
  case Hole
  with hole show ?case by auto
next
  case (More f ls C rs)
  from ‹More f ls C rs : σ → τ in aContext F A›
    [unfolded More_hastype]
  obtain ρs μ νs
    where f: "f : ρs @ μ # νs → τ in F"
      and ls: "ls :⇩l ρs in A"
      and C: "C : σ → μ in aContext F A"
      and rs: "rs :⇩l νs in A" by auto
  show ?case
    using More(1)[OF C] more[OF f ls C _ rs]
    by (auto simp: bind_eq_Some_conv)
qed

lemma hastype_aContext_cases[consumes 1, case_names Hole More]:
  assumes C: "C : σ → τ in aContext F A"
    and hole: "C = □ ⟹ thesis"
    and more: "⋀f μs ρ νs ls D rs.
      C = More f ls D rs ⟹
      f : μs @ ρ # νs → τ in F ⟹
      ls :⇩l μs in A ⟹
      D : σ → ρ in aContext F A ⟹
      rs :⇩l νs in A ⟹
      thesis"
  shows thesis
proof (cases C)
  case Hole
  with hole show ?thesis by auto
next
  case (More f ls D rs)
  from C[unfolded this More_hastype]
  obtain ρs μ νs
    where f: "f : ρs @ μ # νs → τ in F"
      and ls: "ls :⇩l ρs in A"
      and D: "D : σ → μ in aContext F A"
      and rs: "rs :⇩l νs in A" by auto
  show ?thesis
    using more[OF More f ls D rs].
qed

lemma (in sorted_map) map_args_actxt_hastype:
  assumes "C : σ → τ in aContext F A"
  shows "map_args_actxt f C : σ → τ in aContext F B"
  using assms
  apply (induct C arbitrary: τ)
  by (auto dest!: sorted_map_list simp: More_hastype)

context sorted_algebra begin

lemma intp_ctxt_hastype:
  assumes C: "C : σ → τ in aContext F A" and a: "a : σ in A"
  shows "I⟨C;a⟩ : τ in A"
  using C
proof (induct arbitrary: τ)
  case Hole
  with a show ?case by simp
next
  case (More f ls C rs)
  then show ?case by (auto intro!: sort_matches list_all2_appendI simp: More_hastype)
qed

lemma ctxt_has_same_type:
  assumes C: "C : σ → τ in aContext F A" and "a : σ in A"
  shows "I⟨C;a⟩ : τ' in A ⟷ τ' = τ"
  using assms by (auto simp: has_same_type intp_ctxt_hastype)

lemma eval_ctxt_hastype:
  assumes C: "C : σ → τ in 𝒞(F,V)" and α: "α :⇩s V → A"
  shows "I⟦C⟧⇩c α : σ → τ in aContext F A"
  using sorted_map.map_args_actxt_hastype[OF eval_sorted_map[OF α] C].

end

lemmas apply_ctxt_hastype = term.intp_ctxt_hastype
lemmas subst_ctxt_hastype = term.eval_ctxt_hastype

lemma subt_in_dom:
  assumes s: "s ∈ dom 𝒯(F,V)" and st: "s ⊵ t" shows "t ∈ dom 𝒯(F,V)"
  using st s
proof (induction)
  case (refl t)
  then show ?case.
next
  case (subt u ss t f)
  from Fun_in_dom_imp_arg_in_dom[OF ‹Fun f ss ∈ dom 𝒯(F,V)› ‹u ∈ set ss›] subt.IH
  show ?case by auto
qed


lemma hastype_context_decompose:
  assumes "C⟨t⟩ : τ in 𝒯(F,V)"
  shows "∃ σ. C : σ → τ in 𝒞(F,V) ∧ t : σ in 𝒯(F,V)"
  using assms
proof (induct C arbitrary: τ)
  case Hole
  then show ?case by auto
next
  case (More f bef C aft τ)
  from More(2) have "Fun f (bef @ C⟨t⟩ # aft) : τ in 𝒯(F,V)" by auto
  from this[unfolded Fun_hastype] obtain σs where
    f: "f : σs → τ in F" and list: "bef @ C⟨t⟩ # aft :⇩l σs in 𝒯(F,V)" 
    by auto
  from list have len: "length σs = length bef + Suc (length aft)"
    by (simp add: list_all2_conv_all_nth)
  let ?i = "length bef" 
  from len have "?i < length σs" by auto
  hence id: "take ?i σs @ σs ! ?i # drop (Suc ?i) σs = σs"
    by (metis id_take_nth_drop)
  from list have Ct: "C⟨t⟩ : σs ! ?i in 𝒯(F,V)"
    by (metis (no_types, lifting) list_all2_Cons1 list_all2_append1 nth_append_length)
  from list have bef: "bef :⇩l take ?i σs in 𝒯(F,V)"
    by (metis (no_types, lifting) append_eq_conv_conj list_all2_append1)
  from list have aft: "aft :⇩l drop (Suc ?i) σs in 𝒯(F,V)"
    by (metis (no_types, lifting) Cons_nth_drop_Suc append_eq_conv_conj drop_all length_greater_0_conv linorder_le_less_linear list.rel_inject(2) list.simps(3) list_all2_append1)
  from More(1)[OF Ct] obtain σ where C: "C : σ → σs ! ?i in 𝒞(F,V)" and t: "t : σ in 𝒯(F,V)" 
    by auto
  show ?case 
    by (intro exI[of _ σ] conjI More_hastypeI[OF _ bef _ aft, of _ "σs ! ?i"] C t, unfold id, rule f)
qed

lemma apply_ctxt_in_dom_imp_in_dom:
  assumes "C⟨t⟩ ∈ dom 𝒯(F,V)" 
  shows "t ∈ dom 𝒯(F,V)"
  apply (rule subt_in_dom[OF assms]) by simp

lemma apply_ctxt_hastype_imp_hastype_context:
  assumes C: "C⟨t⟩ : τ in 𝒯(F,V)" and t: "t : σ in 𝒯(F,V)"
  shows "C : σ → τ in 𝒞(F,V)"
  using hastype_context_decompose[OF C] t by (auto simp: has_same_type)

end