section ‹Fairness of Completion›
theory Completion_Fairness
imports
Abstract_Completion
Prime_Critical_Pairs
begin
locale kb_inf =
kb less for less :: "('a, 'b :: infinite) term ⇒ ('a, 'b) term ⇒ bool" (infix "≻" 50)
begin
lemma CP_subset_imp_rstep_CP_subset:
assumes "CP R ⊆ (⋃i≤n. (rstep (S i))⇧↔)"
shows "(rstep (CP R))⇧↔ ⊆ (⋃i≤n. (rstep (S i))⇧↔)" (is "_ ⊆ ?A")
proof
fix s t
assume "(s, t) ∈ (rstep (CP R))⇧↔"
then have "(s, t) ∈ rstep (CP R) ∨ (t, s) ∈ rstep (CP R)" by auto
moreover
{ fix s t
assume "(s, t) ∈ rstep (CP R)"
then have "(s, t) ∈ ?A"
proof (rule rstepE)
fix C σ l r
assume cp: "(l, r) ∈ CP R"
and [simp]: "s = C⟨l ⋅ σ⟩" "t = C⟨r ⋅ σ⟩"
from assms [THEN subsetD, OF cp]
show ?thesis by auto
qed }
ultimately show "(s, t) ∈ ?A" by (metis (no_types) Union_sym)
qed
lemma PCP_subset_imp_rstep_PCP_subset:
assumes "PCP R ⊆ (⋃i≤n. (rstep (S i))⇧↔)"
shows "(rstep (PCP R))⇧↔ ⊆ (⋃i≤n. (rstep (S i))⇧↔)" (is "_ ⊆ ?A")
proof
fix s t
assume "(s, t) ∈ (rstep (PCP R))⇧↔"
then have "(s, t) ∈ rstep (PCP R) ∨ (t, s) ∈ rstep (PCP R)" by auto
moreover
{ fix s t
assume "(s, t) ∈ rstep (PCP R)"
then have "(s, t) ∈ ?A"
proof (rule rstepE)
fix C σ l r
assume pcp: "(l, r) ∈ PCP R"
and [simp]: "s = C⟨l ⋅ σ⟩" "t = C⟨r ⋅ σ⟩"
from assms [THEN subsetD, OF pcp]
show ?thesis by auto
qed }
ultimately show "(s, t) ∈ ?A" by (metis (no_types) Union_sym)
qed
lemma PCP_subset_imp_rstep_PCP_subset':
assumes "PCP R ⊆ (rstep R)⇧↓ ∪ (⋃i≤n. (rstep (S i))⇧↔)"
shows "(rstep (PCP R))⇧↔ ⊆ (rstep R)⇧↓ ∪ (⋃i≤n. (rstep (S i))⇧↔)" (is "_ ⊆ ?A")
proof
fix s t
assume "(s, t) ∈ (rstep (PCP R))⇧↔"
then have *: "(s, t) ∈ rstep (PCP R) ∨ (t, s) ∈ rstep (PCP R)" by auto
moreover
{ fix s t
assume "(s, t) ∈ rstep (PCP R)"
then have "(s, t) ∈ ?A"
proof (rule rstepE)
fix C σ l r
assume pcp: "(l, r) ∈ PCP R"
and [simp]: "s = C⟨l ⋅ σ⟩" "t = C⟨r ⋅ σ⟩"
from assms [THEN subsetD, OF pcp]
show ?thesis by(auto) (metis atMost_iff rstep.simps)
qed }
ultimately
show "(s, t) ∈ ?A" by (auto simp del: reverseTrs intro: join_sym)
qed
lemma fair_imp_nabla:
assumes "PCP R ⊆ (⋃i≤n. (rstep (S i))⇧↔)"
shows "⋀s t u. (t, u) ∈ nabla R s ⟹ (t, u) ∈ (rstep R)⇧↓ ∪ (⋃i≤n. (rstep (S i))⇧↔)"
using PCP_subset_imp_rstep_PCP_subset [OF assms]
by (auto simp add: nabla_def)
lemma fair_new_imp_nabla:
assumes "PCP R ⊆ (rstep R)⇧↓ ∪ (⋃i≤n. (rstep (S i))⇧↔)"
shows "⋀s t u. (t, u) ∈ nabla R s ⟹ (t, u) ∈ (rstep R)⇧↓ ∪ (⋃i≤n. (rstep (S i))⇧↔)"
using PCP_subset_imp_rstep_PCP_subset' [OF assms]
by (auto simp: nabla_def)
lemma finite_run:
assumes "R 0 = {}" and "E n = {}"
and run: "∀i<n. (E i, R i) ⊢⇩K⇩B (E (Suc i), R (Suc i))"
and nabla: "⋀s t u. (t, u) ∈ nabla (R n) s ⟹ (t, u) ∈ (rstep (R n))⇧↓ ∪ (⋃i≤n. (rstep (E i))⇧↔)"
shows "(rstep (E 0))⇧↔⇧* = (rstep (R n))⇧↔⇧* ∧ SN (rstep (R n)) ∧ CR (rstep (R n))"
proof -
have R_less: "⋀i. i ≤ n ⟹ R i ⊆ {(x, y). x ≻ y}"
and "(rstep (E 0))⇧↔⇧* = (rstep (R n))⇧↔⇧*"
and SN: "SN (rstep (R n))"
by (fact finite_runD [OF assms(1-3)])+
moreover
have "CR (rstep (R n))"
proof -
define mless where "mless x y = mulex less¯¯ y x" for x y
write mless (infix "≻''" 50)
interpret lab: ars_labeled_sn "λM. mstep M (R n)" UNIV "op ≻'"
by (standard) (auto simp: mless_def intro: SN_less SN_mulex)
interpret ars_peak_decreasing "λM. mstep M (R n)" UNIV "op ≻'"
proof
fix s t u :: "('a, 'b) term" and M⇩1 M⇩2 :: "('a, 'b) term multiset"
define M where "M = {#t, u#}"
assume "(s, t) ∈ mstep M⇩1 (R n)" and "(s, u) ∈ mstep M⇩2 (R n)"
then have *: "(s, t) ∈ (rstep (R n))" "(s, u) ∈ rstep (R n)" by (auto iff: mstep_iff)
{ fix v w
assume "(v, w) ∈ nabla (R n) s"
then have "(s, v) ∈ (rstep (R n))⇧+" and "(s, w) ∈ (rstep (R n))⇧+" by (auto simp: nabla_def)
have "M⇩1 ≻' {#v, w#}"
proof -
from ‹(s, t) ∈ mstep M⇩1 (R n)› have ne1: "M⇩1 ≠ {#}" by (auto iff: mstep_iff)
have "∀u. u ∈# {#v, w#} ⟶ (∃z. z ∈# M⇩1 ∧ z ≻ u)"
proof -
{ have "∃z. z ∈# M⇩1 ∧ z ≻ v"
using ‹(s, t) ∈ mstep M⇩1 (R n)› and ‹(s, v) ∈ (rstep (R n))⇧+›
and rsteps_subset_less [OF R_less [of n]] by (auto simp: mstep_iff dest: trans) }
moreover
{ have "∃z. z ∈# M⇩1 ∧ z ≻ w"
using ‹(s, t) ∈ mstep M⇩1 (R n)› and ‹(s, w) ∈ (rstep (R n))⇧+›
and rsteps_subset_less [OF R_less [of n]] by (auto simp: mstep_iff dest: trans) }
ultimately show ?thesis by (auto simp: M_def)
qed
from mulex_on_all_strict [OF ne1 _ _ this, of UNIV]
have less1: "mulex less¯¯ {#v, w#} M⇩1" by auto (metis (lifting, no_types) conversep.intros mulex_on_mono)
then show ?thesis by (simp add: mless_def)
qed }
note nabla_less = this
let ?D = "(⋃c∈lab.downset2 M⇩1 M⇩2. mstep c (R n))⇧↔⇧*"
{ fix v w
assume nabla': "(v, w) ∈ nabla (R n) s"
let ?M = "{#v, w#}"
from nabla [OF nabla']
have "(v, w) ∈ (rstep (R n))⇧↓ ∪ (⋃ i≤n. (rstep (E i))⇧↔)" .
then have "(v, w) ∈ ?D"
proof
assume "(v, w) ∈ (rstep (R n))⇧↓"
then obtain u where 1: "(v, u) ∈ (rstep (R n))⇧*"
and 2: "(w, u) ∈ (rstep (R n))⇧*" by auto
from rsteps_imp_msteps [of _ ?M, OF _ 1 R_less]
have "(v, u) ∈ (mstep ?M (R n))⇧↔⇧*" by (auto simp: M_def)
from lab.conversion_in_downset2 [OF this] and nabla_less [OF nabla']
have 3: "(v, u) ∈ ?D" by simp
from rsteps_imp_msteps [of _ ?M, OF _ 2 R_less]
have "(u, w) ∈ (mstep ?M (R n))⇧↔⇧*" by (auto simp: M_def) (metis conversion_def in_rtrancl_UnI rtrancl_converseI)
from lab.conversion_in_downset2 [OF this] and nabla_less [OF nabla']
have 4: "(u, w) ∈ ?D" by simp
from 3 and 4 show ?thesis by (auto simp: conversion_def)
next
assume "(v, w) ∈ (⋃i ≤ n. (rstep (E i))⇧↔)"
then obtain i where "i ≤ n" and "(v, w) ∈ (rstep (E i))⇧↔" by auto
then have "(v, w) ∈ (mstep ?M (E i))⇧↔" by (auto iff: mstep_iff simp: M_def)
then have "(v, w) ∈ (mstep ?M (E i ∪ R i))⇧↔⇧*" by (auto simp: conversion_def)
then show ?thesis using ‹i ≤ n›
proof (induct "n - i" arbitrary: i)
case 0
with ‹i ≤ n› have [simp]: "i = n" by arith
with 0 have "(v, w) ∈ (mstep ?M (R n))⇧↔⇧*" by (simp add: assms)
from lab.conversion_in_downset2 [OF this] and nabla_less [OF nabla']
show ?case by auto
next
case (Suc m)
from ‹Suc m = n - i› have *: "m = n - Suc i" and leq: "Suc i ≤ n" by auto
from run have **: "(E i, R i) ⊢⇩K⇩B (E (Suc i), R (Suc i))" using leq by auto
from ‹(v, w) ∈ (mstep ?M (E i ∪ R i))⇧↔⇧*›
have "(v, w) ∈ (mstep ?M (E (Suc i) ∪ R (Suc i)))⇧↔⇧*"
using msteps_subset [OF ** R_less [OF leq]] by blast
from Suc.hyps(1) [OF * this leq]
show ?case .
qed
qed }
note ** = this
from peak_imp_nabla2 [OF SN_imp_variable_condition [OF SN] *]
show "(t, u) ∈ ?D"
by (auto dest!: ** simp: conversion_def)
qed
from CR show "CR (rstep (R n))" by simp
qed
ultimately show ?thesis by blast
qed
text ‹Every finite and fair run of abstract completion yields a complete TRS
for the given set of equations.›
lemma finite_fair_run:
assumes "R 0 = {}" and "E n = {}"
and "∀i<n. (E i, R i) ⊢⇩K⇩B (E (Suc i), R (Suc i))"
and fair: "PCP (R n) ⊆ (⋃i≤n. (rstep (E i))⇧↔)"
shows "(rstep (E 0))⇧↔⇧* = (rstep (R n))⇧↔⇧* ∧ SN (rstep (R n)) ∧ CR (rstep (R n))"
using finite_run [OF assms(1-3)] and fair_imp_nabla [OF fair] by blast
lemma finite_fair_new_run:
assumes "R 0 = {}" and "E n = {}"
and "∀i<n. (E i, R i) ⊢⇩K⇩B (E (Suc i), R (Suc i))"
and fair: "PCP (R n) ⊆ (rstep (R n))⇧↓ ∪ (⋃i≤n. (rstep (E i))⇧↔)"
shows "(rstep (E 0))⇧↔⇧* = (rstep (R n))⇧↔⇧* ∧ SN (rstep (R n)) ∧ CR (rstep (R n))"
using finite_run [OF assms(1-3)] and fair_new_imp_nabla [OF fair] by blast
end
locale kb_irun_inf =
kb_irun less for less :: "('a, 'b :: infinite) term ⇒ ('a, 'b) term ⇒ bool" (infix "≻" 50)
begin
lemma infinite_fair_run:
assumes nonfail: "E⇩ω = {}"
and fair: "PCP R⇩ω ⊆ (⋃i. (rstep (E i))⇧↔)"
shows "(rstep (E 0))⇧↔⇧* = (rstep R⇩ω)⇧↔⇧* ∧ SN (rstep R⇩ω) ∧ CR (rstep R⇩ω)"
proof (intro conjI)
show "SN (rstep R⇩ω)" by (rule SN_rstep_R_per)
show "(rstep (E 0))⇧↔⇧* = (rstep R⇩ω)⇧↔⇧*"
proof -
have "rstep ((⋃i. E i) ∪ (⋃i. R i)) ⊆ (rstep (E 0))⇧↔⇧*"
proof
fix s t assume "(s, t) ∈ rstep ((⋃i. E i) ∪ (⋃i. R i))"
then obtain i where "(s, t) ∈ rstep (E i ∪ R i)" by (auto simp: rstep_union rstep_UN)
then show "(s, t) ∈ (rstep (E 0))⇧↔⇧*"
proof (induct i arbitrary: s t)
case (Suc i)
have "(rstep (E i ∪ R i))⇧↔⇧* ⊆ ((rstep (E 0))⇧↔⇧*)⇧↔⇧*"
using Suc(1) by (intro conversion_mono) auto
with Suc(2) and rstep_E_R_Suc_conversion [THEN equalityD2, of i]
show ?case by auto
qed (auto simp: R0)
qed
from conversion_mono [OF this]
have "(rstep ((⋃i. E i) ∪ (⋃i. R i)))⇧↔⇧* ⊆ (rstep (E 0))⇧↔⇧*" by simp
moreover have "(rstep (E 0))⇧↔⇧* ⊆ (rstep ((⋃i. E i) ∪ (⋃i. R i)))⇧↔⇧*"
by (intro conversion_mono) (auto simp: rstep_union rstep_UN)
ultimately have "(rstep (E 0))⇧↔⇧* = (rstep ((⋃i. E i) ∪ (⋃i. R i)))⇧↔⇧*" by blast
also have "… = (rstep (⋃i. R i))⇧↔⇧*"
proof
have "(rstep ((⋃i. E i) ∪ (⋃i. R i)))⇧↔⇧* ⊆ ((rstep (⋃i. R i))⇧↔⇧*)⇧↔⇧*"
using subset_trans [OF rstep_E_i_subset [OF nonfail] join_imp_conversion]
by (intro conversion_mono) (auto simp: rstep_union rstep_UN)
then show "(rstep ((⋃i. E i) ∪ (⋃i. R i)))⇧↔⇧* ⊆ (rstep (⋃i. R i))⇧↔⇧*" by simp
qed (auto simp: rstep_union intro: conversion_mono [THEN subsetD])
finally show ?thesis unfolding rstep_R_inf_conv_iff [OF nonfail] .
qed
interpret ars_source_decreasing "op ≻" "rstep R⇩ω" UNIV
proof
show "SN {≻}" by (rule SN_less)
have pcp: "⋀s t. (s, t) ∈ rstep (PCP R⇩ω) ⟹ (s, t) ∈ (⋃i. (rstep (E i))⇧↔)"
using fair [THEN rstep_mono] by (auto simp: rstep_UN rstep_union rstep_rstep)
fix s t u presume "(s, t) ∈ slab R⇩ω s" and "(s, u) ∈ slab R⇩ω s"
then have "(t, u) ∈ nabla R⇩ω s ^^ 2" using R_per_varcond by (intro peak_imp_nabla2) auto
moreover
{ fix v w assume *: "(v, w) ∈ nabla R⇩ω s" "v = t ∨ w = u"
then have "s ≻ v" and "s ≻ w"
using rsteps_subset_less [OF rstep_R_per_less]
by (auto elim!: nablaE simp: rstep_rstep)
consider "(v, w) ∈ (rstep R⇩ω)⇧↓" | "(v, w) ∈ (⋃i. rstep (E i))⇧↔"
using * by (elim nablaE) (blast dest: pcp)+
then have "(v, w) ∈ (⋃v∈{v∈UNIV. s ≻ v}. slab R⇩ω v)⇧↔⇧*"
proof (cases)
case 1
then obtain x where "(v, x) ∈ (rstep R⇩ω)⇧*" and "(w, x) ∈ (rstep R⇩ω)⇧*" by blast
then have "(v, x) ∈ (⋃a∈{a∈UNIV. v ≽ a}. slab R⇩ω a)⇧↔⇧*"
and "(w, x) ∈ (⋃v∈{v∈UNIV. w ≽ v}. slab R⇩ω v)⇧↔⇧*"
using rsteps_slabI [OF _ _ rstep_R_per_less] by auto
then have "(v, x) ∈ (⋃a∈{a∈UNIV. s ≻ a}. slab R⇩ω a)⇧↔⇧*"
and "(x, w) ∈ (⋃a∈{a∈UNIV. s ≻ a}. slab R⇩ω a)⇧↔⇧*"
using ‹s ≻ v› and ‹s ≻ w›
by (auto intro: slab_conv_less_label simp: conversion_inv)
then show ?thesis by (auto simp: conversion_def)
next
let ?R = "⋃i. R i"
case 2
with rstep_E_i_subset [OF nonfail] have "(v, w) ∈ (rstep (⋃i. R i))⇧↓" by blast
then obtain x where "(v, x) ∈ (rstep ?R)⇧*" and "(w, x) ∈ (rstep ?R)⇧*" by blast
then have "(v, x) ∈ (⋃a∈{a∈UNIV. v ≽ a}. slab ?R a)⇧↔⇧*"
and "(x, w) ∈ (⋃v∈{v∈UNIV. w ≽ v}. slab ?R v)⇧↔⇧*"
using rsteps_slabI [OF _ _ rstep_R_inf_less] by (auto simp: conversion_inv)
with slab_R_inf_conv [OF nonfail]
have "(v, x) ∈ (⋃a∈{a∈UNIV. v ≽ a}. slab R⇩ω a)⇧↔⇧*"
and "(x, w) ∈ (⋃a∈{a∈UNIV. w ≽ a}. slab R⇩ω a)⇧↔⇧*" by auto
then have "(v, x) ∈ (⋃a∈{a∈UNIV. s ≻ a}. slab R⇩ω a)⇧↔⇧*"
and "(x, w) ∈ (⋃a∈{a∈UNIV. s ≻ a}. slab R⇩ω a)⇧↔⇧*"
using ‹s ≻ v› and ‹s ≻ w›
by (auto intro: slab_conv_less_label simp: conversion_inv)
then show ?thesis by (auto simp: conversion_def)
qed }
ultimately show "(t, u) ∈ (⋃v∈{v∈UNIV. s ≻ v}. slab R⇩ω v)⇧↔⇧*"
by (auto simp: conversion_def) (blast dest: rtrancl_trans)
qed
show "CR (rstep R⇩ω)" using CR by (simp add: UN_source_step)
qed
end
end