# Theory DFS

(*  Title:      Presburger-Automata/DFS.thy
Author:     Toshiaki Nishihara and Yasuhiko Minamide
Author:     Stefan Berghofer and Alex Krauss, TU Muenchen, 2008-2009
*)

section ‹Depth First Search›

theory DFS
imports Main
begin

definition "succsr succs = {(x, y). y ∈ set (succs x)}"

partial_function (tailrec) gen_dfs
where
"gen_dfs succs ins memb S wl =
(case wl of
[] ⇒ S
| x # xs ⇒
if memb x S then gen_dfs succs ins memb S xs
else gen_dfs succs ins memb (ins x S) (succs x @ xs))"

lemma gen_dfs_simps[simp]:
"gen_dfs succs ins memb S [] = S"
"gen_dfs succs ins memb S (x # xs) =
(if memb x S then gen_dfs succs ins memb S xs
else gen_dfs succs ins memb (ins x S) (succs x @ xs))"
by (simp_all add: gen_dfs.simps)

locale DFS =
fixes succs :: "'a ⇒ 'a list"
and is_node :: "'a ⇒ bool"
and invariant :: "'b ⇒ bool"
and ins :: "'a ⇒ 'b ⇒ 'b"
and memb :: "'a ⇒ 'b ⇒ bool"
and empt :: 'b
assumes ins_eq: "⋀x y S. is_node x ⟹ is_node y ⟹ invariant S ⟹ ¬ memb y S ⟹
memb x (ins y S) = ((x = y) ∨ memb x S)"
and empt: "⋀x. is_node x ⟹ ¬ memb x empt"
and succs_is_node: "⋀x. is_node x ⟹ list_all is_node (succs x)"
and empt_invariant: "invariant empt"
and ins_invariant: "⋀x S. is_node x ⟹ invariant S ⟹ ¬ memb x S ⟹ invariant (ins x S)"
and graph_finite: "finite {x. is_node x}"
begin

definition rel where
"rel = inv_image finite_psubset (λS. {n. is_node n ∧ ¬ memb n S})"

abbreviation "dfs ≡ gen_dfs succs ins memb"

lemma dfs_induct [consumes 2, case_names base step]:
assumes S: "invariant S"
and xs: "list_all is_node xs"
and I1: "⋀S. invariant S ⟹ P S []"
and I2: "⋀S x xs. invariant S ⟹ is_node x ⟹ list_all is_node xs ⟹
(memb x S ⟹ P S xs) ⟹ (¬ memb x S ⟹ P (ins x S) (succs x @ xs)) ⟹ P S (x # xs)"
shows "P S xs" using I1 I2 S xs
apply induction_schema
apply atomize_elim
apply (case_tac xs, simp+)
apply atomize_elim
apply (rule conjI)
apply (rule ins_invariant, assumption+)
apply (rule succs_is_node, assumption)
apply (relation "rel <*lex*> measure length")
apply (simp add: wf_lex_prod rel_def)
apply simp
apply simp
apply (rule disjI1)
apply (simp add: rel_def finite_psubset_def)
apply (rule conjI)
apply (auto simp add: ins_eq graph_finite cong: conj_cong)
done

definition "succss xs = (⋃x∈xs. set (succs x))"

definition "set_of S = {x. is_node x ∧ memb x S}"

definition "reachable xs = {(x, y). y ∈ set (succs x)}⇧*  xs"

lemma visit_subset_dfs: "invariant S ⟹ list_all is_node xs ⟹
is_node y ⟹ memb y S ⟹ memb y (dfs S xs)"
by (induct S xs rule: dfs_induct) (simp_all add: ins_eq)

lemma next_subset_dfs: "invariant S ⟹ list_all is_node xs ⟹
x ∈ set xs ⟹ memb x (dfs S xs)"
proof (induct S xs rule: dfs_induct)
case base
then show ?case by simp
next
case (step S y xs)
then show ?case
by (auto simp add: visit_subset_dfs ins_eq ins_invariant succs_is_node)
qed

lemma succss_closed_dfs':
"invariant ys ⟹ list_all is_node xs ⟹
succss (set_of ys) ⊆ set xs ∪ set_of ys ⟹
succss (set_of (dfs ys xs)) ⊆ set_of (dfs ys xs)"
by (induct ys xs rule: dfs_induct)
(auto simp add: ins_eq succss_def set_of_def cong: conj_cong)

lemma succss_closed_dfs: "list_all is_node xs ⟹
succss (set_of (dfs empt xs)) ⊆ set_of (dfs empt xs)"
apply (rule succss_closed_dfs')
apply (rule empt_invariant)
apply assumption
apply (simp add: succss_def)
apply (rule subsetI)
apply (erule UN_E)
apply (simp add: set_of_def empt cong: conj_cong)
done

lemma Image_closed_trancl: assumes "r  X ⊆ X" shows "r⇧*  X = X"
proof
show "X ⊆ r⇧*  X" by auto
show "r⇧*  X ⊆ X"
proof -
{ fix x y
assume y: "y ∈ X"
assume "(y,x) ∈ r⇧*"
then have "x ∈ X" using assms y
by induct (auto simp add: Image_def)
} then show ?thesis by auto
qed
qed

lemma reachable_closed_dfs:
assumes "list_all is_node xs"
shows "reachable (set xs) ⊆ set_of (dfs empt xs)"
proof -
from assms have "reachable (set xs) ⊆ reachable (set_of (dfs empt xs))"
apply (unfold reachable_def)
apply (rule Image_mono)
apply (auto simp add: set_of_def next_subset_dfs empt_invariant list_all_iff)
done
also from succss_closed_dfs assms have "… = set_of (dfs empt xs)"
apply (unfold reachable_def)
apply (rule Image_closed_trancl)
apply (auto simp add: succss_def set_of_def)
done
finally show ?thesis .
qed

lemma reachable_succs: "reachable (set (succs x)) ⊆ reachable {x}"
by (auto simp add: reachable_def intro: converse_rtrancl_into_rtrancl)

lemma dfs_subset_reachable_visit_nodes:
"invariant ys ⟹ list_all is_node xs ⟹
set_of (dfs ys xs) ⊆ reachable (set xs) ∪ set_of ys"
proof (induct ys xs rule: dfs_induct)
case base
then show ?case by (simp add: reachable_def)
next
case (step S x xs)
show ?case
proof (cases "memb x S")
case True
with step show ?thesis
by (auto simp add: reachable_def)
next
case False
have "reachable (set (succs x)) ⊆ reachable {x}"
by (rule reachable_succs)
then have "reachable (set (succs x @ xs)) ⊆ reachable (set (x # xs))"
by (auto simp add: reachable_def)
then show ?thesis using step
by (auto simp add: reachable_def ins_eq set_of_def cong: conj_cong)
qed
qed

theorem dfs_eq_reachable:
assumes y: "is_node y"
and xs: "list_all is_node xs"
shows "memb y (dfs empt xs) = (y ∈ reachable (set xs))"
proof
assume "memb y (dfs empt xs)"
with dfs_subset_reachable_visit_nodes [OF empt_invariant xs] y
show "y ∈ reachable (set xs)"
by (auto simp add: empt set_of_def)
next
assume "y ∈ reachable (set xs)"
with reachable_closed_dfs [OF xs] show "memb y (dfs empt xs)"
by (auto simp add: set_of_def)
qed

theorem dfs_eq_rtrancl:
assumes y: "is_node y"
and x: "is_node x"
shows "memb y (dfs empt [x]) = ((x,y) ∈ (succsr succs)⇧*)"
proof -
from x have x': "list_all is_node [x]" by simp
show ?thesis
by (simp only: dfs_eq_reachable [OF y x'] reachable_def succsr_def) (auto simp add: empt)
qed

theorem dfs_invariant [consumes 2, case_names base step]:
assumes S: "invariant S"
and xs: "list_all is_node xs"
and H: "I S"
and I: "⋀S x. ¬ memb x S ⟹ is_node x ⟹ invariant S ⟹ I S ⟹ I (ins x S)"
shows "I (dfs S xs)"
proof -
from S xs H
have "I (dfs S xs) ∧ invariant (dfs S xs)"
proof (induct S xs rule: dfs_induct)
case base
then show ?case by simp
next
case (step S x xs)
show ?case
proof (cases "memb x S")
case True
then show ?thesis by (simp add: step)
next
case False
then show ?thesis
apply simp
apply (rule step)
apply assumption
apply (rule I)
apply assumption
apply (rule step)+
done
qed
qed
then show ?thesis ..
qed

theorem dfs_invariant': "invariant S ⟹ list_all is_node xs ⟹ invariant (dfs S xs)"
by (induct S xs rule: dfs_induct) auto

theorem succsr_is_node:
assumes "(x, y) ∈ (succsr succs)⇧*"
shows "is_node x ⟹ is_node y" using assms
proof induct
case base
then show ?case .
next
case (step y z)
then have "is_node y" by simp
then have "list_all is_node (succs y)"
by (rule succs_is_node)
with step show ?case
by (simp add: succsr_def list_all_iff)
qed

end

declare gen_dfs_simps [simp del]

end


# Theory Presburger_Automata

(*  Title:      Presburger-Automata/Presburger_Automata.thy
Author:     Markus Reiter and Stefan Berghofer, TU Muenchen, 2008-2009
*)

theory Presburger_Automata
imports DFS "HOL-Library.Nat_Bijection"
begin

section ‹General automata›

definition
"reach tr p as q = (q = foldl tr p as)"

lemma reach_nil: "reach tr p [] p" by (simp add: reach_def)

lemma reach_snoc: "reach tr p bs q ⟹ reach tr p (bs @ [b]) (tr q b)"
by (simp add: reach_def)

lemma reach_nil_iff: "reach tr p [] q = (p = q)" by (auto simp add: reach_def)

lemma reach_snoc_iff: "reach tr p (bs @ [b]) k = (∃q. reach tr p bs q ∧ k = tr q b)"
by (auto simp add: reach_def)

lemma reach_induct [consumes 1, case_names Nil snoc, induct set: reach]:
assumes "reach tr p w q"
and "P [] p"
and  "⋀k x y. ⟦reach tr p x k; P x k⟧ ⟹ P (x @ [y]) (tr k y)"
shows "P w q"
using assms by (induct w arbitrary: q rule: rev_induct) (simp add: reach_def)+

lemma reach_trans: "⟦reach tr p a r; reach tr r b q⟧ ⟹ reach tr p (a @ b) q"
by (simp add: reach_def)

lemma reach_inj: "⟦reach tr p a q; reach tr p a q'⟧ ⟹ q = q'"
by (simp add: reach_def)

definition
"accepts tr P s as = P (foldl tr s as)"

locale Automaton =
fixes trans :: "'a ⇒ 'b ⇒ 'a"
and is_node :: "'a ⇒ bool"
and is_alpha :: "'b ⇒ bool"
assumes trans_is_node: "⋀q a. ⟦is_node q; is_alpha a⟧ ⟹ is_node (trans q a)"
begin

lemma steps_is_node:
assumes "is_node q"
and "list_all is_alpha w"
shows "is_node (foldl trans q w)"
using assms by (induct w arbitrary: q) (simp add: trans_is_node)+

lemma reach_is_node: "⟦reach trans p w q; is_node p; list_all is_alpha w⟧ ⟹ is_node q"
by (simp add: steps_is_node reach_def)

end

section ‹BDDs›

definition
is_alph :: "nat ⇒ bool list ⇒ bool" where
"is_alph n = (λw. length w = n)"

datatype 'a bdd = Leaf 'a | Branch "'a bdd" "'a bdd" for map: bdd_map

primrec bddh :: "nat ⇒ 'a bdd ⇒ bool"
where
"bddh n (Leaf x) = True"
| "bddh n (Branch l r) = (case n of 0 ⇒ False | Suc m ⇒ bddh m l ∧ bddh m r)"

lemma bddh_ge:
assumes "m ≥ n"
assumes "bddh n bdd"
shows "bddh m bdd"
using assms
proof (induct bdd arbitrary: n m)
case (Branch l r)
then obtain v where V: "n = Suc v" by (cases n) simp+
show ?case proof (cases "n = m")
case True
with Branch show ?thesis by simp
next
case False
with Branch have "∃w. m = Suc w ∧ n ≤ w" by (cases m) simp+
then obtain w where W: "m = Suc w ∧ n ≤ w" ..
with Branch V have "v ≤ w ∧ bddh v l ∧ bddh v r" by simp
with Branch have "bddh w l ∧ bddh w r" by blast
with W show ?thesis by simp
qed
qed simp

abbreviation "bdd_all ≡ pred_bdd"

fun bdd_lookup :: "'a bdd ⇒ bool list ⇒ 'a"
where
"bdd_lookup (Leaf x) bs = x"
| "bdd_lookup (Branch l r) (b#bs) = bdd_lookup (if b then r else l) bs"

lemma bdd_all_bdd_lookup: "⟦bddh (length ws) bdd; bdd_all P bdd⟧ ⟹ P (bdd_lookup bdd ws)"
by (induct bdd ws rule: bdd_lookup.induct) simp+

lemma bdd_all_bdd_lookup_iff: "bddh n bdd ⟹ bdd_all P bdd = (∀ws. length ws = n ⟶ P (bdd_lookup bdd ws))"
apply (rule iffI)
apply (simp add: bdd_all_bdd_lookup)
proof (induct bdd arbitrary: n)
case Leaf thus ?case
apply simp
apply (erule mp)
apply (rule_tac x="replicate n False" in exI, simp)
done
next
case (Branch l r n)
then obtain k where k: "n = Suc k" by (cases n) simp+
from Branch have R: "⋀ws. length ws = n ⟹ P (bdd_lookup (Branch l r) ws)" by simp
have "⋀ws. length ws = k ⟹ P (bdd_lookup l ws) ∧ P (bdd_lookup r ws)"
proof -
fix ws :: "bool list" assume H: "length ws = k"
with k have "length (False#ws) = n" by simp
hence 1: "P (bdd_lookup (Branch l r) (False#ws))" by (rule R)
from H k have "length (True#ws) = n" by simp
hence "P (bdd_lookup (Branch l r) (True#ws))" by (rule R)
with 1 show "P (bdd_lookup l ws) ∧ P (bdd_lookup r ws)" by simp
qed
with Branch k show ?case by auto
qed

lemma bdd_all_bdd_map:
assumes "bdd_all P bdd"
and "⋀a. P a ⟹ Q (f a)"
shows "bdd_all Q (bdd_map f bdd)"
using assms by (induct bdd) simp+

lemma bddh_bdd_map:
shows "bddh n (bdd_map f bdd) = bddh n bdd"
proof
assume "bddh n (bdd_map f bdd)" thus "bddh n bdd" proof (induct bdd arbitrary: n)
case (Branch l r n)
then obtain k where "n = Suc k" by (cases n) simp+
with Branch show ?case by simp
qed simp
next
assume "bddh n bdd" thus "bddh n (bdd_map f bdd)" proof (induct bdd arbitrary: n)
case (Branch l r n)
then obtain k where "n = Suc k" by (cases n) simp+
with Branch show ?case by simp
qed simp
qed

lemma bdd_map_bdd_lookup:
assumes "bddh (length ws) bdd"
shows "bdd_lookup (bdd_map f bdd) ws = f (bdd_lookup bdd ws)"
using assms by (induct bdd ws rule: bdd_lookup.induct) (auto simp add: bddh_bdd_map)+

fun bdd_binop :: "('a ⇒ 'b ⇒ 'c) ⇒ 'a bdd ⇒ 'b bdd ⇒ 'c bdd"
where
"bdd_binop f (Leaf x) (Leaf y) = Leaf (f x y)"
| "bdd_binop f (Branch l r) (Leaf y) = Branch (bdd_binop f l (Leaf y)) (bdd_binop f r (Leaf y))"
| "bdd_binop f (Leaf x) (Branch l r) = Branch (bdd_binop f (Leaf x) l) (bdd_binop f (Leaf x) r)"
| "bdd_binop f (Branch l⇩1 r⇩1) (Branch l⇩2 r⇩2) = Branch (bdd_binop f l⇩1 l⇩2) (bdd_binop f r⇩1 r⇩2)"

lemma bddh_binop: "bddh n (bdd_binop f l r) = (bddh n l ∧ bddh n r)"
by (induct f l r arbitrary: n rule: bdd_binop.induct) (auto split: nat.split_asm)

lemma bdd_lookup_binop: "⟦bddh (length bs) l; bddh (length bs) r⟧ ⟹
bdd_lookup (bdd_binop f l r) bs = f (bdd_lookup l bs) (bdd_lookup r bs)"
apply (induct f l r arbitrary: bs rule: bdd_binop.induct)
apply simp
apply (case_tac bs)
apply simp+
apply (case_tac bs)
apply simp+
apply (case_tac bs)
apply simp+
done

lemma bdd_all_bdd_binop:
assumes "bdd_all P bdd"
and "bdd_all Q bdd'"
and "⋀a b. ⟦P a; Q b⟧ ⟹ R (f a b)"
shows "bdd_all R (bdd_binop f bdd bdd')"
using assms by (induct f bdd bdd' rule: bdd_binop.induct) simp+

lemma insert_list_idemp[simp]:
"List.insert x (List.insert x xs) = List.insert x xs"
by simp

primrec add_leaves :: "'a bdd ⇒ 'a list ⇒ 'a list"
where
"add_leaves (Leaf x) xs = List.insert x xs"
| "add_leaves (Branch b c) xs = add_leaves c (add_leaves b xs)"

"bddh n b ⟹ (x ∈ set (add_leaves b xs)) = ((∃bs. x = bdd_lookup b bs ∧ is_alph n bs) ∨ x ∈ set xs)"
apply (induct b arbitrary: xs n)
apply (auto split: nat.split_asm)
apply (rule_tac x="replicate n arbitrary" in exI)
apply (simp add: is_alph_def)
apply (rule_tac x="True # bs" in exI)
apply (simp add: is_alph_def)
apply (rule_tac x="False # bs" in exI)
apply (simp add: is_alph_def)
apply (case_tac bs)
apply (simp add: is_alph_def)
apply (simp add: is_alph_def)
apply (drule_tac x=list in spec)
apply (case_tac a)
apply simp
apply simp
apply (rule_tac x=list in exI)
apply simp
done

"list_all P (add_leaves tr xs) ⟷ bdd_all P tr ∧ list_all P xs"
by (induct tr arbitrary: xs) (auto simp add: list_all_iff)

add_leaves_bdd_all_eq [where xs="[]", simplified, symmetric]

"set xs ⊆ set ys ⟹ set (add_leaves tr xs) ⊆ set (add_leaves tr ys)"
by (induct tr arbitrary: xs ys) auto

"set (add_leaves (bdd_binop f b b') [f x y. x ← xs, y ← ys]) ⊆
(⋃x∈set (add_leaves b xs). ⋃y∈set (add_leaves b' ys). {f x y})" (is "?A ⊆ ?B")
proof -
have "?A ⊆ (⋃x∈set (add_leaves b xs). f x  set (add_leaves b' ys))"
proof (induct f b b' arbitrary: xs ys rule: bdd_binop.induct)
case (1 f x y xs ys) then show ?case by auto
next
case (2 f l r y xs ys) then show ?case
apply auto
apply (drule_tac ys1="[f x y. x ← add_leaves l xs, y ← List.insert y ys]" in
rev_subsetD [OF _ add_leaves_mono])
apply auto
apply (drule meta_spec, drule meta_spec, drule subsetD, assumption)
apply simp
done
next
case (3 f x l r xs ys) then show ?case
apply auto
apply (drule_tac ys1="[f x y. x ← List.insert x xs, y ← add_leaves l ys]" in
rev_subsetD [OF _ add_leaves_mono])
apply auto
apply (drule meta_spec, drule meta_spec, drule subsetD, assumption)
apply simp
done
next
case (4 f l⇩1 r⇩1 l⇩2 r⇩2 xs ys) then show ?case
apply auto
apply (drule_tac ys1="[f x y. x ← add_leaves l⇩1 xs, y ← add_leaves l⇩2 ys]" in
rev_subsetD [OF _ add_leaves_mono])
apply simp
apply (drule meta_spec, drule meta_spec, drule subsetD, assumption)
apply simp
done
qed
also have "(⋃x∈set (add_leaves b xs). f x  set (add_leaves b' ys)) = ?B"
by auto
finally show ?thesis .
qed

section ‹DFAs›

type_synonym bddtable = "nat bdd list"
type_synonym astate = "bool list"
type_synonym dfa = "bddtable × astate"

definition
dfa_is_node :: "dfa ⇒ nat ⇒ bool" where
"dfa_is_node A = (λq. q < length (fst A))"

definition
wf_dfa :: "dfa ⇒ nat ⇒ bool" where
"wf_dfa A n =
(list_all (bddh n) (fst A) ∧
list_all (bdd_all (dfa_is_node A)) (fst A) ∧
length (snd A) = length (fst A) ∧
length (fst A) > 0)"

definition
dfa_trans :: "dfa ⇒ nat ⇒ bool list ⇒ nat" where
"dfa_trans A q bs ≡ bdd_lookup (fst A ! q) bs"
definition
dfa_accepting :: "dfa ⇒ nat ⇒ bool" where
"dfa_accepting A q = snd A ! q"

locale aut_dfa =
fixes A n
assumes well_formed: "wf_dfa A n"

sublocale aut_dfa < Automaton "dfa_trans A" "dfa_is_node A" "is_alph n"
proof
fix q a
assume Q: "dfa_is_node A q" and A: "is_alph n a"
hence QL: "q < length (fst A)" by (simp add: dfa_is_node_def)
with well_formed A have H: "bddh (length a) (fst A ! q)" by (simp add: wf_dfa_def list_all_iff is_alph_def)
from QL well_formed have "bdd_all (dfa_is_node A) (fst A ! q)" by (simp add: wf_dfa_def list_all_iff)
with H show "dfa_is_node A (dfa_trans A q a)" by (simp add: dfa_trans_def bdd_all_bdd_lookup)
qed

context aut_dfa begin
lemmas trans_is_node = trans_is_node
lemmas steps_is_node = steps_is_node
lemmas reach_is_node = reach_is_node
end

lemmas dfa_trans_is_node = aut_dfa.trans_is_node [OF aut_dfa.intro]
lemmas dfa_steps_is_node = aut_dfa.steps_is_node [OF aut_dfa.intro]
lemmas dfa_reach_is_node = aut_dfa.reach_is_node [OF aut_dfa.intro]

abbreviation "dfa_steps A ≡ foldl (dfa_trans A)"
abbreviation "dfa_accepts A ≡ accepts (dfa_trans A) (dfa_accepting A) 0"
abbreviation "dfa_reach A ≡ reach (dfa_trans A)"

lemma dfa_startnode_is_node: "wf_dfa A n ⟹ dfa_is_node A 0"
by (simp add: dfa_is_node_def wf_dfa_def)

subsection ‹Minimization›

primrec make_tr :: "(nat ⇒ 'a) ⇒ nat ⇒ nat ⇒ 'a list"
where
"make_tr f 0 i = []"
| "make_tr f (Suc n) i = f i # make_tr f n (Suc i)"

primrec fold_map_idx :: "(nat ⇒ 'c ⇒ 'a ⇒ 'c × 'b) ⇒ nat ⇒ 'c ⇒ 'a list ⇒ 'c × 'b list"
where
"fold_map_idx f i y [] = (y, [])"
| "fold_map_idx f i y (x # xs) =
(let (y', x') = f i y x in
let (y'', xs') = fold_map_idx f (Suc i) y' xs in (y'', x' # xs'))"

definition init_tr :: "dfa ⇒ bool list list" where
"init_tr = (λ(bd,as). make_tr (λi. make_tr (λj. as ! i ≠ as ! j) i 0) (length bd - 1) 1)"

definition tr_lookup :: "bool list list ⇒ nat ⇒ nat ⇒ bool" where
"tr_lookup = (λT i j. (if i = j then False else if i > j then T ! (i - 1) ! j else T ! (j - 1) ! i))"

fun check_eq :: "nat bdd ⇒ nat bdd ⇒ bool list list ⇒ bool" where
"check_eq (Leaf i) (Leaf j) T = (¬ tr_lookup T i j)" |
"check_eq (Branch l r) (Leaf i) T = (check_eq l (Leaf i) T ∧ check_eq r (Leaf i) T)" |
"check_eq (Leaf i) (Branch l r) T = (check_eq (Leaf i) l T ∧ check_eq (Leaf i) r T)" |
"check_eq (Branch l1 r1) (Branch l2 r2) T = (check_eq l1 l2 T ∧ check_eq r1 r2 T)"

definition iter :: "dfa ⇒ bool list list ⇒ bool × bool list list" where
"iter = (λ(bd,as) T. fold_map_idx (λi. fold_map_idx (λj c b.
let b' = b ∨ ¬ check_eq (bd ! i) (bd ! j) T
in (c ∨ b ≠ b', b')) 0) 1 False T)"

definition count_tr :: "bool list list ⇒ nat" where
"count_tr = foldl (foldl (λy x. if x then y else Suc y)) 0"

lemma fold_map_idx_fst_snd_eq:
assumes f: "⋀i c x. fst (f i c x) = (c ∨ x ≠ snd (f i c x))"
shows "fst (fold_map_idx f i c xs) = (c ∨ xs ≠ snd (fold_map_idx f i c xs))"
by (induct xs arbitrary: i c) (simp_all add: split_beta f)

lemma foldl_mono:
assumes f: "⋀x y y'. y < y' ⟹ f y x < f y' x" and y: "y < y'"
shows "foldl f y xs < foldl f y' xs" using y
by (induct xs arbitrary: y y') (simp_all add: f)

lemma fold_map_idx_count:
assumes f: "⋀i c x y. fst (f i c x) = (c ∨ g y (snd (f i c x)) < (g y x::nat))"
and f': "⋀i c x y. g y (snd (f i c x)) ≤ g y x"
and g: "⋀x y y'. y < y' ⟹ g y x < g y' x"
shows "fst (fold_map_idx f i c xs) =
(c ∨ foldl g y (snd (fold_map_idx f i c xs)) < foldl g y xs)"
and "foldl g y (snd (fold_map_idx f i c xs)) ≤ foldl g y xs"
proof (induct xs arbitrary: i c y)
case (Cons x xs) {
case 1
show ?case using f' [of y i c x, simplified le_eq_less_or_eq]
by (auto simp add: split_beta Cons(1) [of _ _ "g y (snd (f i c x))"] f [of _ _ _ y]
intro: less_le_trans foldl_mono g Cons)
next
case 2
show ?case using f' [of y i c x, simplified le_eq_less_or_eq]
by (auto simp add: split_beta intro: order_trans less_imp_le
intro!: foldl_mono g Cons) }
qed simp_all

lemma iter_count:
assumes eq: "(b, T') = iter (bd, as) T"
and b: "b"
shows "count_tr T' < count_tr T"
proof -
let ?f = "fold_map_idx (λi. fold_map_idx (λj c b.
let b' = b ∨ ¬ check_eq (bd ! i) (bd ! j) T
in (c ∨ b ≠ b', b')) 0) (Suc 0) False T"
from eq [symmetric] b have "fst ?f"
by (auto simp add: iter_def)
also have "fst ?f = (False ∨ count_tr (snd ?f) < count_tr T)"
unfolding count_tr_def
by (rule fold_map_idx_count foldl_mono | simp)+
finally show ?thesis
by (simp add: eq [THEN arg_cong, of snd, simplified] iter_def)
qed

function fixpt :: "dfa ⇒ bool list list ⇒ bool list list" where
"fixpt M T = (let (b, T2) = iter M T in if b then fixpt M T2 else T2)"
by auto
termination by (relation "measure (λ(M, T). count_tr T)") (auto simp: iter_count)

lemma fixpt_True[simp]: "fst (iter M T) ⟹ fixpt M T = fixpt M (snd (iter M T))"
by (simp add: split_beta)

lemma fixpt_False[simp]: "¬ (fst (iter M T)) ⟹ fixpt M T = T"
by (simp add: split_beta iter_def fold_map_idx_fst_snd_eq)

declare fixpt.simps [simp del]

lemma fixpt_induct:
assumes H: "⋀M T. (fst (iter M T) ⟹ P M (snd (iter M T))) ⟹ P M T"
shows "P M T"
proof (induct M T rule: fixpt.induct)
case (1 M T)
show ?case by (rule H) (rule 1 [OF refl prod.collapse])
qed

definition dist_nodes :: "dfa ⇒ nat ⇒ nat ⇒ nat ⇒ nat ⇒ bool" where
"dist_nodes = (λM n m p q. ∃w. length w = n ∧ list_all (is_alph m) w ∧
dfa_accepting M (dfa_steps M p w) ≠ dfa_accepting M (dfa_steps M q w))"

definition wf_tr :: "dfa ⇒ bool list list ⇒ bool" where
"wf_tr = (λM T. length T = length (fst M) - 1 ∧ (∀i < length T. length (T ! i) = i + 1))"

lemma make_tr_len: "length (make_tr f n i) = n"
by (induct n arbitrary: i) simp_all

lemma make_tr_nth: "j < n ⟹ make_tr f n i ! j = f (i + j)"
by (induct n arbitrary: i j) (auto simp add: nth_Cons')

lemma init_tr_wf: "wf_tr M (init_tr M)"
by (simp add: init_tr_def wf_tr_def split_beta make_tr_len make_tr_nth)

lemma fold_map_idx_len: "length (snd (fold_map_idx f i y xs)) = length xs"
by (induct xs arbitrary: i y) (simp_all add: split_beta)

lemma fold_map_idx_nth: "j < length xs ⟹
snd (fold_map_idx f i y xs) ! j = snd (f (i + j) (fst (fold_map_idx f i y (take j xs))) (xs ! j))"
by (induct xs arbitrary: i j y) (simp_all add: split_beta nth_Cons' take_Cons')

lemma init_tr_dist_nodes:
assumes "dfa_is_node M q" and "p < q"
shows "tr_lookup (init_tr M) q p = dist_nodes M 0 v p q"
proof -
have 1: "dist_nodes M 0 v p q = (snd M ! p ≠ snd M ! q)" by (simp add: dist_nodes_def dfa_accepting_def)
from assms have "tr_lookup (init_tr M) q p = (snd M ! p ≠ snd M ! q)"
by (auto simp add: dfa_is_node_def init_tr_def tr_lookup_def make_tr_nth split_beta)
with 1 show ?thesis by simp
qed

lemma dist_nodes_suc:
"dist_nodes M (Suc n) v p q = (∃bs. is_alph v bs ∧ dist_nodes M n v (dfa_trans M p bs) (dfa_trans M q bs))"
proof
assume "dist_nodes M (Suc n) v p q"
then obtain w where W: "length w = Suc n" and L: "list_all (is_alph v) w" and A: "dfa_accepting M (dfa_steps M p w) ≠ dfa_accepting M (dfa_steps M q w)" unfolding dist_nodes_def by blast
then obtain b bs where B: "w = b # bs" by (cases w) auto
from A have A2: "dfa_accepting M (dfa_steps M (dfa_trans M p b) bs) ≠ dfa_accepting M (dfa_steps M (dfa_trans M q b) bs)"
unfolding B by simp
with W B L show "∃bs. is_alph v bs ∧ dist_nodes M n v (dfa_trans M p bs) (dfa_trans M q bs)" by (auto simp: dist_nodes_def)
next
assume "∃bs. is_alph v bs ∧ dist_nodes M n v (dfa_trans M p bs) (dfa_trans M q bs)"
then obtain b bs where W: "length bs = n" and V: "is_alph v b" and V': "list_all (is_alph v) bs"
and A: "dfa_accepting M (dfa_steps M (dfa_trans M p b) bs) ≠ dfa_accepting M (dfa_steps M (dfa_trans M q b) bs)"
unfolding dist_nodes_def by blast
hence "dfa_accepting M (dfa_steps M p (b # bs)) ≠ dfa_accepting M (dfa_steps M q (b # bs))" by simp
moreover from W have "length (b # bs) = Suc n" by simp
moreover from V V' have "list_all (is_alph v) (b # bs)" by simp
ultimately show "dist_nodes M (Suc n) v p q" unfolding dist_nodes_def by blast
qed

lemma bdd_lookup_append:
assumes "bddh n B" and "length bs ≥ n"
shows "bdd_lookup B (bs @ w) = bdd_lookup B bs"
using assms
proof (induct B bs arbitrary: n rule: bdd_lookup.induct)
case (2 l r b bs n)
then obtain n' where N: "n = Suc n'" by (cases n) simp+
with 2 show ?case by (cases b) auto
qed simp+

lemma bddh_exists: "∃n. bddh n B"
proof (induct B)
case (Branch l r)
then obtain n m where L: "bddh n l" and R: "bddh m r" by blast
with bddh_ge[of n "max n m" l] bddh_ge[of m "max n m" r] have "bddh (Suc (max n m)) (Branch l r)" by simp
thus ?case by (rule exI)
qed simp

lemma check_eq_dist_nodes:
assumes "∀p q. dfa_is_node M q ∧ p < q ⟶ tr_lookup T q p = (∃n < m. dist_nodes M n v p q)" and "m > 0"
and "bdd_all (dfa_is_node M) l" and "bdd_all (dfa_is_node M) r"
shows "(¬ check_eq l r T) = (∃bs. bddh (length bs) l ∧ bddh (length bs) r ∧ (∃n < m. dist_nodes M n v (bdd_lookup l bs) (bdd_lookup r bs)))"
using assms proof (induct l r T rule: check_eq.induct)
case (1 i j T)
have "i < j ∨ i = j ∨ i > j" by auto
thus ?case by (elim disjE) (insert 1, auto simp: dist_nodes_def tr_lookup_def)
next
case (2 l r i T)
hence IV1: "(¬ check_eq l (Leaf i) T) = (∃bs. bddh (length bs) l ∧ bddh (length bs) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup l bs) (bdd_lookup (Leaf i) bs)))" by simp
from 2 have IV2: "(¬ check_eq r (Leaf i) T) = (∃bs. bddh (length bs) r ∧ bddh (length bs) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup r bs) (bdd_lookup (Leaf i) bs)))" by simp
have "(¬ check_eq (Branch l r) (Leaf i) T) = (¬ check_eq l (Leaf i) T ∨ ¬ check_eq r (Leaf i) T)" by simp
also have "… = (∃bs. bddh (length bs) (Branch l r) ∧ bddh (length bs) (Leaf i) ∧ (∃n<m . dist_nodes M n v (bdd_lookup (Branch l r) bs) (bdd_lookup (Leaf i) bs)))" (is "(?L ∨ ?R) = ?E")
proof
assume "?L ∨ ?R"
thus "?E" proof (elim disjE)
assume "?L"
then obtain bs where O: "bddh (length bs) l ∧ bddh (length bs) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup l bs) (bdd_lookup (Leaf i) bs))" unfolding IV1 by blast
from bddh_exists obtain k where B: "bddh k r" by blast
with O have "bddh (length bs + k) r" and "bddh (length bs + k) l" and "bddh (length bs + k) (Leaf i)" by (simp add: bddh_ge[of k "length bs + k"] bddh_ge[of "length bs" "length bs + k"])+
with O have "bddh (length (False # bs @ replicate k False)) (Branch l r) ∧ bddh (length (False # bs @ replicate k False)) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Branch l r) (False # bs @ replicate k False)) (bdd_lookup (Leaf i) (False # bs @ replicate k False)))" by (auto simp: bdd_lookup_append)
thus ?thesis by (rule exI)
next
assume "?R"
then obtain bs where O: "bddh (length bs) r ∧ bddh (length bs) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup r bs) (bdd_lookup (Leaf i) bs))" unfolding IV2 by blast
from bddh_exists obtain k where B: "bddh k l" by blast
with O have "bddh (length bs + k) l" and "bddh (length bs + k) r" and "bddh (length bs + k) (Leaf i)" by (simp add: bddh_ge[of k "length bs + k"] bddh_ge[of "length bs" "length bs + k"])+
with O have "bddh (length (True # bs @ replicate k False)) (Branch l r) ∧ bddh (length (True # bs @ replicate k False)) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Branch l r) (True # bs @ replicate k False)) (bdd_lookup (Leaf i) (True # bs @ replicate k False)))" by (auto simp: bdd_lookup_append)
thus ?thesis by (rule exI)
qed
next
assume "?E"
then obtain bs where O: "bddh (length bs) (Branch l r) ∧ bddh (length bs) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Branch l r) bs) (bdd_lookup (Leaf i) bs))" by blast
then obtain b br where B: "bs = b # br" by (cases bs) auto
with O IV1 IV2 show "?L ∨ ?R" by (cases b) auto
qed
finally show ?case by simp
next
case (3 i l r T)
hence IV1: "(¬ check_eq (Leaf i) l T) = (∃bs. bddh (length bs) l ∧ bddh (length bs) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Leaf i) bs) (bdd_lookup l bs)))" by simp
from 3 have IV2: "(¬ check_eq (Leaf i) r T) = (∃bs. bddh (length bs) r ∧ bddh (length bs) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Leaf i) bs) (bdd_lookup r bs)))" by simp
have "(¬ check_eq (Leaf i) (Branch l r) T) = (¬ check_eq (Leaf i) l T ∨ ¬ check_eq (Leaf i) r T)" by simp
also have "… = (∃bs. bddh (length bs) (Branch l r) ∧ bddh (length bs) (Leaf i) ∧ (∃n<m . dist_nodes M n v (bdd_lookup (Leaf i) bs) (bdd_lookup (Branch l r) bs)))" (is "(?L ∨ ?R) = ?E")
proof
assume "?L ∨ ?R"
thus "?E" proof (elim disjE)
assume "?L"
then obtain bs where O: "bddh (length bs) l ∧ bddh (length bs) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Leaf i) bs) (bdd_lookup l bs))" unfolding IV1 by blast
from bddh_exists obtain k where B: "bddh k r" by blast
with O have "bddh (length bs + k) r" and "bddh (length bs + k) l" and "bddh (length bs + k) (Leaf i)" by (simp add: bddh_ge[of k "length bs + k"] bddh_ge[of "length bs" "length bs + k"])+
with O have "bddh (length (False # bs @ replicate k False)) (Branch l r) ∧ bddh (length (False # bs @ replicate k False)) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Leaf i) (False # bs @ replicate k False)) (bdd_lookup (Branch l r) (False # bs @ replicate k False)))" by (auto simp: bdd_lookup_append)
thus ?thesis by (rule exI)
next
assume "?R"
then obtain bs where O: "bddh (length bs) r ∧ bddh (length bs) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Leaf i) bs) (bdd_lookup r bs))" unfolding IV2 by blast
from bddh_exists obtain k where B: "bddh k l" by blast
with O have "bddh (length bs + k) l" and "bddh (length bs + k) r" and "bddh (length bs + k) (Leaf i)" by (simp add: bddh_ge[of k "length bs + k"] bddh_ge[of "length bs" "length bs + k"])+
with O have "bddh (length (True # bs @ replicate k False)) (Branch l r) ∧ bddh (length (True # bs @ replicate k False)) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Leaf i) (True # bs @ replicate k False)) (bdd_lookup (Branch l r) (True # bs @ replicate k False)))" by (auto simp: bdd_lookup_append)
thus ?thesis by (rule exI)
qed
next
assume "?E"
then obtain bs where O: "bddh (length bs) (Branch l r) ∧ bddh (length bs) (Leaf i) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Leaf i) bs) (bdd_lookup (Branch l r) bs))" by blast
then obtain b br where B: "bs = b # br" by (cases bs) auto
with O IV1 IV2 show "?L ∨ ?R" by (cases b) auto
qed
finally show ?case by simp
next
case (4 l1 r1 l2 r2 T)
hence IV1: "(¬ check_eq l1 l2 T) = (∃bs. bddh (length bs) l1 ∧ bddh (length bs) l2 ∧ (∃n<m. dist_nodes M n v (bdd_lookup l1 bs) (bdd_lookup l2 bs)))" by simp
from 4 have IV2: "(¬ check_eq r1 r2 T) = (∃bs. bddh (length bs) r1 ∧ bddh (length bs) r2 ∧ (∃n<m. dist_nodes M n v (bdd_lookup r1 bs) (bdd_lookup r2 bs)))" by simp
have "(¬ check_eq (Branch l1 r1) (Branch l2 r2) T) = (¬ check_eq l1 l2 T ∨ ¬ check_eq r1 r2 T)" by simp
also have "… = (∃bs. bddh (length bs) (Branch l1 r1) ∧ bddh (length bs) (Branch l2 r2) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (Branch l1 r1) bs) (bdd_lookup (Branch l2 r2) bs)))"
(is "(?L ∨ ?R) = (∃bs. ?E bs)") proof
assume "?L ∨ ?R"
thus "∃bs. ?E bs" proof (elim disjE)
assume "?L"
then obtain bs where O: "bddh (length bs) l1 ∧ bddh (length bs) l2 ∧ (∃n<m. dist_nodes M n v (bdd_lookup l1 bs) (bdd_lookup l2 bs))" unfolding IV1 by blast
from bddh_exists obtain k1 k2 where K1: "bddh k1 r1" and K2: "bddh k2 r2" by blast
with O have "bddh (length bs + max k1 k2) l1" and "bddh (length bs + max k1 k2) l2" and "bddh (length bs + max k1 k2) r1" and "bddh (length bs + max k1 k2) r2"
by (simp add: bddh_ge[of "length bs" "length bs + max k1 k2"] bddh_ge[of k1 "length bs + max k1 k2"] bddh_ge[of k2 "length bs + max k1 k2"])+
with O have "bddh (length (False # bs @ replicate (max k1 k2) False)) (Branch l1 r1) ∧ bddh (length (False # bs @ replicate (max k1 k2) False)) (Branch l2 r2) ∧
(∃n<m. dist_nodes M n v (bdd_lookup (Branch l1 r1) (False # bs @ replicate (max k1 k2) False)) (bdd_lookup (Branch l2 r2) (False # bs @ replicate (max k1 k2) False)))"
by (auto simp: bdd_lookup_append)
thus ?thesis by (rule exI)
next
assume "?R"
then obtain bs where O: "bddh (length bs) r1 ∧ bddh (length bs) r2 ∧ (∃n<m. dist_nodes M n v (bdd_lookup r1 bs) (bdd_lookup r2 bs))" unfolding IV2 by blast
from bddh_exists obtain k1 k2 where K1: "bddh k1 l1" and K2: "bddh k2 l2" by blast
with O have "bddh (length bs + max k1 k2) l1" and "bddh (length bs + max k1 k2) l2" and "bddh (length bs + max k1 k2) r1" and "bddh (length bs + max k1 k2) r2"
by (simp add: bddh_ge[of "length bs" "length bs + max k1 k2"] bddh_ge[of k1 "length bs + max k1 k2"] bddh_ge[of k2 "length bs + max k1 k2"])+
with O have "bddh (length (True # bs @ replicate (max k1 k2) False)) (Branch l1 r1) ∧ bddh (length (True # bs @ replicate (max k1 k2) False)) (Branch l2 r2) ∧
(∃n<m. dist_nodes M n v (bdd_lookup (Branch l1 r1) (True # bs @ replicate (max k1 k2) False)) (bdd_lookup (Branch l2 r2) (True # bs @ replicate (max k1 k2) False)))"
by (auto simp: bdd_lookup_append)
thus ?thesis by (rule exI)
qed
next
assume "∃bs. ?E bs"
then obtain bs where O: "?E bs" by blast
then obtain b br where B: "bs = b # br" by (cases bs) auto
with O IV1 IV2 show "?L ∨ ?R" by (cases b) auto
qed
finally show ?case by simp
qed

lemma iter_wf: "wf_tr M T ⟹ wf_tr M (snd (iter M T))"
by (simp add: wf_tr_def iter_def fold_map_idx_len fold_map_idx_nth split_beta)

lemma fixpt_wf: "wf_tr M T ⟹ wf_tr M (fixpt M T)"
proof (induct M T rule: fixpt_induct)
case (1 M T)
show ?case proof (cases "fst (iter M T)")
case True with 1 show ?thesis by (simp add: iter_wf)
next
case False with 1 show ?thesis by simp
qed
qed

lemma list_split:
assumes "n ≤ length bss"
shows "∃b bs. bss = b @ bs ∧ length b = n"
using assms proof (induct bss arbitrary: n)
case (Cons a as)
show ?case proof (cases n)
case (Suc n')
with Cons have "∃b bs. as = b @ bs ∧ length b = n'" by simp
then obtain b bs where B: "as = b @ bs ∧ length b = n'" by blast
with Suc Cons have "a # as = (a # b) @ bs ∧ length (a # b) = n" by simp
thus ?thesis by blast
qed simp
qed simp

lemma iter_dist_nodes:
assumes "wf_tr M T"
and "wf_dfa M v"
and "∀p q. dfa_is_node M q ∧ p < q ⟶ tr_lookup T q p = (∃n < m. dist_nodes M n v p q)" and "m > 0"
and "dfa_is_node M q" and "p < q"
shows "tr_lookup (snd (iter M T)) q p = (∃n < Suc m. dist_nodes M n v p q)"
proof -
from assms obtain m' where M': "m = Suc m'" by (cases m) simp+
have C: "(¬ check_eq (fst M ! q) (fst M ! p) T) = (∃n<m. dist_nodes M (Suc n) v p q)" proof
assume "¬ check_eq (fst M ! q) (fst M ! p) T"
with assms have "∃bs. bddh (length bs) (fst M ! q) ∧ bddh (length bs) (fst M ! p) ∧ (∃n < m. dist_nodes M n v (bdd_lookup (fst M ! q) bs) (bdd_lookup (fst M ! p) bs))"
by (simp add: check_eq_dist_nodes wf_dfa_def list_all_iff dfa_is_node_def)
then obtain bs n bss where X: "bddh (length bs) (fst M ! q) ∧ bddh (length bs) (fst M ! p) ∧ n < m ∧
length bss = n ∧ list_all (is_alph v) bss ∧ dfa_accepting M (dfa_steps M (bdd_lookup (fst M ! q) bs) bss) ≠ dfa_accepting M (dfa_steps M (bdd_lookup (fst M ! p) bs) bss)"
unfolding dist_nodes_def by blast
from list_split[of v "bs @ replicate v False"] have "∃b' bs'. bs @ replicate v False = b' @ bs' ∧ length b' = v" by simp
then obtain b' bs' where V: "bs @ replicate v False = b' @ bs' ∧ length b' = v" by blast
with X bdd_lookup_append[of "length bs" "fst M ! q" "bs" "replicate v False"] bdd_lookup_append[of "length bs" "fst M ! p" "bs" "replicate v False"]
have 1: "dfa_accepting M (dfa_steps M (bdd_lookup (fst M ! q) (bs @ replicate v False)) bss) ≠ dfa_accepting M (dfa_steps M (bdd_lookup (fst M ! p) (bs @ replicate v False)) bss)" by simp
from assms have "bddh v (fst M ! q) ∧ bddh v (fst M ! p)" by (simp add: wf_dfa_def dfa_is_node_def list_all_iff)
with 1 V have "dfa_accepting M (dfa_steps M (dfa_trans M q b') bss) ≠ dfa_accepting M (dfa_steps M (dfa_trans M p b') bss)" by (auto simp: bdd_lookup_append dfa_trans_def)
with X V have "is_alph v b' ∧ dist_nodes M n v (dfa_trans M p b') (dfa_trans M q b')" by (auto simp: dist_nodes_def is_alph_def)
hence "dist_nodes M (Suc n) v p q" by (auto simp: dist_nodes_suc)
with X show "∃n<m. dist_nodes M (Suc n) v p q" by auto
next
assume "∃n<m. dist_nodes M (Suc n) v p q"
hence "∃bs. ∃n<m. is_alph v bs ∧ dist_nodes M n v (dfa_trans M p bs) (dfa_trans M q bs)" by (auto simp: dist_nodes_suc)
then obtain bs where X: "∃n<m. is_alph v bs ∧ dist_nodes M n v (dfa_trans M p bs) (dfa_trans M q bs)" by blast
hence BS: "length bs = v" by (auto simp: is_alph_def)
with assms have "bddh (length bs) (fst M ! p) ∧ bddh (length bs) (fst M ! q)" by (simp add: wf_dfa_def dfa_is_node_def list_all_iff)
with X have "bddh (length bs) (fst M ! p) ∧ bddh (length bs) (fst M ! q) ∧ (∃n<m. dist_nodes M n v (bdd_lookup (fst M ! q) bs) (bdd_lookup (fst M ! p) bs))" by (auto simp: dfa_trans_def dist_nodes_def)
moreover from assms have "bdd_all (dfa_is_node M) (fst M ! p) ∧ bdd_all (dfa_is_node M) (fst M ! q)" by (simp add: wf_dfa_def dfa_is_node_def list_all_iff)
moreover note assms(3,4)
ultimately show "¬ check_eq (fst M ! q) (fst M ! p) T" by (auto simp: check_eq_dist_nodes)
qed

from assms have "tr_lookup (snd (iter M T)) q p =
(if tr_lookup T q p then True else ¬ check_eq (fst M ! q) (fst M ! p) T)"
by (auto simp add: iter_def wf_tr_def split_beta fold_map_idx_nth tr_lookup_def dfa_is_node_def)
also have "… = (tr_lookup T q p ∨ ¬ check_eq (fst M ! q) (fst M ! p) T)" by simp
also from assms C have "… = ((∃n<m. dist_nodes M n v p q) ∨ (∃n<m. dist_nodes M (Suc n) v p q))" by simp
also have "… = (∃n < m. dist_nodes M n v p q ∨ dist_nodes M (Suc n) v p q)" by auto
also have "… = (∃n < Suc m. dist_nodes M n v p q)" proof
assume "∃n<m. dist_nodes M n v p q ∨ dist_nodes M (Suc n) v p q"
then obtain n where D: "dist_nodes M n v p q ∨ dist_nodes M (Suc n) v p q" and N: "n < m" by blast
moreover from N have "n < Suc m" by simp
ultimately show "∃n < Suc m. dist_nodes M n v p q" by (elim disjE) blast+
next
assume "∃n < Suc m. dist_nodes M n v p q"
then obtain n where N: "n < Suc m" and D: "dist_nodes M n v p q" by blast
from N have "n < m ∨ n = m" by auto
from this D M' show "∃n<m. dist_nodes M n v p q ∨ dist_nodes M (Suc n) v p q" by auto
qed
finally show ?thesis by simp
qed

lemma fixpt_dist_nodes':
assumes "wf_tr M T" and "wf_dfa M v"
and "∀p q. dfa_is_node M q ∧ p < q ⟶ tr_lookup T q p = (∃n < m. dist_nodes M n v p q)" and "m > 0"
and "dfa_is_node M q" and "p < q"
shows "tr_lookup (fixpt M T) q p = (∃n. dist_nodes M n v p q)"
using assms proof (induct M T arbitrary: m rule: fixpt_induct)
case (1 M T m)
let ?T = "snd (iter M T)"
show ?case proof (cases "fst (iter M T)")
case True
{ fix p' q' assume H: "dfa_is_node M q' ∧ p' < q'"
with 1 have "tr_lookup ?T q' p' = (∃n < Suc m. dist_nodes M n v p' q')" by (simp only: iter_dist_nodes)
} hence 2: "∀p q. dfa_is_node M q ∧ p < q ⟶ tr_lookup ?T q p = (∃n < Suc m. dist_nodes M n v p q)" by simp moreover
from 1 have "wf_tr M ?T" by (simp add: iter_wf) moreover
note 1(3,6,7) 1(1)[of "Suc m"] True
ultimately have "tr_lookup (fixpt M ?T) q p = (∃n. dist_nodes M n v p q)" by simp
with True show ?thesis by (simp add: Let_def split_beta)
next
case False
then have F: "snd (iter M T) = T" by (simp add: iter_def fold_map_idx_fst_snd_eq split_beta)
have C: "⋀m'. ∀p q. dfa_is_node M q ∧ p < q ⟶ tr_lookup T q p = (∃n < m' + m. dist_nodes M n v p q)"
proof -
fix m' show "∀p q. dfa_is_node M q ∧ p < q ⟶ tr_lookup T q p = (∃n < m' + m. dist_nodes M n v p q)"
proof (induct m')
case 0 with 1 show ?case by simp
next
case (Suc m')
{ fix p' q' assume H: "dfa_is_node M q'" and H2: "p' < q'"
note 1(2,3) Suc
moreover from Suc 1 have "0 < m' + m" by simp
moreover note H H2
ultimately have "tr_lookup (snd (iter M T)) q' p' = (∃n < Suc (m' + m). dist_nodes M n v p' q')" by (rule iter_dist_nodes)
with F have "tr_lookup T q' p' = (∃n < Suc m' + m. dist_nodes M n v p' q')" by simp
} thus ?case by simp
qed
qed
{
fix p' q' assume H: "dfa_is_node M q' ∧ p' < q'"
have "tr_lookup T q' p' = (∃n. dist_nodes M n v p' q')" proof
assume "tr_lookup T q' p'"
with H C[of 0] show "∃n. dist_nodes M n v p' q'" by auto
next
assume H': "∃n. dist_nodes M n v p' q'"
then obtain n where "dist_nodes M n v p' q'" by blast
moreover have "n < Suc n + m" by simp
ultimately have "∃n' < Suc n + m. dist_nodes M n' v p' q'" by blast
with H C[of "Suc n"] show "tr_lookup T q' p'" by simp
qed
} hence "∀p q. dfa_is_node M q ∧ p < q ⟶ tr_lookup T q p = (∃n. dist_nodes M n v p q)" by simp
with False ‹dfa_is_node M q› ‹p < q› show ?thesis by simp
qed
qed

lemma fixpt_dist_nodes:
assumes "wf_dfa M v"
and "dfa_is_node M p" and "dfa_is_node M q"
shows "tr_lookup (fixpt M (init_tr M)) p q = (∃n. dist_nodes M n v p q)"
proof -
{ fix p q assume H1: "p < q" and H2: "dfa_is_node M q"
from init_tr_wf have "wf_tr M (init_tr M)" by simp
moreover note assms(1)
moreover {
fix p' q' assume "dfa_is_node M q'" and "p' < q'"
hence "tr_lookup (init_tr M) q' p' = dist_nodes M 0 v p' q'" by (rule init_tr_dist_nodes)
also have "… = (∃n < 1. dist_nodes M n v p' q')" by auto
finally have "tr_lookup (init_tr M) q' p' = (∃n<1. dist_nodes M n v p' q')" by simp
} hence "∀p q. dfa_is_node M q ∧ p < q ⟶ tr_lookup (init_tr M) q p = (∃n<1. dist_nodes M n v p q)" by simp
moreover note H1 H2
ultimately have "tr_lookup (fixpt M (init_tr M)) q p = (∃n. dist_nodes M n v p q)" by (simp only: fixpt_dist_nodes'[of _ _ _ 1])
}
with assms(2,3) show ?thesis by (auto simp: tr_lookup_def dist_nodes_def)
qed

primrec mk_eqcl' :: "nat option list ⇒ nat ⇒ nat ⇒ nat ⇒ bool list list ⇒ nat option list"
where
"mk_eqcl' [] i j l T = []"
| "mk_eqcl' (x#xs) i j l T = (if tr_lookup T j i ∨ x ≠ None then x else Some l) # mk_eqcl' xs i (Suc j) l T"

lemma mk_eqcl'_len: "length (mk_eqcl' xs i j l T) = length xs" by (induct xs arbitrary: j) simp+

function mk_eqcl  :: "nat option list ⇒ nat list ⇒ nat ⇒ bool list list ⇒ nat list × nat list" where
"mk_eqcl [] zs i T = ([], zs)" |
"mk_eqcl (None # xs) zs i T = (let (xs',zs') = mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T in (length zs # xs', zs'))" |
"mk_eqcl (Some l # xs) zs i T = (let (xs',zs') = mk_eqcl xs zs (Suc i) T in (l # xs', zs'))"
by pat_completeness auto
termination by (lexicographic_order simp: mk_eqcl'_len)

lemma mk_eqcl'_bound:
assumes "⋀x k. ⟦x ∈ set xs; x = Some k⟧ ⟹ k < l"
and "x ∈ set (mk_eqcl' xs i j l T)" and "x = Some k"
shows "k ≤ l"
using assms proof (induct xs arbitrary: j)
case (Cons y xs j)
hence "x = y ∨ x = Some l ∨ x ∈ set (mk_eqcl' xs i (Suc j) l T)" by (cases "tr_lookup T j i ∨ y ≠ None") auto
thus ?case proof (elim disjE)
assume "x = y"
hence "x ∈ set (y # xs)" by simp
with Cons(2)[of x k] Cons(4) show ?thesis by simp
qed (insert Cons, auto)
qed simp

lemma mk_eqcl'_nth':
assumes "⋀x k. ⟦x ∈ set xs; x = Some k⟧ ⟹ k < l"
and "⋀i'. ⟦i' < length xs; ¬ tr_lookup T (i' + j) i⟧ ⟹ xs ! i' = None"
and "i < j" and "j' < length xs"
shows "(mk_eqcl' xs i j l T ! j' = Some l) = (¬ tr_lookup T (j' + j) i)"
using assms proof (induct xs arbitrary: j j')
case (Cons x xs j)
have I1:"⋀i'. ⟦i' < length xs; ¬ tr_lookup T (i' + Suc j) i⟧ ⟹ xs ! i' = None" proof -
fix i' assume H: "i' < length xs" "¬ tr_lookup T (i' + Suc j) i"
with Cons(3)[of "Suc i'"] show "xs ! i' = None" by simp
qed
have "j' = 0 ∨ j' > 0" by auto
thus ?case proof (elim disjE)
assume "j' > 0"
then obtain j'' where J: "j' = Suc j''" by (cases j') simp+
from Cons(1)[of "Suc j" j''] I1 Cons(2,4,5) J show ?thesis by simp
next
assume H: "j' = 0"
with Cons(3)[of 0] have "¬ tr_lookup T j i ⟹ x = None" by simp
with Cons H show ?thesis by auto
qed
qed simp

lemma mk_eqcl'_nth:
assumes "⋀i' j' k. ⟦i' < length xs; j' < length xs; xs ! i' = Some k⟧ ⟹ (xs ! j' = Some k) = (¬ tr_lookup T (i' + jj) (j' + jj))"
and "⋀a b c. ⟦a ≤ length T; b ≤ length T; c ≤ length T; ¬ tr_lookup T a b; ¬ tr_lookup T b c⟧ ⟹ ¬ tr_lookup T a c"
and "length xs + jj = length T + 1"
and "⋀x k. ⟦x ∈ set xs; x = Some k⟧ ⟹ k < l"
and "⋀i'. ⟦i' < length xs; ¬ tr_lookup T (i' + jj) ii⟧ ⟹ xs ! i' = None"
and "ii < jj"
and "i < length xs" and "mk_eqcl' xs ii jj l T ! i = Some m"
and "j < length xs"
shows "(mk_eqcl' xs ii jj l T ! j = Some m) = (¬ tr_lookup T (i + jj) (j + jj))"
using assms proof (induct xs arbitrary: jj i j)
case Nil
from Nil(7) have False by simp
thus ?case by simp
next
case (Cons y xs jj i j)
show ?case proof (cases i)
case 0
show ?thesis proof (cases j)
case 0
with ‹i=0› Cons(9) show ?thesis by (simp add: tr_lookup_def)
next
case (Suc j')
from 0 Cons(5,9) have 1: "y = Some m ∧ m < l ∨ (y = None ∧ ¬ tr_lookup T jj ii ∧ m = l)" by (cases y, cases "tr_lookup T jj ii", auto)
thus ?thesis proof (elim disjE)
assume H: "y = Some m ∧ m < l"
from Suc have "(mk_eqcl' (y # xs) ii jj l T ! j = Some m) = (mk_eqcl' xs ii (Suc jj) l T ! j' = Some m)" by simp
also from H have "… = (xs ! j' = Some m)" proof (induct xs arbitrary: jj j')
case (Cons a xs jj j') thus ?case by (cases j') simp+
qed simp
also from Suc have "… = ((y # xs) ! j = Some m)" by simp
also from Cons(2)[of i j m] Cons(8,10) Suc 0 H have "… = (¬ tr_lookup T (i + jj) (j + jj))" by simp
finally show ?thesis by simp
next
assume H: "y = None ∧ ¬ tr_lookup T jj ii ∧ m = l"
with Suc have "(mk_eqcl' (y # xs) ii jj l T ! j = Some m) = (mk_eqcl' xs ii (Suc jj) l T ! j' = Some l)" by simp
also have "… = (¬ tr_lookup T (j' + Suc jj) ii)" proof (rule mk_eqcl'_nth')
from Cons(5) show "⋀x k. ⟦x ∈ set xs; x = Some k⟧ ⟹ k < l" by simp
show "⋀i'. ⟦i' < length xs; ¬ tr_lookup T (i' + Suc jj) ii⟧ ⟹ xs ! i' = None" proof -
fix i' assume "i' < length xs" "¬ tr_lookup T (i' + Suc jj) ii"
with Cons(6)[of "Suc i'"] show "xs ! i' = None" by simp
qed
from Cons(7) show "ii < Suc jj" by simp
from Cons(10) Suc show "j' < length xs" by simp
qed
also from Suc H 0 have "… = (¬ tr_lookup T (j + jj) ii ∧ ¬ tr_lookup T (i + jj) ii)" by (simp add: add.commute)
also have "… = (¬ tr_lookup T (i + jj) (j + jj) ∧ ¬ tr_lookup T (i + jj) ii)" proof
assume H': "¬ tr_lookup T (j + jj) ii ∧ ¬ tr_lookup T (i + jj) ii"
hence "¬ tr_lookup T ii (j + jj)" by (auto simp: tr_lookup_def)
with H' Cons(3)[of "i + jj" ii "j + jj"] Cons(4,7,8,10) show "¬ tr_lookup T (i + jj) (j + jj) ∧ ¬ tr_lookup T (i + jj) ii" by simp
next
assume H': "¬ tr_lookup T (i + jj) (j + jj) ∧ ¬ tr_lookup T (i + jj) ii"
hence "¬ tr_lookup T (j + jj) (i + jj)" by (auto simp: tr_lookup_def)
with H' Cons(3)[of "j + jj" "i + jj" ii] Cons(4,7,8,10) show "¬ tr_lookup T (j + jj) ii ∧ ¬ tr_lookup T (i + jj) ii" by simp
qed
also from 0 H have "… = (¬ tr_lookup T (i + jj) (j + jj))" by simp
finally show ?thesis by simp
qed
qed
next
case (Suc i')
show ?thesis proof (cases j)
case 0
have "m ≤ l" proof (rule mk_eqcl'_bound)
from Cons(5) show "⋀x k. ⟦x ∈ set (y # xs); x = Some k⟧ ⟹ k < l" by simp
from Cons(8) have "i < length (mk_eqcl' (y # xs) ii jj l T)" by (simp add: mk_eqcl'_len)
with Cons(9) have "∃i < length (mk_eqcl' (y # xs) ii jj l T). mk_eqcl' (y # xs) ii jj l T ! i = Some m" by blast
thus "Some m ∈ set (mk_eqcl' (y # xs) ii jj l T)" by (simp only: in_set_conv_nth)
show "Some m = Some m" by simp
qed
hence "m < l ∨ m = l" by auto
thus ?thesis proof (elim disjE)
assume H: "m < l"
with Cons(9) have I: "(y # xs) ! i = Some m" proof (induct ("y # xs") arbitrary: jj i)
case (Cons a l jj i) thus ?case by (cases i) (auto, cases "tr_lookup T jj ii ∨ a ≠ None", simp+)
qed simp
from 0 H have "(mk_eqcl' (y # xs) ii jj l T ! j = Some m) = ((y#xs) ! j = Some m)" by (cases "tr_lookup T jj ii ∨ y ≠ None") simp+
also from Cons(8,10) I have "… = (¬ tr_lookup T (i + jj) (j + jj))" by (rule Cons(2))
finally show ?thesis by simp
next
assume H: "m = l"
from Cons(5,6,7,8) have "(mk_eqcl' (y # xs) ii jj l T ! i = Some l) = (¬ tr_lookup T (i + jj) ii)" by (rule mk_eqcl'_nth')
with H Cons(9) have I: "¬ tr_lookup T (i + jj) ii" by simp

with 0 H Cons(5) have "(mk_eqcl' (y # xs) ii jj l T ! j = Some m) = (¬ tr_lookup T (j + jj) ii ∧ ¬ tr_lookup T (i + jj) ii ∧ y = None)" by auto
also from Cons(6)[of 0] 0 have "… = (¬ tr_lookup T (j + jj) ii ∧ ¬ tr_lookup T (i + jj) ii)" by auto
also have "… = (¬ tr_lookup T (i + jj) (j + jj) ∧ ¬ tr_lookup T (i + jj) ii)" proof
assume H': "¬ tr_lookup T (j + jj) ii ∧ ¬ tr_lookup T (i + jj) ii"
hence "¬ tr_lookup T ii (j + jj)" by (auto simp: tr_lookup_def)
with H' Cons(3)[of "i + jj" ii "j + jj"] Cons(4,7,8,10) show "¬ tr_lookup T (i + jj) (j + jj) ∧ ¬ tr_lookup T (i + jj) ii" by simp
next
assume H': "¬ tr_lookup T (i + jj) (j + jj) ∧ ¬ tr_lookup T (i + jj) ii"
hence "¬ tr_lookup T (j + jj) (i + jj)" by (auto simp: tr_lookup_def)
with H' Cons(3)[of "j + jj" "i + jj" ii] Cons(4,7,8,10) show "¬ tr_lookup T (j + jj) ii ∧ ¬ tr_lookup T (i + jj) ii" by simp
qed
also from I have "… = (¬ tr_lookup T (i + jj) (j + jj))" by simp
finally show ?thesis by simp
qed
next
case (Suc j')
hence "(mk_eqcl' (y # xs) ii jj l T ! j = Some m) = (mk_eqcl' xs ii (Suc jj) l T ! j' = Some m)" by simp
also have "… = (¬ tr_lookup T (i' + Suc jj) (j' + Suc jj))" proof (rule Cons(1))
show "⋀i' j' k. ⟦i' < length xs; j' < length xs; xs ! i' = Some k⟧ ⟹ (xs ! j' = Some k) = (¬ tr_lookup T (i' + Suc jj) (j' + Suc jj))" proof -
fix i' j' k assume "i' < length xs" "j' < length xs" "xs ! i' = Some k"
with Cons(2)[of "Suc i'" "Suc j'" k] show "(xs ! j' = Some k) = (¬ tr_lookup T (i' + Suc jj) (j' + Suc jj))" by simp
qed
from Cons(3) show "⋀a b c. ⟦a ≤ length T; b ≤ length T; c ≤ length T; ¬ tr_lookup T a b; ¬ tr_lookup T b c ⟧ ⟹ ¬ tr_lookup T a c" by blast
from Cons(4) show "length xs + Suc jj = length T + 1" by simp
from Cons(5) show "⋀x k. ⟦x ∈ set xs; x = Some k⟧ ⟹ k < l" by simp
show "⋀i'. ⟦i' < length xs; ¬ tr_lookup T (i' + Suc jj) ii⟧ ⟹ xs ! i' = None" proof -
fix i' assume "i' < length xs" "¬ tr_lookup T (i' + Suc jj) ii"
with Cons(6)[of "Suc i'"] show "xs ! i' = None" by simp
qed
from Cons(7) show "ii < Suc jj" by simp
from Cons(8) ‹i=Suc i'› show "i' < length xs" by simp
from Cons(9) ‹i=Suc i'› show "mk_eqcl' xs ii (Suc jj) l T ! i' = Some m" by simp
from Cons(10) Suc show "j' < length xs" by simp
qed
also from Suc ‹i=Suc i'› have "… = (¬ tr_lookup T (i + jj) (j + jj))" by simp
finally show ?thesis by simp
qed
qed
qed

lemma mk_eqcl'_Some:
assumes "i < length xs" and "xs ! i ≠ None"
shows "mk_eqcl' xs ii j l T ! i = xs ! i"
using assms proof (induct xs arbitrary: j i)
case (Cons y xs j i)
thus ?case by (cases i) auto
qed simp

lemma mk_eqcl'_Some2:
assumes "i < length xs"
and "k < l"
shows "(mk_eqcl' xs ii j l T ! i = Some k) = (xs ! i = Some k)"
using assms proof (induct xs arbitrary: j i)
case (Cons y xs j i)
thus ?case by (cases i) auto
qed simp

lemma mk_eqcl_fst_Some:
assumes "i < length xs" and "k < length zs"
shows "(fst (mk_eqcl xs zs ii T) ! i = k) = (xs ! i = Some k)"
using assms proof (induct xs zs ii T arbitrary: i rule: mk_eqcl.induct)
case (2 xs zs ii T i)
thus ?case by (cases i) (simp add: split_beta mk_eqcl'_len mk_eqcl'_Some2)+
next
case (3 l xs zs ii T i)
thus ?case by (cases i) (simp add: split_beta)+
qed simp

lemma mk_eqcl_len_snd:
"length zs ≤ length (snd (mk_eqcl xs zs i T))"
by (induct xs zs i T rule: mk_eqcl.induct) (simp add: split_beta)+

lemma mk_eqcl_len_fst:
"length (fst (mk_eqcl xs zs i T)) = length xs"
by (induct xs zs i T rule: mk_eqcl.induct) (simp add: split_beta mk_eqcl'_len)+

lemma mk_eqcl_set_snd:
assumes "i ∉ set zs"
and "j > i"
shows "i ∉ set (snd (mk_eqcl xs zs j T))"
using assms by (induct xs zs j T rule: mk_eqcl.induct) (auto simp: split_beta)

lemma mk_eqcl_snd_mon:
assumes "⋀j1 j2. ⟦j1 < j2; j2 < length zs⟧ ⟹ zs ! j1 < zs ! j2"
and "⋀x. x ∈ set zs ⟹ x < i"
and "j1 < j2" and "j2 < length (snd (mk_eqcl xs zs i T))"
shows "snd (mk_eqcl xs zs i T) ! j1 < snd (mk_eqcl xs zs i T) ! j2"
using assms proof (induct xs zs i T rule: mk_eqcl.induct)
case (2 xs zs i T)
have "⋀j1 j2. ⟦j1 < j2; j2 < length (zs @ [i])⟧ ⟹ (zs @ [i]) ! j1 < (zs @ [i]) ! j2" proof -
fix j1 j2 assume H: "j1 < j2" "j2 < length (zs @ [i])"
hence "j2 < length zs ∨ j2 = length zs" by auto
from this H 2 show "(zs @ [i]) ! j1 < (zs @ [i]) ! j2" by (elim disjE) (simp add: nth_append)+
qed moreover
have "⋀x. x ∈ set (zs @ [i]) ⟹ x < Suc i" proof -
fix x assume "x ∈ set (zs @ [i])"
hence "x ∈ set zs ∨ x = i" by auto
with 2(3)[of x] show "x < Suc i" by auto
qed moreover
note 2(4) moreover
from 2(5) have "j2 < length (snd (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T))" by (simp add: split_beta)
ultimately have "snd (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T) ! j1 < snd (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T) ! j2" by (rule 2(1))
thus ?case by (simp add: split_beta)
next
case (3 l xs zs i T)
note 3(2) moreover
have "⋀x. x ∈ set zs ⟹ x < Suc i" proof -
fix x assume "x ∈ set zs"
with 3(3)[of x] show "x < Suc i" by simp
qed moreover
note 3(4) moreover
from 3(5) have "j2 < length (snd (mk_eqcl xs zs (Suc i) T))" by (simp add: split_beta)
ultimately have "snd (mk_eqcl xs zs (Suc i) T) ! j1 < snd (mk_eqcl xs zs (Suc i) T) ! j2" by (rule 3(1))
thus ?case by (simp add: split_beta)
qed simp

lemma mk_eqcl_snd_nth:
assumes "i < length zs"
shows "snd (mk_eqcl xs zs j T) ! i = zs ! i"
using assms by (induct xs zs j T rule: mk_eqcl.induct) (simp add: split_beta nth_append)+

lemma mk_eqcl_bound:
assumes "⋀x k. ⟦x ∈ set xs; x = Some k⟧ ⟹ k < length zs"
and "x ∈ set (fst (mk_eqcl xs zs ii T))"
shows "x < length (snd (mk_eqcl xs zs ii T))"
using assms proof (induct xs zs ii T rule: mk_eqcl.induct)
case (2 xs zs i T)
hence "x = length zs ∨ x ∈ set (fst (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T))" by (auto simp: split_beta)
thus ?case proof (elim disjE)
assume "x = length zs"
hence "x < length (zs @ [i])" by simp
also have "… ≤ length (snd (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T))" by (simp only: mk_eqcl_len_snd)
finally show ?thesis by (simp add: split_beta)
next
assume H: "x ∈ set (fst (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T))"
have "⋀x k. ⟦x ∈ set (mk_eqcl' xs i (Suc i) (length zs) T); x = Some k⟧ ⟹ k < length (zs @ [i])" proof -
fix x k assume H': "x ∈ set (mk_eqcl' xs i (Suc i) (length zs) T)" " x = Some k"
{ fix x' k' assume "x' ∈ set xs" "x' = Some k'"
with 2 have "k' < length zs" by simp
} from this H' have "k ≤ length zs" by (rule mk_eqcl'_bound)
thus "k < length (zs @ [i])" by simp
qed
with H 2 show ?thesis by (simp add: split_beta)
qed
next
case (3 l xs zs i T)
hence "x = l ∨ x ∈ set (fst (mk_eqcl xs zs (Suc i) T))" by (auto simp: split_beta)
thus ?case proof (elim disjE)
assume "x = l"
with 3 have "x < length zs" by simp
also from 3 have "… ≤ length (snd (mk_eqcl (Some l # xs) zs i T))" by (simp only: mk_eqcl_len_snd)
finally show ?thesis by simp
next
assume "x ∈ set (fst (mk_eqcl xs zs (Suc i) T))"
with 3 have "x < length (snd (mk_eqcl xs zs (Suc i) T))" by simp
thus ?thesis by (simp add: split_beta)
qed
qed simp

lemma mk_eqcl_fst_snd:
assumes "⋀i. i < length zs ⟹ zs ! i < length xs + ii ∧ (zs ! i ≥ ii ⟶ xs ! (zs ! i - ii) = Some i)"
and "⋀j1 j2. ⟦j1 < j2; j2 < length zs⟧ ⟹ zs ! j1 < zs ! j2"
and "⋀z. z ∈ set zs ⟹ z < ii"
and "i < length (snd (mk_eqcl xs zs ii T))"
and "length xs + ii ≤ length T + 1"
shows "snd (mk_eqcl xs zs ii T) ! i < length (fst (mk_eqcl xs zs ii T)) + ii ∧ (snd (mk_eqcl xs zs ii T) ! i ≥ ii ⟶  fst (mk_eqcl xs zs ii T) ! (snd (mk_eqcl xs zs ii T) ! i - ii) = i)"
using assms proof (induct xs zs ii T arbitrary: i rule: mk_eqcl.induct)
case (1 zs ii T i)
from 1(1)[of i] 1(4,5) show ?case by simp
next
case (2 xs zs i T j)
have "⋀i'. i' < length (zs @ [i]) ⟹ (zs @ [i]) ! i' < length (mk_eqcl' xs i (Suc i) (length zs) T) + Suc i ∧
(Suc i ≤ (zs @ [i]) ! i' ⟶ mk_eqcl' xs i (Suc i) (length zs) T ! ((zs @ [i]) ! i' - Suc i) = Some i')" proof -
fix i' assume "i' < length (zs @ [i])"
hence "i' < length zs ∨ i' = length zs" by auto
thus "(zs @ [i]) ! i' < length (mk_eqcl' xs i (Suc i) (length zs) T) + Suc i ∧ (Suc i ≤ (zs @ [i]) ! i' ⟶ mk_eqcl' xs i (Suc i) (length zs) T ! ((zs @ [i]) ! i' - Suc i) = Some i')"
proof (elim disjE)
assume H: "i' < length zs"
with 2(2) have I: "zs ! i' < length (None # xs) + i ∧ (i ≤ zs ! i' ⟶ (None # xs) ! (zs ! i' - i) = Some i')" by simp
with H have G1: "(zs @ [i]) ! i' < length (mk_eqcl' xs i (Suc i) (length zs) T) + Suc i" by (auto simp: mk_eqcl'_len nth_append)
{ assume H': "Suc i ≤ (zs @ [i]) ! i'"
then obtain k where K: "(zs @ [i]) ! i' - i = Suc k" by (cases "(zs @ [i]) ! i' - i") simp+
hence K': "k = (zs @ [i]) ! i' - Suc i" by simp
from K H' H I have "xs ! k = Some i'" by (simp add: nth_append)
with K I H have "mk_eqcl' xs i (Suc i) (length zs) T ! k = Some i'" by (auto simp add: mk_eqcl'_Some nth_append)
with K' have "mk_eqcl' xs i (Suc i) (length zs) T ! ((zs @ [i]) ! i' - Suc i) = Some i'" by simp
} with G1 show ?thesis by simp
qed simp
qed
moreover have "⋀j1 j2. ⟦j1 < j2; j2 < length (zs @ [i])⟧ ⟹ (zs @ [i]) ! j1 < (zs @ [i]) ! j2" proof -
fix j1 j2 assume H: "j1 < j2" "j2 < length (zs @ [i])"
hence "j2 < length zs ∨ j2 = length zs" by auto
from this H 2(3)[of j1 j2] 2(4)[of "zs ! j1"] show "(zs @ [i]) ! j1 < (zs @ [i]) ! j2" by (elim disjE) (simp add: nth_append)+
qed
moreover have "⋀z. z ∈ set (zs @ [i]) ⟹ z < Suc i" proof -
fix z assume "z ∈ set (zs @ [i])"
hence "z ∈ set zs ∨ z = i" by auto
with 2(4)[of z] show "z < Suc i" by auto
qed
moreover from 2 have "j < length (snd (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T))" by (simp add: split_beta)
moreover from 2 have "length (mk_eqcl' xs i (Suc i) (length zs) T) + Suc i ≤ length T + 1" by (simp add: mk_eqcl'_len)
ultimately have IV: "snd (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T) ! j < length (fst (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T)) + Suc i ∧
(Suc i ≤ snd (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T) ! j ⟶
fst (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T) ! (snd (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T) ! j - Suc i) = j)" by (rule 2(1))
hence G1: "snd (mk_eqcl (None # xs) zs i T) ! j < length (fst (mk_eqcl (None # xs) zs i T)) + i" by (auto simp: split_beta)
{ assume "i ≤ snd (mk_eqcl (None # xs) zs i T) ! j"
hence "i = snd (mk_eqcl (None # xs) zs i T) ! j ∨ Suc i ≤ snd (mk_eqcl (None # xs) zs i T) ! j" by auto
hence "fst (mk_eqcl (None # xs) zs i T) ! (snd (mk_eqcl (None # xs) zs i T) ! j - i) = j" proof (elim disjE)
assume H: "i = snd (mk_eqcl (None # xs) zs i T) ! j"
define k where "k = length zs"
hence K: "snd (mk_eqcl (None # xs) zs i T) ! k = i" by (simp add: mk_eqcl_snd_nth split_beta)
{ assume "j ≠ k"
hence "j < k ∨ j > k" by auto
hence "snd (mk_eqcl (None # xs) zs i T) ! j ≠ i" proof (elim disjE)
assume H': "j < k"
from k_def have "k < length (zs @ [i])" by simp
also have "… ≤ length (snd (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T))" by (simp only: mk_eqcl_len_snd)
also have "… = length (snd (mk_eqcl (None # xs) zs i T))" by (simp add: split_beta)
finally have K': "k < length (snd (mk_eqcl (None # xs) zs i T))" by simp
from 2(3,4) H' this have "snd (mk_eqcl (None # xs) zs i T) ! j < snd (mk_eqcl (None # xs) zs i T) ! k" by (rule mk_eqcl_snd_mon)
with K show ?thesis by simp
next
assume H': "j > k"
from 2(3,4) H' 2(5) have "snd (mk_eqcl (None # xs) zs i T) ! k < snd (mk_eqcl (None # xs) zs i T) ! j" by (rule mk_eqcl_snd_mon)
with K show ?thesis by simp
qed
}
with H k_def have "j = length zs" by auto
with H show ?thesis by (simp add: split_beta)
next
assume H: "Suc i ≤ snd (mk_eqcl (None # xs) zs i T) ! j"
then obtain k where K: "snd (mk_eqcl (None # xs) zs i T) ! j - i = Suc k" by (cases "snd (mk_eqcl (None # xs) zs i T) ! j - i") simp+
hence K': "k = snd (mk_eqcl (None # xs) zs i T) ! j - Suc i" by simp
from H IV have "fst (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T) ! (snd (mk_eqcl (mk_eqcl' xs i (Suc i) (length zs) T) (zs @ [i]) (Suc i) T) ! j - Suc i) = j"
by (auto simp: split_beta)
with K' have "fst (mk_eqcl (None # xs) zs i T) ! Suc k = j" by (simp add: split_beta)
with K show ?thesis by simp
qed
} with G1 show ?case by simp
next
case (3 l xs zs i T j)
have 1: "snd (mk_eqcl (Some l # xs) zs i T) = snd (mk_eqcl xs zs (Suc i) T)" by (simp add: split_beta)
have 2: "length (fst (mk_eqcl (Some l # xs) zs i T)) = length (Some l # xs)" by (simp add: split_beta mk_eqcl_len_fst)
have "⋀j. j < length zs ⟹ zs ! j < length xs + Suc i ∧ (Suc i ≤ zs ! j ⟶ xs ! (zs ! j - Suc i) = Some j)" proof -
fix j assume H: "j < length zs"
with 3(2)[of j] have I: "zs ! j < length (Some l # xs) + i ∧ (i ≤ zs ! j ⟶ (Some l # xs) ! (zs ! j - i) = Some j)" by simp
hence G1: "zs ! j < length xs + Suc i" and G2: "i ≤ zs ! j ⟶ (Some l # xs) ! (zs ! j - i) = Some j" by simp+
{ assume H2: "Suc i ≤ zs ! j"
then obtain k where K: "zs ! j - i = Suc k" by (cases "zs ! j - i") simp+
with H2 G2 have "xs ! k = Some j" by simp
moreover from K have "k = zs ! j - Suc i" by simp
ultimately have "xs ! (zs ! j - Suc i) = Some j" by simp
}
with G1 show "zs ! j < length xs + Suc i ∧ (Suc i ≤ zs ! j ⟶ xs ! (zs ! j - Suc i) = Some j)" by simp
qed
moreover note 3(3)
moreover have "⋀z. z ∈ set zs ⟹ z < Suc i" proof -
fix z assume "z ∈ set zs"
with 3(4)[of z] show "z < Suc i" by simp
qed
moreover from 3(5) 1 have "j < length (snd (mk_eqcl xs zs (Suc i) T))" by simp
moreover from 3 have "length xs + Suc i ≤ length T + 1" by simp
ultimately have IV: "snd (mk_eqcl xs zs (Suc i) T) ! j < length (fst (mk_eqcl xs zs (Suc i) T)) + Suc i ∧
(Suc i ≤ snd (mk_eqcl xs zs (Suc i) T) ! j ⟶ fst (mk_eqcl xs zs (Suc i) T) ! (snd (mk_eqcl xs zs (Suc i) T) ! j - Suc i) = j)" by (rule 3(1))
with 1 have G1: "snd (mk_eqcl (Some l # xs) zs i T) ! j < length (fst (mk_eqcl (Some l # xs) zs i T)) + i" by (simp add: split_beta mk_eqcl_len_fst)
{ assume "i ≤ snd (mk_eqcl (Some l # xs) zs i T) ! j"
hence "i = snd (mk_eqcl (Some l # xs) zs i T) ! j ∨ i < snd (mk_eqcl (Some l # xs) zs i T) ! j" by auto
hence "fst (mk_eqcl (Some l # xs) zs i T) ! (snd (mk_eqcl (Some l # xs) zs i T) ! j - i) = j" proof (elim disjE)
assume H: "i = snd (mk_eqcl (Some l # xs) zs i T) ! j"
with 3 1 have "∃j < length (snd (mk_eqcl xs zs (Suc i) T)). snd (mk_eqcl xs zs (Suc i) T) ! j = i" by auto
hence T1: "i ∈ set (snd (mk_eqcl xs zs (Suc i) T))" by (simp only: in_set_conv_nth)
from 3(4) have "i ∉ set zs" by auto
hence "i ∉ set (snd (mk_eqcl xs zs (Suc i) T))" by (simp add: mk_eqcl_set_snd)
with T1 show ?thesis by simp
next
assume H: "i < snd (mk_eqcl (Some l # xs) zs i T) ! j"
from H obtain k where K: "snd (mk_eqcl (Some l # xs) zs i T) ! j - i = Suc k" by (cases "snd (mk_eqcl (Some l # xs) zs i T) ! j - i") simp+
hence K': "snd (mk_eqcl (Some l # xs) zs i T) ! j - Suc i = k" by simp
from 1 H IV have "fst (mk_eqcl xs zs (Suc i) T) ! (snd (mk_eqcl xs zs (Suc i) T) ! j - Suc i) = j" by simp
with K K' show ?thesis by (simp add: split_beta)
qed
} with G1 show ?case by simp
qed

lemma mk_eqcl_fst_nth:
assumes "⋀i j k. ⟦i < length xs; j < length xs; xs ! i = Some k⟧ ⟹ (xs ! j = Some k) = (¬ tr_lookup T (i + ii) (j + ii))"
and "⋀a b c. ⟦a ≤ length T; b ≤ length T; c ≤ length T; ¬ tr_lookup T a b; ¬ tr_lookup T b c⟧ ⟹ ¬ tr_lookup T a c"
and "⋀x k. ⟦x ∈ set xs; x = Some k⟧ ⟹ k < length zs"
and "length xs + ii = length T + 1"
and "i < length xs" and "j < length xs"
shows "(fst (mk_eqcl xs zs ii T) ! i = fst (mk_eqcl xs zs ii T) ! j) = (¬ tr_lookup T (i + ii) (j + ii))"
using assms proof (induct xs zs ii T arbitrary: i j rule: mk_eqcl.induct)
case (1 zs ii T) thus ?case by simp
next
case (2 xs zs ii T)
{ fix i j assume H: "i < j" "j < length (None # xs)"
then obtain j' where J: "j = Suc j'" by (cases j) simp+
have "(fst (mk_eqcl (None # xs) zs ii T) ! i = fst (mk_eqcl (None # xs) zs ii T) ! j) = (¬ tr_lookup T (i + ii) (j + ii))" proof (cases i)
case 0
with J have "(fst (mk_eqcl (None # xs) zs ii T) ! i = fst (mk_eqcl (None # xs) zs ii T) ! j) = (fst (mk_eqcl (mk_eqcl' xs ii (Suc ii) (length zs) T) (zs @ [ii]) (Suc ii) T) ! j' = length zs)"
by (auto simp add: split_beta)
also from H J have "… = (mk_eqcl' xs ii (Suc ii) (length zs) T ! j' = Some (length zs))" by (simp add: mk_eqcl_fst_Some mk_eqcl'_len)
also have "… = (¬ tr_lookup T (j' + Suc ii) ii)" proof -
have "⋀x k. ⟦x ∈ set xs; x = Some k⟧ ⟹ k < length zs" proof -
fix x k assume "x ∈ set xs" "x = Some k"
with 2(4)[of x k] show "k < length zs" by simp
qed moreover
have "⋀i'. ⟦i' < length xs; ¬ tr_lookup T (i' + Suc ii) ii⟧ ⟹ xs ! i' = None" proof -
fix i' assume H: "i' < length xs" "¬ tr_lookup T (i' + Suc ii) ii"
{ assume H': "xs ! i' ≠ None"
then obtain k where "xs ! i' = Some k" by (cases "xs ! i'") simp+
with 2(2)[of "Suc i'" 0 k] H have False by simp
} thus "xs ! i' = None" by (cases "xs ! i'") simp+
qed moreover
from H J have "ii < Suc ii" "j' < length xs" by simp+
ultimately show ?thesis by (rule mk_eqcl'_nth')
qed
also from J 0 have "… = (¬ tr_lookup T (i + ii) (j + ii))" by (auto simp: tr_lookup_def)
finally show ?thesis by simp
next
case (Suc i')
have "⋀i j k. ⟦i < length (mk_eqcl' xs ii (Suc ii) (length zs) T); j < length (mk_eqcl' xs ii (Suc ii) (length zs) T); mk_eqcl' xs ii (Suc ii) (length zs) T ! i = Some k⟧
⟹ (mk_eqcl' xs ii (Suc ii) (length zs) T ! j = Some k) = (¬ tr_lookup T (i + Suc ii) (j + Suc ii))" proof -
fix i j k assume H: "i < length (mk_eqcl' xs ii (Suc ii) (length zs) T)" "j < length (mk_eqcl' xs ii (Suc ii) (length zs) T)" "mk_eqcl' xs ii (Suc ii) (length zs) T ! i = Some k"
{ fix i' j' k assume "i' < length xs" "j' < length xs" "xs ! i' = Some k"
with 2(2)[of "Suc i'" "Suc j'" k] have "(xs ! j' = Some k) = (¬ tr_lookup T (i' + Suc ii) (j' + Suc ii))" by simp
} moreover
note 2(3) moreover
from 2(5) have "length xs + Suc ii = length T + 1" by simp moreover
{ fix x k assume "x ∈ set xs" "x = Some k"
with 2(4)[of x k] have "k < length zs" by simp
} moreover
have "⋀i'. ⟦i' < length xs; ¬ tr_lookup T (i' + Suc ii) ii⟧ ⟹ xs ! i' = None" proof -
fix i' assume H': "i' < length xs" "¬ tr_lookup T (i' + Suc ii) ii"
{ assume "xs ! i' ≠ None"
then obtain k where K: "xs ! i' = Some k" by (cases "xs ! i'") simp+
with H' 2(2)[of "Suc i'" 0 k] have False by simp
} thus "xs ! i' = None" by (cases "xs ! i' = None") simp+
qed moreover
have "ii < Suc ii" by simp moreover
from H have "i < length xs" by (simp add: mk_eqcl'_len) moreover
note H(3) moreover
from H have "j < length xs" by (simp add: mk_eqcl'_len)
ultimately show "(mk_eqcl' xs ii (Suc ii) (length zs) T ! j = Some k) = (¬ tr_lookup T (i + Suc ii) (j + Suc ii))" by (rule mk_eqcl'_nth)
qed moreover
note 2(3) moreover
have "⋀x k. ⟦x ∈ set (mk_eqcl' xs ii (Suc ii) (length zs) T); x = Some k⟧ ⟹ k < length (zs @ [ii])" proof -
fix x k assume H: "x ∈ set (mk_eqcl' xs ii (Suc ii) (length zs) T)" "x = Some k"
{ fix x k assume "x ∈ set xs" "x = Some k"
with 2(4)[of x k] have "k < length zs" by simp
} from this H have "k ≤ length zs" by (rule mk_eqcl'_bound)
thus "k < length (zs @ [ii])" by simp
qed moreover
from 2(5) have "length (mk_eqcl' xs ii (Suc ii) (length zs) T) + Suc ii = length T + 1" by (simp add: mk_eqcl'_len) moreover
from H Suc J have "i' < length (mk_eqcl' xs ii (Suc ii) (length zs) T)" "j' < length (mk_eqcl' xs ii (Suc ii) (length zs) T)" by (simp add: mk_eqcl'_len)+
ultimately have IV: "(fst (mk_eqcl (mk_eqcl' xs ii (Suc ii) (length zs) T) (zs @ [ii]) (Suc ii) T) ! i' = fst (mk_eqcl (mk_eqcl' xs ii (Suc ii) (length zs) T) (zs @ [ii]) (Suc ii) T) ! j') =
(¬ tr_lookup T (i' + Suc ii) (j' + Suc ii))" by (rule 2(1))
with Suc J show ?thesis by (simp add: split_beta)
qed
} note L = this
have "i < j ∨ i = j ∨ i > j" by auto
thus ?case proof (elim disjE)
assume "i > j"
with 2(6) L have "(fst (mk_eqcl (None # xs) zs ii T) ! j = fst (mk_eqcl (None # xs) zs ii T) ! i) = (¬ tr_lookup T (i + ii) (j + ii))" by (auto simp: tr_lookup_def)
thus ?thesis by auto
qed (insert 2(7) L, simp add: tr_lookup_def)+
next
case (3 l xs zs ii T i j)
{ fix i j assume H: "i < j" "j < length (Some l # xs)"
then obtain j' where J: "j = Suc j'" by (cases j) simp+
have "(fst (mk_eqcl (Some l # xs) zs ii T) ! i = fst (mk_eqcl (Some l # xs) zs ii T) ! j) = (¬ tr_lookup T (i + ii) (j + ii))" proof (cases i)
case 0
with J have "(fst (mk_eqcl (Some l # xs) zs ii T) ! i = fst (mk_eqcl (Some l # xs) zs ii T) ! j) = (fst (mk_eqcl xs zs (Suc ii) T) ! j' = l)" by (auto simp add: split_beta)
also from 3(4)[of "Some l" l] H J have "… = (xs ! j' = Some l)" by (simp add: mk_eqcl_fst_Some)
also from J have "… = ((Some l # xs) ! j = Some l)" by simp
also from H 0 3(2)[of i j l] have "… = (¬ tr_lookup T (i + ii) (j + ii))" by simp
finally show ?thesis by simp
next
case (Suc i')
have "⋀i j k. ⟦i < length xs; j < length xs; xs ! i = Some k⟧ ⟹ (xs ! j = Some k) = (¬ tr_lookup T (i + Suc ii) (j + Suc ii))" proof -
fix i j k assume "i < length xs" "j < length xs" "xs ! i = Some k"
with 3(2)[of "Suc i" "Suc j" k] show "(xs ! j = Some k) = (¬ tr_lookup T (i + Suc ii) (j + Suc ii))" by simp
qed moreover
note 3(3) moreover
have "⋀x k. ⟦x ∈ set xs; x = Some k⟧ ⟹ k < length zs" proof -
fix x k assume "x ∈ set xs" "x = Some k"
with 3(4)[of x k] show "k < length zs" by simp
qed moreover
from 3(5) H Suc J have "length xs + Suc ii = length T + 1" "i' < length xs" "j' < length xs" by simp+
ultimately have "(fst (mk_eqcl xs zs (Suc ii) T) ! i' = fst (mk_eqcl xs zs (Suc ii) T) ! j') = (¬ tr_lookup T (i' + Suc ii) (j' + Suc ii))" by (rule 3(1))
with J Suc show ?thesis by (simp add: split_beta)
qed
} note L = this
have "i < j ∨ i = j ∨ i > j" by auto
thus ?case proof (elim disjE)
assume "i > j"
with 3(6) L have "(fst (mk_eqcl (Some l # xs) zs ii T) ! j = fst (mk_eqcl (Some l # xs) zs ii T) ! i) = (¬ tr_lookup T (j + ii) (i + ii))" by simp
thus ?thesis by (auto simp: tr_lookup_def)
qed (insert 3(7) L, simp add: tr_lookup_def)+
qed

definition min_dfa :: "dfa ⇒ dfa" where
"min_dfa = (λ(bd, as). let (os, ns) = mk_eqcl (replicate (length bd) None) [] 0 (fixpt (bd, as) (init_tr (bd, as))) in
(map (λp. bdd_map (λq. os ! q) (bd ! p)) ns, map (λp. as ! p) ns))"

definition eq_nodes :: "dfa ⇒ nat ⇒ nat ⇒ nat ⇒ bool" where
"eq_nodes = (λM v p q. ¬ (∃n. dist_nodes M n v p q))"

lemma mk_eqcl_fixpt_fst_bound:
assumes "dfa_is_node M i"
shows "fst (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! i < length (snd (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))))"
(is "fst ?M ! i < length (snd ?M)")
proof -
{ fix x k assume H: "x ∈ set (replicate (length (fst M)) (None::nat option))" "x = Some k"
hence "k < length []" by (cases "length (fst M) = 0") simp+
} moreover
from assms have "fst ?M ! i ∈ set (fst ?M)" by (simp add: dfa_is_node_def mk_eqcl_len_fst)
ultimately show ?thesis by (rule mk_eqcl_bound)
qed

lemma mk_eqcl_fixpt_fst_nth:
assumes "wf_dfa M v"
and "dfa_is_node M p" and "dfa_is_node M q"
shows "(fst (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! p = fst (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! q)
= eq_nodes M v p q"
(is "(fst ?M ! p = fst ?M ! q) = eq_nodes M v p q")
proof -
have WF: "wf_tr M (fixpt M (init_tr M))" by (simp only: fixpt_wf init_tr_wf)

have "(fst ?M ! p = fst ?M ! q) = (¬ tr_lookup (fixpt M (init_tr M)) p q)" proof -
{ fix i j k assume H: "i < length (replicate (length (fst M)) None)" "j < length (replicate (length (fst M)) None)" "replicate (length (fst M)) None ! i = Some k"
hence "(replicate (length (fst M)) None ! j = Some k) = (¬ tr_lookup (fixpt M (init_tr M)) (i + 0) (j + 0))" by simp
}
moreover
have "⋀a b c. ⟦a ≤ length (fixpt M (init_tr M)); b ≤ length (fixpt M (init_tr M)); c ≤ length (fixpt M (init_tr M)); ¬ tr_lookup (fixpt M (init_tr M)) a b; ¬ tr_lookup (fixpt M (init_tr M)) b c⟧
⟹ ¬ tr_lookup (fixpt M (init_tr M)) a c" proof -
fix a b c assume H': "a ≤ length (fixpt M (init_tr M))" "b ≤ length (fixpt M (init_tr M))" "c ≤ length (fixpt M (init_tr M))" "¬ tr_lookup (fixpt M (init_tr M)) a b"
"¬ tr_lookup (fixpt M (init_tr M)) b c"
{ fix q assume H'': "q ≤ length (fixpt M (init_tr M))"
from assms have "length (fst M) > 0" by (simp add: wf_dfa_def)
then obtain m where M: "length (fst M) = Suc m" by (cases "length (fst M)") simp+
hence M': "m = length (fst M) - 1" by simp
with H'' WF have "q ≤ m" by (simp add: wf_tr_def)
with M have "q < length (fst M)" by simp
}
with H' have D: "dfa_is_node M a" "dfa_is_node M b" "dfa_is_node M c" by (auto simp: dfa_is_node_def)
with H'(4,5) assms(1) have "¬ (∃n. dist_nodes M n v a b)" "¬ (∃n. dist_nodes M n v b c)" by (simp add: fixpt_dist_nodes[symmetric])+
hence "¬ (∃n. dist_nodes M n v a c)" by (auto simp: dist_nodes_def)
with H' assms D show "¬ tr_lookup (fixpt M (init_tr M)) a c" by (simp add: fixpt_dist_nodes[symmetric])
qed
moreover have "⋀x k. ⟦x ∈ set (replicate (length (fst M)) None); x = Some k⟧ ⟹ k < length []" proof -
fix x k assume "x ∈ set (replicate (length (fst M)) (None::nat option))" "x = Some k"
thus "k < length []" by (cases "length (fst M) = 0") simp+
qed
moreover from WF assms have "length (replicate (length (fst M)) None) + 0 = length (fixpt M (init_tr M)) + 1" by (simp add: wf_tr_def wf_dfa_def)
moreover from assms have "p < length (replicate (length (fst M)) None)" "q < length (replicate (length (fst M)) None)" by (simp add: dfa_is_node_def)+
ultimately have "(fst ?M ! p = fst ?M ! q) = (¬ tr_lookup (fixpt M (init_tr M)) (p+0) (q+0))" by (rule mk_eqcl_fst_nth)
thus ?thesis by simp
qed
also from assms have "… = eq_nodes M v p q" by (simp only: fixpt_dist_nodes eq_nodes_def)
finally show ?thesis by simp
qed

lemma mk_eqcl_fixpt_fst_snd_nth:
assumes "i < length (snd (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))))"
and "wf_dfa M v"
shows "snd (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! i < length (fst (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M)))) ∧
fst (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! (snd (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! i) = i"
(is "snd ?M ! i < length (fst ?M) ∧ fst ?M ! (snd ?M ! i) = i")
proof -
have "⋀i. i < length [] ⟹ [] ! i < length (replicate (length (fst M)) None) + 0 ∧ (0 ≤ [] ! i ⟶ replicate (length (fst M)) None ! ([] ! i - 0) = Some i)" by simp
moreover have "⋀j1 j2. ⟦j1 < j2; j2 < length []⟧ ⟹ [] ! j1 < [] ! j2" by simp
moreover have "⋀z. z ∈ set [] ⟹ z < 0" by simp
moreover note assms(1)
moreover have "length (replicate (length (fst M)) None) + 0 ≤ length (fixpt M (init_tr M)) + 1" proof -
have WF: "wf_tr M (fixpt M (init_tr M))" by (simp only: init_tr_wf fixpt_wf)
from assms have "length (fst M) > 0" by (simp add: wf_dfa_def)
then obtain m where M:"length (fst M) = Suc m" by (cases "length (fst M)") simp+
hence M': "m = length (fst M) - 1" by simp
with WF have "length (fixpt M (init_tr M)) = m" by (simp add: wf_tr_def)
with M show ?thesis by simp
qed
ultimately have "snd ?M ! i < length (fst ?M) + 0 ∧ (0 ≤ snd ?M ! i ⟶ fst ?M ! (snd ?M ! i - 0) = i)" by (rule mk_eqcl_fst_snd)
thus ?thesis by simp
qed

lemma eq_nodes_dfa_trans:
assumes "eq_nodes M v p q"
and "is_alph v bs"
shows "eq_nodes M v (dfa_trans M p bs) (dfa_trans M q bs)"
proof (rule ccontr)
assume H: "¬ eq_nodes M v (dfa_trans M p bs) (dfa_trans M q bs)"
then obtain n w where "length w = n" "list_all (is_alph v) w" "dfa_accepting M (dfa_steps M (dfa_trans M p bs) w) ≠ dfa_accepting M (dfa_steps M (dfa_trans M q bs) w)"
unfolding eq_nodes_def dist_nodes_def by blast
with assms have "length (bs # w) = Suc n" "list_all (is_alph v) (bs # w)" "dfa_accepting M (dfa_steps M p (bs # w)) ≠ dfa_accepting M (dfa_steps M q (bs # w))" by simp+
hence "¬ eq_nodes M v p q" unfolding eq_nodes_def dist_nodes_def by blast
with assms show False by simp
qed

lemma mk_eqcl_fixpt_trans:
assumes "wf_dfa M v"
and "dfa_is_node M p"
and "is_alph v bs"
shows "dfa_trans (min_dfa M) (fst (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! p) bs =
fst (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! (dfa_trans M p bs)"
(is "dfa_trans (min_dfa M) (fst ?M ! p) bs = fst ?M ! (dfa_trans M p bs)")
proof -
let ?q = "snd ?M ! (fst ?M ! p)"
from assms have I1: "?q < length (fst ?M)" "fst ?M ! ?q = fst ?M ! p" by (simp add: mk_eqcl_fixpt_fst_bound mk_eqcl_fixpt_fst_snd_nth)+
with assms have I2: "bddh (length bs) (fst M ! ?q)" by (simp add: mk_eqcl_len_fst wf_dfa_def list_all_iff is_alph_def)
from I1 have I3: "dfa_is_node M ?q" by (simp add: mk_eqcl_len_fst dfa_is_node_def)
with assms I1 have "eq_nodes M v p ?q" by (simp add: mk_eqcl_fixpt_fst_nth[symmetric])
with assms have "eq_nodes M v (dfa_trans M p bs) (dfa_trans M ?q bs)" by (simp add: eq_nodes_dfa_trans)
with assms I3 have "fst ?M ! (dfa_trans M p bs) = fst ?M ! (dfa_trans M ?q bs)" by (simp add: dfa_trans_is_node mk_eqcl_fixpt_fst_nth)

with assms I2 show ?thesis by (simp add: dfa_trans_def min_dfa_def split_beta mk_eqcl_fixpt_fst_bound bdd_map_bdd_lookup)
qed

lemma mk_eqcl_fixpt_steps:
assumes "wf_dfa M v"
and "dfa_is_node M p"
and "list_all (is_alph v) w"
shows "dfa_steps (min_dfa M) (fst (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! p) w =
fst (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! (dfa_steps M p w)"
(is "dfa_steps (min_dfa M) (fst ?M ! p) w = fst ?M ! (dfa_steps M p w)")
using assms by (induct w arbitrary: p) (simp add: mk_eqcl_fixpt_trans dfa_trans_is_node)+

lemma mk_eqcl_fixpt_startnode:
assumes "length (fst M) > 0"
shows "length (snd (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M)))) > 0 ∧
fst (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! 0 = 0 ∧ snd (mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))) ! 0 = 0"
(is "length (snd ?M) > 0 ∧ fst ?M ! 0 = 0 ∧ snd ?M ! 0 = 0")
proof -
from assms obtain k where K: "length (fst M) = Suc k" by (cases "length (fst M)") simp+
from K have "length (snd ?M) = length (snd (mk_eqcl (mk_eqcl' (replicate k None) 0 (Suc 0) 0 (fixpt M (init_tr M))) [0] (Suc 0) (fixpt M (init_tr M))))" by (simp add: split_beta)
also have "… ≥ length [0::nat]" by (simp only: mk_eqcl_len_snd)
finally have "length (snd ?M) > 0" by auto
with K show ?thesis by (simp add: split_beta mk_eqcl_snd_nth)
qed

lemma min_dfa_wf:
"wf_dfa M v ⟹ wf_dfa (min_dfa M) v"
proof -
assume H: "wf_dfa M v"
obtain bd as where "min_dfa M = (bd, as)" by (cases "min_dfa M") auto
hence M: "bd = fst (min_dfa M)" "as = snd (min_dfa M)" by simp+
let ?M = "mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))"

{ fix x assume "x ∈ set bd"
then obtain i where I: "i < length bd" "x = bd ! i" by (auto simp: in_set_conv_nth)

with M H have "snd ?M ! i < length (fst ?M)" by (simp add: min_dfa_def split_beta mk_eqcl_fixpt_fst_snd_nth)
hence N: "dfa_is_node M (snd ?M ! i)" by (simp add: mk_eqcl_len_fst dfa_is_node_def)
with H have BH: "bddh v (fst M ! (snd ?M ! i))" by (simp add: wf_dfa_def list_all_iff dfa_is_node_def)

from I M have BI: "bd ! i = bdd_map (λq. fst ?M ! q) (fst M ! (snd ?M ! i))" by (simp add: split_beta min_dfa_def)
with BH have G1: "bddh v (bd ! i)" by (simp add: bddh_bdd_map)

from H N have "bdd_all (dfa_is_node M) (fst M ! (snd ?M ! i))" by (simp add: wf_dfa_def list_all_iff dfa_is_node_def)
moreover
{ fix q assume "dfa_is_node M q"
hence "fst ?M ! q < length (snd ?M)" by (simp add: mk_eqcl_fixpt_fst_bound)
hence "dfa_is_node (min_dfa M) (fst ?M ! q)" by (simp add: dfa_is_node_def min_dfa_def split_beta)
}
ultimately have "bdd_all (dfa_is_node (min_dfa M)) (bdd_map (λq. fst ?M ! q) (fst M ! (snd ?M ! i)))" by (simp add: bdd_all_bdd_map)
with G1 BI I have "bddh v x ∧ bdd_all (dfa_is_node (min_dfa M)) x" by simp
}
hence G: "list_all (bddh v) bd ∧ list_all (bdd_all (dfa_is_node (min_dfa M))) bd" by (simp add: list_all_iff)

from H have "length (fst M) > 0" by (simp add: wf_dfa_def)
hence "length (snd ?M) > 0" by (auto simp only: mk_eqcl_fixpt_startnode)

with G M show "wf_dfa (min_dfa M) v" by (simp add: wf_dfa_def min_dfa_def split_beta)
qed

lemma min_dfa_accept:
assumes "wf_dfa M v"
and "list_all (is_alph v) w"
shows "dfa_accepts (min_dfa M) w = dfa_accepts M w"
proof -
let ?M = "mk_eqcl (replicate (length (fst M)) None) [] 0 (fixpt M (init_tr M))"

from assms have "length (fst M) > 0" by (simp add: wf_dfa_def)
hence SN: "length (snd ?M) > 0 ∧ fst ?M ! 0 = 0 ∧ snd ?M ! 0 = 0" by (auto simp only: mk_eqcl_fixpt_startnode)
have D: "dfa_steps (min_dfa M) 0 w = fst ?M ! dfa_steps M 0 w" proof -
from assms have "dfa_is_node M 0" by (simp add: wf_dfa_def dfa_is_node_def)
moreover from SN have "dfa_steps (min_dfa M) 0 w = dfa_steps (min_dfa M) (fst ?M ! 0) w" by simp
moreover note assms
ultimately show ?thesis by (simp add: mk_eqcl_fixpt_steps)
qed

from assms have WF: "wf_dfa (min_dfa M) v" by (simp add: min_dfa_wf)
hence "dfa_is_node (min_dfa M) 0" by (simp add: dfa_startnode_is_node)
with WF assms have "dfa_is_node (min_dfa M) (dfa_steps (min_dfa M) 0 w)" by (simp add: dfa_steps_is_node)
with D have DN: "dfa_is_node (min_dfa M) (fst ?M ! dfa_steps M 0 w)" by simp

let ?q = "snd ?M ! (fst ?M ! dfa_steps M 0 w)"

from assms have N: "dfa_is_node M (dfa_steps M 0 w)" by (simp add: dfa_steps_is_node dfa_startnode_is_node)
with assms have I: "?q < length (fst ?M)" "fst ?M ! ?q = fst ?M ! dfa_steps M 0 w" by (simp add: mk_eqcl_fixpt_fst_bound mk_eqcl_fixpt_fst_snd_nth)+
hence "dfa_is_node M ?q" by (simp add: mk_eqcl_len_fst dfa_is_node_def)
with assms N I have EQ: "eq_nodes M v (dfa_steps M 0 w) ?q" by (simp add: mk_eqcl_fixpt_fst_nth[symmetric])
have A: "dfa_accepting M (dfa_steps M 0 w) = dfa_accepting M ?q" proof (rule ccontr)
assume H: "dfa_accepting M (dfa_steps M 0 w) ≠ dfa_accepting M ?q"
hence "dist_nodes M 0 v (dfa_steps M 0 w) ?q" by (auto simp: dist_nodes_def)
with EQ show False by (simp add: eq_nodes_def)
qed

from D have "dfa_accepts (min_dfa M) w = snd (min_dfa M) ! (fst ?M ! dfa_steps M 0 w)" by (simp add: accepts_def dfa_accepting_def)
also from WF DN have "… = dfa_accepting M ?q" by (simp add: dfa_is_node_def wf_dfa_def min_dfa_def split_beta dfa_accepting_def)
also from A have "… = dfa_accepts M w" by (simp add: accepts_def)

finally show ?thesis by simp
qed

section ‹NFAs›

type_synonym nbddtable = "bool list bdd list"
type_synonym nfa = "nbddtable × astate"

definition
nfa_is_node :: "nfa ⇒ bool list ⇒ bool" where
"nfa_is_node A = (λqs. length qs = length (fst A))"

definition
wf_nfa :: "nfa ⇒ nat ⇒ bool" where
"wf_nfa A n =
(list_all (bddh n) (fst A) ∧
list_all (bdd_all (nfa_is_node A)) (fst A) ∧
length (snd A) = length (fst A) ∧
length (fst A) > 0)"

definition
set_of_bv :: "bool list ⇒ nat set" where
"set_of_bv bs = {i. i < length bs ∧ bs ! i}"

fun
bv_or :: "bool list ⇒ bool list ⇒ bool list"
where
"bv_or [] [] = []" |
"bv_or (x # xs) (y # ys) = (x ∨ y) # (bv_or xs ys)"

lemma bv_or_nth:
assumes "length l = length r"
assumes "i < length l"
shows "bv_or l r ! i = (l ! i ∨ r ! i)"
using assms proof (induct l r arbitrary: i rule: bv_or.induct)
case (2 xx xss yy yss ii)
have "ii = 0 ∨ ii > 0" by auto
thus ?case proof (elim disjE)
assume "ii > 0"
then obtain j where J: "ii = Suc j" by (induct ii) simp+
with 2 show ?thesis by simp
qed simp
qed simp+

lemma bv_or_length:
assumes "length l = length r"
shows "length (bv_or l r) = length l"
using assms by (induct l r rule: bv_or.induct) simp+

lemma bv_or_set_of_bv:
assumes "nfa_is_node A p" and "nfa_is_node A q"
shows "set_of_bv (bv_or p q) = set_of_bv p ∪ set_of_bv q"
using assms by (auto simp: nfa_is_node_def set_of_bv_def bv_or_length bv_or_nth)

lemma bv_or_is_node: "⟦nfa_is_node A p; nfa_is_node A q⟧ ⟹ nfa_is_node A (bv_or p q)"
by (simp add: bv_or_length nfa_is_node_def)

fun subsetbdd
where
"subsetbdd [] [] bdd = bdd"
| "subsetbdd (bdd' # bdds) (b # bs) bdd =
(if b then subsetbdd bdds bs (bdd_binop bv_or bdd bdd') else subsetbdd bdds bs bdd)"

definition
nfa_emptybdd :: "nat ⇒ bool list bdd" where
"nfa_emptybdd n = Leaf (replicate n False)"

lemma bdd_all_is_node_subsetbdd:
assumes "list_all (bdd_all (nfa_is_node A)) (fst A)"
and "nfa_is_node A q"
shows "bdd_all (nfa_is_node A) (subsetbdd (fst A) q (nfa_emptybdd (length q)))"
proof -
{ fix bdds :: "bool list bdd list" and q :: "bool list" and bd :: "bool list bdd" and n
assume "list_all (bdd_all (λl. length l = n)) bdds" and "bdd_all (λl. length l = n) bd" and "length bdds = length q"
hence "bdd_all (λl. length l = n) (subsetbdd bdds q bd)" by (induct bdds q bd rule: subsetbdd.induct) (simp add: bdd_all_bdd_binop[of "λl. length l =n" _ "λl. length l = n"] bv_or_length)+
}
with assms show ?thesis by (simp add: nfa_is_node_def nfa_emptybdd_def)
qed

lemma bddh_subsetbdd:
assumes "list_all (bddh l) (fst A)"
and "bddh l bdd'"
and "nfa_is_node A q"
shows "bddh l (subsetbdd (fst A) q bdd')"
using assms unfolding nfa_is_node_def by (induct ("fst A") q bdd' rule: subsetbdd.induct) (simp add: bddh_binop)+

lemma bdd_lookup_subsetbdd':
assumes "length bdds = length q"
and "∀x ∈ set bdds. bddh (length ws) x"
and "bddh (length ws) obdd"
and "⋀bs w. ⟦bs ∈ set bdds; length w = length ws⟧ ⟹ length (bdd_lookup bs w) = c"
and "⋀w. length w = length ws ⟹ length (bdd_lookup obdd w) = c"
and "a < c"
shows "bdd_lookup (subsetbdd bdds q obdd) ws ! a = ((∃i < length q. q ! i ∧ bdd_lookup (bdds ! i) ws ! a) ∨ bdd_lookup obdd ws ! a)"
using assms proof (induct bdds q obdd rule: subsetbdd.induct)
case (2 bdd' bdds x xs bdd)
show ?case proof (cases x)
case True
with 2 have H: "bdd_lookup (subsetbdd bdds xs (bdd_binop bv_or bdd bdd')) ws ! a =
((∃i<length xs. xs ! i ∧ bdd_lookup (bdds ! i) ws ! a) ∨ bdd_lookup (bdd_binop bv_or bdd bdd') ws ! a)" by (simp add: bddh_binop bdd_lookup_binop bv_or_length)
from 2 have "((∃i < length xs. xs ! i ∧ bdd_lookup (bdds ! i) ws ! a) ∨ bdd_lookup (bdd_binop bv_or bdd bdd') ws ! a) =
((∃i < length xs. xs ! i ∧ bdd_lookup (bdds ! i) ws ! a) ∨ (bdd_lookup bdd' ws) ! a ∨ (bdd_lookup bdd ws) ! a)" by (auto simp: bdd_lookup_binop bv_or_nth)
also have "… = ((∃i < Suc (length xs). (True # xs) ! i ∧ bdd_lookup ((bdd' # bdds) ! i) ws ! a) ∨ bdd_lookup bdd ws ! a)"
(is "((∃i. ?P i) ∨ ?Q ∨ ?R) = ((∃i. ?S i) ∨ ?R)") proof
assume "(∃i. ?P i) ∨ ?Q ∨ ?R" thus "(∃i. ?S i) ∨ ?R" by (elim disjE) auto
next
assume "(∃i. ?S i) ∨ ?R" thus "(∃i. ?P i) ∨ ?Q ∨ ?R" proof (elim disjE)
assume "∃i. ?S i"
then obtain i where I: "?S i" ..
{ assume "i = 0" with I have "?Q" by simp }
{ assume "i ≠ 0" then obtain j where "i = Suc j" by (cases i) simp+ with I have "∃j. ?P j" by auto }
with ‹i=0 ⟹ ?Q› show ?thesis by (cases "i=0") simp+
qed simp
qed
finally have "((∃i<length xs. xs ! i ∧ bdd_lookup (bdds ! i) ws ! a) ∨ bdd_lookup (bdd_binop bv_or bdd bdd') ws ! a) =
((∃i<Suc (length xs). (True # xs) ! i ∧ bdd_lookup ((bdd' # bdds) ! i) ws ! a) ∨ bdd_lookup bdd ws ! a)" by simp
with True H show ?thesis by simp
next
case False
with 2 have H: "bdd_lookup (subsetbdd bdds xs bdd) ws ! a = ((∃i < length xs. xs ! i ∧ bdd_lookup (bdds ! i) ws ! a) ∨ bdd_lookup bdd ws ! a)" by simp
have "((∃i<length xs. xs ! i ∧ bdd_lookup (bdds ! i) ws ! a) ∨ bdd_lookup bdd ws ! a) =
((∃i<Suc (length xs). (False # xs) ! i ∧ bdd_lookup ((bdd' # bdds) ! i) ws ! a) ∨ bdd_lookup bdd ws ! a)"
(is "((∃i. ?S i) ∨ ?R) = ((∃i. ?P i) ∨ ?R)") proof
assume "(∃i. ?S i) ∨ ?R" thus "(∃i. ?P i) ∨ ?R" by (elim disjE) auto
next
assume "(∃i. ?P i) ∨ ?R" thus "(∃i. ?S i) ∨ ?R" proof (elim disjE)
assume "∃i. ?P i"
then obtain i where "?P i" ..
then obtain j where "i = Suc j" by (cases i) simp+
with ‹?P i› show ?thesis by auto
qed simp
qed
with False H show ?thesis by simp
qed
qed simp+

lemma bdd_lookup_subsetbdd:
assumes "wf_nfa N (length ws)"
and "nfa_is_node N q"
and "a < length (fst N)"
shows "bdd_lookup (subsetbdd (fst N) q (nfa_emptybdd (length q))) ws ! a = (∃i< length q. q ! i ∧ bdd_lookup (fst N ! i) ws ! a)"
proof -
{
fix w :: "bool list"
assume H: "length w = length ws"
from assms have "∀bd ∈ set (fst N). bdd_all (nfa_is_node N) bd" by (simp add: wf_nfa_def list_all_iff) moreover
from assms have "∀bd ∈ set (fst N). bddh (length ws) bd" by (simp add: wf_nfa_def list_all_iff) moreover
note H
ultimately have "∀bd ∈ set (fst N). nfa_is_node N (bdd_lookup bd w)" by (simp add: bdd_all_bdd_lookup)
}
with assms have "bdd_lookup (subsetbdd (fst N) q (nfa_emptybdd (length q))) ws ! a = ((∃i < length q. q ! i ∧ bdd_lookup (fst N ! i) ws ! a) ∨ bdd_lookup (nfa_emptybdd (length q)) ws ! a)"
by (simp add: bdd_lookup_subsetbdd' nfa_is_node_def wf_nfa_def list_all_iff nfa_emptybdd_def)
with assms show ?thesis by (auto simp: nfa_emptybdd_def nfa_is_node_def)
qed

definition
nfa_trans :: "nfa ⇒ bool list ⇒ bool list ⇒ bool list" where
"nfa_trans A qs bs = bdd_lookup (subsetbdd (fst A) qs (nfa_emptybdd (length qs))) bs"

fun nfa_accepting' :: "bool list ⇒ bool list ⇒ bool" where
"nfa_accepting' [] bs = False"
| "nfa_accepting' as [] = False"
| "nfa_accepting' (a # as) (b # bs) = (a ∧ b ∨ nfa_accepting' as bs)"
definition nfa_accepting :: "nfa ⇒ bool list ⇒ bool" where
"nfa_accepting A = nfa_accepting' (snd A)"

lemma nfa_accepting'_set_of_bv: "nfa_accepting' l r = (set_of_bv l ∩ set_of_bv r ≠ {})"
proof -
have nfa_accepting_help: "⋀as q. nfa_accepting' as q = (∃i. i < length as ∧ i < length q ∧ as ! i ∧ q ! i)"
proof -
fix as q
show "nfa_accepting' as q = (∃i < length as. i < length q ∧ as ! i ∧ q ! i)"
proof (induct as q rule: nfa_accepting'.induct)
case (3 a as q qs)
thus ?case proof (cases "a∧q")
case False
with 3 have "nfa_accepting' as qs = (∃i < length as. i < length qs ∧ as ! i ∧ qs ! i)" (is "?T = _") by simp
also have "… = (∃j < length as. j < length qs ∧ (a#as) ! Suc j ∧ (q#qs) ! Suc j)" by simp
also have "… = (∃j < length (a#as). j < length (q#qs) ∧ (a#as) ! j ∧ (q#qs) ! j)" (is "(∃j. ?P j) = (∃j. ?Q j)")
proof
assume "∃j. ?P j"
then obtain j where "?P j" ..
hence "?Q (Suc j)" by simp
thus "∃j. ?Q j" by (rule exI)
next
assume "∃j. ?Q j"
then obtain j where J: "?Q j" ..
with False obtain i where "j = Suc i" by (cases j) simp+
with J have "?P i" by simp
thus "∃i. ?P i" by (rule exI)
qed
also from False have "… = ((a∧q ∧ ?Q 0) ∨ (¬ (a∧q) ∧ (∃j. ?Q j)))" by auto
also have "… = ((a ∧ q ∧ (∃j. ?Q j)) ∨ (¬(a∧q) ∧ (∃j. ?Q j)))" by auto
also have "… = (∃j. ?Q j)" by auto
finally have "?T = (∃j. ?Q j)" .
with False show ?thesis by auto
qed (auto simp: 3)
qed simp+
qed
hence "nfa_accepting' l r = (∃i. i < length l ∧ i < length r ∧ l ! i ∧ r ! i)" by simp
also have "… = (∃i. i ∈ set_of_bv l ∧ i ∈ set_of_bv r)" by (auto simp: set_of_bv_def)
also have "… = (set_of_bv l ∩ set_of_bv r ≠ {})" by auto
finally show ?thesis .
qed

lemma nfa_accepting_set_of_bv: "nfa_accepting A q = (set_of_bv (snd A) ∩ set_of_bv q ≠ {})"
by (simp add: nfa_accepting'_set_of_bv nfa_accepting_def)

definition
nfa_startnode :: "nfa ⇒ bool list" where
"nfa_startnode A = (replicate (length (fst A)) False)[0:=True]"

locale aut_nfa =
fixes A n
assumes well_formed: "wf_nfa A n"

sublocale aut_nfa < Automaton "nfa_trans A" "nfa_is_node A" "is_alph n"
proof
fix q a
assume Q: "nfa_is_node A q" and A: "is_alph n a"
with well_formed have "bdd_all (nfa_is_node A) (subsetbdd (fst A) q (nfa_emptybdd (length q)))"
by (simp add: wf_nfa_def bdd_all_is_node_subsetbdd)
moreover from well_formed Q have "bddh n (subsetbdd (fst A) q (nfa_emptybdd (length q)))"
by (simp add: wf_nfa_def nfa_emptybdd_def bddh_subsetbdd)
with A have "bddh (length a) (subsetbdd (fst A) q (nfa_emptybdd (length q)))" by (simp add: is_alph_def)
ultimately have "nfa_is_node A (bdd_lookup (subsetbdd (fst A) q (nfa_emptybdd (length q))) a)"
by (simp add: bdd_all_bdd_lookup)
then show "nfa_is_node A (nfa_trans A q a)" by (simp add: nfa_trans_def)
qed

context aut_nfa begin
lemmas trans_is_node = trans_is_node
lemmas steps_is_node = steps_is_node
lemmas reach_is_node = reach_is_node
end

lemmas nfa_trans_is_node = aut_nfa.trans_is_node [OF aut_nfa.intro]
lemmas nfa_steps_is_node = aut_nfa.steps_is_node [OF aut_nfa.intro]
lemmas nfa_reach_is_node = aut_nfa.reach_is_node [OF aut_nfa.intro]

abbreviation "nfa_steps A ≡ foldl (nfa_trans A)"
abbreviation "nfa_accepts A ≡ accepts (nfa_trans A) (nfa_accepting A) (nfa_startnode A)"
abbreviation "nfa_reach A ≡ reach (nfa_trans A)"

lemma nfa_startnode_is_node: "wf_nfa A n ⟹ nfa_is_node A (nfa_startnode A)"
by (simp add: nfa_is_node_def wf_nfa_def nfa_startnode_def)

section ‹Automata Constructions›

subsection ‹Negation›

definition
negate_dfa :: "dfa ⇒ dfa" where
"negate_dfa = (λ(t,a). (t, map Not a))"

lemma negate_wf_dfa: "wf_dfa (negate_dfa A) l = wf_dfa A l"
by (simp add: negate_dfa_def wf_dfa_def dfa_is_node_def split_beta)

lemma negate_negate_dfa: "negate_dfa (negate_dfa A) = A"
proof (induct A)
case (Pair t a) thus ?case by (induct a) (simp add: negate_dfa_def)+
qed

lemma dfa_accepts_negate:
assumes "wf_dfa A n"
and "list_all (is_alph n) bss"
shows "dfa_accepts (negate_dfa A) bss = (¬ dfa_accepts A bss)"
proof -
have "dfa_steps (negate_dfa A) 0 bss = dfa_steps A 0 bss"
by (simp add: negate_dfa_def dfa_trans_def [abs_def] split_beta)
moreover from assms have "dfa_is_node A (dfa_steps A 0 bss)"
by (simp add: dfa_steps_is_node dfa_startnode_is_node)
ultimately show ?thesis using assms
by (simp add: accepts_def dfa_accepting_def wf_dfa_def dfa_is_node_def negate_dfa_def split_beta)
qed

subsection ‹Product Automaton›

definition
prod_succs :: "dfa ⇒ dfa ⇒ nat × nat ⇒ (nat × nat) list" where
"prod_succs A B = (λ(i, j). add_leaves (bdd_binop Pair (fst A ! i) (fst B ! j)) [])"

definition
"prod_is_node A B = (λ(i, j). dfa_is_node A i ∧ dfa_is_node B j)"

definition
prod_invariant :: "dfa ⇒ dfa ⇒ nat option list list × (nat × nat) list ⇒ bool" where
"prod_invariant A B = (λ(tab, ps).
length tab = length (fst A) ∧ (∀tab'∈set tab. length tab' = length (fst B)))"

definition
"prod_ins = (λ(i, j). λ(tab, ps).
(tab[i := (tab ! i)[j := Some (length ps)]],
ps @ [(i, j)]))"

definition
prod_memb :: "nat × nat ⇒ nat option list list × (nat × nat) list ⇒ bool" where
"prod_memb = (λ(i, j). λ(tab, ps). tab ! i ! j ≠ None)"

definition
prod_empt :: "dfa ⇒ dfa ⇒ nat option list list × (nat × nat) list" where
"prod_empt A B = (replicate (length (fst A)) (replicate (length (fst B)) None), [])"

definition
prod_dfs :: "dfa ⇒ dfa ⇒ nat × nat ⇒ nat option list list × (nat × nat) list" where
"prod_dfs A B x = gen_dfs (prod_succs A B) prod_ins prod_memb (prod_empt A B) [x]"

definition
binop_dfa :: "(bool ⇒ bool ⇒ bool) ⇒ dfa ⇒ dfa ⇒ dfa" where
"binop_dfa f A B =
(let (tab, ps) = prod_dfs A B (0, 0)
in
(map (λ(i, j). bdd_binop (λk l. the (tab ! k ! l)) (fst A ! i) (fst B ! j)) ps,
map (λ(i, j). f (snd A ! i) (snd B ! j)) ps))"

locale prod_DFS =
fixes A B n
assumes well_formed1: "wf_dfa A n"
and well_formed2: "wf_dfa B n"

sublocale prod_DFS < DFS "prod_succs A B" "prod_is_node A B" "prod_invariant A B" prod_ins prod_memb "prod_empt A B"
apply unfold_locales
apply (simp add: prod_memb_def prod_ins_def prod_invariant_def
prod_is_node_def split_paired_all dfa_is_node_def)
apply (case_tac "a = aa")
apply (case_tac "b = ba")
apply auto[3]
apply (simp add: prod_memb_def prod_empt_def prod_is_node_def split_paired_all dfa_is_node_def)
apply (insert well_formed1 well_formed2)[]
apply (simp add: prod_is_node_def prod_succs_def split_paired_all dfa_is_node_def wf_dfa_def)
apply (drule conjunct1 [OF conjunct2])+
apply (simp add: list_all_iff)
apply (rule ballI)
apply (simp add: split_paired_all)
apply (drule subsetD [OF add_leaves_binop_subset [where xs="[]" and ys="[]", simplified]])
apply clarify
apply (drule_tac x="fst A ! a" in bspec)
apply simp
apply (drule_tac x="fst B ! b" in bspec)
apply simp
apply (simp add: prod_invariant_def prod_empt_def set_replicate_conv_if)
apply (simp add: prod_is_node_def prod_invariant_def
prod_memb_def prod_ins_def split_paired_all dfa_is_node_def)
apply (rule ballI)
apply (drule subsetD [OF set_update_subset_insert])
apply auto
apply (simp add: prod_is_node_def dfa_is_node_def)
done

context prod_DFS
begin

lemma prod_dfs_eq_rtrancl: "prod_is_node A B x ⟹ prod_is_node A B y ⟹
prod_memb y (prod_dfs A B x) = ((x, y) ∈ (succsr (prod_succs A B))⇧*)"
by (unfold prod_dfs_def) (rule dfs_eq_rtrancl)

lemma prod_dfs_bij:
assumes x: "prod_is_node A B x"
shows "(fst (prod_dfs A B x) ! i ! j = Some k ∧ dfa_is_node A i ∧ dfa_is_node B j) =
(k < length (snd (prod_dfs A B x)) ∧ (snd (prod_dfs A B x) ! k = (i, j)))"
proof -
from x have "list_all (prod_is_node A B) [x]" by simp
with empt_invariant
have "(fst (dfs (prod_empt A B) [x]) ! i ! j = Some k ∧ dfa_is_node A i ∧ dfa_is_node B j) =
(k < length (snd (dfs (prod_empt A B) [x])) ∧ (snd (dfs (prod_empt A B) [x]) ! k = (i, j)))"
proof (induct rule: dfs_invariant)
case base
show ?case
by (auto simp add: prod_empt_def dfa_is_node_def)
next
case (step S y)
obtain y1 y2 where y: "y = (y1, y2)" by (cases y)
show ?case
proof (cases "y1 = i")
case True
show ?thesis
proof (cases "y2 = j")
case True
with step y ‹y1 = i› show ?thesis
by (auto simp add: prod_ins_def prod_memb_def split_beta nth_append
prod_invariant_def prod_is_node_def dfa_is_node_def)
next
case False
with step y ‹y1 = i› show ?thesis
by (auto simp add: prod_ins_def prod_memb_def split_beta nth_append
prod_invariant_def prod_is_node_def dfa_is_node_def)
qed
next
case False
with step y show ?thesis
by (auto simp add: prod_ins_def prod_memb_def split_beta nth_append)
qed
qed
then show ?thesis by (simp add: prod_dfs_def)
qed

lemma prod_dfs_mono:
assumes z: "prod_invariant A B z"
and xs: "list_all (prod_is_node A B) xs"
and H: "fst z ! i ! j = Some k"
shows "fst (gen_dfs (prod_succs A B) prod_ins prod_memb z xs) ! i ! j = Some k"
using z xs
apply (rule dfs_invariant)
apply (rule H)
apply (simp add: prod_ins_def prod_memb_def split_paired_all prod_is_node_def prod_invariant_def)
apply (case_tac "aa = i")
apply (case_tac "ba = j")
apply (simp add: dfa_is_node_def)+
done

lemma prod_dfs_start:
"⟦dfa_is_node A i; dfa_is_node B j⟧ ⟹ fst (prod_dfs A B (i, j)) ! i ! j = Some 0"
apply (simp add: prod_dfs_def empt prod_is_node_def gen_dfs_simps)
apply (rule prod_dfs_mono)
apply (rule ins_invariant)
apply (simp add: prod_is_node_def dfa_is_node_def)
apply (rule empt_invariant)
apply (rule empt)
apply (simp add: prod_is_node_def)
apply (rule succs_is_node)
apply (simp add: prod_is_node_def)
apply (simp add: prod_ins_def prod_empt_def dfa_is_node_def)
done

lemma prod_dfs_inj:
assumes x: "prod_is_node A B x" and i1: "dfa_is_node A i1" and i2: "dfa_is_node B i2"
and j1: "dfa_is_node A j1" and j2: "dfa_is_node B j2"
and i: "fst (prod_dfs A B x) ! i1 ! i2 = Some k"
and j: "fst (prod_dfs A B x) ! j1 ! j2 = Some k"
shows "(i1, i2) = (j1, j2)"
proof -
from x i1 i2 i
have "k < length (snd (prod_dfs A B x)) ∧ snd (prod_dfs A B x) ! k = (i1, i2)"
by (simp add: prod_dfs_bij [symmetric])
moreover from x j1 j2 j
have "k < length (snd (prod_dfs A B x)) ∧ snd (prod_dfs A B x) ! k = (j1, j2)"
by (simp add: prod_dfs_bij [symmetric])
ultimately show ?thesis by simp
qed

lemma prod_dfs_statetrans:
assumes bs: "length bs = n"
and i: "dfa_is_node A i" and j: "dfa_is_node B j"
and s1: "dfa_is_node A s1" and s2: "dfa_is_node B s2"
and k: "fst (prod_dfs A B (s1, s2)) ! i ! j = Some k"
obtains k'
where "fst (prod_dfs A B (s1, s2)) !
dfa_trans A i bs ! dfa_trans B j bs = Some k'"
and "dfa_is_node A (dfa_trans A i bs)"
and "dfa_is_node B (dfa_trans B j bs)"
and "k' < length (snd (prod_dfs A B (s1, s2)))"
proof -
from i well_formed1 bs have h_tr1: "bddh (length bs) (fst A ! i)" by (simp add: wf_dfa_def dfa_is_node_def list_all_iff)
from j well_formed2 bs have h_tr2: "bddh (length bs) (fst B ! j)" by (simp add: wf_dfa_def dfa_is_node_def list_all_iff)
from i j k have "prod_memb (i, j) (prod_dfs A B (s1, s2))"
by (simp add: prod_memb_def split_beta)
then have "((s1, s2), (i, j)) ∈ (succsr (prod_succs A B))⇧*"
using i j s1 s2
by (simp add: prod_dfs_eq_rtrancl prod_is_node_def)
moreover from h_tr1 h_tr2 have "(bdd_lookup (fst A ! i) bs, bdd_lookup (fst B ! j) bs) =
bdd_lookup (bdd_binop Pair (fst A ! i) (fst B ! j)) bs"
by (simp add: bdd_lookup_binop)
with i j h_tr1 h_tr2
have "((i, j), (bdd_lookup (fst A ! i) bs, bdd_lookup (fst B ! j) bs)) ∈
succsr (prod_succs A B)"
by (auto simp add: succsr_def prod_succs_def
add_leaves_bdd_lookup [of "length bs"] bddh_binop is_alph_def)
ultimately have "((s1, s2), (bdd_lookup (fst A ! i) bs, bdd_lookup (fst B ! j) bs)) ∈
(succsr (prod_succs A B))⇧*" ..
moreover from well_formed1 well_formed2 bs i j
have "prod_is_node A B (bdd_lookup (fst A ! i) bs, bdd_lookup (fst B ! j) bs)"
by (auto simp: prod_is_node_def bdd_all_bdd_lookup is_alph_def dfa_trans_is_node dfa_trans_def[symmetric])
moreover from i well_formed1 bs
have s_tr1: "dfa_is_node A (dfa_trans A i bs)"
by (simp add: is_alph_def dfa_trans_is_node)
moreover from j well_formed2 bs
have s_tr2: "dfa_is_node B (dfa_trans B j bs)"
by (simp add: is_alph_def dfa_trans_is_node)
ultimately have "∃k'. fst (prod_dfs A B (s1, s2)) !
dfa_trans A i bs ! dfa_trans B j bs = Some k'"
using s1 s2
by (simp add: prod_dfs_eq_rtrancl [symmetric] prod_memb_def split_beta prod_is_node_def dfa_trans_def)
then obtain k' where k': "fst (prod_dfs A B (s1, s2)) !
dfa_trans A i bs ! dfa_trans B j bs = Some k'" ..
from k' s_tr1 s_tr2 s1 s2
have "k' < length (snd (prod_dfs A B (s1, s2))) ∧
snd (prod_dfs A B (s1, s2)) ! k' = (dfa_trans A i bs, dfa_trans B j bs)"
by (simp add: prod_dfs_bij [symmetric] prod_is_node_def)
then have "k' < length (snd (prod_dfs A B (s1, s2)))" by simp
with k' s_tr1 s_tr2 show ?thesis ..
qed

lemma binop_wf_dfa: "wf_dfa (binop_dfa f A B) n"
proof -
let ?dfa = "binop_dfa f A B"
from well_formed1 well_formed2 have is_node_s1_s2: "prod_is_node A B (0, 0)" by (simp add: prod_is_node_def wf_dfa_def dfa_is_node_def)
let ?tr = "map (λ(i,j). bdd_binop (λk l. the (fst (prod_dfs A B (0, 0)) ! k ! l)) (fst A ! i) (fst B ! j)) (snd (prod_dfs A B (0,0)))"
{
fix i j
assume ij: "(i, j) ∈ set (snd (prod_dfs A B (0, 0)))"
then obtain k where k: "k < length (snd (prod_dfs A B (0, 0)))"
"snd (prod_dfs A B (0, 0)) ! k = (i, j)"
by (auto simp add: in_set_conv_nth)
from conjI [OF k] obtain ij_k: "fst (prod_dfs A B (0,0)) ! i ! j = Some k"
and i: "dfa_is_node A i" and j: "dfa_is_node B j"
by (simp add: prod_dfs_bij [OF is_node_s1_s2, symmetric])
from well_formed1 i have bddh_tr1: "bddh n (fst A ! i)"
and less_tr1: "bdd_all (dfa_is_node A) (fst A ! i)" by (simp add: wf_dfa_def list_all_iff dfa_is_node_def)+
from well_formed2 j have bddh_tr2: "bddh n (fst B ! j)"
and less_tr2: "bdd_all (dfa_is_node B) (fst B ! j)" by (simp add: wf_dfa_def list_all_iff dfa_is_node_def)+
from bddh_tr1 bddh_tr2 have 1: "bddh n (bdd_binop (λk l. the (fst (prod_dfs A B (0, 0)) ! k ! l)) (fst A ! i) (fst B ! j))"
by (simp add: bddh_binop)
have "∀bs. length bs = n ⟶ the (fst (prod_dfs A B (0, 0)) ! dfa_trans A i bs ! dfa_trans B j bs)
< length (snd (prod_dfs A B (0, 0)))"
proof (intro strip)
fix bs
assume bs: "length (bs::bool list) = n"
moreover note i j
moreover from well_formed1 well_formed2 have "dfa_is_node A 0" and "dfa_is_node B 0"
by (simp add: dfa_is_node_def wf_dfa_def)+
moreover note ij_k
ultimately obtain m where "fst (prod_dfs A B (0, 0)) ! dfa_trans A i bs ! dfa_trans B j bs = Some m"
and "m < length (snd (prod_dfs A B (0, 0)))" by (rule prod_dfs_statetrans)
then show "the (fst (prod_dfs A B (0,0)) ! dfa_trans A i bs ! dfa_trans B j bs) < length (snd (prod_dfs A B (0,0)))" by simp
qed
with bddh_tr1 bddh_tr2 have 2: "bdd_all (λq. q < length (snd (prod_dfs A B (0, 0)))) (bdd_binop (λk l. the (fst (prod_dfs A B (0,0)) ! k ! l)) (fst A ! i) (fst B ! j))"
by (simp add: bddh_binop bdd_lookup_binop bdd_all_bdd_lookup_iff[of n _ "λx. x < length (snd (prod_dfs A B (0,0)))"] dfa_trans_def)
note this 1
}
hence 1: "list_all (bddh n) ?tr" and 2: "list_all (bdd_all (λq. q < length ?tr)) ?tr" by (auto simp: split_paired_all list_all_iff)
from well_formed1 well_formed2 have 3: "fst (prod_dfs A B (0, 0)) ! 0 ! 0 = Some 0" by (simp add: wf_dfa_def dfa_is_node_def prod_dfs_start)
from is_node_s1_s2 have "(fst (prod_dfs A B (0,0)) ! 0 ! 0 = Some 0 ∧ dfa_is_node A 0 ∧ dfa_is_node B 0) =
(0 < length (snd (prod_dfs A B (0,0))) ∧ snd (prod_dfs A B (0,0)) ! 0 = (0,0))" by (rule prod_dfs_bij)
with 3 well_formed1 well_formed2 have "0 < length (snd (prod_dfs A B (0,0)))" by (simp add: wf_dfa_def dfa_is_node_def)
with 1 2 3 show "wf_dfa (binop_dfa f A B) n" by (simp add: binop_dfa_def wf_dfa_def split_beta dfa_is_node_def)
qed

theorem binop_dfa_reachable:
assumes bss: "list_all (is_alph n) bss"
shows "(∃m. dfa_reach (binop_dfa f A B) 0 bss m ∧
fst (prod_dfs A B (0, 0)) ! s⇩1 ! s⇩2 = Some m ∧
dfa_is_node A s⇩1 ∧ dfa_is_node B s⇩2) =
(dfa_reach A 0 bss s⇩1 ∧ dfa_reach B 0 bss s⇩2)"
proof -
let ?tr = "map (λ(i, j).
bdd_binop (λk l. the (fst (prod_dfs A B (0,0)) ! k ! l)) (fst A ! i) (fst B ! j))
(snd (prod_dfs A B (0,0)))"
have T: "?tr = fst (binop_dfa f A B)" by (simp add: binop_dfa_def split_beta)
from well_formed1 well_formed2 have is_node_s1_s2: "prod_is_node A B (0, 0)" by (simp add: prod_is_node_def wf_dfa_def dfa_is_node_def)
from well_formed1 well_formed2 have s1: "dfa_is_node A 0" and s2: "dfa_is_node B 0" by (simp add: dfa_is_node_def wf_dfa_def)+
from s1 s2 have start: "fst (prod_dfs A B (0,0)) ! 0 ! 0 = Some 0"
by (rule prod_dfs_start)
show "(∃m. dfa_reach (binop_dfa f A B) 0 bss m ∧
fst (prod_dfs A B (0, 0)) ! s⇩1 ! s⇩2 = Some m ∧
dfa_is_node A s⇩1 ∧ dfa_is_node B s⇩2) =
(dfa_reach A 0 bss s⇩1 ∧ dfa_reach B 0 bss s⇩2)"
(is "(∃m. ?lhs1 m ∧ ?lhs2 m ∧ ?lhs3 ∧ ?lhs4) = ?rhs"
is "?lhs = _")
proof
assume "∃m. ?lhs1 m ∧ ?lhs2 m ∧ ?lhs3 ∧ ?lhs4"
then obtain m where lhs: "?lhs1 m" "?lhs2 m" "?lhs3" "?lhs4" by auto
from lhs bss show ?rhs
proof (induct arbitrary: s⇩1 s⇩2)
case Nil
from is_node_s1_s2
s1 s2 ‹dfa_is_node A s⇩1› ‹dfa_is_node B s⇩2›
have "(0, 0) = (s⇩1, s⇩2)"
using start ‹fst (prod_dfs A B (0,0)) ! s⇩1 ! s⇩2 = Some 0›
by (rule prod_dfs_inj)
moreover have "dfa_reach A 0 [] 0" by (rule reach_nil)
moreover have "dfa_reach B 0 [] 0" by (rule reach_nil)
ultimately show ?case by simp
next
case (snoc j bss bs s⇩1 s⇩2)
then have "length bs = n" by (simp add: is_alph_def)
moreover from binop_wf_dfa have "dfa_is_node (binop_dfa f A B) 0" by (simp add: dfa_is_node_def wf_dfa_def)
with snoc binop_wf_dfa [of f] have "dfa_is_node (binop_dfa f A B) j" by (simp add: dfa_reach_is_node)
then have j: "j < length (snd (prod_dfs A B (0,0)))" by (simp add: binop_dfa_def dfa_is_node_def split_beta)
with prod_dfs_bij [OF is_node_s1_s2,
of "fst (snd (prod_dfs A B (0,0)) ! j)" "snd (snd (prod_dfs A B (0,0)) ! j)"]
have j_tr1: "dfa_is_node A (fst (snd (prod_dfs A B (0,0)) ! j))"
and j_tr2: "dfa_is_node B (snd (snd (prod_dfs A B (0,0)) ! j))"
and Some_j: "fst (prod_dfs A B (0,0)) ! fst (snd (prod_dfs A B (0,0)) ! j) ! snd (snd (prod_dfs A B (0,0)) ! j) = Some j"
by auto
note j_tr1 j_tr2 s1 s2 Some_j
ultimately obtain k
where k: "fst (prod_dfs A B (0,0)) !
dfa_trans A (fst (snd (prod_dfs A B (0, 0)) ! j)) bs !
dfa_trans B (snd (snd (prod_dfs A B (0, 0)) ! j)) bs = Some k"
and s_tr1': "dfa_is_node A (dfa_trans A (fst (snd (prod_dfs A B (0,0)) ! j)) bs)"
and s_tr2': "dfa_is_node B (dfa_trans B (snd (snd (prod_dfs A B (0,0)) ! j)) bs)"
by (rule prod_dfs_statetrans)

from well_formed1 well_formed2 j_tr1 j_tr2 snoc
have lh: "bddh (length bs) (fst A ! fst (snd (prod_dfs A B (0,0)) ! j))"
and rh: "bddh (length bs) (fst B ! snd (snd (prod_dfs A B (0,0)) ! j))"
by (auto simp: wf_dfa_def dfa_is_node_def list_all_iff is_alph_def)
from snoc(3)[unfolded dfa_trans_def binop_dfa_def Let_def split_beta fst_conv nth_map[OF j] bdd_lookup_binop[OF lh,OF rh], folded dfa_trans_def] k
have "fst (prod_dfs A B (0,0)) ! s⇩1 ! s⇩2 = Some k" by simp
with is_node_s1_s2 ‹dfa_is_node A s⇩1› ‹dfa_is_node B s⇩2› s_tr1' s_tr2'
have "(s⇩1, s⇩2) = (dfa_trans A (fst (snd (prod_dfs A B (0,0)) ! j)) bs, dfa_trans B (snd (snd (prod_dfs A B (0,0)) ! j)) bs)"
using k
by (rule prod_dfs_inj)
moreover from snoc Some_j j_tr1 j_tr2
have "dfa_reach A 0 bss (fst (snd (prod_dfs A B (0,0)) ! j))" by simp
hence "dfa_reach A 0 (bss @ [bs]) (dfa_trans A (fst (snd (prod_dfs A B (0,0)) ! j)) bs)"
by (rule reach_snoc)
moreover from snoc Some_j j_tr1 j_tr2
have "dfa_reach B 0 bss (snd (snd (prod_dfs A B (0,0)) ! j))" by simp
hence "dfa_reach B 0 (bss @ [bs]) (dfa_trans B (snd (snd (prod_dfs A B (0,0)) ! j)) bs)"
by (rule reach_snoc)
ultimately show "dfa_reach A 0 (bss @ [bs]) s⇩1 ∧ dfa_reach B 0 (bss @ [bs]) s⇩2"
by simp
qed
next
assume ?rhs
hence reach: "dfa_reach A 0 bss s⇩1" "dfa_reach B 0 bss s⇩2" by simp_all
then show ?lhs using bss
proof (induct arbitrary: s⇩2)
case Nil
with start s1 s2 show ?case
by (auto intro: reach_nil simp: reach_nil_iff)
next
case (snoc j bss bs s⇩2)
from snoc(3)
obtain s⇩2' where reach_s2': "dfa_reach B 0 bss s⇩2'" and s2': "s⇩2 = dfa_trans B s⇩2' bs"
by (auto simp: reach_snoc_iff)
from snoc(2) [OF reach_s2'] snoc(4)
obtain m where reach_m: "dfa_reach (binop_dfa f A B) 0 bss m"
and m: "fst (prod_dfs A B (0,0)) ! j ! s⇩2' = Some m"
and j: "dfa_is_node A j" and s2'': "dfa_is_node B s⇩2'"
by auto
from snoc have "list_all (is_alph n) bss" by simp
with binop_wf_dfa reach_m dfa_startnode_is_node[OF binop_wf_dfa]
have m_less: "dfa_is_node (binop_dfa f A B) m"
by (rule dfa_reach_is_node)
from is_node_s1_s2 m j s2''
have m': "(m < length (snd (prod_dfs A B (0,0))) ∧
snd (prod_dfs A B (0,0)) ! m = (j, s⇩2'))"
by (simp add: prod_dfs_bij [symmetric])
with j s2'' have "dfa_is_node A (fst (snd (prod_dfs A B (0,0)) ! m))"
"dfa_is_node B (snd (snd (prod_dfs A B (0,0)) ! m))"
by simp_all
with well_formed1 well_formed2 snoc
have bddh: "bddh (length bs) (fst A ! fst (snd (prod_dfs A B (0,0)) ! m))"
"bddh (length bs) (fst B ! snd (snd (prod_dfs A B (0,0)) ! m))"
by (simp add: wf_dfa_def is_alph_def dfa_is_node_def list_all_iff)+
from snoc have "length bs = n" by (simp add: is_alph_def)
then obtain k where k: "fst (prod_dfs A B (0,0)) !
dfa_trans A j bs ! dfa_trans B s⇩2' bs = Some k"
and s_tr1: "dfa_is_node A (dfa_trans A j bs)"
and s_tr2: "dfa_is_node B (dfa_trans B s⇩2' bs)"
using j s2'' s1 s2 m
by (rule prod_dfs_statetrans)
show ?case
apply (rule exI)
apply (simp add: s2')
apply (intro conjI)
apply (rule reach_snoc)
apply (rule reach_m)
apply (cut_tac m_less)
apply (simp add: dfa_trans_def binop_dfa_def split_beta dfa_is_node_def)
apply (simp add: bddh bdd_lookup_binop split_beta)
apply (simp add: dfa_trans_def[symmetric] m' k)
apply (rule s_tr1)
apply (rule s_tr2)
done
qed
qed
qed

lemma binop_dfa_steps:
assumes X: "list_all (is_alph n) bs"
shows "snd (binop_dfa f A B) ! dfa_steps (binop_dfa f A B) 0 bs = f (snd A ! dfa_steps A 0 bs) (snd B ! dfa_steps B 0 bs)"
(is "?as3 ! dfa_steps ?A 0 bs = ?rhs")
proof -
note 2 = dfa_startnode_is_node[OF well_formed1]
note 5 = dfa_startnode_is_node[OF well_formed2]
note B = dfa_startnode_is_node[OF binop_wf_dfa]
define tab where "tab = fst (prod_dfs A B (0,0))"
define ps where "ps = snd (prod_dfs A B (0,0))"
from tab_def ps_def have prod: "prod_dfs A B (0,0) = (tab, ps)" by simp
define s1 where "s1 = dfa_steps A 0 bs"
define s2 where "s2 = dfa_steps B 0 bs"
with s1_def have "dfa_reach A 0 bs s1" and "dfa_reach B 0 bs s2" by (simp add: reach_def)+
with X have "∃m. dfa_reach ?A 0 bs m ∧ fst (prod_dfs A B (0, 0)) ! s1 ! s2 = Some m ∧ dfa_is_node A s1 ∧ dfa_is_node B s2"
by (simp add: binop_dfa_reachable)
with tab_def have "∃m. dfa_reach ?A 0 bs m ∧ tab ! s1 ! s2 = Some m ∧ dfa_is_node A s1 ∧ dfa_is_node B s2" by simp
then obtain m where R: "dfa_reach ?A 0 bs m" and M: "tab ! s1 ! s2 = Some m" and s1: "dfa_is_node A s1" and s2: "dfa_is_node B s2" by blast
hence M': "m = dfa_steps ?A 0 bs" by (simp add: reach_def)
from B X R binop_wf_dfa [of f] have mL: "dfa_is_node ?A m" by (simp add: dfa_reach_is_node)
from 2 5 M s1 s2 have bij: "m < length (snd (prod_dfs A B (0, 0))) ∧ snd (prod_dfs A B (0, 0)) ! m = (s1, s2)" unfolding tab_def
by (simp add: prod_dfs_bij[symmetric] prod_is_node_def)
with mL have "snd (binop_dfa f A B) ! m = f (snd A ! s1) (snd B ! s2)"
by (simp add: binop_dfa_def split_beta dfa_is_node_def)
with M' s1_def s2_def
show "snd ?A ! dfa_steps ?A 0 bs = f (snd A ! dfa_steps A 0 bs) (snd B ! dfa_steps B 0 bs)"
by simp
qed

end

lemma binop_wf_dfa:
assumes A: "wf_dfa A n" and B: "wf_dfa B n"
shows "wf_dfa (binop_dfa f A B) n"
proof -
from A B
interpret prod_DFS A B n by unfold_locales
show ?thesis by (rule binop_wf_dfa)
qed

theorem binop_dfa_accepts:
assumes A: "wf_dfa A n"
and B: "wf_dfa B n"
and X: "list_all (is_alph n) bss"
shows "dfa_accepts (binop_dfa f A B) bss = f (dfa_accepts A bss) (dfa_accepts B bss)"
proof -
from A B
interpret prod_DFS A B n by unfold_locales
from X show ?thesis
by (simp add: accepts_def dfa_accepting_def binop_dfa_steps)
qed

definition
and_dfa :: "dfa ⇒ dfa ⇒ dfa" where
"and_dfa = binop_dfa (∧)"

lemma and_wf_dfa:
assumes "wf_dfa M n"
and "wf_dfa N n"
shows "wf_dfa (and_dfa M N) n"
using assms by (simp add: and_dfa_def binop_wf_dfa)

lemma and_dfa_accepts:
assumes "wf_dfa M n"
and "wf_dfa N n"
and "list_all (is_alph n) bs"
shows "dfa_accepts (and_dfa M N) bs = (dfa_accepts M bs ∧ dfa_accepts N bs)"
using assms by (simp add: binop_dfa_accepts and_dfa_def)

definition
or_dfa :: "dfa ⇒ dfa ⇒ dfa" where
"or_dfa = binop_dfa (∨)"

lemma or_wf_dfa:
assumes "wf_dfa M n" and "wf_dfa N n"
shows "wf_dfa (or_dfa M N) n"
using assms by (simp add: or_dfa_def binop_wf_dfa)

lemma or_dfa_accepts:
assumes "wf_dfa M n" and "wf_dfa N n"
and "list_all (is_alph n) bs"
shows "dfa_accepts (or_dfa M N) bs = (dfa_accepts M bs ∨ dfa_accepts N bs)"
using assms by (simp add: binop_dfa_accepts or_dfa_def)

definition
imp_dfa :: "dfa ⇒ dfa ⇒ dfa" where
"imp_dfa = binop_dfa (⟶)"

lemma imp_wf_dfa:
assumes "wf_dfa M n" and "wf_dfa N n"
shows "wf_dfa (imp_dfa M N) n"
using assms by (simp add: binop_wf_dfa imp_dfa_def)

lemma imp_dfa_accepts:
assumes "wf_dfa M n" and "wf_dfa N n"
and "list_all (is_alph n) bs"
shows "dfa_accepts (imp_dfa M N) bs = (dfa_accepts M bs ⟶ dfa_accepts N bs)"
using assms by (auto simp add: binop_dfa_accepts imp_dfa_def)

subsection ‹Transforming DFAs to NFAs›

definition
nfa_of_dfa :: "dfa ⇒ nfa" where
"nfa_of_dfa = (λ(bdd,as). (map (bdd_map (λq. (replicate (length bdd) False)[q:=True])) bdd, as))"

lemma dfa2wf_nfa:
assumes "wf_dfa M n"
shows "wf_nfa (nfa_of_dfa M) n"
proof -
have "⋀a. dfa_is_node M a ⟹ nfa_is_node (nfa_of_dfa M) ((replicate (length (fst M)) False)[a:=True])"
by (simp add: dfa_is_node_def nfa_is_node_def nfa_of_dfa_def split_beta)
hence "⋀bdd. bdd_all (dfa_is_node M) bdd ⟹ bdd_all (nfa_is_node (nfa_of_dfa M)) (bdd_map (λq. (replicate (length (fst M)) False)[q:=True]) bdd)"
by (simp add: bdd_all_bdd_map)
with assms have "list_all (bdd_all (nfa_is_node (nfa_of_dfa M))) (fst (nfa_of_dfa M))" by (simp add: list_all_iff split_beta nfa_of_dfa_def wf_dfa_def)
with assms show ?thesis by (simp add: wf_nfa_def wf_dfa_def nfa_of_dfa_def split_beta list_all_iff bddh_bdd_map)
qed

lemma replicate_upd_inj: "⟦q < n; (replicate n False)[q:=True] = (replicate n False)[p:=True]⟧ ⟹ (q = p)" (is "⟦_ ;?lhs = ?rhs⟧ ⟹  _")
proof -
assume q: "q < n" and r: "?lhs = ?rhs"
{ assume "p ≠ q"
with q have "?lhs ! q = True" by simp
moreover from ‹p ≠ q› q have "?rhs ! q = False" by simp
ultimately have "?lhs ≠ ?rhs" by auto
}
with r show "q = p" by auto
qed

lemma nfa_of_dfa_reach':
assumes V: "wf_dfa M l"
and X: "list_all (is_alph l) bss"
and N: "n1 = (replicate (length (fst M)) False)[q:=True]"
and Q: "dfa_is_node M q"
and R: "nfa_reach (nfa_of_dfa M) n1 bss n2"
shows "∃p. dfa_reach M q bss p ∧ n2 = (replicate (length (fst M)) False)[p:=True]"
proof -
from R V X N Q show ?thesis proof induct
case Nil
hence "dfa_reach M q [] q" by (simp add: reach_nil)
with Nil show ?case by auto
next
case (snoc j bss bs)
hence N1: "nfa_is_node (nfa_of_dfa M) n1" by (simp add: nfa_is_node_def nfa_of_dfa_def split_beta)
from snoc have V2: "wf_nfa (nfa_of_dfa M) l" by (