Session Presburger-Automata

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 = (xxs. 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 l1 r1) (Branch l2 r2) = Branch (bdd_binop f l1 l2) (bdd_binop f r1 r2)"

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)"

lemma add_leaves_bdd_lookup:
  "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

lemma add_leaves_bdd_all_eq:
  "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)

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

lemma add_leaves_mono:
  "set xs  set ys  set (add_leaves tr xs)  set (add_leaves tr ys)"
  by (induct tr arbitrary: xs ys) auto

lemma add_leaves_binop_subset:
  "set (add_leaves (bdd_binop f b b') [f x y. x  xs, y  ys]) 
   (xset (add_leaves b xs). yset (add_leaves b' ys). {f x y})" (is "?A  ?B")
proof -
  have "?A  (xset (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 l1 r1 l2 r2 xs ys) then show ?case
    apply auto
    apply (drule_tac ys1="[f x y. x  add_leaves l1 xs, y  add_leaves l2 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 "(xset (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 "aq")
        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 " = ((aq  ?Q 0)  (¬ (aq)  (j. ?Q j)))" by auto
        also have " = ((a  q  (j. ?Q j))  (¬(aq)  (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: add_leaves_bdd_all_eq' list_all_iff)
  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)) ! s1 ! s2 = Some m 
    dfa_is_node A s1  dfa_is_node B s2) =
   (dfa_reach A 0 bss s1  dfa_reach B 0 bss s2)"
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)) ! s1 ! s2 = Some m 
     dfa_is_node A s1  dfa_is_node B s2) =
    (dfa_reach A 0 bss s1  dfa_reach B 0 bss s2)"
    (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: s1 s2)
      case Nil
      from is_node_s1_s2
        s1 s2 ‹dfa_is_node A s1 ‹dfa_is_node B s2
      have "(0, 0) = (s1, s2)"
        using start ‹fst (prod_dfs A B (0,0)) ! s1 ! s2 = 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 s1 s2)
      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)) ! s1 ! s2 = Some k" by simp
      with is_node_s1_s2 ‹dfa_is_node A s1 ‹dfa_is_node B s2 s_tr1' s_tr2'
      have "(s1, s2) = (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]) s1  dfa_reach B 0 (bss @ [bs]) s2"
        by simp
    qed
  next
    assume ?rhs
    hence reach: "dfa_reach A 0 bss s1" "dfa_reach B 0 bss s2" by simp_all
    then show ?lhs using bss
    proof (induct arbitrary: s2)
      case Nil
      with start s1 s2 show ?case
        by (auto intro: reach_nil simp: reach_nil_iff)
    next
      case (snoc j bss bs s2)
      from snoc(3)
      obtain s2' where reach_s2': "dfa_reach B 0 bss s2'" and s2': "s2 = dfa_trans B s2' 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 ! s2' = Some m"
        and j: "dfa_is_node A j" and s2'': "dfa_is_node B s2'"
        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, s2'))"
        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 s2' 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 s2' 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 (