section "Decreasing Diagrams2"
theory Decreasing_Diagrams2
imports
"Decreasing-Diagrams-II.Decreasing_Diagrams_II"
"Check-NT.Critical_Pairs"
begin
text ‹ARSs whose relation is the union of an indexed set of relations.›
definition ds :: "'a rel ⇒ 'a set ⇒ 'a set"
where "ds r S = {y . ∃x ∈ S. (y,x) ∈ r}"
lemma ds_to_under[simp]: "ds r {a} = under r a" "ds r {a,b} = under r a ∪ under r b"
by (auto simp: ds_def under_def)
definition fars_ld :: "'a rel ⇒ ('a ⇒ 'b rel) ⇒ 'a set ⇒ bool"
where "fars_ld gt r I = (∀ a ∈ I. ∀ b ∈ I. ∀ x y z. (x,y) ∈ r a ∧ (x,z) ∈ r b ⟶ (∃ y1 y2 z1 z2 v.
( (y,y1) ∈ (⋃c∈under gt a. r c)⇧* ∧ ((y1,y2) ∈ (r b)⇧=) ∧ (y2,v) ∈ (⋃c∈under gt a ∪ under gt b. r c)⇧* ∧
(z,z1) ∈ (⋃c∈under gt b. r c)⇧* ∧ ((z1,z2) ∈ (r a)⇧=) ∧ (z2,v) ∈ (⋃c∈under gt a ∪ under gt b. r c)⇧*)))"
definition fars_eld :: "'a rel ⇒ 'a rel ⇒ ('a ⇒ 'b rel) ⇒ bool"
where "fars_eld gt ge r = ((∀ x y z a b. (x,y) ∈ r a ∧ (x,z) ∈ r b ⟶ (∃ y1 y2 z1 z2 v.
((y,y1) ∈ ((⋃c∈under gt a. r c)⇧↔)⇧* ∧ (y1,y2) ∈ (⋃c∈under ge b. r c)⇧= ∧ (y2,v) ∈ ((⋃c∈under gt a ∪ under gt b. r c)⇧↔)⇧* ∧
(z,z1) ∈ ((⋃c∈under gt b. r c)⇧↔)⇧* ∧ (z1,z2) ∈ (⋃c∈under ge a. r c)⇧= ∧ (z2,v) ∈ ((⋃c∈under gt a ∪ under gt b. r c)⇧↔)⇧*))))"
definition rel_props :: "'a rel ⇒ 'a rel ⇒ bool"
where "rel_props gt ge ⟷ trans gt ∧ trans ge ∧ wf gt ∧ refl ge ∧ ge O gt O ge ⊆ gt"
lemma fars_eld_imp_cr:
assumes rp: "rel_props gt ge" and pk: "fars_eld gt ge r"
shows "CR (⋃c ∈ UNIV. r c)"
proof (induct rule: edd_cr[of gt ge])
case (peak a b s t u)
then have *: "(t,u) ∈ ((⋃c∈under gt a. r c)⇧↔)⇧* O (⋃c∈under ge b. r c)⇧= O
((⋃c∈under gt a ∪ under gt b. r c)⇧↔)⇧* O (((⋃c∈under gt b. r c)⇧↔)⇧* O (⋃c∈under ge a. r c)⇧= O
((⋃c∈under gt a ∪ under gt b. r c)⇧↔)⇧*)¯" using pk[unfolded fars_eld_def, rule_format, of s t a u b] by blast
show ?case by (intro subsetD[OF _ *]) (unfold converse_inward, regexp)
qed (insert rp, auto simp: rel_props_def refl_on_def)
type_synonym ('f,'v) step = "('f,'v) term × ('f,'v) rule × pos × ('f,'v) subst × bool × ('f,'v) term"
type_synonym ('f,'v) lpeak = "('f,'v) step × ('f,'v) step"
type_synonym ('f,'v) join = "('f,'v) step list × ('f,'v) step list"
type_synonym ('f,'v,'a) labeling = "('f,'v) step ⇒ 'a"
definition get_source :: "('f,'v) step ⇒ ('f,'v) term"
where "get_source s = fst s"
definition get_rule :: "('f,'v) step ⇒ ('f,'v) rule"
where "get_rule s = fst (snd s)"
definition get_pos :: "('f,'v) step ⇒ pos"
where "get_pos s = fst (snd (snd s))"
definition get_subst :: "('f,'v) step ⇒ ('f,'v) subst"
where "get_subst s = fst (snd (snd (snd s)))"
definition get_target :: "('f,'v) step ⇒ ('f,'v) term" where
"get_target step = (case step of
(s, r, p, σ, s_to_t, t) ⇒ if s_to_t then t else s)"
lemma rstep_r_p_s_ctxt_closed2:
assumes "(s,t) ∈ rstep_r_p_s R rl p σ"
shows "(C⟨s⟩,C⟨t⟩) ∈ rstep_r_p_s R rl (hole_pos C<#>p) σ"
using assms by (auto simp: Let_def rstep_r_p_s_def ctxt_of_pos_term_append)
lemma rstep_r_p_s_ctxt_closed:
assumes "(s,t) ∈ rstep_r_p_s R rl p σ" and "q ∈ poss u"
shows "((ctxt_of_pos_term q u)⟨s⟩,(ctxt_of_pos_term q u)⟨t⟩) ∈ rstep_r_p_s R rl (q<#>p) σ"
using rstep_r_p_s_ctxt_closed2[OF assms(1)] assms(2)
by (auto simp: rstep_r_p_s_def Let_def replace_at_below_poss replace_at_subt_at)
(metis hole_pos_ctxt_of_pos_term[OF assms(2)])+
lemma rstep_r_p_s_subst_closed:
assumes "(s, t) ∈ rstep_r_p_s R rl p τ"
shows "(s ⋅ σ, t ⋅ σ) ∈ rstep_r_p_s R rl p (τ ∘⇩s σ)"
using assms unfolding rstep_r_p_s_def'
by (auto simp add: ctxt_of_pos_term_subst)
fun step_close:: "('f,'v) step ⇒ ('f,'v) ctxt ⇒ ('f,'v) subst ⇒ ('f,'v) step"
where "step_close (s, rl, p, σ, b, t) C τ = (C⟨s ⋅ τ⟩, rl, hole_pos C <#> p, σ ∘⇩s τ, b, C⟨t ⋅ τ⟩)"
type_synonym ('f,'v) seq = "('f,'v) term × ('f,'v) step list"
inductive_set seq :: "('f,'v) trs ⇒ ('f,'v) seq set"
for ℛ where
"(s,[]) ∈ seq ℛ"
| "(s,t) ∈ rstep_r_p_s ℛ r p σ ⟹ (t,ts) ∈ seq ℛ ⟹ (s, (s,r,p,σ,True,t) # ts) ∈ seq ℛ"
lemma rstep_is_seq:
assumes "(s,t) ∈ rstep_r_p_s R r p σ"
shows "(s,[(s,r,p,σ,True,t)]) ∈ seq R"
using assms seq.intros by blast
fun first :: "('f,'v) seq ⇒ ('f,'v) term"
where "first (s,_) = s"
fun last :: "('f,'v) seq ⇒ ('f,'v) term"
where
"last (s, []) = s"
| "last (s, step # ss) = last (get_target step, ss)"
lemma seq_chop_first:
assumes "(s,(s,rl,p,σ,True,t) # ss) ∈ seq R"
shows "(t,ss) ∈ seq R" and "(s,t) ∈ rstep_r_p_s R rl p σ"
using assms seq.cases by auto
fun seq_close :: "('f,'v) seq ⇒ ('f,'v) ctxt ⇒ ('f,'v) subst ⇒ ('f,'v) seq"
where "seq_close ss C τ = (C⟨fst ss ⋅ τ⟩, map (λstep. step_close step C τ) (snd ss))"
definition seq_concat :: "('f,'v) seq ⇒ ('f,'v) seq ⇒ ('f,'v) seq"
where "seq_concat σ1 σ2 = (first σ1, snd σ1 @ snd σ2)"
lemma seq_concat_seq_close:
shows "seq_close (seq_concat ts us) C τ = seq_concat (seq_close ts C τ) (seq_close us C τ)"
proof -
obtain t tq u uq where ts_dec: "ts = (t,tq)" and us_dec: "us = (u,uq)"
by (cases ts, cases us, auto)
thus ?thesis unfolding seq_concat_def by auto
qed
lemma seq_concat_labels:
shows "map l (snd (seq_concat ts us)) = (map l (snd ts)) @ (map l (snd us))"
proof -
obtain t tq u uq where ts_dec: "ts = (t,tq)" and us_dec: "us = (u,uq)"
by (cases ts, cases us, auto)
show ?thesis unfolding seq_concat_def by auto
qed
lemma seq_dec:
assumes "ss ∈ seq R"
and "map l (snd ss) = l1 @ l2"
shows "∃ L1 L2. ss = seq_concat L1 L2 ∧ L1 ∈ seq R ∧ L2 ∈ seq R ∧ map l (snd L1) = l1 ∧
(map l (snd L2) = l2) ∧ first ss = first L1 ∧ last L1 = first L2 ∧ last L2 = last ss"
using assms
proof (induct l1 arbitrary: ss)
case Nil
hence L1: "(first ss, []) ∈ seq R" (is "?L1 ∈ _") by (auto intro: seq.intros)
hence "ss = seq_concat ?L1 ss" by (cases ss) (auto simp: seq_concat_def)
then show ?case using Nil L1 by (cases ss) (auto)
next
case (Cons a ls)
then obtain s step ts where ss_dec: "ss = (s,step#ts)" by (cases ss, auto)
with Cons(2) have "(s,step#ts) ∈ seq R" by auto
then obtain rl p σ t where step_dec: "step = (s,rl,p,σ,True,t)" by (cases, auto)
hence step: "(s,t) ∈ rstep_r_p_s R rl p σ" using Cons(2)
unfolding ss_dec step_dec using seq.cases by auto
have i1:"(t,ts) ∈ seq R" using Cons(2) seq_chop_first(1) unfolding ss_dec step_dec by fast
have i2:"map l (snd (t,ts)) = ls@l2" using Cons(3) Cons unfolding ss_dec step_dec by auto
from Cons(1)[OF i1 i2] obtain L1 L2 where
IH: "(t, ts) = seq_concat L1 L2" "L1 ∈ seq R" "L2 ∈ seq R"
"map l (snd L1) = ls" "map l (snd L2) = l2"
"first (t, ts) = first L1" "last L1 = first L2" "last L2 = last (t, ts)" by fast
have t: "first L1 = t" using IH(1) unfolding seq_concat_def by auto
have f1: "ss = seq_concat (s,step # snd L1) L2" using IH(1)
unfolding ss_dec step_dec seq_concat_def by auto
have f2: "(s,step # snd L1) ∈ seq R"
unfolding step_dec using seq.intros(2)[OF step] IH(2) t
by (metis first.cases first.simps snd_conv step_dec)
have f4: "map l (snd (s,step# snd L1)) = a # ls"
using IH(4) Cons(3) unfolding ss_dec step_dec by auto
have e1: "first ss = first ((s, step # snd L1))" unfolding ss_dec by auto
have e2: "last (s,step#snd L1) = first L2"
using IH step_dec apply (auto simp add: get_target_def)
by (metis first.simps surjective_pairing)
have e3: "last L2 = last ss"
unfolding ss_dec step_dec last.simps get_target_def using IH by auto
show ?case using f1 f2 IH(3) f4 IH(5) using e1 e2 e3 by metis
qed
lemma seq_close_length: "length (snd ss) = length (snd (seq_close ss C τ))" by auto
lemma step_super_closed1: "get_target (step_close step C σ) = C⟨get_target step ⋅ σ⟩"
unfolding get_target_def Let_def by (cases step, simp)
lemma seq_super_closed1:
assumes seq:"ss ∈ seq R"
shows "seq_close ss C σ ∈ seq R ∧ (first (seq_close ss C σ)) = C⟨first ss ⋅ σ⟩ ∧
last (seq_close ss C σ) = C⟨last ss ⋅ σ⟩"
using seq
proof (induct "snd ss" arbitrary: ss)
case Nil then obtain s where ss_dec: "ss = (s,[])" by (cases ss, auto)
thus ?case using seq.intros unfolding ss_dec by auto
next
case (Cons step ts)
from Cons(2) obtain s where ss_dec: "ss=(s,step#ts)" by (cases ss, auto)
with Cons(3) obtain rl p τ t where step_dec: "step=(s,rl,p,τ,True,t)" by (auto elim: seq.cases)
hence step: "(s,t) ∈ rstep_r_p_s R rl p τ" and i:"(t,ts) ∈ seq R" (is "?ts ∈ _")
using Cons(3) seq.cases unfolding ss_dec step_dec by auto
from Cons(1)[OF _ i] have ih:
"seq_close ?ts C σ ∈ seq R" "(first (seq_close ?ts C σ)) = (C⟨first ?ts⋅σ⟩)"
"last (seq_close ?ts C σ) = C⟨last ?ts⋅σ⟩"
by auto
have C_step: "(C⟨s⋅σ⟩,C⟨t⋅σ⟩) ∈ rstep_r_p_s R rl (hole_pos C<#>p) (τ∘⇩s σ)"
using rstep_r_p_s_ctxt_closed2[OF rstep_r_p_s_subst_closed[OF step]] by auto
hence C_seq: "(seq_close ss C σ) ∈ seq R"
using ih(1) seq.intros(2)[OF C_step] unfolding ss_dec step_dec by auto
hence C_first: "first (seq_close ss C σ) = C⟨first ss⋅σ⟩" unfolding ss_dec step_dec by auto
have "last (seq_close ?ts C σ) = C⟨last ?ts⋅σ⟩" using ih by auto
hence C_last: "last (seq_close ss C σ) = C⟨last ss⋅σ⟩"
unfolding ss_dec seq_close.simps last.simps fst_conv snd_conv
list.map get_target_def step_dec by auto
show ?case using C_seq C_first C_last by auto
qed
definition local_peaks :: "('f,string) trs ⇒ (('f,string) lpeak) set"
where "local_peaks ℛ = {((s,r⇩1,p⇩1,σ⇩1,True,t),(s,r⇩2,p⇩2,σ⇩2,True,u)) | s t u r⇩1 r⇩2 p⇩1 p⇩2 σ⇩1 σ⇩2.
(s,t) ∈ rstep_r_p_s ℛ r⇩1 p⇩1 σ⇩1 ∧ (s,u) ∈ rstep_r_p_s ℛ r⇩2 p⇩2 σ⇩2}"
definition critical_peaks :: "('f,string) trs ⇒ (bool × ('f,string) lpeak) set"
where "critical_peaks ℛ = {(C = □, (l ⋅ σ, (l, r), ε, σ, True, r ⋅ σ), (l ⋅ σ, (l', r'), hole_pos C, τ, True, (C ⋅⇩c σ)⟨r' ⋅ τ⟩)) | l r l' r' l'' C σ τ.
(l, r) ∈ ℛ ∧ (l', r') ∈ ℛ ∧ l = C⟨l''⟩ ∧ is_Fun l'' ∧
mgu_var_disjoint_string l'' l' = Some (σ, τ) }"
lemma critical_peak_is_local_peak:
assumes "(b,s1,s2) ∈ critical_peaks R"
shows "(s1,s2) ∈ local_peaks R"
using assms
unfolding critical_peaks_def local_peaks_def rstep_r_p_s_def
by auto (metis ctxt_of_pos_term_hole_pos hole_pos_subst mgu_var_disjoint_generic_sound)+
lemma critical_peaksI:
assumes "(l, r) ∈ R" and "(l', r') ∈ R" and "l = C⟨l''⟩"
and "is_Fun l''" and "mgu_var_disjoint_string l'' l' = Some (σ, τ)" and "s = r ⋅ σ"
and "t = (C ⋅⇩c σ)⟨r' ⋅ τ⟩" and "b = (C = □)"
shows "(b, (l ⋅ σ, (l, r), ε, σ, True, s), (l ⋅ σ, (l', r'), hole_pos C, τ, True, t)) ∈ critical_peaks R"
using assms unfolding critical_peaks_def by blast
lemma critical_peak_to_critical_pair:
assumes "(b,s1,s2) ∈ critical_peaks R"
shows "(b, get_target s1,get_target s2) ∈ critical_pairs R R"
using assms
unfolding critical_peaks_def critical_pairs_def get_target_def
by fastforce
definition parallel_peak :: "('f,string) trs ⇒ (('f,string) lpeak) ⇒ bool"
where "parallel_peak ℛ p = (
p ∈ local_peaks ℛ ∧
(let ((s,r⇩1,p⇩1,σ⇩1,b,t),(s,r⇩2,p⇩2,σ⇩2,d,u)) = p in parallel_pos p⇩1 p⇩2)
)"
definition variable_peak :: "('f,string) trs ⇒ (('f,string) lpeak) ⇒ bool"
where "variable_peak ℛ p = (
p ∈ local_peaks ℛ ∧
(let ((s,rl⇩1,p⇩1,σ⇩1,b,t),(s,rl⇩2,p⇩2,σ⇩2,d,u)) = p in
∃ r. ((p⇩1 <#> r = p⇩2) ∧ ¬ (r ∈ poss (fst rl⇩1) ∧ is_Fun ((fst rl⇩1) |_ r)))
))"
definition function_peak :: "('f,string) trs ⇒ ('f,string) lpeak ⇒ bool"
where "function_peak ℛ p = (
p ∈ local_peaks ℛ ∧
(let ((s,rl⇩1,p⇩1,σ⇩1,b,t),(s,rl⇩2,p⇩2,σ⇩2,d,u)) = p in
∃ r. ((p⇩1 <#> r = p⇩2) ∧ r ∈ poss (fst rl⇩1) ∧ is_Fun ((fst rl⇩1) |_ r)))
)"
lemma function_peak_inst_of_critical_peak:
assumes "function_peak R p"
shows "∃ C δ b cp. (b,cp) ∈ critical_peaks R ∧ p = (step_close (fst cp) C δ, step_close (snd cp) C δ)"
proof -
from assms obtain s l1 r1 p1 σ1 t l2 r2 p2 σ2 u v where
p: "p = ((s, (l1, r1), p1, σ1, True, t), (s, (l2, r2), p2, σ2, True, u))" and
st:"(s,t) ∈ rstep_r_p_s R (l1, r1) p1 σ1" and
su:"(s,u) ∈ rstep_r_p_s R (l2, r2) p2 σ2" and
v:"p1 <#> v = p2" and vl1:"v ∈ poss l1" and l1v:"is_Fun (l1 |_ v)"
unfolding function_peak_def local_peaks_def by auto
from st su have
p1: "p1 ∈ poss s" and σ1: "s |_ p1 = l1 ⋅ σ1" and
t: "t = replace_at s p1 (r1 ⋅ σ1)" and lr1: "(l1,r1) ∈ R" and
p2: "p2 ∈ poss s" and σ2: "s |_ p2 = l2 ⋅ σ2" and
u: "u = replace_at s p2 (r2 ⋅ σ2)" and lr2: "(l2,r2) ∈ R"
unfolding rstep_r_p_s_def' by auto
from v have l2v: "(l1 ⋅ σ1) |_ v = l2 ⋅ σ2" using σ1 σ2 p1 by auto
from l2v subt_at_subst[OF vl1] have "l1 |_ v ⋅ σ1 = l2 ⋅ σ2" by metis
from mgu_var_disjoint_string_complete[OF this]
obtain μ1 μ2 δ where mgu: "mgu_var_disjoint_string (l1 |_ v) l2 = Some (μ1, μ2)"
and d1:"σ1 = μ1 ∘⇩s δ" and d2:"σ2 = μ2 ∘⇩s δ" and mu12:"l1 |_v ⋅ μ1 = l2 ⋅ μ2"
by fast
let ?s' = "l1 ⋅ μ1"
let ?t' = "r1 ⋅ μ1"
let ?C' = "ctxt_of_pos_term v l1"
let ?u' = "(?C' ⋅⇩c μ1)⟨r2 ⋅ μ2⟩"
let ?C = "ctxt_of_pos_term p1 s"
from p1 σ1 d1 have s_inst:"?C⟨?s' ⋅ δ⟩ = s" using replace_at_ident by simp
from d1 t have t_inst:"t = ?C⟨?t' ⋅ δ⟩" using replace_at_ident by simp
from u v[symmetric] d2 ctxt_of_pos_term_append[OF p1] σ1 d1
have u_inst: "?C⟨?u' ⋅ δ⟩ = u" apply simp
unfolding ctxt_of_pos_term_subst[OF vl1] subst_subst
by simp
have "v = hole_pos ?C'" by (metis hole_pos_ctxt_of_pos_term vl1)
with critical_peaksI[OF lr1 lr2 _ l1v mgu, of ?C' ?t' ?u' "?C' = □"] ctxt_supt_id[OF vl1]
have "(?C' = □, (?s', (l1, r1), ε, μ1, True, ?t') ,(?s', (l2, r2), v, μ2, True, ?u')) ∈ critical_peaks R"
(is "(?b, ?cp) ∈ _") by auto
moreover have "p = (step_close (fst ?cp) ?C δ, step_close (snd ?cp) ?C δ)"
unfolding p using s_inst p1 d1 d2 v u_inst t_inst by simp
ultimately show ?thesis by fast
qed
lemma mirror:
assumes "p ∈ local_peaks R"
shows "(snd p,fst p) ∈ local_peaks R"
using assms unfolding local_peaks_def by auto
lemma local_peaks_helper:
assumes pos: "p1 ≤ p2"
and p: "((s,r1,p1,σ1,t),(s,r2,p2,σ2,u)) ∈ local_peaks R" (is "?p ∈ _")
shows "variable_peak R ?p ∨ function_peak R ?p"
proof -
from pos obtain r where "(p1 <#> r) = p2" using prefix_pos_diff by fast
thus ?thesis using p unfolding variable_peak_def function_peak_def by auto
qed
lemma local_peaks_cases:
assumes p: "p ∈ local_peaks ℛ"
shows "parallel_peak ℛ p ∨ variable_peak ℛ p ∨ variable_peak ℛ (snd p, fst p) ∨ function_peak ℛ p ∨ function_peak ℛ (snd p, fst p)"
proof -
from assms obtain s t u r1 r2 p1 p2 σ1 σ2 where
"(s,t) ∈ rstep_r_p_s ℛ r1 p1 σ1 ∧ (s,u) ∈ rstep_r_p_s ℛ r2 p2 σ2" and
p_dec: "p = ((s,r1,p1,σ1,True,t),(s,r2,p2,σ2,True,u))"
unfolding local_peaks_def by fast
thus ?thesis
proof (cases "parallel_pos p1 p2")
case True
hence "parallel_peak ℛ p"
using p unfolding parallel_peak_def p_dec Let_def by auto
thus ?thesis by auto
next
case False note F = this
thus ?thesis
proof (cases "p1 ≤ p2")
case True thus ?thesis using local_peaks_helper p p_dec by fast
next
case False
hence "p2 ≤ p1" using F parallel_pos by auto
thus ?thesis using local_peaks_helper mirror p p_dec by (metis fst_conv snd_conv)
qed
qed
qed
lemma variable_peak_decompose:
assumes "variable_peak R p"
shows "∃ s t u l1 r1 p1 σ1 l2 r2 p2 σ2 q q1 q2 w. (
p = ((s,(l1,r1),p1,σ1,True,t),(s,(l2,r2),p2,σ2,True,u)) ∧
(s,t) ∈ rstep_r_p_s R (l1, r1) p1 σ1 ∧
(s,u) ∈ rstep_r_p_s R (l2, r2) p2 σ2 ∧
p1 <#> q = p2 ∧
(q1<#> q2) = q ∧
q1 ∈ poss l1 ∧
l1 |_ q1 = Var w)"
proof -
from assms obtain s rl1 p1 s1 t rl2 p2 s2 u q where
p: "p ∈ local_peaks R" and
p_dec: "p = ((s,rl1,p1,s1,True,t),(s,rl2,p2,s2,True,u))" and
q:"p1 <#> q = p2" and
px: "¬ (q ∈ poss (fst rl1) ∧ is_Fun ((fst rl1) |_ q))"
unfolding variable_peak_def local_peaks_def Let_def by blast
then obtain l1 r1 l2 r2 where rl1: "(l1,r1) = rl1" and rl2: "(l2,r2) = rl2"
using surjective_pairing by metis
hence s1: "(s,t) ∈ rstep_r_p_s R (l1,r1) p1 s1" and s2:"(s,u) ∈ rstep_r_p_s R (l2,r2) p2 s2"
using p p_dec unfolding local_peaks_def by auto
have σ1: "s |_ p1 = l1 ⋅ s1" using s1 unfolding rl1[symmetric] rstep_r_p_s_def' by auto
have p2: "p2 ∈ poss s" using s2 unfolding rl2[symmetric] rstep_r_p_s_def' by auto
from px have py: "¬(q ∈ poss l1 ∧ is_Fun (l1 |_ q))" using rl1 by auto
from py obtain q1 q2 w where k: "q = q1<#>q2" and q1:"q1 ∈ poss l1" and w:"l1 |_ q1 = Var w"
using σ1 p2 pos_into_subst[of l1 s1 "s |_ p1" q] poss_append_poss q[symmetric] by auto
thus ?thesis using s1 s2 q p_dec rl1 rl2 by fast
qed
lemma variable_steps_lin:
assumes xy:"(x, y) ∈ rstep_r_p_s R (l1, r1) p1 σ1"
and xz:"(x, z) ∈ rstep_r_p_s R (l2, r2) p2 σ2"
and "p1 <#> v = p2"
and "(v1 <#> v2) = v" and "v1 ∈ poss l1" and "l1 |_ v1 = Var w"
and linl1: "linear_term l1"
defines "τ ≡ (λy. if y = w then replace_at (σ1 y) v2 (r2 ⋅ σ2) else σ1 y)"
defines "t ≡ (ctxt_of_pos_term p1 x)⟨r1 ⋅ τ⟩"
shows "(z, t) ∈ (rstep_r_p_s R (l1, r1) p1 τ)" (is "?g1")
"linear_term r1 ⟶ (
(y = t) ∨
(∃q. (q ∈ poss r1 ∧ (r1 |_ q = Var w) ∧ (y,t) ∈ (rstep_r_p_s R (l2,r2) (p1<#>q<#>v2) σ2))))" (is "?g2")
proof -
from xy[unfolded rstep_r_p_s_def']
have p1: "p1 ∈ poss x" and lr1: "(l1,r1) ∈ R" and σ1: "x |_ p1 = l1 ⋅ σ1"
and y: "y = replace_at x p1 (r1 ⋅ σ1)" by auto
from xz[unfolded rstep_r_p_s_def']
have p2: "p2 ∈ poss x" and lr2: "(l2,r2) ∈ R" and σ2: "x |_ p2 = l2 ⋅ σ2"
and z: "z = replace_at x p2 (r2 ⋅ σ2)" by auto
from assms(3) have v:"p2 = p1 <#> v" using less_eq_pos_def by auto
hence l2v:"(l1 ⋅ σ1) |_ v = l2 ⋅ σ2" using σ1 σ2 p1 p2 by auto
from v z σ1 have zp1:"z = replace_at x p1 (replace_at (l1 ⋅ σ1) v (r2 ⋅ σ2))"
using ctxt_of_pos_term_append[OF p1] ctxt_ctxt by force
from assms have v12: "v = v1 <#> v2" by auto
from assms have w: "l1 |_ v1 = Var w" by auto
from assms p2 have ths: "v ∈ poss (x |_ p1)" by auto
have v1: "v1 ∈ poss l1" using assms by auto
from assms have wv2: "σ1 w |_ v2 = l2 ⋅ σ2" using l2v by auto
have v1l1σ1:"v1 ∈ poss (l1 ⋅ σ1)" using v1 by simp
let ?cr = "replace_at x p1 (r1 ⋅ τ)"
from linear_term_replace_in_subst[OF linl1 v1 w, of σ1 τ, simplified]
have "l1 ⋅ τ = replace_at (l1 ⋅ σ1) v1 (τ w)" using τ_def by auto
also have "... = replace_at (l1 ⋅ σ1) v1 (replace_at (σ1 w) v2 (r2 ⋅ σ2))" using τ_def by auto
also have "... = replace_at (l1 ⋅ σ1) v (r2 ⋅ σ2)"
using v12 v1 w
ctxt_of_pos_term_append[OF v1l1σ1]
ctxt_ctxt by auto
finally have "l1 ⋅ τ = replace_at (l1 ⋅ σ1) v (r2 ⋅ σ2)" .
with zp1 have zp2: "z = replace_at x p1 (l1 ⋅ τ)" by auto
hence zcr:"(z, ?cr) ∈ rstep R" using subset_rstep lr1 by auto
have p1z: "p1 ∈ poss z" using zp1 by (metis less_eq_simps(1) p2 replace_at_below_poss v z)
have k: "ctxt_of_pos_term p1 x = ctxt_of_pos_term p1 z"
using ctxt_of_pos_term_replace_at_below[OF p1] zp2 by auto
have zcr: "(z,?cr) ∈ rstep_r_p_s R (l1,r1) p1 τ"
unfolding rstep_r_p_s_def Let_def
using p1z lr1 zp2 k by force
thus "?g1" unfolding t_def by auto
have g2a: "(w ∉ vars_term r1) ⟶ (y = ?cr)"
proof
assume A: "w ∉ vars_term r1"
show "y = ?cr"
proof -
from A have "r1 ⋅ τ = r1 ⋅ σ1" unfolding τ_def by (induct r1, auto)
hence "?cr = y" using y by auto
thus ?thesis by auto
qed
qed
have g2b: "w ∈ vars_term r1 ⟶ (linear_term r1 ⟶ (∃q. (q ∈ poss r1 ∧ (r1 |_ q = Var w) ∧
(y, ?cr) ∈ (rstep_r_p_s R (l2,r2) (p1<#>q<#>v2) σ2))))" (is "_ ⟶ (?l ⟶ ?s)")
proof
assume W: "w ∈ vars_term r1"
show "?l ⟶ ?s"
proof
assume linr1: "linear_term r1"
show "?s" proof -
from W obtain q where q: "q ∈ poss r1" and qw: "r1 |_ q = Var w"
using supteq_imp_subt_at[OF supteq_Var[OF W]] by auto
have qr1σ1:"q ∈ poss (r1 ⋅ σ1)" using q by simp
from linear_term_replace_in_subst[OF linr1 q qw, of σ1 τ, simplified]
have "r1 ⋅ τ = replace_at (r1 ⋅ σ1) q (τ w)" using τ_def by auto
also have "... = replace_at (r1 ⋅ σ1) q (replace_at (σ1 w) v2 (r2 ⋅ σ2))" using τ_def by auto
also have "... = replace_at (r1 ⋅ σ1) (q <#> v2) (r2 ⋅ σ2)"
using q qw ctxt_of_pos_term_append[OF qr1σ1] ctxt_ctxt by auto
finally have s3:"r1 ⋅ τ = replace_at (r1 ⋅ σ1) (q <#> v2) (r2 ⋅ σ2)" .
from wv2 qw have "(r1 ⋅ σ1) |_ (q <#> v2) = l2 ⋅ σ2"
using q subt_at_append[OF qr1σ1, of v2] by auto
hence ths: "r1 ⋅ σ1 = (ctxt_of_pos_term (q <#> v2) (r1 ⋅ σ1))⟨l2 ⋅ σ2⟩"
using qr1σ1 ctxt_supt_id σ1 p2 poss_append_poss q qw subt_at_subst v v1 v12 w using y by metis
have k: "(q<#>v2) ∈ poss (r1 ⋅ σ1)" using q
by (metis v12 w v1 σ1 p2 poss_append_poss qr1σ1 qw subst_apply_term.simps(1) subt_at_subst v)
from ths k lr2 have key: "(r1 ⋅ σ1, r1 ⋅ τ) ∈ rstep_r_p_s R (l2,r2) (q<#>v2) σ2"
unfolding s3 rstep_r_p_s_def Let_def by auto
hence r: "((ctxt_of_pos_term p1 x)⟨r1⋅σ1⟩,(ctxt_of_pos_term p1 x)⟨r1 ⋅ τ⟩) ∈ rstep_r_p_s R (l2,r2) (p1<#>q<#>v2) σ2"
using rstep_r_p_s_ctxt_closed p1 by auto
show ?thesis using q qw r unfolding y by auto
qed
qed
qed
show "?g2" using g2a g2b unfolding t_def by auto
qed
fun mapi :: "(nat ⇒ 'a ⇒ 'b) ⇒ nat ⇒ 'a list ⇒ 'b list" where
"mapi f i [] = []"
| "mapi f i (x # xs) = f i x # mapi f (i + 1) xs"
lemma append_mapi:
"mapi f n (xs @ ys) = mapi f n xs @ mapi f (n + length xs) ys"
by (induct xs arbitrary: n) simp_all
lemma length_mapi:
"length (mapi f n xs) = length xs"
by (induct xs arbitrary: n) simp_all
lemma length_concat_mapi:
"length (concat (mapi (λi. map (f i)) n xs)) = length (concat xs)"
by (induct xs arbitrary: n) simp_all
lemma concat_replicate_empty:
"concat (mapi (λi. map (f i)) n (replicate m [])) = []"
by (induct m arbitrary: n) simp_all
lemma mapi_nth:
assumes "i < length xs"
shows "(mapi f j xs) ! i = f (j + i) (xs ! i)"
using assms
by (induct i arbitrary: xs j) (case_tac[!] xs, auto)
lemma mapi_drop:
shows "drop i (mapi f j xs) = mapi f (j + i) (drop i xs)"
by (induct xs arbitrary: j i) (auto, case_tac i, auto)
lemma mapi_map_replicate_trivial:
shows "mapi (λi. map (f i)) j (replicate i []) = replicate i []"
by (induct i arbitrary: j) auto
lemma fst_concat_mapi1:
"map fst (concat xs) = map fst (concat (mapi (λi. map (λ(rl,p,σ). (rl,i<#p,σ))) n xs))"
by (induct xs arbitrary: n) auto
lemma fst_concat_mapi2:
assumes "∀i < length (concat steps). fst ((concat steps) ! i) = (l,r)"
shows "∀i < length (concat (mapi (λi. map (λ(rl, p, σ). (rl, i <# p, σ))) n steps)).
fst (concat (mapi (λi. map (λ(rl, p, σ). (rl, i <# p, σ))) n steps) ! i) = (l, r)"
proof (intro allI impI)
fix i
assume A: "i < length (concat (mapi (λi. map (λ(rl, p, σ). (rl, i <# p, σ))) n steps))"
have l: "i < length (concat steps)" using A length_concat_mapi by metis
have "map fst (concat steps) ! i = (l, r)" using nth_map l assms by auto
hence "map fst (concat (mapi (λi. map (λ(rl,p,σ). (rl, i <# p,σ))) n steps)) ! i = (l, r)"
using fst_concat_mapi1 l by metis
thus "fst (concat (mapi (λi. map (λ(rl, p, σ). (rl, i <# p, σ))) n steps) ! i) = (l, r)"
using nth_map A by auto
qed
lemma fst_concat_mapi3:
assumes "∀j < length steps. ∀i < length (steps ! j). fst (steps ! j ! i) = (l, r)"
shows "∀i < length (concat steps). fst ((concat steps) ! i) = (l, r)"
using assms
proof (induct steps)
case (Cons s ss)
show ?case
proof (intro allI impI)
fix i
assume A: "i < length (concat (s # ss))"
show "fst (concat (s # ss) ! i) = (l, r)"
proof (cases "i < length s")
case True
have "∀i < length s. fst (s ! i) = (l, r)" using Cons by auto
hence elt: "fst (s ! i) = (l, r)" using True by auto
from True have "s ! i = concat (s # ss) ! i" using nth_append[of s] by simp
thus ?thesis using elt by auto
next
case False
have k: "∀j < length ss. ∀i < length (ss ! j). fst (ss ! j ! i) = (l, r)" using Cons(2) by auto
have k2: "∀i < length s. fst (s ! i) = (l, r)" using Cons(2) by auto
hence k': "∀i < length (concat ss). fst (concat ss ! i) = (l, r)" using Cons(1)[OF k] by auto
have "i < length s + length (concat ss)" using k' False A by auto
hence "fst (concat ss ! (i - length s)) = (l, r)" using False k' by auto
thus ?thesis using k2 False using nth_append[of s] by simp
qed
qed
qed auto
lemma fst_concat_mapi:
assumes "∀j<length steps. ∀i<length (steps ! j). fst (steps ! j ! i) = (l, r)"
shows "∀i<length (concat (mapi (λi. map (λ(rl, p, σ). (rl, i <# p, σ))) n steps)).
fst (concat (mapi (λi. map (λ(rl, p, σ). (rl, i <# p, σ))) n steps) ! i) = (l, r)"
by (rule fst_concat_mapi2[OF fst_concat_mapi3[OF assms]])
lemma concat_singleton:
assumes "concat xs = [z]"
shows "(∃i < length xs. xs ! i = [z] ∧ (∀j < length xs. j ≠ i ⟶ (xs ! j) = []))"
using assms
proof (induct xs)
case (Cons x xs)
show ?case
proof (cases x)
case Nil
with Cons have "concat xs = [z]" by auto
with Cons obtain i where
len:"i<length xs" and
z:"xs ! i = [z]" and
nil:"∀j<length xs. j ≠ i ⟶ (xs ! j) = []"
by auto
let ?i = "Suc i"
from len have "?i<length (x # xs)"
by auto
moreover from z have "(x # xs) ! ?i = [z]" by auto
moreover have "∀j<length (x # xs). j ≠ ?i ⟶ (x # xs) ! j = []" using Nil nil
by (metis gr0_conv_Suc length_Cons linorder_neqE_nat not_less_eq nth_Cons' nth_Cons_Suc)
ultimately show ?thesis by auto
qed (insert Cons, auto)
qed auto
lemma concat_Cons:
assumes "concat xss = x # xs"
shows "∃i < length xss. ∃ys. (∀j < i. xss ! j = []) ∧
xss ! i = x # ys ∧ xs = ys @ concat (drop (Suc i) xss)"
using assms
proof (induct xss arbitrary: x xs)
case (Cons z zs)
show ?case
proof (cases "z = []")
case False
with Cons have x:"x = hd z" by (metis concat.simps(2) hd_append2 list.sel(1))
have "0 < length (z # zs)" by auto
moreover have "∀j < 0. (z # zs) ! j = []" by auto
moreover have "(z # zs) ! 0 = x # tl z" using x nth_Cons_0 False by simp
moreover have "xs = tl z @ concat (drop (Suc 0) (z # zs))" using Cons False
by (metis concat.simps(2) drop_0 drop_Suc_Cons list.sel(3) tl_append2)
ultimately show ?thesis by auto
next
case True
with Cons have "concat zs = x # xs" by auto
from Cons(1)[OF this] obtain i ys where IH:
"i < length zs"
"∀j<i. zs ! j = []"
"zs ! i = x # ys"
"xs = ys @ concat (drop (Suc i) zs)"
by auto
hence "(Suc i) < length (z # zs)" by auto
moreover have "∀j < Suc i. (z # zs) ! j = []" using IH True less_Suc_eq_0_disj by force
moreover have "(z # zs) ! (Suc i) = x # ys" using IH by auto
moreover have "xs = ys @ concat (drop (Suc (Suc i)) (z # zs))" using IH by auto
ultimately show ?thesis by auto
qed
qed auto
lemma update_eq:
assumes "∀j < length ss. j ≠ i ⟶ ss ! j = ts ! j"
and "length ss = length ts"
shows "ss = ts[i:=ss ! i]"
proof -
have "∀j < length ss. ss ! j = ts[i:=ss ! i] ! j"
apply clarsimp using assms apply (case_tac "j = i") by auto
moreover have "length ss = length (ts[i:=ss ! i])" using assms by auto
ultimately show ?thesis using nth_equalityI by blast
qed
lemma concat_steps_empty:
assumes "[] = concat (mapi (λi. map (f i)) n steps)"
shows "∀ i < length steps. steps ! i = []"
using assms
proof (induct steps arbitrary: n)
case Nil thus ?case by auto
next
case (Cons x xs)
from Cons have x:"x = []" by auto
from Cons have "[] = concat (mapi (λi. map (f i)) (Suc n) xs)" by auto
hence "∀i<length xs. xs ! i = []" using Cons by auto
thus ?case using x by (metis Suc_less_eq gr0_conv_Suc length_Cons nth_Cons_Suc nth_non_equal_first_eq)
qed
inductive_set
par_rstep2 :: "('f,'v) trs ⇒ (('f,'v)term × (('f,'v) rule × pos × ('f,'v) subst)list × ('f,'v) term) set"
for R :: "('f,'v)trs"
where
root_step2[intro]: "(s,t) ∈ R ⟹ (s ⋅ σ, [((s, t), ε, σ)], t ⋅ σ) ∈ par_rstep2 R"
| par_step_fun2[intro]: "⟦⋀i. i < length ts ⟹ (ss ! i, steps ! i, ts ! i) ∈ par_rstep2 R⟧ ⟹
length ss = length ts ⟹ length ss = length steps ⟹
(Fun f ss, concat (mapi (λi si. (map (λ (rl, p, σ). (rl, i <# p,σ)) si)) 0 steps), Fun f ts) ∈ par_rstep2 R"
| par_step_var2[intro]: "(Var x, [], Var x) ∈ par_rstep2 R"
lemma par_rstep2_refl:
shows "(s, [], s) ∈ par_rstep2 R"
proof (induct s)
case (Fun f ts)
let ?steps = "replicate (length ts) []"
{
fix i
assume "i < length ts"
hence "(ts ! i, replicate (length ts) [] ! i, ts ! i) ∈ par_rstep2 R" using Fun by auto
}
from par_rstep2.intros(2)[OF this]
show ?case using concat_replicate_empty length_replicate by metis
qed auto
lemma par_rstep2_empty:
assumes "(s, [], t) ∈ par_rstep2 R"
shows "s = t"
using assms
proof (induct s arbitrary: t)
case (Var x) show ?case using par_rstep2.cases[OF Var] by auto
next
case (Fun f ss) obtain ts steps where
steps_empty: "[] = concat (mapi (λi. map (λ(rl, p, σ). (rl, i <# p, σ))) 0 steps)" and t_dec: "t = Fun f ts"
and steps: "(∀x<length ts. (ss ! x, steps ! x, ts ! x) ∈ par_rstep2 R)" and l:"length ss = length ts" "length ss = length steps"
using Fun(2) unfolding par_rstep2.simps[of "Fun f ss" "[]" t R] by auto
have steps_i: "∀i < length steps. (steps ! i = [])" using concat_steps_empty steps_empty l by fast
hence "∀i<length ts. (ss ! i, steps ! i, ts ! i) ∈ par_rstep2 R" using steps l by auto
have "∀i < length ts. (ss ! i = ts ! i)"
proof (intro allI impI)
fix i
assume A: "i < length ts"
have "(ss ! i, steps ! i, ts ! i) ∈ par_rstep2 R" using steps A by auto
thus "ss ! i = ts ! i" using Fun(1) by (metis A steps_i l(1) l(2) nth_mem)
qed
hence "ss = ts" using l by (metis nth_equalityI)
thus ?case unfolding t_dec by auto
qed
lemma par_rstep2_append:
assumes "length ss = length ts" and "length ts = length steps"
and "∀i < length ss. (ss ! i, steps ! i, ts ! i) ∈ par_rstep2 R"
and "∀i < length ss'. (ss' ! i, steps' ! i, ts' ! i) ∈ par_rstep2 R"
shows "∀ i < length (ss @ ss'). ((ss @ ss') ! i, (steps @ steps') ! i, (ts @ ts') ! i) ∈ par_rstep2 R"
using assms
proof (induct rule: list_induct3)
case (Cons s ss t ts step steps)
show ?case
proof (intro allI impI)
fix i
assume i: "i < length ((s # ss) @ ss')"
show "(((s # ss) @ ss') ! i, ((step # steps) @ steps') ! i, ((t # ts) @ ts') ! i) ∈ par_rstep2 R"
proof (cases i)
case 0
thus ?thesis using Cons by auto
next
case (Suc j)
from Cons have "∀i<length (ss @ ss'). ((ss @ ss') ! i, (steps @ steps') ! i, (ts @ ts') ! i) ∈ par_rstep2 R" by fastforce
with Suc i show ?thesis by simp
qed
qed
qed auto
lemma par_rstep2_ctxt_closed:
assumes "(s,steps,t) ∈ par_rstep2 R"
shows "(C⟨s⟩, map (λ (rl, p, σ). (rl, hole_pos C <#> p, σ)) steps, C⟨t⟩) ∈ par_rstep2 R"
using assms
proof (induct C arbitrary:s t steps)
case (More f ls C' rs)
hence step: "(C'⟨s⟩, map (λ (rl, p, σ). (rl, hole_pos C' <#> p, σ)) steps, C'⟨t⟩) ∈ par_rstep2 R" (is "(_,?steps,_) ∈ _")
using More by auto
have ls: "∀ i < length ls. (ls ! i, [], ls ! i) ∈ par_rstep2 R"
using par_rstep2_refl by auto
have rs: "∀ i < length rs. (rs ! i,[], rs ! i) ∈ par_rstep2 R"
using par_rstep2_refl by auto
let ?steps' = "replicate (length ls) [] @ (?steps # replicate (length rs) [])"
from par_rstep2_append[of "[C'⟨s⟩]" "[C'⟨t⟩]" "[?steps]"] step rs
have "∀i < length (C'⟨s⟩ # rs). ((C'⟨s⟩ # rs) ! i, (?steps # replicate (length rs) []) ! i, (C'⟨t⟩ # rs) ! i) ∈ par_rstep2 R"
by simp
hence x: "∀i < length (ls @ C'⟨s⟩ # rs). ((ls @ C'⟨s⟩ # rs) ! i, ?steps' ! i, (ls @ C'⟨t⟩ # rs) ! i) ∈ par_rstep2 R"
(is "∀ i < length _ . (?ss ! i, _, ?ts ! i) ∈ _")
using par_rstep2_append[of ls ls] ls by simp
have l: "length ?ss = length ?ts" by auto
have lx: "length (replicate (length ls) []) = length ls" by auto
have "(Fun f ?ss, concat (mapi (λi. map (λ(rl, p, σ). (rl, i <# p, σ))) 0 ?steps'), Fun f ?ts) ∈ par_rstep2 R"
using x l by auto
hence "(Fun f ?ss,concat (mapi (λi. map (λ(rl, p, σ). (rl, i <# p, σ))) (length ls) ([?steps] @ replicate (length rs) [])), Fun f ?ts) ∈ par_rstep2 R"
unfolding append_mapi concat_append concat_replicate_empty[where ?n=0] by auto
hence "(Fun f ?ss,
concat (mapi (λi. map (λ(rl, p, σ). (rl, i <# p, σ))) (length ls) [?steps]) @
concat (mapi (λi. map (λ(rl, p, σ). (rl, i <# p, σ))) (Suc (length ls)) (replicate (length rs) [])), Fun f ?ts) ∈ par_rstep2 R"
unfolding append_mapi concat_append by auto
hence *: "(Fun f ?ss, concat (mapi (λi. map (λ(rl, p, σ). (rl, i <# p, σ))) (length ls) [?steps]), Fun f ?ts) ∈ par_rstep2 R"
unfolding length_append[symmetric] lx using concat_replicate_empty append_Nil2 by metis
have f_comp: "((λ(rl, p, σ). (rl, length ls <# p, σ)) ∘ (λ(rl, p, σ). (rl, hole_pos C' <#> p, σ))) =
((λ(rl, p, σ). (rl, length ls <# hole_pos C' <#> p, σ)))" by auto
from * show ?case apply auto using f_comp by metis
qed auto
lemma rstep_r_p_s_imp_par_rstep2:
assumes "(s,t) ∈ rstep_r_p_s R (l,r) p σ"
shows "(s, [((l, r), p, σ)], t) ∈ par_rstep2 R"
proof -
from assms obtain C where lr: "(l,r) ∈ R" and C_dec: "C = ctxt_of_pos_term p s" and p: "p ∈ poss s"
and s_dec: "s = C⟨l ⋅ σ⟩" and t_dec: "t = C⟨r ⋅ σ⟩" unfolding rstep_r_p_s_def by fastforce
have h: "hole_pos C = p" unfolding C_dec using p by auto
hence s:"(l ⋅ σ, [((l, r), ε, σ)], r ⋅ σ) ∈ par_rstep2 R" using par_rstep2.intros(1)[OF lr] by auto
have "(C⟨l ⋅ σ⟩, [((l, r), p, σ)], C⟨r ⋅ σ⟩) ∈ par_rstep2 R" using par_rstep2_ctxt_closed[OF s] using h by auto
thus ?thesis unfolding s_dec t_dec using par_rstep2_ctxt_closed C_dec by auto
qed
lemma par_rstep2_singleton:
assumes "(s, steps, t) ∈ par_rstep2 R"
and "steps = [(lr, p, σ)]"
shows "(s, t) ∈ rstep_r_p_s R lr p σ"
using assms
proof (induct arbitrary: lr p σ)
case (par_step_fun2 ts ss steps f)
let ?msteps = "mapi (λi. map (λ(lr, p, σ). (lr, i <# p, σ))) 0 steps"
from par_step_fun2 obtain i where
im:"i < length ?msteps" and mstepsi:"?msteps ! i = [(lr, p, σ)]"
and mstepsnil:"∀j < length ?msteps. j ≠ i ⟶ ?msteps ! j = []"
using concat_singleton[of ?msteps "(lr, p, σ)"] by auto
hence i: "i < length steps" using length_mapi by metis
from i par_step_fun2 have its:"i < length ts" by auto
{
fix j
assume j:"j < length ss" and "j ≠ i"
with par_step_fun2 mstepsnil im length_mapi have nil:"?msteps ! j = []" by metis
from j have *:"j < length steps" by (metis par_step_fun2(4))
from nil have nil:"steps ! j = []" unfolding mapi_nth[OF *] by simp
have "j < length ts" using j par_step_fun2(3) by auto
from par_step_fun2(1)[OF this, unfolded nil] have "ss ! j = ts ! j"
using par_rstep2_empty by auto
}
hence "∀j < length ss. j ≠ i ⟶ ss ! j = ts ! j" by blast
hence "ss = ts[i := ss ! i]" using i par_step_fun2 update_eq by blast
hence ts:"ts = take i ss @ ts ! i # drop (Suc i) ss"
by (metis append_eq_conv_conj append_take_drop_id its length_take par_step_fun2.hyps(3) take_drop_update_first upd_conv_take_nth_drop)
from mapi_nth[OF i,of _ 0] have
stepsi:"?msteps ! i = (λi. map (λ(lr, p, σ). (lr, i <# p, σ))) i (steps ! i)" by auto
with mstepsi obtain q where q:"p = i<#q" by auto
with stepsi mstepsi have stepsi:"steps ! i = [(lr, q, σ)]" by auto
from par_step_fun2(2)[OF its stepsi] have
"q ∈ poss (ss ! i)" "lr ∈ R"
"(ss ! i) |_ q = fst lr ⋅ σ" "(ts ! i) = (ctxt_of_pos_term q (ss ! i))⟨snd lr ⋅ σ⟩"
unfolding rstep_r_p_s_def' by auto
hence "(Fun f ss, Fun f ts) ∈ rstep_r_p_s R lr p σ" using q
its par_step_fun2(3) unfolding rstep_r_p_s_def' apply auto
using id_take_nth_drop[of i ts] ts by metis
thus ?case by auto
next
case (root_step2 l r τ)
thus ?case unfolding rstep_r_p_s_def by auto
qed auto
lemma par_step_merge:
assumes "length ss = length ts"
and "∀ j < length ss. ∃ steps. (∀i<length steps. fst (steps ! i) = (l, r)) ∧ (ss ! j, steps, ts ! j) ∈ par_rstep2 R"
shows "∃ steps. (∀i<length steps. fst (steps ! i) = (l, r)) ∧ (Fun f ss, steps, Fun f ts) ∈ par_rstep2 R"
proof -
from assms have a:"∃ steps. (length steps = length ss) ∧
(∀ j < length ss. (∀i<length (steps ! j). fst ((steps ! j) ! i) = (l, r)) ∧ (ss ! j, steps ! j, ts ! j) ∈ par_rstep2 R)"
proof (induct ss arbitrary: ts)
case (Cons s ss)
obtain u us where ts_dec: "ts = u # us" using Cons by (cases ts, auto)
hence l: "length ss = length us" using Cons by auto
from Cons(3) obtain steps1 where step1: "(∀i<length steps1. fst (steps1 ! i) = (l,r)) ∧ (s, steps1, u) ∈ par_rstep2 R"
using ts_dec by auto
have y: "∀j<length ss. ∃steps. (∀i<length steps. fst (steps ! i) = (l, r)) ∧ (ss ! j, steps, us ! j) ∈ par_rstep2 R"
proof (intro allI impI)
fix j
assume A:"j < length ss"
from Cons(3) A obtain steps where
"(∀i<length steps. fst (steps ! i) = (l, r)) ∧ ((s # ss) ! (j + 1), steps, (u # us) ! (j + 1)) ∈ par_rstep2 R"
unfolding ts_dec by auto
thus "∃ steps. (∀i<length steps. ((fst (steps!i) = (l,r)))) ∧ (ss ! j, steps, us ! j) ∈ par_rstep2 R"
using Cons by auto
qed
obtain steps2 where l1: "length steps2 = length ss" and
steps2: "∀j<length ss. (∀i<length (steps2 ! j). fst (steps2 ! j ! i) = (l, r)) ∧ (ss ! j, steps2 ! j, us ! j) ∈ par_rstep2 R"
using Cons(1)[OF l y] unfolding ts_dec by auto
have l: "length (steps1 # steps2) = length (s # ss)" using l1 by auto
have "∀j<length (s # ss).
(∀i<length ((steps1 # steps2) ! j). fst ((steps1 # steps2) ! j ! i) = (l,r)) ∧
((s # ss) ! j, (steps1 # steps2) ! j, ts ! j) ∈ par_rstep2 R"
proof (intro allI impI)
fix j
assume j: "j < length (s # ss)"
show "(∀i<length ((steps1 # steps2) ! j). fst ((steps1#steps2)!j!i) = (l,r)) ∧
((s # ss) ! j, (steps1 # steps2) ! j, ts ! j) ∈ par_rstep2 R"
proof (cases j)
case 0
thus ?thesis using step1 unfolding ts_dec by auto
next
case (Suc j')
thus ?thesis unfolding ts_dec using steps2 j by (metis length_Cons not_less_eq nth_Cons_Suc)
qed
qed
thus ?case using l by metis
qed auto
then obtain steps where l: "length steps = length ss" and
k: "∀j<length ts. (∀i<length (steps ! j). fst (steps ! j ! i) = (l, r)) ∧ (ss ! j, steps ! j, ts ! j) ∈ par_rstep2 R"
using assms(1) by auto
hence two: "(Fun f ss, concat (mapi (λi. map (λ(rl, p, σ). (rl, i <# p, σ))) 0 steps), Fun f ts) ∈ par_rstep2 R"
(is "(_,?steps,_) ∈ _")
using assms by auto
have j: "∀j<length steps. ∀i<length (steps ! j). fst (steps ! j ! i) = (l, r)" using k l assms(1) by auto
have one: "∀i<length ?steps. fst (?steps ! i) = (l, r)" using fst_concat_mapi[OF j] by auto
show ?thesis using one two by auto
qed
lemma subst_step_imp_par_rstep2:
assumes "(σ1(w), τ(w)) ∈ rstep_r_p_s R (l, r) v2 σ2"
and "∀x. (x = w) ∨ (σ1(x) = τ(x))"
shows "∃ steps. (∀i < length steps. fst (steps ! i) = (l, r)) ∧ (t ⋅ σ1, steps, t ⋅ τ) ∈ par_rstep2 R"
proof (induct t)
case (Var y)
thus ?case
proof (cases "y = w")
case True
let ?steps = "[((l, r), v2, σ2)]"
have len: "∀i < length ?steps. fst (?steps ! i) = (l, r)" by auto
from True have "(σ1 y, τ y) ∈ rstep_r_p_s R (l, r) v2 σ2"
using assms unfolding par_rstep2_def by auto
hence "(σ1 y, ?steps, τ y) ∈ par_rstep2 R" using rstep_r_p_s_imp_par_rstep2 by fast
hence "(Var y ⋅ σ1, ?steps, Var y ⋅ τ) ∈ par_rstep2 R" by auto
thus ?thesis using len by blast
next
case False
have len: "∀i < length []. fst ([] ! i) = (l, r)" by auto
have id: "(Var y ⋅ σ1, [], Var y ⋅ σ1) ∈ par_rstep2 R" using par_rstep2_refl by auto
have "σ1(y) = τ(y)" using assms False by auto
hence "(Var y ⋅ σ1, [], Var y ⋅ τ) ∈ par_rstep2 R" using id by auto
thus ?thesis using len by blast
qed
next
case (Fun f ts)
let ?tsσ = "map (λt. t ⋅ σ1) ts"
let ?tsτ = "map (λt. t ⋅ τ) ts"
from Fun have "∀ j < length ts. ∃ steps.
(∀i<length steps. fst (steps ! i) = (l, r)) ∧ (ts ! j ⋅ σ1, steps, ts ! j ⋅ τ) ∈ par_rstep2 R" by auto
hence x: "∀j < length ?tsσ. ∃ steps.
(∀i<length steps. fst (steps ! i) = (l, r)) ∧ (?tsσ ! j, steps, ?tsτ ! j) ∈ par_rstep2 R" by auto
have "∃steps. (∀i<length steps. fst (steps ! i) = (l, r)) ∧ (Fun f ?tsσ, steps, Fun f ?tsτ) ∈ par_rstep2 R"
using par_step_merge[OF _ x] by auto
thus ?case by auto
qed
lemma par_rstep2_decompose:
assumes "(s, steps, t) ∈ par_rstep2 R"
and "steps = x # xs"
shows "∃ s'. (s, [x], s') ∈ par_rstep2 R ∧ (s', xs, t) ∈ par_rstep2 R"
using assms
proof (induct arbitrary: x xs rule: par_rstep2.induct)
case (root_step2 s t σ)
hence "xs = []" by auto
hence "(t ⋅ σ, xs, t ⋅ σ) ∈ par_rstep2 R" using par_rstep2_refl by auto
moreover from root_step2 have "(s ⋅ σ, [x], t ⋅ σ) ∈ par_rstep2 R" by auto
ultimately show ?case by auto
next
case (par_step_fun2 ts ss steps f)
let ?msteps = "mapi (λi. map (λ(lr, p, σ). (lr, i <# p, σ))) 0 steps"
from concat_Cons[OF par_step_fun2(5)] obtain i ys where
i: "i < length ?msteps" and
nil: "∀j < i. ?msteps ! j = []" and
x: "?msteps ! i = x # ys" and
xs: "xs = ys @ concat (drop (Suc i) ?msteps)" by auto
hence ist: "i < length steps" using length_mapi by metis
from x have "x # ys = map (λ(lr, p, σ). (lr, i <# p, σ)) (steps ! i)"
unfolding mapi_nth[OF ist, of _ 0] by auto
then obtain lr p σ zs where x:"x = (lr, i<#p, σ)" and zs:"steps ! i = (lr, p, σ) # zs"
and ys:"ys = map (λ(lr, p, σ). (lr, i <# p, σ)) zs" by auto
with par_step_fun2 ist obtain s' where
s': "(ss ! i, [(lr, p, σ)], s') ∈ par_rstep2 R ∧ (s', zs, ts ! i) ∈ par_rstep2 R"
by fastforce
let ?z = "(lr, p, σ)"
let ?us = "take i ss @ s' # drop (Suc i) ss"
let ?steps' = "replicate i [] @ [[?z]] @ replicate (length steps - (Suc i)) []"
have steps':"length ss = length ?steps'" using ist par_step_fun2(4) by auto
have us: "length ss = length ?us" using ist par_step_fun2(4) by auto
{
fix j
assume j:"j < length ?us"
{
assume "j < i"
hence "?steps' ! j = []"
by (metis (erased, hide_lams) length_replicate nth_append nth_replicate)
moreover have "?us ! j = ss ! j"
by (metis ‹j < i› j nat_le_linear nth_append_take_is_nth_conv take_all us)
ultimately have "(ss ! j, ?steps' ! j, ?us ! j) ∈ par_rstep2 R"
using par_rstep2_refl by auto
} moreover {
assume "j = i"
hence "?us ! j = s'" by (metis j nat_less_le nth_append_take us)
moreover have "?steps' ! j = [?z]"
by (metis ‹j = i› append_Cons length_replicate nth_append_length)
ultimately have "(ss ! j, ?steps' ! j, ?us ! j) ∈ par_rstep2 R"
using s' ‹j = i› by auto
} moreover {
assume *:"j > i"
have "j < length steps" unfolding par_step_fun2(4)[symmetric] us using j .
hence "j - Suc i < length steps - Suc i" using * by auto
hence "?steps' ! j = []" using * unfolding nth_append by auto
moreover from * have "?us ! j = ss ! j"
by (metis j less_imp_le_nat nat_le_linear nth_append nth_append_drop_is_nth_conv take_all us)
ultimately have "(ss ! j, ?steps' ! j, ?us ! j) ∈ par_rstep2 R"
using par_rstep2_refl by auto
}
ultimately
have "(ss ! j, ?steps' ! j, ?us ! j) ∈ par_rstep2 R" by fastforce
} note args = this
have conc: "concat (mapi (λi. map (λ(lr, p, σ). (lr, i <# p, σ))) 0 ?steps') = [x]"
apply (subst append_mapi)+
apply (subst concat_append)+
apply (subst mapi_map_replicate_trivial)+
apply (subst concat_replicate_trivial)+
using x by auto
from par_rstep2.intros(2)[OF args us steps', unfolded conc]
have first:"(Fun f ss, [x], Fun f ?us) ∈ par_rstep2 R" by auto
let ?steps'' = "take i steps @ zs # drop (Suc i) steps"
have steps'': "length ?us = length ?steps''"
by (metis ist length_list_update par_step_fun2(4) upd_conv_take_nth_drop)
have ts: "length ?us = length ts"by (metis par_step_fun2(3) us)
{
fix j
assume j: "j < length ts"
have "(?us ! j, ?steps'' ! j, ts ! j) ∈ par_rstep2 R"
by (metis ist j less_imp_le_nat nth_append_take nth_list_update_neq par_step_fun2.hyps(1) par_step_fun2.hyps(4) s' upd_conv_take_nth_drop)
} note args = this
let ?isteps = "mapi (λi. map (λ(lr, p, σ). (lr, i <# p, σ))) 0 (take i steps)"
{
fix xs
assume "xs ∈ set ?isteps"
then obtain j where j:"j < length (take i steps)" and xs: "?isteps ! j = xs"
by (metis (erased, lifting) in_set_idx length_mapi)
hence eq: "steps ! j = (take i steps) ! j" by auto
from j have j2:"j < length steps" by auto
from xs eq have "?msteps ! j = xs"
unfolding mapi_nth[OF j2, of _ 0] mapi_nth[OF j, of _ 0] by auto
moreover have "j < i" using j by auto
ultimately have "xs = []" using nil by blast
}
hence *:"concat (mapi (λi. map (λ(lr, p, σ). (lr, i <# p, σ))) 0 (take i steps)) = []"
by auto
from ist have min:"(min (length steps) i) = i" by auto
have conc: "concat (mapi (λi. map (λ(lr, p, σ). (lr, i <# p, σ))) 0 ?steps'') = xs"
apply (subst append_mapi)
apply (subst concat_append)
apply (subst *)
apply (simp add: min)
unfolding xs ys zs
apply (subst mapi_drop[of "Suc i" _ 0 steps])
by auto
from par_rstep2.intros(2)[OF args ts steps'', unfolded conc]
have "(Fun f ?us, xs, Fun f ts) ∈ par_rstep2 R" by auto
with first show ?case by auto
qed auto
lemma par_rstep2_imp_seq:
assumes "(t, steps, v) ∈ par_rstep2 R"
shows "∃ ss ∈ seq R. first ss = t ∧ last ss = v ∧ length steps = length (snd ss) ∧
(∀ i < length steps. steps ! i = (get_rule (snd ss ! i), get_pos (snd ss ! i), get_subst (snd ss ! i)))"
using assms
proof (induct steps arbitrary: t)
case Nil hence eq:"t = v" using par_rstep2_empty by auto
hence "(t,[]) ∈ seq R" (is "?ss") using seq.intros by auto
thus ?case unfolding eq apply auto
by (metis last.simps(1) first.simps snd_conv)
next
case (Cons x xs)
then obtain t' where step: "(t, [x], t') ∈ par_rstep2 R" and steps: "(t', xs, v) ∈ par_rstep2 R"
using par_rstep2_decompose by metis
then obtain rl p σ where x_dec: "x = (rl,p,σ)" using prod_cases3 by blast
with step have step: "(t, t') ∈ rstep_r_p_s R rl p σ"
using par_rstep2_singleton by metis
then obtain ss' where key: "ss' ∈ seq R ∧ first ss' = t' ∧ last ss' = v ∧ length xs = length (snd ss') ∧
(∀i<length xs. xs ! i = (get_rule (snd ss' ! i), get_pos (snd ss' ! i), get_subst (snd ss' ! i)))"
using Cons steps by metis
hence "(t, (t, rl, p, σ, True, t') # snd ss') ∈ seq R" (is "?ss ∈ _")
using step seq.intros(2) by (metis first.elims snd_conv)
moreover have "first ?ss = t" by auto
moreover have "last ?ss = v" using key unfolding last.simps get_target_def
apply auto by (metis first.simps surjective_pairing)
moreover have "length (x # xs) = length (snd ?ss)" using key by auto
moreover have "∀i<length (x # xs). (x # xs) ! i = (get_rule (snd ?ss ! i), get_pos (snd ?ss ! i), get_subst (snd ?ss ! i))"
apply (intro allI impI) apply (case_tac i)
using key unfolding x_dec get_rule_def get_pos_def get_subst_def by auto
ultimately show ?case by fast
qed
lemma variable_steps_left_lin:
assumes xy:"(s, t) ∈ rstep_r_p_s R (l1, r1) p1 σ1"
and xz:"(s, u) ∈ rstep_r_p_s R (l2, r2) p2 σ2"
and "p1 <#> q = p2"
and "(v1 <#> v2) = q" and "v1 ∈ poss l1" and "l1 |_ v1 = Var w"
and lin: "linear_term l1"
defines "τ ≡ (λy. if y = w then replace_at (σ1 y) v2 (r2 ⋅ σ2) else σ1 y)"
defines "v ≡ (ctxt_of_pos_term p1 s)⟨r1 ⋅ τ⟩"
shows "(u, v) ∈ (rstep_r_p_s R (l1, r1) p1 τ)" (is "?g1")
"∃steps. (∀ i < length steps. ((fst (steps!i)) = (l2,r2))) ∧
(t,steps,v) ∈ par_rstep2 R" (is "?g2")
proof -
from assms show ?g1 using variable_steps_lin(1)[OF xy xz] by fast
show ?g2
proof -
have k1: "p1<#>v1 ∈ poss s" using assms unfolding rstep_r_p_s_def Let_def by auto
have k2: "(p1<#>v1)<#>v2 ∈ poss s" using assms unfolding rstep_r_p_s_def Let_def by auto
have s_dec1: "s = (ctxt_of_pos_term p1 s)⟨l1⋅σ1⟩" using xy unfolding rstep_r_p_s_def Let_def by auto
hence "s|_p1 = l1⋅σ1" by (metis (erased, lifting) mem_Collect_eq old.prod.case rstep_r_p_s_def subt_at_ctxt_of_pos_term xy)
hence "(s|_p1)|_v1 = σ1(w)" using assms by (metis subst_apply_term.simps(1) subt_at_subst)
hence "s|_(p1<#>v1) = σ1(w)" using k1 by (metis subterm_poss_conv)
hence "(s|_(p1<#>v1))|_v2 = (σ1(w))|_v2" by metis
hence "(s|_(p1<#>v1<#>v2)) = (σ1(w))|_v2" using k2 by (metis Position.append_assoc k1 subt_at_append)
hence "(s|_p2) = (σ1(w))|_v2" using assms by auto
have s_dec2: "s = (ctxt_of_pos_term p2 s)⟨l2⋅σ2⟩" using xz unfolding rstep_r_p_s_def Let_def by auto
hence "s|_p2 = l2⋅σ2" by (metis (erased, lifting) mem_Collect_eq old.prod.case rstep_r_p_s_def subt_at_ctxt_of_pos_term xz)
hence s1:"σ1(w) = replace_at (σ1 w) v2 (l2⋅σ2)" using assms
by (metis ‹s |_ p1 <#> v1 = σ1 w› ‹s |_ p2 = σ1 w |_ v2› ctxt_supt_id k2 subterm_poss_conv)
have s2:"τ(w) = replace_at (σ1 w) v2 (r2⋅σ2)" using assms by auto
have "(l2⋅σ2,r2⋅σ2) ∈ rstep_r_p_s R (l2,r2) ε σ2" using assms unfolding rstep_r_p_s_def Let_def by auto
hence "(replace_at (σ1 w) v2 (l2⋅σ2),replace_at (σ1 w) v2 (r2⋅σ2)) ∈ rstep_r_p_s R (l2,r2) v2 σ2"
unfolding rstep_r_p_s_def Let_def apply auto
apply (metis ‹s |_ p1 <#> v1 = σ1 w› k2 poss_append_poss s1) apply (metis s1) by (metis s1)
hence subst_step: "(σ1(w),τ(w)) ∈ rstep_r_p_s R (l2,r2) v2 σ2" using s1 s2 by auto
have aux: "∀x. (x = w) ∨ (σ1(x) = τ(x))" using assms unfolding τ_def by auto
then obtain steps where A1: "∀i < length steps. (fst (steps!i) = (l2,r2))" and B1: "(r1⋅σ1,steps,r1⋅τ) ∈ par_rstep2 R"
using subst_step_imp_par_rstep2[OF subst_step aux] by fast
have B2: "((ctxt_of_pos_term p1 s)⟨r1 ⋅ σ1⟩, map (λ(rl, p, σ). (rl, hole_pos (ctxt_of_pos_term p1 s) <#> p, σ)) steps, (ctxt_of_pos_term p1 s)⟨r1 ⋅ τ⟩) ∈ par_rstep2 R" (is "(_,?steps,_) ∈ _")
using par_rstep2_ctxt_closed[OF B1] by auto
have A2: "∀i < length ?steps. ((fst (?steps!i)) = (l2,r2))"
proof (intro allI impI)
fix i
assume "i < length ?steps"
hence l:"i < length steps" by auto
hence "fst (steps!i) = (l2,r2)" using A1 by auto
then obtain p1 σ1 where step_dec: "steps!i = ((l2,r2),p1,σ1)" by (cases "steps ! i", auto)
have "(λ(rl, p, σ). (rl, hole_pos (ctxt_of_pos_term p1 s) <#> p, σ)) (steps ! i) =
((l2, r2),hole_pos (ctxt_of_pos_term p1 s) <#>p1,σ1)"
using step_dec by auto
thus "fst (?steps!i) = (l2,r2)" unfolding nth_map[OF l] using step_dec by auto
qed
have t_dec: "t = (ctxt_of_pos_term p1 s)⟨r1⋅σ1⟩" using xy unfolding rstep_r_p_s_def Let_def by auto
from A2 B2 show ?thesis unfolding t_dec v_def by fast
qed
qed
type_synonym ('f,'v) conv = "('f,'v) term × ('f,'v) step list"
inductive_set conv :: "('f,'v) trs ⇒ ('f,'v) conv set"
for ℛ where
"(s, []) ∈ conv ℛ"
| "(s, t) ∈ rstep_r_p_s ℛ r p σ ⟹ (t, ts) ∈ conv ℛ ⟹ (s, (s,r,p,σ,True,t) # ts) ∈ conv ℛ"
| "(s, t) ∈ rstep_r_p_s ℛ r p σ ⟹ (s, ts) ∈ conv ℛ ⟹ (t, (s,r,p,σ,False,t) # ts) ∈ conv ℛ"
lemma seq_imp_conv:
assumes "ss ∈ seq R"
shows "ss ∈ conv R"
using assms
proof (induct "snd ss" arbitrary:"ss")
case Nil then obtain s where ss_dec: "ss = (s,[])" by (cases ss, auto)
thus ?case by (auto intro: conv.intros)
next
case (Cons step ts)
from Cons(2) obtain s where ss_dec: "ss = (s, step # ts)" by (cases ss, auto)
with Cons(3) obtain rl p τ t where step_dec: "step = (s, rl, p, τ, True, t)" by (auto elim: seq.cases)
hence "(s,t) ∈ rstep_r_p_s R rl p τ" and "(t, ts) ∈ conv R"
using Cons by (auto simp add: seq_chop_first ss_dec step_dec)
thus ?case unfolding ss_dec step_dec by (simp add: conv.intros)
qed
fun conv_close :: "('f,'v) seq ⇒ ('f,'v) ctxt ⇒ ('f,'v) subst ⇒ ('f,'v) seq"
where "conv_close ss C τ = (C⟨fst ss ⋅ τ⟩, map (λstep. step_close step C τ) (snd ss))"
lemma conv_super_closed1:
assumes "ss ∈ conv R"
shows "conv_close ss C σ ∈ conv R ∧ (first (conv_close ss C σ)) = C⟨first ss ⋅ σ⟩ ∧
last (conv_close ss C σ) = C⟨last ss ⋅ σ⟩"
proof -
from assms obtain u steps where "ss = (u, steps)" and conv:"(u, steps) ∈ conv R" by (cases ss) auto
let ?ss = "(u, steps)"
from conv have "conv_close ?ss C σ ∈ conv R ∧ (first (conv_close ?ss C σ)) = C⟨first ?ss ⋅ σ⟩ ∧
last (conv_close ?ss C σ) = C⟨last ?ss ⋅ σ⟩"
proof (induct rule: conv.induct)
case (2 s t r p τ ts)
then have "(C⟨s ⋅ σ⟩,C⟨t ⋅ σ⟩) ∈ rstep_r_p_s R r (hole_pos C<#>p) (τ ∘⇩s σ)"
using rstep_r_p_s_ctxt_closed2[OF rstep_r_p_s_subst_closed[OF 2(1)]] by auto
with 2 show ?case by (auto intro: conv.intros simp: get_target_def)
next
case (3 t s r p τ ts)
then have "(C⟨t ⋅ σ⟩,C⟨s ⋅ σ⟩) ∈ rstep_r_p_s R r (hole_pos C<#>p) (τ ∘⇩s σ)"
using rstep_r_p_s_ctxt_closed2[OF rstep_r_p_s_subst_closed[OF 3(1)]] by auto
with 3 show ?case by (auto intro: conv.intros simp: get_target_def)
qed (auto intro: conv.intros)
with ‹ss = (u, steps)› show ?thesis by auto
qed
definition conv_concat :: "('f,'v) seq ⇒ ('f,'v) seq ⇒ ('f,'v) seq"
where "conv_concat σ1 σ2 = (first σ1, snd σ1 @ snd σ2)"
lemma conv_chop_first_left:
assumes "(s, (s, rl, p, σ, True, t) # ss) ∈ conv R"
shows "(t, ss) ∈ conv R ∧ (s, t) ∈ rstep_r_p_s R rl p σ"
using assms by cases auto
lemma conv_chop_first_right:
assumes "(s, (t, rl, p, σ, False, s) # ss) ∈ conv R"
shows "(t, ss) ∈ conv R ∧ (t, s) ∈ rstep_r_p_s R rl p σ"
using assms by cases auto
lemma conv_dec:
assumes "ss ∈ conv R"
and "map l (snd ss) = l1 @ l2"
shows "∃ L1 L2. ss = conv_concat L1 L2 ∧ L1 ∈ conv R ∧ L2 ∈ conv R ∧ map l (snd L1) = l1 ∧
(map l (snd L2) = l2) ∧ first ss = first L1 ∧ last L1 = first L2 ∧ last L2 = last ss"
using assms
proof (induct l1 arbitrary: ss)
case Nil
hence L1: "(first ss, []) ∈ conv R" (is "?L1 ∈ _") by (auto intro: conv.intros)
hence "ss = conv_concat ?L1 ss" by (cases ss) (auto simp: conv_concat_def)
then show ?case using Nil L1 by (cases ss) (auto)
next
case (Cons a ls)
then obtain s step ts where ss_dec: "ss = (s,step#ts)" by (cases ss, auto)
with Cons(2) have "(s,step#ts) ∈ conv R" by auto
then consider (left) rl p σ t where "step = (s,rl,p,σ,True,t)" "(s,t) ∈ rstep_r_p_s R rl p σ"
| (right) rl p σ t where "step = (t,rl,p,σ,False,s)" "(t, s) ∈ rstep_r_p_s R rl p σ"
by cases auto
then show ?case
proof (cases)
case (left)
have i1:"(t,ts) ∈ conv R" using conv_chop_first_left(1)[OF Cons(2)[unfolded ss_dec[unfolded left]]] by auto
have i2:"map l (snd (t,ts)) = ls@l2" using Cons(3) Cons unfolding ss_dec left by auto
from Cons(1)[OF i1 i2] obtain L1 L2 where
IH: "(t, ts) = conv_concat L1 L2" "L1 ∈ conv R" "L2 ∈ conv R"
"map l (snd L1) = ls" "map l (snd L2) = l2"
"first (t, ts) = first L1" "last L1 = first L2" "last L2 = last (t, ts)" by fast
have t: "first L1 = t" using IH(1) unfolding conv_concat_def by auto
have f1: "ss = conv_concat (s,step # snd L1) L2" using IH(1)
unfolding ss_dec left conv_concat_def by auto
have f2: "(s,step # snd L1) ∈ conv R"
using conv.intros step IH(2) t using left apply auto by (smt conv.intros(2) first.simps prod.collapse)
have f4: "map l (snd (s,step# snd L1)) = a # ls"
using IH(4) Cons(3) unfolding ss_dec left by auto
have e1: "first ss = first ((s, step # snd L1))" unfolding ss_dec by auto
have e2: "last (s,step#snd L1) = first L2"
using IH left apply (auto simp add: get_target_def)
by (metis first.simps surjective_pairing)
have e3: "last L2 = last ss"
unfolding ss_dec left last.simps get_target_def using IH by auto
show ?thesis using f1 f2 IH(3) f4 IH(5) using e1 e2 e3 by metis
next
case (right)
have i1:"(t,ts) ∈ conv R" using conv_chop_first_right(1)[OF Cons(2)[unfolded ss_dec[unfolded right]]] by auto
have i2:"map l (snd (t,ts)) = ls@l2" using Cons(3) Cons unfolding ss_dec right by auto
from Cons(1)[OF i1 i2] obtain L1 L2 where
IH: "(t, ts) = conv_concat L1 L2" "L1 ∈ conv R" "L2 ∈ conv R"
"map l (snd L1) = ls" "map l (snd L2) = l2"
"first (t, ts) = first L1" "last L1 = first L2" "last L2 = last (t, ts)" by fast
have t: "first L1 = t" using IH(1) unfolding conv_concat_def by auto
have f1: "ss = conv_concat (s,step # snd L1) L2" using IH(1)
unfolding ss_dec right conv_concat_def by auto
have f2: "(s,step # snd L1) ∈ conv R"
using conv.intros step IH(2) t using right apply auto by (smt conv.intros(3) first.simps prod.collapse)
have f4: "map l (snd (s,step# snd L1)) = a # ls"
using IH(4) Cons(3) unfolding ss_dec right by auto
have e1: "first ss = first ((s, step # snd L1))" unfolding ss_dec by auto
have e2: "last (s,step#snd L1) = first L2"
using IH right apply (auto simp add: get_target_def)
by (metis first.simps surjective_pairing)
have e3: "last L2 = last ss"
unfolding ss_dec right last.simps get_target_def using IH by auto
show ?thesis using f1 f2 IH(3) f4 IH(5) using e1 e2 e3 by metis
qed
qed
definition ld_trs :: "('f,char list) trs ⇒ ('f,char list) lpeak ⇒
('f,char list) seq ⇒ ('f, char list) seq ⇒ ('f, char list) seq ⇒
('f,char list) seq ⇒ ('f, char list) seq ⇒ ('f, char list) seq ⇒
bool"
where "ld_trs R p jl1 jl2 jl3 jr1 jr2 jr3 = (p ∈ local_peaks R ∧
jl1 ∈ seq R ∧ jl2 ∈ seq R ∧ jl3 ∈ seq R ∧
jr1 ∈ seq R ∧ jr2 ∈ seq R ∧ jr3 ∈ seq R ∧
get_target (fst p) = first jl1 ∧ last jl1 = first jl2 ∧ last jl2 = first jl3 ∧
get_target (snd p) = first jr1 ∧ last jr1 = first jr2 ∧ last jr2 = first jr3 ∧
last jl3 = last jr3
)"
definition ldc_trs :: "('f,char list) trs ⇒ ('f,char list) lpeak ⇒
('f,char list) conv ⇒ ('f, char list) seq ⇒ ('f, char list) conv ⇒
('f,char list) conv ⇒ ('f, char list) seq ⇒ ('f, char list) conv ⇒ bool"
where "ldc_trs R p cl⇩1 sl cl⇩2 cr⇩1 sr cr⇩2 = (p ∈ local_peaks R ∧
cl⇩1 ∈ conv R ∧ sl ∈ seq R ∧ cl⇩2 ∈ conv R ∧
cr⇩1 ∈ conv R ∧ sr ∈ seq R ∧ cr⇩2 ∈ conv R ∧
get_target (fst p) = first cl⇩1 ∧ last cl⇩1 = first sl ∧ last sl = first cl⇩2 ∧
get_target (snd p) = first cr⇩1 ∧ last cr⇩1 = first sr ∧ last sr = first cr⇩2 ∧
last cl⇩2 = last cr⇩2)"
definition diamond_trs :: "('f,char list) trs ⇒ ('f,char list) lpeak ⇒ ('f,char list) conv ⇒ ('f,char list) conv ⇒ bool"
where "diamond_trs R p jl jr = (ldc_trs R p (get_target (fst p),[]) jl (last jl,[]) (get_target (snd p),[]) jr (last jr,[])
∧ length (snd jl) ≤ 1 ∧ length (snd jr) ≤ 1)"
definition ld2_trs :: "('f,char list) trs ⇒ ('f,char list) lpeak ⇒ ('f,char list) conv ⇒ ('f,char list) conv ⇒ bool"
where "ld2_trs R p jl jr = (ldc_trs R p (get_target (fst p),[]) jl (last jl,[]) (get_target (snd p),[]) jr (last jr,[]) ∧ (length (snd jr) ≤ 1 ∧ (length (snd jl) ≤ 1 ∨ (¬ linear_term (snd (get_rule (fst p)))))))"
type_synonym 'a relp = "'a rel × 'a rel"
definition ELD_1 :: "'a relp ⇒ 'a ⇒ 'a ⇒ 'a list ⇒ 'a list ⇒ 'a list ⇒ bool"
where "ELD_1 r β α σ⇩1 σ⇩2 σ⇩3 = (set σ⇩1 ⊆ ds (fst r) {β} ∧ length σ⇩2 ≤ 1 ∧ set σ⇩2 ⊆ ds (snd r) {α} ∧ set σ⇩3 ⊆ ds (fst r) {α,β})"
definition eld_conv :: "(('f,'v,'a) labeling) ⇒ 'a relp ⇒ ('f,'v) lpeak
⇒ ('f,'v) conv ⇒ ('f,'v) seq ⇒ ('f,'v) conv
⇒ ('f,'v) conv ⇒ ('f,'v) seq ⇒ ('f,'v) conv ⇒ bool"
where "eld_conv l r p cl⇩1 sl cl⇩2 cr⇩1 sr cr⇩2 =
(ELD_1 r (l (fst p)) (l (snd p)) (map l (snd cl⇩1)) (map l (snd sl)) (map l (snd cl⇩2)) ∧
ELD_1 r (l (snd p)) (l (fst p)) (map l (snd cr⇩1)) (map l (snd sr)) (map l (snd cr⇩2)))"
definition eldc :: "('f,char list) trs ⇒ ('f,char list,'a) labeling ⇒ 'a relp ⇒ ('f,char list) lpeak ⇒ bool"
where "eldc ℛ l r p = (∃ cl⇩1 sl cl⇩2 cr⇩1 sr cr⇩2.
ldc_trs ℛ p cl⇩1 sl cl⇩2 cr⇩1 sr cr⇩2 ∧ eld_conv l r p cl⇩1 sl cl⇩2 cr⇩1 sr cr⇩2)"
definition fan :: "('f,'v) trs ⇒ ('f,'v) lpeak ⇒ ('f,'v) conv ⇒ ('f,'v) conv ⇒ ('f,'v) conv
⇒ ('f,'v) conv ⇒ ('f,'v) conv ⇒ ('f,'v) conv ⇒ bool"
where "fan R p jl1 jl2 jl3 jr1 jr2 jr3 = (
(∀ i < length (snd jl1). (get_source (fst p),get_source ((snd jl1)!i)) ∈ (rstep R)^*) ∧
(∀ i < length (snd jl2). (get_source (fst p),get_source ((snd jl2)!i)) ∈ (rstep R)^*) ∧
(∀ i < length (snd jl3). (get_source (fst p),get_source ((snd jl3)!i)) ∈ (rstep R)^*) ∧
(∀ i < length (snd jr1). (get_source (fst p),get_source ((snd jr1)!i)) ∈ (rstep R)^*) ∧
(∀ i < length (snd jr2). (get_source (fst p),get_source ((snd jr2)!i)) ∈ (rstep R)^*) ∧
(∀ i < length (snd jr3). (get_source (fst p),get_source ((snd jr3)!i)) ∈ (rstep R)^*)
)"
definition eld_fan :: "('f,char list) trs ⇒ ('f,char list,'a) labeling ⇒ 'a relp ⇒ ('f,char list) lpeak ⇒ bool"
where "eld_fan ℛ l r p = (∃ cl⇩1 sl cl⇩2 cr⇩1 sr cr⇩2.
ldc_trs ℛ p cl⇩1 sl cl⇩2 cr⇩1 sr cr⇩2 ∧ eld_conv l r p cl⇩1 sl cl⇩2 cr⇩1 sr cr⇩2 ∧ fan ℛ p cl⇩1 sl cl⇩2 cr⇩1 sr cr⇩2)"
definition eld :: "('f,char list) trs ⇒ ('f,char list,'a) labeling ⇒ 'a relp ⇒ ('f,char list) lpeak ⇒ bool"
where
"eld ℛ l r p = (∃ cl⇩1 sl cl⇩2 cr⇩1 sr cr⇩2.
ld_trs ℛ p cl⇩1 sl cl⇩2 cr⇩1 sr cr⇩2 ∧ eld_conv l r p cl⇩1 sl cl⇩2 cr⇩1 sr cr⇩2 )"
definition is_labeling :: "('f,char list) trs ⇒ ('f,char list,'a) labeling ⇒ 'a relp ⇒ bool"
where "is_labeling R l r = (∀ b1 b2 s rl1 t u rl2 v C ρ σ1 σ2 p1 p2 b.
((s, t) ∈ rstep_r_p_s R rl1 p1 σ1 ∧ (u, v) ∈ rstep_r_p_s R rl2 p2 σ2 ⟶ (
let st1 = (s, rl1, p1, σ1, b1, t) in
let st2 = (u, rl2, p2, σ2, b2, v) in
((l st1, l st2) ∈ (fst r) ⟶ (l (step_close st1 C ρ), l (step_close st2 C ρ)) ∈ (fst r)) ∧
((l st1, l st2) ∈ (snd r) ⟶ (l (step_close st1 C ρ), l (step_close st2 C ρ)) ∈ (snd r)))) ∧
l (s, rl1, p1, σ1, b, t) = l (s, rl1, p1, σ1, ¬b, t))"
definition labels :: "('f,'v,'a) labeling ⇒ ('f,'v) conv ⇒ 'a set"
where "labels l ss = set (map l (snd ss))"
definition weld_seq :: "('f,'v,'a) labeling ⇒ 'a relp ⇒ ('f,'v) lpeak ⇒ ('f,'v) seq ⇒ ('f,'v) seq ⇒ bool"
where "weld_seq l r p jl jr = (
(∀ a ∈ labels l jl. a ∈ ds (snd r) {l (snd p)}) ∧
(∀ b ∈ labels l jr. b ∈ ds (snd r) {l (fst p)}))"
definition weld :: "('f,char list) trs ⇒ ('f,char list,'a) labeling ⇒ 'a relp ⇒ ('f,char list) lpeak ⇒ bool"
where "weld R l r p = (∃ jl jr. (ld2_trs R p jl jr ∧ weld_seq l r p jl jr))"
definition compatible :: "('f,char list) trs ⇒ ('f,char list,'a) labeling ⇒ 'a relp ⇒ bool"
where "compatible R l r = (is_labeling R l r ∧
(∀ p. variable_peak R p ∨ parallel_peak R p ⟶ eldc R l r p))"
definition weakly_compatible :: "('f,char list) trs ⇒ ('f,char list,'a) labeling ⇒ 'a relp ⇒ bool"
where "weakly_compatible R l r = (is_labeling R l r ∧
(left_linear_trs R ⟶ (∀ p. variable_peak R p ∨ parallel_peak R p ⟶ weld R l r p)))"
lemma linear_and_weld_imp_eld:
assumes "linear_trs R" and "weld R l r p"
shows "eldc R l r p"
proof -
from assms obtain jl jr where ld2_trs: "ld2_trs R p jl jr" and weld_seq: "weld_seq l r p jl jr"
unfolding weld_def by auto
then obtain s rl1 p1 σ1 t rl2 p2 σ2 u where
p_dec: "p = ((s,rl1,p1,σ1,True,t),(s,rl2,p2,σ2,True,u))" and lp: "p ∈ local_peaks R"
unfolding ld2_trs_def ldc_trs_def local_peaks_def by fast
obtain jl1 where jl1_eq: "jl1 = (get_target (fst p),[])" and "jl1 ∈ conv R" using conv.simps by fastforce
obtain jl3 where jl3_eq: "jl3 = (last jl,[])" and "jl3 ∈ conv R" using conv.simps by fastforce
obtain jr1 where jr1_eq: "jr1 = (get_target (snd p),[])" and "jr1 ∈ conv R" using conv.simps by fastforce
obtain jr3 where jr3_eq: "jr3 = (last jr,[])" and "jr3 ∈ conv R" using conv.simps by fastforce
hence ld: "ldc_trs R p jl1 jl jl3 jr1 jr jr3" using jl1_eq jl3_eq jr1_eq jr3_eq ld2_trs unfolding ld2_trs_def by auto
from lp have "(s,t) ∈ rstep_r_p_s R rl1 p1 σ1" unfolding local_peaks_def p_dec by auto
hence "rl1 ∈ R" unfolding rstep_r_p_s_def by (auto simp: Let_def)
hence "linear_term (snd (get_rule (fst p)))" unfolding p_dec get_rule_def apply auto using assms unfolding linear_trs_def by (metis assms(1) linear_trsE prod.collapse)
hence jl: "length (snd jl) ≤ 1" using ld2_trs unfolding weld_def ldc_trs_def ld2_trs_def weld_seq_def eld_conv_def linear_trs_def using assms(1) by auto
have jr: "length (snd jr) ≤ 1" using ld2_trs unfolding ld2_trs_def by auto
have "ELD_1 r (l (fst p)) (l (snd p)) [] (map l (snd jl)) []" using weld_seq jl unfolding ELD_1_def ds_def apply auto unfolding weld_seq_def labels_def ds_def by auto
moreover have "ELD_1 r (l (snd p)) (l (fst p)) [] (map l (snd jr)) []" using weld_seq jr unfolding ELD_1_def ds_def apply auto unfolding weld_seq_def labels_def ds_def by auto
ultimately have "eld_conv l r p jl1 jl jl3 jr1 jr jr3" unfolding jl1_eq jl3_eq jr1_eq jr3_eq eld_conv_def by auto
hence "eld_conv l r p jl1 jl jl3 jr1 jr jr3" and "ldc_trs R p jl1 jl jl3 jr1 jr jr3" using ld by auto
hence "∃ jl1 jl2 jl3 jr1 jr2 jr3. ldc_trs R p jl1 jl2 jl3 jr1 jr2 jr3 ∧ eld_conv l r p jl1 jl2 jl3 jr1 jr2 jr3" by blast
thus ?thesis unfolding eldc_def by auto
qed
lemma linear_and_weakly_compatible_is_compatible:
assumes "linear_trs R" and "weakly_compatible R l r"
shows "compatible R l r" proof -
from assms have ll: "left_linear_trs R" unfolding linear_trs_def left_linear_trs_def by auto
have 1: "is_labeling R l r" using assms unfolding weakly_compatible_def by auto
{
fix p assume A: "variable_peak R p ∨ parallel_peak R p"
hence " weld R l r p" using assms(2) ll unfolding weakly_compatible_def by metis
hence "eldc R l r p" using linear_and_weld_imp_eld[OF assms(1)] by fast
}
thus ?thesis using 1 unfolding compatible_def by auto
qed
lemma ldc_trs_closed:
fixes C τ
assumes "ldc_trs R p jl1 jl2 jl3 jr1 jr2 jr3"
shows "ldc_trs R ((step_close (fst p) C τ),(step_close (snd p) C τ))
(conv_close jl1 C τ) (seq_close jl2 C τ) (conv_close jl3 C τ)
(conv_close jr1 C τ) (seq_close jr2 C τ) (conv_close jr3 C τ) " (is "ldc_trs R ?P _ _ _ _ _ _")
proof -
from assms obtain s rl1 p1 σ1 t rl2 p2 σ2 u
where p_dec: "p = ((s,rl1,p1,σ1,True,t),(s,rl2,p2,σ2,True,u))" and "p ∈ local_peaks R"
unfolding ldc_trs_def local_peaks_def by fast
hence l:"(s,t) ∈ rstep_r_p_s R rl1 p1 σ1" and r:"(s,u) ∈ rstep_r_p_s R rl2 p2 σ2" unfolding local_peaks_def by auto
from l have P1: "(C⟨s⋅τ⟩,C⟨t⋅τ⟩) ∈ rstep_r_p_s R rl1 (hole_pos C<#> p1) (σ1∘⇩s τ)"
using rstep_r_p_s_ctxt_closed2 rstep_r_p_s_subst_closed by metis
from r have P2: "(C⟨s⋅τ⟩,C⟨u⋅τ⟩) ∈ rstep_r_p_s R rl2 (hole_pos C<#> p2) (σ2∘⇩s τ)"
using rstep_r_p_s_ctxt_closed2 rstep_r_p_s_subst_closed by metis
from P1 P2 have P: "?P ∈ local_peaks R" unfolding local_peaks_def p_dec step_close.simps fst_conv snd_conv Let_def by fast
from assms have jl1:"jl1 ∈ conv R" and jl2:"jl2 ∈ seq R" and jl3:"jl3 ∈ conv R"
and jr1:"jr1 ∈ conv R" and jr2:"jr2 ∈ seq R" and jr3:"jr3 ∈ conv R"
and l: "get_target (fst p) = first jl1" and r: "get_target (snd p) = first jr1" and b: "last jl3 = last jr3" unfolding ldc_trs_def by auto
have JL1: "conv_close jl1 C τ ∈ conv R" using conv_super_closed1[OF jl1] by fast
have JL2: "seq_close jl2 C τ ∈ seq R" using seq_super_closed1[OF jl2] by fast
have JL3: "conv_close jl3 C τ ∈ conv R" using conv_super_closed1[OF jl3] by fast
have JR1: "conv_close jr1 C τ ∈ conv R" using conv_super_closed1[OF jr1] by fast
have JR2: "seq_close jr2 C τ ∈ seq R" using seq_super_closed1[OF jr2] by fast
have JR3: "conv_close jr3 C τ ∈ conv R" using conv_super_closed1[OF jr3] by fast
have L1: "get_target (step_close (fst (p)) C τ) = first (conv_close jl1 C τ)"
using step_super_closed1 l conv_super_closed1[OF jl1] by metis
have L2: "last (conv_close jl1 C τ) = first (seq_close jl2 C τ)"
using l conv_super_closed1[OF jl1] seq_super_closed1[OF jl2] by (metis assms ldc_trs_def)
have L3: "last (seq_close jl2 C τ) = first (conv_close jl3 C τ)"
using l seq_super_closed1[OF jl2] conv_super_closed1[OF jl3] by (metis assms ldc_trs_def)
have R1: "get_target (step_close (snd (p)) C τ) = first (conv_close jr1 C τ)"
using step_super_closed1 r conv_super_closed1[OF jr1] by metis
have R2: "last (conv_close jr1 C τ) = first (seq_close jr2 C τ)"
using l conv_super_closed1[OF jr1] seq_super_closed1[OF jr2] by (metis assms ldc_trs_def)
have R3: "last (seq_close jr2 C τ) = first (conv_close jr3 C τ)"
using l seq_super_closed1[OF jr2] conv_super_closed1[OF jr3] by (metis assms ldc_trs_def)
have "last (conv_close jl3 C τ) = last (conv_close jr3 C τ)" using conv_super_closed1 jl3 jr3 b by metis
thus ?thesis using P JL1 JL2 JL3 JR1 JR2 JR3 L1 L2 L3 R1 R2 R3 unfolding ldc_trs_def by auto
qed
lemma el_closed:
fixes C τ
assumes lab: "is_labeling R l r"
and s1: "(s,t) ∈ rstep_r_p_s R rl1 p1 σ1"
and ss: "ss ∈ seq R"
and dec: "∀ b ∈ set (map l (snd ss)). (b,l (s,rl1,p1,σ1,True,t)) ∈ (snd r)"
shows "∀ b ∈ set (map l (snd (seq_close ss C τ))). (b,l (step_close (s,rl1,p1,σ1,True,t) C τ)) ∈ (snd r)"
using ss dec
proof (induct "snd ss" arbitrary:"ss")
case Nil thus ?case by auto
next
case (Cons step steps)
from Cons(2) obtain u where ss_dec: "ss = (u,step # steps)" by (cases ss, auto)
with Cons(3) obtain rl2 p2 σ2 v where step_dec: "step = (u,rl2,p2,σ2,True,v)" and s2: "(u,v) ∈ rstep_r_p_s R rl2 p2 σ2"
using seq.cases by blast
have "(l step, l (s,rl1,p1,σ1,True,t)) ∈ (snd r)" using Cons unfolding ss_dec step_dec by auto
hence step_close: "(l (step_close step C τ), l (step_close (s,rl1,p1,σ1,True,t) C τ)) ∈ snd r"
using lab s1 s2 unfolding is_labeling_def step_dec Let_def by blast
hence vs: "(v,steps) ∈ seq R" using Cons unfolding ss_dec step_dec using seq_chop_first by fast
hence "∀b∈set (map l (snd (v,steps))). (b, l (s, rl1, p1, σ1, True, t)) ∈ snd r" using Cons unfolding ss_dec step_dec by auto
hence "∀ b ∈ set (map l (snd (seq_close (v,steps) C τ))). (b,l (step_close (s,rl1,p1,σ1,True,t) C τ)) ∈ snd r"
using Cons(1)[OF _ vs] Cons by auto
thus ?case using step_close unfolding ss_dec by auto
qed
lemma eseq_super_closed2:
fixes C σ
assumes step': "(s',t') ∈ rstep_r_p_s R rl' p' ρ"
and lab: "is_labeling R l r"
and seq: "ss ∈ seq R"
and dec:"∀ b ∈ set (map l (snd ss)). (b,l (s',rl',p',ρ,True,t')) ∈ (fst r)"
shows "(∀ b ∈ set (map l (snd (seq_close ss C σ))). (b,l (step_close (s',rl',p',ρ,True,t') C σ)) ∈ (fst r))"
using seq dec proof (induct "snd ss" arbitrary: ss)
case Nil then obtain s where ss_dec: "ss = (s,[])" using surjective_pairing by metis
thus ?case using seq.intros unfolding ss_dec by auto
next
case (Cons step ts)
from Cons(2) obtain s where ss_dec: "ss=(s,step#ts)" by (cases ss, auto)
with Cons(3) obtain rl p τ t where step_dec: "step=(s,rl,p,τ,True,t)" using seq.cases by blast
hence step: "(s,t) ∈ rstep_r_p_s R rl p τ" and i:"(t,ts) ∈ seq R" (is "?ts ∈ _") using Cons(3) seq.cases unfolding ss_dec step_dec by auto
have j:"∀b ∈ set (map l (snd ?ts)). (b,l (s',rl',p',ρ,True,t')) ∈ fst r" using Cons unfolding ss_dec snd_conv by auto
from Cons(1)[OF _ i j] have
ih: "(∀ b ∈ set (map l (snd (seq_close ?ts C σ))). (b,l (C⟨s'⋅σ⟩,rl',hole_pos C<#>p',ρ ∘⇩s σ,True,C⟨t'⋅σ⟩)) ∈ fst r)" by auto
have C_label: "(l (s,rl,p,τ,True,t),l (s',rl',p',ρ,True,t')) ∈ fst r" using Cons unfolding ss_dec step_dec snd_conv by auto
have C_label2: "(l (step_close (s,rl,p,τ,True,t) C σ),l (step_close (s',rl',p',ρ,True,t') C σ)) ∈ fst r"
using step step' C_label lab dec unfolding is_labeling_def Let_def by fast
hence C_labels: "(∀b∈set (map l (snd (seq_close ss C σ))). (b, l (C⟨s' ⋅ σ⟩, rl', hole_pos C <#> p', ρ ∘⇩s σ,True, C⟨t' ⋅ σ⟩)) ∈ fst r)"
using ih(1) unfolding ss_dec step_dec seq_close.simps snd_conv step_close.simps Let_def by auto
show ?case using C_labels by auto
qed
lemma eseq_super_closed3:
fixes C σ
assumes step': "(s',t') ∈ rstep_r_p_s R rl' p' ρ"
and step'': "(s'',t'') ∈ rstep_r_p_s R rl'' p'' ρ'"
and lab: "is_labeling R l r"
and seq: "ss ∈ seq R"
and dec:"∀ b ∈ set (map l (snd ss)). ((b,l (s',rl',p',ρ,True,t')) ∈ fst r ∨ (b,l (s'',rl'',p'',ρ',True,t'')) ∈ fst r)"
shows "(∀ b ∈ set (map l (snd (seq_close ss C σ))). ((b,l (step_close (s',rl',p',ρ,True,t') C σ)) ∈ fst r) ∨ (b,l (step_close (s'',rl'',p'',ρ',True,t'') C σ)) ∈ fst r)"
using seq dec proof (induct "snd ss" arbitrary: ss)
case Nil then obtain s where ss_dec: "ss = (s,[])" using surjective_pairing by metis
thus ?case using seq.intros unfolding ss_dec by auto
next
case (Cons step ts)
from Cons(2) obtain s where ss_dec: "ss=(s,step#ts)" by (cases ss, auto)
with Cons(3) obtain rl p τ t where step_dec: "step=(s,rl,p,τ,True,t)"
using seq.cases by blast
hence step: "(s,t) ∈ rstep_r_p_s R rl p τ" and i:"(t,ts) ∈ seq R" (is "?ts ∈ _") using Cons(3) seq.cases unfolding step_dec ss_dec by auto
have j:"∀b ∈ set (map l (snd ?ts)). ((b, l (s',rl',p',ρ,True,t')) ∈ fst r ∨ (b,l (s'',rl'',p'',ρ',True,t'')) ∈ fst r)" using Cons unfolding ss_dec snd_conv by auto
from Cons(1)[OF _ i j] have
ih: "(∀ b ∈ set (map l (snd (seq_close ?ts C σ))). ((b,l (step_close (s',rl',p',ρ,True,t') C σ)) ∈ fst r) ∨ (b,l (step_close (s'',rl'',p'',ρ',True,t'') C σ)) ∈ fst r)" (is "∀ b ∈ _. (b,?a') ∈ ?r ∨ (b,?a'') ∈ ?r") by auto
have C_step: "(C⟨s⋅σ⟩,C⟨t⋅σ⟩) ∈ rstep_r_p_s R rl (hole_pos C<#>p) (τ∘⇩s σ)" using rstep_r_p_s_ctxt_closed2[OF rstep_r_p_s_subst_closed[OF step]] by auto
have C_label: "(l (s,rl,p,τ,True,t),l (s',rl',p',ρ,True,t')) ∈ fst r ∨ (l (s,rl,p,τ,True,t),l (s'',rl'',p'',ρ',True,t'')) ∈ fst r" using Cons(4) unfolding ss_dec step_dec snd_conv by auto
have C_label2: "(l (step_close (s,rl,p,τ,True,t) C σ),?a') ∈ fst r ∨ (l (step_close (s,rl,p,τ,True,t) C σ),?a'') ∈ fst r" (is "(?a,_) ∈ fst r ∨ _") proof(cases "(l (s,rl,p,τ,True,t),l (s',rl',p',ρ,True,t')) ∈ ?r")
case True thus ?thesis using step step' lab dec unfolding is_labeling_def Let_def by fast
next
case False hence l: "(l (s,rl,p,τ,True,t),l (s'',rl'',p'',ρ',True,t'')) ∈ fst r" using C_label by auto
thus ?thesis using step step'' C_step rstep_r_p_s_ctxt_closed2[OF rstep_r_p_s_subst_closed[OF step''],of "C" "σ"] l lab dec unfolding is_labeling_def Let_def by fast
qed
hence C_labels: "(∀b∈set (map l (snd (seq_close ss C σ))). ((b,?a') ∈ fst r ∨ (b,?a'') ∈ fst r))"
using ih unfolding ss_dec step_dec seq_close.simps snd_conv step_close.simps Let_def by auto
show ?case using C_labels by auto
qed
lemma conv_imp_conv:
assumes "ss ∈ conv R"
and "set (map l (snd ss)) ⊆ ds r S"
and "is_labeling R l (r,r')"
defines "rel ≡ λ c. {(s,t). ∃ r p σ b. (s,t) ∈ rstep_r_p_s R r p σ ∧ l (s,r,p,σ,True,t) = c}"
shows "(first ss, last ss) ∈ ((⋃c ∈ ds r S. (rel c))⇧↔)^*"
proof -
from assms obtain t ts where ss_dec: "ss = (t,ts)" by (metis surjective_pairing)
from assms(1,2) show ?thesis unfolding ss_dec
proof (induct)
case (2 s t rl p σ ts)
then have "l (s, rl, p, σ, True, t) ∈ ds r S" by auto
then have "(s, t) ∈ UNION (ds r S) rel" using 2 unfolding rel_def by blast
then have "(s, t) ∈ ((⋃a∈ds r S. rel a)⇧↔)⇧*" by blast
with 2 show ?case by (auto simp: get_target_def)
next
case (3 s t rl p σ ts)
then have "l (s, rl, p, σ, False, t) ∈ ds r S" by auto
moreover have "l (s, rl, p, σ, False, t) = l (s, rl, p, σ, True, t)"
using assms(3)[unfolded is_labeling_def, rule_format, of s t rl p σ, where b = False] by simp
ultimately have "l (s, rl, p, σ, True, t) ∈ ds r S" by auto
then have "(s, t) ∈ UNION (ds r S) rel" using 3(1) unfolding rel_def by blast
then have "(t, s) ∈ ((⋃a∈ds r S. rel a)⇧↔)⇧*" by blast
with 3 show ?case by (auto simp: get_target_def)
qed auto
qed
lemma econv_super_closed2:
assumes step': "(s',t') ∈ rstep_r_p_s R rl' p' ρ"
and lab: "is_labeling R l r"
and conv: "ss ∈ conv R"
and dec:"∀ b ∈ set (map l (snd ss)). (b, l (s',rl',p',ρ, b', t')) ∈ (fst r)"
shows "∀ b ∈ set (map l (snd (conv_close ss C σ))). (b, l (step_close (s',rl',p',ρ, b', t') C σ)) ∈ (fst r)"
proof -
obtain s steps where ss:"ss = (s, steps)" by (cases ss, auto)
from conv[unfolded ss] dec[unfolded ss]
have "∀ b ∈ set (map l (snd (conv_close (s, steps) C σ))). (b, l (step_close (s',rl',p',ρ, b', t') C σ)) ∈ (fst r)"
proof (induct)
case (2 s t rl p τ ts)
have "∀b∈set (map l (snd (t, ts))). (b, l (s', rl', p', ρ, b', t')) ∈ fst r" using 2(4) by auto
from 2(3)[OF this] have ih:"∀b∈set (map l (snd (conv_close (t, ts) C σ))). (b, l (step_close (s', rl', p', ρ, b', t') C σ)) ∈ fst r" .
have C_label: "(l (s,rl,p,τ,True,t),l (s',rl',p',ρ,b',t')) ∈ fst r" using 2(4) unfolding snd_conv by auto
have C_label2: "(l (step_close (s,rl,p,τ,True,t) C σ),l (step_close (s',rl',p',ρ,b',t') C σ)) ∈ fst r"
using 2(1) step' C_label lab[unfolded is_labeling_def Let_def, rule_format, of s t rl p] by blast
then show ?case using ih(1) unfolding conv_close.simps snd_conv step_close.simps Let_def by auto
next
case (3 t s rl p τ ts)
have "∀b∈set (map l (snd (t, ts))). (b, l (s', rl', p', ρ, b', t')) ∈ fst r" using 3(4) by auto
from 3(3)[OF this] have ih:"∀b∈set (map l (snd (conv_close (t, ts) C σ))). (b, l (step_close (s', rl', p', ρ, b', t') C σ)) ∈ fst r" .
have C_label: "(l (t,rl,p,τ,False,s), l (s',rl',p',ρ,b',t')) ∈ fst r" using 3(4) unfolding snd_conv by auto
then have C_label2: "(l (step_close (t,rl,p,τ,False,s) C σ),l (step_close (s',rl',p',ρ,b',t') C σ)) ∈ fst r"
using 3(1) step' C_label lab[unfolded is_labeling_def Let_def, rule_format, of t s rl p τ s' t' rl' p' ρ] by blast
then show ?case using ih(1) unfolding conv_close.simps snd_conv step_close.simps Let_def by auto
qed auto
with ss show ?thesis by auto
qed
lemma econv_super_closed3:
fixes C σ
assumes step': "(s',t') ∈ rstep_r_p_s R rl' p' ρ"
and step'': "(s'',t'') ∈ rstep_r_p_s R rl'' p'' ρ'"
and lab: "is_labeling R l r"
and conv: "ss ∈ conv R"
and dec:"∀ b ∈ set (map l (snd ss)). ((b,l (s',rl',p',ρ,b',t')) ∈ fst r ∨ (b,l (s'',rl'',p'',ρ',b'',t'')) ∈ fst r)"
shows "∀ b ∈ set (map l (snd (conv_close ss C σ))). ((b,l (step_close (s',rl',p',ρ,b',t') C σ)) ∈ fst r)
∨ (b,l (step_close (s'',rl'',p'',ρ',b'',t'') C σ)) ∈ fst r"
proof -
obtain s steps where ss:"ss = (s, steps)" by (cases ss, auto)
from conv[unfolded ss] dec[unfolded ss]
have "∀ b ∈ set (map l (snd (conv_close (s, steps) C σ))). ((b,l (step_close (s',rl',p',ρ,b',t') C σ)) ∈ fst r)
∨ (b,l (step_close (s'',rl'',p'',ρ',b'',t'') C σ)) ∈ fst r"
proof (induct)
case (2 s t rl p τ ts)
have "∀b∈set (map l (snd (t, ts))). (b, l (s', rl', p', ρ, b', t')) ∈ fst r ∨
(b, l (s'', rl'', p'', ρ', b'', t'')) ∈ fst r" using 2(4) by auto
from 2(3)[OF this] have ih:"∀b∈set (map l (snd (conv_close (t, ts) C σ))).
(b, l (step_close (s', rl', p', ρ, b', t') C σ)) ∈ fst r ∨
(b, l (step_close (s'', rl'', p'', ρ', b'', t'') C σ)) ∈ fst r" .
have C_label: "(l (s,rl,p,τ,True,t),l (s',rl',p',ρ,b',t')) ∈ fst r ∨
(l (s,rl,p,τ,True,t),l (s'',rl'',p'',ρ',b'',t'')) ∈ fst r" using 2(4) unfolding snd_conv by auto
have C_label2: "(l (step_close (s,rl,p,τ,True,t) C σ),l (step_close (s',rl',p',ρ,b',t') C σ)) ∈ fst r ∨
(l (step_close (s,rl,p,τ,True,t) C σ),l (step_close (s'',rl'',p'',ρ',b'',t'') C σ)) ∈ fst r"
using 2(1) step' step'' C_label lab[unfolded is_labeling_def Let_def, rule_format, of s t rl p] by blast
then show ?case using ih(1) unfolding conv_close.simps snd_conv step_close.simps Let_def by auto
next
case (3 t s rl p τ ts)
have "∀b∈set (map l (snd (t, ts))). (b, l (s', rl', p', ρ, b', t')) ∈ fst r ∨
(b, l (s'', rl'', p'', ρ', b'', t'')) ∈ fst r" using 3(4) by auto
from 3(3)[OF this] have ih:"∀b∈set (map l (snd (conv_close (t, ts) C σ))).
(b, l (step_close (s', rl', p', ρ, b', t') C σ)) ∈ fst r ∨
(b, l (step_close (s'', rl'', p'', ρ', b'', t'') C σ)) ∈ fst r" .
have C_label: "(l (t,rl,p,τ,False,s), l (s',rl',p',ρ,b',t')) ∈ fst r ∨
(l (t,rl,p,τ,False,s), l (s'',rl'',p'',ρ',b'',t'')) ∈ fst r" using 3(4) unfolding snd_conv by auto
then have C_label2: "(l (step_close (t,rl,p,τ,False,s) C σ),l (step_close (s',rl',p',ρ,b',t') C σ)) ∈ fst r ∨
(l (step_close (t,rl,p,τ,False,s) C σ),l (step_close (s'',rl'',p'',ρ',b'',t'') C σ)) ∈ fst r"
using 3(1) step' step'' C_label lab[unfolded is_labeling_def Let_def, rule_format, of t s rl p τ] by blast
then show ?case using ih(1) unfolding conv_close.simps snd_conv step_close.simps Let_def by auto
qed auto
with ss show ?thesis by auto
qed
lemma conv_concat_conv_close:
shows "conv_close (conv_concat ts us) C τ = conv_concat (conv_close ts C τ) (conv_close us C τ)"
proof -
obtain t tq u uq where ts_dec: "ts = (t,tq)" and us_dec: "us = (u,uq)"
by (cases ts, cases us, auto)
thus ?thesis unfolding conv_concat_def by auto
qed
lemma conv_concat_labels:
shows "map l (snd (conv_concat ts us)) = (map l (snd ts)) @ (map l (snd us))"
proof -
obtain t tq u uq where ts_dec: "ts = (t,tq)" and us_dec: "us = (u,uq)"
by (cases ts, cases us, auto)
show ?thesis unfolding conv_concat_def by auto
qed
lemma eld_conv_closed:
fixes C τ
assumes d: "ldc_trs R p jl1 jl2 jl3 jr1 jr2 jr3"
and "eld_conv l r p jl1 jl2 jl3 jr1 jr2 jr3"
and lab: "is_labeling R l r"
shows "eld_conv l r ((step_close (fst p) C τ),(step_close (snd p) C τ))
(conv_close jl1 C τ) (seq_close jl2 C τ) (conv_close jl3 C τ)
(conv_close jr1 C τ) (seq_close jr2 C τ) (conv_close jr3 C τ)"
(is "eld_conv _ _ ?P ?JL1 ?JL2 ?JL3 ?JR1 ?JR2 ?JR3")
proof -
{
fix s rl1 p1 σ1 t rl2 p2 σ2 u l1 l2 l3 jl1 jl2 jl3 b1 b2
let ?a = "l (s,rl1,p1,σ1,True,t)"
let ?a' = "l (s,rl2,p2,σ2,True,u)"
let ?A = "l (step_close (s, rl1, p1, σ1, True, t) C τ)"
let ?A' = "l (step_close (s, rl2, p2, σ2, True, u) C τ)"
assume
lstep: "(s,t) ∈ rstep_r_p_s R rl1 p1 σ1" and
lstep': "(s,u) ∈ rstep_r_p_s R rl2 p2 σ2" and
ELD_l: "ELD_1 r ?a ?a' (map l (snd jl1)) (map l (snd jl2)) (map l (snd jl3))" and
L1:"jl1 ∈ conv R" and L2: "jl2 ∈ seq R" and L3: "jl3 ∈ conv R"
have "length (snd jl2) ≤ 1" using ELD_l unfolding ELD_1_def by auto
hence JL: "length (snd (seq_close jl2 C τ)) ≤ 1" using seq_close_length by auto
from ELD_l have
ELD1: "∀ b ∈ set (map l (snd jl1)). (b, ?a) ∈ fst r" and
ELD2: "∀ b ∈ set (map l (snd jl2)). (b, ?a') ∈ snd r" and
ELD3: "∀ b ∈ set (map l (snd jl3)). ((b, ?a) ∈ fst r ∨ (b, ?a') ∈ fst r)"
unfolding ELD_1_def ds_def by auto
let ?sc = "λL. conv_close L C τ"
have L1:"∀ b ∈ set (map l (snd (?sc jl1))). (b, ?A) ∈ fst r"
using econv_super_closed2[OF lstep lab L1] ELD1 unfolding fst_conv by auto
have L2:"∀ b ∈ set (map l (snd (?sc jl2))). (b,?A') ∈ snd r"
using el_closed[OF lab _ L2] lstep' ELD2 unfolding snd_conv by auto
have L3:"∀ b ∈ set (map l (snd (?sc jl3))). ((b, ?A) ∈ fst r ∨ (b, ?A') ∈ fst r)"
using econv_super_closed3[OF lstep lstep' lab L3] ELD3 unfolding fst_conv by simp
hence L: "ELD_1 r ?A ?A' (map l (snd (?sc jl1))) (map l (snd (?sc jl2))) (map l (snd (?sc jl3)))"
unfolding ELD_1_def ds_def using L1 L2 L3 JL by auto
with L have " ELD_1 r ?A ?A' (map l (snd (?sc jl1))) (map l (snd (?sc jl2))) (map l (snd (?sc jl3)))" by auto
} note * = this
from assms have pl:"p ∈ local_peaks R" unfolding ldc_trs_def by auto
then obtain s rl1 p1 σ1 t rl2 p2 σ2 u where p: "p = ((s, rl1, p1, σ1, True, t),(s, rl2, p2, σ2, True, u))"
unfolding local_peaks_def by blast
have lstep: "(s, t) ∈ rstep_r_p_s R rl1 p1 σ1" using pl unfolding local_peaks_def p by auto
have lstep': "(s, u) ∈ rstep_r_p_s R rl2 p2 σ2" using pl unfolding local_peaks_def p by auto
let ?a = "l (s, rl1, p1, σ1, True, t)"
let ?a' = "l (s, rl2, p2, σ2, True, u)"
from assms obtain l1 l2 l3 where jl1_dec2: "map l (snd jl1) = l1" and jl2_dec2: "map l (snd jl2) = l2"
and jl3_dec2: "map l (snd jl3) = l3" and LD_l: "ELD_1 r ?a ?a' (map l (snd jl1)) (map l (snd jl2)) (map l (snd jl3))"
unfolding eld_conv_def unfolding p by auto
have jl1:"jl1 ∈ conv R" and jl2: "jl2 ∈ seq R" and jl3: "jl3 ∈ conv R" using d unfolding ldc_trs_def by auto
from assms obtain r1 r2 r3 where jr1_dec2: "map l (snd jr1) = r1" and jr2_dec2: "map l (snd jr2) = r2"
and jr3_dec2: "map l (snd jr3) = r3" and LD_r: "ELD_1 r ?a' ?a (map l (snd jr1)) (map l (snd jr2)) (map l (snd jr3))"
unfolding eld_conv_def unfolding p by auto
have jr1:"jr1 ∈ conv R" and jr2: "jr2 ∈ seq R" and jr3: "jr3 ∈ conv R" using d unfolding ldc_trs_def by auto
from *[OF lstep lstep' LD_l jl1 jl2 jl3] *[OF lstep' lstep LD_r jr1 jr2 jr3] show ?thesis
unfolding eld_conv_def p by auto
qed
lemma eld_closed:
fixes C τ
assumes "eldc R l r p"
and lab: "is_labeling R l r"
shows "eldc R l r (step_close (fst p) C τ,step_close (snd p) C τ)"
proof -
from assms(1) obtain jl1 jl2 jl3 jr1 jr2 jr3 where d: "ldc_trs R p jl1 jl2 jl3 jr1 jr2 jr3"
and D: "eld_conv l r p jl1 jl2 jl3 jr1 jr2 jr3" unfolding eldc_def by auto
have C_d:"ldc_trs R (step_close (fst p) C τ,step_close (snd p) C τ)
(conv_close jl1 C τ) (seq_close jl2 C τ) (conv_close jl3 C τ)
(conv_close jr1 C τ) (seq_close jr2 C τ) (conv_close jr3 C τ)"
(is "ldc_trs R ?p ?jl1 ?jl2 ?jl3 ?jr1 ?jr2 ?jr3") using ldc_trs_closed[OF d] by fast
have "eld_conv l r ?p ?jl1 ?jl2 ?jl3 ?jr1 ?jr2 ?jr3" using eld_conv_closed[OF d D lab] by auto
thus ?thesis using C_d unfolding eldc_def by fast
qed
lemma critical:
assumes "function_peak R p"
and cp:"∀ (b, p) ∈ critical_peaks R. eldc R l r p"
and lab: "is_labeling R l r"
shows "eldc R l r p"
proof -
from function_peak_inst_of_critical_peak assms(1) obtain C δ b cp where
"(b, cp) ∈ critical_peaks R" and
inst: "p = (step_close (fst cp) C δ, step_close (snd cp) C δ)"
by blast
hence eldc: "eldc R l r cp" using cp by auto
thus ?thesis using eld_closed[OF eldc] trans eldc lab inst by fast
qed
lemma left:
assumes "variable_peak R p ∨ function_peak R p"
and cps: "∀ (b, p) ∈ critical_peaks R. eldc R l r p"
and lab: "compatible R l r"
shows "eldc R l r p"
proof (cases "variable_peak R p")
case True thus ?thesis using lab unfolding compatible_def by fast
next
case False hence "function_peak R p" using assms by auto
thus ?thesis using critical lab cps unfolding eldc_def compatible_def by fast
qed
lemma eld_mirror: assumes "eldc R l r p" shows "eldc R l r (snd p,fst p)" proof -
from assms obtain jl1 jl2 jl3 jr1 jr2 jr3 where d: "ldc_trs R p jl1 jl2 jl3 jr1 jr2 jr3"
and D: "eld_conv l r p jl1 jl2 jl3 jr1 jr2 jr3" unfolding eldc_def by auto
from d have d: "ldc_trs R (snd p,fst p) jr1 jr2 jr3 jl1 jl2 jl3" unfolding ldc_trs_def by (metis fst_conv mirror snd_conv)
from D have D: "eld_conv l r (snd p,fst p) jr1 jr2 jr3 jl1 jl2 jl3" unfolding eld_conv_def by auto
show ?thesis using d D unfolding eldc_def by fast
qed
lemma main_eld:
assumes cps:"∀ (b, p) ∈ critical_peaks R. eldc R l r p"
and lab: "compatible R l r"
shows "∀ p ∈ local_peaks R. eldc R l r p"
proof
fix p
assume A: "p ∈ local_peaks R"
show "eldc R l r p"
proof -
show ?thesis using local_peaks_cases[OF A]
proof (cases "parallel_peak R p")
case True
show ?thesis using True lab unfolding compatible_def by fast
next
case False note po = this
thus ?thesis using local_peaks_cases[OF A]
proof (cases "variable_peak R p ∨ function_peak R p")
case True
show ?thesis using left[OF True cps lab] by auto
next
case False
hence F: "variable_peak R (snd p,fst p) ∨ function_peak R (snd p,fst p)"
using local_peaks_cases[OF A] po by auto
hence "eldc R l r (snd p, fst p)" using left[OF F cps lab] by auto
thus ?thesis using eld_mirror by (metis fst_conv snd_conv surjective_pairing)
qed
qed
qed
qed
lemma trivial_peak_eld:
assumes eq: "t1 = t2"
and "((s1,r1,p1,σ1,True,t1),(s2,r2,p2,σ2,True,t2)) ∈ local_peaks R"
shows "eld R lab r ((s1,r1,p1,σ1,True,t1),(s2,r2,p2,σ2,True,t2))" (is "eld _ _ _ ?p")
unfolding eld_def
proof (intro exI conjI)
show "eld_conv lab r ?p (t1,[]) (t1, []) (t1,[]) (t2,[]) (t2, []) (t2,[])"
unfolding eld_conv_def ELD_1_def by auto
show "ld_trs R ?p (t1,[]) (t1, []) (t1,[]) (t2,[]) (t2,[]) (t2,[])"
using assms conv.intros(1) seq.intros(1) unfolding get_target_def ld_trs_def by auto
qed
lemma trivial_peak_eld_fan:
assumes eq: "t1 = t2"
and "((s1,r1,p1,σ1,True,t1),(s2,r2,p2,σ2,True,t2)) ∈ local_peaks R"
shows "eld_fan R lab r ((s1,r1,p1,σ1,True,t1),(s2,r2,p2,σ2,True,t2))" (is "eld_fan _ _ _ ?p")
unfolding eld_fan_def
proof (intro exI conjI)
show "eld_conv lab r ?p (t1,[]) (t1, []) (t1,[]) (t2,[]) (t2, []) (t2,[])"
unfolding eld_conv_def ELD_1_def by auto
show "ldc_trs R ?p (t1,[]) (t1, []) (t1,[]) (t2,[]) (t2,[]) (t2,[])"
using assms conv.intros(1) seq.intros(1) unfolding get_target_def ldc_trs_def by auto
show "fan R ?p (t1,[]) (t1, []) (t1,[]) (t2,[]) (t2,[]) (t2,[])"
unfolding fan_def get_source_def by auto
qed
lemma rstep_is_rstep_r_p_s: "rstep R = (⋃ (rl,p,σ). rstep_r_p_s R rl p σ)" proof
show "rstep R ⊆ (⋃(rl, p, σ). rstep_r_p_s R rl p σ)" proof
fix s t assume A:"(s, t) ∈ rstep R" show "(s,t) ∈ (⋃(rl, p, σ). rstep_r_p_s R rl p σ)" proof -
obtain rl p σ where "(s,t) ∈ rstep_r_p_s R rl p σ" using A rstep_iff_rstep_r_p_s by metis
thus ?thesis by blast
qed
qed
next
show "(⋃(rl, p, σ). rstep_r_p_s R rl p σ) ⊆ rstep R" proof
fix s t assume A: "(s,t) ∈ (⋃(rl, p, σ). rstep_r_p_s R rl p σ)" show "(s,t) ∈ rstep R" proof -
from A obtain l r p σ where "(s, t) ∈ rstep_r_p_s R (l, r) p σ" by auto
thus ?thesis using rstep_iff_rstep_r_p_s by metis
qed
qed
qed
lemma rstep_is_rstep_r_p_s_ast: "(⋃ (rl,p,σ). rstep_r_p_s R rl p σ)^* = (rstep R)^*" using rstep_is_rstep_r_p_s by metis
definition rlstep_r_p_s :: "('f,'v) trs ⇒ ('f,'v,'a) labeling ⇒ ('f,'v) rule ⇒ pos ⇒ ('f,'v) subst ⇒ 'a ⇒ ('f,'v) term rel"
where "rlstep_r_p_s R l rl p σ = (λa. {(s,t). (s,t) ∈ rstep_r_p_s R rl p σ ∧ a = l (s,rl,p,σ,True,t)})"
abbreviation label_trs :: "('f,'v) trs ⇒ ('f,'v,'a) labeling ⇒ 'a ⇒ ('f,'v) term rel" where
"label_trs R l ≡ λa. ⋃ (rl,p,σ) ∈ UNIV. rlstep_r_p_s R l rl p σ a"
lemma local_peak_introduce:
assumes "(s,t) ∈ rlstep_r_p_s R l rl1 p1 σ1 a" and "(s,u) ∈ rlstep_r_p_s R l rl2 p2 σ2 b"
shows "((s,rl1,p1,σ1,True,t),(s,rl2,p2,σ2,True,u)) ∈ local_peaks R" and "a = l (s,rl1,p1,σ1,True,t)" and "b = l (s,rl2,p2,σ2,True,u)"
using assms unfolding local_peaks_def rlstep_r_p_s_def apply auto using surjective_pairing by metis
lemma R_step_imp_lars_step:
assumes "(s,t) ∈ rstep_r_p_s R rl p σ"
shows "(s,t) ∈ label_trs R l (l (s,rl,p,σ,True,t))"
using assms unfolding rlstep_r_p_s_def by blast
lemma seq_imp_ast: assumes "ss ∈ seq R" and "set (map l (snd ss)) ⊆ ds r S"
defines "rel ≡ λ c. {(s,t). ∃ r p σ. (s,t) ∈ rstep_r_p_s R r p σ ∧ l (s,r,p,σ,True,t) = c}"
shows "(first ss,last ss) ∈ (⋃c ∈ ds r S. rel c)^*"
proof -
from assms obtain t ts where ss_dec: "ss = (t,ts)" by (metis surjective_pairing)
from assms show ?thesis unfolding ss_dec proof (induct ts arbitrary:t rule:list.induct)
case Nil hence "first (t,[]) = last (t,[])" by auto
thus ?case by auto
next
case (Cons x xs)
from Cons(2) obtain rl p σ u where x_dec: "x = (t,rl,p,σ,True,u)" by (cases, auto)
have step: "(t,u) ∈ rstep_r_p_s R rl p σ" using seq_chop_first Cons(2) unfolding x_dec by fast
have seq: "(u,xs) ∈ seq R" using seq_chop_first Cons(2) unfolding x_dec by fast
have lab: "l (t,rl,p,σ,True,u) ∈ ds r S" using step Cons(3) x_dec by auto
hence step: "(t,u) ∈ (UNION (ds r S) rel)" using step unfolding rel_def by fast
from Cons(1)[OF seq] Cons(3) have steps:"(first (u, xs), Decreasing_Diagrams2.last (u, xs)) ∈ (UNION (ds r S) rel)⇧*" unfolding x_dec rel_def by auto
thus ?case using step unfolding x_dec unfolding first.simps last.simps get_target_def apply auto by (metis converse_rtrancl_into_rtrancl local.step)
qed
qed
lemma seq_imp_refl: assumes "ss ∈ seq R" and "length (snd ss) ≤ 1" and "set (map l (snd ss)) ⊆ ds r S"
defines "rel ≡ λ c. {(s,t). ∃ r p σ. (s,t) ∈ rstep_r_p_s R r p σ ∧ l (s,r,p,σ,True,t) = c}"
shows "(first ss,last ss) ∈ (⋃c ∈ ds r S. rel c)^=" proof (cases "snd ss")
case Nil hence "first ss = last ss" by (cases "ss", auto)
thus ?thesis by auto
next
case (Cons x xs) hence ss_dec: "ss = (fst ss, x#xs)" using assms by (metis (erased, hide_lams) surjective_pairing)
hence seq:"(fst ss, x#xs) ∈ seq R" using assms by auto
then obtain t rl p σ u where x_dec: "x = (t,rl,p,σ,True,u)" by (cases, auto)
hence xs_dec: "xs = []" using assms Cons by auto
hence k: "(fst ss,(t,rl,p,σ,True,u)#[]) ∈ seq R" using ss_dec seq unfolding x_dec by auto
hence eq1: "fst ss = t" using seq.cases by (cases, auto)
hence ss_dec: "ss = (t,[x])" using ss_dec xs_dec by auto
from k have "(t,(t,rl,p,σ,True,u)#[]) ∈ seq R" by (cases, auto)
hence step: "(t,u) ∈ rstep_r_p_s R rl p σ" using seq_chop_first by fast
have lab: "l (t,rl,p,σ,True,u) ∈ ds r S" using assms ss_dec unfolding x_dec by (metis (erased, hide_lams) insert_iff list.simps(9) local.Cons set_simps(2) subsetCE x_dec)
have eq2: "last ss = u" unfolding ss_dec x_dec xs_dec last.simps get_target_def by auto
show ?thesis using step lab unfolding ss_dec first.simps last.simps x_dec get_target_def snd_conv rel_def by fastforce
qed
lemma eld_imp_fars_eld_step:
assumes la: "l (x,rl1,p1,s1,True,y) = a" and lb: "l (x,rl2,p2,s2,True,z) = b"
and eld: "eldc R l r ((x,rl1,p1,s1,True,y),(x,rl2,p2,s2,True,z))" (is "eldc R l r ?p")
and lab: "is_labeling R l r"
defines "rel ≡ λ c. {(s,t). ∃ r p σ. (s,t) ∈ rstep_r_p_s R r p σ ∧ l (s,r,p,σ,True,t) = c}"
shows "(∃y1 y2 z1 z2 v.
(y, y1) ∈ ((⋃c∈ds (fst r) {a}. rel c)⇧↔)⇧* ∧
(y1, y2) ∈ (⋃c∈ds (snd r) {b}. rel c)⇧= ∧
(y2, v) ∈ ((⋃c∈ds (fst r) {a, b}. rel c)⇧↔)⇧* ∧
(z, z1) ∈ ((⋃c∈ds (fst r) {b}. rel c)⇧↔)⇧* ∧
(z1, z2) ∈ (⋃c∈ds (snd r) {a}. rel c)⇧= ∧
(z2, v) ∈ ((⋃c∈ds (fst r) {a, b}. rel c)⇧↔)⇧* )"
proof -
from eld obtain jl1 jl2 jl3 jr1 jr2 jr3 where d: "ldc_trs R ((x, rl1, p1, s1,True, y), x, rl2, p2, s2,True, z) jl1 jl2 jl3 jr1 jr2 jr3"
and eld: "eld_conv l r ((x, rl1, p1, s1,True, y), x, rl2, p2, s2,True, z) jl1 jl2 jl3 jr1 jr2 jr3" unfolding eldc_def by auto
from d eld have jl1: "jl1 ∈ conv R" and fsty: "first jl1 = y" unfolding ldc_trs_def get_target_def by auto
then obtain σ1 σ2 σ3
where ml1: "map l (snd jl1) = σ1" and ml2: "map l (snd jl2) = σ2 " and ml3: "map l (snd jl3) = σ3"
and l1: "jl1 ∈ conv R" and l2: "jl2 ∈ seq R" and l3: "jl3 ∈ conv R"
and eld1: "ELD_1 r (l (fst ?p)) (l (snd ?p)) σ1 σ2 σ3" using eld d unfolding ldc_trs_def eld_conv_def by auto
have len2: "length (snd jl2) ≤ 1" using eld1 ml2 unfolding ELD_1_def using length_map by auto
hence eq_l1: "first jl1 = y" using fsty by blast
have m1: "set (map l (snd jl1)) ⊆ ds (fst r) {a}" using ml1 using eld1 unfolding ELD_1_def fst_conv snd_conv la lb by auto
have l1: "(first jl1,last jl1) ∈ ((⋃c ∈ ds (fst r) {a}. rel c)⇧↔)^*" using conv_imp_conv[OF l1 m1] lab unfolding rel_def by (cases r) auto
have m2: "set (map l (snd jl2)) ⊆ ds (snd r) {b}" using ml2 using eld1 unfolding ELD_1_def fst_conv snd_conv la lb by auto
have l2: "(first jl2,last jl2) ∈ (⋃c ∈ ds (snd r) {b}. rel c)^=" using seq_imp_refl[OF l2 len2 m2] eld unfolding rel_def by fast
have m3: "set (map l (snd jl3)) ⊆ ds (fst r) {a,b}" using ml3 using eld1 unfolding ELD_1_def fst_conv snd_conv la lb ds_def by auto
have l3: "(first jl3,last jl3) ∈ ((⋃c ∈ ds (fst r) {a,b}. rel c)⇧↔)^*" using conv_imp_conv[OF l3 m3] eld lab unfolding rel_def by (cases r) auto
from d eld have jr1: "jr1 ∈ conv R" and fstz: "first jr1 = z" unfolding ldc_trs_def get_target_def by auto
then obtain τ1 τ2 τ3
where mr1: "map l (snd jr1) = τ1" and mr2: "map l (snd jr2) = τ2" and mr3: "map l (snd jr3) = τ3"
and r1: "jr1 ∈ conv R" and r2: "jr2 ∈ seq R" and r3: "jr3 ∈ conv R"
and eld1: "ELD_1 r (l (snd ?p)) (l (fst ?p)) τ1 τ2 τ3" using eld d unfolding ldc_trs_def eld_conv_def by auto
have len2: "length (snd jr2) ≤ 1" using eld1 mr2 unfolding ELD_1_def using length_map by auto
have m1: "set (map l (snd jr1)) ⊆ ds (fst r) {b}" using mr1 using eld1 unfolding ELD_1_def fst_conv snd_conv la lb by auto
have r1: "(first jr1,last jr1) ∈ ((⋃c ∈ ds (fst r) {b}. rel c)⇧↔)^*" using conv_imp_conv[OF r1 m1] eld lab unfolding rel_def by (cases r) auto
have m2: "set (map l (snd jr2)) ⊆ ds (snd r) {a}" using mr2 using eld1 unfolding ELD_1_def fst_conv snd_conv la lb by auto
have r2: "(first jr2,last jr2) ∈ (⋃c ∈ ds (snd r) {a}. rel c)^=" using seq_imp_refl[OF r2 len2 m2] eld unfolding rel_def by fast
have m3: "set (map l (snd jr3)) ⊆ ds (fst r) {a,b}" using mr3 using eld1 unfolding ELD_1_def fst_conv snd_conv la lb ds_def by auto
have r3: "(first jr3,last jr3) ∈ ((⋃c ∈ ds (fst r) {a,b}. rel c)⇧↔)^*" using conv_imp_conv[OF r3 m3] eld lab unfolding rel_def by (cases r) auto
have eq: "last jl1 = first jl2" "last jl2 = first jl3"
"last jr1 = first jr2" "last jr2 = first jr3"
"last jl3 = last jr3" using d unfolding ldc_trs_def by auto
show ?thesis using l1 l2 l3 r1 r2 r3 unfolding eq using fsty fstz by blast
qed
lemma eld_imp_fars_eld:
assumes lp: "∀ p ∈ local_peaks R. eldc R l r p"
and lab: "is_labeling R l r"
shows "fars_eld (fst r) (snd r) (λ c. {(s,t). ∃ r p σ. (s,t) ∈ (rstep_r_p_s R r p σ) ∧ l (s,r,p,σ,True,t) = c})" (is "fars_eld _ _ ?rel")
proof -
{ fix a b x y z
assume "(x, y) ∈ {(s, t). ∃r p σ. (s, t) ∈ rstep_r_p_s R r p σ ∧ l (s, r, p, σ, True, t) = a}"
and "(x, z) ∈ {(s, t). ∃r p σ. (s, t) ∈ rstep_r_p_s R r p σ ∧ l (s, r, p, σ, True, t) = b}"
then obtain rl1 p1 s1 rl2 p2 s2 where
"(x,y) ∈ rstep_r_p_s R rl1 p1 s1" and la:"l (x,rl1,p1,s1, True,y) = a" and
"(x,z) ∈ rstep_r_p_s R rl2 p2 s2" and lb:"l (x,rl2,p2,s2, True,z) = b"
by auto
hence lp_mem: "((x,rl1,p1,s1, True,y),(x,rl2,p2,s2, True,z)) ∈ local_peaks R" (is "?p ∈ _")
unfolding local_peaks_def by fast
hence eld: "eldc R l r ?p" using lp by auto
have "(∃y1 y2 z1 z2 v. (y, y1) ∈ ((⋃c∈ds (fst r) {a}. ?rel c)⇧↔)⇧* ∧ (y1, y2) ∈ (⋃c∈ds (snd r) {b}. ?rel c)⇧= ∧ (y2, v) ∈ ((⋃c∈ds (fst r) {a, b}. ?rel c)⇧↔)⇧* ∧
(z, z1) ∈ ((⋃c∈ds (fst r) {b}. ?rel c)⇧↔)⇧* ∧ (z1, z2) ∈ (⋃c∈ds (snd r) {a}. ?rel c)⇧= ∧ (z2, v) ∈ ((⋃c∈ds (fst r) {a, b}. ?rel c)⇧↔)⇧* )"
using eld_imp_fars_eld_step[OF la lb eld lab] unfolding rel_def by auto
}
thus ?thesis unfolding fars_eld_def rel_def unfolding ds_to_under
apply (intro allI)
subgoal premises p for x y z a b using p[of x y a z b] by blast
done
qed
lemma main:
assumes "rel_props (fst r) (snd r)"
and lab: "compatible R l r"
and dec: "∀ (b, p) ∈ critical_peaks R. eldc R l r p"
shows "CR (rstep R)"
proof -
let ?rel = "λ c. {(s,t). ∃ r p σ. ((s,t) ∈ rstep_r_p_s R r p σ ∧ l (s,r,p,σ,True,t) = c)}"
from assms have i: "irrefl (fst r)" unfolding rel_props_def by (metis irrefl_def wf_not_sym)
have lp: "∀p ∈ local_peaks R. eldc R l r p" using main_eld[OF dec lab] by fast
have eq: "(⋃c∈UNIV. ?rel c) = (rstep R)" (is "?l = _") unfolding rstep_is_rstep_r_p_s using assms apply auto by blast
hence fars_eld: "fars_eld (fst r) (snd r) ?rel" using eld_imp_fars_eld[OF lp] lab[unfolded compatible_def] by auto
thus ?thesis using fars_eld_imp_cr[OF assms(1) fars_eld] eq by auto
qed
lemma parallel_peak_close:
assumes "parallel_peak R p"
shows "∃ s rl1 p1 σ1 t rl2 p2 σ2 u v.(
p = ((s,rl1,p1,σ1,True,t),(s,rl2,p2,σ2,True,u)) ∧
(s,t) ∈ rstep_r_p_s R rl1 p1 σ1 ∧
(s,u) ∈ rstep_r_p_s R rl2 p2 σ2 ∧
(t,v) ∈ rstep_r_p_s R rl2 p2 σ2 ∧
(u,v) ∈ rstep_r_p_s R rl1 p1 σ1
)" proof -
from assms(1) obtain r1 p1 s1 t s r2 p2 s2 u where p: "p ∈ local_peaks R" and p_dec: "p = ((s,r1,p1,s1,True,t),(s,r2,p2,s2,True,u))" and b:"parallel_pos p1 p2" unfolding parallel_peak_def local_peaks_def Let_def by fast
hence s1: "(s,t) ∈ rstep_r_p_s R r1 p1 s1" and s2: "(s,u) ∈ rstep_r_p_s R r2 p2 s2" unfolding local_peaks_def by auto
obtain v where j1: "(t,v) ∈ rstep_r_p_s R r2 p2 s2" and j2:"(u,v) ∈ rstep_r_p_s R r1 p1 s1" using parallel_steps[OF _ _ b] s1 s2 surj_pair by metis
thus ?thesis using s1 s2 p_dec by fast
qed
lemma local_peaks_intros:
assumes "parallel_peak R p"
shows "p ∈ local_peaks R"
using assms unfolding parallel_peak_def by auto
lemma diamond_trs_and_weld_seq_imp_eld:
assumes "diamond_trs R p jl jr"
and weld_seq: "weld_seq l r p jl jr"
shows "eldc R l r p"
proof -
from assms have ldc_trs: "ldc_trs R p (get_target (fst p),[]) jl (last jl,[]) (get_target (snd p),[]) jr (last jr,[])"
(is "ldc_trs _ _ ?jl1 _ ?jl3 ?jr1 _ ?jr3") unfolding ldc_trs_def diamond_trs_def by auto
have "eld_conv l r p ?jl1 jl ?jl3 ?jr1 jr ?jr3" proof -
have "∀a∈set (map l (snd jl)). (a, l (snd p)) ∈ snd r" using assms unfolding weld_seq_def labels_def ds_def by auto
hence l: "ELD_1 r (l (fst p)) (l (snd p)) [] (map l (snd jl)) []" using assms unfolding diamond_trs_def weld_seq_def ELD_1_def ds_def by auto
have lx: "map l (snd jl) = [] @ map l (snd jl) @ []" by auto
have "∀a∈set (map l (snd jr)). (a, l (fst p)) ∈ snd r" using assms unfolding weld_seq_def labels_def ds_def by auto
hence r: "ELD_1 r (l (snd p)) (l (fst p)) [] (map l (snd jr)) []" using assms unfolding diamond_trs_def weld_seq_def ELD_1_def ds_def by auto
have rx: "map l (snd jr) = [] @ map l (snd jr) @ []" by auto
show ?thesis using l lx r rx unfolding eld_conv_def get_target_def by auto
qed
thus ?thesis using ldc_trs unfolding eldc_def by fast
qed
fun rule_labeling :: "(('f,'v) rule ⇒ nat) ⇒ ('f,'v) step ⇒ nat"
where "rule_labeling i (s,rl,p,σ,t) = i rl"
lemma rl_is_labeling: "is_labeling R (rule_labeling i) r" unfolding is_labeling_def by auto
lemma rl_parallel:
assumes r: "refl (snd r)"
and "parallel_peak R p"
shows "eldc R (rule_labeling i) r p"
proof -
obtain s rl1 p1 σ1 t rl2 p2 σ2 u v where
p_dec: "p = ((s,rl1,p1,σ1,True,t),(s,rl2,p2,σ2,True,u))" (is "p = ?p") and
steps: "(s,t) ∈ rstep_r_p_s R rl1 p1 σ1 ∧
(s,u) ∈ rstep_r_p_s R rl2 p2 σ2 ∧
(t,v) ∈ rstep_r_p_s R rl2 p2 σ2 ∧
(u,v) ∈ rstep_r_p_s R rl1 p1 σ1" using parallel_peak_close[OF assms(2)] by fast
have lp: "p ∈ local_peaks R" using local_peaks_intros[OF assms(2)] by auto
from steps have jl: "(t,[(t,rl2,p2,σ2,True,v)]) ∈ seq R" (is "?jl ∈ _") using seq.intros by fast
from steps have jr: "(u,[(u,rl1,p1,σ1,True,v)]) ∈ seq R" (is "?jr ∈ _") using seq.intros by fast
have diamond_trs: "diamond_trs R ?p ?jl ?jr" using lp jl jr conv.intros unfolding p_dec ldc_trs_def last.simps get_target_def diamond_trs_def by auto
have weld_seq: "weld_seq (rule_labeling i) r ?p ?jl ?jr" unfolding weld_seq_def labels_def ds_def apply auto using r apply (metis UNIV_I refl_on_def) using r by (metis UNIV_I refl_on_def)
thus ?thesis using diamond_trs_and_weld_seq_imp_eld[OF diamond_trs weld_seq] unfolding p_dec by metis
qed
lemma rl_variable:
assumes r: "refl (snd r)"
and vp: "variable_peak R p"
and lin: "linear_trs R"
shows "eldc R (rule_labeling i) r p"
proof -
from assms have p: "p ∈ local_peaks R" unfolding variable_peak_def by auto
from assms variable_peak_decompose[OF vp] obtain s t u l1 r1 p1 σ1 l2 r2 p2 σ2 q q1 q2 w where
p_dec: "p = ((s, (l1, r1), p1, σ1,True, t), s, (l2, r2), p2, σ2,True, u)" and
s1: "(s, t) ∈ rstep_r_p_s R (l1, r1) p1 σ1" and s2: "(s, u) ∈ rstep_r_p_s R (l2, r2) p2 σ2" and
rest: "p1 <#> q = p2" "q1 <#> q2 = q" "q1 ∈ poss l1" "l1 |_ q1 = Var w" by fast
let ?σ3 = "(λy. if y = w then (ctxt_of_pos_term q2 (σ1 y))⟨r2 ⋅ σ2⟩ else σ1 y)"
let ?v = "(ctxt_of_pos_term p1 s)⟨r1 ⋅ ?σ3⟩"
from lin have linl1: "linear_term l1" and linl2: "linear_term r1" using s1 s2 unfolding rstep_r_p_s_def linear_trs_def Let_def by auto
from variable_steps_lin[OF s1 s2 rest linl1] linl2 have
sr: "(u, ?v) ∈ rstep_r_p_s R (l1, r1) p1 ?σ3" and
sl: "t = ?v ∨ (∃q. q ∈ poss r1 ∧ r1 |_ q = Var w ∧ (t, ?v) ∈ rstep_r_p_s R (l2, r2) (p1 <#> q <#> q2) σ2)" unfolding linear_trs_def by auto
have jr: "(u,[(u,(l1,r1),p1,?σ3,True,?v)]) ∈ seq R" (is "?jr ∈ _") using rstep_is_seq[OF sr] by auto
show ?thesis proof (cases "t = ?v")
case True hence jl: "(t,[]) ∈ seq R" (is "?jl ∈ _") using seq.intros by auto
have "last ?jl = get_target (fst p)" unfolding p_dec last.simps get_target_def by auto
hence diamond_trs: "diamond_trs R p ?jl ?jr" using p jl jr True unfolding diamond_trs_def ldc_trs_def p_dec get_target_def apply auto
using conv.intros(1) apply blast
using conv.intros(1) apply blast
using conv.intros(1) apply blast
by (simp add: get_target_def)
have weld_seq: "weld_seq (rule_labeling i) r p ?jl ?jr" unfolding weld_seq_def labels_def p_dec ds_def apply auto using r by (metis (poly_guards_query) UNIV_I refl_on_def)
thus ?thesis using diamond_trs_and_weld_seq_imp_eld[OF diamond_trs weld_seq] by fast
next
case False then obtain q where sl: "(t, ?v) ∈ rstep_r_p_s R (l2, r2) (p1 <#> q <#> q2) σ2" using sl by auto
hence jl: "(t,[(t,(l2,r2),p1<#>q<#>q2,σ2,True,?v)]) ∈ seq R" (is "?jl ∈ _") using rstep_is_seq[OF sl] by auto
hence diamond_trs: "diamond_trs R p ?jl ?jr" using p jl jr False unfolding diamond_trs_def ldc_trs_def p_dec get_target_def apply auto
using conv.intros(1) apply blast
using conv.intros(1) apply blast
using conv.intros(1) apply blast
using conv.intros(1) apply blast
by (auto simp add: get_target_def)
have weld_seq: "weld_seq (rule_labeling i) r p ?jl ?jr" unfolding weld_seq_def labels_def p_dec ds_def apply auto using r apply (metis UNIV_I refl_on_def) using r by (metis UNIV_I refl_on_def)
thus ?thesis using diamond_trs_and_weld_seq_imp_eld[OF diamond_trs weld_seq] by fast
qed
qed
lemma rule_labeling_is_compatible:
assumes r: "refl (snd r)"
and lin: "linear_trs R"
shows "compatible R (rule_labeling i) r"
unfolding compatible_def using assms rl_is_labeling rl_variable[OF r _ lin] rl_parallel by blast
lemma rule_labeling_has_rel_props:
defines "r ≡ ({(n,m). n < (m::nat)},{(n,m). n ≤ (m::nat)})"
shows "rel_props (fst r) (snd r)"
proof -
have r: "refl (snd r)" using r_def apply auto by (simp add: refl_on_def)
have t1: "trans (fst r)" using r_def apply auto by (metis less_trans transp_def transp_trans)
have t2: "trans (snd r)" using r_def apply auto by (metis order_trans transp_def transp_trans)
have wf: "wf (fst r)" using r_def apply auto by (metis wf_less)
have compat: "snd r O fst r O snd r ⊆ fst r" unfolding r_def by auto
have "rel_props (fst r) (snd r)" unfolding rel_props_def using t1 t2 wf r compat by auto
thus ?thesis by auto
qed
corollary rule_labeling_is_sound:
defines "r ≡ ({(n,m). n < (m::nat)},{(n,m). n ≤ (m::nat)})"
assumes lin: "linear_trs R"
and dec: "∀ (b,p) ∈ critical_peaks R. eldc R (rule_labeling i) r p" (is "∀ (b,p) ∈ _ . eldc _ ?l ?r _")
shows "CR (rstep R)"
proof -
have r: "refl (snd r)" using r_def apply auto by (simp add: refl_on_def)
have lab: "compatible R (rule_labeling i) ?r" using rule_labeling_is_compatible[OF r lin] by auto
have props: "rel_props (fst r) (snd r)" using rule_labeling_has_rel_props r_def by fast
show ?thesis using main[OF props lab dec] by auto
qed
fun source_labeling :: "('f,'v) step ⇒ ('f,'v) term"
where "source_labeling (s,rl,p,σ,t) = s"
fun sl_rel :: "('f,'v) trs ⇒ ('f,'v) trs ⇒ (('f,'v) term) relp"
where "sl_rel R S = (((relto (rstep R) (rstep S))^+)¯,((rstep S ∪ rstep R)^* )¯)"
lemma sl_is_labeling:
"is_labeling (R∪S) source_labeling (sl_rel R S)"
proof -
{fix s a b t u C ρ σ1 aa p1 ba v σ2 p2
assume C:"(u, s) ∈ ((rstep S)⇧* O rstep R O (rstep S)⇧* )⇧+" (is "_ ∈ ?rel^+")
then obtain n where n1: "n > 0" and n:"(u,s) ∈ ?rel^^n" by (metis trancl_power)
from n have "(C⟨u ⋅ ρ⟩, C⟨s ⋅ ρ⟩) ∈ ?rel^^n" proof (induct n arbitrary:u)
case 0 thus ?case by auto
next
case (Suc n) then obtain v where step: "(u,v) ∈ ?rel" and steps: "(v,s) ∈ ?rel^^n" by (metis relpow_Suc_E2)
from step obtain u' v' where "(u,u') ∈ (rstep S)^*" and "(u',v') ∈ rstep R" and "(v',v) ∈ (rstep S)^*" by auto
then obtain u' v' where "(C⟨u⋅ρ⟩,C⟨u'⋅ρ⟩) ∈ (rstep S)^*" and "(C⟨u'⋅ρ⟩,C⟨v'⋅ρ⟩) ∈ rstep R" and "(C⟨v'⋅ρ⟩,C⟨v⋅ρ⟩) ∈ (rstep S)^*"
by (metis rstep.ctxt rstep.subst rsteps_closed_ctxt rsteps_closed_subst)
hence 1:"(C⟨u⋅ρ⟩,C⟨v⋅ρ⟩) ∈ ?rel" by auto
from steps have 2:"(C⟨v⋅ρ⟩,C⟨s⋅ρ⟩) ∈ ?rel^^n" using Suc by auto
show ?case using 1 2 by (metis relpow_Suc_I2)
qed
hence "((C⟨u ⋅ ρ⟩, C⟨s ⋅ ρ⟩) ∈ ?rel^+)" using n1 by (metis trancl_power)
} note A = this
{fix s a b t u C ρ σ1 aa p1 ba v σ2 p2
assume "(u, s) ∈ (rstep S ∪ rstep R)⇧*"
hence "(C⟨u ⋅ ρ⟩, C⟨s ⋅ ρ⟩) ∈ (rstep S ∪ rstep R)⇧*" by (metis rstep_union rsteps_closed_ctxt rsteps_closed_subst)
}
thus ?thesis using A unfolding is_labeling_def step_close.simps by auto
qed
lemma sl_par:
assumes pp: "parallel_peak (R∪S) p"
shows "weld (R∪S) source_labeling (sl_rel R S) p" (is "weld _ _ ?r _")
proof -
obtain s rl1 p1 σ1 t rl2 p2 σ2 u v where
p_dec: "p = ((s,rl1,p1,σ1,True,t),(s,rl2,p2,σ2,True,u))" and
steps: "(s,t) ∈ rstep_r_p_s (R∪S) rl1 p1 σ1 ∧
(s,u) ∈ rstep_r_p_s (R∪S) rl2 p2 σ2 ∧
(t,v) ∈ rstep_r_p_s (R∪S) rl2 p2 σ2 ∧
(u,v) ∈ rstep_r_p_s (R∪S) rl1 p1 σ1" using parallel_peak_close[OF assms] by fast
have lp: "p ∈ local_peaks (R∪S)" using local_peaks_intros[OF assms] by auto
from steps have jl: "(t,[(t,rl2,p2,σ2,True,v)]) ∈ seq (R∪S)" (is "?jl ∈ _") using seq.intros by fast
from steps have jr: "(u,[(u,rl1,p1,σ1,True,v)]) ∈ seq (R∪S)" (is "?jr ∈ _") using seq.intros by fast
have diamond_trs: "diamond_trs (R∪S) p ?jl ?jr" using lp jl jr unfolding p_dec diamond_trs_def ldc_trs_def last.simps get_target_def
apply auto
using conv.intros(1) apply blast
using conv.intros(1) apply blast
using conv.intros(1) apply blast
using conv.intros(1) by blast
from steps have s1:"(s,t) ∈ rstep (R ∪ S)" using rstep_r_p_s_imp_rstep by fast
from steps have s2:"(s,u) ∈ rstep (R ∪ S)" using rstep_r_p_s_imp_rstep by fast
have weld_seq: "weld_seq source_labeling ?r p ?jl ?jr" unfolding weld_seq_def labels_def p_dec ds_def apply auto
using s1 s2 unfolding ds_def by auto
show ?thesis using diamond_trs weld_seq unfolding weld_def ld2_trs_def diamond_trs_def by fast
qed
lemma sl_evar:
assumes vp: "variable_peak (R∪S) p" (is "variable_peak ?R _")
and lin: "linear_trs (R∪S)"
shows "weld (R∪S) source_labeling (sl_rel R S) p"
proof -
from assms have p: "p ∈ local_peaks ?R" unfolding variable_peak_def by auto
from assms variable_peak_decompose[OF vp] obtain s t u l1 r1 p1 σ1 l2 r2 p2 σ2 q q1 q2 w where
p_dec: "p = ((s, (l1, r1), p1, σ1,True, t), s, (l2, r2), p2, σ2,True, u)" and
s1: "(s, t) ∈ rstep_r_p_s ?R (l1, r1) p1 σ1" and s2: "(s, u) ∈ rstep_r_p_s ?R (l2, r2) p2 σ2" and
rest: "p1 <#> q = p2" "q1 <#> q2 = q" "q1 ∈ poss l1" "l1 |_ q1 = Var w" by fast
let ?σ3 = "(λy. if y = w then (ctxt_of_pos_term q2 (σ1 y))⟨r2 ⋅ σ2⟩ else σ1 y)"
let ?v = "(ctxt_of_pos_term p1 s)⟨r1 ⋅ ?σ3⟩"
from s1 lin have l:"linear_term l1 ∧ linear_term r1" unfolding rstep_r_p_s_def Let_def linear_trs_def by auto
from variable_steps_lin[OF s1 s2 rest] l have
sr: "(u, ?v) ∈ rstep_r_p_s ?R (l1, r1) p1 ?σ3" and
sl: "t = ?v ∨ (∃q. q ∈ poss r1 ∧ r1 |_ q = Var w ∧ (t, ?v) ∈ rstep_r_p_s ?R (l2, r2) (p1 <#> q <#> q2) σ2)" by auto
have jr: "(u,[(u,(l1,r1),p1,?σ3,True,?v)]) ∈ seq ?R" (is "?jr ∈ _") using rstep_is_seq[OF sr] by auto
show ?thesis proof (cases "t = ?v")
case True hence jl: "(t,[]) ∈ seq ?R" (is "?jl ∈ _") using seq.intros by auto
have "last ?jl = get_target (fst p)" unfolding p_dec last.simps get_target_def by auto
hence diamond_trs: "diamond_trs ?R p ?jl ?jr" using p jl jr True unfolding diamond_trs_def ldc_trs_def p_dec apply auto
using conv.intros(1) apply blast
using conv.intros(1) apply blast
using conv.intros(1) apply blast
by (auto simp add: get_target_def)
have "weld_seq source_labeling (sl_rel R S) p ?jl ?jr"
unfolding weld_seq_def labels_def p_dec ds_def apply auto using s2
by (metis (erased, hide_lams) inf_sup_aci(5) r_into_rtrancl rstep_r_p_s_imp_rstep rstep_union)
thus ?thesis using diamond_trs unfolding weld_def diamond_trs_def ld2_trs_def by fast
next
case False then obtain q where sl: "(t, ?v) ∈ rstep_r_p_s ?R (l2, r2) (p1 <#> q <#> q2) σ2" using sl by auto
hence jl: "(t,[(t,(l2,r2),p1<#>q<#>q2,σ2,True,?v)]) ∈ seq ?R" (is "?jl ∈ _") using rstep_is_seq[OF sl] by auto
hence diamond_trs: "diamond_trs ?R p ?jl ?jr" using p jl jr unfolding diamond_trs_def ldc_trs_def p_dec get_target_def apply auto
using conv.intros(1) apply blast
using conv.intros(1) apply blast
using conv.intros(1) apply blast
using conv.intros(1) apply blast
by (auto simp add: get_target_def)
have r: "refl (snd (sl_rel R S))" by (auto intro: refl_rtrancl)
have weld_seq: "weld_seq source_labeling (sl_rel R S) p ?jl ?jr"
unfolding weld_seq_def labels_def p_dec ds_def apply auto
using s1 apply (metis (erased, hide_lams) inf_sup_aci(5) r_into_rtrancl rstep_r_p_s_imp_rstep rstep_union)
using s2 by (metis (erased, hide_lams) inf_sup_aci(5) r_into_rtrancl rstep_r_p_s_imp_rstep rstep_union)
thus ?thesis using diamond_trs unfolding weld_def diamond_trs_def ld2_trs_def by fast
qed
qed
lemma source_labeling_is_weakly_compatible:
assumes lin: "linear_trs (R ∪ S)"
shows "weakly_compatible (R ∪ S) source_labeling (sl_rel R S)"
using sl_is_labeling sl_par sl_evar lin
unfolding weakly_compatible_def weld_def eld_def eld_conv_def weld_seq_def
by fast
definition rel_rstep :: "('f,'v) trs ⇒ ('f,'v) trs ⇒ (('f,'v) term) rel"
where "rel_rstep R S = relto (rstep R) (rstep S)"
lemma S_RS:
assumes "(s,t) ∈ (rstep S)^*"
and "(t,u) ∈ relto (rstep R) (rstep S)"
shows "(s,u) ∈ relto (rstep R) (rstep S)"
using assms(2) rtrancl_trans[OF assms(1)] by auto
lemma S_RS_trancl:
assumes "(s,t) ∈ (rstep S)^*"
and "(t,u) ∈ (relto (rstep R) (rstep S))^+"
shows "(s,u) ∈ (relto (rstep R) (rstep S))^+" (is "_ ∈ ?R^+")
proof -
from assms obtain m where "(t,m) ∈ ?R" and mu:"(m,u) ∈ ?R^*" by (auto dest!: tranclD)
hence "(s,m) ∈ ?R" using assms(1) S_RS by metis
thus ?thesis using mu by auto
qed
lemma RS_S:
assumes "(t, u) ∈ relto (rstep R) (rstep S)"
and "(u, v) ∈ (rstep S)⇧*"
shows "(t, v) ∈ relto (rstep R) (rstep S)"
using assms by force
lemma RS_S_trancl:
assumes "(t,u) ∈ (relto (rstep R) (rstep S))^+"
and "(u,v) ∈ (rstep S)^*"
shows "(t,v) ∈ (relto (rstep R) (rstep S))^+" (is "_ ∈ ?R")
proof -
from assms obtain m where "(t,m) ∈ ?R^*" and "(m,u) ∈ ?R" by blast
thus ?thesis using assms RS_S rtrancl_into_trancl1 tranclD2 by metis
qed
lemma rel_compat:
assumes "(s,t) ∈ (rstep S ∪ rstep R)^*"
and "(t,u) ∈ (rel_rstep R S)^+"
and "(u,v) ∈ (rstep S ∪ rstep R)^*"
shows "(s,v) ∈ (rel_rstep R S)^+"
proof -
have k: "(rstep S ∪ rstep R)^* ⊆ ((rstep S)^* ∪ (relto (rstep R) (rstep S))^*)" by regexp
from k have ab: "(s,t) ∈ (relto (rstep R) (rstep S))^* ∨ (s,t) ∈ (rstep S)^*" (is "?a ∨ ?b") using assms by auto
from k have cd:"(u,v) ∈ (relto (rstep R) (rstep S))^* ∨ (u,v) ∈ (rstep S)^*" (is "?c ∨ ?d") using assms by auto
have su: "(s,u) ∈ (relto (rstep R) (rstep S))^+"
proof (cases "?a")
case True thus ?thesis using assms unfolding rel_rstep_def by (metis rtrancl_trancl_trancl)
next
case False hence "?b" using ab by auto
thus ?thesis using assms(2) unfolding rel_rstep_def using S_RS_trancl by metis
qed
thus ?thesis
proof (cases "?c")
case True thus ?thesis unfolding rel_rstep_def using su by (metis True trancl_rtrancl_trancl)
next
case False hence "?d" using cd by auto
thus ?thesis using su unfolding rel_rstep_def using RS_S_trancl by metis
qed
qed
corollary source_labeling_and_SN_is_sound:
fixes R S
defines "r ≡ sl_rel R S"
assumes lin: "linear_trs (R∪S)" (is "linear_trs ?R")
and SN: "SN (rstep (R∪S))"
and dec: "∀(b,p) ∈ critical_peaks (R∪S). eldc (R∪S) source_labeling r p"
shows "CR (rstep (R∪S))"
proof -
have lab: "compatible ?R source_labeling r"
using source_labeling_is_weakly_compatible[OF lin] using linear_and_weakly_compatible_is_compatible[OF lin]
unfolding r_def by auto
have t1: "trans (fst r)" unfolding r_def sl_rel.simps by auto
have t2: "trans (snd r)" unfolding r_def sl_rel.simps by (auto intro: trans_rtrancl)
have SN_R:"SN (rstep R)" and SN_S:"SN (rstep S)" using SN apply (metis SN_subset Un_left_absorb rstep_union subset_Un_eq)
by (metis (erased, hide_lams) SN SN_subset le_sup_iff rstep_union subset_refl)
have "SN_rel (rstep R) (rstep S)"
proof -
have "SN_rel_on_alt (rstep (R ∪ S)) {} (Collect top)" by (metis SN SN_rel_empty2 SN_rel_on_conv top_set_def)
hence "∃x⇩1. SN_rel_on_alt x⇩1 {} (Collect top) ∧ rstep R ⊆ x⇩1 ∧ rstep S ⊆ x⇩1" using rstep_union by auto
thus "SN_rel (rstep R) (rstep S)" by (metis (no_types) SN_rel_mono' SN_rel_on_conv sup_bot.right_neutral top_set_def)
qed
hence "SN ((fst r)¯)" using SN_R by (auto simp: r_def SN_imp_SN_trancl SN_rel_on_def)
hence wf: "wf (fst r)" using r_def SN_iff_wf by auto
have r: "refl (snd r)" using r_def by (auto intro: refl_rtrancl)
have compat: "snd r O fst r O snd r ⊆ fst r" unfolding r_def apply auto
using rel_compat unfolding rel_rstep_def by metis
have rel_props:"rel_props (fst r) (snd r)" unfolding rel_props_def
using t1 t2 wf r compat r_def by auto
from lin have ll: "left_linear_trs (R∪S)" unfolding left_linear_trs_def linear_trs_def by auto
show ?thesis using main[OF rel_props lab dec] by fast
qed
lemma rl_variable2:
assumes r: "refl (snd r)"
and vp: "variable_peak R p"
and ll: "left_linear_trs R"
shows "weld R (rule_labeling i) r p"
proof -
from assms have p: "p ∈ local_peaks R" unfolding variable_peak_def by auto
from assms variable_peak_decompose[OF vp] obtain s t u l1 r1 p1 σ1 l2 r2 p2 σ2 q q1 q2 w where
p_dec: "p = ((s, (l1, r1), p1, σ1,True, t), s, (l2, r2), p2, σ2,True, u)" and
s1: "(s, t) ∈ rstep_r_p_s R (l1, r1) p1 σ1" and s2: "(s, u) ∈ rstep_r_p_s R (l2, r2) p2 σ2" and
rest: "p1 <#> q = p2" "q1 <#> q2 = q" "q1 ∈ poss l1" "l1 |_ q1 = Var w" by fast
let ?σ3 = "(λy. if y = w then (ctxt_of_pos_term q2 (σ1 y))⟨r2 ⋅ σ2⟩ else σ1 y)"
let ?v = "(ctxt_of_pos_term p1 s)⟨r1 ⋅ ?σ3⟩"
from ll have ll1: "linear_term l1" using s1 s2 unfolding rstep_r_p_s_def left_linear_trs_def Let_def by auto
show ?thesis
proof (cases "linear_term r1")
case False
from variable_steps_left_lin[OF s1 s2 rest ll1] obtain steps where
sr: "(u, ?v) ∈ rstep_r_p_s R (l1, r1) p1 ?σ3" and
sl: "∀i<length steps. fst (steps ! i) = (l2, r2)" "(t, steps, ?v) ∈ par_rstep2 R" unfolding linear_trs_def by auto
have jr: "(u,[(u,(l1,r1),p1,?σ3,True,?v)]) ∈ seq R" (is "?jr ∈ _") using rstep_is_seq[OF sr] by auto
obtain jl where "jl ∈ seq R" and "first jl = t" and "last jl = ?v"
and jl_lab: "∀i < length (snd jl). fst (snd (snd jl ! i)) = (l2,r2)"
using par_rstep2_imp_seq sl unfolding get_rule_def by force
hence d: "ldc_trs R p (get_target (fst p),[]) (get_target (fst p),[]) jl (get_target (snd p),[]) (get_target (snd p),[]) ?jr"
using p jr by (auto intro: conv.intros seq.intros seq_imp_conv simp: get_target_def ldc_trs_def p_dec)
hence d2: "ld2_trs R p jl ?jr" using False unfolding ld2_trs_def p_dec get_rule_def ldc_trs_def
using ‹jl ∈ seq R› jr by (auto intro: conv.intros simp: get_target_def)
have "weld_seq (rule_labeling i) r p jl ?jr" unfolding weld_seq_def p_dec labels_def using jl_lab r
unfolding ds_def apply auto apply (metis UNIV_I fst_conv in_set_conv_nth refl_onD snd_conv)
by (metis UNIV_I refl_onD)
thus ?thesis unfolding weld_def using d2 by fast
next
case True
hence l: "linear_term r1" by auto
from variable_steps_lin[OF s1 s2 rest ll1] l have
sr: "(u, ?v) ∈ rstep_r_p_s R (l1, r1) p1 ?σ3" and
sl: "t = ?v ∨ (∃q. q ∈ poss r1 ∧ r1 |_ q = Var w ∧ (t, ?v) ∈ rstep_r_p_s R (l2, r2) (p1 <#> q <#> q2) σ2)"
unfolding linear_trs_def by auto
have jr: "(u,[(u,(l1,r1),p1,?σ3,True,?v)]) ∈ seq R" (is "?jr ∈ _") using rstep_is_seq[OF sr] by auto
show ?thesis
proof (cases "t = ?v")
case True
hence jl: "(t,[]) ∈ seq R" (is "?jl ∈ _") using seq.intros by auto
have "?jl ∈ seq R" using jl by auto
moreover have "length (snd ?jl) ≤ 1" by auto
moreover have "first ?jl = t" by auto
moreover have lastl: "last ?jl = ?v" using True by auto
ultimately have jl: "?jl ∈ seq R ∧ length (snd ?jl) ≤ 1 ∧ first ?jl = t ∧ last ?jl = ?v" by auto
have "p ∈ local_peaks R" using s1 s2 unfolding p_dec local_peaks_def by auto
hence "ldc_trs R p (t,[]) ?jl (last ?jl,[]) (u,[]) (u,[]) ?jr"
using jl jr lastl unfolding last.simps ldc_trs_def unfolding p_dec ldc_trs_def local_peaks_def get_target_def
apply (simp add: seq.intros(1)) by (simp add: conv.intros(1) seq_imp_conv)
hence d2: "ld2_trs R p ?jl ?jr" using jl jr unfolding ld2_trs_def get_target_def apply auto
unfolding get_target_def apply auto by (simp add: ldc_trs_def p_dec)
have "weld_seq (rule_labeling i) r p ?jl ?jr" unfolding weld_seq_def p_dec labels_def using r
unfolding ds_def apply auto using assms(1) by (metis UNIV_I refl_onD)
thus ?thesis using d2 unfolding weld_def by fast
next
case False
then obtain q where sl: "(t, ?v) ∈ rstep_r_p_s R (l2, r2) (p1 <#> q <#> q2) σ2" using sl by auto
hence jl: "(t,[(t,(l2,r2),p1<#>q<#>q2,σ2,True,?v)]) ∈ seq R" (is "?jl ∈ _") using rstep_is_seq[OF sl] by auto
hence diamond_trs: "diamond_trs R p ?jl ?jr"
using p jl jr by (auto intro: conv.intros simp: get_target_def diamond_trs_def ldc_trs_def p_dec)
hence d2: "ld2_trs R p ?jl ?jr" using p jl jr unfolding p_dec get_target_def diamond_trs_def ldc_trs_def ld2_trs_def by auto
have "weld_seq (rule_labeling i) r p ?jl ?jr" unfolding weld_seq_def p_dec labels_def using r
unfolding ds_def apply auto using assms(1) by (metis UNIV_I refl_on_def)+
thus ?thesis using d2 unfolding weld_def by fast
qed
qed
qed
lemma rule_labeling_parallel2:
assumes "refl (snd r)"
and "parallel_peak R p"
shows "weld R (rule_labeling i) r p"
proof -
from assms parallel_peak_close obtain s t u v rl1 p1 σ1 rl2 p2 σ2
where p_dec: "p = ((s, rl1, p1, σ1,True, t), s, rl2, p2, σ2,True, u)" and x: "(s, t) ∈ rstep_r_p_s R rl1 p1 σ1 ∧
(s, u) ∈ rstep_r_p_s R rl2 p2 σ2 ∧ (t, v) ∈ rstep_r_p_s R rl2 p2 σ2 ∧ (u, v) ∈ rstep_r_p_s R rl1 p1 σ1"
by fast
from x have 1:"(s,[(s,rl1,p1,σ1,True,t)]) ∈ seq R" by (metis rstep_is_seq)
from x have 2:"(s,[(s,rl2,p2,σ2,True,u)]) ∈ seq R" by (metis rstep_is_seq)
from x have 3:"(t,[(t,rl2,p2,σ2,True,v)]) ∈ seq R" (is "?jl ∈ _") by (metis rstep_is_seq)
from x have 4:"(u,[(u,rl1,p1,σ1,True,v)]) ∈ seq R" (is "?jr ∈ _") by (metis rstep_is_seq)
from p_dec x have "p ∈ local_peaks R" (is "?p ∈ _") unfolding local_peaks_def by fast
hence "ldc_trs R p (first ?jl,[]) ?jl (last ?jl,[]) (first ?jr,[]) ?jr (last ?jr,[])" using 3 4 conv.simps unfolding last.simps get_target_def snd_conv first.simps p_dec unfolding ldc_trs_def get_target_def apply auto
unfolding get_target_def by auto
hence x1: "ld2_trs R p ?jl ?jr" unfolding ld2_trs_def by (simp add: ldc_trs_def)
have x2: "weld_seq (rule_labeling i) r p ?jl ?jr"
unfolding weld_seq_def p_dec labels_def ds_def apply auto using assms
apply (metis UNIV_I refl_on_def) by (metis UNIV_I assms(1) refl_on_def)
thus ?thesis using x1 unfolding weld_def by auto
qed
lemma rule_labeling_is_weakly_compatible:
assumes "refl (snd r)"
and "left_linear_trs R"
shows "weakly_compatible R (rule_labeling i) r"
proof -
have c: "is_labeling R (rule_labeling i) r" using rl_is_labeling by fast
{
fix p
assume "variable_peak R p ∨ parallel_peak R p" and "left_linear_trs R"
hence "weld R (rule_labeling i) r p" using rl_variable2[OF assms(1) _ assms(2)] rule_labeling_parallel2[OF assms(1)] by metis
}
thus ?thesis unfolding weakly_compatible_def using c by fast
qed
definition R_d :: "('f,'v) trs ⇒ ('f,'v) trs"
where "R_d R = {rl ∈ R. ¬ linear_term (snd rl)}"
definition R_nd :: "('f,'v) trs ⇒ ('f,'v) trs"
where "R_nd R = {rl ∈ R. linear_term (snd rl)}"
definition lex_r :: "'a relp ⇒ 'b relp ⇒ ('a × 'b) relp"
where "lex_r r1 r2 = (lex_two (fst r1) (snd r1) (fst r2),
lex_two (fst r1) (snd r1) (snd r2))"
lemma map_dec:
assumes "map f xs = ys1@ys2"
shows "∃ xs1 xs2. xs = xs1@xs2 ∧ map f xs1 = ys1 ∧ map f xs2 = ys2"
using assms
proof (induct ys1 arbitrary: ys2 xs)
case (Cons y ys)
then obtain x' xs' where xs_dec: "xs = x'#xs'" by (metis append_Cons list.distinct(1) list.exhaust list.simps(8))
hence map1: "map f xs' = ys@ys2" using Cons by auto
then obtain xs1 xs2 where xs'_dec: "xs' = xs1 @ xs2" and map:" map f xs1 = ys ∧ map f xs2 = ys2" using Cons(1)[of xs' ys2] by fast
hence "xs = (x'#xs1)@xs2" and "map f (x'#xs1) = (f x')#ys" and "map f xs2 = ys2" unfolding xs_dec by auto
thus ?case by (metis Cons.prems append_Cons list.sel(1) list.simps(9))
qed auto
lemma R_d_union_R_nd: "R_d R ∪ R_nd R = R" unfolding R_d_def R_nd_def by auto
lemma l_sl:
fixes l r R
assumes "(s,t) ∈ (rstep R)^*"
shows "(t,s) ∈ (snd (sl_rel (R_d R) (R_nd R)))"
using assms unfolding sl_rel.simps apply auto using R_d_union_R_nd by (metis inf_sup_aci(5) rstep_union)
lemma l_imp_ll:
fixes l r R
defines "ll ≡ (λ step. (source_labeling step,l step))"
and "rr ≡ (lex_r (sl_rel (R_d R) (R_nd R)) r)"
assumes "l step ∈ ds (fst r) {l step', l step''}"
and "(get_source step',get_source step) ∈ (rstep R)^*"
and "(get_source step'',get_source step) ∈ (rstep R)^*"
shows "ll step ∈ ds (fst rr) {ll step', ll step''}"
proof -
from assms obtain s rl p σ t where step_dec: "step = (s,rl,p,σ,t)" by (metis (erased, hide_lams) source_labeling.cases)
show ?thesis
proof (cases "l step ∈ ds (fst r) {l step'}")
case True
from assms obtain s' rl' p' σ' t' where step'_dec: "step' = (s',rl',p',σ',t')"
by (metis (erased, hide_lams) source_labeling.cases)
have "(source_labeling step',source_labeling step) ∈ (rstep R)^*" using assms unfolding step_dec step'_dec
unfolding get_source_def by auto
hence l2: "(source_labeling step,source_labeling step') ∈ (snd (sl_rel (R_d R) (R_nd R)))" using l_sl by auto
hence l1: "(l step,l step') ∈ (fst r)" using True unfolding ds_def by auto
hence "(ll step,ll step') ∈ fst rr" using l2 unfolding lex_r_def ll_def rr_def by auto
thus ?thesis unfolding ds_def by auto
next
case False
from assms obtain s' rl' p' σ' t' where step''_dec: "step'' = (s',rl',p',σ',t')"
by (metis (erased, hide_lams) source_labeling.cases)
have "(source_labeling step'',source_labeling step) ∈ (rstep R)^*"
using assms unfolding step_dec step''_dec unfolding get_source_def by auto
hence l2: "(source_labeling step,source_labeling step'') ∈ (snd (sl_rel (R_d R) (R_nd R)))" using l_sl by auto
hence l1: "(l step,l step'') ∈ (fst r)" using False assms unfolding ds_def by auto
hence "(ll step,ll step'') ∈ fst rr" using l2 unfolding lex_r_def ll_def rr_def by auto
thus ?thesis unfolding ds_def by auto
qed
qed
lemma l_imp_ll_seq:
fixes l r R
defines "ll ≡ (λ step. (source_labeling step,l step))"
and "rr ≡ (lex_r (sl_rel (R_d R) (R_nd R)) r)"
assumes "set (map l ss) ⊆ ds (fst r) {l step',l step''}"
and "∀i < length ss. (get_source step' ,get_source (ss !i)) ∈ (rstep R)^*"
and "∀i < length ss. (get_source step'',get_source (ss !i)) ∈ (rstep R)^*"
shows "set (map ll ss) ⊆ ds (fst rr) {ll step',ll step''}"
using assms(3-5)
proof (induct ss)
case (Cons t ts)
hence step:"l t ∈ ds (fst r) {l step',l step''}" and steps:"set (map l ts) ⊆ ds (fst r) {l step', l step''}" by auto
from Cons have c1: "∀i<length ts. (get_source step', get_source (ts ! i)) ∈ (rstep R)⇧*" by auto
from Cons have c2: "∀i<length ts. (get_source step'', get_source (ts ! i)) ∈ (rstep R)⇧*" by auto
hence 2: "set (map ll ts) ⊆ ds (fst rr) {ll step', ll step''}" using Cons(1)[OF steps c1 c2] by auto
have r1: "(get_source step', get_source t) ∈ (rstep R)⇧*" using Cons assms by auto
have r2: "(get_source step'', get_source t) ∈ (rstep R)⇧*" using Cons assms by auto
have 1: "ll t ∈ ds (fst rr) {ll step', ll step''}" using l_imp_ll[OF step r1 r2] unfolding ll_def rr_def by auto
show ?case using 1 2 by auto
qed auto
lemma l_imp_ll_eq:
fixes l r R
defines "ll ≡ (λ step. (source_labeling step,l step))"
and "rr ≡ (lex_r (sl_rel (R_d R) (R_nd R)) r)"
assumes "l step ∈ ds (snd r) {l step'}"
and "(get_source step',get_source step) ∈ (rstep R)^*"
shows "ll step ∈ ds (snd rr) {ll step'}"
proof -
from assms obtain s rl p σ t where step_dec: "step = (s,rl,p,σ,t)" by (metis (erased, hide_lams) source_labeling.cases)
from assms obtain s' rl' p' σ' t' where step'_dec: "step' = (s',rl',p',σ',t')" by (metis (erased, hide_lams) source_labeling.cases)
have "(source_labeling step',source_labeling step) ∈ (rstep R)^*" using assms unfolding step_dec step'_dec unfolding get_source_def by auto
hence l2: "(source_labeling step,source_labeling step') ∈ (snd (sl_rel (R_d R) (R_nd R)))" using l_sl by auto
hence l1: "(l step,l step') ∈ (snd r)" using assms unfolding ds_def by auto
hence "(ll step,ll step') ∈ snd rr" using l2 unfolding lex_r_def ll_def rr_def by auto
thus ?thesis unfolding ds_def by auto
qed
lemma l_imp_ll_seq_eq:
fixes l r R
defines "ll ≡ (λ step. (source_labeling step,l step))"
and "rr ≡ (lex_r (sl_rel (R_d R) (R_nd R)) r)"
assumes "set (map l ss) ⊆ ds (snd r) {l step'}"
and "∀i < length ss. (get_source step' ,get_source (ss !i)) ∈ (rstep R)^*"
shows "set (map ll ss) ⊆ ds (snd rr) {ll step'}"
using assms(3-4)
proof (induct ss)
case (Cons t ts)
hence step:"l t ∈ ds (snd r) {l step'}" and steps:"set (map l ts) ⊆ ds (snd r) {l step'}" by auto
from Cons have c1: "∀i<length ts. (get_source step', get_source (ts ! i)) ∈ (rstep R)⇧*" by auto
hence 2: "set (map ll ts) ⊆ ds (snd rr) {ll step'}" using Cons(1)[OF steps c1] by auto
have r1: "(get_source step', get_source t) ∈ (rstep R)⇧*" using Cons assms by auto
have 1: "ll t ∈ ds (snd rr) {ll step'}" using l_imp_ll_eq[OF step r1] unfolding ll_def rr_def by auto
show ?case using 1 2 by auto
qed auto
lemma r_ast_seq_imp_r_ast:
assumes "(s,t) ∈ (rstep R)^*" and "t = first ss" and "ss ∈ seq R"
shows "∀i < length (snd ss). (s,get_source ((snd ss)!i)) ∈ (rstep R)^*"
proof -
from assms obtain ts where ss_dec: "ss = (t,ts)" by (metis first.elims)
from assms have ?thesis unfolding ss_dec apply auto
proof (induct ts arbitrary: t )
case (Cons step steps)
from Cons(3) obtain rl p σ u where step_dec: "step = (t,rl,p,σ,True,u)"
using seq.cases by blast
hence "(t,u) ∈ rstep_r_p_s R rl p σ" using Cons by (metis (poly_guards_query) seq_chop_first(2))
hence ast:"(s,u) ∈ (rstep R)^*" by (metis (poly_guards_query) Cons.prems(1) rstep_r_p_s_imp_rstep rtrancl.rtrancl_into_rtrancl)
hence rst:"(u,steps) ∈ seq R" by (metis Cons.prems(2) seq_chop_first(1) step_dec)
from Cons(1)[OF ast rst] have 2: "∀i < length steps.(s, get_source (steps ! i)) ∈ (rstep R)⇧*" by auto
have 1: "(s,get_source (step)) ∈ (rstep R)^*" unfolding step_dec get_source_def using Cons by auto
show ?case using 1 2 by (metis (erased, hide_lams) Cons.prems(3) One_nat_def add.commute add_Suc_right diff_Suc_Suc diff_zero gr0_conv_Suc list.size(4) monoid_add_class.add.right_neutral nat_add_left_cancel_less nth_Cons_pos nth_non_equal_first_eq)
qed auto
thus ?thesis unfolding ss_dec by auto
qed
lemma len_append: "∀ i < length xs. (xs ! i = (xs @ ys) ! i)" by (metis nth_append)
lemma source_labeling_eld_seq_imp_eld_seq:
assumes ldc_trs: "ldc_trs R p jl1 jl2 jl3 jr1 jr2 jr3"
and "eld_conv l r p jl1 jl2 jl3 jr1 jr2 jr3"
and fan: "fan R p jl1 jl2 jl3 jr1 jr2 jr3"
defines "ll ≡ (λ step. (source_labeling step,l step))"
and "rr ≡ (lex_r (sl_rel (R_d R) (R_nd R)) r)"
shows "eld_conv ll rr p jl1 jl2 jl3 jr1 jr2 jr3"
proof -
{
fix lp rp ss1 ss2 ss3
assume A2:"ELD_1 r (l lp) (l rp) (map l (snd ss1)) (map l (snd ss2)) (map l (snd ss3))"
and A3a: "ss1 ∈ conv R" and A3b: "ss2 ∈ seq R" and A3c: "ss3 ∈ conv R" and
A4: "(get_source lp, first ss1) ∈ (rstep R)^*" and A5: "get_source lp = get_source rp"
and s1: "∀i < length (snd ss1). (get_source lp,get_source ((snd ss1)!i)) ∈ (rstep R)^*"
and s2: "∀i<length (snd ss2). (get_source rp, get_source (snd ss2 ! i)) ∈ (rstep R)⇧*"
and s3: "∀i<length (snd ss3). (get_source lp, get_source (snd ss3 ! i)) ∈ (rstep R)⇧*"
from A2 have l:"length (map l (snd ss2)) ≤ 1" unfolding ELD_1_def by auto
hence 1: "set (map l (snd ss1)) ⊆ ds (fst r) {l lp,l lp}" and
2: "set (map l (snd ss2)) ⊆ ds (snd r) {l rp}" and
3: "set (map l (snd ss3)) ⊆ ds (fst r) {l rp,l lp}"
using A2 unfolding ELD_1_def by auto
have s3': "∀i<length (snd ss3). (get_source rp, get_source (snd ss3 ! i)) ∈ (rstep R)⇧*" using s3 A5 by auto
have "set (map ll (snd ss1)) ⊆ ds (fst rr) {ll lp}"
and "set (map ll (snd ss2)) ⊆ ds (snd rr) {ll rp}"
and "set (map ll (snd ss3)) ⊆ ds (fst rr) {ll rp,ll lp}"
using l_imp_ll_seq[OF 1 s1 s1] using l_imp_ll_seq_eq[OF 2 s2] using l_imp_ll_seq[OF 3 s3' s3] unfolding ll_def rr_def by auto
hence "ELD_1 rr (ll lp) (ll rp) (map ll (snd ss1)) (map ll (snd ss2)) (map ll (snd ss3))"
unfolding ELD_1_def using l by auto
} note F = this
from assms obtain s rl q σ t rl2 q2 σ2 t2 where p_dec: "p = ((s,rl,q,σ,True,t),(s,rl2,q2,σ2,True,t2))"
and step1: "(s,t) ∈ rstep_r_p_s R rl q σ" and step2: "(s,t2) ∈ rstep_r_p_s R rl2 q2 σ2"
using assms unfolding ldc_trs_def local_peaks_def get_source_def get_target_def by auto
from assms have ELDl: "ELD_1 r (l (fst p)) (l (snd p)) (map l (snd jl1)) (map l (snd jl2)) (map l (snd jl3))"
unfolding ldc_trs_def eld_conv_def by auto
have "(get_source (fst p),get_target (fst p)) ∈ rstep R" using step1
unfolding p_dec get_source_def get_target_def apply auto by (metis rstep_r_p_s_imp_rstep)
obtain jl where jl: "jl = seq_concat jl1 (seq_concat jl2 jl3)" by auto
have stepl: "(get_source (fst p), first jl1) ∈ (rstep R)⇧*" using assms unfolding ldc_trs_def
by (metis (no_types, lifting) ‹(get_source (fst p), get_target (fst p)) ∈ rstep R› first.simps r_into_rtrancl seq_concat_def)
have "(get_source (snd p),get_target (snd p)) ∈ rstep R" using step2
unfolding p_dec get_source_def get_target_def apply auto by (metis rstep_r_p_s_imp_rstep)
obtain jr where jr:"jr = seq_concat jr1 (seq_concat jr2 jr3)" by auto
have stepr: "(get_source (snd p), first jr1) ∈ (rstep R)⇧*" using assms unfolding ldc_trs_def
by (metis (no_types, lifting) ‹(get_source (snd p), get_target (snd p)) ∈ rstep R› first.simps r_into_rtrancl seq_concat_def)
from assms have ELDr: "ELD_1 r (l (snd p)) (l (fst p)) (map l (snd jr1)) (map l (snd jr2)) (map l (snd jr3))"
unfolding ldc_trs_def eld_conv_def by fast
have A5: "get_source (fst p) = get_source (snd p)" using ldc_trs unfolding ldc_trs_def local_peaks_def get_source_def by auto
show ?thesis using ldc_trs unfolding ldc_trs_def local_peaks_def eld_def
using F[OF ELDl _ _ _ stepl A5] using F[OF ELDr _ _ _ stepr A5[symmetric]] using assms unfolding ldc_trs_def fan_def
by (simp add: A5 eld_conv_def)
qed
lemma source_labeling_eld_imp_eld:
assumes "eld_fan R l r p"
defines "ll ≡ (λ step. (source_labeling step,l step))"
and "rr ≡ (lex_r (sl_rel (R_d R) (R_nd R)) r)"
shows "eldc R ll rr p"
proof -
from assms obtain jl1 jl2 jl3 jr1 jr2 jr3 where d:"ldc_trs R p jl1 jl2 jl3 jr1 jr2 jr3"
and ELD:"eld_conv l r p jl1 jl2 jl3 jr1 jr2 jr3"
and fan:"fan R p jl1 jl2 jl3 jr1 jr2 jr3" unfolding eld_fan_def by auto
show ?thesis using d source_labeling_eld_seq_imp_eld_seq[OF d ELD fan] unfolding ll_def rr_def eldc_def by fast
qed
lemma rel_props_lex:
assumes "rel_props (fst r1) (snd r1)"
and "rel_props (fst r2) (snd r2)"
defines "r ≡ lex_r r1 r2"
shows "rel_props (fst r) (snd r)"
proof -
have t1: "trans (fst r1)"
and t1': "trans (snd r1)"
and t2: "trans (fst r2)"
and t2': "trans (snd r2)"
using assms unfolding rel_props_def by auto
{
fix x1 x2 y1 y2 z1 z2
assume A: "((x1,x2),(y1,y2)) ∈ fst r" and B: "((y1,y2),(z1,z2)) ∈ fst r"
have "((x1,x2),(z1,z2)) ∈ fst r"
proof (cases "(x1,y1) ∈ fst r1")
case True note T1 = this
hence "(x1,z1) ∈ fst r1"
proof (cases "(y1,z1) ∈ fst r1")
case True
thus ?thesis using T1 t1 trans_def by metis
next
case False
hence T2: "(y1,z1) ∈ snd r1" using B unfolding r_def lex_r_def by auto
have "(x1,x1) ∈ snd r1" using assms(1) unfolding rel_props_def by (metis UNIV_I refl_on_def)
thus ?thesis using T1 assms(1) T2 unfolding rel_props_def r_def lex_r_def t1 by auto
qed
thus ?thesis unfolding r_def lex_r_def by auto
next
case False
hence T1: "(x1,y1) ∈ snd r1" and T2: "(x2,y2) ∈ fst r2" using A unfolding r_def lex_r_def by auto
thus ?thesis
proof (cases "(y1,z1) ∈ fst r1")
next
case True
have T3: "(z1,z1) ∈ snd r1" using assms(1) unfolding rel_props_def by (metis UNIV_I refl_on_def)
thus ?thesis using T1 True T3 assms(1-2) unfolding rel_props_def r_def lex_r_def by auto
next
case False
hence T3: "(y1,z1) ∈ snd r1" and T4: "(y2,z2) ∈ fst r2" using B unfolding r_def lex_r_def by auto
have "(x1,z1) ∈ snd r1" using T1 T3 t1' unfolding trans_def by metis
moreover have "(x2,z2) ∈ fst r2" using T2 T4 t2 unfolding trans_def by metis
ultimately show ?thesis unfolding r_def lex_r_def by auto
qed
qed
}
hence tA: "trans (fst r)" unfolding trans_def by (metis prod.collapse)
{
fix x1 x2 y1 y2 z1 z2
assume A: "((x1,x2),(y1,y2)) ∈ snd r" and B: "((y1,y2),(z1,z2)) ∈ snd r"
have "((x1,x2),(z1,z2)) ∈ snd r"
proof (cases "(x1,y1) ∈ fst r1")
case True note T1 = this
hence "(x1,z1) ∈ fst r1"
proof (cases "(y1,z1) ∈ fst r1")
case True
thus ?thesis using T1 t1 unfolding trans_def by metis
next
case False
hence T2: "(y1,z1) ∈ snd r1" using B unfolding r_def lex_r_def by auto
have "(x1,x1) ∈ snd r1" using assms(1) unfolding rel_props_def by (metis UNIV_I refl_on_def)
thus ?thesis using T1 assms(1) T2 unfolding rel_props_def r_def lex_r_def t1 by auto
qed
thus ?thesis unfolding r_def lex_r_def by auto
next
case False
hence T1: "(x1,y1) ∈ snd r1" and T2: "(x2,y2) ∈ snd r2" using A unfolding r_def lex_r_def by auto
thus ?thesis
proof (cases "(y1,z1) ∈ fst r1")
case True
have T3: "(z1,z1) ∈ snd r1" using assms(1) unfolding rel_props_def by (metis UNIV_I refl_on_def)
thus ?thesis using T1 True T3 assms(1-2) unfolding rel_props_def r_def lex_r_def by auto
next
case False
hence T3: "(y1,z1) ∈ snd r1" and T4: "(y2,z2) ∈ snd r2" using B unfolding r_def lex_r_def by auto
have "(x1,z1) ∈ snd r1" using T1 T3 t1' unfolding trans_def by metis
moreover have "(x2,z2) ∈ snd r2" using T2 T4 t2' unfolding trans_def by metis
ultimately show ?thesis unfolding r_def lex_r_def by auto
qed
qed
}
hence tB: "trans (snd r)" unfolding trans_def by (metis prod.collapse)
let ?s1 = "(fst r1)¯"
let ?ns1 = "(snd r1)¯"
let ?s2 = "(fst r2)¯"
have SN1: "SN ?s1" using assms unfolding rel_props_def by (metis SN_iff_wf converse_converse)
have SN2: "SN ?s2" using assms unfolding rel_props_def by (metis SN_iff_wf converse_converse)
have compat: "?ns1 O ?s1 ⊆ ?s1" using assms unfolding rel_props_def refl_on_def by auto
have SN: "SN (lex_two ?s1 ?ns1 ?s2)" (is "SN ?R") using lex_two[OF compat SN1 SN2] by auto
hence "?R = ((fst r)¯)" unfolding r_def lex_r_def by auto
hence "SN ((fst r)¯)" using SN unfolding r_def lex_r_def by auto
hence wf: "wf ((fst r))" by (metis SN_iff_wf converse_converse)
{
fix x1 x2
assume "(x1,x1) ∈ snd r1" and "(x2,x2) ∈ snd r2"
hence "((x1,x2),(x1,x2)) ∈ snd r" unfolding r_def lex_r_def by auto
} note r_key = this
have r1: "∀ x1 ∈ UNIV. (x1,x1) ∈ snd r1"
using assms unfolding rel_props_def by (metis UNIV_I refl_on_def)
have r2: "∀ x2 ∈ UNIV. (x2,x2) ∈ snd r2"
using assms unfolding rel_props_def by (metis UNIV_I refl_on_def)
have r: "∀ (x1,x2) ∈ UNIV. ((x1,x2),x1,x2) ∈ snd r" using r_key r1 r2 by auto
hence r: "refl (snd r)" using refl_on_def' by fast
{
fix x1 x2 y1 y2 z1 z2 v1 v2
assume A: "((x1,x2),(y1,y2)) ∈ snd r" and B: "((y1,y2),(z1,z2)) ∈ fst r" and C: "((z1,z2),(v1,v2)) ∈ snd r"
have D: "((x1,x2),(z1,z2)) ∈ fst r"
proof (cases "(x1,y1) ∈ fst r1")
case True note T1 = this
show ?thesis
proof (cases "(y1,z1) ∈ fst r1")
case True
hence "(x1,z1) ∈ fst r1" using T1 t1 unfolding trans_def by metis
thus ?thesis unfolding r_def lex_r_def by auto
next
case False
hence "(y1,z1) ∈ snd r1" using B unfolding r_def lex_r_def by auto
moreover have "(x1,x1) ∈ snd r1" using assms unfolding rel_props_def by (metis UNIV_I r1)
ultimately have "(x1,z1) ∈ fst r1" using T1 assms unfolding rel_props_def by auto
thus ?thesis unfolding r_def lex_r_def by auto
qed
next
case False
hence T2: "(x1,y1) ∈ snd r1" and W1:"(x2,y2) ∈ snd r2" using A unfolding r_def lex_r_def by auto
thus ?thesis
proof (cases "(y1,z1) ∈ fst r1")
case True
have "(z1,z1) ∈ snd r1" using assms unfolding rel_props_def by (metis UNIV_I r1)
hence "(x1,z1) ∈ fst r1" using T2 True assms unfolding rel_props_def by auto
thus ?thesis unfolding r_def lex_r_def by auto
next
case False
hence "(y1,z1) ∈ snd r1" and W2:"(y2,z2) ∈ fst r2" using B unfolding r_def lex_r_def by auto
hence k1: "(x1,z1) ∈ snd r1" using T2 t1' unfolding trans_def by metis
hence "(z2,z2) ∈ snd r2" using assms unfolding rel_props_def by (metis UNIV_I r2)
hence "(x2,z2) ∈ fst r2" using W1 W2 assms unfolding rel_props_def by auto
thus ?thesis using k1 unfolding r_def lex_r_def by auto
qed
qed
have "((x1,x2),(v1,v2)) ∈ fst r"
proof (cases "(x1,z1) ∈ fst r1")
case True note T1 = this
thus ?thesis
proof (cases "(z1,v1) ∈ fst r1")
case True
hence "(x1,v1) ∈ fst r1" using T1 t1 unfolding trans_def by metis
thus ?thesis unfolding r_def lex_r_def by auto
next
case False
hence T2: "(z1,v1) ∈ snd r1" using C unfolding r_def lex_r_def by auto
have "(x1,x1) ∈ snd r1" using assms unfolding rel_props_def by (metis UNIV_I r1)
hence "(x1,v1) ∈ fst r1" using T1 T2 assms unfolding rel_props_def by auto
thus ?thesis unfolding r_def lex_r_def by auto
qed
next
case False
hence T1: "(x1,z1) ∈ snd r1" and W0: "(x2,z2) ∈ fst r2" using D unfolding r_def lex_r_def by auto
thus ?thesis
proof (cases "(z1,v1) ∈ fst r1")
case True
have "(v1,v1) ∈ snd r1" using assms unfolding rel_props_def by (metis UNIV_I r1)
hence "(x1,v1) ∈ fst r1" using assms T1 True unfolding rel_props_def by auto
thus ?thesis unfolding r_def lex_r_def by auto
next
case False
have W2: "(x2,x2) ∈ snd r2" using assms unfolding rel_props_def using UNIV_I r2 by metis
from False have "(z1,v1) ∈ snd r1" and W1: "(z2,v2) ∈ snd r2" using C unfolding r_def lex_r_def by auto
hence "(x1,v1) ∈ snd r1" using T1 t1' unfolding trans_def by metis
moreover have "(x2,v2) ∈ fst r2" using W0 W1 W2 using assms unfolding rel_props_def by auto
ultimately show ?thesis unfolding r_def lex_r_def by auto
qed
qed
}
hence compat: "snd r O fst r O snd r ⊆ fst r" by auto
show ?thesis using tA tB wf r compat unfolding rel_props_def by simp
qed
lemma SN_rel_has_rel_props:
assumes SN: "SN_rel (rstep (R_d R)) (rstep (R_nd R))"
defines "r ≡ (sl_rel (R_d R) (R_nd R))"
shows "rel_props (fst r) (snd r)"
proof -
have t1: "trans (fst r)" unfolding r_def sl_rel.simps fst_conv by (metis trans_converse trans_trancl)
have t2: "trans (snd r)" unfolding r_def sl_rel.simps snd_conv by (metis trans_converse trans_rtrancl)
have "SN (((rstep (R_nd R))⇧* O rstep (R_d R) O (rstep (R_nd R))⇧*))" using SN unfolding r_def sl_rel.simps fst_conv by (metis SN_rel_on_def)
hence wf: "wf (fst r)" unfolding r_def sl_rel.simps fst_conv by (metis SN_iff_wf wf_converse_trancl)
have r: "refl (snd r)" unfolding r_def sl_rel.simps by (auto intro: refl_rtrancl)
have compat: "snd r O fst r O snd r ⊆ fst r" unfolding r_def apply auto by (metis rel_compat rel_rstep_def)
show ?thesis unfolding rel_props_def using t1 t2 wf r compat by auto
qed
lemma is_labeling_lex:
assumes "is_labeling R l1 r1"
and "is_labeling R l2 r2"
shows "is_labeling R (λ step. (l1 step,l2 step)) (lex_r r1 r2)"
using assms unfolding is_labeling_def Let_def lex_r_def by auto
lemma SN_rel_is_labeling:
"is_labeling R source_labeling (sl_rel (R_d R) (R_nd R))" (is "is_labeling ?R ?l ?r")
proof -
have eq: "R = (R_d R) ∪ (R_nd R)" unfolding R_d_def R_nd_def by auto
show ?thesis using sl_is_labeling eq by metis
qed
lemma l_imp_ll_eq3:
fixes l1 l2 r1 r2 R
defines "ll ≡ (λ step. (l1 step,l2 step))"
and "rr ≡ (lex_r r1 r2)"
assumes "l1 step ∈ ds (snd r1) {l1 step'}"
and "l2 step ∈ ds (snd r2) {l2 step'}"
and "(get_source step',get_source step) ∈ (rstep R)^*"
shows "ll step ∈ ds (snd rr) {ll step'}"
unfolding ll_def rr_def using assms unfolding lex_r_def ds_def by auto
lemma l_imp_ll_seq_eq3:
fixes l1 l r1 r R
defines "ll ≡ (λ step. (l step,l1 step))"
and "rr ≡ (lex_r r r1)"
assumes "set (map l ss) ⊆ ds (snd r) {l step'}"
and "set (map l1 ss) ⊆ ds (snd r1) {l1 step'}"
and "∀i < length ss. (get_source step' ,get_source (ss !i)) ∈ (rstep R)^*"
shows "set (map ll ss) ⊆ ds (snd rr) {ll step'}"
using assms(3-5)
proof (induct ss)
case Nil thus ?case by auto
next
case (Cons t ts)
hence step:"l t ∈ ds (snd r) {l step'}" and steps:"set (map l ts) ⊆ ds (snd r) {l step'}" by auto
from Cons have step':"l1 t ∈ ds (snd r1) {l1 step'}" and steps':"set (map l1 ts) ⊆ ds (snd r1) {l1 step'}" by auto
from Cons have c1: "∀i<length ts. (get_source step', get_source (ts ! i)) ∈ (rstep R)⇧*" by auto
hence 2: "set (map ll ts) ⊆ ds (snd rr) {ll step'}" using Cons(1)[OF steps steps' c1] by auto
have r1: "(get_source step', get_source t) ∈ (rstep R)⇧*" using Cons assms by auto
have 1: "ll t ∈ ds (snd rr) {ll step'}" using l_imp_ll_eq3[OF step step' r1] unfolding ll_def rr_def by blast
show ?case using 1 2 by auto
qed
lemma l_imp_ll3:
fixes l l1 r r1 R
defines "ll ≡ (λ step. (l step,l1 step))"
and "rr ≡ (lex_r r r1)"
assumes "l step ∈ ds (fst r) {l step', l step''}"
and "(get_source step',get_source step) ∈ (rstep R)^*"
and "(get_source step'',get_source step) ∈ (rstep R)^*"
shows "ll step ∈ ds (fst rr) {ll step', ll step''}"
using assms unfolding ds_def ll_def rr_def lex_r_def by auto
lemma l_imp_ll_seq3:
fixes l1 l r1 r R
defines "ll ≡ (λ step. (l step,l1 step))"
and "rr ≡ (lex_r r r1)"
assumes "set (map l ss) ⊆ ds (fst r) {l step',l step''}"
and "∀i < length ss. (get_source step' ,get_source (ss !i)) ∈ (rstep R)^*"
and "∀i < length ss. (get_source step'',get_source (ss !i)) ∈ (rstep R)^*"
shows "set (map ll ss) ⊆ ds (fst rr) {ll step',ll step''}"
using assms(3-)
proof (induct ss)
case Nil thus ?case by auto
next
case (Cons t ts)
hence step:"l t ∈ ds (fst r) {l step',l step''}" and steps:"set (map l ts) ⊆ ds (fst r) {l step', l step''}" by auto
from Cons have c1: "∀i<length ts. (get_source step', get_source (ts ! i)) ∈ (rstep R)⇧*" by auto
from Cons have c2: "∀i<length ts. (get_source step'', get_source (ts ! i)) ∈ (rstep R)⇧*" by auto
hence 2: "set (map ll ts) ⊆ ds (fst rr) {ll step', ll step''}" using Cons(1)[OF steps c1 c2] by auto
have r1: "(get_source step', get_source t) ∈ (rstep R)⇧*" using Cons assms by auto
have r2: "(get_source step'', get_source t) ∈ (rstep R)⇧*" using Cons assms by auto
have 1: "ll t ∈ ds (fst rr) {ll step', ll step''}" using l_imp_ll3[OF step r1 r2] unfolding ll_def rr_def by fast
show ?case using 1 2 by auto
qed
lemma conv_concat_map:
assumes "conv_concat ss1 ss2 = ss"
shows "map l (snd ss1)@map l (snd ss2) = map l (snd ss)" proof -
from assms obtain x xs y ys where ss1_dec: "(x,xs) = ss1" and ss2_dec: "(y,ys) = ss2" using prod.collapse by blast
show ?thesis unfolding assms[symmetric] conv_concat_def ss1_dec[symmetric] ss2_dec[symmetric] by auto
qed
lemma conv_concat_left_empty:
shows "conv_concat (first ss2,[]) ss2 = ss2" proof -
obtain y ys where ss2_dec: "(y,ys) = ss2" using prod.collapse by blast
show ?thesis unfolding conv_concat_def unfolding ss2_dec[symmetric] first.simps by auto
qed
lemma eld_seq_and_weld_seq_imp_eld_seq2:
assumes diamond_trs: "diamond_trs R p jl jr"
and eld_conv: "eld_conv l1 r1 p (first jl,[]) jl (last jl,[]) (first jr,[]) jr (last jr,[])" (is "eld_conv _ _ _ ?jl1 ?jl2 ?jl3 ?jr1 ?jr2 ?jr3")
and weld_seq: "weld_seq l2 r2 p jl jr"
shows "eld_conv (λ step. (l1 step,l2 step)) (lex_r r1 r2) p (first jl,[]) jl (last jl,[]) (first jr,[]) jr (last jr,[])"
(is "eld_conv ?l ?r p _ _ _ _ _ _") proof -
have a: "ELD_1 r1 (l1 (fst p)) (l1 (snd p)) (map l1 (snd ?jl1)) (map l1 (snd ?jl2)) (map l1 (snd ?jl3))" using eld_conv unfolding eld_conv_def by auto
have b: "ELD_1 r2 (l2 (fst p)) (l2 (snd p)) (map l2 (snd ?jl1)) (map l2 (snd ?jl2)) (map l2 (snd ?jl3))" using weld_seq unfolding weld_seq_def
by (metis (no_types, lifting) ELD_1_def Nil_is_map_conv a bot_least labels_def length_map list.set(1) snd_conv subsetI)
have 1: "ELD_1 (lex_r r1 r2) (l1 (fst p), l2 (fst p)) (l1 (snd p), l2 (snd p)) (map ?l (snd ?jl1)) (map ?l (snd ?jl2)) (map ?l (snd ?jl3))"
proof -
have x1: "length (map (λstep. (l1 step, l2 step)) (snd jl)) ≤ 1"
using eld_conv weld_seq unfolding eld_conv_def weld_seq_def by (metis (mono_tags, lifting) diamond_trs diamond_trs_def length_map)
have x2: "set (map (λstep. (l1 step, l2 step)) (snd jl)) ⊆ ds (snd (lex_r r1 r2)) {(l1 (snd p), l2 (snd p))}"
using eld_conv weld_seq unfolding eld_conv_def weld_seq_def proof (cases "length (snd jl) = 0")
case True thus ?thesis using eld_conv weld_seq eld_conv_def weld_seq_def by auto
next
case False hence length: "length (snd jl) = 1" using diamond_trs unfolding diamond_trs_def using Decreasing_Diagrams2.seq.simps One_nat_def ldc_trs_def le_antisym le_numeral_extra(4) length_0_conv list.size(4) prod.collapse trans_le_add2 by linarith
then obtain elt elts where "(snd jl) = elt#elts" by (metis (mono_tags, lifting) False last.elims length_0_conv snd_conv)
hence elt: "(snd jl) = [elt]" using length by auto
have 1: "l1 elt ∈ under (snd r1) (l1 (snd p))" using eld_conv unfolding ELD_1_def eld_conv_def elt by auto
have "(∀a∈labels l2 jl. a ∈ ds (snd r2) {l2 (snd p)})" using weld_seq unfolding weld_seq_def by auto
hence "(l2 elt) ∈ {y. ∃x∈{l2 (snd p)}. (y, x) ∈ snd r2}" unfolding under_def ds_def unfolding labels_def elt by auto
hence 2: "l2 elt ∈ under (snd r2) (l2 (snd p))" unfolding under_def ds_def unfolding labels_def elt by auto
thus ?thesis using 1 unfolding elt ds_def under_def apply auto unfolding lex_r_def by auto
qed
show ?thesis using x1 x2 unfolding ELD_1_def by auto
qed
have a: "ELD_1 r1 (l1 (snd p)) (l1 (fst p)) (map l1 (snd ?jr1)) (map l1 (snd ?jr2)) (map l1 (snd ?jr3))" using eld_conv unfolding eld_conv_def by blast
have b: "ELD_1 r2 (l2 (snd p)) (l2 (fst p)) (map l2 (snd ?jr1)) (map l2 (snd ?jr2)) (map l2 (snd ?jr3))" using weld_seq unfolding weld_seq_def
by (metis ELD_1_def a bot_least labels_def length_map list.map_disc_iff list.set(1) snd_conv subsetI)
have 2: "ELD_1 (lex_r r1 r2) (l1 (snd p), l2 (snd p)) (l1 (fst p), l2 (fst p)) (map ?l (snd ?jr1)) (map ?l (snd ?jr2)) (map ?l (snd ?jr3))"
proof -
have x1: "length (map (λstep. (l1 step, l2 step)) (snd jr)) ≤ 1"
using eld_conv weld_seq unfolding eld_conv_def weld_seq_def by (metis (mono_tags, lifting) diamond_trs diamond_trs_def length_map)
have x2: "set (map (λstep. (l1 step, l2 step)) (snd jr)) ⊆ ds (snd (lex_r r1 r2)) {(l1 (fst p), l2 (fst p))}"
using eld_conv weld_seq unfolding eld_conv_def weld_seq_def proof (cases "length (snd jr) = 0")
case True thus ?thesis using eld_conv weld_seq eld_conv_def weld_seq_def by auto
next
case False hence length: "length (snd jr) = 1" using diamond_trs unfolding diamond_trs_def using Decreasing_Diagrams2.seq.simps One_nat_def ldc_trs_def le_antisym le_numeral_extra(4) length_0_conv list.size(4) prod.collapse trans_le_add2 by linarith
then obtain elt elts where "(snd jr) = elt#elts" by (metis (mono_tags, lifting) False last.elims length_0_conv snd_conv)
hence elt: "(snd jr) = [elt]" using length by auto
have 1: "l1 elt ∈ under (snd r1) (l1 (fst p))" using eld_conv unfolding ELD_1_def eld_conv_def elt by auto
have "(∀a∈labels l2 jr. a ∈ ds (snd r2) {l2 (fst p)})" using weld_seq unfolding weld_seq_def by auto
hence "(l2 elt) ∈ {y. ∃x∈{l2 (fst p)}. (y, x) ∈ snd r2}" unfolding under_def ds_def unfolding labels_def elt by auto
hence 2: "l2 elt ∈ under (snd r2) (l2 (fst p))" unfolding under_def ds_def unfolding labels_def elt by auto
thus ?thesis using 1 unfolding elt ds_def under_def apply auto unfolding lex_r_def by auto
qed
show ?thesis using x1 x2 unfolding ELD_1_def by auto
qed
thus ?thesis using 1 2 unfolding eld_conv_def by auto
qed
lemma eld_seq_and_weld_seq_imp_eld_seq:
assumes "ld2_trs R p jl jr"
and eld_conv: "eld_conv l1 r1 p jl (last jl,[]) (last jl,[]) (first jr,[]) jr (last jr,[])" (is "eld_conv _ _ _ ?jl1 ?jl2 ?jl3 ?jr1 ?jr2 ?jr3")
and weld_seq: "weld_seq l2 r2 p jl jr"
shows "eld_conv (λ step. (l1 step,l2 step)) (lex_r r1 r2) p jl (last jl,[]) (last jl,[]) (first jr,[]) jr (last jr,[])" (is "eld_conv ?l ?r _ _ _ _ _ _ _")
proof -
from assms have l1: "ELD_1 r1 (l1 (fst p)) (l1 (snd p)) (map l1 (snd ?jl1)) (map l1 (snd ?jl2)) (map l1 (snd ?jl3))"unfolding eld_conv_def by auto
hence f1:"ELD_1 ?r (?l (fst p)) (?l (snd p)) (map ?l (snd ?jl1)) (map ?l (snd ?jl2)) (map ?l (snd ?jl3))" using assms(3) unfolding
weld_seq_def ELD_1_def apply auto unfolding lex_r_def under_def ds_def by auto
from assms have x: "ELD_1 r1 (l1 (snd p)) (l1 (fst p)) (map l1 (snd ?jr1)) (map l1 (snd ?jr2)) (map l1 (snd ?jr3))" unfolding eld_conv_def by auto
from assms have "length (snd jr) ≤ 1" unfolding ld2_trs_def by auto
have a: "ELD_1 r1 (l1 (snd p)) (l1 (fst p)) (map l1 (snd ?jr1)) (map l1 (snd ?jr2)) (map l1 (snd ?jr3))" using eld_conv unfolding eld_conv_def by blast
have b: "ELD_1 r2 (l2 (snd p)) (l2 (fst p)) (map l2 (snd ?jr1)) (map l2 (snd ?jr2)) (map l2 (snd ?jr3))" using weld_seq unfolding weld_seq_def
by (metis ELD_1_def a bot_least labels_def length_map list.map_disc_iff list.set(1) snd_conv subsetI)
have 2: "ELD_1 (lex_r r1 r2) (l1 (snd p), l2 (snd p)) (l1 (fst p), l2 (fst p)) (map ?l (snd ?jr1)) (map ?l (snd ?jr2)) (map ?l (snd ?jr3))"
proof -
have x1: "length (map (λstep. (l1 step, l2 step)) (snd jr)) ≤ 1" using assms unfolding ld2_trs_def by auto
have x2: "set (map (λstep. (l1 step, l2 step)) (snd jr)) ⊆ ds (snd (lex_r r1 r2)) {(l1 (fst p), l2 (fst p))}"
using eld_conv weld_seq unfolding eld_conv_def weld_seq_def proof (cases "length (snd jr) = 0")
case True thus ?thesis using eld_conv weld_seq eld_conv_def weld_seq_def by auto
next
case False hence length: "length (snd jr) = 1" using x1 using One_nat_def ‹length (snd jr) ≤ 1› dual_order.antisym last.elims le_numeral_extra(4) length_0_conv list.size(4) snd_conv trans_le_add2 by linarith
then obtain elt elts where "(snd jr) = elt#elts" by (metis (mono_tags, lifting) False last.elims length_0_conv snd_conv)
hence elt: "(snd jr) = [elt]" using length by auto
have 1: "l1 elt ∈ under (snd r1) (l1 (fst p))" using eld_conv unfolding ELD_1_def eld_conv_def elt by auto
have "(∀a∈labels l2 jr. a ∈ ds (snd r2) {l2 (fst p)})" using weld_seq unfolding weld_seq_def by auto
hence "(l2 elt) ∈ {y. ∃x∈{l2 (fst p)}. (y, x) ∈ snd r2}" unfolding under_def ds_def unfolding labels_def elt by auto
hence 2: "l2 elt ∈ under (snd r2) (l2 (fst p))" unfolding under_def ds_def unfolding labels_def elt by auto
thus ?thesis using 1 unfolding elt ds_def under_def apply auto unfolding lex_r_def by auto
qed
show ?thesis using x1 x2 unfolding ELD_1_def by auto
qed
hence f2:"ELD_1 ?r (?l (snd p)) (?l (fst p)) (map ?l (snd ?jr1)) (map ?l (snd ?jr2)) (map ?l (snd ?jr3))" using assms(3) unfolding
weld_seq_def ELD_1_def by auto
from f1 f2 show ?thesis unfolding eld_conv_def by auto
qed
lemma SN_rel_diamond_trs_imp_eld_seq:
assumes "diamond_trs R p jl jr"
shows "eld_conv source_labeling (sl_rel (R_d R) (R_nd R)) p (get_target (fst p),[]) jl (last jl,[]) (get_target (snd p),[]) jr (last jr,[])" (is "eld_conv ?l ?r _ ?jl1 ?jl2 ?jl3 ?jr1 ?jr2 ?jr3")
proof -
have "ldc_trs R p ?jl1 ?jl2 ?jl3 ?jr1 ?jr2 ?jr3" and l1: "length (snd jl) ≤ 1" and l2: "length (snd jr) ≤ 1"
using assms unfolding diamond_trs_def by auto
obtain s rl1 p1 σ1 t rl2 p2 σ2 u where p_dec: "p = ((s,rl1,p1,σ1,True,t),(s,rl2,p2,σ2,True,u))"
using assms unfolding local_peaks_def diamond_trs_def ldc_trs_def by blast
have st: "(s,t) ∈ rstep_r_p_s R rl1 p1 σ1" and su: "(s,u) ∈ rstep_r_p_s R rl2 p2 σ2"
using assms unfolding local_peaks_def diamond_trs_def ldc_trs_def p_dec by auto
have jl: "jl ∈ seq R" and jr: "jr ∈ seq R" using assms unfolding ldc_trs_def diamond_trs_def by auto
have eq: "fst jl = first jl" by (metis first.simps prod.collapse)
have step: "(s,t) ∈ (rstep R)^*" using st by (metis r_into_rtrancl rstep_r_p_s_imp_rstep)
hence ast:"(s,fst jl) ∈ (rstep R)^*" using assms
unfolding diamond_trs_def ldc_trs_def p_dec get_target_def eq[symmetric] by auto
have "∀i < length (snd jl). (s,get_source ((snd jl)!i)) ∈ (rstep R)^*"
using r_ast_seq_imp_r_ast[OF ast eq jl] by auto
hence la: "set (map ?l (snd jl)) ⊆ ds (snd ?r) {?l (snd p)}"
unfolding p_dec ds_def get_source_def apply auto
by (metis (no_types, hide_lams) R_d_union_R_nd fst_conv in_set_conv_nth inf_sup_aci(5) rstep_union)
have 1: "ELD_1 ?r (?l (fst p)) (?l (snd p)) [] (map ?l (snd jl)) []"
using la l1 unfolding ELD_1_def by auto
have eq: "fst jr = first jr" by (metis first.simps prod.collapse)
have step: "(s,u) ∈ (rstep R)^*" using su by (metis r_into_rtrancl rstep_r_p_s_imp_rstep)
hence ast:"(s,fst jr) ∈ (rstep R)^*"
using assms unfolding diamond_trs_def ldc_trs_def p_dec get_target_def eq[symmetric] by auto
have "∀i < length (snd jr). (s,get_source ((snd jr)!i)) ∈ (rstep R)^*"
using r_ast_seq_imp_r_ast[OF ast eq jr] by auto
hence lb: "set (map ?l (snd jr)) ⊆ ds (snd ?r) {?l (fst p)}"
unfolding p_dec ds_def get_source_def apply auto
by (metis (no_types, hide_lams) R_d_union_R_nd fst_conv in_set_conv_nth inf_sup_aci(5) rstep_union)
have 2: "ELD_1 ?r (?l (snd p)) (?l (fst p)) [] (map ?l (snd jr)) []"
using lb l2 unfolding ELD_1_def by auto
show ?thesis using 1 2 assms unfolding eld_conv_def diamond_def using list.simps(8) snd_conv by auto
qed
lemma SN_rel_ld2_trs_imp_eld_seq:
assumes "ld2_trs R p jl jr" "length (snd jl) > 1"
and "SN_rel (rstep (R_d R)) (rstep (R_nd R))"
shows "eld_conv source_labeling (sl_rel (R_d R) (R_nd R)) p jl (last jl,[]) (last jl,[]) (first jr,[]) jr (last jr,[])"
(is "eld_conv ?l ?r _ _ _ _ _ _ _")
proof -
show ?thesis proof (cases "diamond_trs R p jl jr")
case True thus ?thesis using assms(2) unfolding diamond_trs_def by auto
next
case False
{
fix p
assume d2: "ld2_trs R p jl jr"
obtain s rl1 p1 σ1 t rl2 p2 σ2 u where p_dec: "p = ((s,rl1,p1,σ1,True,t),(s,rl2,p2,σ2,True,u))"
using d2 unfolding ld2_trs_def local_peaks_def diamond_trs_def ldc_trs_def by blast
have st: "(s,t) ∈ rstep_r_p_s R rl1 p1 σ1" and su: "(s,u) ∈ rstep_r_p_s R rl2 p2 σ2"
using d2 unfolding ld2_trs_def local_peaks_def diamond_trs_def ldc_trs_def p_dec by auto
have jl: "jl ∈ seq R" and jr: "jr ∈ seq R" using d2 unfolding ld2_trs_def ldc_trs_def diamond_trs_def
by auto
have l1: "length (snd jr) ≤ 1" using d2 unfolding ld2_trs_def by auto
have eq: "fst jr = first jr" by (metis first.simps prod.collapse)
have step: "(s,u) ∈ (rstep R)^*" using su by (metis r_into_rtrancl rstep_r_p_s_imp_rstep)
hence ast:"(s,fst jr) ∈ (rstep R)^*" using d2
unfolding ld2_trs_def diamond_trs_def ldc_trs_def p_dec get_target_def eq[symmetric] by auto
have "∀i < length (snd jr). (s,get_source ((snd jr)!i)) ∈ (rstep R)^*"
using r_ast_seq_imp_r_ast[OF ast eq jr] by auto
hence la: "set (map ?l (snd jr)) ⊆ ds (snd ?r) {?l (fst p)}"
unfolding p_dec ds_def get_source_def apply auto
by (metis (no_types, hide_lams) R_d_union_R_nd fst_conv in_set_conv_nth inf_sup_aci(5) rstep_union)
have 1: "ELD_1 ?r (?l (snd p)) (?l (fst p)) [] (map ?l (snd jr)) []"
using la l1 unfolding ELD_1_def by auto
have 2: "ELD_1 ?r (?l (fst p)) (?l (snd p)) (map ?l (snd jl)) [] []"
proof (cases "length (snd jl) ≤ 1")
case True thus ?thesis using assms(2) unfolding diamond_trs_def by auto
next
case False hence nl: "¬ linear_term (snd (get_rule (fst p)))" using d2 unfolding ld2_trs_def by auto
have "(s,t) ∈ rstep_r_p_s R rl1 p1 σ1" using st by auto
hence x: "(s,t) ∈ rstep_r_p_s (R_d R ∪ R_nd R) rl1 p1 σ1" unfolding R_d_def R_nd_def by (metis R_d_def R_d_union_R_nd R_nd_def)
hence "(s,t) ∈ rstep_r_p_s (R_d R) rl1 p1 σ1"
proof (cases "rl1 ∈ R_d R")
case True thus ?thesis using x unfolding R_d_def rstep_r_p_s_def by auto
next
case False
have "rl1 ∈ R" using st unfolding rstep_r_p_s_def apply auto by metis
hence "rl1 ∈ R_nd R" using False unfolding R_d_def R_nd_def by auto
thus ?thesis using nl unfolding p_dec get_rule_def R_nd_def by auto
qed
hence st2: "(s,t) ∈ rstep (R_d R)" by (metis rstep_r_p_s_imp_rstep)
hence "(t,s) ∈ fst ?r" unfolding sl_rel.simps by auto
from st2 have st3: "(s,t) ∈ (relto (rstep (R_d R)) (rstep (R_nd R)))^+" by auto
have uu: "(t,t) ∈ (rstep R)^*" by auto
have eq: "t = first jl" using d2 unfolding ld2_trs_def ldc_trs_def unfolding p_dec get_target_def by auto
from r_ast_seq_imp_r_ast[OF uu eq jl] have y: "∀i<length (snd jl). (t, get_source (snd jl ! i)) ∈ (rstep R)⇧*" by auto
{
fix i assume A: "i < length (snd jl)"
have "(t,get_source (snd jl !i)) ∈ (rstep R)^*" (is "(t,?v) ∈ _") using A y by auto
hence l: "(t,?v) ∈ (rstep (R_d R) ∪ rstep (R_nd R))^*" by (metis R_d_union_R_nd rstep_union)
have k: "(rstep (R_d R) ∪ rstep (R_nd R))^* ⊆ ((rstep (R_nd R))^* ∪ (relto (rstep (R_d R)) (rstep (R_nd R)))^*)" by regexp
hence "(t,?v) ∈ (relto (rstep (R_d R)) (rstep (R_nd R)))^* ∨ (t,?v) ∈ (rstep (R_nd R))^*" using l by auto
hence "(?v, s) ∈ fst (sl_rel (R_d R) (R_nd R))" using st3 apply auto by (metis RS_S_trancl)
}
hence "∀i<length (snd jl). (get_source (snd jl ! i),s) ∈ (fst ?r)" using y by auto
hence "set (map ?l (snd jl)) ⊆ ds (fst ?r) {?l (fst p)}" unfolding p_dec get_source_def ds_def apply auto by (metis fst_conv in_set_idx)
thus ?thesis unfolding ELD_1_def by auto
qed
have "eld_conv source_labeling ?r p jl (last jl,[]) (last jl,[]) (first jr,[]) jr (last jr,[])"
using 1 2 unfolding eld_conv_def by auto
} note * = this
from assms have ld2_trs: "ld2_trs R p jl jr" unfolding ld2_trs_def by auto
show ?thesis using *[OF ld2_trs] by (simp add: eld_conv_def)
qed
qed
lemma SN_rel_compatible:
assumes wll: "weakly_compatible R l r"
and SN: "SN_rel (rstep (R_d R)) (rstep (R_nd R))"
and ll: "left_linear_trs R"
defines "ll ≡ (λ step. (source_labeling step,l step))"
and "rr ≡ (lex_r (sl_rel (R_d R) (R_nd R)) r)" (is "_ ≡ lex_r ?r1 _")
shows "compatible R ll rr"
unfolding compatible_def
proof
from wll show "is_labeling R ll rr" unfolding ll_def rr_def weakly_compatible_def
using is_labeling_lex SN_rel_is_labeling by blast
show "∀p. variable_peak R p ∨ parallel_peak R p ⟶ eldc R ll rr p"
proof (intro allI impI)
fix p
assume A: "variable_peak R p ∨ parallel_peak R p"
then have "weld R l r p" using wll ll unfolding weakly_compatible_def by blast
then obtain jl jr where d2: "ld2_trs R p jl jr" and weld_seq:"weld_seq l r p jl jr"
unfolding weld_def by blast
have cases: "length (snd jl) ≤ 1 ∨ 1 < length (snd jl)" (is "?case1 ∨ ?case2") by auto
{ assume ?case1
hence diamond: "diamond_trs R p jl jr" using d2 unfolding diamond_trs_def ld2_trs_def by auto
have eld: "eld_conv source_labeling (sl_rel (R_d R) (R_nd R)) p (first jl, []) jl (last jl, []) (first jr, []) jr (last jr, [])"
using SN_rel_diamond_trs_imp_eld_seq[OF diamond] diamond unfolding diamond_trs_def ldc_trs_def by auto
have "eld_conv ll rr p (first jl,[]) jl (last jl,[]) (first jr,[]) jr (last jr,[])"
using eld_seq_and_weld_seq_imp_eld_seq2[OF diamond eld weld_seq] unfolding ll_def rr_def by auto
} note 1 = this
{ assume case2: ?case2
have eld_conv: "eld_conv source_labeling (sl_rel (R_d R) (R_nd R)) p jl (last jl, []) (last jl, []) (first jr, []) jr (last jr, [])"
using SN_rel_ld2_trs_imp_eld_seq[OF d2 case2 SN] by auto
have "eld_conv ll rr p jl (last jl,[]) (last jl,[]) (first jr,[]) jr (last jr,[])"
using eld_seq_and_weld_seq_imp_eld_seq[OF d2 eld_conv weld_seq] unfolding ll_def rr_def by auto
} note 2 = this
from d2 have "ldc_trs R p jl (last jl,[]) (last jl,[]) (first jr,[]) jr (last jr,[])"
by (simp add: ldc_trs_def seq.intros(1) seq_imp_conv ld2_trs_def)
moreover have "ldc_trs R p (first jl,[]) jl (last jl,[]) (first jr,[]) jr (last jr,[])"
using d2 unfolding ld2_trs_def ldc_trs_def by auto
moreover have "eld_conv ll rr p jl (last jl,[]) (last jl,[]) (first jr,[]) jr (last jr,[]) ∨
eld_conv ll rr p (first jl,[]) jl (last jl,[]) (first jr,[]) jr (last jr,[])"
using 1 2 cases by auto
ultimately show "eldc R ll rr p" unfolding eldc_def by blast
qed
qed
lemma SN_rel_lex:
assumes wll: "weakly_compatible R l r"
and rp: "rel_props (fst r) (snd r)"
and SN: "SN_rel (rstep (R_d R)) (rstep (R_nd R))"
and dec: "∀ (b,p) ∈ critical_peaks R. eld_fan R l r p"
and ll: "left_linear_trs R"
defines "ll ≡ (λ step. (source_labeling step,l step))"
and "rr ≡ (lex_r (sl_rel (R_d R) (R_nd R)) r)" (is "_ ≡ lex_r ?r1 ?r2")
shows "rel_props (fst rr) (snd rr)"
and "compatible R ll rr"
and "∀ (b,p) ∈ critical_peaks R. eldc R ll rr p"
proof -
show "rel_props (fst rr) (snd rr)"
using rel_props_lex rp SN_rel_has_rel_props SN unfolding rr_def by blast
show "compatible R ll rr" using assms SN_rel_compatible by fast
show "∀(b, p)∈critical_peaks R. eldc R ll rr p"
using source_labeling_eld_imp_eld dec unfolding ll_def rr_def by fast
qed
lemma rule_labeling_conv_is_sound_ll:
defines "r ≡ ({(n,m). n < (m::nat)},{(n,m). n ≤ (m::nat)})"
assumes ll: "left_linear_trs R"
and SN: "SN_rel (rstep (R_d R)) (rstep (R_nd R))"
and dec: "∀ (b,p) ∈ critical_peaks R. eld_fan R (rule_labeling i) r p"
shows "CR (rstep R)"
proof -
have r: "refl (snd r)" unfolding r_def refl_on_def by simp
have rp: "rel_props (fst r) (snd r)" using rule_labeling_has_rel_props unfolding r_def by fast
have el: "weakly_compatible R (rule_labeling i) r"
using rule_labeling_is_weakly_compatible[OF r ll] by auto
from SN_rel_lex[OF el rp SN dec ll] show ?thesis using main by blast
qed
lemma ld_trs_implies_ldc_trs:
assumes "ld_trs R p jl1 jl2 jl3 jr1 jr2 jr3"
shows "ldc_trs R p jl1 jl2 jl3 jr1 jr2 jr3"
using assms unfolding ld_trs_def ldc_trs_def using seq_imp_conv by blast
thm seq.induct
lemma seq_imp_ast2:
assumes "jl ∈ seq R"
shows "(first jl, last jl) ∈ (rstep R)⇧*"
proof -
obtain s ss where jl:"jl = (s, ss)" by (cases jl, auto)
from assms[unfolded jl] have "(first (s, ss), last (s, ss)) ∈ (rstep R)⇧*"
proof (induct rule: seq.induct)
case (2 s t r p σ ts)
then have "(s, t) ∈ rstep R" using rstep_r_p_s_imp_rstep by blast
with 2 show ?case by (auto simp: get_target_def r_into_rtrancl)
qed auto
then show ?thesis unfolding jl by auto
qed
lemma seq_comp2:
assumes jl: "jl ∈ seq R" and "(s,first jl) ∈ (rstep R)⇧*"
shows "(s,last jl) ∈ (rstep R)⇧*"
proof -
have "(first jl, last jl) ∈ (rstep R)⇧* " using assms seq_imp_ast2[OF jl] by auto
thus ?thesis using assms using rtrancl_trans by auto
qed
lemma seq_comp:
assumes "jl ∈ seq R" and "(s,first jl) ∈ (rstep R)⇧*"
shows "∀i < length (snd jl). (s, get_source (snd jl ! i)) ∈ (rstep R)⇧*" proof -
{fix i
assume A: "i < length (snd jl)"
from A have "(s, get_source (snd jl ! i)) ∈ (rstep R)⇧*" using assms(1) assms(2) r_ast_seq_imp_r_ast by blast
} thus ?thesis by auto
qed
lemma ld_trs_implies_fan:
assumes ld_trs: "ld_trs R p jl1 jl2 jl3 jr1 jr2 jr3"
shows "fan R p jl1 jl2 jl3 jr1 jr2 jr3"
proof -
have eq: "get_source (fst p) = get_source (snd p)" using ld_trs unfolding ld_trs_def local_peaks_def get_source_def by auto
have jl1: "jl1 ∈ seq R" and jl2: "jl2 ∈ seq R" and jl3: "jl3 ∈ seq R"
and eq_jl12: "last jl1 = first jl2" and eq_jl23: "last jl2 = first jl3"
and jr1: "jr1 ∈ seq R" and jr2: "jr2 ∈ seq R" and jr3: "jr3 ∈ seq R"
and eq_jr12: "last jr1 = first jr2" and eq_jr23: "last jr2 = first jr3"
using ld_trs unfolding ld_trs_def by auto
from assms have "(get_source (fst p),first jl1) ∈ rstep R"
using ld_trs unfolding ld_trs_def local_peaks_def get_source_def get_target_def
using rstep_r_p_s_imp_rstep by force
hence L1: "(get_source (fst p),first jl1) ∈ (rstep R)⇧*" by auto
have L2: "(get_source (fst p),first jl2) ∈ (rstep R)⇧*" using seq_comp2[OF jl1 L1] eq_jl12 by auto
have L3: "(get_source (fst p),first jl3) ∈ (rstep R)⇧*" using seq_comp2[OF jl2 L2] eq_jl23 by auto
from assms have "(get_source (snd p), first jr1) ∈ rstep R"
using ld_trs unfolding ld_trs_def local_peaks_def get_source_def get_target_def
using rstep_r_p_s_imp_rstep by force
hence R1: "(get_source (snd p),first jr1) ∈ (rstep R)⇧*" by auto
have R2: "(get_source (snd p),first jr2) ∈ (rstep R)⇧*" using seq_comp2[OF jr1 R1] eq_jr12 by auto
have R3: "(get_source (snd p),first jr3) ∈ (rstep R)⇧*" using seq_comp2[OF jr2 R2] eq_jr23 by auto
from seq_comp[OF jl1 L1] seq_comp[OF jl2 L2] seq_comp[OF jl3 L3]
seq_comp[OF jr1 R1] seq_comp[OF jr2 R2] seq_comp[OF jr3 R3]
show ?thesis unfolding fan_def using eq by auto
qed
lemma rule_labeling_is_sound_ll:
defines "r ≡ ({(n,m). n < (m::nat)},{(n,m). n ≤ (m::nat)})"
assumes ll: "left_linear_trs R"
and SN: "SN_rel (rstep (R_d R)) (rstep (R_nd R))"
and dec: "∀ (b,p) ∈ critical_peaks R. eld R (rule_labeling i) r p"
shows "CR (rstep R)"
proof -
have "∀ (b,p) ∈ critical_peaks R. eld_fan R (rule_labeling i) r p"
proof
fix b p assume A: "(b,p) ∈ critical_peaks R"
from A dec have eld: "eld R (rule_labeling i) r p" by auto
have "eld_fan R (rule_labeling i) r p" using eld unfolding eld_fan_def eld_def
using ld_trs_implies_ldc_trs ld_trs_implies_fan by metis
then show "eld_fan R (rule_labeling i) r p" by auto
qed
then show ?thesis using SN ll r_def rule_labeling_conv_is_sound_ll by auto
qed
hide_const (open) last
end