Theory Main_Result_DCR_N1
subsection ‹DCR implies LD Property›
theory Main_Result_DCR_N1
imports
DCR3_Method
"Decreasing-Diagrams.Decreasing_Diagrams"
begin
subsubsection ‹Auxiliary definitions›
definition map_seq_labels :: "('b ⇒ 'c) ⇒ ('a,'b) seq ⇒ ('a,'c) seq"
where
"map_seq_labels f σ = (fst σ, map (λ(α,a). (f α, a)) (snd σ))"
fun map_diag_labels :: "('b ⇒ 'c) ⇒
('a,'b) seq × ('a,'b) seq × ('a,'b) seq × ('a,'b) seq ⇒
('a,'c) seq × ('a,'c) seq × ('a,'c) seq × ('a,'c) seq"
where
"map_diag_labels f (τ,σ,σ',τ') = ((map_seq_labels f τ), (map_seq_labels f σ), (map_seq_labels f σ'), (map_seq_labels f τ'))"
fun f_to_ls :: "(nat ⇒ 'a) ⇒ nat ⇒ 'a list"
where
"f_to_ls f 0 = []"
| "f_to_ls f (Suc n) = (f_to_ls f n) @ [(f n)]"
subsubsection ‹Auxiliary lemmas›
lemma lem_ftofs_len: "length (f_to_ls f n) = n" by (induct n, simp+)
lemma lem_irr_inj_im_irr:
fixes r::"'a rel" and r'::"'b rel" and f::"'a ⇒ 'b"
assumes "irrefl r" and "inj_on f (Field r)"
and "r' = {(a',b'). ∃ a b. a' = f a ∧ b' = f b ∧ (a,b) ∈ r}"
shows "irrefl r'"
using assms unfolding inj_on_def Field_def irrefl_def by blast
lemma lem_tr_inj_im_tr:
fixes r::"'a rel" and r'::"'b rel" and f::"'a ⇒ 'b"
assumes "trans r" and "inj_on f (Field r)"
and "r' = {(a',b'). ∃ a b. a' = f a ∧ b' = f b ∧ (a,b) ∈ r}"
shows "trans r'"
using assms unfolding inj_on_def Field_def trans_def by blast
lemma lem_lpeak_expr: "local_peak lrs (τ, σ) = (∃ a b c α β. (a,α,b) ∈ lrs ∧ (a,β,c) ∈ lrs ∧ τ = (a,[(α,b)]) ∧ σ = (a,[(β,c)]))"
proof
assume "local_peak lrs (τ, σ)"
then show "∃ a b c α β. (a,α,b) ∈ lrs ∧ (a,β,c) ∈ lrs ∧ τ = (a,[(α,b)]) ∧ σ = (a,[(β,c)])"
unfolding Decreasing_Diagrams.local_peak_def Decreasing_Diagrams.peak_def
apply(cases τ, cases σ, simp)
using Decreasing_Diagrams.seq_tail1(2)
by (metis (no_types, lifting) Suc_length_conv length_0_conv prod.collapse)
next
assume "∃ a b c α β. (a,α,b) ∈ lrs ∧ (a,β,c) ∈ lrs ∧ τ = (a,[(α,b)]) ∧ σ = (a,[(β,c)])"
then obtain a b c α β where "(a,α,b) ∈ lrs ∧ (a,β,c) ∈ lrs ∧ τ = (a,[(α,b)]) ∧ σ = (a,[(β,c)])" by blast
then show "local_peak lrs (τ, σ)"
unfolding Decreasing_Diagrams.local_peak_def Decreasing_Diagrams.peak_def
by (simp add: Decreasing_Diagrams.seq.intros)
qed
lemma lem_map_seq:
fixes lrs::"('a,'b) lars" and f::"'b ⇒ 'c" and lrs'::"('a,'c) lars" and σ::"('a,'b) seq"
assumes a1: "lrs' = {(a,l',b). ∃l. l' = f l ∧ (a,l,b) ∈ lrs }"
and a2: "σ ∈ Decreasing_Diagrams.seq lrs"
shows "(map_seq_labels f σ) ∈ Decreasing_Diagrams.seq lrs'"
proof -
have "∀ s a. (a,s) ∈ Decreasing_Diagrams.seq lrs ⟶ (map_seq_labels f (a,s)) ∈ Decreasing_Diagrams.seq lrs'"
proof
fix s
show "∀ a. (a,s) ∈ Decreasing_Diagrams.seq lrs ⟶ (map_seq_labels f (a,s)) ∈ Decreasing_Diagrams.seq lrs'"
proof (induct s)
show "∀a. (a, []) ∈ Decreasing_Diagrams.seq lrs ⟶ map_seq_labels f (a, []) ∈ Decreasing_Diagrams.seq lrs'"
unfolding map_seq_labels_def by (simp add: seq.intros(1))
next
fix p s1
assume d1: "∀b. (b, s1) ∈ Decreasing_Diagrams.seq lrs ⟶ map_seq_labels f (b, s1) ∈ Decreasing_Diagrams.seq lrs'"
show "∀b. (b, p # s1) ∈ Decreasing_Diagrams.seq lrs ⟶ map_seq_labels f (b, p # s1) ∈ Decreasing_Diagrams.seq lrs'"
proof (intro allI impI)
fix b
assume e1: "(b, p # s1) ∈ Decreasing_Diagrams.seq lrs"
moreover obtain l b' where e2: "p = (l, b')" by force
ultimately have e3: "(b,l,b') ∈ lrs ∧ (b',s1) ∈ Decreasing_Diagrams.seq lrs"
by (metis Decreasing_Diagrams.seq_tail1(1) Decreasing_Diagrams.seq_tail1(2) prod.collapse snd_conv)
then have "(b,f l,b') ∈ lrs'" using a1 by blast
moreover have "map_seq_labels f (b', s1) ∈ Decreasing_Diagrams.seq lrs'" using d1 e3 by blast
ultimately show "map_seq_labels f (b, p # s1) ∈ Decreasing_Diagrams.seq lrs'"
using e2 unfolding map_seq_labels_def by (simp add: seq.intros(2))
qed
qed
qed
moreover obtain a s where "σ = (a,s)" by force
ultimately show "(map_seq_labels f σ) ∈ Decreasing_Diagrams.seq lrs'" using a2 by blast
qed
lemma lem_map_diag:
fixes lrs::"('a,'b) lars" and f::"'b ⇒ 'c" and lrs'::"('a,'c) lars"
and d::"('a,'b) seq × ('a,'b) seq × ('a,'b) seq × ('a,'b) seq"
assumes a1: "lrs' = {(a,l',b). ∃l. l' = f l ∧ (a,l,b) ∈ lrs }"
and a2: "diagram lrs d"
shows "diagram lrs' (map_diag_labels f d)"
proof -
obtain τ σ σ' τ' where b1: "d = (τ, σ, σ', τ')" using prod_cases4 by blast
moreover obtain τ1 σ1 σ1' τ1' where b2: "τ1 = (map_seq_labels f τ) ∧ σ1 = (map_seq_labels f σ)
∧ (σ1' = map_seq_labels f σ') ∧ (τ1' = map_seq_labels f τ')" by blast
ultimately have b3: "(map_diag_labels f d) = (τ1, σ1, σ1', τ1')" by simp
have b4: "fst σ = fst τ ∧ lst σ = fst τ' ∧ lst τ = fst σ' ∧ lst σ' = lst τ'"
using b1 a2 unfolding Decreasing_Diagrams.diagram_def by simp
have b5: "σ1 ∈ Decreasing_Diagrams.seq lrs' ∧ τ1 ∈ Decreasing_Diagrams.seq lrs'
∧ σ1' ∈ Decreasing_Diagrams.seq lrs' ∧ τ1' ∈ Decreasing_Diagrams.seq lrs'"
using a1 a2 b1 b2 lem_map_seq[of lrs' f] by (simp add: Decreasing_Diagrams.diagram_def)
moreover have "fst σ1 = fst τ1" using b2 b4 unfolding map_seq_labels_def by simp
moreover have "lst σ1 = fst τ1' ∧ lst τ1 = fst σ1'" using b4
by (simp add: b2 map_seq_labels_def lst_def, metis (no_types, lifting) case_prod_beta last_map snd_conv)
moreover have "lst σ1' = lst τ1'" using b4
by (simp add: b2 map_seq_labels_def lst_def, metis (no_types, lifting) case_prod_beta last_map snd_conv)
ultimately show "diagram lrs' (map_diag_labels f d)" using b3 b5 unfolding Decreasing_Diagrams.diagram_def by simp
qed
lemma lem_map_D_loc:
fixes cmp cmp' s1 s2 s3 s4 f
assumes a1: "Decreasing_Diagrams.D cmp s1 s2 s3 s4"
and a2: "trans cmp" and a3: "irrefl cmp" and a4: "inj_on f (Field cmp)"
and a5: "cmp' = {(a',b'). ∃ a b. a' = f a ∧ b' = f b ∧ (a,b) ∈ cmp}"
and a6: "length s1 = 1" and a7: "length s2 = 1"
shows "Decreasing_Diagrams.D cmp' (map f s1) (map f s2) (map f s3) (map f s4)"
proof -
obtain α where b1: "s2 = [α]" using a7 by (metis One_nat_def Suc_length_conv length_0_conv)
moreover obtain β where b2: "s1 = [β]" using a6 by (metis One_nat_def Suc_length_conv length_0_conv)
ultimately have b3: "Decreasing_Diagrams.D cmp [β] [α] s3 s4" using a1 by blast
then obtain σ1 σ2 σ3 τ1 τ2 τ3 where b4: "s3 = σ1@σ2@σ3" and b5: "s4 = τ1@τ2@τ3" and b6: "LD' cmp β α σ1 σ2 σ3 τ1 τ2 τ3"
using Decreasing_Diagrams.proposition3_4_inv[of cmp β α s3 s4] a2 a3 by blast
obtain σ1' σ2' σ3' where b7: "σ1' = map f σ1 ∧ σ2' = map f σ2 ∧ σ3' = map f σ3" by blast
obtain τ1' τ2' τ3' where b8: "τ1' = map f τ1 ∧ τ2' = map f τ2 ∧ τ3' = map f τ3" by blast
obtain s3' s4' where b9: "s3' = map f s3" and b10: "s4' = map f s4" by blast
have "trans cmp'" using a2 a4 a5 lem_tr_inj_im_tr by blast
moreover have "irrefl cmp'" using a3 a4 a5 lem_irr_inj_im_irr by blast
moreover have "s3' = σ1'@σ2'@σ3'" using b4 b7 b9 by simp
moreover have "s4' = τ1'@τ2'@τ3'" using b5 b8 b10 by simp
moreover have "LD' cmp' (f β) (f α) σ1' σ2' σ3' τ1' τ2' τ3'"
proof -
have c1: "LD_1' cmp β α σ1 σ2 σ3" and c2: "LD_1' cmp α β τ1 τ2 τ3"
using b6 unfolding Decreasing_Diagrams.LD'_def by blast+
have "LD_1' cmp' (f β) (f α) σ1' σ2' σ3'"
using c1 unfolding Decreasing_Diagrams.LD_1'_def Decreasing_Diagrams.ds_def by (simp add: a5 b7, blast)
moreover have "LD_1' cmp' (f α) (f β) τ1' τ2' τ3'"
using c2 unfolding Decreasing_Diagrams.LD_1'_def Decreasing_Diagrams.ds_def by (simp add: a5 b8, blast)
ultimately show "LD' cmp' (f β) (f α) σ1' σ2' σ3' τ1' τ2' τ3'" unfolding Decreasing_Diagrams.LD'_def by blast
qed
ultimately have "Decreasing_Diagrams.D cmp' [f β] [f α] s3' s4'" using Decreasing_Diagrams.proposition3_4[of cmp'] by blast
moreover have "(map f s1) = [f β] ∧ (map f s2) = [f α]" using b1 b2 by simp
ultimately show "Decreasing_Diagrams.D cmp' (map f s1) (map f s2) (map f s3) (map f s4)" using b9 b10 by simp
qed
lemma lem_map_DD_loc:
fixes lrs::"('a,'b) lars" and cmp::"'b rel" and lrs'::"('a,'c) lars" and cmp'::"'c rel" and f::"'b ⇒ 'c"
assumes a1: "trans cmp" and a2: "irrefl cmp" and a3: "inj_on f (Field cmp)"
and a4: "cmp' = {(a',b'). ∃ a b. a' = f a ∧ b' = f b ∧ (a,b) ∈ cmp}"
and a5: "lrs' = {(a,l',b). ∃l. l' = f l ∧ (a,l,b) ∈ lrs }"
and a6: "length (snd (fst d)) = 1" and a7: "length (snd (fst (snd d))) = 1"
and a8: "DD lrs cmp d"
shows "DD lrs' cmp' (map_diag_labels f d)"
proof -
have "diagram lrs' (map_diag_labels f d)" using a4 a5 a8 lem_map_diag unfolding Decreasing_Diagrams.DD_def by blast
moreover have "D2 cmp' (map_diag_labels f d)"
proof -
obtain τ σ σ' τ' where c1: "d = (τ,σ,σ',τ')" by (metis prod_cases3)
obtain s1 s2 s3 s4 where c2: "s1 = labels τ ∧ s2 = labels σ ∧ s3 = labels σ' ∧ s4 = labels τ'" by blast
have "Decreasing_Diagrams.D cmp s1 s2 s3 s4"
using a8 c1 c2 unfolding Decreasing_Diagrams.DD_def Decreasing_Diagrams.D2_def by simp
moreover have "length s1 = 1 ∧ length s2 = 1" using a6 a7 c1 c2 unfolding labels_def by simp
ultimately have "Decreasing_Diagrams.D cmp' (map f s1) (map f s2) (map f s3) (map f s4)"
using a1 a2 a3 a4 lem_map_D_loc by blast
moreover have "labels (map_seq_labels f τ) = (map f s1)"
and "labels (map_seq_labels f σ) = (map f s2)"
and "labels (map_seq_labels f σ') = (map f s3)"
and "labels (map_seq_labels f τ') = (map f s4)"
using c2 unfolding map_seq_labels_def Decreasing_Diagrams.labels_def by force+
ultimately have "D2 cmp' ((map_seq_labels f τ), (map_seq_labels f σ), (map_seq_labels f σ'), (map_seq_labels f τ'))"
unfolding Decreasing_Diagrams.D2_def by simp
then show "D2 cmp' (map_diag_labels f d)" using c1 unfolding Decreasing_Diagrams.D2_def by simp
qed
ultimately show "DD lrs' cmp' (map_diag_labels f d)" unfolding Decreasing_Diagrams.DD_def by blast
qed
lemma lem_ddseq_mon: "lrs1 ⊆ lrs2 ⟹ Decreasing_Diagrams.seq lrs1 ⊆ Decreasing_Diagrams.seq lrs2"
proof -
assume a1: "lrs1 ⊆ lrs2"
show "Decreasing_Diagrams.seq lrs1 ⊆ Decreasing_Diagrams.seq lrs2"
proof
fix a s
assume b1: "(a,s) ∈ Decreasing_Diagrams.seq lrs1"
show "(a,s) ∈ Decreasing_Diagrams.seq lrs2"
by (rule Decreasing_Diagrams.seq.induct[of _ _ lrs1],
simp only: b1, simp only: seq.intros(1), meson a1 contra_subsetD seq.intros(2))
qed
qed
lemma lem_dd_D_mon:
fixes cmp1 cmp2 α β s1 s2
assumes a1: "trans cmp1 ∧ irrefl cmp1" and a2: "trans cmp2 ∧ irrefl cmp2" and a3: "cmp1 ⊆ cmp2"
and a4: "Decreasing_Diagrams.D cmp1 [α] [β] s1 s2"
shows "Decreasing_Diagrams.D cmp2 [α] [β] s1 s2"
proof -
obtain σ1 σ2 σ3 τ1 τ2 τ3
where b1: "s1 = σ1@σ2@σ3 ∧ s2 = τ1@τ2@τ3" and b2: "LD' cmp1 α β σ1 σ2 σ3 τ1 τ2 τ3"
using a1 a4 Decreasing_Diagrams.proposition3_4_inv[of "cmp1" α β s1 s2] by blast
then have b3: "LD_1' cmp1 α β σ1 σ2 σ3" and b4: "LD_1' cmp1 β α τ1 τ2 τ3"
unfolding Decreasing_Diagrams.LD'_def by blast+
have "LD_1' cmp2 α β σ1 σ2 σ3"
using a3 b3 unfolding Decreasing_Diagrams.LD_1'_def Decreasing_Diagrams.ds_def by blast
moreover have "LD_1' cmp2 β α τ1 τ2 τ3"
using a3 b4 unfolding Decreasing_Diagrams.LD_1'_def Decreasing_Diagrams.ds_def by blast
ultimately show "Decreasing_Diagrams.D cmp2 [α] [β] s1 s2"
using Decreasing_Diagrams.proposition3_4[of cmp2 α β] by (simp add: a2 b1 LD'_def)
qed
subsubsection ‹Result›
text ‹The next lemma has the following meaning: every ARS in the finite DCR hierarchy has the LD property.›
lemma lem_dcr_to_ld:
fixes n::nat and r::"'U rel"
assumes "DCR n r"
shows "LD (UNIV::nat set) r"
proof -
obtain g::"nat ⇒ 'U rel" where
b1: "DCR_generating g" and b3: "r = ⋃ { r'. ∃ α'. α' < n ∧ r' = g α' }"
using assms unfolding DCR_def by blast
obtain lrs::"('U, nat) lars" where b4: "lrs = {(a,α',b). α' < n ∧ (a,b) ∈ g α'}" by blast
obtain cmp::"nat rel" where b5: "cmp = {(α, β). α < β }" by blast
have "r = unlabel lrs" using b3 b4 unfolding unlabel_def by blast
moreover have b6: "trans cmp" using b5 unfolding trans_def by force
moreover have b7: "wf cmp"
proof -
have "cmp = ({(x::nat, y::nat). x < y})"
unfolding b5 lex_prod_def by fastforce
moreover have "wf {(x::nat, y::nat). x < y}" using wf_less by blast
ultimately show ?thesis using wf_lex_prod by blast
qed
moreover have "∀P. local_peak lrs P ⟶ (∃ σ' τ'. DD lrs cmp (fst P,snd P,σ',τ'))"
proof (intro allI impI)
fix P
assume c1: "local_peak lrs P"
moreover obtain τ σ where c2: "P = (τ, σ)" using surjective_pairing by blast
ultimately obtain a b c α β
where c3: "(a,α,b) ∈ lrs ∧ (a,β,c) ∈ lrs"
and c4: "σ = (a,[(α,b)]) ∧ τ = (a,[(β,c)])" using lem_lpeak_expr[of lrs] by blast
then have c5: "α < n ∧ β < n" and c6: "(a,b) ∈ (g α) ∧ (a,c) ∈ (g β)" using b4 by blast+
obtain b' b'' c' c'' d where
c7: "(b,b') ∈ (𝔏1 g α)^* ∧ (b',b'') ∈ (g β)^= ∧ (b'',d) ∈ (𝔏v g α β)^*"
and c8: "(c,c') ∈ (𝔏1 g β)^* ∧ (c',c'') ∈ (g α)^= ∧ (c'',d) ∈ (𝔏v g β α)^*"
using b1 c6 unfolding DCR_generating_def 𝔇_def by (metis (no_types, lifting) mem_Collect_eq old.prod.case)
obtain pn1 where "(b,b') ∈ (𝔏1 g α)^^pn1" using c7 by fastforce
then obtain ph1 where pc9: "ph1 0 = b ∧ ph1 pn1 = b'" and "∀ i::nat. i < pn1 ⟶ (ph1 i, ph1 (Suc i)) ∈ (𝔏1 g α)"
using relpow_fun_conv by metis
then have "∀ i::nat. i<pn1 ⟶ (∃ α'. α' < α ∧ (ph1 i, ph1 (Suc i)) ∈ g α')" unfolding 𝔏1_def by blast
then obtain pαi1::"nat ⇒ nat"
where pc10: "∀ i::nat. i<pn1 ⟶ (pαi1 i) < α ∧ (ph1 i, ph1 (Suc i)) ∈ g (pαi1 i)" by metis
let ?pf1 = "λi. ( pαi1 i, ph1 (Suc i) )"
obtain pls1 where pc11: "pls1 = (f_to_ls ?pf1 pn1)" by blast
obtain n1 where "(b'',d) ∈ (𝔏v g α β)^^n1" using c7 by fastforce
then obtain h1 where c9: "h1 0 = b'' ∧ h1 n1 = d" and "∀ i::nat. i < n1 ⟶ (h1 i, h1 (Suc i)) ∈ (𝔏v g α β)"
using relpow_fun_conv by metis
then have "∀ i::nat. i < n1 ⟶ (∃ α'. (α' < α ∨ α' < β) ∧ (h1 i, h1 (Suc i)) ∈ g α')" unfolding 𝔏v_def by blast
then obtain αi1::"nat ⇒ nat"
where c10: "∀ i::nat. i<n1 ⟶ ((αi1 i) < α ∨ (αi1 i) < β) ∧ (h1 i, h1 (Suc i)) ∈ g (αi1 i)" by metis
let ?f1 = "λi. ( αi1 i, h1 (Suc i) )"
obtain ls1 where c11: "ls1 = (f_to_ls ?f1 n1)" by blast
obtain τ'' where qc12: "τ'' = (if b' = b'' then (b'', ls1) else (b', (β, b'') # ls1))" by blast
obtain τ' where c12: "τ' = (b, pls1 @ (snd τ''))" by blast
obtain pn2 where "(c,c') ∈ (𝔏1 g β)^^pn2" using c8 by fastforce
then obtain ph2 where pc13: "ph2 0 = c ∧ ph2 pn2 = c'" and "∀ i::nat. i < pn2 ⟶ (ph2 i, ph2 (Suc i)) ∈ (𝔏1 g β)"
using relpow_fun_conv by metis
then have "∀ i::nat. i<pn2 ⟶ (∃ α'. α' < β ∧ (ph2 i, ph2 (Suc i)) ∈ g α')" unfolding 𝔏1_def by blast
then obtain pαi2::"nat ⇒ nat"
where pc14: "∀ i::nat. i<pn2 ⟶ (pαi2 i) < β ∧ (ph2 i, ph2 (Suc i)) ∈ g (pαi2 i)" by metis
let ?pf2 = "λi. ( pαi2 i, ph2 (Suc i) )"
obtain pls2 where pc15: "pls2 = (f_to_ls ?pf2 pn2)" by blast
have "𝔏v g β α = 𝔏v g α β" unfolding 𝔏v_def by blast
then have "(c'',d) ∈ (𝔏v g α β)^*" using c8 by simp
then obtain n2 where "(c'',d) ∈ (𝔏v g α β)^^n2" using c8 by fastforce
then obtain h2 where c13: "h2 0 = c'' ∧ h2 n2 = d" and "∀ i::nat. i < n2 ⟶ (h2 i, h2 (Suc i)) ∈ (𝔏v g α β)"
using relpow_fun_conv by metis
then have "∀ i::nat. i<n2 ⟶ (∃ α'. (α' < α ∨ α' < β) ∧ (h2 i, h2 (Suc i)) ∈ g α')" unfolding 𝔏v_def by blast
then obtain αi2::"nat ⇒ nat"
where c14: "∀ i::nat. i<n2 ⟶ ((αi2 i) < α ∨ (αi2 i) < β) ∧ (h2 i, h2 (Suc i)) ∈ g (αi2 i)" by metis
let ?f2 = "λi. ( αi2 i, h2 (Suc i) )"
obtain ls2 where c15: "ls2 = (f_to_ls ?f2 n2)" by blast
obtain σ'' where qc16: "σ'' = (if c' = c'' then (c'', ls2) else (c', (α, c'') # ls2))" by blast
obtain σ' where c16: "σ' = (c, pls2 @ (snd σ''))" by blast
have "DD lrs cmp (τ, σ, σ', τ')"
proof -
have d1': "∀ k. k < pn1 ⟶ (ph1 k, pαi1 k, ph1 (Suc k)) ∈ lrs"
proof (intro allI impI)
fix k
assume "k < pn1"
moreover then have "(ph1 k, ph1 (Suc k)) ∈ g (pαi1 k) ∧ (pαi1 k < n)"
using c5 pc10 by force
ultimately show "(ph1 k, pαi1 k, ph1 (Suc k)) ∈ lrs" using b4 by blast
qed
have d1: "∀ k. k < n1 ⟶ (h1 k, αi1 k, h1 (Suc k)) ∈ lrs"
proof (intro allI impI)
fix k
assume "k < n1"
moreover then have "(h1 k, h1 (Suc k)) ∈ g (αi1 k) ∧ αi1 k < n"
using c5 c10 by force
ultimately show "(h1 k, αi1 k, h1 (Suc k)) ∈ lrs" using b4 by blast
qed
have d2': "∀ k. k < pn2 ⟶ (ph2 k, pαi2 k, ph2 (Suc k)) ∈ lrs"
proof (intro allI impI)
fix k
assume "k < pn2"
moreover then have "(ph2 k, ph2 (Suc k)) ∈ g (pαi2 k) ∧ pαi2 k < n"
using c5 pc14 by force
ultimately show "(ph2 k, pαi2 k, ph2 (Suc k)) ∈ lrs" using b4 by blast
qed
have d2: "∀ k. k < n2 ⟶ (h2 k, αi2 k, h2 (Suc k)) ∈ lrs"
proof (intro allI impI)
fix k
assume "k < n2"
moreover then have "(h2 k, h2 (Suc k)) ∈ g (αi2 k) ∧ αi2 k < n"
using c5 c14 by force
ultimately show "(h2 k, αi2 k, h2 (Suc k)) ∈ lrs" using b4 by blast
qed
have d3: "τ'' ∈ Decreasing_Diagrams.seq lrs"
proof -
have "∀ k. k ≤ n1 ⟶ (b'', (f_to_ls ?f1 k)) ∈ Decreasing_Diagrams.seq lrs"
proof
fix k0
show "k0 ≤ n1 ⟶ (b'', (f_to_ls ?f1 k0)) ∈ Decreasing_Diagrams.seq lrs"
proof (induct k0)
show "0 ≤ n1 ⟶ (b'', f_to_ls ?f1 0) ∈ Decreasing_Diagrams.seq lrs"
using Decreasing_Diagrams.seq.intros(1)[of _ lrs] by simp
next
fix k
assume g1: "k ≤ n1 ⟶ (b'', f_to_ls ?f1 k) ∈ Decreasing_Diagrams.seq lrs"
show "Suc k ≤ n1 ⟶ (b'', f_to_ls ?f1 (Suc k)) ∈ Decreasing_Diagrams.seq lrs"
proof
assume h1: "Suc k ≤ n1"
then have h2: "(b'', f_to_ls ?f1 k) ∈ Decreasing_Diagrams.seq lrs" using g1 by simp
obtain s where h3: "s = (h1 k, [(αi1 k, h1 (Suc k))])" by blast
then have "s ∈ Decreasing_Diagrams.seq lrs"
using h1 d1 Decreasing_Diagrams.seq.intros(2)[of "h1 k" "αi1 k"] Decreasing_Diagrams.seq.intros(1)[of _ lrs] by simp
moreover have "lst (b'', f_to_ls ?f1 k) = fst s"
using c9 h3 unfolding lst_def by (cases k, simp+)
ultimately show "(b'', f_to_ls ?f1 (Suc k)) ∈ Decreasing_Diagrams.seq lrs"
using h2 h3 Decreasing_Diagrams.seq_concat_helper[of b'' "f_to_ls ?f1 k" lrs s] by simp
qed
qed
qed
then have "(b'', ls1) ∈ Decreasing_Diagrams.seq lrs" using c11 by blast
moreover then have "b' ≠ b'' ⟶ (b', (β, b'') # ls1) ∈ Decreasing_Diagrams.seq lrs"
using b4 c5 c7 Decreasing_Diagrams.seq.intros(2)[of b' β b''] by fastforce
ultimately show "τ'' ∈ Decreasing_Diagrams.seq lrs" using qc12 by simp
qed
have d4: "σ'' ∈ Decreasing_Diagrams.seq lrs"
proof -
have "∀ k. k ≤ n2 ⟶ (c'', (f_to_ls ?f2 k)) ∈ Decreasing_Diagrams.seq lrs"
proof
fix k0
show "k0 ≤ n2 ⟶ (c'', (f_to_ls ?f2 k0)) ∈ Decreasing_Diagrams.seq lrs"
proof (induct k0)
show "0 ≤ n2 ⟶ (c'', f_to_ls ?f2 0) ∈ Decreasing_Diagrams.seq lrs"
using Decreasing_Diagrams.seq.intros(1)[of _ lrs] by simp
next
fix k
assume g1: "k ≤ n2 ⟶ (c'', f_to_ls ?f2 k) ∈ Decreasing_Diagrams.seq lrs"
show "Suc k ≤ n2 ⟶ (c'', f_to_ls ?f2 (Suc k)) ∈ Decreasing_Diagrams.seq lrs"
proof
assume h1: "Suc k ≤ n2"
then have h2: "(c'', f_to_ls ?f2 k) ∈ Decreasing_Diagrams.seq lrs" using g1 by simp
obtain s where h3: "s = (h2 k, [(αi2 k, h2 (Suc k))])" by blast
then have "s ∈ Decreasing_Diagrams.seq lrs"
using h1 d2 Decreasing_Diagrams.seq.intros(2)[of "h2 k" "αi2 k"] Decreasing_Diagrams.seq.intros(1)[of _ lrs] by simp
moreover have "lst (c'', f_to_ls ?f2 k) = fst s"
using c13 h3 unfolding lst_def by (cases k, simp+)
ultimately show "(c'', f_to_ls ?f2 (Suc k)) ∈ Decreasing_Diagrams.seq lrs"
using h2 h3 Decreasing_Diagrams.seq_concat_helper[of c'' "f_to_ls ?f2 k" lrs s] by simp
qed
qed
qed
then have "(c'', ls2) ∈ Decreasing_Diagrams.seq lrs" using c15 by blast
moreover then have "c' ≠ c'' ⟶ (c', (α, c'') # ls2) ∈ Decreasing_Diagrams.seq lrs"
using b4 c5 c8 Decreasing_Diagrams.seq.intros(2)[of c' α c''] by fastforce
ultimately show "σ'' ∈ Decreasing_Diagrams.seq lrs" using qc16 by simp
qed
have "σ ∈ Decreasing_Diagrams.seq lrs" by (simp add: c3 c4 seq.intros(1) seq.intros(2))
moreover have "τ ∈ Decreasing_Diagrams.seq lrs" by (simp add: c3 c4 seq.intros(1) seq.intros(2))
moreover have d5: "σ' ∈ Decreasing_Diagrams.seq lrs ∧ lst σ' = lst σ''"
proof -
have "(c, pls2) ∈ Decreasing_Diagrams.seq lrs"
proof -
have "∀ k. k ≤ pn2 ⟶ (c, (f_to_ls ?pf2 k)) ∈ Decreasing_Diagrams.seq lrs"
proof
fix k0
show "k0 ≤ pn2 ⟶ (c, (f_to_ls ?pf2 k0)) ∈ Decreasing_Diagrams.seq lrs"
proof (induct k0)
show "0 ≤ pn2 ⟶ (c, f_to_ls ?pf2 0) ∈ Decreasing_Diagrams.seq lrs"
using Decreasing_Diagrams.seq.intros(1)[of _ lrs] by simp
next
fix k
assume g1: "k ≤ pn2 ⟶ (c, f_to_ls ?pf2 k) ∈ Decreasing_Diagrams.seq lrs"
show "Suc k ≤ pn2 ⟶ (c, f_to_ls ?pf2 (Suc k)) ∈ Decreasing_Diagrams.seq lrs"
proof
assume h1: "Suc k ≤ pn2"
then have h2: "(c, f_to_ls ?pf2 k) ∈ Decreasing_Diagrams.seq lrs" using g1 by simp
obtain s where h3: "s = (ph2 k, [(pαi2 k, ph2 (Suc k))])" by blast
then have "s ∈ Decreasing_Diagrams.seq lrs"
using h1 d2' Decreasing_Diagrams.seq.intros(2)[of "ph2 k" "pαi2 k"] Decreasing_Diagrams.seq.intros(1)[of _ lrs] by simp
moreover have "lst (c, f_to_ls ?pf2 k) = fst s"
using pc13 h3 unfolding lst_def by (cases k, simp+)
ultimately show "(c, f_to_ls ?pf2 (Suc k)) ∈ Decreasing_Diagrams.seq lrs"
using h2 h3 Decreasing_Diagrams.seq_concat_helper[of c "f_to_ls ?pf2 k" lrs s] by simp
qed
qed
qed
then show ?thesis using pc15 by blast
qed
moreover have "lst (c, pls2) = fst σ''"
proof -
have "lst (c, pls2) = c'" using pc13 pc15 unfolding lst_def by (cases pn2, simp+)
then show ?thesis unfolding qc16 by simp
qed
ultimately show ?thesis using d4
unfolding c16 using Decreasing_Diagrams.seq_concat_helper[of c pls2 lrs σ'' ] by blast
qed
moreover have d6: "τ' ∈ Decreasing_Diagrams.seq lrs ∧ lst τ' = lst τ''"
proof -
have "(b, pls1) ∈ Decreasing_Diagrams.seq lrs"
proof -
have "∀ k. k ≤ pn1 ⟶ (b, (f_to_ls ?pf1 k)) ∈ Decreasing_Diagrams.seq lrs"
proof
fix k0
show "k0 ≤ pn1 ⟶ (b, (f_to_ls ?pf1 k0)) ∈ Decreasing_Diagrams.seq lrs"
proof (induct k0)
show "0 ≤ pn1 ⟶ (b, f_to_ls ?pf1 0) ∈ Decreasing_Diagrams.seq lrs"
using Decreasing_Diagrams.seq.intros(1)[of _ lrs] by simp
next
fix k
assume g1: "k ≤ pn1 ⟶ (b, f_to_ls ?pf1 k) ∈ Decreasing_Diagrams.seq lrs"
show "Suc k ≤ pn1 ⟶ (b, f_to_ls ?pf1 (Suc k)) ∈ Decreasing_Diagrams.seq lrs"
proof
assume h1: "Suc k ≤ pn1"
then have h2: "(b, f_to_ls ?pf1 k) ∈ Decreasing_Diagrams.seq lrs" using g1 by simp
obtain s where h3: "s = (ph1 k, [(pαi1 k, ph1 (Suc k))])" by blast
then have "s ∈ Decreasing_Diagrams.seq lrs"
using h1 d1' Decreasing_Diagrams.seq.intros(2)[of "ph1 k" "pαi1 k"] Decreasing_Diagrams.seq.intros(1)[of _ lrs] by simp
moreover have "lst (b, f_to_ls ?pf1 k) = fst s"
using pc9 h3 unfolding lst_def by (cases k, simp+)
ultimately show "(b, f_to_ls ?pf1 (Suc k)) ∈ Decreasing_Diagrams.seq lrs"
using h2 h3 Decreasing_Diagrams.seq_concat_helper[of b "f_to_ls ?pf1 k" lrs s] by simp
qed
qed
qed
then show ?thesis using pc11 by blast
qed
moreover have "lst (b, pls1) = fst τ''"
proof -
have "lst (b, pls1) = b'" using pc9 pc11 unfolding lst_def by (cases pn1, simp+)
then show ?thesis unfolding qc12 by simp
qed
ultimately show ?thesis using d3
unfolding c12 using Decreasing_Diagrams.seq_concat_helper[of b pls1 lrs τ'' ] by blast
qed
moreover have "fst σ = fst τ" using c4 by simp
moreover have "lst σ = fst τ'" using c4 c12 unfolding lst_def by simp
moreover have "lst τ = fst σ'" using c4 c16 unfolding lst_def by simp
moreover have "lst σ' = lst τ'"
proof -
have "lst τ'' = d"
proof (cases "n1 = 0")
assume "n1 = 0"
then show "lst τ'' = d" using c9 c11 qc12 unfolding lst_def by force
next
assume "n1 ≠ 0"
moreover then have "last ls1 = ( αi1 (n1-1), h1 n1 )" using c11 by (cases n1, simp+)
ultimately show "lst τ'' = d" using c9 c11 qc12 lem_ftofs_len unfolding lst_def
by (smt last_ConsR list.distinct(1) list.size(3) snd_conv)
qed
moreover have "lst σ'' = d"
proof (cases "n2 = 0")
assume "n2 = 0"
then show "lst σ'' = d" using c13 c15 qc16 unfolding lst_def by force
next
assume "n2 ≠ 0"
moreover then have "last ls2 = ( αi2 (n2-1), h2 n2 )" using c15 by (cases n2, simp+)
ultimately show "lst σ'' = d" using c13 c15 qc16 lem_ftofs_len unfolding lst_def
by (smt last_ConsR list.distinct(1) list.size(3) snd_conv)
qed
moreover have "lst τ' = lst τ'' ∧ lst σ' = lst σ''" using d5 d6 by blast
ultimately show ?thesis by metis
qed
moreover have "Decreasing_Diagrams.D cmp (labels τ) (labels σ) (labels σ') (labels τ')"
proof -
obtain σ1 where e01: "σ1 = (f_to_ls pαi2 pn2)" by blast
obtain σ2 where e1: "σ2 = (if c' = c'' then [] else [α])" by blast
obtain σ3 where e2: "σ3 = (f_to_ls αi2 n2)" by blast
obtain τ1 where e02: "τ1 = (f_to_ls pαi1 pn1)" by blast
obtain τ2 where e3: "τ2 = (if b' = b'' then [] else [β])" by blast
obtain τ3 where e4: "τ3 = (f_to_ls αi1 n1)" by blast
have "labels τ = [β] ∧ labels σ = [α]" using c4 unfolding labels_def by simp
moreover have "labels σ' = σ1 @ σ2 @ σ3"
proof -
have "labels σ'' = σ2 @ σ3"
proof -
have "∀ k. k ≤ n2 ⟶ map fst (f_to_ls ?f2 k) = f_to_ls αi2 k"
proof
fix k
show "k ≤ n2 ⟶ map fst (f_to_ls ?f2 k) = f_to_ls αi2 k" by (induct k, simp+)
qed
then show ?thesis using c15 qc16 e1 e2 unfolding labels_def by simp
qed
moreover have "labels σ' = σ1 @ labels σ''"
proof -
have "∀ k. k ≤ pn2 ⟶ map fst (f_to_ls ?pf2 k) = f_to_ls pαi2 k"
proof
fix k
show "k ≤ pn2 ⟶ map fst (f_to_ls ?pf2 k) = f_to_ls pαi2 k" by (induct k, simp+)
qed
then have "map fst pls2 = σ1" unfolding pc15 e01 by blast
then show ?thesis unfolding c16 labels_def by simp
qed
ultimately show ?thesis by simp
qed
moreover have "labels τ' = τ1 @ τ2 @ τ3"
proof -
have "labels τ'' = τ2 @ τ3"
proof -
have "∀ k. k ≤ n1 ⟶ map fst (f_to_ls ?f1 k) = f_to_ls αi1 k"
proof
fix k
show "k ≤ n1 ⟶ map fst (f_to_ls ?f1 k) = f_to_ls αi1 k" by (induct k, simp+)
qed
then show ?thesis using c11 qc12 e3 e4 unfolding labels_def by simp
qed
moreover have "labels τ' = τ1 @ labels τ''"
proof -
have "∀ k. k ≤ pn1 ⟶ map fst (f_to_ls ?pf1 k) = f_to_ls pαi1 k"
proof
fix k
show "k ≤ pn1 ⟶ map fst (f_to_ls ?pf1 k) = f_to_ls pαi1 k" by (induct k, simp+)
qed
then have "map fst pls1 = τ1" unfolding pc11 e02 by blast
then show ?thesis unfolding c12 labels_def by simp
qed
ultimately show ?thesis by simp
qed
moreover have "LD' cmp β α σ1 σ2 σ3 τ1 τ2 τ3"
proof -
let ?dn = "{α' . (α',α) ∈ cmp ∨ (α',β) ∈ cmp}"
have pf1: "set σ1 ⊆ {y. (y, β) ∈ cmp}"
proof -
have "∀ k. k ≤ pn2 ⟶ set (f_to_ls pαi2 k) ⊆ {y. (y, β) ∈ cmp}"
proof
fix k
show "k ≤ pn2 ⟶ set (f_to_ls pαi2 k) ⊆ {y. (y, β) ∈ cmp}" using b5 pc14 by (induct k, simp+)
qed
then show ?thesis using e01 by blast
qed
have pf2: "set τ1 ⊆ {y. (y, α) ∈ cmp}"
proof -
have "∀ k. k ≤ pn1 ⟶ set (f_to_ls pαi1 k) ⊆ {y. (y, α) ∈ cmp}"
proof
fix k
show "k ≤ pn1 ⟶ set (f_to_ls pαi1 k) ⊆ {y. (y, α) ∈ cmp}" using b5 pc10 by (induct k, simp+)
qed
then show ?thesis using e02 by blast
qed
have f1: "set σ3 ⊆ ?dn"
proof -
have "∀ k. k ≤ n2 ⟶ set (f_to_ls αi2 k) ⊆ ?dn"
proof
fix k
show "k ≤ n2 ⟶ set (f_to_ls αi2 k) ⊆ ?dn" using b5 c14 by (induct k, simp+)
qed
then show ?thesis using e2 by blast
qed
have f2: "set τ3 ⊆ ?dn"
proof -
have "∀ k. k ≤ n1 ⟶ set (f_to_ls αi1 k) ⊆ ?dn"
proof
fix k
show "k ≤ n1 ⟶ set (f_to_ls αi1 k) ⊆ ?dn" using b5 c10 by (induct k, simp+)
qed
then show ?thesis using e4 by blast
qed
have "LD_1' cmp β α σ1 σ2 σ3" using pf1 f1 e1 e2 unfolding LD_1'_def Decreasing_Diagrams.ds_def by simp
moreover have "LD_1' cmp α β τ1 τ2 τ3" using pf2 f2 e3 e4 unfolding LD_1'_def Decreasing_Diagrams.ds_def by force
ultimately show ?thesis unfolding LD'_def by blast
qed
moreover have "trans cmp ∧ wf cmp" using b6 b7 by blast
moreover then have "irrefl cmp" using irrefl_def by fastforce
ultimately show ?thesis using proposition3_4[of cmp β α σ1 σ2 σ3 τ1 τ2 τ3] by simp
qed
ultimately show ?thesis unfolding DD_def diagram_def D2_def by simp
qed
then show "∃ σ' τ'. DD lrs cmp (fst P,snd P,σ',τ')" using c2 by fastforce
qed
ultimately show ?thesis unfolding LD_def by blast
qed
section ‹Main theorem›
text ‹The next theorem has the following meaning:
if the cardinality of a binary relation $r$ does not exceed the first uncountable cardinal (‹cardSuc |UNIV::nat set|›), then the following two conditions are equivalent:›
text ‹1. $r$ is confluent (‹Abstract_Rewriting.CR r›)›
text ‹2. $r$ can be proven confluent using the decreasing diagrams method with natural numbers as labels (‹Decreasing_Diagrams.LD (UNIV::nat set) r›).›
theorem N1_completeness:
fixes r::"'a rel"
assumes "|r| ≤o cardSuc |UNIV::nat set|"
shows "Abstract_Rewriting.CR r = Decreasing_Diagrams.LD (UNIV::nat set) r"
proof
assume b0: "CR r"
have b1: "|r| ≤o cardSuc |UNIV::nat set|" using assms by simp
obtain κ where b2: "κ = cardSuc |UNIV::nat set|" by blast
have "|Field r| ≤o cardSuc |UNIV::nat set|"
proof (cases "finite r")
assume "finite r"
then show ?thesis using b2 lem_fin_fl_rel by (metis Field_card_of Field_natLeq cardSuc_ordLeq_ordLess
card_of_card_order_on card_of_mono2 finite_iff_ordLess_natLeq ordLess_imp_ordLeq)
next
assume "¬ finite r"
then show ?thesis using b1 b2 lem_rel_inf_fld_card using ordIso_ordLeq_trans by blast
qed
moreover have "confl_rel r" using b0 unfolding confl_rel_def Abstract_Rewriting.CR_on_def by blast
ultimately show "LD (UNIV::nat set) r" using lem_dc3_confl_lewsuc[of r] lem_dcr_to_ld by blast
next
assume "LD (UNIV::nat set) r"
then show "CR r" using Decreasing_Diagrams.sound by blast
qed
end