Theory 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]
  by (simp add: fset_inject)
  
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
  by (auto simp add: fQ_inf_e.rep_eq)


end