Theory Regular_Relation_Abstract_Impl

theory Regular_Relation_Abstract_Impl
  imports Pair_Automaton
    GTT_Transitive_Closure
    RR2_Infinite_Q_infinity
    Horn_Fset
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 "[]"]
  by auto (metis length_greater_0_conv zip_eq_Nil_iff)+

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

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

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)
  
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

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)
  qed
qed

end


end