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`