Theory Lambda_Free_KBO_Std
section ‹The Graceful Standard Knuth--Bendix Order for Lambda-Free Higher-Order Terms›
theory Lambda_Free_KBO_Std
imports Lambda_Free_KBO_Util Nested_Multisets_Ordinals.Multiset_More
abbrevs ">t" = ">⇩t"
and "≥t" = "≥⇩t"
begin
text ‹
This theory defines the standard version of the graceful Knuth--Bendix order for ‹λ›-free
higher-order terms. Standard means that one symbol is allowed to have a weight of 0.
›
subsection ‹Setup›
locale kbo_std = kbo_std_basis _ _ arity_sym arity_var wt_sym
for
arity_sym :: "'s ⇒ enat" and
arity_var :: "'v ⇒ enat" and
wt_sym :: "'s ⇒ nat"
begin
subsection ‹Weights›
primrec wt :: "('s, 'v) tm ⇒ nat" where
"wt (Hd ζ) = (LEAST w. ∃f ∈ ground_heads ζ. w = wt_sym f + the_enat (δ * arity_sym f))"
| "wt (App s t) = (wt s - δ) + wt t"
lemma wt_Hd_Sym: "wt (Hd (Sym f)) = wt_sym f + the_enat (δ * arity_sym f)"
by simp
lemma exists_wt_sym: "∃f ∈ ground_heads ζ. wt (Hd ζ) = wt_sym f + the_enat (δ * arity_sym f)"
by (auto intro: Least_in_nonempty_set_imp_ex)
lemma wt_le_wt_sym: "f ∈ ground_heads ζ ⟹ wt (Hd ζ) ≤ wt_sym f + the_enat (δ * arity_sym f)"
using not_le_imp_less not_less_Least by fastforce
lemma enat_the_enat_δ_times_arity_sym[simp]: "enat (the_enat (δ * arity_sym f)) = δ * arity_sym f"
using arity_sym_ne_infinity_if_δ_gt_0 imult_is_infinity zero_enat_def by fastforce
lemma wt_arg_le: "wt (arg s) ≤ wt s"
by (cases s) auto
lemma wt_ge_ε: "wt s ≥ ε"
by (induct s, metis exists_wt_sym of_nat_eq_enat le_diff_conv of_nat_id wt_sym_ge,
simp add: add_increasing)
lemma wt_ge_δ: "wt s ≥ δ"
by (meson δ_le_ε order.trans enat_ord_simps(1) wt_ge_ε)
lemma wt_gt_δ_if_superunary: "arity_hd (head s) > 1 ⟹ wt s > δ"
proof (induct s)
case ζ: (Hd ζ)
obtain g where
g_in_grs: "g ∈ ground_heads ζ" and
wt_ζ: "wt (Hd ζ) = wt_sym g + the_enat (δ * arity_sym g)"
using exists_wt_sym by blast
have "arity_hd ζ > 1"
using ζ by auto
hence ary_g: "arity_sym g > 1"
using ground_heads_arity[OF g_in_grs] by simp
show ?case
proof (cases "δ = 0")
case True
thus ?thesis
by (metis ε_gt_0 gr0I leD wt_ge_ε)
next
case δ_ne_0: False
hence ary_g_ninf: "arity_sym g ≠ ∞"
using arity_sym_ne_infinity_if_δ_gt_0 by blast
hence "δ < the_enat (enat δ * arity_sym g)"
using δ_ne_0 ary_g by (cases "arity_sym g") (auto simp: one_enat_def)
thus ?thesis
unfolding wt_ζ by simp
qed
next
case (App s t)
thus ?case
using wt_ge_δ[of t] by force
qed
lemma wt_App_δ: "wt (App s t) = wt t ⟹ wt s = δ"
by (simp add: order.antisym wt_ge_δ)
lemma wt_App_ge_fun: "wt (App s t) ≥ wt s"
by (metis diff_le_mono2 wt_ge_δ le_diff_conv wt.simps(2))
lemma wt_hd_le: "wt (Hd (head s)) ≤ wt s"
by (induct s, simp) (metis head_App leD le_less_trans not_le_imp_less wt_App_ge_fun)
lemma wt_δ_imp_δ_eq_ε: "wt s = δ ⟹ δ = ε"
by (metis δ_le_ε le_antisym wt_ge_ε)
lemma wt_ge_arity_head_if_δ_gt_0:
assumes δ_gt_0: "δ > 0"
shows "wt s ≥ arity_hd (head s)"
proof (induct s)
case (Hd ζ)
obtain f where
f_in_ζ: "f ∈ ground_heads ζ" and
wt_ζ: "wt (Hd ζ) = wt_sym f + the_enat (δ * arity_sym f)"
using exists_wt_sym by blast
have "arity_sym f ≥ arity_hd ζ"
by (rule ground_heads_arity[OF f_in_ζ])
hence "the_enat (δ * arity_sym f) ≥ arity_hd ζ"
using δ_gt_0
by (metis One_nat_def Suc_ile_eq dual_order.trans enat_ord_simps(2)
enat_the_enat_δ_times_arity_sym i0_lb mult.commute mult.right_neutral mult_left_mono
one_enat_def)
thus ?case
unfolding wt_ζ by (metis add.left_neutral add_mono le_iff_add plus_enat_simps(1) tm.sel(1))
next
case App
thus ?case
by (metis dual_order.trans enat_ord_simps(1) head_App wt_App_ge_fun)
qed
lemma wt_ge_num_args_if_δ_eq_0:
assumes δ_eq_0: "δ = 0"
shows "wt s ≥ num_args s"
by (induct s, simp_all,
metis (no_types) δ_eq_0 ε_gt_0 wt_δ_imp_δ_eq_ε add_le_same_cancel1 le_0_eq le_trans
minus_nat.diff_0 not_gr_zero not_less_eq_eq)
lemma wt_ge_num_args: "wary s ⟹ wt s ≥ num_args s"
using wt_ge_arity_head_if_δ_gt_0 wt_ge_num_args_if_δ_eq_0
by (meson order.trans enat_ord_simps(1) neq0_conv wary_num_args_le_arity_head)
subsection ‹Inductive Definitions›
inductive gt :: "('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool" (infix ‹>⇩t› 50) where
gt_wt: "vars_mset t ⊇# vars_mset s ⟹ wt t > wt s ⟹ t >⇩t s"
| gt_unary: "wt t = wt s ⟹ ¬ head t ≤≥⇩h⇩d head s ⟹ num_args t = 1 ⟹
(∃f ∈ ground_heads (head t). arity_sym f = 1 ∧ wt_sym f = 0) ⟹ arg t >⇩t s ∨ arg t = s ⟹
t >⇩t s"
| gt_diff: "vars_mset t ⊇# vars_mset s ⟹ wt t = wt s ⟹ head t >⇩h⇩d head s ⟹ t >⇩t s"
| gt_same: "vars_mset t ⊇# vars_mset s ⟹ wt t = wt s ⟹ head t = head 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_wt :: "('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool" where
gt_wtI: "vars_mset t ⊇# vars_mset s ⟹ wt t > wt s ⟹ gt_wt t s"
inductive gt_diff :: "('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool" where
gt_diffI: "vars_mset t ⊇# vars_mset s ⟹ wt t = wt s ⟹ head t >⇩h⇩d head s ⟹ gt_diff t s"
inductive gt_unary :: "('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool" where
gt_unaryI: "wt t = wt s ⟹ ¬ head t ≤≥⇩h⇩d head s ⟹ num_args t = 1 ⟹
(∃f ∈ ground_heads (head t). arity_sym f = 1 ∧ wt_sym f = 0) ⟹ arg t ≥⇩t s ⟹ gt_unary t s"
inductive gt_same :: "('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool" where
gt_sameI: "vars_mset t ⊇# vars_mset s ⟹ wt t = wt s ⟹ head t = head s ⟹
(∀f ∈ ground_heads (head t). extf f (>⇩t) (args t) (args s)) ⟹ gt_same t s"
lemma gt_iff_wt_unary_diff_same: "t >⇩t s ⟷ gt_wt t s ∨ gt_unary t s ∨ gt_diff t s ∨ gt_same t s"
by (subst gt.simps) (auto simp: gt_wt.simps gt_unary.simps gt_diff.simps gt_same.simps)
lemma gt_imp_vars_mset: "t >⇩t s ⟹ vars_mset t ⊇# vars_mset s"
by (induct rule: gt.induct) (auto intro: subset_mset.trans)
lemma gt_imp_vars: "t >⇩t s ⟹ vars t ⊇ vars s"
using set_mset_mono[OF gt_imp_vars_mset] by simp
subsection ‹Irreflexivity›
theorem gt_irrefl: "wary s ⟹ ¬ s >⇩t s"
proof (induct "size s" arbitrary: s rule: less_induct)
case less
note ih = this(1) and wary_s = this(2)
show ?case
proof
assume s_gt_s: "s >⇩t s"
show False
using s_gt_s
proof (cases rule: gt.cases)
case gt_same
then obtain f where f: "extf f (>⇩t) (args s) (args s)"
by fastforce
thus False
using wary_s ih by (metis wary_args extf_irrefl size_in_args)
qed (auto simp: comp_hd_def gt_hd_irrefl)
qed
qed
subsection ‹Transitivity›
lemma gt_imp_wt_ge: "t >⇩t s ⟹ wt t ≥ wt s"
by (induct rule: gt.induct) auto
lemma not_extf_gt_nil_singleton_if_δ_eq_ε:
assumes wary_s: "wary s" and δ_eq_ε: "δ = ε"
shows "¬ extf f (>⇩t) [] [s]"
proof
assume nil_gt_s: "extf f (>⇩t) [] [s]"
note s_gt_nil = extf_singleton_nil_if_δ_eq_ε[OF δ_eq_ε, of f gt s]
have "¬ extf f (>⇩t) [] []"
by (rule extf_irrefl) simp
moreover have "extf f (>⇩t) [] []"
using extf_trans_from_irrefl[of "{s}", OF _ _ _ _ _ _ nil_gt_s s_gt_nil] gt_irrefl[OF wary_s]
by fastforce
ultimately show False
by sat
qed
lemma gt_sub_arg: "wary (App s t) ⟹ App s t >⇩t t"
proof (induct t arbitrary: s rule: measure_induct_rule[of size])
case (less t)
note ih = this(1) and wary_st = this(2)
{
assume wt_st: "wt (App s t) = wt t"
hence δ_eq_ε: "δ = ε"
using wt_App_δ wt_δ_imp_δ_eq_ε by metis
hence δ_gt_0: "δ > 0"
using ε_gt_0 by simp
have wt_s: "wt s = δ"
by (rule wt_App_δ[OF wt_st])
have
wary_t: "wary t" and
nargs_lt: "num_args s < arity_hd (head s)"
using wary_st wary.simps by blast+
have ary_hd_s: "arity_hd (head s) = 1"
by (metis One_nat_def arity.wary_AppE dual_order.order_iff_strict eSuc_enat enat_defs(1)
enat_defs(2) ileI1 linorder_not_le not_iless0 wary_st wt_gt_δ_if_superunary wt_s)
hence nargs_s: "num_args s = 0"
by (metis enat_ord_simps(2) less_one nargs_lt one_enat_def)
have "s = Hd (head s)"
by (simp add: Hd_head_id nargs_s)
then obtain f where
f_in: "f ∈ ground_heads (head s)" and
wt_f_etc: "wt_sym f + the_enat (δ * arity_sym f) = δ"
using exists_wt_sym wt_s by fastforce
have ary_f_1: "arity_sym f = 1"
proof -
have ary_f_ge_1: "arity_sym f ≥ 1"
using ary_hd_s f_in ground_heads_arity by fastforce
hence "enat δ * arity_sym f = δ"
using wt_f_etc by (metis enat_ord_simps(1) enat_the_enat_δ_times_arity_sym le_add2
le_antisym mult.right_neutral mult_left_mono zero_le)
thus ?thesis
using δ_gt_0 by (cases "arity_sym f") (auto simp: one_enat_def)
qed
hence wt_f_0: "wt_sym f = 0"
using wt_f_etc by simp
{
assume hd_s_ncmp_t: "¬ head s ≤≥⇩h⇩d head t"
have ?case
by (rule gt_unary[OF wt_st]) (auto simp: hd_s_ncmp_t nargs_s intro: f_in ary_f_1 wt_f_0)
}
moreover
{
assume hd_s_gt_t: "head s >⇩h⇩d head t"
have ?case
by (rule gt_diff) (auto simp: hd_s_gt_t wt_s[folded δ_eq_ε])
}
moreover
{
assume "head t >⇩h⇩d head s"
hence False
using ary_f_1 exists_wt_sym f_in gt_hd_def gt_sym_antisym unary_wt_sym_0_gt wt_f_0 by blast
}
moreover
{
assume hd_t_eq_s: "head t = head s"
hence nargs_t_le: "num_args t ≤ 1"
using ary_hd_s wary_num_args_le_arity_head[OF wary_t] by (simp add: one_enat_def)
have extf: "extf f (>⇩t) [t] (args t)" for f
proof (cases "args t")
case Nil
thus ?thesis
by (simp add: extf_singleton_nil_if_δ_eq_ε[OF δ_eq_ε])
next
case args_t: (Cons ta ts)
hence ts: "ts = []"
using ary_hd_s[folded hd_t_eq_s] wary_num_args_le_arity_head[OF wary_t]
nargs_t_le by simp
have ta: "ta = arg t"
by (metis apps.simps(1) apps.simps(2) args_t tm.sel(6) tm_collapse_apps ts)
hence t: "t = App (fun t) ta"
by (metis args.simps(1) args_t not_Cons_self2 tm.exhaust_sel ts)
have "t >⇩t ta"
by (rule ih[of ta "fun t", folded t, OF _ wary_t]) (metis ta size_arg_lt t tm.disc(2))
thus ?thesis
unfolding args_t ts by (metis extf_singleton gt_irrefl wary_t)
qed
have ?case
by (rule gt_same)
(auto simp: hd_t_eq_s wt_s[folded δ_eq_ε] length_0_conv[THEN iffD1, OF nargs_s] extf)
}
ultimately have ?case
unfolding comp_hd_def by metis
}
thus ?case
using gt_wt by fastforce
qed
lemma gt_arg: "wary s ⟹ is_App s ⟹ s >⇩t arg s"
by (cases s) (auto intro: gt_sub_arg)
theorem gt_trans: "wary u ⟹ wary t ⟹ wary s ⟹ 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). wary u ⟶ wary t ⟶ wary 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#} ⟹
wary ua ⟹ wary ta ⟹ wary sa ⟹ ua >⇩t ta ⟹ ta >⇩t sa ⟹ ua >⇩t sa" and
wary_u: "wary u" and wary_t: "wary t" and wary_s: "wary s" and
u_gt_t: "u >⇩t t" and t_gt_s: "t >⇩t s"
have "vars_mset u ⊇# vars_mset t" and "vars_mset t ⊇# vars_mset s"
using u_gt_t t_gt_s by (auto simp: gt_imp_vars_mset)
hence vars_u_s: "vars_mset u ⊇# vars_mset s"
by auto
have wt_u_ge_t: "wt u ≥ wt t" and wt_t_ge_s: "wt t ≥ wt s"
using gt_imp_wt_ge u_gt_t t_gt_s by auto
{
assume wt_t_s: "wt t = wt s" and wt_u_t: "wt u = wt t"
hence wt_u_s: "wt u = wt s"
by simp
have wary_arg_u: "wary (arg u)"
by (rule wary_arg[OF wary_u])
have wary_arg_t: "wary (arg t)"
by (rule wary_arg[OF wary_t])
have wary_arg_s: "wary (arg s)"
by (rule wary_arg[OF wary_s])
have "u >⇩t s"
using t_gt_s
proof cases
case gt_unary_t_s: gt_unary
have t_app: "is_App t"
by (metis args_Nil_iff_is_Hd gt_unary_t_s(3) length_greater_0_conv less_numeral_extra(1))
have δ_eq_ε: "δ = ε"
using gt_unary_t_s(4) unary_wt_sym_0_imp_δ_eq_ε by blast
show ?thesis
using u_gt_t
proof cases
case gt_unary_u_t: gt_unary
have u_app: "is_App u"
by (metis args_Nil_iff_is_Hd gt_unary_u_t(3) length_greater_0_conv less_numeral_extra(1))
hence arg_u_gt_s: "arg u >⇩t s"
using ih[of "arg u" t s] gt_unary_u_t(5) t_gt_s size_arg_lt wary_arg_u wary_s wary_t
by force
hence arg_u_ge_s: "arg u ≥⇩t s"
by sat
{
assume "size (arg u) < size t"
hence ?thesis
using ih[of u "arg u" s] arg_u_gt_s gt_arg by (simp add: u_app wary_arg_u wary_s wary_u)
}
moreover
{
assume "size (arg t) < size s"
hence "u >⇩t arg t"
using ih[of u t "arg t"] args_Nil_iff_is_Hd gt_arg gt_unary_t_s(3) u_gt_t wary_t wary_u
by force
hence ?thesis
using ih[of u "arg t" s] args_Nil_iff_is_Hd gt_unary_t_s(3,5) size_arg_lt wary_arg_t
wary_s wary_u by force
}
moreover
{
assume sz_u_gt_t: "size u > size t" and sz_t_gt_s: "size t > size s"
have wt_fun_u: "wt (fun u) = δ"
by (metis antisym gt_imp_wt_ge gt_unary_u_t(5) tm.collapse(2) u_app wt_App_δ wt_arg_le
wt_t_s wt_u_s)
have nargs_fun_u: "num_args (fun u) = 0"
by (metis args.simps(1) gt_unary_u_t(3) list.size(3) one_arg_imp_Hd tm.collapse(2)
u_app)
{
assume hd_u_eq_s: "head u = head s"
hence ary_hd_s: "arity_hd (head s) = 1"
using ground_heads_arity gt_unary_u_t(3,4) hd_u_eq_s one_enat_def
wary_num_args_le_arity_head wary_u by fastforce
have extf: "extf f (>⇩t) (args u) (args s)" for f
proof (cases "args s")
case Nil
thus ?thesis
by (metis Hd_head_id δ_eq_ε append_Nil args.simps(2) extf_singleton_nil_if_δ_eq_ε
gt_unary_u_t(3) head_fun length_greater_0_conv less_irrefl_nat nargs_fun_u
tm.exhaust_sel zero_neq_one)
next
case args_s: (Cons sa ss)
hence ss: "ss = []"
by (cases s, simp, metis One_nat_def antisym_conv ary_hd_s diff_Suc_1
enat_ord_simps(1) le_add2 length_0_conv length_Cons list.size(4) one_enat_def
wary_num_args_le_arity_head wary_s)
have sa: "sa = arg s"
by (metis apps.simps(1) apps.simps(2) args_s tm.sel(6) tm_collapse_apps ss)
have s_app: "is_App s"
using args_Nil_iff_is_Hd args_s by force
have args_u: "args u = [arg u]"
by (metis append_Nil args.simps(2) args_Nil_iff_is_Hd gt_unary_u_t(3) length_0_conv
nargs_fun_u tm.collapse(2) zero_neq_one)
have max_sz_u_t_s: "Max {size s, size t, size u} = size u"
using sz_t_gt_s sz_u_gt_t by auto
have max_sz_arg_u_t_arg_t: "Max {size (arg t), size t, size (arg u)} < size u"
using size_arg_lt sz_u_gt_t t_app u_app by fastforce
have "{#size (arg u), size t, size (arg t)#} < {#size u, size t, size s#}"
using max_sz_arg_u_t_arg_t
by (simp add: Max_lt_imp_lt_mset insert_commute max_sz_u_t_s)
hence arg_u_gt_arg_t: "arg u >⇩t arg t"
using ih[OF _ wary_arg_u wary_t wary_arg_t] args_Nil_iff_is_Hd gt_arg
gt_unary_t_s(3) gt_unary_u_t(5) wary_t by force
have max_sz_arg_s_s_arg_t: "Max {size (arg s), size s, size (arg t)} < size u"
using s_app t_app size_arg_lt sz_t_gt_s sz_u_gt_t by force
have "{#size (arg t), size s, size (arg s)#} < {#size u, size t, size s#}"
by (meson add_mset_lt_lt_lt less_trans mset_lt_single_iff s_app size_arg_lt
sz_t_gt_s sz_u_gt_t t_app)
hence arg_t_gt_arg_s: "arg t >⇩t arg s"
using ih[OF _ wary_arg_t wary_s wary_arg_s]
gt_unary_t_s(5) gt_arg args_Nil_iff_is_Hd args_s wary_s by force
have "arg u >⇩t arg s"
using ih[of "arg u" "arg t" "arg s"] arg_u_gt_arg_t arg_t_gt_arg_s
by (simp add: add_mset_lt_le_lt less_imp_le_nat s_app size_arg_lt t_app u_app
wary_arg_s wary_arg_t wary_arg_u)
thus ?thesis
unfolding args_u args_s ss sa by (metis extf_singleton gt_irrefl wary_arg_u)
qed
have ?thesis
by (rule gt_same[OF vars_u_s wt_u_s hd_u_eq_s]) (simp add: extf)
}
moreover
{
assume "head u >⇩h⇩d head s"
hence ?thesis
by (rule gt_diff[OF vars_u_s wt_u_s])
}
moreover
{
assume "head s >⇩h⇩d head u"
hence False
using gt_hd_def gt_hd_irrefl gt_sym_antisym gt_unary_u_t(4) unary_wt_sym_0_gt by blast
}
moreover
{
assume "¬ head u ≤≥⇩h⇩d head s"
hence ?thesis
by (rule gt_unary[OF wt_u_s _ gt_unary_u_t(3,4) arg_u_ge_s])
}
ultimately have ?thesis
unfolding comp_hd_def by sat
}
ultimately show ?thesis
by (metis args_Nil_iff_is_Hd dual_order.strict_trans2 gt_unary_t_s(3) gt_unary_u_t(3)
length_0_conv not_le_imp_less size_arg_lt zero_neq_one)
next
case gt_diff_u_t: gt_diff
have False
using gt_diff_u_t(3) gt_hd_def gt_hd_irrefl gt_sym_antisym gt_unary_t_s(4)
unary_wt_sym_0_gt by blast
thus ?thesis
by sat
next
case gt_same_u_t: gt_same
have hd_u_ncomp_s: "¬ head u ≤≥⇩h⇩d head s"
by (rule gt_unary_t_s(2)[folded gt_same_u_t(3)])
have "num_args u ≤ 1"
by (metis enat_ord_simps(1) ground_heads_arity gt_same_u_t(3) gt_unary_t_s(4) one_enat_def
order_trans wary_num_args_le_arity_head wary_u)
hence nargs_u: "num_args u = 1"
by (cases "args u",
metis Hd_head_id δ_eq_ε append_Nil args.simps(2) gt_same_u_t(3,4) gt_unary_t_s(3,4)
head_fun list.size(3) not_extf_gt_nil_singleton_if_δ_eq_ε one_arg_imp_Hd
tm.collapse(2)[OF t_app] wary_arg_t,
simp)
have "arg u >⇩t arg t"
by (metis extf_singleton[THEN iffD1] append_Nil args.simps args_Nil_iff_is_Hd
comp_hd_def gt_hd_def gt_irrefl gt_same_u_t(3,4) gt_unary_t_s(2,3) head_fun
length_0_conv nargs_u one_arg_imp_Hd t_app tm.collapse(2) u_gt_t wary_u)
hence "arg u >⇩t s"
using ih[OF _ wary_arg_u wary_arg_t wary_s] gt_unary_t_s(5)
by (metis add_mset_lt_left_lt add_mset_lt_lt_lt args_Nil_iff_is_Hd list.size(3) nargs_u
size_arg_lt t_app zero_neq_one)
hence arg_u_ge_s: "arg u ≥⇩t s"
by sat
show ?thesis
by (rule gt_unary[OF wt_u_s hd_u_ncomp_s nargs_u _ arg_u_ge_s])
(simp add: gt_same_u_t(3) gt_unary_t_s(4))
qed (simp add: wt_u_t)
next
case gt_diff_t_s: gt_diff
show ?thesis
using u_gt_t
proof cases
case gt_unary_u_t: gt_unary
have "is_App u"
by (metis args_Nil_iff_is_Hd gt_unary_u_t(3) length_greater_0_conv less_numeral_extra(1))
hence "arg u >⇩t s"
using ih[of "arg u" t s] gt_unary_u_t(5) t_gt_s size_arg_lt wary_arg_u wary_s wary_t
by force
hence arg_u_ge_s: "arg u ≥⇩t s"
by sat
{
assume "head u = head s"
hence False
using gt_diff_t_s(3) gt_unary_u_t(2) unfolding comp_hd_def by force
}
moreover
{
assume "head s >⇩h⇩d head u"
hence False
using gt_hd_def gt_hd_irrefl gt_sym_antisym gt_unary_u_t(4) unary_wt_sym_0_gt by blast
}
moreover
{
assume "head u >⇩h⇩d head s"
hence ?thesis
by (rule gt_diff[OF vars_u_s wt_u_s])
}
moreover
{
assume "¬ head u ≤≥⇩h⇩d head s"
hence ?thesis
by (rule gt_unary[OF wt_u_s _ gt_unary_u_t(3,4) arg_u_ge_s])
}
ultimately show ?thesis
unfolding comp_hd_def by sat
next
case gt_diff_u_t: gt_diff
have "head u >⇩h⇩d head s"
using gt_diff_u_t(3) gt_diff_t_s(3) gt_hd_trans by blast
thus ?thesis
by (rule gt_diff[OF vars_u_s wt_u_s])
next
case gt_same_u_t: gt_same
have "head u >⇩h⇩d head s"
using gt_diff_t_s(3) gt_same_u_t(3) by simp
thus ?thesis
by (rule gt_diff[OF vars_u_s wt_u_s])
qed (simp add: wt_u_t)
next
case gt_same_t_s: gt_same
show ?thesis
using u_gt_t
proof cases
case gt_unary_u_t: gt_unary
have "is_App u"
by (metis args_Nil_iff_is_Hd gt_unary_u_t(3) length_greater_0_conv less_numeral_extra(1))
hence "arg u >⇩t s"
using ih[of "arg u" t s] gt_unary_u_t(5) t_gt_s size_arg_lt wary_arg_u wary_s wary_t
by force
hence arg_u_ge_s: "arg u ≥⇩t s"
by sat
have "¬ head u ≤≥⇩h⇩d head s"
using gt_same_t_s(3) gt_unary_u_t(2) by simp
thus ?thesis
by (rule gt_unary[OF wt_u_s _ gt_unary_u_t(3,4) arg_u_ge_s])
next
case gt_diff_u_t: gt_diff
have "head u >⇩h⇩d head s"
using gt_diff_u_t(3) gt_same_t_s(3) by simp
thus ?thesis
by (rule gt_diff[OF vars_u_s wt_u_s])
next
case gt_same_u_t: gt_same
have hd_u_s: "head u = head s"
by (simp only: gt_same_t_s(3) gt_same_u_t(3))
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"
have wary_sa: "wary sa" and wary_ta: "wary ta" and wary_ua: "wary ua"
using wary_args ua_in ta_in sa_in wary_u wary_t wary_s by blast+
show "ua >⇩t sa"
by (auto intro!: ih[OF Max_lt_imp_lt_mset wary_ua wary_ta wary_sa 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)"
by (clarify, rule extf_trans_from_irrefl[of ?S _ "args t", OF _ _ _ _ _ gt_trans_args])
(auto simp: gt_same_u_t(3,4) gt_same_t_s(4) wary_args wary_u wary_t wary_s gt_irrefl)
thus ?thesis
by (rule gt_same[OF vars_u_s wt_u_s hd_u_s])
qed (simp add: wt_u_t)
qed (simp add: wt_t_s)
}
thus "u >⇩t s"
using vars_u_s wt_t_ge_s wt_u_ge_t by (force intro: gt_wt)
qed
lemma gt_antisym: "wary s ⟹ wary t ⟹ 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"
proof (cases "wt (App s t) > wt s")
case True
thus ?thesis
using gt_wt by simp
next
case False
hence wt_st: "wt (App s t) = wt s"
by (meson order.antisym not_le_imp_less wt_App_ge_fun)
hence δ_eq_ε: "δ = ε"
by (metis add_diff_cancel_left' diff_diff_cancel wt_δ_imp_δ_eq_ε wt_ge_δ wt.simps(2))
have vars_st: "vars_mset (App s t) ⊇# vars_mset s"
by auto
have hd_st: "head (App s t) = head s"
by auto
have extf: "∀f ∈ ground_heads (head (App s t)). extf f (>⇩t) (args (App s t)) (args s)"
by (simp add: δ_eq_ε extf_snoc_if_δ_eq_ε)
show ?thesis
by (rule gt_same[OF vars_st wt_st hd_st extf])
qed
theorem gt_proper_sub: "wary t ⟹ proper_sub s t ⟹ t >⇩t s"
by (induct t) (auto intro: gt_sub_fun gt_sub_arg gt_trans sub.intros wary_sub)
subsection ‹Compatibility with Functions›
theorem gt_compat_fun:
assumes
wary_t: "wary t" and
t'_gt_t: "t' >⇩t t"
shows "App s t' >⇩t App s t"
proof -
have vars_st': "vars_mset (App s t') ⊇# vars_mset (App s t)"
by (simp add: t'_gt_t gt_imp_vars_mset)
show ?thesis
proof (cases "wt t' > wt t")
case True
hence wt_st': "wt (App s t') > wt (App s t)"
by (simp only: wt.simps)
show ?thesis
by (rule gt_wt[OF vars_st' wt_st'])
next
case False
hence "wt t' = wt t"
using t'_gt_t gt_imp_wt_ge order.not_eq_order_implies_strict by fastforce
hence wt_st': "wt (App s t') = wt (App s t)"
by (simp only: wt.simps)
have head_st': "head (App s t') = head (App s t)"
by simp
have extf: "⋀f. extf f (>⇩t) (args s @ [t']) (args s @ [t])"
using t'_gt_t by (metis extf_compat_list gt_irrefl[OF wary_t])
show ?thesis
by (rule gt_same[OF vars_st' wt_st' head_st']) (simp add: extf)
qed
qed
subsection ‹Compatibility with Arguments›
theorem gt_compat_arg:
assumes wary_s't: "wary (App s' t)" and s'_gt_s: "s' >⇩t s"
shows "App s' t >⇩t App s t"
proof -
have vars_s't: "vars_mset (App s' t) ⊇# vars_mset (App s t)"
by (simp add: s'_gt_s gt_imp_vars_mset)
show ?thesis
using s'_gt_s
proof cases
case gt_wt_s'_s: gt_wt
have "wt (App s' t) > wt (App s t)"
by (simp add: wt_ge_δ) (metis add_diff_assoc add_less_cancel_right gt_wt_s'_s(2) wt_ge_δ)
thus ?thesis
by (rule gt_wt[OF vars_s't])
next
case gt_unary_s'_s: gt_unary
have False
by (metis ground_heads_arity gt_unary_s'_s(3) gt_unary_s'_s(4) leD one_enat_def wary_AppE
wary_s't)
thus ?thesis
by sat
next
case _: gt_diff
thus ?thesis
by (simp add: gt_diff)
next
case gt_same_s'_s: gt_same
have wt_s't: "wt (App s' t) = wt (App s t)"
by (simp add: gt_same_s'_s(2))
have hd_s't: "head (App s' t) = head (App s t)"
by (simp add: gt_same_s'_s(3))
have "∀f ∈ ground_heads (head (App s' t)). extf f (>⇩t) (args (App s' t)) (args (App s t))"
using gt_same_s'_s(4) by (auto intro: extf_compat_append_right)
thus ?thesis
by (rule gt_same[OF vars_s't wt_s't hd_s't])
qed
qed
subsection ‹Stability under Substitution›
:: "('v ⇒ ('s, 'v) tm) ⇒ ('s, 'v) tm ⇒ nat" where
"extra_wt ρ s = (∑x ∈# vars_mset s. wt (ρ x) - wt (Hd (Var x)))"
lemma
[simp]: "extra_wt ρ (Hd (Var x)) = wt (ρ x) - wt (Hd (Var x))" and
[simp]: "extra_wt ρ (Hd (Sym f)) = 0" and
[simp]: "extra_wt ρ (App s t) = extra_wt ρ s + extra_wt ρ t"
unfolding extra_wt_def by simp+
lemma :
assumes vars_s: "vars_mset t ⊇# vars_mset s"
shows "extra_wt ρ t ≥ extra_wt ρ s"
proof (unfold extra_wt_def)
let ?diff = "λv. wt (ρ v) - wt (Hd (Var v))"
have "vars_mset s + (vars_mset t - vars_mset s) = vars_mset t"
using vars_s by (meson subset_mset.add_diff_inverse)
hence "{#?diff v. v ∈# vars_mset t#} =
{#?diff v. v ∈# vars_mset s#} + {#?diff v. v ∈# vars_mset t - vars_mset s#}"
by (metis image_mset_union)
thus "(∑v ∈# vars_mset t. ?diff v) ≥ (∑v ∈# vars_mset s. ?diff v)"
by simp
qed
lemma wt_subst:
assumes wary_ρ: "wary_subst ρ" and wary_s: "wary s"
shows "wt (subst ρ s) = wt s + extra_wt ρ s"
using wary_s
proof (induct s rule: tm.induct)
case ζ: (Hd ζ)
show ?case
proof (cases ζ)
case x: (Var x)
let ?ξ = "head (ρ x)"
obtain g where
g_in_grs_ξ: "g ∈ ground_heads ?ξ" and
wt_ξ: "wt (Hd ?ξ) = wt_sym g + the_enat (δ * arity_sym g)"
using exists_wt_sym by blast
have "g ∈ ground_heads ζ"
using x g_in_grs_ξ wary_ρ wary_subst_def by auto
hence wt_ρx_ge: "wt (ρ x) ≥ wt (Hd ζ)"
by (metis (full_types) dual_order.trans wt_le_wt_sym wt_ξ wt_hd_le)
thus ?thesis
using x by (simp add: extra_wt_def)
qed auto
next
case (App s t)
note ih_s = this(1) and ih_t = this(2) and wary_st = this(3)
have "wary s"
using wary_st by (meson wary_AppE)
hence "⋀n. extra_wt ρ s + (wt s - δ + n) = wt (subst ρ s) - δ + n"
using ih_s by (metis (full_types) add_diff_assoc2 ab_semigroup_add_class.add_ac(1)
add.left_commute wt_ge_δ)
hence "extra_wt ρ s + (wt s + wt t - δ + extra_wt ρ t) = wt (subst ρ s) + wt (subst ρ t) - δ"
using ih_t wary_st
by (metis (no_types) add_diff_assoc2 ab_semigroup_add_class.add_ac(1) wary_AppE wt_ge_δ)
thus ?case
by (simp add: wt_ge_δ)
qed
theorem gt_subst:
assumes wary_ρ: "wary_subst ρ"
shows "wary t ⟹ wary s ⟹ 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). wary t ⟶ wary 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#} ⟹ wary ta ⟹ wary sa ⟹ ta >⇩t sa ⟹
subst ρ ta >⇩t subst ρ sa" and
wary_t: "wary t" and wary_s: "wary s" and t_gt_s: "t >⇩t s"
show "subst ρ t >⇩t subst ρ s"
proof (cases "wt (subst ρ t) = wt (subst ρ s)")
case wt_ρt_ne_ρs: False
have vars_s: "vars_mset t ⊇# vars_mset s"
by (simp add: t_gt_s gt_imp_vars_mset)
hence vars_ρs: "vars_mset (subst ρ t) ⊇# vars_mset (subst ρ s)"
by (rule vars_mset_subst_subseteq)
have wt_t_ge_s: "wt t ≥ wt s"
by (simp add: gt_imp_wt_ge t_gt_s)
have "wt (subst ρ t) > wt (subst ρ s)"
using wt_ρt_ne_ρs unfolding wt_subst[OF wary_ρ wary_s] wt_subst[OF wary_ρ wary_t]
by (metis add_le_cancel_left add_less_le_mono extra_wt_subseteq
order.not_eq_order_implies_strict vars_s wt_t_ge_s)
thus ?thesis
by (rule gt_wt[OF vars_ρs])
next
case wt_ρt_eq_ρs: True
show ?thesis
using t_gt_s
proof cases
case gt_wt
hence False
using wt_ρt_eq_ρs wary_s wary_t
by (metis add_diff_cancel_right' diff_le_mono2 extra_wt_subseteq wt_subst leD wary_ρ)
thus ?thesis
by sat
next
case gt_unary
have wary_ρt: "wary (subst ρ t)"
by (simp add: wary_subst_wary wary_t wary_ρ)
show ?thesis
proof (cases t)
case Hd
hence False
using gt_unary(3) by simp
thus ?thesis
by sat
next
case t: (App t1 t2)
hence t2: "t2 = arg t"
by simp
hence wary_t2: "wary t2"
using wary_t by blast
show ?thesis
proof (cases "t2 = s")
case True
moreover have "subst ρ t >⇩t subst ρ t2"
using gt_sub_arg wary_ρt unfolding t by simp
ultimately show ?thesis
by simp
next
case t2_ne_s: False
hence t2_gt_s: "t2 >⇩t s"
using gt_unary(5) t2 by blast
have "subst ρ t2 >⇩t subst ρ s"
by (rule ih[OF _ wary_t2 wary_s t2_gt_s]) (simp add: t)
thus ?thesis
by (metis gt_sub_arg gt_trans subst.simps(2) t wary_ρ wary_ρt wary_s wary_subst_wary
wary_t2)
qed
qed
next
case _: gt_diff
note vars_s = this(1) and hd_t_gt_hd_s = this(3)
have vars_ρs: "vars_mset (subst ρ t) ⊇# vars_mset (subst ρ s)"
by (rule vars_mset_subst_subseteq[OF vars_s])
have "head (subst ρ t) >⇩h⇩d head (subst ρ s)"
by (meson hd_t_gt_hd_s wary_subst_ground_heads gt_hd_def rev_subsetD wary_ρ)
thus ?thesis
by (rule gt_diff[OF vars_ρs wt_ρt_eq_ρs])
next
case _: gt_same
note vars_s = this(1) and hd_s_eq_hd_t = this(3) and extf = this(4)
have vars_ρs: "vars_mset (subst ρ t) ⊇# vars_mset (subst ρ s)"
by (rule vars_mset_subst_subseteq[OF vars_s])
have hd_ρt: "head (subst ρ t) = head (subst ρ s)"
by (simp add: hd_s_eq_hd_t)
{
fix f
assume f_in_grs: "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 extf f_in_grs wary_subst_ground_heads wary_ρ 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])
show "∀x ∈ ?S. ¬ subst ρ x >⇩t subst ρ x"
using gt_irrefl wary_t wary_s wary_args wary_ρ wary_subst_wary by fastforce
next
show "∀z ∈ ?S. ∀y ∈ ?S. ∀x ∈ ?S. subst ρ z >⇩t subst ρ y ⟶ subst ρ y >⇩t subst ρ x ⟶
subst ρ z >⇩t subst ρ x"
using gt_trans wary_t wary_s wary_args wary_ρ wary_subst_wary by (metis Un_iff)
next
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 "∀y ∈ ?S. ∀x ∈ ?S. y >⇩t x ⟶ subst ρ y >⇩t subst ρ x"
using ih sz_a size_in_args wary_t wary_s wary_args wary_ρ wary_subst_wary by fastforce
qed auto
hence "extf f (>⇩t) (args (subst ρ t)) (args (subst ρ s))"
by (auto simp: hd_s_eq_hd_t 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 vars_ρs wt_ρt_eq_ρs hd_ρt])
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). {# 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
vars_t: "vars_mset t ⊇# vars_mset s" and
vars_s: "vars_mset s ⊇# vars_mset t"
by (simp only: vars_mset_empty_iff[THEN iffD2, OF gr_s]
vars_mset_empty_iff[THEN iffD2, OF gr_t])+
show ?case
proof (cases "wt t = wt s")
case False
moreover
{
assume "wt t > wt s"
hence "t >⇩t s"
by (rule gt_wt[OF vars_t])
}
moreover
{
assume "wt s > wt t"
hence "s >⇩t t"
by (rule gt_wt[OF vars_s])
}
ultimately show ?thesis
by linarith
next
case wt_t: True
note wt_s = wt_t[symmetric]
obtain g where ξ: "head t = Sym g"
by (metis ground_head[OF gr_t] hd.collapse(2))
obtain f where ζ: "head s = Sym f"
by (metis ground_head[OF gr_s] hd.collapse(2))
{
assume g_gt_f: "g >⇩s f"
have "t >⇩t s"
by (rule gt_diff[OF vars_t wt_t]) (simp add: ξ ζ g_gt_f gt_hd_def)
}
moreover
{
assume f_gt_g: "f >⇩s g"
have "s >⇩t t"
by (rule gt_diff[OF vars_s wt_s]) (simp add: ξ ζ f_gt_g gt_hd_def)
}
moreover
{
assume g_eq_f: "g = f"
hence hd_t: "head t = head s"
using ξ ζ by force
note hd_s = hd_t[symmetric]
have gr_ts: "∀t ∈ set (args t). ground t"
using gr_t ground_args by auto
have gr_ss: "∀s ∈ set (args s). ground s"
using gr_s ground_args by auto
let ?ts = "args t"
let ?ss = "args s"
have ?thesis
proof (cases "?ts = ?ss")
case ts_eq_ss: True
show ?thesis
using ξ ζ g_eq_f ts_eq_ss by (simp add: tm_expand_apps)
next
case False
hence "extf g (>⇩t) (args t) ?ss ∨ extf g (>⇩t) ?ss ?ts"
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_commute Un_iff in_lists_iff_set less_multiset_doubletons size_in_args sup_ge2)
moreover
{
assume extf: "extf g (>⇩t) ?ts ?ss"
have "t >⇩t s"
by (rule gt_same[OF vars_t wt_t hd_t]) (simp add: extf ξ)
}
moreover
{
assume extf: "extf g (>⇩t) ?ss ?ts"
have "s >⇩t t"
by (rule gt_same[OF vars_s wt_s hd_s]) (simp add: extf[unfolded g_eq_f] ζ)
}
ultimately show ?thesis
by sat
qed
}
ultimately show ?thesis
using gt_sym_total by blast
qed
qed
subsection ‹Well-foundedness›
abbreviation gtw :: "('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool" (infix ‹>⇩t⇩w› 50) where
"(>⇩t⇩w) ≡ λt s. wary t ∧ wary s ∧ t >⇩t s"
abbreviation gtwg :: "('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool" (infix ‹>⇩t⇩w⇩g› 50) where
"(>⇩t⇩w⇩g) ≡ λt s. ground t ∧ t >⇩t⇩w s"
lemma ground_gt_unary:
assumes gr_t: "ground t"
shows "¬ gt_unary t s"
proof
assume gt_unary_t_s: "gt_unary t s"
hence "t >⇩t s"
using gt_iff_wt_unary_diff_same by blast
hence gr_s: "ground s"
using gr_t gt_imp_vars by blast
have ngr_t_or_s: "¬ ground t ∨ ¬ ground s"
using gt_unary_t_s by cases (blast dest: ground_head not_comp_hd_imp_Var)
show False
using gr_t gr_s ngr_t_or_s by sat
qed
theorem gt_wf: "wfP (λs t. t >⇩t⇩w s)"
proof -
have ground_wfP: "wfP (λs t. t >⇩t⇩w⇩g s)"
unfolding wfP_iff_no_inf_chain
proof
assume "∃f. inf_chain (>⇩t⇩w⇩g) f"
then obtain t where t_bad: "bad (>⇩t⇩w⇩g) t"
unfolding inf_chain_def bad_def by blast
let ?ff = "worst_chain (>⇩t⇩w⇩g) (λt s. size t > size s)"
note wf_sz = wf_app[OF wellorder_class.wf, of size, simplified]
have ffi_ground: "⋀i. ground (?ff i)" and ffi_wary: "⋀i. wary (?ff i)"
using worst_chain_bad[OF wf_sz t_bad, unfolded inf_chain_def] by fast+
have "inf_chain (>⇩t⇩w⇩g) ?ff"
by (rule worst_chain_bad[OF wf_sz t_bad])
hence bad_wt_diff_same:
"inf_chain (λt s. ground t ∧ (gt_wt t s ∨ gt_diff t s ∨ gt_same t s)) ?ff"
unfolding inf_chain_def using gt_iff_wt_unary_diff_same ground_gt_unary by blast
have wf_wt: "wf {(s, t). ground t ∧ gt_wt t s}"
by (rule wf_subset[OF wf_app[of _ wt, OF wf_less]]) (auto simp: gt_wt.simps)
have wt_O_diff_same: "{(s, t). ground t ∧ gt_wt t s}
O {(s, t). ground t ∧ (gt_diff t s ∨ gt_same t s)} ⊆ {(s, t). ground t ∧ gt_wt t s}"
unfolding gt_wt.simps gt_diff.simps gt_same.simps by auto
have wt_diff_same_as_union: "{(s, t). ground t ∧ (gt_wt t s ∨ gt_diff t s ∨ gt_same t s)} =
{(s, t). ground t ∧ gt_wt t s} ∪ {(s, t). ground t ∧ (gt_diff t s ∨ gt_same t s)}"
by auto
obtain k1 where bad_diff_same:
"inf_chain (λt s. ground t ∧ (gt_diff t s ∨ gt_same t s)) (λi. ?ff (i + k1))"
using wf_infinite_down_chain_compatible[OF wf_wt _ wt_O_diff_same, of ?ff] bad_wt_diff_same
unfolding inf_chain_def wt_diff_same_as_union[symmetric] by auto
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_wt_unary_diff_same gt_imp_vars by fastforce
show "sym (head t) >⇩s sym (head s)"
using gt_diff_t_s by cases (simp add: gt_hd_def gr_s gr_t ground_hd_in_ground_heads)
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 auto
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 k2 where bad_same: "inf_chain (λt s. ground t ∧ gt_same t s) (λi. ?ff (i + k2))"
using wf_infinite_down_chain_compatible[OF wf_diff _ diff_O_same, of "λi. ?ff (i + k1)"]
bad_diff_same
unfolding inf_chain_def diff_same_as_union[symmetric] by (auto simp: add.assoc)
hence hd_sym: "⋀i. is_Sym (head (?ff (i + k2)))"
unfolding inf_chain_def by (simp add: ground_head)
define f where "f = sym (head (?ff k2))"
have hd_eq_f: "head (?ff (i + k2)) = Sym f" for i
unfolding f_def
proof (induct i)
case 0
thus ?case
by (auto simp: 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
define max_args where "max_args = wt (?ff k2)"
have wt_eq_max_args: "wt (?ff (i + k2)) = max_args" for i
unfolding max_args_def
proof (induct i)
case (Suc ia)
thus ?case
using bad_same unfolding inf_chain_def gt_same.simps by simp
qed auto
have nargs_le_max_args: "num_args (?ff (i + k2)) ≤ max_args" for i
unfolding wt_eq_max_args[of i, symmetric] by (rule wt_ge_num_args[OF ffi_wary])
let ?U_of = "λi. set (args (?ff (i + k2)))"
define U where "U = (⋃i. ?U_of i)"
have gr_u: "⋀u. u ∈ U ⟹ ground u"
unfolding U_def by (blast dest: ground_args[OF _ ffi_ground])
have wary_u: "⋀u. u ∈ U ⟹ wary u"
unfolding U_def by (blast dest: wary_args[OF _ ffi_wary])
have "¬ bad (>⇩t⇩w⇩g) u" if u_in: "u ∈ ?U_of i" for u i
proof
assume u_bad: "bad (>⇩t⇩w⇩g) u"
have sz_u: "size u < size (?ff (i + k2))"
by (rule size_in_args[OF u_in])
show False
proof (cases "i + k2")
case 0
thus False
using sz_u min_worst_chain_0[OF wf_sz u_bad] by simp
next
case Suc
hence gt: "?ff (i + k2 - 1) >⇩t⇩w ?ff (i + k2)"
using worst_chain_pred[OF wf_sz t_bad] by auto
moreover have "?ff (i + k2) >⇩t⇩w u"
using gt gt_proper_sub sub_args sz_u u_in wary_args by auto
ultimately have "?ff (i + k2 - 1) >⇩t⇩w u"
using gt_trans by blast
thus False
using Suc sz_u min_worst_chain_Suc[OF wf_sz u_bad] ffi_ground by fastforce
qed
qed
hence u_good: "⋀u. u ∈ U ⟹ ¬ bad (>⇩t⇩w⇩g) u"
unfolding U_def by blast
let ?gtwu = "λt s. t ∈ U ∧ t >⇩t⇩w s"
have gtwu_irrefl: "⋀x. ¬ ?gtwu x x"
using gt_irrefl by auto
have "⋀i j. ∀t ∈ set (args (?ff (i + k2))). ∀s ∈ set (args (?ff (j + k2))). t >⇩t s ⟶
t ∈ U ∧ t >⇩t⇩w s"
using wary_u unfolding U_def by blast
moreover have "⋀i. extf f (>⇩t) (args (?ff (i + k2))) (args (?ff (Suc i + k2)))"
using bad_same hd_eq_f unfolding inf_chain_def gt_same.simps by auto
ultimately have "⋀i. extf f ?gtwu (args (?ff (i + k2))) (args (?ff (Suc i + k2)))"
by (rule extf_mono_strong)
hence "inf_chain (extf f ?gtwu) (λi. args (?ff (i + k2)))"
unfolding inf_chain_def by blast
hence nwf_ext:
"¬ wfP (λxs ys. length ys ≤ max_args ∧ length xs ≤ max_args ∧ extf f ?gtwu ys xs)"
unfolding inf_chain_def wfp_def wf_iff_no_infinite_down_chain using nargs_le_max_args by fast
have gtwu_le_gtwg: "?gtwu ≤ (>⇩t⇩w⇩g)"
by (auto intro!: gr_u)
have "wfP (λs t. ?gtwu t s)"
unfolding wfP_iff_no_inf_chain
proof (intro notI, elim exE)
fix f
assume bad_f: "inf_chain ?gtwu f"
hence bad_f0: "bad ?gtwu (f 0)"
by (rule inf_chain_bad)
hence "f 0 ∈ U"
using bad_f unfolding inf_chain_def by blast
hence "¬ bad (>⇩t⇩w⇩g) (f 0)"
using u_good by blast
hence "¬ bad ?gtwu (f 0)"
using bad_f inf_chain_bad inf_chain_subset[OF _ gtwu_le_gtwg] by blast
thus False
using bad_f0 by sat
qed
hence wf_ext: "wfP (λxs ys. length ys ≤ max_args ∧ length xs ≤ max_args ∧ extf f ?gtwu ys xs)"
using extf_wf_bounded[of ?gtwu] gtwu_irrefl by blast
show False
using nwf_ext wf_ext by blast
qed
let ?subst = "subst grounding_ρ"
have "wfP (λs t. ?subst t >⇩t⇩w⇩g ?subst s)"
by (rule wfP_app[OF ground_wfP])
hence "wfP (λs t. ?subst t >⇩t⇩w ?subst s)"
by (simp add: ground_grounding_ρ)
thus ?thesis
by (auto intro: wfp_subset wary_subst_wary[OF wary_grounding_ρ] gt_subst[OF wary_grounding_ρ])
qed
end
end