Theory First_Order_Clause.Monomorphic_Typing

theory Monomorphic_Typing
  imports
    Nonground_Term_Typing
    Ground_Term_Typing
    IsaFoR_Nonground_Term
    Typed_IMGU
begin

no_notation Ground_Term_Typing.welltyped (‹_ ⊢ _ : _› [1000, 0, 50] 50)
notation Ground_Term_Typing.welltyped (‹_ ⊢ _ :⇩G _› [1000, 0, 50] 50)

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

inductive welltyped :: "('v, 'ty) var_types ⇒ ('f,'v) term ⇒ 'ty ⇒ bool" 
  for 𝒱 where
    Var: "welltyped 𝒱 (Var x) τ" if 
    "𝒱 x = τ" 
  | Fun: "welltyped 𝒱 (Fun f ts) τ" if 
    "ℱ f (length ts) = Some (τs, τ)"
    "list_all2 (welltyped 𝒱) ts τs"

(* TODO: Introduce notations also for lifting + substition *)
notation welltyped (‹_ ⊢ _ : _› [1000, 0, 50] 50)


sublocale "term": base_typing where welltyped = "welltyped 𝒱" for 𝒱
proof unfold_locales
  show "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
qed

sublocale "term": term_typing where 
  welltyped = "welltyped 𝒱" and apply_context = ctxt_apply_term for 𝒱
proof unfold_locales
  fix t t' c τ τ'

  assume
    welltyped_t_t': "𝒱 ⊢ t : τ'" "𝒱 ⊢ t' : τ'" and
    welltyped_c_t: "𝒱 ⊢ c⟨t⟩ : τ"

  from welltyped_c_t show "𝒱 ⊢ c⟨t'⟩ : τ"
  proof (induction c arbitrary: τ)
    case Hole
    then show ?case
      using welltyped_t_t'
      by auto
  next
    case (More f ss1 c ss2)

    have "𝒱 ⊢ Fun f (ss1 @ c⟨t⟩ # ss2) : τ"
      using More.prems
      by simp

    then have "𝒱 ⊢ Fun f (ss1 @ c⟨t'⟩ # ss2) : τ"
    proof (cases 𝒱 "Fun f (ss1 @ c⟨t⟩ # ss2)" τ rule: welltyped.cases)
      case (Fun τs)

      show ?thesis
      proof (rule welltyped.Fun)
        show "ℱ f (length (ss1 @ c⟨t'⟩ # ss2)) = Some (τs, τ)"
          using Fun 
          by simp
      next
        show "list_all2 (welltyped 𝒱) (ss1 @ c⟨t'⟩ # ss2) τs"
          using ‹list_all2 (welltyped 𝒱) (ss1 @ c⟨t⟩ # 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 c t τ
  assume "𝒱 ⊢ c⟨t⟩ : τ" 
  then show "∃τ'. 𝒱 ⊢ t : τ'"
    by
      (induction c arbitrary: τ)
      (auto simp: welltyped.simps list_all2_Cons1 list_all2_append1)
qed

sublocale "term": base_typing_properties where
  id_subst = "Var :: 'v ⇒ ('f, 'v) term" and comp_subst = "(∘⇩s)" and subst = "(⋅)" and
  vars = term.vars and welltyped = welltyped and to_ground = term.to_ground and
  from_ground = term.from_ground and
  subst_updates = subst_updates and apply_subst = apply_subst and subst_update = fun_upd
proof(unfold_locales; (intro welltyped.Var refl)?)
  fix t :: "('f, 'v) term" and 𝒱 σ τ
  assume type_preserving_σ: " ∀x∈term.vars t. 𝒱 ⊢ Var x : 𝒱 x ⟶ 𝒱 ⊢ σ x : 𝒱 x"

  show "𝒱 ⊢ t ⋅ σ : τ ⟷ 𝒱 ⊢ t : τ"  
  proof (rule iffI)

    assume "𝒱 ⊢ t : τ"

    then show "𝒱 ⊢ t ⋅ σ : τ"
      using type_preserving_σ
      by 
        (induction rule: welltyped.induct)
        (auto simp: list.rel_mono_strong list_all2_map1 welltyped.simps)
  next

    assume "𝒱 ⊢ t ⋅ σ : τ"

    then show "𝒱 ⊢ t : τ"
      using type_preserving_σ
    proof (induction "t ⋅ σ" τ arbitrary: t rule: welltyped.induct)
      case (Var x τ)

      then obtain x' where t: "t = Var x'"
        by (metis subst_apply_eq_Var)

      have "𝒱 ⊢ t : 𝒱 x'"
        unfolding t
        by (simp add: welltyped.Var)

      moreover have "𝒱 ⊢ t : 𝒱 x"
        using Var
        unfolding t
        by (simp add: welltyped.simps)

      ultimately have 𝒱_x': "τ = 𝒱 x'"
        using Var.hyps
        by blast

      show ?case
        unfolding t 𝒱_x'
        by (simp add: welltyped.Var)
    next
      case (Fun f τs τ ts)

      then show ?case
        by (cases t) (simp_all add: list.rel_mono_strong list_all2_map1 welltyped.simps)
    qed
  qed
next
  fix t :: "('f, 'v) term" and 𝒱 𝒱' τ

  assume "𝒱 ⊢ t : τ" "∀x∈term.vars t. 𝒱 x = 𝒱' x"

  then show "𝒱' ⊢ t : τ"
    by (induction rule: welltyped.induct) (simp_all add: welltyped.simps list.rel_mono_strong)
next
  fix 𝒱 𝒱' :: "('v, 'ty) var_types" and t :: "('f, 'v) term" and ρ :: "('f, 'v) subst" and τ

  assume
    renaming: "term.is_renaming ρ" and
    𝒱: "∀x∈term.vars t. 𝒱 x = 𝒱' (term.rename ρ x)"

  then show "𝒱' ⊢ t ⋅ ρ : τ ⟷ 𝒱 ⊢ t : τ"
  proof(intro iffI)

    assume "𝒱' ⊢ t ⋅ ρ : τ"

    with 𝒱 show "𝒱 ⊢ t : τ"
    proof(induction t arbitrary: τ)
      case (Var x)

      then have "𝒱' (term.rename ρ x) = τ"
        using renaming Var term.id_subst_rename[OF renaming]
        by (metis eval_term.simps(1) term.right_uniqueD welltyped.Var)

      then have "𝒱 x = τ"
        by (simp add: Var.prems(1))

      then show ?case
        by(rule welltyped.Var)
    next
      case (Fun f ts)

      then have "𝒱' ⊢ Fun f (map (λs. s ⋅ ρ) ts) : τ"
        by auto

      then obtain τs where τs:
        "list_all2 (welltyped 𝒱') (map (λs. s ⋅ ρ) ts) τs" 
        "ℱ f (length (map (λs. s ⋅ ρ) ts)) = Some (τs, τ)"
        using welltyped.simps
        by blast

      then have ℱ: "ℱ f (length ts) = Some (τs, τ)"
        by simp

      show ?case
      proof(rule welltyped.Fun[OF ℱ])

        show "list_all2 (welltyped 𝒱) ts τs"
          using τs(1) Fun.IH
          by (smt (verit, ccfv_SIG) Fun.prems(1) eval_term.simps(2) in_set_conv_nth length_map
              list_all2_conv_all_nth nth_map term.set_intros(4))
      qed
    qed
  next
    assume "𝒱 ⊢ t : τ"

    then show "𝒱' ⊢ t ⋅ ρ : τ"
      using 𝒱
    proof(induction rule: welltyped.induct)
      case (Var x τ)

      then have "𝒱' (term.rename ρ x) = τ"
        by simp

      then show ?case
        using term.id_subst_rename[OF renaming]
        by (metis eval_term.simps(1) welltyped.Var)
    next
      case (Fun f ts τs τ)

      have "list_all2 (welltyped 𝒱') (map (λs. s ⋅ ρ) ts) τs"
        using Fun
        by (auto simp: list.rel_mono_strong list_all2_map1)

      then show ?case
        by (simp add: Fun.hyps welltyped.simps)
    qed
  qed
next
  fix 𝒱 :: "('v, 'ty) var_types"  and x

  show "𝒱 ⊢ Var x : 𝒱 x ∨ ¬ term.is_welltyped 𝒱 (Var x)"
    by (simp add: Var)
qed

sublocale "term": typed_term_imgu where 
  welltyped = "welltyped :: ('v ⇒ 'ty) ⇒ ('f, 'v) Term.term ⇒ 'ty ⇒ bool"
  by unfold_locales

lemma exists_witness_if_exists_const_for_all_types: 
  assumes "⋀τ. ∃f. ℱ f 0 = Some ([], τ)"
  shows "∃t. term.is_ground t ∧ welltyped 𝒱 t τ"
proof -
  fix 𝒱 :: "('v, 'ty) var_types" and τ

  obtain f where f: "ℱ f 0 = Some ([], τ)"
    using assms
    by blast

  show "∃t. term.is_ground t ∧ 𝒱 ⊢ t : τ"
  proof(rule exI[of _ "Fun f []"], intro conjI welltyped.Fun)

    show "term.is_ground (Fun f [])"
      by simp
  next

    show "ℱ f (length []) = Some ([], τ)"
      using f
      by simp
  next

    show "list_all2 (welltyped 𝒱) [] []"
      by simp
  qed
qed

end

end