Theory First_Order_Clause.IsaFoR_Nonground_Term

theory IsaFoR_Nonground_Term
  imports
    "Regular_Tree_Relations.Ground_Terms"
    Nonground_Term
    Abstract_Substitution.Substitution_First_Order_Term
begin

text ‹Prefer @{thm [source] term_subst.subst_id_subst} to @{thm [source] subst_apply_term_empty}.›
declare subst_apply_term_empty[no_atp]

global_interpretation "term": base_functional_substitution where
  comp_subst = "(∘⇩s)" and id_subst = Var and subst = "(⋅)" and vars = vars_term
proof unfold_locales
  fix t :: "('f, 'v) term"  and σ τ :: "('f, 'v) subst"

  assume "⋀x. x ∈ vars_term t ⟹ σ x = τ x"

  then show "t ⋅ σ = t ⋅ τ"
    by (rule term_subst_eq)
next

  show "∃t. is_ground_trm t"
    using vars_term_of_gterm
    by metis
next
  fix x :: 'v

  show "vars_term (Var x) = {x}"
    by simp
next
  fix σ σ' :: "('f, 'v) subst" and x

  show "(σ ∘⇩s σ') x = σ x ⋅ σ'"
    unfolding subst_compose_def ..
next
  fix t :: "('f, 'v) term" and ρ :: "('f, 'v) subst"

  show "vars_term (t ⋅ ρ) = ⋃ (vars_term ` ρ ` vars_term t)"
    using vars_term_subst .
qed

global_interpretation "term" : nonground_term where
  comp_subst = "(∘⇩s)" and Var = Var and term_subst = "(⋅)" and term_vars = vars_term and
  term_to_ground = gterm_of_term and term_from_ground = term_of_gterm
proof unfold_locales
  fix t :: "('f, 'v) term"

  show "finite (vars_term t)"
    by simp
next
  fix t :: "('f, 'v) term"

  show "(vars_term t = {}) ⟷ (∀σ. t ⋅ σ = t)"
    using is_ground_trm_iff_ident_forall_subst .
next
  fix t :: "('f, 'v) term" and ts :: "('f, 'v) term set"

  assume "finite ts" "vars_term t ≠ {}"

  then show "∃σ. t ⋅ σ ≠ t ∧ t ⋅ σ ∉ ts"
  proof(induction t arbitrary: ts)
    case (Var x)

    obtain t' where t': "t' ∉ ts" "is_Fun t'"
      using Var.prems(1) finite_list by blast

    define σ :: "('f, 'v) subst" where "⋀x. σ x = t'"

    have "Var x ⋅ σ ≠ Var x"
      using t'
      unfolding σ_def
      by auto

    moreover have "Var x ⋅ σ ∉ ts"
      using t'
      unfolding σ_def
      by simp

    ultimately show ?case
      using Var
      by blast
  next
    case (Fun f args)

    obtain a where a: "a ∈ set args" and a_vars: "vars_term a ≠ {}"
      using Fun.prems
      by fastforce

    then obtain σ where
      σ: "a ⋅ σ ≠ a" and
      a_σ_not_in_args: "a ⋅ σ ∉ ⋃ (set `  term.args ` ts)"
      by (metis Fun.IH Fun.prems(1) List.finite_set finite_UN finite_imageI)

    then have "Fun f args ⋅ σ ≠ Fun f args"
      by (metis a subsetI term.set_intros(4) term_subst.comp_subst.left.action_neutral
          vars_term_subset_subst_eq)

    moreover have "Fun f args ⋅ σ ∉ ts"
      using a a_σ_not_in_args
      by auto

    ultimately show ?case
      using Fun
      by blast
  qed
next
   {
    fix t :: "('f, 'v) term"
    assume t_is_ground: "is_ground_trm t"

    have "∃g. term_of_gterm g = t"
    proof(intro exI)

      from t_is_ground
      show "term_of_gterm (gterm_of_term t) = t"
        by (induction t) (simp_all add: map_idI)

    qed
  }

  then show "{t :: ('f, 'v) term. is_ground_trm t} = range term_of_gterm"
    by fastforce
next
  fix t⇩G :: "'f gterm"

  show "gterm_of_term (term_of_gterm t⇩G) = t⇩G"
    by simp
next
  fix ρ :: "('f, 'v) subst"

  show "term_subst.is_renaming ρ ⟷ inj ρ ∧ (∀x. ∃x'. ρ x = Var x')"
    using term_subst_is_renaming_iff
    unfolding is_Var_def .
next
   fix ρ :: "('f, 'v) subst" and t
  assume ρ: "term_subst.is_renaming ρ"
  show "vars_term (t ⋅ ρ) = term.rename ρ ` vars_term t"
  proof(induction t)
    case (Var x)
    have "ρ x = Var (term.rename ρ x)"
      using ρ
      unfolding term.rename_def[OF ρ] term_subst_is_renaming_iff is_Var_def
      by (meson someI_ex)

    then show ?case
      by auto
  next
    case (Fun f ts)
    then show ?case
      by auto
  qed
next
  fix t :: "('f, 'v) term" and μ :: "('f, 'v) subst" and unifications

  assume imgu:
    "term_subst.is_imgu μ unifications"
    "∀unification∈unifications. finite unification"
    "finite unifications"

  show "vars_term (t ⋅ μ) ⊆ vars_term t ∪ ⋃ (vars_term ` ⋃ unifications)"
    using range_vars_subset_if_is_imgu[OF imgu] vars_term_subst_apply_term_subset
    by fastforce
qed

lemma term_context_ground_iff_term_is_ground [simp]: "Term_Context.ground t = term.is_ground t"
  by (induction t) simp_all

declare Term_Context.ground_vars_term_empty [simp del]

lemma infinite_terms [intro]: "infinite (UNIV :: ('f, 'v) term set)"
proof -
  have "infinite (UNIV :: ('f, 'v) term list set)"
    using infinite_UNIV_listI .

  then have "⋀f :: 'f. infinite ((Fun f) ` (UNIV :: ('f, 'v) term list set))"
    by (meson finite_imageD injI term.inject(2))

  then show "infinite (UNIV :: ('f, 'v) term set)"
    using infinite_super top_greatest 
    by blast
qed

end