Theory Regular_Relation_Impl

theory Regular_Relation_Impl
  imports Pair_Automaton GTT_Transitive_Closure RR2_Infinite_Impl AR.Horn_Autoref
begin


abbreviation TA_of_lists where
  "TA_of_lists Δ Δ⇩E ≡ TA (fset_of_list Δ) (fset_of_list Δ⇩E)"

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

definition Δ⇩ε_rules :: "('q, 'f) ta ⇒ ('q, 'f) ta ⇒ ('q × 'q) horn set" where
  "Δ⇩ε_rules A B =
    {zip ps qs →⇩h (p, q) |f ps p qs q. f ps → p |∈| rules A ∧ f qs → q |∈| rules B ∧ length ps = length qs} ∪
    {[(p, q)] →⇩h (p', q) |p p' q. (p, p') |∈| eps A} ∪
    {[(p, q)] →⇩h (p, q') |p q q'. (q, q') |∈| eps B}"

locale Δ⇩ε_horn =
  fixes A :: "('q, 'f) ta" and B :: "('q, 'f) ta"
begin

sublocale horn "Δ⇩ε_rules A B" .

lemma Δ⇩ε_infer0:
  "infer0 = {(p, q) |f p q. f [] → p |∈| rules A ∧ f [] → q |∈| rules B}"
  unfolding horn.infer0_def Δ⇩ε_rules_def
  using zip_Nil[of "[]"] zip_inj[of "[]" "[]"] by auto force+

lemma Δ⇩ε_infer1:
  "infer1 pq X = {(p, q) |f ps p qs q. f ps → p |∈| rules A ∧ f qs → q |∈| rules B ∧ length ps = length qs ∧
    (fst pq, snd pq) ∈ set (zip ps qs) ∧ set (zip ps qs) ⊆ insert pq X} ∪
    {(p', snd pq) |p p'. (p, p') |∈| eps A ∧ p = fst pq} ∪
    {(fst pq, q') |q q'. (q, q') |∈| eps B ∧ q = snd pq}"
  unfolding Δ⇩ε_rules_def horn_infer1_union
  apply (intro arg_cong2[of _ _ _ _ "(∪)"])
    by (auto simp: horn.infer1_def simp flip: ex_simps(1)) force+

lemma Δ⇩ε_sound:
  "Δ⇩ε_set A B = saturate"
proof (intro set_eqI iffI, goal_cases lr rl)
  case (lr x) obtain p q where x: "x = (p, q)" by (cases x)
  show ?case using lr unfolding x
  proof (induct)
    case (Δ⇩ε_set_cong f ps p qs q) show ?case
      apply (intro infer[of "zip ps qs" "(p, q)"])
      subgoal using Δ⇩ε_set_cong(1-3) by (auto simp: Δ⇩ε_rules_def)
      subgoal using Δ⇩ε_set_cong(3,5) by (auto simp: zip_nth_conv)
      done
  next
    case (Δ⇩ε_set_eps1 p p' q) then show ?case
      by (intro infer[of "[(p, q)]" "(p', q)"]) (auto simp: Δ⇩ε_rules_def)
  next
    case (Δ⇩ε_set_eps2 q q' p) then show ?case
      by (intro infer[of "[(p, q)]" "(p, q')"]) (auto simp: Δ⇩ε_rules_def)
  qed
next
  case (rl x) obtain p q where x: "x = (p, q)" by (cases x)
  show ?case using rl unfolding x
  proof (induct)
    case (infer as a) then show ?case
      using Δ⇩ε_set_cong[of _ "map fst as" "fst a" A "map snd as" "snd a" B]
        Δ⇩ε_set_eps1[of _ "fst a" A "snd a" B] Δ⇩ε_set_eps2[of _ "snd a" B "fst a" A]
      by (auto simp: Δ⇩ε_rules_def)
  qed
qed

end

definition Δ⇩ε_infer0_list where
  "Δ⇩ε_infer0_list Δ⇩A Δ⇩B = map (map_prod r_rhs r_rhs) (
     filter (λ(ra, rb). case (ra, rb) of (f ps → p, g qs → q) ⇒ f = g ∧ ps = [] ∧ qs = []) (List.product Δ⇩A Δ⇩B))"

definition Δ⇩ε_infer1_list where
  "Δ⇩ε_infer1_list Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε 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) ⊆ set ((fst pq, snd pq) # bs)) (List.product Δ⇩A Δ⇩B)) @
    map (λ(p, p'). (p', snd pq)) (filter (λ(p, p') ⇒ p = fst pq) Δ⇩A⇩ε) @
    map (λ(q, q'). (fst pq, q')) (filter (λ(q, q') ⇒ q = snd pq) Δ⇩B⇩ε)"

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

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

sublocale Δ⇩ε_horn A B .

sublocale l: horn_list "Δ⇩ε_rules A B" "Δ⇩ε_infer0_list Δ⇩A Δ⇩B" "Δ⇩ε_infer1_list Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε"
  apply (unfold_locales)
  unfolding Δ⇩ε_horn.Δ⇩ε_infer0 Δ⇩ε_horn.Δ⇩ε_infer1 Δ⇩ε_infer0_list_def Δ⇩ε_infer1_list_def set_append Un_assoc[symmetric]
  subgoal apply (auto split!: prod.splits ta_rule.splits simp: fset_of_list_elem)
    apply (force simp: r_rhs_def map_prod_def)
    done
  apply (intro arg_cong2[of _ _ _ _ "(∪)"])
  by (auto  simp: fset_of_list_elem r_rhs_def map_prod_def) (force split: ta_rule.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_list_impl.saturate_impl (Δ⇩ε_infer0_list Δ⇩A Δ⇩B) (Δ⇩ε_infer1_list Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε)"

lemma Δ⇩ε_impl_sound:
  assumes "Δ⇩ε_impl Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε = Some xs"
  shows "fset_of_list xs = Δ⇩ε (TA_of_lists Δ⇩A Δ⇩A⇩ε) (TA_of_lists Δ⇩B Δ⇩B⇩ε)"
proof -
  have "Δ⇩ε_impl Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε = Some xs ⟹ set xs = Δ⇩ε_set (TA_of_lists Δ⇩A Δ⇩A⇩ε) (TA_of_lists Δ⇩B Δ⇩B⇩ε)"
    using Δ⇩ε_list.saturate_impl_sound unfolding Δ⇩ε_impl_def Δ⇩ε_horn.Δ⇩ε_sound .
  from this[OF assms] show ?thesis
    by (simp add: Δ⇩ε.abs_eq fset_of_list.abs_eq)
qed

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

lemma Δ⇩ε_impl [code]:
  "Δ⇩ε (TA_of_lists Δ⇩A Δ⇩A⇩ε) (TA_of_lists Δ⇩B Δ⇩B⇩ε) =
    fset_of_list (the (Δ⇩ε_impl Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε))"
  by (auto simp add: Δ⇩ε_impl_complete Δ⇩ε_impl_sound)

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

definition Δ_trancl_rules :: "('q, 'f) ta ⇒ ('q, 'f) ta ⇒ ('q × 'q) horn set" where
  "Δ_trancl_rules A B =
    Δ⇩ε_rules A B ∪ {[(p, q), (q, r)] →⇩h (p, r) |p q r. True}"

locale Δ_trancl_horn =
  fixes A :: "('q, 'f) ta" and B :: "('q, 'f) ta"
begin

sublocale horn "Δ_trancl_rules A B" .

lemma Δ_trancl_infer0:
  "infer0 = horn.infer0 (Δ⇩ε_rules A B)"
  by (auto simp: Δ⇩ε_rules_def Δ_trancl_rules_def horn.infer0_def)

lemma Δ_trancl_infer1:
  "infer1 pq X = horn.infer1 (Δ⇩ε_rules A B) pq X ∪
   {(r, snd pq) |r p'. (r, p') ∈ X ∧ p' = fst pq} ∪
   {(fst pq, r) |q' r. (q', r) ∈ (insert pq X) ∧ q' = snd pq}"
  unfolding Δ_trancl_rules_def horn_infer1_union Un_assoc
  apply (intro arg_cong2[of _ _ _ _ "(∪)"] HOL.refl)
  by (auto simp: horn.infer1_def simp flip: ex_simps(1)) force+

lemma Δ_trancl_sound:
  "Δ_trancl_set A B = saturate"
proof (intro set_eqI iffI, goal_cases lr rl)
  case (lr x) obtain p q where x: "x = (p, q)" by (cases x)
  show ?case using lr unfolding x
  proof (induct)
    case (Δ_set_cong f ps p qs q) show ?case
      apply (intro infer[of "zip ps qs" "(p, q)"])
      subgoal using Δ_set_cong(1-3) by (auto simp: Δ_trancl_rules_def Δ⇩ε_rules_def)
      subgoal using Δ_set_cong(3,5) by (auto simp: zip_nth_conv)
      done
  next
    case (Δ_set_eps1 p p' q) then show ?case
      by (intro infer[of "[(p, q)]" "(p', q)"]) (auto simp: Δ_trancl_rules_def Δ⇩ε_rules_def)
  next
    case (Δ_set_eps2 q q' p) then show ?case
      by (intro infer[of "[(p, q)]" "(p, q')"]) (auto simp: Δ_trancl_rules_def Δ⇩ε_rules_def)
  next
    case (Δ_set_trans p q r) then show ?case
      by (intro infer[of "[(p,q), (q,r)]" "(p, r)"]) (auto simp: Δ_trancl_rules_def Δ⇩ε_rules_def)
  qed
next
  case (rl x) obtain p q where x: "x = (p, q)" by (cases x)
  show ?case using rl unfolding x
  proof (induct)
    case (infer as a) then show ?case
      using Δ_set_cong[of _ "map fst as" "fst a" A "map snd as" "snd a" B]
        Δ_set_eps1[of _ "fst a" A "snd a" B] Δ_set_eps2[of _ "snd a" B "fst a" A]
        Δ_set_trans[of "fst a" "snd (hd as)" A B "snd a"]
      by (auto simp: Δ_trancl_rules_def Δ⇩ε_rules_def)
  qed
qed

end

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

definition Δ_trancl_infer1 :: "('q, 'f) ta_rule list ⇒ ('q × 'q) list ⇒  ('q, 'f) ta_rule list ⇒ ('q × 'q) list
  ⇒ 'q × 'q ⇒ ('q × 'q) list ⇒ ('q × 'q) list" where
  "Δ_trancl_infer1 Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε pq bs =
    Δ⇩ε_infer1_list Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε pq bs @
    map (λ(r, p'). (r, snd pq)) (filter (λ(r, p') ⇒ p' = fst pq) bs) @
    map (λ(q', r). (fst pq, r)) (filter (λ(q', r) ⇒ q' = snd pq) (pq # bs))"

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

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

sublocale Δ_trancl_horn A B .

sublocale l: horn_list "Δ_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 Δ⇩ε_list.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

"Δ_trancl_impl Δ_A Δ_A_ε Δ_B Δ_B_ε =">definition "Δ_trancl_impl Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε =
   horn_list_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 "fset_of_list xs = Δ_trancl (TA_of_lists Δ⇩A Δ⇩A⇩ε) (TA_of_lists Δ⇩B Δ⇩B⇩ε)"
proof -
  have "Δ_trancl_impl Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε = Some xs ⟹ set xs = Δ_trancl_set (TA_of_lists Δ⇩A Δ⇩A⇩ε) (TA_of_lists Δ⇩B Δ⇩B⇩ε)"
    using Δ_trancl_list.saturate_impl_sound unfolding Δ_trancl_impl_def Δ_trancl_horn.Δ_trancl_sound .
  from this[OF assms] show ?thesis
    by (simp add: Δ_trancl.abs_eq fset_of_list.abs_eq)
qed

lemma Δ_trancl_impl_complete:
  fixes Δ⇩A :: "('q, 'f) ta_rule list" and Δ⇩B :: "('q, 'f) ta_rule list"
    and Δ⇩A⇩ε :: "('q × 'q) list" and Δ⇩B⇩ε :: "('q × 'q) list"
  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_of_lists Δ⇩A Δ⇩A⇩ε) (TA_of_lists Δ⇩B Δ⇩B⇩ε) =
    fset_of_list (the (Δ_trancl_impl Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε))"
  by (auto simp add: Δ_trancl_impl_complete Δ_trancl_impl_sound)


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

definition Δ_Atr_rules :: "('q × 'q) fset ⇒ ('q, 'f) ta ⇒ ('q, 'f) ta ⇒ ('q × 'q) horn set" where
  "Δ_Atr_rules Q A B =
    {[] →⇩h (p, q) | p q. (p , q) |∈| Q} ∪
    {[(p, q),(r, v)] →⇩h (p, v) |p q r v. (q, r) |∈| Δ⇩ε B A}"

locale Δ_Atr_horn =
  fixes Q :: "('q × 'q) fset" and A :: "('q, 'f) ta" and B :: "('q, 'f) ta"
begin

sublocale horn "Δ_Atr_rules Q A B" .

lemma Δ_Atr_infer0: "infer0 = fset Q"
  by (auto simp: horn.infer0_def Δ_Atr_rules_def fmember.rep_eq)
  
lemma Δ_Atr_infer1:
  "infer1 pq X = {(p, snd pq) | p q. (p, q) ∈ X ∧ (q, fst pq) |∈| Δ⇩ε B A} ∪
   {(fst pq, v) | q r v. (snd pq, r) |∈| Δ⇩ε B A ∧ (r, v) ∈ X} ∪
   {(fst pq, snd pq) | q . (snd pq, fst pq) |∈| Δ⇩ε B A}"
  unfolding Δ_Atr_rules_def horn_infer1_union
  by (auto simp: horn.infer1_def simp flip: ex_simps(1)) force+

lemma Δ_Atr_sound:
  "Δ_Atrans_set Q A B = saturate"
proof (intro set_eqI iffI, goal_cases lr rl)
  case (lr x) obtain p q where x: "x = (p, q)" by (cases x)
  show ?case using lr unfolding x
  proof (induct)
    case (base p q)
    then show ?case
      by (intro infer[of "[]" "(p, q)"]) (auto simp: Δ_Atr_rules_def)
  next
    case (step p q r v)
    then show ?case
      by (intro infer[of "[(p, q), (r, v)]" "(p, v)"]) (auto simp: Δ_Atr_rules_def)
  qed
next
  case (rl x) obtain p q where x: "x = (p, q)" by (cases x)
  show ?case using rl unfolding x
  proof (induct)
    case (infer as a) then show ?case
      using base[of "fst a" "snd a" Q A B]
      using Δ_Atrans_set.step[of "fst a" _ Q A B "snd a"]
      by (auto simp: Δ_Atr_rules_def) blast
  qed
qed

end

definition Δ_Atr_infer0_list where
  "Δ_Atr_infer0_list Q = Q"

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

(*  (λ (p, q). snd p = fst q ∧ snd q = fst pq)*)

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

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

sublocale Δ_Atr_horn "fset_of_list Q" A B .

lemma infer1:
  "infer1 pq (set bs) = set (Δ_Atr_infer1_list Q Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε pq bs)"
proof -
  have "{(p, snd pq) | p q. (p, q) ∈ (set bs) ∧ (q, fst pq) |∈| Δ⇩ε B A} ∪
   {(fst pq, v) | q r v. (snd pq, r) |∈| Δ⇩ε B A ∧ (r, v) ∈ (set bs)} ∪
   {(fst pq, snd pq) | q . (snd pq, fst pq) |∈| Δ⇩ε B A} = set (Δ_Atr_infer1_list Q Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε pq bs)"
  unfolding Δ_Atr_infer1_list_def set_append Un_assoc[symmetric] Let_def
  by (intro arg_cong2[of _ _ _ _ "(∪)"])
     (auto simp: image_Collect simp flip: Δ⇩ε_impl fset_of_list_elem)
  then show ?thesis
    using Δ_Atr_horn.Δ_Atr_infer1[of "fset_of_list Q" A B pq "set bs"]
    by simp
qed

sublocale l: horn_list "Δ_Atr_rules (fset_of_list Q) A B" "Δ_Atr_infer0_list Q" "Δ_Atr_infer1_list Q Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε"
  apply (unfold_locales)
  unfolding Δ_Atr_horn.Δ_Atr_infer0 Δ_Atr_infer0_list_def 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

"Δ_Atr_impl Q Δ_A Δ_A_ε Δ_B Δ_B_ε =">definition "Δ_Atr_impl Q Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε =
   horn_list_impl.saturate_impl (Δ_Atr_infer0_list Q) (Δ_Atr_infer1_list Q Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε)"

lemma Δ_Atr_impl_sound:
  assumes "Δ_Atr_impl Q Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε = Some xs"
  shows "fset_of_list xs = Δ_Atrans (fset_of_list Q) (TA_of_lists Δ⇩A Δ⇩A⇩ε) (TA_of_lists Δ⇩B Δ⇩B⇩ε)"
proof -
  have "Δ_Atr_impl Q Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε = Some xs ⟹ set xs = Δ_Atrans_set (fset_of_list Q) (TA_of_lists Δ⇩A Δ⇩A⇩ε) (TA_of_lists Δ⇩B Δ⇩B⇩ε)"
    using Δ_Atr_list.saturate_impl_sound unfolding Δ_Atr_impl_def Δ_Atr_horn.Δ_Atr_sound .
  from this[OF assms] show ?thesis
    by (simp add: Δ_Atrans.abs_eq fset_of_list.abs_eq)
qed

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

lemma Δ_Atr_impl [code]:
  "Δ_Atrans (fset_of_list Q) (TA_of_lists Δ⇩A Δ⇩A⇩ε) (TA_of_lists Δ⇩B Δ⇩B⇩ε) = fset_of_list (the (Δ_Atr_impl Q Δ⇩A Δ⇩A⇩ε Δ⇩B Δ⇩B⇩ε))"
  by (auto simp add: Δ_Atr_impl_complete Δ_Atr_impl_sound)


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

definition Q_inf_rules :: "('q, 'f option × 'g option) ta ⇒ ('q × 'q) horn set" where
  "Q_inf_rules A =
    {[] →⇩h (ps ! i, p) |f ps p i. (None, Some f) ps → p |∈| rules A ∧ i < length ps} ∪
    {[(p, q)] →⇩h (p, r) |p q r. (q, r) |∈| eps A} ∪
    {[(p, q), (q, r)] →⇩h (p, r) |p q r. True}"

locale Q_horn =
  fixes A :: "('q, 'f option × 'g option) ta"
begin

sublocale horn "Q_inf_rules A" .

lemma Q_infer0:
  "infer0 = {(ps ! i, p) |f ps p i. (None, Some f) ps → p |∈| rules A ∧ i < length ps}"
  unfolding horn.infer0_def Q_inf_rules_def by auto

lemma Q_infer1:
  "infer1 pq X = {(fst pq, r) | q r. (q, r) |∈| eps A ∧ q = snd pq} ∪
    {(r, snd pq) |r p'. (r, p') ∈ X ∧ p' = fst pq} ∪
    {(fst pq, r) |q' r. (q', r) ∈ (insert pq X) ∧ q' = snd pq}"
  unfolding Q_inf_rules_def horn_infer1_union
  by (auto simp: horn.infer1_def simp flip: ex_simps(1)) force+

lemma Q_sound:
  "Q_inf A = saturate"
proof (intro set_eqI iffI, goal_cases lr rl)
  case (lr x) obtain p q where x: "x = (p, q)" by (cases x)
  show ?case using lr unfolding x
  proof (induct)
    case (trans p q r)
    then show ?case
      by (intro infer[of "[(p,q), (q,r)]" "(p, r)"])
        (auto simp: Q_inf_rules_def)
  next
    case (rule f qs q i)
    then show ?case
      by (intro infer[of "[]" "(qs ! i, q)"])
        (auto simp: Q_inf_rules_def)
  next
    case (eps p q r)
    then show ?case
      by (intro infer[of "[(p, q)]" "(p, r)"])
        (auto simp: Q_inf_rules_def)
  qed
next
  case (rl x) obtain p q where x: "x = (p, q)" by (cases x)
  show ?case using rl unfolding x
  proof (induct)
    case (infer as a) then show ?case
      using Q_inf.eps[of "fst a" _ A "snd a"]
      using Q_inf.trans[of "fst a" "snd (hd as)" A "snd a"]
      by (auto simp: Q_inf_rules_def intro: Q_inf.rule) blast
  qed
qed

end

definition Q_infer0_list where
  "Q_infer0_list Δ = concat (map (λ r. case r of f ps → p ⇒ map (λ x. Pair x p) ps)
     (filter (λ r. case r of f ps → p ⇒ fst f = None ∧ snd f ≠ None ∧ ps ≠ []) Δ))"

definition Q_infer1_list :: "('q × 'q) list ⇒ 'q × 'q ⇒ ('q × 'q) list ⇒ ('q × 'q) list" where
  "Q_infer1_list Δε pq bs =
    map (λ(q, r). (fst pq, r)) (filter (λ (q, r) ⇒ q = snd pq) Δε) @
    map (λ(r, p'). (r, snd pq)) (filter (λ(r, p') ⇒ p' = fst pq) bs) @
    map (λ(q', r). (fst pq, r)) (filter (λ(q', r) ⇒ q' = snd pq) (pq # bs))"

locale Q_list =
  fixes Δ :: "('q, 'f option × 'g option) ta_rule list" and Δε :: "('q × 'q) list"
begin

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

sublocale l: horn_list "Q_inf_rules A" "Q_infer0_list Δ" "Q_infer1_list Δε"
  apply (unfold_locales)
  unfolding Q_horn.Q_infer0 Q_horn.Q_infer1 Q_infer0_list_def Q_infer1_list_def set_append Un_assoc[symmetric]
  apply (force simp: fset_of_list_elem in_set_conv_nth)
  apply (intro arg_cong2[of _ _ _ _ "(∪)"])
  apply (auto simp flip: ex_simps(1) simp: fset_of_list_elem horn.infer0_def horn.infer1_def)
  done

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

end

definition Q_impl where
  "Q_impl Δ Δε = horn_list_impl.saturate_impl (Q_infer0_list Δ) (Q_infer1_list Δε)"

lemma Q_impl_sound:
  "Q_impl Δ Δε = Some xs ⟹ set xs = Q_inf (TA_of_lists Δ Δε)"
  using Q_list.saturate_impl_sound unfolding Q_impl_def Q_horn.Q_sound .

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


"Q_infinity_impl Δ Δε = (let Q = fset_of_list (the (Q_impl Δ Δε)) in">definition "Q_infinity_impl Δ Δε = (let Q = fset_of_list (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) |∈| fset_of_list (the (Q_impl Δ Δε)) ∧
    (p, q) |∈| fset_of_list (the (Q_impl Δ Δε)))"
  unfolding Q_infinity_impl_def
  by (auto simp: Let_def fimage_iff fBex_def) fastforce

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

lemma fQ_inf_e_code [code]:
  "fQ_inf_e (TA_of_lists Δ Δε) = Q_infinity_impl Δ Δε"
  using loop_sound_correct
  by (auto simp add: fQ_inf_e.rep_eq fmember.rep_eq)


export_code GTT_comp in Haskell
export_code GTT_trancl in Haskell
export_code Inf_reg_impl in Haskell


end