theory Ground_Confluence
imports GTT_TRS GTT_RRn GTT_Transitive_Closure Lisa.LS_Extras
begin
abbreviation some_rsteps_to_GTT where
"some_rsteps_to_GTT R ≡ (trs_to_ta_A R, trs_to_ta_B R)"
abbreviation GTT_comp' where
"GTT_comp' G1 G2 ≡ GTT_comp (fmap_states_gtt Inl G1) (fmap_states_gtt Inr G2)"
lemma trancl_map_prod_mono:
"map_both f ` R⇧+ ⊆ (map_both f ` R)⇧+"
proof -
have "(f x, f y) ∈ (map_both f ` R)⇧+" if "(x, y) ∈ R⇧+" for x y using that
by (induct) (auto intro: trancl_into_trancl)
then show ?thesis by auto
qed
lemma trancl_full_on:
"(X × X)⇧+ = X × X"
using trancl_unfold_left[of "X × X"] trancl_unfold_right[of "X × X"] by auto
lemma Restr_trancl_Restr:
"Restr ((Restr R X)⇧+) X = (Restr R X)⇧+"
using trancl_mono_set[of "Restr R X" "X × X"]
by (auto simp: trancl_full_on)
lemma trancl_map_both_Restr:
assumes "inj_on f X"
shows "(map_both f ` Restr R X)⇧+ = map_both f ` (Restr R X)⇧+"
proof -
have [simp]:
"map_prod (inv_into X f ∘ f) (inv_into X f ∘ f) ` Restr R X = Restr R X"
using inv_into_f_f[OF assms]
apply (intro equalityI subrelI)
apply (auto simp: comp_def map_prod_def image_def)
apply (metis (no_types, lifting) IntI SigmaI case_prod_conv)
done
have [simp]:
"map_prod (f ∘ inv_into X f) (f ∘ inv_into X f) ` (map_both f ` Restr R X)⇧+ = (map_both f ` Restr R X)⇧+"
using f_inv_into_f[of _ f X] subsetD[OF trancl_mono_set[OF image_mono[of "Restr R X" "X × X" "map_both f"]]]
by (intro equalityI subrelI) (auto simp: map_prod_surj_on trancl_full_on comp_def rev_image_eqI)
show ?thesis using assms trancl_map_prod_mono[of f "Restr R X"]
image_mono[OF trancl_map_prod_mono[of "inv_into X f" "map_both f ` Restr R X"], of "map_both f"]
by (intro equalityI) (simp_all add: image_comp map_prod.comp)
qed
lemma trancl_map_both_adapt_vars_Restr:
"(map_both adapt_vars ` Restr X {t. ground t})⇧+ =
map_both adapt_vars ` (Restr X {t. ground t})⇧+"
by (auto simp: trancl_map_both_Restr inj_on_def)
lemma Restr_map_both_adapt_vars:
"Restr (map_both adapt_vars ` X) {t. ground t} =
map_both adapt_vars ` (Restr X {t. ground t})"
by (auto)
lemma map_both_adapt_vars_Restr_Id:
"map_both adapt_vars ` Restr Id {t. ground t} = Restr Id {t. ground t}"
apply (auto)
apply (metis IdI IntI SigmaI adapt_vars_adapt_vars ground_adapt_vars map_prod_imageI mem_Collect_eq)
done
lemma Restr_rtrancl_map_both_adapt_vars:
"Restr ((map_both adapt_vars ` Restr X {t. ground t})⇧*) {t. ground t} =
map_both adapt_vars ` (Restr ((Restr X {t. ground t})⇧*) {t. ground t})"
using trancl_mono_set[OF Int_mono[OF _ subset_refl], of "X" "UNIV" "{t. ground t} × {t. ground t}"]
by (simp del: reflcl_trancl trancl_reflcl add: rtrancl_trancl_reflcl Int_Un_distrib2 image_Un
trancl_map_both_adapt_vars_Restr Restr_map_both_adapt_vars map_both_adapt_vars_Restr_Id)
lemma converse_Restr:
"(Restr R T)¯ = Restr (R¯) T"
by auto
lemma map_both_comp1:
"map_both f ` (Restr R X O Restr S X) ⊆ map_both f ` (Restr R X) O map_both f ` (Restr S X)"
by auto
lemma map_both_comp:
"inj_on f X ⟹ map_both f ` (Restr R X) O map_both f ` (Restr S X) = map_both f ` (Restr R X O Restr S X)"
apply (intro equalityI map_both_comp1)
apply auto
by (smt IntI SigmaI case_prodI inj_onD map_prod_imageI mem_Collect_eq relcomp_unfold)
lemma relcomp_map_both_adapt_vars_Restr:
shows "(map_both adapt_vars ` Restr R {t. ground t}) O
(map_both adapt_vars ` Restr S {t. ground t}) =
map_both adapt_vars ` (Restr R {t. ground t} O Restr S {t. ground t})"
by (intro map_both_comp) (auto simp: inj_on_def)
lemma map_both_converse:
"map_both f ` (X¯) = (map_both f ` X)¯"
by auto
lemma gtt_lang_inverse:
"gtt_lang (prod.swap 𝒢) = (gtt_lang 𝒢)¯"
by auto
lemma CR_Restr_conv:
"CR (Restr R A) ⟷
(Restr ((Restr R A)⇧*) A)¯ O (Restr ((Restr R A)⇧*) A) ⊆ (Restr ((Restr R A)⇧*) A) O (Restr ((Restr R A)⇧*) A)¯"
proof -
obtain Q where Q: "(Restr R A)⇧+ = Restr Q A" using Restr_trancl_Restr by metis
show ?thesis unfolding CR_iff_meet_subset_join meet_def join_def rtrancl_converse
by (auto simp: reflcl_trancl[symmetric] Q)
qed
lemma GCR_criterion_GTT:
assumes "ground_trs R" "finite R"
shows "CR_on (rstep R) {t. ground t} ⟷
(let GR = GTT_trancl (some_rsteps_to_GTT R) in
gtt_lang (GTT_comp' (prod.swap GR) GR) ⊆ gtt_lang (GTT_comp' GR (prod.swap GR)))" (is "?L ⟷ ?R")
proof -
let ?G = "some_rsteps_to_GTT R"
let ?Gs = "GTT_trancl (some_rsteps_to_GTT R)"
let ?Gl = "GTT_comp' (prod.swap ?Gs) ?Gs" and ?Gr = "GTT_comp' ?Gs (prod.swap ?Gs)"
have R_conv: "?R ⟷ gtt_lang ?Gl ⊆ gtt_lang ?Gr" by (simp add: Let_def)
have *: "(l, r) ∈ R ⟹ vars_term r ⊆ vars_term l" for l r
using assms by (auto simp: ground_trs_def ground_vars_term_empty)
have "Restr (rstep R) {t. ground t} ⊆ map_both adapt_vars ` gtt_lang (some_rsteps_to_GTT R)"
using rstep_to_gtt_accept[OF assms(1)]
apply (auto simp: image_def)
apply (smt IntI adapt_vars_adapt_vars case_prodI ground_adapt_vars map_prod_simp mem_Collect_eq mem_Sigma_iff)
done
note rtrancl_mono[OF this]
moreover have
"map_both adapt_vars ` gtt_lang (some_rsteps_to_GTT R) ⊆ (Restr (rstep R) {t. ground t})⇧*"
using gtt_accept_to_rstep_rtrancl[OF assms(1)]
by (intro subrelI conjunct1[OF rtrancl_on_iff_rtrancl_restr]) (auto simp: rstep_ground[of R] *)
note rtrancl_mono[OF this]
ultimately have **:
"(map_both adapt_vars ` gtt_lang ?G)⇧* = (Restr (rstep R) {t. ground t})⇧*"
by simp
have t: "map_both adapt_vars ` gtt_lang ?Gs = Restr ((Restr (rstep R) {t. ground t})⇧*) {t. ground t}"
using arg_cong[OF **, of "λX. Restr X {t. ground t}"]
arg_cong[OF GTT_trancl_lang[of "?G"], of "λX. map_prod rep rep ` X"]
using finite_ta_states[OF assms(2)]
by (simp add: Restr_rtrancl_map_both_adapt_vars Restr_map_both_adapt_vars Restr_rtrancl_gtt_lang_eq_trancl_gtt_lang)
have l: "map_both adapt_vars ` gtt_lang ?Gl =
(Restr ((Restr (rstep R) {t. ground t})⇧*) {t. ground t})¯ O Restr ((Restr (rstep R) {t. ground t})⇧*) {t. ground t}"
(is "?Gl' = _")
apply (subst gtt_comp_lang)
apply auto[1]
apply (subst gtt_lang_fmap_states_gtt, simp)+
unfolding relcomp_map_both_adapt_vars_Restr image_comp prod.map_comp comp_def
apply (subst image_cong[OF refl, of _ _ "map_both adapt_vars"])
apply (auto simp: adapt_vars_idemp)[1]
unfolding relcomp_map_both_adapt_vars_Restr[symmetric]
apply (simp only: gtt_lang_inverse converse_Restr[symmetric] map_both_converse t)
done
have r: "map_both adapt_vars ` gtt_lang ?Gr =
Restr ((Restr (rstep R) {t. ground t})⇧*) {t. ground t} O (Restr ((Restr (rstep R) {t. ground t})⇧*) {t. ground t})¯"
(is "?Gr' = _")
apply (subst gtt_comp_lang)
apply auto[1]
apply (subst gtt_lang_fmap_states_gtt, simp)+
unfolding relcomp_map_both_adapt_vars_Restr image_comp prod.map_comp comp_def
apply (subst image_cong[OF refl, of _ _ "map_both adapt_vars"])
apply (auto simp: adapt_vars_idemp)[1]
unfolding relcomp_map_both_adapt_vars_Restr[symmetric]
apply (simp only: gtt_lang_inverse converse_Restr[symmetric] map_both_converse t)
done
have R_conv': "?R ⟷ ?Gl' ⊆ ?Gr'" unfolding R_conv
proof (intro iffI, goal_cases lr rl)
case lr then show ?case by (rule image_mono)
next
case rl
show ?case
using image_mono[OF rl, of "map_both (adapt_vars :: _ ⇒ ('a, ('a, 'b) term option + ('a, 'b) term option) term)"]
unfolding image_comp comp_def prod.map_comp
by (subst (asm) (1 2) image_cong[OF refl, of _ _ "λx. x"]) auto
qed
show ?thesis unfolding R_conv' l r
apply (subst CR_on_iff_CR_Restr, simp add: rstep_ground[of R] *)
unfolding CR_Restr_conv ..
qed
lemma inj_on_image_subset_iff:
"inj_on f (A ∪ B) ⟹ f ` A ⊆ f ` B ⟷ A ⊆ B"
by (metis image_Un inj_on_Un_image_eq_iff le_iff_sup sup.right_idem)
lemma inj_term_of_gterm:
"inj term_of_gterm"
by (metis injI term_of_gterm_inv)
lemma subset_ta_lang_GTT_to_RR2_conv:
"ta_lang (GTT_to_RR2 UNIV G1) ⊆ ta_lang (GTT_to_RR2 UNIV G2) ⟷ gtt_lang G1 ⊆ gtt_lang G2"
proof -
have *: "{gpair t u |t u. (t, u) ∈ map_both gterm_of_term ` X} = (case_prod gpair ∘ map_both gterm_of_term) ` X"
for X by force
show ?thesis
unfolding gta_lang_to_ta_lang[symmetric] GTT_to_RR2[unfolded RR2_spec_def, OF subset_UNIV]
inj_image_subset_iff[OF inj_term_of_gterm] *
apply (simp only: subset_UNIV UNIV_def[symmetric] UNIV_Times_UNIV Int_UNIV_right)
proof (intro inj_on_image_subset_iff inj_onI, goal_cases)
case (1 s t) obtain s1 t1 s2 t2 where [simp]: "s = (s1, s2)" "t = (t1, t2)" by (cases s; cases t)
have "ground s1" "ground s2" "ground t1" "ground t2" using 1(1,2) by auto
then show ?case using arg_cong[OF 1(3), of "λp. (term_of_gterm (gfst p), term_of_gterm (gsnd p))"]
by (auto 0 1 simp: comp_def gfst_gpair gsnd_gpair gterm_of_term_inv' dest!: adapt_vars_inj)
qed
qed
lemma GCR_criterion:
assumes "ground_trs R" "finite R"
shows "CR_on (rstep R) {t. ground t} ⟷
(let GR = GTT_trancl (some_rsteps_to_GTT R) in
ta_lang (GTT_to_RR2 UNIV ((GTT_comp' (prod.swap GR) GR))) ⊆
ta_lang (GTT_to_RR2 UNIV ((GTT_comp' GR (prod.swap GR)))))"
unfolding subset_ta_lang_GTT_to_RR2_conv using GCR_criterion_GTT[OF assms] .
lemma ground_trs_Var_rstep:
assumes "ground_trs R" "(s, t) ∈ (rstep R)" "is_Var s"
shows False using assms(2,3,1)
proof (induction rule:rstep_induct)
case (rule s t)
then show ?case unfolding ground_trs_def by fastforce
next
case (subst s t σ)
then have "is_Var s" by force
then show ?case
using subst.IH subst.prems(2) by blast
next
case (ctxt s t C)
have "is_Var s" using ctxt(2) by (metis ctxt_supteq supteq_Var_id term.collapse(1))
then show ?case using ctxt by simp
qed
lemma ground_trs_Var_trstep:
assumes "ground_trs R" "(s, t) ∈ (rstep R)⇧+" "is_Var s"
shows False
using assms(2,3,1)
proof (induction rule:trancl.induct)
case (r_into_trancl a b)
thus ?case using ground_trs_Var_rstep[of R a b] by argo
next
case (trancl_into_trancl a b c)
then show ?case by blast
qed
lemma ground_trs_Var_rtrstep:
assumes "ground_trs R" "(s, t) ∈ (rstep R)⇧*" "is_Var s"
shows "s = t"
using assms(2,3,1)
proof (cases "s = t")
case False
hence "(s, t) ∈ (rstep R)⇧+"
by (meson assms(2) rtranclD)
then show ?thesis using assms(1,3) ground_trs_Var_trstep by auto
qed (argo)
lemma ground_trancl:
assumes "ground_trs R" "(a,b) ∈ (rstep R)⇧*" "ground a"
shows "ground b"
using assms by (metis ground_trs_def ground_vars_term_empty rsteps_ground split_conv subsetI)
lemma ground_tranclI:
assumes "ground_trs R" "(a,b) ∈ (rstep R)⇧*" "ground b"
shows "ground a"
proof -
have "ground_trs (R¯)" using assms(1) unfolding ground_trs_def by fastforce
moreover have "(b,a) ∈ (rstep (R¯))⇧*" using assms(2) rtrancl_converseI by force
ultimately show ?thesis using assms(3)
using ground_trancl by blast
qed
lemma rel_exp:
"(R ∪ N)⇧* = N⇧* ∪ N⇧* O R O (N ∪ R)⇧*"
by regexp
lemma ground_rrstep:
assumes "ground_trs R" "(a,b) ∈ (rrstep R)"
shows "ground a" "ground b"
using assms rrstep_def'[of R] unfolding ground_trs_def
by (metis (no_types, lifting) case_prodD ground_subst_apply rrstepE) +
lemma CR_by_GCR:
assumes "ground_trs R"
shows "CR_on (rstep R) {t. ground t} ⟷ CR (rstep R)"
using assms
proof (intro iffI, goal_cases lr rl)
case rl
then show ?case unfolding CR_on_def by simp
next
case lr
{fix s u v
assume "(s,u) ∈ (rstep R)⇧*" "(s, v) ∈ (rstep R)⇧*"
hence "∃t. (u,t) ∈ (rstep R)⇧* ∧ (v, t) ∈ (rstep R)⇧*"
proof (induction s arbitrary: u v)
case (Var x)
have "u = Var x" "v = Var x"
using assms ground_trs_Var_rtrstep[of R "Var x" u]
Var.prems(1) apply blast
using Var.prems(2) assms
ground_trs_Var_rtrstep[of R "Var x" v]
by blast
then show ?case by blast
next
case (Fun f ss)
have rstep_split:
"(rstep R)⇧* = (nrrstep R)⇧* ∪ ((nrrstep R)⇧* O (rrstep R) O (nrrstep R ∪ rrstep R)⇧*)"
using rstep_iff_rrstep_or_nrrstep[of R] rel_exp[of "rrstep R" "nrrstep R"] by argo
{assume rstep_asm:"((Fun f ss, u) ∉ (nrrstep R)⇧*) ∨ ((Fun f ss, v) ∉ (nrrstep R)⇧*)"
then have "(u, v) ∈ (rstep R)⇧↓"
proof (rule disjE, goal_cases u v)
case u
with rstep_split obtain c d where c:"(Fun f ss,c) ∈ ((nrrstep R)⇧*)"
"(c,d) ∈ (rrstep R)"
"(d, u) ∈ (nrrstep R ∪ rrstep R)⇧*"
using Fun(2)
by auto
hence "ground c" using ground_rrstep[of R c d] assms by fastforce
with c(1) have "ground (Fun f ss)" using
ground_tranclI[of R "Fun f ss" c]
using assms rstep_split by auto
then show ?case using lr Fun(2,3) unfolding CR_on_def by blast
next
case v
with rstep_split obtain c d where c:"(Fun f ss,c) ∈ ((nrrstep R)⇧*)"
"(c,d) ∈ (rrstep R)"
"(d, v) ∈ (nrrstep R ∪ rrstep R)⇧*"
using Fun(3)
by auto
hence "ground c" using ground_rrstep[of R c d] assms by fastforce
with c(1) have "ground (Fun f ss)" using
ground_tranclI[of R "Fun f ss" c]
using assms rstep_split by auto
then show ?case using lr Fun(2,3) unfolding CR_on_def by blast
qed
}
note step1= this
{assume nrstep_asm:"(Fun f ss, u) ∈ (nrrstep R)⇧*" "(Fun f ss, v) ∈ (nrrstep R)⇧*"
then obtain us vs where us_vs:"u = Fun f us ∧ (length us = length ss)"
"v = Fun f vs ∧ (length vs = length ss)"
by (metis nrrsteps_preserve_root')
hence "∀i <length ss. (ss!i,us!i) ∈ (rstep R)⇧*"
"∀i <length ss. (ss!i,vs!i) ∈ (rstep R)⇧*"
using nrrsteps_imp_eq_root_arg_rsteps[of "Fun f ss" "Fun f us" R]
nrrsteps_imp_eq_root_arg_rsteps[of "Fun f ss" "Fun f vs" R]
nrstep_asm
by (simp add:us_vs)+
hence cond:"∀i < length ss. ∃ts⇩i. (us!i, ts⇩i) ∈ (rstep R)⇧* ∧ (vs!i, ts⇩i) ∈ (rstep R)⇧*"
by (meson Fun.IH nth_mem)
then have "∃t. (u, t) ∈ (rstep R)⇧* ∧ (v, t) ∈ (rstep R)⇧*"
proof -
obtain ts where "(length ts = length ss)"
"(∀i< length ss. ((us!i, ts!i) ∈ (rstep R)⇧*) ∧ ((vs!i, ts!i) ∈ (rstep R)⇧*))"
using construct_exI'[OF cond] by blast
hence "(length ts = length ss) " "((u, Fun f ts) ∈ (rstep R)⇧*) ∧ (v, Fun f ts) ∈ (rstep R)⇧*"
using us_vs by (simp add: us_vs(1) us_vs(2) args_rsteps_imp_rsteps)+
then show ?thesis by blast
qed
}
with step1 show ?case by blast
qed}
then show ?case unfolding CR_defs
by (meson joinI)
qed
end