Theory KBO
section ‹KBO›
text ‹
Below, we formalize a variant of KBO that includes subterm coefficient functions.
A more standard definition is obtained by setting all subterm coefficients to 1.
For this special case it would be possible to define more efficient code-equations that
do not have to evaluate subterm coefficients at all.
›
theory KBO
imports
Lexicographic_Extension
First_Order_Terms.Subterm_and_Context
Polynomial_Factorization.Missing_List
begin
subsection ‹Subterm Coefficient Functions›
text ‹
Given a function @{term scf}, associating positions with subterm coefficients, and
a list @{term xs}, the function @{term scf_list} yields an expanded list where each
element of @{term xs} is replicated a number of times according to its subterm coefficient.
›
definition scf_list :: "(nat ⇒ nat) ⇒ 'a list ⇒ 'a list"
where
"scf_list scf xs = concat (map (λ(x, i). replicate (scf i) x) (zip xs [0 ..< length xs]))"
lemma set_scf_list [simp]:
assumes "∀i < length xs. scf i > 0"
shows "set (scf_list scf xs) = set xs"
using assms by (auto simp: scf_list_def set_zip set_conv_nth[of xs])
lemma scf_list_subset: "set (scf_list scf xs) ⊆ set xs"
by (auto simp: scf_list_def set_zip)
lemma scf_list_empty [simp]:
"scf_list scf [] = []" by (auto simp: scf_list_def)
lemma scf_list_bef_i_aft [simp]:
"scf_list scf (bef @ i # aft) =
scf_list scf bef @ replicate (scf (length bef)) i @
scf_list (λ i. scf (Suc (length bef + i))) aft"
unfolding scf_list_def
proof (induct aft rule: List.rev_induct)
case (snoc a aft)
define bia where "bia = bef @ i # aft"
have bia: "bef @ i # aft @ [a] = bia @ [a]" by (simp add: bia_def)
have zip: "zip (bia @ [a]) [0..<length (bia @ [a])]
= zip bia [0..<length bia] @ [(a, length bia)]" by simp
have concat:
"concat (map (λ(x, i). replicate (scf i) x) (zip bia [0..<length bia] @ [(a, length bia)])) =
concat (map (λ(x, i). replicate (scf i) x) (zip bia [0..<length bia])) @
replicate (scf (length bia)) a" by simp
show ?case
unfolding bia zip concat
unfolding bia_def snoc
by simp
qed simp
lemma scf_list_map [simp]:
"scf_list scf (map f xs) = map f (scf_list scf xs)"
by (induct xs rule: List.rev_induct) (auto simp: scf_list_def)
text ‹
The function @{term scf_term} replicates each argument a number of times according to its
subterm coefficient function.
›
fun scf_term :: "('f × nat ⇒ nat ⇒ nat) ⇒ ('f, 'v) term ⇒ ('f, 'v) term"
where
"scf_term scf (Var x) = (Var x)" |
"scf_term scf (Fun f ts) = Fun f (scf_list (scf (f, length ts)) (map (scf_term scf) ts))"
lemma vars_term_scf_subset:
"vars_term (scf_term scf s) ⊆ vars_term s"
proof (induct s)
case (Fun f ss)
have "vars_term (scf_term scf (Fun f ss)) =
(⋃x∈set (scf_list (scf (f, length ss)) ss). vars_term (scf_term scf x))" by auto
also have "… ⊆ (⋃x∈set ss. vars_term (scf_term scf x))"
using scf_list_subset [of _ ss] by blast
also have "… ⊆ (⋃x∈set ss. vars_term x)" using Fun by auto
finally show ?case by auto
qed auto
lemma scf_term_subst:
"scf_term scf (t ⋅ σ) = scf_term scf t ⋅ (λ x. scf_term scf (σ x))"
proof (induct t)
case (Fun f ts)
{ fix t
assume "t ∈ set (scf_list (scf (f, length ts)) ts)"
with scf_list_subset [of _ ts] have "t ∈ set ts" by auto
then have "scf_term scf (t ⋅ σ) = scf_term scf t ⋅ (λx. scf_term scf (σ x))" by (rule Fun) }
then show ?case by auto
qed auto
subsection ‹Weight Functions›
locale weight_fun =
fixes w :: "'f × nat ⇒ nat"
and w0 :: nat
and scf :: "'f × nat ⇒ nat ⇒ nat"
begin
text ‹
The ∗‹weight› of a term is computed recursively, where variables have weight @{term w0}
and the weight of a compound term is computed by adding the weight of its root symbol
@{term "w (f, n)"} to the weighted sum where weights of arguments are multiplied
according to their subterm coefficients.
›
fun weight :: "('f, 'v) term ⇒ nat"
where
"weight (Var x) = w0" |
"weight (Fun f ts) =
(let n = length ts; scff = scf (f, n) in
w (f, n) + sum_list (map (λ (ti, i). weight ti * scff i) (zip ts [0 ..< n])))"
text ‹
Alternatively, we can replicate arguments via @{const scf_list}.
The advantage is that then both @{const weight} and @{const scf_term} are defined
via @{const scf_list}.
›
lemma weight_simp [simp]:
"weight (Fun f ts) = w (f, length ts) + sum_list (map weight (scf_list (scf (f, length ts)) ts))"
proof -
define scff where "scff = (scf (f, length ts) :: nat ⇒ nat)"
have "(∑(ti, i) ← zip ts [0..<length ts]. weight ti * scff i) =
sum_list (map weight (scf_list scff ts))"
proof (induct ts rule: List.rev_induct)
case (snoc t ts)
moreover
{ fix n
have "sum_list (replicate n (weight t)) = n * weight t" by (induct n) auto }
ultimately show ?case by (simp add: scf_list_def)
qed simp
then show ?thesis by (simp add: Let_def scff_def)
qed
declare weight.simps(2)[simp del]
abbreviation "SCF ≡ scf_term scf"
lemma sum_list_scf_list:
assumes "⋀ i. i < length ts ⟹ f i > 0"
shows "sum_list (map weight ts) ≤ sum_list (map weight (scf_list f ts))"
using assms unfolding scf_list_def
proof (induct ts rule: List.rev_induct)
case (snoc t ts)
have "sum_list (map weight ts) ≤
sum_list (map weight (concat (map (λ(x, i). replicate (f i) x) (zip ts [0..<length ts]))))"
by (auto intro!: snoc)
moreover
from snoc(2) [of "length ts"] obtain n where "f (length ts) = Suc n" by (auto elim: lessE)
ultimately show ?case by simp
qed simp
end
subsection ‹Definition of KBO›
text ‹
The precedence is given by three parameters:
▪ a predicate @{term pr_strict} for strict decrease between two function symbols,
▪ a predicate @{term pr_weak} for weak decrease between two function symbols, and
▪ a function indicating whether a symbol is least in the precedence.
›
locale kbo = weight_fun w w0 scf
for w w0 and scf :: "'f × nat ⇒ nat ⇒ nat" +
fixes least :: "'f ⇒ bool"
and pr_strict :: "'f × nat ⇒ 'f × nat ⇒ bool"
and pr_weak :: "'f × nat ⇒ 'f × nat ⇒ bool"
begin
text ‹
The result of @{term kbo} is a pair of Booleans encoding strict/weak decrease.
Interestingly, the bound on the lengths of the lists in the lexicographic extension is not
required for KBO.
›
fun kbo :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ bool × bool"
where
"kbo s t = (if (vars_term_ms (SCF t) ⊆# vars_term_ms (SCF s) ∧ weight t ≤ weight s)
then if (weight t < weight s)
then (True, True)
else (case s of
Var y ⇒ (False, (case t of Var x ⇒ x = y | Fun g ts ⇒ ts = [] ∧ least g))
| Fun f ss ⇒ (case t of
Var x ⇒ (True, True)
| Fun g ts ⇒ if pr_strict (f, length ss) (g, length ts)
then (True, True)
else if pr_weak (f, length ss) (g, length ts)
then lex_ext_unbounded kbo ss ts
else (False, False)))
else (False, False))"
text ‹Abbreviations for strict (S) and nonstrict (NS) KBO.›
abbreviation "S ≡ λ s t. fst (kbo s t)"
abbreviation "NS ≡ λ s t. snd (kbo s t)"
text ‹
For code-generation we do not compute the weights of @{term s} and @{term t} repeatedly.
›
lemma kbo_code: "kbo s t = (let wt = weight t; ws = weight s in
if (vars_term_ms (SCF t) ⊆# vars_term_ms (SCF s) ∧ wt ≤ ws)
then if wt < ws
then (True, True)
else (case s of
Var y ⇒ (False, (case t of Var x ⇒ True | Fun g ts ⇒ ts = [] ∧ least g))
| Fun f ss ⇒ (case t of
Var x ⇒ (True, True)
| Fun g ts ⇒ let ff = (f, length ss); gg = (g, length ts) in
if pr_strict ff gg
then (True, True)
else if pr_weak ff gg
then lex_ext_unbounded kbo ss ts
else (False, False)))
else (False, False))"
unfolding kbo.simps[of s t] Let_def
by (auto simp del: kbo.simps split: term.splits)
end
declare kbo.kbo_code[code]
declare weight_fun.weight.simps[code]
lemma mset_replicate_mono:
assumes "m1 ⊆# m2"
shows "∑⇩# (mset (replicate n m1)) ⊆# ∑⇩# (mset (replicate n m2))"
proof (induct n)
case (Suc n)
have "∑⇩# (mset (replicate (Suc n) m1)) =
∑⇩# (mset (replicate n m1)) + m1" by simp
also have "… ⊆# ∑⇩# (mset (replicate n m1)) + m2" using ‹m1 ⊆# m2› by auto
also have "… ⊆# ∑⇩# (mset (replicate n m2)) + m2" using Suc by auto
finally show ?case by (simp add: union_commute)
qed simp
text ‹
While the locale @{locale kbo} only fixes its parameters, we now demand that these
parameters are sensible, e.g., encoding a well-founded precedence, etc.
›
locale admissible_kbo =
kbo w w0 scf least pr_strict pr_weak
for w w0 pr_strict pr_weak and least :: "'f ⇒ bool" and scf +
assumes w0: "w (f, 0) ≥ w0" "w0 > 0"
and adm: "w (f, 1) = 0 ⟹ pr_weak (f, 1) (g, n)"
and least: "least f = (w (f, 0) = w0 ∧ (∀ g. w (g, 0) = w0 ⟶ pr_weak (g, 0) (f, 0)))"
and scf: "i < n ⟹ scf (f, n) i > 0"
and pr_weak_refl [simp]: "pr_weak fn fn"
and pr_weak_trans: "pr_weak fn gm ⟹ pr_weak gm hk ⟹ pr_weak fn hk"
and pr_strict: "pr_strict fn gm ⟷ pr_weak fn gm ∧ ¬ pr_weak gm fn"
and pr_SN: "SN {(fn, gm). pr_strict fn gm}"
begin
lemma weight_w0: "weight t ≥ w0"
proof (induct t)
case (Fun f ts)
show ?case
proof (cases ts)
case Nil
with w0(1) have "w0 ≤ w (f, length ts)" by auto
then show ?thesis by auto
next
case (Cons s ss)
then obtain i where i: "i < length ts" by auto
from scf[OF this] have scf: "0 < scf (f, length ts) i" by auto
then obtain n where scf: "scf (f, length ts) i = Suc n" by (auto elim: lessE)
from id_take_nth_drop[OF i] i obtain bef aft where ts: "ts = bef @ ts ! i # aft" and ii: "length bef = i" by auto
define tsi where "tsi = ts ! i"
note ts = ts[folded tsi_def]
from i have tsi: "tsi ∈ set ts" unfolding tsi_def by auto
from Fun[OF this] have w0: "w0 ≤ weight tsi" .
show ?thesis using scf ii w0 unfolding ts
by simp
qed
qed simp
lemma weight_gt_0: "weight t > 0"
using weight_w0 [of t] and w0 by arith
lemma weight_0 [iff]: "weight t = 0 ⟷ False"
using weight_gt_0 [of t] by auto
lemma not_S_Var: "¬ S (Var x) t"
using weight_w0[of t] by (cases t, auto)
lemma S_imp_NS: "S s t ⟹ NS s t"
proof (induct s t rule: kbo.induct)
case (1 s t)
from 1(2) have S: "S s t" .
from S have w: "vars_term_ms (SCF t) ⊆# vars_term_ms (SCF s) ∧ weight t ≤ weight s"
by (auto split: if_splits)
note S = S w
note IH = 1(1)[OF w]
show ?case
proof (cases "weight t < weight s")
case True
with S show ?thesis by simp
next
case False
note IH = IH[OF False]
note S = S False
from not_S_Var[of _ t] S
obtain f ss where s: "s = Fun f ss" by (cases s, auto)
note IH = IH[OF s]
show ?thesis
proof (cases t)
case (Var x)
from S show ?thesis by (auto, insert Var s, auto)
next
case (Fun g ts)
note IH = IH[OF Fun]
let ?f = "(f, length ss)"
let ?g = "(g, length ts)"
let ?lex = "lex_ext_unbounded kbo ss ts"
from S[simplified, unfolded s Fun] have disj: "pr_strict ?f ?g ∨ pr_weak ?f ?g ∧ fst ?lex" by (auto split: if_splits)
show ?thesis
proof (cases "pr_strict ?f ?g")
case True
then show ?thesis using S s Fun by auto
next
case False
with disj have fg: "pr_weak ?f ?g" and lex: "fst ?lex" by auto
note IH = IH[OF False fg]
from lex have "fst (lex_ext kbo (length ss + length ts) ss ts)"
unfolding lex_ext_def Let_def by auto
from lex_ext_stri_imp_nstri[OF this] have lex: "snd ?lex"
unfolding lex_ext_def Let_def by auto
with False fg S s Fun show ?thesis by auto
qed
qed
qed
qed
subsection ‹Reflexivity and Irreflexivity›
lemma NS_refl: "NS s s"
proof (induct s)
case (Fun f ss)
have "snd (lex_ext kbo (length ss) ss ss)"
by (rule all_nstri_imp_lex_nstri, insert Fun[unfolded set_conv_nth], auto)
then have "snd (lex_ext_unbounded kbo ss ss)" unfolding lex_ext_def Let_def by simp
then show ?case by auto
qed simp
lemma pr_strict_irrefl: "¬ pr_strict fn fn"
unfolding pr_strict by auto
lemma S_irrefl: "¬ S t t"
proof (induct t)
case (Var x) then show ?case by (rule not_S_Var)
next
case (Fun f ts)
from pr_strict_irrefl have "¬ pr_strict (f, length ts) (f, length ts)" .
moreover
{ assume "fst (lex_ext_unbounded kbo ts ts)"
then obtain i where "i < length ts" and "S (ts ! i) (ts ! i)"
unfolding lex_ext_unbounded_iff by auto
with Fun have False by auto }
ultimately show ?case by auto
qed
subsection ‹Monotonicity (a.k.a. Closure under Contexts)›
lemma S_mono_one:
assumes S: "S s t"
shows "S (Fun f (ss1 @ s # ss2)) (Fun f (ss1 @ t # ss2))"
proof -
let ?ss = "ss1 @ s # ss2"
let ?ts = "ss1 @ t # ss2"
let ?s = "Fun f ?ss"
let ?t = "Fun f ?ts"
from S have w: "weight t ≤ weight s" and v: "vars_term_ms (SCF t) ⊆# vars_term_ms (SCF s)"
by (auto split: if_splits)
have v': "vars_term_ms (SCF ?t) ⊆# vars_term_ms (SCF ?s)" using mset_replicate_mono[OF v] by simp
have w': "weight ?t ≤ weight ?s" using sum_list_replicate_mono[OF w] by simp
have lex: "fst (lex_ext_unbounded kbo ?ss ?ts)"
unfolding lex_ext_unbounded_iff fst_conv
by (rule disjI1, rule exI[of _ "length ss1"], insert S NS_refl, auto simp del: kbo.simps simp: nth_append)
show ?thesis using v' w' lex by simp
qed
lemma S_ctxt: "S s t ⟹ S (C⟨s⟩) (C⟨t⟩)"
by (induct C, auto simp del: kbo.simps intro: S_mono_one)
lemma NS_mono_one:
assumes NS: "NS s t" shows "NS (Fun f (ss1 @ s # ss2)) (Fun f (ss1 @ t # ss2))"
proof -
let ?ss = "ss1 @ s # ss2"
let ?ts = "ss1 @ t # ss2"
let ?s = "Fun f ?ss"
let ?t = "Fun f ?ts"
from NS have w: "weight t ≤ weight s" and v: "vars_term_ms (SCF t) ⊆# vars_term_ms (SCF s)"
by (auto split: if_splits)
have v': "vars_term_ms (SCF ?t) ⊆# vars_term_ms (SCF ?s)" using mset_replicate_mono[OF v] by simp
have w': "weight ?t ≤ weight ?s" using sum_list_replicate_mono[OF w] by simp
have lex: "snd (lex_ext_unbounded kbo ?ss ?ts)"
unfolding lex_ext_unbounded_iff snd_conv
proof (intro disjI2 conjI allI impI)
fix i
assume "i < length (ss1 @ t # ss2)"
then show "NS (?ss ! i) (?ts ! i)" using NS NS_refl
by (cases "i = length ss1", auto simp del: kbo.simps simp: nth_append)
qed simp
show ?thesis using v' w' lex by simp
qed
lemma NS_ctxt: "NS s t ⟹ NS (C⟨s⟩) (C⟨t⟩)"
by (induct C, auto simp del: kbo.simps intro: NS_mono_one)
subsection ‹The Subterm Property›
lemma NS_Var_imp_eq_least: "NS (Var x) t ⟹ t = Var x ∨ (∃ f. t = Fun f [] ∧ least f)"
by (cases t, insert weight_w0[of t], auto split: if_splits)
lemma kbo_supt_one: "NS s (t :: ('f, 'v) term) ⟹ S (Fun f (bef @ s # aft)) t"
proof (induct t arbitrary: f s bef aft)
case (Var x)
note NS = this
let ?ss = "bef @ s # aft"
let ?t = "Var x"
have "length bef < length ?ss" by auto
from scf[OF this, of f] obtain n where scf:"scf (f, length ?ss) (length bef) = Suc n" by (auto elim: lessE)
obtain X where "vars_term_ms (SCF (Fun f ?ss)) = vars_term_ms (SCF s) + X"
by (simp add: o_def scf[simplified])
then have vs: "vars_term_ms (SCF s) ⊆# vars_term_ms (SCF (Fun f ?ss))" by simp
from NS have vt: "vars_term_ms (SCF ?t) ⊆# vars_term_ms (SCF s)" by (auto split: if_splits)
from vt vs have v: "vars_term_ms (SCF ?t) ⊆# vars_term_ms (SCF (Fun f ?ss))" by (rule subset_mset.order_trans)
from weight_w0[of "Fun f ?ss"] v show ?case by simp
next
case (Fun g ts f s bef aft)
let ?t = "Fun g ts"
let ?ss = "bef @ s # aft"
note NS = Fun(2)
note IH = Fun(1)
have "length bef < length ?ss" by auto
from scf[OF this, of f] obtain n where scff:"scf (f, length ?ss) (length bef) = Suc n" by (auto elim: lessE)
note scff = scff[simplified]
obtain X where "vars_term_ms (SCF (Fun f ?ss)) = vars_term_ms (SCF s) + X"
by (simp add: o_def scff)
then have vs: "vars_term_ms (SCF s) ⊆# vars_term_ms (SCF (Fun f ?ss))" by simp
have ws: "weight s ≤ sum_list (map weight (scf_list (scf (f, length ?ss)) ?ss))"
by (simp add: scff)
from NS have wt: "weight ?t ≤ weight s" and
vt: "vars_term_ms (SCF ?t) ⊆# vars_term_ms (SCF s)" by (auto split: if_splits)
from ws wt have w: "weight ?t ≤ sum_list (map weight (scf_list (scf (f, length ?ss)) ?ss))" by simp
from vt vs have v: "vars_term_ms (SCF ?t) ⊆# vars_term_ms (SCF (Fun f ?ss))" by auto
then have v': "(vars_term_ms (SCF ?t) ⊆# vars_term_ms (SCF (Fun f ?ss))) = True" by simp
show ?case
proof (cases "weight ?t = weight (Fun f ?ss)")
case False
with w v show ?thesis by auto
next
case True
from wt[unfolded True] weight_gt_0[of s]
have wf: "w (f, length ?ss) = 0"
and lsum: "sum_list (map weight (scf_list (scf (f, length ?ss)) bef)) = 0"
"sum_list (map weight (scf_list (λ i. (scf (f, length ?ss) (Suc (length bef) + i))) aft)) = 0"
and n: "n = 0"
by (auto simp: scff)
have "sum_list (map weight bef) ≤ sum_list (map weight (scf_list (scf (f, length ?ss)) bef))"
by (rule sum_list_scf_list, rule scf, auto)
with lsum(1) have "sum_list (map weight bef) = 0" by arith
then have bef: "bef = []" using weight_gt_0[of "hd bef"] by (cases bef, auto)
have "sum_list (map weight aft) ≤ sum_list (map weight (scf_list (λ i. (scf (f, length ?ss) (Suc (length bef) + i))) aft))"
by (rule sum_list_scf_list, rule scf, auto)
with lsum(2) have "sum_list (map weight aft) = 0" by arith
then have aft: "aft = []" using weight_gt_0[of "hd aft"] by (cases aft, auto)
note scff = scff[unfolded bef aft n, simplified]
from bef aft
have ba: "bef @ s # aft = [s]" by simp
with wf have wf: "w (f, 1) = 0" by auto
from wf have wst: "weight s = weight ?t" using scff unfolding True[unfolded ba]
by (simp add: scf_list_def)
let ?g = "(g, length ts)"
let ?f = "(f, 1)"
show ?thesis
proof (cases "pr_strict ?f ?g")
case True
with w v show ?thesis unfolding ba by simp
next
case False
note admf = adm[OF wf]
from admf have pg: "pr_weak ?f ?g" .
from pg False[unfolded pr_strict] have "pr_weak ?g ?f" by auto
from pr_weak_trans[OF this admf] have g: "⋀ h k. pr_weak ?g (h, k)" .
show ?thesis
proof (cases ts)
case Nil
have "fst (lex_ext_unbounded kbo [s] ts)"
unfolding Nil lex_ext_unbounded_iff by auto
with pg w v show ?thesis unfolding ba by simp
next
case (Cons t tts)
{
fix x
assume s: "s = Var x"
from NS_Var_imp_eq_least[OF NS[unfolded s Cons]] have False by auto
}
then obtain h ss where s: "s = Fun h ss" by (cases s, auto)
from NS wst g[of h "length ss"] pr_strict[of "(h, length ss)" "(g, length ts)"] have lex: "snd (lex_ext_unbounded kbo ss ts)"
unfolding s by (auto split: if_splits)
from lex obtain s0 sss where ss: "ss = s0 # sss" unfolding Cons lex_ext_unbounded_iff snd_conv by (cases ss, auto)
from lex[unfolded ss Cons] have "S s0 t ∨ NS s0 t"
by (cases "kbo s0 t", simp add: lex_ext_unbounded.simps del: kbo.simps split: if_splits)
with S_imp_NS[of s0 t] have "NS s0 t" by blast
from IH[OF _ this, of h Nil sss] have S: "S s t" unfolding Cons s ss by simp
have "fst (lex_ext_unbounded kbo [s] ts)" unfolding Cons
unfolding lex_ext_unbounded_iff fst_conv
by (rule disjI1[OF exI[of _ 0]], insert S, auto simp del: kbo.simps)
then have lex: "fst (lex_ext_unbounded kbo [s] ts) = True" by simp
note all = lex wst[symmetric] S pg scff v'
note all = all[unfolded ba, unfolded s ss Cons]
have w: "weight (Fun f [t]) = weight (t :: ('f, 'v) term)" for t
using wf scff by (simp add: scf_list_def)
show ?thesis unfolding ba unfolding s ss Cons
unfolding kbo.simps[of "Fun f [Fun h (s0 # sss)]"]
unfolding all w using all by simp
qed
qed
qed
qed
lemma S_supt:
assumes supt: "s ⊳ t"
shows "S s t"
proof -
from supt obtain C where s: "s = C⟨t⟩" and C: "C ≠ □" by auto
show ?thesis unfolding s using C
proof (induct C arbitrary: t)
case (More f bef C aft t)
show ?case
proof (cases "C = □")
case True
from kbo_supt_one[OF NS_refl, of f bef t aft] show ?thesis unfolding True by simp
next
case False
from kbo_supt_one[OF S_imp_NS[OF More(1)[OF False]], of f bef t aft]
show ?thesis by simp
qed
qed simp
qed
lemma NS_supteq:
assumes "s ⊵ t"
shows "NS s t"
using S_imp_NS[OF S_supt[of s t]] NS_refl[of s] using assms[unfolded subterm.le_less]
by blast
subsection ‹Least Elements›
lemma NS_all_least:
assumes l: "least f"
shows "NS t (Fun f [])"
proof (induct t)
case (Var x)
show ?case using l[unfolded least] l
by auto
next
case (Fun g ts)
show ?case
proof (cases ts)
case (Cons s ss)
with Fun[of s] have "NS s (Fun f [])" by auto
from S_imp_NS[OF kbo_supt_one[OF this, of g Nil ss]] show ?thesis unfolding Cons by simp
next
case Nil
from weight_w0[of "Fun g []"] have w: "weight (Fun g []) ≥ weight (Fun f [])"
using l[unfolded least] by auto
from lex_ext_least_1
have "snd (lex_ext kbo 0 [] [])" .
then have lex: "snd (lex_ext_unbounded kbo [] [])" unfolding lex_ext_def Let_def by simp
then show ?thesis using w l[unfolded least] unfolding Fun Nil by (auto simp: empty_le)
qed
qed
lemma not_S_least:
assumes l: "least f"
shows "¬ S (Fun f []) t"
proof (cases t)
case (Fun g ts)
show ?thesis unfolding Fun
proof
assume S: "S (Fun f []) (Fun g ts)"
from S[unfolded Fun, simplified]
have w: "w (g, length ts) + sum_list (map weight (scf_list (scf (g, length ts)) ts)) ≤ weight (Fun f [])"
by (auto split: if_splits)
show False
proof (cases ts)
case Nil
with w have "w (g, 0) ≤ weight (Fun f [])" by simp
also have "weight (Fun f []) ≤ w0" using l[unfolded least] by simp
finally have g: "w (g, 0) = w0" using w0(1)[of g] by auto
with w Nil l[unfolded least] have gf: "w (g, 0) = w (f, 0)" by simp
with S have p: "pr_weak (f, 0) (g, 0)" unfolding Nil
by (simp split: if_splits add: pr_strict)
with l[unfolded least, THEN conjunct2, rule_format, OF g] have p2: "pr_weak (g, 0) (f, 0)" by auto
from p p2 gf S have "fst (lex_ext_unbounded kbo [] ts)" unfolding Nil
by (auto simp: pr_strict)
then show False unfolding lex_ext_unbounded_iff by auto
next
case (Cons s ss)
then have ts: "ts = [] @ s # ss" by auto
from scf[of 0 "length ts" g] obtain n where scff: "scf (g, length ts) 0 = Suc n" unfolding Cons by (auto elim: lessE)
let ?e = "sum_list (map weight (
scf_list (λi. scf (g, Suc (length ss)) (Suc i)) ss
))"
have "w0 + sum_list (map weight (replicate n s)) ≤ weight s + sum_list (map weight (replicate n s))"
using weight_w0[of s] by auto
also have "… = sum_list (map weight (replicate (scf (g, length ts) 0) s))" unfolding scff by simp
also have "w (g, length ts) + … + ?e ≤ w0" using w l[unfolded least] unfolding ts scf_list_bef_i_aft by auto
finally have "w0 + sum_list (map weight (replicate n s)) + w (g, length ts) + ?e ≤ w0" by arith
then have wg: "w (g, length ts) = 0" and null: "?e = 0" "sum_list (map weight (replicate n s)) = 0" by auto
from null(2) weight_gt_0[of s] have n: "n = 0" by (cases n, auto)
have "sum_list (map weight ss) ≤ ?e"
by (rule sum_list_scf_list, rule scf, auto)
from this[unfolded null] weight_gt_0[of "hd ss"] have ss: "ss = []" by (cases ss, auto)
with Cons have ts: "ts = [s]" by simp
note scff = scff[unfolded ts n, simplified]
from wg ts have wg: "w (g, 1) = 0" by auto
from adm[OF wg, rule_format, of f] have "pr_weak (g, 1) (f, 0)" by auto
with S[unfolded Fun ts] l[unfolded least] weight_w0[of s] scff
have "fst (lex_ext_unbounded kbo [] [s])"
by (auto split: if_splits simp: scf_list_def pr_strict)
then show ?thesis unfolding lex_ext_unbounded_iff by auto
qed
qed
qed simp
lemma NS_least_least:
assumes l: "least f"
and NS: "NS (Fun f []) t"
shows "∃ g. t = Fun g [] ∧ least g"
proof (cases t)
case (Var x)
show ?thesis using NS unfolding Var by simp
next
case (Fun g ts)
from NS[unfolded Fun, simplified]
have w: "w (g, length ts) + sum_list (map weight (scf_list (scf (g, length ts)) ts)) ≤ weight (Fun f [])"
by (auto split: if_splits)
show ?thesis
proof (cases ts)
case Nil
with w have "w (g, 0) ≤ weight (Fun f [])" by simp
also have "weight (Fun f []) ≤ w0" using l[unfolded least] by simp
finally have g: "w (g, 0) = w0" using w0(1)[of g] by auto
with w Nil l[unfolded least] have gf: "w (g, 0) = w (f, 0)" by simp
with NS[unfolded Fun] have p: "pr_weak (f, 0) (g, 0)" unfolding Nil
by (simp split: if_splits add: pr_strict)
have least: "least g" unfolding least
proof (rule conjI[OF g], intro allI)
fix h
from l[unfolded least] have "w (h, 0) = w0 ⟶ pr_weak (h, 0) (f, 0)" by blast
with pr_weak_trans p show "w (h, 0) = w0 ⟶ pr_weak (h, 0) (g, 0)" by blast
qed
show ?thesis
by (rule exI[of _ g], unfold Fun Nil, insert least, auto)
next
case (Cons s ss)
then have ts: "ts = [] @ s # ss" by auto
from scf[of 0 "length ts" g] obtain n where scff: "scf (g, length ts) 0 = Suc n" unfolding Cons by (auto elim: lessE)
let ?e = "sum_list (map weight (
scf_list (λi. scf (g, Suc (length ss)) (Suc i)) ss
))"
have "w0 + sum_list (map weight (replicate n s)) ≤ weight s + sum_list (map weight (replicate n s))"
using weight_w0[of s] by auto
also have "… = sum_list (map weight (replicate (scf (g, length ts) 0) s))" unfolding scff by simp
also have "w (g, length ts) + … + ?e ≤ w0" using w l[unfolded least] unfolding ts scf_list_bef_i_aft by auto
finally have "w0 + sum_list (map weight (replicate n s)) + w (g, length ts) + ?e ≤ w0" by arith
then have wg: "w (g, length ts) = 0" and null: "?e = 0" "sum_list (map weight (replicate n s)) = 0" by auto
from null(2) weight_gt_0[of s] have n: "n = 0" by (cases n, auto)
have "sum_list (map weight ss) ≤ ?e"
by (rule sum_list_scf_list, rule scf, auto)
from this[unfolded null] weight_gt_0[of "hd ss"] have ss: "ss = []" by (cases ss, auto)
with Cons have ts: "ts = [s]" by simp
note scff = scff[unfolded ts n, simplified]
from wg ts have wg: "w (g, 1) = 0" by auto
from adm[OF wg, rule_format, of f] have "pr_weak (g, 1) (f, 0)" by auto
with NS[unfolded Fun ts] l[unfolded least] weight_w0[of s] scff
have "snd (lex_ext_unbounded kbo [] [s])"
by (auto split: if_splits simp: scf_list_def pr_strict)
then show ?thesis unfolding lex_ext_unbounded_iff snd_conv by auto
qed
qed
subsection ‹Stability (a.k.a. Closure under Substitutions›
lemma weight_subst: "weight (t ⋅ σ) =
weight t + sum_mset (image_mset (λ x. weight (σ x) - w0) (vars_term_ms (SCF t)))"
proof (induct t)
case (Var x)
show ?case using weight_w0[of "σ x"] by auto
next
case (Fun f ts)
let ?ts = "scf_list (scf (f, length ts)) ts"
define sts where "sts = ?ts"
have id: "map (λ t. weight (t ⋅ σ)) ?ts = map (λ t. weight t + sum_mset (image_mset (λ x. weight (σ x) - w0) (vars_term_ms (scf_term scf t)))) ?ts"
by (rule map_cong[OF refl Fun], insert scf_list_subset[of _ ts], auto)
show ?case
by (simp add: o_def id, unfold sts_def[symmetric], induct sts, auto)
qed
lemma weight_stable_le:
assumes ws: "weight s ≤ weight t"
and vs: "vars_term_ms (SCF s) ⊆# vars_term_ms (SCF t)"
shows "weight (s ⋅ σ) ≤ weight (t ⋅ σ)"
proof -
from vs[unfolded mset_subset_eq_exists_conv] obtain u where vt: "vars_term_ms (SCF t) = vars_term_ms (SCF s) + u" ..
show ?thesis unfolding weight_subst vt using ws by auto
qed
lemma weight_stable_lt:
assumes ws: "weight s < weight t"
and vs: "vars_term_ms (SCF s) ⊆# vars_term_ms (SCF t)"
shows "weight (s ⋅ σ) < weight (t ⋅ σ)"
proof -
from vs[unfolded mset_subset_eq_exists_conv] obtain u where vt: "vars_term_ms (SCF t) = vars_term_ms (SCF s) + u" ..
show ?thesis unfolding weight_subst vt using ws by auto
qed
text ‹KBO is stable, i.e., closed under substitutions.›
lemma kbo_stable:
fixes σ :: "('f, 'v) subst"
assumes "NS s t"
shows "(S s t ⟶ S (s ⋅ σ) (t ⋅ σ)) ∧ NS (s ⋅ σ) (t ⋅ σ)" (is "?P s t")
using assms
proof (induct s arbitrary: t)
case (Var y t)
then have not: "¬ S (Var y) t" using not_S_Var[of y t] by auto
from NS_Var_imp_eq_least[OF Var]
have "t = Var y ∨ (∃ f. t = Fun f [] ∧ least f)" by simp
then obtain f where "t = Var y ∨ t = Fun f [] ∧ least f" by auto
then have "NS (Var y ⋅ σ) (t ⋅ σ)"
proof
assume "t = Var y"
then show ?thesis using NS_refl[of "t ⋅ σ"] by auto
next
assume "t = Fun f [] ∧ least f"
with NS_all_least[of f "Var y ⋅ σ"] show ?thesis by auto
qed
with not show ?case by blast
next
case (Fun f ss t)
note NS = Fun(2)
note IH = Fun(1)
let ?s = "Fun f ss"
define s where "s = ?s"
let ?ss = "map (λ s. s ⋅ σ) ss"
from NS have v: "vars_term_ms (SCF t) ⊆# vars_term_ms (SCF ?s)" and w: "weight t ≤ weight ?s"
by (auto split: if_splits)
from weight_stable_le[OF w v] have wσ: "weight (t ⋅ σ) ≤ weight (?s ⋅ σ)" by auto
from vars_term_ms_subst_mono[OF v, of "λ x. SCF (σ x)"] have vσ: "vars_term_ms (SCF (t ⋅ σ)) ⊆# vars_term_ms (SCF (?s ⋅ σ))"
unfolding scf_term_subst .
show ?case
proof (cases "weight (t ⋅ σ) < weight (?s ⋅ σ)")
case True
with vσ show ?thesis by auto
next
case False
with weight_stable_lt[OF _ v, of σ] w have w: "weight t = weight ?s" by arith
show ?thesis
proof (cases t)
case (Var y)
from set_mset_mono[OF v, folded s_def]
have "y ∈ vars_term (SCF s)" unfolding Var by (auto simp: o_def)
also have "… ⊆ vars_term s" by (rule vars_term_scf_subset)
finally have "y ∈ vars_term s" by auto
from supteq_Var[OF this] have "?s ⊳ Var y" unfolding s_def Fun by auto
from S_supt[OF supt_subst[OF this]] have S: "S (?s ⋅ σ) (t ⋅ σ)" unfolding Var .
from S_imp_NS[OF S] S show ?thesis by auto
next
case (Fun g ts) note t = this
let ?f = "(f, length ss)"
let ?g = "(g, length ts)"
let ?ts = "map (λ s. s ⋅ σ) ts"
show ?thesis
proof (cases "pr_strict ?f ?g")
case True
then have S: "S (?s ⋅ σ) (t ⋅ σ)" using wσ vσ unfolding t by simp
from S S_imp_NS[OF S] show ?thesis by simp
next
case False note prec = this
show ?thesis
proof (cases "pr_weak ?f ?g")
case False
with v w prec have "¬ NS ?s t" unfolding t by (auto simp del: vars_term_ms.simps)
with NS show ?thesis by blast
next
case True
from v w have "vars_term_ms (SCF t) ⊆# vars_term_ms (SCF ?s) ∧ weight t ≤ weight ?s" "¬ weight t < weight ?s" by auto
{
fix i
assume i: "i < length ss" "i < length ts"
and S: "S (ss ! i) (ts ! i)"
have "S (map (λs. s ⋅ σ) ss ! i) (map (λs. s ⋅ σ) ts ! i)"
using IH[OF _ S_imp_NS[OF S]] S i unfolding set_conv_nth by (force simp del: kbo.simps)
} note IH_S = this
{
fix i
assume i: "i < length ss" "i < length ts"
and NS: "NS (ss ! i) (ts ! i)"
have "NS (map (λs. s ⋅ σ) ss ! i) (map (λs. s ⋅ σ) ts ! i)"
using IH[OF _ NS] i unfolding set_conv_nth by (force simp del: kbo.simps)
} note IH_NS = this
{
assume "S ?s t"
with prec v w True have lex: "fst (lex_ext_unbounded kbo ss ts)"
unfolding s_def t by simp
have "fst (lex_ext_unbounded kbo ?ss ?ts)"
by (rule lex_ext_unbounded_map_S[OF _ _ lex], insert IH_NS IH_S, blast+)
with vσ wσ prec True have "S (?s ⋅ σ) (t ⋅ σ)"
unfolding t by auto
}
moreover
{
from NS prec v w True have lex: "snd (lex_ext_unbounded kbo ss ts)"
unfolding t by simp
have "snd (lex_ext_unbounded kbo ?ss ?ts)"
by (rule lex_ext_unbounded_map_NS[OF _ _ lex], insert IH_S IH_NS, blast)
with vσ wσ prec True have "NS (?s ⋅ σ) (t ⋅ σ)"
unfolding t by auto
}
ultimately show ?thesis by auto
qed
qed
qed
qed
qed
lemma S_subst:
"S s t ⟹ S (s ⋅ (σ :: ('f, 'v) subst)) (t ⋅ σ)"
using kbo_stable[OF S_imp_NS, of s t σ] by auto
lemma NS_subst: "NS s t ⟹ NS (s ⋅ (σ :: ('f, 'v) subst)) (t ⋅ σ)" using kbo_stable[of s t σ] by auto
subsection ‹Transitivity and Compatibility›
lemma kbo_trans: "(S s t ⟶ NS t u ⟶ S s u) ∧
(NS s t ⟶ S t u ⟶ S s u) ∧
(NS s t ⟶ NS t u ⟶ NS s u)"
(is "?P s t u")
proof (induct s arbitrary: t u)
case (Var x t u)
from not_S_Var[of x t] have nS: "¬ S (Var x) t" .
show ?case
proof (cases "NS (Var x) t")
case False
with nS show ?thesis by blast
next
case True
from NS_Var_imp_eq_least[OF this] obtain f where
"t = Var x ∨ t = Fun f [] ∧ least f" by blast
then show ?thesis
proof
assume "t = Var x"
then show ?thesis using nS by blast
next
assume "t = Fun f [] ∧ least f"
then have t: "t = Fun f []" and least: "least f" by auto
from not_S_least[OF least] have nS': "¬ S t u" unfolding t .
show ?thesis
proof (cases "NS t u")
case True
with NS_least_least[OF least, of u] t obtain h where
u: "u = Fun h []" and least: "least h" by auto
from NS_all_least[OF least] have NS: "NS (Var x) u" unfolding u .
with nS nS' show ?thesis by blast
next
case False
with S_imp_NS[of t u] show ?thesis by blast
qed
qed
qed
next
case (Fun f ss t u) note IH = this
let ?s = "Fun f ss"
show ?case
proof (cases "NS ?s t")
case False
with S_imp_NS[of ?s t] show ?thesis by blast
next
case True note st = this
then have vst: "vars_term_ms (SCF t) ⊆# vars_term_ms (SCF ?s)" and wst: "weight t ≤ weight ?s"
by (auto split: if_splits)
show ?thesis
proof (cases "NS t u")
case False
with S_imp_NS[of t u] show ?thesis by blast
next
case True note tu = this
then have vtu: "vars_term_ms (SCF u) ⊆# vars_term_ms (SCF t)" and wtu: "weight u ≤ weight t"
by (auto split: if_splits)
from vst vtu have v: "vars_term_ms (SCF u) ⊆# vars_term_ms (SCF ?s)" by simp
from wst wtu have w: "weight u ≤ weight ?s" by simp
show ?thesis
proof (cases "weight u < weight ?s")
case True
with v show ?thesis by auto
next
case False
with wst wtu have wst: "weight t = weight ?s" and wtu: "weight u = weight t" and w: "weight u = weight ?s" by arith+
show ?thesis
proof (cases u)
case (Var z)
with v w show ?thesis by auto
next
case (Fun h us) note u = this
show ?thesis
proof (cases t)
case (Fun g ts) note t = this
let ?f = "(f, length ss)"
let ?g = "(g, length ts)"
let ?h = "(h, length us)"
from st t wst have fg: "pr_weak ?f ?g" by (simp split: if_splits add: pr_strict)
from tu t u wtu have gh: "pr_weak ?g ?h" by (simp split: if_splits add: pr_strict)
from pr_weak_trans[OF fg gh] have fh: "pr_weak ?f ?h" .
show ?thesis
proof (cases "pr_strict ?f ?h")
case True
with w v u show ?thesis by auto
next
case False
let ?lex = "lex_ext_unbounded kbo"
from False fh have hf: "pr_weak ?h ?f" unfolding pr_strict by auto
from pr_weak_trans[OF hf fg] have hg: "pr_weak ?h ?g" .
from hg have gh2: "¬ pr_strict ?g ?h" unfolding pr_strict by auto
from pr_weak_trans[OF gh hf] have gf: "pr_weak ?g ?f" .
from gf have fg2: "¬ pr_strict ?f ?g" unfolding pr_strict by auto
from st t wst fg2 have st: "snd (?lex ss ts)"
by (auto split: if_splits)
from tu t u wtu gh2 have tu: "snd (?lex ts us)"
by (auto split: if_splits)
{
fix s t u
assume "s ∈ set ss"
from IH[OF this, of t u]
have "(NS s t ∧ S t u ⟶ S s u) ∧
(S s t ∧ NS t u ⟶ S s u) ∧
(NS s t ∧ NS t u ⟶ NS s u) ∧
(S s t ∧ S t u ⟶ S s u)"
using S_imp_NS[of s t] by blast
} note IH = this
let ?b = "length ss + length ts + length us"
note lex = lex_ext_compat[of ss ts us kbo ?b, OF IH]
let ?lexb = "lex_ext kbo ?b"
note conv = lex_ext_def Let_def
from st have st: "snd (?lexb ss ts)" unfolding conv by simp
from tu have tu: "snd (?lexb ts us)" unfolding conv by simp
from lex st tu have su: "snd (?lexb ss us)" by blast
then have su: "snd (?lex ss us)" unfolding conv by simp
from w v u su fh have NS: "NS ?s u" by simp
{
assume st: "S ?s t"
with t wst fg fg2 have st: "fst (?lex ss ts)"
by (auto split: if_splits)
then have st: "fst (?lexb ss ts)" unfolding conv by simp
from lex st tu have su: "fst (?lexb ss us)" by blast
then have su: "fst (?lex ss us)" unfolding conv by simp
from w v u su fh have S: "S ?s u" by simp
} note S_left = this
{
assume tu: "S t u"
with t u wtu gh2 have tu: "fst (?lex ts us)"
by (auto split: if_splits)
then have tu: "fst (?lexb ts us)" unfolding conv by simp
from lex st tu have su: "fst (?lexb ss us)" by blast
then have su: "fst (?lex ss us)" unfolding conv by simp
from w v u su fh have S: "S ?s u" by simp
} note S_right = this
from NS S_left S_right show ?thesis by blast
qed
next
case (Var x) note t = this
from tu weight_w0[of u] have least: "least h" and u: "u = Fun h []" unfolding t u
by (auto split: if_splits)
from NS_all_least[OF least] have NS: "NS ?s u" unfolding u .
from not_S_Var have nS': "¬ S t u" unfolding t .
show ?thesis
proof (cases "S ?s t")
case False
with nS' NS show ?thesis by blast
next
case True
then have "vars_term_ms (SCF t) ⊆# vars_term_ms (SCF ?s)"
by (auto split: if_splits)
from set_mset_mono[OF this, unfolded set_mset_vars_term_ms t]
have "x ∈ vars_term (SCF ?s)" by simp
also have "… ⊆ vars_term ?s" by (rule vars_term_scf_subset)
finally obtain s sss where ss: "ss = s # sss" by (cases ss, auto)
from kbo_supt_one[OF NS_all_least[OF least, of s], of f Nil sss]
have "S ?s u" unfolding ss u by simp
with NS show ?thesis by blast
qed
qed
qed
qed
qed
qed
qed
lemma S_trans: "S s t ⟹ S t u ⟹ S s u" using S_imp_NS[of s t] kbo_trans[of s t u] by blast
lemma NS_trans: "NS s t ⟹ NS t u ⟹ NS s u" using kbo_trans[of s t u] by blast
lemma NS_S_compat: "NS s t ⟹ S t u ⟹ S s u" using kbo_trans[of s t u] by blast
lemma S_NS_compat: "S s t ⟹ NS t u ⟹ S s u" using kbo_trans[of s t u] by blast
subsection ‹Strong Normalization (a.k.a. Well-Foundedness)›
lemma kbo_strongly_normalizing:
fixes s :: "('f, 'v) term"
shows "SN_on {(s, t). S s t} {s}"
proof -
let ?SN = "λ t :: ('f, 'v) term. SN_on {(s, t). S s t} {t}"
let ?m1 = "λ (f, ss). weight (Fun f ss)"
let ?m2 = "λ (f, ss). (f, length ss)"
let ?rel' = "lex_two {(fss, gts). ?m1 fss > ?m1 gts} {(fss, gts). ?m1 fss ≥ ?m1 gts} {(fss, gts). pr_strict (?m2 fss) (?m2 gts)}"
let ?rel = "inv_image ?rel' (λ x. (x, x))"
have SN_rel: "SN ?rel"
by (rule SN_inv_image, rule lex_two, insert SN_inv_image[OF pr_SN, of ?m2] SN_inv_image[OF SN_nat_gt, of ?m1],
auto simp: inv_image_def)
note conv = SN_on_all_reducts_SN_on_conv
show "?SN s"
proof (induct s)
case (Var x)
show ?case unfolding conv[of _ "Var x"] using not_S_Var[of x] by auto
next
case (Fun f ss)
then have subset: "set ss ⊆ {s. ?SN s}" by blast
let ?P = "λ (f, ss). set ss ⊆ {s. ?SN s} ⟶ ?SN (Fun f ss)"
{
fix fss
have "?P fss"
proof (induct fss rule: SN_induct[OF SN_rel])
case (1 fss)
obtain f ss where fss: "fss = (f, ss)" by force
{
fix g ts
assume "?m1 (f, ss) > ?m1 (g, ts) ∨ ?m1 (f, ss) ≥ ?m1 (g, ts) ∧ pr_strict (?m2 (f, ss)) (?m2 (g, ts))"
and "set ts ⊆ {s. ?SN s}"
then have "?SN (Fun g ts)"
using 1[rule_format, of "(g, ts)", unfolded fss split] by auto
} note IH = this[unfolded split]
show ?case unfolding fss split
proof
assume SN_s: "set ss ⊆ {s. ?SN s}"
let ?f = "(f, length ss)"
let ?s = "Fun f ss"
let ?SNt = "λ g ts. ?SN (Fun g ts)"
let ?sym = "λ g ts. (g, length ts)"
let ?lex = "lex_ext kbo (weight ?s)"
let ?lexu = "lex_ext_unbounded kbo"
let ?lex_SN = "{(ys, xs). (∀ y ∈ set ys. ?SN y) ∧ fst (?lex ys xs)}"
from lex_ext_SN[of kbo "weight ?s", OF NS_S_compat]
have SN: "SN ?lex_SN" .
{
fix g and ts :: "('f, 'v) term list"
assume "pr_weak ?f (?sym g ts) ∧ weight (Fun g ts) ≤ weight ?s ∧ set ts ⊆ {s. ?SN s}"
then have "?SNt g ts"
proof (induct ts arbitrary: g rule: SN_induct[OF SN])
case (1 ts g)
note inner_IH = 1(1)
let ?g = "(g, length ts)"
let ?t = "Fun g ts"
from 1(2) have fg: "pr_weak ?f ?g" and w: "weight ?t ≤ weight ?s" and SN: "set ts ⊆ {s. ?SN s}" by auto
show "?SNt g ts" unfolding conv[of _ ?t]
proof (intro allI impI)
fix u
assume "(?t, u) ∈ {(s, t). S s t}"
then have tu: "S ?t u" by auto
then show "?SN u"
proof (induct u)
case (Var x)
then show ?case using not_S_Var[of x] unfolding conv[of _ "Var x"] by auto
next
case (Fun h us)
let ?h = "(h, length us)"
let ?u = "Fun h us"
note tu = Fun(2)
{
fix u
assume u: "u ∈ set us"
then have "?u ⊳ u" by auto
from S_trans[OF tu S_supt[OF this]] have "S ?t u" by auto
from Fun(1)[OF u this] have "?SN u" .
} then have SNu: "set us ⊆ {s . ?SN s}" by blast
note IH = IH[OF _ this]
from tu have wut: "weight ?u ≤ weight ?t" by (simp split: if_splits)
show ?case
proof (cases "?m1 (f, ss) > ?m1 (h, us) ∨ ?m1 (f, ss) ≥ ?m1 (h, us) ∧ pr_strict (?m2 (f, ss)) (?m2 (h, us))")
case True
from IH[OF True[unfolded split]] show ?thesis by simp
next
case False
with wut w have wut: "weight ?t = weight ?u" "weight ?s = weight ?u" by auto
note False = False[unfolded split wut]
note tu = tu[unfolded kbo.simps[of ?t] wut, unfolded Fun term.simps, simplified]
from tu have gh: "pr_weak ?g ?h" unfolding pr_strict by (auto split: if_splits)
from pr_weak_trans[OF fg gh] have fh: "pr_weak ?f ?h" .
from False wut fh have "¬ pr_strict ?f ?h" unfolding pr_strict by auto
with fh have hf: "pr_weak ?h ?f" unfolding pr_strict by auto
from pr_weak_trans[OF hf fg] have hg: "pr_weak ?h ?g" .
from hg have gh2: "¬ pr_strict ?g ?h" unfolding pr_strict by auto
from tu gh2 have lex: "fst (?lexu ts us)" by (auto split: if_splits)
from fh wut SNu have "pr_weak ?f ?h ∧ weight ?u ≤ weight ?s ∧ set us ⊆ {s. ?SN s}"
by auto
note inner_IH = inner_IH[OF _ this]
show ?thesis
proof (rule inner_IH, rule, unfold split, intro conjI ballI)
have "fst (?lexu ts us)" by (rule lex)
moreover have "length us ≤ weight ?s"
proof -
have "length us ≤ sum_list (map weight us)"
proof (induct us)
case (Cons u us)
from Cons have "length (u # us) ≤ Suc (sum_list (map weight us))" by auto
also have "... ≤ sum_list (map weight (u # us))" using weight_gt_0[of u]
by auto
finally show ?case .
qed simp
also have "… ≤ sum_list (map weight (scf_list (scf (h, length us)) us))"
by (rule sum_list_scf_list[OF scf])
also have "... ≤ weight ?s" using wut by simp
finally show ?thesis .
qed
ultimately show "fst (?lex ts us)" unfolding lex_ext_def Let_def by auto
qed (insert SN, blast)
qed
qed
qed
qed
}
from this[of f ss] SN_s show "?SN ?s" by auto
qed
qed
}
from this[of "(f, ss)", unfolded split]
show ?case using Fun by blast
qed
qed
lemma S_SN: "SN {(x, y). S x y}"
using kbo_strongly_normalizing unfolding SN_defs by blast
subsection ‹Ground Totality›
lemma ground_SCF [simp]:
"ground (SCF t) = ground t"
proof -
have *: "∀i<length xs. scf (f, length xs) i > 0"
for f :: 'f and xs :: "('f, 'v) term list" using scf by simp
show ?thesis by (induct t) (auto simp: set_scf_list [OF *])
qed
declare kbo.simps[simp del]
lemma ground_vars_term_ms: "ground t ⟹ vars_term_ms t = {#}"
by (induct t) auto
context
fixes F :: "('f × nat) set"
assumes pr_weak: "pr_weak = pr_strict⇧=⇧="
and pr_gtotal: "⋀f g. f ∈ F ⟹ g ∈ F ⟹ f = g ∨ pr_strict f g ∨ pr_strict g f"
begin
lemma S_ground_total:
assumes "funas_term s ⊆ F" and "ground s" and "funas_term t ⊆ F" and "ground t"
shows "s = t ∨ S s t ∨ S t s"
using assms
proof (induct s arbitrary: t)
case IH: (Fun f ss)
note [simp] = ground_vars_term_ms
let ?s = "Fun f ss"
have *: "(vars_term_ms (SCF t) ⊆# vars_term_ms (SCF ?s)) = True"
"(vars_term_ms (SCF ?s) ⊆# vars_term_ms (SCF t)) = True"
using ‹ground ?s› and ‹ground t› by (auto simp: scf)
from IH(5) obtain g ts where t[simp]: "t = Fun g ts" by (cases t, auto)
let ?t = "Fun g ts"
let ?f = "(f, length ss)"
let ?g = "(g, length ts)"
from IH have f: "?f ∈ F" and g: "?g ∈ F" by auto
{
assume "¬ ?case"
note contra = this[unfolded kbo.simps[of ?s] kbo.simps[of t] *, unfolded t term.simps]
from pr_gtotal[OF f g] contra have fg: "?f = ?g" by (auto split: if_splits)
have IH: "∀(s, t)∈set (zip ss ts). s = t ∨ S s t ∨ S t s"
using IH by (auto elim!: in_set_zipE) blast
from fg have len: "length ss = length ts" by auto
from lex_ext_unbounded_total[OF IH NS_refl len] contra fg
have False by (auto split: if_splits)
}
then show ?case by blast
qed auto
end
subsection ‹Summary›
text ‹
At this point we have shown well-foundedness @{thm [source] S_SN},
transitivity and compatibility @{thm [source] S_trans NS_trans NS_S_compat S_NS_compat},
closure under substitutions @{thm [source] S_subst NS_subst},
closure under contexts @{thm [source] S_ctxt NS_ctxt},
the subterm property @{thm [source] S_supt NS_supteq},
reflexivity of the weak @{thm [source] NS_refl} and irreflexivity of the strict
part @{thm [source] S_irrefl},
and ground-totality @{thm [source] S_ground_total}.
In particular, this allows us to show that KBO is an instance of
strongly normalizing order pairs (@{locale SN_order_pair}).
›
sublocale SN_order_pair "{(x, y). S x y}" "{(x, y). NS x y}"
by (unfold_locales, insert NS_refl NS_trans S_trans S_SN NS_S_compat S_NS_compat)
(auto simp: refl_on_def trans_def, blast+)
end
end