theory LLRG_Confluence_Impl
imports Ground_Confluence_Impl LLRG_Confluence
begin
text ‹CR procedure for left-linear, right-ground systems›
definition llrg_cr_procedure_wrap :: "(nat list × nat) list ⇒ ((nat list, nat list) term × (nat list, nat list) term) list ⇒ answer" where
"llrg_cr_procedure_wrap F R =
(if left_linear_trs (set R) ∧ right_ground_trs (set R) ∧ funas_trs (set R) ⊆ set F
then case lv_gcr_procedure_rbt (rbt_bulkload (map (λx. (x, ())) ((None, 0) # map (map_prod Some id) F))) (rbt_bulkload (map (λx. (x, ())) (map (map_both (map_funs_term Some)) R))) of
dRETURN True ⇒ YES
| dRETURN False ⇒ NO
| _ ⇒ MAYBE
else MAYBE)"
lemma map_CR:
assumes "inj f"
shows "CR (map_both f ` R) ⟷ CR R"
proof -
note [simp] = trancl_converse Ground_Confluence_Impl.map_both_converse map_both_relcomp inj_on_by_inj[OF assms] trancl_map_both_Restr[OF assms, simplified]
{ fix s t assume R: "R⇧↑ ⊆ R⇧↓" and st: "(s, t) ∈ (map_both f ` R)⇧↑"
have *: "s = t ∨ (∃s' t'. s = f s' ∧ t = f t')" using st
by (fastforce simp: meet_def simp flip: reflcl_trancl)
have "(inv f s, inv f t) ∈ R⇧↑" using imageI[OF st, of "map_both (inv f)"] assms
by (fastforce simp: meet_def simp flip: reflcl_trancl)
then have "(inv f s, inv f t) ∈ R⇧↓" using R by blast
from imageI[OF this, of "map_both f"] have "(s, t) ∈ (map_both f ` R)⇧↓" using assms *
by (fastforce simp add: join_def simp flip: reflcl_trancl)
} moreover
{ fix s t assume R: "(map_both f ` R)⇧↑ ⊆ (map_both f ` R)⇧↓" and st: "(s, t) ∈ R⇧↑"
have "(f s, f t) ∈ (map_both f ` R)⇧↑" using imageI[OF st, of "map_both f"] assms
by (fastforce simp: meet_def simp flip: reflcl_trancl)
then have "(f s, f t) ∈ (map_both f ` R)⇧↓" using R by blast
from imageI[OF this, of "map_both (inv f)"] have "(s, t) ∈ R⇧↓" using assms
by (fastforce simp: join_def simp flip: reflcl_trancl)
} ultimately show ?thesis unfolding CR_iff_meet_subset_join by auto
qed
lemma map_prod_times:
"map_prod f g ` (X × Y) = f ` X × g ` Y"
by auto
lemma funas_trs_map_funs_trs [simp]:
"funas_trs (map_funs_trs f R) = map_prod f id ` funas_trs R"
using image_iff
by (fastforce simp: map_funs_trs.simps funas_trs_def funas_rule_def funas_term_map_funs_term
intro!: map_prod_imageI[of _ _ _ f id, simplified])
lemma sig_step_def':
"sig_step F R = Restr R {t. funas_term t ⊆ F}"
by (auto simp: sig_step_def)
lemma map_funs_rule_def':
"map_funs_rule f = map_both (map_funs_term f)"
by auto
lemma map_funs_trs_def':
"map_funs_trs f R = map_both (map_funs_term f) ` R"
by (auto simp: map_funs_trs.simps map_funs_rule_def')
lemma term_from_mapped_signature:
assumes "funas_term t ⊆ map_prod h id ` F"
obtains t' where "funas_term t' ⊆ F" "t = map_funs_term h t'"
using assms
proof (induct t arbitrary: thesis)
case (Var x)
show ?case using Var(1)[of "Var x"] by simp
next
case (Fun f ts)
obtain f' where [simp]: "(f', length ts) ∈ F" "f = h f'" using Fun(3) by auto
{
fix i assume i: "i < length ts"
have "funas_term (ts ! i) ⊆ map_prod h id ` F" using i funas_subterm[OF Fun(3)] by blast
then obtain ti' where "funas_term ti' ⊆ F" "ts ! i = map_funs_term h ti'"
using Fun(1)[of "ts ! i"] i by (auto simp add: id_def)
then have "∃ti'. funas_term ti' ⊆ F ∧ ts ! i = map_funs_term h ti'" by metis }
then obtain ts' where *: "funas_term (ts' i) ⊆ F" and [simp]: "map_funs_term h (ts' i) = ts ! i"
if "i < length ts" for i using that by metis
show ?case using subsetD[OF *]
by (intro Fun(2)[of "Fun f' (map ts' [0..<length ts])"]) (auto intro: nth_equalityI)
qed
lemma llrg_cr_procedure_wrap_sound:
shows "llrg_cr_procedure_wrap F R = YES ⟶ CR (Restr (rstep (set R)) {t. funas_term t ⊆ set F})" (is ?T)
and "llrg_cr_procedure_wrap F R = NO ⟶ ¬ CR (Restr (rstep (set R)) {t. funas_term t ⊆ set F})" (is ?F)
proof -
{ let ?R = "map_funs_trs Some (set R)"
assume m: "llrg_cr_procedure_wrap F R ≠ MAYBE"
then have pre: "left_linear_trs (set R)" "right_ground_trs (set R)" "funas_trs (set R) ⊆ set F"
by (auto simp: llrg_cr_procedure_wrap_def split: if_splits)
have *: "map_funs_term Some ` {t. funas_term t ⊆ set F} = {t. funas_term t ⊆ map_prod Some id ` set F}"
by (auto simp: funas_term_map_funs_term intro!: map_prod_imageI[of _ _ _ Some id, simplified] imageI
elim: term_from_mapped_signature)
have **: "sig_step (map_prod Some id ` set F) (rstep ?R) =
Restr (map_both (map_funs_term Some) ` rstep (set R)) (map_funs_term Some ` {t. funas_term t ⊆ set F})"
using pre(3) unfolding sig_step_def' *
apply (intro equalityI)
subgoal by (auto elim!: term_from_mapped_signature dest!: rstep_imp_map_rstep[of _ _ ?R the]
simp: term.map_comp comp_def term.map_ident map_funs_trs_comp map_funs_trs_id[unfolded id_def])
subgoal by (auto dest!: rstep_imp_map_rstep[of _ _ "set R" Some])
done
have pre': "left_linear_trs ?R" "right_ground_trs ?R" "funas_trs ?R ⊆ map_prod Some id ` set F"
subgoal using pre(1) by simp
subgoal using pre(2) by (auto simp: right_ground_trs_def map_funs_trs.simps)
subgoal using pre(3) by auto
done
have *: "left_linear_trs ?R" "right_ground_trs ?R" using pre
by - (simp, fastforce simp: right_ground_trs_def map_funs_trs.simps split: prod.splits)
have lv: "lv_trs ?R" using *
unfolding lv_trs_code left_linear_trs_def right_ground_trs_def ground_vars_term_empty
linear_term.simps is_partition_def
by (fastforce simp add: ground_imp_linear_term[unfolded ground_vars_term_empty] split: prod.splits)
have llrg: "llrg ?R" using * by (auto simp: left_linear_trs_def right_ground_trs_def llrg_def)
define foo where "foo = lv_gcr_procedure_rbt
(rbt_bulkload
(map (λx. (x, ())) ((None, 0) # map (map_prod Some id) F)))
(rbt_bulkload
(map (λx. (x, ())) (map (map_both (map_funs_term Some)) R)))"
define bar where "bar = CR (Restr (rstep (map_both (map_funs_term Some) ` set R))
{s. ground s ∧
funas_term s ⊆ insert (None, 0) (map_prod Some id ` set F)})"
have "llrg_cr_procedure_wrap F R = YES ⟷ CR (Restr (rstep (set R)) {t. funas_term t ⊆ set F})"
apply (subst map_CR[symmetric, of "map_funs_term Some"], simp add: map_funs_term_inj)
apply (subst image_Int, simp add: prod.inj_map map_funs_term_inj)
unfolding map_prod_times **[symmetric]
apply (subst CR_GCR_equiv[OF llrg pre'(3), of None], (auto)[1])
apply (subst CR_on_iff_CR_Restr)
unfolding sig_step_def'
subgoal for s t using pre'(2) rstep_ground_llrg[OF llrg] by auto
apply (subst Restr_subset, (auto)[1])
using pre'(3) lv m
order.trans[OF lv_gcr_procedure_rbt.refine[OF rbt_bulkload_comp_rs_rel rbt_bulkload_comp_rs_rel, unfolded in_nres_rel_iff conc_Id id_def] lv_gcr_procedure_sound, of "map (map_both (map_funs_term Some)) R" "(None, 0) # map (map_prod Some id) F"]
by (auto simp: llrg_cr_procedure_wrap_def map_funs_trs_def' split: if_splits dres.splits bool.splits)
}
then show ?F ?T by force+
qed
export_code YES NO MAYBE ta_size_rbt tal_size dRETURN cr_procedure lv_gcr_procedure_wrap llrg_cr_procedure_wrap Var Fun nat_of_integer rec_term funas_trs set in Haskell module_name GCR file code
end