Theory Nonground_Term

theory Nonground_Term
 imports
    Abstract_Substitution.Substitution_First_Order_Term
    Abstract_Substitution.Functional_Substitution_Lifting
    Ground_Term_Extra
begin

no_notation subst_compose (infixl "∘⇩s" 75)
notation subst_compose (infixl "⊙" 75)

no_notation subst_apply_term (infixl "⋅" 67)
notation subst_apply_term (infixl "⋅t" 67)

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

section ‹Nonground Terms and Substitutions›

type_synonym 'f ground_term = "'f gterm"


subsection ‹Unified naming›

locale vars_def =
  fixes vars_def :: "'expr ⇒ 'var"
begin

abbreviation "vars ≡ vars_def"

end

locale grounding_def =
  fixes
    to_ground_def :: "'expr ⇒ 'expr⇩G" and
    from_ground_def :: "'expr⇩G ⇒ 'expr"
begin

abbreviation "to_ground ≡ to_ground_def"

abbreviation "from_ground ≡ from_ground_def"

end

subsection ‹Term›

locale nonground_term_properties =
  base_functional_substitution +
  finite_variables +
  all_subst_ident_iff_ground

locale term_grounding =
  variables_in_base_imgu where base_vars = vars and base_subst = subst +
  grounding

(* TODO: Is there a better way for this? *)
locale nonground_term
begin

sublocale vars_def where vars_def = vars_term .

sublocale grounding_def where
  to_ground_def = gterm_of_term and from_ground_def = term_of_gterm .

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

sublocale nonground_term_properties where
  subst = "(⋅t)" and id_subst = Var and comp_subst = "(⊙)" and
  vars = "vars :: ('f, 'v) term ⇒ 'v set"
proof unfold_locales
  fix t :: "('f, 'v) term"  and σ τ :: "('f, 'v) subst"
  assume "⋀x. x ∈ vars t ⟹ σ x = τ x"
  then show "t ⋅t σ = t ⋅t τ"
    by(rule term_subst_eq)
next
  fix t :: "('f, 'v) term"
  show "finite (vars t)"
    by simp
next
  fix t :: "('f, 'v) term"
  show "(vars t = {}) = (∀σ. 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 t ≠ {}"
  then show "∃σ. t ⋅t σ ≠ 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 ⋅t σ ≠ Var x"
      using t'
      unfolding σ_def
      by auto

    moreover have "Var x ⋅t σ ∉ 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 a ≠ {}"
      using Fun.prems
      by fastforce

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

    then have "Fun f args ⋅t σ ≠ 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 ⋅t σ ∉ ts"
      using a a_σ_not_in_args
      by auto

    ultimately show ?case
      using Fun
      by blast
  qed
next
  fix t :: "('f, 'v) term" and ρ :: "('f, 'v) subst"

  show "vars (t ⋅t ρ) = ⋃ (vars ` ρ ` vars t)"
    using vars_term_subst.
next
  show "∃t. vars t = {}"
    using vars_term_of_gterm
    by metis
next
  fix x :: 'v
  show "vars (Var x) = {x}"
    by simp
next
  fix σ σ' :: "('f, 'v) subst" and x
  show "(σ ⊙ σ') x = σ x ⋅t σ'"
    unfolding subst_compose_def ..
qed

sublocale renaming_variables where
  vars = "vars :: ('f, 'v) term ⇒ 'v set" and subst = "(⋅t)" and id_subst = Var and
  comp_subst = "(⊙)"
proof unfold_locales
  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 (t ⋅t ρ) = rename ρ ` vars t"
  proof(induction t)
    case (Var x)
    have "ρ x = Var (rename ρ x)"
      using ρ
      unfolding 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
qed

sublocale term_grounding where
  subst = "(⋅t)" and id_subst = Var and comp_subst = "(⊙)" and
  vars = "vars :: ('f, 'v) term ⇒ 'v set" and from_ground = from_ground and
  to_ground = to_ground
proof unfold_locales
   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 (t ⋅t μ) ⊆ vars t ∪ ⋃ (vars ` ⋃ unifications)"
    using range_vars_subset_if_is_imgu[OF imgu] vars_term_subst_apply_term_subset
    by fastforce
next
  {
    fix t :: "('f, 'v) term"
    assume t_is_ground: "is_ground t"

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

      from t_is_ground
      show "from_ground (to_ground t) = t"
        by(induction t)(simp_all add: map_idI)

    qed
  }

  then show "{t :: ('f, 'v) term. is_ground t} = range from_ground"
    by fastforce
next
  fix t⇩G :: "('f) ground_term"
  show "to_ground (from_ground t⇩G) = t⇩G"
    by simp
qed

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

declare Term_Context.ground_vars_term_empty [simp del]

lemma obtain_ground_fun:
  assumes "is_ground t"
  obtains f ts where "t = Fun f ts"
  using assms
  by(cases t) auto

end

subsection ‹Setup for lifting from terms›

locale lifting =
  based_functional_substitution_lifting +
  all_subst_ident_iff_ground_lifting +
  grounding_lifting +
  renaming_variables_lifting +
  variables_in_base_imgu_lifting

locale term_based_lifting =
  "term": nonground_term +
  lifting where
  comp_subst = "(⊙)" and id_subst = Var and base_subst = "(⋅t)" and base_vars = term.vars

end