Theory Regular_Tree_Relations.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