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