theory Ground_Confluence_Impl
imports GTT_RRn GTT_Transitive_Closure_Impl GTT_TRS_Impl GTT_RRn_Impl
TA.Tree_Automata_Containment_Impl LV_to_GTT_Impl TA_Simplify_Impl
begin
subsection ‹LV-TRS decision procedure›
term trs_to_gtt
term GTT_trancl
term GTT_comp
term GTT_to_RR2
term ta_lang_containment
term lv_trs_to_gtt_impl
term GTT_trancl_rbt
term GTT_comp_rbt
term GTT_to_RR2_impl
term ta_lang_containment_impl
definition lv_gcr_procedure :: "_ ⇒ (_ :: compare_order, _ :: compare_order) trs ⇒ _" where
"lv_gcr_procedure F R = do {
let Gr = fixed_signature.trs_to_gtt F R;
let GS = GTT_trancl Gr;
let GM = prod.swap GS;
let GL0 = GTT_comp (map_both (fmap_states_ta Inl) GM) (map_both (fmap_states_ta Inr) GS);
let GR0 = GTT_comp (map_both (fmap_states_ta Inr) GS) (map_both (fmap_states_ta Inl) GM);
let GL1 = trim_gtt GL0;
let GR1 = trim_gtt GR0;
let GL = GTT_to_RR2 F GL1;
let GR = GTT_to_RR2 F GR1;
GL' ← ta_nat GL;
GR' ← ta_nat GR;
let GL'' = trim_ta GL';
let GR'' = trim_ta GR';
ASSUME (ta_finite GL'');
ASSUME (ta_finite GR'');
res :: (_, unit) term xoption ← ta_lang_containment GL'' GR'';
RETURN (case res of XNone ⇒ True | XSome _ ⇒ False)
}"
lemma ta_lang_containment_impl_ref:
shows "(λA B. RETURN (ta_lang_containment_impl A B), ta_lang_containment) ∈ dflt_ta_rel →⇩r dflt_ta_rel →⇩r ⟨⟨⟨Id, Id⟩term_rel⟩xoption_rel⟩nres_rel"
by (intro fun_relI nres_relI[OF ta_lang_containment_impl.refine])
lemma ta_trim_autoref:
"(ta_only_prs_code ∘ ta_only_res_code, trim_ta) ∈ dflt_ta_rel →⇩r dflt_ta_rel"
unfolding trim_ta_def comp_def using ta_only_res_autoref dflt_TA_rel_finite
conc_trans_additional(1)[OF ta_only_prs_code.refine[unfolded in_nres_rel_iff] ta_only_prs]
by (refine_vcg) (blast dest: fun_relD RETURN_ref_RETURND)
lemma ta_nat_impl_autoref:
shows "(λA. RETURN (ta_nat_impl A), ta_nat) ∈ dflt_ta_rel →⇩r ⟨dflt_ta_rel⟩nres_rel"
by (intro fun_relI ta_nat_impl.refine)
lemma GTT_trancl_rbt_autoref:
"(λG. nres_of (GTT_trancl_rbt G), λG. RETURN (GTT_trancl G)) ∈ dflt_gtt_rel →⇩r ⟨dflt_gtt_rel⟩nres_rel"
by (intro fun_relI GTT_trancl_rbt.refine)
lemma GTT_comp_rbt_autoref:
"(λG1 G2. nres_of (GTT_comp_rbt G1 G2), λG1 G2. RETURN (GTT_comp G1 G2)) ∈ dflt_gtt_rel →⇩r dflt_gtt_rel →⇩r ⟨dflt_gtt_rel⟩nres_rel"
by (intro fun_relI GTT_comp_rbt.refine)
lemma ta_make_autoref':
"FORCE_id R1 ⟹ FORCE_id R2 ⟹ FORCE_id R3 ⟹ FORCE_id R4 ⟹ FORCE_id R5 ⟹ (ta_make_code, ta.make) ∈ ⟨R1⟩comp_rs_rel → ⟨⟨R2, R3⟩ta_rule_rel⟩comp_rs_rel → ⟨R4 ×⇩r R5⟩list_set_rel → dflt_ta_rel"
using ta_make_autoref by simp
schematic_goal GTT_to_RR2_rbt:
notes [autoref_rules] = param_replicate param_zip_fill ta_make_autoref'
shows "(?f, GTT_to_RR2)
∈ ⟨Id ×⇩r Id⟩comp_rs_rel → dflt_ta_rel ×⇩r dflt_ta_rel → dflt_ta_rel"
unfolding GTT_to_RR2_def[abs_def] parallel_closure_automaton_def GTT_to_RR2_root_def pair_automaton_def
ta_make_simps ta.simps ta.make_def comp_def map_prod_def
unfolding set_comprehension_aux image_comp comp_def ta.make_def[symmetric]
by autoref
concrete_definition GTT_to_RR2_rbt uses GTT_to_RR2_rbt
lemma GTT_to_RR2_rbt_autoref:
"FORCE_id R ⟹
(GTT_to_RR2_rbt, GTT_to_RR2) ∈ ⟨R⟩comp_rs_rel → dflt_ta_rel ×⇩r dflt_ta_rel → dflt_ta_rel"
using GTT_to_RR2_rbt.refine by simp
lemma map_both_autoref:
"(map_both, map_both) ∈ (R →⇩r R') →⇩r (R ×⇩r R →⇩r R' ×⇩r R')"
by (auto dest: fun_relD)
lemma prod_swap_autoref:
"(prod.swap, prod.swap) ∈ R ×⇩r R' →⇩r R' ×⇩r R"
by auto
lemma image_impl':
fixes f :: "'a :: compare ⇒ 'b :: compare"
assumes "FORCE_id R" "FORCE_id R'"
shows "(RBT_Impl.ord.rbt_bulkload (comp2lt compare_res) ∘ map (λx. (f x, ())) ∘ RBT_Impl.keys, λX. f ` X)
∈ ⟨R⟩comp_rs_rel → ⟨R'⟩comp_rs_rel"
using assms image_impl[of f] by simp
lemma inj_on_by_inj:
"inj f ⟹ inj_on f X"
unfolding inj_on_def by auto
lemma ASSUME_autoref:
"P ⟹ (RETURN (), ASSUME P) ∈ ⟨Id⟩nres_rel"
by refine_vcg auto
lemma ta_finite_restrict_ta:
"ta_finite A ⟹ ta_finite (ta_restrict A X)"
by (auto simp: ta_finite_def ta_restrict_def)
lemma ta_finite_trim_ta:
"ta_finite A ⟹ ta_finite (trim_ta A)"
by (auto simp: trim_ta_def ta_finite_restrict_ta)
"foo?"">lemma "foo?":
"FORCE_id (⟨Id, Id⟩ta_rule_rel)"
by simp
definition ta_only_reach' where
"ta_only_reach' A = ta_only_reach A"
definition ta_only_prod' where
"ta_only_prod' A = ta_only_prod A"
lemma ta_final_update_def':
"ta_final_update f A = ta.make (f (ta_final A)) (ta_rules A) (ta_eps A)"
by (cases A) auto
schematic_goal ta_final_update_impl:
assumes "FORCE_id R"
shows "(?f, ta_final_update) ∈ (⟨R⟩comp_rs_rel →⇩r ⟨R⟩comp_rs_rel) →⇩r dflt_ta_rel →⇩r dflt_ta_rel"
unfolding ta_final_update_def' assms[simplified]
by autoref
concrete_definition ta_final_update_impl uses ta_final_update_impl
lemma ta_only_prod'_autoref:
"(ta_only_prs_code, ta_only_prod') ∈ dflt_ta_rel →⇩r dflt_ta_rel"
by (intro fun_relI RETURN_ref_RETURND[OF conc_trans_additional(1)[OF ta_only_prs_code.refine[unfolded in_nres_rel_iff] ta_only_prs[OF dflt_TA_rel_finite]], folded ta_only_prod'_def])
lemmas ta_only_reach'_autoref = ta_only_res_autoref[folded ta_only_reach'_def]
schematic_goal trim_gtt_impl:
notes [autoref_rules] = ta_final_update_impl.refine ta_only_prod'_autoref ta_only_reach'_autoref
shows "(?f, trim_gtt) ∈ dflt_gtt_rel →⇩r dflt_gtt_rel"
unfolding trim_gtt_def gtt_only_reach_def gtt_only_prod_def comp_def Let_def fst_map_prod snd_map_prod
ta_only_reach'_def[symmetric] ta_only_prod'_def[symmetric] map_prod_def
by autoref
concrete_definition trim_gtt_impl uses trim_gtt_impl[THEN fun_relD]
schematic_goal lv_gcr_procedure_rbt:
notes [autoref_rules] = ta_lang_containment_impl_ref ta_trim_autoref ta_nat_impl_autoref
GTT_trancl_rbt_autoref GTT_comp_rbt_autoref GTT_to_RR2_rbt_autoref ta_make_autoref'
map_both_autoref prod_swap_autoref
shows "(?f, lv_gcr_procedure) ∈ ⟨Id ×⇩r Id⟩comp_rs_rel →⇩r ⟨⟨Id,Id⟩term_rel ×⇩r ⟨Id,Id⟩term_rel⟩comp_rs_rel →⇩r ⟨Id⟩nres_rel"
unfolding lv_gcr_procedure_def fmap_states_ta_def[folded ta.make_def]
let_to_bind_conv[of "GTT_trancl _"] let_to_bind_conv[of "GTT_comp _ _"]
unfolding Let_def
using [[autoref_trace_failed_id]]
apply (rule HOL.back_subst[of "λx. (x, _) ∈ _"])
apply (rule fun_relI)+
apply (rule autoref_bind[THEN fun_relD, THEN fun_relD])
apply (rule GTT_trancl_rbt.refine)
apply (rule trs_to_gtt_autoref[THEN fun_relD, THEN fun_relD], assumption, assumption)
apply (rule fun_relI)
apply (rule autoref_bind[THEN fun_relD, THEN fun_relD])
apply (rule GTT_comp_rbt.refine)
apply (rule map_both_autoref[THEN fun_relD, THEN fun_relD])
apply (rule fun_relI)
apply (rule ta_make_autoref[THEN fun_relD, THEN fun_relD, THEN fun_relD])
apply (rule image_impl[THEN fun_relD])
apply (rule ta_impl_autoref(1)[THEN fun_relD], assumption)
apply (rule image_impl'[THEN fun_relD])
apply (rule "foo?")
apply simp
apply (rule ta_impl_autoref(2)[THEN fun_relD])
apply assumption
apply (rule list_set_autoref_inj_image[simplified])
apply (rule prod.inj_map[OF inj_Inl inj_Inl, unfolded map_prod_def, THEN inj_on_by_inj])
apply (subst prod_rel_id_simp)
apply (subst fun_rel_id_simp)
apply (rule IdI)
apply (rule ta_impl_autoref(3)[THEN fun_relD, unfolded prod_rel_id_simp], assumption)
apply (rule prod_swap_autoref[THEN fun_relD], assumption)
apply (rule map_both_autoref[THEN fun_relD, THEN fun_relD])
apply (rule fun_relI)
apply (rule ta_make_autoref[THEN fun_relD, THEN fun_relD, THEN fun_relD])
apply (rule image_impl[THEN fun_relD])
apply (rule ta_impl_autoref(1)[THEN fun_relD], assumption)
apply (rule image_impl'[THEN fun_relD])
apply (rule "foo?")
apply simp
apply (rule ta_impl_autoref(2)[THEN fun_relD])
apply assumption
apply (rule list_set_autoref_inj_image[simplified])
apply (rule prod.inj_map[OF inj_Inr inj_Inr, unfolded map_prod_def, THEN inj_on_by_inj])
apply (subst prod_rel_id_simp)
apply (subst fun_rel_id_simp)
apply (rule IdI)
apply (rule ta_impl_autoref(3)[THEN fun_relD, unfolded prod_rel_id_simp], assumption)
apply (assumption)
apply (rule fun_relI)
apply (rule autoref_bind[THEN fun_relD, THEN fun_relD])
apply (rule GTT_comp_rbt_autoref[THEN fun_relD, THEN fun_relD])
apply (rule map_both_autoref[THEN fun_relD, THEN fun_relD])
apply (rule fun_relI)
apply (rule ta_make_autoref[THEN fun_relD, THEN fun_relD, THEN fun_relD])
apply (rule image_impl[THEN fun_relD])
apply (rule ta_impl_autoref(1)[THEN fun_relD], assumption)
apply (rule image_impl'[THEN fun_relD])
apply (rule "foo?")
apply simp
apply (rule ta_impl_autoref(2)[THEN fun_relD])
apply assumption
apply (rule list_set_autoref_inj_image[simplified])
apply (rule prod.inj_map[OF inj_Inr inj_Inr, unfolded map_prod_def, THEN inj_on_by_inj])
apply (subst prod_rel_id_simp)
apply (subst fun_rel_id_simp)
apply (rule IdI)
apply (rule ta_impl_autoref(3)[THEN fun_relD, unfolded prod_rel_id_simp], assumption)
apply (assumption)
apply (rule map_both_autoref[THEN fun_relD, THEN fun_relD])
apply (rule fun_relI)
apply (rule ta_make_autoref[THEN fun_relD, THEN fun_relD, THEN fun_relD])
apply (rule image_impl[THEN fun_relD])
apply (rule ta_impl_autoref(1)[THEN fun_relD], assumption)
apply (rule image_impl'[THEN fun_relD])
apply (rule "foo?")
apply simp
apply (rule ta_impl_autoref(2)[THEN fun_relD])
apply assumption
apply (rule list_set_autoref_inj_image[simplified])
apply (rule prod.inj_map[OF inj_Inl inj_Inl, unfolded map_prod_def, THEN inj_on_by_inj])
apply (subst prod_rel_id_simp)
apply (subst fun_rel_id_simp)
apply (rule IdI)
apply (rule ta_impl_autoref(3)[THEN fun_relD, unfolded prod_rel_id_simp], assumption)
apply (rule prod_swap_autoref[THEN fun_relD], assumption)
apply (rule fun_relI)
apply (rule autoref_bind[THEN fun_relD, THEN fun_relD])
apply (rule ta_nat_impl_autoref[THEN fun_relD])
apply (rule GTT_to_RR2_rbt.refine[THEN fun_relD, THEN fun_relD])
apply assumption
apply (rule trim_gtt_impl.refine)
apply assumption
apply (rule fun_relI)
apply (rule autoref_bind[THEN fun_relD, THEN fun_relD])
apply (rule ta_nat_impl_autoref[THEN fun_relD])
apply (rule GTT_to_RR2_rbt.refine[THEN fun_relD, THEN fun_relD])
apply assumption
apply (rule trim_gtt_impl.refine)
apply assumption
apply (rule fun_relI)
apply (rule autoref_bind[THEN fun_relD, THEN fun_relD])
apply (rule ASSUME_autoref)
apply (rule ta_finite_trim_ta)
apply (simp only: dflt_TA_rel_finite)
apply (rule fun_relI)
apply (rule autoref_bind[THEN fun_relD, THEN fun_relD])
apply (rule ASSUME_autoref)
apply (rule ta_finite_trim_ta)
apply (simp only: dflt_TA_rel_finite)
apply (rule fun_relI)
apply (rule autoref_bind[THEN fun_relD, THEN fun_relD])
apply (rule ta_lang_containment_impl_ref[THEN fun_relD, THEN fun_relD])
apply (rule ta_trim_autoref[THEN fun_relD])
apply assumption
apply (rule ta_trim_autoref[THEN fun_relD])
apply assumption
apply (rule fun_relI)
apply (rule param_RETURN[THEN fun_relD])
apply (rule xoption_autoref(3)[THEN fun_relD, THEN fun_relD, THEN fun_relD])
apply (rule IdI)
apply (rule fun_relI)
apply (rule IdI)
apply assumption
unfolding nres_of_simps(3)[symmetric] nres_of_bind[symmetric]
by (rule refl)
concrete_definition lv_gcr_procedure_rbt uses lv_gcr_procedure_rbt[THEN fun_relD, THEN fun_relD]
lemma Restr_trancl_Restr':
"R `` X ⊆ X ⟹ Restr (R⇧+) X = (Restr R X)⇧+"
using trancl_restrict_reachable[of _ _ R X] subsetD[OF trancl_mono_set[of "Restr R X" R]]
by (auto dest: tranclD tranclD2)
lemma Restr_converse:
"Restr (A¯) X = (Restr A X)¯"
by auto
lemma map_both_converse:
"(map_both f ` A)¯ = map_both f ` (A¯)"
by auto
lemma ta_syms_fmap_states_ta:
"ta_syms (fmap_states_ta f A) = ta_syms A"
by (auto simp: ta_syms_def fmap_states_ta_def split: ta_rule.splits intro: rev_image_eqI)
lemma (in fixed_signature) gtt_syms_trs_to_gtt:
assumes "funas_trs R ⊆ ℱ"
shows "gtt_syms (trs_to_gtt R) ⊆ ℱ"
proof -
have [dest!]: "map_vars_term h t ⊵ Fun f ts ⟹ (f, length ts) ∈ funas_term t" for h t f ts
by (drule supteq_imp_funas_term_subset) simp
show ?thesis using assms
by (auto simp: trs_to_gtt_def trs_to_ta_L_def trs_to_ta_R_def ta_syms_def
L_trs_ta_set_def R_trs_ta_set_def term_to_ta_L_def term_to_ta_R_def fmap_states_ta_def
term_to_ta_def term_TA_def embed_term_def subsetD[OF lhs_wf] subsetD[OF rhs_wf]
split: ta_rule.splits)
qed
lemma ta_restrict_finite:
"ta_finite A ⟹ ta_finite (ta_restrict A X)"
by (auto simp: ta_finite_def ta_restrict_def)
lemma trim_ta_finite:
"ta_finite A ⟹ ta_finite (trim_ta A)"
unfolding trim_ta_def by (intro ta_restrict_finite)
lemma ta_lang_subset_conv:
"ta_lang A ⊆ ta_lang B ⟷ gta_lang A ⊆ gta_lang B"
by (metis gta_lang_to_ta_lang gta_lang_def_sym image_mono)
lemma cancel_image:
"inj_on f (A ∪ B) ⟹ f ` A ⊆ f ` B ⟷ A ⊆ B"
by (auto dest!: subsetD inj_onD)
lemma Restr_relcomp:
"A `` X ⊆ X ⟹ Restr (A O B) X = Restr A X O Restr B X"
"B¯ `` X ⊆ X ⟹ Restr (A O B) X = Restr A X O Restr B X"
by auto
lemma map_both_relcomp:
"inj_on f (snd ` A ∪ fst ` B) ⟹ map_both f ` A O map_both f ` B = map_both f ` (A O B)"
by (force simp: inj_on_def intro: rev_image_eqI)
lemma map_trancl:
"map_both f ` R⇧+ ⊆ (map_both f ` R)⇧+"
proof (intro subrelI)
fix x y assume "(x, y) ∈ map_both f ` R⇧+"
then obtain u v where xy: "x = f u" "y = f v" and *: "(u, v) ∈ R⇧+" by auto
show "(x, y) ∈ (map_both f ` R)⇧+" unfolding xy using *
by (induct) (blast, meson map_prod_imageI trancl.simps)
qed
lemma map_trancl':
assumes "R ⊆ X × X" "inj_on f X"
shows "map_both f ` R⇧+ = (map_both f ` R)⇧+"
apply (intro equalityI map_trancl subrelI)
subgoal for x y using image_mono[OF map_trancl[of "inv_into X f" "map_both f ` R"], of "map_both f"]
unfolding image_comp comp_def prod.map_comp
apply (subst (asm) (1 2) image_cong[OF refl, of _ _ id])
subgoal using assms(1) by (auto split: prod.splits simp: map_prod_def inv_into_f_f[OF assms(2)])
subgoal using assms(1) by (auto 0 3 split: prod.splits simp: map_prod_def f_inv_into_f dest: tranclD tranclD2)
subgoal by auto
done
done
lemma gtt_lang_preserves_sig:
assumes "gtt_syms G ⊆ F" "funas_term s ⊆ F" "(s, t) ∈ gtt_lang G"
shows "funas_term t ⊆ F"
proof -
obtain ss ts C where
s: "s = fill_holes C ss" "length ss = num_holes C" and
t: "t = fill_holes C ts" "length ts = num_holes C" and
h: "⋀i. i < num_holes C ⟹ ∃q. q ∈ ta_res (fst G) (ss ! i) ∧ q ∈ ta_res (snd G) (ts ! i)"
using assms(3)
by (auto 0 0 simp: gtt_accept_equiv elim!: gtt_accept'.cases)
have "funas_mctxt C ⊆ F" using s assms(2) by (auto simp: funas_mctxt_fill_holes)
moreover have "funas_term (ts ! i) ⊆ F" if "i < num_holes C" for i
using h[OF that] assms(1) by (auto dest: ta_syms_res)
ultimately show ?thesis using t(2)
unfolding t(1) by (fastforce simp: funas_mctxt_fill_holes in_set_conv_nth)
qed
lemmas trancl_trancl = tranclp_idemp[to_set]
lemma inj_on_gterm_of_term:
"inj_on gterm_of_term {t. ground t}"
by (unfold inj_on_def, metis gterm_of_term_inv mem_Collect_eq)
lemma trancl_Restr_parstep:
"(Restr (par_rstep R) {t. ground t ∧ funas_term t ⊆ F})⇧+ = (Restr ((rstep R)⇧=) {t. ground t ∧ funas_term t ⊆ F})⇧+"
(is "?L = ?R")
proof (rule equalityI, goal_cases LR RL)
case LR
have "?L ⊆ ?R⇧+"
proof (intro trancl_mono_set subrelI, elim IntE SigmaE2 CollectE conjE, goal_cases)
case (1 s t) then show ?case
proof (induct rule: par_rstep.induct)
case (par_step_fun ts ss f)
let ?r = "Restr ((rstep R)⇧=) {t. ground t ∧ funas_term t ⊆ F}"
have "(Fun f ss, Fun f (take i ts @ drop i ss)) ∈ ?r⇧+" if "i ≤ length ts" for i using that
proof (induct i)
case 0 then show ?case using par_step_fun(4-5) by (auto 0 4)
next
case (Suc i)
have *: "(ss ! i, ts ! i) ∈ (Restr ((rstep R)⇧=) {t. ground t ∧ funas_term t ⊆ F})⇧+"
using Suc(2) par_step_fun(3-)
by (intro par_step_fun(2)) (auto simp: UN_subset_iff)
show ?case using Suc(2)
apply (subst take_Suc_conv_app_nth, simp)
apply (rule trancl_trans[OF Suc(1)], simp)
apply (subst Cons_nth_drop_Suc[symmetric], simp add: par_step_fun(3))
unfolding append.assoc append.simps
apply (intro subset_trans[OF map_trancl[of _ ?r], THEN subsetD, OF _ imageI[OF *],
unfolded map_prod_def prod.simps] trancl_mono_set subrelI IntI)
subgoal by (auto intro: ctxt_closed_one)
using Suc(2) par_step_fun(3-)
by (force simp: UN_subset_iff dest!: in_set_takeD in_set_dropD)
qed
from this[of "length ts"] show ?case using par_step_fun(3) by simp
qed (auto 0 3)
qed
then show ?case by simp
next
case RL show ?case by (intro trancl_mono_set Int_mono rstep_par_rstep Un_least) auto
qed
lemma lv_gcr_procedure_sound:
assumes "lv_trs R" "funas_trs R ⊆ F"
shows "lv_gcr_procedure F R ≤ SPEC ((=) (CR (Restr (rstep R) {t. ground t ∧ funas_term t ⊆ F})))"
proof -
define r where "r = map_both gterm_of_term ` Restr ((rstep R)⇧=) {t. ground t ∧ funas_term t ⊆ F}"
define Gr where "Gr = fixed_signature.trs_to_gtt F R"
note Gr = fixed_signature.gtt_lang_trs_to_gtt[OF assms(1), of F, unfolded fixed_signature.st_def]
define GS where "GS = GTT_trancl Gr"
have GS: "ggtt_lang F GS = r⇧+"
unfolding GS_def Gr_def GTT_trancl_lang r_def
apply (subst Restr_trancl_Restr')
subgoal using gtt_lang_preserves_sig[OF fixed_signature.gtt_syms_trs_to_gtt[OF assms(2)]] by blast
unfolding Gr
apply (subst map_trancl'[OF _ inj_on_gterm_of_term], (auto)[1])
unfolding image_comp comp_def prod.map_comp adapt_vars_def
apply (subst image_cong[OF refl, of _ _ "map_both gterm_of_term"], (auto simp: gterm.map_ident)[1])
apply (subst (1 2) map_trancl'[OF _ inj_on_gterm_of_term, symmetric], (auto)[2])
apply (intro arg_cong[of _ _ "(`) _"] trancl_Restr_parstep)
done
define GM where "GM = prod.swap GS"
have GM: "ggtt_lang F GM = (r¯)⇧+" using `ggtt_lang F GS = r⇧+`
unfolding GM_def gtt_lang_swap[of "fst GS" "snd GS", folded prod.swap_def, symmetric]
Restr_converse map_both_converse[symmetric] trancl_converse by simp
have **: "gtt_syms GM ⊆ F" "gtt_syms GS ⊆ F"
unfolding GM_def GS_def gtt_syms_GTT_trancl fst_swap snd_swap Un_commute[of "ta_syms (snd _)"] Un_absorb
unfolding Gr_def using fixed_signature.gtt_syms_trs_to_gtt[OF assms(2)] by assumption+
define GL0 where "GL0 = GTT_comp (map_both (fmap_states_ta Inl) GM) (map_both (fmap_states_ta Inr) GS)"
have *: "map_both gterm_of_term ` Restr (map_both adapt_vars ` R) {t. funas_term t ⊆ F} =
map_both gterm_of_term ` Restr R {t. funas_term t ⊆ F}" if "R ⊆ {t. ground t} × {t. ground t}"
for R :: "('a, ('a, unit) Term.term + ('a, unit) Term.term) term rel"
using subsetD[OF that]
apply (intro equalityI subrelI)
subgoal for x y
by (rule rev_image_eqI[of "map_both term_of_gterm (x, y)"]) (auto simp: gterm_of_term_inv')
subgoal for x y by (auto intro!: rev_image_eqI[of "map_both term_of_gterm (x, y)"]
simp: gterm_of_term_inv' adapt_vars_def gterm.map_ident)
done
have GL0: "ggtt_lang F GL0 = (r¯)⇧+ O r⇧+"
unfolding GL0_def
apply (subst gtt_comp_lang, (auto)[1])
apply (subst Restr_relcomp(1))
subgoal using gtt_lang_preserves_sig[of "fmap_states_gtt Inl GM"] **(1)
by (auto simp: ta_syms_fmap_states_ta)
apply (subst map_both_relcomp[symmetric])
subgoal unfolding inj_on_def
by (intro ballI impI, subst (1 2) gterm_of_term_inv[symmetric]) fastforce+
by (simp_all add: gtt_lang_fmap_states_gtt * GM GS)
define GR0 where "GR0 = GTT_comp (fmap_states_gtt Inr GS) (fmap_states_gtt Inl GM)"
have GR0: "ggtt_lang F GR0 = r⇧+ O (r¯)⇧+"
unfolding GR0_def
apply (subst gtt_comp_lang, (auto)[1])
apply (subst Restr_relcomp(1))
subgoal using gtt_lang_preserves_sig[of "fmap_states_gtt Inr GS"] **(2)
by (auto simp: ta_syms_fmap_states_ta)
apply (subst map_both_relcomp[symmetric])
subgoal unfolding inj_on_def
by (intro ballI impI, subst (1 2) gterm_of_term_inv[symmetric]) fastforce+
by (simp_all add: gtt_lang_fmap_states_gtt * GM GS)
define GL1 where "GL1 = trim_gtt GL0"
have GL1: "ggtt_lang F GL1 = (r¯)⇧+ O r⇧+" using GL0 by (simp add: GL1_def trim_gtt_lang)
define GR1 where "GR1 = trim_gtt GR0"
have GR1: "ggtt_lang F GR1 = r⇧+ O (r¯)⇧+" using GR0 by (simp add: GR1_def trim_gtt_lang)
define GL where "GL = GTT_to_RR2 F GL1"
have "gtt_syms GL1 ⊆ F" using trim_gtt_prod_syms[of GL0]
unfolding GL0_def GL1_def gtt_syms_GTT_comp ta_syms_fmap_states_ta fst_map_prod snd_map_prod using ** by auto
then have GL: "RR2_spec GL ((r¯)⇧+ O r⇧+)"
using GTT_to_RR2[of GL1 F] by (simp add: GL_def GL1)
define GR where "GR = GTT_to_RR2 F GR1"
have "gtt_syms GR1 ⊆ F" using trim_gtt_prod_syms[of GR0]
unfolding GR0_def GR1_def gtt_syms_GTT_comp ta_syms_fmap_states_ta fst_map_prod snd_map_prod using ** by auto
then have GR: "RR2_spec GR (r⇧+ O (r¯)⇧+)"
using GTT_to_RR2[of GR1 F] by (simp add: GR_def GR1)
{ fix GL' GR' :: "(nat, _) ta" and res :: "(_, unit) term xoption"
assume GL': "RR2_spec GL' ((r¯)⇧+ O r⇧+)" and GR': "RR2_spec GR' (r⇧+ O (r¯)⇧+)"
and res: "case res of XNone ⇒ (ta_lang GL' :: (_, unit) term set) ⊆ ta_lang GR'
| XSome t ⇒ t ∈ (ta_lang GL' :: (_, unit) term set) - ta_lang GR'"
define fin where "fin = (case res of XNone ⇒ True | XSome x ⇒ False)"
have *: "(Restr ((rstep R)⇧=) {t. ground t ∧ funas_term t ⊆ F})⇧+ =
Restr ((Restr (rstep R) {t. ground t ∧ funas_term t ⊆ F})⇧*) {t. ground t ∧ funas_term t ⊆ F}"
unfolding trancl_reflcl[symmetric]
apply (subst Restr_trancl_Restr', (auto)[1])
by (rule arg_cong[of _ _ trancl]) blast
have "fin ⟷ (ta_lang GL' :: (_, unit) term set) ⊆ ta_lang GR'"
unfolding fin_def using res by (cases res) auto
note this[unfolded ta_lang_subset_conv GL'[unfolded RR2_spec_def] GR'[unfolded RR2_spec_def]]
then have "fin ⟷ (r¯)⇧+ O r⇧+ ⊆ r⇧+ O (r¯)⇧+"
apply (subst (asm) cancel_image[of "λt. (gfst t, gsnd t)", symmetric])
subgoal by (auto simp: inj_on_def gfst_gpair gsnd_gpair)
subgoal unfolding trs_to_ta_extra_simps(3) image_comp comp_def
unfolding prod.case_distrib[of gfst] prod.case_distrib[of gsnd] gfst_gpair gsnd_gpair
unfolding prod.collapse[unfolded fst_def snd_def] by simp
done
also have "... ⟷ CR (Restr (rstep R) {t. ground t ∧ funas_term t ⊆ F})"
unfolding r_def CR_iff_meet_subset_join meet_def join_def map_both_converse
apply (subst (1 2 3 4) map_trancl'[OF _ inj_on_gterm_of_term, symmetric], (auto)[2])
apply (subst (1 2) map_both_relcomp[OF inj_on_subset[OF inj_on_gterm_of_term]], (auto dest: tranclD tranclD2)[2])
apply (subst cancel_image[OF inj_on_subset[OF map_prod_inj_on[OF inj_on_gterm_of_term inj_on_gterm_of_term]]], (auto dest: tranclD tranclD2)[1])
unfolding trancl_converse rtrancl_converse *
unfolding Restr_converse[symmetric] rtrancl_converse[symmetric]
apply (subst (1 2) Restr_relcomp[symmetric], (auto simp flip: reflcl_trancl dest: tranclD tranclD2)[2])
apply (rule iffI)
apply (subst (1 2) Un_Diff_Int[of "_ O _" "{t. ground t ∧ funas_term t ⊆ F} × {t. ground t ∧ funas_term t ⊆ F}", symmetric])
apply (rule Un_mono)
by (auto simp flip: reflcl_trancl dest: tranclD tranclD2)
also note calculation
} note * = this
show ?thesis
unfolding lv_gcr_procedure_def Let_def Gr_def[symmetric] GM_def[symmetric] GS_def[symmetric]
unfolding GL0_def[symmetric] GR0_def[symmetric] GL1_def[symmetric] GR1_def[symmetric] GL_def[symmetric] GR_def[symmetric]
apply (refine_vcg ta_nat_sound2[of GL "(r¯)⇧+ O r⇧+"] ta_nat_sound2[of GR "r⇧+ O (r¯)⇧+"] ta_lang_containment)
subgoal premises p for GL' GR' res using GL[unfolded p] GR[unfolded p] p(5)
unfolding trim_ta_lang by (simp only: *)
done
qed
subsection ‹(Old) procedure for ground systems, for reference›
term trim_ta
term "x :: (_, _) ta_code"
term ta_code.trim
term ta_code.α
term trs_to_gtt_impl
term GTT_trancl_impl
term GTT_comp_impl
term GTT_to_RR2_impl
term ta_make_code
term ta_lang_containment_impl
thm trs_to_gtt_impl_def trs_to_ta_A_impl_sound trs_to_ta_B_impl_sound rstep_to_gtt_accept gtt_accept_to_rstep_rtrancl
thm GTT_trancl_impl_sound GTT_trancl_lang
thm GTT_comp_impl_sound gtt_comp_lang
thm GTT_to_RR2_impl.refine GTT_to_RR2
thm ta_make_autoref
thm ta_lang_containment_impl.refine ta_lang_containment
definition rtrancl_gtt where
"rtrancl_gtt R = GTT_trancl_impl (trs_to_gtt_impl R)"
"ta_Inl ≡ map_ta_list Inl id"">abbreviation "ta_Inl ≡ map_ta_list Inl id"
"ta_Inr ≡ map_ta_list Inr id"">abbreviation "ta_Inr ≡ map_ta_list Inr id"
definition left_gtt where
"left_gtt R = rtrancl_gtt R ⤜ (λ(A, B) ⇒ (GTT_comp_impl (ta_Inl B, ta_Inl A) (ta_Inr A, ta_Inr B)))"
definition right_gtt where
"right_gtt R = rtrancl_gtt R ⤜ (λ(A, B) ⇒ (GTT_comp_impl (ta_Inl A, ta_Inl B) (ta_Inr B, ta_Inr A)))"
definition ta_list_to_triple :: "('q :: compare_order, 'f :: compare_order) ta_list ⇒
('q, unit) RBT_Impl.rbt × (('q, 'f) ta_rule, unit) RBT_Impl.rbt × ('q × 'q) list" where
"ta_list_to_triple A = (RBT_Impl.rbt_bulkload (map (λk. (k, ())) (tal_final A)),
RBT_Impl.rbt_bulkload (map (λk. (k, ())) (tal_rules A)),
remdups_sort (tal_eps A))"
definition ta_triple_to_impl where
"ta_triple_to_impl = (λ(F,R,E). ta_make_code F R E)"
lemma remdups_sort_list_set_rel:
"R = Id ⟹ (remdups_sort xs, set xs) ∈ ⟨R⟩list_set_rel"
by (auto simp: list_set_rel_def br_def)
lemma rbt_bulkload_comp_rs_rel:
"R = Id ⟹ (rbt_bulkload (map (λk. (k :: _ :: compare_order, ())) x), set x) ∈ ⟨R⟩comp_rs_rel"
by (auto simp: map2set_rel_def rbt_map_rel_def rbt_map_rel'_def in_br_conv restrict_map_def comp_def
rbt_lookup_into_class lt_of_comp_post_simp ord_defs rbt_lookup_rbt_bulkload map_of_map_restrict
intro!: relcompI[of _ "λx. if x ∈ _ then Some () else None"] split: if_splits)
lemma ta_triple_to_impl_ta_list_to_triple_dflt_ta_rel:
"(ta_triple_to_impl (ta_list_to_triple x), ta_of x) ∈ dflt_ta_rel"
proof -
obtain fs rs es where x: "x = ta_list fs rs es" by (cases x) auto
show ?thesis using
ta_make_autoref[THEN fun_relD, THEN fun_relD, THEN fun_relD, OF
rbt_bulkload_comp_rs_rel[of _ fs] rbt_bulkload_comp_rs_rel[of _ rs] remdups_sort_list_set_rel[of _ es]]
by (auto simp: ta_list_to_triple_def ta_triple_to_impl_def ta_of_def x split: ta_list.split)
qed
"GTT_to_RR2_impl' ≡ ta_triple_to_impl ∘∘ GTT_to_RR2_impl"">abbreviation "GTT_to_RR2_impl' ≡ ta_triple_to_impl ∘∘ GTT_to_RR2_impl"
"ta_list_to_impl ≡ ta_triple_to_impl ∘ ta_list_to_triple"">abbreviation "ta_list_to_impl ≡ ta_triple_to_impl ∘ ta_list_to_triple"
"gtt_list_to_impl ≡ map_both ta_list_to_impl"">abbreviation "gtt_list_to_impl ≡ map_both ta_list_to_impl"
definition cr_procedure :: "(nat list, nat list) rule list ⇒ (_, unit) term option" where
"cr_procedure R = do {
A ← left_gtt R;
B ← right_gtt R;
let F = RBT_Impl.rbt_bulkload (map (λk. (k, ())) (concat (map funas_rule_list R)));
let A' = GTT_to_RR2_impl' F (gtt_list_to_impl A);
let B' = GTT_to_RR2_impl' F (gtt_list_to_impl B);
case_xoption None Some (ta_lang_containment_impl A' B')
}"
lemma finite_ta_states_ta_of:
"finite (ta_states (ta_of x))"
by (cases x) (auto simp: ta_of_def ta_states_def r_states_def)
lemma map_ta_rule_def':
"map_ta_rule f g = case_ta_rule (λh qs q. (g h) (map f qs) → (f q))"
by (auto split: ta_rule.splits)
lemma ta_of_map_ta_list:
"ta_of (map_ta_list f id x) = fmap_states_ta f (ta_of x)"
by (cases x) (auto simp: ta_of_def fmap_states_ta_def ta.make_def map_ta_rule_def')
lemma ta_triple_to_impl_ref:
"R1 = Id ⟹ R2 = Id ⟹ R3 = Id ⟹ (ta_triple_to_impl, λ(F, E, R). ta.make F E R) ∈
⟨R1⟩comp_rs_rel ×⇩r ⟨R2⟩comp_rs_rel ×⇩r ⟨R3⟩list_set_rel → dflt_ta_rel"
using ta_make_autoref by (auto simp: ta_triple_to_impl_def dest!: fun_relD)
lemma ta_make_collapse:
"ta.make (ta_final A) (ta_rules A) (ta_eps A) = A"
by simp
lemma ta_syms_trs_to_ta:
"ta_syms (trs_to_ta_A R) ⊆ funas_trs R" "ta_syms (trs_to_ta_B R) ⊆ funas_trs R"
by (auto simp: ta_syms_def trs_to_ta_A_def trs_to_ta_B_def cmn_ta_rules_def TRS_terms_def TRS_fst_def TRS_snd_def
funas_trs_def funas_rule_def dest!: subsetD[OF supteq_imp_funas_term_subset])
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 adapt_vars_inj_on_ground_terms:
"inj_on adapt_vars {t. ground t}"
by (auto simp: inj_on_def)
lemma ground_Fun:
"ground t ⟹ is_Fun t"
by (cases t) auto
lemma ground_trs_wf:
assumes "ground_trs R" shows "wf_trs R"
using assms by (auto simp: ground_trs_def wf_trs_def' ground_vars_term_empty ground_Fun)
lemma cr_procedure_correct:
assumes "ground_trs (set R)"
defines "F ≡ funas_trs (set R)"
obtains "cr_procedure R = None" "CR (Restr (rstep (set R)) {t. ground t ∧ funas_term t ⊆ F})" |
z where "cr_procedure R = Some z" "¬ CR (Restr (rstep (set R)) {t. ground t ∧ funas_term t ⊆ F})"
proof -
define res where "res = cr_procedure R"
let ?RR2 = "λAl Ar. ta_triple_to_impl (GTT_to_RR2_impl
(rbt_bulkload (map (λk. (k, ())) (concat (map funas_rule_list R))))
(ta_triple_to_impl (ta_list_to_triple Al), ta_triple_to_impl (ta_list_to_triple Ar)))"
obtain Rl Rr Pl Pr Vl Vr where
R: "GTT_trancl_impl (trs_to_gtt_impl R) = Some (Rl, Rr)" and
P: "GTT_comp_impl (ta_Inl Rr, ta_Inl Rl) (ta_Inr Rl, ta_Inr Rr) = Some (Pl, Pr)" and
V: "GTT_comp_impl (ta_Inl Rl, ta_Inl Rr) (ta_Inr Rr, ta_Inr Rl) = Some (Vl, Vr)" and
res: "res = (case ta_lang_containment_impl (?RR2 Pl Pr) (?RR2 Vl Vr) of
XNone ⇒ None | XSome x ⇒ Some x)"
using res_def by (auto simp: rtrancl_gtt_def cr_procedure_def left_gtt_def right_gtt_def
GTT_comp_impl_complete GTT_trancl_impl_complete Let_def split: bind_split_asm)
have GR: "gtt_lang (ta_of Rl, ta_of Rr) = Restr (map_both adapt_vars ` (rstep (set R))⇧*) {t. ground t}"
using GTT_trancl_impl_sound[OF R] GTT_trancl_lang[of "(trs_to_ta_A (set R), trs_to_ta_B (set R))"]
reachability_gtt_equiv[OF assms(1)]
by (simp add: trs_to_gtt_impl_def trs_to_ta_A_impl_sound trs_to_ta_B_impl_sound map_prod_def split_def)
have GP: "gtt_lang (ta_of Pl, ta_of Pr) = (map_both adapt_vars ` gtt_lang (ta_of Rl, ta_of Rr))¯ O map_both adapt_vars ` gtt_lang (ta_of Rl, ta_of Rr)"
unfolding GTT_comp_impl_sound[OF P, unfolded map_prod_def prod.simps]
apply (subst gtt_comp_lang, (auto simp: ta_of_map_ta_list)[1])
apply (subst (1) gtt_lang_swap[symmetric])
by (simp add: ta_of_map_ta_list map_prod_def gtt_lang_fmap_states_gtt[of _ "(_,_)", unfolded map_prod_def prod.simps])
have GV: "gtt_lang (ta_of Vl, ta_of Vr) = map_both adapt_vars ` gtt_lang (ta_of Rl, ta_of Rr) O (map_both adapt_vars ` gtt_lang (ta_of Rl, ta_of Rr))¯"
unfolding GTT_comp_impl_sound[OF V, unfolded map_prod_def prod.simps]
apply (subst gtt_comp_lang, (auto simp: ta_of_map_ta_list)[1])
apply (subst (2) gtt_lang_swap[symmetric])
by (simp add: ta_of_map_ta_list map_prod_def gtt_lang_fmap_states_gtt[of _ "(_,_)", unfolded map_prod_def prod.simps])
have F: "F = set (concat (map funas_rule_list R))"
by (auto simp: F_def funas_trs_def)
note GTT_to_RR2_impl.refine[THEN fun_relD, THEN fun_relD, OF rbt_bulkload_comp_rs_rel
prod_relI[OF ta_triple_to_impl_ta_list_to_triple_dflt_ta_rel ta_triple_to_impl_ta_list_to_triple_dflt_ta_rel],
of "concat (map funas_rule_list R)", folded F]
note fun_relD[OF ta_triple_to_impl_ref, OF _ _ _ this, unfolded comp_def prod.simps ta_make_collapse]
from this[of Pl Pr] this[of Vl Vr]
have *: "(?RR2 Pl Pr, GTT_to_RR2 F (ta_of Pl, ta_of Pr)) ∈ dflt_ta_rel"
"(?RR2 Vl Vr, GTT_to_RR2 F (ta_of Vl, ta_of Vr)) ∈ dflt_ta_rel" by simp_all
note conc_trans_additional(1)[OF ta_lang_containment_impl.refine[OF this] ta_lang_containment]
note inres_SPEC[OF _ this[unfolded Tree_Automata_Autoref_Setup.term_rel_id_simp xoption_rel_id_simp
conc_Id id_def], unfolded inres_simps, OF refl *[THEN dflt_TA_rel_finite]]
then have "case res of
None ⇒ ta_lang (GTT_to_RR2 F (ta_of Pl, ta_of Pr)) ⊆ (ta_lang (GTT_to_RR2 F (ta_of Vl, ta_of Vr)) :: (_, unit) term set)
| Some t ⇒ t ∈ ta_lang (GTT_to_RR2 F (ta_of Pl, ta_of Pr)) - ta_lang (GTT_to_RR2 F (ta_of Vl, ta_of Vr))"
unfolding res xoption.case_distrib option.simps .
then have res': "case res of
None ⇒ ta_lang (GTT_to_RR2 F (ta_of Pl, ta_of Pr)) ⊆ (ta_lang (GTT_to_RR2 F (ta_of Vl, ta_of Vr)) :: (_, unit) term set)
| Some _ ⇒ ¬ ta_lang (GTT_to_RR2 F (ta_of Pl, ta_of Pr)) ⊆ (ta_lang (GTT_to_RR2 F (ta_of Vl, ta_of Vr)) :: (_, unit) term set)"
by (auto split: option.splits)
have "ta_syms (ta_of Rl) ∪ ta_syms (ta_of Rr) ⊆ F"
using arg_cong[OF GTT_trancl_impl_sound[OF R], of gtt_syms, unfolded gtt_syms_GTT_trancl] ta_syms_trs_to_ta[of "set R"]
by (auto simp: F_def trs_to_gtt_impl_def map_prod_def trs_to_ta_A_impl_sound trs_to_ta_B_impl_sound)
then have F: "gtt_syms (ta_of Pl, ta_of Pr) ⊆ F" "gtt_syms (ta_of Vl, ta_of Vr) ⊆ F"
by (auto simp: GTT_comp_impl_sound[OF P, unfolded map_prod_def prod.simps]
GTT_comp_impl_sound[OF V, unfolded map_prod_def prod.simps] gtt_syms_GTT_comp
ta_of_map_ta_list ta_syms_fmap_states_ta)
have **: "Restr R {t. ground t ∧ funas_term t ⊆ F} = Restr (Restr R {t. ground t}) {t. funas_term t ⊆ F}" for R by auto
have ***: "Restr (map_both adapt_vars ` A) {t. ground t} = map_both adapt_vars ` (Restr A {t. ground t})" for A
by auto
have ****: "A ⊆ {t. ground t} × {t. ground t} ⟹ Restr (map_both adapt_vars ` A) {t. funas_term t ⊆ F}
= map_both adapt_vars ` Restr A {t. funas_term t ⊆ F}" for A by auto
have *****: "A ∩ X ⊆ B ∩ X ⟹ A ∩ (UNIV - X) ⊆ B ∩ (UNIV - X) ⟹ A ⊆ B" for A B X
by auto
have aconv: "ground_trs ((set R)¯)" using assms(1) by (auto simp: ground_trs_def)
have "ta_lang (GTT_to_RR2 F (ta_of Pl, ta_of Pr)) ⊆ (ta_lang (GTT_to_RR2 F (ta_of Vl, ta_of Vr)) :: (_, unit) term set)
⟷ CR (Restr (rstep (set R)) {t. ground t ∧ funas_term t ⊆ F})"
unfolding F[THEN GTT_to_RR2, unfolded GP GV GR RR2_spec_def] ta_lang_subset_conv
unfolding set_comprehension_aux ** map_both_converse
apply (subst cancel_image, (rule inj_on_subset[OF _ subset_UNIV], insert gpair_inject, auto simp: inj_on_def)[1])
apply (subst cancel_image, rule inj_on_subset[OF map_prod_inj_on[OF inj_on_gterm_of_term inj_on_gterm_of_term]], force)
apply (subst map_both_relcomp, (auto intro: inj_on_subset[OF adapt_vars_inj_on_ground_terms])[1])
unfolding *** map_both_converse
apply (subst map_both_relcomp, (auto intro: inj_on_subset[OF adapt_vars_inj_on_ground_terms])[1])+
apply (subst ****, (auto)[1])+
apply (subst cancel_image, (auto intro: inj_on_subset[OF map_prod_inj_on[OF adapt_vars_inj_on_ground_terms adapt_vars_inj_on_ground_terms]])[1])+
apply (subst (1 2) Restr_relcomp)
subgoal using rsteps_preserve_funas_terms[of _ F, OF _ _ _ ground_trs_wf[OF assms(1)]]
by (auto simp: F_def)
subgoal using rsteps_preserve_funas_terms[of _ F, OF _ _ _ ground_trs_wf[OF aconv]]
by (auto simp: F_def rtrancl_converse)
unfolding Restr_converse Int_assoc times_Int_times reflcl_trancl[symmetric] Int_Un_distrib2
apply (subst (1 2 3 4) Restr_trancl_Restr')
subgoal using subsetD[OF rstep_preserves_funas_terms[of _ F, OF _ _ _ ground_trs_wf[OF assms(1)]]]
ground_rstep_domain[OF aconv] by (auto simp: F_def)
apply (subst (1 2 3 4) Restr_trancl_Restr[symmetric])
unfolding Int_Un_distrib2[symmetric] reflcl_trancl Restr_converse[symmetric]
apply (subst (1 2) Restr_relcomp[symmetric])
subgoal using rsteps_preserve_funas_terms[of _ F, OF _ _ _ ground_trs_wf[OF assms(1)]]
rsteps_ground[of "set R", OF assms(1)[THEN ground_trs_wf, unfolded wf_trs_def, THEN spec, THEN spec, rule_format, THEN conjunct2]]
by (auto simp: F_def
dest!: subsetD[OF rtrancl_mono[of "Restr (rstep (set R)) ({t. ground t} ∩ {t. funas_term t ⊆ F})", OF Int_lower1, unfolded F_def]])
subgoal using rsteps_preserve_funas_terms[of _ F, OF _ _ _ ground_trs_wf[OF aconv]]
rsteps_ground[of "(set R)¯", OF aconv[THEN ground_trs_wf, unfolded wf_trs_def, THEN spec, THEN spec, rule_format, THEN conjunct2]]
by (auto simp: F_def rtrancl_converse
dest!: subsetD[OF rtrancl_mono[of "Restr (rstep (set R)) ({t. ground t} ∩ {t. funas_term t ⊆ F})", OF Int_lower1, unfolded F_def]])
unfolding CR_iff_meet_subset_join meet_def join_def rtrancl_converse
apply (intro iffI)
subgoal
apply (rule *****[of _ "(Collect ground ∩ {t. funas_term t ⊆ F}) × (Collect ground ∩ {t. funas_term t ⊆ F})"])
subgoal .
proof (standard, goal_cases)
case (1 x z)
then obtain y where y: "(y, x) ∈ (Restr (rstep (set R)) ({t. ground t} ∩ {t. funas_term t ⊆ F}))⇧*"
"(y, z) ∈ (Restr (rstep (set R)) ({t. ground t} ∩ {t. funas_term t ⊆ F}))⇧*" by auto
consider "x ∉ {t. ground t} ∩ {t. funas_term t ⊆ F}" | "z ∉ {t. ground t} ∩ {t. funas_term t ⊆ F}"
using 1 by auto
then show ?case
proof (cases)
case 1
then have "x = y" using y(1) unfolding rtrancl_trancl_reflcl by (auto simp: trancl_unfold_right)
then have "y = z" using 1 y(2) unfolding rtrancl_trancl_reflcl by (auto simp: trancl_unfold_left)
show ?thesis using 1 `x = y` `y =z` by blast
next
case 2
then have "z = y" using y(2) unfolding rtrancl_trancl_reflcl by (auto simp: trancl_unfold_right)
then have "y = x" using 2 y(1) unfolding rtrancl_trancl_reflcl by (auto simp: trancl_unfold_left)
show ?thesis using 1 `z = y` `y = x` by blast
qed
qed
subgoal by (intro Int_mono subset_refl) .
from res'[unfolded this res_def] show ?thesis by (auto split: option.splits intro: that)
qed
text ‹Wrap LV-TRS GCR procedure with check of preconditions.›
datatype answer = YES | NO | MAYBE
lemma lv_trs_code [code_unfold]:
"lv_trs R ⟷ (∀(l, r) ∈ R. linear_term (Fun undefined [l, r]))"
by (auto simp: lv_trs_def is_partition_def less_Suc_eq split: prod.splits)
definition lv_gcr_procedure_wrap :: "(nat list × nat) list ⇒ ((nat list, nat list) term × (nat list, nat list) term) list ⇒ answer" where
"lv_gcr_procedure_wrap F R =
(if lv_trs (set R) ∧ funas_trs (set R) ⊆ set F
then case lv_gcr_procedure_rbt (rbt_bulkload (map (λx. (x, ())) F)) (rbt_bulkload (map (λx. (x, ())) R)) of
dRETURN True ⇒ YES
| dRETURN False ⇒ NO
| _ ⇒ MAYBE
else MAYBE)"
lemma lv_gcr_procedure_wrap_sound:
shows "lv_gcr_procedure_wrap F R = YES ⟶ CR (Restr (rstep (set R)) {t. ground t ∧ funas_term t ⊆ set F})"
and "lv_gcr_procedure_wrap F R = NO ⟶ ¬ CR (Restr (rstep (set R)) {t. ground t ∧ funas_term t ⊆ set F})"
using 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 R F]
by (auto simp: lv_gcr_procedure_wrap_def split: if_splits dres.splits bool.splits)
text ‹Diagnostics›
"ta_size A = (card (ta_states A), card (ta_rules A), card (ta_eps A))"">definition "ta_size A = (card (ta_states A), card (ta_rules A), card (ta_eps A))"
schematic_goal ta_size_rbt:
"(?f, ta_size) ∈ dflt_ta_rel →⇩r nat_rel ×⇩r nat_rel ×⇩r nat_rel"
unfolding ta_size_def
by autoref
concrete_definition ta_size_rbt uses ta_size_rbt
definition tal_size where
"tal_size A = (length (uniq_list (concat (map (case_ta_rule (λ_ qs q. q # qs)) (tal_rules A)) @ concat (map (λ(l, r). [l, r]) (tal_eps A)))),
length (uniq_list (tal_rules A)), length (uniq_list (tal_eps A)))"
end