Session VYDRA_MDL

Theory Timestamp

theory Timestamp
  imports "HOL-Library.Extended_Nat" "HOL-Library.Extended_Real"
begin

class timestamp = comm_monoid_add + semilattice_sup +
  fixes tfin :: "'a set" and ι :: "nat ⇒ 'a"
  assumes ι_mono: "⋀i j. i ≤ j ⟹ ι i ≤ ι j"
    and ι_fin: "⋀i. ι i ∈ tfin"
    and ι_progressing: "x ∈ tfin ⟹ ∃j. ¬ι j ≤ ι i + x"
    and zero_tfin: "0 ∈ tfin"
    and tfin_closed: "c ∈ tfin ⟹ d ∈ tfin ⟹ c + d ∈ tfin"
    and add_mono: "c ≤ d ⟹ a + c ≤ a + d"
    and add_pos: "a ∈ tfin ⟹ 0 < c ⟹ a < a + c"
begin

lemma add_mono_comm:
  fixes a :: 'a
  shows "c ≤ d ⟹ c + a ≤ d + a"
  by (auto simp: add.commute add_mono)

end

instantiation prod :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
begin

definition zero_prod :: "'a × 'b" where
  "zero_prod = (zero_class.zero, zero_class.zero)"

fun plus_prod :: "'a × 'b ⇒ 'a × 'b ⇒ 'a × 'b" where
  "(a, b) + (c, d) = (a + c, b + d)"

instance
  by standard (auto simp: zero_prod_def ac_simps)

end

instantiation enat :: timestamp
begin

definition tfin_enat :: "enat set" where
  "tfin_enat = UNIV - {∞}"

definition ι_enat :: "nat ⇒ enat" where
  "ι_enat n = n"

instance
  by standard (auto simp add: ι_enat_def tfin_enat_def dest!: leD)

end

instantiation ereal :: timestamp
begin

definition ι_ereal :: "nat ⇒ ereal" where
  "ι_ereal n = ereal n"

definition tfin_ereal :: "ereal set" where
  "tfin_ereal = UNIV - {-∞, ∞}"

lemma ereal_add_pos:
  fixes a :: ereal
  shows "a ∈ tfin ⟹ 0 < c ⟹ a < a + c"
  by (auto simp: tfin_ereal_def) (metis add.right_neutral ereal_add_cancel_left ereal_le_add_self order_less_le)

instance
  by standard (auto simp add: ι_ereal_def tfin_ereal_def add.commute
      ereal_add_le_add_iff2 not_le less_PInf_Ex_of_nat ereal_less_ereal_Ex reals_Archimedean2 intro: ereal_add_pos)

end

class timestamp_strict = timestamp +
  assumes timestamp_strict_total: "a ≤ b ∨ b ≤ a"
    and add_mono_strict: "c < d ⟹ a + c < a + d"

instantiation nat :: timestamp_strict
begin

definition tfin_nat :: "nat set" where
  "tfin_nat = UNIV"

definition ι_nat :: "nat ⇒ nat" where
  "ι_nat n = n"

instance
  by standard (auto simp add: ι_nat_def tfin_nat_def dest!: leD)

end

instantiation real :: timestamp_strict
begin

definition tfin_real :: "real set" where "tfin_real = UNIV"

definition ι_real :: "nat ⇒ real" where "ι_real n = real n"
instance
  by standard (auto simp: tfin_real_def ι_real_def not_le reals_Archimedean2)

end

class timestamp_total = timestamp +
  assumes timestamp_total: "a ≤ b ∨ b ≤ a"
  assumes aux: "0 ≤ a ⟹ a ≤ c ⟹ a ∈ tfin ⟹ c ∈ tfin ⟹ 0 ≤ b ⟹ b ∉ tfin ⟹ c < a + b"

instantiation enat :: timestamp_total
begin

instance
  apply standard
   apply (auto simp: tfin_enat_def)
  done

end

instantiation ereal :: timestamp_total
begin

instance
  apply standard
   apply (auto simp: tfin_ereal_def)
  done

end

class timestamp_total_strict = timestamp_total +
  assumes add_mono_strict_total: "c < d ⟹ a + c < a + d"

instantiation nat :: timestamp_total_strict
begin

instance
  apply standard
  apply (auto simp: tfin_nat_def)
  done

end

instantiation real :: timestamp_total_strict
begin

instance
  apply standard
  apply (auto simp: tfin_real_def)
  done

end

end

Theory Interval

(*<*)
theory Interval
  imports "HOL-Library.Product_Lexorder" Timestamp
begin
(*>*)

section ‹Intervals›

typedef (overloaded) ('a :: timestamp) ℐ = "{(i :: 'a, j :: 'a, lei :: bool, lej :: bool). 0 ≤ i ∧ i ≤ j ∧ i ∈ tfin ∧ ¬(j = 0 ∧ ¬lej)}"
  by (intro exI[of _ "(0, 0, True, True)"]) (auto intro: zero_tfin)

setup_lifting type_definition_ℐ

instantiation ℐ :: (timestamp) equal begin

lift_definition equal_ℐ :: "'a ℐ ⇒ 'a ℐ ⇒ bool" is "(=)" .

instance by standard (transfer, auto)

end

lift_definition left :: "'a :: timestamp ℐ ⇒ 'a" is "fst" .
lift_definition right :: "'a :: timestamp ℐ ⇒ 'a" is "fst ∘ snd" .

lift_definition memL :: "'a :: timestamp ⇒ 'a ⇒ 'a ℐ ⇒ bool" is
  "λt t' (a, b, lei, lej). if lei then t + a ≤ t' else t + a < t'" .

lift_definition memR :: "'a :: timestamp ⇒ 'a ⇒ 'a ℐ ⇒ bool" is
  "λt t' (a, b, lei, lej). if lej then t' ≤ t + b else t' < t + b" .

definition mem :: "'a :: timestamp ⇒ 'a ⇒ 'a ℐ ⇒ bool" where
  "mem t t' I ⟷ memL t t' I ∧ memR t t' I"

lemma memL_mono: "memL t t' I ⟹ t'' ≤ t ⟹ memL t'' t' I"
  by transfer (auto simp: add.commute order_le_less_subst2 order_subst2 add_mono split: if_splits)

lemma memL_mono': "memL t t' I ⟹ t' ≤ t'' ⟹ memL t t'' I"
  by transfer (auto split: if_splits)

lemma memR_mono: "memR t t' I ⟹ t ≤ t'' ⟹ memR t'' t' I"
  apply transfer
  apply (simp split: prod.splits)
  apply (meson add_mono_comm dual_order.trans order_less_le_trans)
  done

lemma memR_mono': "memR t t' I ⟹ t'' ≤ t' ⟹ memR t t'' I"
  by transfer (auto split: if_splits)

lemma memR_dest: "memR t t' I ⟹ t' ≤ t + right I"
  by transfer (auto split: if_splits)

lemma memR_tfin_refl:
  assumes fin: "t ∈ tfin"
  shows "memR t t I"
  by (transfer fixing: t) (force split: if_splits intro: order_trans[OF _ add_mono, where ?x=t and ?a1=t and ?c1=0] add_pos[OF fin])

lemma right_I_add_mono:
  fixes x :: "'a :: timestamp"
  shows "x ≤ x + right I"
  by transfer (auto split: if_splits intro: order_trans[OF _ add_mono, of _ _ 0])

lift_definition interval :: "'a :: timestamp ⇒ 'a ⇒ bool ⇒ bool ⇒ 'a ℐ" is
  "λi j lei lej. (if 0 ≤ i ∧ i ≤ j ∧ i ∈ tfin ∧ ¬(j = 0 ∧ ¬lej)then (i, j, lei, lej) else Code.abort (STR ''malformed interval'') (λ_. (0, 0, True, True)))"
  by (auto intro: zero_tfin)

lemma "Rep_ℐ I = (l, r, b1, b2) ⟹ memL 0 0 I ⟷ l = 0 ∧ b1"
  by transfer auto

lift_definition dropL :: "'a :: timestamp ℐ ⇒ 'a ℐ" is
  "λ(l, r, b1, b2). (0, r, True, b2)"
  by (auto intro: zero_tfin)

lemma memL_dropL: "t ≤ t' ⟹ memL t t' (dropL I)"
  by transfer auto

lemma memR_dropL: "memR t t' (dropL I) = memR t t' I"
  by transfer auto

lift_definition flipL :: "'a :: timestamp ℐ ⇒ 'a ℐ" is
  "λ(l, r, b1, b2). if ¬(l = 0 ∧ b1) then (0, l, True, ¬b1) else Code.abort (STR ''invalid flipL'') (λ_. (0, 0, True, True))"
  by (auto intro: zero_tfin split: if_splits)

lemma memL_flipL: "t ≤ t' ⟹ memL t t' (flipL I)"
  by transfer (auto split: if_splits)

lemma memR_flipLD: "¬memL 0 0 I ⟹ memR t t' (flipL I) ⟹ ¬memL t t' I"
  by transfer (auto split: if_splits)

lemma memR_flipLI:
  fixes t :: "'a :: timestamp"
  shows "(⋀u v. (u :: 'a :: timestamp) ≤ v ∨ v ≤ u) ⟹ ¬memL t t' I ⟹ memR t t' (flipL I)"
  by transfer (force split: if_splits)

lemma "t ∈ tfin ⟹ memL 0 0 I ⟷ memL t t I"
  apply transfer
  apply (simp split: prod.splits)
  apply (metis add.right_neutral add_pos antisym_conv2 dual_order.eq_iff order_less_imp_not_less)
  done

definition "full (I :: ('a :: timestamp_total) ℐ) ⟷ (∀t t'. 0 ≤ t ∧ t ≤ t' ∧ t ∈ tfin ∧ t' ∈ tfin ⟶ mem t t' I)"

lemma "memL 0 0 I ⟹ right I ∉ tfin ⟹ full I"
  unfolding full_def mem_def
  by transfer (fastforce split: if_splits dest: aux)

(*<*)
end
(*>*)
v class="head">

Theory Trace

(*<*)
theory Trace
  imports "HOL-Library.Stream" Timestamp
begin
(*>*)

section ‹Infinite Traces›

inductive sorted_list :: "'a :: order list ⇒ bool" where
  [intro]: "sorted_list []"
| [intro]: "sorted_list [x]"
| [intro]: "x ≤ y ⟹ sorted_list (y # ys) ⟹ sorted_list (x # y # ys)"

lemma sorted_list_app: "sorted_list xs ⟹ (⋀x. x ∈ set xs ⟹ x ≤ y) ⟹ sorted_list (xs @ [y])"
  by (induction xs rule: sorted_list.induct) auto

lemma sorted_list_drop: "sorted_list xs ⟹ sorted_list (drop n xs)"
proof (induction xs arbitrary: n rule: sorted_list.induct)
  case (2 x n)
  then show ?case
    by (cases n) auto
next
  case (3 x y ys n)
  then show ?case
    by (cases n) auto
qed auto

lemma sorted_list_ConsD: "sorted_list (x # xs) ⟹ sorted_list xs"
  by (auto elim: sorted_list.cases)

lemma sorted_list_Cons_nth: "sorted_list (x # xs) ⟹ j < length xs ⟹ x ≤ xs ! j"
  by (induction "x # xs" arbitrary: x xs j rule: sorted_list.induct)
     (fastforce simp: nth_Cons split: nat.splits)+

lemma sorted_list_atD: "sorted_list xs ⟹ i ≤ j ⟹ j < length xs ⟹ xs ! i ≤ xs ! j"
proof (induction xs arbitrary: i j rule: sorted_list.induct)
  case (2 x i j)
  then show ?case
    by (cases i) auto
next
  case (3 x y ys i j)
  have "x ≤ (x # y # ys) ! j"
    using 3(5) sorted_list_Cons_nth[OF sorted_list.intros(3)[OF 3(1,2)]]
    by (auto simp: nth_Cons split: nat.splits)
  then show ?case
    using 3
    by (cases i) auto
qed auto

coinductive ssorted :: "'a :: order stream ⇒ bool" where
  "shd s ≤ shd (stl s) ⟹ ssorted (stl s) ⟹ ssorted s"

lemma ssorted_siterate[simp]: "(⋀n. n ≤ f n) ⟹ ssorted (siterate f n)"
  by (coinduction arbitrary: n) auto

lemma ssortedD: "ssorted s ⟹ s !! i ≤ stl s !! i"
  by (induct i arbitrary: s) (auto elim: ssorted.cases)

lemma ssorted_sdrop: "ssorted s ⟹ ssorted (sdrop i s)"
  by (coinduction arbitrary: i s) (auto elim: ssorted.cases ssortedD)

lemma ssorted_monoD: "ssorted s ⟹ i ≤ j ⟹ s !! i ≤ s !! j"
proof (induct "j - i" arbitrary: j)
  case (Suc x)
  from Suc(1)[of "j - 1"] Suc(2-4) ssortedD[of s "j - 1"]
    show ?case by (cases j) (auto simp: le_Suc_eq Suc_diff_le)
qed simp

lemma sorted_stake: "ssorted s ⟹ sorted_list (stake i s)"
proof (induct i arbitrary: s)
  case (Suc i)
  then show ?case
    by (cases i) (auto elim: ssorted.cases)
qed auto

lemma ssorted_monoI: "∀i j. i ≤ j ⟶ s !! i ≤ s !! j ⟹ ssorted s"
  by (coinduction arbitrary: s)
    (auto dest: spec2[of _ "Suc _" "Suc _"] spec2[of _ 0 "Suc 0"])

lemma ssorted_iff_mono: "ssorted s ⟷ (∀i j. i ≤ j ⟶ s !! i ≤ s !! j)"
  using ssorted_monoI ssorted_monoD by metis

typedef (overloaded) ('a, 'b :: timestamp) trace = "{s :: ('a set × 'b) stream.
  ssorted (smap snd s) ∧ (∀x. x ∈ snd ` sset s ⟶ x ∈ tfin) ∧ (∀i x. x ∈ tfin ⟶ (∃j. ¬snd (s !! j) ≤ snd (s !! i) + x))}"
  by (auto simp: ι_mono ι_fin ι_progressing stream.set_map
      intro!: exI[of _ "smap (λn. ({}, ι n)) nats"] ssorted_monoI)

setup_lifting type_definition_trace

lift_definition Γ :: "('a, 'b :: timestamp) trace ⇒ nat ⇒ 'a set" is
  "λs i. fst (s !! i)" .
lift_definition τ :: "('a, 'b :: timestamp) trace ⇒ nat ⇒ 'b" is
  "λs i. snd (s !! i)" .

lemma τ_mono[simp]: "i ≤ j ⟹ τ s i ≤ τ s j"
  by transfer (auto simp: ssorted_iff_mono)

lemma τ_fin: "τ σ i ∈ tfin"
  by transfer auto

lemma ex_lt_τ: "x ∈ tfin ⟹ ∃j. ¬τ s j ≤ τ s i + x"
  by transfer auto

lemma le_τ_less: "τ σ i ≤ τ σ j ⟹ j < i ⟹ τ σ i = τ σ j"
  by (simp add: antisym)

lemma less_τD: "τ σ i < τ σ j ⟹ i < j"
  by (meson τ_mono less_le_not_le not_le_imp_less)

(*<*)
end
(*>*)
class="head">

Theory MDL

theory MDL
  imports Interval Trace
begin

section ‹Formulas and Satisfiability›

declare [[typedef_overloaded]]

datatype ('a, 't :: timestamp) formula = Bool bool | Atom 'a | Neg "('a, 't) formula" |
  Bin "bool ⇒ bool ⇒ bool" "('a, 't) formula" "('a, 't) formula" |
  Prev "'t ℐ" "('a, 't) formula" | Next "'t ℐ" "('a, 't) formula" |
  Since "('a, 't) formula" "'t ℐ" "('a, 't) formula" |
  Until "('a, 't) formula" "'t ℐ" "('a, 't) formula" |
  MatchP "'t ℐ" "('a, 't) regex" | MatchF "'t ℐ" "('a, 't) regex"
  and ('a, 't) regex = Lookahead "('a, 't) formula" | Symbol "('a, 't) formula" |
  Plus "('a, 't) regex" "('a, 't) regex" | Times "('a, 't) regex" "('a, 't) regex" |
  Star "('a, 't) regex"

fun eps :: "('a, 't :: timestamp) regex ⇒ bool" where
  "eps (Lookahead phi) = True"
| "eps (Symbol phi) = False"
| "eps (Plus r s) = (eps r ∨ eps s)"
| "eps (Times r s) = (eps r ∧ eps s)"
| "eps (Star r) = True"

fun atms :: "('a, 't :: timestamp) regex ⇒ ('a, 't) formula set" where
  "atms (Lookahead phi) = {phi}"
| "atms (Symbol phi) = {phi}"
| "atms (Plus r s) = atms r ∪ atms s"
| "atms (Times r s) = atms r ∪ atms s"
| "atms (Star r) = atms r"

lemma size_atms[termination_simp]: "phi ∈ atms r ⟹ size phi < size r"
  by (induction r) auto

fun wf_fmla :: "('a, 't :: timestamp) formula ⇒ bool"
  and wf_regex :: "('a, 't) regex ⇒ bool" where
  "wf_fmla (Bool b) = True"
| "wf_fmla (Atom a) = True"
| "wf_fmla (Neg phi) = wf_fmla phi"
| "wf_fmla (Bin f phi psi) = (wf_fmla phi ∧ wf_fmla psi)"
| "wf_fmla (Prev I phi) = wf_fmla phi"
| "wf_fmla (Next I phi) = wf_fmla phi"
| "wf_fmla (Since phi I psi) = (wf_fmla phi ∧ wf_fmla psi)"
| "wf_fmla (Until phi I psi) = (wf_fmla phi ∧ wf_fmla psi)"
| "wf_fmla (MatchP I r) = (wf_regex r ∧ (∀phi ∈ atms r. wf_fmla phi))"
| "wf_fmla (MatchF I r) = (wf_regex r ∧ (∀phi ∈ atms r. wf_fmla phi))"
| "wf_regex (Lookahead phi) = False"
| "wf_regex (Symbol phi) = wf_fmla phi"
| "wf_regex (Plus r s) = (wf_regex r ∧ wf_regex s)"
| "wf_regex (Times r s) = (wf_regex s ∧ (¬eps s ∨ wf_regex r))"
| "wf_regex (Star r) = wf_regex r"

fun progress :: "('a, 't :: timestamp) formula ⇒ 't list ⇒ nat" where
  "progress (Bool b) ts = length ts"
| "progress (Atom a) ts = length ts"
| "progress (Neg phi) ts = progress phi ts"
| "progress (Bin f phi psi) ts = min (progress phi ts) (progress psi ts)"
| "progress (Prev I phi) ts = min (length ts) (Suc (progress phi ts))"
| "progress (Next I phi) ts = (case progress phi ts of 0 ⇒ 0 | Suc k ⇒ k)"
| "progress (Since phi I psi) ts = min (progress phi ts) (progress psi ts)"
| "progress (Until phi I psi) ts = (if length ts = 0 then 0 else
  (let k = min (length ts - 1) (min (progress phi ts) (progress psi ts)) in
   Min {j. 0 ≤ j ∧ j ≤ k ∧ memR (ts ! j) (ts ! k) I}))"
| "progress (MatchP I r) ts = Min ((λf. progress f ts) ` atms r)"
| "progress (MatchF I r) ts = (if length ts = 0 then 0 else
  (let k = min (length ts - 1) (Min ((λf. progress f ts) ` atms r)) in
   Min {j. 0 ≤ j ∧ j ≤ k ∧ memR (ts ! j) (ts ! k) I}))"

fun bounded_future_fmla :: "('a, 't :: timestamp) formula ⇒ bool"
  and bounded_future_regex :: "('a, 't) regex ⇒ bool" where
  "bounded_future_fmla (Bool b) ⟷ True"
| "bounded_future_fmla (Atom a) ⟷ True"
| "bounded_future_fmla (Neg phi) ⟷ bounded_future_fmla phi"
| "bounded_future_fmla (Bin f phi psi) ⟷ bounded_future_fmla phi ∧ bounded_future_fmla psi"
| "bounded_future_fmla (Prev I phi) ⟷ bounded_future_fmla phi"
| "bounded_future_fmla (Next I phi) ⟷ bounded_future_fmla phi"
| "bounded_future_fmla (Since phi I psi) ⟷ bounded_future_fmla phi ∧ bounded_future_fmla psi"
| "bounded_future_fmla (Until phi I psi) ⟷ bounded_future_fmla phi ∧ bounded_future_fmla psi ∧ right I ∈ tfin"
| "bounded_future_fmla (MatchP I r) ⟷ bounded_future_regex r"
| "bounded_future_fmla (MatchF I r) ⟷ bounded_future_regex r ∧ right I ∈ tfin"
| "bounded_future_regex (Lookahead phi) ⟷ bounded_future_fmla phi"
| "bounded_future_regex (Symbol phi) ⟷ bounded_future_fmla phi"
| "bounded_future_regex (Plus r s) ⟷ bounded_future_regex r ∧ bounded_future_regex s"
| "bounded_future_regex (Times r s) ⟷ bounded_future_regex r ∧ bounded_future_regex s"
| "bounded_future_regex (Star r) ⟷ bounded_future_regex r"

lemmas regex_induct[case_names Lookahead Symbol Plus Times Star, induct type: regex] =
  regex.induct[of "λ_. True", simplified]

definition "Once I φ ≡ Since (Bool True) I φ"
definition "Historically I φ ≡ Neg (Once I (Neg φ))"
definition "Eventually I φ ≡ Until (Bool True) I φ"
definition "Always I φ ≡ Neg (Eventually I (Neg φ))"

fun rderive :: "('a, 't :: timestamp) regex ⇒ ('a, 't) regex" where
  "rderive (Lookahead phi) = Lookahead (Bool False)"
| "rderive (Symbol phi) = Lookahead phi"
| "rderive (Plus r s) = Plus (rderive r) (rderive s)"
| "rderive (Times r s) = (if eps s then Plus (rderive r) (Times r (rderive s)) else Times r (rderive s))"
| "rderive (Star r) = Times (Star r) (rderive r)"

lemma atms_rderive: "phi ∈ atms (rderive r) ⟹ phi ∈ atms r ∨ phi = Bool False"
  by (induction r) (auto split: if_splits)

lemma size_formula_positive: "size (phi :: ('a, 't :: timestamp) formula) > 0"
  by (induction phi) auto

lemma size_regex_positive: "size (r :: ('a, 't :: timestamp) regex) > Suc 0"
  by (induction r) (auto intro: size_formula_positive)

lemma size_rderive[termination_simp]: "phi ∈ atms (rderive r) ⟹ size phi < size r"
  by (drule atms_rderive) (auto intro: size_atms size_regex_positive)

locale MDL =
  fixes σ :: "('a, 't :: timestamp) trace"
begin

fun sat :: "('a, 't) formula ⇒ nat ⇒ bool"
  and match :: "('a, 't) regex ⇒ (nat × nat) set" where
  "sat (Bool b) i = b"
| "sat (Atom a) i = (a ∈ Γ σ i)"
| "sat (Neg φ) i = (¬ sat φ i)"
| "sat (Bin f φ ψ) i = (f (sat φ i) (sat ψ i))"
| "sat (Prev I φ) i = (case i of 0 ⇒ False | Suc j ⇒ mem (τ σ j) (τ σ i) I ∧ sat φ j)"
| "sat (Next I φ) i = (mem (τ σ i) (τ σ (Suc i)) I ∧ sat φ (Suc i))"
| "sat (Since φ I ψ) i = (∃j≤i. mem (τ σ j) (τ σ i) I ∧ sat ψ j ∧ (∀k ∈ {j<..i}. sat φ k))"
| "sat (Until φ I ψ) i = (∃j≥i. mem (τ σ i) (τ σ j) I ∧ sat ψ j ∧ (∀k ∈ {i..<j}. sat φ k))"
| "sat (MatchP I r) i = (∃j≤i. mem (τ σ j) (τ σ i) I ∧ (j, Suc i) ∈ match r)"
| "sat (MatchF I r) i = (∃j≥i. mem (τ σ i) (τ σ j) I ∧ (i, Suc j) ∈ match r)"
| "match (Lookahead φ) = {(i, i) | i. sat φ i}"
| "match (Symbol φ) = {(i, Suc i) | i. sat φ i}"
| "match (Plus r s) = match r ∪ match s"
| "match (Times r s) = match r O match s"
| "match (Star r) = rtrancl (match r)"

lemma "sat (Prev I (Bool False)) i ⟷ sat (Bool False) i"
  "sat (Next I (Bool False)) i ⟷ sat (Bool False) i"
  "sat (Since φ I (Bool False)) i ⟷ sat (Bool False) i"
  "sat (Until φ I (Bool False)) i ⟷ sat (Bool False) i"
  apply (auto split: nat.splits)
  done

lemma prev_rewrite: "sat (Prev I φ) i ⟷ sat (MatchP I (Times (Symbol φ) (Symbol (Bool True)))) i"
  apply (auto split: nat.splits)
  subgoal for j
    by (fastforce intro: exI[of _ j])
  done

lemma next_rewrite: "sat (Next I φ) i ⟷ sat (MatchF I (Times (Symbol (Bool True)) (Symbol φ))) i"
  by (fastforce intro: exI[of _ "Suc i"])

lemma trancl_Base: "{(i, Suc i) |i. P i}* = {(i, j). i ≤ j ∧ (∀k∈{i..<j}. P k)}"
proof -
  have "(x, y) ∈ {(i, j). i ≤ j ∧ (∀k∈{i..<j}. P k)}"
    if "(x, y) ∈ {(i, Suc i) |i. P i}*" for x y
    using that by (induct rule: rtrancl_induct) (auto simp: less_Suc_eq)
  moreover have "(x, y) ∈ {(i, Suc i) |i. P i}*"
    if "(x, y) ∈ {(i, j). i ≤ j ∧ (∀k∈{i..<j}. P k)}" for x y
    using that unfolding mem_Collect_eq prod.case Ball_def
    by (induct y arbitrary: x)
       (auto 0 3 simp: le_Suc_eq intro: rtrancl_into_rtrancl[rotated])
  ultimately show ?thesis by blast
qed

lemma Ball_atLeastLessThan_reindex:
  "(∀k∈{j..<i}. P (Suc k)) = (∀k ∈ {j<..i}. P k)"
  by (auto simp: less_eq_Suc_le less_eq_nat.simps split: nat.splits)

lemma since_rewrite: "sat (Since φ I ψ) i ⟷ sat (MatchP I (Times (Symbol ψ) (Star (Symbol φ)))) i"
proof (rule iffI)
  assume "sat (Since φ I ψ) i"
  then obtain j where j_def: "j ≤ i" "mem (τ σ j) (τ σ i) I" "sat ψ j"
    "∀k ∈ {j..<i}. sat φ (Suc k)"
    by auto
  have "k ∈ {Suc j..<Suc i} ⟹ (k, Suc k) ∈ match (Symbol φ)" for k
    using j_def(4)
    by (cases k) auto
  then have "(Suc j, Suc i) ∈ (match (Symbol φ))*"
    using j_def(1) trancl_Base
    by auto
  then show "sat (MatchP I (Times (Symbol ψ) (Star (Symbol φ)))) i"
    using j_def(1,2,3)
    by auto
next
  assume "sat (MatchP I (Times (Symbol ψ) (Star (Symbol φ)))) i"
  then obtain j where j_def: "j ≤ i" "mem (τ σ j) (τ σ i) I" "(Suc j, Suc i) ∈ (match (Symbol φ))*" "sat ψ j"
    by auto
  have "⋀k. k ∈ {Suc j..<Suc i} ⟹ (k, Suc k) ∈ match (Symbol φ)"
    using j_def(3) trancl_Base[of "λk. (k, Suc k) ∈ match (Symbol φ)"]
    by simp
  then have "∀k ∈ {j..<i}. sat φ (Suc k)"
    by auto
  then show "sat (Since φ I ψ) i"
    using j_def(1,2,4) Ball_atLeastLessThan_reindex[of j i "sat φ"]
    by auto
qed

lemma until_rewrite: "sat (Until φ I ψ) i ⟷ sat (MatchF I (Times (Star (Symbol φ)) (Symbol ψ))) i"
proof (rule iffI)
  assume "sat (Until φ I ψ) i"
  then obtain j where j_def: "j ≥ i" "mem (τ σ i) (τ σ j) I" "sat ψ j"
    "∀k ∈ {i..<j}. sat φ k"
    by auto
  have "k ∈ {i..<j} ⟹ (k, Suc k) ∈ match (Symbol φ)" for k
    using j_def(4)
    by auto
  then have "(i, j) ∈ (match (Symbol φ))*"
    using j_def(1) trancl_Base
    by simp
  then show "sat (MatchF I (Times (Star (Symbol φ)) (Symbol ψ))) i"
    using j_def(1,2,3)
    by auto
next
  assume "sat (MatchF I (Times (Star (Symbol φ)) (Symbol ψ))) i"
  then obtain j where j_def: "j ≥ i" "mem (τ σ i) (τ σ j) I" "(i, j) ∈ (match (Symbol φ))*" "sat ψ j"
    by auto
  have "⋀k. k ∈ {i..<j} ⟹ (k, Suc k) ∈ match (Symbol φ)"
    using j_def(3) trancl_Base[of "λk. (k, Suc k) ∈ match (Symbol φ)"]
    by auto
  then have "∀k ∈ {i..<j}. sat φ k"
    by simp
  then show "sat (Until φ I ψ) i"
    using j_def(1,2,4)
    by auto
qed

lemma match_le: "(i, j) ∈ match r ⟹ i ≤ j"
proof (induction r arbitrary: i j)
  case (Times r s)
  then show ?case using order.trans by fastforce
next
  case (Star r)
  from Star.prems show ?case
    unfolding match.simps
    by (induct i j rule: rtrancl.induct) (force dest: Star.IH)+
qed auto

lemma match_Times: "(i, i + n) ∈ match (Times r s) ⟷
  (∃k ≤ n. (i, i + k) ∈ match r ∧ (i + k, i + n) ∈ match s)"
  using match_le by auto (metis le_iff_add nat_add_left_cancel_le)

lemma rtrancl_unfold: "(x, z) ∈ rtrancl R ⟹
  x = z ∨ (∃y. (x, y) ∈ R ∧ x ≠ y ∧ (y, z) ∈ rtrancl R)"
  by (induction x z rule: rtrancl.induct) auto

lemma rtrancl_unfold': "(x, z) ∈ rtrancl R ⟹
  x = z ∨ (∃y. (x, y) ∈ rtrancl R ∧ y ≠ z ∧ (y, z) ∈ R)"
  by (induction x z rule: rtrancl.induct) auto

lemma match_Star: "(i, i + Suc n) ∈ match (Star r) ⟷
  (∃k ≤ n. (i, i + 1 + k) ∈ match r ∧ (i + 1 + k, i + Suc n) ∈ match (Star r))"
proof (rule iffI)
  assume assms: "(i, i + Suc n) ∈ match (Star r)"
  obtain k where k_def: "(i, k) ∈ local.match r" "i ≤ k" "i ≠ k"
    "(k, i + Suc n) ∈ (local.match r)*"
    using rtrancl_unfold[OF assms[unfolded match.simps]] match_le by auto
  from k_def(4) have "(k, i + Suc n) ∈ match (Star r)"
    unfolding match.simps by simp
  then have k_le: "k ≤ i + Suc n"
    using match_le by blast
  from k_def(2,3) obtain k' where k'_def: "k = i + Suc k'"
    by (metis Suc_diff_Suc le_add_diff_inverse le_neq_implies_less)
  show "∃k ≤ n. (i, i + 1 + k) ∈ match r ∧ (i + 1 + k, i + Suc n) ∈ match (Star r)"
    using k_def k_le unfolding k'_def by auto
next
  assume assms: "∃k ≤ n. (i, i + 1 + k) ∈ match r ∧
    (i + 1 + k, i + Suc n) ∈ match (Star r)"
  then show "(i, i + Suc n) ∈ match (Star r)"
    by (induction n) auto
qed

lemma match_refl_eps: "(i, i) ∈ match r ⟹ eps r"
proof (induction r)
  case (Times r s)
  then show ?case
    using match_Times[where ?i=i and ?n=0]
    by auto
qed auto

lemma wf_regex_eps_match: "wf_regex r ⟹ eps r ⟹ (i, i) ∈ match r"
  by (induction r arbitrary: i) auto

lemma match_Star_unfold: "i < j ⟹ (i, j) ∈ match (Star r) ⟹ ∃k ∈ {i..<j}. (i, k) ∈ match (Star r) ∧ (k, j) ∈ match r"
  using rtrancl_unfold'[of i j "match r"] match_le[of _ j r] match_le[of i _ "Star r"]
  by auto (meson atLeastLessThan_iff order_le_less)

lemma match_rderive: "wf_regex r ⟹ i ≤ j ⟹ (i, Suc j) ∈ match r ⟷ (i, j) ∈ match (rderive r)"
proof (induction r arbitrary: i j)
  case (Times r1 r2)
  then show ?case
    using match_refl_eps[of "Suc j" r2] match_le[of _ "Suc j" r2]
    apply (auto)
          apply (metis le_Suc_eq relcomp.simps)
         apply (meson match_le relcomp.simps)
        apply (metis le_SucE relcomp.simps)
       apply (meson relcomp.relcompI wf_regex_eps_match)
      apply (meson match_le relcomp.simps)
     apply (metis le_SucE relcomp.simps)
    apply (meson match_le relcomp.simps)
    done
next
  case (Star r)
  then show ?case
    using match_Star_unfold[of i "Suc j" r]
    by auto (meson match_le rtrancl.simps)
qed auto

end

lemma atms_nonempty: "atms r ≠ {}"
  by (induction r) auto

lemma atms_finite: "finite (atms r)"
  by (induction r) auto

lemma progress_le_ts:
  assumes "⋀t. t ∈ set ts ⟹ t ∈ tfin"
  shows "progress phi ts ≤ length ts"
  using assms
proof (induction phi ts rule: progress.induct)
  case (8 phi I psi ts)
  have "ts ≠ [] ⟹ Min {j. j ≤ min (length ts - Suc 0) (min (progress phi ts) (progress psi ts)) ∧
    memR (ts ! j) (ts ! min (length ts - Suc 0) (min (progress phi ts) (progress psi ts))) I}
    ≤ length ts"
    apply (rule le_trans[OF Min_le[where ?x="min (length ts - Suc 0) (min (progress phi ts) (progress psi ts))"]])
      apply (auto simp: in_set_conv_nth intro!: memR_tfin_refl 8(3))
    apply (metis One_nat_def diff_less length_greater_0_conv less_numeral_extra(1) min.commute min.strict_coboundedI2)
    done
  then show ?case
    by auto
next
  case (9 I r ts)
  then show ?case
    using atms_nonempty[of r] atms_finite[of r]
    by auto (meson Min_le dual_order.trans finite_imageI image_iff)
next
  case (10 I r ts)
  have "ts ≠ [] ⟹ Min {j. j ≤ min (length ts - Suc 0) (MIN f∈atms r. progress f ts) ∧
    memR (ts ! j) (ts ! min (length ts - Suc 0) (MIN f∈atms r. progress f ts)) I}
    ≤ length ts"
    apply (rule le_trans[OF Min_le[where ?x="min (length ts - Suc 0) (Min ((λf. progress f ts) ` atms r))"]])
      apply (auto simp: in_set_conv_nth intro!: memR_tfin_refl 10(2))
    apply (metis One_nat_def diff_less length_greater_0_conv less_numeral_extra(1) min.commute min.strict_coboundedI2)
    done
  then show ?case
    by auto
qed (auto split: nat.splits)

end
class="head">

Theory NFA

theory NFA
  imports "HOL-Library.IArray"
begin

type_synonym state = nat

datatype transition = eps_trans state nat | symb_trans state | split_trans state state

fun state_set :: "transition ⇒ state set" where
  "state_set (eps_trans s _) = {s}"
| "state_set (symb_trans s) = {s}"
| "state_set (split_trans s s') = {s, s'}"

fun fmla_set :: "transition ⇒ nat set" where
  "fmla_set (eps_trans _ n) = {n}"
| "fmla_set _ = {}"

lemma rtranclp_closed: "rtranclp R q q' ⟹ X = X ∪ {q'. ∃q ∈ X. R q q'} ⟹
  q ∈ X ⟹ q' ∈ X"
  by (induction q q' rule: rtranclp.induct) auto

lemma rtranclp_closed_sub: "rtranclp R q q' ⟹ {q'. ∃q ∈ X. R q q'} ⊆ X ⟹
  q ∈ X ⟹ q' ∈ X"
  by (induction q q' rule: rtranclp.induct) auto

lemma rtranclp_closed_sub': "rtranclp R q q' ⟹ q' = q ∨ (∃q''. R q q'' ∧ rtranclp R q'' q')"
  using converse_rtranclpE by force

lemma rtranclp_step: "rtranclp R q q'' ⟹ (⋀q'. R q q' ⟷ q' ∈ X) ⟹
  q = q'' ∨ (∃q' ∈ X. R q q' ∧ rtranclp R q' q'')"
  by (induction q q'' rule: rtranclp.induct)
     (auto intro: rtranclp.rtrancl_into_rtrancl)

lemma rtranclp_unfold: "rtranclp R x z ⟹ x = z ∨ (∃y. R x y ∧ rtranclp R y z)"
  by (induction x z rule: rtranclp.induct) auto

context fixes
  q0 :: "state" and
  qf :: "state" and
  transs :: "transition list"
begin

(* sets of states *)

qualified definition SQ :: "state set" where
  "SQ = {q0..<q0 + length transs}"

lemma q_in_SQ[code_unfold]: "q ∈ SQ ⟷ q0 ≤ q ∧ q < q0 + length transs"
  by (auto simp: SQ_def)

lemma finite_SQ: "finite SQ"
  by (auto simp add: SQ_def)

lemma transs_q_in_set: "q ∈ SQ ⟹ transs ! (q - q0) ∈ set transs"
  by (auto simp add: SQ_def)

qualified definition Q :: "state set" where
  "Q = SQ ∪ {qf}"

lemma finite_Q: "finite Q"
  by (auto simp add: Q_def SQ_def)

lemma SQ_sub_Q: "SQ ⊆ Q"
  by (auto simp add: SQ_def Q_def)

(* set of formula indices *)

qualified definition nfa_fmla_set :: "nat set" where
  "nfa_fmla_set = ⋃(fmla_set ` set transs)"

(* step relation *)

qualified definition step_eps :: "bool list ⇒ state ⇒ state ⇒ bool" where
  "step_eps bs q q' ⟷ q ∈ SQ ∧
    (case transs ! (q - q0) of eps_trans p n ⇒ n < length bs ∧ bs ! n ∧ p = q'
    | split_trans p p' ⇒ p = q' ∨ p' = q' | _ ⇒ False)"

lemma step_eps_dest: "step_eps bs q q' ⟹ q ∈ SQ"
  by (auto simp add: step_eps_def)

lemma step_eps_mono: "step_eps [] q q' ⟹ step_eps bs q q'"
  by (auto simp: step_eps_def split: transition.splits)

(* successors in step relation *)

qualified definition step_eps_sucs :: "bool list ⇒ state ⇒ state set" where
  "step_eps_sucs bs q = (if q ∈ SQ then
    (case transs ! (q - q0) of eps_trans p n ⇒ if n < length bs ∧ bs ! n then {p} else {}
    | split_trans p p' ⇒ {p, p'} | _ ⇒ {}) else {})"

lemma step_eps_sucs_sound: "q' ∈ step_eps_sucs bs q ⟷ step_eps bs q q'"
  by (auto simp add: step_eps_sucs_def step_eps_def split: transition.splits)

qualified definition step_eps_set :: "bool list ⇒ state set ⇒ state set" where
  "step_eps_set bs R = ⋃(step_eps_sucs bs ` R)"

lemma step_eps_set_sound: "step_eps_set bs R = {q'. ∃q ∈ R. step_eps bs q q'}"
  using step_eps_sucs_sound by (auto simp add: step_eps_set_def)

lemma step_eps_set_mono: "R ⊆ S ⟹ step_eps_set bs R ⊆ step_eps_set bs S"
  by (auto simp add: step_eps_set_def)

(* reflexive and transitive closure of step relation *)

qualified definition step_eps_closure :: "bool list ⇒ state ⇒ state ⇒ bool" where
  "step_eps_closure bs = (step_eps bs)**"

lemma step_eps_closure_dest: "step_eps_closure bs q q' ⟹ q ≠ q' ⟹ q ∈ SQ"
  unfolding step_eps_closure_def
  apply (induction q q' rule: rtranclp.induct) using step_eps_dest by auto

qualified definition step_eps_closure_set :: "state set ⇒ bool list ⇒ state set" where
  "step_eps_closure_set R bs = ⋃((λq. {q'. step_eps_closure bs q q'}) ` R)"

lemma step_eps_closure_set_refl: "R ⊆ step_eps_closure_set R bs"
  by (auto simp add: step_eps_closure_set_def step_eps_closure_def)

lemma step_eps_closure_set_mono: "R ⊆ S ⟹ step_eps_closure_set R bs ⊆ step_eps_closure_set S bs"
  by (auto simp add: step_eps_closure_set_def)

lemma step_eps_closure_set_empty: "step_eps_closure_set {} bs = {}"
  by (auto simp add: step_eps_closure_set_def)

lemma step_eps_closure_set_mono': "step_eps_closure_set R [] ⊆ step_eps_closure_set R bs"
  by (auto simp: step_eps_closure_set_def step_eps_closure_def) (metis mono_rtranclp step_eps_mono)

lemma step_eps_closure_set_split: "step_eps_closure_set (R ∪ S) bs =
  step_eps_closure_set R bs ∪ step_eps_closure_set S bs"
  by (auto simp add: step_eps_closure_set_def)

lemma step_eps_closure_set_Un: "step_eps_closure_set (⋃x ∈ X. R x) bs =
  (⋃x ∈ X. step_eps_closure_set (R x) bs)"
  by (auto simp add: step_eps_closure_set_def)

lemma step_eps_closure_set_idem: "step_eps_closure_set (step_eps_closure_set R bs) bs =
  step_eps_closure_set R bs"
  unfolding step_eps_closure_set_def step_eps_closure_def by auto

lemma step_eps_closure_set_flip:
  assumes "step_eps_closure_set R bs = R ∪ S"
  shows "step_eps_closure_set S bs ⊆ R ∪ S"
  using step_eps_closure_set_idem[of R bs, unfolded assms, unfolded step_eps_closure_set_split]
  by auto

lemma step_eps_closure_set_unfold: "(⋀q'. step_eps bs q q' ⟷ q' ∈ X) ⟹
  step_eps_closure_set {q} bs = {q} ∪ step_eps_closure_set X bs"
  unfolding step_eps_closure_set_def step_eps_closure_def
  using rtranclp_step[of "step_eps bs" q]
  by (auto simp add: converse_rtranclp_into_rtranclp)

lemma step_step_eps_closure: "step_eps bs q q' ⟹ q ∈ R ⟹ q' ∈ step_eps_closure_set R bs"
  unfolding step_eps_closure_set_def step_eps_closure_def by auto

lemma step_eps_closure_set_code[code]:
  "step_eps_closure_set R bs =
    (let R' = R ∪ step_eps_set bs R in if R = R' then R else step_eps_closure_set R' bs)"
  using rtranclp_closed
  by (auto simp add: step_eps_closure_set_def step_eps_closure_def step_eps_set_sound Let_def)

(* no step_eps *)

lemma step_eps_closure_empty: "step_eps_closure bs q q' ⟹ (⋀q'. ¬step_eps bs q q') ⟹ q = q'"
  unfolding step_eps_closure_def by (induction q q' rule: rtranclp.induct) auto

lemma step_eps_closure_set_step_id: "(⋀q q'. q ∈ R ⟹ ¬step_eps bs q q') ⟹
  step_eps_closure_set R bs = R"
  using step_eps_closure_empty step_eps_closure_set_refl unfolding step_eps_closure_set_def by blast

(* wildcard step relation *)

qualified definition step_symb :: "state ⇒ state ⇒ bool" where
  "step_symb q q' ⟷ q ∈ SQ ∧
    (case transs ! (q - q0) of symb_trans p ⇒ p = q' | _ ⇒ False)"

lemma step_symb_dest: "step_symb q q' ⟹ q ∈ SQ"
  by (auto simp add: step_symb_def)

(* successors in wildcard step relation *)

qualified definition step_symb_sucs :: "state ⇒ state set" where
  "step_symb_sucs q = (if q ∈ SQ then
    (case transs ! (q - q0) of symb_trans p ⇒ {p} | _ ⇒ {}) else {})"

lemma step_symb_sucs_sound: "q' ∈ step_symb_sucs q ⟷ step_symb q q'"
  by (auto simp add: step_symb_sucs_def step_symb_def split: transition.splits)

qualified definition step_symb_set :: "state set ⇒ state set" where
  "step_symb_set R = {q'. ∃q ∈ R. step_symb q q'}"

lemma step_symb_set_mono: "R ⊆ S ⟹ step_symb_set R ⊆ step_symb_set S"
  by (auto simp add: step_symb_set_def)

lemma step_symb_set_empty: "step_symb_set {} = {}"
  by (auto simp add: step_symb_set_def)

lemma step_symb_set_proj: "step_symb_set R = step_symb_set (R ∩ SQ)"
  using step_symb_dest by (auto simp add: step_symb_set_def)

lemma step_symb_set_split: "step_symb_set (R ∪ S) = step_symb_set R ∪ step_symb_set S"
  by (auto simp add: step_symb_set_def)

lemma step_symb_set_Un: "step_symb_set (⋃x ∈ X. R x) = (⋃x ∈ X. step_symb_set (R x))"
  by (auto simp add: step_symb_set_def)

lemma step_symb_set_code[code]: "step_symb_set R = ⋃(step_symb_sucs ` R)"
  using step_symb_sucs_sound by (auto simp add: step_symb_set_def)

(* delta function *)

qualified definition delta :: "state set ⇒ bool list ⇒ state set" where
  "delta R bs = step_symb_set (step_eps_closure_set R bs)"

lemma delta_eps: "delta (step_eps_closure_set R bs) bs = delta R bs"
  unfolding delta_def step_eps_closure_set_idem by (rule refl)

lemma delta_eps_split:
  assumes "step_eps_closure_set R bs = R ∪ S"
  shows "delta R bs = step_symb_set R ∪ delta S bs"
  unfolding delta_def assms step_symb_set_split
  using step_symb_set_mono[OF step_eps_closure_set_flip[OF assms], unfolded step_symb_set_split]
    step_symb_set_mono[OF step_eps_closure_set_refl] by auto

lemma delta_split: "delta (R ∪ S) bs = delta R bs ∪ delta S bs"
  by (auto simp add: delta_def step_symb_set_split step_eps_closure_set_split)

lemma delta_Un: "delta (⋃x ∈ X. R x) bs = (⋃x ∈ X. delta (R x) bs)"
  unfolding delta_def step_eps_closure_set_Un step_symb_set_Un by simp

lemma delta_step_symb_set_absorb: "delta R bs = delta R bs ∪ step_symb_set R"
  using step_eps_closure_set_refl by (auto simp add: delta_def step_symb_set_def)

lemma delta_sub_eps_mono:
  assumes "S ⊆ step_eps_closure_set R bs"
  shows "delta S bs ⊆ delta R bs"
  unfolding delta_def
  using step_symb_set_mono[OF step_eps_closure_set_mono[OF assms, of bs,
        unfolded step_eps_closure_set_idem]] by simp

(* run delta function *)

qualified definition run :: "state set ⇒ bool list list ⇒ state set" where
  "run R bss = foldl delta R bss"

lemma run_eps_split:
  assumes "step_eps_closure_set R bs = R ∪ S" "step_symb_set R = {}"
  shows "run R (bs # bss) = run S (bs # bss)"
  unfolding run_def foldl.simps delta_eps_split[OF assms(1), unfolded assms(2)]
  by auto

lemma run_empty: "run {} bss = {}"
  unfolding run_def
  by (induction bss)
     (auto simp add: delta_def step_symb_set_empty step_eps_closure_set_empty)

lemma run_Nil: "run R [] = R"
  by (auto simp add: run_def)

lemma run_Cons: "run R (bs # bss) = run (delta R bs) bss"
  unfolding run_def by simp

lemma run_split: "run (R ∪ S) bss = run R bss ∪ run S bss"
  unfolding run_def
  by (induction bss arbitrary: R S) (auto simp add: delta_split)

lemma run_Un: "run (⋃x ∈ X. R x) bss = (⋃x ∈ X. run (R x) bss)"
  unfolding run_def
  by (induction bss arbitrary: R) (auto simp add: delta_Un)

lemma run_comp: "run R (bss @ css) = run (run R bss) css"
  unfolding run_def by simp

(* accept function *)

qualified definition accept_eps :: "state set ⇒ bool list ⇒ bool" where
  "accept_eps R bs ⟷ (qf ∈ step_eps_closure_set R bs)"

lemma step_eps_accept_eps: "step_eps bs q qf ⟹ q ∈ R ⟹ accept_eps R bs"
  unfolding accept_eps_def using step_step_eps_closure by simp

lemma accept_eps_empty: "accept_eps {} bs ⟷ False"
  by (auto simp add: accept_eps_def step_eps_closure_set_def)

lemma accept_eps_split: "accept_eps (R ∪ S) bs ⟷ accept_eps R bs ∨ accept_eps S bs"
  by (auto simp add: accept_eps_def step_eps_closure_set_split)

lemma accept_eps_Un: "accept_eps (⋃x ∈ X. R x) bs ⟷ (∃x ∈ X. accept_eps (R x) bs)"
  by (auto simp add: accept_eps_def step_eps_closure_set_def)

qualified definition accept :: "state set ⇒ bool" where
  "accept R ⟷ accept_eps R []"

(* is a run accepting? *)

qualified definition run_accept_eps :: "state set ⇒ bool list list ⇒ bool list ⇒ bool" where
  "run_accept_eps R bss bs = accept_eps (run R bss) bs"

lemma run_accept_eps_empty: "¬run_accept_eps {} bss bs"
  unfolding run_accept_eps_def run_empty accept_eps_empty by simp

lemma run_accept_eps_Nil: "run_accept_eps R [] cs ⟷ accept_eps R cs"
  by (auto simp add: run_accept_eps_def run_Nil)

lemma run_accept_eps_Cons: "run_accept_eps R (bs # bss) cs ⟷ run_accept_eps (delta R bs) bss cs"
  by (auto simp add: run_accept_eps_def run_Cons)

lemma run_accept_eps_Cons_delta_cong: "delta R bs = delta S bs ⟹
  run_accept_eps R (bs # bss) cs ⟷ run_accept_eps S (bs # bss) cs"
  unfolding run_accept_eps_Cons by auto

lemma run_accept_eps_Nil_eps: "run_accept_eps (step_eps_closure_set R bs) [] bs ⟷ run_accept_eps R [] bs"
  unfolding run_accept_eps_Nil accept_eps_def step_eps_closure_set_idem by (rule refl)

lemma run_accept_eps_Cons_eps: "run_accept_eps (step_eps_closure_set R cs) (cs # css) bs ⟷
  run_accept_eps R (cs # css) bs"
  unfolding run_accept_eps_Cons delta_eps by (rule refl)

lemma run_accept_eps_Nil_eps_split:
  assumes "step_eps_closure_set R bs = R ∪ S" "step_symb_set R = {}" "qf ∉ R"
  shows "run_accept_eps R [] bs = run_accept_eps S [] bs"
  unfolding Nil run_accept_eps_Nil accept_eps_def assms(1)
  using assms(3) step_eps_closure_set_refl step_eps_closure_set_flip[OF assms(1)] by auto

lemma run_accept_eps_Cons_eps_split:
  assumes "step_eps_closure_set R cs = R ∪ S" "step_symb_set R = {}" "qf ∉ R"
  shows "run_accept_eps R (cs # css) bs = run_accept_eps S (cs # css) bs"
  unfolding run_accept_eps_def Cons run_eps_split[OF assms(1,2)] by (rule refl)

lemma run_accept_eps_split: "run_accept_eps (R ∪ S) bss bs ⟷
  run_accept_eps R bss bs ∨ run_accept_eps S bss bs"
  unfolding run_accept_eps_def run_split accept_eps_split by auto

lemma run_accept_eps_Un: "run_accept_eps (⋃x ∈ X. R x) bss bs ⟷
  (∃x ∈ X. run_accept_eps (R x) bss bs)"
  unfolding run_accept_eps_def run_Un accept_eps_Un by simp

qualified definition run_accept :: "state set ⇒ bool list list ⇒ bool" where
  "run_accept R bss = accept (run R bss)"

end

definition "iarray_of_list xs = IArray xs"

context fixes
  transs :: "transition iarray"
  and len :: nat
begin

qualified definition step_eps' :: "bool iarray ⇒ state ⇒ state ⇒ bool" where
  "step_eps' bs q q' ⟷ q < len ∧
    (case transs !! q of eps_trans p n ⇒ n < IArray.length bs ∧ bs !! n ∧ p = q'
    | split_trans p p' ⇒ p = q' ∨ p' = q' | _ ⇒ False)"

qualified definition step_eps_closure' :: "bool iarray ⇒ state ⇒ state ⇒ bool" where
  "step_eps_closure' bs = (step_eps' bs)**"

qualified definition step_eps_sucs' :: "bool iarray ⇒ state ⇒ state set" where
  "step_eps_sucs' bs q = (if q < len then
    (case transs !! q of eps_trans p n ⇒ if n < IArray.length bs ∧ bs !! n then {p} else {}
    | split_trans p p' ⇒ {p, p'} | _ ⇒ {}) else {})"

lemma step_eps_sucs'_sound: "q' ∈ step_eps_sucs' bs q ⟷ step_eps' bs q q'"
  by (auto simp add: step_eps_sucs'_def step_eps'_def split: transition.splits)

qualified definition step_eps_set' :: "bool iarray ⇒ state set ⇒ state set" where
  "step_eps_set' bs R = ⋃(step_eps_sucs' bs ` R)"

lemma step_eps_set'_sound: "step_eps_set' bs R = {q'. ∃q ∈ R. step_eps' bs q q'}"
  using step_eps_sucs'_sound by (auto simp add: step_eps_set'_def)

qualified definition step_eps_closure_set' :: "state set ⇒ bool iarray ⇒ state set" where
  "step_eps_closure_set' R bs = ⋃((λq. {q'. step_eps_closure' bs q q'}) ` R)"

lemma step_eps_closure_set'_code[code]:
  "step_eps_closure_set' R bs =
    (let R' = R ∪ step_eps_set' bs R in if R = R' then R else step_eps_closure_set' R' bs)"
  using rtranclp_closed
  by (auto simp add: step_eps_closure_set'_def step_eps_closure'_def step_eps_set'_sound Let_def)

qualified definition step_symb_sucs' :: "state ⇒ state set" where
  "step_symb_sucs' q = (if q < len then
    (case transs !! q of symb_trans p ⇒ {p} | _ ⇒ {}) else {})"

qualified definition step_symb_set' :: "state set ⇒ state set" where
  "step_symb_set' R = ⋃(step_symb_sucs' ` R)"

qualified definition delta' :: "state set ⇒ bool iarray ⇒ state set" where
  "delta' R bs = step_symb_set' (step_eps_closure_set' R bs)"

qualified definition accept_eps' :: "state set ⇒ bool iarray ⇒ bool" where
  "accept_eps' R bs ⟷ (len ∈ step_eps_closure_set' R bs)"

qualified definition accept' :: "state set ⇒ bool" where
  "accept' R ⟷ accept_eps' R (iarray_of_list [])"

qualified definition run' :: "state set ⇒ bool iarray list ⇒ state set" where
  "run' R bss = foldl delta' R bss"

qualified definition run_accept_eps' :: "state set ⇒ bool iarray list ⇒ bool iarray ⇒ bool" where
  "run_accept_eps' R bss bs = accept_eps' (run' R bss) bs"

qualified definition run_accept' :: "state set ⇒ bool iarray list ⇒ bool" where
  "run_accept' R bss = accept' (run' R bss)"

end

locale nfa_array =
  fixes transs :: "transition list"
    and transs' :: "transition iarray"
    and len :: nat
  assumes transs_eq: "transs' = IArray transs"
    and len_def: "len = length transs"
begin

abbreviation "step_eps ≡ NFA.step_eps 0 transs"
abbreviation "step_eps' ≡ NFA.step_eps' transs' len"
abbreviation "step_eps_closure ≡ NFA.step_eps_closure 0 transs"
abbreviation "step_eps_closure' ≡ NFA.step_eps_closure' transs' len"
abbreviation "step_eps_sucs ≡ NFA.step_eps_sucs 0 transs"
abbreviation "step_eps_sucs' ≡ NFA.step_eps_sucs' transs' len"
abbreviation "step_eps_set ≡ NFA.step_eps_set 0 transs"
abbreviation "step_eps_set' ≡ NFA.step_eps_set' transs' len"
abbreviation "step_eps_closure_set ≡ NFA.step_eps_closure_set 0 transs"
abbreviation "step_eps_closure_set' ≡ NFA.step_eps_closure_set' transs' len"
abbreviation "step_symb_sucs ≡ NFA.step_symb_sucs 0 transs"
abbreviation "step_symb_sucs' ≡ NFA.step_symb_sucs' transs' len"
abbreviation "step_symb_set ≡ NFA.step_symb_set 0 transs"
abbreviation "step_symb_set' ≡ NFA.step_symb_set' transs' len"
abbreviation "delta ≡ NFA.delta 0 transs"
abbreviation "delta' ≡ NFA.delta' transs' len"
abbreviation "accept_eps ≡ NFA.accept_eps 0 len transs"
abbreviation "accept_eps' ≡ NFA.accept_eps' transs' len"
abbreviation "accept ≡ NFA.accept 0 len transs"
abbreviation "accept' ≡ NFA.accept' transs' len"
abbreviation "run ≡ NFA.run 0 transs"
abbreviation "run' ≡ NFA.run' transs' len"
abbreviation "run_accept_eps ≡ NFA.run_accept_eps 0 len transs"
abbreviation "run_accept_eps' ≡ NFA.run_accept_eps' transs' len"
abbreviation "run_accept ≡ NFA.run_accept 0 len transs"
abbreviation "run_accept' ≡ NFA.run_accept' transs' len"

lemma q_in_SQ: "q ∈ NFA.SQ 0 transs ⟷ q < len"
  using len_def
  by (auto simp: NFA.SQ_def)

lemma step_eps'_eq: "bs' = IArray bs ⟹ step_eps bs q q' ⟷ step_eps' bs' q q'"
  by (auto simp: NFA.step_eps_def NFA.step_eps'_def q_in_SQ transs_eq split: transition.splits)

lemma step_eps_closure'_eq: "bs' = IArray bs ⟹ step_eps_closure bs q q' ⟷ step_eps_closure' bs' q q'"
proof -
  assume lassm: "bs' = IArray bs"
  have step_eps_eq_folded: "step_eps bs = step_eps' bs'"
    using step_eps'_eq[OF lassm]
    by auto
  show ?thesis
    by (auto simp: NFA.step_eps_closure_def NFA.step_eps_closure'_def step_eps_eq_folded)
qed

lemma step_eps_sucs'_eq: "bs' = IArray bs ⟹ step_eps_sucs bs q = step_eps_sucs' bs' q"
  by (auto simp: NFA.step_eps_sucs_def NFA.step_eps_sucs'_def q_in_SQ transs_eq
      split: transition.splits)

lemma step_eps_set'_eq: "bs' = IArray bs ⟹ step_eps_set bs R = step_eps_set' bs' R"
  by (auto simp: NFA.step_eps_set_def NFA.step_eps_set'_def step_eps_sucs'_eq)

lemma step_eps_closure_set'_eq: "bs' = IArray bs ⟹ step_eps_closure_set R bs = step_eps_closure_set' R bs'"
  by (auto simp: NFA.step_eps_closure_set_def NFA.step_eps_closure_set'_def step_eps_closure'_eq)

lemma step_symb_sucs'_eq: "bs' = IArray bs ⟹ step_symb_sucs R = step_symb_sucs' R"
  by (auto simp: NFA.step_symb_sucs_def NFA.step_symb_sucs'_def q_in_SQ transs_eq
      split: transition.splits)

lemma step_symb_set'_eq: "bs' = IArray bs ⟹ step_symb_set R = step_symb_set' R"
  by (auto simp: step_symb_set_code NFA.step_symb_set'_def step_symb_sucs'_eq)

lemma delta'_eq: "bs' = IArray bs ⟹ delta R bs = delta' R bs'"
  by (auto simp: NFA.delta_def NFA.delta'_def step_eps_closure_set'_eq step_symb_set'_eq)

lemma accept_eps'_eq: "bs' = IArray bs ⟹ accept_eps R bs = accept_eps' R bs'"
  by (auto simp: NFA.accept_eps_def NFA.accept_eps'_def step_eps_closure_set'_eq)

lemma accept'_eq: "accept R = accept' R"
  by (auto simp: NFA.accept_def NFA.accept'_def accept_eps'_eq iarray_of_list_def)

lemma run'_eq: "bss' = map IArray bss ⟹ run R bss = run' R bss'"
  by (induction bss arbitrary: R bss') (auto simp: NFA.run_def NFA.run'_def delta'_eq)

lemma run_accept_eps'_eq: "bss' = map IArray bss ⟹ bs' = IArray bs ⟹
  run_accept_eps R bss bs ⟷ run_accept_eps' R bss' bs'"
  by (auto simp: NFA.run_accept_eps_def NFA.run_accept_eps'_def accept_eps'_eq run'_eq)

lemma run_accept'_eq: "bss' = map IArray bss ⟹
  run_accept R bss ⟷ run_accept' R bss'"
  by (auto simp: NFA.run_accept_def NFA.run_accept'_def run'_eq accept'_eq)

end

locale nfa =
  fixes q0 :: nat
    and qf :: nat
    and transs :: "transition list"
  assumes state_closed: "⋀t. t ∈ set transs ⟹ state_set t ⊆ NFA.Q q0 qf transs"
    and transs_not_Nil: "transs ≠ []"
    and qf_not_in_SQ: "qf ∉ NFA.SQ q0 transs"
begin

abbreviation "SQ ≡ NFA.SQ q0 transs"
abbreviation "Q ≡ NFA.Q q0 qf transs"
abbreviation "nfa_fmla_set ≡ NFA.nfa_fmla_set transs"
abbreviation "step_eps ≡ NFA.step_eps q0 transs"
abbreviation "step_eps_sucs ≡ NFA.step_eps_sucs q0 transs"
abbreviation "step_eps_set ≡ NFA.step_eps_set q0 transs"
abbreviation "step_eps_closure ≡ NFA.step_eps_closure q0 transs"
abbreviation "step_eps_closure_set ≡ NFA.step_eps_closure_set q0 transs"
abbreviation "step_symb ≡ NFA.step_symb q0 transs"
abbreviation "step_symb_sucs ≡ NFA.step_symb_sucs q0 transs"
abbreviation "step_symb_set ≡ NFA.step_symb_set q0 transs"
abbreviation "delta ≡ NFA.delta q0 transs"
abbreviation "run ≡ NFA.run q0 transs"
abbreviation "accept_eps ≡ NFA.accept_eps q0 qf transs"
abbreviation "run_accept_eps ≡ NFA.run_accept_eps q0 qf transs"

lemma Q_diff_qf_SQ: "Q - {qf} = SQ"
  using qf_not_in_SQ by (auto simp add: NFA.Q_def)

lemma q0_sub_SQ: "{q0} ⊆ SQ"
  using transs_not_Nil by (auto simp add: NFA.SQ_def)

lemma q0_sub_Q: "{q0} ⊆ Q"
  using q0_sub_SQ SQ_sub_Q by auto

lemma step_eps_closed: "step_eps bs q q' ⟹ q' ∈ Q"
  using transs_q_in_set state_closed
  by (fastforce simp add: NFA.step_eps_def split: transition.splits)

lemma step_eps_set_closed: "step_eps_set bs R ⊆ Q"
  using step_eps_closed by (auto simp add: step_eps_set_sound)

lemma step_eps_closure_closed: "step_eps_closure bs q q' ⟹ q ≠ q' ⟹ q' ∈ Q"
  unfolding NFA.step_eps_closure_def
  apply (induction q q' rule: rtranclp.induct) using step_eps_closed by auto

lemma step_eps_closure_set_closed_union: "step_eps_closure_set R bs ⊆ R ∪ Q"
  using step_eps_closure_closed by (auto simp add: NFA.step_eps_closure_set_def NFA.step_eps_closure_def)

lemma step_eps_closure_set_closed: "R ⊆ Q ⟹ step_eps_closure_set R bs ⊆ Q"
  using step_eps_closure_set_closed_union by auto

lemma step_symb_closed: "step_symb q q' ⟹ q' ∈ Q"
  using transs_q_in_set state_closed
  by (fastforce simp add: NFA.step_symb_def split: transition.splits)

lemma step_symb_set_closed: "step_symb_set R ⊆ Q"
  using step_symb_closed by (auto simp add: NFA.step_symb_set_def)

lemma step_symb_set_qf: "step_symb_set {qf} = {}"
  using qf_not_in_SQ step_symb_set_proj[of _ _ "{qf}"] step_symb_set_empty by auto

lemma delta_closed: "delta R bs ⊆ Q"
  using step_symb_set_closed by (auto simp add: NFA.delta_def)

lemma run_closed_Cons: "run R (bs # bss) ⊆ Q"
  unfolding NFA.run_def
  using delta_closed by (induction bss arbitrary: R bs) auto

lemma run_closed: "R ⊆ Q ⟹ run R bss ⊆ Q"
  using run_Nil run_closed_Cons by (cases bss) auto

(* transitions from accepting state *)

lemma step_eps_qf: "step_eps bs qf q ⟷ False"
  using qf_not_in_SQ step_eps_dest by force

lemma step_symb_qf: "step_symb qf q ⟷ False"
  using qf_not_in_SQ step_symb_dest by force

lemma step_eps_closure_qf: "step_eps_closure bs q q' ⟹ q = qf ⟹ q = q'"
  unfolding NFA.step_eps_closure_def
  apply (induction q q' rule: rtranclp.induct) using step_eps_qf by auto

lemma step_eps_closure_set_qf: "step_eps_closure_set {qf} bs = {qf}"
  using step_eps_closure_qf unfolding NFA.step_eps_closure_set_def NFA.step_eps_closure_def by auto

lemma delta_qf: "delta {qf} bs = {}"
  using step_eps_closure_qf step_symb_qf
  by (auto simp add: NFA.delta_def NFA.step_symb_set_def NFA.step_eps_closure_set_def)

lemma run_qf_many: "run {qf} (bs # bss) = {}"
  unfolding run_Cons delta_qf run_empty by (rule refl)

lemma run_accept_eps_qf_many: "run_accept_eps {qf} (bs # bss) cs ⟷ False"
  unfolding NFA.run_accept_eps_def using run_qf_many accept_eps_empty by simp

lemma run_accept_eps_qf_one: "run_accept_eps {qf} [] bs ⟷ True"
  unfolding NFA.run_accept_eps_def NFA.accept_eps_def using run_Nil step_eps_closure_set_refl by force

end

locale nfa_cong = nfa q0 qf transs + nfa': nfa q0' qf' transs'
  for q0 q0' qf qf' transs transs' +
  assumes SQ_sub: "nfa'.SQ ⊆ SQ" and
  qf_eq: "qf = qf'" and
  transs_eq: "⋀q. q ∈ nfa'.SQ ⟹ transs ! (q - q0) = transs' ! (q - q0')"
begin

lemma q_Q_SQ_nfa'_SQ:  "q ∈ nfa'.Q ⟹ q ∈ SQ ⟷ q ∈ nfa'.SQ"
  using SQ_sub qf_not_in_SQ qf_eq by (auto simp add: NFA.Q_def)

lemma step_eps_cong: "q ∈ nfa'.Q ⟹ step_eps bs q q' ⟷ nfa'.step_eps bs q q'"
  using q_Q_SQ_nfa'_SQ transs_eq by (auto simp add: NFA.step_eps_def)

lemma eps_nfa'_step_eps_closure: "step_eps_closure bs q q' ⟹ q ∈ nfa'.Q ⟹
  q' ∈ nfa'.Q ∧ nfa'.step_eps_closure bs q q'"
  unfolding NFA.step_eps_closure_def
  apply (induction q q' rule: rtranclp.induct)
  using nfa'.step_eps_closure_closed step_eps_cong by (auto simp add: NFA.step_eps_closure_def)

lemma nfa'_eps_step_eps_closure: "nfa'.step_eps_closure bs q q' ⟹ q ∈ nfa'.Q ⟹
  q' ∈ nfa'.Q ∧ step_eps_closure bs q q'"
  unfolding NFA.step_eps_closure_def
  apply (induction q q' rule: rtranclp.induct)
  using nfa'.step_eps_closed step_eps_cong
  by (auto simp add: NFA.step_eps_closure_def intro: rtranclp.intros(2))

lemma step_eps_closure_set_cong: "R ⊆ nfa'.Q ⟹ step_eps_closure_set R bs =
  nfa'.step_eps_closure_set R bs"
  using eps_nfa'_step_eps_closure nfa'_eps_step_eps_closure
  by (fastforce simp add: NFA.step_eps_closure_set_def)

lemma step_symb_cong: "q ∈ nfa'.Q ⟹ step_symb q q' ⟷ nfa'.step_symb q q'"
  using q_Q_SQ_nfa'_SQ transs_eq by (auto simp add: NFA.step_symb_def)

lemma step_symb_set_cong: "R ⊆ nfa'.Q ⟹ step_symb_set R = nfa'.step_symb_set R"
  using step_symb_cong by (auto simp add: NFA.step_symb_set_def)

lemma delta_cong: "R ⊆ nfa'.Q ⟹ delta R bs = nfa'.delta R bs"
  using step_symb_set_cong nfa'.step_eps_closure_set_closed
  by (auto simp add: NFA.delta_def step_eps_closure_set_cong)

lemma run_cong: "R ⊆ nfa'.Q ⟹ run R bss = nfa'.run R bss"
  unfolding NFA.run_def
  using nfa'.delta_closed delta_cong by (induction bss arbitrary: R) auto

lemma accept_eps_cong: "R ⊆ nfa'.Q ⟹ accept_eps R bs ⟷ nfa'.accept_eps R bs"
  unfolding NFA.accept_eps_def using step_eps_closure_set_cong qf_eq by auto

lemma run_accept_eps_cong:
  assumes "R ⊆ nfa'.Q"
  shows "run_accept_eps R bss bs ⟷ nfa'.run_accept_eps R bss bs"
  unfolding NFA.run_accept_eps_def run_cong[OF assms]
    accept_eps_cong[OF nfa'.run_closed[OF assms]] by simp

end

fun list_split :: "'a list ⇒ ('a list × 'a list) set" where
  "list_split [] = {}"
| "list_split (x # xs) = {([], x # xs)} ∪ (⋃(ys, zs) ∈ list_split xs. {(x # ys, zs)})"

lemma list_split_unfold: "(⋃(ys, zs) ∈ list_split (x # xs). f ys zs) =
  f [] (x # xs) ∪ (⋃(ys, zs) ∈ list_split xs. f (x # ys) zs)"
  by (induction xs) auto

lemma list_split_def: "list_split xs = (⋃n < length xs. {(take n xs, drop n xs)})"
  using less_Suc_eq_0_disj by (induction xs rule: list_split.induct) auto+

locale nfa_cong' = nfa q0 qf transs + nfa': nfa q0' qf' transs'
  for q0 q0' qf qf' transs transs' +
  assumes SQ_sub: "nfa'.SQ ⊆ SQ" and
  qf'_in_SQ: "qf' ∈ SQ" and
  transs_eq: "⋀q. q ∈ nfa'.SQ ⟹ transs ! (q - q0) = transs' ! (q - q0')"
begin

lemma nfa'_Q_sub_Q: "nfa'.Q ⊆ Q"
  unfolding NFA.Q_def using SQ_sub qf'_in_SQ by auto

lemma q_SQ_SQ_nfa'_SQ:  "q ∈ nfa'.SQ ⟹ q ∈ SQ ⟷ q ∈ nfa'.SQ"
  using SQ_sub by auto

lemma step_eps_cong_SQ: "q ∈ nfa'.SQ ⟹ step_eps bs q q' ⟷ nfa'.step_eps bs q q'"
  using q_SQ_SQ_nfa'_SQ transs_eq by (auto simp add: NFA.step_eps_def)

lemma step_eps_cong_Q: "q ∈ nfa'.Q ⟹ nfa'.step_eps bs q q' ⟹ step_eps bs q q'"
  using SQ_sub transs_eq by (auto simp add: NFA.step_eps_def)

lemma nfa'_step_eps_closure_cong: "nfa'.step_eps_closure bs q q' ⟹ q ∈ nfa'.Q ⟹
  step_eps_closure bs q q'"
  unfolding NFA.step_eps_closure_def
  apply (induction q q' rule: rtranclp.induct)
  using NFA.Q_def NFA.step_eps_closure_def
  by (auto simp add: rtranclp.rtrancl_into_rtrancl step_eps_cong_SQ step_eps_dest)

lemma nfa'_step_eps_closure_set_sub: "R ⊆ nfa'.Q ⟹ nfa'.step_eps_closure_set R bs ⊆
  step_eps_closure_set R bs"
  unfolding NFA.step_eps_closure_set_def
  using nfa'_step_eps_closure_cong by fastforce

lemma eps_nfa'_step_eps_closure_cong: "step_eps_closure bs q q' ⟹ q ∈ nfa'.Q ⟹
  (q' ∈ nfa'.Q ∧ nfa'.step_eps_closure bs q q') ∨
  (nfa'.step_eps_closure bs q qf' ∧ step_eps_closure bs qf' q')"
  unfolding NFA.step_eps_closure_def
  apply (induction q q' rule: rtranclp.induct)
  using nfa'.step_eps_closure_closed nfa'.step_eps_closed step_eps_cong_SQ NFA.Q_def
  by (auto simp add: intro: rtranclp.rtrancl_into_rtrancl) fastforce+

lemma nfa'_eps_step_eps_closure_cong: "nfa'.step_eps_closure bs q q' ⟹ q ∈ nfa'.Q ⟹
  q' ∈ nfa'.Q ∧ step_eps_closure bs q q'"
  unfolding NFA.step_eps_closure_def
  apply (induction q q' rule: rtranclp.induct)
  using nfa'.step_eps_closed step_eps_cong_Q
  by (auto