Theory Lambda_Free_EPO

(*  Title:       The Embedding Path Order for Lambda-Free Higher-Order Terms
    Author:      Alexander Bentkamp <a.bentkamp at vu.nl>, 2018
    Maintainer:  Alexander Bentkamp <a.bentkamp at vu.nl>
*)

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

theory Lambda_Free_EPO
imports Chop Nested_Multisets_Ordinals.Multiset_More
abbrevs ">t" = ">t"
  and "≥t" = "≥t"
begin

text ‹
This theory defines the embedding path order for λ›-free
higher-order terms.
›

subsection ‹Setup›

locale epo = 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_list: "ext_compat_list (extf f)"
  assumes extf_ext_compat_snoc: "ext_compat_snoc (extf f)"
  assumes extf_ext_compat_cons: "ext_compat_cons (extf f)"
  assumes extf_min_empty: "extf f gt [a] []" (* TODO: seperate definition? *)
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_list = ext_compat_list.compat_list[OF extf_ext_compat_list]

lemmas extf_compat_cons = ext_compat_cons.compat_cons[OF extf_ext_compat_cons]
lemmas extf_compat_snoc = ext_compat_snoc.compat_snoc[OF extf_ext_compat_snoc]

lemmas extf_compat_append_right = ext_compat_snoc.compat_append_right[OF extf_ext_compat_snoc]
lemmas extf_compat_append_left = ext_compat_cons.compat_append_left[OF extf_ext_compat_cons]

lemma extf_snoc: "extf f gt (xs @ [z]) xs"
proof (induction xs)
  case Nil
  then show ?case 
    using extf_min_empty by force
next
  case (Cons a xs)
  then show ?case
    by (simp add: extf_compat_cons)
qed

subsection ‹Inductive Definitions›

definition
  chkchop :: "(('s, 'v) tm  ('s, 'v) tm  bool)  ('s, 'v) tm  ('s, 'v) tm  bool"
where
  [simp]: "chkchop gt t s  is_Hd s  gt t (chop s)"

definition
  chkchop_same :: "(('s, 'v) tm  ('s, 'v) tm  bool)  ('s, 'v) tm  ('s, 'v) tm  bool"
where
  [simp]: "chkchop_same gt t s  
            (if is_Var (head t) 
            then is_App t  chkchop gt (chop t) s 
            else chkchop gt t s)"

lemma chkchop_mono[mono]: "gt  gt'  chkchop gt  chkchop gt'"
  using chkchop_def by blast

lemma chkchop_same_mono[mono]: "gt  gt'  chkchop_same gt  chkchop_same gt'"
  using chkchop_same_def by fastforce

inductive gt :: "('s, 'v) tm  ('s, 'v) tm  bool" (infix ">t" 50) where
  gt_chop: "is_App t  chop t >t s  chop t = s  t >t s"
| gt_diff: "head t >hd head s  is_Sym (head s)  chkchop (>t) t s  t >t s"
| gt_same: "head t = head s  chkchop_same (>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_chop :: "('s, 'v) tm  ('s, 'v) tm  bool" where
  gt_chopI: "is_App t  chop t t s  gt_chop t s"

inductive gt_diff :: "('s, 'v) tm  ('s, 'v) tm  bool" where
  gt_diffI: "head t >hd head s  is_Sym (head s)  chkchop (>t) t s  gt_diff t s"

inductive gt_same :: "('s, 'v) tm  ('s, 'v) tm  bool" where
  gt_sameI: "head t = head s  chkchop_same (>t) t s 
    (f  ground_heads (head t). extf f (>t) (args t) (args s))  gt_same t s"

lemma gt_iff_chop_diff_same: "t >t s  gt_chop t s  gt_diff t s  gt_same t s"
  by (subst gt.simps) (auto simp: gt_chop.simps gt_diff.simps gt_same.simps)

subsection ‹Transitivity›

lemma t_gt_chop_t: "is_App t  t >t chop t"
  by (simp add: gt_chop)

lemma gt_trans: "u >t t  t >t s  u >t s"
proof (simp only: atomize_imp,
    rule measure_induct_rule[of "λ(u, t, s). {#hsize u, hsize t, hsize 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. {#hsize ua, hsize ta, hsize sa#} < {#hsize u, hsize t, hsize s#} 
      ua >t ta  ta >t sa  ua >t sa" and
    u_gt_t: "u >t t" and t_gt_s: "t >t s"

  show "u >t s"
    using u_gt_t
  proof cases
    case gt_chop
    then have "chop u >t s" using ih[of "chop u" t s]
      using add_mset_lt_left_lt hsize_chop_lt t_gt_s by blast
    show ?thesis
      using local.gt_chop(1) local.gt_chop(2) chop u >t s gt.gt_chop by presburger
  next
    case gt_diff_u_t: gt_diff
    show ?thesis
      using t_gt_s
    proof cases
      case gt_chop
      then have "u >t chop t" 
        using chkchop_def gt_diff_u_t(3) by presburger 
      then show ?thesis using ih[of u "chop t" s]
        using hsize_chop_lt local.gt_chop(1) local.gt_chop(2) by fastforce
    next
      case gt_diff_t_s: 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 using ih[of u t "chop s"]
        by (metis add_mset_lt_left_lt add_mset_lt_right_lt chkchop_def gt_diff gt_diff_t_s(2) 
          gt_diff_t_s(3) hsize_chop_lt u_gt_t)
    next
      case gt_same_t_s: gt_same
      have "head u >hd head s"
        using gt_diff_u_t(1) gt_same_t_s(1) by auto
      thus ?thesis using ih[of u t "chop s"]
        by (metis add_mset_lt_left_lt add_mset_lt_right_lt chkchop_def chkchop_same_def gt_diff 
          gt_diff_u_t(2) gt_same_t_s(1) gt_same_t_s(2) hsize_chop_lt u_gt_t)
    qed
  next
    case gt_same_u_t: gt_same
    show ?thesis
      using t_gt_s
    proof cases
      case gt_chop
      then show ?thesis 
      proof (cases "is_Var (head u)")
        case True
        then show ?thesis  using ih[of "chop u" "chop t" s]
          by (metis add_mset_lt_left_lt add_mset_lt_lt_lt chkchop_def chkchop_same_def gt.gt_chop 
            gt_same_u_t(2) hsize_chop_lt local.gt_chop(1) local.gt_chop(2))
      next
        case False
        then show ?thesis using ih[of u "chop t" s] 
          by (metis add_mset_lt_left_lt add_mset_lt_right_lt chkchop_def chkchop_same_def 
            gt_same_u_t(2) hsize_chop_lt local.gt_chop(1) local.gt_chop(2))
      qed
    next
      case gt_diff_t_s: gt_diff
      have "head u >hd head s"
        by (simp add: gt_diff_t_s(1) gt_same_u_t(1))
      thus ?thesis using ih[of u t "chop s"]
        by (metis add_mset_lt_left_lt add_mset_lt_right_lt chkchop_def gt_diff gt_diff_t_s(1)
         gt_diff_t_s(2) gt_diff_t_s(3) gt_same_u_t(1) hsize_chop_lt  u_gt_t)
    next
      case gt_same_t_s: 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
               hsize_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
      have "chkchop_same (>t) u s"
      proof (cases "head u")
        case (Var x)
        then show ?thesis
        proof (cases u)
          case (Hd _)
          then show ?thesis 
            using Var
            using gt_same_u_t(2) by force
        next
          case (App u1 u2)
          then have "chop u >t chop t" 
            by (metis Var chkchop_def chkchop_same_def gt_same_t_s(2) gt_same_u_t(1) 
              gt_same_u_t(2) hd.disc(1))
          then show ?thesis
          proof (cases t)
            case (Hd _)
            then show ?thesis
              using Var gt_same_t_s(2) gt_same_u_t(1) by force
          next
            case t_App: (App t1 t2)
            then have "is_App s  chop t >t chop s" 
              using gt_same_t_s unfolding chkchop_same_def unfolding chkchop_def using Var hd_u_s by auto
            then have "chkchop (>t) (chop u) s" 
              unfolding chkchop_def using ih[of "chop u" "chop t" "chop s"]
              by (metis App chop u >t chop t t_App add_mset_lt_lt_le less_imp_le mset_lt_single_iff hsize_chop_lt tm.disc(2))
            then show ?thesis unfolding chkchop_same_def 
              using Var by (simp add: App)
          qed
        qed
      next
        case (Sym f)
        have "chkchop (>t) u s" 
         proof (cases s)
           case (Hd _)
           then show ?thesis 
             by simp
         next
           case (App s1 s2)
           then have "t >t chop s"
             using Sym gt_same_t_s(1) gt_same_t_s(2) hd_u_s by auto
           then have "u >t chop s" using ih[of u t "chop s"] 
             by (metis App add_mset_lt_right_lt mset_lt_single_iff hsize_chop_lt tm.disc(2) u_gt_t)
           then show ?thesis unfolding chkchop_def
             by blast
         qed
        then show ?thesis
          by (simp add: Sym) 
      qed
      thus ?thesis 
        using flocal.ground_heads (head u). extf f (>t) (args u) (args s) gt_same hd_u_s by blast
    qed
  qed
qed

subsection ‹Irreflexivity›

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

  show False
    using s_gt_s
  proof cases
    case gt_chop
    then show False using ih[of "chop s"]
      by (metis gt.gt_chop gt_trans hsize_chop_lt)
  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 "hsize si < hsize s"
      by (rule hsize_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_emb_fun: "App s t >t s"
proof (induction s rule:measure_induct_rule[of "hsize"])
  case (less s)
  have extf: "f  ground_heads (head s). extf f (>t) (args (App s t)) (args s)"
    using extf_snoc by force
  have "head (App s t) = head s"
    by simp
  have "chkchop_same (>t) (App s t) s"
  proof (cases "is_Hd s")
    case True
    then show ?thesis
      by simp
  next
    case False
    have chop_gt_chop: "(chop (App s t)) >t chop s" using less[of "chop s"]
      using False hsize_chop_lt by (metis App_apps apps.simps(1) chop_apps)
    then show ?thesis 
    proof (cases "is_Var (head s)")
      case True
      then show ?thesis
        by (simp add: True chop_gt_chop)
    next
      case False
      then show ?thesis using less[of "chop s"]
        by (simp add: chop_gt_chop gt_chop)
    qed
  qed
  then show ?case
    using extf gt_same by auto
qed

lemma gt_emb_arg: "App s t >t t"
proof (induction s rule:measure_induct_rule[of "hsize"])
  case (less s)
  then show ?case
  proof (cases "is_Hd s")
    case True
    then show ?thesis 
      by (metis chop_App_Hd t_gt_chop_t tm.disc(2))
  next
    case False
    have "chop (App s t) >t t" using less[of "chop s"] 
      by (metis App_apps False apps.simps(1) chop_apps hsize_chop_lt)
    then show ?thesis 
      using gt_chop tm.disc(2) by blast
  qed
qed

subsection ‹Compatibility with Contexts›

lemma gt_compat_fun:
  assumes "t' >t t"
  shows "App s t' >t App s t"
using assms  apply (simp only:atomize_imp)
proof (induction rule:measure_induct_rule[of "λ(t, s). hsize t + hsize s" "λ(t, s). t' >t t  App s t' >t App s t" "(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. hsize ta + hsize sa < hsize t + hsize s  t' >t ta  App sa t' >t App sa ta"
  and t'_gt_t:"t' >t t" 

  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  "App s t' >t App s t"
  proof (rule gt_same)
    show "head (App s t') = head (App s t)" by simp
    show "flocal.ground_heads (head (App s t')). extf f (>t) (args (App s t')) (args (App s t))"
      by (simp add: extf_args_single)
    have 0: "chop (App s t') >t chop (App s t)" 
    proof (cases s)
      case (Hd _)
      then show ?thesis using chop_App_Hd
        by (simp add: chop_App_Hd t'_gt_t)
    next
      case (App s1 s2)
      then show ?thesis using ih[of t "chop s"] chop_fun 
        by (metis nat_add_left_cancel_less hsize_chop_lt t'_gt_t tm.disc(2) tm.sel(4) tm.sel(6))
    qed
    show "chkchop_same (>t) (App s t') (App s t)"
    proof (cases "is_Var (head (App s t'))")
      case True
      then show ?thesis unfolding chkchop_same_def chkchop_def
        using True 0 by auto
    next
      case False
      have "App s t' >t chop (App s t)" using 0 by (simp add: gt_chop)
      then show ?thesis  unfolding chkchop_same_def chkchop_def 
        using False by auto
    qed
  qed
qed

theorem gt_compat_arg:
  shows "s' >t s  t' t t  App s' t' >t App s t"
proof (simp only:atomize_imp,induction rule:measure_induct[of "λ(s',s,t). hsize s' + hsize s + hsize t" "λ(s',s,t). s' >t s  t' t t  App s' t' >t App s t" "(s',s,t)", simplified prod.case],
    simp only: split_paired_all prod.case atomize_imp[symmetric] atomize_all[symmetric])
  fix s' s t
  assume ih:"ab ac ba. hsize ab + hsize ac + hsize ba < hsize s' + hsize s + hsize t  ab >t ac  t' t ba  App ab t' >t App ac ba" 
    and "s' >t s" and "t' t t" 

  {
    fix s''::"('s,'v) tm" assume hsize_s'':"hsize s''  hsize s'"
    assume chkchop_s'_s: "chkchop (>t) s'' s"
    then have "chkchop (>t) (App s'' t') (App s t)" 
    proof (cases "is_Hd s")
      case True
      then show ?thesis using chkchop_s'_s unfolding chkchop_def
        by (metis t' t t chop_App_Hd gt_emb_arg gt_trans)
    next
      case False
      then show ?thesis using chkchop_s'_s unfolding chkchop_def
        using ih[of s'' "chop s" t] hsize_s''
        by (metis t' t t add_less_mono add_mono_thms_linordered_field(1) chop_fun le_eq_less_or_eq nat_add_left_cancel_less hsize_chop_lt tm.sel(4) tm.sel(6))
    qed
  }
  note chkchop_compat_arg = this

  show "App s' t' >t App s t " using s' >t s
  proof (cases rule:gt.cases)
    case gt_chop
    then show ?thesis 
    proof (cases "t = t'")
      case True
      show ?thesis using True gt.gt_chop[of "App s' t'" "App s t"] gt_chop chkchop_compat_arg[of "chop s'"]
        by (metis add_strict_right_mono chop_fun ih hsize_chop_lt tm.disc(2) tm.sel(4) tm.sel(6))
    next
      case False
      then have "t' >t t"
        using t' t t by blast
      have "App s' t' >t App (chop s') t'"
        by (metis chop_fun local.gt_chop(1) t_gt_chop_t tm.disc(2) tm.sel(4) tm.sel(6))
      moreover have "... >t App s t"  using ih[of "chop s'" s t]
        using t' >t t gt_compat_fun local.gt_chop(1) local.gt_chop(2) hsize_chop_lt by fastforce
      ultimately show ?thesis using gt_trans by blast
    qed
  next
    case gt_diff
    then show ?thesis 
      using chkchop_compat_arg gt.gt_diff by auto
  next
    case gt_same
    have hd_s'_eq_s: "head s' = head s" 
      by (simp add: local.gt_same(1))
    {
      fix f assume f_gh: "f  ground_heads (head s)"
      have f_s_args: 
        "extf f (>t) (args s') (args s)"
        using local.gt_same(3) f_gh by (simp add: hd_s'_eq_s)
      have f_compat_snoc: 
        "xs ys x. extf f (>t) ys xs  extf f (>t) (ys @ [x]) (xs @ [x])" 
        by (simp add: extf_compat_append_right)
     
      have f_st_args2:
        "extf f (>t) (args (App s' t)) (args (App s t))"
        by (simp add: f_compat_snoc f_s_args)
      have 0:"zUNIV. yUNIV. xUNIV. z >t y  y >t x  z >t x" 
        using gt_trans by blast
      then have f_trans:"xs ys zs. extf f (>t) zs ys  extf f (>t) ys xs  extf f (>t) zs xs" 
        using  extf_trans[of _ UNIV, unfolded lists_UNIV, OF UNIV_I UNIV_I UNIV_I 0] by metis
      have "extf f (>t) (args (App s' t')) (args (App s t))"
      proof (cases "t' = t")
        case True
        then show ?thesis using f_st_args2 by metis
      next
        case False
        have f_st_args1: 
          "extf f (>t) (args (App s' t')) (args (App s' t))"
          using extf_compat_list t' t t False by simp
        then show ?thesis using f_trans f_st_args1 f_st_args2 by metis
      qed
    }
    note extf_cond = this
    have "chkchop_same (>t) (App s' t') (App s t)" unfolding chkchop_same_def
      using chop_fun chkchop_compat_arg[of "chop s'", unfolded le_eq_less_or_eq] 
      chkchop_compat_arg[of s'] chkchop_def chkchop_same_def 
      hsize_chop_lt   epo.extf_min_empty[OF epo_axioms] gt.gt_same gt_antisym hd_s'_eq_s head_App 
      leI less_irrefl_nat local.gt_same(2) local.gt_same(3) tm.sel(4) tm.sel(6) tm.disc(2)
      by metis
    then show ?thesis 
      using extf_cond gt.gt_same hd_s'_eq_s by auto
  qed
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
  then show ?case 
  by (simp add: gt_compat_fun t'_gt_t)
next
  case (snoc x xs)
  then show ?case unfolding App_apps[symmetric] append_Cons[symmetric]
    using gt_compat_arg by blast
qed

theorem gt_or_eq_compat_App: "s' t s  t' t t  App s' t' t App s t"
  using gt_compat_fun gt_compat_arg by blast

theorem gt_compat_App:
  shows "s' t s  t' >t t  App s' t' >t App s t"
  using gt_compat_fun gt_compat_arg by blast


subsection "Compatibility with Embedding Relation"

lemma gt_embedding_step_property:
  assumes "t emb s"
  shows "t >t s"
using assms proof (induct)
  case (left t1 t2)
  then show ?case 
    using gt_emb_fun by blast
next
  case (right t1 t2)
  then show ?case 
    using gt_emb_arg by blast
next
  case (context_left t s u)
  then show ?case 
    using gt_compat_arg by blast
next
  case (context_right t s u)
  then show ?case
    using gt_compat_fun by auto
qed

lemma gt_embedding_property:
  assumes "t emb s" "t  s"
  shows "t >t s"
  using assms 
proof (induction)
  case (refl t)
  then show ?case by simp
next
  case (step t u s)
  then show ?case using gt_embedding_step_property gt_trans by blast
qed

subsection "Stability under Substitutions"

(* TODO: move *)
lemma extf_map2:
  assumes
    "yset ys  set xs. xset ys  set xs. y >t x  (h y) >t (h x)"
    "extf f (>t) ys xs"
  shows
    "extf f (>t) (map h ys) (map h xs)"
  apply (rule extf_map[of "set ys  set xs" ys xs "(>t)" h f])
        apply simp
       apply (simp add: in_listsI)
      apply (simp add: in_listsI)
  using gt_antisym apply blast
  using gt_trans apply blast
  by (simp add: assms)+

theorem gt_sus: 
  assumes ρ_wary: "wary_subst ρ"
  assumes ghd: "x. ground_heads (Var x) = UNIV" (* This condition is only needed for gt_same, not for gt_diff ! *)
  shows "t >t s  subst ρ t >t subst ρ s"
proof (simp only:atomize_imp,induction rule:measure_induct[of "λ(t,s). {# hsize t, hsize 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] atomize_all[symmetric])
  fix t s
  assume ih:"tt ss.
               {# hsize tt, hsize ss #} < {# hsize t, hsize s #} 
               tt >t ss  subst ρ tt >t subst ρ ss" 
    and "t >t s" 
  show "subst ρ t >t subst ρ s" using t >t s
  proof (cases)
    case t_gt_s_chop: gt_chop
    then show ?thesis 
      using emb_step_subst emb_step_chop[OF t_gt_s_chop(1)] gt_embedding_step_property 
       emb_step_hsize gt_trans ih[of "chop t" s] by (metis add_mset_lt_left_lt)
  next
    case t_gt_s_diff: gt_diff
    have gt_diff1: "head (subst ρ t) >hd head (subst ρ s)" 
      by (meson assms gt_hd_def subsetCE t_gt_s_diff(1) wary_subst_ground_heads)
    have gt_diff2: "is_Sym (head (subst ρ s))"
      by (metis ground_imp_subst_iden hd.collapse(2) hd.simps(18) head_subst t_gt_s_diff(2) tm.sel(1) tm.simps(17))
    have gt_diff3: "chkchop (>t) (subst ρ t) (subst ρ s)"    
    proof (cases s)
      case (Hd _)
      then show ?thesis 
        using t_gt_s_diff unfolding chkchop_def 
        by (metis ground_imp_subst_iden hd.collapse(2) hd.simps(18) tm.disc(1) tm.sel(1) tm.simps(17))
    next
      case s_App: (App s1 s2)
      then show ?thesis using t_gt_s_diff unfolding chkchop_def
        using ih[of t "chop s"] chop_subst_Sym hsize_chop_lt tm.disc(2)
        by (metis add_mset_lt_left_lt add_mset_lt_right_lt)
    qed
    show ?thesis
      using gt_diff gt_diff1 gt_diff2 gt_diff3 by blast
  next
    case t_gt_s_same: gt_same
    have gt_same1: "head (subst ρ t) = head (subst ρ s)" 
      by (simp add: t_gt_s_same(1))

    have extf_map_ts:"fground_heads (head t). extf f (>t) (map (subst ρ) (args t)) (map (subst ρ) (args s))"
    proof -
      have ih_args: "yset (args t)  set (args s). xset (args t)  set (args s). y >t x  subst ρ y >t subst ρ x"
        by (metis Un_iff less_multiset_doubletons hsize_in_args ih)
      have "fground_heads (head t). extf f (>t) (args t) (args s)"  
        using ghd t_gt_s_same(3) by metis
      then show ?thesis
        using extf_map[of "set (args t)  set (args s)" "args t" "args s" gt "subst ρ"]
        using gt_irrefl gt_trans ih_args by blast
    qed

    show ?thesis
    proof (cases "head t")
      case (Var x1)
      then have "is_Var (head t)" by simp
      {
        fix u :: "('s, 'v) tm"
        assume "ground_heads (head u)  ground_heads (head t)" "hsize u  hsize (subst ρ (Hd (head t)))"
        then have "apps u (map (subst ρ) (args t)) >t apps u (map (subst ρ) (args s))" 
        proof (induct "hsize u" arbitrary:u rule:less_induct)
          case less
          then show ?case 
          proof (cases u)
            case u_Hd: (Hd _)
            then have "args u = []" 
              by simp
            then show ?thesis 
            proof (cases s)
              case s_Hd: (Hd _)
              show ?thesis
                by (smt (verit, best) Nil_is_map_conv UNIV_I Var args u = [] is_Var (head t) 
                     append_self_conv2 args.simps(1) args_Nil_iff_is_Hd args_apps chkchop_def 
                     chkchop_same_def extf_map_ts ghd gt_same head_apps s_Hd t_gt_s_same(2))
            next
              case s_App: (App _ _)
              then have "is_App t"
                using is_Var (head t) chkchop_same_def t_gt_s_same(2) by presburger
  
              have "chop t >t chop s" 
                using is_App t is_Var (head t) s_App t_gt_s_same(2) by auto
              then have "subst ρ (chop t) >t subst ρ (chop s)" using ih
                by (metis is_App t less_multiset_doubletons s_App hsize_chop_lt tm.disc(2))
  
              define ut where "ut = apps u (map (subst ρ) (args t))"
              define us where "us = apps u (map (subst ρ) (args s))"
              have 0:"ss. args (apps u ss) = ss" 
                using  args u = [] by simp
              have chop_us: "chop us = subst ρ (chop s)" 
                unfolding chop_def subst_apps us_def 0 using hd_map
                by (metis (no_types, lifting) args_Nil_iff_is_Hd map_tl s_App tm.disc(2))
              have chop_ut: "chop ut = subst ρ (chop t)"
                unfolding chop_def subst_apps ut_def 0 using is_App t 
                by (simp add: args_Nil_iff_is_Hd hd_map map_tl)
  
              have "head ut = head us" 
                by (simp add: us_def ut_def)
              moreover have "chkchop_same (>t) ut us" unfolding chkchop_def chkchop_same_def
                by (metis "0" Nil_is_map_conv is_App t subst ρ (chop t) >t subst ρ (chop s) 
                  args_Nil_iff_is_Hd chop_us chop_ut gt_chop ut_def)
              moreover have "flocal.ground_heads (head ut). extf f (>t) (args ut) (args us)" 
                using extf_map_ts less us_def ut_def using "0" by auto
              ultimately show "ut >t us" 
                using gt_same by blast
            qed
          next
            case u_app: (App _ _)
            let ?ut = "apps u (map (subst ρ) (args t))"
            let ?us = "apps u (map (subst ρ) (args s))"
            have 1:"head ?ut = head ?ut" 
              by simp
            have "apps (chop u) (map (subst ρ) (args t)) >t apps (chop u) (map (subst ρ) (args s))"
              using less.hyps[of "chop u"] hsize_chop_lt 
              by (metis Var dual_order.trans ghd less.prems(2) less_or_eq_imp_le subset_UNIV tm.disc(2) u_app)
            then have "chop ?ut >t chop ?us" 
              by (simp add: chop_apps u_app)
            then have 2:"chkchop_same (>t) ?ut ?us" unfolding chkchop_same_def chkchop_def
              by (metis (no_types, lifting) Nil_is_map_conv is_Var (head t) append_is_Nil_conv 
                args_Nil_iff_is_Hd args_apps chkchop_same_def gt.simps t_gt_s_same(2))
            have 3:"flocal.ground_heads (head ?ut). extf f (>t) (args ?ut) (args ?us)"
              using extf_compat_append_left extf_map_ts less.prems(1) by auto
            show ?thesis using gt_same 1 2 3 by simp
          qed
        qed
      }
      note inner_induction = this
      show ?thesis using inner_induction[of "subst ρ (Hd (head t))", unfolded subst_apps[symmetric]]
        by (metis Var ghd order_refl subset_UNIV t_gt_s_same(1) tm_collapse_apps)
    next
      case (Sym _)
      then have "is_Sym (head (subst ρ t))" "head (subst ρ t) = head t"
        by simp_all
      then have "chkchop_same (>t) t s"
        using t_gt_s_same unfolding chkchop_same_def chkchop_def
        using Sym by metis
      then have gt_same2: "chkchop_same (>t) (subst ρ t) (subst ρ s)" unfolding chkchop_same_def chkchop_def
         using ih[of t "chop s"] 
         by (metis (no_types, lifting) Sym head (subst ρ t) = head t is_Sym (head (subst ρ t)) 
             add_mset_commute add_mset_lt_left_lt chop_subst_Sym ground_imp_subst_iden hd.simps(18) 
             hsize_chop_lt t_gt_s_same(1) tm.collapse(1) tm.simps(17))
      have gt_same3: "flocal.ground_heads (head (subst ρ t)). extf f (>t) (args (subst ρ t)) (args (subst ρ s))"
        using head (subst ρ t) = head t extf_compat_append_left extf_map_ts t_gt_s_same(1) by auto
      show ?thesis using gt_same gt_same1 gt_same2 gt_same3 by blast
    qed
  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). {# hsize t, hsize 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. {# hsize ta, hsize sa #} < {# hsize t, hsize 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 "chkchop (>t) t s  s >t t"
    unfolding chkchop_def tm.case_eq_if using ih[of t "chop s"]
    by (metis (no_types, lifting) add_mset_commute add_mset_lt_left_lt gr_s gr_t ground_chop gt_chop hsize_chop_lt)
  moreover have "chkchop (>t) s t  t >t s"
    unfolding chkchop_def tm.case_eq_if using ih[of "chop t" s]
    by (metis add_mset_lt_left_lt gr_s gr_t ground_chop gt_chop.intros gt_iff_chop_diff_same hsize_chop_lt)
  moreover
  {
    assume
      chkembs_t_s: "chkchop (>t) t s" and
      chkembs_s_t: "chkchop (>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))

    {
      assume g_gt_f: "g >s f"
      have "t >t s"
        using chkembs_t_s f g g_gt_f gt_diff gt_sym_imp_hd by auto
    }
    moreover
    {
      assume f_gt_g: "f >s g"
      have "s >t t" 
        using chkembs_s_t f f_gt_g g gt_diff gt_sym_imp_hd by auto
    }
    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"
          using chkembs_t_s g gt_same hd_t ts_gt_ss by auto
      }
      moreover
      {
        assume ss_gt_ts: "extf g (>t) ?ss ?ts"
        have "s >t t"
          using chkembs_s_t f g_eq_f gt_same hd_t ss_gt_ts by auto
      }
      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]
        using less_multiset_doubletons epo_axioms hsize_in_args in_listsI by (metis Un_iff)
    }
    ultimately have ?case
      using gt_sym_total by blast
  }
  ultimately show ?case
    by fast
qed


subsection ‹Well-foundedness›


lemma gt_imp_vars: "t >t s  vars t  vars s"
proof (simp only: atomize_imp,
    rule measure_induct_rule[of "λ(t, s). hsize t + hsize 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. hsize ta + hsize sa < hsize t + hsize 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_chop)
    thus ?thesis
      using ih
      by (metis add_mono_thms_linordered_field(1) le_supI1 order_refl hsize_chop_lt vars_chop)
  next
    case gt_diff
    show ?thesis 
    proof (cases s)
      case Hd
      thus ?thesis
        using gt_diff(2) 
        by (metis empty_iff hd.collapse(2) hd.simps(18) subsetI tm.sel(1) tm.simps(17))
    next
      case (App s1 s2)
      have "vars (chop s)  vars t" using ih 
        using App chkchop_def local.gt_diff(3) nat_add_left_cancel_less hsize_chop_lt tm.disc(2) by blast
      thus ?thesis 
        using  App  le_sup_iff local.gt_diff(2) tm.disc(2) vars_chop
        by (metis empty_iff hd.collapse(2) hd.simps(18) subsetI)
    qed
  next
    case gt_same
    thus ?thesis
    proof (cases "head t")
      case (Var x)
      then show ?thesis 
      proof (cases t)
        case (Hd _)
        then show ?thesis using Var local.gt_same(2) by force
      next
        case (App t1 t2)
        then show ?thesis
        proof (cases s)
          case (Hd _)
          then show ?thesis 
            using local.gt_same(1) vars_head_subseteq by fastforce
        next
          case (App s1 s2)
          then have "chop t >t chop s"
            using Var local.gt_same(2) by force
          then have "vars (chop s)  vars (chop t)" using ih[OF _ chop t >t chop s] 
            by (metis App Var add_less_mono chkchop_same_def hd.disc(1) hsize_chop_lt 
             local.gt_same(2) tm.disc(2))
          then show ?thesis using gt_same(1) vars_chop[of t] vars_chop[of s]
            by (metis App Var chkchop_same_def hd.disc(1) le_sup_iff local.gt_same(2) 
              sup.coboundedI1 tm.disc(2) vars_head_subseteq)
        qed
      qed
    next
      case (Sym f)
      then have "chkchop (>t) t s" using gt_same chkchop_same_def by auto
      then show ?thesis 
      proof (cases s)
        case (Hd _)
        then show ?thesis using local.gt_same(1) vars_head_subseteq by force 
      next
        case (App s1 s2)
        then show ?thesis unfolding chkchop_def using vars_chop ih[of t "chop s"] 
          by (metis chkchop (>t) t s chkchop_def le_sup_iff local.gt_same(1) 
              nat_add_left_cancel_less hsize_chop_lt tm.disc(2) vars_head_subseteq)
      qed
    qed
  qed      
qed  

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 ghd_UNIV: "x. ground_heads_var x = UNIV"
  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. hsize t > hsize s)"
    let ?U_of = "λi. {u. (?ff i) emb u}"

    note wf_sz = wf_app[OF wellorder_class.wf, of hsize, 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_u: "u. u  U  ground u" unfolding U_def
      using gr ground_emb by fastforce

    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: "hsize u < hsize ?ti"
        using emb_hsize_neq u_in by blast

      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"
          using gt_embedding_property u_in by blast
        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_chop (?ff i) (?ff (Suc i))" 
      proof
        assume a: "gt_chop (?ff i) (?ff (Suc i))"
        then have "chop (?ff i)  ?U_of i" 
          by (metis (mono_tags, lifting) emb_step_chop emb_step_is_emb gt_chop gt_chop.cases gt_irrefl mem_Collect_eq)
        then have  uij_in:"chop (?ff i)  U" unfolding U_def by fast

        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: "chop (?ff i) >t ?ff (Suc (Suc i))"
          using gt_trans by (metis (mono_tags, lifting) a gt_chop.cases)

        have "inf_chain (>tg) (λj. if j = 0 then chop (?ff i) 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) (chop (?ff i))"
          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_chop_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_chop_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 chkchop_def chkchop_same_def 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"
    thm UnionI CollectI
    have "t  set (args (?ff i))  t  U" for t i
      unfolding U_def apply (rule UnionI[of "?U_of i"]) 
      using arg_emb CollectI arg_emb hsize_in_args by fast+
    moreover have "i. extf f (>tg) (args (?ff (i + k))) (args (?ff (Suc i + k)))"
      using bad_same hd_eq_f unfolding  inf_chain_def gt_same.simps f_def hd.collapse(2)[OF ground_head, OF gr]
      using extf_mono_strong[of _ _ "(>t)" "(λt s. ground t  t >t s)" ] ground_hd_in_ground_heads 
      by (metis (no_types, lifting) ground_args)
    ultimately have "i. extf f ?gtu (args (?ff (i + k))) (args (?ff (Suc i + k)))"
      using extf_mono_strong[of _ _ "(λt s. ground t  t >t s)" "λ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
    using gt_sus ghd_UNIV ground_heads.simps(1) wary_grounding_ρ wfP_eq_minimal
    by (metis (no_types, lifting))
qed

end

end