Theory Lambda_Free_Term

(*  Title:       Lambda-Free Higher-Order Terms
    Author:      Jasmin Blanchette <jasmin.blanchette at inria.fr>, 2016
    Maintainer:  Jasmin Blanchette <jasmin.blanchette at inria.fr>
*)

section ‹Lambda-Free Higher-Order Terms›

theory Lambda_Free_Term
imports Lambda_Free_Util
abbrevs ">s" = ">⇩s"
  and ">h" = ">⇩h⇩d"
  and "≤≥h" = "≤≥⇩h⇩d"
begin

text ‹
This theory defines ‹λ›-free higher-order terms and related locales.
›


subsection ‹Precedence on Symbols›

locale gt_sym =
  fixes
    gt_sym :: "'s ⇒ 's ⇒ bool" (infix ‹>⇩s› 50)
  assumes
    gt_sym_irrefl: "¬ f >⇩s f" and
    gt_sym_trans: "h >⇩s g ⟹ g >⇩s f ⟹ h >⇩s f" and
    gt_sym_total: "f >⇩s g ∨ g >⇩s f ∨ g = f" and
    gt_sym_wf: "wfP (λf g. g >⇩s f)"
begin

lemma gt_sym_antisym: "f >⇩s g ⟹ ¬ g >⇩s f"
  by (metis gt_sym_irrefl gt_sym_trans)

end


subsection ‹Heads›

datatype (plugins del: size) (syms_hd: 's, vars_hd: 'v) hd =
  is_Var: Var (var: 'v)
| Sym (sym: 's)

abbreviation is_Sym :: "('s, 'v) hd ⇒ bool" where
  "is_Sym ζ ≡ ¬ is_Var ζ"

lemma finite_vars_hd[simp]: "finite (vars_hd ζ)"
  by (cases ζ) auto

lemma finite_syms_hd[simp]: "finite (syms_hd ζ)"
  by (cases ζ) auto


subsection ‹Terms›

consts head0 :: 'a

datatype (syms: 's, vars: 'v) tm =
  is_Hd: Hd (head: "('s, 'v) hd")
| App ("fun": "('s, 'v) tm") (arg: "('s, 'v) tm")
where
  "head (App s _) = head0 s"
| "fun (Hd ζ) = Hd ζ"
| "arg (Hd ζ) = Hd ζ"

overloading head0 ≡ "head0 :: ('s, 'v) tm ⇒ ('s, 'v) hd"
begin

primrec head0 :: "('s, 'v) tm ⇒ ('s, 'v) hd" where
  "head0 (Hd ζ) = ζ"
| "head0 (App s _) = head0 s"

end

lemma head_App[simp]: "head (App s t) = head s"
  by (cases s) auto

declare tm.sel(2)[simp del]

lemma head_fun[simp]: "head (fun s) = head s"
  by (cases s) auto

abbreviation ground :: "('s, 'v) tm ⇒ bool" where
  "ground t ≡ vars t = {}"

abbreviation is_App :: "('s, 'v) tm ⇒ bool" where
  "is_App s ≡ ¬ is_Hd s"

lemma
  size_fun_lt: "is_App s ⟹ size (fun s) < size s" and
  size_arg_lt: "is_App s ⟹ size (arg s) < size s"
  by (cases s; simp)+

lemma
  finite_vars[simp]: "finite (vars s)" and
  finite_syms[simp]: "finite (syms s)"
  by (induct s) auto

lemma
  vars_head_subseteq: "vars_hd (head s) ⊆ vars s" and
  syms_head_subseteq: "syms_hd (head s) ⊆ syms s"
  by (induct s) auto

fun args :: "('s, 'v) tm ⇒ ('s, 'v) tm list" where
  "args (Hd _) = []"
| "args (App s t) = args s @ [t]"

lemma set_args_fun: "set (args (fun s)) ⊆ set (args s)"
  by (cases s) auto

lemma arg_in_args: "is_App s ⟹ arg s ∈ set (args s)"
  by (cases s rule: tm.exhaust) auto

lemma
  vars_args_subseteq: "si ∈ set (args s) ⟹ vars si ⊆ vars s" and
  syms_args_subseteq: "si ∈ set (args s) ⟹ syms si ⊆ syms s"
  by (induct s) auto

lemma args_Nil_iff_is_Hd: "args s = [] ⟷ is_Hd s"
  by (cases s) auto

abbreviation num_args :: "('s, 'v) tm ⇒ nat" where
  "num_args s ≡ length (args s)"

lemma size_ge_num_args: "size s ≥ num_args s"
  by (induct s) auto

lemma Hd_head_id: "num_args s = 0 ⟹ Hd (head s) = s"
  by (metis args.cases args.simps(2) length_0_conv snoc_eq_iff_butlast tm.collapse(1) tm.disc(1))

lemma one_arg_imp_Hd: "num_args s = 1 ⟹ s = App t u ⟹ t = Hd (head t)"
  by (simp add: Hd_head_id)

lemma size_in_args: "s ∈ set (args t) ⟹ size s < size t"
  by (induct t) auto

primrec apps :: "('s, 'v) tm ⇒ ('s, 'v) tm list ⇒ ('s, 'v) tm" where
  "apps s [] = s"
| "apps s (t # ts) = apps (App s t) ts"

lemma
  vars_apps[simp]: "vars (apps s ss) = vars s ∪ (⋃s ∈ set ss. vars s)" and
  syms_apps[simp]: "syms (apps s ss) = syms s ∪ (⋃s ∈ set ss. syms s)" and
  head_apps[simp]: "head (apps s ss) = head s" and
  args_apps[simp]: "args (apps s ss) = args s @ ss" and
  is_App_apps[simp]: "is_App (apps s ss) ⟷ args (apps s ss) ≠ []" and
  fun_apps_Nil[simp]: "fun (apps s []) = fun s" and
  fun_apps_Cons[simp]: "fun (apps (App s sa) ss) = apps s (butlast (sa # ss))" and
  arg_apps_Nil[simp]: "arg (apps s []) = arg s" and
  arg_apps_Cons[simp]: "arg (apps (App s sa) ss) = last (sa # ss)"
  by (induct ss arbitrary: s sa) (auto simp: args_Nil_iff_is_Hd)

lemma apps_append[simp]: "apps s (ss @ ts) = apps (apps s ss) ts"
  by (induct ss arbitrary: s ts) auto

lemma App_apps: "App (apps s ts) t = apps s (ts @ [t])"
  by simp

lemma tm_inject_apps[iff, induct_simp]: "apps (Hd ζ) ss = apps (Hd ξ) ts ⟷ ζ = ξ ∧ ss = ts"
  by (metis args_apps head_apps same_append_eq tm.sel(1))

lemma tm_collapse_apps[simp]: "apps (Hd (head s)) (args s) = s"
  by (induct s) auto

lemma tm_expand_apps: "head s = head t ⟹ args s = args t ⟹ s = t"
  by (metis tm_collapse_apps)

lemma tm_exhaust_apps_sel[case_names apps]: "(s = apps (Hd (head s)) (args s) ⟹ P) ⟹ P"
  by (atomize_elim, induct s) auto

lemma tm_exhaust_apps[case_names apps]: "(⋀ζ ss. s = apps (Hd ζ) ss ⟹ P) ⟹ P"
  by (metis tm_collapse_apps)

lemma tm_induct_apps[case_names apps]:
  assumes "⋀ζ ss. (⋀s. s ∈ set ss ⟹ P s) ⟹ P (apps (Hd ζ) ss)"
  shows "P s"
  using assms
  by (induct s taking: size rule: measure_induct_rule) (metis size_in_args tm_collapse_apps)

lemma
  ground_fun: "ground s ⟹ ground (fun s)" and
  ground_arg: "ground s ⟹ ground (arg s)"
  by (induct s) auto

lemma ground_head: "ground s ⟹ is_Sym (head s)"
  by (cases s rule: tm_exhaust_apps) (auto simp: is_Var_def)

lemma ground_args: "t ∈ set (args s) ⟹ ground s ⟹ ground t"
  by (induct s rule: tm_induct_apps) auto

primrec vars_mset :: "('s, 'v) tm ⇒ 'v multiset" where
  "vars_mset (Hd ζ) = mset_set (vars_hd ζ)"
| "vars_mset (App s t) = vars_mset s + vars_mset t"

lemma set_vars_mset[simp]: "set_mset (vars_mset t) = vars t"
  by (induct t) auto

lemma vars_mset_empty_iff[iff]: "vars_mset s = {#} ⟷ ground s"
  by (induct s) (auto simp: mset_set_empty_iff)

lemma vars_mset_fun[intro]: "vars_mset (fun t) ⊆# vars_mset t"
  by (cases t) auto

lemma vars_mset_arg[intro]: "vars_mset (arg t) ⊆# vars_mset t"
  by (cases t) auto


subsection ‹hsize›

text ‹The hsize of a term is the number of heads (Syms or Vars) in the term.›

primrec hsize :: "('s, 'v) tm ⇒ nat" where
  "hsize (Hd ζ) = 1"
| "hsize (App s t) = hsize s + hsize t"

lemma hsize_size: "hsize t * 2 = size t + 1"
  by (induct t) auto

lemma hsize_pos[simp]: "hsize t > 0"
  by (induction t; simp)

lemma hsize_fun_lt: "is_App s ⟹ hsize (fun s) < hsize s"
  by (cases s; simp)

lemma hsize_arg_lt: "is_App s ⟹ hsize (arg s) < hsize s"
  by (cases s; simp)
  
lemma hsize_ge_num_args: "hsize s ≥ hsize s"
  by (induct s) auto

lemma hsize_in_args: "s ∈ set (args t) ⟹ hsize s < hsize t"
  by (induct t) auto

lemma hsize_apps: "hsize (apps t ts) = hsize t + sum_list (map hsize ts)"
  by (induct ts arbitrary:t; simp)

lemma hsize_args: "1 + sum_list (map hsize (args t)) = hsize t"
  by (metis hsize.simps(1) hsize_apps tm_collapse_apps)


subsection ‹Substitutions›

primrec subst :: "('v ⇒ ('s, 'v) tm) ⇒ ('s, 'v) tm ⇒ ('s, 'v) tm" where
  "subst ρ (Hd ζ) = (case ζ of Var x ⇒ ρ x | Sym f ⇒ Hd (Sym f))"
| "subst ρ (App s t) = App (subst ρ s) (subst ρ t)"

lemma subst_apps[simp]: "subst ρ (apps s ts) = apps (subst ρ s) (map (subst ρ) ts)"
  by (induct ts arbitrary: s) auto

lemma head_subst[simp]: "head (subst ρ s) = head (subst ρ (Hd (head s)))"
  by (cases s rule: tm_exhaust_apps) (auto split: hd.split)

lemma args_subst[simp]:
  "args (subst ρ s) = (case head s of Var x ⇒ args (ρ x) | Sym f ⇒ []) @ map (subst ρ) (args s)"
  by (cases s rule: tm_exhaust_apps) (auto split: hd.split)

lemma ground_imp_subst_iden: "ground s ⟹ subst ρ s = s"
  by (induct s) (auto split: hd.split)

lemma vars_mset_subst[simp]: "vars_mset (subst ρ s) = (∑⇩# {#vars_mset (ρ x). x ∈# vars_mset s#})"
proof (induct s)
  case (Hd ζ)
  show ?case
    by (cases ζ) auto
qed auto

lemma vars_mset_subst_subseteq:
  "vars_mset t ⊇# vars_mset s ⟹ vars_mset (subst ρ t) ⊇# vars_mset (subst ρ s)"
  unfolding vars_mset_subst
  by (metis (no_types) add_diff_cancel_right' diff_subset_eq_self image_mset_union sum_mset.union
    subset_mset.add_diff_inverse)

lemma vars_subst_subseteq: "vars t ⊇ vars s ⟹ vars (subst ρ t) ⊇ vars (subst ρ s)"
  unfolding set_vars_mset[symmetric] vars_mset_subst by auto


subsection ‹Subterms›

inductive sub :: "('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool" where
  sub_refl: "sub s s"
| sub_fun: "sub s t ⟹ sub s (App u t)"
| sub_arg: "sub s t ⟹ sub s (App t u)"

inductive_cases sub_HdE[simplified, elim]: "sub s (Hd ξ)"
inductive_cases sub_AppE[simplified, elim]: "sub s (App t u)"
inductive_cases sub_Hd_HdE[simplified, elim]: "sub (Hd ζ) (Hd ξ)"
inductive_cases sub_Hd_AppE[simplified, elim]: "sub (Hd ζ) (App t u)"

lemma in_vars_imp_sub: "x ∈ vars s ⟷ sub (Hd (Var x)) s"
  by induct (auto intro: sub.intros elim: hd.set_cases(2))

lemma sub_args: "s ∈ set (args t) ⟹ sub s t"
  by (induct t) (auto intro: sub.intros)

lemma sub_size: "sub s t ⟹ size s ≤ size t"
  by induct auto

lemma sub_subst: "sub s t ⟹ sub (subst ρ s) (subst ρ t)"
proof (induct t)
  case (Hd ζ)
  thus ?case
    by (cases ζ; blast intro: sub.intros)
qed (auto intro: sub.intros del: sub_AppE elim!: sub_AppE)

abbreviation proper_sub :: "('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool" where
  "proper_sub s t ≡ sub s t ∧ s ≠ t"

lemma proper_sub_Hd[simp]: "¬ proper_sub s (Hd ζ)"
  using sub.cases by blast

lemma proper_sub_subst:
  assumes psub: "proper_sub s t"
  shows "proper_sub (subst ρ s) (subst ρ t)"
proof (cases t)
  case Hd
  thus ?thesis
    using psub by simp
next
  case t: (App t1 t2)
  have "sub s t1 ∨ sub s t2"
    using t psub by blast
  hence "sub (subst ρ s) (subst ρ t1) ∨ sub (subst ρ s) (subst ρ t2)"
    using sub_subst by blast
  thus ?thesis
    unfolding t by (auto intro: sub.intros dest: sub_size)
qed


subsection ‹Maximum Arities›

locale arity =
  fixes
    arity_sym :: "'s ⇒ enat" and
    arity_var :: "'v ⇒ enat"
begin

primrec arity_hd :: "('s, 'v) hd ⇒ enat" where
  "arity_hd (Var x) = arity_var x"
| "arity_hd (Sym f) = arity_sym f"

definition arity :: "('s, 'v) tm ⇒ enat" where
  "arity s = arity_hd (head s) - num_args s"

lemma arity_simps[simp]:
  "arity (Hd ζ) = arity_hd ζ"
  "arity (App s t) = arity s - 1"
  by (auto simp: arity_def enat_diff_diff_eq add.commute eSuc_enat plus_1_eSuc(1))

lemma arity_apps[simp]: "arity (apps s ts) = arity s - length ts"
proof (induct ts arbitrary: s)
  case (Cons t ts)
  thus ?case
    by (case_tac "arity s"; simp add: one_enat_def)
qed simp

inductive wary :: "('s, 'v) tm ⇒ bool" where
  wary_Hd[intro]: "wary (Hd ζ)"
| wary_App[intro]: "wary s ⟹ wary t ⟹ num_args s < arity_hd (head s) ⟹ wary (App s t)"

inductive_cases wary_HdE: "wary (Hd ζ)"
inductive_cases wary_AppE: "wary (App s t)"
inductive_cases wary_binaryE[simplified]: "wary (App (App s t) u)"

lemma wary_fun[intro]: "wary t ⟹ wary (fun t)"
  by (cases t) (auto elim: wary.cases)

lemma wary_arg[intro]: "wary t ⟹ wary (arg t)"
  by (cases t) (auto elim: wary.cases)

lemma wary_args: "s ∈ set (args t) ⟹ wary t ⟹ wary s"
  by (induct t arbitrary: s, simp)
   (metis Un_iff args.simps(2) wary.cases insert_iff length_pos_if_in_set
      less_numeral_extra(3) list.set(2) list.size(3) set_append tm.distinct(1) tm.inject(2))

lemma wary_sub: "sub s t ⟹ wary t ⟹ wary s"
  by (induct rule: sub.induct) (auto elim: wary.cases)

lemma wary_inf_ary: "(⋀ζ. arity_hd ζ = ∞) ⟹ wary s"
  by induct auto

lemma wary_num_args_le_arity_head: "wary s ⟹ num_args s ≤ arity_hd (head s)"
  by (induct rule: wary.induct) (auto simp: zero_enat_def[symmetric] Suc_ile_eq)

lemma wary_apps:
  "wary s ⟹ (⋀sa. sa ∈ set ss ⟹ wary sa) ⟹ length ss ≤ arity s ⟹ wary (apps s ss)"
proof (induct ss arbitrary: s)
  case (Cons sa ss)
  note ih = this(1) and wary_s = this(2) and wary_ss = this(3) and nargs_s_sa_ss = this(4)
  show ?case
    unfolding apps.simps
  proof (rule ih)
    have "wary sa"
      using wary_ss by simp
    moreover have " enat (num_args s) < arity_hd (head s)"
      by (metis (mono_tags) One_nat_def add.comm_neutral arity_def diff_add_zero enat_ord_simps(1)
        idiff_enat_enat less_one list.size(4) nargs_s_sa_ss not_add_less2
        order.not_eq_order_implies_strict wary_num_args_le_arity_head wary_s)
    ultimately show "wary (App s sa)"
      by (rule wary_App[OF wary_s])
  next
    show "⋀sa. sa ∈ set ss ⟹ wary sa"
      using wary_ss by simp
  next
    show "length ss ≤ arity (App s sa)"
    proof (cases "arity s")
      case enat
      thus ?thesis
        using nargs_s_sa_ss by (simp add: one_enat_def)
    qed simp
  qed
qed simp

lemma wary_cases_apps[consumes 1, case_names apps]:
  assumes
    wary_t: "wary t" and
    apps: "⋀ζ ss. t = apps (Hd ζ) ss ⟹ (⋀sa. sa ∈ set ss ⟹ wary sa) ⟹ length ss ≤ arity_hd ζ ⟹ P"
  shows P
  using apps
proof (atomize_elim, cases t rule: tm_exhaust_apps)
  case t: (apps ζ ss)
  show "∃ζ ss. t = apps (Hd ζ) ss ∧ (∀sa. sa ∈ set ss ⟶ wary sa) ∧ enat (length ss) ≤ arity_hd ζ"
    by (rule exI[of _ ζ], rule exI[of _ ss])
      (auto simp: t wary_args[OF _ wary_t] wary_num_args_le_arity_head[OF wary_t, unfolded t, simplified])
qed

lemma arity_hd_head: "wary s ⟹ arity_hd (head s) = arity s + num_args s"
  by (simp add: arity_def enat_sub_add_same wary_num_args_le_arity_head)

lemma arity_head_ge: "arity_hd (head s) ≥ arity s"
  by (induct s) (auto intro: enat_le_imp_minus_le)

inductive wary_fo :: "('s, 'v) tm ⇒ bool" where
  wary_foI[intro]: "is_Hd s ∨ is_Sym (head s) ⟹ length (args s) = arity_hd (head s) ⟹
    (∀t ∈ set (args s). wary_fo t) ⟹ wary_fo s"

lemma wary_fo_args: "s ∈ set (args t) ⟹ wary_fo t ⟹ wary_fo s"
  by (induct t arbitrary: s rule: tm_induct_apps, simp)
    (metis args.simps(1) args_apps self_append_conv2 wary_fo.cases)

lemma wary_fo_arg: "wary_fo (App s t) ⟹ wary_fo t"
  by (erule wary_fo.cases) auto

end


subsection ‹Potential Heads of Ground Instances of Variables›

locale ground_heads = gt_sym "(>⇩s)" + arity arity_sym arity_var
    for
      gt_sym :: "'s ⇒ 's ⇒ bool" (infix ‹>⇩s› 50) and
      arity_sym :: "'s ⇒ enat" and
      arity_var :: "'v ⇒ enat" +
  fixes
    ground_heads_var :: "'v ⇒ 's set"
  assumes
    ground_heads_var_arity: "f ∈ ground_heads_var x ⟹ arity_sym f ≥ arity_var x" and
    ground_heads_var_nonempty: "ground_heads_var x ≠ {}"
begin

primrec ground_heads :: "('s, 'v) hd ⇒ 's set" where
  "ground_heads (Var x) = ground_heads_var x"
| "ground_heads (Sym f) = {f}"

lemma ground_heads_arity: "f ∈ ground_heads ζ ⟹ arity_sym f ≥ arity_hd ζ"
  by (cases ζ) (auto simp: ground_heads_var_arity)

lemma ground_heads_nonempty[simp]: "ground_heads ζ ≠ {}"
  by (cases ζ) (auto simp: ground_heads_var_nonempty)

lemma sym_in_ground_heads: "is_Sym ζ ⟹ sym ζ ∈ ground_heads ζ"
  by (metis ground_heads.simps(2) hd.collapse(2) hd.set_sel(1) hd.simps(16))

lemma ground_hd_in_ground_heads: "ground s ⟹ sym (head s) ∈ ground_heads (head s)"
  by (simp add: ground_head sym_in_ground_heads)

lemma some_ground_head_arity: "arity_sym (SOME f. f ∈ ground_heads (Var x)) ≥ arity_var x"
  by (simp add: ground_heads_var_arity ground_heads_var_nonempty some_in_eq)

definition wary_subst :: "('v ⇒ ('s, 'v) tm) ⇒ bool" where
  "wary_subst ρ ⟷
   (∀x. wary (ρ x) ∧ arity (ρ x) ≥ arity_var x ∧ ground_heads (head (ρ x)) ⊆ ground_heads_var x)"

definition strict_wary_subst :: "('v ⇒ ('s, 'v) tm) ⇒ bool" where
  "strict_wary_subst ρ ⟷
   (∀x. wary (ρ x) ∧ arity (ρ x) ∈ {arity_var x, ∞}
    ∧ ground_heads (head (ρ x)) ⊆ ground_heads_var x)"

lemma strict_imp_wary_subst: "strict_wary_subst ρ ⟹ wary_subst ρ"
  unfolding strict_wary_subst_def wary_subst_def using eq_iff by force

lemma wary_subst_wary:
  assumes wary_ρ: "wary_subst ρ" and wary_s: "wary s"
  shows "wary (subst ρ s)"
  using wary_s
proof (induct s rule: tm.induct)
  case (App s t)
  note wary_st = this(3)
  from wary_st have wary_s: "wary s"
    by (rule wary_AppE)
  from wary_st have wary_t: "wary t"
    by (rule wary_AppE)
  from wary_st have nargs_s_lt: "num_args s < arity_hd (head s)"
    by (rule wary_AppE)

  note wary_ρs = App(1)[OF wary_s]
  note wary_ρt = App(2)[OF wary_t]

  note wary_ρx = wary_ρ[unfolded wary_subst_def, rule_format, THEN conjunct1]
  note ary_ρx = wary_ρ[unfolded wary_subst_def, rule_format, THEN conjunct2]

  have "num_args (ρ x) + num_args s < arity_hd (head (ρ x))" if hd_s: "head s = Var x" for x
  proof -
    have ary_hd_s: "arity_hd (head s) = arity_var x"
      using hd_s arity_hd.simps(1) by presburger
    hence "num_args s ≤ arity (ρ x)"
      by (metis (no_types) wary_num_args_le_arity_head ary_ρx dual_order.trans wary_s)
    hence "num_args s + num_args (ρ x) ≤ arity_hd (head (ρ x))"
      by (metis (no_types) arity_hd_head[OF wary_ρx] add_right_mono plus_enat_simps(1))
    thus ?thesis
      using ary_hd_s by (metis (no_types) add.commute add_diff_cancel_left' ary_ρx arity_def
        idiff_enat_enat leD nargs_s_lt order.not_eq_order_implies_strict)
  qed
  hence nargs_ρs: "num_args (subst ρ s) < arity_hd (head (subst ρ s))"
    using nargs_s_lt by (auto split: hd.split)

  show ?case
    by simp (rule wary_App[OF wary_ρs wary_ρt nargs_ρs])
qed (auto simp: wary_ρ[unfolded wary_subst_def] split: hd.split)

lemmas strict_wary_subst_wary = wary_subst_wary[OF strict_imp_wary_subst]

lemma wary_subst_ground_heads:
  assumes wary_ρ: "wary_subst ρ"
  shows "ground_heads (head (subst ρ s)) ⊆ ground_heads (head s)"
proof (induct s rule: tm_induct_apps)
  case (apps ζ ss)
  show ?case
  proof (cases ζ)
    case x: (Var x)
    thus ?thesis
      using wary_ρ wary_subst_def x by auto
  qed auto
qed

lemmas strict_wary_subst_ground_heads = wary_subst_ground_heads[OF strict_imp_wary_subst]

definition grounding_ρ :: "'v ⇒ ('s, 'v) tm" where
  "grounding_ρ x = (let s = Hd (Sym (SOME f. f ∈ ground_heads_var x)) in
     apps s (replicate (the_enat (arity s - arity_var x)) s))"

lemma ground_grounding_ρ: "ground (subst grounding_ρ s)"
  by (induct s) (auto simp: Let_def grounding_ρ_def elim: hd.set_cases(2) split: hd.split)

lemma strict_wary_grounding_ρ: "strict_wary_subst grounding_ρ"
  unfolding strict_wary_subst_def
proof (intro allI conjI)
  fix x

  define f where "f = (SOME f. f ∈ ground_heads_var x)"
  define s :: "('s, 'v) tm" where "s = Hd (Sym f)"

  have wary_s: "wary s"
    unfolding s_def by (rule wary_Hd)
  have ary_s_ge_x: "arity s ≥ arity_var x"
    unfolding s_def f_def using some_ground_head_arity by simp
  have grρ_x: "grounding_ρ x = apps s (replicate (the_enat (arity s - arity_var x)) s)"
    unfolding grounding_ρ_def Let_def f_def[symmetric] s_def[symmetric] by (rule refl)

  show "wary (grounding_ρ x)"
    unfolding grρ_x by (auto intro!: wary_s wary_apps[OF wary_s] enat_the_enat_minus_le)
  show "arity (grounding_ρ x) ∈ {arity_var x, ∞}"
    unfolding grρ_x using ary_s_ge_x by (cases "arity s"; cases "arity_var x"; simp)
  show "ground_heads (head (grounding_ρ x)) ⊆ ground_heads_var x"
    unfolding grρ_x s_def f_def by (simp add: some_in_eq ground_heads_var_nonempty)
qed

lemmas wary_grounding_ρ = strict_wary_grounding_ρ[THEN strict_imp_wary_subst]

definition gt_hd :: "('s, 'v) hd ⇒ ('s, 'v) hd ⇒ bool" (infix ‹>⇩h⇩d› 50) where
  "ξ >⇩h⇩d ζ ⟷ (∀g ∈ ground_heads ξ. ∀f ∈ ground_heads ζ. g >⇩s f)"

definition comp_hd :: "('s, 'v) hd ⇒ ('s, 'v) hd ⇒ bool" (infix ‹≤≥⇩h⇩d› 50) where
  "ξ ≤≥⇩h⇩d ζ ⟷ ξ = ζ ∨ ξ >⇩h⇩d ζ ∨ ζ >⇩h⇩d ξ"

lemma gt_hd_irrefl: "¬ ζ >⇩h⇩d ζ"
  unfolding gt_hd_def using gt_sym_irrefl by (meson ex_in_conv ground_heads_nonempty)

lemma gt_hd_trans: "χ >⇩h⇩d ξ ⟹ ξ >⇩h⇩d ζ ⟹ χ >⇩h⇩d ζ"
  unfolding gt_hd_def using gt_sym_trans by (meson ex_in_conv ground_heads_nonempty)

lemma gt_sym_imp_hd: "g >⇩s f ⟹ Sym g >⇩h⇩d Sym f"
  unfolding gt_hd_def by simp

lemma not_comp_hd_imp_Var: "¬ ξ ≤≥⇩h⇩d ζ ⟹ is_Var ζ ∨ is_Var ξ"
  using gt_sym_total by (cases ζ; cases ξ; auto simp: comp_hd_def gt_hd_def)

end

end