text ‹GTT for accepting parallel steps of a (left-linear, right-ground) TRS›
theory GTT_TRS
imports GTT GTT_Transitive_Closure Tree_Automata_Utils
begin
type_synonym ('f, 'q) term_state = "('f, 'q) term option"
definition cmn_ta_rules :: "('f, 'v) term set ⇒ (('f, 'v) term option, 'f) ta_rule set" where
"cmn_ta_rules T ≡ {f (map Some ts) → Some (Fun f ts) |f ts t. Fun f ts ⊴ t ∧ t ∈ T}"
definition TRS_fst :: "('f, 'v) trs ⇒ ('f, 'v) term set" where
"TRS_fst Ts ≡ {fst R |R. R ∈ Ts} "
definition TRS_snd :: "('f, 'v) trs ⇒ ('f, 'v) term set" where
"TRS_snd Ts ≡ {snd R |R. R ∈ Ts}"
definition TRS_terms :: "('f, 'v) trs ⇒ ('f, 'v) term set" where
"TRS_terms Ts ≡ TRS_fst Ts ∪ TRS_snd Ts"
definition trs_to_ta_A :: "('f, 'v) trs ⇒ (('f, 'v) term option, 'f) ta" where
"trs_to_ta_A Ts ≡ ta.make {}
(cmn_ta_rules (TRS_terms Ts))
{(Some l, Some r) |l r. (l, r) ∈ Ts}"
definition trs_to_ta_B :: "('f, 'v) trs ⇒ (('f, 'v) term option, 'f) ta" where
"trs_to_ta_B Ts ≡ ta.make {}
(cmn_ta_rules (TRS_terms Ts))
{(Some r, Some l) |l r. (l,r) ∈ Ts}"
abbreviation abs :: "('f, 'v) term ⇒ ('f, ('f, 'v) term option) term" where
"abs x ≡ adapt_vars x"
abbreviation rep :: "('f, ('f, 'v) term option) term ⇒ ('f, 'v) term" where
"rep x ≡ adapt_vars x"
abbreviation abs_R :: "(('f, 'v) term × ('f, 'v) term) set ⇒
(('f, ('f, 'v) term option) term × ('f, ('f, 'v) term option) term) set" where
"abs_R R ≡ (λt. (abs (fst t), abs (snd t))) ` R"
lemma symmetry_in_G_D:
"ta_rules (trs_to_ta_B R) = ta_rules (trs_to_ta_A R)"
"ta_eps (trs_to_ta_B R) = (λt. (snd t, fst t)) ` ta_eps (trs_to_ta_A R)"
unfolding trs_to_ta_B_def trs_to_ta_A_def by force+
lemma finite_embedding:
assumes "finite R"
shows "finite {(Some l, Some r) |l r. (l, r) ∈ R}"
proof -
have "{(Some l, Some r) |l r. (l, r) ∈ R} = (λ(l, r). (Some l, Some r)) ` R"
by auto
then show ?thesis using assms by auto
qed
lemma finite_collect:
assumes "finite S"
shows "finite {t |t w. t ⊴ w ∧ w ∈ S}"
proof -
have "∀w ∈ S. finite {t. t ⊴ w}" using finite_subterms assms by auto
hence "finite (⋃ ((λw. {t. t ⊴ w}) ` S))" using assms by blast
moreover have "{t |t w. t ⊴ w ∧ w ∈ S} = ⋃ ((λw. {t. t ⊴ w}) ` S)"
by blast
ultimately show ?thesis by argo
qed
lemma finite_ta_states:
assumes "finite R"
shows "finite (ta_states (trs_to_ta_A R))" "finite (ta_states (trs_to_ta_B R))"
proof -
have eps: "finite (ta_eps (trs_to_ta_A R))" using assms finite_embedding[OF assms]
unfolding trs_to_ta_A_def ta.make_def by auto
moreover have rules: "finite (ta_rules (trs_to_ta_A R))"
proof -
have fin: "finite (TRS_terms R)" using assms unfolding TRS_terms_def TRS_fst_def TRS_snd_def
proof -
have "∀f. finite {t. ∃p. (t :: ('a, 'b) Term.term) = f p ∧ p ∈ R}"
by (metis (no_types) Collect_mem_eq assms finite_image_set)
then show "finite ({fst p |p. p ∈ R} ∪ {snd p |p. p ∈ R})"
by blast
qed
let ?fts = "{Fun f ts |f ts t. (∃t ⊵ Fun f ts. t ∈ TRS_terms R)}"
have fin_fun: "finite {Fun f ts |f ts t. ∃t ⊵ Fun f ts. t ∈ TRS_terms R}"
proof -
have "{uu. ∃f ts t. uu = Fun f ts ∧ (∃t ⊵ Fun f ts. t ∈ TRS_terms R)}
⊆ {uu. ∃t w. uu = t ∧ w ⊵ t ∧ w ∈ TRS_terms R}" by blast
thus ?thesis
using finite_collect[OF fin]
finite_subset[of A "{uu. ∃t w. uu = t ∧ w ⊵ t ∧ w ∈ TRS_terms R}" for A]
by presburger
qed
then have "finite {f map Some ts → Some (Fun f ts) |f ts. ∃t ⊵ Fun f ts. t ∈ TRS_terms R}"
proof -
have "{f (map Some ts) → Some (Fun f ts) |f ts. ∃t ⊵ Fun f ts. t ∈ TRS_terms R} =
(λu. case u of Fun f ts ⇒ f (map Some ts) → Some (Fun f ts)) `
{Fun f ts |f ts t . (∃t ⊵ Fun f ts. t ∈ TRS_terms R)}"
by (smt Collect_cong Term.term.simps(6) setcompr_eq_image)
then show ?thesis using fin_fun by simp
qed
then show ?thesis unfolding trs_to_ta_A_def ta.make_def cmn_ta_rules_def by auto
qed
ultimately show "finite (ta_states (trs_to_ta_A R))"
unfolding trs_to_ta_A_def ta_states_def ta.make_def
by (simp add: r_states_def)
show "finite (ta_states (trs_to_ta_B R))"
using finite_imageI[of "ta_eps (trs_to_ta_A R)" "λt. (snd t, fst t)"] eps
symmetry_in_G_D[of R] rules unfolding ta_states_def trs_to_ta_B_def ta.make_def
by (simp add: r_states_def)
qed
lemma conv_adpvars_G:
assumes "ground s" and "s ⊴ t ∧ t ∈ TRS_terms R"
shows "Some s ∈ ta_res (trs_to_ta_A R) (adapt_vars s)"
using assms
proof (induction s)
case (Fun f ss)
have 0: "∀i < length ss. (map (ta_res (trs_to_ta_A R)) (map adapt_vars ss)) ! i =
ta_res (trs_to_ta_A R) (adapt_vars (ss ! i))"
by simp
{ fix i
assume i: "i < length ss"
hence "ground (ss ! i)" using Fun(2) by simp
moreover have "ss ! i ⊴ t ∧ t ∈ TRS_terms R" using Fun(3)
by (meson ‹i < length ss› nth_mem supteq.refl supteq.subt supteq_trans)
moreover have "adapt_vars (ss ! i) = ss ! i"
by (simp add: adapt_vars_id calculation(1))
ultimately have "Some (ss ! i) ∈ ta_res (trs_to_ta_A R) (adapt_vars (ss ! i))"
using Fun(1) i by fastforce
} note ref = this
have 1: "f (map Some ss) → Some (Fun f ss) ∈ ta_rules (trs_to_ta_A R)"
unfolding trs_to_ta_A_def cmn_ta_rules_def TRS_terms_def
by (metis (mono_tags, lifting) CollectI Fun.prems(2) TRS_terms_def ta_make_simps(1))
thus ?case
proof -
have "∀i < length ss. (map Some ss) ! i ∈ map (ta_res (trs_to_ta_A R)) (map adapt_vars ss) ! i"
using ref by simp
then show ?thesis using 1 by force
qed
qed (fastforce)
lemma conv_adpvars_D:
assumes "ground s" and "s ⊴ t ∧ t ∈ TRS_terms R"
shows "Some s ∈ ta_res (trs_to_ta_B R) (adapt_vars s)"
using assms
proof (induction s)
case (Fun f ss)
have 0: "∀i < length ss. (map (ta_res (trs_to_ta_B R)) (map adapt_vars ss)) ! i =
ta_res (trs_to_ta_B R) (adapt_vars (ss ! i))"
by simp
{ fix i
assume i: "i < length ss"
hence "ground (ss ! i)" using Fun(2) by simp
moreover have "ss ! i ⊴ t ∧ t ∈ TRS_terms R" using Fun(3)
by (meson ‹i < length ss› nth_mem supteq.refl supteq.subt supteq_trans)
moreover have "adapt_vars (ss ! i) = ss ! i"
by (simp add: adapt_vars_id calculation(1))
ultimately have "Some (ss ! i) ∈ ta_res (trs_to_ta_B R) (adapt_vars (ss ! i))"
using Fun(1) i by fastforce} note ref = this
have 1: "f (map Some ss) → Some (Fun f ss) ∈ ta_rules (trs_to_ta_B R)"
unfolding trs_to_ta_A_def cmn_ta_rules_def TRS_terms_def
by (metis (mono_tags, lifting) CollectI Fun.prems(2) cmn_ta_rules_def ta_make_simps(1) trs_to_ta_B_def)
thus ?case
proof -
have "∀i < length ss. (map Some ss) ! i ∈ map (ta_res (trs_to_ta_B R)) (map adapt_vars ss) ! i"
using ref by simp
then show ?thesis using 1 by force
qed
qed (fastforce)
lemma rstep_to_gtt_accept:
assumes "ground_trs R" "ground u" "ground v" "(u, v) ∈ rstep R"
shows "gtt_accept (trs_to_ta_A R, trs_to_ta_B R) (abs u) (abs v)"
using assms(4,3,2,1)
proof (induction rule: rstepE)
case (rstep s t C σ l r)
let ?𝒢 = "(trs_to_ta_A R, trs_to_ta_B R)"
let ?C = "adapt_vars_ctxt C"
let ?s = "adapt_vars l"
let ?t = "adapt_vars r"
have grnd_s_t: "ground l" "ground r" using rstep(3,8) unfolding ground_trs_def by fastforce+
hence 1: "Some r ∈ ta_res (trs_to_ta_A R) (adapt_vars l)"
proof -
from rstep have "(Some l, Some r) ∈ ta_eps (trs_to_ta_A R)" unfolding trs_to_ta_A_def
by (metis (mono_tags, lifting) mem_Collect_eq ta_make_simps(2))
hence s_res: "Some r ∈ ta_res (trs_to_ta_A R) (Var (Some l))" by auto
have "Some l ∈ ta_res (trs_to_ta_A R) (adapt_vars l)"
using grnd_s_t(1) rstep(3) conv_adpvars_G[of l l R]
unfolding TRS_terms_def TRS_fst_def by auto
hence loc: "Var (Some l) ∈ ta_res' (trs_to_ta_A R) (adapt_vars l)"
using ta_res_res'_inclusion[of "Some l" "trs_to_ta_A R" "adapt_vars l"] by blast
thus ?thesis using ta_res'_ta_res[OF "loc" "s_res"] by argo
qed
hence 2: "Some r ∈ ta_res (trs_to_ta_B R) (adapt_vars r)"
proof -
have t_res: "Some r ∈ ta_res (trs_to_ta_B R) (Var (Some r))"
unfolding trs_to_ta_B_def trs_to_ta_B_def using rule by simp
have "Some r ∈ ta_res (trs_to_ta_B R) (adapt_vars r)"
using grnd_s_t(2) rstep(3) conv_adpvars_D[of r r R]
unfolding TRS_terms_def TRS_snd_def by auto
hence loc: "Var (Some r) ∈ ta_res' (trs_to_ta_B R) (adapt_vars r)"
using ta_res_res'_inclusion[of "Some r" "trs_to_ta_B R" "adapt_vars r"] by blast
thus ?thesis using ta_res'_ta_res[OF "loc" "t_res"] by argo
qed
with 1 have IH: "gtt_accept (trs_to_ta_A R, trs_to_ta_B R) (adapt_vars l) (adapt_vars r)"
by force
moreover have u_v: "u = C⟨l⟩" "v = C⟨r⟩" using grnd_s_t ground_subst_apply rstep(1,2,4,5) by metis+
ultimately have "gtt_accept' ?𝒢 (adapt_vars u) (adapt_vars v)"
proof -
have loc: "?C⟨?s⟩ = adapt_vars u" "?C⟨?t⟩ = adapt_vars v"
using u_v by simp_all
moreover have "fill_holes (mctxt_of_ctxt ?C) [?s] = ?C⟨?s⟩"
"fill_holes (mctxt_of_ctxt ?C) [?t] = ?C⟨?t⟩"
using fill_holes_mctxt_of_ctxt by blast+
ultimately show ?thesis
using accept'_closed_ctxt[of "[adapt_vars l]" "[adapt_vars r]" "?𝒢"
"mctxt_of_ctxt (adapt_vars_ctxt C)"]
IH
by (simp add:loc gtt_accept_equiv)
qed
thus ?thesis using gtt_accept_equiv by blast
qed
lemma ground_rstep_domain:
assumes "ground_trs R" "(a, b) ∈ (rstep R)" "ground b"
shows "ground a"
using assms(2,1,3)
proof (induction rule: rstepE)
case (rstep s t C σ l r)
have grnd: "ground l" "ground r" using rstep(3,6) unfolding ground_trs_def by fast+
have "a = C⟨l⟩" " b = C⟨r⟩"
using rstep(1,4) ground_subst_apply[OF grnd(1)] apply presburger
using rstep(2,5) ground_subst_apply[OF grnd(2)] by presburger
then show ?case using rstep(7) grnd
using ground_ctxt_apply by blast
qed
lemma rstep_trancl_to_gtt_trancl:
assumes "ground_trs R"
shows "Restr (abs_R ((rstep R)⇧*)) {t. ground t}
⊆ gtt_lang (GTT_trancl (trs_to_ta_A R, trs_to_ta_B R))"
proof -
{ fix s t
assume asm: "(s, t) ∈ (Restr (abs_R ((rstep R)⇧*)) {t. ground t})"
hence grnd: "ground s" "ground t" by blast+
define u v where u_v: "u = rep s" "v = rep t"
moreover then have rep: "(u, v) ∈ (rstep R)⇧*"
by (smt IntE Pair_inject adapt_vars_reverse asm grnd(1) grnd(2) imageE prod.collapse)
hence grnd': "ground u" "ground v" using grnd unfolding u_v by force+
have "(abs u, abs v) ∈ (gtt_lang (trs_to_ta_A R, trs_to_ta_B R))⇧*"
using rep grnd' assms(1)
proof (induction u v rule:rtrancl.induct)
case (rtrancl_refl a)
then show ?case by blast
next
case (rtrancl_into_rtrancl a b c)
hence grnd: "ground b" using ground_rstep_domain[of R b c] by fast
hence "(GTT_TRS.abs a, GTT_TRS.abs b) ∈ (gtt_lang (trs_to_ta_A R, trs_to_ta_B R))⇧*"
using rtrancl_into_rtrancl(3,4,6) by blast
moreover have "(GTT_TRS.abs b, GTT_TRS.abs c)
∈ (gtt_lang (trs_to_ta_A R, trs_to_ta_B R))"
using grnd rtrancl_into_rtrancl(2,5,6) rstep_to_gtt_accept[of R b c]
by auto
ultimately show ?case
by (meson rtrancl.rtrancl_into_rtrancl)
qed
hence "(s, t) ∈ (gtt_lang (trs_to_ta_A R, trs_to_ta_B R))⇧*"
using u_v
by (simp add: u_v(1) u_v(2) grnd(1) grnd(2))
moreover have "(s, t) ∈ {t. ground t} × {t. ground t}"
using grnd by blast
ultimately have "(s, t) ∈ Restr ((gtt_lang (trs_to_ta_A R, trs_to_ta_B R))⇧*) {t. ground t}"
by blast
}
then have "Restr (abs_R ((rstep R)⇧*)) {t. ground t}
⊆ Restr ((gtt_lang (trs_to_ta_A R, trs_to_ta_B R))⇧*) {t. ground t}"
by blast
then show ?thesis
using GTT_trancl_lang[of "(trs_to_ta_A R, trs_to_ta_B R)"]
by (simp add: Restr_rtrancl_gtt_lang_eq_trancl_gtt_lang)
qed
lemma Some_ta_res:
assumes "q ∈ ta_res (trs_to_ta_A R) s" "ground_trs R" "ground s"
shows "∃p. q = Some p"
using assms
proof (induction s arbitrary: q)
case (Var x)
then show ?case by simp
next
case (Fun f ss)
then obtain q' qs where q'_qs: "f qs → q' ∈ ta_rules (trs_to_ta_A R)"
"(q', q) ∈ (ta_eps (trs_to_ta_A R))⇧*"
"length qs = length ss"
"∀i < length ss. qs ! i ∈ map (ta_res (trs_to_ta_A R)) ss ! i"
by auto
then have "∃p'. q' = Some p'" unfolding trs_to_ta_A_def
by (smt CollectD cmn_ta_rules_def ta_make_simps(1) ta_rule.inject)
then show ?case using q'_qs(2) unfolding trs_to_ta_A_def
by (smt CollectD Pair_inject rtranclE ta_make_simps(2))
qed
lemma Some_ta_res_D:
assumes "q ∈ ta_res (trs_to_ta_B R) s" "ground_trs R" "ground s"
shows "∃p. q = Some p"
using assms
proof (induction s arbitrary: q)
case (Var x)
then show ?case by simp
next
case (Fun f ss)
then obtain q' qs where q'_qs: "f qs → q' ∈ ta_rules (trs_to_ta_B R)"
"(q', q) ∈ (ta_eps (trs_to_ta_B R))⇧*"
"length qs = length ss"
"∀i < length ss. qs ! i ∈ map (ta_res (trs_to_ta_B R)) ss ! i"
by auto
then have "∃p'. q' = Some p'" unfolding trs_to_ta_B_def
by (smt CollectD cmn_ta_rules_def ta_make_simps(1) ta_rule.inject)
then show ?case using q'_qs(2) unfolding trs_to_ta_B_def
by (smt CollectD Pair_inject rtranclE ta_make_simps(2))
qed
lemma ta_eps_tranclp_G:
assumes "(a, b) ∈ (ta_eps (trs_to_ta_A R))⇧+"
shows "∃l r. (a = Some l ∧ b = Some r) ∧ (l, r) ∈ R⇧+" using assms
proof (induction rule: trancl_induct)
case base
then show ?case unfolding trs_to_ta_A_def ta.make_def
by auto
next
case (step c b)
then obtain l r' where l: "a = Some l ∧ c = Some r'" "(l, r') ∈ R⇧+" by blast
then obtain r where "b = Some r ∧ (r', r) ∈ R " using step(2)
unfolding trs_to_ta_A_def make_def by auto
then show ?case using l by auto
qed
lemma ta_eps_rtraclp_G:
assumes "(Some l, Some r) ∈ (ta_eps (trs_to_ta_A R))⇧*"
shows "(l, r) ∈ R⇧*" using assms
proof (cases "Some l = Some r")
case False
hence "(Some l, Some r) ∈ (ta_eps (trs_to_ta_A R))⇧+" using assms
by (meson rtranclD)
hence "(l, r) ∈ R⇧+" using ta_eps_tranclp_G by blast
then show ?thesis by fast
qed (blast)
lemma ta_res_G_rstep:
assumes "ground_trs R" "ground s"
"Some q ∈ ta_res (trs_to_ta_A R) s"
shows "(adapt_vars s, q) ∈ (rstep R)⇧*"
using assms(3,2,1)
proof (induction s arbitrary: q)
case (Var x)
then show ?case by simp
next
case (Fun f ss)
then obtain qs q' where q'_qs: "f qs → q' ∈ ta_rules (trs_to_ta_A R)"
"(q', Some q) ∈ (ta_eps (trs_to_ta_A R))⇧*"
"length qs = length ss"
"∀i < length ss. qs ! i ∈ ta_res (trs_to_ta_A R) (ss ! i)" by auto
have grnd: "∀i < length ss. ground (ss ! i)" using Fun(3) by auto
hence "∀i < length qs. ∃x. Some x = qs ! i"
using Some_ta_res q'_qs(3,4) assms(1)
by metis
then obtain ps where ps: "qs = map Some ps"
using construct_exI'[of "length qs" "λx i. Some x = qs ! i"]
by (metis map_nth_eq_conv)
{ fix i
assume i: "i < length ss"
hence "(adapt_vars (ss ! i), ps ! i) ∈ (rstep R)⇧*"
using Fun(1) ps q'_qs(3,4) grnd assms(1) by auto }
hence "(Fun f (map adapt_vars ss), Fun f ps) ∈ (rstep R)⇧*"
by (metis (mono_tags, lifting) args_rsteps_imp_rsteps length_map nth_map ps q'_qs(3))
hence 1: "(adapt_vars (Fun f ss), Fun f ps) ∈ (rstep R)⇧*"
using Fun(3) by simp
have "f (map Some ps) → q' ∈ ta_rules (trs_to_ta_A R)"
using q'_qs(1) ps by blast
hence "q' = Some (Fun f ps)" unfolding trs_to_ta_A_def ta.make_def cmn_ta_rules_def
by fastforce
then have "(Some (Fun f ps), Some q) ∈ (ta_eps (trs_to_ta_A R))⇧*" using q'_qs(2) by argo
then have "(Fun f ps, q) ∈ R⇧*" using ta_eps_rtraclp_G by blast
with 1 show ?case
by (smt rtranclD rtrancl_trancl_trancl subset_rstep trancl_into_rtrancl trancl_mono)
qed
lemma ta_eps_tranclp_D:
assumes "(a, b) ∈ (ta_eps (trs_to_ta_B R))⇧+"
shows "∃l r. (a = Some r ∧ b = Some l) ∧ (l, r) ∈ R⇧+ " using assms
proof (induction rule: trancl_induct)
case base
then show ?case unfolding trs_to_ta_B_def ta.make_def
by auto
next
case (step c b)
then obtain r l' where l: "a = Some r ∧ c = Some l'" "(l', r) ∈ R⇧+" by blast
then obtain l where "b = Some l ∧ (l, l') ∈ R" using step(2)
unfolding trs_to_ta_B_def make_def by auto
then show ?case using l by auto
qed
lemma ta_eps_rtraclp_D:
assumes "(Some l, Some r) ∈ (ta_eps (trs_to_ta_B R))⇧*"
shows "(r, l) ∈ R⇧*" using assms
proof (cases "Some l = Some r")
case False
hence "(Some l, Some r) ∈ (ta_eps (trs_to_ta_B R))⇧+" using assms
by (meson rtranclD)
hence "(r, l) ∈ R⇧+" using ta_eps_tranclp_D by blast
then show ?thesis by fast
qed (blast)
lemma ta_res_D_rstep:
assumes "ground_trs R" "ground t"
"Some q ∈ ta_res (trs_to_ta_B R) t"
shows "(q, adapt_vars t) ∈ (rstep R)⇧*"
using assms(3,2,1)
proof (induction t arbitrary: q)
case (Var x)
then show ?case by simp
next
case (Fun f ts)
then obtain qs q' where q'_qs: "f qs → q' ∈ ta_rules (trs_to_ta_B R)"
"(q', Some q) ∈ (ta_eps (trs_to_ta_B R))⇧*"
"length qs = length ts"
"∀i < length ts. qs ! i ∈ ta_res (trs_to_ta_B R) (ts ! i)" by auto
have grnd: "∀i< length ts. ground (ts ! i)" using Fun(3) by auto
hence "∀i < length qs. ∃x. Some x = qs ! i"
using Some_ta_res_D[of "qs ! i" R "ts ! i" for i] q'_qs(3,4) assms(1)
by metis
then obtain ps where ps: "qs = map Some ps"
using construct_exI'[of "length qs" "λ x i. Some x = qs ! i"]
by (metis map_nth_eq_conv)
{ fix i
assume i: "i < length ts"
hence "(ps ! i, adapt_vars (ts ! i)) ∈ (rstep R)⇧*"
using Fun(1) ps q'_qs(3,4) grnd assms(1) by auto }
hence "(Fun f ps, Fun f (map adapt_vars ts)) ∈ (rstep R)⇧*"
by (metis (mono_tags, lifting) args_rsteps_imp_rsteps length_map nth_map ps q'_qs(3))
hence 1: "(Fun f ps, adapt_vars (Fun f ts)) ∈ (rstep R)⇧*"
using Fun(3) by simp
have "(f (map Some ps) → q') ∈ ta_rules (trs_to_ta_B R)"
using q'_qs(1) ps by blast
hence "q' = Some (Fun f ps)" unfolding trs_to_ta_B_def ta.make_def cmn_ta_rules_def
by fastforce
then have "(Some (Fun f ps), Some q) ∈ (ta_eps (trs_to_ta_B R))⇧*" using q'_qs(2) by argo
then have "(q, Fun f ps) ∈ R⇧*" using ta_eps_rtraclp_D by blast
with 1 show ?case
by (smt rtranclD rtrancl_trancl_trancl subset_rstep trancl_into_rtrancl trancl_mono)
qed
lemma gtt_accept_to_rstep_rtrancl:
assumes "ground_trs R" "ground u" "ground v"
"gtt_accept (trs_to_ta_A R, trs_to_ta_B R) u v"
shows "(rep u, rep v) ∈ (rstep R)⇧*"
using assms(4,3,2,1)
proof (induction rule:gtt_accept.induct)
case (refl t)
then show ?case by force
next
case (join q s t)
obtain p where p: "Some p = q"
using Some_ta_res[of q R s] join(1,4,5) unfolding fst_conv by blast
then have "(adapt_vars s, p) ∈ (rstep R)⇧*"
using ta_res_G_rstep[of R s p] join(1,4,5)
unfolding fst_conv by blast
moreover have "(p, adapt_vars t) ∈ (rstep R)⇧*"
using ta_res_D_rstep[of R t p] join(2,3,5) p
unfolding snd_conv by blast
ultimately show ?case by fastforce
next
case (ctxt ss ts f)
have ad_Fun: "adapt_vars (Fun f ss) = Fun f (map adapt_vars ss)"
"adapt_vars (Fun f ss) = Fun f (map adapt_vars ss)"
using ctxt(4,5) by simp+
{ fix i
assume i: "i < length ss"
with ctxt have "gtt_accept (trs_to_ta_A R, trs_to_ta_B R) (ss ! i) (ts ! i)"
by (auto elim:gtt_accept.cases)
moreover have "ground (ss ! i) ∧ ground (ts ! i)" using i ctxt(1,3,4) by force
ultimately have "(adapt_vars (ss ! i), adapt_vars (ts ! i)) ∈ (rstep R)⇧*"
using ctxt(2,5) i by blast }
with ad_Fun show ?case
using args_rsteps_imp_rsteps[of "map adapt_vars ss" "map adapt_vars ts" R f]
by (simp add: ctxt.hyps)
qed
lemma abs_R_rtrancl:
assumes "ground a" "ground b" "ground c" "(a, b) ∈ abs_R (R⇧*)" "(b, c) ∈ abs_R (R⇧*)"
shows "(a, c) ∈ abs_R (R⇧*)"
proof -
obtain a' b' c' where obt: "a = abs a'" "b = abs b'" "c = abs c'"
using assms by blast
then have "(a', b') ∈ R⇧*" using assms(1,2,4)
by (smt adapt_vars_reverse fst_conv image_iff relcompE rtrancl_idemp_self_comp snd_conv)
moreover have "(b', c') ∈ R⇧*" using assms(2,3,5) obt(2,3)
by (smt adapt_vars_reverse fst_conv image_iff relcompE rtrancl_idemp_self_comp snd_conv)
ultimately have "(a', c') ∈ R⇧*" by fastforce
then show ?thesis using obt(1,3)
by (metis (mono_tags, lifting) fst_conv obt(1) obt(3) rev_image_eqI snd_conv)
qed
lemma gtt_lang_to_rstep_rtrancl:
assumes "ground_trs R"
shows "gtt_lang (GTT_trancl (trs_to_ta_A R, trs_to_ta_B R)) ⊆ Restr (abs_R ((rstep R)⇧*)) {t. ground t}"
proof -
have "Restr ((gtt_lang (trs_to_ta_A R, trs_to_ta_B R))⇧*) {t. ground t}
⊆ Restr (abs_R ((rstep R)⇧*)) {t. ground t}"
proof -
{ fix u v
assume asm: "(u, v) ∈ Restr ((gtt_lang (trs_to_ta_A R, trs_to_ta_B R))⇧*) {t. ground t}"
then have grnd: "ground u" "ground v" by blast+
moreover have u_v: "(u, v) ∈ (gtt_lang (trs_to_ta_A R, trs_to_ta_B R))⇧*"
using asm by fast
have "(u, v) ∈ abs_R ((rstep R)⇧*)"
using u_v grnd assms
proof (induction u v rule: rtrancl.induct)
case (rtrancl_refl a)
hence "abs (rep a) = a" by auto
moreover have "(rep a, rep a) ∈ (rstep R)⇧*" by blast
ultimately show ?case
by (metis (mono_tags, lifting) fst_conv rev_image_eqI snd_conv)
next
case (rtrancl_into_rtrancl a b c)
then have grnd_b: "ground b" by force
hence 1: "(a, b) ∈ abs_R ((rstep R)⇧*)"
using rtrancl_into_rtrancl(3,4,5,6) by fast
have "(rep b, rep c) ∈ (rstep R)⇧*"
using grnd_b rtrancl_into_rtrancl(2,5,6) gtt_accept_to_rstep_rtrancl by blast
hence "(b, c) ∈ abs_R ((rstep R)⇧*)"
using grnd_b rtrancl_into_rtrancl(5)
by (smt adapt_vars_adapt_vars fst_conv rev_image_eqI snd_conv)
with 1 show ?case using abs_R_rtrancl rtrancl_into_rtrancl(4,5) grnd_b by blast
qed
hence "(u, v) ∈ Restr (abs_R ((rstep R)⇧*)) {t. ground t}"
using grnd by blast }
thus ?thesis by blast
qed
thus ?thesis using GTT_trancl_lang[of "(trs_to_ta_A R, trs_to_ta_B R)"]
by (simp add: Restr_rtrancl_gtt_lang_eq_trancl_gtt_lang)
qed
lemma reachability_gtt_equiv:
assumes "ground_trs R"
shows "gtt_lang (GTT_trancl (trs_to_ta_A R, trs_to_ta_B R))
= Restr (abs_R ((rstep R)⇧*)) {t. ground t}"
using gtt_lang_to_rstep_rtrancl[OF assms] rstep_trancl_to_gtt_trancl[OF assms]
by auto
end