Theory P_Automata

theory P_Automata imports Labeled_Transition_Systems.LTS begin


section ‹Automata›


subsection ‹P-Automaton locale›

locale P_Automaton = LTS transition_relation 
  for transition_relation :: "('state::finite, 'label) transition set" +
  fixes Init :: "'ctr_loc::enum ⇒ 'state"
    and finals :: "'state set"
begin

definition initials :: "'state set" where
  "initials ≡ Init ` UNIV"

lemma initials_list:
  "initials = set (map Init Enum.enum)"
  using enum_UNIV unfolding initials_def by force

definition accepts_aut :: "'ctr_loc ⇒ 'label list ⇒ bool" where
  "accepts_aut ≡ λp w. (∃q ∈ finals. (Init p, w, q) ∈ trans_star)"

definition lang_aut :: "('ctr_loc * 'label list) set" where
  "lang_aut = {(p,w). accepts_aut p w}"

definition nonempty where
  "nonempty ⟷ lang_aut ≠ {}"

lemma nonempty_alt: 
  "nonempty ⟷ (∃p. ∃q ∈ finals. ∃w. (Init p, w, q) ∈ trans_star)"
  unfolding lang_aut_def nonempty_def accepts_aut_def by auto

typedef 'a mark_state = "{(Q :: 'a set, I). I ⊆ Q}"
  by auto
setup_lifting type_definition_mark_state
lift_definition get_visited :: "'a mark_state ⇒ 'a set" is fst .
lift_definition get_next :: "'a mark_state ⇒ 'a set" is snd .
lift_definition make_mark_state :: "'a set ⇒ 'a set ⇒ 'a mark_state" is "λQ J. (Q ∪ J, J)" by auto
lemma get_next_get_visited: "get_next ms ⊆ get_visited ms"
  by transfer auto
lemma get_next_set_next[simp]: "get_next (make_mark_state Q J) = J"
  by transfer auto
lemma get_visited_set_next[simp]: "get_visited (make_mark_state Q J) = Q ∪ J"
  by transfer auto

function mark where
  "mark ms ⟷
     (let Q = get_visited ms; I = get_next ms in
     if I ∩ finals ≠ {} then True
     else let J = (⋃(q,w,q')∈transition_relation. if q ∈ I ∧ q' ∉ Q then {q'} else {}) in
       if J = {} then False else mark (make_mark_state Q J))"
  by auto
termination by (relation "measure (λms. card (UNIV :: 'a set) - card (get_visited ms :: 'a set))")
    (fastforce intro!: diff_less_mono2 psubset_card_mono split: if_splits)+

declare mark.simps[simp del]

lemma trapped_transitions: "(p, w, q) ∈ trans_star ⟹
  ∀p ∈ Q. (∀γ q. (p, γ, q) ∈ transition_relation ⟶ q ∈ Q) ⟹
  p ∈ Q ⟹ q ∈ Q"
  by (induct p w q rule: trans_star.induct) auto

lemma mark_complete: "(p, w, q) ∈ trans_star ⟹ (get_visited ms - get_next ms) ∩ finals = {} ⟹
  ∀p ∈ get_visited ms - get_next ms. ∀q γ. (p, γ, q) ∈ transition_relation ⟶ q ∈ get_visited ms ⟹
  p ∈ get_visited ms ⟹ q ∈ finals ⟹ mark ms"
proof (induct p w q arbitrary: ms rule: trans_star.induct)
  case (trans_star_refl p)
  then show ?case by (subst mark.simps) (auto simp: Let_def)
next
  case step: (trans_star_step p γ q' w q)
  define J where "J ≡ ⋃(q, w, q')∈transition_relation. if q ∈ get_next ms ∧ q' ∉ get_visited ms then {q'} else {}"
  show ?case
  proof (cases "J = {}")
    case True
    then have "q' ∈ get_visited ms"
      by (smt (z3) DiffI Diff_disjoint Int_iff J_def SUP_bot_conv(2) case_prod_conv insertI1 
          step.hyps(1) step.prems(2) step.prems(3))
    with True show ?thesis
      using step(1,2,4,5,7)
      by (subst mark.simps)
        (auto 10 0 intro!: step(3) elim!: set_mp[of _ "get_next ms"] simp: split_beta J_def
          dest: trapped_transitions[of q' w q "get_visited ms"])
  next
    case False
    then have [simp]: "get_visited ms ∪ J - J = get_visited ms"
      by (auto simp: J_def split: if_splits)
    then have "p ∈ get_visited ms ⟹ (p, γ, q) ∈ transition_relation ⟹ q ∉ get_visited ms ⟹ q ∈ J" for p γ q
      using step(5)
      by (cases "p ∈ get_next ms") 
        (auto simp only: J_def simp_thms if_True if_False intro!: UN_I[of "(p, γ, q)"])
    with False show ?thesis
      using step(1,4,5,6,7)
      by (subst mark.simps)
        (auto 0 2 simp add: Let_def J_def[symmetric] disj_commute
        intro!: step(3)[of "make_mark_state (get_visited ms) J"])
  qed
qed


lemma mark_sound: "mark ms ⟹ (∃p ∈ get_next ms. ∃q ∈ finals. ∃w. (p, w, q) ∈ trans_star)"
  by (induct ms rule: mark.induct)
    (subst (asm) (2) mark.simps, fastforce dest: trans_star_step simp: Let_def split: if_splits)

lemma nonempty_code[code]: "nonempty = mark (make_mark_state {} (set (map Init Enum.enum)))"
  using mark_complete[of _ _ _ "make_mark_state {} initials"]
        mark_sound[of "make_mark_state {} initials"] nonempty_alt 
  unfolding initials_def initials_list[symmetric] by auto


end


subsection ‹Intersection P-Automaton locale›

locale Intersection_P_Automaton = 
  A1: P_Automaton ts1 Init finals1 +
  A2: P_Automaton ts2 Init finals2
  for ts1 :: "('state :: finite, 'label) transition set" 
    and Init :: "'ctr_loc :: enum ⇒ 'state" 
    and finals1 :: "'state set" 
    and ts2 :: "('state, 'label) transition set" 
    and finals2 :: "'state set" 
begin

sublocale pa: P_Automaton "inters ts1 ts2" "(λp. (Init p, Init p))" "inters_finals finals1 finals2"
  .

definition accepts_aut_inters where
  "accepts_aut_inters p w = pa.accepts_aut p w"

definition lang_aut_inters :: "('ctr_loc * 'label list) set" where
  "lang_aut_inters = {(p,w). accepts_aut_inters p w}"

lemma trans_star_inter:
  assumes "(p1, w, p2) ∈ A1.trans_star"
  assumes "(q1, w, q2) ∈ A2.trans_star"
  shows "((p1,q1), w :: 'label list, (p2,q2)) ∈ pa.trans_star"
  using assms
proof (induction w arbitrary: p1 q1)
  case (Cons α w1')
  obtain p' where p'_p: "(p1, α, p') ∈ ts1 ∧ (p', w1', p2) ∈ A1.trans_star"
    using Cons by (metis LTS.trans_star_cons) 
  obtain q' where q'_p: "(q1, α, q') ∈ ts2 ∧(q', w1', q2) ∈ A2.trans_star"
    using Cons by (metis LTS.trans_star_cons) 
  have ind: "((p', q'), w1', p2, q2) ∈ pa.trans_star"
  proof -
    have "Suc (length w1') = length (α#w1')"
      by auto
    moreover
    have "(p', w1', p2) ∈ A1.trans_star"
      using p'_p by simp
    moreover
    have "(q', w1', q2) ∈ A2.trans_star"
      using q'_p by simp
    ultimately
    show "((p', q'), w1', p2, q2) ∈ pa.trans_star"
      using Cons(1) by auto
  qed
  moreover
  have "((p1, q1), α, (p', q')) ∈ (inters ts1 ts2)"
    by (simp add: inters_def p'_p q'_p)
  ultimately
  have "((p1, q1), α#w1', p2, q2) ∈ pa.trans_star"
    by (meson LTS.trans_star.trans_star_step)
  moreover
  have "length ((α#w1')) > 0"
    by auto
  moreover
  have "hd ((α#w1')) = α"
    by auto
  ultimately
  show ?case
    by force
next
  case Nil
  then show ?case
    by (metis LTS.trans_star.trans_star_refl LTS.trans_star_empty)
qed

lemma inters_trans_star1:
  assumes "(p1q2, w :: 'label list, p2q2) ∈ pa.trans_star"
  shows "(fst p1q2, w, fst p2q2) ∈ A1.trans_star"
  using assms 
proof (induction rule: LTS.trans_star.induct[OF assms(1)])
  case (1 p)
  then show ?case
    by (simp add: LTS.trans_star.trans_star_refl) 
next
  case (2 p γ q' w q)
  then have ind: "(fst q', w, fst q) ∈ A1.trans_star"
    by auto
  from 2(1) have "(p, γ, q') ∈ 
                     {((p1, q1), α, p2, q2) |p1 q1 α p2 q2. (p1, α, p2) ∈ ts1 ∧ (q1, α, q2) ∈ ts2}"
    unfolding inters_def by auto
  then have "∃p1 q1. p = (p1, q1) ∧ (∃p2 q2. q' = (p2, q2) ∧ (p1, γ, p2) ∈ ts1 ∧ (q1, γ, q2) ∈ ts2)"
    by simp
  then obtain p1 q1 where "p = (p1, q1) ∧ (∃p2 q2. q' = (p2, q2) ∧ (p1, γ, p2) ∈ ts1 ∧ (q1, γ, q2) ∈ ts2)"
    by auto
  then show ?case
    using LTS.trans_star.trans_star_step ind by fastforce
qed

lemma inters_trans_star:
  assumes "(p1q2, w :: 'label list, p2q2) ∈ pa.trans_star"
  shows "(snd p1q2, w, snd p2q2) ∈ A2.trans_star"
  using assms 
proof (induction rule: LTS.trans_star.induct[OF assms(1)])
  case (1 p)
  then show ?case
    by (simp add: LTS.trans_star.trans_star_refl) 
next
  case (2 p γ q' w q)
  then have ind: "(snd q', w, snd q) ∈ A2.trans_star"
    by auto
  from 2(1) have "(p, γ, q') ∈ 
                     {((p1, q1), α, p2, q2) |p1 q1 α p2 q2. (p1, α, p2) ∈ ts1 ∧ (q1, α, q2) ∈ ts2}"
    unfolding inters_def by auto
  then have "∃p1 q1. p = (p1, q1) ∧ (∃p2 q2. q' = (p2, q2) ∧ (p1, γ, p2) ∈ ts1 ∧ (q1, γ, q2) ∈ ts2)"
    by simp
  then obtain p1 q1 where "p = (p1, q1) ∧ (∃p2 q2. q' = (p2, q2) ∧ (p1, γ, p2) ∈ ts1 ∧ (q1, γ, q2) ∈ ts2)"
    by auto
  then show ?case
    using LTS.trans_star.trans_star_step ind by fastforce
qed

lemma inters_trans_star_iff:
  "((p1,q2), w :: 'label list, (p2,q2)) ∈ pa.trans_star ⟷ (p1, w, p2) ∈ A1.trans_star ∧ (q2, w, q2) ∈ A2.trans_star"
  by (metis fst_conv inters_trans_star inters_trans_star1 snd_conv trans_star_inter)

lemma inters_accept_iff: "accepts_aut_inters p w ⟷ A1.accepts_aut p w ∧ A2.accepts_aut p w"
proof
  assume "accepts_aut_inters p w"
  then show "A1.accepts_aut p w ∧ A2.accepts_aut p w"
    unfolding accepts_aut_inters_def A1.accepts_aut_def A2.accepts_aut_def pa.accepts_aut_def 
    unfolding inters_finals_def 
    using inters_trans_star_iff[of _ _ w _ ]
    using SigmaE fst_conv inters_trans_star inters_trans_star1 snd_conv
    by (metis (no_types, lifting))
next
  assume a: "A1.accepts_aut p w ∧ A2.accepts_aut p w"
  then have "(∃q∈finals1. (Init p, w, q) ∈ A1.trans_star) ∧ 
             (∃q∈finals2. (Init p, w, q) ∈ A2.trans_star)" 
    unfolding A1.accepts_aut_def A2.accepts_aut_def by auto
  then show "accepts_aut_inters p w"
    unfolding accepts_aut_inters_def pa.accepts_aut_def inters_finals_def
    by (auto simp: P_Automaton.accepts_aut_def intro: trans_star_inter)
qed

lemma lang_aut_alt: 
  "pa.lang_aut = {(p, w). (p, w) ∈ lang_aut_inters}"
  unfolding pa.lang_aut_def lang_aut_inters_def accepts_aut_inters_def pa.accepts_aut_def
  by auto

lemma inters_lang: "lang_aut_inters = A1.lang_aut ∩ A2.lang_aut"
  unfolding lang_aut_inters_def A1.lang_aut_def A2.lang_aut_def using inters_accept_iff by auto

end


section ‹Automata with epsilon›


subsection ‹P-Automaton with epsilon locale›

locale P_Automaton_ε = LTS_ε transition_relation for transition_relation :: "('state::finite, 'label option) transition set" +
  fixes finals :: "'state set" and Init :: "'ctr_loc :: enum ⇒ 'state"
begin

definition accepts_aut_ε :: "'ctr_loc ⇒ 'label list ⇒ bool" where
  "accepts_aut_ε ≡ λp w. (∃q ∈ finals. (Init p, w, q) ∈ trans_star_ε)"

definition lang_aut_ε :: "('ctr_loc * 'label list) set" where
  "lang_aut_ε = {(p,w). accepts_aut_ε p w}"

definition nonempty_ε where
  "nonempty_ε ⟷ lang_aut_ε ≠ {}"

end


subsection ‹Intersection P-Automaton with epsilon locale›

locale Intersection_P_Automaton_ε = 
  A1: P_Automaton_ε ts1 finals1 Init +
  A2: P_Automaton_ε ts2 finals2 Init
  for ts1 :: "('state :: finite, 'label option) transition set" 
    and finals1 :: "'state set" 
    and Init :: "'ctr_loc :: enum ⇒ 'state"
    and ts2 :: "('state, 'label option) transition set" 
    and finals2 :: "'state set" 
begin

abbreviation ε :: "'label option" where
  "ε == None"

sublocale pa: P_Automaton_ε "inters_ε ts1 ts2" "inters_finals finals1 finals2" "(λp. (Init p, Init p))"
  .

definition accepts_aut_inters_ε where
  "accepts_aut_inters_ε p w = pa.accepts_aut_ε p w"

definition lang_aut_inters_ε :: "('ctr_loc * 'label list) set" where
  "lang_aut_inters_ε = {(p,w). accepts_aut_inters_ε p w}"


lemma trans_star_trans_star_ε_inter:
  assumes "LTS_ε.ε_exp w1 w"
  assumes "LTS_ε.ε_exp w2 w"
  assumes "(p1, w1, p2) ∈ A1.trans_star"
  assumes "(q1, w2, q2) ∈ A2.trans_star"
  shows "((p1,q1), w :: 'label list, (p2,q2)) ∈ pa.trans_star_ε"
  using assms
proof (induction "length w1 + length w2" arbitrary: w1 w2 w p1 q1 rule: less_induct)
  case less
  then show ?case
  proof (cases "∃α w1' w2' β. w1=Some α#w1' ∧ w2=Some β#w2'")
    case True
    from True obtain α β w1' w2' where True'':
      "w1=Some α#w1'"
      "w2=Some β#w2'"
      by auto
    have "α = β"
      by (metis True''(1) True''(2) LTS_ε.ε_exp_Some_hd less.prems(1) less.prems(2))
    then have True':   
      "w1=Some α#w1'"
      "w2=Some α#w2'"
      using True'' by auto
    define w' where "w' = tl w"
    obtain p' where p'_p: "(p1, Some α, p') ∈ ts1 ∧ (p', w1', p2) ∈ A1.trans_star"
      using less True'(1) by (metis LTS_ε.trans_star_cons_ε)
    obtain q' where q'_p: "(q1, Some α, q') ∈ ts2 ∧(q', w2', q2) ∈ A2.trans_star"
      using less True'(2) by (metis LTS_ε.trans_star_cons_ε) 
    have ind: "((p', q'), w', p2, q2) ∈ pa.trans_star_ε"
    proof -
      have "length w1' + length w2' < length w1 + length w2"
        using True'(1) True'(2) by simp
      moreover
      have "LTS_ε.ε_exp w1' w'"
        by (metis (no_types) LTS_ε.ε_exp_def less(2) True'(1) list.map(2) list.sel(3) 
            option.simps(3) removeAll.simps(2) w'_def)
      moreover
      have "LTS_ε.ε_exp w2' w'"
        by (metis (no_types) LTS_ε.ε_exp_def less(3) True'(2) list.map(2) list.sel(3)
            option.simps(3) removeAll.simps(2) w'_def)
      moreover
      have "(p', w1', p2) ∈ A1.trans_star"
        using p'_p by simp
      moreover
      have "(q', w2', q2) ∈ A2.trans_star"
        using q'_p by simp
      ultimately
      show "((p', q'), w', p2, q2) ∈ pa.trans_star_ε"
        using less(1)[of w1' w2' w' p' q'] by auto
    qed
    moreover
    have "((p1, q1), Some α, (p', q')) ∈ (inters_ε ts1 ts2)"
      by (simp add: inters_ε_def p'_p q'_p)
    ultimately
    have "((p1, q1), α#w', p2, q2) ∈ pa.trans_star_ε"
      by (meson LTS_ε.trans_star_ε.trans_star_ε_step_γ)
    moreover
    have "length w > 0"
      using less(3) True' LTS_ε.ε_exp_Some_length by metis
    moreover
    have "hd w = α"
      using less(3) True' LTS_ε.ε_exp_Some_hd by metis
    ultimately
    show ?thesis
      using w'_def by force
  next
    case False
    note False_outer_outer_outer_outer = False
    show ?thesis 
    proof (cases "w1 = [] ∧ w2 = []")
      case True
      then have same: "p1 = p2 ∧ q1 = q2"
        by (metis LTS.trans_star_empty less.prems(3) less.prems(4))
      have "w = []"
        using True less(2) LTS_ε.exp_empty_empty by auto
      then show ?thesis
        using less True
        by (simp add: LTS_ε.trans_star_ε.trans_star_ε_refl same)
    next
      case False
      note False_outer_outer_outer = False
      show ?thesis
      proof (cases "∃w1'. w1=ε#w1'")
        case True (* Adapted from above. Maybe they can be merged. *)
        then obtain w1' where True':
          "w1=ε#w1'"
          by auto
        obtain p' where p'_p: "(p1, ε, p') ∈ ts1 ∧ (p', w1', p2) ∈ A1.trans_star"
          using less True'(1) by (metis LTS_ε.trans_star_cons_ε)
        have q'_p: "(q1, w2, q2) ∈ A2.trans_star"
          using less by metis
        have ind: "((p', q1), w, p2, q2) ∈ pa.trans_star_ε"
        proof -
          have "length w1' + length w2 < length w1 + length w2"
            using True'(1) by simp
          moreover
          have "LTS_ε.ε_exp w1' w"
            by (metis (no_types) LTS_ε.ε_exp_def less(2) True'(1) removeAll.simps(2))
          moreover
          have "LTS_ε.ε_exp w2 w"
            by (metis (no_types) less(3))
          moreover
          have "(p', w1', p2) ∈ A1.trans_star"
            using p'_p by simp
          moreover
          have "(q1, w2, q2) ∈ A2.trans_star"
            using q'_p by simp
          ultimately
          show "((p', q1), w, p2, q2) ∈ pa.trans_star_ε"
            using less(1)[of w1' w2 w p' q1] by auto
        qed
        moreover
        have "((p1, q1), ε, (p', q1)) ∈ (inters_ε ts1 ts2)"
          by (simp add: inters_ε_def p'_p q'_p)
        ultimately
        have "((p1, q1), w, p2, q2) ∈ pa.trans_star_ε"
          using LTS_ε.trans_star_ε.simps by fastforce
        then
        show ?thesis
           by force
      next
        case False
        note False_outer_outer = False
        then show ?thesis
        proof (cases "∃w2'. w2 = ε # w2'")
          case True (* Adapted from above. Maybe they can be merged. *)
          then obtain w2' where True':
            "w2=ε#w2'"
            by auto
          have p'_p: "(p1, w1, p2) ∈ A1.trans_star"
            using less by (metis)
          obtain q' where q'_p: "(q1, ε, q') ∈ ts2 ∧(q', w2', q2) ∈ A2.trans_star"
            using less True'(1) by (metis LTS_ε.trans_star_cons_ε) 
          have ind: "((p1, q'), w, p2, q2) ∈ pa.trans_star_ε"
          proof -
            have "length w1 + length w2' < length w1 + length w2"
              using True'(1) True'(1) by simp
            moreover
            have "LTS_ε.ε_exp w1 w"
              by (metis (no_types) less(2))
            moreover
            have "LTS_ε.ε_exp w2' w"
              by (metis (no_types) LTS_ε.ε_exp_def less(3) True'(1) removeAll.simps(2))
            moreover
            have "(p1, w1, p2) ∈ A1.trans_star"
              using p'_p by simp
            moreover
            have "(q', w2', q2) ∈ A2.trans_star"
              using q'_p by simp
            ultimately
            show "((p1, q'), w, p2, q2) ∈ pa.trans_star_ε"
              using less(1)[of w1 w2' w p1 q'] by auto
          qed
          moreover
          have "((p1, q1), ε, (p1, q')) ∈ inters_ε ts1 ts2"
            by (simp add: inters_ε_def p'_p q'_p)
          ultimately
          have "((p1, q1), w, p2, q2) ∈ pa.trans_star_ε"
            using LTS_ε.trans_star_ε.simps by fastforce
          then
          show ?thesis
            by force
        next
          case False
          then have "(w1 = [] ∧ (∃α w2'. w2 = Some α # w2')) ∨ ((∃α w1'. w1 = Some α # w1') ∧ w2 = [])"
            using False_outer_outer False_outer_outer_outer False_outer_outer_outer_outer
            by (metis neq_Nil_conv option.exhaust_sel)
          then show ?thesis
            by (metis LTS_ε.ε_exp_def LTS_ε.ε_exp_Some_length less.prems(1) less.prems(2) 
                less_numeral_extra(3) list.simps(8) list.size(3) removeAll.simps(1))
        qed
      qed
    qed
  qed
qed

lemma trans_star_ε_inter:
  assumes "(p1, w :: 'label list, p2) ∈ A1.trans_star_ε"
  assumes "(q1, w, q2) ∈ A2.trans_star_ε"
  shows "((p1, q1), w, (p2, q2)) ∈ pa.trans_star_ε"
proof -
  have "∃w1'. LTS_ε.ε_exp w1' w ∧ (p1, w1', p2) ∈ A1.trans_star"
    using assms by (simp add: LTS_ε.trans_star_ε_ε_exp_trans_star)
  then obtain w1' where "LTS_ε.ε_exp w1' w ∧ (p1, w1', p2) ∈ A1.trans_star"
    by auto
  moreover
  have "∃w2'. LTS_ε.ε_exp w2' w ∧ (q1, w2', q2) ∈ A2.trans_star"
    using assms by (simp add: LTS_ε.trans_star_ε_ε_exp_trans_star)
  then obtain w2' where "LTS_ε.ε_exp w2' w ∧ (q1, w2', q2) ∈ A2.trans_star"
    by auto
  ultimately
  show ?thesis
    using trans_star_trans_star_ε_inter by metis
qed

lemma inters_trans_star_ε1:
  assumes "(p1q2, w :: 'label list, p2q2) ∈ pa.trans_star_ε"
  shows "(fst p1q2, w, fst p2q2) ∈ A1.trans_star_ε"
  using assms 
proof (induction rule: LTS_ε.trans_star_ε.induct[OF assms(1)])
  case (1 p)
  then show ?case
    by (simp add: LTS_ε.trans_star_ε.trans_star_ε_refl)
next
  case (2 p γ q' w q)
  then have ind: "(fst q', w, fst q) ∈ A1.trans_star_ε"
    by auto
  from 2(1) have "(p, Some γ, q') ∈ 
                     {((p1, q1), α, p2, q2) |p1 q1 α p2 q2. (p1, α, p2) ∈ ts1 ∧ (q1, α, q2) ∈ ts2} ∪ 
                     {((p1, q1), ε, p2, q1) |p1 p2 q1. (p1, ε, p2) ∈ ts1} ∪
                     {((p1, q1), ε, p1, q2) |p1 q1 q2. (q1, ε, q2) ∈ ts1}"
    unfolding inters_ε_def by auto
  moreover                
  {
    assume "(p, Some γ, q') ∈ {((p1, q1), α, p2, q2) |p1 q1 α p2 q2. (p1, α, p2) ∈ ts1 ∧ (q1, α, q2) ∈ ts2}"
    then have "∃p1 q1. p = (p1, q1) ∧ (∃p2 q2. q' = (p2, q2) ∧ (p1, Some γ, p2) ∈ ts1 ∧ (q1, Some γ, q2) ∈ ts2)"
      by simp
    then obtain p1 q1 where "p = (p1, q1) ∧ (∃p2 q2. q' = (p2, q2) ∧ (p1, Some γ, p2) ∈ ts1 ∧ (q1, Some γ, q2) ∈ ts2)"
      by auto
    then have ?case
      using LTS_ε.trans_star_ε.trans_star_ε_step_γ ind by fastforce
  }
  moreover
  {
    assume "(p, Some γ, q') ∈ {((p1, q1), ε, p2, q1) |p1 p2 q1. (p1, ε, p2) ∈ ts1}"
    then have ?case
      by auto
  }
  moreover
  {
    assume "(p, Some γ, q') ∈ {((p1, q1), ε, p1, q2) |p1 q1 q2. (q1, ε, q2) ∈ ts1}"
    then have ?case
      by auto
  }  
  ultimately 
  show ?case 
    by auto
next
  case (3 p q' w q)
  then have ind: "(fst q', w, fst q) ∈ A1.trans_star_ε"
    by auto
  from 3(1) have "(p, ε, q') ∈
                     {((p1, q1), α, (p2, q2)) | p1 q1 α p2 q2. (p1, α, p2) ∈ ts1 ∧ (q1, α, q2) ∈ ts2} ∪
                     {((p1, q1), ε, (p2, q1)) | p1 p2 q1. (p1, ε, p2) ∈ ts1} ∪
                     {((p1, q1), ε, (p1, q2)) | p1 q1 q2. (q1, ε, q2) ∈ ts2}"
    unfolding inters_ε_def by auto
  moreover                
  {
    assume "(p, ε, q') ∈ {((p1, q1), α, p2, q2) |p1 q1 α p2 q2. (p1, α, p2) ∈ ts1 ∧ (q1, α, q2) ∈ ts2}"
    then have "∃p1 q1. p = (p1, q1) ∧ (∃p2 q2. q' = (p2, q2) ∧ (p1, ε, p2) ∈ ts1 ∧ (q1, ε, q2) ∈ ts2)"
      by simp
    then obtain p1 q1 where "p = (p1, q1) ∧ (∃p2 q2. q' = (p2, q2) ∧ (p1, ε, p2) ∈ ts1 ∧ (q1, ε, q2) ∈ ts2)"
      by auto
    then have ?case
      using LTS_ε.trans_star_ε.trans_star_ε_step_ε ind by fastforce
  }
  moreover
  {
    assume "(p, ε, q') ∈ {((p1, q1), ε, p2, q1) |p1 p2 q1. (p1, ε, p2) ∈ ts1}"
    then have "∃p1 p2 q1. p = (p1, q1) ∧ q' = (p2, q1) ∧ (p1, ε, p2) ∈ ts1"
      by auto
    then obtain p1 p2 q1 where "p = (p1, q1) ∧ q' = (p2, q1) ∧ (p1, ε, p2) ∈ ts1"
      by auto
    then have ?case
      using LTS_ε.trans_star_ε.trans_star_ε_step_ε ind by fastforce
  }
  moreover
  {
    assume "(p, ε, q') ∈ {((p1, q1), ε, p1, q2) |p1 q1 q2. (q1, ε, q2) ∈ ts2}"
    then have "∃p1 q1 q2. p = (p1, q1) ∧ q' = (p1, q2) ∧ (q1, ε, q2) ∈ ts2"
      by auto
    then obtain p1 q1 q2 where "p = (p1, q1) ∧ q' = (p1, q2) ∧ (q1, ε, q2) ∈ ts2"
      by auto
    then have ?case
      using LTS_ε.trans_star_ε.trans_star_ε_step_ε ind by fastforce
  }  
  ultimately 
  show ?case 
    by auto
qed

lemma inters_trans_star_ε:
  assumes "(p1q2, w :: 'label list, p2q2) ∈ pa.trans_star_ε"
  shows "(snd p1q2, w, snd p2q2) ∈ A2.trans_star_ε"
  using assms 
proof (induction rule: LTS_ε.trans_star_ε.induct[OF assms(1)])
  case (1 p)
  then show ?case
    by (simp add: LTS_ε.trans_star_ε.trans_star_ε_refl) 
next
  case (2 p γ q' w q)
  then have ind: "(snd q', w, snd q) ∈ A2.trans_star_ε"
    by auto
  from 2(1) have "(p, Some γ, q') ∈ 
                     {((p1, q1), α, p2, q2) |p1 q1 α p2 q2. (p1, α, p2) ∈ ts1 ∧ (q1, α, q2) ∈ ts2} ∪ 
                     {((p1, q1), ε, p2, q1) |p1 p2 q1. (p1, ε, p2) ∈ ts1} ∪
                     {((p1, q1), ε, p1, q2) |p1 q1 q2. (q1, ε, q2) ∈ ts2}"
    unfolding inters_ε_def by auto
  moreover                
  {
    assume "(p, Some γ, q') ∈ {((p1, q1), α, p2, q2) |p1 q1 α p2 q2. (p1, α, p2) ∈ ts1 ∧ (q1, α, q2) ∈ ts2}"
    then have "∃p1 q1. p = (p1, q1) ∧ (∃p2 q2. q' = (p2, q2) ∧ (p1, Some γ, p2) ∈ ts1 ∧ (q1, Some γ, q2) ∈ ts2)"
      by simp
    then obtain p1 q1 where "p = (p1, q1) ∧ (∃p2 q2. q' = (p2, q2) ∧ (p1, Some γ, p2) ∈ ts1 ∧ (q1, Some γ, q2) ∈ ts2)"
      by auto
    then have ?case
      using LTS_ε.trans_star_ε.trans_star_ε_step_γ ind by fastforce
  }
  moreover
  {
    assume "(p, Some γ, q') ∈ {((p1, q1), ε, p2, q1) |p1 p2 q1. (p1, ε, p2) ∈ ts1}"
    then have ?case
      by auto
  }
  moreover
  {
    assume "(p, Some γ, q') ∈ {((p1, q1), ε, p1, q2) |p1 q1 q2. (q1, ε, q2) ∈ ts2}"
    then have ?case
      by auto
  }  
  ultimately 
  show ?case 
    by auto
next
  case (3 p q' w q)
  then have ind: "(snd q', w, snd q) ∈ A2.trans_star_ε"
    by auto
  from 3(1) have "(p, ε, q') ∈
                     {((p1, q1), α, (p2, q2)) | p1 q1 α p2 q2. (p1, α, p2) ∈ ts1 ∧ (q1, α, q2) ∈ ts2} ∪
                     {((p1, q1), ε, (p2, q1)) | p1 p2 q1. (p1, ε, p2) ∈ ts1} ∪
                     {((p1, q1), ε, (p1, q2)) | p1 q1 q2. (q1, ε, q2) ∈ ts2}"
    unfolding inters_ε_def by auto
  moreover                
  {
    assume "(p, ε, q') ∈ {((p1, q1), α, p2, q2) |p1 q1 α p2 q2. (p1, α, p2) ∈ ts1 ∧ (q1, α, q2) ∈ ts2}"
    then have "∃p1 q1. p = (p1, q1) ∧ (∃p2 q2. q' = (p2, q2) ∧ (p1, ε, p2) ∈ ts1 ∧ (q1, ε, q2) ∈ ts2)"
      by simp
    then obtain p1 q1 where "p = (p1, q1) ∧ (∃p2 q2. q' = (p2, q2) ∧ (p1, ε, p2) ∈ ts1 ∧ (q1, ε, q2) ∈ ts2)"
      by auto
    then have ?case
      using LTS_ε.trans_star_ε.trans_star_ε_step_ε ind by fastforce
  }
  moreover
  {
    assume "(p, ε, q') ∈ {((p1, q1), ε, p2, q1) |p1 p2 q1. (p1, ε, p2) ∈ ts1}"
    then have "∃p1 p2 q1. p = (p1, q1) ∧ q' = (p2, q1) ∧ (p1, ε, p2) ∈ ts1"
      by auto
    then obtain p1 p2 q1 where "p = (p1, q1) ∧ q' = (p2, q1) ∧ (p1, ε, p2) ∈ ts1"
      by auto
    then have ?case
      using LTS_ε.trans_star_ε.trans_star_ε_step_ε ind by fastforce
  }
  moreover
  {
    assume "(p, ε, q') ∈ {((p1, q1), ε, p1, q2) |p1 q1 q2. (q1, ε, q2) ∈ ts2}"
    then have "∃p1 q1 q2. p = (p1, q1) ∧ q' = (p1, q2) ∧ (q1, ε, q2) ∈ ts2"
      by auto
    then obtain p1 q1 q2 where "p = (p1, q1) ∧ q' = (p1, q2) ∧ (q1, ε, q2) ∈ ts2"
      by auto
    then have ?case
      using LTS_ε.trans_star_ε.trans_star_ε_step_ε ind by fastforce
  }
  ultimately
  show ?case
    by auto
qed

lemma inters_trans_star_ε_iff:
  "((p1,q2), w :: 'label list, (p2,q2)) ∈ pa.trans_star_ε ⟷ 
   (p1, w, p2) ∈ A1.trans_star_ε ∧ (q2, w, q2) ∈ A2.trans_star_ε"
  by (metis fst_conv inters_trans_star_ε inters_trans_star_ε1 snd_conv trans_star_ε_inter)

lemma inters_ε_accept_ε_iff: 
  "accepts_aut_inters_ε p w ⟷ A1.accepts_aut_ε p w ∧ A2.accepts_aut_ε p w"
proof
  assume "accepts_aut_inters_ε p w"
  then show "A1.accepts_aut_ε p w ∧ A2.accepts_aut_ε p w"
    unfolding accepts_aut_inters_ε_def A1.accepts_aut_ε_def A2.accepts_aut_ε_def pa.accepts_aut_ε_def 
    unfolding inters_finals_def 
    using inters_trans_star_ε_iff[of _ _ w _ ]
    using SigmaE fst_conv inters_trans_star_ε inters_trans_star_ε1 snd_conv
    by (metis (no_types, lifting))
next
  assume a: "A1.accepts_aut_ε p w ∧ A2.accepts_aut_ε p w"
  then have "(∃q∈finals1. (Init p, w, q) ∈ A1.trans_star_ε) ∧ 
             (∃q∈finals2. (Init p, w, q) ∈ LTS_ε.trans_star_ε ts2)" 
    unfolding A1.accepts_aut_ε_def A2.accepts_aut_ε_def by auto
  then show "accepts_aut_inters_ε p w"
    unfolding accepts_aut_inters_ε_def pa.accepts_aut_ε_def inters_finals_def
    by (auto simp: P_Automaton_ε.accepts_aut_ε_def intro: trans_star_ε_inter)
qed

lemma inters_ε_lang_ε: "lang_aut_inters_ε = A1.lang_aut_ε ∩ A2.lang_aut_ε"
  unfolding lang_aut_inters_ε_def P_Automaton_ε.lang_aut_ε_def using inters_ε_accept_ε_iff by auto

end

end