Theory Basic_Terms

theory Basic_Terms 
  imports Sorted_Contexts
begin

lemma map_le_map_add_left:
  assumes disj: "dom m ∩ dom n = {}"
  shows "m ⊆⇩m m ++ n"
  using map_le_map_add map_add_comm[OF disj] by auto

section ‹Basic Terms›

text ‹Given two signatures C and D, a term ‹f(s⇩1,…,s⇩n)› is called a basic term
if ‹f : [σ⇩1,…,σ⇩n] → τ in D› and ‹s⇩1 : σ⇩1,…,s⇩n : σ⇩n in 𝒯(C,X)›.
We define the sorted set of basic terms as follows.›

fun Basic_Term :: "('f,'s) ssig ⇒ ('f,'s) ssig ⇒ ('v ⇀ 's) ⇒ ('f,'v) term ⇀ 's" ("𝒯⇩B'(_,_,_')")
  where "𝒯⇩B(C,D,X) (Var x) = None"
  | "𝒯⇩B(C,D,X) (Fun f ss) = (case those (map 𝒯(C,X) ss) of Some σs ⇒ D (f,σs) | _ ⇒ None)"

abbreviation ground_Basic_Term ("𝒯⇩B'(_,_')") where
  "𝒯⇩B(C,D) ≡ 𝒯⇩B(C,D,λx. None) :: ('f,unit) term ⇀ 's"

lemma Var_hastype_Basic:
  "Var x : σ in 𝒯⇩B(C,D,X) ⟷ False" by (simp add: hastype_def)

lemma Fun_hastype_Basic:
  "Fun f ss : τ in 𝒯⇩B(C,D,X) ⟷ (∃σs. f : σs → τ in D ∧ ss :⇩l σs in 𝒯(C,X))"
  apply (unfold hastype_list_iff_those)
  by (auto simp: hastype_def fun_hastype_def split:option.split_asm)

lemma hastype_Basic:
  "s : τ in 𝒯⇩B(C,D,X) ⟷ (∃f ss σs. s = Fun f ss ∧ f : σs → τ in D ∧ ss :⇩l σs in 𝒯(C,X))"
  by (cases s, auto simp: Var_hastype_Basic Fun_hastype_Basic)

lemma in_dom_Basic:
  "s ∈ dom 𝒯⇩B(C,D,X) ⟷ (∃f ss σs τ. s = Fun f ss ∧ f : σs → τ in D ∧ ss :⇩l σs in 𝒯(C,X))"
  by (auto simp: in_dom_iff_ex_type hastype_Basic)

lemma hastype_BasicE:
  assumes "s : τ in 𝒯⇩B(C,D,X)"
    and "⋀f ss σs. s = Fun f ss ⟹ f : σs → τ in D ⟹ ss :⇩l σs in 𝒯(C,X) ⟹ thesis"
  shows thesis
  using assms by (auto simp: hastype_Basic)

lemma hastype_BasicI:
  "s = Fun f ss ⟹ f : σs → τ in D ⟹ ss :⇩l σs in 𝒯(C,X) ⟹ s : τ in 𝒯⇩B(C,D,X)"
  by (auto simp: hastype_Basic)

lemma Basic_mono:
  assumes D: "D ⊆⇩m D'" and C: "C ⊆⇩m C'" and X: "X ⊆⇩m X'"
  shows "𝒯⇩B(C,D,X) ⊆⇩m 𝒯⇩B(C',D',X')"
proof (safe intro!: subssetI elim!: hastype_BasicE)
  fix f ss σs τ assume f: "f : σs → τ in D" and ss: "ss :⇩l σs in 𝒯(C,X)"
  from subssigD[OF D f] Term_mono[OF C X, THEN subsset_hastype_listD, OF ss]
  show "Fun f ss : τ in 𝒯⇩B(C',D',X')"
    by (intro hastype_BasicI[OF refl])
qed

text ‹Basic terms are terms of the joint signature, if the signatures are disjoint.›

lemma Basic_Term:
  assumes disj: "dom C ∩ dom D = {}"
  shows "𝒯⇩B(C,D,X) ⊆⇩m 𝒯(C++D,X)"
proof (intro subssetI)
  fix s σ
  assume s: "s : σ in 𝒯⇩B(C,D,X)"
  show "s : σ in 𝒯(C++D,X)"
  proof (cases s)
    case (Var x1)
    with s show ?thesis by (auto simp: Var_hastype_Basic)
  next
    case sfss: (Fun f ss)
    with s obtain τs where ss: "ss :⇩l τs in 𝒯(C,X)" and f: "f : τs → σ in D"
      by (auto simp: Fun_hastype_Basic)
    from disj have C: "C ⊆⇩m C++D" by (simp add: map_le_map_add_left)
    from Term_mono_left[OF C, THEN subssetD] ss
    have ssF: "ss :⇩l τs in 𝒯(C++D,X)" by (metis subsset_hastype_listD subssetI)
    have "D ⊆⇩m C++D" by auto
    from subssigD[OF this f] have fF: "f : τs → σ in C++D".
    with ssF have "Fun f ss : σ in 𝒯(C++D,X)" by (auto simp: Fun_hastype)
    then show ?thesis by (auto simp: sfss)
  qed
qed

text ‹Basic terms are preserved under constructor substitution.›

lemma subst_Basic_Term:
  assumes θ: "θ :⇩s X → 𝒯(C,V)" and s: "s : τ in 𝒯⇩B(C,D,X)"
  shows "s⋅θ : τ in 𝒯⇩B(C,D,V)"
proof-
  from s[unfolded hastype_Basic]
  obtain f ss σs where s: "s = Fun f ss" and f: "f : σs → τ in D" and ss: "ss :⇩l σs in 𝒯(C,X)"
    by (auto simp: hastype_Basic)
  from map_subst_hastype[OF θ ss] f
  show ?thesis by (auto simp: hastype_Basic s)
qed

lemma in_dom_Basic_Term_imp_vars: "s ∈ dom 𝒯⇩B(C,D,V) ⟹ x ∈ vars s ⟹ x ∈ dom V"
  apply (elim in_dom_hastypeE)
  apply (cases s)
  by (auto simp: Fun_hastype_Basic list_all2_conv_all_nth in_set_conv_nth dest!: hastype_in_Term_imp_vars)

lemma in_dom_Basic_empty_subst_id:
  assumes "s ∈ dom 𝒯⇩B(C,D,∅)"
  shows "s⋅θ = s"
  using assms
  by (auto elim!: in_dom_hastypeE hastype_BasicE simp: o_def map_subst_Term_empty_id)

lemma in_dom_Basic_empty_subst_subst:
  assumes "s ∈ dom 𝒯⇩B(C,D,∅)"
  shows "s⋅θ⋅τ = s⋅undefined"
  using assms
  by (auto elim!: in_dom_hastypeE hastype_BasicE simp: o_def map_subst_subst_Term_empty)

end