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
(*>*)