theory RPO
imports
"Check-NT.Term_Order_Impl"
QTRS.Lexicographic_Extension
"Check-NT.Reduction_Pair"
Reduction_Order_Impl
QTRS.Term_Impl
"../Auxiliaries/Multiset_Extension2"
Polynomial_Factorization.Missing_Multiset
begin
datatype order_tag = Lex | Mul
fun rpo :: "('f × nat ⇒ 'f × nat ⇒ bool × bool) × ('f × nat ⇒ bool) ⇒ ('f × nat ⇒ order_tag) ⇒ nat ⇒
('f, 'v) term ⇒ ('f, 'v) term ⇒ bool × bool"
where
"rpo _ _ _ (Var x) (Var y) = (False, x = y)" |
"rpo pr _ _ (Var x) (Fun g ts) = (False, ts = [] ∧ (snd pr) (g,0))" |
"rpo pr c n (Fun f ss) (Var y) = (let con = (∃ s ∈ set ss. snd (rpo pr c n s (Var y))) in (con,con))" |
"rpo pr c n (Fun f ss) (Fun g ts) = (
if (∃ s ∈ set ss. snd (rpo pr c n s (Fun g ts)))
then (True,True)
else (let (prs,prns) = (fst pr) (f,length ss) (g,length ts) in
if prns ∧ (∀ t ∈ set ts. fst (rpo pr c n (Fun f ss) t))
then if prs
then (True,True)
else if c (f,length ss) = Lex ∧ c (g,length ts) = Lex
then lex_ext (rpo pr c n) n ss ts
else if c (f,length ss) = Mul ∧ c (g,length ts) = Mul
then mul_ext (rpo pr c n) ss ts
else (length ss ≠ 0 ∧ length ts = 0, length ts = 0)
else (False,False)))"
lemma rpo_stri_imp_nstri[rule_format]: "fst (rpo pr c n s t) ⟶
snd (rpo pr c n s t)"
proof (induct rule: rpo.induct[of "λ pr c n s t. fst (rpo pr c n s t) ⟶ snd (rpo pr c n s t)"])
case (4 "pr" c n f ss g ts)
obtain prc prl where prec: "pr = (prc,prl)" by (cases "pr", auto)
obtain s ns where prc: "prc (f,length ss) (g,length ts) = (s,ns)" by force
show ?case
by (cases "length ss = length ts ∨ length ts ≤ n", auto simp: Let_def lex_ext_stri_imp_nstri
mul_ext_stri_imp_nstri prec prc)
qed (auto simp: Let_def)
locale rpo_pr = precedence prc prl
for prc :: "'f × nat ⇒ 'f × nat ⇒ bool × bool"
and prl :: "'f × nat ⇒ bool" +
fixes c :: "'f × nat ⇒ order_tag"
begin
abbreviation rpo_pr where "rpo_pr ≡ rpo pr c"
lemma rpo_nstri_refl:
shows "snd (rpo_pr n s s)"
proof (induct s)
let ?ns ="{(x, y). snd (rpo_pr n x y)}"
let ?s = "{(x, y). fst (rpo_pr n x y)}"
case (Fun f ss)
have rec11: "snd (lex_ext (rpo_pr n) n ss ss)"
by (rule all_nstri_imp_lex_nstri, auto simp: Fun)
have rec12: "snd (mul_ext (rpo_pr n) ss ss)"
using ns_mul_ext_refl_local[of ?ns "mset ss" ?s] and Fun and in_multiset_in_set[of ss]
unfolding mul_ext_def Let_def snd_conv locally_refl_def by simp
have rec21: "∀ s ∈ set ss. fst (rpo_pr n (Fun f ss) s)"
proof
fix s
assume s: "s ∈ set ss"
with Fun have rec: "snd (rpo_pr n s s)" by auto
show "fst (rpo_pr n (Fun f ss) s)"
proof (cases s)
case (Fun g ts)
from s rec have "∃ t ∈ set ss. snd (rpo_pr n t s)" by auto
with Fun show ?thesis by auto
next
case (Var x)
from s rec have "∃ t ∈ set ss. snd (rpo_pr n t s)" by auto
with Var show ?thesis by auto
qed
qed
have rec22: "∀ s ∈ set ss. fst (rpo_pr n (Fun f ss) s)"
proof
fix s
assume s: "s ∈ set ss"
with Fun have rec: "snd (rpo_pr n s s)" by auto
show "fst (rpo_pr n (Fun f ss) s)"
proof (cases s)
case (Fun g ts)
from s rec have "∃ t ∈ set ss. snd (rpo_pr n t s)" by auto
with Fun show ?thesis by auto
next
case (Var x)
from s rec have "∃ t ∈ set ss. snd (rpo_pr n t s)" by auto
with Var show ?thesis by auto
qed
qed
from rec11 rec12 rec21 rec22 show ?case by (cases "c (f,length ss)", auto simp: Let_def prc_refl)
qed simp
lemma supt_imp_rpo_stri: assumes "s ⊳ t"
shows "fst (rpo_pr n s t)"
using assms
proof (induct)
case (arg s ss f)
have refl: "snd (rpo_pr n s s)" by (rule rpo_nstri_refl)
from arg refl have fact: "∃ t ∈ set ss. snd (rpo_pr n t s)" by auto
thus ?case
by (cases s, auto)
next
case (subt s ss t f)
from subt rpo_stri_imp_nstri[of "pr" c n s t] have "∃ s ∈ set ss. snd (rpo_pr n s t)" by auto
thus ?case
by (cases t, auto)
qed
lemma supteq_imp_rpo_nstri: assumes supteq: "s ⊵ t" shows "snd (rpo_pr n s t)"
proof -
from supteq have "s = t ∨ s ⊳ t" by auto
thus ?thesis
proof
assume "s = t"
with rpo_nstri_refl show ?thesis by auto
next
assume "s ⊳ t"
from rpo_stri_imp_nstri[OF supt_imp_rpo_stri[OF this]]
show ?thesis .
qed
qed
lemma rpo_nstri_mono: assumes rel: "snd (rpo_pr n s t)"
shows "snd (rpo_pr n (Fun f (bef @ s # aft)) (Fun f (bef @ t # aft)))"
proof -
let ?ss = "bef @ s # aft"
let ?ts = "bef @ t # aft"
let ?s = "Fun f ?ss"
let ?len = "Suc (length bef + length aft)"
have aft_bef: "∀ b ∈ set bef ∪ set aft. fst (rpo_pr n ?s b)"
proof (intro ballI)
fix b
assume elem: "b ∈ set bef ∪ set aft"
show "fst (rpo_pr n ?s b)"
proof (rule supt_imp_rpo_stri, cases "b ∈ set bef")
assume "b ∈ set bef"
thus "?s ⊳ b" by (auto simp: supt.intros)
next
assume bbef: "b ∉ set bef"
show "?s ⊳ b"
proof (cases "b ∈ set aft")
assume "b ∉ set aft"
thus "?s ⊳ b" using bbef elem by blast
qed (auto simp: supt.intros)
qed
qed
from rel have "∃ s ∈ set ?ss. snd (rpo_pr n s t)" by (auto)
hence t: "fst (rpo_pr n ?s t)" by (cases t, auto)
let ?map = "map (λ (s,t). rpo_pr n s t)"
from length_append have sslts: "length ?ss = length ?ts" by simp
have "(mset ?ss, mset ?ts) ∈ ns_mul_ext {(x, y). snd (rpo_pr n x y)}
{(x, y). fst (rpo_pr n x y)}"
proof (rule all_ns_ns_mul_ext)
from sslts show "length ?ss = length ?ts" by assumption
{
fix i assume i_bd: "i < length ?ts"
have "(?ss ! i, ?ts ! i) ∈ {(x, y). snd (rpo_pr n x y)}"
proof (cases "i < length bef")
case True
with append_Cons_nth_left[OF this] and rpo_nstri_refl
show ?thesis by simp
next
case False note Hineq = this
thus ?thesis proof (cases "i - length bef")
case 0
with False have "i = length bef" by simp
with nth_append_length and rel show ?thesis by simp
next
case (Suc j)
from nth_append and False
have "⋀u. (bef @ u # aft) ! i = (u # aft) ! (i - length bef)" by metis
with Suc and rpo_nstri_refl show ?thesis by simp
qed
qed
}
thus "∀i. i < length ?ts ⟶ (?ss ! i, ?ts ! i) ∈ {(x, y). snd (rpo_pr n x y)}" by simp
qed
hence mul_ext: "snd (mul_ext (rpo_pr n) ?ss ?ts)" unfolding mul_ext_def by simp
have lex_ext: "snd (lex_ext (rpo_pr n) n ?ss ?ts)"
proof (rule all_nstri_imp_lex_nstri[of ?ts _ ?ss, simplified], intro allI impI)
fix i
assume i: "i < ?len"
show "snd (rpo_pr n (?ss ! i) (?ts ! i))" (is "?nstri i")
proof (cases "i = length bef")
case True
with rel show "?nstri i" by auto
next
case False
show ?thesis
proof (cases "i < length bef")
case True
with rpo_nstri_refl[of n] show "?nstri i" by (simp add: nth_append)
next
case False
with ‹i ≠ length bef› have "i - length bef > 0" by arith
then obtain j where i: "i - length bef = Suc j" by (cases "i - length bef", auto)
with False rpo_nstri_refl[of n "aft ! j"] show "?nstri i" by (simp add: nth_append)
qed
qed
qed
show ?thesis unfolding rpo.simps Let_def
by (cases "∃ s ∈ set ?ss. snd (rpo_pr n s (Fun f ?ts))",
(cases "c (f,length (bef @ s # aft))",
simp_all add: prc_refl t aft_bef mul_ext lex_ext)+)
qed
lemma rpo_stri_mono:
assumes rel: "fst (rpo_pr n s t)"
shows "fst (rpo_pr n (Fun f (bef @ s # aft)) (Fun f (bef @ t # aft)))"
proof -
let ?ss = "bef @ s # aft"
let ?ts = "bef @ t # aft"
let ?s = "Fun f ?ss"
have aft_bef: "∀ b ∈ set bef ∪ set aft. fst (rpo_pr n ?s b)"
proof (intro ballI)
fix b
assume elem: "b ∈ set bef ∪ set aft"
show "fst (rpo_pr n ?s b)"
proof (rule supt_imp_rpo_stri, cases "b ∈ set bef")
assume "b ∈ set bef"
thus "?s ⊳ b" by (auto simp: supt.intros)
next
assume bbef: "b ∉ set bef"
show "?s ⊳ b"
proof (cases "b ∈ set aft")
assume "b ∉ set aft"
thus "?s ⊳ b" using bbef elem by blast
qed (auto simp: supt.intros)
qed
qed
from rpo_stri_imp_nstri[OF rel] have "∃ s ∈ set ?ss. snd (rpo_pr n s t)" by auto
hence t: "fst (rpo_pr n ?s t)" by (cases t, auto)
let ?map = "map (λ (s,t). rpo_pr n s t)"
obtain stri nstri where st: "rpo_pr n s t = (stri,nstri)" by force
with rel have stri: "stri = True" by simp
let ?ba = "bef @ aft"
have Hrew: "⋀t. remove_nth (length bef) (bef @ t # aft) = ?ba" by (simp add: remove_nth_def)
have bef_bd: "⋀t. length bef < length (bef @ t # aft)" by simp
with rpo_nstri_refl
have "∀i. i < length ?ba ⟶ (?ba ! i, ?ba ! i) ∈ {(x, y). snd (rpo_pr n x y)}"
by auto
from all_ns_ns_mul_ext[OF _ this]
have H: "(mset ?ba, mset ?ba) ∈ ns_mul_ext {(x, y). snd (rpo_pr n x y)} {(x, y). fst (rpo_pr n x y)}"
by metis
from rel have s_s_t: "∀b. b ∈# {#t#} ⟶ (∃a. a ∈# {#s#} ∧ (a,b) ∈ {(x,y). fst (rpo_pr n x y)})" by simp
from remove_nth_soundness[OF bef_bd[of s]] and Hrew and nth_append_length[of bef s aft]
and insert_DiffM2[OF nth_mem_mset[OF bef_bd[of s]]]
have H1: "mset ?ba + {#s#} = mset ?ss" by auto
from remove_nth_soundness[OF bef_bd[of t]] and Hrew and nth_append_length[of bef t aft]
and insert_DiffM2[OF nth_mem_mset[OF bef_bd[of t]]]
have H2: "mset ?ba + {#t#} = mset ?ts" by auto
have "{#s#} ≠ {#}" by simp
from ns_s_mul_ext_union_multiset_l[OF H this s_s_t] and H1 and H2
have "(mset ?ss, mset ?ts)
∈ s_mul_ext {(x, y). snd (rpo_pr n x y)} {(x, y). fst (rpo_pr n x y)}" by simp
hence mul_ext: "fst (mul_ext (rpo_pr n) ?ss ?ts)" unfolding mul_ext_def by simp
{
fix i
assume i: "i < length bef"
hence "snd (rpo_pr n (?ss ! i) (?ts ! i))" by (simp add: rpo_nstri_refl[of n] nth_append)
}
hence lex_ext: "fst (lex_ext (rpo_pr n) n ?ss ?ts)"
by (simp add: lex_ext_iff, intro exI[of _ "length bef"], simp add: st stri)
show ?thesis by (simp only: rpo.simps Let_def,
cases "∃ s ∈ set ?ss. snd (rpo_pr n s (Fun f ?ts))",
simp, simp add: prc_refl t aft_bef mul_ext lex_ext,
cases "c (f, length (bef @ s # aft))", simp_all)
qed
lemma rpo_stable: fixes σ :: "('f,'v)subst"
shows "(fst (rpo_pr n s t) ⟶ fst (rpo_pr n (s ⋅ σ) (t ⋅ σ))) ∧ (snd (rpo_pr n s t) ⟶ snd (rpo_pr n (s ⋅ σ) (t ⋅ σ)))"
(is "?p s t")
proof -
have "pr = pr ⟶ c = c ⟶ ?p s t"
proof (induct rule: rpo.induct[of "λ p d n s t. p = pr ⟶ d = c ⟶ (fst (rpo_pr n s t) ⟶ fst (rpo_pr n (s ⋅ σ) (t ⋅ σ))) ∧ (snd (rpo_pr n s t) ⟶ snd (rpo_pr n (s ⋅ σ) (t ⋅ σ)))"])
case (1 _ _ n x y)
show ?case by (auto simp: rpo_nstri_refl)
next
case (2 _ _ n x g ts)
let ?g = "(g,length ts)"
show ?case
proof -
show ?thesis
proof (cases "σ x")
case (Var y)
show ?thesis by (auto simp: Var)
next
case (Fun f ss)
let ?f = "(f,length ss)"
show ?thesis
proof (cases "ts = [] ∧ prl ?g")
case False thus ?thesis by auto
next
case True
hence ts: "ts = []" and g: "prl ?g" by auto
obtain s ns where "prc ?f ?g = (s,ns)" by force
with prl[OF g, of ?f] have prc: "prc ?f ?g = (s, True)" by auto
from ns_mul_ext_bottom have "snd (mul_ext (rpo_pr n) ss [])" by (simp add: Let_def mul_ext_def)
thus ?thesis using prc by (auto simp: ts Fun prc all_nstri_imp_mul_nstri[of "[]", simplified]
all_nstri_imp_lex_nstri[of "[]", simplified])
qed
qed
qed
next
case (3 p d n f ss y)
{
assume "∃ s ∈ set ss. snd (rpo_pr n s (Var y))" and p: "p = pr" and d: "d = c"
from this obtain s where s: "s ∈ set ss" and "snd (rpo_pr n s (Var y))" by force
with 3 p d have "snd (rpo_pr n (s ⋅ σ) (Var y ⋅ σ))" by auto
with s have "∃ s' ∈ set (map (λ s'. s' ⋅ σ) ss). snd (rpo_pr n s' (Var y ⋅ σ))" by auto
}
thus ?case by (cases "Var y ⋅ σ", auto simp: Let_def)
next
case (4 p d n f ss g ts)
let ?map = "map (λ s'. s' ⋅ σ)"
let ?t = "Fun g ts"
let ?s = "Fun f ss"
let ?f = "(f,length ss)"
let ?g = "(g,length ts)"
let ?ssig = "Fun f ss ⋅ σ"
let ?tsig = "Fun g ts ⋅ σ"
let ?ss = "?map ss"
let ?ts = "?map ts"
show ?case
proof (cases "p = pr")
case True note p = this
show ?thesis
proof (cases "d = c")
case True note d = this
show ?thesis
proof (cases "∃ s ∈ set ss. snd (rpo_pr n s ?t)")
case True
from this obtain s where s: "s ∈ set ss" and "snd (rpo_pr n s ?t)" by auto
with 4 p d have "snd (rpo_pr n (s ⋅ σ) ?tsig)" by auto
with s have "∃ s' ∈ set ?ss. snd (rpo_pr n s' ?tsig)" by auto
thus ?thesis by auto
next
case False
hence not1: "¬ (∃ s ∈ set ss. snd (rpo_pr n s ?t))" by force
show ?thesis
proof (cases "snd (rpo_pr n ?s ?t)")
case False
with rpo_stri_imp_nstri have "¬ (fst (rpo_pr n ?s ?t))" by blast
with False show ?thesis by auto
next
case True note Hsnd = this
with not1 have smallTs: "∀ t ∈ set ts. fst (rpo_pr n ?s t)" by (cases ?thesis, auto)
obtain s ns where prc: "prc ?f ?g = (s,ns)" by force
from True smallTs have ge: "ns = True"
by (cases ?thesis, auto simp: Let_def not1 prc)
note prc = prc[unfolded ge]
have "∀ t ∈ set ts. fst (rpo_pr n ?ssig (t ⋅ σ))"
by (intro ballI, rule 4(2)[THEN mp[OF _ p], THEN mp[OF _ d], THEN conjunct1, THEN mp[OF _ smallTs[THEN bspec]], unfolded p d, OF not1], auto simp: prc)
hence smallTssig: "∀ t ∈ set ?ts. fst (rpo_pr n ?ssig t)" by auto
show ?thesis
proof (cases s)
case True with smallTssig not1 show ?thesis by (auto simp: prc)
next
case False
hence "s = False" by simp
note prc = prc[unfolded this]
show ?thesis
proof (cases "c (f,length ss) = c (g,length ts)")
case False note cfg = this
thus ?thesis
proof (cases "c (f,length ss)")
case Lex note cf = this
with cfg have cg: "c (g,length ts) = Mul" by (cases "c (g,length ts)") simp
{
assume Hfst: "fst (local.rpo_pr n (Fun f ss) (Fun g ts))"
from Hfst and smallTs have ss_ne: "map (λt. t ⋅ σ) ss ≠ []"
by (simp add: cf cg prc not1)
from Hfst and smallTs have ts_e: "map (λt. t ⋅ σ) ts = []"
by (simp add: cf cg prc not1)
from ss_ne and ts_e and prc and cf and cg
have "fst (local.rpo_pr n (Fun f ss ⋅ σ) (Fun g ts ⋅ σ))"
by simp
}
moreover
{
assume Hsnd: "snd (local.rpo_pr n (Fun f ss) (Fun g ts))"
from Hsnd and smallTs have ts_e: "map (λt. t ⋅ σ) ts = []"
by (simp add: cf cg prc not1)
with prc and cf and cg
have "snd (local.rpo_pr n (Fun f ss ⋅ σ) (Fun g ts ⋅ σ))"
by simp
}
ultimately show ?thesis by simp
next
case Mul note cf = this
with cfg have cg: "c (g,length ts) = Lex" by (cases "c (g,length ts)") simp_all
{
assume Hfst: "fst (local.rpo_pr n (Fun f ss) (Fun g ts))"
from Hfst and smallTs have ss_ne: "map (λt. t ⋅ σ) ss ≠ []"
by (simp add: cf cg prc not1)
from Hfst and smallTs have ts_e: "map (λt. t ⋅ σ) ts = []"
by (simp add: cf cg prc not1)
from ss_ne and ts_e and prc and cf and cg
have "fst (local.rpo_pr n (Fun f ss ⋅ σ) (Fun g ts ⋅ σ))"
by simp
}
moreover
{
assume Hsnd: "snd (local.rpo_pr n (Fun f ss) (Fun g ts))"
from Hsnd and smallTs have ts_e: "map (λt. t ⋅ σ) ts = []"
by (simp add: cf cg prc not1)
with prc and cf and cg
have "snd (local.rpo_pr n (Fun f ss ⋅ σ) (Fun g ts ⋅ σ))"
by simp
}
ultimately show ?thesis by simp
qed
next
case True note cfg = this
show ?thesis
proof (cases "c (f,length ss)")
case Mul note cf = this
with cfg have cg: "c (g,length ts) = Mul" by simp
from prc not1 smallTs Hsnd cf cg
have snd_mul: "snd (mul_ext (rpo_pr n) ss ts)" by auto
let ?ind = "λ s t. (fst (rpo_pr n s t) ⟶ fst (rpo_pr n (s ⋅ σ) (t ⋅ σ))) ∧
(snd (rpo_pr n s t) ⟶ snd (rpo_pr n (s ⋅ σ) (t ⋅ σ)))"
have ind: "⋀ s t. s ∈ set ss ⟹ t ∈ set ts ⟹ ?ind s t"
by (rule 4(4)[unfolded p d, OF not1 refl, simplified], auto simp: prc smallTs cf cg)
have snd_mul2: "snd (mul_ext (rpo_pr n) ?ss ?ts)"
by (rule nstri_mul_ext_map, insert snd_mul ind, auto)
have nstri: "snd (rpo_pr n ?ssig ?tsig)"
by (simp add: Let_def prc smallTssig[simplified] snd_mul2 cf cg)
{
assume "fst (rpo_pr n ?s ?t)"
with not1 smallTs prc snd_mul cf cg
have fst_mul: "fst (mul_ext (rpo_pr n) ss ts)" by auto
have fst_mul2: "fst (mul_ext (rpo_pr n) ?ss ?ts)"
by (rule stri_mul_ext_map, insert fst_mul ind, auto)
have "fst (rpo_pr n ?ssig ?tsig)"
by (simp add: Let_def prc smallTssig[simplified] fst_mul2 cf cg)
}
with nstri show ?thesis by simp
next
case Lex note cf = this
with cfg have cg: "c (g,length ts) = Lex" by simp
from prc not1 smallTs Hsnd cf cg
have snd_lex: "snd (lex_ext (rpo_pr n) n ss ts)" by auto
let ?ind = "λ i. (fst (rpo_pr n (ss ! i) (ts ! i)) ⟶ fst (rpo_pr n (ss ! i ⋅ σ)
(ts ! i ⋅ σ))) ∧ (snd (rpo_pr n (ss ! i) (ts ! i)) ⟶ snd (rpo_pr n (ss ! i ⋅ σ)
(ts ! i ⋅ σ)))"
have ind: "⋀ i. ⟦i < length ss; i < length ts⟧ ⟹ ?ind i"
by (rule 4(3)[unfolded p d, OF not1 refl, simplified], auto simp: prc smallTs cf cg)
from snd_lex have eq_small: "length ss = length ts ∨ length ts ≤ n"
by (simp add: lex_ext_iff)
from ind snd_lex have snd_lex2: "snd (lex_ext (rpo_pr n) n ?ss ?ts)"
by (simp add: lex_ext_iff eq_small, auto)
have nstri: "snd (rpo_pr n ?ssig ?tsig)"
by (simp add: Let_def prc snd_lex smallTssig[simplified] snd_lex2 cf cg)
{
assume "fst (rpo_pr n ?s ?t)"
with not1 smallTs prc snd_lex cf cg have "fst (lex_ext (rpo_pr n) n ss ts)" by auto
with ind have fst_lex2: "fst (lex_ext (rpo_pr n) n ?ss ?ts)"
by (simp add: lex_ext_iff eq_small, auto)
have "fst (rpo_pr n ?ssig ?tsig)"
by (simp add: Let_def prc snd_lex smallTssig[simplified] fst_lex2 cf cg)
}
with nstri show ?thesis by simp
qed
qed
qed
qed
qed
qed simp
qed simp
qed
thus ?thesis by simp
qed
lemma rpo_least_1: assumes "prl (f,0)"
shows "snd (rpo_pr n t (Fun f []))"
proof (cases t, simp add: assms)
case (Fun g ts)
let ?g = "(g,length ts)"
obtain s ns where "prc ?g (f,0) = (s,ns)" by force
with prl[OF assms, of ?g] have prc: "prc ?g (f,0) = (s,True)" by auto
show ?thesis
proof (cases "c (f,0)")
case Mul note cf = this
show ?thesis
proof (cases "c (g,length ts)")
case Mul note cg = this
from ns_mul_ext_bottom have H: "snd (mul_ext (rpo_pr n) ts [])" by (simp add: mul_ext_def Let_def)
thus ?thesis by (simp add: assms Fun prc cf cg)
next
case Lex note cg = this show ?thesis by (simp add: assms Fun prc cf cg)
qed
next
case Lex note cf = this
show ?thesis
proof (cases "c (g,length ts)")
case Mul note cg = this show ?thesis by (simp add: assms Fun prc cf cg)
next
case Lex note cg = this show ?thesis unfolding Fun by (simp add: lex_ext_least_1 prc cf cg)
qed
qed
qed
lemma rpo_least_2: assumes "prl (f,0)"
shows "¬ fst (rpo_pr n (Fun f []) t)"
proof (cases t, simp)
case (Fun g ts)
let ?g = "(g,length ts)"
obtain s ns where "prc (f,0) ?g = (s,ns)" by force
with prl2[OF assms, of ?g] have prc: "prc (f,0) ?g = (False,ns)" by auto
show ?thesis
proof (cases "c (f,0)")
case Mul note cf = this
show ?thesis
proof (cases "c (g,length ts)")
case Mul note cg = this
from s_mul_ext_bottom_strict have "¬ fst (mul_ext (rpo_pr n) [] ts)"
by (simp add: mul_ext_def Let_def)
thus ?thesis unfolding Fun by (simp add: Let_def lex_ext_least_2 prc cf cg)
next
case Lex note cg = this show ?thesis by (simp add: Fun cf cg prc)
qed
next
case Lex note cf = this
show ?thesis
proof (cases "c (g,length ts)")
case Mul note cg = this show ?thesis by (simp add: Fun cf cg prc)
next
case Lex note cg = this
show ?thesis unfolding Fun by (simp add: Let_def lex_ext_least_2 prc cf cg)
qed
qed
qed
lemma rpo_least_3: assumes "prl (f,0)"
and "snd (rpo_pr n (Fun f []) t)"
shows "snd (rpo_pr n u t)"
using assms
proof (cases t, simp)
case (Fun g ts)
let ?g = "(g,length ts)"
obtain s ns where "prc (f,0) ?g = (s,ns)" by force
with prl2[OF ‹prl (f,0)›, of ?g] have prc: "prc (f,0) ?g = (False,ns)" by auto
show ?thesis
proof (cases ts)
case Nil
with Fun assms prc have "prc (f,0) ?g = (False,True)" by (cases ?thesis, auto simp: Let_def)
with prl3[OF ‹prl (f,0)›, of ?g] Nil have "prl (g,0)" by auto
show ?thesis unfolding Fun Nil using rpo_least_1[OF ‹prl (g,0)›] .
next
case (Cons s tts)
have "¬ fst (rpo_pr n (Fun f []) s)" by (rule rpo_least_2[OF ‹prl (f,0)›])
with ‹snd (rpo_pr n (Fun f []) t)› Fun Cons have False by (simp add: Let_def)
thus ?thesis ..
qed
qed
lemma rpo_compat[rule_format]:
fixes s t u :: "('f,'v)term"
shows "
(snd (rpo_pr n s t) ∧ fst (rpo_pr n t u) ⟶ fst (rpo_pr n s u)) ∧
(fst (rpo_pr n s t) ∧ snd (rpo_pr n t u) ⟶ fst (rpo_pr n s u)) ∧
(snd (rpo_pr n s t) ∧ snd (rpo_pr n t u) ⟶ snd (rpo_pr n s u))" (is "?tran s t u")
proof (rule
wf_induct[OF wf_measures[of "[λ (s,t,u). size s, λ (s,t,u). size t, λ (s,t,u). size u]"],
of "λ (s,t,u). ?tran s t u" "(s,t,u)", simplified], clarify)
fix s t u :: "('f,'v)term"
assume ind: "∀ s' t' u'. (size s' < size s ⟶ ?tran s' t' u') ∧ (size s' = size s ∧ (size t' < size t ∨ size t' = size t ∧ size u' < size u) ⟶ ?tran s' t' u')"
let ?GR = "λ s t. fst (rpo_pr n s t)"
let ?GE = "λ s t. snd (rpo_pr n s t)"
show "?tran s t u"
proof (cases t)
case (Var x)
{
assume "?GR t u"
with Var have False by (cases u, auto)
}
moreover
{
assume gr: "?GR s t" and ge: "?GE t u"
have "?GR s u"
proof (cases u)
case (Var y)
with ge ‹t = Var x› have "t = u" by auto
with gr show ?thesis by auto
next
case (Fun h us)
with ge Var have us: "us = []" and pri: "prl (h,0)" by auto
from gr Var obtain f ss where s: "s = Fun f ss" by (cases s, auto)
with gr Var obtain s' where s': "s' ∈ set ss" by (auto simp: Let_def)
have "?GE s' u" by (simp only: Fun us, rule rpo_least_1, rule pri)
with s' have "∃ s' ∈ set ss. ?GE s' u" by (auto)
with s Fun show ?thesis by simp
qed
}
moreover
{
assume ge1: "?GE s t" and ge2: "?GE t u"
have "?GE s u"
proof (cases u)
case (Var y)
with ge2 ‹t = Var x› have "t = u" by auto
with ge1 show ?thesis by auto
next
case (Fun h us)
with ge2 Var have us: "us = []" and pri: "prl (h,0)" by auto
show ?thesis by (simp only: Fun us, rule rpo_least_1, rule pri)
qed
}
ultimately show ?thesis by blast
next
case (Fun g ts)
let ?t = "Fun g ts"
from Fun have t: "t = ?t" .
show ?thesis
proof (cases s)
case (Var x)
{
assume gr: "?GR s t"
with Var Fun have False by auto
}
moreover
{
assume ge: "?GE s t" and gr: "?GR t u"
with Var Fun have pri: "prl (g,0)" and "ts = []" by auto
with gr Fun have False using rpo_least_2[of g n u] by auto
}
moreover
{
assume ge1: "?GE s t" and ge2: "?GE t u"
with Var Fun have pri: "prl (g,0)" and empty: "ts = []" by auto
have "?GE s u" by (rule rpo_least_3[of g n u], rule pri, simp add: empty[symmetric] Fun[symmetric], rule ge2)
}
ultimately show ?thesis by blast
next
case (Fun f ss)
let ?s = "Fun f ss"
from Fun have s: "s = ?s" .
let ?s1 = "∃ s' ∈ set ss. ?GE s' t"
let ?t1 = "∃ t' ∈ set ts. ?GE t' u"
let ?ls = "length ss"
let ?lt = "length ts"
let ?f = "(f,?ls)"
let ?g = "(g,?lt)"
obtain ps pns where prc: "prc ?f ?g = (ps,pns)" by force
let ?tran2 = "λ a b c.
(snd (rpo_pr n a b) ∧ fst (rpo_pr n b c) ⟶ fst (rpo_pr n a c)) ∧
(fst (rpo_pr n a b) ∧ snd (rpo_pr n b c) ⟶ fst (rpo_pr n a c)) ∧
(snd (rpo_pr n a b) ∧ snd (rpo_pr n b c) ⟶ snd (rpo_pr n a c)) ∧
(fst (rpo_pr n a b) ∧ fst (rpo_pr n b c) ⟶ fst (rpo_pr n a c))"
from s have "∀ s' ∈ set ss. size s' < size s" by (auto simp: size_simps)
with ind have ind2: "⋀ s' t' u'. ⟦s' ∈ set ss⟧ ⟹ ?tran s' t' u'" by blast
with rpo_stri_imp_nstri have ind3: "⋀ us s' t' u'. ⟦s' ∈ set ss; t' ∈ set ts; u' ∈ set us⟧ ⟹ ?tran2 s' t' u'" by blast
{
assume ge: "?GE s t" and gr: "?GR t u"
have "?GR s u"
proof (cases ?s1)
case True
from this obtain s' where s': "s' ∈ set ss" and ges: "?GE s' t" by auto
with s s' ind2[of s' t u, simplified] ges gr have "?GR s' u" by auto
hence "?GE s' u" by (rule rpo_stri_imp_nstri)
with s' s show ?thesis by (cases u, auto simp: Let_def)
next
case False
show ?thesis
proof (cases ?t1)
case True
from this obtain t' where t': "t' ∈ set ts" and ges: "?GE t' u" by auto
from t' t False ge s have gr2: "?GR s t'" by (cases "∀ t' ∈ set ts. ?GR ?s t'", auto)
from t' s t gr2 ges spec[OF spec[OF spec[OF ind]], of s _ u, simplified] show "?GR s u" using size_simps supt.intros by auto
next
case False
from t this gr obtain h us where u: "u = Fun h us" by (cases u, auto simp: Let_def)
let ?u = "Fun h us"
from s t u ge gr have ge: "?GE ?s ?t" and gr: "?GR ?t ?u" by auto
from ‹¬ ?s1› t ge have st': "∀ t' ∈ set ts. ?GR ?s t'" by (cases ?thesis, auto)
from ‹¬ ?t1› u gr have tu': "∀ u' ∈ set us. ?GR ?t u'" by (cases ?thesis, auto)
let ?lu = "length us"
let ?h = "(h,?lu)"
obtain ps2 pns2 where prc2: "prc ?g ?h = (ps2,pns2)" by force
obtain ps3 pns3 where prc3: "prc ?f ?h = (ps3,pns3)" by force
from ‹¬ ?s1› t ge st' have fg: "pns" by (cases ?thesis, auto simp: Let_def prc)
from ‹¬ ?t1› u gr tu' have gh: "pns2" by (cases ?thesis, auto simp: Let_def prc2)
note compat = prc_compat[OF prc prc2 prc3]
from fg gh compat have fh: "pns3" by simp
from tu' s t ge spec[OF spec[OF ind], of s t, simplified] u
have su': "∀ u' ∈ set us. ?GR ?s u'" using size_simps supt.intros by auto
show ?thesis
proof (cases ps3)
case True
with su' s u fh prc3 show ?thesis by (auto)
next
case False
from False fg gh compat have nfg: "¬ ps" and ngh: "¬ ps2" by blast+
show ?thesis
proof (cases "c ?f")
case Mul note cf = this
show ?thesis
proof (cases "c ?g")
case Mul note cg = this
show ?thesis
proof (cases "c ?h")
case Mul note ch = this
from fg ‹¬ ?s1› t ge st' prc nfg cf cg
have mul1: "snd (mul_ext (rpo_pr n) ss ts)" by auto
from gh ‹¬ ?t1› u gr tu' prc2 ngh cg ch
have mul2: "fst (mul_ext (rpo_pr n) ts us)" by auto
from mul1 mul2 mul_ext_compat[OF ind3, of ss ts us]
have "fst (mul_ext (rpo_pr n) ss us)" by auto
with s u fh su' prc3 cf ch show ?thesis by simp
next
case Lex note ch = this
from gh ‹¬ ?t1› u gr tu' prc2 ngh cg ch have us_e: "us = []" by simp
from gh ‹¬ ?t1› u gr tu' prc2 ngh cg ch have ts_ne: "ts ≠ []" by simp
from ns_mul_ext_bottom_uniqueness[of "mset ts"]
have "⋀f. snd (mul_ext f [] ts) ⟹ ts = []" unfolding mul_ext_def by (simp add: Let_def)
with ts_ne fg ‹¬ ?s1› t ge st' prc nfg cf cg have ss_ne: "ss ≠ []"
by (cases ss) auto
from us_e ss_ne s u fh su' prc3 cf cg ch show ?thesis by simp
qed
next
case Lex note cg = this
from fg ‹¬ ?s1› t ge st' prc nfg cf cg have ts_e: "ts = []" by simp
with gh ‹¬ ?t1› u gr tu' prc2 ngh cg show ?thesis
by (cases "c ?h") (simp_all add: lex_ext_least_2)
qed
next
case Lex note cf = this
show ?thesis
proof (cases "c ?g")
case Mul note cg = this
from fg ‹¬ ?s1› t ge st' prc nfg cf cg have ts_e: "ts = []" by simp
with gh ‹¬ ?t1› u gr tu' prc2 ngh cg show ?thesis
by (cases "c ?h") (auto simp: Let_def s_mul_ext_def s_mul_ext_bottom mul_ext_def elim: mult2_alt_sE)
next
case Lex note cg = this
show ?thesis
proof (cases "c ?h")
case Mul note ch = this
from gh ‹¬ ?t1› u gr tu' prc2 ngh cg ch have us_e: "us = []" by simp
from gh ‹¬ ?t1› u gr tu' prc2 ngh cg ch have ts_ne: "ts ≠ []" by simp
from lex_ext_iff[of _ _ "[]" ts]
have "⋀f. snd (lex_ext f n [] ts) ⟹ ts = []" by simp
with ts_ne fg ‹¬ ?s1› t ge st' prc nfg cf cg have ss_ne: "ss ≠ []"
by (cases ss) auto
from us_e ss_ne s u fh su' prc3 cf cg ch show ?thesis by simp
next
case Lex note ch = this
from fg ‹¬ ?s1› t ge st' prc nfg cf cg
have lex1: "snd (lex_ext (rpo_pr n) n ss ts)" by auto
from gh ‹¬ ?t1› u gr tu' prc2 ngh cg ch
have lex2: "fst (lex_ext (rpo_pr n) n ts us)" by auto
from lex1 lex2 lex_ext_compat[OF ind3, of ss ts us]
have "fst (lex_ext (rpo_pr n) n ss us)" by auto
with s u fh su' prc3 cf cg ch show ?thesis by simp
qed
qed
qed
qed
qed
qed
}
moreover
{
assume gr: "?GR s t" and ge: "?GE t u"
have "?GR s u"
proof (cases ?s1)
case True
from this obtain s' where s': "s' ∈ set ss" and ges: "?GE s' t" by auto
with s s' ind2[of s' t u, simplified] ges ge have "?GE s' u" by auto
with s' s show ?thesis by (cases u, auto simp: Let_def)
next
case False
show ?thesis
proof (cases ?t1)
case True
from this obtain t' where t': "t' ∈ set ts" and ges: "?GE t' u" by auto
have tt': "?GE t t'" by (rule rpo_stri_imp_nstri[OF supt_imp_rpo_stri],
auto simp: t t' supt.intros)
from t' t False gr s have gr2: "?GR s t'" by (cases "∀ t' ∈ set ts. ?GR ?s t'", auto)
from t' s t gr2 ges spec[OF spec[OF spec[OF ind]], of s _ u, simplified]
show "?GR s u" using size_simps by auto
next
case False
from t this ge obtain h us where u: "u = Fun h us" by (cases u, auto simp: Let_def)
let ?u = "Fun h us"
from s t u ge gr have gr: "?GR ?s ?t" and ge: "?GE ?t ?u" by auto
from ‹¬ ?s1› t gr have st': "∀ t' ∈ set ts. ?GR ?s t'" by (cases ?thesis, auto)
from ‹¬ ?t1› u ge have tu': "∀ u' ∈ set us. ?GR ?t u'" by (cases ?thesis, auto)
let ?lu = "length us"
let ?h = "(h,?lu)"
obtain ps2 pns2 where prc2: "prc ?g ?h = (ps2,pns2)" by force
obtain ps3 pns3 where prc3: "prc ?f ?h = (ps3,pns3)" by force
from ‹¬ ?s1› t gr st' have fg: "pns" by (cases ?thesis, auto simp: Let_def prc)
from ‹¬ ?t1› u ge tu' have gh: "pns2" by (cases ?thesis, auto simp: Let_def prc2)
note compat = prc_compat[OF prc prc2 prc3]
from fg gh compat have fh: "pns3" by simp
from tu' s t rpo_stri_imp_nstri[OF gr] spec[OF spec[OF ind], of s t,
simplified] u have su': "∀ u' ∈ set us. ?GR ?s u'" using size_simps by auto
show ?thesis
proof (cases ps3)
case True
with su' s u fh prc3 show ?thesis by (auto)
next
case False
from False fg gh compat have nfg: "¬ ps" and ngh: "¬ ps2" by blast+
show ?thesis
proof (cases "c ?f")
case Mul note cf = this
show ?thesis
proof (cases "c ?g")
case Mul note cg = this
show ?thesis
proof (cases "c ?h")
case Mul note ch = this
from fg ‹¬ ?s1› t gr st' prc nfg cf cg
have mul1: "fst (mul_ext (rpo_pr n) ss ts)" by auto
from gh ‹¬ ?t1› u ge tu' prc2 ngh cg ch
have mul2: "snd (mul_ext (rpo_pr n) ts us)" by auto
from mul1 mul2 mul_ext_compat[OF ind3, of ss ts us]
have "fst (mul_ext (rpo_pr n) ss us)" by auto
with s u fh su' prc3 cf ch show ?thesis by simp
next
case Lex note ch = this
from gh ‹¬ ?t1› u ge tu' prc2 ngh cg ch have us_e: "us = []" by simp
from fg ‹¬ ?s1› t gr st' prc nfg cf cg s_mul_ext_bottom_strict
have ss_ne: "ss ≠ []" by (cases ss) (auto simp: Let_def mul_ext_def)
from us_e ss_ne s u fh su' prc3 cf cg ch show ?thesis by simp
qed
next
case Lex note cg = this
from fg ‹¬ ?s1› t gr st' prc nfg cf cg s_mul_ext_bottom_strict
have ss_ne: "ss ≠ []" by (cases ss) (auto simp: mul_ext_def)
from fg ‹¬ ?s1› t gr st' prc nfg cf cg have ts_e: "ts = []" by simp
show ?thesis
proof (cases "c ?h")
case Mul note ch = this
with gh ‹¬ ?t1› u ge tu' prc2 ngh cg ch ns_mul_ext_bottom_uniqueness
have "us = []" by simp
with ss_ne s u fh su' prc3 cf cg ch s_mul_ext_bottom
show ?thesis by (simp add: Let_def mul_ext_def s_mul_ext_def mult2_alt_s_def)
next
case Lex note ch = this
from lex_ext_iff[of _ _ "[]" us]
have "⋀f. snd (lex_ext f n [] us) ⟹ us = []" by simp
with ts_e gh ‹¬ ?t1› u ge tu' prc2 ngh cg ch
have "us = []" by simp
with ss_ne s u fh su' prc3 cf cg ch s_mul_ext_bottom
show ?thesis by (simp add: mul_ext_def)
qed
qed
next
case Lex note cf = this
show ?thesis
proof (cases "c ?g")
case Mul note cg = this
from fg ‹¬ ?s1› t gr st' prc nfg cf cg have ss_ne: "ss ≠ []" by simp
from fg ‹¬ ?s1› t gr st' prc nfg cf cg have ts_e: "ts = []" by simp
show ?thesis
proof (cases "c ?h")
case Mul note ch = this
from ts_e gh ‹¬ ?t1› u ge tu' prc2 ngh cg ch
ns_mul_ext_bottom_uniqueness[of "mset us"]
have "us = []" by (simp add: mul_ext_def Let_def)
with ss_ne s u fh su' prc3 cf cg ch s_mul_ext_bottom
show ?thesis by (simp add: mul_ext_def)
next
case Lex note ch = this
from gh ‹¬ ?t1› u ge tu' prc2 ngh cg ch have "us = []" by simp
with ss_ne s u fh su' prc3 cf cg ch
show ?thesis by (simp add: lex_ext_iff)
qed
next
case Lex note cg = this
show ?thesis
proof (cases "c ?h")
case Mul note ch = this
from gh ‹¬ ?t1› u ge tu' prc2 ngh cg ch have us_e: "us = []" by simp
have "⋀f. fst (lex_ext f n ss ts) ⟹ ss ≠ []"
by (cases ss) (simp_all add: lex_ext_iff)
with fg ‹¬ ?s1› t gr st' prc nfg cf cg have ss_ne: "ss ≠ []" by simp
with us_e s u fh su' prc3 cf cg ch show ?thesis by simp
next
case Lex note ch = this
from fg ‹¬ ?s1› t gr st' prc nfg cf cg
have lex1: "fst (lex_ext (rpo_pr n) n ss ts)" by auto
from gh ‹¬ ?t1› u ge tu' prc2 ngh cg ch
have lex2: "snd (lex_ext (rpo_pr n) n ts us)" by auto
from lex1 lex2 lex_ext_compat[OF ind3, of ss ts us]
have "fst (lex_ext (rpo_pr n) n ss us)" by auto
with s u fh su' prc3 cf cg ch show ?thesis by auto
qed
qed
qed
qed
qed
qed
}
moreover
{
assume ge1: "?GE s t" and ge2: "?GE t u" and ngt1: "¬ ?GR s t" and ngt2: "¬ ?GR t u"
have "¬ ?s1"
proof
assume ?s1
with s have "?GR s t" by (cases t, auto)
with ngt1 show False ..
qed
have "¬ ?t1"
proof
assume ?t1
with t have "?GR t u" by (cases u, auto)
with ngt2 show False ..
qed
from t ‹¬ ?t1› ge2 obtain h us where u: "u = Fun h us" by (cases u, auto simp: Let_def)
let ?u = "Fun h us"
from s t u ge1 ge2 have ge1: "?GE ?s ?t" and ge2: "?GE ?t ?u" by auto
from ‹¬ ?s1› t ge1 have st': "∀ t' ∈ set ts. ?GR ?s t'" by (cases ?thesis, auto)
from ‹¬ ?t1› u ge2 have tu': "∀ u' ∈ set us. ?GR ?t u'" by (cases ?thesis, auto)
let ?lu = "length us"
let ?h = "(h,?lu)"
obtain ps2 pns2 where prc2: "prc ?g ?h = (ps2,pns2)" by force
obtain ps3 pns3 where prc3: "prc ?f ?h = (ps3,pns3)" by force
from ‹¬ ?s1› t ge1 st' have fg: "pns" by (cases ?thesis, auto simp: Let_def prc)
from ‹¬ ?t1› u ge2 tu' have gh: "pns2" by (cases ?thesis, auto simp: Let_def prc2)
note compat = prc_compat[OF prc prc2 prc3]
from compat fg gh have fh: pns3 by blast
from tu' s t ge1 spec[OF spec[OF ind], of s t, simplified] u
have su': "∀ u' ∈ set us. ?GR ?s u'" using size_simps by auto
from ‹¬ ?s1› st' ge1 ngt1 s t have nfg: "¬ ps"
by (simp add: Let_def, cases ?thesis, simp, cases ps, auto simp: prc fg)
from ‹¬ ?t1› tu' ge2 ngt2 t u have ngh: "¬ ps2"
by (simp add: Let_def, cases ?thesis, simp, cases ps2, auto simp: prc2 gh)
have "?GE s u"
proof (cases "c ?f")
case Mul note cf = this
show ?thesis
proof (cases "c ?g")
case Mul note cg = this
show ?thesis
proof (cases "c ?h")
case Mul note ch = this
from fg ‹¬ ?s1› t ge1 st' prc nfg cf cg
have mul1: "snd (mul_ext (rpo_pr n) ss ts)" by auto
from gh ‹¬ ?t1› u ge2 tu' prc2 ngh cg ch
have mul2: "snd (mul_ext (rpo_pr n) ts us)" by auto
from mul1 mul2 mul_ext_compat[OF ind3, of ss ts us]
have "snd (mul_ext (rpo_pr n) ss us)" by auto
with s u fh su' prc3 cf ch show ?thesis by simp
next
case Lex note ch = this
from gh ‹¬ ?t1› u ge2 tu' prc2 ngh cg ch have us_e: "us = []" by simp
with s u fh su' prc3 cf cg ch show ?thesis by simp
qed
next
case Lex note cg = this
from fg ‹¬ ?s1› t ge1 st' prc nfg cf cg have ts_e: "ts = []" by simp
show ?thesis
proof (cases "c ?h")
case Mul note ch = this
with gh ‹¬ ?t1› u ge2 tu' prc2 ngh cg ch have "us = []" by simp
with s u fh su' prc3 cf cg ch ns_mul_ext_bottom
show ?thesis by (simp add: ns_mul_ext_def mul_ext_def Let_def mult2_alt_ns_def)
next
case Lex note ch = this
have "⋀f. snd (lex_ext f n [] us) ⟹ us = []" by (simp_all add: lex_ext_iff)
with ts_e gh ‹¬ ?t1› u ge2 tu' prc2 ngh cg ch have "us = []" by simp
with s u fh su' prc3 cf cg ch show ?thesis by simp
qed
qed
next
case Lex note cf = this
show ?thesis
proof (cases "c ?g")
case Mul note cg = this
from fg ‹¬ ?s1› t ge1 st' prc nfg cf cg have ts_e: "ts = []" by simp
show ?thesis
proof (cases "c ?h")
case Mul note ch = this
with ts_e gh ‹¬ ?t1› u ge2 tu' prc2 ngh cg ch
ns_mul_ext_bottom_uniqueness[of "mset us"]
have "us = []" by (simp add: Let_def mul_ext_def)
with s u fh su' prc3 cf cg ch show ?thesis by simp
next
case Lex note ch = this
with gh ‹¬ ?t1› u ge2 tu' prc2 ngh cg ch have "us = []" by simp
with s u fh su' prc3 cf cg ch show ?thesis by (simp add: lex_ext_least_1)
qed
next
case Lex note cg = this
show ?thesis
proof (cases "c ?h")
case Mul note ch = this
with gh ‹¬ ?t1› u ge2 tu' prc2 ngh cg ch have "us = []" by simp
with s u fh su' prc3 cf cg ch show ?thesis by (simp add: lex_ext_least_1)
next
case Lex note ch = this
from ‹¬ ?s1› st' ge1 s t fg nfg cf cg
have lex1: "snd (lex_ext (rpo_pr n) n ss ts)" by (auto simp: prc)
from ‹¬ ?t1› tu' ge2 t u gh ngh cg ch
have lex2: "snd (lex_ext (rpo_pr n) n ts us)" by (auto simp: prc2)
from lex1 lex2 lex_ext_compat[OF ind3, of ss ts us]
have "snd (lex_ext (rpo_pr n) n ss us)" by auto
with fg gh su' s u fh cf cg ch show ?thesis by (auto simp: prc3)
qed
qed
qed
}
ultimately
show ?thesis using rpo_stri_imp_nstri[of "pr" c n s u] by auto
qed
qed
qed
lemma rpo_trans:
assumes one: "fst (rpo_pr n s t)"
and two: "fst (rpo_pr n t u)"
shows "fst (rpo_pr n s u)"
using assms rpo_compat rpo_stri_imp_nstri[OF one] by blast
lemma rpo_large_sym:
assumes prec: "⋀ g. g ∈ funas_term t ⟹ prc (f,length ss) g = (True,True)"
and vars: "vars_term t ⊆ vars_term (Fun f ss)"
shows "rpo_pr n (Fun f ss) t = (True,True)"
using assms
proof (induct t)
case (Var x)
hence "x ∈ vars_term (Fun f ss)" by simp
from supteq_Var[OF this]
have"Fun f ss ⊳ Var x" unfolding subterm.le_less by simp
from supt_imp_rpo_stri[OF this] have "fst (rpo_pr n (Fun f ss) (Var x))" .
with rpo_stri_imp_nstri[OF this] show ?case by (cases "rpo_pr n (Fun f ss) (Var x)", auto)
next
case (Fun g ts)
from Fun(2) have prec: "prc (f,length ss) (g,length ts) = (True,True)" by simp
{
fix t
assume t: "t ∈ set ts"
from t Fun(3) have v: "vars_term t ⊆ vars_term (Fun f ss)" by auto
from t Fun(2) have p: "⋀ g . g ∈ funas_term t ⟹ prc (f,length ss) g = (True,True)"
by auto
from Fun(1)[OF t p v] have "rpo_pr n (Fun f ss) t = (True,True)" .
}
thus ?case
by (simp add: prec)
qed
context
fixes F :: "('f × nat) set"
assumes pr_gtotal: "⋀f g. f ∈ F ⟹ g ∈ F ⟹ f = g ∨ fst (prc f g) ∨ fst (prc g f)"
and lpo: "⋀ f. f ∈ F ⟹ c f = Lex"
begin
lemma lpo_ground_total:
assumes "funas_term s ⊆ F" and "ground s" and "funas_term t ⊆ F" and "ground t"
shows "s = t ∨ fst (rpo_pr n s t) ∨ fst (rpo_pr n t s)"
using assms
proof (induct "size s + size t" arbitrary: s t rule: nat_less_induct)
case (1 s t)
note IH = 1(1)[rule_format, OF _ refl]
note gs = 1(2-3)
note gt = 1(4-5)
from 1 obtain f ss where s: "s = Fun f ss" by (cases s, auto)
from 1 obtain g ts where t: "t = Fun g ts" by (cases t, auto)
let ?f = "(f,length ss)"
let ?g = "(g,length ts)"
let ?s = "Fun f ss"
let ?t = "Fun g ts"
let ?S = "λ s t. fst (rpo_pr n s t)"
let ?NS = "λ s t. snd (rpo_pr n s t)"
{
assume contra: "¬ ?case"
{
fix si
assume si: "si ∈ set ss"
from si gs have gsi: "funas_term si ⊆ F" "ground si" unfolding s by auto
from si have "size si + size t < size s + size t" unfolding s by (auto simp: size_simps)
from IH[OF this gsi gt] have "(si = t ∨ ?S si t) ∨ ?S t si" by simp
hence "?S t si"
proof
assume "si = t ∨ ?S si t"
hence "?NS si t" using rpo_nstri_refl rpo_stri_imp_nstri by blast
moreover have "?S s si" using supt_imp_rpo_stri[of s si n] unfolding s using si by auto
ultimately have "?S s t" using rpo_compat by auto
with contra show "?S t si" by simp
qed simp
}
hence tsi: "(∀ si ∈ set ss. ?S ?t si) = True" unfolding t by auto
{
fix ti
assume ti: "ti ∈ set ts"
from ti gt have gti: "funas_term ti ⊆ F" "ground ti" unfolding t by auto
from ti have "size s + size ti < size s + size t" unfolding t by (auto simp: size_simps)
from IH[OF this gs gti] have "(ti = s ∨ ?S ti s) ∨ ?S s ti" by auto
hence "?S s ti"
proof
assume "ti = s ∨ ?S ti s"
hence "?NS ti s" using rpo_nstri_refl rpo_stri_imp_nstri by blast
moreover have "?S t ti" using supt_imp_rpo_stri[of t ti n] unfolding t using ti by auto
ultimately have "?S t s" using rpo_compat by auto
with contra show "?S s ti" by simp
qed simp
}
hence sti: "(∀ ti ∈ set ts. ?S ?s ti) = True" unfolding s by auto
from gs gt have f: "?f ∈ F" and g: "?g ∈ F" unfolding s t by auto
note lpo = lpo[OF f] lpo[OF g]
note contra = contra[unfolded s t rpo.simps tsi sti fst_conv lpo, simplified]
from pr_gtotal[OF f g] contra prc_stri_imp_nstri[of ?f ?g] prc_stri_imp_nstri[of ?g ?f]
have fg: "?f = ?g"
by (cases "prc ?f ?g", cases "prc ?g ?f", auto split: prod.splits if_splits)
hence fg': "f = g" "length ss = length ts" by auto
note contra = contra[unfolded fg' prc_refl Let_def split]
{
fix si ti
assume "(si, ti) ∈ set (zip ss ts)"
from in_set_zipE[OF this]
have si: "si ∈ set ss" and ti: "ti ∈ set ts" by auto
hence "size si + size ti < size si + size t" unfolding s t by (auto simp: size_simps)
also have "… < size s + size t" unfolding s t using si by (auto simp: size_simps)
finally have size: "size si + size ti < size s + size t" by simp
from ti gt have gti: "funas_term ti ⊆ F" "ground ti" unfolding t by auto
from si gs have gsi: "funas_term si ⊆ F" "ground si" unfolding s by auto
from IH[OF size gsi gti]
have "si = ti ∨ ?S si ti ∨ ?S ti si" .
}
hence IH: "(∀(s, t)∈set (zip ss ts). s = t ∨ ?S s t ∨ ?S t s)" by auto
from contra have "¬ fst (lex_ext (rpo_pr n) n ss ts)"
"¬ fst (lex_ext (rpo_pr n) n ts ss)" by (auto split: if_splits)
with lex_ext_total[of ss ts "rpo_pr n" n, OF IH rpo_nstri_refl fg'(2)]
have "ss = ts" by auto
with fg contra have False by auto
}
thus ?case by blast
qed
end
definition RPO_S_pr where "RPO_S_pr n = {(s,t) . fst (rpo_pr n s t)}"
definition RPO_NS_pr where "RPO_NS_pr n = {(s,t). snd (rpo_pr n s t)}"
lemma RPO_NS_subt: assumes st: "s ⊵ t"
shows "(s,t) ∈ RPO_NS_pr n"
using supteq_imp_rpo_nstri[OF st]
unfolding RPO_NS_pr_def by blast
lemma RPO_subt: "s ∈ set ss ⟹ (s,t) ∈ RPO_NS_pr n ⟹ (Fun f ss,t) ∈ RPO_S_pr n"
unfolding RPO_S_pr_def RPO_NS_pr_def by (cases t, auto simp: Let_def)
lemma RPO_prec: "⟦⋀ t. t ∈ set ts ⟹ (Fun f ss, t) ∈ RPO_S_pr n⟧ ⟹
fst (prc (f,length ss) (g,length ts)) ⟹ (Fun f ss, Fun g ts) ∈ RPO_S_pr n"
unfolding RPO_S_pr_def
using prc_stri_imp_nstri[of "(f,length ss)" "(g,length ts)"]
by (cases "prc (f,length ss) (g,length ts)", auto)
lemma RPO_refl: "(s,s) ∈ RPO_NS_pr n"
unfolding RPO_NS_pr_def
by (simp add: rpo_nstri_refl)
lemma RPO_stri: "(s,t) ∈ RPO_S_pr n ⟹ (s,t) ∈ RPO_NS_pr n"
unfolding RPO_S_pr_def RPO_NS_pr_def
using rpo_stri_imp_nstri by auto
lemma RPO_least_Var: "prl (g,0) ⟹ (Var x,Fun g []) ∈ RPO_NS_pr n"
unfolding RPO_NS_pr_def
using rpo_least_1 by blast
lemma RPO_least_Fun: "prl (g,0) ⟹ (Fun f ss,Fun g []) ∈ RPO_NS_pr n"
unfolding RPO_NS_pr_def
using rpo_least_1 by blast
lemma RPO_S_least_Fun: "prl (g,0) ⟹ ss ≠ [] ⟹ (Fun f ss, Fun g []) ∈ RPO_S_pr n"
by (rule RPO_subt[where s = "hd ss"], simp, unfold RPO_NS_pr_def,
insert rpo_least_1, blast)
lemma RPO_S_mul: assumes ms: "(mset ss, mset ts) ∈ s_mul_ext (RPO_NS_pr n) (RPO_S_pr n)"
and prc: "snd (prc (f,length ss) (g,length ts))"
and fmul: "c (f,length ss) = Mul"
and gmul: "c (g,length ts) = Mul"
shows "(Fun f ss, Fun g ts) ∈ RPO_S_pr n"
unfolding RPO_S_pr_def
proof (rule, unfold split)
let ?n = "length ss"
let ?m = "length ts"
let ?f = "(f,?n)"
let ?g = "(g,?m)"
from prc obtain b where prc: "prc ?f ?g = (b,True)" by (cases "prc ?f ?g", auto)
from ms have ms': "fst (mul_ext (rpo_pr n) ss ts)"
unfolding mul_ext_def Let_def RPO_NS_pr_def RPO_S_pr_def by simp
from ms
obtain as bs A' B' where
id: "mset ss = mset as + A'"
"mset ts = mset bs + B'"
and len: "length as = length bs"
and as: "⋀ i. i < length bs ⟹ (as ! i, bs ! i) ∈ RPO_NS_pr n"
and A': "⋀ b. b ∈# B' ⟹ ∃ a. a ∈# A' ∧ (a,b) ∈ RPO_S_pr n"
by (auto simp: s_mul_ext_def mult2_alt_s_def elim: multpw_listE)
{
fix t
assume "t ∈ set ts"
hence "t ∈# mset ts" unfolding in_multiset_in_set .
hence "t ∈# mset bs ∨ t ∈# B'" unfolding id by simp
hence "∃ s. s ∈# mset as + A' ∧ (s,t) ∈ RPO_NS_pr n"
proof
assume "t ∈# B'"
from A'[OF this] obtain s where A': "s ∈# A'" and S: "(s,t) ∈ RPO_S_pr n"
by blast
from RPO_stri[OF S] A' show ?thesis by auto
next
assume "t ∈# mset bs"
hence "t ∈ set bs" unfolding in_multiset_in_set .
from this[unfolded set_conv_nth] obtain i where t: "t = bs ! i"
and i: "i < length bs" by auto
from as[OF i] have NS: "(as ! i, t) ∈ RPO_NS_pr n" unfolding t .
from i len have "as ! i ∈# mset as"
unfolding in_multiset_in_set set_conv_nth by auto
with NS show ?thesis by auto
qed
then obtain s where s: "s ∈ set ss" and NS: "(s,t) ∈ RPO_NS_pr n"
unfolding in_multiset_in_set id[symmetric] by blast
from RPO_subt[OF this] have "(Fun f ss, t) ∈ RPO_S_pr n" .
}
thus "fst (rpo_pr n (Fun f ss) (Fun g ts))"
unfolding RPO_S_pr_def
by (auto simp: fmul gmul prc ms')
qed
lemma RPO_NS_mul: assumes ms: "(mset ss, mset ts) ∈ ns_mul_ext (RPO_NS_pr n) (RPO_S_pr n)"
and prc: "snd (prc (f,length ss) (g,length ts))"
and fmul: "c (f,length ss) = Mul"
and gmul: "c (g,length ts) = Mul"
shows "(Fun f ss, Fun g ts) ∈ RPO_NS_pr n"
unfolding RPO_NS_pr_def
proof (rule, unfold split)
let ?n = "length ss"
let ?m = "length ts"
let ?f = "(f,?n)"
let ?g = "(g,?m)"
from prc obtain b where prc: "prc ?f ?g = (b,True)" by (cases "prc ?f ?g", auto)
from ms have ms': "snd (mul_ext (rpo_pr n) ss ts)"
unfolding mul_ext_def Let_def RPO_NS_pr_def RPO_S_pr_def by simp
from ms
obtain as bs A' B' where
id: "mset ss = mset as + A'"
"mset ts = mset bs + B'"
and len: "length as = length bs"
and as: "⋀ i. i < length bs ⟹ (as ! i, bs ! i) ∈ RPO_NS_pr n"
and A': "⋀ b. b ∈# B' ⟹ ∃ a. a ∈# A' ∧ (a,b) ∈ RPO_S_pr n"
by (auto simp: ns_mul_ext_def mult2_alt_ns_def elim: multpw_listE)
{
fix t
assume "t ∈ set ts"
hence "t ∈# mset ts" unfolding in_multiset_in_set .
hence "t ∈# mset bs ∨ t ∈# B'" unfolding id by simp
hence "∃ s. s ∈# mset as + A' ∧ (s,t) ∈ RPO_NS_pr n"
proof
assume "t ∈# B'"
from A'[OF this] obtain s where A': "s ∈# A'" and S: "(s,t) ∈ RPO_S_pr n"
by blast
from RPO_stri[OF S] A' show ?thesis by auto
next
assume "t ∈# mset bs"
hence "t ∈ set bs" unfolding in_multiset_in_set .
from this[unfolded set_conv_nth] obtain i where t: "t = bs ! i"
and i: "i < length bs" by auto
from as[OF i] have NS: "(as ! i, t) ∈ RPO_NS_pr n" unfolding t .
from i len have "as ! i ∈# mset as"
unfolding in_multiset_in_set set_conv_nth by auto
with NS show ?thesis by auto
qed
then obtain s where s: "s ∈ set ss" and NS: "(s,t) ∈ RPO_NS_pr n"
unfolding in_multiset_in_set id[symmetric] by blast
from RPO_subt[OF this] have "(Fun f ss, t) ∈ RPO_S_pr n" .
}
thus "snd (rpo_pr n (Fun f ss) (Fun g ts))"
unfolding RPO_S_pr_def
by (auto simp: fmul gmul prc ms')
qed
lemma RPO_lex:
defines lexext: "lexext n ≡ lex_ext (λ a b. ((a,b) ∈ RPO_S_pr n,(a,b) ∈ RPO_NS_pr n)) n"
assumes lex: "fst (lexext n ss ts)"
and prc: "snd (prc (f,length ss) (g,length ts))"
and ts: "⋀ t. t ∈ set ts ⟹ (Fun f ss,t) ∈ RPO_S_pr n"
and fmul: "c (f,length ss) = Lex"
and gmul: "c (g,length ts) = Lex"
shows "(Fun f ss, Fun g ts) ∈ RPO_S_pr n"
unfolding RPO_S_pr_def
proof (rule, unfold split)
let ?n = "length ss"
let ?m = "length ts"
let ?f = "(f,?n)"
let ?g = "(g,?m)"
from prc obtain b where prc: "prc ?f ?g = (b,True)" by (cases "prc ?f ?g", auto)
note lex = lex[unfolded lexext RPO_NS_pr_def RPO_S_pr_def]
with ts[unfolded RPO_S_pr_def]
show "fst (rpo_pr n (Fun f ss) (Fun g ts))"
unfolding RPO_S_pr_def
by (auto simp: fmul gmul prc)
qed
lemma RPO_NS_lex:
defines lexext: "lexext n ≡ lex_ext (λ a b. ((a,b) ∈ RPO_S_pr n,(a,b) ∈ RPO_NS_pr n)) n"
assumes lex: "snd (lexext n ss ts)"
and prc: "snd (prc (f,length ss) (g,length ts))"
and ts: "⋀ t. t ∈ set ts ⟹ (Fun f ss,t) ∈ RPO_S_pr n"
and fmul: "c (f,length ss) = Lex"
and gmul: "c (g,length ts) = Lex"
shows "(Fun f ss, Fun g ts) ∈ RPO_NS_pr n"
unfolding RPO_NS_pr_def
proof (rule, unfold split)
let ?n = "length ss"
let ?m = "length ts"
let ?f = "(f,?n)"
let ?g = "(g,?m)"
from prc obtain b where prc: "prc ?f ?g = (b,True)" by (cases "prc ?f ?g", auto)
note lex = lex[unfolded lexext RPO_NS_pr_def RPO_S_pr_def]
with ts[unfolded RPO_S_pr_def]
show "snd (rpo_pr n (Fun f ss) (Fun g ts))"
unfolding RPO_S_pr_def
by (auto simp: fmul gmul prc)
qed
lemma RPO_NS_refl: "refl (RPO_NS_pr n)"
unfolding refl_on_def RPO_NS_pr_def
by (simp add: rpo_nstri_refl)
lemma RPO_NS_trans: "trans (RPO_NS_pr n)"
unfolding trans_def RPO_NS_pr_def
using rpo_compat by blast
lemma RPO_S_trans: "trans (RPO_S_pr n)"
unfolding trans_def RPO_S_pr_def
using rpo_trans by blast
lemma RPO_compat: "RPO_NS_pr n O RPO_S_pr n ⊆ RPO_S_pr n"
using rpo_compat[of n]
by (unfold RPO_S_pr_def RPO_NS_pr_def, auto)
lemma RPO_S_SN: "SN (RPO_S_pr m :: ('f,'v)term rel)"
unfolding RPO_S_pr_def
proof - {
fix t :: "('f,'v)term"
let ?Rp = "λ s t. fst (rpo_pr m s t)"
let ?R = "{(s,t). ?Rp s t}"
let ?S = "λx. SN_on ?R {x}"
note iff = SN_on_all_reducts_SN_on_conv[of ?R]
{
fix x
have "?S (Var x)" unfolding iff[of "Var x"]
proof (intro allI impI)
fix s
assume "(Var x, s) ∈ ?R"
hence False by (cases s, auto)
thus "?S s" ..
qed
} note var_SN = this
have "?S t"
proof (induct t)
case (Var x) show ?case by (rule var_SN)
next
case (Fun f ts)
let ?Slist = "λ ys. ∀ y ∈ set ys. ?S y"
let ?r3 = "{((f,ab), (g,ab')). ((c f = c g) ⟶ (?Slist ab ∧
(c f = Mul ⟶ fst (mul_ext (rpo_pr m) ab ab')) ∧
(c f = Lex ⟶ fst (lex_ext (rpo_pr m) m ab ab'))))
∧ ((c f ≠ c g) ⟶ (ab ≠ [] ∧ ab' = []))}"
let ?r0 = "lex_two {(f,g). fst (prc f g)} {(f,g). snd (prc f g)} ?r3"
let ?ge = "λ t s. snd (rpo_pr m t s)"
let ?gr = ?Rp
{
fix ab
{
assume "∃S. S 0 = ab ∧ (∀i. (S i, S (Suc i)) ∈ ?r3)"
then obtain S where
S0: "S 0 = ab" and
SS: "∀i. (S i, S (Suc i)) ∈ ?r3"
by auto
let ?Sf = "λi. fst (S i)"
let ?Sn = "λi. snd (fst (S i))"
let ?Sts = "λi. snd (S i)"
have False
proof (cases "∀i. c (?Sf i) = Mul")
case True
let ?r' = "{(ys, xs).
(∀y∈set ys. SN_on {(s, t). fst (local.rpo_pr m s t)} {y})
∧ fst (mul_ext (rpo_pr m) ys xs)}"
{
fix i
from True[rule_format, of i] and True[rule_format, of "Suc i"]
and SS[rule_format, of i]
have "(snd (S i), (snd (S (Suc i)))) ∈ ?r'" by auto
}
hence Hf: "¬ SN_on ?r' {snd (S 0)}"
unfolding SN_on_def by auto
from mul_ext_SN[of "rpo_pr m", rule_format, OF rpo_nstri_refl]
and rpo_compat[of m] and rpo_stri_imp_nstri[of "pr" c m]
have "SN ?r'" by blast
from SN_on_subset2[OF subset_UNIV[of "{snd (S 0)}"], OF this]
have "SN_on ?r' {snd (S 0)}" .
with Hf show ?thesis ..
next
case False note HMul = this
show ?thesis
proof (cases "∀i. c (?Sf i) = Lex")
case True
let ?r' = "{(ys, xs).
(∀y∈set ys. SN_on {(s, t). fst (local.rpo_pr m s t)} {y})
∧ fst (lex_ext (rpo_pr m) m ys xs)}"
{
fix i
from True[rule_format, of i] and True[rule_format, of "Suc i"]
and SS[rule_format, of i]
have "(snd (S i), (snd (S (Suc i)))) ∈ ?r'" by auto
}
hence Hf: "¬ SN_on ?r' {snd (S 0)}"
unfolding SN_on_def by auto
from lex_ext_SN[of "rpo_pr m" m] and rpo_stri_imp_nstri and rpo_compat[of m]
have "SN ?r'" by blast
from SN_on_subset2[OF subset_UNIV[of "{snd (S 0)}"] this]
have "SN_on ?r' {snd (S 0)}" .
with Hf show ?thesis ..
next
case False note HLex = this
from HMul and HLex
have "∃i. c (?Sf i)
≠ c (?Sf (Suc i))"
proof (cases ?thesis, simp)
case False
hence T: "∀i. c (?Sf i)
= c (?Sf (Suc i))" by simp
{
fix i
have "c (?Sf i) = c (?Sf 0)"
proof (induct i)
case (Suc j) thus ?case by (simp add: T[rule_format, of j])
qed simp
}
thus ?thesis using HMul HLex
by (cases "c (?Sf 0)") auto
qed
then obtain i where
Hdiff: "c (?Sf i) ≠ c (?Sf (Suc i))"
by auto
from Hdiff have Hf: "snd (S (Suc i)) = []"
using SS[rule_format, of i] by auto
show ?thesis
proof (cases "c (?Sf (Suc i)) = c (?Sf (Suc (Suc i)))")
case False thus ?thesis using Hf and SS[rule_format, of "Suc i"] by auto
next
case True
show ?thesis
proof (cases "c (?Sf (Suc i))")
case Mul
with True and SS[rule_format, of "Suc i"]
have "fst (mul_ext (rpo_pr m) (snd (S (Suc i)))
(snd (S (Suc (Suc i)))))"
by auto
with Hf and s_mul_ext_bottom_strict show ?thesis
by (simp add: Let_def mul_ext_def s_mul_ext_bottom_strict)
next
case Lex
with True and SS[rule_format, of "Suc i"]
have "fst (lex_ext (rpo_pr m) m (snd (S (Suc i)))
(snd (S (Suc (Suc i)))))"
by auto
with Hf show ?thesis by (simp add: lex_ext_iff)
qed
qed
qed
qed
}
hence "SN_on ?r3 {ab}" unfolding SN_on_def unfolding singleton_iff ..
}
hence "SN ?r3" unfolding SN_on_def by blast
have SN:"SN ?r0" (is "SN ?r0")
proof (rule lex_two[OF _ prc_SN ‹SN ?r3›])
let ?r' = "{(f,g). fst (prc f g)}"
let ?r = "{(f,g). snd (prc f g)}"
{
fix a1 a2 a3
assume "(a1,a2) ∈ ?r" "(a2,a3) ∈ ?r'"
hence "(a1,a3) ∈ ?r'"
by (cases "prc a1 a2", cases "prc a2 a3", cases "prc a1 a3",
insert prc_compat[of a1 a2 _ _ a3], force)
}
thus "?r O ?r' ⊆ ?r'" by auto
qed
let ?m = "λ (f,ts). ((f,length ts), ((f, length ts), ts))"
let ?r = "inv_image ?r0 ?m"
have SN_r: "SN ?r" by (rule SN_inv_image[OF SN])
let ?ind = "λ (f,ts). ?Slist ts ⟶ ?S (Fun f ts)"
have "?ind (f,ts)"
proof (rule SN_induct[OF SN_r, of ?ind])
fix fts
assume ind: "⋀ gss. (fts,gss) ∈ ?r ⟹ ?ind gss"
obtain f ts where Pair: "fts = (f,ts)" by force
show "?ind fts" unfolding Pair split
proof (intro impI)
assume ts: "?Slist ts"
let ?t = "Fun f ts"
show "?S ?t"
proof (simp only: iff[of ?t], intro allI impI)
fix s
assume "(?t,s) ∈ ?R"
hence "?gr ?t s" by simp
thus "?S s"
proof (induct s, simp add: var_SN)
case (Fun g ss) note IH = this
let ?s = "Fun g ss"
from Fun have t_gr_s: "?gr ?t ?s" by auto
show "?S ?s"
proof (cases "∃ t ∈ set ts. ?ge t ?s")
case True
then obtain t where "t ∈ set ts" and ge: "?ge t ?s" by auto
with ts have "?S t" by auto
show "?S ?s"
proof (unfold iff[of ?s], intro allI impI)
fix u
assume "(?s,u) ∈ ?R"
with rpo_compat ge have u: "?gr t u" by blast
with ‹?S t›[unfolded iff[of t]]
show "?S u" by simp
qed
next
case False note oFalse = this
let ?ls = "length ss"
let ?lt = "length ts"
let ?f = "(f,?lt)"
let ?g = "(g,?ls)"
obtain s1 ns1 where prc1: "prc ?f ?g = (s1,ns1)" by force
from False t_gr_s have f_ge_g: "ns1"
by (cases ?thesis, auto simp: Let_def prc1)
from False t_gr_s f_ge_g have small_ss: "∀ s ∈ set ss. ?gr ?t s"
by (cases ?thesis, auto simp: Let_def)
with Fun have ss_S: "?Slist ss" by auto
show ?thesis
proof (cases s1)
case True
hence "((f,ts),(g,ss)) ∈ ?r" by (simp add: prc1)
with ind have "?ind (g,ss)" using Pair by auto
with ss_S show ?thesis by auto
next
case False
show ?thesis
proof (cases "c ?f")
case Mul note cf = this
show ?thesis
proof (cases "c ?g")
case Mul note cg = this
from False oFalse t_gr_s small_ss f_ge_g cf cg
have mul: "fst (mul_ext (rpo_pr m) ts ss)"
by (cases ?thesis, auto simp: Let_def prc1)
from False mul ts f_ge_g cf cg have "((f,ts),(g,ss)) ∈ ?r"
by (simp add: prc1)
with ind have "?ind (g,ss)" using Pair by auto
with ss_S show ?thesis by auto
next
case Lex note cg = this
from cf cg False oFalse f_ge_g t_gr_s small_ss prc1
have "((f,ts),(g,ss)) ∈ ?r" by auto
with ind have "?ind (g,ss)" using Pair by auto
with ss_S show ?thesis by simp
qed
next
case Lex note cf = this
show ?thesis
proof (cases "c ?g")
case Mul note cg = this
from cf cg False oFalse f_ge_g t_gr_s small_ss prc1
have "((f,ts),(g,ss)) ∈ ?r" by auto
with ind have "?ind (g,ss)" using Pair by auto
with ss_S show ?thesis by simp
next
case Lex note cg = this
from False oFalse t_gr_s small_ss f_ge_g cf cg
have mul: "fst (lex_ext (rpo_pr m) m ts ss)"
by (cases ?thesis, auto simp: Let_def prc1)
from False mul ts f_ge_g cf cg have "((f,ts),(g,ss)) ∈ ?r"
by (simp add: prc1)
with ind have "?ind (g,ss)" using Pair by auto
with ss_S show ?thesis by auto
qed
qed
qed
qed
qed
qed
qed
qed
with Fun show ?case by simp
qed
}
from SN_I[OF this]
show "SN {(s::('f, 'v)term, t). fst (rpo_pr m s t)}" .
qed
end
sublocale rpo_pr ⊆ rpo_redpair: mono_ce_af_redtriple "RPO_S_pr n" "RPO_NS_pr n" "RPO_NS_pr n" full_af
proof (unfold_locales, rule RPO_S_SN)
show "subst.closed (RPO_NS_pr n)"
unfolding subst.closed_def
proof (rule subrelI)
fix s t :: "('f, 'v) term"
assume "(s,t) ∈ subst.closure (RPO_NS_pr n)"
then obtain u v and σ::"('f, 'v) subst"
where "(u,v) ∈ RPO_NS_pr n" and "u⋅σ = s" and "v⋅σ = t"
by (cases rule: subst.closure.cases) auto
thus "(s,t) ∈ RPO_NS_pr n" unfolding RPO_NS_pr_def using rpo_stable[of n] by auto
qed
next
show "subst.closed (RPO_S_pr n)"
unfolding subst.closed_def
proof (rule subrelI)
fix s t :: "('f, 'v) term"
assume "(s,t) ∈ subst.closure (RPO_S_pr n)"
then obtain u v and σ :: "('f, 'v) subst"
where "(u,v) ∈ RPO_S_pr n" and "u⋅σ = s" and "v⋅σ = t"
by (cases rule: subst.closure.cases) auto
thus "(s,t) ∈ RPO_S_pr n" unfolding RPO_S_pr_def using rpo_stable[of n] by auto
qed
next
show "ctxt.closed (RPO_NS_pr n)"
by (rule one_imp_ctxt_closed, unfold RPO_NS_pr_def, insert rpo_nstri_mono, blast)
show "∃ k. ∀ m ≥ k. ∀ c. ce_trs (c,m) ⊆ RPO_NS_pr n"
proof (intro exI allI impI)
fix m c
show "ce_trs (c,m) ⊆ RPO_NS_pr n"
unfolding RPO_NS_pr_def
by (simp add: ce_trs.simps, auto simp: size_simps rpo_stri_imp_nstri[OF supt_imp_rpo_stri])
qed
show "∃ k. ∀ m ≥ k. ∀ c. ce_trs (c,m) ⊆ RPO_S_pr n"
proof (intro exI allI impI)
fix m c
show "ce_trs (c,m) ⊆ RPO_S_pr n"
unfolding RPO_S_pr_def
by (simp add: ce_trs.simps, auto simp: size_simps supt_imp_rpo_stri)
qed
show "RPO_S_pr n O RPO_NS_pr n ⊆ RPO_S_pr n"
unfolding RPO_S_pr_def RPO_NS_pr_def using rpo_compat[of n] by auto
show "RPO_S_pr n ⊆ RPO_NS_pr n" using rpo_stri_imp_nstri
unfolding RPO_S_pr_def RPO_NS_pr_def by blast
qed (rule RPO_compat, rule full_af)
sublocale rpo_pr ⊆ rpo_redpair: redtriple_order "RPO_S_pr n" "RPO_NS_pr n" "RPO_NS_pr n"
by (unfold_locales, insert RPO_NS_refl RPO_NS_trans RPO_S_trans, auto)
context rpo_pr
begin
lemma RPO_S_pr_ctxt_closed: "ctxt.closed (RPO_S_pr n)"
by (rule one_imp_ctxt_closed, unfold RPO_S_pr_def, insert rpo_stri_mono, blast)
lemma rpo_manna_ness: assumes "⋀ l r. (l,r) ∈ R ⟹ fst (rpo_pr n l r)"
shows "SN (rstep R)"
by (rule rpo_redpair.manna_ness, rule RPO_S_pr_ctxt_closed[of n], insert assms, unfold RPO_S_pr_def, auto)
sublocale reduction_order "λ s t. fst (rpo_pr n s t)"
proof
let ?SS = "λ s t. fst (rpo_pr n s t)"
fix s t u :: "('f,'a)term" and σ :: "('f,'a) subst" and C
show "?SS s t ⟹ ?SS t u ⟹ ?SS s u" by (rule rpo_trans)
show "?SS s t ⟹ ?SS (s ⋅ σ) (t ⋅ σ)" using rpo_stable by auto
show "?SS s t ⟹ ?SS C⟨s⟩ C⟨t⟩"
using ctxt.closedD[OF RPO_S_pr_ctxt_closed [of n], unfolded RPO_S_pr_def] by auto
show "SN {(x, y). ?SS x y}" using RPO_S_SN[of n] unfolding RPO_S_pr_def .
qed
end
definition
rpo_strict
where
"rpo_strict pr τ n ≡ λ(s, t). check (fst (rpo (pr_nat pr) τ n s t)) (''could not orient '' +#+ shows s +@+ '' >RPO '' +#+ shows t +@+ shows_nl)"
definition
rpo_nstrict
where
"rpo_nstrict pr τ n ≡ λ (s,t). check (snd (rpo (pr_nat pr) τ n s t)) (''could not orient '' +#+ shows s +@+ '' >=RPO '' +#+ shows t +@+ shows_nl)"
interpretation rpo_pr_prc: rpo_pr "prc_nat pr" "prl_nat pr" c
for "pr" :: "'f × nat ⇒ nat" and c :: "'f × nat ⇒ order_tag" ..
abbreviation RPO_S where "RPO_S pr τ n ≡ rpo_pr.RPO_S_pr (prc_nat pr) (prl_nat pr) τ n"
abbreviation RPO_NS where "RPO_NS pr τ n ≡ rpo_pr.RPO_NS_pr (prc_nat pr) (prl_nat pr) τ n"
interpretation RPO_redtriple_impl: redtriple_impl "RPO_S pr τ n" "RPO_NS pr τ n" "RPO_NS pr τ n" "rpo_strict pr τ n" "rpo_nstrict pr τ n" "rpo_nstrict pr τ n"
by (unfold_locales, unfold rpo_strict_def rpo_nstrict_def rpo_pr_prc.RPO_S_pr_def rpo_pr_prc.RPO_NS_pr_def, auto)
interpretation RPO_ce_mono_redpair: mono_ce_af_redtriple_order_impl "RPO_S pr τ n" "RPO_NS pr τ n" "RPO_NS pr τ n" "rpo_strict pr τ n" "rpo_nstrict pr τ n" "rpo_nstrict pr τ n" succeed full_af
by (unfold_locales, rule rpo_pr_prc.RPO_S_pr_ctxt_closed)
fun rpo_unbounded :: "('f × nat ⇒ 'f × nat ⇒ bool × bool) × ('f × nat ⇒ bool)
⇒ ('f × nat ⇒ order_tag) ⇒ ('f,'v)term ⇒ ('f,'v)term ⇒ bool × bool" where
"rpo_unbounded _ _ (Var x) (Var y) = (False, x = y)"
| "rpo_unbounded pr _ (Var x) (Fun g ts) = (False, ts = [] ∧ snd pr (g,0))"
| "rpo_unbounded pr c (Fun f ss) (Var y) =
(let con = ∃s ∈ set ss. snd (rpo_unbounded pr c s (Var y)) in (con,con))"
| "rpo_unbounded pr c (Fun f ss) (Fun g ts) = (
if ∃s ∈ set ss. snd (rpo_unbounded pr c s (Fun g ts))
then (True,True)
else (case (fst pr) (f,length ss) (g,length ts) of (prs,prns) ⇒
if prns ∧ (∀t ∈ set ts. fst (rpo_unbounded pr c (Fun f ss) t))
then if prs
then (True,True)
else if c (f,length ss) = c (g,length ts)
then if c (f,length ss) = Mul
then mul_ext (rpo_unbounded pr c) ss ts
else lex_ext_unbounded (rpo_unbounded pr c) ss ts
else (length ss ≠ 0 ∧ length ts = 0, length ts = 0)
else (False,False)))"
lemma rpo_unbounded_stri_imp_nstri[rule_format]: "fst (rpo_unbounded pr c s t) ⟶
snd (rpo_unbounded pr c s t)"
proof (induct rule: rpo_unbounded.induct[of "λ pr c s t. fst (rpo_unbounded pr c s t) ⟶ snd (rpo_unbounded pr c s t)"])
case (4 "pr" c f ss g ts)
obtain prc prl where prec: "pr = (prc,prl)" by (cases "pr", auto)
obtain s ns where prc: "prc (f,length ss) (g,length ts) = (s,ns)" by force
show ?case
by (auto simp: Let_def lex_ext_unbounded_stri_imp_nstri
mul_ext_stri_imp_nstri prec prc)
qed (auto simp: Let_def)
lemma rpo_to_rpo_unbounded:
assumes "∀ f i. (f, i) ∈ funas_term s ∪ funas_term t ⟶ i ≤ n" (is "?b s t")
shows "rpo pr c n s t = rpo_unbounded pr c s t" (is "?e pr c s t")
proof -
let ?p = "λp c s t. ?b s t ⟶ ?e p c s t"
{
fix p c s t
have "?p p c s t"
proof (induct rule: rpo_unbounded.induct[where P = ?p])
case (3 p c f ss y)
show ?case
proof (intro impI)
assume "?b (Fun f ss) (Var y)"
hence "⋀ s. s ∈ set ss ⟹ ?b s (Var y)" by auto
with 3 show "?e p c (Fun f ss) (Var y)" by simp
qed
next
case (4 p c f ss g ts) note IH = this
show ?case
proof (intro impI)
assume "?b (Fun f ss) (Fun g ts)"
hence bs: "⋀ s. s ∈ set ss ⟹ ?b s (Fun g ts)"
and bt: "⋀ t. t ∈ set ts ⟹ ?b (Fun f ss) t"
and ss: "length ss ≤ n" and ts: "length ts ≤ n" by auto
with 4(1) have s: "⋀ s. s ∈ set ss ⟹ ?e p c s (Fun g ts)" by simp
show "?e p c (Fun f ss) (Fun g ts)"
proof (cases "∃ s ∈ set ss. snd (rpo p c n s (Fun g ts))")
case True with s show ?thesis by simp
next
case False note oFalse = this
with s have oFalse2: "¬ (∃s ∈ set ss. snd (rpo_unbounded p c s (Fun g ts)))"
by simp
obtain prns prs where Hsns: "(fst p) (f,length ss) (g,length ts) = (prs, prns)" by force
with bt 4(2)[OF oFalse2 Hsns[symmetric]]
have t: "⋀ t. t ∈ set ts ⟹ ?e p c (Fun f ss) t" by force
show ?thesis
proof (cases "prns ∧ (∀t∈set ts. fst (rpo p c n (Fun f ss) t))")
case False
show ?thesis
proof (cases "prns")
case False thus ?thesis by (simp add: oFalse oFalse2 Hsns)
next
case True
with False have Hf1: "¬ (∀t∈set ts. fst (rpo p c n (Fun f ss) t))" by simp
with t have Hf2: "¬ (∀t∈set ts. fst (rpo_unbounded p c (Fun f ss) t))" by auto
show ?thesis by (simp add: oFalse oFalse2 Hf1 Hf2)
qed
next
case True
hence prns: "prns" and Hts: "∀t∈set ts. fst (rpo p c n (Fun f ss) t)" by auto
from Hts and t have Hts2: "∀t∈set ts. fst (rpo_unbounded p c (Fun f ss) t)" by auto
show ?thesis
proof (cases "prs")
case True thus ?thesis by (simp add: oFalse oFalse2 Hsns prns Hts Hts2)
next
case False note prs = this
show ?thesis
proof (cases "c (f,length ss) = c (g,length ts)")
case False thus ?thesis
by (cases "c (f,length ss)", simp_all add: oFalse oFalse2 Hsns prns Hts Hts2)
next
case True note cfg = this
show ?thesis
proof (cases "c (f,length ss)")
case Mul note cf = this
with cfg have cg: "c (g,length ts) = Mul" by simp
{
fix x y
assume x_in_ss: "x ∈ set ss" and y_in_ts: "y ∈ set ts"
from 4(3)[OF oFalse2 Hsns[symmetric] _ prs cfg cf
x_in_ss y_in_ts] prns Hts2 bs[OF x_in_ss] bt[OF y_in_ts]
have "rpo p c n x y = rpo_unbounded p c x y" by auto
}
with mul_ext_cong[of ss ss ts ts]
have "mul_ext (rpo p c n) ss ts = mul_ext (rpo_unbounded p c) ss ts"
by metis
thus ?thesis
by (simp add: oFalse oFalse2 Hsns prns Hts Hts2 cf cg)
next
case Lex note cf = this
hence ncf: "c (f,length ss) ≠ Mul" by simp
from cf cfg have cg: "c (g,length ts) = Lex" by simp
{
fix i
assume iss: "i < length ss" and its: "i < length ts"
from nth_mem_mset[OF iss] and in_multiset_in_set
have in_ss: "ss ! i ∈ set ss" by force
from nth_mem_mset[OF its] and in_multiset_in_set
have in_ts: "ts ! i ∈ set ts" by force
from 4(4)[OF oFalse2 Hsns[symmetric] _ prs cfg ncf iss its]
prns Hts2 bs[OF in_ss] bt[OF in_ts]
have "rpo p c n (ss ! i) (ts ! i) = rpo_unbounded p c (ss ! i) (ts ! i)"
by simp
}
with lex_ext_cong[of ss ss n n ts ts]
have "lex_ext (rpo p c n) n ss ts
= lex_ext (rpo_unbounded p c) n ss ts" by metis
hence " lex_ext (rpo p c n) n ss ts = lex_ext_unbounded (rpo_unbounded p c) ss ts"
by (simp add: lex_ext_to_lex_ext_unbounded[OF ss ts, of "rpo_unbounded p c"])
thus ?thesis
by (simp add: oFalse oFalse2 Hsns prns prs Hts Hts2 cf cg)
qed
qed
qed
qed
qed
qed
qed auto
}
thus ?thesis using assms by simp
qed
definition
rpo_strict_unbounded
where
"rpo_strict_unbounded pr c ≡ λ(s, t). check (fst (rpo_unbounded pr c s t)) (''could not orient '' +#+ shows s +@+ '' >RPO '' +#+ shows t +@+ shows_nl)"
definition
rpo_nstrict_unbounded
where
"rpo_nstrict_unbounded pr c ≡ λ(s, t). check (snd (rpo_unbounded pr c s t)) (''could not orient '' +#+ shows s +@+ '' >=RPO '' +#+ shows t +@+ shows_nl)"
type_synonym 'f status_prec_repr = "(('f × nat) × (nat × order_tag))list"
fun shows_rpo_repr :: "('f :: show) status_prec_repr ⇒ shows"
where
"shows_rpo_repr prs =
shows ''RPO with the following precedence'' ∘ shows_nl ∘ foldr (λ((f, n), (pr, s)).
shows ''precedence('' ∘ shows f ∘ shows ''['' ∘ shows n ∘ shows '']) = '' ∘ shows pr ∘ shows_nl) prs ∘
shows_nl ∘
shows ''precedence(_) = 0'' ∘ shows_nl ∘
shows ''and the following status'' ∘ shows_nl ∘
foldr (λ((f, n), (pr, s)).
shows ''status('' ∘ shows f ∘ shows ''['' ∘ shows n ∘ shows '']) = '' ∘
shows (case s of Mul ⇒ ''mul'' | Lex ⇒ ''lex'') ∘ shows_nl) prs ∘
shows_nl ∘
shows ''status(_) = lex'' ∘ shows_nl"
fun create_RPO_redtriple :: "(('f :: show) status_prec_repr ⇒ ('g × nat ⇒ nat) × ('g × nat ⇒ order_tag)) ⇒ 'f status_prec_repr ⇒ ('g :: show,'v :: show)redtriple"
where "create_RPO_redtriple prec_repr_to_pr pr = (let (p,τ) = prec_repr_to_pr pr;
ns = rpo_nstrict_unbounded (pr_nat p) τ in
⦇ redtriple.valid = succeed,
s = rpo_strict_unbounded (pr_nat p) τ,
ns = ns, nst = ns,
af = full_af,
mono_af = full_af,
mono = (λ _. succeed),
desc = shows_rpo_repr pr,
not_ws_ns = Some [],
cpx = no_complexity_check⦈)"
interpretation RPO_redpair: generic_redtriple_impl "create_RPO_redtriple (prec_repr_to_pr :: ('f :: show)status_prec_repr ⇒ ('g :: show × nat ⇒ nat) × ('g × nat ⇒ order_tag))"
proof
fix "prτ" :: "('f :: show)status_prec_repr"
and s_list ns_list nst_list :: "('g :: show,'v :: show)rule list"
let ?rp = "create_RPO_redtriple prec_repr_to_pr prτ :: ('g,'v)redtriple"
let ?af = "redtriple.af ?rp :: ('g af)"
let ?af' = "redtriple.mono_af ?rp :: ('g af)"
let ?cpx = "redtriple.cpx ?rp"
let ?cpx' = "λ cm cc. isOK(?cpx cm cc)"
let ?pr = "prec_repr_to_pr prτ"
obtain "pr" τ where id: "?pr = (pr,τ)" by (cases ?pr, auto)
assume stri: "isOK(check_allm (redtriple.s ?rp) s_list)"
and nstri: "isOK (check_allm (redtriple.ns ?rp) ns_list)"
and nstri_top: "isOK (check_allm (redtriple.nst ?rp) nst_list)"
obtain n where n: "n = max_list (map (λ (s,t). max_list (map snd ((funas_term_list s) @ (funas_term_list t)))) (s_list @ ns_list @ nst_list))" by auto
{
fix s t
assume st: "(s,t) ∈ set (s_list @ ns_list @ nst_list)"
have "∀ f i. (f,i) ∈ funas_term s ∪ funas_term t ⟶ i ≤ n"
proof (intro allI impI)
fix f i
assume fi: "(f,i) ∈ funas_term s ∪ funas_term t"
from max_list st have one: "max_list (map snd ((funas_term_list s) @ (funas_term_list t))) ≤ n" (is "?ml ≤ n") unfolding n by force
from fi max_list have two: "i ≤ ?ml" by force
from one two show "i ≤ n" by simp
qed
hence "rpo (pr_nat pr) τ n s t = rpo_unbounded (pr_nat pr) τ s t"
by (rule rpo_to_rpo_unbounded)
} note main = this
have mono: "mono_ce_af_redtriple_order (RPO_S pr τ n) (RPO_NS pr τ n) (RPO_NS pr τ n) full_af" ..
let ?S = "RPO_S pr τ n :: ('g, 'v) term rel"
have ctxt: "ctxt.closed ?S"
by (rule RPO_ce_mono_redpair.checkMonoSound, simp)
have ce_af: "cpx_ce_af_redtriple_order ?S (RPO_NS pr τ n) (RPO_NS pr τ n) full_af full_af no_complexity"
by (unfold_locales, rule ctxt_closed_imp_af_monotone[OF ctxt])
show "∃ S NS NST. cpx_ce_af_redtriple_order S NS NST ?af ?af' ?cpx' ∧ set s_list ⊆ S ∧ set ns_list ⊆ NS ∧ set nst_list ⊆ NST ∧
not_ws_info NS (redtriple.not_ws_ns ?rp) ∧
(isOK (redtriple.mono ?rp (s_list @ ns_list @ nst_list)) ⟶ mono_ce_af_redtriple_order S NS NST ?af ∧ ctxt.closed S)"
proof (simp add: id Let_def, intro exI, intro conjI allI ws_fun_argI, rule ce_af)
show "ctxt.closed ?S" by (rule ctxt)
next
fix f nn i and ts :: "('g,'v)term list"
assume nn: "length ts = nn" and i: "i < nn"
show "(Fun f ts, ts ! i) ∈ RPO_NS pr τ n"
by (rule rpo_pr_prc.RPO_NS_subt, insert i[folded nn], auto)
next
{
fix s t
assume st: "(s,t) ∈ set s_list"
with stri have "fst (rpo_unbounded (pr_nat pr) τ s t)"
by (auto simp: id rpo_strict_unbounded_def Let_def)
with st have "fst (rpo (pr_nat pr) τ n s t)" by (simp add: main)
hence "(s,t) ∈ RPO_S pr τ n" unfolding rpo_pr_prc.RPO_S_pr_def by simp
}
thus "set s_list ⊆ RPO_S pr τ n" ..
{
fix s t
assume st: "(s,t) ∈ set (ns_list @ nst_list)"
with nstri nstri_top have "snd (rpo_unbounded (pr_nat pr) τ s t)"
by (auto simp: id rpo_nstrict_unbounded_def Let_def)
with st have "snd (rpo (pr_nat pr) τ n s t)" by (simp add: main)
hence "(s,t) ∈ RPO_NS pr τ n" unfolding rpo_pr_prc.RPO_NS_pr_def by simp
} note * = this
show "set ns_list ⊆ RPO_NS pr τ n" using * by auto
show "set nst_list ⊆ RPO_NS pr τ n" using * by auto
qed (rule mono)
qed
definition check_LPO_valid :: "('f :: show × nat ⇒ nat) ⇒ ('f × nat) list ⇒ nat × 'f × _ × shows check" where
"check_LPO_valid prec fs = (let
F = set fs;
pr = (λ f g. if g ∈ F then if f ∈ F then (prec f > prec g, prec f > prec g ∨ f = g) else (True, True) else (False, f = g));
n = max_list (map snd fs);
fs_pr = map (λ f. (f, prec f)) fs;
cs = map fst (filter (λ (fn,p). snd fn = 0 ∧ p = 0) fs_pr); (* constants with precedence 0 *)
c = fst (if cs = [] then (if fs = [] then Code.abort (STR ''empty function symbol list in LPO'') (λ x. hd fs)
else hd fs) else hd cs);
prl = (λ f. f = (c,(0 :: nat)));
valid = do {
check (cs ≠ []) (shows ''did not find minimal constant, i.e., one with precedence 0'');
check (distinct (map snd fs_pr)) (shows ''precedence is not distinct'')
}
in (n, c, (pr, prl), valid))"
definition create_LPO_redorder :: "('f :: show × nat ⇒ nat) ⇒ ('f × nat) list ⇒ ('f, string) redord"
where "create_LPO_redorder prec fs = (let
(n, c, pr, valid) = check_LPO_valid prec fs;
F = set fs;
S = rpo pr (λ _. Lex) n
in ⦇ redord.valid = valid,
redord.less = (λ s t. fst (S s t)),
redord.min_const = c ⦈)"
lemma rpo_prec_mono: assumes prc: "⋀ f g. fst (prc1 f g) ⟹ fst (prc2 f g)"
"⋀ f g. snd (prc1 f g) ⟹ snd (prc2 f g)"
shows "fst (rpo (prc1,prl) c n s t) ⟹ fst (rpo (prc2,prl) c n s t)"
"snd (rpo (prc1,prl) c n s t) ⟹ snd (rpo (prc2,prl) c n s t)"
proof (atomize(full), induct "size s + size t" arbitrary: s t rule: less_induct)
case (less s t)
let ?S1 = "λ s t. fst (rpo (prc1, prl) c n s t)"
let ?NS1 = "λ s t. snd (rpo (prc1, prl) c n s t)"
let ?S2 = "λ s t. fst (rpo (prc2, prl) c n s t)"
let ?NS2 = "λ s t. snd (rpo (prc2, prl) c n s t)"
show ?case
proof (cases s)
case (Var x)
thus ?thesis by (cases t, auto)
next
case s: (Fun f ss)
hence "⋀ si. si ∈ set ss ⟹ size si + size t < size s + size t" by (auto simp: size_simps)
note IH_si_t = less[OF this]
show ?thesis
proof (cases t)
case (Var y)
thus ?thesis unfolding s using IH_si_t by (auto simp: Let_def)
next
case t: (Fun g ts)
hence size: "⋀ ti. ti ∈ set ts ⟹ size s + size ti < size s + size t" by (auto simp: size_simps)
note IH_s_ti = less[OF this]
{
assume contra: "¬ ?thesis"
with rpo_stri_imp_nstri
have NS1: "?NS1 s t" and S2: "¬ ?S2 s t" by blast+
let ?f = "(f,length ss)" let ?g = "(g,length ts)"
obtain prs1 prns1 where prc1: "prc1 ?f ?g = (prs1, prns1)" by force
obtain prs2 prns2 where prc2: "prc2 ?f ?g = (prs2, prns2)" by force
from S2[unfolded s t] IH_si_t have *: "(∃si∈set ss. ?NS1 si (Fun g ts)) = False"
by (auto split: if_splits simp: t)
note NS1 = NS1[unfolded s t rpo.simps this if_False fst_conv prc1 Let_def split]
from NS1 IH_s_ti t s have prns1: prns1 and s_ti: "(∀t∈set ts. ?S2 (Fun f ss) t) = True"
by (auto split: if_splits)
from prc[of ?f ?g] prns1 prc1 prc2 have prns2: "prns2 = True" and prs1: "prs1 ⟹ prs2" by auto
note S2 = S2[unfolded s t rpo.simps s_ti prc2 Let_def fst_conv split s_ti prns2]
from S2 prs1 have prs1: "prs1 = False" by (auto split: if_splits)
note NS1 = NS1[unfolded prs1 if_False]
{
fix si ti
assume mem: "si ∈ set ss" "ti ∈ set ts"
hence "size si < size s" unfolding s
by (auto simp: size_simps)
with size[OF mem(2)] have "size si + size ti < size s + size t" by auto
}
note IH = less[OF this]
from lex_ext_unbounded_mono[of ss ts "rpo (prc1, prl) c n" "rpo (prc2, prl) c n"]
IH[unfolded set_conv_nth]
have lex: "(snd (lex_ext (rpo (prc1, prl) c n) n ss ts) ⟶ snd (lex_ext (rpo (prc2, prl) c n) n ss ts)) ∧
(fst (lex_ext (rpo (prc1, prl) c n) n ss ts) ⟶ fst (lex_ext (rpo (prc2, prl) c n) n ss ts))"
unfolding lex_ext_def by (auto simp: Let_def)
with NS1 S2 contra * s_ti prns2 s t prc1 prc2 prs1
have mul: "snd (mul_ext (rpo (prc1, prl) c n) ss ts) ∧ ¬ snd (mul_ext (rpo (prc2, prl) c n) ss ts) ∨
fst (mul_ext (rpo (prc1, prl) c n) ss ts) ∧ ¬ fst (mul_ext (rpo (prc2, prl) c n) ss ts)"
by (auto split: if_splits simp: Let_def)
note d = mul_ext_def Let_def snd_conv fst_conv
{
assume ns: "snd (mul_ext (rpo (prc1, prl) c n) ss ts)"
have "snd (mul_ext (rpo (prc2, prl) c n) ss ts)" unfolding d
by (rule ns_mul_ext_local_mono[OF _ _ ns[unfolded d]], insert IH, auto)
} note ns = this
{
assume s: "fst (mul_ext (rpo (prc1, prl) c n) ss ts)"
have "fst (mul_ext (rpo (prc2, prl) c n) ss ts)" unfolding d
by (rule s_mul_ext_local_mono[OF _ _ s[unfolded d]], insert IH, auto)
} note s = this
from mul ns s have False by auto
}
thus ?thesis by blast
qed
qed
qed
lemma create_LPO_redorder: "reduction_order_impl create_LPO_redorder"
proof (unfold_locales, intro conjI)
fix prec and fs :: "('a × nat)list"
let ?O = "create_LPO_redorder prec fs"
let ?S = "redord.less ?O"
let ?c = "redord.min_const ?O"
assume valid: "isOK (redord.valid ?O)"
obtain n c prc prl valid where *: "check_LPO_valid prec fs = (n, c, (prc,prl), valid)"
by (cases "check_LPO_valid prec fs", auto)
note lpo = create_LPO_redorder_def[of prec fs, unfolded * Let_def split]
let ?SS = "λs t :: ('a,string)term. fst (rpo (prc, prl) (λ_. Lex) n s t)"
have less: "?S = ?SS"
unfolding lpo by auto
from valid have valid: "valid = return ()" unfolding lpo by auto
have c: "?c = c" unfolding lpo by simp
note * = *[unfolded check_LPO_valid_def prc_nat_def Let_def prl_nat_def valid, simplified]
let ?F = "set fs"
from * have prc: "prc = (λf g. if g ∈ set fs then if f ∈ set fs then (prec g < prec f, prec g < prec f ∨ f = g) else (True, True)
else (False, f = g))"
and prl: "prl = (λf. f = (c,0))" by auto
let ?fs_pr = "map (λf. (f, prec f)) fs"
let ?prs = "λ f g. fst (prc f g)"
let ?prw = "λ f g. snd (prc f g)"
let ?cs = "[(fn, p)← ?fs_pr . snd fn = 0 ∧ p = 0]"
define cs where "cs = ?cs"
from * have cc: "c = fst (hd (map fst cs))" by (auto split: if_splits simp: cs_def)
from * have cs: "cs ≠ []" unfolding cs_def by auto
then obtain rest ac pc where cs: "cs = ((c,ac),pc) # rest" unfolding cc by (cases cs, auto)
from arg_cong[OF this, of set, unfolded cs_def]
have "((c, ac), pc) ∈ {x ∈ (λf. (f, prec f)) ` set fs. case x of (fn, p) ⇒ snd fn = 0 ∧ p = 0}"
by auto
hence p_c: "prec (c,0) = 0" and cF: "(c,0) ∈ ?F" by auto
thus "(?c,0) ∈ ?F" unfolding c by auto
from * valid
have dist: "distinct (map snd ?fs_pr)" unfolding check_def by (auto split: if_splits)
from this[unfolded distinct_map] have inj: "inj_on snd (set (map (λf. (f, prec f)) fs))" ..
{
fix f g
assume "f ∈ ?F" "g ∈ ?F" "f ≠ g"
with inj_onD[OF inj, of "(f, prec f)" "(g, prec g)"] have "prec f ≠ prec g" by force
hence "prec f > prec g ∨ prec g > prec f" by linarith
}
hence total: "⋀ f g. f ∈ ?F ⟹ g ∈ ?F ⟹ f = g ∨ prec f > prec g ∨ prec f < prec g" by auto
hence total_prec_F: "⋀ f g. f ∈ ?F ⟹ g ∈ ?F ⟹ f = g ∨ ?prs f g ∨ ?prs g f"
unfolding prc by auto
interpret rpo: rpo_pr prc prl "λ _. Lex"
proof
show "SN {(f, g). fst (prc f g)}" unfolding SN_iff_wf
by (rule wf_subset[OF wf_measures[of "[(λ f. if f ∈ ?F then 0 else 1), prec]"]],
auto simp: prc)
show "prl g ⟹ snd (prc f g) = True" for f g using cF total[OF cF, of f] by (auto simp: prc prl p_c)
qed (insert cF p_c, auto simp: prc prl split: if_splits)
show "reduction_order (redord.less ?O)" unfolding less ..
from rpo.lpo_ground_total[OF _ refl, of ?F, OF total_prec_F]
show "∀s t. fground ?F s ∧ fground ?F t ⟶ s = t ∨ ?S s t ∨ ?S t s"
unfolding less fground_def by auto
have id: "{(f, g). fst (prc f g)}¯ = {(f, g). fst (prc g f)}" by auto
from SN_imp_wf[OF rpo.prc_SN, unfolded id] have wf:"wf {(gm,fn). ?prs fn gm}" .
from wf total_well_order_extension obtain Pt where Pt:"{(gm,fn). ?prs fn gm} ⊆ Pt" and
wo:"Well_order Pt" and univ:"Field Pt = (UNIV :: ('a × nat) set)" by metis
let ?psx = "λ (fn :: 'a × nat) gm. (gm,fn) ∈ Pt - Id"
let ?pwx = "λ fn gm. (gm,fn) ∈ Pt"
from wo[unfolded well_order_on_def] have lin:"Linear_order Pt" and wf: "wf (Pt - Id)" by auto
from Linear_order_in_diff_Id[OF lin] univ have ptotal:"⋀fn gm. fn = gm ∨ ?psx fn gm ∨ ?psx gm fn" by blast
from lin[unfolded linear_order_on_def partial_order_on_def preorder_on_def refl_on_def] univ
have refl_Pt:"⋀x. (x,x) ∈ Pt" and trans_Pt: "trans Pt" by blast+
{
fix f g
assume "(g,f) ∈ Pt" "(f,g) ∈ Pt" "f ≠ g"
hence "(g,g) ∈ (Pt - Id) O (Pt - Id)" by auto
with wf have False by (meson wf_comp_self wf_not_refl)
} note two_step = this
interpret rpox: rpo_pr "λ f g. (?psx f g, ?pwx f g)" prl "λ _. Lex"
proof (unfold_locales, unfold fst_conv snd_conv)
fix f g h :: "'a × nat"
{ fix s1 ns1 h s2 ns2 s ns
assume "(?psx f g, ?pwx f g) = (s1, ns1)"
"(?psx g h, ?pwx g h) = (s2, ns2)"
"(?psx f h, ?pwx f h) = (s, ns)"
hence id: "s1 = ?psx f g" "ns1 = ?pwx f g"
"s2 = ?psx g h" "ns2 = ?pwx g h"
"s = ?psx f h" "ns = ?pwx f h"
by auto
from two_step[of f g]
show "(ns1 ∧ ns2 ⟶ ns) ∧ (ns1 ∧ s2 ⟶ s) ∧ (s1 ∧ ns2 ⟶ s)"
using trans_Pt[unfolded trans_def, rule_format, of h g f] unfolding id
by auto
}
have id: "{(f, g). (g, f) ∈ Pt - Id}¯ = Pt - Id" by auto
show "SN {(f, g). ?psx f g}" using wf unfolding SN_iff_wf id .
{
assume "prl g"
with rpo.prl[OF this, of f] have "fst (prc f g) ∨ f = g" by (auto simp: prc)
with Pt refl_Pt[of g]
show "((g, f) ∈ Pt) = True" by auto
}
assume f: "prl f" and gf: "(g,f) ∈ Pt"
from f have fc: "f = (c,0)" unfolding prl by auto
show "prl g"
proof (rule ccontr)
assume "¬ prl g"
hence gc: "g ≠ (c,0)" unfolding prl by auto
hence "?prs g (c,0)" using total_prec_F[of g, OF _ cF] p_c cF unfolding prc by auto
with Pt fc have "(f, g) ∈ Pt" by auto
from two_step[OF this gf] gc fc
show False by auto
qed
qed (auto simp: refl_Pt)
let ?SX = "λs t :: ('a,string)term. fst (rpox.rpo_pr n s t)"
let ?WX = "λs t :: ('a,string)term. snd (rpox.rpo_pr n s t)"
have gt: "ground s ⟹ ground t ⟹ s = t ∨ ?SX s t ∨ ?SX t s"
for s t
by (rule rpox.lpo_ground_total[of UNIV], insert ptotal, auto)
have gto: "gtotal_reduction_order ?SX"
by (unfold_locales, rule gt)
show "∃gt. gtotal_reduction_order gt ∧ (∀s t. ?S s t ⟶ gt s t) ∧
(∀t. ground t ⟶ gt⇧=⇧= t (Fun ?c []))" unfolding less c
proof (intro exI conjI allI impI, rule gto)
fix s t
{
assume S: "?SS s t"
show "?SX s t"
proof (rule rpo_prec_mono(1)[OF _ _ S], unfold fst_conv snd_conv)
fix f g
show "?prw f g ⟹ (g,f) ∈ Pt" using Pt by (auto simp: prc refl_Pt split: if_splits)
assume "?prs f g" thus "(g,f) ∈ Pt - Id" using Pt rpo.prc_refl[of g]
by (auto simp: prc refl_Pt split: if_splits)
qed
}
assume t: "ground (t :: ('a,string)term)"
let ?ct = "Fun c [] :: ('a,string)term"
have "ground ?ct" by auto
from gt[OF t this] have "?SX⇧=⇧= t ?ct ∨ ?SX ?ct t" by auto
thus "?SX⇧=⇧= t ?ct"
proof
assume S: "?SX ?ct t"
from rpox.rpo_least_1[of c n t] have "?WX t ?ct" unfolding prl by auto
with rpox.rpo_compat[of n] S have "?SX t t" by blast
with rpox.irrefl
show "?SX⇧=⇧= t ?ct" by blast
qed
qed
qed
end