Theory First_Order_Clause.Ground_Term_Typing

theory Ground_Term_Typing
  imports
    Term_Typing
    IsaFoR_Ground_Context
begin

type_synonym ('f, 'ty) fun_types = "'f ⇒ nat ⇒ ('ty list × 'ty) option"

inductive welltyped for ℱ ::"('f, 'ty) fun_types" where 
  GFun: "welltyped ℱ (GFun f ts) τ" if 
  "ℱ f (length ts) = Some (τs, τ)"
  "list_all2 (welltyped ℱ) ts τs"

notation welltyped (‹_ ⊢ _ : _› [1000, 0, 50] 50)

global_interpretation "term": term_typing where
  welltyped = "welltyped ℱ" and apply_context = apply_ground_context 
proof unfold_locales

  show right_unique_welltyped: "right_unique (welltyped ℱ)"
  proof (rule right_uniqueI)
    fix t τ⇩1 τ⇩2
    assume "ℱ ⊢ t : τ⇩1" and "ℱ ⊢ t : τ⇩2"

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

  fix t t' c τ τ'
  assume
    welltyped_t_t': "ℱ ⊢ t : τ'" "ℱ ⊢ t' : τ'" and
    welltyped_c_t: "ℱ ⊢ c⟨t⟩⇩G : τ"

  from welltyped_c_t show "ℱ ⊢ c⟨t'⟩⇩G : τ"
  proof (induction c arbitrary: τ)
    case Hole

    then show ?case
      using welltyped_t_t' right_unique_welltyped[THEN right_uniqueD]
      by auto
  next
    case (More f ss1 c ss2)

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

    hence "ℱ ⊢ 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 (length (ss1 @ c⟨t'⟩⇩G # ss2)) = Some (τs, τ)"
          using GFun(1)
          by simp
      next

        show "list_all2 (welltyped ℱ) (ss1 @ c⟨t'⟩⇩G # ss2) τs"
          using GFun(2) 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 c t τ
  assume "ℱ ⊢ c⟨t⟩⇩G : τ" 
  then show "∃τ'. ℱ ⊢ t : τ'"
    by 
      (induction c arbitrary: τ)
      (auto simp: welltyped.simps list_all2_Cons1 list_all2_append1)
qed

end