Theory Nonground_Term_Typing

theory Nonground_Term_Typing
  imports
    Term_Typing
    Typed_Functional_Substitution
    Functional_Substitution_Typing
    Nonground_Term
begin

locale base_typed_properties =
  explicitly_typed_subst_stability +
  explicitly_replaceable_𝒱 +
  explicitly_typed_renaming +
  explicitly_typed_grounding_functional_substitution

locale base_typing_properties =
  base_functional_substitution_typing +
  typed: base_typed_properties +
  welltyped: base_typed_properties where typed = welltyped

locale base_inhabited_typing_properties =
  base_typing_properties +
  typed: inhabited_explicitly_typed_functional_substitution +
  welltyped: inhabited_explicitly_typed_functional_substitution where typed = welltyped

locale nonground_term_typing =
  "term": nonground_term +
  fixes β„± :: "('f, 'ty) fun_types"
begin

inductive typed :: "('v, 'ty) var_types β‡’ ('f,'v) term β‡’ 'ty β‡’ bool"
  for 𝒱 where
    Var: "𝒱 x = Ο„ ⟹ typed 𝒱 (Var x) Ο„"
  | Fun: "β„± f = (Ο„s, Ο„) ⟹ typed 𝒱 (Fun f ts) Ο„"

textβ€ΉNote: Implicitly implies that every function symbol has a fixed arityβ€Ί
inductive welltyped :: "('v, 'ty) var_types β‡’ ('f,'v) term β‡’ 'ty β‡’ bool"
  for 𝒱 where
    Var: "𝒱 x = Ο„ ⟹ welltyped 𝒱 (Var x) Ο„"
  | Fun: "β„± f = (Ο„s, Ο„) ⟹ list_all2 (welltyped 𝒱) ts Ο„s ⟹ welltyped 𝒱 (Fun f ts) Ο„"

sublocale "term": explicit_typing "typed (𝒱 :: ('v, 'ty) var_types)" "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 (full_types) typed.simps welltyped.cases)
qed

sublocale "term": term_typing where
  typed = "typed (𝒱 :: 'v β‡’ 'ty)" and welltyped = "welltyped 𝒱" and Fun = Fun
proof unfold_locales
  fix t t' c Ο„ Ο„'

  assume
    t_type: "welltyped 𝒱 t Ο„'" and
    t'_type: "welltyped 𝒱 t' Ο„'" and
    c_type: "welltyped 𝒱 c⟨t⟩ Ο„"

  from c_type show "welltyped 𝒱 c⟨t'⟩ Ο„"
  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 𝒱 (Fun f (ss1 @ c⟨t⟩ # ss2)) Ο„"
      using More.prems
      by simp

    hence "welltyped 𝒱 (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 = (Ο„s, Ο„)"
          using β€Ήβ„± f = (Ο„s, Ο„)β€Ί .
      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 t t' c Ο„ Ο„'
  assume
    t_type: "typed 𝒱 t Ο„'" and
    t'_type: "typed 𝒱 t' Ο„'" and
    c_type: "typed 𝒱 c⟨t⟩ Ο„"

  from c_type show "typed 𝒱 c⟨t'⟩ Ο„"
  proof (induction c arbitrary: Ο„)
    case Hole
    then show ?case
      using t'_type t_type
      by auto
  next
    case (More f ss1 c ss2)

    have "typed 𝒱 (Fun f (ss1 @ c⟨t⟩ # ss2)) Ο„"
      using More.prems
      by simp

    hence "typed 𝒱 (Fun f (ss1 @ c⟨t'⟩ # ss2)) Ο„"
    proof (cases 𝒱 "Fun f (ss1 @ c⟨t⟩ # ss2)" Ο„ rule: typed.cases)
      case (Fun Ο„s)

      then show ?thesis
        by (simp add: typed.simps)
    qed

    thus ?case
      by simp
  qed
next
  fix f ts Ο„
  assume "welltyped 𝒱 (Fun f ts) Ο„"
  then show "βˆ€t∈set ts. term.is_welltyped 𝒱 t"
    by (cases rule: welltyped.cases) (metis in_set_conv_nth list_all2_conv_all_nth)
next
  fix t
  show "term.is_typed 𝒱 t"
    by (metis term.exhaust prod.exhaust typed.simps)
qed

sublocale "term": base_typing_properties where
  id_subst = "Var :: 'v β‡’ ('f, 'v) term" and comp_subst = "(βŠ™)" and subst = "(β‹…t)" and
  vars = term.vars and welltyped = welltyped and typed = typed and to_ground = term.to_ground and
  from_ground = term.from_ground
proof(unfold_locales; (intro typed.Var welltyped.Var refl)?)
  fix Ο„ and 𝒱 and t :: "('f, 'v) term" and Οƒ
  assume is_typed_on: "βˆ€x ∈ term.vars t. typed 𝒱 (Οƒ x) (𝒱 x)"

  show "typed 𝒱 (t β‹…t Οƒ) Ο„ ⟷ typed 𝒱 t Ο„"
  proof(rule iffI)
    assume "typed 𝒱 t Ο„"

    then show "typed 𝒱 (t β‹…t Οƒ) Ο„"
      using is_typed_on
      by(induction rule: typed.induct)(auto simp: typed.Fun)
  next
    assume "typed 𝒱 (t β‹…t Οƒ) Ο„"

    then show "typed 𝒱 t Ο„"
      using is_typed_on
      by(induction t)(auto simp: typed.simps)
  qed
next
  fix Ο„ and 𝒱 and t :: "('f, 'v) term" and Οƒ

  assume is_welltyped_on: "βˆ€x ∈ term.vars t. welltyped 𝒱 (Οƒ x) (𝒱 x)"

  show "welltyped 𝒱 (t β‹…t Οƒ) Ο„ ⟷ welltyped 𝒱 t Ο„"
  proof(rule iffI)

    assume "welltyped 𝒱 t Ο„"

    then show "welltyped 𝒱 (t β‹…t Οƒ) Ο„"
      using is_welltyped_on
      by(induction rule: welltyped.induct)
        (auto simp: list.rel_mono_strong list_all2_map1 welltyped.simps)
  next

    assume "welltyped 𝒱 (t β‹…t Οƒ) Ο„"

    then show "welltyped 𝒱 t Ο„"
      using is_welltyped_on
    proof(induction "t β‹…t Οƒ" Ο„ arbitrary: t rule: welltyped.induct)
      case (Var x Ο„)

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

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

      moreover have "welltyped 𝒱 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 "typed 𝒱 t Ο„" "βˆ€x∈term.vars t. 𝒱 x = 𝒱' x"

  then show "typed 𝒱' t Ο„"
    by (cases rule: typed.cases) (simp_all add: typed.simps)
next
  fix t :: "('f, 'v) term" and 𝒱 𝒱' Ο„

  assume "welltyped 𝒱 t Ο„" "βˆ€x∈term.vars t. 𝒱 x = 𝒱' x"

  then show "welltyped 𝒱' 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_subst.is_renaming ρ" and 𝒱: "βˆ€x∈term.vars t. 𝒱 x = 𝒱' (term.rename ρ x)"

  show "typed 𝒱' (t β‹…t ρ) Ο„ ⟷ typed 𝒱 t Ο„"
  proof(intro iffI)
    assume "typed 𝒱' (t β‹…t ρ) Ο„"
    with 𝒱 show "typed 𝒱 t Ο„"
    proof(induction t arbitrary: Ο„)
      case (Var x)

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

      then have "𝒱 x = Ο„"
        by (simp add: renaming Var.prems)

      then show ?case
        by(rule typed.Var)
    next
      case (Fun f ts)
      then show ?case
        by (simp add: typed.simps)
    qed
  next
    assume "typed 𝒱 t Ο„"
    then show "typed 𝒱' (t β‹…t ρ) Ο„"
      using 𝒱
    proof(induction rule: typed.induct)
      case (Var x Ο„)

      have "𝒱' (term.rename ρ x) = Ο„"
        using Var.hyps Var.prems
        by auto

      then show ?case
        by (metis eval_term.simps(1) renaming term.id_subst_rename typed.Var)
    next
      case (Fun f Ο„s Ο„ ts)

      then show ?case
        by (simp add: typed.simps)
    qed
  qed
next
  fix 𝒱 𝒱' :: "('v, 'ty) var_types" and t :: "('f, 'v) term" and ρ :: "('f, 'v) subst" and Ο„

  assume
    renaming: "term_subst.is_renaming ρ" and
    𝒱: "βˆ€x∈term.vars t. 𝒱 x = 𝒱' (term.rename ρ x)"

  then show "welltyped 𝒱' (t β‹…t ρ) Ο„ ⟷ welltyped 𝒱 t Ο„"
  proof(intro iffI)

    assume "welltyped 𝒱' (t β‹…t ρ) Ο„"

    with 𝒱 show "welltyped 𝒱 t Ο„"
    proof(induction t arbitrary: Ο„)
      case (Var x)

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

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

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

      then have "welltyped 𝒱' (Fun f (map (Ξ»s. s β‹…t ρ) ts)) Ο„"
        by auto

      then obtain Ο„s where Ο„s:
        "list_all2 (welltyped 𝒱') (map (Ξ»s. s β‹…t ρ) ts) Ο„s" "β„± f = (Ο„s, Ο„)"
        using welltyped.simps
        by blast

      show ?case
      proof(rule welltyped.Fun[OF Ο„s(2)])

        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 "welltyped 𝒱 t Ο„"
    then show "welltyped 𝒱' (t β‹…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 Ο„s Ο„ ts)

      have "list_all2 (welltyped 𝒱') (map (Ξ»s. s β‹…t ρ) 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
qed

end

locale nonground_term_inhabited_typing =
  nonground_term_typing where β„± = β„± for β„± :: "('f, 'ty) fun_types" +
  assumes types_inhabited: "β‹€Ο„. βˆƒf. β„± f = ([], Ο„)"
begin

sublocale base_inhabited_typing_properties where
  id_subst = "Var :: 'v β‡’ ('f, 'v) term" and comp_subst = "(βŠ™)" and subst = "(β‹…t)" and
  vars = term.vars and welltyped = welltyped and typed = typed and to_ground = term.to_ground and
  from_ground = term.from_ground
proof unfold_locales
  fix 𝒱 :: "('v, 'ty) var_types" and Ο„

  obtain f where f: "β„± f = ([], Ο„)"
    using types_inhabited
    by blast

  show "βˆƒt. term.is_ground t ∧ welltyped 𝒱 t Ο„"
  proof(rule exI[of _ "Fun f []"], intro conjI welltyped.Fun)

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

    show "β„± f = ([], Ο„)"
      by(rule f)
  next

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

  then show "βˆƒt. term.is_ground t ∧ typed 𝒱 t Ο„"
    using term.typed_if_welltyped
    by blast
qed

end

end