theory Conditional_Rewriting
imports
QTRS.Trs
"Check-NT.Reduction_Pair"
QTRS.Renaming_Interpretations
begin
type_synonym ('f, 'v) condition = "('f, 'v) term × ('f, 'v) term"
type_synonym ('f, 'v) crule = "('f, 'v) rule × ('f, 'v) condition list"
type_synonym ('f, 'v) ctrs = "('f, 'v) crule set"
text ‹A conditional rewrite step of level @{term n}.›
fun cstep_n :: "('f, 'v) ctrs ⇒ nat ⇒ ('f, 'v) term rel"
where
"cstep_n R 0 = {}" |
cstep_n_Suc: "cstep_n R (Suc n) =
{(C⟨l ⋅ σ⟩, C⟨r ⋅ σ⟩) | C l r σ cs.
((l, r), cs) ∈ R ∧ (∀ (s⇩i, t⇩i) ∈ set cs. (s⇩i ⋅ σ, t⇩i ⋅ σ) ∈ (cstep_n R n)⇧*)}"
definition conds_n_sat
where
conds_n_sat_iff: "conds_n_sat R n cs σ ⟷ (∀(s⇩i, t⇩i) ∈ set cs. (s⇩i ⋅ σ, t⇩i ⋅ σ) ∈ (cstep_n R n)⇧*)"
lemma conds_n_satD:
assumes "conds_n_sat R n cs σ" and "(s, t) ∈ set cs"
shows "(s ⋅ σ, t ⋅ σ) ∈ (cstep_n R n)⇧*"
using assms by (auto simp: conds_n_sat_iff)
lemma conds_n_sat_append [simp]:
"conds_n_sat R n (cs @ ds) σ ⟷ conds_n_sat R n cs σ ∧ conds_n_sat R n ds σ"
by (auto simp add: conds_n_sat_iff)
lemma conds_n_sat_Nil [simp]:
"conds_n_sat R n [] σ"
by (simp add: conds_n_sat_iff)
lemma conds_n_sat_singleton [simp]:
"conds_n_sat R n [c] σ ⟷ (fst c ⋅ σ, snd c ⋅ σ) ∈ (cstep_n R n)⇧*"
by (auto simp: conds_n_sat_iff)
lemma conds_n_sat_subst_list:
"conds_n_sat R n (subst_list σ cs) τ = conds_n_sat R n cs (σ ∘⇩s τ)"
by (auto simp: conds_n_sat_iff subst_set_def)
lemma cstep_n_SucI [Pure.intro?]:
assumes "((l, r), cs) ∈ R"
and "∀(s⇩i, t⇩i) ∈ set cs. (s⇩i ⋅ σ, t⇩i ⋅ σ) ∈ (cstep_n R n)⇧*"
and "s = C⟨l ⋅ σ⟩"
and "t = C⟨r ⋅ σ⟩"
shows "(s, t) ∈ cstep_n R (Suc n)"
using assms by (auto) blast
lemma cstep_nE:
assumes "(s, t) ∈ cstep_n R n"
obtains C l r σ cs n' where "((l, r), cs) ∈ R" and "n = Suc n'"
and "∀(s⇩i, t⇩i) ∈ set cs. (s⇩i ⋅ σ, t⇩i ⋅ σ) ∈ (cstep_n R n')⇧*"
and "s = C⟨l ⋅ σ⟩"
and "t = C⟨r ⋅ σ⟩"
using assms by (cases n) auto
lemma cstep_n_SucE:
assumes "(s, t) ∈ cstep_n R (Suc n)"
obtains C l r σ cs where "((l, r), cs) ∈ R"
and "∀(s⇩i, t⇩i) ∈ set cs. (s⇩i ⋅ σ, t⇩i ⋅ σ) ∈ (cstep_n R n)⇧*"
and "s = C⟨l ⋅ σ⟩"
and "t = C⟨r ⋅ σ⟩"
using assms by auto
declare cstep_n_Suc [simp del]
lemma cstep_n_Suc_mono:
"cstep_n R n ⊆ cstep_n R (Suc n)"
proof (induct n)
case (Suc n)
show ?case
using rtrancl_mono [OF Suc] by (auto elim!: cstep_n_SucE intro!: cstep_n_SucI)
qed simp
lemma cstep_n_mono:
assumes "i ≤ n"
shows "cstep_n R i ⊆ cstep_n R n"
using assms
proof (induct "n - i" arbitrary: i)
case (Suc k)
then have "k = n - Suc i" and "Suc i ≤ n" by arith+
from Suc.hyps(1) [OF this] show ?case using cstep_n_Suc_mono by blast
qed simp
lemma csteps_n_mono:
assumes "m ≤ n"
shows "(cstep_n R m)⇧* ⊆ (cstep_n R n)⇧*"
using assms by (intro rtrancl_mono cstep_n_mono)
lemma conds_n_sat_mono:
"m ≤ n ⟹ conds_n_sat R m cs σ ⟹ conds_n_sat R n cs σ"
using csteps_n_mono [of m n R]
by (auto simp: conds_n_sat_iff)
lemma cstep_n_mono':
"cstep_n R m ⊆ cstep_n R (m + k)"
using cstep_n_mono [of "m" "m + k"] by simp
lemma cstep_n_ctxt:
assumes "(s, t) ∈ cstep_n R n"
shows "(C⟨s⟩, C⟨t⟩) ∈ cstep_n R n"
using assms by (cases n) (auto elim!: cstep_n_SucE intro: cstep_n_SucI [where C = "C ∘⇩c D" for D])
lemma all_ctxt_closed_csteps_n [intro]:
"all_ctxt_closed UNIV ((cstep_n R n)⇧*)"
by (rule trans_ctxt_imp_all_ctxt_closed)
(auto simp: ctxt.closed_def elim!: ctxt.closure.cases intro: trans_rtrancl refl_rtrancl cstep_n_ctxt [THEN rtrancl_map])
lemma cstep_n_subst:
assumes "(s, t) ∈ cstep_n R n"
shows "(s ⋅ σ, t ⋅ σ) ∈ cstep_n R n"
using assms
proof (induct n arbitrary: s t σ)
case (Suc n)
from ‹(s, t) ∈ cstep_n R (Suc n)› obtain C l r cs τ
where "((l, r), cs) ∈ R" and "∀(s⇩i, t⇩i) ∈ set cs. (s⇩i ⋅ τ, t⇩i ⋅ τ) ∈ (cstep_n R n)⇧*"
and "s = C⟨l ⋅ τ⟩" and "t = C⟨r ⋅ τ⟩" by (rule cstep_n_SucE)
then show ?case
using Suc.hyps and rtrancl_map [of "cstep_n R n" "λt. t ⋅ σ"]
by (auto intro!: cstep_n_SucI [of l r cs R "τ ∘⇩s σ" _ _ "C ⋅⇩c σ"])
qed simp
lemma cstep_n_ctxt_subst:
assumes "(s, t) ∈ cstep_n R n"
shows "(D ⟨s ⋅ σ⟩, D ⟨t ⋅ σ⟩) ∈ cstep_n R n"
by (intro cstep_n_ctxt cstep_n_subst) fact
definition "cstep R = (⋃n. cstep_n R n)"
lemma cstep_iff:
"(s, t) ∈ cstep R ⟷ (∃n. (s, t) ∈ cstep_n R n)"
by (auto simp: cstep_def)
definition conds_sat
where
conds_sat_iff: "conds_sat R cs σ ⟷ (∀(s⇩i, t⇩i) ∈ set cs. (s⇩i ⋅ σ, t⇩i ⋅ σ) ∈ (cstep R)⇧*)"
lemma conds_sat_subst_list:
"conds_sat R (subst_list σ cs) τ = conds_sat R cs (σ ∘⇩s τ)"
by (auto simp: conds_sat_iff subst_set_def)
lemma conds_sat_append [simp]:
"conds_sat R (cs⇩1 @ cs⇩2) σ ⟷ conds_sat R cs⇩1 σ ∧ conds_sat R cs⇩2 σ"
by (auto simp: conds_sat_iff)
lemma NF_cstep_subterm:
assumes "t ∈ NF (cstep R)" and "t ⊵ s"
shows "s ∈ NF (cstep R)"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain u where "(s, u) ∈ cstep R" by auto
from ‹t ⊵ s› obtain C where "t = C⟨s⟩" by auto
with ‹(s, u) ∈ cstep R› have "(t, C⟨u⟩) ∈ cstep R"
using cstep_iff cstep_n_ctxt by blast
hence "t ∉ NF (cstep R)" by auto
with assms show False by simp
qed
lemma cstep_n_empty [simp]: "cstep_n {} n = {}"
by (induct n) (auto simp: cstep_n_Suc)
lemma cstep_empty [simp]: "cstep {} = {}"
unfolding cstep_def by simp
lemma csteps_n_trans:
assumes "(s, t) ∈ (cstep_n R m)⇧*" and "(t, u) ∈ (cstep_n R n)⇧*"
shows "(s, u) ∈ (cstep_n R (max m n))⇧*"
using assms
and cstep_n_mono [of m "max m n" R, THEN rtrancl_mono]
and cstep_n_mono [of n "max m n" R, THEN rtrancl_mono]
by (auto dest!: set_mp)
lemma csteps_imp_csteps_n:
assumes "(s, t) ∈ (cstep R)⇧*"
shows "∃n. (s, t) ∈ (cstep_n R n)⇧*"
using assms by (induct) (auto intro: csteps_n_trans simp: cstep_iff)
lemma cstep_n_imp_cstep:
assumes "(s, t) ∈ cstep_n R n"
shows "(s, t) ∈ cstep R"
using assms by (auto simp: cstep_iff)
lemma csteps_n_imp_csteps:
assumes "(s, t) ∈ (cstep_n R n)⇧*"
shows "(s, t) ∈ (cstep R)⇧*"
using assms by (induct; auto dest: cstep_n_imp_cstep)
lemma csteps_n_subset_csteps:
"(cstep_n R n)⇧* ⊆ (cstep R)⇧*"
by (auto dest: csteps_n_imp_csteps)
lemma all_cstep_imp_cstep_n:
assumes "∀i < (k::nat). (s⇩i i, t⇩i i) ∈ (cstep R)⇧*"
shows "∃n. ∀i < k. (s⇩i i, t⇩i i) ∈ (cstep_n R n)⇧*" (is "∃n. ∀i < k. ?P i n")
proof -
have "∀i < k. ∃n⇩i. ?P i n⇩i"
using assms by (auto intro: csteps_imp_csteps_n)
then obtain f where *: "∀i < k. ?P i (f i)" by metis
define n where "n ≡ Max (set (map f [0 ..< k]))"
have "∀i < k. f i ≤ n" by (auto simp: n_def)
then have "∀i < k. ?P i n"
using cstep_n_mono [of "f i" n R for i, THEN rtrancl_mono] and * by blast
then show ?thesis ..
qed
lemma cstepI:
assumes "((l, r), cs) ∈ R"
and conds: "∀(s⇩i, t⇩i) ∈ set cs. (s⇩i ⋅ σ, t⇩i ⋅ σ) ∈ (cstep R)⇧*"
and "s = C⟨l ⋅ σ⟩"
and "t = C⟨r ⋅ σ⟩"
shows "(s, t) ∈ cstep R"
proof -
obtain n where "∀(s⇩i, t⇩i) ∈ set cs. (s⇩i ⋅ σ, t⇩i ⋅ σ) ∈ (cstep_n R n)⇧*"
using all_cstep_imp_cstep_n[of "length cs" "λi. fst (cs ! i) ⋅ σ" "λi. snd (cs ! i) ⋅ σ" R]
and conds
by (auto simp: all_set_conv_all_nth split_beta')
then have "(s, t) ∈ cstep_n R (Suc n)" using assms by (intro cstep_n_SucI) (assumption)+
then show ?thesis using cstep_iff by auto
qed
lemma cstepE [elim]:
assumes "(s, t) ∈ cstep R"
and imp: "⋀C σ l r cs. ⟦((l, r), cs) ∈ R; ∀(s⇩i, t⇩i) ∈ set cs. (s⇩i ⋅ σ, t⇩i ⋅ σ) ∈ (cstep R)⇧*; s = C⟨l ⋅ σ⟩; t = C⟨r ⋅ σ⟩⟧ ⟹ P"
shows "P"
proof -
obtain n where *: "(s, t) ∈ cstep_n R n" using assms by (auto simp: cstep_iff)
then show ?thesis
proof (cases n)
case (Suc n')
have **: "(cstep_n R n')⇧* ⊆ (cstep R)⇧*" by (rule rtrancl_mono) (auto simp: cstep_iff)
show ?thesis
by (rule cstep_n_SucE [OF * [unfolded Suc]], rule imp, insert **) auto
qed simp
qed
lemma Var_NF_cstep:
assumes "∀ ((l, r), cs) ∈ R. is_Fun l"
shows "Var x ∈ NF (cstep R)"
proof
fix s
show "(Var x, s) ∉ cstep R"
proof
assume "(Var x, s) ∈ cstep R"
then show "False" using assms supteq_var_imp_eq by fastforce
qed
qed
lemma cstep_ctxt_closed:
"ctxt.closed (cstep R)"
by (rule ctxt.closedI) (auto intro: cstep_n_ctxt simp: cstep_iff)
lemma csteps_all_ctxt_closed[intro]: "all_ctxt_closed UNIV ((cstep r)^*)"
using cstep_ctxt_closed by (blast intro: trans_ctxt_imp_all_ctxt_closed trans_rtrancl refl_rtrancl)
lemma join_csteps_all_ctxt_closed: "all_ctxt_closed UNIV ((cstep r)⇧↓)"
proof -
have var:"∀x. (Var x, Var x) ∈ (cstep r)⇧↓" by fast
{ fix f ss ts
assume a:"length ts = length ss" "∀i<length ts. (ts ! i, ss ! i) ∈ (cstep r)⇧↓"
from a(2) have "∀i<length ts. ∃ ui. (ts ! i, ui)∈ (cstep r)^* ∧ (ss ! i, ui) ∈ (cstep r)^*" by blast
with choice have "∃ui. ∀i<length ts. (ts ! i, ui i)∈ (cstep r)^* ∧ (ss ! i, ui i) ∈ (cstep r)^*" by meson
then obtain ui where ui:"⋀i. i<length ts ⟹ (ts ! i, ui i)∈ (cstep r)^* ∧ (ss ! i, ui i) ∈ (cstep r)^*" by blast
let ?us = "map ui [0 ..<length ts]"
have lus: "length ts = length ?us" by simp
from ui have uss:"⋀j. j < length ts ⟹ (ss ! j, ?us ! j) ∈ (cstep r)^*" by auto
from ui have ust:"⋀j. j < length ts ⟹ (ts ! j, ?us ! j) ∈ (cstep r)^*" by auto
note acc = conjunct1[OF csteps_all_ctxt_closed[unfolded all_ctxt_closed_def], rule_format]
from acc[OF _ lus ust] have tseq:"(Fun f ts, Fun f ?us) ∈ (cstep r)⇧*" by blast
from acc[OF _ lus[unfolded a(1)] uss[unfolded a(1)]] a(1) have sseq:"(Fun f ss, Fun f ?us) ∈ (cstep r)⇧*" by force
with tseq have "(Fun f ts, Fun f ss) ∈ (cstep r)⇧↓" by blast
}
with var show ?thesis unfolding all_ctxt_closed_def by auto
qed
abbreviation clhs :: "('f, 'v) crule ⇒ ('f, 'v) term"
where
"clhs ρ ≡ fst (fst ρ)"
abbreviation crhs :: "('f, 'v) crule ⇒ ('f, 'v) term"
where
"crhs ρ ≡ snd (fst ρ)"
definition X_vars :: "('f, 'v) crule ⇒ nat ⇒ 'v set"
where
"X_vars ρ i = vars_term (clhs ρ) ∪ ⋃(vars_term ` rhss (set (take i (snd ρ))))"
lemma X_vars_mono:
"i ≤ j ⟹ X_vars ρ i ⊆ X_vars ρ j"
by (fastforce simp: X_vars_def dest: set_take_subset_set_take)
definition Y_vars ::"('f, 'v) crule ⇒ nat ⇒ 'v set"
where
"Y_vars ρ i =
vars_term (crhs ρ) ∪ vars_term (snd (snd ρ ! i)) ∪ (vars_trs (set (drop (Suc i) (snd ρ))))"
lemma X_vars_alt :
assumes "i ≤ length (snd ρ)"
shows "X_vars ρ i = vars_term (clhs ρ) ∪ ⋃((λj. vars_term (snd (snd ρ ! j))) ` {j. j < i})"
proof -
let ?L = "⋃(vars_term ` (rhss (set (List.take i (snd ρ)))))"
let ?R = "⋃((λj. vars_term (snd (snd ρ ! j))) ` {j. j < i})"
{ fix x
assume "x ∈ ?L"
hence "∃j. j < i ∧ x ∈ vars_term (snd ((snd ρ) ! j))" unfolding set_conv_nth using nth_take[of _ i "snd ρ"] by fastforce
then obtain j where j:"j < i" and x:"x ∈ vars_term (snd (snd ρ ! j))" by blast
hence "x ∈ ?R" by blast
} hence *: "?L ⊆ ?R" by auto
{ fix x
assume "x ∈ ?R"
hence "∃j. j < i ∧ x ∈ vars_term (snd ((snd ρ) ! j))" by blast
then obtain j where j:"j < i" and x:"x ∈ vars_term (snd (snd ρ ! j))" by blast
hence "x ∈ vars_term (snd (take i (snd ρ) ! j))" using nth_take[OF j(1)] by force
with j(1) have "x ∈ ?L" unfolding set_conv_nth length_take min_absorb2[OF assms] by blast
} hence "?R ⊆ ?L" by auto
with * have *:"?L = ?R" by blast
show ?thesis unfolding X_vars_def * by blast
qed
lemma set_drop_nth: "set (drop i xs) = {xs ! j | j. j ≥ i ∧ j < length xs}"
proof -
{
fix j
have "i ≤ j ⟹ j < length xs ⟹ ∃ia. xs ! j = drop i xs ! ia ∧ ia < length xs - i"
by (metis diff_less_mono le_add_diff_inverse less_or_eq_imp_le nth_drop)
}
thus ?thesis unfolding set_conv_nth by auto
qed
lemma Y_vars_alt :
assumes i: "i < length (snd ρ)"
shows "Y_vars ρ i = vars_term (crhs ρ) ∪
⋃ {vars_term (fst (snd ρ ! j)) | j. i < j ∧ j < length (snd ρ)} ∪
⋃ {vars_term (snd (snd ρ ! j)) | j. i ≤ j ∧ j < length (snd ρ)}"
(is "_ = ?A ∪ ?B ∪ ?C")
proof -
{
fix x
have "(x ∈ Y_vars ρ i) = (x ∈ ?A ∨ x ∈ vars_term (snd (snd ρ ! i))
∨ x ∈ vars_trs (set (drop (Suc i) (snd ρ))))" (is "_ = (_ ∨ x ∈ ?B' ∨ x ∈ ?C')")
unfolding Y_vars_def by auto
also have "?C' = UNION (set (drop (Suc i) (snd ρ))) vars_rule" unfolding vars_trs_def by auto
also have "set (drop (Suc i) (snd ρ)) = {snd ρ ! j | j. j ≥ Suc i ∧ j < length (snd ρ)}"
(is "_ = ?C''") unfolding set_drop_nth ..
also have "(x ∈ ?B' ∨ x ∈ UNION ?C'' vars_rule) = (x ∈ ?B ∪ ?C)"
proof -
{
assume "x ∈ ?B'"
hence "x ∈ ?C" using i by auto
} moreover {
assume "x ∈ UNION ?C'' vars_rule"
then obtain j where "x ∈ vars_rule (snd ρ ! j)"
and *: "j > i" "j ≥ i" "j < length (snd ρ)" by auto
hence "x ∈ vars_term (fst (snd ρ ! j)) ∪ vars_term (snd (snd ρ ! j))"
by (auto simp: vars_rule_def)
with * have "x ∈ ?B ∪ ?C" by blast
} moreover {
assume "x ∈ ?B"
then obtain j where "x ∈ vars_term (fst (snd ρ ! j))"
and *: "Suc i ≤ j" "j < length (snd ρ)" by auto
hence "x ∈ vars_rule (snd ρ ! j)"
by (auto simp: vars_rule_def)
with * have "x ∈ UNION ?C'' vars_rule" by blast
} moreover {
assume "x ∈ ?C"
then obtain j where xx: "x ∈ vars_term (snd (snd ρ ! j))"
and *: "i ≤ j" "j < length (snd ρ)" by auto
hence x: "x ∈ vars_rule (snd ρ ! j)"
by (auto simp: vars_rule_def)
have "x ∈ ?B' ∪ UNION ?C'' vars_rule"
proof (cases "j = i")
case False
with * have "Suc i ≤ j" by auto
with * x show ?thesis by blast
qed (insert xx, auto)
}
ultimately show ?thesis by blast
qed
finally have "(x ∈ Y_vars ρ i) = (x ∈ ?A ∪ ?B ∪ ?C)" by auto
}
thus ?thesis by blast
qed
definition type3 :: "('f, 'v) ctrs ⇒ bool"
where
"type3 R ⟷ (∀ ρ ∈ R. vars_term (crhs ρ) ⊆ (vars_term (clhs ρ) ∪ vars_trs (set (snd ρ))))"
definition dctrs :: "('f, 'v) ctrs ⇒ bool"
where
"dctrs R ⟷ (∀ ρ ∈ R. ∀ i < length (snd ρ). vars_term (fst (snd ρ ! i)) ⊆ X_vars ρ i)"
definition wf_ctrs :: "('f, 'v) ctrs ⇒ bool"
where
"wf_ctrs R ⟷ (∀((l, r), cs) ∈ R. is_Fun l) ∧ type3 R ∧ dctrs R"
definition funs_crule :: "('f, 'v) crule ⇒ 'f set"
where
"funs_crule ρ = funs_rule (fst ρ) ∪ funs_trs (set (snd ρ))"
definition funas_crule :: "('f, 'v) crule ⇒ ('f × nat) set"
where
"funas_crule ρ = funas_rule (fst ρ) ∪ funas_trs (set (snd ρ))"
definition funs_ctrs :: "('f, 'v) ctrs ⇒ 'f set"
where
"funs_ctrs R = ⋃(funs_crule ` R)"
definition funas_ctrs :: "('f, 'v) ctrs ⇒ ('f × nat) set"
where
"funas_ctrs R = ⋃(funas_crule ` R)"
definition vars_crule :: "('f, 'v) crule ⇒ 'v set"
where
"vars_crule ρ = vars_rule (fst ρ) ∪ vars_trs (set (snd ρ))"
definition vars_ctrs :: "('f, 'v) ctrs ⇒ 'v set"
where
"vars_ctrs R = ⋃(vars_crule ` R)"
text ‹The underlying unconditional TRS›
definition Ru :: "('f, 'v) ctrs ⇒ ('f, 'v) trs"
where
"Ru R = fst ` R"
lemma defined_R_imp_Ru: "root l = Some fn ⟹ ((l, r), cs) ∈ R ⟹ defined (Ru R) fn"
by (force simp: Ru_def defined_def)
lemma cstep_imp_Ru_step: "(cstep R) ⊆ (rstep (Ru R))"
proof
fix s t
assume "(s,t) ∈ cstep R"
with cstep_iff cstep_n.simps(1) obtain n where n:"(s,t) ∈ cstep_n R (Suc n)"
by (metis empty_iff not0_implies_Suc)
hence "∃C l r σ cs. (s,t) = (C⟨l ⋅ σ⟩, C⟨r ⋅ σ⟩) ∧ ((l,r),cs) ∈ R" unfolding Ru_def cstep_n.simps(2) by fast
hence *:"∃C l r σ. (s,t) = (C⟨l ⋅ σ⟩, C⟨r ⋅ σ⟩) ∧ (l,r) ∈ Ru R" unfolding Ru_def by force
with rule rstep_r_p_s_imp_rstep * rstep_r_p_s_def show "(s,t) ∈ rstep (Ru R)" by fast
qed
lemma Ru_NF_imp_R_NF: "t ∈ NF (rstep (Ru R)) ⟹ t ∈ NF (cstep R)"
using NF_anti_mono [OF cstep_imp_Ru_step] by blast
lemma funas_ctrs_cond:
assumes rho:"ρ ∈ R" and i:"i < length (snd ρ)" shows "funas_rule (snd ρ ! i) ⊆ funas_ctrs R"
using assms funas_crule_def unfolding funas_ctrs_def funas_trs_def set_conv_nth by blast
lemma wf_ctrs_steps_preserves_funas:
assumes wf: "wf_ctrs R" and s: "funas_term s ⊆ F" and R: "funas_ctrs R ⊆ F"
and st:"(s, t) ∈ (cstep R)⇧*"
shows "funas_term t ⊆ F"
proof-
from wf[unfolded wf_ctrs_def] have t3:"type3 R" and dctrs:"dctrs R" by auto
let ?rfuns = "λ v. funas_term v ⊆ F"
from rtrancl_power csteps_imp_csteps_n[OF st] obtain n k where st':"(s,t) ∈ (cstep_n R n) ^^ k" by blast
let ?P = "λ (n,k). ∀ s t. ?rfuns s ⟶ (s,t) ∈ (cstep_n R n) ^^ k ⟶ ?rfuns t"
have "?P (n,k)" proof(induct rule: wf_induct[OF wf_measures, of "[fst, snd]" ?P])
case (1 nk) note ind = this
obtain n k where nk: "nk = (n,k)" by force
{ fix s t
assume s:"?rfuns s" and st:"(s, t) ∈ (cstep_n R n) ^^ k"
hence "?rfuns t" proof(cases k)
case 0
with s st show ?thesis by simp
next
case (Suc m)
from relpow_Suc_E[OF st[unfolded Suc]] obtain u where u:"(s,u) ∈ (cstep_n R n) ^^ m" "(u,t) ∈ cstep_n R n" by blast
have "((n,m), nk) ∈ measures [fst, snd]" unfolding nk Suc by auto
from ind[rule_format, OF this, unfolded split, rule_format, OF s u(1)] have fu:"?rfuns u" by auto
show ?thesis proof (cases n)
case 0
from u(2)[unfolded 0 cstep_n.simps] show ?thesis by auto
next
case (Suc n)
from u(2)[unfolded Suc cstep_n.simps] obtain C l r σ cs where step:"(u,t) = (C⟨l ⋅ σ⟩, C⟨r ⋅ σ⟩)"
"((l, r), cs) ∈ R" "∀(s⇩i, t⇩i)∈set cs. (s⇩i ⋅ σ, t⇩i ⋅ σ) ∈ (cstep_n R n)⇧*" by force
from this(1) fu have fl:"?rfuns (l ⋅ σ)" by auto
with supteq_imp_funas_term_subset supteq_Var
have fx:"⋀x. x ∈ vars_term l ⟹ ?rfuns (σ x)" by fastforce
{ fix i
assume i:"i < length cs"
let ?stm = " λ m. (fst (cs ! m) ⋅ σ, snd (cs ! m) ⋅ σ)"
from i have "funas_rule (?stm i) ⊆ F" proof (induct i rule:nat_less_induct)
fix i
assume ind2:"∀m<i. (m < length cs ⟶ funas_rule (?stm m) ⊆ F)" and i:"i < length cs"
from dctrs[unfolded dctrs_def, rule_format, OF step(2), of i] i have
vs:"vars_term (fst (cs ! i)) ⊆ vars_term l ∪ X_vars ((l, r), cs) i" by auto
{ fix j x
assume "x ∈ ⋃(vars_term ` rhss (set (take i cs)))"
hence "∃j. j < i ∧ x ∈ vars_term (snd (cs ! j))" unfolding set_conv_nth using nth_take[of _ i cs] by fastforce
then obtain j where j:"j < i" and x:"x ∈ vars_term (snd (cs ! j))" by blast
from ind2[rule_format, OF j] i j have "funas_term (snd (cs ! j) ⋅ σ) ⊆ F" unfolding funas_rule_def by auto
with x supteq_imp_funas_term_subset supteq_Var have "?rfuns (σ x)" by fastforce
} note vt = this
{ fix x assume "x ∈ vars_term (fst (cs ! i))"
with vs[unfolded X_vars_def] fx vt have "?rfuns (σ x)" by auto
}
with funas_ctrs_cond[OF step(2), unfolded snd_conv, OF i] R have lhs:"?rfuns (fst (cs ! i) ⋅ σ)"
unfolding funas_term_subst funas_rule_def by blast
from i have "(fst (cs ! i), snd (cs ! i)) ∈ set cs" by auto
from step(3)[rule_format, OF this, unfolded split] obtain l where
st:"(fst (cs ! i) ⋅ σ, snd (cs ! i) ⋅ σ) ∈ (cstep_n R n) ^^ l" unfolding rtrancl_power by blast
have "((n,l), nk) ∈ measures [fst, snd]" unfolding nk Suc by auto
from ind[rule_format, OF this, unfolded split, rule_format, OF lhs st]
have rhs:"funas_term (snd (cs ! i) ⋅ σ) ⊆ F" by auto
from lhs rhs show "funas_rule (?stm i) ⊆ F" unfolding funas_rule_def by auto
qed
} note aux = this
from t3[unfolded type3_def, rule_format, OF step(2)]
have vr:"vars_term r ⊆ vars_term l ∪ vars_trs (set cs )" by auto
from funas_rule_def[of "(l,r)"] have "funas_term r ⊆ funas_crule ((l, r), cs)" unfolding funas_crule_def by auto
with step(2) have fr:"funas_term r ⊆ funas_ctrs R" unfolding funas_ctrs_def by auto
{ fix j x
assume j:"j < length cs" and "x ∈ vars_rule (cs ! j)"
with supteq_Var have "fst (cs ! j) ⊵ Var x ∨ snd (cs ! j) ⊵ Var x" unfolding vars_rule_def by fastforce
hence x:"fst (cs ! j) ⋅ σ ⊵ Var x ⋅ σ ∨ snd (cs ! j) ⋅ σ ⊵ Var x ⋅ σ" by auto
from aux j have "funas_rule (fst (cs ! j) ⋅ σ, snd (cs ! j) ⋅ σ) ⊆ F" unfolding funas_rule_def by auto
with x supteq_imp_funas_term_subset have "?rfuns (σ x)" unfolding funas_rule_def by force
}
with vr[unfolded set_conv_nth vars_trs_def] fx have "⋀x. x ∈ vars_term r ⟹ ?rfuns (σ x)" by blast
with step(2) fr R have lhs:"?rfuns (r ⋅ σ)" unfolding funas_term_subst funas_rule_def by blast
from step(1) have t:"t = C⟨r ⋅ σ⟩" and u:"u = C⟨l ⋅ σ⟩" by (fast,fast)
from lhs fu show "?rfuns t" unfolding t u by auto
qed
qed
}
thus ?case unfolding nk split by blast
qed
from this[unfolded split, rule_format, OF s st'] show ?thesis by auto
qed
lemma funs_crule_funas_crule:
"funs_crule r = fst ` funas_crule r"
unfolding funs_crule_def funas_crule_def funs_trs_funas_trs funs_rule_funas_rule by blast
lemma funs_ctrs_funas_ctrs:
"funs_ctrs R = fst ` funas_ctrs R"
proof -
from funs_crule_funas_crule have "⋃(funs_crule ` R) = ⋃(((λx. fst ` x) ∘ funas_crule) ` R)" by (metis comp_apply)
thus ?thesis unfolding funs_ctrs_def funas_ctrs_def image_Union by force
qed
lemma wf_ctrs_steps_preserves_funs:
assumes wf: "wf_ctrs R" and s: "funs_term s ⊆ F"
and R: "funs_ctrs R ⊆ F" and st: "(s, t) ∈ (cstep R)⇧*"
shows "funs_term t ⊆ F"
proof -
from s R wf_ctrs_steps_preserves_funas[OF wf _ _ st, of "F × UNIV"]
show ?thesis unfolding funs_term_funas_term funs_ctrs_funas_ctrs by fastforce
qed
lemma cstep_map_funs_term:
assumes R: "⋀ f. f ∈ funs_ctrs R ⟹ h f = f" and "(s, t) ∈ cstep R"
shows "(map_funs_term h s, map_funs_term h t) ∈ cstep R"
proof -
let ?h = "map_funs_term h"
from assms[unfolded cstep_def] obtain n where "(s,t) ∈ cstep_n R n" by auto
hence "(?h s, ?h t) ∈ cstep_n R n"
proof (induct n arbitrary: s t)
case (Suc n)
from cstep_n_SucE[OF Suc(2)]
obtain C l r σ cs
where rule: "((l,r), cs) ∈ R" and cs: "∀(s⇩i, t⇩i)∈set cs. (s⇩i ⋅ σ, t⇩i ⋅ σ) ∈ (cstep_n R n)⇧*"
and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩" .
let ?σ = "map_funs_subst h σ"
note funs_defs = funs_ctrs_def funs_crule_def[abs_def] funs_rule_def[abs_def] funs_trs_def
from rule have lr: "funs_term l ∪ funs_term r ⊆ funs_ctrs R" unfolding funs_defs
by auto
have hl: "?h l = l"
by (rule funs_term_map_funs_term_id[OF R], insert lr, auto)
have hr: "?h r = r"
by (rule funs_term_map_funs_term_id[OF R], insert lr, auto)
show ?case unfolding s t
unfolding map_funs_subst_distrib map_funs_term_ctxt_distrib hl hr
proof (rule cstep_n_SucI[OF rule _ refl refl], rule)
fix s⇩i t⇩i
assume in_cs: "(s⇩i,t⇩i) ∈ set cs"
from in_cs rule have st: "funs_term s⇩i ∪ funs_term t⇩i ⊆ funs_ctrs R" unfolding funs_defs by force
have hs: "?h s⇩i = s⇩i"
by (rule funs_term_map_funs_term_id[OF R], insert st, auto)
have ht: "?h t⇩i = t⇩i"
by (rule funs_term_map_funs_term_id[OF R], insert st, auto)
from in_cs cs have steps: "(s⇩i ⋅ σ, t⇩i ⋅ σ) ∈ (cstep_n R n)⇧*" by auto
have "(?h (s⇩i ⋅ σ), ?h (t⇩i ⋅ σ)) ∈ (cstep_n R n)⇧*"
by (rule rtrancl_map[OF Suc(1) steps])
thus "(s⇩i ⋅ ?σ, t⇩i ⋅ ?σ) ∈ (cstep_n R n)⇧*" unfolding map_funs_subst_distrib hs ht .
qed
qed simp
thus ?thesis unfolding cstep_def by auto
qed
definition normalized :: "('f, 'v) ctrs ⇒ ('f, 'v) subst ⇒ bool"
where
"normalized R σ ⟷ (∀x. σ x ∈ NF (cstep R))"
lemma empty_subst_normalized:
assumes "∀((l, r), cs) ∈ R. is_Fun l"
shows "normalized R Var"
by (simp add: Var_NF_cstep assms normalized_def)
definition "strongly_irreducible R t ⟷ (∀σ. normalized R σ ⟶ t ⋅ σ ∈ NF (cstep R))"
lemma strongly_irreducible_I [Pure.intro?]:
assumes "⋀σ. normalized R σ ⟹ t ⋅ σ ∈ NF (cstep R)"
shows "strongly_irreducible R t"
using assms by (auto simp add: strongly_irreducible_def)
lemma Var_strongly_irreducible_cstep:
"∀ ((l, r), cs) ∈ R. is_Fun l ⟹ strongly_irreducible R (Var x)"
by (rule strongly_irreducible_I) (simp add: normalized_def)
lemma constructor_term_imp_strongly_irreducible:
fixes t R
assumes varcond: "∀((l, r), cs) ∈ R. is_Fun l"
and constr: "funas_term t ⊆ funas_ctrs R - { f. defined (Ru R) f }"
shows "strongly_irreducible R t"
using constr
proof (induction t)
case (Var x)
show ?case using varcond Var_strongly_irreducible_cstep[of R x] by simp
next
case (Fun f ts)
show ?case
proof
fix σ
assume norm: "normalized R σ"
show "Fun f ts ⋅ σ ∈ NF (cstep R)"
proof
fix s
show "(Fun f ts ⋅ σ, s) ∉ cstep R"
proof
assume "(Fun f ts ⋅ σ, s) ∈ cstep R"
with cstepE [of "Fun f ts ⋅ σ" s "R"] obtain C τ l r cs
where "((l, r), cs) ∈ R" and "Fun f ts ⋅ σ = C⟨l ⋅ τ⟩" and "s = C⟨r ⋅ τ⟩"
and "∀(s⇩i, t⇩i)∈set cs. (s⇩i ⋅ τ, t⇩i ⋅ τ) ∈ (cstep R)⇧*" by auto
from varcond ‹((l, r), cs) ∈ R› Ru_def have "is_Fun l" by fastforce
show "False"
proof (cases C)
case (Hole)
with ‹Fun f ts ⋅ σ = C⟨l ⋅ τ⟩› have "Fun f ts ⋅ σ = l ⋅ τ" by auto
with ‹is_Fun l› ‹((l, r), cs) ∈ R›
have "(f, length ts) ∈ {f. defined (Ru R) f}"
using map_eq_imp_length_eq [of "λt. t ⋅ σ" ts]
by (cases l) (force intro: defined_R_imp_Ru)+
with Fun.prems show "False" by auto
next
case (More g lts D rts)
{
fix u
assume "u ∈ set ts"
then have "funas_term u ⊆ funas_term (Fun f ts)" by auto
with Fun.prems have "funas_term u ⊆ funas_ctrs R - {f. defined (Ru R) f}" by auto
}
note * = this
{
fix u
assume "u ∈ set ts"
from * [OF this] and Fun.IH[OF this]
have "strongly_irreducible R u" by auto
}
note IH = this
from More ‹Fun f ts ⋅ σ = C⟨l ⋅ τ⟩› have "map (λt. t ⋅ σ) ts = lts @ D⟨l ⋅ τ⟩ # rts" by simp
then obtain u where u: "u ∈ set ts" and "u ⋅ σ = D⟨l ⋅ τ⟩"
by (induct ts arbitrary: lts rts) (auto simp: Cons_eq_append_conv)
then have "u ⋅ σ ⊵ l ⋅ τ" by simp
then show "False"
proof (cases rule: supteq_subst_cases)
note supteq_imp_funas_term_subset [simp del]
case (in_term v)
with ‹is_Fun l› and * [OF u] and defined_R_imp_Ru[OF _ ‹((l, r), cs) ∈ R›]
show ?thesis
using supteq_imp_funas_term_subset [OF ‹u ⊵ v›] and map_eq_imp_length_eq
by (cases l; cases v) (fastforce)+
next
have "(l ⋅ τ, r ⋅ τ) ∈ cstep R" by (rule cstepI [of _ _ _ _ _ _ □], fact+) (simp_all)
moreover
case (in_subst x)
ultimately show ?thesis using norm NF_cstep_subterm[of "σ x" R "l ⋅ τ"]
by (auto simp: normalized_def)
qed
qed
qed
qed
qed
qed
lemma strongly_irreducible_imp_NF:
assumes vc: "∀((l, r), cs) ∈ R. is_Fun l"
and si: "strongly_irreducible R t"
shows "t ∈ NF (cstep R)"
by (metis empty_subst_normalized si strongly_irreducible_def subst_apply_term_empty vc)
lemma constructor_term_NF_cstep:
assumes varcond: "∀((l, r), cs) ∈ R. is_Fun l"
and constr: "funas_term t ⊆ funas_ctrs R - { f. defined (Ru R) f}"
shows "t ∈ NF (cstep R)"
by (auto simp: assms constructor_term_imp_strongly_irreducible strongly_irreducible_imp_NF)
lemma ground_Ru_NF_imp_strongly_irreducible:
assumes varcond: "∀((l, r), cs) ∈ R. is_Fun l"
and ground: "ground t"
and ru_nf: "t ∈ NF (rstep (Ru R))"
shows "strongly_irreducible R t"
using ground ru_nf
proof (induction t)
case (Fun f ts)
from Fun.prems(1) have "∀σ. Fun f ts ⋅ σ = Fun f ts"
using ground_subst_apply by blast
then show ?case
using Fun.prems(2) Ru_NF_imp_R_NF [of "Fun f ts" R] strongly_irreducible_I[of R "Fun f ts"]
by fastforce
qed simp
context
fixes R :: "('f, 'v) ctrs"
assumes vc: "∀((l, r), cs) ∈ R. is_Fun l"
begin
lemma syntactic_det_imp_strong_det:
assumes "(∀ ((l, r), cs) ∈ R. ∀ (s⇩i, t⇩i) ∈ set cs.
((funas_term t⇩i ⊆ ((funas_ctrs R) - { f. defined (Ru R) f }) ∨
(ground t⇩i ∧ t⇩i ∈ NF (rstep (Ru R))))))"
shows str_det: "(∀ ((l, r), cs) ∈ R. ∀ (s⇩i, t⇩i) ∈ set cs. strongly_irreducible R t⇩i)"
proof -
{
fix l r cs s⇩i t⇩i
assume "((l, r), cs) ∈ R" and "(s⇩i, t⇩i) ∈ set cs"
moreover
{
assume *: "funas_term t⇩i ⊆ funas_ctrs R - { f. defined (Ru R) f }"
from vc have **: "∀((l, r), cs) ∈ R. is_Fun l" by auto
have "strongly_irreducible R t⇩i"
using constructor_term_imp_strongly_irreducible [OF ** *] by auto
}
moreover
{
assume "ground t⇩i ∧ t⇩i ∈ NF (rstep (Ru R))"
then have "strongly_irreducible R t⇩i"
using ground_Ru_NF_imp_strongly_irreducible
by (simp add: Ru_NF_imp_R_NF ground_subst_apply strongly_irreducible_I)
}
ultimately
have "strongly_irreducible R t⇩i" using assms by fastforce
}
then show ?thesis by force
qed
end
lemma Var_cstep_n [dest]:
assumes "(Var x, t) ∈ cstep_n R n"
and "∀((l, r), cs) ∈ R. is_Fun l"
shows "False"
using assms by (auto simp: elim!: cstep_nE) (case_tac C; case_tac l; force)
lemma Var_rtrancl_cstep_n [dest]:
assumes "(Var x, t) ∈ (cstep_n R n)⇧*"
and "∀((l, r), cs) ∈ R. is_Fun l"
shows "t = Var x"
using assms by (induct) auto
subsection ‹TRS for level @{term n}.›
fun trs_n :: "('f, 'v) ctrs ⇒ nat ⇒ ('f, 'v) trs"
where
"trs_n R 0 = {}" |
"trs_n R (Suc n) =
{(l ⋅ σ, r ⋅ σ) | l r σ cs.
((l, r), cs) ∈ R ∧ (∀ (s⇩i, t⇩i) ∈ set cs. (s⇩i ⋅ σ, t⇩i ⋅ σ) ∈ (rstep (trs_n R n))⇧*)}"
lemma trs_n_SucI:
assumes "((l, r), cs) ∈ R"
and "⋀s⇩i t⇩i. (s⇩i, t⇩i) ∈ set cs ⟹ (s⇩i ⋅ σ, t⇩i ⋅ σ) ∈ (rstep (trs_n R n))⇧*"
shows "(l ⋅ σ, r ⋅ σ) ∈ trs_n R (Suc n)"
using assms by (simp) blast
lemma trs_nE:
assumes "(s, t) ∈ trs_n R n"
obtains l r σ cs n' where "n = Suc n'" and "s = l ⋅ σ" and "t = r ⋅ σ" and "((l, r), cs) ∈ R"
and "∀ (s⇩i, t⇩i) ∈ set cs. (s⇩i ⋅ σ, t⇩i ⋅ σ) ∈ (rstep (trs_n R n'))⇧*"
using assms by (cases n; simp) blast
lemma trs_n_SucE:
assumes "(s, t) ∈ trs_n R (Suc n)"
obtains l r σ cs where "s = l ⋅ σ" and "t = r ⋅ σ" and "((l, r), cs) ∈ R"
and "∀ (s⇩i, t⇩i) ∈ set cs. (s⇩i ⋅ σ, t⇩i ⋅ σ) ∈ (rstep (trs_n R n))⇧*"
using assms by (simp) blast
declare trs_n.simps(2) [simp del]
lemma trs_n_subst:
assumes "(l, r) ∈ trs_n R n"
shows "(l ⋅ σ, r ⋅ σ) ∈ trs_n R n"
using assms
proof (induction n)
case (Suc n)
from Suc.prems obtain l' r' σ' cs
where [simp]: "l = l' ⋅ σ'" "r = r' ⋅ σ'" and "((l', r'), cs) ∈ R"
and "∀(s⇩i, t⇩i) ∈ set cs. (s⇩i ⋅ σ', t⇩i ⋅ σ') ∈ (rstep (trs_n R n))⇧*"
by (auto elim: trs_n_SucE)
moreover then have "∀(s⇩i, t⇩i) ∈ set cs.
(s⇩i ⋅ (σ' ∘⇩s σ), t⇩i ⋅ (σ' ∘⇩s σ)) ∈ (rstep (trs_n R n))⇧*" by (auto intro: rsteps_closed_subst)
ultimately have "(l' ⋅ (σ' ∘⇩s σ), r' ⋅ (σ' ∘⇩s σ)) ∈ trs_n R (Suc n)"
by (blast intro: trs_n_SucI)
then show ?case by simp
qed simp
lemma no_step_from_constructor:
assumes vc: "∀((l, r), cs) ∈ R. is_Fun l"
and "funas_term t ⊆ funas_ctrs R - { f. defined (Ru R) f }"
and fp: "p ∈ funposs t"
shows "(t ⋅ σ |_ p, u) ∉ trs_n R n"
proof
assume "(t ⋅ σ |_ p, u) ∈ trs_n R n"
from trs_nE [OF this] obtain l r τ cs where *: "((l, r), cs) ∈ R" and **: "t ⋅ σ |_ p = l ⋅ τ"
by metis
then obtain f ts where [simp]: "l = Fun f ts" using vc by (cases l, auto)
have "defined (Ru R) (f, length ts)" using * by (intro defined_R_imp_Ru) (auto)
moreover from fp ** have "(f, length ts) ∈ funas_term t"
proof -
from funposs_fun_conv [OF fp] obtain g ss where ***: "t |_ p = Fun g ss" by blast
with funposs_imp_poss [OF fp] have "t ⋅ σ |_ p = Fun g (map (λx. x ⋅ σ) ss)" by auto
then have [simp]: "g = f" "length ts = length ss" using ** map_eq_imp_length_eq by (force)+
from *** funposs_imp_poss [OF fp] show ?thesis by (auto simp add: funas_term_poss_conv)
qed
ultimately show "False" using assms(2) by blast
qed
lemma cstep_n_rstep_trs_n_conv:
"cstep_n R n = rstep (trs_n R n)"
proof (induction n)
case (Suc n)
{ fix s t
assume "(s, t) ∈ cstep_n R (Suc n)"
then have "(s, t) ∈ rstep (trs_n R (Suc n))"
by (auto elim!: cstep_n_SucE simp: Suc split: prod.splits)
(metis rstep.ctxt rstep.rule trs_n_SucI) }
moreover
{ fix s t
assume "(s, t) ∈ rstep (trs_n R (Suc n))"
then obtain u v C σ where "(u, v) ∈ trs_n R (Suc n)"
and [simp]: "s = C⟨u ⋅ σ⟩""t = C⟨v ⋅ σ⟩" ..
then obtain l r cs τ where "((l, r), cs) ∈ R"
and [simp]: "u = l ⋅ τ" "v = r ⋅ τ"
and "∀(s⇩i, t⇩i) ∈ set cs. (s⇩i ⋅ τ, t⇩i ⋅ τ) ∈ (rstep (trs_n R n))⇧*"
by (auto elim: trs_n_SucE)
moreover then have "∀(s⇩i, t⇩i) ∈ set cs. (s⇩i ⋅ (τ ∘⇩s σ), t⇩i ⋅ (τ ∘⇩s σ)) ∈ (cstep_n R n)⇧*"
by (auto intro: rsteps_closed_subst simp: Suc)
ultimately have "(C⟨l ⋅ (τ ∘⇩s σ)⟩, C⟨r ⋅ (τ ∘⇩s σ)⟩) ∈ cstep_n R (Suc n)" by (blast intro: cstep_n_SucI)
then have "(s, t) ∈ cstep_n R (Suc n)" by simp }
ultimately show ?case by auto
qed simp
lemma trs_n_Suc_mono:
"trs_n R n ⊆ trs_n R (Suc n)"
proof (induct n)
case (Suc n)
then have "rstep (trs_n R n) ⊆ rstep (trs_n R (Suc n))" by (metis rstep_mono)
from rtrancl_mono [OF this]
show ?case by (auto elim!: trs_n_SucE intro!: trs_n_SucI)
qed simp
lemma rrstep_trs_n [simp]:
"rrstep (trs_n R n) = trs_n R n"
by (auto simp: CS_rrstep_conv [symmetric]
elim: subst.closure.cases intro: subst.closureI2 [of _ _ _ _ Var] trs_n_subst)
lemma cstep_rstep_UN_trs_n_conv: "cstep R = rstep (⋃n. trs_n R n)"
by (auto simp: cstep_def cstep_n_rstep_trs_n_conv rstep_UN)
lemma Var_trs_n [dest]:
assumes "(Var x, t) ∈ trs_n R n"
and "∀((l, r), cs) ∈ R. is_Fun l"
shows "False"
using assms by (induct n) (force elim!: trs_n_SucE split: prod.splits)+
lemma linear_term_cstep_n_cases':
assumes "linear_term s"
and cstep: "(s ⋅ σ, u) ∈ cstep_n R n"
shows "(∃τ. s ⋅ τ = u ∧ (∀x. (σ x, τ x) ∈ (cstep_n R n)⇧*)) ∨
(∃p ∈ funposs s. (s ⋅ σ |_ p, u |_ p) ∈ trs_n R n)"
proof -
from cstep [THEN cstep_nE] obtain C l r σ' cs k
where rule: "((l, r), cs) ∈ R" and [simp]: "n = Suc k"
and conds: "conds_n_sat R k cs σ'"
and s_σ: "s ⋅ σ = C⟨l ⋅ σ'⟩" and u: "u = C⟨r ⋅ σ'⟩"
unfolding conds_n_sat_iff by metis
define p where "p ≡ hole_pos C"
have *: "p ∈ poss (s ⋅ σ)" by (simp add: assms s_σ p_def)
show ?thesis
proof (cases "p ∈ funposs s")
case False
with * obtain q⇩1 q⇩2 x
where p: "p = q⇩1 <#> q⇩2" and q⇩1: "q⇩1 ∈ poss s"
and lq⇩1: "s |_ q⇩1 = Var x" and q⇩2: "q⇩2 ∈ poss (σ x)"
by (rule poss_subst_apply_term)
moreover
have [simp]: "s ⋅ σ |_ p = l ⋅ σ'" using assms p_def s_σ by auto
ultimately
have [simp]: "σ x |_ q⇩2 = l ⋅ σ'" by simp
define τ where "τ ≡ λy. if y = x then replace_at (σ x) q⇩2 (r ⋅ σ') else σ y"
have τ_x: "τ x = replace_at (σ x) q⇩2 (r ⋅ σ')" by (simp add: τ_def)
have [simp]: "⋀y. y ≠ x ⟹ τ y = σ y" by (simp add: τ_def)
have "(σ x, τ x) ∈ cstep_n R n"
proof -
let ?C = "ctxt_of_pos_term q⇩2 (σ x)"
have "(?C⟨l ⋅ σ'⟩, ?C⟨r ⋅ σ'⟩) ∈ cstep_n R n"
using conds by (auto intro!: cstep_n_SucI rule simp: conds_n_sat_iff)
then show ?thesis using q⇩2 by (simp add: τ_def replace_at_ident)
qed
then have "∀x. (σ x, τ x) ∈ (cstep_n R n)⇧*" by (auto simp: τ_def)
moreover have "s ⋅ τ = u"
proof -
have [simp]: "ctxt_of_pos_term p (s ⋅ σ) = C" by (simp add: assms s_σ p_def)
have "s ⋅ σ |_ q⇩1 = σ x" by (simp add: lq⇩1 q⇩1)
from linear_term_replace_in_subst [OF ‹linear_term s› q⇩1 lq⇩1, of σ τ, OF _ τ_x, folded ctxt_ctxt_compose]
and q⇩1 and ctxt_of_pos_term_append [of q⇩1 "s ⋅ σ" q⇩2, folded p, unfolded this, symmetric]
show "s ⋅ τ = u" by (simp add: u)
qed
ultimately show ?thesis by blast
next
case True
moreover have "(s ⋅ σ |_ p, u |_ p) ∈ trs_n R (Suc k)"
using conds
by (auto simp: conds_n_sat_iff p_def s_σ u
intro: trs_n_SucI [OF rule] simp: cstep_n_rstep_trs_n_conv)
ultimately show ?thesis by auto
qed
qed
lemma linear_term_cstep_n_cases [consumes 2]:
assumes "linear_term s"
and "(s ⋅ σ, u) ∈ cstep_n R n"
obtains (varposs) τ where "s ⋅ τ = u"
and "∀x. (σ x, τ x) ∈ (cstep_n R n)⇧*"
| (funposs) p where "p ∈ funposs s" and "(s ⋅ σ |_ p, u |_ p) ∈ trs_n R n"
using linear_term_cstep_n_cases' [OF assms] by blast
lemma linear_term_rtrancl_cstep_n_cases':
assumes "linear_term s"
and "(s ⋅ σ, t) ∈ (cstep_n R n)⇧*"
shows "(∃τ. s ⋅ τ = t ∧ (∀x. (σ x, τ x) ∈ (cstep_n R n)⇧*)) ∨
(∃τ p u. (∀x. (σ x, τ x) ∈ (cstep_n R n)⇧*) ∧
p ∈ funposs s ∧ (s ⋅ τ |_ p, u) ∈ trs_n R n)"
using assms(2)
proof (induct)
case base
let ?τ = "σ"
have "s ⋅ σ = s ⋅ ?τ" using coincidence_lemma by blast
moreover have "∀x. (σ x, ?τ x) ∈ (cstep_n R n)⇧*" by auto
ultimately show ?case by auto
next
case (step t u)
show ?case using step(3)
proof
assume "∃τ. s ⋅ τ = t ∧ (∀x. (σ x, τ x) ∈ (cstep_n R n)⇧*)"
then obtain τ where t: "t = s ⋅ τ" and *: "∀x. (σ x, τ x) ∈ (cstep_n R n)⇧*" by blast
then have "(s ⋅ τ, u) ∈ cstep_n R n" using ‹(t, u) ∈ cstep_n R n› by auto
with ‹linear_term s›
show ?thesis
using * by (cases rule: linear_term_cstep_n_cases; blast dest: rtrancl_trans)
qed blast
qed
lemma linear_term_rtrancl_cstep_n_cases [consumes 2]:
assumes "linear_term s"
and "(s ⋅ σ, t) ∈ (cstep_n R n)⇧*"
obtains (varposs) τ where "s ⋅ τ = t" and "∀x. (σ x, τ x) ∈ (cstep_n R n)⇧*"
| (funposs) τ p u where "∀x. (σ x, τ x) ∈ (cstep_n R n)⇧*"
and "p ∈ funposs s" and "(s ⋅ τ |_ p, u) ∈ trs_n R n"
using linear_term_rtrancl_cstep_n_cases' [OF assms] by blast
definition properly_oriented
where
"properly_oriented R ⟷ (∀ρ ∈ R.
vars_term (crhs ρ) ⊆ vars_term (clhs ρ) ∨
(∀i < length (snd ρ). vars_term (fst (snd ρ ! i)) ⊆ X_vars ρ i))"
definition extended_properly_oriented
where
"extended_properly_oriented R ⟷ (∀ρ ∈ R. vars_term (crhs ρ) ⊆ vars_term (clhs ρ) ∨
(∃m ≤ length (snd ρ).
(∀i < m. vars_term (fst (snd ρ ! i)) ⊆ X_vars ρ i) ∧
(∀i∈{m ..< length (snd ρ)}. vars_term (crhs ρ) ∩ vars_rule (snd ρ ! i) ⊆ X_vars ρ m)))"
definition right_stable :: "('f, 'v) ctrs ⇒ bool"
where
"right_stable R ⟷ (∀ ρ ∈ R. ∀ i < length (snd ρ).
let t⇩i = snd (snd ρ ! i) in
(vars_term (clhs ρ) ∪ ⋃(vars_term ` lhss (set (take (Suc i) (snd ρ)))) ∪
⋃(vars_term ` (rhss (set (take i (snd ρ)))))) ∩ vars_term t⇩i = {} ∧
(linear_term t⇩i ∧ funas_term t⇩i ⊆ funas_ctrs R - { f. defined (Ru R) f } ∨
ground t⇩i ∧ t⇩i ∈ NF (rstep (Ru R))))"
lemma right_stable_rhsD:
assumes "right_stable R" and "ρ ∈ R" and "i < length (snd ρ)"
shows "(vars_term (clhs ρ) ∪ ⋃(vars_term ` lhss (set (take (Suc i) (snd ρ)))) ∪
⋃(vars_term ` (rhss (set (take i (snd ρ)))))) ∩ vars_term (snd (snd ρ ! i)) = {}"
using assms by (auto simp: right_stable_def Let_def)
lemma right_stable_rhs_cases [consumes 3, case_names lct [linear cterm] gnf [ground nf]]:
assumes "right_stable R" and "ρ ∈ R"
and "t ∈ rhss (set (snd ρ))"
obtains
(lct) "linear_term t" and "funas_term t ⊆ funas_ctrs R - {f. defined (Ru R) f}" |
(gnf) "ground t" and "t ∈ NF (rstep (Ru R))"
proof -
obtain i where "i < length (snd ρ)" and "t = snd (snd ρ ! i)"
using assms(3) by (auto dest: in_set_idx)
with assms(1, 2) show ?thesis using lct and gnf by (auto simp: right_stable_def Let_def)
qed
lemma crule_cases:
assumes "⋀l r cs. ρ = ((l, r), cs) ⟹ P"
shows "P"
using assms by (cases ρ; auto)
lemma cstep_subst:
assumes "(s, t) ∈ cstep R"
shows "(s ⋅ σ, t ⋅ σ) ∈ cstep R"
using assms
by (auto simp: cstep_def dest: cstep_n_subst)
lemma subst_closed_cstep [intro]:
"subst.closed (cstep R)"
using cstep_subst subst.closedI by blast
lemma cstep_ctxt:
assumes "(s, t) ∈ cstep R"
shows "(C⟨s⟩, C⟨t⟩) ∈ cstep R"
using assms
by (simp add: cstep_ctxt_closed ctxt.closedD)
lemma csteps_ctxt:
assumes "(s, t) ∈ (cstep R)⇧*"
shows "(C⟨s⟩, C⟨t⟩) ∈ (cstep R)⇧*"
using assms
by (simp add: cstep_ctxt_closed ctxt.closedD ctxt.closed_rtrancl)
abbreviation conds :: "('f, 'v) crule ⇒ ('f, 'v) rule list"
where
"conds ρ ≡ snd ρ"
lemma conds_n_sat_mono':
assumes "conds_n_sat R n cs σ"
and "set ds ⊆ set cs"
shows "conds_n_sat R n ds σ"
using assms by (auto simp: conds_n_sat_iff)
definition evars_crule :: "('f, 'v) crule ⇒ 'v set"
where "evars_crule ρ = vars_trs (set (conds ρ)) - vars_term (clhs ρ)"
lemmas args_csteps_imp_csteps = args_steps_imp_steps [OF cstep_ctxt_closed]
lemma substs_csteps:
assumes "⋀x. (σ x, τ x) ∈ (cstep R)⇧*"
shows "(t ⋅ σ, t ⋅ τ) ∈ (cstep R)⇧*"
proof (induct t)
case (Var y)
show ?case using assms by simp_all
next
case (Fun f ts)
then have "∀i<length (map (λt. t ⋅ σ) ts).
(map (λt. t ⋅ σ ) ts ! i, map (λt. t ⋅ τ) ts ! i) ∈ (cstep R)⇧*" by auto
from args_csteps_imp_csteps [OF _ this] show ?case by simp
qed
lemma term_subst_cstep:
assumes "⋀x. x ∈ vars_term t ⟹ (σ x, τ x) ∈ cstep R"
shows "(t ⋅ σ, t ⋅ τ) ∈ (cstep R)⇧*"
using assms
proof (induct t)
case (Fun f ts)
{ fix t⇩i
assume t⇩i: "t⇩i ∈ set ts"
with Fun(2) have "⋀x. x ∈ vars_term t⇩i ⟹ (σ x, τ x) ∈ cstep R" by auto
from Fun(1) [OF t⇩i this] have "(t⇩i ⋅ σ, t⇩i ⋅ τ) ∈ (cstep R)⇧*" by blast
}
then show ?case by (simp add: args_csteps_imp_csteps)
qed (auto)
lemma term_subst_csteps:
assumes "⋀x. x ∈ vars_term t ⟹ (σ x, τ x) ∈ (cstep R)⇧*"
shows "(t ⋅ σ, t ⋅ τ) ∈ (cstep R)⇧*"
using assms
proof (induct t)
case (Fun f ts)
{ fix t⇩i
assume t⇩i: "t⇩i ∈ set ts"
with Fun(2) have "⋀x. x ∈ vars_term t⇩i ⟹ (σ x, τ x) ∈ (cstep R)⇧*" by auto
from Fun(1) [OF t⇩i this] have "(t⇩i ⋅ σ, t⇩i ⋅ τ) ∈ (cstep R)⇧*" by blast
}
then show ?case by (simp add: args_csteps_imp_csteps)
qed (auto)
lemma term_subst_csteps_join:
assumes "⋀y. y ∈ vars_term u ⟹ (σ⇩1 y, σ⇩2 y) ∈ (cstep R)⇧↓"
shows "(u ⋅ σ⇩1, u ⋅ σ⇩2) ∈ (cstep R)⇧↓"
using assms
proof -
{ fix x
assume "x ∈ vars_term u"
from assms [OF this] have "∃σ. (σ⇩1 x, σ x) ∈ (cstep R)⇧* ∧ (σ⇩2 x, σ x) ∈ (cstep R)⇧*" by auto
}
then have "∀x ∈ vars_term u. ∃σ. (σ⇩1 x, σ x) ∈ (cstep R)⇧* ∧ (σ⇩2 x, σ x) ∈ (cstep R)⇧*" by blast
then obtain s where "∀x ∈ vars_term u. (σ⇩1 x, (s x) x) ∈ (cstep R)⇧* ∧ (σ⇩2 x, (s x) x) ∈ (cstep R)⇧*" by metis
then obtain σ where "∀x ∈ vars_term u. (σ⇩1 x, σ x) ∈ (cstep R)⇧* ∧ (σ⇩2 x, σ x) ∈ (cstep R)⇧*" by fast
then have "(u ⋅ σ⇩1, u ⋅ σ) ∈ (cstep R)⇧* ∧ (u ⋅ σ⇩2, u ⋅ σ) ∈ (cstep R)⇧*" using term_subst_csteps by metis
then show ?thesis by blast
qed
lemma subst_csteps_imp_csteps:
fixes σ :: "('f, 'v) subst"
assumes "∀x∈vars_term t. (σ x, τ x) ∈ (cstep R)⇧*"
shows "(t ⋅ σ, t ⋅ τ) ∈ (cstep R)⇧*"
by (rule all_ctxt_closed_subst_step)
(insert assms, auto)
lemma replace_at_subst_csteps:
fixes σ τ :: "('f, 'v) subst"
assumes *: "⋀x. (σ x, τ x) ∈ (cstep R)⇧*"
and "p ∈ poss t"
and "t |_ p = Var x"
shows "(replace_at (t ⋅ σ) p (τ x), t ⋅ τ) ∈ (cstep R)⇧*"
using assms(2-)
proof (induction t arbitrary: p)
case (Fun f ts)
then obtain i q where [simp]: "p = i <# q" and i: "i < length ts"
and q: "q ∈ poss (ts ! i)" and [simp]: "ts ! i |_ q = Var x" by (cases p) auto
let ?C = "ctxt_of_pos_term q (ts ! i ⋅ σ)"
let ?ts = "map (λt. t ⋅ τ) ts"
let ?ss = "take i (map (λt. t ⋅ σ) ts) @ ?C⟨τ x⟩ # drop (Suc i) (map (λt. t ⋅ σ) ts)"
have "∀j<length ts. (?ss ! j, ?ts ! j) ∈ (cstep R)⇧*"
proof (intro allI impI)
fix j
assume j: "j < length ts"
moreover
{ assume [simp]: "j = i"
have "?ss ! j = ?C⟨τ x⟩" using i by (simp add: nth_append_take)
with Fun.IH [of "ts ! i" q]
have "(?ss ! j, ?ts ! j) ∈ (cstep R)⇧*" using q and i by simp }
moreover
{ assume "j < i"
with i have "?ss ! j = ts ! j ⋅ σ"
and "?ts ! j = ts ! j ⋅ τ" by (simp_all add: nth_append_take_is_nth_conv)
then have "(?ss ! j, ?ts ! j) ∈ (cstep R)⇧*" by (auto simp: * subst_csteps_imp_csteps) }
moreover
{ assume "j > i"
with i and j have "?ss ! j = ts ! j ⋅ σ"
and "?ts ! j = ts ! j ⋅ τ" by (simp_all add: nth_append_drop_is_nth_conv)
then have "(?ss ! j, ?ts ! j) ∈ (cstep R)⇧*" by (auto simp: * subst_csteps_imp_csteps) }
ultimately show "(?ss ! j, ?ts ! j) ∈ (cstep R)⇧*" by arith
qed
moreover have "i < length ts" by fact
ultimately show ?case
by (simp add: args_csteps_imp_csteps)
qed simp
fun map_funs_crule :: "('f ⇒ 'g) ⇒ ('f, 'v) crule ⇒ ('g, 'v) crule"
where
"map_funs_crule f r = ((map_funs_term f (clhs r), map_funs_term f (crhs r)), map (map_funs_rule f) (conds r))"
lemma map_funs_crule_id [simp]: "map_funs_crule id = id" by auto
fun map_funs_ctrs :: "('f ⇒ 'g) ⇒ ('f, 'v) ctrs ⇒ ('g, 'v) ctrs"
where
"map_funs_ctrs f R = map_funs_crule f ` R"
lemma conds_sat_Cons:
"conds_sat R (c # cs) σ ⟷ (fst c ⋅ σ, snd c ⋅ σ) ∈ (cstep R)⇧* ∧ conds_sat R cs σ"
by (auto simp: conds_sat_iff)
lemma conds_n_sat_Cons:
"conds_n_sat R n (c # cs) σ ⟷
(fst c ⋅ σ, snd c ⋅ σ) ∈ (cstep_n R n)⇧* ∧ conds_n_sat R n cs σ"
by (auto simp: conds_n_sat_iff)
lemma conds_sat_conds_n_sat:
"conds_sat R cs σ ⟷ (∃n. conds_n_sat R n cs σ)" (is "?P = ?Q")
proof
assume "?Q" then show "?P"
by (auto simp: conds_sat_iff conds_n_sat_iff dest: csteps_n_imp_csteps)
next
assume "?P" then show "?Q"
proof (induct cs)
case (Cons c cs)
then show ?case
apply (auto simp: conds_sat_Cons conds_n_sat_Cons dest!: csteps_imp_csteps_n)
apply (rule_tac x = "max n na" in exI)
apply (auto simp: max_def conds_n_sat_iff conds_sat_iff
dest!: csteps_n_mono)
apply (rule_tac m1 = na and n1 = n in csteps_n_mono [THEN subsetD])
apply force+
done
qed simp
qed
subsection ‹Permutation Types for Conditional Rules and CTRSs›
interpretation crule_pt: prod_pt rule_pt.permute_prod rules_pt.permute_list ..
adhoc_overloading
PERMUTE crule_pt.permute_prod and
FRESH crule_pt.fresh crule_pt.fresh_set
interpretation ctrs_pt: set_pt crule_pt.permute_prod ..
adhoc_overloading
PERMUTE ctrs_pt.permute_set and
FRESH ctrs_pt.fresh
lemma finite_crule_supp:
"finite (crule_pt.supp ((l, r), cs))"
by (simp add: finite_term_supp rule_fs.finite_supp)
interpretation crule_fs: finitely_supported crule_pt.permute_prod
by standard (auto simp: finite_rule_supp finite_term_supp)
lemma conds_n_sat_perm_shift:
"conds_n_sat R n (π ∙ cs) σ = conds_n_sat R n cs (σ ∘ Rep_perm π)"
by (auto simp: conds_n_sat_iff permute_term_subst_apply_term eqvt split: prod.splits)
lemma supp_vars_crule_eq:
fixes r :: "('f, 'v :: infinite) crule"
shows "crule_pt.supp r = vars_crule r"
by (cases r; auto simp: vars_crule_def vars_trs_def supp_vars_term_eq vars_rule_def)
lemma vars_crule_disjoint:
fixes l r u v :: "('f, 'v :: infinite) term"
and cs ds :: "('f, 'v) rule list"
shows "∃p. vars_crule (p ∙ ((l, r), cs)) ∩ vars_crule ((u, v), ds) = {}"
proof -
from crule_fs.supp_fresh_set obtain p
where "crule_pt.supp (p ∙ ((l, r), cs)) ♯ ((u, v), ds)" by blast
from crule_pt.fresh_set_disjoint [OF this]
show ?thesis
by (auto simp: supp_vars_crule_eq vars_rule_def)
qed
lemma X_vars_eqvt [eqvt]:
"p ∙ X_vars r i = X_vars (p ∙ r) i"
proof -
have "take i (snd (p ∙ r)) = p ∙ take i (snd r)"
by (metis (no_types, hide_lams) crule_pt.snd_eqvt rules_pt.permute_list_def take_map)
then show ?thesis
by (simp_all add: X_vars_def eqvt)
qed
lemma variant_conds_n_sat_cstep_n:
assumes "π ∙ ρ ∈ R"
and "conds_n_sat R n (conds ρ) σ"
shows "(clhs ρ ⋅ σ, crhs ρ ⋅ σ) ∈ cstep_n R (Suc n)"
proof -
from assms(1) have r: "((π ∙ clhs ρ, π ∙ crhs ρ), π ∙ conds ρ) ∈ R"
by (simp add: eqvt split: prod.split)
(metis crule_pt.snd_eqvt prod.collapse rules_pt.permute_list_def)
from assms(2) have "conds_n_sat R n (- π ∙ π ∙ conds ρ) σ"
by (metis rules_pt.permute_minus_cancel(2))
from conds_n_sat_perm_shift [THEN iffD1, OF this]
have "conds_n_sat R n (π ∙ conds ρ) (σ ∘ Rep_perm (- π))" (is "conds_n_sat _ _ _ ?τ") by auto
from conds_n_sat_iff [THEN iffD1, OF this]
have "∀(s⇩i, t⇩i)∈set (π ∙ conds ρ). (s⇩i ⋅ ?τ, t⇩i ⋅ ?τ) ∈ (cstep_n R n)⇧*" .
from cstep_n_SucI [OF r this, of _ □]
have "(π ∙ clhs ρ ⋅ ?τ, π ∙ crhs ρ ⋅ ?τ) ∈ cstep_n R (Suc n)" by force
then have "(clhs ρ ⋅ (sop π ∘⇩s ?τ), crhs ρ ⋅ (sop π ∘⇩s ?τ)) ∈ cstep_n R (Suc n)" by simp
then show ?thesis
by (metis (no_types, lifting) permute_term_subst_apply_term subst_subst
term_apply_subst_Var_Rep_perm term_pt.permute_minus_cancel(2))
qed
lemma variant_conds_sat_cstep:
assumes "π ∙ ρ ∈ R"
and "conds_sat R (conds ρ) σ"
shows "(clhs ρ ⋅ σ, crhs ρ ⋅ σ) ∈ cstep R"
using assms conds_sat_conds_n_sat cstep_n_imp_cstep variant_conds_n_sat_cstep_n by blast
lemma rsteps_eqvt:
"π ∙ (rstep R)⇧* = (rstep (π ∙ R))⇧*"
using rstep_eqvt [of π R]
by (metis permute_rstep rstep_rtrancl_idemp)
lemma trs_n_eqvt_aux:
"π ∙ (trs_n (-π ∙ R) n) = trs_n R n"
proof (induct n)
case (Suc n)
then have IH: "π ∙ (trs_n (-π ∙ R) n) = trs_n R n" by blast
show ?case
proof (intro equalityI subrelI, goal_cases)
case (1 s t)
then have "(-π ∙ s, -π ∙ t) ∈ trs_n (-π ∙ R) (Suc n)"
using inv_rule_mem_trs_simps(1) by blast
then show ?case unfolding trs_n.simps apply (simp add: IH [symmetric])
apply auto
apply (rule_tac x = "π ∙ l" in exI)
apply (rule_tac x = "π ∙ r" in exI)
apply (rule_tac x = "sop (-π) ∘⇩s σ ∘⇩s sop π" in exI)
apply (auto simp:)
apply (metis term_pt.permute_minus_cancel(1))
apply (metis term_pt.permute_minus_cancel(1))
apply (rule_tac x = "π ∙ cs" in exI)
apply (auto simp: eqvt)
by (metis (no_types, lifting) case_prodD rstep_imp_perm_rstep rstep_rtrancl_idemp term_apply_subst_eqvt)
next
case (2 s t)
then have "(-π ∙ s, -π ∙ t) ∈ trs_n (-π ∙ R) (Suc n)"
apply (auto simp: trs_n.simps(2))
apply (rule_tac x = "-π ∙ l" in exI)
apply (rule_tac x = "-π ∙ r" in exI)
apply (rule_tac x = "sop π ∘⇩s σ ∘⇩s sop (-π)" in exI)
apply auto
apply (rule_tac x = "-π ∙ cs" in exI)
apply (auto simp: eqvt map_idI rsteps_eqvt IH)
by force
then show ?case using inv_rule_mem_trs_simps(1) by blast
qed
qed simp
lemma rstep_perm_trs_n:
shows "rstep (π ∙ (trs_n R n)) = rstep (trs_n (π ∙ R) n)"
using trs_n_eqvt_aux [of "-π" R n]
apply (simp)
by (metis rstep_permute)
lemma cstep_permute:
"cstep (π ∙ R) = cstep R"
proof -
have "cstep (π ∙ R) = (⋃n. rstep (trs_n (π ∙ R) n))"
by (auto simp: cstep_def cstep_n_rstep_trs_n_conv)
also have "… = (⋃n. rstep (π ∙ (trs_n R n)))" unfolding rstep_perm_trs_n ..
also have "… = (⋃n. rstep (trs_n R n))" unfolding rstep_permute ..
also have "… = cstep R" by (auto simp: cstep_def cstep_n_rstep_trs_n_conv)
finally show ?thesis .
qed
lemma cstep_eqvt [eqvt]:
"π ∙ cstep R = cstep (π ∙ R)"
proof -
have "π ∙ cstep R = π ∙ (⋃n. rstep (trs_n R n))"
by (auto simp: cstep_def cstep_n_rstep_trs_n_conv)
also have "… = (⋃n. rstep (π ∙ (trs_n R n)))" by (auto simp: eqvt)
also have "… = (⋃n. rstep (trs_n (π ∙ R) n))" unfolding rstep_perm_trs_n ..
also have "… = cstep (π ∙ R)" by (auto simp: cstep_def cstep_n_rstep_trs_n_conv)
finally show ?thesis .
qed
lemma permute_cstep [simp]:
"π ∙ cstep R = cstep R"
by (simp add: eqvt cstep_permute)
lemma csteps_eqvt:
"π ∙ (cstep R)⇧* = (cstep (π ∙ R))⇧*"
proof (intro equalityI subrelI)
fix s t assume "(s, t) ∈ π ∙ (cstep R)⇧*"
then have "(-π ∙ s, -π ∙ t) ∈ (cstep R)⇧*" by auto
then show "(s, t) ∈ (cstep (π ∙ R))⇧*"
apply (induct "-π ∙ s" "-π ∙ t" arbitrary: t)
apply auto
by (metis (no_types, lifting) cstep_eqvt inv_rule_mem_trs_simps(2) minus_minus rtrancl.rtrancl_into_rtrancl term_pt.permute_minus_cancel(1))
next
fix s t assume "(s, t) ∈ (cstep (π ∙ R))⇧*"
then show "(s, t) ∈ π ∙ (cstep R)⇧*"
apply (induct)
using inv_rule_mem_trs_simps(1) apply blast
by (metis cstep_eqvt inv_rule_mem_trs_simps(1) rtrancl.rtrancl_into_rtrancl)
qed
lemma cstep_n_permute_iff:
"(π ∙ s, π ∙ t) ∈ cstep_n R n ⟷ (s, t) ∈ cstep_n R n"
by (auto simp: cstep_n_rstep_trs_n_conv split: prod.splits)
lemma subst_compose_o_assoc:
"(σ ∘⇩s τ) ∘ f = (σ ∘ f) ∘⇩s τ"
by (rule ext) (simp add: subst_compose)
lemma perm_csteps_n_perm:
assumes "(π ∙ s, t) ∈ (cstep_n R n)⇧*"
shows "∃u. t = π ∙ u"
using assms by (metis term_pt.permute_minus_cancel(1))
lemma subst_list_subst_compose:
"subst_list (σ ∘⇩s τ) xs = subst_list τ (subst_list σ xs)"
by (simp add: subst_list_def)
lemma subst_list_Rep_perm:
"subst_list (σ ∘ Rep_perm π) xs = subst_list σ (π ∙ xs)"
by (auto simp: subst_list_def permute_term_subst_apply_term [symmetric] eqvt)
lemma finite_vars_crule: "finite (vars_crule r)"
by (auto simp: vars_crule_def vars_defs)
lemma nth_subst_list [simp]:
"i < length ts ⟹ subst_list σ ts ! i = (fst (ts ! i) ⋅ σ, snd (ts ! i) ⋅ σ)"
by (auto simp: subst_list_def)
lemma length_subst_list [simp]:
"length (subst_list σ ts) = length ts"
by (auto simp: subst_list_def)
lemma vars_conds_vars_crule_subset:
"x ∈ vars_term (fst (conds r ! i)) ⟹ i < length (conds r) ⟹ x ∈ vars_crule r"
"x ∈ vars_term (snd (conds r ! i)) ⟹ i < length (conds r) ⟹ x ∈ vars_crule r"
by (auto simp: vars_crule_def vars_defs)
lemma permute_conds_set [simp]:
fixes cs :: "('f, 'v::infinite) rule list"
shows "π ∙ set cs = set (π ∙ cs)"
by (induct cs) (auto simp: eqvt)
lemma cstep_imp_map_cstep:
assumes "(s, t) ∈ cstep R"
shows "(map_funs_term h s, map_funs_term h t) ∈ cstep (map_funs_ctrs h R)"
(is "(?h s, ?h t) ∈ cstep (?H R)")
proof -
obtain n where "(s, t) ∈ cstep_n R n" using assms by (auto simp: cstep_iff)
then have "(?h s, ?h t) ∈ cstep_n (?H R) n"
proof (induct n arbitrary: s t)
case (Suc n)
then obtain C σ l r cs where rule: "((l, r), cs) ∈ R"
and *: "∀(u, v) ∈ set cs. (u ⋅ σ, v ⋅ σ) ∈ (cstep_n R n)⇧*"
and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩" by (auto elim: cstep_n_SucE)
let ?σ = "?h ∘ σ"
let ?C = "map_funs_ctxt h C"
let ?cs = "map (map_funs_rule h) cs"
have "((?h l, ?h r), ?cs) ∈ ?H R" using rule by force
moreover have "?h s = ?C⟨?h l ⋅ ?σ⟩" and "?h t = ?C⟨?h r ⋅ ?σ⟩" by (auto simp: s t o_def)
moreover have "∀(u, v) ∈ set ?cs. (u ⋅ ?σ, v ⋅ ?σ) ∈ (cstep_n (?H R) n)⇧*"
using rtrancl_map [where f = ?h and r = "cstep_n R n", OF Suc.hyps]
and * by (auto simp: o_def) force
ultimately show ?case by (blast intro: cstep_n_SucI)
qed simp
then show ?thesis by (auto simp: cstep_iff)
qed
definition "trs2ctrs R = { (r, []) | r. r ∈ R }"
lemma cstep_n_subset:
assumes "R ⊆ S"
shows "cstep_n R n ⊆ cstep_n S n"
using assms and rtrancl_mono [of "cstep_n R n" "cstep_n S n" for n]
by (induct n) (auto elim!: cstep_n_SucE intro!: cstep_n_SucI split: prod.splits, blast)
lemma cstep_subset:
assumes "R ⊆ S"
shows "cstep R ⊆ cstep S"
using cstep_n_subset [OF assms] by (force simp: cstep_iff)
lemma conds_sat_mono:
assumes "R ⊆ S"
shows "conds_sat R cs σ ⟹ conds_sat S cs σ"
using rtrancl_mono [OF cstep_subset [OF assms]] by (auto simp: conds_sat_iff)
end