theory Rule_Labeling_Impl
imports
Decreasing_Diagrams2
"Check-NT.Critical_Pairs_Impl"
Equational_Reasoning_Impl
QTRS.Map_Choice
begin
abbreviation DD2_last where "DD2_last ≡ Decreasing_Diagrams2.last"
definition critical_peaks_impl :: "('f,string)rules ⇒ ('f,string)rules ⇒ (bool × ('f,string) lpeak) list"
where "critical_peaks_impl P R ≡ concat (map (λ (l,r).
concat (map (λ p. let C = ctxt_of_pos_term p l; l'' = l |_ p; b = (C = □) in
if is_Var l'' then [] else
concat (map (λ (l',r'). case mgu_var_disjoint_string l'' l' of
Some (σ,τ) ⇒ [(b, (l ⋅ σ, (l, r), ε, σ, True, r ⋅ σ), (l ⋅ σ, (l', r'), p, τ, True, (C ⋅⇩c σ)⟨r' ⋅ τ⟩))]
| None ⇒ []) R)) (poss_list l))) P)"
lemma critical_peaks_impl:
"set (critical_peaks_impl R R) = critical_peaks (set R)" (is "?l = ?r")
proof -
note cpdefs = critical_peaks_impl_def critical_peaks_def set_concat
set_map Let_def poss_list_sound
{
fix b s1 s2
assume "(b,s1,s2) ∈ ?r"
from this[unfolded cpdefs]
obtain l r l' r' l'' C σ τ where
b: "b = (C = □)" and s1: "s1 = (l ⋅ σ, (l, r), ε, σ, True, r ⋅ σ)"
and s2: "s2 = ( l ⋅ σ, (l', r'), hole_pos C, τ, True, (C ⋅⇩c σ)⟨r' ⋅ τ⟩)"
and lr: "(l, r) ∈ set R" and lr': "(l', r') ∈ set R"
and l: "l = C⟨l''⟩" and l'': "is_Fun l''"
and mgu: "mgu_var_disjoint_string l'' l' = Some (σ, τ)"
by auto
let ?p = "hole_pos C"
from l have p: "?p ∈ poss l" by auto
from l p have C: "C = ctxt_of_pos_term ?p l" by auto
from l p have l: "l |_ ?p = l''" by auto
have "(b,s1,s2) ∈ ?l" unfolding cpdefs b s1 s2
by (rule, rule, rule lr, unfold cpdefs, rule, rule imageI[OF p],
insert C l lr' l'' mgu, force)
}
hence "?r ⊆ ?l" by auto
moreover
{
fix b s1 s2
assume "(b,s1,s2) ∈ ?l"
from this[unfolded cpdefs]
obtain l r p l' r' σ τ where
lr: "(l,r) ∈ set R" and p: "p ∈ poss l" and lp: "is_Fun (l |_ p)"
and lr': "(l',r') ∈ set R"
and mgu: "Some (σ,τ) = mgu_var_disjoint_string (l |_ p) l'"
and b: "b = (ctxt_of_pos_term p l = □)"
and s1: "s1 = (l ⋅ σ, (l, r), ε, σ, True, r ⋅ σ)"
and s2: "s2 = (l ⋅ σ, (l', r'), p, τ, True, (ctxt_of_pos_term p l ⋅⇩c σ)⟨r' ⋅ τ⟩)"
by force
from p have pp: "hole_pos (ctxt_of_pos_term p l) = p" by simp
from s1 have s: "get_target s1 = r ⋅ σ" unfolding get_target_def by simp
from s2 have t: "get_target s2 = (ctxt_of_pos_term p l ⋅⇩c σ)⟨r' ⋅ τ⟩"
unfolding get_target_def by simp
from critical_peaksI[OF lr lr' _ lp mgu[symmetric] s t b]
have "(b,s1,s2) ∈ ?r" using ctxt_supt_id[OF p, symmetric] s1 s2 pp
unfolding get_target_def by auto
}
hence "?l ⊆ ?r" by auto
ultimately show ?thesis by auto
qed
type_synonym ('f, 'v) rule_lab_repr = "(('f, 'v) rule × nat) list"
definition rule_lab_repr_to_lab :: "('f :: key, 'v :: key ) rule_lab_repr ⇒ ('f, 'v) rule ⇒ nat"
where
"rule_lab_repr_to_lab ps = fun_of_map (ceta_map_of ps) 0"
fun rseq_to_step_list :: "('f, 'v) term ⇒ ('f, 'v) rseq ⇒ ('f, 'v) step list"
where
"rseq_to_step_list s [] = []"
| "rseq_to_step_list s ((p,lr,t) # steps) = (
let u = subt_at s p;
v = subt_at t p;
σ = (case match_list Var [(fst lr, u), (snd lr, v)] of
Some τ ⇒ τ
| None ⇒ undefined)
in (s,lr,p,σ,True,t) # rseq_to_step_list t steps)"
primrec rseq_to_ddseq :: "('f, 'v) term × ('f, 'v) rseq ⇒ ('f, 'v) seq"
where "rseq_to_ddseq (s, rseq) = (s, rseq_to_step_list s rseq)"
lemma check_rsteps'_sound_dd_seq:
assumes "isOK (check_rsteps' R rseq s w)"
shows "rseq_to_ddseq (s, rseq) ∈ seq (set R) ∧ DD2_last (rseq_to_ddseq (s, rseq)) = w"
using assms
proof (induct rseq arbitrary: s)
case Nil
have "rseq_to_ddseq (s, []) ∈ seq (set R)" using seq.intros by auto
moreover have "DD2_last (rseq_to_ddseq (s, [])) = s" by auto
moreover have "s = w" using Nil check_rsteps_sound by fastforce
ultimately show ?case by auto
next
case (Cons r rs)
show ?case
proof (cases r)
case (fields p lr t)
with Cons have IH: "rseq_to_ddseq (t, rs) ∈ seq (set R)" and
"DD2_last (rseq_to_ddseq (t, rs)) = w" by auto
with fields have last:"DD2_last (rseq_to_ddseq (s, r # rs)) = w"
by (simp add: get_target_def)
let ?σ = "case match_list Var [(fst lr, s |_ p), (snd lr, t |_ p)] of Some τ ⇒ τ"
from fields Cons(2) obtain τ where
"lr ∈ set R" and "p ∈ poss s" and "p ∈ poss t" and
"ctxt_of_pos_term p s = ctxt_of_pos_term p t" and
"match_list Var [(fst lr, s |_ p), (snd lr, t |_ p)] = Some τ"
apply (simp del: check_rstep')
unfolding check_rstep'_def unfolding check_prop_rstep'_def
unfolding check_prop_rstep_rule_def unfolding Let_def
apply (cases "match_list Var [(fst lr, s |_ p), (snd lr, t |_ p)]") by auto
moreover from this match_list_matches have "(fst lr) ⋅ ?σ = s |_ p ∧ (snd lr) ⋅ ?σ = t |_ p"
by fastforce
ultimately have "(s, t) ∈ rstep_r_p_s (set R) lr p ?σ"
unfolding rstep_r_p_s_def' by (cases lr, auto simp: replace_at_ident)
with IH have "rseq_to_ddseq (s, r # rs) ∈ seq (set R)" using fields seq.intros by fastforce
with last show ?thesis by blast
qed
qed
fun eseq_to_step_list :: "('f, 'v) term ⇒ ('f, 'v) eseq ⇒ ('f, 'v) step list"
where
"eseq_to_step_list s [] = []"
| "eseq_to_step_list s ((p,lr,b,t) # steps) = (
let u = subt_at s p; v = subt_at t p in
if b then (let σ = (case match_list Var [(fst lr, u), (snd lr, v)] of
Some τ ⇒ τ
| None ⇒ undefined)
in (s,lr,p,σ,b,t) # eseq_to_step_list t steps)
else (let σ = (case match_list Var [(snd lr, u), (fst lr, v)] of
Some τ ⇒ τ
| None ⇒ undefined)
in (t,lr,p,σ,b,s) # eseq_to_step_list t steps))"
primrec eseq_to_ddconv :: "('f, 'v) term × ('f, 'v) eseq ⇒ ('f, 'v) conv"
where "eseq_to_ddconv (s, eseq) = (s, eseq_to_step_list s eseq)"
definition
check_estep' ::
"('f::show, 'v::show) equation list ⇒
pos ⇒ ('f, 'v) rule ⇒ bool ⇒ ('f, 'v) term ⇒ ('f, 'v) term ⇒
shows check"
where
"check_estep' E p rule l_to_r s t ≡ do {
check (rule ∈ set E)
(shows_rule rule +@+ ''is not an equation of'' +#+ shows_nl +@+ shows_eqs E +@+ shows_nl);
check (p ∈ poss s) (shows p +@+ '' is not a position of '' +#+ shows s +@+ shows_nl);
check (p ∈ poss t) (shows p +@+ '' is not a position of '' +#+ shows t +@+ shows_nl);
let C = ctxt_of_pos_term p s;
let D = ctxt_of_pos_term p t;
let u = subt_at s p;
let v = subt_at t p;
let rrule = (if l_to_r then rule else (snd rule, fst rule));
let err = (''the term '' +#+ shows t
+@+ '' does not result from a proper application of term '' +#+ shows s +@+ '' using equation ''
+#+ shows_nl +@+ shows_eq rrule +@+ '' at position '' +#+ shows p +@+ shows_nl);
(case match_list Var [(fst rrule, u), (snd rrule, v)] of
Some σ ⇒ check (C = D) err
| None ⇒ error err)
}"
fun
check_conversion' ::
"('f::show, 'v::show) equation list ⇒
('f, 'v) eseq ⇒ ('f, 'v) term ⇒ ('f, 'v) term ⇒ shows check"
where
"check_conversion' E [] s u = check (s = u) (
''the last term of the conversion '' +#+ shows_nl +@+ shows s +@+ shows_nl +@+
''does not correspond to the goal term'' +#+ shows_nl +@+ shows u +@+ shows_nl)"
| "check_conversion' E ((p, r, l_to_r, t) # c) s u = do {
check_estep' E p r l_to_r s t;
check_conversion' E c t u
}"
definition eseq_last :: "('f,'v)term ⇒ ('f,'v) eseq ⇒ ('f,'v)term"
where "eseq_last s steps ≡ last (s # map (λ (_,_,_,s). s) steps)"
lemma check_conversion_sound_dd_conv:
assumes "isOK (check_conversion' E eseq s w)"
shows "eseq_to_ddconv (s, eseq) ∈ conv (set E) ∧ DD2_last (eseq_to_ddconv (s, eseq)) = w"
using assms
proof (induct eseq arbitrary: s)
case Nil
have "eseq_to_ddconv (s, []) ∈ conv (set E)" by (auto intro: conv.intros)
moreover have "DD2_last (eseq_to_ddconv (s, [])) = s" by auto
moreover have "s = w" using Nil by fastforce
ultimately show ?case by auto
next
case (Cons r rs)
show ?case
proof (cases r)
case (fields p lr b t)
with Cons have IH: "eseq_to_ddconv (t, rs) ∈ conv (set E)" and
"DD2_last (eseq_to_ddconv (t, rs)) = w" by auto
with fields have last:"DD2_last (eseq_to_ddconv (s, r # rs)) = w"
by (cases b) (auto simp: get_target_def)
show ?thesis
proof (cases b)
case True
let ?σ = "case match_list Var [(fst lr, s |_ p), (snd lr, t |_ p)] of Some τ ⇒ τ"
from fields Cons(2) True obtain τ where
"lr ∈ set E" and "p ∈ poss s" and "p ∈ poss t" and
"ctxt_of_pos_term p s = ctxt_of_pos_term p t" and
"match_list Var [(fst lr, s |_ p), (snd lr, t |_ p)] = Some τ"
apply (simp add: check_estep'_def Let_def)
apply (cases "match_list Var [(fst lr, s |_ p), (snd lr, t |_ p)]") by auto
moreover with match_list_matches have "(fst lr) ⋅ ?σ = s |_ p ∧ (snd lr) ⋅ ?σ = t |_ p"
by fastforce
ultimately have step:"(s, t) ∈ rstep_r_p_s (set E) lr p ?σ"
unfolding rstep_r_p_s_def' by (cases lr, auto simp: replace_at_ident)
from IH have "eseq_to_ddconv (s, r # rs) ∈ conv (set E)" unfolding fields
using True conv.intros(2)[OF step] by simp
with last show ?thesis by blast
next
case False
let ?σ = "case match_list Var [(snd lr, s |_ p), (fst lr, t |_ p)] of Some τ ⇒ τ"
from fields Cons(2) False obtain τ where
"lr ∈ set E" and "p ∈ poss s" and "p ∈ poss t" and
"ctxt_of_pos_term p t = ctxt_of_pos_term p s" and
"match_list Var [(snd lr, s |_ p), (fst lr, t |_ p)] = Some τ"
apply (simp add: check_estep'_def Let_def)
apply (cases "match_list Var [(snd lr, s |_ p), (fst lr, t |_ p)]") by auto
moreover with match_list_matches have "(fst lr) ⋅ ?σ = t |_ p ∧ (snd lr) ⋅ ?σ = s |_ p"
by fastforce
ultimately have step:"(t, s) ∈ rstep_r_p_s (set E) lr p ?σ"
unfolding rstep_r_p_s_def' by (cases lr, auto simp: replace_at_ident)
from IH have "eseq_to_ddconv (s, r # rs) ∈ conv (set E)" unfolding fields
using False conv.intros(3)[OF step] by simp
with last show ?thesis by blast
qed
qed
qed
definition check_ELD_1_nat :: "nat ⇒ nat ⇒ nat list ⇒ nat list ⇒ nat list ⇒ shows check"
where
"check_ELD_1_nat β α σ⇩1 σ⇩2 σ⇩3 = do {
check_allm (λx. check (x < β)
(shows ''the labels are not decreasing: '' +@+ shows x +@+ shows '' is not smaller '' +@+ shows β +@+ shows_nl)) σ⇩1;
check_allm (λx. check (x ≤ α)
(shows ''the labels are not decreasing: '' +@+ shows x +@+ shows '' is not smaller equal '' +@+ shows α +@+ shows_nl)) σ⇩2;
check (length σ⇩2 ≤ 1) (shows '' the length of the middle sequence is greater 1'' +@+ shows_nl);
check_allm (λx. check (x < α ∨ x < β)
(shows ''the labels are not decreasing: '' +@+ shows x +@+ shows '' is not smaller ''
+@+ shows α +@+ shows '' or smaller '' +@+ shows β +@+ shows_nl)) σ⇩3
}"
lemma check_ELD_1_nat :
assumes "isOK (check_ELD_1_nat β α σ⇩1 σ⇩2 σ⇩3)"
shows "ELD_1 ({(n, m). n < m},{(n, m). n ≤ m}) β α σ⇩1 σ⇩2 σ⇩3"
using assms
unfolding check_ELD_1_nat_def ELD_1_def ds_def
by auto
definition split_seq :: "nat ⇒ nat ⇒ nat list ⇒ nat list × nat list × nat list"
where
"split_seq α β ss = (
let (ss', r) = span (λn. n < α) ss in
case r of
Nil ⇒ (ss',[],[])
| Cons h t ⇒ if h ≤ β then (ss',[h],t) else (ss',[],r)
)"
lemma split_seq_is_split:
assumes "split_seq α β ss = (ss⇩1, ss⇩2, ss⇩3)"
shows "ss⇩1 @ ss⇩2 @ ss⇩3 = ss"
using assms
by (auto split: list.splits if_splits simp: split_seq_def) (metis takeWhile_dropWhile_id)
lemma split_complete:
assumes "split_seq α β ss = (ss⇩1, ss⇩2, ss⇩3)"
and "∀ x ∈ set ss⇩3. x < α ∨ x < β"
shows "ELD_1 ({(n, m). n < m},{(n, m). n ≤ m}) α β ss⇩1 ss⇩2 ss⇩3"
proof -
obtain ss' r where sp: "(ss', r) = span (λn. n < α) ss" by auto
show ?thesis
proof (cases r)
case Nil
with assms sp have "ss⇩1 = ss'" "ss⇩2 = []" "ss⇩3 = []"
unfolding split_seq_def Let_def by auto
with sp show ?thesis unfolding ELD_1_def using set_takeWhileD under_def by fastforce
next
case (Cons h t)
show ?thesis
proof(cases "h ≤ β")
case True
with assms sp Cons have "ss⇩1 = ss'" "ss⇩2 = [h]" "ss⇩3 = t"
unfolding split_seq_def Let_def by (case_tac "dropWhile (λn. n < α) ss", auto)+
with sp True Cons show ?thesis unfolding ELD_1_def ds_def apply auto
by (metis set_takeWhileD) (metis assms(2))
next
case False
with assms sp Cons have "ss⇩1 = ss'" "ss⇩2 = []" "ss⇩3 = r"
unfolding split_seq_def Let_def by (case_tac "dropWhile (λn. n < α) ss", auto)+
with sp False Cons show ?thesis unfolding ELD_1_def ds_def apply auto
by (metis set_takeWhileD) (metis assms(2))
qed
qed
qed
definition check_cpeak_eld ::
"('f :: show, 'v :: show) rules ⇒ ('f, 'v) lpeak ⇒ ('f, 'v) rule ⇒('f, 'v) rseq ⇒ ('f, 'v) rseq ⇒
(('f, 'v) rule ⇒ nat) ⇒ shows check"
where
"check_cpeak_eld R p cp j1 j2 lab =
(case p of ((s1,r1,p1,σ1,True,t1),(s2,r2,p2,σ2,True,t2)) ⇒
do {
check (instance_rule (t1, t2) cp) id;
let u = rseq_last (fst cp) j1;
let v = rseq_last (snd cp) j2;
check_rsteps' R j1 (fst cp) u;
check_rsteps' R j2 (snd cp) v;
check (u = v) (shows ''the rewrite sequences end in different terms: ''
+@+ shows u +@+ shows '' and '' +@+ shows v +@+ shows_nl);
let α = lab r1;
let β = lab r2;
let τ = map (rule_labeling lab) (snd (rseq_to_ddseq (t1, j1)));
let σ = map (rule_labeling lab) (snd (rseq_to_ddseq (t2, j2)));
let (τ⇩1, τ⇩2, τ⇩3) = split_seq α β τ;
let (σ⇩1, σ⇩2, σ⇩3) = split_seq β α σ;
check_ELD_1_nat α β τ⇩1 τ⇩2 τ⇩3;
check_ELD_1_nat β α σ⇩1 σ⇩2 σ⇩3
})"
lemma check_cpeak_eld:
defines "r ≡ ({(n, m) . n < m}, {(n, m) . n ≤ m})"
assumes "(b, (s1,r1,p1,σ1,True,t1),(s2,r2,p2,σ2,True,t2)) ∈ critical_peaks (set R)" (is "(b, ?p) ∈ critical_peaks (set R)")
and "isOK (check_cpeak_eld R ((s1,r1,p1,σ1,True,t1),(s2,r2,p2,σ2,True,t2)) cp j1 j2 lab)"
shows "eld (set R) (rule_labeling lab) r ?p" (is "eld _ ?l _ _")
proof -
let ?u = "rseq_last (fst cp) j1"
let ?v = "rseq_last (snd cp) j2"
let ?j1cp = "rseq_to_ddseq ((fst cp), j1)"
let ?j2cp = "rseq_to_ddseq ((snd cp), j2)"
let ?j1t = "rseq_to_ddseq (t1, j1)"
let ?j2t = "rseq_to_ddseq (t2, j2)"
from assms have
steps1: "isOK (check_rsteps' R j1 (fst cp) ?u)" and
steps2: "isOK (check_rsteps' R j2 (snd cp) ?v)"and
eq: "?u = ?v" and
inst: "instance_rule (t1, t2) cp"
by (auto simp add: Let_def check_cpeak_eld_def)
from inst obtain ρ where ρ: "t1 = fst cp ⋅ ρ ∧ t2 = snd cp ⋅ ρ"
unfolding instance_rule_def by auto
let ?j1ρ = "seq_close ?j1cp □ ρ"
let ?j2ρ = "seq_close ?j2cp □ ρ"
from assms obtain σ1 σ2 σ3 τ1 τ2 τ3 where
σ: "(σ1,σ2,σ3) = split_seq (lab r2) (lab r1) (map ?l (snd ?j2t))" and
τ: "(τ1,τ2,τ3) = split_seq (lab r1) (lab r2) (map ?l (snd ?j1t))" and
σok: "isOK (check_ELD_1_nat (lab r2) (lab r1) σ1 σ2 σ3)" and
τok: "isOK (check_ELD_1_nat (lab r1) (lab r2) τ1 τ2 τ3)"
unfolding Let_def check_cpeak_eld_def using check_ELD_1_nat by auto
moreover have "map ?l (snd ?j1t) = map ?l (snd ?j1ρ)" by (induct j1, auto)
moreover have "map ?l (snd ?j2t) = map ?l (snd ?j2ρ)" by (induct j2, auto)
ultimately have σ2: "split_seq (lab r2) (lab r1) (map ?l (snd ?j2ρ)) = (σ1,σ2,σ3)"
and τ2: "split_seq (lab r1) (lab r2) (map ?l (snd ?j1ρ)) = (τ1,τ2,τ3)" by auto
from assms(2) critical_peak_is_local_peak have lp:"?p ∈ local_peaks (set R)" by fast
from steps1 check_rsteps'_sound_dd_seq have j1cpseq: "?j1cp ∈ seq (set R)" and
j1cplast:"DD2_last ?j1cp = ?u" by auto
from steps2 check_rsteps'_sound_dd_seq have j2cpseq: "?j2cp ∈ seq (set R)" and
j2cplast:"DD2_last ?j2cp = ?v" by auto
from seq_super_closed1[OF j1cpseq, of "□" ρ] ρ j1cplast have j1seq:"?j1ρ ∈ seq (set R)"
and " get_target (fst ?p) = first ?j1ρ" and "DD2_last ?j1ρ = ?u ⋅ ρ"
unfolding get_target_def by auto
moreover from seq_super_closed1[OF j2cpseq, of "□" ρ] ρ j2cplast have j2seq:"?j2ρ ∈ seq (set R)"
and " get_target (snd ?p) = first ?j2ρ" and "DD2_last ?j2ρ = ?v ⋅ ρ"
unfolding get_target_def by auto
moreover from seq_dec[OF j2seq split_seq_is_split[OF σ2,symmetric]] obtain jr1 jr23 where
"?j2ρ = seq_concat jr1 jr23" and "jr1 ∈ seq (set R)" and "jr23 ∈ seq (set R)" and
"map ?l (snd jr1) = σ1" and σ23:"map ?l (snd jr23) = σ2 @ σ3" and "first ?j2ρ = first jr1" and
"DD2_last jr1 = first jr23" and "DD2_last jr23 = DD2_last ?j2ρ" by blast
moreover from seq_dec[OF ‹jr23 ∈ seq (set R)› σ23] obtain jr2 jr3 where
"jr23 = seq_concat jr2 jr3" and "jr2 ∈ seq (set R)" and "jr3 ∈ seq (set R)" and
"map ?l (snd jr2) = σ2" and "map ?l (snd jr3) = σ3" and "first jr23 = first jr2" and
"DD2_last jr2 = first jr3" and "DD2_last jr3 = DD2_last jr23" by blast
moreover from seq_dec[OF j1seq split_seq_is_split[OF τ2,symmetric]] obtain jl1 jl23 where
"?j1ρ = seq_concat jl1 jl23" and "jl1 ∈ seq (set R)" and "jl23 ∈ seq (set R)" and
"map ?l (snd jl1) = τ1" and τ23:"map ?l (snd jl23) = τ2 @ τ3" and "first ?j1ρ = first jl1" and
"DD2_last jl1 = first jl23" and "DD2_last jl23 = DD2_last ?j1ρ" by blast
moreover from seq_dec[OF ‹jl23 ∈ seq (set R)› τ23] obtain jl2 jl3 where
"jl23 = seq_concat jl2 jl3" and "jl2 ∈ seq (set R)" and "jl3 ∈ seq (set R)" and
"map ?l (snd jl2) = τ2" and "map ?l (snd jl3) = τ3" and "first jl23 = first jl2" and
"DD2_last jl2 = first jl3" and "DD2_last jl3 = DD2_last jl23" by blast
ultimately moreover have ld:"ld_trs (set R) ?p jl1 jl2 jl3 jr1 jr2 jr3"
unfolding ld_trs_def using lp eq by (auto simp: seq_concat_def)
ultimately have "eld_conv (rule_labeling lab) r ?p jl1 jl2 jl3 jr1 jr2 jr3"
unfolding eld_conv_def r_def using check_ELD_1_nat[OF σok] check_ELD_1_nat[OF τok]
by auto
with ld show ?thesis unfolding eld_def by fast
qed
definition "cpeak_instance s cp s' cp' =
(match_list (λ _. s) [(s, s'), (fst cp, fst cp'), (snd cp, snd cp')] ≠ None)"
definition check_cpeak_eldc ::
"('f :: show, 'v :: show) rules ⇒ ('f, 'v) lpeak ⇒ ('f, 'v) term ⇒ ('f, 'v) rule ⇒
('f, 'v) eseq ⇒ ('f, 'v) rseq ⇒ ('f, 'v) eseq ⇒ ('f, 'v) eseq ⇒ ('f, 'v) rseq ⇒ ('f, 'v) eseq ⇒
(('f, 'v) rule ⇒ nat) ⇒ nat option ⇒ shows check"
where
"check_cpeak_eldc R p s cp cl⇩1 sl cl⇩2 cr⇩1 sr cr⇩2 lab n =
(case p of ((s1,r1,p1,σ1,True,t1),(s2,r2,p2,σ2,True,t2)) ⇒
do {
check (cpeak_instance s cp s1 (t1, t2)) id;
let u⇩1 = eseq_last (fst cp) cl⇩1;
let v⇩1 = eseq_last (snd cp) cr⇩1;
let u⇩2 = rseq_last u⇩1 sl;
let v⇩2 = rseq_last v⇩1 sr;
let u⇩3 = eseq_last u⇩2 cl⇩2;
let v⇩3 = eseq_last v⇩2 cr⇩2;
check_conversion' R cl⇩1 (fst cp) u⇩1;
check_rsteps' R sl u⇩1 u⇩2;
check_conversion' R cl⇩2 u⇩2 u⇩3;
check_conversion' R cr⇩1 (snd cp) v⇩1;
check_rsteps' R sr v⇩1 v⇩2;
check_conversion' R cr⇩2 v⇩2 v⇩3;
check (u⇩3 = v⇩3) (shows ''the conversions end in different terms: '' +@+
shows u⇩3 +@+ shows '' and '' +@+ shows v⇩3 +@+ shows_nl);
let α = lab r1;
let β = lab r2;
let cl⇩1 = snd (eseq_to_ddconv (fst cp, cl⇩1));
let sl = snd (rseq_to_ddseq (u⇩1, sl));
let cl⇩2 = snd (eseq_to_ddconv (u⇩2, cl⇩2));
let cr⇩1 = snd (eseq_to_ddconv (snd cp, cr⇩1));
let sr = snd (rseq_to_ddseq (v⇩1, sr));
let cr⇩2 = snd (eseq_to_ddconv (v⇩2, cr⇩2));
let τ⇩1 = map (rule_labeling lab) cl⇩1;
let τ⇩2 = map (rule_labeling lab) sl;
let τ⇩3 = map (rule_labeling lab) cl⇩2;
let σ⇩1 = map (rule_labeling lab) cr⇩1;
let σ⇩2 = map (rule_labeling lab) sr;
let σ⇩3 = map (rule_labeling lab) cr⇩2;
check_ELD_1_nat α β τ⇩1 τ⇩2 τ⇩3;
check_ELD_1_nat β α σ⇩1 σ⇩2 σ⇩3;
case n of
Some n ⇒ do {
let check_reachable = (λt. check (List.member (reachable_terms R s n) t)
(shows ''the fan property is violated: '' +@+ shows t +@+
shows '' is not reachable from '' +@+ shows s +@+
shows '' in '' +@+ shows n +@+ shows '' steps'' +@+ shows_nl));
check_allm check_reachable (map get_source cl⇩1);
check_allm check_reachable (map get_source sl);
check_allm check_reachable (map get_source cl⇩2);
check_allm check_reachable (map get_source cr⇩1);
check_allm check_reachable (map get_source sr);
check_allm check_reachable (map get_source cr⇩2)
}
| None ⇒ succeed
})"
lemma get_source_closed:
assumes "i < length ss"
shows "get_source ((map (λstep. step_close step C σ) ss) ! i) = C⟨get_source (ss ! i) ⋅ σ⟩"
using assms
proof (induct ss arbitrary: i)
case Nil
then show ?case by (auto simp: get_source_def)
next
case (Cons step ss)
then show ?case by (cases step, cases i) (auto simp: get_source_def)
qed
lemma check_cpeak_eldc:
defines "r ≡ ({(n, m) . n < m}, {(n, m) . n ≤ m})"
assumes "(b, (s1,r1,p1,σ1,True,t1),(s2,r2,p2,σ2,True,t2)) ∈ critical_peaks (set R)" (is "(b, ?p) ∈ critical_peaks (set R)")
and "isOK (check_cpeak_eldc R ((s1,r1,p1,σ1,True,t1),(s2,r2,p2,σ2,True,t2)) s cp cl⇩1 sl cl⇩2 cr⇩1 sr cr⇩2 lab n)"
and "n = None ⟶ linear_trs (set R)"
shows "eld_fan (set R) (rule_labeling lab) r ?p ∨ eldc (set R) (rule_labeling lab) r ?p ∧ linear_trs (set R)" (is "eld_fan _ ?l _ _ ∨ _")
proof -
let ?u⇩1 = "eseq_last (fst cp) cl⇩1"
let ?v⇩1 = "eseq_last (snd cp) cr⇩1"
let ?u⇩2 = "rseq_last ?u⇩1 sl"
let ?v⇩2 = "rseq_last ?v⇩1 sr"
let ?u⇩3 = "eseq_last ?u⇩2 cl⇩2"
let ?v⇩3 = "eseq_last ?v⇩2 cr⇩2"
let ?cl⇩1 = "eseq_to_ddconv (fst cp, cl⇩1)"
let ?sl = "rseq_to_ddseq (?u⇩1, sl)"
let ?cl⇩2 = "eseq_to_ddconv (?u⇩2, cl⇩2)"
let ?cr⇩1 = "eseq_to_ddconv (snd cp, cr⇩1)"
let ?sr = "rseq_to_ddseq (?v⇩1, sr)"
let ?cr⇩2 = "eseq_to_ddconv (?v⇩2, cr⇩2)"
from assms have
cl1: "isOK (check_conversion' R cl⇩1 (fst cp) ?u⇩1)" and
sl: "isOK (check_rsteps' R sl ?u⇩1 ?u⇩2)" and
cl2: "isOK (check_conversion' R cl⇩2 ?u⇩2 ?u⇩3)" and
cr1: "isOK (check_conversion' R cr⇩1 (snd cp) ?v⇩1)" and
sr: "isOK (check_rsteps' R sr ?v⇩1 ?v⇩2)" and
cr2: "isOK (check_conversion' R cr⇩2 ?v⇩2 ?v⇩3)" and
eq: "?u⇩3 = ?v⇩3" and inst: "cpeak_instance s cp s1 (t1, t2)"
by (auto simp add: Let_def check_cpeak_eldc_def)
from inst obtain ρ where "match_list (λ_. s) [(s, s1), (fst cp, t1), (snd cp, t2)] = Some ρ"
unfolding cpeak_instance_def by auto
from match_list_sound[OF this] have ρ: "t1 = fst cp ⋅ ρ ∧ t2 = snd cp ⋅ ρ ∧ s1 = s ⋅ ρ"
unfolding matchers_def by auto
let ?s = "λs. seq_close s □ ρ"
let ?c = "λc. conv_close c □ ρ"
have "ldc_trs (set R) ?p (?c ?cl⇩1) (?s ?sl) (?c ?cl⇩2) (?c ?cr⇩1) (?s ?sr) (?c ?cr⇩2)"
unfolding ldc_trs_def
proof (intro conjI)
from assms(2) critical_peak_is_local_peak show lp:"?p ∈ local_peaks (set R)" by fast
from check_conversion_sound_dd_conv[OF cl1] have "?cl⇩1 ∈ conv (set R)" and "DD2_last ?cl⇩1 = ?u⇩1" by auto
with conv_super_closed1[OF this(1), of □ ρ] show "(?c ?cl⇩1) ∈ conv (set R)" and "DD2_last (?c ?cl⇩1) = first (?s ?sl)" by auto
from check_rsteps'_sound_dd_seq[OF sl] have "?sl ∈ seq (set R)" and "DD2_last ?sl = ?u⇩2" by auto
with seq_super_closed1[OF this(1), of □ ρ] show "(?s ?sl) ∈ seq (set R)" and "DD2_last (?s ?sl) = first (?c ?cl⇩2)" by auto
from check_conversion_sound_dd_conv[OF cl2] have "?cl⇩2 ∈ conv (set R)" and "DD2_last ?cl⇩2 = ?u⇩3" by auto
with conv_super_closed1[OF this(1), of □ ρ] have "(?c ?cl⇩2) ∈ conv (set R)" and u3:"DD2_last (?c ?cl⇩2) = ?u⇩3 ⋅ ρ" by auto
from check_conversion_sound_dd_conv[OF cr1] have "?cr⇩1 ∈ conv (set R)" and "DD2_last ?cr⇩1 = ?v⇩1" by auto
with conv_super_closed1[OF this(1), of □ ρ] show "(?c ?cr⇩1) ∈ conv (set R)" and "DD2_last (?c ?cr⇩1) = first (?s ?sr)" by auto
from check_rsteps'_sound_dd_seq[OF sr] have "?sr ∈ seq (set R)" and "DD2_last ?sr = ?v⇩2" by auto
with seq_super_closed1[OF this(1), of □ ρ] show "(?s ?sr) ∈ seq (set R)" and "DD2_last (?s ?sr) = first (?c ?cr⇩2)" by auto
from check_conversion_sound_dd_conv[OF cr2] have "?cr⇩2 ∈ conv (set R)" and v3:"DD2_last ?cr⇩2 = ?v⇩3" by auto
with conv_super_closed1[OF this(1), of □ ρ] have "(?c ?cr⇩2) ∈ conv (set R)" and v3:"DD2_last (?c ?cr⇩2) = ?v⇩3 ⋅ ρ" by auto
show "get_target (fst ?p) = first (?c ?cl⇩1)" unfolding get_target_def using ρ by auto
show "get_target (snd ?p) = first (?c ?cr⇩1)" unfolding get_target_def using ρ by auto
from u3 v3 eq show "DD2_last (?c ?cl⇩2) = DD2_last (?c ?cr⇩2)" by auto
show "(?c ?cl⇩2) ∈ conv (set R)" and "(?c ?cr⇩2) ∈ conv (set R)" by fact+
qed
moreover have "eld_conv ?l r ?p (?c ?cl⇩1) (?s ?sl) (?c ?cl⇩2) (?c ?cr⇩1) (?s ?sr) (?c ?cr⇩2)"
proof -
from assms[unfolded check_cpeak_eldc_def Let_def]
have "ELD_1 r (?l (fst ?p)) (?l (snd ?p)) (map ?l (snd ?cl⇩1)) (map ?l (snd ?sl)) (map ?l (snd ?cl⇩2))"
and "ELD_1 r (?l (snd ?p)) (?l (fst ?p)) (map ?l (snd ?cr⇩1)) (map ?l (snd ?sr)) (map ?l (snd ?cr⇩2))"
using check_ELD_1_nat by auto
moreover have "map ?l (snd ?cl⇩1) = map ?l (snd (?c ?cl⇩1))" and
"map ?l (snd ?sl) = map ?l (snd (?s ?sl))" and
"map ?l (snd ?cl⇩2) = map ?l (snd (?c ?cl⇩2))" and
"map ?l (snd ?cr⇩1) = map ?l (snd (?c ?cr⇩1))" and
"map ?l (snd ?sr) = map ?l (snd (?s ?sr))" and
"map ?l (snd ?cr⇩2) = map ?l (snd (?c ?cr⇩2))"by auto
ultimately show ?thesis unfolding eld_conv_def by metis
qed
moreover have "fan (set R) ?p (?c ?cl⇩1) (?s ?sl) (?c ?cl⇩2) (?c ?cr⇩1) (?s ?sr) (?c ?cr⇩2) ∨ linear_trs (set R)"
proof (cases n)
case (Some n)
show ?thesis unfolding fan_def
proof (intro disjI1 conjI allI impI)
fix i assume i:"i < length (snd (?c ?cl⇩1))"
then have i2:"i < length (snd ?cl⇩1)" by auto
then have "snd ?cl⇩1 ! i ∈ set (snd ?cl⇩1)" using nth_mem by auto
with assms[unfolded Let_def check_cpeak_eldc_def] Some
have "List.member (reachable_terms R s n) (get_source (snd ?cl⇩1 ! i))" by auto
then have "(s, get_source (snd ?cl⇩1 ! i)) ∈ (rstep (set R))⇧*"
using reachable_terms in_set_member by metis
then show "(get_source (fst ?p), get_source (snd (?c ?cl⇩1) ! i)) ∈ (rstep (set R))⇧*"
using get_source_closed[OF i2, of □ ρ] ρ
by (auto intro: rsteps_closed_subst simp: get_source_def)
next
fix i assume i:"i < length (snd (?c ?cl⇩2))"
then have i2:"i < length (snd ?cl⇩2)" by auto
then have "snd ?cl⇩2 ! i ∈ set (snd ?cl⇩2)" using nth_mem by auto
with assms[unfolded Let_def check_cpeak_eldc_def] Some
have "List.member (reachable_terms R s n) (get_source (snd ?cl⇩2 ! i))" by auto
then have "(s, get_source (snd ?cl⇩2 ! i)) ∈ (rstep (set R))⇧*"
using reachable_terms in_set_member by metis
then show "(get_source (fst ?p), get_source (snd (?c ?cl⇩2) ! i)) ∈ (rstep (set R))⇧*"
using get_source_closed[OF i2, of □ ρ] ρ
by (auto intro: rsteps_closed_subst simp: get_source_def)
next
fix i assume i:"i < length (snd (?c ?cr⇩1))"
then have i2:"i < length (snd ?cr⇩1)" by auto
then have "snd ?cr⇩1 ! i ∈ set (snd ?cr⇩1)" using nth_mem by auto
with assms[unfolded Let_def check_cpeak_eldc_def] Some
have "List.member (reachable_terms R s n) (get_source (snd ?cr⇩1 ! i))" by auto
then have "(s, get_source (snd ?cr⇩1 ! i)) ∈ (rstep (set R))⇧*"
using reachable_terms in_set_member by metis
then show "(get_source (fst ?p), get_source (snd (?c ?cr⇩1) ! i)) ∈ (rstep (set R))⇧*"
using get_source_closed[OF i2, of □ ρ] ρ
by (auto intro: rsteps_closed_subst simp: get_source_def)
next
fix i assume i:"i < length (snd (?c ?cr⇩2))"
then have i2:"i < length (snd ?cr⇩2)" by auto
then have "snd ?cr⇩2 ! i ∈ set (snd ?cr⇩2)" using nth_mem by auto
with assms[unfolded Let_def check_cpeak_eldc_def] Some
have "List.member (reachable_terms R s n) (get_source (snd ?cr⇩2 ! i))" by auto
then have "(s, get_source (snd ?cr⇩2 ! i)) ∈ (rstep (set R))⇧*"
using reachable_terms in_set_member by metis
then show "(get_source (fst ?p), get_source (snd (?c ?cr⇩2) ! i)) ∈ (rstep (set R))⇧*"
using get_source_closed[OF i2, of □ ρ] ρ
by (auto intro: rsteps_closed_subst simp: get_source_def)
next
fix i assume i:"i < length (snd (?s ?sl))"
then have i2:"i < length (snd ?sl)" by auto
then have "snd ?sl ! i ∈ set (snd ?sl)" using nth_mem by auto
with assms[unfolded Let_def check_cpeak_eldc_def] Some
have "List.member (reachable_terms R s n) (get_source (snd ?sl ! i))" by auto
then have "(s, get_source (snd ?sl ! i)) ∈ (rstep (set R))⇧*"
using reachable_terms in_set_member by metis
then show "(get_source (fst ?p), get_source (snd (?s ?sl) ! i)) ∈ (rstep (set R))⇧*"
using get_source_closed[OF i2, of □ ρ] ρ
by (auto intro: rsteps_closed_subst simp: get_source_def)
next
fix i assume i:"i < length (snd (?s ?sr))"
then have i2:"i < length (snd ?sr)" by auto
then have "snd ?sr ! i ∈ set (snd ?sr)" using nth_mem by auto
with assms[unfolded Let_def check_cpeak_eldc_def] Some
have "List.member (reachable_terms R s n) (get_source (snd ?sr ! i))" by auto
then have "(s, get_source (snd ?sr ! i)) ∈ (rstep (set R))⇧*"
using reachable_terms in_set_member by metis
then show "(get_source (fst ?p), get_source (snd (?s ?sr) ! i)) ∈ (rstep (set R))⇧*"
using get_source_closed[OF i2, of □ ρ] ρ
by (auto intro: rsteps_closed_subst simp: get_source_def)
qed
next
case None
with assms show ?thesis unfolding check_cpeak_eldc_def by auto
qed
ultimately show ?thesis unfolding eld_fan_def eldc_def by fast
qed
lemma linear_imp_SN_rel_d_nd:
assumes "linear_trs R"
shows "SN_rel (rstep (R_d R)) (rstep (R_nd R))"
proof -
from assms have "R_d R = {}" unfolding R_d_def linear_trs_def by auto
thus ?thesis using SN_rel_empty1 by auto
qed
definition check_rule_labeling_eld ::
"('f :: {key, show}, string) rules ⇒ ('f :: {key, show}, string) rule_lab_repr ⇒
('f :: {key, show},string) crit_pair_joins ⇒ shows check"
where
"check_rule_labeling_eld R lab js = do {
let cps = critical_peaks_impl R R;
let l = rule_lab_repr_to_lab lab;
let joins = js @ (map (λ (u, j1, v, j2). (v, j2, u ,j1)) js);
check_allm (λ(b, (s1,r1,p1,σ1,True,t1),(s2,r2,p2,σ2,True,t2)).
try check (t1 = t2) (shows '' pair non-trivial '') catch
(λe. check_exm (λ(u, j1, v, j2).
(check_cpeak_eld R ((s1,r1,p1,σ1,True,t1),(s2,r2,p2,σ2,True,t2)) (u, v) j1 j2 l))
joins (λes. shows_nl +@+ shows ''the critical peak '' +@+ shows_rule' shows shows '' <- . -> '' (t1, t2)
+@+ shows '' could not be joined decreasingly:'' +@+ shows_nl +@+ shows_sep id id es)))
cps
}"
lemma check_rule_labeling_eld:
assumes "isOK (check_rule_labeling_eld R lab js)"
and "SN_rel (rstep (R_d (set R))) (rstep (R_nd (set R)))"
and "left_linear_trs (set R)"
shows "CR (rstep (set R))"
using assms (3,2)
proof (rule rule_labeling_is_sound_ll)
note ok = assms(1)[unfolded check_rule_labeling_eld_def, simplified]
let ?l = "rule_lab_repr_to_lab lab"
let ?rl = "rule_labeling ?l"
let ?joins = "js @ (map (λ (u, j1, v, j2). (v, j2, u ,j1)) js)"
def r ≡ "({(n, m). n < (m :: nat)}, {(n, m). n ≤ (m :: nat)})"
show "∀(b, p) ∈ critical_peaks (set R). eld (set R) ?rl r p"
proof
fix b p
assume p:"(b, p) ∈ critical_peaks (set R)"
hence pi:"(b, p) ∈ set (critical_peaks_impl R R)" using critical_peaks_impl by auto
then obtain s1 r1 p1 σ1 t1 s2 r2 p2 σ2 t2 where
fields: "p = ((s1,r1,p1,σ1,True,t1),(s2,r2,p2,σ2,True,t2))"
by (cases p, auto simp: critical_peaks_impl critical_peaks_def)
from bspec[OF ok pi]
have "(t1 = t2) ∨ (isOK (existsM (λ(u, j1, v, j2). check_cpeak_eld R p (u, v) j1 j2 ?l) ?joins))"
unfolding fields by simp
thus "eld (set R) ?rl r p"
proof
assume "t1 = t2"
moreover have "p ∈ local_peaks (set R)" using critical_peak_is_local_peak fields p by fast
ultimately show ?thesis using trivial_peak_eld unfolding fields by fast
next
assume "isOK (existsM (λ(u, j1, v, j2). check_cpeak_eld R p (u, v) j1 j2 ?l) ?joins)"
then obtain u j1 v j2 where "isOK(check_cpeak_eld R p (u, v) j1 j2 ?l)"
unfolding isOK_existsM by (split prod.splits, force)
thus ?thesis using check_cpeak_eld p unfolding r_def fields by fast
qed
qed
qed
type_synonym ('f,'v) crit_peak_convs = "(('f,'v) term ×
('f,'v) term × ('f, 'v) eseq × ('f, 'v) rseq × ('f, 'v) eseq ×
('f,'v) term × ('f, 'v) eseq × ('f, 'v) rseq × ('f, 'v) eseq) list"
definition check_rule_labeling_eldc ::
"('f :: {key, show}, string) rules ⇒ ('f :: {key, show}, string) rule_lab_repr ⇒
('f :: {key, show},string) crit_peak_convs ⇒ nat option ⇒ shows check"
where
"check_rule_labeling_eldc R lab cs n = do {
let cps = critical_peaks_impl R R;
let l = rule_lab_repr_to_lab lab;
let convs = cs @ (map (λ (s, u, cl⇩1, sl, cl⇩2, v, cr⇩1, sr, cr⇩2). (s, v, cr⇩1, sr, cr⇩2, u ,cl⇩1, sl, cl⇩2)) cs);
check_allm (λ(b, (s1, r1, p1, σ1, True, t1),(s2, r2, p2, σ2, True, t2)).
try check (t1 = t2) (shows '' pair non-trivial '') catch
(λe. check_exm (λ(s, u, cl⇩1, sl, cl⇩2, v, cr⇩1, sr, cr⇩2).
(check_cpeak_eldc R ((s1, r1, p1, σ1, True, t1),(s2, r2, p2, σ2, True, t2)) s (u, v) cl⇩1 sl cl⇩2 cr⇩1 sr cr⇩2 l n))
convs (λes. shows_nl +@+ shows ''the critical peak '' +@+
shows t1 +@+ shows '' <- '' +@+ shows s1 +@+ shows '' -> '' +@+ shows t2 +@+
shows '' could not be joined decreasingly:'' +@+ shows_nl +@+ shows_sep id id es)))
cps
}"
lemma check_rule_labeling_eldc:
assumes "isOK (check_rule_labeling_eldc R lab cs n)"
and "SN_rel (rstep (R_d (set R))) (rstep (R_nd (set R)))"
and "left_linear_trs (set R)"
and "n = None ⟶ linear_trs (set R)"
shows "CR (rstep (set R))"
proof -
note ok = assms(1)[unfolded check_rule_labeling_eldc_def, simplified]
let ?l = "rule_lab_repr_to_lab lab"
let ?rl = "rule_labeling ?l"
let ?convs = "cs @ (map (λ (s, u, cl⇩1, sl, cl⇩2, v, cr⇩1, sr, cr⇩2). (s, v, cr⇩1, sr, cr⇩2, u ,cl⇩1, sl, cl⇩2)) cs)"
def r ≡ "({(n, m). n < (m :: nat)}, {(n, m). n ≤ (m :: nat)})"
{ fix b p
assume p:"(b, p) ∈ critical_peaks (set R)"
hence pi:"(b, p) ∈ set (critical_peaks_impl R R)" using critical_peaks_impl by auto
then obtain s r1 p1 σ1 t1 r2 p2 σ2 t2 where fields: "p = ((s,r1,p1,σ1,True,t1),(s,r2,p2,σ2,True,t2))"
by (cases p, auto simp: critical_peaks_impl critical_peaks_def)
from bspec[OF ok pi]
consider (trivial) "(t1 = t2)" | (ok) "isOK (existsM (λ(s, u, cl⇩1, sl, cl⇩2, v, cr⇩1, sr, cr⇩2).
check_cpeak_eldc R p s (u, v) cl⇩1 sl cl⇩2 cr⇩1 sr cr⇩2 ?l n) ?convs)"
unfolding fields by fastforce
then have "eld_fan (set R) ?rl r p ∨ eldc (set R) ?rl r p ∧ linear_trs (set R)"
proof (cases)
case (trivial)
moreover have "p ∈ local_peaks (set R)" using critical_peak_is_local_peak fields p by fast
ultimately show ?thesis using trivial_peak_eld_fan unfolding fields by fast
next
case (ok)
then obtain s' u cl⇩1 sl cl⇩2 v cr⇩1 sr cr⇩2 where "isOK(check_cpeak_eldc R p s' (u, v) cl⇩1 sl cl⇩2 cr⇩1 sr cr⇩2 ?l n)"
unfolding isOK_existsM by (split prod.splits, force)
from check_cpeak_eldc[OF p[unfolded fields] this[unfolded fields]] assms(4) show ?thesis
unfolding r_def fields by auto
qed
}
then consider (fan) "(∀(b, p) ∈ critical_peaks (set R). eld_fan (set R) ?rl r p)"
| (linear) "(∀(b, p) ∈ critical_peaks (set R). eldc (set R) ?rl r p) ∧ linear_trs (set R)"
unfolding eld_fan_def eldc_def by blast
then show ?thesis
proof (cases)
case fan
then show ?thesis using rule_labeling_conv_is_sound_ll[OF assms(3,2)] unfolding r_def by auto
next
case linear
then show ?thesis using rule_labeling_is_sound unfolding r_def by auto
qed
qed
end