# 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
```