Theory Sorted_Contexts

section ‹Sorted Contexts›

theory Sorted_Contexts
  imports
    First_Order_Terms.Subterm_and_Context
    Sorted_Terms
begin

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)}"

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


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)

end

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

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

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

lemmas hastype_context_apply = term.intp_ctxt_hastype

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)

lemma subst_apply_ctxt_sorted:
  assumes "C : σ → τ in 𝒞(F,X)" and "θ :⇩s X → 𝒯(F,V)"
  shows "C ⋅⇩c θ : σ → τ in 𝒞(F,V)"
  using assms
proof(induct arbitrary: θ rule: hastype_aContext_induct)
  case (Hole)
  then show ?case by simp
next
  case (More f σb ρ σa τ bef C aft)
  have fssig: "f : σb @ ρ # σa → τ in F" using More(1) .
  have bef:"bef :⇩l σb in 𝒯(F,X)" using More(2) .
  have Cssig:"C : σ → ρ in 𝒞(F,X)" using More(3) .
  have aft:"aft :⇩l σa in 𝒯(F,X)" using More(5) .
  have theta:"θ :⇩s X → 𝒯(F,V)" using More(6) .
  hence ctheta:"C ⋅⇩c θ : σ → ρ in 𝒞(F,V)" using More(4) by simp
  have len_bef:"length bef = length σb" using bef list_all2_iff by blast
  have len_aft:"length aft = length σa" using aft list_all2_iff by blast
  { fix i
    assume len_i:"i < length σb"
    hence "bef ! i ⋅ θ : σb ! i in 𝒯(F,V)"
    proof -
      have "bef ! i : σb ! i in 𝒯(F,X)" using bef
        by (simp add: len_i list_all2_conv_all_nth)
      from subst_hastype[OF theta this] 
      show ?thesis.
    qed
  } note * = this
  have mb: "map (λt. t ⋅ θ) bef :⇩l σb in 𝒯(F,V)" using length_map 
    by (auto simp:* theta bef list_all2_conv_all_nth len_bef)
  { fix i
    assume len_i:"i < length σa"
    hence "aft ! i ⋅ θ : σa ! i in 𝒯(F,V)"
    proof -
      have "aft ! i : σa ! i in 𝒯(F,X)" using aft
        by (simp add: len_i list_all2_conv_all_nth)
      from subst_hastype[OF theta this] 
      show ?thesis.
    qed
  } note ** = this
  have ma: "map (λt. t ⋅ θ) aft :⇩l σa in 𝒯(F,V)" using length_map
    by (auto simp:** theta aft list_all2_conv_all_nth len_aft)
  show "More f bef C aft ⋅⇩c θ : σ → τ in 𝒞(F,V)"
    by (auto intro!: More_hastypeI fssig simp:ctheta mb ma)
qed

end