# Theory Pi_Equivalence_Checking

```(* Author: Dmitriy Traytel *)

section ‹Deciding Equivalence of \$\Pi\$-Extended Regular Expressions›

(*<*)
theory Pi_Equivalence_Checking
imports Pi_Regular_Exp "HOL-Library.While_Combinator" List_More
begin
(*>*)

lemma image2p_in_rel: "BNF_Greatest_Fixpoint.image2p f g (in_rel R) =  in_rel (map_prod f g ` R)"
unfolding image2p_def fun_eq_iff by auto

lemma image2p_apply: "BNF_Greatest_Fixpoint.image2p f g R x y = (∃x' y'. R x' y' ∧ f x' = x ∧ g y' = y)"
unfolding image2p_def fun_eq_iff by auto

lemma rtrancl_fold_product:
shows "{((r, s), (f a r, f a s))| r s a. a ∈ A}^* =
{((r, s), (fold f w r, fold f w s))| r s w. w ∈ lists A}" (is "?L = ?R")
proof-
{ fix x :: "('a × 'a) × 'a × 'a"
obtain r s r' s' where x: "x = ((r, s), (r', s'))" by (cases x) auto
have "((r, s), (r', s')) ∈ ?L ⟹ ((r, s), (r', s')) ∈ ?R"
proof(induction rule: converse_rtrancl_induct2)
case refl show ?case by(force intro!: fold_simps(1)[symmetric])
next
case step thus ?case by(force intro!: fold_simps(2)[symmetric])
qed
with x have "x ∈ ?L ⟹ x ∈ ?R" by simp
} moreover
{ fix x :: "('a × 'a) × 'a × 'a"
obtain r s r' s' where x: "x = ((r, s), (r', s'))" by (cases x) auto
{ fix w have "∀x∈set w. x ∈ A ⟹ ((r, s), fold f w r, fold f w s) ∈ ?L"
proof(induction w rule: rev_induct)
case Nil show ?case by simp
next
case snoc thus ?case by (auto elim!: rtrancl_into_rtrancl)
qed
}
hence "((r, s), (r', s')) ∈ ?R ⟹ ((r, s), (r', s')) ∈ ?L" by auto
with x have "x ∈ ?R ⟹ x ∈ ?L" by simp
} ultimately show ?thesis by blast
qed

lemma in_fold_lQuot: "v ∈ fold lQuot w L ⟷ w @ v ∈ L"
by (induct w arbitrary: L) (simp_all add: lQuot_def)

lemma (in project) lang_eq_ext: "⟦wf n r; wf n s⟧ ⟹ (lang n r = lang n s) =
(∀w ∈ lists(Σ n). w ∈ lang n r ⟷ w ∈ lang n s)"
by (auto dest!: lang_subset_lists)

lemma (in project) lang_eq_ext_Nil_fold_Deriv:
fixes r s n
assumes WF: "wf n r" "wf n s"
defines "𝔅 ≡ {(fold lQuot w (lang n r), fold lQuot w (lang n s))| w. w∈lists (Σ n)}"
shows "lang n r = lang n s ⟷ (∀(K, L) ∈ 𝔅. [] ∈ K ⟷ [] ∈ L)"
unfolding lang_eq_ext[OF WF] 𝔅_def
by (subst (1 2) in_fold_lQuot[of "[]", simplified, symmetric]) auto

locale rexp_DA = project "set o σ" wf_atom project lookup
for σ :: "nat ⇒ 'a list"
and wf_atom :: "nat ⇒ 'b :: linorder ⇒ bool"
and project :: "'a ⇒ 'a"
and lookup :: "'b ⇒ 'a ⇒ bool" +
fixes init :: "'b rexp ⇒ 's"
fixes delta :: "'a ⇒ 's ⇒ 's"
fixes final :: "'s ⇒ bool"
fixes wf_state :: "'s ⇒ bool"
fixes post :: "'s ⇒ 's"
fixes L :: "'s ⇒ 'a lang"
fixes n :: "nat"
assumes L_init[simp]: "wf n r ⟹ L (init r) = lang n r"
assumes L_delta[simp]: "⟦a ∈ set (σ n); wf_state s⟧ ⟹ L (delta a s) = lQuot a (L s)"
assumes final_iff_Nil[simp]: "final s ⟷ [] ∈ L s"
assumes L_wf_state[dest]: "wf_state s ⟹ L s ⊆ lists (set (σ n))"
assumes init_wf_state[simp]: "wf n r ⟹ wf_state (init r)"
assumes delta_wf_state[simp]: "⟦a ∈ set (σ n); wf_state s⟧ ⟹ wf_state (delta a s)"
assumes L_post[simp]: "wf_state s ⟹ L (post s) = L s"
assumes wf_state_post[simp]: "wf_state s ⟹ wf_state (post s)"
begin

lemma L_deltas[simp]: "⟦wf_word n w; wf_state s⟧ ⟹ L (fold delta w s) = fold lQuot w (L s)"
by (induction w arbitrary: s) auto

definition progression (infix "→" 60) where
"R → S = (∀s1 s2. R s1 s2 ⟶ wf_state s1 ∧ wf_state s2 ∧ final s1 = final s2 ∧
(∀x ∈ set (σ n). BNF_Greatest_Fixpoint.image2p post post S (post (delta x s1)) (post (delta x s2))))"

lemma SUPR_progression[intro!]: "∀n. ∃m. X n → Y m ⟹ (SUP n. X n) → (SUP n. Y n)"
unfolding progression_def image2p_def by fastforce

definition bisimulation where
"bisimulation R = R → R"

definition bisimulation_upto where
"bisimulation_upto R f = R → f R"

declare image2pI[intro!] image2pE[elim!]
lemmas bisim_def = bisimulation_def progression_def
lemmas bisim_upto_def = bisimulation_upto_def progression_def

definition compatible where
"compatible f = (mono f ∧ (∀R S. R → S ⟶ f R → f S))"

lemmas compat_def = compatible_def progression_def

lemma bisimulation_upto_bisimulation:
assumes "compatible f" "bisimulation_upto R f"
obtains S where "bisimulation S" "R ≤ S"
proof
{ fix n from assms have "(f^^n) R → (f^^Suc n) R"
by (induct n) (auto simp: bisimulation_upto_def compatible_def) }
then show "bisimulation (SUP n. (f^^n) R)"
unfolding bisimulation_def by (auto simp del: funpow.simps)
show "R ≤ (SUP n. (f^^n) R)" by (auto intro!: exI[of _ 0])
qed

lemma bisimulation_eqL: "bisimulation (λs1 s2. wf_state s1 ∧ wf_state s2 ∧ L s1 = L s2)"
unfolding bisim_def by (auto simp: lQuot_def)

lemma coinduction:
assumes bisim[unfolded bisim_def]: "bisimulation R" and
WF: "wf_state s1" "wf_state s2" and R: "R s1 s2"
shows "L s1 = L s2"
proof (rule set_eqI)
fix w
from R WF show "w ∈ L s1 ⟷ w ∈ L s2"
proof (induction w arbitrary: s1 s2)
case Nil then show ?case using bisim by simp
next
case (Cons a w s1 s2)
show ?case
proof cases
assume a: "a ∈ set (σ n)"
with ‹R s1 s2› obtain s1' s2' where "R s1' s2'" "wf_state s1'" "wf_state s2'" and
*[symmetric]: "post s1' = post (delta a s1)"  "post s2' = post (delta a s2)"
using bisim unfolding image2p_apply by blast
then have "w ∈ L (post (delta a s1)) ⟷ w ∈ L (post (delta a s2))"
unfolding * using Cons.IH[of s1' s2'] by simp
with a Cons.prems(2,3) show ?case by (simp add: lQuot_def)
next
assume "a ∉ set (σ n)"
thus ?case using Cons.prems bisim by force
qed
qed
qed

lemma coinduction_upto:
assumes "bisimulation_upto R f" and WF: "wf_state s1" "wf_state s2" and "R s1 s2" "compatible f"
shows "L s1 = L s2"
proof (rule bisimulation_upto_bisimulation[OF assms(5,1)])
fix S assume "R ≤ S"
assume "bisimulation S"
then show "L s1 = L s2"
proof (rule coinduction[OF _ WF])
from ‹R ≤ S› ‹R s1 s2› show "S s1 s2" by blast
qed
qed

fun test_invariant where
"test_invariant (ws, _ :: ('s × 's) list , _ :: 's rel) = (case ws of [] ⇒  False | (w::'a list,p,q)#_ ⇒ final p = final q)"
fun test where "test (ws, _ :: 's rel) = (case ws of [] ⇒  False | (p,q)#_ ⇒ final p = final q)"

fun step_invariant where "step_invariant (ws, ps, N) =
(let
(w, r, s) = hd ws;
ps' = (r, s) # ps;
succs = map (λa.
let r' = delta a r; s' = delta a s
in ((a # w, r', s'), (post r', post s'))) (σ n);
new = remdups' snd (filter (λ(_, rs). rs ∉ N) succs);
ws' = tl ws @ map fst new;
N' = set (map snd new) ∪ N
in (ws', ps', N'))"

fun step where "step (ws, N) =
(let
(r, s) = hd ws;
succs = map (λa.
let r' = delta a r; s' = delta a s
in ((r', s'), (post r', post s'))) (σ n);
new = remdups' snd (filter (λ(_, rs). rs ∉ N) succs)
in (tl ws @ map fst new, set (map snd new) ∪ N))"

definition closure_invariant where "closure_invariant = while_option test_invariant step_invariant"
definition closure where "closure = while_option test step"

definition invariant where
"invariant r s = (λ(ws, ps, N).
(r, s) ∈ snd ` set ws ∪ set ps ∧
distinct (map snd ws @ ps) ∧
bij_betw (map_prod post post) (set (map snd ws @ ps)) N ∧
(∀(w, r', s') ∈ set ws. fold delta (rev w) r = r' ∧ fold delta (rev w) s = s' ∧
wf_word n (rev w) ∧ wf_state r' ∧ wf_state s') ∧
(∀(r', s') ∈ set ps. (∃w. fold delta w r = r' ∧ fold delta w s = s') ∧
wf_state r' ∧ wf_state s' ∧ (final r' ⟷ final s') ∧
(∀a∈set (σ n). (post (delta a r'), post (delta a s')) ∈ N)))"

lemma invariant_start:
"⟦wf_state r; wf_state s⟧ ⟹ invariant r s ([([], r, s)], [], {(post r, post s)})"
by (auto simp add: invariant_def bij_betw_def)

lemma step_invariant_mono:
assumes "step_invariant (ws, ps, N) = (ws', ps', N')"
shows "snd ` set ws ∪ set ps ⊆ snd ` set ws' ∪ set ps'"
using assms proof (intro subsetI, elim UnE)
fix x assume "x ∈ snd `set ws"
with assms show "x ∈ snd ` set ws' ∪ set ps'"
proof (cases "x = snd (hd ws)")
case False with ‹x ∈ image snd (set ws)› have "x ∈ snd ` set (tl ws)" by (cases ws) auto
with assms show ?thesis by (auto split: prod.splits simp: Let_def)
qed (auto split: prod.splits simp: Let_def)
qed (auto split: prod.splits simp: Let_def)

lemma step_invatiant_unfold: "step_invariant (w # ws, ps, N) = (ws', ps', N') ⟹ (∃xs r s.
w = (xs, r, s) ∧ ps' = (r, s) # ps ∧
ws' = ws @ remdups' (map_prod post post o snd) (filter (λ(_, p). map_prod post post p ∉ N)
(map (λa. (a#xs, delta a r, delta a s)) (σ n))) ∧
N' = set (map (λa. (post (delta a r), post (delta a s))) (σ n)) ∪ N)"
by (auto split: prod.splits dest!: mp_remdups'
simp: Let_def filter_map set_n_lists image_Collect image_image comp_def)

lemma invariant: "invariant r s st ⟹ test_invariant st ⟹ invariant r s (step_invariant st)"
proof (unfold invariant_def, (split prod.splits)+, elim case_prodE conjE, clarify, intro allI impI conjI)
fix ws ps N ws' ps' N'
assume test_invariant: "test_invariant (ws, ps, N)"
and step_invariant: "step_invariant (ws, ps, N) = (ws', ps', N')"
and rs: "(r, s) ∈ snd ` set ws ∪ set ps"
and distinct: "distinct (map snd ws @ ps)"
and bij: "bij_betw (map_prod post post) (set (map snd ws @ ps)) N"
and ws: "∀(w, r', s') ∈ set ws. fold delta (rev w) r = r' ∧ fold delta (rev w) s = s' ∧
wf_word n (rev w) ∧ wf_state r' ∧ wf_state s'"
(is "∀(w, r', s') ∈ set ws. ?ws w r' s'")
and ps: "∀(r', s') ∈ set ps. (∃w. fold delta w r = r' ∧ fold delta w s = s') ∧
wf_state r' ∧ wf_state s' ∧ (final r' ⟷ final s') ∧
(∀a∈set (σ n). (post (delta a r'), post (delta a s')) ∈ N)"
(is "∀(r, s) ∈ set ps. ?ps r s N")
from test_invariant obtain x xs where ws_Cons: "ws = x # xs" by (cases ws) auto
obtain w r' s' where x: "x = (w, r', s')" and ps': "ps' = (r', s') # ps"
and ws': "ws' = xs @ remdups' (map_prod post post o snd)
(filter (λ(_, p). map_prod post post p ∉ N)
(map (λa. (a # w, delta a r',  delta a s')) (σ n)))"
and N': "N' = (set (map (λa. (post (delta a r'), post (delta a s'))) (σ n)) - N) ∪ N"
using step_invatiant_unfold[OF step_invariant[unfolded ws_Cons]] by blast
hence ws'ps': "set (map snd ws' @ ps') =
set (remdups' (map_prod post post) (filter (λp. map_prod post post p ∉ N)
(map (λa. (delta a r',  delta a s')) (σ n)))) ∪ (set (map snd ws @ ps))"
unfolding ws' ps' ws_Cons x by (auto dest!: mp_remdups' simp: filter_map image_image image_Un o_def)
from rs step_invariant show "(r, s) ∈ snd ` set ws' ∪ set ps'" by (blast dest: step_invariant_mono)
(*next*)
from distinct ps' ws' ws_Cons x bij show "distinct (map snd ws' @ ps')"
by (auto simp: bij_betw_def
intro!: imageI[of _ _ "map_prod post post"] distinct_remdups'_strong
map_prod_imageI[of _ _ _ post post]
dest!: mp_remdups'
elim: image_eqI[of _ snd, OF sym[OF snd_conv]])
(*next*)
from ps' ws' N' ws x bij show "bij_betw (map_prod post post) (set (map snd ws' @ ps')) N'"
unfolding ws'ps' N' by (intro bij_betw_combine[OF _ bij]) (auto simp: bij_betw_def map_prod_def)
(*next*)
from ws x ws_Cons have wr's': "?ws w r' s'" by auto
with ws ws_Cons show "∀(w, r', s') ∈ set ws'. ?ws w r' s'" unfolding ws'
by (auto dest!: mp_remdups' elim!: subsetD)
(*next*)
from ps wr's' test_invariant[unfolded ws_Cons x] show "∀(r', s') ∈ set ps'. ?ps r' s' N'" unfolding ps' N'
by (fastforce simp: image_Collect)
qed

lemma step_commute: "ws ≠ [] ⟹
(case step_invariant (ws, ps, N) of (ws', ps', N') ⇒ (map snd ws', N')) = step (map snd ws, N)"
apply (auto split: prod.splits)
apply (auto simp only: step_invariant.simps step.simps Let_def map_apfst_remdups' filter_map list.map_comp apfst_def map_prod_def snd_conv id_def)
apply (auto simp: filter_map comp_def map_tl hd_map)
apply (intro image_eqI, auto)+
done

lemma closure_invariant_closure:
"map_option (λ(ws, ps, N). (map snd ws, N)) (closure_invariant (ws, ps, N)) = closure (map snd ws, N)"
unfolding closure_invariant_def closure_def
by (rule trans[OF while_option_commute[of _ test _ _ "step"]])
(auto split: list.splits simp del: step_invariant.simps step.simps list.map simp: step_commute)

lemma
assumes result: "closure_invariant ([([], init r, init s)], [], {(post (init r), post (init s))}) =
Some(ws, ps, N)" (is "closure_invariant ([([], ?r, ?s)], _) = _")
and WF: "wf n r" "wf n s"
shows closure_invariant_sound: "ws = [] ⟹ lang n r = lang n s" and
counterexample: "ws ≠ [] ⟹ rev (fst (hd ws)) ∈ lang n r ⟷ rev (fst (hd ws)) ∉ lang n s"
proof -
from WF have wf_state: "wf_state ?r" "wf_state ?s" by simp_all
from invariant invariant_start[OF wf_state] have invariant_ps: "invariant ?r ?s (ws, ps, N)"
by (rule while_option_rule[OF _ result[unfolded closure_invariant_def]])
{ assume "ws = []"
with invariant_ps have "bisimulation (in_rel (set ps))" "(?r, ?s) ∈ set ps"
by (auto simp: bij_betw_def invariant_def bisimulation_def progression_def image2p_in_rel)
with wf_state have "L ?r = L ?s" by (auto dest: coinduction)
with WF show "lang n r = lang n s" by simp
}
{ assume "ws ≠ []"
then obtain w r' s' ws' where ws: "ws = (w, r', s') # ws'" by (cases ws) auto
with invariant_ps have "r' = fold delta (rev w) (init r)" "s' = fold delta (rev w) (init s)"
"wf_word n (rev w)" unfolding invariant_def by auto
moreover have "¬ test_invariant ((w, r', s') # ws', ps, N)"
by (rule while_option_stop[OF result[unfolded ws closure_invariant_def]])
ultimately have "rev (fst (hd ws)) ∈ L ?r ⟷ rev (fst (hd ws)) ∉ L ?s"
unfolding ws using wf_state by (simp add: in_fold_lQuot)
with WF show "rev (fst (hd ws)) ∈ lang n r ⟷ rev (fst (hd ws)) ∉ lang n s" by simp
}
qed

lemma closure_sound:
assumes result: "closure ([(init r, init s)], {(post (init r), post (init s))}) = Some ([], N)"
and WF: "wf n r" "wf n s"
shows "lang n r = lang n s"
using trans[OF closure_invariant_closure[of "[([], init r, init s)]", simplified] result]
by (auto dest: closure_invariant_sound[OF _ WF])

definition check_eqv where
"check_eqv r s =
(let r' = init r; s' = init s in (case closure ([(r', s')], {(post r', post s')}) of
Some ([], _) ⇒ True | _ ⇒ False))"

lemma check_eqv_sound:
assumes "check_eqv r s" and WF: "wf n r" "wf n s"
shows "lang n r = lang n s"
using closure_sound assms
by (auto simp: check_eqv_def Let_def split: option.splits list.splits)

definition counterexample where
"counterexample r s =
(let r' = init r; s' = init s in (case closure_invariant ([([], r', s')], [], {(post r', post s')}) of
Some((w,_,_) # _, _) ⇒ Some (rev w) | _ => None))"

lemma counterexample_sound:
assumes result: "counterexample r s = Some w"  and WF: "wf n r" "wf n s"
shows "w ∈ lang n r ⟷ w ∉ lang n s"
using assms unfolding counterexample_def Let_def
by (auto dest!: counterexample[of r s] split: option.splits list.splits)

text‹Auxiliary exacutable functions:›

definition reachable :: "'b rexp ⇒ 's set" where
"reachable s = snd (the (rtrancl_while (λ_. True) (λs. map (λa. post (delta a s)) (σ n)) (init s)))"

definition automaton :: "'b rexp ⇒ (('s * 'a) * 's) set" where
"automaton s =
snd (the
(let i = init s;
start = (([i], {post i}), {});
test_invariant = λ((ws, Z), A). ws ≠ [];
step_invariant = λ((ws, Z), A).
(let s = hd ws;
new_edges = map (λa. ((s, a), delta a s)) (σ n);
new = remdups (filter (λss. post ss ∉ Z) (map snd new_edges))
in ((new @ tl ws, post ` set new ∪ Z), set new_edges ∪ A))
in while_option test_invariant step_invariant start))"

definition match :: "'b rexp ⇒ 'a list ⇒ bool" where
"match s w = final (fold delta w (init s))"

lemma match_correct: "⟦wf_word n w; wf n s⟧ ⟹ match s w ⟷ w ∈ lang n s"
unfolding match_def
by (induct w arbitrary: s) (auto simp: in_fold_lQuot lQuot_def)

end

locale rexp_DFA = rexp_DA σ wf_atom project lookup init delta final wf_state post L n
for σ :: "nat ⇒ 'a list"
and wf_atom :: "nat ⇒ 'b :: linorder ⇒ bool"
and project :: "'a ⇒ 'a"
and lookup :: "'b ⇒ 'a ⇒ bool"
and init :: "'b rexp ⇒ 's"
and delta :: "'a ⇒ 's ⇒ 's"
and final :: "'s ⇒ bool"
and wf_state :: "'s ⇒ bool"
and post :: "'s ⇒ 's"
and L :: "'s ⇒ 'a lang"
and n :: nat +
assumes fin: "finite {fold delta w (init s) | w. True}"
begin

abbreviation "Reachable s ≡ {fold delta w (init s) | w. True}"

lemma closure_invariant_termination:
assumes WF: "wf n r" "wf n s"
and result: "closure_invariant ([([], init r, init s)], [], {(post (init r), post (init s))}) = None"
(is "closure_invariant ([([], ?r, ?s)], _) = None" is "?cl = None")
shows "False"
proof -
let ?D =  "post ` Reachable r × post ` Reachable s"
let ?X = "λps. ?D - map_prod post post ` set ps"
let ?f = "λ(ws, ps, N). card (?X ps)"
have "∃st. ?cl = Some st" unfolding closure_invariant_def
proof (rule measure_while_option_Some[of "invariant ?r ?s" _ _ ?f], intro conjI)
fix st assume base: "invariant ?r ?s st" and "test_invariant st"
hence step: "invariant ?r ?s (step_invariant st)" by (rule invariant)
obtain ws ps N where st: "st = (ws, ps, N)" by (cases st) blast
hence "finite (?X ps)" by (blast intro: finite_cartesian_product fin)
moreover obtain ws' ps' N' where step_invariant: "step_invariant (ws, ps, N) = (ws', ps', N')"
by (cases "step_invariant (ws, ps, N)") blast
moreover
{ have "map_prod post post ` set ps ⊆ ?D" using base[unfolded st invariant_def] by fast
moreover
have "map_prod post post ` set ps' ⊆ ?D" using step[unfolded st step_invariant invariant_def]
by fast
moreover
{ have "distinct (map snd ws @ ps)" "inj_on (map_prod post post) (set (map snd ws @ ps))"
using base[unfolded st invariant_def] by (auto simp: bij_betw_def)
hence "distinct (map (map_prod post post) (map snd ws @ ps))" unfolding distinct_map ..
hence "map_prod post post ` set ps ⊂ map_prod post post ` set (snd (hd ws) # ps)"
using ‹test_invariant st› st by (cases ws) (simp_all, blast)
moreover have "map_prod post post ` set ps' = map_prod post post ` set (snd (hd ws) # ps)"
using step_invariant by (auto split: prod.splits)
ultimately have "map_prod post post ` set ps ⊂ map_prod post post ` set ps'" by simp
}
ultimately have "?X ps' ⊂ ?X ps" by (auto simp add: image_set simp del: set_map)
}
ultimately show "?f (step_invariant st) < ?f st" unfolding st step_invariant
using psubset_card_mono[of "?X ps" "?X ps'"] by simp
qed (auto simp add: invariant_start WF invariant)
then show False using result by auto
qed

lemma closure_termination:
assumes WF: "wf n r" "wf n s"
and result: "closure ([(init r, init s)], {(post (init r), post (init s))}) = None"
shows "False"
using trans[OF closure_invariant_closure[of "[([], init r, init s)]", simplified] result]
by (auto intro: closure_invariant_termination[OF WF])

lemma closure_invariant_complete:
assumes eq: "lang n r = lang n s"
and WF:  "wf n r" "wf n s"
shows "∃ps N. closure_invariant ([([], init r, init s)], [], {(post (init r), post (init s))}) =
Some([], ps, N)" (is "∃_ _. closure_invariant ([([], ?r, ?s)], _) = _" is "∃_ _. ?cl = _")
proof (cases ?cl)
case (Some st)
moreover obtain ws ps N where ws_ps_N: "st = (ws, ps, N)" by (cases st) blast
ultimately show ?thesis
proof (cases ws)
case (Cons wrs ws)
with Some obtain w where "counterexample r s = Some w" unfolding counterexample_def
by (cases wrs) (auto simp: ws_ps_N)
with eq counterexample_sound[OF _ WF] show ?thesis by blast
qed blast
qed (auto intro: closure_invariant_termination[OF WF])

lemma closure_complete:
assumes "lang n r = lang n s" "wf n r" "wf n s"
shows "∃N. closure ([(init r, init s)], {(post (init r), post (init s))}) = Some ([], N)"
using closure_invariant_complete[OF assms]
by (subst closure_invariant_closure[of "[([], init r, init s)]", simplified, symmetric]) auto

lemma check_eqv_complete:
assumes "lang n r = lang n s" "wf n r" "wf n s"
shows "check_eqv r s"
using closure_complete[OF assms] by (auto simp: check_eqv_def)

lemma counterexample_complete:
assumes "lang n r ≠ lang n s" and WF: "wf n r" "wf n s"
shows "∃w. counterexample r s = Some w"
using closure_invariant_sound[OF _ WF] closure_invariant_termination[OF WF] assms
by (fastforce simp: counterexample_def Let_def split: option.splits list.splits)

end

locale rexp_DA_no_post = rexp_DA σ wf_atom project lookup init delta final wf_state id L n
for σ :: "nat ⇒ 'a list"
and wf_atom :: "nat ⇒ 'b :: linorder ⇒ bool"
and project :: "'a ⇒ 'a"
and lookup :: "'b ⇒ 'a ⇒ bool"
and init :: "'b rexp ⇒ 's"
and delta :: "'a ⇒ 's ⇒ 's"
and final :: "'s ⇒ bool"
and wf_state :: "'s ⇒ bool"
and L :: "'s ⇒ 'a lang"
and n :: nat
begin

lemma step_efficient[code]: "step (ws, N) =
(let
(r, s) = hd ws;
new = remdups (filter (λ(r,s). (r,s) ∉ N) (map (λa. (delta a r, delta a s)) (σ n)))
in (tl ws @ new, set new ∪ N))"
by (force simp: Let_def map_apfst_remdups' filter_map o_def split: prod.splits)

end

locale rexp_DFA_no_post = rexp_DFA σ wf_atom project lookup init delta final wf_state id L
for σ :: "nat ⇒ 'a list"
and wf_atom :: "nat ⇒ 'b :: linorder ⇒ bool"
and project :: "'a ⇒ 'a"
and lookup :: "'b ⇒ 'a ⇒ bool"
and init :: "'b rexp ⇒ 's"
and delta :: "'a ⇒ 's ⇒ 's"
and final :: "'s ⇒ bool"
and wf_state :: "'s ⇒ bool"
and L :: "'s ⇒ 'a lang"
begin

sublocale rexp_DA_no_post by unfold_locales

end

locale rexp_DA_sim = project "set o σ" wf_atom project lookup
for σ :: "nat ⇒ 'a list"
and wf_atom :: "nat ⇒ 'b :: linorder ⇒ bool"
and project :: "'a ⇒ 'a"
and lookup :: "'b ⇒ 'a ⇒ bool" +
fixes init :: "'b rexp ⇒ 's"
fixes sim_delta :: "'s ⇒ 's list"
fixes final :: "'s ⇒ bool"
fixes wf_state :: "'s ⇒ bool"
fixes L :: "'s ⇒ 'a lang"
fixes post :: "'s ⇒ 's"
fixes n :: nat
assumes L_init[simp]: "wf n r ⟹ L (init r) = lang n r"
assumes final_iff_Nil[simp]: "final s ⟷ [] ∈ L s"
assumes L_wf_state[dest]: "wf_state s ⟹ L s ⊆ lists (set (σ n))"
assumes init_wf_state[simp]: "wf n r ⟹ wf_state (init r)"
assumes L_post[simp]: "wf_state s ⟹ L (post s) = L s"
assumes wf_state_post[simp]: "wf_state s ⟹ wf_state (post s)"
assumes L_sim_delta[simp]: "wf_state s ⟹ map L (sim_delta s) = map (λa. lQuot a (L s)) (σ n)"
assumes sim_delta_wf_state[simp]: "wf_state s ⟹ ∀s' ∈ set (sim_delta s). wf_state s'"
begin

definition "delta a s = sim_delta s ! index (σ n) a"

lemma length_sim_delta[simp]: "wf_state s ⟹ length (sim_delta s) = length (σ n)"
by (metis L_sim_delta length_map)

lemma L_delta[simp]: "⟦a ∈ set (σ n); wf_state s⟧ ⟹ L (delta a s) = lQuot a (L s)"
using L_sim_delta[of s] unfolding delta_def in_set_conv_nth
by (subst (asm) list_eq_iff_nth_eq) auto

lemma delta_wf_state[simp]: "⟦a ∈ set (σ n); wf_state s⟧ ⟹ wf_state (delta a s)"
unfolding delta_def by (auto intro: bspec[OF sim_delta_wf_state nth_mem])

sublocale rexp_DA σ wf_atom project lookup init delta final wf_state post L
by unfold_locales auto

sublocale rexp_DA_sim_no_post: rexp_DA_no_post σ wf_atom project lookup init delta final wf_state L
by unfold_locales auto

end

(*<*)
end
(*>*)
```