section ‹Abstract Completion›
theory Abstract_Completion
imports
"../Orderings/Reduction_Order"
Peak_Decreasingness
QTRS.Encompassment
"../Auxiliaries/Multiset_Extension2"
QTRS.Lexicographic_Extension
begin
lemma (in reduction_order) SN_encomp_Un_less:
"SN ({⋅⊳} ∪ {≻})"
using SN_encomp_Un_rewrel [of "{≻}"]
and ctxt and subst and SN_less by blast
lemma (in reduction_order) SN_encomp_Un_less_relto_encompeq:
"SN (relto ({⋅⊳} ∪ {≻}) {⋅⊵})"
using commutes_rewrel_encomp [of "{≻}"] and ctxt and subst
by (intro qc_SN_relto_encompeq SN_encomp_Un_less)
(auto dest: encomp_order.less_le_trans)
locale kb = reduction_order less
for less :: "('a, 'b) term ⇒ ('a, 'b) term ⇒ bool" (infix "≻" 50) +
fixes enc :: bool -- ‹‹True› if encompassment condition is used›
begin
definition "rstep_enc R =
(if enc then {(s, t). ∃(l, r)∈R. (s, t) ∈ rstep_rule (l, r) ∧ s ⋅⊳ l}
else rstep R)"
lemma rstep_encD [dest]:
"(s, t) ∈ rstep_enc R ⟹ (s, t) ∈ rstep R"
by (auto simp: rstep_enc_def rstep_rule.simps split: if_splits)
inductive
KB :: "('a, 'b) trs × ('a, 'b) trs ⇒ ('a, 'b) trs × ('a, 'b) trs ⇒ bool" (infix "⊢⇩K⇩B" 55)
where
deduce: "(u, s) ∈ rstep R ⟹ (u, t) ∈ rstep R ⟹ (E, R) ⊢⇩K⇩B (E ∪ {(s, t)}, R)" |
orientl: "s ≻ t ⟹ (s, t) ∈ E ⟹ (E, R) ⊢⇩K⇩B (E - {(s, t)}, R ∪ {(s, t)})" |
orientr: "t ≻ s ⟹ (s, t) ∈ E ⟹ (E, R) ⊢⇩K⇩B (E - {(s, t)}, R ∪ {(t, s)})" |
delete: "(s, s) ∈ E ⟹ (E, R) ⊢⇩K⇩B (E - {(s, s)}, R)" |
compose: "(t, u) ∈ rstep (R - {(s, t)}) ⟹ (s, t) ∈ R ⟹ (E, R) ⊢⇩K⇩B (E, (R - {(s, t)}) ∪ {(s, u)})" |
simplifyl: "(s, u) ∈ rstep R ⟹ (s, t) ∈ E ⟹ (E, R) ⊢⇩K⇩B ((E - {(s, t)}) ∪ {(u, t)}, R)" |
simplifyr: "(t, u) ∈ rstep R ⟹ (s, t) ∈ E ⟹ (E, R) ⊢⇩K⇩B ((E - {(s, t)}) ∪ {(s, u)}, R)" |
collapse: "(t, u) ∈ rstep_enc (R - {(t, s)}) ⟹ (t, s) ∈ R ⟹ (E, R) ⊢⇩K⇩B (E ∪ {(u, s)}, R - {(t, s)})"
lemma deduce_subset:
assumes "E' = E ∪ {(s, t)}" and "R' = R"
and "(u, s) ∈ rstep R" and "(u, t) ∈ rstep R"
shows "E ∪ R ⊆ E' ∪ R'"
using assms by fast
lemma deduce':
assumes "E' = E ∪ {(s, t)}" and "R' = R"
and "(u, s) ∈ rstep R" and "(u, t) ∈ rstep R"
shows "E' ∪ R' ⊆ E ∪ R ∪ (rstep R)¯ O rstep R"
using assms by fast
lemma orientl_subset:
assumes "E' = E - {(s, t)}" and "R' = R ∪ {(s, t)}"
and "s ≻ t" and "(s, t) ∈ E"
shows "E ∪ R ⊆ E' ∪ R' ∪ R'¯"
using assms by fast
lemma orientl':
assumes "E' = E - {(s, t)}" and "R' = R ∪ {(s, t)}"
and "s ≻ t" and "(s, t) ∈ E"
shows "E' ∪ R' ⊆ E ∪ R ∪ E¯"
using assms by fast
lemma orientr_subset:
assumes "E' = E - {(s, t)}" and "R' = R ∪ {(t, s)}"
and "t ≻ s" and "(s, t) ∈ E"
shows "E ∪ R ⊆ E' ∪ R' ∪ R'¯"
using assms by fast
lemma orientr':
assumes "E' = E - {(s, t)}" and "R' = R ∪ {(t, s)}"
and "t ≻ s" and "(s, t) ∈ E"
shows "E' ∪ R' ⊆ E ∪ R ∪ E¯"
using assms by fast
lemma delete_subset:
assumes "E' = E - {(s, s)}" and "R' = R"
and "(s, s) ∈ E"
shows "E ∪ R ⊆ E' ∪ R' ∪ Id"
using assms by fast
lemma delete':
assumes "E' = E - {(s, s)}" and "R' = R"
and "(s, s) ∈ E"
shows "E' ∪ R' ⊆ E ∪ R"
using assms by fast
lemma compose_subset:
assumes "E' = E" and "R' = (R - {(s, t)}) ∪ {(s, u)}"
and "(t, u) ∈ rstep (R - {(s, t)})" and "(s, t) ∈ R"
shows "E ∪ R ⊆ E' ∪ R' ∪ rstep R' O (rstep R')¯"
using assms by fast
lemma compose':
assumes "E' = E" and "R' = (R - {(s, t)}) ∪ {(s, u)}"
and "(t, u) ∈ rstep (R - {(s, t)})" and "(s, t) ∈ R"
shows "E' ∪ R' ⊆ E ∪ R ∪ rstep R O rstep R"
using assms by fast
lemma simplifyl_subset:
assumes "E' = (E - {(s, t)}) ∪ {(u, t)}" and "R' = R"
and "(s, u) ∈ rstep R" and "(s, t) ∈ E"
shows "E ∪ R ⊆ E' ∪ R' ∪ rstep R' O rstep E' ∪ rstep E' O (rstep R')¯"
using assms by fast
lemma simplifyl':
assumes "E' = (E - {(s, t)}) ∪ {(u, t)}" and "R' = R"
and "(s, u) ∈ rstep R" and "(s, t) ∈ E"
shows "E' ∪ R' ⊆ E ∪ R ∪ (rstep R)¯ O rstep E ∪ rstep E O rstep R"
using assms by fast
lemma simplifyr_subset:
assumes "E' = (E - {(s, t)}) ∪ {(s, u)}" and "R' = R"
and "(t, u) ∈ rstep R" and "(s, t) ∈ E"
shows "E ∪ R ⊆ E' ∪ R' ∪ rstep R' O rstep E' ∪ rstep E' O (rstep R')¯"
using assms by fast
lemma simplifyr':
assumes "E' = (E - {(s, t)}) ∪ {(s, u)}" and "R' = R"
and "(t, u) ∈ rstep R" and "(s, t) ∈ E"
shows "E' ∪ R' ⊆ E ∪ R ∪ (rstep R)¯ O rstep E ∪ rstep E O rstep R"
using assms by fast
lemma collapse_subset:
assumes "E' = E ∪ {(u, s)}" and "R' = R - {(t, s)}"
and "(t, u) ∈ rstep_enc (R - {(t, s)})" and "(t, s) ∈ R"
shows "E ∪ R ⊆ E' ∪ R' ∪ rstep_enc R' O rstep E'"
using assms by fast
lemma collapse':
assumes "E' = E ∪ {(u, s)}" and "R' = R - {(t, s)}"
and "(t, u) ∈ rstep_enc (R - {(t, s)})" and "(t, s) ∈ R"
shows "E' ∪ R' ⊆ E ∪ R ∪ (rstep R)¯ O rstep R"
using assms by fast
lemma rstep_reflcl_symcl_Un_idemp [simp]:
"rstep (((rstep R ∪ rstep S)⇧↔)⇧*) = ((rstep R ∪ rstep S)⇧↔)⇧*"
unfolding symcl_Un
unfolding rstep_simps(5) [symmetric]
unfolding rstep_union [symmetric]
unfolding rstep_rtrancl_idemp
by (rule refl)
lemma KB_subset:
assumes "(E, R) ⊢⇩K⇩B (E', R')"
shows "rstep (E ∪ R) ⊆ (rstep R')⇧= O (rstep (E' ∪ R'))⇧= O ((rstep R')¯)⇧="
proof -
have "E ∪ R ⊆ (rstep R')⇧= O (rstep (E' ∪ R'))⇧= O ((rstep R')¯)⇧=" (is "?L ⊆ ?R")
proof
fix s t
assume *: "(s, t) ∈ ?L"
from assms show "(s, t) ∈ ?R"
proof (cases)
case deduce
from deduce_subset [OF this] show ?thesis using * by blast
next
case orientl
from orientl_subset [OF this] show ?thesis using * by blast
next
case orientr
from orientr_subset [OF this] show ?thesis using * by blast
next
case delete
from delete_subset [OF this] show ?thesis using * by blast
next
case compose
from compose_subset [OF this] show ?thesis using * by blast
next
case simplifyl
from simplifyl_subset [OF this] show ?thesis using * by blast
next
case simplifyr
from simplifyr_subset [OF this] show ?thesis using * by blast
next
case collapse
from collapse_subset [OF this] show ?thesis using * by (blast 11)
qed
qed
from rstep_mono [OF this] show ?thesis by (simp add: rstep_simps)
qed
lemma KB_subset':
assumes "(E, R) ⊢⇩K⇩B (E', R')"
shows "rstep (E' ∪ R') ⊆ ((rstep (E ∪ R))⇧↔)⇧*"
(is "?L ⊆ ?R")
proof -
have "E' ∪ R' ⊆ ((rstep (E ∪ R))⇧↔)⇧*" (is "?L ⊆ ?R")
proof
fix s t
assume *: "(s, t) ∈ ?L"
from assms show "(s, t) ∈ ?R"
proof (cases)
case deduce
from deduce' [OF this] and *
have "(s, t) ∈ E ∪ R ∨ (s, t) ∈ (rstep R)¯ O rstep R" by auto
then show ?thesis
proof
assume "(s, t) ∈ (rstep R)¯ O rstep R"
then obtain u where "(s, u) ∈ (rstep R)¯" and "(u, t) ∈ rstep R" by auto
then have "(s, u) ∈ ?R" and "(u, t) ∈ ?R" by auto
then show ?thesis by simp
qed blast
next
case orientl
from orientl' [OF this] show ?thesis using * by blast
next
case orientr
from orientr' [OF this] show ?thesis using * by blast
next
case delete
from delete' [OF this] show ?thesis using * by blast
next
case compose
from compose' [OF this] and *
have "(s, t) ∈ E ∪ R ∨ (s, t) ∈ rstep R O rstep R" by auto
then show ?thesis
proof
assume "(s, t) ∈ rstep R O rstep R"
then obtain u where "(s, u) ∈ rstep R" and "(u, t) ∈ rstep R" by auto
then have "(s, u) ∈ ?R" and "(u, t) ∈ ?R" by auto
then show ?thesis by simp
qed blast
next
case simplifyl
from simplifyl' [OF this] and *
have "(s, t) ∈ E ∪ R ∨ (s, t) ∈ (rstep R)¯ O rstep E ∨ (s, t) ∈ rstep E O rstep R" by auto
then show ?thesis
proof (elim disjE)
assume "(s, t) ∈ (rstep R)¯ O rstep E"
then obtain u where "(s, u) ∈ (rstep R)¯" and "(u, t) ∈ rstep E" by auto
then have "(s, u) ∈ ?R" and "(u, t) ∈ ?R" by auto
then show ?thesis by simp
next
assume "(s, t) ∈ rstep E O rstep R"
then obtain u where "(s, u) ∈ rstep E" and "(u, t) ∈ rstep R" by auto
then have "(s, u) ∈ ?R" and "(u, t) ∈ ?R" by auto
then show ?thesis by simp
qed blast
next
case simplifyr
from simplifyr' [OF this] and *
have "(s, t) ∈ E ∪ R ∨ (s, t) ∈ (rstep R)¯ O rstep E ∨ (s, t) ∈ rstep E O rstep R" by auto
then show ?thesis
proof (elim disjE)
assume "(s, t) ∈ (rstep R)¯ O rstep E"
then obtain u where "(s, u) ∈ (rstep R)¯" and "(u, t) ∈ rstep E" by auto
then have "(s, u) ∈ ?R" and "(u, t) ∈ ?R" by auto
then show ?thesis by simp
next
assume "(s, t) ∈ rstep E O rstep R"
then obtain u where "(s, u) ∈ rstep E" and "(u, t) ∈ rstep R" by auto
then have "(s, u) ∈ ?R" and "(u, t) ∈ ?R" by auto
then show ?thesis by simp
qed blast
next
case collapse
from collapse' [OF this] and *
have "(s, t) ∈ E ∪ R ∨ (s, t) ∈ (rstep R)¯ O rstep R" by auto
then show ?thesis
proof
assume "(s, t) ∈ (rstep R)¯ O rstep R"
then obtain u where "(s, u) ∈ (rstep R)¯" and "(u, t) ∈ rstep R" by auto
then have "(s, u) ∈ ?R" and "(u, t) ∈ ?R" by auto
then show ?thesis by auto
qed blast
qed
qed
from rstep_mono [OF this] show ?thesis by (simp add: rstep_simps)
qed
lemma step_subset:
"(rstep R')⇧= O (rstep (E' ∪ R'))⇧= O ((rstep R')¯)⇧= ⊆ ((rstep (E' ∪ R'))⇧↔)⇧*"
(is "?L ⊆ ?R")
proof
fix s t assume "(s, t) ∈ ?L"
then obtain u and v where "(s, u) ∈ (rstep R')⇧="
and "(u, v) ∈ (rstep (E' ∪ R'))⇧="
and "(v, t) ∈ ((rstep R')¯)⇧=" by auto
then have "(s, u) ∈ ?R" and "(u, v) ∈ ?R" and "(v, t) ∈ ?R" by auto
then show "(s, t) ∈ ?R" by auto
qed
lemma KB_conversion:
assumes "(E, R) ⊢⇩K⇩B (E', R')"
shows "(rstep (E ∪ R))⇧↔⇧* = (rstep (E' ∪ R'))⇧↔⇧*" (is "?L = ?R")
proof
note * = subset_trans [OF KB_subset [OF assms] step_subset]
with converse_mono [THEN iffD2, OF *]
have "(rstep (E ∪ R))⇧↔ ⊆ ?R"
unfolding conversion_def
unfolding rtrancl_converse [symmetric]
unfolding symcl_converse by blast
from rtrancl_mono [OF this] show "?L ⊆ ?R"
unfolding conversion_def and rtrancl_idemp .
next
note * = KB_subset' [OF assms]
with converse_mono [THEN iffD2, OF *]
have "(rstep (E' ∪ R'))⇧↔ ⊆ ?L"
unfolding conversion_def
unfolding rtrancl_converse [symmetric]
unfolding symcl_converse by blast
from rtrancl_mono [OF this] show "?R ⊆ ?L"
unfolding conversion_def and rtrancl_idemp .
qed
lemma KB_rtrancl_conversion:
assumes "KB⇧*⇧* (E, R) (E', R')"
shows "(rstep (E ∪ R))⇧↔⇧* = (rstep (E' ∪ R'))⇧↔⇧*"
using assms
by (induct "(E, R)" "(E', R')" arbitrary: E' R')
(force dest: KB_conversion)+
lemma KB_rtrancl_rules_subset_less:
assumes "KB⇧*⇧* (E, R) (E', R')" and "R ⊆ {≻}"
shows "R' ⊆ {≻}"
using assms
proof (induction "(E, R)" "(E', R')" arbitrary: E' R')
case (rtrancl_into_rtrancl ER'')
moreover then obtain E'' and R''
where [simp]: "ER'' = (E'', R'')" by force
ultimately have "(E'', R'') ⊢⇩K⇩B (E', R')" and "R'' ⊆ {≻}" by simp+
moreover
{
fix s t u
assume "(t, u) ∈ rstep (R'' - {(s, t)})" and "(s, t) ∈ R''" and "R'' ⊆ {≻}"
then have "s ≻ u" by (induct t u) (blast intro: subst ctxt dest: trans)
}
ultimately show ?case by (cases) auto
qed
definition mstep :: "('a, 'b) term multiset ⇒ ('a, 'b) trs ⇒ ('a, 'b) term rel"
where
"mstep M R = {(s, t). (s, t) ∈ rstep R ∧ (∃s' t'. s' ∈# M ∧ t' ∈# M ∧ s' ≽ s ∧ t' ≽ t)}"
lemma mstep_iff:
"(x, y) ∈ mstep M R ⟷ (x, y) ∈ rstep R ∧ (∃s' t'. s' ∈# M ∧ t' ∈# M ∧ s' ≽ x ∧ t' ≽ y)"
by (auto simp: mstep_def)
lemma UN_mstep:
"(⋃x∈R. mstep M {x}) = mstep M R"
by (auto simp add: mstep_iff) blast+
lemma mstep_Un [simp]:
"mstep M (R ∪ R') = mstep M R ∪ mstep M R'"
by (auto iff: mstep_iff)
lemma mstep_mono [simp]:
"R ⊆ R' ⟹ mstep M R ⊆ mstep M R'"
unfolding mstep_def by fast
lemma step_subset':
"(mstep M R')⇧= O (mstep M (E' ∪ R'))⇧= O ((mstep M R')¯)⇧= ⊆ ((mstep M (E' ∪ R'))⇧↔)⇧*"
(is "?L ⊆ ?R")
proof
fix s t assume "(s, t) ∈ ?L"
then obtain u and v where "(s, u) ∈ (mstep M R')⇧="
and "(u, v) ∈ (mstep M (E' ∪ R'))⇧="
and "(v, t) ∈ ((mstep M R')¯)⇧=" by auto
then have "(s, u) ∈ ?R" and "(u, v) ∈ ?R" and "(v, t) ∈ ?R" by auto
then show "(s, t) ∈ ?R" by auto
qed
lemma mstep_converse:"(mstep M R)⇧↔ = mstep M (R⇧↔)"
unfolding mstep_def by auto
lemma rstep_subset_less:
assumes "R ⊆ {(x, y). x ≻ y}"
shows "rstep R ⊆ {(x, y). x ≻ y}"
proof
fix x y assume "(x, y) ∈ rstep R" then show "(x, y) ∈ {(x, y). x ≻ y}"
using assms by (induct) (auto intro: subst ctxt)
qed
lemma rsteps_subset_less:
assumes "R ⊆ {(x, y). x ≻ y}"
shows "(rstep R)⇧+ ⊆ {(x, y). x ≻ y}"
proof
fix s t
assume "(s, t) ∈ (rstep R)⇧+"
then show "(s, t) ∈ {(x, y). x ≻ y}"
proof (induct)
case (base u)
with rstep_subset_less [OF assms] show ?case by auto
next
case (step t u)
then show ?case
using rstep_subset_less [OF assms]
by auto (metis in_mono mem_Collect_eq split_conv trans)
qed
qed
lemma mstep_subset:
assumes "(E, R) ⊢⇩K⇩B (E', R')" and "R' ⊆ {(x, y). x ≻ y}"
shows "mstep M (E ∪ R) ⊆ (mstep M (E' ∪ R'))⇧↔⇧*"
proof
fix s t
assume "(s, t) ∈ mstep M (E ∪ R)"
then obtain s' and t' where "s' ∈# M" and "t' ∈# M"
and "s' ≽ s" and "t' ≽ t" and "(s, t) ∈ rstep (E ∪ R)"
by (auto simp: mstep_def)
with KB_subset [OF assms(1)] obtain u and v
where "(s, u) ∈ (rstep R')⇧=" and "(u, v) ∈ (rstep (E' ∪ R'))⇧="
and "(v, t) ∈ ((rstep R')¯)⇧=" by blast
moreover then have "(t, v) ∈ (rstep R')⇧=" by auto
ultimately have "s ≽ u" and "t ≽ v" using rstep_subset_less [OF assms(2)] by auto
with ‹s' ≽ s› and ‹t' ≽ t› have "s' ≽ u" and "t' ≽ v" using trans by blast+
then have "(s, u) ∈ (mstep M R')⇧="
and "(u, v) ∈ (mstep M (E' ∪ R'))⇧="
and "(v, t) ∈ ((mstep M R')¯)⇧="
using ‹s' ∈# M› and ‹t' ∈# M›
and ‹s' ≽ s› and ‹t' ≽ t›
and ‹(s, u) ∈ (rstep R')⇧=›
and ‹(u, v) ∈ (rstep (E' ∪ R'))⇧=›
and ‹(v, t) ∈ ((rstep R')¯)⇧=›
unfolding mstep_def by (blast)+
then have "(s, t) ∈ (mstep M R')⇧= O ((mstep M (E' ∪ R')))⇧= O ((mstep M R')¯)⇧=" by blast
with step_subset' [of M R' E'] show "(s, t) ∈ (mstep M (E' ∪ R'))⇧↔⇧*"
unfolding conversion_def by blast
qed
lemma mstep_subset':
assumes "(E, R) ⊢⇩K⇩B (E', R')" and "R' ⊆ {(x, y). x ≻ y}"
shows "(mstep M (E ∪ R))¯ ⊆ (mstep M (E' ∪ R'))⇧↔⇧*"
using converse_mono [THEN iffD2, OF mstep_subset [OF assms, of M]]
by simp
lemma mstep_symcl_subset:
assumes "(E, R) ⊢⇩K⇩B (E', R')" and "R' ⊆ {(x, y). x ≻ y}"
shows "(mstep M (E ∪ R))⇧↔ ⊆ (mstep M (E' ∪ R'))⇧↔⇧*"
using mstep_subset [OF assms] and mstep_subset' [OF assms] by blast
lemma msteps_subset:
assumes "(E, R) ⊢⇩K⇩B (E', R')" and "R' ⊆ {(x, y). x ≻ y}"
shows "(mstep M (E ∪ R))⇧↔⇧* ⊆ (mstep M (E' ∪ R'))⇧↔⇧*"
using mstep_symcl_subset [OF assms, THEN rtrancl_mono] by (simp add: conversion_def)
lemma UNIV_mstep_rstep_iff [simp]:
"(⋃M∈UNIV. mstep M R) = rstep R"
proof -
have *: "⋀s t. (s, t) ∈ rstep R ⟹
s ∈# {#s, t#} ∧ t ∈# {#s, t#} ∧ s ≽ s ∧ t ≽ t ∧
(s, t) ∈ mstep {#s, t#} R" by (auto iff: mstep_iff)
show ?thesis by (auto iff: mstep_iff) (insert *, blast)
qed
lemma rstep_imp_mstep:
assumes "(t, u) ∈ rstep R" and "s ∈# M" and "s ≽ t" and "t ≻ u"
shows "(t, u) ∈ mstep M R"
using assms by (auto simp: mstep_iff dest: trans)
lemma rsteps_imp_msteps:
assumes "t ∈# M" and "(t, u) ∈ (rstep R)⇧*" and "R ⊆ {(x, y). x ≻ y}"
shows "(t, u) ∈ (mstep M R)⇧*"
using assms(2, 1)
proof (induct)
case base show ?case by simp
next
note less = rstep_subset_less [OF assms(3)]
case (step u v)
have "(u, v) ∈ rstep R" by fact
moreover have "t ∈# M" by fact
moreover
from ‹(t, u) ∈ (rstep R)⇧*› and less
have "t ≽ u" by (induct) (auto dest: trans)
moreover have "u ≻ v" using less and step by blast
ultimately have "(u, v) ∈ mstep M R" by (rule rstep_imp_mstep)
with step show ?case by auto
qed
lemma mstep_conv_imp_rstep_conv:"(mstep M R)⇧↔⇧* ⊆ (rstep R)⇧↔⇧*"
by (rule conversion_mono, insert mstep_iff, auto)
subsection ‹Finite runs›
lemma finite_runD:
assumes "R 0 = {}" and "E n = {}"
and run: "∀i<n. (E i, R i) ⊢⇩K⇩B (E (Suc i), R (Suc i))"
shows finite_run_imp_conversion_eq: "(rstep (E 0))⇧↔⇧* = (rstep (R n))⇧↔⇧*"
and finite_run_imp_SN: "SN (rstep (R n))"
and finite_run_imp_R_less: "⋀i. i ≤ n ⟹ R i ⊆ {(x, y). x ≻ y}"
proof -
have *: "⋀i. i ≤ n ⟹ KB⇧*⇧* (E 0, R 0) (E i, R i)"
proof -
fix i assume "i ≤ n"
with run show "KB⇧*⇧* (E 0, R 0) (E i, R i)"
by (induct i) (auto, metis (hide_lams, no_types) Suc_le_eq rtranclp.rtrancl_into_rtrancl)
qed
from * [THEN KB_rtrancl_rules_subset_less] and ‹R 0 = {}›
show "⋀i. i ≤ n ⟹ R i ⊆ {(x, y). x ≻ y}" by auto
with rstep_subset_less [of "R n"]
show "SN (rstep (R n))" using SN_less by (simp add: assms) (metis SN_subset)
from KB_rtrancl_conversion [OF * [of n]]
show "(rstep (E 0))⇧↔⇧* = (rstep (R n))⇧↔⇧*" by (simp add: assms)
qed
end
subsection ‹Infinite runs›
context kb
begin
lemma KB_E_subset:
assumes "(E, R) ⊢⇩K⇩B (E', R')"
shows "E ⊆ E' ∪ (rstep R' O E') ∪ (E' O (rstep R')¯) ∪ R'⇧↔ ∪ Id"
using assms by (cases) blast+
lemma KB_R_subset:
assumes "(E, R) ⊢⇩K⇩B (E', R')"
shows "R ⊆ R' ∪ rstep_enc R' O E' ∪ R' O (rstep R')¯"
proof -
{ fix s t u
assume "R' = R - {(s, t)} ∪ {(s, u)}" and "(t, u) ∈ rstep (R - {(s, t)})" and "(s, t) ∈ R"
then have "(s, u) ∈ R'" and "(t, u) ∈ rstep R'" by auto
then have "(s, t) ∈ R' O (rstep R')¯" by blast }
with assms show ?thesis by (cases) blast+
qed
text ‹Source labeling of rewrite steps.›
abbreviation "slab S ≡ source_step (rstep S)"
lemma slab_conv_below_ctxt_subst:
assumes "(s, t) ∈ (⋃v∈{v. u ≽ v}. slab S v)⇧↔⇧*"
shows "(C⟨s ⋅ σ⟩, C⟨t ⋅ σ⟩) ∈ (⋃v∈{v. C⟨u ⋅ σ⟩ ≽ v}. slab S v)⇧↔⇧*"
using assms
unfolding conversion_def
proof (induct)
case (step y z)
then have "(C⟨y ⋅ σ⟩, C⟨z ⋅ σ⟩) ∈ (⋃v∈{v. C⟨u ⋅ σ⟩ ≽ v}. slab S v)⇧↔"
by (blast intro: ctxt subst)
with step show ?case by (blast intro: rtrancl_into_rtrancl)
qed blast
lemma rsteps_slabI:
assumes "(s, t) ∈ (rstep S)⇧*" "w ≽ s" and "rstep S ⊆ {≻}"
shows "w ≽ t ∧ (s, t) ∈ (⋃v∈{v. w ≽ v}. slab S v)⇧↔⇧*"
using assms
proof (induct)
case (step t u)
from step(3, 4, 5) have "w ≽ t" and "(s, t) ∈ (⋃v∈{v. w ≽ v}. slab S v)⇧↔⇧*" by (blast)+
moreover with step(2, 5) have "t ≻ u" and "(t, u) ∈ (⋃v∈{v. w ≽ v}. slab S v)⇧↔⇧*" by auto
ultimately show ?case by (blast intro: trans rtrancl_trans)
qed simp
lemma slab_conv_below_label:
assumes "(s, t) ∈ (⋃v∈{v. u ≽ v}. slab S v)⇧↔⇧*" and "w ≽ u"
shows "(s, t) ∈ (⋃v∈{v. w ≽ v}. slab S v)⇧↔⇧*"
using assms unfolding conversion_def
proof (induct)
case (step t v)
from step(2, 4) have "(t, v) ∈ (⋃v∈{v. w ≽ v}. slab S v)⇧↔" by (blast dest: trans)
with step(3) [OF step(4)] show ?case by (blast intro: rtrancl_into_rtrancl)
qed simp
lemma slab_conv_less_label:
assumes "(s, t) ∈ (⋃v∈{v. u ≽ v}. slab S v)⇧↔⇧*" and "w ≻ u"
shows "(s, t) ∈ (⋃v∈{v. w ≻ v}. slab S v)⇧↔⇧*"
using assms unfolding conversion_def
proof (induct)
case (step t v)
from step(2, 4) have "(t, v) ∈ (⋃v∈{v. w ≻ v}. slab S v)⇧↔" by (blast dest: trans)
with step(3) [OF step(4)] show ?case by (blast intro: rtrancl_into_rtrancl)
qed simp
lemma msteps_imp_source_steps:
assumes "∀ t ∈# M. s ≻ t"
shows "(mstep M ℛ)⇧↔⇧* ⊆ (⋃z ∈ {z. s ≻ z}. slab ℛ z)⇧↔⇧*"
proof-
have "mstep M ℛ ⊆ (⋃z ∈ {z. s ≻ z}. slab ℛ z)"
proof
fix t u
assume a: "(t, u) ∈ mstep M ℛ"
then have tu: "(t, u) ∈ rstep ℛ" unfolding mstep_def mem_Collect_eq by auto
from a have "∃ v ∈# M. v ≽ t" unfolding mstep_def mem_Collect_eq by auto
with assms transD [OF trans_less] have st: "s ≻ t" by blast
from tu have "(t, u) ∈ slab ℛ t" unfolding source_step_def by auto
with st show "(t, u) ∈ (⋃z ∈ {z. s ≻ z}. slab ℛ z)" by auto
qed
from conversion_mono [OF this] show ?thesis by auto
qed
end
locale kb_irun = kb +
fixes R E
assumes R0: "R 0 = {}" and enc: enc
and irun: "⋀i. (E i, R i) ⊢⇩K⇩B (E (Suc i), R (Suc i))"
begin
lemma rstep_encE [elim]:
assumes "(s, t) ∈ rstep_enc S"
obtains C and σ and l and r where "(l, r) ∈ S" and "s ⋅⊳ l"
and "s = C⟨l ⋅ σ⟩" and "t = C⟨r ⋅ σ⟩"
using assms by (auto simp: rstep_enc_def) (insert enc, auto elim: rstep_rule.cases)
lemma rstep_encI [intro]:
assumes "s ⋅⊳ l" and "(l, r) ∈ S" and "s = C⟨l ⋅ σ⟩" and "t = C⟨r ⋅ σ⟩"
shows "(s, t) ∈ rstep_enc S"
using assms by (auto simp: rstep_enc_def)
lemma rstep_E_R_Suc_conversion:
"(rstep (E i ∪ R i))⇧↔⇧* = (rstep (E (Suc i) ∪ R (Suc i)))⇧↔⇧*"
using KB_conversion [OF irun [of i]] by blast
abbreviation Rinf ("R⇩∞") where "R⇩∞ ≡ (⋃i. R i)"
abbreviation Einf ("E⇩∞") where "E⇩∞ ≡ (⋃i. E i)"
definition "R⇩ω = (⋃i. ⋂j∈{j. j≥i}. R j)"
definition "E⇩ω = (⋃i. ⋂j∈{j. j≥i}. E j)"
lemma R_per_subset_R_inf: "R⇩ω ⊆ R⇩∞"
by (auto simp: R⇩ω_def)
lemma E_per_subset_E_inf: "E⇩ω ⊆ E⇩∞"
by (auto simp: E⇩ω_def)
lemma rstep_R_per_subset_rstep_R_inf: "rstep R⇩ω ⊆ rstep R⇩∞"
using R_per_subset_R_inf and rstep_mono by blast
lemma run_R_less: "R i ⊆ {≻}"
proof -
{ fix i
have "KB⇧*⇧* (E 0, R 0) (E i, R i)"
using irun by (induct i) (auto intro: rtranclp.rtrancl_into_rtrancl) }
from KB_rtrancl_rules_subset_less [OF this] and R0
show ?thesis by auto
qed
lemma rstep_R_inf_less: "rstep R⇩∞ ⊆ {≻}"
using run_R_less by (auto elim!: rstepE intro: ctxt subst)
lemma SN_rstep_R_per:
"SN (rstep R⇩ω)"
by (rule ccontr)
(insert SN_less rstep_R_per_subset_rstep_R_inf rstep_R_inf_less, auto simp: SN_defs)
lemma R_per_varcond:
"∀(l, r) ∈ R⇩ω. vars_term r ⊆ vars_term l"
using SN_rstep_R_per by (rule SN_imp_variable_condition)
lemma rstep_R_per_less: "rstep R⇩ω ⊆ {≻}"
proof
fix s t assume "(s, t) ∈ rstep R⇩ω"
then obtain C σ l r where "(l, r) ∈ R⇩ω" and [simp]: "s = C⟨l ⋅ σ⟩" "t = C⟨r ⋅ σ⟩" by blast
then obtain i where "(l, r) ∈ R i" by (auto simp: R⇩ω_def)
then show "(s, t) ∈ {≻}" using run_R_less [of i] by (auto simp: ctxt subst)
qed
abbreviation "termless ≡ (relto ({⋅⊳} ∪ {≻}) {⋅⊵})⇧+"
abbreviation "lexless ≡ lex_two termless Id termless"
abbreviation "mulless ≡ s_mul_ext Id {≻}"
sublocale mlessop: SN_order_pair mulless "ns_mul_ext Id {≻}"
proof (intro SN_order_pair.mul_ext_SN_order_pair)
show "SN_order_pair {≻} Id"
by (standard) (auto simp: refl_on_def trans_def SN_less dest: trans)
qed
context
assumes nonfail: "E⇩ω = {}"
begin
lemma E_i_subset_join_R_inf:
"E i ⊆ (rstep R⇩∞)⇧↓" (is "_ ⊆ ?R⇧↓")
proof
fix s t assume "(s, t) ∈ E i"
then show "(s, t) ∈ ?R⇧↓"
proof (induct "{#s, t#}" arbitrary: s t i rule: SN_induct [OF mlessop.SN])
case less: 1
note IH = this(1)
from nonfail have "∃j>i. (s, t) ∉ E j" using Suc_le_eq unfolding E⇩ω_def by blast
moreover define j where "j = (LEAST j. j > i ∧ (s, t) ∉ E j)"
ultimately have "j > i" and not_j: "(s, t) ∉ E j" by (metis (lifting) LeastI)+
then have "j - 1 < j" and [simp]: "Suc (j - Suc 0) = j" by auto
from not_less_Least [OF this(1) [unfolded j_def], folded j_def] and ‹(s, t) ∈ E i› and ‹j > i›
have "(s, t) ∈ E (j - 1)" by (cases "j = Suc i") auto
with KB_E_subset [OF irun [of "j - 1"]] and not_j
consider "(s, t) ∈ ((R j)⇧↔)⇧=" | "(s, t) ∈ rstep (R j) O E j" | "(s, t) ∈ E j O (rstep (R j))¯"
by auto blast
then show ?case
proof (cases)
case 2
then obtain u where su: "(s, u) ∈ rstep (R j)" and ut: "(u, t) ∈ E j" by blast
then have "s ≻ u" using run_R_less [of j] by (blast intro: ctxt subst)
then have "({#s, t#}, {#u, t#}) ∈ mulless"
by (intro s_mul_ext_IdI [of "{#s#}" _ "{#t#}" _ "{#u#}"]) simp_all
from IH [OF this ut] have "(u, t) ∈ ?R⇧↓" by blast
moreover have "(s, u) ∈ ?R⇧*" using su by blast
ultimately show ?thesis by (blast intro: rtrancl_join_join)
next
case 3
then obtain u where su: "(s, u) ∈ E j" and tu: "(t, u) ∈ rstep (R j)" by blast
then have "t ≻ u" using run_R_less [of j] by (blast intro: ctxt subst)
then have "({#s, t#}, {#s, u#}) ∈ mulless"
by (intro s_mul_ext_IdI [of "{#t#}" _ "{#s#}" _ "{#u#}"]) simp_all
from IH [OF this su] have "(s, u) ∈ ?R⇧↓" by blast
moreover have "(t, u) ∈ ?R⇧*" using tu by blast
ultimately show ?thesis by (blast intro: join_rtrancl_join)
qed blast
qed
qed
lemma rstep_E_i_subset:
"rstep (E i) ⊆ (rstep R⇩∞)⇧↓" (is "?E ⊆ ?R⇧↓")
proof
fix s t assume "(s, t) ∈ ?E"
then obtain C σ l r where "(l, r) ∈ E i" and "s = C⟨l ⋅ σ⟩" and "t = C⟨r ⋅ σ⟩" by blast
moreover with E_i_subset_join_R_inf [of i] have "(l, r) ∈ ?R⇧↓" by blast
ultimately show "(s, t) ∈ ?R⇧↓" by auto
qed
lemma SN_lexless: "SN lexless"
by (intro lex_two)
(auto simp only: SN_trancl_SN_conv intro: SN_encomp_Un_less_relto_encompeq)
lemma source_step_R_inf_subset:
"source_step R⇩∞ l ⊆ (⋃t∈{t. l ≽ t}. slab R⇩ω t)⇧↔⇧*" (is "source_step ?R l ⊆ ?L l")
proof
fix t u assume "(t, u) ∈ source_step R⇩∞ l"
then obtain r where "(l, r) ∈ ?R" and [simp]: "t = l" "u = r" by blast
have "(l, r) ∈ ?L l" using ‹(l, r) ∈ ?R›
proof (induct "(l, r)" arbitrary: l r rule: SN_induct [OF SN_lexless])
case less: 1
note IH = this(1)
have lr: "(l, r) ∈ ?R" using less by blast
show ?case
proof (cases "(l, r) ∈ R⇩ω")
case False
with lr obtain j where "(l, r) ∈ R j" and "∃i>j. (l, r) ∉ R i"
by (force simp: R⇩ω_def le_eq_less_or_eq)
moreover define i where "i = (LEAST i. i > j ∧ (l, r) ∉ R i)"
ultimately have "i > j" and not_i: "(l, r) ∉ R i" by (metis (lifting) LeastI)+
then have "i - 1 < i" and [simp]: "Suc (i - Suc 0) = i" by auto
from not_less_Least [OF this(1) [unfolded i_def], folded i_def] and ‹i > j› and ‹(l, r) ∈ R j›
have "(l, r) ∈ R (i - 1)" by (cases "i = Suc j") auto
with KB_R_subset [OF irun [of "i - 1"]] and not_i
consider "(l, r) ∈ rstep_enc (R i) O E i" | "(l, r) ∈ R i O (rstep (R i))¯" by force
then show ?thesis
proof (cases)
case 1
then obtain u where lu: "(l, u) ∈ rstep_enc (R i)" and "(u, r) ∈ E i" by blast
with E_i_subset_join_R_inf have "(u, r) ∈ (rstep ?R)⇧↓" by blast
then obtain v where uv: "(u, v) ∈ (rstep ?R)⇧*" and rv: "(r, v) ∈ (rstep ?R)⇧*" by blast
have "(l, r) ∈ (rstep ?R)⇧+" using lr by auto
from trancl_mono [OF this rstep_R_inf_less] have "l ≻ r" by simp
with rv have rv_L: "(r, v) ∈ ?L l"
proof (induct)
case (step x y)
with rtrancl_mono [OF rstep_R_inf_less] have "l ≻ x" by (auto dest: trans)
from step have "(r, x) ∈ ?L l" by blast
moreover have "(x, y) ∈ ?L l"
proof -
obtain C σ l' r' where *: "(l', r') ∈ ?R" and x: "x = C⟨l' ⋅ σ⟩" and y: "y = C⟨r' ⋅ σ⟩"
using step(2) by fast
then have "x ⋅⊵ l'" by auto
then have "(l, l') ∈ termless" using ‹l ≻ x› by blast
then have "((l, r), (l', r')) ∈ lexless" by auto
from IH [OF this *] have "(l', r') ∈ ?L l'" .
then have "(x, y) ∈ ?L x"
unfolding x y conversion_def [symmetric] by (rule slab_conv_below_ctxt_subst)
with slab_conv_below_label [OF ‹(x, y) ∈ ?L x›, of l] and ‹l ≻ x› show ?thesis by simp
qed
ultimately show ?case by (auto simp: conversion_def)
qed simp
from uv have "(l, v) ∈ ?L l"
proof (induct)
case base
from lu obtain l' r' where *: "(l', r') ∈ ?R" and lu': "(l, u) ∈ rstep_enc {(l', r')}" by fast
then have "((l, r), (l', r')) ∈ lexless" by auto
from IH [OF this *] have "(l', r') ∈ ?L l'" .
moreover obtain C σ where "l = C⟨l' ⋅ σ⟩" and "u = C⟨r' ⋅ σ⟩" using lu' by blast
ultimately show ?case
using slab_conv_below_ctxt_subst [of l' r' R⇩ω l' C σ] by simp
next
case (step x w)
then obtain l' r' where *: "(l', r') ∈ ?R"
and "(u, x) ∈ (rstep ?R)⇧*" and xw: "(x, w) ∈ rstep {(l', r')}" by blast
moreover have "(l, u) ∈ (rstep ?R)⇧+" using lu by (blast)
ultimately have "(l, x) ∈ (rstep ?R)⇧+" by auto
then have "l ≻ x" using trancl_mono_set [OF rstep_R_inf_less] by auto
moreover with xw have "x ⋅⊵ l'" by blast
ultimately have "(l, l') ∈ termless" by blast
then have "((l, r), (l', r')) ∈ lexless" by auto
from IH [OF this *] have "(l', r') ∈ ?L l'" .
moreover obtain C σ where "x = C⟨l' ⋅ σ⟩" and "w = C⟨r' ⋅ σ⟩" using xw by blast
ultimately have "(x, w) ∈ ?L x" using slab_conv_below_ctxt_subst [of l' r' R⇩ω l' C σ] by simp
moreover have "l ≽ x" using ‹l ≻ x› by simp
ultimately have "(x, w) ∈ ?L l" by (metis slab_conv_below_label)
moreover have "(l, x) ∈ ?L l" using step by blast
ultimately show ?case by (auto simp: conversion_def)
qed
moreover have "(v, r) ∈ ?L l" using rv_L by (simp add: conversion_inv)
ultimately show ?thesis unfolding conversion_def by (blast dest: rtrancl_trans)
next
case 2
then obtain u l' r' where l'r': "(l', r') ∈ R i"
and lv: "(l, u) ∈ R i" and rv: "(r, u) ∈ rstep {(l', r')}" by blast
then have "r ≻ u" and "r ⋅⊵ l'" and "l ≻ r" using ‹(l, r) ∈ R (i - 1)›
using run_R_less [THEN compatible_rstep_imp_less, of r u i] and run_R_less by auto
then have "(r, u) ∈ termless" and "(l, l') ∈ termless" by blast+
then have "((l, r), (l, u)) ∈ lexless" and "((l, r), (l', r')) ∈ lexless" by auto
with IH and l'r' and lv have "(l, u) ∈ ?L l" and "(l', r') ∈ ?L l'" by blast+
moreover obtain C and σ where "r = C⟨l' ⋅ σ⟩" and "u = C⟨r' ⋅ σ⟩" using rv by blast
ultimately have "(r, u) ∈ ?L r"
using slab_conv_below_ctxt_subst by auto
with ‹l ≻ r› have "(r, u) ∈ ?L l" using slab_conv_below_label by blast
then have "(u, r) ∈ ?L l" by (auto simp: conversion_inv)
with ‹(l, u) ∈ ?L l› show ?thesis unfolding conversion_def by (blast dest: rtrancl_trans)
qed
qed blast
qed
then show "(t, u) ∈ ?L l" by simp
qed
lemma slab_R_inf_subset:
"slab R⇩∞ s ⊆ (⋃t∈{t. s ≽ t}. slab R⇩ω t)⇧↔⇧*" (is "slab ?R s ⊆ ?L s")
proof
fix t u assume "(t, u) ∈ slab ?R s"
then obtain C σ l r where "(l, r) ∈ ?R"
and [simp]: "s = t" "t = C⟨l ⋅ σ⟩" "u = C⟨r ⋅ σ⟩" by fast
with source_step_R_inf_subset [of l]
have "(l, r) ∈ ?L l" by blast
from slab_conv_below_ctxt_subst [OF this] show "(t, u) ∈ ?L s" by simp
qed
lemma slab_R_inf_conv:
assumes "(t, u) ∈ (⋃a∈{a. s ≽ a}. slab R⇩∞ a)⇧↔⇧*"
shows "(t, u) ∈ (⋃a∈{a. s ≽ a}. slab R⇩ω a)⇧↔⇧*"
using assms
unfolding conversion_def
proof (induct)
case (step u v)
from step(2) obtain a where "s ≽ a" and "(u, v) ∈ (slab R⇩∞ a)⇧↔" by blast
with slab_R_inf_subset [of a]
have "(u, v) ∈ (⋃x∈{x. a ≽ x}. slab R⇩ω x)⇧↔⇧*" by (auto simp: conversion_inv)
with ‹s ≽ a› have "(u, v) ∈ (⋃x∈{x. s ≽ x}. slab R⇩ω x)⇧↔⇧*"
using slab_conv_below_label by blast
with step(3) show ?case by (auto simp: conversion_def)
qed simp
lemma rstep_R_inf_conv_iff:
"(rstep R⇩∞)⇧↔⇧* = (rstep R⇩ω)⇧↔⇧*"
proof
show "(rstep R⇩ω)⇧↔⇧* ⊆ (rstep R⇩∞)⇧↔⇧*"
using rstep_R_per_subset_rstep_R_inf
by (intro conversion_mono) auto
have "(rstep R⇩∞)⇧↔⇧* ⊆ (⋃s. slab R⇩∞ s)⇧↔⇧*"
by (intro conversion_mono) auto
also have "… ⊆ ((⋃s. slab R⇩ω s)⇧↔⇧*)⇧↔⇧*"
apply (intro conversion_mono)
apply (auto dest!: slab_R_inf_subset [THEN subsetD])
apply (rule conversion_mono [THEN subsetD])
apply auto
done
also have "… ⊆ ((rstep R⇩ω)⇧↔⇧*)⇧↔⇧*" by (intro conversion_mono) auto
finally show "(rstep R⇩∞)⇧↔⇧* ⊆ (rstep R⇩ω)⇧↔⇧*" by simp
qed
end
end
end