theory Completion
imports
"Check-NT.Critical_Pairs"
Equational_Reasoning
"Check-NT.Reduction_Pair"
QTRS.Lexicographic_Extension
begin
type_synonym
('f, 'v) completion_state = "('f, 'v) equations × ('f, 'v) trs"
type_synonym
('f, 'v) completion_run = "nat × (nat ⇒ ('f, 'v) completion_state)"
lemma conversion_imp_conversion_subset:
assumes conversion: "⋀ s t. (s, t) ∈ E - E' ⟹ (s, t) ∈ (rstep E')⇧↔⇧*"
shows "(rstep E)⇧↔⇧* ⊆ (rstep E')⇧↔⇧*"
unfolding esteps_is_conversion[symmetric]
unfolding subsumes_def[symmetric]
unfolding subsumes_via_rule_conversion
proof (clarify)
fix s t
assume mem: "(s, t) ∈ E"
show "(s, t) ∈ (estep E')⇧*"
proof (cases "(s, t) ∈ E'")
case False
with mem have "(s, t) ∈ E - E'" by simp
from assms[OF this]
show ?thesis unfolding estep_sym_closure_conv by auto
next
case True
hence "(s, t) ∈ E'⇧↔" by simp
hence "(s, t) ∈ estep E'" unfolding estep_def by auto
thus ?thesis by auto
qed
qed
lemma conversion_imp_conversion_id:
assumes conversion1: "⋀ s t. (s, t) ∈ E - E' ⟹ (s, t) ∈ (rstep E')⇧↔⇧*"
and conversion2: "⋀ s t. (s, t) ∈ E' - E ⟹ (s, t) ∈ (rstep E)⇧↔⇧*"
shows "(rstep E)⇧↔⇧* = (rstep E')⇧↔⇧*" (is "?l = ?r")
proof
show "?l ⊆ ?r"
by (rule conversion_imp_conversion_subset[OF conversion1])
next
show "?r ⊆ ?l"
by (rule conversion_imp_conversion_subset[OF conversion2])
qed
locale completion = redpair_order S NS
for S NS :: "('f, 'v) trs" +
assumes mono: "ctxt.closed S"
begin
inductive_set comp_step :: "('f, 'v) completion_state rel" where
deduce: "(u, s) ∈ rstep R ⟹ (u, t) ∈ rstep R ⟹ ((E, R), (E ∪ {(s, t)}, R)) ∈ comp_step"
| orientl: "(s, t) ∈ S ⟹ ((E ∪ {(s, t)}, R), (E, R ∪ {(s, t)})) ∈ comp_step"
| orientr: "(t, s) ∈ S ⟹ ((E ∪ {(s, t)}, R), (E, R ∪ {(t, s)})) ∈ comp_step"
| simplifyl: "(s, u) ∈ rstep R ⟹ ((E ∪ {(s, t)}, R), (E ∪ {(u, t)}, R)) ∈ comp_step"
| simplifyr: "(t, u) ∈ rstep R ⟹ ((E ∪ {(s, t)}, R), (E ∪ {(s, u)}, R)) ∈ comp_step"
| delete: "((E ∪ {(s, s)}, R), (E, R)) ∈ comp_step"
| compose: "(t, u) ∈ rstep R ⟹ ((E, R ∪ {(s, t)}), (E, R ∪ {(s, u)})) ∈ comp_step"
| collapse: "(s, u) ∈ rstep R ⟹ ((E, R ∪ {(s, t)}), (E ∪ {(u, t)}, R)) ∈ comp_step"
definition completion_run :: "('f, 'v) completion_run ⇒ bool"
where "completion_run crun ≡
(case crun of (n, ERi) ⇒ (∀ i < n. (ERi i, ERi (Suc i)) ∈ comp_step))"
definition full_completion_run :: "('f, 'v) equations ⇒ ('f, 'v) completion_run ⇒ bool"
where "full_completion_run E crun ≡
completion_run crun ∧ (case crun of (n, ERi) ⇒ ERi 0 = (E, {}) ∧ fst (ERi n) = {})"
definition result :: "('f, 'v) completion_run ⇒ ('f, 'v) trs"
where "result crun ≡ snd (snd crun (fst crun))"
definition eqns :: "('f, 'v) completion_state ⇒ ('f, 'v) equations"
where "eqns ER ≡ fst ER ∪ snd ER"
lemma completion_run_conversion:
assumes "completion_run (n, ERi)"
and "i ≤ n"
shows "(rstep (eqns (ERi 0)))⇧↔⇧* = (rstep (eqns (ERi i)))⇧↔⇧*"
using ‹i ≤ n›
proof (induct i)
case 0
show ?case by simp
next
case (Suc i)
obtain E R where ERi: "ERi i = (E, R)" by force
obtain E' R' where ERsi: "ERi (Suc i) = (E', R')" by force
from Suc assms have "(ERi i, ERi (Suc i)) ∈ comp_step" unfolding
completion_run_def by auto
hence step: "((E, R),(E', R')) ∈ comp_step" unfolding ERi ERsi .
from Suc have "(rstep (eqns (ERi 0)))⇧↔⇧* = (rstep (eqns (ERi i)))⇧↔⇧*" by simp
also have "... = (rstep (E ∪ R))⇧↔⇧*" unfolding ERi eqns_def by simp
also have "... = (rstep (E' ∪ R'))⇧↔⇧*" (is "?l = ?r")
using step
proof (cases rule: comp_step.cases)
case (delete s)
show ?thesis unfolding delete
by (rule conversion_imp_conversion_id, auto)
next
case (deduce u s t)
from deduce(3) have "(s, u) ∈ (rstep (E ∪ R))⇧↔" by auto
also have "(u, t) ∈ (rstep (E ∪ R))⇧↔" using deduce(4) by auto
finally have conv: "(s, t) ∈ (rstep (E ∪ R))⇧↔⇧*" by auto
show ?thesis unfolding deduce
by (rule conversion_imp_conversion_id, insert conv, auto)
next
case (orientl s t)
show ?thesis unfolding orientl
by (rule conversion_imp_conversion_id, auto)
next
case (orientr s t)
show ?thesis unfolding orientr
by (rule conversion_imp_conversion_id, auto)
next
case (simplifyl s u F t)
from simplifyl(4) have "(s, u) ∈ (rstep (F ∪ R ∪ {(u, t)}))⇧↔" by auto
also have "(u, t) ∈ (rstep (F ∪ R ∪ {(u, t)}))⇧↔" by auto
finally have st: "(s, t) ∈ (rstep (F ∪ R ∪ {(u, t)}))⇧↔⇧*" by auto
from simplifyl(4) have "(u, s) ∈ (rstep (F ∪ R ∪ {(s, t)}))⇧↔" by auto
also have "(s, t) ∈ (rstep (F ∪ R ∪ {(s, t)}))⇧↔" by auto
finally have ut: "(u, t) ∈ (rstep (F ∪ R ∪ {(s, t)}))⇧↔⇧*" by auto
show ?thesis unfolding simplifyl
by (rule conversion_imp_conversion_id, insert st ut, auto)
next
case (simplifyr t u F s)
have "(s, u) ∈ (rstep (F ∪ R ∪ {(s, u)}))⇧↔" by auto
also have "(u, t) ∈ (rstep (F ∪ R ∪ {(s, u)}))⇧↔" using simplifyr(4) by auto
finally have st: "(s, t) ∈ (rstep (F ∪ R ∪ {(s, u)}))⇧↔⇧*" by auto
have "(s, t) ∈ (rstep (F ∪ R ∪ {(s, t)}))⇧↔" by auto
also have "(t, u) ∈ (rstep (F ∪ R ∪ {(s, t)}))⇧↔" using simplifyr(4) by auto
finally have su: "(s, u) ∈ (rstep (F ∪ R ∪ {(s, t)}))⇧↔⇧*" by auto
show ?thesis unfolding simplifyr
by (rule conversion_imp_conversion_id, insert st su, auto)
next
case (compose t u Q s)
have "(s, u) ∈ (rstep (E ∪ Q ∪ {(s, u)}))⇧↔" by auto
also have "(u, t) ∈ (rstep (E ∪ Q ∪ {(s, u)}))⇧↔" using compose(4) by auto
finally have st: "(s, t) ∈ (rstep (E ∪ Q ∪ {(s, u)}))⇧↔⇧*" by auto
have "(s, t) ∈ (rstep (E ∪ Q ∪ {(s, t)}))⇧↔" by auto
also have "(t, u) ∈ (rstep (E ∪ Q ∪ {(s, t)}))⇧↔" using compose(4) by auto
finally have su: "(s, u) ∈ (rstep (E ∪ Q ∪ {(s, t)}))⇧↔⇧*" by auto
show ?thesis unfolding compose
by (rule conversion_imp_conversion_id, insert st su , auto)
next
case (collapse s u t)
from collapse(3) have "(s, u) ∈ (rstep (E ∪ R' ∪ {(u, t)}))⇧↔" by auto
also have "(u, t) ∈ (rstep (E ∪ R' ∪ {(u, t)}))⇧↔" by auto
finally have st: "(s, t) ∈ (rstep (E ∪ R' ∪ {(u, t)}))⇧↔⇧*" by auto
from collapse(3) have "(u, s) ∈ (rstep (E ∪ R' ∪ {(s, t)}))⇧↔" by auto
also have "(s, t) ∈ (rstep (E ∪ R' ∪ {(s, t)}))⇧↔" by auto
finally have ut: "(u, t) ∈ (rstep (E ∪ R' ∪ {(s, t)}))⇧↔⇧*" by auto
show ?thesis unfolding collapse
by (rule conversion_imp_conversion_id, insert st ut, auto)
qed
finally show ?case unfolding ERsi eqns_def by simp
qed
lemma completion_run_orientation:
assumes "completion_run (n, ERi)"
and "snd (ERi 0) ⊆ S"
and "i ≤ n"
shows "snd (ERi i) ⊆ S"
using ‹i ≤ n›
proof (induct i)
case 0 show ?case using assms by simp
next
case (Suc i)
obtain E R where ERi: "ERi i = (E, R)" by force
obtain E' R' where ERsi: "ERi (Suc i) = (E', R')" by force
from Suc assms have "(ERi i, ERi (Suc i)) ∈ comp_step" unfolding
completion_run_def by auto
hence step: "((E, R),(E', R')) ∈ comp_step" unfolding ERi ERsi .
from Suc have "snd (ERi i) ⊆ S" by simp
hence or: "R ⊆ S" unfolding ERi by simp
have "R' ⊆ S" using step
proof (cases rule: comp_step.cases)
case (delete s)
thus ?thesis using or by auto
next
case (deduce u s t)
thus ?thesis using or by auto
next
case (orientl s t)
thus ?thesis using or by auto
next
case (orientr s t)
thus ?thesis using or by auto
next
case (simplifyl s u F t)
thus ?thesis using or by auto
next
case (simplifyr t u F s)
thus ?thesis using or by auto
next
case (compose t u Q s)
note t = or[unfolded compose] compose(4)
from rstep_subset[OF mono subst_S] t(1) have "rstep Q ⊆ S" by simp
with t(2) have tu: "(t, u) ∈ S" ..
have "(s, u) ∈ S" by (rule trans_S_point[OF _ tu], insert t(1), auto)
thus ?thesis using or compose(4) unfolding compose by auto
next
case (collapse s u t)
thus ?thesis using or by auto
qed
thus ?case unfolding ERsi by simp
qed
lemma full_completion_run:
assumes full: "full_completion_run E crun"
shows "(rstep E)⇧↔⇧* = (rstep (result crun))⇧↔⇧* ∧ SN (rstep (result crun))"
proof -
obtain n ERi where crun: "crun = (n, ERi)" by force
note full = full[unfolded crun full_completion_run_def split]
from full have run: "completion_run (n, ERi)" by simp
from completion_run_conversion[OF run, of n]
have conv: "(rstep E)⇧↔⇧* = (rstep (result crun))⇧↔⇧*"
using full unfolding crun result_def eqns_def by auto
from completion_run_orientation[OF run, of n]
have "result crun ⊆ S" using full unfolding crun result_def eqns_def by auto
from manna_ness[OF mono this] conv show ?thesis by simp
qed
end
type_synonym
('f, 'v) comp_conversion_terms = "nat ⇒ ('f, 'v) term"
type_synonym
('f, 'v) comp_conversion_rules = "nat ⇒ ('f, 'v) rule × bool option"
type_synonym
('f, 'v) comp_conversion = "nat × ('f, 'v) comp_conversion_terms × ('f, 'v) comp_conversion_rules"
locale full_completion_run = completion S NS
for S NS :: "('f, string) trs" +
fixes E :: "nat ⇒ ('f, string) equations"
and R :: "nat ⇒ ('f, string) trs"
and E0 :: "('f, string) equations"
and n :: nat
assumes frun: "full_completion_run E0 (n, λ i. (E i, R i))"
and fair: "⋀ b l r. (b, l, r) ∈ critical_pairs (R n) (R n) ⟹
(∃ i. i ≤ n ∧ (l, r) ∈ E i) ∨ (l, r) ∈ (rstep (R n))⇧↓"
begin
lemma E0_Rn_conversion: "(rstep E0)⇧↔⇧* = (rstep (R n))⇧↔⇧*"
using full_completion_run[OF frun] unfolding result_def by simp
lemma Rn_SN: "SN (rstep (R n))"
using full_completion_run[OF frun] unfolding result_def by simp
definition R_all where "R_all ≡ ⋃ {R i | i. i ≤ n}"
definition E_all where "E_all ≡ ⋃ {E i | i. i ≤ n}"
fun valid_step :: "('f, string) term ⇒ ('f, string) rule × bool option ⇒ ('f, string) term ⇒ bool"
where "valid_step s (lr, None) t = (lr ∈ E_all ∧ (s, t) ∈ (rstep {lr})⇧↔)"
| "valid_step s (lr, Some True) t = (lr ∈ R_all ∧ (s, t) ∈ rstep {lr})"
| "valid_step s (lr, Some False) t = (lr ∈ R_all ∧ (s, t) ∈ (rstep {lr})¯)"
fun comp_conversion :: "('f, string) term ⇒ ('f, string) comp_conversion ⇒ ('f, string) term ⇒ bool"
where "comp_conversion s (m, si, ri) t ⟷
s = si 0 ∧ t = si m ∧ (∀ i < m. valid_step (si i) (ri i) (si (Suc i)))"
fun rewrite_conversion :: "('f, string) comp_conversion ⇒ bool"
where "rewrite_conversion (m, _, ri) ⟷
(∀ i < m. fst (ri i) ∈ R n) ∧ (∃ k ≤ m. (∀ i < k. snd (ri i) = Some True) ∧
(∀ i. k ≤ i ⟶ i < m ⟶ snd (ri i) = Some False))"
lemma forward_step:
assumes "snd r = Some True" and "valid_step s r t"
shows "(s, t) ∈ (rstep (R_all ∩ {fst r}))"
proof -
from assms(1) obtain lr where r: "r = (lr, Some True)" by (cases r, auto)
note valid = assms(2)[unfolded r, simplified]
from valid show ?thesis unfolding r fst_conv
by auto
qed
lemma backward_step:
assumes "snd r = Some False" and "valid_step s r t"
shows "(s, t) ∈ (rstep (R_all ∩ {fst r}))¯"
proof -
from assms(1) obtain lr where r: "r = (lr, Some False)" by (cases r, auto)
note valid = assms(2)[unfolded r, simplified]
from valid show ?thesis unfolding r fst_conv
by auto
qed
lemma equation_step:
assumes "snd r = None" and "valid_step s r t"
shows "(s, t) ∈ (rstep (E_all ∩ {fst r}))⇧↔"
proof -
from assms(1) obtain lr where r: "r = (lr, None)" by (cases r, auto)
note valid = assms(2)[unfolded r, simplified]
from valid show ?thesis unfolding r fst_conv
by auto
qed
lemma rewrite_conversion_imp_join:
assumes conv: "comp_conversion s conv t"
and rewr: "rewrite_conversion conv"
shows "(s, t) ∈ (rstep (R n))⇧↓"
proof -
obtain m si ri where c: "conv = (m, si, ri)" by (cases conv, auto)
note rewr = rewr[unfolded c, simplified]
from rewr obtain k where km: "k ≤ m" and
forward: "⋀ i. i < k ⟹ snd (ri i) = Some True"
and backward: "⋀ i. k ≤ i ⟹ i < m ⟹ snd (ri i) = Some False"
by auto
note conv = conv[unfolded c, simplified]
from forward km
have forward: "(s, si k) ∈ (rstep (R n))⇧*"
proof (induct k)
case 0
show ?case using conv by simp
next
case (Suc k)
hence steps: "(s, si k) ∈ (rstep (R n))⇧*" by auto
from Suc(2) have snd: "snd (ri k) = Some True" by simp
with conv Suc(3) have valid: "valid_step (si k) (ri k) (si (Suc k))" by simp
from Suc(3) rewr have Rn: "fst (ri k) ∈ R n" by auto
from set_mp[OF rstep_mono forward_step[OF snd valid], of "R n"]
have "(si k, si (Suc k)) ∈ rstep (R n)" using Rn by auto
with steps show ?case by auto
qed
let ?R = "((rstep (R n))¯)"
{
fix i
assume i: "k + i ≤ m"
from i have "(si k, si (k + i)) ∈ ?R⇧*"
proof (induct i)
case 0
show ?case by simp
next
case (Suc i)
let ?i = "k + i"
from Suc have steps: "(si k, si ?i) ∈ ?R⇧*" by auto
from Suc(2) have ki: "?i < m" by simp
from backward[OF _ this] have snd: "snd (ri ?i) = Some False" by simp
from conv ki have "valid_step (si ?i) (ri ?i) (si (Suc ?i))" by simp
from backward_step[OF snd this]
have step: "(si ?i, si (Suc ?i)) ∈ (rstep (R_all ∩ {fst (ri ?i)}))¯" by auto
from rewr ki have fst: "fst (ri ?i) ∈ R n" by simp
have "(si ?i, si (Suc ?i)) ∈ ?R" unfolding reverseTrs
by (rule set_mp[OF rstep_mono step[unfolded reverseTrs]],
insert fst, auto)
with steps show ?case by auto
qed
}
from this[of "m - k"] km have "(si k, si m) ∈ ?R⇧*" by auto
with conv have "(t, si k) ∈ (?R⇧*)¯" by simp
hence backward: "(t, si k) ∈ (rstep (R n))⇧*" unfolding rtrancl_converse by simp
show ?thesis
by (rule, rule forward, rule backward)
qed
definition orule :: "('f, string) rule ⇒ nat"
where "orule lr ≡ LEAST i. i ≤ n ∧ lr ∈ R (n - i)"
fun
c ::
"('f, string) term ⇒ ('f, string) rule × bool option ⇒ ('f, string) term ⇒
('f, string) term list × nat"
where
"c s (_, None) t = ([s, t], 0)" |
"c s (lr, Some True) t = ([s], orule lr)" |
"c s (lr, Some False) t = ([t], orule lr)"
fun cost :: "('f, string) comp_conversion ⇒ (('f, string) term list × nat) list"
where "cost (m, si, ri) = map (λ i. c (si i) (ri i) (si (Suc i))) [0 ..< m]"
fun
conversion_merge ::
"('f, string) comp_conversion ⇒ ('f, string) comp_conversion ⇒ ('f, string) comp_conversion"
where
"conversion_merge (m1, si1, ri1) (m2, si2, ri2) =
(m1 + m2,
(λ i. if i < m1 then si1 i else si2 (i - m1)),
(λ i. if i < m1 then ri1 i else ri2 (i - m1)))"
lemma conversion_merge:
assumes c1: "comp_conversion t1 c1 t2"
and c2: "comp_conversion t2 c2 t3"
shows "comp_conversion t1 (conversion_merge c1 c2) t3 ∧
cost (conversion_merge c1 c2) = cost c1 @ cost c2"
proof -
obtain m1 si1 ri1 where 1: "c1 = (m1, si1, ri1)" by (cases c1, auto)
obtain m2 si2 ri2 where 2: "c2 = (m2, si2, ri2)" by (cases c2, auto)
note c1 = c1[unfolded 1]
note c2 = c2[unfolded 2]
let ?m = "m1 + m2"
let ?si = "(λ i. if i < m1 then si1 i else si2 (i - m1))"
let ?ri = "(λ i. if i < m1 then ri1 i else ri2 (i - m1))"
let ?c = "conversion_merge (m1, si1, ri1) (m2, si2, ri2)"
{
fix i
assume i: "i ≤ m1"
have "?si i = si1 i" using i c1 c2
by (cases "i < m1", auto)
} note si1 = this
{
fix i
assume i: "i ≥ m1"
hence "?si i = si2 (i - m1)" by simp
} note si2 = this
show ?thesis unfolding conversion_merge.simps comp_conversion.simps 1 2
proof (intro conjI allI impI)
have "t1 = si1 0" using c1 by simp
also have "... = ?si 0" using si1[of 0] by simp
finally show "t1 = ?si 0" .
next
have "t3 = si2 m2" using c2 by simp
also have "... = ?si ?m" using si2[of ?m] by simp
finally show "t3 = ?si ?m" .
next
fix i
assume i: "i < ?m"
show "valid_step (?si i) (?ri i) (?si (Suc i))"
proof (cases "i < m1")
case True
thus ?thesis using si1[of i] si1[of "Suc i"] c1 by auto
next
case False
hence id: "Suc i - m1 = Suc (i - m1)" by simp
with False have id: "?si i = si2 (i - m1)" "?si (Suc i) = si2 (Suc (i - m1))" by auto
show ?thesis unfolding id using i False c2 by simp
qed
next
have le: "0 ≤ m1" by simp
let ?c = "λ i. c (?si i) (?ri i) (?si (Suc i))"
let ?c1 = "λ i. c (si1 i) (ri1 i) (si1 (Suc i))"
let ?c2 = "λ i. c (si2 i) (ri2 i) (si2 (Suc i))"
have id1: "cost (?m, ?si, ?ri) = map ?c [0 ..< m1] @ map ?c [m1 ..< ?m]"
unfolding cost.simps upt_add_eq_append[OF le] map_append ..
have id2: "map ?c [0 ..< m1] = map ?c1 [0 ..< m1]"
proof (rule nth_map_conv, simp, intro allI impI)
fix i
assume "i < length [0 ..< m1]"
hence i: "i < m1" by simp
hence "?c ([0 ..< m1] ! i) = ?c i" by simp
also have "... = ?c1 i" using si1[of i] si1[of "Suc i"] i by simp
finally show "?c ([0 ..< m1] ! i) = ?c1 ([0 ..< m1] ! i)" using i by simp
qed
have id3: "map ?c [m1 ..< ?m] = map ?c2 [0 ..< m2]"
proof (rule nth_map_conv, simp, intro allI impI)
fix i
assume "i < length [m1..< ?m]"
hence i: "i < m2" by simp
hence "?c ([m1 ..< ?m] ! i) = ?c (m1 + i)" by simp
also have "... = ?c2 i" using si2[of "m1 + i"] si2[of "m1 + Suc i"] i by simp
finally show "?c ([m1 ..< ?m] ! i) = ?c2 ([0 ..< m2] ! i)" using i by simp
qed
from id1[unfolded id2 id3]
show "cost (?m, ?si, ?ri) = cost (m1, si1, ri1) @ cost(m2, si2, ri2)"
by simp
qed
qed
definition conversion_merge_three :: "('f, string) comp_conversion ⇒ ('f, string) comp_conversion ⇒ ('f, string) comp_conversion ⇒ ('f, string) comp_conversion"
where "conversion_merge_three c1 c2 c3 = conversion_merge (conversion_merge c1 c2) c3"
lemma conversion_merge_three:
assumes c1: "comp_conversion t1 c1 t2"
and c2: "comp_conversion t2 c2 t3"
and c3: "comp_conversion t3 c3 t4"
shows "comp_conversion t1 (conversion_merge_three c1 c2 c3) t4 ∧
cost (conversion_merge_three c1 c2 c3) = cost c1 @ cost c2 @ cost c3"
proof -
from conversion_merge[OF c1 c2] have c12: "comp_conversion t1 (conversion_merge c1 c2) t3"
and cost: "cost (conversion_merge c1 c2) = cost c1 @ cost c2" by auto
from conversion_merge[OF c12 c3] cost show ?thesis
unfolding conversion_merge_three_def by simp
qed
fun
conversion_split ::
"('f, string) comp_conversion ⇒ nat ⇒
('f, string) comp_conversion × ('f, string) comp_conversion"
where
"conversion_split (m, si, ri) k = (
(k, si, ri),
(m - k, λ i. si (i + k), λ i. ri (i + k)))"
lemma conversion_split_left:
assumes "comp_conversion t (m, si, ri) u"
and "k ≤ m"
shows "comp_conversion t (fst (conversion_split (m, si, ri) k)) (si k)"
using assms by auto
lemma conversion_split_right:
assumes "comp_conversion t (m, si, ri) u"
and "k ≤ m"
shows "comp_conversion (si k) (snd (conversion_split (m, si, ri) k)) u"
using assms by auto
lemma conversion_split_cost:
assumes k: "k ≤ m"
shows "cost (m, si, ri) = cost (fst (conversion_split (m, si, ri) k)) @
cost (snd (conversion_split (m, si, ri) k))"
proof -
from upt_add_eq_append[of 0 k "m - k"] k
have id: "[0..<m] = [0..<k] @ [k..<m]" by simp
show ?thesis by (simp add: id, rule nth_map_conv, auto simp: ac_simps)
qed
fun
conversion_split_three ::
"('f, string) comp_conversion ⇒ nat ⇒ nat ⇒
('f, string) comp_conversion × ('f, string) comp_conversion × ('f, string) comp_conversion"
where
"conversion_split_three c123 k1 k2 = (
let (c12, c3) = conversion_split c123 k2;
(c1, c2) = conversion_split c12 k1
in (c1, c2, c3))"
lemma conversion_split_three:
assumes c: "comp_conversion t (m, si, ri) u"
and k1: "k1 ≤ k2"
and k2: "k2 ≤ m"
and s3: "conversion_split_three (m, si, ri) k1 k2 = (c1, c2, c3)"
shows "comp_conversion t c1 (si k1) ∧
comp_conversion (si k1) c2 (si k2) ∧
comp_conversion (si k2) c3 u ∧
cost (m, si, ri) = cost c1 @ cost c2 @ cost c3 ∧
c2 = (k2 - k1, (λ i. si (k1 + i)), (λ i. ri (k1 + i)))"
proof -
let ?c = "comp_conversion"
let ?s = "conversion_split"
obtain c12 c3' where s1: "?s (m, si, ri) k2 = (c12, c3')" by force
note s3 = s3[unfolded conversion_split_three.simps Let_def s1 split]
from s3 have s2: "?s c12 k1 = (c1, c2)" by (cases "?s c12 k1", auto)
from s3[unfolded s2] s1 have s1: "?s (m, si, ri) k2 = (c12, c3)" by simp
from conversion_split_right[OF c k2, unfolded s1] have 3: "?c (si k2) c3 u" by simp
from conversion_split_left[OF c k2, unfolded s1] have 12: "?c t c12 (si k2)" by simp
have c12: "c12 = (k2, si, ri)" using s1 by simp
note 12 = 12[unfolded c12]
note s2 = s2[unfolded c12]
have c2: "c2 = (k2 - k1, λi. si (k1 + i), λi. ri (k1 + i))" using s2
by (auto simp: ac_simps)
from conversion_split_left[OF 12 k1, unfolded s2] have 1: "?c t c1 (si k1)" by simp
from conversion_split_right[OF 12 k1, unfolded s2] have 2: "?c (si k1) c2 (si k2)" by simp
from conversion_split_cost[OF k2, of si ri, unfolded s1]
have "cost (m, si, ri) = cost c12 @ cost c3" by simp
also have "... = cost c1 @ cost c2 @ cost c3"
using conversion_split_cost[OF k1, of si ri] unfolding c12 using s2 by auto
finally
show ?thesis using 1 2 3 c2 by simp
qed
definition C where
"C ≡ lex_two
{(xs,ys). (mset ys, mset xs) ∈ mult1 (S¯)}
{(xs,ys). mset xs = mset ys}
{(a,b :: nat) . a > b}"
definition Cost :: "('f, string) comp_conversion rel" where
"Cost ≡ {(a, b). (mset (cost b), mset (cost a)) ∈ mult (C¯)}"
lemma comp_step:
"i < n ⟹ ((E i, R i), (E (Suc i), R (Suc i))) ∈ comp_step"
using frun[unfolded full_completion_run_def split completion_run_def]
by auto
lemma rstep_R_all_S: "rstep R_all ⊆ S"
proof -
note frun = frun[unfolded full_completion_run_def split]
hence crun: "completion_run (n, λi. (E i, R i))" ..
{
fix i
assume "i ≤ n"
from completion_run_orientation[OF crun _ this] frun
have "R i ⊆ S" by auto
}
hence rel: "R_all ⊆ S" unfolding R_all_def by auto
show ?thesis
by (rule rstep_subset[OF mono subst_S rel])
qed
lemma proof_simplification:
assumes cconv: "comp_conversion s conv t"
and nrewr: "¬ rewrite_conversion conv"
shows "∃ conv'. comp_conversion s conv' t ∧ (conv, conv') ∈ Cost"
proof -
obtain m si ri where c: "conv = (m, si, ri)" by (cases conv, auto)
note cconv = cconv[unfolded c]
note conv = cconv[simplified]
from conv have valid: "⋀ i. i < m ⟹ valid_step (si i) (ri i) (si (Suc i))"
by auto
let ?smaller = "λ i. ∃ m' si' ri'. comp_conversion (si i) (m', si', ri') (si (Suc i)) ∧
(∀ i' < m'. (c (si i) (ri i) (si (Suc i)), c (si' i') (ri' i') (si' (Suc i'))) ∈ C)"
let ?smaller2 = "λ i. ∃ m' si' ri'. comp_conversion (si i) (m', si', ri') (si (Suc (Suc i))) ∧
(∀ i' < m'. (c (si i) (ri i) (si (Suc i)), c (si' i') (ri' i') (si' (Suc i'))) ∈ C)"
have main: "(∃ i < m. ?smaller i) ∨ (∃ i. Suc i < m ∧ ?smaller2 i)"
proof (cases "∃ i < m. snd (ri i) = None")
case True note 1 = this
then obtain i where i: "i < m" and snd: "snd (ri i) = None" by auto
then obtain lr where ri: "ri i = (lr, None)" by (cases "ri i", auto)
from equation_step[OF snd valid[OF i]]
have step: "(si i, si (Suc i)) ∈ (rstep E_all)⇧↔"
and lr_step: "(si i, si (Suc i)) ∈ (rstep {lr})⇧↔" and lr_mem: "lr ∈ E_all"
unfolding ri by auto
have ci: "c (si i) (ri i) (si (Suc i)) = ([si i, si (Suc i)], 0)" (is "_ = ?ci")
unfolding ri by simp
{
from lr_mem[unfolded E_all_def] obtain j where j: "j ≤ n" and lr_mem: "lr ∈ E j"
by auto
let ?P = "λ j. j ≤ n ∧ lr ∈ E (n - j)"
have P: "?P (n - j)" using lr_mem j by simp
obtain j where j: "j = (LEAST j. ?P j)" by auto
from LeastI[of ?P, OF P] have lr_mem: "?P j" unfolding j .
from frun[unfolded full_completion_run_def]
have lr_nmem: "lr ∉ E n" by auto
have j0: "j ≠ 0"
proof
assume "j = 0"
with lr_nmem lr_mem show False by simp
qed
hence "j - Suc 0 < j" by simp
from not_less_Least[OF this[unfolded j]] have lr_nmem: "¬ ?P (j - Suc 0)"
unfolding j .
from j0 lr_mem have id: "n - (j - Suc 0) = Suc (n - j)" by (cases j, auto)
have "∃ j < n. lr ∈ E j ∧ lr ∉ E (Suc j)"
by (intro exI conjI, insert j0 lr_mem lr_nmem, auto simp: id)
}
then obtain j where j: "j < n" and lr_mem: "lr ∈ E j"
and lr_nmem: "lr ∉ E (Suc j)" by blast
hence neq: "E j ≠ E (Suc j)" by auto
show ?thesis
proof (rule disjI1, rule exI, rule conjI[OF i])
from comp_step[OF j] have cstep: "((E j, R j), (E (Suc j), R (Suc j))) ∈ comp_step" .
from cstep show "?smaller i"
proof(cases)
case (delete s)
with lr_mem lr_nmem have "lr = (s, s)" by simp
from lr_step[unfolded this] have "(si i, si (Suc i)) ∈ (rstep Id)⇧↔"
by auto
with rstep_id have id: "si i = si (Suc i)" by force
let ?si' = "λ n :: nat. si i"
let ?ri' = ri
from id have conv: "comp_conversion (si i) (0, ?si', ?ri') (si (Suc i))"
by simp
show ?thesis
by (intro exI conjI, rule conv, simp add: ci)
next
case (orientl s t)
with lr_mem lr_nmem have lr: "lr = (s, t)" by simp
let ?si' = "λ i' :: nat. if i' = 0 then si i else si (Suc i)"
from j have "Suc j ≤ n" by simp
with orientl(2) have st: "(s, t) ∈ R_all" unfolding R_all_def by blast
from lr_step[unfolded lr] show ?thesis
proof
assume step: "(si i, si (Suc i)) ∈ rstep {(s, t)}"
let ?ri' = "λ i' :: nat. ((s, t), Some True)"
have conv: "comp_conversion (si i) (Suc 0, ?si', ?ri') (si (Suc i))"
using step st
by (auto simp: R_all_def)
have C: "(?ci, c (?si' 0) (?ri' 0) (?si' (Suc 0))) ∈ C"
by (simp add: C_def mult1_ab_a)
show ?thesis
by (intro exI conjI, rule conv, insert C, auto simp: ci)
next
assume step: "(si i, si (Suc i)) ∈ (rstep {(s, t)})¯"
let ?ri' = "λ i' :: nat. ((s, t), Some False)"
have conv: "comp_conversion (si i) (Suc 0, ?si', ?ri') (si (Suc i))"
using step st
by simp
have C: "(?ci, c (?si' 0) (?ri' 0) (?si' (Suc 0))) ∈ C"
by (simp add: C_def mult1_ab_b)
show ?thesis
by (intro exI conjI, rule conv, insert C, auto simp: ci)
qed
next
case (orientr t s)
with lr_mem lr_nmem have lr: "lr = (s, t)" by simp
let ?si' = "λ i' :: nat. if i' = 0 then si i else si (Suc i)"
from j have "Suc j ≤ n" by simp
with orientr(2) have st: "(t, s) ∈ R_all" unfolding R_all_def by blast
from lr_step[unfolded lr] show ?thesis
proof
assume "(si i, si (Suc i)) ∈ rstep {(s, t)}"
hence step: "(si i, si (Suc i)) ∈ (rstep {(t, s)})¯" unfolding reverseTrs
converse_def by auto
let ?ri' = "λ i' :: nat. ((t, s), Some False)"
have conv: "comp_conversion (si i) (Suc 0, ?si', ?ri') (si (Suc i))"
using step st
by (auto simp: R_all_def)
have C: "(?ci, c (?si' 0) (?ri' 0) (?si' (Suc 0))) ∈ C"
by (simp add: C_def mult1_ab_b)
show ?thesis
by (intro exI conjI, rule conv, insert C, auto simp: ci)
next
assume "(si i, si (Suc i)) ∈ (rstep {(s, t)})¯"
hence step: "(si i, si (Suc i)) ∈ rstep {(t, s)}" unfolding reverseTrs converse_def by auto
let ?ri' = "λ i' :: nat. ((t, s), Some True)"
have conv: "comp_conversion (si i) (Suc 0, ?si', ?ri') (si (Suc i))"
using step st
by simp
have C: "(?ci, c (?si' 0) (?ri' 0) (?si' (Suc 0))) ∈ C"
by (simp add: C_def mult1_ab_a)
show ?thesis
by (intro exI conjI, rule conv, insert C, auto simp: ci)
qed
next
case (simplifyl s u E' t)
with lr_mem lr_nmem have lr: "lr = (s, t)" by simp
from lr_step[unfolded lr] have step: "(si i, si (Suc i)) ∈ rstep {(s, t),(t, s)}"
by auto
then obtain D l r σ where id: "si i = D⟨l ⋅ σ⟩" "si (Suc i) = D⟨r ⋅ σ⟩" and
mem: "(l, r) = (s, t) ∨ (l, r) = (t, s)" by auto
from simplifyl(4) obtain l' r' D' σ' where
id': "s = D'⟨l' ⋅ σ'⟩" "u = D'⟨r' ⋅ σ'⟩" and lr': "(l', r') ∈ R j"
by auto
from j have "j ≤ n" "Suc j ≤ n" by auto
with simplifyl(2) lr' have lr': "(l', r') ∈ R_all" and
ut: "(u, t) ∈ E_all" unfolding E_all_def R_all_def by blast+
have su_step: "(D⟨s ⋅ σ⟩, D⟨u ⋅ σ⟩) ∈ rstep (R_all ∩ {(l', r')})"
by (unfold id',
rule rstepI[of l' r' _ _ "D ∘⇩c (D' ⋅⇩c σ)" "σ' ∘⇩s σ"], insert lr', auto)
have su_S: "(D⟨s ⋅ σ⟩, D⟨u ⋅ σ⟩) ∈ S"
by (rule set_mp[OF rstep_R_all_S], insert su_step, auto)
from mem
show ?thesis
proof
assume "(l, r) = (s, t)"
hence id2: "l = s" "r = t" by auto
note id = id[unfolded id2]
let ?one = "D⟨s ⋅ σ⟩"
let ?two = "D⟨u ⋅ σ⟩"
let ?three = "D⟨t ⋅ σ⟩"
let ?si' = "λ i' :: nat. case i' of 0 ⇒ ?one | Suc 0 ⇒ ?two | _ ⇒ ?three"
let ?ri' = "λ i' :: nat. case i' of 0 ⇒ ((l', r'), Some True) | _ ⇒ ((u, t), None)"
have step1: "(?one, ?two) ∈ rstep {(l', r')}" using su_step by auto
have conv: "comp_conversion (si i) (Suc (Suc 0), ?si', ?ri') (si (Suc i))"
unfolding id
by (simp add: all_less_two lr' ut step1, auto)
have C0: "(?ci, c (?si' 0) (?ri' 0) (?si' (Suc 0))) ∈ C"
by (simp add: C_def id mult1_ab_a)
have C1: "(?ci, c (?si' (Suc 0)) (?ri' (Suc 0)) (?si' (Suc (Suc 0)))) ∈ C"
by (fastforce simp: C_def id mult1_def su_S)
show ?thesis
by (intro exI conjI, rule conv, unfold all_less_two, insert C0 C1, auto simp: ci)
next
assume "(l, r) = (t, s)"
hence id2: "l = t" "r = s" by auto
note id = id[unfolded id2]
let ?one = "D⟨t ⋅ σ⟩"
let ?two = "D⟨u ⋅ σ⟩"
let ?three = "D⟨s ⋅ σ⟩"
let ?si' = "λ i' :: nat. case i' of 0 ⇒ ?one | Suc 0 ⇒ ?two | _ ⇒ ?three"
let ?ri' = "λ i' :: nat. case i' of 0 ⇒ ((u, t), None) | _ ⇒ ((l', r'), Some False)"
have step2: "(?two, ?three) ∈ (rstep {(l', r')})¯" using su_step by auto
have conv: "comp_conversion (si i) (Suc (Suc 0), ?si', ?ri') (si (Suc i))"
unfolding id using step2
by (simp add: all_less_two lr' ut, auto)
have C0: "(?ci, c (?si' 0) (?ri' 0) (?si' (Suc 0))) ∈ C"
by (fastforce simp: C_def id mult1_def add_mset_commute su_S)
have C1: "(?ci, c (?si' (Suc 0)) (?ri' (Suc 0)) (?si' (Suc (Suc 0)))) ∈ C"
by (auto simp: C_def id mult1_ab_b)
show ?thesis
by (intro exI conjI, rule conv, unfold all_less_two, insert C0 C1, auto simp: ci)
qed
next
case (simplifyr t u E' s)
with lr_mem lr_nmem have lr: "lr = (s, t)" by simp
from lr_step[unfolded lr] have step: "(si i, si (Suc i)) ∈ rstep {(s, t),(t, s)}"
by auto
then obtain D l r σ where id: "si i = D⟨l ⋅ σ⟩" "si (Suc i) = D⟨r ⋅ σ⟩" and
mem: "(l, r) = (s, t) ∨ (l, r) = (t, s)" by auto
from simplifyr(4) obtain l' r' D' σ' where
id': "t = D'⟨l' ⋅ σ'⟩" "u = D'⟨r' ⋅ σ'⟩" and lr': "(l', r') ∈ R j"
by auto
from j have "j ≤ n" "Suc j ≤ n" by auto
with simplifyr(2) lr' have lr': "(l', r') ∈ R_all" and
su: "(s, u) ∈ E_all" unfolding E_all_def R_all_def by blast+
have tu_step: "(D⟨t ⋅ σ⟩, D⟨u ⋅ σ⟩) ∈ rstep (R_all ∩ {(l', r')})"
by (unfold id',
rule rstepI[of l' r' _ _ "D ∘⇩c (D' ⋅⇩c σ)" "σ' ∘⇩s σ"], insert lr', auto)
have tu_S: "(D⟨t ⋅ σ⟩, D⟨u ⋅ σ⟩) ∈ S"
by (rule set_mp[OF rstep_R_all_S], insert tu_step, auto)
from mem
show ?thesis
proof
assume "(l, r) = (s, t)"
hence id2: "l = s" "r = t" by auto
note id = id[unfolded id2]
let ?one = "D⟨s ⋅ σ⟩"
let ?two = "D⟨u ⋅ σ⟩"
let ?three = "D⟨t ⋅ σ⟩"
let ?si' = "λ i' :: nat. case i' of 0 ⇒ ?one | Suc 0 ⇒ ?two | _ ⇒ ?three"
let ?ri' = "λ i' :: nat. case i' of 0 ⇒ ((s, u), None) | _ ⇒ ((l', r'), Some False)"
have step2: "(?two, ?three) ∈ (rstep {(l', r')})¯" using tu_step by auto
have conv: "comp_conversion (si i) (Suc (Suc 0), ?si', ?ri') (si (Suc i))"
unfolding id using step2
by (auto simp: all_less_two lr' su)
have C0: "(?ci, c (?si' 0) (?ri' 0) (?si' (Suc 0))) ∈ C"
apply (auto simp: C_def id tu_S)
proof -
have f1: "{#} + {#D⟨s ⋅ σ⟩#} + ({#} + {#D⟨u ⋅ σ⟩#}) = {#D⟨s ⋅ σ⟩, D⟨u ⋅ σ⟩#}"
by auto
have f2: "{#} + {#D⟨s ⋅ σ⟩#} + ({#} + {#D⟨t ⋅ σ⟩#}) = {#D⟨s ⋅ σ⟩, D⟨t ⋅ σ⟩#}"
by auto
have "({#} + {#D⟨u ⋅ σ⟩#}, {#D⟨t ⋅ σ⟩#}) ∈ mult1 (S¯)"
using tu_S by auto
then show "({#D⟨s ⋅ σ⟩, D⟨u ⋅ σ⟩#}, {#D⟨s ⋅ σ⟩, D⟨t ⋅ σ⟩#}) ∈ mult1 (S¯)"
using f2 f1 by (metis (no_types) add_mset_add_single mult1_union)
qed
have C1: "(?ci, c (?si' (Suc 0)) (?ri' (Suc 0)) (?si' (Suc (Suc 0)))) ∈ C"
by (auto simp: C_def id mult1_ab_b)
show ?thesis
by (intro exI conjI, rule conv, unfold all_less_two, insert C0 C1, auto simp: ci)
next
assume "(l, r) = (t, s)"
hence id2: "l = t" "r = s" by auto
note id = id[unfolded id2]
let ?one = "D⟨t ⋅ σ⟩"
let ?two = "D⟨u ⋅ σ⟩"
let ?three = "D⟨s ⋅ σ⟩"
let ?si' = "λ i' :: nat. case i' of 0 ⇒ ?one | Suc 0 ⇒ ?two | _ ⇒ ?three"
let ?ri' = "λ i' :: nat. case i' of 0 ⇒ ((l', r'), Some True) | _ ⇒ ((s, u), None)"
have step1: "(?one, ?two) ∈ rstep {(l', r')}" using tu_step by auto
have conv: "comp_conversion (si i) (Suc (Suc 0), ?si', ?ri') (si (Suc i))"
unfolding id using step1
by (simp add: all_less_two lr' su, auto)
have C0: "(?ci, c (?si' 0) (?ri' 0) (?si' (Suc 0))) ∈ C"
by (auto simp: C_def id mult1_ab_a)
have C1: "(?ci, c (?si' (Suc 0)) (?ri' (Suc 0)) (?si' (Suc (Suc 0)))) ∈ C"
by (fastforce simp: C_def id mult1_def tu_S)
show ?thesis
by (intro exI conjI, rule conv, unfold all_less_two, insert C0 C1, auto simp: ci)
qed
qed (insert neq lr_mem lr_nmem, auto)
qed
next
case False note not_1 = this
hence no_eqns: "⋀ i. i < m ⟹ snd (ri i) ≠ None" by auto
show ?thesis
proof (cases "∃ i < m. fst (ri i) ∉ R n")
case True note 2 = this
then obtain i where i: "i < m" and nmem: "fst (ri i) ∉ R n" by auto
from no_eqns[OF i] obtain lr dir where ri: "ri i = (lr, Some dir)" by (cases "ri i", cases "snd (ri i)", auto)
from valid[OF i, unfolded ri] have lr_all: "lr ∈ R_all" by (cases dir, auto)
from ri nmem have lr_n: "lr ∉ R n" by auto
obtain j' where j': "j' = orule lr" by auto
obtain j where jj': "j = n - j'" by auto
{
let ?P = "λ j. j ≤ n ∧ lr ∈ R (n - j)"
from lr_all[unfolded R_all_def] obtain j'' where j'': "j'' ≤ n"
and lr_j'': "lr ∈ R j''" by blast
have j': "j' = (LEAST j. ?P j)" unfolding j' orule_def by simp
have P: "?P (n - j'')" using lr_j'' j'' by simp
from LeastI[of ?P, OF P] have lr_mem: "?P j'" unfolding j' .
have j'0: "j' ≠ 0"
proof
assume "j' = 0"
with lr_n lr_mem show False by simp
qed
from j'0 lr_mem have id: "n - (j' - Suc 0) = Suc (n - j')" by (cases j', auto)
have one: "lr ∈ R j" unfolding jj' using lr_mem by simp
{
fix k
assume kj: "k > j" and kn: "k ≤ n"
hence "n - k < j'" unfolding jj' by auto
from not_less_Least[OF this[unfolded j']] have "lr ∉ R k" using kn
by auto
} note two = this
have three: "j < n" unfolding jj' using j'0 lr_mem by auto
have four: "j' ≤ n" using lr_mem by simp
note one two three four
}
hence lr_mem: "lr ∈ R j" and j: "j < n" and j'n: "j' ≤ n" and lr_nmemk: "⋀ k. j < k ⟹ k ≤ n ⟹ lr ∉ R k" by auto
from lr_nmemk[of "Suc j"] j have lr_nmem: "lr ∉ R (Suc j)" by simp
with lr_mem have neq: "R j ≠ R (Suc j)" by auto
from forward_step[OF _ valid[OF i]] backward_step[OF _ valid[OF i]]
have fbstep: "(dir ∧ (si i, si (Suc i)) ∈ rstep (R_all ∩ {lr})) ∨ (¬ dir ∧ (si i, si (Suc i)) ∈ rstep ((R_all ∩ {lr})¯))"
unfolding ri reverseTrs by (cases dir, auto)
let ?lr = "if dir then lr else (snd lr, fst lr)"
let ?R_all = "if dir then R_all else R_all¯"
let ?step = "λ st. ∃ D l r σ. si i = D⟨l ⋅ σ⟩ ∧ si (Suc i) = D⟨r ⋅ σ⟩ ∧ (l, r) = st ∧ st ∈ ?R_all"
{
assume dir with fbstep have "?step ?lr" by force
}
moreover
{
assume "¬ dir" with fbstep have "?step ?lr" by force
}
ultimately have "?step ?lr" by blast
then obtain D l r σ where id: "si i = D⟨l ⋅ σ⟩" "si (Suc i) = D⟨r ⋅ σ⟩"
"(l, r) = ?lr"
and mem: "?lr ∈ ?R_all" by auto
show ?thesis
proof (rule disjI1, rule exI, rule conjI[OF i])
from comp_step[OF j] have cstep: "((E j, R j), (E (Suc j), R (Suc j))) ∈ comp_step" .
from cstep show "?smaller i"
proof(cases)
case (compose t u R' s)
with lr_mem lr_nmem have lr: "lr = (s, t)" by simp
note id = id[unfolded lr snd_conv fst_conv]
note mem = mem[unfolded lr snd_conv fst_conv]
from compose(4) obtain l' r' D' σ' where
id': "t = D'⟨l' ⋅ σ'⟩" "u = D'⟨r' ⋅ σ'⟩" and lr': "(l', r') ∈ R'"
by auto
from lr' compose(3) have lr': "(l', r') ∈ R (Suc j)" by auto
from j have "j ≤ n" "Suc j ≤ n" by auto
with compose(3) lr' have lr': "(l', r') ∈ R_all" and
su: "(s, u) ∈ R_all" unfolding R_all_def by blast+
have tu_step: "(D⟨t ⋅ σ⟩, D⟨u ⋅ σ⟩) ∈ rstep (R_all ∩ {(l', r')})"
by (unfold id',
rule rstepI[of l' r' _ _ "D ∘⇩c (D' ⋅⇩c σ)" "σ' ∘⇩s σ"], insert lr', auto)
have tu_S: "(D⟨t ⋅ σ⟩, D⟨u ⋅ σ⟩) ∈ S"
by (rule set_mp[OF rstep_R_all_S], insert tu_step, auto)
{
from j jj' obtain k where k: "j' = Suc k" by (cases j', auto)
have "orule (s, u) ≤ k"
unfolding orule_def
proof (rule Least_le, intro conjI)
show "k ≤ n" using j j'n unfolding jj' k by auto
next
have id: "Suc (n - Suc k) = n - k" using j j'n unfolding jj' k
by auto
show "(s, u) ∈ R (n - k)" using compose(3) unfolding jj' k id
by simp
qed
hence "orule (s, u) < j'" unfolding k by simp
}
note o_su = this
show ?thesis
proof (cases dir)
case True
from True ri have ci: "c (si i) (ri i) (si (Suc i)) = ([si i], j')"
(is "_ = ?ci")
unfolding j' by simp
from True id have id2: "l = s" "r = t" by auto
from True mem have mem: "(s, t) ∈ R_all" by auto
have st_S: "(D⟨s ⋅ σ⟩, D⟨t ⋅ σ⟩) ∈ S"
by (rule set_mp[OF rstep_R_all_S], insert mem, auto)
note id = id(1-2)[unfolded id2]
let ?one = "D⟨s ⋅ σ⟩"
let ?two = "D⟨u ⋅ σ⟩"
let ?three = "D⟨t ⋅ σ⟩"
let ?si' = "λ i' :: nat. case i' of 0 ⇒ ?one | Suc 0 ⇒ ?two | _ ⇒ ?three"
let ?ri' = "λ i' :: nat. case i' of 0 ⇒ ((s, u), Some True) | _ ⇒ ((l', r'), Some False)"
have step2: "(?two, ?three) ∈ (rstep {(l', r')})¯" using tu_step by auto
have conv: "comp_conversion (si i) (Suc (Suc 0), ?si', ?ri') (si (Suc i))"
unfolding id using step2
by (auto simp: all_less_two lr' su)
have C0: "(?ci, c (?si' 0) (?ri' 0) (?si' (Suc 0))) ∈ C"
by (auto simp: C_def id o_su)
have C1: "(?ci, c (?si' (Suc 0)) (?ri' (Suc 0)) (?si' (Suc (Suc 0)))) ∈ C"
by (auto simp: C_def id st_S)
show ?thesis
by (intro exI conjI, rule conv, unfold all_less_two, insert C0 C1, auto simp: ci)
next
case False
from False ri have ci: "c (si i) (ri i) (si (Suc i)) = ([si (Suc i)], j')"
(is "_ = ?ci")
unfolding j' by simp
from False id have id2: "l = t" "r = s" by auto
from False mem have mem: "(s, t) ∈ R_all" by auto
have st_S: "(D⟨s ⋅ σ⟩, D⟨t ⋅ σ⟩) ∈ S"
by (rule set_mp[OF rstep_R_all_S], insert mem, auto)
note id = id(1-2)[unfolded id2]
let ?one = "D⟨t ⋅ σ⟩"
let ?two = "D⟨u ⋅ σ⟩"
let ?three = "D⟨s ⋅ σ⟩"
let ?si' = "λ i' :: nat. case i' of 0 ⇒ ?one | Suc 0 ⇒ ?two | _ ⇒ ?three"
let ?ri' = "λ i' :: nat. case i' of 0 ⇒ ((l', r'), Some True) | _ ⇒ ((s, u), Some False)"
have step1: "(?one, ?two) ∈ rstep {(l', r')}" using tu_step by auto
have conv: "comp_conversion (si i) (Suc (Suc 0), ?si', ?ri') (si (Suc i))"
unfolding id using step1
by (simp add: all_less_two lr' su, auto)
have C0: "(?ci, c (?si' 0) (?ri' 0) (?si' (Suc 0))) ∈ C"
by (auto simp: C_def id st_S)
have C1: "(?ci, c (?si' (Suc 0)) (?ri' (Suc 0)) (?si' (Suc (Suc 0)))) ∈ C"
by (auto simp: C_def id o_su)
show ?thesis
by (intro exI conjI, rule conv, unfold all_less_two, insert C0 C1, auto simp: ci)
qed
next
case (collapse s u t)
with lr_mem lr_nmem have lr: "lr = (s, t)" by simp
note id = id[unfolded lr snd_conv fst_conv]
note mem = mem[unfolded lr snd_conv fst_conv]
from collapse(3) obtain l' r' D' σ' where
id': "s = D'⟨l' ⋅ σ'⟩" "u = D'⟨r' ⋅ σ'⟩" and lr'sj: "(l', r') ∈ R (Suc j)"
by auto
from j have "j ≤ n" "Suc j ≤ n" by auto
with collapse(2) lr'sj have lr': "(l', r') ∈ R_all" and
ut: "(u, t) ∈ E_all" unfolding E_all_def R_all_def by blast+
have su_step: "(D⟨s ⋅ σ⟩, D⟨u ⋅ σ⟩) ∈ rstep (R_all ∩ {(l', r')})"
by (unfold id', rule rstepI[of l' r' _ _ "D ∘⇩c (D' ⋅⇩c σ)" "σ' ∘⇩s σ"], insert lr', auto)
have su_S: "(D⟨s ⋅ σ⟩, D⟨u ⋅ σ⟩) ∈ S"
by (rule set_mp[OF rstep_R_all_S], insert su_step, auto)
{
from j jj' obtain k where k: "j' = Suc k" by (cases j', auto)
have "orule (l', r') ≤ k"
unfolding orule_def
proof (rule Least_le, intro conjI)
show "k ≤ n" using j j'n unfolding jj' k by auto
next
have id: "Suc (n - Suc k) = n - k" using j j'n unfolding jj' k
by auto
show "(l', r') ∈ R (n - k)" using collapse(1) lr'sj unfolding jj' k id
by simp
qed
hence "orule (l', r') < j'" unfolding k by simp
}
note o_lr' = this
show ?thesis
proof (cases dir)
case True
from True ri have ci: "c (si i) (ri i) (si (Suc i)) = ([si i], j')"
(is "_ = ?ci")
unfolding j' by simp
from True id have id2: "l = s" "r = t" by auto
from True mem have mem: "(s, t) ∈ R_all" by auto
have st_S: "(D⟨s ⋅ σ⟩, D⟨t ⋅ σ⟩) ∈ S"
by (rule set_mp[OF rstep_R_all_S], insert mem, auto)
note id = id(1-2)[unfolded id2]
let ?one = "D⟨s ⋅ σ⟩"
let ?two = "D⟨u ⋅ σ⟩"
let ?three = "D⟨t ⋅ σ⟩"
let ?si' = "λ i' :: nat. case i' of 0 ⇒ ?one | Suc 0 ⇒ ?two | _ ⇒ ?three"
let ?ri' = "λ i' :: nat. case i' of 0 ⇒ ((l', r'), Some True) | _ ⇒ ((u, t), None)"
have step1: "(?one, ?two) ∈ rstep {(l', r')}" using su_step by auto
have conv: "comp_conversion (si i) (Suc (Suc 0), ?si', ?ri') (si (Suc i))"
unfolding id
by (simp add: all_less_two lr' ut step1, auto)
have C0: "(?ci, c (?si' 0) (?ri' 0) (?si' (Suc 0))) ∈ C"
by (simp add: C_def id o_lr')
have C1: "(?ci, c (?si' (Suc 0)) (?ri' (Suc 0)) (?si' (Suc (Suc 0)))) ∈ C"
by (auto simp: C_def id st_S su_S)
show ?thesis
by (intro exI conjI, rule conv, unfold all_less_two, insert C0 C1, auto simp: ci)
next
case False
from False ri have ci: "c (si i) (ri i) (si (Suc i)) = ([si (Suc i)], j')"
(is "_ = ?ci")
unfolding j' by simp
from False id have id2: "l = t" "r = s" by auto
from False mem have mem: "(s, t) ∈ R_all" by auto
have st_S: "(D⟨s ⋅ σ⟩, D⟨t ⋅ σ⟩) ∈ S"
by (rule set_mp[OF rstep_R_all_S], insert mem, auto)
note id = id(1-2)[unfolded id2]
let ?one = "D⟨t ⋅ σ⟩"
let ?two = "D⟨u ⋅ σ⟩"
let ?three = "D⟨s ⋅ σ⟩"
let ?si' = "λ i' :: nat. case i' of 0 ⇒ ?one | Suc 0 ⇒ ?two | _ ⇒ ?three"
let ?ri' = "λ i' :: nat. case i' of 0 ⇒ ((u, t), None) | _ ⇒ ((l', r'), Some False)"
have step2: "(?two, ?three) ∈ (rstep {(l', r')})¯" using su_step by auto
have conv: "comp_conversion (si i) (Suc (Suc 0), ?si', ?ri') (si (Suc i))"
unfolding id using step2
by (simp add: all_less_two lr' ut, auto)
have C0: "(?ci, c (?si' 0) (?ri' 0) (?si' (Suc 0))) ∈ C"
by (auto simp: C_def id su_S st_S)
have C1: "(?ci, c (?si' (Suc 0)) (?ri' (Suc 0)) (?si' (Suc (Suc 0)))) ∈ C"
by (auto simp: C_def id o_lr')
show ?thesis
by (intro exI conjI, rule conv, unfold all_less_two, insert C0 C1, auto simp: ci)
qed
qed (insert lr_mem lr_nmem neq, auto)
qed
next
case False note 3 = this
{
fix i b
assume i: "i < m"
from no_eqns[OF i] have "(snd (ri i) ≠ Some b) = (snd (ri i) = Some (¬ b))" by auto
} note not_Some = this
from 3 have all_R_n: "⋀ i. i < m ⟹ fst (ri i) ∈ R n" by auto
with nrewr[unfolded c rewrite_conversion.simps]
have nrewr: "⋀ k. k ≤ m ⟹ (∃ i < k. snd (ri i) ≠ Some True) ∨
(∃ i ≥ k. i < m ∧ snd (ri i) ≠ Some False)" by auto
{
def aux ≡ "λ b. {(i, Suc i) | i. snd (ri i) = Some b}"
def f ≡ "aux True"
def b ≡ "aux False"
{
fix i j fb
assume ij: "(i, j) ∈ fb⇧*" and sub: "fb ⊆ f ∪ b"
from ij[unfolded rtrancl_is_UN_relpow] obtain n where ij: "(i, j) ∈ fb^^n" by auto
hence "j = i + n ∧ (∀ k. k ≥ i ⟶ k < j ⟶ (k, Suc k) ∈ fb)"
proof (induct n arbitrary: i j)
case (Suc n)
from Suc(2) obtain k where ik: "(i, k) ∈ fb^^n" and kj: "(k, j) ∈ fb" by auto
from kj sub have j: "j = Suc k" unfolding f_def aux_def b_def by auto
from Suc(1)[OF ik] kj show ?case unfolding j by (metis add_Suc_right neqE not_less_eq)
qed auto
hence "∃ n. j = i + n ∧ (∀ k. k ≥ i ⟶ k < j ⟶ (k, Suc k) ∈ fb)" by blast
} note rtrancl_elim = this
have "(0, m) ∈ (f ∪ b)⇧*" unfolding rtrancl_fun_conv
by (rule exI[of _ "λ x. x"], rule exI[of _ m], insert not_Some, auto simp: f_def aux_def b_def)
hence "(0, m) ∈ (f⇧* O b⇧*) ∪ (f ∪ b)⇧* O b O f O (f ∪ b)⇧*"
by regexp
hence "(0, m) ∈ (f ∪ b)⇧* O b O f O (f ∪ b)⇧*"
proof
assume "(0, m) ∈ (f⇧* O b⇧*)"
then obtain k where k: "(0, k) ∈ f⇧*" and km: "(k, m) ∈ b⇧*" by auto
from rtrancl_elim[OF k] have k: "⋀ i. i < k ⟹ (i, Suc i) ∈ f" by auto
from rtrancl_elim[OF km] obtain n where m: "m = k + n" and
km: "⋀ i. i ≥ k ⟹ i < m ⟹ (i, Suc i) ∈ b" by auto
from m have "k ≤ m" by auto
from nrewr[OF this] have False
proof
assume "∃ i < k. snd (ri i) ≠ Some True"
then obtain i where i: "i < k" and neg: "snd (ri i) ≠ Some True" by auto
from i m not_Some[of i] neg have "snd (ri i) = Some False" by auto
with k[OF i] show False unfolding f_def aux_def by auto
next
assume "∃i≥k. i < m ∧ snd (ri i) ≠ Some False"
then obtain i where i: "i ≥ k" "i < m" and neg: "snd (ri i) ≠ Some False" by blast
from not_Some[OF i(2)] neg have "snd (ri i) = Some True" by auto
with km[OF i] show False unfolding b_def aux_def by auto
qed
thus ?thesis by simp
qed
then obtain i j k where r: "(i, j) ∈ b" and f: "(j, k) ∈ f" and
km: "(k, m) ∈ (f ∪ b)⇧*" by auto
from r f have j: "j = Suc i" and k: "k = Suc (Suc i)" unfolding b_def f_def aux_def by auto
from rtrancl_elim[OF km[unfolded k]] have "i < m" "Suc i < m" by auto
with r f have "∃ l. l < m ∧ Suc l < m ∧ snd (ri l) = Some False ∧ snd (ri (Suc l)) = Some True"
unfolding b_def f_def aux_def by blast
} note peak1 = this
{
let ?P = "λ i. i < m ∧ snd (ri i) ≠ Some True"
obtain i where i: "i = (LEAST i. ?P i)" by auto
from nrewr[of m] have "∃ i. ?P i" by auto
from LeastI_ex[of ?P, OF this] have Pi: "?P i" unfolding i .
with not_Some[of i] have im: "i < m" and rev: "snd (ri i) = Some False"
by auto
{
fix j
assume "j < i"
from not_less_Least[OF this[unfolded i]] have "¬ ?P j" .
} hence "∀ j < i. ¬ ?P j" by simp
with nrewr[of i] im have "∃ j ≥ i. j < m ∧ (snd (ri j)) ≠ Some False"
by auto
then obtain j where ji: "j ≥ i" and jm: "j < m" and forw: "snd (ri j) ≠ Some False" by auto
from not_Some[OF jm] forw have forw: "snd (ri j) = Some True" by simp
with rev have "i ≠ j" by auto
with ji have ji: "j > i" by auto
let ?P = "λ k. k > i ∧ k ≤ j ∧ snd (ri k) = Some True"
obtain k where k: "k = (LEAST k. ?P k)" by auto
have Pj: "?P j" using ji forw by simp
from LeastI[of ?P, OF Pj] have Pk: "?P k" unfolding k .
then obtain l where kl: "k = Suc l" by (cases k, auto)
note Pk = Pk[unfolded kl]
from kl have "l < k" by auto
from not_less_Least[of _ ?P, OF this[unfolded k]] have Pl: "¬ ?P l" .
from kl Pk jm have lm: "l < m" "Suc l < m" by auto
{
assume "l = i"
hence "snd (ri l) = Some False" using rev by simp
}
moreover
{
assume "l ≠ i"
with Pk have "i < l" by auto
with Pk Pl have "snd (ri l) ≠ Some True" by simp
with not_Some[OF lm(1)] have "snd (ri l) = Some False" by simp
}
ultimately have rev: "snd (ri l) = Some False" by auto
with Pk lm
have "∃ l. l < m ∧ Suc l < m ∧ snd (ri l) = Some False ∧ snd (ri (Suc l)) = Some True" by blast
} note peak2 = this
from peak1 peak2
obtain i where i: "i < m" "Suc i < m" and revs: "snd (ri i) = Some False"
and forws: "snd (ri (Suc i)) = Some True" by auto
let ?i = i
let ?i' = "Suc ?i"
let ?i'' = "Suc ?i'"
show ?thesis
proof (rule disjI2, rule exI, rule conjI[OF i(2)])
from forward_step[OF forws valid[OF i(2)]]
have forw: "(si ?i', si ?i'') ∈ rstep {fst (ri ?i')}" by auto
have forw: "(si ?i', si ?i'') ∈ rstep (R n)"
by (rule set_mp[OF rstep_mono forw], insert all_R_n[OF i(2)], auto)
from backward_step[OF revs valid[OF i(1)]]
have rev: "(si ?i', si ?i) ∈ rstep {fst (ri ?i)}" by auto
have rev: "(si ?i', si ?i) ∈ rstep (R n)"
by (rule set_mp[OF rstep_mono rev], insert all_R_n[OF i(1)], auto)
have "c (si i) (ri i) (si ?i') = c (si i) (fst (ri i), snd (ri i)) (si ?i')" by simp
also have "... = ([si ?i'], orule (fst (ri i)))" (is "_ = ?ci") unfolding revs by simp
finally have ci: "c (si i) (ri i) (si ?i') = ?ci" .
from subset_trans[OF rstep_mono rstep_R_all_S, of "R n"]
have "rstep (R n) ⊆ S" unfolding R_all_def by auto
hence RnS: "⋀ x. x ∈ rstep (R n) ⟹ x ∈ S" by auto
from RnS[OF forw] have i'i'': "(si ?i', si ?i'') ∈ S" .
from RnS[OF rev] have i'i: "(si ?i', si ?i) ∈ S" .
let ?CP = "critical_pairs (R n) (R n)"
let ?cp = "∃ D b l r σ. si ?i = D⟨l ⋅ σ⟩ ∧ si ?i'' = D⟨r ⋅ σ⟩
∧ ((b, l, r) ∈ ?CP ∨ (b, r, l) ∈ ?CP)"
let ?join = "(si ?i, si ?i'') ∈ (rstep (R n))⇧↓"
from critical_pairs_main[OF rev forw]
have "?join ∨ ?cp" .
hence "?join ∨ (¬ ?join ∧ ?cp)" by blast
thus "?smaller2 i"
proof
assume join: ?join
then obtain u where iu: "(si ?i, u) ∈ (rstep (R n))⇧*"
and i''u: "(si ?i'', u) ∈ (rstep (R n))⇧*"
by auto
note conv = qrsteps_imp_qrsteps_r_p_s[where Q = "{}" and nfs = False, simplified]
{
fix s t lr p σ
assume "(s, t) ∈ qrstep_r_p_s False {} (R n) lr p σ"
note step = this[unfolded qrstep_r_p_s_def, simplified]
from step have mem: "lr ∈ R n" by simp
have step: "(s, t) ∈ rstep {lr}" unfolding rstep_iff_rstep_r_p_s
proof (intro exI)
show "(s, t) ∈ rstep_r_p_s {lr} (fst lr, snd lr) p σ"
using step unfolding rstep_r_p_s_def' by auto
qed
note mem step
} note qrstep_conv = this
from conv[OF iu] obtain mf sif lrf pf σf
where idf: "sif 0 = si i" "sif mf = u"
and stepsf: "⋀ j. j < mf ⟹
(sif j, sif (Suc j)) ∈ qrstep_r_p_s False {} (R n) (lrf j) (pf j) (σf j)"
by blast
note stepsf = qrstep_conv[OF stepsf]
from conv[OF i''u] obtain mr sir lrr "pr" σr
where idr: "sir 0 = si ?i''" "sir mr = u"
and stepsr: "⋀ j. j < mr ⟹
(sir j, sir (Suc j)) ∈ qrstep_r_p_s False {} (R n) (lrr j) (pr j) (σr j)"
by blast
note stepsr = qrstep_conv[OF stepsr]
let ?m = "mf + mr"
let ?si = "λ j. if j < mf then sif j else sir (mr - (j - mf))"
let ?ri =
"λ j. if j < mf then (lrf j, Some True)else (lrr (mr - (j - mf) - Suc 0), Some False)"
obtain m' where m': "m' = ?m" by auto
obtain si' where si': "si' = ?si" by auto
obtain ri' where ri': "ri' = ?ri" by auto
let ?fstep = "λ j. (si' j, si' (Suc j)) ∈ rstep {(fst (ri' j))} ∧ fst (ri' j) ∈ R n"
{
fix j
assume j: "j < mf"
hence fst: "fst (ri' j) = lrf j" and sij: "si' j = sif j"
unfolding ri' si' by auto
have sisj: "?si (Suc j) = sif (Suc j)"
proof (cases "Suc j < mf")
case True thus ?thesis by simp
next
case False
with j have "Suc j = mf" by simp
thus ?thesis using idf idr by simp
qed
hence sisj: "si' (Suc j) = sif (Suc j)" unfolding si' .
from stepsf[OF j] have "?fstep j" unfolding fst sij sisj by simp
} note stepsf = this
have sii: "si i = si' 0" unfolding si' m' using idf idr by (cases mf, auto)
{
fix j
assume j: "j < mf"
hence "(si ?i', si' j) ∈ S"
proof (induct j)
case 0
show ?case using i'i unfolding sii .
next
case (Suc j)
hence rel: "(si ?i', si' j) ∈ S" and less: "j < mf" by auto
show ?case
proof (rule trans_S_point[OF rel RnS])
show "(si' j, si' (Suc j)) ∈ rstep (R n)"
using stepsf[OF less] using qrstep_rule_conv[where Q = "{}" and R = "R n"] by auto
qed
qed
} note smallf = this
let ?rstep = "λ j. (si' j, si' (Suc j)) ∈ (rstep {(fst (ri' j))})¯
∧ fst (ri' j) ∈ R n"
{
fix j
assume j1: "¬ j < mf" and j2: "j < m'"
from j1 have fst: "fst (ri' j) = lrr (mr + mf - Suc j)" and
sij: "si' j = sir (mr + mf - j)"
and sisj: "si' (Suc j) = sir (mr + mf - Suc j)"
unfolding si' ri'
by auto
note j2 = j2[unfolded m']
have less: "mr + mf - Suc j < mr" using j1 j2 by arith
have id: "Suc (mr + mf - Suc j) = mr + mf - j" using j1 j2 by arith
from stepsr[OF less] have "?rstep j" unfolding fst sij sisj id by auto
} note stepsr = this
have sii'': "si ?i'' = si' m'" unfolding si' m' by (simp add: idr)
{
fix j
assume j: "j < mr"
hence "(si ?i', si' (mf + mr - j)) ∈ S"
proof (induct j)
case 0
show ?case using i'i'' unfolding sii'' m' by simp
next
case (Suc j)
hence rel: "(si ?i', si' (mf + mr - j)) ∈ S" and less: "j < mr" by auto
show ?case
proof (rule trans_S_point[OF rel RnS])
let ?j = "mf + mr - Suc j"
have id: "Suc ?j = mf + mr - j" using Suc(2) by auto
from less have jm': "?j < m'" unfolding m' by auto
from less have jmf: "¬ ?j < mf" by auto
from stepsr[OF jmf jm', unfolded id]
qrstep_rule_conv[where Q = "{}" and R = "R n"]
have "(si' ?j, si' (mf + mr - j)) ∈ (rstep (R n))¯" by force
thus "(si' (mf + mr - j), si' (mf + mr - Suc j)) ∈ rstep (R n)"
by auto
qed
qed
} note smallg = this
have conv: "comp_conversion (si ?i) (m', si', ri') (si ?i'')"
proof (unfold comp_conversion.simps, intro conjI allI impI)
show "si ?i'' = si' m'" unfolding sii'' ..
next
show "si i = si' 0" unfolding sii ..
next
fix i
assume i: "i < m'"
show "valid_step (si' i) (ri' i) (si' (Suc i))"
proof (cases "i < mf")
case True
with stepsf[OF this]
show ?thesis unfolding ri' by (auto simp: R_all_def)
next
case False
with stepsr[OF this i] i
show ?thesis unfolding ri' by (auto simp: R_all_def)
qed
qed
show ?thesis
proof (intro exI conjI, rule conv, unfold ci, intro allI impI)
fix j
assume j: "j < m'"
show "(?ci, c (si' j) (ri' j) (si' (Suc j))) ∈ C" (is "(_, ?c) ∈ C")
proof (cases "j < mf")
case True
hence c: "?c = ([si' j], orule (lrf j))"
unfolding ri' by simp
from smallf[OF True] have "(si ?i', si' j) ∈ S" .
thus ?thesis unfolding c C_def by auto
next
case False
from False have "j = mf + (j - mf)" by simp
then obtain k where jk: "j = mf + k" by simp
with j[unfolded m'] have kmr: "mr - k - Suc 0 < mr" by arith
from j[unfolded m'] kmr jk
have id: "mf + mr - (mr - k - Suc 0) = Suc (mf + k)" by auto
from False have c: "?c = ([si' (Suc j)], orule (lrr (mr + mf - Suc j)))"
unfolding ri' by simp
have "(si ?i', si' (Suc j)) ∈ S" using smallg[OF kmr]
unfolding jk id by auto
thus ?thesis unfolding c C_def by auto
qed
qed
next
assume "¬ ?join ∧ ?cp"
then obtain D b l r σ where id: "si ?i = D⟨l ⋅ σ⟩" "si ?i'' = D⟨r ⋅ σ⟩"
and mem: "((b, l, r) ∈ ?CP ∨ (b, r, l) ∈ ?CP)"
and njoin: "¬ ?join" by force
{
assume "(l, r) ∈ (rstep (R n))⇧↓" (is "_ ∈ ?R⇧↓")
then obtain u where lu: "(l, u) ∈ ?R⇧*" and ru: "(r, u) ∈ ?R⇧*"
by auto
note Dσ = rsteps_closed_ctxt[OF rsteps_closed_subst[of _ _ _ σ], of _ _ _ D]
from Dσ[OF lu] Dσ[OF ru] njoin have False unfolding id by auto
} note njoin = this
let ?si' = "λ i' :: nat. case i' of 0 ⇒ si ?i | _ ⇒ si ?i''"
from mem
show ?thesis
proof
assume cp: "(b, l, r) ∈ ?CP"
from fair[OF cp] njoin have lr: "(l, r) ∈ E_all"
unfolding E_all_def by auto
let ?ri' = "λ i' :: nat. ((l, r), None)"
have conv: "comp_conversion (si ?i) (Suc 0, ?si', ?ri') (si ?i'')"
unfolding id using lr by auto
have C0: "(?ci, c (?si' 0) (?ri' 0) (?si' (Suc 0))) ∈ C"
using i'i i'i''
by (auto simp: C_def id)
show ?thesis
by (intro exI conjI, rule conv, insert C0, auto simp: ci)
next
assume cp: "(b, r, l) ∈ ?CP"
from fair[OF cp] njoin have lr: "(r, l) ∈ E_all"
unfolding E_all_def by auto
let ?ri' = "λ i' :: nat. ((r, l), None)"
have conv: "comp_conversion (si ?i) (Suc 0, ?si', ?ri') (si ?i'')"
unfolding id using lr by auto
have C0: "(?ci, c (?si' 0) (?ri' 0) (?si' (Suc 0))) ∈ C"
using i'i i'i''
by (auto simp: C_def id)
show ?thesis
by (intro exI conjI, rule conv, insert C0, auto simp: ci)
qed
qed
qed
qed
qed
let ?comp = "comp_conversion"
let ?m = "mset"
note id = c
from main show ?thesis
proof
assume "∃ i < m. ?smaller i"
then obtain i where i: "i < m" and small: "?smaller i" by auto
let ?c = "c (si i) (ri i) (si (Suc i))"
let ?split = "conversion_split_three (m, si, ri) i (Suc i)"
obtain bef cc aft where csplit: "?split = (bef, cc, aft)" by (cases ?split, force)
from i have "i ≤ Suc i" "Suc i ≤ m" by auto
from conversion_split_three[OF cconv this csplit]
have bef: "?comp s bef (si i)"
and aft: "?comp (si (Suc i)) aft t"
and cost_old: "cost (m, si, ri) = cost bef @ [?c] @ cost aft" by auto
from small obtain m' si' ri' where c: "comp_conversion (si i) (m', si', ri') (si (Suc i))"
and small: "⋀ i'. i' < m' ⟹ (?c,
c (si' i') (ri' i') (si' (Suc i'))) ∈ C" by blast
let ?merge = "conversion_merge_three bef (m', si', ri') aft"
from conversion_merge_three[OF bef c aft]
have conv: "?comp s ?merge t"
and cost_new: "cost ?merge = cost bef @ cost (m', si', ri') @ cost aft" by auto
let ?bef = "?m (cost bef)"
let ?aft = "?m (cost aft)"
let ?old = "?m [?c]"
let ?new = "?m (cost (m', si', ri'))"
show ?thesis unfolding id
proof (intro exI conjI, rule conv, unfold Cost_def, rule, unfold split,
unfold cost_old cost_new mset_append)
have "(?bef + (?new + ?aft), ?bef + (?old + ?aft)) ∈ mult1 (C¯)" (is "(?l, ?r) ∈ _")
unfolding mult1_def
proof (rule, unfold split, intro exI conjI allI impI)
have "?r = (?bef + ?aft) + {#?c#}" by (simp add: ac_simps)
then show "mset (cost bef) + (mset [c (si i) (ri i) (si (Suc i))] +
mset (cost aft)) = add_mset (c (si i) (ri i) (si (Suc i))) (mset (cost bef) +
mset (cost aft))"
by auto
next
show "?l = (?bef + ?aft) + ?new" by (simp add: ac_simps)
next
fix b
assume "b ∈# ?new"
hence "b ∈ set (cost (m', si', ri'))" unfolding in_multiset_in_set .
from this[unfolded cost.simps set_map] obtain j
where j: "j ∈ set [0..<m']" and b: "b = c (si' j) (ri' j) (si' (Suc j))"
by auto
from j have j: "j < m'" by auto
from small[OF j]
show "(b, ?c) ∈ C¯" unfolding b by simp
qed
thus "(?l, ?r) ∈ mult (C¯)" unfolding mult_def by auto
qed
next
assume "∃ i. Suc i < m ∧ ?smaller2 i"
then obtain i where i: "Suc i < m" and small: "?smaller2 i" by auto
let ?c = "c (si i) (ri i) (si (Suc i))"
let ?c' = "c (si (Suc i)) (ri (Suc i)) (si (Suc (Suc i)))"
let ?split = "conversion_split_three (m, si, ri) i (Suc (Suc i))"
obtain bef cc aft where csplit: "?split = (bef, cc, aft)" by (cases ?split, force)
have id': "2 = Suc (Suc 0)" by simp
from i have "i ≤ Suc (Suc i)" "Suc (Suc i) ≤ m" by auto
from conversion_split_three[OF cconv this csplit]
have bef: "?comp s bef (si i)"
and aft: "?comp (si (Suc (Suc i))) aft t"
and cost_old: "cost (m, si, ri) = cost bef @ [?c, ?c'] @ cost aft" by (auto simp: id')
from small obtain m' si' ri' where c: "comp_conversion (si i) (m', si', ri') (si (Suc (Suc i)))"
and small: "⋀ i'. i' < m' ⟹ (?c,
c (si' i') (ri' i') (si' (Suc i'))) ∈ C" by blast
let ?merge = "conversion_merge_three bef (m', si', ri') aft"
from conversion_merge_three[OF bef c aft]
have conv: "?comp s ?merge t"
and cost_new: "cost ?merge = cost bef @ cost (m', si', ri') @ cost aft" by auto
let ?bef = "?m (cost bef)"
let ?aft = "?m (cost aft)"
let ?old = "?m [?c, ?c']"
let ?mid = "?m [?c]"
let ?new = "?m (cost (m', si', ri'))"
show ?thesis unfolding id
proof (intro exI conjI, rule conv, unfold Cost_def, rule, unfold split,
unfold cost_old cost_new mset_append)
have "(?bef + (?new + ?aft), ?bef + (?mid + ?aft)) ∈ mult1 (C¯)" (is "(?l, ?z) ∈ _")
unfolding mult1_def
proof (rule, unfold split, intro exI conjI allI impI)
have "?z = (?bef + ?aft) + {#?c#}" by (simp add: ac_simps)
then show "mset (cost bef) + (mset [c (si i) (ri i) (si (Suc i))] + mset (cost aft)) =
add_mset (c (si i) (ri i) (si (Suc i))) (mset (cost bef) +
mset (cost aft))" by auto
next
show "?l = (?bef + ?aft) + ?new" by (simp add: ac_simps)
next
fix b
assume "b ∈# ?new"
hence "b ∈ set (cost (m', si', ri'))" unfolding in_multiset_in_set .
from this[unfolded cost.simps set_map] obtain j
where j: "j ∈ set [0..<m']" and b: "b = c (si' j) (ri' j) (si' (Suc j))"
by auto
from j have j: "j < m'" by auto
from small[OF j]
show "(b, ?c) ∈ C¯" unfolding b by simp
qed
also have "(?z, ?bef + (?old + ?aft)) ∈ mult1 (C¯)" (is "(_, ?r) ∈ _")
unfolding mult1_def
by (rule, unfold split, rule exI[of _ ?c'], rule exI[of _ ?z], rule exI[of _ "{#}"], auto simp: ac_simps)
finally
show "(?l, ?r) ∈ mult (C¯)" unfolding mult_def .
qed
qed
qed
lemma SN_C: "SN C"
unfolding C_def
proof (rule lex_two[OF _ _ SN_nat_gt])
have "SN {(a, a'). (mset a', mset a) ∈ mult1 (S¯)} =
wf {(a', a). (mset a', mset a) ∈ mult1 (S¯)}" (is "?goal = _")
unfolding SN_iff_wf converse_unfold by auto
also have "..."
using wf_inv_image[OF wf_mult1[OF SN[unfolded SN_iff_wf]], of mset]
unfolding inv_image_def .
finally show ?goal .
qed auto
lemma Cost_SN: "SN Cost"
proof -
have "SN Cost = wf {(b, a). (mset (cost b), mset (cost a)) ∈ mult (C¯)}"
unfolding Cost_def SN_iff_wf converse_unfold
by auto
also have "..."
using wf_inv_image[OF wf_mult[OF SN_C[unfolded SN_iff_wf]], of "λ x. mset (cost x)"]
unfolding inv_image_def .
finally show ?thesis .
qed
lemma conversion_imp_join:
assumes conv: "comp_conversion s conv t"
shows "(s, t) ∈ (rstep (R n))⇧↓"
proof -
from conv have "∃ conv. comp_conversion s conv t ∧ rewrite_conversion conv"
proof (induct conv rule: SN_induct[OF Cost_SN])
case (1 conv)
show ?case
proof (cases "rewrite_conversion conv")
case True
show ?thesis
by (intro exI conjI, rule 1(2), rule True)
next
case False
from proof_simplification[OF 1(2) False]
obtain conv' where conv: "comp_conversion s conv' t" and rel: "(conv, conv') ∈ Cost" by blast
from 1(1)[OF rel conv] show ?thesis .
qed
qed
then obtain conv where conv: "comp_conversion s conv t"
and rewr: "rewrite_conversion conv" by blast
show ?thesis
by (rule rewrite_conversion_imp_join[OF conv rewr])
qed
lemma Rn_CR: "CR (rstep (R n))"
proof (rule Newman[OF Rn_SN], unfold critical_pair_lemma, clarify)
fix b l r
assume cp: "(b, l, r) ∈ critical_pairs (R n) (R n)"
show "(l, r) ∈ (rstep (R n))⇧↓"
proof (rule ccontr)
assume njoin: "¬ ?thesis"
from fair[OF cp] njoin have lr: "(l, r) ∈ E_all" unfolding E_all_def by auto
let ?si = "λ i :: nat. if i = 0 then l else r"
let ?ri = "λ i :: nat. ((l, r), None)"
have "comp_conversion l (Suc 0, ?si, ?ri) r" using lr by auto
from conversion_imp_join[OF this] njoin
show False by simp
qed
qed
lemmas completion_sound = E0_Rn_conversion Rn_SN Rn_CR
end
end