# Theory Regular_Tree_Relations.Regular_Relation_Impl

```theory Regular_Relation_Impl
imports Tree_Automata_Impl
Regular_Relation_Abstract_Impl
Horn_Fset
begin

section ‹Computing the epsilon transitions for the composition of GTT's›

definition Δ⇩ε_infer0_cont where
"Δ⇩ε_infer0_cont Δ⇩A Δ⇩B =
(let arules = filter (λ r. r_lhs_states r = []) (sorted_list_of_fset Δ⇩A) in
let brules = filter (λ r. r_lhs_states r = []) (sorted_list_of_fset Δ⇩B) in
(map (map_prod r_rhs r_rhs) (filter (λ(ra, rb). r_root ra = r_root rb) (List.product arules brules))))"

definition Δ⇩ε_infer1_cont where
"Δ⇩ε_infer1_cont Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε =
(let (arules, aeps) = (sorted_list_of_fset Δ⇩A, sorted_list_of_fset Δ⇩A⇩ε) in
let (brules, beps) = (sorted_list_of_fset Δ⇩B, sorted_list_of_fset Δ⇩B⇩ε) in
let prules = List.product arules brules in
(λ pq bs.
map (map_prod r_rhs r_rhs) (filter (λ(ra, rb). case (ra, rb) of (TA_rule f ps p, TA_rule g qs q) ⇒
f = g ∧ length ps = length qs ∧ (fst pq, snd pq) ∈ set (zip ps qs) ∧
set (zip ps qs) ⊆ insert (fst pq, snd pq) (fset bs)) prules) @
map (λ(p, p'). (p', snd pq)) (filter (λ(p, p') ⇒ p = fst pq) aeps) @
map (λ(q, q'). (fst pq, q')) (filter (λ(q, q') ⇒ q = snd pq) beps)))"

locale Δ⇩ε_fset =
fixes Δ⇩A :: "('q :: linorder, 'f :: linorder) ta_rule fset" and Δ⇩A⇩ε :: "('q × 'q) fset"
and Δ⇩B :: "('q, 'f) ta_rule fset" and Δ⇩B⇩ε :: "('q × 'q) fset"
begin

abbreviation A where "A ≡ TA Δ⇩A Δ⇩A⇩ε"
abbreviation B where "B ≡ TA Δ⇩B Δ⇩B⇩ε"

sublocale Δ⇩ε_horn A B .

sublocale l: horn_fset "Δ⇩ε_rules A B" "Δ⇩ε_infer0_cont Δ⇩A Δ⇩B" "Δ⇩ε_infer1_cont Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε"
apply (unfold_locales)
unfolding Δ⇩ε_horn.Δ⇩ε_infer0 Δ⇩ε_horn.Δ⇩ε_infer1 Δ⇩ε_infer0_cont_def Δ⇩ε_infer1_cont_def set_append Un_assoc[symmetric]
unfolding sorted_list_of_fset_simps union_fset
subgoal
apply (auto split!: prod.splits ta_rule.splits simp: comp_def fset_of_list_elem r_rhs_def
map_prod_def fSigma.rep_eq image_def Bex_def)
apply (metis ta_rule.exhaust_sel)
done
unfolding Let_def prod.case set_append Un_assoc
apply (intro arg_cong2[of _ _ _ _ "(∪)"])
subgoal
apply (auto split!: prod.splits ta_rule.splits)
apply (smt (verit, del_insts) Pair_inject map_prod_imageI mem_Collect_eq ta_rule.inject ta_rule.sel(3))
done
by (force simp add: image_def split!: prod.splits)+

lemmas infer = l.infer0 l.infer1
lemmas saturate_impl_sound = l.saturate_impl_sound
lemmas saturate_impl_complete = l.saturate_impl_complete

end

definition Δ⇩ε_impl where
"Δ⇩ε_impl Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε = horn_fset_impl.saturate_impl (Δ⇩ε_infer0_cont Δ⇩A Δ⇩B) (Δ⇩ε_infer1_cont Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε)"

lemma Δ⇩ε_impl_sound:
assumes "Δ⇩ε_impl Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε = Some xs"
shows "xs = Δ⇩ε (TA Δ⇩A Δ⇩A⇩ε) (TA Δ⇩B Δ⇩B⇩ε)"
using Δ⇩ε_fset.saturate_impl_sound[OF assms[unfolded Δ⇩ε_impl_def]]
unfolding Δ⇩ε_horn.Δ⇩ε_sound[symmetric]
by (auto simp flip: Δ⇩ε.rep_eq)

lemma Δ⇩ε_impl_complete:
fixes Δ⇩A :: "('q :: linorder, 'f :: linorder) ta_rule fset" and Δ⇩B :: "('q, 'f) ta_rule fset"
and Δ⇩ε⇩A :: "('q × 'q) fset" and Δ⇩ε⇩B :: "('q × 'q) fset"
shows "Δ⇩ε_impl Δ⇩A Δ⇩ε⇩A Δ⇩B Δ⇩ε⇩B ≠ None" unfolding Δ⇩ε_impl_def
by (intro Δ⇩ε_fset.saturate_impl_complete)
(auto simp flip: Δ⇩ε_horn.Δ⇩ε_sound)

lemma Δ⇩ε_impl [code]:
"Δ⇩ε (TA Δ⇩A Δ⇩A⇩ε) (TA Δ⇩B Δ⇩B⇩ε) = the (Δ⇩ε_impl Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε)"
using Δ⇩ε_impl_complete[of Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε] Δ⇩ε_impl_sound[of Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε]
by force

section ‹Computing the epsilon transitions for the transitive closure of GTT's›

definition Δ_trancl_infer0 where
"Δ_trancl_infer0 Δ⇩A Δ⇩B = Δ⇩ε_infer0_cont Δ⇩A Δ⇩B"

definition Δ_trancl_infer1 :: "('q :: linorder , 'f  :: linorder) ta_rule fset ⇒ ('q × 'q) fset ⇒  ('q, 'f) ta_rule fset ⇒ ('q × 'q) fset
⇒ 'q × 'q ⇒ ('q × 'q) fset ⇒ ('q × 'q) list" where
"Δ_trancl_infer1 Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε pq bs =
Δ⇩ε_infer1_cont Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε pq bs @
sorted_list_of_fset (
(λ(r, p'). (r, snd pq)) |`| (ffilter (λ(r, p') ⇒ p' = fst pq) bs) |∪|
(λ(q', r). (fst pq, r)) |`| (ffilter (λ(q', r) ⇒ q' = snd pq) (finsert pq bs)))"

locale Δ_trancl_list =
fixes Δ⇩A :: "('q :: linorder, 'f :: linorder) ta_rule fset" and Δ⇩A⇩ε :: "('q × 'q) fset"
and Δ⇩B :: "('q, 'f) ta_rule fset" and Δ⇩B⇩ε :: "('q × 'q) fset"
begin

abbreviation A where "A ≡ TA Δ⇩A Δ⇩A⇩ε"
abbreviation B where "B ≡ TA Δ⇩B Δ⇩B⇩ε"

sublocale Δ_trancl_horn A B .

sublocale l: horn_fset "Δ_trancl_rules A B"
"Δ_trancl_infer0 Δ⇩A Δ⇩B" "Δ_trancl_infer1 Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε"
apply (unfold_locales)
unfolding Δ_trancl_rules_def horn_infer0_union horn_infer1_union
Δ_trancl_infer0_def Δ_trancl_infer1_def Δ⇩ε_fset.infer set_append
by (auto simp flip: ex_simps(1) simp: horn.infer0_def horn.infer1_def intro!: arg_cong2[of _ _ _ _ "(∪)"])

lemmas saturate_impl_sound = l.saturate_impl_sound
lemmas saturate_impl_complete = l.saturate_impl_complete

end

definition "Δ_trancl_impl Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε =
horn_fset_impl.saturate_impl (Δ_trancl_infer0 Δ⇩A Δ⇩B) (Δ_trancl_infer1 Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε)"

lemma Δ_trancl_impl_sound:
assumes "Δ_trancl_impl Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε = Some xs"
shows "xs = Δ_trancl (TA Δ⇩A Δ⇩A⇩ε) (TA Δ⇩B Δ⇩B⇩ε)"
using Δ_trancl_list.saturate_impl_sound[OF assms[unfolded Δ_trancl_impl_def]]
unfolding Δ_trancl_horn.Δ_trancl_sound[symmetric] Δ_trancl.rep_eq[symmetric]
by auto

lemma Δ_trancl_impl_complete:
fixes Δ⇩A :: "('q :: linorder, 'f :: linorder) ta_rule fset" and Δ⇩B :: "('q, 'f) ta_rule fset"
and Δ⇩A⇩ε :: "('q × 'q) fset" and Δ⇩B⇩ε :: "('q × 'q) fset"
shows "Δ_trancl_impl Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε ≠ None"
unfolding Δ_trancl_impl_def
by (intro Δ_trancl_list.saturate_impl_complete)
(auto simp flip: Δ_trancl_horn.Δ_trancl_sound)

lemma Δ_trancl_impl [code]:
"Δ_trancl (TA Δ⇩A Δ⇩A⇩ε) (TA Δ⇩B Δ⇩B⇩ε) = (the (Δ_trancl_impl Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε))"
using Δ_trancl_impl_complete[of Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε]
using Δ_trancl_impl_sound[of Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε]
by force

section ‹Computing the epsilon transitions for the transitive closure of pair automata›

definition Δ_Atr_infer1_cont :: "('q :: linorder × 'q) fset ⇒ ('q, 'f :: linorder) ta_rule fset ⇒ ('q × 'q) fset ⇒
('q, 'f) ta_rule fset ⇒ ('q × 'q) fset ⇒ 'q × 'q ⇒ ('q × 'q) fset ⇒ ('q × 'q) list" where
"Δ_Atr_infer1_cont Q Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε =
(let G = sorted_list_of_fset (the (Δ⇩ε_impl Δ⇩B Δ⇩B⇩ε Δ⇩A Δ⇩A⇩ε)) in
(λ pq bs.
(let bs_list = sorted_list_of_fset bs in
map (λ (p, q). (fst p, snd pq))  (filter (λ (p, q). snd p = fst q ∧ snd q = fst pq) (List.product bs_list G)) @
map (λ (p, q). (fst pq, snd q))  (filter (λ (p, q). snd p = fst q ∧ fst p = snd pq) (List.product G bs_list)) @
map (λ (p, q). (fst pq, snd pq)) (filter (λ (p, q). snd pq = p ∧ fst pq = q) G))))"

locale Δ_Atr_fset =
fixes Q :: "('q :: linorder × 'q) fset" and  Δ⇩A :: "('q, 'f :: linorder) ta_rule fset" and Δ⇩A⇩ε :: "('q × 'q) fset"
and Δ⇩B :: "('q, 'f) ta_rule fset" and Δ⇩B⇩ε :: "('q × 'q) fset"
begin

abbreviation A where "A ≡ TA Δ⇩A Δ⇩A⇩ε"
abbreviation B where "B ≡ TA Δ⇩B Δ⇩B⇩ε"

sublocale Δ_Atr_horn Q A B .

lemma infer1:
"infer1 pq (fset bs) = set (Δ_Atr_infer1_cont Q Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε pq bs)"
proof -
have "{(p, snd pq) | p q. (p, q) ∈ (fset bs) ∧ (q, fst pq) |∈| Δ⇩ε B A} ∪
{(fst pq, v) | q r v. (snd pq, r) |∈| Δ⇩ε B A ∧ (r, v) ∈ (fset bs)} ∪
{(fst pq, snd pq) | q . (snd pq, fst pq) |∈| Δ⇩ε B A} = set (Δ_Atr_infer1_cont Q Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε pq bs)"
unfolding Δ_Atr_infer1_cont_def set_append Un_assoc[symmetric] Let_def
unfolding sorted_list_of_fset_simps union_fset
apply (intro arg_cong2[of _ _ _ _ "(∪)"])
apply (simp_all add: fSigma_repeq flip: Δ⇩ε_impl fset_of_list_elem)
apply force+
done
then show ?thesis
using Δ_Atr_horn.Δ_Atr_infer1[of Q A B pq "fset bs"]
by simp
qed

sublocale l: horn_fset "Δ_Atr_rules Q A B" "sorted_list_of_fset Q" "Δ_Atr_infer1_cont Q Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε"
apply (unfold_locales)
unfolding Δ_Atr_horn.Δ_Atr_infer0 fset_of_list.rep_eq
using infer1
by auto

lemmas infer = l.infer0 l.infer1
lemmas saturate_impl_sound = l.saturate_impl_sound
lemmas saturate_impl_complete = l.saturate_impl_complete

end

definition "Δ_Atr_impl Q Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε =
horn_fset_impl.saturate_impl (sorted_list_of_fset Q) (Δ_Atr_infer1_cont Q Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε)"

lemma Δ_Atr_impl_sound:
assumes "Δ_Atr_impl Q Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε = Some xs"
shows "xs = Δ_Atrans Q (TA Δ⇩A Δ⇩A⇩ε) (TA Δ⇩B Δ⇩B⇩ε)"
using Δ_Atr_fset.saturate_impl_sound[OF assms[unfolded Δ_Atr_impl_def]]
unfolding Δ_Atr_horn.Δ_Atr_sound[symmetric] Δ_Atrans.rep_eq[symmetric]

lemma Δ_Atr_impl_complete:
shows "Δ_Atr_impl Q Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε ≠ None" unfolding Δ_Atr_impl_def
by (intro Δ_Atr_fset.saturate_impl_complete)
(auto simp: finite_Δ_Atrans_set simp flip: Δ_Atr_horn.Δ_Atr_sound)

lemma Δ_Atr_impl [code]:
"Δ_Atrans Q (TA Δ⇩A Δ⇩A⇩ε) (TA Δ⇩B Δ⇩B⇩ε) = (the (Δ_Atr_impl Q Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε))"
using Δ_Atr_impl_complete[of Q Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε] Δ_Atr_impl_sound[of Q Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε]
by force

section ‹Computing the Q infinity set for the infinity predicate automaton›

definition Q_infer0_cont  :: "('q :: linorder, 'f :: linorder option × 'g :: linorder option) ta_rule fset ⇒ ('q × 'q) list" where
"Q_infer0_cont Δ = concat (sorted_list_of_fset (
(λ r. case r of TA_rule f ps p ⇒ map (λ x. Pair x p) ps) |`|
(ffilter (λ r. case r of TA_rule f ps p ⇒ fst f = None ∧ snd f ≠ None ∧ ps ≠ []) Δ)))"

definition Q_infer1_cont :: "('q ::linorder × 'q) fset ⇒ 'q × 'q ⇒ ('q × 'q) fset ⇒ ('q × 'q) list" where
"Q_infer1_cont Δε =
(let eps = sorted_list_of_fset Δε in
(λ pq bs.
let bs_list = sorted_list_of_fset bs in
map (λ (q, r). (fst pq, r)) (filter (λ (q, r) ⇒ q = snd pq) eps) @
map (λ(r, p'). (r, snd pq)) (filter (λ(r, p') ⇒ p' = fst pq) bs_list) @
map (λ(q', r). (fst pq, r)) (filter (λ(q', r) ⇒ q' = snd pq) (pq # bs_list))))"

locale Q_fset =
fixes Δ :: "('q :: linorder, 'f :: linorder option × 'g :: linorder option) ta_rule fset" and Δε :: "('q × 'q) fset"
begin

abbreviation A where "A ≡ TA Δ Δε"
sublocale Q_horn A .

sublocale l: horn_fset "Q_inf_rules A" "Q_infer0_cont Δ" "Q_infer1_cont Δε"
apply (unfold_locales)
unfolding Q_horn.Q_infer0 Q_horn.Q_infer1 Q_infer0_cont_def Q_infer1_cont_def set_append Un_assoc[symmetric]
unfolding sorted_list_of_fset_simps union_fset
subgoal
apply (auto simp add: Bex_def split!: ta_rule.splits)
apply (rule_tac x = "TA_rule (lift_None_Some f) ps p" in exI)
apply (force dest: in_set_idx)+
done
unfolding Let_def set_append Un_assoc
by (intro arg_cong2[of _ _ _ _ "(∪)"]) auto

lemmas saturate_impl_sound = l.saturate_impl_sound
lemmas saturate_impl_complete = l.saturate_impl_complete

end

definition Q_impl where
"Q_impl Δ Δε = horn_fset_impl.saturate_impl (Q_infer0_cont Δ) (Q_infer1_cont Δε)"

lemma Q_impl_sound:
"Q_impl Δ Δε = Some xs ⟹ fset xs = Q_inf (TA Δ Δε)"
using Q_fset.saturate_impl_sound unfolding Q_impl_def Q_horn.Q_sound .

lemma Q_impl_complete:
"Q_impl Δ Δε ≠ None"
proof -
let ?A = "TA Δ Δε"
have *: "Q_inf ?A ⊆ fset (𝒬 ?A |×| 𝒬 ?A)"
by (auto simp add: Q_inf_states_ta_states(1, 2) subrelI)
have "finite (Q_inf ?A)"
by (intro finite_subset[OF *]) simp
then show ?thesis unfolding Q_impl_def
by (intro Q_fset.saturate_impl_complete) (auto simp: Q_horn.Q_sound)
qed

definition "Q_infinity_impl Δ Δε = (let Q = the (Q_impl Δ Δε) in
snd |`| ((ffilter (λ (p, q). p = q) Q) |O| Q))"

lemma Q_infinity_impl_fmember:
"q |∈| Q_infinity_impl Δ Δε ⟷ (∃ p. (p, p) |∈| the (Q_impl Δ Δε) ∧
(p, q) |∈| the (Q_impl Δ Δε))"
unfolding Q_infinity_impl_def
by (auto simp: Let_def image_iff Bex_def) fastforce

lemma loop_sound_correct [simp]:
"fset (Q_infinity_impl Δ Δε) = Q_inf_e (TA Δ Δε)"
proof -
obtain Q where [simp]: "Q_impl Δ Δε = Some Q" using Q_impl_complete[of Δ Δε]
by blast
have "fset Q = (Q_inf (TA Δ Δε))"
using Q_impl_sound[of Δ Δε]
by (auto simp: fset_of_list.rep_eq)
then show ?thesis
by (force simp: Q_infinity_impl_fmember Let_def fset_of_list_elem
fset_of_list.rep_eq)
qed

lemma fQ_inf_e_code [code]:
"fQ_inf_e (TA Δ Δε) = Q_infinity_impl Δ Δε"
using loop_sound_correct