theory LV_to_GTT
imports Main TRS_GTT
begin
lemma subst_unification:
assumes "vars_term s ∩ vars_term t = {}"
obtains μ where "s ⋅ σ = s ⋅ μ" "t ⋅ τ = t ⋅ μ"
using assms
by (auto intro!: that[of "λx. if x ∈ vars_term s then σ x else τ x"] simp: term_subst_eq_conv)
lemma subst_unification_list:
assumes "is_partition (map vars_term ss)" "length μs = length ss"
shows "∃σ. ∀i < length ss. (ss!i) ⋅ (μs!i) = (ss!i) ⋅ σ"
using assms
proof (induction ss arbitrary: μs)
case (Cons s ss)
then have "is_partition (map vars_term ss)"
by (simp add: Cons.IH is_partition_Cons)
then show ?case using Cons
proof (cases ss)
case (Cons s' ss')
then have len1:"length ss > 0" by simp
define μ where μ:"μ = μs!0"
define μs' where μs': "μs' = tl μs"
then have len2:"length μs' = length ss" using Cons.prems(2) by simp
with μ μs' len1 have μs:"μs = μ # (μs')"
by (metis Cons.prems(2) hd_Cons_tl length_0_conv list.simps(3) nth_Cons_0)
then obtain σ' where σ':"∀i<length ss. ss ! i ⋅ (μs' ! i) = ss ! i ⋅ σ' "
using Cons.IH ‹is_partition (map vars_term ss)› len2 by blast
define σ where "σ = (λx. if x ∈ vars_term s then (μ x) else σ' x)"
then have " ∀i<length (s # ss). (s # ss) ! i ⋅ ((μ# μs') ! i) = (s # ss) ! i ⋅ σ "
using len1 Cons.prems term_subst_eq_conv
unfolding is_partition_def σ'
by (smt IntI σ' empty_iff length_Cons length_map less_Suc_eq_0_disj neq0_conv nth_Cons' nth_Cons_Suc nth_map)
then show ?thesis unfolding μs by blast
qed (auto)
qed (auto)
definition lv_trs :: "('f, 'v) trs ⇒ bool" where
"lv_trs R ≡ ∀(l, r) ∈ R. linear_term l ∧ linear_term r ∧ (vars_term l ∩ vars_term r = {})"
locale fixed_signature =
fixes ℱ :: "('f × nat) set"
begin
definition signed_term :: "('f,'v) term ⇒ bool" where
st_def: "signed_term s ⟷ funas_term s ⊆ ℱ"
lemma funas_term_subset:
assumes "s = t ⋅ σ"
shows "funas_term t ⊆ funas_term s" using assms
using funas_term_subst by blast
lemma funas_term_ctxt:
assumes "s = C⟨t⟩"
shows "funas_term t ⊆ funas_term s" using assms
by (simp add: assms)
definition embed_term :: "('f,'v) term ⇒ ('f, unit) term" where
"embed_term T = map_vars_term (const ()) T"
lemma embed_inv:
assumes "Fun f ss = embed_term t"
shows "∃ts. t = Fun f ts ∧ ss = map embed_term ts"
using assms unfolding embed_term_def
by (smt Term.term.simps(10) map_vars_term_as_subst subst_apply_term.elims term.distinct(1) term.inject(2))
lemma funas_term_embed:
"funas_term (adapt_vars (embed_term t)) = funas_term t"
by (simp add: adapt_vars_def embed_term_def)
definition embed_ctxt :: "('f,'q)ctxt ⇒ ('f,unit)ctxt" where
"embed_ctxt = map_vars_ctxt (const ())"
lemma embed_subterm:
assumes "s ⊴ t" shows "embed_term s ⊴ embed_term t"
unfolding embed_term_def
by (simp add: assms map_vars_term_as_subst)
definition embed_TRS :: "('f,'v) trs ⇒ ('f, unit) trs" where
"embed_TRS R = (λ(l,r). (map_vars_term (const ()) l, (map_vars_term (const ()) r))) ` R"
definition term_TA :: "('f,'v) term ⇒ (('f, unit) term option, 'f) ta_rule set" where
"term_TA t = ({(f (map Some ts) → Some (Fun f ts))|f ts. Fun f ts ⊴ (embed_term t)})"
definition term_to_ta :: "('f, 'v) term ⇒ (('f, unit) term option, 'f) ta" where
"term_to_ta t = ta.make ({Some (embed_term (t::('f, 'v) term))})
(((term_TA t) ∪ {g (replicate n (Some (Var ()))) → Some (Var ()) |g n. (g, n) ∈ ℱ}))
{}"
lemma ta_rules_Some:
assumes "(f qs → q) ∈ ta_rules (term_to_ta t)"
shows "∃v. q = Some v"
using assms unfolding term_to_ta_def term_TA_def by auto
lemma ta_rules_Some_conv:
assumes "(f qs → Some t) ∈ ta_rules (term_to_ta (l::('f,'v) term))"
shows "∃ qs'. qs = map Some qs'"
using assms
proof -
have "(f qs → Some t) ∈ (term_TA l)
∨ ((f qs → Some t) ∈ {g (replicate n (Some (Var ()))) → Some (Var ()) |g n. (g, n) ∈ ℱ})"
using assms unfolding term_to_ta_def by auto
thus ?thesis
proof (rule disjE, goal_cases left right)
case left
then show ?case unfolding term_TA_def
by fast
next
case right
then show ?case unfolding replicate.simps
by (smt map_replicate mem_Collect_eq ta_rule.inject)
qed
qed
lemma ground_res:
assumes "ground s" "signed_term s"
shows "Some (Var ()) ∈ ta_res (term_to_ta t) (adapt_vars (embed_term s))"
using assms
proof (induction s)
case (Fun f ss)
{
fix i
assume i:"i < length ss"
hence "ground (ss!i)" using Fun.prems by auto
moreover have "signed_term (ss!i)" using Fun(3) i by (fastforce simp: st_def set_conv_nth)
ultimately have "Some (Var ()) ∈ ta_res (term_to_ta t) (adapt_vars (embed_term (ss!i)))"
using Fun.IH using i by force
} note ind = this
hence concl:"∀i<length ss.
(replicate (length ss) (Some (Var ()))) ! i
∈ ta_res (term_to_ta t)
(adapt_vars (embed_term (ss !i)))" using ind unfolding embed_term_def using replicate.simps
by simp
have repl:"f (replicate (length ss) (Some (Var ()))) → Some (Var ())
∈ {g (replicate n (Some (Var ()))) → Some (Var ()) |g n. (g, n) ∈ ℱ}"
proof -
have "(f, length ss) ∈ ℱ"
using Fun.prems(2) by (simp add: st_def)
show ?thesis
using ‹(f, length ss) ∈ ℱ› by blast
qed
hence "f (replicate (length ss) (Some (Var ()))) → Some (Var ()) ∈ ta_rules (term_to_ta t)"
unfolding term_to_ta_def by force
then show ?case using concl
using ta_res.simps(2) unfolding ta_res.simps embed_term_def term.map adapt_vars_simps
unfolding length_map map_map comp_def term.map_comp const_def
by force
qed (auto)
lemma ta_eps_refl:
assumes "(s,t) ∈ ta_eps (term_to_ta p)" "t ≠ Some (Var ())"
shows "s = t"
using assms unfolding term_to_ta_def by fastforce
lemma ta_rules_refl:
assumes "(g ss → Some (Fun f ts)) ∈ ta_rules (term_to_ta p)"
shows "g = f" "ss = (map Some ts)"
using assms unfolding term_to_ta_def term_TA_def by force+
assumes"ground t"shows"ground (embed_term t)"unfoldingembed_term_def ">lemma assumes "ground t" shows "ground (embed_term t)" unfolding embed_term_def
by (simp add: assms)
lemma embed:
assumes "ground s" "embed_term s ⊴ embed_term t"
shows "Some (embed_term s) ∈ ta_res (term_to_ta t) (adapt_vars (embed_term s))"
using assms
proof (induction s)
case (Fun f ss)
have "Fun f (map embed_term ss) ⊴ embed_term (Fun f ss)" using Fun(2) unfolding embed_term_def
by simp
hence trans:"Fun f (map embed_term ss) ⊴ embed_term t" using Fun(2,3) using subterm.order.trans by blast
{
fix i
assume i:"i < length ss"
hence grnd_i:"ground (ss!i)" using Fun(2) by fastforce
from i Fun.prems(2) have "embed_term (ss!i) ⊴ embed_term t"
by (metis arg_subteq length_map local.trans nth_map nth_mem subterm.order.trans)
with i grnd_i have "Some (embed_term (ss!i)) ∈ ta_res (term_to_ta t) (adapt_vars (embed_term (ss!i)))"
using Fun by force
} note ind = this
moreover have
"(f (map Some (map embed_term ss)) → Some (Fun f (map embed_term ss))) ∈ ta_rules (term_to_ta t)" using Fun(3) trans
unfolding term_to_ta_def term_TA_def by force
hence "(f (map Some (map embed_term ss)) → Some (embed_term (Fun f ss))) ∈ ta_rules (term_to_ta t)"
using Fun(2) embed_term_def
by (metis Term.term.simps(10) map_eq_conv')
then show ?case using ind unfolding ta_res.simps embed_term_def term.map adapt_vars_simps
unfolding length_map map_map comp_def term.map_comp const_def
by force
qed (force)
lemma instance_to_lang:
assumes "linear_term (t::('f,'v) term)" "(s::('f,'v) term) = t ⋅ σ" "ground s" "signed_term s"
shows "embed_term s ∈ ta_lang (term_to_ta t)"
using assms(1,3,4,2)
proof (induction t arbitrary: s)
case (Var x)
then have 0:"ta_final (term_to_ta (Var x)) = {Some (Var ())}"
unfolding term_to_ta_def embed_term_def
by auto
have grnd:"ground (embed_term s)" using Var(2) by (simp add: embed_term_def)
have "Some (Var ()) ∈ ta_res (term_to_ta (Var x)) (adapt_vars (embed_term s))"
using ground_res[OF Var(2,3)].
then have "ta_final (term_to_ta (Var x)) ∩ ta_res (term_to_ta (Var x)) (adapt_vars (embed_term s)) ≠ {}"
using 0 by blast
then show ?case using grnd 0 unfolding ta_lang_def
by (smt adapt_vars_adapt_vars ground_adapt_vars mem_Collect_eq)
next
case (Fun g ts)
have signed: "signed_term (Fun g ts)" using funas_term_subset[OF Fun(5)] unfolding st_def
using Fun.prems(3) st_def by auto
define TA where TA:" TA = (term_to_ta (Fun g ts))"
then have 0:"ta_final (term_to_ta (Fun g ts)) = {Some (embed_term (Fun g ts))}"
unfolding term_to_ta_def embed_term_def
by (meson ta_make_simps(3))
define ss where ss:"ss= (map (λi.(i ⋅ σ)) ts)"
then have s:"s = Fun g ss" using Fun(5) by auto
{
fix i
assume i:"i < length ts"
have st:"signed_term (ss!i)" using Fun(4) i unfolding s st_def
using ss by fastforce
hence ss':"(ss!i) = (ts!i) ⋅ σ" using Fun(4) ss i by auto
hence grnd:"ground (ss!i)" using s i ss' Fun(3)
by (metis ground_recur length_map ss)
{ fix f ps
assume asm:"(Fun f ps) ⊴ (ts!i)"
hence "f (map (Some∘embed_term) ps) → Some (Fun f (map embed_term ps))
∈ ta_rules TA"
proof -
have "Fun f (map embed_term ps) ⊴ embed_term (ts!i)" using embed_subterm[OF asm]
by (metis Term.term.simps(10) embed_term_def map_eq_conv)
then show ?thesis unfolding TA term_to_ta_def term_TA_def TA
by (smt Term.term.simps(10) UnI1 embed_term_def i length_map map_map mem_Collect_eq nth_map nth_mem supteq.subt ta_make_simps(1))
qed
} note int = this
have "Some (embed_term (ts!i)) ∈ ta_res TA (adapt_vars (embed_term (ss!i)))"
using ss ss' grnd int st
proof (induction "ts!i" arbitrary: "ss" "ts" "i")
case (Var x)
hence 0:"embed_term (ts!i) = Var ()" unfolding embed_term_def by force
then show ?case using ground_res[OF Var(4) Var(6)] Var(1)
by (simp add: "0" Var.hyps ‹⋀t. Some (Var ()) ∈ ta_res (term_to_ta t) (adapt_vars (embed_term (ss ! i)))› TA)
next
case (Fun f ps)
then obtain qs where qs:"ss!i = Fun f qs" using Fun(2)
by (metis subst_apply_term.simps(2))
then have len:"length qs = length ps"
by (metis Fun.hyps(2) ‹ss ! i = ts ! i ⋅ σ› weak_match.simps(3) weak_match_match)
have loc_int:"f (map (Some∘embed_term) ps) → Some (Fun f (map embed_term ps))
∈ ta_rules TA"
using Fun(6)
by (simp add: Fun.hyps(2))
{
fix j
assume j:"j < length ps"
hence j_subst:"(qs!j) = (ps!j) ⋅ σ" using Fun qs len
by (metis Fun.hyps(2) map_nth_eq_conv subst_apply_term.simps(2) term.sel(4))
hence qs_j:"signed_term (qs ! j)" using j qs Fun(6)
by (smt Fun.prems(5) UN_I basic_trans_rules(31) funas_term_args len nth_mem st_def subsetI term.sel(4))
have "⋀ h psa. ps ! j ⊵ Fun h psa
⟹ h map (Some ∘ embed_term) psa → Some (Fun h (map embed_term psa))∈ ta_rules TA "
using Fun(2) Fun(6) j
by (metis nth_mem supteq.subt)
hence "Some (embed_term (ps ! j)) ∈ ta_res TA (adapt_vars (embed_term (qs ! j)))"
using Fun(1)[of ps j qs] Fun(6) j_subst qs_j
by (metis Fun.hyps(2) Fun.prems(2) Fun.prems(3) ground_recur j len nth_mem qs subst_apply_term.simps(2) term.inject(2))
} note ind= this
then have "Some (embed_term (Fun f ps)) ∈ ta_res TA (adapt_vars (embed_term (Fun f qs)))"
using len loc_int
unfolding ta_res.simps embed_term_def term.map adapt_vars_simps
unfolding length_map map_map comp_def term.map_comp const_def
by (smt length_map mem_Collect_eq nth_map rtrancl.intros(1))
then show ?case using Fun(2) qs by argo
qed
}
then have ind1:"(length ts = length ss) ∧
(∀ i < length ss. Some (embed_term (ts ! i))
∈ ((map (ta_res (term_to_ta (Fun g ts)))
(map (adapt_vars∘embed_term) ss)) ! i))" using ss
using TA by auto
have ind2:"(g (map Some (map embed_term ts)) → Some (Fun g (map embed_term ts)))
∈ ta_rules (term_to_ta (Fun g ts))"
proof -
have "(Fun g (map embed_term ts)) ⊴ embed_term (Fun g ts)" unfolding embed_term_def by auto
then show ?thesis unfolding term_TA_def term_to_ta_def by force
qed
moreover have "Fun g (map embed_term ts) = embed_term (Fun g ts)"
by (simp add: embed_term_def)
ultimately have temp:"(g (map Some (map embed_term ts)) → Some (embed_term (Fun g ts)))
∈ ta_rules (term_to_ta (Fun g ts))"
by argo
have temp2:"(Some (embed_term (Fun g ts)) , Some (embed_term (Fun g ts))) ∈ (ta_eps (term_to_ta (Fun g ts)))^*"
by simp
have "Some (embed_term (Fun g ts))
∈ ta_res (term_to_ta (Fun g ts)) (adapt_vars (embed_term (Fun g ss)))"
using ind1 temp temp2
unfolding ta_res.simps embed_term_def term.map adapt_vars_simps
unfolding length_map map_map comp_def term.map_comp const_def
by force
hence "(ta_res (term_to_ta (Fun g ts)) (adapt_vars (embed_term (Fun g ss))))
∩ (ta_final (term_to_ta (Fun g ts))) ≠ {}" using 0 by auto
moreover have "ground (embed_term (Fun g ss))" using s Fun(3) unfolding embed_term_def
by force
ultimately show ?case unfolding ta_lang_def s
by (smt adapt_vars_adapt_vars ground_adapt_vars inf_commute mem_Collect_eq)
qed
lemma lang_to_instance_0:
fixes s t :: "('f,'v) term"
assumes "linear_term t" "ground s" "t ⊴ t'" "Some (embed_term t) ∈ ta_res (term_to_ta t') (adapt_vars (embed_term s))"
shows "∃σ. s = t ⋅ σ"
using assms
proof (induction t arbitrary: s)
case (Fun f ts)
obtain g ss where s:"s = Fun g ss" using Fun(3)
using ground.elims(2) by metis
define TA where TA:"TA = (term_to_ta t')"
have "ta_final TA= {Some (embed_term t')}"
unfolding term_to_ta_def TA
by force
have Some: "Some (embed_term (Fun f ts)) ∈ (ta_res TA (adapt_vars (embed_term s)))" using Fun(5) unfolding TA by auto
obtain q qs where q_qs:
"(g qs → q) ∈ ta_rules TA ∧
(q, Some (embed_term (Fun f ts))) ∈ ((ta_eps TA)^*) ∧
length qs = length ss ∧
(∀ i < length ss. qs ! i ∈ (map (ta_res TA) (map adapt_vars (map embed_term ss))) ! i)"
using ta_res.simps(2)[of TA g "(map adapt_vars (map embed_term ss))"] Some
unfolding embed_term_def s
unfolding ta_res.simps embed_term_def term.map adapt_vars_simps
unfolding length_map map_map comp_def term.map_comp const_def
by blast
then have q:"q = Some (embed_term (Fun f ts))"
unfolding TA term_to_ta_def by simp
then have qs:"qs = (map Some (map embed_term ts))" "f = g" unfolding TA using ta_rules_refl
apply (smt TA Term.term.simps(10) embed_term_def map_eq_conv q_qs)
by (smt TA Term.term.simps(10) ‹⋀thesis. (⋀q qs. g qs → q ∈ ta_rules TA ∧ (q, Some (embed_term (Fun f ts))) ∈ (ta_eps TA)⇧* ∧ length qs = length ss ∧ (∀i<length ss. qs ! i ∈ map (ta_res TA) (map adapt_vars (map embed_term ss)) ! i) ⟹ thesis) ⟹ thesis› embed_term_def pair_in_Id_conv rtrancl_empty ta_make_simps(2) ta_rules_refl(1) term_to_ta_def)
with q_qs
have rec:"(∀ i < length ss. (map Some (map embed_term ts)) ! i ∈
(map (ta_res TA) (map adapt_vars (map embed_term ss))) ! i)" by blast
have len_eq: "length ss = length ts" using qs q_qs by force
{ fix i
assume i:"i < length ts"
have lin:"linear_term (ts!i)" using Fun(2)
using i by auto
have grd:"ground (ss!i)"
using Fun.prems(2) i len_eq s by auto
have st:"(ts!i) ⊴ t'" using Fun(4) i
by (meson arg_subteq nth_mem supteq_trans)
then have res:"(map Some (map embed_term ts)) ! i ∈
(map (ta_res TA) (map adapt_vars (map embed_term ss))) ! i"
using len_eq rec i by presburger
then have "(Some (embed_term (ts!i))) ∈ (ta_res TA (adapt_vars (embed_term (ss!i))))"
using map_map i
by (simp add: len_eq)
with lin grd st i have "∃σ⇩i.(ss ! i) = (ts!i) ⋅ σ⇩i"
using Fun.IH using TA nth_mem by blast
} note * = this
then obtain σs where σs:"length σs = length ts" "∀i < length ts. (ss ! i) = (ts!i) ⋅ (σs!i)"
using construct_exI'[of "length ts" "λ σ⇩i i. (ss!i) = (ts!i) ⋅ σ⇩i"]
by blast
have is_par:"is_partition (map vars_term ts)" using Fun(2) by simp
then obtain σ where "∀i < length ts. (ss!i) = (ts!i) ⋅ σ"
using subst_unification_list[of "ts" "σs"] σs(1,2)
by presburger
hence "s = (Fun f ts) ⋅ σ" using s qs(2) len_eq
by (metis map_nth_eq_conv subst_apply_term.simps(2))
then show ?case by auto
qed (auto)
lemma lang_to_instance:
assumes "ground s" "linear_term (t::('f,'v) term)" "(embed_term s) ∈ ta_lang (term_to_ta t)" "signed_term s"
shows "∃σ. (s :: ('f,'v) term) = t ⋅ σ"
proof -
have "Some (embed_term t) ∈ ta_res (term_to_ta t) (adapt_vars (embed_term s))"
using assms(3) by (auto elim!: ta_langE2 simp: term_to_ta_def)
then show ?thesis using lang_to_instance_0[of t s t] assms
by blast
qed
definition term_to_ta_L::"('f, 'v) term ⇒ (('f, unit) term + ('f, unit) term, 'f) ta" where
"term_to_ta_L t = fmap_states_ta (λx.(case x of Some y ⇒ Inl y| None ⇒ Inr (Var ()))) (term_to_ta t)"
lemma inj_on_states:
shows "inj_on (λx.(case x of Some y ⇒ Inl y| None ⇒ Inr (Var ()))) (ta_states (term_to_ta t))"
proof -
let ?map = "(λx.(case x of Some y ⇒ Inl y|None ⇒ Inr (Var ())))"
{ fix x y
assume xy:"x ∈ta_states (term_to_ta t)" "y ∈ta_states (term_to_ta t)"
hence "?map x = ?map y ⟶ x = y"
by (cases x, cases y, simp, simp, simp add: option.case_eq_if) }
thus ?thesis unfolding inj_on_def term_to_ta_def by fast
qed
lemma ta_rules_Inl_eq:
"ta_rules (term_to_ta_L (l::('f,'v) term)) = ({(f (map Inl ts) → Inl (Fun f ts)) |f ts. Fun f ts ⊴ (embed_term l)})
∪ {g1 (replicate n1 (Inl (Var ()))) → Inl (Var ()) |g1 n1. (g1, n1) ∈ ℱ}"
proof -
let ?g = "(λx.(case x of Some y ⇒ Inl y| None ⇒ Inr (Var ())))"
let ?rep_rule = "λr. case r of g qs → q ⇒ g (map ?g qs) → ?g q"
{ fix f ts
assume subt: "Fun f ts ⊴ (embed_term l)"
have "?rep_rule (f (map Some ts) → Some (Fun f ts)) = (f (map Inl ts) → Inl (Fun f ts))"
by simp }
hence 1:"?rep_rule ` ({(f (map Some ts) → Some (Fun f ts))|f ts. Fun f ts ⊴ (embed_term l)})
= ({(f (map Inl ts) → Inl (Fun f ts))|f ts. Fun f ts ⊴ (embed_term l)})"
by (smt Collect_cong setcompr_eq_image)
{ fix g1 n1
assume "(g1,n1) ∈ ℱ"
have "?rep_rule (g1 (replicate n1 (Some (Var ()))) → Some (Var ()))
= (g1 (replicate n1 (Inl (Var ()))) → Inl (Var ()))"
by simp }
hence 2:"?rep_rule ` {g1 (replicate n1 (Some (Var ()))) → Some (Var ()) |g1 n1. (g1, n1) ∈ ℱ}
= {g1 (replicate n1 (Inl (Var ()))) → Inl (Var ()) |g1 n1. (g1, n1) ∈ ℱ}"
using Collect_cong setcompr_eq_image
by (smt option.simps(5) ta_rule.case)
have "ta_rules (term_to_ta_L l) = ?rep_rule ` (ta_rules (term_to_ta l))"
using ta_rules_Some_conv unfolding term_to_ta_L_def fmap_states_ta_def by simp
then show ?thesis unfolding term_to_ta_def term_TA_def
by (simp add: 1 2 image_Un)
qed
lemma ta_rules_Inl_conv:
assumes "(f qs → Inl t) ∈ ta_rules (term_to_ta_L (l::('f,'v) term))"
shows "∃ qs'. qs = map Inl qs'"
proof -
let ?g = "(λx.(case x of Some y ⇒ Inl y| None ⇒ Inr (Var ())))"
let ?rep_rule = "λr. case r of g qs → q ⇒ g (map ?g qs) → ?g q"
have "ta_rules (term_to_ta_L l) = ?rep_rule ` (ta_rules (term_to_ta l))"
using assms ta_rules_Some_conv unfolding term_to_ta_L_def fmap_states_ta_def by simp
then obtain qs'' q'' where qs'':"(qs = map ?g qs'')" "(Inl t = ?g q'')" "(f qs'' → q'') ∈ ta_rules (term_to_ta (l::('f,'v) term))"
by (smt assms imageE option.simps(5) r_sym.cases sum.inject(1) ta_rule.case ta_rule.inject ta_rules_Some)
then obtain qs''' where "qs'' = map Some qs'''" using ta_rules_Some_conv
using ta_rules_Some
by metis
hence "qs = map Inl qs'''" using qs''(1) by simp
thus ?thesis by force
qed
lemma lang_equiv_L:
"ta_lang (term_to_ta_L t) = ta_lang (term_to_ta t)"
using inj_on_states unfolding term_to_ta_L_def
by (simp add: inj_on_states fmap_ta(2))
lemma instance_to_res_L:
assumes "linear_term (t :: ('f,'v) term)" "(s :: ('f,'v) term) = t ⋅ σ" "ground s" "signed_term s"
shows "Inl (embed_term t) ∈ ta_res (term_to_ta_L t) (adapt_vars (embed_term s))"
proof -
have "adapt_vars (embed_term s) ∈ ta_lang (term_to_ta t)" using assms instance_to_lang[OF assms]
by force
hence "adapt_vars (embed_term s) ∈ ta_lang (term_to_ta_L t)" using lang_equiv_L by force
moreover have "ta_final (term_to_ta_L t) = {Inl (embed_term t)}"
unfolding term_to_ta_L_def term_to_ta_def
by (simp add: fmap_states_ta_def')
ultimately show ?thesis
unfolding ta_lang_def
by (smt ‹adapt_vars (embed_term s) ∈ ta_lang (term_to_ta_L t)› singletonD ta_langE2 ta_res_adapt_vars_ground)
qed
lemma res_to_instance_L:
assumes "linear_term (t::('f,'v) term)" "ground s"
"Inl (embed_term t) ∈ ta_res (term_to_ta_L t) (adapt_vars (embed_term s))" "signed_term s"
shows "∃σ. (s::('f,'v) term) = t ⋅ σ"
proof -
have grnd: "ground (adapt_vars (embed_term s))" unfolding embed_term_def
by (simp add: assms(2))
have "ta_final (term_to_ta_L t) = {Inl (embed_term t)}"
unfolding term_to_ta_L_def term_to_ta_def
by (simp add: fmap_states_ta_def')
moreover then have "ta_res (term_to_ta_L t) (adapt_vars (embed_term s)) ∩ (ta_final (term_to_ta_L t)) ≠ {}"
using assms(3) by simp
ultimately have " (embed_term s) ∈ ta_lang (term_to_ta_L t)" using assms(2,3) grnd
unfolding ta_lang_def
by (smt CollectI Int_commute adapt_vars_reverse)
hence "(embed_term s) ∈ ta_lang (term_to_ta t)" using lang_equiv_L
by auto
then show ?thesis using lang_to_instance[OF assms(2,1)] assms(2,4)
by argo
qed
definition term_to_ta_R :: "('f, 'v) term ⇒ (('f, unit) term + ('f, unit) term, 'f) ta" where
"term_to_ta_R t = fmap_states_ta (λx.(case x of Some y ⇒ Inr y| None ⇒ Inl (Var ()))) (term_to_ta t)"
lemma inj_on_states_R:
shows "inj_on (λx.(case x of Some y ⇒ Inr y| None ⇒ Inl (Var ()))) (ta_states (term_to_ta t))"
proof -
let ?map = "(λx.(case x of Some y ⇒ Inr y|None ⇒ Inl (Var ())))"
{ fix x y
assume xy:"x ∈ta_states (term_to_ta t)" "y ∈ta_states (term_to_ta t)"
hence "?map x = ?map y ⟶ x = y"
by (cases x, cases y, simp, simp, simp add: option.case_eq_if) }
thus ?thesis unfolding inj_on_def term_to_ta_def by fast
qed
lemma ta_final_R:
"ta_final (term_to_ta_R t) = {Inr (embed_term t)}"
unfolding term_to_ta_R_def term_to_ta_def
by (simp add: fmap_states_ta_def')
lemma ta_eps_R:
"ta_eps (term_to_ta_R t) = {}"
unfolding term_to_ta_R_def term_to_ta_def by (simp add: fmap_states_ta_def')
lemma lang_equiv_R:
"ta_lang (term_to_ta_R t) = ta_lang (term_to_ta t)"
using inj_on_states unfolding term_to_ta_R_def
by (simp add: inj_on_states_R fmap_ta(2))
lemma instance_to_res_R:
assumes "linear_term (t :: ('f,'v) term)" "(s :: ('f,'v) term) = t ⋅ σ" "ground s" "signed_term s"
shows "Inr (embed_term t) ∈ ta_res (term_to_ta_R t) (adapt_vars (embed_term s))"
proof -
have "adapt_vars (embed_term s) ∈ ta_lang (term_to_ta t)" using assms instance_to_lang[OF assms]
by force
hence "adapt_vars (embed_term s) ∈ ta_lang (term_to_ta_R t)" using lang_equiv_R by force
moreover have "ta_final (term_to_ta_R t) = {Inr (embed_term t)}"
unfolding term_to_ta_R_def term_to_ta_def
by (simp add: fmap_states_ta_def')
ultimately show ?thesis
unfolding ta_lang_def
by (smt ‹adapt_vars (embed_term s) ∈ ta_lang (term_to_ta_R t)› singletonD ta_langE2 ta_res_adapt_vars_ground)
qed
lemma ta_rules_Inr_eq:
"ta_rules (term_to_ta_R (r :: ('f,'v) term)) = {(f (map Inr ts) → Inr (Fun f ts))|f ts. Fun f ts ⊴ (embed_term r)}
∪ {g1 (replicate n1 (Inr (Var ()))) → Inr (Var ()) |g1 n1. (g1, n1) ∈ ℱ}"
proof -
let ?g = "(λx.(case x of Some y ⇒ Inr y| None ⇒ Inl (Var ())))"
let ?rep_rule = "λr. case r of g qs → q ⇒ g (map ?g qs) → ?g q"
{ fix f ts
assume subt: "Fun f ts ⊴ (embed_term r)"
have "?rep_rule (f (map Some ts) → Some (Fun f ts)) = (f (map Inr ts) → Inr (Fun f ts))"
by simp }
hence 1:"?rep_rule ` ({(f (map Some ts) → Some (Fun f ts))|f ts. Fun f ts ⊴ (embed_term r)})
= ({(f (map Inr ts) → Inr (Fun f ts))|f ts. Fun f ts ⊴ (embed_term r)})"
by (smt Collect_cong setcompr_eq_image)
{ fix g1 n1
assume "(g1,n1) ∈ ℱ"
have "?rep_rule (g1 (replicate n1 (Some (Var ()))) → Some (Var ()))
= (g1 (replicate n1 (Inr (Var ()))) → Inr (Var ()))"
by simp }
hence 2:"?rep_rule ` {g1 (replicate n1 (Some (Var ()))) → Some (Var ()) |g1 n1. (g1, n1) ∈ ℱ}
= {g1 (replicate n1 (Inr (Var ()))) → Inr (Var ()) |g1 n1. (g1, n1) ∈ ℱ}"
using Collect_cong setcompr_eq_image
by (smt option.simps(5) ta_rule.case)
have "ta_rules (term_to_ta_R r) = ?rep_rule ` (ta_rules (term_to_ta r))"
using ta_rules_Some_conv unfolding term_to_ta_R_def fmap_states_ta_def by simp
then show ?thesis unfolding term_to_ta_def term_TA_def
by (simp add: 1 2 image_Un)
qed
lemma ta_rules_Inr_conv:
assumes "f qs → Inr t ∈ ta_rules (term_to_ta_R (l :: ('f,'v) term))"
shows "∃qs'. qs = map Inr qs'"
proof -
let ?g = "(λx.(case x of Some y ⇒ Inr y| None ⇒ Inl (Var ())))"
let ?rep_rule = "λr. case r of g qs → q ⇒ g (map ?g qs) → ?g q"
have "ta_rules (term_to_ta_R l) = ?rep_rule ` (ta_rules (term_to_ta l))"
using assms ta_rules_Some_conv unfolding term_to_ta_R_def fmap_states_ta_def by simp
then obtain qs'' q'' where qs'':"(qs = map ?g qs'')" "(Inr t = ?g q'')" "(f qs'' → q'') ∈ ta_rules (term_to_ta (l::('f,'v) term))"
by (smt Inr_inject assms image_iff option.simps(5) ta_rule.case ta_rule.exhaust ta_rule.inject ta_rules_Some)
then obtain qs''' where "qs'' = map Some qs'''" using ta_rules_Some_conv
using ta_rules_Some
by metis
hence "qs = map Inr qs'''" using qs''(1) by simp
thus ?thesis by force
qed
lemma res_to_instance_R:
assumes "linear_term (t :: ('f,'v) term)" "ground s"
"Inr (embed_term t) ∈ ta_res (term_to_ta_R t) (adapt_vars (embed_term s))" "signed_term s"
shows "∃σ. (s :: ('f,'v) term) = t ⋅ σ"
proof -
have grnd: "ground (adapt_vars (embed_term s))" unfolding embed_term_def
by (simp add: assms(2))
have "ta_final (term_to_ta_R t) = {Inr (embed_term t)}"
unfolding term_to_ta_R_def term_to_ta_def
by (simp add: fmap_states_ta_def')
moreover then have "ta_res (term_to_ta_R t) (adapt_vars (embed_term s)) ∩ (ta_final (term_to_ta_R t)) ≠ {}"
using assms(3) by simp
ultimately have " (embed_term s) ∈ ta_lang (term_to_ta_R t)" using assms(2,3) grnd
unfolding ta_lang_def
by (smt CollectI Int_commute adapt_vars_reverse)
hence "(embed_term s) ∈ ta_lang (term_to_ta t)" using lang_equiv_R
by auto
then show ?thesis using lang_to_instance[OF assms(2,1)] assms(2,4)
by argo
qed
definition L_trs_ta_set :: "('f, 'v) trs ⇒ (('f, unit) term + ('f, unit) term, 'f) ta set" where
"L_trs_ta_set TRS = {(term_to_ta_L t)|t. t ∈ fst ` TRS}"
definition trs_to_ta_L :: "('f,'v) trs ⇒ (('f, unit) term + ('f, unit) term, 'f) ta" where
"trs_to_ta_L TRS = ta.make {}
(⋃ (ta_rules ` (L_trs_ta_set TRS)))
{(Inl (embed_term s), Inr (embed_term t))| s t . (s,t) ∈ TRS}"
lemma ta_eps_trs_ta:
"ta_eps (trs_to_ta_L R) = {(Inl (embed_term s), Inr (embed_term t))| s t . (s,t) ∈ R}"
unfolding trs_to_ta_L_def by force
definition R_trs_ta_set :: "('f, 'v) trs ⇒ (('f, unit) term + ('f, unit) term, 'f) ta set" where
"R_trs_ta_set TRS = {(term_to_ta_R t)|t. t ∈ snd ` TRS}"
definition trs_to_ta_R :: "('f,'v) trs ⇒ (('f, unit) term + ('f, unit) term, 'f) ta" where
"trs_to_ta_R TRS = ta.make {}
(⋃ (ta_rules ` (R_trs_ta_set TRS)))
{}"
lemma ta_eps_trs_R:
"ta_eps (trs_to_ta_R TRS) = {}"
unfolding trs_to_ta_R_def by force
lemma ta_subset_L:
assumes "t ∈ fst ` TRS"
shows "ta_subset (term_to_ta_L t⦇ta_final := {}⦈) (trs_to_ta_L TRS)"
proof -
have "ta_eps (term_to_ta_L t) ⊆ ta_eps (trs_to_ta_L TRS)" unfolding term_to_ta_L_def term_to_ta_def
by (simp add: fmap_states_ta_def')
moreover have "ta_rules (term_to_ta_L t) ⊆ ta_rules (trs_to_ta_L TRS)" using assms
by (auto simp: term_to_ta_L_def L_trs_ta_set_def trs_to_ta_L_def term_to_ta_def)
ultimately show ?thesis by (auto simp: ta_subset_def)
qed
lemma L_rules_is_Inl:
assumes "f qs → q ∈ ta_rules (trs_to_ta_L trs)"
shows "is_Inl q"
proof -
obtain t where "f qs → q ∈ ta_rules (term_to_ta_L t)" "t ∈ fst ` trs"
using assms unfolding trs_to_ta_L_def L_trs_ta_set_def
by (smt UN_iff mem_Collect_eq ta_make_simps(1))
thus ?thesis using ta_rules_Inl_eq[of t] unfolding is_Inl_def by blast
qed
lemma trs_res_L:
assumes "linear_term (t :: ('f,'v) term)" "(s :: ('f,'v) term) = t ⋅ σ" "ground s" "t ∈ fst ` trs" "signed_term s"
shows "Inl (embed_term t) ∈ ta_res (trs_to_ta_L trs) (adapt_vars (embed_term s))"
using ta_subset_L[OF assms(4)] instance_to_res_L[OF assms(1-3,5)]
by (auto simp: ta_subset_def ta_res_stable)
lemma ta_eps_trancl:
"(ta_eps (trs_to_ta_L R))⇧+ = ta_eps (trs_to_ta_L R)"
proof -
let ?R = "ta_eps (trs_to_ta_L R)"
have " fst ` ?R ∩ snd ` ?R = {}" unfolding trs_to_ta_L_def by force
hence "trans ?R" using ta_eps_trs_ta
apply (auto simp: trans_def)
by (smt Inl_Inr_False Pair_inject mem_Collect_eq ta_eps_trs_ta)
thus ?thesis using trancl_id by simp
qed
lemma ta_rules_trs_L:
assumes "TRS ≠ {}"
shows "ta_rules (trs_to_ta_L (TRS::('f,'v) trs))
= ({(f (map Inl ts) → Inl (Fun f ts))|f ts r. Fun f ts ⊴ (embed_term r) ∧ r ∈ fst ` TRS})
∪ {g (replicate n (Inl (Var ()))) → Inl (Var ()) |g n. (g, n) ∈ ℱ}"
proof -
let ?var = "{(f (map Inl ts) → ((Inl (Fun f ts))::('f,unit) term + ('f, unit) term) )|f ts r. Fun f ts ⊴ (embed_term r) ∧ r ∈ fst ` TRS}"
let ?const = "{g (replicate n (Inl (Var ()))) → Inl (Var ()) |g n. (g, n) ∈ ℱ}"
have "(UNION (L_trs_ta_set TRS) ta_rules) ⊆ ?var ∪ ?const"
proof -
{ fix y
assume y:"(y ∈ (⋃x∈{term_to_ta_L t |t. t ∈ lhss TRS}. ta_rules x))"
hence "(∃t ∈ fst ` TRS. y ∈ (ta_rules (term_to_ta_L t)))"
by auto
hence " (y ∈ ?var ∪ ?const)"
by (smt Un_iff fixed_signature.ta_rules_Inl_eq st_def mem_Collect_eq)
}
hence 1:"(⋃x∈{term_to_ta_L t |t. t ∈ lhss TRS}. ta_rules x) ⊆ ?var ∪ ?const"
by blast
thus ?thesis unfolding L_trs_ta_set_def using ta_rules_Inl_eq by simp
qed
moreover have "?var ∪ ?const ⊆ (UNION (L_trs_ta_set TRS) ta_rules) "
proof -
{ fix y
assume y:"y ∈ ?var ∪ ?const"
hence "y ∈ ?var ∨ y ∈ ?const" by simp
hence "(y ∈ (⋃x∈{term_to_ta_L t |t. t ∈ lhss TRS}. ta_rules x))"
proof (rule disjE, goal_cases var const)
case var
then obtain f ts r where r:"y = f map Inl ts → Inl (Fun f ts)" "((embed_term r) ⊵ (Fun f ts))" " r ∈ lhss TRS"
by fast
hence "y ∈ ta_rules (term_to_ta_L r)" unfolding ta_rules_Inl_eq by blast
hence "y ∈ (⋃x∈{term_to_ta_L t |t. t ∈ lhss TRS}. ta_rules x)" using r(3) by auto
then show ?case unfolding L_trs_ta_set_def using ta_rules_Inr_eq by blast
next
case const
then obtain g n where g_n:"y = g replicate n (Inl (Var ())) → Inl (Var ()) ∧
(g, n) ∈ ℱ" by fast
hence "∀r ∈ fst ` TRS. y ∈ ta_rules (term_to_ta_L r)" using g_n
unfolding ta_rules_Inl_eq by blast
then have "∃r ∈ (fst ` TRS). y ∈ ta_rules (term_to_ta_L r)" using assms by auto
hence "y ∈ (⋃x∈{term_to_ta_L t |t. t ∈ lhss TRS}. ta_rules x)" by fast
then show ?case unfolding L_trs_ta_set_def by blast
qed
}
then show ?thesis unfolding L_trs_ta_set_def
by force
qed
ultimately show ?thesis using ta_rules_Inl_eq unfolding trs_to_ta_L_def L_trs_ta_set_def
apply simp
by (smt le_sup_iff subset_antisym)
qed
lemma trs_res_to_instance_L:
assumes "lv_trs (R :: ('f,'v) trs)"
"ground s" "signed_term s"
"Inl (embed_term t') ∈ ta_res (trs_to_ta_L R) (adapt_vars (embed_term s))" "linear_term t'" "R ≠ {}"
shows "∃σ. (s :: ('f,'v) term) = t' ⋅ σ"
using assms(4,3,1,2,5)
proof (induction s arbitrary: t' rule: ta_res.induct)
case (2 TA f ss)
obtain qs q where q_qs:
"(f qs → q) ∈ ta_rules (trs_to_ta_L R)"
"(q, Inl (embed_term t')) ∈ ((ta_eps (trs_to_ta_L R))^*)"
"length qs = length ss"
"(∀ i < length ss. qs ! i ∈ (map (ta_res (trs_to_ta_L R)) (map adapt_vars (map embed_term ss)))! i)"
using 2(2) ta_res.simps(2)[of "trs_to_ta_L R" f "(map adapt_vars (map embed_term ss))"]
unfolding embed_term_def
unfolding ta_res.simps embed_term_def term.map adapt_vars_simps
unfolding length_map map_map comp_def term.map_comp const_def
by blast
have t:"q = Inl (embed_term t')" using q_qs(2) unfolding trs_to_ta_L_def
using rtranclE by force
then obtain l where l:"(f qs → Inl (embed_term t')) ∈ ta_rules (term_to_ta_L (l::('f,'v) term))" "l ∈ fst ` R"
using q_qs(1) unfolding trs_to_ta_L_def L_trs_ta_set_def by auto
then obtain qs' where qs':"qs = map Inl qs'" using ta_rules_Inl_conv by metis
then show ?case
proof (cases "embed_term t'")
case (Var r)
then have r:"r = ()" using l ta_rules_trs_L[of R] by simp
then obtain x where x:"t' = Var x" using Var unfolding embed_term_def
by (metis is_VarE is_VarI term.map_disc_iff)
then obtain σ where "(Fun f ss) = (Var x) ⋅ σ"
by (metis const_def subst_apply_term.simps(1))
then show ?thesis using x by fast
next
case (Fun g ts)
have g_f:"g = f" "ts = qs'" using q_qs(1) qs' unfolding t Fun using ta_rules_trs_L[OF assms(6)]
by (simp)+
hence t':"Fun g ts = embed_term t'" using 2(6) Fun
by argo
then obtain ts' where g_ts:"t' = Fun g ts'" "ts = map embed_term ts'" using embed_inv by blast
then have ts':"qs' = map (embed_term) ts' ∧ t' = (Fun f ts')" unfolding g_f Fun t' by blast
hence len_eq:"length ts' = length ss" using q_qs(3) qs' by fastforce
{ fix i
assume i: "i < length ss"
hence grnd: "ground (ss!i)" using 2(5) by simp
have sig:"signed_term (ss!i)" using i 2(3) unfolding st_def
by fastforce
have av:"adapt_vars (embed_term (ss!i)) = (map adapt_vars (map embed_term ss))!i"
using map_map i unfolding embed_term_def adapt_vars_def by fastforce
hence inr:"Inl (qs' ! i) ∈ (ta_res (trs_to_ta_L R)) (adapt_vars ( embed_term (ss!i)))" using q_qs(3,4) i qs'
by auto
have linear:"linear_term (ts'!i)" using 2(6) ts' unfolding embed_term_def
using i q_qs(3) qs' by fastforce
have "(qs'!i) = embed_term (ts'!i)"
using i q_qs(3) qs' ts' by auto
with i grnd sig linear av inr have "∃σ. ((ss!i) = (ts'!i) ⋅ σ)"
using 2(1)[of i "ss!i" "ts'!i"] 2(4)
using nth_mem
by metis }
note ind= this
then obtain σs where σs:
"length σs = length ss"
"(∀i < length ss. ((ss!i) = (ts'!i) ⋅ (σs!i)))"
using construct_exI'[of "length ss" "λ σ i.((ss!i) = (ts'!i) ⋅ σ)"]
by blast
then obtain σ where "∀i< length ts'.(ts'!i) ⋅ (σs!i) = (ts'!i) ⋅ σ" using len_eq subst_unification_list[of "ts'" "σs"] 2(6) ts'
by (metis linear_term.simps(2))
hence "Fun f ss = Fun f ts' ⋅ σ" using σs(2) len_eq
by (metis map_nth_eq_conv subst_apply_term.simps(2))
then show ?thesis using ts' by meson
qed
qed (auto)
lemma trs_res_to_Inr_instance_L:
assumes "lv_trs (R :: ('f,'v) trs)"
"ground s" "signed_term s"
"Inr r ∈ ta_res (trs_to_ta_L R) (adapt_vars (embed_term s))"
shows "∃σ l' r'. (s :: ('f,'v) term) = l' ⋅ σ ∧ (l',r') ∈ R ∧ r = embed_term r'"
using assms(4,1,2,3)
proof (cases s)
case (Fun f ss)
obtain qs q where q_qs:
"(f qs → q) ∈ ta_rules (trs_to_ta_L R)"
"(q, Inr r) ∈ ((ta_eps (trs_to_ta_L R))^*)"
"length qs = length ss"
"(∀ i < length ss. qs ! i ∈ (map (ta_res (trs_to_ta_L R)) (map adapt_vars (map embed_term ss)))! i)"
using assms(4) ta_res.simps(2)[of "trs_to_ta_L R" f "(map adapt_vars (map embed_term ss))"]
unfolding embed_term_def Fun
unfolding ta_res.simps embed_term_def term.map adapt_vars_simps
unfolding length_map map_map comp_def term.map_comp const_def
by blast
obtain l where l:"q = Inl l" using L_rules_is_Inl[OF q_qs(1)] unfolding is_Inl_def by blast
hence "(Inl l, Inr r) ∈ ((ta_eps (trs_to_ta_L R))^+)" using q_qs(2)
by (meson Inl_Inr_False rtranclD)
moreover have "(Inl l, Inr r) ∈ (ta_eps (trs_to_ta_L R))" using ta_eps_trancl
using calculation by blast
then obtain l' r' where l'_r':"l = embed_term l'" "r = embed_term r'"
"(l', r') ∈ R"
using assms(3) unfolding trs_to_ta_L_def
by (smt Inr_inject Pair_inject mem_Collect_eq sum.inject(1) ta_make_simps(2))
hence lin:"linear_term l'" "linear_term r'" using assms(1) unfolding lv_trs_def by fast+
moreover have Inl_res:"Inl (embed_term l') ∈ ta_res (trs_to_ta_L R) (adapt_vars (embed_term (Fun f ss)))"
using q_qs(1,3,4) unfolding l l'_r'(1)
ta_res.simps(2)[of "trs_to_ta_L R" f "(map adapt_vars (map embed_term ss))"]
unfolding embed_term_def
unfolding ta_res.simps embed_term_def term.map adapt_vars_simps
unfolding length_map map_map comp_def term.map_comp const_def
by blast
moreover have "∃σ. (Fun f ss) = l'⋅ σ"
using trs_res_to_instance_L[OF assms(1,2,3)] Inl_res lin(1) l'_r'(3) unfolding Fun
by blast
with l'_r'(2,3) show ?thesis unfolding Fun by fast
qed (auto)
lemma term_to_ta_rules:
assumes "f ts → Some t ∈ ta_rules (term_to_ta s)"
shows "∃ss. ts = map Some ss ∧ (t = Fun f ss ∨ t = Var ())"
using assms unfolding term_to_ta_def term_TA_def
by (smt Un_iff assms mem_Collect_eq option.sel ta_make_simps(1) ta_rule.inject ta_rules_Some_conv)
lemma term_to_ta_R_rules:
assumes "f ts → Inr t ∈ ta_rules (term_to_ta_R s)"
shows "∃ss. ts = map Inr ss ∧ (t = Fun f ss ∨ t = Var ())"
using assms unfolding ta_rules_Inr_eq
by (smt Collect_disj_eq Inr_inject assms mem_Collect_eq ta_rule.inject ta_rules_Inr_conv)
lemma ta_rules_trs_R:
assumes "R ≠ {}"
shows "ta_rules (trs_to_ta_R (R :: ('f,'v) trs))
= ({(f (map Inr ts) → Inr (Fun f ts))|f ts r. Fun f ts ⊴ (embed_term r) ∧ r ∈ snd ` R})
∪ {g (replicate n (Inr (Var ()))) → Inr (Var ()) |g n. (g, n) ∈ ℱ}"
proof -
let ?var = "{(f (map Inr ts) → ((Inr (Fun f ts))::('f,unit) term + ('f, unit) term) )|f ts r. Fun f ts ⊴ (embed_term r) ∧ r ∈ snd ` R}"
let ?const = "{g (replicate n (Inr (Var ()))) → Inr (Var ()) |g n. (g, n) ∈ ℱ}"
have "(UNION (R_trs_ta_set R) ta_rules) ⊆ ?var ∪ ?const"
proof -
{ fix y
assume y:"(y ∈ (⋃x∈{term_to_ta_R t |t. t ∈ rhss R}. ta_rules x))"
hence "(∃t ∈ snd ` R. y ∈ (ta_rules (term_to_ta_R t)))"
by auto
hence " (y ∈ ?var ∪ ?const)"
by (smt Un_iff fixed_signature.ta_rules_Inr_eq mem_Collect_eq)}
hence 1:"(⋃x∈{term_to_ta_R t |t. t ∈ rhss R}. ta_rules x) ⊆ ?var ∪ ?const"
by blast
thus ?thesis unfolding R_trs_ta_set_def using ta_rules_Inr_eq by simp
qed
moreover have " ?var ∪ ?const ⊆ (UNION (R_trs_ta_set R) ta_rules) "
proof -
{ fix y
assume y:"y ∈ ?var ∪ ?const"
hence "y ∈ ?var ∨ y ∈ ?const" by simp
hence "(y ∈ (⋃x∈{term_to_ta_R t |t. t ∈ rhss R}. ta_rules x))"
proof (rule disjE, goal_cases var const)
case var
then obtain f ts r where r:"y = f map Inr ts → Inr (Fun f ts)" "((embed_term r) ⊵ (Fun f ts))" " r ∈ rhss R"
by fast
hence "y ∈ ta_rules (term_to_ta_R r)" unfolding ta_rules_Inr_eq by blast
hence "y ∈ (⋃x∈{term_to_ta_R t |t. t ∈ rhss R}. ta_rules x)" using r(3) by auto
then show ?case unfolding R_trs_ta_set_def using ta_rules_Inr_eq by blast
next
case const
then obtain g n where g_n:"y = g replicate n (Inr (Var ())) → Inr (Var ()) ∧
(g, n) ∈ ℱ" by fast
hence "∀r ∈ snd ` R. y ∈ ta_rules (term_to_ta_R r)" using g_n
unfolding ta_rules_Inr_eq by blast
then have "∃r ∈ (snd ` R). y ∈ ta_rules (term_to_ta_R r)" using assms by auto
hence "y ∈ (⋃x∈{term_to_ta_R t |t. t ∈ rhss R}. ta_rules x)" by fast
then show ?case unfolding R_trs_ta_set_def using ta_rules_Inr_eq by blast
qed
}
then show ?thesis unfolding R_trs_ta_set_def
by force
qed
ultimately show ?thesis using ta_rules_Inr_eq unfolding trs_to_ta_R_def R_trs_ta_set_def
apply simp
by (smt le_sup_iff subset_antisym)
qed
lemma replicate_Inr:
assumes "ls = replicate n (Inr a)" "ls = map Inr ls'"
shows "ls' = replicate n a"
using assms
proof (induction ls arbitrary: n ls')
case (Cons b ls)
hence n:"n = Suc (length ls)"
by (metis length_Cons length_replicate)
have "ls = replicate (length ls) (Inr a)" using Cons(2) n by auto
moreover have "ls = map Inr (tl ls')" using Cons(3) by fastforce
ultimately have "tl ls' = replicate (length ls) a" using Cons(1)[of "length ls" "tl ls'"] by satx
moreover have "hd ls' = a" using n Cons(3,2) by force
ultimately show ?case using n
using Cons.prems(2) by force
qed (force)
lemma trs_res_to_instance_R:
assumes "lv_trs (R :: ('f,'v) trs)"
"ground s" "signed_term s"
"Inr (embed_term t') ∈ ta_res (trs_to_ta_R R) (adapt_vars (embed_term s))" "linear_term t'" "R ≠ {}"
shows "∃σ. (s :: ('f,'v) term) = t' ⋅ σ"
using assms(4,3,1,2,5)
proof (induction s arbitrary: t' rule: ta_res.induct)
case (2 TA f ss)
obtain qs q where q_qs:
"(f qs → q) ∈ ta_rules (trs_to_ta_R R)"
"(q, Inr (embed_term t')) ∈ ((ta_eps (trs_to_ta_R R))^*)"
"length qs = length ss"
"(∀ i < length ss. qs ! i ∈ (map (ta_res (trs_to_ta_R R)) (map adapt_vars (map embed_term ss)))! i)"
using 2(2) ta_res.simps(2)[of "trs_to_ta_R R" f "(map adapt_vars (map embed_term ss))"]
unfolding embed_term_def
unfolding ta_res.simps embed_term_def term.map adapt_vars_simps
unfolding length_map map_map comp_def term.map_comp const_def
by blast
have t:"q = Inr (embed_term t')" using q_qs(2) unfolding trs_to_ta_R_def
using rtranclE by force
then obtain l where l:"(f qs → Inr (embed_term t')) ∈ ta_rules (term_to_ta_R (l::('f,'v) term))" "l ∈ snd ` R"
using q_qs(1) unfolding trs_to_ta_R_def R_trs_ta_set_def by auto
then obtain qs' where qs':"qs = map Inr qs'" using ta_rules_Inr_conv by metis
then show ?case
proof (cases "embed_term t'")
case (Var r)
then have r:"r = ()" using l ta_rules_trs_R[of R] by simp
then obtain x where x:"t' = Var x" using Var unfolding embed_term_def
by (metis is_VarE is_VarI term.map_disc_iff)
then obtain σ where "(Fun f ss) = (Var x) ⋅ σ"
by (metis const_def subst_apply_term.simps(1))
then show ?thesis using x by fast
next
case (Fun g ts)
have g_f:"g = f" "ts = qs'" using q_qs(1) qs' unfolding t Fun using ta_rules_trs_R[OF assms(6)]
by (simp)+
hence t':"Fun g ts = embed_term t'" using 2(6) Fun
by argo
then obtain ts' where g_ts:"t' = Fun g ts'" "ts = map embed_term ts'" using embed_inv by blast
then obtain ts' where ts':"qs' = map (embed_term) ts' ∧ t' = (Fun f ts')" unfolding g_f Fun t' by blast
hence len_eq:"length ts' = length ss" using q_qs(3) qs' by fastforce
{ fix i
assume i: "i < length ss"
hence grnd: "ground (ss!i)" using 2(5) by simp
have sig:"signed_term (ss!i)" using i 2(3) unfolding st_def
by fastforce
have av:"adapt_vars (embed_term (ss!i)) = (map adapt_vars (map embed_term ss))!i"
using map_map i unfolding embed_term_def adapt_vars_def by fastforce
hence inr:"Inr (qs' ! i) ∈ (ta_res (trs_to_ta_R R)) (adapt_vars ( embed_term (ss!i)))" using q_qs(3,4) i qs'
by auto
have linear:"linear_term (ts'!i)" using 2(6) ts' unfolding embed_term_def
using i q_qs(3) qs' by fastforce
have "(qs'!i) = embed_term (ts'!i)"
using i q_qs(3) qs' ts' by auto
with i grnd sig linear av inr have "∃σ. ((ss!i) = (ts'!i) ⋅ σ)"
using 2(1)[of i "ss!i" "ts'!i"] 2(4)
using nth_mem
by metis }
note ind= this
then obtain σs where σs:
"length σs = length ss"
"(∀i < length ss. ((ss!i) = (ts'!i) ⋅ (σs!i)))"
using construct_exI'[of "length ss" "λ σ i.((ss!i) = (ts'!i) ⋅ σ)"]
by blast
then obtain σ where "∀i< length ts'.(ts'!i) ⋅ (σs!i) = (ts'!i) ⋅ σ" using len_eq subst_unification_list[of "ts'" "σs"] 2(6) ts'
by (metis linear_term.simps(2))
hence "Fun f ss = Fun f ts' ⋅ σ" using σs(2) len_eq
by (metis map_nth_eq_conv subst_apply_term.simps(2))
then show ?thesis using ts' by meson
qed
qed (auto)
lemma ta_subset_R:
assumes "t ∈ snd ` R"
shows "ta_subset (term_to_ta_R t⦇ta_final := {}⦈) (trs_to_ta_R R)"
proof -
have "ta_eps (term_to_ta_R t) ⊆ ta_eps (trs_to_ta_R R)" unfolding term_to_ta_R_def term_to_ta_def
by (simp add: fmap_states_ta_def')
moreover have "ta_rules (term_to_ta_R t) ⊆ ta_rules (trs_to_ta_R R)" using assms
by (auto simp: term_to_ta_R_def R_trs_ta_set_def trs_to_ta_R_def term_to_ta_def)
ultimately show ?thesis by (auto simp: ta_subset_def)
qed
lemma trs_res_R:
assumes "linear_term (t :: ('f,'v) term)" "(s :: ('f,'v) term) = t ⋅ σ" "ground s" "t ∈ snd ` trs" "signed_term s"
shows "Inr (embed_term t) ∈ ta_res (trs_to_ta_R trs) (adapt_vars (embed_term s))"
using ta_subset_R[OF assms(4)] instance_to_res_R[OF assms(1-3,5)]
by (auto simp: ta_subset_def ta_res_stable)
lemma neg_res_R_trs:
assumes "ground (s :: ('f,'v) term)" "signed_term s"
shows "∀v. Inl v ∉ ta_res (trs_to_ta_R trs) (adapt_vars (embed_term s))"
proof (rule ccontr)
assume asm:"¬(∀(v::('f, unit) term). Inl v ∉ ta_res (trs_to_ta_R trs) (adapt_vars (embed_term s)))"
have "∃(v::('f, unit) term). Inl v ∈ ta_res (trs_to_ta_R trs) (adapt_vars (embed_term s))"
using asm by simp
then obtain v where v:"Inl (v::('f,unit) term) ∈ ta_res (trs_to_ta_R trs) (adapt_vars (embed_term s))"
by auto
obtain f ss where s:"s = Fun f ss" using assms using ground.elims(2) by blast
obtain qs q where q_qs:"(f qs → q) ∈ ta_rules (trs_to_ta_R trs) "
"(q,Inl v) ∈ ((ta_eps (trs_to_ta_R trs) )^*) "
"length qs = length ss"
"(∀ i < length ss. qs ! i ∈ (map (ta_res (trs_to_ta_R trs)) (map adapt_vars (map embed_term ss)))! i)"
using v ta_res.simps(2)[of "trs_to_ta_R trs" f "(map adapt_vars (map embed_term ss))"] map_map
unfolding embed_term_def s
unfolding ta_res.simps embed_term_def term.map adapt_vars_simps
unfolding length_map map_map comp_def term.map_comp const_def
by blast
have "q = Inl v" using ta_eps_trs_R[of trs] q_qs(2) by auto
hence qsq:"(f qs → Inl v) ∈ ta_rules (trs_to_ta_R trs)"
using q_qs(1) by auto
then obtain t where "(f qs → Inl v) ∈ ta_rules (term_to_ta_R t)" "t ∈ snd ` trs"
unfolding trs_to_ta_R_def R_trs_ta_set_def by auto
thus False using ta_rules_Inr_eq[of t] by blast
qed
subsection ‹GTT acceptance results›
definition trs_to_gtt where
"trs_to_gtt R = (trs_to_ta_L R, trs_to_ta_R R)"
lemma r_to_gtt_accept:
assumes "lv_trs (R :: ('f,'v) trs)" "ground u" "ground v" "(u :: ('f,'v) term) = s ⋅ σ" "v = t ⋅ σ"
"(s, t) ∈ R" "signed_term u" "signed_term v"
shows "gtt_accept (trs_to_gtt R) (adapt_vars (embed_term u)) (adapt_vars (embed_term v))"
proof -
have linear:"linear_term s" "linear_term t" using assms(1,6) unfolding lv_trs_def by (fast)+
have "Inl (embed_term s) ∈ ta_res (trs_to_ta_L R) (adapt_vars (embed_term u))"
using trs_res_L[OF linear(1) assms(4,2)] assms(6,7) unfolding fst_def by fast
moreover have "(Inl (embed_term s), Inr (embed_term t)) ∈ ta_eps (trs_to_ta_L R)"
using assms(6) ta_eps_trs_ta[of R] by auto
ultimately have 1:"Inr (embed_term t) ∈ ta_res (trs_to_ta_L R) (adapt_vars (embed_term u))"
by (meson rtrancl.simps ta_res_eps)
from linear(2) have "Inr (embed_term t) ∈ ta_res (trs_to_ta_R R) (adapt_vars (embed_term v))"
using trs_res_R[OF linear(2) assms(5,3)] assms(6,8) unfolding snd_def by fast
thus ?thesis using 1 by (auto simp: trs_to_gtt_def)
qed
lemma rstep_to_gtt_accept:
assumes "lv_trs (R :: ('f,'v) trs)" "ground s" "ground t" "(s, t) ∈ rstep R" "signed_term s" "signed_term t"
shows "gtt_accept (trs_to_gtt R) (adapt_vars (embed_term s)) (adapt_vars (embed_term t))"
using assms(4,3,2,1)
proof (induction rule: rstepE)
case (rstep s t C σ l r)
let ?𝒢 = "(trs_to_ta_L R, trs_to_ta_R R)"
let ?C = "adapt_vars_ctxt (embed_ctxt C)"
let ?s = "adapt_vars (embed_term (l ⋅ σ))"
let ?t = "adapt_vars (embed_term (r ⋅ σ))"
thm rstep(1,4,5,6,7,8) funas_term_ctxt
have signed:"signed_term ?s" "signed_term ?t" using assms(5,6) funas_term_ctxt[OF rstep(4)]
funas_term_ctxt[OF rstep(5)] funas_term_embed unfolding st_def rstep(1,2) by fast+
have "gtt_accept (trs_to_gtt R) (adapt_vars (embed_term (l ⋅ σ))) (adapt_vars (embed_term (r ⋅ σ)))"
using r_to_gtt_accept rstep signed
using ground_ctxt_apply
by (metis (no_types, lifting) fixed_signature.funas_term_embed st_def)
hence "gtt_accept' (trs_to_gtt R) (adapt_vars (embed_term s)) (adapt_vars (embed_term t))"
proof -
have loc:"(?C)⟨?s⟩ = adapt_vars (embed_term s)"
"(?C)⟨?t⟩ = adapt_vars (embed_term t)"
using rstep(1,4,6) unfolding embed_ctxt_def embed_term_def
apply (simp add: rstep.hyps(2) rstep.hyps(3) map_vars_term_ctxt_commute)
using rstep(2,5,6) unfolding embed_ctxt_def embed_term_def
by (simp add: rstep.hyps(2) rstep.hyps(3) map_vars_term_ctxt_commute)
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 (embed_term s)]" "[adapt_vars (embed_term t)]" "?𝒢"
"mctxt_of_ctxt (adapt_vars_ctxt (embed_ctxt C))"]
by (smt One_nat_def ‹gtt_accept (trs_to_gtt R) (adapt_vars (embed_term (l ⋅ σ))) (adapt_vars (embed_term (r ⋅ σ)))› accept'_closed_ctxt gtt_accept'_refl gtt_accept_equiv length_Cons list.size(3) nth_Cons' num_holes_mctxt_of_ctxt)
qed
then show ?case using rstep(1,2,3) using accept'_closed_ctxt
using gtt_accept_equiv by blast
qed
lemma par_rstep_to_gtt_accept:
assumes "lv_trs R" "ground u" "ground v" "(u, v) ∈ par_rstep R" "signed_term u" "signed_term v"
shows "gtt_accept (trs_to_gtt R) (adapt_vars (embed_term u)) (adapt_vars (embed_term v))"
using assms(4,3,2,1,5,6)
proof (induction rule: par_rstep.induct)
case (root_step s t σ)
show ?case using rstep_to_gtt_accept[OF root_step(4,3,2)] root_step(1,5,6) by auto
next
case (par_step_fun ts ss f)
{ fix i
assume i: "i < length ts"
hence "ground (ss!i)" "ground (ts!i)" "signed_term (ss!i)" "signed_term (ts!i)" using par_step_fun(4,5,2,7,8)
subgoal by simp
subgoal by (meson ground_recur i par_step_fun.prems(1))
subgoal using i par_step_fun.hyps(2) par_step_fun.prems(4) by (fastforce simp: st_def)
subgoal using i par_step_fun.prems(5) by (fastforce simp: st_def)
done
hence "gtt_accept (trs_to_gtt R)
(adapt_vars (embed_term (ss ! i)))
(adapt_vars (embed_term (ts ! i)))"
by (simp add: i par_step_fun.IH par_step_fun.prems(3))}
then show ?case using par_step_fun(2) unfolding embed_term_def by auto
qed (auto)
lemma gtt_accept_to_par_rstep:
assumes "lv_trs (R :: ('f,'v) trs)" "ground (s :: ('f,'v) term)" "ground (t :: ('f,'v) term)"
"u = adapt_vars (embed_term s)" "v = adapt_vars (embed_term t)"
"gtt_accept (trs_to_gtt R) u v" "signed_term s" "signed_term t"
shows "(s, t) ∈ par_rstep R"
using assms(6,5,4,3,2,1,7,8)
proof (induction arbitrary: s t rule:gtt_accept.induct)
case (join q l r)
have "is_Inl q ∨ is_Inr q" unfolding is_Inl_def is_Inr_def using obj_sumE by auto
then show ?case
proof (rule disjE, goal_cases Inl Inr)
case Inl
then obtain v where q:"q = Inl v"
by (meson is_Inl_def)
have "Inl v ∉ ta_res (trs_to_ta_R R) (adapt_vars (embed_term t))"
using neg_res_R_trs[OF join(5,9)] by force
then show ?case using join(2) unfolding q snd_def join(3) by (simp add: trs_to_gtt_def)
next
case Inr
then obtain v where v:"q = Inr v" unfolding is_Inr_def by auto
hence l_v:"Inr v ∈ ta_res (trs_to_ta_L R) l" using join(1) unfolding fst_def trs_to_gtt_def by fast
then obtain σ⇩l u' v' where u'_v':"(s::('f,'v) term) = u' ⋅ σ⇩l" "(u',v') ∈ R" "v = embed_term v'"
using trs_res_to_Inr_instance_L[OF join(7,6,8) ] l_v join(4)
by blast
then have r_v':"Inr (embed_term v') ∈ ta_res (trs_to_ta_R R) r" using join(2) unfolding v u'_v'(3)
by (simp add: u'_v'(1) trs_to_gtt_def)
have lin: "linear_term v'" using u'_v'(2) join(7) unfolding lv_trs_def by fast
have "R ≠ {}" using u'_v'(2) by auto
then obtain σ⇩r where σ⇩r:"t = v' ⋅ σ⇩r" using trs_res_to_instance_R[OF join(7,5,9)] r_v' join(3) lin
by blast
then obtain σ where σ:"u' ⋅ σ⇩l = u' ⋅ σ" "v' ⋅ σ⇩r = v' ⋅ σ"
using u'_v'(2) join(7) unfolding lv_trs_def using subst_unification by blast
then show ?case using σ⇩r u'_v'(1,2) by auto
qed
next
case (ctxt ss ts f)
have grst:"ground (Fun f ss)" "ground (Fun f ts)" using ctxt(3,4) unfolding embed_term_def
apply (metis ctxt.prems(4) ground_adapt_vars ground_map_vars_term)
by (metis ctxt.prems(1) ctxt.prems(3) embed_term_def ground_adapt_vars ground_map_vars_term)
then obtain ss' where ss':"s = (Fun f ss') ∧ (length ss' = length ss) ∧ ss = map (adapt_vars ∘ embed_term) ss'"
using ctxt(3) map_map unfolding embed_term_def
by (smt Term.term.simps(10) adapt_vars_simps ctxt.prems(2) ctxt.prems(4) embed_term_def ground.elims(2) length_map term.inject(2))
from grst obtain ts' where ts':"t = (Fun f ts') ∧ (length ts' = length ts) ∧ ts = map (adapt_vars ∘ embed_term) ts'"
using ctxt(4) map_map unfolding embed_term_def
by (smt Term.term.simps(10) adapt_vars_def ctxt.prems(1) ctxt.prems(3) embed_term_def ground.elims(2) length_map term.inject(2))
{ fix i
assume i: "i < length ss"
have ii:"ss!i = adapt_vars (embed_term (ss'!i))" "ts!i = adapt_vars (embed_term (ts'!i))"
apply (metis comp_apply i map_nth_eq_conv ss')
by (metis comp_eq_dest_lhs ctxt.hyps i nth_map ts')
have grnd: "ground (ss'!i)" "ground (ts'!i)" using i ss' ts' ctxt(1,5,6)
apply (metis ground_recur)
by (metis ctxt.hyps ctxt.prems(3) ground_recur i ts')
moreover have "signed_term (ss'!i)" "signed_term (ts'!i)" using st_def[of s] st_def[of t] ss' ts' ctxt(8,9)
apply (metis (no_types, lifting) UN_I fixed_signature.st_def funas_term_args i nth_mem order_trans subsetI term.sel(4))
using st_def[of t] ts' ctxt(9) i ctxt(1)
by (metis (no_types, lifting) UN_I st_def funas_term_args nth_mem order_trans subsetI term.sel(4))
ultimately have "(ss' ! i, ts' ! i) ∈ par_rstep R" using i ctxt.IH
using ctxt.prems(5) ii(1) ii(2) by blast }
then show ?case using ss' ts' ctxt(1)
by (metis par_rstep.par_step_fun)
next
case (refl ta)
hence "s = t"
by (metis adapt_vars_adapt_vars embed embed_term_def ground_adapt_vars ground_imp_linear_term
ground_map_vars_term ground_subst_apply lang_to_instance_0 subterm.eq_iff subterm.eq_iff)
then show ?case by fast
qed
lemma signed_term_adapt_vars [simp]:
"signed_term (adapt_vars t) = signed_term t"
by (auto simp: st_def)
lemma gtt_lang_trs_to_gtt:
assumes "lv_trs (R :: ('f,'v) trs)"
shows "Restr (gtt_lang (trs_to_gtt R)) {t. signed_term t} = map_both adapt_vars ` Restr (par_rstep R) {t. ground t ∧ signed_term t}"
proof (intro equalityI subrelI, goal_cases LR RL)
case (LR s t)
then show ?case
using gtt_accept_to_par_rstep[OF assms, of "adapt_vars s" "adapt_vars t" s t]
unfolding adapt_vars_def embed_term_def term.map_comp
by (auto 0 0 simp: term.map_comp comp_def ground_map_vars_term_simp[of _ "λx. x", folded adapt_vars_def] adapt_vars_def[symmetric] adapt_vars_id
intro!: rev_image_eqI[of "(adapt_vars s, adapt_vars t)"])
next
case (RL s t)
then show ?case
using par_rstep_to_gtt_accept[OF assms, of "adapt_vars s" "adapt_vars t"]
unfolding adapt_vars_def embed_term_def term.map_comp
by (auto 0 0 simp: term.map_comp comp_def ground_map_vars_term_simp[of _ "λx. x", folded adapt_vars_def])
(simp_all only: adapt_vars_idemp)
qed
end
end