theory Embedding_Trs
imports
QTRS.Trs
"HOL-Library.Sublist"
begin
definition "Emb F P =
{(Fun f ts, t) | f ts t. (f, length ts) ∈ F ∧ t ∈ set ts} ∪
{(Fun f ss, Fun g ts) | f ss g ts.
P (f, length ss) (g, length ts) ∧ (f, length ss) ∈ F ∧ (g, length ts) ∈ F ∧ subseq ts ss}"
definition "emb F P = (rstep (Emb F P))⇧+"
definition "embeq F P = (rstep (Emb F P))⇧*"
lemma Emb_arg:
assumes "(f, length ts) ∈ F" and "t ∈ set ts"
shows "(Fun f ts, t) ∈ Emb F P"
using assms by (auto simp: Emb_def)
lemma Emb_subseq:
assumes "P (f, length ss) (g, length ts)"
and "(f, length ss) ∈ F" and "(g, length ts) ∈ F"
and "subseq ts ss"
shows "(Fun f ss, Fun g ts) ∈ Emb F P"
using assms by (auto simp: Emb_def)
lemma embeq_arg:
assumes "(f, length ts) ∈ F" and "t ∈ set ts"
shows "(Fun f ts, t) ∈ embeq F P"
using Emb_arg [OF assms, of P] by (auto simp: embeq_def)
lemma embeq_subseq:
assumes "P (f, length ss) (g, length ts)"
and "(f, length ss) ∈ F" and "(g, length ts) ∈ F"
and "subseq ts ss"
shows "(Fun f ss, Fun g ts) ∈ embeq F P"
using Emb_subseq [of P, OF assms] by (auto simp: embeq_def)
lemma embeq_trans:
"(s, t) ∈ embeq F P ⟹ (t, u) ∈ embeq F P ⟹ (s, u) ∈ embeq F P"
by (auto simp: embeq_def)
inductive pairwise for P
where
Nil [simp, intro]: "pairwise P [] []" |
Cons [intro]: "P x y ⟹ pairwise P xs ys ⟹ pairwise P (x # xs) (y # ys)"
lemma pairwise_refl:
"pairwise P⇧=⇧= xs xs"
by (induct xs) auto
lemma list_emb_subseq_left:
assumes "list_emb P xs zs"
obtains ys where "subseq xs ys" and "pairwise P⇧=⇧= ys zs"
using assms and pairwise_refl by (induct) (auto)
lemma list_emb_subseq_right:
assumes "list_emb P xs zs"
obtains ys where "pairwise P⇧=⇧= xs ys" and "subseq ys zs"
using assms by (induct) auto
lemma pairwiseD:
assumes "pairwise P xs ys"
shows "length xs = length ys ∧ (∀i < length xs. P (xs ! i) (ys ! i))"
using assms by (induct) (auto simp: nth_Cons split: nat.splits)
lemma list_emb_conjunct2:
assumes "list_emb (λx y. P x y ∧ Q x y) xs ys"
shows "list_emb Q xs ys"
using assms by (induct) auto
lemma pairwise_rsteps:
assumes "pairwise (λs t. (s, t) ∈ (rstep R)⇧*) ss ts"
shows "(Fun f ss, Fun f ts) ∈ (rstep R)⇧*"
proof (rule args_rsteps_imp_rsteps)
show "length ss = length ts"
and "∀i < length ss. (ss ! i, ts ! i) ∈ (rstep R)⇧*"
using pairwiseD [OF assms] by auto
qed
lemma pairwise_length:
assumes "pairwise P xs ys"
shows "length xs = length ys"
using assms by (induct) simp_all
lemma pairwise_embeq:
assumes "pairwise (λs t. (t, s) ∈ embeq F P)⇧=⇧= ss ts"
shows "(Fun f ts, Fun f ss) ∈ embeq F P"
proof (unfold embeq_def, rule args_rsteps_imp_rsteps)
show "length ts = length ss"
and "∀i < length ts. (ts ! i, ss ! i) ∈ (rstep (Emb F P))⇧*"
using pairwiseD [OF assms] by (auto simp: embeq_def)
qed
lemma emb_reflcl_embeq [simp]:
"(emb F P)⇧= = embeq F P"
by (auto simp: embeq_def emb_def)
lemma Emb_cases [consumes 1, case_names arg subseq, cases set: Emb]:
assumes "(s, t) ∈ Emb F P"
and "⋀f ts. ⟦(f, length ts) ∈ F; t ∈ set ts; s = Fun f ts⟧ ⟹ Q"
and "⋀f ss g ts. ⟦P (f, length ss) (g, length ts); (f, length ss) ∈ F; (g, length ts) ∈ F;
subseq ts ss; s = Fun f ss; t = Fun g ts⟧ ⟹ Q"
shows Q
using assms by (auto simp: Emb_def)
lemma contains_Emb:
assumes "⋀t f ts. t ∈ set ts ⟹ (Fun f ts, t) ∈ R"
and "⋀f g ss ts. ⟦P (f, length ss) (g, length ts); subseq ts ss⟧ ⟹ (Fun f ss, Fun g ts) ∈ R"
and *: "(s, t) ∈ Emb F P"
shows "(s, t) ∈ R"
using * and assms by (cases) auto
lemma emb_subsetI:
fixes R :: "('f, 'v) term rel"
assumes trans: "⋀s t u. (s, t) ∈ R ⟹ (t, u) ∈ R ⟹ (s, u) ∈ R"
and ctxt: "⋀C s t. (s, t) ∈ R ⟹ (C⟨s⟩, C⟨t⟩) ∈ R"
and subst: "⋀σ s t. (s, t) ∈ R ⟹ (s ⋅ σ, t ⋅ σ) ∈ R"
and *: "⋀t f ts. t ∈ set ts ⟹ (Fun f ts, t) ∈ R"
"⋀f g ss ts. ⟦P (f, length ss) (g, length ts); subseq ts ss⟧ ⟹ (Fun f ss, Fun g ts) ∈ R"
shows "emb F P ⊆ R"
proof
{ fix s t :: "('f, 'v) term"
assume "(s, t) ∈ rstep (Emb F P)"
then have "(s, t) ∈ R"
proof (induct)
case (IH C σ l r)
with contains_Emb [OF *, of P]
have "(l, r) ∈ R" by blast
then show ?case by (auto dest: subst ctxt)
qed }
note * = this
fix s t :: "('f, 'v) term"
assume "(s, t) ∈ emb F P"
then show "(s, t) ∈ R"
unfolding emb_def by (induct s t) (auto dest: * trans)
qed
end