Theory Sorted_Contexts

section ‹Sorted Contexts›

theory Sorted_Contexts
  imports
    First_Order_Terms.Subterm_and_Context
    Sorted_Terms
begin

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


(* sorted contexts *)

inductive has_type_context :: "('f,'s) ssig ⇒ ('v ⇀ 's) ⇒ 's ⇒ ('f,'v)ctxt ⇒ 's ⇒ bool"
   for F V σ where
  Hole: "has_type_context F V σ Hole σ"
| More: "f : σb @ ρ # σa → τ in F ⟹
  bef :⇩l σb in 𝒯(F,V) ⟹ has_type_context F V σ C ρ ⟹ aft :⇩l σa in 𝒯(F,V) ⟹
  has_type_context F V σ (More f bef C aft) τ" 

hide_fact (open) Hole More

abbreviation has_type_context' ("((_) :⇩c/ (_) → (_) in/ 𝒯'(_,_'))" [50,61,51,51,51]50)
  where "C :⇩c σ → τ in 𝒯(F,V) ≡ has_type_context F V σ C τ"

lemma hastype_context_apply:
  assumes "C :⇩c σ → τ in 𝒯(F,V)" and "t : σ in 𝒯(F,V)" 
  shows "C⟨t⟩ : τ in 𝒯(F,V)"
  using assms
proof induct
  case (More f σb ρ σa τ bef C aft)
  show ?case unfolding ctxt_apply_term.simps
  proof (intro Fun_hastypeI[OF More(1)])
    show "bef @ C⟨t⟩ # aft :⇩l σb @ ρ # σa in 𝒯(F,V)" 
      using More(2,5) More(4)[OF More(6)]
      by (simp add: list_all2_appendI)
  qed
qed auto

lemma hastype_context_decompose:
  assumes "C⟨t⟩ : τ in 𝒯(F,V)"
  shows "∃ σ. C :⇩c σ → τ in 𝒯(F,V) ∧ t : σ in 𝒯(F,V)"
  using assms
proof (induct C arbitrary: τ)
  case Hole
  then show ?case by (auto intro: has_type_context.Hole)
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 :⇩c σ → σs ! ?i in 𝒯(F,V)" and t: "t : σ in 𝒯(F,V)" 
    by auto
  show ?case 
    by (intro exI[of _ σ] conjI has_type_context.More[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 :⇩c σ → τ in 𝒯(F,V)"
  using hastype_context_decompose[OF C] t by (auto simp: has_same_type)

lemma subst_apply_ctxt_sorted:
  assumes "C :⇩c σ → τ in 𝒯(F,X)" and "θ :⇩s X → 𝒯(F,V)"
  shows "C ⋅⇩c θ :⇩c σ → τ in 𝒯(F,V)"
  using assms
proof(induct arbitrary: θ rule: has_type_context.induct)
  case (Hole)
  then show ?case by (simp add: has_type_context.Hole)
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 :⇩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 θ :⇩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 θ :⇩c σ → τ in 𝒯(F,V)"
    by (auto intro!: has_type_context.intros fssig simp:ctheta mb ma)
qed

end