# Theory PDS

```theory PDS imports "P_Automata" "HOL-Library.While_Combinator" begin

section ‹PDS›

datatype 'label operation = pop | swap 'label | push 'label 'label
type_synonym ('ctr_loc, 'label) rule = "('ctr_loc × 'label) × ('ctr_loc × 'label operation)"
type_synonym ('ctr_loc, 'label) conf = "'ctr_loc × 'label list"

text ‹We define push down systems.›

locale PDS =
fixes Δ :: "('ctr_loc, 'label::finite) rule set"
(* 'ctr_loc is the type of control locations *)

begin

primrec lbl :: "'label operation ⇒ 'label list" where
"lbl pop = []"
| "lbl (swap γ) = [γ]"
| "lbl (push γ  γ') = [γ, γ']"

definition is_rule :: "'ctr_loc × 'label ⇒ 'ctr_loc × 'label operation ⇒ bool" (infix "↪" 80) where
"pγ ↪ p'w ≡ (pγ,p'w) ∈ Δ"

inductive_set transition_rel :: "(('ctr_loc, 'label) conf × unit × ('ctr_loc, 'label) conf) set" where
"(p, γ) ↪ (p', w) ⟹
((p, γ#w'), (), (p', (lbl w)@w')) ∈ transition_rel"

interpretation LTS transition_rel .

notation step_relp (infix "⇒" 80)
notation step_starp (infix "⇒⇧*" 80)

lemma step_relp_def2:
"(p, γw') ⇒ (p',ww') ⟷ (∃γ w' w. γw' = γ#w' ∧ ww' = (lbl w)@w' ∧ (p, γ) ↪ (p', w))"
by (metis (no_types, lifting) PDS.transition_rel.intros step_relp_def transition_rel.cases)

end

section ‹PDS with P automata›

type_synonym ('ctr_loc, 'label) sat_rule = "('ctr_loc, 'label) transition set ⇒ ('ctr_loc, 'label) transition set ⇒ bool"

datatype ('ctr_loc, 'noninit, 'label) state =
is_Init: Init (the_Ctr_Loc: 'ctr_loc) (* p ∈ P *)
| is_Noninit: Noninit (the_St: 'noninit) (* q ∈ Q ∧ q ∉ P *)
| is_Isolated: Isolated (the_Ctr_Loc: 'ctr_loc) (the_Label: 'label) (* q⇩p⇩γ *)

lemma finitely_many_states:
assumes "finite (UNIV :: 'ctr_loc set)"
assumes "finite (UNIV :: 'noninit set)"
assumes "finite (UNIV :: 'label set)"
shows "finite (UNIV :: ('ctr_loc, 'noninit, 'label) state set)"
proof -
define Isolated' :: "('ctr_loc * 'label) ⇒ ('ctr_loc, 'noninit, 'label) state" where
"Isolated' == λ(c :: 'ctr_loc, l:: 'label). Isolated c l"
define Init' :: "'ctr_loc ⇒ ('ctr_loc, 'noninit, 'label) state" where
"Init' = Init"
define Noninit' :: "'noninit ⇒ ('ctr_loc, 'noninit, 'label) state" where
"Noninit' = Noninit"

have split: "UNIV = (Init' ` UNIV) ∪ (Noninit' ` UNIV) ∪ (Isolated' ` (UNIV :: (('ctr_loc * 'label) set)))"
unfolding Init'_def Noninit'_def
proof (rule; rule; rule; rule)
fix x :: "('ctr_loc, 'noninit, 'label) state"
assume "x ∈ UNIV"
moreover
assume "x ∉ range Isolated'"
moreover
assume "x ∉ range Noninit"
ultimately
show "x ∈ range Init"
by (metis Isolated'_def prod.simps(2) range_eqI state.exhaust)
qed

have "finite (Init' ` (UNIV:: 'ctr_loc set))"
using assms by auto
moreover
have "finite (Noninit' ` (UNIV:: 'noninit set))"
using assms by auto
moreover
have "finite (UNIV :: (('ctr_loc * 'label) set))"
using assms by (simp add: finite_Prod_UNIV)
then have "finite (Isolated' ` (UNIV :: (('ctr_loc * 'label) set)))"
by auto
ultimately
show "finite (UNIV :: ('ctr_loc, 'noninit, 'label) state set)"
unfolding split by auto
qed

instantiation state :: (finite, finite, finite) finite begin

instance by standard (simp add: finitely_many_states)

end

locale PDS_with_P_automata = PDS Δ
for Δ :: "('ctr_loc::enum, 'label::finite) rule set"
+
fixes final_inits :: "('ctr_loc::enum) set"
fixes final_noninits :: "('noninit::finite) set"
begin

(* Corresponds to Schwoon's F *)
definition finals :: "('ctr_loc, 'noninit::finite, 'label) state set" where
"finals = Init ` final_inits ∪ Noninit ` final_noninits"

lemma F_not_Ext: "¬(∃f∈finals. is_Isolated f)"
using finals_def by fastforce

(* Corresponds to Schwoon's P *)
definition inits :: "('ctr_loc, 'noninit, 'label) state set" where
"inits = {q. is_Init q}"

lemma inits_code[code]: "inits = set (map Init Enum.enum)"
by (auto simp: inits_def is_Init_def simp flip: UNIV_enum)

definition noninits :: "('ctr_loc, 'noninit, 'label) state set" where
"noninits = {q. is_Noninit q}"

definition isols :: "('ctr_loc, 'noninit, 'label) state set" where
"isols = {q. is_Isolated q}"

sublocale LTS transition_rel .
notation step_relp (infix "⇒" 80)
notation step_starp (infix "⇒⇧*" 80)

definition accepts :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition set ⇒ ('ctr_loc, 'label) conf ⇒ bool" where
"accepts ts ≡ λ(p,w). (∃q ∈ finals. (Init p,w,q) ∈ LTS.trans_star ts)"

lemma accepts_accepts_aut: "accepts ts (p, w) ⟷ P_Automaton.accepts_aut ts Init finals p w"
unfolding accepts_def P_Automaton.accepts_aut_def inits_def by auto

definition accepts_ε :: "(('ctr_loc, 'noninit, 'label) state, 'label option) transition set ⇒ ('ctr_loc, 'label) conf ⇒ bool" where
"accepts_ε ts ≡ λ(p,w). (∃q ∈ finals. (Init p,w,q) ∈ LTS_ε.trans_star_ε ts)"

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

lemma accepts_mono[mono]: "mono accepts"
proof (rule, rule)
fix c :: "('ctr_loc, 'label) conf"
fix ts ts' :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition set"
assume accepts_ts: "accepts ts c"
assume tsts': "ts ⊆ ts'"
obtain p l where pl_p: "c = (p,l)"
by (cases c)
obtain q where q_p:  "q ∈ finals ∧ (Init p, l, q) ∈ LTS.trans_star ts"
using accepts_ts unfolding pl_p accepts_def by auto
then have "(Init p, l, q) ∈ LTS.trans_star ts'"
using tsts' LTS_trans_star_mono monoD by blast
then have "accepts ts' (p,l)"
unfolding accepts_def using q_p by auto
then show "accepts ts' c"
unfolding pl_p .
qed

lemma accepts_cons: "(Init p, γ, Init p') ∈ ts ⟹ accepts ts (p', w) ⟹ accepts ts (p, γ # w)"
using LTS.trans_star.trans_star_step accepts_def by fastforce

definition lang :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition set ⇒ ('ctr_loc, 'label) conf set" where
"lang ts = {c. accepts ts c}"

lemma lang_lang_aut: "lang ts = (λ(s,w). (s, w)) ` (P_Automaton.lang_aut ts Init finals)"
unfolding lang_def P_Automaton.lang_aut_def
by (auto simp: inits_def accepts_def P_Automaton.accepts_aut_def image_iff intro!: exI[of _ "Init _"])

lemma lang_aut_lang: "P_Automaton.lang_aut ts Init finals = lang ts"
unfolding lang_lang_aut
by (auto 0 3 simp: P_Automaton.lang_aut_def P_Automaton.accepts_aut_def inits_def image_iff)

definition lang_ε :: "(('ctr_loc, 'noninit, 'label) state, 'label option) transition set ⇒ ('ctr_loc, 'label) conf set" where
"lang_ε ts = {c. accepts_ε ts c}"

subsection ‹Saturations›

definition saturated :: "('c, 'l) sat_rule ⇒ ('c, 'l) transition set ⇒ bool" where
"saturated rule ts ⟷ (∄ts'. rule ts ts')"

definition saturation :: "('c, 'l) sat_rule ⇒ ('c, 'l) transition set ⇒ ('c, 'l) transition set ⇒ bool" where
"saturation rule ts ts' ⟷ rule⇧*⇧* ts ts' ∧ saturated rule ts'"

lemma no_infinite:
assumes "⋀ts ts' :: ('c ::finite, 'l::finite) transition set. rule ts ts' ⟹ card ts' = Suc (card ts)"
assumes "∀i :: nat. rule (tts i) (tts (Suc i))"
shows "False"
proof -
define f where "f i = card (tts i)" for i
have f_Suc: "∀i. f i < f (Suc i)"
using assms f_def lessI by metis
have "∀i. ∃j. f j > i"
proof
fix i
show "∃j. i < f j"
proof(induction i)
case 0
then show ?case
by (metis f_Suc neq0_conv)
next
case (Suc i)
then show ?case
by (metis Suc_lessI f_Suc)
qed
qed
then have "∃j. f j > card (UNIV :: ('c, 'l) transition set)"
by auto
then show False
by (metis card_seteq f_def finite_UNIV le_eq_less_or_eq nat_neq_iff subset_UNIV)
qed

lemma saturation_termination:
assumes "⋀ts ts' :: ('c ::finite, 'l::finite) transition set. rule ts ts' ⟹ card ts' = Suc (card ts)"
shows "¬(∃tts. (∀i :: nat. rule (tts i) (tts (Suc i))))"
using assms no_infinite by blast

lemma saturation_exi:
assumes "⋀ts ts' :: ('c ::finite, 'l::finite) transition set. rule ts ts' ⟹ card ts' = Suc (card ts)"
shows "∃ts'. saturation rule ts ts'"
proof (rule ccontr)
assume a: "∄ts'. saturation rule ts ts'"
define g where "g ts = (SOME ts'. rule ts ts')" for ts
define tts where "tts i = (g ^^ i) ts" for i
have "∀i :: nat. rule⇧*⇧* ts (tts i) ∧ rule (tts i) (tts (Suc i))"
proof
fix i
show "rule⇧*⇧* ts (tts i) ∧ rule (tts i) (tts (Suc i))"
proof (induction i)
case 0
have "rule ts (g ts)"
by (metis g_def a rtranclp.rtrancl_refl saturation_def saturated_def someI)
then show ?case
using tts_def a saturation_def by auto
next
case (Suc i)
then have sat_Suc: "rule⇧*⇧* ts (tts (Suc i))"
by fastforce
then have "rule (g ((g ^^ i) ts)) (g (g ((g ^^ i) ts)))"
by (metis Suc.IH tts_def g_def a r_into_rtranclp rtranclp_trans saturation_def saturated_def
someI)
then have "rule (tts (Suc i)) (tts (Suc (Suc i)))"
unfolding tts_def by simp
then show ?case
using sat_Suc by auto
qed
qed
then have "∀i. rule (tts i) (tts (Suc i))"
by auto
then show False
using no_infinite assms by auto
qed

subsection ‹Saturation rules›

inductive pre_star_rule :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition set ⇒ (('ctr_loc, 'noninit, 'label) state, 'label) transition set ⇒ bool" where
add_trans: "(p, γ) ↪ (p', w) ⟹ (Init p', lbl w, q) ∈ LTS.trans_star ts ⟹
(Init p, γ, q) ∉ ts ⟹ pre_star_rule ts (ts ∪ {(Init p, γ, q)})"

definition pre_star1 :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition set ⇒ (('ctr_loc, 'noninit, 'label) state, 'label) transition set" where
"pre_star1 ts =
(⋃((p, γ), (p', w)) ∈ Δ. ⋃q ∈ LTS.reach ts (Init p') (lbl w). {(Init p, γ, q)})"

lemma pre_star1_mono: "mono pre_star1"
unfolding pre_star1_def
by (auto simp: mono_def LTS.trans_star_code[symmetric] elim!: bexI[rotated]
LTS_trans_star_mono[THEN monoD, THEN subsetD])

lemma pre_star_rule_pre_star1:
assumes "X ⊆ pre_star1 ts"
shows "pre_star_rule⇧*⇧* ts (ts ∪ X)"
proof -
have "finite X"
by simp
from this assms show ?thesis
proof (induct X arbitrary: ts rule: finite_induct)
case (insert x F)
then obtain p γ p' w q where *: "(p, γ) ↪ (p', w)"
"(Init p', lbl w, q) ∈ LTS.trans_star ts" and x:
"x = (Init p, γ, q)"
by (auto simp: pre_star1_def is_rule_def LTS.trans_star_code)
with insert show ?case
proof (cases "(Init p, γ, q) ∈ ts")
case False
with insert(1,2,4) x show ?thesis
by (intro converse_rtranclp_into_rtranclp[of pre_star_rule, OF add_trans[OF * False]])
(auto intro!: insert(3)[of "insert x ts", simplified x Un_insert_left]
intro: pre_star1_mono[THEN monoD, THEN set_mp, of ts])
qed simp
qed

lemma pre_star_rule_pre_star1s: "pre_star_rule⇧*⇧* ts (((λs. s ∪ pre_star1 s) ^^ k) ts)"
by (induct k) (auto elim!: rtranclp_trans intro: pre_star_rule_pre_star1)

definition "pre_star_loop = while_option (λs. s ∪ pre_star1 s ≠ s) (λs. s ∪ pre_star1 s)"
definition "pre_star_exec = the o pre_star_loop"
definition "pre_star_exec_check A = (if inits ⊆ LTS.srcs A then pre_star_loop A else None)"

definition "accept_pre_star_exec_check A c = (if inits ⊆ LTS.srcs A then Some (accepts (pre_star_exec A) c) else None)"

lemma while_option_finite_subset_Some: fixes C :: "'a set"
assumes "mono f" and "!!X. X ⊆ C ⟹ f X ⊆ C" and "finite C" and X: "X ⊆ C" "X ⊆ f X"
shows "∃P. while_option (λA. f A ≠ A) f X = Some P"
proof(rule measure_while_option_Some[where
f= "%A::'a set. card C - card A" and P= "%A. A ⊆ C ∧ A ⊆ f A" and s= X])
fix A assume A: "A ⊆ C ∧ A ⊆ f A" "f A ≠ A"
show "(f A ⊆ C ∧ f A ⊆ f (f A)) ∧ card C - card (f A) < card C - card A"
(is "?L ∧ ?R")
proof
show ?L by(metis A(1) assms(2) monoD[OF ‹mono f›])
show ?R
by (metis A assms(2,3) card_seteq diff_less_mono2 equalityI linorder_le_less_linear
rev_finite_subset)
qed

lemma pre_star_exec_terminates: "∃t. pre_star_loop s = Some t"
unfolding pre_star_loop_def
by (rule while_option_finite_subset_Some[where C=UNIV])
(auto simp: mono_def dest: pre_star1_mono[THEN monoD])

lemma pre_star_exec_code[code]:
"pre_star_exec s = (let s' = pre_star1 s in if s' ⊆ s then s else pre_star_exec (s ∪ s'))"
unfolding pre_star_exec_def pre_star_loop_def o_apply
by (subst while_option_unfold)(auto simp: Let_def)

lemma saturation_pre_star_exec: "saturation pre_star_rule ts (pre_star_exec ts)"
proof -
from pre_star_exec_terminates obtain t where t: "pre_star_loop ts = Some t"
by blast
obtain k where k: "t = ((λs. s ∪ pre_star1 s) ^^ k) ts" and le: "pre_star1 t ⊆ t"
using while_option_stop2[OF t[unfolded pre_star_loop_def]] by auto
have "(⋃{us. pre_star_rule t us}) - t ⊆ pre_star1 t"
by (auto simp: pre_star1_def LTS.trans_star_code[symmetric] prod.splits is_rule_def
pre_star_rule.simps)
from subset_trans[OF this le] show ?thesis
unfolding saturation_def saturated_def pre_star_exec_def o_apply k t
by (auto 9 0 simp: pre_star_rule_pre_star1s subset_eq pre_star_rule.simps)
qed

inductive post_star_rules :: "(('ctr_loc, 'noninit, 'label) state, 'label option) transition set ⇒ (('ctr_loc, 'noninit, 'label) state, 'label option) transition set ⇒ bool" where
"(p, γ) ↪ (p', pop) ⟹
(Init p, [γ], q) ∈ LTS_ε.trans_star_ε ts ⟹
(Init p', ε, q) ∉ ts ⟹
post_star_rules ts (ts ∪ {(Init p', ε, q)})"
"(p, γ) ↪ (p', swap γ') ⟹
(Init p, [γ], q) ∈ LTS_ε.trans_star_ε ts ⟹
(Init p', Some γ', q) ∉ ts ⟹
post_star_rules ts (ts ∪ {(Init p', Some γ', q)})"
"(p, γ) ↪ (p', push γ' γ'') ⟹
(Init p, [γ], q) ∈ LTS_ε.trans_star_ε ts ⟹
(Init p', Some γ', Isolated p' γ') ∉ ts ⟹
post_star_rules ts (ts ∪ {(Init p', Some γ', Isolated p' γ')})"
"(p, γ) ↪ (p', push γ' γ'') ⟹
(Init p, [γ], q) ∈ LTS_ε.trans_star_ε ts ⟹
(Isolated p' γ', Some γ'', q) ∉ ts ⟹
(Init p', Some γ', Isolated p' γ') ∈ ts ⟹
post_star_rules ts (ts ∪ {(Isolated p' γ', Some γ'', q)})"

lemma pre_star_rule_mono:
"pre_star_rule ts ts' ⟹ ts ⊂ ts'"
unfolding pre_star_rule.simps by auto

lemma post_star_rules_mono:
"post_star_rules ts ts' ⟹ ts ⊂ ts'"
proof(induction rule: post_star_rules.induct)
case (add_trans_pop p γ p' q ts)
then show ?case by auto
next
case (add_trans_swap p γ p' γ' q ts)
then show ?case by auto
next
case (add_trans_push_1 p γ p' γ' γ'' q ts)
then show ?case by auto
next
case (add_trans_push_2 p γ p' γ' γ'' q ts)
then show ?case by auto
qed

lemma pre_star_rule_card_Suc: "pre_star_rule ts ts' ⟹ card ts' = Suc (card ts)"
unfolding pre_star_rule.simps by auto

lemma post_star_rules_card_Suc: "post_star_rules ts ts' ⟹ card ts' = Suc (card ts)"
proof(induction rule: post_star_rules.induct)
case (add_trans_pop p γ p' q ts)
then show ?case by auto
next
case (add_trans_swap p γ p' γ' q ts)
then show ?case by auto
next
case (add_trans_push_1 p γ p' γ' γ'' q ts)
then show ?case by auto
next
case (add_trans_push_2 p γ p' γ' γ'' q ts)
then show ?case by auto
qed

lemma pre_star_saturation_termination:
"¬(∃tts. (∀i :: nat. pre_star_rule (tts i) (tts (Suc i))))"
using no_infinite pre_star_rule_card_Suc by blast

lemma post_star_saturation_termination:
"¬(∃tts. (∀i :: nat. post_star_rules (tts i) (tts (Suc i))))"
using no_infinite post_star_rules_card_Suc by blast

lemma pre_star_saturation_exi:
shows "∃ts'. saturation pre_star_rule ts ts'"
using pre_star_rule_card_Suc saturation_exi by blast

lemma post_star_saturation_exi:
shows "∃ts'. saturation post_star_rules ts ts'"
using post_star_rules_card_Suc saturation_exi by blast

lemma pre_star_rule_incr: "pre_star_rule A B ⟹ A ⊆ B"
proof(induction rule: pre_star_rule.inducts)
case (add_trans p γ p' w q rel)
then show ?case
by auto
qed

lemma post_star_rules_incr: "post_star_rules A B ⟹ A ⊆ B"
proof(induction rule: post_star_rules.inducts)
case (add_trans_pop p γ p' q ts)
then show ?case
by auto
next
case (add_trans_swap p γ p' γ' q ts)
then show ?case
by auto
next
case (add_trans_push_1 p γ p' γ' γ'' q ts)
then show ?case
by auto
next
case (add_trans_push_2 p γ p' γ' γ'' q ts)
then show ?case
by auto
qed

lemma saturation_rtranclp_pre_star_rule_incr: "pre_star_rule⇧*⇧* A B ⟹ A ⊆ B"
proof (induction rule: rtranclp_induct)
case base
then show ?case by auto
next
case (step y z)
then show ?case
using pre_star_rule_incr by auto
qed

lemma saturation_rtranclp_post_star_rule_incr: "post_star_rules⇧*⇧* A B ⟹ A ⊆ B"
proof (induction rule: rtranclp_induct)
case base
then show ?case by auto
next
case (step y z)
then show ?case
using post_star_rules_incr by auto
qed

lemma pre_star'_incr_trans_star:
"pre_star_rule⇧*⇧* A A' ⟹ LTS.trans_star A ⊆ LTS.trans_star A'"
using mono_def LTS_trans_star_mono saturation_rtranclp_pre_star_rule_incr by metis

lemma post_star'_incr_trans_star:
"post_star_rules⇧*⇧* A A' ⟹ LTS.trans_star A ⊆ LTS.trans_star A'"
using mono_def LTS_trans_star_mono saturation_rtranclp_post_star_rule_incr by metis

lemma post_star'_incr_trans_star_ε:
"post_star_rules⇧*⇧* A A' ⟹ LTS_ε.trans_star_ε A ⊆ LTS_ε.trans_star_ε A'"
using mono_def LTS_ε_trans_star_ε_mono saturation_rtranclp_post_star_rule_incr by metis

lemma pre_star_lim'_incr_trans_star:
"saturation pre_star_rule A A' ⟹ LTS.trans_star A ⊆ LTS.trans_star A'"

lemma post_star_lim'_incr_trans_star:
"saturation post_star_rules A A' ⟹ LTS.trans_star A ⊆ LTS.trans_star A'"

lemma post_star_lim'_incr_trans_star_ε:
"saturation post_star_rules A A' ⟹ LTS_ε.trans_star_ε A ⊆ LTS_ε.trans_star_ε A'"

subsection ‹Pre* lemmas›

lemma inits_srcs_iff_Ctr_Loc_srcs:
"inits ⊆ LTS.srcs A ⟷ (∄q γ q'. (q, γ, Init q') ∈ A)"
proof
assume "inits ⊆ LTS.srcs A"
then show "∄q γ q'. (q, γ, Init q') ∈ A"
by (simp add: Collect_mono_iff LTS.srcs_def inits_def)
next
assume "∄q γ q'. (q, γ, Init q') ∈ A"
show "inits ⊆ LTS.srcs A"
by (metis LTS.srcs_def2 inits_def ‹∄q γ q'. (q, γ, Init q') ∈ A› mem_Collect_eq
state.collapse(1) subsetI)
qed

lemma lemma_3_1:
assumes "p'w ⇒⇧* pv"
assumes "pv ∈ lang A"
assumes "saturation pre_star_rule A A'"
shows "accepts A' p'w"
using assms
proof (induct rule: converse_rtranclp_induct)
case base
define p where "p = fst pv"
define v where "v = snd pv"
from base have "∃q ∈ finals. (Init p, v, q) ∈ LTS.trans_star A'"
unfolding lang_def p_def v_def using pre_star_lim'_incr_trans_star accepts_def by fastforce
then show ?case
unfolding accepts_def p_def v_def by auto
next
case (step p'w p''u)
define p' where "p' = fst p'w"
define w  where "w = snd p'w"
define p'' where "p'' = fst p''u"
define u  where "u = snd p''u"
have p'w_def: "p'w = (p', w)"
using p'_def w_def by auto
have p''u_def: "p''u = (p'', u)"
using p''_def u_def by auto

then have "accepts A' (p'', u)"
using step by auto
then obtain q where q_p: "q ∈ finals ∧ (Init p'', u, q) ∈ LTS.trans_star A'"
unfolding accepts_def by auto
have "∃γ w1 u1. w=γ#w1 ∧ u=lbl u1@w1 ∧ (p', γ) ↪ (p'', u1)"
using p''u_def p'w_def step.hyps(1) step_relp_def2 by auto
then obtain γ w1 u1 where γ_w1_u1_p: "w=γ#w1 ∧ u=lbl u1@w1 ∧ (p', γ) ↪ (p'', u1)"
by blast

then have "∃q1. (Init p'', lbl u1, q1) ∈ LTS.trans_star A' ∧ (q1, w1, q) ∈ LTS.trans_star A'"
using q_p LTS.trans_star_split by auto

then obtain q1 where q1_p: "(Init p'', lbl u1, q1) ∈ LTS.trans_star A' ∧ (q1, w1, q) ∈ LTS.trans_star A'"
by auto

then have in_A': "(Init p', γ, q1) ∈ A'"
using γ_w1_u1_p add_trans[of p' γ p'' u1 q1 A'] saturated_def saturation_def step.prems by metis

then have "(Init p', γ#w1, q) ∈ LTS.trans_star A'"
using LTS.trans_star.trans_star_step q1_p by meson
then have t_in_A': "(Init p', w, q) ∈ LTS.trans_star A'"
using γ_w1_u1_p by blast

from q_p t_in_A' have "q ∈ finals ∧ (Init p', w, q) ∈ LTS.trans_star A'"
by auto
then show ?case
unfolding accepts_def p'w_def by auto
qed

lemma word_into_init_empty_states:
fixes A :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition set"
assumes "(p, w, ss, Init q) ∈ LTS.trans_star_states A"
assumes "inits ⊆ LTS.srcs A"
shows "w = [] ∧ p = Init q ∧ ss=[p]"
proof -
define q1 :: "('ctr_loc, 'noninit, 'label) state" where
"q1 = Init q"
have q1_path: "(p, w, ss, q1) ∈ LTS.trans_star_states A"
moreover
have "q1 ∈ inits"
ultimately
have "w = [] ∧ p = q1 ∧ ss=[p]"
proof(induction rule: LTS.trans_star_states.induct[OF q1_path])
case (1 p)
then show ?case by auto
next
case (2 p γ q' w ss q)
have "∄q γ q'. (q, γ, Init q') ∈ A"
using assms(2) unfolding inits_def LTS.srcs_def by (simp add: Collect_mono_iff)
then show ?case
using 2 assms(2) by (metis inits_def is_Init_def mem_Collect_eq)
qed
then show ?thesis
using q1_def by fastforce
qed

(* This corresponds to and slightly generalizes Schwoon's lemma 3.2(b) *)
lemma word_into_init_empty:
fixes A :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition set"
assumes "(p, w, Init q) ∈ LTS.trans_star A"
assumes "inits ⊆ LTS.srcs A"
shows "w = [] ∧ p = Init q"
using assms word_into_init_empty_states LTS.trans_star_trans_star_states by metis

lemma step_relp_append_aux:
assumes "pu ⇒⇧* p1y"
shows "(fst pu, snd pu @ v) ⇒⇧* (fst p1y, snd p1y @ v)"
using assms
proof (induction rule: rtranclp_induct)
case base
then show ?case by auto
next
case (step p'w p1y)
define p where "p = fst pu"
define u where "u = snd pu"
define p' where "p' = fst p'w"
define w where "w = snd p'w"
define p1 where "p1 = fst p1y"
define y where "y = snd p1y"
have step_1: "(p,u) ⇒⇧* (p',w)"
by (simp add: p'_def p_def step.hyps(1) u_def w_def)
have step_2: "(p',w) ⇒ (p1,y)"
by (simp add: p'_def p1_def step.hyps(2) w_def y_def)
have step_3: "(p, u @ v) ⇒⇧* (p', w @ v)"
by (simp add: p'_def p_def step.IH u_def w_def)

note step' = step_1 step_2 step_3

from step'(2) have "∃γ w' wa. w = γ # w' ∧ y = lbl wa @ w' ∧ (p', γ) ↪ (p1, wa)"
using step_relp_def2[of p' w p1 y] by auto
then obtain γ w' wa where γ_w'_wa_p: " w = γ # w' ∧ y = lbl wa @ w' ∧ (p', γ) ↪ (p1, wa)"
by metis
then have "(p, u @ v) ⇒⇧* (p1, y @ v)"
by (metis (no_types, lifting) PDS.step_relp_def2 append.assoc append_Cons rtranclp.simps step_3)
then show ?case
by (simp add: p1_def p_def u_def y_def)
qed

lemma step_relp_append:
assumes "(p, u) ⇒⇧* (p1, y)"
shows "(p, u @ v) ⇒⇧* (p1, y @ v)"
using assms step_relp_append_aux by auto

lemma step_relp_append_empty:
assumes "(p, u) ⇒⇧* (p1, [])"
shows "(p, u @ v) ⇒⇧* (p1, v)"
using step_relp_append[OF assms] by auto

lemma lemma_3_2_a':
assumes "inits ⊆ LTS.srcs A"
assumes "pre_star_rule⇧*⇧* A A'"
assumes "(Init p, w, q) ∈ LTS.trans_star A'"
shows "∃p' w'. (Init p', w', q) ∈ LTS.trans_star A ∧ (p, w) ⇒⇧* (p', w')"
using assms(2) assms(3)
proof (induction arbitrary: p q w rule: rtranclp_induct)
case base
then have "(Init p, w, q) ∈ LTS.trans_star A ∧ (p, w) ⇒⇧* (p, w)"
by auto
then show ?case
by auto
next
case (step Aiminus1 Ai)

from step(2) obtain p1 γ p2 w2 q' where p1_γ_p2_w2_q'_p:
"Ai = Aiminus1 ∪ {(Init p1, γ, q')}"
"(p1, γ) ↪ (p2, w2)"
"(Init p2, lbl w2, q') ∈ LTS.trans_star Aiminus1"
"(Init p1, γ, q') ∉ Aiminus1"
by (meson pre_star_rule.cases)

define t :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition"
where "t = (Init p1, γ, q')"

obtain ss where ss_p: "(Init p, w, ss, q) ∈ LTS.trans_star_states Ai"
using step(4) LTS.trans_star_trans_star_states by metis

define j where "j = count (transitions_of' (Init p, w, ss, q)) t"

from j_def ss_p show ?case
proof (induction j arbitrary: p q w ss)
case 0
then have "(Init p, w, q) ∈ LTS.trans_star Aiminus1"
using count_zero_remove_trans_star_states_trans_star p1_γ_p2_w2_q'_p(1) t_def by metis
then show ?case
using step.IH by metis
next
case (Suc j')
have "∃u v u_ss v_ss.
ss = u_ss@v_ss ∧ w = u@[γ]@v ∧
(Init p,u,u_ss, Init p1) ∈ LTS.trans_star_states Aiminus1 ∧
(Init p1,[γ],q') ∈ LTS.trans_star Ai ∧
(q',v,v_ss,q) ∈ LTS.trans_star_states Ai ∧
(Init p, w, ss, q) = ((Init p, u, u_ss, Init p1), γ) @@⇧γ (q', v, v_ss, q)"
using split_at_first_t[of "Init p" w ss q Ai j' "Init p1" γ q' Aiminus1]
using Suc(2,3) t_def  p1_γ_p2_w2_q'_p(1,4) t_def by auto
then obtain u v u_ss v_ss where u_v_u_ss_v_ss_p:
"ss = u_ss@v_ss ∧ w = u@[γ]@v"
"(Init p,u,u_ss, Init p1) ∈ LTS.trans_star_states Aiminus1"
"(Init p1,[γ],q') ∈ LTS.trans_star Ai"
"(q',v,v_ss,q) ∈ LTS.trans_star_states Ai"
"(Init p, w, ss, q) = ((Init p, u, u_ss, Init p1), γ) @@⇧γ (q', v, v_ss, q)"
by blast
from this(2) have "∃p'' w''. (Init p'', w'', Init p1) ∈ LTS.trans_star A ∧ (p, u) ⇒⇧* (p'', w'')"
using Suc(1)[of p u _ "Init p1"] step.IH step.prems(1)
by (meson LTS.trans_star_states_trans_star LTS.trans_star_trans_star_states)
from this this(1) have VIII: "(p, u) ⇒⇧* (p1, [])"
using word_into_init_empty assms(1) by blast

note IX = p1_γ_p2_w2_q'_p(2)
note III = p1_γ_p2_w2_q'_p(3)
from III have III_2: "∃w2_ss. (Init p2, lbl w2, w2_ss, q') ∈ LTS.trans_star_states Aiminus1"
using LTS.trans_star_trans_star_states[of "Init p2" "lbl w2" q' Aiminus1] by auto
then obtain w2_ss where III_2: "(Init p2, lbl w2, w2_ss, q') ∈ LTS.trans_star_states Aiminus1"
by blast

from III have V:
"(Init p2, lbl w2, w2_ss, q') ∈ LTS.trans_star_states Aiminus1"
"(q', v, v_ss, q) ∈ LTS.trans_star_states Ai"
using III_2 ‹(q', v, v_ss, q) ∈ LTS.trans_star_states Ai› by auto

define w2v where "w2v = lbl w2 @ v"
define w2v_ss where "w2v_ss = w2_ss @ tl v_ss"

from V(1) have "(Init p2, lbl w2, w2_ss, q') ∈ LTS.trans_star_states Ai"
using trans_star_states_mono p1_γ_p2_w2_q'_p(1) using Un_iff subsetI by (metis (no_types))
then have V_merged: "(Init p2, w2v, w2v_ss, q) ∈ LTS.trans_star_states Ai"
using V(2) unfolding w2v_def w2v_ss_def by (meson LTS.trans_star_states_append)

have j'_count: "j' = count (transitions_of' (Init p2, w2v, w2v_ss, q)) t"
proof -
define countts where
"countts == λx. count (transitions_of' x) t"

have "countts (Init p, w, ss, q) = Suc j' "
using Suc.prems(1) countts_def by force
moreover
have "countts (Init p, u, u_ss, Init p1) = 0"
using LTS.avoid_count_zero countts_def p1_γ_p2_w2_q'_p(4) t_def u_v_u_ss_v_ss_p(2)
by fastforce
moreover
from u_v_u_ss_v_ss_p(5) have "countts (Init p, w, ss, q) = countts (Init p, u, u_ss, Init p1) + 1 + countts (q', v, v_ss, q)"
using count_combine_trans_star_states countts_def t_def u_v_u_ss_v_ss_p(2)
u_v_u_ss_v_ss_p(4) by fastforce
ultimately
have "Suc j' = 0 + 1 + countts (q', v, v_ss, q)"
by auto
then have "j' = countts (q', v, v_ss, q)"
by auto
moreover
have "countts (Init p2, lbl w2, w2_ss, q') = 0"
using III_2 LTS.avoid_count_zero countts_def p1_γ_p2_w2_q'_p(4) t_def by fastforce
moreover
have "(Init p2, w2v, w2v_ss, q) = (Init p2, lbl w2, w2_ss, q') @@´ (q', v, v_ss, q)"
using w2v_def w2v_ss_def by auto
then have "countts (Init p2, w2v, w2v_ss, q) = countts (Init p2, lbl w2, w2_ss, q') + countts (q', v, v_ss, q)"
using ‹(Init p2, lbl w2, w2_ss, q') ∈ LTS.trans_star_states Ai›
count_append_trans_star_states countts_def t_def u_v_u_ss_v_ss_p(4) by fastforce
ultimately
show ?thesis
qed

have "∃p' w'. (Init p', w', q) ∈ LTS.trans_star A ∧ (p2, w2v) ⇒⇧* (p', w')"
using Suc(1) using j'_count V_merged by auto
then obtain p' w' where p'_w'_p: "(Init p', w', q) ∈ LTS.trans_star A" "(p2, w2v) ⇒⇧* (p', w')"
by blast

note X = p'_w'_p(2)

have "(p,w) = (p,u@[γ]@v)"
using ‹ss = u_ss @ v_ss ∧ w = u @ [γ] @ v› by blast

have "(p,u@[γ]@v) ⇒⇧* (p1,γ#v)"
using VIII step_relp_append_empty by auto

from X have "(p1,γ#v) ⇒ (p2, w2v)"
by (metis IX LTS.step_relp_def transition_rel.intros w2v_def)

from X have
"(p2, w2v) ⇒⇧* (p', w')"
by simp

have "(p, w) ⇒⇧* (p', w')"
using X ‹(p, u @ [γ] @ v) ⇒⇧* (p1, γ # v)› ‹(p, w) = (p, u @ [γ] @ v)› ‹(p1, γ # v) ⇒ (p2, w2v)› by auto

then have "(Init p', w', q) ∈ LTS.trans_star A ∧ (p, w) ⇒⇧* (p', w')"
using p'_w'_p(1) by auto
then show ?case
by metis
qed
qed

lemma lemma_3_2_a:
assumes "inits ⊆ LTS.srcs A"
assumes "saturation pre_star_rule A A'"
assumes "(Init p, w, q) ∈ LTS.trans_star A'"
shows "∃p' w'. (Init p', w', q) ∈ LTS.trans_star A ∧ (p, w) ⇒⇧* (p', w')"
using assms lemma_3_2_a' saturation_def by metis

― ‹Corresponds to one direction of Schwoon's theorem 3.2›
theorem pre_star_rule_subset_pre_star_lang:
assumes "inits ⊆ LTS.srcs A"
assumes "pre_star_rule⇧*⇧* A A'"
shows "{c. accepts A' c} ⊆ pre_star (lang A)"
proof
fix c :: "'ctr_loc × 'label list"
assume c_a: "c ∈ {w. accepts A' w}"
define p where "p = fst c"
define w where "w = snd c"
from p_def w_def c_a have "accepts A' (p,w)"
by auto
then have "∃q ∈ finals. (Init p, w, q) ∈ LTS.trans_star A'"
unfolding accepts_def by auto
then obtain q where q_p: "q ∈ finals" "(Init p, w, q) ∈ LTS.trans_star A'"
by auto
then have "∃p' w'. (p,w) ⇒⇧* (p',w') ∧ (Init p', w', q) ∈ LTS.trans_star A"
using lemma_3_2_a' assms(1) assms(2) by metis
then obtain p' w' where p'_w'_p: "(p,w) ⇒⇧* (p',w')" "(Init p', w', q) ∈ LTS.trans_star A"
by auto
then have "(p', w') ∈ lang A"
unfolding lang_def unfolding accepts_def using q_p(1) by auto
then have "(p,w) ∈ pre_star (lang A)"
unfolding pre_star_def using p'_w'_p(1) by auto
then show "c ∈ pre_star (lang A)"
unfolding p_def w_def by auto
qed

― ‹Corresponds to Schwoon's theorem 3.2›
theorem pre_star_rule_accepts_correct:
assumes "inits ⊆ LTS.srcs A"
assumes "saturation pre_star_rule A A'"
shows "{c. accepts A' c} = pre_star (lang A)"
proof (rule; rule)
fix c :: "'ctr_loc × 'label list"
define p where "p = fst c"
define w where "w = snd c"
assume "c ∈ pre_star (lang A)"
then have "(p,w) ∈ pre_star (lang A)"
unfolding p_def w_def by auto
then have "∃p' w'. (p',w') ∈ lang A ∧ (p,w) ⇒⇧* (p',w')"
unfolding pre_star_def by force
then obtain p' w' where "(p',w') ∈ lang A ∧ (p,w) ⇒⇧* (p',w')"
by auto
then have "∃q ∈ finals. (Init p, w, q) ∈ LTS.trans_star A'"
using lemma_3_1 assms(2) unfolding accepts_def by force
then have "accepts A' (p,w)"
unfolding accepts_def by auto
then show "c ∈ {c. accepts A' c}"
using p_def w_def by auto
next
fix c :: "'ctr_loc × 'label list"
assume "c ∈ {w. accepts A' w}"
then show "c ∈ pre_star (lang A)"
using pre_star_rule_subset_pre_star_lang assms unfolding saturation_def by auto
qed

― ‹Corresponds to Schwoon's theorem 3.2›
theorem pre_star_rule_correct:
assumes "inits ⊆ LTS.srcs A"
assumes "saturation pre_star_rule A A'"
shows "lang A' = pre_star (lang A)"
using assms(1) assms(2) lang_def pre_star_rule_accepts_correct by auto

theorem pre_star_exec_accepts_correct:
assumes "inits ⊆ LTS.srcs A"
shows "{c. accepts (pre_star_exec A) c} = pre_star (lang A)"
using pre_star_rule_accepts_correct[of A "pre_star_exec A"] saturation_pre_star_exec[of A]
assms by auto

theorem pre_star_exec_lang_correct:
assumes "inits ⊆ LTS.srcs A"
shows "lang (pre_star_exec A) = pre_star (lang A)"
using pre_star_rule_correct[of A "pre_star_exec A"] saturation_pre_star_exec[of A] assms by auto

theorem pre_star_exec_check_accepts_correct:
assumes "pre_star_exec_check A ≠ None"
shows "{c. accepts (the (pre_star_exec_check A)) c} = pre_star (lang A)"
using pre_star_exec_accepts_correct assms unfolding pre_star_exec_check_def pre_star_exec_def
by (auto split: if_splits)

theorem pre_star_exec_check_correct:
assumes "pre_star_exec_check A ≠ None"
shows "lang (the (pre_star_exec_check A)) = pre_star (lang A)"
using pre_star_exec_check_accepts_correct assms unfolding lang_def by auto

theorem accept_pre_star_exec_correct_True:
assumes "inits ⊆ LTS.srcs A"
assumes "accepts (pre_star_exec A) c"
shows "c ∈ pre_star (lang A)"
using pre_star_exec_accepts_correct assms(1) assms(2) by blast

theorem accept_pre_star_exec_correct_False:
assumes "inits ⊆ LTS.srcs A"
assumes "¬accepts (pre_star_exec A) c"
shows "c ∉ pre_star (lang A)"
using pre_star_exec_accepts_correct assms(1) assms(2) by blast

theorem accept_pre_star_exec_correct_Some_True:
assumes "accept_pre_star_exec_check A c = Some True"
shows "c ∈ pre_star (lang A)"
proof -
have "inits ⊆ LTS.srcs A"
using assms unfolding accept_pre_star_exec_check_def
by (auto split: if_splits)
moreover
have "accepts (pre_star_exec A) c"
using assms
using accept_pre_star_exec_check_def calculation by auto
ultimately
show "c ∈ pre_star (lang A)"
using accept_pre_star_exec_correct_True by auto
qed

theorem accept_pre_star_exec_correct_Some_False:
assumes "accept_pre_star_exec_check A c = Some False"
shows "c ∉ pre_star (lang A)"
proof -
have "inits ⊆ LTS.srcs A"
using assms unfolding accept_pre_star_exec_check_def
by (auto split: if_splits)
moreover
have "¬accepts (pre_star_exec A) c"
using assms
using accept_pre_star_exec_check_def calculation by auto
ultimately
show "c ∉ pre_star (lang A)"
using accept_pre_star_exec_correct_False by auto
qed

theorem accept_pre_star_exec_correct_None:
assumes "accept_pre_star_exec_check A c = None"
shows "¬inits ⊆ LTS.srcs A"
using assms unfolding accept_pre_star_exec_check_def by auto

subsection ‹Post* lemmas›

lemma lemma_3_3':
assumes "pv ⇒⇧* p'w"
and "(fst pv, snd pv) ∈ lang_ε A"
and "saturation post_star_rules A A'"
shows "accepts_ε A' (fst p'w, snd p'w)"
using assms
proof (induct arbitrary: pv rule: rtranclp_induct)
case base
show ?case
using assms post_star_lim'_incr_trans_star_ε
by (auto simp: lang_ε_def accepts_ε_def)
next
case (step p''u p'w)
define p' where "p' = fst p'w"
define w  where "w = snd p'w"
define p'' where "p'' = fst p''u"
define u  where "u = snd p''u"
have p'w_def: "p'w = (p', w)"
using p'_def w_def by auto
have p''u_def: "p''u = (p'', u)"
using p''_def u_def by auto

then have "accepts_ε A' (p'', u)"
using assms(2) p''_def step.hyps(3) step.prems(2) u_def by metis
then have "∃q. q ∈ finals ∧ (Init p'', u, q) ∈ LTS_ε.trans_star_ε A'"
by (auto simp: accepts_ε_def)
then obtain q where q_p: "q ∈ finals ∧ (Init p'', u, q) ∈ LTS_ε.trans_star_ε A'"
by metis
then have "∃u_ε. q ∈ finals ∧ LTS_ε.ε_exp u_ε u ∧ (Init p'', u_ε, q) ∈ LTS.trans_star A'"
using LTS_ε.trans_star_ε_iff_ε_exp_trans_star[of "Init p''" u q A'] by auto
then obtain u_ε where II: "q ∈ finals" "LTS_ε.ε_exp u_ε u" "(Init p'', u_ε, q) ∈ LTS.trans_star A'"
by blast
have "∃γ u1 w1. u=γ#u1 ∧ w=lbl w1@u1 ∧ (p'', γ) ↪ (p', w1)"
using p''u_def p'w_def step.hyps(2) step_relp_def2 by auto
then obtain γ u1 w1 where III: "u=γ#u1" "w=lbl w1@u1" "(p'', γ) ↪ (p', w1)"
by blast

have p'_inits: "Init p' ∈ inits"
unfolding inits_def by auto
have p''_inits: "Init p'' ∈ inits"
unfolding inits_def by auto

have "∃γ_ε u1_ε. LTS_ε.ε_exp γ_ε [γ] ∧ LTS_ε.ε_exp u1_ε u1 ∧ (Init p'', γ_ε@u1_ε, q) ∈ LTS.trans_star A'"
proof -
have "∃γ_ε u1_ε. LTS_ε.ε_exp γ_ε [γ] ∧ LTS_ε.ε_exp u1_ε u1 ∧ u_ε = γ_ε @ u1_ε"
using LTS_ε.ε_exp_split'[of u_ε γ u1] II(2) III(1) by auto
then obtain γ_ε u1_ε where "LTS_ε.ε_exp γ_ε [γ] ∧ LTS_ε.ε_exp u1_ε u1 ∧ u_ε = γ_ε @ u1_ε"
by auto
then have "(Init p'', γ_ε@u1_ε , q) ∈ LTS.trans_star A'"
using II(3) by auto
then show ?thesis
using ‹LTS_ε.ε_exp γ_ε [γ] ∧ LTS_ε.ε_exp u1_ε u1 ∧ u_ε = γ_ε @ u1_ε› by blast
qed
then obtain γ_ε u1_ε where
iii: "LTS_ε.ε_exp γ_ε [γ]" and
iv: "LTS_ε.ε_exp u1_ε u1" "(Init p'', γ_ε@u1_ε, q) ∈ LTS.trans_star A'"
by blast
then have VI: "∃q1. (Init p'', γ_ε, q1) ∈ LTS.trans_star A' ∧ (q1, u1_ε, q) ∈ LTS.trans_star A'"
then obtain q1 where VI: "(Init p'', γ_ε, q1) ∈ LTS.trans_star A'" "(q1, u1_ε, q) ∈ LTS.trans_star A'"
by blast

then have VI_2: "(Init p'', [γ], q1) ∈ LTS_ε.trans_star_ε A'" "(q1, u1, q) ∈ LTS_ε.trans_star_ε A'"
by (meson LTS_ε.trans_star_ε_iff_ε_exp_trans_star iii VI(2) iv(1))+

show ?case
proof (cases w1)
case pop
then have r: "(p'', γ) ↪ (p', pop)"
using III(3) by blast
then have "(Init p', ε, q1) ∈ A'"
using VI_2(1) add_trans_pop assms saturated_def saturation_def p'_inits by metis
then have "(Init p', w, q) ∈ LTS_ε.trans_star_ε A'"
using III(2) VI_2(2) pop LTS_ε.trans_star_ε.trans_star_ε_step_ε by fastforce
then have "accepts_ε A' (p', w)"
unfolding accepts_ε_def using II(1) by blast
then show ?thesis
using p'_def w_def by force
next
case (swap γ')
then have r: "(p'', γ) ↪ (p', swap γ')"
using III(3) by blast
then have "(Init p', Some γ', q1) ∈ A'"
by (metis VI_2(1) add_trans_swap assms(3) saturated_def saturation_def)
have "(Init p', w, q) ∈ LTS_ε.trans_star_ε A'"
using III(2) LTS_ε.trans_star_ε.trans_star_ε_step_γ VI_2(2) append_Cons append_self_conv2
lbl.simps(3) swap ‹(Init p', Some γ', q1) ∈ A'› by fastforce
then have "accepts_ε A' (p', w)"
unfolding accepts_ε_def
using II(1) by blast
then show ?thesis
using p'_def w_def by force
next
case (push γ' γ'')
then have r: "(p'', γ) ↪ (p', push γ' γ'')"
using III(3) by blast
from this VI_2 iii post_star_rules.intros(3)[OF this, of q1 A', OF VI_2(1)]
have "(Init p', Some γ', Isolated p' γ') ∈ A'"
using assms(3) by (meson saturated_def saturation_def)
from this r VI_2 iii post_star_rules.intros(4)[OF r, of q1 A', OF VI_2(1)]
have "(Isolated p' γ', Some γ'', q1) ∈ A'"
using assms(3) using saturated_def saturation_def by metis
have "(Init p', [γ'], Isolated p' γ') ∈ LTS_ε.trans_star_ε A' ∧
(Isolated p' γ', [γ''], q1) ∈ LTS_ε.trans_star_ε A' ∧
(q1, u1, q) ∈ LTS_ε.trans_star_ε A'"
by (metis LTS_ε.trans_star_ε.simps VI_2(2) ‹(Init p', Some γ', Isolated p' γ') ∈ A'›
‹(Isolated p' γ', Some γ'', q1) ∈ A'›)
have "(Init p', w, q) ∈ LTS_ε.trans_star_ε A'"
using III(2) VI_2(2) ‹(Init p', Some γ', Isolated p' γ') ∈ A'›
‹(Isolated p' γ', Some γ'', q1) ∈ A'› push LTS_ε.append_edge_edge_trans_star_ε by auto
then have "accepts_ε A' (p', w)"
unfolding accepts_ε_def
using II(1) by blast
then show ?thesis
using p'_def w_def by force

qed
qed

lemma lemma_3_3:
assumes "(p,v) ⇒⇧* (p',w)"
and "(p, v) ∈ lang_ε A"
and "saturation post_star_rules A A'"
shows "accepts_ε A' (p', w)"
using assms lemma_3_3' by force

lemma init_only_hd:
assumes "(ss, w) ∈ LTS.path_with_word A"
assumes "inits ⊆ LTS.srcs A"
assumes "count (transitions_of (ss, w)) t > 0"
assumes "t = (Init p1, γ, q1)"
shows "hd (transition_list (ss, w)) = t ∧ count (transitions_of (ss, w)) t = 1"
using assms LTS.source_only_hd by (metis LTS.srcs_def2 inits_srcs_iff_Ctr_Loc_srcs)

lemma no_edge_to_Ctr_Loc_avoid_Ctr_Loc:
assumes "(p, w, qq) ∈ LTS.trans_star Aiminus1"
assumes "w ≠ []"
assumes "inits ⊆ LTS.srcs Aiminus1"
shows "qq ∉ inits"
using assms LTS.no_end_in_source by (metis subset_iff)

lemma no_edge_to_Ctr_Loc_avoid_Ctr_Loc_ε:
assumes "(p, [γ], qq) ∈ LTS_ε.trans_star_ε Aiminus1"
assumes "inits ⊆ LTS.srcs Aiminus1"
shows "qq ∉ inits"
using assms LTS_ε.no_edge_to_source_ε by (metis subset_iff)

lemma no_edge_to_Ctr_Loc_post_star_rules':
assumes "post_star_rules⇧*⇧* A Ai"
assumes "∄q γ q'. (q, γ, Init q') ∈ A"
shows "∄q γ q'. (q, γ, Init q') ∈ Ai"
using assms
proof (induction rule: rtranclp_induct)
case base
then show ?case by auto
next
case (step Aiminus1 Ai)
then have ind: "∄q γ q'. (q, γ, Init q') ∈ Aiminus1"
by auto
from step(2) show ?case
proof (cases rule: post_star_rules.cases)
case (add_trans_pop p γ p' q)
have "q ∉ inits"
using ind no_edge_to_Ctr_Loc_avoid_Ctr_Loc_ε inits_srcs_iff_Ctr_Loc_srcs
then have "∄qq. q = Init qq"
then show ?thesis
next
case (add_trans_swap p γ p' γ' q)
have "q ∉ inits"
by metis
then have "∄qq. q = Init qq"
then show ?thesis
next
case (add_trans_push_1 p γ p' γ' γ'' q)
have "q ∉ inits"
by metis
then have "∄qq. q = Init qq"
then show ?thesis
next
case (add_trans_push_2 p γ p' γ' γ'' q)
have "q ∉ inits"
by metis
then have "∄qq. q = Init qq"
then show ?thesis
qed
qed

lemma no_edge_to_Ctr_Loc_post_star_rules:
assumes "post_star_rules⇧*⇧* A Ai"
assumes "inits ⊆ LTS.srcs A"
shows "inits ⊆ LTS.srcs Ai"
using assms no_edge_to_Ctr_Loc_post_star_rules' inits_srcs_iff_Ctr_Loc_srcs by metis

lemma source_and_sink_isolated:
assumes "N ⊆ LTS.srcs A"
assumes "N ⊆ LTS.sinks A"
shows "∀p γ q. (p, γ, q) ∈ A ⟶ p ∉ N ∧ q ∉ N"
by (metis LTS.srcs_def2 LTS.sinks_def2 assms(1) assms(2) in_mono)

lemma post_star_rules_Isolated_source_invariant':
assumes "post_star_rules⇧*⇧* A A'"
assumes "isols ⊆ LTS.isolated A"
assumes "(Init p', Some γ', Isolated p' γ') ∉ A'"
shows "∄p γ. (p, γ, Isolated p' γ') ∈ A'"
using assms
proof (induction rule: rtranclp_induct)
case base
then show ?case
unfolding isols_def is_Isolated_def using LTS.isolated_no_edges by fastforce
next
case (step Aiminus1 Ai)
from step(2) show ?case
proof (cases rule: post_star_rules.cases)
case (add_trans_pop p''' γ'' p'' q)
then have "(Init p', Some γ', Isolated p' γ') ∉ Ai"
using step.prems(2) by blast
then have nin: "∄p γ. (p, γ, Isolated p' γ') ∈ Aiminus1"
using local.add_trans_pop(1) step.IH step.prems(1,2) by fastforce
then have "Isolated p' γ' ≠ q"
then have "∄p γ. (p, γ, Isolated p' γ') = (Init p'', ε, q)"
by auto
then show ?thesis
next
case (add_trans_swap p'''' γ'' p'' γ''' q)
then have "(Init p', Some γ', Isolated p' γ') ∉ Ai"
using step.prems(2) by blast
then have nin: "∄p γ. (p, γ, Isolated p' γ') ∈ Aiminus1"
using local.add_trans_swap(1) step.IH step.prems(1,2) by fastforce
then have "Isolated p' γ' ≠ q"
using LTS.srcs_def2
then have "∄p γ. (p, γ, Isolated p' γ') = (Init p'', Some γ''', q)"
by auto
then show ?thesis
next
case (add_trans_push_1 p'''' γ'' p'' γ''' γ''''' q)
then have "(Init p', Some γ', Isolated p' γ') ∉ Ai"
using step.prems(2) by blast
then show ?thesis
using add_trans_push_1(1) Un_iff state.inject(2) prod.inject singleton_iff step.IH
step.prems(1,2) by blast
next
case (add_trans_push_2 p'''' γ'' p'' γ''' γ'''' q)
have "(Init p', Some γ', Isolated p' γ') ∉ Ai"
using step.prems(2) .
then have nin: "∄p γ. (p, γ, Isolated p' γ') ∈ Aiminus1"
using local.add_trans_push_2(1) step.IH step.prems(1) by fastforce
then have "Isolated p' γ' ≠ q"
by (metis state.disc(1,3) LTS_ε.trans_star_not_to_source_ε)
then have "∄p γ. (p, γ, Isolated p' γ') = (Init p'', ε, q)"
by auto
then show ?thesis
qed
qed

lemma post_star_rules_Isolated_source_invariant:
assumes "post_star_rules⇧*⇧* A A'"
assumes "isols ⊆ LTS.isolated A"
assumes "(Init p', Some γ', Isolated p' γ') ∉ A'"
shows "Isolated p' γ' ∈ LTS.srcs A'"
by (meson LTS.srcs_def2 assms(1) assms(2) assms(3) post_star_rules_Isolated_source_invariant')

lemma post_star_rules_Isolated_sink_invariant':
assumes "post_star_rules⇧*⇧* A A'"
assumes "isols ⊆ LTS.isolated A"
assumes "(Init p', Some γ', Isolated p' γ') ∉ A'"
shows "∄p γ. (Isolated p' γ', γ, p) ∈ A'"
using assms
proof (induction rule: rtranclp_induct)
case base
then show ?case
unfolding isols_def is_Isolated_def
using LTS.isolated_no_edges by fastforce
next
case (step Aiminus1 Ai)
from step(2) show ?case
proof (cases rule: post_star_rules.cases)
case (add_trans_pop p''' γ'' p'' q)
then have "(Init p', Some γ', Isolated p' γ') ∉ Ai"
using step.prems(2) by blast
then have nin: "∄p γ. (Isolated p' γ', γ, p) ∈ Aiminus1"
using local.add_trans_pop(1) step.IH step.prems(1,2) by fastforce
then have "Isolated p' γ' ≠ q"
LTS_ε.trans_star_not_to_source_ε[of "Init p'''" "[γ'']" q Aiminus1 "Isolated p' γ'"]
UnI1 local.add_trans_pop(3) by (metis (full_types) state.distinct(3))
then have "∄p γ. (p, γ, Isolated p' γ') = (Init p'', ε, q)"
by auto
then show ?thesis
next
case (add_trans_swap p'''' γ'' p'' γ''' q)
then have "(Init p', Some γ', Isolated p' γ') ∉ Ai"
using step.prems(2) by blast
then have nin: "∄p γ. (Isolated p' γ', γ, p) ∈ Aiminus1"
using local.add_trans_swap(1) step.IH step.prems(1,2) by fastforce
then have "Isolated p' γ' ≠ q"
using LTS_ε.trans_star_not_to_source_ε[of "Init p''''" "[γ'']" q Aiminus1]
local.add_trans_swap(3) post_star_rules_Isolated_source_invariant[of _ Aiminus1 p' γ'] UnCI
local.add_trans_swap(1) step.hyps(1) step.prems(1,2) state.simps(7) by metis
then have "∄p γ. (p, γ, Isolated p' γ') = (Init p'', Some γ''', q)"
by auto
then show ?thesis
next
case (add_trans_push_1 p'''' γ'' p'' γ''' γ''''' q)
then have "(Init p', Some γ', Isolated p' γ') ∉ Ai"
using step.prems(2) by blast
then show ?thesis
using add_trans_push_1(1) Un_iff state.inject prod.inject singleton_iff step.IH
step.prems(1,2) by blast
next
case (add_trans_push_2 p'''' γ'' p'' γ''' γ'''' q)
have "(Init p', Some γ', Isolated p' γ') ∉ Ai"
using step.prems(2) by blast
then have nin: "∄p γ. (Isolated p' γ', γ, p) ∈ Aiminus1"
using local.add_trans_push_2(1) step.IH step.prems(1,2) by fastforce
then have "Isolated p' γ' ≠ q"
using state.disc(3)
LTS_ε.trans_star_not_to_source_ε[of "Init p''''" "[γ'']" q Aiminus1 "Isolated p' γ'"]
using post_star_rules_Isolated_source_invariant[of _ Aiminus1 p' γ'] UnCI
local.add_trans_push_2(1) step.hyps(1) step.prems(1,2) state.disc(1) by metis
then have "∄p γ. (Isolated p' γ', γ, p) = (Init p'', ε, q)"
by auto
then show ?thesis
qed
qed

lemma post_star_rules_Isolated_sink_invariant:
assumes "post_star_rules⇧*⇧* A A'"
assumes "isols ⊆ LTS.isolated A"
assumes "(Init p', Some γ', Isolated p' γ') ∉ A'"
shows "Isolated p' γ' ∈ LTS.sinks A'"
by (meson LTS.sinks_def2 assms(1,2,3) post_star_rules_Isolated_sink_invariant')

― ‹Corresponds to Schwoon's lemma 3.4›
lemma rtranclp_post_star_rules_constains_successors_states:
assumes "post_star_rules⇧*⇧* A A'"
assumes "inits ⊆ LTS.srcs A"
assumes "isols ⊆ LTS.isolated A"
assumes "(Init p, w, ss, q) ∈ LTS.trans_star_states A'"
shows "(¬is_Isolated q ⟶ (∃p' w'. (Init p', w', q) ∈ LTS_ε.trans_star_ε A ∧ (p',w') ⇒⇧* (p, LTS_ε.remove_ε w))) ∧
(is_Isolated q ⟶ (the_Ctr_Loc q, [the_Label q]) ⇒⇧* (p, LTS_ε.remove_ε w))"
using assms
proof (induction arbitrary: p q w ss rule: rtranclp_induct)
case base
{
assume ctr_loc: "is_Init q ∨ is_Noninit q"
then have "(Init p, LTS_ε.remove_ε w, q) ∈ LTS_ε.trans_star_ε A"
using base LTS_ε.trans_star_states_trans_star_ε by metis
then have "∃p' w'. (p', w', q) ∈ LTS_ε.trans_star_ε A"
by auto
then have ?case
using ctr_loc ‹(Init p, LTS_ε.remove_ε w, q) ∈ LTS_ε.trans_star_ε A› by blast
}
moreover
{
assume "is_Isolated q"
then have ?case
proof (cases w)
case Nil
then have False using base
using LTS.trans_star_empty LTS.trans_star_states_trans_star ‹is_Isolated q›
by (metis state.disc(7))
then show ?thesis
by metis
next
case (Cons γ w_rest)
then have "(Init p, γ#w_rest, ss, q) ∈ LTS.trans_star_states A"
using base Cons by blast
then have "∃s γ'. (s, γ', q) ∈ A"
using LTS.trans_star_states_transition_relation by metis
then have False
using ‹is_Isolated q› isols_def base.prems(2) LTS.isolated_no_edges
by (metis mem_Collect_eq subset_eq)
then show ?thesis
by auto
qed
}
ultimately
show ?case
by (meson state.exhaust_disc)
next
case (step Aiminus1 Ai)
from step(2) have "∃p1 γ p2 w2 q1. Ai = Aiminus1 ∪ {(p1, γ, q1)} ∧ (p1, γ, q1) ∉ Aiminus1"
by (cases rule: post_star_rules.cases) auto
then obtain p1 γ q1 where p1_γ_p2_w2_q'_p:
"Ai = Aiminus1 ∪ {(p1, γ, q1)}"
"(p1, γ, q1) ∉ Aiminus1"
by auto

define t where "t = (p1, γ, q1)"
define j where "j = count (transitions_of' (Init p, w, ss, q)) t"

note ss_p = step(6)

from j_def ss_p show ?case
proof (induction j arbitrary: p q w ss)
case 0
then have "(Init p, w, ss, q) ∈ LTS.trans_star_states Aiminus1"
using count_zero_remove_path_with_word_trans_star_states p1_γ_p2_w2_q'_p(1) t_def
by metis
then show ?case
using step by auto
next
case (Suc j)
from step(2) show ?case
proof (cases rule: post_star_rules.cases)
case (add_trans_pop p2 γ2 p1 q1) (* Note: p1 shadows p1 from above. q1 shadows q1 from above. *)
have t_def: "t = (Init p1, ε, q1)"
have init_Ai: "inits ⊆ LTS.srcs Ai"
using step(1,2) step(4)
using no_edge_to_Ctr_Loc_post_star_rules
using r_into_rtranclp by (metis)
have t_hd_once: "hd (transition_list (ss, w)) = t ∧ count (transitions_of (ss, w)) t = 1"
proof -
have "(ss, w) ∈ LTS.path_with_word Ai"
using Suc(3) LTS.trans_star_states_path_with_word by metis
moreover
have "inits ⊆ LTS.srcs Ai"
using init_Ai by auto
moreover
have "0 < count (transitions_of (ss, w)) t"
by (metis Suc.prems(1) transitions_of'.simps zero_less_Suc)
moreover
have "t = (Init p1, ε, q1)"
using t_def by auto
moreover
have "Init p1 ∈ inits"
ultimately
show "hd (transition_list (ss, w)) = t ∧ count (transitions_of (ss, w)) t = 1"
using init_only_hd[of ss w Ai t p1 ε q1] by auto
qed

have "transition_list (ss, w) ≠ []"
by (metis LTS.trans_star_states_path_with_word LTS.path_with_word.simps Suc.prems(1)
Suc.prems(2) count_empty less_not_refl2 list.distinct(1) transition_list.simps(1)
transitions_of'.simps transitions_of.simps(2) zero_less_Suc)
then have ss_w_split: "([Init p1,q1], [ε]) @´ (tl ss,  tl w) = (ss, w)"
using t_hd_once t_def hd_transition_list_append_path_with_word by metis
then have ss_w_split': "(Init p1, [ε], [Init p1,q1], q1) @@´ (q1, tl w, tl ss, q) = (Init p1, w, ss, q)"
by auto
have VII: "p = p1"
proof -
have "(Init p, w, ss, q) ∈ LTS.trans_star_states Ai"
using Suc.prems(2) by blast
moreover
have "t = hd (transition_list' (Init p, w, ss, q))"
using ‹hd (transition_list (ss, w)) = t ∧ count (transitions_of (ss, w)) t = 1›
by fastforce
moreover
have "transition_list' (Init p, w, ss, q) ≠ []"
by (simp add: ‹transition_list (ss, w) ≠ []›)
moreover
have "t = (Init p1, ε, q1)"
using t_def by auto
ultimately
show "p = p1"
using LTS.hd_is_hd by fastforce
qed
have "j=0"
using Suc(2) ‹hd (transition_list (ss, w)) = t ∧ count (transitions_of (ss, w)) t = 1›
by force
have "(Init p1, [ε], [Init p1, q1], q1) ∈ LTS.trans_star_states Ai"
proof -
have "(Init p1, ε, q1) ∈ Ai"
moreover
have "(Init p1, ε, q1) ∉ Aiminus1"
ultimately
show "(Init p1, [ε], [Init p1, q1], q1) ∈ LTS.trans_star_states Ai"
by (meson LTS.trans_star_states.trans_star_states_refl
LTS.trans_star_states.trans_star_states_step)
qed
have "(q1, tl w, tl ss, q) ∈ LTS.trans_star_states Aiminus1"
proof -
from Suc(3) have "(ss, w) ∈ LTS.path_with_word Ai"
by (meson LTS.trans_star_states_path_with_word)
then have tl_ss_w_Ai: "(tl ss, tl w) ∈ LTS.path_with_word Ai"
by (metis LTS.path_with_word.simps ‹transition_list (ss, w) ≠ []› list.sel(3)
transition_list.simps(2))
from t_hd_once have zero_p1_ε_q1: "0 = count (transitions_of (tl ss, tl w)) (Init p1, ε, q1)"
using count_append_path_with_word_γ[of "[hd ss]" "[]" "tl ss" "hd w" "tl w" "Init p1" ε q1, simplified]
‹(Init p1, [ε], [Init p1, q1], q1) ∈ LTS.trans_star_states Ai›
‹transition_list (ss, w) ≠ []› Suc.prems(2) VII
LTS.transition_list_Cons[of "Init p" w ss q Ai ε q1] by (auto simp: t_def)
have Ai_Aiminus1: "Ai = Aiminus1 ∪ {(Init p1, ε, q1)}"
from t_hd_once tl_ss_w_Ai zero_p1_ε_q1 Ai_Aiminus1
count_zero_remove_path_with_word[OF tl_ss_w_Ai, of "Init p1" ε q1 Aiminus1]
have "(tl ss, tl w) ∈ LTS.path_with_word Aiminus1"
by auto
moreover
have "hd (tl ss) = q1"
using Suc.prems(2) VII ‹transition_list (ss, w) ≠ []› t_def
LTS.transition_list_Cons t_hd_once by fastforce
moreover
have "last ss = q"
by (metis LTS.trans_star_states_last Suc.prems(2))
ultimately
show "(q1, tl w, tl ss, q) ∈ LTS.trans_star_states Aiminus1"
by (metis (no_types, lifting) LTS.trans_star_states_path_with_word
LTS.path_with_word_trans_star_states LTS.path_with_word_not_empty Suc.prems(2)
last_ConsR list.collaps```