Theory Lambda_Free_RPO_Std

(*  Title:       The Graceful Recursive Path Order for Lambda-Free Higher-Order Terms
    Author:      Jasmin Blanchette <jasmin.blanchette at inria.fr>, 2016
    Author:      Uwe Waldmann <waldmann at mpi-inf.mpg.de>, 2016
    Author:      Daniel Wand <dwand at mpi-inf.mpg.de>, 2016
    Maintainer:  Jasmin Blanchette <jasmin.blanchette at inria.fr>
*)

section ‹The Graceful Recursive Path Order for Lambda-Free Higher-Order Terms›

theory Lambda_Free_RPO_Std
imports Lambda_Free_Term Extension_Orders Nested_Multisets_Ordinals.Multiset_More
abbrevs ">t" = ">t"
  and "≥t" = "≥t"
begin

text ‹
This theory defines the graceful recursive path order (RPO) for ‹λ›-free
higher-order terms.
›


subsection ‹Setup›

locale rpo_basis = ground_heads "(>s)" arity_sym arity_var
    for
      gt_sym :: "'s ⇒ 's ⇒ bool" (infix ‹>s› 50) and
      arity_sym :: "'s ⇒ enat" and
      arity_var :: "'v ⇒ enat" +
  fixes
    extf :: "'s ⇒ (('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool) ⇒ ('s, 'v) tm list ⇒ ('s, 'v) tm list ⇒ bool"
  assumes
    extf_ext_trans_before_irrefl: "ext_trans_before_irrefl (extf f)" and
    extf_ext_compat_cons: "ext_compat_cons (extf f)" and
    extf_ext_compat_list: "ext_compat_list (extf f)"
begin

lemma extf_ext_trans: "ext_trans (extf f)"
  by (rule ext_trans_before_irrefl.axioms(1)[OF extf_ext_trans_before_irrefl])

lemma extf_ext: "ext (extf f)"
  by (rule ext_trans.axioms(1)[OF extf_ext_trans])

lemmas extf_mono_strong = ext.mono_strong[OF extf_ext]
lemmas extf_mono = ext.mono[OF extf_ext, mono]
lemmas extf_map = ext.map[OF extf_ext]
lemmas extf_trans = ext_trans.trans[OF extf_ext_trans]
lemmas extf_irrefl_from_trans =
  ext_trans_before_irrefl.irrefl_from_trans[OF extf_ext_trans_before_irrefl]
lemmas extf_compat_append_left = ext_compat_cons.compat_append_left[OF extf_ext_compat_cons]
lemmas extf_compat_list = ext_compat_list.compat_list[OF extf_ext_compat_list]

definition chkvar :: "('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool" where
  [simp]: "chkvar t s ⟷ vars_hd (head s) ⊆ vars t"

end

locale rpo = rpo_basis _ _ arity_sym arity_var
  for
    arity_sym :: "'s ⇒ enat" and
    arity_var :: "'v ⇒ enat"
begin


subsection ‹Inductive Definitions›

definition
  chksubs :: "(('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool) ⇒ ('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool"
where
  [simp]: "chksubs gt t s ⟷ (case s of App s1 s2 ⇒ gt t s1 ∧ gt t s2 | _ ⇒ True)"

lemma chksubs_mono[mono]: "gt ≤ gt' ⟹ chksubs gt ≤ chksubs gt'"
  by (auto simp: tm.case_eq_if) force+

inductive gt :: "('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool" (infix ‹>t› 50) where
  gt_sub: "is_App t ⟹ (fun t >t s ∨ fun t = s) ∨ (arg t >t s ∨ arg t = s) ⟹ t >t s"
| gt_diff: "head t >hd head s ⟹ chkvar t s ⟹ chksubs (>t) t s ⟹ t >t s"
| gt_same: "head t = head s ⟹ chksubs (>t) t s ⟹
    (∀f ∈ ground_heads (head t). extf f (>t) (args t) (args s)) ⟹ t >t s"

abbreviation ge :: "('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool" (infix ‹≥t› 50) where
  "t ≥t s ≡ t >t s ∨ t = s"

inductive gt_sub :: "('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool" where
  gt_subI: "is_App t ⟹ fun t ≥t s ∨ arg t ≥t s ⟹ gt_sub t s"

inductive gt_diff :: "('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool" where
  gt_diffI: "head t >hd head s ⟹ chkvar t s ⟹ chksubs (>t) t s ⟹ gt_diff t s"

inductive gt_same :: "('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool" where
  gt_sameI: "head t = head s ⟹ chksubs (>t) t s ⟹
    (∀f ∈ ground_heads (head t). extf f (>t) (args t) (args s)) ⟹ gt_same t s"

lemma gt_iff_sub_diff_same: "t >t s ⟷ gt_sub t s ∨ gt_diff t s ∨ gt_same t s"
  by (subst gt.simps) (auto simp: gt_sub.simps gt_diff.simps gt_same.simps)


subsection ‹Transitivity›

lemma gt_fun_imp: "fun t >t s ⟹ t >t s"
  by (cases t) (auto intro: gt_sub)

lemma gt_arg_imp: "arg t >t s ⟹ t >t s"
  by (cases t) (auto intro: gt_sub)

lemma gt_imp_vars: "t >t s ⟹ vars t ⊇ vars s"
proof (simp only: atomize_imp,
    rule measure_induct_rule[of "λ(t, s). size t + size s"
      "λ(t, s). t >t s ⟶ vars t ⊇ vars s" "(t, s)", simplified prod.case],
    simp only: split_paired_all prod.case atomize_imp[symmetric])
  fix t s
  assume
    ih: "⋀ta sa. size ta + size sa < size t + size s ⟹ ta >t sa ⟹ vars ta ⊇ vars sa" and
    t_gt_s: "t >t s"
  show "vars t ⊇ vars s"
    using t_gt_s
  proof cases
    case gt_sub
    thus ?thesis
      using ih[of "fun t" s] ih[of "arg t" s]
      by (meson add_less_cancel_right subsetD size_arg_lt size_fun_lt subsetI tm.set_sel(5,6))
  next
    case gt_diff
    show ?thesis
    proof (cases s)
      case Hd
      thus ?thesis
        using gt_diff(2) by (auto elim: hd.set_cases(2))
    next
      case (App s1 s2)
      thus ?thesis
        using gt_diff(3) ih[of t s1] ih[of t s2] by simp
    qed
  next
    case gt_same
    show ?thesis
    proof (cases s)
      case Hd
      thus ?thesis
        using gt_same(1) vars_head_subseteq by fastforce
    next
      case (App s1 s2)
      thus ?thesis
        using gt_same(2) ih[of t s1] ih[of t s2] by simp
    qed
  qed
qed

theorem gt_trans: "u >t t ⟹ t >t s ⟹ u >t s"
proof (simp only: atomize_imp,
    rule measure_induct_rule[of "λ(u, t, s). {#size u, size t, size s#}"
        "λ(u, t, s). u >t t ⟶ t >t s ⟶ u >t s" "(u, t, s)",
      simplified prod.case],
    simp only: split_paired_all prod.case atomize_imp[symmetric])
  fix u t s
  assume
    ih: "⋀ua ta sa. {#size ua, size ta, size sa#} < {#size u, size t, size s#} ⟹
      ua >t ta ⟹ ta >t sa ⟹ ua >t sa" and
    u_gt_t: "u >t t" and t_gt_s: "t >t s"

  have chkvar: "chkvar u s"
    by (metis (no_types, lifting) chkvar_def gt_imp_vars order_le_less order_le_less_trans t_gt_s
        u_gt_t vars_head_subseteq)

  have chk_u_s_if: "chksubs (>t) u s" if chk_t_s: "chksubs (>t) t s"
  proof (cases s)
    case (App s1 s2)
    thus ?thesis
      using chk_t_s by (auto intro: ih[of _ _ s1, OF _ u_gt_t] ih[of _ _ s2, OF _ u_gt_t])
  qed auto

  have
    fun_u_lt_etc: "is_App u ⟹ {#size (fun u), size t, size s#} < {#size u, size t, size s#}" and
    arg_u_lt_etc: "is_App u ⟹ {#size (arg u), size t, size s#} < {#size u, size t, size s#}"
    by (simp_all add: size_fun_lt size_arg_lt)

  have u_gt_s_if_ui: "is_App u ⟹ fun u ≥t t ∨ arg u ≥t t ⟹ u >t s"
    using ih[of "fun u" t s, OF fun_u_lt_etc] ih[of "arg u" t s, OF arg_u_lt_etc] gt_arg_imp
      gt_fun_imp t_gt_s by blast

  show "u >t s"
    using t_gt_s
  proof cases
    case gt_sub_t_s: gt_sub

    have u_gt_s_if_chk_u_t: ?thesis if chk_u_t: "chksubs (>t) u t"
      using gt_sub_t_s(1)
    proof (cases t)
      case t: (App t1 t2)
      show ?thesis
        using ih[of u t1 s] ih[of u t2 s] gt_sub_t_s(2) chk_u_t unfolding t by auto
    qed auto

    show ?thesis
      using u_gt_t by cases (auto intro: u_gt_s_if_ui u_gt_s_if_chk_u_t)
  next
    case gt_diff_t_s: gt_diff
    show ?thesis
      using u_gt_t
    proof cases
      case gt_diff_u_t: gt_diff
      have "head u >hd head s"
        using gt_diff_u_t(1) gt_diff_t_s(1) by (auto intro: gt_hd_trans)
      thus ?thesis
        by (rule gt_diff[OF _ chkvar chk_u_s_if[OF gt_diff_t_s(3)]])
    next
      case gt_same_u_t: gt_same
      have "head u >hd head s"
        using gt_diff_t_s(1) gt_same_u_t(1) by auto
      thus ?thesis
        by (rule gt_diff[OF _ chkvar chk_u_s_if[OF gt_diff_t_s(3)]])
    qed (auto intro: u_gt_s_if_ui)
  next
    case gt_same_t_s: gt_same
    show ?thesis
      using u_gt_t
    proof cases
      case gt_diff_u_t: gt_diff
      have "head u >hd head s"
        using gt_diff_u_t(1) gt_same_t_s(1) by simp
      thus ?thesis
        by (rule gt_diff[OF _ chkvar chk_u_s_if[OF gt_same_t_s(2)]])
    next
      case gt_same_u_t: gt_same
      have hd_u_s: "head u = head s"
        using gt_same_u_t(1) gt_same_t_s(1) by simp

      let ?S = "set (args u) ∪ set (args t) ∪ set (args s)"

      have gt_trans_args: "∀ua ∈ ?S. ∀ta ∈ ?S. ∀sa ∈ ?S. ua >t ta ⟶ ta >t sa ⟶ ua >t sa"
      proof clarify
        fix sa ta ua
        assume
          ua_in: "ua ∈ ?S" and ta_in: "ta ∈ ?S" and sa_in: "sa ∈ ?S" and
          ua_gt_ta: "ua >t ta" and ta_gt_sa: "ta >t sa"
        show "ua >t sa"
          by (auto intro!: ih[OF Max_lt_imp_lt_mset ua_gt_ta ta_gt_sa])
            (meson ua_in ta_in sa_in Un_iff max.strict_coboundedI1 max.strict_coboundedI2
               size_in_args)+
      qed

      have "∀f ∈ ground_heads (head u). extf f (>t) (args u) (args s)"
      proof (clarify, rule extf_trans[OF _ _ _ gt_trans_args])
        fix f
        assume f_in_grounds: "f ∈ ground_heads (head u)"
        show "extf f (>t) (args u) (args t)"
          using f_in_grounds gt_same_u_t(3) by blast
        show "extf f (>t) (args t) (args s)"
          using f_in_grounds gt_same_t_s(3) unfolding gt_same_u_t(1) by blast
      qed auto
      thus ?thesis
        by (rule gt_same[OF hd_u_s chk_u_s_if[OF gt_same_t_s(2)]])
    qed (auto intro: u_gt_s_if_ui)
  qed
qed


subsection ‹Irreflexivity›

theorem gt_irrefl: "¬ s >t s"
proof (standard, induct s rule: measure_induct_rule[of size])
  case (less s)
  note ih = this(1) and s_gt_s = this(2)

  show False
    using s_gt_s
  proof cases
    case _: gt_sub
    note is_app = this(1) and si_ge_s = this(2)
    have s_gt_fun_s: "s >t fun s" and s_gt_arg_s: "s >t arg s"
      using is_app by (simp_all add: gt_sub)

    have "fun s >t s ∨ arg s >t s"
      using si_ge_s is_app s_gt_arg_s s_gt_fun_s by auto
    moreover
    {
      assume fun_s_gt_s: "fun s >t s"
      have "fun s >t fun s"
        by (rule gt_trans[OF fun_s_gt_s s_gt_fun_s])
      hence False
        using ih[of "fun s"] is_app size_fun_lt by blast
    }
    moreover
    {
      assume arg_s_gt_s: "arg s >t s"
      have "arg s >t arg s"
        by (rule gt_trans[OF arg_s_gt_s s_gt_arg_s])
      hence False
        using ih[of "arg s"] is_app size_arg_lt by blast
    }
    ultimately show False
      by sat
  next
    case gt_diff
    thus False
      by (cases "head s") (auto simp: gt_hd_irrefl)
  next
    case gt_same
    note in_grounds = this(3)

    obtain si where si_in_args: "si ∈ set (args s)" and si_gt_si: "si >t si"
      using in_grounds
      by (metis (full_types) all_not_in_conv extf_irrefl_from_trans ground_heads_nonempty gt_trans)
    have "size si < size s"
      by (rule size_in_args[OF si_in_args])
    thus False
      by (rule ih[OF _ si_gt_si])
  qed
qed

lemma gt_antisym: "t >t s ⟹ ¬ s >t t"
  using gt_irrefl gt_trans by blast


subsection ‹Subterm Property›

lemma
  gt_sub_fun: "App s t >t s" and
  gt_sub_arg: "App s t >t t"
  by (auto intro: gt_sub)

theorem gt_proper_sub: "proper_sub s t ⟹ t >t s"
  by (induct t) (auto intro: gt_sub_fun gt_sub_arg gt_trans)


subsection ‹Compatibility with Functions›

lemma gt_compat_fun:
  assumes t'_gt_t: "t' >t t"
  shows "App s t' >t App s t"
proof -
  have t'_ne_t: "t' ≠ t"
    using gt_antisym t'_gt_t by blast
  have extf_args_single: "∀f ∈ ground_heads (head s). extf f (>t) (args s @ [t']) (args s @ [t])"
    by (simp add: extf_compat_list t'_gt_t t'_ne_t)
  show ?thesis
    by (rule gt_same) (auto simp: gt_sub gt_sub_fun t'_gt_t intro!: extf_args_single)
qed

theorem gt_compat_fun_strong:
  assumes t'_gt_t: "t' >t t"
  shows "apps s (t' # us) >t apps s (t # us)"
proof (induct us rule: rev_induct)
  case Nil
  show ?case
    using t'_gt_t by (auto intro!: gt_compat_fun)
next
  case (snoc u us)
  note ih = snoc

  let ?v' = "apps s (t' # us @ [u])"
  let ?v = "apps s (t # us @ [u])"

  show ?case
  proof (rule gt_same)
    show "chksubs (>t) ?v' ?v"
      using ih by (auto intro: gt_sub gt_sub_arg)
  next
    show "∀f ∈ ground_heads (head ?v'). extf f (>t) (args ?v') (args ?v)"
      by (metis args_apps extf_compat_list gt_irrefl t'_gt_t)
  qed simp
qed


subsection ‹Compatibility with Arguments›

theorem gt_diff_same_compat_arg:
  assumes
    extf_compat_snoc: "⋀f. ext_compat_snoc (extf f)" and
    diff_same: "gt_diff s' s ∨ gt_same s' s"
  shows "App s' t >t App s t"
proof -
  {
    assume "s' >t s"
    hence "App s' t >t s"
      using gt_sub_fun gt_trans by blast
    moreover have "App s' t >t t"
      by (simp add: gt_sub_arg)
    ultimately have "chksubs (>t) (App s' t) (App s t)"
      by auto
  }
  note chk_s't_st = this

  show ?thesis
    using diff_same
  proof
    assume "gt_diff s' s"
    hence
      s'_gt_s: "s' >t s" and
      hd_s'_gt_s: "head s' >hd head s" and
      chkvar_s'_s: "chkvar s' s" and
      chk_s'_s: "chksubs (>t) s' s"
      using gt_diff.cases by (auto simp: gt_iff_sub_diff_same)

    have chkvar_s't_st: "chkvar (App s' t) (App s t)"
      using chkvar_s'_s by auto
    show ?thesis
      by (rule gt_diff[OF _ chkvar_s't_st chk_s't_st[OF s'_gt_s]])
        (simp add: hd_s'_gt_s[simplified])
  next
    assume "gt_same s' s"
    hence
      s'_gt_s: "s' >t s" and
      hd_s'_eq_s: "head s' = head s" and
      chk_s'_s: "chksubs (>t) s' s" and
      gts_args: "∀f ∈ ground_heads (head s'). extf f (>t) (args s') (args s)"
      using gt_same.cases by (auto simp: gt_iff_sub_diff_same, metis)

    have gts_args_t:
      "∀f ∈ ground_heads (head (App s' t)). extf f (>t) (args (App s' t)) (args (App s t))"
      using gts_args ext_compat_snoc.compat_append_right[OF extf_compat_snoc] by simp

    show ?thesis
      by (rule gt_same[OF _ chk_s't_st[OF s'_gt_s] gts_args_t]) (simp add: hd_s'_eq_s)
  qed
qed


subsection ‹Stability under Substitution›

lemma gt_imp_chksubs_gt:
  assumes t_gt_s: "t >t s"
  shows "chksubs (>t) t s"
proof -
  have "is_App s ⟹ t >t fun s ∧ t >t arg s"
    using t_gt_s by (meson gt_sub gt_trans)
  thus ?thesis
    by (simp add: tm.case_eq_if)
qed

theorem gt_subst:
  assumes wary_ρ: "wary_subst ρ"
  shows "t >t s ⟹ subst ρ t >t subst ρ s"
proof (simp only: atomize_imp,
    rule measure_induct_rule[of "λ(t, s). {#size t, size s#}"
        "λ(t, s). t >t s ⟶ subst ρ t >t subst ρ s" "(t, s)",
      simplified prod.case],
    simp only: split_paired_all prod.case atomize_imp[symmetric])
  fix t s
  assume
    ih: "⋀ta sa. {#size ta, size sa#} < {#size t, size s#} ⟹ ta >t sa ⟹
      subst ρ ta >t subst ρ sa" and
    t_gt_s: "t >t s"

  {
    assume chk_t_s: "chksubs (>t) t s"
    have "chksubs (>t) (subst ρ t) (subst ρ s)"
    proof (cases s)
      case s: (Hd ζ)
      show ?thesis
      proof (cases ζ)
        case ζ: (Var x)
        have psub_x_t: "proper_sub (Hd (Var x)) t"
          using ζ s t_gt_s gt_imp_vars gt_irrefl in_vars_imp_sub by fastforce
        show ?thesis
          unfolding ζ s
          by (rule gt_imp_chksubs_gt[OF gt_proper_sub[OF proper_sub_subst]]) (rule psub_x_t)
      qed (auto simp: s)
    next
      case s: (App s1 s2)
      have "t >t s1" and "t >t s2"
        using s chk_t_s by auto
      thus ?thesis
        using s by (auto intro!: ih[of t s1] ih[of t s2])
    qed
  }
  note chk_ρt_ρs_if = this

  show "subst ρ t >t subst ρ s"
    using t_gt_s
  proof cases
    case gt_sub_t_s: gt_sub
    obtain t1 t2 where t: "t = App t1 t2"
      using gt_sub_t_s(1) by (metis tm.collapse(2))
    show ?thesis
      using gt_sub ih[of t1 s] ih[of t2 s] gt_sub_t_s(2) t by auto
  next
    case gt_diff_t_s: gt_diff
    have "head (subst ρ t) >hd head (subst ρ s)"
      by (meson wary_subst_ground_heads gt_diff_t_s(1) gt_hd_def subsetCE wary_ρ)
    moreover have "chkvar (subst ρ t) (subst ρ s)"
      unfolding chkvar_def using vars_subst_subseteq[OF gt_imp_vars[OF t_gt_s]] vars_head_subseteq
      by force
    ultimately show ?thesis
      by (rule gt_diff[OF _ _ chk_ρt_ρs_if[OF gt_diff_t_s(3)]])
  next
    case gt_same_t_s: gt_same

    have hd_ρt_eq_ρs: "head (subst ρ t) = head (subst ρ s)"
      using gt_same_t_s(1) by simp

    {
      fix f
      assume f_in_grounds: "f ∈ ground_heads (head (subst ρ t))"

      let ?S = "set (args t) ∪ set (args s)"

      have extf_args_s_t: "extf f (>t) (args t) (args s)"
        using gt_same_t_s(3) f_in_grounds wary_ρ wary_subst_ground_heads by blast
      have "extf f (>t) (map (subst ρ) (args t)) (map (subst ρ) (args s))"
      proof (rule extf_map[of ?S, OF _ _ _ _ _ _ extf_args_s_t])
        have sz_a: "∀ta ∈ ?S. ∀sa ∈ ?S. {#size ta, size sa#} < {#size t, size s#}"
          by (fastforce intro: Max_lt_imp_lt_mset dest: size_in_args)
        show "∀ta ∈ ?S. ∀sa ∈ ?S. ta >t sa ⟶ subst ρ ta >t subst ρ sa"
          using ih sz_a size_in_args by fastforce
      qed (auto intro!: gt_irrefl elim!: gt_trans)
      hence "extf f (>t) (args (subst ρ t)) (args (subst ρ s))"
        by (auto simp: gt_same_t_s(1) intro: extf_compat_append_left)
    }
    hence "∀f ∈ ground_heads (head (subst ρ t)).
      extf f (>t) (args (subst ρ t)) (args (subst ρ s))"
      by blast
    thus ?thesis
      by (rule gt_same[OF hd_ρt_eq_ρs chk_ρt_ρs_if[OF gt_same_t_s(2)]])
  qed
qed


subsection ‹Totality on Ground Terms›

theorem gt_total_ground:
  assumes extf_total: "⋀f. ext_total (extf f)"
  shows "ground t ⟹ ground s ⟹ t >t s ∨ s >t t ∨ t = s"
proof (simp only: atomize_imp,
    rule measure_induct_rule[of "λ(t, s). {# size t, size s #}"
      "λ(t, s). ground t ⟶ ground s ⟶ t >t s ∨ s >t t ∨ t = s" "(t, s)", simplified prod.case],
    simp only: split_paired_all prod.case atomize_imp[symmetric])
  fix t s :: "('s, 'v) tm"
  assume
    ih: "⋀ta sa. {# size ta, size sa #} < {# size t, size s #} ⟹ ground ta ⟹ ground sa ⟹
      ta >t sa ∨ sa >t ta ∨ ta = sa" and
    gr_t: "ground t" and gr_s: "ground s"

  let ?case = "t >t s ∨ s >t t ∨ t = s"

  have "chksubs (>t) t s ∨ s >t t"
    unfolding chksubs_def tm.case_eq_if using ih[of t "fun s"] ih[of t "arg s"] mset_lt_single_iff
    by (metis add_mset_lt_right_lt gr_s gr_t ground_arg ground_fun gt_sub size_arg_lt size_fun_lt)
  moreover have "chksubs (>t) s t ∨ t >t s"
    unfolding chksubs_def tm.case_eq_if using ih[of "fun t" s] ih[of "arg t" s]
    by (metis add_mset_lt_left_lt gr_s gr_t ground_arg ground_fun gt_sub size_arg_lt size_fun_lt)  
  moreover
  {
    assume
      chksubs_t_s: "chksubs (>t) t s" and
      chksubs_s_t: "chksubs (>t) s t"

    obtain g where g: "head t = Sym g"
      using gr_t by (metis ground_head hd.collapse(2))
    obtain f where f: "head s = Sym f"
      using gr_s by (metis ground_head hd.collapse(2))

    have chkvar_t_s: "chkvar t s" and chkvar_s_t: "chkvar s t"
      using g f by simp_all

    {
      assume g_gt_f: "g >s f"
      have "t >t s"
        by (rule gt_diff[OF _ chkvar_t_s chksubs_t_s]) (simp add: g f gt_sym_imp_hd[OF g_gt_f])
    }
    moreover
    {
      assume f_gt_g: "f >s g"
      have "s >t t"
        by (rule gt_diff[OF _ chkvar_s_t chksubs_s_t]) (simp add: g f gt_sym_imp_hd[OF f_gt_g])
    }
    moreover
    {
      assume g_eq_f: "g = f"
      hence hd_t: "head t = head s"
        using g f by auto

      let ?ts = "args t"
      let ?ss = "args s"

      have gr_ts: "∀ta ∈ set ?ts. ground ta"
        using ground_args[OF _ gr_t] by blast
      have gr_ss: "∀sa ∈ set ?ss. ground sa"
        using ground_args[OF _ gr_s] by blast

      {
        assume ts_eq_ss: "?ts = ?ss"
        have "t = s"
          using hd_t ts_eq_ss by (rule tm_expand_apps)
      }
      moreover
      {
        assume ts_gt_ss: "extf g (>t) ?ts ?ss"
        have "t >t s"
          by (rule gt_same[OF hd_t chksubs_t_s]) (auto simp: g ts_gt_ss)
      }
      moreover
      {
        assume ss_gt_ts: "extf g (>t) ?ss ?ts"
        have "s >t t"
          by (rule gt_same[OF hd_t[symmetric] chksubs_s_t]) (auto simp: f[folded g_eq_f] ss_gt_ts)
      }
      ultimately have ?case
        using ih gr_ss gr_ts
          ext_total.total[OF extf_total, rule_format, of "set ?ts ∪ set ?ss" "(>t)" ?ts ?ss g]
        by (metis Un_iff in_listsI less_multiset_doubletons size_in_args)
    }
    ultimately have ?case
      using gt_sym_total by blast
  }
  ultimately show ?case
    by fast
qed


subsection ‹Well-foundedness›

abbreviation gtg :: "('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool" (infix ‹>tg› 50) where
  "(>tg) ≡ λt s. ground t ∧ t >t s"

theorem gt_wf:
  assumes extf_wf: "⋀f. ext_wf (extf f)"
  shows "wfP (λs t. t >t s)"
proof -
  have ground_wfP: "wfP (λs t. t >tg s)"
    unfolding wfP_iff_no_inf_chain
  proof
    assume "∃f. inf_chain (>tg) f"
    then obtain t where t_bad: "bad (>tg) t"
      unfolding inf_chain_def bad_def by blast

    let ?ff = "worst_chain (>tg) (λt s. size t > size s)"
    let ?U_of = "λi. if is_App (?ff i) then {fun (?ff i)} ∪ set (args (?ff i)) else {}"

    note wf_sz = wf_app[OF wellorder_class.wf, of size, simplified]

    define U where "U = (⋃i. ?U_of i)"

    have gr: "⋀i. ground (?ff i)"
      using worst_chain_bad[OF wf_sz t_bad, unfolded inf_chain_def] by fast
    have gr_fun: "⋀i. ground (fun (?ff i))"
      by (rule ground_fun[OF gr])
    have gr_args: "⋀i s. s ∈ set (args (?ff i)) ⟹ ground s"
      by (rule ground_args[OF _ gr])
    have gr_u: "⋀u. u ∈ U ⟹ ground u"
      unfolding U_def by (auto dest: gr_args) (metis (lifting) empty_iff gr_fun)

    have "¬ bad (>tg) u" if u_in: "u ∈ ?U_of i" for u i
    proof
      let ?ti = "?ff i"

      assume u_bad: "bad (>tg) u"
      have sz_u: "size u < size ?ti"
      proof (cases "?ff i")
        case Hd
        thus ?thesis
          using u_in size_in_args by fastforce
      next
        case App
        thus ?thesis
          using u_in size_in_args insert_iff size_fun_lt by fastforce
      qed

      show False
      proof (cases i)
        case 0
        thus False
          using sz_u min_worst_chain_0[OF wf_sz u_bad] by simp
      next
        case Suc
        hence "?ff (i - 1) >t ?ff i"
          using worst_chain_pred[OF wf_sz t_bad] by simp
        moreover have "?ff i >t u"
        proof -
          have u_in: "u ∈ ?U_of i"
            using u_in by blast
          have ffi_ne_u: "?ff i ≠ u"
            using sz_u by fastforce
          hence "is_App (?ff i) ⟹ ¬ sub u (?ff i) ⟹ ?ff i >t u"
            using u_in gt_sub sub_args by auto
          thus "?ff i >t u"
            using ffi_ne_u u_in gt_proper_sub sub_args by fastforce
        qed
        ultimately have "?ff (i - 1) >t u"
          by (rule gt_trans)
        thus False
          using Suc sz_u min_worst_chain_Suc[OF wf_sz u_bad] gr by fastforce
      qed
    qed
    hence u_good: "⋀u. u ∈ U ⟹ ¬ bad (>tg) u"
      unfolding U_def by blast

    have bad_diff_same: "inf_chain (λt s. ground t ∧ (gt_diff t s ∨ gt_same t s)) ?ff"
      unfolding inf_chain_def
    proof (intro allI conjI)
      fix i

      show "ground (?ff i)"
        by (rule gr)

      have gt: "?ff i >t ?ff (Suc i)"
        using worst_chain_pred[OF wf_sz t_bad] by blast

      have "¬ gt_sub (?ff i) (?ff (Suc i))"
      proof
        assume a: "gt_sub (?ff i) (?ff (Suc i))"
        hence fi_app: "is_App (?ff i)" and
          fun_or_arg_fi_ge: "fun (?ff i) ≥t ?ff (Suc i) ∨ arg (?ff i) ≥t ?ff (Suc i)"
          unfolding gt_sub.simps by blast+
        have "fun (?ff i) ∈ ?U_of i"
          unfolding U_def using fi_app by auto
        moreover have "arg (?ff i) ∈ ?U_of i"
          unfolding U_def using fi_app arg_in_args by force
        ultimately obtain uij where uij_in: "uij ∈ U" and uij_cases: "uij ≥t ?ff (Suc i)"
          unfolding U_def using fun_or_arg_fi_ge by blast

        have "⋀n. ?ff n >t ?ff (Suc n)"
          by (rule worst_chain_pred[OF wf_sz t_bad, THEN conjunct2])
        hence uij_gt_i_plus_3: "uij >t ?ff (Suc (Suc i))"
          using gt_trans uij_cases by blast

        have "inf_chain (>tg) (λj. if j = 0 then uij else ?ff (Suc (i + j)))"
          unfolding inf_chain_def
          by (auto intro!: gr gr_u[OF uij_in] uij_gt_i_plus_3 worst_chain_pred[OF wf_sz t_bad])
        hence "bad (>tg) uij"
          unfolding bad_def by fastforce
        thus False
          using u_good[OF uij_in] by sat
      qed
      thus "gt_diff (?ff i) (?ff (Suc i)) ∨ gt_same (?ff i) (?ff (Suc i))"
        using gt unfolding gt_iff_sub_diff_same by sat
    qed

    have "wf {(s, t). ground s ∧ ground t ∧ sym (head t) >s sym (head s)}"
      using gt_sym_wf unfolding wfp_def wf_iff_no_infinite_down_chain by fast
    moreover have "{(s, t). ground t ∧ gt_diff t s}
      ⊆ {(s, t). ground s ∧ ground t ∧ sym (head t) >s sym (head s)}"
    proof (clarsimp, intro conjI)
      fix s t
      assume gr_t: "ground t" and gt_diff_t_s: "gt_diff t s"
      thus gr_s: "ground s"
        using gt_iff_sub_diff_same gt_imp_vars by fastforce

      show "sym (head t) >s sym (head s)"
        using gt_diff_t_s ground_head[OF gr_s] ground_head[OF gr_t]
        by (cases; cases "head s"; cases "head t") (auto simp: gt_hd_def)
    qed
    ultimately have wf_diff: "wf {(s, t). ground t ∧ gt_diff t s}"
      by (rule wf_subset)

    have diff_O_same: "{(s, t). ground t ∧ gt_diff t s} O {(s, t). ground t ∧ gt_same t s}
      ⊆ {(s, t). ground t ∧ gt_diff t s}"
      unfolding gt_diff.simps gt_same.simps
      by clarsimp (metis chksubs_def empty_subsetI gt_diff[unfolded chkvar_def] gt_imp_chksubs_gt
        gt_same gt_trans)

    have diff_same_as_union: "{(s, t). ground t ∧ (gt_diff t s ∨ gt_same t s)} =
      {(s, t). ground t ∧ gt_diff t s} ∪ {(s, t). ground t ∧ gt_same t s}"
      by auto

    obtain k where bad_same: "inf_chain (λt s. ground t ∧ gt_same t s) (λi. ?ff (i + k))"
      using wf_infinite_down_chain_compatible[OF wf_diff _ diff_O_same, of ?ff] bad_diff_same
      unfolding inf_chain_def diff_same_as_union[symmetric] by auto
    hence hd_sym: "⋀i. is_Sym (head (?ff (i + k)))"
      unfolding inf_chain_def by (simp add: ground_head)

    define f where "f = sym (head (?ff k))"

    have hd_eq_f: "head (?ff (i + k)) = Sym f" for i
    proof (induct i)
      case 0
      thus ?case
        by (auto simp: f_def hd.collapse(2)[OF hd_sym, of 0, simplified])
    next
      case (Suc ia)
      thus ?case
        using bad_same unfolding inf_chain_def gt_same.simps by simp
    qed

    let ?gtu = "λt s. t ∈ U ∧ t >t s"

    have "t ∈ set (args (?ff i)) ⟹ t ∈ ?U_of i" for t i
      unfolding U_def
      by (cases "is_App (?ff i)", simp_all,
        metis (lifting) neq_iff size_in_args sub.cases sub_args tm.discI(2))
    moreover have "⋀i. extf f (>t) (args (?ff (i + k))) (args (?ff (Suc i + k)))"
      using bad_same hd_eq_f unfolding inf_chain_def gt_same.simps by auto
    ultimately have "⋀i. extf f ?gtu (args (?ff (i + k))) (args (?ff (Suc i + k)))"
      using extf_mono_strong[of _ _ "(>t)" "λt s. t ∈ U ∧ t >t s"] unfolding U_def by blast
    hence "inf_chain (extf f ?gtu) (λi. args (?ff (i + k)))"
      unfolding inf_chain_def by blast
    hence nwf_ext: "¬ wfP (λxs ys. extf f ?gtu ys xs)"
      unfolding wfP_iff_no_inf_chain by fast

    have gtu_le_gtg: "?gtu ≤ (>tg)"
      by (auto intro!: gr_u)

    have "wfP (λs t. ?gtu t s)"
      unfolding wfP_iff_no_inf_chain
    proof (intro notI, elim exE)
      fix f
      assume bad_f: "inf_chain ?gtu f"
      hence bad_f0: "bad ?gtu (f 0)"
        by (rule inf_chain_bad)

      have "f 0 ∈ U"
        using bad_f unfolding inf_chain_def by blast
      hence good_f0: "¬ bad ?gtu (f 0)"
        using u_good bad_f inf_chain_bad inf_chain_subset[OF _ gtu_le_gtg] by blast

      show False
        using bad_f0 good_f0 by sat
    qed
    hence wf_ext: "wfP (λxs ys. extf f ?gtu ys xs)"
      by (rule ext_wf.wf[OF extf_wf, rule_format])

    show False
      using nwf_ext wf_ext by blast
  qed

  let ?subst = "subst grounding_ρ"

  have "wfP (λs t. ?subst t >tg ?subst s)"
    by (rule wfP_app[OF ground_wfP])
  hence "wfP (λs t. ?subst t >t ?subst s)"
    by (simp add: ground_grounding_ρ)
  thus ?thesis
    by (auto intro: wfp_subset gt_subst[OF wary_grounding_ρ])
qed

end

end