chapter ‹Term Rewrite Systems›
theory Trs
imports
Term_More
"Abstract-Rewriting.Relative_Rewriting"
Term_Rewriting
begin
text ‹A theory on first-order term rewrite systems (TRSs).›
context
fixes shp :: "'f ⇒ 'f"
begin
interpretation sharp_syntax .
abbreviation sharp_trs :: "('f, 'v) trs ⇒ ('f, 'v) trs"
where
"sharp_trs R ≡ dir_image R ♯"
end
context sharp_syntax
begin
adhoc_overloading
SHARP "sharp_trs shp"
end
subsection ‹Variables of Rules›
definition
vars_rule :: "('f, 'v) rule ⇒ 'v set"
where
"vars_rule r = vars_term (fst r) ∪ vars_term (snd r)"
lemma finite_vars_rule:
"finite (vars_rule r)"
by (auto simp: vars_rule_def)
subsection ‹Variables of TRSs›
definition vars_trs :: "('f, 'v) trs ⇒ 'v set" where
"vars_trs R = (⋃r∈R. vars_rule r)"
lemma vars_trs_union: "vars_trs (R ∪ S) = vars_trs R ∪ vars_trs S"
unfolding vars_trs_def by auto
lemma finite_trs_has_finite_vars:
assumes "finite R" shows "finite (vars_trs R)"
using assms unfolding vars_trs_def vars_rule_def [abs_def] by simp
lemmas vars_defs = vars_trs_def vars_rule_def
subsection ‹Function Symbols of Rules›
definition funs_rule :: "('f, 'v) rule ⇒ 'f set" where
"funs_rule r = funs_term (fst r) ∪ funs_term (snd r)"
text ‹The same including arities.›
definition funas_rule :: "('f, 'v) rule ⇒ 'f sig" where
"funas_rule r = funas_term (fst r) ∪ funas_term (snd r)"
subsection ‹Function Symbols of TRSs›
definition funs_trs :: "('f, 'v) trs ⇒ 'f set" where
"funs_trs R = (⋃r∈R. funs_rule r)"
definition funas_trs :: "('f, 'v) trs ⇒ 'f sig" where
"funas_trs R = (⋃r∈R. funas_rule r)"
lemma funs_rule_funas_rule: "funs_rule rl = fst ` funas_rule rl"
using funs_term_funas_term unfolding funs_rule_def funas_rule_def image_Un by metis
lemma funs_trs_funas_trs:"funs_trs R = fst ` funas_trs R"
unfolding funs_trs_def funas_trs_def image_UN using funs_rule_funas_rule by metis
lemma finite_funas_rule: "finite (funas_rule lr)"
unfolding funas_rule_def
using finite_funas_term by auto
lemma finite_funas_trs:
assumes "finite R"
shows "finite (funas_trs R)"
unfolding funas_trs_def
using assms finite_funas_rule by auto
lemma funas_empty[simp]: "funas_trs {} = {}" unfolding funas_trs_def by simp
lemma funas_trs_union[simp]: "funas_trs (R ∪ S) = funas_trs R ∪ funas_trs S"
unfolding funas_trs_def by blast
definition funas_args_rule :: "('f, 'v) rule ⇒ 'f sig" where
"funas_args_rule r = funas_args_term (fst r) ∪ funas_args_term (snd r)"
definition funas_args_trs :: "('f, 'v) trs ⇒ 'f sig" where
"funas_args_trs R = (⋃r∈R. funas_args_rule r)"
lemmas funas_args_defs =
funas_args_trs_def funas_args_rule_def funas_args_term_def
definition roots_rule :: "('f, 'v) rule ⇒ 'f sig"
where
"roots_rule r = set_option (root (fst r)) ∪ set_option (root (snd r))"
definition roots_trs :: "('f, 'v) trs ⇒ 'f sig" where
"roots_trs R = (⋃r∈R. roots_rule r)"
lemmas roots_defs =
roots_trs_def roots_rule_def
definition funas_head :: "('f, 'v) trs ⇒ ('f, 'v) trs ⇒ 'f sig" where
"funas_head P R = funas_trs P - (funas_trs R ∪ funas_args_trs P)"
lemmas funs_defs = funs_trs_def funs_rule_def
lemmas funas_defs =
funas_trs_def funas_rule_def
funas_args_defs
funas_head_def
roots_defs
text ‹A function symbol is said to be \emph{defined} (w.r.t.\ to a given
TRS) if it occurs as root of some left-hand side.›
definition
defined :: "('f, 'v) trs ⇒ ('f × nat) ⇒ bool"
where
"defined R fn ⟷ (∃l r. (l, r) ∈ R ∧ root l = Some fn)"
lemma defined_funas_trs: assumes d: "defined R fn" shows "fn ∈ funas_trs R"
proof -
from d [unfolded defined_def] obtain l r
where "(l, r) ∈ R" and "root l = Some fn" by auto
then show ?thesis
unfolding funas_trs_def funas_rule_def [abs_def] by (cases l) force+
qed
lemma ctxt_closed_R_imp_supt_R_distr:
assumes "ctxt.closed R" and "s ⊳ t" and "(t, u) ∈ R" shows "∃t. (s, t) ∈ R ∧ t ⊳ u"
proof -
from ‹s ⊳ t› obtain C where "C ≠ □" and "C⟨t⟩ = s" by auto
from ‹ctxt.closed R› and ‹(t,u) ∈ R›
have RCtCu: "(C⟨t⟩,C⟨u⟩) ∈ R" by (rule ctxt.closedD)
from ‹C ≠ □› have "C⟨u⟩ ⊳ u" by auto
from RCtCu have "(s,C⟨u⟩) ∈ R" unfolding ‹C⟨t⟩ = s› .
from this and ‹C⟨u⟩ ⊳ u› show ?thesis by auto
qed
lemma ctxt_closed_imp_qc_supt: "ctxt.closed R ⟹ {⊳} O R ⊆ R O (R ∪ {⊳})⇧*" by blast
text ‹Let~$R$ be a relation on terms that is closed under contexts. If~$R$
is well-founded then $R \cup \rhd$ is well-founed.›
lemma SN_imp_SN_union_supt:
assumes "SN R" and "ctxt.closed R"
shows "SN (R ∪ {⊳})"
proof -
from ‹ctxt.closed R› have "quasi_commute R {⊳}"
unfolding quasi_commute_def by (rule ctxt_closed_imp_qc_supt)
have "SN {⊳}" by (rule SN_supt)
from ‹SN R› and ‹SN {⊳}› and ‹quasi_commute R {⊳}›
show ?thesis by (rule quasi_commute_imp_SN)
qed
lemma stable_loop_imp_not_SN:
assumes stable: "subst.closed r" and steps: "(s, s ⋅ σ) ∈ r⇧+"
shows "¬ SN_on r {s}"
proof -
let ?f = "λ i. s ⋅ (power.power Var (∘⇩s) σ i)"
have main: "⋀ i. (?f i, ?f (Suc i)) ∈ r⇧+"
proof -
fix i
show "(?f i, ?f (Suc i)) ∈ r⇧+"
proof (induct i, simp add: steps)
case (Suc i)
from Suc subst.closed_trancl[OF stable] have step: "(?f i ⋅ σ, ?f (Suc i) ⋅ σ) ∈ r⇧+" by auto
let ?σg = "power.power Var (∘⇩s) σ i"
let ?σgs = "power.power Var (∘⇩s) σ (Suc i)"
have idi: "?σg ∘⇩s σ = σ ∘⇩s ?σg" by (rule subst_monoid_mult.power_commutes)
have idsi: "?σgs ∘⇩s σ = σ ∘⇩s ?σgs" by (rule subst_monoid_mult.power_commutes)
have "?f i ⋅ σ = s ⋅ ?σg ∘⇩s σ" by simp
also have "… = ?f (Suc i)" unfolding idi by simp
finally have one: "?f i ⋅ σ = ?f (Suc i)" .
have "?f (Suc i) ⋅ σ = s ⋅ ?σgs ∘⇩s σ" by simp
also have "… = ?f (Suc (Suc i))" unfolding idsi by simp
finally have two: "?f (Suc i) ⋅ σ = ?f (Suc (Suc i))" by simp
show ?case using one two step by simp
qed
qed
then have "¬ SN_on (r⇧+) {?f 0}" unfolding SN_on_def by best
then show ?thesis using SN_on_trancl by force
qed
lemma subst_closed_supteq: "subst.closed {⊵}" by blast
lemma subst_closed_supt: "subst.closed {⊳}" by blast
lemma rstep_relcomp_idemp1 [simp]:
"rstep (rstep R O rstep S) = rstep R O rstep S"
proof -
{ fix s t
assume "(s, t) ∈ rstep (rstep R O rstep S)"
then have "(s, t) ∈ rstep R O rstep S"
by (induct) blast+ }
then show ?thesis by auto
qed
lemma rstep_relcomp_idemp2 [simp]:
"rstep (rstep R O rstep S O rstep T) = rstep R O rstep S O rstep T"
proof -
{ fix s t
assume "(s, t) ∈ rstep (rstep R O rstep S O rstep T)"
then have "(s, t) ∈ rstep R O rstep S O rstep T"
by (induct) blast+ }
then show ?thesis by auto
qed
lemma ctxt_closed_rsteps [intro]: "ctxt.closed ((rstep R)⇧*)" by blast
lemma subset_rstep: "R ⊆ rstep R" by auto
lemma subst_closure_rstep_subset: "subst.closure (rstep R) ⊆ rstep R"
by (auto elim: subst.closure.cases)
lemma subst_closed_rstep [intro]: "subst.closed (rstep R)" by blast
lemma subst_closed_rsteps: "subst.closed ((rstep R)⇧*)" by blast
lemma ctxt_closed_supt_subset: "ctxt.closed R ⟹ {⊳} O R ⊆ R O {⊳}" by blast
lemmas supt_rsteps_subset = ctxt_closed_supt_subset [OF ctxt_closed_rsteps]
lemma supteq_rsteps_subset:
"{⊵} O (rstep R)⇧* ⊆ (rstep R)⇧* O {⊵}" (is "?S ⊆ ?T")
using supt_rsteps_subset [of R] by (auto simp: supt_supteq_set_conv)
lemma quasi_commute_rsteps_supt:
"quasi_commute ((rstep R)⇧*) {⊳}"
unfolding quasi_commute_def using supt_rsteps_subset [of R] by auto
lemma rstep_UN:
"rstep (⋃i∈A. R i) = (⋃i∈A. rstep (R i))"
by (force)
definition
rstep_r_p_s :: "('f, 'v) trs ⇒ ('f, 'v) rule ⇒ pos ⇒ ('f, 'v) subst ⇒ ('f, 'v) trs"
where
"rstep_r_p_s R r p σ = {(s, t).
let C = ctxt_of_pos_term p s in p ∈ poss s ∧ r ∈ R ∧ (C⟨fst r ⋅ σ⟩ = s) ∧ (C⟨snd r ⋅ σ⟩ = t)}"
lemma rstep_r_p_s_def':
"rstep_r_p_s R r p σ = {(s, t).
p ∈ poss s ∧ r ∈ R ∧ s |_ p = fst r ⋅ σ ∧ t = replace_at s p (snd r ⋅ σ)}" (is "?l = ?r")
proof -
{ fix s t
have "((s,t) ∈ ?l) = ((s,t) ∈ ?r)"
unfolding rstep_r_p_s_def Let_def
using ctxt_supt_id [of p s] and subt_at_ctxt_of_pos_term [of p s "fst r ⋅ σ"] by auto }
then show ?thesis by auto
qed
lemma parallel_steps:
fixes p⇩1 :: pos
assumes "(s, t) ∈ rstep_r_p_s R⇩1 (l⇩1, r⇩1) p⇩1 σ⇩1"
and "(s, u) ∈ rstep_r_p_s R⇩2 (l⇩2, r⇩2) p⇩2 σ⇩2"
and par: "p⇩1 ⊥ p⇩2"
shows "(t, (ctxt_of_pos_term p⇩1 u)⟨r⇩1 ⋅ σ⇩1⟩) ∈ rstep_r_p_s R⇩2 (l⇩2, r⇩2) p⇩2 σ⇩2 ∧
(u, (ctxt_of_pos_term p⇩1 u)⟨r⇩1 ⋅ σ⇩1⟩) ∈ rstep_r_p_s R⇩1 (l⇩1, r⇩1) p⇩1 σ⇩1"
proof -
have p1: "p⇩1 ∈ poss s" and lr1: "(l⇩1, r⇩1) ∈ R⇩1" and σ1: "s |_ p⇩1 = l⇩1 ⋅ σ⇩1"
and t: "t = replace_at s p⇩1 (r⇩1 ⋅ σ⇩1)"
and p2: "p⇩2 ∈ poss s" and lr2: "(l⇩2, r⇩2) ∈ R⇩2" and σ2: "s |_ p⇩2 = l⇩2 ⋅ σ⇩2"
and u: "u = replace_at s p⇩2 (r⇩2 ⋅ σ⇩2)" using assms by (auto simp: rstep_r_p_s_def')
have "replace_at t p⇩2 (r⇩2 ⋅ σ⇩2) = replace_at u p⇩1 (r⇩1 ⋅ σ⇩1)"
using t and u and parallel_replace_at [OF ‹p⇩1 ⊥ p⇩2› p1 p2] by auto
moreover
have "(t, (ctxt_of_pos_term p⇩2 t)⟨r⇩2 ⋅ σ⇩2⟩) ∈ rstep_r_p_s R⇩2 (l⇩2, r⇩2) p⇩2 σ⇩2"
proof -
have "t |_ p⇩2 = l⇩2 ⋅ σ⇩2" using σ2 and parallel_replace_at_subt_at [OF par p1 p2] and t by auto
moreover have "p⇩2 ∈ poss t" using parallel_poss_replace_at [OF par p1] and t and p2 by auto
ultimately show ?thesis using lr2 and ctxt_supt_id [of p⇩2 t] by (simp add: rstep_r_p_s_def)
qed
moreover
have "(u, (ctxt_of_pos_term p⇩1 u)⟨r⇩1 ⋅ σ⇩1⟩) ∈ rstep_r_p_s R⇩1 (l⇩1, r⇩1) p⇩1 σ⇩1"
proof -
have par': "p⇩2 ⊥ p⇩1" using parallel_pos_sym [OF par] .
have "u |_ p⇩1 = l⇩1 ⋅ σ⇩1" using σ1 and parallel_replace_at_subt_at [OF par' p2 p1] and u by auto
moreover have "p⇩1 ∈ poss u" using parallel_poss_replace_at [OF par' p2] and u and p1 by auto
ultimately show ?thesis using lr1 and ctxt_supt_id [of p⇩1 u] by (simp add: rstep_r_p_s_def)
qed
ultimately show ?thesis by auto
qed
lemma rstep_iff_rstep_r_p_s:
"(s, t) ∈ rstep R ⟷ (∃l r p σ. (s, t) ∈ rstep_r_p_s R (l, r) p σ)" (is "?lhs = ?rhs")
proof
assume "(s, t) ∈ rstep R"
then obtain C σ l r where s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩" and "(l, r) ∈ R" by auto
let ?p = "hole_pos C"
let ?C = "ctxt_of_pos_term ?p s"
have C: "ctxt_of_pos_term ?p s = C" unfolding s by (induct C) simp_all
have "?p ∈ poss s" unfolding s by simp
moreover have "(l, r) ∈ R" by fact
moreover have "?C⟨l ⋅ σ⟩ = s" unfolding C by (simp add: s)
moreover have "?C⟨r ⋅ σ⟩ = t" unfolding C by (simp add: t)
ultimately show "?rhs" unfolding rstep_r_p_s_def Let_def by auto
next
assume "?rhs"
then obtain l r p σ where "p ∈ poss s"
and "(l, r) ∈ R"
and s[symmetric]: "(ctxt_of_pos_term p s)⟨l ⋅ σ⟩ = s"
and t[symmetric]: "(ctxt_of_pos_term p s)⟨r ⋅ σ⟩ = t"
unfolding rstep_r_p_s_def Let_def by auto
then show "?lhs" by auto
qed
lemma rstep_r_p_s_imp_rstep:
assumes "(s, t) ∈ rstep_r_p_s R r p σ"
shows "(s, t) ∈ rstep R"
using assms by (cases r) (auto simp: rstep_iff_rstep_r_p_s)
text ‹Rewriting steps below the root position.›
definition
nrrstep :: "('f, 'v) trs ⇒ ('f, 'v) trs"
where
"nrrstep R = {(s,t). ∃r i ps σ. (s,t) ∈ rstep_r_p_s R r (i#ps) σ}"
text ‹An alternative characterisation of non-root rewrite steps.›
lemma nrrstep_def':
"nrrstep R = {(s, t). ∃l r C σ. (l, r) ∈ R ∧ C ≠ □ ∧ s = C⟨l⋅σ⟩ ∧ t = C⟨r⋅σ⟩}"
(is "?lhs = ?rhs")
proof
show "?lhs ⊆ ?rhs"
proof (rule subrelI)
fix s t assume "(s, t) ∈ nrrstep R"
then obtain l r i ps σ where step: "(s, t) ∈ rstep_r_p_s R (l, r) (i # ps) σ"
unfolding nrrstep_def by best
let ?C = "ctxt_of_pos_term (i # ps) s"
from step have"i # ps ∈ poss s" and "(l, r) ∈ R" and "s = ?C⟨l⋅σ⟩" and "t = ?C⟨r⋅σ⟩"
unfolding rstep_r_p_s_def Let_def by auto
moreover from ‹i # ps ∈ poss s› have "?C ≠ □" by (induct s) auto
ultimately show "(s, t) ∈ ?rhs" by auto
qed
next
show "?rhs ⊆ ?lhs"
proof (rule subrelI)
fix s t assume "(s, t) ∈ ?rhs"
then obtain l r C σ where in_R: "(l, r) ∈ R" and "C ≠ □"
and s: "s = C⟨l⋅σ⟩" and t: "t = C⟨r⋅σ⟩" by auto
from ‹C ≠ □› obtain i p where ip: "hole_pos C = i # p" by (induct C) auto
have "i # p ∈ poss s" using hole_pos_poss[of C] unfolding s ip by simp
then have C: "C = ctxt_of_pos_term (i # p) s"
unfolding s ip[symmetric] by simp
from ‹i # p ∈ poss s› in_R s t have "(s, t) ∈ rstep_r_p_s R (l, r) (i # p) σ"
unfolding rstep_r_p_s_def C by simp
then show "(s, t) ∈ nrrstep R" unfolding nrrstep_def by best
qed
qed
lemma nrrstepI: "(l,r) ∈ R ⟹ s = C⟨l⋅σ⟩ ⟹ t = C⟨r ⋅ σ⟩ ⟹ C ≠ □ ⟹ (s,t) ∈ nrrstep R" unfolding nrrstep_def' by auto
lemma nrrstep_union: "nrrstep (R ∪ S) = nrrstep R ∪ nrrstep S"
unfolding nrrstep_def' by blast
lemma nrrstep_empty[simp]: "nrrstep {} = {}" unfolding nrrstep_def' by blast
text ‹Rewriting step at the root position.›
definition
rrstep :: "('f, 'v) trs ⇒ ('f, 'v) trs"
where
"rrstep R = {(s,t). ∃r σ. (s,t) ∈ rstep_r_p_s R r [] σ}"
text ‹An alternative characterisation of root rewrite steps.›
lemma rrstep_def': "rrstep R = {(s, t). ∃l r σ. (l, r) ∈ R ∧ s = l⋅σ ∧ t = r⋅σ}"
(is "_ = ?rhs")
by (auto simp: rrstep_def rstep_r_p_s_def)
lemma rules_subset_rrstep [simp]: "R ⊆ rrstep R"
by (force simp: rrstep_def' intro: exI [of _ Var])
lemma rrstep_union: "rrstep (R ∪ S) = rrstep R ∪ rrstep S" unfolding rrstep_def' by blast
lemma rrstep_empty[simp]: "rrstep {} = {}"
unfolding rrstep_def' by auto
lemma subst_closed_rrstep: "subst.closed (rrstep R)"
unfolding subst.closed_def
proof
fix ss ts
assume "(ss,ts) ∈ subst.closure (rrstep R)"
then show "(ss,ts) ∈ rrstep R"
proof
fix s t σ
assume ss: "ss = s ⋅ σ" and ts: "ts = t ⋅ σ" and step: "(s,t) ∈ rrstep R"
from step obtain l r δ where lr: "(l,r) ∈ R" and s: "s = l ⋅ δ" and t: "t = r ⋅ δ" unfolding rrstep_def' by auto
obtain sig where "sig = δ ∘⇩s σ" by auto
with ss s ts t have "ss = l ⋅ sig" and "ts = r ⋅ sig" by simp+
with lr show "(ss,ts) ∈ rrstep R" unfolding rrstep_def' by (auto simp: Let_def)
qed
qed
lemma rstep_iff_rrstep_or_nrrstep: "rstep R = (rrstep R ∪ nrrstep R)"
proof
show "rstep R ⊆ rrstep R ∪ nrrstep R"
proof (rule subrelI)
fix s t assume "(s,t) ∈ rstep R"
then obtain l r p σ where rstep_rps: "(s,t) ∈ rstep_r_p_s R (l,r) p σ"
by (auto simp: rstep_iff_rstep_r_p_s)
then show "(s,t) ∈ rrstep R ∪ nrrstep R" unfolding rrstep_def nrrstep_def by (cases p) auto
qed
next
show "rrstep R ∪ nrrstep R ⊆ rstep R"
proof (rule subrelI)
fix s t assume "(s,t) ∈ rrstep R ∪ nrrstep R"
then show "(s,t) ∈ rstep R" by (auto simp: rrstep_def nrrstep_def rstep_iff_rstep_r_p_s)
qed
qed
lemma rstep_i_pos_imp_rstep_arg_i_pos:
assumes nrrstep: "(Fun f ss,t) ∈ rstep_r_p_s R (l,r) (i#ps) σ"
shows "(ss!i,t|_[i]) ∈ rstep_r_p_s R (l,r) ps σ"
proof -
from nrrstep obtain C where C:"C = ctxt_of_pos_term (i#ps) (Fun f ss)"
and pos: "(i#ps) ∈ poss (Fun f ss)"
and Rlr: "(l,r) ∈ R"
and Fun: "C⟨l⋅σ⟩ = Fun f ss"
and t: "C⟨r⋅σ⟩ = t" unfolding rstep_r_p_s_def Let_def by auto
then obtain D where C':"C = More f (take i ss) D (drop (Suc i) ss)" by auto
then have CFun: "C⟨l⋅σ⟩ = Fun f (take i ss @ (D⟨l⋅σ⟩) # drop (Suc i) ss)" by auto
from pos have len: "i < length ss" by auto
from len
have "(take i ss @ (D⟨l⋅σ⟩) # drop (Suc i) ss)!i = D⟨l⋅σ⟩" by (auto simp: nth_append)
with C Fun CFun have ssi: "ss!i = D⟨l⋅σ⟩" by auto
from C' t have t': "t = Fun f (take i ss @ (D⟨r⋅σ⟩) # drop (Suc i) ss)" by auto
from len
have "(take i ss @ (D⟨r⋅σ⟩) # drop (Suc i) ss)!i = D⟨r⋅σ⟩" by (auto simp: nth_append)
with t' have "t|_[i] = (D⟨r⋅σ⟩)|_[]" by auto
then have subt_at: "t|_[i] = D⟨r⋅σ⟩" by simp
from C C' have "D = ctxt_of_pos_term ps (ss!i)" by auto
with pos Rlr ssi[symmetric] subt_at[symmetric]
show ?thesis unfolding rstep_r_p_s_def Let_def by auto
qed
lemma ctxt_closure_rstep_eq [simp]: "ctxt.closure (rstep R) = rstep R"
by (rule ctxt.closure_id) blast
lemma subst_closure_rstep_eq [simp]: "subst.closure (rstep R) = rstep R"
by (rule subst.closure_id) blast
lemma supt_rstep_subset:
"{⊳} O rstep R ⊆ rstep R O {⊳}"
proof (rule subrelI)
fix s t assume "(s,t) ∈ {⊳} O rstep R" then show "(s,t) ∈ rstep R O {⊳}"
proof (induct s)
case (Var x)
then have "∃u. Var x ⊳ u ∧ (u,t) ∈ rstep R" by auto
then obtain u where "Var x ⊳ u" and "(u,t) ∈ rstep R" by auto
from ‹Var x ⊳ u› show ?case by (cases rule: supt.cases)
next
case (Fun f ss)
then obtain u where "Fun f ss ⊳ u" and "(u,t) ∈ rstep R" by auto
from ‹Fun f ss ⊳ u› obtain C
where "C ≠ □" and "C⟨u⟩ = Fun f ss" by auto
from ‹C ≠ □› have "C⟨t⟩ ⊳ t" by (rule nectxt_imp_supt_ctxt)
from ‹(u,t) ∈ rstep R› have "(C⟨u⟩,C⟨t⟩) ∈ rstep R" ..
then have "(Fun f ss,C⟨t⟩) ∈ rstep R" unfolding ‹C⟨u⟩ = Fun f ss› .
with ‹C⟨t⟩ ⊳ t› show ?case by auto
qed
qed
lemma ne_rstep_seq_imp_list_of_terms:
assumes "(s,t) ∈ (rstep R)⇧+"
shows "∃ts. length ts > 1 ∧ ts!0 = s ∧ ts!(length ts - 1) = t ∧
(∀i<length ts - 1. (ts!i,ts!(Suc i)) ∈ (rstep R))" (is "∃ts. _ ∧ _ ∧ _ ∧ ?P ts")
using assms
proof (induct rule: trancl.induct)
case (r_into_trancl x y)
let ?ts = "[x,y]"
have "length ?ts > 1" by simp
moreover have "?ts!0 = x" by simp
moreover have "?ts!(length ?ts - 1) = y" by simp
moreover from r_into_rtrancl r_into_trancl have "?P ?ts" by auto
ultimately show ?case by fast
next
case (trancl_into_trancl x y z)
then obtain ts where "length ts > 1" and "ts!0 = x"
and last1: "ts!(length ts - 1) = y" and "?P ts" by auto
let ?ts = "ts@[z]"
have len: "length ?ts = length ts + 1" by simp
from ‹length ts > 1› have "length ?ts > 1" by auto
moreover with ‹ts!0 = x› have "?ts!0 = x" by (induct ts) auto
moreover have last2: "?ts!(length ?ts - 1) = z" by simp
moreover have "?P ?ts"
proof (intro allI impI)
fix i assume A: "i < length ?ts - 1"
show "(?ts!i,?ts!(Suc i)) ∈ rstep R"
proof (cases "i < length ts - 1")
case True with ‹?P ts› A show ?thesis unfolding len unfolding nth_append by auto
next
case False with A have "i = length ts - 1" by simp
with last1 ‹length ts > 1› have "?ts!i = y" unfolding nth_append by auto
have "Suc i = length ?ts - 1" using ‹i = length ts - 1› using ‹length ts > 1› by auto
with last2 have "?ts!(Suc i) = z" by auto
from ‹(y,z) ∈ rstep R› show ?thesis unfolding ‹?ts!(Suc i) = z› ‹?ts!i = y› .
qed
qed
ultimately show ?case by fast
qed
locale E_compatible =
fixes R :: "('f,'v)trs" and E :: "('f,'v)trs"
assumes E: "E O R = R" "Id ⊆ E"
begin
definition restrict_SN_supt_E :: "('f, 'v) trs" where
"restrict_SN_supt_E = restrict_SN R R ∪ restrict_SN (E O {⊳} O E) R"
lemma ctxt_closed_R_imp_supt_restrict_SN_E_distr:
assumes "ctxt.closed R"
and "(s,t) ∈ (restrict_SN (E O {⊳}) R)"
and "(t,u) ∈ restrict_SN R R"
shows "(∃t. (s,t) ∈ restrict_SN R R ∧ (t,u) ∈ restrict_SN (E O {⊳}) R)" (is "∃ t. _ ∧ (t,u) ∈ ?snSub")
proof -
from ‹(s,t) ∈ ?snSub› obtain v where "SN_on R {s}" and ac: "(s,v) ∈ E" and "v ⊳ t" unfolding restrict_SN_def supt_def by auto
from ‹v ⊳ t› obtain C where "C ≠ Hole" and v: "C⟨t⟩ = v" by best
from ‹(t,u) ∈ restrict_SN R R› have "(t,u) ∈ R" unfolding restrict_SN_def by auto
from ‹ctxt.closed R› and this have RCtCu: "(C⟨t⟩,C⟨u⟩) ∈ R" by (rule ctxt.closedD)
with v ac have "(s,C⟨u⟩) ∈ E O R" by auto
then have sCu: "(s,C⟨u⟩) ∈ R" using E by simp
with ‹SN_on R {s}› have one: "SN_on R {C⟨u⟩}"
using step_preserves_SN_on[of "s" "C⟨u⟩" R] by blast
from ‹C ≠ □› have "C⟨u⟩ ⊳ u" by auto
with one E have "(C⟨u⟩,u) ∈ ?snSub" unfolding restrict_SN_def supt_def by auto
from sCu and ‹SN_on R {s}› and ‹(C⟨u⟩,u) ∈ ?snSub› show ?thesis unfolding restrict_SN_def by auto
qed
lemma ctxt_closed_R_imp_restrict_SN_qc_E_supt:
assumes ctxt: "ctxt.closed R"
shows "quasi_commute (restrict_SN R R) (restrict_SN (E O {⊳} O E) R)" (is "quasi_commute ?r ?s")
proof -
have "?s O ?r ⊆ ?r O (?r ∪ ?s)⇧*"
proof (rule subrelI)
fix x y
assume "(x,y) ∈ ?s O ?r"
from this obtain z where "(x,z) ∈ ?s" and "(z,y) ∈ ?r" by best
then obtain v w where ac: "(x,v) ∈ E" and vw: "v ⊳ w" and wz: "(w,z) ∈ E" and zy: "(z,y) ∈ R" and "SN_on R {x}" unfolding restrict_SN_def supt_def
using E(2) by auto
from wz zy have "(w,y) ∈ E O R" by auto
with E have wy: "(w,y) ∈ R" by auto
from ctxt_closed_R_imp_supt_R_distr[OF ctxt vw wy] obtain w where "(v,w) ∈ R" and "w ⊳ y" using ctxt_closed_R_imp_supt_R_distr[where R = R and s = v and t = z and u = y] by auto
with ac E have "(x,w) ∈ R" and "w ⊳ y" by auto
from this and ‹SN_on R {x}› have "SN_on R {w}" using step_preserves_SN_on
unfolding supt_supteq_conv by auto
with ‹w ⊳ y› E have "(w,y) ∈ ?s" unfolding restrict_SN_def supt_def by force
with ‹(x,w) ∈ R› ‹SN_on R {x}› show "(x,y) ∈ ?r O (?r ∪ ?s)⇧*" unfolding restrict_SN_def by auto
qed
then show ?thesis unfolding quasi_commute_def .
qed
lemma ctxt_closed_imp_SN_restrict_SN_E_supt:
assumes "ctxt.closed R"
and SN: "SN (E O {⊳} O E)"
shows "SN restrict_SN_supt_E"
proof -
let ?r = "restrict_SN R R"
let ?s = "restrict_SN (E O {⊳} O E) R"
from ‹ctxt.closed R› have "quasi_commute ?r ?s"
by (rule ctxt_closed_R_imp_restrict_SN_qc_E_supt)
from SN have "SN ?s" by (rule SN_subset, auto simp: restrict_SN_def)
have "SN ?r" by (rule SN_restrict_SN_idemp)
from ‹SN ?r› and ‹SN ?s› and ‹quasi_commute ?r ?s›
show ?thesis unfolding restrict_SN_supt_E_def by (rule quasi_commute_imp_SN)
qed
end
lemma E_compatible_Id: "E_compatible R Id"
by standard auto
definition restrict_SN_supt :: "('f, 'v) trs ⇒ ('f, 'v) trs" where
"restrict_SN_supt R = restrict_SN R R ∪ restrict_SN {⊳} R"
lemma ctxt_closed_SN_on_subt:
assumes "ctxt.closed R" and "SN_on R {s}" and "s ⊵ t"
shows "SN_on R {t}"
proof (rule ccontr)
assume "¬ SN_on R {t}"
then obtain A where "A 0 = t" and "∀i. (A i,A (Suc i)) ∈ R"
unfolding SN_on_def by best
from ‹s ⊵ t› obtain C where "s = C⟨t⟩" by auto
let ?B = "λi. C⟨A i⟩"
have "∀i. (?B i,?B(Suc i)) ∈ R"
proof
fix i
from ‹∀i. (A i,A(Suc i)) ∈ R› have "(?B i,?B(Suc i)) ∈ ctxt.closure(R)" by fast
then show "(?B i,?B(Suc i)) ∈ R" using ‹ctxt.closed R› by auto
qed
with ‹A 0 = t› have "?B 0 = s ∧ (∀i. (?B i,?B(Suc i)) ∈ R)" unfolding ‹s = C⟨t⟩› by auto
then have "¬ SN_on R {s}" unfolding SN_on_def by auto
with assms show "False" by simp
qed
lemma ctxt_closed_R_imp_supt_restrict_SN_distr:
assumes R: "ctxt.closed R"
and st: "(s,t) ∈ (restrict_SN {⊳} R)"
and tu: "(t,u) ∈ restrict_SN R R"
shows "(∃t. (s,t) ∈ restrict_SN R R ∧ (t,u) ∈ restrict_SN {⊳} R)" (is "∃ t. _ ∧ (t,u) ∈ ?snSub")
using E_compatible.ctxt_closed_R_imp_supt_restrict_SN_E_distr[OF E_compatible_Id R _ tu, of s]
st by auto
lemma ctxt_closed_R_imp_restrict_SN_qc_supt:
assumes "ctxt.closed R"
shows "quasi_commute (restrict_SN R R) (restrict_SN supt R)" (is "quasi_commute ?r ?s")
using E_compatible.ctxt_closed_R_imp_restrict_SN_qc_E_supt[OF E_compatible_Id assms] by auto
lemma ctxt_closed_imp_SN_restrict_SN_supt:
assumes "ctxt.closed R"
shows "SN (restrict_SN_supt R)"
using E_compatible.ctxt_closed_imp_SN_restrict_SN_E_supt[OF E_compatible_Id assms]
unfolding E_compatible.restrict_SN_supt_E_def[OF E_compatible_Id] restrict_SN_supt_def
using SN_supt by auto
lemma SN_restrict_SN_supt_rstep:
shows "SN (restrict_SN_supt (rstep R))"
proof -
have "ctxt.closed (rstep R)" by (rule ctxt_closed_rstep)
then show ?thesis by (rule ctxt_closed_imp_SN_restrict_SN_supt)
qed
lemma nrrstep_imp_pos_term:
"(Fun f ss,t) ∈ nrrstep R ⟹
∃i s. t = Fun f (ss[i:=s]) ∧ (ss!i,s) ∈ rstep R ∧ i < length ss"
proof -
assume "(Fun f ss,t) ∈ nrrstep R"
then obtain l r i ps σ where rstep_rps:"(Fun f ss,t) ∈ rstep_r_p_s R (l,r) (i#ps) σ"
unfolding nrrstep_def by auto
then obtain C
where "(l,r) ∈ R"
and pos: "(i#ps) ∈ poss (Fun f ss)"
and C: "C = ctxt_of_pos_term (i#ps) (Fun f ss)"
and "C⟨l⋅σ⟩ = Fun f ss"
and t: "C⟨r⋅σ⟩ = t"
unfolding rstep_r_p_s_def Let_def by auto
then obtain D where "C = More f (take i ss) D (drop (Suc i) ss)" by auto
with t have t': "t = Fun f (take i ss @ (D⟨r⋅σ⟩) # drop (Suc i) ss)" by auto
from rstep_rps have "(ss!i,t|_[i]) ∈ rstep_r_p_s R (l,r) ps σ"
by (rule rstep_i_pos_imp_rstep_arg_i_pos)
then have rstep:"(ss!i,t|_[i]) ∈ rstep R" by (auto simp: rstep_iff_rstep_r_p_s)
then have "(C⟨ss!i⟩,C⟨t|_[i]⟩) ∈ rstep R" ..
from pos have len: "i < length ss" by auto
from len
have "(take i ss @ (D⟨r⋅σ⟩) # drop (Suc i) ss)!i = D⟨r⋅σ⟩" by (auto simp: nth_append)
with C t' have "t|_[i] = D⟨r⋅σ⟩" by auto
with t' have "t = Fun f (take i ss @ (t|_[i]) # drop (Suc i) ss)" by auto
with len have "t = Fun f (ss[i:=t|_[i]])" by (auto simp: upd_conv_take_nth_drop)
with rstep len show "∃i s. t = Fun f (ss[i:=s]) ∧ (ss!i,s) ∈ rstep R ∧ i < length ss" by auto
qed
lemma rstep_cases[consumes 1, case_names root nonroot]:
"⟦(s,t) ∈ rstep R; (s,t) ∈ rrstep R ⟹ P; (s,t) ∈ nrrstep R ⟹ P⟧ ⟹ P"
by (auto simp: rstep_iff_rrstep_or_nrrstep)
lemma nrrstep_imp_rstep: "(s,t) ∈ nrrstep R ⟹ (s,t) ∈ rstep R"
by (auto simp: rstep_iff_rrstep_or_nrrstep)
lemma nrrstep_imp_Fun: "(s,t) ∈ nrrstep R ⟹ ∃f ss. s = Fun f ss"
proof -
assume "(s,t) ∈ nrrstep R"
then obtain i ps where "i#ps ∈ poss s"
unfolding nrrstep_def rstep_r_p_s_def Let_def by auto
then show "∃f ss. s = Fun f ss" by (cases s) auto
qed
lemma nrrstep_imp_subt_rstep:
assumes "(s,t) ∈ nrrstep R"
shows "∃i. i < num_args s ∧ num_args s = num_args t ∧ (s|_[i],t|_[i]) ∈ rstep R ∧ (∀j. i ≠ j ⟶ s|_[j] = t|_[j])"
proof -
from ‹(s,t) ∈ nrrstep R› obtain f ss where "s = Fun f ss" using nrrstep_imp_Fun by blast
with ‹(s,t) ∈ nrrstep R› have "(Fun f ss,t) ∈ nrrstep R" by simp
then obtain i u where "t = Fun f (ss[i := u])" and "(ss!i,u) ∈ rstep R" and "i < length ss"
using nrrstep_imp_pos_term by best
from ‹s = Fun f ss› and ‹t = Fun f (ss[i := u])› have "num_args s = num_args t" by auto
from ‹i < length ss› and ‹s = Fun f ss› have "i < num_args s" by auto
from ‹s = Fun f ss› have "s|_[i] = (ss!i)" by auto
from ‹t = Fun f (ss[i := u])› and ‹i < length ss› have "t|_[i] = u" by auto
from ‹s = Fun f ss› and ‹t = Fun f (ss[i := u])›
have "∀j. j ≠ i ⟶ s|_[j] = t|_[j]" by auto
with ‹(ss!i,u) ∈ rstep R›
and ‹i < num_args s›
and ‹num_args s = num_args t›
and ‹s|_[i] = (ss!i)›[symmetric] and ‹t|_[i] = u›[symmetric]
show ?thesis by (auto)
qed
lemma finite_range:
fixes f::"nat ⇒ 'a"
assumes "finite (range f)"
shows "∃x. ∃⇩∞i. f i = x"
proof (rule ccontr)
assume "¬(∃x. ∃⇩∞i. f i = x)"
then have "∀x. ∃j. ∀i>j. f i ≠ x" unfolding INFM_nat by blast
from choice[OF this] obtain j where neq: "∀x. ∀i>j x. f i ≠ x" ..
from finite_range_imageI[OF assms] have "finite (range (j ∘ f))" by (simp add: comp_def)
from finite_nat_bounded[OF this] obtain m where "range (j ∘ f) ⊆ {..<m}" ..
then have "j (f m) < m" by (auto simp: comp_def)
with neq show False by blast
qed
lemma nrrstep_subt: assumes "(s, t) ∈ nrrstep R" shows "∃u⊲s. ∃v⊲t. (u, v) ∈ rstep R"
proof -
from assms obtain l r C σ where "(l, r) ∈ R" and "C ≠ □"
and s: "s = C⟨l⋅σ⟩" and t: "t = C⟨r⋅σ⟩" unfolding nrrstep_def' by best
from ‹C ≠ □› s have "s ⊳ l⋅σ" by auto
moreover from ‹C ≠ □› t have "t ⊳ r⋅σ" by auto
moreover from ‹(l, r) ∈ R› have "(l⋅σ, r⋅σ) ∈ rstep R" by auto
ultimately show ?thesis by auto
qed
lemma nrrstep_args:
assumes "(s, t) ∈ nrrstep R"
shows "∃f ss ts. s = Fun f ss ∧ t = Fun f ts ∧ length ss = length ts
∧ (∃j<length ss. (ss!j, ts!j) ∈ rstep R ∧ (∀i<length ss. i ≠ j ⟶ ss!i = ts!i))"
proof -
from assms obtain l r C σ where "(l, r) ∈ R" and "C ≠ □"
and s: "s = C⟨l⋅σ⟩" and t: "t = C⟨r⋅σ⟩" unfolding nrrstep_def' by best
from ‹C ≠ □› obtain f ss1 D ss2 where C: "C = More f ss1 D ss2" by (induct C) auto
have "s = Fun f (ss1 @ D⟨l⋅σ⟩ # ss2)" (is "_ = Fun f ?ss") by (simp add: s C)
moreover have "t = Fun f (ss1 @ D⟨r⋅σ⟩ # ss2)" (is "_ = Fun f ?ts") by (simp add: t C)
moreover have "length ?ss = length ?ts" by simp
moreover have "∃j<length ?ss.
(?ss!j, ?ts!j) ∈ rstep R ∧ (∀i<length ?ss. i ≠ j ⟶ ?ss!i = ?ts!i)"
proof -
let ?j = "length ss1"
have "?j < length ?ss" by simp
moreover have "(?ss!?j, ?ts!?j) ∈ rstep R"
proof -
from ‹(l, r) ∈ R› have "(D⟨l⋅σ⟩, D⟨r⋅σ⟩) ∈ rstep R" by auto
then show ?thesis by auto
qed
moreover have "∀i<length ?ss. i ≠ ?j ⟶ ?ss!i = ?ts!i" (is "∀i<length ?ss. _ ⟶ ?P i")
proof (intro allI impI)
fix i assume "i < length ?ss" and "i ≠ ?j"
then have "i < length ss1 ∨ length ss1 < i" by auto
then show "?P i"
proof
assume "i < length ss1" then show "?P i" by (auto simp: nth_append)
next
assume "i > length ss1" then show "?P i"
using ‹i < length ?ss› by (auto simp: nth_Cons' nth_append)
qed
qed
ultimately show ?thesis by best
qed
ultimately show ?thesis by auto
qed
lemma nrrstep_iff_arg_rstep:
"(s,t) ∈ nrrstep R ⟷
(∃f ss i t'. s = Fun f ss ∧ i < length ss ∧ t = Fun f (ss[i:=t']) ∧ (ss!i,t') ∈ rstep R)"
(is "?L ⟷ ?R")
proof
assume L: ?L
from nrrstep_args[OF this]
obtain f ss ts where "s = Fun f ss" "t = Fun f ts" by auto
with nrrstep_imp_pos_term[OF L[unfolded this]]
show ?R by auto
next assume R: ?R
then obtain f i ss t'
where s: "s = Fun f ss" and t: "t = Fun f (ss[i:=t'])"
and i: "i < length ss" and st': "(ss ! i, t') ∈ rstep R" by auto
from st' obtain C l r σ where lr: "(l, r) ∈ R" and s': "ss!i = C⟨l ⋅ σ⟩" and t': "t' = C⟨r ⋅ σ⟩" by auto
let ?D = "More f (take i ss) C (drop (Suc i) ss)"
have "s = ?D⟨l ⋅ σ⟩" "t = ?D⟨r ⋅ σ⟩" unfolding s t
using id_take_nth_drop[OF i] upd_conv_take_nth_drop[OF i] s' t' by auto
with lr show ?L apply(rule nrrstepI) using t' by auto
qed
lemma subterms_NF_imp_SN_on_nrrstep:
assumes "∀s⊲t. s ∈ NF (rstep R)" shows "SN_on (nrrstep R) {t}"
proof
fix S assume "S 0 ∈ {t}" and "∀i. (S i, S (Suc i)) ∈ nrrstep R"
then have "(t, S (Suc 0)) ∈ nrrstep R" by auto
then obtain l r C σ where "(l, r) ∈ R" and "C ≠ □" and t: "t = C⟨l⋅σ⟩" unfolding nrrstep_def' by auto
then obtain f ss1 D ss2 where C: "C = More f ss1 D ss2" by (induct C) auto
have "t ⊳ D⟨l⋅σ⟩" unfolding t C by auto
moreover have "D⟨l⋅σ⟩ ∉ NF (rstep R)"
proof -
from ‹(l, r) ∈ R› have "(D⟨l⋅σ⟩, D⟨r⋅σ⟩) ∈ rstep R" by auto
then show ?thesis by auto
qed
ultimately show False using assms by simp
qed
lemma args_NF_imp_SN_on_nrrstep:
assumes "∀t∈set ts. t ∈ NF (rstep R)" shows "SN_on (nrrstep R) {Fun f ts}"
proof
fix S assume "S 0 ∈ {Fun f ts}" and "∀i. (S i, S (Suc i)) ∈ nrrstep R"
then have "(Fun f ts, S (Suc 0)) ∈ nrrstep R"
unfolding singletonD[OF ‹S 0 ∈ {Fun f ts}›, symmetric] by simp
then obtain l r C σ where "(l, r) ∈ R" and "C ≠ □" and "Fun f ts = C⟨l⋅σ⟩"
unfolding nrrstep_def' by auto
then obtain ss1 D ss2 where C: "C = More f ss1 D ss2" by (induct C) auto
with ‹Fun f ts = C⟨l⋅σ⟩› have "D⟨l⋅σ⟩ ∈ set ts" by auto
moreover have "D⟨l⋅σ⟩ ∉ NF (rstep R)"
proof -
from ‹(l, r) ∈ R› have "(D⟨l⋅σ⟩, D⟨r⋅σ⟩) ∈ rstep R" by auto
then show ?thesis by auto
qed
ultimately show False using assms by simp
qed
lemma rrstep_imp_rule_subst:
assumes "(s,t) ∈ rrstep R"
shows "∃l r σ. (l,r) ∈ R ∧ (l⋅σ) = s ∧ (r⋅σ) = t"
proof -
have "ctxt_of_pos_term [] s = Hole" by auto
obtain l r σ where "(s,t) ∈ rstep_r_p_s R (l,r) [] σ" using assms unfolding rrstep_def by best
then have "let C = ctxt_of_pos_term [] s in [] ∈ poss s ∧ (l,r) ∈ R ∧ C⟨l⋅σ⟩ = s ∧ C⟨r⋅σ⟩ = t" unfolding rstep_r_p_s_def by simp
with ‹ctxt_of_pos_term [] s = Hole› have "(l,r) ∈ R" and "l⋅σ = s" and "r⋅σ = t" unfolding Let_def by auto
then show ?thesis by auto
qed
lemma nrrstep_preserves_root:
assumes "(Fun f ss,t) ∈ nrrstep R" (is "(?s,t) ∈ nrrstep R") shows "∃ts. t = (Fun f ts)"
using assms unfolding nrrstep_def rstep_r_p_s_def Let_def by auto
lemma nrrstep_equiv_root: assumes "(s,t) ∈ nrrstep R" shows "∃f ss ts. s = Fun f ss ∧ t = Fun f ts"
proof -
from assms obtain f ss where "s = Fun f ss" using nrrstep_imp_Fun by best
with assms obtain ts where "t = Fun f ts" using nrrstep_preserves_root by best
from ‹s = Fun f ss› and ‹t = Fun f ts› show ?thesis by best
qed
lemma nrrstep_reflects_root:
assumes "(s,Fun g ts) ∈ nrrstep R" (is "(s,?t) ∈ nrrstep R")
shows "∃ss. s = (Fun g ss)"
proof -
from assms obtain f ss ts' where "s = Fun f ss" and "Fun g ts = Fun f ts'" using nrrstep_equiv_root by best
then have "f = g" by simp
with ‹s = Fun f ss› have "s = Fun g ss" by simp
then show ?thesis by auto
qed
lemma nrrsteps_preserve_root:
assumes "(Fun f ss,t) ∈ (nrrstep R)⇧*"
shows "∃ts. t = (Fun f ts)"
using assms by induct (auto simp: nrrstep_preserves_root)
lemma nrrstep_Fun_imp_arg_rsteps:
assumes "(Fun f ss,Fun f ts) ∈ nrrstep R" (is "(?s,?t) ∈ nrrstep R") and "i < length ss"
shows "(ss!i,ts!i) ∈ (rstep R)⇧*"
proof -
from assms have "[i] ∈ poss ?s" using empty_pos_in_poss by simp
from ‹(?s,?t) ∈ nrrstep R›
obtain l r j ps σ
where A: "let C = ctxt_of_pos_term (j#ps) ?s in (j#ps) ∈ poss ?s ∧ (l,r) ∈ R ∧ C⟨l⋅σ⟩ = ?s ∧ C⟨r⋅σ⟩ = ?t" unfolding nrrstep_def rstep_r_p_s_def by force
let ?C = "ctxt_of_pos_term (j#ps) ?s"
from A have "(j#ps) ∈ poss ?s" and "(l,r) ∈ R" and "?C⟨l⋅σ⟩ = ?s" and "?C⟨r⋅σ⟩ = ?t" using Let_def by auto
have C: "?C = More f (take j ss) (ctxt_of_pos_term ps (ss!j)) (drop (Suc j) ss)" (is "?C = More f ?ss1 ?D ?ss2") by auto
from ‹?C⟨l⋅σ⟩ = ?s› have "?D⟨l⋅σ⟩ = (ss!j)" by (auto simp: take_drop_imp_nth)
from ‹(l,r) ∈ R› have "(l⋅σ,r⋅σ) ∈ (subst.closure R)" by auto
then have "(?D⟨l⋅σ⟩,?D⟨r⋅σ⟩) ∈ (ctxt.closure(subst.closure R))"
and "(?C⟨l⋅σ⟩,?C⟨r⋅σ⟩) ∈ (ctxt.closure(subst.closure R))" by (auto simp only: ctxt.closure.intros)
then have D_rstep: "(?D⟨l⋅σ⟩,?D⟨r⋅σ⟩) ∈ rstep R" and "(?C⟨l⋅σ⟩,?C⟨r⋅σ⟩) ∈ rstep R"
unfolding rstep_eq_closure by auto
from ‹?C⟨r⋅σ⟩ = ?t› and C have "?t = Fun f (take j ss @ ?D⟨r⋅σ⟩ # drop (Suc j) ss)" by auto
then have ts: "ts = (take j ss @ ?D⟨r⋅σ⟩ # drop (Suc j) ss)" by auto
have "j = i ∨ j ≠ i" by simp
from ‹j#ps ∈ poss ?s› have "j < length ss" by simp
then have "(take j ss @ ?D⟨r⋅σ⟩ # drop (Suc j) ss) ! j = ?D⟨r⋅σ⟩" by (auto simp: nth_append_take)
with ts have "ts!j = ?D⟨r⋅σ⟩" by auto
have "j = i ∨ j ≠ i" by simp
then show "(ss!i,ts!i) ∈ (rstep R)⇧*"
proof
assume "j = i"
with ‹ts!j = ?D⟨r⋅σ⟩› and ‹?D⟨l⋅σ⟩ = ss!j› and D_rstep show ?thesis by auto
next
assume "j ≠ i"
with ‹i < length ss› and ‹j < length ss› have "(take j ss @ ?D⟨r⋅σ⟩ # drop (Suc j) ss) ! i = ss!i" by (auto simp: nth_append_take_drop_is_nth_conv)
with ts have "ts!i = ss!i" by auto
then show ?thesis by auto
qed
qed
lemma nrrstep_imp_arg_rsteps:
assumes "(s,t) ∈ nrrstep R" and "i < num_args s" shows "(args s!i,args t!i) ∈ (rstep R)⇧*"
proof (cases s)
fix x assume "s = Var x" then show ?thesis using assms by auto
next
fix f ss assume "s = Fun f ss"
then have "(Fun f ss,t) ∈ nrrstep R" using assms by simp
then obtain ts where "t = Fun f ts" using nrrstep_preserves_root by best
with ‹(s,t) ∈ nrrstep R› and ‹s = Fun f ss› have "(Fun f ss,Fun f ts) ∈ nrrstep R" by simp
from ‹s = Fun f ss› and ‹i < num_args s› have "i < length ss" by simp
with ‹(Fun f ss,Fun f ts) ∈ nrrstep R›
have "(ss!i,ts!i) ∈ (rstep R)⇧*" by (rule nrrstep_Fun_imp_arg_rsteps)
with ‹s = Fun f ss› and ‹t = Fun f ts› show ?thesis by simp
qed
lemma nrrsteps_imp_rsteps: "(s,t) ∈ (nrrstep R)⇧* ⟹ (s,t) ∈ (rstep R)⇧*"
proof (induct rule: rtrancl.induct)
case (rtrancl_refl a) then show ?case by simp
next
case (rtrancl_into_rtrancl a b c)
then have IH: "(a,b) ∈ (rstep R)⇧*" and nrrstep: "(b,c) ∈ nrrstep R" by auto
from nrrstep have "(b,c) ∈ rstep R" using nrrstep_imp_rstep by auto
with IH show ?case by auto
qed
lemma nrrstep_Fun_preserves_num_args:
assumes "(Fun f ss,Fun f ts) ∈ nrrstep R" (is "(?s,?t) ∈ nrrstep R")
shows "length ss = length ts"
proof -
from assms obtain l r i ps σ
where "let C = ctxt_of_pos_term (i#ps) ?s in (i#ps) ∈ poss ?s ∧ (l,r) ∈ R ∧ C⟨l⋅σ⟩ = ?s ∧ C⟨r⋅σ⟩ = ?t" (is "let C = ?C in _")
unfolding nrrstep_def rstep_r_p_s_def by force
then have "(l,r) ∈ R" and Cl: "?C⟨l⋅σ⟩ = ?s" and Cr: "?C⟨r⋅σ⟩ = ?t" unfolding Let_def by auto
have C: "?C = More f (take i ss) (ctxt_of_pos_term ps (ss!i)) (drop (Suc i) ss)" (is "?C = More f ?ss1 ?D ?ss2") by simp
from C and Cl have s: "?s = Fun f (take i ss @ ?D⟨l⋅σ⟩ # drop (Suc i) ss)" (is "?s = Fun f ?ss") by simp
from C and Cr have t: "?t = Fun f (take i ss @ ?D⟨r⋅σ⟩ # drop (Suc i) ss)" (is "?t = Fun f ?ts") by simp
from s and t have ss: "ss = ?ss" and ts: "ts = ?ts" by auto
have "length ?ss = length ?ts" by auto
with ss and ts show ?thesis by simp
qed
lemma nrrstep_equiv_num_args:
assumes "(s,t) ∈ nrrstep R" shows "num_args s = num_args t"
proof -
from assms obtain f ss ts where s:"s = Fun f ss" and t:"t = Fun f ts" using nrrstep_equiv_root by best
with assms have "(Fun f ss,Fun f ts) ∈ nrrstep R" by simp
then have "length ss = length ts" by (rule nrrstep_Fun_preserves_num_args)
with s and t show ?thesis by auto
qed
lemma nrrsteps_equiv_num_args:
assumes "(s,t) ∈ (nrrstep R)⇧*" shows "num_args s = num_args t"
using assms by (induct, auto simp: nrrstep_equiv_num_args)
lemma nrrstep_preserves_num_args:
assumes "(s,t) ∈ nrrstep R" and "i < num_args s" shows "i < num_args t"
proof (cases s)
fix x assume "s = Var x" then show ?thesis using assms by auto
next
fix f ss assume "s = Fun f ss"
with assms obtain ts where "t = Fun f ts" using nrrstep_preserves_root by best
from ‹(s,t) ∈ nrrstep R› have "length ss = length ts" unfolding ‹s = Fun f ss› and ‹t = Fun f ts› by (rule nrrstep_Fun_preserves_num_args)
with assms and ‹s = Fun f ss› and ‹t = Fun f ts› show ?thesis by auto
qed
lemma nrrstep_reflects_num_args:
assumes "(s,t) ∈ nrrstep R" and "i < num_args t" shows "i < num_args s"
proof (cases t)
fix x assume "t = Var x" then show ?thesis using assms by auto
next
fix g ts assume "t = Fun g ts"
with assms obtain ss where "s = Fun g ss" using nrrstep_reflects_root by best
from ‹(s,t) ∈ nrrstep R› have "length ss = length ts" unfolding ‹s = Fun g ss› and ‹t = Fun g ts› by (rule nrrstep_Fun_preserves_num_args)
with assms and ‹s = Fun g ss› and ‹t = Fun g ts› show ?thesis by auto
qed
lemma nrrsteps_imp_arg_rsteps:
assumes "(s,t) ∈ (nrrstep R)⇧*" and "i < num_args s"
shows "(args s!i,args t!i) ∈ (rstep R)⇧*"
using assms
proof (induct rule: rtrancl.induct)
case (rtrancl_refl a) then show ?case by auto
next
case (rtrancl_into_rtrancl a b c)
then have IH: "(args a!i,args b!i) ∈ (rstep R)⇧*" by auto
from ‹(a,b) ∈ (nrrstep R)⇧*› and ‹i < num_args a› have "i < num_args b" by induct (auto simp: nrrstep_preserves_num_args)
with ‹(b,c) ∈ nrrstep R›
have "(args b!i,args c!i) ∈ (rstep R)⇧*" by (rule nrrstep_imp_arg_rsteps)
with IH show ?case by simp
qed
lemma nrrsteps_imp_eq_root_arg_rsteps:
assumes steps: "(s,t) ∈ (nrrstep R)⇧*"
shows "root s = root t ∧ (∀i<num_args s. (s |_ [i], t |_ [i] ) ∈ (rstep R)⇧*)"
proof (cases s)
case (Var x)
have "s = t" using steps unfolding Var
proof (induct)
case (step y z)
from nrrstep_imp_Fun[OF step(2)] step(3) have False by auto
then show ?case ..
qed simp
then show ?thesis by auto
next
case (Fun f ss)
from nrrsteps_equiv_num_args[OF steps]
nrrsteps_imp_arg_rsteps[OF steps]
nrrsteps_preserve_root[OF steps[unfolded Fun]]
show ?thesis unfolding Fun by auto
qed
definition
wf_trs :: "('f, 'v) trs ⇒ bool"
where
"wf_trs R = (∀l r. (l,r) ∈ R ⟶ (∃f ts. l = Fun f ts) ∧ vars_term r ⊆ vars_term l)"
lemma wf_trs_imp_lhs_Fun:
"wf_trs R ⟹ (l,r) ∈ R ⟹ ∃f ts. l = Fun f ts"
unfolding wf_trs_def by blast
lemma rstep_imp_Fun:
assumes "wf_trs R"
shows "(s, t) ∈ rstep R ⟹ ∃f ss. s = Fun f ss"
proof -
assume "(s, t) ∈ rstep R"
then obtain C l r σ where lr: "(l,r) ∈ R" and s: "s = C ⟨ l ⋅ σ ⟩" by auto
with wf_trs_imp_lhs_Fun[OF assms lr] show ?thesis by (cases C, auto)
qed
lemma SN_on_imp_SN_on_subt:
assumes "SN_on (rstep R) {t}" shows "∀s⊴t. SN_on (rstep R) {s}"
proof (rule ccontr)
assume "¬(∀s⊴t. SN_on (rstep R) {s})"
then obtain s where "t ⊵ s" and "¬ SN_on (rstep R) {s}" by auto
then obtain S where "S 0 = s" and chain: "chain (rstep R) S" by auto
from ‹t ⊵ s› obtain C where t: "t = C⟨s⟩" by auto
let ?S = "λi. C⟨S i⟩"
from ‹S 0 = s› have "?S 0 = t" by (simp add: t)
moreover from chain have "chain (rstep R) ?S" by blast
ultimately have "¬ SN_on (rstep R) {t}" by best
with assms show False by simp
qed
lemma not_SN_on_subt_imp_not_SN_on:
assumes "¬ SN_on (rstep R) {t}" and "s ⊵ t"
shows "¬ SN_on (rstep R) {s}"
using assms SN_on_imp_SN_on_subt by blast
lemma SN_on_instance_imp_SN_on_var:
assumes "SN_on (rstep R) {t ⋅ σ}" and "x ∈ vars_term t"
shows "SN_on (rstep R) {Var x ⋅ σ}"
proof -
from assms have "t ⊵ Var x" by auto
then have "t⋅σ ⊵ (Var x)⋅σ" by (rule supteq_subst)
with SN_on_imp_SN_on_subt and assms show ?thesis by best
qed
lemma var_imp_var_of_arg:
assumes "x ∈ vars_term (Fun f ss)" (is "x ∈ vars_term ?s")
shows "∃i < num_args (Fun f ss). x ∈ vars_term (ss!i)"
proof -
from assms have "x ∈ ⋃(set (map vars_term ss))" by simp
then have "x ∈ (⋃i<length ss. vars_term(ss!i))" unfolding set_conv_nth by auto
then have "∃i<length ss. x ∈ vars_term(ss!i)" using UN_iff by best
then obtain i where "i < length ss" and "x ∈ vars_term(ss!i)" by auto
then have "i < num_args ?s" by simp
with ‹x ∈ vars_term(ss!i)› show ?thesis by auto
qed
lemma subt_instance_and_not_subst_imp_subt:
"s⋅σ ⊵ t ⟹ ∀x ∈ vars_term s. ¬((Var x)⋅σ ⊵ t) ⟹ ∃u. s ⊵ u ∧ t = u⋅σ"
proof (induct s arbitrary: t rule: term.induct)
case (Var x) then show ?case by auto
next
case (Fun f ss)
from ‹Fun f ss⋅σ ⊵ t› have "(Fun f ss⋅σ = t) ∨ (Fun f ss⋅σ ⊳ t)" by auto
then show ?case
proof
assume "Fun f ss⋅σ = t" with Fun show ?thesis by auto
next
assume "Fun f ss⋅σ ⊳ t"
then have "Fun f (map (λt. t⋅σ) ss) ⊳ t" by simp
then have "∃s ∈ set (map (λt. t⋅σ) ss). s ⊵ t" (is "∃s ∈ set ?ss'. s ⊵ t") by (rule supt_Fun_imp_arg_supteq)
then obtain s' where "s' ∈ set ?ss'" and "s' ⊵ t" by best
then have "∃i < length ?ss'. ?ss'!i = s'" using in_set_conv_nth[where ?x = "s'"] by best
then obtain i where "i < length ?ss'" and "?ss'!i = s'" by best
then have "?ss'!i = (ss!i)⋅σ" by auto
from ‹?ss'!i = s'› have "s' = (ss!i)⋅σ" unfolding ‹?ss'!i = (ss!i)⋅σ› by simp
from ‹s' ⊵ t› have "(ss!i)⋅σ ⊵ t" unfolding ‹s' = (ss!i)⋅σ› by simp
with ‹i < length ?ss'› have "(ss!i) ∈ set ss" by auto
with ‹(ss!i)⋅σ ⊵ t› have "∃s ∈ set ss. s⋅σ ⊵ t" by best
then obtain s where "s ∈ set ss" and "s⋅σ ⊵ t" by best
with Fun have "∀x ∈ vars_term s. ¬((Var x)⋅σ ⊵ t)" by force
from Fun
have IH: "s ∈ set ss ⟶ (∀v. s⋅σ ⊵ v ⟶ (∀x ∈ vars_term s. ¬ Var x⋅σ ⊵ v) ⟶ (∃u. s ⊵ u ∧ v = u⋅σ))"
by auto
with ‹s ∈ set ss› have "!!v. s⋅σ ⊵ v ⟹ (∀x ∈ vars_term s. ¬ Var x⋅σ ⊵ v) ⟶ (∃u. s ⊵ u ∧ v = u⋅σ)"
by simp
with ‹s⋅σ ⊵ t› have "(∀x ∈ vars_term s. ¬ Var x⋅σ ⊵ t) ⟶ (∃u. s ⊵ u ∧ t = u⋅σ)" by simp
with ‹∀x ∈ vars_term s. ¬ Var x⋅σ ⊵ t› obtain u where "s ⊵ u" and "t = u⋅σ" by best
with ‹s ∈ set ss› have "Fun f ss ⊵ u" by auto
with ‹t = u⋅σ› show ?thesis by best
qed
qed
lemma SN_imp_SN_subt:
"SN_on (rstep R) {s} ⟹ s ⊵ t ⟹ SN_on (rstep R) {t}"
by (rule ctxt_closed_SN_on_subt[OF ctxt_closed_rstep])
lemma subterm_preserves_SN_gen:
assumes ctxt: "ctxt.closed R"
and SN: "SN_on R {t}" and supt: "t ⊳ s"
shows "SN_on R {s}"
proof -
from supt have "t ⊵ s" by auto
then show ?thesis using ctxt_closed_SN_on_subt[OF ctxt SN, of s] by simp
qed
context E_compatible
begin
lemma SN_on_step_E_imp_SN_on: assumes "SN_on R {s}"
and "(s,t) ∈ E"
shows "SN_on R {t}"
using assms E(1) unfolding SN_on_all_reducts_SN_on_conv[of _ t] SN_on_all_reducts_SN_on_conv[of _ s]
by blast
lemma SN_on_step_REs_imp_SN_on:
assumes R: "ctxt.closed R"
and st: "(s,t) ∈ (R ∪ E O {⊳} O E)"
and SN: "SN_on R {s}"
shows "SN_on R {t}"
proof (cases "(s,t) ∈ R")
case True
from step_preserves_SN_on[OF this SN] show ?thesis .
next
case False
with st obtain u v where su: "(s,u) ∈ E" and uv: "u ⊳ v" and vt: "(v,t) ∈ E" by auto
have u: "SN_on R {u}" by (rule SN_on_step_E_imp_SN_on[OF SN su])
with uv R have "SN_on R {v}" by (metis subterm_preserves_SN_gen)
then show ?thesis by (rule SN_on_step_E_imp_SN_on[OF _ vt])
qed
lemma restrict_SN_supt_E_I:
"ctxt.closed R ⟹ SN_on R {s} ⟹ (s,t) ∈ R ∪ E O {⊳} O E ⟹ (s,t) ∈ restrict_SN_supt_E"
unfolding restrict_SN_supt_E_def restrict_SN_def
using SN_on_step_REs_imp_SN_on[of s t] E(2) by auto
lemma ctxt_closed_imp_SN_on_E_supt:
assumes R: "ctxt.closed R"
and SN: "SN (E O {⊳} O E)"
shows "SN_on (R ∪ E O {⊳} O E) {t. SN_on R {t}}"
proof -
{
fix f
assume f0: "SN_on R {f 0}" and f: "⋀ i. (f i, f (Suc i)) ∈ R ∪ E O {⊳} O E"
from ctxt_closed_imp_SN_restrict_SN_E_supt[OF assms]
have SN: "SN restrict_SN_supt_E" .
{
fix i
have "SN_on R {f i}"
by (induct i, rule f0, rule SN_on_step_REs_imp_SN_on[OF R f])
} note fi = this
{
fix i
from f[of i] fi[of i]
have "(f i, f (Suc i)) ∈ restrict_SN_supt_E" by (metis restrict_SN_supt_E_I[OF R])
}
with SN have False by auto
}
then show ?thesis unfolding SN_on_def by blast
qed
end
lemma subterm_preserves_SN:
"SN_on (rstep R) {t} ⟹ t ⊳ s ⟹ SN_on (rstep R) {s}"
by (rule subterm_preserves_SN_gen[OF ctxt_closed_rstep])
lemma SN_on_r_imp_SN_on_supt_union_r:
assumes ctxt: "ctxt.closed R"
and "SN_on R T"
shows "SN_on (supt ∪ R) T" (is "SN_on ?S T")
proof (rule ccontr)
assume "¬ SN_on ?S T"
then obtain s where ini: "s 0 : T" and chain: "chain ?S s"
unfolding SN_on_def by auto
have SN: "∀i. SN_on R {s i}"
proof
fix i show "SN_on R {s i}"
proof (induct i)
case 0 show ?case using assms using ‹s 0 ∈ T› and SN_on_subset2[of "{s 0}" T R] by simp
next
case (Suc i)
from chain have "(s i, s (Suc i)) ∈ ?S" by simp
then show ?case
proof
assume "(s i, s (Suc i)) ∈ supt"
from subterm_preserves_SN_gen[OF ctxt Suc this] show ?thesis .
next
assume "(s i, s (Suc i)) ∈ R"
from step_preserves_SN_on[OF this Suc] show ?thesis .
qed
qed
qed
have "¬ (∃S. ∀i. (S i, S (Suc i)) ∈ restrict_SN_supt R)"
using ctxt_closed_imp_SN_restrict_SN_supt[OF ctxt] unfolding SN_defs by auto
moreover have "∀i. (s i, s (Suc i)) ∈ restrict_SN_supt R"
proof
fix i
from SN have SN: "SN_on R {s i}" by simp
from chain have "(s i, s (Suc i)) ∈ supt ∪ R" by simp
then show "(s i, s (Suc i)) ∈ restrict_SN_supt R"
unfolding restrict_SN_supt_def restrict_SN_def using SN by auto
qed
ultimately show False by auto
qed
lemma SN_on_rstep_imp_SN_on_supt_union_rstep:
"SN_on (rstep R) T ⟹ SN_on (supt ∪ rstep R) T"
by (rule SN_on_r_imp_SN_on_supt_union_r[OF ctxt_closed_rstep])
lemma SN_supt_r_trancl:
assumes ctxt: "ctxt.closed R"
and a: "SN R"
shows "SN ((supt ∪ R)⇧+)"
proof -
have "SN (supt ∪ R)"
using SN_on_r_imp_SN_on_supt_union_r[OF ctxt, of UNIV]
and a by force
then show "SN ((supt ∪ R)⇧+)" by (rule SN_imp_SN_trancl)
qed
lemma SN_supt_rstep_trancl:
"SN (rstep R) ⟹ SN ((supt ∪ rstep R)⇧+)"
by (rule SN_supt_r_trancl[OF ctxt_closed_rstep])
lemma SN_imp_SN_arg_gen:
assumes ctxt: "ctxt.closed R"
and SN: "SN_on R {Fun f ts}" and arg: "t ∈ set ts" shows "SN_on R {t}"
proof -
from arg have "Fun f ts ⊵ t" by auto
with SN show ?thesis by (rule ctxt_closed_SN_on_subt[OF ctxt])
qed
lemma SN_imp_SN_arg:
"SN_on (rstep R) {Fun f ts} ⟹ t ∈ set ts ⟹ SN_on (rstep R) {t}"
by (rule SN_imp_SN_arg_gen[OF ctxt_closed_rstep])
lemma SNinstance_imp_SN:
assumes "SN_on (rstep R) {t ⋅ σ}"
shows "SN_on (rstep R) {t}"
proof(rule ccontr)
assume "¬ SN_on (rstep R) {t}"
then have "¬ SN_on (rstep R) {t ⋅ σ}"
proof (simp add: SN_on_def)
assume "∃f. f 0 = t ∧ (∀ i. (f i, f (Suc i)) ∈ rstep R)"
from this obtain f where prem: "f 0 = t ∧ (∀ i. (f i, f (Suc i)) ∈ rstep R)" by auto
let ?g = "λ i. (f i) ⋅ σ"
from prem have "?g 0 = t ⋅ σ ∧ (∀ i. (?g i, ?g (Suc i)) ∈ rstep R)" using subst_closed_rstep
by auto
then show "∃ f. f 0 = t ⋅ σ ∧ (∀ i. (f i, f (Suc i)) ∈ rstep R)" by auto
qed
with assms show "False" by simp
qed
lemma rstep_imp_C_s_r:
assumes "(s,t) ∈ rstep R"
shows "∃C σ l r. (l,r) ∈ R ∧ s = C⟨l⋅σ⟩ ∧ t = C⟨r⋅σ⟩"
proof -
from assms obtain l r p σ where step:"(s,t) ∈ rstep_r_p_s R (l,r) p σ"
unfolding rstep_iff_rstep_r_p_s by best
let ?C = "ctxt_of_pos_term p s"
from step have "p ∈ poss s" and "(l,r) ∈ R" and "?C⟨l⋅σ⟩ = s" and "?C⟨r⋅σ⟩ = t"
unfolding rstep_r_p_s_def Let_def by auto
then have "(l,r) ∈ R ∧ s = ?C⟨l⋅σ⟩ ∧ t = ?C⟨r⋅σ⟩" by auto
then show ?thesis by force
qed
lemma SN_Var:
assumes "wf_trs R" shows "SN_on (rstep R) {Var x}"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain S where [symmetric]: "S 0 = Var x"
and chain: "chain (rstep R) S" by auto
then have "(Var x, S (Suc 0)) ∈ rstep R" by force
then obtain C l r σ where "(l, r) ∈ R" and "Var x = C⟨l ⋅ σ⟩" by best
then have "Var x = l ⋅ σ" by (induct C) simp_all
then obtain y where "l = Var y" by (induct l) simp_all
with assms and ‹(l, r) ∈ R› show False unfolding wf_trs_def by blast
qed
fun map_funs_rule :: "('f ⇒ 'g) ⇒ ('f, 'v) rule ⇒ ('g, 'v) rule"
where
"map_funs_rule fg lr = (map_funs_term fg (fst lr), map_funs_term fg (snd lr))"
fun map_funs_trs :: "('f ⇒ 'g) ⇒ ('f, 'v) trs ⇒ ('g, 'v) trs"
where
"map_funs_trs fg R = map_funs_rule fg ` R"
lemma map_funs_trs_union: "map_funs_trs fg (R ∪ S) = map_funs_trs fg R ∪ map_funs_trs fg S"
unfolding map_funs_trs.simps by auto
lemma rstep_map_funs_term: assumes R: "⋀ f. f ∈ funs_trs R ⟹ h f = f" and step: "(s,t) ∈ rstep R"
shows "(map_funs_term h s, map_funs_term h t) ∈ rstep R"
proof -
from step obtain C l r σ where s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩" and rule: "(l,r) ∈ R" by auto
let ?σ = "map_funs_subst h σ"
let ?h = "map_funs_term h"
note funs_defs = funs_rule_def[abs_def] funs_trs_def
from rule have lr: "funs_term l ∪ funs_term r ⊆ funs_trs 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 ?thesis unfolding s t
unfolding map_funs_subst_distrib map_funs_term_ctxt_distrib hl hr
by (rule rstepI[OF rule refl refl])
qed
lemma wf_trs_map_funs_trs[simp]: "wf_trs (map_funs_trs f R) = wf_trs R"
unfolding wf_trs_def
proof (rule iffI, intro allI impI)
fix l r
assume "∀l r. (l, r) ∈ map_funs_trs f R ⟶ (∃f ts. l = Fun f ts) ∧ vars_term r ⊆ vars_term l" and "(l, r) ∈ R"
then show "(∃f ts. l = Fun f ts) ∧ vars_term r ⊆ vars_term l" by (cases l, force+)
next
assume ass: " ∀l r. (l, r) ∈ R ⟶ (∃f ts. l = Fun f ts) ∧ vars_term r ⊆ vars_term l"
show "∀l r. (l, r) ∈ map_funs_trs f R ⟶ (∃f ts. l = Fun f ts) ∧ vars_term r ⊆ vars_term l"
proof (intro allI impI)
fix l r
assume "(l, r) ∈ map_funs_trs f R"
with ass
show "(∃f ts. l = Fun f ts) ∧ vars_term r ⊆ vars_term l"
by (cases l, force+)
qed
qed
lemma map_funs_trs_comp: "map_funs_trs fg (map_funs_trs gh R) = map_funs_trs (fg o gh) R"
proof -
have mr: "map_funs_rule (fg o gh) = map_funs_rule fg o map_funs_rule gh"
by (rule ext, auto simp: map_funs_term_comp)
then show ?thesis
by (auto simp: map_funs_term_comp image_comp mr)
qed
lemma map_funs_trs_mono: assumes "R ⊆ R'" shows "map_funs_trs fg R ⊆ map_funs_trs fg R'"
using assms by auto
lemma map_funs_trs_power_mono:
fixes R R' :: "('f,'v)trs" and fg :: "'f ⇒ 'f"
assumes "R ⊆ R'" shows "((map_funs_trs fg)^^n) R ⊆ ((map_funs_trs fg)^^n) R'"
using assms by (induct n, simp, auto)
declare map_funs_trs.simps[simp del]
lemma rstep_imp_map_rstep:
assumes "(s, t) ∈ rstep R"
shows "(map_funs_term fg s, map_funs_term fg t) ∈ rstep (map_funs_trs fg R)"
using assms
proof (induct)
case (IH C σ l r)
then have "(map_funs_term fg l, map_funs_term fg r) ∈ map_funs_trs fg R" (is "(?l, ?r) ∈ ?R")
unfolding map_funs_trs.simps by force
then have "(?l, ?r) ∈ rstep ?R" ..
then have "(?l ⋅ map_funs_subst fg σ, ?r ⋅ map_funs_subst fg σ) ∈ rstep ?R" ..
then show ?case by auto
qed
lemma rsteps_imp_map_rsteps: assumes "(s,t) ∈ (rstep R)⇧*"
shows "(map_funs_term fg s, map_funs_term fg t) ∈ (rstep (map_funs_trs fg R))⇧*"
using assms
proof (induct, clarify)
case (step y z)
then have "(map_funs_term fg y, map_funs_term fg z) ∈ rstep (map_funs_trs fg R)" using rstep_imp_map_rstep
by (auto simp: map_funs_trs.simps)
with step show ?case by auto
qed
lemma SN_map_imp_SN:
assumes SN: "SN_on (rstep (map_funs_trs fg R)) {map_funs_term fg t}"
shows "SN_on (rstep R) {t}"
proof (rule ccontr)
assume "¬ SN_on (rstep R) {t}"
from this obtain f where cond: "f 0 = t ∧ (∀ i. (f i, f (Suc i)) ∈ rstep R)"
unfolding SN_on_def by auto
obtain g where g: "g = (λ i. map_funs_term fg (f i))" by auto
with cond have cond2: "g 0 = map_funs_term fg t ∧ (∀ i. (g i, g (Suc i)) ∈ rstep (map_funs_trs fg R))"
using rstep_imp_map_rstep[where fg = fg] by blast
from SN
have "¬ (∃ g. (g 0 = map_funs_term fg t ∧ (∀ i. (g i, g (Suc i)) ∈ rstep (map_funs_trs fg R))))"
unfolding SN_on_def by auto
with cond2 show False by auto
qed
lemma rstep_iff_map_rstep:
assumes "inj fg"
shows "(s, t) ∈ rstep R ⟷ (map_funs_term fg s, map_funs_term fg t) ∈ rstep (map_funs_trs fg R)"
proof
assume "(s,t) ∈ rstep R"
then show "(map_funs_term fg s, map_funs_term fg t) ∈ rstep(map_funs_trs fg R)"
by (rule rstep_imp_map_rstep)
next
assume "(map_funs_term fg s, map_funs_term fg t) ∈ rstep (map_funs_trs fg R)"
then have "(map_funs_term fg s, map_funs_term fg t) ∈ ctxt.closure(subst.closure(map_funs_trs fg R))"
by (simp add: rstep_eq_closure)
then obtain C u v where "(u,v) ∈ subst.closure(map_funs_trs fg R)" and "C⟨u⟩ = map_funs_term fg s"
and "C⟨v⟩ = map_funs_term fg t"
by (cases rule: ctxt.closure.cases) force
then obtain σ w x where "(w,x) ∈ map_funs_trs fg R" and "w⋅σ = u" and "x⋅σ = v"
by (cases rule: subst.closure.cases) force
then obtain l r where "w = map_funs_term fg l" and "x = map_funs_term fg r"
and "(l,r) ∈ R" by (auto simp: map_funs_trs.simps)
have ps: "C⟨map_funs_term fg l ⋅ σ⟩ = map_funs_term fg s" and pt: "C⟨map_funs_term fg r ⋅ σ⟩ = map_funs_term fg t"
unfolding ‹w = map_funs_term fg l›[symmetric] ‹x = map_funs_term fg r›[symmetric] ‹w⋅σ = u› ‹x⋅σ = v›
‹C⟨u⟩ = map_funs_term fg s› ‹C⟨v⟩ = map_funs_term fg t› by auto
let ?gf = "the_inv fg"
let ?C = "map_funs_ctxt ?gf C"
let ?σ = "map_funs_subst ?gf σ"
have gffg: "?gf ∘ fg = id" using the_inv_f_f[OF assms] by (intro ext, auto)
from ps and pt have "s = map_funs_term ?gf (C⟨map_funs_term fg l ⋅ σ⟩)"
and "t = map_funs_term ?gf (C⟨map_funs_term fg r ⋅ σ⟩)" by (auto simp: map_funs_term_comp gffg)
then have s: "s = ?C⟨map_funs_term ?gf (map_funs_term fg l ⋅ σ)⟩"
and t: "t = ?C⟨map_funs_term ?gf (map_funs_term fg r ⋅ σ)⟩" using map_funs_term_ctxt_distrib by auto
from s have "s = ?C⟨l⋅?σ⟩" by (simp add: map_funs_term_comp gffg)
from t have "t = ?C⟨r⋅?σ⟩" by (simp add: map_funs_term_comp gffg)
from ‹(l, r) ∈ R› have "(l⋅?σ, r⋅?σ) ∈ subst.closure R" by blast
then have "(?C⟨l⋅?σ⟩,?C⟨r⋅?σ⟩) ∈ ctxt.closure(subst.closure R)" by blast
then show "(s,t) ∈ rstep R" unfolding ‹s = ?C⟨l⋅?σ⟩› ‹t = ?C⟨r⋅?σ⟩› by (simp add: rstep_eq_closure)
qed
lemma rstep_map_funs_trs_power_mono:
fixes R R' :: "('f,'v)trs" and fg :: "'f ⇒ 'f"
assumes subset: "R ⊆ R'" shows "rstep (((map_funs_trs fg)^^n) R) ⊆ rstep (((map_funs_trs fg)^^n) R')"
by (rule rstep_mono, rule map_funs_trs_power_mono, rule subset)
lemma subsetI3: "(⋀x y z. (x, y, z) ∈ A ⟹ (x, y, z) ∈ B) ⟹ A ⊆ B" by auto
lemma aux: "(⋃a∈P. {(x,y,z). x = fst a ∧ y = snd a ∧ Q a z}) = {(x,y,z). (x,y) ∈ P ∧ Q (x,y) z}" (is "?P = ?Q")
proof
show "?P ⊆ ?Q"
proof
fix x assume "x ∈ ?P"
then obtain a where "a ∈ P" and "x ∈ {(x,y,z). x = fst a ∧ y = snd a ∧ Q a z}" by auto
then obtain b where "Q (fst x, fst (snd x)) (snd (snd x))" and "(fst x, fst (snd x)) = a" and "snd (snd x) = b" by force
from ‹a ∈ P› have "(fst a,snd a) ∈ P" unfolding split_def by simp
from ‹Q (fst x, fst (snd x)) (snd (snd x))› have "Q a b" unfolding ‹(fst x, fst (snd x)) = a› ‹snd (snd x) = b› .
from ‹(fst a,snd a) ∈ P› and ‹Q a b› show "x ∈ ?Q" unfolding split_def ‹(fst x, fst (snd x)) = a›[symmetric] ‹snd (snd x) = b›[symmetric] by simp
qed
next
show "?Q ⊆ ?P"
proof (rule subsetI3)
fix x y z assume "(x,y,z) ∈ ?Q"
then have "(x,y) ∈ P" and "Q (x,y) z" by auto
then have "x = fst(x,y) ∧ y = snd(x,y) ∧ Q (x,y) z" by auto
then have "(x,y,z) ∈ {(x,y,z). x = fst(x,y) ∧ y = snd(x,y) ∧ Q (x,y) z}" by auto
then have "∃p∈P. (x,y,z) ∈ {(x,y,z). x = fst p ∧ y = snd p ∧ Q p z}" using ‹(x,y) ∈ P› by blast
then show "(x,y,z) ∈ ?P" unfolding UN_iff[symmetric] by simp
qed
qed
lemma finite_imp_finite_DP_on':
assumes "finite R"
shows "finite {(l, r, u).
∃h us. u = Fun h us ∧ (l, r) ∈ R ∧ r ⊵ u ∧ (h, length us) ∈ F ∧ ¬ (l ⊳ u)}"
proof -
have "⋀l r. (l, r) ∈ R ⟹ finite {u. r ⊵ u}"
proof -
fix l r
assume "(l, r) ∈ R"
show "finite {u. r ⊵ u}" by (rule finite_subterms)
qed
with ‹finite R› have "finite(⋃(l, r) ∈ R. {u. r ⊵ u})" by auto
have "finite(⋃lr∈R. {(l, r, u). l = fst lr ∧ r = snd lr ∧ snd lr ⊵ u})"
proof (rule finite_UN_I)
show "finite R" by (rule ‹finite R›)
next
fix lr
assume "lr ∈ R"
have "finite {u. snd lr ⊵ u}" by (rule finite_subterms)
then show "finite {(l,r,u). l = fst lr ∧ r = snd lr ∧ snd lr ⊵ u}" by auto
qed
then have "finite {(l,r,u). (l,r) ∈ R ∧ r ⊵ u}" unfolding aux by auto
have "{(l,r,u). (l,r) ∈ R ∧ r ⊵ u} ⊇ {(l,r,u). (∃h us. u = Fun h us ∧ (l,r) ∈ R ∧ r ⊵ u ∧ (h, length us) ∈ F ∧ ¬(l ⊳ u))}" by auto
with ‹finite {(l,r,u). (l,r) ∈ R ∧ r ⊵ u}› show ?thesis using finite_subset by fast
qed
lemma card_image_le':
assumes "finite S"
shows "card (⋃y∈S.{x. x = f y}) ≤ card S"
proof -
have A:"(⋃y∈S. {x. x = f y}) = f ` S" by auto
from assms show ?thesis unfolding A using card_image_le by auto
qed
lemma subteq_of_map_imp_map: "map_funs_term g s ⊵ t ⟹ ∃u. t = map_funs_term g u"
proof (induct s arbitrary: t)
case (Var x)
then have "map_funs_term g (Var x) ⊳ t ∨ map_funs_term g (Var x) = t" by auto
then show ?case
proof
assume "map_funs_term g (Var x) ⊳ t" then show ?thesis by (cases rule: supt.cases) auto
next
assume "map_funs_term g (Var x) = t" then show ?thesis by best
qed
next
case (Fun f ss)
then have "map_funs_term g (Fun f ss) ⊳ t ∨ map_funs_term g (Fun f ss) = t" by auto
then show ?case
proof
assume "map_funs_term g (Fun f ss) ⊳ t"
then show ?case using Fun by (cases rule: supt.cases) (auto simp: supt_supteq_conv)
next
assume "map_funs_term g (Fun f ss) = t" then show ?thesis by best
qed
qed
lemma map_funs_term_inj:
assumes "inj (fg :: ('f ⇒ 'g))"
shows "inj (map_funs_term fg)"
proof -
{
fix s t :: "('f,'v)term"
assume "map_funs_term fg s = map_funs_term fg t"
then have "s = t"
proof (induct s arbitrary: t)
case (Var x) with assms show ?case by (induct t) auto
next
case (Fun f ss) then show ?case
proof (induct t)
case (Var y) then show ?case by auto
next
case (Fun g ts)
then have A: "map (map_funs_term fg) ss = map (map_funs_term fg) ts" by simp
then have len_eq:"length ss = length ts" by (rule map_eq_imp_length_eq)
from A have "!!i. i < length ss ⟹ (map (map_funs_term fg) ss)!i = (map (map_funs_term fg) ts)!i" by auto
with len_eq have eq: "!!i. i < length ss ⟹ map_funs_term fg (ss!i) = map_funs_term fg (ts!i)" using nth_map by auto
have in_set: "!!i. i < length ss ⟹ (ss!i) ∈ set ss" by auto
from Fun have "∀i < length ss. (ss!i) = (ts!i)" using in_set eq by auto
with len_eq have "ss = ts" using nth_equalityI[where xs = ss and ys = ts] by simp
have "f = g" using Fun ‹inj fg› unfolding inj_on_def by auto
with ‹ss = ts› show ?case by simp
qed
qed
}
then show ?thesis unfolding inj_on_def by auto
qed
lemma rsteps_closed_ctxt:
assumes "(s, t) ∈ (rstep R)⇧*"
shows "(C⟨s⟩, C⟨t⟩) ∈ (rstep R)⇧*"
proof -
from assms obtain n where "(s,t) ∈ (rstep R)^^n"
using rtrancl_is_UN_relpow by auto
then show ?thesis
proof (induct n arbitrary: s)
case 0 then show ?case by auto
next
case (Suc n)
from relpow_Suc_D2[OF ‹(s,t) ∈ (rstep R)^^Suc n›] obtain u
where "(s,u) ∈ (rstep R)" and "(u,t) ∈ (rstep R)^^n" by auto
from ‹(s,u) ∈ (rstep R)› have "(C⟨s⟩,C⟨u⟩) ∈ (rstep R)" ..
from Suc and ‹(u,t) ∈ (rstep R)^^n› have "(C⟨u⟩,C⟨t⟩) ∈ (rstep R)⇧*" by simp
with ‹(C⟨s⟩,C⟨u⟩) ∈ (rstep R)› show ?case by auto
qed
qed
lemma not_Nil_imp_last: "xs ≠ [] ⟹ ∃ys y. xs = ys@[y]"
proof (induct xs)
case Nil then show ?case by simp
next
case (Cons x xs) show ?case
proof (cases xs)
assume "xs = []" with Cons show ?thesis by simp
next
fix x' xs' assume "xs = x'#xs'"
then have "xs ≠ []" by simp
with Cons obtain ys y where "xs = ys@[y]" by auto
then have "x#xs = x#(ys@[y])" by simp
then have "x#xs = (x#ys)@[y]" by simp
then show ?thesis by auto
qed
qed
lemma Nil_or_last: "xs = [] ∨ (∃ys y. xs = ys@[y])"
proof (cases xs)
assume "xs = []" then show ?thesis by simp
next
fix x' xs' assume "xs = x'#xs'"
then have "xs ≠ []" by simp
then show ?thesis using not_Nil_imp_last by auto
qed
lemma one_imp_ctxt_closed: assumes one: "⋀ f bef s t aft. (s,t) ∈ r ⟹ (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ r"
shows "ctxt.closed r"
proof
fix s t C
assume st: "(s,t) ∈ r"
show "(C⟨s⟩, C⟨t⟩) ∈ r"
proof (induct C)
case (More f bef C aft)
from one[OF More] show ?case by auto
qed (insert st, auto)
qed
lemma ctxt_closed_nrrstep [intro]: "ctxt.closed (nrrstep R)"
proof (rule one_imp_ctxt_closed)
fix f bef s t aft
assume "(s,t) ∈ nrrstep R"
from this[unfolded nrrstep_def'] obtain l r C σ
where lr: "(l,r) ∈ R" and C: "C ≠ □"
and s: "s = C⟨l⋅σ⟩" and t: "t = C⟨r ⋅ σ⟩" by auto
show "(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ nrrstep R"
proof (rule nrrstepI[OF lr])
show "More f bef C aft ≠ □" by simp
qed (insert s t, auto)
qed
definition all_ctxt_closed :: "'f sig ⇒ ('f, 'v) trs ⇒ bool" where
"all_ctxt_closed F r ⟷ (∀f ts ss. (f, length ss) ∈ F ⟶ length ts = length ss ⟶
(∀i. i < length ts ⟶ (ts ! i, ss ! i) ∈ r) ⟶ (∀ i. i < length ts ⟶ funas_term (ts ! i) ∪ funas_term (ss ! i) ⊆ F) ⟶ (Fun f ts, Fun f ss) ∈ r) ∧ (∀ x. (Var x, Var x) ∈ r)"
lemma all_ctxt_closedD: "all_ctxt_closed F r ⟹ (f,length ss) ∈ F ⟹ length ts = length ss
⟹ ⟦⋀ i. i < length ts ⟹ (ts ! i, ss ! i) ∈ r ⟧
⟹ ⟦⋀ i. i < length ts ⟹ funas_term (ts ! i) ⊆ F ⟧
⟹ ⟦⋀ i. i < length ts ⟹ funas_term (ss ! i) ⊆ F ⟧
⟹ (Fun f ts, Fun f ss) ∈ r"
unfolding all_ctxt_closed_def by auto
lemma all_ctxt_closed_sig_reflE: assumes all: "all_ctxt_closed F r"
shows "funas_term t ⊆ F ⟹ (t,t) ∈ r"
proof (induct t)
case (Var x)
from all[unfolded all_ctxt_closed_def] show ?case by auto
next
case (Fun f ts)
show ?case
by (rule all_ctxt_closedD[OF all _ _ Fun(1)], insert Fun(2), force+)
qed
lemma all_ctxt_closed_reflE: assumes all: "all_ctxt_closed UNIV r"
shows "(t,t) ∈ r"
by (rule all_ctxt_closed_sig_reflE[OF all], auto)
lemma all_ctxt_closed_relpow:
assumes acc:"all_ctxt_closed UNIV Q"
shows "all_ctxt_closed UNIV (Q ^^ n)"
proof-
{ fix f ss ts
assume a: "length ts = length ss" "∀i<length ts. (ts ! i, ss ! i) ∈ Q ^^ n"
then have "(Fun f ts, Fun f ss) ∈ Q ^^ n" proof(induct n arbitrary: ss ts)
case 0
with relpow_0_I list_eq_iff_nth_eq relpow_0_E show ?case by metis
next
case (Suc j)
{ fix i
assume "i < length ts"
from relpow_Suc_D2[OF Suc(3)[rule_format, OF this]] have "∃ u. (ts ! i, u) ∈ Q ∧ (u, ss ! i) ∈ Q ^^ j" by auto
}
with Suc(3) have "∀ i. ∃ u. i < length ts ⟶ (ts ! i, u) ∈ Q ∧ (u, ss ! i) ∈ Q ^^ j" by blast
from choice[OF this] obtain ui where x:"∀i < (length ts). (ts ! i, ui i) ∈ Q ∧ (ui i, ss ! i) ∈ Q ^^ j" by blast
let ?us = "map ui [0..<length ts]"
from x have 1:"∀i < (length ts). (ts ! i, ?us ! i) ∈ Q ∧ (?us ! i, ss ! i) ∈ Q ^^ j" by auto
from Suc(2) have 2:"length ?us = length ss" by simp
with Suc(2) have 3:"length ts = length ?us" by auto
from Suc(1)[OF 2] 1 have y:"(Fun f ?us, Fun f ss) ∈ Q ^^ j" by fastforce
from conjunct1[OF acc[unfolded all_ctxt_closed_def], rule_format, OF _ 3] x have "(Fun f ts, Fun f ?us) ∈ Q" by fastforce
from relpow_Suc_I2[OF this y] show ?case by blast
qed
} note 1 = this
from assms[unfolded all_ctxt_closed_def] have "∀x. (Var x, Var x) ∈ Q ^^ n" by (induct n, auto)
with 1 show ?thesis unfolding all_ctxt_closed_def by simp
qed
lemma all_ctxt_closed_subst_step_sig:
fixes r :: "('f, 'v) trs" and t :: "('f, 'v) term"
assumes all: "all_ctxt_closed F r"
and sig: "funas_term t ⊆ F"
and steps: "⋀ x. x ∈ vars_term t ⟹ (σ x, τ x) ∈ r"
and sig_subst: "⋀ x. x ∈ vars_term t ⟹ funas_term (σ x) ∪ funas_term (τ x) ⊆ F"
shows "(t ⋅ σ, t ⋅ τ) ∈ r"
using sig steps sig_subst
proof (induct t)
case (Var x)
then show ?case by auto
next
case (Fun f ts)
{
fix t
assume t: "t ∈ set ts"
with Fun(2-3) have "funas_term t ⊆ F" "⋀ x. x ∈ vars_term t ⟹ (σ x, τ x) ∈ r" by auto
from Fun(1)[OF t this Fun(4)] t have step: "(t ⋅ σ, t ⋅ τ) ∈ r" by auto
from Fun(4) t have "⋀ x. x ∈ vars_term t ⟹ funas_term (σ x) ∪ funas_term (τ x) ⊆ F" by auto
with ‹funas_term t ⊆ F› have "funas_term (t ⋅ σ) ∪ funas_term (t ⋅ τ) ⊆ F" unfolding funas_term_subst by auto
note step this
}
then have steps: "⋀ i. i < length ts ⟹ (ts ! i ⋅ σ, ts ! i ⋅ τ) ∈ r ∧ funas_term (ts ! i ⋅ σ) ∪ funas_term (ts ! i ⋅ τ) ⊆ F" unfolding set_conv_nth by auto
with all_ctxt_closedD[OF all, of f "map (λ t. t ⋅ τ) ts" "map (λ t. t ⋅ σ) ts"] Fun(2)
show ?case by auto
qed
lemma all_ctxt_closed_subst_step:
fixes r :: "('f, 'v) trs" and t :: "('f, 'v) term"
assumes all: "all_ctxt_closed UNIV r"
and steps: "⋀ x. x ∈ vars_term t ⟹ (σ x, τ x) ∈ r"
shows "(t ⋅ σ, t ⋅ τ) ∈ r"
by (rule all_ctxt_closed_subst_step_sig[OF all _ steps], auto)
lemma all_ctxt_closed_ctxtE: assumes all: "all_ctxt_closed F R"
and Fs: "funas_term s ⊆ F"
and Ft: "funas_term t ⊆ F"
and step: "(s,t) ∈ R"
shows "funas_ctxt C ⊆ F ⟹ (C ⟨ s ⟩, C ⟨ t ⟩) ∈ R"
proof(induct C)
case Hole
from step show ?case by auto
next
case (More f bef C aft)
let ?n = "length bef"
let ?m = "Suc (?n + length aft)"
show ?case unfolding ctxt_apply_term.simps
proof (rule all_ctxt_closedD[OF all])
fix i
let ?t = "λ s. (bef @ C ⟨ s ⟩ # aft) ! i"
assume "i < length (bef @ C⟨s⟩ # aft)"
then have i: "i < ?m" by auto
then have mem: "⋀ s. ?t s ∈ set (bef @ C ⟨ s ⟩ # aft)" unfolding set_conv_nth by auto
from mem[of s] More Fs show "funas_term (?t s) ⊆ F" by auto
from mem[of t] More Ft show "funas_term (?t t) ⊆ F" by auto
from More have step: "(C ⟨ s ⟩, C ⟨ t ⟩) ∈ R" by auto
{
fix s
assume "s ∈ set bef ∪ set aft"
with More have "funas_term s ⊆ F" by auto
from all_ctxt_closed_sig_reflE[OF all this] have "(s,s) ∈ R" by auto
} note steps = this
show "(?t s, ?t t) ∈ R"
proof (cases "i = ?n")
case True
then show ?thesis using step by auto
next
case False
show ?thesis
proof (cases "i < ?n")
case True
then show ?thesis unfolding append_Cons_nth_left[OF True] using steps by auto
next
case False
with ‹i ≠ ?n› i have "∃ k. k < length aft ∧ i = Suc ?n + k" by presburger
then obtain k where k: "k < length aft" and i: "i = Suc ?n + k" by auto
from k show ?thesis using steps unfolding i by (auto simp: nth_append)
qed
qed
qed (insert More, auto)
qed
lemma trans_ctxt_sig_imp_all_ctxt_closed: assumes tran: "trans r"
and refl: "⋀ t. funas_term t ⊆ F ⟹ (t,t) ∈ r"
and ctxt: "⋀ C s t. funas_ctxt C ⊆ F ⟹ funas_term s ⊆ F ⟹ funas_term t ⊆ F ⟹ (s,t) ∈ r ⟹ (C ⟨ s ⟩, C ⟨ t ⟩) ∈ r"
shows "all_ctxt_closed F r"
unfolding all_ctxt_closed_def
proof (rule, intro allI impI)
fix f ts ss
assume f: "(f,length ss) ∈ F" and
l: "length ts = length ss" and
steps: "∀ i < length ts. (ts ! i, ss ! i) ∈ r" and
sig: "∀ i < length ts. funas_term (ts ! i) ∪ funas_term (ss ! i) ⊆ F"
from sig have sig_ts: "⋀ t. t ∈ set ts ⟹ funas_term t ⊆ F" unfolding set_conv_nth by auto
let ?p = "λ ss. (Fun f ts, Fun f ss) ∈ r ∧ funas_term (Fun f ss) ⊆ F"
let ?r = "λ xsi ysi. (xsi, ysi) ∈ r ∧ funas_term ysi ⊆ F"
have init: "?p ts" by (rule conjI[OF refl], insert f sig_ts l, auto)
have "?p ss"
proof (rule parallel_list_update[where p = ?p and r = ?r, OF _ HOL.refl init l[symmetric]])
fix xs i y
assume len: "length xs = length ts"
and i: "i < length ts"
and r: "?r (xs ! i) y"
and p: "?p xs"
let ?C = "More f (take i xs) Hole (drop (Suc i) xs)"
have id1: "Fun f xs = ?C ⟨ xs ! i⟩" using id_take_nth_drop[OF i[folded len]] by simp
have id2: "Fun f (xs[i := y]) = ?C ⟨ y ⟩" using upd_conv_take_nth_drop[OF i[folded len]] by simp
from p[unfolded id1] have C: "funas_ctxt ?C ⊆ F" and xi: "funas_term (xs ! i) ⊆ F" by auto
from r have "funas_term y ⊆ F" "(xs ! i, y) ∈ r" by auto
with ctxt[OF C xi this] C have r: "(Fun f xs, Fun f (xs[i := y])) ∈ r"
and f: "funas_term (Fun f (xs[i := y])) ⊆ F" unfolding id1 id2 by auto
from p r tran have "(Fun f ts, Fun f (xs[i := y])) ∈ r" unfolding trans_def by auto
with f
show "?p (xs[i := y])" by auto
qed (insert sig steps, auto)
then show "(Fun f ts, Fun f ss) ∈ r" ..
qed (insert refl, auto)
lemma trans_ctxt_imp_all_ctxt_closed: assumes tran: "trans r"
and refl: "refl r"
and ctxt: "ctxt.closed r"
shows "all_ctxt_closed F r"
by (rule trans_ctxt_sig_imp_all_ctxt_closed[OF tran _ ctxt.closedD[OF ctxt]], insert refl[unfolded refl_on_def], auto)
lemma all_ctxt_closed_rsteps[intro]: "all_ctxt_closed F ((rstep r)⇧*)"
by (blast intro: trans_ctxt_imp_all_ctxt_closed trans_rtrancl refl_rtrancl)
lemma subst_rsteps_imp_rsteps:
fixes σ :: "('f, 'v) subst"
assumes "∀x∈vars_term t. (σ x, τ x) ∈ (rstep R)⇧*"
shows "(t ⋅ σ, t ⋅ τ) ∈ (rstep R)⇧*"
by (rule all_ctxt_closed_subst_step)
(insert assms, auto)
lemma rtrancl_trancl_into_trancl:
assumes len: "length ts = length ss"
and steps: "∀ i < length ts. (ts ! i, ss ! i) ∈ R⇧*"
and i: "i < length ts"
and step: "(ts ! i, ss ! i) ∈ R⇧+"
and ctxt: "ctxt.closed R"
shows "(Fun f ts, Fun f ss) ∈ R⇧+"
proof -
from ctxt have ctxt_rt: "ctxt.closed (R⇧*)" by blast
from ctxt have ctxt_t: "ctxt.closed (R⇧+)" by blast
from id_take_nth_drop[OF i] have ts: "ts = take i ts @ ts ! i # drop (Suc i) ts" (is "_ = ?ts") by auto
from id_take_nth_drop[OF i[simplified len]] have ss: "ss = take i ss @ ss ! i # drop (Suc i) ss" (is "_ = ?ss") by auto
let ?mid = "take i ss @ ts ! i # drop (Suc i) ss"
from trans_ctxt_imp_all_ctxt_closed[OF trans_rtrancl refl_rtrancl ctxt_rt] have all: "all_ctxt_closed UNIV (R⇧*)" .
from ctxt_closed_one[OF ctxt_t step] have "(Fun f ?mid, Fun f ?ss) ∈ R⇧+" .
then have part1: "(Fun f ?mid, Fun f ss) ∈ R⇧+" unfolding ss[symmetric] .
from ts have lents: "length ts = length ?ts" by simp
have "(Fun f ts, Fun f ?mid) ∈ R⇧*"
proof (rule all_ctxt_closedD[OF all], simp, simp only: lents, simp add: len)
fix j
assume jts: "j < length ts"
from i len have i: "i < length ss" by auto
show "(ts ! j, ?mid ! j) ∈ R⇧*"
proof (cases "j < i")
case True
with i have j: "j < length ss" by auto
with True have id: "?mid ! j = ss ! j" by (simp add: nth_append)
from steps len j have "(ts ! j, ss ! j) ∈ R⇧*" by auto
then show ?thesis using id by simp
next
case False
show ?thesis
proof (cases "j = i")
case True
then have "?mid ! j = ts ! j" using i by (simp add: nth_append)
then show ?thesis by simp
next
case False
from i have min: "min (length ss) i = i" by simp
from False ‹¬ j < i› have "j > i" by arith
then obtain k where k: "j - i = Suc k" by (cases "j - i", auto)
then have j: "j = Suc (i+k)" by auto
with jts len have ss: "Suc i + k ≤ length ss" and jlen: "j < length ts" by auto
then have "?mid ! j = ss ! j" using j i by (simp add: nth_append min ‹¬ j < i› nth_drop[OF ss])
with steps jlen show ?thesis by auto
qed
qed
qed auto
with part1 show ?thesis by auto
qed
lemma SN_ctxt_apply_imp_SN_ctxt_to_term_list_gen:
assumes ctxt: "ctxt.closed r"
assumes SN: "SN_on r {C⟨t⟩}"
shows "SN_on r (set (ctxt_to_term_list C))"
proof -
{
fix u
assume "u ∈ set (ctxt_to_term_list C)"
from ctxt_to_term_list_supt[OF this, of t] have "C⟨t⟩ ⊵ u"
by (rule supt_imp_supteq)
from ctxt_closed_SN_on_subt[OF ctxt, OF SN this]
have "SN_on r {u}" by auto
}
then show ?thesis
unfolding SN_on_def by auto
qed
lemma rstep_subset: "ctxt.closed R' ⟹ subst.closed R' ⟹ R ⊆ R' ⟹ rstep R ⊆ R'" by fast
lemma trancl_rstep_ctxt:
"(s,t) ∈ (rstep R)⇧+ ⟹ (C⟨s⟩, C⟨t⟩) ∈ (rstep R)⇧+"
by (rule ctxt.closedD, blast)
lemma args_steps_imp_steps_gen:
assumes ctxt: "⋀ bef s t aft. (s, t) ∈ r (length bef) ⟹
length ts = Suc (length bef + length aft) ⟹
(Fun f (bef @ (s :: ('f, 'v) term) # aft), Fun f (bef @ t # aft)) ∈ R⇧*"
and len: "length ss = length ts"
and args: "⋀ i. i < length ts ⟹ (ss ! i, ts ! i) ∈ (r i)⇧*"
shows "(Fun f ss, Fun f ts) ∈ R⇧*"
proof -
let ?tss = "λi. take i ts @ drop i ss"
{
fix bef :: "('f,'v)term list" and s t and aft :: "('f,'v)term list"
assume "(s,t) ∈ (r (length bef))⇧*" and len: "length ts = Suc (length bef + length aft)"
then have "(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ R⇧*"
proof (induct)
case (step t u)
from step(3)[OF len] ctxt[OF step(2) len] show ?case by auto
qed simp
}
note one = this
have a:"∀i ≤ length ts. (Fun f ss,Fun f (?tss i)) ∈ R⇧*"
proof (intro allI impI)
fix i assume "i ≤ length ts" then show "(Fun f ss,Fun f (?tss i)) ∈ R⇧*"
proof (induct i)
case 0
then show ?case by simp
next
case (Suc i)
then have IH: "(Fun f ss,Fun f (?tss i)) ∈ R⇧*"
and i: "i < length ts" by auto
have si: "?tss (Suc i) = take i ts @ ts ! i # drop (Suc i) ss"
unfolding take_Suc_conv_app_nth[OF i] by simp
have ii: "?tss i = take i ts @ ss ! i # drop (Suc i) ss"
unfolding Cons_nth_drop_Suc[OF i[unfolded len[symmetric]]] ..
from i have i': "length (take i ts) < length ts" and len': "length (take i ts) = i" by auto
from len i have len'': "length ts = Suc (length (take i ts) + length (drop (Suc i) ss))" by simp
from one[OF args[OF i'] len''] IH
show ?case unfolding si ii len' by auto
qed
qed
from this[THEN spec, THEN mp[OF _ le_refl]]
show ?thesis using len by auto
qed
lemma args_steps_imp_steps:
assumes ctxt: "ctxt.closed R"
and len: "length ss = length ts" and args: "∀i<length ss. (ss!i, ts!i) ∈ R⇧*"
shows "(Fun f ss, Fun f ts) ∈ R⇧*"
proof (rule args_steps_imp_steps_gen[OF _ len])
fix i
assume "i < length ts" then show "(ss ! i, ts ! i) ∈ R⇧*" using args len by auto
qed (insert ctxt_closed_one[OF ctxt], auto)
lemmas args_rsteps_imp_rsteps = args_steps_imp_steps [OF ctxt_closed_rstep]
lemma replace_at_subst_steps:
fixes σ τ :: "('f, 'v) subst"
assumes acc: "all_ctxt_closed UNIV r"
and refl: "refl r"
and *: "⋀x. (σ x, τ x) ∈ r"
and "p ∈ poss t"
and "t |_ p = Var x"
shows "(replace_at (t ⋅ σ) p (τ x), t ⋅ τ) ∈ r"
using assms(4-)
proof (induction t arbitrary: p)
case (Var x)
then show ?case using refl by (simp add: refl_on_def)
next
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) ∈ 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) ∈ 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) ∈ r" by (auto simp: * all_ctxt_closed_subst_step [OF acc]) }
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) ∈ r" by (auto simp: * all_ctxt_closed_subst_step [OF acc]) }
ultimately show "(?ss ! j, ?ts ! j) ∈ r" by arith
qed
moreover have "i < length ts" by fact
ultimately show ?case
by (auto intro: all_ctxt_closedD [OF acc])
qed
lemma replace_at_subst_rsteps:
fixes σ τ :: "('f, 'v) subst"
assumes *: "⋀x. (σ x, τ x) ∈ (rstep R)⇧*"
and "p ∈ poss t"
and "t |_ p = Var x"
shows "(replace_at (t ⋅ σ) p (τ x), t ⋅ τ) ∈ (rstep R)⇧*"
by (intro replace_at_subst_steps[OF _ _ assms], auto simp: refl_on_def)
lemma substs_rsteps:
assumes "⋀x. (σ x, τ x) ∈ (rstep R)⇧*"
shows "(t ⋅ σ, t ⋅ τ) ∈ (rstep 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) ∈ (rstep R)⇧*" by auto
from args_rsteps_imp_rsteps [OF _ this] show ?case by simp
qed
lemma nrrstep_Fun_imp_arg_rstep:
fixes ss :: "('f,'v)term list"
assumes "(Fun f ss,Fun f ts) ∈ nrrstep R" (is "(?s,?t) ∈ nrrstep R")
shows "∃C i. i < length ss ∧ (ss!i,ts!i) ∈ rstep R ∧ C⟨ss!i⟩ = Fun f ss ∧ C⟨ts!i⟩ = Fun f ts"
proof -
from ‹(?s,?t) ∈ nrrstep R›
obtain l r j ps σ where A: "let C = ctxt_of_pos_term (j#ps) ?s in (j#ps) ∈ poss ?s ∧ (l,r) ∈ R ∧ C⟨l⋅σ⟩ = ?s ∧ C⟨r⋅σ⟩ = ?t" unfolding nrrstep_def rstep_r_p_s_def by force
let ?C = "ctxt_of_pos_term (j#ps) ?s"
from A have "(j#ps) ∈ poss ?s" and "(l,r) ∈ R" and "?C⟨l⋅σ⟩ = ?s" and "?C⟨r⋅σ⟩ = ?t" using Let_def by auto
have C: "?C = More f (take j ss) (ctxt_of_pos_term ps (ss!j)) (drop (Suc j) ss)" (is "?C = More f ?ss1 ?D ?ss2") by auto
from ‹?C⟨l⋅σ⟩ = ?s› have "?D⟨l⋅σ⟩ = (ss!j)" by (auto simp: take_drop_imp_nth)
from ‹(l,r) ∈ R› have "(l⋅σ,r⋅σ) ∈ (subst.closure R)" by auto
then have "(?D⟨l⋅σ⟩,?D⟨r⋅σ⟩) ∈ (ctxt.closure(subst.closure R))" and "(?C⟨l⋅σ⟩,?C⟨r⋅σ⟩) ∈ (ctxt.closure(subst.closure R))" by (auto simp only: ctxt.closure.intros)
then have D_rstep: "(?D⟨l⋅σ⟩,?D⟨r⋅σ⟩) ∈ rstep R" and "(?C⟨l⋅σ⟩,?C⟨r⋅σ⟩) ∈ rstep R"
by (auto simp: rstep_eq_closure)
from ‹?C⟨r⋅σ⟩ = ?t› and C have "?t = Fun f (take j ss @ ?D⟨r⋅σ⟩ # drop (Suc j) ss)" by auto
then have ts: "ts = (take j ss @ ?D⟨r⋅σ⟩ # drop (Suc j) ss)" by auto
from ‹j#ps ∈ poss ?s› have r0: "j < length ss" by simp
then have "(take j ss @ ?D⟨r⋅σ⟩ # drop (Suc j) ss) ! j = ?D⟨r⋅σ⟩" by (auto simp: nth_append_take)
with ts have "ts!j = ?D⟨r⋅σ⟩" by auto
let ?C' = "More f (take j ss) □ (drop (Suc j) ss)"
from D_rstep have r1: "(ss!j,ts!j) ∈ rstep R" unfolding ‹ts!j = ?D⟨r⋅σ⟩› ‹?D⟨l⋅σ⟩ = ss!j› by simp
have "?s = ?C⟨l⋅σ⟩" unfolding ‹?C⟨l⋅σ⟩ = ?s› by simp
also have "… = ?C'⟨?D⟨l⋅σ⟩⟩" unfolding C by simp
finally have r2:"?C'⟨ss!j⟩ = ?s" unfolding ‹?D⟨l⋅σ⟩ = ss!j› by simp
have "?t = ?C⟨r⋅σ⟩" unfolding ‹?C⟨r⋅σ⟩ = ?t› by simp
also have "… = ?C'⟨?D⟨r⋅σ⟩⟩" unfolding C by simp
finally have r3:"?C'⟨ts!j⟩ = ?t" unfolding ‹ts!j = ?D⟨r⋅σ⟩› by simp
from r0 r1 r2 r3 show ?thesis by best
qed
lemma pair_fun_eq[simp]:
fixes f :: "'a ⇒ 'b" and g :: "'b ⇒ 'a"
shows "((λ(x,y). (x,f y)) ∘ (λ(x,y). (x,g y))) = (λ(x,y). (x,(f ∘ g) y))" (is "?f = ?g")
proof (rule ext)
fix ab :: "'c * 'b"
obtain a b where "ab = (a,b)" by force
have "((λ(x,y). (x,f y))∘(λ(x,y). (x,g y))) (a,b) = (λ(x,y). (x,(f∘g) y)) (a,b)" by simp
then show "?f ab = ?g ab" unfolding ‹ab = (a,b)› by simp
qed
lemma restrict_singleton:
assumes "x ∈ subst_domain σ" shows "∃t. σ |s {x} = (λy. if y = x then t else Var y)"
proof -
have "σ |s {x} = (λy. if y = x then σ y else Var y)" by (simp add: subst_restrict_def)
then have "σ |s {x} = (λy. if y = x then σ x else Var y)" by (simp cong: if_cong)
then show ?thesis by (rule exI[of _ "σ x"])
qed
definition rstep_r_c_s :: "('f,'v)rule ⇒ ('f,'v)ctxt ⇒ ('f,'v)subst ⇒ ('f,'v)term rel"
where "rstep_r_c_s r C σ = {(s,t) | s t. s = C⟨fst r ⋅ σ⟩ ∧ t = C⟨snd r ⋅ σ⟩}"
lemma rstep_iff_rstep_r_c_s: "((s,t) ∈ rstep R) = (∃ l r C σ. (l,r) ∈ R ∧ (s,t) ∈ rstep_r_c_s (l,r) C σ)" (is "?left = ?right")
proof
assume ?left
then obtain l r p σ where step: "(s,t) ∈ rstep_r_p_s R (l,r) p σ"
unfolding rstep_iff_rstep_r_p_s by blast
obtain D where D: "D = ctxt_of_pos_term p s" by auto
with step have Rrule: "(l,r) ∈ R" and s: "s = D⟨l ⋅ σ⟩" and t: "t = D⟨r ⋅ σ⟩"
unfolding rstep_r_p_s_def by (force simp: Let_def)+
then show ?right unfolding rstep_r_c_s_def by auto
next
assume ?right
from this obtain l r C σ where "(l,r) ∈ R ∧ (s,t) ∈ rstep_r_c_s (l,r) C σ" by auto
then have rule: "(l,r) ∈ R" and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩"
unfolding rstep_r_c_s_def by auto
show ?left unfolding rstep_eq_closure by (auto simp: s t intro: rule)
qed
lemma rstep_subset_characterization:
"(rstep R ⊆ rstep S) = (∀ l r. (l,r) ∈ R ⟶ (∃ l' r' C σ . (l',r') ∈ S ∧ l = C⟨l' ⋅ σ⟩ ∧ r = C⟨r' ⋅ σ⟩))" (is "?left = ?right")
proof
assume ?right
show ?left
proof (rule subsetI, simp add: split_paired_all)
fix s t
assume "(s,t) ∈ rstep R"
then obtain l r C σ where step: "(l,r) ∈ R ∧ (s,t) ∈ rstep_r_c_s (l,r) C σ"
unfolding rstep_iff_rstep_r_c_s by best
then have Rrule: "(l,r) ∈ R" and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩"
unfolding rstep_r_c_s_def by (force)+
from Rrule ‹?right› obtain l' r' C' σ' where Srule: "(l',r') ∈ S" and l: "l = C'⟨l' ⋅ σ'⟩" and r: "r = C'⟨r' ⋅ σ'⟩"
by (force simp: Let_def)+
let ?D = "C ∘⇩c (C' ⋅⇩c σ)"
let ?sig = "σ' ∘⇩s σ"
have s2: "s = ?D⟨l' ⋅ ?sig⟩" by (simp add: s l)
have t2: "t = ?D⟨r' ⋅ ?sig⟩" by (simp add: t r)
from s2 t2 have sStep: "(s,t) ∈ rstep_r_c_s (l',r') ?D ?sig" unfolding rstep_r_c_s_def by force
with Srule show "(s,t) ∈ rstep S" by (simp only: rstep_iff_rstep_r_c_s, blast)
qed
next
assume ?left
show ?right
proof (rule ccontr)
assume "¬ ?right"
from this obtain l r where "(l,r) ∈ R" and cond: "∀ l' r' C σ. (l',r') ∈ S ⟶ (l ≠ C⟨l' ⋅ σ⟩ ∨ r ≠ C⟨r' ⋅ σ⟩)" by blast
then have "(l,r) ∈ rstep R" by blast
with ‹?left› have "(l,r) ∈ rstep S" by auto
with cond show False by (simp only: rstep_iff_rstep_r_c_s, unfold rstep_r_c_s_def, force)
qed
qed
lemma rstep_preserves_funas_terms_var_cond:
assumes "funas_trs R ⊆ F" and "funas_term s ⊆ F" and "(s,t) ∈ rstep R"
and wf: "⋀ l r. (l,r) ∈ R ⟹ vars_term r ⊆ vars_term l"
shows "funas_term t ⊆ F"
proof -
from ‹(s,t) ∈ rstep R› obtain l r C σ where R: "(l,r) ∈ R"
and s: "s = C⟨l⋅σ⟩" and t: "t = C⟨r⋅σ⟩" by auto
from ‹funas_trs R ⊆ F› and R have "funas_term r ⊆ F"
unfolding funas_defs [abs_def] by force
with wf[OF R] ‹funas_term s ⊆ F› show ?thesis unfolding s t by (force simp: funas_term_subst)
qed
lemma rstep_preserves_funas_terms:
assumes "funas_trs R ⊆ F" and "funas_term s ⊆ F" and "(s,t) ∈ rstep R"
and wf: "wf_trs R"
shows "funas_term t ⊆ F"
by (rule rstep_preserves_funas_terms_var_cond[OF assms(1-3)], insert wf[unfolded wf_trs_def], auto)
lemma rsteps_preserve_funas_terms_var_cond:
assumes F: "funas_trs R ⊆ F" and s: "funas_term s ⊆ F" and steps: "(s,t) ∈ (rstep R)⇧*"
and wf: "⋀ l r. (l,r) ∈ R ⟹ vars_term r ⊆ vars_term l"
shows "funas_term t ⊆ F"
using steps
proof (induct)
case base then show ?case by (rule s)
next
case (step t u)
show ?case by (rule rstep_preserves_funas_terms_var_cond[OF F step(3) step(2) wf])
qed
lemma rsteps_preserve_funas_terms:
assumes F: "funas_trs R ⊆ F" and s: "funas_term s ⊆ F"
and steps: "(s,t) ∈ (rstep R)⇧*" and wf: "wf_trs R"
shows "funas_term t ⊆ F"
by (rule rsteps_preserve_funas_terms_var_cond[OF assms(1-3)], insert wf[unfolded wf_trs_def], auto)
lemma no_Var_rstep [simp]:
assumes "wf_trs R" and "(Var x, t) ∈ rstep R" shows "False"
using rstep_imp_Fun[OF assms] by auto
lemma lhs_wf:
assumes R: "(l, r) ∈ R" and "funas_trs R ⊆ F"
shows "funas_term l ⊆ F"
using assms by (force simp: funas_trs_def funas_rule_def)
lemma rhs_wf:
assumes R: "(l, r) ∈ R" and "funas_trs R ⊆ F"
shows "funas_term r ⊆ F"
using assms by (force simp: funas_trs_def funas_rule_def)
lemma supt_map_funs_term [intro]:
assumes "t ⊳ s"
shows "map_funs_term fg t ⊳ map_funs_term fg s"
using assms
proof (induct)
case (arg s ss f)
then have "map_funs_term fg s ∈ set(map (map_funs_term fg) ss)" by simp
then show ?case unfolding term.map by (rule supt.arg)
next
case (subt s ss u f)
then have "map_funs_term fg s ∈ set(map (map_funs_term fg) ss)" by simp
with ‹map_funs_term fg s ⊳ map_funs_term fg u› show ?case
unfolding term.map by (metis supt.subt)
qed
lemma nondef_root_imp_arg_step:
assumes "(Fun f ss, t) ∈ rstep R"
and wf: "∀(l, r)∈R. is_Fun l"
and ndef: "¬ defined R (f, length ss)"
shows "∃i<length ss. (ss ! i, t |_ [i]) ∈ rstep R
∧ t = Fun f (take i ss @ (t |_ [i]) # drop (Suc i) ss)"
proof -
from assms obtain l r p σ
where rstep_r_p_s: "(Fun f ss, t) ∈ rstep_r_p_s R (l, r) p σ"
unfolding rstep_iff_rstep_r_p_s by auto
let ?C = "ctxt_of_pos_term p (Fun f ss)"
from rstep_r_p_s have "p ∈ poss (Fun f ss)" and "(l, r) ∈ R"
and "?C⟨l ⋅ σ⟩ = Fun f ss" and "?C⟨r ⋅ σ⟩ = t" unfolding rstep_r_p_s_def Let_def by auto
have "∃i q. p = i#q"
proof (cases p)
case Cons then show ?thesis by auto
next
case Nil
have "?C = □" unfolding Nil by simp
with ‹?C⟨l⋅σ⟩ = Fun f ss› have "l⋅σ = Fun f ss" by simp
have "∀(l,r)∈R. ∃f ss. l = Fun f ss"
proof (intro ballI impI)
fix lr assume "lr ∈ R"
with wf have "∀x. fst lr ≠ Var x" by auto
then have "∃f ss. (fst lr) = Fun f ss" by (cases "fst lr") auto
then show "(λ(l,r). ∃f ss. l = Fun f ss) lr" by auto
qed
with ‹(l,r) ∈ R› obtain g ts where "l = Fun g ts" unfolding wf_trs_def by best
with ‹l⋅σ = Fun f ss› ‹l = Fun g ts› and ‹(l, r) ∈ R› ndef
show ?thesis unfolding defined_def by auto
qed
then obtain i q where "p = i#q" by auto
from ‹p ∈ poss(Fun f ss)› have "i < length ss" and "q ∈ poss(ss!i)" unfolding ‹p = i#q› by auto
let ?D = "ctxt_of_pos_term q (ss!i)"
have C: "?C = More f (take i ss) ?D (drop (Suc i) ss)" unfolding ‹p = i#q› by auto
from ‹?C⟨l⋅σ⟩ = Fun f ss› have "take i ss@?D⟨l⋅σ⟩#drop (Suc i) ss = ss" unfolding C by auto
then have "(take i ss@?D⟨l⋅σ⟩#drop (Suc i) ss)!i = ss!i" by simp
with ‹i < length ss› have "?D⟨l⋅σ⟩ = ss!i" using nth_append_take[where xs = ss and i = i] by auto
have t: "t = Fun f (take i ss@?D⟨r⋅σ⟩#drop (Suc i) ss)" unfolding ‹?C⟨r⋅σ⟩ = t›[symmetric] C by simp
from ‹i < length ss› have "t|_[i] = ?D⟨r⋅σ⟩" unfolding t unfolding subt_at.simps using nth_append_take[where xs = ss and i = i] by auto
from ‹q ∈ poss(ss!i)› and ‹(l,r) ∈ R›
and ‹?D⟨l⋅σ⟩ = ss!i› and ‹t|_[i] = ?D⟨r⋅σ⟩›[symmetric]
have "(ss!i,t|_[i]) ∈ rstep_r_p_s R (l,r) q σ" unfolding rstep_r_p_s_def Let_def by auto
then have "(ss!i,t|_[i]) ∈ rstep R" unfolding rstep_iff_rstep_r_p_s by auto
from ‹i < length ss› and this and t show ?thesis unfolding ‹t|_[i] = ?D⟨r⋅σ⟩›[symmetric] by auto
qed
lemma nondef_root_imp_arg_steps:
assumes "(Fun f ss,t) ∈ (rstep R)⇧*"
and wf: "∀(l, r)∈R. is_Fun l"
and "¬ defined R (f,length ss)"
shows "∃ts. length ts = length ss ∧ t = Fun f ts ∧ (∀i<length ss. (ss!i,ts!i) ∈ (rstep R)⇧*)"
proof -
from assms obtain n where "(Fun f ss,t) ∈ (rstep R)^^n"
using rtrancl_imp_relpow by best
then show ?thesis
proof (induct n arbitrary: t)
case 0 then show ?case by auto
next
case (Suc n)
then obtain u where "(Fun f ss,u) ∈ (rstep R)^^n" and "(u,t) ∈ rstep R" by auto
with Suc obtain ts where IH1: "length ts = length ss" and IH2: "u = Fun f ts" and IH3: "∀i<length ss. (ss!i,ts!i) ∈ (rstep R)⇧*" by auto
from ‹(u,t) ∈ rstep R› have "(Fun f ts,t) ∈ rstep R" unfolding ‹u = Fun f ts› .
from nondef_root_imp_arg_step[OF this wf ‹¬ defined R (f,length ss)›[simplified IH1[symmetric]]]
obtain j where "j < length ts"
and "(ts!j,t|_[j]) ∈ rstep R"
and B: "t = Fun f (take j ts@(t|_[j])#drop (Suc j) ts)" (is "t = Fun f ?ts") by auto
from ‹j < length ts› have "length ?ts = length ts" by auto
then have A: "length ?ts = length ss" unfolding ‹length ts = length ss› .
have C: "∀i<length ss. (ss!i,?ts!i) ∈ (rstep R)⇧*"
proof (intro allI, intro impI)
fix i assume "i < length ss"
from ‹i < length ss› and IH3 have "(ss!i,ts!i) ∈ (rstep R)⇧*" by auto
have "i = j ∨ i ≠ j" by auto
then show "(ss!i,?ts!i) ∈ (rstep R)⇧*"
proof
assume "i = j"
from ‹j < length ts› have "j ≤ length ts" by simp
from nth_append_take[OF this] have "?ts!j = t|_[j]" by simp
from ‹(ts!j,t|_[j]) ∈ rstep R› have "(ts!i,t|_[i]) ∈ rstep R" unfolding ‹i = j› .
with ‹(ss!i,ts!i) ∈ (rstep R)⇧*› show ?thesis unfolding ‹i = j› unfolding ‹?ts!j = t|_[j]› by auto
next
assume "i ≠ j"
from ‹i < length ss› have "i ≤ length ts" unfolding ‹length ts = length ss› by simp
from ‹j < length ts› have "j ≤ length ts" by simp
from nth_append_take_drop_is_nth_conv[OF ‹i ≤ length ts› ‹j ≤ length ts› ‹i ≠ j›]
have "?ts!i = ts!i" by simp
with ‹(ss!i,ts!i) ∈ (rstep R)⇧*› show ?thesis by auto
qed
qed
from A and B and C show ?case by blast
qed
qed
lemma rstep_imp_nrrstep:
assumes "is_Fun s" and "¬ defined R (the (root s))" and "∀(l,r)∈R. is_Fun l"
and "(s, t) ∈ rstep R"
shows "(s, t) ∈ nrrstep R"
proof -
from ‹is_Fun s› obtain f ss where s: "s = Fun f ss" by (cases s) auto
with assms have undef: "¬ defined R (f, length ss)" by simp
from assms have non_var: "∀(l, r)∈R. is_Fun l" by auto
from nondef_root_imp_arg_step[OF ‹(s, t) ∈ rstep R›[unfolded s] non_var undef]
obtain i where "i < length ss" and step: "(ss ! i, t |_ [i]) ∈ rstep R"
and t: "t = Fun f (take i ss @ (t |_ [i]) # drop (Suc i) ss)" by auto
from step obtain C l r σ where "(l, r) ∈ R" and lhs: "ss ! i = C⟨l ⋅ σ⟩"
and rhs: "t |_ [i] = C⟨r ⋅ σ⟩" by auto
let ?C = "More f (take i ss) C (drop (Suc i) ss)"
have "(l, r) ∈ R" by fact
moreover have "?C ≠ □" by simp
moreover have "s = ?C⟨l ⋅ σ⟩"
proof -
have "s = Fun f (take i ss @ ss!i # drop (Suc i) ss)"
using id_take_nth_drop[OF ‹i < length ss›] unfolding s by simp
also have "… = ?C⟨l ⋅ σ⟩" by (simp add: lhs)
finally show ?thesis .
qed
moreover have "t = ?C⟨r ⋅ σ⟩"
proof -
have "t = Fun f (take i ss @ t |_ [i] # drop (Suc i) ss)" by fact
also have "… = Fun f (take i ss @ C⟨r ⋅ σ⟩ # drop (Suc i) ss)" by (simp add: rhs)
finally show ?thesis by simp
qed
ultimately show "(s, t) ∈ nrrstep R" unfolding nrrstep_def' by blast
qed
lemma rsteps_imp_nrrsteps:
assumes "is_Fun s" and "¬ defined R (the (root s))"
and no_vars: "∀(l, r)∈R. is_Fun l"
and "(s, t) ∈ (rstep R)⇧*"
shows "(s, t) ∈ (nrrstep R)⇧*"
using ‹(s, t) ∈ (rstep R)⇧*›
proof (induct)
case base show ?case by simp
next
case (step u v)
from assms obtain f ss where s: "s = Fun f ss" by (induct s) auto
from nrrsteps_preserve_root[OF ‹(s, u) ∈ (nrrstep R)⇧*›[unfolded s]]
obtain ts where u: "u = Fun f ts" by auto
from nrrsteps_equiv_num_args[OF ‹(s, u) ∈ (nrrstep R)⇧*›[unfolded s]]
have len: "length ss = length ts" unfolding u by simp
have "is_Fun u" by (simp add: u)
have undef: "¬ defined R (the (root u))"
using ‹¬ defined R (the (root s))›
unfolding s u by (simp add: len)
have "(u, v) ∈ nrrstep R"
using rstep_imp_nrrstep[OF ‹is_Fun u› undef no_vars] step
by simp
with step show ?case by auto
qed
lemma left_var_imp_not_SN:
fixes R :: "('f,'v)trs" and t :: "('f, 'v) term"
assumes "(Var y, r) ∈ R" (is "(?y, _) ∈ _")
shows "¬ (SN_on (rstep R) {t})"
proof (rule steps_imp_not_SN_on)
fix t :: "('f,'v)term"
let ?yt = "subst y t"
show "(t, r ⋅ ?yt) ∈ rstep R"
by (rule rstepI[OF assms, where C = □ and σ = ?yt], auto simp: subst_def)
qed
lemma not_SN_subt_imp_not_SN:
assumes ctxt: "ctxt.closed R" and SN: "¬ SN_on R {t}" and sub: "s ⊵ t"
shows "¬ SN_on R {s}"
using ctxt_closed_SN_on_subt[OF ctxt _ sub] SN
by auto
lemma root_Some:
assumes "root t = Some fn"
obtains ss where "length ss = snd fn" and "t = Fun (fst fn) ss"
using assms by (induct t) auto
lemma map_funs_rule_power:
fixes f :: "'f ⇒ 'f"
shows "((map_funs_rule f) ^^ n) = map_funs_rule (f ^^ n)"
proof (rule sym, intro ext, clarify)
fix l r :: "('f,'v)term"
show "map_funs_rule (f ^^ n) (l,r) = (map_funs_rule f ^^ n) (l,r)"
proof (induct n)
case 0
show ?case by (simp add: term.map_ident)
next
case (Suc n)
have "map_funs_rule (f ^^ Suc n) (l,r) = map_funs_rule f (map_funs_rule (f ^^ n) (l,r))"
by (simp add: map_funs_term_comp)
also have "… = map_funs_rule f ((map_funs_rule f ^^ n) (l,r))" unfolding Suc ..
also have "… = (map_funs_rule f ^^ (Suc n)) (l,r)" by simp
finally show ?case .
qed
qed
lemma map_funs_trs_power:
fixes f :: "'f ⇒ 'f"
shows "map_funs_trs f ^^ n = map_funs_trs (f ^^ n)"
proof
fix R :: "('f, 'v) trs"
have "map_funs_rule (f ^^ n) ` R = (map_funs_rule f ^^ n) ` R" unfolding map_funs_rule_power ..
also have "… = ((λ R. map_funs_trs f R) ^^ n) R" unfolding map_funs_trs.simps
apply (induct n)
apply simp
by (metis comp_apply funpow.simps(2) image_comp)
finally have "map_funs_rule (f ^^ n) ` R = (map_funs_trs f ^^ n) R" .
then show "(map_funs_trs f ^^ n) R = map_funs_trs (f ^^ n) R"
by (simp add: map_funs_trs.simps)
qed
context
fixes shp :: "'f ⇒ 'f"
begin
interpretation sharp_syntax .
definition DP_on :: "'f sig ⇒ ('f, 'v) trs ⇒ ('f, 'v) trs"
where
"DP_on F R = {(s, t). ∃l r h us. s = ♯ l ∧ t = ♯ (Fun h us) ∧
(l, r) ∈ R ∧ r ⊵ Fun h us ∧ (h, length us) ∈ F ∧ ¬ l ⊳ Fun h us}"
abbreviation "DP R ≡ DP_on {f. defined R f} R"
lemma rrstepE:
assumes "(s, t) ∈ rrstep R"
obtains l and r and σ where "(l, r) ∈ R" and "s = l ⋅ σ" and "t = r ⋅ σ"
using assms by (auto simp: rrstep_def rstep_r_p_s_def)
lemma nrrstepE:
assumes "(s, t) ∈ nrrstep R"
obtains C and l and r and σ where "C ≠ □" and "(l, r) ∈ R"
and "s = C⟨l ⋅ σ⟩" and "t = C⟨r ⋅ σ⟩"
using assms apply (auto simp: nrrstep_def rstep_r_p_s_def)
by (metis ctxt_apply_term.simps(1) poss_Cons_poss subt_at_ctxt_of_pos_term subt_at_nepos_neq)
lemma nrrstep_imp_sharp_nrrstep: assumes "(s, t) ∈ nrrstep R"
shows "(♯ s, ♯ t) ∈ nrrstep R"
proof -
from assms obtain C l r σ where "C ≠ □" and "(l, r) ∈ R"
and *: "s = C⟨l ⋅ σ⟩" "t = C⟨r ⋅ σ⟩"
by (auto elim: nrrstepE)
then obtain D f ss ts where "C = More f ss D ts"
and "s = Fun f (ss @ D⟨l ⋅ σ⟩ # ts)" by (cases C) (auto elim: sharp_term.elims)
moreover with ‹t = C⟨r ⋅ σ⟩› have "t = Fun f (ss @ D⟨r ⋅ σ⟩ # ts)"
using assms by auto
moreover define C' where "C' = More (♯ f) ss D ts"
ultimately have "♯ s = C'⟨l ⋅ σ⟩" and "♯ t = C'⟨r ⋅ σ⟩" by simp+
moreover have "C' ≠ □" using ‹C ≠ □› by (simp add: C'_def)
ultimately show "(♯ s, ♯ t) ∈ nrrstep R" using ‹(l, r) ∈ R› by (auto simp: nrrstep_def')
qed
lemma nrrstep_imp_sharp_rstep:
assumes "(s, t) ∈ nrrstep R"
shows "(♯ s, ♯ t) ∈ rstep R"
using nrrstep_imp_sharp_nrrstep[OF assms] by (rule nrrstep_imp_rstep)
lemma nrrsteps_imp_sharp_rsteps:
"(s, t) ∈ (nrrstep R)⇧* ⟹ (♯ s, ♯ t) ∈ (rstep R)⇧*"
proof (induct rule: rtrancl_induct)
case (step a b)
from ‹(a,b) ∈ nrrstep R› have "(♯ a, ♯ b) ∈ rstep R"
by (rule nrrstep_imp_sharp_rstep)
with step show ?case by auto
qed simp
lemma finiteR_imp_finiteDP:
assumes "finite R"
shows "finite (DP_on F R)"
proof -
have fS: "finite {(l, r, u).
∃h us. u = Fun h us ∧ (l,r) ∈ R ∧ r ⊵ u ∧ (h, length us) ∈ F ∧ ¬(l ⊳ u)}" (is "finite ?S")
using assms by (rule finite_imp_finite_DP_on')
let ?f = "λ(x :: ('f, 'v) term, y, z :: ('f, 'v) term). (♯ x, ♯ z)"
have eq1: "(⋃y∈?S. {x. x = ?f y}) = ?f ` ?S" by blast
with fS have "finite(?f ` ?S)" by auto
have "DP_on F R = ?f ` ?S" (is "?DP = ?T")
proof
show "?DP ⊆ ?T"
proof
fix x assume "x ∈ ?DP"
then obtain l r h us
where "fst x = ♯ l" and "snd x = ♯ (Fun h us)"
and "(l,r) ∈ R" "r ⊵ Fun h us" and "(h, length us) ∈ F" and " ¬(l ⊳ Fun h us)"
by (auto simp: DP_on_def split_def)
then have "(l,r,Fun h us) ∈ ?S" by auto
then show "x ∈ ?T" unfolding eq1[symmetric]
proof (rule UN_I)
have "x = (fst x, snd x)" by simp
then have "x = (♯ l, ♯ (Fun h us))"
unfolding ‹fst x = ♯ l› ‹snd x = ♯ (Fun h us)› .
then show "x ∈ {x. x = ?f (l,r,Fun h us)}" by auto
qed
qed
next
show "?T ⊆ ?DP"
proof
fix x assume "x ∈ ?T"
then have "x ∈ (⋃y∈?S. {x. x = ?f y})" unfolding eq1 .
then obtain y where "y ∈ ?S" and "x = ?f y" by fast
then obtain l r h us where "y = (l, r, Fun h us)" and dp: "(l, r) ∈ R"
and "r ⊵ Fun h us" and "(h, length us) ∈ F" and "¬ (l ⊳ Fun h us)" by blast
moreover with ‹x = ?f y› have "x = (♯ l, ♯ (Fun h us))" by auto
ultimately show "x ∈ ?DP" using dp unfolding DP_on_def by auto
qed
qed
with fS show ?thesis by auto
qed
lemma vars_sharp_eq_vars [simp]: "vars_term (♯ t) = vars_term t"
by (induct t) auto
lemma wf_trs_imp_wf_DP_on:
assumes "wf_trs R"
shows "wf_trs (DP_on F R)"
unfolding wf_trs_def
proof (intro allI impI)
fix s t
assume "(s,t) ∈ DP_on F R"
then obtain l r h us where "s = ♯ l" and "t = ♯ (Fun h us)" and "(l, r) ∈ R"
and "r ⊵ (Fun h us)" "¬ (l ⊳ Fun h us)"
by (auto simp:DP_on_def)
from ‹wf_trs R› and ‹(l,r) ∈ R›
have "∃f ss. l = Fun f ss" and "vars_term r ⊆ vars_term l" by (auto simp: wf_trs_def)
from ‹∃f ss. l = Fun f ss› obtain f ss where "l = Fun f ss" by auto
then have "s = Fun (♯ f) ss" unfolding ‹s = ♯ l› by simp
then have "∃f ss. s = Fun f ss" by auto
from ‹r ⊵ Fun h us› have "vars_term(Fun h us) ≤ vars_term r" by (induct rule: supteq.induct) auto
then have "vars_term t ⊆ vars_term s" unfolding ‹s = ♯ l›
and ‹t = ♯ (Fun h us)› vars_sharp_eq_vars using ‹vars_term r ≤ vars_term l› by simp
from ‹∃f ss. s = Fun f ss› ‹vars_term t ⊆ vars_term s›
show "(∃f ss. s = Fun f ss) ∧ vars_term t ⊆ vars_term s" by simp
qed
lemma sharp_eq_imp_eq:
fixes s :: "('f, 'v) term"
assumes "inj (♯ :: 'f ⇒ 'f)"
shows "♯ s = ♯ t ⟹ s = t"
proof (cases s)
case (Var x)
assume "♯ s = ♯ t" with Var show ?thesis by (induct t) auto
next
case (Fun f ss)
assume "♯ s = ♯ t"
with Fun have "♯ (Fun f ss) = ♯ t" by simp
then obtain g ts where t: "t = Fun g ts" by (induct t) auto
with ‹♯ s = ♯ t› have "Fun (♯ f) ss = Fun (♯ g) ts" unfolding ‹s = Fun f ss› ‹t = Fun g ts›
by simp
then have "f = g" and "ss = ts" using ‹inj (♯ :: 'f ⇒ 'f)›[unfolded inj_on_def] by auto
then show ?thesis unfolding Fun t by simp
qed
lemma DP_on_step_in_R:
fixes R :: "('f, 'v) trs" and v :: "('f, 'v) term ⇒ 'v"
assumes "(s, t) ∈ DP_on F R" and inj: "inj (♯ :: 'f ⇒ 'f)"
shows "∃C. funas_ctxt C ⊆ funas_trs R ∧
(sharp_term (the_inv ♯) s, C⟨sharp_term (the_inv ♯) t⟩) ∈ R"
proof -
let ?us = "sharp_term (the_inv (♯ :: 'f ⇒ 'f))"
from assms obtain l r f ts
where s: "s = ♯ l" and t: "t = ♯ (Fun f ts)"
and R: "(l,r) ∈ R" and sub: "r ⊵ Fun f ts" unfolding DP_on_def supt_supteq_conv by auto
from sub obtain C where r: "r = C⟨Fun f ts⟩" by auto
from rhs_wf[OF R subset_refl] have "funas_term r ⊆ funas_trs R" .
then have "funas_term (C⟨Fun f ts⟩) ⊆ funas_trs R" unfolding r .
then have "funas_ctxt C ⊆ funas_trs R" and "funas_term (Fun f ts) ⊆ funas_trs R" by auto
from lhs_wf[OF R subset_refl] have "funas_term l ⊆ funas_trs R" .
have us: "?us s = l" unfolding s by (cases l, auto simp: the_inv_f_f[OF inj])
have ut: "?us t = Fun f ts" unfolding t by (simp add: the_inv_f_f[OF inj])
from R have "(?us s,C⟨?us t⟩) ∈ R" unfolding us ut r .
with ‹funas_ctxt C ⊆ funas_trs R› show ?thesis by best
qed
lemma sharp_rrstep_imp_rstep:
assumes rrstep: "(♯ s, ♯ t) ∈ subst.closure (DP_on F R)" and "inj (♯ :: 'f ⇒ 'f)" and "wf_trs R"
shows "∃C. (s, C⟨t⟩) ∈ rstep R"
proof -
from ‹wf_trs R› have "wf_trs (DP_on F R)" by (rule wf_trs_imp_wf_DP_on)
from rrstep obtain l r σ where "(l,r) ∈ DP_on F R" and ss: "♯ s = l⋅σ" and st: "♯ t = r⋅σ"
by (induct, auto)
from ‹(l,r) ∈ DP_on F R› obtain l' r' h' us'
where l: "l = ♯ l'" and r: "r = ♯ (Fun h' us')" (is "r = ♯ ?u'")
and l'r': "(l',r') ∈ R" and "r' ⊵ (Fun h' us')" and "¬ l' ⊳ Fun h' us'"
unfolding DP_on_def by auto
from ‹wf_trs R› and ‹(l',r') ∈ R› obtain f' ss' where l': "l' = Fun f' ss'" using wf_trs_imp_lhs_Fun by best
from ‹r' ⊵ ?u'› obtain C where r': "r' = C⟨?u'⟩" by best
have ss: "♯ s = (Fun (♯ f') ss') ⋅ σ" unfolding ss l l' by simp
then obtain f where s: "s = (Fun f ss') ⋅ σ" by (cases s, auto)
from s ss have "♯ f = ♯ f'" by simp
with ‹inj (♯ :: 'f ⇒ 'f)›[unfolded inj_on_def] have f: "f = f'" by simp
have ts: "♯ t = (Fun (♯ h') us') ⋅ σ" unfolding st r by simp
then obtain h where t: "t = (Fun h us') ⋅ σ" by (cases t, auto)
from t ts have "♯ h = ♯ h'" by simp
with ‹inj (♯ :: 'f ⇒ 'f)›[unfolded inj_on_def] have h: "h = h'" by simp
show ?thesis
by (rule exI[of _ "C ⋅⇩c σ"], unfold s t f h, rule rstepI[OF l'r', of _ □ σ], unfold l' r', simp, simp)
qed
definition DP_simple :: " 'f sig ⇒ ('f, 'v) trs ⇒ ('f, 'v) trs"
where
"DP_simple D R = {(s, t).
∃l r h us. s = ♯ l ∧ t = ♯ (Fun h us) ∧ (l, r) ∈ R ∧ (h, length us) ∈ D ∧ r ⊵ Fun h us}"
lemma DP_on_subset_DP_simple: "DP_on F R ⊆ DP_simple F R"
by (auto simp: DP_on_def DP_simple_def)
lemma funas_DP_simple_subset:
"funas_trs (DP_simple D R) ⊆ funas_trs R ∪ ♯ (funas_trs R)"
(is "?F ⊆ ?H ∪ ?I")
proof (rule subrelI)
fix f n
assume "(f,n) ∈ ?F"
then obtain s t where st: "(s,t) ∈ DP_simple D R" and "(f,n) ∈ funas_rule (s,t)"
unfolding funas_trs_def by auto
then obtain u where fn: "(f,n) ∈ funas_term u" and u: "u = s ∨ u = t" unfolding funas_rule_def
by auto
from st[unfolded DP_simple_def] obtain l r uu where lr: "(l,r) ∈ R" and s: "s = ♯ l" and t: "t = ♯ uu" and uu: "r ⊵ uu"
by force
from fn u[unfolded s t] obtain v where fn: "(f, n) ∈ funas_term (♯ v)" and v: "v = l ∨ v = uu" by auto
from fn have fn: "(f, n) ∈ funas_term v ∪ ♯ (funas_term v)"
by (cases v, auto)
from uu obtain C where r: "r = C⟨uu⟩" ..
have "funas_term uu ⊆ funas_term r" unfolding r by simp
with v have "funas_term v ⊆ funas_rule (l,r)" unfolding funas_rule_def by auto
then have subset: "funas_term v ⊆ funas_trs R" using lr unfolding funas_trs_def by auto
with fn show "(f,n) ∈ ?H ∪ ?I" by auto
qed
lemma funas_DP_on_subset:
"funas_trs (DP_on F R) ⊆ funas_trs R ∪ ♯ (funas_trs R)"
by (rule order.trans [OF _ funas_DP_simple_subset [of F]])
(insert DP_on_subset_DP_simple, auto simp: funas_trs_def)
end
text ‹The set of minimally nonterminating terms with respect to a relation @{term "R"}.›
definition Tinf :: "('f, 'v) trs ⇒ ('f, 'v) terms"
where
"Tinf R = {t. ¬ SN_on R {t} ∧ (∀s ⊲ t. SN_on R {s})}"
lemma not_SN_imp_subt_Tinf:
assumes "¬ SN_on R {s}" shows "∃t⊴s. t ∈ Tinf R"
proof -
let ?S = "{t | t. s ⊵ t ∧ ¬ SN_on R {t}}"
from assms have s: "s ∈ ?S" by auto
from mp[OF spec[OF spec[OF SN_imp_minimal[OF SN_supt]]] s]
obtain t where st: "s ⊵ t" and nSN: "¬ SN_on R {t}"
and min: "∀ u. (t,u) ∈ supt ⟶ u ∉ ?S" by auto
have "t ∈ Tinf R" unfolding Tinf_def
proof (simp add: nSN, intro allI impI)
fix u
assume u: "t ⊳ u"
from u st have "s ⊳ u" using supteq_supt_trans by auto
with min u show "SN_on R {u}" by auto
qed
with st show ?thesis by auto
qed
lemma not_SN_imp_Tinf:
assumes "¬ SN R" shows "∃t. t ∈ Tinf R"
using assms not_SN_imp_subt_Tinf unfolding SN_on_def by blast
lemma ctxt_of_pos_term_map_funs_term_conv [iff]:
assumes "p ∈ poss s"
shows "map_funs_ctxt fg (ctxt_of_pos_term p s) = (ctxt_of_pos_term p (map_funs_term fg s))"
using assms
proof (induct s arbitrary: p)
case (Var x) then show ?case by simp
next
case (Fun f ss) then show ?case
proof (cases p)
case Nil then show ?thesis by simp
next
case (Cons i q)
with ‹p ∈ poss(Fun f ss)› have "i < length ss" and "q ∈ poss(ss!i)" unfolding Cons poss.simps by auto
then have "ss!i ∈ set ss" by simp
with Fun and ‹q ∈ poss(ss!i)›
have IH: "map_funs_ctxt fg(ctxt_of_pos_term q (ss!i)) = ctxt_of_pos_term q (map_funs_term fg (ss!i))" by simp
have "map_funs_ctxt fg(ctxt_of_pos_term p (Fun f ss)) = map_funs_ctxt fg(ctxt_of_pos_term (i#q) (Fun f ss))" unfolding Cons by simp
also have "… = map_funs_ctxt fg(More f (take i ss) (ctxt_of_pos_term q (ss!i)) (drop (Suc i) ss))" by simp
also have "… = More (fg f) (map (map_funs_term fg) (take i ss)) (map_funs_ctxt fg(ctxt_of_pos_term q (ss!i))) (map (map_funs_term fg) (drop (Suc i) ss))" by simp
also have "… = More (fg f) (map (map_funs_term fg) (take i ss)) (ctxt_of_pos_term q (map_funs_term fg (ss!i))) (map (map_funs_term fg) (drop (Suc i) ss))" unfolding IH by simp
also have "… = More (fg f) (take i (map (map_funs_term fg) ss)) (ctxt_of_pos_term q (map (map_funs_term fg) ss!i)) (drop (Suc i) (map (map_funs_term fg) ss))" unfolding nth_map[OF ‹i < length ss›,symmetric] take_map drop_map nth_map by simp
finally show ?thesis unfolding Cons by simp
qed
qed
lemma var_rewrite_imp_not_SN:
assumes sn: "SN_on (rstep R) {u}" and step: "(t, s) ∈ rstep R"
shows "is_Fun t"
using assms
proof (cases t)
case (Fun f ts) then show ?thesis by simp
next
case (Var x)
from step obtain l r p σ where "(Var x, s) ∈ rstep_r_p_s R (l,r) p σ" unfolding Var rstep_iff_rstep_r_p_s by best
then have "l ⋅ σ = Var x" and rule: "(l,r) ∈ R" unfolding rstep_r_p_s_def by (auto simp: Let_def)
from this obtain y where "l = Var y" (is "_ = ?y") by (cases l, auto)
with rule have "(?y, r) ∈ R" by auto
then have "¬ (SN_on (rstep R) {u})" by (rule left_var_imp_not_SN)
with sn show ?thesis by blast
qed
lemma rstep_id: "rstep Id = Id"
by (rule set_eqI, simp only: split_paired_all, simp only: rstep_iff_rstep_r_p_s, unfold rstep_r_p_s_def, auto simp: Let_def,
rule exI, rule exI[where x = "[]"], auto, rule exI[where x = Var], auto)
lemma map_funs_rule_id [simp]: "map_funs_rule id = id"
by (intro ext, auto)
lemma map_funs_trs_id [simp]: "map_funs_trs id = id"
by (intro ext, auto simp: map_funs_trs.simps)
definition sig_step :: "'f sig ⇒ ('f, 'v) trs ⇒ ('f, 'v) trs" where
"sig_step F R = {(a, b). (a, b) ∈ R ∧ funas_term a ⊆ F ∧ funas_term b ⊆ F}"
lemma sig_step_union: "sig_step F (R ∪ S) = sig_step F R ∪ sig_step F S"
unfolding sig_step_def by auto
lemma sig_step_UNIV: "sig_step UNIV R = R" unfolding sig_step_def by simp
lemma sig_stepI[intro]: "(a,b) ∈ R ⟹ funas_term a ⊆ F ⟹ funas_term b ⊆ F ⟹ (a,b) ∈ sig_step F R" unfolding sig_step_def by auto
lemma sig_stepE[elim,consumes 1]: "(a,b) ∈ sig_step F R ⟹ ⟦(a,b) ∈ R ⟹ funas_term a ⊆ F ⟹ funas_term b ⊆ F ⟹ P⟧ ⟹ P" unfolding sig_step_def by auto
lemma all_ctxt_closed_sig_rsteps [intro]:
fixes R :: "('f, 'v) trs"
shows "all_ctxt_closed F ((sig_step F (rstep R))⇧*)" (is "all_ctxt_closed _ (?R⇧*)")
proof (rule trans_ctxt_sig_imp_all_ctxt_closed)
fix C :: "('f,'v)ctxt" and s t :: "('f,'v)term"
assume C: "funas_ctxt C ⊆ F"
and s: "funas_term s ⊆ F"
and t: "funas_term t ⊆ F"
and steps: "(s,t) ∈ ?R⇧*"
from steps
show "(C ⟨ s ⟩, C ⟨ t ⟩) ∈ ?R⇧*"
proof (induct)
case (step t u)
from step(2) have tu: "(t,u) ∈ rstep R" and t: "funas_term t ⊆ F" and u: "funas_term u ⊆ F" by auto
have "(C ⟨ t ⟩, C ⟨ u ⟩) ∈ ?R" by (rule sig_stepI[OF rstep_ctxt[OF tu]], insert C t u, auto)
with step(3) show ?case by auto
qed auto
qed (auto intro: trans_rtrancl)
lemma wf_loop_imp_sig_ctxt_rel_not_SN:
assumes R: "(l,C⟨l⟩) ∈ R" and wf_l: "funas_term l ⊆ F"
and wf_C: "funas_ctxt C ⊆ F"
and ctxt: "ctxt.closed R"
shows "¬ SN_on (sig_step F R) {l}"
proof -
let ?t = "λ i. (C^i)⟨l⟩"
have "∀i. funas_term (?t i) ⊆ F"
proof
fix i show "funas_term (?t i) ⊆ F" unfolding funas_term_ctxt_apply
by (rule Un_least[OF _ wf_l], induct i, insert wf_C, auto)
qed
moreover have "∀i. (?t i,?t(Suc i)) ∈ R"
proof
fix i
show "(?t i, ?t (Suc i)) ∈ R"
proof (induct i)
case 0 with R show ?case by auto
next
case (Suc i)
from ctxt.closedD[OF ctxt Suc, of C]
show ?case by simp
qed
qed
ultimately have steps: "∀i. (?t i,?t(Suc i)) ∈ sig_step F R" unfolding sig_step_def by blast
show ?thesis unfolding SN_defs
by (simp, intro exI[of _ ?t], simp only: steps, simp)
qed
lemma lhs_var_imp_sig_step_not_SN_on:
assumes x: "(Var x, r) ∈ R" and F: "funas_trs R ⊆ F"
shows "¬ SN_on (sig_step F (rstep R)) {Var x}"
proof -
let ?σ = "(λx. r)"
let ?t = "λi. (?σ ^^ i) x"
obtain t where t: "t = ?t" by auto
from rhs_wf[OF x F] have wf_r: "funas_term r ⊆ F" .
{
fix i
have "funas_term (?t i) ⊆ F"
proof (induct i)
case 0 show ?case using wf_r by auto
next
case (Suc i)
have "?t (Suc i) = ?t i ⋅ ?σ" unfolding subst_power_Suc subst_compose_def by simp
also have "funas_term ... ⊆ F" unfolding funas_term_subst[of "?t i"]
using Suc wf_r by auto
finally show ?case .
qed
} note wf_t = this
{
fix i
have "(t i, t (Suc i)) ∈ (sig_step F (rstep R))" unfolding t
by (rule sig_stepI[OF rstepI[OF x, of _ □ "?σ ^^ i"] wf_t wf_t], auto simp: subst_compose_def)
} note steps = this
have x: "t 0 = Var x" unfolding t by simp
with steps show ?thesis unfolding SN_defs not_not
by (intro exI[of _ t], auto)
qed
lemma rhs_free_vars_imp_sig_step_not_SN:
assumes R: "(l,r) ∈ R" and free: "¬ vars_term r ⊆ vars_term l"
and F: "funas_trs R ⊆ F"
shows "¬ SN_on (sig_step F (rstep R)) {l}"
proof -
from free obtain x where x: "x ∈ vars_term r - vars_term l" by auto
then have "x ∈ vars_term r" by simp
from supteq_Var[OF this] have "r ⊵ Var x" .
then obtain C where r: "C⟨Var x⟩ = r" by auto
let ?σ = "λy. if y = x then l else Var y"
let ?t = "λi. ((C ⋅⇩c ?σ)^i)⟨l⟩"
from rhs_wf[OF R] F have wf_r: "funas_term r ⊆ F" by fast
from lhs_wf[OF R] F have wf_l: "funas_term l ⊆ F" by fast
from wf_r[unfolded r[symmetric]]
have wf_C: "funas_ctxt C ⊆ F" by simp
from x have neq: "∀y∈vars_term l. y ≠ x" by auto
have "l⋅?σ = l ⋅ Var"
by (rule term_subst_eq, insert neq, auto)
then have l: "l ⋅ ?σ = l" by simp
have wf_C: "funas_ctxt (C ⋅⇩c ?σ) ⊆ F" using wf_C wf_l
by simp
have rsigma: "r⋅?σ = (C ⋅⇩c ?σ)⟨l⟩" unfolding r[symmetric] by simp
from R have lr: "(l ⋅ ?σ, r ⋅ ?σ) ∈ rstep R" by auto
then have lr: "(l,(C ⋅⇩c ?σ)⟨l⟩) ∈ rstep R" unfolding l unfolding rsigma .
show ?thesis
by (rule wf_loop_imp_sig_ctxt_rel_not_SN[OF lr wf_l wf_C ctxt_closed_rstep])
qed
lemma lhs_var_imp_rstep_not_SN: assumes "(Var x,r) ∈ R" shows "¬ SN(rstep R)"
using lhs_var_imp_sig_step_not_SN_on[OF assms subset_refl] unfolding sig_step_def SN_defs by blast
lemma rhs_free_vars_imp_rstep_not_SN:
assumes "(l,r) ∈ R" and "¬ vars_term r ⊆ vars_term l"
shows "¬ SN_on (rstep R) {l}"
using rhs_free_vars_imp_sig_step_not_SN[OF assms subset_refl] unfolding sig_step_def SN_defs by blast
lemma free_right_rewrite_imp_not_SN:
assumes step: "(t,s) ∈ rstep_r_p_s R (l,r) p σ"
and vars: "¬ vars_term l ⊇ vars_term r"
shows "¬ SN_on (rstep R) {t}"
proof
assume SN: "SN_on (rstep R) {t}"
let ?C = "ctxt_of_pos_term p t"
from step have left: "?C⟨l ⋅ σ⟩ = t" (is "?t = t") and right: "?C⟨r ⋅ σ⟩ = s" and pos: "p ∈ poss t"
and rule: "(l,r) ∈ R"
unfolding rstep_r_p_s_def by (auto simp: Let_def)
from rhs_free_vars_imp_rstep_not_SN[OF rule vars] have nSN:"¬ SN_on (rstep R) {l}" by simp
from SN_imp_SN_subt[OF SN ctxt_imp_supteq[of ?C "l ⋅ σ", simplified left]]
have SN: "SN_on (rstep R) {l ⋅ σ}" .
from SNinstance_imp_SN[OF SN] nSN show False by simp
qed
lemma not_SN_on_rstep_subst_apply_term[intro]:
assumes "¬ SN_on (rstep R) {t}" shows "¬ SN_on (rstep R) {t ⋅ σ}"
using assms unfolding SN_on_def by best
lemma SN_rstep_imp_wf_trs: assumes "SN (rstep R)" shows "wf_trs R"
proof (rule ccontr)
assume "¬ wf_trs R"
then obtain l r where R: "(l,r) ∈ R"
and not_wf: "(∀f ts. l ≠ Fun f ts) ∨ ¬(vars_term r ⊆ vars_term l)" unfolding wf_trs_def
by auto
from not_wf have "¬ SN (rstep R)"
proof
assume free: "¬ vars_term r ⊆ vars_term l"
from rhs_free_vars_imp_rstep_not_SN[OF R free] show ?thesis unfolding SN_defs by auto
next
assume "∀f ts. l ≠ Fun f ts"
then obtain x where l:"l = Var x" by (cases l) auto
with R have "(Var x,r) ∈ R" unfolding l by simp
from lhs_var_imp_rstep_not_SN[OF this] show ?thesis by simp
qed
with assms show False by blast
qed
lemma SN_sig_step_imp_wf_trs: assumes SN: "SN (sig_step F (rstep R))" and F: "funas_trs R ⊆ F" shows "wf_trs R"
proof (rule ccontr)
assume "¬ wf_trs R"
then obtain l r where R: "(l,r) ∈ R"
and not_wf: "(∀f ts. l ≠ Fun f ts) ∨ ¬(vars_term r ⊆ vars_term l)" unfolding wf_trs_def
by auto
from not_wf have "¬ SN (sig_step F (rstep R))"
proof
assume free: "¬ vars_term r ⊆ vars_term l"
from rhs_free_vars_imp_sig_step_not_SN[OF R free F] show ?thesis unfolding SN_on_def by auto
next
assume "∀f ts. l ≠ Fun f ts"
then obtain x where l:"l = Var x" by (cases l) auto
with R have "(Var x,r) ∈ R" unfolding l by simp
from lhs_var_imp_sig_step_not_SN_on[OF this F] show ?thesis
unfolding SN_on_def by auto
qed
with assms show False by blast
qed
lemma rstep_cases'[consumes 1, case_names root nonroot]:
assumes rstep: "(s, t) ∈ rstep R"
and root: "⋀l r σ. (l, r) ∈ R ⟹ l ⋅ σ = s ⟹ r ⋅ σ = t ⟹ P"
and nonroot: "⋀f ss1 u ss2 v. s = Fun f (ss1 @ u # ss2) ⟹ t = Fun f (ss1 @ v # ss2) ⟹ (u, v) ∈ rstep R ⟹ P"
shows "P"
proof -
from rstep_imp_C_s_r[OF rstep] obtain C σ l r
where R: "(l,r) ∈ R" and s: "C⟨l⋅σ⟩ = s" and t: "C⟨r⋅σ⟩ = t" by fast
show ?thesis proof (cases C)
case Hole
from s t have "l⋅σ = s" and "r⋅σ = t" by (auto simp: Hole)
with R show ?thesis by (rule root)
next
case (More f ss1 D ss2)
let ?u = "D⟨l⋅σ⟩"
let ?v = "D⟨r⋅σ⟩"
have "s = Fun f (ss1 @ ?u # ss2)" by (simp add: More s[symmetric])
moreover have "t = Fun f (ss1 @ ?v # ss2)" by (simp add: More t[symmetric])
moreover have "(?u,?v) ∈ rstep R" using R by auto
ultimately show ?thesis by (rule nonroot)
qed
qed
lemma NF_Var: assumes wf: "wf_trs R" shows "(Var x, t) ∉ rstep R"
proof
assume "(Var x, t) ∈ rstep R"
from rstep_imp_C_s_r[OF this] obtain C l r σ
where R: "(l,r) ∈ R" and lhs: "Var x = C⟨l⋅σ⟩" by fast
from lhs have "Var x = l⋅σ" by (induct C) auto
then obtain y where l: "l = Var y" by (induct l) auto
from wf R obtain f ss where "l = Fun f ss" unfolding wf_trs_def by best
with l show False by simp
qed
lemma rstep_cases_Fun'[consumes 2, case_names root nonroot]:
assumes wf: "wf_trs R"
and rstep: "(Fun f ss,t) ∈ rstep R"
and root': "⋀ls r σ. (Fun f ls,r) ∈ R ⟹ map (λt. t⋅σ) ls = ss ⟹ r⋅σ = t ⟹ P"
and nonroot': "⋀i u. i < length ss ⟹ t = Fun f (take i ss@u#drop (Suc i) ss) ⟹ (ss!i,u) ∈ rstep R ⟹ P"
shows "P"
using rstep proof (cases rule: rstep_cases')
case (root l r σ)
with wf obtain g ls where l: "l = Fun g ls" unfolding wf_trs_def by best
from root have [simp]: "g = f" unfolding l by simp
from root have "(Fun f ls,r) ∈ R" and "map (λt. t⋅σ) ls = ss" and "r⋅σ = t" unfolding l by auto
then show ?thesis by (rule root')
next
case (nonroot g ss1 u ss2 v)
then have [simp]: "g = f" and args: "ss = ss1 @ u # ss2" by auto
let ?i = "length ss1"
from args have ss1: "take ?i ss = ss1" by simp
from args have "drop ?i ss = u # ss2" by simp
then have "drop (Suc 0) (drop ?i ss) = ss2" by simp
then have ss2: "drop (Suc ?i) ss = ss2" by simp
from args have len: "?i < length ss" by simp
from id_take_nth_drop[OF len] have "ss = take ?i ss @ ss!?i # drop (Suc ?i) ss" by simp
then have u: "ss!?i = u" unfolding args unfolding ss1[unfolded args] ss2[unfolded args] by simp
from nonroot have "t = Fun f (take ?i ss@v#drop (Suc ?i) ss)" unfolding ss1 ss2 by simp
moreover from nonroot have "(ss!?i,v) ∈ rstep R" unfolding u by simp
ultimately show ?thesis by (rule nonroot'[OF len])
qed
lemma rstep_preserves_undefined_root:
assumes "wf_trs R" and "¬ defined R (f, length ss)" and "(Fun f ss, t) ∈ rstep R"
shows "∃ts. length ts = length ss ∧ t = Fun f ts"
proof -
from ‹wf_trs R› and ‹(Fun f ss, t) ∈ rstep R› show ?thesis
proof (cases rule: rstep_cases_Fun')
case (root ls r σ)
then have "defined R (f, length ss)" by (auto simp: defined_def)
with ‹¬ defined R (f, length ss)› show ?thesis by simp
next
case (nonroot i u) then show ?thesis by simp
qed
qed
lemma rstep_ctxt_imp_nrrstep: assumes step: "(s,t) ∈ rstep R" and C: "C ≠ □" shows "(C⟨s⟩,C⟨t⟩) ∈ nrrstep R"
proof -
from step[unfolded rstep_iff_rstep_r_c_s rstep_r_c_s_def]
obtain l r D σ where lr: "(l,r) ∈ R" and s: "s = D⟨l ⋅ σ⟩" and t: "t = D⟨r ⋅ σ⟩" by auto
show ?thesis
by (unfold nrrstep_def', rule, clarify, rule exI[of _ l], rule exI[of _ r], rule exI[of _ "C ∘⇩c D"], rule exI[of _ σ], simp add: lr s t, cases C, auto simp: C)
qed
lemma rsteps_ctxt_imp_nrrsteps: assumes steps: "(s,t) ∈ (rstep R)⇧*" and C: "C ≠ □" shows "(C⟨s⟩,C⟨t⟩) ∈ (nrrstep R)⇧*"
using steps
proof (induct)
case base show ?case by simp
next
case (step t u)
from rstep_ctxt_imp_nrrstep[OF step(2) C] step(3) show ?case by simp
qed
lemma nrrstep_mono:
assumes "R ⊆ R'"
shows "nrrstep R ⊆ nrrstep R'"
using assms by (force simp: nrrstep_def rstep_r_p_s_def Let_def)
lemma singleton_subst_restrict [simp]:
"subst x s |s {x} = subst x s"
unfolding subst_def subst_restrict_def by (rule ext) simp
lemma singleton_subst_map [simp]:
"f ∘ subst x s = (f ∘ Var)(x := f s)" by (intro ext, auto simp: subst_def)
lemma subst_restrict_vars [simp]:
"(λz. if z ∈ V then f z else g z) |s V = f |s V"
unfolding subst_restrict_def
proof (intro ext)
fix x
show "(if x ∈ V then if x ∈ V then f x else g x else Var x)
= (if x ∈ V then f x else Var x)" by simp
qed
lemma subst_restrict_restrict [simp]:
assumes "V ∩ W = {}"
shows "((λz. if z ∈ V then f z else g z) |s W) = g |s W"
unfolding subst_restrict_def
proof (intro ext)
fix x
show "(if x ∈ W then if x ∈ V then f x else g x else Var x)
= (if x ∈ W then g x else Var x)" using assms by auto
qed
lemma rstep_rstep: "rstep (rstep R) = rstep R"
proof -
have "ctxt.closure (subst.closure (rstep R)) = rstep R" by (simp only: subst_closure_rstep_eq ctxt_closure_rstep_eq)
then show ?thesis unfolding rstep_eq_closure .
qed
lemma rstep_trancl_distrib: "rstep (R⇧+) ⊆ (rstep R)⇧+"
proof
fix s t
assume "(s,t) ∈ rstep (R⇧+)"
then show "(s,t) ∈ (rstep R)⇧+"
proof
fix l r C σ
presume lr: "(l,r) ∈ R⇧+" and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩"
from lr have "(C⟨l ⋅ σ⟩, C⟨r ⋅ σ⟩) ∈ (rstep R)⇧+"
proof(induct)
case (base r)
then show ?case by auto
next
case (step r rr)
from step(2) have "(C⟨r ⋅ σ⟩, C⟨rr ⋅ σ⟩) ∈ (rstep R)" by auto
with step(3) show ?case by auto
qed
then show "(s,t) ∈ (rstep R)⇧+" unfolding s t .
qed auto
qed
lemma rsteps_closed_subst:
assumes "(s, t) ∈ (rstep R)⇧*"
shows "(s ⋅ σ, t ⋅ σ) ∈ (rstep R)⇧*"
using assms and subst.closed_rtrancl [OF subst_closed_rstep] by (auto simp: subst.closed_def)
lemma join_subst:
"subst.closed r ⟹ (s, t) ∈ r⇧↓ ⟹ (s ⋅ σ, t ⋅ σ) ∈ r⇧↓"
by (simp add: join_def subst.closedD subst.closed_comp subst.closed_converse subst.closed_rtrancl)
lemma join_subst_rstep [intro]:
"(s, t) ∈ (rstep R)⇧↓ ⟹ (s ⋅ σ, t ⋅ σ) ∈ (rstep R)⇧↓"
by (intro join_subst, auto)
lemma join_ctxt [intro]:
assumes "(s, t) ∈ (rstep R)⇧↓"
shows "(C⟨s⟩, C⟨t⟩) ∈ (rstep R)⇧↓"
proof -
from assms obtain u where "(s, u) ∈ (rstep R)⇧*" and "(t, u) ∈ (rstep R)⇧*" by auto
then have "(C⟨s⟩, C⟨u⟩) ∈ (rstep R)⇧*" and "(C⟨t⟩, C⟨u⟩) ∈ (rstep R)⇧*" by (auto intro: rsteps_closed_ctxt)
then show ?thesis by blast
qed
lemma rstep_simps:
"rstep (R⇧=) = (rstep R)⇧="
"rstep (rstep R) = rstep R"
"rstep (R ∪ S) = rstep R ∪ rstep S"
"rstep Id = Id"
"rstep (R⇧↔) = (rstep R)⇧↔"
by auto
lemma rstep_rtrancl_idemp [simp]:
"rstep ((rstep R)⇧*) = (rstep R)⇧*"
proof -
{ fix s t
assume "(s, t) ∈ rstep ((rstep R)⇧*)"
then have "(s, t) ∈ (rstep R)⇧*"
by (induct) (metis rsteps_closed_ctxt rsteps_closed_subst) }
then show ?thesis by auto
qed
definition instance_rule :: "('f, 'v) rule ⇒ ('f, 'w) rule ⇒ bool" where
[code del]: "instance_rule lr st ⟷ (∃ σ. fst lr = fst st ⋅ σ ∧ snd lr = snd st ⋅ σ)"
definition eq_rule_mod_vars :: "('f, 'v) rule ⇒ ('f, 'v) rule ⇒ bool" where
"eq_rule_mod_vars lr st ⟷ instance_rule lr st ∧ instance_rule st lr"
notation eq_rule_mod_vars ("(_/ =⇩v _)" [51,51] 50)
lemma instance_rule_var_cond: assumes eq: "instance_rule (s,t) (l,r)"
and vars: "vars_term r ⊆ vars_term l"
shows "vars_term t ⊆ vars_term s"
proof -
from eq[unfolded instance_rule_def]
obtain τ where s: "s = l ⋅ τ" and t: "t = r ⋅ τ" by auto
show ?thesis
proof
fix x
assume "x ∈ vars_term t"
from this[unfolded t] have "x ∈ vars_term (l ⋅ τ)" using vars unfolding vars_term_subst by auto
then show "x ∈ vars_term s" unfolding s by auto
qed
qed
lemma instance_rule_rstep: assumes step: "(s,t) ∈ rstep {lr}"
and bex: "Bex R (instance_rule lr)"
shows "(s,t) ∈ rstep R"
proof -
from bex obtain lr' where inst: "instance_rule lr lr'" and R: "lr' ∈ R" by auto
obtain l r where lr: "lr = (l,r)" by force
obtain l' r' where lr': "lr' = (l',r')" by force
note inst = inst[unfolded lr lr']
note R = R[unfolded lr']
from inst[unfolded instance_rule_def] obtain σ where l: "l = l' ⋅ σ" and r: "r = r' ⋅ σ" by auto
from step[unfolded lr] obtain C τ where "s = C ⟨l ⋅ τ⟩" "t = C ⟨r ⋅ τ⟩" by auto
with l r have s: "s = C⟨l' ⋅ (σ ∘⇩s τ)⟩" and t: "t = C⟨r' ⋅ (σ ∘⇩s τ)⟩" by auto
from rstepI[OF R s t] show ?thesis .
qed
lemma eq_rule_mod_vars_var_cond: assumes eq: "(l,r) =⇩v (s,t)"
and vars: "vars_term r ⊆ vars_term l"
shows "vars_term t ⊆ vars_term s"
by (rule instance_rule_var_cond[OF _ vars], insert eq[unfolded eq_rule_mod_vars_def], auto)
lemma eq_rule_mod_varsE[elim]: assumes "(l,r) =⇩v (s,t)"
shows "∃ σ τ. l = s ⋅ σ ∧ r = t ⋅ σ ∧ s = l ⋅ τ ∧ t = r ⋅ τ ∧ range σ ⊆ range Var ∧ range τ ⊆ range Var"
proof -
from assms[unfolded eq_rule_mod_vars_def instance_rule_def fst_conv snd_conv]
obtain σ τ where l: "l = s ⋅ σ" and r: "r = t ⋅ σ" and s: "s = l ⋅ τ" and t: "t = r ⋅ τ" by blast+
let ?vst = "vars_term (Fun f [s,t])"
let ?vlr = "vars_term (Fun f [l,r])"
define σ' where "σ' ≡ λ x. if x ∈ ?vst then σ x else Var x"
define τ' where "τ' ≡ λ x. if x ∈ ?vlr then τ x else Var x"
show ?thesis
proof (intro exI conjI)
show l: "l = s ⋅ σ'" unfolding l σ'_def
by (rule term_subst_eq, auto)
show r: "r = t ⋅ σ'" unfolding r σ'_def
by (rule term_subst_eq, auto)
show s: "s = l ⋅ τ'" unfolding s τ'_def
by (rule term_subst_eq, auto)
show t: "t = r ⋅ τ'" unfolding t τ'_def
by (rule term_subst_eq, auto)
have "Fun f [s,t] ⋅ Var = Fun f [l, r] ⋅ τ'" unfolding s t by simp
also have "… = Fun f [s,t] ⋅ (σ' ∘⇩s τ')" unfolding l r by simp
finally have "Fun f [s,t] ⋅ (σ' ∘⇩s τ') = Fun f [s,t] ⋅ Var" by simp
from term_subst_eq_rev[OF this] have vst: "⋀ x. x ∈ ?vst ⟹ σ' x ⋅ τ' = Var x" unfolding subst_compose_def by auto
have "Fun f [l,r] ⋅ Var = Fun f [s, t] ⋅ σ'" unfolding l r by simp
also have "… = Fun f [l,r] ⋅ (τ' ∘⇩s σ')" unfolding s t by simp
finally have "Fun f [l,r] ⋅ (τ' ∘⇩s σ') = Fun f [l,r] ⋅ Var" by simp
from term_subst_eq_rev[OF this] have vlr: "⋀ x. x ∈ ?vlr ⟹ τ' x ⋅ σ' = Var x" unfolding subst_compose_def by auto
{
fix x
have "σ' x ∈ range Var"
proof (cases "x ∈ ?vst")
case True
from vst[OF this] show ?thesis by (cases "σ' x", auto)
next
case False
then show ?thesis unfolding σ'_def by auto
qed
}
then show "range σ' ⊆ range Var" by auto
{
fix x
have "τ' x ∈ range Var"
proof (cases "x ∈ ?vlr")
case True
from vlr[OF this] show ?thesis by (cases "τ' x", auto)
next
case False
then show ?thesis unfolding τ'_def by auto
qed
}
then show "range τ' ⊆ range Var" by auto
qed
qed
definition
linear_trs :: "('f, 'v) trs ⇒ bool"
where
"linear_trs R ≡ ∀(l, r)∈R. linear_term l ∧ linear_term r"
lemma linear_trsE[elim,consumes 1]: "linear_trs R ⟹ (l,r) ∈ R ⟹ linear_term l ∧ linear_term r"
unfolding linear_trs_def by auto
lemma linear_trsI[intro]: "⟦ ⋀ l r. (l,r) ∈ R ⟹ linear_term l ∧ linear_term r⟧ ⟹ linear_trs R"
unfolding linear_trs_def by auto
definition
left_linear_trs :: "('f, 'v) trs ⇒ bool"
where
"left_linear_trs R ⟷ (∀(l, r)∈R. linear_term l)"
lemma left_linear_trs_union: "left_linear_trs (R ∪ S) = (left_linear_trs R ∧ left_linear_trs S)"
unfolding left_linear_trs_def by auto
lemma left_linear_mono: assumes "left_linear_trs S" and "R ⊆ S" shows "left_linear_trs R"
using assms unfolding left_linear_trs_def by auto
lemma left_linear_map_funs_trs[simp]: "left_linear_trs (map_funs_trs f R) = left_linear_trs R"
unfolding left_linear_trs_def by (auto simp: map_funs_trs.simps)
lemma left_linear_weak_match_rstep:
assumes rstep: "(u, v) ∈ rstep R"
and weak_match: "weak_match s u"
and ll: "left_linear_trs R"
shows "∃t. (s, t) ∈ rstep R ∧ weak_match t v"
using weak_match
proof (induct rule: rstep_induct_rule [OF rstep])
case (1 C sig l r)
from 1(2) show ?case
proof (induct C arbitrary: s)
case (More f bef C aft s)
let ?n = "Suc (length bef + length aft)"
let ?m = "length bef"
from More(2) obtain ss where s: "s = Fun f ss" and lss: "?n = length ss" and wm: "(∀i<length ss. weak_match (ss ! i) ((bef @ C⟨l ⋅ sig⟩ # aft) ! i))" by (cases s, auto)
from lss wm[THEN spec, of ?m] have "weak_match (ss ! ?m) C⟨l ⋅ sig⟩" by auto
from More(1)[OF this] obtain t where wmt: "weak_match t C⟨r ⋅ sig⟩" and step: "(ss ! ?m,t) ∈ rstep R" by auto
from lss have mss: "?m < length ss" by simp
let ?tsi = "λ t. take ?m ss @ t # drop (Suc ?m) ss"
let ?ts = "?tsi t"
let ?ss = "?tsi (ss ! ?m)"
from id_take_nth_drop[OF mss]
have lts: "length ?ts = ?n" using lss by auto
show ?case
proof (rule exI[of _ "Fun f ?ts"], intro conjI)
have "weak_match (Fun f ?ts) (More f bef C aft)⟨r ⋅ sig⟩ =
weak_match (Fun f ?ts) (Fun f (bef @ C⟨r ⋅ sig⟩ # aft))" by simp
also have "… = True" proof (simp only: weak_match.simps lts, simp, intro allI impI)
fix i
assume i: "i < ?n"
show "weak_match (?ts ! i) ((bef @ C⟨r ⋅ sig⟩ # aft) ! i)"
proof (cases "i = ?m")
case True
have "weak_match (?ts ! i) ((bef @ C⟨r ⋅ sig⟩ # aft) ! i) = weak_match t C⟨r ⋅ sig⟩"
using True mss by (simp add: nth_append)
then show ?thesis using wmt by simp
next
case False
have eq: "?ts ! i = ss ! i ∧ (bef @ C⟨r ⋅ sig⟩ # aft) ! i = (bef @ C⟨l ⋅ sig⟩ # aft) ! i"
proof (cases "i < ?m")
case True
then show ?thesis by (simp add: nth_append lss[symmetric])
next
case False
with ‹i ≠ ?m› i have "∃ j. i = Suc (?m + j) ∧ j < length aft" by presburger
then obtain j where i: "i = Suc (?m + j)" and j: "j < length aft" by auto
then have id: " (Suc (length bef + j) - min (Suc (length bef + length aft)) (length bef)) = Suc j" by simp
from j show ?thesis by (simp add: nth_append i id lss[symmetric])
qed
then show ?thesis using wm[THEN spec, of i] i[unfolded lss] by (simp)
qed
qed
finally show "weak_match (Fun f ?ts) (More f bef C aft)⟨r ⋅ sig⟩" by simp
next
have "s = Fun f ?ss" unfolding s using id_take_nth_drop[OF mss, symmetric] by simp
also have "… = (More f (take ?m ss) □ (drop (Suc ?m) ss))⟨(ss ! ?m)⟩" (is "_ = ?C⟨_⟩") by simp
finally have s: "s = ?C⟨ss ! ?m⟩" .
have t: "Fun f ?ts = ?C⟨t⟩" by simp
from rstep_ctxt[OF step]
show "(s, Fun f ?ts) ∈ rstep R"
unfolding s t .
qed
next
case (Hole s)
from ll 1(1) have "linear_term l" unfolding left_linear_trs_def by auto
from linear_weak_match[OF this Hole[simplified] refl] obtain τ where
"s = l ⋅ τ" and "(∀ x ∈ vars_term l . weak_match (Var x ⋅ τ) (Var x ⋅ sig))"
by auto
then obtain tau where s: "s = l ⋅ tau" and wm: "(∀ x ∈ vars_term l . weak_match (tau x) (Var x ⋅ sig))"
by (auto)
let ?delta = "(λ x. if x ∈ vars_term l then tau x else Var x ⋅ sig)"
show ?case
proof (rule exI[of _ "r ⋅ ?delta"], rule conjI)
have "s = l ⋅ (tau |s (vars_term l))" unfolding s by (rule coincidence_lemma)
also have "… = l ⋅ (?delta |s (vars_term l))" by simp
also have "… = l ⋅ ?delta" by (rule coincidence_lemma[symmetric])
finally have s: "s = l ⋅ ?delta" .
from 1(1) have step: "(l ⋅ ?delta, r ⋅ ?delta) ∈ rstep R" by auto
then show "(s, r ⋅ ?delta) ∈ rstep R" unfolding s .
next
have "weak_match (r ⋅ ?delta) (r ⋅ sig)"
proof (induct r)
case (Fun f ss)
from this[unfolded set_conv_nth]
show ?case by (force)
next
case (Var x)
show ?case
proof (cases "x ∈ vars_term l")
case True
with wm Var show ?thesis by simp
next
case False
show ?thesis by (simp add: Var False weak_match_refl)
qed
qed
then show "weak_match (r ⋅ ?delta) (□ ⟨(r ⋅ sig)⟩)" by simp
qed
qed
qed
context
begin
private fun S where
"S R s t 0 = s"
| "S R s t (Suc i) = (SOME u. (S R s t i,u) ∈ rstep R ∧ weak_match u (t(Suc i)))"
lemma weak_match_SN:
assumes wm: "weak_match s t"
and ll: "left_linear_trs R"
and SN: "SN_on (rstep R) {s}"
shows "SN_on (rstep R) {t}"
proof
fix f
assume t0: "f 0 ∈ {t}" and chain: "chain (rstep R) f"
let ?s = "S R s f"
let ?P = "λi u. (?s i, u) ∈ rstep R ∧ weak_match u (f (Suc i))"
have "∀i. (?s i, ?s (Suc i)) ∈ rstep R ∧ weak_match (?s (Suc i)) (f (Suc i))"
proof
fix i show "(?s i, ?s (Suc i)) ∈ rstep R ∧ weak_match (?s (Suc i)) (f (Suc i))"
proof (induct i)
case 0
from chain have ini: "(f 0, f (Suc 0)) ∈ rstep R" by simp
then have "(t, f (Suc 0)) ∈ rstep R" unfolding singletonD[OF t0, symmetric] .
from someI_ex[OF left_linear_weak_match_rstep[OF this wm ll]]
show ?case by simp
next
case (Suc i)
then have IH1: "(?s i, ?s (Suc i)) ∈ rstep R"
and IH2: "weak_match (?s (Suc i)) (f (Suc i))" by auto
from chain have nxt: "(f (Suc i), f (Suc (Suc i))) ∈ rstep R" by simp
from someI_ex[OF left_linear_weak_match_rstep[OF this IH2 ll]]
have "∃u. ?P (Suc i) u" by auto
from someI_ex[OF this]
show ?case by simp
qed
qed
moreover have "?s 0 = s" by simp
ultimately have "¬ SN_on (rstep R) {s}" by best
with SN show False by simp
qed
end
lemma lhs_notin_NF_rstep: "(l, r) ∈ R ⟹ l ∉ NF (rstep R)" by auto
lemma NF_instance:
assumes "(t ⋅ σ) ∈ NF (rstep R)" shows "t ∈ NF (rstep R)"
using assms by auto
lemma NF_subterm:
assumes "t ∈ NF (rstep R)" and "t ⊵ s"
shows "s ∈ NF (rstep R)"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain u where "(s, u) ∈ rstep R" by auto
from ‹t ⊵ s› obtain C where "t = C⟨s⟩" by auto
with ‹(s, u) ∈ rstep R› have "(t, C⟨u⟩) ∈ rstep R" by auto
then have "t ∉ NF (rstep R)" by auto
with assms show False by simp
qed
abbreviation
lhss :: "('f, 'v) trs ⇒ ('f, 'v) terms"
where
"lhss R ≡ fst ` R"
abbreviation
rhss :: "('f, 'v) trs ⇒ ('f, 'v) terms"
where
"rhss R ≡ snd ` R"
definition map_funs_trs_wa :: "('f × nat ⇒ 'g) ⇒ ('f, 'v) trs ⇒ ('g, 'v) trs" where
"map_funs_trs_wa fg R = (λ(l, r). (map_funs_term_wa fg l, map_funs_term_wa fg r)) ` R"
lemma map_funs_trs_wa_union: "map_funs_trs_wa fg (R ∪ S) = map_funs_trs_wa fg R ∪ map_funs_trs_wa fg S"
unfolding map_funs_trs_wa_def by auto
lemma map_funs_term_wa_compose: "map_funs_term_wa gh (map_funs_term_wa fg t) = map_funs_term_wa (λ (f,n). gh (fg (f,n), n)) t"
by (induct t, auto)
lemma map_funs_trs_wa_compose: "map_funs_trs_wa gh (map_funs_trs_wa fg R) = map_funs_trs_wa (λ (f,n). gh (fg (f,n), n)) R" (is "?L = map_funs_trs_wa ?fgh R")
proof -
have "map_funs_trs_wa ?fgh R = {(map_funs_term_wa ?fgh l, map_funs_term_wa ?fgh r)| l r. (l,r) ∈ R}" unfolding map_funs_trs_wa_def by auto
also have "… = {(map_funs_term_wa gh (map_funs_term_wa fg l), map_funs_term_wa gh (map_funs_term_wa fg r)) | l r. (l,r) ∈ R}" unfolding map_funs_term_wa_compose ..
finally show ?thesis unfolding map_funs_trs_wa_def by force
qed
lemma map_funs_trs_wa_funas_trs_id: assumes R: "funas_trs R ⊆ F"
and id: "⋀ g n. (g,n) ∈ F ⟹ f (g,n) = g"
shows "map_funs_trs_wa f R = R"
proof -
{
fix l r
assume "(l,r) ∈ R"
with R have l: "funas_term l ⊆ F" and r: "funas_term r ⊆ F" unfolding funas_trs_def
by (force simp: funas_rule_def)+
from map_funs_term_wa_funas_term_id[OF l id] map_funs_term_wa_funas_term_id[OF r id]
have "map_funs_term_wa f l = l" "map_funs_term_wa f r = r" by auto
} note main = this
have "map_funs_trs_wa f R = {(map_funs_term_wa f l, map_funs_term_wa f r) | l r. (l,r) ∈ R}"
unfolding map_funs_trs_wa_def by force
also have "… = R" using main by force
finally show ?thesis .
qed
lemma map_funs_trs_wa_rstep: assumes step:"(s,t) ∈ rstep R"
shows "(map_funs_term_wa fg s,map_funs_term_wa fg t) ∈ rstep (map_funs_trs_wa fg R)"
using step
proof (induct)
case (IH C σ l r)
show ?case unfolding map_funs_trs_wa_def
by (rule rstepI[where l = "map_funs_term_wa fg l" and r = "map_funs_term_wa fg r" and C = "map_funs_ctxt_wa fg C"], auto simp: IH)
qed
lemma map_funs_trs_wa_rsteps: assumes step:"(s,t) ∈ (rstep R)⇧*"
shows "(map_funs_term_wa fg s,map_funs_term_wa fg t) ∈ (rstep (map_funs_trs_wa fg R))⇧*"
using step
proof (induct)
case (step a b)
from map_funs_trs_wa_rstep[OF step(2), of fg] step(3) show ?case by auto
qed auto
lemma rstep_ground:
assumes wf_trs: "⋀l r. (l, r) ∈ R ⟹ vars_term r ⊆ vars_term l"
and ground: "ground s"
and step: "(s, t) ∈ rstep R"
shows "ground t"
using step ground
proof (induct)
case (IH C σ l r)
from wf_trs[OF IH(1)] IH(2)
show ?case by auto
qed
lemma rsteps_ground:
assumes wf_trs: "⋀l r. (l, r) ∈ R ⟹ vars_term r ⊆ vars_term l"
and ground: "ground s"
and steps: "(s, t) ∈ (rstep R)⇧*"
shows "ground t"
using steps ground
by (induct, insert rstep_ground[OF wf_trs], auto)
definition locally_terminating :: "('f,'v)trs ⇒ bool"
where "locally_terminating R ≡ ∀ F. finite F ⟶ SN (sig_step F (rstep R))"
lemma supt_rstep_stable:
assumes "(s, t) ∈ {⊳} ∪ rstep R"
shows "(s ⋅ σ, t ⋅ σ) ∈ {⊳} ∪ rstep R"
using assms proof
assume "s ⊳ t" show ?thesis
proof (rule UnI1)
from ‹s ⊳ t› show "s ⋅ σ ⊳ t ⋅ σ" by (rule supt_subst)
qed
next
assume "(s, t) ∈ rstep R" show ?thesis
proof (rule UnI2)
from ‹(s, t) ∈ rstep R› show "(s ⋅ σ, t ⋅ σ) ∈ rstep R" ..
qed
qed
lemma supt_rstep_trancl_stable:
assumes "(s, t) ∈ ({⊳} ∪ rstep R)⇧+"
shows "(s ⋅ σ, t ⋅ σ) ∈ ({⊳} ∪ rstep R)⇧+"
using assms proof (induct)
case (base u)
then have "(s ⋅ σ, u ⋅ σ) ∈ {⊳} ∪ rstep R" by (rule supt_rstep_stable)
then show ?case ..
next
case (step u v)
from ‹(s ⋅ σ, u ⋅ σ) ∈ ({⊳} ∪ rstep R)⇧+›
and supt_rstep_stable[OF ‹(u, v) ∈ {⊳} ∪ rstep R›, of "σ"]
show ?case ..
qed
lemma supt_rsteps_stable:
assumes "(s, t) ∈ ({⊳} ∪ rstep R)⇧*"
shows "(s ⋅ σ, t ⋅ σ) ∈ ({⊳} ∪ rstep R)⇧*"
using assms
proof (induct)
case base then show ?case ..
next
case (step u v)
from ‹(s, u) ∈ ({⊳} ∪ rstep R)⇧*› and ‹(u, v) ∈ {⊳} ∪ rstep R›
have "(s, v) ∈ ({⊳} ∪ rstep R)⇧+" by (rule rtrancl_into_trancl1)
from trancl_into_rtrancl[OF supt_rstep_trancl_stable[OF this]]
show ?case .
qed
lemma eq_rule_mod_vars_refl[simp]: "r =⇩v r"
proof (cases r)
case (Pair l r)
{
have "fst (l, r) = fst (l, r) ⋅ Var ∧ snd (l, r) = snd (l, r) ⋅ Var" by auto
}
then show ?thesis unfolding Pair eq_rule_mod_vars_def instance_rule_def by best
qed
lemma instance_rule_refl[simp]: "instance_rule r r"
using eq_rule_mod_vars_refl[of r] unfolding eq_rule_mod_vars_def by simp
lemma is_Fun_Fun_conv: "is_Fun t = (∃f ts. t = Fun f ts)" by auto
lemma wf_trs_def':
"wf_trs R = (∀(l, r)∈R. is_Fun l ∧ vars_term r ⊆ vars_term l)"
by (rule iffI) (auto simp: wf_trs_def is_Fun_Fun_conv)
definition wf_rule :: "('f, 'v) rule ⇒ bool" where
"wf_rule r ⟷ is_Fun (fst r) ∧ vars_term (snd r) ⊆ vars_term (fst r)"
definition wf_rules :: "('f, 'v) trs ⇒ ('f, 'v) trs" where
"wf_rules R = {r. r ∈ R ∧ wf_rule r}"
lemma wf_trs_wf_rules[simp]: "wf_trs (wf_rules R)"
unfolding wf_trs_def' wf_rules_def wf_rule_def split_def by simp
lemma wf_rules_subset[simp]: "wf_rules R ⊆ R"
unfolding wf_rules_def by auto
fun wf_reltrs :: "('f, 'v) trs ⇒ ('f, 'v) trs ⇒ bool" where
"wf_reltrs R S = (
wf_trs R ∧ (R ≠ {} ⟶ (∀l r. (l, r) ∈ S ⟶ vars_term r ⊆ vars_term l)))"
lemma SN_rel_imp_wf_reltrs:
assumes SN_rel: "SN_rel (rstep R) (rstep S)"
shows "wf_reltrs R S"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain l r where "¬ wf_trs R ∨ R ≠ {} ∧ (l,r) ∈ S ∧ ¬ vars_term r ⊆ vars_term l" (is "_ ∨ ?two") by auto
then show False
proof
assume "¬ wf_trs R"
with SN_rstep_imp_wf_trs[OF SN_rel_imp_SN[OF assms]]
show False by simp
next
assume ?two
then obtain ll rr x where lr: "(l,r) ∈ S" and llrr: "(ll,rr) ∈ R" and x: "x ∈ vars_term r" and nx: "x ∉ vars_term l" by auto
obtain f and σ
where sigma: "σ = (λy. if x = y then Fun f [ll,l] else Var y)" by auto
have id: "σ |s (vars_term l) = Var" unfolding sigma
by (simp add: subst_restrict_def, rule ext, auto simp: nx)
have l: "l = l ⋅ σ" by (simp add: coincidence_lemma[of l σ] id)
have "(l ⋅ σ, r ⋅ σ) ∈ rstep S" using lr by auto
with l have sstep: "(l, r ⋅ σ) ∈ rstep S" by simp
from supteq_subst[OF supteq_Var[OF x], of σ] have
"r ⋅ σ ⊵ Fun f [ll,l]" unfolding sigma by auto
then obtain C where "C⟨Fun f [ll, l]⟩ = r ⋅ σ" by auto
with sstep have sstep: "(l,C⟨Fun f [ll, l]⟩) ∈ rstep S" by simp
obtain r where r: "r = relto (rstep R) (rstep S) ∪ {⊳}" by auto
have "(C⟨Fun f [ll,l]⟩, C⟨Fun f [rr,l]⟩) ∈ rstep R"
unfolding rstep_iff_rstep_r_c_s
by (rule exI, rule exI, rule exI[of _ "C ∘⇩c More f [] □ [l]"], rule exI[of _ Var], intro conjI, rule llrr, unfold rstep_r_c_s_def, simp)
with sstep have relto: "(l,C⟨Fun f [rr,l]⟩) ∈ r" unfolding r by auto
have "C⟨Fun f [rr,l]⟩ ⊵ Fun f [rr,l]" using ctxt_imp_supteq by auto
also have "Fun f [rr,l] ⊳ l" by auto
finally have supt: "C⟨Fun f [rr,l]⟩ ⊳ l" unfolding supt_def by simp
then have "(C⟨Fun f [rr,l]⟩, l) ∈ r" unfolding r by auto
with relto have loop: "(l, l) ∈ r⇧+" by auto
have "SN r" unfolding r
by (rule SN_imp_SN_union_supt[OF SN_rel[unfolded SN_rel_defs]], blast)
then have "SN (r⇧+)" by (rule SN_imp_SN_trancl)
with loop show False unfolding SN_on_def by auto
qed
qed
lemmas rstep_wf_rules_subset = rstep_mono[OF wf_rules_subset]
definition map_vars_trs :: "('v ⇒ 'w) ⇒ ('f, 'v) trs ⇒ ('f, 'w) trs" where
"map_vars_trs f R = (λ (l, r). (map_vars_term f l, map_vars_term f r)) ` R"
lemma map_vars_trs_rstep:
assumes "(s, t) ∈ rstep (map_vars_trs f R)" (is "_ ∈ rstep ?R")
shows "(s ⋅ τ, t ⋅ τ) ∈ rstep R"
using assms
proof
fix ml mr C σ
presume mem: "(ml,mr) ∈ ?R" and s: "s = C⟨ml ⋅ σ⟩" and t: "t = C⟨mr ⋅ σ⟩"
let ?m = "map_vars_term f"
from mem obtain l r where mem: "(l,r) ∈ R" and id: "ml = ?m l" "mr = ?m r"
unfolding map_vars_trs_def by auto
have id: "s ⋅ τ = (C ⋅⇩c τ)⟨?m l ⋅ σ ∘⇩s τ⟩" "t ⋅ τ = (C ⋅⇩c τ)⟨?m r ⋅ σ ∘⇩s τ⟩" by (auto simp: s t id)
then show "(s ⋅ τ, t ⋅ τ) ∈ rstep R"
unfolding id apply_subst_map_vars_term
using mem by auto
qed auto
lemma map_vars_rsteps:
assumes "(s,t) ∈ (rstep (map_vars_trs f R))⇧*" (is "_ ∈ (rstep ?R)⇧*")
shows "(s ⋅ τ, t ⋅ τ) ∈ (rstep R)⇧*"
using assms
proof (induct)
case base then show ?case by simp
next
case (step t u)
from map_vars_trs_rstep[OF step(2), of τ] step(3) show ?case by auto
qed
lemma rsteps_subst_closed: "(s,t) ∈ (rstep R)⇧+ ⟹ (s ⋅ σ, t ⋅ σ) ∈ (rstep R)⇧+"
proof -
let ?R = "rstep R"
assume steps: "(s,t) ∈ ?R⇧+"
have subst: "subst.closed (?R⇧+)" by (rule subst.closed_trancl[OF subst_closed_rstep])
from this[unfolded subst.closed_def] steps show ?thesis by auto
qed
lemma supteq_rtrancl_supt:
"(R⇧+ O {⊵}) ⊆ ({⊳} ∪ R)⇧+" (is "?l ⊆ ?r")
proof
fix x z
assume "(x,z) ∈ ?l"
then obtain y where xy: "(x,y) ∈ R⇧+" and yz: "y ⊵ z" by auto
from xy have xy: "(x,y) ∈ ?r" by (rule trancl_mono, simp)
show "(x,z) ∈ ?r"
proof (cases "y = z")
case True
with xy show ?thesis by simp
next
case False
with yz have yz: "(y,z) ∈ {⊳} ∪ R" by auto
with xy have xz: "(x,z) ∈ ?r O ({⊳} ∪ R)" by auto
then show ?thesis by (metis UnCI trancl_unfold)
qed
qed
lemma rrstepI[intro]: "(l, r) ∈ R ⟹ s = l ⋅ σ ⟹ t = r ⋅ σ ⟹ (s, t) ∈ rrstep R"
unfolding rrstep_def' by auto
lemma CS_rrstep_conv: "subst.closure = rrstep"
by (intro ext, unfold rrstep_def', rule, insert subst.closure.cases, blast, auto)
subsection ‹Rewrite steps at a fixed position›
inductive_set rstep_pos :: "('f, 'v) trs ⇒ pos ⇒ ('f, 'v) term rel" for R and p
where
rule [intro]:"(l, r) ∈ R ⟹ p ∈ poss s ⟹ s |_ p = l ⋅ σ ⟹
(s, replace_at s p (r ⋅ σ)) ∈ rstep_pos R p"
lemma rstep_pos_subst:
assumes "(s, t) ∈ rstep_pos R p"
shows "(s ⋅ σ, t ⋅ σ) ∈ rstep_pos R p"
using assms
proof (cases)
case (rule l r σ')
with rstep_pos.intros [OF this(2), of p "s ⋅ σ" "σ' ∘⇩s σ"]
show ?thesis by (auto simp: ctxt_of_pos_term_subst)
qed
lemma rstep_pos_rule:
assumes "(l, r) ∈ R"
shows "(l, r) ∈ rstep_pos R []"
using rstep_pos.intros [OF assms, of "[]" l Var] by simp
lemma rstep_pos_rstep_r_p_s_conv:
"rstep_pos R p = {(s, t) | s t r σ. (s, t) ∈ rstep_r_p_s R r p σ}"
by (auto simp: rstep_r_p_s_def Let_def subt_at_ctxt_of_pos_term
intro: replace_at_ident
elim!: rstep_pos.cases)
lemma rstep_rstep_pos_conv:
"rstep R = {(s, t) | s t p. (s, t) ∈ rstep_pos R p}"
by (force simp: rstep_pos_rstep_r_p_s_conv rstep_iff_rstep_r_p_s)
lemma rstep_pos_supt:
assumes "(s, t) ∈ rstep_pos R p"
and q: "q ∈ poss u" and u: "u |_ q = s"
shows "(u, (ctxt_of_pos_term q u)⟨t⟩) ∈ rstep_pos R (q @ p)"
using assms
proof (cases)
case (rule l r σ)
with q and u have "(q @ p) ∈ poss u" and "u |_ (q @ p) = l ⋅ σ" by auto
with rstep_pos.rule [OF rule(2) this] show ?thesis
unfolding rule by (auto simp: ctxt_of_pos_term_append u)
qed
lemma rrstep_rstep_pos_conv:
"rrstep R = rstep_pos R []"
by (auto simp: rrstep_def rstep_pos_rstep_r_p_s_conv)
lemma rrstep_imp_rstep:
assumes "(s, t) ∈ rrstep R"
shows "(s, t) ∈ rstep R"
using assms by (auto simp: rrstep_def rstep_iff_rstep_r_p_s)
lemma not_NF_rstep_imp_subteq_not_NF_rrstep:
assumes "s ∉ NF (rstep R)"
shows "∃t ⊴ s. t ∉ NF (rrstep R)"
proof -
from assms obtain u where "(s, u) ∈ rstep R" by auto
then obtain l r C σ where "(l, r) ∈ R" and s: "s = C⟨l ⋅ σ⟩" and u: "u = C⟨r ⋅ σ⟩" by auto
then have "(l ⋅ σ, r ⋅ σ) ∈ rrstep R" and "l ⋅ σ ⊴ s" by auto
then show ?thesis by blast
qed
lemma all_subt_NF_rrstep_iff_all_subt_NF_rstep:
"(∀s ⊲ t. s ∈ NF (rrstep R)) ⟷ (∀s ⊲ t. s ∈ NF (rstep R))"
by (auto dest: rrstep_imp_rstep supt_supteq_trans not_NF_rstep_imp_subteq_not_NF_rrstep)
lemma not_in_poss_imp_NF_rstep_pos [simp]:
assumes "p ∉ poss s"
shows "s ∈ NF (rstep_pos R p)"
using assms by (auto simp: NF_def elim: rstep_pos.cases)
lemma Var_rstep_imp_rstep_pos_Empty:
assumes "(Var x, t) ∈ rstep R"
shows "(Var x, t) ∈ rstep_pos R []"
using assms by (metis Var_supt nrrstep_subt rrstep_rstep_pos_conv rstep_cases)
lemma rstep_args_NF_imp_rrstep:
assumes "(s, t) ∈ rstep R"
and "∀u ⊲ s. u ∈ NF (rstep R)"
shows "(s, t) ∈ rrstep R"
using assms by (metis NF_iff_no_step nrrstep_subt rstep_cases)
lemma rstep_pos_imp_rstep_pos_Empty:
assumes "(s, t) ∈ rstep_pos R p"
shows "(s |_ p, t |_ p) ∈ rstep_pos R []"
using assms by (cases) (auto simp: replace_at_subt_at intro: rstep_pos_rule rstep_pos_subst)
lemma rstep_pos_arg:
assumes "(s, t) ∈ rstep_pos R p"
and "i < length ss" and "ss ! i = s"
shows "(Fun f ss, (ctxt_of_pos_term [i] (Fun f ss))⟨t⟩) ∈ rstep_pos R (i # p)"
using assms
apply (cases)
apply (auto)
by (metis term.sel(4) ctxt_apply_term.simps(2) ctxt_of_pos_term.simps(2) poss_Cons_poss rstep_pos.intros subt_at.simps(2))
lemma rstep_imp_max_pos:
assumes "(s, t) ∈ rstep R"
shows "∃u. ∃p∈poss s. (s, u) ∈ rstep_pos R p ∧ (∀v ⊲ s |_ p. v ∈ NF (rstep R))"
using assms
proof (induction s arbitrary: t)
case (Var x)
from Var_rstep_imp_rstep_pos_Empty [OF this] show ?case by auto
next
case (Fun f ss)
show ?case
proof (cases "∀v ⊲ Fun f ss |_ []. v ∈ NF (rstep R)")
case True
moreover with Fun.prems
have "(Fun f ss, t) ∈ rstep_pos R []"
by (auto dest: rstep_args_NF_imp_rrstep simp: rrstep_rstep_pos_conv)
ultimately show ?thesis by auto
next
case False
then obtain v where "v ⊲ Fun f ss" and "v ∉ NF (rstep R)" by auto
then obtain s and w where "s ∈ set ss" and "s ⊵ v" and "(s, w) ∈ rstep R"
by (auto simp: NF_def) (metis NF_iff_no_step NF_subterm supt_Fun_imp_arg_supteq)
from Fun.IH [OF this(1, 3)] obtain u and p
where "p ∈ poss s" and *: "(s, u) ∈ rstep_pos R p"
and **: "∀v ⊲ s |_ p. v ∈ NF (rstep R)" by blast
from ‹s ∈ set ss› obtain i
where "i < length ss" and [simp]:"ss ! i = s" by (auto simp: in_set_conv_nth)
with ‹p ∈ poss s› have "i # p ∈ poss (Fun f ss)" by auto
moreover with ** have "∀v ⊲ Fun f ss |_ (i # p). v ∈ NF (rstep R)" by auto
moreover from rstep_pos_arg [OF * ‹i < length ss› ‹ss ! i = s›]
have "(Fun f ss, (ctxt_of_pos_term [i] (Fun f ss))⟨u⟩) ∈ rstep_pos R (i # p)" .
ultimately show ?thesis by blast
qed
qed
lemma rhs_free_vars_imp_rstep_not_SN':
assumes "(l, r) ∈ R" and "¬ vars_term r ⊆ vars_term l"
shows "¬ SN (rstep R)"
using rhs_free_vars_imp_rstep_not_SN [OF assms] by (auto simp: SN_defs)
lemma SN_imp_variable_condition:
assumes "SN (rstep R)"
shows "∀(l, r) ∈ R. vars_term r ⊆ vars_term l"
using assms and rhs_free_vars_imp_rstep_not_SN' [of _ _ R] by blast
definition "non_collapsing R ⟷ (∀ lr ∈ R. is_Fun (snd lr))"
subsection ‹Parallel rewrite relation›
text ‹the parallel rewrite relation›
inductive_set par_rstep :: "('f,'v)trs ⇒ ('f,'v)trs" for R :: "('f,'v)trs"
where root_step[intro]: "(s,t) ∈ R ⟹ (s ⋅ σ,t ⋅ σ) ∈ par_rstep R"
| par_step_fun[intro]: "⟦⋀ i. i < length ts ⟹ (ss ! i,ts ! i) ∈ par_rstep R⟧ ⟹ length ss = length ts
⟹ (Fun f ss, Fun f ts) ∈ par_rstep R"
| par_step_var[intro]: "(Var x, Var x) ∈ par_rstep R"
lemma par_rstep_refl[intro]: "(t,t) ∈ par_rstep R"
by (induct t, auto)
lemma all_ctxt_closed_par_rstep[intro]: "all_ctxt_closed F (par_rstep R)"
unfolding all_ctxt_closed_def
by auto
lemma args_par_rstep_pow_imp_par_rstep_pow:
"length xs = length ys ⟹ ∀i<length xs. (xs ! i, ys ! i) ∈ par_rstep R ^^ n ⟹
(Fun f xs, Fun f ys) ∈ par_rstep R ^^ n"
proof(induct n arbitrary:ys)
case 0
then have "∀i<length xs. (xs ! i = ys ! i)" by simp
with 0 show ?case using relpow_0_I list_eq_iff_nth_eq by metis
next
case (Suc n)
let ?c = "λ z i. (xs ! i, z) ∈ par_rstep R ^^ n ∧ (z, ys ! i) ∈ par_rstep R"
{ fix i assume "i < length xs"
from relpow_Suc_E[OF Suc(3)[rule_format, OF this]]
have "∃ z. (?c z i)" by metis
}
with choice have "∃ zf. ∀ i < length xs. (?c (zf i) i)" by meson
then obtain zf where a:"∀ i < length xs. (?c (zf i) i)" by auto
let ?zs = "map zf [0..<length xs]"
have len:"length xs = length ?zs" by simp
from a map_nth have "∀i<length xs. (xs ! i, ?zs ! i) ∈ par_rstep R ^^ n" by auto
from Suc(1)[OF len this] have n:"(Fun f xs, Fun f ?zs) ∈ par_rstep R ^^ n" by auto
from a map_nth have "∀i<length xs. (?zs ! i, ys ! i) ∈ par_rstep R" by auto
with par_step_fun len Suc(2) have "(Fun f ?zs, Fun f ys) ∈ par_rstep R" by auto
with n show ?case by auto
qed
lemma ctxt_closed_par_rstep[intro]: "ctxt.closed (par_rstep R)"
proof (rule one_imp_ctxt_closed)
fix f bef s t aft
assume st: "(s,t) ∈ par_rstep R"
let ?ss = "bef @ s # aft"
let ?ts = "bef @ t # aft"
show "(Fun f ?ss, Fun f ?ts) ∈ par_rstep R"
proof (rule par_step_fun)
fix i
assume "i < length ?ts"
show "(?ss ! i, ?ts ! i) ∈ par_rstep R"
using par_rstep_refl[of "?ts ! i" R] st by (cases "i = length bef", auto simp: nth_append)
qed simp
qed
lemma subst_closed_par_rstep: "(s,t) ∈ par_rstep R ⟹ (s ⋅ σ, t ⋅ σ) ∈ par_rstep R"
proof (induct rule: par_rstep.induct)
case (root_step s t τ)
show ?case
using par_rstep.root_step[OF root_step, of "τ ∘⇩s σ"] by auto
next
case (par_step_var x)
show ?case by auto
next
case (par_step_fun ss ts f)
show ?case unfolding subst_apply_term.simps
by (rule par_rstep.par_step_fun, insert par_step_fun(2-3), auto)
qed
lemma R_par_rstep: "R ⊆ par_rstep R"
using root_step[of _ _ R Var] by auto
lemma par_rstep_rsteps: "par_rstep R ⊆ (rstep R)⇧*"
proof
fix s t
assume "(s,t) ∈ par_rstep R"
then show "(s,t) ∈ (rstep R)⇧*"
proof (induct rule: par_rstep.induct)
case (root_step s t sigma)
then show ?case by auto
next
case (par_step_var x)
then show ?case by auto
next
case (par_step_fun ts ss f)
from all_ctxt_closedD[of UNIV, OF all_ctxt_closed_rsteps _ par_step_fun(3) par_step_fun(2)]
show ?case unfolding par_step_fun(3) by simp
qed
qed
lemma rstep_par_rstep: "rstep R ⊆ par_rstep R"
by (rule rstep_subset[OF ctxt_closed_par_rstep subst.closedI R_par_rstep],
insert subst_closed_par_rstep, auto)
lemma par_rsteps_rsteps: "(par_rstep R)⇧* = (rstep R)⇧*" (is "?P = ?R")
proof
from rtrancl_mono[OF par_rstep_rsteps[of R]] show "?P ⊆ ?R" by simp
from rtrancl_mono[OF rstep_par_rstep] show "?R ⊆ ?P" .
qed
lemma wf_trs_par_rstep: assumes wf: "⋀ l r. (l,r) ∈ R ⟹ is_Fun l"
and step: "(Var x, t) ∈ par_rstep R"
shows "t = Var x"
using step
proof (cases rule: par_rstep.cases)
case (root_step l r σ)
from root_step(1) wf[OF root_step(3)] show ?thesis by (cases l, auto)
qed auto
text ‹main lemma which tells us, that either a parallel rewrite step of l ⋅ σ is inside l, or
we can do the step completely inside σ›
lemma par_rstep_linear_subst: assumes lin: "linear_term l"
and step: "(l ⋅ σ, t) ∈ par_rstep R"
shows "(∃ τ. t = l ⋅ τ ∧ (∀ x ∈ vars_term l. (σ x, τ x) ∈ par_rstep R) ∨
(∃ C l'' l' r'. l = C⟨l''⟩ ∧ is_Fun l'' ∧ (l',r') ∈ R ∧ (l'' ⋅ σ = l' ⋅ τ) ∧ ((C ⋅⇩c σ) ⟨ r' ⋅ τ ⟩, t) ∈ par_rstep R))"
using lin step
proof (induction l arbitrary: t)
case (Var x t)
let ?tau = "λ y. t"
show ?case
by (rule exI[of _ ?tau], rule disjI1, insert Var(2), auto)
next
case (Fun f ss)
let ?ss = "map (λ s. s ⋅ σ) ss"
let ?R = "par_rstep R"
from Fun(3)
show ?case
proof (cases rule: par_rstep.cases)
case (root_step l r τ)
show ?thesis
proof (rule exI, rule disjI2, intro exI conjI)
show "(l,r) ∈ R" by (rule root_step(3))
show "Fun f ss = □⟨Fun f ss⟩" by simp
show "(Fun f ss) ⋅ σ = l ⋅ τ" by (rule root_step(1))
show "((□ ⋅⇩c σ)⟨ r ⋅ τ ⟩, t) ∈ ?R" unfolding root_step(2) using par_rstep_refl by simp
qed simp
next
case (par_step_var x)
then show ?thesis by simp
next
case (par_step_fun ts ss1 g)
then have id: "ss1 = ?ss" "g = f" and len: "length ts = length ss" by auto
let ?p1 = "λ τ i. ts ! i = ss ! i ⋅ τ ∧ (∀ x ∈ vars_term (ss ! i). (σ x, τ x) ∈ ?R)"
let ?p2 = "λ τ i. (∃ C l'' l' r'. ss ! i = C⟨ l''⟩ ∧ is_Fun l'' ∧ (l',r') ∈ R ∧ l'' ⋅ σ = l' ⋅ τ ∧ ((C ⋅⇩c σ)⟨ r' ⋅ τ ⟩, (ts ! i)) ∈ ?R)"
let ?p = "λ τ i. ?p1 τ i ∨ ?p2 τ i"
{
fix i
assume i: "i < length ss"
with par_step_fun(4) id have i2: "i < length ts" by auto
from par_step_fun(3)[OF i2] have step: "(ss ! i ⋅ σ, ts ! i) ∈ par_rstep R" unfolding id nth_map[OF i] .
from i have mem: "ss ! i ∈ set ss" by auto
from Fun.prems(1) mem have "linear_term (ss ! i)" by auto
from Fun.IH[OF mem this step] have "∃ τ. ?p τ i" .
}
then have "∀ i. ∃ tau. i < length ss ⟶ ?p tau i" by blast
from choice[OF this] obtain taus where taus: "⋀ i. i < length ss ⟹ ?p (taus i) i" by blast
show ?thesis
proof (cases "∃ i. i < length ss ∧ ?p2 (taus i) i")
case True
then obtain i where i: "i < length ss" and p2: "?p2 (taus i) i" by blast+
from par_step_fun(2)[unfolded id] have t: "t = Fun f ts" .
from i have i': "i < length ts" unfolding len .
from p2 obtain C l'' l' r' where ssi: "ss ! i = C ⟨l''⟩" and "is_Fun l''" "(l',r') ∈ R" "l'' ⋅ σ = l' ⋅ taus i"
and tsi: "((C ⋅⇩c σ) ⟨ r' ⋅ taus i ⟩, ts ! i) ∈ ?R" by blast
from id_take_nth_drop[OF i, unfolded ssi] obtain bef aft where ss: "ss = bef @ C ⟨ l'' ⟩ # aft"
and bef: "bef = take i ss"
and aft: "aft = drop (Suc i) ss" by blast
let ?C = "More f bef C aft"
let ?r = "(C ⋅⇩c σ) ⟨ r' ⋅ taus i ⟩"
let ?sig = "map (λ s. s ⋅ σ)"
let ?bra = "?sig bef @ ?r # ?sig aft"
have C: "(?C ⋅⇩c σ) ⟨ r' ⋅ taus i ⟩ = Fun f ?bra" by simp
show ?thesis unfolding ss
proof (rule exI[of _ "taus i"], rule disjI2, rule exI[of _ ?C], intro exI conjI)
show "is_Fun l''" by fact
show "(l',r') ∈ R" by fact
show "l'' ⋅ σ = l' ⋅ taus i" by fact
show "((?C ⋅⇩c σ) ⟨ r' ⋅ taus i ⟩, t) ∈ ?R" unfolding C t
proof (rule par_rstep.par_step_fun)
show "length ?bra = length ts"
unfolding len unfolding ss by simp
next
fix j
assume j: "j < length ts"
show "(?bra ! j, ts ! j) ∈ ?R"
proof (cases "j = i")
case True
then have "?bra ! j = ?r" using bef i by (simp add: nth_append)
then show ?thesis using tsi True by simp
next
case False
from bef i have "min (length ss) i = i" by simp
then have "?bra ! j = (?sig bef @ (C ⟨ l'' ⟩ ⋅ σ) # ?sig aft) ! j" using False bef i by (simp add: nth_append)
also have "... = ?sig ss ! j" unfolding ss by simp
also have "... = ss1 ! j" unfolding id ..
finally show ?thesis
using par_step_fun(3)[OF j] by auto
qed
qed
qed simp
next
case False
with taus have taus: "⋀ i. i < length ss ⟹ ?p1 (taus i) i" by blast
from Fun(2) have "is_partition (map vars_term ss)" by simp
from subst_merge[OF this, of taus] obtain τ where tau: "⋀ i x. i < length ss ⟹ x ∈ vars_term (ss ! i) ⟹ τ x = taus i x" by auto
let ?tau = τ
{
fix i
assume i: "i < length ss"
then have mem: "ss ! i ∈ set ss" by auto
from taus[OF i] have p1: "?p1 (taus i) i" .
have id: "ss ! i ⋅ (taus i) = ss ! i ⋅ τ"
by (rule term_subst_eq, rule tau[OF i, symmetric])
have "?p1 ?tau i"
proof (rule conjI[OF _ ballI])
fix x
assume x: "x ∈ vars_term (ss ! i)"
with p1 have step: "(σ x, taus i x) ∈ par_rstep R" by auto
with tau[OF i x]
show "(σ x, ?tau x) ∈ par_rstep R" by simp
qed (insert p1[unfolded id], auto)
} note p1 = this
have p1: "⋀ i. i < length ss ⟹ ?p1 τ i" by (rule p1)
let ?ss = "map (λ s. s ⋅ τ) ss"
show ?thesis unfolding par_step_fun(2) id
proof (rule exI[of _ τ], rule disjI1, rule conjI[OF _ ballI])
have "ts = map (λ i. ts ! i) [0 ..< (length ts)]" by (rule map_nth[symmetric])
also have "... = map (λ i. ?ss ! i) [0 ..< length ?ss]" unfolding len using p1 by auto
also have "... = ?ss" by (rule map_nth)
finally have ts: "ts = ?ss" .
show "Fun f ts = Fun f ss ⋅ τ" unfolding ts by auto
next
fix x
assume "x ∈ vars_term (Fun f ss)"
then obtain s where s: "s ∈ set ss" and x: "x ∈ vars_term s" by auto
from s[unfolded set_conv_nth] obtain i where i: "i < length ss" and s: "s = ss ! i" by auto
from p1[OF i] x[unfolded s]
show "(σ x, τ x) ∈ par_rstep R" by blast
qed
qed
qed
qed
lemma par_rstep_id:
"(s, t) ∈ R ⟹ (s, t) ∈ par_rstep R"
using par_rstep.root_step [of s t R Var] by simp
subsection ‹Function Symbols and Variables›
subsection ‹Function Symbols and Variables›
fun root_list :: "('f, 'v) term ⇒ ('f × nat) list"
where
"root_list (Var x) = []" |
"root_list (Fun f ts) = [(f, length ts)]"
definition vars_rule_list :: "('f, 'v) rule ⇒ 'v list"
where
"vars_rule_list r = vars_term_list (fst r) @ vars_term_list (snd r)"
definition funs_rule_list :: "('f, 'v) rule ⇒ 'f list"
where
"funs_rule_list r = funs_term_list (fst r) @ funs_term_list (snd r)"
definition funas_rule_list :: "('f, 'v) rule ⇒ ('f × nat) list"
where
"funas_rule_list r = funas_term_list (fst r) @ funas_term_list (snd r)"
definition roots_rule_list :: "('f, 'v) rule ⇒ ('f × nat) list"
where
"roots_rule_list r = root_list (fst r) @ root_list (snd r)"
definition funas_args_rule_list :: "('f, 'v) rule ⇒ ('f × nat) list"
where
"funas_args_rule_list r = funas_args_term_list (fst r) @ funas_args_term_list (snd r)"
lemma set_vars_rule_list [simp]:
"set (vars_rule_list r) = vars_rule r"
by (simp add: vars_rule_list_def vars_rule_def)
lemma set_funs_rule_list [simp]:
"set (funs_rule_list r) = funs_rule r"
by (simp add: funs_rule_list_def funs_rule_def)
lemma set_funas_rule_list [simp]:
"set (funas_rule_list r) = funas_rule r"
by (simp add: funas_rule_list_def funas_rule_def)
lemma set_roots_rule_list [simp]:
"set (roots_rule_list r) = roots_rule r"
by (cases "fst r" "snd r" rule: term.exhaust [case_product term.exhaust])
(auto simp: roots_rule_list_def roots_rule_def ac_simps)
lemma set_funas_args_rule_list [simp]:
"set (funas_args_rule_list r) = funas_args_rule r"
by (simp add: funas_args_rule_list_def funas_args_rule_def)
definition vars_trs_list :: "('f, 'v) rule list ⇒ 'v list"
where
"vars_trs_list trs = concat (map vars_rule_list trs)"
definition funs_trs_list :: "('f, 'v) rule list ⇒ 'f list"
where
"funs_trs_list trs = concat (map funs_rule_list trs)"
definition funas_trs_list :: "('f, 'v) rule list ⇒ ('f × nat) list"
where
"funas_trs_list trs = concat (map funas_rule_list trs)"
definition roots_trs_list :: "('f, 'v) rule list ⇒ ('f × nat) list"
where
"roots_trs_list trs = remdups (concat (map roots_rule_list trs))"
definition funas_args_trs_list :: "('f, 'v) rule list ⇒ ('f × nat) list"
where
"funas_args_trs_list trs = concat (map funas_args_rule_list trs)"
lemma set_vars_trs_list [simp]:
"set (vars_trs_list trs) = vars_trs (set trs)"
by (simp add: vars_trs_def vars_trs_list_def)
lemma set_funs_trs_list [simp]:
"set (funs_trs_list R) = funs_trs (set R)"
by (simp add: funs_trs_def funs_trs_list_def)
lemma set_funas_trs_list [simp]:
"set (funas_trs_list R) = funas_trs (set R)"
by (simp add: funas_trs_def funas_trs_list_def)
lemma set_roots_trs_list [simp]:
"set (roots_trs_list R) = roots_trs (set R)"
by (simp add: roots_trs_def roots_trs_list_def)
lemma set_funas_args_trs_list [simp]:
"set (funas_args_trs_list R) = funas_args_trs (set R)"
by (simp add: funas_args_trs_def funas_args_trs_list_def)
lemmas vars_list_defs = vars_trs_list_def vars_rule_list_def
lemmas funs_list_defs = funs_trs_list_def funs_rule_list_def
lemmas funas_list_defs = funas_trs_list_def funas_rule_list_def
lemmas roots_list_defs = roots_trs_list_def roots_rule_list_def
lemmas funas_args_list_defs = funas_args_trs_list_def funas_args_rule_list_def
lemma vars_trs_list_Nil [simp]:
"vars_trs_list [] = []" unfolding vars_trs_list_def by simp
context
fixes R :: "('f, 'v) trs"
assumes "wf_trs R"
begin
lemma funas_term_subst_rhs:
assumes "funas_trs R ⊆ F" and "(l, r) ∈ R" and "funas_term (l ⋅ σ) ⊆ F"
shows "funas_term (r ⋅ σ) ⊆ F"
proof -
have "vars_term r ⊆ vars_term l" using ‹wf_trs R› and ‹(l, r) ∈ R› by (auto simp: wf_trs_def)
moreover have "funas_term l ⊆ F" and "funas_term r ⊆ F"
using ‹funas_trs R ⊆ F› and ‹(l, r) ∈ R› by (auto simp: funas_defs) force+
ultimately show ?thesis
using ‹funas_term (l ⋅ σ) ⊆ F› by (force simp: funas_term_subst)
qed
lemma vars_rule_lhs:
"r ∈ R ⟹ vars_rule r = vars_term (fst r)"
using ‹wf_trs R› by (cases r) (auto simp: wf_trs_def vars_rule_def)
end
abbreviation NF_trs :: "('f, 'v) trs ⇒ ('f, 'v) terms" where
"NF_trs R ≡ NF (rstep R)"
lemma NF_trs_mono: "r ⊆ s ⟹ NF_trs s ⊆ NF_trs r"
by (rule NF_anti_mono[OF rstep_mono])
lemma NF_trs_union: "NF_trs (R ∪ S) = NF_trs R ∩ NF_trs S"
unfolding rstep_union using NF_anti_mono[of _ "rstep R ∪ rstep S"] by auto
abbreviation NF_terms :: "('f, 'v) terms ⇒ ('f, 'v) terms" where
"NF_terms Q ≡ NF (rstep (Id_on Q))"
lemma NF_terms_anti_mono:
"Q ⊆ Q' ⟹ NF_terms Q' ⊆ NF_terms Q"
by (rule NF_trs_mono, auto)
lemma lhs_var_not_NF:
assumes "l ∈ T" and "is_Var l" shows "t ∉ NF_terms T"
proof -
from assms obtain x where l: "l = Var x" by (cases l, auto)
let ?σ = "subst x t"
from assms have "l ∉ NF_terms T" by auto
with NF_instance[of l "?σ" "Id_on T"]
have "l ⋅ ?σ ∉ NF_terms T" by auto
then show ?thesis by (simp add: l subst_def)
qed
lemma not_NF_termsE[elim]:
assumes "s ∉ NF_terms Q"
obtains l C σ where "l ∈ Q" and "s = C⟨l ⋅ σ⟩"
proof -
from assms obtain t where "(s, t) ∈ rstep (Id_on Q)" by auto
with ‹⋀l C σ. ⟦l ∈ Q; s = C⟨l ⋅ σ⟩⟧ ⟹ thesis› show ?thesis by auto
qed
lemma notin_NF_E [elim]:
fixes R :: "('f, 'v) trs"
assumes "t ∉ NF_trs R"
obtains C l and σ :: "('f, 'v) subst" where "l ∈ lhss R" and "t = C⟨l ⋅ σ⟩"
proof -
assume 1: "⋀l C (σ::('f, 'v) subst). l ∈ lhss R ⟹ t = C⟨l ⋅ σ⟩ ⟹ thesis"
from assms obtain u where "(t, u) ∈ rstep R" by (auto simp: NF_def)
then obtain C σ l r where "(l, r) ∈ R" and "t = C⟨l ⋅ σ⟩" by blast
with 1 show ?thesis by force
qed
lemma NF_ctxt_subst: "NF_terms Q = {t. ¬ (∃ C q σ. t = C⟨q⋅σ⟩ ∧ q ∈ Q)}" (is "_ = ?R")
proof -
{
fix t
assume "t ∉ ?R"
then obtain C q σ where t: "t = C⟨q⋅σ⟩" and q: "q ∈ Q" by auto
have "(t,t) ∈ rstep (Id_on Q)"
unfolding t using q by auto
then have "t ∉ NF_terms Q" by auto
}
moreover
{
fix t
assume "t ∉ NF_terms Q"
then obtain C q σ where t: "t = C⟨q⋅σ⟩" and q: "q ∈ Q" by auto
then have "t ∉ ?R" by auto
}
ultimately show ?thesis by auto
qed
lemma some_NF_imp_no_Var:
assumes "t ∈ NF_terms Q"
shows "Var x ∉ Q"
proof
assume "Var x ∈ Q"
with assms[unfolded NF_ctxt_subst] have "⋀ σ C. t ≠ C ⟨ σ x ⟩" by force
from this[of Hole "λ _. t"] show False by simp
qed
lemma NF_map_vars_term_inj:
assumes inj: "⋀ x. n (m x) = x" and NF: "t ∈ NF_terms Q"
shows "(map_vars_term m t) ∈ NF_terms (map_vars_term m ` Q)"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain u where "(map_vars_term m t, u) ∈ rstep (Id_on (map_vars_term m ` Q))" by blast
then obtain ml mr C σ where in_mR: "(ml, mr) ∈ Id_on (map_vars_term m ` Q)"
and mt: "map_vars_term m t = C⟨ml ⋅ σ⟩" by best
let ?m = n
from in_mR obtain l r where "(l, r) ∈ Id_on Q" and ml: "ml = map_vars_term m l" by auto
have "t = map_vars_term ?m (map_vars_term m t)" by (simp add: map_vars_term_inj_compose[of n m, OF inj])
also have "… = map_vars_term ?m (C⟨ml ⋅ σ⟩)" by (simp add: mt)
also have "… = (map_vars_ctxt ?m C)⟨map_vars_term ?m (map_vars_term m l ⋅ σ)⟩"
by (simp add: map_vars_term_ctxt_commute ml)
also have "… = (map_vars_ctxt ?m C)⟨l ⋅ (map_vars_subst_ran ?m (σ ∘ m))⟩"
by (simp add: apply_subst_map_vars_term map_vars_subst_ran)
finally show False using NF and ‹(l, r) ∈ Id_on Q› by auto
qed
lemma notin_NF_terms: "t ∈ Q ⟹ t ∉ NF_terms Q"
using lhs_notin_NF_rstep[of t t "Id_on Q"] by (simp add: Id_on_iff)
lemma NF_termsI [intro]:
assumes NF: "⋀ C l σ. t = C ⟨l ⋅ σ⟩ ⟹ l ∈ Q ⟹ False"
shows "t ∈ NF_terms Q"
by (rule ccontr, rule not_NF_termsE [OF _ NF])
lemma NF_args_imp_NF:
assumes ss: "⋀ s. s ∈ set ss ⟹ s ∈ NF_terms Q"
and someNF: "t ∈ NF_terms Q"
and root: "Some (f,length ss) ∉ root ` Q"
shows "(Fun f ss) ∈ NF_terms Q"
proof
fix C l σ
assume id: "Fun f ss = C ⟨ l ⋅ σ ⟩" and l: "l ∈ Q"
show False
proof (cases C)
case Hole
with id have id: "Fun f ss = l ⋅ σ" by simp
show False
proof (cases l)
case (Fun g ls)
with id have fg: "f = g" and ss: "ss = map (λ s. s ⋅ σ) ls" by auto
from arg_cong[OF ss, of length] have len: "length ss = length ls" by simp
from l[unfolded Fun] root[unfolded fg len] show False by force
next
case (Var x)
from some_NF_imp_no_Var[OF someNF] Var l show False by auto
qed
next
case (More g bef D aft)
note id = id[unfolded More]
from id have NF: "ss ! length bef = D ⟨l ⋅ σ⟩" by auto
from id have mem: "ss ! length bef ∈ set ss" by auto
from ss[OF mem, unfolded NF_ctxt_subst NF] l show False by auto
qed
qed
lemma NF_Var_is_Fun:
assumes Q: "Ball Q is_Fun"
shows "Var x ∈ NF_terms Q"
proof
fix C l σ
assume x: "Var x = C ⟨ l ⋅ σ ⟩" and l: "l ∈ Q"
from l Q obtain f ls where l: "l = Fun f ls" by (cases l, auto)
then show False using x by (cases C, auto)
qed
lemma NF_terms_lhss [simp]: "NF_terms (lhss R) = NF (rstep R)"
proof
show "NF (rstep R) ⊆ NF_terms (lhss R)" by force
next
show "NF_terms (lhss R) ⊆ NF (rstep R)"
proof
fix s assume NF: "s ∈ NF_terms (lhss R)"
show "s ∈ NF (rstep R)"
proof (rule ccontr)
assume "s ∉ NF (rstep R)"
then obtain t where "(s, t) ∈ rstep R" by auto
then obtain l r C σ where "(l, r) ∈ R" and s: "s = C⟨l ⋅ σ⟩" by auto
then have "(l, l) ∈ Id_on (lhss R)" by force
then have "(s, s) ∈ rstep (Id_on (lhss R))" unfolding s by auto
with NF show False by auto
qed
qed
qed
fun funposs_list :: "('f, 'v) term ⇒ pos list"
where
"funposs_list (Var x) = []" |
"funposs_list (Fun f ss) = ([] # concat (map (λ (i, ps).
map ((#) i) ps) (zip [0 ..< length ss] (map funposs_list ss))))"
lemma set_funposs_list [simp]:
"set (funposs_list t) = funposs t"
by (induct t; auto simp: UNION_set_zip)
abbreviation "relstep R E ≡ relto (rstep R) (rstep E)"
lemma args_SN_on_relstep_nrrstep_imp_args_SN_on:
assumes SN: "⋀ u. s ⊳ u ⟹ SN_on (relstep R E) {u}"
and st: "(s,t) ∈ nrrstep (R ∪ E)"
and supt: "t ⊳ u"
shows "SN_on (relstep R E) {u}"
proof -
from nrrstepE[OF st] obtain C l r σ where "C ≠ □" and lr: "(l,r) ∈ R ∪ E"
and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩" by blast
then obtain f bef C aft where s: "s = Fun f (bef @ C⟨l ⋅ σ⟩ # aft)" and t: "t = Fun f (bef @ C⟨r ⋅ σ⟩ # aft)"
by (cases C, auto)
let ?ts = "bef @ C⟨r ⋅ σ⟩ # aft"
let ?ss = "bef @ C⟨l ⋅ σ⟩ # aft"
from supt obtain D where "t = D⟨u⟩" and "D ≠ □" by auto
then obtain bef' aft' D where t': "t = Fun f (bef' @ D⟨u⟩ # aft')" unfolding t by (cases D, auto)
have "D⟨u⟩ ⊵ u" by auto
then have supt: "⋀ s. s ⊳ D⟨u⟩ ⟹ s ⊳ u" by (metis supt_supteq_trans)
show "SN_on (relstep R E) {u}"
proof (cases "D⟨u⟩ ∈ set ?ss")
case True
then have "s ⊳ D⟨u⟩" unfolding s by auto
then have "s ⊳ u" by (rule supt)
with SN show ?thesis by auto
next
case False
have "D⟨u⟩ ∈ set ?ts" using arg_cong[OF t'[unfolded t], of args] by auto
with False have Du: "D⟨u⟩ = C⟨r ⋅ σ⟩" by auto
have "s ⊳ C⟨l ⋅ σ⟩" unfolding s by auto
with SN have "SN_on (relstep R E) {C⟨l ⋅ σ⟩}" by auto
from step_preserves_SN_on_relto[OF _ this, of "C⟨r ⋅ σ⟩"] lr
have SN: "SN_on (relstep R E) {D⟨u⟩}" using Du by auto
show ?thesis
by (rule ctxt_closed_SN_on_subt[OF ctxt.closed_relto SN], auto)
qed
qed
lemma Tinf_nrrstep:
assumes tinf: "s ∈ Tinf (relstep R E)" and st: "(s,t) ∈ nrrstep (R ∪ E)"
and t: "¬ SN_on (relstep R E) {t}"
shows "t ∈ Tinf (relstep R E)"
unfolding Tinf_def
by (standard, intro conjI[OF t] allI impI, rule args_SN_on_relstep_nrrstep_imp_args_SN_on[OF _ st],
insert tinf[unfolded Tinf_def], auto)
lemma subterm_preserves_SN_on_relstep:
"SN_on (relstep R E) {s} ⟹ s ⊵ t ⟹ SN_on (relstep R E) {t}"
using SN_imp_SN_subt [of "rstep (rstep ((rstep E)⇧*) O rstep R O rstep ((rstep E)⇧*))"]
by (simp only: rstep_relcomp_idemp2) (simp only: rstep_rtrancl_idemp)
inductive_set rstep_rule :: "('f, 'v) rule ⇒ ('f, 'v) term rel" for ρ
where
rule: "s = C⟨fst ρ ⋅ σ⟩ ⟹ t = C⟨snd ρ ⋅ σ⟩ ⟹ (s, t) ∈ rstep_rule ρ"
lemma rstep_ruleI [intro]:
"s = C⟨l ⋅ σ⟩ ⟹ t = C⟨r ⋅ σ⟩ ⟹ (s, t) ∈ rstep_rule (l, r)"
by (auto simp: rstep_rule.simps)
lemma rstep_rule_ctxt:
"(s, t) ∈ rstep_rule ρ ⟹ (C⟨s⟩, C⟨t⟩) ∈ rstep_rule ρ"
using rstep_rule.rule [of "C⟨s⟩" "C ∘⇩c D" ρ _ "C⟨t⟩" for D]
by (auto elim: rstep_rule.cases simp: ctxt_of_pos_term_append)
lemma rstep_rule_subst:
assumes "(s, t) ∈ rstep_rule ρ"
shows "(s ⋅ σ, t ⋅ σ) ∈ rstep_rule ρ"
using assms
proof (cases)
case (rule C τ)
then show ?thesis
using rstep_rule.rule [of "s ⋅ σ" _ "ρ" "τ ∘⇩s σ"]
by (auto elim!: rstep_rule.cases simp: ctxt_of_pos_term_subst)
qed
lemma rstep_rule_imp_rstep:
"ρ ∈ R ⟹ (s, t) ∈ rstep_rule ρ ⟹ (s, t) ∈ rstep R"
by (force elim: rstep_rule.cases)
lemma rstep_imp_rstep_rule:
assumes "(s, t) ∈ rstep R"
obtains l r where "(l, r) ∈ R" and "(s, t) ∈ rstep_rule (l, r)"
using assms by blast
lemma term_subst_rstep:
assumes "⋀x. x ∈ vars_term t ⟹ (σ x, τ x) ∈ rstep R"
shows "(t ⋅ σ, t ⋅ τ) ∈ (rstep 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) ∈ rstep R" by auto
from Fun(1) [OF t⇩i this] have "(t⇩i ⋅ σ, t⇩i ⋅ τ) ∈ (rstep R)⇧*" by blast
}
then show ?case by (simp add: args_rsteps_imp_rsteps)
qed (auto)
lemma term_subst_rsteps:
assumes "⋀x. x ∈ vars_term t ⟹ (σ x, τ x) ∈ (rstep R)⇧*"
shows "(t ⋅ σ, t ⋅ τ) ∈ (rstep R)⇧*"
by (metis assms rstep_rtrancl_idemp rtrancl_idemp term_subst_rstep)
lemma term_subst_rsteps_join:
assumes "⋀y. y ∈ vars_term u ⟹ (σ⇩1 y, σ⇩2 y) ∈ (rstep R)⇧↓"
shows "(u ⋅ σ⇩1, u ⋅ σ⇩2) ∈ (rstep R)⇧↓"
using assms
proof -
{ fix x
assume "x ∈ vars_term u"
from assms [OF this] have "∃σ. (σ⇩1 x, σ x) ∈ (rstep R)⇧* ∧ (σ⇩2 x, σ x) ∈ (rstep R)⇧*" by auto
}
then have "∀x ∈ vars_term u. ∃σ. (σ⇩1 x, σ x) ∈ (rstep R)⇧* ∧ (σ⇩2 x, σ x) ∈ (rstep R)⇧*" by blast
then obtain s where "∀x ∈ vars_term u. (σ⇩1 x, (s x) x) ∈ (rstep R)⇧* ∧ (σ⇩2 x, (s x) x) ∈ (rstep R)⇧*" by metis
then obtain σ where "∀x ∈ vars_term u. (σ⇩1 x, σ x) ∈ (rstep R)⇧* ∧ (σ⇩2 x, σ x) ∈ (rstep R)⇧*" by fast
then have "(u ⋅ σ⇩1, u ⋅ σ) ∈ (rstep R)⇧* ∧ (u ⋅ σ⇩2, u ⋅ σ) ∈ (rstep R)⇧*" using term_subst_rsteps by metis
then show ?thesis by blast
qed
lemma funas_trs_converse [simp]: "funas_trs (R¯) = funas_trs R"
by (auto simp: funas_defs)
lemma rstep_rev: assumes "(s, t) ∈ rstep_pos {(l,r)} p" shows "((t, s) ∈ rstep_pos {(r,l)} p)"
proof-
from assms obtain σ where step:"t = (ctxt_of_pos_term p s)⟨r ⋅ σ⟩" "p ∈ poss s" "s |_ p = l ⋅ σ"
unfolding rstep_pos.simps by auto
with replace_at_below_poss[of p s p] have pt:"p ∈ poss t" by auto
with step ctxt_supt_id[OF step(2)] have "s = (ctxt_of_pos_term p t)⟨l ⋅ σ⟩"
by (simp add: ctxt_of_pos_term_replace_at_below)
with step ctxt_supt_id[OF pt] show ?thesis unfolding rstep_pos.simps
by (metis pt replace_at_subt_at singletonI)
qed
lemma conversion_ctxt_closed: "(s, t) ∈ (rstep R)⇧↔⇧* ⟹ (C⟨s⟩, C⟨t⟩) ∈ (rstep R)⇧↔⇧*"
using rsteps_closed_ctxt unfolding conversion_def
by (simp only: rstep_simps(5)[symmetric])
lemma conversion_subst_closed:
"(s, t) ∈ (rstep R)⇧↔⇧* ⟹ (s ⋅ σ, t ⋅ σ) ∈ (rstep R)⇧↔⇧*"
using rsteps_closed_subst unfolding conversion_def
by (simp only: rstep_simps(5)[symmetric])
lemma rstep_simulate_conv:
assumes "⋀ l r. (l, r) ∈ S ⟹ (l, r) ∈ (rstep R)⇧↔⇧*"
shows "(rstep S) ⊆ (rstep R)⇧↔⇧*"
proof
fix s t
assume "(s, t) ∈ rstep S"
then obtain l r C σ where s: "s = C⟨l ⋅ σ⟩" and t:"t = C⟨r ⋅ σ⟩" and lr: "(l, r) ∈ S"
unfolding rstep_iff_rstep_r_c_s rstep_r_c_s_def by auto
with assms have "(l, r) ∈ (rstep R)⇧↔⇧*" by auto
then show "(s, t) ∈ (rstep R)⇧↔⇧*" using conversion_ctxt_closed conversion_subst_closed s t by metis
qed
lemma symcl_simulate_conv:
assumes "⋀ l r. (l, r) ∈ S ⟹ (l, r) ∈ (rstep R)⇧↔⇧*"
shows "(rstep S)⇧↔ ⊆ (rstep R)⇧↔⇧*"
using rstep_simulate_conv[OF assms]
by auto (metis conversion_inv subset_iff)
lemma conv_union_simulate:
assumes "⋀ l r. (l, r) ∈ S ⟹ (l, r) ∈ (rstep R)⇧↔⇧*"
shows "(rstep (R ∪ S))⇧↔⇧* = (rstep R)⇧↔⇧*"
proof
show "(rstep (R ∪ S))⇧↔⇧* ⊆ (rstep R)⇧↔⇧*"
unfolding conversion_def
proof
fix s t
assume "(s, t) ∈ ((rstep (R ∪ S))⇧↔)⇧*"
then show "(s, t) ∈ ((rstep R)⇧↔)⇧*"
proof (induct rule: rtrancl_induct)
case (step u t)
then have "(u, t) ∈ (rstep R)⇧↔ ∨ (u, t) ∈ (rstep S)⇧↔" by auto
then show ?case
proof
assume "(u, t) ∈ (rstep R)⇧↔"
with step show ?thesis using rtrancl_into_rtrancl by metis
next
assume "(u, t) ∈ (rstep S)⇧↔"
with symcl_simulate_conv[OF assms] have "(u, t) ∈ (rstep R)⇧↔⇧*" by auto
with step show ?thesis by auto
qed
qed simp
qed
next
show "(rstep R)⇧↔⇧* ⊆ (rstep (R ∪ S))⇧↔⇧*"
unfolding conversion_def
using rstep_union rtrancl_mono sup.cobounded1 symcl_Un
by metis
qed
definition "suptrel R = (relto {⊳} (rstep R))⇧+"
end