Theory Ground_Typing

theory Ground_Typing
  imports
    Ground_Clause
    Clause_Typing
    Term_Typing
begin

inductive typed for ℱ where
  GFun: "ℱ f = (τs, τ) ⟹ typed ℱ (GFun f ts) τ"

inductive welltyped for ℱ where
  GFun: "ℱ f = (τs, τ) ⟹ list_all2 (welltyped ℱ) ts τs ⟹ welltyped ℱ (GFun f ts) τ"

locale ground_term_typing =
  fixes ℱ :: "('f, 'ty) fun_types"
begin

abbreviation typed where "typed ≡ Ground_Typing.typed ℱ"
abbreviation welltyped where "welltyped ≡ Ground_Typing.welltyped ℱ"

sublocale explicit_typing where typed = typed and welltyped = welltyped
proof unfold_locales

  show "right_unique typed"
  proof (rule right_uniqueI)
    fix t τ⇩1 τ⇩2

    assume "typed t τ⇩1" and "typed t τ⇩2"

    thus "τ⇩1 = τ⇩2"
      by (auto elim!: typed.cases)
  qed
next

  show "right_unique welltyped"
  proof (rule right_uniqueI)
    fix t τ⇩1 τ⇩2

    assume "welltyped t τ⇩1" and "welltyped t τ⇩2"

    thus "τ⇩1 = τ⇩2"
      by (auto elim!: welltyped.cases)
  qed
next
  fix t τ

  assume "welltyped t τ"

  then show "typed t τ"
    by (metis typed.intros welltyped.cases)
qed

sublocale term_typing where typed = typed and welltyped = welltyped and Fun = GFun
proof unfold_locales
  fix t t' c τ τ'

  assume
    t_type: "welltyped t τ'" and
    t'_type: "welltyped t' τ'" and
    c_type: "welltyped c⟨t⟩⇩G τ"

  from c_type show "welltyped c⟨t'⟩⇩G τ"
  proof (induction c arbitrary: τ)
    case Hole

    then show ?case
      using t_type t'_type
      by auto
  next
    case (More f ss1 c ss2)

    have "welltyped (GFun f (ss1 @ c⟨t⟩⇩G # ss2)) τ"
      using More.prems
      by simp

    then have "welltyped (GFun f (ss1 @ c⟨t'⟩⇩G # ss2)) τ"
    proof (cases ℱ "GFun f (ss1 @ c⟨t⟩⇩G # ss2)" τ rule: welltyped.cases)
      case (GFun τs)

      show ?thesis
      proof (rule welltyped.GFun)
        show "ℱ f = (τs, τ)"
          using ‹ℱ f = (τs, τ)› .
      next
        show "list_all2 welltyped (ss1 @ c⟨t'⟩⇩G # ss2) τs"
          using ‹list_all2 welltyped (ss1 @ c⟨t⟩⇩G # ss2) τs›
          using More.IH
          by (smt (verit, del_insts) list_all2_Cons1 list_all2_append1 list_all2_lengthD)
      qed
    qed

    thus ?case
      by simp
  qed
next
  fix t t' c τ τ'

  assume "typed t τ'" "typed t' τ'" "typed c⟨t⟩⇩G τ"

  then show "typed c⟨t'⟩⇩G τ"
    by(induction c arbitrary: τ) (auto simp: typed.simps)
next
  fix f ts τ

  assume "welltyped (GFun f ts) τ"

  then show "∀t∈set ts. is_welltyped t"
    by (metis gterm.inject in_set_conv_nth list_all2_conv_all_nth welltyped.simps)
next
  fix t

  show "is_typed t"
    by (cases t) (meson surj_pair typed.intros)
qed

end

locale ground_typing = "term": ground_term_typing
begin

sublocale clause_typing where term_typed = term.typed and term_welltyped = term.welltyped
  by unfold_locales

end

end